aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-01-18 15:46:23 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-04-25 00:28:53 +0200
commite8a6467545c2814c9418889201e8be19c0cef201 (patch)
tree7f513d854b76b02f52f98ee0e87052c376175a0f /interp
parent30d3515546cf244837c6340b6b87c5f51e68cbf4 (diff)
[location] Make location optional in Loc.located
This completes the Loc.ghost removal, the idea is to gear the API towards optional, but uniform, location handling. We don't print <unknown> anymore in the case there is no location. This is what the test suite expects. The old printing logic for located items was a bit inconsistent as it sometimes printed <unknown> and other times it printed nothing as the caller checked for `is_ghost` upstream.
Diffstat (limited to 'interp')
-rw-r--r--interp/constrexpr_ops.ml22
-rw-r--r--interp/constrexpr_ops.mli6
-rw-r--r--interp/constrextern.ml66
-rw-r--r--interp/constrintern.ml338
-rw-r--r--interp/dumpglob.ml57
-rw-r--r--interp/dumpglob.mli20
-rw-r--r--interp/implicit_quantifiers.ml32
-rw-r--r--interp/implicit_quantifiers.mli6
-rw-r--r--interp/modintern.ml12
-rw-r--r--interp/notation_ops.ml59
-rw-r--r--interp/reserve.ml4
-rw-r--r--interp/smartlocate.ml12
-rw-r--r--interp/smartlocate.mli2
-rw-r--r--interp/stdarg.mli2
-rw-r--r--interp/topconstr.ml25
-rw-r--r--interp/topconstr.mli4
16 files changed, 338 insertions, 329 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 4b61ab494..ce349a63f 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -236,14 +236,14 @@ let raw_cases_pattern_expr_loc (l, _) = l
let local_binder_loc = function
| CLocalAssum ((loc,_)::_,_,t)
- | CLocalDef ((loc,_),t,None) -> Loc.merge loc (constr_loc t)
- | CLocalDef ((loc,_),b,Some t) -> Loc.merge loc (Loc.merge (constr_loc b) (constr_loc t))
+ | CLocalDef ((loc,_),t,None) -> Loc.merge_opt loc (constr_loc t)
+ | CLocalDef ((loc,_),b,Some t) -> Loc.merge_opt loc (Loc.merge_opt (constr_loc b) (constr_loc t))
| CLocalAssum ([],_,_) -> assert false
| CLocalPattern (loc,_) -> loc
let local_binders_loc bll = match bll with
| [] -> None
- | h :: l -> Some (Loc.merge (local_binder_loc h) (local_binder_loc (List.last bll)))
+ | h :: l -> Loc.merge_opt (local_binder_loc h) (local_binder_loc (List.last bll))
(** Pseudo-constructors *)
@@ -274,27 +274,27 @@ let expand_binders ?loc mkC bl c =
| b :: bl ->
match b with
| CLocalDef ((loc1,_) as n, oty, b) ->
- let env, c = loop ~loc:(Loc.opt_merge loc1 loc) bl c in
+ let env, c = loop ?loc:(Loc.merge_opt loc1 loc) bl c in
let env = add_name_in_env env n in
(env, Loc.tag ?loc @@ CLetIn (n,oty,b,c))
| CLocalAssum ((loc1,_)::_ as nl, bk, t) ->
- let env, c = loop ~loc:(Loc.opt_merge loc1 loc) bl c in
+ let env, c = loop ?loc:(Loc.merge_opt loc1 loc) bl c in
let env = List.fold_left add_name_in_env env nl in
(env, mkC ?loc (nl,bk,t) c)
| CLocalAssum ([],_,_) -> loop ?loc bl c
| CLocalPattern (loc1, (p, ty)) ->
- let env, c = loop ~loc:(Loc.opt_merge loc1 loc) bl c in
+ let env, c = loop ?loc:(Loc.merge_opt loc1 loc) bl c in
let ni = Hook.get fresh_var env c in
let id = (loc1, Name ni) in
let ty = match ty with
| Some ty -> ty
- | None -> Loc.tag ~loc:loc1 @@ CHole (None, IntroAnonymous, None)
+ | None -> Loc.tag ?loc:loc1 @@ CHole (None, IntroAnonymous, None)
in
let e = Loc.tag @@ CRef (Libnames.Ident (loc1, ni), None) in
let c = Loc.tag ?loc @@
CCases
(LetPatternStyle, None, [(e,None,None)],
- [(Loc.tag ~loc:loc1 ([(loc1,[p])], c))])
+ [(Loc.tag ?loc:loc1 ([(loc1,[p])], c))])
in
(ni :: env, mkC ?loc ([id],Default Explicit,ty) c)
in
@@ -316,12 +316,12 @@ let prod_constr_expr c bl = mkCProdN ?loc:(local_binders_loc bl) bl c
let coerce_reference_to_id = function
| Ident (_,id) -> id
| Qualid (loc,_) ->
- CErrors.user_err ~loc ~hdr:"coerce_reference_to_id"
+ CErrors.user_err ?loc ~hdr:"coerce_reference_to_id"
(str "This expression should be a simple identifier.")
let coerce_to_id = function
| _loc, CRef (Ident (loc,id),_) -> (loc,id)
- | a -> CErrors.user_err ~loc:(constr_loc a)
+ | a -> CErrors.user_err ?loc:(constr_loc a)
~hdr:"coerce_to_id"
(str "This expression should be a simple identifier.")
@@ -329,5 +329,5 @@ let coerce_to_name = function
| _loc, CRef (Ident (loc,id),_) -> (loc,Name id)
| loc, CHole (_,_,_) -> (loc,Anonymous)
| a -> CErrors.user_err
- ~loc:(constr_loc a) ~hdr:"coerce_to_name"
+ ?loc:(constr_loc a) ~hdr:"coerce_to_name"
(str "This expression should be a name.")
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 82e4f54b0..d51576c04 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -34,9 +34,9 @@ val binder_kind_eq : binder_kind -> binder_kind -> bool
(** {6 Retrieving locations} *)
-val constr_loc : constr_expr -> Loc.t
-val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t
-val raw_cases_pattern_expr_loc : raw_cases_pattern_expr -> Loc.t
+val constr_loc : constr_expr -> Loc.t option
+val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t option
+val raw_cases_pattern_expr_loc : raw_cases_pattern_expr -> Loc.t option
val local_binders_loc : local_binder_expr list -> Loc.t option
(** {6 Constructors}*)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 5960a6baa..30b81ecc4 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -108,7 +108,7 @@ let is_record indsp =
let encode_record r =
let indsp = global_inductive r in
if not (is_record indsp) then
- user_err ~loc:(loc_of_reference r) ~hdr:"encode_record"
+ user_err ?loc:(loc_of_reference r) ~hdr:"encode_record"
(str "This type is not a structure type.");
indsp
@@ -259,11 +259,11 @@ let make_notation_gen loc ntn mknot mkprim destprim l =
let make_notation loc ntn (terms,termlists,binders as subst) =
if not (List.is_empty termlists) || not (List.is_empty binders) then
- Loc.tag ~loc @@ CNotation (ntn,subst)
+ Loc.tag ?loc @@ CNotation (ntn,subst)
else
make_notation_gen loc ntn
- (fun (loc,ntn,l) -> Loc.tag ~loc @@ CNotation (ntn,(l,[],[])))
- (fun (loc,p) -> Loc.tag ~loc @@ CPrim p)
+ (fun (loc,ntn,l) -> Loc.tag ?loc @@ CNotation (ntn,(l,[],[])))
+ (fun (loc,p) -> Loc.tag ?loc @@ CPrim p)
destPrim terms
let make_pat_notation ?loc ntn (terms,termlists as subst) args =
@@ -293,9 +293,9 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
match pat with
| loc, PatCstr(cstrsp,args,na)
when !Flags.in_debugger||Inductiveops.constructor_has_local_defs cstrsp ->
- let c = extern_reference ~loc Id.Set.empty (ConstructRef cstrsp) in
+ let c = extern_reference ?loc Id.Set.empty (ConstructRef cstrsp) in
let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
- Loc.tag ~loc @@ CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), [])
+ Loc.tag ?loc @@ CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), [])
| _ ->
try
if !Flags.raw_print || !print_no_symbol then raise No_match;
@@ -304,7 +304,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
| None -> raise No_match
| Some key ->
let loc = cases_pattern_loc pat in
- insert_pat_alias ~loc (insert_pat_delimiters ~loc (Loc.tag ~loc @@ CPatPrim p) key) na
+ insert_pat_alias ?loc (insert_pat_delimiters ?loc (Loc.tag ?loc @@ CPatPrim p) key) na
with No_match ->
try
if !Flags.raw_print || !print_no_symbol then raise No_match;
@@ -312,8 +312,8 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
(uninterp_cases_pattern_notations pat)
with No_match ->
match pat with
- | loc, PatVar (Name id) -> Loc.tag ~loc @@ CPatAtom (Some (Ident (loc,id)))
- | loc, PatVar (Anonymous) -> Loc.tag ~loc @@ CPatAtom None
+ | loc, PatVar (Name id) -> Loc.tag ?loc @@ CPatAtom (Some (Ident (loc,id)))
+ | loc, PatVar (Anonymous) -> Loc.tag ?loc @@ CPatAtom None
| loc, PatCstr(cstrsp,args,na) ->
let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
let p =
@@ -330,22 +330,22 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
| (_loc, CPatAtom(None)) :: tail -> ip q tail acc
(* we don't want to have 'x = _' in our patterns *)
| head :: tail -> ip q tail
- ((extern_reference ~loc Id.Set.empty (ConstRef c), head) :: acc)
+ ((extern_reference ?loc Id.Set.empty (ConstRef c), head) :: acc)
in
- Loc.tag ~loc @@ CPatRecord(List.rev (ip projs args []))
+ Loc.tag ?loc @@ CPatRecord(List.rev (ip projs args []))
with
Not_found | No_match | Exit ->
- let c = extern_reference ~loc Id.Set.empty (ConstructRef cstrsp) in
+ let c = extern_reference ?loc Id.Set.empty (ConstructRef cstrsp) in
if !Topconstr.asymmetric_patterns then
if pattern_printable_in_both_syntax cstrsp
- then Loc.tag ~loc @@ CPatCstr (c, None, args)
- else Loc.tag ~loc @@ CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), [])
+ then Loc.tag ?loc @@ CPatCstr (c, None, args)
+ else Loc.tag ?loc @@ CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), [])
else
let full_args = add_patt_for_params (fst cstrsp) args in
match drop_implicits_in_patt (ConstructRef cstrsp) 0 full_args with
- | Some true_args -> Loc.tag ~loc @@ CPatCstr (c, None, true_args)
- | None -> Loc.tag ~loc @@ CPatCstr (c, Some full_args, [])
- in insert_pat_alias ~loc p na
+ | Some true_args -> Loc.tag ?loc @@ CPatCstr (c, None, true_args)
+ | None -> Loc.tag ?loc @@ CPatCstr (c, Some full_args, [])
+ in insert_pat_alias ?loc p na
and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
(tmp_scope, scopes as allscopes) vars =
function
@@ -398,11 +398,11 @@ and extern_notation_pattern (tmp_scope,scopes as allscopes) vars (loc, t) = func
if List.mem keyrule !print_non_active_notations then raise No_match;
match t with
| PatCstr (cstr,_,na) ->
- let p = apply_notation_to_pattern ~loc (ConstructRef cstr)
+ let p = apply_notation_to_pattern ?loc (ConstructRef cstr)
(match_notation_constr_cases_pattern (loc, t) pat) allscopes vars keyrule in
- insert_pat_alias ~loc p na
- | PatVar Anonymous -> Loc.tag ~loc @@ CPatAtom None
- | PatVar (Name id) -> Loc.tag ~loc @@ CPatAtom (Some (Ident (loc,id)))
+ insert_pat_alias ?loc p na
+ | PatVar Anonymous -> Loc.tag ?loc @@ CPatAtom None
+ | PatVar (Name id) -> Loc.tag ?loc @@ CPatAtom (Some (Ident (loc,id)))
with
No_match -> extern_notation_pattern allscopes vars (loc, t) rules
@@ -582,13 +582,13 @@ let rec remove_coercions inctx c =
been confused with ordinary application or would have need
a surrounding context and the coercion to funclass would
have been made explicit to match *)
- if List.is_empty l then a' else Loc.tag ~loc @@ GApp (a',l)
+ if List.is_empty l then a' else Loc.tag ?loc @@ GApp (a',l)
| _ -> c
with Not_found -> c)
| _ -> c
let rec flatten_application = function
- | (loc, GApp ((_, GApp(a,l')),l)) -> flatten_application (Loc.tag ~loc @@ GApp (a,l'@l))
+ | (loc, GApp ((_, GApp(a,l')),l)) -> flatten_application (Loc.tag ?loc @@ GApp (a,l'@l))
| a -> a
(**********************************************************************)
@@ -600,7 +600,7 @@ let extern_possible_prim_token scopes r =
let (sc,n) = uninterp_prim_token r in
match availability_of_prim_token n sc scopes with
| None -> None
- | Some key -> Some (insert_delimiters (Loc.tag ~loc:(loc_of_glob_constr r) @@ CPrim n) key)
+ | Some key -> Some (insert_delimiters (Loc.tag ?loc:(loc_of_glob_constr r) @@ CPrim n) key)
with No_match ->
None
@@ -644,10 +644,10 @@ let rec extern inctx scopes vars r =
let r'' = flatten_application r' in
if !Flags.raw_print || !print_no_symbol then raise No_match;
extern_notation scopes vars r'' (uninterp_notations r'')
- with No_match -> Loc.map_with_loc (fun ~loc -> function
+ with No_match -> Loc.map_with_loc (fun ?loc -> function
| GRef (ref,us) ->
extern_global (select_stronger_impargs (implicits_of_global ref))
- (extern_reference ~loc vars ref) (extern_universes us)
+ (extern_reference ?loc vars ref) (extern_universes us)
| GVar id -> CRef (Ident (loc,id),None)
@@ -701,7 +701,7 @@ let rec extern inctx scopes vars r =
(* we give up since the constructor is not complete *)
| (arg, scopes) :: tail ->
let head = extern true scopes vars arg in
- ip q locs' tail ((extern_reference ~loc Id.Set.empty (ConstRef c), head) :: acc)
+ ip q locs' tail ((extern_reference ?loc Id.Set.empty (ConstRef c), head) :: acc)
in
CRecord (List.rev (ip projs locals args []))
with
@@ -709,7 +709,7 @@ let rec extern inctx scopes vars r =
let args = extern_args (extern true) vars args in
extern_app inctx
(select_stronger_impargs (implicits_of_global ref))
- (Some ref,extern_reference ~loc:rloc vars ref) (extern_universes us) args
+ (Some ref,extern_reference ?loc:rloc vars ref) (extern_universes us) args
end
| _ ->
@@ -781,7 +781,7 @@ let rec extern inctx scopes vars r =
let listdecl =
Array.mapi (fun i fi ->
let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in
- let bl = List.map (extended_glob_local_binder_of_decl ~loc) bl in
+ let bl = List.map (extended_glob_local_binder_of_decl ?loc) bl in
let (assums,ids,bl) = extern_local_binder scopes vars bl in
let vars0 = List.fold_right (name_fold Id.Set.add) ids vars in
let vars1 = List.fold_right (name_fold Id.Set.add) ids vars' in
@@ -798,7 +798,7 @@ let rec extern inctx scopes vars r =
| GCoFix n ->
let listdecl =
Array.mapi (fun i fi ->
- let bl = List.map (extended_glob_local_binder_of_decl ~loc) blv.(i) in
+ let bl = List.map (extended_glob_local_binder_of_decl ?loc) blv.(i) in
let (_,ids,bl) = extern_local_binder scopes vars bl in
let vars0 = List.fold_right (name_fold Id.Set.add) ids vars in
let vars1 = List.fold_right (name_fold Id.Set.add) ids vars' in
@@ -871,7 +871,7 @@ and extern_local_binder scopes vars = function
(assums,ids, CLocalPattern(Loc.tag @@ (p,ty)) :: l)
and extern_eqn inctx scopes vars (loc,(ids,pl,c)) =
- Loc.tag ~loc ([loc,List.map (extern_cases_pattern_in_scope scopes vars) pl],
+ Loc.tag ?loc ([loc,List.map (extern_cases_pattern_in_scope scopes vars) pl],
extern inctx scopes vars c)
and extern_notation (tmp_scope,scopes as allscopes) vars t = function
@@ -943,12 +943,12 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function
extern true (scopt,scl@scopes) vars c, None)
terms in
let a = CRef (Qualid (loc, shortest_qualid_of_syndef vars kn),None) in
- Loc.tag ~loc @@ if List.is_empty l then a else CApp ((None, Loc.tag a),l) in
+ Loc.tag ?loc @@ if List.is_empty l then a else CApp ((None, Loc.tag a),l) in
if List.is_empty args then e
else
let args = fill_arg_scopes args argsscopes scopes in
let args = extern_args (extern true) vars args in
- Loc.tag ~loc @@ explicitize false argsimpls (None,e) args
+ Loc.tag ?loc @@ explicitize false argsimpls (None,e) args
with
No_match -> extern_notation allscopes vars t rules
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 585f03808..a672771b1 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -118,7 +118,7 @@ type internalization_error =
| NonLinearPattern of Id.t
| BadPatternsNumber of int * int
-exception InternalizationError of Loc.t * internalization_error
+exception InternalizationError of internalization_error Loc.located
let explain_variable_capture id id' =
pr_id id ++ str " is dependent in the type of " ++ pr_id id' ++
@@ -271,7 +271,7 @@ let error_expect_binder_notation_type ?loc id =
(pr_id id ++
str " is expected to occur in binding position in the right-hand side.")
-let set_var_scope loc id istermvar env ntnvars =
+let set_var_scope ?loc id istermvar env ntnvars =
try
let isonlybinding,idscopes,typ = Id.Map.find id ntnvars in
if istermvar then isonlybinding := false;
@@ -282,12 +282,12 @@ let set_var_scope loc id istermvar env ntnvars =
| Some (tmp, scope) ->
let s1 = make_current_scope tmp scope in
let s2 = make_current_scope env.tmp_scope env.scopes in
- if not (List.equal String.equal s1 s2) then error_inconsistent_scope ~loc id s1 s2
+ if not (List.equal String.equal s1 s2) then error_inconsistent_scope ?loc id s1 s2
end
in
match typ with
| NtnInternTypeBinder ->
- if istermvar then error_expect_binder_notation_type ~loc id
+ if istermvar then error_expect_binder_notation_type ?loc id
| NtnInternTypeConstr ->
(* We need sometimes to parse idents at a constr level for
factorization and we cannot enforce this constraint:
@@ -302,14 +302,14 @@ let set_type_scope env = {env with tmp_scope = Notation.current_type_scope_name
let reset_tmp_scope env = {env with tmp_scope = None}
-let rec it_mkGProd loc2 env body =
+let rec it_mkGProd ?loc env body =
match env with
- (loc1, (na, bk, t)) :: tl -> it_mkGProd loc2 tl (Loc.tag ~loc:(Loc.merge loc1 loc2) @@ GProd (na, bk, t, body))
+ (loc2, (na, bk, t)) :: tl -> it_mkGProd ?loc:loc2 tl (Loc.tag ?loc:(Loc.merge_opt loc loc2) @@ GProd (na, bk, t, body))
| [] -> body
-let rec it_mkGLambda loc2 env body =
+let rec it_mkGLambda ?loc env body =
match env with
- (loc1, (na, bk, t)) :: tl -> it_mkGLambda loc2 tl (Loc.tag ~loc:(Loc.merge loc1 loc2) @@ GLambda (na, bk, t, body))
+ (loc2, (na, bk, t)) :: tl -> it_mkGLambda ?loc:loc2 tl (Loc.tag ?loc:(Loc.merge_opt loc loc2) @@ GLambda (na, bk, t, body))
| [] -> body
(**********************************************************************)
@@ -371,15 +371,15 @@ let push_name_env ?(global_level=false) ntnvars implargs env =
function
| loc,Anonymous ->
if global_level then
- user_err ~loc (str "Anonymous variables not allowed");
+ user_err ?loc (str "Anonymous variables not allowed");
env
| loc,Name id ->
check_hidden_implicit_parameters id env.impls ;
if Id.Map.is_empty ntnvars && Id.equal id ldots_var
- then error_ldots_var ~loc;
- set_var_scope loc id false env ntnvars;
+ then error_ldots_var ?loc;
+ set_var_scope ?loc id false env ntnvars;
if global_level then Dumpglob.dump_definition (loc,id) true "var"
- else Dumpglob.dump_binding loc id;
+ else Dumpglob.dump_binding ?loc id;
{env with ids = Id.Set.add id env.ids; impls = Id.Map.add id implargs env.impls}
let intern_generalized_binder ?(global_level=false) intern_type lvar
@@ -393,11 +393,11 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar
let ty' = intern_type {env with ids = ids; unb = true} ty in
let fvs = Implicit_quantifiers.generalizable_vars_of_glob_constr ~bound:ids ~allowed:ids' ty' in
let env' = List.fold_left
- (fun env (x, l) -> push_name_env ~global_level lvar (Variable,[],[],[])(*?*) env (l, Name x))
+ (fun env (l, x) -> push_name_env ~global_level lvar (Variable,[],[],[])(*?*) env (l, Name x))
env fvs in
let bl = List.map
- (fun (id, loc) ->
- (loc, (Name id, b, Loc.tag ~loc @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None))))
+ (fun (loc, id) ->
+ (loc, (Name id, b, Loc.tag ?loc @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None))))
fvs
in
let na = match na with
@@ -424,7 +424,7 @@ let intern_assumption intern lvar env nal bk ty =
List.fold_left
(fun (env, bl) (loc, na as locna) ->
(push_name_env lvar impls env locna,
- (loc,(na,k,locate_if_hole ~loc na ty))::bl))
+ (Loc.tag ?loc (na,k,locate_if_hole ?loc na ty))::bl))
(env, []) nal
| Generalized (b,b',t) ->
let env, b = intern_generalized_binder intern_type lvar env (List.hd nal) b b' t ty in
@@ -448,20 +448,20 @@ let intern_local_pattern intern lvar env p =
List.fold_left
(fun env (loc, i) ->
let bk = Default Implicit in
- let ty = Loc.tag ~loc @@ CHole (None, Misctypes.IntroAnonymous, None) in
+ let ty = Loc.tag ?loc @@ CHole (None, Misctypes.IntroAnonymous, None) in
let n = Name i in
let env, _ = intern_assumption intern lvar env [(loc, n)] bk ty in
env)
env (free_vars_of_pat [] p)
-let glob_local_binder_of_extended = Loc.with_loc (fun ~loc -> function
+let glob_local_binder_of_extended = Loc.with_loc (fun ?loc -> function
| GLocalAssum (na,bk,t) -> (na,bk,None,t)
| GLocalDef (na,bk,c,Some t) -> (na,bk,Some c,t)
| GLocalDef (na,bk,c,None) ->
- let t = Loc.tag ~loc @@ GHole(Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) in
+ let t = Loc.tag ?loc @@ GHole(Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) in
(na,bk,Some c,t)
| GLocalPattern (_,_,_,_) ->
- Loc.raise ~loc (Stream.Error "pattern with quote not allowed here.")
+ Loc.raise ?loc (Stream.Error "pattern with quote not allowed here.")
)
let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd")
@@ -469,18 +469,18 @@ let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd"
let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = function
| CLocalAssum(nal,bk,ty) ->
let env, bl' = intern_assumption intern lvar env nal bk ty in
- let bl' = List.map (fun (loc,(na,c,t)) -> Loc.tag ~loc @@ GLocalAssum (na,c,t)) bl' in
+ let bl' = List.map (fun (loc,(na,c,t)) -> Loc.tag ?loc @@ GLocalAssum (na,c,t)) bl' in
env, bl' @ bl
| CLocalDef((loc,na as locna),def,ty) ->
let term = intern env def in
let ty = Option.map (intern env) ty in
(push_name_env lvar (impls_term_list term) env locna,
- (Loc.tag ~loc @@ GLocalDef (na,Explicit,term,ty)) :: bl)
+ (Loc.tag ?loc @@ GLocalDef (na,Explicit,term,ty)) :: bl)
| CLocalPattern (loc,(p,ty)) ->
let tyc =
match ty with
| Some ty -> ty
- | None -> Loc.tag ~loc @@ CHole(None,Misctypes.IntroAnonymous,None)
+ | None -> Loc.tag ?loc @@ CHole(None,Misctypes.IntroAnonymous,None)
in
let env = intern_local_pattern intern lvar env p in
let il = List.map snd (free_vars_of_pat [] p) in
@@ -495,7 +495,7 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio
let bk = Default Explicit in
let _, bl' = intern_assumption intern lvar env [na] bk tyc in
let _,(_,bk,t) = List.hd bl' in
- (env, (Loc.tag ~loc @@ GLocalPattern((cp,il),id,bk,t)) :: bl)
+ (env, (Loc.tag ?loc @@ GLocalPattern((cp,il),id,bk,t)) :: bl)
let intern_generalization intern env lvar loc bk ak c =
let c = intern {env with unb = true} c in
@@ -517,15 +517,15 @@ let intern_generalization intern env lvar loc bk ak c =
| None -> false
in
if pi then
- (fun (id, loc') acc ->
- Loc.tag ~loc:(Loc.merge loc' loc) @@
- GProd (Name id, bk, Loc.tag ~loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
+ (fun (loc', id) acc ->
+ Loc.tag ?loc:(Loc.merge_opt loc' loc) @@
+ GProd (Name id, bk, Loc.tag ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
else
- (fun (id, loc') acc ->
- Loc.tag ~loc:(Loc.merge loc' loc) @@
- GLambda (Name id, bk, Loc.tag ~loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
+ (fun (loc', id) acc ->
+ Loc.tag ?loc:(Loc.merge_opt loc' loc) @@
+ GLambda (Name id, bk, Loc.tag ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
in
- List.fold_right (fun (id, loc as lid) (env, acc) ->
+ List.fold_right (fun (loc, id as lid) (env, acc) ->
let env' = push_name_env lvar (Variable,[],[],[]) env (loc, Name id) in
(env', abs lid acc)) fvs (env,c)
in c'
@@ -566,44 +566,46 @@ let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function
in
(renaming',env), Name id'
-type letin_param =
- | LPLetIn of Loc.t * (Name.t * glob_constr * glob_constr option)
- | LPCases of Loc.t * (cases_pattern * Id.t list) * Id.t
+type letin_param_r =
+ | LPLetIn of Name.t * glob_constr * glob_constr option
+ | LPCases of (cases_pattern * Id.t list) * Id.t
+and letin_param = letin_param_r Loc.located
let make_letins =
List.fold_right
(fun a c ->
match a with
- | LPLetIn (loc,(na,b,t)) ->
- Loc.tag ~loc @@ GLetIn(na,b,t,c)
- | LPCases (loc,(cp,il),id) ->
- let tt = (Loc.tag ~loc @@ GVar id, (Name id,None)) in
- Loc.tag ~loc @@ GCases(Misctypes.LetPatternStyle,None,[tt],[(loc,(il,[cp],c))]))
+ | loc, LPLetIn (na,b,t) ->
+ Loc.tag ?loc @@ GLetIn(na,b,t,c)
+ | loc, LPCases ((cp,il),id) ->
+ let tt = (Loc.tag ?loc @@ GVar id, (Name id,None)) in
+ Loc.tag ?loc @@ GCases(Misctypes.LetPatternStyle,None,[tt],[(loc,(il,[cp],c))]))
let rec subordinate_letins letins = function
(* binders come in reverse order; the non-let are returned in reverse order together *)
(* with the subordinated let-in in writing order *)
| (loc, GLocalDef (na,_,b,t))::l ->
- subordinate_letins (LPLetIn (loc,(na,b,t))::letins) l
+ subordinate_letins ((Loc.tag ?loc @@ LPLetIn (na,b,t))::letins) l
| (loc, GLocalAssum (na,bk,t))::l ->
let letins',rest = subordinate_letins [] l in
letins',((loc,(na,bk,t)),letins)::rest
| (loc, GLocalPattern (u,id,bk,t)) :: l ->
- subordinate_letins (LPCases (loc,u,id)::letins) ([Loc.tag ~loc @@ GLocalAssum (Name id,bk,t)] @ l)
+ subordinate_letins ((Loc.tag ?loc @@ LPCases (u,id))::letins)
+ ([Loc.tag ?loc @@ GLocalAssum (Name id,bk,t)] @ l)
| [] ->
letins,[]
let terms_of_binders bl =
- let rec term_of_pat pt = Loc.map_with_loc (fun ~loc -> function
+ let rec term_of_pat pt = Loc.map_with_loc (fun ?loc -> function
| PatVar (Name id) -> CRef (Ident (loc,id), None)
| PatVar (Anonymous) -> error "Cannot turn \"_\" into a term."
| PatCstr (c,l,_) ->
let r = Qualid (loc,qualid_of_path (path_of_global (ConstructRef c))) in
- let hole = Loc.tag ~loc @@ CHole (None,Misctypes.IntroAnonymous,None) in
+ let hole = Loc.tag ?loc @@ CHole (None,Misctypes.IntroAnonymous,None) in
let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in
CAppExpl ((None,r,None),params @ List.map term_of_pat l)) pt in
let rec extract_variables = function
- | (loc, GLocalAssum (Name id,_,_))::l -> (Loc.tag ~loc @@ CRef (Ident (loc,id), None)) :: extract_variables l
+ | (loc, GLocalAssum (Name id,_,_))::l -> (Loc.tag ?loc @@ CRef (Ident (loc,id), None)) :: extract_variables l
| (loc, GLocalDef (Name id,_,_,_))::l -> extract_variables l
| (loc, GLocalDef (Anonymous,_,_,_))::l
| (loc, GLocalAssum (Anonymous,_,_))::l -> error "Cannot turn \"_\" into a term."
@@ -663,7 +665,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
let bindings = Id.Map.map mk_env terms in
Some (Genintern.generic_substitute_notation bindings arg)
in
- Loc.tag ~loc @@ GHole (knd, naming, arg)
+ Loc.tag ?loc @@ GHole (knd, naming, arg)
| NBinderList (x,y,iter,terminator) ->
(try
(* All elements of the list are in scopes (scopt,subscopes) *)
@@ -681,24 +683,24 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
let a,letins = snd (Option.get binderopt) in
let e = make_letins letins (aux subst' infos c') in
let (loc,(na,bk,t)) = a in
- Loc.tag ~loc @@ GProd (na,bk,t,e)
+ Loc.tag ?loc @@ GProd (na,bk,t,e)
| NLambda (Name id,NHole _,c') when option_mem_assoc id binderopt ->
let a,letins = snd (Option.get binderopt) in
let (loc,(na,bk,t)) = a in
- Loc.tag ~loc @@ GLambda (na,bk,t,make_letins letins (aux subst' infos c'))
+ Loc.tag ?loc @@ GLambda (na,bk,t,make_letins letins (aux subst' infos c'))
(* Two special cases to keep binder name synchronous with BinderType *)
| NProd (na,NHole(Evar_kinds.BinderType na',naming,arg),c')
when Name.equal na na' ->
let subinfos,na = traverse_binder subst avoid subinfos na in
- let ty = Loc.tag ~loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in
- Loc.tag ~loc @@ GProd (na,Explicit,ty,aux subst' subinfos c')
+ let ty = Loc.tag ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in
+ Loc.tag ?loc @@ GProd (na,Explicit,ty,aux subst' subinfos c')
| NLambda (na,NHole(Evar_kinds.BinderType na',naming,arg),c')
when Name.equal na na' ->
let subinfos,na = traverse_binder subst avoid subinfos na in
- let ty = Loc.tag ~loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in
- Loc.tag ~loc @@ GLambda (na,Explicit,ty,aux subst' subinfos c')
+ let ty = Loc.tag ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in
+ Loc.tag ?loc @@ GLambda (na,Explicit,ty,aux subst' subinfos c')
| t ->
- glob_constr_of_notation_constr_with_binders ~loc
+ glob_constr_of_notation_constr_with_binders ?loc
(traverse_binder subst avoid) (aux subst') subinfos t
and subst_var (terms, _binderopt, _terminopt) (renaming, env) id =
(* subst remembers the delimiters stack in the interpretation *)
@@ -708,7 +710,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
intern {env with tmp_scope = scopt;
scopes = subscopes @ env.scopes} a
with Not_found ->
- Loc.tag ~loc (
+ Loc.tag ?loc (
try
GVar (Id.Map.find id renaming)
with Not_found ->
@@ -729,8 +731,8 @@ let make_subst ids l =
let intern_notation intern env lvar loc ntn fullargs =
let ntn,(args,argslist,bll as fullargs) = contract_notation ntn fullargs in
- let ((ids,c),df) = interp_notation ~loc ntn (env.tmp_scope,env.scopes) in
- Dumpglob.dump_notation_location (ntn_loc loc fullargs ntn) ntn df;
+ let ((ids,c),df) = interp_notation ?loc ntn (env.tmp_scope,env.scopes) in
+ Dumpglob.dump_notation_location (ntn_loc ?loc fullargs ntn) ntn df;
let ids,idsl,idsbl = split_by_type ids in
let terms = make_subst ids args in
let termlists = make_subst idsl argslist in
@@ -748,9 +750,9 @@ let string_of_ty = function
| Variable -> "var"
let gvar (loc, id) us = match us with
-| None -> Loc.tag ~loc @@ GVar id
+| None -> Loc.tag ?loc @@ GVar id
| Some _ ->
- user_err ~loc (str "Variable " ++ pr_id id ++
+ user_err ?loc (str "Variable " ++ pr_id id ++
str " cannot have a universe instance")
let intern_var genv (ltacvars,ntnvars) namedctx loc id us =
@@ -758,9 +760,9 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id us =
try
let ty,expl_impls,impls,argsc = Id.Map.find id genv.impls in
let expl_impls = List.map
- (fun id -> Loc.tag ~loc @@ CRef (Ident (loc,id),None), Some (loc,ExplByName id)) expl_impls in
+ (fun id -> Loc.tag ?loc @@ CRef (Ident (loc,id),None), Some (loc,ExplByName id)) expl_impls in
let tys = string_of_ty ty in
- Dumpglob.dump_reference loc "<>" (Id.to_string id) tys;
+ Dumpglob.dump_reference ?loc "<>" (Id.to_string id) tys;
gvar (loc,id) us, make_implicits_list impls, argsc, expl_impls
with Not_found ->
(* Is [id] bound in current term or is an ltac var bound to constr *)
@@ -770,15 +772,15 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id us =
(* Is [id] a notation variable *)
else if Id.Map.mem id ntnvars
then
- (set_var_scope loc id true genv ntnvars; gvar (loc,id) us, [], [], [])
+ (set_var_scope ?loc id true genv ntnvars; gvar (loc,id) us, [], [], [])
(* Is [id] the special variable for recursive notations *)
else if Id.equal id ldots_var
then if Id.Map.is_empty ntnvars
- then error_ldots_var ~loc
+ then error_ldots_var ?loc
else gvar (loc,id) us, [], [], []
else if Id.Set.mem id ltacvars.ltac_bound then
(* Is [id] bound to a free name in ltac (this is an ltac error message) *)
- user_err ~loc ~hdr:"intern_var"
+ user_err ?loc ~hdr:"intern_var"
(str "variable " ++ pr_id id ++ str " should be bound to a term.")
else
(* Is [id] a goal or section variable *)
@@ -789,8 +791,8 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id us =
let ref = VarRef id in
let impls = implicits_of_global ref in
let scopes = find_arguments_scope ref in
- Dumpglob.dump_reference loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var";
- Loc.tag ~loc @@ GRef (ref, us), impls, scopes, []
+ Dumpglob.dump_reference ?loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var";
+ Loc.tag ?loc @@ GRef (ref, us), impls, scopes, []
with e when CErrors.noncritical e ->
(* [id] a goal variable *)
gvar (loc,id) us, [], [], []
@@ -820,11 +822,11 @@ let check_no_explicitation l =
| [] -> ()
| (_, None) :: _ -> assert false
| (_, Some (loc, _)) :: _ ->
- user_err ~loc (str"Unexpected explicitation of the argument of an abbreviation.")
+ user_err ?loc (str"Unexpected explicitation of the argument of an abbreviation.")
let dump_extended_global loc = function
- | TrueGlobal ref -> (*feedback_global loc ref;*) Dumpglob.add_glob loc ref
- | SynDef sp -> Dumpglob.add_glob_kn loc sp
+ | TrueGlobal ref -> (*feedback_global loc ref;*) Dumpglob.add_glob ?loc ref
+ | SynDef sp -> Dumpglob.add_glob_kn ?loc sp
let intern_extended_global_of_qualid (loc,qid) =
let r = Nametab.locate_extended qid in dump_extended_global loc r; r
@@ -833,18 +835,18 @@ let intern_reference ref =
let qid = qualid_of_reference ref in
let r =
try intern_extended_global_of_qualid qid
- with Not_found -> error_global_not_found ~loc:(fst qid) (snd qid)
+ with Not_found -> error_global_not_found ?loc:(fst qid) (snd qid)
in
Smartlocate.global_of_extended_global r
(* Is it a global reference or a syntactic definition? *)
let intern_qualid loc qid intern env lvar us args =
match intern_extended_global_of_qualid (loc,qid) with
- | TrueGlobal ref -> (Loc.tag ~loc @@ GRef (ref, us)), true, args
+ | TrueGlobal ref -> (Loc.tag ?loc @@ GRef (ref, us)), true, args
| SynDef sp ->
let (ids,c) = Syntax_def.search_syntactic_definition sp in
let nids = List.length ids in
- if List.length args < nids then error_not_enough_arguments ~loc;
+ if List.length args < nids then error_not_enough_arguments ?loc;
let args1,args2 = List.chop nids args in
check_no_explicitation args1;
let terms = make_subst ids (List.map fst args1) in
@@ -854,11 +856,11 @@ let intern_qualid loc qid intern env lvar us args =
let c = instantiate_notation_constr loc intern lvar subst infos c in
let c = match us, c with
| None, _ -> c
- | Some _, (loc, GRef (ref, None)) -> Loc.tag ~loc @@ GRef (ref, us)
+ | Some _, (loc, GRef (ref, None)) -> Loc.tag ?loc @@ GRef (ref, us)
| Some _, (loc, GApp ((loc', GRef (ref, None)), arg)) ->
- Loc.tag ~loc @@ GApp (Loc.tag ~loc:loc' @@ GRef (ref, us), arg)
+ Loc.tag ?loc @@ GApp (Loc.tag ?loc:loc' @@ GRef (ref, us), arg)
| Some _, _ ->
- user_err ~loc (str "Notation " ++ pr_qualid qid ++
+ user_err ?loc (str "Notation " ++ pr_qualid qid ++
str " cannot have a universe instance, its expanded head
does not start with a reference")
in
@@ -874,7 +876,7 @@ let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args =
| Qualid (loc, qid) ->
let r,projapp,args2 =
try intern_qualid loc qid intern env ntnvars us args
- with Not_found -> error_global_not_found ~loc qid
+ with Not_found -> error_global_not_found ?loc qid
in
let x, imp, scopes, l = find_appl_head_data r in
(x,imp,scopes,l), args2
@@ -890,7 +892,7 @@ let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args =
(* Extra allowance for non globalizing functions *)
if !interning_grammar || env.unb then
(gvar (loc,id) us, [], [], []), args
- else error_global_not_found ~loc qid
+ else error_global_not_found ?loc qid
let interp_reference vars r =
let (r,_,_,_),_ =
@@ -952,7 +954,7 @@ let rec has_duplicate = function
| x::l -> if Id.List.mem x l then (Some x) else has_duplicate l
let loc_of_lhs lhs =
- Loc.merge (fst (List.hd lhs)) (fst (List.last lhs))
+ Loc.merge_opt (fst (List.hd lhs)) (fst (List.last lhs))
let check_linearity lhs ids =
match has_duplicate ids with
@@ -968,7 +970,7 @@ let check_number_of_pattern loc n l =
let check_or_pat_variables loc ids idsl =
if List.exists (fun ids' -> not (List.eq_set Id.equal ids ids')) idsl then
- user_err ~loc (str
+ user_err ?loc (str
"The components of this disjunctive pattern must bind the same variables.")
(** Use only when params were NOT asked to the user.
@@ -977,7 +979,7 @@ let check_constructor_length env loc cstr len_pl pl0 =
let n = len_pl + List.length pl0 in
if Int.equal n (Inductiveops.constructor_nallargs cstr) then false else
(Int.equal n (Inductiveops.constructor_nalldecls cstr) ||
- (error_wrong_numarg_constructor ~loc env cstr
+ (error_wrong_numarg_constructor ?loc env cstr
(Inductiveops.constructor_nrealargs cstr)))
let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 =
@@ -1002,14 +1004,14 @@ let add_implicits_check_constructor_length env loc c len_pl1 pl2 =
let nargs = Inductiveops.constructor_nallargs c in
let nargs' = Inductiveops.constructor_nalldecls c in
let impls_st = implicits_of_global (ConstructRef c) in
- add_implicits_check_length (error_wrong_numarg_constructor ~loc env c)
+ add_implicits_check_length (error_wrong_numarg_constructor ?loc env c)
nargs nargs' impls_st len_pl1 pl2
let add_implicits_check_ind_length env loc c len_pl1 pl2 =
let nallargs = inductive_nallargs_env env c in
let nalldecls = inductive_nalldecls_env env c in
let impls_st = implicits_of_global (IndRef c) in
- add_implicits_check_length (error_wrong_numarg_inductive ~loc env c)
+ add_implicits_check_length (error_wrong_numarg_inductive ?loc env c)
nallargs nalldecls impls_st len_pl1 pl2
(** Do not raise NotEnoughArguments thanks to preconditions*)
@@ -1020,7 +1022,7 @@ let chop_params_pattern loc ind args with_letin =
assert (nparams <= List.length args);
let params,args = List.chop nparams args in
List.iter (function _, PatVar Anonymous -> ()
- | loc', PatVar _ | loc', PatCstr(_,_,_) -> error_parameter_not_implicit ~loc:loc') params;
+ | loc', PatVar _ | loc', PatCstr(_,_,_) -> error_parameter_not_implicit ?loc:loc') params;
args
let find_constructor loc add_params ref =
@@ -1028,10 +1030,10 @@ let find_constructor loc add_params ref =
| ConstructRef cstr -> cstr
| IndRef _ ->
let error = str "There is an inductive name deep in a \"in\" clause." in
- user_err ~loc ~hdr:"find_constructor" error
+ user_err ?loc ~hdr:"find_constructor" error
| ConstRef _ | VarRef _ ->
let error = str "This reference is not a constructor." in
- user_err ~loc ~hdr:"find_constructor" error
+ user_err ?loc ~hdr:"find_constructor" error
in
cstr, match add_params with
| Some nb_args ->
@@ -1053,7 +1055,7 @@ let check_duplicate loc fields =
match dups with
| [] -> ()
| (r, _) :: _ ->
- user_err ~loc (str "This record defines several times the field " ++
+ user_err ?loc (str "This record defines several times the field " ++
pr_reference r ++ str ".")
(** [sort_fields ~complete loc fields completer] expects a list
@@ -1078,7 +1080,7 @@ let sort_fields ~complete loc fields completer =
let gr = global_reference_of_reference first_field_ref in
(gr, Recordops.find_projection gr)
with Not_found ->
- user_err ~loc:(loc_of_reference first_field_ref) ~hdr:"intern"
+ user_err ?loc:(loc_of_reference first_field_ref) ~hdr:"intern"
(pr_reference first_field_ref ++ str": Not a projection")
in
(* the number of parameters *)
@@ -1109,7 +1111,7 @@ let sort_fields ~complete loc fields completer =
by a let-in in the record declaration
(its value is fixed from other fields). *)
if first_field && not regular && complete then
- user_err ~loc (str "No local fields allowed in a record construction.")
+ user_err ?loc (str "No local fields allowed in a record construction.")
else if first_field then
build_proj_list projs proj_kinds (idx+1) ~acc_first_idx:idx acc
else if not regular && complete then
@@ -1122,7 +1124,7 @@ let sort_fields ~complete loc fields completer =
| None :: projs ->
if complete then
(* we don't want anonymous fields *)
- user_err ~loc (str "This record contains anonymous fields.")
+ user_err ?loc (str "This record contains anonymous fields.")
else
(* anonymous arguments don't appear in proj_kinds *)
build_proj_list projs proj_kinds (idx+1) ~acc_first_idx acc
@@ -1136,13 +1138,13 @@ let sort_fields ~complete loc fields completer =
| (field_ref, field_value) :: fields ->
let field_glob_ref = try global_reference_of_reference field_ref
with Not_found ->
- user_err ~loc:(loc_of_reference field_ref) ~hdr:"intern"
+ user_err ?loc:(loc_of_reference field_ref) ~hdr:"intern"
(str "The field \"" ++ pr_reference field_ref ++ str "\" does not exist.") in
let remaining_projs, (field_index, _) =
let the_proj (idx, glob_ref) = eq_gr field_glob_ref glob_ref in
try CList.extract_first the_proj remaining_projs
with Not_found ->
- user_err ~loc
+ user_err ?loc
(str "This record contains fields of different records.")
in
index_fields fields remaining_projs ((field_index, field_value) :: acc)
@@ -1199,12 +1201,12 @@ let alias_of als = match als.alias_ids with
let rec subst_pat_iterator y t (loc, p) = match p with
| RCPatAtom id ->
- begin match id with Some x when Id.equal x y -> t | _ -> Loc.tag ~loc p end
+ begin match id with Some x when Id.equal x y -> t | _ -> Loc.tag ?loc p end
| RCPatCstr (id,l1,l2) ->
- Loc.tag ~loc @@ RCPatCstr (id, List.map (subst_pat_iterator y t) l1,
+ Loc.tag ?loc @@ RCPatCstr (id, List.map (subst_pat_iterator y t) l1,
List.map (subst_pat_iterator y t) l2)
- | RCPatAlias (p,a) -> Loc.tag ~loc @@ RCPatAlias (subst_pat_iterator y t p,a)
- | RCPatOr pl -> Loc.tag ~loc @@ RCPatOr (List.map (subst_pat_iterator y t) pl)
+ | RCPatAlias (p,a) -> Loc.tag ?loc @@ RCPatAlias (subst_pat_iterator y t p,a)
+ | RCPatOr pl -> Loc.tag ?loc @@ RCPatOr (List.map (subst_pat_iterator y t) pl)
let drop_notations_pattern looked_for =
(* At toplevel, Constructors and Inductives are accepted, in recursive calls
@@ -1214,7 +1216,7 @@ let drop_notations_pattern looked_for =
if top then looked_for g else
match g with ConstructRef _ -> () | _ -> raise Not_found
with Not_found ->
- error_invalid_pattern_notation ~loc ()
+ error_invalid_pattern_notation ?loc ()
in
let test_kind top =
if top then looked_for else function ConstructRef _ -> () | _ -> raise Not_found
@@ -1240,7 +1242,7 @@ let drop_notations_pattern looked_for =
(* Convention: do not deactivate implicit arguments and scopes for further arguments *)
test_kind top g;
let nvars = List.length vars in
- if List.length pats < nvars then error_not_enough_arguments ~loc;
+ if List.length pats < nvars then error_not_enough_arguments ?loc;
let pats1,pats2 = List.chop nvars pats in
let subst = make_subst vars pats1 in
let idspl1 = List.map (in_not false loc scopes (subst, Id.Map.empty) []) args in
@@ -1249,17 +1251,17 @@ let drop_notations_pattern looked_for =
| _ -> raise Not_found)
| TrueGlobal g ->
test_kind top g;
- Dumpglob.add_glob loc g;
+ Dumpglob.add_glob ?loc g;
let (_,argscs) = find_remaining_scopes [] pats g in
Some (g,[],List.map2 (fun x -> in_pat false (x,snd scopes)) argscs pats)
with Not_found -> None
and in_pat top scopes (loc, pt) = match pt with
- | CPatAlias (p, id) -> Loc.tag ~loc @@ RCPatAlias (in_pat top scopes p, id)
+ | CPatAlias (p, id) -> Loc.tag ?loc @@ RCPatAlias (in_pat top scopes p, id)
| CPatRecord l ->
let sorted_fields =
sort_fields ~complete:false loc l (fun _idx -> (loc, CPatAtom None)) in
begin match sorted_fields with
- | None -> Loc.tag ~loc @@ RCPatAtom None
+ | None -> Loc.tag ?loc @@ RCPatAtom None
| Some (n, head, pl) ->
let pl =
if !asymmetric_patterns then pl else
@@ -1272,7 +1274,7 @@ let drop_notations_pattern looked_for =
| CPatCstr (head, None, pl) ->
begin
match drop_syndef top scopes head pl with
- | Some (a,b,c) -> Loc.tag ~loc @@ RCPatCstr(a, b, c)
+ | Some (a,b,c) -> Loc.tag ?loc @@ RCPatCstr(a, b, c)
| None -> raise (InternalizationError (loc,NotAConstructor head))
end
| CPatCstr (r, Some expl_pl, pl) ->
@@ -1281,36 +1283,36 @@ let drop_notations_pattern looked_for =
raise (InternalizationError (loc,NotAConstructor r)) in
if expl_pl == [] then
(* Convention: (@r) deactivates all further implicit arguments and scopes *)
- Loc.tag ~loc @@ RCPatCstr (g, List.map (in_pat false scopes) pl, [])
+ Loc.tag ?loc @@ RCPatCstr (g, List.map (in_pat false scopes) pl, [])
else
(* Convention: (@r expl_pl) deactivates implicit arguments in expl_pl and in pl *)
(* but not scopes in expl_pl *)
let (argscs1,_) = find_remaining_scopes expl_pl pl g in
- Loc.tag ~loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
+ Loc.tag ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
| CPatNotation ("- _",([_loc,CPatPrim(Numeral p)],[]),[])
when Bigint.is_strictly_pos p ->
- fst (Notation.interp_prim_token_cases_pattern_expr ~loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes)
+ fst (Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes)
| CPatNotation ("( _ )",([a],[]),[]) ->
in_pat top scopes a
| CPatNotation (ntn, fullargs,extrargs) ->
let ntn,(args,argsl as fullargs) = contract_pat_notation ntn fullargs in
- let ((ids',c),df) = Notation.interp_notation ~loc ntn scopes in
+ let ((ids',c),df) = Notation.interp_notation ?loc ntn scopes in
let (ids',idsl',_) = split_by_type ids' in
- Dumpglob.dump_notation_location (patntn_loc loc fullargs ntn) ntn df;
+ Dumpglob.dump_notation_location (patntn_loc ?loc fullargs ntn) ntn df;
let substlist = make_subst idsl' argsl in
let subst = make_subst ids' args in
in_not top loc scopes (subst,substlist) extrargs c
| CPatDelimiters (key, e) ->
- in_pat top (None,find_delimiters_scope ~loc key::snd scopes) e
- | CPatPrim p -> fst (Notation.interp_prim_token_cases_pattern_expr ~loc (test_kind false) p scopes)
+ in_pat top (None,find_delimiters_scope ?loc key::snd scopes) e
+ | CPatPrim p -> fst (Notation.interp_prim_token_cases_pattern_expr ?loc (test_kind false) p scopes)
| CPatAtom Some id ->
begin
match drop_syndef top scopes id [] with
- | Some (a,b,c) -> Loc.tag ~loc @@ RCPatCstr (a, b, c)
- | None -> Loc.tag ~loc @@ RCPatAtom (Some (find_pattern_variable id))
+ | Some (a,b,c) -> Loc.tag ?loc @@ RCPatCstr (a, b, c)
+ | None -> Loc.tag ?loc @@ RCPatAtom (Some (find_pattern_variable id))
end
- | CPatAtom None -> Loc.tag ~loc @@ RCPatAtom None
- | CPatOr pl -> Loc.tag ~loc @@ RCPatOr (List.map (in_pat top scopes) pl)
+ | CPatAtom None -> Loc.tag ?loc @@ RCPatAtom None
+ | CPatOr pl -> Loc.tag ?loc @@ RCPatOr (List.map (in_pat top scopes) pl)
| CPatCast _ ->
assert false
and in_pat_sc scopes x = in_pat false (x,snd scopes)
@@ -1324,21 +1326,21 @@ let drop_notations_pattern looked_for =
let (a,(scopt,subscopes)) = Id.Map.find id subst in
in_pat top (scopt,subscopes@snd scopes) a
with Not_found ->
- if Id.equal id ldots_var then Loc.tag ~loc @@ RCPatAtom (Some id) else
+ if Id.equal id ldots_var then Loc.tag ?loc @@ RCPatAtom (Some id) else
anomaly (str "Unbound pattern notation variable: " ++ Id.print id)
end
| NRef g ->
ensure_kind top loc g;
let (_,argscs) = find_remaining_scopes [] args g in
- Loc.tag ~loc @@ RCPatCstr (g, [], List.map2 (in_pat_sc scopes) argscs args)
+ Loc.tag ?loc @@ RCPatCstr (g, [], List.map2 (in_pat_sc scopes) argscs args)
| NApp (NRef g,pl) ->
ensure_kind top loc g;
let (argscs1,argscs2) = find_remaining_scopes pl args g in
- Loc.tag ~loc @@ RCPatCstr (g,
+ Loc.tag ?loc @@ RCPatCstr (g,
List.map2 (fun x -> in_not false loc (x,snd scopes) fullsubst []) argscs1 pl @
List.map (in_pat false scopes) args, [])
| NList (x,y,iter,terminator,lassoc) ->
- if not (List.is_empty args) then user_err ~loc
+ if not (List.is_empty args) then user_err ?loc
(strbrk "Application of arguments to a recursive notation not supported in patterns.");
(try
(* All elements of the list are in scopes (scopt,subscopes) *)
@@ -1353,8 +1355,8 @@ let drop_notations_pattern looked_for =
anomaly (Pp.str "Inconsistent substitution of recursive notation"))
| NHole _ ->
let () = assert (List.is_empty args) in
- Loc.tag ~loc @@ RCPatAtom None
- | t -> error_invalid_pattern_notation ~loc ()
+ Loc.tag ?loc @@ RCPatAtom None
+ | t -> error_invalid_pattern_notation ?loc ()
in in_pat true
let rec intern_pat genv aliases pat =
@@ -1362,7 +1364,7 @@ let rec intern_pat genv aliases pat =
let idslpl2 = List.map (intern_pat genv empty_alias) pl2 in
let (ids',pll) = product_of_cases_patterns aliases.alias_ids (idslpl1@idslpl2) in
let pl' = List.map (fun (asubst,pl) ->
- (asubst, Loc.tag ~loc @@ PatCstr (c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in
+ (asubst, Loc.tag ?loc @@ PatCstr (c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in
ids',pl' in
match pat with
| loc, RCPatAlias (p, id) ->
@@ -1382,10 +1384,10 @@ let rec intern_pat genv aliases pat =
intern_cstr_with_all_args loc c with_letin idslpl1 (expl_pl@pl2)
| loc, RCPatAtom (Some id) ->
let aliases = merge_aliases aliases id in
- (aliases.alias_ids,[aliases.alias_map, Loc.tag ~loc @@ PatVar (alias_of aliases)])
+ (aliases.alias_ids,[aliases.alias_map, Loc.tag ?loc @@ PatVar (alias_of aliases)])
| loc, RCPatAtom (None) ->
let { alias_ids = ids; alias_map = asubst; } = aliases in
- (ids, [asubst, Loc.tag ~loc @@ PatVar (alias_of aliases)])
+ (ids, [asubst, Loc.tag ?loc @@ PatVar (alias_of aliases)])
| loc, RCPatOr pl ->
assert (not (List.is_empty pl));
let pl' = List.map (intern_pat genv aliases) pl in
@@ -1406,7 +1408,7 @@ let rec intern_pat genv aliases pat =
[pattern] rule. *)
let rec check_no_patcast (loc, pt) = match pt with
| CPatCast (_,_) ->
- CErrors.user_err ~loc ~hdr:"check_no_patcast"
+ CErrors.user_err ?loc ~hdr:"check_no_patcast"
(Pp.strbrk "Casts are not supported here.")
| CPatDelimiters(_,p)
| CPatAlias(p,_) -> check_no_patcast p
@@ -1440,11 +1442,11 @@ let intern_ind_pattern genv scopes pat =
let no_not =
try
drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) scopes pat
- with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type ~loc
+ with InternalizationError(loc,NotAConstructor _) -> error_bad_inductive_type ?loc
in
match no_not with
| loc, RCPatCstr (head, expl_pl, pl) ->
- let c = (function IndRef ind -> ind | _ -> error_bad_inductive_type ~loc) head in
+ let c = (function IndRef ind -> ind | _ -> error_bad_inductive_type ?loc) head in
let with_letin, pl2 = add_implicits_check_ind_length genv loc c
(List.length expl_pl) pl in
let idslpl1 = List.rev_map (intern_pat genv empty_alias) expl_pl in
@@ -1452,8 +1454,8 @@ let intern_ind_pattern genv scopes pat =
(with_letin,
match product_of_cases_patterns [] (List.rev_append idslpl1 idslpl2) with
| _,[_,pl] -> (c,chop_params_pattern loc c pl with_letin)
- | _ -> error_bad_inductive_type ~loc)
- | x -> error_bad_inductive_type ~loc:(raw_cases_pattern_expr_loc x)
+ | _ -> error_bad_inductive_type ?loc)
+ | x -> error_bad_inductive_type ?loc:(raw_cases_pattern_expr_loc x)
(**********************************************************************)
(* Utilities for application *)
@@ -1474,8 +1476,8 @@ let get_implicit_name n imps =
Some (Impargs.name_of_implicit (List.nth imps (n-1)))
let set_hole_implicit i b = function
- | (loc, GRef (r,_)) | (_, GApp ((loc, (GRef (r,_))),_)) -> Loc.tag ~loc (Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None)
- | (loc, GVar id) -> Loc.tag ~loc (Evar_kinds.ImplicitArg (VarRef id,i,b),Misctypes.IntroAnonymous,None)
+ | (loc, GRef (r,_)) | (_, GApp ((loc, (GRef (r,_))),_)) -> Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None)
+ | (loc, GVar id) -> Loc.tag ?loc (Evar_kinds.ImplicitArg (VarRef id,i,b),Misctypes.IntroAnonymous,None)
| _ -> anomaly (Pp.str "Only refs have implicits")
let exists_implicit_name id =
@@ -1492,10 +1494,10 @@ let extract_explicit_arg imps args =
let id = match pos with
| ExplByName id ->
if not (exists_implicit_name id imps) then
- user_err ~loc
+ user_err ?loc
(str "Wrong argument name: " ++ pr_id id ++ str ".");
if Id.Map.mem id eargs then
- user_err ~loc (str "Argument name " ++ pr_id id
+ user_err ?loc (str "Argument name " ++ pr_id id
++ str " occurs more than once.");
id
| ExplByPos (p,_id) ->
@@ -1505,11 +1507,11 @@ let extract_explicit_arg imps args =
if not (is_status_implicit imp) then failwith "imp";
name_of_implicit imp
with Failure _ (* "nth" | "imp" *) ->
- user_err ~loc
+ user_err ?loc
(str"Wrong argument position: " ++ int p ++ str ".")
in
if Id.Map.mem id eargs then
- user_err ~loc (str"Argument at position " ++ int p ++
+ user_err ?loc (str"Argument at position " ++ int p ++
str " is mentioned more than once.");
id in
(Id.Map.add id (loc, a) eargs, rargs)
@@ -1519,7 +1521,7 @@ let extract_explicit_arg imps args =
(* Main loop *)
let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
- let rec intern env = Loc.with_loc (fun ~loc -> function
+ let rec intern env = Loc.with_loc (fun ?loc -> function
| CRef (ref,us) ->
let (c,imp,subscopes,l),_ =
intern_applied_reference intern env (Environ.named_context globalenv)
@@ -1564,7 +1566,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
push_name_env ntnvars (impls_type_list ~args:fix_args tyi)
en (Loc.tag @@ Name name)) 0 env' lf in
(a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in
- Loc.tag ~loc @@
+ Loc.tag ?loc @@
GRec (GFix
(Array.map (fun (ro,_,_,_) -> ro) idl,n),
Array.of_list lf,
@@ -1591,7 +1593,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
push_name_env ntnvars (impls_type_list ~args:cofix_args tyi)
en (Loc.tag @@ Name name)) 0 env' lf in
(b,c,intern {env'' with tmp_scope = None} bd)) dl idl_tmp in
- Loc.tag ~loc @@
+ Loc.tag ?loc @@
GRec (GCoFix n,
Array.of_list lf,
Array.map (fun (bl,_,_) -> bl) idl,
@@ -1600,30 +1602,30 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
| CProdN ([],c2) ->
intern_type env c2
| CProdN ((nal,bk,ty)::bll,c2) ->
- iterate_prod loc env bk ty (Loc.tag ~loc @@ CProdN (bll, c2)) nal
+ iterate_prod ?loc env bk ty (Loc.tag ?loc @@ CProdN (bll, c2)) nal
| CLambdaN ([],c2) ->
intern env c2
| CLambdaN ((nal,bk,ty)::bll,c2) ->
- iterate_lam loc (reset_tmp_scope env) bk ty (Loc.tag ~loc @@ CLambdaN (bll, c2)) nal
+ iterate_lam loc (reset_tmp_scope env) bk ty (Loc.tag ?loc @@ CLambdaN (bll, c2)) nal
| CLetIn (na,c1,t,c2) ->
let inc1 = intern (reset_tmp_scope env) c1 in
let int = Option.map (intern_type env) t in
- Loc.tag ~loc @@
+ Loc.tag ?loc @@
GLetIn (snd na, inc1, int,
intern (push_name_env ntnvars (impls_term_list inc1) env na) c2)
| CNotation ("- _",([_, CPrim (Numeral p)],[],[]))
when Bigint.is_strictly_pos p ->
- intern env (Loc.tag ~loc @@ CPrim (Numeral (Bigint.neg p)))
+ intern env (Loc.tag ?loc @@ CPrim (Numeral (Bigint.neg p)))
| CNotation ("( _ )",([a],[],[])) -> intern env a
| CNotation (ntn,args) ->
intern_notation intern env ntnvars loc ntn args
| CGeneralization (b,a,c) ->
intern_generalization intern env ntnvars loc b a c
| CPrim p ->
- fst (Notation.interp_prim_token ~loc p (env.tmp_scope,env.scopes))
+ fst (Notation.interp_prim_token ?loc p (env.tmp_scope,env.scopes))
| CDelimiters (key, e) ->
intern {env with tmp_scope = None;
- scopes = find_delimiters_scope ~loc key :: env.scopes} e
+ scopes = find_delimiters_scope ?loc key :: env.scopes} e
| CAppExpl ((isproj,ref,us), args) ->
let (f,_,args_scopes,_),args =
let args = List.map (fun a -> (a,None)) args in
@@ -1631,7 +1633,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
lvar us args ref
in
(* Rem: GApp(_,f,[]) stands for @f *)
- Loc.tag ~loc @@
+ Loc.tag ?loc @@
GApp (f, intern_args env args_scopes (List.map fst args))
| CApp ((isproj,f), args) ->
@@ -1658,15 +1660,15 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
let fields =
sort_fields ~complete:true loc fs
- (fun _idx -> Loc.tag ~loc @@ CHole (Some (Evar_kinds.QuestionMark st),
+ (fun _idx -> Loc.tag ?loc @@ CHole (Some (Evar_kinds.QuestionMark st),
Misctypes.IntroAnonymous, None))
in
begin
match fields with
- | None -> user_err ~loc ~hdr:"intern" (str"No constructor inference.")
+ | None -> user_err ?loc ~hdr:"intern" (str"No constructor inference.")
| Some (n, constrname, args) ->
- let pars = List.make n (Loc.tag ~loc @@ CHole (None, Misctypes.IntroAnonymous, None)) in
- let app = Loc.tag ~loc @@ CAppExpl ((None, constrname,None), List.rev_append pars args) in
+ let pars = List.make n (Loc.tag ?loc @@ CHole (None, Misctypes.IntroAnonymous, None)) in
+ let app = Loc.tag ?loc @@ CAppExpl ((None, constrname,None), List.rev_append pars args) in
intern env app
end
| CCases (sty, rtnpo, tms, eqns) ->
@@ -1701,7 +1703,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
let main_sub_eqn = Loc.tag @@
([],thepats, (* "|p1,..,pn" *)
Option.cata (intern_type env')
- (Loc.tag ~loc @@ GHole(Evar_kinds.CasesType false,Misctypes.IntroAnonymous,None))
+ (Loc.tag ?loc @@ GHole(Evar_kinds.CasesType false,Misctypes.IntroAnonymous,None))
rtnpo) (* "=> P" if there were a return predicate P, and "=> _" otherwise *) in
let catch_all_sub_eqn =
if List.for_all (irrefutable globalenv) thepats then [] else
@@ -1710,7 +1712,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
Some (Loc.tag @@ GCases(Term.RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn))
in
let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
- Loc.tag ~loc @@
+ Loc.tag ?loc @@
GCases (sty, rtnpo, tms, List.flatten eqns')
| CLetTuple (nal, (na,po), b, c) ->
let env' = reset_tmp_scope env in
@@ -1720,7 +1722,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env')
(Loc.tag na') in
intern_type env'' u) po in
- Loc.tag ~loc @@
+ Loc.tag ?loc @@
GLetTuple (List.map snd nal, (na', p'), b',
intern (List.fold_left (push_name_env ntnvars (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c)
| CIf (c, (na,po), b1, b2) ->
@@ -1730,7 +1732,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env)
(Loc.tag na') in
intern_type env'' p) po in
- Loc.tag ~loc @@
+ Loc.tag ?loc @@
GIf (c', (na', p'), intern env b1, intern env b2)
| CHole (k, naming, solve) ->
let k = match k with
@@ -1756,28 +1758,28 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
let (_, glb) = Genintern.generic_intern ist gen in
Some glb
in
- Loc.tag ~loc @@
+ Loc.tag ?loc @@
GHole (k, naming, solve)
(* Parsing pattern variables *)
| CPatVar n when allow_patvar ->
- Loc.tag ~loc @@
+ Loc.tag ?loc @@
GPatVar (true,n)
| CEvar (n, []) when allow_patvar ->
- Loc.tag ~loc @@
+ Loc.tag ?loc @@
GPatVar (false,n)
(* end *)
(* Parsing existential variables *)
| CEvar (n, l) ->
- Loc.tag ~loc @@
+ Loc.tag ?loc @@
GEvar (n, List.map (on_snd (intern env)) l)
| CPatVar _ ->
raise (InternalizationError (loc,IllegalMetavariable))
(* end *)
| CSort s ->
- Loc.tag ~loc @@
+ Loc.tag ?loc @@
GSort s
| CCast (c1, c2) ->
- Loc.tag ~loc @@
+ Loc.tag ?loc @@
GCast (intern env c1, Miscops.map_cast_type (intern_type env) c2)
)
and intern_type env = intern (set_type_scope env)
@@ -1836,7 +1838,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
let rec canonize_args case_rel_ctxt arg_pats forbidden_names match_acc var_acc =
let add_name l = function
| _,Anonymous -> l
- | loc,(Name y as x) -> (y, Loc.tag ~loc @@ PatVar x) :: l in
+ | loc,(Name y as x) -> (y, Loc.tag ?loc @@ PatVar x) :: l in
match case_rel_ctxt,arg_pats with
(* LetIn in the rel_context *)
| LocalDef _ :: t, l when not with_letin ->
@@ -1860,13 +1862,13 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
[], None in
(tm',(snd na,typ)), extra_id, match_td
- and iterate_prod loc2 env bk ty body nal =
+ and iterate_prod ?loc env bk ty body nal =
let env, bl = intern_assumption intern ntnvars env nal bk ty in
- it_mkGProd loc2 bl (intern_type env body)
+ it_mkGProd ?loc bl (intern_type env body)
- and iterate_lam loc2 env bk ty body nal =
+ and iterate_lam loc env bk ty body nal =
let env, bl = intern_assumption intern ntnvars env nal bk ty in
- it_mkGLambda loc2 bl (intern env body)
+ it_mkGLambda ?loc bl (intern env body)
and intern_impargs c env l subscopes args =
let eargs, rargs = extract_explicit_arg l args in
@@ -1898,7 +1900,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
| (imp::impl', []) ->
if not (Id.Map.is_empty eargs) then
(let (id,(loc,_)) = Id.Map.choose eargs in
- user_err ~loc (str "Not enough non implicit \
+ user_err ?loc (str "Not enough non implicit \
arguments to accept the argument bound to " ++
pr_id id ++ str"."));
[]
@@ -1915,8 +1917,8 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
and smart_gapp f loc = function
| [] -> f
| l -> match f with
- | (loc', GApp (g, args)) -> Loc.tag ~loc:(Loc.merge loc' loc) @@ GApp (g, args@l)
- | _ -> Loc.tag ~loc:(Loc.merge (loc_of_glob_constr f) loc) @@ GApp (f, l)
+ | (loc', GApp (g, args)) -> Loc.tag ?loc:(Loc.merge_opt loc' loc) @@ GApp (g, args@l)
+ | _ -> Loc.tag ?loc:(Loc.merge_opt (loc_of_glob_constr f) loc) @@ GApp (f, l)
and intern_args env subscopes = function
| [] -> []
@@ -1929,7 +1931,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
intern env c
with
InternalizationError (loc,e) ->
- user_err ~loc ~hdr:"internalize"
+ user_err ?loc ~hdr:"internalize"
(explain_internalization_error e)
(**************************************************************************)
@@ -1969,7 +1971,7 @@ let intern_pattern globalenv patt =
intern_cases_pattern globalenv (None,[]) empty_alias patt
with
InternalizationError (loc,e) ->
- user_err ~loc ~hdr:"internalize" (explain_internalization_error e)
+ user_err ?loc ~hdr:"internalize" (explain_internalization_error e)
(*********************************************************************)
@@ -2055,12 +2057,12 @@ let interp_notation_constr ?(impls=empty_internalization_env) nenv a =
let interp_binder env sigma na t =
let t = intern_gen IsType env t in
- let t' = locate_if_hole ~loc:(loc_of_glob_constr t) na t in
+ let t' = locate_if_hole ?loc:(loc_of_glob_constr t) na t in
understand ~expected_type:IsType env sigma t'
let interp_binder_evars env evdref na t =
let t = intern_gen IsType env t in
- let t' = locate_if_hole ~loc:(loc_of_glob_constr t) na t in
+ let t' = locate_if_hole ?loc:(loc_of_glob_constr t) na t in
understand_tcc_evars env evdref ~expected_type:IsType t'
open Environ
@@ -2079,7 +2081,7 @@ let intern_context global_level env impl_env binders =
tmp_scope = None; scopes = []; impls = impl_env}, []) binders in
(lenv.impls, List.map glob_local_binder_of_extended bl)
with InternalizationError (loc,e) ->
- user_err ~loc ~hdr:"internalize" (explain_internalization_error e)
+ user_err ?loc ~hdr:"internalize" (explain_internalization_error e)
let interp_rawcontext_evars env evdref k bl =
let open EConstr in
@@ -2087,7 +2089,7 @@ let interp_rawcontext_evars env evdref k bl =
List.fold_left
(fun (env,params,n,impls) (na, k, b, t) ->
let t' =
- if Option.is_empty b then locate_if_hole ~loc:(loc_of_glob_constr t) na t
+ if Option.is_empty b then locate_if_hole ?loc:(loc_of_glob_constr t) na t
else t
in
let t = understand_tcc_evars env evdref ~expected_type:IsType t' in
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 9f549b0c0..10621f14d 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -139,30 +139,32 @@ let interval loc =
let loc1,loc2 = Loc.unloc loc in
loc1, loc2-1
-let dump_ref loc filepath modpath ident ty =
+let dump_ref ?loc filepath modpath ident ty =
match !glob_output with
| Feedback ->
- Feedback.feedback (Feedback.GlobRef (loc, filepath, modpath, ident, ty))
+ Option.iter (fun loc ->
+ Feedback.feedback (Feedback.GlobRef (loc, filepath, modpath, ident, ty))
+ ) loc
| NoGlob -> ()
- | _ when not (Loc.is_ghost loc) ->
+ | _ -> Option.iter (fun loc ->
let bl,el = interval loc in
dump_string (Printf.sprintf "R%d:%d %s %s %s %s\n"
bl el filepath modpath ident ty)
- | _ -> ()
+ ) loc
-let dump_reference loc modpath ident ty =
+let dump_reference ?loc modpath ident ty =
let filepath = Names.DirPath.to_string (Lib.library_dp ()) in
- dump_ref loc filepath modpath ident ty
+ dump_ref ?loc filepath modpath ident ty
-let dump_modref loc mp ty =
+let dump_modref ?loc mp ty =
let (dp, l) = Lib.split_modpath mp in
let filepath = Names.DirPath.to_string dp in
let modpath = Names.DirPath.to_string (Names.DirPath.make l) in
let ident = "<>" in
- dump_ref loc filepath modpath ident ty
+ dump_ref ?loc filepath modpath ident ty
-let dump_libref loc dp ty =
- dump_ref loc (Names.DirPath.to_string dp) "<>" "<>" ty
+let dump_libref ?loc dp ty =
+ dump_ref ?loc (Names.DirPath.to_string dp) "<>" "<>" ty
let cook_notation df sc =
(* We encode notations so that they are space-free and still human-readable *)
@@ -208,10 +210,10 @@ let dump_notation_location posl df (((path,secpath),_),sc) =
let secpath = Names.DirPath.to_string secpath in
let df = cook_notation df sc in
List.iter (fun l ->
- dump_ref (Loc.make_loc l) path secpath df "not")
+ dump_ref ~loc:(Loc.make_loc l) path secpath df "not")
posl
-let add_glob_gen loc sp lib_dp ty =
+let add_glob_gen ?loc sp lib_dp ty =
if dump () then
let mod_dp,id = Libnames.repr_path sp in
let mod_dp = remove_sections mod_dp in
@@ -219,50 +221,51 @@ let add_glob_gen loc sp lib_dp ty =
let filepath = Names.DirPath.to_string lib_dp in
let modpath = Names.DirPath.to_string mod_dp_trunc in
let ident = Names.Id.to_string id in
- dump_ref loc filepath modpath ident ty
+ dump_ref ?loc filepath modpath ident ty
-let add_glob loc ref =
- if dump () && not (Loc.is_ghost loc) then
+let add_glob ?loc ref =
+ if dump () then
let sp = Nametab.path_of_global ref in
let lib_dp = Lib.library_part ref in
let ty = type_of_global_ref ref in
- add_glob_gen loc sp lib_dp ty
+ add_glob_gen ?loc sp lib_dp ty
let mp_of_kn kn =
let mp,sec,l = Names.repr_kn kn in
Names.MPdot (mp,l)
-let add_glob_kn loc kn =
- if dump () && not (Loc.is_ghost loc) then
+let add_glob_kn ?loc kn =
+ if dump () then
let sp = Nametab.path_of_syndef kn in
let lib_dp = Lib.dp_of_mp (mp_of_kn kn) in
- add_glob_gen loc sp lib_dp "syndef"
+ add_glob_gen ?loc sp lib_dp "syndef"
-let dump_binding loc id = ()
+let dump_binding ?loc id = ()
-let dump_def ty loc secpath id =
+let dump_def ?loc ty secpath id = Option.iter (fun loc ->
if !glob_output = Feedback then
Feedback.feedback (Feedback.GlobDef (loc, id, secpath, ty))
else
let bl,el = interval loc in
dump_string (Printf.sprintf "%s %d:%d %s %s\n" ty bl el secpath id)
+ ) loc
let dump_definition (loc, id) sec s =
- dump_def s loc (Names.DirPath.to_string (Lib.current_dirpath sec)) (Names.Id.to_string id)
+ dump_def ?loc s (Names.DirPath.to_string (Lib.current_dirpath sec)) (Names.Id.to_string id)
let dump_constraint (((loc, n),_), _, _) sec ty =
match n with
| Names.Name id -> dump_definition (loc, id) sec ty
| Names.Anonymous -> ()
-let dump_moddef loc mp ty =
+let dump_moddef ?loc mp ty =
let (dp, l) = Lib.split_modpath mp in
let mp = Names.DirPath.to_string (Names.DirPath.make l) in
- dump_def ty loc "<>" mp
+ dump_def ?loc ty "<>" mp
-let dump_notation (loc,(df,_)) sc sec =
+let dump_notation (loc,(df,_)) sc sec = Option.iter (fun loc ->
(* We dump the location of the opening '"' *)
let i = fst (Loc.unloc loc) in
let location = (Loc.make_loc (i, i+1)) in
- dump_def "not" location (Names.DirPath.to_string (Lib.current_dirpath sec)) (cook_notation df sc)
-
+ dump_def ~loc:location "not" (Names.DirPath.to_string (Lib.current_dirpath sec)) (cook_notation df sc)
+ ) loc
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index e84a64052..f42055af7 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -22,19 +22,19 @@ val feedback_glob : unit -> unit
val pause : unit -> unit
val continue : unit -> unit
-val add_glob : Loc.t -> Globnames.global_reference -> unit
-val add_glob_kn : Loc.t -> Names.kernel_name -> unit
-
-val dump_definition : Loc.t * Names.Id.t -> bool -> string -> unit
-val dump_moddef : Loc.t -> Names.module_path -> string -> unit
-val dump_modref : Loc.t -> Names.module_path -> string -> unit
-val dump_reference : Loc.t -> string -> string -> string -> unit
-val dump_libref : Loc.t -> Names.DirPath.t -> string -> unit
+val add_glob : ?loc:Loc.t -> Globnames.global_reference -> unit
+val add_glob_kn : ?loc:Loc.t -> Names.kernel_name -> unit
+
+val dump_definition : Names.Id.t Loc.located -> bool -> string -> unit
+val dump_moddef : ?loc:Loc.t -> Names.module_path -> string -> unit
+val dump_modref : ?loc:Loc.t -> Names.module_path -> string -> unit
+val dump_reference : ?loc:Loc.t -> string -> string -> string -> unit
+val dump_libref : ?loc:Loc.t -> Names.DirPath.t -> string -> unit
val dump_notation_location : (int * int) list -> Constrexpr.notation ->
(Notation.notation_location * Notation_term.scope_name option) -> unit
-val dump_binding : Loc.t -> Names.Id.Set.elt -> unit
+val dump_binding : ?loc:Loc.t -> Names.Id.Set.elt -> unit
val dump_notation :
- Loc.t * (Constrexpr.notation * Notation.notation_location) ->
+ (Constrexpr.notation * Notation.notation_location) Loc.located ->
Notation_term.scope_name option -> bool -> unit
val dump_constraint :
Constrexpr.typeclass_constraint -> bool -> string -> unit
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index fa7712bdc..dd04e2030 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -29,11 +29,11 @@ let generalizable_table = Summary.ref Id.Pred.empty ~name:"generalizable-ident"
let declare_generalizable_ident table (loc,id) =
if not (Id.equal id (root_of_id id)) then
- user_err ~loc ~hdr:"declare_generalizable_ident"
+ user_err ?loc ~hdr:"declare_generalizable_ident"
((pr_id id ++ str
" is not declarable as generalizable identifier: it must have no trailing digits, quote, or _"));
if Id.Pred.mem id table then
- user_err ~loc ~hdr:"declare_generalizable_ident"
+ user_err ?loc ~hdr:"declare_generalizable_ident"
((pr_id id++str" is already declared as a generalizable identifier"))
else Id.Pred.add id table
@@ -80,7 +80,7 @@ let is_freevar ids env x =
(* Auxiliary functions for the inference of implicitly quantified variables. *)
let ungeneralizable loc id =
- user_err ~loc ~hdr:"Generalization"
+ user_err ?loc ~hdr:"Generalization"
(str "Unbound and ungeneralizable variable " ++ pr_id id)
let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l =
@@ -128,8 +128,8 @@ let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.emp
let rec vars bound vs (loc, t) = match t with
| GVar id ->
if is_freevar bound (Global.env ()) id then
- if Id.List.mem_assoc id vs then vs
- else (id, loc) :: vs
+ if Id.List.mem_assoc_sym id vs then vs
+ else (Loc.tag ?loc id) :: vs
else vs
| GApp (f,args) -> List.fold_left (vars bound) vs (f::args)
@@ -189,7 +189,7 @@ let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.emp
vars_option bound' vs tyopt
in fun rt ->
let vars = List.rev (vars bound [] rt) in
- List.iter (fun (id, loc) ->
+ List.iter (fun (loc, id) ->
if not (Id.Set.mem id allowed || find_generalizable_ident id) then
ungeneralizable loc id) vars;
vars
@@ -212,7 +212,7 @@ let combine_params avoid fn applied needed =
| Anonymous -> false
in
if not (List.exists is_id needed) then
- user_err ~loc (str "Wrong argument name: " ++ Nameops.pr_id id);
+ user_err ?loc (str "Wrong argument name: " ++ Nameops.pr_id id);
true
| _ -> false) applied
in
@@ -246,7 +246,7 @@ let combine_params avoid fn applied needed =
aux (t' :: ids) avoid' app need
| (x,_) :: _, [] ->
- user_err ~loc:(Constrexpr_ops.constr_loc x) (str "Typeclass does not expect more arguments")
+ user_err ?loc:(Constrexpr_ops.constr_loc x) (str "Typeclass does not expect more arguments")
in aux [] avoid applied needed
let combine_params_freevar =
@@ -256,21 +256,21 @@ let combine_params_freevar =
let destClassApp (loc, cl) =
match cl with
- | CApp ((None, (_loc, CRef (ref, inst))), l) -> loc, ref, List.map fst l, inst
- | CAppExpl ((None, ref, inst), l) -> loc, ref, l, inst
- | CRef (ref, inst) -> loc_of_reference ref, ref, [], inst
+ | CApp ((None, (_loc, CRef (ref, inst))), l) -> Loc.tag ?loc (ref, List.map fst l, inst)
+ | CAppExpl ((None, ref, inst), l) -> Loc.tag ?loc (ref, l, inst)
+ | CRef (ref, inst) -> Loc.tag ?loc:(loc_of_reference ref) (ref, [], inst)
| _ -> raise Not_found
let destClassAppExpl (loc, cl) =
match cl with
- | CApp ((None, (_loc, CRef (ref, inst))), l) -> loc, ref, l, inst
- | CRef (ref, inst) -> loc_of_reference ref, ref, [], inst
+ | CApp ((None, (_loc, CRef (ref, inst))), l) -> Loc.tag ?loc (ref, l, inst)
+ | CRef (ref, inst) -> Loc.tag ?loc:(loc_of_reference ref) (ref, [], inst)
| _ -> raise Not_found
let implicit_application env ?(allow_partial=true) f ty =
let is_class =
try
- let (_, r, _, _ as clapp) = destClassAppExpl ty in
+ let (_, (r, _, _) as clapp) = destClassAppExpl ty in
let (loc, qid) = qualid_of_reference r in
let gr = Nametab.locate qid in
if Typeclasses.is_class gr then Some (clapp, gr) else None
@@ -278,7 +278,7 @@ let implicit_application env ?(allow_partial=true) f ty =
in
match is_class with
| None -> ty, env
- | Some ((loc, id, par, inst), gr) ->
+ | Some ((loc, (id, par, inst)), gr) ->
let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in
let c, avoid =
let c = class_info gr in
@@ -296,7 +296,7 @@ let implicit_application env ?(allow_partial=true) f ty =
end;
let pars = List.rev (List.combine ci rd) in
let args, avoid = combine_params avoid f par pars in
- Loc.tag ~loc @@ CAppExpl ((None, id, inst), args), avoid
+ Loc.tag ?loc @@ CAppExpl ((None, id, inst), args), avoid
in c, avoid
let implicits_of_glob_constr ?(with_products=true) l =
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 71009ec3c..945bed2aa 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -16,8 +16,8 @@ open Globnames
val declare_generalizable : Vernacexpr.locality_flag -> (Id.t located) list option -> unit
val ids_of_list : Id.t list -> Id.Set.t
-val destClassApp : constr_expr -> Loc.t * reference * constr_expr list * instance_expr option
-val destClassAppExpl : constr_expr -> Loc.t * reference * (constr_expr * explicitation located option) list * instance_expr option
+val destClassApp : constr_expr -> (reference * constr_expr list * instance_expr option) located
+val destClassAppExpl : constr_expr -> (reference * (constr_expr * explicitation located option) list * instance_expr option) located
(** Fragile, should be used only for construction a set of identifiers to avoid *)
@@ -31,7 +31,7 @@ val free_vars_of_binders :
order with the location of their first occurrence *)
val generalizable_vars_of_glob_constr : ?bound:Id.Set.t -> ?allowed:Id.Set.t ->
- glob_constr -> (Id.t * Loc.t) list
+ glob_constr -> Id.t located list
val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 166711659..45e6cd06c 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -26,16 +26,16 @@ let error_not_a_module_loc kind loc qid =
| ModType -> Modops.ModuleTypingError (Modops.NotAModuleType s)
| ModAny -> ModuleInternalizationError (NotAModuleNorModtype s)
in
- Loc.raise ~loc e
+ Loc.raise ?loc e
let error_application_to_not_path loc me =
- Loc.raise ~loc (Modops.ModuleTypingError (Modops.ApplicationToNotPath me))
+ Loc.raise ?loc (Modops.ModuleTypingError (Modops.ApplicationToNotPath me))
let error_incorrect_with_in_module loc =
- Loc.raise ~loc (ModuleInternalizationError IncorrectWithInModule)
+ Loc.raise ?loc (ModuleInternalizationError IncorrectWithInModule)
let error_application_to_module_type loc =
- Loc.raise ~loc (ModuleInternalizationError IncorrectModuleApplication)
+ Loc.raise ?loc (ModuleInternalizationError IncorrectModuleApplication)
(** Searching for a module name in the Nametab.
@@ -47,12 +47,12 @@ let lookup_module_or_modtype kind (loc,qid) =
try
if kind == ModType then raise Not_found;
let mp = Nametab.locate_module qid in
- Dumpglob.dump_modref loc mp "modtype"; (mp,Module)
+ Dumpglob.dump_modref ?loc mp "modtype"; (mp,Module)
with Not_found ->
try
if kind == Module then raise Not_found;
let mp = Nametab.locate_modtype qid in
- Dumpglob.dump_modref loc mp "mod"; (mp,ModType)
+ Dumpglob.dump_modref ?loc mp "mod"; (mp,ModType)
with Not_found -> error_not_a_module_loc kind loc qid
let lookup_module lqid = fst (lookup_module_or_modtype Module lqid)
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 32c564156..328fdd519 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -227,8 +227,8 @@ let split_at_recursive_part c =
| None ->
let () = sub := Some c in
begin match l with
- | [] -> Loc.tag ~loc @@ GVar ldots_var
- | _ :: _ -> Loc.tag ~loc:loc0 @@ GApp (Loc.tag ~loc @@ GVar ldots_var, l)
+ | [] -> Loc.tag ?loc @@ GVar ldots_var
+ | _ :: _ -> Loc.tag ?loc:loc0 @@ GApp (Loc.tag ?loc @@ GVar ldots_var, l)
end
| Some _ ->
(* Not narrowed enough to find only one recursive part *)
@@ -243,10 +243,13 @@ let split_at_recursive_part c =
| GVar v when Id.equal v ldots_var -> (* Not enough context *) raise Not_found
| _ -> outer_iterator, c
-let subtract_loc loc1 loc2 = Loc.make_loc (fst (Loc.unloc loc1),fst (Loc.unloc loc2)-1)
+let subtract_loc loc1 loc2 =
+ let l1 = fst (Option.cata Loc.unloc (0,0) loc1) in
+ let l2 = fst (Option.cata Loc.unloc (0,0) loc2) in
+ Some (Loc.make_loc (l1,l2-1))
let check_is_hole id = function _, GHole _ -> () | t ->
- user_err ~loc:(loc_of_glob_constr t)
+ user_err ?loc:(loc_of_glob_constr t)
(strbrk "In recursive notation with binders, " ++ pr_id id ++
strbrk " is expected to come without type.")
@@ -298,7 +301,7 @@ let compare_recursive_parts found f f' (iterator,subc) =
let loc1 = loc_of_glob_constr iterator in
let loc2 = loc_of_glob_constr (Option.get !terminator) in
(* Here, we would need a loc made of several parts ... *)
- user_err ~loc:(subtract_loc loc1 loc2)
+ user_err ?loc:(subtract_loc loc1 loc2)
(str "Both ends of the recursive pattern are the same.")
| Some (x,y,RecursiveTerms lassoc) ->
let newfound,x,y,lassoc =
@@ -342,7 +345,7 @@ let notation_constr_and_vars_of_glob_constr a =
| GApp ((loc, GVar f),[c]) when Id.equal f ldots_var ->
(* Fall on the second part of the recursive pattern w/o having
found the first part *)
- user_err ~loc
+ user_err ?loc
(str "Cannot find where the recursive pattern starts.")
| _c ->
aux' c
@@ -459,7 +462,7 @@ let rec subst_pat subst (loc, pat) =
| PatCstr (((kn,i),j),cpl,n) ->
let kn' = subst_mind subst kn
and cpl' = List.smartmap (subst_pat subst) cpl in
- Loc.tag ~loc @@
+ Loc.tag ?loc @@
if kn' == kn && cpl' == cpl then pat else
PatCstr (((kn',i),j),cpl',n)
@@ -749,11 +752,11 @@ let rec map_cases_pattern_name_left f = Loc.map (function
)
let rec fold_cases_pattern_eq f x p p' = match p, p' with
- | (loc, PatVar na), (_, PatVar na') -> let x,na = f x na na' in x, Loc.tag ~loc @@ PatVar na
+ | (loc, PatVar na), (_, PatVar na') -> let x,na = f x na na' in x, Loc.tag ?loc @@ PatVar na
| (loc, PatCstr (c,l,na)), (_, PatCstr (c',l',na')) when eq_constructor c c' ->
let x,l = fold_cases_pattern_list_eq f x l l' in
let x,na = f x na na' in
- x, Loc.tag ~loc @@ PatCstr (c,l,na)
+ x, Loc.tag ?loc @@ PatCstr (c,l,na)
| _ -> failwith "Not equal"
and fold_cases_pattern_list_eq f x pl pl' = match pl, pl' with
@@ -799,13 +802,13 @@ let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma)
match b, b' with
| GLocalAssum (na,bk,t), GLocalAssum (na',bk',t') ->
let alp, na = unify_name alp na na' in
- alp, Loc.tag ~loc @@ GLocalAssum (na, unify_binding_kind bk bk', unify_term alp t t')
+ alp, Loc.tag ?loc @@ GLocalAssum (na, unify_binding_kind bk bk', unify_term alp t t')
| GLocalDef (na,bk,c,t), GLocalDef (na',bk',c',t') ->
let alp, na = unify_name alp na na' in
- alp, Loc.tag ~loc @@ GLocalDef (na, unify_binding_kind bk bk', unify_term alp c c', unify_opt_term alp t t')
+ alp, Loc.tag ?loc @@ GLocalDef (na, unify_binding_kind bk bk', unify_term alp c c', unify_opt_term alp t t')
| GLocalPattern ((p,ids),id,bk,t), GLocalPattern ((p',_),_,bk',t') ->
let alp, p = unify_pat alp p p' in
- alp, Loc.tag ~loc @@ GLocalPattern ((p,ids), id, unify_binding_kind bk bk', unify_term alp t t')
+ alp, Loc.tag ?loc @@ GLocalPattern ((p,ids), id, unify_binding_kind bk bk', unify_term alp t t')
| _ -> raise No_match in
let rec unify alp bl bl' =
match bl, bl' with
@@ -832,7 +835,7 @@ let bind_bindinglist_as_term_env alp (terms,onlybinders,termlists,binderlists) v
let unify_pat p p' =
if cases_pattern_eq (map_cases_pattern_name_left (name_app (rename_var (snd alp))) p) p' then p'
else raise No_match in
- let unify_term_binder c (loc, b') = Loc.tag ~loc @@
+ let unify_term_binder c (loc, b') = Loc.tag ?loc @@
match c, b' with
| (_, GVar id), GLocalAssum (na', bk', t') ->
GLocalAssum (unify_id id na', bk', t')
@@ -895,21 +898,21 @@ let rec match_cases_pattern_binders metas acc (_, pat1) (_, pat2) =
let glue_letin_with_decls = true
-let rec match_iterated_binders islambda decls bi = Loc.with_loc (fun ~loc -> function
+let rec match_iterated_binders islambda decls bi = Loc.with_loc (fun ?loc -> function
| GLambda (Name p,bk,t,(_, GCases (LetPatternStyle,None,[((_, GVar e),_)],[(_,(ids,[cp],b))])))
when islambda && Id.equal p e ->
- match_iterated_binders islambda ((Loc.tag ~loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b
+ match_iterated_binders islambda ((Loc.tag ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b
| GLambda (na,bk,t,b) when islambda ->
- match_iterated_binders islambda ((Loc.tag ~loc @@ GLocalAssum(na,bk,t))::decls) b
+ match_iterated_binders islambda ((Loc.tag ?loc @@ GLocalAssum(na,bk,t))::decls) b
| GProd (Name p,bk,t,(_, GCases (LetPatternStyle,None,[((_, GVar e),_)],[(_,(ids,[cp],b))])))
when not islambda && Id.equal p e ->
- match_iterated_binders islambda ((Loc.tag ~loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b
+ match_iterated_binders islambda ((Loc.tag ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b
| GProd ((Name _ as na),bk,t,b) when not islambda ->
- match_iterated_binders islambda ((Loc.tag ~loc @@ GLocalAssum(na,bk,t))::decls) b
+ match_iterated_binders islambda ((Loc.tag ?loc @@ GLocalAssum(na,bk,t))::decls) b
| GLetIn (na,c,t,b) when glue_letin_with_decls ->
match_iterated_binders islambda
- ((Loc.tag ~loc @@ GLocalDef (na,Explicit (*?*), c,t))::decls) b
- | b -> (decls, Loc.tag ~loc b)
+ ((Loc.tag ?loc @@ GLocalDef (na,Explicit (*?*), c,t))::decls) b
+ | b -> (decls, Loc.tag ?loc b)
) bi
let remove_sigma x (terms,onlybinders,termlists,binderlists) =
@@ -989,13 +992,13 @@ let rec match_ inner u alp metas sigma a1 a2 =
(* "λ p, let 'cp = p in t" -> "λ 'cp, t" *)
| GLambda (Name p,bk,t1,(_, GCases (LetPatternStyle,None,[((_, GVar e),_)],[(_,(ids,[cp],b1))]))),
NBinderList (x,_,NLambda (Name _id2,_,b2),termin) when Id.equal p e ->
- let (decls,b) = match_iterated_binders true [Loc.tag ~loc @@ GLocalPattern((cp,ids),p,bk,t1)] b1 in
+ let (decls,b) = match_iterated_binders true [Loc.tag ?loc @@ GLocalPattern((cp,ids),p,bk,t1)] b1 in
let alp,sigma = bind_bindinglist_env alp sigma x decls in
match_in u alp metas sigma b termin
(* Matching recursive notations for binders: ad hoc cases supporting let-in *)
| GLambda (na1,bk,t1,b1), NBinderList (x,_,NLambda (Name _id2,_,b2),termin)->
- let (decls,b) = match_iterated_binders true [Loc.tag ~loc @@ GLocalAssum (na1,bk,t1)] b1 in
+ let (decls,b) = match_iterated_binders true [Loc.tag ?loc @@ GLocalAssum (na1,bk,t1)] b1 in
(* TODO: address the possibility that termin is a Lambda itself *)
let alp,sigma = bind_bindinglist_env alp sigma x decls in
match_in u alp metas sigma b termin
@@ -1003,13 +1006,13 @@ let rec match_ inner u alp metas sigma a1 a2 =
(* "∀ p, let 'cp = p in t" -> "∀ 'cp, t" *)
| GProd (Name p,bk,t1,(_, GCases (LetPatternStyle,None,[((_, GVar e),_)],[(_,(ids,[cp],b1))]))),
NBinderList (x,_,NProd (Name _id2,_,b2),(NVar v as termin)) when Id.equal p e ->
- let (decls,b) = match_iterated_binders true [Loc.tag ~loc @@ GLocalPattern ((cp,ids),p,bk,t1)] b1 in
+ let (decls,b) = match_iterated_binders true [Loc.tag ?loc @@ GLocalPattern ((cp,ids),p,bk,t1)] b1 in
let alp,sigma = bind_bindinglist_env alp sigma x decls in
match_in u alp metas sigma b termin
| GProd (na1,bk,t1,b1), NBinderList (x,_,NProd (Name _id2,_,b2),termin)
when na1 != Anonymous ->
- let (decls,b) = match_iterated_binders false [Loc.tag ~loc @@ GLocalAssum (na1,bk,t1)] b1 in
+ let (decls,b) = match_iterated_binders false [Loc.tag ?loc @@ GLocalAssum (na1,bk,t1)] b1 in
(* TODO: address the possibility that termin is a Prod itself *)
let alp,sigma = bind_bindinglist_env alp sigma x decls in
match_in u alp metas sigma b termin
@@ -1021,15 +1024,15 @@ let rec match_ inner u alp metas sigma a1 a2 =
| GLambda (Name p,bk,t,(_, GCases (LetPatternStyle,None,[((_, GVar e),_)],[(_,(ids,[cp],b1))]))),
NLambda (Name id,_,b2)
when is_bindinglist_meta id metas ->
- let alp,sigma = bind_bindinglist_env alp sigma id [Loc.tag ~loc @@ GLocalPattern ((cp,ids),p,bk,t)] in
+ let alp,sigma = bind_bindinglist_env alp sigma id [Loc.tag ?loc @@ GLocalPattern ((cp,ids),p,bk,t)] in
match_in u alp metas sigma b1 b2
| GLambda (na,bk,t,b1), NLambda (Name id,_,b2)
when is_bindinglist_meta id metas ->
- let alp,sigma = bind_bindinglist_env alp sigma id [Loc.tag ~loc @@ GLocalAssum (na,bk,t)] in
+ let alp,sigma = bind_bindinglist_env alp sigma id [Loc.tag ?loc @@ GLocalAssum (na,bk,t)] in
match_in u alp metas sigma b1 b2
| GProd (na,bk,t,b1), NProd (Name id,_,b2)
when is_bindinglist_meta id metas && na != Anonymous ->
- let alp,sigma = bind_bindinglist_env alp sigma id [Loc.tag ~loc @@ GLocalAssum (na,bk,t)] in
+ let alp,sigma = bind_bindinglist_env alp sigma id [Loc.tag ?loc @@ GLocalAssum (na,bk,t)] in
match_in u alp metas sigma b1 b2
(* Matching compositionally *)
@@ -1041,7 +1044,7 @@ let rec match_ inner u alp metas sigma a1 a2 =
if n1 < n2 then
let l21,l22 = List.chop (n2-n1) l2 in f1,l1, NApp (f2,l21), l22
else if n1 > n2 then
- let l11,l12 = List.chop (n1-n2) l1 in Loc.tag ~loc @@ GApp (f1,l11),l12, f2,l2
+ let l11,l12 = List.chop (n1-n2) l1 in Loc.tag ?loc @@ GApp (f1,l11),l12, f2,l2
else f1,l1, f2, l2 in
let may_use_eta = does_not_come_from_already_eta_expanded_var f1 in
List.fold_left2 (match_ may_use_eta u alp metas)
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 1565ba4a9..20fdd6caa 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -86,12 +86,12 @@ let in_reserved : Id.t * notation_constr -> obj =
let declare_reserved_type_binding (loc,id) t =
if not (Id.equal id (root_of_id id)) then
- user_err ~loc ~hdr:"declare_reserved_type"
+ user_err ?loc ~hdr:"declare_reserved_type"
((pr_id id ++ str
" is not reservable: it must have no trailing digits, quote, or _"));
begin try
let _ = Id.Map.find id !reserve_table in
- user_err ~loc ~hdr:"declare_reserved_type"
+ user_err ?loc ~hdr:"declare_reserved_type"
((pr_id id++str" is already bound to a type"))
with Not_found -> () end;
add_anonymous_leaf (in_reserved (id,t))
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index fd9599ec0..a9d94669a 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -46,7 +46,7 @@ let locate_global_with_alias ?(head=false) (loc,qid) =
if head then global_of_extended_global_head ref
else global_of_extended_global ref
with Not_found ->
- user_err ~loc (pr_qualid qid ++
+ user_err ?loc (pr_qualid qid ++
str " is bound to a notation that does not denote a reference.")
let global_inductive_with_alias r =
@@ -54,27 +54,27 @@ let global_inductive_with_alias r =
try match locate_global_with_alias lqid with
| IndRef ind -> ind
| ref ->
- user_err ~loc:(loc_of_reference r) ~hdr:"global_inductive"
+ user_err ?loc:(loc_of_reference r) ~hdr:"global_inductive"
(pr_reference r ++ spc () ++ str "is not an inductive type.")
- with Not_found -> Nametab.error_global_not_found ~loc qid
+ with Not_found -> Nametab.error_global_not_found ?loc qid
let global_with_alias ?head r =
let (loc,qid as lqid) = qualid_of_reference r in
try locate_global_with_alias ?head lqid
- with Not_found -> Nametab.error_global_not_found ~loc qid
+ with Not_found -> Nametab.error_global_not_found ?loc qid
let smart_global ?head = function
| AN r ->
global_with_alias ?head r
| ByNotation (loc,(ntn,sc)) ->
- Notation.interp_notation_as_global_reference ~loc (fun _ -> true) ntn sc
+ Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc
let smart_global_inductive = function
| AN r ->
global_inductive_with_alias r
| ByNotation (loc,(ntn,sc)) ->
destIndRef
- (Notation.interp_notation_as_global_reference ~loc isIndRef ntn sc)
+ (Notation.interp_notation_as_global_reference ?loc isIndRef ntn sc)
let loc_of_smart_reference = function
| AN r -> loc_of_reference r
diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli
index 0749ca576..acae1a391 100644
--- a/interp/smartlocate.mli
+++ b/interp/smartlocate.mli
@@ -38,4 +38,4 @@ val smart_global : ?head:bool -> reference or_by_notation -> global_reference
val smart_global_inductive : reference or_by_notation -> inductive
(** Return the loc of a smart reference *)
-val loc_of_smart_reference : reference or_by_notation -> Loc.t
+val loc_of_smart_reference : reference or_by_notation -> Loc.t option
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index 113fe40ba..44a176d94 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -22,7 +22,7 @@ open Tactypes
open Genarg
(** FIXME: nothing to do there. *)
-val loc_of_or_by_notation : ('a -> Loc.t) -> 'a or_by_notation -> Loc.t
+val loc_of_or_by_notation : ('a -> Loc.t option) -> 'a or_by_notation -> Loc.t option
val wit_unit : unit uniform_genarg_type
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 2ffeb1f83..a74e64172 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -59,7 +59,7 @@ let rec cases_pattern_fold_names f a pt = match snd pt with
| CPatAtom (Some (Ident (_,id))) when not (is_constructor id) -> f id a
| CPatPrim _ | CPatAtom _ -> a
| CPatCast ((loc,_),_) ->
- CErrors.user_err ~loc ~hdr:"cases_pattern_fold_names"
+ CErrors.user_err ?loc ~hdr:"cases_pattern_fold_names"
(Pp.strbrk "Casts are not supported here.")
let ids_of_pattern =
@@ -103,7 +103,7 @@ let rec fold_local_binders g f n acc b = function
| [] ->
f n acc b
-let fold_constr_expr_with_binders g f n acc = Loc.with_loc (fun ~loc -> function
+let fold_constr_expr_with_binders g f n acc = Loc.with_loc (fun ?loc -> function
| CAppExpl ((_,_,_),l) -> List.fold_left (f n) acc l
| CApp ((_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l)
| CProdN (l,b) | CLambdaN (l,b) -> fold_constr_expr_binders g f n acc b l
@@ -181,9 +181,9 @@ let split_at_annot bl na =
end
| CLocalDef _ as x :: rest -> aux (x :: acc) rest
| CLocalPattern (loc,_) :: rest ->
- Loc.raise ~loc (Stream.Error "pattern with quote not allowed after fix")
+ Loc.raise ?loc (Stream.Error "pattern with quote not allowed after fix")
| [] ->
- user_err ~loc
+ user_err ?loc
(str "No parameter named " ++ Nameops.pr_id id ++ str".")
in aux [] bl
@@ -271,19 +271,20 @@ let rec replace_vars_constr_expr l = function
(* Returns the ranges of locs of the notation that are not occupied by args *)
(* and which are then occupied by proper symbols of the notation (or spaces) *)
-let locs_of_notation loc locs ntn =
- let (bl, el) = Loc.unloc loc in
- let locs = List.map Loc.unloc locs in
+let locs_of_notation ?loc locs ntn =
+ let unloc loc = Option.cata Loc.unloc (0,0) loc in
+ let (bl, el) = unloc loc in
+ let locs = List.map unloc locs in
let rec aux pos = function
| [] -> if Int.equal pos el then [] else [(pos,el)]
| (ba,ea)::l -> if Int.equal pos ba then aux ea l else (pos,ba)::aux ea l
in aux bl (List.sort (fun l1 l2 -> fst l1 - fst l2) locs)
-let ntn_loc loc (args,argslist,binderslist) =
- locs_of_notation loc
+let ntn_loc ?loc (args,argslist,binderslist) =
+ locs_of_notation ?loc
(List.map constr_loc (args@List.flatten argslist)@
- List.map_filter local_binders_loc binderslist)
+ List.map local_binders_loc binderslist)
-let patntn_loc loc (args,argslist) =
- locs_of_notation loc
+let patntn_loc ?loc (args,argslist) =
+ locs_of_notation ?loc
(List.map cases_pattern_expr_loc (args@List.flatten argslist))
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index b6ac40041..fabb1cb93 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -40,9 +40,9 @@ val map_constr_expr_with_binders :
'a -> constr_expr -> constr_expr
val ntn_loc :
- Loc.t -> constr_notation_substitution -> string -> (int * int) list
+ ?loc:Loc.t -> constr_notation_substitution -> string -> (int * int) list
val patntn_loc :
- Loc.t -> cases_pattern_notation_substitution -> string -> (int * int) list
+ ?loc:Loc.t -> cases_pattern_notation_substitution -> string -> (int * int) list
(** For cases pattern parsing errors *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 14:33:35 +0000