aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrexpr_ops.ml194
-rw-r--r--interp/constrexpr_ops.mli10
-rw-r--r--interp/constrextern.ml359
-rw-r--r--interp/constrextern.mli6
-rw-r--r--interp/constrintern.ml662
-rw-r--r--interp/dumpglob.ml57
-rw-r--r--interp/dumpglob.mli20
-rw-r--r--interp/implicit_quantifiers.ml62
-rw-r--r--interp/implicit_quantifiers.mli6
-rw-r--r--interp/modintern.ml25
-rw-r--r--interp/notation.ml88
-rw-r--r--interp/notation.mli13
-rw-r--r--interp/notation_ops.ml422
-rw-r--r--interp/notation_ops.mli4
-rw-r--r--interp/reserve.ml4
-rw-r--r--interp/smartlocate.ml18
-rw-r--r--interp/smartlocate.mli2
-rw-r--r--interp/stdarg.ml2
-rw-r--r--interp/stdarg.mli2
-rw-r--r--interp/topconstr.ml171
-rw-r--r--interp/topconstr.mli4
21 files changed, 1078 insertions, 1053 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 542f9feaf..79e0e6164 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -60,30 +60,30 @@ let explicitation_eq ex1 ex2 = match ex1, ex2 with
let eq_located f (_, x) (_, y) = f x y
let rec cases_pattern_expr_eq p1 p2 =
- if p1 == p2 then true
- else match p1, p2 with
- | CPatAlias(_,a1,i1), CPatAlias(_,a2,i2) ->
+ if CAst.(p1.v == p2.v) then true
+ else match CAst.(p1.v, p2.v) with
+ | CPatAlias(a1,i1), CPatAlias(a2,i2) ->
Id.equal i1 i2 && cases_pattern_expr_eq a1 a2
- | CPatCstr(_,c1,a1,b1), CPatCstr(_,c2,a2,b2) ->
+ | CPatCstr(c1,a1,b1), CPatCstr(c2,a2,b2) ->
eq_reference c1 c2 &&
Option.equal (List.equal cases_pattern_expr_eq) a1 a2 &&
List.equal cases_pattern_expr_eq b1 b2
- | CPatAtom(_,r1), CPatAtom(_,r2) ->
+ | CPatAtom(r1), CPatAtom(r2) ->
Option.equal eq_reference r1 r2
- | CPatOr (_, a1), CPatOr (_, a2) ->
+ | CPatOr a1, CPatOr a2 ->
List.equal cases_pattern_expr_eq a1 a2
- | CPatNotation (_, n1, s1, l1), CPatNotation (_, n2, s2, l2) ->
+ | CPatNotation (n1, s1, l1), CPatNotation (n2, s2, l2) ->
String.equal n1 n2 &&
cases_pattern_notation_substitution_eq s1 s2 &&
List.equal cases_pattern_expr_eq l1 l2
- | CPatPrim(_,i1), CPatPrim(_,i2) ->
+ | CPatPrim i1, CPatPrim i2 ->
prim_token_eq i1 i2
- | CPatRecord (_, l1), CPatRecord (_, l2) ->
+ | CPatRecord l1, CPatRecord l2 ->
let equal (r1, e1) (r2, e2) =
eq_reference r1 r2 && cases_pattern_expr_eq e1 e2
in
List.equal equal l1 l2
- | CPatDelimiters(_,s1,e1), CPatDelimiters(_,s2,e2) ->
+ | CPatDelimiters(s1,e1), CPatDelimiters(s2,e2) ->
String.equal s1 s2 && cases_pattern_expr_eq e1 e2
| _ -> false
@@ -98,78 +98,78 @@ let eq_universes u1 u2 =
| _, _ -> false
let rec constr_expr_eq e1 e2 =
- if e1 == e2 then true
- else match e1, e2 with
+ if CAst.(e1.v == e2.v) then true
+ else match CAst.(e1.v, e2.v) with
| CRef (r1,u1), CRef (r2,u2) -> eq_reference r1 r2 && eq_universes u1 u2
- | CFix(_,id1,fl1), CFix(_,id2,fl2) ->
+ | CFix(id1,fl1), CFix(id2,fl2) ->
eq_located Id.equal id1 id2 &&
List.equal fix_expr_eq fl1 fl2
- | CCoFix(_,id1,fl1), CCoFix(_,id2,fl2) ->
+ | CCoFix(id1,fl1), CCoFix(id2,fl2) ->
eq_located Id.equal id1 id2 &&
List.equal cofix_expr_eq fl1 fl2
- | CProdN(_,bl1,a1), CProdN(_,bl2,a2) ->
+ | CProdN(bl1,a1), CProdN(bl2,a2) ->
List.equal binder_expr_eq bl1 bl2 &&
constr_expr_eq a1 a2
- | CLambdaN(_,bl1,a1), CLambdaN(_,bl2,a2) ->
+ | CLambdaN(bl1,a1), CLambdaN(bl2,a2) ->
List.equal binder_expr_eq bl1 bl2 &&
constr_expr_eq a1 a2
- | CLetIn(_,(_,na1),a1,t1,b1), CLetIn(_,(_,na2),a2,t2,b2) ->
+ | CLetIn((_,na1),a1,t1,b1), CLetIn((_,na2),a2,t2,b2) ->
Name.equal na1 na2 &&
constr_expr_eq a1 a2 &&
Option.equal constr_expr_eq t1 t2 &&
constr_expr_eq b1 b2
- | CAppExpl(_,(proj1,r1,_),al1), CAppExpl(_,(proj2,r2,_),al2) ->
+ | CAppExpl((proj1,r1,_),al1), CAppExpl((proj2,r2,_),al2) ->
Option.equal Int.equal proj1 proj2 &&
eq_reference r1 r2 &&
List.equal constr_expr_eq al1 al2
- | CApp(_,(proj1,e1),al1), CApp(_,(proj2,e2),al2) ->
+ | CApp((proj1,e1),al1), CApp((proj2,e2),al2) ->
Option.equal Int.equal proj1 proj2 &&
constr_expr_eq e1 e2 &&
List.equal args_eq al1 al2
- | CRecord (_, l1), CRecord (_, l2) ->
+ | CRecord l1, CRecord l2 ->
let field_eq (r1, e1) (r2, e2) =
eq_reference r1 r2 && constr_expr_eq e1 e2
in
List.equal field_eq l1 l2
- | CCases(_,_,r1,a1,brl1), CCases(_,_,r2,a2,brl2) ->
+ | CCases(_,r1,a1,brl1), CCases(_,r2,a2,brl2) ->
(** Don't care about the case_style *)
Option.equal constr_expr_eq r1 r2 &&
List.equal case_expr_eq a1 a2 &&
List.equal branch_expr_eq brl1 brl2
- | CLetTuple (_, n1, (m1, e1), t1, b1), CLetTuple (_, n2, (m2, e2), t2, b2) ->
+ | CLetTuple (n1, (m1, e1), t1, b1), CLetTuple (n2, (m2, e2), t2, b2) ->
List.equal (eq_located Name.equal) n1 n2 &&
Option.equal (eq_located Name.equal) m1 m2 &&
Option.equal constr_expr_eq e1 e2 &&
constr_expr_eq t1 t2 &&
constr_expr_eq b1 b2
- | CIf (_, e1, (n1, r1), t1, f1), CIf (_, e2, (n2, r2), t2, f2) ->
+ | CIf (e1, (n1, r1), t1, f1), CIf (e2, (n2, r2), t2, f2) ->
constr_expr_eq e1 e2 &&
Option.equal (eq_located Name.equal) n1 n2 &&
Option.equal constr_expr_eq r1 r2 &&
constr_expr_eq t1 t2 &&
constr_expr_eq f1 f2
| CHole _, CHole _ -> true
- | CPatVar(_,i1), CPatVar(_,i2) ->
+ | CPatVar i1, CPatVar i2 ->
Id.equal i1 i2
- | CEvar (_, id1, c1), CEvar (_, id2, c2) ->
+ | CEvar (id1, c1), CEvar (id2, c2) ->
Id.equal id1 id2 && List.equal instance_eq c1 c2
- | CSort(_,s1), CSort(_,s2) ->
+ | CSort s1, CSort s2 ->
Miscops.glob_sort_eq s1 s2
- | CCast(_,a1,(CastConv b1|CastVM b1)), CCast(_,a2,(CastConv b2|CastVM b2)) ->
+ | CCast(a1,(CastConv b1|CastVM b1)), CCast(a2,(CastConv b2|CastVM b2)) ->
constr_expr_eq a1 a2 &&
constr_expr_eq b1 b2
- | CCast(_,a1,CastCoerce), CCast(_,a2, CastCoerce) ->
+ | CCast(a1,CastCoerce), CCast(a2, CastCoerce) ->
constr_expr_eq a1 a2
- | CNotation(_, n1, s1), CNotation(_, n2, s2) ->
+ | CNotation(n1, s1), CNotation(n2, s2) ->
String.equal n1 n2 &&
constr_notation_substitution_eq s1 s2
- | CPrim(_,i1), CPrim(_,i2) ->
+ | CPrim i1, CPrim i2 ->
prim_token_eq i1 i2
- | CGeneralization (_, bk1, ak1, e1), CGeneralization (_, bk2, ak2, e2) ->
+ | CGeneralization (bk1, ak1, e1), CGeneralization (bk2, ak2, e2) ->
binding_kind_eq bk1 bk2 &&
Option.equal abstraction_kind_eq ak1 ak2 &&
constr_expr_eq e1 e2
- | CDelimiters(_,s1,e1), CDelimiters(_,s2,e2) ->
+ | CDelimiters(s1,e1), CDelimiters(s2,e2) ->
String.equal s1 s2 &&
constr_expr_eq e1 e2
| _ -> false
@@ -183,7 +183,7 @@ and case_expr_eq (e1, n1, p1) (e2, n2, p2) =
Option.equal (eq_located Name.equal) n1 n2 &&
Option.equal cases_pattern_expr_eq p1 p2
-and branch_expr_eq (_, p1, e1) (_, p2, e2) =
+and branch_expr_eq (_, (p1, e1)) (_, (p2, e2)) =
List.equal (eq_located (List.equal cases_pattern_expr_eq)) p1 p2 &&
constr_expr_eq e1 e2
@@ -228,67 +228,34 @@ and constr_notation_substitution_eq (e1, el1, bl1) (e2, el2, bl2) =
and instance_eq (x1,c1) (x2,c2) =
Id.equal x1 x2 && constr_expr_eq c1 c2
-let constr_loc = function
- | CRef (Ident (loc,_),_) -> loc
- | CRef (Qualid (loc,_),_) -> loc
- | CFix (loc,_,_) -> loc
- | CCoFix (loc,_,_) -> loc
- | CProdN (loc,_,_) -> loc
- | CLambdaN (loc,_,_) -> loc
- | CLetIn (loc,_,_,_,_) -> loc
- | CAppExpl (loc,_,_) -> loc
- | CApp (loc,_,_) -> loc
- | CRecord (loc,_) -> loc
- | CCases (loc,_,_,_,_) -> loc
- | CLetTuple (loc,_,_,_,_) -> loc
- | CIf (loc,_,_,_,_) -> loc
- | CHole (loc,_,_,_) -> loc
- | CPatVar (loc,_) -> loc
- | CEvar (loc,_,_) -> loc
- | CSort (loc,_) -> loc
- | CCast (loc,_,_) -> loc
- | CNotation (loc,_,_) -> loc
- | CGeneralization (loc,_,_,_) -> loc
- | CPrim (loc,_) -> loc
- | CDelimiters (loc,_,_) -> loc
-
-let cases_pattern_expr_loc = function
- | CPatAlias (loc,_,_) -> loc
- | CPatCstr (loc,_,_,_) -> loc
- | CPatAtom (loc,_) -> loc
- | CPatOr (loc,_) -> loc
- | CPatNotation (loc,_,_,_) -> loc
- | CPatRecord (loc, _) -> loc
- | CPatPrim (loc,_) -> loc
- | CPatDelimiters (loc,_,_) -> loc
- | CPatCast(loc,_,_) -> loc
+let constr_loc c = CAst.(c.loc)
+let cases_pattern_expr_loc cp = CAst.(cp.loc)
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
+ | CLocalPattern (loc,_) -> loc
let local_binders_loc bll = match bll with
- | [] -> Loc.ghost
- | h :: l ->
- Loc.merge (local_binder_loc h) (local_binder_loc (List.last bll))
+ | [] -> None
+ | h :: l -> Loc.merge_opt (local_binder_loc h) (local_binder_loc (List.last bll))
(** Pseudo-constructors *)
-let mkIdentC id = CRef (Ident (Loc.ghost, id),None)
-let mkRefC r = CRef (r,None)
-let mkCastC (a,k) = CCast (Loc.ghost,a,k)
-let mkLambdaC (idl,bk,a,b) = CLambdaN (Loc.ghost,[idl,bk,a],b)
-let mkLetInC (id,a,t,b) = CLetIn (Loc.ghost,id,a,t,b)
-let mkProdC (idl,bk,a,b) = CProdN (Loc.ghost,[idl,bk,a],b)
+let mkIdentC id = CAst.make @@ CRef (Ident (Loc.tag id),None)
+let mkRefC r = CAst.make @@ CRef (r,None)
+let mkCastC (a,k) = CAst.make @@ CCast (a,k)
+let mkLambdaC (idl,bk,a,b) = CAst.make @@ CLambdaN ([idl,bk,a],b)
+let mkLetInC (id,a,t,b) = CAst.make @@ CLetIn (id,a,t,b)
+let mkProdC (idl,bk,a,b) = CAst.make @@ CProdN ([idl,bk,a],b)
let mkAppC (f,l) =
let l = List.map (fun x -> (x,None)) l in
- match f with
- | CApp (_,g,l') -> CApp (Loc.ghost, g, l' @ l)
- | _ -> CApp (Loc.ghost, (None, f), l)
+ match CAst.(f.v) with
+ | CApp (g,l') -> CAst.make @@ CApp (g, l' @ l)
+ | _ -> CAst.make @@ CApp ((None, f), l)
let add_name_in_env env n =
match snd n with
@@ -297,67 +264,66 @@ let add_name_in_env env n =
let (fresh_var, fresh_var_hook) = Hook.make ~default:(fun _ _ -> assert false) ()
-let expand_binders mkC loc bl c =
- let rec loop loc bl c =
+let expand_binders ?loc mkC bl c =
+ let rec loop ?loc bl c =
match bl with
| [] -> ([], c)
| b :: bl ->
match b with
| CLocalDef ((loc1,_) as n, oty, b) ->
- let env, c = loop (Loc.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, CLetIn (loc,n,oty,b,c))
+ (env, CAst.make ?loc @@ CLetIn (n,oty,b,c))
| CLocalAssum ((loc1,_)::_ as nl, bk, t) ->
- let env, c = loop (Loc.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.merge loc1 loc) bl c in
+ (env, mkC ?loc (nl,bk,t) c)
+ | CLocalAssum ([],_,_) -> loop ?loc bl c
+ | CLocalPattern (loc1, (p, ty)) ->
+ 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 -> CHole (loc1, None, IntroAnonymous, None)
+ | None -> CAst.make ?loc:loc1 @@ CHole (None, IntroAnonymous, None)
in
- let e = CRef (Libnames.Ident (loc1, ni), None) in
- let c =
+ let e = CAst.make @@ CRef (Libnames.Ident (loc1, ni), None) in
+ let c = CAst.make ?loc @@
CCases
- (loc, LetPatternStyle, None, [(e,None,None)],
- [(loc1, [(loc1,[p])], c)])
+ (LetPatternStyle, None, [(e,None,None)],
+ [(Loc.tag ?loc:loc1 ([(loc1,[p])], c))])
in
- (ni :: env, mkC loc ([id],Default Explicit,ty) c)
+ (ni :: env, mkC ?loc ([id],Default Explicit,ty) c)
in
- let (_, c) = loop loc bl c in
+ let (_, c) = loop ?loc bl c in
c
-let mkCProdN loc bll c =
- let mk loc b c = CProdN (loc,[b],c) in
- expand_binders mk loc bll c
+let mkCProdN ?loc bll c =
+ let mk ?loc b c = CAst.make ?loc @@ CProdN ([b],c) in
+ expand_binders ?loc mk bll c
-let mkCLambdaN loc bll c =
- let mk loc b c = CLambdaN (loc,[b],c) in
- expand_binders mk loc bll c
+let mkCLambdaN ?loc bll c =
+ let mk ?loc b c = CAst.make ?loc @@ CLambdaN ([b],c) in
+ expand_binders ?loc mk bll c
(* Deprecated *)
-let abstract_constr_expr c bl = mkCLambdaN (local_binders_loc bl) bl c
-let prod_constr_expr c bl = mkCProdN (local_binders_loc bl) bl c
+let abstract_constr_expr c bl = mkCLambdaN ?loc:(local_binders_loc bl) bl c
+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
- | CRef (Ident (loc,id),_) -> (loc,id)
- | a -> CErrors.user_err ~loc:(constr_loc a)
+ | { CAst.v = CRef (Ident (loc,id),_); _ } -> (loc,id)
+ | { CAst.loc; _ } -> CErrors.user_err ?loc
~hdr:"coerce_to_id"
(str "This expression should be a simple identifier.")
let coerce_to_name = function
- | CRef (Ident (loc,id),_) -> (loc,Name id)
- | CHole (loc,_,_,_) -> (loc,Anonymous)
- | a -> CErrors.user_err
- ~loc:(constr_loc a) ~hdr:"coerce_to_name"
- (str "This expression should be a name.")
+ | { CAst.v = CRef (Ident (loc,id),_) } -> (loc,Name id)
+ | { CAst.loc; CAst.v = CHole (_,_,_) } -> (loc,Anonymous)
+ | { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_name"
+ (str "This expression should be a name.")
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index b547288e3..0ff51b060 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 local_binders_loc : local_binder_expr list -> Loc.t
+val constr_loc : constr_expr -> Loc.t option
+val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t option
+val local_binders_loc : local_binder_expr list -> Loc.t option
(** {6 Constructors}*)
@@ -48,10 +48,10 @@ val mkLambdaC : Name.t located list * binder_kind * constr_expr * constr_expr ->
val mkLetInC : Name.t located * constr_expr * constr_expr option * constr_expr -> constr_expr
val mkProdC : Name.t located list * binder_kind * constr_expr * constr_expr -> constr_expr
-val mkCLambdaN : Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
+val mkCLambdaN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
(** Same as [abstract_constr_expr], with location *)
-val mkCProdN : Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
+val mkCProdN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr
(** Same as [prod_constr_expr], with location *)
(** @deprecated variant of mkCLambdaN *)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 58b38cdac..4c29fc809 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -17,6 +17,7 @@ open Termops
open Libnames
open Globnames
open Impargs
+open CAst
open Constrexpr
open Constrexpr_ops
open Notation_ops
@@ -107,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
@@ -143,45 +144,45 @@ module PrintingConstructor = Goptions.MakeRefTable(PrintingRecordConstructor)
let insert_delimiters e = function
| None -> e
- | Some sc -> CDelimiters (Loc.ghost,sc,e)
+ | Some sc -> CAst.make @@ CDelimiters (sc,e)
-let insert_pat_delimiters loc p = function
+let insert_pat_delimiters ?loc p = function
| None -> p
- | Some sc -> CPatDelimiters (loc,sc,p)
+ | Some sc -> CAst.make ?loc @@ CPatDelimiters (sc,p)
-let insert_pat_alias loc p = function
+let insert_pat_alias ?loc p = function
| Anonymous -> p
- | Name id -> CPatAlias (loc,p,id)
+ | Name id -> CAst.make ?loc @@ CPatAlias (p,id)
(**********************************************************************)
(* conversion of references *)
-let extern_evar loc n l = CEvar (loc,n,l)
+let extern_evar n l = CEvar (n,l)
(** We allow customization of the global_reference printer.
For instance, in the debugger the tables of global references
may be inaccurate *)
-let default_extern_reference loc vars r =
- Qualid (loc,shortest_qualid_of_global vars r)
+let default_extern_reference ?loc vars r =
+ Qualid (Loc.tag ?loc @@ shortest_qualid_of_global vars r)
let my_extern_reference = ref default_extern_reference
let set_extern_reference f = my_extern_reference := f
let get_extern_reference () = !my_extern_reference
-let extern_reference loc vars l = !my_extern_reference loc vars l
+let extern_reference ?loc vars l = !my_extern_reference ?loc vars l
(**********************************************************************)
(* mapping patterns to cases_pattern_expr *)
let add_patt_for_params ind l =
if !Flags.in_debugger then l else
- Util.List.addn (Inductiveops.inductive_nparamdecls ind) (CPatAtom (Loc.ghost,None)) l
+ Util.List.addn (Inductiveops.inductive_nparamdecls ind) (CAst.make @@ CPatAtom None) l
let add_cpatt_for_params ind l =
if !Flags.in_debugger then l else
- Util.List.addn (Inductiveops.inductive_nparamdecls ind) (PatVar (Loc.ghost,Anonymous)) l
+ Util.List.addn (Inductiveops.inductive_nparamdecls ind) (CAst.make @@ PatVar Anonymous) l
let drop_implicits_in_patt cst nb_expl args =
let impl_st = (implicits_of_global cst) in
@@ -189,7 +190,7 @@ let drop_implicits_in_patt cst nb_expl args =
let rec impls_fit l = function
|[],t -> Some (List.rev_append l t)
|_,[] -> None
- |h::t,CPatAtom(_,None)::tt when is_status_implicit h -> impls_fit l (t,tt)
+ |h::t, { CAst.v = CPatAtom None }::tt when is_status_implicit h -> impls_fit l (t,tt)
|h::_,_ when is_status_implicit h -> None
|_::t,hh::tt -> impls_fit (hh::l) (t,tt)
in let rec aux = function
@@ -235,8 +236,8 @@ let expand_curly_brackets loc mknot ntn l =
(* side effect *)
mknot (loc,!ntn',l)
-let destPrim = function CPrim(_,t) -> Some t | _ -> None
-let destPatPrim = function CPatPrim(_,t) -> Some t | _ -> None
+let destPrim = function { CAst.v = CPrim t } -> Some t | _ -> None
+let destPatPrim = function { CAst.v = CPatPrim t } -> Some t | _ -> None
let make_notation_gen loc ntn mknot mkprim destprim l =
if has_curly_brackets ntn
@@ -258,23 +259,23 @@ 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
- CNotation (loc,ntn,subst)
+ CAst.make ?loc @@ CNotation (ntn,subst)
else
make_notation_gen loc ntn
- (fun (loc,ntn,l) -> CNotation (loc,ntn,(l,[],[])))
- (fun (loc,p) -> CPrim (loc,p))
+ (fun (loc,ntn,l) -> CAst.make ?loc @@ CNotation (ntn,(l,[],[])))
+ (fun (loc,p) -> CAst.make ?loc @@ CPrim p)
destPrim terms
-let make_pat_notation loc ntn (terms,termlists as subst) args =
- if not (List.is_empty termlists) then CPatNotation (loc,ntn,subst,args) else
+let make_pat_notation ?loc ntn (terms,termlists as subst) args =
+ if not (List.is_empty termlists) then (CAst.make ?loc @@ CPatNotation (ntn,subst,args)) else
make_notation_gen loc ntn
- (fun (loc,ntn,l) -> CPatNotation (loc,ntn,(l,[]),args))
- (fun (loc,p) -> CPatPrim (loc,p))
+ (fun (loc,ntn,l) -> CAst.make ?loc @@ CPatNotation (ntn,(l,[]),args))
+ (fun (loc,p) -> CAst.make ?loc @@ CPatPrim p)
destPatPrim terms
-let mkPat loc qid l =
+let mkPat ?loc qid l = CAst.make ?loc @@
(* Normally irrelevant test with v8 syntax, but let's do it anyway *)
- if List.is_empty l then CPatAtom (loc,Some qid) else CPatCstr (loc,qid,None,l)
+ if List.is_empty l then CPatAtom (Some qid) else CPatCstr (qid,None,l)
let pattern_printable_in_both_syntax (ind,_ as c) =
let impl_st = extract_impargs_data (implicits_of_global (ConstructRef c)) in
@@ -290,11 +291,11 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
(* pboutill: There are letins in pat which is incompatible with notations and
not explicit application. *)
match pat with
- | PatCstr(loc,cstrsp,args,na)
+ | { loc; v = 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
- CPatCstr (loc, c, Some (add_patt_for_params (fst cstrsp) args), [])
+ CAst.make ?loc @@ CPatCstr (c, Some (add_patt_for_params (fst cstrsp) args), [])
| _ ->
try
if !Flags.raw_print || !print_no_symbol then raise No_match;
@@ -303,17 +304,17 @@ 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 (CPatPrim(loc,p)) key) na
+ insert_pat_alias ?loc (insert_pat_delimiters ?loc (CAst.make ?loc @@ CPatPrim p) key) na
with No_match ->
try
if !Flags.raw_print || !print_no_symbol then raise No_match;
extern_notation_pattern scopes vars pat
(uninterp_cases_pattern_notations pat)
with No_match ->
- match pat with
- | PatVar (loc,Name id) -> CPatAtom (loc,Some (Ident (loc,id)))
- | PatVar (loc,Anonymous) -> CPatAtom (loc, None)
- | PatCstr(loc,cstrsp,args,na) ->
+ CAst.map_with_loc (fun ?loc -> function
+ | PatVar (Name id) -> CPatAtom (Some (Ident (loc,id)))
+ | PatVar (Anonymous) -> CPatAtom None
+ | PatCstr(cstrsp,args,na) ->
let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
let p =
try
@@ -326,26 +327,32 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
| Some c :: q ->
match args with
| [] -> raise No_match
- | CPatAtom(_, None) :: tail -> ip q tail acc
+
+
+
+
+
+ | { CAst.v = 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
- CPatRecord(loc, List.rev (ip projs args []))
+ 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 CPatCstr (loc, c, None, args)
- else CPatCstr (loc, c, Some (add_patt_for_params (fst cstrsp) args), [])
+ then CPatCstr (c, None, args)
+ else 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 -> CPatCstr (loc, c, None, true_args)
- |None -> CPatCstr (loc, 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))
+ | Some true_args -> CPatCstr (c, None, true_args)
+ | None -> CPatCstr (c, Some full_args, [])
+ in (insert_pat_alias ?loc (CAst.make ?loc p) na).v
+ ) pat
+and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args))
(tmp_scope, scopes as allscopes) vars =
function
| NotationRule (sc,ntn) ->
@@ -372,11 +379,11 @@ and apply_notation_to_pattern loc gr ((subst,substlist),(nb_to_drop,more_args))
|Some true_args -> true_args
|None -> raise No_match
in
- insert_pat_delimiters loc
- (make_pat_notation loc ntn (l,ll) l2') key
+ insert_pat_delimiters ?loc
+ (make_pat_notation ?loc ntn (l,ll) l2') key
end
| SynDefRule kn ->
- let qid = Qualid (loc, shortest_qualid_of_syndef vars kn) in
+ let qid = Qualid (Loc.tag ?loc @@ shortest_qualid_of_syndef vars kn) in
let l1 =
List.rev_map (fun (c,(scopt,scl)) ->
extern_cases_pattern_in_scope (scopt,scl@scopes) vars c)
@@ -389,19 +396,20 @@ and apply_notation_to_pattern loc gr ((subst,substlist),(nb_to_drop,more_args))
|None -> raise No_match
in
assert (List.is_empty substlist);
- mkPat loc qid (List.rev_append l1 l2')
+ mkPat ?loc qid (List.rev_append l1 l2')
and extern_notation_pattern (tmp_scope,scopes as allscopes) vars t = function
| [] -> raise No_match
| (keyrule,pat,n as _rule)::rules ->
try
if List.mem keyrule !print_non_active_notations then raise No_match;
- match t with
- | PatCstr (loc,cstr,_,na) ->
- let p = apply_notation_to_pattern loc (ConstructRef cstr)
+ let loc = t.loc in
+ match t.v with
+ | PatCstr (cstr,_,na) ->
+ let p = apply_notation_to_pattern ?loc (ConstructRef cstr)
(match_notation_constr_cases_pattern t pat) allscopes vars keyrule in
- insert_pat_alias loc p na
- | PatVar (loc,Anonymous) -> CPatAtom (loc, None)
- | PatVar (loc,Name id) -> CPatAtom (loc, Some (Ident (loc,id)))
+ insert_pat_alias ?loc p na
+ | PatVar Anonymous -> CAst.make ?loc @@ CPatAtom None
+ | PatVar (Name id) -> CAst.make ?loc @@ CPatAtom (Some (Ident (loc,id)))
with
No_match -> extern_notation_pattern allscopes vars t rules
@@ -410,7 +418,7 @@ let rec extern_notation_ind_pattern allscopes vars ind args = function
| (keyrule,pat,n as _rule)::rules ->
try
if List.mem keyrule !print_non_active_notations then raise No_match;
- apply_notation_to_pattern Loc.ghost (IndRef ind)
+ apply_notation_to_pattern (IndRef ind)
(match_notation_constr_ind_pattern ind args pat) allscopes vars keyrule
with
No_match -> extern_notation_ind_pattern allscopes vars ind args rules
@@ -419,9 +427,9 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args =
(* pboutill: There are letins in pat which is incompatible with notations and
not explicit application. *)
if !Flags.in_debugger||Inductiveops.inductive_has_local_defs ind then
- let c = extern_reference Loc.ghost vars (IndRef ind) in
+ let c = extern_reference vars (IndRef ind) in
let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
- CPatCstr (Loc.ghost, c, Some (add_patt_for_params ind args), [])
+ CAst.make @@ CPatCstr (c, Some (add_patt_for_params ind args), [])
else
try
if !Flags.raw_print || !print_no_symbol then raise No_match;
@@ -429,18 +437,18 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args =
match availability_of_prim_token p sc scopes with
| None -> raise No_match
| Some key ->
- insert_pat_delimiters Loc.ghost (CPatPrim(Loc.ghost,p)) key
+ insert_pat_delimiters (CAst.make @@ CPatPrim p) key
with No_match ->
try
if !Flags.raw_print || !print_no_symbol then raise No_match;
extern_notation_ind_pattern scopes vars ind args
(uninterp_ind_pattern_notations ind)
with No_match ->
- let c = extern_reference Loc.ghost vars (IndRef ind) in
+ let c = extern_reference vars (IndRef ind) in
let args = List.map (extern_cases_pattern_in_scope scopes vars) args in
match drop_implicits_in_patt (IndRef ind) 0 args with
- |Some true_args -> CPatCstr (Loc.ghost, c, None, true_args)
- |None -> CPatCstr (Loc.ghost, c, Some args, [])
+ |Some true_args -> CAst.make @@ CPatCstr (c, None, true_args)
+ |None -> CAst.make @@ CPatCstr (c, Some args, [])
let extern_cases_pattern vars p =
extern_cases_pattern_in_scope (None,[]) vars p
@@ -461,11 +469,11 @@ let is_projection nargs = function
else None
with Not_found -> None)
| _ -> None
-
+
let is_hole = function CHole _ | CEvar _ -> true | _ -> false
let is_significant_implicit a =
- not (is_hole a)
+ not (is_hole (a.CAst.v))
let is_needed_for_correct_partial_application tail imp =
List.is_empty tail && not (maximal_insertion_of imp)
@@ -474,7 +482,7 @@ exception Expl
(* Implicit args indexes are in ascending order *)
(* inctx is useful only if there is a last argument to be deduced from ctxt *)
-let explicitize loc inctx impl (cf,f) args =
+let explicitize inctx impl (cf,f) args =
let impl = if !Constrintern.parsing_explicit then [] else impl in
let n = List.length args in
let rec exprec q = function
@@ -489,7 +497,7 @@ let explicitize loc inctx impl (cf,f) args =
is_significant_implicit (Lazy.force a))
in
if visible then
- (Lazy.force a,Some (Loc.ghost, ExplByName (name_of_implicit imp))) :: tail
+ (Lazy.force a,Some (Loc.tag @@ ExplByName (name_of_implicit imp))) :: tail
else
tail
| a::args, _::impl -> (Lazy.force a,None) :: exprec (q+1) (args,impl)
@@ -511,41 +519,41 @@ let explicitize loc inctx impl (cf,f) args =
let args1 = exprec 1 (args1,impl1) in
let args2 = exprec (i+1) (args2,impl2) in
let ip = Some (List.length args1) in
- CApp (loc,(ip,f),args1@args2)
+ CApp ((ip,f),args1@args2)
| None ->
let args = exprec 1 (args,impl) in
- if List.is_empty args then f else CApp (loc, (None, f), args)
+ if List.is_empty args then f.CAst.v else CApp ((None, f), args)
in
try expl ()
with Expl ->
- let f',us = match f with CRef (f,us) -> f,us | _ -> assert false in
+ let f',us = match f with { CAst.v = CRef (f,us) } -> f,us | _ -> assert false in
let ip = if !print_projections then ip else None in
- CAppExpl (loc, (ip, f', us), List.map Lazy.force args)
+ CAppExpl ((ip, f', us), List.map Lazy.force args)
let is_start_implicit = function
| imp :: _ -> is_status_implicit imp && maximal_insertion_of imp
| [] -> false
-let extern_global loc impl f us =
+let extern_global impl f us =
if not !Constrintern.parsing_explicit && is_start_implicit impl
then
- CAppExpl (loc, (None, f, us), [])
+ CAppExpl ((None, f, us), [])
else
CRef (f,us)
-let extern_app loc inctx impl (cf,f) us args =
+let extern_app inctx impl (cf,f) us args =
if List.is_empty args then
(* If coming from a notation "Notation a := @b" *)
- CAppExpl (loc, (None, f, us), [])
+ CAppExpl ((None, f, us), [])
else if not !Constrintern.parsing_explicit &&
((!Flags.raw_print ||
(!print_implicits && not !print_implicits_explicit_args)) &&
List.exists is_status_implicit impl)
then
let args = List.map Lazy.force args in
- CAppExpl (loc, (is_projection (List.length args) cf,f,us), args)
+ CAppExpl ((is_projection (List.length args) cf,f,us), args)
else
- explicitize loc inctx impl (cf,CRef (f,us)) args
+ explicitize inctx impl (cf, CAst.make @@ CRef (f,us)) args
let rec fill_arg_scopes args subscopes scopes = match args, subscopes with
| [], _ -> []
@@ -559,7 +567,7 @@ let extern_args extern env args =
List.map map args
let match_coercion_app = function
- | GApp (loc,GRef (_,r,_),args) -> Some (loc, r, 0, args)
+ | {loc; v = GApp ({ v = GRef (r,_) },args)} -> Some (loc, r, 0, args)
| _ -> None
let rec remove_coercions inctx c =
@@ -581,13 +589,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 GApp (loc,a',l)
+ if List.is_empty l then a' else CAst.make ?loc @@ GApp (a',l)
| _ -> c
with Not_found -> c)
| _ -> c
let rec flatten_application = function
- | GApp (loc,GApp(_,a,l'),l) -> flatten_application (GApp (loc,a,l'@l))
+ | {loc; v = GApp ({ v = GApp(a,l')},l)} -> flatten_application (CAst.make ?loc @@ GApp (a,l'@l))
| a -> a
(**********************************************************************)
@@ -599,7 +607,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 (CPrim (loc_of_glob_constr r,n)) key)
+ | Some key -> Some (insert_delimiters (CAst.make ?loc:(loc_of_glob_constr r) @@ CPrim n) key)
with No_match ->
None
@@ -607,16 +615,18 @@ let extern_optimal_prim_token scopes r r' =
let c = extern_possible_prim_token scopes r in
let c' = if r==r' then None else extern_possible_prim_token scopes r' in
match c,c' with
- | Some n, (Some (CDelimiters _) | None) | _, Some n -> n
+ | Some n, (Some ({ CAst.v = CDelimiters _}) | None) | _, Some n -> n
| _ -> raise No_match
(**********************************************************************)
(* mapping decl *)
let extended_glob_local_binder_of_decl loc = function
- | (p,bk,None,t) -> GLocalAssum (loc,p,bk,t)
- | (p,bk,Some x,GHole (_, _, Misctypes.IntroAnonymous, None)) -> GLocalDef (loc,p,bk,x,None)
- | (p,bk,Some x,t) -> GLocalDef (loc,p,bk,x,Some t)
+ | (p,bk,None,t) -> GLocalAssum (p,bk,t)
+ | (p,bk,Some x, { v = GHole ( _, Misctypes.IntroAnonymous, None) } ) -> GLocalDef (p,bk,x,None)
+ | (p,bk,Some x,t) -> GLocalDef (p,bk,x,Some t)
+
+let extended_glob_local_binder_of_decl ?loc u = CAst.make ?loc (extended_glob_local_binder_of_decl loc u)
(**********************************************************************)
(* mapping glob_constr to constr_expr *)
@@ -641,25 +651,25 @@ 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 -> match r' with
- | GRef (loc,ref,us) ->
- extern_global loc (select_stronger_impargs (implicits_of_global ref))
- (extern_reference loc vars ref) (extern_universes us)
+ with No_match -> CAst.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)
- | GVar (loc,id) -> CRef (Ident (loc,id),None)
+ | GVar id -> CRef (Ident (loc,id),None)
- | GEvar (loc,n,[]) when !print_meta_as_hole -> CHole (loc, None, Misctypes.IntroAnonymous, None)
+ | GEvar (n,[]) when !print_meta_as_hole -> CHole (None, Misctypes.IntroAnonymous, None)
- | GEvar (loc,n,l) ->
- extern_evar loc n (List.map (on_snd (extern false scopes vars)) l)
+ | GEvar (n,l) ->
+ extern_evar n (List.map (on_snd (extern false scopes vars)) l)
- | GPatVar (loc,(b,n)) ->
- if !print_meta_as_hole then CHole (loc, None, Misctypes.IntroAnonymous, None) else
- if b then CPatVar (loc,n) else CEvar (loc,n,[])
+ | GPatVar (b,n) ->
+ if !print_meta_as_hole then CHole (None, Misctypes.IntroAnonymous, None) else
+ if b then CPatVar n else CEvar (n,[])
- | GApp (loc,f,args) ->
+ | GApp (f,args) ->
(match f with
- | GRef (rloc,ref,us) ->
+ | {loc = rloc; v = GRef (ref,us) } ->
let subscopes = find_arguments_scope ref in
let args = fill_arg_scopes args subscopes (snd scopes) in
begin
@@ -698,119 +708,120 @@ 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 (loc, List.rev (ip projs locals args []))
+ CRecord (List.rev (ip projs locals args []))
with
| Not_found | No_match | Exit ->
let args = extern_args (extern true) vars args in
- extern_app loc inctx
+ extern_app inctx
(select_stronger_impargs (implicits_of_global ref))
- (Some ref,extern_reference rloc vars ref) (extern_universes us) args
+ (Some ref,extern_reference ?loc:rloc vars ref) (extern_universes us) args
end
-
+
| _ ->
- explicitize loc inctx [] (None,sub_extern false scopes vars f)
+ explicitize inctx [] (None,sub_extern false scopes vars f)
(List.map (fun c -> lazy (sub_extern true scopes vars c)) args))
- | GLetIn (loc,na,b,t,c) ->
- CLetIn (loc,(loc,na),sub_extern false scopes vars b,
+ | GLetIn (na,b,t,c) ->
+ CLetIn ((loc,na),sub_extern false scopes vars b,
Option.map (extern_typ scopes vars) t,
extern inctx scopes (add_vname vars na) c)
- | GProd (loc,na,bk,t,c) ->
+ | GProd (na,bk,t,c) ->
let t = extern_typ scopes vars t in
let (idl,c) = factorize_prod scopes (add_vname vars na) na bk t c in
- CProdN (loc,[(Loc.ghost,na)::idl,Default bk,t],c)
+ CProdN ([(Loc.tag na)::idl,Default bk,t],c)
- | GLambda (loc,na,bk,t,c) ->
+ | GLambda (na,bk,t,c) ->
let t = extern_typ scopes vars t in
let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) na bk t c in
- CLambdaN (loc,[(Loc.ghost,na)::idl,Default bk,t],c)
+ CLambdaN ([(Loc.tag na)::idl,Default bk,t],c)
- | GCases (loc,sty,rtntypopt,tml,eqns) ->
+ | GCases (sty,rtntypopt,tml,eqns) ->
let vars' =
List.fold_right (name_fold Id.Set.add)
(cases_predicate_names tml) vars in
let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in
let tml = List.map (fun (tm,(na,x)) ->
let na' = match na,tm with
- | Anonymous, GVar (_, id) ->
+ | Anonymous, { v = GVar id } ->
begin match rtntypopt with
| None -> None
| Some ntn ->
if occur_glob_constr id ntn then
- Some (Loc.ghost, Anonymous)
+ Some (Loc.tag Anonymous)
else None
end
| Anonymous, _ -> None
- | Name id, GVar (_,id') when Id.equal id id' -> None
- | Name _, _ -> Some (Loc.ghost,na) in
+ | Name id, { v = GVar id' } when Id.equal id id' -> None
+ | Name _, _ -> Some (Loc.tag na) in
(sub_extern false scopes vars tm,
na',
- Option.map (fun (loc,ind,nal) ->
- let args = List.map (fun x -> PatVar (Loc.ghost, x)) nal in
+ Option.map (fun (loc,(ind,nal)) ->
+ let args = List.map (fun x -> CAst.make @@ PatVar x) nal in
let fullargs = add_cpatt_for_params ind args in
extern_ind_pattern_in_scope scopes vars ind fullargs
) x))
tml
in
let eqns = List.map (extern_eqn inctx scopes vars) eqns in
- CCases (loc,sty,rtntypopt',tml,eqns)
+ CCases (sty,rtntypopt',tml,eqns)
- | GLetTuple (loc,nal,(na,typopt),tm,b) ->
- CLetTuple (loc,List.map (fun na -> (Loc.ghost,na)) nal,
- (Option.map (fun _ -> (Loc.ghost,na)) typopt,
+ | GLetTuple (nal,(na,typopt),tm,b) ->
+ CLetTuple (List.map (fun na -> (Loc.tag na)) nal,
+ (Option.map (fun _ -> (Loc.tag na)) typopt,
Option.map (extern_typ scopes (add_vname vars na)) typopt),
sub_extern false scopes vars tm,
extern inctx scopes (List.fold_left add_vname vars nal) b)
- | GIf (loc,c,(na,typopt),b1,b2) ->
- CIf (loc,sub_extern false scopes vars c,
- (Option.map (fun _ -> (Loc.ghost,na)) typopt,
+ | GIf (c,(na,typopt),b1,b2) ->
+ CIf (sub_extern false scopes vars c,
+ (Option.map (fun _ -> (Loc.tag na)) typopt,
Option.map (extern_typ scopes (add_vname vars na)) typopt),
sub_extern inctx scopes vars b1, sub_extern inctx scopes vars b2)
- | GRec (loc,fk,idv,blv,tyv,bv) ->
+ | GRec (fk,idv,blv,tyv,bv) ->
let vars' = Array.fold_right Id.Set.add idv vars in
(match fk with
| GFix (nv,n) ->
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
let n =
match fst nv.(i) with
| None -> None
- | Some x -> Some (Loc.ghost, out_name (List.nth assums x))
+ | Some x -> Some (Loc.tag @@ out_name (List.nth assums x))
in
let ro = extern_recursion_order scopes vars (snd nv.(i)) in
- ((Loc.ghost, fi), (n, ro), bl, extern_typ scopes vars0 ty,
+ ((Loc.tag fi), (n, ro), bl, extern_typ scopes vars0 ty,
extern false scopes vars1 def)) idv
in
- CFix (loc,(loc,idv.(n)),Array.to_list listdecl)
+ CFix ((loc,idv.(n)),Array.to_list listdecl)
| 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
- ((Loc.ghost, fi),bl,extern_typ scopes vars0 tyv.(i),
+ ((Loc.tag fi),bl,extern_typ scopes vars0 tyv.(i),
sub_extern false scopes vars1 bv.(i))) idv
in
- CCoFix (loc,(loc,idv.(n)),Array.to_list listdecl))
+ CCoFix ((loc,idv.(n)),Array.to_list listdecl))
- | GSort (loc,s) -> CSort (loc,extern_glob_sort s)
+ | GSort s -> CSort (extern_glob_sort s)
- | GHole (loc,e,naming,_) -> CHole (loc, Some e, naming, None) (** TODO: extern tactics. *)
+ | GHole (e,naming,_) -> CHole (Some e, naming, None) (** TODO: extern tactics. *)
- | GCast (loc,c, c') ->
- CCast (loc,sub_extern true scopes vars c,
+ | GCast (c, c') ->
+ CCast (sub_extern true scopes vars c,
Miscops.map_cast_type (extern_typ scopes vars) c')
+ ) r'
and extern_typ (_,scopes) =
extern true (Notation.current_type_scope_name (),scopes)
@@ -820,7 +831,7 @@ and sub_extern inctx (_,scopes) = extern inctx (None,scopes)
and factorize_prod scopes vars na bk aty c =
let c = extern_typ scopes vars c in
match na, c with
- | Name id, CProdN (loc,[nal,Default bk',ty],c)
+ | Name id, { CAst.loc ; v = CProdN ([nal,Default bk',ty],c) }
when binding_kind_eq bk bk' && constr_expr_eq aty ty
&& not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) ->
nal,c
@@ -830,7 +841,7 @@ and factorize_prod scopes vars na bk aty c =
and factorize_lambda inctx scopes vars na bk aty c =
let c = sub_extern inctx scopes vars c in
match c with
- | CLambdaN (loc,[nal,Default bk',ty],c)
+ | { CAst.loc; v = CLambdaN ([nal,Default bk',ty],c) }
when binding_kind_eq bk bk' && constr_expr_eq aty ty
&& not (occur_name na ty) (* avoid na in ty escapes scope *) ->
nal,c
@@ -839,14 +850,14 @@ and factorize_lambda inctx scopes vars na bk aty c =
and extern_local_binder scopes vars = function
[] -> ([],[],[])
- | GLocalDef (_,na,bk,bd,ty)::l ->
+ | { v = GLocalDef (na,bk,bd,ty)}::l ->
let (assums,ids,l) =
extern_local_binder scopes (name_fold Id.Set.add na vars) l in
(assums,na::ids,
- CLocalDef((Loc.ghost,na), extern false scopes vars bd,
+ CLocalDef((Loc.tag na), extern false scopes vars bd,
Option.map (extern false scopes vars) ty) :: l)
- | GLocalAssum (_,na,bk,ty)::l ->
+ | { v = GLocalAssum (na,bk,ty)}::l ->
let ty = extern_typ scopes vars ty in
(match extern_local_binder scopes (name_fold Id.Set.add na vars) l with
(assums,ids,CLocalAssum(nal,k,ty')::l)
@@ -854,20 +865,20 @@ and extern_local_binder scopes vars = function
match na with Name id -> not (occur_var_constr_expr id ty')
| _ -> true ->
(na::assums,na::ids,
- CLocalAssum((Loc.ghost,na)::nal,k,ty')::l)
+ CLocalAssum((Loc.tag na)::nal,k,ty')::l)
| (assums,ids,l) ->
(na::assums,na::ids,
- CLocalAssum([(Loc.ghost,na)],Default bk,ty) :: l))
+ CLocalAssum([(Loc.tag na)],Default bk,ty) :: l))
- | GLocalPattern (_,(p,_),_,bk,ty)::l ->
+ | { v = GLocalPattern ((p,_),_,bk,ty)}::l ->
let ty =
if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in
let p = extern_cases_pattern vars p in
let (assums,ids,l) = extern_local_binder scopes vars l in
- (assums,ids, CLocalPattern(Loc.ghost,p,ty) :: l)
+ (assums,ids, CLocalPattern(Loc.tag @@ (p,ty)) :: l)
-and extern_eqn inctx scopes vars (loc,ids,pl,c) =
- (loc,[loc,List.map (extern_cases_pattern_in_scope scopes vars) pl],
+and extern_eqn inctx scopes vars (loc,(ids,pl,c)) =
+ 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
@@ -877,13 +888,13 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function
try
if List.mem keyrule !print_non_active_notations then raise No_match;
(* Adjusts to the number of arguments expected by the notation *)
- let (t,args,argsscopes,argsimpls) = match t,n with
- | GApp (_,f,args), Some n
+ let (t,args,argsscopes,argsimpls) = match t.v ,n with
+ | GApp (f,args), Some n
when List.length args >= n ->
let args1, args2 = List.chop n args in
let subscopes, impls =
- match f with
- | GRef (_,ref,us) ->
+ match f.v with
+ | GRef (ref,us) ->
let subscopes =
try List.skipn n (find_arguments_scope ref)
with Failure _ -> [] in
@@ -895,15 +906,15 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function
subscopes,impls
| _ ->
[], [] in
- (if Int.equal n 0 then f else GApp (Loc.ghost,f,args1)),
+ (if Int.equal n 0 then f else CAst.make @@ GApp (f,args1)),
args2, subscopes, impls
- | GApp (_,(GRef (_,ref,us) as f),args), None ->
+ | GApp ({ v = GRef (ref,us) } as f, args), None ->
let subscopes = find_arguments_scope ref in
let impls =
select_impargs_size
(List.length args) (implicits_of_global ref) in
f, args, subscopes, impls
- | GRef (_,ref,us), Some 0 -> GApp (Loc.ghost,t,[]), [], [], []
+ | GRef (ref,us), Some 0 -> CAst.make @@ GApp (t,[]), [], [], []
| _, None -> t, [], [], []
| _ -> raise No_match in
(* Try matching ... *)
@@ -939,12 +950,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
- if List.is_empty l then a else CApp (loc,(None,a),l) in
+ CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make 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
- explicitize loc false argsimpls (None,e) args
+ CAst.make ?loc @@ explicitize false argsimpls (None,e) args
with
No_match -> extern_notation allscopes vars t rules
@@ -964,8 +975,6 @@ let extern_glob_type vars c =
(******************************************************************)
(* Main translation function from constr -> constr_expr *)
-let loc = Loc.ghost (* for constr and pattern, locations are lost *)
-
let extern_constr_gen lax goal_concl_style scopt env sigma t =
(* "goal_concl_style" means do alpha-conversion using the "goal" convention *)
(* i.e.: avoid using the names of goal/section/rel variables and the short *)
@@ -1007,11 +1016,11 @@ let extern_closed_glob ?lax goal_concl_style env sigma t =
let any_any_branch =
(* | _ => _ *)
- (loc,[],[PatVar (loc,Anonymous)],GHole (loc,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None))
+ Loc.tag ([],[CAst.make @@ PatVar Anonymous], CAst.make @@ GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None))
-let rec glob_of_pat env sigma = function
- | PRef ref -> GRef (loc,ref,None)
- | PVar id -> GVar (loc,id)
+let rec glob_of_pat env sigma pat = CAst.make @@ match pat with
+ | PRef ref -> GRef (ref,None)
+ | PVar id -> GVar id
| PEvar (evk,l) ->
let test decl = function PVar id' -> Id.equal (NamedDecl.get_id decl) id' | _ -> false in
let l = Evd.evar_instance_array test (Evd.find sigma evk) l in
@@ -1019,36 +1028,36 @@ let rec glob_of_pat env sigma = function
| None -> Id.of_string "__"
| Some id -> id
in
- GEvar (loc,id,List.map (on_snd (glob_of_pat env sigma)) l)
+ GEvar (id,List.map (on_snd (glob_of_pat env sigma)) l)
| PRel n ->
let id = try match lookup_name_of_rel n env with
| Name id -> id
| Anonymous ->
anomaly ~label:"glob_constr_of_pattern" (Pp.str "index to an anonymous variable")
with Not_found -> Id.of_string ("_UNBOUND_REL_"^(string_of_int n)) in
- GVar (loc,id)
- | PMeta None -> GHole (loc,Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None)
- | PMeta (Some n) -> GPatVar (loc,(false,n))
- | PProj (p,c) -> GApp (loc,GRef (loc, ConstRef (Projection.constant p),None),
+ GVar id
+ | PMeta None -> GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None)
+ | PMeta (Some n) -> GPatVar (false,n)
+ | PProj (p,c) -> GApp (CAst.make @@ GRef (ConstRef (Projection.constant p),None),
[glob_of_pat env sigma c])
| PApp (f,args) ->
- GApp (loc,glob_of_pat env sigma f,Array.map_to_list (glob_of_pat env sigma) args)
+ GApp (glob_of_pat env sigma f,Array.map_to_list (glob_of_pat env sigma) args)
| PSoApp (n,args) ->
- GApp (loc,GPatVar (loc,(true,n)),
+ GApp (CAst.make @@ GPatVar (true,n),
List.map (glob_of_pat env sigma) args)
| PProd (na,t,c) ->
- GProd (loc,na,Explicit,glob_of_pat env sigma t,glob_of_pat (na::env) sigma c)
+ GProd (na,Explicit,glob_of_pat env sigma t,glob_of_pat (na::env) sigma c)
| PLetIn (na,b,t,c) ->
- GLetIn (loc,na,glob_of_pat env sigma b, Option.map (glob_of_pat env sigma) t,
+ GLetIn (na,glob_of_pat env sigma b, Option.map (glob_of_pat env sigma) t,
glob_of_pat (na::env) sigma c)
| PLambda (na,t,c) ->
- GLambda (loc,na,Explicit,glob_of_pat env sigma t, glob_of_pat (na::env) sigma c)
+ GLambda (na,Explicit,glob_of_pat env sigma t, glob_of_pat (na::env) sigma c)
| PIf (c,b1,b2) ->
- GIf (loc, glob_of_pat env sigma c, (Anonymous,None),
+ GIf (glob_of_pat env sigma c, (Anonymous,None),
glob_of_pat env sigma b1, glob_of_pat env sigma b2)
| PCase ({cip_style=LetStyle; cip_ind_tags=None},PMeta None,tm,[(0,n,b)]) ->
let nal,b = it_destRLambda_or_LetIn_names n (glob_of_pat env sigma b) in
- GLetTuple (loc,nal,(Anonymous,None),glob_of_pat env sigma tm,b)
+ GLetTuple (nal,(Anonymous,None),glob_of_pat env sigma tm,b)
| PCase (info,p,tm,bl) ->
let mat = match bl, info.cip_ind with
| [], _ -> []
@@ -1065,10 +1074,10 @@ let rec glob_of_pat env sigma = function
return_type_of_predicate ind nargs (glob_of_pat env sigma p)
| _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive")
in
- GCases (loc,RegularStyle,rtn,[glob_of_pat env sigma tm,indnames],mat)
- | PFix f -> Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkFix f)) (** FIXME bad env *)
- | PCoFix c -> Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkCoFix c))
- | PSort s -> GSort (loc,s)
+ GCases (RegularStyle,rtn,[glob_of_pat env sigma tm,indnames],mat)
+ | PFix f -> (Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkFix f))).v (** FIXME bad env *)
+ | PCoFix c -> (Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkCoFix c))).v
+ | PSort s -> GSort s
let extern_constr_pattern env sigma pat =
extern true (None,[]) Id.Set.empty (glob_of_pat env sigma pat)
@@ -1078,5 +1087,5 @@ let extern_rel_context where env sigma sign =
let where = Option.map EConstr.of_constr where in
let a = detype_rel_context where [] (names_of_rel_context env,env) sigma sign in
let vars = vars_of_env env in
- let a = List.map (extended_glob_local_binder_of_decl Loc.ghost) a in
+ let a = List.map (extended_glob_local_binder_of_decl) a in
pi3 (extern_local_binder (None,[]) vars a)
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index b39339450..ea627cff1 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -37,7 +37,7 @@ val extern_closed_glob : ?lax:bool -> bool -> env -> Evd.evar_map -> closed_glob
val extern_constr : ?lax:bool -> bool -> env -> Evd.evar_map -> constr -> constr_expr
val extern_constr_in_scope : bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr
-val extern_reference : Loc.t -> Id.Set.t -> global_reference -> reference
+val extern_reference : ?loc:Loc.t -> Id.Set.t -> global_reference -> reference
val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr
val extern_sort : Evd.evar_map -> sorts -> glob_sort
val extern_rel_context : constr option -> env -> Evd.evar_map ->
@@ -55,9 +55,9 @@ val print_projections : bool ref
(** Customization of the global_reference printer *)
val set_extern_reference :
- (Loc.t -> Id.Set.t -> global_reference -> reference) -> unit
+ (?loc:Loc.t -> Id.Set.t -> global_reference -> reference) -> unit
val get_extern_reference :
- unit -> (Loc.t -> Id.Set.t -> global_reference -> reference)
+ unit -> (?loc:Loc.t -> Id.Set.t -> global_reference -> reference)
(** This governs printing of implicit arguments. If [with_implicits] is
on and not [with_arguments] then implicit args are printed prefixed
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 2426366c6..3b3dccc99 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -15,6 +15,7 @@ open Namegen
open Libnames
open Globnames
open Impargs
+open CAst
open Glob_term
open Glob_ops
open Patternops
@@ -118,7 +119,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' ++
@@ -217,7 +218,7 @@ let contract_notation ntn (l,ll,bll) =
let ntn' = ref ntn in
let rec contract_squash n = function
| [] -> []
- | CNotation (_,"{ _ }",([a],[],[])) :: l ->
+ | { CAst.v = CNotation ("{ _ }",([a],[],[])) } :: l ->
ntn' := expand_notation_string !ntn' n;
contract_squash n (a::l)
| a :: l ->
@@ -230,7 +231,7 @@ let contract_pat_notation ntn (l,ll) =
let ntn' = ref ntn in
let rec contract_squash n = function
| [] -> []
- | CPatNotation (_,"{ _ }",([a],[]),[]) :: l ->
+ | { CAst.v = CPatNotation ("{ _ }",([a],[]),[]) } :: l ->
ntn' := expand_notation_string !ntn' n;
contract_squash n (a::l)
| a :: l ->
@@ -271,7 +272,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 +283,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 +303,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 (GProd (Loc.merge loc1 loc2, na, bk, t, body))
+ (loc2, (na, bk, t)) :: tl -> it_mkGProd ?loc:loc2 tl (CAst.make ?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 (GLambda (Loc.merge loc1 loc2, na, bk, t, body))
+ (loc2, (na, bk, t)) :: tl -> it_mkGLambda ?loc:loc2 tl (CAst.make ?loc:(Loc.merge_opt loc loc2) @@ GLambda (na, bk, t, body))
| [] -> body
(**********************************************************************)
@@ -322,14 +323,14 @@ let build_impls = function
let impls_type_list ?(args = []) =
let rec aux acc = function
- |GProd (_,na,bk,_,c) -> aux ((build_impls bk na)::acc) c
- |_ -> (Variable,[],List.append args (List.rev acc),[])
+ | { v = GProd (na,bk,_,c) } -> aux ((build_impls bk na)::acc) c
+ | _ -> (Variable,[],List.append args (List.rev acc),[])
in aux []
let impls_term_list ?(args = []) =
let rec aux acc = function
- |GLambda (_,na,bk,_,c) -> aux ((build_impls bk na)::acc) c
- |GRec (_, fix_kind, nas, args, tys, bds) ->
+ | { v = GLambda (na,bk,_,c) } -> aux ((build_impls bk na)::acc) c
+ | { v = GRec (fix_kind, nas, args, tys, bds) } ->
let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in
let acc' = List.fold_left (fun a (na, bk, _, _) -> (build_impls bk na)::a) acc args.(nb) in
aux acc' bds.(nb)
@@ -345,13 +346,13 @@ let rec check_capture ty = function
| [] ->
()
-let locate_if_hole loc na = function
- | GHole (_,_,naming,arg) ->
+let locate_if_hole ?loc na = function
+ | { v = GHole (_,naming,arg) } ->
(try match na with
- | Name id -> glob_constr_of_notation_constr loc
+ | Name id -> glob_constr_of_notation_constr ?loc
(Reserve.find_reserved_type id)
| Anonymous -> raise Not_found
- with Not_found -> GHole (loc, Evar_kinds.BinderType na, naming, arg))
+ with Not_found -> CAst.make ?loc @@ GHole (Evar_kinds.BinderType na, naming, arg))
| x -> x
let reset_hidden_inductive_implicit_test env =
@@ -371,15 +372,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 +394,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, GHole (loc, Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None))))
+ (fun (loc, id) ->
+ (loc, (Name id, b, CAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None))))
fvs
in
let na = match na with
@@ -407,7 +408,7 @@ let intern_generalized_binder ?(global_level=false) intern_type lvar
let name =
let id =
match ty with
- | CApp (_, (_, CRef (Ident (loc,id),_)), _) -> id
+ | { CAst.v = CApp ((_, { CAst.v = CRef (Ident (loc,id),_) } ), _) } -> id
| _ -> default_non_dependent_ident
in Implicit_quantifiers.make_fresh ids' (Global.env ()) id
in Name name
@@ -424,44 +425,45 @@ 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
env, b
-let glob_local_binder_of_extended = function
- | GLocalAssum (loc,na,bk,t) -> (na,bk,None,t)
- | GLocalDef (loc,na,bk,c,Some t) -> (na,bk,Some c,t)
- | GLocalDef (loc,na,bk,c,None) ->
- let t = GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) in
+let glob_local_binder_of_extended = CAst.with_loc_val (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 = CAst.make ?loc @@ GHole(Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) in
(na,bk,Some c,t)
- | GLocalPattern (loc,_,_,_,_) ->
- Loc.raise ~loc (Stream.Error "pattern with quote not allowed here.")
+ | GLocalPattern (_,_,_,_) ->
+ Loc.raise ?loc (Stream.Error "pattern with quote not allowed here.")
+ )
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)) -> GLocalAssum (loc,na,c,t)) bl' in
+ let bl' = List.map (fun (loc,(na,c,t)) -> CAst.make ?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,
- GLocalDef (loc,na,Explicit,term,ty) :: bl)
- | CLocalPattern (loc,p,ty) ->
+ (CAst.make ?loc @@ GLocalDef (na,Explicit,term,ty)) :: bl)
+ | CLocalPattern (loc,(p,ty)) ->
let tyc =
match ty with
| Some ty -> ty
- | None -> CHole(loc,None,Misctypes.IntroAnonymous,None)
+ | None -> CAst.make ?loc @@ CHole(None,Misctypes.IntroAnonymous,None)
in
let il,cp =
match !intern_cases_pattern_fwd (None,env.scopes) p with
| (il, [(subst,cp)]) ->
if not (Id.Map.equal Id.equal subst Id.Map.empty) then
- user_err ~loc (str "Unsupported nested \"as\" clause.");
+ user_err ?loc (str "Unsupported nested \"as\" clause.");
il,cp
| _ -> assert false
in
@@ -472,7 +474,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, GLocalPattern(loc,(cp,il),id,bk,t) :: bl)
+ (env, (CAst.make ?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
@@ -494,13 +496,15 @@ let intern_generalization intern env lvar loc bk ak c =
| None -> false
in
if pi then
- (fun (id, loc') acc ->
- GProd (Loc.merge loc' loc, Name id, bk, GHole (loc', Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
+ (fun (loc', id) acc ->
+ CAst.make ?loc:(Loc.merge_opt loc' loc) @@
+ GProd (Name id, bk, CAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
else
- (fun (id, loc') acc ->
- GLambda (Loc.merge loc' loc, Name id, bk, GHole (loc', Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc))
+ (fun (loc', id) acc ->
+ CAst.make ?loc:(Loc.merge_opt loc' loc) @@
+ GLambda (Name id, bk, CAst.make ?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'
@@ -541,48 +545,51 @@ 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
+(* Unused thus fatal warning *)
+(* 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)) ->
- GLetIn(loc,na,b,t,c)
- | LPCases (loc,(cp,il),id) ->
- let tt = (GVar(loc,id),(Name id,None)) in
- GCases(loc,Misctypes.LetPatternStyle,None,[tt],[(loc,il,[cp],c)]))
+ | loc, LPLetIn (na,b,t) ->
+ CAst.make ?loc @@ GLetIn(na,b,t,c)
+ | loc, LPCases ((cp,il),id) ->
+ let tt = (CAst.make ?loc @@ GVar id, (Name id,None)) in
+ CAst.make ?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 *)
- | GLocalDef (loc,na,_,b,t)::l ->
- subordinate_letins (LPLetIn (loc,(na,b,t))::letins) l
- | GLocalAssum (loc,na,bk,t)::l ->
+ | { loc; v = GLocalDef (na,_,b,t) }::l ->
+ subordinate_letins ((Loc.tag ?loc @@ LPLetIn (na,b,t))::letins) l
+ | { loc; v = GLocalAssum (na,bk,t)}::l ->
let letins',rest = subordinate_letins [] l in
letins',((loc,(na,bk,t)),letins)::rest
- | GLocalPattern (loc,u,id,bk,t) :: l ->
- subordinate_letins (LPCases (loc,u,id)::letins) ([GLocalAssum (loc,Name id,bk,t)] @ l)
+ | { loc; v = GLocalPattern (u,id,bk,t)} :: l ->
+ subordinate_letins ((Loc.tag ?loc @@ LPCases (u,id))::letins)
+ ([CAst.make ?loc @@ GLocalAssum (Name id,bk,t)] @ l)
| [] ->
letins,[]
let terms_of_binders bl =
- let rec term_of_pat = function
- | PatVar (loc,Name id) -> CRef (Ident (loc,id), None)
- | PatVar (loc,Anonymous) -> error "Cannot turn \"_\" into a term."
- | PatCstr (loc,c,l,_) ->
+ let rec term_of_pat pt = CAst.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 = CHole (loc,None,Misctypes.IntroAnonymous,None) in
+ let hole = CAst.make ?loc @@ CHole (None,Misctypes.IntroAnonymous,None) in
let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in
- CAppExpl (loc,(None,r,None),params @ List.map term_of_pat l) in
+ CAppExpl ((None,r,None),params @ List.map term_of_pat l)) pt in
let rec extract_variables = function
- | GLocalAssum (loc,Name id,_,_)::l -> CRef (Ident (loc,id), None) :: extract_variables l
- | GLocalDef (loc,Name id,_,_,_)::l -> extract_variables l
- | GLocalDef (loc,Anonymous,_,_,_)::l
- | GLocalAssum (loc,Anonymous,_,_)::l -> error "Cannot turn \"_\" into a term."
- | GLocalPattern (loc,(u,_),_,_,_) :: l -> term_of_pat u :: extract_variables l
+ | {loc; v = GLocalAssum (Name id,_,_)}::l -> (CAst.make ?loc @@ CRef (Ident (loc,id), None)) :: extract_variables l
+ | {loc; v = GLocalDef (Name id,_,_,_)}::l -> extract_variables l
+ | {loc; v = GLocalDef (Anonymous,_,_,_)}::l
+ | {loc; v = GLocalAssum (Anonymous,_,_)}::l -> error "Cannot turn \"_\" into a term."
+ | {loc; v = GLocalPattern ((u,_),_,_,_)}::l -> term_of_pat u :: extract_variables l
| [] -> [] in
extract_variables bl
@@ -638,7 +645,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
- GHole (loc, knd, naming, arg)
+ CAst.make ?loc @@ GHole (knd, naming, arg)
| NBinderList (x,y,iter,terminator) ->
(try
(* All elements of the list are in scopes (scopt,subscopes) *)
@@ -656,24 +663,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
- GProd (loc,na,bk,t,e)
+ CAst.make ?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
- GLambda (loc,na,bk,t,make_letins letins (aux subst' infos c'))
+ CAst.make ?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 = GHole (loc,Evar_kinds.BinderType na,naming,arg) in
- GProd (loc,na,Explicit,ty,aux subst' subinfos c')
+ let ty = CAst.make ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in
+ CAst.make ?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 = GHole (loc,Evar_kinds.BinderType na,naming,arg) in
- GLambda (loc,na,Explicit,ty,aux subst' subinfos c')
+ let ty = CAst.make ?loc @@ GHole (Evar_kinds.BinderType na,naming,arg) in
+ CAst.make ?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 *)
@@ -683,11 +690,12 @@ let instantiate_notation_constr loc intern ntnvars subst infos c =
intern {env with tmp_scope = scopt;
scopes = subscopes @ env.scopes} a
with Not_found ->
+ CAst.make ?loc (
try
- GVar (loc, Id.Map.find id renaming)
+ GVar (Id.Map.find id renaming)
with Not_found ->
(* Happens for local notation joint with inductive/fixpoint defs *)
- GVar (loc,id)
+ GVar id)
in aux (terms,None,None) infos c
let split_by_type ids =
@@ -703,8 +711,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
@@ -722,9 +730,9 @@ let string_of_ty = function
| Variable -> "var"
let gvar (loc, id) us = match us with
-| None -> GVar (loc, id)
+| None -> CAst.make ?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 =
@@ -732,9 +740,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 -> CRef (Ident (loc,id),None), Some (loc,ExplByName id)) expl_impls in
+ (fun id -> CAst.make ?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 *)
@@ -744,15 +752,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 *)
@@ -763,29 +771,29 @@ 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";
- GRef (loc, ref, us), impls, scopes, []
+ Dumpglob.dump_reference ?loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var";
+ CAst.make ?loc @@ GRef (ref, us), impls, scopes, []
with e when CErrors.noncritical e ->
(* [id] a goal variable *)
gvar (loc,id) us, [], [], []
let find_appl_head_data c =
- match c with
- | GRef (loc,ref,_) as x ->
+ match c.v with
+ | GRef (ref,_) ->
let impls = implicits_of_global ref in
let scopes = find_arguments_scope ref in
- x, impls, scopes, []
- | GApp (_,GRef (_,ref,_),l) as x
+ c, impls, scopes, []
+ | GApp ({ v = GRef (ref,_) },l)
when l != [] && Flags.version_strictly_greater Flags.V8_2 ->
let n = List.length l in
let impls = implicits_of_global ref in
let scopes = find_arguments_scope ref in
- x, List.map (drop_first_implicits n) impls,
+ c, List.map (drop_first_implicits n) impls,
List.skipn_at_least n scopes,[]
- | x -> x,[],[],[]
+ | _ -> c,[],[],[]
-let error_not_enough_arguments loc =
- user_err ~loc (str "Abbreviation is not applied enough.")
+let error_not_enough_arguments ?loc =
+ user_err ?loc (str "Abbreviation is not applied enough.")
let check_no_explicitation l =
let is_unset (a, b) = match b with None -> false | Some _ -> true in
@@ -794,11 +802,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
@@ -807,18 +815,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 -> GRef (loc, ref, us), true, args
+ | TrueGlobal ref -> (CAst.make ?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
@@ -828,11 +836,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 _, GRef (loc, ref, None) -> GRef (loc, ref, us)
- | Some _, GApp (loc, GRef (loc', ref, None), arg) ->
- GApp (loc, GRef (loc', ref, us), arg)
+ | Some _, { loc; v = GRef (ref, None) } -> CAst.make ?loc @@ GRef (ref, us)
+ | Some _, { loc; v = GApp ({ loc = loc' ; v = GRef (ref, None) }, arg) } ->
+ CAst.make ?loc @@ GApp (CAst.make ?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,"
++ str " its expanded head does not start with a reference")
in
@@ -841,14 +849,14 @@ let intern_qualid loc qid intern env lvar us args =
(* Rule out section vars since these should have been found by intern_var *)
let intern_non_secvar_qualid loc qid intern env lvar us args =
match intern_qualid loc qid intern env lvar us args with
- | GRef (_, VarRef _, _),_,_ -> raise Not_found
+ | { v = GRef (VarRef _, _) },_,_ -> raise Not_found
| r -> r
let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args = function
| 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
@@ -864,11 +872,11 @@ 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,_,_,_),_ =
- intern_applied_reference (fun _ -> error_not_enough_arguments Loc.ghost)
+ intern_applied_reference (fun _ -> error_not_enough_arguments ?loc:None)
{ids = Id.Set.empty; unb = false ;
tmp_scope = None; scopes = []; impls = empty_internalization_env} []
(vars, Id.Map.empty) None [] r
@@ -878,19 +886,14 @@ let interp_reference vars r =
(** {5 Cases } *)
(** Private internalization patterns *)
-type raw_cases_pattern_expr =
- | RCPatAlias of Loc.t * raw_cases_pattern_expr * Id.t
- | RCPatCstr of Loc.t * Globnames.global_reference
+type raw_cases_pattern_expr_r =
+ | RCPatAlias of raw_cases_pattern_expr * Id.t
+ | RCPatCstr of Globnames.global_reference
* raw_cases_pattern_expr list * raw_cases_pattern_expr list
(** [RCPatCstr (loc, c, l1, l2)] represents ((@c l1) l2) *)
- | RCPatAtom of Loc.t * Id.t option
- | RCPatOr of Loc.t * raw_cases_pattern_expr list
-
-let raw_cases_pattern_expr_loc = function
- | RCPatAlias (loc,_,_) -> loc
- | RCPatCstr (loc,_,_,_) -> loc
- | RCPatAtom (loc,_) -> loc
- | RCPatOr (loc,_) -> loc
+ | RCPatAtom of Id.t option
+ | RCPatOr of raw_cases_pattern_expr list
+and raw_cases_pattern_expr = raw_cases_pattern_expr_r CAst.t
(** {6 Elementary bricks } *)
let apply_scope_env env = function
@@ -930,7 +933,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
@@ -946,7 +949,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.
@@ -955,7 +958,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 =
@@ -969,10 +972,10 @@ let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2
else Int.equal args_len nargs_with_letin || (fst (fail (nargs - List.length impl_list + i))))
,l)
|imp::q as il,[] -> if is_status_implicit imp && maximal_insertion_of imp
- then let (b,out) = aux i (q,[]) in (b,RCPatAtom(Loc.ghost,None)::out)
+ then let (b,out) = aux i (q,[]) in (b,(CAst.make @@ RCPatAtom None)::out)
else fail (remaining_args (len_pl1+i) il)
|imp::q,(hh::tt as l) -> if is_status_implicit imp
- then let (b,out) = aux i (q,l) in (b,RCPatAtom(Loc.ghost,None)::out)
+ then let (b,out) = aux i (q,l) in (b,(CAst.make @@ RCPatAtom(None))::out)
else let (b,out) = aux (succ i) (q,tt) in (b,hh::out)
in aux 0 (impl_list,pl2)
@@ -980,14 +983,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*)
@@ -997,8 +1000,8 @@ let chop_params_pattern loc ind args with_letin =
else Inductiveops.inductive_nparams ind in
assert (nparams <= List.length args);
let params,args = List.chop nparams args in
- List.iter (function PatVar(_,Anonymous) -> ()
- | PatVar (loc',_) | PatCstr(loc',_,_,_) -> error_parameter_not_implicit ~loc:loc') params;
+ List.iter (function { v = PatVar Anonymous } -> ()
+ | { loc; v = PatVar _ } | { loc; v = PatCstr(_,_,_) } -> error_parameter_not_implicit ?loc) params;
args
let find_constructor loc add_params ref =
@@ -1006,10 +1009,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 ->
@@ -1018,7 +1021,7 @@ let find_constructor loc add_params ref =
then Inductiveops.inductive_nparamdecls ind
else Inductiveops.inductive_nparams ind
in
- List.make nb ([], [(Id.Map.empty, PatVar(Loc.ghost,Anonymous))])
+ List.make nb ([], [(Id.Map.empty, CAst.make @@ PatVar Anonymous)])
| None -> []
let find_pattern_variable = function
@@ -1031,7 +1034,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
@@ -1056,7 +1059,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 *)
@@ -1087,7 +1090,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
@@ -1100,7 +1103,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
@@ -1114,13 +1117,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)
@@ -1186,14 +1189,14 @@ let product_of_cases_patterns aliases idspl =
List.map (fun (subst',ptail) -> (merge_subst subst subst',p::ptail)) ptaill) pl)))
idspl (aliases.alias_ids,[aliases.alias_map,[]])
-let rec subst_pat_iterator y t p = match p with
- | RCPatAtom (_,id) ->
- begin match id with Some x when Id.equal x y -> t | _ -> p end
- | RCPatCstr (loc,id,l1,l2) ->
- RCPatCstr (loc,id,List.map (subst_pat_iterator y t) l1,
+let rec subst_pat_iterator y t = CAst.(map (function
+ | RCPatAtom id as p ->
+ begin match id with Some x when Id.equal x y -> t.v | _ -> p end
+ | RCPatCstr (id,l1,l2) ->
+ RCPatCstr (id,List.map (subst_pat_iterator y t) l1,
List.map (subst_pat_iterator y t) l2)
- | RCPatAlias (l,p,a) -> RCPatAlias (l,subst_pat_iterator y t p,a)
- | RCPatOr (l,pl) -> RCPatOr (l,List.map (subst_pat_iterator y t) pl)
+ | RCPatAlias (p,a) -> RCPatAlias (subst_pat_iterator y t p,a)
+ | RCPatOr pl -> 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
@@ -1203,18 +1206,18 @@ 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
in
(** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
- let rec rcp_of_glob = function
- | GVar (loc,id) -> RCPatAtom (loc,Some id)
- | GHole (loc,_,_,_) -> RCPatAtom (loc,None)
- | GRef (loc,g,_) -> RCPatCstr (loc, g,[],[])
- | GApp (loc,GRef (_,g,_),l) -> RCPatCstr (loc, g, List.map rcp_of_glob l,[])
- | _ -> CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr ")
+ let rec rcp_of_glob x = CAst.(map (function
+ | GVar id -> RCPatAtom (Some id)
+ | GHole (_,_,_) -> RCPatAtom (None)
+ | GRef (g,_) -> RCPatCstr (g,[],[])
+ | GApp ({ v = GRef (g,_) }, l) -> RCPatCstr (g, List.map rcp_of_glob l,[])
+ | _ -> CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr "))) x
in
let rec drop_syndef top scopes re pats =
let (loc,qid) = qualid_of_reference re in
@@ -1237,7 +1240,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
@@ -1246,73 +1249,75 @@ 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 = function
- | CPatAlias (loc, p, id) -> RCPatAlias (loc, in_pat top scopes p, id)
- | CPatRecord (loc, l) ->
+ and in_pat top scopes pt =
+ let open CAst in
+ let loc = pt.loc in
+ match pt.v with
+ | CPatAlias (p, id) -> CAst.make ?loc @@ RCPatAlias (in_pat top scopes p, id)
+ | CPatRecord l ->
let sorted_fields =
- sort_fields ~complete:false loc l (fun _idx -> (CPatAtom (loc, None))) in
+ sort_fields ~complete:false loc l (fun _idx -> CAst.make ?loc @@ CPatAtom None) in
begin match sorted_fields with
- | None -> RCPatAtom (loc, None)
+ | None -> CAst.make ?loc @@ RCPatAtom None
| Some (n, head, pl) ->
let pl =
if !asymmetric_patterns then pl else
- let pars = List.make n (CPatAtom (loc, None)) in
+ let pars = List.make n (CAst.make ?loc @@ CPatAtom None) in
List.rev_append pars pl in
match drop_syndef top scopes head pl with
- |Some (a,b,c) -> RCPatCstr(loc, a, b, c)
- |None -> raise (InternalizationError (loc,NotAConstructor head))
+ | Some (a,b,c) -> CAst.make ?loc @@ RCPatCstr(a, b, c)
+ | None -> raise (InternalizationError (loc,NotAConstructor head))
end
- | CPatCstr (loc, head, None, pl) ->
+ | CPatCstr (head, None, pl) ->
begin
match drop_syndef top scopes head pl with
- | Some (a,b,c) -> RCPatCstr(loc, a, b, c)
+ | Some (a,b,c) -> CAst.make ?loc @@ RCPatCstr(a, b, c)
| None -> raise (InternalizationError (loc,NotAConstructor head))
end
- | CPatCstr (loc, r, Some expl_pl, pl) ->
+ | CPatCstr (r, Some expl_pl, pl) ->
let g = try locate (snd (qualid_of_reference r))
with Not_found ->
raise (InternalizationError (loc,NotAConstructor r)) in
if expl_pl == [] then
(* Convention: (@r) deactivates all further implicit arguments and scopes *)
- RCPatCstr (loc, g, List.map (in_pat false scopes) pl, [])
+ CAst.make ?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
- RCPatCstr (loc, 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 ->
- let (pat, _df) = Notation.interp_prim_token_cases_pattern_expr loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes in
+ CAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
+ | CPatNotation ("- _",([{ CAst.v = CPatPrim(Numeral p) }],[]),[])
+ when Bigint.is_strictly_pos p ->
+ let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes in
rcp_of_glob pat
- | CPatNotation (_,"( _ )",([a],[]),[]) ->
+ | CPatNotation ("( _ )",([a],[]),[]) ->
in_pat top scopes a
- | CPatNotation (loc, ntn, fullargs,extrargs) ->
+ | 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 (loc, key, e) ->
- in_pat top (None,find_delimiters_scope loc key::snd scopes) e
- | CPatPrim (loc,p) ->
- let (pat, _df) = Notation.interp_prim_token_cases_pattern_expr loc (test_kind false) p scopes in
+ | CPatDelimiters (key, e) ->
+ in_pat top (None,find_delimiters_scope ?loc key::snd scopes) e
+ | CPatPrim p ->
+ let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (test_kind false) p scopes in
rcp_of_glob pat
- | CPatAtom (loc, Some id) ->
+ | CPatAtom Some id ->
begin
match drop_syndef top scopes id [] with
- |Some (a,b,c) -> RCPatCstr (loc, a, b, c)
- |None -> RCPatAtom (loc, Some (find_pattern_variable id))
+ | Some (a,b,c) -> CAst.make ?loc @@ RCPatCstr (a, b, c)
+ | None -> CAst.make ?loc @@ RCPatAtom (Some (find_pattern_variable id))
end
- | CPatAtom (loc,None) -> RCPatAtom (loc,None)
- | CPatOr (loc, pl) ->
- RCPatOr (loc,List.map (in_pat top scopes) pl)
- | CPatCast (loc,_,_) ->
+ | CPatAtom None -> CAst.make ?loc @@ RCPatAtom None
+ | CPatOr pl -> CAst.make ?loc @@ RCPatOr (List.map (in_pat top scopes) pl)
+ | CPatCast (_,_) ->
(* We raise an error if the pattern contains a cast, due to
current restrictions on casts in patterns. Cast in patterns
are supportted only in local binders and only at top
@@ -1325,7 +1330,7 @@ let drop_notations_pattern looked_for =
lambdas in the encoding of match in constr. This check is
here and not in the parser because it would require
duplicating the levels of the [pattern] rule. *)
- CErrors.user_err ~loc ~hdr:"drop_notations_pattern"
+ CErrors.user_err ?loc ~hdr:"drop_notations_pattern"
(Pp.strbrk "Casts are not supported in this pattern.")
and in_pat_sc scopes x = in_pat false (x,snd scopes)
and in_not top loc scopes (subst,substlist as fullsubst) args = function
@@ -1338,21 +1343,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 RCPatAtom (loc,Some id) else
+ if Id.equal id ldots_var then CAst.make ?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
- RCPatCstr (loc, g, [], List.map2 (in_pat_sc scopes) argscs args)
+ CAst.make ?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
- RCPatCstr (loc, g,
+ CAst.make ?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) *)
@@ -1367,8 +1372,8 @@ let drop_notations_pattern looked_for =
anomaly (Pp.str "Inconsistent substitution of recursive notation"))
| NHole _ ->
let () = assert (List.is_empty args) in
- RCPatAtom (loc, None)
- | t -> error_invalid_pattern_notation ~loc ()
+ CAst.make ?loc @@ RCPatAtom None
+ | t -> error_invalid_pattern_notation ?loc ()
in in_pat true
let rec intern_pat genv aliases pat =
@@ -1376,13 +1381,14 @@ 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 (idslpl1@idslpl2) in
let pl' = List.map (fun (asubst,pl) ->
- (asubst, PatCstr (loc,c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in
+ (asubst, CAst.make ?loc @@ PatCstr (c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in
ids',pl' in
- match pat with
- | RCPatAlias (loc, p, id) ->
+ let loc = CAst.(pat.loc) in
+ match CAst.(pat.v) with
+ | RCPatAlias (p, id) ->
let aliases' = merge_aliases aliases id in
intern_pat genv aliases' p
- | RCPatCstr (loc, head, expl_pl, pl) ->
+ | RCPatCstr (head, expl_pl, pl) ->
if !asymmetric_patterns then
let len = if List.is_empty expl_pl then Some (List.length pl) else None in
let c,idslpl1 = find_constructor loc len head in
@@ -1394,13 +1400,13 @@ let rec intern_pat genv aliases pat =
let with_letin, pl2 =
add_implicits_check_constructor_length genv loc c (List.length idslpl1 + List.length expl_pl) pl in
intern_cstr_with_all_args loc c with_letin idslpl1 (expl_pl@pl2)
- | RCPatAtom (loc, Some id) ->
+ | RCPatAtom (Some id) ->
let aliases = merge_aliases aliases id in
- (aliases.alias_ids,[aliases.alias_map, PatVar (loc, alias_of aliases)])
- | RCPatAtom (loc, None) ->
+ (aliases.alias_ids,[aliases.alias_map, CAst.make ?loc @@ PatVar (alias_of aliases)])
+ | RCPatAtom (None) ->
let { alias_ids = ids; alias_map = asubst; } = aliases in
- (ids, [asubst, PatVar (loc, alias_of aliases)])
- | RCPatOr (loc, pl) ->
+ (ids, [asubst, CAst.make ?loc @@ PatVar (alias_of aliases)])
+ | RCPatOr pl ->
assert (not (List.is_empty pl));
let pl' = List.map (intern_pat genv aliases) pl in
let (idsl,pl') = List.split pl' in
@@ -1420,11 +1426,12 @@ 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
- | RCPatCstr (loc, head, expl_pl, pl) ->
- let c = (function IndRef ind -> ind | _ -> error_bad_inductive_type ~loc) head in
+ let loc = no_not.CAst.loc in
+ match no_not.CAst.v with
+ | RCPatCstr (head, expl_pl, pl) ->
+ 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
@@ -1432,8 +1439,8 @@ let intern_ind_pattern genv scopes pat =
(with_letin,
match product_of_cases_patterns empty_alias (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
(**********************************************************************)
(* Utilities for application *)
@@ -1454,8 +1461,8 @@ let get_implicit_name n imps =
Some (Impargs.name_of_implicit (List.nth imps (n-1)))
let set_hole_implicit i b = function
- | GRef (loc,r,_) | GApp (_,GRef (loc,r,_),_) -> (loc,Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None)
- | GVar (loc,id) -> (loc,Evar_kinds.ImplicitArg (VarRef id,i,b),Misctypes.IntroAnonymous,None)
+ | {loc; v = GRef (r,_) } | { v = GApp ({loc; v = GRef (r,_)},_) } -> Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None)
+ | {loc; v = 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 =
@@ -1472,10 +1479,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) ->
@@ -1485,11 +1492,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)
@@ -1499,15 +1506,15 @@ let extract_explicit_arg imps args =
(* Main loop *)
let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
- let rec intern env = function
- | CRef (ref,us) as x ->
+ let rec intern env = CAst.with_loc_val (fun ?loc -> function
+ | CRef (ref,us) ->
let (c,imp,subscopes,l),_ =
- intern_applied_reference intern env (Environ.named_context globalenv)
- lvar us [] ref
+ intern_applied_reference intern env (Environ.named_context globalenv)
+ lvar us [] ref
in
- apply_impargs c env imp subscopes l (constr_loc x)
+ apply_impargs c env imp subscopes l loc
- | CFix (loc, (locid,iddef), dl) ->
+ | CFix ((locid,iddef), dl) ->
let lf = List.map (fun ((_, id),_,_,_,_) -> id) dl in
let dl = Array.of_list dl in
let n =
@@ -1521,7 +1528,9 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
let before, after = split_at_annot bl n in
let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in
let ro = f (intern env') in
- let n' = Option.map (fun _ -> List.count (function GLocalAssum _ -> true | _ -> false (* remove let-ins *)) rbefore) n in
+ let n' = Option.map (fun _ -> List.count (function | { v = GLocalAssum _ } -> true
+ | _ -> false (* remove let-ins *))
+ rbefore) n in
n', ro, List.fold_left intern_local_binder (env',rbefore) after
in
let n, ro, (env',rbl) =
@@ -1540,15 +1549,16 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
let (_,bli,tyi,_) = idl_temp.(i) in
let fix_args = (List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli) in
push_name_env ntnvars (impls_type_list ~args:fix_args tyi)
- en (Loc.ghost, Name name)) 0 env' lf in
+ en (Loc.tag @@ Name name)) 0 env' lf in
(a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in
- GRec (loc,GFix
+ CAst.make ?loc @@
+ GRec (GFix
(Array.map (fun (ro,_,_,_) -> ro) idl,n),
Array.of_list lf,
Array.map (fun (_,bl,_,_) -> bl) idl,
Array.map (fun (_,_,ty,_) -> ty) idl,
Array.map (fun (_,_,_,bd) -> bd) idl)
- | CCoFix (loc, (locid,iddef), dl) ->
+ | CCoFix ((locid,iddef), dl) ->
let lf = List.map (fun ((_, id),_,_,_) -> id) dl in
let dl = Array.of_list dl in
let n =
@@ -1566,84 +1576,87 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
let (bli,tyi,_) = idl_tmp.(i) in
let cofix_args = List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli in
push_name_env ntnvars (impls_type_list ~args:cofix_args tyi)
- en (Loc.ghost, Name name)) 0 env' lf in
+ en (Loc.tag @@ Name name)) 0 env' lf in
(b,c,intern {env'' with tmp_scope = None} bd)) dl idl_tmp in
- GRec (loc,GCoFix n,
+ CAst.make ?loc @@
+ GRec (GCoFix n,
Array.of_list lf,
Array.map (fun (bl,_,_) -> bl) idl,
Array.map (fun (_,ty,_) -> ty) idl,
Array.map (fun (_,_,bd) -> bd) idl)
- | CProdN (loc,[],c2) ->
+ | CProdN ([],c2) ->
intern_type env c2
- | CProdN (loc,(nal,bk,ty)::bll,c2) ->
- iterate_prod loc env bk ty (CProdN (loc, bll, c2)) nal
- | CLambdaN (loc,[],c2) ->
+ | CProdN ((nal,bk,ty)::bll,c2) ->
+ iterate_prod ?loc env bk ty (CAst.make ?loc @@ CProdN (bll, c2)) nal
+ | CLambdaN ([],c2) ->
intern env c2
- | CLambdaN (loc,(nal,bk,ty)::bll,c2) ->
- iterate_lam loc (reset_tmp_scope env) bk ty (CLambdaN (loc, bll, c2)) nal
- | CLetIn (loc,na,c1,t,c2) ->
+ | CLambdaN ((nal,bk,ty)::bll,c2) ->
+ iterate_lam loc (reset_tmp_scope env) bk ty (CAst.make ?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
- GLetIn (loc, snd na, inc1, int,
+ CAst.make ?loc @@
+ GLetIn (snd na, inc1, int,
intern (push_name_env ntnvars (impls_term_list inc1) env na) c2)
- | CNotation (loc,"- _",([CPrim (_,Numeral p)],[],[]))
+ | CNotation ("- _",([{ CAst.v = CPrim (Numeral p) }],[],[]))
when Bigint.is_strictly_pos p ->
- intern env (CPrim (loc,Numeral (Bigint.neg p)))
- | CNotation (_,"( _ )",([a],[],[])) -> intern env a
- | CNotation (loc,ntn,args) ->
+ intern env (CAst.make ?loc @@ CPrim (Numeral (Bigint.neg p)))
+ | CNotation ("( _ )",([a],[],[])) -> intern env a
+ | CNotation (ntn,args) ->
intern_notation intern env ntnvars loc ntn args
- | CGeneralization (loc,b,a,c) ->
+ | CGeneralization (b,a,c) ->
intern_generalization intern env ntnvars loc b a c
- | CPrim (loc, p) ->
- fst (Notation.interp_prim_token loc p (env.tmp_scope,env.scopes))
- | CDelimiters (loc, key, e) ->
+ | CPrim p ->
+ 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
- | CAppExpl (loc, (isproj,ref,us), args) ->
+ 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
intern_applied_reference intern env (Environ.named_context globalenv)
lvar us args ref
in
(* Rem: GApp(_,f,[]) stands for @f *)
- GApp (loc, f, intern_args env args_scopes (List.map fst args))
+ CAst.make ?loc @@
+ GApp (f, intern_args env args_scopes (List.map fst args))
- | CApp (loc, (isproj,f), args) ->
+ | CApp ((isproj,f), args) ->
let f,args = match f with
(* Compact notations like "t.(f args') args" *)
- | CApp (_,(Some _,f), args') when not (Option.has_some isproj) ->
+ | { CAst.v = CApp ((Some _,f), args') } when not (Option.has_some isproj) ->
f,args'@args
(* Don't compact "(f args') args" to resolve implicits separately *)
| _ -> f,args in
let (c,impargs,args_scopes,l),args =
- match f with
+ match f.CAst.v with
| CRef (ref,us) ->
intern_applied_reference intern env
(Environ.named_context globalenv) lvar us args ref
- | CNotation (loc,ntn,([],[],[])) ->
+ | CNotation (ntn,([],[],[])) ->
let c = intern_notation intern env ntnvars loc ntn ([],[],[]) in
let x, impl, scopes, l = find_appl_head_data c in
(x,impl,scopes,l), args
- | x -> (intern env f,[],[],[]), args in
- apply_impargs c env impargs args_scopes
+ | _ -> (intern env f,[],[],[]), args in
+ apply_impargs c env impargs args_scopes
(merge_impargs l args) loc
- | CRecord (loc, fs) ->
+ | CRecord fs ->
let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
let fields =
sort_fields ~complete:true loc fs
- (fun _idx -> CHole (loc, Some (Evar_kinds.QuestionMark st),
- Misctypes.IntroAnonymous, None))
+ (fun _idx -> CAst.make ?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 (CHole (loc, None, Misctypes.IntroAnonymous, None)) in
- let app = CAppExpl (loc, (None, constrname,None), List.rev_append pars args) in
+ let pars = List.make n (CAst.make ?loc @@ CHole (None, Misctypes.IntroAnonymous, None)) in
+ let app = CAst.make ?loc @@ CAppExpl ((None, constrname,None), List.rev_append pars args) in
intern env app
end
- | CCases (loc, sty, rtnpo, tms, eqns) ->
+ | CCases (sty, rtnpo, tms, eqns) ->
let as_in_vars = List.fold_left (fun acc (_,na,inb) ->
Option.fold_left (fun acc tt -> Id.Set.union (ids_of_cases_indtype tt) acc)
(Option.fold_left (fun acc (_,y) -> name_fold Id.Set.add y acc) acc na)
@@ -1656,54 +1669,57 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
(tm,ind)::inds, Option.fold_right Id.Set.add extra_id ex_ids, List.rev_append match_td matchs)
tms ([],Id.Set.empty,[]) in
let env' = Id.Set.fold
- (fun var bli -> push_name_env ntnvars (Variable,[],[],[]) bli (Loc.ghost,Name var))
+ (fun var bli -> push_name_env ntnvars (Variable,[],[],[]) bli (Loc.tag @@ Name var))
(Id.Set.union ex_ids as_in_vars) (reset_hidden_inductive_implicit_test env) in
(* PatVars before a real pattern do not need to be matched *)
let stripped_match_from_in =
let rec aux = function
| [] -> []
- | (_,PatVar _) :: q -> aux q
+ | (_, { v = PatVar _}) :: q -> aux q
| l -> l
in aux match_from_in in
let rtnpo = match stripped_match_from_in with
| [] -> Option.map (intern_type env') rtnpo (* Only PatVar in "in" clauses *)
| l ->
(* Build a return predicate by expansion of the patterns of the "in" clause *)
- let thevars,thepats = List.split l in
+ let thevars, thepats = List.split l in
let sub_rtn = (* Some (GSort (Loc.ghost,GType None)) *) None in
- let sub_tms = List.map (fun id -> GVar (Loc.ghost,id),(Name id,None)) thevars (* "match v1,..,vn" *) in
- let main_sub_eqn =
- (Loc.ghost,[],thepats, (* "|p1,..,pn" *)
+ let sub_tms = List.map (fun id -> (CAst.make @@ GVar id),(Name id,None)) thevars (* "match v1,..,vn" *) in
+ let main_sub_eqn = Loc.tag @@
+ ([],thepats, (* "|p1,..,pn" *)
Option.cata (intern_type env')
- (GHole(Loc.ghost,Evar_kinds.CasesType false,Misctypes.IntroAnonymous,None))
+ (CAst.make ?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
- [Loc.ghost,[],List.make (List.length thepats) (PatVar(Loc.ghost,Anonymous)), (* "|_,..,_" *)
- GHole(Loc.ghost,Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None)] (* "=> _" *) in
- Some (GCases(Loc.ghost,Term.RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn))
+ [Loc.tag @@ ([],List.make (List.length thepats) (CAst.make @@ PatVar Anonymous), (* "|_,..,_" *)
+ CAst.make @@ GHole(Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None))] (* "=> _" *) in
+ Some (CAst.make @@ 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
- GCases (loc, sty, rtnpo, tms, List.flatten eqns')
- | CLetTuple (loc, nal, (na,po), b, c) ->
+ CAst.make ?loc @@
+ GCases (sty, rtnpo, tms, List.flatten eqns')
+ | CLetTuple (nal, (na,po), b, c) ->
let env' = reset_tmp_scope env in
(* "in" is None so no match to add *)
let ((b',(na',_)),_,_) = intern_case_item env' Id.Set.empty (b,na,None) in
let p' = Option.map (fun u ->
let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env')
- (Loc.ghost,na') in
+ (Loc.tag na') in
intern_type env'' u) po in
- GLetTuple (loc, List.map snd nal, (na', p'), b',
+ CAst.make ?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 (loc, c, (na,po), b1, b2) ->
+ | CIf (c, (na,po), b1, b2) ->
let env' = reset_tmp_scope env in
let ((c',(na',_)),_,_) = intern_case_item env' Id.Set.empty (c,na,None) in (* no "in" no match to ad too *)
let p' = Option.map (fun p ->
let env'' = push_name_env ntnvars (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env)
- (Loc.ghost,na') in
+ (Loc.tag na') in
intern_type env'' p) po in
- GIf (loc, c', (na', p'), intern env b1, intern env b2)
- | CHole (loc, k, naming, solve) ->
+ CAst.make ?loc @@
+ GIf (c', (na', p'), intern env b1, intern env b2)
+ | CHole (k, naming, solve) ->
let k = match k with
| None ->
let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
@@ -1727,27 +1743,33 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
let (_, glb) = Genintern.generic_intern ist gen in
Some glb
in
- GHole (loc, k, naming, solve)
+ CAst.make ?loc @@
+ GHole (k, naming, solve)
(* Parsing pattern variables *)
- | CPatVar (loc, n) when allow_patvar ->
- GPatVar (loc, (true,n))
- | CEvar (loc, n, []) when allow_patvar ->
- GPatVar (loc, (false,n))
+ | CPatVar n when allow_patvar ->
+ CAst.make ?loc @@
+ GPatVar (true,n)
+ | CEvar (n, []) when allow_patvar ->
+ CAst.make ?loc @@
+ GPatVar (false,n)
(* end *)
(* Parsing existential variables *)
- | CEvar (loc, n, l) ->
- GEvar (loc, n, List.map (on_snd (intern env)) l)
- | CPatVar (loc, _) ->
+ | CEvar (n, l) ->
+ CAst.make ?loc @@
+ GEvar (n, List.map (on_snd (intern env)) l)
+ | CPatVar _ ->
raise (InternalizationError (loc,IllegalMetavariable))
(* end *)
- | CSort (loc, s) ->
- GSort(loc,s)
- | CCast (loc, c1, c2) ->
- GCast (loc,intern env c1, Miscops.map_cast_type (intern_type env) c2)
-
+ | CSort s ->
+ CAst.make ?loc @@
+ GSort s
+ | CCast (c1, c2) ->
+ CAst.make ?loc @@
+ GCast (intern env c1, Miscops.map_cast_type (intern_type env) c2)
+ )
and intern_type env = intern (set_type_scope env)
- and intern_local_binder env bind =
+ and intern_local_binder env bind : intern_env * Glob_term.extended_glob_local_binder list =
intern_local_binder_aux intern ntnvars env bind
(* Expands a multiple pattern into a disjunction of multiple patterns *)
@@ -1766,7 +1788,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
(ids,List.flatten mpl')
(* Expands a pattern-matching clause [lhs => rhs] *)
- and intern_eqn n env (loc,lhs,rhs) =
+ and intern_eqn n env (loc,(lhs,rhs)) =
let eqn_ids,pll = intern_disjunctive_multiple_pattern env loc n lhs in
(* Linearity implies the order in ids is irrelevant *)
check_linearity lhs eqn_ids;
@@ -1774,16 +1796,16 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
List.map (fun (asubst,pl) ->
let rhs = replace_vars_constr_expr asubst rhs in
let rhs' = intern {env with ids = env_ids} rhs in
- (loc,eqn_ids,pl,rhs')) pll
+ (loc,(eqn_ids,pl,rhs'))) pll
and intern_case_item env forbidden_names_for_gen (tm,na,t) =
(* the "match" part *)
let tm' = intern env tm in
(* the "as" part *)
let extra_id,na = match tm', na with
- | GVar (loc,id), None when not (Id.Map.mem id (snd lvar)) -> Some id,(loc,Name id)
- | GRef (loc, VarRef id, _), None -> Some id,(loc,Name id)
- | _, None -> None,(Loc.ghost,Anonymous)
+ | {loc; v = GVar id}, None when not (Id.Map.mem id (snd lvar)) -> Some id,(loc,Name id)
+ | {loc; v = GRef (VarRef id, _)}, None -> Some id,(loc,Name id)
+ | _, None -> None,(Loc.tag Anonymous)
| _, Some (loc,na) -> None,(loc,na) in
(* the "in" part *)
let match_td,typ = match t with
@@ -1801,14 +1823,14 @@ 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,PatVar(loc,x)) :: l in
+ | loc,(Name y as x) -> (y, CAst.make ?loc @@ PatVar x) :: l in
match case_rel_ctxt,arg_pats with
(* LetIn in the rel_context *)
| LocalDef _ :: t, l when not with_letin ->
- canonize_args t l forbidden_names match_acc ((Loc.ghost,Anonymous)::var_acc)
+ canonize_args t l forbidden_names match_acc ((Loc.tag Anonymous)::var_acc)
| [],[] ->
(add_name match_acc na, var_acc)
- | _::t,PatVar (loc,x)::tt ->
+ | _::t, { loc; v = PatVar x}::tt ->
canonize_args t tt forbidden_names
(add_name match_acc (loc,x)) ((loc,x)::var_acc)
| (LocalAssum (cano_name,ty) | LocalDef (cano_name,_,ty)) :: t, c::tt ->
@@ -1820,18 +1842,18 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
let _,args_rel =
List.chop nparams (List.rev mip.Declarations.mind_arity_ctxt) in
canonize_args args_rel l (Id.Set.elements forbidden_names_for_gen) [] [] in
- match_to_do, Some (cases_pattern_expr_loc t,ind,List.rev_map snd nal)
+ match_to_do, Some (cases_pattern_expr_loc t,(ind,List.rev_map snd nal))
| None ->
[], 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
@@ -1854,15 +1876,16 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
(* with implicit arguments if maximal insertion is set *)
[]
else
- GHole (set_hole_implicit (n,get_implicit_name n l) (force_inference_of imp) c) ::
- aux (n+1) impl' subscopes' eargs rargs
+ (CAst.map_from_loc (fun ?loc (a,b,c) -> GHole(a,b,c))
+ (set_hole_implicit (n,get_implicit_name n l) (force_inference_of imp) c)
+ ) :: aux (n+1) impl' subscopes' eargs rargs
end
| (imp::impl', a::rargs') ->
intern enva a :: aux (n+1) impl' subscopes' eargs rargs'
| (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"."));
[]
@@ -1871,17 +1894,18 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
intern_args env subscopes rargs
in aux 1 l subscopes eargs rargs
- and apply_impargs c env imp subscopes l loc =
+ and apply_impargs c env imp subscopes l loc =
+ let l : (Constrexpr.constr_expr * Constrexpr.explicitation Loc.located option) list = l in
let imp = select_impargs_size (List.length (List.filter (fun (_,x) -> x == None) l)) imp in
let l = intern_impargs c env imp subscopes l in
smart_gapp c loc l
and smart_gapp f loc = function
| [] -> f
- | l -> match f with
- | GApp (loc', g, args) -> GApp (Loc.merge loc' loc, g, args@l)
- | _ -> GApp (Loc.merge (loc_of_glob_constr f) loc, f, l)
-
+ | l -> match f with
+ | { loc = loc'; v = GApp (g, args) } -> CAst.make ?loc:(Loc.merge_opt loc' loc) @@ GApp (g, args@l)
+ | _ -> CAst.make ?loc:(Loc.merge_opt (loc_of_glob_constr f) loc) @@ GApp (f, l)
+
and intern_args env subscopes = function
| [] -> []
| a::args ->
@@ -1893,7 +1917,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)
(**************************************************************************)
@@ -1933,7 +1957,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)
(*********************************************************************)
@@ -2019,12 +2043,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_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_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'
let my_intern_constr env lvar acc c =
@@ -2041,7 +2065,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
@@ -2049,7 +2073,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_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 19c872b31..cfc6e6c2a 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -28,11 +28,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
@@ -79,7 +79,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 =
@@ -91,11 +91,11 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l =
else ungeneralizable loc id
else l
in
- let rec aux bdvars l c = match c with
+ let rec aux bdvars l c = match CAst.(c.v) with
| CRef (Ident (loc,id),_) -> found loc id bdvars l
- | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id),_) :: _, [], [])) when not (Id.Set.mem id bdvars) ->
+ | CNotation ("{ _ : _ | _ }", ({ CAst.v = CRef (Ident (_, id),_) } :: _, [], [])) when not (Id.Set.mem id bdvars) ->
Topconstr.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add id bdvars) l c
- | c -> Topconstr.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c
+ | _ -> Topconstr.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c
in aux bound l c
let ids_of_names l =
@@ -119,16 +119,16 @@ let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr li
in aux bound l binders
let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.empty) =
- let rec vars bound vs = function
- | GVar (loc,id) ->
+ let rec vars bound vs t = match t with
+ | { loc; CAst.v = 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
| c -> Glob_ops.fold_glob_constr_with_binders Id.Set.add vars bound vs c
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
@@ -151,7 +151,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
@@ -185,31 +185,35 @@ 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 =
fun avoid (_, decl) ->
let id' = next_name_away_from (RelDecl.get_name decl) avoid in
- (CRef (Ident (Loc.ghost, id'),None), Id.Set.add id' avoid)
+ (CAst.make @@ CRef (Ident (Loc.tag id'),None), Id.Set.add id' avoid)
let destClassApp cl =
- match cl with
- | CApp (loc, (None, CRef (ref, inst)), l) -> loc, ref, List.map fst l, inst
- | CAppExpl (loc, (None, ref, inst), l) -> loc, ref, l, inst
- | CRef (ref, inst) -> loc_of_reference ref, ref, [], inst
+ let open CAst in
+ let loc = cl.loc in
+ match cl.v with
+ | CApp ((None, { v = 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 cl =
- match cl with
- | CApp (loc, (None, CRef (ref, inst)), l) -> loc, ref, l, inst
- | CRef (ref, inst) -> loc_of_reference ref, ref, [], inst
+ let open CAst in
+ let loc = cl.loc in
+ match cl.v with
+ | CApp ((None, { v = 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
@@ -217,7 +221,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
@@ -235,7 +239,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
- CAppExpl (loc, (None, id, inst), args), avoid
+ CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid
in c, avoid
let implicits_of_glob_constr ?(with_products=true) l =
@@ -249,12 +253,12 @@ let implicits_of_glob_constr ?(with_products=true) l =
(ExplByPos (i, name), (true, true, true)) :: l
| _ -> l
in
- let rec aux i c =
+ let rec aux i { loc; CAst.v = c } =
let abs na bk b =
add_impl i na bk (aux (succ i) b)
in
match c with
- | GProd (loc, na, bk, t, b) ->
+ | GProd (na, bk, t, b) ->
if with_products then abs na bk b
else
let () = match bk with
@@ -263,9 +267,9 @@ let implicits_of_glob_constr ?(with_products=true) l =
pr_name na ++ strbrk " and following binders")
| _ -> ()
in []
- | GLambda (loc, na, bk, t, b) -> abs na bk b
- | GLetIn (loc, na, b, t, c) -> aux i c
- | GRec (_, fix_kind, nas, args, tys, bds) ->
+ | GLambda (na, bk, t, b) -> abs na bk b
+ | GLetIn (na, b, t, c) -> aux i b
+ | GRec (fix_kind, nas, args, tys, bds) ->
let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in
List.fold_left_i (fun i l (na,bk,_,_) -> add_impl i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb)
| _ -> []
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 d4ade7058..3115c2bcb 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)
@@ -65,17 +65,16 @@ let transl_with_decl env = function
let ctx = Evd.evar_context_universe_context ectx in
WithDef (fqid,(c,ctx))
-let loc_of_module = function
- | CMident (loc,_) | CMapply (loc,_,_) | CMwith (loc,_,_) -> loc
+let loc_of_module l = l.CAst.loc
(* Invariant : the returned kind is never ModAny, and it is
equal to the input kind when this one isn't ModAny. *)
-let rec interp_module_ast env kind = function
+let rec interp_module_ast env kind m = match m.CAst.v with
| CMident qid ->
- let (mp,kind) = lookup_module_or_modtype kind qid in
+ let (mp,kind) = lookup_module_or_modtype kind (m.CAst.loc,qid) in
(MEident mp, kind)
- | CMapply (_,me1,me2) ->
+ | CMapply (me1,me2) ->
let me1',kind1 = interp_module_ast env kind me1 in
let me2',kind2 = interp_module_ast env ModAny me2 in
let mp2 = match me2' with
@@ -85,8 +84,8 @@ let rec interp_module_ast env kind = function
if kind2 == ModType then
error_application_to_module_type (loc_of_module me2);
(MEapply (me1',mp2), kind1)
- | CMwith (loc,me,decl) ->
+ | CMwith (me,decl) ->
let me,kind = interp_module_ast env kind me in
- if kind == Module then error_incorrect_with_in_module loc;
+ if kind == Module then error_incorrect_with_in_module m.CAst.loc;
let decl = transl_with_decl env decl in
(MEwith(me,decl), kind)
diff --git a/interp/notation.ml b/interp/notation.ml
index 7be2fe0f0..d19654b10 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -219,10 +219,10 @@ let remove_delimiters scope =
with Not_found ->
assert false (* A delimiter for scope [scope] should exist *)
-let find_delimiters_scope loc key =
+let find_delimiters_scope ?loc key =
try String.Map.find key !delimiters_map
with Not_found ->
- user_err ~loc ~hdr:"find_delimiters"
+ user_err ?loc ~hdr:"find_delimiters"
(str "Unknown scope delimiting key " ++ str key ++ str ".")
(* Uninterpretation tables *)
@@ -263,16 +263,16 @@ let notations_key_table = ref (KeyMap.empty : notation_rule list KeyMap.t)
let prim_token_key_table = ref KeyMap.empty
let glob_prim_constr_key = function
- | GApp (_,GRef (_,ref,_),_) | GRef (_,ref,_) -> RefKey (canonical_gr ref)
+ | { CAst.v = GApp ({ CAst.v = GRef (ref,_) } ,_) } | { CAst.v = GRef (ref,_) } -> RefKey (canonical_gr ref)
| _ -> Oth
let glob_constr_keys = function
- | GApp (_,GRef (_,ref,_),_) -> [RefKey (canonical_gr ref); Oth]
- | GRef (_,ref,_) -> [RefKey (canonical_gr ref)]
+ | { CAst.v = GApp ({ CAst.v = GRef (ref,_) },_) } -> [RefKey (canonical_gr ref); Oth]
+ | { CAst.v = GRef (ref,_) } -> [RefKey (canonical_gr ref)]
| _ -> [Oth]
let cases_pattern_key = function
- | PatCstr (_,ref,_,_) -> RefKey (canonical_gr (ConstructRef ref))
+ | { CAst.v = PatCstr (ref,_,_) } -> RefKey (canonical_gr (ConstructRef ref))
| _ -> Oth
let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
@@ -290,7 +290,7 @@ let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
type required_module = full_path * string list
type 'a prim_token_interpreter =
- Loc.t -> 'a -> glob_constr
+ ?loc:Loc.t -> 'a -> glob_constr
type cases_pattern_status = bool (* true = use prim token in patterns *)
@@ -298,7 +298,7 @@ type 'a prim_token_uninterpreter =
glob_constr list * (glob_constr -> 'a option) * cases_pattern_status
type internal_prim_token_interpreter =
- Loc.t -> prim_token -> required_module * (unit -> glob_constr)
+ ?loc:Loc.t -> prim_token -> required_module * (unit -> glob_constr)
let prim_token_interpreter_tab =
(Hashtbl.create 7 : (scope_name, internal_prim_token_interpreter) Hashtbl.t)
@@ -308,7 +308,7 @@ let add_prim_token_interpreter sc interp =
let cont = Hashtbl.find prim_token_interpreter_tab sc in
Hashtbl.replace prim_token_interpreter_tab sc (interp cont)
with Not_found ->
- let cont = (fun _loc _p -> raise Not_found) in
+ let cont = (fun ?loc _p -> raise Not_found) in
Hashtbl.add prim_token_interpreter_tab sc (interp cont)
let declare_prim_token_interpreter sc interp (patl,uninterp,b) =
@@ -324,22 +324,22 @@ let mkString = function
| None -> None
| Some s -> if Unicode.is_utf8 s then Some (String s) else None
-let delay dir int loc x = (dir, (fun () -> int loc x))
+let delay dir int ?loc x = (dir, (fun () -> int ?loc x))
let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) =
declare_prim_token_interpreter sc
- (fun cont loc -> function Numeral n-> delay dir interp loc n | p -> cont loc p)
+ (fun cont ?loc -> function Numeral n-> delay dir interp ?loc n | p -> cont ?loc p)
(patl, (fun r -> Option.map mkNumeral (uninterp r)), inpat)
let declare_string_interpreter sc dir interp (patl,uninterp,inpat) =
declare_prim_token_interpreter sc
- (fun cont loc -> function String s -> delay dir interp loc s | p -> cont loc p)
+ (fun cont ?loc -> function String s -> delay dir interp ?loc s | p -> cont ?loc p)
(patl, (fun r -> mkString (uninterp r)), inpat)
-let check_required_module loc sc (sp,d) =
+let check_required_module ?loc sc (sp,d) =
try let _ = Nametab.global_of_path sp in ()
with Not_found ->
- user_err ~loc ~hdr:"prim_token_interpreter"
+ user_err ?loc ~hdr:"prim_token_interpreter"
(str "Cannot interpret in " ++ str sc ++ str " without requiring first module " ++ str (List.last d) ++ str ".")
(* Look if some notation or numeral printer in [scope] can be used in
@@ -444,49 +444,49 @@ let notation_of_prim_token = function
| Numeral n -> "- "^(to_string (neg n))
| String _ -> raise Not_found
-let find_prim_token check_allowed loc p sc =
+let find_prim_token check_allowed ?loc p sc =
(* Try for a user-defined numerical notation *)
try
let (_,c),df = find_notation (notation_of_prim_token p) sc in
- let pat = Notation_ops.glob_constr_of_notation_constr loc c in
+ let pat = Notation_ops.glob_constr_of_notation_constr ?loc c in
check_allowed pat;
pat, df
with Not_found ->
(* Try for a primitive numerical notation *)
- let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc loc p in
- check_required_module loc sc spdir;
+ let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc ?loc p in
+ check_required_module ?loc sc spdir;
let pat = interp () in
check_allowed pat;
pat, ((dirpath (fst spdir),DirPath.empty),"")
-let interp_prim_token_gen g loc p local_scopes =
+let interp_prim_token_gen ?loc g p local_scopes =
let scopes = make_current_scopes local_scopes in
let p_as_ntn = try notation_of_prim_token p with Not_found -> "" in
- try find_interpretation p_as_ntn (find_prim_token g loc p) scopes
+ try find_interpretation p_as_ntn (find_prim_token ?loc g p) scopes
with Not_found ->
- user_err ~loc ~hdr:"interp_prim_token"
+ user_err ?loc ~hdr:"interp_prim_token"
((match p with
| Numeral n -> str "No interpretation for numeral " ++ str (to_string n)
| String s -> str "No interpretation for string " ++ qs s) ++ str ".")
-let interp_prim_token =
- interp_prim_token_gen (fun _ -> ())
+let interp_prim_token ?loc =
+ interp_prim_token_gen ?loc (fun _ -> ())
-let rec check_allowed_ref_in_pat looked_for = function
+let rec check_allowed_ref_in_pat looked_for = CAst.(with_val (function
| GVar _ | GHole _ -> ()
- | GRef (_,g,_) -> looked_for g
- | GApp (loc,GRef (_,g,_),l) ->
+ | GRef (g,_) -> looked_for g
+ | GApp ({ v = GRef (g,_) },l) ->
looked_for g; List.iter (check_allowed_ref_in_pat looked_for) l
- | _ -> raise Not_found
+ | _ -> raise Not_found))
-let interp_prim_token_cases_pattern_expr loc looked_for p =
- interp_prim_token_gen (check_allowed_ref_in_pat looked_for) loc p
+let interp_prim_token_cases_pattern_expr ?loc looked_for p =
+ interp_prim_token_gen ?loc (check_allowed_ref_in_pat looked_for) p
-let interp_notation loc ntn local_scopes =
+let interp_notation ?loc ntn local_scopes =
let scopes = make_current_scopes local_scopes in
try find_interpretation ntn (find_notation ntn) scopes
with Not_found ->
- user_err ~loc
+ user_err ?loc
(str "Unknown interpretation for notation \"" ++ str ntn ++ str "\".")
let uninterp_notations c =
@@ -521,8 +521,8 @@ let uninterp_prim_token_ind_pattern ind args =
if not b then raise Notation_ops.No_match;
let args' = List.map
(fun x -> snd (glob_constr_of_closed_cases_pattern x)) args in
- let ref = GRef (Loc.ghost,ref,None) in
- match numpr (GApp (Loc.ghost,ref,args')) with
+ let ref = CAst.make @@ GRef (ref,None) in
+ match numpr (CAst.make @@ GApp (ref,args')) with
| None -> raise Notation_ops.No_match
| Some n -> (sc,n)
with Not_found -> raise Notation_ops.No_match
@@ -540,7 +540,7 @@ let uninterp_prim_token_cases_pattern c =
let availability_of_prim_token n printer_scope local_scopes =
let f scope =
- try ignore (Hashtbl.find prim_token_interpreter_tab scope Loc.ghost n); true
+ try ignore ((Hashtbl.find prim_token_interpreter_tab scope) n); true
with Not_found -> false in
let scopes = make_current_scopes local_scopes in
Option.map snd (find_without_delimiters f (Some printer_scope,None) scopes)
@@ -822,7 +822,7 @@ let pr_scope_classes sc =
let pr_notation_info prglob ntn c =
str "\"" ++ str ntn ++ str "\" := " ++
- prglob (Notation_ops.glob_constr_of_notation_constr Loc.ghost c)
+ prglob (Notation_ops.glob_constr_of_notation_constr c)
let pr_named_scope prglob scope sc =
(if String.equal scope default_scope then
@@ -890,25 +890,25 @@ let global_reference_of_notation test (ntn,(sc,c,_)) =
Some (ntn,sc,ref)
| _ -> None
-let error_ambiguous_notation loc _ntn =
- user_err ~loc (str "Ambiguous notation.")
+let error_ambiguous_notation ?loc _ntn =
+ user_err ?loc (str "Ambiguous notation.")
-let error_notation_not_reference loc ntn =
- user_err ~loc
+let error_notation_not_reference ?loc ntn =
+ user_err ?loc
(str "Unable to interpret " ++ quote (str ntn) ++
str " as a reference.")
-let interp_notation_as_global_reference loc test ntn sc =
+let interp_notation_as_global_reference ?loc test ntn sc =
let scopes = match sc with
| Some sc ->
- let scope = find_scope (find_delimiters_scope Loc.ghost sc) in
+ let scope = find_scope (find_delimiters_scope sc) in
String.Map.add sc scope String.Map.empty
| None -> !scope_map in
let ntns = browse_notation true ntn scopes in
let refs = List.map (global_reference_of_notation test) ntns in
match Option.List.flatten refs with
| [_,_,ref] -> ref
- | [] -> error_notation_not_reference loc ntn
+ | [] -> error_notation_not_reference ?loc ntn
| refs ->
let f (ntn,sc,ref) =
let def = find_default ntn !scope_stack in
@@ -918,8 +918,8 @@ let interp_notation_as_global_reference loc test ntn sc =
in
match List.filter f refs with
| [_,_,ref] -> ref
- | [] -> error_notation_not_reference loc ntn
- | _ -> error_ambiguous_notation loc ntn
+ | [] -> error_notation_not_reference ?loc ntn
+ | _ -> error_ambiguous_notation ?loc ntn
let locate_notation prglob ntn scope =
let ntns = factorize_entries (browse_notation false ntn !scope_map) in
diff --git a/interp/notation.mli b/interp/notation.mli
index 300480ff1..d271a88fe 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -55,7 +55,7 @@ val find_scope : scope_name -> scope
val declare_delimiters : scope_name -> delimiters -> unit
val remove_delimiters : scope_name -> unit
-val find_delimiters_scope : Loc.t -> delimiters -> scope_name
+val find_delimiters_scope : ?loc:Loc.t -> delimiters -> scope_name
(** {6 Declare and uses back and forth an interpretation of primitive token } *)
@@ -69,7 +69,7 @@ type required_module = full_path * string list
type cases_pattern_status = bool (** true = use prim token in patterns *)
type 'a prim_token_interpreter =
- Loc.t -> 'a -> glob_constr
+ ?loc:Loc.t -> 'a -> glob_constr
type 'a prim_token_uninterpreter =
glob_constr list * (glob_constr -> 'a option) * cases_pattern_status
@@ -83,11 +83,10 @@ val declare_string_interpreter : scope_name -> required_module ->
(** Return the [term]/[cases_pattern] bound to a primitive token in a
given scope context*)
-val interp_prim_token : Loc.t -> prim_token -> local_scopes ->
+val interp_prim_token : ?loc:Loc.t -> prim_token -> local_scopes ->
glob_constr * (notation_location * scope_name option)
-
(* This function returns a glob_const representing a pattern *)
-val interp_prim_token_cases_pattern_expr : Loc.t -> (global_reference -> unit) -> prim_token ->
+val interp_prim_token_cases_pattern_expr : ?loc:Loc.t -> (global_reference -> unit) -> prim_token ->
local_scopes -> glob_constr * (notation_location * scope_name option)
(** Return the primitive token associated to a [term]/[cases_pattern];
@@ -116,7 +115,7 @@ val declare_notation_interpretation : notation -> scope_name option ->
val declare_uninterpretation : interp_rule -> interpretation -> unit
(** Return the interpretation bound to a notation *)
-val interp_notation : Loc.t -> notation -> local_scopes ->
+val interp_notation : ?loc:Loc.t -> notation -> local_scopes ->
interpretation * (notation_location * scope_name option)
type notation_rule = interp_rule * interpretation * int option
@@ -139,7 +138,7 @@ val level_of_notation : notation -> level (** raise [Not_found] if no level *)
(** {6 Miscellaneous} *)
-val interp_notation_as_global_reference : Loc.t -> (global_reference -> bool) ->
+val interp_notation_as_global_reference : ?loc:Loc.t -> (global_reference -> bool) ->
notation -> delimiters option -> global_reference
(** Checks for already existing notations *)
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index d08fb107b..74644b206 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -24,19 +24,19 @@ open Notation_term
let on_true_do b f c = if b then (f c; b) else b
-let compare_glob_constr f add t1 t2 = match t1,t2 with
- | GRef (_,r1,_), GRef (_,r2,_) -> eq_gr r1 r2
- | GVar (_,v1), GVar (_,v2) -> on_true_do (Id.equal v1 v2) add (Name v1)
- | GApp (_,f1,l1), GApp (_,f2,l2) -> f f1 f2 && List.for_all2eq f l1 l2
- | GLambda (_,na1,bk1,ty1,c1), GLambda (_,na2,bk2,ty2,c2)
+let compare_glob_constr f add t1 t2 = match CAst.(t1.v,t2.v) with
+ | GRef (r1,_), GRef (r2,_) -> eq_gr r1 r2
+ | GVar v1, GVar v2 -> on_true_do (Id.equal v1 v2) add (Name v1)
+ | GApp (f1,l1), GApp (f2,l2) -> f f1 f2 && List.for_all2eq f l1 l2
+ | GLambda (na1,bk1,ty1,c1), GLambda (na2,bk2,ty2,c2)
when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
on_true_do (f ty1 ty2 && f c1 c2) add na1
- | GProd (_,na1,bk1,ty1,c1), GProd (_,na2,bk2,ty2,c2)
+ | GProd (na1,bk1,ty1,c1), GProd (na2,bk2,ty2,c2)
when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
on_true_do (f ty1 ty2 && f c1 c2) add na1
| GHole _, GHole _ -> true
- | GSort (_,s1), GSort (_,s2) -> Miscops.glob_sort_eq s1 s2
- | GLetIn (_,na1,b1,t1,c1), GLetIn (_,na2,b2,t2,c2) when Name.equal na1 na2 ->
+ | GSort s1, GSort s2 -> Miscops.glob_sort_eq s1 s2
+ | GLetIn (na1,b1,t1,c1), GLetIn (na2,b2,t2,c2) when Name.equal na1 na2 ->
on_true_do (f b1 b2 && f c1 c2) add na1
| (GCases _ | GRec _
| GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _),_
@@ -117,60 +117,63 @@ let name_to_ident = function
let to_id g e id = let e,na = g e (Name id) in e,name_to_ident na
-let rec cases_pattern_fold_map loc g e = function
- | PatVar (_,na) ->
- let e',na' = g e na in e', PatVar (loc,na')
- | PatCstr (_,cstr,patl,na) ->
+let rec cases_pattern_fold_map ?loc g e = CAst.with_val (function
+ | PatVar na ->
+ let e',na' = g e na in e', CAst.make ?loc @@ PatVar na'
+ | PatCstr (cstr,patl,na) ->
let e',na' = g e na in
- let e',patl' = List.fold_map (cases_pattern_fold_map loc g) e patl in
- e', PatCstr (loc,cstr,patl',na')
+ let e',patl' = List.fold_map (cases_pattern_fold_map ?loc g) e patl in
+ e', CAst.make ?loc @@ PatCstr (cstr,patl',na')
+ )
let subst_binder_type_vars l = function
| Evar_kinds.BinderType (Name id) ->
let id =
- try match Id.List.assoc id l with GVar(_,id') -> id' | _ -> id
+ try match Id.List.assoc id l with { CAst.v = GVar id' } -> id' | _ -> id
with Not_found -> id in
Evar_kinds.BinderType (Name id)
| e -> e
-let rec subst_glob_vars l = function
- | GVar (_,id) as r -> (try Id.List.assoc id l with Not_found -> r)
- | GProd (loc,Name id,bk,t,c) ->
+let rec subst_glob_vars l gc = CAst.map (function
+ | GVar id as r -> (try (Id.List.assoc id l).CAst.v with Not_found -> r)
+ | GProd (Name id,bk,t,c) ->
let id =
- try match Id.List.assoc id l with GVar(_,id') -> id' | _ -> id
+ try match Id.List.assoc id l with { CAst.v = GVar id' } -> id' | _ -> id
with Not_found -> id in
- GProd (loc,Name id,bk,subst_glob_vars l t,subst_glob_vars l c)
- | GLambda (loc,Name id,bk,t,c) ->
+ GProd (Name id,bk,subst_glob_vars l t,subst_glob_vars l c)
+ | GLambda (Name id,bk,t,c) ->
let id =
- try match Id.List.assoc id l with GVar(_,id') -> id' | _ -> id
+ try match Id.List.assoc id l with { CAst.v = GVar id' } -> id' | _ -> id
with Not_found -> id in
- GLambda (loc,Name id,bk,subst_glob_vars l t,subst_glob_vars l c)
- | GHole (loc,x,naming,arg) -> GHole (loc,subst_binder_type_vars l x,naming,arg)
- | r -> map_glob_constr (subst_glob_vars l) r (* assume: id is not binding *)
+ GLambda (Name id,bk,subst_glob_vars l t,subst_glob_vars l c)
+ | GHole (x,naming,arg) -> GHole (subst_binder_type_vars l x,naming,arg)
+ | _ -> (map_glob_constr (subst_glob_vars l) gc).CAst.v (* assume: id is not binding *)
+ ) gc
let ldots_var = Id.of_string ".."
-let glob_constr_of_notation_constr_with_binders loc g f e = function
- | NVar id -> GVar (loc,id)
- | NApp (a,args) -> GApp (loc,f e a, List.map (f e) args)
+let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
+ let lt x = CAst.make ?loc x in lt @@ match nc with
+ | NVar id -> GVar id
+ | NApp (a,args) -> GApp (f e a, List.map (f e) args)
| NList (x,y,iter,tail,swap) ->
let t = f e tail in let it = f e iter in
- let innerl = (ldots_var,t)::(if swap then [] else [x,GVar(loc,y)]) in
- let inner = GApp (loc,GVar (loc,ldots_var),[subst_glob_vars innerl it]) in
- let outerl = (ldots_var,inner)::(if swap then [x,GVar(loc,y)] else []) in
- subst_glob_vars outerl it
+ let innerl = (ldots_var,t)::(if swap then [] else [x, lt @@ GVar y]) in
+ let inner = lt @@ GApp (lt @@ GVar (ldots_var),[subst_glob_vars innerl it]) in
+ let outerl = (ldots_var,inner)::(if swap then [x, lt @@ GVar y] else []) in
+ (subst_glob_vars outerl it).CAst.v
| NBinderList (x,y,iter,tail) ->
let t = f e tail in let it = f e iter in
- let innerl = [(ldots_var,t);(x,GVar(loc,y))] in
- let inner = GApp (loc,GVar (loc,ldots_var),[subst_glob_vars innerl it]) in
+ let innerl = [(ldots_var,t);(x, lt @@ GVar y)] in
+ let inner = lt @@ GApp (lt @@ GVar ldots_var,[subst_glob_vars innerl it]) in
let outerl = [(ldots_var,inner)] in
- subst_glob_vars outerl it
+ (subst_glob_vars outerl it).CAst.v
| NLambda (na,ty,c) ->
- let e',na = g e na in GLambda (loc,na,Explicit,f e ty,f e' c)
+ let e',na = g e na in GLambda (na,Explicit,f e ty,f e' c)
| NProd (na,ty,c) ->
- let e',na = g e na in GProd (loc,na,Explicit,f e ty,f e' c)
+ let e',na = g e na in GProd (na,Explicit,f e ty,f e' c)
| NLetIn (na,b,t,c) ->
- let e',na = g e na in GLetIn (loc,na,f e b,Option.map (f e) t,f e' c)
+ let e',na = g e na in GLetIn (na,f e b,Option.map (f e) t,f e' c)
| NCases (sty,rtntypopt,tml,eqnl) ->
let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
let e',t' = match t with
@@ -178,36 +181,36 @@ let glob_constr_of_notation_constr_with_binders loc g f e = function
| Some (ind,nal) ->
let e',nal' = List.fold_right (fun na (e',nal) ->
let e',na' = g e' na in e',na'::nal) nal (e',[]) in
- e',Some (loc,ind,nal') in
+ e',Some (Loc.tag ?loc (ind,nal')) in
let e',na' = g e' na in
(e',(f e tm,(na',t'))::tml')) tml (e,[]) in
let fold (idl,e) na = let (e,na) = g e na in ((name_cons na idl,e),na) in
let eqnl' = List.map (fun (patl,rhs) ->
let ((idl,e),patl) =
- List.fold_map (cases_pattern_fold_map loc fold) ([],e) patl in
- (loc,idl,patl,f e rhs)) eqnl in
- GCases (loc,sty,Option.map (f e') rtntypopt,tml',eqnl')
+ List.fold_map (cases_pattern_fold_map ?loc fold) ([],e) patl in
+ Loc.tag (idl,patl,f e rhs)) eqnl in
+ GCases (sty,Option.map (f e') rtntypopt,tml',eqnl')
| NLetTuple (nal,(na,po),b,c) ->
let e',nal = List.fold_map g e nal in
let e'',na = g e na in
- GLetTuple (loc,nal,(na,Option.map (f e'') po),f e b,f e' c)
+ GLetTuple (nal,(na,Option.map (f e'') po),f e b,f e' c)
| NIf (c,(na,po),b1,b2) ->
let e',na = g e na in
- GIf (loc,f e c,(na,Option.map (f e') po),f e b1,f e b2)
+ GIf (f e c,(na,Option.map (f e') po),f e b1,f e b2)
| NRec (fk,idl,dll,tl,bl) ->
let e,dll = Array.fold_map (List.fold_map (fun e (na,oc,b) ->
let e,na = g e na in
(e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in
let e',idl = Array.fold_map (to_id g) e idl in
- GRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl)
- | NCast (c,k) -> GCast (loc,f e c,Miscops.map_cast_type (f e) k)
- | NSort x -> GSort (loc,x)
- | NHole (x, naming, arg) -> GHole (loc, x, naming, arg)
- | NRef x -> GRef (loc,x,None)
+ GRec (fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl)
+ | NCast (c,k) -> GCast (f e c,Miscops.map_cast_type (f e) k)
+ | NSort x -> GSort x
+ | NHole (x, naming, arg) -> GHole (x, naming, arg)
+ | NRef x -> GRef (x,None)
-let glob_constr_of_notation_constr loc x =
+let glob_constr_of_notation_constr ?loc x =
let rec aux () x =
- glob_constr_of_notation_constr_with_binders loc (fun () id -> ((),id)) aux () x
+ glob_constr_of_notation_constr_with_binders ?loc (fun () id -> ((),id)) aux () x
in aux () x
(******************************************************************************)
@@ -218,14 +221,15 @@ let add_name r = function Anonymous -> () | Name id -> add_id r id
let split_at_recursive_part c =
let sub = ref None in
+ let open CAst in
let rec aux = function
- | GApp (loc0,GVar(loc,v),c::l) when Id.equal v ldots_var ->
+ | { loc = loc0; v = GApp ({ loc; v = GVar v },c::l) } when Id.equal v ldots_var -> (* *)
begin match !sub with
| None ->
let () = sub := Some c in
begin match l with
- | [] -> GVar (loc, ldots_var)
- | _ :: _ -> GApp (loc0, GVar (loc, ldots_var), l)
+ | [] -> CAst.make ?loc @@ GVar ldots_var
+ | _ :: _ -> CAst.make ?loc:loc0 @@ GApp (CAst.make ?loc @@ GVar ldots_var, l)
end
| Some _ ->
(* Not narrowed enough to find only one recursive part *)
@@ -236,14 +240,17 @@ let split_at_recursive_part c =
match !sub with
| None -> (* No recursive pattern found *) raise Not_found
| Some c ->
- match outer_iterator with
- | GVar (_,v) when Id.equal v ldots_var -> (* Not enough context *) raise Not_found
+ match outer_iterator.v with
+ | 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)
+let check_is_hole id = function { CAst.v = GHole _ } -> () | 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.")
@@ -254,21 +261,22 @@ type recursive_pattern_kind =
| RecursiveBinders of glob_constr * glob_constr
let compare_recursive_parts found f f' (iterator,subc) =
+ let open CAst in
let diff = ref None in
let terminator = ref None in
- let rec aux c1 c2 = match c1,c2 with
- | GVar(_,v), term when Id.equal v ldots_var ->
+ let rec aux c1 c2 = match c1.v, c2.v with
+ | GVar v, term when Id.equal v ldots_var ->
(* We found the pattern *)
assert (match !terminator with None -> true | Some _ -> false);
- terminator := Some term;
+ terminator := Some c2;
true
- | GApp (_,GVar(_,v),l1), GApp (_,term,l2) when Id.equal v ldots_var ->
+ | GApp ({ v = GVar v },l1), GApp (term, l2) when Id.equal v ldots_var ->
(* We found the pattern, but there are extra arguments *)
(* (this allows e.g. alternative (recursive) notation of application) *)
assert (match !terminator with None -> true | Some _ -> false);
terminator := Some term;
List.for_all2eq aux l1 l2
- | GVar (_,x), GVar (_,y) when not (Id.equal x y) ->
+ | GVar x, GVar y when not (Id.equal x y) ->
(* We found the position where it differs *)
let lassoc = match !terminator with None -> false | Some _ -> true in
let x,y = if lassoc then y,x else x,y in
@@ -278,8 +286,8 @@ let compare_recursive_parts found f f' (iterator,subc) =
true
| Some _ -> false
end
- | GLambda (_,Name x,_,t_x,c), GLambda (_,Name y,_,t_y,term)
- | GProd (_,Name x,_,t_x,c), GProd (_,Name y,_,t_y,term) ->
+ | GLambda (Name x,_,t_x,c), GLambda (Name y,_,t_y,term)
+ | GProd (Name x,_,t_x,c), GProd (Name y,_,t_y,term) ->
(* We found a binding position where it differs *)
begin match !diff with
| None ->
@@ -295,7 +303,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 =
@@ -311,13 +319,13 @@ let compare_recursive_parts found f f' (iterator,subc) =
(pi1 !found, (x,y) :: pi2 !found, pi3 !found),x,y,lassoc in
let iterator =
f' (if lassoc then iterator
- else subst_glob_vars [x,GVar(Loc.ghost,y)] iterator) in
+ else subst_glob_vars [x, CAst.make @@ GVar y] iterator) in
(* found have been collected by compare_constr *)
found := newfound;
NList (x,y,iterator,f (Option.get !terminator),lassoc)
| Some (x,y,RecursiveBinders (t_x,t_y)) ->
let newfound = (pi1 !found, pi2 !found, (x,y) :: pi3 !found) in
- let iterator = f' (subst_glob_vars [x,GVar(Loc.ghost,y)] iterator) in
+ let iterator = f' (subst_glob_vars [x, CAst.make @@ GVar y] iterator) in
(* found have been collected by compare_constr *)
found := newfound;
check_is_hole x t_x;
@@ -335,52 +343,52 @@ let notation_constr_and_vars_of_glob_constr a =
try compare_recursive_parts found aux aux' (split_at_recursive_part c)
with Not_found ->
found := keepfound;
- match c with
- | GApp (_,GVar (loc,f),[c]) when Id.equal f ldots_var ->
+ match c.CAst.v with
+ | GApp ({ CAst.v = GVar f; loc},[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 ->
+ | _c ->
aux' c
- and aux' = function
- | GVar (_,id) -> add_id found id; NVar id
- | GApp (_,g,args) -> NApp (aux g, List.map aux args)
- | GLambda (_,na,bk,ty,c) -> add_name found na; NLambda (na,aux ty,aux c)
- | GProd (_,na,bk,ty,c) -> add_name found na; NProd (na,aux ty,aux c)
- | GLetIn (_,na,b,t,c) -> add_name found na; NLetIn (na,aux b,Option.map aux t,aux c)
- | GCases (_,sty,rtntypopt,tml,eqnl) ->
- let f (_,idl,pat,rhs) = List.iter (add_id found) idl; (pat,aux rhs) in
+ and aux' x = CAst.with_val (function
+ | GVar id -> add_id found id; NVar id
+ | GApp (g,args) -> NApp (aux g, List.map aux args)
+ | GLambda (na,bk,ty,c) -> add_name found na; NLambda (na,aux ty,aux c)
+ | GProd (na,bk,ty,c) -> add_name found na; NProd (na,aux ty,aux c)
+ | GLetIn (na,b,t,c) -> add_name found na; NLetIn (na,aux b,Option.map aux t, aux c)
+ | GCases (sty,rtntypopt,tml,eqnl) ->
+ let f (_,(idl,pat,rhs)) = List.iter (add_id found) idl; (pat,aux rhs) in
NCases (sty,Option.map aux rtntypopt,
List.map (fun (tm,(na,x)) ->
add_name found na;
Option.iter
- (fun (_,_,nl) -> List.iter (add_name found) nl) x;
- (aux tm,(na,Option.map (fun (_,ind,nal) -> (ind,nal)) x))) tml,
+ (fun (_,(_,nl)) -> List.iter (add_name found) nl) x;
+ (aux tm,(na,Option.map (fun (_,(ind,nal)) -> (ind,nal)) x))) tml,
List.map f eqnl)
- | GLetTuple (loc,nal,(na,po),b,c) ->
+ | GLetTuple (nal,(na,po),b,c) ->
add_name found na;
List.iter (add_name found) nal;
NLetTuple (nal,(na,Option.map aux po),aux b,aux c)
- | GIf (loc,c,(na,po),b1,b2) ->
+ | GIf (c,(na,po),b1,b2) ->
add_name found na;
NIf (aux c,(na,Option.map aux po),aux b1,aux b2)
- | GRec (_,fk,idl,dll,tl,bl) ->
+ | GRec (fk,idl,dll,tl,bl) ->
Array.iter (add_id found) idl;
let dll = Array.map (List.map (fun (na,bk,oc,b) ->
if bk != Explicit then
error "Binders marked as implicit not allowed in notations.";
add_name found na; (na,Option.map aux oc,aux b))) dll in
NRec (fk,idl,dll,Array.map aux tl,Array.map aux bl)
- | GCast (_,c,k) -> NCast (aux c,Miscops.map_cast_type aux k)
- | GSort (_,s) -> NSort s
- | GHole (_,w,naming,arg) ->
+ | GCast (c,k) -> NCast (aux c,Miscops.map_cast_type aux k)
+ | GSort s -> NSort s
+ | GHole (w,naming,arg) ->
if arg != None then has_ltac := true;
NHole (w, naming, arg)
- | GRef (_,r,_) -> NRef r
+ | GRef (r,_) -> NRef r
| GEvar _ | GPatVar _ ->
error "Existential variables not allowed in notations."
-
+ ) x
in
let t = aux a in
(* Side effect *)
@@ -451,13 +459,13 @@ let notation_constr_of_constr avoiding t =
notation_constr_of_glob_constr nenv t
let rec subst_pat subst pat =
- match pat with
+ match pat.CAst.v with
| PatVar _ -> pat
- | PatCstr (loc,((kn,i),j),cpl,n) ->
+ | PatCstr (((kn,i),j),cpl,n) ->
let kn' = subst_mind subst kn
and cpl' = List.smartmap (subst_pat subst) cpl in
- if kn' == kn && cpl' == cpl then pat else
- PatCstr (loc,((kn',i),j),cpl',n)
+ if kn' == kn && cpl' == cpl then pat else
+ CAst.make ?loc:pat.CAst.loc @@ PatCstr (((kn',i),j),cpl',n)
let rec subst_notation_constr subst bound raw =
match raw with
@@ -587,9 +595,9 @@ let abstract_return_type_context pi mklam tml rtno =
rtno
let abstract_return_type_context_glob_constr =
- abstract_return_type_context (fun (_,_,nal) -> nal)
- (fun na c ->
- GLambda(Loc.ghost,na,Explicit,GHole(Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None),c))
+ abstract_return_type_context (fun (_,(_,nal)) -> nal)
+ (fun na c -> CAst.make @@
+ GLambda(na,Explicit,CAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None),c))
let abstract_return_type_context_notation_constr =
abstract_return_type_context snd
@@ -661,18 +669,19 @@ let add_binding_env alp (terms,onlybinders,termlists,binderlists) var v =
let add_bindinglist_env (terms,onlybinders,termlists,binderlists) x bl =
(terms,onlybinders,termlists,(x,bl)::binderlists)
-let rec pat_binder_of_term = function
- | GVar (loc, id) -> PatVar (loc, Name id)
- | GApp (loc, GRef (_,ConstructRef cstr,_), l) ->
+let rec pat_binder_of_term t = CAst.map (function
+ | GVar id -> PatVar (Name id)
+ | GApp ({ CAst.v = GRef (ConstructRef cstr,_)}, l) ->
let nparams = Inductiveops.inductive_nparams (fst cstr) in
let _,l = List.chop nparams l in
- PatCstr (loc, cstr, List.map pat_binder_of_term l, Anonymous)
+ PatCstr (cstr, List.map pat_binder_of_term l, Anonymous)
| _ -> raise No_match
+ ) t
let bind_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var v =
try
let v' = Id.List.assoc var terms in
- match v, v' with
+ match CAst.(v.v, v'.v) with
| GHole _, _ -> sigma
| _, GHole _ ->
let sigma = Id.List.remove_assoc var terms,onlybinders,termlists,binderlists in
@@ -686,7 +695,7 @@ let bind_termlist_env alp (terms,onlybinders,termlists,binderlists as sigma) var
try
let vl' = Id.List.assoc var termlists in
let unify_term v v' =
- match v, v' with
+ match CAst.(v.v, v'.v) with
| GHole _, _ -> v'
| _, GHole _ -> v
| _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v' else raise No_match in
@@ -703,7 +712,7 @@ let bind_termlist_env alp (terms,onlybinders,termlists,binderlists as sigma) var
let bind_term_as_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var id =
try
match Id.List.assoc var terms with
- | GVar (_,id') ->
+ | { CAst.v = GVar id' } ->
(if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp),
sigma
| _ -> anomaly (str "A term which can be a binder has to be a variable")
@@ -711,7 +720,7 @@ let bind_term_as_binding_env alp (terms,onlybinders,termlists,binderlists as sig
(* The matching against a term allowing to find the instance has not been found yet *)
(* If it will be a different name, we shall unfortunately fail *)
(* TODO: look at the consequences for alp *)
- alp, add_env alp sigma var (GVar (Loc.ghost,id))
+ alp, add_env alp sigma var (CAst.make @@ GVar id)
let bind_binding_as_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var id =
try
@@ -738,16 +747,17 @@ let bind_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var
else (fst alp,(id1,id2)::snd alp),sigma
with Not_found -> alp, add_binding_env alp sigma var v
-let rec map_cases_pattern_name_left f = function
- | PatVar (loc,na) -> PatVar (loc,f na)
- | PatCstr (loc,c,l,na) -> PatCstr (loc,c,List.map_left (map_cases_pattern_name_left f) l,f na)
+let rec map_cases_pattern_name_left f = CAst.map (function
+ | PatVar na -> PatVar (f na)
+ | PatCstr (c,l,na) -> PatCstr (c,List.map_left (map_cases_pattern_name_left f) l,f na)
+ )
-let rec fold_cases_pattern_eq f x p p' = match p, p' with
- | PatVar (loc,na), PatVar (_,na') -> let x,na = f x na na' in x, PatVar (loc,na)
- | PatCstr (loc,c,l,na), PatCstr (_,c',l',na') when eq_constructor c c' ->
+let rec fold_cases_pattern_eq f x p p' = let open CAst in match p, p' with
+ | { loc; v = PatVar na}, { v = PatVar na' } -> let x,na = f x na na' in x, CAst.make ?loc @@ PatVar na
+ | { loc; v = PatCstr (c,l,na)}, { v = 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, PatCstr (loc,c,l,na)
+ x, CAst.make ?loc @@ PatCstr (c,l,na)
| _ -> failwith "Not equal"
and fold_cases_pattern_list_eq f x pl pl' = match pl, pl' with
@@ -758,9 +768,9 @@ and fold_cases_pattern_list_eq f x pl pl' = match pl, pl' with
x, p :: pl
| _ -> assert false
-let rec cases_pattern_eq p1 p2 = match p1, p2 with
-| PatVar (_, na1), PatVar (_, na2) -> Name.equal na1 na2
-| PatCstr (_, c1, pl1, na1), PatCstr (_, c2, pl2, na2) ->
+let rec cases_pattern_eq p1 p2 = match CAst.(p1.v, p2.v) with
+| PatVar na1, PatVar na2 -> Name.equal na1 na2
+| PatCstr (c1, pl1, na1), PatCstr (c2, pl2, na2) ->
eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 &&
Name.equal na1 na2
| _ -> false
@@ -779,7 +789,7 @@ let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma)
let unify_pat alp p p' =
try fold_cases_pattern_eq unify_name alp p p' with Failure _ -> raise No_match in
let unify_term alp v v' =
- match v, v' with
+ match CAst.(v.v, v'.v) with
| GHole _, _ -> v'
| _, GHole _ -> v
| _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v else raise No_match in
@@ -790,16 +800,17 @@ let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma)
| None, None -> None in
let unify_binding_kind bk bk' = if bk == bk' then bk' else raise No_match in
let unify_binder alp b b' =
- match b, b' with
- | GLocalAssum (loc,na,bk,t), GLocalAssum (_,na',bk',t') ->
+ let loc, loc' = CAst.(b.loc, b'.loc) in
+ match CAst.(b.v, b'.v) with
+ | GLocalAssum (na,bk,t), GLocalAssum (na',bk',t') ->
let alp, na = unify_name alp na na' in
- alp, GLocalAssum (loc, na, unify_binding_kind bk bk', unify_term alp t t')
- | GLocalDef (loc,na,bk,c,t), GLocalDef (_,na',bk',c',t') ->
+ alp, CAst.make ?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, GLocalDef (loc, na, unify_binding_kind bk bk', unify_term alp c c', unify_opt_term alp t t')
- | GLocalPattern (loc,(p,ids),id,bk,t), GLocalPattern (_,(p',_),_,bk',t') ->
+ alp, CAst.make ?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, GLocalPattern (loc, (p,ids), id, unify_binding_kind bk bk', unify_term alp t t')
+ alp, CAst.make ?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
@@ -826,18 +837,18 @@ 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 b' =
+ let unify_term_binder c = CAst.(map (fun b' ->
match c, b' with
- | GVar (loc, id), GLocalAssum (_, na', bk', t') ->
- GLocalAssum (loc, unify_id id na', bk', t')
- | c, GLocalPattern (loc, (p',ids), id, bk', t') ->
+ | { v = GVar id}, GLocalAssum (na', bk', t') ->
+ GLocalAssum (unify_id id na', bk', t')
+ | c, GLocalPattern ((p',ids), id, bk', t') ->
let p = pat_binder_of_term c in
- GLocalPattern (loc, (unify_pat p p',ids), id, bk', t')
- | _ -> raise No_match in
+ GLocalPattern ((unify_pat p p',ids), id, bk', t')
+ | _ -> raise No_match )) in
let rec unify cl bl' =
match cl, bl' with
| [], [] -> []
- | c :: cl, GLocalDef (_, _, _, _, t) :: bl' -> unify cl bl'
+ | c :: cl, { CAst.v = GLocalDef ( _, _, _, t) } :: bl' -> unify cl bl'
| c :: cl, b' :: bl' -> unify_term_binder c b' :: unify cl bl'
| _ -> raise No_match in
let bl = unify cl bl' in
@@ -879,9 +890,9 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
| _ -> raise No_match
let rec match_cases_pattern_binders metas acc pat1 pat2 =
- match (pat1,pat2) with
- | PatVar (_,na1), PatVar (_,na2) -> match_names metas acc na1 na2
- | PatCstr (_,c1,patl1,na1), PatCstr (_,c2,patl2,na2)
+ match CAst.(pat1.v, pat2.v) with
+ | PatVar na1, PatVar na2 -> match_names metas acc na1 na2
+ | PatCstr (c1,patl1,na1), PatCstr (c2,patl2,na2)
when eq_constructor c1 c2 && Int.equal (List.length patl1) (List.length patl2) ->
List.fold_left2 (match_cases_pattern_binders metas)
(match_names metas acc na1 na2) patl1 patl2
@@ -889,21 +900,22 @@ let rec match_cases_pattern_binders metas acc pat1 pat2 =
let glue_letin_with_decls = true
-let rec match_iterated_binders islambda decls = function
- | GLambda (loc,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,ids,[cp],b)]))
+let rec match_iterated_binders islambda decls bi = CAst.(with_loc_val (fun ?loc -> function
+ | GLambda (Name p,bk,t, { v = GCases (LetPatternStyle,None,[({ v = GVar e },_)],[(_,(ids,[cp],b))])})
when islambda && Id.equal p e ->
- match_iterated_binders islambda (GLocalPattern (loc,(cp,ids),p,bk,t)::decls) b
- | GLambda (loc,na,bk,t,b) when islambda ->
- match_iterated_binders islambda (GLocalAssum (loc,na,bk,t)::decls) b
- | GProd (loc,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,ids,[cp],b)]))
+ match_iterated_binders islambda ((CAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b
+ | GLambda (na,bk,t,b) when islambda ->
+ match_iterated_binders islambda ((CAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b
+ | GProd (Name p,bk,t, { v = GCases (LetPatternStyle,None,[({ v = GVar e },_)],[(_,(ids,[cp],b))]) } )
when not islambda && Id.equal p e ->
- match_iterated_binders islambda (GLocalPattern (loc,(cp,ids),p,bk,t)::decls) b
- | GProd (loc,(Name _ as na),bk,t,b) when not islambda ->
- match_iterated_binders islambda (GLocalAssum (loc,na,bk,t)::decls) b
- | GLetIn (loc,na,c,t,b) when glue_letin_with_decls ->
+ match_iterated_binders islambda ((CAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b
+ | GProd ((Name _ as na),bk,t,b) when not islambda ->
+ match_iterated_binders islambda ((CAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b
+ | GLetIn (na,c,t,b) when glue_letin_with_decls ->
match_iterated_binders islambda
- (GLocalDef (loc,na,Explicit (*?*), c,t)::decls) b
- | b -> (decls,b)
+ ((CAst.make ?loc @@ GLocalDef (na,Explicit (*?*), c,t))::decls) b
+ | b -> (decls, CAst.make ?loc b)
+ )) bi
let remove_sigma x (terms,onlybinders,termlists,binderlists) =
(Id.List.remove_assoc x terms,onlybinders,termlists,binderlists)
@@ -964,91 +976,92 @@ let does_not_come_from_already_eta_expanded_var =
(* The following test is then an approximation of what can be done *)
(* optimally (whether other looping situations can occur remains to be *)
(* checked). *)
- function GVar _ -> false | _ -> true
+ function { CAst.v = GVar _ } -> false | _ -> true
let rec match_ inner u alp metas sigma a1 a2 =
- match (a1,a2) with
-
+ let open CAst in
+ let loc = a1.loc in
+ match a1.v, a2 with
(* Matching notation variable *)
- | r1, NVar id2 when is_term_meta id2 metas -> bind_term_env alp sigma id2 r1
- | GVar (_,id1), NVar id2 when is_onlybinding_meta id2 metas -> bind_binding_as_term_env alp sigma id2 id1
- | r1, NVar id2 when is_bindinglist_meta id2 metas -> bind_term_env alp sigma id2 r1
+ | r1, NVar id2 when is_term_meta id2 metas -> bind_term_env alp sigma id2 a1
+ | GVar id1, NVar id2 when is_onlybinding_meta id2 metas -> bind_binding_as_term_env alp sigma id2 id1
+ | r1, NVar id2 when is_bindinglist_meta id2 metas -> bind_term_env alp sigma id2 a1
(* Matching recursive notations for terms *)
| r1, NList (x,y,iter,termin,lassoc) ->
- match_termlist (match_hd u alp) alp metas sigma r1 x y iter termin lassoc
+ match_termlist (match_hd u alp) alp metas sigma a1 x y iter termin lassoc
(* "λ p, let 'cp = p in t" -> "λ 'cp, t" *)
- | GLambda (loc,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,ids,[cp],b1)])),
+ | GLambda (Name p,bk,t1, { v = GCases (LetPatternStyle,None,[({ v = GVar e},_)],[(_,(ids,[cp],b1))])}),
NBinderList (x,_,NLambda (Name _id2,_,b2),termin) when Id.equal p e ->
- let (decls,b) = match_iterated_binders true [GLocalPattern(loc,(cp,ids),p,bk,t1)] b1 in
+ let (decls,b) = match_iterated_binders true [CAst.make ?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 (loc,na1,bk,t1,b1), NBinderList (x,_,NLambda (Name _id2,_,b2),termin)->
- let (decls,b) = match_iterated_binders true [GLocalAssum (loc,na1,bk,t1)] b1 in
+ | GLambda (na1,bk,t1,b1), NBinderList (x,_,NLambda (Name _id2,_,b2),termin)->
+ let (decls,b) = match_iterated_binders true [CAst.make ?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
(* "∀ p, let 'cp = p in t" -> "∀ 'cp, t" *)
- | GProd (loc,Name p,bk,t1,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,ids,[cp],b1)])),
+ | GProd (Name p,bk,t1, { v = GCases (LetPatternStyle,None,[({ v = 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 [GLocalPattern (loc,(cp,ids),p,bk,t1)] b1 in
+ let (decls,b) = match_iterated_binders true [CAst.make ?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 (loc,na1,bk,t1,b1), NBinderList (x,_,NProd (Name _id2,_,b2),termin)
+ | GProd (na1,bk,t1,b1), NBinderList (x,_,NProd (Name _id2,_,b2),termin)
when na1 != Anonymous ->
- let (decls,b) = match_iterated_binders false [GLocalAssum (loc,na1,bk,t1)] b1 in
+ let (decls,b) = match_iterated_binders false [CAst.make ?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
(* Matching recursive notations for binders: general case *)
- | r, NBinderList (x,y,iter,termin) ->
- match_binderlist_with_app (match_hd u) alp metas sigma r x y iter termin
+ | _r, NBinderList (x,y,iter,termin) ->
+ match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin
(* Matching individual binders as part of a recursive pattern *)
- | GLambda (loc,Name p,bk,t,GCases (_,LetPatternStyle,None,[(GVar(_,e),_)],[(_,ids,[cp],b1)])),
+ | GLambda (Name p,bk,t, { v = GCases (LetPatternStyle,None,[({ v = GVar e },_)],[(_,(ids,[cp],b1))])}),
NLambda (Name id,_,b2)
when is_bindinglist_meta id metas ->
- let alp,sigma = bind_bindinglist_env alp sigma id [GLocalPattern (loc,(cp,ids),p,bk,t)] in
+ let alp,sigma = bind_bindinglist_env alp sigma id [CAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t)] in
match_in u alp metas sigma b1 b2
- | GLambda (loc,na,bk,t,b1), NLambda (Name id,_,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 [GLocalAssum (loc,na,bk,t)] in
+ let alp,sigma = bind_bindinglist_env alp sigma id [CAst.make ?loc @@ GLocalAssum (na,bk,t)] in
match_in u alp metas sigma b1 b2
- | GProd (loc,na,bk,t,b1), NProd (Name id,_,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 [GLocalAssum (loc,na,bk,t)] in
+ let alp,sigma = bind_bindinglist_env alp sigma id [CAst.make ?loc @@ GLocalAssum (na,bk,t)] in
match_in u alp metas sigma b1 b2
(* Matching compositionally *)
- | GVar (_,id1), NVar id2 when alpha_var id1 id2 (fst alp) -> sigma
- | GRef (_,r1,_), NRef r2 when (eq_gr r1 r2) -> sigma
- | GApp (loc,f1,l1), NApp (f2,l2) ->
+ | GVar id1, NVar id2 when alpha_var id1 id2 (fst alp) -> sigma
+ | GRef (r1,_), NRef r2 when (eq_gr r1 r2) -> sigma
+ | GApp (f1,l1), NApp (f2,l2) ->
let n1 = List.length l1 and n2 = List.length l2 in
let f1,l1,f2,l2 =
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 GApp (loc,f1,l11),l12, f2,l2
+ let l11,l12 = List.chop (n1-n2) l1 in CAst.make ?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)
(match_in u alp metas sigma f1 f2) l1 l2
- | GLambda (_,na1,_,t1,b1), NLambda (na2,t2,b2) ->
+ | GLambda (na1,_,t1,b1), NLambda (na2,t2,b2) ->
match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2
- | GProd (_,na1,_,t1,b1), NProd (na2,t2,b2) ->
+ | GProd (na1,_,t1,b1), NProd (na2,t2,b2) ->
match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2
- | GLetIn (_,na1,b1,_,c1), NLetIn (na2,b2,None,c2)
- | GLetIn (_,na1,b1,None,c1), NLetIn (na2,b2,_,c2) ->
+ | GLetIn (na1,b1,_,c1), NLetIn (na2,b2,None,c2)
+ | GLetIn (na1,b1,None,c1), NLetIn (na2,b2,_,c2) ->
match_binders u alp metas na1 na2 (match_in u alp metas sigma b1 b2) c1 c2
- | GLetIn (_,na1,b1,Some t1,c1), NLetIn (na2,b2,Some t2,c2) ->
+ | GLetIn (na1,b1,Some t1,c1), NLetIn (na2,b2,Some t2,c2) ->
match_binders u alp metas na1 na2
(match_in u alp metas (match_in u alp metas sigma b1 b2) t1 t2) c1 c2
- | GCases (_,sty1,rtno1,tml1,eqnl1), NCases (sty2,rtno2,tml2,eqnl2)
+ | GCases (sty1,rtno1,tml1,eqnl1), NCases (sty2,rtno2,tml2,eqnl2)
when sty1 == sty2
&& Int.equal (List.length tml1) (List.length tml2)
&& Int.equal (List.length eqnl1) (List.length eqnl2) ->
@@ -1062,17 +1075,17 @@ let rec match_ inner u alp metas sigma a1 a2 =
(fun s (tm1,_) (tm2,_) ->
match_in u alp metas s tm1 tm2) sigma tml1 tml2 in
List.fold_left2 (match_equations u alp metas) sigma eqnl1 eqnl2
- | GLetTuple (_,nal1,(na1,to1),b1,c1), NLetTuple (nal2,(na2,to2),b2,c2)
+ | GLetTuple (nal1,(na1,to1),b1,c1), NLetTuple (nal2,(na2,to2),b2,c2)
when Int.equal (List.length nal1) (List.length nal2) ->
let sigma = match_opt (match_binders u alp metas na1 na2) sigma to1 to2 in
let sigma = match_in u alp metas sigma b1 b2 in
let (alp,sigma) =
List.fold_left2 (match_names metas) (alp,sigma) nal1 nal2 in
match_in u alp metas sigma c1 c2
- | GIf (_,a1,(na1,to1),b1,c1), NIf (a2,(na2,to2),b2,c2) ->
+ | GIf (a1,(na1,to1),b1,c1), NIf (a2,(na2,to2),b2,c2) ->
let sigma = match_opt (match_binders u alp metas na1 na2) sigma to1 to2 in
List.fold_left2 (match_in u alp metas) sigma [a1;b1;c1] [a2;b2;c2]
- | GRec (_,fk1,idl1,dll1,tl1,bl1), NRec (fk2,idl2,dll2,tl2,bl2)
+ | GRec (fk1,idl1,dll1,tl1,bl1), NRec (fk2,idl2,dll2,tl2,bl2)
when match_fix_kind fk1 fk2 && Int.equal (Array.length idl1) (Array.length idl2) &&
Array.for_all2 (fun l1 l2 -> Int.equal (List.length l1) (List.length l2)) dll1 dll2
->
@@ -1086,13 +1099,13 @@ let rec match_ inner u alp metas sigma a1 a2 =
let alp,sigma = Array.fold_right2 (fun id1 id2 alsig ->
match_names metas alsig (Name id1) (Name id2)) idl1 idl2 (alp,sigma) in
Array.fold_left2 (match_in u alp metas) sigma bl1 bl2
- | GCast(_,c1,CastConv t1), NCast (c2,CastConv t2)
- | GCast(_,c1,CastVM t1), NCast (c2,CastVM t2) ->
+ | GCast(c1,CastConv t1), NCast (c2,CastConv t2)
+ | GCast(c1,CastVM t1), NCast (c2,CastVM t2) ->
match_in u alp metas (match_in u alp metas sigma c1 c2) t1 t2
- | GCast(_,c1, CastCoerce), NCast(c2, CastCoerce) ->
+ | GCast(c1, CastCoerce), NCast(c2, CastCoerce) ->
match_in u alp metas sigma c1 c2
- | GSort (_,GType _), NSort (GType _) when not u -> sigma
- | GSort (_,s1), NSort s2 when Miscops.glob_sort_eq s1 s2 -> sigma
+ | GSort (GType _), NSort (GType _) when not u -> sigma
+ | GSort s1, NSort s2 when Miscops.glob_sort_eq s1 s2 -> sigma
| GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
| a, NHole _ -> sigma
@@ -1102,21 +1115,21 @@ let rec match_ inner u alp metas sigma a1 a2 =
otherwise how to ensure it corresponds to a well-typed eta-expansion;
we make an exception for types which are metavariables: this is useful e.g.
to print "{x:_ & P x}" knowing that notation "{x & P x}" is not defined. *)
- | b1, NLambda (Name id as na,(NHole _ | NVar _ as t2),b2) when inner ->
+ | _b1, NLambda (Name id as na,(NHole _ | NVar _ as t2),b2) when inner ->
let avoid =
- free_glob_vars b1 @ (* as in Namegen: *) glob_visible_short_qualid b1 in
+ free_glob_vars a1 @ (* as in Namegen: *) glob_visible_short_qualid a1 in
let id' = Namegen.next_ident_away id avoid in
- let t1 = GHole(Loc.ghost,Evar_kinds.BinderType (Name id'),Misctypes.IntroAnonymous,None) in
+ let t1 = CAst.make @@ GHole(Evar_kinds.BinderType (Name id'),Misctypes.IntroAnonymous,None) in
let sigma = match t2 with
| NHole _ -> sigma
| NVar id2 -> bind_term_env alp sigma id2 t1
| _ -> assert false in
let (alp,sigma) =
if is_bindinglist_meta id metas then
- bind_bindinglist_env alp sigma id [GLocalAssum (Loc.ghost,Name id',Explicit,t1)]
+ bind_bindinglist_env alp sigma id [CAst.make @@ GLocalAssum (Name id',Explicit,t1)]
else
match_names metas (alp,sigma) (Name id') na in
- match_in u alp metas sigma (mkGApp Loc.ghost b1 (GVar (Loc.ghost,id'))) b2
+ match_in u alp metas sigma (mkGApp a1 (CAst.make @@ GVar id')) b2
| (GRec _ | GEvar _), _
| _,_ -> raise No_match
@@ -1129,7 +1142,7 @@ and match_binders u alp metas na1 na2 sigma b1 b2 =
let (alp,sigma) = match_names metas (alp,sigma) na1 na2 in
match_in u alp metas sigma b1 b2
-and match_equations u alp metas sigma (_,_,patl1,rhs1) (patl2,rhs2) =
+and match_equations u alp metas sigma (_,(_,patl1,rhs1)) (patl2,rhs2) =
(* patl1 and patl2 have the same length because they respectively
correspond to some tml1 and tml2 that have the same length *)
let (alp,sigma) =
@@ -1137,9 +1150,9 @@ and match_equations u alp metas sigma (_,_,patl1,rhs1) (patl2,rhs2) =
(alp,sigma) patl1 patl2 in
match_in u alp metas sigma rhs1 rhs2
-let term_of_binder = function
- | Name id -> GVar (Loc.ghost,id)
- | Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)
+let term_of_binder bi = CAst.make @@ match bi with
+ | Name id -> GVar id
+ | Anonymous -> GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)
let match_notation_constr u c (metas,pat) =
let terms,binders,termlists,binderlists =
@@ -1150,7 +1163,7 @@ let match_notation_constr u c (metas,pat) =
with Not_found ->
(* Happens for binders bound to Anonymous *)
(* Find a better way to propagate Anonymous... *)
- GVar (Loc.ghost,x) in
+ CAst.make @@GVar x in
List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders') ->
match typ with
| NtnTypeConstr ->
@@ -1169,7 +1182,7 @@ let match_notation_constr u c (metas,pat) =
let add_patterns_for_params ind l =
let mib,_ = Global.lookup_inductive ind in
let nparams = mib.Declarations.mind_nparams in
- Util.List.addn nparams (PatVar (Loc.ghost,Anonymous)) l
+ Util.List.addn nparams (CAst.make @@ PatVar Anonymous) l
let bind_env_cases_pattern (terms,x,termlists,y as sigma) var v =
try
@@ -1194,12 +1207,13 @@ let match_cases_pattern_list match_fun metas sigma rest x y iter termin lassoc =
(terms,onlybinders,(x,if lassoc then l else List.rev l)::termlists, binderlists)
let rec match_cases_pattern metas (terms,(),termlists,() as sigma) a1 a2 =
- match (a1,a2) with
- | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 r1),(0,[])
- | PatVar (_,Anonymous), NHole _ -> sigma,(0,[])
- | PatCstr (loc,(ind,_ as r1),largs,_), NRef (ConstructRef r2) when eq_constructor r1 r2 ->
+ let open CAst in
+ match a1.v, a2 with
+ | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(0,[])
+ | PatVar Anonymous, NHole _ -> sigma,(0,[])
+ | PatCstr ((ind,_ as r1),largs,_), NRef (ConstructRef r2) when eq_constructor r1 r2 ->
sigma,(0,add_patterns_for_params (fst r1) largs)
- | PatCstr (loc,(ind,_ as r1),args1,_), NApp (NRef (ConstructRef r2),l2)
+ | PatCstr ((ind,_ as r1),args1,_), NApp (NRef (ConstructRef r2),l2)
when eq_constructor r1 r2 ->
let l1 = add_patterns_for_params (fst r1) args1 in
let le2 = List.length l2 in
@@ -1211,7 +1225,7 @@ let rec match_cases_pattern metas (terms,(),termlists,() as sigma) a1 a2 =
(List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args)
| r1, NList (x,y,iter,termin,lassoc) ->
(match_cases_pattern_list (match_cases_pattern_no_more_args)
- metas (terms,(),termlists,()) r1 x y iter termin lassoc),(0,[])
+ metas (terms,(),termlists,()) a1 x y iter termin lassoc),(0,[])
| _ -> raise No_match
and match_cases_pattern_no_more_args metas sigma a1 a2 =
diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli
index a61ba172e..64f811dc2 100644
--- a/interp/notation_ops.mli
+++ b/interp/notation_ops.mli
@@ -33,12 +33,12 @@ val notation_constr_of_glob_constr : notation_interp_env ->
(** Re-interpret a notation as a [glob_constr], taking care of binders *)
-val glob_constr_of_notation_constr_with_binders : Loc.t ->
+val glob_constr_of_notation_constr_with_binders : ?loc:Loc.t ->
('a -> Name.t -> 'a * Name.t) ->
('a -> notation_constr -> glob_constr) ->
'a -> notation_constr -> glob_constr
-val glob_constr_of_notation_constr : Loc.t -> notation_constr -> glob_constr
+val glob_constr_of_notation_constr : ?loc:Loc.t -> notation_constr -> glob_constr
(** {5 Matching a notation pattern against a [glob_constr]} *)
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 d863e0561..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,28 +54,28 @@ 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
+ | ByNotation (loc,(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) ->
+ | 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
- | ByNotation (loc,_,_) -> loc
+ | ByNotation (loc,(_,_)) -> loc
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.ml b/interp/stdarg.ml
index 5920b0d50..34fc5b2dc 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -32,7 +32,7 @@ let wit_pre_ident : string uniform_genarg_type =
let loc_of_or_by_notation f = function
| AN c -> f c
- | ByNotation (loc,s,_) -> loc
+ | ByNotation (loc,(s,_)) -> loc
let wit_int_or_var =
make0 ~dyn:(val_tag (topwit wit_int)) "int_or_var"
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index ac40a2328..6a98ee64d 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -21,7 +21,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 239226b2e..1fe63c19c 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -34,6 +34,10 @@ let _ = Goptions.declare_bool_option {
let error_invalid_pattern_notation ?loc () =
user_err ?loc (str "Invalid notation for pattern.")
+(* Legacy functions *)
+let down_located f (_l, x) = f x
+let located_fold_left f x (_l, y) = f x y
+
(**********************************************************************)
(* Functions on constr_expr *)
@@ -43,23 +47,23 @@ let is_constructor id =
(Nametab.locate_extended (qualid_of_ident id)))
with Not_found -> false
-let rec cases_pattern_fold_names f a = function
- | CPatRecord (_, l) ->
+let rec cases_pattern_fold_names f a pt = match CAst.(pt.v) with
+ | CPatRecord l ->
List.fold_left (fun acc (r, cp) -> cases_pattern_fold_names f acc cp) a l
- | CPatAlias (_,pat,id) -> f id a
- | CPatOr (_,patl) ->
+ | CPatAlias (pat,id) -> f id a
+ | CPatOr (patl) ->
List.fold_left (cases_pattern_fold_names f) a patl
- | CPatCstr (_,_,patl1,patl2) ->
+ | CPatCstr (_,patl1,patl2) ->
List.fold_left (cases_pattern_fold_names f)
(Option.fold_left (List.fold_left (cases_pattern_fold_names f)) a patl1) patl2
- | CPatNotation (_,_,(patl,patll),patl') ->
+ | CPatNotation (_,(patl,patll),patl') ->
List.fold_left (cases_pattern_fold_names f)
(List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll)) patl'
- | CPatDelimiters (_,_,pat) -> cases_pattern_fold_names f a pat
- | CPatAtom (_,Some (Ident (_,id))) when not (is_constructor id) -> f id a
+ | CPatDelimiters (_,pat) -> cases_pattern_fold_names f a pat
+ | 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"
+ | CPatCast ({CAst.loc},_) ->
+ CErrors.user_err ?loc ~hdr:"cases_pattern_fold_names"
(Pp.strbrk "Casts are not supported here.")
let ids_of_pattern =
@@ -67,7 +71,7 @@ let ids_of_pattern =
let ids_of_pattern_list =
List.fold_left
- (Loc.located_fold_left
+ (located_fold_left
(List.fold_left (cases_pattern_fold_names Id.Set.add)))
Id.Set.empty
@@ -79,7 +83,7 @@ let ids_of_cases_tomatch tms =
(fun (_, ona, indnal) l ->
Option.fold_right (fun t ids -> cases_pattern_fold_names Id.Set.add ids t)
indnal
- (Option.fold_right (Loc.down_located (name_fold Id.Set.add)) ona l))
+ (Option.fold_right (down_located (name_fold Id.Set.add)) ona l))
tms Id.Set.empty
let rec fold_constr_expr_binders g f n acc b = function
@@ -97,55 +101,56 @@ let rec fold_local_binders g f n acc b = function
f n (fold_local_binders g f n' acc b l) t
| CLocalDef ((_,na),c,t)::l ->
Option.fold_left (f n) (f n (fold_local_binders g f (name_fold g na n) acc b l) c) t
- | CLocalPattern (_,pat,t)::l ->
+ | CLocalPattern (_,(pat,t))::l ->
let acc = fold_local_binders g f (cases_pattern_fold_names g n pat) acc b l in
Option.fold_left (f n) acc t
| [] ->
f n acc b
-let fold_constr_expr_with_binders g f n acc = function
- | CAppExpl (loc,(_,_,_),l) -> List.fold_left (f n) acc l
- | CApp (loc,(_,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
- | CLetIn (_,na,a,t,b) ->
+let fold_constr_expr_with_binders g f n acc = CAst.with_val (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
+ | CLetIn (na,a,t,b) ->
f (name_fold g (snd na) n) (Option.fold_left (f n) (f n acc a) t) b
- | CCast (loc,a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b
- | CCast (loc,a,CastCoerce) -> f n acc a
- | CNotation (_,_,(l,ll,bll)) ->
+ | CCast (a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b
+ | CCast (a,CastCoerce) -> f n acc a
+ | CNotation (_,(l,ll,bll)) ->
(* The following is an approximation: we don't know exactly if
an ident is binding nor to which subterms bindings apply *)
let acc = List.fold_left (f n) acc (l@List.flatten ll) in
- List.fold_left (fun acc bl -> fold_local_binders g f n acc (CHole (Loc.ghost,None,IntroAnonymous,None)) bl) acc bll
- | CGeneralization (_,_,_,c) -> f n acc c
- | CDelimiters (loc,_,a) -> f n acc a
+ List.fold_left (fun acc bl -> fold_local_binders g f n acc (CAst.make @@ CHole (None,IntroAnonymous,None)) bl) acc bll
+ | CGeneralization (_,_,c) -> f n acc c
+ | CDelimiters (_,a) -> f n acc a
| CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CRef _ ->
acc
- | CRecord (loc,l) -> List.fold_left (fun acc (id, c) -> f n acc c) acc l
- | CCases (loc,sty,rtnpo,al,bl) ->
+ | CRecord l -> List.fold_left (fun acc (id, c) -> f n acc c) acc l
+ | CCases (sty,rtnpo,al,bl) ->
let ids = ids_of_cases_tomatch al in
let acc = Option.fold_left (f (Id.Set.fold g ids n)) acc rtnpo in
let acc = List.fold_left (f n) acc (List.map (fun (fst,_,_) -> fst) al) in
- List.fold_right (fun (loc,patl,rhs) acc ->
+ List.fold_right (fun (loc,(patl,rhs)) acc ->
let ids = ids_of_pattern_list patl in
f (Id.Set.fold g ids n) acc rhs) bl acc
- | CLetTuple (loc,nal,(ona,po),b,c) ->
- let n' = List.fold_right (Loc.down_located (name_fold g)) nal n in
- f (Option.fold_right (Loc.down_located (name_fold g)) ona n') (f n acc b) c
- | CIf (_,c,(ona,po),b1,b2) ->
+ | CLetTuple (nal,(ona,po),b,c) ->
+ let n' = List.fold_right (down_located (name_fold g)) nal n in
+ f (Option.fold_right (down_located (name_fold g)) ona n') (f n acc b) c
+ | CIf (c,(ona,po),b1,b2) ->
let acc = f n (f n (f n acc b1) b2) c in
Option.fold_left
- (f (Option.fold_right (Loc.down_located (name_fold g)) ona n)) acc po
- | CFix (loc,_,l) ->
+ (f (Option.fold_right (down_located (name_fold g)) ona n)) acc po
+ | CFix (_,l) ->
let n' = List.fold_right (fun ((_,id),_,_,_,_) -> g id) l n in
List.fold_right (fun (_,(_,o),lb,t,c) acc ->
fold_local_binders g f n'
(fold_local_binders g f n acc t lb) c lb) l acc
- | CCoFix (loc,_,_) ->
+ | CCoFix (_,_) ->
Feedback.msg_warning (strbrk "Capture check in multiple binders not done"); acc
+ )
let free_vars_of_constr_expr c =
let rec aux bdvars l = function
- | CRef (Ident (_,id),_) -> if Id.List.mem id bdvars then l else Id.Set.add id l
+ | { CAst.v = CRef (Ident (_,id),_) } -> if Id.List.mem id bdvars then l else Id.Set.add id l
| c -> fold_constr_expr_with_binders (fun a l -> a::l) aux bdvars l c
in aux [] Id.Set.empty c
@@ -180,20 +185,20 @@ let split_at_annot bl na =
end
| CLocalDef ((_,na),_,_) as x :: rest ->
if Name.equal (Name id) na then
- user_err ~loc
+ user_err ?loc
(Nameops.pr_id id ++ str" must be a proper parameter and not a local definition.")
else
aux (x :: acc) rest
- | CLocalPattern (loc,_,_) :: rest ->
- Loc.raise ~loc (Stream.Error "pattern with quote not allowed after fix")
+ | CLocalPattern (_,_) :: rest ->
+ 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
(* Used in correctness and interface *)
-let map_binder g e nal = List.fold_right (Loc.down_located (name_fold g)) nal e
+let map_binder g e nal = List.fold_right (down_located (name_fold g)) nal e
let map_binders f g e bl =
(* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
@@ -208,85 +213,87 @@ let map_local_binders f g e bl =
(map_binder g e nal, CLocalAssum(nal,k,f e ty)::bl)
| CLocalDef((loc,na),c,ty) ->
(name_fold g na e, CLocalDef((loc,na),f e c,Option.map (f e) ty)::bl)
- | CLocalPattern (loc,pat,t) ->
+ | CLocalPattern (loc,(pat,t)) ->
let ids = ids_of_pattern pat in
- (Id.Set.fold g ids e, CLocalPattern (loc,pat,Option.map (f e) t)::bl) in
+ (Id.Set.fold g ids e, CLocalPattern (loc,(pat,Option.map (f e) t))::bl) in
let (e,rbl) = List.fold_left h (e,[]) bl in
(e, List.rev rbl)
-let map_constr_expr_with_binders g f e = function
- | CAppExpl (loc,r,l) -> CAppExpl (loc,r,List.map (f e) l)
- | CApp (loc,(p,a),l) ->
- CApp (loc,(p,f e a),List.map (fun (a,i) -> (f e a,i)) l)
- | CProdN (loc,bl,b) ->
- let (e,bl) = map_binders f g e bl in CProdN (loc,bl,f e b)
- | CLambdaN (loc,bl,b) ->
- let (e,bl) = map_binders f g e bl in CLambdaN (loc,bl,f e b)
- | CLetIn (loc,na,a,t,b) ->
- CLetIn (loc,na,f e a,Option.map (f e) t,f (name_fold g (snd na) e) b)
- | CCast (loc,a,c) -> CCast (loc,f e a, Miscops.map_cast_type (f e) c)
- | CNotation (loc,n,(l,ll,bll)) ->
+let map_constr_expr_with_binders g f e = CAst.map (function
+ | CAppExpl (r,l) -> CAppExpl (r,List.map (f e) l)
+ | CApp ((p,a),l) ->
+ CApp ((p,f e a),List.map (fun (a,i) -> (f e a,i)) l)
+ | CProdN (bl,b) ->
+ let (e,bl) = map_binders f g e bl in CProdN (bl,f e b)
+ | CLambdaN (bl,b) ->
+ let (e,bl) = map_binders f g e bl in CLambdaN (bl,f e b)
+ | CLetIn (na,a,t,b) ->
+ CLetIn (na,f e a,Option.map (f e) t,f (name_fold g (snd na) e) b)
+ | CCast (a,c) -> CCast (f e a, Miscops.map_cast_type (f e) c)
+ | CNotation (n,(l,ll,bll)) ->
(* This is an approximation because we don't know what binds what *)
- CNotation (loc,n,(List.map (f e) l,List.map (List.map (f e)) ll,
+ CNotation (n,(List.map (f e) l,List.map (List.map (f e)) ll,
List.map (fun bl -> snd (map_local_binders f g e bl)) bll))
- | CGeneralization (loc,b,a,c) -> CGeneralization (loc,b,a,f e c)
- | CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a)
+ | CGeneralization (b,a,c) -> CGeneralization (b,a,f e c)
+ | CDelimiters (s,a) -> CDelimiters (s,f e a)
| CHole _ | CEvar _ | CPatVar _ | CSort _
| CPrim _ | CRef _ as x -> x
- | CRecord (loc,l) -> CRecord (loc,List.map (fun (id, c) -> (id, f e c)) l)
- | CCases (loc,sty,rtnpo,a,bl) ->
- let bl = List.map (fun (loc,patl,rhs) ->
+ | CRecord l -> CRecord (List.map (fun (id, c) -> (id, f e c)) l)
+ | CCases (sty,rtnpo,a,bl) ->
+ let bl = List.map (fun (loc,(patl,rhs)) ->
let ids = ids_of_pattern_list patl in
- (loc,patl,f (Id.Set.fold g ids e) rhs)) bl in
+ (loc,(patl,f (Id.Set.fold g ids e) rhs))) bl in
let ids = ids_of_cases_tomatch a in
let po = Option.map (f (Id.Set.fold g ids e)) rtnpo in
- CCases (loc, sty, po, List.map (fun (tm,x,y) -> f e tm,x,y) a,bl)
- | CLetTuple (loc,nal,(ona,po),b,c) ->
- let e' = List.fold_right (Loc.down_located (name_fold g)) nal e in
- let e'' = Option.fold_right (Loc.down_located (name_fold g)) ona e in
- CLetTuple (loc,nal,(ona,Option.map (f e'') po),f e b,f e' c)
- | CIf (loc,c,(ona,po),b1,b2) ->
- let e' = Option.fold_right (Loc.down_located (name_fold g)) ona e in
- CIf (loc,f e c,(ona,Option.map (f e') po),f e b1,f e b2)
- | CFix (loc,id,dl) ->
- CFix (loc,id,List.map (fun (id,n,bl,t,d) ->
+ CCases (sty, po, List.map (fun (tm,x,y) -> f e tm,x,y) a,bl)
+ | CLetTuple (nal,(ona,po),b,c) ->
+ let e' = List.fold_right (down_located (name_fold g)) nal e in
+ let e'' = Option.fold_right (down_located (name_fold g)) ona e in
+ CLetTuple (nal,(ona,Option.map (f e'') po),f e b,f e' c)
+ | CIf (c,(ona,po),b1,b2) ->
+ let e' = Option.fold_right (down_located (name_fold g)) ona e in
+ CIf (f e c,(ona,Option.map (f e') po),f e b1,f e b2)
+ | CFix (id,dl) ->
+ CFix (id,List.map (fun (id,n,bl,t,d) ->
let (e',bl') = map_local_binders f g e bl in
let t' = f e' t in
(* Note: fix names should be inserted before the arguments... *)
let e'' = List.fold_left (fun e ((_,id),_,_,_,_) -> g id e) e' dl in
let d' = f e'' d in
(id,n,bl',t',d')) dl)
- | CCoFix (loc,id,dl) ->
- CCoFix (loc,id,List.map (fun (id,bl,t,d) ->
+ | CCoFix (id,dl) ->
+ CCoFix (id,List.map (fun (id,bl,t,d) ->
let (e',bl') = map_local_binders f g e bl in
let t' = f e' t in
let e'' = List.fold_left (fun e ((_,id),_,_,_) -> g id e) e' dl in
let d' = f e'' d in
(id,bl',t',d')) dl)
+ )
(* Used in constrintern *)
let rec replace_vars_constr_expr l = function
- | CRef (Ident (loc,id),us) as x ->
- (try CRef (Ident (loc,Id.Map.find id l),us) with Not_found -> x)
+ | { CAst.loc; v = CRef (Ident (loc_id,id),us) } as x ->
+ (try CAst.make ?loc @@ CRef (Ident (loc_id,Id.Map.find id l),us) with Not_found -> x)
| c -> map_constr_expr_with_binders Id.Map.remove
replace_vars_constr_expr l c
(* 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 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-29 14:42:17 +0000