Parser: use the same syntax for functions in logic and programs

In logic, a lambda-term is written (fun (x y : int) -> term).
Also, local function definitions (let f x = t1 in t2) are allowed
and translated as (let f = fun x -> t1 in t2).

src/parser/lexer.mll

@@ -104,7 +104,7 @@ let hexadigit = ['0'-'9' 'a'-'f' 'A'-'F']
 
 let op_char_1 = ['=' '<' '>' '~']
 let op_char_2 = ['+' '-']
-let op_char_3 = ['*' '/' '%']
+let op_char_3 = ['*' '/' '%' '\\']
 let op_char_4 = ['!' '$' '&' '?' '@' '^' '.' ':' '|' '#']
 let op_char_34 = op_char_3 | op_char_4
 let op_char_234 = op_char_2 | op_char_34
@@ -188,8 +188,6 @@ rule token = parse
       { AND }
   | "\\/"
       { OR }
-  | "\\"
-      { LAMBDA }
   | "."
       { DOT }
   | ".."

src/parser/parser.mly

@@ -119,7 +119,7 @@
 %token AND ARROW
 %token BAR
 %token COLON COMMA
-%token DOT DOTDOT EQUAL LAMBDA LTGT
+%token DOT DOTDOT EQUAL LTGT
 %token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTSQ
 %token LARROW LRARROW OR
 %token RIGHTPAR RIGHTSQ
@@ -483,12 +483,20 @@ term_:
           let id = id_anonymous $2.pat_loc in
           Tlet (id, { $4 with term_desc = Tcast ($4, ty) }, $6)
       | _ -> Tmatch ($4, [$2, $6]) }
+| LET labels(lident_op_id) EQUAL term IN term
+    { Tlet ($2, $4, $6) }
+| LET labels(lident) mk_term(lam_defn) IN term
+    { Tlet ($2, $3, $5) }
+| LET labels(lident_op_id) mk_term(lam_defn) IN term
+    { Tlet ($2, $3, $5) }
 | MATCH term WITH match_cases(term) END
     { Tmatch ($2, $4) }
 | MATCH comma_list2(term) WITH match_cases(term) END
     { Tmatch (mk_term (Ttuple $2) $startpos($2) $endpos($2), $4) }
 | quant comma_list1(quant_vars) triggers DOT term
     { Tquant ($1, List.concat $2, $3, $5) }
+| FUN binders ARROW term
+    { Tquant (Tlambda, $2, [], $4) }
 | EPSILON
     { Loc.errorm "Epsilon terms are currently not supported in WhyML" }
 | label term %prec prec_named
@@ -496,6 +504,9 @@ term_:
 | term cast
     { Tcast ($1, $2) }
 
+lam_defn:
+| binders EQUAL term  { Tquant (Tlambda, $1, [], $3) }
+
 term_arg: mk_term(term_arg_) { $1 }
 term_dot: mk_term(term_dot_) { $1 }
 
@@ -555,7 +566,6 @@ triggers:
 quant:
 | FORALL  { Tforall }
 | EXISTS  { Texists }
-| LAMBDA  { Tlambda }
 
 numeral:
 | INTEGER { Number.ConstInt $1 }
@@ -564,28 +574,18 @@ numeral:
 (* Program declarations *)
 
 pdecl:
-| VAL top_ghost labels(lident_rich) type_v          { Dval ($3, $2, $4) }
-| LET top_ghost labels(lident_rich) fun_defn        { Dfun ($3, $2, $4) }
-| LET top_ghost labels(lident_rich) EQUAL fun_expr  { Dfun ($3, $2, $5) }
-| LET REC with_list1(rec_defn)                      { Drec $3 }
-| EXCEPTION labels(uident)                          { Dexn ($2, PTtuple []) }
-| EXCEPTION labels(uident) ty                       { Dexn ($2, $3) }
+| 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 }
 
-(* Function declarations *)
-
-type_v:
-| params cast spec  { ($1, $2, $3) }
-
-(*
-simple_type_c:
-| ty spec { PTpure $1, $2 }
-*)
-
 (* Function definitions *)
 
 rec_defn:
