Compare commits

...

105 Commits

Author SHA1 Message Date
Olivier 13e3eb627d [WIP] change the semantics of absurd.
1 month ago
Olivier 61fe7683b2 TODO : take a look, dune promote.
1 month ago
Olivier 51e1099335 Debugging options passed through the command line.
1 month ago
Olivier 26b35a28fe Change syntax of [use].
1 month ago
Olivier 2575c634d5 The argument of [eq] do not need to be bounded in the graph.
1 month ago
Olivier 658f84a0c0 Add support for Refl in the parser.
1 month ago
Olivier 4389661b23 Yet other tests for type equalities.
1 month ago
Olivier 3d942fb9bd Add tests for absurd.
1 month ago
Olivier 722ce13802 The user needs to provide a path to import type declarations from other midml files.
1 month ago
Olivier 791156bfa3 Fix small bug with inconstent environment.
1 month ago
Olivier c8e08b341b Add comments in [run.t].
1 month ago
Olivier 6cfafe90d2 Rename a test.
1 month ago
Olivier 29068717f0 Promote test suite.
1 month ago
Olivier d0ee82cf86 Promote the test suite.
1 month ago
Olivier 1dca2ed8e6 [Data] Replace error-prone [is_leaf] with its opposite [has_structure].
1 month ago
Olivier 595b1c8295 Modify transitivity test.
1 month ago
Olivier 2b5e84c4af Change the representation of System F type variables to be more informative.
1 month ago
Olivier e18becf2d5 [debug] is an environment variable.
1 month ago
Olivier 11aafb12e3 Delete erase_rigid_vars
1 month ago
Olivier 4434302ece Delete unify_rigid_vars
1 month ago
Olivier 59724cdd22 Store local abstract ids in schemes.
1 month ago
Olivier b14172a078 Fix shrinker.
1 month ago
Olivier ad13a23908 Add tests.
1 month ago
Olivier a8dc970923 Modify [exit_equality].
1 month ago
Olivier 4197f79390 Cosmetic changes.
1 month ago
Olivier 6a403c0578 new_tyvar
1 month ago
Olivier 4c1d37bc66 Fix propagation of scopes.
1 month ago
Olivier 0cdb2226e6 Add support for inconsistent environments.
1 month ago
Olivier 18813ecd42 Erase abstract structures.
1 month ago
Olivier 784c53955e Add debug printing.
1 month ago
Olivier 12bb72f72a Unbind abstracts.
1 month ago
Olivier 1546c05619 Implementing O.abstract in the client.
1 month ago
Olivier ec32370b04 A few changes about abstract types.
1 month ago
Olivier 5c95557e32 Unify all variables with the same abstract structure.
1 month ago
Olivier 898292f7a8 Fix the conjunction of two abstracts with same id.
1 month ago
Olivier 1464ec3d3a Change conversion to deep_ty.
1 month ago
Olivier deef4d4022 Fix printing of equality witness type.
1 month ago
Olivier 8d9be82ac7 Fix propagation of scopes.
1 month ago
Olivier 9b3ea3b1f0 Add tests.
1 month ago
Olivier 866e0f3b17 Debug printing facilities.
1 month ago
Olivier cb4c80d84e Add new error for unbound type variables.
1 month ago
Olivier 34ae8b990c Add filename in error messages.
1 month ago
Olivier 69061b4786 Add Use in ML.
1 month ago
Olivier 66ff395a0b Add Refl in ML.
1 month ago
Olivier dabb2bd699 Add Absurd in ML.
3 months ago
Olivier 7679076de4 Add a new constraint for adding an equality.
3 months ago
Olivier 652e11e214 Inline the Unifier in [Generalization.ml], add support for type equality during unification.
3 months ago
Olivier 890fd03c99 Keep trace of edges (indexed by scopes) in a stack to remove them later.
3 months ago
Olivier c0148519ca Change order of function in [EqEnv].
3 months ago
Olivier d1f3c5f55f Use a single search function.
3 months ago
Olivier 905c703eb8 Module names abbreviations.
3 months ago
Olivier 69d5788ee0 Small change in [get_rigid].
3 months ago
Olivier e8971a1efb Move the module [EqEnv] in the more appropriate file [Generalization.ml].
3 months ago
Olivier 82cb2cec09 More elegant unification algorithm.
3 months ago
Olivier 8cca988db1 Equations environment using a Hashtbl
3 months ago
Olivier ef736a2012 Not sure that this is necessary.
3 months ago
Olivier d59a61f1cb Generalization uses abstract structures for rigid variables.
3 months ago
Olivier 05b3d73873 Abstract structure.
3 months ago
Olivier 712d2f882a Add a scope type in the data.
3 months ago
Olivier c5ae34bb7c Typo.
3 months ago
Olivier 4871534e80 Remove useless [params] argument in [convert].
3 months ago
Olivier ffa2926759 Remove the redundant construct type_annotation.
3 months ago
Olivier 0f2f30d6a2 PAnnot does not introduce new type variables.
3 months ago
Olivier d930badf40 New syntax to introduce flexible variables.
3 months ago
Olivier 831ad5e504 Factorize annotation and rigid variables introduction.
3 months ago
Olivier 0953471d08 Tests for ML.
3 months ago
Gabriel Scherer da7b11b618 small fixes
3 months ago
Olivier 85a8bde8a6 Small fix in the printer.
3 months ago
Olivier 3f41a22455 ML: introduction of rigid variables outside of annotation.
3 months ago
Olivier 87721fd67c 'For' construct in printer.
3 months ago
Gabriel Scherer c9661dfd5f remove the broken gitlab CI script
3 months ago
Gabriel Scherer 75564b3837 CHANGES entry on Solver errors
3 months ago
Gabriel Scherer 3401db210c support for (non-polymorphic) 'let rec' in Infer.ml
3 months ago
Gabriel Scherer 054ca8434b client/F: support "let rec"
3 months ago
Gabriel Scherer 5471bd8d1f client/F: keep bound variable type in 'let'
3 months ago
Gabriel Scherer 3fdb9a141e support 'let rec .. in ..' in the ML parser and AST
3 months ago
SCHERER Gabriel 7a61062b78 Merge branch 'errors-with-ranges' into 'master'
3 months ago
Gabriel Scherer c00f5569d8 include all Infer errors in the testsuite
3 months ago
Gabriel Scherer 85743ed827 use an error type in the Solver as well
3 months ago
Gabriel Scherer 3df581777c consistently use 'loc' instead of 'range' to describe source locations
3 months ago
Gabriel Scherer e31e8032fa consistently emit error locations in Infer error messages
4 months ago
Gabriel Scherer 22dde290e5 include location ranges in FTypeChecker error messages
4 months ago
SCHERER Gabriel 8514e05b91 Merge branch 'env-concat' into 'master'
4 months ago
SCHERER Gabriel 2ab5a617e7 Merge branch 'master' into 'env-concat'
4 months ago
SCHERER Gabriel 95416593ec Merge branch 'variants-error-message' into 'master'
4 months ago
Olivier c47ba76407 [FTypeChecker] More informative error message (and more robust code) when typechecking variants.
4 months ago
Olivier 47283f04f4 Small improvement in a comment.
4 months ago
Olivier 1083149b06 Add tests for pattern-matching.
4 months ago
Olivier 2025ded107 [binding_pattern] add new bindings directly in the environment.
4 months ago
SCHERER Gabriel f3f73388db Merge branch 'type-equations' into 'master'
4 months ago
Olivier 5f23395b5c Add an UnboundTypeVariable error.
4 months ago
Olivier 0debfbb71b More explicit error message printing.
4 months ago
Olivier 98ea579c6a Remove unused equality check and change comments.
4 months ago
Alistair O'Brien 5bd10c668c Apply 1 suggestion(s) to 1 file(s)
4 months ago
Olivier bcb579eafc Change 'int' to more correct 'nat' in the test suite.
4 months ago
Olivier b9749e2b57 Add tests.
4 months ago
Olivier a7006dcbb8 Smart constructors in TestF.ml.
4 months ago
Olivier 66c9de7c55 Add break in printing of annotations.
4 months ago
Olivier eed3db1da6 Comments in F.ml
4 months ago
Olivier 384f9ac3c5 Add Refl / Use in System F.
4 months ago
Olivier 473521d53a Add absurd in F.
4 months ago
Olivier 784bb81952 Equality between types always uses graph translation.
4 months ago
Olivier 6946340570 Define type equalities in [Structure.ml].
4 months ago
Olivier 36980073f3 Add type equality in F.
4 months ago
Olivier 36bad208b0 Remove unused type declaration.
4 months ago

