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

whyml: clone algebraic type declarations

parent 7729cc16
......@@ -115,7 +115,7 @@ let syms_expr s _e = s (* TODO *)
let create_ty_decl its =
(* let syms = Util.option_fold syms_ity Sid.empty its.its_def in *)
let news = news_id Sid.empty its.its_pure.ts_name in
let news = Sid.singleton its.its_pure.ts_name in
mk_decl (PDtype its) (*syms*) news
type pre_constructor = preid * (pvsymbol * bool) list
......@@ -124,8 +124,7 @@ type pre_data_decl = itysymbol * pre_constructor list
let create_data_decl tdl =
(* let syms = ref Sid.empty in *)
let add s (its,_) = news_id s its.its_pure.ts_name in
let news = ref (List.fold_left add Sid.empty tdl) in
let news = ref Sid.empty in
let projections = Hid.create 17 in (* id -> plsymbol *)
let build_constructor its (id,al) =
(* check well-formedness *)
......@@ -147,12 +146,12 @@ let create_data_decl tdl =
let tvl = List.map ity_var its.its_args in
let res = vty_value (ity_app its tvl its.its_regs) in
let pls = create_plsymbol ~hidden ~rdonly id vtvs res in
news := Sid.add pls.pl_ls.ls_name !news;
news := news_id !news pls.pl_ls.ls_name;
(* build the projections, if any *)
let build_proj id vtv =
try Hid.find projections id with Not_found ->
let pls = create_plsymbol ~hidden (id_clone id) [res] vtv in
news := Sid.add pls.pl_ls.ls_name !news;
news := news_id !news pls.pl_ls.ls_name;
Hid.add projections id pls;
pls
in
......@@ -165,6 +164,7 @@ let create_data_decl tdl =
in
let build_type (its,cl) =
Hid.clear projections;
news := news_id !news its.its_pure.ts_name;
its, List.map (build_constructor its) cl
in
let tdl = List.map build_type tdl in
......@@ -184,7 +184,7 @@ let new_regs old_vars news vars =
let old_regs = add_regs old_vars.vars_reg Sreg.empty in
let regs = add_regs vars.vars_reg Sreg.empty in
let regs = Sreg.diff regs old_regs in
Sreg.fold (fun r acc -> Sid.add r.reg_name acc) regs news
Sreg.fold (fun r s -> news_id s r.reg_name) regs news
let create_let_decl ld =
let vars = vars_merge ld.let_expr.e_varm vars_empty in
......@@ -201,7 +201,8 @@ let create_let_decl ld =
mk_decl (PDlet ld) (*syms*) news
let create_rec_decl ({ rec_defn = rdl } as d) =
let add_rd s { fun_ps = p } = check_vars p.ps_vars; news_id s p.ps_name in
let add_rd s { fun_ps = p } =
check_vars p.ps_vars; news_id s p.ps_name in
let news = List.fold_left add_rd Sid.empty rdl in
(*
let add_rd syms { rec_ps = ps; rec_lambda = l; rec_vars = vm } =
......@@ -238,6 +239,25 @@ let create_exn_decl xs =
*)
mk_decl (PDexn xs) (*syms*) news
(** {2 Cloning} *)
let clone_data_decl sm pd = match pd.pd_node with
| PDdata tdl ->
let news = ref Sid.empty in
let add_pl pl =
let pl = Mls.find pl.pl_ls sm.sm_pls in
news := news_id !news pl.pl_ls.ls_name;
pl in
let add_cs (cs,pjl) =
add_pl cs, List.map (Util.option_map add_pl) pjl in
let add_td (its,csl) =
let its = Mits.find its sm.sm_its in
news := news_id !news its.its_pure.ts_name;
its, List.map add_cs csl in
let tdl = List.map add_td tdl in
mk_decl (PDdata tdl) (*!syms*) !news
| _ -> invalid_arg "Mlw_decl.clone_data_decl"
(** {2 Known identifiers} *)
type known_map = pdecl Mid.t
......
......@@ -66,6 +66,10 @@ val create_rec_decl : rec_defn -> pdecl
val create_exn_decl : xsymbol -> pdecl
(** {2 Cloning} *)
val clone_data_decl : Mlw_expr.symbol_map -> pdecl -> pdecl
(** {2 Known identifiers} *)
type known_map = pdecl Mid.t
......
......@@ -40,6 +40,21 @@ type plsymbol = {
let pl_equal : plsymbol -> plsymbol -> bool = (==)
let create_plsymbol_unsafe, restore_pl =
let ls_to_pls = Wls.create 17 in
(fun ls args value effect ~hidden ~rdonly ->
let pl = {
pl_ls = ls;
pl_args = args;
pl_value = value;
pl_effect = effect;
pl_hidden = hidden;
pl_rdonly = rdonly;
} in
Wls.set ls_to_pls ls pl;
pl),
Wls.find ls_to_pls
let create_plsymbol ?(hidden=false) ?(rdonly=false) id args value =
let ty_of_vtv vtv = ty_of_ity vtv.vtv_ity in
let pure_args = List.map ty_of_vtv args in
......@@ -47,14 +62,8 @@ let create_plsymbol ?(hidden=false) ?(rdonly=false) id args value =
let eff_read e r = eff_read e ~ghost:value.vtv_ghost r in
let effect = Util.option_fold eff_read eff_empty value.vtv_mut in
let arg_reset acc a = Util.option_fold eff_reset acc a.vtv_mut in
let effect = List.fold_left arg_reset effect args in {
pl_ls = ls;
pl_args = args;
pl_value = value;
pl_effect = effect;
pl_hidden = hidden;
pl_rdonly = rdonly;
}
let effect = List.fold_left arg_reset effect args in
create_plsymbol_unsafe ls args value effect ~hidden ~rdonly
let ity_of_ty_opt ty = ity_of_ty (Util.def_option ty_bool ty)
......@@ -69,6 +78,69 @@ let fake_pls = Wls.memoize 17 (fun ls ->
exception HiddenPLS of lsymbol
exception RdOnlyPLS of lsymbol
(** cloning *)
type symbol_map = {
sm_pure : Theory.symbol_map;
sm_its : itysymbol Mits.t;
sm_pls : plsymbol Mls.t;
}
let pl_clone sm =
let itsm, regm = its_clone sm in
let conv_reg r = Mreg.find r regm in
let conv_its its = Mits.find_def its its itsm in
let conv_ts ts = Mts.find_def ts ts sm.Theory.sm_ts in
let rec conv_ity ity = match ity.ity_node with
| Ityapp (its,tl,rl) ->
let tl = List.map conv_ity tl in
let rl = List.map conv_reg rl in
ity_app (conv_its its) tl rl
| Itypur (ts,tl) ->
let tl = List.map conv_ity tl in
ity_pur (conv_ts ts) tl
| Ityvar _ -> ity
in
let conv_vtv v =
let ghost = v.vtv_ghost in
let mut, ity = match v.vtv_mut with
| Some r -> let r = conv_reg r in Some r, r.reg_ity
| None -> None, conv_ity v.vtv_ity in
vty_value ~ghost ?mut ity
in
let conv_eff eff =
let e = eff_empty in
assert (Sexn.is_empty eff.eff_raises);
assert (Sexn.is_empty eff.eff_ghostx);
let conv fn r e = fn e (conv_reg r) in
let e = Sreg.fold (conv (eff_read ~ghost:false)) eff.eff_reads e in
let e = Sreg.fold (conv (eff_write ~ghost:false)) eff.eff_writes e in
let e = Sreg.fold (conv (eff_read ~ghost:true)) eff.eff_ghostr e in
let e = Sreg.fold (conv (eff_write ~ghost:true)) eff.eff_ghostw e in
let conv r u e = match u with
| Some u -> eff_refresh e (conv_reg r) (conv_reg u)
| None -> eff_reset e (conv_reg r) in
Mreg.fold conv eff.eff_resets e
in
let add_pl opls nls acc =
let npls = try restore_pl nls with Not_found ->
let args = List.map conv_vtv opls.pl_args in
let value = conv_vtv opls.pl_value in
let effect = conv_eff opls.pl_effect in
let hidden = opls.pl_hidden in
let rdonly = opls.pl_rdonly in
create_plsymbol_unsafe nls args value effect ~hidden ~rdonly
in
Mls.add opls.pl_ls npls acc
in
let add_ls ols nls acc =
try add_pl (restore_pl ols) nls acc with Not_found -> acc
in
let plsm = Mls.fold add_ls sm.Theory.sm_ls Mls.empty in
{ sm_pure = sm;
sm_its = itsm;
sm_pls = plsm; }
(** patterns *)
type ppattern = {
......
......@@ -55,6 +55,16 @@ val create_plsymbol : ?hidden:bool -> ?rdonly:bool ->
exception HiddenPLS of lsymbol
exception RdOnlyPLS of lsymbol
(** cloning *)
type symbol_map = private {
sm_pure : Theory.symbol_map;
sm_its : itysymbol Mits.t;
sm_pls : plsymbol Mls.t;
}
val pl_clone : Theory.symbol_map -> symbol_map
(** patterns *)
type ppattern = private {
......
......@@ -353,21 +353,31 @@ let clone_export uc m inst =
let sm = match Theory.get_rev_decls nth with
| { td_node = Clone (_,sm) } :: _ -> sm
| _ -> assert false in
let itsm = its_clone sm in
let psm = pl_clone sm in
let conv_its its = Mits.find_def its its psm.sm_its in
let conv_ts ts = Mts.find_def ts ts sm.Theory.sm_ts in
let psh = Hid.create 3 in
let find_ps def id = try Hid.find psh id with Not_found -> def in
let add_pdecl uc d = { uc with
muc_decls = d :: uc.muc_decls;
muc_known = known_add_decl (Theory.get_known uc.muc_theory) uc.muc_known d;
muc_local = Sid.union uc.muc_local d.pd_news }
in
muc_local = Sid.union uc.muc_local d.pd_news } in
let add_pd uc pd = match pd.pd_node with
| PDtype its ->
let its = Mits.find its itsm in
add_pdecl uc (create_ty_decl its)
| PDdata _dl -> assert false (* TODO *)
add_pdecl uc (create_ty_decl (conv_its its))
| PDdata _ ->
add_pdecl uc (clone_data_decl psm pd)
| PDexn xs ->
let rec conv_ity ity = match ity.ity_node with
| Ityapp (s,tl,[]) -> ity_app (conv_its s) (List.map conv_ity tl) []
| Itypur (s,tl) -> ity_pur (conv_ts s) (List.map conv_ity tl)
| Ityapp _ | Ityvar _ -> assert false (* can't happen *) in
let nxs = create_xsymbol (id_clone xs.xs_name) (conv_ity xs.xs_ity) in
Hid.add psh xs.xs_name (XS nxs);
add_pdecl uc (create_exn_decl nxs)
| PDval _lv -> assert false (* TODO *)
| PDlet _ld -> assert false (* TODO *)
| PDrec _rd -> assert false (* TODO *)
| PDexn _xs -> assert false (* TODO *)
in
let uc = { uc with
muc_known = merge_known uc.muc_known (Mid.set_diff m.mod_known m.mod_local);
......@@ -380,19 +390,16 @@ let clone_export uc m inst =
| LS ls -> not (Mls.mem ls inst.inst_ls)
| _ -> true in
let f_ts = function
| TS ts -> TS (Mts.find_def ts ts sm.sm_ts)
| PT pt -> PT (Mits.find_def pt pt itsm)
in
let f_ps = function
| LS ls -> LS (Mls.find_def ls ls sm.sm_ls)
| TS ts -> TS (Mts.find_def ts ts sm.Theory.sm_ts)
| PT pt -> PT (Mits.find_def pt pt psm.sm_its) in
let f_ps ps = match ps with
| LS ls -> LS (Mls.find_def ls ls sm.Theory.sm_ls)
| PV _ as x -> x (* TODO *)
| PS _ as x -> x (* TODO *)
| PL _ as x -> x (* TODO *)
| XS _ as x -> x (* TODO *)
in
| PL pl -> PL (Mls.find_def pl pl.pl_ls psm.sm_pls)
| XS xs -> find_ps ps xs.xs_name in
let rec f_ns ns = {
ns_ts = Mstr.map f_ts (Mstr.filter g_ts ns.ns_ts);
ns_ps = Mstr.map f_ps (Mstr.filter g_ps ns.ns_ps);
ns_ns = Mstr.map f_ns ns.ns_ns; }
in
ns_ns = Mstr.map f_ns ns.ns_ns; } in
add_to_module uc nth (f_ns m.mod_export)
......@@ -514,7 +514,8 @@ let its_clone sm =
with Not_found -> ()
in
Mts.iter add_ts sm.Theory.sm_ts;
Hits.fold Mits.add itsh Mits.empty
Hits.fold Mits.add itsh Mits.empty,
Hreg.fold Mreg.add regh Mreg.empty
(** computation types (with effects) *)
......
......@@ -127,7 +127,7 @@ val ity_s_fold :
val ity_s_all : (itysymbol -> bool) -> (tysymbol -> bool) -> ity -> bool
val ity_s_any : (itysymbol -> bool) -> (tysymbol -> bool) -> ity -> bool
val its_clone : Theory.symbol_map -> itysymbol Mits.t
val its_clone : Theory.symbol_map -> itysymbol Mits.t * region Mreg.t
(* traversal functions on type variables and regions *)
......
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