compiling to-evm1.sml

examples/string.timl

@@ -1,5 +1,8 @@
 structure String = struct
 
+(* fun int2str a = __&int2str a *)
+(* fun print a = __&print a *)
+
 open Array
 
 datatype string = String {len : Nat} of array char {len}

examples/unit-test-basic.timl

@@ -5,10 +5,7 @@ fun snd a = __&snd a
 fun not a = __&not a
 val true = __&true
 val false = __&false
-fun int2str a = __&int2str a
 fun nat2int {n : Nat} (a : nat {n}) = __&nat2int a
-fun print a = __&print a
-
 val str_int = int2str
 fun println s = print s; print "\n"
 

micro-timl/micro-timl-ex-pp.sml

@@ -646,6 +646,22 @@ fun pp_e (params as (str_var, str_i, str_s, str_k, pp_t)) s (depth_t, depth) e =
           str ")";
           close_box ()
         )
+      | ENewArrayValues (t, es) =>
+        (
+          open_vbox ();
+          open_hbox ();
+          str "ENewArrayValues";
+          space ();
+          str "(";
+          pp_t t;
+          close_box ();
+          comma ();
+          open_vbox_noindent ();
+          app (fn e => (pp_e e; comma ())) es;
+          str ")";
+          close_box ();
+          close_box ()
+        )
       | ELetIdx (i, branch) =>
         let
           val (name, e_body) = get_bind branch

micro-timl/micro-timl-ex.sml

@@ -1119,7 +1119,6 @@ fun default_expr_visitor_vtable
           | ENever data => #visit_ENever vtable this env data
           | EBuiltin data => #visit_EBuiltin vtable this env data
           | ELet data => #visit_ELet vtable this env data
-          | EEmptyArray t => EEmptyArray $ #visit_ty vtable this env t
           | ELetIdx data => #visit_ELetIdx vtable this env data
           | ELetType data => #visit_ELetType vtable this env data
           | ELetConstr data => #visit_ELetConstr vtable this env data
@@ -1133,6 +1132,8 @@ fun default_expr_visitor_vtable
           | EPairAssign data => #visit_EPairAssign vtable this env data
           | EProjProtected data => #visit_EProjProtected vtable this env data
           | EHalt data => #visit_EHalt vtable this env data
+          | EEmptyArray t => EEmptyArray $ #visit_ty vtable this env t
+          | ENewArrayValues (t, es) => ENewArrayValues (#visit_ty vtable this env t, visit_list (#visit_expr vtable this) env es)
       end
     fun visit_EVar this env data =
       let

micro-timl/micro-timl-pp.sml

@@ -215,6 +215,16 @@ fun pp_t (params as (str_var, str_b, str_i, str_s, str_k)) s depth t =
           str ")";
           close_box ()
         )
+      | TiBool i =>
+        (
+          open_hbox ();
+          str "TiBool";
+          space ();
+          str "(";
+          str $ str_i i;
+          str ")";
+          close_box ()
+        )
       | TArr (t, i) =>
         (
           open_hbox ();
@@ -227,6 +237,20 @@ fun pp_t (params as (str_var, str_b, str_i, str_s, str_k)) s depth t =
           str ")";
           close_box ()
         )
+      | TPreArray (t, i1, i2) =>
+        (
+          open_hbox ();
+          str "TArr";
+          space ();
+          str "(";
+          pp_t t;
+          comma ();
+          str $ str_i i1;
+          comma ();
+          str $ str_i i2;
+          str ")";
+          close_box ()
+        )
       | TAbsT bind =>
         let
           val (name, k, t) = get_bind_anno bind

micro-timl/micro-timl-typecheck.sml

@@ -308,13 +308,27 @@ fun kc (ctx as (ictx, tctx) : icontext * tcontext) t_input =
       in
         (TNat i, KType)
       end
+    | TiBool i =>
+      let
+        val i = sc_against_sort ictx (i, SBool)
+      in
+        (TiBool i, KType)
+      end
     | TArr (t, i) =>
       let
         val t = kc_against_kind ctx (t, KType)
         val i = sc_against_sort ictx (i, SNat)
       in
         (TArr (t, i), KType)
       end
