Compare commits
10 Commits
master
...
type-equat
Author | SHA1 | Date |
---|---|---|
Olivier | 19b1d4a6cf | |
Olivier | aed5c4d0fd | |
Olivier | 647587109a | |
Olivier | e48962cd4a | |
Olivier | 47ec0af486 | |
Olivier | 0d65e0621f | |
Olivier | 382c75e51c | |
Olivier | 1ae9154c52 | |
Olivier | 1e797805df | |
Olivier | 685c59ec42 |
|
@ -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`.
|
||||
|
|
19
client/F.ml
19
client/F.ml
|
@ -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)
|
||||
|
|
|
@ -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
|
||||
|
||||
|
|
|
@ -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"
|
||||
|
|
|
@ -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 =
|
||||
|
|
|
@ -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:
|
||||
|
|
|
@ -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)
|
||||
|
|
|
@ -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) }
|
||||
|
||||
|
|
|
@ -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
|
||||
|
||||
|
|
|
@ -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 =
|
||||
|
|
|
@ -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)
|
||||
|
|
|
@ -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."
|
||||
|
|
|
@ -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;
|
||||
]
|
||||
)]
|
||||
|
||||
|
|
|
@ -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]
|
||||
[{}]
|
||||
()
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -12,7 +12,7 @@
|
|||
open Signatures
|
||||
|
||||
module Make
|
||||
(S : OSTRUCTURE)
|
||||
(S : OCSTRUCTURE)
|
||||
(U : MUNIFIER with type 'a structure = 'a S.structure)
|
||||
= struct
|
||||
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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()
|
||||
|
|
|
@ -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
|
||||
|
|
|
@ -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 *)
|
||||
|
|
|
@ -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
|
||||
|
|
Loading…
Reference in New Issue