From 00bc4885ad3560995fd47902e3cb4329de333ee5 Mon Sep 17 00:00:00 2001
From: Vesa Karvonen <vesa.a.j.k@gmail.com>
Date: Tue, 28 Jul 2020 09:00:28 +0300
Subject: [PATCH] Change to accept syms without parens and to declare multiple
 names

Syntax of names is changed such that in simple declaration and binding contexts
the parentheses around a symbol can be omitted.  For example, previously one
would write:

    {(+), (-)} = Int
    (+): int -> int -> int

Now one can also write:

    {+, -} = Int
    + : int -> int -> int

Parentheses are still required when declaring symbol named functions:

    type (|) a b = ;; ...
    (+) x y = ;; ...

Of course, the infix notation can still also be used:

    type a | n = ;; ...
    x + y = ;; ...

Syntax of declarations is also changed such that multiple names can be declared
with the same type.  Previously one would write:

    (+): int -> int -> int
    (-): int -> int -> int

Now one can also write:

    + - : int -> int -> int

To make this possible, only implicit type parameters are allowed before the
colon.  Previously one could write:

    id a: a -> a

Now one must write:

    id: (a : type) -> a -> a

Implicit type parameters are still allowed before the colon:

    id 'a: a -> a

As explicit type parameters preceding the colon are a relic from 1ML without
type inference this should not cause major inconvenience.

Syntax of paths (namelists) is also changed to allow symbols without
parentheses.
---
 basis/index.1ml         |   2 +-
 examples/fc.1ml         |   2 +-
 examples/leibniz.1mls   |   2 +-
 examples/type-level.1ml |  10 +--
 lexer.mll               |   4 +-
 paper.1ml               |  10 +--
 parser.mly              | 185 ++++++++++++++++++++++++++--------------
 prelude/index.1ml       |  10 +--
 prelude/index.1mls      |  71 +++++----------
 prelude/primitives.1ml  |  32 +++----
 regression.1ml          |  14 +--
 syntax.ml               |   7 ++
 talk.1ml                |   6 +-
 13 files changed, 198 insertions(+), 157 deletions(-)

