From d02c17b3faf6ef8822c6ce9c3bb24bce2b99caef Mon Sep 17 00:00:00 2001 From: Jean-Christophe Filliatre Date: Tue, 14 Feb 2017 11:40:03 +0100 Subject: [PATCH] use mod_inst in module cloning --- src/mlw/pinterp.ml | 2 +- src/mlw/pmodule.ml | 41 ++++++++++++++++++++---------- src/mlw/pmodule.mli | 5 +++- src/parser/typing.ml | 59 ++++++++++++++++++++++---------------------- 4 files changed, 63 insertions(+), 44 deletions(-) diff --git a/src/mlw/pinterp.ml b/src/mlw/pinterp.ml index f8cae6f01..5dba33372 100644 --- a/src/mlw/pinterp.ml +++ b/src/mlw/pinterp.ml @@ -22,7 +22,7 @@ open Ity open Expr -module Nummap = Map.Make(BigInt) +(* module Nummap = Map.Make(BigInt) *) type value = | Vconstr of rsymbol * field list diff --git a/src/mlw/pmodule.ml b/src/mlw/pmodule.ml index 956b66081..f44dfe1cd 100644 --- a/src/mlw/pmodule.ml +++ b/src/mlw/pmodule.ml @@ -113,11 +113,24 @@ and mod_inst = { mi_ts : itysymbol Mts.t; mi_ls : lsymbol Mls.t; mi_pr : prsymbol Mpr.t; + mi_pk : prop_kind Mpr.t; mi_pv : pvsymbol Mvs.t; mi_rs : rsymbol Mrs.t; mi_xs : xsymbol Mexn.t; } +let empty_mod_inst m = { + mi_mod = m; + mi_ty = Mts.empty; + mi_ts = Mts.empty; + mi_ls = Mls.empty; + mi_pr = Mpr.empty; + mi_pk = Mpr.empty; + mi_pv = Mvs.empty; + mi_rs = Mrs.empty; + mi_xs = Mexn.empty; +} + (** {2 Module under construction} *) type pmodule_uc = { @@ -456,7 +469,7 @@ let cl_find_xs cl xs = else Mexn.find xs cl.xs_table let clone_ls inst cl ls = - if Mls.mem ls inst.inst_ls then raise (CannotInstantiate ls.ls_name); + if Mls.mem ls inst.mi_ls then raise (CannotInstantiate ls.ls_name); let constr = ls.ls_constr in let id = id_clone ls.ls_name in let at = List.map (clone_ty cl) ls.ls_args in @@ -465,16 +478,16 @@ let clone_ls inst cl ls = cl.ls_table <- Mls.add ls ls' cl.ls_table; ls' -let cl_init_ty cl ({ts_name = id} as ts) ty = - let its = restore_its ts and ity = ity_of_ty ty in +let cl_init_ty cl ({ts_name = id} as ts) ity = + let its = restore_its ts in if not (Sid.mem id cl.cl_local) then raise (NonLocal id); let stv = Stv.of_list ts.ts_args in if not (Stv.subset (ity_freevars Stv.empty ity) stv && its_pure its && ity_immutable ity) then raise (BadInstance id); cl.ty_table <- Mts.add ts ity cl.ty_table -let cl_init_ts cl ({ts_name = id} as ts) ts' = - let its = restore_its ts and its' = restore_its ts' in +let cl_init_ts cl ({ts_name = id} as ts) its' = + let its = restore_its ts and ts' = its'.its_ts in if not (Sid.mem id cl.cl_local) then raise (NonLocal id); if not (List.length ts.ts_args = List.length ts'.ts_args && its_pure its && its_pure its') then raise (BadInstance id); @@ -497,10 +510,10 @@ let cl_init_pr cl {pr_name = id} _ = let cl_init m inst = let cl = empty_clones m in - Mts.iter (cl_init_ty cl) inst.inst_ty; - Mts.iter (cl_init_ts cl) inst.inst_ts; - Mls.iter (cl_init_ls cl) inst.inst_ls; - Mpr.iter (cl_init_pr cl) inst.inst_pr; + Mts.iter (cl_init_ty cl) inst.mi_ty; + Mts.iter (cl_init_ts cl) inst.mi_ts; + Mls.iter (cl_init_ls cl) inst.mi_ls; + Mpr.iter (cl_init_pr cl) inst.mi_pk; cl (* clone declarations *) @@ -508,7 +521,7 @@ let cl_init m inst = let clone_decl inst cl uc d = match d.d_node with | Dtype _ | Ddata _ -> assert false (* impossible *) | Dparam ls -> - if Mls.mem ls inst.inst_ls then uc else + if Mls.mem ls inst.mi_ls then uc else let d = create_param_decl (clone_ls inst cl ls) in add_pdecl ~vc:false uc (create_pure_decl d) | Dlogic ldl -> @@ -521,7 +534,7 @@ let clone_decl inst cl uc d = match d.d_node with | Dind (s, idl) -> let get_ls (ls,_) = clone_ls inst cl ls in let get_case (pr,f) = - if Mpr.mem pr inst.inst_pr then raise (CannotInstantiate pr.pr_name); + if Mpr.mem pr inst.mi_pk then raise (CannotInstantiate pr.pr_name); let pr' = create_prsymbol (id_clone pr.pr_name) in cl.pr_table <- Mpr.add pr pr' cl.pr_table; pr', clone_fmla cl f in @@ -530,7 +543,7 @@ let clone_decl inst cl uc d = match d.d_node with let d = create_ind_decl s (List.map2 get_ind lls idl) in add_pdecl ~vc:false uc (create_pure_decl d) | Dprop (k,pr,f) -> - let skip, k' = match k, Mpr.find_opt pr inst.inst_pr with + let skip, k' = match k, Mpr.find_opt pr inst.mi_pk with | Pgoal, _ -> true, Pgoal | Plemma, Some Pgoal -> true, Pgoal | Plemma, _ -> false, Plemma @@ -567,7 +580,7 @@ let clone_type_decl inst cl tdl = if not (Hits.mem htd s) then let alg = Sits.add s alg in let id' = id_clone id in - let cloned = Mts.mem ts inst.inst_ts || Mts.mem ts inst.inst_ty in + let cloned = Mts.mem ts inst.mi_ts || Mts.mem ts inst.mi_ty in let conv_pj v = create_pvsymbol (id_clone v.pv_vs.vs_name) ~ghost:v.pv_ghost (conv_ity alg v.pv_ity) in let save_itd itd = @@ -896,6 +909,7 @@ let clone_export uc m inst = mi_ts = Mts.map (cl_find_its cl) mi.mi_ts; mi_ls = Mls.map (cl_find_ls cl) mi.mi_ls; mi_pr = Mpr.map (cl_find_pr cl) mi.mi_pr; + mi_pk = mi.mi_pk; mi_pv = Mvs.map (cl_find_pv cl) mi.mi_pv; mi_rs = Mrs.map (cl_find_rs cl) mi.mi_rs; mi_xs = Mexn.map (cl_find_xs cl) mi.mi_xs} @@ -919,6 +933,7 @@ let clone_export uc m inst = mi_ts = cl.ts_table; mi_ls = cl.ls_table; mi_pr = cl.pr_table; + mi_pk = inst.mi_pk; mi_pv = cl.pv_table; mi_rs = cl.rs_table; mi_xs = cl.xs_table} in diff --git a/src/mlw/pmodule.mli b/src/mlw/pmodule.mli index ea61b4a10..7b2067769 100644 --- a/src/mlw/pmodule.mli +++ b/src/mlw/pmodule.mli @@ -66,11 +66,14 @@ and mod_inst = { mi_ts : itysymbol Mts.t; mi_ls : lsymbol Mls.t; mi_pr : prsymbol Mpr.t; + mi_pk : prop_kind Mpr.t; mi_pv : pvsymbol Mvs.t; mi_rs : rsymbol Mrs.t; mi_xs : xsymbol Mexn.t; } +val empty_mod_inst: pmodule -> mod_inst + (** {2 Module under construction} *) type pmodule_uc = private { @@ -106,7 +109,7 @@ val restore_module : theory -> pmodule val use_export : pmodule_uc -> pmodule -> pmodule_uc -val clone_export : pmodule_uc -> pmodule -> Theory.th_inst -> pmodule_uc +val clone_export : pmodule_uc -> pmodule -> mod_inst -> pmodule_uc (** {2 Logic decls} *) diff --git a/src/parser/typing.ml b/src/parser/typing.ml index bb840457b..6da04ccf5 100644 --- a/src/parser/typing.ml +++ b/src/parser/typing.ml @@ -997,62 +997,63 @@ let find_module env file q = if Debug.test_flag Glob.flag then Glob.use (qloc_last q) m.mod_theory.th_name; m -let type_inst ({muc_theory = tuc} as _muc) {mod_theory = t} s = +let type_inst ({muc_theory = tuc} as muc) ({mod_theory = t} as m) s = let add_inst s = function | CStsym (p,[],PTtyapp (q,[])) -> let ts1 = find_tysymbol_ns t.th_export p in - let ts2 = find_tysymbol tuc q in - if Mts.mem ts1 s.inst_ty then Loc.error ~loc:(qloc p) + let ts2 = find_itysymbol muc q in + if Mts.mem ts1 s.mi_ty then Loc.error ~loc:(qloc p) (ClashSymbol ts1.ts_name.id_string); - { s with inst_ts = Loc.try4 ~loc:(qloc p) Mts.add_new - (ClashSymbol ts1.ts_name.id_string) ts1 ts2 s.inst_ts } + { s with mi_ts = Loc.try4 ~loc:(qloc p) Mts.add_new + (ClashSymbol ts1.ts_name.id_string) ts1 ts2 s.mi_ts } | CStsym (p,tvl,pty) -> let ts1 = find_tysymbol_ns t.th_export p in let tvl = List.map (fun id -> tv_of_string id.id_str) tvl in - let ts2 = Loc.try3 ~loc:(qloc p) create_tysymbol - (id_clone ts1.ts_name) tvl (Some (ty_of_pty tuc pty)) in - let ty2 = ty_app ts2 (List.map ty_var ts1.ts_args) in - let check v ty = match ty.ty_node with - | Tyvar u -> tv_equal u v | _ -> false in - begin match ty2.ty_node with - | Tyapp (ts2, tyl) when Lists.equal check tvl tyl -> - if Mts.mem ts1 s.inst_ty then Loc.error ~loc:(qloc p) + let ts2 = Loc.try3 ~loc:(qloc p) create_alias_itysymbol + (id_clone ts1.ts_name) tvl (ity_of_pty muc pty) in + let ty2 = ity_app ts2 (List.map ity_var ts1.ts_args) [] in + let check v ty = match ty.ity_node with + | Ityvar (u, _) -> tv_equal u v | _ -> false in + begin match ty2.ity_node with + | Ityapp (ts2, tyl, _) | Ityreg { reg_its = ts2; reg_args = tyl } + when Lists.equal check tvl tyl -> + if Mts.mem ts1 s.mi_ty then Loc.error ~loc:(qloc p) (ClashSymbol ts1.ts_name.id_string); - { s with inst_ts = Loc.try4 ~loc:(qloc p) Mts.add_new - (ClashSymbol ts1.ts_name.id_string) ts1 ts2 s.inst_ts } + { s with mi_ts = Loc.try4 ~loc:(qloc p) Mts.add_new + (ClashSymbol ts1.ts_name.id_string) ts1 ts2 s.mi_ts } | _ -> - if Mts.mem ts1 s.inst_ts then Loc.error ~loc:(qloc p) + if Mts.mem ts1 s.mi_ts then Loc.error ~loc:(qloc p) (ClashSymbol ts1.ts_name.id_string); - { s with inst_ty = Loc.try4 ~loc:(qloc p) Mts.add_new - (ClashSymbol ts1.ts_name.id_string) ts1 ty2 s.inst_ty } + { s with mi_ty = Loc.try4 ~loc:(qloc p) Mts.add_new + (ClashSymbol ts1.ts_name.id_string) ts1 ty2 s.mi_ty } end | CSfsym (p,q) -> let ls1 = find_fsymbol_ns t.th_export p in let ls2 = find_fsymbol tuc q in - { s with inst_ls = Loc.try4 ~loc:(qloc p) Mls.add_new - (ClashSymbol ls1.ls_name.id_string) ls1 ls2 s.inst_ls } + { s with mi_ls = Loc.try4 ~loc:(qloc p) Mls.add_new + (ClashSymbol ls1.ls_name.id_string) ls1 ls2 s.mi_ls } | CSpsym (p,q) -> let ls1 = find_psymbol_ns t.th_export p in let ls2 = find_psymbol tuc q in - { s with inst_ls = Loc.try4 ~loc:(qloc p) Mls.add_new - (ClashSymbol ls1.ls_name.id_string) ls1 ls2 s.inst_ls } + { s with mi_ls = Loc.try4 ~loc:(qloc p) Mls.add_new + (ClashSymbol ls1.ls_name.id_string) ls1 ls2 s.mi_ls } | CSvsym (p,_) -> Loc.errorm ~loc:(qloc p) "program symbol instantiation is not supported yet" (* TODO *) | CSaxiom p -> let pr = find_prop_ns t.th_export p in - { s with inst_pr = Loc.try4 ~loc:(qloc p) Mpr.add_new - (ClashSymbol pr.pr_name.id_string) pr Paxiom s.inst_pr } + { s with mi_pk = Loc.try4 ~loc:(qloc p) Mpr.add_new + (ClashSymbol pr.pr_name.id_string) pr Paxiom s.mi_pk } | CSlemma p -> let pr = find_prop_ns t.th_export p in - { s with inst_pr = Loc.try4 ~loc:(qloc p) Mpr.add_new - (ClashSymbol pr.pr_name.id_string) pr Plemma s.inst_pr } + { s with mi_pk = Loc.try4 ~loc:(qloc p) Mpr.add_new + (ClashSymbol pr.pr_name.id_string) pr Plemma s.mi_pk } | CSgoal p -> let pr = find_prop_ns t.th_export p in - { s with inst_pr = Loc.try4 ~loc:(qloc p) Mpr.add_new - (ClashSymbol pr.pr_name.id_string) pr Pgoal s.inst_pr } + { s with mi_pk = Loc.try4 ~loc:(qloc p) Mpr.add_new + (ClashSymbol pr.pr_name.id_string) pr Pgoal s.mi_pk } in - List.fold_left add_inst empty_inst s + List.fold_left add_inst (empty_mod_inst m) s let add_decl muc env file d = let vc = muc.muc_theory.uc_path = [] && -- 2.24.1