This commit is contained in:
Olivier 2023-01-23 09:58:39 +01:00
parent d558af66c4
commit 5a017aeaa7
1 changed files with 34 additions and 13 deletions

View File

@ -50,6 +50,11 @@ type rank =
let base_rank =
0
type scope =
int
let base_scope =
0
(* -------------------------------------------------------------------------- *)
@ -122,6 +127,7 @@ type 'a data = {
id: id;
mutable structure: 'a S.structure;
mutable rank: rank;
mutable scope: scope;
mutable status: status;
mutable mark: mark;
}
@ -146,6 +152,19 @@ let adjust_rank (data : 'a data) (k : rank) =
else
raise VariableScopeEscape
(* If [s] is greater than the current rank, it causes an error : a type equality
is escaping its scope. Otherwise [adjust_scope data s] is equivalent to
[data.scope <- max s data.scope]. *)
let _adjust_scope (data : 'a data) (s : scope) =
assert (data.status <> Generic);
if s > data.scope then
if s <= data.rank then
data.scope <- s
else
raise VariableScopeEscape
(* The module [Data] satisfies the signature [USTRUCTURE] required by the
functor [Unifier.Make]. *)
@ -160,10 +179,10 @@ module Data = struct
let dummy : mark =
fresh_mark()
let make structure rank status =
let make structure rank scope status =
let id = fresh_id() in
let mark = dummy in
{ id; structure; rank; status; mark }
{ id; structure; rank; scope; status; mark }
let map f data =
{ data with structure = S.map f data.structure }
@ -198,21 +217,23 @@ 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
(* The new scope is the maximum of the two scopes. *)
let scope = max data1.scope data2.scope in
(* 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, data1.rank, data2.status, data2.rank with
| Generic, _, _, _
| _, _, Generic, _ ->
match (data1.status, data1.rank), (data2.status, data2.rank) with
| (Generic, _), ( _, _)
| (_, _), (Generic, _) ->
assert false
| Flexible, _, Flexible, _ ->
| (Flexible, _), (Flexible, _) ->
Flexible
| Rigid, _, Rigid, _ ->
| (Rigid, _), (Rigid, _) ->
(* One cannot unify two rigid variables. *)
raise InconsistentConjunction
| Rigid, rigid_rank, Flexible, _
| Flexible, _, Rigid, rigid_rank ->
| (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. *)
@ -221,7 +242,7 @@ module Data = struct
in
(* There is no need to preserve marks during unification. *)
let mark = dummy in
{ id; structure; rank; status; mark }
{ id; structure; rank; scope; status; mark }
let is_leaf data =
S.is_leaf data.structure
@ -268,7 +289,7 @@ exception Cycle =
propagation updates a child's rank, based on its father's rank; there is no
need for a child's rank to exceed its father's rank. (Indeed, the father
determines every child.) Upward propagation updates a father's rank, based
the ranks of all of its children: there is no need for a father's rank to
on the ranks of all of its children: there is no need for a father's rank to
exceed the maximum of its children's ranks. (Indeed, the children together
determine the father.) These operations are performed at generalization
time because it would be costly (and it is unnecessary) to perform them
@ -325,7 +346,7 @@ let register v r =
let flexible structure =
let r = state.young in
let status = Flexible in
let v = U.fresh (Data.make structure r status) in
let v = U.fresh (Data.make structure r base_scope status) in
register v r;
v
@ -333,7 +354,7 @@ let rigid () =
let r = state.young in
let structure = S.leaf in
let status = Rigid in
let v = U.fresh (Data.make structure r status) in
let v = U.fresh (Data.make structure r base_scope status) in
register v r;
v