diff --git a/basis/index.1ml b/basis/index.1ml
index 473375d8..2a5fccc2 100644
--- a/basis/index.1ml
+++ b/basis/index.1ml
@@ -6,7 +6,7 @@ List = import "./list"
 
 type ORD = {
   type t
-  (<=) : t -> t ~> Bool.t
+  <= : t -> t ~> Bool.t
 }
 
 type SET = {
diff --git a/examples/fc.1ml b/examples/fc.1ml
index a1bb894e..20317435 100644
--- a/examples/fc.1ml
+++ b/examples/fc.1ml
@@ -38,7 +38,7 @@ GADTs = {
 AssociatedTypes = {
   type EQ = {
     type t
-    (==): t -> t -> bool
+    == : t -> t -> bool
   }
 
   type COLLECTS = {
diff --git a/examples/leibniz.1mls b/examples/leibniz.1mls
index c262c87d..59da822e 100644
--- a/examples/leibniz.1mls
+++ b/examples/leibniz.1mls
@@ -3,7 +3,7 @@ type t a b
 type a ~ b = t a b
 
 id 'a: a ~ a                           ;; Reflexivity
-(<<) 'a 'b 'c: b ~ c -> a ~ b -> a ~ c ;; Transitivity
+<< 'a 'b 'c: b ~ c -> a ~ b -> a ~ c   ;; Transitivity
 invert 'a 'b: a ~ b -> b ~ a           ;; Symmetry
 
 to   'a 'b: a ~ b -> a -> b
diff --git a/examples/type-level.1ml b/examples/type-level.1ml
index 07c9aa11..5642580f 100644
--- a/examples/type-level.1ml
+++ b/examples/type-level.1ml
@@ -28,8 +28,8 @@ TypeLevel: {
 
     not: t -> t
 
-    (&&&): t -> t -> t
-    (|||): t -> t -> t
+    &&& : t -> t -> t
+    ||| : t -> t -> t
 
     equals: t -> t -> t
   }
@@ -56,15 +56,15 @@ TypeLevel: {
 
     succ: t -> t
 
-    (+): t -> t -> t
-    (*): t -> t -> t
+    + : t -> t -> t
+    * : t -> t -> t
   }
 
   List: {
     type t = type -> (type _ _ _) -> type
 
     nil: t
-    (::): type -> t -> t
+    :: : type -> t -> t
 
     map: (type _ _) -> t -> t
 
diff --git a/lexer.mll b/lexer.mll
index db5024de..084cd91d 100644
--- a/lexer.mll
+++ b/lexer.mll
@@ -253,7 +253,7 @@ let escape = ['n''t''\\''\'''\"']
 let character = [^'"''\\''\n'] | '\\'escape
 
 let num = digit+
-let name = (letter | '_') (letter | digit | '_' | tick)*
+let word = (letter | '_') (letter | digit | '_' | tick)*
 let text = '"'character*'"'
 let char = '\''character '\''
 
@@ -298,7 +298,7 @@ rule token = parse
   | "}" { RBRACE }
   | "," { COMMA }
   | ";" { SEMI }
-  | name as s { NAME s }
+  | word as s { WORD s }
   | symbol* as s { SYM s }
   | num as s { NUM (convert_num s) }
   | char as s { CHAR (convert_char s) }
diff --git a/paper.1ml b/paper.1ml
index ee244e65..355d109a 100644
--- a/paper.1ml
+++ b/paper.1ml
@@ -60,9 +60,9 @@ type EQ = {
 type MAP = {
   type key
   type map a
-  empty (a : type) : map a
-  add (a : type) : key -> a -> map a ~> map a
-  lookup (a : type) : key -> map a ~> opt a
+  empty : (a : type) -> map a
+  add : (a : type) -> key -> a -> map a ~> map a
+  lookup : (a : type) -> key -> map a ~> opt a
 }
 
 Map (Key : EQ) :> MAP with (type key = Key.t) = {
@@ -101,8 +101,8 @@ entries (c : type) (C : COLL c) (xs : c) : list (C.key, C.val) =
   List.map (C.keys xs) (fun (k : C.key) => (k, caseopt (C.lookup xs k) bot id))
 
 type MONAD (m : type -> type) = {
-  return (a : type) : a ~> m a
-  bind (a : type) (b : type) : m a -> (a ~> m b) ~> m b
+  return : (a : type) -> a ~> m a
+  bind : (a : type) -> (b : type) -> m a -> (a ~> m b) ~> m b
 }
 map (a : type) (b : type) (m : type -> type) (M : MONAD m) (f : a ~> b) (mx : m a) =
   M.bind a b mx (fun (x : a) => M.return b (f x))  ;; : m b
diff --git a/parser.mly b/parser.mly
index 6489e214..de2bc01a 100644
--- a/parser.mly
+++ b/parser.mly
@@ -42,7 +42,7 @@ let parse_error s = raise (Source.Error (Source.nowhere_region, s))
 
 %token EOF
 
-%token<string> NAME
+%token<string> WORD
 %token<string> SYM
 %token<string> TEXT
 %token<char> CHAR
@@ -54,36 +54,80 @@ let parse_error s = raise (Source.Error (Source.nowhere_region, s))
 
 %%
 
-label :
-  | name
-    { $1 }
-  | sym
-    { $1 }
-  | NUM
-    { index($1)@@at() }
+word :
+  | WORD
+    { $1@@at() }
+;
+
+hole :
+  | HOLE
+    { "_"@@at() }
 ;
+
 sym :
   | SYM
     { $1@@at() }
 ;
-name :
-  | NAME
-    { $1@@at() }
+psym :
   | LPAR sym RPAR
     { $2 }
 ;
-namelist :
-  | name
-    { $1::[] }
-  | name DOT namelist
-    { $1::$3 }
+
+pname :
+  | word
+    { $1 }
+  | psym
+    { $1 }
+;
+
+name :
+  | word
+    { $1 }
+  | psym
+    { $1 }
+  | sym
+    { $1 }
+;
+
+phead :
+  | word
+    { $1 }
+  | psym
+    { $1 }
+  | hole
+    { $1 }
 ;
 
 head :
+  | word
+    { $1 }
+  | psym
+    { $1 }
+  | hole
+    { $1 }
+  | sym
+    { $1 }
+;
+
+names :
+  | name
+    { [$1] }
+  | name names
+    { $1::$2 }
+;
+
+label :
   | name
     { $1 }
-  | HOLE
-    { "_"@@at() }
+  | NUM
+    { index($1)@@at() }
+;
+
+path :
+  | label
+    { $1::[] }
+  | label DOT path
+    { $1::$3 }
 ;
 
 infixtyp :
@@ -95,27 +139,27 @@ infixtyp :
 typdec :
   | infixtyp
     { $1 }
-  | TYPE name typparamlist
+  | TYPE pname typparamlist
     { ($2, $3) }
 ;
 typpat :
   | infixtyp
     { $1 }
-  | TYPE head typparamlist
+  | TYPE phead typparamlist
     { ($2, $3) }
 ;
 
 implparam :
   | TICK LPAR head COLON TYPE RPAR
     { (headB($3)@@ati 3, TypT@@ati 5, Impl@@ati 1)@@at() }
-  | TICK LPAR TYPE head RPAR
+  | TICK LPAR TYPE phead RPAR
     { (headB($4)@@ati 4, TypT@@ati 3, Impl@@ati 1)@@at() }
   | TICK head
     { (headB($2)@@ati 2, TypT@@ati 1, Impl@@ati 1)@@at() }
 ;
 annparam :
-  | LPAR head COLON typ RPAR
-    { (headB($2)@@ati 2, $4, Expl@@ati 3)@@at() }
+  | LPAR head annot RPAR
+    { (headB($2)@@ati 2, $3, Expl@@ati 3)@@at() }
   | LPAR typpat optannot RPAR
     { let (h, tps) = $2 in
       (headB(h)@@h.at,
@@ -185,10 +229,10 @@ attyp :
 withtyp :
   | infpathexp
     { pathT($1)@@at() }
-  | withtyp WITH LPAR namelist typparamlist EQUAL exp RPAR
+  | withtyp WITH LPAR path typparamlist EQUAL exp RPAR
     { WithT($1, $4, funE($5, $7)@@span[ati 5; ati 7])@@at() }
-  | withtyp WITH LPAR TYPE namelist typparamlist EQUAL typ RPAR
-    { WithT($1, $5, funE($6, typE($8)@@ati 8)@@span[ati 6; ati 8])@@at() }
+  | withtyp WITH LPAR TYPE path typparamlist typdef RPAR
+    { WithT($1, $5, funE($6, $7)@@span[ati 6; ati 7])@@at() }
 ;
 typ :
   | withtyp
@@ -213,28 +257,37 @@ typlist :
     { $1::$3 }
 ;
 
+annot :
+  | COLON typ
+    { $2 }
+;
 optannot :
   |
     { None }
-  | COLON typ
-    { Some $2 }
+  | annot
+    { Some $1 }
 ;
 
+typdef :
+  | EQUAL typ
+    { typE($2)@@ati 2 }
+;
 opttypdef :
   |
     { None }
-  | EQUAL typ
-    { Some (typE($2)@@ati 2) }
+  | typdef
+    { Some $1 }
 ;
 
 atdec :
-  | name typparamlist COLON typ
-    { VarD($1, funT($2, $4, Pure@@ati 2)@@span[ati 2; ati 4])@@at() }
-  | name typparamlist EQUAL exp
-    { VarD($1, funT($2, EqT($4)@@ati 4, Pure@@ati 3)@@span[ati 2; ati 4])
-        @@at() }
+  | names implparamlist annot
+    { let t = funT($2, $3, Pure@@ati 2)@@span[ati 2; ati 3] in
+      ($1 |> List.map (fun n -> VarD(n, t)@@at()) |> seqDs)@@at() }
+  | names implparamlist EQUAL exp
+    { let t = funT($2, EqT($4)@@ati 4, Pure@@ati 3)@@span[ati 2; ati 4] in
+      ($1 |> List.map (fun n -> VarD(n, t)@@at()) |> seqDs)@@at() }
   | name
-    { VarD($1, funT([], EqT(VarE($1)@@ati 1)@@ati 1, Pure@@ati 1)@@ati 1)@@at() }
+    { VarD($1, EqT(VarE($1)@@at())@@at())@@at() }
   | typdec optannot opttypdef
     { VarD(fst $1,
         funT(snd $1,
@@ -272,7 +325,7 @@ dotpathexp :
     { DotE($1, $3)@@at() }
 ;
 atpathexp :
-  | name
+  | pname
     { VarE($1)@@at() }
   | HOLE
     { typE(HoleT@@at())@@at() }
@@ -307,10 +360,8 @@ dotexp :
     { DotE($1, $3)@@at() }
 ;
 atexp :
-  | name
-    { VarE($1)@@at() }
-  | HOLE
-    { typE(HoleT@@at())@@at() }
+  | atpathexp
+    { $1 }
   | PRIMITIVE TEXT
     { match Prim.fun_of_string $2 with
       | Some f -> PrimE(Prim.FunV f)@@at()
@@ -395,7 +446,7 @@ explist :
 ;
 
 funbind :
-  | head param paramlist
+  | phead param paramlist
     { ($1, $2::$3) }
   | oneexplparam sym oneexplparam
     { ($2, $1 @ $3) }
@@ -437,12 +488,12 @@ bindanns_opt :
 atbind :
   | funbind bindanns_opt EQUAL exp
     { let (h, ps) = $1 in VarB(h, funE(ps, $2($4))@@at())@@at() }
-  | atpat bindanns_opt EQUAL exp
+  | bindpat bindanns_opt EQUAL exp
     { patB($1, $2($4))@@at() }
   | name
     { VarB($1, VarE($1.it@@at())@@at())@@at() }
-  | typpat bindanns_opt EQUAL typ
-    { VarB(fst $1, funE(snd $1, $2(typE($4)@@span[ati 2; ati 4]))@@at())@@at() }
+  | typpat bindanns_opt typdef
+    { VarB(fst $1, funE(snd $1, $2($3))@@at())@@at() }
   | ELLIPSIS exp
     { InclB($2)@@at() }
   | DO exp
@@ -469,15 +520,22 @@ bind :
     { letB($2, $4)@@at() }
 ;
 
+bindpat :
+  | atpat
+    { $1 }
+  | sym
+    { headP $1@@at() }
+;
+
 atpat :
-  | head
+  | phead
     { headP $1@@at() }
   | LBRACE decon RBRACE
     { strP($2, at())@@at() }
   | LPAR RPAR
     { strP([], at())@@at() }
-  | LPAR head typparam typparamlist COLON typ RPAR
-    { annotP(headP($2)@@$2.at, funT($3::$4, $6, Pure@@at())@@at())@@at() }
+  | LPAR head typparam typparamlist annot RPAR
+    { annotP(headP($2)@@$2.at, funT($3::$4, $5, Pure@@at())@@at())@@at() }
   | LPAR patlist RPAR
     { match $2 with [p] -> p | ps -> tupP(ps, at())@@at() }
   | LPAR typpat optannot RPAR
@@ -515,20 +573,23 @@ patlist :
 ;
 
 atdecon :
-  | name optannot EQUAL pat
-    { ($1, opt annotP($4, $2)@@span[ati 2; ati 4])@@at() }
-  | name optannot
-    { ($1, opt annotP(varP($1)@@ati 1, $2)@@at())@@at() }
-  | name typparam typparamlist COLON typ
-    { ($1, annotP(varP($1)@@$1.at,
-       funT($2::$3, $5, Pure@@at())@@at())@@at())@@at() }
+  | names optannot EQUAL pat
+    { let p = opt annotP($4, $2)@@span[ati 2; ati 4] in
+      $1 |> List.map (fun n -> (n, p)@@at()) }
+  | names implparam implparamlist annot
+    { let t = funT($2::$3, $4, Pure@@at())@@at() in
+      $1 |> List.map (fun n -> (n, annotP(varP(n)@@n.at, t)@@at())@@at()) }
+  | names annot
+    { $1 |> List.map (fun n -> (n, annotP(varP(n)@@n.at, $2)@@at())@@at()) }
+  | name
+    { [($1, varP($1)@@at())@@at()] }
   | typdec optannot
     { let (n, tps) = $1 in
-      (n,
-       annotP(varP(n)@@n.at,
-         funT(tps,
-           Lib.Option.value $2 ~default:(TypT@@at()),
-           Pure@@at())@@at())@@at())@@at() }
+      [(n,
+        annotP(varP(n)@@n.at,
+          funT(tps,
+            Lib.Option.value $2 ~default:(TypT@@at()),
+            Pure@@at())@@at())@@at())@@at()] }
 /*
   | LPAR decon RPAR
     { $2 }
@@ -538,9 +599,9 @@ decon :
   |
     { [] }
   | atdecon
-    { [$1] }
+    { $1 }
   | atdecon COMMA decon
-    { $1::$3 }
+    { $1@$3 }
 ;
 
 prog :
diff --git a/prelude/index.1ml b/prelude/index.1ml
index 2804afa7..b7185c9c 100644
--- a/prelude/index.1ml
+++ b/prelude/index.1ml
@@ -58,7 +58,7 @@ List = {
   ...rec {type t _} => {type t x = Opt.t (x, t x)}
   nil = Opt.none
   hd :: tl = Opt.some (hd, tl)
-  case {nil, (::)} = Opt.case {
+  case {nil, ::} = Opt.case {
     none = nil
     some (hd, tl) = hd :: tl
   }
@@ -66,9 +66,9 @@ List = {
 
 {either, inl, inr, plus} = Alt
 {false, not, true} = Bool
-{(<<), (<|), (>>), (|>), bot, const, curry, flip, id, uncurry} = Fun
-{(%), (*), (+), (-), (/), (<), (<=), (<>), (==), (>), (>=)} = Int
-{(::), nil} = List
+{<<, <|, >>, |>, bot, const, curry, flip, id, uncurry} = Fun
+{%, *, +, -, /, <, <=, <>, ==, >, >=} = Int
+{::, nil} = List
 {none, some} = Opt
 {cross, fork, fst, snd} = Pair
-{(++), print} = Text
+{++, print} = Text
diff --git a/prelude/index.1mls b/prelude/index.1mls
index 2ebae144..b5117f18 100644
--- a/prelude/index.1mls
+++ b/prelude/index.1mls
@@ -11,18 +11,15 @@ Alt: {
 
 Bool: {
   type t = bool
-  (==): t -> t -> bool
-  (<>): t -> t -> bool
-  true: t
-  false: t
+  <> == : t -> t -> bool
+  false true: t
   not: t -> t
   toText: t -> text
 }
 
 Char: {
   type t = char
-  (==): t -> t -> bool
-  (<>): t -> t -> bool
+  <> == : t -> t -> bool
   toInt: t -> int
   fromInt: int -> t
   print: t ~> {}
@@ -36,25 +33,16 @@ Fun: {
   curry 'a 'b 'c: ((a, b) ~> c) -> a -> b ~> c
   uncurry 'a 'b 'c: (a ~> b ~> c) -> (a, b) ~> c
   flip 'a 'b 'c: (a ~> b ~> c) -> b -> a ~> c
-  (<<) 'a 'b 'c: (b ~> c) -> (a ~> b) -> a ~> c
-  (>>) 'a 'b 'c: (a ~> b) -> (b ~> c) -> a ~> c
-  (<|) 'a 'b: (a ~> b) -> a ~> b
-  (|>) 'a 'b: a -> (a ~> b) ~> b
+  << 'a 'b 'c: (b ~> c) -> (a ~> b) -> a ~> c
+  >> 'a 'b 'c: (a ~> b) -> (b ~> c) -> a ~> c
+  <| 'a 'b: (a ~> b) -> a ~> b
+  |> 'a 'b: a -> (a ~> b) ~> b
 }
 
 Int: {
   type t = int
-  (==): t -> t -> bool
-  (<>): t -> t -> bool
-  (<): t -> t -> bool
-  (>): t -> t -> bool
-  (<=): t -> t -> bool
-  (>=): t -> t -> bool
-  (+): t -> t -> t
-  (-): t -> t -> t
-  (*): t -> t -> t
-  (/): t -> t -> t
-  (%): t -> t -> t
+  % * + - / : t -> t -> t
+  < <= <> == > >= : t -> t -> bool
   toText: t -> text
   print: t ~> {}
 }
@@ -62,8 +50,8 @@ Int: {
 List: {
   type t _
   nil 'a: t a
-  (::) 'a: a -> t a -> t a
-  case 'a 'o: {nil: o, (::): a ~> t a ~> o} -> t a ~> o
+  :: 'a: a -> t a -> t a
+  case 'a 'o: {nil: o, :: : a ~> t a ~> o} -> t a ~> o
 }
 
 Opt: {
@@ -87,13 +75,8 @@ System: {
 
 Text: {
   type t = text
-  (==): t -> t -> bool
-  (<>): t -> t -> bool
-  (<): t -> t -> bool
-  (>): t -> t -> bool
-  (<=): t -> t -> bool
-  (>=): t -> t -> bool
-  (++): t -> t -> t
+  ++ : t -> t -> t
+  < <= <> == > >= : t -> t -> bool
   length: t -> int
   sub: t -> int -> char
   fromChar: char -> t
@@ -113,29 +96,20 @@ type opt a = Opt.t a
 type text = Text.t
 type zero = Zero.t
 
-(%): int -> int -> int
-(*): int -> int -> int
-(+): int -> int -> int
-(++): text -> text -> text
-(-): int -> int -> int
-(/): int -> int -> int
-(::) 'a: a -> list a -> list a
-(<): int -> int -> bool
-(<<) 'a 'b 'c: (b ~> c) -> (a ~> b) -> a ~> c
-(<=): int -> int -> bool
-(<>): int -> int -> bool
-(<|) 'a 'b: (a ~> b) -> a ~> b
-(==): int -> int -> bool
-(>): int -> int -> bool
-(>=): int -> int -> bool
-(>>) 'a 'b 'c: (a ~> b) -> (b ~> c) -> a ~> c
-(|>) 'a 'b: a -> (a ~> b) ~> b
+% * + - / : int -> int -> int
+++ : text -> text -> text
+:: 'a: a -> list a -> list a
+< <= <> == > >= : int -> int -> bool
+<< 'a 'b 'c: (b ~> c) -> (a ~> b) -> a ~> c
+>> 'a 'b 'c: (a ~> b) -> (b ~> c) -> a ~> c
+<| 'a 'b: (a ~> b) -> a ~> b
+|> 'a 'b: a -> (a ~> b) ~> b
 bot 'a 'b: a -> b
 const 'a 'b: a -> b -> a
 cross 'a 'b 'c 'd: (a ~> c) -> (b ~> d) -> (a, b) ~> (c, d)
 curry 'a 'b 'c: ((a, b) ~> c) -> a -> b ~> c
 either 'a 'b 'o: (a ~> o) -> (b ~> o) -> alt a b ~> o
-false: bool
+false true: bool
 flip 'a 'b 'c: (a ~> b ~> c) -> b -> a ~> c
 fork 'a 'b 'c: (a ~> b) -> (a ~> c) -> a ~> (b, c)
 fst 'a 'b: (a, b) -> a
@@ -149,5 +123,4 @@ plus 'a 'b 'c 'd: (a ~> c) -> (b ~> d) -> alt a b ~> alt c d
 print: text ~> {}
 snd 'a 'b: (a, b) -> b
 some 'a: a -> opt a
-true: bool
 uncurry 'a 'b 'c: (a ~> b ~> c) -> (a, b) ~> c
diff --git a/prelude/primitives.1ml b/prelude/primitives.1ml
index b1eff63b..319936e1 100644
--- a/prelude/primitives.1ml
+++ b/prelude/primitives.1ml
@@ -2,8 +2,8 @@ local
   pbo (p: _ -> _) l r = p (l, r)
 
   PolyEq (type t) = {
-    (==) = pbo (primitive "==" t)
-    (<>) = pbo (primitive "<>" t)
+    == = pbo (primitive "==" t)
+    <> = pbo (primitive "<>" t)
   }
 
 type bool = primitive "bool"
@@ -29,26 +29,26 @@ System = {
 }
 
 Int = {
-  (+) = pbo primitive "Int.+"
-  (-) = pbo primitive "Int.-"
-  (*) = pbo primitive "Int.*"
-  (/) = pbo primitive "Int./"
-  (%) = pbo primitive "Int.%"
-  (<) = pbo primitive "Int.<"
-  (>) = pbo primitive "Int.>"
-  (<=) = pbo primitive "Int.<="
-  (>=) = pbo primitive "Int.>="
+  + = pbo primitive "Int.+"
+  - = pbo primitive "Int.-"
+  * = pbo primitive "Int.*"
+  / = pbo primitive "Int./"
+  % = pbo primitive "Int.%"
+  < = pbo primitive "Int.<"
+  > = pbo primitive "Int.>"
+  <= = pbo primitive "Int.<="
+  >= = pbo primitive "Int.>="
   toText = primitive "Int.toText"
   print = primitive "Int.print"
   ...PolyEq int
 }
 
 Text = {
-  (++) = pbo primitive "Text.++"
-  (<) = pbo primitive "Text.<"
-  (>) = pbo primitive "Text.>"
-  (<=) = pbo primitive "Text.<="
-  (>=) = pbo primitive "Text.>="
+  ++ = pbo primitive "Text.++"
+  < = pbo primitive "Text.<"
+  > = pbo primitive "Text.>"
+  <= = pbo primitive "Text.<="
+  >= = pbo primitive "Text.>="
   length = primitive "Text.length"
   sub = pbo primitive "Text.sub"
   fromChar = primitive "Text.fromChar"
diff --git a/regression.1ml b/regression.1ml
index 795653f2..34624c0f 100644
--- a/regression.1ml
+++ b/regression.1ml
@@ -54,9 +54,9 @@ Equivalence: {
 
 ;;
 
-type MONOID = {type t, empty: t, (++): t -> t ~> t}
+type MONOID = {type t, empty: t, ++ : t -> t ~> t}
 cat (M: MONOID) = List.foldl M.++ M.empty
-do assert (cat {empty = 0, (++) = (+)} (40 :: (2 :: nil)) == 42)
+do assert (cat {empty = 0, ++ = (+)} (40 :: (2 :: nil)) == 42)
 
 Poly: {type t} = {} ;; Poly 'x = {type t = x}
 do 1: Poly.t
@@ -266,7 +266,7 @@ Alt = Alt : {
   ...(= Alt)
   type a | b = alt a b
 }
-(|) = Alt.|
+| = Alt.|
 
 type AnAlt = {x: int} | {y: bool}
 
@@ -318,8 +318,8 @@ N :> {
 
 ListN = let
   type I (type x) (type p _) (type t _ _) = {
-    nil     :               p N.Z
-    (::) 'n : x ~> t x n ~> p (N.S n)
+    nil   :               p N.Z
+    :: 'n : x ~> t x n ~> p (N.S n)
   }
 in {
   ...rec {type t _ _} => {type t x n = wrap (type p _) -> I x p t ~> p n}
@@ -334,8 +334,8 @@ in {
 
   case 'x 'n: (type p _) -> I x p t -> t x n ~> p n
 
-  nil  'x    :               t x N.Z
-  (::) 'x 'n : x -> t x n -> t x (N.S n)
+  nil 'x    :               t x N.Z
+  ::  'x 'n : x -> t x n -> t x (N.S n)
 }
 
 ListN = {
diff --git a/syntax.ml b/syntax.ml
index 80b64e27..fed2580e 100644
--- a/syntax.ml
+++ b/syntax.ml
@@ -335,6 +335,13 @@ let rollP(p, t2) =
    annot = Some t2}
 
 
+(* *)
+
+let seqDs = function
+  | [] -> EmptyD
+  | d::ds -> (List.fold_left (fun s d -> seqD(s, d)@@d.at) d ds).it
+
+
 (* String conversion *)
 
 let node label = function
diff --git a/talk.1ml b/talk.1ml
index f4486fc3..8d40f1e8 100644
--- a/talk.1ml
+++ b/talk.1ml
@@ -32,9 +32,9 @@ type EQ = {
 type MAP = {
   type key
   type map a
-  empty a : map a
-  lookup a : key -> map a ~> opt a
-  add a : key -> a -> map a ~> map a
+  empty : (a : type) -> map a
+  lookup : (a : type) -> key -> map a ~> opt a
+  add : (a : type) -> key -> a -> map a ~> map a
 }
 
 Map (Key : EQ) :> MAP with (type key = Key.t) = {