@ -1,10 +0,0 @@
include: 'https://gitlab.com/gasche/gitlab-ocaml-ci-example/-/raw/11c1d7e/.gitlab-ci.yml'
.build-matrix:
parallel:
matrix:
- OCAML_COMPILER: "4.12.0"
variables:
DUNE_DOC_TARGETS: ""

@ -2,6 +2,16 @@
## 2022/06/03
* **Incompatible** changes to the Solver error-handling logic: instead of
raising several different exceptions, the solver now raises a single Error
exception carrying a datatype indicating the error case.
All errors now consistently report the source location when
available (if it was provided when building the constraint). This
improves in particular the error-reporting behavior of our
demonstration client, which is now able to show source locations on
type-checking errors.
* 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

@ -1,5 +1,5 @@
(* tyconstr_id is the name of an datatype constructor.
label_id is the name of a field label or data constructor. *)
(* [tyconstr_id] is the name of an datatype constructor.
[label_id] is the name of a field label or data constructor. *)
type tyconstr_id = Type of string
type label_id = Label of string
@ -46,6 +46,8 @@ module Env = struct
}
exception UnexpectedRecord
exception DeclarationNotFound of tyconstr_id
exception LabelNotFound of label_id
let empty = {
datatypes = TyConstrMap.empty;
@ -64,19 +66,17 @@ module Env = struct
labels = add_labels e.labels tdescr.labels_descr;
}
let find_label { labels ; _ } (Label l) =
LabelMap.find (Label l) labels
let find_decl { datatypes ; _ } (Type tid) =
TyConstrMap.find (Type tid) datatypes
let label_index { labels_descr ; _ } l =
let combine i ldescr = (i, ldescr.label_name) in
List.mapi combine labels_descr
|> List.find (fun (_, l') -> l = l')
|> fst
let () = ignore label_index
let find_label { labels ; _ } label =
try
LabelMap.find label labels
with Not_found ->
raise (LabelNotFound label)
let find_decl { datatypes ; _ } tid =
try
TyConstrMap.find tid datatypes
with Not_found ->
raise (DeclarationNotFound tid)
let map (type b1 b2 t1 t2)
(f : (b1, t1) decl -> (b2, t2) decl)

@ -1,5 +1,5 @@
(* tyconstr_id is the name of an datatype constructor.
label_id is the name of a field label or data constructor. *)
(* [tyconstr_id] is the name of an datatype constructor.
[label_id] is the name of a field label or data constructor. *)
type tyconstr_id = Type of string
type label_id = Label of string
@ -34,6 +34,8 @@ module Env : sig
type ('b, 't) t
exception UnexpectedRecord
exception DeclarationNotFound of tyconstr_id
exception LabelNotFound of label_id
val empty: ('b, 't) t
val add_decl: ('b, 't) t -> ('b, 't) decl -> ('b, 't) t

@ -79,21 +79,6 @@ module Nominal2deBruijn (N : Map.OrderedType) = struct
let current = current + 1 in
{ map; current }
(* [concat env1 env2] extends [env1] with all the bindings of [env2];
bindings of [env2] shadow any binding of the same variable in [env1]. *)
let concat env1 env2 =
(* We need to shift the de Bruijn levels of [env2] (and its
[current] value) by as many bindings as there are in [env1]. *)
let shift _x in1 in2 =
match in2 with
| None -> in1
| Some lvl -> Some (env1.current + lvl)
in
{
current = env1.current + env2.current;
map = M.merge shift env1.map env2.map;
}
end
(* -------------------------------------------------------------------------- *)

@ -49,11 +49,6 @@ module Nominal2deBruijn (N : Map.OrderedType) : sig
to [slide (bump env) x]. *)
val bump: env -> env
(* [concat env1 env2] extends [env1] with all the bindings of [env2];
bindings of [env2] shadow any binding of the same variable in [env1]. *)
val concat: env -> env -> env
end
(* -------------------------------------------------------------------------- *)

