Hack not working yet.
This commit is contained in:
parent
02d4f16044
commit
59cb5ec7f9
|
@ -11,7 +11,7 @@
|
|||
|
||||
open Signatures
|
||||
|
||||
module Make (S : STRUCTURE_LEAF) = struct
|
||||
module Make (UserS : STRUCTURE_LEAF) = struct
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
|
@ -71,15 +71,7 @@ let base_rank =
|
|||
(* An active variable is intended to become generic some day. A generic
|
||||
variable never becomes active again. *)
|
||||
|
||||
type status = Rigid | Flexible | Generic
|
||||
|
||||
type rigidity = Rigid | Flexible
|
||||
|
||||
let status_of_rigidity : rigidity -> status = function
|
||||
| Flexible ->
|
||||
Flexible
|
||||
| Rigid ->
|
||||
Rigid
|
||||
type status = Active | Generic
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
|
@ -109,6 +101,70 @@ let fresh_mark : unit -> mark =
|
|||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* We define a [structure] type which is either abstract or a user-defined
|
||||
structure from the module S.
|
||||
Rigid variables have abstract strucutres.
|
||||
*)
|
||||
|
||||
module S = struct
|
||||
type 'a structure =
|
||||
| Abstract of int
|
||||
| User of 'a UserS.structure
|
||||
|
||||
exception InconsistentConjunction =
|
||||
UserS.InconsistentConjunction
|
||||
|
||||
let conjunction f s1 s2 =
|
||||
match s1, s2 with
|
||||
| Abstract n1, Abstract n2 ->
|
||||
if Int.equal n1 n2 then s1
|
||||
else raise InconsistentConjunction
|
||||
| User s1, User s2 ->
|
||||
User (UserS.conjunction f s1 s2)
|
||||
| Abstract _, User _
|
||||
| User _, Abstract _ ->
|
||||
raise InconsistentConjunction
|
||||
|
||||
let iter f s =
|
||||
match s with
|
||||
| Abstract _ ->
|
||||
()
|
||||
| User s ->
|
||||
UserS.iter f s
|
||||
|
||||
let fold f s acc =
|
||||
match s with
|
||||
| Abstract _ ->
|
||||
acc
|
||||
| User s ->
|
||||
UserS.fold f s acc
|
||||
|
||||
let map f s =
|
||||
match s with
|
||||
| Abstract n ->
|
||||
Abstract n
|
||||
| User s ->
|
||||
User (UserS.map f s)
|
||||
|
||||
let leaf = User (UserS.leaf)
|
||||
|
||||
let is_leaf s =
|
||||
match s with
|
||||
| Abstract _ ->
|
||||
false
|
||||
| User s ->
|
||||
UserS.is_leaf s
|
||||
|
||||
let is_abstract s =
|
||||
match s with
|
||||
| Abstract _ ->
|
||||
true
|
||||
| User _ ->
|
||||
false
|
||||
end
|
||||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* The type ['a data] groups all of the information that we associate with an
|
||||
equivalence class. *)
|
||||
|
||||
|
@ -136,7 +192,8 @@ exception VariableScopeEscape of int * int
|
|||
|
||||
let adjust_rank (data : 'a data) (k : rank) =
|
||||
if k < data.rank then
|
||||
if data.status = Flexible then
|
||||
(* TODO Faire avec data.scope au lieu de (S.is_abstract data.structure) *)
|
||||
if data.status = Active && not (S.is_abstract data.structure) then
|
||||
data.rank <- k
|
||||
else
|
||||
raise (VariableScopeEscape (k, data.rank))
|
||||
|
@ -202,19 +259,32 @@ module Data = struct
|
|||
| Generic, _
|
||||
| _, Generic ->
|
||||
assert false
|
||||
| Flexible, Flexible ->
|
||||
Flexible
|
||||
(* One cannot unify two rigid variables, *)
|
||||
| Rigid, Rigid ->
|
||||
fail ()
|
||||
| Rigid, Flexible ->
|
||||
(* ... or give it a non-leaf structure. *)
|
||||
if not (S.is_leaf structure) then fail ();
|
||||
Rigid
|
||||
| Flexible, Rigid ->
|
||||
(* ... or give it a non-leaf structure. *)
|
||||
if not (S.is_leaf structure) then fail ();
|
||||
Rigid
|
||||
| Active, Active ->
|
||||
(* TODO pas besoin de ça si on a les scopes. *)
|
||||
if S.is_abstract data1.structure then
|
||||
if S.is_abstract data2.structure then
|
||||
(* Rigid + Rigid *)
|
||||
fail ()
|
||||
else
|
||||
(* Rigid + Flexible *)
|
||||
begin
|
||||
if (rank < data1.rank) then fail ();
|
||||
(* ... or give it a non-leaf structure. *)
|
||||
if not (S.is_leaf structure) then fail ();
|
||||
Active
|
||||
end
|
||||
else
|
||||
if S.is_abstract data2.structure then
|
||||
(* Flexible + Rigid *)
|
||||
begin
|
||||
if (rank < data2.rank) then fail ();
|
||||
(* ... or give it a non-leaf structure. *)
|
||||
if not (S.is_leaf structure) then fail ();
|
||||
Active
|
||||
end
|
||||
else
|
||||
(* Flexible + Flexible *)
|
||||
Active
|
||||
in
|
||||
(* There is no need to preserve marks during unification. *)
|
||||
let mark = dummy in
|
||||
|
@ -223,8 +293,12 @@ module Data = struct
|
|||
let is_leaf data =
|
||||
S.is_leaf data.structure
|
||||
|
||||
let project data =
|
||||
data.structure
|
||||
let project (data : 'a structure) =
|
||||
match data.structure with
|
||||
| S.Abstract _ ->
|
||||
assert false
|
||||
| S.User s ->
|
||||
s
|
||||
|
||||
end
|
||||
|
||||
|
@ -319,11 +393,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 (rigidity : rigidity) structure =
|
||||
let fresh ~(rigidity:bool) structure =
|
||||
let r = state.young in
|
||||
if rigidity = Rigid then
|
||||
if rigidity then
|
||||
assert (S.is_leaf structure);
|
||||
let v = U.fresh (Data.make structure r (status_of_rigidity rigidity)) in
|
||||
let v = U.fresh (Data.make structure r Active) in
|
||||
register v r;
|
||||
v
|
||||
|
||||
|
@ -733,7 +807,7 @@ let instantiate { generics; quantifiers; root } =
|
|||
let data = get v in
|
||||
assert (data.status = Generic);
|
||||
data.mark <- i;
|
||||
fresh Flexible S.leaf
|
||||
fresh ~rigidity:false S.leaf
|
||||
)
|
||||
in
|
||||
|
||||
|
@ -766,10 +840,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
|
||||
|
|
|
@ -22,9 +22,15 @@ open Signatures
|
|||
operations that allow constructing, inspecting, and instantiating
|
||||
schemes. *)
|
||||
module Make
|
||||
(S : sig (** @inline *) include STRUCTURE_LEAF end)
|
||||
(UserS : sig (** @inline *) include STRUCTURE_LEAF end)
|
||||
: sig
|
||||
|
||||
module S : sig
|
||||
type 'a structure =
|
||||
| Abstract of int
|
||||
| User of 'a UserS.structure
|
||||
end
|
||||
|
||||
(** {2 Unification} *)
|
||||
|
||||
(**This submodule defines the data attached with a unification variable. *)
|
||||
|
@ -64,9 +70,7 @@ module Make
|
|||
variables/types that cannot escape their scope, such as local
|
||||
abstract types or existential unpacking. *)
|
||||
|
||||
type status = Rigid | Flexible | Generic
|
||||
|
||||
type rigidity = Rigid | Flexible
|
||||
type status = Active | Generic
|
||||
|
||||
(* 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
|
||||
|
@ -133,7 +137,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: rigidity -> variable S.structure -> variable
|
||||
val fresh: rigidity:bool -> 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
|
||||
|
|
|
@ -304,9 +304,9 @@ module UVar = struct
|
|||
(* This should never happen. *)
|
||||
Printf.ksprintf failwith "Unbound variable %d" v
|
||||
|
||||
let ubind (v : variable) rigidity so =
|
||||
let ubind (v : variable) ~(rigidity : bool) so =
|
||||
assert (not (VarTable.mem table v));
|
||||
let uv = G.fresh rigidity (OS.map uvar so) in
|
||||
let uv = G.fresh ~rigidity (G.S.User (OS.map uvar so)) in
|
||||
VarTable.add table v uv;
|
||||
uv
|
||||
|
||||
|
@ -473,7 +473,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 ~rigidity:false s);
|
||||
let result = solve range c in
|
||||
uunbind v;
|
||||
result
|
||||
|
@ -499,11 +499,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 urs = List.map (fun v -> ubind v G.Rigid None) rs in
|
||||
let urs = List.map (fun v -> ubind v ~rigidity:true 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 ~rigidity:false 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