Mutually recursive ADTs and labels in Core

- Removed `ELabel` construct from Core
- Added `DD_Label` constructor to `Core.data_def`

src/Lang/Core.mli

@@ -104,21 +104,36 @@ and ctor_type = {
 (** Variables *)
 type var = Var.t
 
-(** ADT definition *)
-type data_def = {
-  dd_tvar  : TVar.ex;
-    (** Type variable, that represents this ADT. *)
+(** Data-like definition (ADT or label) *)
+type data_def =
+  | DD_Data of (** Algebraic datatype *)
+    { tvar  : TVar.ex;
+        (** Type variable, that represents this ADT. *)
 
-  dd_proof : var;
-    (** An irrelevant variables that stores the proof that this ADT has
-      the following constructors. *)
+      proof : var;
+        (** An irrelevant variable that stores the proof that this ADT has
+          the following constructors. *)
 
-  dd_args  : TVar.ex list;
-    (** List of type parameters of this ADT. *)
+      args  : TVar.ex list;
+        (** List of type parameters of this ADT. *)
 
-  dd_ctors : ctor_type list
-    (** List of constructors. *)
-}
+      ctors : ctor_type list
+        (** List of constructors. *)
+    }
+
+  | DD_Label of (** Label *)
+    { tvar      : keffect tvar;
+        (** Type variable that represents effect of this label *)
+
+      var       : var;
+        (** Regular variable that would store the label *)
+
+      delim_tp  : ttype;
+        (** Type of the delimiter *)
+
+      delim_eff : effect
+        (** Effect of the delimiter *)
+    }
 
 (* ========================================================================= *)
 (** Operations on kinds *)
@@ -200,9 +215,6 @@ type expr =
     (** Shallow pattern matching. The first parameter is the proof that the
       type of the matched value is an ADT *)
 
-  | ELabel of keffect tvar * var * ttype * effect * expr
-    (** Create a fresh runtime tag for control operators. *)
-
   | EShift of value * var * expr * ttype
     (** Shift-0 operator parametrized by runtime tag, binder for continuation
       variable, body, and the type of the whole expression. *)

src/Lang/CorePriv/SExprPrinter.ml

@@ -96,17 +96,28 @@ and tr_ctor_type { ctor_name; ctor_tvars; ctor_arg_types } =
     List.map tr_type ctor_arg_types)
 
 let tr_data_def (dd : Syntax.data_def) =
-  List (
-    tr_tvar_ex dd.dd_tvar ::
-    tr_var  dd.dd_proof ::
-    List (List.map tr_tvar_ex dd.dd_args) ::
-    List.map tr_ctor_type dd.dd_ctors)
+  match dd with
+  | DD_Data adt ->
+    List (
+      Sym "data" ::
+      tr_tvar_ex adt.tvar ::
+      tr_var  adt.proof ::
+      List (List.map tr_tvar_ex adt.args) ::
+      List.map tr_ctor_type adt.ctors)
+
+  | DD_Label lbl ->
+    List [
+      Sym "label";
+      tr_tvar lbl.tvar;
+      tr_var lbl.var;
+      tr_type lbl.delim_tp;
+      tr_type lbl.delim_eff
+    ]
 
 let rec tr_expr (e : Syntax.expr) =
   match e with
   | EValue v -> tr_value v
-  | ELet _ | ELetPure _ | ELetIrr _ | ELetRec _ | EData _ | ELabel _
-  | EReset _ -> 
+  | ELet _ | ELetPure _ | ELetIrr _ | ELetRec _ | EData _ | EReset _ ->
     List (Sym "defs" :: tr_defs e)
   | EApp(v1, v2) ->
     List [ Sym "app"; tr_value v1; tr_value v2 ]
@@ -151,9 +162,6 @@ and tr_defs (e : Syntax.expr) =
     List (Sym "let-rec" :: List.map tr_rec_def rds) :: tr_defs e2
   | EData(dds, e2) ->
     List (Sym "data" :: List.map tr_data_def dds) :: tr_defs e2
