get rid of user-supplied ty_base

What was its purpose in the first place? Integers are protected
in Simplify anyway and then we can simply forget the difference
between the infinite sorts (as we do in encoding_tptp).

drivers/simplify.drv

@@ -33,11 +33,6 @@ transformation "encoding_tptp"
 theory BuiltIn
   syntax logic (=)  "(EQ %1 %2)"
 
-  (* use with explicit polymorphism *)
-  (* meta "enco_poly" "explicit" *)
-  meta "encoding : base" type int
-
-  (* use with encoding_decorate *)
   meta "enco_poly" "decorate"
   meta "encoding : kept" type int
 

src/transform/encoding.ml

@@ -28,8 +28,7 @@ open Trans
 
 let debug = Debug.register_flag "encoding"
 
-let meta_kept = register_meta      "encoding : kept" [MTty]
-let meta_base = register_meta_excl "encoding : base" [MTtysymbol]
+let meta_kept = register_meta "encoding : kept" [MTty]
 
 let meta_select_kept = register_meta_excl "select_kept" [MTstring]
 let meta_enco_kept   = register_meta_excl "enco_kept"   [MTstring]

src/transform/encoding.mli

@@ -19,7 +19,6 @@
 
 val debug : Debug.flag
 
-val meta_base : Theory.meta
 val meta_kept : Theory.meta
 
 val ft_select_kept : (Env.env,Ty.Sty.t)  Trans.flag_trans

src/transform/encoding_decorate.ml

@@ -70,9 +70,6 @@ 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
@@ -97,10 +94,10 @@ let mono_init =
   init
 
 let mono kept =
-  Trans.decl (d_monomorph ty_base kept (lsmap kept)) mono_init
+  let kept = Sty.add ty_type kept in
+  Trans.decl (d_monomorph kept (lsmap kept)) mono_init
 
 let t = Trans.on_tagged_ty Encoding.meta_kept (fun kept ->
-  let kept = Sty.add ty_type kept in
   Trans.compose (deco kept) (mono kept))
 
 let () = Hashtbl.replace Encoding.ft_enco_poly "decorate" (const t)

src/transform/encoding_explicit.ml

