From 7231d5affc5ffc445bfdbe07732bc5abc20f4e5f Mon Sep 17 00:00:00 2001
From: charguer <arthur@chargueraud.org>
Date: Mon, 29 Feb 2016 18:15:42 +0100
Subject: [PATCH] label_jssyntax

---
 generator/Makefile                | 12 ++--
 generator/tests/jsref/Heap.ml     | 70 +++++++++++++++++++++++
 generator/tests/jsref/JsSyntax.ml | 88 ++++++++++++++---------------
 generator/tests/jsref/LibHeap.ml  | 93 -------------------------------
 generator/tests/jsref/Shared.ml   | 48 +---------------
 5 files changed, 122 insertions(+), 189 deletions(-)
 create mode 100644 generator/tests/jsref/Heap.ml
 delete mode 100644 generator/tests/jsref/LibHeap.ml

diff --git a/generator/Makefile b/generator/Makefile
index 212ed53..52cc3ed 100644
--- a/generator/Makefile
+++ b/generator/Makefile
@@ -111,12 +111,7 @@ tests/jsref: tests/jsref/JsInterpreter.log.js
 tests/jsrefunlog: tests/jsref/JsInterpreter.unlog.js
 
 
-arthur: $(ML_JSREF:.ml=.log.js) $(ML_JSREF:.ml=.unlog.js) $(ML_JSREF:.ml=.token.js)
 
-# foo:
-# 	make $(ML_JSREF:.ml=.log.js)
-# 
-# tests/jsref/JsInterpreter.log.js
 
 
 ######### lineof target #########
