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

Mdecl: count new and used symbols

parent 6d5bd39a
......@@ -197,7 +197,7 @@ let create_constructor ~constr id s fl =
let argl = List.map (fun a -> t_var a.pv_vs) fl in
let q = make_post (fs_app ls argl ty) in
let c = create_cty fl [] [q] Mexn.empty eff_empty ity in
mk_rs (id_register id) c (RLls ls) None
mk_rs ls.ls_name c (RLls ls) None
let rs_of_ls ls =
let v_args = List.map (fun ty ->
......@@ -707,12 +707,12 @@ let rec e_rs_subst sm e =
let d = e_rs_subst sm d in
ity_equal_check d.e_ity v.pv_ity;
if e_ghost d <> v.pv_ghost then Loc.errorm
"Expr.create_rec_defn: ghost status mismatch";
"Expr.let_rec: ghost status mismatch";
e_let (LDvar (v,d)) (e_rs_subst sm e)
| Elet (LDsym (s,d),e) ->
let d = c_rs_subst sm d in
if c_ghost d <> rs_ghost s then Loc.errorm
"Expr.create_rec_defn: ghost status mismatch";
"Expr.let_rec: ghost status mismatch";
let ns = rs_dup s d.c_cty in
e_let (LDsym (ns,d)) (e_rs_subst (Mrs.add s ns sm) e)
| Elet (LDrec fdl,e) ->
......@@ -746,7 +746,7 @@ and c_rs_subst sm ({c_node = n; c_cty = c} as d) =
and rec_fixp dl =
let update sm (s,({c_cty = c} as d)) =
if c_ghost d <> rs_ghost s then Loc.errorm
"Expr.create_rec_defn: ghost status mismatch";
"Expr.let_rec: ghost status mismatch";
let c = if List.length c.cty_pre < List.length s.rs_cty.cty_pre
then c else cty_add_pre [List.hd s.rs_cty.cty_pre] c in
if eff_equal c.cty_effect s.rs_cty.cty_effect then sm, (s,d)
......@@ -763,7 +763,7 @@ let let_rec fdl =
(* check that the all variants use the same order *)
let varl1 = match fdl with
| (_,_,vl,_)::_ -> List.rev vl
| [] -> invalid_arg "Expr.create_rec_defn" in
| [] -> invalid_arg "Expr.let_rec" in
let no_int t = not (ty_equal (t_type t) ty_int) in
let check_variant (_,_,vl,_) =
let vl, varl1 = match List.rev vl, varl1 with
......@@ -801,7 +801,7 @@ let let_rec fdl =
not (ity_equal s.rs_cty.cty_result c.cty_result) ||
(c_ghost d && not (rs_ghost s)) || c.cty_args = [] ||
s.rs_logic <> RLnone
then invalid_arg "Expr.create_rec_defn";
then invalid_arg "Expr.let_rec";
(* prepare the extra "decrease" precondition *)
let pre = match ds with
| Some ls -> ps_app ls (List.map fst varl) :: c.cty_pre
......@@ -811,7 +811,8 @@ let let_rec fdl =
let c = create_cty c.cty_args pre
c.cty_post c.cty_xpost start_eff c.cty_result in
let ns = create_rsymbol id ~ghost:(rs_ghost s) ~kind:RKnone c in
Mrs.add s ns sm, (ns, c_ghostify (rs_ghost s) d) in
let sm = Mrs.add_new (Invalid_argument "Expr.let_rec") s ns sm in
sm, (ns, c_ghostify (rs_ghost s) d) in
let sm, dl = Lists.map_fold_left update Mrs.empty fdl in
(* produce the recursive definition *)
let conv (s,d) = s, c_rs_subst sm d in
......@@ -823,6 +824,11 @@ let let_rec fdl =
let rdl = List.map2 merge fdl (rec_fixp (List.map conv dl)) in
LDrec rdl, rdl
let ls_decr_of_let_defn = function
| LDrec ({rec_rsym = {rs_cty = {cty_pre = {t_node = Tapp (ls,_)}::_}};
rec_varl = _::_ }::_) -> Some ls
| _ -> None
(* pretty-pringting *)
open Format
......
......@@ -168,6 +168,10 @@ val let_sym :
val let_rec :
(rsymbol * cexp * variant list * rs_kind) list -> let_defn * rec_defn list
val ls_decr_of_let_defn : let_defn -> lsymbol option
(* returns the dummy predicate symbol used in the precondition of
the rec_rsym rsymbol to store the instantiated variant list *)
(** {2 Callable expressions} *)
val c_app : rsymbol -> pvsymbol list -> ity list -> ity -> cexp
......
......@@ -516,7 +516,7 @@ let create_itysymbol_alias id args def =
create_its ~ts ~pm:false ~mfld:[] ~regs ~aimm:tl ~aexp:tl
~avis:tl ~afrz:tl ~rvis:rl ~rfrz:rl ~def:(Some def)
exception ImpurePrivateField of ity
exception ImpureField of ity
let create_itysymbol_rich id args pm flds =
let ts = create_tysymbol id args None in
......@@ -531,13 +531,13 @@ let create_itysymbol_rich id args pm flds =
if not (Stv.subset dargs sargs) then
raise (Ty.UnboundTypeVar (Stv.choose (Stv.diff dargs sargs)));
let mfld = Mpv.fold (fun f m l -> if m then f::l else l) flds [] in
if pm then (* private mutable record *)
if pm then begin (* private mutable record *)
let tl = List.map Util.ttrue args in
let () = collect_all (fun () i -> if not i.ity_pure
then Loc.error ?loc:id.pre_loc (ImpurePrivateField i)) () in
Mpv.iter (fun {pv_vs = v; pv_ity = i} _ -> if not i.ity_pure
then Loc.error ?loc:v.vs_name.id_loc (ImpureField i)) flds;
create_its ~ts ~pm ~mfld ~regs:[] ~aimm:tl ~aexp:tl ~avis:tl
~afrz:tl ~rvis:[] ~rfrz:[] ~def:None
else (* non-private updatable type *)
end else (* non-private updatable type *)
let top_regs ity = ity_r_fold (fun s r -> Sreg.add r s) ity in
let regs = Sreg.elements (collect_all top_regs Sreg.empty) in
let check_args s = List.map (fun v -> Stv.mem v s) args in
......@@ -1239,9 +1239,9 @@ let () = Exn_printer.register (fun fmt e -> match e with
"Region %a is used twice" print_reg r
| UnboundRegion r -> fprintf fmt
"Unbound region %a" print_reg r
| ImpurePrivateField ity -> fprintf fmt
"Field type %a is mutable, it cannot be used in a private record"
print_ity_full ity
| ImpureField ity -> fprintf fmt
"Field type %a is mutable, it cannot be used in a type which is \
private, recursive, or has an invariant" print_ity_full ity
(*
| UnboundException xs -> fprintf fmt
"This function raises %a but does not specify a post-condition for it"
......
......@@ -93,7 +93,7 @@ val ity_hash : ity -> int
val reg_hash : region -> int
val pv_hash : pvsymbol -> int
exception ImpurePrivateField of ity
exception ImpureField of ity
exception DuplicateRegion of region
exception UnboundRegion of region
......
......@@ -40,11 +40,7 @@ let check_field stv f =
if not (Stv.subset ftv stv) then Loc.error ?loc
(Ty.UnboundTypeVar (Stv.choose (Stv.diff ftv stv)));
if not f.pv_ity.ity_pure then Loc.error ?loc
(Ity.ImpurePrivateField f.pv_ity)
(* FIXME: the ImpurePrivateField error message in Ity is
too restrictive wrt all the cases we use check_field.
We should either provide different exceptions or rewrite
the message. *)
(Ity.ImpureField f.pv_ity)
let check_invariant stv svs p =
let ptv = t_ty_freevars Stv.empty p in
......@@ -159,3 +155,146 @@ and mdecl_node =
| MDlet of let_defn
| MDexn of xsymbol
| MDpure
let md_equal : mdecl -> mdecl -> bool = (==)
let get_news node pure =
let news_id s id = Sid.add_new (Decl.ClashIdent id) id s in
let news_rs news s = news_id news s.rs_name in
let news_pure news d = Sid.union news d.Decl.d_news in
let news = List.fold_left news_pure Sid.empty pure in
match node with
| MDtype dl ->
let news_itd news d =
let news = news_id news d.itd_its.its_ts.ts_name in
let news = List.fold_left news_rs news d.itd_fields in
List.fold_left news_rs news d.itd_constructors in
List.fold_left news_itd news dl
| MDlet (LDvar (v,_)) -> news_id news v.pv_vs.vs_name
| MDlet (LDsym (s,_)) -> news_id news s.rs_name
| MDlet (LDrec rdl) ->
let news_rd news d = news_id news d.rec_sym.rs_name in
List.fold_left news_rd news rdl
| MDexn xs -> news_id news xs.xs_name
| MDpure -> news
let get_syms node pure =
let syms_ts s ts = Sid.add ts.ts_name s in
let syms_ls s ls = Sid.add ls.ls_name s in
let syms_ty s ty = ty_s_fold syms_ts s ty in
let syms_term s t = t_s_fold syms_ty syms_ls s t in
let syms_pure syms d = Sid.union syms d.Decl.d_syms in
let syms_vari syms (t,r) = Opt.fold syms_ls (syms_term syms t) r in
let syms = List.fold_left syms_pure Sid.empty pure in
let syms_its syms s = Sid.add s.its_ts.ts_name syms in
let syms_ity syms ity = ity_s_fold syms_its syms ity in
let syms_xs xs syms = Sid.add xs.xs_name syms in
let syms_pv syms v = syms_ity syms v.pv_ity in
let rec syms_pat syms p = match p.pat_node with
| Pwild | Pvar _ -> syms
| Papp (s,pl) ->
let syms = List.fold_left syms_ty syms s.ls_args in
List.fold_left syms_pat syms pl
| Por (p,q) -> syms_pat (syms_pat syms p) q
| Pas (p,_) -> syms_pat syms p in
let syms_cty syms c =
let add_tl syms tl = List.fold_left syms_term syms tl in
let add_xq xs ql syms = syms_xs xs (add_tl syms ql) in
let syms = add_tl (add_tl syms c.cty_pre) c.cty_post in
let syms = Mexn.fold add_xq c.cty_xpost syms in
Sexn.fold syms_xs c.cty_effect.eff_raises syms in
let rec syms_expr syms e = match e.e_node with
| Evar _ | Econst _ | Eabsurd -> syms
| Eassert (_,t) | Epure t -> syms_term syms t
| Eexec c -> syms_cexp syms c
| Eassign al ->
let syms_as syms (v,s,u) =
syms_pv (syms_pv (Sid.add s.rs_name syms) u) v in
List.fold_left syms_as syms al
| Elet (ld,e) ->
let esms = syms_expr Sid.empty e in
let esms = match ld with
| LDvar _ -> esms
| LDsym (s,_) -> Sid.remove s.rs_name esms
| LDrec rdl ->
let del_rd syms rd = Sid.remove rd.rec_sym.rs_name syms in
List.fold_left del_rd esms rdl in
syms_let_defn (Sid.union syms esms) ld
| Efor (i,_,invl,e) ->
syms_pv (List.fold_left syms_term (syms_expr syms e) invl) i
| Ewhile (d,invl,varl,e) ->
let syms = List.fold_left syms_vari (syms_expr syms e) varl in
List.fold_left syms_term (syms_eity syms d) invl
| Eif (c,d,e) ->
syms_expr (syms_expr (syms_eity syms c) d) e
| Ecase (d,bl) ->
let add_branch syms (p,e) =
syms_pat (syms_expr syms e) p.pp_pat in
List.fold_left add_branch (syms_eity syms d) bl
| Etry (d,xl) ->
let add_branch syms (xs,v,e) =
syms_xs xs (syms_pv (syms_expr syms e) v) in
List.fold_left add_branch (syms_expr syms d) xl
| Eraise (xs,e) ->
syms_xs xs (syms_eity syms e)
and syms_eity syms e =
syms_expr (syms_ity syms e.e_ity) e
and syms_city syms c =
let syms = syms_ity (syms_cexp syms c) c.c_cty.cty_result in
List.fold_left syms_pv syms c.c_cty.cty_args
and syms_cexp syms c = match c.c_node with
| Capp (s,vl) ->
let syms = List.fold_left syms_pv syms vl in
syms_cty (Sid.add s.rs_name syms) s.rs_cty
| Cfun e -> syms_cty (syms_expr syms e) c.c_cty
| Cany -> syms_cty syms c.c_cty
and syms_let_defn syms = function
| LDvar (_,e) -> syms_eity syms e
| LDsym (s,c) ->
let syms = match s.rs_logic with
| RLpv _ -> syms_ls (syms_ts syms ts_func) fs_func_app
| _ -> syms in
syms_city syms c
| LDrec rdl as ld ->
let add_rd syms rd =
let syms = List.fold_left syms_vari syms rd.rec_varl in
let syms = match rd.rec_sym.rs_logic with
| RLpv _ -> syms_ls (syms_ts syms ts_func) fs_func_app
| _ -> syms in
syms_city syms rd.rec_fun in
let dsms = List.fold_left add_rd Sid.empty rdl in
let dsms = match ls_decr_of_let_defn ld with
| Some ls -> Sid.remove ls.ls_name dsms | None -> dsms in
let del_rd syms rd = Sid.remove rd.rec_rsym.rs_name syms in
Sid.union syms (List.fold_left del_rd dsms rdl)
in
match node with
| MDtype dl ->
let syms_itd syms d =
(* the syms of the invariants are already in [pure] *)
let syms = Opt.fold syms_ity syms d.itd_its.its_def in
let add_fd syms s = syms_ity syms s.rs_cty.cty_result in
let add_cs syms s = List.fold_left syms_pv syms s.rs_cty.cty_args in
let syms = List.fold_left add_fd syms d.itd_fields in
List.fold_left add_cs syms d.itd_constructors in
List.fold_left syms_itd syms dl
| MDlet ld ->
let syms = syms_let_defn syms ld in
let vars = match ld with
| LDvar (_,e) -> e.e_effect.eff_reads
| LDsym (_,c) -> cty_reads c.c_cty
| LDrec rdl -> List.fold_left (fun s rd ->
Spv.union s (cty_reads rd.rec_fun.c_cty)) Spv.empty rdl in
Spv.fold (fun v s -> Sid.add v.pv_vs.vs_name s) vars syms
| MDexn xs -> syms_ity syms xs.xs_ity
| MDpure -> syms
let mk_decl = let r = ref 0 in fun node pure ->
{ md_node = node; md_pure = pure;
md_syms = get_syms node pure;
md_news = get_news node pure;
md_tag = (incr r; !r) }
let create_type_decl dl =
let ldl = assert false (* TODO *) in
mk_decl (MDtype dl) ldl
......@@ -54,3 +54,5 @@ and mdecl_node = private
| MDlet of let_defn
| MDexn of xsymbol
| MDpure
val create_type_decl : its_defn list -> mdecl
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