Commit 609ce9bf authored by François Bobot's avatar François Bobot

meta kept : tysymbol -> ty

parent e459c7fc
......@@ -22,7 +22,7 @@ open Theory
open Task
open Trans
let meta_kept = register_meta "encoding : kept" [MTtysymbol]
let meta_kept = register_meta "encoding : kept" [MTty]
let meta_base = register_meta_excl "encoding : base" [MTtysymbol]
let debug = Debug.register_flag "encoding"
......
......@@ -67,11 +67,7 @@ let load_prelude kept env =
specials = specials;
trans_lsymbol = Hls.create 17;
trans_tsymbol = trans_tsymbol} in
let clone_builtin ts (task,sty) =
let ty = match ts.ts_def with
| Some ty -> ty
| None -> try ty_app ts [] with BadTypeArity(_,_,_) ->
failwith "kept without definition must be constant" in
let clone_builtin ty (task,sty) =
let add_ts task ts = add_ty_decl task [ts,Tabstract] in
let task = ty_s_fold add_ts task ty in
let is_constant =
......@@ -82,7 +78,6 @@ let load_prelude kept env =
match ty.ty_node with
| Tyapp (ts,_) -> ts
| _ -> assert false in
let task = add_ts task ts in
let tb = create_tysymbol (id_clone ts_head.ts_name) []
(if is_constant then None else Some (ty_of_ty tenv_tmp ty)) in
let task = add_ts task tb in
......@@ -91,6 +86,8 @@ let load_prelude kept env =
let t2tb = create_fsymbol (id_clone logic_t2tb.ls_name) [ty] tytb in
let task = add_logic_decl task [tb2t,None] in
let task = add_logic_decl task [t2tb,None] in
let name = id_fresh "meta_ty" in
let ts = create_tysymbol name [] (Some ty) in
let th_inst = create_inst
~ts:[type_t,ts;type_tb,tb]
~ls:[logic_t2tb,t2tb;logic_tb2t,tb2t] ~lemma:[] ~goal:[] in
......@@ -100,7 +97,7 @@ let load_prelude kept env =
if is_constant then Hts.add trans_tsymbol ts_head tb;
Hty.add specials ty lconv;
task,Sty.add ty sty in
let task,kept = Sts.fold clone_builtin kept (task,Sty.empty) in
let task,kept = Sty.fold clone_builtin kept (task,Sty.empty) in
task, { tenv_tmp with kept = kept}
......@@ -279,7 +276,7 @@ let decl tenv d =
res
*)
let t env = Trans.on_tagged_ts meta_kept (fun s ->
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)
......
......@@ -104,8 +104,8 @@ let mono_init =
let mono kept =
Trans.decl (d_monomorph ty_base kept (lsmap kept)) mono_init
let t = Trans.on_tagged_ts Encoding.meta_kept (fun tss ->
let kept = Libencoding.get_kept_types tss in
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 () = Encoding.register_enco_poly "decorate" (const t)
......
......@@ -152,8 +152,8 @@ 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_ts Encoding.meta_kept (fun tss ->
let kept = Libencoding.get_kept_types tss in
let monomorph tyb = 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
......
......@@ -441,29 +441,16 @@ let monomorphise_goal =
acc)
let collect_green_part sts =
let extract ts tys =
assert (ts.ts_args = []); (* UnsupportedTySymbol? *)
Mty.add (match ts.ts_def with
| None -> ty_app ts []
| Some ty -> ty) ts tys in
Sts.fold extract sts Mty.empty
(* Some general env creation function *)
let create_env task tenv kept =
let keep = collect_green_part kept in
let projty = Mty.fold (fun ty _ ty_ty ->
let create_env task tenv keep =
let projty = Sty.fold (fun ty ty_ty ->
Mty.add ty ty ty_ty)
keep Mty.empty in
let task = Mty.fold (fun ty ts task ->
let task = Sty.fold (fun ty task ->
let add_ts task ts = add_ty_decl task [ts,Tabstract] in
let task = ty_s_fold add_ts task ty in
let task = add_ts task ts in
task (* the meta is yet here *)) keep task in
let keep = Mty.fold (fun ty _ sty -> Sty.add ty sty) keep Sty.empty in
task,{
task,{
etenv = tenv;
ekeep = keep;
eprojty = projty;
......@@ -492,7 +479,7 @@ let create_trans_complete kept complete =
Trans.fold_map fold_map env init_task
let encoding_instantiate =
Trans.on_tagged_ts meta_kept (fun kept ->
Trans.on_tagged_ty meta_kept (fun kept ->
Trans.on_meta_excl meta_complete (fun complete ->
create_trans_complete kept complete))
......@@ -508,10 +495,7 @@ let find_mono ~only_mono sty f =
ty_add sty ty else sty in
f_ty_fold add sty f
let create_meta_ty ty =
let name = id_fresh "meta_ty" in
let ts = create_tysymbol name [] (Some ty) in
(create_meta meta_kept [MAts ts])
let create_meta_ty ty = create_meta meta_kept [MAty ty]
let create_meta_ty = Wty.memoize 17 create_meta_ty
......@@ -554,51 +538,6 @@ let () =
"mono", mono_in_mono;
"all", mono_in_def]
(* Select array *)
let meta_kept_array = register_meta "encoding : kept_array" [MTtysymbol]
(* select the type array which appear as argument of set and get.
set and get must be in sls *)
let find_mono_array ~only_mono sls sty f =
let add sty ls tyl _ =
match tyl with
| ty::_ when Sls.mem ls sls && is_ty_mono ~only_mono ty ->
Sty.add ty sty
| _ -> sty in
f_app_fold add sty f
let create_meta_ty ty =
let name = id_fresh "meta_ty" in
let ts = create_tysymbol name [] (Some ty) in
(create_meta meta_kept_array [MAts ts])
let create_meta_ty = Wty.memoize 17 create_meta_ty
let create_meta_tyl sty d =
Sty.fold (flip $ cons create_meta_ty) sty [create_decl d]
let mono_in_goal sls pr f =
let sty = (try find_mono_array ~only_mono:true sls Sty.empty f
with Exit -> assert false) (*monomorphise goal should have been used*) in
create_meta_tyl sty (create_prop_decl Pgoal pr f)
let mono_in_goal sls = Trans.tgoal (mono_in_goal sls)
let trans_array th_array =
let set = ns_find_ls th_array.th_export ["set"] in
let get = ns_find_ls th_array.th_export ["get"] in
let sls = Sls.add set (Sls.add get Sls.empty) in
mono_in_goal sls
let trans_array env =
let th_array = Env.find_theory env ["array"] "Array" in
Trans.on_used_theory th_array (fun used ->
if not used then Trans.identity else trans_array th_array)
let () = Trans.register_env_transform "use_builtin_array" trans_array
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. byte"
......
......@@ -204,14 +204,3 @@ 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
(* convert tysymbols tagged with meta_kept to a set of types *)
let get_kept_types tss =
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)
......@@ -47,7 +47,3 @@ 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
(* convert tysymbols tagged with meta_kept to a set of types *)
val get_kept_types : Sts.t -> Sty.t
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