From 17260fb40802652c2ac0d2d7efdfbcb6b80228cd Mon Sep 17 00:00:00 2001 From: Andrei Paskevich Date: Wed, 19 Aug 2015 20:58:09 +0200 Subject: [PATCH] Pmodule: clone type definitions --- src/mlw/pmodule.ml | 159 +++++++++++++++++++++++++++++++++++++++------ 1 file changed, 139 insertions(+), 20 deletions(-) diff --git a/src/mlw/pmodule.ml b/src/mlw/pmodule.ml index a38bbddde..286f2516b 100644 --- a/src/mlw/pmodule.ml +++ b/src/mlw/pmodule.ml @@ -462,14 +462,34 @@ let cl_find_xs cl xs = let cl_clone_ls inst cl ls = if Mls.mem ls inst.inst_ls then raise (CannotInstantiate ls.ls_name); let constr = ls.ls_constr in - let id = id_clone ls.ls_name in + let id = id_clone ls.ls_name in let at = List.map (cl_trans_ty cl) ls.ls_args in let vt = Opt.map (cl_trans_ty cl) ls.ls_value in let ls' = create_lsymbol ~constr id at vt in cl.ls_table <- Mls.add ls ls' cl.ls_table; ls' -let cl_add_ls cl ({ls_name = id} as ls) ls' = +let cl_init_ty cl ({ts_name = id} as ts) ty = + let rec restore_ity ty = match ty.ty_node with + | Tyapp (s,tl) -> + ity_app_fresh (restore_its s) (List.map restore_ity tl) + | Tyvar v -> ity_var v in + let its = restore_its ts and ity = restore_ity ty 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_impure its || not ity.ity_pure 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 + if not (Sid.mem id cl.cl_local) then raise (NonLocal id); + if List.length ts.ts_args <> List.length ts'.ts_args || + its_impure its || its_impure its' then raise (BadInstance id); + cl.ts_table <- Mts.add its.its_ts its' cl.ts_table + +let cl_init_ls cl ({ls_name = id} as ls) ls' = + if not (Sid.mem id cl.cl_local) then raise (NonLocal id); let mtch sb ty ty' = try ty_match sb ty' (cl_trans_ty cl ty) with TypeMismatch _ -> raise (BadInstance id) in let sbs = match ls.ls_value,ls'.ls_value with @@ -480,23 +500,23 @@ let cl_add_ls cl ({ls_name = id} as ls) ls' = with Invalid_argument _ -> raise (BadInstance id)); cl.ls_table <- Mls.add ls ls' cl.ls_table -let cl_found_ls inst cl uc ls = - let nls = match Mls.find_opt ls inst.inst_ls with - | None -> - let ns = Theory.get_namespace uc.muc_theory in - (try Some (ns_find_ls ns [ls.ls_name.id_string]) - with Not_found -> None) - | nls -> nls in - match nls with - | Some ls' -> cl_add_ls cl ls ls'; true - | None -> false +let cl_init_pr cl {pr_name = id} _ = + if not (Sid.mem id cl.cl_local) then raise (NonLocal 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; + cl (* clone declarations *) let clone_decl inst cl uc d = match d.d_node with | Dtype _ | Ddata _ -> assert false (* impossible *) | Dparam ls -> - if cl_found_ls inst cl uc ls then uc else + if Mls.mem ls inst.inst_ls then uc else let d = create_param_decl (cl_clone_ls inst cl ls) in add_pdecl ~vc:false uc (create_pure_decl d) | Dlogic ldl -> @@ -530,7 +550,111 @@ let clone_decl inst cl uc d = match d.d_node with let d = create_prop_decl k' pr' (cl_trans_fmla cl f) in add_pdecl ~vc:false uc (create_pure_decl d) -let clone_type_decl _inst _cl _tdl = assert false +let clone_type_decl inst cl tdl = + let def = + List.fold_left (fun m d -> Mits.add d.itd_its d m) Mits.empty tdl in + let htd = Hits.create 5 in + + let rec visit alg ({its_ts = {ts_name = id} as ts} as s) d = + 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 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_rs o n = + cl.rs_table <- Mrs.add o n cl.rs_table; + match o.rs_logic, n.rs_logic with + | RLls o, RLls n -> cl.ls_table <- Mls.add o n cl.ls_table; + | RLnone, RLnone -> () (* constructors with invariants *) + | _ -> assert false in + let save_itd itd = + List.iter2 save_rs d.itd_constructors itd.itd_constructors; + List.iter2 save_rs d.itd_fields itd.itd_fields; + Hits.add htd s (Some itd) in + (* alias *) + if s.its_def <> None then begin + if cloned then raise (CannotInstantiate id); + let def = conv_ity alg (Opt.get s.its_def) in + let itd = create_alias_decl id' ts.ts_args def in + cl.ts_table <- Mts.add ts itd.itd_its cl.ts_table; + save_itd itd + end else + (* abstract *) + if d.itd_fields = [] && d.itd_constructors = [] && + d.itd_invariant = [] then begin + if cloned then Hits.add htd s None else begin + let itd = create_abstract_type_decl id' ts.ts_args s.its_privmut in + cl.ts_table <- Mts.add ts itd.itd_its cl.ts_table; + save_itd itd + end + end else + (* variant *) + if s.its_mfields = [] && d.itd_constructors <> [] && + d.itd_invariant = [] then begin + if cloned then raise (CannotInstantiate id); + let conv_fd m fd = + let v = Opt.get fd.rs_field in Mpv.add v (conv_pj v) m in + let fldm = List.fold_left conv_fd Mpv.empty d.itd_fields in + let conv_pj pj = match Mpv.find_opt pj fldm with + | Some pj' -> true, pj' | None -> false, conv_pj pj in + let conv_cs cs = + id_clone cs.rs_name, List.map conv_pj cs.rs_cty.cty_args in + let csl = List.map conv_cs d.itd_constructors in + match Mts.find_opt ts cl.ts_table with + | Some s' -> + let itd = create_rec_variant_decl s' csl in + save_itd itd + | None -> + let itd = create_flat_variant_decl id' ts.ts_args csl in + cl.ts_table <- Mts.add ts itd.itd_its cl.ts_table; + save_itd itd + end else begin + (* flat record *) + if cloned then raise (CannotInstantiate id); + let mfld = Spv.of_list s.its_mfields in + let priv = d.itd_constructors = [] in + let mut = its_mutable s in + let pjl = List.map (fun fd -> Opt.get fd.rs_field) d.itd_fields in + let fdl = List.map (fun v -> Spv.mem v mfld, conv_pj v) pjl in + let inv = + if d.itd_invariant = [] then [] else + if d.itd_fields = [] then + List.map (cl_trans_fmla cl) d.itd_invariant else + let ovl = List.map (fun v -> v.pv_vs) pjl in + let nvl = List.map (fun (_,v) -> t_var v.pv_vs) fdl in + let conv_inv f = + let f = t_exists_close ovl [] f in + match (cl_trans_fmla cl f).t_node with + | Tquant (Texists, tq) -> + let xvl,_,f = t_open_quant tq in + let add s xv nv = Mvs.add xv nv s in + t_subst (List.fold_left2 add Mvs.empty xvl nvl) f + | _ -> assert false (* can't be *) in + List.map conv_inv d.itd_invariant in + let itd = create_flat_record_decl id' ts.ts_args priv mut fdl inv in + cl.ts_table <- Mts.add ts itd.itd_its cl.ts_table; + save_itd itd + end + + and conv_ity alg ity = + let rec down ity = match ity.ity_node with + | Ityreg {reg_its = s; reg_args = tl} + | Ityapp (s,tl,_) | Itypur (s,tl) -> + if Sits.mem s alg then begin + if not (Mts.mem s.its_ts cl.ts_table) then + let id = id_clone s.its_ts.ts_name in + let s = create_itysymbol_pure id s.its_ts.ts_args in + cl.ts_table <- Mts.add s.its_ts s cl.ts_table + end else Opt.iter (visit alg s) (Mits.find_opt s def); + List.iter down tl + | Ityvar _ -> () in + down ity; + cl_trans_ity cl ity in + + Mits.iter (visit Sits.empty) def; + Lists.map_filter (fun d -> Hits.find htd d.itd_its) tdl + let clone_pdecl inst cl uc d = match d.pd_node with | PDtype tdl -> let tdl = clone_type_decl inst cl tdl in @@ -559,12 +683,7 @@ let add_clone uc mi = muc_units = Uclone mi :: uc.muc_units } let clone_export uc m inst = - let check_local id = - if not (Sid.mem id m.mod_local) then raise (NonLocal id) in - Mts.iter (fun ts _ -> check_local ts.ts_name) inst.inst_ts; - Mls.iter (fun ls _ -> check_local ls.ls_name) inst.inst_ls; - Mpr.iter (fun pr _ -> check_local pr.pr_name) inst.inst_pr; - let cl = empty_clones m in + let cl = cl_init m inst in let rec add_unit uc u = match u with | Udecl d -> clone_pdecl inst cl uc d | Uuse m -> use_export uc m -- 2.24.1