typechecking string.timl

elaborate.sml

@@ -350,8 +350,10 @@ local
                       String.implode $ rev $ loop (ls, [])
                     end
                   val s = unescape s
+                  val e = ENewArrayValues (BaseType (Byte, r), map (fn c => EByte (c, r)) $ String.explode s, r)
+                  val e = EApp (EVar (QID $ qid_add_r r $ CSTR_STRING_NAMEFUL, false), e)
                 in
-                  ENewArrayValues (BaseType (Byte, r), map (fn c => EByte (c, r)) $ String.explode s, r)
+                  e
                 end)
 	| S.BinOp (EBApp, e1, e2, r) =>
 	  let 
@@ -366,6 +368,9 @@ local
 		     else if x = "__&not" then EUnOp (EUPrim EUPBoolNeg, elab e2, r)
 		     (* else if x = "__&int2str" then EUnOp (EUInt2Str, elab e2, r) *)
 		     else if x = "__&nat2int" then EUnOp (EUNat2Int, elab e2, r)
+		     else if x = "__&int2nat" then EUnOp (EUInt2Nat, elab e2, r)
+		     else if x = "__&byte2int" then EUnOp (EUPrim EUPByte2Int, elab e2, r)
+		     else if x = "__&int2byte" then EUnOp (EUPrim EUPInt2Byte, elab e2, r)
 		     else if x = "__&array_length" then EUnOp (EUArrayLen, elab e2, r)
 		     (* else if x = "__&print" then EUnOp (EUPrint, elab e2, r) *)
 		     else if x = "__&printc" then EUnOp (EUPrintc, elab e2, r)

examples/array.timl