@ -4,21 +4,26 @@
(* 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
F. *)
type range =
Lexing.position * Lexing.position
let dummy_range : range =
Lexing.(dummy_pos, dummy_pos)
type loc = Utils.loc
type ('a, 'b) typ =
| TyVar of 'a
@ -27,10 +32,12 @@ 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
type tyvar = int
type tyvar =
string * int
type nominal_type =
(tyvar, tyvar) typ
@ -53,31 +60,56 @@ 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
| Hole of range * ('a, 'b) typ * ('a, 'b) term list
| Annot of range * ('a, 'b) term * ('a, 'b) typ
| Abs of range * tevar * ('a, 'b) typ * ('a, 'b) term
| App of range * ('a, 'b) term * ('a, 'b) term
| Let of range * tevar * ('a, 'b) term * ('a, 'b) term
| TyAbs of range * 'b * ('a, 'b) term
| TyApp of range * ('a, 'b) term * ('a, 'b) typ
| Tuple of range * ('a, 'b) term list
| Proj of range * int * ('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
| Var of loc * tevar
| Hole of loc * ('a, 'b) typ * ('a, 'b) term list
| Annot of loc * ('a, 'b) term * ('a, 'b) typ
| Abs of loc * tevar * ('a, 'b) typ * ('a, 'b) term
| App of loc * ('a, 'b) term * ('a, 'b) term
| Let of loc * rec_status * tevar * ('a, 'b) typ * ('a, 'b) term * ('a, 'b) term
| TyAbs of loc * 'b * ('a, 'b) term
| TyApp of loc * ('a, 'b) term * ('a, 'b) typ
| Tuple of loc * ('a, 'b) term list
| Proj of loc * int * ('a, 'b) term
| LetProd of loc * tevar list * ('a, 'b) term * ('a, 'b) term
| Variant of loc * Datatype.label_id * ('a, 'b) datatype * ('a,'b) term
| Match of loc * ('a,'b) typ * ('a,'b) term * ('a,'b) branch list
| Absurd of loc * ('a,'b) typ
| Refl of loc * ('a,'b) typ
| Use of loc * ('a,'b) term * ('a,'b) typ * ('a,'b) typ * ('a,'b) term
and rec_status = Recursive | Non_recursive
and ('a,'b) branch = ('a,'b) pattern * ('a,'b) term
and ('a,'b) pattern =
| PVar of range * tevar
| PAnnot of range * ('a, 'b) pattern * ('a, 'b) typ
| PWildcard of range
| PTuple of range * ('a,'b) pattern list
| PVariant of range * Datatype.label_id * ('a, 'b) datatype * ('a,'b) pattern
| PVar of loc * tevar
| PAnnot of loc * ('a, 'b) pattern * ('a, 'b) typ
| PWildcard of loc
| PTuple of loc * ('a,'b) pattern list
| PVariant of loc * Datatype.label_id * ('a, 'b) datatype * ('a,'b) pattern
type nominal_term = (tyvar, tyvar) term
type nominal_pattern = (tyvar, tyvar) pattern
@ -90,10 +122,10 @@ type debruijn_term =
(* Constructors. *)
let ftyabs vs t =
List.fold_right (fun v t -> TyAbs (dummy_range, v, t)) vs t
let ftyapp t tys =
List.fold_left (fun t ty -> TyApp (dummy_range, t, ty)) t tys
let ftyabs ~loc vs t =
List.fold_right (fun v t -> TyAbs (loc, v, t)) vs t
let ftyapp ~loc t tys =
List.fold_left (fun t ty -> TyApp (loc, t, ty)) t tys
(* -------------------------------------------------------------------------- *)
@ -149,7 +181,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
(* -------------------------------------------------------------------------- *)
@ -169,36 +204,39 @@ module TypeInTerm : DeBruijn.TRAVERSE
let rec traverse lookup extend env t =
let trav env = traverse lookup extend env in
let trav_ty env ty =
TypeInType.traverse lookup extend env ty in
match t with
| Var (pos, x) ->
Var (pos, x)
| Hole (pos, ty, ts) ->
let ty' = TypeInType.traverse lookup extend env ty in
let ty' = trav_ty env ty in
let ts' = List.map (trav env) ts in
Hole (pos, ty', ts')
| Annot (pos, t, ty) ->
let t' = trav env t
and ty' = TypeInType.traverse lookup extend env ty in
and ty' = trav_ty env ty in
Annot (pos, t', ty')
| Abs (pos, x, ty, t) ->
let ty' = TypeInType.traverse lookup extend env ty
let ty' = trav_ty env ty
and t' = trav env t in
Abs (pos, x, ty', t')
| App (pos, t1, t2) ->
let t1' = trav env t1
and t2' = trav env t2 in
App (pos, t1', t2')
| Let (pos, x, t1, t2) ->
| Let (pos, rec_, x, ty, t1, t2) ->
let ty' = trav_ty env ty in
let t1' = trav env t1
and t2' = trav env t2 in
Let (pos, x, t1', t2')
Let (pos, rec_, x, ty', t1', t2')
| TyAbs (pos, x, t) ->
let env, x = extend env x in
let t' = trav env t in
TyAbs (pos, x, t')
| TyApp (pos, t, ty) ->
let t' = trav env t
and ty' = TypeInType.traverse lookup extend env ty in
and ty' = trav_ty env ty in
TyApp (pos, t', ty')
| Tuple (pos, ts) ->
let ts' = List.map (trav env) ts in
@ -215,10 +253,22 @@ module TypeInTerm : DeBruijn.TRAVERSE
and t' = trav env t in
Variant (pos, lbl, dty', t')
| Match (pos, ty, t, brs) ->
let ty' = TypeInType.traverse lookup extend env ty in
let ty' = trav_ty env ty in
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' = trav_ty env ty in
Absurd (pos, ty')
| Refl (pos, ty) ->
let ty' = trav_ty env ty in
Refl (pos, ty')
| Use (pos, t, ty1, ty2, u) ->
let t' = trav env t in
let ty1' = trav_ty env ty1 in
let ty2' = trav_ty env ty2 in
let u' = trav env u in
Use (pos, t', ty1', ty2', u')
and traverse_datatype lookup extend env (tid, tyargs) =
(tid, List.map (TypeInType.traverse lookup extend env) tyargs)
@ -250,6 +300,11 @@ end
(* -------------------------------------------------------------------------- *)
module TyVar = struct
type t = tyvar
let compare = Stdlib.compare
end
(* Type-in-type weakening and substitution. *)
module Type = struct
@ -257,7 +312,7 @@ module Type = struct
include DeBruijn.MakeSubst(TypeVar)(TypeInType)(TypeInType)
include DeBruijn.MakeTranslate(TypeVar)(TypeInType)(Int)
include DeBruijn.MakeTranslate(TypeVar)(TypeInType)(TyVar)
end
(* -------------------------------------------------------------------------- *)
@ -265,11 +320,11 @@ end
(* Translation of nominal terms to de Bruijn terms. *)
module Term = struct
include DeBruijn.MakeTranslate(TypeVar)(TypeInTerm)(Int)
include DeBruijn.MakeTranslate(TypeVar)(TypeInTerm)(TyVar)
end
module N2DB = DeBruijn.Nominal2deBruijn(Int)
module N2DB = DeBruijn.Nominal2deBruijn(TyVar)
(* Translate a nominal-F datatype description into a De Bruijn version *)
let translate_datatype tdescr =

@ -4,20 +4,26 @@
(* 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
F. *)
type range =
Lexing.position * Lexing.position
val dummy_range: range
type loc = Utils.loc
type ('a, 'b) typ =
| TyVar of 'a
@ -26,12 +32,12 @@ 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
type tyvar =
int
string * int
type nominal_type =
(tyvar, tyvar) typ
@ -55,32 +61,54 @@ 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
type ('a, 'b) term =
| Var of range * tevar
| Hole of range * ('a, 'b) typ * ('a, 'b) term list
| Annot of range * ('a, 'b) term * ('a, 'b) typ
| Abs of range * tevar * ('a, 'b) typ * ('a, 'b) term
| App of range * ('a, 'b) term * ('a, 'b) term
| Let of range * tevar * ('a, 'b) term * ('a, 'b) term
| TyAbs of range * 'b * ('a, 'b) term
| TyApp of range * ('a, 'b) term * ('a, 'b) typ
| Tuple of range * ('a, 'b) term list
| Proj of range * int * ('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
| Var of loc * tevar
| Hole of loc * ('a, 'b) typ * ('a, 'b) term list
| Annot of loc * ('a, 'b) term * ('a, 'b) typ
| Abs of loc * tevar * ('a, 'b) typ * ('a, 'b) term
| App of loc * ('a, 'b) term * ('a, 'b) term
| Let of loc * rec_status * tevar * ('a, 'b) typ * ('a, 'b) term * ('a, 'b) term
| TyAbs of loc * 'b * ('a, 'b) term
| TyApp of loc * ('a, 'b) term * ('a, 'b) typ
| Tuple of loc * ('a, 'b) term list
| Proj of loc * int * ('a, 'b) term
| LetProd of loc * tevar list * ('a, 'b) term * ('a, 'b) term
| Variant of loc * Datatype.label_id * ('a, 'b) datatype * ('a,'b) term
| Match of loc * ('a,'b) typ * ('a,'b) term * ('a,'b) branch list
| Absurd of loc * ('a,'b) typ
| Refl of loc * ('a,'b) typ
| Use of loc * ('a,'b) term * ('a,'b) typ * ('a,'b) typ * ('a,'b) term
and rec_status = Recursive | Non_recursive
and ('a,'b) branch = ('a,'b) pattern * ('a,'b) term
and ('a,'b) pattern =
| PVar of range * tevar
| PAnnot of range * ('a, 'b) pattern * ('a, 'b) typ
| PWildcard of range
| PTuple of range * ('a,'b) pattern list
| PVariant of range * Datatype.label_id * ('a, 'b) datatype * ('a,'b) pattern
| PVar of loc * tevar
| PAnnot of loc * ('a, 'b) pattern * ('a, 'b) typ
| PWildcard of loc
| PTuple of loc * ('a,'b) pattern list
| PVariant of loc * Datatype.label_id * ('a, 'b) datatype * ('a,'b) pattern
type nominal_term =
(tyvar, tyvar) term
@ -98,11 +126,13 @@ type debruijn_term =
(* Constructors. *)
val ftyabs: 'b list -> ('a, 'b) term -> ('a, 'b) term
val ftyapp: ('a, 'b) term -> ('a, 'b) typ list -> ('a, 'b) term
val ftyabs: loc:loc -> 'b list -> ('a, 'b) term -> ('a, 'b) term
val ftyapp: loc:loc -> ('a, 'b) term -> ('a, 'b) typ list -> ('a, 'b) term
(* -------------------------------------------------------------------------- *)
module TyVar : Map.OrderedType with type t = tyvar
module Type : sig
(* Type-in-type weakening and substitution. *)
@ -116,7 +146,7 @@ module Type : sig
(* Translation of nominal types to de Bruijn types. *)
val translate: nominal_type -> debruijn_type
val translate_open: DeBruijn.Nominal2deBruijn(Int).env -> nominal_type -> debruijn_type
val translate_open: DeBruijn.Nominal2deBruijn(TyVar).env -> nominal_type -> debruijn_type
end
(* -------------------------------------------------------------------------- *)

@ -2,14 +2,11 @@
(* We translate from System F to P and then print the P term (resp. type). *)
let new_id : unit -> int =
Inferno.Utils.gensym()
let new_tyvar () =
Printf.sprintf "a%d" (new_id())
let new_tyvar (s,x) =
Printf.sprintf "%s%d" s x
let translate_old_var (x : F.tyvar) =
Printf.sprintf "r%d" x
let translate_old_var ((s,x) : F.tyvar) =
Printf.sprintf "?%s%d" s x
let translate_tyvar env x =
try
@ -33,13 +30,15 @@ let rec translate_type (env : (F.tyvar * P.tyvar) list) (ty : F.nominal_type) :
| F.TyProduct tys ->
P.TyProduct (List.map (self env) tys)
| F.TyForall (x, ty) ->
let alpha = new_tyvar () in
let alpha = new_tyvar x in
P.TyForall (alpha, self ((x, alpha) :: env) ty)
| F.TyMu (x, ty) ->
let alpha = new_tyvar () in
let alpha = new_tyvar x in
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)
@ -52,16 +51,21 @@ let rec translate_term env (t : F.nominal_term) : P.term =
| F.Hole (_, ty, ts) ->
P.Hole (Some (translate_type env ty), List.map (self env) ts)
| F.Annot (_, t, ty) ->
P.Annot (self env t, (P.Flexible, [], translate_type env ty))
P.Annot (self env t, translate_type env ty)
| F.Abs (_, x, ty, t) ->
let annot = P.PAnnot (P.PVar x, (P.Flexible, [], translate_type env ty)) in
P.Abs (annot, self env t)
let x_annot = P.PAnnot (P.PVar x, translate_type env ty) in
P.Abs (x_annot, self env t)
| F.App (_, t1, t2) ->
P.App (self env t1, self env t2)
| F.Let (_, x, t, u) ->
P.Let (P.PVar x, self env t, self env u)
| F.Let (_, rec_, x, ty, t, u) ->
let rec_ = match rec_ with
| F.Recursive -> P.Recursive
| F.Non_recursive -> P.Non_recursive
in
let x_annot = P.PAnnot (P.PVar x, translate_type env ty) in
P.Let (rec_, x_annot, self env t, self env u)
| F.TyAbs (_, x, t) ->
let alpha = new_tyvar () in
let alpha = new_tyvar x in
P.TyAbs (alpha, self ((x, alpha) :: env) t)
| F.TyApp (_, t, ty) ->
P.TyApp (self env t, translate_type env ty)
@ -71,7 +75,7 @@ let rec translate_term env (t : F.nominal_term) : P.term =
P.Proj (i, self env t)
| F.LetProd (_, xs, t, u) ->
let pat = P.PTuple (List.map (fun x -> P.PVar x) xs) in
P.Let (pat , self env t, self env u)
P.Let (P.Non_recursive, pat, self env t, self env u)
| F.Variant (_, lbl, (tid, tys) , t) ->
P.Variant (
lbl,
@ -84,6 +88,16 @@ 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 (Some (translate_type env ty))
| F.Refl (_, ty) ->
P.Refl (Some (translate_type env ty))
| F.Use (_, t, ty1, ty2, u) ->
let t' = self env t in
let ty1' = translate_type env ty1 in
let ty2' = translate_type env ty2 in
let u' = self env u in
P.Use (t', ty1', ty2', u')
and translate_branch env (pat, t) =
(translate_pattern env pat, translate_term env t)
@ -96,7 +110,7 @@ and translate_pattern env pat =
| F.PWildcard _ ->
P.PWildcard
| F.PAnnot (_, p, ty) ->
P.PAnnot (self env p, (P.Flexible, [], translate_type env ty))
P.PAnnot (self env p, translate_type env ty)
| F.PTuple (_, ps) ->
P.PTuple (List.map (self env) ps)
| F.PVariant (_, lbl, (tid, tys), p) ->
@ -118,7 +132,7 @@ let str =
let (++) d1 d2 =
d1 ^^ hardline ^^ d2
let new_id : unit -> F.tyvar =
let new_id : unit -> int =
Inferno.Utils.gensym()
let new_tyvar () : P.tyvar =
@ -155,6 +169,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 +206,28 @@ 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."
| UnexpectedRecord ->
str "Type error." ++
str "A record was expected."
| DeclarationNotFound (Datatype.Type tid) ->
str "Scope error." ++
str "Unknown type declaration : %s." tid
| LabelNotFound (Datatype.Label lid) ->
str "Scope error." ++
str "Unknown variant constructor : %s." lid

@ -6,12 +6,19 @@ type type_error =
| NotAnArrow of debruijn_type
| NotAProduct of debruijn_type
| NotAForall of debruijn_type
| NotAnEqual of debruijn_type
| UnboundTermVariable of tevar
| UnboundTypeVariable of int
| TwoOccurencesOfSameVariable of string
| ContextNotAbsurd
| UnexpectedRecord
| DeclarationNotFound of Datatype.tyconstr_id
| LabelNotFound of Datatype.label_id
and arity_requirement = Index of int | Total of int
exception TypeError of type_error
exception TypeError of loc * type_error
(* -------------------------------------------------------------------------- *)
@ -37,58 +44,99 @@ 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 =
try
(* Obtain the type associated with [x]. *)
let ty = TermVarMap.find x types in
let lookup ~loc { types; names; _ } x =
(* Obtain the type associated with [x]. *)
match TermVarMap.find x types with
| exception Not_found ->
raise (TypeError (loc, UnboundTermVariable x))
| ty ->
(* Find how long ago [x] was bound. *)
let w = N2DB.lookup names x in
(* Shift the type [ty] by this amount, so that it makes sense in the
current scope. *)
Type.lift w 0 ty
with Not_found ->
(* 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 }
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 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; }
with Conflict x -> Error x
names = N2DB.slide names x;
equations; }
let extend_with_tevar_no_dup ~loc ({ types; _ } as env) x ty =
if TermVarMap.mem x types then
raise (TypeError (loc, TwoOccurencesOfSameVariable x));
extend_with_tevar env x ty
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 } }
(* -------------------------------------------------------------------------- *)
@ -101,95 +149,32 @@ let unfold ty =
| _ ->
assert false
let rec as_arrow ty =
let rec as_arrow ~loc ty =
match ty with
| TyArrow (ty1, ty2) ->
ty1, ty2
| TyMu _ ->
as_arrow (unfold ty)
as_arrow ~loc (unfold ty)
| _ ->
raise (TypeError (NotAnArrow ty))
raise (TypeError (loc, NotAnArrow ty))
let rec as_product ty =
let rec as_product ~loc ty =
match ty with
| TyProduct tys ->
tys
| TyMu _ ->
as_product (unfold ty)
as_product ~loc (unfold ty)
| _ ->
raise (TypeError (NotAProduct ty))
raise (TypeError (loc, NotAProduct ty))
let rec as_forall ty =
let rec as_forall ~loc ty =
match ty with
| TyForall ((), ty) ->
ty
| TyMu _ ->
as_forall (unfold ty)
as_forall ~loc (unfold ty)
| _ ->
raise (TypeError (NotAForall 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
raise (TypeError (loc, NotAForall ty))
(* -------------------------------------------------------------------------- *)
@ -197,204 +182,279 @@ let _unsound_equal ty1 ty2 =
(* 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. *)