bring simplify back to the realm of consistency

drivers/simplify.drv

@@ -27,7 +27,7 @@ transformation "remove_triggers"
 trigger they can't appear since = can't appear *)
 (*transformation "filter_trigger_builtin"*)
 
-(* transformation "encoding_tptp" *)
+transformation "encoding_tptp"
 
 theory BuiltIn
   syntax logic (=)  "(EQ %1 %2)"
@@ -63,6 +63,12 @@ theory int.Int
   remove prop Antisymm
   remove prop Total
 
+  (* use with explicit polymorphism *)
+  meta "encoding : base" type int
+
+  (* use with encoding_decorate *)
+  (* meta "encoding : kept" type int *)
+
 end
 
 (*

src/transform/encoding.ml

@@ -23,6 +23,7 @@ open Task
 open Trans
 
 let meta_kept = register_meta "encoding : kept" [MTtysymbol]
+let meta_base = register_meta_excl "encoding : base" [MTtysymbol]
 
 type enco_opt =
     { meta : meta;

src/transform/encoding.mli

@@ -23,6 +23,7 @@ open Task
 open Trans
 
 val meta_kept : meta
+val meta_base : meta
 
 val register_enco_select : string -> (env -> task trans) -> unit
 val register_enco_kept : string -> (env -> task trans) -> unit

src/transform/encoding_decorate.ml

@@ -75,6 +75,9 @@ let deco kept = Trans.decl (deco_decl kept) deco_init
 
 (** Monomorphisation *)
 
+let ts_base = create_tysymbol (id_fresh "uni") [] None
+let ty_base = ty_app ts_base []
+
 let ts_deco = create_tysymbol (id_fresh "deco") [] None
 let ty_deco = ty_app ts_deco []
 let ls_deco = create_fsymbol (id_fresh "sort") [ty_type;ty_base] ty_deco
@@ -90,6 +93,7 @@ let lsmap kept = Wls.memoize 63 (fun ls ->
      && List.for_all2 ty_equal tyl ls.ls_args then ls
   else create_lsymbol (id_clone ls.ls_name) tyl tyr)
 
+let d_ts_base = create_ty_decl [ts_base, Tabstract]
 let d_ts_deco = create_ty_decl [ts_deco, Tabstract]
 
 let mono_init =
@@ -97,7 +101,8 @@ let mono_init =
   let init = Task.add_decl init d_ts_deco in
   init
 
-let mono kept = Trans.decl (d_monomorph kept (lsmap kept)) mono_init
+let mono kept =
+  Trans.decl (d_monomorph ty_base kept (lsmap kept)) mono_init
 
 let t = Trans.on_meta Encoding.meta_kept (fun tds ->
   let kept = Libencoding.get_kept_types tds in

src/transform/encoding_explicit.ml

@@ -139,20 +139,39 @@ 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 ts_base = create_tysymbol (id_fresh "uni") [] None
+let ty_base = ty_app ts_base []
+
+let lsmap tyb kept = Wls.memoize 63 (fun ls ->
+  let tymap ty = if Sty.mem ty kept then ty else tyb 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 d_ts_base = create_ty_decl [ts_base, Tabstract]
+
+let monomorph tyb = 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
+  let tyb = match tyb.ty_node with
+    | Tyapp (_,[]) when not (Sty.mem tyb kept) -> tyb
+    | _ -> ty_base
+  in
+  let decl = Libencoding.d_monomorph tyb kept (lsmap tyb kept) in
   Trans.decl decl (Task.add_decl None d_ts_base))
 
+let monomorph = Trans.on_meta Encoding.meta_base (fun tds ->
+  let tyb = match Task.get_meta_excl Encoding.meta_base tds with
+    | Some [Theory.MAts ts] when ts.ts_args = [] ->
+        begin match ts.ts_def with
+          | Some ty -> ty
+          | None -> ty_app ts []
+        end
+    | _ -> ty_base
+  in
+  monomorph tyb)
+
 let () = Encoding.register_enco_poly "explicit"
     (fun _ -> Trans.compose explicit monomorph)
 

src/transform/libencoding.ml

@@ -68,19 +68,10 @@ let lsdecl_of_tydecl tdl =
   in
   List.fold_right add tdl []
 
-(* sort symbol by default (= undeco) *)
-let ts_base = create_tysymbol (id_fresh "uni") [] None
-
-(* sort by default (= undeco) *)
-let ty_base = ty_app ts_base []
-
-(* ts_base declaration *)
-let d_ts_base = create_ty_decl [ts_base, Tabstract]
-
 (* convert a constant to a functional symbol of type ty_base *)
-let ls_of_const =
+let ls_of_const ty_base =
   let ht = Hterm.create 63 in
-  let ls_of_t t = match t.t_node with
+  fun t -> match t.t_node with
     | Tconst _ ->
         begin try Hterm.find ht t with Not_found ->
           let s = "const_" ^ Pp.string_of Pretty.print_term t in
@@ -89,30 +80,23 @@ let ls_of_const =
           ls
         end
     | _ -> assert false
-  in
-  fun c -> ls_of_t (t_const c)
-
-(* convert a constant to a term of type ty_base *)
-let term_of_const c = t_app (ls_of_const c) [] ty_base
 
-(* 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 tss (Sty.singleton ty_type)
+let ls_of_const =
+  let ht = Hty.create 3 in
+  fun ty -> try Hty.find ht ty with Not_found ->
+    let fn = ls_of_const ty in
+    Hty.add ht ty fn;
+    fn
 
 (* monomorphise modulo the set of kept types * and an lsymbol map *)
 
-let vs_monomorph kept vs =
+let vs_monomorph ty_base kept vs =
   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
-  let f_mono = f_monomorph kept lsmap consts in
+let rec t_monomorph ty_base kept lsmap consts vmap t =
+  let t_mono = t_monomorph ty_base kept lsmap consts in
+  let f_mono = f_monomorph ty_base kept lsmap consts in
   t_label_copy t (match t.t_node with
     | Tbvar _ ->
         assert false
@@ -120,8 +104,8 @@ let rec t_monomorph kept lsmap consts vmap t =
         Mvs.find v vmap
     | Tconst _ when Sty.mem t.t_ty kept ->
         t
-    | Tconst c ->
-        let ls = ls_of_const c in
+    | Tconst _ ->
+        let ls = ls_of_const ty_base t in
         consts := Sls.add ls !consts;
         t_app ls [] ty_base
     | Tapp (fs,_) when is_ls_of_ts fs ->
@@ -134,20 +118,20 @@ let rec t_monomorph kept lsmap consts vmap t =
         t_if (f_mono vmap f) (t_mono vmap t1) (t_mono vmap t2)
     | Tlet (t1,b) ->
         let u,t2,close = t_open_bound_cb b in
-        let v = vs_monomorph kept u in
+        let v = vs_monomorph ty_base kept u in
         let t2 = t_mono (Mvs.add u (t_var v) vmap) t2 in
         t_let (t_mono vmap t1) (close v t2)
     | Tcase _ ->
         Printer.unsupportedTerm t "no match expressions at this point"
     | Teps b ->
         let u,f,close = f_open_bound_cb b in
-        let v = vs_monomorph kept u in
+        let v = vs_monomorph ty_base kept u in
         let f = f_mono (Mvs.add u (t_var v) vmap) f in
         t_eps (close v f))
 
-and f_monomorph kept lsmap consts vmap f =
-  let t_mono = t_monomorph kept lsmap consts in
-  let f_mono = f_monomorph kept lsmap consts in
+and f_monomorph ty_base kept lsmap consts vmap f =
+  let t_mono = t_monomorph ty_base kept lsmap consts in
+  let f_mono = f_monomorph ty_base kept lsmap consts in
   f_label_copy f (match f.f_node with
     | Fapp (ps,[t1;t2]) when ls_equal ps ps_equ ->
         f_equ (t_mono vmap t1) (t_mono vmap t2)
@@ -155,7 +139,7 @@ and f_monomorph kept lsmap consts vmap f =
         f_app (lsmap ps) (List.map (t_mono vmap) tl)
     | Fquant (q,b) ->
         let ul,tl,f1,close = f_open_quant_cb b in
-        let vl = List.map (vs_monomorph kept) ul in
+        let vl = List.map (vs_monomorph ty_base kept) ul in
         let add acc u v = Mvs.add u (t_var v) acc in
         let vmap = List.fold_left2 add vmap ul vl in
         let tl = tr_map (t_mono vmap) (f_mono vmap) tl in
@@ -170,14 +154,17 @@ and f_monomorph kept lsmap consts vmap f =
         f_if (f_mono vmap f1) (f_mono vmap f2) (f_mono vmap f3)
     | Flet (t,b) ->
         let u,f1,close = f_open_bound_cb b in
-        let v = vs_monomorph kept u in
+        let v = vs_monomorph ty_base kept u in
         let f1 = f_mono (Mvs.add u (t_var v) vmap) f1 in
         f_let (t_mono vmap t) (close v f1)
     | Fcase _ ->
         Printer.unsupportedFmla f "no match expressions at this point")
 
-let d_monomorph kept lsmap d =
+let d_monomorph ty_base kept lsmap d =
+  let kept = Sty.add ty_base kept in
   let consts = ref Sls.empty in
+  let t_mono = t_monomorph ty_base kept lsmap consts in
+  let f_mono = f_monomorph ty_base kept lsmap consts in
   let dl = match d.d_node with
     | Dtype tdl ->
         let add td acc = match td with
@@ -196,12 +183,12 @@ let d_monomorph kept lsmap d =
           match ld with
           | Some ld ->
               let ul,e = open_ls_defn ld in
-              let vl = List.map (vs_monomorph kept) ul in
+              let vl = List.map (vs_monomorph ty_base kept) ul in
               let add acc u v = Mvs.add u (t_var v) acc in
               let vmap = List.fold_left2 add Mvs.empty ul vl in
               let e = match e with
-                | Term t -> Term (t_monomorph kept lsmap consts vmap t)
-                | Fmla f -> Fmla (f_monomorph kept lsmap consts vmap f)
+                | Term t -> Term (t_mono vmap t)
+                | Fmla f -> Fmla (f_mono vmap f)
               in
               make_ls_defn ls vl e
           | None ->
@@ -209,12 +196,23 @@ let d_monomorph kept lsmap d =
         in
         [create_logic_decl (List.map conv ldl)]
     | Dind idl ->
-        let iconv (pr,f) = pr, f_monomorph kept lsmap consts Mvs.empty f in
+        let iconv (pr,f) = pr, f_mono Mvs.empty f in
         let conv (ls,il) = lsmap ls, List.map iconv il in
         [create_ind_decl (List.map conv idl)]
     | Dprop (k,pr,f) ->
-        [create_prop_decl k pr (f_monomorph kept lsmap consts Mvs.empty f)]
+        [create_prop_decl k pr (f_mono Mvs.empty f)]
   in
   let add ls acc = create_logic_decl [ls,None] :: acc in
   Sls.fold add !consts dl
 
+(* 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 =
+    if ts.ts_args <> [] then acc
+    else match ts.ts_def with
+    | Some ty -> Sty.add ty acc
+    | None -> Sty.add (ty_app ts []) acc
+  in
+  Sts.fold add tss (Sty.singleton ty_type)
+

src/transform/libencoding.mli

@@ -45,23 +45,8 @@ val f_type_close : (vsymbol Mtv.t -> fmla -> fmla) -> fmla -> fmla
 (* convert a type declaration to a list of lsymbol declarations *)
 val lsdecl_of_tydecl : ty_decl list -> decl list
 
-(* sort symbol by default (= undeco) *)
-val ts_base : tysymbol
-
-(* sort by default (= undeco) *)
-val ty_base : ty
-
-(* ts_base declaration *)
-val d_ts_base : decl
-
-(* convert a constant to a functional symbol of type ty_base *)
-val ls_of_const : constant -> lsymbol
-
-(* convert a constant to a term of type ty_base *)
-val term_of_const : constant -> term
-
-(* monomorphise modulo the set of kept types * and an lsymbol map *)
-val d_monomorph : Sty.t -> (lsymbol -> lsymbol) -> decl -> decl list
+(* monomorphise wrt the base type, the set of kept types, and a symbol map *)
+val d_monomorph : ty -> 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