fix some bugs in Libencoding and update explicit_polymorphism

Makefile.in

@@ -108,11 +108,11 @@ LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
 	     whyconf
 
 LIB_TRANSFORM = simplify_recursive_definition simplify_formula inlining \
-		split_conjunction libencoding \
+		split_conjunction \
 		eliminate_definition eliminate_algebraic \
 		eliminate_inductive eliminate_let eliminate_if \
 		encoding_enumeration encoding encoding_decorate_mono \
-		encoding_decorate encoding_bridge \
+		libencoding encoding_decorate encoding_bridge \
 		explicit_polymorphism encoding_simple encoding_simple2 encoding_instantiate \
 		simplify_array filter_trigger split_goal
 

src/transform/encoding_bridge.ml

@@ -87,7 +87,7 @@ let load_prelude kept env =
       (if is_constant then None else Some (ty_of_ty tenv_tmp ty)) in
     let task = add_ts task tb in
     let tytb = ty_app tb [] in 
-    let tb2t = create_fsymbol (id_clone logic_t2tb.ls_name) [tytb] ty in
+    let tb2t = create_fsymbol (id_clone logic_tb2t.ls_name) [tytb] ty in
     let t2tb = create_fsymbol (id_clone logic_t2tb.ls_name) [ty] tytb in
     let task = add_logic_decl task [tb2t,None] in
     let task = add_logic_decl task [t2tb,None] in

src/transform/encoding_simple.ml

@@ -75,7 +75,7 @@ let init_tenv kept =
     trans_lsymbol = Hls.create 17 }
 
 let is_kept tenv ts =
-  ts_equal ts Explicit_polymorphism.ts_ty ||
+  ts_equal ts Libencoding.ts_type ||
   ts.ts_args = [] && match tenv.kept with
   | Some s -> Sts.mem ts s
   | None   -> true

src/transform/explicit_polymorphism.ml

@@ -27,11 +27,7 @@ open Ty
 open Term
 open Decl
 open Task
-
-(** type representing types *)
-let ts_ty = Ty.create_tysymbol (id_fresh "ty") [] None
-let my_t = ty_app ts_ty []
-let t_decl = Decl.create_ty_decl [ts_ty, Tabstract]
+open Libencoding
 
 (** module with printing functions *)
 module Debug = struct
@@ -53,162 +49,123 @@ end
 
 module Transform = struct
 
-  (** {1 memoization facilities} *)
-
-  (** [find construct tbl id] searches for the object associated with
-  [id] in [tbl]. It creates it with [construct id] if it cannot find it. *)
-  let find_generic construct tbl id =
-    try Hashtbl.find tbl id
-    with Not_found ->
-      let new_image = construct id in
-      Hashtbl.add tbl id new_image;
-      new_image
-
   (** creates a new logic symbol, with a different type if the
   given symbol was polymorphic *)
-  let logic_to_logic lsymbol =
+  let findL = Wls.memoize 63 (fun lsymbol ->
     if ls_equal lsymbol ps_equ then lsymbol else
     let new_ty = ls_ty_freevars lsymbol in
     (* as many t as type vars *)
     if Stv.is_empty new_ty then lsymbol (* same type *) else
-      let add _ acc = my_t :: acc in
+      let add _ acc = ty_type :: acc in
       let args = Stv.fold add new_ty lsymbol.ls_args in
       (* creates a new lsymbol with the same name but a different type *)
-      Term.create_lsymbol (id_clone lsymbol.ls_name) args lsymbol.ls_value
-
-  (** creates a lsymbol associated with the given tysymbol *)
-  let type_to_logic ty =
-    let name = id_clone ty.ts_name in
-    let args = (List.map (const my_t) ty.ts_args) in
-    Term.create_fsymbol name args my_t
-
-  (** different finders for logic and type declarations *)
-
-  let findL tbl x = find_generic logic_to_logic tbl x
-  let findT tbl x = find_generic type_to_logic tbl x
+      Term.create_lsymbol (id_clone lsymbol.ls_name) args lsymbol.ls_value)
 
   (** {1 transformations} *)
 
