encoding_decorate can use the tag "encoding_decorate : kept"

printer : print_prelude inside printers instead of prover.ml. Required for smt which has its own prelude.

drivers/cvc3.drv

@@ -13,7 +13,7 @@ unknown "\\bunknown\\b\\|\\bsat\\b" "Unknown"
 transformation "simplify_recursive_definition"      
 (* transformation (*"split_goal_pos_neg_goal"*) "split_goal_pos_neg_all"*)
 transformation "inline_trivial"
-transformation "remove_logic_definition"
+transformation "eliminate_definition"
 transformation "encoding_decorate"
 
 theory BuiltIn
@@ -56,6 +56,10 @@ theory algebra.AC
   remove cloned prop Assoc.Assoc
 end
 
+theory transform.encoding_decorate.Kept
+  tag cloned type t "encoding_decorate : kept"
+end
+
 (*
 Local Variables: 
 mode: why

drivers/z3.drv

@@ -11,10 +11,10 @@ unknown "^\\(unknown\\|sat\\|Fail\\)" "Unknown"
 
 (* À discuter *)
 transformation "simplify_recursive_definition"      
-(*transformation (*"split_goal_pos_neg_goal"*) "split_goal_pos_neg_all"*)
 transformation "inline_trivial"
-transformation "remove_logic_definition"
+transformation "eliminate_definition"
 transformation "encoding_decorate"
+(* transformation "encoding_decorate_every_simple" *)
 
 
 theory BuiltIn
@@ -58,9 +58,13 @@ theory algebra.AC
   remove cloned prop Assoc.Assoc
 end
 
+theory transform.encoding_decorate.Kept
+  tag cloned type t "encoding_decorate : kept"
+end
+
 (*
 Local Variables: 
 mode: why
-compile-command: "make -C ../.. bench"
+compile-command: "unset LANG; make -C .. bench"
 End: 
 *)

src/core/pretty.ml

@@ -338,12 +338,12 @@ let print_decl fmt d = match d.d_node with
   | Dind il   -> print_list newline print_ind_decl fmt il
   | Dprop p   -> print_prop_decl fmt p
 
-let print_tdecl fmt = function
-  | Decl d ->
+let print_task_tdecl fmt = function
+  | Task.Decl d ->
       print_decl fmt d
-  | Use th ->
+  | Task.Use th ->
       fprintf fmt "@[<hov 2>(* use %a *)@]" print_th th
-  | Clone (th,inst) ->
+  | Task.Clone (th,inst) ->
       fprintf fmt "@[<hov 2>(* clone %a with %a *)@]"
         print_th th (print_list comma print_inst) inst
 
@@ -353,7 +353,7 @@ let print_task fmt task =
 
 let print_named_task fmt name task =
   fprintf fmt "@[<hov 2>task %s@\n%a@]@\nend@."
-    name (print_list newline2 print_tdecl) (task_tdecls task)
+    name (print_list newline2 print_task_tdecl) (task_tdecls task)
 
 let print_th_tdecl fmt = function
   | Theory.Decl d ->

src/core/pretty.mli

@@ -54,6 +54,7 @@ val print_ind_decl : formatter -> ind_decl -> unit
 val print_prop_decl : formatter -> prop_decl -> unit
 
 val print_decl : formatter -> decl -> unit
+val print_task_tdecl : formatter -> Task.tdecl -> unit
 val print_task : formatter -> task -> unit
 val print_theory : formatter -> theory -> unit
 

src/core/task.ml

@@ -42,6 +42,8 @@ and tdecl =
   | Use   of theory
   | Clone of theory * (ident * ident) list
 
+let create_decl d = Decl d
+
 let task_known = option_apply Mid.empty (fun t -> t.task_known)
 let task_clone = option_apply Mid.empty (fun t -> t.task_clone)
 let task_used  = option_apply Mid.empty (fun t -> t.task_used)

src/core/task.mli

@@ -41,6 +41,8 @@ and tdecl = private
   | Use   of theory
   | Clone of theory * (ident * ident) list
 
+val create_decl : decl -> tdecl
+
 val task_known : task -> known_map
 val task_clone : task -> clone_map
 val task_used  : task -> use_map

src/core/trans.ml

@@ -99,6 +99,23 @@ let decl_l fn =
   in
   map_l fn
 
+
+let tdecl fn =
+  let fn = WHdecl.memoize 63 fn in
+  let fn task acc = match task.task_decl with
+    | Decl d -> List.fold_left add_tdecl acc (fn d)
+    | td -> add_tdecl acc td
+  in
+  map fn
+
+let tdecl_l fn =
+  let fn = WHdecl.memoize 63 fn in
+  let fn task acc = match task.task_decl with
+    | Decl d -> List.rev_map (List.fold_left add_tdecl acc) (fn d)
+    | td -> [add_tdecl acc td]
+  in
+  map_l fn
+
 let rewrite fnT fnF = decl (fun d -> [decl_map fnT fnF d])
 
 (** exception to use in a transformation *)

src/core/trans.mli

@@ -55,6 +55,9 @@ val map_l : (task_hd -> task -> task list) -> task -> task tlist
 val decl   : (decl -> decl list     ) -> task -> task trans
 val decl_l : (decl -> decl list list) -> task -> task tlist
 
+val tdecl   : (decl -> tdecl list     ) -> task -> task trans
+val tdecl_l : (decl -> tdecl list list) -> task -> task tlist
+
 val rewrite : (term -> term) -> (fmla -> fmla) -> task -> task trans
 
 (** exception to use in a transformation *)

src/driver/prover.ml

@@ -63,7 +63,6 @@ let print_task drv fmt task =
   let apply task tr = Register.apply_driver tr drv task in
   let task = List.fold_left apply task transl in
   let printer = printer (driver_query drv task) in
-  print_prelude drv task fmt;
   fprintf fmt "@[%a@]@?" printer task
 
 let prove_task ?debug ~command ~timelimit ~memlimit drv task =

src/printer/alt_ergo.ml

@@ -129,7 +129,8 @@ let rec print_fmla drv fmt f = match f.f_node with
 and print_expr drv fmt = e_apply (print_term drv fmt) (print_fmla drv fmt)
 
 and print_triggers drv fmt tl =
-  let tl = List.map (List.filter (function Term _ -> true | Fmla _ -> false)) tl in
+  let tl = List.map (List.filter (function Term _ -> true | Fmla _ -> false))
+    tl in
   let tl = List.filter (function [] -> false | _::_ -> true) tl in
   if tl = [] then () else fprintf fmt "@ [%a]"
     (print_list alt (print_list comma (print_expr drv))) tl
@@ -207,6 +208,7 @@ let () = Register.register_printer "alt-ergo"
      print_task drv fmt task)
 
 let print_goal drv fmt (id, f, task) =
