Implementing O.abstract in the client.

This commit is contained in:
Olivier 2023-04-05 14:11:48 +02:00
parent ec32370b04
commit 1546c05619
6 changed files with 75 additions and 36 deletions

View File

@ -13,14 +13,10 @@ module S =
structure as follows. *)
module O = struct
include ML2F
type tyvar =
int
(* See also [fresh_tyvar] *)
let inject n =
2 * n
Flexible n
type 'a structure = 'a S.structure
let pprint = S.pprint
@ -29,7 +25,10 @@ module O = struct
F.nominal_type
let variable x =
F.TyVar x
F.TyVar (id_of_tyvar x)
let abstract id =
Abstract id
let structure t =
match t with
@ -43,7 +42,7 @@ module O = struct
F.TyEq (t1, t2)
let mu x t =
F.TyMu (x, t)
F.TyMu (id_of_tyvar x, t)
end
@ -173,7 +172,7 @@ let coerce ~loc (vs1 : O.tyvar list) (vs2 : O.tyvar list) : coercion =
(* Assume the term [t] has type [forall vs1, _]. *)
fun t ->
(* Introduce the desired quantifiers. *)
List.fold_right (ftyabs1 ~loc) vs2 (
List.fold_right (ftyabs1 ~loc) (List.map O.id_of_tyvar vs2) (
(* Now, specialize the term [t]. For each member of [vs1],
we must provide a suitable instantiation. *)
F.ftyapp ~loc t (
@ -182,7 +181,7 @@ let coerce ~loc (vs1 : O.tyvar list) (vs2 : O.tyvar list) : coercion =
otherwise we get rid of it (by instantiating it with an arbitrary
closed type, say [bottom]). *)
let suitable (v : O.tyvar) : O.ty =
if List.mem v vs2 then F.TyVar v else bottom
if List.mem v vs2 then F.TyVar (O.id_of_tyvar v) else bottom
(* TEMPORARY need an efficient membership test in [vs2] *)
in
List.map suitable vs1
@ -399,7 +398,7 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
that, if the lists [a] and [b] happen to be equal, no extra code is
produced. *)
let sch tyvars =
List.fold_right (fun alpha sch -> F.TyForall (alpha, sch)) tyvars ty in
List.fold_right (fun alpha sch -> F.TyForall (alpha, sch)) (List.map O.id_of_tyvar tyvars) ty in
let rec_ = match rec_ with
| ML.Recursive -> F.Recursive
| ML.Non_recursive -> F.Non_recursive
@ -432,11 +431,12 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
fun (x : a) -> loop x
*)
flet ~loc (x, ty,
F.ftyapp ~loc (F.Var (loc, x)) (List.map (fun v -> F.TyVar v) a),
F.ftyapp ~loc (F.Var (loc, x))
(List.map (fun v -> F.TyVar (O.id_of_tyvar v)) a),
t')
in
F.Let (loc, rec_, x, sch a,
F.ftyabs ~loc a t'',
F.ftyabs ~loc (List.map O.id_of_tyvar a) t'',
flet ~loc (x, sch b, coerce ~loc a b (F.Var (loc, x)),
u'))
@ -474,7 +474,8 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
in t'
) (instance x w)
in
F.ftyapp ~loc (coerce ~loc alphas betas (F.ftyabs ~loc alphas t')) tys
F.ftyapp ~loc (coerce ~loc alphas betas
(F.ftyabs ~loc (List.map O.id_of_tyvar alphas) t')) tys
| ML.Some_ (_, tyvars, t) ->
let on_tyvar alpha k =
@ -728,7 +729,7 @@ let hastype (env : ML.datatype_env) (t : ML.term) : F.nominal_term co =
let+ (vs, t) =
correlate loc (let0 (exist (hastype env t))) in
(* [vs] are the binders that we must introduce *)
F.ftyabs ~loc vs t
F.ftyabs ~loc (List.map O.id_of_tyvar vs) t
let hastype_with_hook ~(hook : unit -> 'a) (env : ML.datatype_env) (t : ML.term)
: ('a * F.nominal_term) co

View File

@ -1,10 +1,28 @@
(* Translation from ML types to F types *)
let fresh_tyvar =
let cpt = ref 0 in
type tyvar =
| User of int
| Flexible of int (* TODO : find a better type than int (?) *)
| Abstract of int (* TODO : find a better type than int (?) *)
(* We generate odd number for the user and even number for the solver *)
fun () -> incr cpt; 2 * !cpt + 1
(* We use a hash-table as a redirection from type variables obtained by
the solver to unique System F type variable identifiers. *)
let table_id : (tyvar, int) Hashtbl.t =
Hashtbl.create 256
let gensym =
Inferno.Utils.gensym ()
let id_of_tyvar v =
try
Hashtbl.find table_id v
with Not_found ->
let fresh_id = gensym () in
Hashtbl.add table_id v fresh_id;
fresh_id
let fresh_tyvar () =
id_of_tyvar (User (gensym ()))
(* Translation of ML datatype environment into System F datatype environment. *)

View File

@ -1323,6 +1323,9 @@ let generalize generation : variable list =
(* -------------------------------------------------------------------------- *)
type variable_binding =
variable * (abstract_id option)
(* We are in charge of constructing and instantiating schemes, that is, graph
fragments that contain generic (universally quantified, to-be-copied)
variables and can have outgoing edges towards active (not-to-be-copied)
@ -1355,7 +1358,7 @@ type scheme = {
this list is chosen in an arbitrary way, and thereafter matters: it is
exposed to the user via the functions [quantifiers] and [instantiate],
which must agree on this order. *)
quantifiers : variable list;
quantifiers : variable_binding list;
}
@ -1421,7 +1424,8 @@ let schemify (root : variable) : scheme =
let generics = !accu in
(* Compute [quantifiers]. *)
let has_no_structure v = Option.is_none (get v).structure in
let quantifiers = List.filter has_no_structure generics in
let quantifiers = List.filter has_no_structure generics
|> List.map (fun v -> (v,None)) in
(* Done. *)
let generics = Array.of_list generics in
{ generics; quantifiers; root }
@ -1469,6 +1473,16 @@ let exit ~rectypes abstract_ids roots =
any of these schemes. *)
let quantifiers = generalize generation in
let get_ids v =
match (get v).structure with
| Some (Abs.Abstract id) ->
v, Some id
| Some (Abs.User _) | None ->
v, None
in
let quantifiers = List.map get_ids quantifiers in
(* For every root in the list [roots], build a scheme. *)
let schemes = List.map schemify roots in
@ -1525,7 +1539,7 @@ let instantiate { generics; quantifiers; root } =
) generics mapping;
(* Return the (instantiated) quantifiers and root. *)
List.map copy quantifiers, copy root
List.map copy (List.map fst quantifiers), copy root
(* -------------------------------------------------------------------------- *)

View File

@ -70,6 +70,9 @@ module Make
type abstract_id =
int
type variable_binding =
variable * (abstract_id option)
val is_consistent_env: unit -> bool
exception InconsistentContext
@ -92,7 +95,7 @@ module Make
(**[quantifiers σ] returns the quantifiers of the scheme [σ], in an arbitrary
fixed order. The quantifiers are {i generic} unifier variables. They carry
no structure. *)
val quantifiers: scheme -> variable list
val quantifiers: scheme -> variable_binding list
(**[body σ] returns the body of the scheme [σ]. It is represented as a
variable, that is, a vertex in the unification graph. *)
@ -198,7 +201,7 @@ module Make
The pair [(vs, schemes)] is returned. *)
val exit: rectypes:bool -> abstract_id list -> variable list
-> variable list * scheme list
-> (variable * abstract_id option) list * scheme list
val exit_equality: rectypes:bool -> unit

View File

@ -357,6 +357,8 @@ module type OUTPUT = sig
type. *)
val variable: tyvar -> ty
val abstract: int -> tyvar
(**[structure s] turns [s], a structure whose children are decoded types,
into a decoded type. *)
val structure: ty structure -> ty

View File

@ -393,12 +393,16 @@ end (* UVar *)
(* [decode_variable] decodes a variable, which must have
leaf structure. The decoded variable is determined by the unique identity
of the variable [v]. *)
let decode_variable (v : U.variable) : O.tyvar =
let decode_variable_binding ((v,id_opt) : U.variable * abstract option)
: O.tyvar =
let data = U.get v in
match U.project data with
| Some (ABS.User _) -> assert false
| None -> O.inject (U.id data)
| Some (ABS.Abstract _id) -> assert false (*DecodeTable.find decode_table id*)
| None -> begin match id_opt with
| Some id -> O.abstract id
| None -> O.inject (U.id data)
end
| Some (ABS.Abstract _id) -> assert false
(* The module [D] is used to decode non-leaf structures *)
module D =
@ -410,8 +414,8 @@ module D =
match U.project s with
| None ->
O.variable (O.inject (U.id s))
| Some (ABS.Abstract _id) ->
failwith "todo"
| Some (ABS.Abstract id) ->
O.variable (O.abstract id)
| Some (ABS.User s) ->
O.structure s
end)
@ -425,7 +429,7 @@ let decode : U.variable -> O.ty =
if rectypes then D.new_cyclic_decoder() else D.new_acyclic_decoder()
let decode_scheme (s : G.scheme) : scheme =
List.map decode_variable (G.quantifiers s),
List.map decode_variable_binding (G.quantifiers s),
decode (G.body s)
(* -------------------------------------------------------------------------- *)
@ -600,18 +604,15 @@ let rec solve : type a . loc:loc option -> a co -> a on_sol =
our entry points. The generalization engine also produces a list
[gammas] of the young variables that should be universally
quantified here. *)
let gammas, ss = exit ~loc ~rectypes rs uvs in
(* All rigid variables of [rs] must be generalizable. This assertion
may be costly and should be removed or disabled in the future. *)
(* assert (urs |> List.for_all (fun r -> List.exists (U.eq r) gammas)); *)
List.iter uunbind vs (* (vs @ vrs) *) ;
let variable_bindings, ss = exit ~loc ~rectypes rs uvs in
List.iter uunbind vs ;
(* Extend the environment [env]. *)
List.iter2 Env.bind xs ss;
(* Proceed to solve [c2] in the extended environment. *)
let (On_sol r2) = solve ~loc c2 in
List.iter Env.unbind xs;
On_sol (fun () ->
List.map decode_variable gammas,
List.map decode_variable_binding variable_bindings,
List.map decode_scheme ss,
r1(),
r2()