compiled to-evm1.sml

elaborate.sml

@@ -3,6 +3,7 @@ structure S = Ast
 structure E = NamefulExpr
 open S
 open E
+open Pervasive
 open Bind
 
 infixr 0 $
@@ -401,6 +402,7 @@ local
         | S.ETriOp (S.ETIte, e1, e2, e3, _) => ETriOp (ETIte, elab e1, elab e2, elab e3)
         | S.ETriOp (S.ETIfDec, e, e1, e2, r) => ECaseSumbool (elab e, IBind (("__p", r), elab e1), IBind (("__p", r), elab e2), r)
         | S.ENever r => ENever (elab_mt (S.VarT (NONE, ("_", r))), r)
+        | S.EStrConcat (e1, e2, r) => EApp (EVar (QID $ qid_add_r r $ STR_CONCAT_NAMEFUL, false), EPair (elab e1, elab e2))
 
   and elab_decl decl =
       case decl of

examples/code-gen-test1.pkg

@@ -1,39 +1,39 @@
-(* unit-test-basic.timl *)
+(* (* unit-test-basic.timl *) *)
 
-(* basic.timl *)
-(* list.timl *)
+(* (* basic.timl *) *)
+(* (* list.timl *) *)
 
-stdlib.pkg
+(* stdlib.pkg *)
 
-(* unit-test-bool.timl *)
-(* unit-test-array.timl *)
-(* unit-test-list.timl *)
+(* (* unit-test-bool.timl *) *)
+(* (* unit-test-array.timl *) *)
+(* (* unit-test-list.timl *) *)
 
-(* perversive-list.timl *)
-(* trivial.timl *)
-(* bigO-evolve.timl *)
-(* fold-evolve.timl *)
-(* single-var.timl *)
-(* bug.timl *)
-(* pldi-2017-review-example.timl *)
-(* braun-tree-sortedness.timl *)
-(* rbt-sortedness.timl *)
+(* (* perversive-list.timl *) *)
+(* (* trivial.timl *) *)
+(* (* bigO-evolve.timl *) *)
+(* (* fold-evolve.timl *) *)
+(* (* single-var.timl *) *)
+(* (* bug.timl *) *)
+(* (* pldi-2017-review-example.timl *) *)
+(* (* braun-tree-sortedness.timl *) *)
+(* (* rbt-sortedness.timl *) *)
 
-(* ragged-matrix.timl *)
-(* tree.timl *)
-(* msort.timl *)
-(* insertion-sort.timl *)
-(* braun-tree.timl *)
-(* rbt.timl *)
-(* functional-queue.timl *)
-(* array-bsearch.timl *)
-(* array-heap.timl *)
-(* array-msort.timl *)
-(* array-msort-inplace.timl *)
-(* array-kmed.timl *)
-(* dlist.timl *)
-(* qsort.timl *)
-(* dijkstra.timl *)
+(* (* ragged-matrix.timl *) *)
+(* (* tree.timl *) *)
+(* (* msort.timl *) *)
+(* (* insertion-sort.timl *) *)
+(* (* braun-tree.timl *) *)
+(* (* rbt.timl *) *)
+(* (* functional-queue.timl *) *)
+(* (* array-bsearch.timl *) *)
+(* (* array-heap.timl *) *)
+(* (* array-msort.timl *) *)
+(* (* array-msort-inplace.timl *) *)
+(* (* array-kmed.timl *) *)
+(* (* dlist.timl *) *)
+(* (* qsort.timl *) *)
+(* (* dijkstra.timl *) *)
 
-(* dynamic-table.timl *)
-(* dynamic-table-test.timl *)
+(* (* dynamic-table.timl *) *)
+(* (* dynamic-table-test.timl *) *)

examples/pervasive.timl

@@ -1,5 +1,6 @@
 structure Pervasive = struct
 
-datatype some_nat = SomeNat {n : Nat} of nat {n}
+(* assuming 256-bit integers *)
+datatype some_nat = SomeNat {n : Nat | n < 2 ** 256} of nat {n}
 
 end

examples/rbt.timl

@@ -4,7 +4,7 @@
 
 structure LogFacts = struct
 datatype lemma1 {a b : Nat} =
-         Lemma1 {2 ^^ a <= b + 1 -> a <= ceil (log2 $(b + 1))} of lemma1 {a} {b}
+         Lemma1 {2 ** a <= b + 1 -> a <= ceil (log2 $(b + 1))} of lemma1 {a} {b}
 
 fun lemma1 {a b : Nat} () return lemma1 {a} {b} =
     @Lemma1 {a} {b} {admit} (* assume this fact as axiom *)
