encoding_twin: make the order of added declarations more deterministic

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