Add simple recursive bindings

basis/list.1ml

@@ -7,18 +7,15 @@ isNil = case {nil = true, _::_ = false}
 head = case {nil = none, x::_ = some x}
 tail = case {nil = none, _::xs = some xs}
 
-foldr (::) nil = rec loop => case {nil, x::xs = x::loop xs}
+rec foldr (::) nil = case {nil, x::xs = x::foldr (::) nil xs}
 
-foldl xss = rec (loop: _ -> _) => fun s => case {
-  nil = s
-  x :: xs = loop (xss x s) xs
-}
+rec foldl (::) nil = case {nil, x::xs = foldl (::) (x::nil) xs}
 
 length = foldl (const 1 >> (+)) 0
 
-nth = rec (loop: _ -> _) => fun n => case {
+rec nth n = case {
   nil = none
-  x :: xs = if n == 0 then some x else loop (n-1) xs
+  x :: xs = if n == 0 then some x else nth (n-1) xs
 }
 
 revPrependTo = foldl (::)

elab.ml

@@ -395,6 +395,12 @@ Trace.debug (lazy ("[VarE] s = " ^ string_of_norm_extyp (ExT([], lookup_var env
     let s, zs = elab_typ env typ "" in
     ExT([], TypT(s)), Pure, zs, IL.LamE("_", erase_extyp s, IL.TupE[])
 
+  | EL.PathE(exp) ->
+    let s, p, zs, e = elab_exp env exp l in
+    if p = Impure then
+      error exp.at "impure type expression";
+    s, p, zs, e
+
   | EL.StrE(bind) ->
     elab_bind env bind l
 
@@ -570,7 +576,8 @@ Trace.debug (lazy ("[UnwrapE] s2 = " ^ string_of_norm_extyp s2));
           ("recursive expression diverges: " ^ Sub.string_of_error e)
       in
       (* TODO: syntactic restriction *)
-      s2, Pure, lift_warn exp.at t2 (add_typs aks3 env) (zs1 @ zs2 @ zs3 @ zs4 @ zs5),
+      s2, Pure,
+      lift_warn exp.at t2 (add_typs aks2 env) (zs1 @ zs2 @ zs3 @ zs4 @ zs5),
       IL.RecE(var.it, erase_typ t2, e)
     | _ ->
       let t2, zs2 = elab_pathexp env1 exp1 l in

examples/fc.1ml

@@ -17,7 +17,7 @@ GADTs = {
         Succ       :      t int ~> case int
         Pair 'a 'b : t a ~> t b ~> case (a, b)
       }
-      ...rec {type t _} => {type t a = wrap (m: I t) ~> m.case a}
+      rec type t a = wrap (m: I t) ~> m.case a
       I = I t
     t
     case (m: I) (e: t _) = e m
@@ -67,4 +67,4 @@ FunctionalDependences = {
   combine 'a (f: T a) (g: T a) : T a = fun (type F _) => f F << g F
 }
 
-Newtype = rec {type T} => {type T = T ~> T}
+Newtype = {rec type T = T ~> T}

examples/hoas.1ml

@@ -17,7 +17,7 @@ let
   type J (type t _) = {type case _, ...I case t}
   type T (type t _) x = (c: J t) ~> c.case x
   ...{
-    ...rec {type t _} => {type t x = wrap T t x}
+    rec type t x = wrap T t x
     case 'x (type case _) (cs: I case t) (e: t _) = e {case, ...cs}
     mk (fn: T t _) = fn
   } :> {
@@ -41,7 +41,7 @@ Fact = Fix <| Lam fun f => Lam fun x =>
      (Val 1)
      (Bin (*) x (App f (Bin (-) x (Val 1))))
 
-eval = rec (eval 'x: t x ~> x) => case (type fun t => t) {
+rec eval 'x: t x ~> x = case (type fun t => t) {
   Bin f x y = f (eval x) (eval y)
   If b c a = eval if eval b then c else a
   App f x = eval f (eval x)

examples/trie.1ml

@@ -8,7 +8,7 @@ FunctionalTrie = {
       alt  'v 'k1 'k2 : t k1 v ~> t k2 v ~> case (alt k1 k2) v
       pair 'v 'k1 'k2 : t k1 (t k2 v)    ~> case (k1, k2) v
     }
-    ...rec {type t _ _} => {type t k v = wrap (m: I t) ~> m.case k v}
+    rec type t k v = wrap (m: I t) ~> m.case k v
     I = I t
 
   t
@@ -17,7 +17,7 @@ FunctionalTrie = {
   alt l r : t _ _ = fun (m: I) => m.alt l r
   pair lr : t _ _ = fun (m: I) => m.pair lr
 
-  lookup = rec (lookup 'k 'v: t k v ~> k ~> opt v) =>
+  rec lookup 'k 'v: t k v ~> k ~> opt v =
     case {
       type case k v = k ~> opt v
       unit m {} = m

lexer.mll

@@ -112,10 +112,14 @@ module Offside = struct
       if column < indent - 2 then error "offside" else
         emit token >>
         get >>= inside_braces break false indent
+    | AND ->
+      if column < indent then error "offside" else
+        emit token >>
+        get >>= inside_braces break false indent
     | _ ->
       if column < indent then error "offside" else
         emit_if (column = indent && insert) COMMA >>
-        nest (token, column) >>
+        nest false (token, column) >>
         get >>= inside_braces break (token <> LOCAL) indent
 
   and inside_local insert indent (token, column) =
@@ -132,7 +136,7 @@ module Offside = struct
         emit IN
       else
         emit_if (column = indent && insert) COMMA >>
-        nest (token, column) >>
+        nest false (token, column) >>
         get >>= inside_local (token <> LOCAL) indent
 
   and inside_let insert indent (token, column) =
@@ -151,12 +155,13 @@ module Offside = struct
         inside_in false column (token, column)
       else
         emit_if (column = indent && insert) COMMA >>
-        nest (token, column) >>
+        nest false (token, column) >>
         get >>= inside_let (token <> LOCAL) indent
 
   and inside_in insert indent (token, column) =
     match token with
-    | RBRACE | COMMA | IN | EOF | RPAR | ELSE | THEN -> unget (token, column)
+    | RBRACE | COMMA | IN | EOF | RPAR | ELSE | THEN | EQUAL ->
+      unget (token, column)
     | SEMI ->
       if column < indent - 2 then error "offside" else
         emit token >>
@@ -170,7 +175,7 @@ module Offside = struct
       let slack = slack_of token in
       if column < indent - slack then unget (token, column) else
         emit_if (slack = 0 && column = indent && insert) SEMI >>
-        nest (token, column) >>
+        nest true (token, column) >>
         get >>= inside_in (slack = 0 && indent <= column) indent
 
   and inside_parens indent (token, column) =
@@ -180,7 +185,7 @@ module Offside = struct
       emit token >>
       get >>= inside_parens indent
     | _ ->
-      nest (token, column) >>
+      nest true (token, column) >>
       get >>= inside_in false indent >>
       get >>= inside_parens indent
 
@@ -203,8 +208,8 @@ module Offside = struct
         emit ELSE >> emit LBRACE >> emit RBRACE >>
         unget (token, column)
 
-  and nest (token, column) =
-    (match token with FUN | REC | IF -> emit LPAR | _ -> unit) >>
+  and nest is_expr (token, column) =
+    (match token with (FUN | REC | IF) when is_expr -> emit LPAR | _ -> unit) >>
     emit token >>
     match token with
     | LBRACE ->
@@ -220,9 +225,11 @@ module Offside = struct
     | DARROW ->
       get >>= fun (token, column) ->
       inside_in false column (token, column) >>
-      emit RPAR
+      if is_expr then emit RPAR else unit
     | EQUAL | DO ->
       get >>= fun (token, column) -> inside_in false column (token, column)
+    | TYPE_ERROR ->
+      get >>= fun (token, column) -> inside_in false column (token, column)
     | IF ->
       inside_if column >>
       emit RPAR
@@ -277,6 +284,7 @@ rule token = parse
   | "import" { IMPORT }
   | "primitive" { PRIMITIVE }
   | "rec" { REC }
+  | "and" { AND }
   | "then" { THEN }
   | "type" { TYPE }
   | "with" { WITH }

parser.mly

@@ -26,7 +26,7 @@ let parse_error s = raise (Source.Error (Source.nowhere_region, s))
 %}
 
 %token HOLE PRIMITIVE
-%token FUN REC LET IN DO WRAP TYPE ELLIPSIS
+%token FUN REC AND LET IN DO WRAP TYPE ELLIPSIS
 %token IF THEN ELSE LOGICAL_OR LOGICAL_AND AS
 %token EQUAL COLON SEAL ARROW SARROW DARROW
 %token WITH
@@ -503,12 +503,24 @@ atbind :
     { $2 }
 */
 ;
+atbinds :
+  | atbind
+    { $1 }
+  | atbind AND atbinds
+    { seqB($1, $3)@@at() }
+;
+recbind :
+  | atbind
+    { $1 }
+  | REC atbinds
+    { recB($2)@@at() }
+;
 bind :
   |
     { EmptyB@@at() }
-  | atbind
+  | recbind
     { $1 }
-  | atbind COMMA bind
+  | recbind COMMA bind
     { seqB($1, $3)@@at() }
   | LOCAL bind IN bind
     { letB($2, $4)@@at() }

prelude/index.1ml

@@ -10,7 +10,7 @@ Fun = {
   type t a b = a ~> b
   id x = x
   const x _ = x
-  bot = rec (bot: _ -> _) => fun x => bot x
+  rec bot: _ -> _ = fun x => bot x
   curry f x y = f (x, y)
   uncurry f (x, y) = f x y
   flip f x y = f y x
@@ -55,7 +55,7 @@ Pair = {
 }
 
 List = {
-  ...rec {type t _} => {type t x = Opt.t (x, t x)}
+  rec type t x = Opt.t (x, t x)
   nil = Opt.none
   hd :: tl = Opt.some (hd, tl)
   case {nil, ::} = Opt.case {

readme.1ml

@@ -46,27 +46,25 @@ p = f (fun x => x)
 
 
 
-type stream = rec t => {hd : int, tl : () ~> opt t} ;; creates rec type
-single x : stream = {hd = x, tl = fun () => none}  ;; b : t rolls value into t
+rec type stream t = {hd : t, tl : () ~> opt (stream t)} ;; creates rec type
+single x : stream _ = {hd = x, tl = fun () => none}  ;; b : t rolls value into t
 {hd = n} = single 5                    ;; pattern match rec value
 do Int.print n                         ;; or:
 do Int.print (single 7).hd             ;; access rec value
 
 
 
 
-count = rec self => fun i =>
-  if i <> 0 then self (i - 1)
+rec count i =
+  if i <> 0 then count (i - 1)
 
-repeat = rec self => fun x : stream =>
-  {hd = x, tl = fun () => some (self x)}
+rec repeat x : stream _ =
+  {hd = x, tl () = some (repeat x)}
 
 
 
-{even, odd} = rec (self : {even : int ~> stream, odd : int ~> stream}) => {
-  even x : stream = {hd = x, tl = fun () => some (self.odd (x + 1))}
-  odd x : stream = {hd = x, tl = fun () => some (self.even (x + 1))}
-}
+rec even x : stream _ = {hd = x, tl () = some (odd (x + 1))}
+and odd x : stream _ = {hd = x, tl () = some (even (x + 1))}