feat(sol-thir): fix compilation errors

aripiprazole · May 8, 2024 · a3e718c · a3e718c
1 parent a0cb4d3
commit a3e718c
Show file tree

Hide file tree

Showing 7 changed files with 57,925 additions and 56,647 deletions.
diff --git a/tree-sitter-sol/examples/Main.sol b/tree-sitter-sol/examples/Main.sol
@@ -1,5 +1,5 @@
 // Natural numbers
-Nat : * = (n : *) -> (n -> n) -> n
+Nat : U = (n : U) -> (n -> n) -> n
 
 Succ (prev : Nat) : Nat = |n succ# zero#|
   succ# (prev n succ# zero#) zero#
@@ -8,7 +8,7 @@ Zero : Nat = |n succ# zero#|
   zero#
 
 // Maybe definition
-Maybe (t : *) = (a : *) -> (t -> a) a -> a
+Maybe (t : U) = (a : U) -> (t -> a) a -> a
 
 Just (value : a) : Maybe a = |t just# nothing#|
   just# value

diff --git a/tree-sitter-sol/grammar.js b/tree-sitter-sol/grammar.js
@@ -5,13 +5,9 @@ module.exports = grammar({
 
   conflicts: ($) => [
     [$.cons_pattern, $.primary],
-    [$.app_expr, $._expr],
     [$.if_stmt, $.if_expr],
-    [$.type_app_expr, $.app_expr],
     [$._expr, $.type_app_expr, $.app_expr],
-    [$._type_expr, $.primary],
     [$._pattern, $.primary],
-    [$.forall_parameter, $.free_variable],
   ],
 
   precedences: ($) => [
@@ -426,7 +422,9 @@ module.exports = grammar({
 
     _arm_body: ($) => choice($.block, $._expr),
 
-    free_variable: ($) => seq('^', $.identifier),
+    free_variable: ($) => seq("'", $.identifier),
+
+    universe_expr: () => 'U',
 
     // Primaries
     primary: ($) =>
@@ -439,6 +437,7 @@ module.exports = grammar({
         $.if_expr,
         $.match_expr,
         $.return_expr,
+        $.universe_expr,
       ),
 
     literal: ($) =>