diff --git a/Makefile.in b/Makefile.in index b69a227073d7b11636d9f9ad49b264c34941141b..33f40eef051c5a74cb9f0416b7163d97c7d0dc86 100644 --- a/Makefile.in +++ b/Makefile.in @@ -134,7 +134,7 @@ TRANSFORM_CMO := simplify_recursive_definition.cmo inlining.cmo\ split_conjunction.cmo encoding_decorate.cmo\ remove_logic_definition.cmo eliminate_inductive.cmo\ compile_match.cmo eliminate_algebraic.cmo\ - eliminate_definition.cmo eliminate_let.cmo + eliminate_let.cmo eliminate_definition.cmo TRANSFORM_CMO := $(addprefix src/transform/,$(TRANSFORM_CMO)) DRIVER_CMO := call_provers.cmo dynlink_compat.cmo driver_parser.cmo\ diff --git a/src/transform/eliminate_definition.ml b/src/transform/eliminate_definition.ml index 884acff23b7c8044681ec19a6c6c52f60761595f..6e7fdf75a378fe34ca7eaa16e342a11ab7f2efb1 100644 --- a/src/transform/eliminate_definition.ml +++ b/src/transform/eliminate_definition.ml @@ -17,29 +17,146 @@ (* *) (**************************************************************************) +open Util open Ident +open Ty open Term open Decl +open Task -let add_ls acc (ls,_) = create_logic_decl [ls,None] :: acc +let unfold_t lm e = List.fold_left (fun e (v,t) -> t_let v t e) e lm +let unfold_f lm e = List.fold_left (fun e (v,t) -> f_let v t e) e lm -let add_ld acc ls ld = - let id = ls.ls_name.id_long ^ "_def" in - let pr = create_prsymbol (id_derive id ls.ls_name) in - create_prop_decl Paxiom pr (ls_defn_axiom ld) :: acc +let add_t_ax task nm ls hd e = + let vl = Svs.elements (t_freevars Svs.empty hd) in + let ax = f_forall vl [[Term hd]] (f_equ hd e) in + let id = id_derive (nm ^ "_def") ls.ls_name in +try + add_decl task (create_prop_decl Paxiom (create_prsymbol id) ax) +with +UnboundVars vs -> + Format.printf "@[%a@\n@]" Pretty.print_fmla ax; assert false -let add_ld acc (ls,ld) = match ld with - | None -> acc - | Some ld -> add_ld acc ls ld +let add_f_ax task nm ls hd e = + let vl = Svs.elements (f_freevars Svs.empty hd) in + let ax = f_forall vl [[Fmla hd]] (f_iff_simp hd e) in + let id = id_derive (nm ^ "_def") ls.ls_name in + add_decl task (create_prop_decl Paxiom (create_prsymbol id) ax) -let elim d = match d.d_node with +let uncompiled = "eliminate_algebraic: compile_match required" + +let rec add_fd kn task nm ls hd lm e = match e.t_node with + | Tlet (t,b) -> + let v,e = t_open_bound b in + add_fd kn task nm ls hd ((v,t)::lm) e + | Tcase ([t],bl) -> + let t = Eliminate_let.remove_let_t (unfold_t lm t) in + begin match t.t_node with + | Tvar v -> + let mk_br (w,m) br = + let (pl,e) = t_open_branch br in + match pl with + | [{ pat_node = Papp (cs,pl) }] -> + let mk_var p = match p.pat_node with + | Pvar v -> t_var v + | _ -> failwith uncompiled + in + w, Mls.add cs (t_app cs (List.map mk_var pl) v.vs_ty, e) m + | [{ pat_node = Pwild }] -> + Some e, m + | _ -> failwith uncompiled + in + let w,m = List.fold_left mk_br (None,Mls.empty) bl in + let find cs = try Mls.find cs m with Not_found -> + let u = id_fresh "u" in + let s = ty_match Mtv.empty (of_option cs.ls_value) v.vs_ty in + let mk_v ty = t_var (create_vsymbol u (ty_inst s ty)) in + t_app cs (List.map mk_v cs.ls_args) v.vs_ty, of_option w + in + let ts = match v.vs_ty.ty_node with + | Tyapp (ts,_) -> ts + | _ -> failwith uncompiled + in + let add_cs tsk cs = + let t,e = find cs in + let lm = lm @ [v,t] in + let hd = t_subst_single v t hd in + add_fd kn tsk (nm ^ "_" ^ cs.ls_name.id_long) ls hd lm e + in + List.fold_left add_cs task (find_constructors kn ts) + | _ -> + add_t_ax task nm ls hd (unfold_t lm e) + end + | _ -> add_t_ax task nm ls hd (unfold_t lm e) + +let rec add_pd kn task nm ls hd lm e = match e.f_node with + | Flet (t,b) -> + let v,e = f_open_bound b in + add_pd kn task nm ls hd ((v,t)::lm) e + | Fcase ([t],bl) -> + let t = Eliminate_let.remove_let_t (unfold_t lm t) in + begin match t.t_node with + | Tvar v -> + let mk_br (w,m) br = + let (pl,e) = f_open_branch br in + match pl with + | [{ pat_node = Papp (cs,pl) }] -> + let mk_var p = match p.pat_node with + | Pvar v -> t_var v + | _ -> failwith uncompiled + in + w, Mls.add cs (t_app cs (List.map mk_var pl) v.vs_ty, e) m + | [{ pat_node = Pwild }] -> + Some e, m + | _ -> failwith uncompiled + in + let w,m = List.fold_left mk_br (None,Mls.empty) bl in + let find cs = try Mls.find cs m with Not_found -> + let u = id_fresh "u" in + let s = ty_match Mtv.empty (of_option cs.ls_value) v.vs_ty in + let mk_v ty = t_var (create_vsymbol u (ty_inst s ty)) in + t_app cs (List.map mk_v cs.ls_args) v.vs_ty, of_option w + in + let ts = match v.vs_ty.ty_node with + | Tyapp (ts,_) -> ts + | _ -> failwith uncompiled + in + let add_cs tsk cs = + let t,e = find cs in + let lm = lm @ [v,t] in + let hd = f_subst_single v t hd in + add_pd kn tsk (nm ^ "_" ^ cs.ls_name.id_long) ls hd lm e + in + List.fold_left add_cs task (find_constructors kn ts) + | _ -> + add_f_ax task nm ls hd (unfold_f lm e) + end + | _ -> add_f_ax task nm ls hd (unfold_f lm e) + +let add_ld kn task ls ld = + let vl,e = open_ls_defn ld in + let tl = List.map t_var vl in + match e with + | Term t -> + add_fd kn task ls.ls_name.id_long ls (t_app ls tl t.t_ty) [] t + | Fmla f -> + add_pd kn task ls.ls_name.id_long ls (f_app ls tl) [] f + +let add_ld kn task (ls,ld) = match ld with + | None -> task + | Some ld -> add_ld kn task ls ld + +let add_ls task (ls,_) = add_decl task (create_logic_decl [ls,None]) + +let elim t task = match t.task_decl.d_node with | Dlogic ll -> - let dl = List.fold_left add_ls [] ll in - let dl = List.fold_left add_ld dl ll in - List.rev dl - | _ -> [d] + let task = List.fold_left add_ls task ll in + let task = List.fold_left (add_ld t.task_known) task ll in + task + | _ -> + add_decl task t.task_decl -let elim = Register.store (fun () -> Trans.decl elim None) +let elim = Register.store (fun () -> Trans.map elim None) let () = Driver.register_transform "eliminate_definition" elim