Avoid code duplication.

This commit is contained in:
François Pottier 2022-04-01 18:02:16 +02:00
parent e24284a064
commit 75eb8bafce
1 changed files with 16 additions and 18 deletions

View File

@ -201,27 +201,25 @@ module Data = struct
let structure = S.conjunction equate data1.structure data2.structure in
(* The new rank is the minimum of the two ranks. *)
let rank = min data1.rank data2.rank in
let fail () = raise InconsistentConjunction in
(* If either variable is rigid, the conjunction is also rigid. *)
(* If either variable is rigid, the conjunction is also rigid. However,
unification in the presence of rigid variables is subject to certain
restrictions. *)
let status : status =
match data1.status, data2.status with
| Generic, _
| _, Generic ->
match data1.status, data1.rank, data2.status, data2.rank with
| Generic, _, _, _
| _, _, Generic, _ ->
assert false
| Flexible, Flexible ->
| Flexible, _, Flexible, _ ->
Flexible
(* One cannot unify two rigid variables, *)
| Rigid, Rigid ->
fail ()
| Rigid, Flexible ->
(* ... or lower the rank of a rigid variable, *)
if (rank < data1.rank) then raise VariableScopeEscape;
(* ... or give it a non-leaf structure. *)
if not (S.is_leaf structure) then fail ();
Rigid
| Flexible, Rigid ->
if (rank < data2.rank) then raise VariableScopeEscape;
if not (S.is_leaf structure) then fail ();
| Rigid, _, Rigid, _ ->
(* One cannot unify two rigid variables. *)
raise InconsistentConjunction
| Rigid, rigid_rank, Flexible, _
| Flexible, _, Rigid, rigid_rank ->
(* One cannot lower the rank of a rigid variable. *)
if rank < rigid_rank then raise VariableScopeEscape;
(* One cannot assign non-leaf structure to a rigid variable. *)
if not (S.is_leaf structure) then raise InconsistentConjunction;
Rigid
in
(* There is no need to preserve marks during unification. *)