cleanup

generator/Makefile

@@ -20,40 +20,46 @@ TESTS_ML    := $(wildcard $(TESTS_DIR)/*.ml)
 JSREF_ML    := $(wildcard $(TESTS_DIR)/$(JSREF_DIR)/*.ml) 
 JSREF_MLI   := $(wildcard $(TESTS_DIR)/$(JSREF_DIR)/*.mli)
 
+###############################################################
+
 # ASSEMBLY_JS must respect dependencies order
-ASSEMBLY_JS := \
-	Ascii.log.js \
-	BinNums.log.js \
-	Bool0.log.js \
-	Datatypes.log.js \
-	Fappli_IEEE_bits.log.js \
-	Fappli_IEEE.log.js \
-	LibBool.log.js \
-	LibReflect.log.js \
-	LibOperation.log.js \
-	LibList.log.js \
-	Heap.log.js \
-	Shared.log.js \
-	LibString.log.js \
-	LibOption.log.js \
+ASSEMBLY_JS_FILES := \
+	BinNums.unlog.js \
+	Bool0.unlog.js \
+	List0.unlog.js \
+	Datatypes.unlog.js \
+	Fappli_IEEE_bits.unlog.js \
+	Fappli_IEEE.unlog.js \
+	LibBool.unlog.js \
+	LibReflect.unlog.js \
+	LibOperation.unlog.js \
+	LibList.unlog.js \
+	LibString.unlog.js \
+	LibOption.unlog.js \
+	LibTactics.unlog.js \
+	LibProd.unlog.js \
+	LibFunc.unlog.js \
+	Heap.unlog.js \
+	Shared.unlog.js \
 	JsNumber.js \
-	JsSyntax.log.js \
-	JsSyntaxAux.log.js \
+	JsSyntax.unlog.js \
+	JsSyntaxAux.unlog.js \
 	Translate_syntax.js \
-	List0.log.js \
-	JsSyntaxInfos.log.js \
-	JsCommon.log.js \
-	JsCommonAux.log.js \
+	JsSyntaxInfos.unlog.js \
+	JsCommon.unlog.js \
+	JsCommonAux.unlog.js \
 	JsPreliminary.log.js \
-	JsInit.log.js \
-	Prheap.js \
-	LibTactics.log.js \
-	LibProd.log.js \
-	LibFunc.log.js \
-	JsInterpreterMonads.log.js \
-	JsInterpreter.log.js \
-	Specif.log.js
-ASSEMBLY_JS := $(STDLIB_DIR)/stdlib.js $(addprefix tests/jsref/,$(ASSEMBLY_JS));
+	JsInit.unlog.js \
+	JsInterpreterMonads.unlog.js \
+	JsInterpreter.log.js
+ASSEMBLY_JS := $(STDLIB_DIR)/stdlib.js $(addprefix tests/jsref/,$(ASSEMBLY_JS_FILES));
+
+
+###############################################################
+
+# --> todo arthur include src files
+#	JsPreliminary.log.js \
+#	JsInterpreter.log.js
 
 
 ###############################################################

generator/TODO

-ARTHUR
 
-- remove "open JsNumber" to more easily trace occurences
 
-- generate "type: " in smart constructors [optional until display is needed]
 
-- generate the escaped source code
 
-- control which file should feature logging 
 
+NEW TODO
 
+- parse pickage in JsCommon needed for eval
 
-=========================================================
-NEXT
+- optimize ML code for 
+      type_compare mutability_compare prim_compare 
+  and test for prim_compare if we can match on pairs of arguments, with a catchall
+
+- move prim_compare and value_compare to a higher file because it is interesting and should be logged
+- move same_value_dec from jscommonaux to a higher file
 
-[arthur did a first pass on JsNumber.ml to make explicit paths
- and on stdlib.ml]
-- continue cleaning up stdlib.ml
-- implement stdlib.js
-	- remove unused functions
-	- sort out remaining ones
-	- need to have one function for each one of stdlib.ml
-	- replace JsNumber by a corresponding JsNumber.mli
-	  (keep JsNumber saved somewhere else for future use)
-	- implement JsNumber.js by hand to match signature of JsNumber.mli,
-	  by implementing number related functions using JS counterpart directly
-     (ask Alan for Int32 and Int64 implementation tricks)
-	- include JsNumber.js in assembly.js by modifying ASSEMBLY_JS in Makefile
+- generate the escaped source code
+
+- LATER: inline the "%able" functions
 
-- remove useless files such as LibReflect LibString etc...
+- LATER: remove useless files such as LibReflect LibString etc...
 
-- in JsInterpreter let append = strappend (* hack for compatibility, to do cleanup *)
 
-[alan or thomas]
-- figure out what to do for Parser_syntax Parser_main
+- BONUS  -- generate "type: " in smart constructors [optional until display is needed]
+
+
+=========================================================
 
 
-[our goal is to build trace for]
 - Introduce testing functions called:
 	- test_exec("code") -> parse, convert, build trace, log trace
 - Test first "var x = 3".
@@ -50,13 +41,16 @@ NEXT
   for each example, check the AST, check step-by-step the execution.
   => to see if the right things get highlighted
 
-[second biggest, only once we manage to build the trace]
 - display JS values/env/heap/ctx in html 
 	- contexts: essentially as before
 	- environments: need to follow the list of environment records
 	- heap: same as before, and do not attempt at first to show
 	  additional information in the heap appart from key/value bindings.
 
+- BONUS in JsInterpreter let append = strappend (* hack for compatibility, to do cleanup *)
+
+
+
 
 =========================================================
 LATER

generator/stdlib_ml/stdlib.mli

@@ -176,16 +176,6 @@ val (!) : 'a ref -> 'a
 val ( === ) : 'a -> 'a -> bool
 
 
-
-
-(*--------------------*)
-
-(* no longer needed it seems 
-module Pervasives : sig
-  val succ : int -> int
-end
-*)
-
 (*--------------------*)
 (* todo: remove when JsNumber.ml becomes .mli file *)
 
@@ -204,32 +194,6 @@ module Int32 : sig
 end
 
 
-
-
-(*--------------------*)
-
-(* 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
-  type bin_op
-  type exp
-end
-
-module Parser_main : sig 
-  val exp_from_string : ?force_strict:bool -> string -> Parser_syntax.exp
-end 
-
-(* ARTHUR: not needed -- tocheck
-   module Parser : sig
-     exception ParserFailure of string
-     exception InvalidArgument
-   end
-
-*)
-
-
 (*--------------------*)
 (* JSRef specific functions, useful for debugging *)
 
@@ -243,32 +207,3 @@ val prerr_endline : string -> unit
 val raise : exn -> 'a
 val stuck : string -> '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
-
-*)

generator/tests/jsref/JsCommon.ml

@@ -584,7 +584,7 @@ let elision_tail_remove ol =
 let parse_pickable = (fun s strict ->
     let str = s in
     (* try  ARTHUR HACK *)
-      let parserExp = Parser_main.exp_from_string ~force_strict:strict str in
+      let parserExp = Translate_syntax.Parser_main.exp_from_string ~force_strict:strict str in
       Some (JsSyntaxInfos.add_infos_prog strict
         (Translate_syntax.exp_to_prog parserExp))
     (* with

generator/tests/jsref/Specif.ml

-type 'a coq_sig =
-  'a
-  (* singleton inductive, whose constructor was exist *)
-

generator/tests/jsref/Translate_syntax.mli

 
-  exception CoqSyntaxDoesNotSupport of string
-  exception Empty_list
+module Parser_syntax : sig (* needed by translate_syntax.mli and by parser_main (below) *)
+  type unary_op
+  type arith_op
+  type bin_op
+  type exp
+end
+
+module Parser_main : sig 
+  val exp_from_string : ?force_strict:bool -> string -> Parser_syntax.exp
+end 
+
+
+
+exception CoqSyntaxDoesNotSupport of string
+exception Empty_list
 
-  val string_to_coq : string -> char list
+val string_to_coq : string -> char list
 
-  val unary_op_to_coq : Parser_syntax.unary_op -> JsSyntax.unary_op
-  val arith_op_to_coq : Parser_syntax.arith_op -> JsSyntax.binary_op
-  val bin_op_to_coq : Parser_syntax.bin_op -> JsSyntax.binary_op
+val unary_op_to_coq : Parser_syntax.unary_op -> JsSyntax.unary_op
+val arith_op_to_coq : Parser_syntax.arith_op -> JsSyntax.binary_op
+val bin_op_to_coq : Parser_syntax.bin_op -> JsSyntax.binary_op
 
-  val exp_to_literal : Parser_syntax.exp -> JsSyntax.literal
+val exp_to_literal : Parser_syntax.exp -> JsSyntax.literal
 
-  val exp_to_exp : Parser_syntax.exp -> JsSyntax.expr
-  val exp_to_stat : Parser_syntax.exp -> JsSyntax.stat
-  val exp_to_prog : Parser_syntax.exp -> JsSyntax.prog
-  val exp_to_elem : Parser_syntax.exp -> JsSyntax.element
-  val exp_to_funcbody :
-    Parser_syntax.exp -> JsSyntax.strictness_flag -> JsSyntax.funcbody
+val exp_to_exp : Parser_syntax.exp -> JsSyntax.expr
+val exp_to_stat : Parser_syntax.exp -> JsSyntax.stat
+val exp_to_prog : Parser_syntax.exp -> JsSyntax.prog
+val exp_to_elem : Parser_syntax.exp -> JsSyntax.element
+val exp_to_funcbody :
+ Parser_syntax.exp -> JsSyntax.strictness_flag -> JsSyntax.funcbody
 
-  val coq_syntax_from_file : ?init:bool -> string -> JsSyntax.prog
-  val coq_syntax_from_string : string -> JsSyntax.prog
-  val coq_syntax_from_main : string -> JsSyntax.prog
+val coq_syntax_from_file : ?init:bool -> string -> JsSyntax.prog
+val coq_syntax_from_string : string -> JsSyntax.prog
+val coq_syntax_from_main : string -> JsSyntax.prog
 
 (*
 module Translate_syntax : sig (* ARTHUR: to implement *)