Skip to content
Snippets Groups Projects
Commit f43fbc7c authored by Shachar Itzhaky's avatar Shachar Itzhaky
Browse files

[bugfix] Replaced cps patch.

Was still causing stack overflows. More robust to just replace
`List.fold_right` with `rev` and `fold_left`.
parent 4f681ca2
Branches
No related tags found
No related merge requests found
......@@ -55,6 +55,11 @@ export COQBUILDDIR_REL
export ADDONS_PATH
export COQPKGS_ROOT
ifdef DEBUG
JSCOQ_DEBUG = 1
export JSCOQ_DEBUG
endif
all:
@echo "Welcome to jsCoq makefile. Targets are:"
@echo ""
......@@ -188,7 +193,7 @@ COQ_BRANCH = V8.13.0
COQ_BRANCH_LATEST = v8.13
COQ_REPOS = https://github.com/coq/coq.git
COQ_PATCHES = trampoline cps timeout $(COQ_PATCHES|$(WORD_SIZE)) $(COQ_PATCHES|$(ARCH))
COQ_PATCHES = trampoline fold timeout $(COQ_PATCHES|$(WORD_SIZE)) $(COQ_PATCHES|$(ARCH))
COQ_PATCHES|64 = coerce-32bit
COQ_PATCHES|Darwin/32 = byte-only
......
......
diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml
index 50fa605..ca970ad 100644
index d2eeebc..e6757ae 100644
--- a/vernac/declaremods.ml
+++ b/vernac/declaremods.ml
@@ -18,6 +18,11 @@ open Libnames
@@ -18,6 +18,9 @@ open Libnames
open Libobject
open Mod_subst
+let rec list_fold_right_cps f l init k =
+ match l with
+ | [] -> k init
+ | x :: xs -> list_fold_right_cps f xs init (fun res -> k (f x res))
+let rec list_fold_right_stackless f l init =
+ List.fold_left (fun x y -> f y x) init (List.rev l)
+
(** {6 Inlining levels} *)
(** Rigid / flexible module signature *)
@@ -315,7 +320,7 @@ and collect_object f i (name, obj as o) acc =
@@ -315,7 +318,7 @@ and collect_object f i (name, obj as o) acc =
| ModuleObject _ | ModuleTypeObject _ -> mark_object f o acc
and collect_objects f i prefix objs acc =
- List.fold_right (fun (id, obj) acc -> collect_object f i (Lib.make_oname prefix id, obj) acc) objs acc
+ list_fold_right_cps (fun (id, obj) acc -> collect_object f i (Lib.make_oname prefix id, obj) acc) objs acc (fun x -> x)
+ list_fold_right_stackless (fun (id, obj) acc -> collect_object f i (Lib.make_oname prefix id, obj) acc) objs acc
and collect_one_export f (f',mp) (exports,objs as acc) =
match filter_and f f' with
@@ -339,7 +344,7 @@ and collect_one_export f (f',mp) (exports,objs as acc) =
@@ -339,7 +342,7 @@ and collect_one_export f (f',mp) (exports,objs as acc) =
and collect_export f i mpl acc =
if Int.equal i 1 then
- List.fold_right (collect_one_export f) mpl acc
+ list_fold_right_cps (collect_one_export f) mpl acc (fun x -> x)
+ list_fold_right_stackless (collect_one_export f) mpl acc
else acc
let open_modtype i ((sp,kn),_) =
@@ -615,11 +620,11 @@ let intern_args params =
@@ -615,7 +618,7 @@ let intern_args params =
let check_sub mtb sub_mtb_l =
(* The constraints are checked and forgot immediately : *)
- ignore (List.fold_right
+ ignore (list_fold_right_cps
+ ignore (list_fold_right_stackless
(fun sub_mtb env ->
Environ.add_constraints
(Subtyping.check_subtypes env mtb sub_mtb) env)
- sub_mtb_l (Global.env()))
+ sub_mtb_l (Global.env()) (fun x -> x))
(** This function checks if the type calculated for the module [mp] is
a subtype of all signatures in [sub_mtb_l]. Uses only the global
@@ -1056,7 +1061,7 @@ let end_library ?except ~output_native_objects dir =
@@ -1056,7 +1059,7 @@ let end_library ?except ~output_native_objects dir =
cenv,(substitute,keep),ast
let import_modules ~export mpl =
- let _,objs = List.fold_right collect_module_objects mpl (MPmap.empty, []) in
+ let _,objs = list_fold_right_cps collect_module_objects mpl (MPmap.empty, []) (fun x -> x) in
+ let _,objs = list_fold_right_stackless collect_module_objects mpl (MPmap.empty, []) in
List.iter (fun (f,o) -> open_object f 1 o) objs;
if export then Lib.add_anonymous_entry (Lib.Leaf (ExportObject { mpl }))
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please to comment