The argument of [eq] do not need to be bounded in the graph.

This commit is contained in:
Olivier 2023-04-21 11:21:32 +02:00
parent 658f84a0c0
commit 2575c634d5
1 changed files with 16 additions and 22 deletions

View File

@ -449,8 +449,6 @@ end = struct
(* Equality test. *)
let eq v1 v2 : scope option =
assert (StructTable.mem (table ()) v1);
assert (StructTable.mem (table ()) v2);
(* The stopping condition of the search is a succeeding unification with
the vertex [v2]. *)
let process v1 scope =
@ -460,8 +458,13 @@ end = struct
with Clash ->
None
in
(* Returns only the scope. *)
Option.map snd @@ search process v1 dummy_scope
(* If one of them is not bounded, then, in particular, it cannot be equal
to the other one, so we fail. *)
if not (is_bounded v1) || not (is_bounded v2) then
None
else
(* Returns only the scope. *)
Option.map snd @@ search process v1 dummy_scope
end (* EqEnv *)
@ -797,24 +800,15 @@ and unify_abs q v1 v2
(* ... otherwise, retrieve their nodes in the rigid graph. *)
let v1 = EqEnv.get_rigid n1 in
let v2 = EqEnv.get_rigid n2 in
(* If one of them is not bounded, then, in particular, it cannot be equal
to the other one, so we fail. *)
if not (EqEnv.is_bounded v1 && EqEnv.is_bounded v2) then begin
if EqEnv.is_consistent_env () then
raise InconsistentConjunction
else
Abs.Abstract n1, Some (EqEnv.scope_inconsistent_env ())
end
else
(* Otherwise, we see if they are equal in the rigid graph. *)
match EqEnv.eq v1 v2 with
| None ->
if EqEnv.is_consistent_env () then
raise InconsistentConjunction
else
Abs.Abstract n1, Some (EqEnv.scope_inconsistent_env ())
| Some scope ->
Abs.Abstract n1, Some scope
(* We see if they are equal in the rigid graph. *)
match EqEnv.eq v1 v2 with
| None ->
if EqEnv.is_consistent_env () then
raise InconsistentConjunction
else
Abs.Abstract n1, Some (EqEnv.scope_inconsistent_env ())
| Some scope ->
Abs.Abstract n1, Some scope
(* [unify_rigid_structure q n s v] unify a rigid variable with abstract
structure [n] with a structure [s] (corresponding to the node [v] in the