"eliminate_algebraic" transformation

Makefile.in

@@ -133,7 +133,7 @@ PARSER_CMO := $(addprefix src/parser/,$(PARSER_CMO))
 TRANSFORM_CMO := simplify_recursive_definition.cmo inlining.cmo\
 	split_conjunction.cmo encoding_decorate.cmo\
 	remove_logic_definition.cmo eliminate_inductive.cmo\
-	compile_match.cmo
+	compile_match.cmo eliminate_algebraic.cmo
 TRANSFORM_CMO := $(addprefix src/transform/,$(TRANSFORM_CMO))
 
 DRIVER_CMO := call_provers.cmo dynlink_compat.cmo driver_parser.cmo\

drivers/why3_total_elimination.drv

+printer "why3"
+filename "%f-%t-%s.why"
+
+transformations
+    "compile_match"
+    "eliminate_algebraic"
+end
+
+theory BuiltIn
+  syntax type   int     "int"
+  syntax type   real    "real"
+  syntax logic  (_=_)   "(%1 = %2)"
+  syntax logic  (_<>_)  "(%1 <> %2)"
+end

src/transform/eliminate_algebraic.ml

@@ -25,43 +25,80 @@ open Decl
 open Task
 
 type state = {
-  cs_map : lsymbol Mls.t;       (* from constructors to abstract functions *)
   mt_map : lsymbol Mts.t;       (* from type symbols to selector functions *)
   pj_map : lsymbol list Mls.t;  (* from constructors to projections *)
 }
 
 let empty_state = {
-  cs_map = Mls.empty;
   mt_map = Mts.empty;
   pj_map = Mls.empty;
 }
 
-let rec rewriteT state t = match t.t_node with
-  | Tcase (tl,bl) -> assert false
-(*
-      let mk_b (pl,_,t) = (pl,t) in
-      let bl = List.map (fun b -> mk_b (t_open_branch b)) bl in
-      Pattern.CompileTerm.compile (find_constructors state) tl bl
-*)
-  | _ -> t_map (rewriteT state) (rewriteF state) t
+let rec rewriteT kn state t = match t.t_node with
+  | Tcase ([t1],bl) ->
+      let mk_br (w,m) br =
+        let (pl,_,e) = t_open_branch br in
+        match pl with
+        | [{ pat_node = Papp (cs,pl) }] ->
+            let add_var e p pj = match p.pat_node with
+              | Pvar v -> t_let v (t_app pj [t1] v.vs_ty) e
+              | _ -> assert false
+            in
+            let pjl = Mls.find cs state.pj_map in
+            let e = List.fold_left2 add_var e pl pjl in
+            w, Mls.add cs e m
+        | [{ pat_node = Pwild }] ->
+            Some e, m
+        | _ -> assert false
+      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 -> of_option w in
+      let ts = match t1.t_ty.ty_node with
+        | Tyapp (ts,_) -> ts
+        | _ -> assert false
+      in
+      let tl = List.map find (find_constructors kn ts) in
+      t_app (Mts.find ts state.mt_map) (t1::tl) t.t_ty
+  | Tcase _ -> assert false
+  | _ -> t_map (rewriteT kn state) (rewriteF kn state) t
 
-and rewriteF state f = match f.f_node with
-  | Fcase (tl,bl) -> assert false
-(*
-      let mk_b (pl,_,f) = (pl,f) in
-      let bl = List.map (fun b -> mk_b (f_open_branch b)) bl in
-      Pattern.CompileFmla.compile (find_constructors state) tl bl
-*)
-  | _ -> f_map (rewriteT state) (rewriteF state) f
+and rewriteF kn state f = match f.f_node with
+  | Fcase ([t1],bl) ->
+      let mk_br (w,m) br =
+        let (pl,_,e) = f_open_branch br in
+        match pl with
+        | [{ pat_node = Papp (cs,pl) }] ->
+            let add_var e p pj = match p.pat_node with
+              | Pvar v -> f_let v (t_app pj [t1] v.vs_ty) e
+              | _ -> assert false
+            in
+            let pjl = Mls.find cs state.pj_map in
+            let e = List.fold_left2 add_var e pl pjl in
+            w, Mls.add cs e m
+        | [{ pat_node = Pwild }] ->
+            Some e, m
+        | _ -> assert false
+      in
+      let w,m = List.fold_left mk_br (None,Mls.empty) bl in
+      let find cs =
+        let arg pj = t_app_infer pj [t1] in
+        let pjl = Mls.find cs state.pj_map in
+        let hd = f_equ t1 (t_app cs (List.map arg pjl) t1.t_ty) in
+        let f  = try Mls.find cs m with Not_found -> of_option w in
+        f_implies hd f
+      in
+      let ts = match t1.t_ty.ty_node with
+        | Tyapp (ts,_) -> ts
+        | _ -> assert false
+      in
+      map_join_left find f_and (find_constructors kn ts)
+  | Fcase _ -> assert false
+  | _ -> f_map (rewriteT kn state) (rewriteF kn state) f
 
 let add_type (state, task) ts csl =
   (* declare constructors as abstract functions *)
