Remove deprecated functions.
This commit is contained in:
parent
e4230c86a9
commit
972f079550
|
@ -1,6 +1,3 @@
|
|||
|
||||
(* -------------------------------------------------------------------------- *)
|
||||
|
||||
(* Translation from ML types to F types *)
|
||||
|
||||
let fresh_tyvar =
|
||||
|
@ -20,87 +17,7 @@ let fresh_tyvar =
|
|||
calling translate_type_expr with parameter "int"
|
||||
gives the translation
|
||||
"mu tau. [{} + {int * tau}]"
|
||||
*)
|
||||
let rec translate_type_expr
|
||||
(env : ML.datatype_env)
|
||||
(params : F.nominal_type list)
|
||||
(type_id : Datatype.tyconstr_id)
|
||||
: F.nominal_type =
|
||||
let desc = Datatype.Env.find_decl env type_id in
|
||||
let tau = fresh_tyvar () in
|
||||
let rec_occur = F.TyVar tau in
|
||||
let tys = translate_typedecl env params desc rec_occur in
|
||||
F.TyMu (tau, F.TySum tys)
|
||||
|
||||
(* Takes a ML type constructor such as "('a,'b) t",
|
||||
a System F type for each parameter ("foo", "bar"),
|
||||
and returns a list of System F types for the arguments
|
||||
of the constructors of "(foo,bar) t".
|
||||
|
||||
For example, for the ML declaration
|
||||
"type 'a list = Nil of () | Cons of ('a * 'a list)"
|
||||
calling translate_type_expr with parameter "int"
|
||||
gives a list containing the constructor types
|
||||
"{}"
|
||||
and
|
||||
"{int * mu tau. [{} + {int * tau}]}".
|
||||
*)
|
||||
and translate_constr_types
|
||||
(env : ML.datatype_env)
|
||||
(params : F.nominal_type list)
|
||||
(type_id : Datatype.tyconstr_id)
|
||||
: F.nominal_type list =
|
||||
let desc = Datatype.Env.find_decl env type_id in
|
||||
let rec_occur = translate_type_expr env params type_id in
|
||||
translate_typedecl env params desc rec_occur
|
||||
|
||||
(* Here [rec_occur] is the value provide when we encounter an
|
||||
occurence of the name of the type we translate *)
|
||||
and translate_type
|
||||
(env : ML.datatype_env)
|
||||
(params : (string * F.nominal_type) list)
|
||||
(rec_occur : F.nominal_type)
|
||||
(name_self : Datatype.tyconstr_id)
|
||||
(ty : ML.typ)
|
||||
: F.nominal_type =
|
||||
let rec tt (ty : ML.typ) : F.nominal_type =
|
||||
match ty with
|
||||
| ML.TyVar x ->
|
||||
List.assoc x params
|
||||
|
||||
| ML.TyArrow (ty1, ty2) ->
|
||||
F.TyArrow (tt ty1, tt ty2)
|
||||
|
||||
| ML.TyProduct tys ->
|
||||
F.TyProduct (List.map tt tys)
|
||||
|
||||
| ML.TyConstr (tid, tys) ->
|
||||
if tid = name_self then begin
|
||||
let desc = Datatype.Env.find_decl env name_self in
|
||||
|
||||
(* This assert should hold as long as we only treat
|
||||
* regular recursion, that is types in which each type parameters
|
||||
* is instantiated with only one type *)
|
||||
assert (tys = List.map (fun x -> ML.TyVar x) desc.Datatype.type_params);
|
||||
rec_occur
|
||||
end
|
||||
else
|
||||
translate_type_expr env (List.map tt tys) tid
|
||||
in
|
||||
tt ty
|
||||
|
||||
and translate_typedecl
|
||||
(env : ML.datatype_env)
|
||||
(params : F.nominal_type list)
|
||||
(desc : (string, ML.typ) Datatype.decl)
|
||||
(rec_occur : F.nominal_type)
|
||||
: F.nominal_type list =
|
||||
let params = List.combine Datatype.(desc.type_params) params in
|
||||
let tys =
|
||||
List.map (fun ldescr -> Datatype.(ldescr.arg_type)) Datatype.(desc.labels_descr)
|
||||
|> List.map (translate_type env params rec_occur Datatype.(desc.name))
|
||||
in
|
||||
tys
|
||||
*)
|
||||
|
||||
(* Translation of ML datatype environment into System F datatype environment. *)
|
||||
|
||||
|
|
Loading…
Reference in New Issue