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.

Author: polytypic

basis/index.1ml

@@ -6,7 +6,7 @@ List = import "./list"
 
 type ORD = {
   type t
-  (<=) : t -> t ~> Bool.t
+  <= : t -> t ~> Bool.t
 }
 
 type SET = {

examples/fc.1ml

@@ -38,7 +38,7 @@ GADTs = {
 AssociatedTypes = {
   type EQ = {
     type t
-    (==): t -> t -> bool
+    == : t -> t -> bool
   }
 
   type COLLECTS = {

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

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
 

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) }

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