-  (** transforms a type into a term (new args of polymorphic symbols).
-      [tblT] is a hashtable used to associate types and symbols
-      [varM] is a Map used to associate some type vars and symbols *)
-  let rec ty_to_term tblT varM ty = match ty.ty_node with
-    | Tyvar v ->
-      assert (Mtv.mem v varM);
-      t_var (Mtv.find v varM)
-    | Tyapp(typ, tys) ->
-      assert (Hashtbl.mem tblT typ); (* nonsense otherwise *)
-      let lsymbol = Hashtbl.find tblT typ in
-      let terms = List.map (ty_to_term tblT varM) tys in
-      t_app lsymbol terms my_t
-
   (** translation of terms *)
-  let rec term_transform tblT tblL varM t = match t.t_node with
+  let rec term_transform varM t = match t.t_node with
     | Tapp(f, terms) ->
-      let terms = args_transform tblT tblL varM f terms (Some t.t_ty) in
-      t_app (findL tblL f) terms t.t_ty
+      let terms = args_transform varM f terms (Some t.t_ty) in
+      t_app (findL f) terms t.t_ty
     | _ -> (* default case : traverse *)
-      t_map (term_transform tblT tblL varM) (fmla_transform tblT tblL varM) t
+      t_map (term_transform varM) (fmla_transform varM) t
 
   (** translation of formulae *)
-  and fmla_transform tblT tblL varM f = match f.f_node with
+  and fmla_transform varM f = match f.f_node with
       (* first case : predicate (not =), we must translate it and its args *)
     | Fapp(p,terms) when not (ls_equal p ps_equ) ->
-      let terms = args_transform tblT tblL varM p terms None in
-      f_app (findL tblL p) terms
+      let terms = args_transform varM p terms None in
+      f_app (findL p) terms
     | _ -> (* otherwise : just traverse and translate *)
-      f_map (term_transform tblT tblL varM) (fmla_transform tblT tblL varM) f
+      f_map (term_transform varM) (fmla_transform varM) f
 
-  and args_transform tblT tblL varM ls args ty =
+  and args_transform varM ls args ty =
     (* Debug.print_list Pretty.print_ty Format.std_formatter type_vars; *)
     let tv_to_ty = ls_app_inst ls args ty in
     (* Debug.print_mtv Pretty.print_ty Format.err_formatter tv_to_ty; *)
-    let args = List.map (term_transform tblT tblL varM) args in
+    let args = List.map (term_transform varM) args in
     (* fresh args to be added at the beginning of the list of arguments *)
-    let add _ ty acc = ty_to_term tblT varM ty :: acc in
+    let add _ ty acc = term_of_ty varM ty :: acc in
     Mtv.fold add tv_to_ty args
 
   (** transforms a list of logic declarations into another.
-  Declares new lsymbols with explicit polymorphic signatures.
-  @param tblT binds type symbols to logic symbols
-  @param tblL hashtable used to memoize new lsymbols *)
-  let logic_transform tblT tblL decls =
+  Declares new lsymbols with explicit polymorphic signatures. *)
+  let logic_transform decls =
     (* if there is a definition, we must take it into account *)
     let helper = function
     | (lsymbol, Some ldef) ->
-      let new_lsymbol = findL tblL lsymbol in (* new lsymbol *)
+      let new_lsymbol = findL lsymbol in (* new lsymbol *)
       let vars,expr = open_ls_defn ldef in
       let add v (vl,vm) =
-        let vs = Term.create_vsymbol (id_fresh "t") my_t in
+        let vs = Term.create_vsymbol (id_fresh "t") ty_type in
         vs :: vl, Mtv.add v vs vm
       in
       let vars,varM = Stv.fold add (ls_ty_freevars lsymbol) (vars,Mtv.empty) in
       (match expr with
       | Term t ->
-          let t = term_transform tblT tblL varM t in
+          let t = term_transform varM t in
           Decl.make_fs_defn new_lsymbol vars t
       | Fmla f ->
-          let f = fmla_transform tblT tblL varM f in
+          let f = fmla_transform varM f in
           Decl.make_ps_defn new_lsymbol vars f)
     | (lsymbol, None) ->
