Parser: "let <kind>" definitions

src/parser/parser.mly

@@ -574,27 +574,33 @@ numeral:
 (* Program declarations *)
 
 pdecl:
-| VAL top_ghost labels(lident_rich) mk_expr(val_defn) { Dlet ($3, $2, $4) }
-| LET top_ghost labels(lident_rich) mk_expr(fun_defn) { Dlet ($3, $2, $4) }
-| LET top_ghost labels(lident_rich) EQUAL expr        { Dlet ($3, $2, $5) }
-| LET REC with_list1(rec_defn)                        { Drec $3 }
-| EXCEPTION labels(uident)                            { Dexn ($2, PTtuple []) }
-| EXCEPTION labels(uident) ty                         { Dexn ($2, $3) }
-
-top_ghost:
-| (* epsilon *) { Gnone  }
-| GHOST         { Gghost }
-| LEMMA         { Glemma }
+| 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 REC with_list1(rec_defn)                         { Drec $3 }
+| EXCEPTION labels(uident)                             { Dexn ($2, PTtuple []) }
+| EXCEPTION labels(uident) ty                          { Dexn ($2, $3) }
+
+ghost:
+| (* epsilon *) { false }
+| GHOST         { true }
+
+kind:
+| (* epsilon *) { Expr.RKnone }
+| FUNCTION      { Expr.RKfunc }
+| CONSTANT      { Expr.RKfunc }
+| PREDICATE     { Expr.RKpred }
+| LEMMA         { Expr.RKlemma }
 
 (* Function definitions *)
 
 rec_defn:
-| top_ghost labels(lident_rich) binders cast? spec EQUAL spec seq_expr
-    { $2, $1, ($3, $4, spec_union $5 $7, $8) }
+| ghost kind labels(lident_rich) binders cast? spec EQUAL spec seq_expr
+    { $3, $1, $2, $4, $5, spec_union $6 $8, $9 }
 
 fun_defn:
 | binders cast? spec EQUAL spec seq_expr
-    { Elam ($1, $2, spec_union $3 $5, $6) }
+    { Efun ($1, $2, spec_union $3 $5, $6) }
 
 val_defn:
 | params cast spec  { Eany ($1, $2, $3) }
@@ -637,38 +643,39 @@ expr_:
       | Eidapp (Qident id, [e1;e2]) when id.id_str = mixfix "[]" ->
           Eidapp (Qident {id with id_str = mixfix "[]<-"}, [e1;e2;$3])
       | _ -> raise Error }
-| LET top_ghost pattern EQUAL seq_expr IN seq_expr
-    { match $3.pat_desc with
-      | Pvar id -> Elet (id, $2, $5, $7)
-      | Pwild -> Elet (id_anonymous $3.pat_loc, $2, $5, $7)
-      | Ptuple [] -> Elet (id_anonymous $3.pat_loc, $2,
-          { $5 with expr_desc = Ecast ($5, PTtuple []) }, $7)
+| LET ghost kind pattern EQUAL seq_expr IN seq_expr
+    { match $4.pat_desc with
+      | Pvar id -> Elet (id, $2, $3, $6, $8)
+      | Pwild -> Elet (id_anonymous $4.pat_loc, $2, $3, $6, $8)
+      | Ptuple [] -> Elet (id_anonymous $4.pat_loc, $2, $3,
+          { $6 with expr_desc = Ecast ($6, PTtuple []) }, $8)
       | Pcast ({pat_desc = Pvar id}, ty) ->
-          Elet (id, $2, { $5 with expr_desc = Ecast ($5, ty) }, $7)
+          Elet (id, $2, $3, { $6 with expr_desc = Ecast ($6, ty) }, $8)
       | Pcast ({pat_desc = Pwild}, ty) ->
-          let id = id_anonymous $3.pat_loc in
-          Elet (id, $2, { $5 with expr_desc = Ecast ($5, ty) }, $7)
+          let id = id_anonymous $4.pat_loc in
+          Elet (id, $2, $3, { $6 with expr_desc = Ecast ($6, ty) }, $8)
       | _ ->
-          let e = match $2 with
-            | Glemma -> Loc.errorm ~loc:($3.pat_loc)
-                "`let lemma' cannot be used with complex patterns"
-            | Gghost -> { $5 with expr_desc = Eghost $5 }
-            | Gnone -> $5 in
-          Ematch (e, [$3, $7]) }
-| LET top_ghost labels(lident_op_id) EQUAL seq_expr IN seq_expr
-    { Elet ($3, $2, $5, $7) }
-| LET top_ghost labels(lident) mk_expr(fun_defn) IN seq_expr
-    { Elet ($3, $2, $4, $6) }
-| LET top_ghost labels(lident_op_id) mk_expr(fun_defn) IN seq_expr
-    { Elet ($3, $2, $4, $6) }
+          let e = if $2 then { $6 with expr_desc = Eghost $6 } else $6 in
+          (match $3 with
+          | Expr.RKnone -> Ematch (e, [$4, $8])
+          | _ -> Loc.errorm ~loc:($4.pat_loc)
+              "`let <kind>' cannot be used with complex patterns") }
+| LET ghost kind labels(lident_op_id) EQUAL seq_expr IN seq_expr
+    { Elet ($4, $2, $3, $6, $8) }
+| LET ghost kind labels(lident) mk_expr(fun_defn) IN seq_expr
+    { Elet ($4, $2, $3, $5, $7) }
+| LET ghost kind labels(lident_op_id) mk_expr(fun_defn) IN seq_expr
+    { Elet ($4, $2, $3, $5, $7) }
 | LET REC with_list1(rec_defn) IN seq_expr
     { Erec ($3, $5) }
 | FUN binders spec ARROW spec seq_expr