-  | ELabel(a, x, tp, eff, e2) ->
-    List [Sym "label"; tr_tvar a; tr_var x; tr_type tp; tr_type eff ] ::
-      tr_defs e2
   | EReset(v, body, x, ret) ->
     List [Sym "reset"; tr_value v; tr_var x; tr_expr ret] :: tr_defs body
 

src/Lang/CorePriv/Syntax.ml

@@ -8,12 +8,19 @@ open TypeBase
 
 type var = Var.t
 
-type data_def = {
-  dd_tvar  : TVar.ex;
-  dd_proof : var;
-  dd_args  : TVar.ex list;
-  dd_ctors : ctor_type list
-}
+type data_def =
+  | DD_Data of
+    { tvar  : TVar.ex;
+      proof : var;
+      args  : TVar.ex list;
+      ctors : ctor_type list
+    }
+  | DD_Label of
+    { tvar      : keffect tvar;
+      var       : var;
+      delim_tp  : ttype;
+      delim_eff : effect
+    }
 
 type expr =
   | EValue    of value
@@ -25,7 +32,6 @@ type expr =
   | ETApp      : value * 'k typ -> expr
   | EData     of data_def list * expr
   | EMatch    of expr * value * match_clause list * ttype * effect
-  | ELabel    of keffect tvar * var * ttype * effect * expr
   | EShift    of value * var * expr * ttype
   | EReset    of value * expr * var * expr
   | ERepl     of (unit -> expr) * ttype * effect

src/Lang/CorePriv/WellTypedInvariant.ml

@@ -186,17 +186,35 @@ let rec check_data : type k.
     failwith "Internal kind error"
 
 let prepare_data_def env (dd : data_def) =
-  let (TVar.Ex a) = dd.dd_tvar in
-  let (env, a) = Env.add_tvar env a in
-  (env, (TVar.Ex a, dd))
-
-let finalize_data_def env (TVar.Ex a, dd) =
-  let (xs, data_tp, ctors) = check_data env (TVar a) dd.dd_args dd.dd_ctors in
-  Env.add_irr_var env dd.dd_proof (Type.t_foralls xs (TData(data_tp, ctors)))
+  match dd with
+  | DD_Data adt ->
+    let (TVar.Ex a) = adt.tvar in
+    let (env, a) = Env.add_tvar env a in
+    (env, DD_Data { adt with tvar = TVar.Ex a })
+  | DD_Label lbl ->
+    let (env, a) = Env.add_tvar env lbl.tvar in
+    (env, DD_Label { lbl with tvar = a })
+
+let finalize_data_def (env, dd_eff) dd =
+  match dd with
+  | DD_Data adt ->
+    let (TVar.Ex a) = adt.tvar in
+    let (xs, data_tp, ctors) = check_data env (TVar a) adt.args adt.ctors in
+    let env =
+      Env.add_irr_var env adt.proof
+        (Type.t_foralls xs (TData(data_tp, ctors))) in
+    (env, dd_eff)
+
+  | DD_Label lbl ->
+    let tp  = tr_type env lbl.delim_tp in
+    let eff = tr_type env lbl.delim_eff in
+    let env = Env.add_var env lbl.var (TLabel(TVar lbl.tvar, tp, eff)) in
+    (* We add nterm effect, since generation of a fresh label is not pure *)
+    (env, Effect.join Effect.nterm dd_eff)
 
 let check_data_defs env dds =
   let (env, dds) = List.fold_left_map prepare_data_def env dds in
-  List.fold_left finalize_data_def env dds
+  List.fold_left finalize_data_def (env, TEffPure) dds
 
 let rec infer_type_eff env e =
   match e with
@@ -242,12 +260,12 @@ let rec infer_type_eff env e =
 
   | EData(dds, e) ->
     let scope = Env.scope env in
-    let env = check_data_defs env dds in
-    let (tp, eff) = infer_type_eff env e in
+    let (env, eff1) = check_data_defs env dds in
+    let (tp, eff2) = infer_type_eff env e in
     begin match
