Commit d7477cf4 authored by Andrei Paskevich's avatar Andrei Paskevich

whyml: do not count the used symbols in program declarations

It is difficult to count all the used symbols in programs.
On the other hand, the pure API already cares about the missing
symbols in verification conditions. So we relieve the program API
of this duty, and trust typechecking (and any other API user) to
not forget to add all the necessary dependencies to a module.

The worst possible outcome, it seems, is that one can extract
an ill-formed OCaml code if the WhyML module is done via the API,
and VCs were not generated.
parent 052152ac
......@@ -34,7 +34,7 @@ type data_decl = itysymbol * constructor list
type pdecl = {
pd_node : pdecl_node;
pd_syms : Sid.t; (* idents used in declaration *)
(* pd_syms : Sid.t; (* idents used in declaration *) *)
pd_news : Sid.t; (* idents introduced in declaration *)
pd_tag : int; (* unique tag *)
}
......@@ -51,36 +51,79 @@ let pd_equal : pdecl -> pdecl -> bool = (==)
let mk_decl =
let r = ref 0 in
fun node syms news ->
fun node (*syms*) news ->
incr r;
{ pd_node = node; pd_syms = syms; pd_news = news; pd_tag = !r; }
{ pd_node = node; (*pd_syms = syms;*) pd_news = news; pd_tag = !r; }
let news_id s id = Sid.add_new (Decl.ClashIdent id) id s
(*
let syms_ts s ts = Sid.add ts.ts_name s
let syms_ls s ls = Sid.add ls.ls_name s
let syms_its s its = Sid.add its.its_pure.ts_name s
let syms_ps s ps = Sid.add ps.ps_name s
let syms_xs s xs = Sid.add xs.xs_name s
let syms_pl s pl = Sid.add pl.pl_ls.ls_name s
let syms_its s its = Sid.add its.its_pure.ts_name s
let syms_ty s ty = ty_s_fold syms_ts s ty
let syms_term s t = t_s_fold syms_ty syms_ls s t
let syms_ity s ity = ity_s_fold syms_its syms_ts s ity
let syms_effect s eff =
let add_raise xs s = syms_ity (syms_xs s xs) xs.xs_ity in
let s = Sexn.fold add_raise eff.eff_raises s in
let s = Sexn.fold add_raise eff.eff_ghostx s in
s
let syms_post s q = syms_term s (term_of_post q)
let syms_xpost s xq =
let add_xq xs q s = syms_post (syms_xs s xs) q in
Mexn.fold add_xq xq s
let syms_varmap s m = Sid.union s (Mid.map (fun _ -> ()) m)
let rec syms_type_c s tyc =
let s = syms_term s tyc.c_pre in
let s = syms_post s tyc.c_post in
let s = syms_xpost s tyc.c_xpost in
let s = syms_effect s tyc.c_effect in
syms_type_v s tyc.c_result
and syms_type_v s = function
| SpecV vtv -> syms_ity s vtv.vtv_ity
| SpecA (pvl,tyc) ->
let add_pv s pv = syms_ity s pv.pv_vtv.vtv_ity in
List.fold_left add_pv (syms_type_c s tyc) pvl
let rec syms_vta s a =
let s = syms_ity s a.vta_arg.vtv_ity in
let s = syms_effect s a.vta_effect in
syms_vty s a.vta_result
and syms_vty s = function
| VTvalue vtv -> syms_ity s vtv.vtv_ity
| VTarrow vta -> syms_vta s vta
let syms_expr s _e = s (* TODO *)
*)
(** {2 Declaration constructors} *)
let create_ty_decl its =
let syms = Util.option_fold syms_ity Sid.empty its.its_def in
(* 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
mk_decl (PDtype its) syms news
mk_decl (PDtype its) (*syms*) news
type pre_constructor = preid * (pvsymbol * bool) list
type pre_data_decl = itysymbol * pre_constructor list
let create_data_decl tdl =
let syms = ref Sid.empty in
(* 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 projections = Hid.create 17 in (* id -> plsymbol *)
......@@ -114,7 +157,7 @@ let create_data_decl tdl =
in
let build_proj (pv,pj) =
let vtv = pv.pv_vtv in
syms := ity_s_fold syms_its syms_ts !syms vtv.vtv_ity;
(* syms := ity_s_fold syms_its syms_ts !syms vtv.vtv_ity; *)
if pj then Some (build_proj pv.pv_vs.vs_name vtv) else None
in
pls, List.map build_proj al
......@@ -124,7 +167,7 @@ let create_data_decl tdl =
its, List.map (build_constructor its) cl
in
let tdl = List.map build_type tdl in
mk_decl (PDdata tdl) !syms !news
mk_decl (PDdata tdl) (*!syms*) !news
let check_vars vars =
if not (Stv.is_empty vars.vars_tv) then
......@@ -136,34 +179,47 @@ let letvar_news = function
let create_let_decl ld =
let news = letvar_news ld.let_var in
(* FIXME!!! This is not a correct way of counting symbols,
since it ignores type symbols and exception symbols, and
lsymbols inside specifications. We should either extend
varmap keeping in Mlw_expr to track all those symbols
(associating them to empty varsets), or use per-symbol maps
and folds in Mlw_ty and Mlw_expr, like we do in Ty and Term. *)
let syms = Mid.map (fun _ -> ()) ld.let_expr.e_vars in
mk_decl (PDlet ld) syms news
(*
let syms = syms_varmap Sid.empty ld.let_expr.e_vars in
let syms = syms_effect syms ld.let_expr.e_effect in
let syms = syms_vty syms ld.let_expr.e_vty in
let syms = syms_expr syms ld.let_expr in
*)
mk_decl (PDlet ld) (*syms*) news
let create_rec_decl rdl =
if rdl = [] then raise Decl.EmptyDecl;
let add_rd s { rec_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 s rd = Sid.union s (Mid.map (fun _ -> ()) rd.rec_vars) in
(* FIXME!!! See the comment in create_let_decl *)
(*
let add_rd syms { rec_ps = ps; rec_lambda = l; rec_vars = vm } =
let syms = syms_varmap syms vm in
let syms = syms_vta syms ps.ps_vta in
let syms = syms_term syms l.l_pre in
let syms = syms_post syms l.l_post in
let syms = syms_xpost syms l.l_xpost in
let addv s { v_term = t; v_rel = ls } =
Util.option_fold syms_ls (syms_term s t) ls in
let syms = List.fold_left addv syms l.l_variant in
syms_expr syms l.l_expr in
let syms = List.fold_left add_rd Sid.empty rdl in
mk_decl (PDrec rdl) syms news
*)
mk_decl (PDrec rdl) (*syms*) news
let create_val_decl vd =
let news = letvar_news vd.val_name in
(* FIXME!!! See the comment in create_let_decl *)
let syms = Mid.map (fun _ -> ()) vd.val_vars in
mk_decl (PDval vd) syms news
(*
let syms = syms_type_v Sid.empty vd.val_spec in
let syms = syms_varmap syms vd.val_vars in
*)
mk_decl (PDval vd) (*syms*) news
let create_exn_decl xs =
let news = Sid.singleton xs.xs_name in
let syms = Sid.empty (* FIXME!!! *) in
mk_decl (PDexn xs) syms news
(*
let syms = syms_ity Sid.empty xs.xs_ity in
*)
mk_decl (PDexn xs) (*syms*) news
(** {2 Known identifiers} *)
......@@ -179,7 +235,7 @@ let merge_known kn1 kn2 =
in
Mid.union check_known kn1 kn2
let known_add_decl lkn0 kn0 decl =
let known_add_decl _lkn0 kn0 decl =
let kn = Mid.map (const decl) decl.pd_news in
let check id decl0 _ =
if pd_equal decl0 decl
......@@ -187,10 +243,13 @@ let known_add_decl lkn0 kn0 decl =
else raise (RedeclaredIdent id)
in
let kn = Mid.union check kn0 kn in
(*
let unk = Mid.set_diff decl.pd_syms kn in
let unk = Mid.set_diff unk lkn0 in
if Sid.is_empty unk then kn
else raise (UnknownIdent (Sid.choose unk))
*)
kn
(* TODO: known_add_decl must check pattern matches for exhaustiveness *)
......
......@@ -36,7 +36,7 @@ type data_decl = itysymbol * constructor list
type pdecl = private {
pd_node : pdecl_node;
pd_syms : Sid.t; (* idents used in declaration *)
(* pd_syms : Sid.t; (* idents used in declaration *) *)
pd_news : Sid.t; (* idents introduced in declaration *)
pd_tag : int; (* unique tag *)
}
......
......@@ -1005,6 +1005,26 @@ let create_fun_defn id lam =
Loc.errorm "Variants are not allowed in a non-recursive definition";
create_fun_defn id lam
(* fold *)
let e_fold fn acc e = match e.e_node with
| Elet (ld,e) -> fn (fn acc ld.let_expr) e
| Erec (rdl,e) ->
let fnrd acc rd = fn acc rd.rec_lambda.l_expr in
fn (List.fold_left fnrd acc rdl) e
| Ecase (e,bl) ->
let fnbr acc (_,e) = fn acc e in
List.fold_left fnbr (fn acc e) bl
| Etry (e,bl) ->
let fnbr acc (_,_,e) = fn acc e in
List.fold_left fnbr (fn acc e) bl
| Eif (e1,e2,e3) -> fn (fn (fn acc e1) e2) e3
| Eapp (e,_) | Eassign (e,_,_) | Eghost e
| Eloop (_,_,e) | Efor (_,_,_,e) | Eraise (_,e)
| Eabstr (e,_,_) -> fn acc e
| Elogic _ | Evalue _ | Earrow _
| Eany _ | Eassert _ | Eabsurd -> acc
(*
- A "proper type" of a vty [v] is [v] with empty specification
(effect/pre/post/xpost). Basically, it is formed from pv_ity's
......
......@@ -271,3 +271,7 @@ val e_for :
val e_abstract : expr -> post -> xpost -> expr
val e_assert : assertion_kind -> term -> expr
val e_absurd : ity -> expr
(** expression traversal *)
val e_fold : ('a -> expr -> 'a) -> 'a -> expr -> 'a
......@@ -268,6 +268,7 @@ let add_pdecl uc d =
| PDexn xs ->
add_exn uc xs
(*
let add_pdecl_with_tuples uc d =
let ids = Mid.set_diff d.pd_syms uc.muc_known in
let ids = Mid.set_diff ids (Theory.get_known uc.muc_theory) in
......@@ -277,6 +278,7 @@ let add_pdecl_with_tuples uc d =
let ixs = Sid.fold add ids Sint.empty in
let add n uc = use_export_theory uc (tuple_theory n) in
add_pdecl (Sint.fold add ixs uc) d
*)
(* create module *)
......@@ -290,6 +292,7 @@ let th_unit =
let mod_exit =
let xs = create_xsymbol (id_fresh "%Exit") ity_unit in
let uc = empty_module (id_fresh "Exit") [] in
let uc = use_export_theory uc (tuple_theory 0) in
let uc = add_pdecl uc (create_exn_decl xs) in
close_module uc
......
......@@ -101,8 +101,4 @@ val add_meta : module_uc -> meta -> meta_arg list -> module_uc
(** Program decls *)
val add_pdecl : module_uc -> pdecl -> module_uc
val add_pdecl_with_tuples : module_uc -> pdecl -> module_uc
(*
val add_ty_pdecl : module_uc -> ty_pdecl list -> module_uc
*)
(* val add_pdecl_with_tuples : module_uc -> pdecl -> module_uc *)
......@@ -104,6 +104,27 @@ let create_denv uc = {
uloc = None;
}
(* Handle tuple symbols *)
let ht_tuple = Hashtbl.create 3
let ts_tuple n = Hashtbl.replace ht_tuple n (); ts_tuple n
let fs_tuple n = Hashtbl.replace ht_tuple n (); fs_tuple n
let count_term_tuples t =
let syms_ts _ ts = match is_ts_tuple_id ts.ts_name with
| Some n -> Hashtbl.replace ht_tuple n () | _ -> () in
let syms_ty _ ty = ty_s_fold syms_ts () ty in
t_s_fold syms_ty (fun _ _ -> ()) () t
let add_pdecl_with_tuples uc pd =
let kn = Theory.get_known (get_theory uc) in
let add_tuple n _ uc =
if Mid.mem (ts_tuple n).ts_name kn then uc
else use_export_theory uc (tuple_theory n) in
let uc = Hashtbl.fold add_tuple ht_tuple uc in
Hashtbl.clear ht_tuple;
add_pdecl uc pd
(** Typing type expressions *)
let rec dity_of_pty ~user denv = function
......@@ -379,7 +400,7 @@ let dvariant uc = function
(* expressions *)
let de_unit ~loc = hidden_ls ~loc (fs_tuple 0)
let de_unit ~loc = hidden_ls ~loc (Term.fs_tuple 0)
let de_app loc e el =
let res = create_type_variable () in
......@@ -619,18 +640,24 @@ let rec dty_of_ty ty = match ty.ty_node with
| Ty.Tyvar v -> Denv.tyuvar v
let create_post lenv x ty f =
let th = get_theory lenv.mod_uc in
let res = create_vsymbol (id_fresh x) ty in
let log_vars = Mstr.add x res lenv.log_vars in
let log_denv = Typing.add_var x (dty_of_ty ty) lenv.log_denv in
let f = Typing.type_fmla (get_theory lenv.mod_uc) log_denv log_vars f in
let f = Typing.type_fmla th log_denv log_vars f in
count_term_tuples f;
create_post res f
let create_pre lenv f =
Typing.type_fmla (get_theory lenv.mod_uc) lenv.log_denv lenv.log_vars f
let th = get_theory lenv.mod_uc in
let f = Typing.type_fmla th lenv.log_denv lenv.log_vars f in
count_term_tuples f;
f
let create_variant lenv (t,r) =
let t =
Typing.type_term (get_theory lenv.mod_uc) lenv.log_denv lenv.log_vars t in
let th = get_theory lenv.mod_uc in
let t = Typing.type_term th lenv.log_denv lenv.log_vars t in
count_term_tuples t;
{ v_term = t; v_rel = r }
let add_local x lv lenv = match lv with
......
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