Commit ef16ef8c authored by Andrei Paskevich's avatar Andrei Paskevich

allow types in metas + improve clone/meta selectors in Task

parent 43445137
......@@ -394,6 +394,7 @@ let print_inst_pr fmt (pr1,pr2) =
fprintf fmt "prop %a = %a" print_pr pr1 print_pr pr2
let print_meta_arg_type fmt = function
| MTty -> fprintf fmt "[type]"
| MTtysymbol -> fprintf fmt "[type symbol]"
| MTlsymbol -> fprintf fmt "[logic symbol]"
| MTprsymbol -> fprintf fmt "[proposition]"
......@@ -401,6 +402,7 @@ let print_meta_arg_type fmt = function
| MTint -> fprintf fmt "[integer]"
let print_meta_arg fmt = function
| MAty ty -> fprintf fmt "type %a" print_ty ty
| MAts ts -> fprintf fmt "type %a" print_ts ts
| MAls ls -> fprintf fmt "logic %a" print_ls ls
| MApr pr -> fprintf fmt "prop %a" print_pr pr
......
......@@ -139,38 +139,38 @@ let remove_prop pr =
create_meta meta_remove_prop [MApr pr]
let get_syntax_map task =
let add_ts td m = match td.td_node with
| Meta (_,[MAts ts; MAstr s]) ->
let add_ts m = function
| [MAts ts; MAstr s] ->
Mid.add_new ts.ts_name s (KnownTypeSyntax ts) m
| _ -> assert false
in
let add_ls td m = match td.td_node with
| Meta (_,[MAls ls; MAstr s]) ->
let add_ls m = function
| [MAls ls; MAstr s] ->
Mid.add_new ls.ls_name s (KnownLogicSyntax ls) m
| _ -> assert false
in
let m = Mid.empty in
let m = Stdecl.fold add_ts (find_meta task meta_syntax_type).tds_set m in
let m = Stdecl.fold add_ls (find_meta task meta_syntax_logic).tds_set m in
let m = Task.on_meta meta_syntax_logic add_ls m task in
let m = Task.on_meta meta_syntax_type add_ts m task in
m
let get_remove_set task =
let add_ts td s = match td.td_node with
| Meta (_,[MAts ts; _]) -> Sid.add ts.ts_name s
let add_ts s = function
| [MAts ts; _] -> Sid.add ts.ts_name s
| _ -> assert false
in
let add_ls td s = match td.td_node with
| Meta (_,[MAls ls; _]) -> Sid.add ls.ls_name s
let add_ls s = function
| [MAls ls; _] -> Sid.add ls.ls_name s
| _ -> assert false
in
let add_pr td s = match td.td_node with
| Meta (_,[MApr pr]) -> Sid.add pr.pr_name s
let add_pr s = function
| [MApr pr] -> Sid.add pr.pr_name s
| _ -> assert false
in
let s = Sid.empty in
let s = Stdecl.fold add_ts (find_meta task meta_syntax_type).tds_set s in
let s = Stdecl.fold add_ls (find_meta task meta_syntax_logic).tds_set s in
let s = Stdecl.fold add_pr (find_meta task meta_remove_prop).tds_set s in
let s = Task.on_meta meta_syntax_type add_ts s task in
let s = Task.on_meta meta_syntax_logic add_ls s task in
let s = Task.on_meta meta_remove_prop add_pr s task in
s
let query_syntax sm id = Mid.find_option id sm
......
......@@ -44,7 +44,7 @@ let mk_tds s = Hstds.hashcons {
tds_tag = Hashweak.dummy_tag;
}
let empty_tds = mk_tds Stdecl.empty
let tds_empty = mk_tds Stdecl.empty
let tds_add td s = mk_tds (Stdecl.add td s.tds_set)
let tds_singleton td = mk_tds (Stdecl.singleton td)
......@@ -54,9 +54,9 @@ let tds_hash tds = Hashweak.tag_hash tds.tds_tag
type clone_map = tdecl_set Mid.t
type meta_map = tdecl_set Mmeta.t
let cm_find cm th = Mid.find_default th.th_name empty_tds cm
let cm_find cm th = Mid.find_default th.th_name tds_empty cm
let mm_find mm t = Mmeta.find_default t empty_tds mm
let mm_find mm t = Mmeta.find_default t tds_empty mm
let cm_add cm th td = Mid.change th.th_name (function
| None -> Some (tds_singleton td)
......@@ -114,8 +114,8 @@ let task_known = option_apply Mid.empty (fun t -> t.task_known)
let task_clone = option_apply Mid.empty (fun t -> t.task_clone)
let task_meta = option_apply Mmeta.empty (fun t -> t.task_meta)
let find_clone task th = cm_find (task_clone task) th
let find_meta task t = mm_find (task_meta task) t
let find_clone_tds task th = cm_find (task_clone task) th
let find_meta_tds task t = mm_find (task_meta task) t
(* constructors with checks *)
......@@ -179,7 +179,7 @@ and flat_tdecl task td = match td.td_node with
and use_export task th =
let td = create_null_clone th in
if Stdecl.mem td (find_clone task th).tds_set then task else
if Stdecl.mem td (find_clone_tds task th).tds_set then task else
let task = List.fold_left flat_tdecl task th.th_decls in
new_clone task th td
......@@ -215,45 +215,88 @@ let task_tdecls = task_fold (fun acc td -> td::acc) []
let task_decls = task_fold (fun acc td ->
match td.td_node with Decl d -> d::acc | _ -> acc) []
(* special selector for metaproperties of a single ident *)
(* Selectors *)
exception NotTaggingMeta of meta
exception NotExclusiveMeta of meta
let on_meta t fn acc task =
let add td acc = match td.td_node with
| Meta (_,ma) -> fn acc ma
| _ -> assert false
in
let tds = find_meta_tds task t in
Stdecl.fold add tds.tds_set acc
let on_theory th fn acc task =
let add td acc = match td.td_node with
| Clone (_,sm) -> fn acc sm
| _ -> assert false
in
let tds = find_clone_tds task th in
Stdecl.fold add tds.tds_set acc
let on_meta_excl t task =
if not t.meta_excl then raise (NotExclusiveMeta t);
let add td _ = match td.td_node with
| Meta (_,ma) -> Some ma
| _ -> assert false
in
let tds = find_meta_tds task t in
Stdecl.fold add tds.tds_set None
let on_used_theory th task =
let td = create_null_clone th in
let tds = find_clone_tds task th in
Stdecl.mem td tds.tds_set
let find_tagged_ts t tds acc =
let on_tagged_ty t task =
begin match t.meta_type with
| MTty :: _ -> ()
| _ -> raise (NotTaggingMeta t)
end;
let add td acc = match td.td_node with
| Meta (_, MAty ty :: _) -> Sty.add ty acc
| _ -> assert false
in
let tds = find_meta_tds task t in
Stdecl.fold add tds.tds_set Sty.empty
let on_tagged_ts t task =
begin match t.meta_type with
| MTtysymbol :: _ -> ()
| _ -> raise (NotTaggingMeta t)
end;
Stdecl.fold (fun td acc -> match td.td_node with
| Meta (s, MAts ts :: _) when meta_equal s t -> Sts.add ts acc
| _ -> assert false) tds.tds_set acc
(* TODO an exception instead of an assert false (wrong META used) *)
let find_tagged_ls t tds acc =
let add td acc = match td.td_node with
| Meta (_, MAts ts :: _) -> Sts.add ts acc
| _ -> assert false
in
let tds = find_meta_tds task t in
Stdecl.fold add tds.tds_set Sts.empty
let on_tagged_ls t task =
begin match t.meta_type with
| MTlsymbol :: _ -> ()
| _ -> raise (NotTaggingMeta t)
end;
Stdecl.fold (fun td acc -> match td.td_node with
| Meta (s, MAls ls :: _) when meta_equal s t -> Sls.add ls acc
| _ -> assert false) tds.tds_set acc
let find_tagged_pr t tds acc =
let add td acc = match td.td_node with
| Meta (_, MAls ls :: _) -> Sls.add ls acc
| _ -> assert false
in
let tds = find_meta_tds task t in
Stdecl.fold add tds.tds_set Sls.empty
let on_tagged_pr t task =
begin match t.meta_type with
| MTprsymbol :: _ -> ()
| _ -> raise (NotTaggingMeta t)
end;
Stdecl.fold (fun td acc -> match td.td_node with
| Meta (s, MApr pr :: _) when meta_equal s t -> Spr.add pr acc
| _ -> assert false) tds.tds_set acc
exception NotExclusiveMeta of meta
let get_meta_excl t tds =
if not t.meta_excl then raise (NotExclusiveMeta t);
Stdecl.fold (fun td _ -> match td.td_node with
| Meta (s,arg) when s = t -> Some arg
| _ -> assert false) tds.tds_set None
let add td acc = match td.td_node with
| Meta (_, MApr pr :: _) -> Spr.add pr acc
| _ -> assert false
in
let tds = find_meta_tds task t in
Stdecl.fold add tds.tds_set Spr.empty
(* Exception reporting *)
......
......@@ -33,6 +33,7 @@ type tdecl_set = private {
val tds_equal : tdecl_set -> tdecl_set -> bool
val tds_hash : tdecl_set -> int
val tds_empty : tdecl_set
type clone_map = tdecl_set Mid.t
type meta_map = tdecl_set Mmeta.t
......@@ -60,8 +61,8 @@ val task_known : task -> known_map
val task_clone : task -> clone_map
val task_meta : task -> meta_map
val find_clone : task -> theory -> tdecl_set
val find_meta : task -> meta -> tdecl_set
val find_clone_tds : task -> theory -> tdecl_set
val find_meta_tds : task -> meta -> tdecl_set
(** {2 constructors} *)
......@@ -95,22 +96,24 @@ val task_decls : task -> decl list
val task_goal : task -> prsymbol
(* special selector for metaproperties of a single ident *)
(** {2 selectors} *)
exception NotTaggingMeta of meta
val find_tagged_ts : meta -> tdecl_set -> Sts.t -> Sts.t
val find_tagged_ls : meta -> tdecl_set -> Sls.t -> Sls.t
val find_tagged_pr : meta -> tdecl_set -> Spr.t -> Spr.t
val on_meta : meta -> ('a -> meta_arg list -> 'a) -> 'a -> task -> 'a
val on_theory : theory -> ('a -> symbol_map -> 'a) -> 'a -> task -> 'a
(* special selector for exclusive metaproperties *)
exception NotExclusiveMeta of meta
val on_meta_excl : meta -> task -> meta_arg list option
val on_used_theory : theory -> task -> bool
val get_meta_excl : meta -> tdecl_set -> meta_arg list option
val on_tagged_ty : meta -> task -> Sty.t
val on_tagged_ts : meta -> task -> Sts.t
val on_tagged_ls : meta -> task -> Sls.t
val on_tagged_pr : meta -> task -> Spr.t
(* exceptions *)
exception NotTaggingMeta of meta
exception NotExclusiveMeta of meta
exception GoalNotFound
exception GoalFound
exception SkipFound
......
......@@ -90,6 +90,7 @@ let ns_find_ns = ns_find (fun ns -> ns.ns_ns)
(** Meta properties *)
type meta_arg_type =
| MTty
| MTtysymbol
| MTlsymbol
| MTprsymbol
......@@ -97,6 +98,7 @@ type meta_arg_type =
| MTint
type meta_arg =
| MAty of ty
| MAts of tysymbol
| MAls of lsymbol
| MApr of prsymbol
......@@ -189,6 +191,7 @@ module Hstdecl = Hashcons.Make (struct
type t = tdecl
let eq_marg a1 a2 = match a1,a2 with
| MAty ty1, MAty ty2 -> ty_equal ty1 ty2
| MAts ts1, MAts ts2 -> ts_equal ts1 ts2
| MAls ls1, MAls ls2 -> ls_equal ls1 ls2
| MApr pr1, MApr pr2 -> pr_equal pr1 pr2
......@@ -215,6 +218,7 @@ module Hstdecl = Hashcons.Make (struct
let hs_cl_pr _ pr acc = Hashcons.combine acc (pr_hash pr)
let hs_ta = function
| MAty ty -> ty_hash ty
| MAts ts -> ts_hash ts
| MAls ls -> ls_hash ls
| MApr pr -> pr_hash pr
......@@ -314,6 +318,7 @@ let known_clone kn sm =
let known_meta kn al =
let check = function
| MAty ty -> ty_s_fold (fun () ts -> known_id kn ts.ts_name) () ty
| MAts ts -> known_id kn ts.ts_name
| MAls ls -> known_id kn ls.ls_name
| MApr pr -> known_id kn pr.pr_name
......@@ -587,6 +592,7 @@ let cl_decl cl inst d = match d.d_node with
| Dprop p -> cl_prop cl inst p
let cl_marg cl = function
| MAty ty -> MAty (cl_trans_ty cl ty)
| MAts ts -> MAts (cl_find_ts cl ts)
| MAls ls -> MAls (cl_find_ls cl ls)
| MApr pr -> MApr (cl_find_pr cl pr)
......@@ -666,6 +672,7 @@ let is_empty_sm sm =
(** Meta properties *)
let get_meta_arg_type = function
| MAty _ -> MTty
| MAts _ -> MTtysymbol
| MAls _ -> MTlsymbol
| MApr _ -> MTprsymbol
......@@ -674,6 +681,12 @@ let get_meta_arg_type = function
let create_meta m al =
let get_meta_arg at a =
(* we allow "constant tysymbol <=> ty" conversion *)
let a = match at,a with
| MTtysymbol, MAty ({ ty_node = Tyapp (ts,[]) }) -> MAts ts
| MTty, MAts ts when ts.ts_args = [] -> MAty (ty_app ts [])
| _, _ -> a
in
let mt = get_meta_arg_type a in
if at = mt then a else raise (MetaTypeMismatch (m,at,mt))
in
......@@ -685,19 +698,20 @@ let create_meta m al =
let add_meta uc s al = add_tdecl uc (create_meta s al)
let clone_meta tdt th tdc = match tdt.td_node, tdc.td_node with
| Meta (t,al), Clone (th',sm) when id_equal th.th_name th'.th_name ->
let clone_meta tdt sm = match tdt.td_node with
| Meta (t,al) ->
let find_ts ts = Mts.find_default ts ts sm.sm_ts in
let find_ls ls = Mls.find_default ls ls sm.sm_ls in
let find_pr pr = Mpr.find_default pr pr sm.sm_pr in
let cl_marg = function
| MAty ty -> MAty (ty_s_map find_ts ty)
| MAts ts -> MAts (find_ts ts)
| MAls ls -> MAls (find_ls ls)
| MApr pr -> MApr (find_pr pr)
| a -> a
in
mk_tdecl (Meta (t, List.map cl_marg al))
| _,_ -> invalid_arg "clone_meta"
| _ -> invalid_arg "clone_meta"
(** Base theories *)
......@@ -738,6 +752,7 @@ let tuple_theory_name s =
(* Exception reporting *)
let print_meta_arg_type fmt = function
| MTty -> fprintf fmt "type"
| MTtysymbol -> fprintf fmt "type_symbol"
| MTlsymbol -> fprintf fmt "logic_symbol"
| MTprsymbol -> fprintf fmt "proposition"
......
......@@ -44,6 +44,7 @@ val ns_find_ns : namespace -> string list -> namespace
(** Meta properties *)
type meta_arg_type =
| MTty
| MTtysymbol
| MTlsymbol
| MTprsymbol
......@@ -51,6 +52,7 @@ type meta_arg_type =
| MTint
type meta_arg =
| MAty of ty
| MAts of tysymbol
| MAls of lsymbol
| MApr of prsymbol
......@@ -176,10 +178,9 @@ val create_meta : meta -> meta_arg list -> tdecl
val add_meta : theory_uc -> meta -> meta_arg list -> theory_uc
val clone_meta : tdecl -> theory -> tdecl -> tdecl
(* [clone_meta td_meta th td_clone] produces from [td_meta]
* a new Meta tdecl instantiated with respect to [td_clone].
* The [th] argument must be the same as in [td_clone]. *)
val clone_meta : tdecl -> symbol_map -> tdecl
(* [clone_meta td_meta sm] produces from [td_meta]
* a new Meta tdecl instantiated with respect to [sm]]. *)
(** Base theories *)
......
......@@ -140,69 +140,81 @@ end)
let on_theory_tds th fn =
let fn = Wtds.memoize 17 fn in
fun task -> fn (find_clone task th) task
fun task -> fn (find_clone_tds task th) task
let on_meta_tds t fn =
let fn = Wtds.memoize 17 fn in
fun task -> fn (find_meta task t) task
fun task -> fn (find_meta_tds task t) task
let on_theory th fn =
let sml td acc = match td.td_node with
let add td acc = match td.td_node with
| Clone (_,sm) -> sm::acc
| _ -> assert false
in
on_theory_tds th (fun tds -> fn (Stdecl.fold sml tds.tds_set []))
on_theory_tds th (fun tds -> fn (Stdecl.fold add tds.tds_set []))
let on_meta t fn =
let mal td acc = match td.td_node with
let add td acc = match td.td_node with
| Meta (_,ma) -> ma::acc
| _ -> assert false
in
on_meta_tds t (fun tds -> fn (Stdecl.fold mal tds.tds_set []))
let on_theories tl fn =
let rec pass acc = function
| th::tl ->
let fn st = pass (Mid.add th.th_name st acc) tl in
on_theory_tds th fn
| [] ->
fn acc
in
pass Mid.empty tl
let on_metas tl fn =
let rec pass acc = function
| t::tl ->
let fn st = pass (Mmeta.add t st acc) tl in
on_meta_tds t fn
| [] ->
fn acc
in
pass Mmeta.empty tl
on_meta_tds t (fun tds -> fn (Stdecl.fold add tds.tds_set []))
let on_used_theory th fn =
let td = create_null_clone th in
on_theory_tds th (fun tds -> fn (Stdecl.mem td tds.tds_set))
let on_used_theories thl fn =
let add acc th = Mid.add th.th_name (create_null_clone th) acc in
let tdm = List.fold_left add Mid.empty thl in
let test _ td tds =
if Stdecl.mem td tds.tds_set then Some () else None
in
on_theories thl (fun cm -> fn (Mid.inter test tdm cm))
let on_meta_excl t fn =
on_meta_tds t (fun tds -> fn (get_meta_excl t tds))
if not t.meta_excl then raise (NotExclusiveMeta t);
let add td _ = match td.td_node with
| Meta (_,ma) -> Some ma
| _ -> assert false
in
on_meta_tds t (fun tds -> fn (Stdecl.fold add tds.tds_set None))
let on_tagged_ty t fn =
begin match t.meta_type with
| MTty :: _ -> ()
| _ -> raise (NotTaggingMeta t)
end;
let add td acc = match td.td_node with
| Meta (_, MAty ty :: _) -> Sty.add ty acc
| _ -> assert false
in
on_meta_tds t (fun tds -> fn (Stdecl.fold add tds.tds_set Sty.empty))
let on_tagged_ts t fn =
on_meta_tds t (fun tds -> fn (find_tagged_ts t tds Sts.empty))
begin match t.meta_type with
| MTtysymbol :: _ -> ()
| _ -> raise (NotTaggingMeta t)
end;
let add td acc = match td.td_node with
| Meta (_, MAts ts :: _) -> Sts.add ts acc
| _ -> assert false
in
on_meta_tds t (fun tds -> fn (Stdecl.fold add tds.tds_set Sts.empty))
let on_tagged_ls t fn =
on_meta_tds t (fun tds -> fn (find_tagged_ls t tds Sls.empty))
begin match t.meta_type with
| MTlsymbol :: _ -> ()
| _ -> raise (NotTaggingMeta t)
end;
let add td acc = match td.td_node with
| Meta (_, MAls ls :: _) -> Sls.add ls acc
| _ -> assert false
in
on_meta_tds t (fun tds -> fn (Stdecl.fold add tds.tds_set Sls.empty))
let on_tagged_pr t fn =
on_meta_tds t (fun tds -> fn (find_tagged_pr t tds Spr.empty))
begin match t.meta_type with
| MTprsymbol :: _ -> ()
| _ -> raise (NotTaggingMeta t)
end;
let add td acc = match td.td_node with
| Meta (_, MApr pr :: _) -> Spr.add pr acc
| _ -> assert false
in
on_meta_tds t (fun tds -> fn (Stdecl.fold add tds.tds_set Spr.empty))
(** register transformations *)
......
......@@ -68,17 +68,13 @@ val rewrite : (term -> term) -> (fmla -> fmla) -> task -> task trans
(* dependent transformatons *)
val on_theories : theory list -> (clone_map -> 'a trans) -> 'a trans
val on_metas : meta list -> (meta_map -> 'a trans) -> 'a trans
val on_meta : meta -> (meta_arg list list -> 'a trans) -> 'a trans
val on_theory : theory -> (symbol_map list -> 'a trans) -> 'a trans
val on_meta : meta -> (meta_arg list list -> 'a trans) -> 'a trans
val on_used_theory : theory -> (bool -> 'a trans) -> 'a trans
val on_used_theories : theory list -> (Ident.Sid.t -> 'a trans) -> 'a trans
val on_meta_excl : meta -> (meta_arg list option -> 'a trans) -> 'a trans
val on_used_theory : theory -> (bool -> 'a trans) -> 'a trans
val on_tagged_ty : meta -> (Sty.t -> 'a trans) -> 'a trans
val on_tagged_ts : meta -> (Sts.t -> 'a trans) -> 'a trans
val on_tagged_ls : meta -> (Sls.t -> 'a trans) -> 'a trans
val on_tagged_pr : meta -> (Spr.t -> 'a trans) -> 'a trans
......
......@@ -212,22 +212,20 @@ let update_task drv task =
in
let task =
Mid.fold (fun _ (th,s) task ->
let cs = (find_clone task th).tds_set in
Stdecl.fold (fun td task -> match td.td_node with
| Clone (_,sm) when is_empty_sm sm ->
Stdecl.fold (fun td task -> add_tdecl task td) s task
| _ -> task
) cs task
if Task.on_used_theory th task then
Stdecl.fold (fun tdm task ->
add_tdecl task tdm
) s task
else task
) drv.drv_meta task
in
let task =
Mid.fold (fun _ (th,s) task ->
let cs = (find_clone task th).tds_set in
Stdecl.fold (fun tdc task ->
Task.on_theory th (fun task sm ->
Stdecl.fold (fun tdm task ->
add_tdecl task (clone_meta tdm th tdc)
add_tdecl task (clone_meta tdm sm)
) s task
) cs task
) task task
) drv.drv_meta_cl task
in
add_tdecl task goal
......
......@@ -222,8 +222,7 @@ let print_task pr thpr fmt task =
let info = {
info_syn = get_syntax_map task;
info_rem = get_remove_set task;
info_ac =
Task.find_tagged_ls meta_ac (find_meta task meta_ac) Sls.empty }
info_ac = Task.on_tagged_ls meta_ac task }
in
let decls = Task.task_decls task in
ignore (print_list_opt (add_flush newline2) (print_decl info) fmt decls)
......
......@@ -221,10 +221,9 @@ let print_decl info fmt d = match d.d_node with
let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt)
let barrays task =
let sds = find_meta task Encoding_arrays.meta_mono_array in
let fold tdecl barrays =
match tdecl.td_node with
| Meta (_,[MAts tst;MAts tsk;MAts tse]) ->
let fold barrays =
function
| [MAts tst;MAts tsk;MAts tse] ->
let extract_ty ts =
if ts.ts_args <> [] then
unsupported "smtv1 : type with argument are not supported";
......@@ -233,7 +232,7 @@ let barrays task =
| None -> ty_app ts [] in
Mts.add tst (extract_ty tsk,extract_ty tse) barrays
| _ -> barrays in
Stdecl.fold fold sds.tds_set Mts.empty
Task.on_meta Encoding_arrays.meta_mono_array fold Mts.empty task
let print_task pr thpr fmt task =
fprintf fmt "(benchmark why3@\n"
......
......@@ -379,6 +379,7 @@ let print_inst_pr fmt (pr1,pr2) =
fprintf fmt "prop %a = %a" print_pr pr1 print_pr pr2
let print_meta_arg fmt = function
| MAty ty -> fprintf fmt "type %a" print_ty ty
| MAts ts -> fprintf fmt "type %a" print_ts ts
| MAls ls -> fprintf fmt "logic %a" print_ls ls
| MApr pr -> fprintf fmt "prop %a" print_pr pr
......
......@@ -441,8 +441,7 @@ let monomorphise_goal =
acc)
let collect_green_part tds =
let sts = Task.find_tagged_ts meta_kept tds Sts.empty in
let collect_green_part sts =
let extract ts tys =
assert (ts.ts_args = []); (* UnsupportedTySymbol? *)
Mty.add (match ts.ts_def with
......@@ -453,8 +452,8 @@ let collect_green_part tds =
(* Some general env creation function *)
let create_env task tenv tds =
let keep = collect_green_part tds in
let create_env task tenv kept =
let keep = collect_green_part kept in
let projty = Mty.fold (fun ty _ ty_ty ->
Mty.add ty ty ty_ty)
keep Mty.empty in
......@@ -483,20 +482,19 @@ let is_ty_mono ~only_mono ty =
with Exit when not only_mono -> false
let create_trans_complete metas =
let tds_kept = Mmeta.find meta_kept metas in
let complete = get_meta_excl meta_complete
(Mmeta.find meta_complete metas) in
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 tds_kept in
let init_task,env = create_env task tenv kept in
Trans.fold_map fold_map env init_task
let encoding_instantiate =
Trans.on_metas [meta_kept;meta_complete] create_trans_complete
Trans.on_tagged_ts 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)
......
......@@ -25,10 +25,6 @@ open Decl
open Theory
open Task
let meta_kept = register_meta "encoding_decorate : kept" [MTtysymbol]
(* From Encoding Polymorphism CADE07*)
type tenv = {
specials : tysymbol Hty.t;
trans_lsymbol : lsymbol Hls.t
......@@ -166,6 +162,7 @@ let fold tenv taskpre task =
begin try
let ud = Hts.create 3 in
let map = function
| MAty ty -> MAty (conv_ty tenv ud ty)
| MAts {ts_name = name; ts_args = []; ts_def = Some ty} ->
MAts (conv_ts tenv ud name ty)
| MAts _ -> raise Exit
......@@ -179,6 +176,7 @@ let fold tenv taskpre task =
| Exit -> add_tdecl task taskpre.task_decl
end
| _ -> add_tdecl task taskpre.task_decl
let t =
let tenv = init_tenv in
Trans.fold (fold tenv) None
......