Commit 1885c308 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

whyml: global program variables in annotations

parent 996fe2f2
...@@ -170,6 +170,7 @@ type dterm = { dt_node : dterm_node; dt_ty : dty } ...@@ -170,6 +170,7 @@ type dterm = { dt_node : dterm_node; dt_ty : dty }
and dterm_node = and dterm_node =
| Tvar of string | Tvar of string
| Tgvar of vsymbol
| Tconst of constant | Tconst of constant
| Tapp of lsymbol * dterm list | Tapp of lsymbol * dterm list
| Tif of dfmla * dterm * dterm | Tif of dfmla * dterm * dterm
...@@ -199,6 +200,8 @@ let rec term env t = match t.dt_node with ...@@ -199,6 +200,8 @@ let rec term env t = match t.dt_node with
| Tvar x -> | Tvar x ->
assert (Mstr.mem x env); assert (Mstr.mem x env);
t_var (Mstr.find x env) t_var (Mstr.find x env)
| Tgvar vs ->
t_var vs
| Tconst c -> | Tconst c ->
t_const c t_const c
| Tapp (s, tl) -> | Tapp (s, tl) ->
......
...@@ -68,6 +68,7 @@ type dterm = { dt_node : dterm_node; dt_ty : dty } ...@@ -68,6 +68,7 @@ type dterm = { dt_node : dterm_node; dt_ty : dty }
and dterm_node = and dterm_node =
| Tvar of string | Tvar of string
| Tgvar of vsymbol
| Tconst of constant | Tconst of constant
| Tapp of lsymbol * dterm list | Tapp of lsymbol * dterm list
| Tif of dfmla * dterm * dterm | Tif of dfmla * dterm * dterm
......
...@@ -117,14 +117,16 @@ let create_user_type_var x = ...@@ -117,14 +117,16 @@ let create_user_type_var x =
tyuvar (create_user_tv x) tyuvar (create_user_tv x)
type denv = { type denv = {
dvars : dty Mstr.t; (* local variables, to be bound later *) dvars : dty Mstr.t; (* local variables, to be bound later *)
gvars : qualid -> vsymbol option; (* global variables, for programs *)
} }
let denv_empty = { dvars = Mstr.empty } let denv_empty = { dvars = Mstr.empty; gvars = Util.const None }
let denv_empty_with_globals gv = { dvars = Mstr.empty; gvars = gv }
let mem_var x denv = Mstr.mem x denv.dvars let mem_var x denv = Mstr.mem x denv.dvars
let find_var x denv = Mstr.find x denv.dvars let find_var x denv = Mstr.find x denv.dvars
let add_var x ty denv = { dvars = Mstr.add x ty denv.dvars } let add_var x ty denv = { denv with dvars = Mstr.add x ty denv.dvars }
let print_denv fmt denv = let print_denv fmt denv =
Mstr.iter (fun x ty -> fprintf fmt "%s:%a,@ " x print_dty ty) denv.dvars Mstr.iter (fun x ty -> fprintf fmt "%s:%a,@ " x print_dty ty) denv.dvars
...@@ -342,7 +344,7 @@ and dpat_node loc uc env = function ...@@ -342,7 +344,7 @@ and dpat_node loc uc env = function
env, Pwild, ty env, Pwild, ty
| PPpvar x -> | PPpvar x ->
let ty = fresh_type_var loc in let ty = fresh_type_var loc in
let env = { dvars = Mstr.add x.id ty env.dvars } in let env = add_var x.id ty env in
env, Pvar x, ty env, Pvar x, ty
| PPpapp (x, pl) -> | PPpapp (x, pl) ->
let s, tyl, ty = specialize_fsymbol x uc in let s, tyl, ty = specialize_fsymbol x uc in
...@@ -374,7 +376,7 @@ and dpat_node loc uc env = function ...@@ -374,7 +376,7 @@ and dpat_node loc uc env = function
env, Papp (s, pl), ty env, Papp (s, pl), ty
| PPpas (p, x) -> | PPpas (p, x) ->
let env, p = dpat uc env p in let env, p = dpat uc env p in
let env = { dvars = Mstr.add x.id p.dp_ty env.dvars } in let env = add_var x.id p.dp_ty env in
env, Pas (p,x), p.dp_ty env, Pas (p,x), p.dp_ty
| PPpor (p, q) -> | PPpor (p, q) ->
let env, p = dpat uc env p in let env, p = dpat uc env p in
...@@ -413,7 +415,8 @@ let check_quant_linearity uqu = ...@@ -413,7 +415,8 @@ let check_quant_linearity uqu =
let check_highord uc env x tl = match x with let check_highord uc env x tl = match x with
| Qident { id = x } when Mstr.mem x env.dvars -> true | Qident { id = x } when Mstr.mem x env.dvars -> true
| _ -> List.length tl > List.length ((find_lsymbol x uc).ls_args) | _ -> env.gvars x <> None ||
List.length tl > List.length ((find_lsymbol x uc).ls_args)
let apply_highord loc x tl = match List.rev tl with let apply_highord loc x tl = match List.rev tl with
| a::[] -> [{pp_loc = loc; pp_desc = PPvar x}; a] | a::[] -> [{pp_loc = loc; pp_desc = PPvar x}; a]
...@@ -438,6 +441,11 @@ and dterm_node ~localize loc uc env = function ...@@ -438,6 +441,11 @@ and dterm_node ~localize loc uc env = function
(* local variable *) (* local variable *)
let ty = Mstr.find x env.dvars in let ty = Mstr.find x env.dvars in
Tvar x, ty Tvar x, ty
| PPvar x when env.gvars x <> None ->
let vs = Util.of_option (env.gvars x) in
assert (ty_closed vs.vs_ty);
let ty = specialize_ty ~loc (Htv.create 0) vs.vs_ty in
Tgvar vs, ty
| PPvar x -> | PPvar x ->
(* 0-arity symbol (constant) *) (* 0-arity symbol (constant) *)
let s, tyl, ty = specialize_fsymbol x uc in let s, tyl, ty = specialize_fsymbol x uc in
...@@ -471,7 +479,7 @@ and dterm_node ~localize loc uc env = function ...@@ -471,7 +479,7 @@ and dterm_node ~localize loc uc env = function
| PPlet (x, e1, e2) -> | PPlet (x, e1, e2) ->
let e1 = dterm ~localize uc env e1 in let e1 = dterm ~localize uc env e1 in
let ty = e1.dt_ty in let ty = e1.dt_ty in
let env = { dvars = Mstr.add x.id ty env.dvars } in let env = add_var x.id ty env in
let e2 = dterm ~localize uc env e2 in let e2 = dterm ~localize uc env e2 in
Tlet (e1, x, e2), e2.dt_ty Tlet (e1, x, e2), e2.dt_ty
| PPmatch (e1, bl) -> | PPmatch (e1, bl) ->
...@@ -508,7 +516,7 @@ and dterm_node ~localize loc uc env = function ...@@ -508,7 +516,7 @@ and dterm_node ~localize loc uc env = function
Tif (dfmla ~localize uc env e1, e2, e3), e2.dt_ty Tif (dfmla ~localize uc env e1, e2, e3), e2.dt_ty
| PPeps (x, ty, e1) -> | PPeps (x, ty, e1) ->
let ty = dty uc ty in let ty = dty uc ty in
let env = { dvars = Mstr.add x.id ty env.dvars } in let env = add_var x.id ty env in
let e1 = dfmla ~localize uc env e1 in let e1 = dfmla ~localize uc env e1 in
Teps (x, ty, e1), ty Teps (x, ty, e1), ty
| PPquant ((PPlambda|PPfunc|PPpred) as q, uqu, trl, a) -> | PPquant ((PPlambda|PPfunc|PPpred) as q, uqu, trl, a) ->
...@@ -519,7 +527,7 @@ and dterm_node ~localize loc uc env = function ...@@ -519,7 +527,7 @@ and dterm_node ~localize loc uc env = function
| Some id -> id | Some id -> id
| None -> assert false | None -> assert false
in in
{ dvars = Mstr.add id.id ty env.dvars }, (id,ty) add_var id.id ty env, (id,ty)
in in
let env, uqu = map_fold_left uquant env uqu in let env, uqu = map_fold_left uquant env uqu in
let trigger e = let trigger e =
...@@ -638,7 +646,7 @@ and dfmla_node ~localize loc uc env = function ...@@ -638,7 +646,7 @@ and dfmla_node ~localize loc uc env = function
| Some id -> id | Some id -> id
| None -> assert false | None -> assert false
in in
{ dvars = Mstr.add id.id ty env.dvars }, (id,ty) add_var id.id ty env, (id,ty)
in in
let env, uqu = map_fold_left uquant env uqu in let env, uqu = map_fold_left uquant env uqu in
let trigger e = let trigger e =
...@@ -677,7 +685,7 @@ and dfmla_node ~localize loc uc env = function ...@@ -677,7 +685,7 @@ and dfmla_node ~localize loc uc env = function
| PPlet (x, e1, e2) -> | PPlet (x, e1, e2) ->
let e1 = dterm ~localize uc env e1 in let e1 = dterm ~localize uc env e1 in
let ty = e1.dt_ty in let ty = e1.dt_ty in
let env = { dvars = Mstr.add x.id ty env.dvars } in let env = add_var x.id ty env in
let e2 = dfmla ~localize uc env e2 in let e2 = dfmla ~localize uc env e2 in
Flet (e1, x, e2) Flet (e1, x, e2)
| PPmatch (e1, bl) -> | PPmatch (e1, bl) ->
...@@ -958,9 +966,7 @@ let add_logics dl th = ...@@ -958,9 +966,7 @@ let add_logics dl th =
check_quant_linearity d.ld_params; check_quant_linearity d.ld_params;
let dadd_var denv (x, ty) = match x with let dadd_var denv (x, ty) = match x with
| None -> denv | None -> denv
| Some id -> | Some id -> add_var id.id (dty th' ty) denv
let ty = dty th' ty in
{ dvars = Mstr.add id.id ty denv.dvars }
in in
let denv = Hashtbl.find denvs id in let denv = Hashtbl.find denvs id in
let denv = List.fold_left dadd_var denv d.ld_params in let denv = List.fold_left dadd_var denv d.ld_params in
......
...@@ -62,6 +62,7 @@ val create_user_type_var : string -> Denv.dty ...@@ -62,6 +62,7 @@ val create_user_type_var : string -> Denv.dty
type denv type denv
val denv_empty : denv val denv_empty : denv
val denv_empty_with_globals : (Ptree.qualid -> vsymbol option) -> denv
val mem_var : string -> denv -> bool val mem_var : string -> denv -> bool
val find_var : string -> denv -> Denv.dty val find_var : string -> denv -> Denv.dty
......
...@@ -262,6 +262,13 @@ let find_variant_ls uc p = ...@@ -262,6 +262,13 @@ let find_variant_ls uc p =
with Not_found -> with Not_found ->
errorm ~loc:(qloc p) "unbound symbol %a" print_qualid p errorm ~loc:(qloc p) "unbound symbol %a" print_qualid p
let find_global_vs uc p =
let x = Typing.string_list_of_qualid [] p in
try match ns_find_ps (get_namespace uc) x with
| PV pv -> Some pv.pv_vs
| _ -> None
with Not_found -> None
let rec dpattern denv ({ pat_loc = loc } as pp) = match pp.pat_desc with let rec dpattern denv ({ pat_loc = loc } as pp) = match pp.pat_desc with
| Ptree.PPpwild -> | Ptree.PPpwild ->
PPwild, create_type_variable (), denv PPwild, create_type_variable (), denv
...@@ -580,7 +587,7 @@ let create_lenv uc = { ...@@ -580,7 +587,7 @@ let create_lenv uc = {
mod_uc = use_export_theory uc Mlw_wp.th_mark; mod_uc = use_export_theory uc Mlw_wp.th_mark;
let_vars = Mstr.empty; let_vars = Mstr.empty;
log_vars = Mstr.empty; log_vars = Mstr.empty;
log_denv = Typing.denv_empty; log_denv = Typing.denv_empty_with_globals (find_global_vs uc);
} }
let rec dty_of_ty ty = match ty.ty_node with let rec dty_of_ty ty = match ty.ty_node with
......
...@@ -37,7 +37,7 @@ module N ...@@ -37,7 +37,7 @@ module N
val add : val add :
x:int -> y: ref int -> x:int -> y: ref int ->
{} unit writes gr { y.contents = (old y.contents) + 4 } {} unit writes gr { gr.contents = (old gr.contents) + 4 }
let test () = let test () =
......
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