Skip to content

GitLab

why3
why3
Commit 9c27debd authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files
Options

- fix a bug in eliminate_let 

- move compile_match to Eliminate_algebraic
- move eliminate_builtin to Eliminate_definition
parent e59c5618
Hide whitespace changes
Inline Side-by-side
Showing with 80 additions and 176 deletions
Makefile.in
View file @ 9c27debd
......@@ -103,8 +103,7 @@ LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
LIB_TRANSFORM = simplify_recursive_definition inlining \
split_conjunction encoding_decorate \
eliminate_builtin eliminate_definition \
compile_match eliminate_algebraic \
eliminate_definition eliminate_algebraic \
eliminate_inductive eliminate_let eliminate_if
LIB_PRINTER = print_real alt_ergo why3 smt coq
......
src/transform/compile_match.ml deleted 100644 → 0
View file @ e59c5618
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Term
open Decl
open Task
let rec rewriteT kn t = match t.t_node with
| Tcase (tl,bl) ->
let tl = List.map (rewriteT kn) tl in
let mk_b (pl,t) = (pl, rewriteT kn t) in
let bl = List.map (fun b -> mk_b (t_open_branch b)) bl in
Pattern.CompileTerm.compile (find_constructors kn) tl bl
| _ -> t_map (rewriteT kn) (rewriteF kn) t
and rewriteF kn f = match f.f_node with
| Fcase (tl,bl) ->
let tl = List.map (rewriteT kn) tl in
let mk_b (pl,f) = (pl, rewriteF kn f) in
let bl = List.map (fun b -> mk_b (f_open_branch b)) bl in
Pattern.CompileFmla.compile (find_constructors kn) tl bl
| _ -> f_map (rewriteT kn) (rewriteF kn) f
let comp t task =
let fnT = rewriteT t.task_known in
let fnF = rewriteF t.task_known in
match t.task_decl with
| Decl d -> add_decl task (decl_map fnT fnF d)
| td -> add_tdecl task td
let compile_match = Register.store (fun () -> Trans.map comp None)
src/transform/compile_match.mli deleted 100644 → 0
View file @ e59c5618
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
val compile_match : Task.task Register.trans_reg
src/transform/eliminate_algebraic.ml
View file @ 9c27debd
......@@ -24,6 +24,35 @@ open Term
open Decl
open Task
(** Compile match patterns *)
let rec rewriteT kn t = match t.t_node with
| Tcase (tl,bl) ->
let tl = List.map (rewriteT kn) tl in
let mk_b (pl,t) = (pl, rewriteT kn t) in
let bl = List.map (fun b -> mk_b (t_open_branch b)) bl in
Pattern.CompileTerm.compile (find_constructors kn) tl bl
| _ -> t_map (rewriteT kn) (rewriteF kn) t
and rewriteF kn f = match f.f_node with
| Fcase (tl,bl) ->
let tl = List.map (rewriteT kn) tl in
let mk_b (pl,f) = (pl, rewriteF kn f) in
let bl = List.map (fun b -> mk_b (f_open_branch b)) bl in
Pattern.CompileFmla.compile (find_constructors kn) tl bl
| _ -> f_map (rewriteT kn) (rewriteF kn) f
let comp t task =
let fnT = rewriteT t.task_known in
let fnF = rewriteF t.task_known in
match t.task_decl with
| Decl d -> add_decl task (decl_map fnT fnF d)
| td -> add_tdecl task td
let compile_match = Register.store (fun () -> Trans.map comp None)
(** Eliminate algebraic types and match statements *)
type state = {
mt_map : lsymbol Mts.t; (* from type symbols to selector functions *)
pj_map : lsymbol list Mls.t; (* from constructors to projections *)
......@@ -209,7 +238,7 @@ let eliminate_compiled_algebraic =
Register.store (fun () -> Trans.fold_map comp empty_state None)
let eliminate_algebraic =
Register.compose Compile_match.compile_match eliminate_compiled_algebraic
Register.compose compile_match eliminate_compiled_algebraic
let () = Register.register_transform "eliminate_algebraic" eliminate_algebraic
src/transform/eliminate_algebraic.mli
View file @ 9c27debd
......@@ -17,6 +17,8 @@
(* *)
(**************************************************************************)
val compile_match : Task.task Register.trans_reg
val eliminate_compiled_algebraic : Task.task Register.trans_reg
val eliminate_algebraic : Task.task Register.trans_reg
......
src/transform/eliminate_builtin.ml deleted 100644 → 0
View file @ e59c5618
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Util
open Ident
open Term
open Decl
let add_ld q = function
| ls, Some _ when Driver.query_remove q ls.ls_name -> (ls, None)
| d -> d
let add_id q (ld,id) = function
| ls, _ when Driver.query_remove q ls.ls_name -> (ls, None)::ld, id
| d -> ld, d::id
let elim q d = match d.d_node with
| Dlogic l ->
create_logic_decls (List.map (add_ld q) l)
| Dind l ->
let ld, id = List.fold_left (add_id q) ([],[]) l in
create_logic_decls (List.rev ld) @ create_ind_decls (List.rev id)
| _ -> [d]
let eliminate_builtin =
Register.store_query (fun q -> Trans.decl (elim q) None)
let () = Register.register_transform "eliminate_builtin" eliminate_builtin
src/transform/eliminate_builtin.mli deleted 100644 → 0
View file @ e59c5618
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
val eliminate_builtin : Task.task Register.trans_reg
src/transform/eliminate_definition.ml
View file @ 9c27debd
......@@ -22,6 +22,31 @@ open Ident
open Term
open Decl
(** Discard defintions of built-in symbols *)
let add_ld q = function
| ls, Some _ when Driver.query_remove q ls.ls_name -> (ls, None)
| d -> d
let add_id q (ld,id) = function
| ls, _ when Driver.query_remove q ls.ls_name -> (ls, None)::ld, id
| d -> ld, d::id
let elim q d = match d.d_node with
| Dlogic l ->
create_logic_decls (List.map (add_ld q) l)
| Dind l ->
let ld, id = List.fold_left (add_id q) ([],[]) l in
create_logic_decls (List.rev ld) @ create_ind_decls (List.rev id)
| _ -> [d]
let eliminate_builtin =
Register.store_query (fun q -> Trans.decl (elim q) None)
let () = Register.register_transform "eliminate_builtin" eliminate_builtin
(** Eliminate definitions of functions and predicates *)
let rec t_insert hd t = match t.t_node with
| Tif (f1,t2,t3) ->
f_if f1 (t_insert hd t2) (t_insert hd t3)
......
src/transform/eliminate_definition.mli
View file @ 9c27debd
......@@ -17,6 +17,8 @@
(* *)
(**************************************************************************)
val eliminate_builtin : Task.task Register.trans_reg
val eliminate_definition_func : Task.task Register.trans_reg
val eliminate_definition_pred : Task.task Register.trans_reg
val eliminate_definition : Task.task Register.trans_reg
......
src/transform/eliminate_if.ml
View file @ 9c27debd
......@@ -22,7 +22,7 @@ open Ident
open Term
open Decl
(* eliminate if-then-else in terms *)
(** Eliminate if-then-else in terms *)
let rec elim_t letl contT t = match t.t_node with
| Tlet (t1,tb) ->
......@@ -86,7 +86,9 @@ let elim_d d = match d.d_node with
| _ ->
[decl_map (fun _ -> assert false) elim_f d]
(* eliminate if-then-else in formulas *)
let eliminate_if_term = Register.store (fun () -> Trans.decl elim_d None)
(** Eliminate if-then-else in formulas *)
let rec elim_t t = t_map elim_t (elim_f true) t
......@@ -101,11 +103,6 @@ and elim_f sign f = match f.f_node with
| _ ->
f_map_sign elim_t elim_f sign f
(* registration *)
let eliminate_if_term =
Register.store (fun () -> Trans.decl elim_d None)
let eliminate_if_fmla =
Register.store (fun () -> Trans.rewrite elim_t (elim_f true) None)
......
src/transform/eliminate_let.ml
View file @ 9c27debd
......@@ -24,44 +24,32 @@ open Decl
(* eliminate let *)
let rec remove_let_t fnF map t = match t.t_node with
let rec elim_t func pred map t = match t.t_node with
| Tvar vs ->
(try Mvs.find vs map with Not_found -> t)
| Tlet (t1,tb) ->
let t1 = remove_let_t fnF map t1 in
| Tlet (t1,tb) when func ->
let vs,t2 = t_open_bound tb in
remove_let_t fnF (Mvs.add vs t1 map) t2
let t1 = elim_t func pred map t1 in
elim_t func pred (Mvs.add vs t1 map) t2
| _ ->
t_map (remove_let_t fnF map) (fnF map) t
t_map (elim_t func pred map) (elim_f func pred map) t
and remove_let_f fnT map f = match f.f_node with
| Flet (t1,fb) ->
let t1 = fnT map t1 in
and elim_f func pred map f = match f.f_node with
| Flet (t1,fb) when pred ->
let vs,f2 = f_open_bound fb in
remove_let_f fnT (Mvs.add vs t1 map) f2
let t1 = elim_t func pred map t1 in
elim_f func pred (Mvs.add vs t1 map) f2
| _ ->
f_map (fnT map) (remove_let_f fnT map) f
f_map (elim_t func pred map) (elim_f func pred map) f
let rec elim_let_t map t = remove_let_t elim_let_f map t
and elim_let_f map f = remove_let_f elim_let_t map f
let eliminate_let_term = Register.store (fun () -> Trans.rewrite
(elim_t true false Mvs.empty) (elim_f true false Mvs.empty) None)
let elim_let_t = elim_let_t Mvs.empty
let elim_let_f = elim_let_f Mvs.empty
let eliminate_let_fmla = Register.store (fun () -> Trans.rewrite
(elim_t false true Mvs.empty) (elim_f false true Mvs.empty) None)
let rec skip_t map t = t_map (skip_t map) (remove_let_f skip_t map) t
let rec skip_f map f = f_map (remove_let_t skip_f map) (skip_f map) f
let skip_t = skip_t Mvs.empty
let skip_f = skip_f Mvs.empty
let eliminate_let_term =
Register.store (fun () -> Trans.rewrite elim_let_t skip_f None)
let eliminate_let_fmla =
Register.store (fun () -> Trans.rewrite skip_t elim_let_f None)
let eliminate_let =
Register.store (fun () -> Trans.rewrite elim_let_t elim_let_f None)
let eliminate_let = Register.store (fun () -> Trans.rewrite
(elim_t true true Mvs.empty) (elim_f true true Mvs.empty) None)
let () =
Register.register_transform "eliminate_let_term" eliminate_let_term;
......
src/transform/eliminate_let.mli
View file @ 9c27debd
......@@ -19,9 +19,6 @@
(** eliminate let *)
val elim_let_t : Term.term -> Term.term
val elim_let_f : Term.fmla -> Term.fmla
val eliminate_let_term : Task.task Register.trans_reg
val eliminate_let_fmla : Task.task Register.trans_reg
val eliminate_let : Task.task Register.trans_reg
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment