From 4b79dcf1ec4ac826faf8b3c6e245082cf158c7c3 Mon Sep 17 00:00:00 2001
From: Andrei Paskevich <andrei@lri.fr>
Date: Mon, 1 Oct 2018 15:09:44 +0200
Subject: [PATCH] encoding_twin: make the order of added declarations more
deterministic
---
src/transform/encoding_twin.ml | 20 ++++++++++++++------
1 file changed, 14 insertions(+), 6 deletions(-)
diff --git a/src/transform/encoding_twin.ml b/src/transform/encoding_twin.ml
index 287a1918e..4d3456124 100644
--- a/src/transform/encoding_twin.ml
+++ b/src/transform/encoding_twin.ml
@@ -46,14 +46,22 @@ let make_pont = Wty.memoize 3 (fun ty ->
create_prop_decl Paxiom pr ax in
t2tb, tb2t, [t2tb_def; tb2t_def; bridge_l; bridge_r])
-let seen = Hty.create 7
+let seen_h = Hty.create 7
+let seen_q = Queue.create ()
+
+let check_in ty =
+ if not (Hty.mem seen_h ty) then begin
+ Hty.add seen_h ty ();
+ Queue.add ty seen_q
+ end
let add_decls tenv decls =
- let add ty () decls =
+ let add decls ty =
let _,_,defs = Mty.find ty tenv in
List.append defs decls in
- let decls = Hty.fold add seen decls in
- Hty.clear seen;
+ let decls = Queue.fold add decls seen_q in
+ Queue.clear seen_q;
+ Hty.clear seen_h;
decls
let conv_arg tenv t aty =
@@ -61,7 +69,7 @@ let conv_arg tenv t aty =
if ty_equal tty aty then t else
try
let t2tb,tb2t,_ = Mty.find tty tenv in
- Hty.replace seen tty ();
+ check_in tty;
match t.t_node with
| Tapp (fs,[t]) when ls_equal fs tb2t -> t
| _ -> fs_app t2tb [t] tty
@@ -73,7 +81,7 @@ let conv_app tenv fs tl tty =
if ty_equal tty vty then t else
try
let _,tb2t,_ = Mty.find tty tenv in
- Hty.replace seen tty ();
+ check_in tty;
fs_app tb2t [t] tty
with Not_found -> t
--
GitLab