-      let new_lsymbol = findL tblL lsymbol in
-      (new_lsymbol, None) in
-    let cur_decl = List.map helper decls
-    in [Decl.create_logic_decl cur_decl]
-
-  (** transforms a list of type declarations *)
-  let type_transform tblT tys =
-    let helper acc = function
-      | (ty_symbol, _) when ty_symbol.ts_def <> None -> acc
-      | (ty_symbol, Tabstract) -> (findT tblT ty_symbol, None) :: acc
-      | _ -> failwith "type_transform : no algebraic type should remain !" in
-    let cur_decl = List.fold_left helper [] tys in
-    Decl.create_ty_decl tys :: Decl.create_logic_decls cur_decl
+      (findL lsymbol, None)
+    in
+    [Decl.create_logic_decl (List.map helper decls)]
 
-  (** transforms a proposition into another (mostly a substitution) *)
-  let prop_transform tblT tblL (prop_kind, prop_name, fmla) =
+  (** transforms a closed formula *)
+  let sentence_transform fmla =
     let type_vars = f_ty_freevars Stv.empty fmla in
     let varM = Stv.fold (* create a vsymbol for each type var *)
-      (fun x m -> Mtv.add x (create_vsymbol (id_fresh "t") my_t) m)
+      (fun x m -> Mtv.add x (create_vsymbol (id_fresh "t") ty_type) m)
       type_vars Mtv.empty in
     (* Debug.print_mtv Pretty.print_vs Format.err_formatter varM;
     Format.eprintf "-----------@."; *)
     (*universal quantification over ty vars*)
-    let new_fmla = (fmla_transform tblT tblL varM fmla) in
+    let new_fmla = fmla_transform varM fmla in
     let vars = Mtv.fold (fun _ value acc -> value::acc) varM [] in
-    let quantified_fmla = f_forall_close vars [] new_fmla in
+    f_forall_close vars [] new_fmla
+
+  (** transform an inductive declaration *)
+  let ind_transform idl =
+    let iconv (pr,f) = pr, sentence_transform f in
+    let conv (ls,il) = findL ls, List.map iconv il in
+    [Decl.create_ind_decl (List.map conv idl)]
+
+  (** transforms a proposition into another (mostly a substitution) *)
+  let prop_transform (prop_kind, prop_name, fmla) =
+    let quantified_fmla = sentence_transform fmla in
     [Decl.create_prop_decl prop_kind prop_name quantified_fmla]
 
 end
 
 (** {2 main part} *)
 
-(** main function, takes hashtables (for memoization of types and logic
-    symbols) and a declaration, and returns the corresponding declaration in
-    explicit polymorphism logic.
-    It is to be applied on every declarations of the task. *)
-let decl_transform tblT tblL d =
-  (*Format.eprintf "%a@." Pretty.print_decl d;*)
-  let result = match d.d_node with
-    | Dind _ ->
-      failwith "Dind : should not have inductive declarations at this point!"
-    | Dtype tys -> Transform.type_transform tblT tys
-    | Dlogic decls -> Transform.logic_transform tblT tblL decls
-    | Dprop prop -> Transform.prop_transform tblT tblL prop in
-  (*Format.eprintf "===@.%a@.@." (Debug.print_list Pretty.print_decl) result;*)
-  result
-
-
-(** the transformation to be registered.
-    It creates two new hashtables, used everywhere, which updates are
-    shared by side effects. *)
-let explicit_polymorphism =
-  let prelude_task = Task.add_decl None t_decl in (* declare t first *)
-  Trans.decl
-      (decl_transform (Hashtbl.create 21) (Hashtbl.create 42)) prelude_task
-
-
-let () = Trans.register_transform "explicit_polymorphism" explicit_polymorphism
-let () = 
-  Encoding.register_enco_poly "explicit" (fun _ -> explicit_polymorphism)
+let decl d = match d.d_node with
+  | Dtype tdl -> d :: Libencoding.lsdecl_of_tydecl tdl
+  | Dlogic ldl -> Transform.logic_transform ldl
+  | Dind idl -> Transform.ind_transform idl
+  | Dprop prop -> Transform.prop_transform prop
+
+let explicit = Trans.decl decl (Task.add_decl None d_ts_type)
+
+(** {2 monomorphise task } *)
+
+let lsmap kept = Wls.memoize 63 (fun ls ->
+  let tymap ty =
+    if Sty.mem ty kept then ty else Libencoding.ty_base in
+  let ty_res = Util.option_map tymap ls.ls_value in
+  let ty_arg = List.map tymap ls.ls_args in
+  if Util.option_eq ty_equal ty_res ls.ls_value &&
+     List.for_all2 ty_equal ty_arg ls.ls_args then ls
+  else create_lsymbol (id_clone ls.ls_name) ty_arg ty_res)
+
+let monomorph = Trans.on_meta Encoding.meta_kept (fun tds ->
+  let kept = Libencoding.get_kept_types tds in
+  let decl = Libencoding.d_monomorph kept (lsmap kept) in
+  Trans.decl decl (Task.add_decl None d_ts_base))
+
+let () = Encoding.register_enco_poly "explicit"
+    (fun _ -> Trans.compose explicit monomorph)
 

