[Experiments] Type representation

src/codegen/compile.ml

@@ -5497,13 +5497,12 @@ end (* Var *)
 (* FIX ME: calling into the prelude will not work if we ever need to compile a program
    that requires top-level cps conversion;
    use new prims instead *)
-module Prelude = struct
+module Internals = struct
   let call_prelude_function env ae var =
-    match Var.get_val env ae var with
-    | (SR.Const(_, Const.Fun mk_fi), code) ->
-      code ^^
-        compile_unboxed_zero ^^ (* A dummy closure *)
-          G.i (Call (nr (mk_fi ())))
+    match VarEnv.lookup_var ae var with
+    | Some (VarEnv.Const(_, Const.Fun mk_fi)) ->
+       compile_unboxed_zero ^^ (* A dummy closure *)
+       G.i (Call (nr (mk_fi ())))
     | _ -> assert false
 
   let add_cycles env ae = call_prelude_function env ae "@add_cycles"
@@ -5560,8 +5559,8 @@ module FuncDec = struct
     Func.of_body outer_env [] [] (fun env -> G.with_region at (
       message_start env sort ^^
       (* cycles *)
-      Prelude.reset_cycles env outer_ae ^^
-      Prelude.reset_refund env outer_ae ^^
+      Internals.reset_cycles env outer_ae ^^
+      Internals.reset_refund env outer_ae ^^
       (* reply early for a oneway *)
       (if control = Type.Returns
        then
@@ -6818,7 +6817,7 @@ and compile_exp (env : E.t) ae exp =
           let (set_meth_pair, get_meth_pair) = new_local env "meth_pair" in
           let (set_arg, get_arg) = new_local env "arg" in
           let _, _, _, ts, _ = Type.as_func e1.note.Note.typ in
-          let add_cycles = Prelude.add_cycles env ae in
+          let add_cycles = Internals.add_cycles env ae in
           code1 ^^ StackRep.adjust env fun_sr SR.Vanilla ^^
           set_meth_pair ^^
           compile_exp_as env ae SR.Vanilla e2 ^^ set_arg ^^
@@ -7360,7 +7359,7 @@ and compile_exp (env : E.t) ae exp =
       let (set_arg, get_arg) = new_local env "arg" in
       let (set_k, get_k) = new_local env "k" in
       let (set_r, get_r) = new_local env "r" in
-      let add_cycles = Prelude.add_cycles env ae in
+      let add_cycles = Internals.add_cycles env ae in
       compile_exp_as env ae SR.Vanilla f ^^ set_meth_pair ^^
       compile_exp_as env ae SR.Vanilla e ^^ set_arg ^^
       compile_exp_as env ae SR.Vanilla k ^^ set_k ^^
@@ -7510,7 +7509,7 @@ and compile_exp (env : E.t) ae exp =
     let (set_r, get_r) = new_local env "r" in
     let mk_body env1 ae1 = compile_exp_as env1 ae1 SR.unit exp_f in
     let captured = Freevars.captured exp_f in
-    let add_cycles = Prelude.add_cycles env ae in
+    let add_cycles = Internals.add_cycles env ae in
     FuncDec.async_body env ae ts captured mk_body exp.at ^^
     set_closure_idx ^^
 

src/ir_def/arrange_ir.ml

@@ -67,6 +67,7 @@ and prim = function
   | AwaitPrim         -> Atom "AwaitPrim"
   | AssertPrim        -> Atom "AssertPrim"
   | ThrowPrim         -> Atom "ThrowPrim"
+  | TypRep t          -> "TypRep" $$ [typ t]
   | ShowPrim t        -> "ShowPrim" $$ [typ t]
   | SerializePrim t   -> "SerializePrim" $$ List.map typ t
   | DeserializePrim t -> "DeserializePrim" $$ List.map typ t

src/ir_def/check_ir.ml

@@ -497,6 +497,9 @@ let rec check_exp env (exp:Ir.exp) : unit =
     | AssertPrim, [exp1] ->
       typ exp1 <: T.bool;
       T.unit <: t
+    | TypRep ot, [] ->
+      check (T.shared ot) "gen_typrep is not defined for operand type";
+      Construct.typRepT <: t
     | ShowPrim ot, [exp1] ->
       check env.flavor.has_show "show expression in non-show flavor";
       check (Show.can_show ot) "show is not defined for operand type";

src/ir_def/construct.ml

@@ -185,6 +185,22 @@ let optE e =
    at = no_region;
  }
 
+let arrayE t es =
+  let effs = List.map eff es in
+  let eff = List.fold_left max_eff T.Triv effs in
+  { it = PrimE (ArrayPrim (Const, t), es);
+    note = Note.{ def with typ = T.Array t; eff };
+    at = no_region;
+  }
+
+let mutArrayE t es =
+  let effs = List.map eff es in
+  let eff = List.fold_left max_eff T.Triv effs in
+  { it = PrimE (ArrayPrim (Var, t), es);
+    note = Note.{ def with typ = T.Array (T.Mut t); eff };
+    at = no_region;
+  }
+
 let tagE i e =
  { it = PrimE (TagPrim i, [e]);
    note = Note.{ def with typ = T.Variant [{T.lab = i; typ = typ e; depr = None}]; eff = eff e };
@@ -216,6 +232,18 @@ let blockE decs exp =
       note = Note.{ def with typ; eff }
     }
 
+let natE n =
+  { it = LitE (NatLit n);
+    at = no_region;
+    note = Note.{ def with typ = T.nat }
+  }
+
+let nat32E n =
+  { it = LitE (Nat32Lit n);
+    at = no_region;
+    note = Note.{ def with typ = T.(Prim Nat32) }
+  }
+
 let textE s =
   { it = LitE (TextLit s);
     at = no_region;
@@ -301,6 +329,16 @@ let dotE exp name typ =
     }
   }
 
+let idxE exp1 exp2 =
+  { it = PrimE (IdxPrim, [exp1; exp2]);
+    at = no_region;
+    note = Note.{ def with
+      typ = T.as_array (typ exp1);
+      eff = max_eff (eff exp1) (eff exp2)
+    }
+  }
+
+
 let switch_optE exp1 exp2 pat exp3 typ1  =
   { it =
       SwitchE
@@ -353,6 +391,7 @@ let tupE exps =
     note = Note.{ def with typ = T.Tup (List.map typ exps); eff };
   }
 
+(* TODO: Is it ok to share this value? *)
 let unitE = tupE []
 
 let breakE l exp =
@@ -505,16 +544,6 @@ let funcD ((id, typ) as f) x exp =
 let nary_funcD ((id, typ) as f) xs exp =
   letD f (nary_funcE id typ xs exp)
 
-(* Continuation types *)
-
-let answerT = T.unit
-
-let contT typ = T.Func (T.Local, T.Returns, [], T.as_seq typ, [])
-
-let err_contT =  T.Func (T.Local, T.Returns, [], [T.catch], [])
-
-let cpsT typ = T.Func (T.Local, T.Returns, [], [contT typ; err_contT], [])
-
 (* Sequence expressions *)
 
 let seqE es =
@@ -626,3 +655,52 @@ let unreachableE =
   (* Do we want a dedicated UnreachableE in the AST? *)
   loopE unitE
 
+(* Internal types *)
+
+(*
+These type definitions mirror the type definitions in prelude/internals.mo.
+It would be good to get rid of that duplication somehow, and use those
+in `prelude/internals.mo` directly.
+*)
+
+let answerT = T.unit
+
+let contT typ = T.Func (T.Local, T.Returns, [], T.as_seq typ, [])
+
+let err_contT =  T.Func (T.Local, T.Returns, [], [T.catch], [])
+
+let cpsT typ = T.Func (T.Local, T.Returns, [], [contT typ; err_contT], [])
+
+let (typRepT, typRepFieldT) =
+  let open T in
+  let typRepC = Con.fresh "TypRep" (Abs ([], Pre)) in
+  let typRepT = Con (typRepC, []) in
+  let fieldC = Con.fresh "Field" (Abs ([], Pre)) in
+  let fieldT = Con (fieldC, []) in
+  let fieldsT = Array fieldT in
+  let objSortT = Variant (List.sort compare_field (
+    List.map (fun lab -> { lab; typ = T.unit; depr = None }) [
+      "object_"; "actor_"; "module_"; "memory"
+    ]
+  )) in
+  let typRepRhs = Variant (List.sort compare_field (
+    List.map (fun lab -> { lab; typ = T.unit; depr = None }) [
+      "null_"; "bool"; "nat"; "int";
+      "nat8"; "nat16"; "nat32"; "nat64";
+      "int8"; "int16"; "int32"; "int64";
+      "word8"; "word16"; "word32"; "word64";
+      "float"; "char"; "text"; "blob"; "error"; "principal";
+      "func_"; "any"; "non"
+    ] @ List.map (fun (lab,typ) -> { lab; typ; depr = None }) [
+      ("ref", Array (Mut typRepT));
+      ("obj", Tup [objSortT; Array fieldT]);
+      ("variant", fieldsT);
+      ("array", typRepT);
+      ("opt", typRepT);
+      ("tup", Array typRepT);
+    ]
+  )) in
+  let fieldRhs = Tup [text; Prim Nat32; typRepT] in
+  set_kind typRepC (Def ([], typRepRhs));
+  set_kind fieldC (Def ([], fieldRhs));
+  typRepT, fieldT

src/ir_def/construct.mli

@@ -58,8 +58,12 @@ val ic_rejectE : exp -> exp
 val ic_callE : exp -> exp -> exp -> exp -> exp
 val projE : exp -> int -> exp
 val optE : exp -> exp
+val arrayE : typ -> exp list -> exp
+val mutArrayE : typ -> exp list -> exp
 val tagE : id -> exp -> exp
 val blockE : dec list -> exp -> exp
+val natE : Mo_values.Numerics.Nat.t -> exp
+val nat32E : Mo_values.Numerics.Nat32.t -> exp
 val textE : string -> exp
 val blobE : string -> exp
 val letE : var -> exp -> exp -> exp
@@ -76,6 +80,7 @@ val callE : exp -> typ list -> exp -> exp
 
 val ifE : exp -> exp -> exp -> typ -> exp
 val dotE : exp -> Type.lab -> typ -> exp
+val idxE : exp -> exp -> exp
 val switch_optE : exp -> exp -> pat -> exp -> typ -> exp
 val switch_variantE : exp -> (id * pat * exp) list -> typ -> exp
 val tupE : exp list -> exp
@@ -113,13 +118,6 @@ val nary_funcD : var -> var list -> exp -> dec
 
 val let_no_shadow : var -> exp -> dec list -> dec list
 
-(* Continuations *)
-
-val answerT : typ
-val contT : typ -> typ
-val err_contT : typ
-val cpsT : typ -> typ
-
 (* Sequence expressions *)
 
 val seqE : exp list -> exp
@@ -130,3 +128,20 @@ val (-->) : var -> exp -> exp
 val (-->*) : var list -> exp -> exp (* n-ary local *)
 val forall : typ_bind list -> exp -> exp (* generalization *)
 val (-*-) : exp -> exp -> exp       (* application *)
+
+(* Internal types *)
+
+(*
+These type definitions mirror the type definitions in prelude/internals.mo.
+It would be good to get rid of that duplication somehow, and use those
+in `prelude/internals.mo` directly.
+*)
+
+
+val answerT : typ
+val contT : typ -> typ
+val err_contT : typ
+val cpsT : typ -> typ
+val typRepT : typ
+val typRepFieldT : typ
+

src/ir_def/ir.ml

@@ -119,6 +119,7 @@ and prim =
   | AwaitPrim                         (* await *)
   | AssertPrim                        (* assertion *)
   | ThrowPrim                         (* throw *)
+  | TypRep of Type.typ                (* Generates the type representation *)
   | ShowPrim of Type.typ              (* debug_show *)
   | SerializePrim of Type.typ list    (* Candid serialization prim *)
   | DeserializePrim of Type.typ list  (* Candid deserialization prim *)