-    { Elam ($2, None, spec_union $3 $5, $6) }
+    { Efun ($2, None, spec_union $3 $5, $6) }
+| ABSTRACT spec seq_expr END
+    { Efun ([], None, $2, $3) }
 | ANY ty spec
     { Eany ([], $2, $3) }
-| VAL top_ghost labels(lident_rich) mk_expr(val_defn) IN seq_expr
-    { Elet ($3, $2, $4, $6) }
+| VAL ghost kind labels(lident_rich) mk_expr(val_defn) IN seq_expr
+    { Elet ($4, $2, $3, $5, $7) }
 | MATCH seq_expr WITH match_cases(seq_expr) END
     { Ematch ($2, $4) }
 | MATCH comma_list2(expr) WITH match_cases(seq_expr) END
@@ -691,8 +698,6 @@ expr_:
     { Etry ($2, $4) }
 | GHOST expr
     { Eghost $2 }
-| ABSTRACT spec seq_expr END
-    { Eabstract($2, $3) }
 | assertion_kind LEFTBRC term RIGHTBRC
     { Eassert ($1, $3) }
 | label expr %prec prec_named

src/parser/ptree.ml

@@ -183,8 +183,6 @@ type spec = {
   sp_diverge : bool;
 }
 
-type top_ghost = Gnone | Gghost | Glemma
-
 type expr = {
   expr_desc : expr_desc;
   expr_loc  : loc;
@@ -200,10 +198,10 @@ and expr_desc =
   | Eapply of expr * expr
   | Einfix of expr * ident * expr
   | Einnfix of expr * ident * expr
-  | Elet of ident * top_ghost * expr * expr
-  | Efun of ident * top_ghost * lambda * expr
+  | Elet of ident * ghost * Expr.rs_kind * expr * expr
   | Erec of fundef list * expr
-  | Elam of lambda
+  | Efun of binder list * pty option * spec * expr
+  | Eany of param list * pty * spec
   | Etuple of expr list
   | Erecord of (qualid * expr) list
   | Eupdate of expr * (qualid * expr) list
@@ -225,16 +223,11 @@ and expr_desc =
   | Eassert of Expr.assertion_kind * term
   | Emark of ident * expr
   | Ecast of expr * pty
-  | Eany of any
   | Eghost of expr
-  | Eabstract of spec * expr
   | Enamed of label * expr
 
-and fundef = ident * top_ghost * lambda
-
-and lambda = binder list * pty option * spec * expr
-
-and any = param list * pty * spec
+and fundef =
+  ident * ghost * Expr.rs_kind * binder list * pty option * spec * expr
 
 type decl =
   | Dtype of type_decl list
@@ -242,6 +235,6 @@ type decl =
   | Dind of Decl.ind_sign * ind_decl list
   | Dprop of Decl.prop_kind * ident * term
   | Dmeta of ident * metarg list
-  | Dlet of ident * top_ghost * expr
+  | Dlet of ident * ghost * Expr.rs_kind * expr
   | Drec of fundef list
   | Dexn of ident * pty

src/parser/typing.ml

@@ -634,28 +634,29 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
       let cs,fl = parse_record ~loc muc get_val fl in
       let d = expr_app loc (DErs cs) fl in
       if re then d else mk_let ~loc "_q " e1 d
-  | Ptree.Elet (id, gh, e1, e2) ->
-      let gh, kind = match gh with
-        | Gnone -> false, RKnone
-        | Gghost -> true, RKnone
-        | Glemma -> true, RKlemma in
+  | Ptree.Elet (id, gh, kind, e1, e2) ->
       let ld = create_user_id id, gh, kind, dexpr muc denv e1 in
       DElet (ld, dexpr muc (denv_add_let denv ld) e2)
-  | Ptree.Efun (id, gh, lam, e2) ->
-      let gh, kind = match gh with
-        | Gnone -> false, RKnone
-        | Gghost -> true, RKnone
-        | Glemma -> true, RKlemma in
-      let e1 = Dexpr.dexpr (dlambda muc denv lam) in
-      let ld = create_user_id id, gh, kind, e1 in
-      DElet (ld, dexpr muc (denv_add_let denv ld) e2)
   | Ptree.Erec (fdl, e1) ->
       let denv, rd = drec_defn muc denv fdl in
       DErec (rd, dexpr muc denv e1)
-  | Ptree.Elam lam ->
-      dlambda muc denv lam
-  | Ptree.Eany any ->
-      dany muc any
+  | Ptree.Efun (bl, pty, sp, e) ->
+      let bl = List.map (dbinder muc) bl in
+      let e = match pty with
+        | Some pty -> { e with expr_desc = Ecast (e, pty) }
+        | None -> e in
+      let ds = match sp.sp_variant with
+        | ({term_loc = loc},_)::_ ->
+            Loc.errorm ~loc "unexpected 'variant' clause"
+        | _ -> dspec muc sp in
+      DEfun (bl, ds, dexpr muc (denv_add_args denv bl) e)
+  | Ptree.Eany (pl, pty, sp) ->
+      let pl = List.map (dparam muc) pl in
+      let ds = match sp.sp_variant with
+        | ({term_loc = loc},_)::_ ->
+            Loc.errorm ~loc "unexpected 'variant' clause"
+        | _ -> dspec muc sp in
+      DEany (pl, ds, dity_of_ity (ity_of_pty muc pty))
   | Ptree.Ematch (e1, bl) ->
       let e1 = dexpr muc denv e1 in
       let branch (pp, e) =
@@ -723,10 +724,6 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
       DEtry (e1, List.map branch cl)
   | Ptree.Eghost e1 ->
       DEghost (dexpr muc denv e1)
-  | Ptree.Eabstract (sp, e1) ->
-      if sp.sp_variant <> [] then
-        Loc.errorm ~loc "unexpected 'variant' clause";
-      DEfun ([], dspec muc sp, dexpr muc denv e1)
   | Ptree.Eabsurd -> DEabsurd
   | Ptree.Eassert (ak, lexpr) ->
       DEassert (ak, dassert muc lexpr)
@@ -740,11 +737,7 @@ let rec dexpr muc denv {expr_desc = desc; expr_loc = loc} =
       DEcast (dexpr muc denv e1, ity_of_pty muc pty))
 
 and drec_defn muc denv fdl =
