Add a scope type in the data.

This commit is contained in:
Olivier 2023-02-10 15:37:36 +01:00
parent 5f9930b04b
commit ec46543398
6 changed files with 48 additions and 27 deletions

View File

@ -103,7 +103,7 @@ type error =
| Unify of F.nominal_type * F.nominal_type
| Cycle of F.nominal_type
| VariableConflict of ML.tevar
| VariableScopeEscape
| VariableScopeEscape of int * int
| Unsupported of string
exception Error of Utils.loc * error
@ -743,7 +743,8 @@ let translate_with_hook ~hook ~rectypes env t =
| Solver.Unbound x -> Unbound (get_tevar x)
| Solver.Unify (t1, t2) -> Unify (t1, t2)
| Solver.Cycle (ty) -> Cycle (ty)
| Solver.VariableScopeEscape -> VariableScopeEscape
| Solver.VariableScopeEscape (rank, scope) ->
VariableScopeEscape (rank, scope)
in
raise (Error (loc, error))
@ -768,7 +769,7 @@ let emit_error loc (error : error) =
emit_type ty1;
Printf.printf "and the type:\n";
emit_type ty2;
| VariableScopeEscape ->
| VariableScopeEscape (_, _) ->
Printf.printf
"A rigid variable escapes its scope.\n"
| VariableConflict (x) ->

View File

@ -3,7 +3,7 @@ type error =
| Unify of F.nominal_type * F.nominal_type
| Cycle of F.nominal_type
| VariableConflict of ML.tevar
| VariableScopeEscape
| VariableScopeEscape of int * int
| Unsupported of string
exception Error of Utils.loc * error

View File

@ -50,6 +50,8 @@ type rank =
let base_rank =
0
let base_scope =
0
(* -------------------------------------------------------------------------- *)
@ -122,6 +124,7 @@ type 'a data = {
id: id;
mutable structure: 'a S.structure;
mutable rank: rank;
mutable scope: rank;
mutable status: status;
mutable mark: mark;
}
@ -139,7 +142,7 @@ let pprint elem data =
At present, this exception does not carry any data; we do not yet know how
to produce a good error message in this situation. *)
exception VariableScopeEscape
exception VariableScopeEscape of { rank: rank; scope: rank }
(* If [data.status] is flexible, then [adjust_rank data k] is equivalent
to [data.rank <- min k data.rank]. If [data.status] is rigid, then it
@ -152,7 +155,20 @@ let adjust_rank (data : 'a data) (k : rank) =
if data.status = Flexible then
data.rank <- k
else
raise VariableScopeEscape
raise (VariableScopeEscape { rank=data.rank; scope=data.scope })
(* 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 : rank) =
assert (data.status <> Generic);
if s > data.scope then
if s <= data.rank then
data.scope <- s
else
raise (VariableScopeEscape { rank=data.rank; scope=data.scope })
(* The module [Data] is meant to be an argument for [Unifier.Make]. *)
@ -169,10 +185,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 }
@ -207,6 +223,8 @@ 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. *)
@ -223,14 +241,14 @@ module Data = struct
| Rigid, rigid_rank, Flexible, _
| Flexible, _, Rigid, rigid_rank ->
(* One cannot lower the rank of a rigid variable. *)
if rank < rigid_rank then raise VariableScopeEscape;
if rank < rigid_rank then raise (VariableScopeEscape { rank; scope });
(* One cannot assign some structure to a rigid variable. *)
if Option.is_some structure then raise InconsistentConjunction;
Rigid
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 =
Option.is_none data.structure
@ -331,19 +349,21 @@ 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 flexible structure =
let r = state.young in
let status = Flexible in
let v = U.fresh (Data.make structure r status) in
register v r;
let fresh_variable structure ~rank ~scope status =
let v = U.fresh (Data.make structure ~rank ~scope status) in
register v rank;
v
let flexible structure =
let rank = state.young in
let scope = base_scope in
fresh_variable structure ~rank ~scope Flexible
let rigid () =
let r = state.young in
let status = Rigid in
let v = U.fresh (Data.make None r status) in
register v r;
v
let rank = state.young in
let scope = rank in
let structure = None in
fresh_variable structure ~rank ~scope Rigid
(* -------------------------------------------------------------------------- *)

View File

@ -141,7 +141,7 @@ module Make
exception Cycle of variable
(**This exception is raised by {!exit}. *)
exception VariableScopeEscape
exception VariableScopeEscape of { rank: int; scope: int }
(**[exit ~rectypes roots] updates the current state by popping a frame off
the current constraint context. It is invoked when the left-hand side of

View File

@ -150,7 +150,7 @@ type _ co =
| Unbound of tevar
| Unify of O.ty * O.ty
| Cycle of O.ty
| VariableScopeEscape
| VariableScopeEscape of int * int
exception Error of loc option * error
@ -408,8 +408,8 @@ let unify ~loc v1 v2 =
| U.Unify (v1, v2) ->
let decode = D.new_cyclic_decoder() in
raise (Error (loc, Unify (decode v1, decode v2)))
| G.VariableScopeEscape ->
raise (Error (loc, VariableScopeEscape))
| G.VariableScopeEscape { rank; scope } ->
raise (Error (loc, VariableScopeEscape (rank, scope)))
let exit ~loc ~rectypes vs =
try
@ -418,8 +418,8 @@ let exit ~loc ~rectypes vs =
| G.Cycle v ->
let decode = D.new_cyclic_decoder() in
raise (Error (loc, Cycle (decode v)))
| G.VariableScopeEscape ->
raise (Error (loc, VariableScopeEscape))
| G.VariableScopeEscape { rank; scope } ->
raise (Error (loc, VariableScopeEscape (rank, scope)))
(* -------------------------------------------------------------------------- *)

View File

@ -419,7 +419,7 @@ module Make
[false]. The error carries a decoded type, which is
a recursive type: that is, this type involves a μ binder. *)
| VariableScopeEscape
| VariableScopeEscape of int * int
(**A rigid variable escapes its scope, that is, roughly
speaking, one attempts to unify a rigid variable with a more
ancient flexible variable. For example, attempting to solve