syntax for closures

src/core/term.ml

@@ -1034,7 +1034,7 @@ let f_neq t1 t2 = f_not (f_app ps_equ [t1; t2])
 let fs_func_app =
   let ty_a = ty_var (create_tvsymbol (id_fresh "a")) in
   let ty_b = ty_var (create_tvsymbol (id_fresh "b")) in
-  create_fsymbol (id_fresh "infix @!") [ty_func ty_a ty_b; ty_a] ty_b
+  create_fsymbol (id_fresh "infix @") [ty_func ty_a ty_b; ty_a] ty_b
 
 let ps_pred_app =
   let ty_a = ty_var (create_tvsymbol (id_fresh "a")) in

src/parser/lexer.mll

@@ -187,6 +187,8 @@ rule token = parse
       { ASYM_AND }
   | "\\/"
       { ASYM_OR }
+  | "\\"
+      { LAMBDA }
   | "."
       { DOT }
   | "|"

src/parser/parser.mly

@@ -91,7 +91,7 @@
 
 %token AND AS AXIOM CLONE
 %token ELSE END EPSILON EXISTS EXPORT FALSE FORALL
-%token GOAL IF IMPORT IN INDUCTIVE LEMMA
+%token GOAL IF IMPORT IN INDUCTIVE LAMBDA LEMMA
 %token LET LOGIC MATCH META NAMESPACE NOT PROP OR
 %token THEN THEORY TRUE TYPE USE WITH
 
@@ -439,8 +439,8 @@ lexpr:
    { mk_pp (PPapp ($1, $2)) }
 | IF lexpr THEN lexpr ELSE lexpr
    { mk_pp (PPif ($2, $4, $6)) }
-| FORALL list1_param_var_sep_comma triggers DOT lexpr
-   { mk_pp (PPquant (PPforall, $2, $3, $5)) }
+| quant list1_param_var_sep_comma triggers DOT lexpr
+   { mk_pp (PPquant ($1, $2, $3, $5)) }
 | EXISTS list1_param_var_sep_comma triggers DOT lexpr
    { mk_pp (PPquant (PPexists, $2, $3, $5)) }
 | STRING lexpr %prec prec_named
@@ -488,6 +488,12 @@ lexpr_arg:
      mk_pp (PPapp (Qident id, [$2])) }
 ;
 
+quant:
+| FORALL  { PPforall }
+| EXISTS  { PPexists }
+| LAMBDA  { PPlambda }
+;
+
 /* Triggers */
 
 triggers:

src/parser/ptree.ml

@@ -28,7 +28,7 @@ type constant = Term.constant
 type label = Ident.label
 
 type pp_quant =
-  | PPforall | PPexists | PPfunc | PPpred
+  | PPforall | PPexists | PPlambda
 
 type pp_binop =
   | PPand | PPor | PPimplies | PPiff

src/parser/typing.ml

@@ -425,7 +425,7 @@ and dterm_node loc env = function
       let env = { env with dvars = Mstr.add x.id ty env.dvars } in
       let e1 = dfmla env e1 in
       Teps (x, ty, e1), ty
-  | PPquant (q, uqu, trl, a) ->
+  | PPquant (PPlambda, uqu, trl, a) ->
       check_quant_linearity uqu;
       let uquant env (idl,ty) =
         let ty = dty env ty in
@@ -443,9 +443,8 @@ and dterm_node loc env = function
 	  TRfmla (dfmla env e)
       in
       let trl = List.map (List.map trigger) trl in
-      let id, ty, f = match q with
-        | PPfunc ->
-            let t = dterm env a in
+      let id, ty, f = match trigger a with
+        | TRterm t ->
             let id = { id = "fc" ; id_loc = loc } in
             let tyl,ty = List.fold_right (fun (_,uty) (tyl,ty) ->
               let nty = Tyapp (ts_func, [uty;ty]) in ty :: tyl, nty)
@@ -458,8 +457,7 @@ and dterm_node loc env = function
               h uqu tyl
             in
             id, ty, Fapp (ps_equ, [h;t])
-        | PPpred ->
-            let f = dfmla env a in
+        | TRfmla f ->
             let id = { id = "pc" ; id_loc = loc } in
             let (uid,uty),uqu = match List.rev uqu with
               | uq :: uqu -> uq, List.rev uqu
@@ -477,10 +475,9 @@ and dterm_node loc env = function
             in
             let u = { dt_node = Tvar uid.id ; dt_ty = uty } in
             id, ty, Fbinop (Fiff, Fapp (ps_pred_app, [h;u]), f)
-        | _ -> error ~loc:loc TermExpected
       in
       Teps (id, ty, Fquant (Fforall, uqu, trl, f)), ty
-  | PPbinop _ | PPunop _ | PPfalse | PPtrue ->
+  | PPquant _ | PPbinop _ | PPunop _ | PPfalse | PPtrue ->
       error ~loc TermExpected
 
 and dfmla env e = match e.pp_desc with