-      Type.supertype_in_scope scope tp, Type.supereffect_in_scope scope eff
+      Type.supertype_in_scope scope tp, Type.supereffect_in_scope scope eff2
     with
-    | Some tp, Some eff -> (tp, eff)
+    | Some tp, Some eff2 -> (tp, Effect.join eff1 eff2)
     | _ ->
       failwith "Internal type error: escaping type variable"
     end
@@ -272,29 +290,6 @@ let rec infer_type_eff env e =
       failwith "Internal type error"
     end
 
-  | ELabel(a, x, tp, eff, e) ->
-    let scope = Env.scope env in
-    let (env, a) = Env.add_tvar env a in
-    let tp  = tr_type env tp  in
-    let eff = tr_type env eff in
-    let env = Env.add_var env x (TLabel(TVar a, tp, eff)) in
-    let (tp, eff) = infer_type_eff env e in
-    begin match
-      Type.supertype_in_scope scope tp, Type.supereffect_in_scope scope eff
-    with
-    | Some tp, Some eff ->
-      (* We add nterm effect, since generation of a fresh label is not pure *)
-      (tp, Effect.join Effect.nterm eff)
-    | _ ->
-      InterpLib.InternalError.report
-        ~reason:"escaping type variable"
-        ~sloc:(SExprPrinter.tr_expr e)
-        ~var:(SExprPrinter.tr_tvar a)
-        ~in_type:(SExprPrinter.tr_type tp)
-        ~in_effect:(SExprPrinter.tr_type eff)
-        ()
-    end
-
   | EShift(v, k, body, tp) ->
     begin match infer_vtype env v with
     | TLabel(eff, tp0, eff0) ->

src/ToCore/DataType.ml

@@ -28,10 +28,11 @@ let prepare_data_def env (dd : S.data_def) =
 let finalize_data_def env (x, (dd : S.data_def)) =
   let (env, args) = List.fold_left_map Env.add_named_tvar env dd.dd_args in
   let ctors = tr_ctor_decls env dd.dd_ctors in
-  { T.dd_tvar  = x;
-    T.dd_proof = dd.dd_proof;
-    T.dd_args  = args;
-    T.dd_ctors = ctors
+  T.DD_Data {
+    tvar  = x;
+    proof = dd.dd_proof;
+    args  = args;
+    ctors = ctors
   }
 
 let tr_data_defs env dds =

src/ToCore/Main.ml

@@ -53,7 +53,12 @@ let rec tr_expr env (e : S.expr) =
     let eff = Type.tr_effect env eff in
     begin match T.TVar.kind a with
     | KEffect ->
-      T.ELabel(a, l, tp, eff, tr_expr env e)
+      T.EData ([DD_Label
+        { tvar      = a;
+          var       = l;
+          delim_tp  = tp;
+          delim_eff = eff
+        }], tr_expr env e)
     | KType | KArrow _ -> failwith "Internal kind error"
     end
 

src/TypeErase.ml

@@ -7,6 +7,12 @@
 module S = Lang.Core
 module T = Lang.Untyped
 
+(** Translate a data or label definition *)
+let tr_data_def (dd : S.data_def) e =
+  match dd with
+  | DD_Data _ -> e
+  | DD_Label lbl -> T.ELabel(lbl.var, e)
+
 (** Translate expression *)
 let rec tr_expr (e : S.expr) =
   match e with
@@ -23,12 +29,10 @@ let rec tr_expr (e : S.expr) =
     tr_value_v v2 (fun v2 ->
     T.EApp(v1, v2)))
   | ETApp(v, _) -> tr_value v
-  | EData(_, e) -> tr_expr e
+  | EData(dds, e) -> List.fold_right tr_data_def dds (tr_expr e)
   | EMatch(_, v, cls, _, _) ->
     tr_value_v v (fun v ->
     T.EMatch(v, List.map tr_clause cls))
-  | ELabel(_, x, _, _, e) ->
-    T.ELabel(x, tr_expr e)
   | EShift(v, x, e, _) ->
     tr_value_v v (fun v ->
     T.EShift(v, x, tr_expr e))