From f12821c668a812ed3d0a8fdebf3a4e6fb9dab404 Mon Sep 17 00:00:00 2001
From: Thomas Wood <thomas.wood09@imperial.ac.uk>
Date: Wed, 5 Oct 2016 15:47:37 +0200
Subject: [PATCH] Switch minimum version to OCaml 4.02.2 (maximum version
<4.03)
Required changes:
* Ignore ocaml.doc and ocaml.text attributes, which are now
automatically extracted from comments.
* Swap type definition attribute syntax in test/* files.
Other changes:
* Add opam package file and `make init` command for dependencies.
* Change "Automatically Generated Attributes" documentation to comments.
---
deprecated/ml-add-cstr-annots.pl | 4 +-
generator/Makefile | 19 ++-
generator/README.org | 14 +-
generator/js_of_ast.ml | 4 +-
generator/opam | 16 ++
generator/tests/jsref/Datatypes.ml | 6 +-
generator/tests/jsref/JsCommon.ml | 16 +-
generator/tests/jsref/JsInterpreterMonads.ml | 8 +-
generator/tests/jsref/JsSyntax.ml | 153 +++++++++----------
generator/tests/jsref/StdMap.ml | 4 +-
generator/tests/lambda/BinNums.ml | 12 +-
generator/tests/lambda/Datatypes.ml | 4 +-
generator/tests/lambda/Lambda.ml | 28 ++--
13 files changed, 152 insertions(+), 136 deletions(-)
create mode 100644 generator/opam
diff --git a/deprecated/ml-add-cstr-annots.pl b/deprecated/ml-add-cstr-annots.pl
index df583ff..0b79c93 100755
--- a/deprecated/ml-add-cstr-annots.pl
+++ b/deprecated/ml-add-cstr-annots.pl
@@ -17,7 +17,7 @@ foreach $fname (@ARGV) {
}
}
$annot = $annot . "] ";
- print NEW $1 . $annot . $2 . " (** Auto Generated Attributes **)\n";
+ print NEW $1 . $annot . $2 . " (* Auto Generated Attributes *)\n";
} else {
print NEW $line;
}
@@ -25,4 +25,4 @@ foreach $fname (@ARGV) {
close(FILE);
close(NEW);
rename("$fname.temp", $fname) or die "can't rename $fname.temp to $fname: $!";
-}
\ No newline at end of file
+}
diff --git a/generator/Makefile b/generator/Makefile
index 25d8f17..215479c 100644
--- a/generator/Makefile
+++ b/generator/Makefile
@@ -5,13 +5,21 @@
# make lineof # build lineof.js
# make interp # build interp.js
#
-# requires: opam switch 4.02.1; eval `opam config env`
+# requires: opam switch 4.02.3; eval `opam config env`
# TODO: test/lambda is not longer supported
###############################################################
# Paths
+all: everything
+init:
+ opam switch 4.02.3
+ eval `opam config env`
+ opam pin -yn add jsjsref .
+ opam install -y jsjsref --deps-only
+
+
STDLIB_DIR := stdlib_ml
TESTS_DIR := tests
JSREF_DIR := jsref
@@ -73,8 +81,6 @@ ALL_LINEOF := $(DISPLAYED:.ml=.token.js) $(DISPLAYED:.ml=.mlloc.js) $(DISPLAYED:
###############################################################
# Global options
-all: everything
-
.PHONY: all clean .log.js .unlog.js .token.js .mlloc.js .ptoken.js .pseudo.js
# all gen log unlog
@@ -103,7 +109,7 @@ DISPLAYGEN := $(OCAMLPAR) ./displayed_sources.byte
ifeq ($(filter clean%,$(MAKECMDGOALS)),)
#-include $(JSREF_ML:.ml=.ml.d)
--include $(JSREF_PATH)/.depends
+include $(JSREF_PATH)/.depends
endif
@@ -122,9 +128,6 @@ $(STDLIB_DIR)/stdlib.cmi: $(STDLIB_DIR)/stdlib.mli
monad_ppx.native: monad_ppx.ml
$(OCAMLBUILD) $@
-#ocamlfind ocamlc -linkpkg -o $@ $<
-# -package compiler-libs.common
-
##### Rule for binaries
%.byte: *.ml _tags monad_ppx.native
@@ -135,8 +138,8 @@ monad_ppx.native: monad_ppx.ml
$(JSREF_PATH)/.depends: $(JSREF_ML)
$(OCAMLDEP) -all -I $(<D) $(<D)/* > $@
-##### Rule for cmi
+##### Rule for cmi
tests/%.cmi: tests/%.ml main.byte stdlib
$(MLTOJS) -mode cmi -I $(<D) $<
diff --git a/generator/README.org b/generator/README.org
index b2cc02d..3752f09 100644
--- a/generator/README.org
+++ b/generator/README.org
@@ -14,7 +14,7 @@
- `node.js` and the `esprima` package. In order to get the esprima
package the more convenient way is to get `npm` (/node package
manager/) and run `npm install esprima`.
- - ocaml 4.02.1
+ - ocaml >= 4.02.2, < 4.03
** How to run it
@@ -34,8 +34,8 @@ make cleanall
** How does it work?
In order to get the statically typed abstract syntax tree (STAST) of
- OCaml we usethe same files that are used in the compiler of OCaml
- 4.02.1 (hence the dependency).
+ OCaml we link against compiler-libs, we have tested against versions
+ 4.02.2 and 4.02.3.
On top, of this STAST, there is a custom back-end that
transliterate OCaml to ECMAScript. The code written in OCaml cannot
@@ -59,11 +59,7 @@ make cleanall
#+BEGIN_src
type 'a tree =
- | Leaf [@f value] of `a
- | Node [@f left, value, right] of `a tree * `a * `a tree
+ | Leaf of `a [@f value]
+ | Node of `a tree * `a * `a tree [@f left, value, right]
#+END_src
-
-Special note: from OCaml 4.02.2 annotations do not have the same
-syntax, but for now we work with OCaml 4.02.1 so the code above
-works and is recommended.
diff --git a/generator/js_of_ast.ml b/generator/js_of_ast.ml
index 006ce5a..77164bd 100644
--- a/generator/js_of_ast.ml
+++ b/generator/js_of_ast.ml
@@ -831,7 +831,9 @@ and js_of_structure_item s =
| Tstr_class _ -> out_of_scope loc "objects"
| Tstr_class_type _ -> out_of_scope loc "class types"
| Tstr_include _ -> out_of_scope loc "includes"
- | Tstr_attribute _ -> out_of_scope loc "attributes"
+ | Tstr_attribute (l, _) ->
+ if l.txt = "ocaml.doc" || l.txt = "ocaml.text" then ("",[])
+ else out_of_scope loc "attributes"
and js_of_branch ctx dest b eobj =
let spat, binders = js_of_pattern b.c_lhs eobj in
diff --git a/generator/opam b/generator/opam
new file mode 100644
index 0000000..648cf9a
--- /dev/null
+++ b/generator/opam
@@ -0,0 +1,16 @@
+opam-version: "1.2"
+name: "jsjsref"
+version: "1.0~dev"
+maintainer: "Thomas Wood <thomas.wood09@imperial.ac.uk>"
+authors: ["Arthur Charguéraud <arthur@chargueraud.org>"
+ "Alan Schmitt <alan.schmitt@inria.fr"
+ "Thomas Wood <thomas.wood09@imperial.ac.uk>"]
+homepage: "http://jscert.org/"
+license: "BSD 3-clause"
+available: [ocaml-version >= "4.02.2" && ocaml-version < "4.03"]
+build: [
+ [make]
+]
+depends: [
+ "ocamlfind" {build}
+]
diff --git a/generator/tests/jsref/Datatypes.ml b/generator/tests/jsref/Datatypes.ml
index 02b3fe2..8cab041 100644
--- a/generator/tests/jsref/Datatypes.ml
+++ b/generator/tests/jsref/Datatypes.ml
@@ -8,7 +8,7 @@ let fst p = let (x, y) = p in x
let snd p = let (x, y) = p in y
type comparison =
-| Eq [@f] (** Auto Generated Attributes **)
-| Lt [@f] (** Auto Generated Attributes **)
-| Gt [@f] (** Auto Generated Attributes **)
+| Eq [@f] (* Auto Generated Attributes *)
+| Lt [@f] (* Auto Generated Attributes *)
+| Gt [@f] (* Auto Generated Attributes *)
diff --git a/generator/tests/jsref/JsCommon.ml b/generator/tests/jsref/JsCommon.ml
index 2b3836d..77de460 100644
--- a/generator/tests/jsref/JsCommon.ml
+++ b/generator/tests/jsref/JsCommon.ml
@@ -238,11 +238,11 @@ let descriptor_intro_empty =
descriptor_configurable = None }
type ref_kind =
-| Coq_ref_kind_null [@f] (** Auto Generated Attributes **)
-| Coq_ref_kind_undef [@f] (** Auto Generated Attributes **)
-| Coq_ref_kind_primitive_base [@f] (** Auto Generated Attributes **)
-| Coq_ref_kind_object [@f] (** Auto Generated Attributes **)
-| Coq_ref_kind_env_record [@f] (** Auto Generated Attributes **)
+| Coq_ref_kind_null [@f] (* Auto Generated Attributes *)
+| Coq_ref_kind_undef [@f] (* Auto Generated Attributes *)
+| Coq_ref_kind_primitive_base [@f] (* Auto Generated Attributes *)
+| Coq_ref_kind_object [@f] (* Auto Generated Attributes *)
+| Coq_ref_kind_env_record [@f] (* Auto Generated Attributes *)
(** val ref_kind_of : ref -> ref_kind **)
@@ -489,8 +489,8 @@ let prog_vardecl p =
concat (LibList.map element_vardecl (prog_elements p))
type preftype =
-| Coq_preftype_number [@f] (** Auto Generated Attributes **)
-| Coq_preftype_string [@f] (** Auto Generated Attributes **)
+| Coq_preftype_number [@f] (* Auto Generated Attributes *)
+| Coq_preftype_string [@f] (* Auto Generated Attributes *)
(** val method_of_preftype : preftype -> string **)
@@ -589,7 +589,7 @@ let parse_pickable = (fun s strict ->
(*Translate_syntax.parse_esprima strict s*)
(* with
(* | Translate_syntax.CoqSyntaxDoesNotSupport _ -> assert false (* Temporary *) *)
- | Parser.ParserFailure _ [@f] (** Auto Generated Attributes **)
+ | Parser.ParserFailure _ [@f] (* Auto Generated Attributes *)
| Parser.InvalidArgument ->
prerr_string ("Warning: Parser error on eval. Input string: \"" ^ str ^ "\"\n");
None
diff --git a/generator/tests/jsref/JsInterpreterMonads.ml b/generator/tests/jsref/JsInterpreterMonads.ml
index d904026..90642ad 100644
--- a/generator/tests/jsref/JsInterpreterMonads.ml
+++ b/generator/tests/jsref/JsInterpreterMonads.ml
@@ -9,10 +9,10 @@ open Shared
type __ = unit
type 't resultof =
-| Coq_result_some [@f value] of 't (** Auto Generated Attributes **)
-| Coq_result_not_yet_implemented [@f] (** Auto Generated Attributes **)
-| Coq_result_impossible [@f] (** Auto Generated Attributes **)
-| Coq_result_bottom [@f state] of state (** Auto Generated Attributes **)
+| Coq_result_some of 't [@f value] (* Auto Generated Attributes *)
+| Coq_result_not_yet_implemented [@f] (* Auto Generated Attributes *)
+| Coq_result_impossible [@f] (* Auto Generated Attributes *)
+| Coq_result_bottom of state [@f state] (* Auto Generated Attributes *)
type 't specres = 't specret resultof
diff --git a/generator/tests/jsref/JsSyntax.ml b/generator/tests/jsref/JsSyntax.ml
index e8e482d..e625ddb 100644
--- a/generator/tests/jsref/JsSyntax.ml
+++ b/generator/tests/jsref/JsSyntax.ml
@@ -43,13 +43,13 @@ type binary_op =
type literal =
| Coq_literal_null [@f]
-| Coq_literal_bool [@f value] of bool
-| Coq_literal_number [@f value] of JsNumber.number
-| Coq_literal_string [@f value] of string
+| Coq_literal_bool of bool [@f value]
+| Coq_literal_number of JsNumber.number [@f value]
+| Coq_literal_string of string [@f value]
type label =
| Coq_label_empty [@f]
-| Coq_label_string [@f value] of string
+| Coq_label_string of string [@f value]
type label_set = label list
@@ -61,61 +61,61 @@ let strictness_false =
false
type propname =
-| Coq_propname_identifier [@f value] of string
-| Coq_propname_string [@f value] of string
-| Coq_propname_number [@f value] of JsNumber.number
+| Coq_propname_identifier of string [@f value]
+| Coq_propname_string of string [@f value]
+| Coq_propname_number of JsNumber.number [@f value]
type expr =
| Coq_expr_this [@f]
-| Coq_expr_identifier [@f name] of string
-| Coq_expr_literal [@f value] of literal
-| Coq_expr_object [@f fields] of (propname * propbody) list
-| Coq_expr_array [@f elements] of expr option list
-| Coq_expr_function [@f func_name_opt, arg_names, body] of string option * string list * funcbody
-| Coq_expr_access [@f obj, field] of expr * expr
-| Coq_expr_member [@f obj, field_name] of expr * string
-| Coq_expr_new [@f func, args] of expr * expr list
-| Coq_expr_call [@f func, args] of expr * expr list
-| Coq_expr_unary_op [@f op, arg] of unary_op * expr
-| Coq_expr_binary_op [@f arg1, op, arg2] of expr * binary_op * expr
-| Coq_expr_conditional [@f cond, then_branch, else_branch] of expr * expr * expr
-| Coq_expr_assign [@f left_expr, op_opt, right_expr] of expr * binary_op option * expr
+| Coq_expr_identifier of string [@f name]
+| Coq_expr_literal of literal [@f value]
+| Coq_expr_object of (propname * propbody) list [@f fields]
+| Coq_expr_array of expr option list [@f elements]
+| Coq_expr_function of string option * string list * funcbody [@f func_name_opt, arg_names, body]
+| Coq_expr_access of expr * expr [@f obj, field]
+| Coq_expr_member of expr * string [@f obj, field_name]
+| Coq_expr_new of expr * expr list [@f func, args]
+| Coq_expr_call of expr * expr list [@f func, args]
+| Coq_expr_unary_op of unary_op * expr [@f op, arg]
+| Coq_expr_binary_op of expr * binary_op * expr [@f arg1, op, arg2]
+| Coq_expr_conditional of expr * expr * expr [@f cond, then_branch, else_branch]
+| Coq_expr_assign of expr * binary_op option * expr [@f left_expr, op_opt, right_expr]
and propbody =
-| Coq_propbody_val [@f expr] of expr
-| Coq_propbody_get [@f body] of funcbody
-| Coq_propbody_set [@f names, body] of string list * funcbody
+| Coq_propbody_val of expr [@f expr]
+| Coq_propbody_get of funcbody [@f body]
+| Coq_propbody_set of string list * funcbody [@f names, body]
and funcbody =
-| Coq_funcbody_intro [@f prog, source] of prog * string
+| Coq_funcbody_intro of prog * string [@f prog, source]
and stat =
-| Coq_stat_expr [@f expr] of expr
-| Coq_stat_label [@f label, stat] of string * stat
-| Coq_stat_block [@f stats] of stat list
-| Coq_stat_var_decl [@f decls] of (string * expr option) list
-| Coq_stat_if [@f cond, then_branch, else_branch] of expr * stat * stat option
-| Coq_stat_do_while [@f labels, body, cond] of label_set * stat * expr
-| Coq_stat_while [@f labels, cond, body] of label_set * expr * stat
-| Coq_stat_with [@f obj, stat] of expr * stat
-| Coq_stat_throw [@f arg] of expr
-| Coq_stat_return [@f arg_opt] of expr option
-| Coq_stat_break [@f label] of label
-| Coq_stat_continue [@f label] of label
-| Coq_stat_try [@f body, catch_stats_opt, finally_opt] of stat * (string * stat) option * stat option
-| Coq_stat_for [@f labels, init, cond, step, body] of label_set * expr option * expr option * expr option * stat
-| Coq_stat_for_var [@f labels, init, cond, step, body] of label_set * (string * expr option) list * expr option * expr option * stat
-| Coq_stat_for_in [@f labels, id, obj, body] of label_set * expr * expr * stat
-| Coq_stat_for_in_var [@f labels, id, init, obj, body] of label_set * string * expr option * expr * stat
+| Coq_stat_expr of expr [@f expr]
+| Coq_stat_label of string * stat [@f label, stat]
+| Coq_stat_block of stat list [@f stats]
+| Coq_stat_var_decl of (string * expr option) list [@f decls]
+| Coq_stat_if of expr * stat * stat option [@f cond, then_branch, else_branch]
+| Coq_stat_do_while of label_set * stat * expr [@f labels, body, cond]
+| Coq_stat_while of label_set * expr * stat [@f labels, cond, body]
+| Coq_stat_with of expr * stat [@f obj, stat]
+| Coq_stat_throw of expr [@f arg]
+| Coq_stat_return of expr option [@f arg_opt]
+| Coq_stat_break of label [@f label]
+| Coq_stat_continue of label [@f label]
+| Coq_stat_try of stat * (string * stat) option * stat option [@f body, catch_stats_opt, finally_opt]
+| Coq_stat_for of label_set * expr option * expr option * expr option * stat [@f labels, init, cond, step, body]
+| Coq_stat_for_var of label_set * (string * expr option) list * expr option * expr option * stat [@f labels, init, cond, step, body]
+| Coq_stat_for_in of label_set * expr * expr * stat [@f labels, id, obj, body]
+| Coq_stat_for_in_var of label_set * string * expr option * expr * stat [@f labels, id, init, obj, body]
| Coq_stat_debugger [@f]
-| Coq_stat_switch [@f labels, arg, body] of label_set * expr * switchbody
+| Coq_stat_switch of label_set * expr * switchbody [@f labels, arg, body]
and switchbody =
-| Coq_switchbody_nodefault [@f clauses] of switchclause list
-| Coq_switchbody_withdefault [@f clauses_before, clause_default, clauses_after] of switchclause list * stat list * switchclause list
+| Coq_switchbody_nodefault of switchclause list [@f clauses]
+| Coq_switchbody_withdefault of switchclause list * stat list * switchclause list [@f clauses_before, clause_default, clauses_after]
and switchclause =
-| Coq_switchclause_intro [@f arg, stats] of expr * stat list
+| Coq_switchclause_intro of expr * stat list [@f arg, stats]
and prog =
-| Coq_prog_intro [@f strictness, elements] of strictness_flag * element list
+| Coq_prog_intro of strictness_flag * element list [@f strictness, elements]
and element =
-| Coq_element_stat [@f stat] of stat
-| Coq_element_func_decl [@f func_name, arg_names, body] of string * string list * funcbody
+| Coq_element_stat of stat [@f stat]
+| Coq_element_func_decl of string * string list * funcbody [@f func_name, arg_names, body]
type propdefs = (propname * propbody) list
@@ -218,19 +218,19 @@ type prealloc =
| Coq_prealloc_error_proto_to_string [@f]
| Coq_prealloc_throw_type_error [@f]
| Coq_prealloc_json [@f]
-| Coq_prealloc_mathop [@f mathop] of mathop
-| Coq_prealloc_native_error [@f error] of native_error
-| Coq_prealloc_native_error_proto [@f error] of native_error
+| Coq_prealloc_mathop of mathop [@f mathop]
+| Coq_prealloc_native_error of native_error [@f error]
+| Coq_prealloc_native_error_proto of native_error [@f error]
type call =
| Coq_call_default [@f]
| Coq_call_after_bind [@f]
-| Coq_call_prealloc [@f prealloc] of prealloc
+| Coq_call_prealloc of prealloc [@f prealloc]
type construct =
| Coq_construct_default [@f]
| Coq_construct_after_bind [@f]
-| Coq_construct_prealloc [@f prealloc] of prealloc
+| Coq_construct_prealloc of prealloc [@f prealloc]
type builtin_has_instance =
| Coq_builtin_has_instance_function [@f]
@@ -271,19 +271,19 @@ type builtin_define_own_prop =
| Coq_builtin_define_own_prop_args_obj [@f]
type object_loc =
-| Coq_object_loc_normal [@f address] of int
-| Coq_object_loc_prealloc [@f prealloc] of prealloc
+| Coq_object_loc_normal of int [@f address]
+| Coq_object_loc_prealloc of prealloc [@f prealloc]
type prim =
| Coq_prim_undef [@f]
| Coq_prim_null [@f]
-| Coq_prim_bool [@f value] of bool
-| Coq_prim_number [@f value] of JsNumber.number
-| Coq_prim_string [@f value] of string
+| Coq_prim_bool of bool [@f value]
+| Coq_prim_number of JsNumber.number [@f value]
+| Coq_prim_string of string [@f value]
type value =
-| Coq_value_prim [@f value] of prim
-| Coq_value_object [@f value] of object_loc
+| Coq_value_prim of prim [@f value]
+| Coq_value_object of object_loc [@f value]
type coq_type =
| Coq_type_undef [@f]
@@ -336,8 +336,8 @@ let attributes_accessor_enumerable x = x.attributes_accessor_enumerable
let attributes_accessor_configurable x = x.attributes_accessor_configurable
type attributes =
-| Coq_attributes_data_of [@f value] of attributes_data
-| Coq_attributes_accessor_of [@f value] of attributes_accessor
+| Coq_attributes_data_of of attributes_data [@f value]
+| Coq_attributes_accessor_of of attributes_accessor [@f value]
type descriptor = { descriptor_value : value option;
descriptor_writable : bool option;
@@ -372,7 +372,7 @@ let descriptor_configurable x = x.descriptor_configurable
type full_descriptor =
| Coq_full_descriptor_undef [@f]
-| Coq_full_descriptor_some [@f value] of attributes
+| Coq_full_descriptor_some of attributes [@f value]
type mutability =
| Coq_mutability_uninitialized_immutable [@f]
@@ -385,8 +385,8 @@ type decl_env_record = (string, mutability * value) Heap.heap
type provide_this_flag = bool
type env_record =
-| Coq_env_record_decl [@f value] of decl_env_record
-| Coq_env_record_object [@f value, provide_this] of object_loc * provide_this_flag
+| Coq_env_record_decl of decl_env_record [@f value]
+| Coq_env_record_object of object_loc * provide_this_flag [@f value, provide_this]
type env_loc = int
@@ -420,8 +420,8 @@ let execution_ctx_strict x = x.execution_ctx_strict
type prop_name = string
type ref_base_type =
-| Coq_ref_base_type_value [@f value] of value
-| Coq_ref_base_type_env_loc [@f value] of env_loc
+| Coq_ref_base_type_value of value [@f value]
+| Coq_ref_base_type_env_loc of env_loc [@f value]
type ref = { ref_base : ref_base_type; ref_name : prop_name;
ref_strict : bool }
@@ -563,10 +563,9 @@ let object_bound_args_ x = x.object_bound_args_
let object_parameter_map_ x = x.object_parameter_map_
type event =
-| Coq_delete_event [@f loc, name, locopt] of object_loc * prop_name * object_loc option
-| Coq_mutateproto_event [@f loc, fields] of object_loc * (object_loc * prop_name) list
- * (object_loc * prop_name) list
-| Coq_enumchange_event [@f loc, name] of object_loc * prop_name
+| Coq_delete_event of object_loc * prop_name * object_loc option [@f loc, name, locopt]
+| Coq_mutateproto_event of object_loc * (object_loc * prop_name) list * (object_loc * prop_name) list [@f loc, fields]
+| Coq_enumchange_event of object_loc * prop_name [@f loc, name]
type state = { state_object_heap : (object_loc, coq_object) Heap.heap;
state_env_record_heap : (env_loc, env_record) Heap.heap;
@@ -589,8 +588,8 @@ type restype =
type resvalue =
| Coq_resvalue_empty [@f]
-| Coq_resvalue_value [@f value] of value
-| Coq_resvalue_ref [@f ref] of ref
+| Coq_resvalue_value of value [@f value]
+| Coq_resvalue_ref of ref [@f ref]
type res = { res_type : restype; res_value : resvalue; res_label : label }
@@ -656,7 +655,7 @@ let res_throw v =
type out =
| Coq_out_div [@f]
-| Coq_out_ter [@f state, res] of state * res
+| Coq_out_ter of state * res [@f state, res]
(** val out_void : state -> out **)
@@ -664,8 +663,8 @@ let out_void s =
Coq_out_ter (s, res_empty)
type 't specret =
-| Coq_specret_val [@f state, res] of state * 't
-| Coq_specret_out [@f out] of out
+| Coq_specret_val of state * 't [@f state, res]
+| Coq_specret_out of out [@f out]
type codetype =
| Coq_codetype_func [@f]
@@ -707,4 +706,4 @@ let thebound =
((fun p -> 1. +. (2. *. p))
1.)))))))))))))))))))))))))))))))
-*)
\ No newline at end of file
+*)
diff --git a/generator/tests/jsref/StdMap.ml b/generator/tests/jsref/StdMap.ml
index 9ce7277..2736e4f 100644
--- a/generator/tests/jsref/StdMap.ml
+++ b/generator/tests/jsref/StdMap.ml
@@ -2,8 +2,8 @@
type ('a,'b) t =
- Empty [@f ]
- | Node [@f l, x, d, r, h] of ('a,'b) t * 'a * 'b * ('a,'b) t * int
+ Empty [@f]
+ | Node of ('a,'b) t * 'a * 'b * ('a,'b) t * int [@f l, x, d, r, h]
let height = function
Empty -> 0
diff --git a/generator/tests/lambda/BinNums.ml b/generator/tests/lambda/BinNums.ml
index 2731729..fc21696 100644
--- a/generator/tests/lambda/BinNums.ml
+++ b/generator/tests/lambda/BinNums.ml
@@ -1,10 +1,10 @@
type positive =
-| Coq_xI [@f label0] of positive (** Auto Generated Attributes **)
-| Coq_xO [@f label0] of positive (** Auto Generated Attributes **)
-| Coq_xH [@f] (** Auto Generated Attributes **)
+| Coq_xI [@f label0] of positive (* Auto Generated Attributes *)
+| Coq_xO [@f label0] of positive (* Auto Generated Attributes *)
+| Coq_xH [@f] (* Auto Generated Attributes *)
type coq_Z =
-| Z0 [@f] (** Auto Generated Attributes **)
-| Zpos [@f label0] of positive (** Auto Generated Attributes **)
-| Zneg [@f label0] of positive (** Auto Generated Attributes **)
+| Z0 [@f] (* Auto Generated Attributes *)
+| Zpos [@f label0] of positive (* Auto Generated Attributes *)
+| Zneg [@f label0] of positive (* Auto Generated Attributes *)
diff --git a/generator/tests/lambda/Datatypes.ml b/generator/tests/lambda/Datatypes.ml
index f27df1c..29f4cd5 100644
--- a/generator/tests/lambda/Datatypes.ml
+++ b/generator/tests/lambda/Datatypes.ml
@@ -1,4 +1,4 @@
type nat =
-| O [@f] (** Auto Generated Attributes **)
-| S [@f label0] of nat (** Auto Generated Attributes **)
+| O [@f] (* Auto Generated Attributes *)
+| S [@f label0] of nat (* Auto Generated Attributes *)
diff --git a/generator/tests/lambda/Lambda.ml b/generator/tests/lambda/Lambda.ml
index 1e5834e..82e00a5 100644
--- a/generator/tests/lambda/Lambda.ml
+++ b/generator/tests/lambda/Lambda.ml
@@ -3,16 +3,16 @@ open Datatypes
open LibVar
type coq_val =
-| Coq_val_int [@f label0] of coq_Z (** Auto Generated Attributes **)
-| Coq_val_clo [@f label0, label1] of var * trm (** Auto Generated Attributes **)
-| Coq_val_err [@f] (** Auto Generated Attributes **)
+| Coq_val_int [@f label0] of coq_Z (* Auto Generated Attributes *)
+| Coq_val_clo [@f label0, label1] of var * trm (* Auto Generated Attributes *)
+| Coq_val_err [@f] (* Auto Generated Attributes *)
and trm =
-| Coq_trm_val [@f label0] of coq_val (** Auto Generated Attributes **)
-| Coq_trm_var [@f label0] of var (** Auto Generated Attributes **)
-| Coq_trm_abs [@f label0, label1] of var * trm (** Auto Generated Attributes **)
-| Coq_trm_app [@f label0, label1] of trm * trm (** Auto Generated Attributes **)
-| Coq_trm_try [@f label0, label1] of trm * trm (** Auto Generated Attributes **)
-| Coq_trm_raise [@f label0] of trm (** Auto Generated Attributes **)
+| Coq_trm_val [@f label0] of coq_val (* Auto Generated Attributes *)
+| Coq_trm_var [@f label0] of var (* Auto Generated Attributes *)
+| Coq_trm_abs [@f label0, label1] of var * trm (* Auto Generated Attributes *)
+| Coq_trm_app [@f label0, label1] of trm * trm (* Auto Generated Attributes *)
+| Coq_trm_try [@f label0, label1] of trm * trm (* Auto Generated Attributes *)
+| Coq_trm_raise [@f label0] of trm (* Auto Generated Attributes *)
(** val subst : var -> coq_val -> trm -> trm **)
@@ -26,13 +26,13 @@ let rec subst x v t = match t with
| Coq_trm_raise t1 -> Coq_trm_raise (subst x v t1)
type beh =
-| Coq_beh_ret [@f label0] of coq_val (** Auto Generated Attributes **)
-| Coq_beh_exn [@f label0] of coq_val (** Auto Generated Attributes **)
-| Coq_beh_err [@f] (** Auto Generated Attributes **)
+| Coq_beh_ret [@f label0] of coq_val (* Auto Generated Attributes *)
+| Coq_beh_exn [@f label0] of coq_val (* Auto Generated Attributes *)
+| Coq_beh_err [@f] (* Auto Generated Attributes *)
type res =
-| Coq_res_return [@f label0] of beh (** Auto Generated Attributes **)
-| Coq_res_bottom [@f] (** Auto Generated Attributes **)
+| Coq_res_return [@f label0] of beh (* Auto Generated Attributes *)
+| Coq_res_bottom [@f] (* Auto Generated Attributes *)
(** val if_success : res -> (coq_val -> res) -> res **)
--
GitLab