diff --git a/generator/stdlib_ml/stdlib.mli b/generator/stdlib_ml/stdlib.mli index 6e287407c762d95cfc09dba4a6cd254906173f31..b5fa642b8fd97b7373f61de02a140a3cc5a36160 100644 --- a/generator/stdlib_ml/stdlib.mli +++ b/generator/stdlib_ml/stdlib.mli @@ -135,36 +135,29 @@ module Int32 : sig val to_float : int32 -> float end -(* should not be needed if we do'nt use JsNumber.ml *) -module Int64 : sig - val one : int64 - val float_of_bits : int64 -> float -end -module List : sig (* should rely on List0 instead *) - val map : ('a -> 'b) -> 'a list -> 'b list - val rev : 'a list -> 'a list -end +(*--------------------*) +(* string operations *) -module String : sig (* should rely on String0 instead *) - val length : string -> int - val append : string -> string -> string - val sub : string -> int -> int -> string - val concat : string -> string list -> string - val iter : (char -> unit) -> string -> unit - val make : int -> char -> string - val get : string -> int -> char -end +(* let string_dec s1 s2 = (string_eq s1 s2) *) +val string_dec : string -> string -> bool -(* Coq outputs exceptions in the place of arbitrary *) -val raise : exn -> 'a -(* JSRef specific functions *) -val prerr_string : string -> unit -val prerr_newline : unit -> unit -val prerr_endline : string -> unit +(* let append s1 s2 = String.append s1 s2 *) +val append : string -> string -> string + +(* let length s = String.length s *) +val length : string -> int + +(* let substring n m s = String.sub s n m *) +val substring : int -> int -> string -> string + +(*--------------------*) + +(* figure out how to deal with parser *) + module Parser_syntax : sig (* needed by translate_syntax.mli and by parser_main (below) *) type unary_op type arith_op @@ -176,20 +169,53 @@ module Parser_main : sig val exp_from_string : ?force_strict:bool -> string -> Parser_syntax.exp end -(* ARTHUR: not needed -module Parser : sig - exception ParserFailure of string - exception InvalidArgument -end +(* ARTHUR: not needed -- tocheck + module Parser : sig + exception ParserFailure of string + exception InvalidArgument + end *) -module Obj : sig (* should not be needed *) - type t -end - -(* only used for debug*) +(*--------------------*) +(* JSRef specific functions, useful for debugging *) val print_endline : string -> unit val __LOC__ : string + +val prerr_string : string -> unit +val prerr_newline : unit -> unit +val prerr_endline : string -> unit + +val raise : exn -> 'a + + + + +(*--------------------*) +(* deprecated *) + +(* should not be needed if we don't use JsNumber.ml *) +(* +module Int64 : sig + val one : int64 + val float_of_bits : int64 -> float +end + +module List : sig (* should rely on List0 instead *) + val map : ('a -> 'b) -> 'a list -> 'b list + val rev : 'a list -> 'a list +end + +module String : sig (* should rely on String0 instead *) + val length : string -> int + val append : string -> string -> string + val sub : string -> int -> int -> string + val concat : string -> string list -> string + val iter : (char -> unit) -> string -> unit + val make : int -> char -> string + val get : string -> int -> char +end + +*) diff --git a/generator/tests/jsref/JsInterpreter.ml b/generator/tests/jsref/JsInterpreter.ml index 672ee7de36d59c1faf7045f88260be590f76f5ea..2f8f9f407796076745794fe9a107b99f5537c86f 100644 --- a/generator/tests/jsref/JsInterpreter.ml +++ b/generator/tests/jsref/JsInterpreter.ml @@ -18,7 +18,7 @@ open LibString open LibTactics open List0 open Shared -open String0 +(*open String0*) type __ = unit let __ = () diff --git a/generator/tests/jsref/JsSyntaxInfos.ml b/generator/tests/jsref/JsSyntaxInfos.ml index b6c9031c06c3a62820d1254d942c6f602be54201..d85f2d84c20ea2bd2f4269906e0667abf941e21a 100644 --- a/generator/tests/jsref/JsSyntaxInfos.ml +++ b/generator/tests/jsref/JsSyntaxInfos.ml @@ -3,9 +3,6 @@ open JsSyntaxAux open LibBool open List0 -(* -let __ = let rec f _ = Obj.repr f in Obj.repr f -*) (** val add_infos_exp : strictness_flag -> expr -> expr **) diff --git a/generator/tests/jsref/Shared.ml b/generator/tests/jsref/Shared.ml index 164ce319557754461beef0d80c828bc4838d2ac1..9c4adb4481ed9763734f8116555bf59f2d49aeb5 100644 --- a/generator/tests/jsref/Shared.ml +++ b/generator/tests/jsref/Shared.ml @@ -1,7 +1,7 @@ open Datatypes open Heap open LibReflect -open String0 +(*open String0*) diff --git a/generator/tests/jsref/String0.ml b/generator/tests/jsref/String0.ml index ad269fb174ddc83d7bf7bb35bd733f50d477b774..354389e30f1c1ba1b459c555c95d16a293473b76 100644 --- a/generator/tests/jsref/String0.ml +++ b/generator/tests/jsref/String0.ml @@ -1,13 +1,4 @@ -(* ARTHUR: hacked this file *) - -let string_dec s1 s2 = (string_eq s1 s2) - -let append s1 s2 = String.append s1 s2 - -let length s = String.length s - -let substring n m s = String.sub s n m (*