WIP Recursive bindings

elab.ml

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

@@ -85,6 +85,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 LOCAL IN DO WRAP UNWRAP TYPE INCLUDE END
+%token FUN REC AND LET LOCAL IN DO WRAP UNWRAP TYPE INCLUDE END
 %token IF THEN ELSE LOGICAL_OR LOGICAL_AND AS
 %token EQUAL COLON SEAL ARROW DARROW
 %token WITH
@@ -376,12 +376,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

@@ -38,40 +38,33 @@ type_error {
 
 ;;
 
+rec isEven n = n == 0 || isOdd (n-1)
+and isOdd n = n == 1 || (not (n == 0) && isEven (n-1));
+
+;;
+
 Mutually = {
-  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);
     };
   };
 
-  V = rec (R: {
-    Even: {
-      make 'x: x => T.Odd.t x => T.Even.t x;
-      size 'x: T.Even.t x -> int;
-    };
-    Odd: {
-      make 'x: opt (T.Even.t x) => T.Odd.t x;
-      size 'x: T.Odd.t x -> int;
-    };
-  }) => {
-    Even = {
+  V = {
+    rec 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 = {
+      size 'x (v: T.Even.t x) : int = 1 + Odd.size v.@(T.Even.t _).tail;
+    }
+    and 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) =
+      size 'x (v: T.Odd.t x) : int =
         caseopt v.@(T.Odd.t x)
           (fun () => 0)
-          (fun e => R.Even.size e);
+          (fun e => Even.size e);
     };
   };
 };
@@ -97,7 +90,7 @@ 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 t a = alt a (t (type (a, a)));
 
   t_int = t int;
 
@@ -121,7 +114,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;
@@ -143,9 +136,9 @@ in {
 
 ListN = {
   ...ListN;
-  map 'x 'y 'n (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 y) {
       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' =
@@ -195,9 +196,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! *)
@@ -316,6 +315,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
@@ -367,6 +425,7 @@ let label_of_exp e =
   | UnwrapE _ -> "UnwrapE"
   | UnrollE _ -> "UnrollE"
   | RecE _ -> "RecE"
+  | AnnotE _ -> "AnnotE"
 
 let label_of_bind b =
   match b.it with
@@ -425,6 +484,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
@@ -434,3 +494,56 @@ 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) ->
+      let s, t = extract_sig_exp p e in
+      s, InclD(t)
+    | 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'