Commit d4bb6587 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

split encoding_instantiate to e_i and e_i_complete

parent 1555cdd0
......@@ -28,9 +28,6 @@ open Task
open Decl
open Encoding
let meta_complete = register_meta_excl
"encoding_instantiate : complete" [MTstring]
exception TooMuchInstantiation of int
let max_instantiation = 512 (* 7 ** 3 = 343 *)
......@@ -522,36 +519,19 @@ let is_ty_mono ~only_mono ty =
let create_trans_complete kept complete =
let task = use_export None builtin_theory in
let tenv = match complete with
| None | Some [MAstr "yes"] -> Complete
| Some [MAstr "no"] -> Incomplete
| _ -> failwith "instantiate complete wrong argument" in
let init_task,env = create_env task tenv kept in
let init_task,env = create_env task complete kept in
Trans.fold_map fold_map env init_task
let encoding_instantiate =
let encoding_instantiate complete =
Trans.compose Libencoding.close_kept
(Trans.on_tagged_ty Libencoding.meta_kept (fun kept ->
Trans.on_meta_excl meta_complete (fun complete ->
create_trans_complete kept complete)))
create_trans_complete kept complete))
let () = Hashtbl.replace Encoding.ft_enco_kept "instantiate"
(const encoding_instantiate)
let create_trans_complete create_env kept complete =
let task = use_export None builtin_theory in
let tenv = match complete with
| None | Some [MAstr "yes"] -> Complete
| Some [MAstr "no"] -> Incomplete
| _ -> failwith "instantiate complete wrong argument" in
let init_task,env = create_env task tenv kept in
Trans.fold_map fold_map env init_task
(const (encoding_instantiate Incomplete))
let t create_env =
Trans.on_tagged_ty Libencoding.meta_kept (fun kept ->
Trans.on_meta_excl meta_complete (fun complete ->
create_trans_complete create_env kept complete))
let () = Hashtbl.replace Encoding.ft_enco_kept "instantiate_complete"
(const (encoding_instantiate Complete))
(*
Local Variables:
......
......@@ -17,29 +17,3 @@
(* *)
(**************************************************************************)
open Ty
open Term
open Decl
open Stdlib
open Task
module Mtyl : Map.S with type key = ty list
type tenv =
| Complete (* The transformation keep the polymorphism *)
| Incomplete (* The environnement when the transformation isn't complete*)
type env = {
etenv : tenv;
ekeep : Sty.t;
prop_toremove : ty Mtv.t Mpr.t;
eprojty : ty Mty.t;
edefined_lsymbol : lsymbol Mtyl.t Mls.t;
edefined_tsymbol : tysymbol Mtyl.t Mts.t;
}
type auto_clone = task -> tenv -> Sty.t -> task * env
val create_env : task -> tenv -> Sty.t -> task * env
val t : auto_clone -> Task.task Trans.trans
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment