diff --git a/generator/Makefile b/generator/Makefile index c30c0e606636ea0970a3d2f4b8b1b83955b89c00..f0a9e7fb3b69b5961b8278ded83c0b3ba239b6ca 100644 --- a/generator/Makefile +++ b/generator/Makefile @@ -33,7 +33,6 @@ ASSEMBLY_JS := \ LibOperation.log.js \ LibList.log.js \ Heap.log.js \ - String0.log.js \ Shared.log.js \ LibString.log.js \ LibOption.log.js \ diff --git a/generator/TODO b/generator/TODO index f76fe9c6dc4876dd88c8ea45d39654bf22a05346..62d067b3aacc8da032b16a5c9a601810a921f5c5 100644 --- a/generator/TODO +++ b/generator/TODO @@ -41,6 +41,9 @@ NEXT (ask Alan for Int32 and Int64 implementation tricks) - include JsNumber.js in assembly.js by modifying ASSEMBLY_JS in Makefile +- remove useless files such as LibReflect LibString etc... + +- in JsInterpreter let append = strappend (* hack for compatibility, to do cleanup *) [thomas, biggest piece, ask if anything problematic] - fill in the "esprima-to-ast.js" file, following the template diff --git a/generator/stdlib_ml/stdlib.mli b/generator/stdlib_ml/stdlib.mli index b5fa642b8fd97b7373f61de02a140a3cc5a36160..ada060d5d76a58c354c1ea60a681ee01aa78194b 100644 --- a/generator/stdlib_ml/stdlib.mli +++ b/generator/stdlib_ml/stdlib.mli @@ -144,10 +144,10 @@ val string_dec : string -> string -> bool (* let append s1 s2 = String.append s1 s2 *) -val append : string -> string -> string +val strappend : string -> string -> string -(* let length s = String.length s *) -val length : string -> int +(* let strlength s = String.length s *) +val strlength : string -> int (* let substring n m s = String.sub s n m *) val substring : int -> int -> string -> string diff --git a/generator/tests/jsref/JsInterpreter.ml b/generator/tests/jsref/JsInterpreter.ml index 2f8f9f407796076745794fe9a107b99f5537c86f..43764db59b5307af80b735c2677f9d304848be7d 100644 --- a/generator/tests/jsref/JsInterpreter.ml +++ b/generator/tests/jsref/JsInterpreter.ml @@ -19,6 +19,8 @@ open LibTactics open List0 open Shared (*open String0*) +let append x y = strappend x y (* hack for compatibility, to do cleanup *) +let length x = strlength x (* hack for compatibility, to do cleanup *) type __ = unit let __ = () @@ -1114,7 +1116,7 @@ let prim_new_object s _foo_ = match _foo_ with Heap.write p ("length") (Coq_attributes_data_of (attributes_data_intro_constant (Coq_value_prim - (Coq_prim_number (number_of_int (length s0)))))))) + (Coq_prim_number (number_of_int (strlength s0)))))))) (fun s' -> res_ter s' (res_val (Coq_value_object l)))))) (** val to_object : state -> value -> result **) @@ -2349,7 +2351,7 @@ let run_construct_prealloc runs0 s c b args = let (l, s2) = object_alloc s0 o in let_binding (attributes_data_intro_constant (Coq_value_prim - (Coq_prim_number (number_of_int (length s1))))) + (Coq_prim_number (number_of_int (strlength s1))))) (fun lenDesc -> if_some (object_heap_map_properties_pickable_option s2 l (fun p -> @@ -3084,7 +3086,7 @@ let run_object_get_own_prop runs0 s c l x = if_spec (to_int32 runs0 s4 c (Coq_value_prim (Coq_prim_string x))) (fun s5 k0 -> - let_binding (number_of_int (length str)) (fun len -> + let_binding (number_of_int (strlength str)) (fun len -> if le_int_decidable len k0 then res_spec s5 Coq_full_descriptor_undef else let resultStr = diff --git a/generator/tests/jsref/LibString.ml b/generator/tests/jsref/LibString.ml index 7e8433eca07a48ae658d272fc6b8fd07683138d6..da3ea98776a31e1ebe11da0c5faedc266c283940 100644 --- a/generator/tests/jsref/LibString.ml +++ b/generator/tests/jsref/LibString.ml @@ -1,5 +1,5 @@ open LibReflect -open String0 +(*open String0*) (** val string_comparable : string coq_Comparable **) diff --git a/generator/tests/jsref/String0.ml b/generator/tests/jsref/String0.ml deleted file mode 100644 index 354389e30f1c1ba1b459c555c95d16a293473b76..0000000000000000000000000000000000000000 --- a/generator/tests/jsref/String0.ml +++ /dev/null @@ -1,42 +0,0 @@ - - -(* - -(** val string_dec : string -> string -> bool **) - -let rec string_dec s1 s2 = match s1 with - | [] -> (match s2 with - | [] -> true - | a::s3 -> false) - | a::s0 -> (match s2 with - | [] -> false - | a0::s4 -> if (=) a a0 then string_dec s0 s4 else false) - -(** val append : string -> string -> string **) - -let rec append s1 s2 = - match s1 with - | [] -> s2 - | c::s1' -> c::(append s1' s2) - -(** val length : string -> int **) - -let rec length l = match l with -| [] -> 0 -| c::s' -> 1 + (length s') - -(** val substring : int -> int -> string -> string **) - -let rec substring n m s = - if n=0 then - if m=0 then - [] - else match s with - | [] -> s - | c::s' -> c::(substring 0 (m-1) s') - else match s with - | [] -> s - | c::s' -> substring (n-1) m s' - - -*) \ No newline at end of file