WIP Recursive bindings

elab.ml

@@ -397,6 +397,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
 

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
   } :> {

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

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
@@ -458,12 +458,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

@@ -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 () else self (i - 1)
+rec count i =
+  if i == 0 then () else 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))}
 
 
 

regression.1ml

@@ -215,46 +215,37 @@ type_error rec (R: {}) => {
   kaboom () = R
 }
 
-Kaboom = rec (R: rec R => {kaboom: () ~> R}) : (= R) => {kaboom () = R}
+rec Kaboom : rec R => {kaboom: () ~> R} = {kaboom () = Kaboom}
+
+rec isEven n = n == 0 || isOdd (n-1)
+and isOdd n = n == 1 || (n <> 0 && isEven (n-1))
 
 ;;
 
 Mutually = let
-  T = rec (R: {
-    Even: {type t _}
-    Odd: {type t _}
-  }) => {
-    Even = {
-      type t x = {head: x, tail: R.Odd.t x}
+  T = {
+    rec Even = {
+      type t x = {head: x, tail: Odd.t x}
     }
-    Odd = {
-      type t x = opt (R.Even.t x)
+    and Odd = {
+      type t x = opt (Even.t x)
     }
   }
 in {
-  ...rec (R: {
-    Even: {
-      size 'x: T.Even.t x ~> int
-    }
-    Odd: {
-      size 'x: T.Odd.t x ~> int
-    }
-  }) => {
-    Even = {
-      ...T.Even
-      make 'x (head: x) (tail: T.Odd.t x) : T.Even.t x =
-        {head, tail}
-      size 'x (v: T.Even.t x) = 1 + R.Odd.size v.tail
-    }
-    Odd = {
-      ...T.Odd
-      make 'x (v: opt (T.Even.t x)) : T.Odd.t x = v
-      size 'x (v: T.Odd.t x) =
-        v |> Opt.case {
-          none = 0
-          some e = R.Even.size e
-        }
-    }
+  rec Even = {
+    ...T.Even
+    make 'x (head: x) (tail: T.Odd.t x) : T.Even.t x =
+      {head, tail}
+    size 'x (v: T.Even.t x) : int = 1 + Odd.size v.tail
+  }
+  and Odd = {
+    ...T.Odd
+    make 'x (v: opt (T.Even.t x)) : T.Odd.t x = v
+    size 'x (v: T.Odd.t x) : int =
+      v |> Opt.case {
+        none = 0
+        some = Even.size
+      }
   }
 
   one = Odd.size (Odd.make (some (Even.make true (Odd.make none))))
@@ -284,9 +275,9 @@ AnnotRecType = {
 }
 
 Hungry = {
-  type eat a = rec eat_a => a ~> eat_a
+  rec type eat a = a ~> eat a
 
-  eater 'a = rec (eater: eat a) : eat a => fun a => eater
+  rec eater 'a: eat a = fun a => eater
 
   do eater 1 2
   do eater 1 2 3
@@ -299,8 +290,8 @@ type_error rec {type t _, type u _} => {
 type_error type rec t => t
 
 PolyRec = {
-  type l a = rec (type t) => a | t
-  ...rec {type t a} => {type t a = a | t (a, a)}
+  rec type l a = a | l a
+  rec type t a = a | t (a, a)
 
   t_int = t int
 
@@ -322,7 +313,7 @@ ListN = let
     (::) '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}
+  rec type t x n = wrap (type p _) -> I x p t ~> p n
 
   case 'x 'n (type p _) (cs: I x p t) (e : t _ _) =
     e p cs
@@ -340,9 +331,9 @@ in {
 
 ListN = {
   ...ListN
-  map 'x 'y (xy: x ~> y) = rec (map 'n: t x n ~> t y n) =>
+  rec map 'x 'y 'n (xy: x ~> y) : t x n ~> t y n =
     case (t _) {
       nil
-      x :: xs = xy x :: map xs
+      x :: xs = xy x :: map xy xs
     }
 }

russo.1ml

@@ -30,11 +30,11 @@ ArraySucc (A : ARRAY) = {
     else (a.1, A.update a.2 (i / 2) x)
 }
 
-MkArray = rec (mkArray : int ~> ARRAY) => fun n =>
-  if n == 0 then ArrayZero else ArraySucc (mkArray (n - 1)) : ARRAY
+rec MkArray n =
+  if n == 0 then ArrayZero else ArraySucc (MkArray (n - 1)) : ARRAY
 
 printArray 't (A : ARRAY) (pr : t ~> ()) a =
-  let loop = rec loop => fun i =>
+  let rec loop i =
     if i == A.dim then
       print "\n"
     else
@@ -67,13 +67,13 @@ type STREAM = {
 }
 
 divides k n =
-  let loop = rec loop => fun i => (i * k == n) || ((i * k < n) && loop (i + 1))
+  let rec loop i = (i * k == n) || ((i * k < n) && loop (i + 1))
   loop 1
 
 sift (S : STREAM) :> STREAM = {
   type state = S.state
   divisor = S.value S.start
-  filter = rec filter => fun s =>
+  rec filter s =
     if divides divisor (S.value s) then filter (S.next s) else s
   start = filter S.start
   next s = filter (S.next s)
@@ -92,10 +92,10 @@ Sieve :> STREAM = {
   value (S :# state) = S.value S.start
 }
 
-nthstate = rec (nthstate : int ~> Sieve.state) => fun n =>
+rec nthstate n =
   if n == 0 then Sieve.start else Sieve.next (nthstate (n -1))
 nthprime n = Sieve.value (nthstate n)
 
-printprimes = rec loop => fun n =>
-  if n == 0 then () else loop (n - 1) ; Int.print (nthprime n) ; print "\n"
+rec printprimes n =
+  if n <> 0 then printprimes (n - 1) ; Int.print (nthprime n) ; print "\n"
 do printprimes 20