From 9bebbb96e58b3c1b0f7f88ba2af45462eae69b0f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 10 Dec 2017 09:26:25 +0100 Subject: [ast] Improve precision of Ast location recognition in serialization. We follow the suggestions in #402 and turn uses of `Loc.located` in `vernac` into `CAst.t`. The impact should be low as this change mostly affects top-level vernaculars. With this change, we are even closer to automatically map a text document to its AST in a programmatic way. --- interp/constrexpr_ops.ml | 119 ++++++++++++++++--------------- interp/constrexpr_ops.mli | 17 +++-- interp/constrextern.ml | 52 +++++++------- interp/constrintern.ml | 152 ++++++++++++++++++++-------------------- interp/constrintern.mli | 2 +- interp/declare.ml | 2 +- interp/declare.mli | 2 +- interp/dumpglob.ml | 6 +- interp/dumpglob.mli | 2 +- interp/implicit_quantifiers.ml | 32 ++++----- interp/implicit_quantifiers.mli | 9 ++- interp/reserve.ml | 2 +- interp/reserve.mli | 3 +- interp/stdarg.mli | 6 +- interp/topconstr.mli | 3 +- 15 files changed, 203 insertions(+), 206 deletions(-) (limited to 'interp') diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 8aca6e333..d05e7d909 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -61,13 +61,13 @@ let explicitation_eq ex1 ex2 = match ex1, ex2 with Id.equal id1 id2 | _ -> false -let eq_located f (_, x) (_, y) = f x y +let eq_ast f { CAst.v = x } { CAst.v = y } = f x y let rec cases_pattern_expr_eq p1 p2 = if CAst.(p1.v == p2.v) then true else match CAst.(p1.v, p2.v) with | CPatAlias(a1,i1), CPatAlias(a2,i2) -> - Name.equal (snd i1) (snd i2) && cases_pattern_expr_eq a1 a2 + eq_ast Name.equal i1 i2 && cases_pattern_expr_eq a1 a2 | CPatCstr(c1,a1,b1), CPatCstr(c2,a2,b2) -> eq_reference c1 c2 && Option.equal (List.equal cases_pattern_expr_eq) a1 a2 && @@ -106,10 +106,10 @@ let rec constr_expr_eq e1 e2 = 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) -> - eq_located Id.equal id1 id2 && + eq_ast Id.equal id1 id2 && List.equal fix_expr_eq fl1 fl2 | CCoFix(id1,fl1), CCoFix(id2,fl2) -> - eq_located Id.equal id1 id2 && + eq_ast Id.equal id1 id2 && List.equal cofix_expr_eq fl1 fl2 | CProdN(bl1,a1), CProdN(bl2,a2) -> List.equal local_binder_eq bl1 bl2 && @@ -117,8 +117,8 @@ let rec constr_expr_eq e1 e2 = | CLambdaN(bl1,a1), CLambdaN(bl2,a2) -> List.equal local_binder_eq bl1 bl2 && constr_expr_eq a1 a2 - | CLetIn((_,na1),a1,t1,b1), CLetIn((_,na2),a2,t2,b2) -> - Name.equal na1 na2 && + | CLetIn(na1,a1,t1,b1), CLetIn(na2,a2,t2,b2) -> + eq_ast Name.equal na1 na2 && constr_expr_eq a1 a2 && Option.equal constr_expr_eq t1 t2 && constr_expr_eq b1 b2 @@ -141,14 +141,14 @@ let rec constr_expr_eq e1 e2 = 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) -> - List.equal (eq_located Name.equal) n1 n2 && - Option.equal (eq_located Name.equal) m1 m2 && + List.equal (eq_ast Name.equal) n1 n2 && + Option.equal (eq_ast 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) -> constr_expr_eq e1 e2 && - Option.equal (eq_located Name.equal) n1 n2 && + Option.equal (eq_ast Name.equal) n1 n2 && Option.equal constr_expr_eq r1 r2 && constr_expr_eq t1 t2 && constr_expr_eq f1 f2 @@ -181,28 +181,28 @@ let rec constr_expr_eq e1 e2 = | CGeneralization _ | CDelimiters _ | CProj _), _ -> false and args_eq (a1,e1) (a2,e2) = - Option.equal (eq_located explicitation_eq) e1 e2 && + Option.equal (eq_ast explicitation_eq) e1 e2 && constr_expr_eq a1 a2 and case_expr_eq (e1, n1, p1) (e2, n2, p2) = constr_expr_eq e1 e2 && - Option.equal (eq_located Name.equal) n1 n2 && + Option.equal (eq_ast Name.equal) n1 n2 && Option.equal cases_pattern_expr_eq p1 p2 -and branch_expr_eq (_, (p1, e1)) (_, (p2, e2)) = +and branch_expr_eq {CAst.v=(p1, e1)} {CAst.v=(p2, e2)} = List.equal (List.equal cases_pattern_expr_eq) p1 p2 && constr_expr_eq e1 e2 and fix_expr_eq (id1,(j1, r1),bl1,a1,b1) (id2,(j2, r2),bl2,a2,b2) = - (eq_located Id.equal id1 id2) && - Option.equal (eq_located Id.equal) j1 j2 && + (eq_ast Id.equal id1 id2) && + Option.equal (eq_ast Id.equal) j1 j2 && recursion_order_expr_eq r1 r2 && List.equal local_binder_eq bl1 bl2 && constr_expr_eq a1 a2 && constr_expr_eq b1 b2 and cofix_expr_eq (id1,bl1,a1,b1) (id2,bl2,a2,b2) = - (eq_located Id.equal id1 id2) && + (eq_ast Id.equal id1 id2) && List.equal local_binder_eq bl1 bl2 && constr_expr_eq a1 a2 && constr_expr_eq b1 b2 @@ -216,10 +216,10 @@ and recursion_order_expr_eq r1 r2 = match r1, r2 with and local_binder_eq l1 l2 = match l1, l2 with | CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) -> - eq_located Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2 + eq_ast Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2 | CLocalAssum (n1, _, e1), CLocalAssum (n2, _, e2) -> (** Don't care about the [binder_kind] *) - List.equal (eq_located Name.equal) n1 n2 && constr_expr_eq e1 e2 + List.equal (eq_ast Name.equal) n1 n2 && constr_expr_eq e1 e2 | _ -> false and constr_notation_substitution_eq (e1, el1, b1, bl1) (e2, el2, b2, bl2) = @@ -244,12 +244,12 @@ and cast_expr_eq c1 c2 = match c1, c2 with 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_opt loc (constr_loc t) - | CLocalDef ((loc,_),b,Some t) -> Loc.merge_opt loc (Loc.merge_opt (constr_loc b) (constr_loc t)) +let local_binder_loc = let open CAst in function + | CLocalAssum ({ 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 | [] -> None @@ -257,9 +257,6 @@ let local_binders_loc bll = match bll with (** Folds and maps *) -(* Legacy functions *) -let down_located f (_l, x) = f x - let is_constructor id = try Globnames.isConstructRef (Smartlocate.global_of_extended_global @@ -269,7 +266,7 @@ let is_constructor id = 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,(loc,na)) -> Name.fold_right f na (cases_pattern_fold_names f a pat) + | CPatAlias (pat,{CAst.v=na}) -> Name.fold_right f na (cases_pattern_fold_names f a pat) | CPatOr (patl) -> List.fold_left (cases_pattern_fold_names f) a patl | CPatCstr (_,patl1,patl2) -> @@ -301,17 +298,17 @@ 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 (down_located (Name.fold_right Id.Set.add)) ona l)) + (Option.fold_right (CAst.with_val (Name.fold_right Id.Set.add)) ona l)) tms Id.Set.empty -let rec fold_local_binders g f n acc b = function +let rec fold_local_binders g f n acc b = let open CAst in function | CLocalAssum (nal,bk,t)::l -> - let nal = snd (List.split nal) in + let nal = List.(map (fun {v} -> v) nal) in let n' = List.fold_right (Name.fold_right g) nal n in f n (fold_local_binders g f n' acc b l) t - | CLocalDef ((_,na),c,t)::l -> + | CLocalDef ( { v = na },c,t)::l -> Option.fold_left (f n) (f n (fold_local_binders g f (Name.fold_right g na n) acc b l) c) t - | CLocalPattern (_,(pat,t))::l -> + | CLocalPattern { v = 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 | [] -> @@ -322,7 +319,7 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function | CApp ((_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l) | CProdN (l,b) | CLambdaN (l,b) -> fold_local_binders g f n acc b l | CLetIn (na,a,t,b) -> - f (Name.fold_right g (snd na) n) (Option.fold_left (f n) (f n acc a) t) b + f (Name.fold_right g (na.CAst.v) n) (Option.fold_left (f n) (f n acc a) t) b | 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,bl,bll)) -> @@ -339,18 +336,18 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function 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 {CAst.v=(patl,rhs)} acc -> let ids = ids_of_pattern_list patl in f (Id.Set.fold g ids n) acc rhs) bl acc | CLetTuple (nal,(ona,po),b,c) -> - let n' = List.fold_right (down_located (Name.fold_right g)) nal n in - f (Option.fold_right (down_located (Name.fold_right g)) ona n') (f n acc b) c + let n' = List.fold_right (CAst.with_val (Name.fold_right g)) nal n in + f (Option.fold_right (CAst.with_val (Name.fold_right 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 (down_located (Name.fold_right g)) ona n)) acc po + (f (Option.fold_right (CAst.with_val (Name.fold_right g)) ona n)) acc po | CFix (_,l) -> - let n' = List.fold_right (fun ((_,id),_,_,_,_) -> g id) l n in + let n' = List.fold_right (fun ( { CAst.v = 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 @@ -369,18 +366,19 @@ let free_vars_of_constr_expr c = let occur_var_constr_expr id c = Id.Set.mem id (free_vars_of_constr_expr c) (* Used in correctness and interface *) -let map_binder g e nal = List.fold_right (down_located (Name.fold_right g)) nal e +let map_binder g e nal = List.fold_right (CAst.with_val (Name.fold_right g)) nal e let map_local_binders f g e bl = (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *) + let open CAst in let h (e,bl) = function CLocalAssum(nal,k,ty) -> (map_binder g e nal, CLocalAssum(nal,k,f e ty)::bl) - | CLocalDef((loc,na),c,ty) -> - (Name.fold_right g na e, CLocalDef((loc,na),f e c,Option.map (f e) ty)::bl) - | CLocalPattern (loc,(pat,t)) -> + | CLocalDef( { loc ; v = na } as cna ,c,ty) -> + (Name.fold_right g na e, CLocalDef(cna,f e c,Option.map (f e) ty)::bl) + | CLocalPattern { loc; v = 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 (make ?loc (pat,Option.map (f e) t))::bl) in let (e,rbl) = List.fold_left h (e,[]) bl in (e, List.rev rbl) @@ -393,7 +391,7 @@ let map_constr_expr_with_binders g f e = CAst.map (function | CLambdaN (bl,b) -> let (e,bl) = map_local_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_right g (snd na) e) b) + CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (na.CAst.v) e) b) | CCast (a,c) -> CCast (f e a, Miscops.map_cast_type (f e) c) | CNotation (n,(l,ll,bl,bll)) -> (* This is an approximation because we don't know what binds what *) @@ -405,32 +403,32 @@ let map_constr_expr_with_binders g f e = CAst.map (function | CPrim _ | CRef _ as x -> x | 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 bl = List.map (fun {CAst.v=(patl,rhs);loc} -> let ids = ids_of_pattern_list patl in - (loc,(patl,f (Id.Set.fold g ids e) rhs))) bl in + CAst.make ?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 (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_right g)) nal e in - let e'' = Option.fold_right (down_located (Name.fold_right g)) ona e in + let e' = List.fold_right (CAst.with_val (Name.fold_right g)) nal e in + let e'' = Option.fold_right (CAst.with_val (Name.fold_right 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_right g)) ona e in + let e' = Option.fold_right (CAst.with_val (Name.fold_right 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 e'' = List.fold_left (fun e ({ CAst.v = id },_,_,_,_) -> g id e) e' dl in let d' = f e'' d in (id,n,bl',t',d')) dl) | 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 e'' = List.fold_left (fun e ({ CAst.v = id },_,_,_) -> g id e) e' dl in let d' = f e'' d in (id,bl',t',d')) dl) | CProj (p,c) -> @@ -471,17 +469,18 @@ let error_invalid_pattern_notation ?loc () = (* Interpret the index of a recursion order annotation *) let split_at_annot bl na = - let names = List.map snd (names_of_local_assums bl) in + let open CAst in + let names = List.map (fun { v } -> v) (names_of_local_assums bl) in match na with | None -> begin match names with | [] -> CErrors.user_err (Pp.str "A fixpoint needs at least one parameter.") | _ -> ([], bl) end - | Some (loc, id) -> + | Some { loc; v = id } -> let rec aux acc = function | CLocalAssum (bls, k, t) as x :: rest -> - let test (_, na) = match na with + let test { CAst.v = na } = match na with | Name id' -> Id.equal id id' | Anonymous -> false in @@ -495,13 +494,13 @@ let split_at_annot bl na = in (List.rev ans, CLocalAssum (r, k, t) :: rest) end - | CLocalDef ((_,na),_,_) as x :: rest -> + | CLocalDef ({ CAst.v = na },_,_) as x :: rest -> if Name.equal (Name id) na then CErrors.user_err ?loc (Id.print id ++ str" must be a proper parameter and not a local definition.") else aux (x :: acc) rest - | CLocalPattern (_,_) :: rest -> + | CLocalPattern _ :: rest -> Loc.raise ?loc (Stream.Error "pattern with quote not allowed after fix") | [] -> CErrors.user_err ?loc @@ -536,14 +535,14 @@ let coerce_reference_to_id = function (str "This expression should be a simple identifier.") let coerce_to_id = function - | { CAst.v = CRef (Ident (loc,id),None) } -> (loc,id) + | { CAst.v = CRef (Ident (loc,id),None) } -> CAst.make ?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 - | { CAst.v = CRef (Ident (loc,id),None) } -> (loc,Name id) - | { CAst.loc; CAst.v = CHole (None,Misctypes.IntroAnonymous,None) } -> (loc,Anonymous) + | { CAst.v = CRef (Ident (loc,id),None) } -> CAst.make ?loc @@ Name id + | { CAst.loc; CAst.v = CHole (None,Misctypes.IntroAnonymous,None) } -> CAst.make ?loc Anonymous | { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_name" (str "This expression should be a name.") @@ -569,8 +568,8 @@ let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function CPatAtom (Some r) | CHole (None,Misctypes.IntroAnonymous,None) -> CPatAtom None - | CLetIn ((loc,Name id),b,None,{ CAst.v = CRef (Ident (_,id'),None) }) when Id.equal id id' -> - CPatAlias (coerce_to_cases_pattern_expr b, (loc,Name id)) + | CLetIn ({CAst.loc;v=Name id},b,None,{ CAst.v = CRef (Ident (_,id'),None) }) when Id.equal id id' -> + CPatAlias (coerce_to_cases_pattern_expr b, CAst.(make ?loc @@ Name id)) | CApp ((None,p),args) when List.for_all (fun (_,e) -> e=None) args -> (mkAppPattern (coerce_to_cases_pattern_expr p) (List.map (fun (a,_) -> coerce_to_cases_pattern_expr a) args)).CAst.v | CAppExpl ((None,r,i),args) -> diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 0b00b0e4d..50c818d3c 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Loc open Names open Libnames open Misctypes @@ -44,9 +43,9 @@ val mkIdentC : Id.t -> constr_expr val mkRefC : reference -> constr_expr val mkAppC : constr_expr * constr_expr list -> constr_expr val mkCastC : constr_expr * constr_expr cast_type -> constr_expr -val mkLambdaC : Name.t located list * binder_kind * constr_expr * 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 mkLambdaC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr +val mkLetInC : lname * constr_expr * constr_expr option * constr_expr -> constr_expr +val mkProdC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr val mkCLambdaN : ?loc:Loc.t -> local_binder_expr list -> constr_expr -> constr_expr (** Same as [abstract_constr_expr], with location *) @@ -72,10 +71,10 @@ val prod_constr_expr : constr_expr -> local_binder_expr list -> constr_expr val coerce_reference_to_id : reference -> Id.t (** FIXME: nothing to do here *) -val coerce_to_id : constr_expr -> Id.t located +val coerce_to_id : constr_expr -> lident (** Destruct terms of the form [CRef (Ident _)]. *) -val coerce_to_name : constr_expr -> Name.t located +val coerce_to_name : constr_expr -> lname (** Destruct terms of the form [CRef (Ident _)] or [CHole _]. *) val coerce_to_cases_pattern_expr : constr_expr -> cases_pattern_expr @@ -84,10 +83,10 @@ val coerce_to_cases_pattern_expr : constr_expr -> cases_pattern_expr val default_binder_kind : binder_kind -val names_of_local_binders : local_binder_expr list -> Name.t located list +val names_of_local_binders : local_binder_expr list -> lname list (** Retrieve a list of binding names from a list of binders. *) -val names_of_local_assums : local_binder_expr list -> Name.t located list +val names_of_local_assums : local_binder_expr list -> lname list (** Same as [names_of_local_binder_exprs], but does not take the [let] bindings into account. *) @@ -113,7 +112,7 @@ val ids_of_cases_indtype : cases_pattern_expr -> Id.Set.t val free_vars_of_constr_expr : constr_expr -> Id.Set.t val occur_var_constr_expr : Id.t -> constr_expr -> bool -val split_at_annot : local_binder_expr list -> Id.t located option -> local_binder_expr list * local_binder_expr list +val split_at_annot : local_binder_expr list -> lident option -> local_binder_expr list * local_binder_expr list val ntn_loc : ?loc:Loc.t -> constr_notation_substitution -> string -> (int * int) list val patntn_loc : ?loc:Loc.t -> cases_pattern_notation_substitution -> string -> (int * int) list diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 9e18966b6..dec86ba81 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -257,7 +257,7 @@ let insert_pat_delimiters ?loc p = function let insert_pat_alias ?loc p = function | Anonymous -> p - | Name _ as na -> CAst.make ?loc @@ CPatAlias (p,(loc,na)) + | Name _ as na -> CAst.make ?loc @@ CPatAlias (p,(CAst.make ?loc na)) (**********************************************************************) (* conversion of references *) @@ -574,7 +574,7 @@ let explicitize inctx impl (cf,f) args = is_significant_implicit (Lazy.force a)) in if visible then - (Lazy.force a,Some (Loc.tag @@ ExplByName (name_of_implicit imp))) :: tail + (Lazy.force a,Some (make @@ ExplByName (name_of_implicit imp))) :: tail else tail | a::args, _::impl -> (Lazy.force a,None) :: exprec (q+1) (args,impl) @@ -816,7 +816,7 @@ let rec extern inctx scopes vars r = (List.map (fun c -> lazy (sub_extern true scopes vars c)) args)) | GLetIn (na,b,t,c) -> - CLetIn ((loc,na),sub_extern false scopes vars b, + CLetIn (make ?loc na,sub_extern false scopes vars b, Option.map (extern_typ scopes vars) t, extern inctx scopes (add_vname vars na) c) @@ -840,12 +840,12 @@ let rec extern inctx scopes vars r = | None -> None | Some ntn -> if occur_glob_constr id ntn then - Some (Loc.tag Anonymous) + Some (CAst.make Anonymous) else None end | Anonymous, _ -> None | Name id, GVar id' when Id.equal id id' -> None - | Name _, _ -> Some (Loc.tag na) in + | Name _, _ -> Some (CAst.make na) in (sub_extern false scopes vars tm, na', Option.map (fun (loc,(ind,nal)) -> @@ -859,15 +859,15 @@ let rec extern inctx scopes vars r = CCases (sty,rtntypopt',tml,eqns) | GLetTuple (nal,(na,typopt),tm,b) -> - CLetTuple (List.map (fun na -> (Loc.tag na)) nal, - (Option.map (fun _ -> (Loc.tag na)) typopt, + CLetTuple (List.map CAst.make nal, + (Option.map (fun _ -> (make 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 (c,(na,typopt),b1,b2) -> CIf (sub_extern false scopes vars c, - (Option.map (fun _ -> (Loc.tag na)) typopt, + (Option.map (fun _ -> (CAst.make na)) typopt, Option.map (extern_typ scopes (add_vname vars na)) typopt), sub_extern inctx scopes vars b1, sub_extern inctx scopes vars b2) @@ -885,13 +885,13 @@ let rec extern inctx scopes vars r = let n = match fst nv.(i) with | None -> None - | Some x -> Some (Loc.tag @@ Name.get_id (List.nth assums x)) + | Some x -> Some (CAst.make @@ Name.get_id (List.nth assums x)) in let ro = extern_recursion_order scopes vars (snd nv.(i)) in - ((Loc.tag fi), (n, ro), bl, extern_typ scopes vars0 ty, + ((CAst.make fi), (n, ro), bl, extern_typ scopes vars0 ty, extern false scopes vars1 def)) idv in - CFix ((loc,idv.(n)),Array.to_list listdecl) + CFix (CAst.(make ?loc idv.(n)), Array.to_list listdecl) | GCoFix n -> let listdecl = Array.mapi (fun i fi -> @@ -899,10 +899,10 @@ let rec extern inctx scopes vars r = let (_,ids,bl) = extern_local_binder scopes vars bl in let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in - ((Loc.tag fi),bl,extern_typ scopes vars0 tyv.(i), + ((CAst.make fi),bl,extern_typ scopes vars0 tyv.(i), sub_extern false scopes vars1 bv.(i))) idv in - CCoFix ((loc,idv.(n)),Array.to_list listdecl)) + CCoFix (CAst.(make ?loc idv.(n)),Array.to_list listdecl)) | GSort s -> CSort (extern_glob_sort s) @@ -932,7 +932,7 @@ and factorize_prod scopes vars na bk aty c = let disjpat = if occur_glob_constr id b then List.map (set_pat_alias id) disjpat else disjpat in let b = extern_typ scopes vars b in let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes vars) disjpat) in - let binder = CLocalPattern (c.loc,(p,None)) in + let binder = CLocalPattern (make ?loc:c.loc (p,None)) in (match b.v with | CProdN (bl,b) -> CProdN (binder::bl,b) | _ -> CProdN ([binder],b)) @@ -943,11 +943,11 @@ and factorize_prod scopes vars na bk aty c = | Name id, CProdN (CLocalAssum(nal,Default bk',ty)::bl,b) when binding_kind_eq bk bk' && constr_expr_eq aty ty && not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) -> - CProdN (CLocalAssum(Loc.tag na::nal,Default bk,aty)::bl,b) + CProdN (CLocalAssum(make na::nal,Default bk,aty)::bl,b) | _, CProdN (bl,b) -> - CProdN (CLocalAssum([Loc.tag na],Default bk,aty)::bl,b) + CProdN (CLocalAssum([make na],Default bk,aty)::bl,b) | _, _ -> - CProdN ([CLocalAssum([Loc.tag na],Default bk,aty)],c) + CProdN ([CLocalAssum([make na],Default bk,aty)],c) and factorize_lambda inctx scopes vars na bk aty c = let store, get = set_temporary_memory () in @@ -960,7 +960,7 @@ and factorize_lambda inctx scopes vars na bk aty c = let disjpat = if occur_glob_constr id b then List.map (set_pat_alias id) disjpat else disjpat in let b = sub_extern inctx scopes vars b in let p = mkCPatOr (List.map (extern_cases_pattern_in_scope scopes vars) disjpat) in - let binder = CLocalPattern (c.loc,(p,None)) in + let binder = CLocalPattern (make ?loc:c.loc (p,None)) in (match b.v with | CLambdaN (bl,b) -> CLambdaN (binder::bl,b) | _ -> CLambdaN ([binder],b)) @@ -971,11 +971,11 @@ and factorize_lambda inctx scopes vars na bk aty c = | CLambdaN (CLocalAssum(nal,Default bk',ty)::bl,b) when binding_kind_eq bk bk' && constr_expr_eq aty ty && not (occur_name na ty) (* avoid na in ty escapes scope *) -> - CLambdaN (CLocalAssum(Loc.tag na::nal,Default bk,aty)::bl,b) + CLambdaN (CLocalAssum(make na::nal,Default bk,aty)::bl,b) | CLambdaN (bl,b) -> - CLambdaN (CLocalAssum([Loc.tag na],Default bk,aty)::bl,b) + CLambdaN (CLocalAssum([make na],Default bk,aty)::bl,b) | _ -> - CLambdaN ([CLocalAssum([Loc.tag na],Default bk,aty)],c) + CLambdaN ([CLocalAssum([make na],Default bk,aty)],c) and extern_local_binder scopes vars = function [] -> ([],[],[]) @@ -985,7 +985,7 @@ and extern_local_binder scopes vars = function let (assums,ids,l) = extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l in (assums,na::ids, - CLocalDef((Loc.tag na), extern false scopes vars bd, + CLocalDef(CAst.make na, extern false scopes vars bd, Option.map (extern false scopes vars) ty) :: l) | GLocalAssum (na,bk,ty) -> @@ -996,21 +996,21 @@ 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.tag na)::nal,k,ty')::l) + CLocalAssum(CAst.make na::nal,k,ty')::l) | (assums,ids,l) -> (na::assums,na::ids, - CLocalAssum([(Loc.tag na)],Default bk,ty) :: l)) + CLocalAssum([CAst.make na],Default bk,ty) :: l)) | GLocalPattern ((p,_),_,bk,ty) -> let ty = if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in let p = mkCPatOr (List.map (extern_cases_pattern vars) p) in let (assums,ids,l) = extern_local_binder scopes vars l in - (assums,ids, CLocalPattern(Loc.tag @@ (p,ty)) :: l) + (assums,ids, CLocalPattern(CAst.make @@ (p,ty)) :: l) and extern_eqn inctx scopes vars (loc,(ids,pll,c)) = let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in - Loc.tag ?loc (pll,extern inctx scopes vars c) + make ?loc (pll,extern inctx scopes vars c) and extern_notation (tmp_scope,scopes as allscopes) vars t = function | [] -> raise No_match diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 694bec897..d03aa3552 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -9,6 +9,7 @@ open Pp open CErrors open Util +open CAst open Names open Nameops open Namegen @@ -328,8 +329,8 @@ let impls_term_list ?(args = []) = in aux [] (* Check if in binder "(x1 x2 .. xn : t)", none of x1 .. xn-1 occurs in t *) -let rec check_capture ty = function - | (loc,Name id)::(_,Name id')::_ when occur_glob_constr id ty -> +let rec check_capture ty = let open CAst in function + | { loc; v = Name id } :: { v = Name id' } :: _ when occur_glob_constr id ty -> raise (InternalizationError (loc,VariableCapture (id,id'))) | _::nal -> check_capture ty nal @@ -360,22 +361,23 @@ let check_hidden_implicit_parameters ?loc id impls = strbrk "the type of a constructor shall use a different name.") let push_name_env ?(global_level=false) ntnvars implargs env = + let open CAst in function - | loc,Anonymous -> + | { loc; v = Anonymous } -> if global_level then user_err ?loc (str "Anonymous variables not allowed"); env - | loc,Name id -> + | { loc; v = Name id } -> check_hidden_implicit_parameters ?loc 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.tmp_scope,env.scopes) ntnvars; - if global_level then Dumpglob.dump_definition (loc,id) true "var" + if global_level then Dumpglob.dump_definition CAst.(make ?loc id) true "var" 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 ntnvars - env (loc, na) b b' t ty = + env {loc;v=na} b b' t ty = let ids = (match na with Anonymous -> fun x -> x | Name na -> Id.Set.add na) env.ids in let ty, ids' = if t then ty, ids else @@ -385,11 +387,11 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars 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 (l, x) -> push_name_env ~global_level ntnvars (Variable,[],[],[])(*?*) env (l, Name x)) + (fun env {loc;v=x} -> push_name_env ~global_level ntnvars (Variable,[],[],[])(*?*) env (make ?loc @@ Name x)) env fvs in let bl = List.map - (fun (loc, id) -> - (loc, (Name id, b, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None)))) + CAst.(map (fun id -> + (Name id, b, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None)))) fvs in let na = match na with @@ -404,7 +406,7 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars in Implicit_quantifiers.make_fresh ids' (Global.env ()) id in Name name | _ -> na - in (push_name_env ~global_level ntnvars (impls_type_list ty')(*?*) env' (loc,na)), (loc,(na,b',ty')) :: List.rev bl + in (push_name_env ~global_level ntnvars (impls_type_list ty')(*?*) env' (make ?loc na)), (make ?loc (na,b',ty')) :: List.rev bl let intern_assumption intern ntnvars env nal bk ty = let intern_type env = intern (set_type_scope env) in @@ -414,9 +416,9 @@ let intern_assumption intern ntnvars env nal bk ty = check_capture ty nal; let impls = impls_type_list ty in List.fold_left - (fun (env, bl) (loc, na as locna) -> + (fun (env, bl) ({loc;v=na} as locna) -> (push_name_env ntnvars impls env locna, - (Loc.tag ?loc (na,k,locate_if_hole ?loc na ty))::bl)) + (make ?loc (na,k,locate_if_hole ?loc na ty))::bl)) (env, []) nal | Generalized (b,b',t) -> let env, b = intern_generalized_binder intern_type ntnvars env (List.hd nal) b b' t ty in @@ -434,7 +436,7 @@ let glob_local_binder_of_extended = DAst.with_loc_val (fun ?loc -> function let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd") -let intern_letin_binder intern ntnvars env ((loc,na as locna),def,ty) = +let intern_letin_binder intern ntnvars env (({loc;v=na} as locna),def,ty) = let term = intern env def in let ty = Option.map (intern env) ty in (push_name_env ntnvars (impls_term_list term) env locna, @@ -448,22 +450,22 @@ let intern_cases_pattern_as_binder ?loc ntnvars env p = user_err ?loc (str "Unsupported nested \"as\" clause."); il,disjpat in - let env = List.fold_right (fun (loc,id) env -> push_name_env ntnvars (Variable,[],[],[]) env (loc,Name id)) il env in + let env = List.fold_right (fun {loc;v=id} env -> push_name_env ntnvars (Variable,[],[],[]) env (make ?loc @@ Name id)) il env in let na = alias_of_pat (List.hd disjpat) in let ienv = Name.fold_right Id.Set.remove na env.ids in let id = Namegen.next_name_away_with_default "pat" na ienv in - let na = (loc, Name id) in + let na = make ?loc @@ Name id in env,((disjpat,il),id),na let intern_local_binder_aux ?(global_level=false) intern ntnvars (env,bl) = function | CLocalAssum(nal,bk,ty) -> let env, bl' = intern_assumption intern ntnvars env nal bk ty in - let bl' = List.map (fun (loc,(na,c,t)) -> DAst.make ?loc @@ GLocalAssum (na,c,t)) bl' in + let bl' = List.map (fun {loc;v=(na,c,t)} -> DAst.make ?loc @@ GLocalAssum (na,c,t)) bl' in env, bl' @ bl - | CLocalDef((loc,na as locna),def,ty) -> + | CLocalDef( {loc; v=na} as locna,def,ty) -> let env,(na,bk,def,ty) = intern_letin_binder intern ntnvars env (locna,def,ty) in env, (DAst.make ?loc @@ GLocalDef (na,bk,def,ty)) :: bl - | CLocalPattern (loc,(p,ty)) -> + | CLocalPattern {loc;v=(p,ty)} -> let tyc = match ty with | Some ty -> ty @@ -472,8 +474,8 @@ let intern_local_binder_aux ?(global_level=false) intern ntnvars (env,bl) = func let env, ((disjpat,il),id),na = intern_cases_pattern_as_binder ?loc ntnvars env p in let bk = Default Explicit in let _, bl' = intern_assumption intern ntnvars env [na] bk tyc in - let _,(_,bk,t) = List.hd bl' in - (env, (DAst.make ?loc @@ GLocalPattern((disjpat,List.map snd il),id,bk,t)) :: bl) + let {v=(_,bk,t)} = List.hd bl' in + (env, (DAst.make ?loc @@ GLocalPattern((disjpat,List.map (fun x -> x.v) il),id,bk,t)) :: bl) let intern_generalization intern env ntnvars loc bk ak c = let c = intern {env with unb = true} c in @@ -495,16 +497,16 @@ let intern_generalization intern env ntnvars loc bk ak c = | None -> false in if pi then - (fun (loc', id) acc -> + (fun {loc=loc';v=id} acc -> DAst.make ?loc:(Loc.merge_opt loc' loc) @@ GProd (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc)) else - (fun (loc', id) acc -> + (fun {loc=loc';v=id} acc -> DAst.make ?loc:(Loc.merge_opt loc' loc) @@ GLambda (Name id, bk, DAst.make ?loc:loc' @@ GHole (Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), acc)) in - List.fold_right (fun (loc, id as lid) (env, acc) -> - let env' = push_name_env ntnvars (Variable,[],[],[]) env (loc, Name id) in + List.fold_right (fun ({loc;v=id} as lid) (env, acc) -> + let env' = push_name_env ntnvars (Variable,[],[],[]) env CAst.(make @@ Name id) in (env', abs lid acc)) fvs (env,c) in c' @@ -571,7 +573,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in let pat, na = match disjpat with | [pat] when is_var store pat -> let na = get () in None, na - | _ -> Some ((List.map snd ids,disjpat),id), snd na in + | _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na.v in (renaming,env), pat, na with Not_found -> try @@ -581,7 +583,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam if onlyident then (* Do not try to interpret a variable as a constructor *) let na = out_var pat in - let env = push_name_env ntnvars (Variable,[],[],[]) env (pat.CAst.loc, na) in + let env = push_name_env ntnvars (Variable,[],[],[]) env (make ?loc:pat.loc na) in (renaming,env), None, na else (* Interpret as a pattern *) @@ -589,7 +591,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam let pat, na = match disjpat with | [pat] when is_var store pat -> let na = get () in None, na - | _ -> Some ((List.map snd ids,disjpat),id), snd na in + | _ -> Some ((List.map (fun x -> x.v) ids,disjpat),id), na.v in (renaming,env), pat, na with Not_found -> (* Binders not bound in the notation do not capture variables *) @@ -601,7 +603,7 @@ let traverse_binder intern_pat ntnvars (terms,_,binders,_ as subst) avoid (renam (renaming',env), None, Name id' type binder_action = -| AddLetIn of Name.t Loc.located * constr_expr * constr_expr option +| AddLetIn of Misctypes.lname * constr_expr * constr_expr option | AddTermIter of (constr_expr * subscopes) Names.Id.Map.t | AddPreBinderIter of Id.t * local_binder_expr (* A binder to be internalized *) | AddBinderIter of Id.t * extended_glob_local_binder (* A binder already internalized - used for generalized binders *) @@ -692,7 +694,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = let knd = match knd with | Evar_kinds.BinderType (Name id as na) -> let na = - try snd (coerce_to_name (fst (Id.Map.find id terms))) + try (coerce_to_name (fst (Id.Map.find id terms))).v with Not_found -> try Name (Id.Map.find id renaming) with Not_found -> na @@ -800,7 +802,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = into a substitution for interpretation and based on binding/constr distinction *) -let cases_pattern_of_name (loc,na) = +let cases_pattern_of_name {loc;v=na} = let atom = match na with Name id -> Some (Ident (loc,id)) | Anonymous -> None in CAst.make ?loc (CPatAtom atom) @@ -898,7 +900,7 @@ let intern_var env (ltacvars,ntnvars) namedctx loc id us = try let ty,expl_impls,impls,argsc = Id.Map.find id env.impls in let expl_impls = List.map - (fun id -> CAst.make ?loc @@ CRef (Ident (loc,id),None), Some (loc,ExplByName id)) expl_impls in + (fun id -> CAst.make ?loc @@ CRef (Ident (loc,id),None), Some (make ?loc @@ ExplByName id)) expl_impls in let tys = string_of_ty ty in Dumpglob.dump_reference ?loc "<>" (Id.to_string id) tys; gvar (loc,id) us, make_implicits_list impls, argsc, expl_impls @@ -958,7 +960,7 @@ let check_no_explicitation l = match l with | [] -> () | (_, None) :: _ -> assert false - | (_, Some (loc, _)) :: _ -> + | (_, Some {loc}) :: _ -> user_err ?loc (str"Unexpected explicitation of the argument of an abbreviation.") let dump_extended_global loc = function @@ -1034,7 +1036,8 @@ let intern_non_secvar_qualid loc qid intern env ntnvars us args = | GRef (VarRef _, _) -> raise Not_found | _ -> r -let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args = function +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 @@ -1069,11 +1072,11 @@ let interp_reference vars r = (** Private internalization patterns *) type 'a raw_cases_pattern_expr_r = - | RCPatAlias of 'a raw_cases_pattern_expr * Name.t Loc.located + | RCPatAlias of 'a raw_cases_pattern_expr * Misctypes.lname | RCPatCstr of Globnames.global_reference * 'a raw_cases_pattern_expr list * 'a raw_cases_pattern_expr list (** [RCPatCstr (loc, c, l1, l2)] represents ((@c l1) l2) *) - | RCPatAtom of (Id.t Loc.located * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option + | RCPatAtom of (Misctypes.lident * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option | RCPatOr of 'a raw_cases_pattern_expr list and 'a raw_cases_pattern_expr = ('a raw_cases_pattern_expr_r, 'a) DAst.t @@ -1133,7 +1136,7 @@ let check_number_of_pattern loc n l = if not (Int.equal n p) then raise (InternalizationError (loc,BadPatternsNumber (n,p))) let check_or_pat_variables loc ids idsl = - if List.exists (fun ids' -> not (List.eq_set (fun (loc,id) (_,id') -> Id.equal id id') ids ids')) idsl then + if List.exists (fun ids' -> not (List.eq_set (fun {loc;v=id} {v=id'} -> Id.equal id id') ids ids')) idsl then user_err ?loc (str "The components of this disjunctive pattern must bind the same variables.") @@ -1372,7 +1375,7 @@ let sort_fields ~complete loc fields completer = (** {6 Manage multiple aliases} *) type alias = { - alias_ids : Id.t Loc.located list; + alias_ids : Misctypes.lident list; alias_map : Id.t Id.Map.t; } @@ -1383,20 +1386,20 @@ let empty_alias = { (* [merge_aliases] returns the sets of all aliases encountered at this point and a substitution mapping extra aliases to the first one *) -let merge_aliases aliases (loc,na) = +let merge_aliases aliases {loc;v=na} = match na with | Anonymous -> aliases | Name id -> - let alias_ids = aliases.alias_ids @ [loc,id] in + let alias_ids = aliases.alias_ids @ [make ?loc id] in let alias_map = match aliases.alias_ids with | [] -> aliases.alias_map - | (_,id') :: _ -> Id.Map.add id id' aliases.alias_map + | {v=id'} :: _ -> Id.Map.add id id' aliases.alias_map in { alias_ids; alias_map; } let alias_of als = match als.alias_ids with | [] -> Anonymous -| (_,id) :: _ -> Name id +| {v=id} :: _ -> Name id (** {6 Expanding notations } @@ -1426,7 +1429,7 @@ let product_of_cases_patterns aliases idspl = let rec subst_pat_iterator y t = DAst.(map (function | RCPatAtom id as p -> - begin match id with Some ((_,x),_) when Id.equal x y -> DAst.get t | _ -> p end + begin match id with Some ({v=x},_) when Id.equal x y -> DAst.get t | _ -> p end | RCPatCstr (id,l1,l2) -> RCPatCstr (id,List.map (subst_pat_iterator y t) l1, List.map (subst_pat_iterator y t) l2) @@ -1456,7 +1459,7 @@ let drop_notations_pattern looked_for genv = in (** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *) let rec rcp_of_glob scopes x = DAst.(map (function - | GVar id -> RCPatAtom (Some ((x.CAst.loc,id),scopes)) + | GVar id -> RCPatAtom (Some (CAst.make ?loc:x.loc id,scopes)) | GHole (_,_,_) -> RCPatAtom (None) | GRef (g,_) -> RCPatCstr (g,[],[]) | GApp (r, l) -> @@ -1562,7 +1565,7 @@ let drop_notations_pattern looked_for genv = begin match drop_syndef top scopes id [] with | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr (a, b, c) - | None -> DAst.make ?loc @@ RCPatAtom (Some ((loc,find_pattern_variable id),scopes)) + | None -> DAst.make ?loc @@ RCPatAtom (Some ((make ?loc @@ find_pattern_variable id),scopes)) end | CPatAtom None -> DAst.make ?loc @@ RCPatAtom None | CPatOr pl -> DAst.make ?loc @@ RCPatOr (List.map (in_pat top scopes) pl) @@ -1592,7 +1595,7 @@ let drop_notations_pattern looked_for genv = 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 DAst.make ?loc @@ RCPatAtom (Some ((loc,id),scopes)) else + if Id.equal id ldots_var then DAst.make ?loc @@ RCPatAtom (Some ((make ?loc id),scopes)) else anomaly (str "Unbound pattern notation variable: " ++ Id.print id ++ str ".") end | NRef g -> @@ -1632,7 +1635,7 @@ let rec intern_pat genv ntnvars aliases pat = let pl' = List.map (fun (asubst,pl) -> (asubst, DAst.make ?loc @@ PatCstr (c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in ids',pl' in - let loc = CAst.(pat.loc) in + let loc = pat.loc in match DAst.get pat with | RCPatAlias (p, id) -> let aliases' = merge_aliases aliases id in @@ -1649,8 +1652,8 @@ let rec intern_pat genv ntnvars 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 (Some ((loc,id),scopes)) -> - let aliases = merge_aliases aliases (loc,Name id) in + | RCPatAtom (Some ({loc;v=id},scopes)) -> + let aliases = merge_aliases aliases (make ?loc @@ Name id) in set_var_scope ?loc id false scopes ntnvars; (aliases.alias_ids,[aliases.alias_map, DAst.make ?loc @@ PatVar (alias_of aliases)]) (* TO CHECK: aura-t-on id? *) | RCPatAtom (None) -> @@ -1696,12 +1699,12 @@ let intern_ind_pattern genv ntnvars scopes pat = let merge_impargs l args = let test x = function - | (_, Some (_, y)) -> explicitation_eq x y + | (_, Some {v=y}) -> explicitation_eq x y | _ -> false in List.fold_right (fun a l -> match a with - | (_,Some (_,(ExplByName id as x))) when + | (_, Some {v=ExplByName id as x}) when List.exists (test x) args -> l | _ -> a::l) l args @@ -1733,7 +1736,7 @@ let extract_explicit_arg imps args = let (eargs,rargs) = aux l in match e with | None -> (eargs,a::rargs) - | Some (loc,pos) -> + | Some {loc;v=pos} -> let id = match pos with | ExplByName id -> if not (exists_implicit_name id imps) then @@ -1772,8 +1775,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = in apply_impargs c env imp subscopes l loc - | CFix ((locid,iddef), dl) -> - let lf = List.map (fun ((_, id),_,_,_,_) -> id) dl in + | CFix ({ CAst.loc = locid; v = iddef}, dl) -> + let lf = List.map (fun ({CAst.v = id},_,_,_,_) -> id) dl in let dl = Array.of_list dl in let n = try List.index0 Id.equal iddef lf @@ -1808,7 +1811,7 @@ let internalize globalenv env pattern_mode (_, 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.tag @@ Name name)) 0 env' lf in + en (CAst.make @@ Name name)) 0 env' lf in (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in DAst.make ?loc @@ GRec (GFix @@ -1817,8 +1820,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = Array.map (fun (_,bl,_,_) -> bl) idl, Array.map (fun (_,_,ty,_) -> ty) idl, Array.map (fun (_,_,_,bd) -> bd) idl) - | CCoFix ((locid,iddef), dl) -> - let lf = List.map (fun ((_, id),_,_,_) -> id) dl in + | CCoFix ({ CAst.loc = locid; v = iddef }, dl) -> + let lf = List.map (fun ({CAst.v = id},_,_,_) -> id) dl in let dl = Array.of_list dl in let n = try List.index0 Id.equal iddef lf @@ -1826,7 +1829,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = raise (InternalizationError (locid,UnboundFixName (true,iddef))) in let idl_tmp = Array.map - (fun ((loc,id),bl,ty,_) -> + (fun ({ CAst.loc; v = id },bl,ty,_) -> let (env',rbl) = List.fold_left intern_local_binder (env,[]) bl in (List.rev (List.map glob_local_binder_of_extended rbl), intern_type env' ty,env')) dl in @@ -1835,7 +1838,7 @@ let internalize globalenv env pattern_mode (_, 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.tag @@ Name name)) 0 env' lf in + en (CAst.make @@ Name name)) 0 env' lf in (b,c,intern {env'' with tmp_scope = None} bd)) dl idl_tmp in DAst.make ?loc @@ GRec (GCoFix n, @@ -1856,7 +1859,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let inc1 = intern (reset_tmp_scope env) c1 in let int = Option.map (intern_type env) t in DAst.make ?loc @@ - GLetIn (snd na, inc1, int, + GLetIn (na.CAst.v, inc1, int, intern (push_name_env ntnvars (impls_term_list inc1) env na) c2) | CNotation ("- _", ([a],[],[],[])) when is_non_zero a -> let p = match a.CAst.v with CPrim (Numeral (p, _)) -> p | _ -> assert false in @@ -1919,7 +1922,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | 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_right Id.Set.add y acc) acc na) + (Option.fold_left (fun acc { CAst.v = y } -> Name.fold_right Id.Set.add y acc) acc na) inb) Id.Set.empty tms in (* as, in & return vars *) let forbidden_vars = Option.cata free_vars_of_constr_expr as_in_vars rtnpo in @@ -1929,7 +1932,7 @@ let internalize globalenv env pattern_mode (_, 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.tag @@ Name var)) + (fun var bli -> push_name_env ntnvars (Variable,[],[],[]) bli (CAst.make @@ 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 = @@ -1969,17 +1972,17 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = 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.tag na') in + (CAst.make na') in intern_type env'' u) po in DAst.make ?loc @@ - GLetTuple (List.map snd nal, (na', p'), b', + GLetTuple (List.map (fun { CAst.v } -> v) nal, (na', p'), b', intern (List.fold_left (push_name_env ntnvars (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c) | CIf (c, (na,po), b1, b2) -> 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.tag na') in + (CAst.make na') in intern_type env'' p) po in DAst.make ?loc @@ GIf (c', (na', p'), intern env b1, intern env b2) @@ -2063,10 +2066,10 @@ let internalize globalenv env pattern_mode (_, 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;v=(lhs,rhs)} = let eqn_ids,pll = intern_disjunctive_multiple_pattern env loc n lhs in (* Linearity implies the order in ids is irrelevant *) - let eqn_ids = List.map snd eqn_ids in + let eqn_ids = List.map (fun x -> x.v) eqn_ids in check_linearity lhs eqn_ids; let env_ids = List.fold_right Id.Set.add eqn_ids env.ids in List.map (fun (asubst,pl) -> @@ -2081,10 +2084,10 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let extra_id,na = let loc = tm'.CAst.loc in match DAst.get tm', na with - | GVar id, None when not (Id.Map.mem id (snd lvar)) -> Some id,(loc,Name id) - | GRef (VarRef id, _), None -> Some id,(loc,Name id) - | _, None -> None,(Loc.tag Anonymous) - | _, Some (loc,na) -> None,(loc,na) in + | GVar id, None when not (Id.Map.mem id (snd lvar)) -> Some id, CAst.make ?loc @@ Name id + | GRef (VarRef id, _), None -> Some id, CAst.make ?loc @@ Name id + | _, None -> None, CAst.make Anonymous + | _, Some ({ CAst.loc; v = na } as lna) -> None, lna in (* the "in" part *) let match_td,typ = match t with | Some t -> @@ -2100,8 +2103,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let (match_to_do,nal) = 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, DAst.make ?loc @@ PatVar x) :: l in + | { CAst.v = Anonymous } -> l + | { CAst.loc; v = (Name y as x) } -> (y, DAst.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 -> @@ -2113,7 +2116,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = | PatVar x -> let loc = c.CAst.loc in canonize_args t tt forbidden_names - (add_name match_acc (loc,x)) ((loc,x)::var_acc) + (add_name match_acc CAst.(make ?loc x)) ((loc,x)::var_acc) | _ -> let fresh = Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names (EConstr.of_constr ty) in @@ -2127,7 +2130,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = 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 + (tm',(na.CAst.v,typ)), extra_id, match_td and intern_impargs c env l subscopes args = let eargs, rargs = extract_explicit_arg l args in @@ -2169,7 +2172,6 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = in aux 1 l subscopes eargs rargs 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 diff --git a/interp/constrintern.mli b/interp/constrintern.mli index f09b17a49..7411fb84b 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -87,7 +87,7 @@ val intern_gen : typing_constraint -> env -> constr_expr -> glob_constr val intern_pattern : env -> cases_pattern_expr -> - Id.t Loc.located list * (Id.t Id.Map.t * cases_pattern) list + lident list * (Id.t Id.Map.t * cases_pattern) list val intern_context : bool -> env -> internalization_env -> local_binder_expr list -> internalization_env * glob_decl list diff --git a/interp/declare.ml b/interp/declare.ml index 72cdabfd2..dfa84f278 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -561,7 +561,7 @@ let do_universe poly l = (str"Cannot declare polymorphic universes outside sections") in let l = - List.map (fun (l, id) -> + List.map (fun {CAst.v=id} -> let lev = Universes.new_univ_id () in (id, lev)) l in diff --git a/interp/declare.mli b/interp/declare.mli index f368d164e..9bec32d29 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -85,6 +85,6 @@ val declare_univ_binders : Globnames.global_reference -> Universes.universe_bind val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit -val do_universe : polymorphic -> Id.t Loc.located list -> unit +val do_universe : polymorphic -> Misctypes.lident list -> unit val do_constraint : polymorphic -> (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list -> unit diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index d7962e29a..e439db2b2 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -249,12 +249,12 @@ let dump_def ?loc ty secpath id = Option.iter (fun loc -> dump_string (Printf.sprintf "%s %d:%d %s %s\n" ty bl el secpath id) ) loc -let dump_definition (loc, id) sec s = +let dump_definition {CAst.loc;v=id} sec s = dump_def ?loc s (Names.DirPath.to_string (Lib.current_dirpath sec)) (Names.Id.to_string id) -let dump_constraint (((loc, n),_), _, _) sec ty = +let dump_constraint (({ CAst.loc; v = n },_), _, _) sec ty = match n with - | Names.Name id -> dump_definition (loc, id) sec ty + | Names.Name id -> dump_definition CAst.(make ?loc id) sec ty | Names.Anonymous -> () let dump_moddef ?loc mp ty = diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index f3ad50f28..c779e860f 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -25,7 +25,7 @@ val continue : unit -> unit val add_glob : ?loc:Loc.t -> Globnames.global_reference -> unit val add_glob_kn : ?loc:Loc.t -> Names.KerName.t -> unit -val dump_definition : Names.Id.t Loc.located -> bool -> string -> unit +val dump_definition : Misctypes.lident -> bool -> string -> unit val dump_moddef : ?loc:Loc.t -> Names.ModPath.t -> string -> unit val dump_modref : ?loc:Loc.t -> Names.ModPath.t -> string -> unit val dump_reference : ?loc:Loc.t -> string -> string -> string -> unit diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index a838d7106..326969b67 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -26,7 +26,7 @@ module RelDecl = Context.Rel.Declaration let generalizable_table = Summary.ref Id.Pred.empty ~name:"generalizable-ident" -let declare_generalizable_ident table (loc,id) = +let declare_generalizable_ident table {CAst.loc;v=id} = if not (Id.equal id (root_of_id id)) then user_err ?loc ~hdr:"declare_generalizable_ident" ((Id.print id ++ str @@ -49,7 +49,7 @@ let cache_generalizable_type (_,(local,cmd)) = let load_generalizable_type _ (_,(local,cmd)) = generalizable_table := add_generalizable cmd !generalizable_table -let in_generalizable : bool * Id.t Loc.located list option -> obj = +let in_generalizable : bool * Misctypes.lident list option -> obj = declare_object {(default_object "GENERALIZED-IDENT") with load_function = load_generalizable_type; cache_function = cache_generalizable_type; @@ -99,7 +99,7 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = in aux bound l c let ids_of_names l = - List.fold_left (fun acc x -> match snd x with Name na -> na :: acc | Anonymous -> acc) [] l + List.fold_left (fun acc x -> match x.CAst.v with Name na -> na :: acc | Anonymous -> acc) [] l let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr list) = let rec aux bdvars l c = match c with @@ -109,7 +109,7 @@ let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr li aux (Id.Set.union (ids_of_list bound) bdvars) l' tl | ((CLocalDef (n, c, t)) :: tl) -> - let bound = match snd n with Anonymous -> [] | Name n -> [n] in + let bound = match n.CAst.v with Anonymous -> [] | Name n -> [n] in let l' = free_vars_of_constr_expr c ~bound:bdvars l in let l'' = Option.fold_left (fun l t -> free_vars_of_constr_expr t ~bound:bdvars l) l' t in aux (Id.Set.union (ids_of_list bound) bdvars) l'' tl @@ -123,13 +123,13 @@ let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.emp | GVar id -> let loc = c.CAst.loc in if is_freevar bound (Global.env ()) id then - if Id.List.mem_assoc_sym id vs then vs - else (Loc.tag ?loc id) :: vs + if List.exists (fun {CAst.v} -> Id.equal v id) vs then vs + else CAst.(make ?loc id) :: vs else vs | _ -> 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 (loc, id) -> + List.iter (fun {CAst.loc;v=id} -> if not (Id.Set.mem id allowed || find_generalizable_ident id) then ungeneralizable loc id) vars; vars @@ -146,7 +146,7 @@ let combine_params avoid fn applied needed = let named, applied = List.partition (function - (t, Some (loc, ExplByName id)) -> + (t, Some {CAst.loc;v=ExplByName id}) -> let is_id (_, decl) = match RelDecl.get_name decl with | Name id' -> Id.equal id id' | Anonymous -> false @@ -157,7 +157,7 @@ let combine_params avoid fn applied needed = | _ -> false) applied in let named = List.map - (fun x -> match x with (t, Some (loc, ExplByName id)) -> id, t | _ -> assert false) + (fun x -> match x with (t, Some {CAst.loc;v=ExplByName id}) -> id, t | _ -> assert false) named in let is_unset (_, decl) = match decl with @@ -198,23 +198,23 @@ let destClassApp cl = 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) + | CApp ((None, { v = CRef (ref, inst) }), l) -> CAst.make ?loc (ref, List.map fst l, inst) + | CAppExpl ((None, ref, inst), l) -> CAst.make ?loc (ref, l, inst) + | CRef (ref, inst) -> CAst.make ?loc:(loc_of_reference ref) (ref, [], inst) | _ -> raise Not_found let destClassAppExpl cl = 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) + | CApp ((None, { v = CRef (ref, inst) } ), l) -> CAst.make ?loc (ref, l, inst) + | CRef (ref, inst) -> CAst.make ?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 ({CAst.v=(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 @@ -222,7 +222,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 ({CAst.loc;v=(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 diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index bfe73160b..625e12003 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -6,18 +6,17 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Loc open Names open Glob_term open Constrexpr open Libnames open Globnames -val declare_generalizable : Vernacexpr.locality_flag -> (Id.t located) list option -> unit +val declare_generalizable : Vernacexpr.locality_flag -> Misctypes.lident list option -> unit val ids_of_list : Id.t list -> Id.Set.t -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 +val destClassApp : constr_expr -> (reference * constr_expr list * instance_expr option) CAst.t +val destClassAppExpl : constr_expr -> (reference * (constr_expr * explicitation CAst.t option) list * instance_expr option) CAst.t (** Fragile, should be used only for construction a set of identifiers to avoid *) @@ -31,7 +30,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 located list + glob_constr -> Misctypes.lident list val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t diff --git a/interp/reserve.ml b/interp/reserve.ml index 04710282f..3e1a7dd9b 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -84,7 +84,7 @@ let in_reserved : Id.t * notation_constr -> obj = declare_object {(default_object "RESERVED-TYPE") with cache_function = cache_reserved_type } -let declare_reserved_type_binding (loc,id) t = +let declare_reserved_type_binding {CAst.loc;v=id} t = if not (Id.equal id (root_of_id id)) then user_err ?loc ~hdr:"declare_reserved_type" ((Id.print id ++ str diff --git a/interp/reserve.mli b/interp/reserve.mli index 4fcef23c5..5899cd628 100644 --- a/interp/reserve.mli +++ b/interp/reserve.mli @@ -6,9 +6,8 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Loc open Names open Notation_term -val declare_reserved_type : Id.t located list -> notation_constr -> unit +val declare_reserved_type : Misctypes.lident list -> notation_constr -> unit val find_reserved_type : Id.t -> notation_constr diff --git a/interp/stdarg.mli b/interp/stdarg.mli index ed00fe296..ea1c63b89 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -41,7 +41,7 @@ val wit_intro_pattern : (constr_expr intro_pattern_expr located, glob_constr_and val wit_ident : Id.t uniform_genarg_type -val wit_var : (Id.t located, Id.t located, Id.t) genarg_type +val wit_var : (lident, lident, Id.t) genarg_type val wit_ref : (reference, global_reference located or_var, global_reference) genarg_type @@ -76,7 +76,7 @@ val wit_red_expr : (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type -val wit_clause_dft_concl : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type +val wit_clause_dft_concl : (lident Locus.clause_expr, lident Locus.clause_expr, Names.Id.t Locus.clause_expr) genarg_type (** Aliases for compatibility *) @@ -84,7 +84,7 @@ val wit_integer : int uniform_genarg_type val wit_preident : string uniform_genarg_type val wit_reference : (reference, global_reference located or_var, global_reference) genarg_type val wit_global : (reference, global_reference located or_var, global_reference) genarg_type -val wit_clause : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type +val wit_clause : (lident Locus.clause_expr, lident Locus.clause_expr, Names.Id.t Locus.clause_expr) genarg_type val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type val wit_intropattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type val wit_redexpr : diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 9fc02461e..66d87707c 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Loc open Names open Constrexpr @@ -15,7 +14,7 @@ val asymmetric_patterns : bool ref [@@ocaml.deprecated "use Constrexpr_ops.asymmetric_patterns"] (** Utilities on constr_expr *) -val split_at_annot : local_binder_expr list -> Id.t located option -> local_binder_expr list * local_binder_expr list +val split_at_annot : local_binder_expr list -> Misctypes.lident option -> local_binder_expr list * local_binder_expr list [@@ocaml.deprecated "use Constrexpr_ops.split_at_annot"] val ntn_loc : ?loc:Loc.t -> constr_notation_substitution -> string -> (int * int) list -- cgit v1.2.3