diff --git a/client/F.ml b/client/F.ml
index f72903d1b3dc7c8fc36eb90c1bfc65f4c320f8b7..88c0c8af569aababc4c421e5f25903025c4f9a13 100644
--- a/client/F.ml
+++ b/client/F.ml
@@ -23,7 +23,7 @@
while the de Bruijn representation is more convenient when type-checking
F. *)
-type range = Utils.range
+type loc = Utils.loc
type ('a, 'b) typ =
| TyVar of 'a
@@ -82,31 +82,31 @@ 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
- | Absurd of range * ('a,'b) typ
- | Refl of range * ('a,'b) typ
- | Use of range * ('a,'b) term * ('a,'b) term
+ | 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 * tevar * ('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) term
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
diff --git a/client/F.mli b/client/F.mli
index 7c062deb710dcdb81e353ed04f2a886e9d51d0e0..82037273fd2cbb990b7b9ca51855b39d9fa8dd76 100644
--- a/client/F.mli
+++ b/client/F.mli
@@ -23,7 +23,7 @@
while the de Bruijn representation is more convenient when type-checking
F. *)
-type range = Utils.range
+type loc = Utils.loc
type ('a, 'b) typ =
| TyVar of 'a
@@ -83,31 +83,31 @@ 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
- | Absurd of range * ('a,'b) typ
- | Refl of range * ('a,'b) typ
- | Use of range * ('a,'b) term * ('a,'b) term
+ | 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 * tevar * ('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) term
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
@@ -125,8 +125,8 @@ type debruijn_term =
(* Constructors. *)
-val ftyabs: loc:Utils.range -> 'b list -> ('a, 'b) term -> ('a, 'b) term
-val ftyapp: loc:Utils.range -> ('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
(* -------------------------------------------------------------------------- *)
diff --git a/client/FTypeChecker.ml b/client/FTypeChecker.ml
index 7a12b7e5569aba1afd8d97413d5d35279d0e2463..4d67c6160b059082e5644932ebc4ac25bbd88dd4 100644
--- a/client/FTypeChecker.ml
+++ b/client/FTypeChecker.ml
@@ -18,7 +18,7 @@ type type_error =
and arity_requirement = Index of int | Total of int
-exception TypeError of range * type_error
+exception TypeError of loc * type_error
(* -------------------------------------------------------------------------- *)
diff --git a/client/FTypeChecker.mli b/client/FTypeChecker.mli
index 8aa38666c6845abf0444f6c18dc2ef91e1591240..1bb09efaca28e017c21362486dd0792abc99a469 100644
--- a/client/FTypeChecker.mli
+++ b/client/FTypeChecker.mli
@@ -24,7 +24,7 @@ type type_error =
*)
and arity_requirement = Index of int | Total of int
-exception TypeError of range * type_error
+exception TypeError of loc * type_error
(* [typeof env t] type-checks the closed term [t] in datatype environment [env]
and constructs its type.
@@ -34,4 +34,4 @@ val typeof: debruijn_datatype_env -> debruijn_term -> debruijn_type
(* Similar to {!typeof}, but returns a [result] type instead of raising an exception. *)
val typeof_result:
- debruijn_datatype_env -> debruijn_term -> (debruijn_type, range * type_error) result
+ debruijn_datatype_env -> debruijn_term -> (debruijn_type, loc * type_error) result
diff --git a/client/Infer.ml b/client/Infer.ml
index 485c7961ff1263d00e011e5e93baf898bf86672f..441136b8120af67997fad7644ef7e59a2d0f6623 100644
--- a/client/Infer.ml
+++ b/client/Infer.ml
@@ -105,7 +105,7 @@ type error =
| VariableConflict of ML.tevar
| VariableScopeEscape
-exception Error of range * error
+exception Error of Utils.loc * error
(* -------------------------------------------------------------------------- *)
@@ -274,8 +274,8 @@ let convert env params ty =
(* -------------------------------------------------------------------------- *)
-(* [get_range t] returns the range of [t]. *)
-let get_range t =
+(* [get_loc t] returns the location of [t]. *)
+let get_loc t =
match t with
| ML.Var (pos, _) | ML.Hole (pos, _) | ML.Abs (pos, _, _)
| ML.App (pos, _, _) | ML.Let (pos, _, _, _) | ML.Annot (pos, _, _)
@@ -283,6 +283,13 @@ let get_range t =
| ML.Variant (pos, _, _) | ML.Match (pos, _, _)
-> pos
+let correlate loc c =
+ (* We (the client) use optional locations,
+ whereas the solver uses non-optional locations. *)
+ match loc with
+ | None -> c
+ | Some loc -> Solver.correlate loc c
+
(* -------------------------------------------------------------------------- *)
(* We will need a type environment to keep trace of term variables that must
@@ -305,7 +312,7 @@ type type_env = (ML.tevar * variable) list
let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.nominal_term co
=
let rec hastype t w =
- let loc = get_range t in
+ let loc = get_loc t in
correlate loc @@
match t with
(* Variable. *)
@@ -628,7 +635,7 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
type; it creates its own using [exist]. And it runs the solver. *)
let hastype (env : ML.datatype_env) (t : ML.term) : F.nominal_term co =
- let loc = get_range t in
+ let loc = get_loc t in
let+ (vs, t) =
correlate loc (let0 (exist (hastype env t))) in
(* [vs] are the binders that we must introduce *)
@@ -648,24 +655,24 @@ let get_tevar x =
let translate_with_hook ~hook ~rectypes env t =
try Solver.solve ~rectypes (hastype_with_hook ~hook env t) with
- | Solver.Unbound (range, x) ->
- raise (Error (range, Unbound (get_tevar x)))
- | Solver.Unify (range, t1, t2) ->
- raise (Error (range, Unify (t1, t2)))
- | Solver.Cycle (range, ty) ->
- raise (Error (range, Cycle ty))
- | Solver.VariableScopeEscape range ->
- raise (Error (range, VariableScopeEscape))
+ | Solver.Unbound (loc, x) ->
+ raise (Error (loc, Unbound (get_tevar x)))
+ | Solver.Unify (loc, t1, t2) ->
+ raise (Error (loc, Unify (t1, t2)))
+ | Solver.Cycle (loc, ty) ->
+ raise (Error (loc, Cycle ty))
+ | Solver.VariableScopeEscape loc ->
+ raise (Error (loc, VariableScopeEscape))
let translate ~rectypes env t =
let ((), res) = translate_with_hook ~hook:ignore ~rectypes env t in
res
-let emit_error range (error : error) =
+let emit_error loc (error : error) =
let emit_type ty =
Utils.emit_endline (FPrinter.print_type ty)
in
- Utils.emit_range range;
+ Utils.emit_loc loc;
begin match error with
| Unbound (s) ->
Printf.printf "Type error: unbound variable \"%s\".\n"
diff --git a/client/Infer.mli b/client/Infer.mli
index 5e2698cdfbe8cee3f46f75fb16efaebeb795ec09..7cb977e760a0e4025010e4cd6a1837512ea6f006 100644
--- a/client/Infer.mli
+++ b/client/Infer.mli
@@ -5,7 +5,7 @@ type error =
| VariableConflict of ML.tevar
| VariableScopeEscape
-exception Error of Utils.range * error
+exception Error of Utils.loc * error
(* Contraint generation, constraint solving and elaboration, combined. *)
val translate: rectypes:bool -> ML.datatype_env -> ML.term -> F.nominal_term
@@ -18,4 +18,4 @@ val translate_with_hook:
hook:(unit -> 'a) ->
rectypes:bool -> ML.datatype_env -> ML.term -> 'a * F.nominal_term
-val emit_error : Utils.range -> error -> unit
+val emit_error : Utils.loc -> error -> unit
diff --git a/client/ML.ml b/client/ML.ml
index 49033951c0cdba7a14f54d51cf8e2aff167eccf5..f91cf3c90a87d7d7559828df864239b0d07cf62d 100644
--- a/client/ML.ml
+++ b/client/ML.ml
@@ -7,20 +7,20 @@ type 'a list = 'a List.t =
| (::) of 'a * 'a list
[@@deriving compare]
-type range = Utils.range
+type loc = Utils.loc
-(* We generate a comparison function [compare_range] that ignores all ranges.
+(* We generate a comparison function [compare_loc] that ignores all locations.
This is useful while testing. *)
-let compare_range _ _ = 0
+let compare_loc _ _ = 0
type tevar = String.t [@@deriving compare]
type tyvar = String.t [@@deriving compare]
type typ =
- | TyVar of range * tyvar
- | TyArrow of range * typ * typ
- | TyProduct of range * typ list
- | TyConstr of range * Datatype.TyConstrId.t * typ list
+ | TyVar of loc * tyvar
+ | TyArrow of loc * typ * typ
+ | TyProduct of loc * typ list
+ | TyConstr of loc * Datatype.TyConstrId.t * typ list
[@@deriving compare]
type rigidity = Flexible | Rigid
@@ -31,27 +31,25 @@ type type_annotation = rigidity * tyvar list * typ [@@deriving compare]
(* some <flexible vars> . <ty> *)
type term =
- | Var of range * tevar
- | Hole of range * term list
- | Abs of range * tevar * term
- | App of range * term * term
- | Let of range * tevar * term * term
- | Annot of range * term * type_annotation
- | Tuple of range * term list
- | LetProd of range * tevar list * term * term
- | Variant of range * Datatype.LabelId.t * term Option.t
- | Match of range * term * branch list
+ | Var of loc * tevar
+ | Hole of loc * term list
+ | Abs of loc * tevar * term
+ | App of loc * term * term
+ | Let of loc * tevar * term * term
+ | Annot of loc * term * type_annotation
+ | Tuple of loc * term list
+ | LetProd of loc * tevar list * term * term
+ | Variant of loc * Datatype.LabelId.t * term Option.t
+ | Match of loc * term * branch list
and branch = pattern * term
and pattern =
- | PVar of range * tevar
- | PWildcard of range
- | PAnnot of range * pattern * type_annotation
- | PVariant of range * Datatype.LabelId.t * pattern Option.t
- | PTuple of range * pattern list
+ | PVar of loc * tevar
+ | PWildcard of loc
+ | PAnnot of loc * pattern * type_annotation
+ | PVariant of loc * Datatype.LabelId.t * pattern Option.t
+ | PTuple of loc * pattern list
[@@deriving compare]
type datatype_env = (tyvar, typ option) Datatype.Env.t
-
-let dummy_pos = (Lexing.( dummy_pos, dummy_pos ))
diff --git a/client/ML2F.ml b/client/ML2F.ml
index 071d07903422b99c2abda804ab0aa1ddb9ec0c53..676090b1adbc0541f5ca7fd6ac494c8fa751275d 100644
--- a/client/ML2F.ml
+++ b/client/ML2F.ml
@@ -38,7 +38,7 @@ let translate_datatype tdescr =
let arg_type =
match ldescr.Datatype.arg_type with
| None ->
- ML.TyProduct (ML.dummy_pos, [])
+ ML.TyProduct (None, [])
| Some ty ->
ty
in
diff --git a/client/MLParser.mly b/client/MLParser.mly
index 91ecc90b8bad0b5cefaccb44068079ec07f189dc..13cda8c43cdcdd4062435dec1d992412a02a520d 100644
--- a/client/MLParser.mly
+++ b/client/MLParser.mly
@@ -39,7 +39,7 @@
%token EOF
-%type<(string list * ML.datatype_env * (string * ML.term) list)> prog
+%type<(string list * ML.datatype_env * (Utils.loc * string * ML.term) list)> prog
%type<ML.term> self_contained_term
%type<ML.datatype_env> self_contained_type_decls
@@ -61,7 +61,7 @@ let self_contained_type_decls :=
(***************** TERMS ***************)
let toplevel_term_decl :=
- | LET ; x = tevar_ ; "=" ; t = term ; { (x, t) }
+ | LET ; x = tevar_ ; "=" ; t = term ; { (Some $loc, x, t) }
let term :=
| ~ = term_abs ; <>
@@ -69,12 +69,12 @@ let term :=
let term_abs :=
| FUN ; xs = list (tevar_) ; "->" ; t = term_abs ;
{
- List.fold_right (fun x t -> Abs ($loc, x, t)) xs t
+ List.fold_right (fun x t -> Abs (Some $loc, x, t)) xs t
}
- | (x, t1, t2) = letin(tevar) ; { Let ($loc, x, t1, t2) }
+ | (x, t1, t2) = letin(tevar) ; { Let (Some $loc, x, t1, t2) }
- | (xs, t1, t2) = letin(tuple(tevar)) ; { LetProd ($loc, xs, t1, t2) }
+ | (xs, t1, t2) = letin(tuple(tevar)) ; { LetProd (Some $loc, xs, t1, t2) }
| ~ = term_app ; <>
@@ -82,30 +82,35 @@ let term_app :=
| t1 = term_app ; t2 = term_atom ;
{
match t1 with
- | Variant ((start_pos, _), l, None) ->
- Variant ((start_pos, $endpos), l, Some t2)
+ | Variant (loc, l, None) ->
+ let loc = match loc with
+ | None -> Some $loc
+ | Some (start_pos, _end_pos) ->
+ Some (start_pos, $endpos)
+ in
+ Variant (loc, l, Some t2)
| _ ->
- App ($loc, t1, t2)
+ App (Some $loc, t1, t2)
}
| ~ = term_atom ; <>
let term_atom :=
- | x = tevar ; { Var ($loc, x) }
+ | x = tevar ; { Var (Some $loc, x) }
- | l = UIDENT ; { Variant ($loc, Datatype.Label l, None) }
+ | l = UIDENT ; { Variant (Some $loc, Datatype.Label l, None) }
- | ts = tuple (term) ; { Tuple ($loc, ts) }
+ | ts = tuple (term) ; { Tuple (Some $loc, ts) }
| MATCH ; t = term ; WITH ;
brs = branches ;
- END ; { Match ($loc, t, brs) }
+ END ; { Match (Some $loc, t, brs) }
| "..."; "["; ts = item_sequence(term, COMMA); "]";
- { Hole ($loc, ts) }
+ { Hole (Some $loc, ts) }
| "(" ; t = term ; ":" ; tyannot = type_annotation ; ")" ;
- { Annot ($loc, t, tyannot) }
+ { Annot (Some $loc, t, tyannot) }
| "(" ; ~ = term ; ")" ; <>
@@ -116,21 +121,21 @@ let branch :=
| pat = pattern ; "->" ; t = term ; { (pat, t) }
let pattern :=
- | l = UIDENT ; pat = pattern_atom ; { PVariant ($loc, Datatype.Label l, Some pat) }
+ | l = UIDENT ; pat = pattern_atom ; { PVariant (Some $loc, Datatype.Label l, Some pat) }
| ~ = pattern_atom ; <>
let pattern_atom :=
- | x = tevar ; { PVar ($loc, x) }
+ | x = tevar ; { PVar (Some $loc, x) }
- | l = UIDENT; { PVariant ($loc, Datatype.Label l, None) }
+ | l = UIDENT; { PVariant (Some $loc, Datatype.Label l, None) }
- | WILDCARD ; { PWildcard $loc }
+ | WILDCARD ; { PWildcard (Some $loc) }
- | ps = tuple (pattern) ; { PTuple ($loc, ps) }
+ | ps = tuple (pattern) ; { PTuple (Some $loc, ps) }
| "(" ; p = pattern ; ":" ; tyannot = type_annotation ; ")" ;
- { PAnnot ($loc, p, tyannot) }
+ { PAnnot (Some $loc, p, tyannot) }
let tevar :=
| ~ = LIDENT ; <>
@@ -146,22 +151,22 @@ let typ :=
let type_arrow :=
| ty1 = type_tyconstr ; "->" ; ty2 = type_arrow ;
- { TyArrow ($loc, ty1, ty2) }
+ { TyArrow (Some $loc, ty1, ty2) }
| ~ = type_tyconstr ; <>
let type_tyconstr :=
| ~ = tyname ; typarams = list (type_atom) ;
- { TyConstr ($loc, tyname, typarams)}
+ { TyConstr (Some $loc, tyname, typarams)}
| ~ = type_atom ; <>
let type_atom :=
- | x = tyvar ; { TyVar ($loc, x) }
+ | x = tyvar ; { TyVar (Some $loc, x) }
| "{" ; tys = separated_list ("*", typ) ; "}" ;
- { TyProduct ($loc, tys) }
+ { TyProduct (Some $loc, tys) }
| "(" ; ~ = typ ; ")" ; <>
diff --git a/client/Utils.ml b/client/Utils.ml
index 4f3c607278df90fbd62b64abaea5167408bd5e6a..90a152233738cb70f98b6bf93a938e56c21d144c 100644
--- a/client/Utils.ml
+++ b/client/Utils.ml
@@ -16,14 +16,14 @@ let emit_endline doc =
emit PPrint.(doc ^^ hardline);
flush stdout
-type range = Lexing.position * Lexing.position
+type loc = (Lexing.position * Lexing.position) option
-let dummy_range : range = Lexing.(dummy_pos, dummy_pos)
+let emit_loc = function
+ | None -> ()
+ | Some range ->
+ print_string (MenhirLib.LexerUtil.range range);
+ flush stdout
-let emit_range range =
- print_string (MenhirLib.LexerUtil.range range);
- flush stdout
-
-let emit_error range doc =
- emit_range range;
+let emit_error loc doc =
+ emit_loc loc;
emit_endline doc
diff --git a/client/Utils.mli b/client/Utils.mli
index 341f7f865ce02f63e7d60ccd14c68e6ddaa8f288..f7da6cb606105365a8acb18cd08a877e0a82ebfe 100644
--- a/client/Utils.mli
+++ b/client/Utils.mli
@@ -16,10 +16,9 @@ val emit : PPrint.document -> unit
end and flushes [stdout]. *)
val emit_endline : PPrint.document -> unit
-type range = Lexing.position * Lexing.position
-val dummy_range : range
-val emit_range : range -> unit
+type loc = (Lexing.position * Lexing.position) option
+val emit_loc : loc -> unit
(* Similar to {!emit_endline}, but starts by printing
- a source location range. *)
-val emit_error : range -> PPrint.document -> unit
+ a source location. *)
+val emit_error : loc -> PPrint.document -> unit
diff --git a/client/bin/midml.ml b/client/bin/midml.ml
index ff1d9908c03e320e42486fc52ca8839110da344f..8aab9ce93c574fbbeb857b3782ef67972c0cade4 100644
--- a/client/bin/midml.ml
+++ b/client/bin/midml.ml
@@ -6,9 +6,10 @@ let rectypes =
let test_ok filename =
match from_file filename with
- | exception (ParsingError range) ->
- Printf.eprintf "%!%sSyntax error.\n%!"
- (LexUtil.range range)
+ | exception (ParsingError loc) ->
+ loc |> Option.iter (fun range ->
+ prerr_string (LexUtil.range range));
+ prerr_endline "Syntax error."
| (datatype_env, t) ->
let rectypes = !rectypes in
let _ = Test.CheckML.test ~verbose:true ~rectypes datatype_env t in ()
diff --git a/client/test/CheckF.ml b/client/test/CheckF.ml
index 0614a8931e560f963321d2e8c53451f1fdfaa6ee..7ff73b8c0beae8e72f687d9dde95c257f043511d 100644
--- a/client/test/CheckF.ml
+++ b/client/test/CheckF.ml
@@ -4,7 +4,7 @@ open Client
FTypechecker returns a [result] that is treated by the user-supplied
[on_error] and [on_ok] functions. *)
let check (env : F.nominal_datatype_env) (t : F.nominal_term)
- : (F.debruijn_type, F.range * FTypeChecker.type_error) result
+ : (F.debruijn_type, Utils.loc * FTypeChecker.type_error) result
=
Printf.printf "Formatting the System F term...\n%!";
let doc = FPrinter.print_term t in
diff --git a/client/test/CheckML.ml b/client/test/CheckML.ml
index 264644a1880331035fce6bd5a1a162286673c1d3..33e9e98a763b3da1a96fb7091c8fcf00da18bd4b 100644
--- a/client/test/CheckML.ml
+++ b/client/test/CheckML.ml
@@ -21,14 +21,14 @@ let equal_term t1 t2 =
(* -------------------------------------------------------------------------- *)
-exception ParsingError of Utils.range
+exception ParsingError of Utils.loc
let wrap parser lexbuf =
let lexbuf = LexUtil.init "test" lexbuf in
try parser MLLexer.read lexbuf
with MLParser.Error ->
let range = Lexing.(lexbuf.lex_start_p, lexbuf.lex_curr_p) in
- raise (ParsingError range)
+ raise (ParsingError (Some range))
(* Main parsing function *)
let parse_term lexbuf = wrap MLParser.self_contained_term lexbuf
@@ -45,10 +45,10 @@ let letify xts =
match xts with
| [] ->
assert false
- | [(_, t)] ->
+ | [(_loc, _last_var, t)] ->
t
- | (x, t) :: xts ->
- ML.Let (ML.dummy_pos, x, t, aux xts)
+ | (loc, x, t) :: xts ->
+ ML.Let (loc, x, t, aux xts)
in
aux xts
@@ -93,9 +93,11 @@ let test_with_args
let s = MLPrinter.to_string t in
let lexbuf = Lexing.from_string s in
match MLParser.self_contained_term MLLexer.read lexbuf with
- | exception (ParsingError range) ->
- Printf.eprintf "%!%sSyntax error on re-parsing.\n%!"
- (LexUtil.range range);
+ | exception (ParsingError loc) ->
+ loc |> Option.iter (fun range ->
+ prerr_string (LexUtil.range range)
+ );
+ prerr_endline "Syntax error on re-parsing.";
false
| t' ->
assert (equal_term t t');
diff --git a/client/test/RandomML.ml b/client/test/RandomML.ml
index b772dea5aaa38b015ba3f56261346bb22539a966..e320cf819ae8332022966caae23286c991d1973c 100644
--- a/client/test/RandomML.ml
+++ b/client/test/RandomML.ml
@@ -14,36 +14,33 @@ let split n st =
open QCheck.Gen
-let pos =
- ML.dummy_pos
-
let int2var k =
"x" ^ string_of_int k
let var x =
- ML.Var (pos, int2var x)
+ ML.Var (None, int2var x)
let bind k =
int2var <$> pure k
let abs self k n =
let+ x, t = pair (bind k) (self (k + 1, n - 1))
- in ML.Abs (pos, x, t)
+ in ML.Abs (None, x, t)
let app self k n =
let* n1, n2 = split (n - 1) in
let+ t1, t2 = pair (self (k, n1)) (self (k, n2))
- in ML.App (pos, t1, t2)
+ in ML.App (None, t1, t2)
let let_ self k n =
let* n1, n2 = split (n - 1) in
let+ x, t1, t2 = triple (bind k) (self (k, n1)) (self (k + 1, n2))
- in ML.Let (pos, x, t1, t2)
+ in ML.Let (None, x, t1, t2)
let pair self k n =
let* n1, n2 = split (n - 1) in
let+ t1, t2 = pair (self (k, n1)) (self (k, n2))
- in ML.Tuple (pos, [t1; t2])
+ in ML.Tuple (None, [t1; t2])
let let_pair self k n =
let* n1, n2 = split (n - 1) in
@@ -53,11 +50,11 @@ let let_pair self k n =
(bind (k + 1))
(self (k, n1))
(self (k + 2, n2))
- in ML.LetProd (pos, [x1; x2], t1, t2)
+ in ML.LetProd (None, [x1; x2], t1, t2)
let annot self k n =
let+ t = self (k, n - 1) in
- ML.Annot (pos, t, (ML.Flexible, ["'a"], ML.TyVar (pos, "'a")))
+ ML.Annot (None, t, (ML.Flexible, ["'a"], ML.TyVar (None, "'a")))
let term = fix (fun self (k, n) ->
if n = 0 then begin
diff --git a/client/test/TestF.ml b/client/test/TestF.ml
index d9c7f5bc174dd1653a4e30124a08485249b561d1..c2e431fd5d84947719639e6c92a60c7c6b53ea8f 100644
--- a/client/test/TestF.ml
+++ b/client/test/TestF.ml
@@ -1,7 +1,5 @@
open Client
-let dummy_range = Utils.dummy_range
-
(* -------------------------------------------------------------------------- *)
(* AST helper functions *)
@@ -10,64 +8,64 @@ let (-->) ty1 ty2 =
F.TyArrow (ty1, ty2)
let unit =
- F.Tuple (dummy_range, [])
+ F.Tuple (None, [])
let unit_type =
F.TyProduct []
let unit_pattern =
- F.PTuple (dummy_range, [])
+ F.PTuple (None, [])
let var x =
- F.(Var (dummy_range, x))
+ F.(Var (None, x))
let annot ty t =
- F.(Annot (dummy_range, ty, t))
+ F.(Annot (None, ty, t))
let abs x ty t =
- F.(Abs (dummy_range, x, ty, t))
+ F.(Abs (None, x, ty, t))
let app t u =
- F.(App (dummy_range, t, u))
+ F.(App (None, t, u))
let tyabs x t =
- F.(TyAbs (dummy_range, x, t))
+ F.(TyAbs (None, x, t))
let tyapp t ty =
- F.(TyApp (dummy_range, t, ty))
+ F.(TyApp (None, t, ty))
let tuple ts =
- F.(Tuple (dummy_range, ts))
+ F.(Tuple (None, ts))
let letprod xs t u =
- F.(LetProd (dummy_range, xs, t, u))
+ F.(LetProd (None, xs, t, u))
let variant lbl datatype t =
- F.(Variant (dummy_range, lbl, datatype, t))
+ F.(Variant (None, lbl, datatype, t))
let match_ ty scrutinee branches =
- F.(Match (dummy_range, ty, scrutinee, branches))
+ F.(Match (None, ty, scrutinee, branches))
let absurd ty =
- F.(Absurd (dummy_range, ty))
+ F.(Absurd (None, ty))
let refl ty =
- F.(Refl (dummy_range, ty))
+ F.(Refl (None, ty))
let use t u =
- F.(Use (dummy_range, t, u))
+ F.(Use (None, t, u))
let pvar x =
- F.(PVar (dummy_range, x))
+ F.(PVar (None, x))
let pwildcard =
- F.(PWildcard dummy_range)
+ F.(PWildcard None)
let ptuple ps =
- F.(PTuple (dummy_range, ps))
+ F.(PTuple (None, ps))
let pvariant lbl datatype t =
- F.(PVariant (dummy_range, lbl, datatype, t))
+ F.(PVariant (None, lbl, datatype, t))
(* -------------------------------------------------------------------------- *)
diff --git a/client/test/TestML.ml b/client/test/TestML.ml
index 1d690c818198f6a93b7c044f8c829980b155dae2..c55da53331e7229f8aff1a9a476d3e6fd23fd0c6 100644
--- a/client/test/TestML.ml
+++ b/client/test/TestML.ml
@@ -2,57 +2,55 @@ open Client
(* A few manually constructed terms. *)
-let dummy_pos = ML.dummy_pos
-
let hole =
- ML.Hole (dummy_pos, [])
+ ML.Hole (None, [])
let x =
- ML.Var (dummy_pos, "x")
+ ML.Var (None, "x")
let y =
- ML.Var (dummy_pos, "y")
+ ML.Var (None, "y")
let id =
- ML.Abs (dummy_pos, "x", x)
+ ML.Abs (None, "x", x)
let delta =
- ML.Abs (dummy_pos, "x", ML.App (dummy_pos, x, x))
+ ML.Abs (None, "x", ML.App (None, x, x))
(* unused *)
let _deltadelta =
- ML.App (dummy_pos, delta, delta)
+ ML.App (None, delta, delta)
let idid =
- ML.App (dummy_pos, id, id)
+ ML.App (None, id, id)
let k =
- ML.Abs (dummy_pos, "x", ML.Abs (dummy_pos, "y", x))
+ ML.Abs (None, "x", ML.Abs (None, "y", x))
let genid =
- ML.Let (dummy_pos, "x", id, x)
+ ML.Let (None, "x", id, x)
let genidid =
- ML.Let (dummy_pos, "x", id, ML.App (dummy_pos, x, x))
+ ML.Let (None, "x", id, ML.App (None, x, x))
let genkidid =
- ML.Let (dummy_pos, "x", ML.App (dummy_pos, k, id), ML.App (dummy_pos, x, id))
+ ML.Let (None, "x", ML.App (None, k, id), ML.App (None, x, id))
let genkidid2 =
- ML.Let (dummy_pos, "x", ML.App (dummy_pos, ML.App (dummy_pos, k, id), id), x)
+ ML.Let (None, "x", ML.App (None, ML.App (None, k, id), id), x)
(* unused *)
let _app_pair = (* ill-typed *)
- ML.App (dummy_pos, ML.Tuple (dummy_pos, [id; id]), id)
+ ML.App (None, ML.Tuple (None, [id; id]), id)
let unit =
- ML.Tuple (dummy_pos, [])
+ ML.Tuple (None, [])
(* "let x1 = (...[], ...[]) in ...[] x1" *)
let regression1 =
- ML.Let (dummy_pos, "x1", ML.Tuple (dummy_pos, [ ML.Hole (dummy_pos, []) ;
- ML.Hole (dummy_pos, []) ]),
- ML.App (dummy_pos, ML.Hole (dummy_pos, []), ML.Var (dummy_pos, "x1")))
+ ML.Let (None, "x1", ML.Tuple (None, [ ML.Hole (None, []) ;
+ ML.Hole (None, []) ]),
+ ML.App (None, ML.Hole (None, []), ML.Var (None, "x1")))
(* "let f = fun x ->
let g = fun y -> (x, y) in
@@ -61,34 +59,34 @@ let regression1 =
fun x -> fun y -> f" *)
let regression2 =
ML.(
- Let (dummy_pos,
+ Let (None,
"f",
- Abs (dummy_pos,
+ Abs (None,
"x",
- Let (dummy_pos,
+ Let (None,
"g",
- Abs (dummy_pos,
+ Abs (None,
"y",
- Tuple (dummy_pos, [x; y])
+ Tuple (None, [x; y])
),
- Var (dummy_pos, "g")
+ Var (None, "g")
)),
- Abs(dummy_pos,
+ Abs(None,
"x",
- Abs(dummy_pos,
+ Abs(None,
"y",
- Var (dummy_pos, "f"))))
+ Var (None, "f"))))
)
let abs_match_with =
ML.(
Abs(
- dummy_pos,
+ None,
"x",
Match(
- dummy_pos,
- Tuple (dummy_pos, []),
- [ (PTuple (dummy_pos, []), Tuple (dummy_pos, [])) ]
+ None,
+ Tuple (None, []),
+ [ (PTuple (None, []), Tuple (None, [])) ]
)
)
)
@@ -110,43 +108,43 @@ let option_env =
} ; {
label_name = Label "Some";
type_name = Type "option";
- arg_type = Some (ML.TyVar (dummy_pos,"'a"));
+ arg_type = Some (ML.TyVar (None,"'a"));
}
]
} in
Datatype.Env.add_decl Datatype.Env.empty option_typedecl
-let none = ML.Variant (dummy_pos, Datatype.Label "None" , None )
+let none = ML.Variant (None, Datatype.Label "None" , None )
let some =
ML.Variant (
- dummy_pos,
+ None,
Datatype.Label "Some",
Some id
)
let match_none = ML.(
- Match (dummy_pos, none, [
- PVariant (dummy_pos, Datatype.Label "None", None), none ;
- PVariant (dummy_pos, Datatype.Label "Some", Some (PVar (dummy_pos, "x"))), x ;
+ Match (None, none, [
+ PVariant (None, Datatype.Label "None", None), none ;
+ PVariant (None, Datatype.Label "Some", Some (PVar (None, "x"))), x ;
])
)
let match_some = ML.(
- Match (dummy_pos, some, [
- PVariant (dummy_pos, Datatype.Label "None", None), none ;
- PVariant (dummy_pos, Datatype.Label "Some", Some (PWildcard dummy_pos)), none
+ Match (None, some, [
+ PVariant (None, Datatype.Label "None", None), none ;
+ PVariant (None, Datatype.Label "Some", Some (PWildcard None)), none
])
)
let match_some_annotated = ML.(
- Match (dummy_pos, some, [
- ( PVariant (dummy_pos, Datatype.Label "None", None), none );
- ( PAnnot (dummy_pos,
- PVariant (dummy_pos, Datatype.Label "Some",
- Some (PWildcard dummy_pos)),
- (Flexible, ["'a"], TyConstr (dummy_pos, Datatype.Type "option",
- [ TyVar (dummy_pos, "'a") ]))),
+ Match (None, some, [
+ ( PVariant (None, Datatype.Label "None", None), none );
+ ( PAnnot (None,
+ PVariant (None, Datatype.Label "Some",
+ Some (PWildcard None)),
+ (Flexible, ["'a"], TyConstr (None, Datatype.Type "option",
+ [ TyVar (None, "'a") ]))),
none );
])
)
@@ -168,11 +166,11 @@ let list_env =
} ; {
label_name = Label "Cons";
type_name = Type "list";
- arg_type = Some (ML.(TyProduct (dummy_pos,
- [ TyVar (dummy_pos, "'a") ;
- TyConstr (dummy_pos,
+ arg_type = Some (ML.(TyProduct (None,
+ [ TyVar (None, "'a") ;
+ TyConstr (None,
Type "list",
- [ TyVar (dummy_pos, "'a") ])
+ [ TyVar (None, "'a") ])
]
)));
}
@@ -181,35 +179,35 @@ let list_env =
Datatype.Env.add_decl option_env list_typedecl
-let nil = ML.Variant (dummy_pos, Datatype.Label "Nil" , None )
+let nil = ML.Variant (None, Datatype.Label "Nil" , None )
let cons =
ML.Variant (
- dummy_pos,
+ None,
Datatype.Label "Cons",
- Some (ML.Tuple (dummy_pos, [ id ; nil ]))
+ Some (ML.Tuple (None, [ id ; nil ]))
)
(* unused *)
let _list_annotated =
let open ML in
Annot (
- dummy_pos,
+ None,
Variant (
- dummy_pos,
+ None,
Datatype.Label "Cons",
- Some (Tuple (dummy_pos, [
- Annot (dummy_pos, id,
- (Flexible, ["'a"], TyArrow (dummy_pos,
- TyVar (dummy_pos, "'a"),
- TyVar (dummy_pos, "'a"))));
+ Some (Tuple (None, [
+ Annot (None, id,
+ (Flexible, ["'a"], TyArrow (None,
+ TyVar (None, "'a"),
+ TyVar (None, "'a"))));
nil ]))
),
- (Flexible, ["'a"; "'b"], TyConstr (dummy_pos,
+ (Flexible, ["'a"; "'b"], TyConstr (None,
Datatype.Type "list",
- [TyArrow (dummy_pos,
- TyVar (dummy_pos, "'a"),
- TyVar (dummy_pos, "'b"))]))
+ [TyArrow (None,
+ TyVar (None, "'a"),
+ TyVar (None, "'b"))]))
)
(* tree *)
@@ -229,10 +227,10 @@ let tree_env =
} ; {
label_name = Label "Node";
type_name = Type "tree";
- arg_type = Some (ML.(TyProduct (dummy_pos, [
- TyConstr (dummy_pos, Type "tree", [ TyVar (dummy_pos, "'a") ]);
- TyVar (dummy_pos, "'a");
- TyConstr (dummy_pos, Type "tree", [ TyVar (dummy_pos, "'a") ]);
+ arg_type = Some (ML.(TyProduct (None, [
+ TyConstr (None, Type "tree", [ TyVar (None, "'a") ]);
+ TyVar (None, "'a");
+ TyConstr (None, Type "tree", [ TyVar (None, "'a") ]);
])))
}
];
@@ -240,13 +238,13 @@ let tree_env =
Datatype.Env.add_decl list_env tree_typedecl
-let leaf = ML.Variant (dummy_pos, Datatype.Label "Leaf" , None )
+let leaf = ML.Variant (None, Datatype.Label "Leaf" , None )
let node =
ML.Variant (
- dummy_pos,
+ None,
Datatype.Label "Node",
- Some (ML.Tuple (dummy_pos, [
+ Some (ML.Tuple (None, [
leaf ;
id ;
leaf ;
@@ -353,25 +351,25 @@ let test_abs_match_with () =
test_ok "fun x -> match () with () -> () end" abs_match_with
let test_let () =
- test_ok "let y = fun x -> x in ()" (ML.Let(dummy_pos, "y", id, unit))
+ test_ok "let y = fun x -> x in ()" (ML.Let(None, "y", id, unit))
let test_let_prod_singleton () =
test_ok "let (y,) = (fun x -> x,) in ()"
- (ML.LetProd (dummy_pos, ["y"], ML.Tuple (dummy_pos, [id]), unit))
+ (ML.LetProd (None, ["y"], ML.Tuple (None, [id]), unit))
let test_let_prod () =
test_ok "let (y,z) = (fun x -> x, ()) in ()"
- (ML.LetProd (dummy_pos, ["y";"z"], ML.Tuple (dummy_pos, [id;unit]), unit))
+ (ML.LetProd (None, ["y";"z"], ML.Tuple (None, [id;unit]), unit))
let test_singleton () =
test_ok
"(fun x -> x,)"
- (ML.Tuple (dummy_pos, [id]))
+ (ML.Tuple (None, [id]))
let test_pair_tuple () =
test_ok
"(fun x -> x, fun x -> x)"
- (ML.Tuple (dummy_pos, [id; id]))
+ (ML.Tuple (None, [id; id]))
let option_env_str =
"type option 'a = None | Some of 'a"
@@ -392,8 +390,8 @@ let test_some_pair () =
test_ok
~typedecl:option_env_str
"Some (fun x -> x, fun x -> x)"
- (ML.Variant (dummy_pos, Datatype.Label "Some",
- Some (ML.Tuple (dummy_pos, [id;id]))))
+ (ML.Variant (None, Datatype.Label "Some",
+ Some (ML.Tuple (None, [id;id]))))
let list_env_str = "type list 'a = Nil | Cons of {'a * list 'a}"
@@ -413,17 +411,17 @@ let test_arrow () =
test_ok
~typedecl:"type func 'a 'b = Func of 'a -> 'b"
"Func (fun x -> x)"
- (ML.Variant (dummy_pos, Datatype.Label "Func", Some id))
+ (ML.Variant (None, Datatype.Label "Func", Some id))
let test_match_tuple () =
test_ok
"match (fun x -> x, ()) with (f, ()) -> f end"
(ML.Match
- (dummy_pos,
- ML.Tuple (dummy_pos, [id;unit]),
- [ (ML.PTuple (dummy_pos, [ML.PVar (dummy_pos, "f");
- ML.PTuple (dummy_pos, [])]),
- ML.Var (dummy_pos, "f")) ]
+ (None,
+ ML.Tuple (None, [id;unit]),
+ [ (ML.PTuple (None, [ML.PVar (None, "f");
+ ML.PTuple (None, [])]),
+ ML.Var (None, "f")) ]
))
let test_match_none () =
@@ -464,21 +462,21 @@ let test_regression2 () =
"let f = fun x -> let g = fun y -> (x, y) in g in fun x -> fun y -> f"
regression2
-let a = ML.TyVar (dummy_pos, "'a")
-let b = ML.TyVar (dummy_pos, "'b")
+let a = ML.TyVar (None, "'a")
+let b = ML.TyVar (None, "'b")
let id_annot annot =
- ML.(Annot (dummy_pos, Abs(dummy_pos, "x", Var (dummy_pos, "x")), annot))
+ ML.(Annot (None, Abs(None, "x", Var (None, "x")), annot))
let test_id_rigid () =
test_ok
"(fun x -> x : for 'a. 'a -> 'a)"
- (id_annot (ML.Rigid, ["'a"], ML.TyArrow (dummy_pos, a, a)))
+ (id_annot (ML.Rigid, ["'a"], ML.TyArrow (None, a, a)))
let test_id_flexible () =
test_ok
"(fun x -> x : some 'a 'b. 'a -> 'b)"
- (id_annot (ML.Flexible, ["'a"; "'b"], ML.TyArrow (dummy_pos, a, b)))
+ (id_annot (ML.Flexible, ["'a"; "'b"], ML.TyArrow (None, a, b)))
let test_suite =
let open Alcotest in
diff --git a/client/test/TestMLRandom.ml b/client/test/TestMLRandom.ml
index 618d9a3894c5c95fce510b97f3c74c1d9e580a42..33081fb56b81ce0be96641c8089fa30f06afcb61 100644
--- a/client/test/TestMLRandom.ml
+++ b/client/test/TestMLRandom.ml
@@ -54,7 +54,7 @@ module Shrinker = struct
(p, subst_under_pat p t x u)
let remove_variable t x =
- subst t x (ML.Hole (ML.dummy_pos, []))
+ subst t x (ML.Hole (None, []))
let remove_variables t xs =
List.fold_left remove_variable t xs
@@ -86,12 +86,12 @@ module Shrinker = struct
important to reproduce typing bugs.
So we start with just (t1) and (t2) as shrinking choices,
even though they typically do not preserve typability. *)
- of_list ts <+> return (ML.Hole (ML.dummy_pos, ts)) in
+ of_list ts <+> return (ML.Hole (None, ts)) in
(match t with
| ML.Hole (_, []) ->
empty
| _ ->
- return (ML.Hole (ML.dummy_pos, []))
+ return (ML.Hole (None, []))
) <+> (
match t with
| ML.Var _ ->
diff --git a/src/Solver.ml b/src/Solver.ml
index b9fae2b4e29f29adec3a7bab2fd0f594e6009fab..6ab4e808482c7accb7f6820865b87194e570ab70 100644
--- a/src/Solver.ml
+++ b/src/Solver.ml
@@ -50,7 +50,7 @@ module VarTable = Hashtbl
(* The syntax of constraints. *)
-type range =
+type loc =
Lexing.position * Lexing.position
type shallow_ty =
@@ -74,9 +74,9 @@ type schemes =
elaboration in an elegant way. *)
type _ co =
-| CRange : range * 'a co -> 'a co
- (**The constraint [CRange (range, c)] is equivalent to the constraint [c],
- and is annotated with [range], a range of positions in some piece of
+| CLoc : loc * 'a co -> 'a co
+ (**The constraint [CLoc (loc, c)] is equivalent to the constraint [c],
+ and is annotated with [loc], a source location in some piece of
source code. *)
| CTrue : unit co
@@ -146,10 +146,10 @@ type _ co =
(* -------------------------------------------------------------------------- *)
(* Exceptions. *)
-exception Unbound of range * tevar
-exception Unify of range * O.ty * O.ty
-exception Cycle of range * O.ty
-exception VariableScopeEscape of range
+exception Unbound of loc option * tevar
+exception Unify of loc option * O.ty * O.ty
+exception Cycle of loc option * O.ty
+exception VariableScopeEscape of loc option
(* A pretty-printer for constraints, used while debugging. *)
@@ -178,7 +178,7 @@ module Printer = struct
[conj], [simple]. The [entry] layer is a synonym for [binders] and is
the entry point. *)
- (* [CRange] and [CMap] constructors are ignored by this printer. *)
+ (* [CLoc] and [CMap] constructors are ignored by this printer. *)
let rec entry : type a . a co -> document = fun c ->
binders c
@@ -187,7 +187,7 @@ module Printer = struct
let next = conj in
let self = binders in
group @@ match c with
- | CRange (_, c) ->
+ | CLoc (_, c) ->
self c
| CMap (c, _) ->
self c
@@ -219,7 +219,7 @@ module Printer = struct
let self = conj in
let next = simple in
group @@ match c with
- | CRange (_, c) ->
+ | CLoc (_, c) ->
self c
| CMap (c, _) ->
self c
@@ -231,7 +231,7 @@ module Printer = struct
and simple : type a . a co -> document = fun c ->
let self = simple in
group @@ match c with
- | CRange (_, c) ->
+ | CLoc (_, c) ->
self c
| CMap (c, _) ->
self c
@@ -288,11 +288,11 @@ module Env = struct
let table =
TeVarMap.create 8
- let lookup range x =
+ let lookup ~loc x =
try
TeVarMap.find table x
with Not_found ->
- raise (Unbound (range, x))
+ raise (Unbound (loc, x))
let bind x s =
(* Shadowing allowed. *)
@@ -398,25 +398,25 @@ let decode_scheme (s : G.scheme) : scheme =
A cyclic decoder is used even if [rectypes] is [false]. Indeed, recursive
types can appear before the occurs check has been performed. *)
-let unify range v1 v2 =
+let unify ~loc v1 v2 =
try
U.unify v1 v2
with
| U.Unify (v1, v2) ->
let decode = D.new_cyclic_decoder() in
- raise (Unify (range, decode v1, decode v2))
+ raise (Unify (loc, decode v1, decode v2))
| G.VariableScopeEscape ->
- raise (VariableScopeEscape range)
+ raise (VariableScopeEscape loc)
-let exit range ~rectypes vs =
+let exit ~loc ~rectypes vs =
try
G.exit ~rectypes vs
with
| G.Cycle v ->
let decode = D.new_cyclic_decoder() in
- raise (Cycle (range, decode v))
+ raise (Cycle (loc, decode v))
| G.VariableScopeEscape ->
- raise (VariableScopeEscape range)
+ raise (VariableScopeEscape loc)
(* -------------------------------------------------------------------------- *)
@@ -433,7 +433,7 @@ let exit range ~rectypes vs =
let rec ok : type a . a co -> bool =
function
- | CRange (_, c) ->
+ | CLoc (_, c) ->
ok c
| CTrue | CPure _ ->
true
@@ -478,26 +478,27 @@ type 'a on_sol =
closure of type ['a on_sol], which implements the second phase: it
describes how to compute a result once resolution is successful.
- [solve] is parameterized with an environment (which maps term variables to
- type schemes) and with a range (the range annotation that was most recently
- encountered on the way down). *)
+ [solve] is parameterized with an environment (which maps term
+ variables to type schemes) and with an optional source location
+ (the location annotation that was most recently encountered on the
+ way down). *)
open UVar
-let rec solve : type a . range -> a co -> a on_sol =
- fun range c -> match c with
- | CRange (range, c) ->
- solve range c
+let rec solve : type a . loc:loc option -> a co -> a on_sol =
+ fun ~loc c -> match c with
+ | CLoc (loc, c) ->
+ solve ~loc:(Some loc) c
| CTrue ->
On_sol (fun () -> ())
| CPure x ->
On_sol (fun () -> x)
| CMap (c, f) ->
- let (On_sol r) = solve range c in
+ let (On_sol r) = solve ~loc c in
On_sol (fun () -> f (r ()))
| CConj (c1, c2) ->
- let (On_sol r1) = solve range c1 in
- let (On_sol r2) = solve range c2 in
+ let (On_sol r1) = solve ~loc c1 in
+ let (On_sol r2) = solve ~loc c2 in
On_sol (fun () ->
(* Even though we recommend using semantic actions without side
effects, it seems wise to impose left-to-right evaluation of
@@ -507,11 +508,11 @@ let rec solve : type a . range -> a co -> a on_sol =
a1, a2
)
| CEq (v, w) ->
- unify range (uvar v) (uvar w);
+ unify ~loc (uvar v) (uvar w);
On_sol (fun () -> ())
| CExist (v, s, c) ->
ignore (flexible v s);
- let result = solve range c in
+ let result = solve ~loc c in
uunbind v;
result
| CDecode v ->
@@ -519,16 +520,16 @@ let rec solve : type a . range -> a co -> a on_sol =
On_sol (fun () -> decode uv)
| CInstance (x, w) ->
(* The environment provides a type scheme for [x]. *)
- let s = Env.lookup range x in
+ let s = Env.lookup ~loc x in
(* Instantiating this type scheme yields a variable [v], which we
unify with [w]. It also yields a list of witnesses, which we
record, as they will be useful during the decoding phase. *)
let witnesses, v = G.instantiate s in
- unify range v (uvar w);
+ unify ~loc v (uvar w);
On_sol (fun () -> List.map decode witnesses)
| CDef (x, v, c) ->
Env.bind x (G.trivial (uvar v));
- let a = solve range c in
+ let a = solve ~loc c in
Env.unbind x;
a
| CLet (rs, xs, vs, c1, c2) ->
@@ -542,7 +543,7 @@ let rec solve : type a . range -> a co -> a on_sol =
basically, but they also serve as named entry points. *)
let uvs = List.map (fun v -> flexible v None) vs in
(* Solve the constraint [c1]. *)
- let (On_sol r1) = solve range c1 in
+ let (On_sol r1) = solve ~loc c1 in
(* Ask the generalization engine to perform an occurs check, to adjust
the ranks of the type variables in the young generation (i.e., all
of the type variables that were registered since the call to
@@ -550,7 +551,7 @@ let rec solve : type a . range -> a co -> a on_sol =
our entry points. The generalization engine also produces a list
[gammas] of the young variables that should be universally
quantified here. *)
- let gammas, ss = exit range ~rectypes uvs in
+ let gammas, ss = exit ~loc ~rectypes uvs in
(* All rigid variables of [rs] must be generalizable. This assertion
may be costly and should be removed or disabled in the future. *)
assert (urs |> List.for_all (fun r -> List.mem r gammas));
@@ -558,7 +559,7 @@ let rec solve : type a . range -> a co -> a on_sol =
(* Extend the environment [env]. *)
List.iter2 Env.bind xs ss;
(* Proceed to solve [c2] in the extended environment. *)
- let (On_sol r2) = solve range c2 in
+ let (On_sol r2) = solve ~loc c2 in
List.iter Env.unbind xs;
On_sol (fun () ->
List.map decode_variable gammas,
@@ -578,9 +579,8 @@ let main (type a) (c : a co) : a =
if not (ok c) then
invalid_arg "solve: ill-formed toplevel constraint";
- let range = Lexing.(dummy_pos, dummy_pos) in
(* Phase 1: solve the constraint. *)
- let (On_sol r) = solve range c in
+ let (On_sol r) = solve ~loc:None c in
(* Phase 2: elaborate. *)
r()
@@ -803,8 +803,8 @@ let let0 c1 =
(* Correlation with the source code. *)
-let correlate range c =
- CRange (range, c)
+let correlate loc c =
+ CLoc (loc, c)
(* -------------------------------------------------------------------------- *)
diff --git a/src/Solver.mli b/src/Solver.mli
index 1452dbd2167412f603e0adb63c733eea395a07e8..cb27ff9af6b9b78febf79b893f6eaf8eaf09ca1f 100644
--- a/src/Solver.mli
+++ b/src/Solver.mli
@@ -385,41 +385,40 @@ module Make
(* Correlation with the source code. *)
- (**The type [range] describes a range in some source code. It is not
+ (**The type [loc] describes a range in some source code. It is not
interpreted by the solver. It is used only as part of error reports. *)
- type range =
- Lexing.position * Lexing.position
+ type loc = Lexing.position * Lexing.position
- (**The constraint [correlate range c] is equivalent to [c], but records that
- this constraint is correlated with the range [range] in the source code.
+ (**The constraint [correlate loc c] is equivalent to [c], but records that
+ this constraint is correlated with the source code location [loc].
This information is used in error reports. The exceptions {!Unbound},
- {!Unify}, {!Cycle}, and {!VariableScopeEscape} carry a range: it is the
- nearest range that encloses the abstract syntax tree node where the error
- is detected. *)
- val correlate: range -> 'a co -> 'a co
+ {!Unify}, {!Cycle}, and {!VariableScopeEscape} carry an optional location:
+ it is the nearest location that encloses the abstract syntax tree node
+ where the error is detected. *)
+ val correlate: loc -> 'a co -> 'a co
(** {2 Solving Constraints} *)
(**This exception is raised by {!solve} when an instantiation constraint
[instance x α] refers to an unbound variable [x]. *)
- exception Unbound of range * tevar
+ exception Unbound of loc option * tevar
(**This exception is raised by {!solve} when an equality constraint cannot
be satisfied. It carries two decoded types, representing the equality
constraint that could not be satisfied. *)
- exception Unify of range * ty * ty
+ exception Unify of loc option * ty * ty
(**This exception is raised by {!solve} when a cyclic equality constraint
is detected, if [rectypes] is [false]. It carries a decoded type, which
is a recursive type: that is, this type involves a μ binder. *)
- exception Cycle of range * ty
+ exception Cycle of loc option * ty
(**This exception is raised by {!solve} when a rigid variable escapes its
scope, that is, roughly speaking, when one attempts to unify a rigid
variable with a more ancient flexible variable. For example, attempting
to solve the constraints [∃α. ∀β. α = β] or [∃α. ∀β. ∃γ. α = β → γ]
causes this exception to be raised. *)
- exception VariableScopeEscape of range
+ exception VariableScopeEscape of loc option
(**[solve ~rectypes c] determines whether the constraint [c] is satisfiable,
and if so, computes and returns its semantic value. (The constraint [c]