+    | TPreArray (t, len, i) =>
+      let
+        val t = kc_against_kind ctx (t, KType)
+        val len = sc_against_sort ictx (len, SNat)
+        val i = sc_against_sort ictx (i, SNat)
+      in
+        (TPreArray (t, len, i), KType)
+      end
     | TProdEx ((t1, b1), (t2, b2)) =>
       let
         val t1 = kc_against_kind ctx (t1, KType)

micro-timl/micro-timl-visitor.sml

@@ -527,6 +527,8 @@ fun default_ty_visitor_vtable
           | TAppT data => #visit_TAppT vtable this env data
           | TProdEx data => #visit_TProdEx vtable this env data
           | TArrowTAL data => #visit_TArrowTAL vtable this env data
+          | TiBool idx => TiBool $ #visit_idx vtable this env idx
+          | TPreArray (t, i1, i2) => TPreArray (#visit_ty vtable this env t, #visit_idx vtable this env i1, #visit_idx vtable this env i2)
       end
     fun visit_TVar this env data =
       let

micro-timl/micro-timl-visitor2.sml

@@ -269,6 +269,16 @@ fun default_ty_visitor2_vtable
           | TAppT data => #visit2_TAppT vtable this env data other
           | TProdEx data => #visit2_TProdEx vtable this env data other
           | TArrowTAL data => #visit2_TArrowTAL vtable this env data other
+          | TiBool i =>
+            (case other of
+                 TiBool i' =>
+                 TiBool $ #visit2_idx vtable this env i i'
+               | _ => error (TiBool i) other)
+          | TPreArray (t, i1, i2) =>
+            (case other of
+                 TPreArray (t', i1', i2') =>
+                 TPreArray (#visit2_ty vtable this env t t', #visit2_idx vtable this env i1 i1', #visit2_idx vtable this env i2 i2')
+               | _ => error (TPreArray (t, i1, i2)) other)
       end
     fun visit2_TVar this env data other =
       let

micro-timl/micro-timl.sml

@@ -38,14 +38,14 @@ datatype ('var, 'bsort, 'idx, 'sort) ty =
          | TQuanI of unit Operators.quan * ('sort, ('var, 'bsort, 'idx, 'sort) ty) ibind_anno
          | TRec of ('bsort kind, ('var, 'bsort, 'idx, 'sort) ty) tbind_anno
          | TNat of 'idx
-         | TiBool of 'idx
          | TArr of ('var, 'bsort, 'idx, 'sort) ty * 'idx
          | TAbsT of ('bsort kind, ('var, 'bsort, 'idx, 'sort) ty) tbind_anno
          | TAppT of ('var, 'bsort, 'idx, 'sort) ty * ('var, 'bsort, 'idx, 'sort) ty
          (* used by compiler/pair-alloc *)
          | TProdEx of (('var, 'bsort, 'idx, 'sort) ty * bool) * (('var, 'bsort, 'idx, 'sort) ty * bool)
          (* used by compiler/code-gen *)
          | TArrowTAL of ('var, 'bsort, 'idx, 'sort) ty Rctx.map * 'idx
+         | TiBool of 'idx
          | TPreArray of ('var, 'bsort, 'idx, 'sort) ty * 'idx * 'idx
 
 type loc = int

micro-timl/to-evm1.sml

@@ -150,7 +150,7 @@ fun impl_prim_expr_un_opr opr =
 fun impl_prim_expr_bin_op opr =
   case opr of
        EBPIntAdd => [ADD]
-     | EBPIntMul => [MUL]
+     | EBPIntMult => [MUL]
      | EBPIntMinus => [SWAP1, SUB]
      | EBPIntDiv => [SWAP1, SDIV]
      | EBPIntLt => [SWAP1, LT]
@@ -167,10 +167,10 @@ fun impl_expr_un_op opr =
   case opr of
       EUPrim opr => impl_prim_expr_un_opr opr
     | EUNat2Int => [NAT2INT]
-    (* | EUPrint => [PRINT] *)
-    | EUPrintc => [PRINTC]
     | EUArrayLen => [PUSH1nat 32, SWAP1, SUB, MLOAD]
     | EUProj proj => [PUSH_tuple_offset $ 32 * choose (0, 1) proj, ADD, MLOAD]
+    (* | EUPrint => [PRINT] *)
+    | EUPrintc => [PRINTC]
 
 fun impl_nat_expr_bin_op opr =
   case opr of