@@ -131,7 +131,7 @@ let meta_enum = Eliminate_algebraic.meta_enum
 let explicit =
   Trans.on_tagged_ts meta_enum (fun enum ->
     if Sts.is_empty enum then explicit
-    else 
+    else
       let ts = Sts.choose enum in
       let ty = ty_app ts (List.map ty_var ts.ts_args) in
       Printer.unsupportedType ty
@@ -140,11 +140,10 @@ let explicit =
 
 (** {2 monomorphise task } *)
 
-let ts_base = create_tysymbol (id_fresh "uni") [] None
-let ty_base = ty_app ts_base []
+open Libencoding
 
-let lsmap tyb kept = Wls.memoize 63 (fun ls ->
-  let tymap ty = if Sty.mem ty kept then ty else tyb in
+let lsmap kept = Wls.memoize 63 (fun ls ->
+  let tymap ty = if Sty.mem ty kept then ty else 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 &&
@@ -153,26 +152,11 @@ let lsmap tyb kept = Wls.memoize 63 (fun ls ->
 
 let d_ts_base = create_ty_decl [ts_base, Tabstract]
 
-let monomorph tyb = Trans.on_tagged_ty Encoding.meta_kept (fun kept ->
+let monomorph = Trans.on_tagged_ty Encoding.meta_kept (fun kept ->
   let kept = Sty.add ty_type 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
+  let decl = d_monomorph kept (lsmap kept) in
   Trans.decl decl (Task.add_decl None d_ts_base))
 
-let monomorph = Trans.on_meta_excl Encoding.meta_base (fun alo ->
-  let tyb = match alo 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 () = Hashtbl.replace Encoding.ft_enco_poly "explicit"
     (fun _ -> Trans.compose explicit monomorph)
 

src/transform/encoding_guard.ml

@@ -259,11 +259,10 @@ let guard =
 
 (** {2 monomorphise task } *)
 
-let ts_base = create_tysymbol (id_fresh "uni") [] None
-let ty_base = ty_app ts_base []
+open Libencoding
 
-let lsmap tyb kept = Wls.memoize 63 (fun ls ->
-  let tymap ty = if Sty.mem ty kept then ty else tyb in
+let lsmap kept = Wls.memoize 63 (fun ls ->
+  let tymap ty = if Sty.mem ty kept then ty else 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 &&
@@ -272,25 +271,10 @@ let lsmap tyb kept = Wls.memoize 63 (fun ls ->
 
 let d_ts_base = create_ty_decl [ts_base, Tabstract]
 
-let monomorph tyb = Trans.on_tagged_ty Encoding.meta_kept (fun kept ->
+let monomorph = Trans.on_tagged_ty Encoding.meta_kept (fun kept ->
   let kept = Sty.add ty_type 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
+  let decl = d_monomorph kept (lsmap kept) in
   Trans.decl decl (Task.add_decl None d_ts_base))
 
-let monomorph = Trans.on_meta_excl Encoding.meta_base (fun alo ->
-  let tyb = match alo 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 () = Hashtbl.replace Encoding.ft_enco_poly "guard"
     (fun _ -> Trans.compose guard monomorph)

src/transform/libencoding.ml

@@ -23,6 +23,15 @@ open Ty
 open Term
 open Decl
 
+(* sort symbol of the "universal" type *)
+let ts_base = create_tysymbol (id_fresh "uni") [] None
+
+(* "universal" sort *)
+let ty_base = ty_app ts_base []
+
+(* ts_base declaration *)
+let d_ts_base = create_ty_decl [ts_base, Tabstract]
+
 (* sort symbol of (polymorphic) types *)
 let ts_type = create_tysymbol (id_fresh "ty") [] None
 
@@ -126,7 +135,7 @@ let lsdecl_of_tydecl_select tdl =
 let lsdecl_of_tydecl tdl = List.fold_left lsdecl_of_tydecl [] tdl
 
 (* convert a constant to a functional symbol of type ty_base *)
-let ls_of_const ty_base =
+let ls_of_const =
   let ht = Hterm.create 63 in
   fun t -> match t.t_node with
     | Tconst _ ->
@@ -138,28 +147,21 @@ let ls_of_const ty_base =
         end
     | _ -> assert false
 
-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 ty_base kept vs =
+let vs_monomorph 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 ty_base kept lsmap consts vmap t =
-  let t_mono = t_monomorph ty_base kept lsmap consts in
+let rec t_monomorph kept lsmap consts vmap t =
+  let t_mono = t_monomorph kept lsmap consts in
   t_label_copy t (match t.t_node with
     | Tvar v ->
         Mvs.find v vmap
     | Tconst _ when Sty.mem (t_type t) kept ->
         t
     | Tconst _ ->
-        let ls = ls_of_const ty_base t in
+        let ls = ls_of_const t in
         consts := Sls.add ls !consts;
         fs_app ls [] ty_base
     | Tapp (ps,[t1;t2]) when ls_equal ps ps_equ ->
@@ -171,19 +173,19 @@ let rec t_monomorph ty_base kept lsmap consts vmap t =
         t_if (t_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 ty_base kept u in
+        let v = vs_monomorph 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 = t_open_bound_cb b in
-        let v = vs_monomorph ty_base kept u in
+        let v = vs_monomorph kept u in
         let f = t_mono (Mvs.add u (t_var v) vmap) f in
         t_eps (close v f)
     | Tquant (q,b) ->
         let ul,tl,f1,close = t_open_quant_cb b in
-        let vl = List.map (vs_monomorph ty_base kept) ul in
+        let vl = List.map (vs_monomorph 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) tl in
@@ -195,10 +197,10 @@ let rec t_monomorph ty_base kept lsmap consts vmap t =
     | Ttrue | Tfalse ->
         t)
 
-let d_monomorph ty_base kept lsmap d =
-  let kept = Sty.add ty_base kept in
+let d_monomorph kept lsmap d =
   let consts = ref Sls.empty in
-  let t_mono = t_monomorph ty_base kept lsmap consts in
+  let kept = Sty.add ty_base kept in
+  let t_mono = t_monomorph kept lsmap consts in
   let dl = match d.d_node with
     | Dtype tdl ->
         let add td acc = match td with
@@ -217,7 +219,7 @@ let d_monomorph ty_base kept lsmap d =
           match ld with
           | Some ld ->
               let ul,e,close = open_ls_defn_cb ld in
-              let vl = List.map (vs_monomorph ty_base kept) ul in
+              let vl = List.map (vs_monomorph 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
               close ls vl (t_mono vmap e)

src/transform/libencoding.mli

@@ -21,6 +21,15 @@ open Ty
 open Term
 open Decl
 
+(* sort symbol of the "universal" type *)
+val ts_base : tysymbol
+
+(* "universal" sort *)
+val ty_base : ty
+
+(* ts_base type declaration *)
+val d_ts_base : decl
+
 (* sort symbol of (polymorphic) types *)
 val ts_type : tysymbol
 
@@ -54,8 +63,8 @@ val lsdecl_of_tydecl : ty_decl list -> decl list
 (* convert a type declaration to a list of lsymbol declarations *)
 val lsdecl_of_tydecl_select : ty_decl list -> 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
+(* monomorphise wrt the set of kept types, and a symbol map *)
+val d_monomorph : Sty.t -> (lsymbol -> lsymbol) -> decl -> decl list
 
 (* close by subtype the set of type tagged by the meta "kept" *)
 val close_kept : Task.task Trans.trans