Merge pull request thibautbenjamin#77 from thibautbenjamin/feature/co…

…ntext-syntax use space separation for lists
jmarkakis · Oct 3, 2024 · 6130960 · 6130960
2 parents e32da55 + 2a11aa0
commit 6130960
Show file tree

Hide file tree

Showing 4 changed files with 6 additions and 11 deletions.
diff --git a/lib/lexer.mll b/lib/lexer.mll
@@ -26,7 +26,6 @@ rule token = parse
   | "_" { WILD }
   | "set" { SET }
   | "!" { BANG }
-  | "," { COMA }
   | "op" { OP }
   | "@" { AT }
   | "" { IGNORE }

diff --git a/lib/parser.mly b/lib/parser.mly
@@ -33,7 +33,7 @@
       context_over ObjR ps
       %}
 
-%token COH OBJ MOR WILD COMA IGNORE
+%token COH OBJ MOR WILD IGNORE
 %token LPAR RPAR LBRA RBRA LCUR RCUR COL BANG OP AT
 %token <string> BUILTIN
 %token <string> IDENT
@@ -74,7 +74,7 @@ cmd:
 
 args_of_same_ty :
   | IDENT COL tyexpr { [Var.make_var $1, $3], $3 }
-  | IDENT COMA args_of_same_ty { (Var.make_var $1, snd $3)::(fst $3), snd $3 }
+  | IDENT args_of_same_ty { (Var.make_var $1, snd $2)::(fst $2), snd $2 }
 
 nonempty_args :
   | LPAR args_of_same_ty RPAR args { List.append (fst $2) $4 }
@@ -161,10 +161,6 @@ ps_list :
   | nonempty_ps_list { $1 }
   | { [] }
 
-int :
-  | INT { $1 }
-
 int_list :
-  | int { [int_of_string  $1] }
-  | INT COMA int_list { (int_of_string $1)::$3 }
+  | INT int_list { (int_of_string $1)::$2 }
   | { [] }
diff --git a/test.t/features/contexts.catt b/test.t/features/contexts.catt
@@ -1,2 +1,2 @@
 coh whisk (x(f(a)g)y(h)z) : comp  f h -> comp g h
-let composition (x, y, z : *) (f, g : x -> y) (h : y -> z) (a : f -> g) = whisk a h
+let composition (x y z : *) (f g : x -> y) (h : y -> z) (a : f -> g) = whisk a h
diff --git a/test.t/features/opposites.catt b/test.t/features/opposites.catt
@@ -25,7 +25,7 @@ let optest12 (x : *) (y : *) (z : *) (f : x -> y) (f' : x -> y) (f'' : x -> y)
                                     (a : f -> f') (b : f' -> f'')
                                     (g : y -> z) (g' : y -> z) (g'' : y -> z)
                                     (c : g -> g') (d : g' -> g'')
-                                    = op { 1 , 2 } (test d c b a)
+                                    = op { 1 2 } (test d c b a)
 
 let nested1  (x : *) (y : *) (z : *) (f : x -> y) (f' : x -> y) (f'' : x -> y)
                                     (a : f -> f') (b : f' -> f'')
@@ -44,4 +44,4 @@ let nested12  (x : *) (y : *) (z : *) (f : x -> y) (f' : x -> y) (f'' : x -> y)
                                     (a : f -> f') (b : f' -> f'')
                                     (g : y -> z) (g' : y -> z) (g'' : y -> z)
                                     (c : g -> g') (d : g' -> g'')
-                                    = op { 1 , 2 } (comp [comp d c] [comp b a])
+                                    = op { 1 2 } (comp [comp d c] [comp b a])