-  let prep (id, gh, (bl, pty, sp, e)) =
-    let gh, kind = match gh with
-      | Gnone -> false, RKnone
-      | Gghost -> true, RKnone
-      | Glemma -> true, RKlemma in
+  let prep (id, gh, kind, bl, pty, sp, e) =
     let bl = List.map (dbinder muc) bl in
     let dity = match pty with
       | Some pty -> dity_of_ity (ity_of_pty muc pty)
@@ -755,25 +748,6 @@ and drec_defn muc denv fdl =
     create_user_id id, gh, kind, bl, dity, pre in
   Dexpr.drec_defn denv (List.map prep fdl)
 
-and dlambda muc denv (bl, pty, sp, e) =
-  let bl = List.map (dbinder muc) bl in
-  let e = match pty with
-    | Some pty -> { e with expr_desc = Ecast (e, pty) }
-    | None -> e in
-  let ds = match sp.sp_variant with
-    | ({term_loc = loc},_)::_ ->
-        Loc.errorm ~loc "unexpected 'variant' clause"
-    | _ -> dspec muc sp in
-  DEfun (bl, ds, dexpr muc (denv_add_args denv bl) e)
-
-and dany muc (pl, pty, sp) =
-  let pl = List.map (dparam muc) pl in
-  let ds = match sp.sp_variant with
-    | ({term_loc = loc},_)::_ ->
-        Loc.errorm ~loc "unexpected 'variant' clause"
-    | _ -> dspec muc sp in
-  DEany (pl, ds, dity_of_ity (ity_of_pty muc pty))
-
 (** Typing declarations *)
 
 open Pdecl
@@ -1039,11 +1013,7 @@ let add_decl muc inth d =
   | _ when inth ->
       (* TODO: should we allow "let function"? what about mixed letrecs? *)
       Loc.errorm "Program declarations are not allowed in pure theories"
-  | Ptree.Dlet (id, gh, e) ->
-      let gh, kind = match gh with
-        | Gnone -> false, RKnone
-        | Gghost -> true, RKnone
-        | Glemma -> true, RKlemma in
+  | Ptree.Dlet (id, gh, kind, e) ->
       let ld = create_user_id id, gh, kind, dexpr muc denv_empty e in
       add_pdecl ~vc muc (create_let_decl (let_defn ~keep_loc:true ld))
   | Ptree.Drec fdl ->