From e36a35ff46d2ddb9e604082be9ee07432436866b Mon Sep 17 00:00:00 2001
From: Yann Hamdaoui <yann.hamdaoui@gmail.com>
Date: Thu, 25 Feb 2021 09:52:33 +0100
Subject: [PATCH] Parsing: add != op, accept more general list elements

---
 src/grammar.lalrpop | 16 ++++++++++++----
 src/parser/lexer.rs |  2 ++
 2 files changed, 14 insertions(+), 4 deletions(-)

diff --git a/src/grammar.lalrpop b/src/grammar.lalrpop
index 6e01970a..21fbca8a 100644
--- a/src/grammar.lalrpop
+++ b/src/grammar.lalrpop
@@ -60,8 +60,7 @@ MetaAnnot: MetaValue =
     };
 
 LeftOp<Op, Current, Previous>: RichTerm =
-    <t1: Current> <op: Op> <t2: Previous> => mk_term::op2(op, t1,
-    t2);
+    <t1: Current> <op: Op> <t2: Previous> => mk_term::op2(op, t1, t2);
 
 LeftOpLazy<Op, Current, Previous>: RichTerm =
     <t1: Current> <op: Op> <t2: Previous> => mk_app!(Term::Op1(op, t1), t2);
@@ -261,9 +260,8 @@ Atom: RichTerm = {
             mk_app!(mk_term::op2(BinaryOp::DynExtend(), id_t, rec), t)
         })
     },
-    "[" <terms: (SpTerm<Atom> ",")*> <last: Term?> "]" => {
+    "[" <terms: (<Term> ",")*> <last: Term?> "]" => {
         let terms : Vec<RichTerm> = terms.into_iter()
-            .map(|x| x.0)
             .chain(last.into_iter()).collect();
         RichTerm::from(Term::List(terms))
     }
@@ -484,6 +482,15 @@ BinOp8: BinaryOp = {
 InfixExpr8: RichTerm = {
     InfixExpr7,
     LeftOp<BinOp8, InfixExpr8, InfixExpr7> => <>,
+    <l: @L> <t1: InfixExpr8> "!=" <t2: InfixExpr7> <r: @R> => {
+        mk_term::op1(
+            UnaryOp::BoolNot(),
+            RichTerm::new(
+                Term::Op2(BinaryOp::Eq(), t1, t2),
+                Some(mk_span(src_id, l, r))
+            )
+        )
+    }
 }
 
 LazyBinOp9: UnaryOp = {
@@ -623,6 +630,7 @@ extern {
         ":" => Token::Normal(NormalToken::Colon),
         "$" => Token::Normal(NormalToken::Dollar),
         "=" => Token::Normal(NormalToken::Equals),
+        "!=" => Token::Normal(NormalToken::NotEquals),
         ";" => Token::Normal(NormalToken::SemiCol),
         "&" => Token::Normal(NormalToken::Ampersand),
         "." => Token::Normal(NormalToken::Dot),
diff --git a/src/parser/lexer.rs b/src/parser/lexer.rs
index aceddc50..fc3199e8 100644
--- a/src/parser/lexer.rs
+++ b/src/parser/lexer.rs
@@ -82,6 +82,8 @@ pub enum NormalToken<'input> {
     Dollar,
     #[token("=")]
     Equals,
+    #[token("!=")]
+    NotEquals,
     #[token(";")]
     SemiCol,
     #[token("&")]