@@ -124,8 +119,15 @@ arthur: $(ML_JSREF:.ml=.log.js) $(ML_JSREF:.ml=.unlog.js) $(ML_JSREF:.ml=.token.
 tests/jsref/lineof.js: lineof.byte $(ML_JSREF:.ml=.token.js)
 	lineof.byte -o $@ $(ML_JSREF:.ml=.token.js)
 
+
+######### short targets #########
+
+unlog: $(ML_JSREF:.ml=.unlog.js) 
+full: $(ML_JSREF:.ml=.log.js) $(ML_JSREF:.ml=.unlog.js) $(ML_JSREF:.ml=.token.js)
 lineof: tests/jsref/lineof.js
 
+
+
 ##################
 
 
diff --git a/generator/tests/jsref/Heap.ml b/generator/tests/jsref/Heap.ml
new file mode 100644
index 0000000..ee057d4
--- /dev/null
+++ b/generator/tests/jsref/Heap.ml
@@ -0,0 +1,70 @@
+open Datatypes
+open LibBool
+open LibList
+open LibReflect
+
+
+type ('k, 'v) heap = ('k * 'v) list
+
+(** val empty : ('a1, 'a2) heap **)
+
+let empty =
+ []
+
+(** val to_list : ('a1, 'a2) heap -> ('a1, 'a2) heap **)
+
+let to_list l =
+ l
+
+(** val assoc : 'a1 coq_Comparable -> 'a1 -> ('a1 * 'a2) list -> 'a2 **)
+
+let rec assoc h1 k l = match l with
+| [] -> raise Not_found
+| p :: l' -> let (x, v) = p in if h1 x k then v else assoc h1 k l'
+
+(** val read : 'a1 coq_Comparable -> ('a1, 'a2) heap -> 'a1 -> 'a2 **)
+
+let read h l k =
+ assoc h k l
+
+(** val write : ('a1, 'a2) heap -> 'a1 -> 'a2 -> ('a1 * 'a2) list **)
+
+let write l k v =
+ (k, v) :: l
+
+(** val rem :
+   'a1 coq_Comparable -> ('a1, 'a2) heap -> 'a1 -> ('a1 * 'a2) list **)
+
+let rem h1 l k =
+ filter (fun p -> if h1 (fst p) k then false else true) l
+
+(** val read_option :
+   'a1 coq_Comparable -> ('a1, 'a2) heap -> 'a1 -> 'a2 option **)
+
+let read_option h =
+ let rec read_option0 l k =
+   match l with
+   | [] -> None
+   | p :: l' ->
+     let (x, v) = p in if h x k then Some v else read_option0 l' k
+ in read_option0
+
+(** val mem_assoc :
+   'a2 coq_Comparable -> 'a2 -> ('a2 * 'a1) list -> bool **)
+
+let rec mem_assoc h1 k l = match l with
+| [] -> false
+| p :: l' -> let (x, y) = p in coq_or (h1 x k) (mem_assoc h1 k l')
+
+(** val indom_dec :
+   'a1 coq_Comparable -> ('a1, 'a2) heap -> 'a1 -> bool **)
+
+let indom_dec h1 h k =
+ mem_assoc h1 k h
+
+(** val indom_decidable :
+   'a1 coq_Comparable -> ('a1, 'a2) heap -> 'a1 -> coq_Decidable **)
+
+let indom_decidable h h0 k =
+ indom_dec h h0 k
+
diff --git a/generator/tests/jsref/JsSyntax.ml b/generator/tests/jsref/JsSyntax.ml
index 6901d6c..ba7a38d 100644
--- a/generator/tests/jsref/JsSyntax.ml
+++ b/generator/tests/jsref/JsSyntax.ml
@@ -1,10 +1,8 @@
 open JsNumber
-open LibHeap
+open Heap
 open LibReflect
 open Shared
 
-module Heap = HeapGen(HeapList)
-
 type unary_op =
 | Coq_unary_op_delete [@f]  (** Auto Generated Attributes **)
 | Coq_unary_op_void [@f]  (** Auto Generated Attributes **)
@@ -70,55 +68,55 @@ type propname =
 
 type expr =
 | Coq_expr_this [@f]  (** Auto Generated Attributes **)
-| Coq_expr_identifier  [@f label0] of string (** Auto Generated Attributes **)
-| Coq_expr_literal  [@f label0] of literal (** Auto Generated Attributes **)
-| Coq_expr_object  [@f label0] of (propname * propbody) list (** Auto Generated Attributes **)
-| Coq_expr_array  [@f label0] of expr option list (** Auto Generated Attributes **)
-| Coq_expr_function  [@f label0, label1, label2] of string option * string list * funcbody (** Auto Generated Attributes **)
-| Coq_expr_access  [@f label0, label1] of expr * expr (** Auto Generated Attributes **)
-| Coq_expr_member  [@f label0, label1] of expr * string (** Auto Generated Attributes **)
-| Coq_expr_new  [@f label0, label1] of expr * expr list (** Auto Generated Attributes **)
-| Coq_expr_call  [@f label0, label1] of expr * expr list (** Auto Generated Attributes **)
-| Coq_expr_unary_op  [@f label0, label1] of unary_op * expr (** Auto Generated Attributes **)
-| Coq_expr_binary_op  [@f label0, label1, label2] of expr * binary_op * expr (** Auto Generated Attributes **)
-| Coq_expr_conditional  [@f label0, label1, label2] of expr * expr * expr (** Auto Generated Attributes **)
-| Coq_expr_assign  [@f label0, label1, label2] of expr * binary_op option * expr (** Auto Generated Attributes **)
+| Coq_expr_identifier  [@f name] of string (** Auto Generated Attributes **)
+| Coq_expr_literal  [@f value] of literal (** Auto Generated Attributes **)
+| Coq_expr_object  [@f fields] of (propname * propbody) list (** Auto Generated Attributes **)
+| Coq_expr_array  [@f elements] of expr option list (** Auto Generated Attributes **)
+| Coq_expr_function  [@f func_name_opt, arg_names, body] of string option * string list * funcbody (** Auto Generated Attributes **)
+| Coq_expr_access  [@f obj, field] of expr * expr (** Auto Generated Attributes **)
+| Coq_expr_member  [@f obj, field_name] of expr * string (** Auto Generated Attributes **)
+| Coq_expr_new  [@f func, args] of expr * expr list (** Auto Generated Attributes **)
+| Coq_expr_call  [@f func, args] of expr * expr list (** Auto Generated Attributes **)
+| Coq_expr_unary_op  [@f op, arg] of unary_op * expr (** Auto Generated Attributes **)
+| Coq_expr_binary_op  [@f arg1, op, arg2] of expr * binary_op * expr (** Auto Generated Attributes **)
+| Coq_expr_conditional  [@f cond, then_branch, else_branch] of expr * expr * expr (** Auto Generated Attributes **)
+| Coq_expr_assign  [@f left_expr, op_opt, right_expr] of expr * binary_op option * expr (** Auto Generated Attributes **)
 and propbody =
-| Coq_propbody_val  [@f label0] of expr (** Auto Generated Attributes **)
-| Coq_propbody_get  [@f label0] of funcbody (** Auto Generated Attributes **)
-| Coq_propbody_set  [@f label0, label1] of string list * funcbody (** Auto Generated Attributes **)
+| Coq_propbody_val  [@f expr] of expr (** Auto Generated Attributes **)
+| Coq_propbody_get  [@f body] of funcbody (** Auto Generated Attributes **)
+| Coq_propbody_set  [@f names, body] of string list * funcbody (** Auto Generated Attributes **)
 and funcbody =
-| Coq_funcbody_intro  [@f label0, label1] of prog * string (** Auto Generated Attributes **)
+| Coq_funcbody_intro  [@f prog, source] of prog * string (** Auto Generated Attributes **)
 and stat =
-| Coq_stat_expr  [@f label0] of expr (** Auto Generated Attributes **)
-| Coq_stat_label  [@f label0, label1] of string * stat (** Auto Generated Attributes **)
-| Coq_stat_block  [@f label0] of stat list (** Auto Generated Attributes **)
-| Coq_stat_var_decl  [@f label0] of (string * expr option) list (** Auto Generated Attributes **)
-| Coq_stat_if  [@f label0, label1, label2] of expr * stat * stat option (** Auto Generated Attributes **)
-| Coq_stat_do_while  [@f label0, label1, label2] of label_set * stat * expr (** Auto Generated Attributes **)
-| Coq_stat_while  [@f label0, label1, label2] of label_set * expr * stat (** Auto Generated Attributes **)
-| Coq_stat_with  [@f label0, label1] of expr * stat (** Auto Generated Attributes **)
-| Coq_stat_throw  [@f label0] of expr (** Auto Generated Attributes **)
-| Coq_stat_return  [@f label0] of expr option (** Auto Generated Attributes **)
-| Coq_stat_break  [@f label0] of label (** Auto Generated Attributes **)
-| Coq_stat_continue  [@f label0] of label (** Auto Generated Attributes **)
-| Coq_stat_try  [@f label0, label1, label2] of stat * (string * stat) option * stat option (** Auto Generated Attributes **)
-| Coq_stat_for  [@f label0, label1, label2, label3, label4] of label_set * expr option * expr option * expr option * stat (** Auto Generated Attributes **)
-| Coq_stat_for_var  [@f label0, label1, label2, label3, label4] of label_set * (string * expr option) list * expr option * expr option * stat (** Auto Generated Attributes **)
-| Coq_stat_for_in  [@f label0, label1, label2, label3] of label_set * expr * expr * stat (** Auto Generated Attributes **)
-| Coq_stat_for_in_var  [@f label0, label1, label2, label3, label4] of label_set * string * expr option * expr * stat (** Auto Generated Attributes **)
+| Coq_stat_expr  [@f expr] of expr (** Auto Generated Attributes **)
+| Coq_stat_label  [@f label, stat] of string * stat (** Auto Generated Attributes **)
+| Coq_stat_block  [@f stats] of stat list (** Auto Generated Attributes **)
+| Coq_stat_var_decl  [@f decls] of (string * expr option) list (** Auto Generated Attributes **)
+| Coq_stat_if  [@f cond, then_branch, else_branch] of expr * stat * stat option (** Auto Generated Attributes **)
+| Coq_stat_do_while  [@f labels, body, cond] of label_set * stat * expr (** Auto Generated Attributes **)
+| Coq_stat_while  [@f labels, cond, body] of label_set * expr * stat (** Auto Generated Attributes **)
+| Coq_stat_with  [@f obj, stat] of expr * stat (** Auto Generated Attributes **)
+| Coq_stat_throw  [@f arg] of expr (** Auto Generated Attributes **)
+| Coq_stat_return  [@f arg_opt] of expr option (** Auto Generated Attributes **)
+| Coq_stat_break  [@f label] of label (** Auto Generated Attributes **)
+| Coq_stat_continue  [@f label] of label (** Auto Generated Attributes **)
+| Coq_stat_try  [@f body, catch_stats_opt, finally_opt] of stat * (string * stat) option * stat option (** Auto Generated Attributes **)
+| Coq_stat_for  [@f labels, TODO_opt1, TODO_opt2, TODO_opt3, body] of label_set * expr option * expr option * expr option * stat (** Auto Generated Attributes **)
+| Coq_stat_for_var  [@f labels, TODO_list1, TODO_opt2, TODO_opt3, body] of label_set * (string * expr option) list * expr option * expr option * stat (** Auto Generated Attributes **)
+| Coq_stat_for_in  [@f labels, TODO_exp1, TODO_exp2, body] of label_set * expr * expr * stat (** Auto Generated Attributes **)
+| Coq_stat_for_in_var  [@f labels, TODO_str1, TODO_exp2, TODO_exp3, body] of label_set * string * expr option * expr * stat (** Auto Generated Attributes **)
 | Coq_stat_debugger [@f]  (** Auto Generated Attributes **)
-| Coq_stat_switch  [@f label0, label1, label2] of label_set * expr * switchbody (** Auto Generated Attributes **)
+| Coq_stat_switch  [@f labels, arg, body] of label_set * expr * switchbody (** Auto Generated Attributes **)
 and switchbody =
-| Coq_switchbody_nodefault  [@f label0] of switchclause list (** Auto Generated Attributes **)
-| Coq_switchbody_withdefault  [@f label0, label1, label2] of switchclause list * stat list * switchclause list (** Auto Generated Attributes **)
+| Coq_switchbody_nodefault  [@f clauses] of switchclause list (** Auto Generated Attributes **)
+| Coq_switchbody_withdefault  [@f clauses_before, default, clauses_after] of switchclause list * stat list * switchclause list (** Auto Generated Attributes **)
 and switchclause =
-| Coq_switchclause_intro  [@f label0, label1] of expr * stat list (** Auto Generated Attributes **)
+| Coq_switchclause_intro  [@f arg, stats] of expr * stat list (** Auto Generated Attributes **)
 and prog =
-| Coq_prog_intro  [@f label0, label1] of strictness_flag * element list (** Auto Generated Attributes **)
+| Coq_prog_intro  [@f strictness, elements] of strictness_flag * element list (** Auto Generated Attributes **)
 and element =
-| Coq_element_stat  [@f label0] of stat (** Auto Generated Attributes **)
-| Coq_element_func_decl  [@f label0, label1, label2] of string * string list * funcbody (** Auto Generated Attributes **)
+| Coq_element_stat  [@f stat] of stat (** Auto Generated Attributes **)
+| Coq_element_func_decl  [@f func_name, arg_names, body] of string * string list * funcbody (** Auto Generated Attributes **)
 
 type propdefs = (propname * propbody) list
 
@@ -389,7 +387,7 @@ type provide_this_flag = bool
 
 type env_record =
 | Coq_env_record_decl  [@f value] of decl_env_record (** Auto Generated Attributes **)
-| Coq_env_record_object  [@f value, label1] of object_loc * provide_this_flag (** Auto Generated Attributes **)
+| Coq_env_record_object  [@f value, provide_this] of object_loc * provide_this_flag (** Auto Generated Attributes **)
 
 type env_loc = int
 
diff --git a/generator/tests/jsref/LibHeap.ml b/generator/tests/jsref/LibHeap.ml
deleted file mode 100644
index e9dcc3a..0000000
--- a/generator/tests/jsref/LibHeap.ml
+++ /dev/null
@@ -1,93 +0,0 @@
-open Datatypes
-open LibBool
-open LibList
-open LibReflect
-
-module type HeapSpec = 
- sig 
-  type ('x0, 'x) heap 
-  
-  val empty : ('a1, 'a2) heap
-  
-  val write : ('a1, 'a2) heap -> 'a1 -> 'a2 -> ('a1, 'a2) heap
-  
-  val to_list : ('a1, 'a2) heap -> ('a1 * 'a2) list
-  
-  val read : 'a1 coq_Comparable -> ('a1, 'a2) heap -> 'a1 -> 'a2
-  
-  val read_option :
-    'a1 coq_Comparable -> ('a1, 'a2) heap -> 'a1 -> 'a2 option
-  
-  val rem : 'a1 coq_Comparable -> ('a1, 'a2) heap -> 'a1 -> ('a1, 'a2) heap
-  
-  val indom_decidable :
-    'a1 coq_Comparable -> ('a1, 'a2) heap -> 'a1 -> coq_Decidable
- end
-
-module HeapList = 
- struct 
-  type ('k, 'v) heap = ('k * 'v) list
-  
-  (** val empty : ('a1, 'a2) heap **)
-  
-  let empty =
-    []
-  
-  (** val to_list : ('a1, 'a2) heap -> ('a1, 'a2) heap **)
-  
-  let to_list l =
-    l
-  
-  (** val assoc : 'a1 coq_Comparable -> 'a1 -> ('a1 * 'a2) list -> 'a2 **)
-  
-  let rec assoc h1 k l = match l with
-  | [] -> raise Not_found
-  | p :: l' -> let (x, v) = p in if h1 x k then v else assoc h1 k l'
-  
-  (** val read : 'a1 coq_Comparable -> ('a1, 'a2) heap -> 'a1 -> 'a2 **)
-  
-  let read h l k =
-    assoc h k l
-  
-  (** val write : ('a1, 'a2) heap -> 'a1 -> 'a2 -> ('a1 * 'a2) list **)
-  
-  let write l k v =
-    (k, v) :: l
-  
-  (** val rem :
-      'a1 coq_Comparable -> ('a1, 'a2) heap -> 'a1 -> ('a1 * 'a2) list **)
-  
-  let rem h1 l k =
-    filter (fun p -> if h1 (fst p) k then false else true) l
-  
-  (** val read_option :
-      'a1 coq_Comparable -> ('a1, 'a2) heap -> 'a1 -> 'a2 option **)
-  
-  let read_option h =
-    let rec read_option0 l k =
-      match l with
-      | [] -> None
-      | p :: l' ->
-        let (x, v) = p in if h x k then Some v else read_option0 l' k
-    in read_option0
-  
-  (** val mem_assoc :
-      'a2 coq_Comparable -> 'a2 -> ('a2 * 'a1) list -> bool **)
-  
-  let rec mem_assoc h1 k l = match l with
-  | [] -> false
-  | p :: l' -> let (x, y) = p in coq_or (h1 x k) (mem_assoc h1 k l')
-  
-  (** val indom_dec :
-      'a1 coq_Comparable -> ('a1, 'a2) heap -> 'a1 -> bool **)
-  
-  let indom_dec h1 h k =
-    mem_assoc h1 k h
-  
-  (** val indom_decidable :
-      'a1 coq_Comparable -> ('a1, 'a2) heap -> 'a1 -> coq_Decidable **)
-  
-  let indom_decidable h h0 k =
-    indom_dec h h0 k
- end
-
diff --git a/generator/tests/jsref/Shared.ml b/generator/tests/jsref/Shared.ml
index 1327790..b7a0f92 100644
--- a/generator/tests/jsref/Shared.ml
+++ b/generator/tests/jsref/Shared.ml
@@ -1,6 +1,6 @@
 open BinInt
 open Datatypes
-open LibHeap
+open Heap
 open LibReflect
 open String0
 
@@ -39,49 +39,5 @@ type 'a coq_Pickable_option =
   'a option
   (* singleton inductive, whose constructor was pickable_option_make *)
 
-module HeapGen = 
- functor (Heap:HeapSpec) ->
- struct 
-  type ('k, 'v) heap = int * ('k, 'v) Heap.heap
-  
-  (** val empty : ('a1, 'a2) heap **)
-  
-  let empty =
-    (0, Heap.empty)
-  
-  (** val to_list : ('a1, 'a2) heap -> ('a1 * 'a2) list **)
-  
-  let to_list h =
-    Heap.to_list (snd h)
-  
-  (** val read : 'a1 coq_Comparable -> ('a1, 'a2) heap -> 'a1 -> 'a2 **)
-  
-  let read h h0 =
-    Heap.read h (snd h0)
-  
-  (** val write :
-      ('a1, 'a2) heap -> 'a1 -> 'a2 -> int * ('a1, 'a2) Heap.heap **)
-  
-  let write h k v =
-    let (id, h0) = h in ((Pervasives.succ id), (Heap.write (snd h) k v))
-  
-  (** val rem :
-      'a1 coq_Comparable -> ('a1, 'a2) heap -> 'a1 -> int * ('a1, 'a2)
-      Heap.heap **)
-  
-  let rem h h0 k =
-    let (id, h1) = h0 in ((Pervasives.succ id), (Heap.rem h (snd h0) k))
-  
-  (** val read_option :
-      'a1 coq_Comparable -> ('a1, 'a2) heap -> 'a1 -> 'a2 option **)
-  
-  let read_option h h0 =
-    Heap.read_option h (snd h0)
-  
-  (** val indom_decidable :
-      'a1 coq_Comparable -> ('a1, 'a2) heap -> 'a1 -> coq_Decidable **)
-  
-  let indom_decidable h1 p =
-    let (n, h0) = p in Heap.indom_decidable h1 (snd (n, h0))
- end
+
 
-- 
GitLab