+  Driver.print_prelude (Driver.query_driver drv) task fmt;
   print_task drv fmt task;
   fprintf fmt "@\n@[<hov 2>goal %a : %a@]@\n" print_ident id (print_fmla drv) f
 

src/printer/coq.ml

@@ -327,6 +327,7 @@ let print_decls drv fmt dl =
 
 let print_task drv fmt task =
   forget_all ();
+  Driver.print_prelude (Driver.query_driver drv) task fmt;
   print_decls drv fmt (Task.task_decls task)
 
 let () = Register.register_printer "coq" print_task

src/printer/smt.ml

@@ -191,6 +191,7 @@ let print_task drv fmt task =
   fprintf fmt "(benchmark toto@\n" 
     (*print_ident (Task.task_goal task).pr_name*);
   fprintf fmt "  :status unknown@\n";
+  Driver.print_prelude (Driver.query_driver drv) task fmt;
   let decls = Task.task_decls task in
   ignore (print_list_opt (add_flush newline2) (print_decl drv) fmt decls);
   fprintf fmt "@\n)@."

src/printer/why3.ml

@@ -328,7 +328,9 @@ let print_decls drv fmt dl =
   fprintf fmt "@[<hov>%a@\n@]" (print_list nothing (print_decl drv)) dl
 
 let print_task drv fmt task =
-  forget_all (); print_decls drv fmt (Task.task_decls task)
+  forget_all (); 
+  Driver.print_prelude (Driver.query_driver drv) task fmt;
+  print_decls drv fmt (Task.task_decls task)
 
 let () = Register.register_printer "why3" print_task
 

