Skip to content

Commit

Permalink
fix parsing of negative numeral parameters
Browse files Browse the repository at this point in the history
  • Loading branch information
javra committed Dec 6, 2023
1 parent ce3f138 commit 18b2230
Show file tree
Hide file tree
Showing 2 changed files with 22 additions and 4 deletions.
8 changes: 4 additions & 4 deletions Aegis/Parser.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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"

Expand All @@ -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
Expand Down
18 changes: 18 additions & 0 deletions Aegis/Tests/Test.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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>;
Expand Down

0 comments on commit 18b2230

Please sign in to comment.