From fa4ee9c5b089578ff91bc46c2f222d1fdc78d5fc Mon Sep 17 00:00:00 2001
From: charguer <arthur@chargueraud.org>
Date: Thu, 3 Mar 2016 18:50:59 +0100
Subject: [PATCH] cleanup
---
generator/Makefile | 1 -
generator/TODO | 3 ++
generator/stdlib_ml/stdlib.mli | 6 ++--
generator/tests/jsref/JsInterpreter.ml | 8 +++--
generator/tests/jsref/LibString.ml | 2 +-
generator/tests/jsref/String0.ml | 42 --------------------------
6 files changed, 12 insertions(+), 50 deletions(-)
delete mode 100644 generator/tests/jsref/String0.ml
diff --git a/generator/Makefile b/generator/Makefile
index c30c0e6..f0a9e7f 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 f76fe9c..62d067b 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 b5fa642..ada060d 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 2f8f9f4..43764db 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 7e8433e..da3ea98 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 354389e..0000000
--- 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
--
GitLab