Compare commits

..

10 Commits

Author SHA1 Message Date
Olivier 19b1d4a6cf Remove unused equality check and change comments. 2022-11-03 16:32:04 +01:00
Olivier aed5c4d0fd Add tests. 2022-11-03 16:32:04 +01:00
Olivier 647587109a Add Refl / Use in System F.
The term Refl is a proof of a type equality TyEq(ty1,ty2) and Use is a construct that introduce a type equality in the typing context.
2022-11-03 16:32:04 +01:00
Olivier e48962cd4a Add break in printing of annotations. 2022-11-03 16:32:04 +01:00
Olivier 47ec0af486 Smart constructors in TestF.ml. 2022-11-03 16:32:04 +01:00
Olivier 0d65e0621f Equality between types always uses graph translation. 2022-11-03 16:32:04 +01:00
Olivier 382c75e51c Define type equalities in [Structure.ml].
This will be useful when we translate System F terms to graphs (a "structure" node of the graph will be represented by a Structure.structure).
2022-11-03 16:28:52 +01:00
Olivier 1ae9154c52 Remove unused type declaration. 2022-09-07 11:15:04 +02:00
Olivier 1e797805df Add absurd in F. 2022-09-07 11:01:06 +02:00
Olivier 685c59ec42 Add type equality in F. 2022-09-07 10:41:02 +02:00
25 changed files with 1107 additions and 508 deletions

View File

@ -1,12 +1,6 @@
# Changes
## 2022/06/03
* Support for rigid variables, that is, variables that cannot be unified with
other rigid variables or with older flexible variables. These variables are
introduced by the new combinators `letr1` and `letrn`. The exception
`VariableScopeEscape`, which is raised when a rigid variable escapes its
scope, is also new.
## 2022/02/XX
* **Incompatible** changes to the solver's high-level API.
The module `Inferno.SolverHi` has been renamed to `Inferno.Solver`.

View File

