Commit 036366ad authored by Adrien KOUTSOS's avatar Adrien KOUTSOS

memoisation on r_equal too.

nsl went from 12s to 11.1s
parent 1f5ed38f
Pipeline #1660 failed with stage
in 10 seconds
......@@ -1304,7 +1304,22 @@ let pseudo_normalize : type a. env -> a term -> a term = fun env t ->
| Bool -> bt_pseudo_normalize env t
let r_equal : type a. env -> a term -> a term -> bool = fun env t t' ->
module PTerm = struct
type t = msg term * msg term
let equal (t0,t0') (t1,t1') = (t_equal t0 t1) && (t_equal t0' t1')
let hash (t,t') = Hashtbl.hash (t.content,t'.content)
end
module PBool = struct
type t = boole term * boole term
let equal (t0,t0') (t1,t1') = (t_equal t0 t1) && (t_equal t0' t1')
let hash (t,t') = Hashtbl.hash (t.content,t'.content)
end
module PTMem = Memoisation.Mem(PTerm)
module PBMem = Memoisation.Mem(PBool)
let _r_equal : type a. env -> (a term * a term) -> bool = fun env (t,t') ->
(* let test = false in *)
......@@ -1345,6 +1360,15 @@ let r_equal : type a. env -> a term -> a term -> bool = fun env t t' ->
| _ -> t_equal nt nt'
let t_r_equal = PTMem.make2 (_r_equal)
let bt_r_equal = PBMem.make2 (_r_equal)
let r_equal : type a. env -> a term -> a term -> bool = fun env t t' ->
match get_sort t with
| Msg -> t_r_equal env (t,t')
| Bool -> bt_r_equal env (t,t')
(******************)
(* Latex Printing *)
......
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