Parse rec keyword after let

src/grammar.lalrpop

@@ -166,7 +166,7 @@ UniTerm: UniTerm = {
     InfixExpr,
     AnnotatedInfixExpr,
     AsUniTerm<Forall>,
-    "let" <pat:Pattern> <meta: Annot<FixedType>?>
+    "let" <recursive:"rec"?> <pat:Pattern> <meta: Annot<FixedType>?>
         "=" <t1: Term>
         "in" <t2: Term> => {
         let t1 = if let Some(mut meta) = meta {
@@ -178,7 +178,9 @@ UniTerm: UniTerm = {
             t1
         };
 
-        UniTerm::from(mk_term::let_pat(pat.0, pat.1, t1, t2))
+	let is_rec = recursive.is_some();
+
+        UniTerm::from(mk_term::let_pat(is_rec, pat.0, pat.1, t1, t2))
     },
     <l: @L> "fun" <pats: Pattern+> "=>" <t: Term> <r: @R> => {
         let pos = mk_pos(src_id, l, r);
@@ -781,6 +783,7 @@ extern {
         "forall" => Token::Normal(NormalToken::Forall),
         "in" => Token::Normal(NormalToken::In),
         "let" => Token::Normal(NormalToken::Let),
+	"rec" => Token::Normal(NormalToken::Rec),
         "switch" => Token::Normal(NormalToken::Switch),
 
         "null" => Token::Normal(NormalToken::Null),

src/parser/lexer.rs

@@ -68,6 +68,8 @@ pub enum NormalToken<'input> {
     In,
     #[token("let")]
     Let,
+    #[token("rec")]
+    Rec,
     #[token("switch")]
     Switch,
 

src/term.rs

@@ -1355,7 +1355,7 @@ pub mod make {
         Term::Let(id.into(), t1.into(), t2.into(), BindingType::Normal).into()
     }
 
-    pub fn let_pat<I, D, T1, T2>(id: Option<I>, pat: D, t1: T1, t2: T2) -> RichTerm
+    pub fn let_pat<I, D, T1, T2>(rec: bool, id: Option<I>, pat: D, t1: T1, t2: T2) -> RichTerm
     where
         T1: Into<RichTerm>,
         T2: Into<RichTerm>,

tests/contracts_fail.rs

@@ -127,7 +127,7 @@ fn records_contracts_poly() {
                 (forall b. {a: Num, b: Num ; b} -> { a: Num ; b})
                 -> {a: Num ; a}
                 -> { ; a}
-            = fun f rec => %record_remove% \"b\" (%record_remove% \"a\" (f rec)) in
+            = fun f r => %record_remove% \"b\" (%record_remove% \"a\" (f r)) in
         f (fun x => x) {a = 1, b = true, c = 3}"
     );
 }

tests/pass/contracts.ncl

@@ -81,7 +81,7 @@ let Assert = fun l x => x || %blame% l in
     (remove (extend {}) == {} | Assert) &&
     (extend (remove {foo = 2}) == {foo =1} | Assert) &&
     (let f | forall a b. {f: a -> a, arg: a ; b} -> a =
-        fun rec => rec.f (rec.arg) in
+        fun r => r.f (r.arg) in
       f { f = fun x => x ++ " suffix", arg = "foo" }
       == "foo suffix"
       | Assert)