Commit 9b1103e4 authored by Andrei Paskevich's avatar Andrei Paskevich

and here is the real fix

parent 8a7fe32c
......@@ -27,14 +27,7 @@ open Task
open Decl
open Encoding
type tenv = {
kept : Sty.t;
pont : (lsymbol * lsymbol) Mty.t; (* t2tb, tb2t *)
seen : unit Hty.t;
next : unit Hty.t;
}
let add_pont ty pont =
let make_pont ty () =
let t2tb =
let t2tb_name = "t2tb" in
let t2tb_id = Libencoding.id_unprotected t2tb_name in
......@@ -43,18 +36,6 @@ let add_pont ty pont =
let tb2t_name = "tb2t" in
let tb2t_id = Libencoding.id_unprotecting tb2t_name in
create_fsymbol tb2t_id [ty] ty in
Mty.add ty (t2tb,tb2t) pont
let make_tenv kept = {
kept = kept;
pont = Sty.fold add_pont kept Mty.empty;
seen = Hty.create 7;
next = Hty.create 7 }
let add_decls tenv ty () decls =
(* if Hty.mem tenv.seen ty then decls else*)
let () = Hty.add tenv.seen ty () in
let (t2tb,tb2t) = Mty.find ty tenv.pont in
let t2tb_def = create_logic_decl [t2tb,None] in
let tb2t_def = create_logic_decl [tb2t,None] in
let bridge_l =
......@@ -75,19 +56,24 @@ let add_decls tenv ty () decls =
let ax = t_forall_close [x_vs] [[t2tb_tb2t_x]] eq in
let pr = create_prsymbol (id_fresh "BridgeR") in
create_prop_decl Paxiom pr ax in
t2tb_def :: tb2t_def :: bridge_l :: bridge_r :: decls
t2tb, tb2t, [t2tb_def; tb2t_def; bridge_l; bridge_r]
let seen = Hty.create 7
let add_decls tenv decls =
let decls = Hty.fold (add_decls tenv) tenv.next decls in
Hty.clear tenv.next;
let add ty () decls =
let _,_,defs = Mty.find ty tenv in
List.append defs decls in
let decls = Hty.fold add seen decls in
Hty.clear seen;
decls
let conv_arg tenv t aty =
let tty = t_type t in
if ty_equal tty aty then t else
try
let (t2tb,tb2t) = Mty.find tty tenv.pont in
Hty.replace tenv.next tty ();
let t2tb,tb2t,_ = Mty.find tty tenv in
Hty.replace seen tty ();
match t.t_node with
| Tapp (fs,[t]) when ls_equal fs tb2t -> t
| _ -> fs_app t2tb [t] tty
......@@ -98,8 +84,8 @@ let conv_app tenv fs tl tty =
let vty = Util.of_option fs.ls_value in
if ty_equal tty vty then t else
try
let (_,tb2t) = Mty.find tty tenv.pont in
Hty.replace tenv.next tty ();
let _,tb2t,_ = Mty.find tty tenv in
Hty.replace seen tty ();
fs_app tb2t [t] tty
with Not_found -> t
......@@ -136,7 +122,7 @@ let decl tenv d =
add_decls tenv decls
let t = Trans.on_tagged_ty Libencoding.meta_kept (fun s ->
Trans.decl (decl (make_tenv s)) None)
Trans.decl (decl (Mty.mapi make_pont s)) None)
let () = Hashtbl.replace Encoding.ft_enco_kept "twin" (const t)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment