Compare commits
1 Commits
master
...
rigid-vari
Author | SHA1 | Date |
---|---|---|
Olivier | c2dfd17f68 |
|
@ -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
|
||||
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
|
Loading…
Reference in New Issue