WIP Recursive bindings

elab.ml

@@ -567,6 +567,13 @@ Trace.debug (lazy ("[RecT] t = " ^ string_of_norm_typ t));
       IL.LetE(e, "_", materialize_typ t)
     )
 
+  | 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

@@ -82,6 +82,7 @@ rule token = parse
   | "wrap" { WRAP }
   | "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 DARROW
 %token WITH
@@ -372,12 +372,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 SEMI bind
+  | recbind SEMI bind
     { SeqB($1, $3)@@at() }
 ;
 

regression.1ml

@@ -68,47 +68,40 @@ 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};
-    };
-    Odd = {
-      type t x = opt (R.Even.t x);
+  T = {
+    rec Even = {
+      type t x = {head: x; tail: Odd.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) =
-        caseopt v.@(T.Odd.t x)
-          (fun () => 0)
-          (fun 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 =
+      caseopt v.@(T.Odd.t x)
+        (fun () => 0)
+        (fun e => Even.size e);
   };
 
   one = Odd.size (Odd.make (some (Even.make true (Odd.make none))));
@@ -117,7 +110,7 @@ in {
 ;;
 
 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);
 
@@ -127,8 +120,8 @@ Hungry = {
 };
 
 PolyRec = {
-  type l a = rec (type t) => alt a t;
-  ...rec {type t a} => {type t a = alt a (t (type (a, a)))};
+  rec type l a = alt a (l a);
+  rec type t a = alt a (t (type (a, a)));
 
   t_int = t int;
 
@@ -152,7 +145,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;
@@ -174,9 +167,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 = nil;
-      (::) x xs = xy x :: map xs;
+      (::) x xs = xy x :: map xy xs;
     };
 };

syntax.ml

@@ -51,6 +51,7 @@ and exp' =
   | UnwrapE of var * typ
   | UnrollE of var * typ
   | RecE of var * typ * exp
+  | AnnotE of exp * typ
 
 and bind = (bind', unit) phrase
 and bind' =
@@ -203,9 +204,7 @@ let unrollE(e, t) =
     let x' = var "@" in
     letE(VarB(x'@@e.at, e)@@e.at, UnrollE(x'@@e.at, t)@@span[e.at; t.at])
 
-let annotE(e, t) =
-  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)
+let annotE(e, t) = AnnotE(e, t)
 
 let sealE(e, t) =
   (* TODO: clone t! *)
@@ -327,6 +326,65 @@ let rollP(p, t2) =
       TypE(t1.it@@p.at)@@p.at)@@p.at)@@p.at)@@span[p.at; t2.at])
 
 
