encoding : forgot to close by subtype the kept set

src/core/trans.ml

@@ -129,6 +129,14 @@ let tgoal_l = gen_goal_l add_tdecl
 
 let rewrite fnT fnF = decl (fun d -> [decl_map fnT fnF d])
 
+let gen_add_decl add decls = function
+  | Some { task_decl = { td_node = Decl d }; task_prev = prev } ->
+    add_decl (List.fold_left add prev decls) d
+  | _ -> assert false
+
+let add_decls  = gen_add_decl add_decl
+let add_tdecls = gen_add_decl add_tdecl
+
 (** dependent transformations *)
 
 module Wtds = Hashweak.Make (struct

src/core/trans.mli

@@ -64,6 +64,9 @@ val tgoal_l : (prsymbol -> fmla -> tdecl list list) -> task tlist
 
 val rewrite : (term -> term) -> (fmla -> fmla) -> task -> task trans
 
+val add_decls  : decl list -> task trans
+val add_tdecls : tdecl list -> task trans
+
 (* dependent transformatons *)
 
 val on_meta : meta -> (meta_arg list list -> 'a trans) -> 'a trans

src/transform/encoding_bridge.ml

@@ -275,9 +275,11 @@ let decl tenv d =
   res
 *)
 
-let t env = Trans.on_tagged_ty meta_kept (fun s ->
-  let init_task,tenv = load_prelude s env in
-  Trans.tdecl (decl tenv) init_task)
+let t env =
+  Trans.compose Libencoding.close_kept
+  (Trans.on_tagged_ty meta_kept (fun s ->
+    let init_task,tenv = load_prelude s env in
+    Trans.tdecl (decl tenv) init_task))
 
 let () = register_enco_kept "bridge" t
 

src/transform/encoding_instantiate.ml

@@ -528,9 +528,10 @@ let create_trans_complete kept complete =
   Trans.fold_map fold_map env init_task
 
 let encoding_instantiate =
-  Trans.on_tagged_ty meta_kept (fun kept ->
-  Trans.on_meta_excl meta_complete (fun complete ->
-    create_trans_complete kept complete))
+  Trans.compose Libencoding.close_kept
+  (Trans.on_tagged_ty meta_kept (fun kept ->
+    Trans.on_meta_excl meta_complete (fun complete ->
+      create_trans_complete kept complete)))
 
 let () =
   register_enco_kept "instantiate" (fun _ -> encoding_instantiate)

src/transform/libencoding.ml

@@ -198,3 +198,18 @@ let d_monomorph ty_base kept lsmap d =
   in
   let add ls acc = create_logic_decl [ls,None] :: acc in
   Sls.fold add !consts dl
+
+(** close by subterm *)
+let close_kept =
+  Trans.on_tagged_ty Encoding.meta_kept (fun kept ->
+    let fold ty acc =
+      let rec add acc ty = ty_fold add (Sty.add ty acc) ty in
+      add acc ty in
+    let kept' = Sty.fold fold kept kept in
+    if kept == kept' then Trans.identity
+    else
+      let kept' = Sty.diff kept' kept in
+      let fold ty acc =
+        Theory.create_meta Encoding.meta_kept [Theory.MAty ty] :: acc in
+      Trans.add_tdecls (Sty.fold fold kept' [])
+  )

src/transform/libencoding.mli

@@ -47,3 +47,6 @@ val lsdecl_of_tydecl : 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
+
+(* Close by subtype the set of type tagged by the meta "kept" *)
+val close_kept : Task.task Trans.trans