-  let cs_add (m,tsk) cs =
-    let id = id_clone cs.ls_name in
-    let fs = create_fsymbol id cs.ls_args (of_option cs.ls_value) in
-    Mls.add cs fs m, add_decl tsk (create_logic_decl [fs, None])
-  in
-  let csmap, task = List.fold_left cs_add (state.cs_map, task) csl in
+  let cs_add tsk cs = add_decl tsk (create_logic_decl [cs, None]) in
+  let task = List.fold_left cs_add task csl in
   (* declare the selector function *)
   let mt_id = id_derive ("match_" ^ ts.ts_name.id_long) ts.ts_name in
   let mt_hd = ty_app ts (List.map ty_var ts.ts_args) in
@@ -75,11 +112,10 @@ let add_type (state, task) ts csl =
   let mt_vl = List.rev_map mt_vs csl in
   let mt_tl = List.rev_map t_var mt_vl in
   let mt_add tsk cs t =
-    let fs = Mls.find cs csmap in
     let id = mt_ls.ls_name.id_long ^ "_" ^ cs.ls_name.id_long in
     let pr = create_prsymbol (id_derive id cs.ls_name) in
-    let vl = List.rev_map (create_vsymbol (id_fresh "u")) fs.ls_args in
-    let hd = t_app fs (List.rev_map t_var vl) (of_option fs.ls_value) in
+    let vl = List.rev_map (create_vsymbol (id_fresh "u")) cs.ls_args in
+    let hd = t_app cs (List.rev_map t_var vl) (of_option cs.ls_value) in
     let hd = t_app mt_ls (hd::mt_tl) mt_ty in
     let vl = List.rev_append mt_vl (List.rev vl) in
     let ax = f_forall vl [[Term hd]] (f_equ hd t) in
@@ -88,15 +124,14 @@ let add_type (state, task) ts csl =
   let task = List.fold_left2 mt_add task csl mt_tl in
   (* declare and define the projection functions *)
   let pj_add (m,tsk) cs =
-    let fs = Mls.find cs csmap in
     let id = cs.ls_name.id_long ^ "_proj_" in
-    let vl = List.rev_map (create_vsymbol (id_fresh "u")) fs.ls_args in
+    let vl = List.rev_map (create_vsymbol (id_fresh "u")) cs.ls_args in
     let tl = List.rev_map t_var vl in
-    let hd = t_app fs tl (of_option fs.ls_value) in
+    let hd = t_app cs tl (of_option cs.ls_value) in
     let c = ref 0 in
     let add (pjl,tsk) t =
       let id = id_derive (id ^ (incr c; string_of_int !c)) cs.ls_name in
-      let ls = create_fsymbol id [of_option fs.ls_value] t.t_ty in
+      let ls = create_fsymbol id [of_option cs.ls_value] t.t_ty in
       let tsk = add_decl tsk (create_logic_decl [ls, None]) in
       let id = id_derive (ls.ls_name.id_long ^ "_def") ls.ls_name in
       let pr = create_prsymbol id in
@@ -105,7 +140,7 @@ let add_type (state, task) ts csl =
       ls::pjl, add_decl tsk (create_prop_decl Paxiom pr ax)
     in
     let pjl,tsk = List.fold_left add ([],tsk) tl in
-    Mls.add cs pjl m, tsk
+    Mls.add cs (List.rev pjl) m, tsk
   in
   let pjmap, task = List.fold_left pj_add (state.pj_map, task) csl in
   (* add the inversion axiom *)
@@ -114,15 +149,14 @@ let add_type (state, task) ts csl =
   let ax_vs = create_vsymbol (id_fresh "u") mt_hd in
   let ax_hd = t_var ax_vs in
   let mk_cs cs =
-    let fs  = Mls.find cs csmap in
     let pjl = Mls.find cs pjmap in
     let app pj = t_app_infer pj [ax_hd] in
-    f_equ ax_hd (t_app fs (List.rev_map app pjl) mt_hd)
+    f_equ ax_hd (t_app cs (List.map app pjl) mt_hd)
   in
   let ax_f = f_forall [ax_vs] [] (map_join_left mk_cs f_or csl) in
   let task = add_decl task (create_prop_decl Paxiom ax_pr ax_f) in
   (* return the updated state and task *)
-  { cs_map = csmap; mt_map = mtmap; pj_map = pjmap }, task
+  { mt_map = mtmap; pj_map = pjmap }, task
 
 let comp t (state,task) = match t.task_decl.d_node with
   | Dtype dl ->
@@ -136,8 +170,8 @@ let comp t (state,task) = match t.task_decl.d_node with
       in
       List.fold_left add (state,task) dl
   | d ->
-      let fnT = rewriteT state in
-      let fnF = rewriteF state in
+      let fnT = rewriteT t.task_known state in
+      let fnF = rewriteF t.task_known state in
       state, add_decl task (decl_map fnT fnF t.task_decl)
 
 let comp = Register.store (fun () -> Trans.fold_map comp empty_state None)