diff --git a/src/mlw/pmodule.ml b/src/mlw/pmodule.ml index 49373ca40a0ffc01dc287f3bf3e8d19e3b78faeb..2832b7628fb125291476968f761a29e2cfe621b2 100644 --- a/src/mlw/pmodule.ml +++ b/src/mlw/pmodule.ml @@ -525,45 +525,47 @@ let rec clone_ity cl ity = match ity.ity_node with | Ityreg r -> ity_reg (clone_reg cl r) | Ityapp (s, tl, rl) -> - let tl = List.map (clone_ity cl) tl in - let rl = List.map (clone_ity cl) rl in + let tl' = List.map (clone_ity cl) tl in begin match Mts.find_opt s.its_ts cl.ts_table with - | Some its -> ity_app_pure its tl rl + | Some s' -> ity_app_pure s' tl' (clone_regs cl s tl rl s') | None -> (* creative indentation *) begin match Mts.find_opt s.its_ts cl.ty_table with - | Some ity -> ity_full_inst (its_match_regs s tl rl) ity - | None -> ity_app_pure s tl rl + | Some ity -> ity_full_inst (its_match_regs s tl' []) ity + | None -> ity_app_pure s tl' (List.map (clone_ity cl) rl) end end | Ityvar _ -> ity and clone_reg cl reg = - (* FIXME: what about top-level non-instantiated regions? - We cannot check in cl.cl_local to see if they are there. - Instead, we should prefill cl.pv_table and cl.rn_table - with all top-level pvsymbols (local or external) before - descending into a let_defn. - TODO: add to module/uc a list of locally-defined toplevel - variables, as well as a set of imported toplevel variables. *) try Mreg.find reg cl.rn_table with Not_found -> - let tl = List.map (clone_ity cl) reg.reg_args in - let rl = List.map (clone_ity cl) reg.reg_regs in - let r = match Mts.find_opt reg.reg_its.its_ts cl.ts_table with - | Some its -> - create_region (id_clone reg.reg_name) its tl rl - | None -> (* creative indentation *) - begin match Mts.find_opt reg.reg_its.its_ts cl.ty_table with - | Some {ity_node = Ityreg r} -> - let sbs = its_match_regs reg.reg_its tl rl in - let tl = List.map (ity_full_inst sbs) r.reg_args in - let rl = List.map (ity_full_inst sbs) r.reg_regs in - create_region (id_clone reg.reg_name) r.reg_its tl rl - | Some _ -> assert false - | None -> - create_region (id_clone reg.reg_name) reg.reg_its tl rl - end in + let tl' = List.map (clone_ity cl) reg.reg_args in + let s',rl' = match Mts.find_opt reg.reg_its.its_ts cl.ts_table with + | Some s' -> s', clone_regs cl reg.reg_its reg.reg_args reg.reg_regs s' + | None -> reg.reg_its, List.map (clone_ity cl) reg.reg_regs in + let r = create_region (id_clone reg.reg_name) s' tl' rl' in cl.rn_table <- Mreg.add reg r cl.rn_table; r +and clone_regs cl s tl rl s' = + if rl = [] then [] else + let base = its_match_regs s tl rl in + let add sbs pj = + let ity = clone_ity cl (ity_full_inst base pj.pv_ity) in + ity_match sbs (Mpv.find pj cl.fd_table).pv_ity ity in + let sbs = List.fold_left add isb_empty s.its_mfields in + let sbs = List.fold_left add sbs s.its_ofields in + let rec inst ity = + if ity.ity_pure then ity_full_inst sbs ity else + match ity.ity_node with + | Ityreg r when Mreg.mem r sbs.isb_reg -> + Mreg.find r sbs.isb_reg + | Ityreg {reg_its = s; reg_args = tl; reg_regs = rl} -> + ity_app s (List.map inst tl) (List.map inst rl) + | Ityapp (s,tl,rl) -> + ity_app_pure s (List.map inst tl) (List.map inst rl) + | Ityvar v -> + Mtv.find v sbs.isb_var in + List.map (fun reg -> inst (ity_reg reg)) s'.its_regions + let cl_find_ls cl ls = if not (Sid.mem ls.ls_name cl.cl_local) then ls else Mls.find ls cl.ls_table @@ -596,11 +598,15 @@ let cl_init m inst = Mts.iter (fun ts _ -> non_local ts.ts_name) inst.mi_ty; let check_ls ls _ = non_local ls.ls_name; + (* TODO: Loc.errorm "`ls` is a program function, it cannot + be instantiated with a logical symbol" *) try ignore (restore_rs ls); raise (BadInstance (BadI ls.ls_name)) with Not_found -> () in Mls.iter check_ls inst.mi_ls; let check_rs rs _ = non_local rs.rs_name; + (* TODO: Loc.errorm "`rs` is a constructor/projection, + it cannot be instantiated" *) match (Mid.find rs.rs_name m.mod_known).pd_node with | PDtype _ -> raise (BadInstance (BadI rs.rs_name)) | PDlet _ | PDexn _ | PDpure -> () in @@ -690,9 +696,9 @@ let cl_save_rs cl s s' = end; match s.rs_logic, s'.rs_logic with | RLls s, RLls s' -> cl_save_ls cl s s' + | RLnone, (RLnone | RLls _ | RLlemma) -> () | RLlemma, RLlemma -> () (* TODO: update cl.pr_table? *) - | RLnone, RLnone -> () - | _ -> assert false + | _ -> raise (BadInstance (BadI s.rs_name)) type smap = { sm_vs : vsymbol Mvs.t; @@ -908,29 +914,64 @@ and clone_let_defn cl sm ld = match ld with let clone_type_record cl s d s' d' = let id = s.its_ts.ts_name in let fields' = Hstr.create 16 in + let matched_fields' = Hpv.create 16 in let add_field' rs' = let pj' = fd_of_rs rs' in Hstr.add fields' pj'.pv_vs.vs_name.id_string rs' in List.iter add_field' d'.itd_fields; - (* check if fields from former type are also declared in the new type *) - let match_pj rs = let pj = fd_of_rs rs in + (* refinement preserves (im)mutability *) + if not (s.its_mutable = s'.its_mutable) then + raise (BadInstance (BadI id)); + (* the fields from the old type must appear in the new type *) + let match_pj (bsb,fsb) rs = + let pj = fd_of_rs rs in let pj_str = pj.pv_vs.vs_name.id_string in let pj_ity = clone_ity cl pj.pv_ity in let pj_ght = pj.pv_ghost in + let pj_mut = List.exists (pv_equal pj) s.its_mfields in let rs' = try Hstr.find fields' pj_str with Not_found -> raise (BadInstance (BadI_not_found (id, pj_str))) in let pj' = fd_of_rs rs' in let pj'_ity = pj'.pv_ity in let pj'_ght = pj'.pv_ghost in - let equal_pjs = ity_equal pj_ity pj'_ity in - if not equal_pjs then - raise (BadInstance (BadI_type_proj (id, pj.pv_vs.vs_name.id_string))); + let pj'_mut = List.exists (pv_equal pj') s'.its_mfields in + let bsb = try ity_match bsb pj'_ity pj_ity with TypeMismatch _ -> + raise (BadInstance (BadI_type_proj (id, pj_str))) in + let fsb = try ity_match fsb pj_ity pj'_ity with TypeMismatch _ -> + raise (BadInstance (BadI_type_proj (id, pj_str))) in if not (pj_ght || not pj'_ght) then - raise (BadInstance (BadI_ghost_proj (id, pj.pv_vs.vs_name.id_string))); + raise (BadInstance (BadI_ghost_proj (id, pj_str))); + if not (pj_mut = pj'_mut) then (* TODO: dedicated BadI *) + raise (BadInstance (BadI_type_proj (id, pj_str))); let ls, ls' = ls_of_rs rs, ls_of_rs rs' in cl.ls_table <- Mls.add ls ls' cl.ls_table; cl.rs_table <- Mrs.add rs rs' cl.rs_table; - cl.fd_table <- Mpv.add pj pj' cl.fd_table in - List.iter match_pj d.itd_fields; + cl.fd_table <- Mpv.add pj pj' cl.fd_table; + Hpv.add matched_fields' pj' pj; + bsb, fsb in + ignore (List.fold_left match_pj (isb_empty,isb_empty) d.itd_fields); + (* the new fields must be separated from the old ones *) + let check_npj' (op,np) rs' = + let pj' = fd_of_rs rs' in + if Hpv.mem matched_fields' pj' then ity_freeze op pj'.pv_ity, np + else op, ity_freeze np pj'.pv_ity in + let op,np = List.fold_left check_npj' (isb_empty,isb_empty) d'.itd_fields in + if not (Mreg.set_disjoint op.isb_reg np.isb_reg) then + raise (BadInstance (BadI id)); +(* NOTE: shouldn't be necessary + (* cannot add fields with regions to an immutable type *) + if not s.its_mutable && not (Mreg.is_empty np.isb_reg) then + raise (BadInstance (BadI id)); +*) + (* if we refine a mutable type, then all new regions in the invariant + come from the new fields (no invariant strengthening on the old ones) *) + let pj_occurs pj f = t_v_occurs pj.pv_vs f > 0 in + let check_opj' pj' pj = + if not pj'.pv_ity.ity_pure && + List.exists (pj_occurs pj') d'.itd_invariant && + not (List.exists (pj_occurs pj) d.itd_invariant) then + raise (BadInstance (BadI id)) in + Hpv.iter check_opj' matched_fields'; + (* validate the refinement *) cl.ts_table <- Mts.add s.its_ts s' cl.ts_table let clone_type_decl inst cl tdl kn = @@ -969,7 +1010,7 @@ let clone_type_decl inst cl tdl kn = let pd' = Mid.find s'.its_ts.ts_name kn in let d' = match pd'.pd_node with | PDtype [d'] -> d' - (* FIXME: we could refine with mutual types *) + (* FIXME? we could refine with mutual types *) | PDtype _ -> raise (BadInstance (BadI id)) | PDlet _ | PDexn _ | PDpure -> raise (BadInstance (BadI id)) in clone_type_record cl s d s' d'; (* clone record fields *) @@ -981,16 +1022,14 @@ let clone_type_decl inst cl tdl kn = List.iter add_vc invl end | None -> begin match Mts.find_opt ts inst.mi_ty with | Some ity -> (* creative indentation *) - (* TODO: clone_type_record, axiom_of_invariant *) - (* TODO: should we only allow cloning into ity for - private types with no fields and no invariant? *) let stv = Stv.of_list ts.ts_args in if not (Stv.subset (ity_freevars Stv.empty ity) stv && - its_pure s && ity.ity_pure) then raise (BadInstance (BadI id)); + d.itd_fields = [] && d.itd_invariant = [] && + its_pure s && ity.ity_pure) then + raise (BadInstance (BadI id)); cl.ty_table <- Mts.add ts ity cl.ty_table | None -> assert false end end; Hits.add htd s None; - (* TODO: check typing conditions for refined record type *) end else (* variant *) if not s.its_mutable && d.itd_constructors <> [] && @@ -1085,6 +1124,7 @@ let clone_pdecl inst cl uc d = match d.pd_node with let add uc d = add_pdecl ~warn:false ~vc:false uc d in List.fold_left add uc dl | PDlet (LDsym (rs, c)) when Mrs.mem rs inst.mi_rs -> + freeze_foreign cl (cty_reads c.c_cty); (* refine only [val] symbols *) let cty = match c.c_node with (* cty for [val constant] is not c.c_cty *) | Cany -> c.c_cty