src/transform/encoding_decorate.ml

@@ -17,11 +17,13 @@
 (*                                                                        *)
 (**************************************************************************)
 
+open Util
 open Ident
 open Ty
 open Term
 open Task
 open Theory
+open Task
 open Decl
 
 let why_filename = ["transform" ; "encoding_decorate"]
@@ -53,7 +55,9 @@ type lconv = {d2t : lsymbol;
               t2u : lsymbol;
               tty : term}
 
-type tenv = {specials : lconv Mty.t;
+type tenv = {query : Driver.driver_query option;
+             clone_builtin : tysymbol -> Task.tdecl list;
+             specials : lconv Hty.t;
              deco : ty;
              undeco : ty;
              sort : lsymbol;
@@ -64,8 +68,7 @@ type tenv = {specials : lconv Mty.t;
        comme specials_type ne depend pas*)
     
 
-let load_prelude env =
-  let specials_type = [ts_int;ts_real] in
+let load_prelude query env =
   let prelude = Env.find_theory env why_filename "Prelude" in
   let sort = Theory.ns_find_ls prelude.th_export ["sort"] in
   let tyty = ty_app (Theory.ns_find_ts prelude.th_export ["ty"]) [] in
@@ -73,20 +76,24 @@ let load_prelude env =
   let undeco = ty_app (Theory.ns_find_ts prelude.th_export ["undeco"]) [] in
   let task = None in
   let task = Task.use_export task prelude in
+  let trans_tsymbol = Hts.create 17 in
+  let specials = Hty.create 17 in
   let builtin = Env.find_theory env why_filename "Builtin" in
   let type_t = Theory.ns_find_ts builtin.th_export ["t"] in
   let logic_d2t = Theory.ns_find_ls builtin.th_export ["d2t"] in
   let logic_t2u = Theory.ns_find_ls builtin.th_export ["t2u"] in
   let logic_tty = Theory.ns_find_ls builtin.th_export ["tty"] in
-  let trans_tsymbol = Hts.create 17 in
-  let clone_builtin (task,spmap) ts =
+  let clone_builtin ts =
+    let task = None in
     let name = ts.ts_name.id_short in
     let th_uc = create_theory (id_fresh ("encoding_decorate_for_"^name)) in
-    let th_uc = use_export th_uc prelude in
-    let ty = (ty_app ts []) in
-    let add_fsymbol fs task =
-      let decl = create_logic_decl [fs,None] in
-      add_decl task decl in
+    let th_uc = Theory.use_export th_uc prelude in
+    let th_uc = 
+      if ts == ts_int || ts = ts_real then th_uc
+      else Theory.add_ty_decl th_uc [ts,Tabstract] in
+    let ty = ty_app ts [] in
+    let add_fsymbol fs th_uc =
+      Theory.add_logic_decl th_uc [fs,None] in
     let tty = create_fsymbol (id_clone ts.ts_name) [] tyty in
     let d2ty = create_fsymbol (id_fresh ("d2"^name)) [deco]  ty in
     let ty2u = create_fsymbol (id_fresh (name^"2u")) [ty] undeco in
@@ -100,12 +107,12 @@ let load_prelude env =
     let th = close_theory th_uc in
     let task = Task.use_export task th in
     Hts.add trans_tsymbol ts tty;
-      task,Mty.add (ty_app ts []) lconv spmap
-  in
-  let task,specials = 
-    List.fold_left clone_builtin (task,Mty.empty) specials_type in
+    Hty.add specials (ty_app ts []) lconv;
+    task_tdecls task in
   task,
-  { specials = specials;
+  { query = query;
+    clone_builtin = clone_builtin;
+    specials = specials;
     deco = deco;
     undeco = undeco;
     ty = tyty;
@@ -113,6 +120,16 @@ let load_prelude env =
     trans_lsymbol = Hls.create 17;
     trans_tsymbol = trans_tsymbol}
 
+let is_kept tenv ts = 
+  ts.ts_args = [] &&  
+    begin
+      ts == ts_int || ts == ts_real  (* for the constant *)
+      || match tenv.query with
+        | None -> true (* every_simple *)
+        | Some query ->
+            let tags = Driver.query_tags query ts.ts_name in
+            Sstr.mem "encoding_decorate : kept" tags
+    end
 
 (* Translate a type to a term *)
 let rec term_of_ty tenv tvar ty =
@@ -134,14 +151,14 @@ let sort_app tenv tvar t ty =
 
 (* Convert a type at the right of an arrow *)
 let conv_ty_neg tenv ty =
-  if Mty.mem ty tenv.specials then
+  if Hty.mem tenv.specials ty then
     ty
   else
     tenv.deco
 
 (* Convert a type at the left of an arrow *)
 let conv_ty_pos tenv ty =
-  if Mty.mem ty tenv.specials then
+  if Hty.mem tenv.specials ty then
     ty
   else
     tenv.undeco
@@ -172,13 +189,13 @@ let conv_arg tenv tvar t ty =
   let tty = t.t_ty in
   if tty == ty then t else
     if ty == tenv.deco then
-      let tylconv = Mty.find tty tenv.specials in
+      let tylconv = Hty.find tenv.specials tty in
       let t = (t_app tylconv.t2u [t] tenv.undeco) in
       sort_app tenv tvar t tty
     else (* tty is tenv.deco *)
       begin
         assert (tty == tenv.deco);
-        let tylconv = Mty.find ty tenv.specials in       
+        let tylconv = Hty.find tenv.specials ty in       
         t_app tylconv.d2t [t] ty
       end
 
@@ -220,10 +237,10 @@ and rewrite_fmla tenv tvar vsvar f =
         let tl = List.map fnT tl in
         begin
           match tl with
-            | [a1;a2] ->
+            | [a1;_] ->
                 let ty = 
-                  if a1.t_ty == ty_int || a2.t_ty == ty_int 
-                  then ty_int 
+                  if Hty.mem tenv.specials a1.t_ty
+                  then a1.t_ty
                   else tenv.deco in
                 let tl = List.map2 (conv_arg tenv tvar) tl [ty;ty] in
                 f_app p tl
@@ -259,6 +276,8 @@ let decl (tenv:tenv) d =
   (* let fnT = rewrite_term tenv in *)
   let fnF = rewrite_fmla tenv in
   match d.d_node with
+    | Dtype [ts,Tabstract] when is_kept tenv ts -> 
+        tenv.clone_builtin ts
     | Dtype [ts,Tabstract] -> 
         let tty = 
           try 
@@ -267,7 +286,7 @@ let decl (tenv:tenv) d =
             let tty = conv_ts tenv ts in
             Hts.add tenv.trans_tsymbol ts tty;
             tty in
-        [create_logic_decl [(tty,None)]]
+        [create_decl (create_logic_decl [(tty,None)])]
     | Dtype _ -> Trans.unsupportedDeclaration 
         d "encoding_decorate : I can work only on abstract\
             type which are not in recursive bloc."
@@ -285,7 +304,7 @@ Perhaps you could use eliminate_definition"
                 let ls_conv = conv_ls tenv ls in
                 Hls.add tenv.trans_lsymbol ls ls_conv;
                 ls_conv,None in
-        [create_logic_decl (List.map fn l)]
+        [create_decl (create_logic_decl (List.map fn l))]
     | Dind _ -> Trans.unsupportedDeclaration
         d "encoding_decorate : I can't work on inductive"
         (* let fn (pr,f) = pr, fnF f in *)
@@ -296,19 +315,29 @@ Perhaps you could use eliminate_definition"
         let f = fnF tvar Mvs.empty f in
         let tvl = Htv.fold (fun _ tv acc -> tv::acc) tvar [] in
         let f = f_forall tvl [] f in
-        [create_prop_decl k pr f]
+        [create_decl (create_prop_decl k pr f)]
 
 (*
 let decl tenv d =
-  Format.printf "@[<hov 2>Decl : %a =>@\n" Pretty.print_decl d;
+  Format.eprintf "@[<hov 2>Decl : %a =>@\n" Pretty.print_decl d;
   let res = decl tenv d in
-  Format.printf "%a@]@." (Pp.print_list Pp.newline Pretty.print_decl) res;
+  Format.eprintf "%a@]@." (Pp.print_list Pp.newline Pretty.print_task_tdecl)
+    res;
   res
 *)
 
-let t = Register.store_env 
-  (fun env -> 
-     let init_task,tenv = load_prelude env in
-     Trans.decl (decl tenv) init_task)
+let t = Register.store_query 
+  (fun query -> 
+     let env = Driver.query_env query in
+     let init_task,tenv = load_prelude (Some query) env in
+     Trans.tdecl (decl tenv) init_task)
 
 let () = Register.register_transform "encoding_decorate" t
+
+
+let t_all = Register.store_env 
+  (fun env -> 
+     let init_task,tenv = load_prelude None env in
+     Trans.tdecl (decl tenv) init_task)
+
+let () = Register.register_transform "encoding_decorate_every_simple" t_all

tests/test-bobot.why

+
+(* test file *)
+
+theory Test_encoding
+  use import int.Int
+  logic id(x: int) : int = x
+  logic id2(x: int) : int = id(x)
+  logic succ(x:int) : int = id(x+1)
+
+  type myt
+  logic f (int) : myt
+  clone transform.encoding_decorate.Kept with type t = myt
+
+  goal G : (forall x:int.f(x)=f(x)) or
+    (forall x:int. x=x+1)
+  goal G2 : forall x:int. let x = 0 + 1 in x = 1
+end
+
+theory Test_simplify_array
+  use import array.Array
+  goal G : forall x,y:int. forall m: (int,int) t. 
+    select(store(m,y,x),y) = x
+end 
+
+theory Test_conjunction
+  use import int.Int
+  goal G : 
+    forall x:int. x*x=4 -> ((x*x*x=8 or x*x*x = -8) and x*x*2 = 8)
+  goal G2 : 
+    forall x:int. 
+    (x+x=4 or x*x=4) -> ((x*x*x=8 or x*x*x = -8) and x*x*2 = 8)
+end
+
+theory Split_conj
+  logic p(x:int)
+    (*goal G : forall x,y,z:int. ((p(x) -> p(y)) and ((not p(x)) -> p(z))) -> ((p(x) and p(y)) or ((not p(x)) and p(z)))*)
+    (*goal G : forall x,y,z:int. (if p(x) then p(y) else p(z)) <-> ((p(x) and p(y)) or ((not p(x)) and p(z)))*)
+    (*goal G : forall x,y,z:int. (if p(x) then p(y) else p(z)) -> (if p(x) then p(y) else p(z))*)
+  goal G : forall x,y,z:int. (p(x) <-> p(z)) -> (p(x) <-> p(z))
+    (*goal G : forall x,y,z:int. (p(z) <-> p(x)) -> (((not p(z)) and (not p(x))  or  ((p(z)) and (p(x))))) *)
+    (*goal G : forall x,y,z:int. (p(x) or p(y)) -> p(z)*)
+end
+
+
+
+
+theory TestEnco
+  use import int.Int
+  type 'a mytype
+  logic id(x: int) : int = x
+  logic id2(x: int) : int = id(x)
+  logic succ(x:int) : int = id(x+1)
+
+  goal G : (forall x:int. x=x) or
+    (forall x:int. x=x+1)
+  logic p('a ) : 'a mytype
+  logic p2('a mytype) : 'a
+  type toto
+  logic f (toto) : toto mytype
+  logic g (int mytype) : toto
+  logic h (int) : toto mytype
+  axiom A1 : forall x : 'a mytype. p(p2(x)) = x
+  goal G2 : forall x:int. f(g(p(x))) = h(x)
+
+
+end
+
+
+
+(*
+Local Variables: 
+compile-command: "make -C .. test"
+End: 
+*)
+

theories/transform/encoding_decorate.why

@@ -13,3 +13,8 @@ theory Builtin
        logic t2u(t) : undeco
        axiom Conv : forall x:t[t2u(x)]. d2t(sort(tty,t2u(x)))=x
 end
+
+theory Kept
+(* If a driver tags this type by "encoding decorate : kept", all the type which clone this one will be kept by the encoding*)
+       type t
+end
\ No newline at end of file