@@ -40,12 +40,12 @@ datatype rbt 'a : {Nat(*size*)} {Bool} {Nat(*black-height*)} =
               {lsize rsize bh : Nat}
               {color = false -> lcolor = true /\ rcolor = true }
               (* We have to add the following two extra invariants. These two invariants can be derived from the other invariants, but because in TiML lemmas, lemma invocations, and inductions must be written as ordinary functions (like in Dafny) which increase a program's running time, deriving these invariants on the fly will increase asymptotic complexity. *)
-              {2 ^^ (bh + b2n (not lcolor) + 1) <= 2 * (lsize + 1) /\ 2 * (lsize + 1) <= 2 ^^ (2 * bh + b2n (not lcolor) + 1)}
-              {2 ^^ (bh + b2n (not rcolor) + 1) <= 2 * (rsize + 1) /\ 2 * (rsize + 1) <= 2 ^^ (2 * bh + b2n (not rcolor) + 1)}
+              {2 ** (bh + b2n (not lcolor) + 1) <= 2 * (lsize + 1) /\ 2 * (lsize + 1) <= 2 ** (2 * bh + b2n (not lcolor) + 1)}
+              {2 ** (bh + b2n (not rcolor) + 1) <= 2 * (rsize + 1) /\ 2 * (rsize + 1) <= 2 ** (2 * bh + b2n (not rcolor) + 1)}
          of color {color} * rbt 'a {lsize} {lcolor} {bh} * (key * 'a) * rbt 'a {rsize} {rcolor} {bh} --> rbt 'a {lsize + 1 + rsize} {color} {bh + b2n color}
 
 datatype size_good {color : Bool} {size bh : Nat} =
-         SizeGood {2 ^^ (bh + b2n (not color) + 1) <= 2 * (size + 1) /\ 2 * (size + 1) <= 2 ^^ (2 * bh + b2n (not color) + 1)}
+         SizeGood {2 ** (bh + b2n (not color) + 1) <= 2 * (size + 1) /\ 2 * (size + 1) <= 2 ** (2 * bh + b2n (not color) + 1)}
          of size_good {color} {size} {bh}
 
 fun rbt_size_good ['a] {color : Bool} {size bh : Nat} (tr : rbt 'a {size} {color} {bh}) return size_good {color} {size} {bh} =

examples/string.timl

@@ -7,7 +7,7 @@ open Array
 
 datatype string = String {len : Nat} of array byte {len}
 
-new_string "abc" == String (new_array {'a', 'b', 'c'})
+(* new_string "abc" == String (new_array {'a', 'b', 'c'}) *)
 
 fun size s =
   let

examples/to-evm1-test.pkg

@@ -1,9 +1,11 @@
+string.timl
+
 (* unit-test-basic.timl *)
 
 (* basic.timl *)
 (* list.timl *)
 
-stdlib.pkg
+(* stdlib.pkg *)
 
 (* unit-test-bool.timl *)
 (* unit-test-array.timl *)

expr-visitor.sml

@@ -148,6 +148,7 @@ fun default_expr_visitor_vtable
           | EEI data => #visit_EEI vtable this env data
           | EET data => #visit_EET vtable this env data
           | ET data => #visit_ET vtable this env data