@@ -593,10 +593,11 @@ rec_defn:
     { $2, $1, ($3, $4, spec_union $5 $7, $8) }
 
 fun_defn:
-| binders cast? spec EQUAL spec seq_expr { ($1, $2, spec_union $3 $5, $6) }
+| binders cast? spec EQUAL spec seq_expr
+    { Elam ($1, $2, spec_union $3 $5, $6) }
 
-fun_expr:
-| FUN binders spec ARROW spec seq_expr { ($2, None, spec_union $3 $5, $6) }
+val_defn:
+| params cast spec  { Eany ($1, $2, $3) }
 
 (* Program expressions *)
 
@@ -656,15 +657,17 @@ expr_:
           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) fun_defn IN seq_expr
-    { Efun ($3, $2, $4, $6) }
-| LET top_ghost labels(lident_op_id) fun_defn IN seq_expr
-    { Efun ($3, $2, $4, $6) }
+| 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 REC with_list1(rec_defn) IN seq_expr
     { Erec ($3, $5) }
-| fun_expr
-    { Elam $1 }
-| VAL top_ghost labels(lident_rich) mk_expr(val_expr) IN seq_expr
+| FUN binders spec ARROW spec seq_expr
+    { Elam ($2, None, spec_union $3 $5, $6) }
+| ANY ty spec
+    { Eany ([], $2, $3) }
+| VAL top_ghost labels(lident_rich) mk_expr(val_defn) IN seq_expr
     { Elet ($3, $2, $4, $6) }
 | MATCH seq_expr WITH match_cases(seq_expr) END
     { Ematch ($2, $4) }
@@ -686,8 +689,6 @@ expr_:
     { Eraise ($3, Some $4) }
 | TRY seq_expr WITH bar_list1(exn_handler) END
     { Etry ($2, $4) }
-| ANY ty spec
-    { Eany ([], $2, $3) }
 | GHOST expr
     { Eghost $2 }
 | ABSTRACT spec seq_expr END
@@ -746,9 +747,6 @@ loop_annotation:
 exn_handler:
 | uqualid pat_arg? ARROW seq_expr { $1, $2, $4 }
 
-val_expr:
-| type_v { Eany $1 }
-
 assertion_kind:
 | ASSERT  { Expr.Assert }
 | ASSUME  { Expr.Assume }

src/parser/ptree.ml

@@ -242,8 +242,6 @@ type decl =
   | Dind of Decl.ind_sign * ind_decl list
   | Dprop of Decl.prop_kind * ident * term
   | Dmeta of ident * metarg list
-  | Dval of ident * top_ghost * any
   | Dlet of ident * top_ghost * expr
-  | Dfun of ident * top_ghost * lambda
   | Drec of fundef list
   | Dexn of ident * pty

src/parser/typing.ml

@@ -1046,22 +1046,6 @@ let add_decl muc inth d =
         | Glemma -> true, RKlemma in
       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.Dfun (id, gh, lam) ->
-      let gh, kind = match gh with
-        | Gnone -> false, RKnone
-        | Gghost -> true, RKnone
-        | Glemma -> true, RKlemma in
-      let e = Dexpr.dexpr (dlambda muc denv_empty lam) in
-      let ld = create_user_id id, gh, kind, e in
-      add_pdecl ~vc muc (create_let_decl (let_defn ~keep_loc:true ld))
-  | Ptree.Dval (id, gh, any) ->
-      let gh, kind = match gh with
-        | Gnone -> false, RKnone
-        | Gghost -> true, RKnone
-        | Glemma -> true, RKlemma in
-      let e = Dexpr.dexpr (dany muc any) in
-      let ld = create_user_id id, gh, kind, e in
-      add_pdecl ~vc muc (create_let_decl (let_defn ~keep_loc:true ld))
   | Ptree.Drec fdl ->
       let _, rd = drec_defn muc denv_empty fdl in
       add_pdecl ~vc muc (create_let_decl (rec_defn ~keep_loc:true rd))