From 18b2230ca1c3f86db6d8fc049d1edbb413e7692b Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <jakob@von-raumer.de>
Date: Wed, 6 Dec 2023 16:03:49 +0100
Subject: [PATCH] fix parsing of negative numeral parameters

---
 Aegis/Parser.lean     |  8 ++++----
 Aegis/Tests/Test.lean | 18 ++++++++++++++++++
 2 files changed, 22 insertions(+), 4 deletions(-)

diff --git a/Aegis/Parser.lean b/Aegis/Parser.lean
index 7dd35d7..b28442e 100644
--- a/Aegis/Parser.lean
+++ b/Aegis/Parser.lean
@@ -47,7 +47,7 @@ mutual
 partial def identifierToString : Identifier → String
 | .name s ps tl =>
   let ps := match ps with
-  | [] => "" 
+  | [] => ""
   | ps@_ => "<" ++ String.intercalate ", " (parameterToString <$> ps) ++ ">"
   let hd := s ++ ps
   match tl with
@@ -84,7 +84,7 @@ syntax "end" : atom
 syntax atom ("[" ident "]")? atomic("::"? "<" parameter,* ">")?  ("::" identifier)? : identifier
 syntax "[" num "]" : identifier
 
-syntax atomic("-" num) : parameter
+syntax "-" num : parameter
 syntax num : parameter
 syntax "user@" identifier : parameter
 syntax "ut@" identifier : parameter
@@ -194,7 +194,7 @@ def elabDeclarationLine : TSyntax `Sierra.declarationLine →
 def elabTypedefLine : TSyntax `Sierra.typedefLine → Except String (Identifier × Identifier)
 | `(typedefLine|type $tlhs = $trhs $[[storable: $_, drop: $_, dup: $_, zero_sized: $_]]?; $[//$_]?) => do
   let tlhs ← elabIdentifier tlhs
-  let trhs ← elabIdentifier trhs 
+  let trhs ← elabIdentifier trhs
   .ok (tlhs, trhs)
 | _ => .error "Could not elab type definition"
 
@@ -210,7 +210,7 @@ def elabSierraFile : Syntax → Except String SierraFile
 
 -- TODO solve this in a better way
 def replaceNaughtyBrackets (s : String) : String :=
-  (s.replace ">" "> ").replace "<" " <"
+  ((s.replace ">" "> ").replace "<" " <").replace "<-" "< -"
 
 def parseGrammar (input : String) : CoreM (Except String SierraFile) := do
   let env ← getEnv
diff --git a/Aegis/Tests/Test.lean b/Aegis/Tests/Test.lean
index 1dff524..acb4286 100644
--- a/Aegis/Tests/Test.lean
+++ b/Aegis/Tests/Test.lean
@@ -3,6 +3,24 @@ import Aegis.Analyzer
 open Lean Meta Qq
 namespace Sierra
 
+
+def negParam := "type F = felt252;
+
+libfunc c1 = felt252_const<-1>;
+libfunc c2 = felt252_const<1>;
+libfunc add = felt252_add;
+
+c1() -> ([0]);
+c2() -> ([1]);
+add([0], [1]) -> ([2]);
+return ([2]);
+
+
+negparam@0() -> (F);"
+
+#eval parseGrammar negParam
+#eval analyzeFile negParam
+
 def code01 := "
 type core::option::Option::<core::integer::u128> = Enum<ut@core::option::Option::<core::integer::u128>, u128, Unit>;
 type Tuple<u128> = Struct<ut@Tuple, u128>;