+(* Substitution *)
+
+type 'a subst = (string * 'a) list
+
+let subst_exp_var (s: 'a subst) (v: var) = try List.assoc v.it s with Not_found -> VarE(v)
+
+let rec subst_exp_typ s t =
+  (match t.it with
+  | PathT(e) -> PathT(subst_exp_exp s e)
+  | PrimT(s) -> PrimT(s)
+  | TypT -> TypT
+  | HoleT -> HoleT
+  | StrT(d) -> StrT(subst_exp_dec s d)
+  | FunT(v, td, tr, e, i) ->
+    FunT(v, subst_exp_typ s td, subst_exp_typ ((v.it, VarE(v))::s) tr, e, i)
+  | WrapT(t) -> WrapT(subst_exp_typ s t)
+  | EqT(e) -> EqT(subst_exp_exp s e)
+  | AsT(tl, tr) -> AsT(subst_exp_typ s tl, subst_exp_typ s tr)
+  | WithT(t, vs, e) -> WithT(subst_exp_typ s t, vs, subst_exp_exp s e)
+  )@@t.at
+
+and subst_exp_dec s d =
+  (match d.it with
+  | EmptyD -> EmptyD
+  | SeqD(dl, dr) -> SeqD(subst_exp_dec s dl, subst_exp_dec s dr)
+  | VarD(v, t) -> VarD(v, subst_exp_typ s t)
+  | InclD(t) -> InclD(subst_exp_typ s t)
+  )@@d.at
+
+and subst_exp_exp s e =
+  (match e.it with
+  | VarE(v) -> subst_exp_var s v
+  | PrimE(s) -> PrimE(s)
+  | TypE(t) -> TypE(subst_exp_typ s t)
+  | StrE(b) -> StrE(subst_exp_bind s b)
+  | FunE(v, t, e, i) ->
+    FunE(v, subst_exp_typ s t, subst_exp_exp ((v.it, VarE(v))::s) e, i)
+  | WrapE(v, t) -> wrapE(subst_exp_var s v@@e.at, subst_exp_typ s t)
+  | RollE(v, t) -> rollE(subst_exp_var s v@@e.at, subst_exp_typ s t)
+  | IfE(v, ec, ea, t) ->
+    ifE(subst_exp_var s v@@e.at, subst_exp_exp s ec, subst_exp_exp s ea, subst_exp_typ s t)
+  | DotE(e, v) -> DotE(subst_exp_exp s e, v)
+  | AppE(vf, va) -> appE(subst_exp_var s vf@@e.at, subst_exp_var s va@@e.at)
+  | UnwrapE(v, t) -> unwrapE(subst_exp_var s v@@e.at, subst_exp_typ s t)
+  | UnrollE(v, t) -> unrollE(subst_exp_var s v@@e.at, subst_exp_typ s t)
+  | RecE(v, t, e) -> RecE(v, subst_exp_typ s t, subst_exp_exp ((v.it, VarE(v))::s) e)
+  | AnnotE(e, t) -> AnnotE(subst_exp_exp s e, subst_exp_typ s t)
+  )@@e.at
+
+and subst_exp_bind s b =
+  (match b.it with
+  | EmptyB -> EmptyB
+  | SeqB(bl, br) -> SeqB(subst_exp_bind s bl, subst_exp_bind s br)
+  | VarB(v, e) -> VarB(v, subst_exp_exp s e)
+  | InclB(e) -> InclB(subst_exp_exp s e)
+  | TypeErrorB(e) -> TypeErrorB(subst_exp_exp s e)
+  )@@b.at
+
+
 (* String conversion *)
 
 let node label = function
@@ -378,6 +436,7 @@ let label_of_exp e =
   | UnwrapE _ -> "UnwrapE"
   | UnrollE _ -> "UnrollE"
   | RecE _ -> "RecE"
+  | AnnotE _ -> "AnnotE"
 
 let label_of_bind b =
   match b.it with
@@ -436,6 +495,7 @@ and string_of_exp e =
   | UnwrapE(x, t) -> node' [string_of_var x; string_of_typ t]
   | UnrollE(x, t) -> node' [string_of_var x; string_of_typ t]
   | RecE(x, t, e) -> node' [string_of_var x; string_of_typ t; string_of_exp e]
+  | AnnotE(e, t) -> node' [string_of_exp e; string_of_typ t]
 
 and string_of_bind b =
   let node' = node (label_of_bind b) in
@@ -445,3 +505,55 @@ and string_of_bind b =
   | VarB(x, e) -> node' [string_of_var x; string_of_exp e]
   | InclB(e) -> node' [string_of_exp e]
   | TypeErrorB(e) -> node' [string_of_exp e]
+
+
+(* rec ... and ... *)
+
+let rec extract_sig_exp p e =
+  let s, d =
+    match e.it with
+    | StrE(b) ->
+      let s, d = extract_sig_bind p b in
+      s, StrT(d)
+    | TypE _ ->
+      [], TypT
+    | FunE(v, td, e, i) ->
+      let _, tc = extract_sig_exp p e in
+      let p =
+        if i.it == Impl then Pure else
+        match e.it with
+        | FunE _ -> Pure
+        | TypE _ -> Pure
+        | _ -> Impure in
+      [], FunT(v, td, tc, p@@e.at, i)
+    | AnnotE(e, t) ->
+      [], t.it
+    | _ -> [], HoleT in
+  s, d@@e.at
+
+and extract_sig_bind p b =
+  let s, d =
+    match b.it with
+    | EmptyB -> [], EmptyD
+    | SeqB(bl, br) ->
+      let sl, dl = extract_sig_bind p bl in
+      let sr, dr = extract_sig_bind p br in
+      (sl @ sr), SeqD(dl, dr)
+    | VarB(v, e) ->
+      let s, t = extract_sig_exp (DotE(p, v)@@b.at) e in
+      ((v.it, DotE(p, v)) :: s), VarD(v, t)
+    | InclB(e) ->
+      [], EmptyD
+    | TypeErrorB(e) -> [], EmptyD in
+  s, d@@b.at
+
+let recB(b) =
+  let r = var "R" in
+  let s, d = extract_sig_bind (VarE(r@@b.at)@@b.at) b in
+  let b' = subst_exp_bind s b in
+  let b' = InclB(RecE(r@@b.at, StrT(d)@@b.at, StrE(b')@@b.at)@@b.at) in
+(*
+  List.iter (fun (v, e) -> Printf.printf "%s %s\n" v (string_of_exp (e@@b.at))) s;
+  Printf.printf "%s\n" (string_of_bind (b'@@b.at));
+ *)
+  b'