Generalization uses abstract structures for rigid variables.

This commit is contained in:
Olivier 2023-02-10 15:48:59 +01:00
parent 05b3d73873
commit d59a61f1cb
3 changed files with 81 additions and 75 deletions

View File

@ -11,7 +11,7 @@
open Signatures
module Make (S : GSTRUCTURE_OPT) = struct
module Make (S : GSTRUCTURE_ABS_OPT) = struct
(* -------------------------------------------------------------------------- *)
@ -76,8 +76,7 @@ let base_scope =
is an error. *)
type status =
| Rigid
| Flexible
| Active
| Generic
(* -------------------------------------------------------------------------- *)
@ -138,36 +137,28 @@ let pprint elem data =
(* [status] and [mark] are currently not printed. *)
(* This exception is raised when a rigid variable escapes its scope, that is,
when it is unified with (or becomes a child of) a variable of lesser rank.
At present, this exception does not carry any data; we do not yet know how
to produce a good error message in this situation. *)
when it is unified with (or becomes a child of) a variable of lesser rank. *)
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
causes an error. Indeed, the rank of a rigid variable is fixed; it can
never decrease. *)
(* The rank of variable must always be above its scope. *)
let check_rank_scope (data : 'a data) =
if data.rank < data.scope then
raise (VariableScopeEscape {rank = data.rank; scope = data.scope})
let adjust_rank (data : 'a data) (k : rank) =
assert (data.status <> Generic);
if k < data.rank then
if data.status = Flexible then
data.rank <- k
else
raise (VariableScopeEscape { rank=data.rank; scope=data.scope })
assert (data.status = Active);
if k < data.rank then begin
data.rank <- k;
check_rank_scope data
end
(* 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 })
let adjust_scope (data : 'a data) (s : rank) =
assert (data.status = Active);
if s > data.scope then begin
data.scope <- s;
check_rank_scope data
end
(* The module [Data] is meant to be an argument for [Unifier.Make]. *)
@ -217,6 +208,8 @@ module Data = struct
fresh identifier. Here, we keep an arbitrary identifier. *)
let conjunction equate data1 data2 =
assert (data1.status = Active);
assert (data2.status = Active);
let id = data1.id in
(* The new structural constraint is the logical conjunction of the two
structural constraints. *)
@ -225,33 +218,17 @@ module Data = struct
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, _ ->
assert false
| Flexible, _, Flexible, _ ->
Flexible
| 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 { rank; scope });
(* One cannot assign some structure to a rigid variable. *)
if Option.is_some structure then raise InconsistentConjunction;
Rigid
in
if rank < scope then
raise (VariableScopeEscape { rank; scope });
let status = Active in
(* There is no need to preserve marks during unification. *)
let mark = dummy in
{ id; structure; rank; scope; status; mark }
let is_leaf data =
Option.is_none data.structure
match data.structure with
| None | Some (S.S.Abstract _) -> true
| Some (S.S.User _) -> false
let project data =
data.structure
@ -349,21 +326,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 fresh_variable structure ~rank ~scope status =
let v = U.fresh (Data.make structure ~rank ~scope status) in
let fresh_variable structure ~rank ~scope =
let v = U.fresh (Data.make structure ~rank ~scope Active) in
register v rank;
v
let flexible structure =
let rank = state.young in
let scope = base_scope in
fresh_variable structure ~rank ~scope Flexible
fresh_variable structure ~rank ~scope
let rigid () =
let rank = state.young in
let scope = rank in
let structure = None in
fresh_variable structure ~rank ~scope Rigid
let structure = Some (S.S.fresh_abstract ()) in
fresh_variable structure ~rank ~scope
(* -------------------------------------------------------------------------- *)
@ -511,7 +488,7 @@ let update_ranks generation =
(* A postcondition of [traverse v] is [U.rank v <= k]. (This is downward
propagation.) [traverse v] returns the updated rank of [v]. *)
let rec traverse v : rank =
let rec traverse v =
let data = get v in
(* The downward propagation phase can never reach a generic variable.
Indeed, a generic variable is never a child of an active variable. *)
@ -538,21 +515,41 @@ let update_ranks generation =
it must now be [k]. *)
assert (data.rank = k);
(* If [v] carries some structure, ... *)
if not (Data.is_leaf data) then
if not (Data.is_leaf data) then begin
(* Update the rank and scope of all children. *)
Data.iter traverse data;
(* On the way back up, compute the maximum of their
scopes, and use it to adjust [v]'s scope.
Note: we are not sure that this propagation is strictly
necessary. We must detect all cases where a variable
rank goes below its scope, but it may be enough to
propagate ranks "down" and never propagate scopes "up".
However propagating scopes in this way follows more
closely the intended meaning of scopes as "lexical
region of vadility / well-formedness": if a variable
[v] is only valid within scope 10, then a variable
representing the type (int -> v) arguably is also only
valid within scope 10. *)
adjust_scope data (
Data.fold (fun child accu ->
max (get child).scope accu
) data data.scope
);
(* ... traverse [v]'s children; on the way back up, compute the
maximum of their ranks, and use it to adjust [v]'s rank. *)
(* As an optimization we also adjust [v]'s rank, which needs
not be higher than its children ranks and its scope. *)
adjust_rank data (
Data.fold (fun child accu ->
max (traverse child) accu
) data base_rank (* the base rank is neutral for [max] *)
max (get child).rank accu
) data data.scope
)
end
end
end;
(* In allowed cases, return [v]'s final rank. *)
data.rank
end
in
let traverse v = ignore (traverse v) in
List.iter traverse generation.by_rank.(k)
done
@ -595,6 +592,11 @@ let generalize generation : variable list =
(* Make this variable generic, ... *)
data.status <- Generic;
(* ... and keep it in the result list, if it has no structure. *)
begin match data.structure with
| Some (S.S.Abstract _) ->
data.structure <- None
| Some (S.S.User _) | None -> ()
end;
Data.is_leaf data
end
end
@ -804,10 +806,8 @@ let pp_status ppf s =
match s with
| Generic ->
Printf.fprintf ppf "generic"
| Flexible ->
Printf.fprintf ppf "flexible"
| Rigid ->
Printf.fprintf ppf "rigid"
| Active ->
Printf.fprintf ppf "active"
let show_variable v =
let data = get v in

View File

@ -22,7 +22,7 @@ open Signatures
operations that allow constructing, inspecting, and instantiating
schemes. *)
module Make
(S : sig (** @inline *) include GSTRUCTURE_OPT end)
(S : sig (** @inline *) include GSTRUCTURE_ABS_OPT end)
: sig
(** {2 Unification} *)

