Skip to content

Commit

Permalink
use space separation for lists
Browse files Browse the repository at this point in the history
  • Loading branch information
thibautbenjamin committed Oct 3, 2024
1 parent e32da55 commit 2a11aa0
Show file tree
Hide file tree
Showing 4 changed files with 6 additions and 11 deletions.
1 change: 0 additions & 1 deletion lib/lexer.mll
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,6 @@ rule token = parse
| "_" { WILD }
| "set" { SET }
| "!" { BANG }
| "," { COMA }
| "op" { OP }
| "@" { AT }
| " " { IGNORE }
Expand Down
10 changes: 3 additions & 7 deletions lib/parser.mly
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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 }
Expand Down Expand Up @@ -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 }
| { [] }
2 changes: 1 addition & 1 deletion test.t/features/contexts.catt
Original file line number Diff line number Diff line change
@@ -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
4 changes: 2 additions & 2 deletions test.t/features/opposites.catt
Original file line number Diff line number Diff line change
Expand Up @@ -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'')
Expand All @@ -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])

0 comments on commit 2a11aa0

Please sign in to comment.