Mlw: "label <uident> in", "<expr> at <uident>", "old <expr>"

share/emacs/why3.el

@@ -29,7 +29,7 @@
    '("(\\*\\([^*)]\\([^*]\\|\\*[^)]\\)*\\)?\\*)" . font-lock-comment-face)
 ;   '("{}\\|{[^|]\\([^}]*\\)}" . font-lock-type-face)
    `(,(why3-regexp-opt '("invariant" "variant" "diverges" "requires" "ensures" "returns" "raises" "reads" "writes" "assert" "assume" "check")) . font-lock-type-face)
-   `(,(why3-regexp-opt '("use" "clone" "namespace" "import" "export" "coinductive" "inductive" "external" "constant" "function" "predicate" "val" "exception" "axiom" "lemma" "goal" "type" "mutable" "model" "abstract" "private" "any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "for" "to" "downto" "do" "done" "loop" "absurd" "ghost" "raise" "try" "with" "theory" "uses" "module" "converter" "fun")) . font-lock-keyword-face)
+   `(,(why3-regexp-opt '("use" "clone" "namespace" "import" "export" "coinductive" "inductive" "external" "constant" "function" "predicate" "val" "exception" "axiom" "lemma" "goal" "type" "mutable" "model" "abstract" "private" "any" "match" "let" "rec" "in" "if" "then" "else" "begin" "end" "while" "for" "to" "downto" "do" "done" "loop" "absurd" "ghost" "raise" "try" "with" "theory" "uses" "module" "converter" "fun" "at" "old" "true" "false" "forall" "exists" "label")) . font-lock-keyword-face)
    )
   "Minimal highlighting for Why3 mode")
 

share/lang/why3.lang

@@ -157,6 +157,7 @@ on linking described in file LICENSE.
 -->
 	<context id="keywords" style-ref="meta-keyword">
           <keyword>abstract</keyword>
+          <keyword>as</keyword>
           <keyword>axiom</keyword>
           <keyword>clone</keyword>
           <keyword>coinductive</keyword>
@@ -170,11 +171,12 @@ on linking described in file LICENSE.
           <keyword>import</keyword>
           <keyword>inductive</keyword>
           <keyword>lemma</keyword>
+          <keyword>meta</keyword>
           <keyword>mutable</keyword>
           <keyword>module</keyword>
-          <keyword>namespace</keyword>
           <keyword>predicate</keyword>
           <keyword>private</keyword>
+          <keyword>scope</keyword>
           <keyword>theory</keyword>
           <keyword>type</keyword>
           <keyword>use</keyword>
@@ -182,6 +184,7 @@ on linking described in file LICENSE.
           <keyword>with</keyword>
 	</context>
 	<context id="meta-words" style-ref="keyword">
+          <keyword>any</keyword>
           <keyword>begin</keyword>
           <keyword>do</keyword>
           <keyword>done</keyword>
@@ -190,11 +193,14 @@ on linking described in file LICENSE.
           <keyword>exists</keyword>
           <keyword>for</keyword>
           <keyword>forall</keyword>
+          <keyword>fun</keyword>
           <keyword>if</keyword>
           <keyword>in</keyword>
+          <keyword>label</keyword>
           <keyword>let</keyword>
           <keyword>loop</keyword>
           <keyword>match</keyword>
+          <keyword>not</keyword>
           <keyword>raise</keyword>
           <keyword>rec</keyword>
           <keyword>then</keyword>
@@ -208,10 +214,12 @@ on linking described in file LICENSE.
           <keyword>absurd</keyword>
           <keyword>assert</keyword>
           <keyword>assume</keyword>
+          <keyword>at</keyword>
 	  <keyword>diverges</keyword>
 	  <keyword>ensures</keyword>
 	  <keyword>check</keyword>
 	  <keyword>invariant</keyword>
+	  <keyword>old</keyword>
 	  <keyword>raises</keyword>
 	  <keyword>reads</keyword>
 	  <keyword>requires</keyword>

share/vim/why3.vim

@@ -43,7 +43,7 @@ syn match    whyEndErr     "\<end\>"
 " Some convenient clusters
 syn cluster  whyAllErrs contains=whyBraceErr,whyBrackErr,whyParenErr,whyCommentErr,whyCountErr,whyDoErr,whyDoneErr,whyEndErr,whyThenErr,whyTheoryErr,whyModuleErr
 
-syn cluster  whyContained contains=whyTodo,whyImport,whyExport,whyTheoryContents,whyModuleContents,whyNamespaceContents,whyModuleKeyword
+syn cluster  whyContained contains=whyTodo,whyImport,whyExport,whyTheoryContents,whyModuleContents,whyScopeContents,whyModuleKeyword
 " ,whyPreDef,whyModParam,whyModParam1,whyPreMPRestr,whyMPRestr,whyMPRestr1,whyMPRestr2,whyMPRestr3,whyModRHS,whyFuncWith,whyFuncStruct,whyModTypeRestr,whyModTRWith,whyWith,whyWithRest,whyModType,whyFullMod,whyVal
 
 " Enclosing delimiters
@@ -70,18 +70,18 @@ syn region   whyNone matchgroup=whyKeyword start="\<if\>" matchgroup=whyKeyword
 
 syn region   whyTheory matchgroup=whyKeyword start="\<theory\>" matchgroup=whyModSpec end="\<\u\(\w\|'\)*\>" contains=@whyAllErrs,whyComment skipwhite skipempty nextgroup=whyTheoryContents
 syn region   whyModule matchgroup=whyKeyword start="\<module\>" matchgroup=whyModSpec end="\<\u\(\w\|'\)*\>" contains=@whyAllErrs,whyComment skipwhite skipempty nextgroup=whyModuleContents
-syn region   whyNamespace matchgroup=whyKeyword start="\<namespace\>" matchgroup=whyModSpec end="\<\u\(\w\|'\)*\>" contains=@whyAllErrs,whyComment,whyImport skipwhite skipempty nextgroup=whyNamespaceContents
+syn region   whyScope matchgroup=whyKeyword start="\<scope\>" matchgroup=whyModSpec end="\<\u\(\w\|'\)*\>" contains=@whyAllErrs,whyComment,whyImport skipwhite skipempty nextgroup=whyScopeContents
 
 syn region   whyTheoryContents start="^" start="."me=e-1 matchgroup=whyModSpec end="\<end\>" contained contains=ALLBUT,@whyContained,whyEndErr,whyTheory,whyModule
 syn region   whyModuleContents start="^" start="."me=e-1 matchgroup=whyModSpec end="\<end\>" contained contains=ALLBUT,@whyContained,whyEndErr,whyTheory,whyModule
-syn region   whyNamespaceContents start="^" start="."me=e-1 matchgroup=whyModSpec end="\<end\>" contained contains=ALLBUT,@whyContained,whyEndErr,whyTheory,whyModule
+syn region   whyScopeContents start="^" start="."me=e-1 matchgroup=whyModSpec end="\<end\>" contained contains=ALLBUT,@whyContained,whyEndErr,whyTheory,whyModule
 
 syn region   whyNone matchgroup=whyKeyword start="\<\(use\|clone\)\>" matchgroup=whyModSpec end="\<\(\w\+\.\)*\u\(\w\|'\)*\>" contains=@whyAllErrs,whyComment,whyString,whyImport,whyExport,whyModuleKeyword
 syn keyword  whyExport contained export
 syn keyword  whyImport contained import
 syn keyword  whyModuleKeyword contained module
 
-syn region   whyNone matchgroup=whyKeyword start="\<\(axiom\|lemma\|goal\|prop\)\>" matchgroup=whyNone end="\<\w\(\w\|'\)*\>" contains=@whyAllErrs,whyComment
+syn region   whyNone matchgroup=whyKeyword start="\<\(axiom\|lemma\|goal\)\>" matchgroup=whyNone end="\<\w\(\w\|'\)*\>" contains=@whyAllErrs,whyComment
 
 syn keyword  whyKeyword  as constant
 syn keyword  whyKeyword  else epsilon exists
@@ -92,7 +92,7 @@ syn keyword  whyKeyword  not predicate
 syn keyword  whyKeyword  then type with
 
 syn keyword  whyKeyword  any
-syn keyword  whyKeyword  exception fun ghost
+syn keyword  whyKeyword  exception fun ghost label
 syn keyword  whyKeyword  model mutable private
 syn keyword  whyKeyword  raise rec val while
 
@@ -102,7 +102,7 @@ syn keyword  whyType     bool int list map option real
 syn keyword  whyType     array ref unit
 
 syn keyword  whySpec     absurd assert assume check diverges ensures invariant
-syn keyword  whySpec     raises reads requires returns variant writes
+syn keyword  whySpec     raises reads requires returns variant writes at old
 
 syn match    whyConstructor  "(\s*)"
 syn match    whyConstructor  "\u\(\w\|'\)*\>"
@@ -149,8 +149,8 @@ syn sync match whyTheorySync  groupthere whyTheory  "\<end\>"
 syn sync match whyModuleSync  grouphere  whyModule  "\<module\>"
 syn sync match whyModuleSync  groupthere whyModule  "\<end\>"
 
-syn sync match whyNamespaceSync  grouphere  whyNamespace  "\<namespace\>"
-syn sync match whyNamespaceSync  groupthere whyNamespace  "\<end\>"
+syn sync match whyScopeSync   grouphere  whyScope   "\<scope\>"
+syn sync match whyScopeSync   groupthere whyScope   "\<end\>"
 
 " Define the default highlighting.
 " For version 5.7 and earlier: only when not done already

src/mlw/dexpr.ml

@@ -852,6 +852,7 @@ let env_empty = {
 exception UnboundLabel of string
 
 let find_old pvm (ovm,old) v =
+  if v.pv_ity.ity_pure then v else
   let n = v.pv_vs.vs_name.id_string in
   (* if v is top-level, both ov and pv are None.
      If v is local, ov and pv must be equal to v.
@@ -882,7 +883,7 @@ let rebase_old {pvm = pvm} preold old fvs =
     if not (Mvs.mem o fvs) then sbs else match preold with
       | Some preold ->
           Mvs.add o (t_var (find_old pvm preold v).pv_vs) sbs
-      | None -> raise (UnboundLabel "'0") in
+      | None -> raise (UnboundLabel "0") in
   Hpv.fold rebase old Mvs.empty
 
 let rebase_pre env preold old pl =
@@ -923,8 +924,8 @@ let cty_of_spec env bl dsp dity =
   let ity = ity_of_dity dity in
   let bl = binders bl in
   let env = add_binders env bl in
-  let preold = Mstr.find_opt "'0" env.old in
-  let env, old = add_label env "'0" in
+  let preold = Mstr.find_opt "0" env.old in
+  let env, old = add_label env "0" in
   let dsp = get_later env dsp ity in
   let _, eff = effect_of_dspec dsp in
   let eff = eff_strong eff in
@@ -1193,9 +1194,9 @@ and rec_defn uloc env ghost {fds = dfdl} =
 
 and lambda uloc env pvl dsp dvl de =
   let env = add_binders env pvl in
+  let preold = Mstr.find_opt "0" env.old in
+  let env, old = add_label env "0" in
   let e = expr uloc env de in
-  let preold = Mstr.find_opt "'0" env.old in
-  let env, old = add_label env "'0" in
   let dsp = get_later env dsp e.e_ity in
   let dvl = get_later env dvl in
   let dvl = rebase_variant env preold old dvl in

src/mlw/dexpr.mli

@@ -58,7 +58,7 @@ exception UnboundLabel of string
 
 type register_old = pvsymbol -> string -> pvsymbol
   (** Program variables occurring under [old] or [at] are passed to
-      a registrar function. The label string must be ['0] for [old]. *)
+      a registrar function. The label string must be [0] for [old]. *)
 
 type 'a later = pvsymbol Mstr.t -> register_old -> 'a
   (** Specification terms are parsed and typechecked after the program

src/mlw/expr.ml

@@ -972,17 +972,20 @@ and print_capp pri s fmt vl = match extract_op s, vl with
 and print_cexp exec pri fmt {c_node = n; c_cty = c} = match n with
   | Cany when exec && c.cty_args = [] ->
       fprintf fmt "@[<hov 2>any %a%a@]" print_ity c.cty_result
-        (print_spec [] c.cty_pre c.cty_post c.cty_xpost c.cty_effect) None
+        (print_spec [] c.cty_pre c.cty_post c.cty_xpost
+          c.cty_oldies c.cty_effect) None
   | Cany ->
-      fprintf fmt "@[<hov 2>any%a@]" print_cty c
+      fprintf fmt "@[<hov 2>any%a@]" print_cty c;
+      forget_cty c
   | Cfun e when exec && c.cty_args = [] ->
       fprintf fmt "@[<hov 2>abstract%a@\n%a@]@\nend"
-        (print_spec [] c.cty_pre c.cty_post c.cty_xpost eff_empty) None
-        print_expr e
+        (print_spec [] c.cty_pre c.cty_post c.cty_xpost
+          c.cty_oldies eff_empty) None print_expr e
   | Cfun e ->
       fprintf fmt "@[<hov 2>fun%a ->@\n%a@]"
-        (print_spec c.cty_args c.cty_pre c.cty_post c.cty_xpost eff_empty) None
-        print_expr e
+        (print_spec c.cty_args c.cty_pre c.cty_post c.cty_xpost
+          c.cty_oldies eff_empty) None print_expr e;
+      forget_cty c
   | Capp (s,[]) when rs_equal s rs_true ->
       pp_print_string fmt "true"
   | Capp (s,[]) when rs_equal s rs_false ->
@@ -1011,7 +1014,7 @@ and print_enode pri fmt e = match e.e_node with
       fprintf fmt (protect_on (pri > 0) "%a@ in@\n%a")
         print_let_defn ld print_expr e;
       forget_let_defn ld
-  | Eif (e0,e1,e2) when is_e_false e1 && is_e_false e2 ->
+  | Eif (e0,e1,e2) when is_e_false e1 && is_e_true e2 ->
       fprintf fmt (protect_on (pri > 4) "not %a") (print_lexpr 4) e0
   | Eif (e0,e1,e2) when is_e_false e2 ->
       fprintf fmt (protect_on (pri > 3) "@[<hov 1>%a &&@ %a@]")
@@ -1019,6 +1022,9 @@ and print_enode pri fmt e = match e.e_node with
   | Eif (e0,e1,e2) when is_e_true e1 ->
       fprintf fmt (protect_on (pri > 2) "@[<hov 1>%a ||@ %a@]")
         (print_lexpr 3) e0 (print_lexpr 2) e2
+  | Eif (e0,e1,e2) when is_e_void e2 ->
+      fprintf fmt (protect_on (pri > 0) "if %a then %a")
+        print_expr e0 print_expr e1
   | Eif (e0,e1,e2) ->
       fprintf fmt (protect_on (pri > 0) "if %a then %a@ else %a")
         print_expr e0 print_expr e1 print_expr e2
@@ -1037,7 +1043,7 @@ and print_enode pri fmt e = match e.e_node with
         print_expr e0 (if ghost then ")" else "")
         (Pp.print_list Pp.newline print_branch) bl
   | Ewhile (d,inv,varl,e) ->
-      fprintf fmt "@[<hov 2]while %a do%a%a@\n%a@]@\ndone"
+      fprintf fmt "@[<hov 2>while %a do%a%a@\n%a@]@\ndone"
         print_expr d print_invariant inv print_variant varl print_expr e
   | Efor (pv,(pvfrom,dir,pvto),inv,e) ->
       fprintf fmt "@[<hov 2>for %a =@ %a@ %s@ %a@ %ado@\n%a@]@\ndone"
@@ -1081,10 +1087,15 @@ and print_let_defn fmt = function
         (if v.pv_ghost then "ghost " else "")
         print_pv v print_id_labels v.pv_vs.vs_name
         (print_lexpr 0 (*4*)) e
-  | LDsym (s,{c_node = Cfun e; c_cty = c}) ->
+  | LDsym (s,{c_node = Cfun e; c_cty = ({cty_args = _::_} as c)}) ->
       fprintf fmt "@[<hov 2>let %a%a =@\n%a@]"
         print_rs_head s print_cty c
-        (print_lexpr 0 (*4*)) e
+        (print_lexpr 0 (*4*)) e;
+      forget_cty c
+  | LDsym (s,{c_node = Cany; c_cty = ({cty_args = _::_} as c)}) ->
+      fprintf fmt "@[<hov 2>val %a%a@]"
+        print_rs_head s print_cty c;
+      forget_cty c
   | LDsym (s,c) ->
       fprintf fmt "@[<hov 2>let %a =@\n%a@]"
         print_rs_head s
@@ -1102,26 +1113,8 @@ and print_rec_fun fst fmt fd =
     print_rs_head fd.rec_sym
     print_cty fd.rec_fun.c_cty
     print_variant fd.rec_varl
-    (print_lexpr 0 (*4*)) e
-
-(*
-let print_val_decl fmt = function
-  | ValV v ->
-      fprintf fmt "@[<hov 2>val %s%a%a :@ %a@]"
-        (if v.pv_ghost then "ghost " else "")
-        print_pv v print_id_labels v.pv_vs.vs_name
-        print_ity v.pv_ity
-  | ValS ({rs_logic = RLpv v; rs_cty = c} as s) ->
-      fprintf fmt "@[<hov 2>val %a%a@]" print_rs_head s
-        (print_spec c.cty_args c.cty_pre (List.tl c.cty_post) c.cty_xpost
-          (Spv.remove v c.cty_reads) c.cty_effect) (Some c.cty_result)
-  | ValS ({rs_logic = RLls _; rs_cty = c} as s) ->
-      fprintf fmt "@[<hov 2>val %a%a@]" print_rs_head s
-        (print_spec c.cty_args c.cty_pre (List.tl c.cty_post) c.cty_xpost
-          c.cty_reads c.cty_effect) (Some c.cty_result)
-  | ValS s ->
-      fprintf fmt "@[<hov 2>val %a%a@]" print_rs_head s print_cty s.rs_cty
-*)
+    (print_lexpr 0 (*4*)) e;
+  forget_cty fd.rec_fun.c_cty
 
 (* exception handling *)
 
@@ -1130,10 +1123,4 @@ let () = Exn_printer.register (fun fmt e -> match e with
       "Function %a is not a constructor" print_rs s
   | FieldExpected s -> fprintf fmt
       "Function %a is not a mutable field" print_rs s
-(*
-  | ItyExpected _e -> fprintf fmt
-      "This expression is not a first-order value"
-  | CtyExpected _e -> fprintf fmt
-      "This expression is not a function and cannot be applied"
-*)
   | _ -> raise e)

src/mlw/ity.ml

@@ -1175,7 +1175,7 @@ exception FoundPrefix of pvsymbol list
 
 let unknown = create_pvsymbol (id_fresh "?") ity_unit
 
-let print_spec args pre post xpost eff fmt ity =
+let print_spec args pre post xpost oldies eff fmt ity =
   let dot fmt () = pp_print_char fmt '.' in
   let print_pfx reg fmt pfx = fprintf fmt "@[%a:@,%a@]"
     (Pp.print_list dot print_pv) pfx print_reg reg in
@@ -1206,6 +1206,8 @@ let print_spec args pre post xpost eff fmt ity =
         (Pp.print_list Pp.comma print_cvr) (Sreg.elements cvr) in
   let print_result fmt ity = fprintf fmt " :@ %a" print_ity ity in
   let print_pre fmt p = fprintf fmt "@\nrequires { @[%a@] }" print_term p in
+  let print_old fmt (o,v) =
+    fprintf fmt "@\nold { %a -> %a }" print_pv o print_pv v in
   let print_post fmt q =
     let v, q = open_post q in
     fprintf str_formatter "%a" print_vs v;
@@ -1225,18 +1227,24 @@ let print_spec args pre post xpost eff fmt ity =
   Pp.print_list_pre Pp.space print_pvty fmt args;
   Pp.print_option print_result fmt ity;
   if eff.eff_oneway then pp_print_string fmt " diverges";
-  if not (Spv.is_empty eff.eff_reads) then fprintf fmt "@\nreads  { %a }"
-    (Pp.print_list Pp.comma print_pv) (Spv.elements eff.eff_reads);
+  let reads = List.fold_right Spv.remove args eff.eff_reads in
+  if not (Spv.is_empty reads) then fprintf fmt "@\nreads  { %a }"
+    (Pp.print_list Pp.comma print_pv) (Spv.elements reads);
   if not (Mreg.is_empty eff.eff_writes) then fprintf fmt "@\nwrites { %a }"
     (Pp.print_list Pp.comma print_write) (Mreg.bindings eff.eff_writes);
   if not (Mreg.is_empty eff.eff_covers) then fprintf fmt "@\ncovers { %a }"
     (Pp.print_list Pp.comma print_raise) (Mreg.bindings eff.eff_covers);
   Pp.print_list Pp.nothing print_pre fmt pre;
+  Pp.print_list Pp.nothing print_old fmt (Mpv.bindings oldies);
   Pp.print_list Pp.nothing print_post fmt post;
   Pp.print_list Pp.nothing print_xpost fmt (Mexn.bindings xpost)
 
 let print_cty fmt c = print_spec c.cty_args c.cty_pre c.cty_post
-  c.cty_xpost c.cty_effect fmt (Some c.cty_result)
+  c.cty_xpost c.cty_oldies c.cty_effect fmt (Some c.cty_result)
+
+let forget_cty c =
+  List.iter forget_pv c.cty_args;
+  Mpv.iter (fun v _ -> forget_pv v) c.cty_oldies
 
 (** exception handling *)
 

src/mlw/ity.mli

@@ -394,6 +394,7 @@ val cty_add_post : cty -> post list -> cty
 
 val forget_reg : region -> unit   (* flush id_unique for a region *)
 val forget_pv  : pvsymbol -> unit (* flush for a program variable *)
+val forget_cty : cty -> unit      (* forget arguments and oldies *)
 
 val print_its : Format.formatter -> itysymbol -> unit (* type symbol *)
 val print_reg : Format.formatter -> region -> unit    (* region *)
@@ -406,5 +407,5 @@ val print_pvty : Format.formatter -> pvsymbol -> unit (* pvsymbol : type *)
 val print_cty  : Format.formatter -> cty -> unit      (* computation type *)
 
 val print_spec :
-  pvsymbol list -> pre list -> post list -> post list Mexn.t ->
-    effect -> Format.formatter -> ity option -> unit (* piecemeal cty *)
+  pvsymbol list -> pre list -> post list -> post list Mexn.t -> pvsymbol Mpv.t
+    -> effect -> Format.formatter -> ity option -> unit (* piecemeal cty *)

src/parser/lexer.mll

@@ -46,10 +46,9 @@
         "let", LET;
         "match", MATCH;
         "meta", META;
-        "scope", SCOPE;
         "not", NOT;
         "predicate", PREDICATE;
-        "prop", PROP;
+        "scope", SCOPE;
         "then", THEN;
         "theory", THEORY;
         "true", TRUE;
@@ -62,6 +61,7 @@
         "any", ANY;
         "assert", ASSERT;
         "assume", ASSUME;
+        "at", AT;
         "begin", BEGIN;
         "check", CHECK;
         "diverges", DIVERGES;
@@ -74,9 +74,10 @@
         "fun", FUN;
         "ghost", GHOST;
         "invariant", INVARIANT;
-        "loop", LOOP;
+        "label", LABEL;
         "module", MODULE;
         "mutable", MUTABLE;
+        "old", OLD;
         "private", PRIVATE;
         "raise", RAISE;
         "raises", RAISES;
@@ -158,8 +159,6 @@ rule token = parse
       { Lexlib.comment lexbuf; token lexbuf }
   | "'" (lident as id)
       { QUOTE_LIDENT id }
-  | "'" (uident as id)
-      { QUOTE_UIDENT id }
   | ","
       { COMMA }
   | "("

src/parser/parser.mly

@@ -96,21 +96,21 @@
 %token <Ptree.real_constant> FLOAT
 %token <string> STRING
 %token <Loc.position> POSITION
-%token <string> QUOTE_UIDENT QUOTE_LIDENT
+%token <string> QUOTE_LIDENT
 
 (* keywords *)
 
 %token AS AXIOM CLONE COINDUCTIVE CONSTANT
 %token ELSE END EPSILON EXISTS EXPORT FALSE FORALL FUNCTION
 %token GOAL IF IMPORT IN INDUCTIVE LEMMA
-%token LET MATCH META NOT PREDICATE PROP SCOPE
+%token LET MATCH META NOT PREDICATE SCOPE
 %token THEN THEORY TRUE TYPE USE WITH
 
 (* program keywords *)
 
-%token ABSTRACT ABSURD ANY ASSERT ASSUME BEGIN CHECK
+%token ABSTRACT ABSURD ANY ASSERT ASSUME AT BEGIN CHECK
 %token DIVERGES DO DONE DOWNTO ENSURES EXCEPTION FOR
-%token FUN GHOST INVARIANT LOOP MODULE MUTABLE
+%token FUN GHOST INVARIANT LABEL MODULE MUTABLE OLD
 %token PRIVATE RAISE RAISES READS REC REQUIRES RETURNS
 %token TO TRY VAL VARIANT WHILE WRITES
 
@@ -147,6 +147,7 @@
 %right AND AMPAMP
 %nonassoc NOT
 %left EQUAL LTGT OP1
+%nonassoc AT OLD
 %nonassoc LARROW
 %nonassoc RIGHTSQ    (* stronger than <- for e1[e2 <- e3] *)
 %left OP2
@@ -235,7 +236,9 @@ meta_arg:
 | CONSTANT  qualid  { Mfs $2 }
 | FUNCTION  qualid  { Mfs $2 }
 | PREDICATE qualid  { Mps $2 }
-| PROP      qualid  { Mpr $2 }
+| AXIOM     qualid  { Max $2 }
+| LEMMA     qualid  { Mlm $2 }
+| GOAL      qualid  { Mgl $2 }
 | STRING            { Mstr $1 }
 | INTEGER           { Mint (small_integer $1) }
 
@@ -460,6 +463,10 @@ term_:
       | Tinfix (l,o,r) -> Tinnfix (l,o,r) | d -> d }
 | NOT term
     { Tunop (Tnot, $2) }
+| OLD term
+    { Tat ($2, mk_id "0" $startpos($1) $endpos($1)) }
+| term AT uident
+    { Tat ($1, $3) }
 | prefix_op term %prec prec_prefix_op
     { Tidapp (Qident $1, [$2]) }
 | l = term ; o = bin_op ; r = term
@@ -515,7 +522,6 @@ term_arg_:
 | numeral                   { Tconst $1 }
 | TRUE                      { Ttrue }
 | FALSE                     { Tfalse }
-| quote_uident              { Tident (Qident $1) }
 | o = oppref ; a = term_arg { Tidapp (Qident o, [a]) }
 | term_sub_                 { $1 }
 
@@ -576,7 +582,7 @@ numeral:
 pdecl:
 | VAL ghost kind labels(lident_rich) mk_expr(val_defn) { Dlet ($4, $2, $3, $5) }
 | LET ghost kind labels(lident_rich) mk_expr(fun_defn) { Dlet ($4, $2, $3, $5) }
-| LET ghost kind labels(lident_rich) EQUAL expr        { Dlet ($4, $2, $3, $6) }
+| LET ghost kind labels(lident_rich) EQUAL seq_expr    { Dlet ($4, $2, $3, $6) }
 | LET REC with_list1(rec_defn)                         { Drec $3 }
 | EXCEPTION labels(uident)                             { Dexn ($2, PTtuple []) }
 | EXCEPTION labels(uident) ty                          { Dexn ($2, $3) }
@@ -624,7 +630,7 @@ expr_:
     { Eand ($1, $3) }
 | expr BARBAR expr
     { Eor ($1, $3) }
-| NOT expr %prec prec_prefix_op
+| NOT expr
     { Enot $2 }
 | prefix_op expr %prec prec_prefix_op
     { Eidapp (Qident $1, [$2]) }
@@ -680,20 +686,18 @@ expr_:
     { Ematch ($2, $4) }
 | MATCH comma_list2(expr) WITH match_cases(seq_expr) END
     { Ematch (mk_expr (Etuple $2) $startpos($2) $endpos($2), $4) }
-| quote_uident COLON seq_expr
-    { Emark ($1, $3) }
-| LOOP loop_annotation seq_expr END
-    { let inv, var = $2 in Eloop (inv, var, $3) }
+| LABEL labels(uident) IN seq_expr
+    { Emark ($2, $4) }
 | WHILE seq_expr DO loop_annotation seq_expr DONE
     { let inv, var = $4 in Ewhile ($2, inv, var, $5) }
 | FOR lident EQUAL seq_expr for_direction seq_expr DO invariant* seq_expr DONE
     { Efor ($2, $4, $5, $6, $8, $9) }
 | ABSURD
     { Eabsurd }
-| RAISE uqualid
-    { Eraise ($2, None) }
-| RAISE LEFTPAR uqualid seq_expr RIGHTPAR
-    { Eraise ($3, Some $4) }
+| RAISE uqualid expr_arg?
+    { Eraise ($2, $3) }
+| RAISE LEFTPAR uqualid expr_arg? RIGHTPAR
+    { Eraise ($3, $4) }
 | TRY seq_expr WITH bar_list1(exn_handler) END
     { Etry ($2, $4) }
 | GHOST expr
@@ -847,13 +851,10 @@ ident:
 | lident { $1 }
 
 uident:
-| UIDENT          { mk_id $1 $startpos $endpos }
+| UIDENT        { mk_id $1 $startpos $endpos }
 
 lident:
-| LIDENT          { mk_id $1 $startpos $endpos }
-
-quote_uident:
-| QUOTE_UIDENT  { mk_id ("'" ^ $1) $startpos $endpos }
+| LIDENT        { mk_id $1 $startpos $endpos }
 
 quote_lident:
 | QUOTE_LIDENT  { mk_id $1 $startpos $endpos }

src/parser/ptree.ml

@@ -94,6 +94,7 @@ and term_desc =
   | Ttuple of term list
   | Trecord of (qualid * term) list
   | Tupdate of term * (qualid * term) list
+  | Tat of term * ident
 
 (*s Declarations. *)
 
@@ -158,7 +159,9 @@ type metarg =
   | Mty  of pty
   | Mfs  of qualid
   | Mps  of qualid
-  | Mpr  of qualid
+  | Max  of qualid
+  | Mlm  of qualid
+  | Mgl  of qualid
   | Mstr of string
   | Mint of int
 
@@ -209,7 +212,6 @@ and expr_desc =
   (* control *)
   | Esequence of expr * expr
   | Eif of expr * expr * expr
-  | Eloop of invariant * variant * expr
   | Ewhile of expr * invariant * variant * expr
   | Eand of expr * expr
   | Eor of expr * expr

src/parser/typing.ml

@@ -72,11 +72,20 @@ let find_psymbol_ns ns q =
   if ls.ls_value = None then ls else
     Loc.error ~loc:(qloc q) (PredicateSymbolExpected ls)
 
-let find_prop     tuc q = find_prop_ns     (Theory.get_namespace tuc) q
 let find_tysymbol tuc q = find_tysymbol_ns (Theory.get_namespace tuc) q
 let find_lsymbol  tuc q = find_lsymbol_ns  (Theory.get_namespace tuc) q
 let find_fsymbol  tuc q = find_fsymbol_ns  (Theory.get_namespace tuc) q
 let find_psymbol  tuc q = find_psymbol_ns  (Theory.get_namespace tuc) q
+let find_prop     tuc q = find_prop_ns     (Theory.get_namespace tuc) q
+
+let find_prop_of_kind k tuc q =
+  let pr = find_prop tuc q in
+  match (Mid.find pr.pr_name (Theory.get_known tuc)).d_node with
+  | Dprop (l,_,_) when l = k -> pr
+  | _ -> Loc.errorm ~loc:(qloc q) "proposition %a is not %s"
+      print_qualid q (match k with
+        | Plemma -> "a lemma" | Paxiom -> "an axiom"
+        | Pgoal  -> "a goal"  | Pskip  -> assert false (* what? *))
 
 let find_itysymbol_ns ns q =
   find_qualid (fun s -> s.its_ts.ts_name) Pmodule.ns_find_its ns q
@@ -218,7 +227,7 @@ let mk_closure loc ls =
   let vl = Lists.mapi mk_v ls.ls_args in
   DTquant (DTlambda, vl, [], mk (DTapp (ls, List.map mk_t vl)))
 
-let rec dterm tuc gvars denv {term_desc = desc; term_loc = loc} =
+let rec dterm tuc gvars at denv {term_desc = desc; term_loc = loc} =
   let func_app e el =
     List.fold_left (fun e1 (loc, e2) ->
       DTfapp (Dterm.dterm ~loc e1, e2)) e el
@@ -228,7 +237,7 @@ let rec dterm tuc gvars denv {term_desc = desc; term_loc = loc} =
     | [], _ -> func_app (DTapp (ls, List.rev_map snd al)) el
     | _, [] -> func_app (mk_closure loc ls) (List.rev_append al el)
   in
-  let qualid_app q el = match gvars q with
+  let qualid_app q el = match gvars at q with
     | Some v -> func_app (DTgvar v.pv_vs) el
     | None ->
         let ls = find_lsymbol tuc q in
@@ -242,24 +251,24 @@ let rec dterm tuc gvars denv {term_desc = desc; term_loc = loc} =
     | _ -> qualid_app q el
   in
   let rec unfold_app e1 e2 el = match e1.term_desc with
-    | Tapply (e11,e12) ->
-        let e12 = dterm tuc gvars denv e12 in
+    | Ptree.Tapply (e11,e12) ->
+        let e12 = dterm tuc gvars at denv e12 in
         unfold_app e11 e12 ((e1.term_loc, e2)::el)
-    | Tident q ->
+    | Ptree.Tident q ->
         qualid_app q ((e1.term_loc, e2)::el)
     | _ ->
-        func_app (DTfapp (dterm tuc gvars denv e1, e2)) el
+        func_app (DTfapp (dterm tuc gvars at denv e1, e2)) el
   in
   Dterm.dterm ~loc (match desc with
   | Ptree.Tident q ->
       qualid_app q []
   | Ptree.Tidapp (q, tl) ->
-      let tl = List.map (dterm tuc gvars denv) tl in
+      let tl = List.map (dterm tuc gvars at denv) tl in
       DTapp (find_lsymbol tuc q, tl)
   | Ptree.Tapply (e1, e2) ->
-      unfold_app e1 (dterm tuc gvars denv e2) []
+      unfold_app e1 (dterm tuc gvars at denv e2) []
   | Ptree.Ttuple tl ->
-      let tl = List.map (dterm tuc gvars denv) tl in
+      let tl = List.map (dterm tuc gvars at denv) tl in