From 14510c80fa9d105ab61f0ecfb96ea89f7edf6587 Mon Sep 17 00:00:00 2001 From: Jon French Date: Mon, 23 Apr 2018 16:04:37 +0100 Subject: start of string pattern matching: currently only literals --- test/ocaml/prelude.sail | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'test') diff --git a/test/ocaml/prelude.sail b/test/ocaml/prelude.sail index 83178aea..1960e56a 100644 --- a/test/ocaml/prelude.sail +++ b/test/ocaml/prelude.sail @@ -15,6 +15,9 @@ val eq_int = "eq_int" : (int, int) -> bool val eq_vec = "eq_list" : forall 'n. (bits('n), bits('n)) -> bool val eq_string = "eq_string" : (string, string) -> bool +val string_startswith = "string_startswith" : (string, string) -> bool +val string_drop = "string_drop" : (string, nat) -> string +val string_length = "string_length" : string -> nat val eq_real = "eq_real" : (real, real) -> bool @@ -303,4 +306,4 @@ val pow2 = "pow2" : forall 'n. atom('n) -> atom(2 ^ 'n) val "print_int" : (string, int) -> unit -val "print_bits" : forall 'n. (string, bits('n)) -> unit \ No newline at end of file +val "print_bits" : forall 'n. (string, bits('n)) -> unit -- cgit v1.2.3 From fca88463c50ec7d27dc2670972f13a6015905f64 Mon Sep 17 00:00:00 2001 From: Jon French Date: Mon, 23 Apr 2018 17:10:55 +0100 Subject: starting to also do integer support --- test/ocaml/prelude.sail | 2 ++ 1 file changed, 2 insertions(+) (limited to 'test') diff --git a/test/ocaml/prelude.sail b/test/ocaml/prelude.sail index 1960e56a..f055a9b6 100644 --- a/test/ocaml/prelude.sail +++ b/test/ocaml/prelude.sail @@ -152,6 +152,8 @@ and cast_unit_vec bitzero = 0b0 val print = "print_endline" : string -> unit +val string_of_int = "string_of_int" : int -> string + val putchar = "putchar" : forall ('a : Type). 'a -> unit val concat_str = "concat_str" : (string, string) -> string -- cgit v1.2.3 From b94549367c2536b3df6fba8586efa1a2a4bca7b8 Mon Sep 17 00:00:00 2001 From: Jon French Date: Fri, 27 Apr 2018 13:19:24 +0100 Subject: further progress --- test/ocaml/prelude.sail | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'test') diff --git a/test/ocaml/prelude.sail b/test/ocaml/prelude.sail index f055a9b6..a9004297 100644 --- a/test/ocaml/prelude.sail +++ b/test/ocaml/prelude.sail @@ -4,6 +4,9 @@ type bits ('n : Int) = vector('n, dec, bit) infix 4 == +val int : int <-> string +overload int = string_of_int + val eq_atom = "eq_int" : forall 'n 'm. (atom('n), atom('m)) -> bool val lteq_atom = "lteq" : forall 'n 'm. (atom('n), atom('m)) -> bool val gteq_atom = "gteq" : forall 'n 'm. (atom('n), atom('m)) -> bool @@ -18,6 +21,7 @@ val eq_string = "eq_string" : (string, string) -> bool val string_startswith = "string_startswith" : (string, string) -> bool val string_drop = "string_drop" : (string, nat) -> string val string_length = "string_length" : string -> nat +val string_append = "string_append" : (string, string) -> string val eq_real = "eq_real" : (real, real) -> bool -- cgit v1.2.3 From f8abc90f5e7ae8e25f2750a186eee2ef30021cf5 Mon Sep 17 00:00:00 2001 From: Jon French Date: Mon, 30 Apr 2018 15:18:56 +0100 Subject: further progress but confounds the type checker? --- test/ocaml/prelude.sail | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'test') diff --git a/test/ocaml/prelude.sail b/test/ocaml/prelude.sail index a9004297..54c88cb8 100644 --- a/test/ocaml/prelude.sail +++ b/test/ocaml/prelude.sail @@ -17,11 +17,15 @@ val eq_int = "eq_int" : (int, int) -> bool val eq_vec = "eq_list" : forall 'n. (bits('n), bits('n)) -> bool +union option ('a : Type) = {None : unit, Some : 'a} + val eq_string = "eq_string" : (string, string) -> bool val string_startswith = "string_startswith" : (string, string) -> bool val string_drop = "string_drop" : (string, nat) -> string val string_length = "string_length" : string -> nat val string_append = "string_append" : (string, string) -> string +val maybe_int_of_prefix = "maybe_int_of_prefix" : string -> option((int, nat)) +val maybe_nat_of_prefix = "maybe_nat_of_prefix" : string -> option((nat, nat)) val eq_real = "eq_real" : (real, real) -> bool -- cgit v1.2.3 From 66047739ae2c5b4e84084930754d78bc21927b8e Mon Sep 17 00:00:00 2001 From: Jon French Date: Tue, 1 May 2018 10:35:07 +0100 Subject: rewriting of builtin mappings e.g. int --- test/ocaml/prelude.sail | 1 + 1 file changed, 1 insertion(+) (limited to 'test') diff --git a/test/ocaml/prelude.sail b/test/ocaml/prelude.sail index 54c88cb8..6cbabed7 100644 --- a/test/ocaml/prelude.sail +++ b/test/ocaml/prelude.sail @@ -26,6 +26,7 @@ val string_length = "string_length" : string -> nat val string_append = "string_append" : (string, string) -> string val maybe_int_of_prefix = "maybe_int_of_prefix" : string -> option((int, nat)) val maybe_nat_of_prefix = "maybe_nat_of_prefix" : string -> option((nat, nat)) +val maybe_int_of_string = "maybe_int_of_string" : string -> option(int) val eq_real = "eq_real" : (real, real) -> bool -- cgit v1.2.3 From 54d4716c42bf3c8f35d0537385bceb09c3b348b1 Mon Sep 17 00:00:00 2001 From: Jon French Date: Tue, 8 May 2018 17:16:09 +0100 Subject: fixed sub-mappings --- test/ocaml/prelude.sail | 2 ++ 1 file changed, 2 insertions(+) (limited to 'test') diff --git a/test/ocaml/prelude.sail b/test/ocaml/prelude.sail index 6cbabed7..5b046104 100644 --- a/test/ocaml/prelude.sail +++ b/test/ocaml/prelude.sail @@ -199,6 +199,8 @@ val sub_range = "sub_int" : forall 'n 'm 'o 'p. val sub_int = "sub_int" : (int, int) -> int +val sub_nat = "sub_int" : (nat, nat) -> nat + val sub_vec : forall 'n. (bits('n), bits('n)) -> bits('n) val sub_vec_int = "sub_vec_int" : forall 'n. (bits('n), int) -> bits('n) -- cgit v1.2.3 From b499927e42e60dba6c33c5e445696f5b9daf8c75 Mon Sep 17 00:00:00 2001 From: Jon French Date: Mon, 11 Jun 2018 12:18:13 +0100 Subject: ocaml test prelude: option is now in stdlib --- test/ocaml/prelude.sail | 2 -- 1 file changed, 2 deletions(-) (limited to 'test') diff --git a/test/ocaml/prelude.sail b/test/ocaml/prelude.sail index c2c5133f..e9295cea 100644 --- a/test/ocaml/prelude.sail +++ b/test/ocaml/prelude.sail @@ -2,8 +2,6 @@ default Order dec $include -union option ('a : Type) = {None : unit, Some : 'a} - val eq_string = "eq_string" : (string, string) -> bool val string_startswith = "string_startswith" : (string, string) -> bool val string_drop = "string_drop" : (string, nat) -> string -- cgit v1.2.3 From 4ddc0093cb9a833d0e92ed62541a14c5bb652367 Mon Sep 17 00:00:00 2001 From: Jon French Date: Mon, 11 Jun 2018 16:22:04 +0100 Subject: fix test exist_pattern.sail -- lem needed much more of the stdlib to be imported --- test/typecheck/pass/exist_pattern.sail | 12 +----------- 1 file changed, 1 insertion(+), 11 deletions(-) (limited to 'test') diff --git a/test/typecheck/pass/exist_pattern.sail b/test/typecheck/pass/exist_pattern.sail index 96b1ecf1..c701f12b 100644 --- a/test/typecheck/pass/exist_pattern.sail +++ b/test/typecheck/pass/exist_pattern.sail @@ -1,6 +1,6 @@ default Order inc -infix 4 == +$include register n : nat @@ -8,16 +8,6 @@ register x : nat register y : nat -val eq_int = {lem: "eq", coq: "Z.eqb"} : (int, int) -> bool -val eq_vec = {lem: "eq_vec", coq: "eq_vec"} : forall ('n : Int). (vector('n, inc, bit), vector('n, inc, bit)) -> bool - -overload operator == = {eq_int, eq_vec} - -val and_bool = {coq: "andb", _: "and_bool"} : (bool, bool) -> bool - -val vector_subrange = {ocaml: "subrange", lem: "subrange_vec_inc", coq: "subrange_vec_inc"} : forall ('n : Int) ('m : Int) ('o : Int), 'm <= 'o <= 'n. - (vector('n, inc, bit), atom('m), atom('o)) -> vector('o - ('m - 1), inc, bit) - type wordsize = {'n, 'n in {8, 16, 32}. range(0, 'n)} let word : wordsize = 8 : range(0, 8) -- cgit v1.2.3 From 22aff19aeea53719004cca2b5c6b25d0a7ed0835 Mon Sep 17 00:00:00 2001 From: Jon French Date: Mon, 11 Jun 2018 16:28:07 +0100 Subject: actually fix exist_pattern test --- test/typecheck/pass/exist_pattern.sail | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'test') diff --git a/test/typecheck/pass/exist_pattern.sail b/test/typecheck/pass/exist_pattern.sail index c701f12b..ac41114f 100644 --- a/test/typecheck/pass/exist_pattern.sail +++ b/test/typecheck/pass/exist_pattern.sail @@ -1,4 +1,4 @@ -default Order inc +default Order dec $include @@ -36,7 +36,7 @@ function main () = { 32 => x = 128 }; match 0b010101 { - 0b01 @ _ : vector(1, inc, bit) @ 0b101 => n = 42, + 0b01 @ _ : vector(1, dec, bit) @ 0b101 => n = 42, _ => n = 0 }; n = 3; -- cgit v1.2.3