From 92837f25cf07bde67e745c5f6a7029c86047b204 Mon Sep 17 00:00:00 2001 From: Peng Wang Date: Tue, 10 Apr 2018 17:23:58 -0400 Subject: [PATCH] typechecking string.timl --- elaborate.sml | 7 ++- examples/array.timl | 2 +- examples/basic.timl | 13 +++--- examples/code-gen-test1.pkg | 68 +++++++++++++++------------- examples/nat.timl | 10 +++++ examples/pervasive.timl | 2 +- examples/stdlib.pkg | 1 + examples/string.timl | 50 +++++++++++---------- examples/to-evm1-test.pkg | 69 +++++++++++++++-------------- examples/unit-test-basic.timl | 1 - micro-timl/evm1.sml | 1 + micro-timl/micro-timl-typecheck.sml | 3 ++ micro-timl/tital-eval.sml | 1 + micro-timl/to-evm1.sml | 1 + operators.sml | 3 ++ parser/timl.grm | 2 + parser/timl.lex | 1 + pervasive.sml | 1 + sortcheck.sml | 2 +- typecheck-main.sml | 3 ++ unit-test.sml | 2 +- 21 files changed, 142 insertions(+), 101 deletions(-) diff --git a/elaborate.sml b/elaborate.sml index 20dca49c..332c74d4 100644 --- a/elaborate.sml +++ b/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 = "__¬" 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) diff --git a/examples/array.timl b/examples/array.timl index 46325429..b395a43a 100644 --- a/examples/array.timl +++ b/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 = diff --git a/examples/basic.timl b/examples/basic.timl index 66ccf536..4ae1e3a7 100644 --- a/examples/basic.timl +++ b/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 = __¬ 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 diff --git a/examples/code-gen-test1.pkg b/examples/code-gen-test1.pkg index de756e48..c19c7792 100644 --- a/examples/code-gen-test1.pkg +++ b/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 *) diff --git a/examples/nat.timl b/examples/nat.timl index f1654a1b..ef54b9d5 100644 --- a/examples/nat.timl +++ b/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 diff --git a/examples/pervasive.timl b/examples/pervasive.timl index 669ff214..c80bb31f 100644 --- a/examples/pervasive.timl +++ b/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 diff --git a/examples/stdlib.pkg b/examples/stdlib.pkg index 47b89ca9..7da45a8a 100644 --- a/examples/stdlib.pkg +++ b/examples/stdlib.pkg @@ -4,3 +4,4 @@ basic.timl nat.timl list.timl array.timl +string.timl diff --git a/examples/string.timl b/examples/string.timl index 20cafd97..e19593bb 100644 --- a/examples/string.timl +++ b/examples/string.timl @@ -2,10 +2,11 @@ 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'}) *) @@ -13,47 +14,48 @@ 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 diff --git a/examples/to-evm1-test.pkg b/examples/to-evm1-test.pkg index 192606c1..fac8906f 100644 --- a/examples/to-evm1-test.pkg +++ b/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 *) *) diff --git a/examples/unit-test-basic.timl b/examples/unit-test-basic.timl index 6c6fe543..c9933fa8 100644 --- a/examples/unit-test-basic.timl +++ b/examples/unit-test-basic.timl @@ -5,7 +5,6 @@ fun snd a = __&snd a fun not a = __¬ 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" diff --git a/micro-timl/evm1.sml b/micro-timl/evm1.sml index 1441441e..26e533fd 100644 --- a/micro-timl/evm1.sml +++ b/micro-timl/evm1.sml @@ -40,6 +40,7 @@ datatype ('idx, 'ty) inst = | SUB | DIV | SDIV + | MOD | LT | GT | SLT diff --git a/micro-timl/micro-timl-typecheck.sml b/micro-timl/micro-timl-typecheck.sml index b3f02629..7ba281b8 100644 --- a/micro-timl/micro-timl-typecheck.sml +++ b/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 diff --git a/micro-timl/tital-eval.sml b/micro-timl/tital-eval.sml index 013a3ab5..aea318c5 100644 --- a/micro-timl/tital-eval.sml +++ b/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 diff --git a/micro-timl/to-evm1.sml b/micro-timl/to-evm1.sml index 386e3003..51f708af 100644 --- a/micro-timl/to-evm1.sml +++ 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] diff --git a/operators.sml b/operators.sml index 5d226b02..c4bdb451 100644 --- a/operators.sml +++ b/operators.sml @@ -126,6 +126,7 @@ datatype prim_expr_bin_op = | EBPIntMinus | EBPIntMult | EBPIntDiv + | EBPIntMod | EBPIntLt | EBPIntGt | EBPIntLe @@ -166,6 +167,7 @@ fun str_prim_expr_bin_op opr = | EBPIntMult => "mult" | EBPIntMinus => "minus" | EBPIntDiv => "div" + | EBPIntMod => "mod" | EBPIntLt => "lt" | EBPIntGt => "gt" | EBPIntLe => "le" @@ -208,6 +210,7 @@ fun pretty_str_prim_expr_bin_op opr = | EBPIntMult => "*" | EBPIntMinus => "-" | EBPIntDiv => "/" + | EBPIntMod => "mod" | EBPIntLt => "<" | EBPIntGt => ">" | EBPIntLe => "<=" diff --git a/parser/timl.grm b/parser/timl.grm index 471dca63..40e7b4de 100644 --- a/parser/timl.grm +++ b/parser/timl.grm @@ -96,6 +96,7 @@ open Ast | SEMI_COLON | NEVER | IFDEC + | MOD %nonterm start of prog | exp of exp @@ -269,6 +270,7 @@ exp : aexp (aexp) | exp MINUS exp (BinOp (EBPrim EBPIntMinus, exp1, exp2, (exp1left, exp2right))) | exp MULT exp (BinOp (EBPrim EBPIntMult, exp1, exp2, (exp1left, exp2right))) | exp DIV exp (BinOp (EBPrim EBPIntDiv, exp1, exp2, (exp1left, exp2right))) + | exp MOD exp (BinOp (EBPrim EBPIntMod, exp1, exp2, (exp1left, exp2right))) | exp LT exp (BinOp (EBPrim EBPIntLt, exp1, exp2, (exp1left, exp2right))) | exp GT exp (BinOp (EBPrim EBPIntGt, exp1, exp2, (exp1left, exp2right))) | exp LE exp (BinOp (EBPrim EBPIntLe, exp1, exp2, (exp1left, exp2right))) diff --git a/parser/timl.lex b/parser/timl.lex index bcd16d3b..ab15efc7 100644 --- a/parser/timl.lex +++ b/parser/timl.lex @@ -77,6 +77,7 @@ val keywords = [ ("else", T.ELSE), ("never", T.NEVER), ("ifdec", T.IFDEC), + ("mod", T.MOD), ("as", T.AS) ] diff --git a/pervasive.sml b/pervasive.sml index e3d0688c..ac361643 100644 --- a/pervasive.sml +++ b/pervasive.sml @@ -2,6 +2,7 @@ structure Pervasive = struct val SOME_NAT_ID = ("Pervasive", 0) +val CSTR_STRING_NAMEFUL = ("String", "String") val STR_CONCAT_NAMEFUL = ("String", "concat") fun qid_add_r r (name, x) = ((name, r), (x, r)) diff --git a/sortcheck.sml b/sortcheck.sml index 93db8cf8..7792ada0 100644 --- a/sortcheck.sml +++ b/sortcheck.sml @@ -273,7 +273,7 @@ and get_bsort gctx (ctx, i) = end | IUExp n => let - val i = check_bsort (ctx, i, Base Time) + val i = check_bsort (ctx, i, Base Time(* todo: bug. This is not enforced in rbt.timl *)) in (ExpI (i, (n, r)), Base Time) end diff --git a/typecheck-main.sml b/typecheck-main.sml index facfa701..56a4956f 100644 --- a/typecheck-main.sml +++ b/typecheck-main.sml @@ -939,6 +939,7 @@ fun get_prim_expr_bin_op_arg1_ty opr = | EBPIntMult => Int | EBPIntMinus => Int | EBPIntDiv => Int + | EBPIntMod => Int | EBPIntLt => Int | EBPIntGt => Int | EBPIntLe => Int @@ -955,6 +956,7 @@ fun get_prim_expr_bin_op_arg2_ty opr = | EBPIntMult => Int | EBPIntMinus => Int | EBPIntDiv => Int + | EBPIntMod => Int | EBPIntLt => Int | EBPIntGt => Int | EBPIntLe => Int @@ -971,6 +973,7 @@ fun get_prim_expr_bin_op_res_ty opr = | EBPIntMult => Int | EBPIntMinus => Int | EBPIntDiv => Int + | EBPIntMod => Int | EBPIntLt => Bool | EBPIntGt => Bool | EBPIntLe => Bool diff --git a/unit-test.sml b/unit-test.sml index 3e1d42c9..876460fa 100644 --- a/unit-test.sml +++ b/unit-test.sml @@ -10,7 +10,7 @@ val test_suites = test_suites @ MicroTiMLTypecheck.UnitTest.test_suites val test_suites = test_suites @ CPS.UnitTest.test_suites val test_suites = test_suites @ CC.UnitTest.test_suites val test_suites = test_suites @ PairAlloc.UnitTest.test_suites -(* val test_suites = test_suites @ CodeGen.UnitTest.test_suites *) +val test_suites = test_suites @ CodeGen.UnitTest.test_suites val test_suites = test_suites @ ToEVM1.UnitTest.test_suites end