WIP Recursive bindings

Author: polytypic

elab.ml

@@ -574,6 +574,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 }
   | "unwrap" { UNWRAP }

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 UNWRAP TYPE ELLIPSIS
+%token FUN REC AND LET IN DO WRAP UNWRAP TYPE ELLIPSIS
 %token IF THEN ELSE LOGICAL_OR LOGICAL_AND AS
 %token EQUAL COLON SEAL ARROW SARROW DARROW
 %token WITH
@@ -436,12 +436,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() }

regression.1ml

@@ -156,48 +156,41 @@ type_error rec (R: {}) => {
   kaboom () = R
 }
 
-Kaboom = rec (R: rec R => {kaboom: () ~> R}) => @(= R) {
-  kaboom () = 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 =
-        @(T.Even.t x) {head, tail}
-      size 'x (v: T.Even.t x) = 1 + R.Odd.size v.@(T.Even.t _).tail
-    }
-    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) =
-        v.@(T.Odd.t x) |> 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.@(T.Even.t _).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.@(T.Odd.t x) |> Opt.case {
+        none = 0
+        some = Even.size
+      }
   }
 
   one = Odd.size (Odd.make (some (Even.make true (Odd.make none))))
@@ -224,7 +217,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: eat a = rec (eater: eat a) => @(eat a) fun a => eater
 
@@ -234,8 +227,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
 
@@ -259,7 +252,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 =
     (unwrap e.@(t _ _): wrap T x n t) p cs
@@ -279,9 +272,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
     }
 }