parsing epsilon expressions

src/parser/lexer.mll

@@ -49,6 +49,7 @@
 	"clone", CLONE;
 	"else", ELSE;
 	"end", END;
+	"epsilon", EPSILON;
 	"exists", EXISTS;
 	"export", EXPORT;
         "false", FALSE;
@@ -161,8 +162,6 @@ rule token = parse
       { LEFTPAR }
   | ")"
       { RIGHTPAR }
-  | "!"
-      { BANG }
   | ":"
       { COLON }
   | "->"
@@ -177,18 +176,12 @@ rule token = parse
       { OP2 (String.make 1 c) }
   | "*" | "/" | "%" as c
       { OP3 (String.make 1 c) }
-  | "@"
-      { AT }
   | "."
       { DOT }
   | "["
       { LEFTSQ }
   | "]"
       { RIGHTSQ }
-  | "{"
-      { LEFTB }
-  | "}"
-      { RIGHTB }
   | "|"
       { BAR }
   | "\""

src/parser/parser.mly

@@ -54,25 +54,21 @@
 
 /* keywords */
 
-%token AND AS AXIOM 
-%token CLONE 
-%token ELSE END EXISTS EXPORT FALSE FORALL  
-%token GOAL
-%token IF IMPORT IN INDUCTIVE LEMMA 
-%token LET LOGIC MATCH 
-%token NAMESPACE NOT OR  
-%token THEN THEORY TRUE TYPE
-%token USE WITH
+%token AND AS AXIOM CLONE 
+%token ELSE END EPSILON EXISTS EXPORT FALSE FORALL  
+%token GOAL IF IMPORT IN INDUCTIVE LEMMA 
+%token LET LOGIC MATCH NAMESPACE NOT OR  
+%token THEN THEORY TRUE TYPE USE WITH
 
 /* symbols */
 
-%token ARROW AT
-%token BANG BAR 
+%token ARROW
+%token BAR 
 %token COLON COMMA  
 %token DOT EQUAL
-%token LEFTB LEFTPAR LEFTSQ 
+%token LEFTPAR LEFTSQ 
 %token LRARROW
-%token QUOTE RIGHTB 
+%token QUOTE
 %token RIGHTPAR RIGHTSQ 
 %token UNDERSCORE
 
@@ -81,30 +77,25 @@
 
 /* Precedences */
 
-%left LEFTB 
-
-%left COLON 
-
-%left IN
+%nonassoc prec_decls
+%nonassoc LOGIC TYPE INDUCTIVE
 
-%left ELSE
+%nonassoc COLON 
+%nonassoc ELSE
+%nonassoc IN
+%nonassoc DOT
 
-%right prec_named
-%right prec_quant
+%nonassoc prec_named
 %right ARROW LRARROW
 %right OR 
 %right AND 
-%right NOT
-%right prec_if
+%nonassoc NOT
 %left EQUAL OP0
 %left OP1
 %left OP2
 %left OP3
-%right unary_op
-%left LEFTSQ
-
-%nonassoc prec_decls
-%nonassoc LOGIC TYPE INDUCTIVE
+%nonassoc prefix_op
+%nonassoc postfix_op
 
 /* Entry points */
 
@@ -385,11 +376,11 @@ lexpr:
 | lexpr OP3 lexpr 
    { let id = { id = infix $2; id_loc = loc_i 2 } in
      mk_pp (PPapp (Qident id, [$1; $3])) }
-| any_op lexpr %prec unary_op
+| any_op lexpr %prec prefix_op
    { let id = { id = prefix $1; id_loc = loc_i 2 } in
      mk_pp (PPapp (Qident id, [$2])) }
 /*
-| lexpr any_op %prec unary_op
+| lexpr any_op %prec postfix_op
    { let id = { id = postfix $2; id_loc = loc_i 2 } in
      mk_pp (PPapp (Qident id, [$1])) }
 */
@@ -397,11 +388,11 @@ lexpr:
    { mk_pp (PPvar $1) }
 | qualid LEFTPAR list1_lexpr_sep_comma RIGHTPAR
    { mk_pp (PPapp ($1, $3)) }