src/transform/explicit_polymorphism.mli

@@ -17,12 +17,3 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(** type of types *)
-
-val ts_ty : Ty.tysymbol
-
-(** transformation from polymorphic logic to untyped logic. The polymorphic
-logic must not have finite support types. *)
-
-val explicit_polymorphism : Task.task Trans.trans
-

src/transform/libencoding.ml

@@ -76,7 +76,9 @@ let ls_of_const =
     | Tconst _ ->
         begin try Hterm.find ht t with Not_found ->
           let s = Pp.string_of Pretty.print_term t in
-          create_fsymbol (id_fresh ("const_" ^ s)) [] ty_base
+          let ls = create_fsymbol (id_fresh ("const_" ^ s)) [] ty_base in
+          Hterm.add ht t ls;
+          ls
         end
     | _ -> assert false
   in
@@ -85,19 +87,20 @@ let ls_of_const =
 (* convert a constant to a term of type ty_base *)
 let term_of_const c = t_app (ls_of_const c) [] ty_base
 
-(* convert a set of preserved tysymbols to a set of types *)
-let tyset_of_tsset kept =
+(* convert tysymbols tagged with meta_kept to a set of types *)
+let get_kept_types tds =
+  let tss = Task.find_tagged_ts Encoding.meta_kept tds Sts.empty in
   let add ts acc = match ts.ts_def with
     | Some ty -> Sty.add ty acc
     | None -> Sty.add (ty_app ts []) acc
   in
-  Sts.fold add kept Sty.empty
+  Sts.fold add tss (Sty.singleton ty_type)
 
 (* monomorphise modulo the set of kept types * and an lsymbol map *)
 
 let vs_monomorph kept vs =
-  if ty_equal vs.vs_ty ty_type || Sty.mem vs.vs_ty kept
-  then vs else create_vsymbol (id_clone vs.vs_name) ty_base
+  if Sty.mem vs.vs_ty kept then vs else
+  create_vsymbol (id_clone vs.vs_name) ty_base
 
 let rec t_monomorph kept lsmap consts vmap t =
   let t_mono = t_monomorph kept lsmap consts in
@@ -107,6 +110,8 @@ let rec t_monomorph kept lsmap consts vmap t =
         assert false
     | Tvar v ->
         Mvs.find v vmap
+    | Tconst _ when Sty.mem t.t_ty kept ->
+        t
     | Tconst c ->
         let ls = ls_of_const c in
         consts := Sls.add ls !consts;
@@ -171,7 +176,7 @@ let d_monomorph kept lsmap d =
           | _, Talgebraic _ ->
               Printer.unsupportedDecl d "no algebraic types at this point"
           | { ts_def = Some _ }, _ -> acc
-          | ts, _ when Sty.exists (ty_s_any (ts_equal ts)) kept -> acc
+          | ts, _ when not (Sty.exists (ty_s_any (ts_equal ts)) kept) -> acc
           | _ -> create_ty_decl [td] :: acc
         in
         List.fold_right add tdl []

src/transform/libencoding.mli

@@ -57,9 +57,9 @@ val ls_of_const : constant -> lsymbol
 (* convert a constant to a term of type ty_base *)
 val term_of_const : constant -> term
 
-(* convert a set of preserved tysymbols to a set of types *)
-val tyset_of_tsset : Sts.t -> Sty.t
-
 (* monomorphise modulo the set of kept types * and an lsymbol map *)
 val d_monomorph : Sty.t -> (lsymbol -> lsymbol) -> decl -> decl list
 
+(* convert tysymbols tagged with meta_kept to a set of types *)
+val get_kept_types : Task.tdecl_set -> Sty.t
+