WIP Recursive bindings

Author: polytypic

elab.ml

@@ -372,6 +372,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
 
@@ -574,6 +580,13 @@ Trace.debug (lazy ("[RecT] t = " ^ string_of_norm_typ t));
     | Some canonic ->
       ExT([], lookup_var env (canonic@@path.at)), Pure, [], IL.VarE(canonic))
 
+  | EL.AnnotE(e, t) ->
+    let exp =
+      let open Syntax in
+      let x' = var "annot" in
+      appE(FunE(x'@@t.at, t, VarE(x'@@t.at)@@t.at, Expl@@t.at)@@span[e.at; t.at], e)@@exp.at in
+    elab_exp env exp l
+
 (*
 rec (X : (b : type) => {type t; type u a}) fun (b : type) => {type t = (X int.u b, X bool.t); type u a = (a, X b.t)}
 s1 = ?Xt:*->*, Xu:*->*->*. !b:*. [= b] -> {t : [= Xt b], u : !a:*. [= a] => [= Xu b a]}

lexer.mll

@@ -108,10 +108,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 >>
+        nest false token >>
         get >>= inside_braces break (token <> LOCAL) indent
 
   and inside_local insert indent (token, column) =
@@ -128,7 +132,7 @@ module Offside = struct
         emit IN
       else
         emit_if (column = indent && insert) COMMA >>
-        nest token >>
+        nest false token >>
         get >>= inside_local (token <> LOCAL) indent
 
   and inside_let insert indent (token, column) =
@@ -147,12 +151,12 @@ module Offside = struct
         inside_in false column (token, column)
       else
         emit_if (column = indent && insert) COMMA >>
-        nest token >>
+        nest false token >>
         get >>= inside_let (token <> LOCAL) indent
 
   and inside_in insert indent (token, column) =
     match token with
-    | RBRACE | COMMA | IN | EOF | RPAR -> unget (token, column)
+    | RBRACE | COMMA | IN | EOF | RPAR | EQUAL -> unget (token, column)
     | SEMI ->
       if column < indent - 2 then error "offside" else
         emit token >>
@@ -170,18 +174,18 @@ 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 >>
+        nest true token >>
         get >>= inside_in (slack = 0 && indent < column) indent
 
   and inside_parens (token, column) =
     match token with
     | RPAR -> emit token
-    | _ -> nest token >> get >>= inside_parens
+    | _ -> nest true token >> get >>= inside_parens
 
-  and nest token =
+  and nest is_expr token =
     match token with
     | FUN | REC ->
-      emit LPAR >> emit token
+      if is_expr then emit LPAR >> emit token else emit token
     | _ ->
       emit token >>
       match token with
@@ -197,7 +201,7 @@ 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)
       | _ ->
@@ -251,6 +255,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
@@ -456,12 +456,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

@@ -48,7 +48,7 @@ Alt = {
 ;;
 
 Opt = {
-  type t x = Alt.t {} x
+  type t = Alt.t {}
   none = Alt.inl ()
   some = Alt.inr
   case {none, some} = Alt.case {inl () = none, inr = some}
@@ -68,7 +68,7 @@ Pair = {
 
 List = {
   local ...Opt, ...Fun
-  ...rec {type t _} => {type t x = Opt.t (x, t x)}
+  rec type t x = Opt.t (x, t x)
   nil :@ t _ = none
   hd :: tl :@ t _ = some (hd, tl)
   case {nil, (::)} (x :@ t _) = x |> 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
-({hd = n} :@ stream) = single 5        ;; p :@ t pattern matches on rec value
-do Int.print n                         ;; or:
-do Int.print (single 7 @: stream).hd   ;; e @: t unrolls rec value directly
+rec type stream t = {hd : t, tl : () ~> opt (stream t)} ;; creates rec type
+single x :@ stream _ = {hd = x, tl () = none}  ;; b :@ t rolls value into t
+({hd = n} :@ stream _) = single 5        ;; p :@ t pattern matches on rec value
+do Int.print n                           ;; or:
+do Int.print (single 7 @: stream _).hd   ;; e @: t unrolls rec value directly
 
 
 
 
-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 =>
-  {hd = x, tl = fun () => some (self x)} :@ stream
+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

@@ -166,46 +166,37 @@ type_error rec (R: {}) => {
   kaboom () = R
 }
 
-Kaboom = rec (R: rec R => {kaboom: () ~> R}) => {kaboom () = R} :@ (= R)
+rec Kaboom : rec R => {kaboom: () ~> R} = {kaboom () = Kaboom} :@ (= Kaboom)
+
+rec isEven n = n == 0 || isOdd (n-1)
+and isOdd n = n == 1 || (not (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 : 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 : 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))))
@@ -232,7 +223,7 @@ type (a `>>` b) c = c
 ;;
 
 Hungry = {
-  type eat a = rec eat_a => a ~> eat_a
+  rec type eat a = a ~> eat a
 
   eater 'a = rec (eater: eat a) => (fun a => eater) :@ eat a
 
@@ -242,8 +233,8 @@ Hungry = {
 }
 
 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
 
@@ -267,7 +258,7 @@ ListN = let
   }
   type T x n (type t _ _) = (type p _) -> I x p t ~> p n
 in {
-  ...rec {type t _ _} => {type t x n = wrap T x n t}
+  rec type t x n = wrap T x n t
 
   case 'x 'n (type p _) (cs: I x p t) (e :# wrap T x n t :@ t x n) =
     e p cs
@@ -287,9 +278,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 : ARRAY =
+  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 (pr (A.sub a i) ; print " " ; loop (i + 1))
   loop 0
@@ -63,13 +63,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)
@@ -88,10 +88,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 () else (printprimes (n - 1) ; Int.print (nthprime n) ; print "\n")
 do printprimes 20