@@ -7,7 +7,7 @@ open Nat
 open List
 
 fun empty_array ['a] () return array 'a {0} = __&empty_array
-fun array {n : Nat} (a : nat {n}, b) = __&array (a, b)
+fun array ['a] {n : Nat} (len : nat {n}, v : 'a) = __&array (len, v)
 fun length {len : Nat} (a : array _ {len}) = __&array_length a
 
 fun sub ['a] {len who : Nat} {who < len} (a : array 'a {len}, n : nat {who}) return 'a using 0.0 =

examples/basic.timl

@@ -2,17 +2,20 @@
 
 structure Basic = struct
 
+open Pervasive
+
 fun fst a = __&fst a
 fun snd a = __&snd a
 fun not a = __&not a
 val true = __&true
 val false = __&false
-fun int2str a = __&int2str a
-fun print a = __&print a
+fun nat2int {n : Nat} (a : nat {n}) = __&nat2int a
+fun int2nat a = __&int2nat a
+fun int2byte a = __&int2byte a
+fun byte2int a = __&byte2int a
+(* fun int2str a = __&int2str a *)
+(* fun print a = __&print a *)
 
-val str_int = int2str
-fun println s = print s; print "\n"
-
 (* a datatype version of boolean that is suitable for pattern-matching *)
 datatype Bool = True | False
 

examples/code-gen-test1.pkg

@@ -1,39 +1,43 @@
-(* (* unit-test-basic.timl *) *)
+pervasive.timl
+nat.timl
+string.timl
+
+unit-test-basic.timl
 
-(* (* basic.timl *) *)
-(* (* list.timl *) *)
+(* basic.timl *)
+(* list.timl *)
 
 (* 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/nat.timl

@@ -83,4 +83,14 @@ fun ceil_half {n : Nat} (n : nat {n}) return nat {ceil ($n / 2)} =
 datatype nat_less_than {m : Nat} =
          NatLT {n : Nat} {n < m} of nat {n} --> nat_less_than {m}
 
+fun for ['a] {m : Time} {start : Nat} {eend : Nat | start <= eend} (start : nat {start}, eend : nat {eend}, init : 'a, f : forall {i : Nat | start <= i /\ i < eend}, nat {i} * 'a -- m --> 'a) return 'a using 1.0 + (m + 3.0) * $(eend - start) =
+  let
+    fun loop {i : Nat | start <= i /\ i <= eend} (i : nat {i}, acc : 'a) (* return using (m + 3.0) * $(eend - i) *) =
+      ifdec i #>= eend then acc
+      else
+        loop (i #+ #1, f (i, acc)) using (m + 3.0) * $(eend - i)
+  in
+    loop (start, init)
+  end
+
 end

examples/pervasive.timl

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

examples/stdlib.pkg

@@ -4,3 +4,4 @@ basic.timl
 nat.timl
 list.timl
 array.timl
+string.timl

examples/string.timl

@@ -2,58 +2,60 @@ structure String = struct
 
 (* fun int2str a = __&int2str a *)
 (* fun print a = __&print a *)
+fun printc a = __&printc a
 
 open Array
 
-datatype string = String {len : Nat} of array byte {len}
+datatype string = String {len : Nat} of array byte {len} --> string
 
 (* new_string "abc" == String (new_array {'a', 'b', 'c'}) *)
 
 fun size s =
   let
     val String arr = s
   in
-    nat2int $ length arr
+    nat2int <| length arr
   end
 
 fun concat (s1, s2) =
   let
-    val String arr1 = s1
-    val String arr2 = s2
-    val len1 = length s1
-    val len2 = length s2
+    val @String {len1} arr1 = s1
+    val @String {len2} arr2 = s2
+    val len1 = length arr1
+    val len2 = length arr2
     val len = len1 #+ len2
-    val arr = array (len, 0)
-    for i = #0 to len1 do
-      update (arr, i, sub(arr1, i))
-    end
-    for i = #0 to len2 do
-      update (arr, len1 #+ i, sub(arr2, i))
-    end
+    val arr = array (len, int2byte 0)
+    val () = for (#0, len1, (), fn {i : Nat | i < len1} (i : nat {i}, _) =>
+      update (arr, i, sub (arr1, i)))
+    val () = for (#0, len2, (), fn {i : Nat | i < len2} (i : nat {i}, _) =>
+      update (arr, len1 #+ i, sub (arr2, i)))
   in 
     String arr
-end
+  end
 
 fun print s =
   let
-    val String arr = s
-    val len = length s
-    for i = #0 to len do
-      printc $ sub(arr, i)
-    end
+    val @String {len} arr = s
+    val len = length arr
+    val () = for (#0, len, (), fn {i : Nat | i < len} (i : nat {i}, _) =>
+      printc <| sub (arr, i))
   in
     ()
 end
 
-fun nat2bytes {d : Nat} {i : Nat | 10 ** d <= i < 10 ** (d+1) \/ i = 0 /\ d = 0} (i : nat {i}) return list byte {d+1} using d =
+fun nat2byte i = int2byte <| nat2int i
+
+fun nat2bytes {d : Nat} {i : Nat | 10 ** d <= i /\ i < 10 ** (d+1) \/ i = 0 /\ d = 0} (i : nat {i}) return list byte {d+1} using $d =
   ifdec i #< #10 then [nat2byte i]
-  else int2byte (nat2int i mod 10) :: @nat2bytes {d-1} {_} (i #/ 10)
+  else int2byte (nat2int i mod 10) :: (@nat2bytes {d-1} {_} (i #/ #10)) (* todo: need to fix precedence here *)
 
-fun int2str i return using 20 =
+fun int2str i return using 20.0 =
   let
-    val Nat n = int2nat i
+    val SomeNat n = int2nat i
   in
-    String (fromList $ rev $ nat2bytes n)
+    String (fromList <| rev <| nat2bytes n)
   end
 
+val str_int = int2str
+
 end

examples/to-evm1-test.pkg

@@ -1,41 +1,42 @@
-string.timl
+(* pervasive.timl *)
+(* string.timl *)
 
-(* 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/unit-test-basic.timl

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

micro-timl/evm1.sml

@@ -40,6 +40,7 @@ datatype ('idx, 'ty) inst =
          | SUB
          | DIV
          | SDIV
+         | MOD
          | LT
          | GT
          | SLT

micro-timl/micro-timl-typecheck.sml

@@ -600,6 +600,7 @@ fun get_prim_expr_bin_op_arg1_ty opr =
     | EBPIntMult => TInt
     | EBPIntMinus => TInt
     | EBPIntDiv => TInt
+    | EBPIntMod => TInt
     | EBPIntLt => TInt
     | EBPIntGt => TInt
     | EBPIntLe => TInt
@@ -616,6 +617,7 @@ fun get_prim_expr_bin_op_arg2_ty opr =
     | EBPIntMult => TInt
     | EBPIntMinus => TInt
     | EBPIntDiv => TInt
+    | EBPIntMod => TInt
     | EBPIntLt => TInt
     | EBPIntGt => TInt
     | EBPIntLe => TInt
@@ -632,6 +634,7 @@ fun get_prim_expr_bin_op_res_ty opr =
     | EBPIntMult => TInt
     | EBPIntMinus => TInt
     | EBPIntDiv => TInt
+    | EBPIntMod => TInt
     | EBPIntLt => TBool
     | EBPIntGt => TBool
     | EBPIntLe => TBool

micro-timl/tital-eval.sml

@@ -237,6 +237,7 @@ fun interp_prim_expr_bin_op opr (a, b) =
     | EBPIntMult => WVInt $ assert_WVInt a * assert_WVInt b
     | EBPIntMinus => WVInt $ assert_WVInt a - assert_WVInt b
     | EBPIntDiv => WVInt $ assert_WVInt a div assert_WVInt b
+    | EBPIntMod => WVInt $ assert_WVInt a mod assert_WVInt b
     | EBPIntLt => WVBool $ assert_WVInt a < assert_WVInt b
     | EBPIntGt => WVBool $ assert_WVInt a > assert_WVInt b
     | EBPIntLe => WVBool $ assert_WVInt a <= assert_WVInt b

micro-timl/to-evm1.sml

@@ -159,6 +159,7 @@ fun impl_prim_expr_bin_op opr =
      | EBPIntMult => [MUL]
      | EBPIntMinus => [SWAP1, SUB]
      | EBPIntDiv => [SWAP1, SDIV]
+     | EBPIntMod => [SWAP1, MOD]
      | EBPIntLt => [SWAP1, LT]
      | EBPIntGt => [SWAP1, GT]
      | EBPIntLe => [GT, ISZERO]