diff --git a/client/F.ml b/client/F.ml
index ece5c0b7620028a8826620435a0bc866a5dafd0f..72891b5935d8698d7f9b806e46fdd6e2a24a19b1 100644
--- a/client/F.ml
+++ b/client/F.ml
@@ -4,11 +4,20 @@
(* Types. *)
-(* We include recursive types [FTyMu] in the target calculus, not only because
+(* We include recursive types [TyMu] in the target calculus, not only because
we might wish to support them, but also because even if we disallow them,
they can still arise during unification (the occurs check is run late), so
we must be able to display them as part of a type error message. *)
+(* Types mixing ∀ and μ are difficult to compare in general. To simplify
+ equality checking, we do not allow ∀ under μ.
+ For instance :
+ ∀ a. μ t. a -> t is allowed
+ μ t . ∀ a . (a -> t) is not allowed
+ μ t . (∀ a . a) -> t is not allowed *)
+
+(* We also include a type equality witness [TyEq]. *)
+
(* Nominal or de Bruijn representation of type variables and binders. The
nominal representation is more convenient when translating from ML to F,
while the de Bruijn representation is more convenient when type-checking
@@ -27,6 +36,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
@@ -53,7 +63,27 @@ type debruijn_datatype_env =
(* Nominal representation of term variables and binders. *)
-type tevar = string
+(* Nominal or de Bruijn representation of type variables and binders. *)
+
+(* We include a term [Refl] that represents a type equality witness.
+ Note that it has only one type argument but is typed as a witness for
+ an equality between two possibly distinct types (see [TyEq] above).
+
+ [Use] is a construct that "opens" a type equality. That is, it allows us to
+ reason in a context where two types are assumed to be equals.
+ It is supposed to be used with a type equality witness as a left-hand side :
+
+ use (eq : TyEq (ty1, ty2)) in
+ ... (* here ty1 and ty2 are assumed to be equal *)
+
+ Doing this might introduce inconsistent assumptions about types (this can
+ occur for example inside a pattern matching). That is why we introduce
+ a construct [Absurd], that can be used as a placeholder in pieces of code
+ with inconsistent equations in the environment and that are thus
+ unreachable. *)
+
+type tevar =
+ string
type ('a, 'b) term =
| Var of range * tevar
@@ -69,6 +99,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 +182,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 +255,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)
diff --git a/client/F.mli b/client/F.mli
index 14fba6e5c1a6c02b4ed906661a8b4b93d2bfabde..ee46f38aafc4eacc238ff6d5f8e1e29491a778e9 100644
--- a/client/F.mli
+++ b/client/F.mli
@@ -4,11 +4,20 @@
(* Types. *)
-(* We include recursive types [FTyMu] in the target calculus, not only because
+(* We include recursive types [TyMu] in the target calculus, not only because
we might wish to support them, but also because even if we disallow them,
they can still arise during unification (the occurs check is run late), so
we must be able to display them as part of a type error message. *)
+(* Types mixing ∀ and μ are difficult to compare in general. To simplify
+ equality checking, we do not allow ∀ under μ.
+ For instance :
+ ∀ a. μ t. a -> t is allowed
+ μ t . ∀ a . (a -> t) is not allowed
+ μ t . (∀ a . a) -> t is not allowed *)
+
+(* We also include a type equality witness [TyEq]. *)
+
(* Nominal or de Bruijn representation of type variables and binders. The
nominal representation is more convenient when translating from ML to F,
while the de Bruijn representation is more convenient when type-checking
@@ -26,6 +35,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
@@ -55,6 +65,23 @@ type debruijn_datatype_env =
(* Nominal or de Bruijn representation of type variables and binders. *)
+(* We include a term [Refl] that represents a type equality witness.
+ Note that it has only one type argument but is typed as a witness for
+ an equality between two possibly distinct types (see [TyEq] above).
+
+ [Use] is a construct that "opens" a type equality. That is, it allows us to
+ reason in a context where two types are assumed to be equals.
+ It is supposed to be used with a type equality witness as a left-hand side :
+
+ use (eq : TyEq (ty1, ty2)) in
+ ... (* here ty1 and ty2 are assumed to be equal *)
+
+ Doing this might introduce inconsistent assumptions about types (this can
+ occur for example inside a pattern matching). That is why we introduce
+ a construct [Absurd], that can be used as a placeholder in pieces of code
+ with inconsistent equations in the environment and that are thus
+ unreachable. *)
+
type tevar =
string
@@ -72,6 +99,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
diff --git a/client/FPrinter.ml b/client/FPrinter.ml
index f8fdad607c69c812afd97fbb44a737361fa69a8d..36c56fb25b52a93561e1ac4b91130ffa1a4f1566 100644
--- a/client/FPrinter.ml
+++ b/client/FPrinter.ml
@@ -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,19 @@ 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
+ | UnboundTypeVariable x ->
+ str "Scope error." ++
+ str "The type variable %d 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 type equations in the typing environment are not contradictory."
diff --git a/client/FTypeChecker.ml b/client/FTypeChecker.ml
index 466c02a7859ab01dd67eb72427c200ab21243292..6084e76e23f0589c5ffba7e88e9e7b36297b12d9 100644
--- a/client/FTypeChecker.ml
+++ b/client/FTypeChecker.ml
@@ -6,8 +6,11 @@ type type_error =
| NotAnArrow of debruijn_type
| NotAProduct of debruijn_type
| NotAForall of debruijn_type
+ | NotAnEqual of debruijn_type
| UnboundTermVariable of tevar
+ | UnboundTypeVariable of tyvar
| TwoOccurencesOfSameVariable of string
+ | ContextNotAbsurd
and arity_requirement = Index of int | Total of int
@@ -37,19 +40,64 @@ module TermVarMap =
module N2DB =
DeBruijn.Nominal2deBruijn(TermVar)
+(* We use a union-find data structure to represent equalities between rigid
+ variables and types. We need the ability to snapshot and rollback changes, to
+ undo 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
+ possible only 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
+
+(* The global store of the union-find. *)
+type uf_store = structure option UF.store
+
+(* A mapping from rigid variables to union-find vertices. *)
+type uf_tyvars = structure option UF.elem list
+
+(* If the type equations introduced are inconsistent, then no need for
+ [store] and [tyvars] *)
+type equations_env =
+ | Equations of { store: uf_store ; tyvars: uf_tyvars }
+ | Inconsistent
+
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;
+ (* We keep trace of whether or not the typing equations is consistent *)
+ equations: equations_env;
}
-type _datatype_env = (unit, debruijn_type) Datatype.Env.t
-
-let empty =
- { types = TermVarMap.empty; names = N2DB.empty }
+let empty = {
+ types = TermVarMap.empty;
+ names = N2DB.empty;
+ equations = Equations { store = UF.new_store() ; tyvars = [] };
+}
-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 +110,59 @@ 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; equations } 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 }
-
-let extend_with_tyvar { types; names } =
- (* Increment the time. *)
- { types; names = N2DB.bump names }
+ names = N2DB.slide names x;
+ equations; }
+
+let extend_with_tyvar { types; names; equations } =
+ match equations with
+ | Inconsistent ->
+ { types; names; equations }
+ | Equations { store; tyvars } ->
+ (* 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. *)
+ let names = N2DB.bump names in
+ { types; names ; equations = Equations { store ; tyvars } }
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
+ match (env1.equations, env2.equations) with
+ | Inconsistent,_ | _, Inconsistent ->
+ { types; names; equations = Inconsistent }
+ | Equations { store = store1; tyvars = tyvars1 },
+ Equations { store = store2; tyvars = tyvars2 } ->
+ assert (store1 == store2);
+ let store = store1 in
+ let tyvars = tyvars1 @ tyvars2 in
+ { types; names; equations = Equations { store; tyvars} }
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
+ match (env1.equations, env2.equations) with
+ | Inconsistent,_ | _, Inconsistent ->
+ Ok { types; names; equations = Inconsistent }
+ | Equations { store = store1; tyvars = tyvars1 },
+ Equations { store = store2; tyvars = tyvars2 } ->
+ assert (store1 == store2);
+ let store = store1 in
+ let tyvars = tyvars1 @ tyvars2 in
+ Ok { types; names; equations = Equations { store; tyvars } }
with Conflict x -> Error x
(* -------------------------------------------------------------------------- *)
@@ -130,204 +205,182 @@ 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 no universal quantification inside a μ-type, because
+ it would be difficult to check type equality otherwise. The boolean
+ [inside_mu] tracks whether we are already under a μ quantifier. *)
+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))
+ begin
+ (* If the type is closed, then [x] was bound by a quantifier before and
+ was added to the environment. *)
+ try
+ List.nth env x
+ with Not_found ->
+ raise (TypeError (UnboundTypeVariable x))
+ end
| 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) ->
+ assert (not inside_mu);
+ (* 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))))
+
+ | 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 env tys =
- List.map (translate env) tys
+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
-
-let rec unify q (v1 : vertex) (v2 : vertex) =
- let (_ : vertex) = UnionFind.merge (merge_struct q) v1 v2 in
- unify_pending q
-and unify_pending q =
+(* We need two operations on equalities between types:
+ - add an equality to the equations in the environment
+ - check if a given equality holds modulo the equations in the environment *)
+
+(* Both operations can be described as first decomposing a given equality
+ "ty1 = ty2" into "simple equalities" between a rigid variable and a type.
+ In fact, the union-find data structure that we use to represent an
+ environment of equations store exactly those simple equalities. *)
+
+(* Then:
+ - to add an equality, we modify our environment by unifying the type
+ variables with the equated type
+ - to check an equality, we check that the simple equalities are already
+ valid in the equations of the environment, and fail otherwise *)
+
+(* The decomposition process does not produce simple equalities if the
+ provided equality is absurd ("int * int = int * bool").
+ Then:
+ - if we are adding this equality to the environment, we record that the
+ environment is now Inconsistent
+ - if we are checking the equality (in a consistent environment), we fail *)
+
+(* The functions below implement a unification procedure that implements both
+ these operations, depending on a [mode] parameter:
+ - in [Input] mode, they add an equality to the environment
+ - in [Check] mode, they check that the equality holds modulo the equations
+ in the environment *)
+
+type mode = Input | Check
+
+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
+
+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
-
-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
+ unify mode store q v1 v2
+
+let unify_types mode env ty1 ty2 =
+ match env.equations with
+ | Inconsistent ->
+ true
+ | Equations { store ; tyvars } ->
+ try
+ let v1 = translate ~inside_mu:false store tyvars ty1
+ and v2 = translate ~inside_mu:false store tyvars ty2 in
+ unify mode 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
+(* Re-package the type unification as a type equality check. *)
+let enforce_equal env ty1 ty2 : unit =
+ if not (unify_types Check env ty1 ty2) then
raise (TypeError (TypeMismatch (ty1, ty2)))
+(* Re-package the type unification as an addition in the environment. *)
+let add_equation env ty1 ty2 : env =
+ if unify_types Input env ty1 ty2 then
+ env
+ else
+ { env with equations = Inconsistent }
+
+let copy_env env store tyvars =
+ let store_copy = UF.copy store in
+ let equations = Equations { store = store_copy; tyvars } in
+ { env with equations }
+
(* -------------------------------------------------------------------------- *)
(* The type-checker. *)
@@ -349,14 +402,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;
+ enforce_equal env (typeof env t) ty;
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;
+ enforce_equal env (typeof env u) ty1;
ty2
| Let (_, x, t, u) ->
let env = extend_with_tevar env x (typeof env t) in
@@ -375,7 +428,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;
+ enforce_equal env ty arg_type;
TyConstr dty
| LetProd (_, xs, t, u) ->
let ty = typeof env t in
@@ -387,8 +440,32 @@ 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 -> enforce_equal env ty ty2) tys;
ty
+ | Absurd (_, ty) ->
+ begin
+ match env.equations with
+ | Inconsistent ->
+ ty
+ | Equations _ ->
+ raise (TypeError (ContextNotAbsurd))
+ end
+ | Refl (_, ty) ->
+ TyEq (ty, ty)
+ | Use (_, t, u) ->
+ begin
+ match env.equations with
+ | Inconsistent ->
+ typeof env u
+ | Equations { store ; tyvars } ->
+ let env = copy_env env store tyvars in
+ match typeof env t with
+ | TyEq (ty1, ty2) ->
+ let env = add_equation env ty1 ty2 in
+ typeof env 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 +484,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;
+ enforce_equal env scrutinee_ty ty;
binding_pattern ty pat
| PTuple (_, ps) ->
let tys = as_product scrutinee_ty in
@@ -432,7 +509,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;
+ enforce_equal env scrutinee_ty (TyConstr dty);
binding_pattern arg_type pat
let typeof datatype_env t =
diff --git a/client/FTypeChecker.mli b/client/FTypeChecker.mli
index 6fefd1ef7e113647b05a6544e241dda1f1244e40..047252e8db109cba5535b5bf202aa6a5a87638c3 100644
--- a/client/FTypeChecker.mli
+++ b/client/FTypeChecker.mli
@@ -8,8 +8,11 @@ type type_error =
| NotAnArrow of debruijn_type
| NotAProduct of debruijn_type
| NotAForall of debruijn_type
+ | NotAnEqual of debruijn_type
| UnboundTermVariable of tevar
+ | UnboundTypeVariable of tyvar
| TwoOccurencesOfSameVariable of string
+ | ContextNotAbsurd
(* An arity-related requirement on a certain (sum or product) type
arising during type-checking:
diff --git a/client/Infer.ml b/client/Infer.ml
index 2612eb72395c63fabdcc2a3bf011663e5b1229fa..96e0f2d5a67c3fd5f9f3f9e128bba91402a81755 100644
--- a/client/Infer.ml
+++ b/client/Infer.ml
@@ -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)
diff --git a/client/P.ml b/client/P.ml
index b47b82f9b424e9ea11481bc7356e8e09a7c52199..495c6feb7504f50da1d34736c57a0d69ed0c6e69 100644
--- a/client/P.ml
+++ b/client/P.ml
@@ -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
diff --git a/client/Printer.ml b/client/Printer.ml
index deee934d8e7642aa55a4a34b6512e1f269c41d3b..c05446ecc4048a4678fdb13c6caccb82a635f6ce 100644
--- a/client/Printer.ml
+++ b/client/Printer.ml
@@ -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) =
@@ -143,7 +147,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 ^^
@@ -167,6 +171,11 @@ and print_term_abs t =
| Abs _ ->
let (ps, t) = flatten_abs t in
print_nary_abstraction "fun" print_pattern ps (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 +192,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 +214,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 =
diff --git a/client/Structure.ml b/client/Structure.ml
index 4988ef178cc597fdc115929ab5d83edbe995a79d..52f2c6f6f2625ce4e72680dc05ce17789f4a2518 100644
--- a/client/Structure.ml
+++ b/client/Structure.ml
@@ -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)
diff --git a/client/test/CheckF.ml b/client/test/CheckF.ml
index e51d35388fcd4fb81feacafd3365cd0844ea3fef..8a5c68684af3015a68bd249526505753b2e78008 100644
--- a/client/test/CheckF.ml
+++ b/client/test/CheckF.ml
@@ -1,6 +1,11 @@
open Client
-let test (env : F.nominal_datatype_env) (t : F.nominal_term) =
+(* Typecheck a System F term after a bunch of debugging printing.
+ FTypechecker returns a [result] that is treated by the user-supplied
+ [on_error] and [on_ok] functions. *)
+let check (env : F.nominal_datatype_env) (t : F.nominal_term)
+ : (F.debruijn_type, FTypeChecker.type_error) result
+ =
Printf.printf "Formatting the System F term...\n%!";
let doc = FPrinter.print_term t in
Printf.printf "Pretty-printing the System F term...\n%!";
@@ -11,8 +16,21 @@ let test (env : F.nominal_datatype_env) (t : F.nominal_term) =
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
+ FTypeChecker.typeof_result env t
+
+(* Test a term that is expected to pass type checking. *)
+let test (env : F.nominal_datatype_env) (t : F.nominal_term) =
+ match check env t with
+ | Ok _ ->
+ ()
| Error e ->
- Utils.emit_endline (FPrinter.print_type_error e);
+ Utils.emit_endline (FPrinter.print_type_error e);
+ failwith "Type-checking error."
+
+(* Test a term that is expected to fail type checking. *)
+let test_error (env : F.nominal_datatype_env) (t : F.nominal_term) =
+ match check env t with
+ | Error _ ->
+ ()
+ | Ok _ ->
failwith "Type-checking error."
- | Ok _v -> ()
diff --git a/client/test/TestF.ml b/client/test/TestF.ml
index 1bcf5c6eda8dec66f27a300bbc0d144a74cca41c..7a766dfbd110495df989ea5813ee4b0cf22ebdcf 100644
--- a/client/test/TestF.ml
+++ b/client/test/TestF.ml
@@ -1,141 +1,667 @@
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 nat_env =
+ let nat_typedecl =
+ let open Datatype in {
+ name = Type "nat";
+ type_params = [];
+ data_kind = Variant;
+ labels_descr = [
+ {
+ label_name = Label "O";
+ type_name = Type "nat";
+ arg_type = F.TyProduct [];
+ } ; {
+ label_name = Label "S";
+ type_name = Type "nat";
+ arg_type = F.TyConstr (Type "nat", []);
+ }
+ ]
+ }
+ in
+ Datatype.Env.add_decl bool_env nat_typedecl
+
+let nat_datatype =
+ Datatype.Type "nat", []
+
+(* 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 "Nat";
+ type_name = Type "ty";
+ arg_type = F.TyEq (F.TyVar alpha, F.TyConstr nat_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 nat_env small_gadt_typedecl
+
+let nat_pattern arg_type pat =
+ pvariant
+ (Datatype.Label "Nat")
+ (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(α,nat)).
+ use w in
+ ( O : α )
+ *)
+let cast =
+ let alpha = 0 in
+ tyabs alpha @@
+ abs "w" (F.TyEq (F.TyVar alpha, F.TyConstr nat_datatype)) @@
+ use (var "w") @@
+ annot (variant (Datatype.Label "O") nat_datatype unit) (F.TyVar alpha)
+
+(*
+Λα.
+ λ(n : α ty).
+ match_α n with
+ | Nat p ->
+ use (p : Eq(α,nat)) in (O : α)
+ | Bool p ->
+ use (p : Eq(α,bool)) in (True : α)
+ *)
+let match_gadt_default =
+ let alpha = 0 in
+
+ let nat_pat =
+ nat_pattern [F.TyVar alpha] (pvar "p")
+ in
+
+ let nat_payoff =
+ use
+ (annot
+ (var "p")
+ (F.TyEq (F.TyVar alpha, F.TyConstr nat_datatype)))
+ (annot
+ (variant
+ (Datatype.Label "O")
+ nat_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") [
+ (nat_pat , nat_payoff);
+ (bool_pat , bool_payoff)
+ ]
+
+(*
+(Λα.
+ λ(n : α ty).
+ match_α n with
+ | Nat p ->
+ use (p : Eq(α,nat)) in (O : α)
+ | Bool p ->
+ use (p : Eq(α,bool)) in (True : α))
+nat
+(Nat (refl_nat))
+ *)
+let default_nat =
+ app
+ (tyapp match_gadt_default (F.TyConstr nat_datatype))
+ (variant
+ (Datatype.Label "Nat")
+ (Datatype.Type "ty", [F.TyConstr nat_datatype])
+ (refl (F.TyConstr nat_datatype)))
+
+(*
+(Λα.
+ λ(n : α ty).
+ match_α n with
+ | Nat p ->
+ use (p : Eq(α,nat)) 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
+ | Nat p ->
+ use (p : Eq(α,nat)) in (O (. : unit) : α)
+ | Bool p ->
+ use (p : Eq(α,bool)) in (True (. : unit) : α)
+ *)
+let default_absurd_wrong =
+ let alpha = 0 in
+
+ let nat_pat =
+ nat_pattern [F.TyVar alpha] (pvar "p")
+ in
+
+ let nat_payoff =
+ use (annot (var "p") (F.TyEq (F.TyVar alpha, F.TyConstr nat_datatype))) @@
+ annot
+ (variant
+ (Datatype.Label "O")
+ nat_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") [
+ (nat_pat , nat_payoff);
+ (bool_pat , bool_payoff)
+ ]
+
+(*
+Λα.
+ λ(x : α ty).
+ λ(y : α ty).
+ match (x, y) with
+ | (Nat p1, Nat p2) ->
+ payoff1
+ | (Bool p1, Bool p2) ->
+ payoff2
+ | (Nat p1, Bool p2) ->
+ payoff3
+ | (Bool p1, Nat 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
+
+ (*
+ (Nat p1, Nat p2) ->
+ use (p1 : Eq(α,nat)) in use (p2 : Eq(α,nat)) in payoff1
+ *)
+ let nat_nat_branch =
+ ptuple [
+ (variant_ty "Nat" (pvar "p1"));
+ (variant_ty "Nat" (pvar "p2"));
+ ] ,
+ double_use nat_datatype nat_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
+
+ (*
+ (Nat p1, Bool p2) ->
+ use (p1 : Eq(α,nat)) in use (p2 : Eq(α,bool)) in payoff3
+ *)
+ and nat_bool_branch =
+ ptuple [
+ (variant_ty "Nat" (pvar "p1"));
+ (variant_ty "Bool" (pvar "p2"));
+ ] ,
+ double_use nat_datatype bool_datatype payoff3
+
+ (*
+ (Bool p1, Nat p2) ->
+ use (p1 : Eq(α,bool)) in use (p2 : Eq(α,nat)) in payoff4
+ *)
+ and bool_nat_branch =
+ ptuple [
+ (variant_ty "Bool" (pvar "p1"));
+ (variant_ty "Nat" (pvar "p2"));
+ ] ,
+ double_use bool_datatype nat_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" ]) [
+ nat_nat_branch ;
+ bool_bool_branch;
+ nat_bool_branch;
+ bool_nat_branch;
+ ]
+
+(*
+Λα.
+ λ(x : α ty).
+ λ(y : α ty).
+ match (x, y) with
+ | (Nat p1, Nat p2) ->
+ ()
+ | (Bool p1, Bool p2) ->
+ ()
+ | (Nat p1, Bool p2) ->
+ .
+ | (Bool p1, Nat 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
+ | (Nat p1, Nat p2) ->
+ ()
+ | (Bool p1, Bool p2) ->
+ ()
+ | (Nat p1, Bool p2) ->
+ ()
+ | (Bool p1, Nat 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
+ | (Nat p1, Nat p2) ->
+ .
+ | (Bool p1, Bool p2) ->
+ .
+ | (Nat p1, Bool p2) ->
+ .
+ | (Bool p1, Nat 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" nat_env cast;
+ test_ok_from_ast "default" small_gadt_env match_gadt_default;
+ test_ok_from_ast "default nat" small_gadt_env default_nat;
+ 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;
]
)]