Commit 5214043f authored by Sylvain Dailler's avatar Sylvain Dailler

Add name to requires and asserts

This is implemented using an attribute that is detected when a
transformation introduces the hypothesis.
Added for assertion_kind and requires.
parent abdb518d
......@@ -8,6 +8,12 @@ Standard library
- in `set.SetApp` and `set.SetImp`, type `t` becomes `set`;
field `contents` becomes `to_fset`; call to `empty` becomes `empty ()`
Language
* It is now possible to give a name to requires and assertions.
`requires Hyp { a = 3 }` tries to give the name `Hyp` to the corresponding
hypothesis after introduction. This uses the attribute [@hyp_name:] which is
now reserved.
Tools
* counterexamples given by `why3prove` are no longer printed using JSON
by default; pass option `--json` to restore the previous behavior
......
......@@ -450,6 +450,15 @@ let extract_field attr =
with
| _ -> None
(* Attributes used to name hypothesis *)
let is_hyp_name_attr a =
Strings.has_prefix "hyp_name:" a.attr_string
let get_hyp_name ~attrs =
try Some (Strings.remove_prefix "hyp_name:"
(Sattr.choose (Sattr.filter is_hyp_name_attr attrs)).attr_string)
with Not_found -> None
(* Functions for working with ITP attributes *)
let is_name_attr a =
......
......@@ -232,3 +232,7 @@ val extract_field: attribute -> (int * string) option
val get_model_trace_attr : attrs:Sattr.t -> attribute
(** Return an attribute of the form ["model_trace:*"].
Raises [Not_found] if there is no such attribute. *)
val get_hyp_name: attrs:Sattr.t -> string option
(** If attrs contains an attribute of the form ["hyp_name:<s>"] returns
[Some <s>] or [None] if no attribute have this form *)
......@@ -1082,8 +1082,13 @@ single_expr_:
{ Ematch ($2, [], $4) }
| GHOST single_expr
{ Eghost $2 }
| assertion_kind LEFTBRC term RIGHTBRC
{ Eassert ($1, $3) }
| assertion_kind option(name) LEFTBRC term RIGHTBRC
{ match $2 with
| None -> Eassert ($1, $4)
| Some name ->
let attr = ATstr (Ident.create_attribute ("hyp_name:" ^ name)) in
let t = { $4 with term_desc = Tattr (attr, $4) } in
Eassert ($1, t) }
| attr single_expr %prec prec_attr
{ Eattr ($1, $2) }
| single_expr cast
......@@ -1182,9 +1187,18 @@ spec:
| (* epsilon *) %prec prec_no_spec { empty_spec }
| single_spec spec { spec_union $1 $2 }
name:
| LIDENT { $1 }
| UIDENT { $1 }
single_spec:
| REQUIRES LEFTBRC term RIGHTBRC
{ { empty_spec with sp_pre = [$3] } }
| REQUIRES option(name) LEFTBRC term RIGHTBRC
{ match $2 with
| None -> { empty_spec with sp_pre = [$4] }
| Some name ->
let attr = ATstr (Ident.create_attribute ("hyp_name:" ^ name)) in
let t = { $4 with term_desc = Tattr (attr, $4) } in
{ empty_spec with sp_pre = [t] } }
| ENSURES LEFTBRC ensures RIGHTBRC
{ { empty_spec with sp_post = [floc $startpos($3) $endpos($3), $3] } }
| RETURNS LEFTBRC match_cases(term) RIGHTBRC
......
......@@ -120,7 +120,9 @@ let rec intros kn pr mal expl f =
(* f is going to be removed, preserve its attributes and location in f2 *)
let f2 = t_attr_copy f f2 in
let fl = Split_goal.split_intro_right ?known_map:kn (dequant false f1) in
let idx = id_fresh "H" ~attrs:intro_attrs in
let idx =
let name = Ident.get_hyp_name ~attrs:f1.t_attrs in
id_fresh (Opt.get_def "H" name) ~attrs:intro_attrs in
let add (subst,dl) f =
let svs = Mvs.set_diff (t_freevars Mvs.empty f) subst in
let subst, dl = Mvs.fold (fun vs _ (subst,dl) ->
......
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