Commit 4c716202 authored by Sylvain Dailler's avatar Sylvain Dailler

Proposition of t_equal modulo labels and triggers.

parent 4d276a7d
......@@ -282,7 +282,7 @@ let rec descend vml t = match t.t_node with
find vs vml
| _ -> Trm (t, vml)
let t_compare t1 t2 =
let t_compare trigger label t1 t2 =
let comp_raise c =
if c < 0 then raise CompLT else if c > 0 then raise CompGT in
let perv_compare h1 h2 = comp_raise (Pervasives.compare h1 h2) in
......@@ -327,7 +327,7 @@ let t_compare t1 t2 =
let rec t_compare bnd vml1 vml2 t1 t2 =
if t1 != t2 || vml1 <> [] || vml2 <> [] then begin
comp_raise (oty_compare t1.t_ty t2.t_ty);
comp_raise (Slab.compare t1.t_label t2.t_label);
if label then comp_raise (Slab.compare t1.t_label t2.t_label) else ();
match descend vml1 t1, descend vml2 t2 with
| Bnd i1, Bnd i2 -> perv_compare i1 i2
| Bnd _, Trm _ -> raise CompLT
......@@ -376,7 +376,7 @@ let t_compare t1 t2 =
let vml1 = (bv1, b1.bv_subst) :: vml1 in
let vml2 = (bv2, b2.bv_subst) :: vml2 in
let tr_cmp t1 t2 = t_compare bnd vml1 vml2 t1 t2; 0 in
comp_raise (Lists.compare (Lists.compare tr_cmp) tr1 tr2);
if trigger then comp_raise (Lists.compare (Lists.compare tr_cmp) tr1 tr2) else ();
t_compare bnd vml1 vml2 f1 f2
| Tbinop (op1,f1,g1), Tbinop (op2,f2,g2) ->
perv_compare op1 op2;
......@@ -402,7 +402,11 @@ let t_compare t1 t2 =
try t_compare 0 [] [] t1 t2; 0
with CompLT -> -1 | CompGT -> 1
let t_equal t1 t2 = (t_compare t1 t2 = 0)
let t_equal t1 t2 = (t_compare true true t1 t2 = 0)
let t_equal_nt_nl t1 t2 = (t_compare false false t1 t2 = 0)
let t_compare = t_compare true true
let t_similar t1 t2 =
oty_equal t1.t_ty t2.t_ty &&
......@@ -1639,4 +1643,3 @@ module TermTF = struct
let tr_fold fnT fnF = tr_fold (t_selecti fnT fnF)
let tr_map_fold fnT fnF = tr_map_fold (t_selecti fnT fnF)
end
......@@ -150,6 +150,8 @@ module Hterm : Exthtbl.S with type key = term
val t_compare : term -> term -> int
val t_equal : term -> term -> bool
val t_hash : term -> int
(* Equality modulo labels and triggers *)
val t_equal_nt_nl : term -> term -> bool
(** {2 Bindings} *)
......
......@@ -147,7 +147,7 @@ let apply pr : Task.task Trans.tlist = Trans.store (fun task ->
(* TODO export the exception *)
| _ -> failwith "Unable to instantiate variables with possible values" in
let inst_nt = t_subst subst nt in
if (Term.t_equal inst_nt g) then
if (Term.t_equal_nt_nl inst_nt g) then
let nlp = List.map (t_subst subst) lp in
let lt = List.map (fun ng -> Task.add_decl task (create_prop_decl Pgoal
(create_prsymbol (gen_ident "G")) ng)) nlp in
......
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