Separate the status type in two.

This commit is contained in:
Olivier 2022-03-17 18:33:51 +01:00
parent e911ccbfa3
commit c2dfd17f68
3 changed files with 35 additions and 16 deletions

View File

@ -73,6 +73,24 @@ let base_rank =
type status = Rigid | Flexible | Generic
type rigidity = Rigid_ | Flexible_
let rigidity_of_status status =
match status with
| Generic ->
assert false
| Flexible ->
Flexible_
| Rigid ->
Rigid_
let status_of_rigidity rigidity =
match rigidity with
| Flexible_ ->
Flexible
| Rigid_ ->
Rigid
(* -------------------------------------------------------------------------- *)
(* We let each equivalence class carry a mutable integer mark. This [mark]
@ -180,22 +198,21 @@ module Data = struct
let rank = min data1.rank data2.rank in
let fail () = raise InconsistentConjunction in
(* If either variables is rigid, the conjunction is also rigid. *)
let status = match data1.status, data2.status with
| Generic, _ | _, Generic ->
(* The unifier never acts on generic variables. *)
assert false
| Flexible, Flexible ->
let status =
match rigidity_of_status data1.status,
rigidity_of_status data2.status with
| Flexible_, Flexible_ ->
Flexible
(* One cannot unify two rigid variables, *)
| Rigid, Rigid ->
| Rigid_, Rigid_ ->
fail ()
(* ... or lower the rank of a rigid variable, *)
| Rigid, Flexible ->
| Rigid_, Flexible_ ->
if (rank < data1.rank) then fail ();
(* ... or give it a non-leaf structure. *)
if not (S.is_leaf structure) then fail ();
Rigid
| Flexible, Rigid ->
| Flexible_, Rigid_ ->
if (rank < data2.rank) then fail ();
(* ... or give it a non-leaf structure. *)
if not (S.is_leaf structure) then fail ();
@ -304,11 +321,11 @@ let register v r =
(* When a fresh unification variable is created, it receives the current rank,
and it is immediately registered at this rank. *)
let fresh status structure =
let fresh rigidity structure =
let r = state.young in
if status = Rigid then
if rigidity = Rigid_ then
assert (S.is_leaf structure);
let v = U.fresh (Data.make structure r status) in
let v = U.fresh (Data.make structure r (status_of_rigidity rigidity)) in
register v r;
v
@ -718,7 +735,7 @@ let instantiate { generics; quantifiers; root } =
let data = get v in
assert (data.status = Generic);
data.mark <- i;
fresh Flexible S.leaf
fresh Flexible_ S.leaf
)
in

View File

@ -66,6 +66,8 @@ module Make
type status = Rigid | Flexible | Generic
type rigidity = Rigid_ | Flexible_
(* The literature defines a type scheme as a type (the ``body''), placed in
the scope of a list of universal quantifiers. Here, the quantifiers are
just variables (which definitely carry no structure), while the body is
@ -131,7 +133,7 @@ module Make
{!fresh} is permitted only if the stack is currently nonempty, that is,
if the current balance of calls to {!enter} versus calls to {!exit} is at
least one. *)
val fresh: status -> variable S.structure -> variable
val fresh: rigidity -> variable S.structure -> variable
(**[enter()] updates the current state by pushing a new frame onto the
current constraint context. It is invoked when the left-hand side of a

View File

@ -466,7 +466,7 @@ let rec solve : type a . range -> a co -> a on_sol =
unify range (uvar v) (uvar w);
On_sol (fun () -> ())
| CExist (v, s, c) ->
ignore (ubind v G.Flexible s);
ignore (ubind v G.Flexible_ s);
let result = solve range c in
uunbind v;
result
@ -492,11 +492,11 @@ let rec solve : type a . range -> a co -> a on_sol =
side of a [let] construct. *)
G.enter();
(* Register the rigid prefix [rs] with th generalization engine. *)
let _ = List.map (fun v -> ubind v G.Rigid None) rs in
let _ = List.map (fun v -> ubind v G.Rigid_ None) rs in
(* Register the variables [vs] with the generalization engine, just as
if they were existentially bound in [c1]. This is what they are,
basically, but they also serve as named entry points. *)
let vs = List.map (fun (_, v) -> ubind v G.Flexible None) xvs in
let vs = List.map (fun (_, v) -> ubind v G.Flexible_ None) xvs in
(* Solve the constraint [c1]. *)
let (On_sol r1) = solve range c1 in
(* Ask the generalization engine to perform an occurs check, to adjust