-| IF lexpr THEN lexpr ELSE lexpr %prec prec_if 
+| IF lexpr THEN lexpr ELSE lexpr
    { mk_pp (PPif ($2, $4, $6)) }
-| FORALL list1_uquant_sep_comma triggers DOT lexpr %prec prec_quant
+| FORALL list1_uquant_sep_comma triggers DOT lexpr
    { mk_pp (PPquant (PPforall, $2, $3, $5)) }
-| EXISTS list1_uquant_sep_comma triggers DOT lexpr %prec prec_quant
+| EXISTS list1_uquant_sep_comma triggers DOT lexpr
    { mk_pp (PPquant (PPexists, $2, $3, $5)) }
 | INTEGER
    { mk_pp (PPconst (Term.ConstInt $1)) }
@@ -419,6 +410,8 @@ lexpr:
    { mk_pp (PPlet ($2, $4, $6)) }
 | MATCH list1_lexpr_sep_comma WITH bar_ match_cases END
    { mk_pp (PPmatch ($2, $5)) }
+| EPSILON lident COLON primitive_type DOT lexpr
+   { mk_pp (PPeps ($2, $4, $6)) }
 | lexpr COLON primitive_type
    { mk_pp (PPcast ($1, $3)) }
 ;
@@ -449,6 +442,7 @@ pattern:
 | uqualid                                       { mk_pat (PPpapp ($1, [])) }
 | uqualid LEFTPAR list1_pat_sep_comma RIGHTPAR  { mk_pat (PPpapp ($1, $3)) }
 | pattern AS lident                             { mk_pat (PPpas ($1,$3)) }
+| LEFTPAR pattern RIGHTPAR                      { $2 }
 ;
 
 triggers:

src/parser/ptree.mli

@@ -72,7 +72,7 @@ and pp_desc =
   | PPquant of pp_quant * uquant list * lexpr list list * lexpr
   | PPnamed of string * lexpr
   | PPlet of ident * lexpr * lexpr
-(*  | PPeps of ident * lexpr *)
+  | PPeps of ident * pty * lexpr
   | PPmatch of lexpr list * (pattern list * lexpr) list
   | PPcast of lexpr * pty
 

src/parser/typing.ml

@@ -266,7 +266,7 @@ and dterm_node =
   | Tlet of dterm * string * dterm
   | Tmatch of dterm list * (dpattern list * dterm) list
   | Tnamed of string * dterm
-  | Teps of string * dfmla
+  | Teps of string * dty * dfmla
 
 and dfmla =
   | Fapp of lsymbol * dterm list
@@ -413,6 +413,11 @@ and dterm_node loc env = function
       let ty = dty env ty in
       if not (unify e1.dt_ty ty) then term_expected_type ~loc e1.dt_ty ty;
       e1.dt_node, ty
+  | PPeps ({id=x}, ty, e1) ->
+      let ty = dty env ty in
+      let env = { env with dvars = Mstr.add x ty env.dvars } in
+      let e1 = dfmla env e1 in
+      Teps (x, ty, e1), ty
   | PPquant _ | PPif _
   | PPprefix _ | PPinfix _ | PPfalse | PPtrue ->
       error ~loc TermExpected
@@ -474,7 +479,7 @@ and dfmla env e = match e.pp_desc with
       Fnamed (x, f1)
   | PPvar x ->
       Fvar (snd (find_prop x env.uc))
-  | PPconst _ | PPcast _ ->
+  | PPeps _ | PPconst _ | PPcast _ ->
       error ~loc:e.pp_loc PredicateExpected
 
 and dpat_list env tl pl =
@@ -551,8 +556,12 @@ let rec term env t = match t.dt_node with
   | Tnamed (x, e1) ->
       let e1 = term env e1 in
       t_label_add x e1
-  | Teps _ ->
-      assert false (*TODO*)
+  | Teps (x, ty, e1) ->
+      let ty = ty_of_dty ty in
+      let v = create_vsymbol (id_fresh x) ty in
+      let env = Mstr.add x v env in
+      let e1 = fmla env e1 in
+      t_eps v e1
 
 and fmla env = function
   | Ftrue ->