+          | ENewArrayValues (t, es, r) => T.ENewArrayValues (#visit_mtype vtable this env t, visit_list (#visit_expr vtable this) env es, r)
 	  | EAbs data => #visit_EAbs vtable this env data
 	  | EAbsI data => #visit_EAbsI vtable this env data
 	  | EAppConstr data => #visit_EAppConstr vtable this env data

generate-file-list.rb

@@ -150,6 +150,7 @@ def wrong_arguments
 uniquefy.sml
 expr.sml
 underscore-exprs.sml
+pervasive.sml
 elaborate.sml
 name-resolve.sml
 package.sml
@@ -198,6 +199,7 @@ def wrong_arguments
 merge-modules.sml
 micro-timl/export-pp.sml
 micro-timl/timl-to-micro-timl.sml
+micro-timl/micro-timl-ex-util-timl.sml
 micro-timl/micro-timl-typecheck.sml
 micro-timl/micro-timl-ex-locally-nameless.sml
 micro-timl/compiler-util.sml

micro-timl/code-gen.sml

@@ -86,6 +86,7 @@ fun cg_c c =
     | ECNat n => WCNat n
     | ECInt n => WCInt n
     | ECBool n => WCBool n
+    | ECByte c => WCByte c
     (* | ECString s => raise Impossible $ "cg_c() on ECString" *)
 
 fun cg_v ectx v =
@@ -116,9 +117,11 @@ fun cg_v ectx v =
 fun cg_expr_un_op opr =
   case opr of
       EUPrim opr => IUPrim opr
-    | EUPrint => IUPrint
     | EUArrayLen => IUArrayLen
     | EUNat2Int => IUNat2Int
+    | EUInt2Nat => IUInt2Nat
+    | EUPrintc => IUPrintc
+    (* | EUPrint => IUPrint *)
     | EUProj _ => raise Impossible "cg_expr_un_op() on EUProj"
 
 fun VAppITs_ctx (e, itctx) =

micro-timl/compiler-util.sml

@@ -1,6 +1,7 @@
 structure CompilerUtil = struct
 
 open MicroTiMLExLocallyNameless
+open MicroTiMLExUtilTiML
 open MicroTiMLExUtil
 
 infixr 0 $
@@ -59,6 +60,10 @@ fun assert_TUnit msg t =
   case t of
       TConst TCUnit => ()
     | _ => raise assert_fail msg
+fun assert_TInt t =
+  case t of
+      TConst TCInt => ()
+    | _ => raise assert_fail "assert_TInt"
 fun assert_TProdEx t =
   case t of
       TProdEx a => a

micro-timl/evm1.sml

@@ -13,6 +13,7 @@ datatype word_const =
          | WCNat of nat
          | WCInt of int
          | WCBool of bool
+         | WCByte of Char.char
          | WCiBool of bool
          | WCLabel of label
 
@@ -47,6 +48,7 @@ datatype ('idx, 'ty) inst =
          | ISZERO
          | AND
          | OR
+         | BYTE
          (* | SHA3 *)
          | POP
          | MLOAD
@@ -67,8 +69,11 @@ datatype ('idx, 'ty) inst =
          | VALUE_Fold of 'ty inner
          | VALUE_AscType of 'ty inner
          | UNPACK of tbinder
+         | UNPACKI of ibinder
          | UNFOLD
          | NAT2INT
+         | INT2NAT
+         | BYTE2INT
          | PRINTC
          | PACK_SUM of injector * 'ty
          | ASCTIME of 'idx inner

micro-timl/micro-timl-ex-util-timl.sml

@@ -0,0 +1,69 @@
+(* Utilities for MicroTiMLEx specialized to Expr *)
+
+structure MicroTiMLExUtilTiML = struct
+
+open Expr
+open MicroTiMLExLongId
+open MicroTiMLExUtil
+
+infixr 0 $
+
+infix 9 %@
+infix 8 %^
+infix 7 %*
+infix 6 %+ 
+infix 4 %<=
+infix 4 %<
+infix 4 %>=
+infix 4 %>
+infix 4 %=
+infixr 3 /\
+infixr 2 \/
+infixr 1 -->
+infix 1 <->
+
+infix 8 %**
+fun a %** b = ExpI (a, b)
+
+val unTAbsT = unBindAnnoName
+
+fun whnf ctx t =
+    case t of
+        TAppT (t1, t2) =>
+        let
+          val t1 = whnf ctx t1
+        in
+          case t1 of
+              TAbsT data =>
+              let
+                val (_, (_, t1)) = unTAbsT data
+              in
+                whnf ctx $ subst0_t_t t2 t1
+              end
+            | _ => TAppT (t1, t2)
+        end
+      | TAppI (t, i) =>
+        let
+          val t = whnf ctx t
+        in
+          case t of
+              TAbsI data =>
+              let
+                val (_, (_, t)) = unTAbsT data
+              in
+                whnf ctx $ subst0_i_t i t
+              end
+            | _ => TAppI (t, i)
+        end
+      | TVar x => TVar x (* todo: look up type aliasing in ctx *)
+      | _ => t
+
+fun MakeSubset (name, s, p) = Subset ((s, dummy), Bind.Bind ((name, dummy), p), dummy)
+local
+  fun IV n = VarI (ID (n, dummy), [])
+in
+fun TSomeNat_packed () = TExistsI $ IBindAnno ((("n", dummy), MakeSubset ("n", BSNat, IV 0 %< ConstIN (2, dummy) %** ("256", dummy))), TNat $ IV 0)
+fun TSomeNat () = TRec $ TBindAnno ((("some_nat", dummy), KType), TSomeNat_packed ())
+end
+
+end

micro-timl/micro-timl-ex-util.sml

@@ -180,41 +180,6 @@ fun collect_TAbsIT b =
       end
     | _ => ([], b)
 
-open MicroTiMLExLongId
-
-val unTAbsT = unBindAnnoName
-
-fun whnf ctx t =
-    case t of
-        TAppT (t1, t2) =>
-        let
-          val t1 = whnf ctx t1
-        in
-          case t1 of
-              TAbsT data =>
-              let
-                val (_, (_, t1)) = unTAbsT data
-              in
-                whnf ctx $ subst0_t_t t2 t1
-              end
-            | _ => TAppT (t1, t2)
-        end
-      | TAppI (t, i) =>
-        let
-          val t = whnf ctx t
-        in
-          case t of
-              TAbsI data =>
-              let
-                val (_, (_, t)) = unTAbsT data
-              in
-                whnf ctx $ subst0_i_t i t
-              end
-            | _ => TAppI (t, i)
-        end
-      | TVar x => TVar x (* todo: look up type aliasing in ctx *)
-      | _ => t
-
 fun eq_t a = MicroTiMLVisitor2.eq_t_fn (curry Equal.eq_var, Equal.eq_bs, Equal.eq_i, Equal.eq_s) a
 
 fun collect_ELet e =