Commit 54f17867 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

Typing: reject invalid or useless "at"/"old"

Also, comment out a seemingly useless invariant in
examples/topological_sorting.mlw detected by the new check.
parent 50a52018
......@@ -115,7 +115,9 @@ module Static
invariant { inv g values !next }
invariant { Fset.subset p.S.contents (vertices g) }
invariant { Fset.subset (Fset.diff (vertices g) p.S.contents) (defined_sort values) }
(*
invariant { Fset.subset (defined_sort (old values)) (defined_sort values) }
*)
variant { S.cardinal p }
let u = S.choose_and_remove p in
dfs g u SA.empty values next
......
......@@ -362,7 +362,7 @@ type ghost = bool
type dbinder = preid option * ghost * dity
type register_old = pvsymbol -> string -> pvsymbol
type register_old = string -> pvsymbol -> pvsymbol
type 'a later = pvsymbol Mstr.t -> xsymbol Mstr.t -> register_old -> 'a
(* specification terms are parsed and typechecked after the program
......@@ -1033,8 +1033,9 @@ let find_old pvm (ovm,old) v =
let ld = let_var id ~ghost:true e in
Hpv.add old v ld; snd ld
let register_old env v l =
find_old env.pvm (Mstr.find_exn (UnboundLabel l) l env.old) v
let register_old env l =
let old = Mstr.find_exn (UnboundLabel l) l env.old in
fun v -> find_old env.pvm old v
let get_later env later =
let pvm = if Mpv.is_empty env.idx then env.pvm else
......
......@@ -60,7 +60,7 @@ exception UnboundLabel of string
val old_mark : string
type register_old = pvsymbol -> string -> pvsymbol
type register_old = string -> pvsymbol -> pvsymbol
(** Program variables occurring under [old] or [at] are passed to
a registrar function. The label string must be ["'Old"] for [old]. *)
......
......@@ -207,6 +207,9 @@ let mk_closure crcmap loc ls =
let vl = Lists.mapi mk_v ls.ls_args in
DTquant (DTlambda, vl, [], mk (DTapp (ls, List.map mk_t vl)))
(* track the use of labels *)
let at_uses = Hstr.create 5
let rec dterm ns km crcmap gvars at denv {term_desc = desc; term_loc = loc} =
let func_app e el =
List.fold_left (fun e1 (loc, e2) ->
......@@ -218,7 +221,15 @@ let rec dterm ns km crcmap gvars at denv {term_desc = desc; term_loc = loc} =
| _, [] -> func_app (mk_closure crcmap loc ls) (List.rev_append al el)
in
let qualid_app q el = match gvars at q with
| Some v -> func_app (DTgvar v.pv_vs) el
| Some v ->
begin match at with
| Some l -> (* check for impact *)
let u = Opt.get (gvars None q) in
if not (pv_equal v u) then
Hstr.replace at_uses l true
| None -> ()
end;
func_app (DTgvar v.pv_vs) el
| None ->
let ls = find_lsymbol_ns ns q in
apply_ls (qloc q) ls [] ls.ls_args el
......@@ -340,8 +351,16 @@ let rec dterm ns km crcmap gvars at denv {term_desc = desc; term_loc = loc} =
let cs, fl = parse_record ~loc ns km get_val fl in
let d = DTapp (cs, fl) in
if re then d else mk_let crcmap ~loc "q " e1 d
| Ptree.Tat (e1, l) ->
DTlabel (dterm ns km crcmap gvars (Some l.id_str) denv e1, Slab.empty)
| Ptree.Tat (e1, ({id_str = l} as id)) ->
Hstr.add at_uses l false;
let e1 = dterm ns km crcmap gvars (Some l) denv e1 in
if not (Hstr.find at_uses l) then begin
(* check if the label has actually been defined *)
ignore (gvars (Some l) (Qident {id with id_str = ""}));
Loc.errorm ~loc:id.id_loc "this `at'/`old' operator is never used"
end;
Hstr.remove at_uses l;
DTlabel (e1, Slab.empty)
| Ptree.Tscope (q, e1) ->
let ns = import_namespace ns (string_list_of_qualid q) in
DTlabel (dterm ns km crcmap gvars at denv e1, Slab.empty)
......@@ -356,14 +375,17 @@ let rec dterm ns km crcmap gvars at denv {term_desc = desc; term_loc = loc} =
DTcast (d1, dty_of_pty ns pty))
type global_vars = string option -> Ptree.qualid -> Ity.pvsymbol option
let no_gvars at q = match at with
| Some _ -> Loc.errorm ~loc:(qloc q)
"`at' and `old' can only be used in program annotations"
| None -> None
let type_term_in_namespace ns km crcmap gvars t =
let t = dterm ns km crcmap gvars None Dterm.denv_empty t in
let type_term_in_namespace ns km crcmap t =
let t = dterm ns km crcmap no_gvars None Dterm.denv_empty t in
Dterm.term ~strict:true ~keep_loc:true t
let type_fmla_in_namespace ns km crcmap gvars f =
let f = dterm ns km crcmap gvars None Dterm.denv_empty f in
let type_fmla_in_namespace ns km crcmap f =
let f = dterm ns km crcmap no_gvars None Dterm.denv_empty f in
Dterm.fmla ~strict:true ~keep_loc:true f
......@@ -500,8 +522,15 @@ let find_local_pv muc lvm q = match q with
let mk_gvars muc lvm old = fun at q ->
match find_local_pv muc lvm q, at with
| Some v, Some l -> Some (old v l)
| v, _ -> v
| Some v, Some l -> Some (old l v)
| None, Some l ->
begin match q with
(* normally, we have no reason to call "old" without
a pvsymbol, but we make an exception for an empty
ident to check if the label is valid at Tat *)
| Qident {id_str = ""} -> Opt.map (old l) None
| _ -> None end
| v, None -> v
let type_term muc lvm old t =
let gvars = mk_gvars muc lvm old in
......
......@@ -35,12 +35,8 @@ val string_list_of_qualid : Ptree.qualid -> string list
val print_qualid : Format.formatter -> Ptree.qualid -> unit
type global_vars = string option -> Ptree.qualid -> Ity.pvsymbol option
val type_term_in_namespace :
Theory.namespace -> Decl.known_map -> Coercion.t -> global_vars ->
Ptree.term -> Term.term
Theory.namespace -> Decl.known_map -> Coercion.t -> Ptree.term -> Term.term
val type_fmla_in_namespace :
Theory.namespace -> Decl.known_map -> Coercion.t -> global_vars ->
Ptree.term -> Term.term
Theory.namespace -> Decl.known_map -> Coercion.t -> Ptree.term -> Term.term
......@@ -237,8 +237,8 @@ let type_ptree ~as_fmla t tables =
let ns = tables.namespace in
let crc = tables.coercion in
if as_fmla
then Typing.type_fmla_in_namespace ns km crc (fun _ _ -> None) t
else Typing.type_term_in_namespace ns km crc (fun _ _ -> None) t
then Typing.type_fmla_in_namespace ns km crc t
else Typing.type_term_in_namespace ns km crc t
exception Arg_parse_type_error of Loc.position * string * exn
......
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