@ -27,6 +27,7 @@ type ('a, 'b) typ =
| TyForall of 'b * ('a, 'b) typ
| TyMu of 'b * ('a, 'b) typ
| TyConstr of ('a, 'b) datatype
| TyEq of ('a, 'b) typ * ('a, 'b) typ
and ('a, 'b) datatype = Datatype.tyconstr_id * ('a, 'b) typ list
@ -69,6 +70,9 @@ type ('a, 'b) term =
| LetProd of range * tevar list * ('a, 'b) term * ('a, 'b) term
| Variant of range * Datatype.label_id * ('a, 'b) datatype * ('a,'b) term
| Match of range * ('a,'b) typ * ('a,'b) term * ('a,'b) branch list
| Absurd of range * ('a,'b) typ
| Refl of range * ('a,'b) typ
| Use of range * ('a,'b) term * ('a,'b) term
and ('a,'b) branch = ('a,'b) pattern * ('a,'b) term
@ -149,7 +153,10 @@ module TypeInType : DeBruijn.TRAVERSE
let env, x = extend env x in
let ty1' = trav env ty1 in
TyMu (x, ty1')
| TyEq (ty1, ty2) ->
let ty1' = trav env ty1 in
let ty2' = trav env ty2 in
TyEq (ty1', ty2')
end
(* -------------------------------------------------------------------------- *)
@ -219,6 +226,16 @@ module TypeInTerm : DeBruijn.TRAVERSE
let t' = trav env t
and brs' = List.map (traverse_branch lookup extend env) brs in
Match (pos, ty', t', brs')
| Absurd (pos, ty) ->
let ty' = TypeInType.traverse lookup extend env ty in
Absurd (pos, ty')
| Refl (pos, ty) ->
let ty' = TypeInType.traverse lookup extend env ty in
Refl (pos, ty')
| Use (pos, t, u) ->
let t' = trav env t in
let u' = trav env u in
Use (pos, t', u')
and traverse_datatype lookup extend env (tid, tyargs) =
(tid, List.map (TypeInType.traverse lookup extend env) tyargs)

View File

@ -26,6 +26,7 @@ type ('a, 'b) typ =
| TyForall of 'b * ('a, 'b) typ
| TyMu of 'b * ('a, 'b) typ
| TyConstr of ('a, 'b) datatype
| TyEq of ('a, 'b) typ * ('a, 'b) typ
and ('a, 'b) datatype = Datatype.tyconstr_id * ('a, 'b) typ list
@ -72,6 +73,9 @@ type ('a, 'b) term =
| LetProd of range * tevar list * ('a, 'b) term * ('a, 'b) term
| Variant of range * Datatype.label_id * ('a, 'b) datatype * ('a,'b) term
| Match of range * ('a,'b) typ * ('a,'b) term * ('a,'b) branch list
| Absurd of range * ('a,'b) typ
| Refl of range * ('a,'b) typ
| Use of range * ('a,'b) term * ('a,'b) term
and ('a,'b) branch = ('a,'b) pattern * ('a,'b) term

View File

@ -40,6 +40,8 @@ let rec translate_type (env : (F.tyvar * P.tyvar) list) (ty : F.nominal_type) :
P.TyMu (alpha, self ((x, alpha) :: env) ty)
| F.TyConstr (constr, tys) ->
P.TyConstr (constr, List.map (self env) tys)
| F.TyEq (ty1, ty2) ->
P.TyEq (self env ty1, self env ty2)
let print_type ty =
Printer.print_type (translate_type [] ty)
@ -84,6 +86,14 @@ let rec translate_term env (t : F.nominal_term) : P.term =
self env t,
List.map (translate_branch env) brs
)
| F.Absurd (_, ty) ->
P.Absurd (translate_type env ty)
| F.Refl (_, ty) ->
P.Refl (translate_type env ty)
| F.Use (_, t, u) ->
let t' = self env t in
let u' = self env u in
P.Use (t', u')
and translate_branch env (pat, t) =
(translate_pattern env pat, translate_term env t)
@ -155,6 +165,8 @@ let rec translate_db_type (env : P.tyvar list) (ty : F.debruijn_type) : P.typ =
P.TyMu (alpha, self (alpha :: env) ty)
| F.TyConstr (constr, tys) ->
P.TyConstr (constr, List.map (self env) tys)
| F.TyEq (ty1, ty2) ->
P.TyEq (self env ty1, self env ty2)
let print_db_type ty =
Printer.print_type (translate_db_type [] ty)
@ -190,9 +202,16 @@ let print_type_error e =
str "Type error." ++
str "This type should be a universal type:" ++
print_db_type ty
| NotAnEqual ty ->
str "Type error." ++
str "This type should be an equality type:" ++
print_db_type ty
| UnboundTermVariable x ->
str "Scope error." ++
str "The variable %s is unbound." x
| TwoOccurencesOfSameVariable x ->
str "Scope error." ++
str "The variable %s is bound twice in a pattern." x
| ContextNotAbsurd ->
str "Type error." ++
str "The context is not absurd"

View File

@ -6,8 +6,10 @@ type type_error =
| NotAnArrow of debruijn_type
| NotAProduct of debruijn_type
| NotAForall of debruijn_type
| NotAnEqual of debruijn_type
| UnboundTermVariable of tevar
| TwoOccurencesOfSameVariable of string
| ContextNotAbsurd
and arity_requirement = Index of int | Total of int
@ -37,19 +39,59 @@ module TermVarMap =
module N2DB =
DeBruijn.Nominal2deBruijn(TermVar)
(* We use a union-find to represent equalities between rigid variables
and types. We need the ability to snapshot and rollback changes, to
"un-do" the addition of an equality to the environment. *)
module UF = struct
include UnionFind.Make(UnionFind.StoreVector)
type 'a elem = 'a rref
end
module S =
Structure
(* We translate types into union-find graphs to check equality.
μ-types create cyclic graphs. Each vertex represents a type expression.
GADTs can add type equalities in the context and we represent
this by unifying their vertices in the union-find graph. This is
only possible when they have compatible structures (or one of the
side has no structure), otherwise the equality is inconsistent. *)
type vertex =
structure option UF.elem
and structure =
(* Corresponds to types from the source language (arrow, product, ...). *)
| SStruct of vertex S.structure
(* Represents ∀α.τ. We use De Bruijn levels, so we don't need to name
explicitly the bound variable α. *)
| SForall of vertex
(* A De Bruijn level corresponding to a ∀-bound variable. Using levels
instead of indices makes the equality test easier. *)
| SForallLevel of int
type env = {
(* A mapping of term variables to types. *)
types: debruijn_type TermVarMap.t;
(* A translation environment of TERM variables to TYPE indices. *)
names: N2DB.env;
(* The global store of the union-find. *)
store: structure option UF.store;
(* A mapping from rigid variables to union-find vertices. *)
tyvars: structure option UF.elem list;
(* Is set to false when an inconsistent equation is introduced in the
environment. It is useful while typechecking pattern-matching. *)
consistent: bool;
}
type _datatype_env = (unit, debruijn_type) Datatype.Env.t
let empty = {
types = TermVarMap.empty;
names = N2DB.empty;
store = UF.new_store();
tyvars = [];
consistent = true;
}
let empty =
{ types = TermVarMap.empty; names = N2DB.empty }
let lookup { types; names } x =
let lookup { types; names; _ } x =
try
(* Obtain the type associated with [x]. *)
let ty = TermVarMap.find x types in
@ -62,32 +104,47 @@ let lookup { types; names } x =
(* must have been raised by [TermVarMap.find] *)
raise (TypeError (UnboundTermVariable x))
let extend_with_tevar { types; names } x ty =
let extend_with_tevar { types; names; store; tyvars; consistent } x ty =
(* Map the name [x] to [ty], and record when it was bound, without
incrementing the time. *)
{ types = TermVarMap.add x ty types;
names = N2DB.slide names x }
names = N2DB.slide names x;
store;
tyvars;
consistent; }
let extend_with_tyvar { types; names } =
let extend_with_tyvar { types; names; store; tyvars; consistent } =
(* Create a fresh vertex for the new type variable *)
let v = UF.make store None in
(* Extend the environment of type variables *)
let tyvars = v :: tyvars in
(* Increment the time. *)
{ types; names = N2DB.bump names }
let names = N2DB.bump names in
{ types; names ; store; tyvars; consistent }
let singleton x ty =
extend_with_tevar empty x ty
let concat env1 env2 =
let combine _ _ ty2 = Some ty2 in
{ types = TermVarMap.union combine env1.types env2.types ;
names = N2DB.concat env1.names env2.names }
let types = TermVarMap.union combine env1.types env2.types in
let names = N2DB.concat env1.names env2.names in
let store = (assert (env1.store == env2.store); env1.store) in
let tyvars = env2.tyvars @ env1.tyvars in
let consistent = env1.consistent && env2.consistent in
{ types; names; store; tyvars; consistent }
let concat_disjoint env1 env2 =
let exception Conflict of TermVarMap.key in
try
let combine x _ _ =
raise (Conflict x) in
let types = TermVarMap.union combine env1.types env2.types
and names = N2DB.concat env1.names env2.names in
Ok { types; names; }
let types = TermVarMap.union combine env1.types env2.types in
let names = N2DB.concat env1.names env2.names in
let store = (assert (env1.store == env2.store); env1.store) in
let tyvars = env2.tyvars @ env1.tyvars in
let consistent = env1.consistent && env2.consistent in
Ok { types; names; store; tyvars; consistent }
with Conflict x -> Error x
(* -------------------------------------------------------------------------- *)
@ -130,202 +187,133 @@ let rec as_forall ty =
(* -------------------------------------------------------------------------- *)
(* [equal1] groups the easy cases of the type equality test. It does not
accept arguments of the form [TyMu]. It expects a self parameter [equal]
that is used to compare the children of the two root nodes. *)
let pointwise equal tys1 tys2 =
try
List.for_all2 equal tys1 tys2
with Invalid_argument _ ->
(* Catching [Invalid_argument] is bad style, but saves a couple calls
to [List.length]. A cleaner approach would be to use arrays instead
of lists. *)
false
let equal1 equal ty1 ty2 =
match ty1, ty2 with
| TyMu _, _
| _, TyMu _ ->
assert false
| TyVar x1, TyVar x2 ->
Int.equal x1 x2
| TyArrow (ty1a, ty1b), TyArrow (ty2a, ty2b) ->
equal ty1a ty2a && equal ty1b ty2b
| TyForall ((), ty1), TyForall ((), ty2) ->
equal ty1 ty2
| TyProduct tys1, TyProduct tys2 ->
pointwise equal tys1 tys2
| TyConstr (Datatype.Type tyconstr1, tys1),
TyConstr (Datatype.Type tyconstr2, tys2) ->
String.equal tyconstr1 tyconstr2 &&
pointwise equal tys1 tys2
| (TyVar _ | TyArrow _ | TyForall _ | TyProduct _ | TyConstr _),
_ ->
false
(* -------------------------------------------------------------------------- *)
(* An unsound approximation of the equality test. (Now unused.) *)
(* Comparing two [TyMu] types simply by comparing their bodies would be
correct, but incomplete: some types that are equal would be considered
different. *)
(* Naively unfolding every [TyMu] type is sound and complete, but leads to
potential non-termination. The following code avoids non-termination by
imposing a budget limit. This makes this equality test unsound: two types
may be considered equal when they are in fact different. *)
let rec equal budget ty1 ty2 =
match ty1, ty2 with
| (TyMu _ as ty1), ty2
| ty2, (TyMu _ as ty1) ->
budget = 0 || equal (budget - 1) (unfold ty1) ty2
| _, _ ->
equal1 (equal budget) ty1 ty2
let budget =
4
let _unsound_equal ty1 ty2 =
equal budget ty1 ty2
(* -------------------------------------------------------------------------- *)
(* A sound approximation of the equality test. *)
(* The System F types produced by an ML type inference algorithm cannot
contain [TyForall] under [TyMu]. In this restricted setting, deciding
type equality is relatively easy. We proceed in two layers, as follows:
- Initially, we perform a normal (structural) equality test, going
down under [TyForall] constructors if necessary. As soon as we
hit a [TyMu] constructor on either side, we switch to the lower
layer:
- In the lower layer, we know that we cannot hit a [TyForall]
constructor (if we do, we report that the types differ). We
map each type (separately) to a graph of unification variables
(where every variable has rigid structure), then we check that
the two graphs can be unified. *)
type equality is relatively easy. We map each type to a graph of
unification variables (where every variable has rigid structure),
then we check that the two graphs can be unified. *)
exception Clash =
Structure.Iter2
module S =
Structure
type vertex =
structure UnionFind.elem
and structure =
| SRigidVar of DeBruijn.index
| SStruct of vertex S.structure
let rec translate (env : vertex list) (ty : F.debruijn_type) : vertex =
match ty with
(* This function assumes that no occurence of forall quantification
appear under a mu-type. *)
let rec translate ~inside_mu store (env : vertex list) (ty : F.debruijn_type)
: vertex
= match ty with
| TyVar x ->
(* If [x] is bound in [env], then [x] is bound by μ, and we
already have a vertex that represents it. Otherwise, [x]
is bound by , and it is regarded as a rigid variable. *)
let n = List.length env in
if x < n then
List.nth env x
else
UnionFind.make (SRigidVar (x - n))
List.nth env x
| TyMu ((), ty) ->
(* Extend the environment with a mapping of this μ-bound variable
to a fresh vertex. *)
let dummy : structure = SRigidVar 0 in
let v1 = UnionFind.make dummy in
let v1 = UF.make store None in
let env = v1 :: env in
(* Translate the body. *)
let v2 = translate env ty in
let v2 = translate ~inside_mu:true store env ty in
(* Unify the vertices [v1] and [v2], keeping [v2]'s structure. *)
let v = UnionFind.merge (fun _ s2 -> s2) v1 v2 in
let v = UF.merge store (fun _ s2 -> s2) v1 v2 in
v
| TyForall _ ->
(* Either we have found a ∀ under a μ, which is unexpected, or one
of the types that we are comparing has more quantifiers than
the other. Either way, we report that the types differ. *)
raise Clash
| TyForall ((), ty) ->
if inside_mu then raise Clash;
(* Extend the environment with a mapping of this forall-bound variable
to a fresh vertex. *)
let v1 = UF.make store (Some (SForallLevel (List.length env))) in
let env = v1 :: env in
(* Translate the body. *)
let v2 = translate ~inside_mu store env ty in
UF.make store (Some (SForall v2))
| TyArrow (ty1, ty2) ->
let v1 = translate env ty1
and v2 = translate env ty2 in
UnionFind.make (SStruct (S.TyArrow (v1, v2)))
let v1 = translate ~inside_mu store env ty1
and v2 = translate ~inside_mu store env ty2 in
UF.make store (Some (SStruct (S.TyArrow (v1, v2))))
| TyProduct tys ->
let vs = translate_list env tys in
UnionFind.make (SStruct (S.TyProduct vs))
let vs = translate_list ~inside_mu store env tys in
UF.make store (Some (SStruct (S.TyProduct vs)))
| TyConstr (id, tys) ->
let vs = translate_list env tys in
UnionFind.make (SStruct (S.TyConstr (id, vs)))
let vs = translate_list ~inside_mu store env tys in
UF.make store (Some (SStruct (S.TyConstr (id, vs))))
and translate_list env tys =
List.map (translate env) tys
| TyEq (ty1, ty2) ->
let v1 = translate ~inside_mu store env ty1
and v2 = translate ~inside_mu store env ty2 in
UF.make store (Some (SStruct (S.TyEq (v1, v2))))
and translate_list ~inside_mu store env tys =
List.map (translate ~inside_mu store env) tys
let insert q v1 v2 =
Stack.push (v1, v2) q
let unify_struct q s1 s2 =
match s1, s2 with
| SRigidVar x1, SRigidVar x2 ->
| SForallLevel x1, SForallLevel x2 ->
if x1 <> x2 then raise Clash
| SStruct s1, SStruct s2 ->
Structure.iter2 (insert q) s1 s2
| SRigidVar _, SStruct _
| SStruct _, SRigidVar _ ->
| SForall s1, SForall s2 ->
insert q s1 s2
| SForallLevel _, _
| SStruct _, _
| SForall _, _ ->
raise Clash
let merge_struct q s1 s2 =
unify_struct q s1 s2;
s1
(* When we try to perform an equality check, the [mode] tells us if
one should unify rigid variables with structure (Input mode), that
is add new equalities in the typing context, or if it is not allowed
(Check mode). *)
type mode = Input | Check
let rec unify q (v1 : vertex) (v2 : vertex) =
let (_ : vertex) = UnionFind.merge (merge_struct q) v1 v2 in
unify_pending q
let merge_struct mode q so1 so2 : structure option =
match so1, so2 with
| Some s1, Some s2 ->
unify_struct q s1 s2;
so1
| None, so | so, None ->
match mode with
| Input ->
so
| Check ->
raise Clash
and unify_pending q =
let rec unify mode store q (v1 : vertex) (v2 : vertex) =
let (_ : vertex) = UF.merge store (merge_struct mode q) v1 v2 in
unify_pending mode store q
and unify_pending mode store q =
match Stack.pop q with
| v1, v2 ->
unify q v1 v2
unify mode store q v1 v2
| exception Stack.Empty ->
()
let unify v1 v2 =
let unify mode store v1 v2 =
let q = Stack.create() in
unify q v1 v2
unify mode store q v1 v2
let rec equal ty1 ty2 =
match ty1, ty2 with
| (TyMu _ as ty1), ty2
| ty2, (TyMu _ as ty1) ->
(* We have hit a μ binder on one side. Switch to layer-1 mode. *)
begin try
let env = [] in
let v1 = translate env ty1
and v2 = translate env ty2 in
unify v1 v2;
true
with Clash ->
false
end
| _, _ ->
(* Otherwise, continue in layer-2 mode. *)
equal1 equal ty1 ty2
let equal mode env ty1 ty2 =
not env.consistent ||
try
let v1 = translate ~inside_mu:false env.store env.tyvars ty1
and v2 = translate ~inside_mu:false env.store env.tyvars ty2 in
unify mode env.store v1 v2;
true
with Clash ->
false
(* -------------------------------------------------------------------------- *)
(* Re-package the type equality test as a type equality check. *)
let (--) ty1 ty2 : unit =
if not (equal ty1 ty2) then
let (--) ty1 ty2 env : unit =
if not (equal Check env ty1 ty2) then
raise (TypeError (TypeMismatch (ty1, ty2)))
(* -------------------------------------------------------------------------- *)
@ -349,14 +337,14 @@ let rec typeof datatype_env env (t : debruijn_term) : debruijn_type =
List.iter on_subterm ts;
ty
| Annot (_, t, ty) ->
typeof env t -- ty;
(typeof env t -- ty) env;
ty
| Abs (_, x, ty1, t) ->
let ty2 = typeof (extend_with_tevar env x ty1) t in
TyArrow (ty1, ty2)
| App (_, t, u) ->
let ty1, ty2 = as_arrow (typeof env t) in
typeof env u -- ty1;
(typeof env u -- ty1) env;
ty2
| Let (_, x, t, u) ->
let env = extend_with_tevar env x (typeof env t) in
@ -375,7 +363,7 @@ let rec typeof datatype_env env (t : debruijn_term) : debruijn_type =
| Variant (_, lbl, dty, t) ->
let arg_type = typeof_variant datatype_env lbl dty in
let ty = typeof env t in
ty -- arg_type;
(ty -- arg_type) env;
TyConstr dty
| LetProd (_, xs, t, u) ->
let ty = typeof env t in
@ -387,8 +375,30 @@ let rec typeof datatype_env env (t : debruijn_term) : debruijn_type =
| Match (_, ty, t, brs) ->
let scrutinee_ty = typeof env t in
let tys = List.map (typeof_branch datatype_env env scrutinee_ty) brs in
List.iter ((--) ty) tys;
List.iter (fun ty2 -> (--) ty ty2 env) tys;
ty
| Absurd (_, ty) ->
if env.consistent then
raise (TypeError (ContextNotAbsurd))
else
ty
| Refl (_, ty) ->
TyEq (ty, ty)
| Use (_, t, u) ->
let store_copy = UF.copy env.store in
let env = { env with store = store_copy } in
begin
match typeof env t with
| TyEq (ty1, ty2) ->
if equal Input env ty1 ty2 then
(* typecheck [u] in a context containing equalities introduced by
the equality ty1 = ty2 *)
typeof env u
else
typeof { env with consistent = false } u
| ty ->
raise (TypeError (NotAnEqual ty))
end
and typeof_variant datatype_env lbl (tid, tyargs) =
let Datatype.{ data_kind ; type_params ; labels_descr; _ } =
@ -407,19 +417,19 @@ and typeof_variant datatype_env lbl (tid, tyargs) =
) tyargs type_params arg_type
and typeof_branch datatype_env env scrutinee_ty (pat, rhs) =
let new_bindings = binding_pattern datatype_env scrutinee_ty pat in
let new_bindings = binding_pattern datatype_env env scrutinee_ty pat in
let new_env = concat env new_bindings in
typeof datatype_env new_env rhs
and binding_pattern datatype_env scrutinee_ty pat =
let binding_pattern = binding_pattern datatype_env in
and binding_pattern datatype_env env scrutinee_ty pat =
let binding_pattern = binding_pattern datatype_env env in
match pat with
| PVar (_, x) ->
singleton x scrutinee_ty
| PWildcard _ ->
empty
| PAnnot (_, pat, ty) ->
scrutinee_ty -- ty;
(scrutinee_ty -- ty) env;
binding_pattern ty pat
| PTuple (_, ps) ->
let tys = as_product scrutinee_ty in
@ -432,7 +442,7 @@ and binding_pattern datatype_env scrutinee_ty pat =
List.fold_left f empty envs
| PVariant (_, lbl, dty, pat) ->
let arg_type = typeof_variant datatype_env lbl dty in
scrutinee_ty -- TyConstr dty;
(scrutinee_ty -- TyConstr dty) env;
binding_pattern arg_type pat
let typeof datatype_env t =

View File

@ -8,8 +8,10 @@ type type_error =
| NotAnArrow of debruijn_type
| NotAProduct of debruijn_type
| NotAForall of debruijn_type
| NotAnEqual of debruijn_type
| UnboundTermVariable of tevar
| TwoOccurencesOfSameVariable of string
| ContextNotAbsurd
(* An arity-related requirement on a certain (sum or product) type
arising during type-checking:

View File

@ -22,8 +22,8 @@ module O = struct
let inject n =
2 * n
type 'a structure = 'a S.structure
let pprint = S.pprint
type 'a structure =
'a S.structure
type ty =
F.nominal_type
@ -39,6 +39,8 @@ module O = struct
F.TyProduct ts
| S.TyConstr (tyconstr, ts) ->
F.TyConstr(tyconstr, ts)
| S.TyEq (t1, t2) ->
F.TyEq (t1, t2)
let mu x t =
F.TyMu (x, t)

View File

@ -67,10 +67,8 @@ let term :=
| ~ = term_abs ; <>
let term_abs :=
| FUN ; xs = list (tevar_) ; "->" ; t = term_abs ;
{
List.fold_right (fun x t -> Abs ($loc, x, t)) xs t
}
| FUN ; x = tevar_ ; "->" ; t = term_abs ;
{ Abs ($loc, x, t) }
| (x, t1, t2) = letin(tevar) ; { Let ($loc, x, t1, t2) }

View File

@ -9,6 +9,7 @@ type typ =
| TyForall of tyvar * typ
| TyMu of tyvar * typ
| TyConstr of datatype
| TyEq of typ * typ
and datatype = Datatype.tyconstr_id * typ list
@ -33,6 +34,9 @@ type term =
| Inj of (typ list) option * int * term
| Variant of Datatype.label_id * datatype option * term option
| Match of typ option * term * branch list
| Absurd of typ
| Refl of typ
| Use of term * term
and branch = pattern * term

View File

@ -38,6 +38,10 @@ and print_type_arrow ty =
print_type_tyconstr ty1
^^ space ^^ string "->"
^//^ print_type_arrow ty2
| TyEq (ty1, ty2) ->
print_type_tyconstr ty1
^^ space ^^ string "="
^//^ print_type_arrow ty2
| ty ->
print_type_tyconstr ty
@ -55,7 +59,7 @@ and print_type_atom ty =
| TyProduct tys ->
surround_separate_map 2 0 (lbrace ^^ rbrace)
lbrace star rbrace print_type tys
| TyMu _ | TyForall _ | TyArrow _ | TyConstr _ as ty ->
| TyMu _ | TyForall _ | TyArrow _ | TyConstr _ | TyEq _ as ty ->
parens (print_type ty)
and print_datatype (Datatype.Type tyconstr, tyargs) =
@ -110,30 +114,6 @@ let print_let_in lhs rhs body =
^^ string "in"
^^ prefix 0 1 empty body
let rec flatten_tyabs t =
match t with
| TyAbs (x, t) ->
let (xs, t) = flatten_tyabs t in
(x::xs, t)
| t ->
([], t)
let rec flatten_abs t =
match t with
| Abs (p, t) ->
let (ps, t) = flatten_abs t in
(p::ps, t)
| t ->
([], t)
let print_nary_abstraction abs print_arg args rhs =
string abs
^^ space
^^ separate_map space print_arg args
^^ space
^^ string "->"
^//^ rhs
let print_annot print_elem (rigidity, tyvars, typ) =
let rigidity_kwd =
string @@ match rigidity with
@ -143,7 +123,7 @@ let print_annot print_elem (rigidity, tyvars, typ) =
"for"
in
surround 2 0 lparen (
print_elem ^^ space ^^ string ":"
print_elem ^^ break 1 ^^ string ":"
^^ (if tyvars = [] then empty
else prefix 2 1 empty
(rigidity_kwd ^^ space ^^
@ -156,17 +136,26 @@ let rec print_term t =
and print_term_abs t =
group @@ match t with
| TyAbs _ ->
let (xs, t) = flatten_tyabs t in
print_nary_abstraction "FUN" print_tyvar xs (print_term_abs t)
| TyAbs (x, t1) ->
string "FUN" ^^ space
^^ print_tyvar x ^^ space
^^ string "->"
^//^ print_term_abs t1
| Let (p, t1, t2) ->
print_let_in
(print_pattern p)
(print_term t1)
(print_term_abs t2)
| Abs _ ->
let (ps, t) = flatten_abs t in
print_nary_abstraction "fun" print_pattern ps (print_term_abs t)
| Abs (p, t) ->
string "fun" ^^ space
^^ print_pattern p ^^ space
^^ string "->"
^//^ print_term_abs t
| Use (t, u) ->
string "use" ^^ space
^^ print_term t
^^ space ^^ string "in" ^^ hardline
^^ print_term u
| t ->
print_term_app t
@ -183,6 +172,11 @@ and print_term_app t =
^^ space ^^ print_term_atom t
| Variant (lbl, dty, t) ->
print_variant lbl dty print_term_atom t
| Refl ty ->
group (
string "Refl"
^^ print_angle_type ty
)
| t ->
print_term_atom t
@ -200,8 +194,10 @@ and print_term_atom t =
print_match ty t brs
| Annot (t, tyannot) ->
print_annot (print_term t) tyannot
| TyAbs _ | Let _ | Abs _
| TyApp _ | App _ | Proj _ | Inj _ | Variant _ as t ->
| Absurd _ ->
dot
| TyAbs _ | Let _ | Abs _ | Use _
| TyApp _ | App _ | Proj _ | Inj _ | Variant _ | Refl _ as t ->
parens (print_term t)
and print_match ty scrutinee brs =

View File

@ -6,6 +6,7 @@ type 'a structure =
| TyArrow of 'a * 'a
| TyProduct of 'a list
| TyConstr of Datatype.tyconstr_id * 'a list
| TyEq of 'a * 'a
(* -------------------------------------------------------------------------- *)
@ -16,7 +17,8 @@ type 'a structure =
let iter f t =
match t with
| TyArrow (t1, t2) ->
| TyArrow (t1, t2)
| TyEq (t1, t2) ->
f t1; f t2
| TyProduct ts
| TyConstr (_, ts) ->
@ -24,7 +26,8 @@ let iter f t =
let fold f t accu =
match t with
| TyArrow (t1, t2) ->
| TyArrow (t1, t2)
| TyEq (t1, t2) ->
let accu = f t1 accu in
let accu = f t2 accu in
accu
@ -34,7 +37,8 @@ let fold f t accu =
let map f t =
match t with
| TyArrow (t1, t2) ->
| TyArrow (t1, t2)
| TyEq (t1, t2) ->
let t1 = f t1 in
let t2 = f t2 in
TyArrow (t1, t2)
@ -57,7 +61,8 @@ let list_iter2 f ts us =
let iter2 f t u =
match t, u with
| TyArrow (t1, t2), TyArrow (u1, u2) ->
| TyArrow (t1, t2), TyArrow (u1, u2)
| TyEq (t1, t2), TyEq (u1, u2) ->
f t1 u1;
f t2 u2
| TyProduct ts1, TyProduct ts2 ->
@ -67,7 +72,8 @@ let iter2 f t u =
list_iter2 f ts1 ts2
| TyArrow _, _
| TyProduct _, _
| TyConstr _, _ ->
| TyConstr _, _
| TyEq _, _->
raise Iter2
(* The function [conjunction] that is expected by the solver is essentially
@ -89,8 +95,10 @@ open PPrint
let pprint leaf s =
match s with
| TyArrow (t1, t2) ->
leaf t1 ^^ string " -> " ^^ leaf t2
parens (leaf t1) ^^ string " -> " ^^ leaf t2
| TyProduct ts ->
braces (separate_map (string " * ") leaf ts)
| TyConstr (Datatype.Type c, ts) ->
string c ^^ parens (separate_map (string ", ") leaf ts)
| TyEq (t1, t2) ->
parens (leaf t1 ^^ string " = " ^^ leaf t2)

View File

@ -16,3 +16,20 @@ let test (env : F.nominal_datatype_env) (t : F.nominal_term) =
Utils.emit_endline (FPrinter.print_type_error e);
failwith "Type-checking error."
| Ok _v -> ()
let test_error (env : F.nominal_datatype_env) (t : F.nominal_term) =
Printf.printf "Formatting the System F term...\n%!";
let doc = FPrinter.print_term t in
Printf.printf "Pretty-printing the System F term...\n%!";
Utils.emit_endline doc;
let env : F.debruijn_datatype_env =
F.translate_env env in
print_string "Converting the System F term to de Bruijn style...\n";
let t : F.debruijn_term =
F.Term.translate t in
print_string "Type-checking the System F term...\n";
match FTypeChecker.typeof_result env t with
| Error _ ->
()
| Ok _v ->
failwith "Type-checking error."

View File

@ -1,141 +1,669 @@
open Client
(* -------------------------------------------------------------------------- *)
(* AST helper functions *)
let (-->) ty1 ty2 =
F.TyArrow (ty1, ty2)
let unit =
F.Tuple (F.dummy_range, [])
let unit_type =
F.TyProduct []
let unit_pattern =
F.PTuple (F.dummy_range, [])
let var x =
F.(Var (dummy_range, x))
let annot ty t =
F.(Annot (dummy_range, ty, t))
let abs x ty t =
F.(Abs (dummy_range, x, ty, t))
let app t u =
F.(App (dummy_range, t, u))
let tyabs x t =
F.(TyAbs (dummy_range, x, t))
let tyapp t ty =
F.(TyApp (dummy_range, t, ty))
let tuple ts =
F.(Tuple (dummy_range, ts))
let letprod xs t u =
F.(LetProd (dummy_range, xs, t, u))
let variant lbl datatype t =
F.(Variant (dummy_range, lbl, datatype, t))
let match_ ty scrutinee branches =
F.(Match (dummy_range, ty, scrutinee, branches))
let absurd ty =
F.(Absurd (dummy_range, ty))
let refl ty =
F.(Refl (dummy_range, ty))
let use t u =
F.(Use (dummy_range, t, u))
let pvar x =
F.(PVar (dummy_range, x))
let pwildcard =
F.(PWildcard dummy_range)
let ptuple ps =
F.(PTuple (dummy_range, ps))
let pvariant lbl datatype t =
F.(PVariant (dummy_range, lbl, datatype, t))
(* -------------------------------------------------------------------------- *)
(* ∀a b. ({} -> (a * (a -> b))) -> b
Λa b. fun (p : {} -> (a * (a -> b))) ->
let (x, f) = p () in f x
*)
let let_prod =
let open F in
let alpha, beta = 0, 1 in
let p, f, x = "p", "f", "x" in
TyAbs (dummy_range, alpha, TyAbs (dummy_range, beta,
Abs (dummy_range, p, TyArrow (TyProduct [],
TyProduct [TyVar alpha; TyArrow (TyVar alpha, TyVar beta)]),
LetProd (dummy_range, [x; f],
App (dummy_range,
Var (dummy_range, p),
Tuple (dummy_range, [])),
App (dummy_range, Var (dummy_range, f), Var (dummy_range, x))))))
tyabs alpha @@
tyabs beta @@
abs p (unit_type --> F.(TyProduct [TyVar alpha; TyVar alpha --> TyVar beta])) @@
letprod [x; f]
(app (var p) (tuple []))
(app (var f) (var x))
(* Λαβ. λ(x:{α*β}. match x with (_, y) -> y end *)
let match_with_prod =
let alpha, beta = 1, 0 in
F.(
TyAbs(dummy_range, alpha,
TyAbs(dummy_range, beta,
Abs(dummy_range, "x",
TyProduct [ TyVar alpha ; TyVar beta ],
Match(dummy_range, TyVar beta,
Var (dummy_range, "x"),
[
(PTuple (dummy_range,
[ PWildcard dummy_range ; PVar (dummy_range, "y") ]) ,
Var (dummy_range, "y"))
]
)
)
)
)
)
tyabs alpha @@
tyabs beta @@
abs "x" (F.TyProduct [ F.TyVar alpha ; F.TyVar beta ]) @@
match_ (F.TyVar beta) (var "x") [
(ptuple [ pwildcard ; pvar "y" ]) , var"y"
]
(* option *)
let option_env =
let option_typedecl =
let open Datatype in {
name = Type "option";
type_params = [ 0 ];
data_kind = Variant;
labels_descr = [
{
label_name = Label "None";
type_name = Type "option";
arg_type = F.TyProduct [];
} ; {
label_name = Label "Some";
type_name = Type "option";
arg_type = F.TyVar 0;
}
];
}
name = Type "option";
type_params = [ 0 ];
data_kind = Variant;
labels_descr = [
{
label_name = Label "None";
type_name = Type "option";
arg_type = F.TyProduct [];
} ; {
label_name = Label "Some";
type_name = Type "option";
arg_type = F.TyVar 0;
}
];
}
in
Datatype.Env.add_decl Datatype.Env.empty option_typedecl
let unit = F.Tuple (F.dummy_range, [])
let unit_pattern = F.PTuple (F.dummy_range, [])
(* None *)
let none =
let alpha = 0 in
F.(
Variant (dummy_range,
Datatype.Label "None", (Datatype.Type "option", [TyForall (alpha, TyVar alpha)]), unit)
)
let label = Datatype.Label "None" in
let datatype = Datatype.Type "option", [F.TyForall (alpha, F.TyVar alpha)] in
variant label datatype unit
let none_pattern =
let alpha = 0 in
F.(
PVariant (dummy_range,
Datatype.Label "None",
(Datatype.Type "option", [TyForall (alpha, TyVar alpha)]),
unit_pattern
)
)
let label = Datatype.Label "None" in
let datatype = Datatype.Type "option", [F.TyForall (alpha, F.TyVar alpha)] in
pvariant label datatype unit_pattern
(* Some Λα.λx:α.x *)
let some =
let alpha = 0 in
F.(
Variant (dummy_range,
Datatype.Label "Some",
(Datatype.Type "option", [ TyForall (alpha, TyArrow (TyVar alpha, TyVar alpha)) ]),
TyAbs (dummy_range, alpha, Abs (dummy_range, "x", TyVar alpha, Var (dummy_range, "x")))
)
)
let label = Datatype.Label "Some" in
let datatype = Datatype.Type "option",
[ F.TyForall (alpha, F.TyVar alpha --> F.TyVar alpha) ] in
variant label datatype @@
tyabs alpha @@
abs "x" (F.TyVar alpha) @@
var "x"
let some_pattern =
let alpha = 0 in
F.(
PVariant (dummy_range,
Datatype.Label "Some",
(Datatype.Type "option", [ TyForall (alpha, TyVar alpha) ]),
PWildcard dummy_range
)
)
let label = Datatype.Label "Some" in
let datatype = Datatype.Type "option", [ F.TyForall (alpha, F.TyVar alpha) ] in
pvariant label datatype pwildcard
(* Λα. match None with
| None -> ()
| Some (_) -> ()
*)
let match_none = F.(
let match_none =
let alpha = 0 in
TyAbs(dummy_range, alpha,
Match (dummy_range,
TyProduct [] ,
none,
[
(none_pattern , unit)
;
(some_pattern , unit)
tyabs alpha @@
match_ unit_type none @@ [
(none_pattern , unit);
(some_pattern , unit);
]
(* ( refl_{} : Eq(∀α.{} , {}) ) *)
let type_eq =
let alpha = 0 in
annot (refl unit_type) @@
F.TyEq (F.TyForall (alpha, unit_type),
unit_type)
(* Λ α. use (Refl_α : eq (α,α)) in λ (x:α). x *)
let introduce_type_eq =
let alpha = 0 in
let x = "x" in
tyabs alpha @@
use
(annot (refl (F.TyVar alpha)) (F.TyEq (F.TyVar alpha, F.TyVar alpha))) @@
abs x (F.TyVar alpha) (var x)
(* Λ αβ. λ (x : eq (α)). use x in (Refl_β : eq (β,α))
* αβ. eq (α,β) -> eq (β,α) *)
let sym =
let alpha = 1 in
let beta = 0 in
let x = "x" in
annot
(tyabs alpha @@
tyabs beta @@
abs x (F.TyEq (F.TyVar alpha, F.TyVar beta)) @@
use (var x) @@
annot (refl (F.TyVar beta)) (F.TyEq (F.TyVar beta, F.TyVar alpha)))
@@
F.TyForall (alpha,
F.TyForall (beta,
F.TyEq (F.TyVar alpha, F.TyVar beta)
--> F.TyEq (F.TyVar beta, F.TyVar alpha)))
(* Λ αβγ.
λ (x : eq (α,β)).
λ (y : eq (β,γ)).
use x in
use y in
(Refl_γ : eq (α,γ))
αβγ. eq (α,β) -> eq (β,γ) -> eq (α,γ) *)
let trans =
let alpha = 2 in
let beta = 1 in
let gamma = 0 in
let x = "x" in
let y = "y" in
annot
(tyabs alpha @@
tyabs beta @@
tyabs gamma @@
abs x (F.TyEq (F.TyVar alpha, F.TyVar beta)) @@
abs y (F.TyEq (F.TyVar beta, F.TyVar gamma)) @@
use (var x) @@
use (var y) @@
annot (refl (F.TyVar gamma)) (F.TyEq (F.TyVar alpha, F.TyVar gamma)))
@@
F.TyForall (alpha,
F.TyForall (beta,
F.TyForall (gamma,
F.TyEq (F.TyVar alpha, F.TyVar beta)
--> (F.TyEq (F.TyVar beta, F.TyVar gamma)
--> F.TyEq (F.TyVar alpha, F.TyVar gamma)))))
let bool_env =
let bool_typedecl =
let open Datatype in {
name = Type "bool";
type_params = [];
data_kind = Variant;
labels_descr = [
{
label_name = Label "True";
type_name = Type "bool";
arg_type = F.TyProduct [];
} ; {
label_name = Label "False";
type_name = Type "bool";
arg_type = F.TyProduct [];
}
]
)
)
)
}
in
Datatype.Env.add_decl option_env bool_typedecl
let test_ok_from_ast datatype_env t () =
Alcotest.(check unit) "type inference" (Test.CheckF.test datatype_env t) ()
let bool_datatype =
Datatype.Type "bool", []
let test_case msg datatype_env t =
Alcotest.(test_case msg `Quick (test_ok_from_ast datatype_env t))
let int_env =
let int_typedecl =
let open Datatype in {
name = Type "int";
type_params = [];
data_kind = Variant;
labels_descr = [
{
label_name = Label "O";
type_name = Type "int";
arg_type = F.TyProduct [];
} ; {
label_name = Label "S";
type_name = Type "int";
arg_type = F.TyConstr (Type "int", []);
}
]
}
in
Datatype.Env.add_decl bool_env int_typedecl
let int_datatype =
Datatype.Type "int", []
(* small gadt *)
let small_gadt_env =
let small_gadt_typedecl =
let alpha = 0 in
let open Datatype in {
name = Type "ty";
type_params = [ alpha ];
data_kind = Variant;
labels_descr = [
{
label_name = Label "Int";
type_name = Type "ty";
arg_type = F.TyEq (F.TyVar alpha, F.TyConstr int_datatype);
} ; {
label_name = Label "Bool";
type_name = Type "ty";
arg_type = F.TyEq (F.TyVar alpha, F.TyConstr bool_datatype);
}
];
}
in
Datatype.Env.add_decl int_env small_gadt_typedecl
let int_pattern arg_type pat =
pvariant
(Datatype.Label "Int")
(Datatype.Type "ty", arg_type)
pat
let bool_pattern arg_type pat =
pvariant
(Datatype.Label "Bool")
(Datatype.Type "ty", arg_type)
pat
(*
Λα.
λ(x : μβ. {} * β).
x
*)
let mu_under_forall =
let alpha = 1 in
let beta = 0 in
let x = "x" in
tyabs alpha @@
abs x (F.TyMu (beta, F.TyProduct [unit_type ; F.TyVar beta])) @@
var x
(*
Λα.
λ(w : Eq(α,int)).
use w in
( O : α )
*)
let cast =
let alpha = 0 in
tyabs alpha @@
abs "w" (F.TyEq (F.TyVar alpha, F.TyConstr int_datatype)) @@
use (var "w") @@
annot (variant (Datatype.Label "O") int_datatype unit) (F.TyVar alpha)
(*
Λα.
λ(n : α ty).
match_α n with
| Int p ->
use (p : Eq(α,int)) in (O : α)
| Bool p ->
use (p : Eq(α,bool)) in (True : α)
*)
let match_gadt_default =
let alpha = 0 in
let int_pat =
int_pattern [F.TyVar alpha] (pvar "p")
in
let int_payoff =
use
(annot
(var "p")
(F.TyEq (F.TyVar alpha, F.TyConstr int_datatype)))
(annot
(variant
(Datatype.Label "O")
int_datatype
unit)
(F.TyVar alpha))
in
let bool_pat =
bool_pattern [F.TyVar alpha] (pvar "p")
in
let bool_payoff =
use
(annot
(var "p")
(F.TyEq (F.TyVar alpha, F.TyConstr bool_datatype)))
(annot
(variant
(Datatype.Label "True")
bool_datatype
unit)
(F.TyVar alpha))
in
tyabs alpha @@
abs "n" (F.TyConstr (Datatype.Type "ty", [F.TyVar alpha])) @@
match_ (F.TyVar alpha) (var "n") [
(int_pat , int_payoff);
(bool_pat , bool_payoff)
]
(*
(Λα.
λ(n : α ty).
match_α n with
| Int p ->
use (p : Eq(α,int)) in (O : α)
| Bool p ->
use (p : Eq(α,bool)) in (True : α))
int
(Int (refl_int))
*)
let default_int =
app
(tyapp match_gadt_default (F.TyConstr int_datatype))
(variant
(Datatype.Label "Int")
(Datatype.Type "ty", [F.TyConstr int_datatype])
(refl (F.TyConstr int_datatype)))
(*
(Λα.
λ(n : α ty).
match_α n with
| Int p ->
use (p : Eq(α,int)) in (O : α)
| Bool p ->
use (p : Eq(α,bool)) in (True : α))
bool
(Bool (refl_bool))
*)
let default_bool =
app
(tyapp match_gadt_default (F.TyConstr bool_datatype))
(variant
(Datatype.Label "Bool")
(Datatype.Type "ty", [F.TyConstr bool_datatype])
(refl (F.TyConstr bool_datatype)))
(*
(Λα.
λ(n : α ty).
match_α n with
| Int p ->
use (p : Eq(α,int)) in (O : α)
| Bool p ->
use (p : Eq(α,bool)) in (True : α))
bool
(Bool (refl_bool))
*)
let default_absurd_wrong =
let alpha = 0 in
let int_pat =
int_pattern [F.TyVar alpha] (pvar "p")
in
let int_payoff =
use (annot (var "p") (F.TyEq (F.TyVar alpha, F.TyConstr int_datatype))) @@
annot
(variant
(Datatype.Label "O")
int_datatype
(absurd unit_type))
(F.TyVar alpha)
in
let bool_pat =
bool_pattern [F.TyVar alpha] (pvar "p")
in
let bool_payoff =
use (annot (var "p") (F.TyEq (F.TyVar alpha, F.TyConstr bool_datatype))) @@
annot
(variant
(Datatype.Label "True")
bool_datatype
(absurd unit_type))
(F.TyVar alpha)
in
tyabs alpha @@
abs "n" (F.TyConstr (Datatype.Type "ty", [F.TyVar alpha])) @@
match_ (F.TyVar alpha) (var "n") [
(int_pat , int_payoff);
(bool_pat , bool_payoff)
]
(*
Λα.
λ(x : α ty).
λ(y : α ty).
match (x, y) with
| (Int p1, Int p2) ->
payoff1
| (Bool p1, Bool p2) ->
payoff2
| (Int p1, Bool p2) ->
payoff3
| (Bool p1, Int p2) ->
payoff4
*)
let test_absurd payoff1 payoff2 payoff3 payoff4 =
let alpha = 0 in
let variant_ty lbl pat =
pvariant
(Datatype.Label lbl)
(Datatype.Type "ty", [F.TyVar alpha])
pat
in
(* Helper functions for payoff *)
(* use (p1 : Eq(α,dt1)) in use (p2 : Eq(α,dt2)) in payoff *)
let double_use datatype1 datatype2 payoff=
use (annot (var "p1") (F.TyEq (F.TyVar alpha, F.TyConstr datatype1))) @@
use (annot (var "p2") (F.TyEq (F.TyVar alpha, F.TyConstr datatype2))) @@
payoff
in
(*
(Int p1, Int p2) ->
use (p1 : Eq(α,int)) in use (p2 : Eq(α,int)) in payoff1
*)
let int_int_branch =
ptuple [
(variant_ty "Int" (pvar "p1"));
(variant_ty "Int" (pvar "p2"));
] ,
double_use int_datatype int_datatype payoff1
(*
(Bool p1, Bool p2) ->
use (p1 : Eq(α,bool)) in use (p2 : Eq(α,bool)) in payoff2
*)
and bool_bool_branch =
ptuple [
(variant_ty "Bool" (pvar "p1"));
(variant_ty "Bool" (pvar "p2"));
] ,
double_use bool_datatype bool_datatype payoff2
(*
(Int p1, Bool p2) ->
use (p1 : Eq(α,int)) in use (p2 : Eq(α,bool)) in payoff3
*)
and int_bool_branch =
ptuple [
(variant_ty "Int" (pvar "p1"));
(variant_ty "Bool" (pvar "p2"));
] ,
double_use int_datatype bool_datatype payoff3
(*
(Bool p1, Int p2) ->
use (p1 : Eq(α,bool)) in use (p2 : Eq(α,int)) in payoff4
*)
and bool_int_branch =
ptuple [
(variant_ty "Bool" (pvar "p1"));
(variant_ty "Int" (pvar "p2"));
] ,
double_use bool_datatype int_datatype payoff4
in
tyabs alpha @@
abs "x" (F.TyConstr (Datatype.Type "ty", [F.TyVar alpha])) @@
abs "y" (F.TyConstr (Datatype.Type "ty", [F.TyVar alpha])) @@
match_ unit_type (tuple [ var "x"; var "y" ]) [
int_int_branch ;
bool_bool_branch;
int_bool_branch;
bool_int_branch;
]
(*
Λα.
λ(x : α ty).
λ(y : α ty).
match (x, y) with
| (Int p1, Int p2) ->
()
| (Bool p1, Bool p2) ->
()
| (Int p1, Bool p2) ->
.
| (Bool p1, Int p2) ->
.
*)
(* This example is ok : the two last branches are unreachable. *)
let test_absurd_ok =
test_absurd
unit
unit
(absurd unit_type)
(absurd unit_type)
(*
Λα.
λ(x : α ty).
λ(y : α ty).
match (x, y) with
| (Int p1, Int p2) ->
()
| (Bool p1, Bool p2) ->
()
| (Int p1, Bool p2) ->
()
| (Bool p1, Int p2) ->
()
*)
(* This example is ok : the two last branches are unreachable, but it is not
mandatory to declare them as such. *)
let test_absurd_ok2 =
test_absurd
unit
unit
unit
unit
(*
Λα.
λ(x : α ty).
λ(y : α ty).
match (x, y) with
| (Int p1, Int p2) ->
.
| (Bool p1, Bool p2) ->
.
| (Int p1, Bool p2) ->
.
| (Bool p1, Int p2) ->
.
*)
(* This example is wrong : the first two branches are reachable, i.e. they
don't introduce type inconsistencies in the environment *)
let test_absurd_wrong =
test_absurd
(absurd unit_type)
(absurd unit_type)
(absurd unit_type)
(absurd unit_type)
let test_ok_from_ast msg datatype_env t =
let test_ok () =
Alcotest.(check unit) "type inference" (Test.CheckF.test datatype_env t) ()
in
Alcotest.(test_case msg `Quick test_ok)
let test_type_error msg datatype_env t =
let test_error () =
Alcotest.(check unit) "type inference"
(Test.CheckF.test_error datatype_env t) ()
in
Alcotest.(test_case msg `Quick test_error)
let test_suite =
[(
"test F ast",
[ test_case "let prod" Datatype.Env.empty let_prod;
test_case "match with prod" Datatype.Env.empty match_with_prod;
test_case "unit" option_env unit;
test_case "none" option_env none;
test_case "some" option_env some;
test_case "match none" option_env match_none;
[ test_ok_from_ast "let prod" Datatype.Env.empty let_prod;
test_ok_from_ast "match with prod" Datatype.Env.empty match_with_prod;
test_ok_from_ast "unit" option_env unit;
test_ok_from_ast "none" option_env none;
test_ok_from_ast "some" option_env some;
test_ok_from_ast "match none" option_env match_none;
test_type_error "type equality" Datatype.Env.empty type_eq;
test_ok_from_ast "introduce type equality" Datatype.Env.empty introduce_type_eq;
test_ok_from_ast "symmetry" Datatype.Env.empty sym;
test_ok_from_ast "transitivity" Datatype.Env.empty trans;
test_ok_from_ast "mu under forall" Datatype.Env.empty mu_under_forall;
test_ok_from_ast "cast" int_env cast;
test_ok_from_ast "default" small_gadt_env match_gadt_default;
test_ok_from_ast "default int" small_gadt_env default_int;
test_ok_from_ast "default bool" small_gadt_env default_bool;
test_type_error "default absurd wrong" small_gadt_env default_absurd_wrong;
test_ok_from_ast "pair of gadt" small_gadt_env test_absurd_ok;
test_ok_from_ast "pair of gadt" small_gadt_env test_absurd_ok2;
test_type_error "pair of gadt" small_gadt_env test_absurd_wrong;
]
)]

View File

@ -103,8 +103,9 @@ Option type
Type inference and translation to System F...
Formatting the System F term...
Pretty-printing the System F term...
FUN a0 a1 ->
Some<option {a1 -> a1*a0 -> a0}> (fun (x : a1) -> x, fun (x : a0) -> x)
FUN a0 ->
FUN a1 ->
Some<option {a1 -> a1*a0 -> a0}> (fun (x : a1) -> x, fun (x : a0) -> x)
Converting the System F term to de Bruijn style...
Type-checking the System F term...
@ -222,11 +223,12 @@ Pattern-matching
Type inference and translation to System F...
Formatting the System F term...
Pretty-printing the System F term...
FUN a0 a1 ->
match<option a0> Some<option (a1 -> a1)> (fun (x : a1) -> x) with
| None<option (a1 -> a1)> () -> None<option a0> ()
| (Some<option (a1 -> a1)> _ : option (a1 -> a1)) -> None<option a0> ()
end
FUN a0 ->
FUN a1 ->
match<option a0> Some<option (a1 -> a1)> (fun (x : a1) -> x) with
| None<option (a1 -> a1)> () -> None<option a0> ()
| (Some<option (a1 -> a1)> _ : option (a1 -> a1)) -> None<option a0> ()
end
Converting the System F term to de Bruijn style...
Type-checking the System F term...
@ -309,7 +311,7 @@ It involves a useless universal quantifier.
Type inference and translation to System F...
Formatting the System F term...
Pretty-printing the System F term...
(FUN a1 a2 -> (fun (x : a2) -> x : a2 -> a2)) [[a0] a0] [{}] ()
(FUN a1 -> FUN a2 -> (fun (x : a2) -> x : a2 -> a2)) [[a0] a0] [{}] ()
Converting the System F term to de Bruijn style...
Type-checking the System F term...
@ -328,8 +330,12 @@ and unreachable from the entry point of a type scheme.
Type inference and translation to System F...
Formatting the System F term...
Pretty-printing the System F term...
(FUN a1 a2 ->
((fun (x : a1 -> a1) (y : a2) -> y) (fun (x : a1) -> x) : a2 -> a2))
(FUN a1 ->
FUN a2 ->
(
(fun (x : a1 -> a1) -> fun (y : a2) -> y) (fun (x : a1) -> x)
: a2 -> a2
))
[[a0] a0]
[{}]
()

View File

@ -12,7 +12,7 @@
open Signatures
module Make
(S : DSTRUCTURE)
(S : OSTRUCTURE)
(U : MUNIFIER with type 'a structure := 'a S.structure)
(O : OUTPUT with type 'a structure := 'a S.structure)
= struct
@ -20,6 +20,28 @@ open U
(* -------------------------------------------------------------------------- *)
(* Decoding a variable. *)
(* The public function [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 : variable) : O.tyvar =
let data = U.get v in
assert (S.is_leaf data);
O.inject (S.id data)
(* The internal function [decode_id] decodes a variable. As above, this
variable must have leaf structure, and the decoded variable is determined
by the unique identity [id], which is already at hand. *)
(* [O.variable] is used to convert the result from [O.tyvar] to [O.ty]. *)
let decode_id (id : id) : O.ty =
O.variable (O.inject id)
(* -------------------------------------------------------------------------- *)
(* An acyclic decoder performs a bottom-up computation over an acyclic graph. *)
let new_acyclic_decoder () : variable -> O.ty =
@ -35,9 +57,14 @@ let new_acyclic_decoder () : variable -> O.ty =
try
Hashtbl.find visited id
with Not_found ->
let a = O.structure (S.map decode data) in
(* Because the graph is assumed to be acyclic, it is ok to update
the hash table only after the recursive call. *)
let a =
if S.is_leaf data then
decode_id id
else
O.structure (S.map decode data)
in
Hashtbl.add visited id a;
a
@ -174,33 +201,36 @@ let new_cyclic_decoder () : variable -> O.ty =
with Not_found ->
(* Otherwise, compute a decoded value [a] for this vertex. *)
let a =
if Hashtbl.mem table id then begin
(* We have just rediscovered this vertex via a back edge. Its
status may be [Active] or [Rediscovered]. We change it to
[Rediscovered], and stop the traversal. *)
Hashtbl.replace table id Rediscovered;
(* Decode this vertex as a (μ-bound) variable, identified by
its unique identity [id]. *)
O.variable (O.inject id)
end
else begin
(* This vertex is not being visited. Before the recursive
call, mark it as being visited. *)
Hashtbl.add table id Active;
(* Perform the recursive traversal. *)
let a = O.structure (S.map decode data) in
(* Mark this vertex as no longer being visited. If it was
recursively rediscovered during the recursive call,
introduce a μ binder. (It would be correct but noisy to
always introduce a μ binder.) *)
let status =
try Hashtbl.find table id with Not_found -> assert false
in
Hashtbl.remove table id;
match status with
| Active -> a
| Rediscovered -> O.mu (O.inject id) a
end
if S.is_leaf data then
(* There is no structure. *)
decode_id id
else
(* There is some structure. *)
if Hashtbl.mem table id then begin
(* We have just rediscovered this vertex via a back edge. Its
status may be [Active] or [Rediscovered]. We change it to
[Rediscovered], and stop the traversal. *)
Hashtbl.replace table id Rediscovered;
decode_id id
end
else begin
(* This vertex is not being visited. Before the recursive
call, mark it as being visited. *)
Hashtbl.add table id Active;
(* Perform the recursive traversal. *)
let a = O.structure (S.map decode data) in
(* Mark this vertex as no longer being visited. If it was
recursively rediscovered during the recursive call,
introduce a μ binder. (It would be correct but noisy to
always introduce a μ binder.) *)
let status =
try Hashtbl.find table id with Not_found -> assert false
in
Hashtbl.remove table id;
match status with
| Active -> a
| Rediscovered -> O.mu (O.inject id) a
end
in
(* If this vertex is isolated, store the decoded value [a] in the
memoization table [visited]. (It would be correct to never

View File

@ -11,29 +11,22 @@
open Signatures
(**This module performs decoding, which is the task of traversing the data
structure maintained by the unifier and transforming it into a data
(**This module offers performs decoding, which is the task of traversing the
data structure maintained by the unifier and transforming it into a data
representation selected by the user (typically, some form of tree). It is
parameterized by the term structure [S], by the unifier [U], and by the
data representation [O]. Read-only access to the unifier's data structure
suffices.
Two decoding algorithms are proposed: the {i acyclic decoder} does not
tolerate cycles, and produces ordinary trees; whereas the {i cyclic
decoder} can deal with cycles, and produces trees that contain μ
binders.
The cyclic decoder can produce μ binders and μ-bound type variables.
Neither decoder has specific support for printing ordinary (-bound)
type variables. In the eyes of the decoders, a type variable is just
a vertex that has no structure; it is up to the user-supplied function
[O.structure] to determine how such a vertex must be printed. *)
suffices. Two decoding algorithms are proposed: the {i acyclic decoder}
does not tolerate cycles, and produces ordinary trees; whereas the {i
cyclic decoder} can deal with cycles, and produces trees that contain μ
binders. *)
module Make
(S : sig (** @inline *) include DSTRUCTURE end)
(S : sig (** @inline *) include OSTRUCTURE end)
(U : sig (** @inline *) include MUNIFIER
with type 'a structure := 'a S.structure end)
(O : sig (** @inline *) include OUTPUT
with type 'a structure := 'a S.structure end)
: sig (** @inline *) include DECODER
with type variable := U.variable
and type tyvar := O.tyvar
and type ty := O.ty end

View File

@ -11,7 +11,7 @@
open Signatures
module Make (S : GSTRUCTURE_OPT) = struct
module Make (S : STRUCTURE_LEAF) = struct
(* -------------------------------------------------------------------------- *)
@ -126,14 +126,6 @@ type 'a data = {
mutable mark: mark;
}
(* A printer (for debugging purposes). *)
let pprint elem data =
let open PPrint in
utf8format "@%d[%d]" data.id data.rank ^^
S.pprint elem data.structure
(* [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
@ -154,15 +146,14 @@ let adjust_rank (data : 'a data) (k : rank) =
else
raise VariableScopeEscape
(* The module [Data] is meant to be an argument for [Unifier.Make]. *)
(* The module [Data] satisfies the signature [USTRUCTURE] required by the
functor [Unifier.Make]. *)
module Data = struct
type 'a structure =
'a data
let pprint = pprint
let id data =
data.id
@ -224,8 +215,8 @@ module Data = struct
| Flexible, _, Rigid, rigid_rank ->
(* One cannot lower the rank of a rigid variable. *)
if rank < rigid_rank then raise VariableScopeEscape;
(* One cannot assign some structure to a rigid variable. *)
if Option.is_some structure then raise InconsistentConjunction;
(* One cannot assign non-leaf structure to a rigid variable. *)
if not (S.is_leaf structure) then raise InconsistentConjunction;
Rigid
in
(* There is no need to preserve marks during unification. *)
@ -233,7 +224,7 @@ module Data = struct
{ id; structure; rank; status; mark }
let is_leaf data =
Option.is_none data.structure
S.is_leaf data.structure
let project data =
data.structure
@ -340,8 +331,9 @@ let flexible structure =
let rigid () =
let r = state.young in
let structure = S.leaf in
let status = Rigid in
let v = U.fresh (Data.make None r status) in
let v = U.fresh (Data.make structure r status) in
register v r;
v
@ -751,7 +743,7 @@ let instantiate { generics; quantifiers; root } =
let data = get v in
assert (data.status = Generic);
data.mark <- i;
flexible None
flexible S.leaf
)
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 STRUCTURE_LEAF end)
: sig
(** {2 Unification} *)
@ -31,7 +31,7 @@ module Make
module Data : sig
(** @inline *)
include DSTRUCTURE
include OSTRUCTURE
(**The type ['a structure] is richer (carries more information) than the
type ['a S.structure]. The function [project] witnesses this fact. It

View File

@ -12,7 +12,7 @@
open Signatures
module Make
(S : OSTRUCTURE)
(S : OCSTRUCTURE)
(U : MUNIFIER with type 'a structure = 'a S.structure)
= struct

View File

@ -16,7 +16,7 @@ open Signatures
parameterized by the term structure [S] and by the unifier [U]. Read-only
access to the unifier's data structure suffices. *)
module Make
(S : sig (** @inline *) include OSTRUCTURE end)
(S : sig (** @inline *) include OCSTRUCTURE end)
(U : sig (** @inline *) include MUNIFIER
with type 'a structure = 'a S.structure end)
: sig (** @inline *) include OCCURS_CHECK

View File

@ -28,9 +28,9 @@ type id = int
(* -------------------------------------------------------------------------- *)
(* [STRUCTURE] describes just the type ['a structure]. *)
(* [SSTRUCTURE] describes just the type ['a structure]. *)
module type STRUCTURE = sig
module type SSTRUCTURE = sig
(**A structure is a piece of information that the unifier attaches to a
variable (or, more accurately, to an equivalence class of variables).
@ -53,23 +53,14 @@ module type STRUCTURE = sig
which indicates the presence of an equality constraint. *)
type 'a structure
(**[pprint] is a structure printer, parameterized over a child printer.
It is used for debugging purposes only. *)
val pprint: ('a -> PPrint.document) -> 'a structure -> PPrint.document
end
(* -------------------------------------------------------------------------- *)
(* [USTRUCTURE] describes an input of [Unifier.Make]. *)
(* The following signatures enrich [STRUCTURE] with additional operations. *)
(* [CONJUNCTIBLE] describes structures with a [conjunction] operation,
as required by [Unifier.Make]. *)
module type CONJUNCTIBLE = sig
module type USTRUCTURE = sig
(** @inline *)
include STRUCTURE
include SSTRUCTURE
(**[InconsistentConjunction] is raised by {!conjunction}. *)
exception InconsistentConjunction
@ -100,23 +91,47 @@ module type CONJUNCTIBLE = sig
end
(* [IDENTIFIABLE] describes a structure with unique identifiers,
as required by [OccursCheck.Make] and [Decoder.Make]. *)
module type IDENTIFIABLE = sig
(* [OCSTRUCTURE] describes an input of [OccursCheck.Make]. *)
module type OCSTRUCTURE = sig
(** @inline *)
include STRUCTURE
include SSTRUCTURE
(**[iter] applies an action to every child of a structure. *)
val iter: ('a -> unit) -> 'a structure -> unit
(**[id] extracts the unique identifier of a structure. *)
val id: 'a structure -> id
end
(* [MAPPABLE] describes traversable, mappable structures. *)
module type MAPPABLE = sig
(* [OSTRUCTURE] describes an input of [Decoder.Make]. *)
module type OSTRUCTURE = sig
(** @inline *)
include STRUCTURE
include OCSTRUCTURE
(**[map] applies a transformation to the children of a structure,
while preserving the shape of the structure. *)
val map: ('a -> 'b) -> 'a structure -> 'b structure
(**[is_leaf s] determines whether the structure [s] is a leaf, that is,
whether it represents the absence of a logical constraint. This function
is typically used by a decoder to determine which equivalence classes
should be translated to "type variables" in a decoded type. *)
val is_leaf: 'a structure -> bool
end
(* [GSTRUCTURE] describes an input of [Structure.Option],
and also describes part of its output. *)
module type GSTRUCTURE = sig
(** @inline *)
include USTRUCTURE
(**[iter] applies an action to every child of a structure. *)
val iter: ('a -> unit) -> 'a structure -> unit
@ -131,74 +146,37 @@ module type MAPPABLE = sig
end
(* -------------------------------------------------------------------------- *)
(* [USTRUCTURE] describes an input of [Unifier.Make]. *)
module type USTRUCTURE = sig
(** @inline *)
include STRUCTURE
(** @inline *)
include CONJUNCTIBLE with type 'a structure := 'a structure
end
(* [OSTRUCTURE] describes an input of [OccursCheck.Make]. *)
module type OSTRUCTURE = sig
(** @inline *)
include STRUCTURE
(** @inline *)
include MAPPABLE with type 'a structure := 'a structure
(** @inline *)
include IDENTIFIABLE with type 'a structure := 'a structure
end
(* [DSTRUCTURE] describes an input of [Decoder.Make]. *)
module type DSTRUCTURE = sig
(** @inline *)
include STRUCTURE
(** @inline *)
include MAPPABLE with type 'a structure := 'a structure
(** @inline *)
include IDENTIFIABLE with type 'a structure := 'a structure
end
(* [GSTRUCTURE] describes an input of [Structure.Option]
and an input of [Solver.Make]. *)
module type GSTRUCTURE = sig
(** @inline *)
include STRUCTURE
(** @inline *)
include CONJUNCTIBLE with type 'a structure := 'a structure
(** @inline *)
include MAPPABLE with type 'a structure := 'a structure
end
(* [GSTRUCTURE_OPT] describes the output of [Structure.Option] and
(* [STRUCTURE_LEAF] describes the output of [Structure.Option] and
an input of [Generalization.Make]. *)
module type GSTRUCTURE_OPT = sig
module S : GSTRUCTURE
module type STRUCTURE_LEAF = sig
(** @inline *)
include GSTRUCTURE with type 'a structure = 'a S.structure option
include GSTRUCTURE
(**The constant [leaf] is a structure that represents the absence of a
logical constraint. It is typically used when a variable is created
fresh. *)
val leaf: 'a structure
(**[is_leaf s] determines whether the structure [s] is a leaf, that is,
whether it represents the absence of a logical constraint. This function
is typically used by a decoder to determine which equivalence classes
should be translated to "type variables" in a decoded type. *)
val is_leaf: 'a structure -> bool
end
(* [HSTRUCTURE] describes an input of [Solver.Make]. *)
module type HSTRUCTURE = sig
(** @inline *)
include GSTRUCTURE
(**[pprint] is a structure printer, parameterized over a child printer.
It is used for debugging purposes only. *)
val pprint: ('a -> PPrint.document) -> 'a structure -> PPrint.document
end
@ -321,7 +299,7 @@ end
module type OUTPUT = sig
(** @inline *)
include STRUCTURE
include SSTRUCTURE
(**A representation of decoded type variables. *)
type tyvar
@ -355,8 +333,12 @@ end
module type DECODER = sig
type variable
type tyvar
type ty
(**[decode_variable v] decodes the variable [v]. *)
val decode_variable: variable -> tyvar
(**[new_acyclic_decoder()] initiates a new decoding phase. It returns a
decoding function [decode], which can be used as many as times as one
wishes. Decoding requires the graph to be acyclic: it is a bottom-up

View File

@ -13,7 +13,7 @@ open Signatures
module Make
(X : TEVAR)
(S : GSTRUCTURE)
(S : HSTRUCTURE)
(O : OUTPUT with type 'a structure = 'a S.structure)
= struct
@ -357,41 +357,17 @@ end (* UVar *)
(in the acyclic case), regardless of how many calls to the decoder are
performed. *)
(* [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 data = U.get v in
match G.Data.project data with
| Some _ -> assert false
| None -> O.inject (G.Data.id data)
(* TODO explain *)
(* The module [D] is used to decode non-leaf structures *)
module D =
Decoder.Make (G.Data) (U) (struct
include O
let pprint = G.Data.pprint
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
O.structure (OS.project_nonleaf (G.Data.project s))
end)
(* -------------------------------------------------------------------------- *)
(* Initialize a decoder for use during elaboration. If [rectypes] is on, a
cyclic decoder is used; otherwise, an acyclic decoder is used. *)
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),
decode (G.body s)
(* -------------------------------------------------------------------------- *)
(* The exceptions [Unify] and [Cycle], raised by the unifier, must be caught
and re-raised in a slightly different format.
@ -420,6 +396,18 @@ let exit range ~rectypes vs =
(* -------------------------------------------------------------------------- *)
(* Initialize a decoder for use during elaboration. If [rectypes] is on, a
cyclic decoder is used; otherwise, an acyclic decoder is used. *)
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 D.decode_variable (G.quantifiers s),
decode (G.body s)
(* -------------------------------------------------------------------------- *)
(* The toplevel constraint that is passed to the solver must have been
constructed by [let0], otherwise we risk encountering type variables that
we cannot register. Indeed, [G.register] must not be called unless
@ -561,7 +549,7 @@ let rec solve : type a . range -> a co -> a on_sol =
let (On_sol r2) = solve range c2 in
List.iter Env.unbind xs;
On_sol (fun () ->
List.map decode_variable gammas,
List.map D.decode_variable gammas,
List.map decode_scheme ss,
r1(),
r2()

View File

@ -31,7 +31,7 @@ open Signatures
elaboration in order to construct an explicitly-typed program. *)
module Make
(X : sig (** @inline *) include TEVAR end)
(S : sig (** @inline *) include GSTRUCTURE end)
(S : sig (** @inline *) include HSTRUCTURE end)
(O : sig (** @inline *) include OUTPUT
with type 'a structure = 'a S.structure end)
: sig

View File

@ -13,8 +13,6 @@ open Signatures
module Option (S : GSTRUCTURE) = struct
module S = S
type 'a structure =
'a S.structure option
@ -54,7 +52,13 @@ module Option (S : GSTRUCTURE) = struct
let s = S.conjunction equate s1 s2 in
if s == s1 then so1 else Some s
let pprint elem os =
PPrint.OCaml.option (S.pprint elem) os
let leaf =
None
let is_leaf =
Option.is_none
let project_nonleaf =
Option.get
end (* Option *)

View File

@ -21,6 +21,11 @@ open Signatures
module Option (S : sig (** @inline *) include GSTRUCTURE end) : sig
(** @inline *)
include GSTRUCTURE_OPT with module S = S
include STRUCTURE_LEAF with type 'a structure = 'a S.structure option
(**[project_nonleaf (Some s)] is [s], while [project_nonleaf None] is
undefined. In other words, if [os] is a non-leaf optional structure,
then [project_nonleaf os] is the underlying structure. *)
val project_nonleaf : 'a structure -> 'a S.structure
end