View File

@ -277,7 +277,11 @@ open C
(* TODO explain why we use [Structure.Option] *)
module OS = Structure.Option(S)
module ABS = Structure.Abstract(S)
module OS = struct
include Structure.Option(ABS)
module S = ABS
end
module G = Generalization.Make(OS)
module U = G.U
@ -326,9 +330,9 @@ module UVar = struct
(* This should never happen. *)
Printf.ksprintf failwith "Unbound variable %d" v
let flexible (v : variable) so =
let flexible (v : variable) (so : variable S.structure option) : U.variable =
assert (not (VarTable.mem table v));
let uv = G.flexible (OS.map uvar so) in
let uv = G.flexible (Option.map (fun s -> ABS.User (S.map uvar s)) so) in
VarTable.add table v uv;
uv
@ -366,8 +370,9 @@ end (* UVar *)
let decode_variable (v : U.variable) : O.tyvar =
let data = U.get v in
match G.Data.project data with
| Some _ -> assert false
| None -> O.inject (G.Data.id data)
| Some (ABS.User _) -> assert false
| None
| Some (ABS.Abstract _) -> O.inject (G.Data.id data)
(* The module [D] is used to decode non-leaf structures *)
module D =
@ -377,8 +382,9 @@ module D =
let structure (s : O.ty U.structure) : O.ty =
match G.Data.project s with
| None -> O.variable (O.inject (G.Data.id s))
| Some s -> O.structure s
| None
| Some (ABS.Abstract _) -> O.variable (O.inject (G.Data.id s))
| Some (ABS.User s) -> O.structure s
end)
(* -------------------------------------------------------------------------- *)