diff options
95 files changed, 799 insertions, 755 deletions
diff --git a/dev/ci/user-overlays/06745-ejgallego-located+vernac.sh b/dev/ci/user-overlays/06745-ejgallego-located+vernac.sh new file mode 100644 index 000000000..d1d61fec2 --- /dev/null +++ b/dev/ci/user-overlays/06745-ejgallego-located+vernac.sh @@ -0,0 +1,13 @@ +if [ "$CI_PULL_REQUEST" = "6745" ] || [ "$CI_BRANCH" = "located+vernac" ]; then + ltac2_CI_BRANCH=located+vernac + ltac2_CI_GITURL=https://github.com/ejgallego/ltac2 + + Equations_CI_BRANCH=located+vernac + Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations + + fiat_parsers_CI_BRANCH=located+vernac + fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat + + Elpi_CI_BRANCH=located+vernac + Elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi.git +fi diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 16a31790a..ab78b0956 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -49,6 +49,14 @@ We changed the type of the following functions: a functional way. The old style of passing `evar_map`s as references is not supported anymore. +Changes in the abstract syntax tree: + +- The practical totality of the AST has been nodified using + `CAst.t`. This means that all objects coming from parsing will be + indeed wrapped in a `CAst.t`. `Loc.located` is on its way to + deprecation. Some minor interfaces changes have resulted from + this. + We have changed the representation of the following types: - `Lib.object_prefix` is now a record instead of a nested tuple. diff --git a/engine/evd.ml b/engine/evd.ml index 0e9472158..2142cee37 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -802,7 +802,7 @@ let make_evar_universe_context e l = | None -> uctx | Some us -> List.fold_left - (fun uctx (loc,id) -> + (fun uctx { CAst.loc; v = id } -> fst (UState.new_univ_variable ?loc univ_rigid (Some id) uctx)) uctx us diff --git a/engine/evd.mli b/engine/evd.mli index b28ce2a62..84fa70ef2 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -506,7 +506,7 @@ val constrain_variables : Univ.LSet.t -> UState.t -> UState.t val evar_universe_context_of_binders : Universes.universe_binders -> UState.t -val make_evar_universe_context : env -> (Id.t located) list option -> UState.t +val make_evar_universe_context : env -> Misctypes.lident list option -> UState.t val restrict_universe_context : evar_map -> Univ.LSet.t -> evar_map (** Raises Not_found if not a name for a universe in this map. *) val universe_of_name : evar_map -> Id.t -> Univ.Level.t diff --git a/engine/uState.ml b/engine/uState.ml index 4b650c9c9..625495866 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -282,7 +282,7 @@ let pr_uctx_level uctx l = Libnames.pr_reference (reference_of_level uctx l) type universe_decl = - (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl + (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl let error_unbound_universes left uctx = let open Univ in @@ -305,7 +305,7 @@ let universe_context ~names ~extensible uctx = let levels = ContextSet.levels uctx.uctx_local in let newinst, left = List.fold_right - (fun (loc,id) (newinst, acc) -> + (fun { CAst.loc; v = id } (newinst, acc) -> let l = try UNameMap.find id (fst uctx.uctx_names) with Not_found -> assert false @@ -325,7 +325,7 @@ let check_universe_context_set ~names ~extensible uctx = if extensible then () else let open Univ in - let left = List.fold_left (fun left (loc,id) -> + let left = List.fold_left (fun left { CAst.loc; v = id } -> let l = try UNameMap.find id (fst uctx.uctx_names) with Not_found -> assert false diff --git a/engine/uState.mli b/engine/uState.mli index 6657d6047..5c85b2b84 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -132,7 +132,7 @@ val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst val normalize : t -> t type universe_decl = - (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl + (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl (** [check_univ_decl ctx decl] diff --git a/engine/universes.ml b/engine/universes.ml index 3a00f0fd1..f3660a559 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -92,14 +92,14 @@ let register_universe_binders ref ubinders = if not (Id.Map.is_empty ubinders) then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders)) -type univ_name_list = Name.t Loc.located list +type univ_name_list = Misctypes.lname list let universe_binders_with_opt_names ref levels = function | None -> universe_binders_of_global ref | Some udecl -> if Int.equal(List.length levels) (List.length udecl) then - List.fold_left2 (fun acc (_,na) lvl -> match na with + List.fold_left2 (fun acc { CAst.v = na} lvl -> match na with | Anonymous -> acc | Name na -> Names.Id.Map.add na lvl acc) empty_binders udecl levels diff --git a/engine/universes.mli b/engine/universes.mli index cb6e2ba1b..04586a6f8 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -35,7 +35,7 @@ val empty_binders : universe_binders val register_universe_binders : Globnames.global_reference -> universe_binders -> unit val universe_binders_of_global : Globnames.global_reference -> universe_binders -type univ_name_list = Name.t Loc.located list +type univ_name_list = Misctypes.lname list (** [universe_binders_with_opt_names ref u l] 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 diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml index c59828794..5b51953bb 100644 --- a/intf/constrexpr.ml +++ b/intf/constrexpr.ml @@ -46,7 +46,7 @@ type prim_token = type instance_expr = Misctypes.glob_level list type cases_pattern_expr_r = - | CPatAlias of cases_pattern_expr * Name.t Loc.located + | CPatAlias of cases_pattern_expr * lname | CPatCstr of reference * cases_pattern_expr list option * cases_pattern_expr list (** [CPatCstr (_, c, Some l1, l2)] represents (@c l1) l2 *) @@ -68,14 +68,14 @@ and cases_pattern_notation_substitution = and constr_expr_r = | CRef of reference * instance_expr option - | CFix of Id.t Loc.located * fix_expr list - | CCoFix of Id.t Loc.located * cofix_expr list + | CFix of lident * fix_expr list + | CCoFix of lident * cofix_expr list | CProdN of local_binder_expr list * constr_expr | CLambdaN of local_binder_expr list * constr_expr - | CLetIn of Name.t Loc.located * constr_expr * constr_expr option * constr_expr + | CLetIn of lname * constr_expr * constr_expr option * constr_expr | CAppExpl of (proj_flag * reference * instance_expr option) * constr_expr list | CApp of (proj_flag * constr_expr) * - (constr_expr * explicitation Loc.located option) list + (constr_expr * explicitation CAst.t option) list | CRecord of (reference * constr_expr) list (* representation of the "let" and "match" constructs *) @@ -84,9 +84,9 @@ and constr_expr_r = * case_expr list * branch_expr list (* branches *) - | CLetTuple of Name.t Loc.located list * (Name.t Loc.located option * constr_expr option) * + | CLetTuple of lname list * (lname option * constr_expr option) * constr_expr * constr_expr - | CIf of constr_expr * (Name.t Loc.located option * constr_expr option) + | CIf of constr_expr * (lname option * constr_expr option) * constr_expr * constr_expr | CHole of Evar_kinds.t option * intro_pattern_naming_expr * Genarg.raw_generic_argument option | CPatVar of patvar @@ -101,18 +101,18 @@ and constr_expr_r = and constr_expr = constr_expr_r CAst.t and case_expr = constr_expr (* expression that is being matched *) - * Name.t Loc.located option (* as-clause *) + * lname option (* as-clause *) * cases_pattern_expr option (* in-clause *) and branch_expr = - (cases_pattern_expr list list * constr_expr) Loc.located + (cases_pattern_expr list list * constr_expr) CAst.t and fix_expr = - Id.t Loc.located * (Id.t Loc.located option * recursion_order_expr) * + lident * (lident option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr and cofix_expr = - Id.t Loc.located * local_binder_expr list * constr_expr * constr_expr + lident * local_binder_expr list * constr_expr * constr_expr and recursion_order_expr = | CStructRec @@ -121,9 +121,9 @@ and recursion_order_expr = (** Anonymous defs allowed ?? *) and local_binder_expr = - | CLocalAssum of Name.t Loc.located list * binder_kind * constr_expr - | CLocalDef of Name.t Loc.located * constr_expr * constr_expr option - | CLocalPattern of (cases_pattern_expr * constr_expr option) Loc.located + | CLocalAssum of lname list * binder_kind * constr_expr + | CLocalDef of lname * constr_expr * constr_expr option + | CLocalPattern of (cases_pattern_expr * constr_expr option) CAst.t and constr_notation_substitution = constr_expr list * (** for constr subterms *) diff --git a/intf/genredexpr.ml b/intf/genredexpr.ml index a8c37c620..bdf3242ca 100644 --- a/intf/genredexpr.ml +++ b/intf/genredexpr.ml @@ -8,8 +8,6 @@ (** Reduction expressions *) -open Names - (** The parsing produces initially a list of [red_atom] *) type 'a red_atom = @@ -52,7 +50,7 @@ type ('a,'b,'c) red_expr_gen = type ('a,'b,'c) may_eval = | ConstrTerm of 'a | ConstrEval of ('a,'b,'c) red_expr_gen * 'a - | ConstrContext of Id.t Loc.located * 'a + | ConstrContext of Misctypes.lident * 'a | ConstrTypeOf of 'a open Libnames diff --git a/intf/misctypes.ml b/intf/misctypes.ml index 33e961419..aafd61b3c 100644 --- a/intf/misctypes.ml +++ b/intf/misctypes.ml @@ -8,7 +8,13 @@ open Names -(** Basic types used both in [constr_expr] and in [glob_constr] *) +(** Basic types used both in [constr_expr], [glob_constr], and [vernacexpr] *) + +(** Located identifiers and objects with syntax. *) + +type lident = Id.t CAst.t +type lname = Name.t CAst.t +type lstring = string CAst.t (** Cases pattern variables *) @@ -101,9 +107,9 @@ type 'a with_bindings = 'a * 'a bindings type 'a or_var = | ArgArg of 'a - | ArgVar of Names.Id.t Loc.located + | ArgVar of lident -type 'a and_short_name = 'a * Id.t Loc.located option +type 'a and_short_name = 'a * lident option type 'a or_by_notation = | AN of 'a @@ -134,7 +140,7 @@ type multi = type 'a core_destruction_arg = | ElimOnConstr of 'a - | ElimOnIdent of Id.t Loc.located + | ElimOnIdent of lident | ElimOnAnonHyp of int type 'a destruction_arg = diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index d16c9bb80..ba28eacea 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -6,19 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Loc open Names open Misctypes open Constrexpr -open Decl_kinds open Libnames (** Vernac expressions, produced by the parser *) - -type lident = Id.t located -type lname = Name.t located -type lstring = string located - type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation (* spiwack: I'm choosing, for now, to have [goal_selector] be a @@ -40,7 +33,8 @@ type goal_reference = | NthGoal of int | GoalId of Id.t -type univ_name_list = Name.t Loc.located list +type univ_name_list = Universes.univ_name_list +[@@ocaml.deprecated "Use [Universes.univ_name_list]"] type printable = | PrintTables @@ -56,7 +50,7 @@ type printable = | PrintMLLoadPath | PrintMLModules | PrintDebugGC - | PrintName of reference or_by_notation * univ_name_list option + | PrintName of reference or_by_notation * Universes.univ_name_list option | PrintGraph | PrintClasses | PrintTypeClasses @@ -72,7 +66,7 @@ type printable = | PrintScopes | PrintScope of string | PrintVisibility of string option - | PrintAbout of reference or_by_notation * univ_name_list option * goal_selector option + | PrintAbout of reference or_by_notation * Universes.univ_name_list option * goal_selector option | PrintImplicit of reference or_by_notation | PrintAssumptions of bool * bool * reference or_by_notation | PrintStrategy of reference or_by_notation option @@ -164,7 +158,7 @@ type option_ref_value = (** Identifier and optional list of bound universes and constraints. *) -type universe_decl_expr = (Id.t Loc.located list, glob_constraint list) gen_universe_decl +type universe_decl_expr = (lident list, glob_constraint list) gen_universe_decl type ident_decl = lident * universe_decl_expr option type name_decl = lname * universe_decl_expr option @@ -177,7 +171,7 @@ type definition_expr = * constr_expr option type fixpoint_expr = - ident_decl * (Id.t located option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr option + ident_decl * (lident option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr option type cofixpoint_expr = ident_decl * local_binder_expr list * constr_expr * constr_expr option @@ -205,7 +199,7 @@ type inductive_expr = type one_inductive_expr = ident_decl * local_binder_expr list * constr_expr option * constructor_expr list -type typeclass_constraint = name_decl * binding_kind * constr_expr +type typeclass_constraint = name_decl * Decl_kinds.binding_kind * constr_expr and typeclass_context = typeclass_constraint list @@ -221,7 +215,7 @@ type syntax_modifier = | SetOnlyParsing | SetOnlyPrinting | SetCompatVersion of Flags.compat_version - | SetFormat of string * string located + | SetFormat of string * lstring type proof_end = | Admitted @@ -321,7 +315,7 @@ type vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit type vernac_argument_status = { name : Name.t; recarg_like : bool; - notation_scope : string Loc.located option; + notation_scope : string CAst.t option; implicit_status : vernac_implicit_status; } @@ -341,15 +335,15 @@ type nonrec vernac_expr = | VernacNotationAddFormat of string * string * string (* Gallina *) - | VernacDefinition of (discharge * definition_object_kind) * name_decl * definition_expr - | VernacStartTheoremProof of theorem_kind * proof_expr list + | VernacDefinition of (Decl_kinds.discharge * Decl_kinds.definition_object_kind) * name_decl * definition_expr + | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list | VernacEndProof of proof_end | VernacExactProof of constr_expr - | VernacAssumption of (discharge * assumption_object_kind) * + | VernacAssumption of (Decl_kinds.discharge * Decl_kinds.assumption_object_kind) * inline * (ident_decl list * constr_expr) with_coercion list - | VernacInductive of cumulative_inductive_parsing_flag * private_flag * inductive_flag * (inductive_expr * decl_notation list) list - | VernacFixpoint of discharge * (fixpoint_expr * decl_notation list) list - | VernacCoFixpoint of discharge * (cofixpoint_expr * decl_notation list) list + | VernacInductive of cumulative_inductive_parsing_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list + | VernacFixpoint of Decl_kinds.discharge * (fixpoint_expr * decl_notation list) list + | VernacCoFixpoint of Decl_kinds.discharge * (cofixpoint_expr * decl_notation list) list | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list | VernacUniverse of lident list @@ -416,7 +410,7 @@ type nonrec vernac_expr = | VernacCreateHintDb of string * bool | VernacRemoveHints of string list * reference list | VernacHints of string list * hints_expr - | VernacSyntacticDefinition of Id.t located * (Id.t list * constr_expr) * + | VernacSyntacticDefinition of lident * (Id.t list * constr_expr) * onlyparsing_flag | VernacDeclareImplicits of reference or_by_notation * (explicitation * bool * bool) list list @@ -482,8 +476,8 @@ type vernac_control = | VernacExpr of vernac_flag list * vernac_expr (* boolean is true when the `-time` batch-mode command line flag was set. the flag is used to print differently in `-time` vs `Time foo` *) - | VernacTime of bool * vernac_control located - | VernacRedirect of string * vernac_control located + | VernacTime of bool * vernac_control CAst.t + | VernacRedirect of string * vernac_control CAst.t | VernacTimeout of int * vernac_control | VernacFail of vernac_control diff --git a/library/declaremods.ml b/library/declaremods.ml index 28a04252a..291039d19 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -451,7 +451,7 @@ let intern_arg interp_modast (acc, cst) (idl,(typ,ann)) = let env = Global.env () in let sobjs = get_module_sobjs false env inl mty in let mp0 = get_module_path mty in - let fold acc (_, id) = + let fold acc {CAst.v=id} = let dir = DirPath.make [id] in let mbid = MBId.make lib_dir id in let mp = MPbound mbid in @@ -982,8 +982,7 @@ type 'modast module_interpretor = Entries.module_struct_entry * Misctypes.module_kind * Univ.ContextSet.t type 'modast module_params = - (Id.t Loc.located list * ('modast * inline)) list - + (lident list * ('modast * inline)) list (** {6 Debug} *) diff --git a/library/declaremods.mli b/library/declaremods.mli index 0df55f34d..db2893376 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -16,7 +16,7 @@ type 'modast module_interpretor = Entries.module_struct_entry * Misctypes.module_kind * Univ.ContextSet.t type 'modast module_params = - (Id.t Loc.located list * ('modast * inline)) list + (Misctypes.lident list * ('modast * inline)) list (** [declare_module interp_modast id fargs typ exprs] declares module [id], with structure constructed by [interp_modast] diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index a3d257154..cad837d08 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -226,7 +226,7 @@ type _ target = type prod_info = production_level * production_position type (_, _) entry = -| TTName : ('self, Name.t Loc.located) entry +| TTName : ('self, Misctypes.lname) entry | TTReference : ('self, reference) entry | TTBigint : ('self, Constrexpr.raw_natural_number) entry | TTConstr : prod_info * 'r target -> ('r, 'r) entry @@ -308,7 +308,7 @@ let interp_entry forpat e = match e with | ETProdBinderList ETBinderOpen -> TTAny TTOpenBinderList | ETProdBinderList (ETBinderClosed tkl) -> TTAny (TTClosedBinderList tkl) -let cases_pattern_expr_of_name (loc,na) = CAst.make ?loc @@ match na with +let cases_pattern_expr_of_name { CAst.loc; v = na } = CAst.make ?loc @@ match na with | Anonymous -> CPatAtom None | Name id -> CPatAtom (Some (Ident (Loc.tag ?loc id))) diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 9f12db649..8a1e6d121 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -36,21 +36,21 @@ let mk_cast = function let loc = Loc.merge_opt (constr_loc c) (constr_loc ty) in CAst.make ?loc @@ CCast(c, CastConv ty) -let binder_of_name expl (loc,na) = - CLocalAssum ([loc, na], Default expl, +let binder_of_name expl { CAst.loc = loc; v = na } = + CLocalAssum ([CAst.make ?loc na], Default expl, CAst.make ?loc @@ CHole (Some (Evar_kinds.BinderType na), IntroAnonymous, None)) let binders_of_names l = List.map (binder_of_name Explicit) l -let mk_fixb (id,bl,ann,body,(loc,tyc)) = +let mk_fixb (id,bl,ann,body,(loc,tyc)) : fix_expr = let ty = match tyc with Some ty -> ty | None -> CAst.make @@ CHole (None, IntroAnonymous, None) in (id,ann,bl,ty,body) -let mk_cofixb (id,bl,ann,body,(loc,tyc)) = - let _ = Option.map (fun (aloc,_) -> +let mk_cofixb (id,bl,ann,body,(loc,tyc)) : cofix_expr = + let _ = Option.map (fun { CAst.loc = aloc } -> CErrors.user_err ?loc:aloc ~hdr:"Constr:mk_cofixb" (Pp.str"Annotation forbidden in cofix expression.")) (fst ann) in @@ -61,10 +61,10 @@ let mk_cofixb (id,bl,ann,body,(loc,tyc)) = let mk_fix(loc,kw,id,dcls) = if kw then - let fb = List.map mk_fixb dcls in + let fb : fix_expr list = List.map mk_fixb dcls in CAst.make ~loc @@ CFix(id,fb) else - let fb = List.map mk_cofixb dcls in + let fb : cofix_expr list = List.map mk_cofixb dcls in CAst.make ~loc @@ CCoFix(id,fb) let mk_single_fix (loc,kw,dcl) = @@ -131,7 +131,7 @@ GEXTEND Gram [ [ id = Prim.ident -> id ] ] ; Prim.name: - [ [ "_" -> Loc.tag ~loc:!@loc Anonymous ] ] + [ [ "_" -> CAst.make ~loc:!@loc Anonymous ] ] ; global: [ [ r = Prim.reference -> r ] ] @@ -196,8 +196,9 @@ GEXTEND Gram | "10" LEFTA [ f=operconstr; args=LIST1 appl_arg -> CAst.make ~loc:(!@loc) @@ CApp((None,f),args) | "@"; f=global; i = instance; args=LIST0 NEXT -> CAst.make ~loc:!@loc @@ CAppExpl((None,f,i),args) - | "@"; (locid,id) = pattern_identref; args=LIST1 identref -> - let args = List.map (fun x -> CAst.make @@ CRef (Ident x,None), None) args in + | "@"; lid = pattern_identref; args=LIST1 identref -> + let { CAst.loc = locid; v = id } = lid in + let args = List.map (fun x -> CAst.make @@ CRef (Ident Loc.(tag ?loc:x.CAst.loc x.CAst.v), None), None) args in CAst.make ~loc:(!@loc) @@ CApp((None, CAst.make ?loc:locid @@ CPatVar id),args) ] | "9" [ ".."; c = operconstr LEVEL "0"; ".." -> @@ -256,11 +257,11 @@ GEXTEND Gram Option.map (mkCProdN ?loc:(fst ty) bl) (snd ty), c2) | "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" -> let fixp = mk_single_fix fx in - let (li,id) = match fixp.CAst.v with + let { CAst.loc = li; v = id } = match fixp.CAst.v with CFix(id,_) -> id | CCoFix(id,_) -> id | _ -> assert false in - CAst.make ~loc:!@loc @@ CLetIn((li,Name id),fixp,None,c) + CAst.make ~loc:!@loc @@ CLetIn( CAst.make ?loc:li @@ Name id,fixp,None,c) | "let"; lb = ["("; l=LIST0 name SEP ","; ")" -> l | "()" -> []]; po = return_type; ":="; c1 = operconstr LEVEL "200"; "in"; @@ -269,17 +270,17 @@ GEXTEND Gram | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> CAst.make ~loc:!@loc @@ - CCases (LetPatternStyle, None, [c1, None, None], [Loc.tag ~loc:!@loc ([[p]], c2)]) + CCases (LetPatternStyle, None, [c1, None, None], [CAst.make ~loc:!@loc ([[p]], c2)]) | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; rt = case_type; "in"; c2 = operconstr LEVEL "200" -> CAst.make ~loc:!@loc @@ - CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [Loc.tag ~loc:!@loc ([[p]], c2)]) + CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [CAst.make ~loc:!@loc ([[p]], c2)]) | "let"; "'"; p=pattern; "in"; t = pattern LEVEL "200"; ":="; c1 = operconstr LEVEL "200"; rt = case_type; "in"; c2 = operconstr LEVEL "200" -> CAst.make ~loc:!@loc @@ - CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [Loc.tag ~loc:!@loc ([[p]], c2)]) + CCases (LetPatternStyle, Some rt, [c1, aliasvar p, Some t], [CAst.make ~loc:!@loc ([[p]], c2)]) | "if"; c=operconstr LEVEL "200"; po = return_type; "then"; b1=operconstr LEVEL "200"; "else"; b2=operconstr LEVEL "200" -> @@ -288,7 +289,7 @@ GEXTEND Gram ; appl_arg: [ [ id = lpar_id_coloneq; c=lconstr; ")" -> - (c,Some (Loc.tag ~loc:!@loc @@ ExplByName id)) + (c,Some (CAst.make ~loc:!@loc @@ ExplByName id)) | c=operconstr LEVEL "9" -> (c,None) ] ] ; atomic_constr: @@ -368,7 +369,7 @@ GEXTEND Gram ; eqn: [ [ pll = LIST1 mult_pattern SEP "|"; - "=>"; rhs = lconstr -> (Loc.tag ~loc:!@loc (pll,rhs)) ] ] + "=>"; rhs = lconstr -> (CAst.make ~loc:!@loc (pll,rhs)) ] ] ; record_pattern: [ [ id = global; ":="; pat = pattern -> (id, pat) ] ] @@ -420,7 +421,8 @@ GEXTEND Gram (fun na -> CLocalAssum (na::nal,Default Implicit,c)) | nal=LIST1 name; "}" -> (fun na -> CLocalAssum (na::nal,Default Implicit, - CAst.make ?loc:(Loc.merge_opt (fst na) (Some !@loc)) @@ CHole (Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None))) + CAst.make ?loc:(Loc.merge_opt na.CAst.loc (Some !@loc)) @@ + CHole (Some (Evar_kinds.BinderType na.CAst.v), IntroAnonymous, None))) | ":"; c=lconstr; "}" -> (fun na -> CLocalAssum ([na],Default Implicit,c)) ] ] @@ -433,7 +435,7 @@ GEXTEND Gram ] ] ; impl_name_head: - [ [ id = impl_ident_head -> (Loc.tag ~loc:!@loc @@ Name id) ] ] + [ [ id = impl_ident_head -> (CAst.make ~loc:!@loc @@ Name id) ] ] ; binders_fixannot: [ [ na = impl_name_head; assum = impl_ident_tail; bl = binders_fixannot -> @@ -453,7 +455,7 @@ GEXTEND Gram | id = name; idl = LIST0 name; bl = binders -> binders_of_names (id::idl) @ bl | id1 = name; ".."; id2 = name -> - [CLocalAssum ([id1;(Loc.tag ~loc:!@loc (Name ldots_var));id2], + [CLocalAssum ([id1;(CAst.make ~loc:!@loc (Name ldots_var));id2], Default Explicit, CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, None))] | bl = closed_binder; bl' = binders -> bl@bl' @@ -495,17 +497,17 @@ GEXTEND Gram | CPatCast (p, ty) -> (p, Some ty) | _ -> (p, None) in - [CLocalPattern (Loc.tag ~loc:!@loc (p, ty))] + [CLocalPattern (CAst.make ~loc:!@loc (p, ty))] ] ] ; typeclass_constraint: - [ [ "!" ; c = operconstr LEVEL "200" -> (Loc.tag ~loc:!@loc Anonymous), true, c + [ [ "!" ; c = operconstr LEVEL "200" -> (CAst.make ~loc:!@loc Anonymous), true, c | "{"; id = name; "}"; ":" ; expl = [ "!" -> true | -> false ] ; c = operconstr LEVEL "200" -> id, expl, c | iid=name_colon ; expl = [ "!" -> true | -> false ] ; c = operconstr LEVEL "200" -> - (Loc.tag ~loc:!@loc iid), expl, c + (CAst.make ~loc:!@loc iid), expl, c | c = operconstr LEVEL "200" -> - (Loc.tag ~loc:!@loc Anonymous), false, c + (CAst.make ~loc:!@loc Anonymous), false, c ] ] ; diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 891c232ee..0b7efe739 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -43,13 +43,13 @@ GEXTEND Gram [ [ LEFTQMARK; id = ident -> id ] ] ; pattern_identref: - [ [ id = pattern_ident -> Loc.tag ~loc:!@loc id ] ] + [ [ id = pattern_ident -> CAst.make ~loc:!@loc id ] ] ; var: (* as identref, but interpret as a term identifier in ltac *) - [ [ id = ident -> Loc.tag ~loc:!@loc id ] ] + [ [ id = ident -> CAst.make ~loc:!@loc id ] ] ; identref: - [ [ id = ident -> Loc.tag ~loc:!@loc id ] ] + [ [ id = ident -> CAst.make ~loc:!@loc id ] ] ; field: [ [ s = FIELD -> Id.of_string s ] ] @@ -70,8 +70,8 @@ GEXTEND Gram ] ] ; name: - [ [ IDENT "_" -> Loc.tag ~loc:!@loc Anonymous - | id = ident -> Loc.tag ~loc:!@loc @@ Name id ] ] + [ [ IDENT "_" -> CAst.make ~loc:!@loc Anonymous + | id = ident -> CAst.make ~loc:!@loc @@ Name id ] ] ; reference: [ [ id = ident; (l,id') = fields -> @@ -95,7 +95,7 @@ GEXTEND Gram ] ] ; ne_lstring: - [ [ s = ne_string -> Loc.tag ~loc:!@loc s ] ] + [ [ s = ne_string -> CAst.make ~loc:!@loc s ] ] ; dirpath: [ [ id = ident; l = LIST0 field -> @@ -105,7 +105,7 @@ GEXTEND Gram [ [ s = STRING -> s ] ] ; lstring: - [ [ s = string -> (Loc.tag ~loc:!@loc s) ] ] + [ [ s = string -> (CAst.make ~loc:!@loc s) ] ] ; integer: [ [ i = INT -> my_int_of_string (!@loc) i diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index 1c3ba7837..482373150 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -29,7 +29,7 @@ GEXTEND Gram ; command: [ [ IDENT "Goal"; c = lconstr -> - VernacDefinition (Decl_kinds.(NoDischarge, Definition), ((Loc.tag ~loc:!@loc Names.Anonymous), None), ProveBody ([], c)) + VernacDefinition (Decl_kinds.(NoDischarge, Definition), ((CAst.make ~loc:!@loc Names.Anonymous), None), ProveBody ([], c)) | IDENT "Proof" -> VernacProof (None,None) | IDENT "Proof" ; IDENT "Mode" ; mn = string -> VernacProofMode mn | IDENT "Proof"; c = lconstr -> VernacExactProof c diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index d90fd3eb7..93e534e0b 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -115,7 +115,7 @@ GEXTEND Gram ; located_vernac: - [ [ v = vernac_control -> Loc.tag ~loc:!@loc v ] ] + [ [ v = vernac_control -> CAst.make ~loc:!@loc v ] ] ; END @@ -134,7 +134,7 @@ let test_plural_form_types loc kwd = function | _ -> () let lname_of_lident : lident -> lname = - Loc.map (fun s -> Name s) + CAst.map (fun s -> Name s) let name_of_ident_decl : ident_decl -> name_decl = on_fst lname_of_lident @@ -629,12 +629,12 @@ GEXTEND Gram VernacCanonical (ByNotation ntn) | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body -> let s = coerce_reference_to_id qid in - VernacDefinition ((NoDischarge,CanonicalStructure),((Loc.tag (Name s)),None),d) + VernacDefinition ((NoDischarge,CanonicalStructure),((CAst.make (Name s)),None),d) (* Coercions *) | IDENT "Coercion"; qid = global; d = def_body -> let s = coerce_reference_to_id qid in - VernacDefinition ((NoDischarge,Coercion),((Loc.tag (Name s)),None),d) + VernacDefinition ((NoDischarge,Coercion),((CAst.make (Name s)),None),d) | IDENT "Identity"; IDENT "Coercion"; f = identref; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> VernacIdentityCoercion (f, s, t) @@ -745,7 +745,7 @@ GEXTEND Gram ; argument_spec: [ [ b = OPT "!"; id = name ; s = OPT scope -> - snd id, not (Option.is_empty b), Option.map (fun x -> Loc.tag ~loc:!@loc x) s + id.CAst.v, not (Option.is_empty b), Option.map (fun x -> CAst.make ~loc:!@loc x) s ] ]; (* List of arguments implicit status, scope, modifiers *) @@ -758,7 +758,7 @@ GEXTEND Gram | "/" -> [`Slash] | "("; items = LIST1 argument_spec; ")"; sc = OPT scope -> let f x = match sc, x with - | None, x -> x | x, None -> Option.map (fun y -> Loc.tag ~loc:!@loc y) x + | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc:!@loc y) x | Some _, Some _ -> user_err Pp.(str "scope declared twice") in List.map (fun (name,recarg_like,notation_scope) -> `Id { name=name; recarg_like=recarg_like; @@ -766,7 +766,7 @@ GEXTEND Gram implicit_status = NotImplicit}) items | "["; items = LIST1 argument_spec; "]"; sc = OPT scope -> let f x = match sc, x with - | None, x -> x | x, None -> Option.map (fun y -> Loc.tag ~loc:!@loc y) x + | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc:!@loc y) x | Some _, Some _ -> user_err Pp.(str "scope declared twice") in List.map (fun (name,recarg_like,notation_scope) -> `Id { name=name; recarg_like=recarg_like; @@ -774,7 +774,7 @@ GEXTEND Gram implicit_status = Implicit}) items | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope -> let f x = match sc, x with - | None, x -> x | x, None -> Option.map (fun y -> Loc.tag ~loc:!@loc y) x + | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc:!@loc y) x | Some _, Some _ -> user_err Pp.(str "scope declared twice") in List.map (fun (name,recarg_like,notation_scope) -> `Id { name=name; recarg_like=recarg_like; @@ -784,11 +784,11 @@ GEXTEND Gram ]; (* Same as [argument_spec_block], but with only implicit status and names *) more_implicits_block: [ - [ name = name -> [(snd name, Vernacexpr.NotImplicit)] + [ name = name -> [(name.CAst.v, Vernacexpr.NotImplicit)] | "["; items = LIST1 name; "]" -> - List.map (fun name -> (snd name, Vernacexpr.Implicit)) items + List.map (fun name -> (name.CAst.v, Vernacexpr.Implicit)) items | "{"; items = LIST1 name; "}" -> - List.map (fun name -> (snd name, Vernacexpr.MaximallyImplicit)) items + List.map (fun name -> (name.CAst.v, Vernacexpr.MaximallyImplicit)) items ] ]; strategy_level: @@ -800,9 +800,9 @@ GEXTEND Gram ; instance_name: [ [ name = ident_decl; sup = OPT binders -> - (let ((loc,id),l) = name in ((loc, Name id),l)), + (CAst.map (fun id -> Name id) (fst name), snd name), (Option.default [] sup) - | -> ((Loc.tag ~loc:!@loc Anonymous), None), [] ] ] + | -> ((CAst.make ~loc:!@loc Anonymous), None), [] ] ] ; hint_info: [ [ "|"; i = OPT natural; pat = OPT constr_pattern -> @@ -1134,8 +1134,8 @@ GEXTEND Gram | IDENT "Reserved"; IDENT "Infix"; s = ne_lstring; l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] -> - let (loc,s) = s in - VernacSyntaxExtension (true,((loc,"x '"^s^"' y"),l)) + let s = CAst.map (fun s -> "x '"^s^"' y") s in + VernacSyntaxExtension (true,(s,l)) | IDENT "Reserved"; IDENT "Notation"; s = ne_lstring; @@ -1166,10 +1166,10 @@ GEXTEND Gram | IDENT "only"; IDENT "parsing" -> SetOnlyParsing | IDENT "compat"; s = STRING -> SetCompatVersion (parse_compat_version s) - | IDENT "format"; s1 = [s = STRING -> Loc.tag ~loc:!@loc s]; - s2 = OPT [s = STRING -> Loc.tag ~loc:!@loc s] -> + | IDENT "format"; s1 = [s = STRING -> CAst.make ~loc:!@loc s]; + s2 = OPT [s = STRING -> CAst.make ~loc:!@loc s] -> begin match s1, s2 with - | (_,k), Some s -> SetFormat(k,s) + | { CAst.v = k }, Some s -> SetFormat(k,s) | s, None -> SetFormat ("text",s) end | x = IDENT; ","; l = LIST1 [id = IDENT -> id ] SEP ","; "at"; lev = level -> SetItemLevel (x::l,lev) diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index accb51366..f36250176 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -192,17 +192,17 @@ module Prim : open Libnames val preident : string Gram.entry val ident : Id.t Gram.entry - val name : Name.t located Gram.entry - val identref : Id.t located Gram.entry + val name : lname Gram.entry + val identref : lident Gram.entry val ident_decl : ident_decl Gram.entry val pattern_ident : Id.t Gram.entry - val pattern_identref : Id.t located Gram.entry + val pattern_identref : lident Gram.entry val base_ident : Id.t Gram.entry val natural : int Gram.entry val bigint : Constrexpr.raw_natural_number Gram.entry val integer : int Gram.entry val string : string Gram.entry - val lstring : string located Gram.entry + val lstring : lstring Gram.entry val qualid : qualid located Gram.entry val fullyqualid : Id.t list located Gram.entry val reference : reference Gram.entry @@ -210,8 +210,8 @@ module Prim : val smart_global : reference or_by_notation Gram.entry val dirpath : DirPath.t Gram.entry val ne_string : string Gram.entry - val ne_lstring : string located Gram.entry - val var : Id.t located Gram.entry + val ne_lstring : lstring Gram.entry + val var : lident Gram.entry end module Constr : @@ -233,10 +233,10 @@ module Constr : val binder : local_binder_expr list Gram.entry (* closed_binder or variable *) val binders : local_binder_expr list Gram.entry (* list of binder *) val open_binders : local_binder_expr list Gram.entry - val binders_fixannot : (local_binder_expr list * (Id.t located option * recursion_order_expr)) Gram.entry - val typeclass_constraint : (Name.t located * bool * constr_expr) Gram.entry + val binders_fixannot : (local_binder_expr list * (lident option * recursion_order_expr)) Gram.entry + val typeclass_constraint : (lname * bool * constr_expr) Gram.entry val record_declaration : constr_expr Gram.entry - val appl_arg : (constr_expr * explicitation located option) Gram.entry + val appl_arg : (constr_expr * explicitation CAst.t option) Gram.entry end module Module : diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 693ab464d..22881c32c 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1295,7 +1295,7 @@ let rec rebuild_return_type rt = CAst.make ?loc @@ Constrexpr.CProdN(n,rebuild_return_type t') | Constrexpr.CLetIn(na,v,t,t') -> CAst.make ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t') - | _ -> CAst.make ?loc @@ Constrexpr.CProdN([Constrexpr.CLocalAssum ([Loc.tag Anonymous], + | _ -> CAst.make ?loc @@ Constrexpr.CProdN([Constrexpr.CLocalAssum ([CAst.make Anonymous], Constrexpr.Default Decl_kinds.Explicit, rt)], CAst.make @@ Constrexpr.CSort(GType [])) @@ -1351,12 +1351,12 @@ let do_build_inductive (fun (n,t,typ) acc -> match typ with | Some typ -> - CAst.make @@ Constrexpr.CLetIn((Loc.tag n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, + CAst.make @@ Constrexpr.CLetIn((CAst.make n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ), acc) | None -> CAst.make @@ Constrexpr.CProdN - ([Constrexpr.CLocalAssum([(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t)], + ([Constrexpr.CLocalAssum([CAst.make n],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t)], acc ) ) @@ -1418,12 +1418,12 @@ let do_build_inductive (fun (n,t,typ) acc -> match typ with | Some typ -> - CAst.make @@ Constrexpr.CLetIn((Loc.tag n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, + CAst.make @@ Constrexpr.CLetIn((CAst.make n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ), acc) | None -> CAst.make @@ Constrexpr.CProdN - ([Constrexpr.CLocalAssum([(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t)], + ([Constrexpr.CLocalAssum([CAst.make n],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t)], acc ) ) @@ -1450,18 +1450,18 @@ let do_build_inductive (fun (n,t,typ) -> match typ with | Some typ -> - Constrexpr.CLocalDef((Loc.tag n), Constrextern.extern_glob_constr Id.Set.empty t, + Constrexpr.CLocalDef((CAst.make n), Constrextern.extern_glob_constr Id.Set.empty t, Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ)) | None -> Constrexpr.CLocalAssum - ([(Loc.tag n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t) + ([(CAst.make n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t) ) rels_params in let ext_rels_constructors = Array.map (List.map (fun (id,t) -> - false,((Loc.tag id), + false,((CAst.make id), with_full_print (Constrextern.extern_glob_type Id.Set.empty) ((* zeta_normalize *) (alpha_rt rel_params_ids t)) ) @@ -1469,7 +1469,7 @@ let do_build_inductive (rel_constructors) in let rel_ind i ext_rel_constructors = - (((Loc.tag @@ relnames.(i)), None), + (((CAst.make @@ relnames.(i)), None), rel_params, Some rel_arities.(i), ext_rel_constructors),[] diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 96e4a94d3..e19fc9b62 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -155,7 +155,7 @@ let build_newrecursive let sigma = Evd.from_env env0 in let (rec_sign,rec_impls) = List.fold_left - (fun (env,impls) (((_,recname),_),bl,arityc,_) -> + (fun (env,impls) (({CAst.v=recname},_),bl,arityc,_) -> let arityc = Constrexpr_ops.mkCProdN bl arityc in let arity,ctx = Constrintern.interp_type env0 sigma arityc in let evd = Evd.from_env env0 in @@ -344,7 +344,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error is_general do_built (fix_rec_l:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) recdefs interactive_proof (continue_proof : int -> Names.Constant.t array -> EConstr.constr array -> int -> Tacmach.tactic) : unit = - let names = List.map (function (((_, name),_),_,_,_,_),_ -> name) fix_rec_l in + let names = List.map (function (({CAst.v=name},_),_,_,_,_),_ -> name) fix_rec_l in let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in let funs_args = List.map fst fun_bodies in let funs_types = List.map (function ((_,_,_,types,_),_) -> types) fix_rec_l in @@ -365,7 +365,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error f_R_mut) in let fname_kn (((fname,_),_,_,_,_),_) = - let f_ref = Ident fname in + let f_ref = Ident CAst.(with_loc_val (fun ?loc n -> (loc,n)) fname) in locate_with_msg (pr_reference f_ref++str ": Not an inductive type!") locate_constant @@ -404,7 +404,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = match fixpoint_exprl with - | [(((_,fname),pl),_,bl,ret_type,body),_] when not is_rec -> + | [(({CAst.v=fname},pl),_,bl,ret_type,body),_] when not is_rec -> let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in ComDefinition.do_definition ~program_mode:false @@ -413,7 +413,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ())); let evd,rev_pconstants = List.fold_left - (fun (evd,l) ((((_,fname),_),_,_,_,_),_) -> + (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) -> let evd,c = Evd.fresh_global (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in @@ -430,7 +430,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp ComFixpoint.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl; let evd,rev_pconstants = List.fold_left - (fun (evd,l) ((((_,fname),_),_,_,_,_),_) -> + (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) -> let evd,c = Evd.fresh_global (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in @@ -460,7 +460,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas let rec_arg_num = let names = List.map - snd + CAst.(with_val (fun x -> x)) (Constrexpr_ops.names_of_local_assums args) in match wf_arg with @@ -476,8 +476,8 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas (None,(Ident (Loc.tag fname)),None) , (List.map (function - | _,Anonymous -> assert false - | _,Name e -> (Constrexpr_ops.mkIdentC e) + | {CAst.v=Anonymous} -> assert false + | {CAst.v=Name e} -> (Constrexpr_ops.mkIdentC e) ) (Constrexpr_ops.names_of_local_assums args) ) @@ -515,7 +515,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas | None -> begin match args with - | [Constrexpr.CLocalAssum ([(_,Name x)],k,t)] -> t,x + | [Constrexpr.CLocalAssum ([{CAst.v=Name x}],k,t)] -> t,x | _ -> error "Recursive argument must be specified" end | Some wf_args -> @@ -525,7 +525,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas (function | Constrexpr.CLocalAssum(l,k,t) -> List.exists - (function (_,Name id) -> Id.equal id wf_args | _ -> false) + (function {CAst.v=Name id} -> Id.equal id wf_args | _ -> false) l | _ -> false ) @@ -546,7 +546,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas let fun_from_mes = let applied_mes = Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC wf_arg]) in - Constrexpr_ops.mkLambdaC ([(Loc.tag @@ Name wf_arg)],Constrexpr_ops.default_binder_kind,wf_arg_type,applied_mes) + Constrexpr_ops.mkLambdaC ([CAst.make @@ Name wf_arg],Constrexpr_ops.default_binder_kind,wf_arg_type,applied_mes) in let wf_rel_from_mes = Constrexpr_ops.mkAppC(Constrexpr_ops.mkRefC ltof,[wf_arg_type;fun_from_mes]) @@ -557,7 +557,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas let a = Names.Id.of_string "___a" in let b = Names.Id.of_string "___b" in Constrexpr_ops.mkLambdaC( - [Loc.tag @@ Name a;Loc.tag @@ Name b], + [CAst.make @@ Name a; CAst.make @@ Name b], Constrexpr.Default Explicit, wf_arg_type, Constrexpr_ops.mkAppC(wf_rel_expr, @@ -592,7 +592,7 @@ and rebuild_nal aux bk bl' nal typ = | _,{ CAst.v = CProdN([],typ) } -> rebuild_nal aux bk bl' nal typ | [], _ -> rebuild_bl aux bl' typ | na::nal,{ CAst.v = CProdN(CLocalAssum(na'::nal',bk',nal't)::rest,typ') } -> - if Name.equal (snd na) (snd na') || Name.is_anonymous (snd na') + if Name.equal (na.CAst.v) (na'.CAst.v) || Name.is_anonymous (na'.CAst.v) then let assum = CLocalAssum([na],bk,nal't) in let new_rest = if nal' = [] then rest else (CLocalAssum(nal',bk',nal't)::rest) in @@ -638,7 +638,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof let _is_struct = match fixpoint_exprl with | [((_,(wf_x,Constrexpr.CWfRec wf_rel),_,_,_),_) as fixpoint_expr] -> - let (((((_,name),pl),_,args,types,body)),_) as fixpoint_expr = + let (((({CAst.v=name},pl),_,args,types,body)),_) as fixpoint_expr = match recompute_binder_list [fixpoint_expr] with | [e] -> e | _ -> assert false @@ -659,10 +659,10 @@ let do_generate_principle pconstants on_error register_built interactive_proof true in if register_built - then register_wf name rec_impls wf_rel (map_option snd wf_x) using_lemmas args types body pre_hook; + then register_wf name rec_impls wf_rel (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook; false |[((_,(wf_x,Constrexpr.CMeasureRec(wf_mes,wf_rel_opt)),_,_,_),_) as fixpoint_expr] -> - let (((((_,name),_),_,args,types,body)),_) as fixpoint_expr = + let (((({CAst.v=name},_),_,args,types,body)),_) as fixpoint_expr = match recompute_binder_list [fixpoint_expr] with | [e] -> e | _ -> assert false @@ -683,7 +683,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof true in if register_built - then register_mes name rec_impls wf_mes wf_rel_opt (map_option snd wf_x) using_lemmas args types body pre_hook; + then register_mes name rec_impls wf_mes wf_rel_opt (map_option (fun x -> x.CAst.v) wf_x) using_lemmas args types body pre_hook; true | _ -> List.iter (function ((_na,(_,ord),_args,_body,_type),_not) -> @@ -696,7 +696,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof fixpoint_exprl; let fixpoint_exprl = recompute_binder_list fixpoint_exprl in let fix_names = - List.map (function ((((_,name),_),_,_,_,_),_) -> name) fixpoint_exprl + List.map (function ((({CAst.v=name},_),_,_,_,_),_) -> name) fixpoint_exprl in (* ok all the expressions are structural *) let recdefs,rec_impls = build_newrecursive fixpoint_exprl in @@ -757,7 +757,7 @@ let rec add_args id new_args = CAst.map (function List.map (fun (b,na,b_option) -> add_args id new_args b, na, b_option) cel, - List.map (fun (loc,(cpl,e)) -> Loc.tag ?loc @@ (cpl,add_args id new_args e)) cal + List.map CAst.(map (fun (cpl,e) -> (cpl,add_args id new_args e))) cal ) | CLetTuple(nal,(na,b_option),b1,b2) -> CLetTuple(nal,(na,Option.map (add_args id new_args) b_option), @@ -875,7 +875,7 @@ let make_graph (f_ref:global_reference) = let l = List.map (fun (id,(n,recexp),bl,t,b) -> - let loc, rec_id = Option.get n in + let { CAst.loc; v=rec_id } = Option.get n in let new_args = List.flatten (List.map @@ -883,7 +883,7 @@ let make_graph (f_ref:global_reference) = | Constrexpr.CLocalDef (na,_,_)-> [] | Constrexpr.CLocalAssum (nal,_,_) -> List.map - (fun (loc,n) -> CAst.make ?loc @@ + (fun {CAst.loc;v=n} -> CAst.make ?loc @@ CRef(Libnames.Ident(loc, Nameops.Name.get_id n),None)) nal | Constrexpr.CLocalPattern _ -> assert false @@ -891,21 +891,21 @@ let make_graph (f_ref:global_reference) = nal_tas ) in - let b' = add_args (snd id) new_args b in - ((((id,None), ( Some (Loc.tag rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) + let b' = add_args id.CAst.v new_args b in + ((((id,None), ( Some CAst.(make rec_id),CStructRec),nal_tas@bl,t,Some b'),[]):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list)) ) fixexprl in l | _ -> let id = Label.to_id (Constant.label c) in - [(((Loc.tag id),None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]] + [((CAst.make id,None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]] in let mp,dp,_ = Constant.repr3 c in do_generate_principle [c,Univ.Instance.empty] error_error false false expr_list; (* We register the infos *) List.iter - (fun ((((_,id),_),_,_,_,_),_) -> add_Function false (Constant.make3 mp dp (Label.of_id id))) + (fun ((({CAst.v=id},_),_,_,_,_),_) -> add_Function false (Constant.make3 mp dp (Label.of_id id))) expr_list) let do_generate_principle = do_generate_principle [] warning_error true diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4 index 7d2c4d082..794a28dd4 100644 --- a/plugins/ltac/coretactics.ml4 +++ b/plugins/ltac/coretactics.ml4 @@ -346,7 +346,7 @@ let () = register_list_tactical "solve" Tacticals.New.tclSOLVE let initial_tacticals () = let idn n = Id.of_string (Printf.sprintf "_%i" n) in - let varn n = Reference (ArgVar (None, idn n)) in + let varn n = Reference (ArgVar (CAst.make (idn n))) in let iter (s, t) = Tacenv.register_ltac false false (Id.of_string s) t in List.iter iter [ "first", TacFun ([Name (idn 0)], TacML (None, (initial_entry "first", [varn 0]))); diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index 4c6d3c2d3..2eb1ef315 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -81,7 +81,7 @@ let pr_int_list_full _prc _prlc _prt l = pr_int_list l let pr_occurrences _prc _prlc _prt l = match l with | ArgArg x -> pr_int_list x - | ArgVar (loc, id) -> Id.print id + | ArgVar { CAst.loc = loc; v=id } -> Id.print id let occurrences_of = function | [] -> NoOccurrences @@ -102,7 +102,7 @@ let int_list_of_VList v = match Value.to_list v with let interp_occs ist gl l = match l with | ArgArg x -> x - | ArgVar (_,id as locid) -> + | ArgVar ({ CAst.v = id } as locid) -> (try int_list_of_VList (Id.Map.find id ist.lfun) with Not_found | CannotCoerceTo _ -> [interp_int ist locid]) let interp_occs ist gl l = @@ -188,7 +188,7 @@ END type 'id gen_place= ('id * hyp_location_flag,unit) location -type loc_place = Id.t Loc.located gen_place +type loc_place = lident gen_place type place = Id.t gen_place let pr_gen_place pr_id = function @@ -199,7 +199,7 @@ let pr_gen_place pr_id = function | HypLocation (id,InHypValueOnly) -> str "in (Value of " ++ pr_id id ++ str ")" -let pr_loc_place _ _ _ = pr_gen_place (fun (_,id) -> Id.print id) +let pr_loc_place _ _ _ = pr_gen_place (fun { CAst.v = id } -> Id.print id) let pr_place _ _ _ = pr_gen_place Id.print let pr_hloc = pr_loc_place () () () @@ -228,11 +228,11 @@ ARGUMENT EXTEND hloc | [ "in" "|-" "*" ] -> [ ConclLocation () ] | [ "in" ident(id) ] -> - [ HypLocation ((Loc.tag id),InHyp) ] + [ HypLocation ((CAst.make id),InHyp) ] | [ "in" "(" "Type" "of" ident(id) ")" ] -> - [ HypLocation ((Loc.tag id),InHypTypeOnly) ] + [ HypLocation ((CAst.make id),InHypTypeOnly) ] | [ "in" "(" "Value" "of" ident(id) ")" ] -> - [ HypLocation ((Loc.tag id),InHypValueOnly) ] + [ HypLocation ((CAst.make id),InHypValueOnly) ] END diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index 00668ddc7..000c3d2fb 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -50,7 +50,7 @@ val lglob : constr_expr Pcoq.Gram.entry type 'id gen_place= ('id * Locus.hyp_location_flag,unit) location -type loc_place = Id.t Loc.located gen_place +type loc_place = lident gen_place type place = Id.t gen_place val wit_hloc : (loc_place, loc_place, place) Genarg.genarg_type @@ -77,6 +77,6 @@ val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry val wit_retroknowledge_field : (Retroknowledge.field, unit, unit) Genarg.genarg_type val wit_in_clause : - (Id.t Loc.located Locus.clause_expr, - Id.t Loc.located Locus.clause_expr, - Id.t Locus.clause_expr) Genarg.genarg_type + (lident Locus.clause_expr, + lident Locus.clause_expr, + Id.t Locus.clause_expr) Genarg.genarg_type diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 286f9d95d..10be8a842 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -71,7 +71,7 @@ END let induction_arg_of_quantified_hyp = function | AnonHyp n -> None,ElimOnAnonHyp n - | NamedHyp id -> None,ElimOnIdent (Loc.tag id) + | NamedHyp id -> None,ElimOnIdent (CAst.make id) (* Versions *_main must come first!! so that "1" is interpreted as a ElimOnAnonHyp and not as a "constr", and "id" is interpreted as a diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 9ef819569..85c9fc5fd 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -37,10 +37,10 @@ let genarg_of_uconstr c = in_gen (rawwit Stdarg.wit_uconstr) c let in_tac tac = in_gen (rawwit Tacarg.wit_ltac) tac let reference_to_id = function - | Libnames.Ident (loc, id) -> (loc, id) + | Libnames.Ident (loc, id) -> CAst.make ?loc id | Libnames.Qualid (loc,_) -> - CErrors.user_err ?loc - (str "This expression should be a simple identifier.") + CErrors.user_err ?loc + (str "This expression should be a simple identifier.") let tactic_mode = Gram.entry_create "vernac:tactic_command" @@ -196,7 +196,7 @@ GEXTEND Gram verbose most of the time. *) fresh_id: [ [ s = STRING -> ArgArg s (*| id = ident -> ArgVar (!@loc,id)*) - | qid = qualid -> let (_pth,id) = Libnames.repr_qualid (snd qid) in ArgVar (Loc.tag ~loc:!@loc id) ] ] + | qid = qualid -> let (_pth,id) = Libnames.repr_qualid (snd qid) in ArgVar (CAst.make ~loc:!@loc id) ] ] ; constr_eval: [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr -> @@ -225,12 +225,12 @@ GEXTEND Gram | l = ident -> Name.Name l ] ] ; let_clause: - [ [ (l,id) = identref; ":="; te = tactic_expr -> - ((l,Name id), arg_of_expr te) - | na = ["_" -> (Some !@loc,Anonymous)]; ":="; te = tactic_expr -> + [ [ idr = identref; ":="; te = tactic_expr -> + (CAst.map (fun id -> Name id) idr, arg_of_expr te) + | na = ["_" -> CAst.make ~loc:!@loc Anonymous]; ":="; te = tactic_expr -> (na, arg_of_expr te) - | (l,id) = identref; args = LIST1 input_fun; ":="; te = tactic_expr -> - ((l,Name id), arg_of_expr (TacFun(args,te))) ] ] + | idr = identref; args = LIST1 input_fun; ":="; te = tactic_expr -> + (CAst.map (fun id -> Name id) idr, arg_of_expr (TacFun(args,te))) ] ] ; match_pattern: [ [ IDENT "context"; oid = OPT Constr.ident; @@ -483,7 +483,7 @@ let pr_ltac_ref = Libnames.pr_reference let pr_tacdef_body tacdef_body = let id, redef, body = match tacdef_body with - | TacticDefinition ((_,id), body) -> Id.print id, false, body + | TacticDefinition ({CAst.v=id}, body) -> Id.print id, false, body | TacticRedefinition (id, body) -> pr_ltac_ref id, true, body in let idl, body = @@ -504,7 +504,7 @@ END VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTacticDefinition | [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => [ VtSideff (List.map (function - | TacticDefinition ((_,r),_) -> r + | TacticDefinition ({CAst.v=r},_) -> r | TacticRedefinition (Ident (_,r),_) -> r | TacticRedefinition (Qualid (_,q),_) -> snd(repr_qualid q)) l), VtLater ] -> [ fun ~atts ~st -> let open Vernacinterp in diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index e68140828..338d61e6f 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -115,16 +115,16 @@ let mk_fix_tac (loc,id,bl,ann,ty) = match bl,ann with [([_],_,_)], None -> 1 | _, Some x -> - let ids = List.map snd (List.flatten (List.map (fun (nal,_,_) -> nal) bl)) in - (try List.index Names.Name.equal (snd x) ids + let ids = List.map (fun x -> x.CAst.v) (List.flatten (List.map (fun (nal,_,_) -> nal) bl)) in + (try List.index Names.Name.equal x.CAst.v ids with Not_found -> user_err Pp.(str "No such fix variable.")) | _ -> user_err Pp.(str "Cannot guess decreasing argument of fix.") in let bl = List.map (fun (nal,bk,t) -> CLocalAssum (nal,bk,t)) bl in (id,n, CAst.make ~loc @@ CProdN(bl,ty)) let mk_cofix_tac (loc,id,bl,ann,ty) = - let _ = Option.map (fun (aloc,_) -> - user_err ~loc:aloc + let _ = Option.map (fun { CAst.loc = aloc } -> + user_err ?loc:aloc ~hdr:"Constr:mk_cofix_tac" (Pp.str"Annotation forbidden in cofix expression.")) ann in let bl = List.map (fun (nal,bk,t) -> CLocalAssum (nal,bk,t)) bl in @@ -134,7 +134,7 @@ let mk_cofix_tac (loc,id,bl,ann,ty) = let destruction_arg_of_constr (c,lbind as clbind) = match lbind with | NoBindings -> begin - try ElimOnIdent (Constrexpr_ops.constr_loc c,snd(Constrexpr_ops.coerce_to_id c)) + try ElimOnIdent (CAst.make ?loc:(Constrexpr_ops.constr_loc c) (Constrexpr_ops.coerce_to_id c).CAst.v) with e when CErrors.noncritical e -> ElimOnConstr clbind end | _ -> ElimOnConstr clbind @@ -152,6 +152,7 @@ let mkTacCase with_evar = function (* Reinterpret ident as notations for variables in the context *) (* because we don't know if they are quantified or not *) | [(clear,ElimOnIdent id),(None,None),None],None -> + let id = CAst.(id.loc, id.v) in TacCase (with_evar,(clear,(CAst.make @@ CRef (Ident id,None),NoBindings))) | ic -> if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic) @@ -161,7 +162,7 @@ let mkTacCase with_evar = function let rec mkCLambdaN_simple_loc ?loc bll c = match bll with - | ((loc1,_)::_ as idl,bk,t) :: bll -> + | ({CAst.loc = loc1}::_ as idl,bk,t) :: bll -> CAst.make ?loc @@ CLambdaN ([CLocalAssum (idl,bk,t)],mkCLambdaN_simple_loc ?loc:(Loc.merge_opt loc1 loc) bll c) | ([],_,_) :: bll -> mkCLambdaN_simple_loc ?loc bll c | [] -> c @@ -169,7 +170,7 @@ let rec mkCLambdaN_simple_loc ?loc bll c = let mkCLambdaN_simple bl c = match bl with | [] -> c | h :: _ -> - let loc = Loc.merge_opt (fst (List.hd (pi1 h))) (Constrexpr_ops.constr_loc c) in + let loc = Loc.merge_opt (List.hd (pi1 h)).CAst.loc (Constrexpr_ops.constr_loc c) in mkCLambdaN_simple_loc ?loc bl c let loc_of_ne_list l = Loc.merge_opt (fst (List.hd l)) (fst (List.last l)) @@ -381,15 +382,20 @@ GEXTEND Gram ; hypident: [ [ id = id_or_meta -> - id,InHyp + let id : Misctypes.lident = id in + id,InHyp | "("; IDENT "type"; IDENT "of"; id = id_or_meta; ")" -> - id,InHypTypeOnly + let id : Misctypes.lident = id in + id,InHypTypeOnly | "("; IDENT "value"; IDENT "of"; id = id_or_meta; ")" -> - id,InHypValueOnly + let id : Misctypes.lident = id in + id,InHypValueOnly ] ] ; hypident_occ: - [ [ (id,l)=hypident; occs=occs -> ((occs,id),l) ] ] + [ [ (id,l)=hypident; occs=occs -> + let id : Misctypes.lident = id in + ((occs,id),l) ] ] ; in_clause: [ [ "*"; occs=occs -> @@ -433,7 +439,8 @@ GEXTEND Gram | -> true ]] ; simple_binder: - [ [ na=name -> ([na],Default Explicit, CAst.make ~loc:!@loc @@ CHole (Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None)) + [ [ na=name -> ([na],Default Explicit, CAst.make ~loc:!@loc @@ + CHole (Some (Evar_kinds.BinderType na.CAst.v), IntroAnonymous, None)) | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> (nal,Default Explicit,c) ] ] ; @@ -565,28 +572,34 @@ GEXTEND Gram TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,na,c,p,false,e)) (* Alternative syntax for "pose proof c as id" *) - | IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":="; + | IDENT "assert"; test_lpar_id_coloneq; "("; lid = identref; ":="; c = lconstr; ")" -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,None,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c)) - | IDENT "eassert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":="; + let { CAst.loc = loc; v = id } = lid in + TacAtom (Loc.tag ?loc @@ TacAssert (false,true,None,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c)) + | IDENT "eassert"; test_lpar_id_coloneq; "("; lid = identref; ":="; c = lconstr; ")" -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,None,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c)) + let { CAst.loc = loc; v = id } = lid in + TacAtom (Loc.tag ?loc @@ TacAssert (true,true,None,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c)) (* Alternative syntax for "assert c as id by tac" *) - | IDENT "assert"; test_lpar_id_colon; "("; (loc,id) = identref; ":"; + | IDENT "assert"; test_lpar_id_colon; "("; lid = identref; ":"; c = lconstr; ")"; tac=by_tactic -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c)) - | IDENT "eassert"; test_lpar_id_colon; "("; (loc,id) = identref; ":"; + let { CAst.loc = loc; v = id } = lid in + TacAtom (Loc.tag ?loc @@ TacAssert (false,true,Some tac,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c)) + | IDENT "eassert"; test_lpar_id_colon; "("; lid = identref; ":"; c = lconstr; ")"; tac=by_tactic -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c)) + let { CAst.loc = loc; v = id } = lid in + TacAtom (Loc.tag ?loc @@ TacAssert (true,true,Some tac,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c)) (* Alternative syntax for "enough c as id by tac" *) - | IDENT "enough"; test_lpar_id_colon; "("; (loc,id) = identref; ":"; + | IDENT "enough"; test_lpar_id_colon; "("; lid = identref; ":"; c = lconstr; ")"; tac=by_tactic -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,false,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c)) - | IDENT "eenough"; test_lpar_id_colon; "("; (loc,id) = identref; ":"; + let { CAst.loc = loc; v = id } = lid in + TacAtom (Loc.tag ?loc @@ TacAssert (false,false,Some tac,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c)) + | IDENT "eenough"; test_lpar_id_colon; "("; lid = identref; ":"; c = lconstr; ")"; tac=by_tactic -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,false,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c)) + let { CAst.loc = loc; v = id } = lid in + TacAtom (Loc.tag ?loc @@ TacAssert (true,false,Some tac,Some (Loc.tag ?loc @@ IntroNaming (IntroIdentifier id)),c)) | IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic -> TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,Some tac,ipat,c)) diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli index 048dcc8e9..ecb0b5796 100644 --- a/plugins/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli @@ -9,7 +9,6 @@ (** Ltac parsing entries *) open Loc -open Names open Pcoq open Libnames open Constrexpr @@ -20,7 +19,7 @@ open Misctypes val open_constr : constr_expr Gram.entry val constr_with_bindings : constr_expr with_bindings Gram.entry val bindings : constr_expr bindings Gram.entry -val hypident : (Id.t located * Locus.hyp_location_flag) Gram.entry +val hypident : (lident * Locus.hyp_location_flag) Gram.entry val constr_may_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry val constr_eval : (constr_expr,reference or_by_notation,constr_expr) may_eval Gram.entry val uconstr : constr_expr Gram.entry @@ -29,8 +28,8 @@ val destruction_arg : constr_expr with_bindings destruction_arg Gram.entry val int_or_var : int or_var Gram.entry val simple_tactic : raw_tactic_expr Gram.entry val simple_intropattern : constr_expr intro_pattern_expr located Gram.entry -val in_clause : Names.Id.t Loc.located Locus.clause_expr Gram.entry -val clause_dft_concl : Names.Id.t Loc.located Locus.clause_expr Gram.entry +val in_clause : lident Locus.clause_expr Gram.entry +val clause_dft_concl : lident Locus.clause_expr Gram.entry val tactic_arg : raw_tactic_arg Gram.entry val tactic_expr : raw_tactic_expr Gram.entry val binder_tactic : raw_tactic_expr Gram.entry diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 4f430b79e..3bc9f2aa0 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -161,7 +161,7 @@ let string_of_genarg_arg (ArgumentType arg) = (keyword "eval" ++ brk (1,1) ++ pr_red_expr (prc,prlc,pr2,pr3) r ++ spc () ++ keyword "in" ++ spc() ++ prc c) - | ConstrContext ((_,id),c) -> + | ConstrContext ({CAst.v=id},c) -> hov 0 (keyword "context" ++ spc () ++ pr_id id ++ spc () ++ str "[ " ++ prlc c ++ str " ]") @@ -364,7 +364,7 @@ let string_of_genarg_arg (ArgumentType arg) = let pr_ltac_or_var pr = function | ArgArg x -> pr x - | ArgVar (loc,id) -> pr_with_comments ?loc (pr_id id) + | ArgVar {CAst.loc;v=id} -> pr_with_comments ?loc (pr_id id) let pr_ltac_constant kn = if !Flags.in_debugger then KerName.print kn @@ -404,7 +404,7 @@ let string_of_genarg_arg (ArgumentType arg) = let pr_as_name = function | Anonymous -> mt () - | Name id -> spc () ++ keyword "as" ++ spc () ++ pr_lident (Loc.tag id) + | Name id -> spc () ++ keyword "as" ++ spc () ++ pr_lident (CAst.make id) let pr_pose_as_style prc na c = spc() ++ prc c ++ pr_as_name na @@ -496,12 +496,12 @@ let string_of_genarg_arg (ArgumentType arg) = let pr_core_destruction_arg prc prlc = function | ElimOnConstr c -> pr_with_bindings prc prlc c - | ElimOnIdent (loc,id) -> pr_with_comments ?loc (pr_id id) + | ElimOnIdent {CAst.loc;v=id} -> pr_with_comments ?loc (pr_id id) | ElimOnAnonHyp n -> int n let pr_destruction_arg prc prlc (clear_flag,h) = pr_clear_flag clear_flag (pr_core_destruction_arg prc prlc) h - + let pr_inversion_kind = function | SimpleInversion -> primitive "simple inversion" | FullInversion -> primitive "inversion" @@ -684,7 +684,7 @@ let pr_goal_selector ~toplevel s = (* match t with | CHole _ -> spc() ++ prlist_with_sep spc (pr_lname) nal | _ ->*) - let s = prlist_with_sep spc pr_lname nal ++ str ":" ++ pr.pr_lconstr t in + let s = prlist_with_sep spc Ppconstr.pr_lname nal ++ str ":" ++ pr.pr_lconstr t in spc() ++ hov 1 (str"(" ++ s ++ str")") in let pr_fix_tac (id,n,c) = @@ -692,10 +692,10 @@ let pr_goal_selector ~toplevel s = (nal,ty)::bll -> if n <= List.length nal then match List.chop (n-1) nal with - _, (_,Name id) :: _ -> id, (nal,ty)::bll - | bef, (loc,Anonymous) :: aft -> + _, {CAst.v=Name id} :: _ -> id, (nal,ty)::bll + | bef, {CAst.loc;v=Anonymous} :: aft -> let id = next_ident_away (Id.of_string"y") avoid in - id, ((bef@(loc,Name id)::aft, ty)::bll) + id, ((bef@(CAst.make ?loc @@ Name id)::aft, ty)::bll) | _ -> assert false else let (id,bll') = set_nth_name avoid (n-List.length nal) bll in @@ -705,7 +705,7 @@ let pr_goal_selector ~toplevel s = let names = List.fold_left (fun ln (nal,_) -> List.fold_left - (fun ln na -> match na with (_,Name id) -> Id.Set.add id ln | _ -> ln) + (fun ln na -> match na with { CAst.v=Name id } -> Id.Set.add id ln | _ -> ln) ln nal) Id.Set.empty bll in let idarg,bll = set_nth_name names n bll in @@ -1087,7 +1087,7 @@ let pr_goal_selector ~toplevel s = if Int.equal n 0 then (List.rev acc, (ty,None)) else match DAst.get ty with Glob_term.GProd(na,Explicit,a,b) -> - strip_ty (([Loc.tag na],(a,None))::acc) (n-1) b + strip_ty (([CAst.make na],(a,None))::acc) (n-1) b | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in strip_ty [] n ty @@ -1158,7 +1158,7 @@ let pr_goal_selector ~toplevel s = if n=0 then (List.rev acc, EConstr.of_constr ty) else match Constr.kind ty with | Constr.Prod(na,a,b) -> - strip_ty (([Loc.tag na],EConstr.of_constr a)::acc) (n-1) b + strip_ty (([CAst.make na],EConstr.of_constr a)::acc) (n-1) b | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in strip_ty [] n ty @@ -1318,7 +1318,7 @@ let () = register_basic_print0 wit_ref pr_reference (pr_or_var (pr_located pr_global)) pr_global; register_basic_print0 wit_ident pr_id pr_id pr_id; - register_basic_print0 wit_var (pr_located pr_id) (pr_located pr_id) pr_id; + register_basic_print0 wit_var pr_lident pr_lident pr_id; register_print0 wit_intro_pattern (lift (Miscprint.pr_intro_pattern pr_constr_expr)) @@ -1328,7 +1328,7 @@ let () = wit_clause_dft_concl (lift (pr_clauses (Some true) pr_lident)) (lift (pr_clauses (Some true) pr_lident)) - (fun c -> Genprint.TopPrinterBasic (fun () -> pr_clauses (Some true) (fun id -> pr_lident (Loc.tag id)) c)) + (fun c -> Genprint.TopPrinterBasic (fun () -> pr_clauses (Some true) (fun id -> pr_lident (CAst.make id)) c)) ; Genprint.register_print0 wit_constr diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index acd7a30c4..e73a18b79 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1773,7 +1773,7 @@ let rec strategy_of_ast = function let mkappc s l = CAst.make @@ CAppExpl ((None,(Libnames.Ident (Loc.tag @@ Id.of_string s)),None),l) let declare_an_instance n s args = - (((Loc.tag @@ Name n),None), Explicit, + (((CAst.make @@ Name n),None), Explicit, CAst.make @@ CAppExpl ((None, Qualid (Loc.tag @@ qualid_of_string s),None), args)) @@ -2006,7 +2006,7 @@ let add_morphism glob binders m s n = let poly = Flags.is_universe_polymorphism () in let instance_id = add_suffix n "_Proper" in let instance = - (((Loc.tag @@ Name instance_id),None), Explicit, + (((CAst.make @@ Name instance_id),None), Explicit, CAst.make @@ CAppExpl ( (None, Qualid (Loc.tag @@ Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None), [cHole; s; m])) diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index 8112cc400..4313456a4 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -374,7 +374,7 @@ let add_ml_tactic_notation name ~level prods = in let ids = List.map_filter get_id prods in let entry = { mltac_name = name; mltac_index = len - i - 1 } in - let map id = Reference (Misctypes.ArgVar (Loc.tag id)) in + let map id = Reference (Misctypes.ArgVar (CAst.make id)) in let tac = TacML (Loc.tag (entry, List.map map ids)) in add_glob_tactic_notation false ~level prods true ids tac in @@ -431,11 +431,11 @@ let warn_unusable_identifier = let register_ltac local tacl = let map tactic_body = match tactic_body with - | Tacexpr.TacticDefinition ((loc,id), body) -> + | Tacexpr.TacticDefinition ({CAst.loc;v=id}, body) -> let kn = Lib.make_kn id in let id_pp = Id.print id in let () = if is_defined_tac kn then - CErrors.user_err ?loc + CErrors.user_err ?loc (str "There is already an Ltac named " ++ id_pp ++ str".") in let is_shadowed = diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index ccd555b61..146d8300d 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -41,7 +41,7 @@ type goal_selector = Vernacexpr.goal_selector = type 'a core_destruction_arg = 'a Misctypes.core_destruction_arg = | ElimOnConstr of 'a - | ElimOnIdent of Id.t located + | ElimOnIdent of lident | ElimOnAnonHyp of int type 'a destruction_arg = @@ -85,8 +85,8 @@ type 'a match_pattern = (* Type of hypotheses for a Match Context rule *) type 'a match_context_hyps = - | Hyp of Name.t located * 'a match_pattern - | Def of Name.t located * 'a match_pattern * 'a match_pattern + | Hyp of lname * 'a match_pattern + | Def of lname * 'a match_pattern * 'a match_pattern (* Type of a Match rule for Match Context and Match *) type ('a,'t) match_rule = @@ -254,7 +254,7 @@ and 'a gen_tactic_expr = | TacFail of global_flag * int or_var * 'n message_token list | TacInfo of 'a gen_tactic_expr | TacLetIn of rec_flag * - (Name.t located * 'a gen_tactic_arg) list * + (lname * 'a gen_tactic_arg) list * 'a gen_tactic_expr | TacMatch of lazy_flag * 'a gen_tactic_expr * @@ -300,7 +300,7 @@ type g_trm = glob_constr_and_expr type g_pat = glob_constr_pattern_and_expr type g_cst = evaluable_global_reference and_short_name or_var type g_ref = ltac_constant located or_var -type g_nam = Id.t located +type g_nam = lident type g_dispatch = < term:g_trm; @@ -328,7 +328,7 @@ type r_trm = constr_expr type r_pat = constr_pattern_expr type r_cst = reference or_by_notation type r_ref = reference -type r_nam = Id.t located +type r_nam = lident type r_lev = rlevel type r_dispatch = < @@ -357,7 +357,7 @@ type t_trm = EConstr.constr type t_pat = constr_pattern type t_cst = evaluable_global_reference type t_ref = ltac_constant located -type t_nam = Id.t +type t_nam = Id.t type t_dispatch = < term:t_trm; @@ -391,5 +391,5 @@ type ltac_call_kind = type ltac_trace = ltac_call_kind Loc.located list type tacdef_body = - | TacticDefinition of Id.t Loc.located * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) + | TacticDefinition of lident * raw_tactic_expr (* indicates that user employed ':=' in Ltac body *) | TacticRedefinition of reference * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index ebffde441..22ec6c5b1 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -6,12 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pattern open Pp +open CErrors +open CAst +open Pattern open Genredexpr open Glob_term open Tacred -open CErrors open Util open Names open Libnames @@ -73,11 +74,11 @@ let strict_check = ref false let adjust_loc loc = if !strict_check then None else loc (* Globalize a name which must be bound -- actually just check it is bound *) -let intern_hyp ist (loc,id as locid) = +let intern_hyp ist ({loc;v=id} as locid) = if not !strict_check then locid else if find_ident id ist then - Loc.tag id + make id else Pretype_errors.error_var_not_found ?loc id @@ -89,7 +90,8 @@ let intern_int_or_var = intern_or_var (fun (n : int) -> n) let intern_string_or_var = intern_or_var (fun (s : string) -> s) let intern_global_reference ist = function - | Ident (loc,id) when find_var id ist -> ArgVar (loc,id) + | Ident (loc,id) when find_var id ist -> + ArgVar CAst.(make ?loc id) | r -> let loc,_ as lqid = qualid_of_reference r in try ArgArg (loc,locate_global_with_alias lqid) @@ -99,7 +101,7 @@ let intern_ltac_variable ist = function | Ident (loc,id) -> if find_var id ist then (* A local variable of any type *) - ArgVar (loc,id) + ArgVar CAst.(make ?loc id) else raise Not_found | _ -> raise Not_found @@ -249,7 +251,7 @@ and intern_or_and_intro_pattern lf ist = function IntroOrPattern (List.map (List.map (intern_intro_pattern lf ist)) ll) let intern_or_and_intro_pattern_loc lf ist = function - | ArgVar (_,id) as x -> + | ArgVar {v=id} as x -> if find_var id ist then x else user_err Pp.(str "Disjunctive/conjunctive introduction pattern expected.") | ArgArg (loc,l) -> ArgArg (loc,intern_or_and_intro_pattern lf ist l) @@ -261,18 +263,18 @@ let intern_intro_pattern_naming_loc lf ist (loc,pat) = let intern_destruction_arg ist = function | clear,ElimOnConstr c -> clear,ElimOnConstr (intern_constr_with_bindings ist c) | clear,ElimOnAnonHyp n as x -> x - | clear,ElimOnIdent (loc,id) -> + | clear,ElimOnIdent {loc;v=id} -> if !strict_check then (* If in a defined tactic, no intros-until *) let c, p = intern_constr ist (CAst.make @@ CRef (Ident (Loc.tag id), None)) in match DAst.get c with - | GVar id -> clear,ElimOnIdent (c.CAst.loc,id) + | GVar id -> clear,ElimOnIdent CAst.(make ?loc:c.loc id) | _ -> clear,ElimOnConstr ((c, p), NoBindings) else - clear,ElimOnIdent (loc,id) + clear,ElimOnIdent CAst.(make ?loc id) let short_name = function - | AN (Ident (loc,id)) when not !strict_check -> Some (loc,id) + | AN (Ident (loc,id)) when not !strict_check -> Some CAst.(make ?loc id) | _ -> None let intern_evaluable_global_reference ist r = @@ -292,9 +294,9 @@ let intern_evaluable_reference_or_by_notation ist = function (* Globalize a reduction expression *) let intern_evaluable ist = function - | AN (Ident (loc,id)) when find_var id ist -> ArgVar (loc,id) + | AN (Ident (loc,id)) when find_var id ist -> ArgVar CAst.(make ?loc id) | AN (Ident (loc,id)) when not !strict_check && find_hyp id ist -> - ArgArg (EvalVarRef id, Some (loc,id)) + ArgArg (EvalVarRef id, Some CAst.(make ?loc id)) | r -> let e = intern_evaluable_reference_or_by_notation ist r in let na = short_name r in @@ -370,7 +372,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = Inr (bound_names,(c,None),dummy_pat) in (l, match p with | Inl r -> interp_ref r - | Inr { CAst.v = CAppExpl((None,r,None),[]) } -> + | Inr { v = CAppExpl((None,r,None),[]) } -> (* We interpret similarly @ref and ref *) interp_ref (AN r) | Inr c -> @@ -400,8 +402,8 @@ let intern_red_expr ist = function | Lazy f -> Lazy (intern_flag ist f) | Pattern l -> Pattern (List.map (intern_constr_with_occurrences ist) l) | Simpl (f,o) -> - Simpl (intern_flag ist f, - Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o) + Simpl (intern_flag ist f, + Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o) | CbvVm o -> CbvVm (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o) | CbvNative o -> CbvNative (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o) | (Red _ | Hnf | ExtraRedExpr _ as r ) -> r @@ -438,7 +440,7 @@ let intern_pattern ist ?(as_type=false) ltacvars = function let intern_constr_may_eval ist = function | ConstrEval (r,c) -> ConstrEval (intern_red_expr ist r,intern_constr ist c) | ConstrContext (locid,c) -> - ConstrContext (intern_hyp ist locid,intern_constr ist c) + ConstrContext (intern_hyp ist locid,intern_constr ist c) | ConstrTypeOf c -> ConstrTypeOf (intern_constr ist c) | ConstrTerm c -> ConstrTerm (intern_constr ist c) @@ -452,12 +454,12 @@ let opt_cons accu = function (* Reads the hypotheses of a "match goal" rule *) let rec intern_match_goal_hyps ist ?(as_type=false) lfun = function - | (Hyp ((_,na) as locna,mp))::tl -> + | (Hyp ({v=na} as locna,mp))::tl -> let ido, metas1, pat = intern_pattern ist ~as_type:true lfun mp in let lfun, metas2, hyps = intern_match_goal_hyps ist lfun tl in let lfun' = name_cons (opt_cons lfun ido) na in lfun', metas1@metas2, Hyp (locna,pat)::hyps - | (Def ((_,na) as locna,mv,mp))::tl -> + | (Def ({v=na} as locna,mv,mp))::tl -> let ido, metas1, patv = intern_pattern ist ~as_type:false lfun mv in let ido', metas2, patt = intern_pattern ist ~as_type:true lfun mp in let lfun, metas3, hyps = intern_match_goal_hyps ist ~as_type lfun tl in @@ -467,7 +469,7 @@ let rec intern_match_goal_hyps ist ?(as_type=false) lfun = function (* Utilities *) let extract_let_names lrc = - let fold accu ((loc, name), _) = + let fold accu ({loc;v=name}, _) = Nameops.Name.fold_right (fun id accu -> if Id.Set.mem id accu then user_err ?loc ~hdr:"glob_tactic" (str "This variable is bound several times.") @@ -813,7 +815,7 @@ let notation_subst bindings tac = let fold id c accu = let loc = Glob_ops.loc_of_glob_constr (fst c) in let c = ConstrMayEval (ConstrTerm c) in - ((loc, Name id), c) :: accu + (CAst.make ?loc @@ Name id, c) :: accu in let bindings = Id.Map.fold fold bindings [] in (** This is theoretically not correct due to potential variable capture, but diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli index e3a4d5c79..8021dc715 100644 --- a/plugins/ltac/tacintern.mli +++ b/plugins/ltac/tacintern.mli @@ -47,7 +47,7 @@ val intern_constr_with_bindings : glob_sign -> constr_expr * constr_expr bindings -> glob_constr_and_expr * glob_constr_and_expr bindings -val intern_hyp : glob_sign -> Id.t Loc.located -> Id.t Loc.located +val intern_hyp : glob_sign -> lident -> lident (** Adds a globalization function for extra generic arguments *) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index f2720954d..79b5c1622 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -9,6 +9,7 @@ open Constrintern open Patternops open Pp +open CAst open Genredexpr open Glob_term open Glob_ops @@ -363,16 +364,16 @@ let error_ltac_variable ?loc id env v s = strbrk "which cannot be coerced to " ++ str s ++ str".") (* Raise Not_found if not in interpretation sign *) -let try_interp_ltac_var coerce ist env (loc,id) = +let try_interp_ltac_var coerce ist env {loc;v=id} = let v = Id.Map.find id ist.lfun in try coerce v with CannotCoerceTo s -> error_ltac_variable ?loc id env v s let interp_ltac_var coerce ist env locid = try try_interp_ltac_var coerce ist env locid - with Not_found -> anomaly (str "Detected '" ++ Id.print (snd locid) ++ str "' as ltac var at interning time.") + with Not_found -> anomaly (str "Detected '" ++ Id.print locid.v ++ str "' as ltac var at interning time.") let interp_ident ist env sigma id = - try try_interp_ltac_var (coerce_var_to_ident false env sigma) ist (Some (env,sigma)) (Loc.tag id) + try try_interp_ltac_var (coerce_var_to_ident false env sigma) ist (Some (env,sigma)) (make id) with Not_found -> id (* Interprets an optional identifier, bound or fresh *) @@ -381,25 +382,25 @@ let interp_name ist env sigma = function | Name id -> Name (interp_ident ist env sigma id) let interp_intro_pattern_var loc ist env sigma id = - try try_interp_ltac_var (coerce_to_intro_pattern env sigma) ist (Some (env,sigma)) (loc,id) + try try_interp_ltac_var (coerce_to_intro_pattern env sigma) ist (Some (env,sigma)) (make ?loc id) with Not_found -> IntroNaming (IntroIdentifier id) let interp_intro_pattern_naming_var loc ist env sigma id = - try try_interp_ltac_var (coerce_to_intro_pattern_naming env sigma) ist (Some (env,sigma)) (loc,id) + try try_interp_ltac_var (coerce_to_intro_pattern_naming env sigma) ist (Some (env,sigma)) (make ?loc id) with Not_found -> IntroIdentifier id -let interp_int ist locid = +let interp_int ist ({loc;v=id} as locid) = try try_interp_ltac_var coerce_to_int ist None locid with Not_found -> - user_err ?loc:(fst locid) ~hdr:"interp_int" - (str "Unbound variable " ++ Id.print (snd locid) ++ str".") + user_err ?loc ~hdr:"interp_int" + (str "Unbound variable " ++ Id.print id ++ str".") let interp_int_or_var ist = function | ArgVar locid -> interp_int ist locid | ArgArg n -> n let interp_int_or_var_as_list ist = function - | ArgVar (_,id as locid) -> + | ArgVar ({v=id} as locid) -> (try coerce_to_int_or_var_list (Id.Map.find id ist.lfun) with Not_found | CannotCoerceTo _ -> [ArgArg (interp_int ist locid)]) | ArgArg n as x -> [x] @@ -408,7 +409,7 @@ let interp_int_or_var_list ist l = List.flatten (List.map (interp_int_or_var_as_list ist) l) (* Interprets a bound variable (especially an existing hypothesis) *) -let interp_hyp ist env sigma (loc,id as locid) = +let interp_hyp ist env sigma ({loc;v=id} as locid) = (* Look first in lfun for a value coercible to a variable *) try try_interp_ltac_var (coerce_to_hyp env sigma) ist (Some (env,sigma)) locid with Not_found -> @@ -416,7 +417,7 @@ let interp_hyp ist env sigma (loc,id as locid) = if is_variable env id then id else Loc.raise ?loc (Logic.RefinerError (env, sigma, Logic.NoSuchHyp id)) -let interp_hyp_list_as_list ist env sigma (loc,id as x) = +let interp_hyp_list_as_list ist env sigma ({loc;v=id} as x) = try coerce_to_hyp_list env sigma (Id.Map.find id ist.lfun) with Not_found | CannotCoerceTo _ -> [interp_hyp ist env sigma x] @@ -425,8 +426,8 @@ let interp_hyp_list ist env sigma l = let interp_reference ist env sigma = function | ArgArg (_,r) -> r - | ArgVar (loc, id) -> - try try_interp_ltac_var (coerce_to_reference env sigma) ist (Some (env,sigma)) (loc, id) + | ArgVar {loc;v=id} -> + try try_interp_ltac_var (coerce_to_reference env sigma) ist (Some (env,sigma)) (make ?loc id) with Not_found -> try VarRef (get_id (Environ.lookup_named id env)) @@ -439,7 +440,7 @@ let try_interp_evaluable env (loc, id) = | _ -> error_not_evaluable (VarRef id) let interp_evaluable ist env sigma = function - | ArgArg (r,Some (loc,id)) -> + | ArgArg (r,Some {loc;v=id}) -> (* Maybe [id] has been introduced by Intro-like tactics *) begin try try_interp_evaluable env (loc, id) @@ -449,8 +450,8 @@ let interp_evaluable ist env sigma = function | _ -> error_global_not_found ?loc (qualid_of_ident id) end | ArgArg (r,None) -> r - | ArgVar (loc, id) -> - try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (loc, id) + | ArgVar {loc;v=id} -> + try try_interp_ltac_var (coerce_to_evaluable_ref env sigma) ist (Some (env,sigma)) (make ?loc id) with Not_found -> try try_interp_evaluable env (loc, id) with Not_found -> error_global_not_found ?loc (qualid_of_ident id) @@ -521,9 +522,9 @@ let default_fresh_id = Id.of_string "H" let interp_fresh_id ist env sigma l = let extract_ident ist env sigma id = try try_interp_ltac_var (coerce_to_ident_not_fresh env sigma) - ist (Some (env,sigma)) (Loc.tag id) + ist (Some (env,sigma)) (make id) with Not_found -> id in - let ids = List.map_filter (function ArgVar (_, id) -> Some id | _ -> None) l in + let ids = List.map_filter (function ArgVar {v=id} -> Some id | _ -> None) l in let avoid = match TacStore.get ist.extra f_avoid_ids with | None -> Id.Set.empty | Some l -> l @@ -535,7 +536,7 @@ let interp_fresh_id ist env sigma l = let s = String.concat "" (List.map (function | ArgArg s -> s - | ArgVar (_,id) -> Id.to_string (extract_ident ist env sigma id)) l) in + | ArgVar {v=id} -> Id.to_string (extract_ident ist env sigma id)) l) in let s = if CLexer.is_keyword s then s^"0" else s in Id.of_string s in Tactics.fresh_id_in_env avoid id env @@ -701,7 +702,7 @@ let interp_constr_with_occurrences ist env sigma (occs,c) = let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) = let p = match a with - | Inl (ArgVar (loc,id)) -> + | Inl (ArgVar {loc;v=id}) -> (* This is the encoding of an ltac var supposed to be bound prioritary to an evaluable reference and otherwise to a constr (it is an encoding to satisfy the "union" type given to Simpl) *) @@ -710,7 +711,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) = with CannotCoerceTo _ -> let c = coerce_to_closed_constr env x in Inr (pattern_of_constr env sigma (EConstr.to_constr sigma c)) in - (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (loc,id) + (try try_interp_ltac_var coerce_eval_ref_or_constr ist (Some (env,sigma)) (make ?loc id) with Not_found -> error_global_not_found ?loc (qualid_of_ident id)) | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b) @@ -756,7 +757,7 @@ let interp_may_eval f ist env sigma = function let (sigma,c_interp) = f ist env sigma c in let (redfun, _) = Redexpr.reduction_of_red_expr env redexp in redfun env sigma c_interp - | ConstrContext ((loc,s),c) -> + | ConstrContext ({loc;v=s},c) -> (try let (sigma,ic) = f ist env sigma c in let ctxt = coerce_to_constr_context (Id.Map.find s ist.lfun) in @@ -821,7 +822,7 @@ let message_of_value v = let interp_message_token ist = function | MsgString s -> Ftactic.return (str s) | MsgInt n -> Ftactic.return (int n) - | MsgIdent (loc,id) -> + | MsgIdent {loc;v=id} -> let v = try Some (Id.Map.find id ist.lfun) with Not_found -> None in match v with | None -> Ftactic.lift (Tacticals.New.tclZEROMSG (Id.print id ++ str" not found.")) @@ -881,7 +882,7 @@ let interp_intro_pattern_naming_option ist env sigma = function let interp_or_and_intro_pattern_option ist env sigma = function | None -> sigma, None - | Some (ArgVar (loc,id)) -> + | Some (ArgVar {loc;v=id}) -> (match interp_intro_pattern_var loc ist env sigma id with | IntroAction (IntroOrAndPattern l) -> sigma, Some (loc,l) | _ -> @@ -906,14 +907,14 @@ let interp_binding_name ist env sigma = function (* If a name is bound, it has to be a quantified hypothesis *) (* user has to use other names for variables if these ones clash with *) (* a name intented to be used as a (non-variable) identifier *) - try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist (Some (env,sigma)) (Loc.tag id) + try try_interp_ltac_var (coerce_to_quantified_hypothesis sigma) ist (Some (env,sigma)) (make id) with Not_found -> NamedHyp id let interp_declared_or_quantified_hypothesis ist env sigma = function | AnonHyp n -> AnonHyp n | NamedHyp id -> try try_interp_ltac_var - (coerce_to_decl_or_quant_hyp env sigma) ist (Some (env,sigma)) (Loc.tag id) + (coerce_to_decl_or_quant_hyp env sigma) ist (Some (env,sigma)) (make id) with Not_found -> NamedHyp id let interp_binding ist env sigma (loc,(b,c)) = @@ -924,7 +925,7 @@ let interp_bindings ist env sigma = function | NoBindings -> sigma, NoBindings | ImplicitBindings l -> - let sigma, l = interp_open_constr_list ist env sigma l in + let sigma, l = interp_open_constr_list ist env sigma l in sigma, ImplicitBindings l | ExplicitBindings l -> let sigma, l = List.fold_left_map (interp_binding ist env) sigma l in @@ -959,14 +960,14 @@ let interp_destruction_arg ist gl arg = interp_open_constr_with_bindings ist env sigma c end | keep,ElimOnAnonHyp n as x -> x - | keep,ElimOnIdent (loc,id) -> + | keep,ElimOnIdent {loc;v=id} -> let error () = user_err ?loc (strbrk "Cannot coerce " ++ Id.print id ++ strbrk " neither to a quantified hypothesis nor to a term.") in let try_cast_id id' = if Tactics.is_quantified_hypothesis id' gl - then keep,ElimOnIdent (loc,id') + then keep,ElimOnIdent CAst.(make ?loc id') else (keep, ElimOnConstr begin fun env sigma -> try (sigma, (constr_of_id env id', NoBindings)) @@ -994,7 +995,7 @@ let interp_destruction_arg ist gl arg = with Not_found -> (* We were in non strict (interactive) mode *) if Tactics.is_quantified_hypothesis id gl then - keep,ElimOnIdent (loc,id) + keep,ElimOnIdent CAst.(make ?loc id) else let c = (DAst.make ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in let f env sigma = @@ -1043,11 +1044,11 @@ let cons_and_check_name id l = else id::l let rec read_match_goal_hyps lfun ist env sigma lidh = function - | (Hyp ((loc,na) as locna,mp))::tl -> + | (Hyp ({loc;v=na} as locna,mp))::tl -> let lidh' = Name.fold_right cons_and_check_name na lidh in Hyp (locna,read_pattern lfun ist env sigma mp):: (read_match_goal_hyps lfun ist env sigma lidh' tl) - | (Def ((loc,na) as locna,mv,mp))::tl -> + | (Def ({loc;v=na} as locna,mv,mp))::tl -> let lidh' = Name.fold_right cons_and_check_name na lidh in Def (locna,read_pattern lfun ist env sigma mv, read_pattern lfun ist env sigma mp):: (read_match_goal_hyps lfun ist env sigma lidh' tl) @@ -1112,7 +1113,7 @@ let rec val_interp ist ?(appl=UnnamedAppl) (tac:glob_tactic_expr) : Val.t Ftacti in Tactic_debug.debug_prompt lev tac eval | _ -> value_interp ist >>= fun v -> return (name_vfun appl v) - + and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacAtom (loc,t) -> @@ -1248,7 +1249,7 @@ and force_vrec ist v : Val.t Ftactic.t = and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t = match r with - | ArgVar (loc,id) -> + | ArgVar {loc;v=id} -> let v = try Id.Map.find id ist.lfun with Not_found -> in_gen (topwit wit_var) id @@ -1416,7 +1417,7 @@ and tactic_of_value ist vle = and interp_letrec ist llc u = Proofview.tclUNIT () >>= fun () -> (* delay for the effects of [lref], just in case. *) let lref = ref ist.lfun in - let fold accu ((_, na), b) = + let fold accu ({v=na}, b) = let v = of_tacvalue (VRec (lref, TacArg (Loc.tag b))) in Name.fold_right (fun id -> Id.Map.add id v) na accu in @@ -1431,7 +1432,7 @@ and interp_letin ist llc u = | [] -> let ist = { ist with lfun } in val_interp ist u - | ((_, na), body) :: defs -> + | ({v=na}, body) :: defs -> Ftactic.bind (interp_tacarg ist body) (fun v -> fold (Name.fold_right (fun id -> Id.Map.add id v) na lfun) defs) in diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index 5f2723a1e..2d448e832 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -75,7 +75,7 @@ val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map (** Interprets tactic expressions *) val interp_hyp : interp_sign -> Environ.env -> Evd.evar_map -> - Id.t Loc.located -> Id.t + lident -> Id.t val interp_glob_closure : interp_sign -> Environ.env -> Evd.evar_map -> ?kind:Pretyping.typing_constraint -> ?pattern_mode:bool -> glob_constr_and_expr -> @@ -125,9 +125,9 @@ val hide_interp : bool -> raw_tactic_expr -> unit Proofview.tactic option -> uni (** Internals that can be useful for syntax extensions. *) val interp_ltac_var : (value -> 'a) -> interp_sign -> - (Environ.env * Evd.evar_map) option -> Id.t Loc.located -> 'a + (Environ.env * Evd.evar_map) option -> lident -> 'a -val interp_int : interp_sign -> Id.t Loc.located -> int +val interp_int : interp_sign -> lident -> int val interp_int_or_var : interp_sign -> int or_var -> int diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli index 2475e41f9..dce6f5558 100644 --- a/plugins/ltac/tactic_debug.mli +++ b/plugins/ltac/tactic_debug.mli @@ -74,7 +74,7 @@ val db_logic_failure : debug_info -> exn -> unit Proofview.NonLogical.t (** Prints a logic failure message for a rule *) val db_breakpoint : debug_info -> - Id.t Loc.located message_token list -> unit Proofview.NonLogical.t + Misctypes.lident message_token list -> unit Proofview.NonLogical.t val extract_ltac_trace : ?loc:Loc.t -> Tacexpr.ltac_trace -> Pp.t option Loc.located diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index e87951dd7..6bf9215e0 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -306,9 +306,9 @@ module PatternMatching (E:StaticEnvironment) = struct [pat] is [Hyp _] or [Def _]. *) let hyp_match pat hyps = match pat with - | Hyp ((_,hypname),typepat) -> + | Hyp ({CAst.v=hypname},typepat) -> hyp_match_type hypname typepat hyps - | Def ((_,hypname),bodypat,typepat) -> + | Def ({CAst.v=hypname},bodypat,typepat) -> hyp_match_body_and_type hypname bodypat typepat hyps (** [hyp_pattern_list_match pats hyps lhs], matches the list of diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index 01d3f79c7..5ce30c3d7 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -255,10 +255,10 @@ let tauto_power_flags = { } let with_flags flags _ ist = - let f = (Loc.tag @@ Id.of_string "f") in - let x = (Loc.tag @@ Id.of_string "x") in + let f = CAst.make @@ Id.of_string "f" in + let x = CAst.make @@ Id.of_string "x" in let arg = Val.Dyn (tag_tauto_flags, flags) in - let ist = { ist with lfun = Id.Map.add (snd x) arg ist.lfun } in + let ist = { ist with lfun = Id.Map.add x.CAst.v arg ist.lfun } in eval_tactic_ist ist (TacArg (Loc.tag @@ TacCall (Loc.tag (ArgVar f, [Reference (ArgVar x)])))) let register_tauto_tactic tac name0 args = diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4 index 40897d62f..55dc7f580 100644 --- a/plugins/quote/g_quote.ml4 +++ b/plugins/quote/g_quote.ml4 @@ -22,7 +22,7 @@ let x = Id.of_string "x" let make_cont (k : Val.t) (c : EConstr.t) = let c = Tacinterp.Value.of_constr c in - let tac = TacCall (Loc.tag (ArgVar (Loc.tag cont), [Reference (ArgVar (Loc.tag x))])) in + let tac = TacCall (Loc.tag (ArgVar CAst.(make cont), [Reference (ArgVar CAst.(make x))])) in let ist = { lfun = Id.Map.add cont k (Id.Map.singleton x c); extra = TacStore.empty; } in Tacinterp.eval_tactic_ist ist (TacArg (Loc.tag tac)) diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index e3e749b75..125afb1a0 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -166,12 +166,12 @@ let ltac_call tac (args:glob_tactic_arg list) = (* Calling a locally bound tactic *) let ltac_lcall tac args = - TacArg(Loc.tag @@ TacCall (Loc.tag (ArgVar(Loc.tag @@ Id.of_string tac),args))) + TacArg(Loc.tag @@ TacCall (Loc.tag (ArgVar CAst.(make @@ Id.of_string tac),args))) let ltac_apply (f : Value.t) (args: Tacinterp.Value.t list) = let fold arg (i, vars, lfun) = let id = Id.of_string ("x" ^ string_of_int i) in - let x = Reference (ArgVar (Loc.tag id)) in + let x = Reference (ArgVar CAst.(make id)) in (succ i, x :: vars, Id.Map.add id arg lfun) in let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in @@ -206,7 +206,7 @@ let get_res = let exec_tactic env evd n f args = let fold arg (i, vars, lfun) = let id = Id.of_string ("x" ^ string_of_int i) in - let x = Reference (ArgVar (Loc.tag id)) in + let x = Reference (ArgVar CAst.(make id)) in (succ i, x :: vars, Id.Map.add id (Value.of_constr arg) lfun) in let (_, args, lfun) = List.fold_right fold args (0, [], Id.Map.empty) in diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 499154d50..4ae746288 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -268,7 +268,7 @@ let interp_wit wit ist gl x = sigma, Tacinterp.Value.cast (topwit wit) arg let interp_hyp ist gl (SsrHyp (loc, id)) = - let s, id' = interp_wit wit_var ist gl (loc, id) in + let s, id' = interp_wit wit_var ist gl CAst.(make ?loc id) in if not_section_id id' then s, SsrHyp (loc, id') else hyp_err ?loc "Can't clear section hypothesis " id' @@ -835,9 +835,9 @@ let rec mkCHoles ?loc n = if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, IntroAnonymous, None)) :: mkCHoles ?loc (n - 1) let mkCHole loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None) let mkCLambda ?loc name ty t = CAst.make ?loc @@ - CLambdaN ([CLocalAssum([loc, name], Default Explicit, ty)], t) + CLambdaN ([CLocalAssum([CAst.make ?loc name], Default Explicit, ty)], t) let mkCArrow ?loc ty t = CAst.make ?loc @@ - CProdN ([CLocalAssum([Loc.tag Anonymous], Default Explicit, ty)], t) + CProdN ([CLocalAssum([CAst.make Anonymous], Default Explicit, ty)], t) let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, CastConv ty) let rec isCHoles = function { CAst.v = CHole _ } :: cl -> isCHoles cl | cl -> cl = [] @@ -855,7 +855,7 @@ let pf_interp_ty ?(resolve_typeclasses=false) ist gl ty = | _, (_, Some ty) -> let rec force_type ty = CAst.(map (function | CProdN (abs, t) -> - n_binders := !n_binders + List.length (List.flatten (List.map (function CLocalAssum (nal,_,_) -> nal | CLocalDef (na,_,_) -> [na] | CLocalPattern (_,_) -> (* We count a 'pat for 1; TO BE CHECKED *) [Loc.tag Name.Anonymous]) abs)); + n_binders := !n_binders + List.length (List.flatten (List.map (function CLocalAssum (nal,_,_) -> nal | CLocalDef (na,_,_) -> [na] | CLocalPattern _ -> (* We count a 'pat for 1; TO BE CHECKED *) [CAst.make Name.Anonymous]) abs)); CProdN (abs, force_type t) | CLetIn (n, v, oty, t) -> incr n_binders; CLetIn (n, v, oty, force_type t) | _ -> (mkCCast ty (mkCType None)).v)) ty in diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 211cad3f5..0d8044f19 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -130,7 +130,7 @@ let pr_ssrhyp _ _ _ = pr_hyp let wit_ssrhyprep = add_genarg "ssrhyprep" pr_hyp let intern_hyp ist (SsrHyp (loc, id) as hyp) = - let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_var) (loc, id)) in + let _ = Tacintern.intern_genarg ist (in_gen (rawwit wit_var) CAst.(make ?loc id)) in if not_section_id id then hyp else hyp_err ?loc "Can't clear section hypothesis " id @@ -316,7 +316,7 @@ END let pr_index = function - | Misctypes.ArgVar (_, id) -> pr_id id + | Misctypes.ArgVar {CAst.v=id} -> pr_id id | Misctypes.ArgArg n when n > 0 -> int n | _ -> mt () let pr_ssrindex _ _ _ = pr_index @@ -330,13 +330,13 @@ let mk_index ?loc = function | iv -> iv let interp_index ist gl idx = - Tacmach.project gl, + Tacmach.project gl, match idx with | Misctypes.ArgArg _ -> idx - | Misctypes.ArgVar (loc, id) -> + | Misctypes.ArgVar id -> let i = try - let v = Id.Map.find id ist.Tacinterp.lfun in + let v = Id.Map.find id.CAst.v ist.Tacinterp.lfun in begin match Tacinterp.Value.to_int v with | Some i -> i | None -> @@ -350,8 +350,8 @@ let interp_index ist gl idx = end | None -> raise Not_found end end - with _ -> CErrors.user_err ?loc (str"Index not a number") in - Misctypes.ArgArg (check_index ?loc i) + with _ -> CErrors.user_err ?loc:id.CAst.loc (str"Index not a number") in + Misctypes.ArgArg (check_index ?loc:id.CAst.loc i) open Pltac @@ -1014,22 +1014,22 @@ let rec mkBstruct i = function | [] -> [] let rec format_local_binders h0 bl0 = match h0, bl0 with - | BFvar :: h, CLocalAssum ([_, x], _, _) :: bl -> + | BFvar :: h, CLocalAssum ([{CAst.v=x}], _, _) :: bl -> Bvar x :: format_local_binders h bl | BFdecl _ :: h, CLocalAssum (lxs, _, t) :: bl -> - Bdecl (List.map snd lxs, t) :: format_local_binders h bl - | BFdef :: h, CLocalDef ((_, x), v, oty) :: bl -> + Bdecl (List.map (fun x -> x.CAst.v) lxs, t) :: format_local_binders h bl + | BFdef :: h, CLocalDef ({CAst.v=x}, v, oty) :: bl -> Bdef (x, oty, v) :: format_local_binders h bl | _ -> [] let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with - | BFvar :: h, { v = CLambdaN ([CLocalAssum([_, x], _, _)], c) } -> + | BFvar :: h, { v = CLambdaN ([CLocalAssum([{CAst.v=x}], _, _)], c) } -> let bs, c' = format_constr_expr h c in Bvar x :: bs, c' | BFdecl _:: h, { v = CLambdaN ([CLocalAssum(lxs, _, t)], c) } -> let bs, c' = format_constr_expr h c in - Bdecl (List.map snd lxs, t) :: bs, c' - | BFdef :: h, { v = CLetIn((_, x), v, oty, c) } -> + Bdecl (List.map (fun x -> x.CAst.v) lxs, t) :: bs, c' + | BFdef :: h, { v = CLetIn({CAst.v=x}, v, oty, c) } -> let bs, c' = format_constr_expr h c in Bdef (x, oty, v) :: bs, c' | [BFcast], { v = CCast (c, CastConv t) } -> @@ -1037,7 +1037,7 @@ let rec format_constr_expr h0 c0 = let open CAst in match h0, c0 with | BFrec (has_str, has_cast) :: h, { v = CFix ( _, [_, (Some locn, CStructRec), bl, t, c]) } -> let bs = format_local_binders h bl in - let bstr = if has_str then [Bstruct (Name (snd locn))] else [] in + let bstr = if has_str then [Bstruct (Name locn.CAst.v)] else [] in bs @ bstr @ (if has_cast then [Bcast t] else []), c | BFrec (_, has_cast) :: h, { v = CCoFix ( _, [_, bl, t, c]) } -> format_local_binders h bl @ (if has_cast then [Bcast t] else []), c @@ -1156,18 +1156,18 @@ ARGUMENT EXTEND ssrbvar TYPED AS constr PRINTED BY pr_ssrbvar END let bvar_lname = let open CAst in function - | { v = CRef (Ident (loc, id), _) } -> Loc.tag ?loc @@ Name id - | { loc = loc } -> Loc.tag ?loc Anonymous + | { v = CRef (Ident (loc, id), _) } -> CAst.make ?loc @@ Name id + | { loc = loc } -> CAst.make ?loc Anonymous let pr_ssrbinder prc _ _ (_, c) = prc c ARGUMENT EXTEND ssrbinder TYPED AS ssrfwdfmt * constr PRINTED BY pr_ssrbinder | [ ssrbvar(bv) ] -> - [ let xloc, _ as x = bvar_lname bv in + [ let { CAst.loc=xloc } as x = bvar_lname bv in (FwdPose, [BFvar]), CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) ] | [ "(" ssrbvar(bv) ")" ] -> - [ let xloc, _ as x = bvar_lname bv in + [ let { CAst.loc=xloc } as x = bvar_lname bv in (FwdPose, [BFvar]), CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) ] | [ "(" ssrbvar(bv) ":" lconstr(t) ")" ] -> @@ -1191,7 +1191,7 @@ GEXTEND Gram [ ["of" | "&"]; c = operconstr LEVEL "99" -> let loc = !@loc in (FwdPose, [BFvar]), - CAst.make ~loc @@ CLambdaN ([CLocalAssum ([Loc.tag ~loc Anonymous],Default Explicit,c)],mkCHole (Some loc)) ] + CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],Default Explicit,c)],mkCHole (Some loc)) ] ]; END @@ -1250,13 +1250,13 @@ END let pr_ssrfixfwd _ _ _ (id, fwd) = str " fix " ++ pr_id id ++ pr_fwd fwd let bvar_locid = function - | { CAst.v = CRef (Ident (loc, id), _) } -> loc, id + | { CAst.v = CRef (Ident (loc, id), _) } -> CAst.make ?loc id | _ -> CErrors.user_err (Pp.str "Missing identifier after \"(co)fix\"") ARGUMENT EXTEND ssrfixfwd TYPED AS ident * ssrfwd PRINTED BY pr_ssrfixfwd | [ "fix" ssrbvar(bv) ssrbinder_list(bs) ssrstruct(sid) ssrfwd(fwd) ] -> - [ let (_, id) as lid = bvar_locid bv in + [ let { CAst.v=id } as lid = bvar_locid bv in let (fk, h), (ck, (rc, oc)) = fwd in let c = Option.get oc in let has_cast, t', c' = match format_constr_expr h c with @@ -1265,8 +1265,10 @@ ARGUMENT EXTEND ssrfixfwd TYPED AS ident * ssrfwd PRINTED BY pr_ssrfixfwd let lb = fix_binders bs in let has_struct, i = let rec loop = function - (l', Name id') :: _ when Option.equal Id.equal sid (Some id') -> true, (l', id') - | [l', Name id'] when sid = None -> false, (l', id') + | {CAst.loc=l'; v=Name id'} :: _ when Option.equal Id.equal sid (Some id') -> + true, CAst.make ?loc:l' id' + | [{CAst.loc=l';v=Name id'}] when sid = None -> + false, CAst.make ?loc:l' id' | _ :: bn -> loop bn | [] -> CErrors.user_err (Pp.str "Bad structural argument") in loop (names_of_local_assums lb) in @@ -1282,7 +1284,7 @@ let pr_ssrcofixfwd _ _ _ (id, fwd) = str " cofix " ++ pr_id id ++ pr_fwd fwd ARGUMENT EXTEND ssrcofixfwd TYPED AS ssrfixfwd PRINTED BY pr_ssrcofixfwd | [ "cofix" ssrbvar(bv) ssrbinder_list(bs) ssrfwd(fwd) ] -> - [ let _, id as lid = bvar_locid bv in + [ let { CAst.v=id } as lid = bvar_locid bv in let (fk, h), (ck, (rc, oc)) = fwd in let c = Option.get oc in let has_cast, t', c' = match format_constr_expr h c with @@ -1323,7 +1325,7 @@ END let intro_id_to_binder = List.map (function | IPatId id -> - let xloc, _ as x = bvar_lname (mkCVar id) in + let { CAst.loc=xloc } as x = bvar_lname (mkCVar id) in (FwdPose, [BFvar]), CAst.make @@ CLambdaN ([CLocalAssum([x], Default Explicit, mkCHole xloc)], mkCHole None) @@ -1332,9 +1334,9 @@ let intro_id_to_binder = List.map (function let binder_to_intro_id = CAst.(List.map (function | (FwdPose, [BFvar]), { v = CLambdaN ([CLocalAssum(ids,_,_)],_) } | (FwdPose, [BFdecl _]), { v = CLambdaN ([CLocalAssum(ids,_,_)],_) } -> - List.map (function (_, Name id) -> IPatId id | _ -> IPatAnon One) ids - | (FwdPose, [BFdef]), { v = CLetIn ((_,Name id),_,_,_) } -> [IPatId id] - | (FwdPose, [BFdef]), { v = CLetIn ((_,Anonymous),_,_,_) } -> [IPatAnon One] + List.map (function {v=Name id} -> IPatId id | _ -> IPatAnon One) ids + | (FwdPose, [BFdef]), { v = CLetIn ({v=Name id},_,_,_) } -> [IPatId id] + | (FwdPose, [BFdef]), { v = CLetIn ({v=Anonymous},_,_,_) } -> [IPatAnon One] | _ -> anomaly "ssrbinder is not a binder")) let pr_ssrhavefwdwbinders _ _ prt (tr,((hpats, (fwd, hint)))) = @@ -1405,7 +1407,7 @@ let ssrorelse = Gram.entry_create "ssrorelse" GEXTEND Gram GLOBAL: ssrorelse ssrseqarg; ssrseqidx: [ - [ test_ssrseqvar; id = Prim.ident -> ArgVar (Loc.tag ~loc:!@loc id) + [ test_ssrseqvar; id = Prim.ident -> ArgVar (CAst.make ~loc:!@loc id) | n = Prim.natural -> ArgArg (check_index ~loc:!@loc n) ] ]; ssrswap: [[ IDENT "first" -> !@loc, true | IDENT "last" -> !@loc, false ]]; diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 25d1472f1..8e6e0347f 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -79,9 +79,9 @@ let aliasvar = function let mk_cnotype mp = aliasvar mp, None in let mk_ctype mp t = aliasvar mp, Some t in let mk_rtype t = Some t in -let mk_dthen ?loc (mp, ct, rt) c = (Loc.tag ?loc (mp, c)), ct, rt in +let mk_dthen ?loc (mp, ct, rt) c = (CAst.make ?loc (mp, c)), ct, rt in let mk_let ?loc rt ct mp c1 = - CAst.make ?loc @@ CCases (LetPatternStyle, rt, ct, [Loc.tag ?loc (mp, c1)]) in + CAst.make ?loc @@ CCases (LetPatternStyle, rt, ct, [CAst.make ?loc (mp, c1)]) in let mk_pat c (na, t) = (c, na, t) in GEXTEND Gram GLOBAL: binder_constr; @@ -94,14 +94,16 @@ GEXTEND Gram ] ]; ssr_dthen: [[ dp = ssr_dpat; "then"; c = lconstr -> mk_dthen ~loc:!@loc dp c ]]; ssr_elsepat: [[ "else" -> [[CAst.make ~loc:!@loc @@ CPatAtom None]] ]]; - ssr_else: [[ mp = ssr_elsepat; c = lconstr -> Loc.tag ~loc:!@loc (mp, c) ]]; + ssr_else: [[ mp = ssr_elsepat; c = lconstr -> CAst.make ~loc:!@loc (mp, c) ]]; binder_constr: [ [ "if"; c = operconstr LEVEL "200"; "is"; db1 = ssr_dthen; b2 = ssr_else -> let b1, ct, rt = db1 in CAst.make ~loc:!@loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2]) | "if"; c = operconstr LEVEL "200";"isn't";db1 = ssr_dthen; b2 = ssr_else -> let b1, ct, rt = db1 in - let b1, b2 = - let (l1, (p1, r1)), (l2, (p2, r2)) = b1, b2 in (l1, (p1, r2)), (l2, (p2, r1)) in + let b1, b2 = let open CAst in + let {loc=l1; v=(p1, r1)}, {loc=l2; v=(p2, r2)} = b1, b2 in + (make ?loc:l1 (p1, r2), make ?loc:l2 (p2, r1)) + in CAst.make ~loc:!@loc @@ CCases (MatchStyle, rt, [mk_pat c ct], [b1; b2]) | "let"; ":"; mp = ssr_mpat; ":="; c = lconstr; "in"; c1 = lconstr -> mk_let ~loc:!@loc no_rt [mk_pat c no_ct] mp c1 @@ -118,7 +120,7 @@ GEXTEND Gram GLOBAL: closed_binder; closed_binder: [ [ ["of" | "&"]; c = operconstr LEVEL "99" -> - [CLocalAssum ([Loc.tag ~loc:!@loc Anonymous], Default Explicit, c)] + [CLocalAssum ([CAst.make ~loc:!@loc Anonymous], Default Explicit, c)] ] ]; END (* }}} *) @@ -553,7 +555,7 @@ GEXTEND Gram let s = coerce_reference_to_id qid in Vernacexpr.VernacDefinition ((Decl_kinds.NoDischarge,Decl_kinds.CanonicalStructure), - ((Loc.tag (Name s)),None), d) + ((CAst.make (Name s)),None), d) ]]; END @@ -584,10 +586,10 @@ END GEXTEND Gram GLOBAL: hloc; hloc: [ - [ "in"; "("; "Type"; "of"; id = ident; ")" -> - Tacexpr.HypLocation ((Loc.tag id), Locus.InHypTypeOnly) - | "in"; "("; IDENT "Value"; "of"; id = ident; ")" -> - Tacexpr.HypLocation ((Loc.tag id), Locus.InHypValueOnly) + [ "in"; "("; "Type"; "of"; id = ident; ")" -> + Tacexpr.HypLocation (CAst.make id, Locus.InHypTypeOnly) + | "in"; "("; IDENT "Value"; "of"; id = ident; ")" -> + Tacexpr.HypLocation (CAst.make id, Locus.InHypValueOnly) ] ]; END diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 71e8b4ac4..73e212365 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -137,9 +137,9 @@ let destGLambda c = match DAst.get c with GLambda (Name id, _, _, c) -> (id, c) let isGHole c = match DAst.get c with GHole _ -> true | _ -> false let mkCHole ~loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None) let mkCLambda ?loc name ty t = CAst.make ?loc @@ - CLambdaN ([CLocalAssum([Loc.tag ?loc name], Default Explicit, ty)], t) + CLambdaN ([CLocalAssum([CAst.make ?loc name], Default Explicit, ty)], t) let mkCLetIn ?loc name bo t = CAst.make ?loc @@ - CLetIn ((Loc.tag ?loc name), bo, None, t) + CLetIn ((CAst.make ?loc name), bo, None, t) let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, dC ty) (** Constructors for rawconstr *) let mkRHole = DAst.make @@ GHole (InternalHole, IntroAnonymous, None) diff --git a/pretyping/univdecls.ml b/pretyping/univdecls.ml index 3cf32d7ff..89f1185a9 100644 --- a/pretyping/univdecls.ml +++ b/pretyping/univdecls.ml @@ -6,12 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Names open CErrors (** Local universes and constraints declarations *) type universe_decl = - (Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl + (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl let default_univ_decl = let open Misctypes in @@ -34,9 +33,9 @@ let interp_univ_constraints env evd cstrs = in List.fold_left interp (evd,Univ.Constraint.empty) cstrs -let interp_univ_decl env decl = +let interp_univ_decl env decl = let open Misctypes in - let pl = decl.univdecl_instance in + let pl : lident list = decl.univdecl_instance in let evd = Evd.from_ctx (Evd.make_evar_universe_context env (Some pl)) in let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in let decl = { univdecl_instance = pl; diff --git a/pretyping/univdecls.mli b/pretyping/univdecls.mli index 0c3b749cb..706d3a157 100644 --- a/pretyping/univdecls.mli +++ b/pretyping/univdecls.mli @@ -8,7 +8,7 @@ (** Local universe and constraint declarations. *) type universe_decl = - (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl + (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl val default_univ_decl : universe_decl diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 873505940..3c7095505 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -10,6 +10,7 @@ open CErrors open Util open Pp +open CAst open Names open Nameops open Libnames @@ -151,7 +152,7 @@ let tag_var = tag Tag.variable if !Flags.beautify && not (Int.equal n 0) then comment (CLexer.extract_comments n) else mt() - let pr_with_comments ?loc pp = pr_located (fun x -> x) (Loc.tag ?loc pp) + let pr_with_comments ?loc pp = pr_located (fun x -> x) (loc, pp) let pr_sep_com sep f c = pr_with_comments ?loc:(constr_loc c) (sep() ++ f c) @@ -220,28 +221,28 @@ let tag_var = tag Tag.variable let pr_expl_args pr (a,expl) = match expl with | None -> pr (lapp,L) a - | Some (_,ExplByPos (n,_id)) -> + | Some {v=ExplByPos (n,_id)} -> anomaly (Pp.str "Explicitation by position not implemented.") - | Some (_,ExplByName id) -> + | Some {v=ExplByName id} -> str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")" let pr_opt_type_spc pr = function | { CAst.v = CHole (_,Misctypes.IntroAnonymous,_) } -> mt () | t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t - let pr_lident (loc,id) = + let pr_lident {loc; v=id} = match loc with | None -> pr_id id | Some loc -> let (b,_) = Loc.unloc loc in - pr_located pr_id @@ Loc.tag ~loc:(Loc.make_loc (b,b + String.length (Id.to_string id))) id + pr_located pr_id (Some (Loc.make_loc (b,b + String.length (Id.to_string id))), id) let pr_lname = function - | (loc,Name id) -> pr_lident (loc,id) - | lna -> pr_located Name.print lna + | {CAst.loc; v=Name id} -> pr_lident CAst.(make ?loc id) + | x -> pr_ast Name.print x let pr_or_var pr = function | ArgArg x -> pr x - | ArgVar (loc,s) -> pr_lident (loc,s) + | ArgVar id -> pr_lident id let pr_prim_token = function | Numeral (n,s) -> str (if s then n else "-"^n) @@ -315,7 +316,7 @@ let tag_var = tag Tag.variable let pr_patt = pr_patt mt - let pr_eqn pr (loc,(pl,rhs)) = + let pr_eqn pr {loc;v=(pl,rhs)} = spc() ++ hov 4 (pr_with_comments ?loc (str "| " ++ @@ -323,12 +324,12 @@ let tag_var = tag Tag.variable ++ str " =>") ++ pr_sep_com spc (pr ltop) rhs)) - let begin_of_binder l_bi = + let begin_of_binder l_bi = let b_loc l = fst (Option.cata Loc.unloc (0,0) l) in match l_bi with - | CLocalDef((loc,_),_,_) -> b_loc loc - | CLocalAssum((loc,_)::_,_,_) -> b_loc loc - | CLocalPattern(loc,(_,_)) -> b_loc loc + | CLocalDef({loc},_,_) -> b_loc loc + | CLocalAssum({loc}::_,_,_) -> b_loc loc + | CLocalPattern{loc} -> b_loc loc | _ -> assert false let begin_of_binders = function @@ -350,12 +351,12 @@ let tag_var = tag Tag.variable | Generalized (b, b', t') -> assert (match b with Implicit -> true | _ -> false); begin match nal with - |[loc,Anonymous] -> + |[{loc; v=Anonymous}] -> hov 1 (str"`" ++ (surround_impl b' ((if t' then str "!" else mt ()) ++ pr t))) - |[loc,Name id] -> + |[{loc; v=Name id}] -> hov 1 (str "`" ++ (surround_impl b' - (pr_lident (loc,id) ++ str " : " ++ + (pr_lident CAst.(make ?loc id) ++ str " : " ++ (if t' then str "!" else mt()) ++ pr t))) |_ -> anomaly (Pp.str "List of generalized binders have alwais one element.") end @@ -375,7 +376,7 @@ let tag_var = tag Tag.variable surround (pr_lname na ++ pr_opt_no_spc (fun t -> str " :" ++ ws 1 ++ pr_c t) topt ++ str" :=" ++ spc() ++ pr_c c) - | CLocalPattern (loc,(p,tyo)) -> + | CLocalPattern {CAst.loc; v = p,tyo} -> let p = pr_patt lsimplepatt p in match tyo with | None -> @@ -410,7 +411,7 @@ let tag_var = tag Tag.variable let pr_guard_annot pr_aux bl (n,ro) = match n with | None -> mt () - | Some (loc, id) -> + | Some {loc; v = id} -> match (ro : Constrexpr.recursion_order_expr) with | CStructRec -> let names_of_binder = function @@ -427,11 +428,11 @@ let tag_var = tag Tag.variable spc() ++ str "{" ++ keyword "measure" ++ spc () ++ pr_aux m ++ spc() ++ pr_id id++ (match r with None -> mt() | Some r -> str" on " ++ pr_aux r) ++ str"}" - let pr_fixdecl pr prd dangling_with_for ((_,id),ro,bl,t,c) = + let pr_fixdecl pr prd dangling_with_for ({v=id},ro,bl,t,c) = let annot = pr_guard_annot (pr lsimpleconstr) bl ro in pr_recursive_decl pr prd dangling_with_for id bl annot t c - let pr_cofixdecl pr prd dangling_with_for ((_,id),bl,t,c) = + let pr_cofixdecl pr prd dangling_with_for ({v=id},bl,t,c) = pr_recursive_decl pr prd dangling_with_for id bl (mt()) t c let pr_recursive pr_decl id = function @@ -461,7 +462,7 @@ let tag_var = tag Tag.variable let pr_simple_return_type pr na po = (match na with - | Some (_,Name id) -> + | Some {v=Name id} -> spc () ++ keyword "as" ++ spc () ++ pr_id id | _ -> mt ()) ++ pr_case_type pr po @@ -492,7 +493,7 @@ let tag_var = tag Tag.variable let pr_fun_sep = spc () ++ str "=>" let pr_dangling_with_for sep pr inherited a = - match a.CAst.v with + match a.v with | (CFix (_,[_])|CCoFix(_,[_])) -> pr sep (latom,E) a | _ -> @@ -507,14 +508,14 @@ let tag_var = tag Tag.variable return ( hov 0 (keyword "fix" ++ spc () ++ pr_recursive - (pr_fixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) fix), + (pr_fixdecl (pr mt) (pr_dangling_with_for mt pr)) id.v fix), lfix ) | CCoFix (id,cofix) -> return ( hov 0 (keyword "cofix" ++ spc () ++ pr_recursive - (pr_cofixdecl (pr mt) (pr_dangling_with_for mt pr)) (snd id) cofix), + (pr_cofixdecl (pr mt) (pr_dangling_with_for mt pr)) id.v cofix), lfix ) | CProdN (bl,a) -> @@ -533,8 +534,8 @@ let tag_var = tag Tag.variable pr_fun_sep ++ pr spc ltop a), llambda ) - | CLetIn ((_,Name x), ({ CAst.v = CFix((_,x'),[_])} - | { CAst.v = CCoFix((_,x'),[_]) } as fx), t, b) + | CLetIn ({v=Name x}, ({ v = CFix({v=x'},[_])} + | { v = CCoFix({v=x'},[_]) } as fx), t, b) when Id.equal x x' -> return ( hv 0 ( @@ -590,7 +591,7 @@ let tag_var = tag Tag.variable hv 0 (str"{|" ++ pr_record_body_gen (pr spc) l ++ str" |}"), latom ) - | CCases (LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[(_,([[p]],b))]) -> + | CCases (LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[{v=([[p]],b)}]) -> return ( hv 0 ( keyword "let" ++ spc () ++ str"'" ++ diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 158906dd2..cedeed5f3 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -10,7 +10,6 @@ objects and their subcomponents. *) (** The default pretty-printers produce pretty-printing commands ({!Pp.t}). *) -open Loc open Libnames open Constrexpr open Names @@ -23,8 +22,8 @@ val pr_tight_coma : unit -> Pp.t val pr_or_var : ('a -> Pp.t) -> 'a or_var -> Pp.t -val pr_lident : Id.t located -> Pp.t -val pr_lname : Name.t located -> Pp.t +val pr_lident : lident -> Pp.t +val pr_lname : lname -> Pp.t val pr_with_comments : ?loc:Loc.t -> Pp.t -> Pp.t val pr_com_at : int -> Pp.t @@ -44,7 +43,7 @@ val pr_glob_level : glob_level -> Pp.t val pr_glob_sort : glob_sort -> Pp.t val pr_guard_annot : (constr_expr -> Pp.t) -> local_binder_expr list -> - ('a * Names.Id.t) option * recursion_order_expr -> + lident option * recursion_order_expr -> Pp.t val pr_record_body : (reference * constr_expr) list -> Pp.t diff --git a/printing/pputils.ml b/printing/pputils.ml index a544b4762..e779fc5fc 100644 --- a/printing/pputils.ml +++ b/printing/pputils.ml @@ -24,9 +24,11 @@ let pr_located pr (loc, x) = before ++ x ++ after | _ -> pr x +let pr_ast pr { CAst.loc; v } = pr_located pr (loc, v) + let pr_or_var pr = function | ArgArg x -> pr x - | ArgVar (_,s) -> Names.Id.print s + | ArgVar {CAst.v=s} -> Names.Id.print s let pr_with_occurrences pr keyword (occs,c) = match occs with diff --git a/printing/pputils.mli b/printing/pputils.mli index f7f586b77..ec5c32fc4 100644 --- a/printing/pputils.mli +++ b/printing/pputils.mli @@ -12,6 +12,7 @@ open Locus open Genredexpr val pr_located : ('a -> Pp.t) -> 'a Loc.located -> Pp.t +val pr_ast : ('a -> Pp.t) -> 'a CAst.t -> Pp.t (** Prints an object surrounded by its commented location *) val pr_or_var : ('a -> Pp.t) -> 'a or_var -> Pp.t diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 31c0d20f3..83cac7ddd 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -11,6 +11,8 @@ open Names open CErrors open Util +open CAst + open Extend open Vernacexpr open Pputils @@ -59,7 +61,7 @@ open Decl_kinds let pr_ident_decl (lid, l) = pr_lident lid ++ pr_universe_decl l - + let string_of_fqid fqid = String.concat "." (List.map Id.to_string fqid) @@ -236,7 +238,7 @@ open Decl_kinds keyword "Module" ++ spc() ++ pr_lfqid id ++ str" := " ++ pr_located pr_qualid qid - let rec pr_module_ast leading_space pr_c = let open CAst in function + let rec pr_module_ast leading_space pr_c = function | { loc ; v = CMident qid } -> if leading_space then spc () ++ pr_located pr_qualid (loc, qid) @@ -287,10 +289,10 @@ open Decl_kinds prlist_strict (pr_module_vardecls pr_c) l let pr_type_option pr_c = function - | { CAst.v = CHole (k, Misctypes.IntroAnonymous, _) } -> mt() + | { v = CHole (k, Misctypes.IntroAnonymous, _) } -> mt() | _ as c -> brk(0,2) ++ str" :" ++ pr_c c - let pr_decl_notation prc ((loc,ntn),c,scopt) = + let pr_decl_notation prc ({loc; v=ntn},c,scopt) = fnl () ++ keyword "where " ++ qs ntn ++ str " := " ++ Flags.without_option Flags.beautify prc c ++ pr_opt (fun sc -> str ": " ++ str sc) scopt @@ -329,7 +331,7 @@ open Decl_kinds let begin_of_inductive = function | [] -> 0 - | (_,((loc,_),_))::_ -> Option.cata (fun loc -> fst (Loc.unloc loc)) 0 loc + | (_,({loc},_))::_ -> Option.cata (fun loc -> fst (Loc.unloc loc)) 0 loc let pr_class_rawexpr = function | FunClass -> keyword "Funclass" @@ -392,8 +394,8 @@ open Decl_kinds | SetOnlyPrinting -> keyword "only printing" | SetOnlyParsing -> keyword "only parsing" | SetCompatVersion v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"") - | SetFormat("text",s) -> keyword "format " ++ pr_located qs s - | SetFormat(k,s) -> keyword "format " ++ qs k ++ spc() ++ pr_located qs s + | SetFormat("text",s) -> keyword "format " ++ pr_ast qs s + | SetFormat(k,s) -> keyword "format " ++ qs k ++ spc() ++ pr_ast qs s let pr_syntax_modifiers = function | [] -> mt() @@ -537,7 +539,7 @@ open Decl_kinds let rec aux = function | SsEmpty -> "()" | SsType -> "(Type)" - | SsSingl (_,id) -> "("^Id.to_string id^")" + | SsSingl { v=id } -> "("^Id.to_string id^")" | SsCompl e -> "-" ^ aux e^"" | SsUnion(e1,e2) -> "("^aux e1 ^" + "^ aux e2^")" | SsSubstr(e1,e2) -> "("^aux e1 ^" - "^ aux e2^")" @@ -661,7 +663,7 @@ open Decl_kinds ++ spc() ++ pr_smart_global q ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]" ) - | VernacInfix (((_,s),mv),q,sn) -> (* A Verifier *) + | VernacInfix (({v=s},mv),q,sn) -> (* A Verifier *) return ( hov 0 (hov 0 (keyword "Infix " ++ qs s ++ str " :=" ++ pr_constrarg q) ++ @@ -670,7 +672,7 @@ open Decl_kinds | None -> mt() | Some sc -> spc() ++ str":" ++ spc() ++ str sc)) ) - | VernacNotation (c,((_,s),l),opt) -> + | VernacNotation (c,({v=s},l),opt) -> return ( hov 2 (keyword "Notation" ++ spc() ++ qs s ++ str " :=" ++ Flags.without_option Flags.beautify pr_constrarg c ++ pr_syntax_modifiers l ++ @@ -680,7 +682,7 @@ open Decl_kinds ) | VernacSyntaxExtension (_, (s, l)) -> return ( - keyword "Reserved Notation" ++ spc() ++ pr_located qs s ++ + keyword "Reserved Notation" ++ spc() ++ pr_ast qs s ++ pr_syntax_modifiers l ) | VernacNotationAddFormat(s,k,v) -> @@ -692,7 +694,7 @@ open Decl_kinds | VernacDefinition ((discharge,kind),id,b) -> (* A verifier... *) let pr_def_token dk = keyword ( - if Name.is_anonymous (snd (fst id)) + if Name.is_anonymous (fst id).v then "Goal" else Kindops.string_of_definition_object_kind dk) in @@ -711,7 +713,7 @@ open Decl_kinds in (pr_binders_arg bl,ty,Some (pr_reduce red ++ pr_lconstr body)) | ProveBody (bl,t) -> - let typ u = if snd (fst id) = Anonymous then (assert (bl = []); u) else (str" :" ++ u) in + let typ u = if (fst id).v = Anonymous then (assert (bl = []); u) else (str" :" ++ u) in (pr_binders_arg bl, typ (pr_spc_lconstr t), None) in let (binds,typ,c) = pr_def_body b in return ( @@ -889,16 +891,16 @@ open Decl_kinds return ( hov 1 ( (if abst then keyword "Declare" ++ spc () else mt ()) ++ - keyword "Instance" ++ - (match instid with - | (loc, Name id), l -> spc () ++ pr_ident_decl ((loc, id),l) ++ spc () - | (_, Anonymous), _ -> mt ()) ++ - pr_and_type_binders_arg sup ++ + keyword "Instance" ++ + (match instid with + | {loc; v = Name id}, l -> spc () ++ pr_ident_decl (CAst.(make ?loc id),l) ++ spc () + | { v = Anonymous }, _ -> mt ()) ++ + pr_and_type_binders_arg sup ++ str":" ++ spc () ++ (match bk with Implicit -> str "! " | Explicit -> mt ()) ++ pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info ++ (match props with - | Some (true, { CAst.v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}" + | Some (true, { v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}" | Some (true,_) -> assert false | Some (false,p) -> spc () ++ str":=" ++ spc () ++ pr_constr p | None -> mt())) @@ -1031,7 +1033,7 @@ open Decl_kinds hov 2 ( keyword "Arguments" ++ spc() ++ pr_smart_global q ++ - let pr_s = function None -> str"" | Some (_,s) -> str "%" ++ str s in + let pr_s = function None -> str"" | Some {v=s} -> str "%" ++ str s in let pr_if b x = if b then x else str "" in let pr_br imp x = match imp with | Vernacexpr.Implicit -> str "[" ++ x ++ str "]" @@ -1237,9 +1239,9 @@ let pr_vernac_flag = (fun f a -> pr_vernac_flag f ++ spc() ++ a) f (pr_vernac_expr v' ++ sep_end v') - | VernacTime (_,(_,v)) -> + | VernacTime (_,{v}) -> return (keyword "Time" ++ spc() ++ pr_vernac_control v) - | VernacRedirect (s, (_,v)) -> + | VernacRedirect (s, {v}) -> return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_control v) | VernacTimeout(n,v) -> return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac_control v) diff --git a/printing/prettyp.mli b/printing/prettyp.mli index fd7f1f92b..c1d8f1d37 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -33,10 +33,10 @@ val print_eval : Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t val print_name : env -> Evd.evar_map -> reference or_by_notation -> - Vernacexpr.univ_name_list option -> Pp.t + Universes.univ_name_list option -> Pp.t val print_opaque_name : env -> Evd.evar_map -> reference -> Pp.t val print_about : env -> Evd.evar_map -> reference or_by_notation -> - Vernacexpr.univ_name_list option -> Pp.t + Universes.univ_name_list option -> Pp.t val print_impargs : reference or_by_notation -> Pp.t (** Pretty-printing functions for classes and coercions *) diff --git a/printing/printmod.mli b/printing/printmod.mli index 97ed063fe..4f15dd393 100644 --- a/printing/printmod.mli +++ b/printing/printmod.mli @@ -13,6 +13,6 @@ val printable_body : DirPath.t -> bool val pr_mutual_inductive_body : Environ.env -> MutInd.t -> Declarations.mutual_inductive_body -> - Vernacexpr.univ_name_list option -> Pp.t + Universes.univ_name_list option -> Pp.t val print_module : bool -> ModPath.t -> Pp.t val print_modtype : ModPath.t -> Pp.t diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 833e34c33..0a50bcf8c 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -79,7 +79,7 @@ type proof_object = { type proof_ending = | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t | Proved of Vernacexpr.opacity_flag * - Vernacexpr.lident option * + Misctypes.lident option * proof_object type proof_terminator = proof_ending -> unit type closed_proof = proof_object * proof_terminator diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 29445a746..06647bf3e 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -50,7 +50,7 @@ type proof_ending = | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t | Proved of Vernacexpr.opacity_flag * - Vernacexpr.lident option * + Misctypes.lident option * proof_object type proof_terminator type closed_proof = proof_object * proof_terminator diff --git a/stm/stm.ml b/stm/stm.ml index 92587b8ea..e7c371798 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -565,8 +565,8 @@ end = struct (* {{{ *) let reachable id = reachable !vcs id let mk_branch_name { expr = x } = Branch.make (match Vernacprop.under_control x with - | VernacDefinition (_,((_, Name i),_),_) -> Id.to_string i - | VernacStartTheoremProof (_,[((_,i),_),_]) -> Id.to_string i + | VernacDefinition (_,({CAst.v=Name i},_),_) -> Id.to_string i + | VernacStartTheoremProof (_,[({CAst.v=i},_),_]) -> Id.to_string i | _ -> "branch") let edit_branch = Branch.make "edit" let branch ?root ?pos name kind = vcs := branch !vcs ?root ?pos name kind @@ -1174,7 +1174,7 @@ end = struct (* {{{ *) match Vernacprop.under_control v with | VernacResetInitial -> Stateid.initial, VtNow - | VernacResetName (_,name) -> + | VernacResetName {CAst.v=name} -> let id = VCS.get_branch_pos (VCS.current_branch ()) in (try let oid = @@ -1236,7 +1236,7 @@ let set_compilation_hints file = let get_hint_ctx loc = let s = Aux_file.get ?loc !hints "context_used" in let ids = List.map Names.Id.of_string (Str.split (Str.regexp " ") s) in - let ids = List.map (fun id -> Loc.tag id) ids in + let ids = List.map (fun id -> CAst.make id) ids in match ids with | [] -> SsEmpty | x :: xs -> @@ -1956,8 +1956,8 @@ end = struct (* {{{ *) = let e, time, batch, fail = let rec find ~time ~batch ~fail = function - | VernacTime (batch,(_,e)) -> find ~time:true ~batch ~fail e - | VernacRedirect (_,(_,e)) -> find ~time ~batch ~fail e + | VernacTime (batch,{CAst.v=e}) -> find ~time:true ~batch ~fail e + | VernacRedirect (_,{CAst.v=e}) -> find ~time ~batch ~fail e | VernacFail e -> find ~time ~batch ~fail:true e | e -> e, time, batch, fail in find ~time:false ~batch:false ~fail:false e in diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index cbbb54e45..93d58b2a9 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -6,10 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Vernacexpr open CErrors open Util open Pp +open CAst +open Vernacexpr let default_proof_mode () = Proof_global.get_default_proof_mode_name () [@ocaml.warning "-3"] @@ -87,13 +88,14 @@ let classify_vernac e = | VernacUnsetOption (["Default";"Proof";"Using"]) | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow (* StartProof *) - | VernacDefinition ((Decl_kinds.DoDischarge,_),((_,i),_),ProveBody _) -> - VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity, idents_of_name i), VtLater - | VernacDefinition (_,((_,i),_),ProveBody _) -> + | VernacDefinition ((Decl_kinds.DoDischarge,_),({v=i},_),ProveBody _) -> + VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity, idents_of_name i), VtLater + + | VernacDefinition (_,({v=i},_),ProveBody _) -> let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in VtStartProof(default_proof_mode (),guarantee, idents_of_name i), VtLater | VernacStartTheoremProof (_,l) -> - let ids = List.map (fun (((_, i), _), _) -> i) l in + let ids = List.map (fun (({v=i}, _), _) -> i) l in let guarantee = if poly then Doesn'tGuaranteeOpacity else GuaranteesOpacity in VtStartProof (default_proof_mode (),guarantee,ids), VtLater | VernacFixpoint (discharge,l) -> @@ -102,7 +104,7 @@ let classify_vernac e = else GuaranteesOpacity in let ids, open_proof = - List.fold_left (fun (l,b) ((((_,id),_),_,_,_,p),_) -> + List.fold_left (fun (l,b) ((({v=id},_),_,_,_,p),_) -> id::l, b || p = None) ([],false) l in if open_proof then VtStartProof (default_proof_mode (),guarantee,ids), VtLater @@ -113,29 +115,29 @@ let classify_vernac e = else GuaranteesOpacity in let ids, open_proof = - List.fold_left (fun (l,b) ((((_,id),_),_,_,p),_) -> + List.fold_left (fun (l,b) ((({v=id},_),_,_,p),_) -> id::l, b || p = None) ([],false) l in if open_proof then VtStartProof (default_proof_mode (),guarantee,ids), VtLater else VtSideff ids, VtLater (* Sideff: apply to all open branches. usually run on master only *) | VernacAssumption (_,_,l) -> - let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> snd id) l) l) in - VtSideff ids, VtLater - | VernacDefinition (_,((_,id),_),DefineBody _) -> VtSideff (idents_of_name id), VtLater + let ids = List.flatten (List.map (fun (_,(l,_)) -> List.map (fun (id, _) -> id.v) l) l) in + VtSideff ids, VtLater + | VernacDefinition (_,({v=id},_),DefineBody _) -> VtSideff (idents_of_name id), VtLater | VernacInductive (_, _,_,l) -> - let ids = List.map (fun (((_,((_,id),_)),_,_,_,cl),_) -> id :: match cl with - | Constructors l -> List.map (fun (_,((_,id),_)) -> id) l - | RecordDecl (oid,l) -> (match oid with Some (_,x) -> [x] | _ -> []) @ + let ids = List.map (fun (((_,({v=id},_)),_,_,_,cl),_) -> id :: match cl with + | Constructors l -> List.map (fun (_,({v=id},_)) -> id) l + | RecordDecl (oid,l) -> (match oid with Some {v=x} -> [x] | _ -> []) @ CList.map_filter (function - | ((_,AssumExpr((_,Names.Name n),_)),_),_ -> Some n + | ((_,AssumExpr({v=Names.Name n},_)),_),_ -> Some n | _ -> None) l) l in VtSideff (List.flatten ids), VtLater | VernacScheme l -> - let ids = List.map snd (CList.map_filter (fun (x,_) -> x) l) in + let ids = List.map (fun {v}->v) (CList.map_filter (fun (x,_) -> x) l) in VtSideff ids, VtLater - | VernacCombinedScheme ((_,id),_) -> VtSideff [id], VtLater - | VernacBeginSection (_,id) -> VtSideff [id], VtLater + | VernacCombinedScheme ({v=id},_) -> VtSideff [id], VtLater + | VernacBeginSection {v=id} -> VtSideff [id], VtLater | VernacUniverse _ | VernacConstraint _ | VernacCanonical _ | VernacCoercion _ | VernacIdentityCoercion _ | VernacAddLoadPath _ | VernacRemoveLoadPath _ | VernacAddMLPath _ @@ -159,10 +161,10 @@ let classify_vernac e = (* (Local) Notations have to disappear *) | VernacEndSegment _ -> VtSideff [], VtNow (* Modules with parameters have to be executed: can import notations *) - | VernacDeclareModule (exp,(_,id),bl,_) - | VernacDefineModule (exp,(_,id),bl,_,_) -> + | VernacDeclareModule (exp,{v=id},bl,_) + | VernacDefineModule (exp,{v=id},bl,_,_) -> VtSideff [id], if bl = [] && exp = None then VtLater else VtNow - | VernacDeclareModuleType ((_,id),bl,_,_) -> + | VernacDeclareModuleType ({v=id},bl,_,_) -> VtSideff [id], if bl = [] then VtLater else VtNow (* These commands alter the parser *) | VernacOpenCloseScope _ | VernacDelimiters _ | VernacBindScope _ @@ -198,7 +200,7 @@ let classify_vernac e = ) poly f in static_classifier ~poly e | VernacTimeout (_,e) -> static_control_classifier ~poly e - | VernacTime (_,(_,e)) | VernacRedirect (_, (_,e)) -> + | VernacTime (_,{v=e}) | VernacRedirect (_, {v=e}) -> static_control_classifier ~poly e | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) (match static_control_classifier ~poly e with diff --git a/tactics/equality.ml b/tactics/equality.ml index 674d01777..9a1ac768c 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1484,7 +1484,7 @@ let simpleInjClause flags with_evars = function | Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (injEq flags ~old:true with_evars clear_flag None)) c let injConcl flags = injClause flags None false None -let injHyp flags clear_flag id = injClause flags None false (Some (clear_flag,ElimOnIdent (Loc.tag id))) +let injHyp flags clear_flag id = injClause flags None false (Some (clear_flag,ElimOnIdent CAst.(make id))) let decompEqThen keep_proofs ntac (lbeq,_,(t,t1,t2) as u) clause = Proofview.Goal.enter begin fun gl -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 29a30b4a2..7e281e2fe 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1190,7 +1190,7 @@ let onOpenInductionArg env sigma tac = function let sigma = Tacmach.New.project gl in tac clear_flag (sigma,(c,NoBindings)) end)) - | clear_flag,ElimOnIdent (_,id) -> + | clear_flag,ElimOnIdent {CAst.v=id} -> (* A quantified hypothesis *) Tacticals.New.tclTHEN (try_intros_until_id_check id) @@ -1206,7 +1206,7 @@ let onInductionArg tac = function Tacticals.New.tclTHEN (intros_until_n n) (Tacticals.New.onLastHyp (fun c -> tac clear_flag (c,NoBindings))) - | clear_flag,ElimOnIdent (_,id) -> + | clear_flag,ElimOnIdent {CAst.v=id} -> (* A quantified hypothesis *) Tacticals.New.tclTHEN (try_intros_until_id_check id) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 1f681d9cf..92dee84f3 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -170,7 +170,7 @@ let rec interp_vernac ~time ~check ~interactive ~state (loc,com) = (* The -time option is only supported from console-based clients due to the way it prints. *) if time then print_cmd_header ?loc com; - let com = if time then VernacTime(time,(loc,com)) else com in + let com = if time then VernacTime(time, CAst.make ?loc com) else com in interp com with reraise -> (* XXX: In non-interactive mode edit_at seems to do very weird diff --git a/vernac/classes.ml b/vernac/classes.ml index 4a2dba859..695be74bb 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -132,7 +132,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~program_mode poly ctx (instid, bk, cl) props ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri = let env = Global.env() in - let ((loc, instid), pl) = instid in + let ({CAst.loc;v=instid}, pl) = instid in let sigma, decl = Univdecls.interp_univ_decl_opt env pl in let tclass, ids = match bk with @@ -410,7 +410,7 @@ let context poly l = let nstatus = match b with | None -> pi3 (ComAssumption.declare_assumption false decl (t, univs) Universes.empty_binders [] impl - Vernacexpr.NoInline (Loc.tag id)) + Vernacexpr.NoInline (CAst.make id)) | Some b -> let decl = (Discharge, poly, Definition) in let entry = Declare.definition_entry ~univs ~types:t b in diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 5d7adb24a..7e5b941ad 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -42,7 +42,7 @@ let should_axiom_into_instance = function true | Global | Local -> !axiom_into_instance -let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl (_,ident) = +let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl {CAst.v=ident} = match local with | Discharge when Lib.sections_are_opened () -> let ctx = match ctx with @@ -109,7 +109,7 @@ let declare_assumptions idl is_coe k (c,uctx) pl imps nl = let maybe_error_many_udecls = function - | ((loc,id), Some _) -> + | ({CAst.loc;v=id}, Some _) -> user_err ?loc ~hdr:"many_universe_declarations" Pp.(str "When declaring multiple axioms in one command, " ++ str "only the first is allowed a universe binder " ++ @@ -126,7 +126,7 @@ let process_assumptions_udecls kind l = in let () = match kind, udecl with | (Discharge, _, _), Some _ when Lib.sections_are_opened () -> - let loc = fst first_id in + let loc = first_id.CAst.loc in let msg = Pp.str "Section variables cannot be polymorphic." in user_err ?loc msg | _ -> () @@ -151,8 +151,8 @@ let do_assumptions kind nl l = let (sigma,_,_),l = List.fold_left_map (fun (sigma,env,ienv) (is_coe,(idl,c)) -> let sigma,(t,imps) = interp_assumption sigma env ienv [] c in let env = - push_named_context (List.map (fun (_,id) -> LocalAssum (id,t)) idl) env in - let ienv = List.fold_right (fun (_,id) ienv -> + push_named_context (List.map (fun {CAst.v=id} -> LocalAssum (id,t)) idl) env in + let ienv = List.fold_right (fun {CAst.v=id} ienv -> let impls = compute_internalization_data env Variable t imps in Id.Map.add id impls ienv) idl ienv in ((sigma,env,ienv),((is_coe,idl),t,imps))) @@ -175,7 +175,7 @@ let do_assumptions kind nl l = let t = replace_vars subst t in let refs, status' = declare_assumptions idl is_coe kind (t,uctx) ubinders imps nl in let subst' = List.map2 - (fun (_,id) (c,u) -> (id, Universes.constr_of_global_univ (c,u))) + (fun {CAst.v=id} (c,u) -> (id, Universes.constr_of_global_univ (c,u))) idl refs in subst'@subst, status' && status, next_uctx uctx) diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 2fa156abd..0491638c9 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -30,5 +30,5 @@ val do_assumptions : locality * polymorphic * assumption_object_kind -> val declare_assumption : coercion_flag -> assumption_kind -> types in_constant_universes_entry -> Universes.universe_binders -> Impargs.manual_implicits -> - bool (** implicit *) -> Vernacexpr.inline -> variable Loc.located -> + bool (** implicit *) -> Vernacexpr.inline -> variable CAst.t -> global_reference * Univ.Instance.t * bool diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index d648e293a..489f299a2 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -102,7 +102,7 @@ let check_mutuality env evd isfix fixl = type structured_fixpoint_expr = { fix_name : Id.t; fix_univs : universe_decl_expr option; - fix_annot : Id.t Loc.located option; + fix_annot : lident option; fix_binders : local_binder_expr list; fix_body : constr_expr option; fix_type : constr_expr @@ -175,7 +175,7 @@ let interp_recursive ~program_mode ~cofix fixl notations = | x , None -> x | Some ls , Some us -> let lsu = ls.univdecl_instance and usu = us.univdecl_instance in - if not (CList.for_all2eq (fun x y -> Id.equal (snd x) (snd y)) lsu usu) then + if not (CList.for_all2eq (fun x y -> Id.equal x.CAst.v y.CAst.v) lsu usu) then user_err Pp.(str "(co)-recursive definitions should all have the same universe binders"); Some us) fixl None in let sigma, decl = Univdecls.interp_univ_decl_opt env all_universes in @@ -323,7 +323,7 @@ let extract_decreasing_argument limit = function let extract_fixpoint_components limit l = let fixl, ntnl = List.split l in - let fixl = List.map (fun (((_,id),pl),ann,bl,typ,def) -> + let fixl = List.map (fun (({CAst.v=id},pl),ann,bl,typ,def) -> let ann = extract_decreasing_argument limit ann in {fix_name = id; fix_annot = ann; fix_univs = pl; fix_binders = bl; fix_body = def; fix_type = typ}) fixl in @@ -331,7 +331,7 @@ let extract_fixpoint_components limit l = let extract_cofixpoint_components l = let fixl, ntnl = List.split l in - List.map (fun (((_,id),pl),bl,typ,def) -> + List.map (fun (({CAst.v=id},pl),bl,typ,def) -> {fix_name = id; fix_annot = None; fix_univs = pl; fix_binders = bl; fix_body = def; fix_type = typ}) fixl, List.flatten ntnl diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index 2c84bd84d..2926e30e5 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -31,7 +31,7 @@ val do_cofixpoint : type structured_fixpoint_expr = { fix_name : Id.t; fix_univs : Vernacexpr.universe_decl_expr option; - fix_annot : Id.t Loc.located option; + fix_annot : Misctypes.lident option; fix_binders : local_binder_expr list; fix_body : constr_expr option; fix_type : constr_expr diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 41474fc63..c650e9e40 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -249,7 +249,7 @@ let inductive_levels env evd poly arities inds = (evd,[]) (Array.to_list levels') destarities sizes in evd, List.rev arities -let check_named (loc, na) = match na with +let check_named {CAst.loc;v=na} = match na with | Name _ -> () | Anonymous -> let msg = str "Parameters must be named." in @@ -260,7 +260,7 @@ let check_param = function | CLocalDef (na, _, _) -> check_named na | CLocalAssum (nas, Default _, _) -> List.iter check_named nas | CLocalAssum (nas, Generalized _, _) -> () -| CLocalPattern (loc,_) -> +| CLocalPattern {CAst.loc} -> Loc.raise ?loc (Stream.Error "pattern with quote not allowed here.") let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite = @@ -364,7 +364,7 @@ let eq_local_binders bl1 bl2 = List.equal local_binder_eq bl1 bl2 let extract_coercions indl = - let mkqid (_,((_,id),_)) = qualid_of_ident id in + let mkqid (_,({CAst.v=id},_)) = qualid_of_ident id in let extract lc = List.filter (fun (iscoe,_) -> iscoe) lc in List.map mkqid (List.flatten(List.map (fun (_,_,_,lc) -> extract lc) indl)) @@ -378,10 +378,10 @@ let extract_params indl = params let extract_inductive indl = - List.map (fun (((_,indname),pl),_,ar,lc) -> { + List.map (fun (({CAst.v=indname},pl),_,ar,lc) -> { ind_name = indname; ind_univs = pl; ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (GType [])) ar; - ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc + ind_lc = List.map (fun (_,({CAst.v=id},t)) -> (id,t)) lc }) indl let extract_mutual_inductive_declaration_components indl = diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index a9a91e304..af34f8b29 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -298,16 +298,16 @@ let do_program_recursive local poly fixkind fixl ntns = let do_program_fixpoint local poly l = let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in match g, l with - | [(n, CWfRec r)], [((((_,id),pl),_,bl,typ,def),ntn)] -> + | [(n, CWfRec r)], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] -> let recarg = match n with - | Some n -> mkIdentC (snd n) + | Some n -> mkIdentC n.CAst.v | None -> user_err ~hdr:"do_program_fixpoint" (str "Recursive argument required for well-founded fixpoints") in build_wellfounded (id, pl, n, bl, typ, out_def def) poly r recarg ntn - | [(n, CMeasureRec (m, r))], [((((_,id),pl),_,bl,typ,def),ntn)] -> + | [(n, CMeasureRec (m, r))], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] -> build_wellfounded (id, pl, n, bl, typ, out_def def) poly (Option.default (CAst.make @@ CRef (lt_ref,None)) r) m ntn @@ -322,7 +322,7 @@ let do_program_fixpoint local poly l = let extract_cofixpoint_components l = let fixl, ntnl = List.split l in - List.map (fun (((_,id),pl),bl,typ,def) -> + List.map (fun (({CAst.v=id},pl),bl,typ,def) -> {fix_name = id; fix_annot = None; fix_univs = pl; fix_binders = bl; fix_body = def; fix_type = typ}) fixl, List.flatten ntnl diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 2f4c95aff..447c5085b 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -367,17 +367,16 @@ requested | InType -> recs ^ "t_nodep") ) in let newid = add_suffix (basename_of_global (IndRef ind)) suffix in - let newref = Loc.tag newid in + let newref = CAst.make newid in ((newref,isdep,ind,z)::l1),l2 in match t with | CaseScheme (x,y,z) -> names "_case" "_case" x y z | InductionScheme (x,y,z) -> names "_ind" "_rec" x y z | EqualityScheme x -> l1,((None,smart_global_inductive x)::l2) - let do_mutual_induction_scheme lnamedepindsort = - let lrecnames = List.map (fun ((_,f),_,_,_) -> f) lnamedepindsort + let lrecnames = List.map (fun ({CAst.v},_,_,_) -> v) lnamedepindsort and env0 = Global.env() in let sigma, lrecspec, _ = List.fold_right @@ -416,7 +415,7 @@ let get_common_underlying_mutual_inductive = function then user_err Pp.(str "A type occurs twice"); mind, List.map_filter - (function (Some id,(_,i)) -> Some (i,snd id) | (None,_) -> None) all + (function (Some id,(_,i)) -> Some (i,id.CAst.v) | (None,_) -> None) all let do_scheme l = let ischeme,escheme = split_scheme l in @@ -450,7 +449,7 @@ let fold_left' f = function let mk_coq_and sigma = Evarutil.new_global sigma (Coqlib.build_coq_and ()) let mk_coq_conj sigma = Evarutil.new_global sigma (Coqlib.build_coq_conj ()) - + let build_combined_scheme env schemes = let evdref = ref (Evd.from_env env) in let defs = List.map (fun cst -> @@ -492,18 +491,19 @@ let build_combined_scheme env schemes = (!evdref, body, typ) let do_combined_scheme name schemes = + let open CAst in let csts = - List.map (fun x -> - let refe = Ident x in - let qualid = qualid_of_reference refe in - try Nametab.locate_constant (snd qualid) - with Not_found -> user_err Pp.(pr_qualid (snd qualid) ++ str " is not declared.")) + List.map (fun {CAst.loc;v} -> + let refe = Ident (Loc.tag ?loc v) in + let qualid = qualid_of_reference refe in + try Nametab.locate_constant (snd qualid) + with Not_found -> user_err Pp.(pr_qualid (snd qualid) ++ str " is not declared.")) schemes in let sigma,body,typ = build_combined_scheme (Global.env ()) csts in let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in - ignore (define (snd name) UserIndividualRequest sigma proof_output (Some typ)); - fixpoint_message None [snd name] + ignore (define name.v UserIndividualRequest sigma proof_output (Some typ)); + fixpoint_message None [name.v] (**********************************************************************) diff --git a/vernac/indschemes.mli b/vernac/indschemes.mli index 4b31389ab..8658d85f6 100644 --- a/vernac/indschemes.mli +++ b/vernac/indschemes.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Loc open Names open Constr open Environ @@ -31,17 +30,17 @@ val declare_rewriting_schemes : inductive -> unit (** Mutual Minimality/Induction scheme *) val do_mutual_induction_scheme : - (Id.t located * bool * inductive * Sorts.family) list -> unit + (Misctypes.lident * bool * inductive * Sorts.family) list -> unit (** Main calls to interpret the Scheme command *) -val do_scheme : (Id.t located option * scheme) list -> unit +val do_scheme : (Misctypes.lident option * scheme) list -> unit (** Combine a list of schemes into a conjunction of them *) val build_combined_scheme : env -> Constant.t list -> Evd.evar_map * constr * types -val do_combined_scheme : Id.t located -> Id.t located list -> unit +val do_combined_scheme : Misctypes.lident -> Misctypes.lident list -> unit (** Hook called at each inductive type definition *) diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 57436784b..7661fff6d 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -214,7 +214,7 @@ let fresh_name_for_anonymous_theorem () = let avoid = Id.Set.of_list (Proof_global.get_all_proof_names ()) in next_global_ident_away default_thm_id avoid -let check_name_freshness locality (loc,id) : unit = +let check_name_freshness locality {CAst.loc;v=id} : unit = (* We check existence here: it's a bit late at Qed time *) if Nametab.exists_cci (Lib.make_path id) || is_section_variable id || locality == Global && Nametab.exists_cci (Lib.make_path_except_section id) @@ -339,7 +339,7 @@ let universe_proof_terminator compute_guard hook = (hook (Some (proof.Proof_global.universes))) is_opaque in begin match idopt with | None -> save_named ~export_seff proof - | Some (_,id) -> save_anonymous ~export_seff proof id + | Some { CAst.v = id } -> save_anonymous ~export_seff proof id end end @@ -444,7 +444,7 @@ let start_proof_com ?inference_hook kind thms hook = let ids = List.map RelDecl.get_name ctx in check_name_freshness (pi1 kind) id; (* XXX: The nf_evar is critical !! *) - evd, (snd id, + evd, (id.CAst.v, (Evarutil.nf_evar evd (EConstr.it_mkProd_or_LetIn t' ctx), (ids, imps @ lift_implicits (Context.Rel.nhyps ctx) imps')))) evd thms in diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index bcffe640c..f63206216 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -89,7 +89,7 @@ let pr_grammar = function (* Parse a format (every terminal starting with a letter or a single quote (except a single quote alone) must be quoted) *) -let parse_format ((loc, str) : lstring) = +let parse_format ({CAst.loc;v=str} : Misctypes.lstring) = let len = String.length str in (* TODO: update the line of the location when the string contains newlines *) let make_loc i j = Option.map (Loc.shift_loc (i+1) (j-len)) loc in @@ -789,7 +789,7 @@ type notation_modifier = { only_parsing : bool; only_printing : bool; compat : Flags.compat_version option; - format : string Loc.located option; + format : Misctypes.lstring option; extra : (string * string) list; } @@ -847,7 +847,7 @@ let interp_modifiers modl = let open NotationMods in | SetFormat ("text",s) :: l -> if not (Option.is_empty acc.format) then user_err Pp.(str "A format is given more than once."); interp { acc with format = Some s; } l - | SetFormat (k,(_,s)) :: l -> + | SetFormat (k,{CAst.v=s}) :: l -> interp { acc with extra = (k,s)::acc.extra; } l in interp default modl @@ -1101,7 +1101,7 @@ module SynData = struct only_parsing : bool; only_printing : bool; compat : Flags.compat_version option; - format : string Loc.located option; + format : Misctypes.lstring option; extra : (string * string) list; (* XXX: Callback to printing, must remove *) @@ -1400,7 +1400,7 @@ let add_notation_interpretation_core local df env ?(impls=empty_internalization_ (* Notations without interpretation (Reserved Notation) *) -let add_syntax_extension local ((loc,df),mods) = let open SynData in +let add_syntax_extension local ({CAst.loc;v=df},mods) = let open SynData in let psd = compute_pure_syntax_data df mods in let sy_rules = make_syntax_rules {psd with compat = None} in Flags.if_verbose (List.iter (fun (f,x) -> f x)) psd.msgs; @@ -1408,11 +1408,11 @@ let add_syntax_extension local ((loc,df),mods) = let open SynData in (* Notations with only interpretation *) -let add_notation_interpretation env ((loc,df),c,sc) = +let add_notation_interpretation env ({CAst.loc;v=df},c,sc) = let df' = add_notation_interpretation_core false df env c sc false false None in Dumpglob.dump_notation (loc,df') sc true -let set_notation_for_interpretation env impls ((_,df),c,sc) = +let set_notation_for_interpretation env impls ({CAst.v=df},c,sc) = (try ignore (Flags.silently (fun () -> add_notation_interpretation_core false df env ~impls c sc false false None) ()); with NoSyntaxRule -> @@ -1421,7 +1421,7 @@ let set_notation_for_interpretation env impls ((_,df),c,sc) = (* Main entry point *) -let add_notation local env c ((loc,df),modifiers) sc = +let add_notation local env c ({CAst.loc;v=df},modifiers) sc = let df' = if no_syntax_modifiers modifiers then (* No syntax data: try to rely on a previously declared rule *) @@ -1448,13 +1448,13 @@ let add_notation_extra_printing_rule df k v = let inject_var x = CAst.make @@ CRef (Ident (Loc.tag @@ Id.of_string x),None) -let add_infix local env ((loc,inf),modifiers) pr sc = +let add_infix local env ({CAst.loc;v=inf},modifiers) pr sc = check_infix_modifiers modifiers; (* check the precedence *) let metas = [inject_var "x"; inject_var "y"] in let c = mkAppC (pr,metas) in - let df = "x "^(quote_notation_token inf)^" y" in - add_notation local env c ((loc,df),modifiers) sc + let df = CAst.make ?loc @@ "x "^(quote_notation_token inf)^" y" in + add_notation local env c (df,modifiers) sc (**********************************************************************) (* Delimiters and classes bound to scopes *) diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli index 9137f7a7e..7740604c3 100644 --- a/vernac/metasyntax.mli +++ b/vernac/metasyntax.mli @@ -12,6 +12,7 @@ open Notation open Constrexpr open Notation_term open Environ +open Misctypes val add_token_obj : string -> unit diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 58e4b00fc..e4bcbc4bb 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -295,10 +295,10 @@ type obligation = type obligations = (obligation array * int) type fixpoint_kind = - | IsFixpoint of (Id.t Loc.located option * Constrexpr.recursion_order_expr) list + | IsFixpoint of (Misctypes.lident option * Constrexpr.recursion_order_expr) list | IsCoFixpoint -type notations = (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list +type notations = (Misctypes.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list type program_info_aux = { prg_name: Id.t; @@ -500,7 +500,7 @@ let rec lam_index n t acc = let compute_possible_guardness_evidences (n,_) fixbody fixtype = match n with - | Some (loc, n) -> [lam_index n fixbody 0] + | Some { CAst.loc; v = n } -> [lam_index n fixbody 0] | None -> (* If recursive argument was not given by user, we try all args. An earlier approach was to look only for inductive arguments, diff --git a/vernac/obligations.mli b/vernac/obligations.mli index bdc97d48c..0ec127152 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -61,10 +61,10 @@ val add_definition : Names.Id.t -> ?term:constr -> types -> ?hook:(UState.t -> unit) Lemmas.declaration_hook -> ?opaque:bool -> obligation_info -> progress type notations = - (Vernacexpr.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list + (Misctypes.lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list type fixpoint_kind = - | IsFixpoint of (Id.t Loc.located option * Constrexpr.recursion_order_expr) list + | IsFixpoint of (Misctypes.lident option * Constrexpr.recursion_order_expr) list | IsCoFixpoint val add_mutual_definitions : diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml index ffe99cfd8..8422baf57 100644 --- a/vernac/proof_using.ml +++ b/vernac/proof_using.ml @@ -51,7 +51,7 @@ let rec process_expr env e ty = let rec aux = function | SsEmpty -> Id.Set.empty | SsType -> set_of_type env ty - | SsSingl (_,id) -> set_of_id env id + | SsSingl { CAst.v = id } -> set_of_id env id | SsUnion(e1,e2) -> Id.Set.union (aux e1) (aux e2) | SsSubstr(e1,e2) -> Id.Set.diff (aux e1) (aux e2) | SsCompl e -> Id.Set.diff (full_set env) (aux e) diff --git a/vernac/record.ml b/vernac/record.ml index 16b95a5ef..1140e3d37 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -62,7 +62,7 @@ let _ = let interp_fields_evars env sigma impls_env nots l = List.fold_left2 - (fun (env, sigma, uimpls, params, impls) no ((loc, i), b, t) -> + (fun (env, sigma, uimpls, params, impls) no ({CAst.loc;v=i}, b, t) -> let sigma, (t', impl) = interp_type_evars_impls env sigma ~impls t in let sigma, b' = Option.cata (fun x -> on_snd (fun x -> Some (fst x)) @@ @@ -92,8 +92,9 @@ let compute_constructor_level evars env l = let binder_of_decl = function | Vernacexpr.AssumExpr(n,t) -> (n,None,t) - | Vernacexpr.DefExpr(n,c,t) -> (n,Some c, match t with Some c -> c - | None -> CAst.make ?loc:(fst n) @@ CHole (None, Misctypes.IntroAnonymous, None)) + | Vernacexpr.DefExpr(n,c,t) -> + (n,Some c, match t with Some c -> c + | None -> CAst.make ?loc:n.CAst.loc @@ CHole (None, Misctypes.IntroAnonymous, None)) let binders_of_decls = List.map binder_of_decl @@ -101,7 +102,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs = let env0 = Global.env () in let sigma, decl = Univdecls.interp_univ_decl_opt env0 pl in let _ = - let error bk (loc, name) = + let error bk {CAst.loc; v=name} = match bk, name with | Default _, Anonymous -> user_err ?loc ~hdr:"record" (str "Record parameters must be named") @@ -110,7 +111,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs = List.iter (function CLocalDef (b, _, _) -> error default_binder_kind b | CLocalAssum (ls, bk, ce) -> List.iter (error bk) ls - | CLocalPattern (loc,(_,_)) -> + | CLocalPattern {CAst.loc} -> Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters.")) ps in let sigma, (impls_env, ((env1,newps), imps)) = interp_context_evars env0 sigma ps in @@ -571,13 +572,13 @@ open Vernacexpr (* [fs] corresponds to fields and [ps] to parameters; [coers] is a list telling if the corresponding fields must me declared as coercions or subinstances. *) -let definition_structure (kind,cum,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,idbuild,s) = +let definition_structure (kind,cum,poly,finite,(is_coe,({CAst.loc;v=idstruc},pl)),ps,cfs,idbuild,s) = let cfs,notations = List.split cfs in let cfs,priorities = List.split cfs in let coers,fs = List.split cfs in let extract_name acc = function - Vernacexpr.AssumExpr((_,Name id),_) -> id::acc - | Vernacexpr.DefExpr ((_,Name id),_,_) -> id::acc + Vernacexpr.AssumExpr({CAst.v=Name id},_) -> id::acc + | Vernacexpr.DefExpr ({CAst.v=Name id},_,_) -> id::acc | _ -> acc in let allnames = idstruc::(List.fold_left extract_name [] fs) in let () = match List.duplicates Id.equal allnames with diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index fa457c895..689d7a423 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -10,6 +10,7 @@ open Pp open CErrors +open CAst open Util open Names open Nameops @@ -471,13 +472,13 @@ let vernac_definition_hook p = function | SubClass -> Class.add_subclass_hook p | _ -> no_hook -let vernac_definition ~atts discharge kind ((loc, id), pl) def = +let vernac_definition ~atts discharge kind ({loc;v=id}, pl) def = let local = enforce_locality_exp atts.locality discharge in let hook = vernac_definition_hook atts.polymorphic kind in let () = match id with | Anonymous -> () - | Name n -> let lid = (loc, n) in + | Name n -> let lid = CAst.make ?loc n in match local with | Discharge -> Dumpglob.dump_definition lid true "var" | Local | Global -> Dumpglob.dump_definition lid false "def" @@ -491,7 +492,7 @@ let vernac_definition ~atts discharge kind ((loc, id), pl) def = (match def with | ProveBody (bl,t) -> (* local binders, typ *) start_proof_and_print (local, atts.polymorphic, DefinitionBody kind) - [((loc, name), pl), (bl, t)] hook + [(CAst.make ?loc name, pl), (bl, t)] hook | DefineBody (bl,red_option,c,typ_opt) -> let red_option = match red_option with | None -> None @@ -546,14 +547,14 @@ let should_treat_as_cumulative cum poly = let vernac_record cum k poly finite struc binders sort nameopt cfs = let is_cumulative = should_treat_as_cumulative cum poly in let const = match nameopt with - | None -> add_prefix "Build_" (snd (fst (snd struc))) - | Some (_,id as lid) -> + | None -> add_prefix "Build_" (fst (snd struc)).v + | Some ({v=id} as lid) -> Dumpglob.dump_definition lid false "constr"; id in if Dumpglob.dump () then ( Dumpglob.dump_definition (fst (snd struc)) false "rec"; List.iter (fun (((_, x), _), _) -> match x with - | Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj" + | Vernacexpr.AssumExpr ({loc;v=Name id}, _) -> Dumpglob.dump_definition (make ?loc id) false "proj" | _ -> ()) cfs); ignore(Record.definition_structure (k,is_cumulative,poly,finite,struc,binders,cfs,const,sort)) @@ -582,9 +583,9 @@ let vernac_inductive ~atts cum lo finite indl = atts.polymorphic finite id bl c oc fs | [ ( id , bl , c , Class _, Constructors [l]), [] ] -> let f = - let (coe, ((loc, id), ce)) = l in + let (coe, ({loc;v=id}, ce)) = l in let coe' = if coe then Some true else None in - (((coe', AssumExpr ((loc, Name id), ce)), None), []) + (((coe', AssumExpr ((make ?loc @@ Name id), ce)), None), []) in vernac_record cum (Class true) atts.polymorphic finite id bl c None [f] | [ ( _ , _, _, Class _, Constructors _), [] ] -> user_err Pp.(str "Inductive classes not supported") @@ -637,7 +638,7 @@ let vernac_scheme l = let vernac_combined_scheme lid l = if Dumpglob.dump () then (Dumpglob.dump_definition lid false "def"; - List.iter (fun lid -> dump_global (Misctypes.AN (Ident lid))) l); + List.iter (fun {loc;v=id} -> dump_global (Misctypes.AN (Ident (Loc.tag ?loc id)))) l); Indschemes.do_combined_scheme lid l let vernac_universe ~atts l = @@ -660,7 +661,7 @@ let vernac_constraint ~atts l = let vernac_import export refl = Library.import_module export (List.map qualid_of_reference refl) -let vernac_declare_module export (loc, id) binders_ast mty_ast = +let vernac_declare_module export {loc;v=id} binders_ast mty_ast = (* We check the state of the system (in section, in module type) and what module information is supplied *) if Lib.sections_are_opened () then @@ -678,7 +679,7 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast = Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared"); Option.iter (fun export -> vernac_import export [Ident (Loc.tag id)]) export -let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = +let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mty_ast_o mexpr_ast_l = (* We check the state of the system (in section, in module type) and what module information is supplied *) if Lib.sections_are_opened () then @@ -689,7 +690,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = let binders_ast,argsexport = List.fold_right (fun (export,idl,ty) (args,argsexport) -> - (idl,ty)::args, (List.map (fun (_,i) -> export,i)idl)@argsexport) binders_ast + (idl,ty)::args, (List.map (fun {v=i} -> export,i)idl)@argsexport) binders_ast ([],[]) in let mp = Declaremods.start_module Modintern.interp_module_ast @@ -719,13 +720,13 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = Option.iter (fun export -> vernac_import export [Ident (Loc.tag id)]) export -let vernac_end_module export (loc,id as lid) = +let vernac_end_module export {loc;v=id} = let mp = Declaremods.end_module () in Dumpglob.dump_modref ?loc mp "mod"; Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is defined"); - Option.iter (fun export -> vernac_import export [Ident lid]) export + Option.iter (fun export -> vernac_import export [Ident (Loc.tag ?loc id)]) export -let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = +let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l = if Lib.sections_are_opened () then user_err Pp.(str "Modules and Module Types are not allowed inside sections."); @@ -735,7 +736,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = let binders_ast,argsexport = List.fold_right (fun (export,idl,ty) (args,argsexport) -> - (idl,ty)::args, (List.map (fun (_,i) -> export,i)idl)@argsexport) binders_ast + (idl,ty)::args, (List.map (fun {v=i} -> export,i)idl)@argsexport) binders_ast ([],[]) in let mp = @@ -765,7 +766,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = Flags.if_verbose Feedback.msg_info (str "Module Type " ++ Id.print id ++ str " is defined") -let vernac_end_modtype (loc,id) = +let vernac_end_modtype {loc;v=id} = let mp = Declaremods.end_modtype () in Dumpglob.dump_modref ?loc mp "modtype"; Flags.if_verbose Feedback.msg_info (str "Module Type " ++ Id.print id ++ str " is defined") @@ -778,21 +779,21 @@ let vernac_include l = (* Sections *) -let vernac_begin_section (_, id as lid) = +let vernac_begin_section ({v=id} as lid) = Proof_global.check_no_pending_proof (); Dumpglob.dump_definition lid true "sec"; Lib.open_section id -let vernac_end_section (loc,_) = +let vernac_end_section {CAst.loc} = Dumpglob.dump_reference ?loc (DirPath.to_string (Lib.current_dirpath true)) "<>" "sec"; Lib.close_section () -let vernac_name_sec_hyp (_,id) set = Proof_using.name_set id set +let vernac_name_sec_hyp {v=id} set = Proof_using.name_set id set (* Dispatcher of the "End" command *) -let vernac_end_segment (_,id as lid) = +let vernac_end_segment ({v=id} as lid) = Proof_global.check_no_pending_proof (); match Lib.find_opening_node id with | Lib.OpenedModule (false,export,_,_) -> vernac_end_module export lid @@ -975,7 +976,7 @@ let vernac_hints ~atts lb h = let vernac_syntactic_definition ~atts lid x y = Dumpglob.dump_definition lid false "syndef"; let local = enforce_module_locality atts.locality in - Metasyntax.add_syntactic_definition (Global.env()) (snd lid) x local y + Metasyntax.add_syntactic_definition (Global.env()) lid.v x local y let vernac_declare_implicits ~atts r l = let local = make_section_locality atts.locality in @@ -1211,7 +1212,7 @@ let vernac_arguments ~atts reference args more_implicits nargs_for_red flags = end; if scopes_specified || clear_scopes_flag then begin - let scopes = List.map (Option.map (fun (loc,k) -> + let scopes = List.map (Option.map (fun {loc;v=k} -> try ignore (Notation.find_scope k); k with UserError _ -> Notation.find_delimiters_scope ?loc k)) scopes @@ -1824,7 +1825,7 @@ let vernac_locate = function let vernac_register id r = if Proof_global.there_are_pending_proofs () then user_err Pp.(str "Cannot register a primitive while in proof editing mode."); - let kn = Constrintern.global_reference (snd id) in + let kn = Constrintern.global_reference id.v in if not (isConstRef kn) then user_err Pp.(str "Register inline: a constant is expected"); match r with @@ -2015,7 +2016,7 @@ let interp ?proof ~atts ~st c = | VernacImport (export,qidl) -> vernac_import export qidl | VernacCanonical qid -> vernac_canonical qid | VernacCoercion (r,s,t) -> vernac_coercion ~atts r s t - | VernacIdentityCoercion ((_,id),s,t) -> + | VernacIdentityCoercion ({v=id},s,t) -> vernac_identity_coercion ~atts id s t (* Type classes *) @@ -2233,12 +2234,12 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) = aux ~polymorphism ~atts v | VernacFail v -> with_fail st true (fun () -> control v) | VernacTimeout (n,v) -> - current_timeout := Some n; - control v - | VernacRedirect (s, (_,v)) -> - Topfmt.with_output_to_file s control v - | VernacTime (batch, (_loc,v)) -> - System.with_time ~batch control v; + current_timeout := Some n; + control v + | VernacRedirect (s, {v}) -> + Topfmt.with_output_to_file s control v + | VernacTime (batch, {v}) -> + System.with_time ~batch control v; and aux ~polymorphism ~atts : _ -> unit = function diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml index 3932d1c7b..172a20b7a 100644 --- a/vernac/vernacprop.ml +++ b/vernac/vernacprop.ml @@ -13,15 +13,15 @@ open Vernacexpr let rec under_control = function | VernacExpr (_, c) -> c - | VernacRedirect (_,(_,c)) - | VernacTime (_,(_,c)) + | VernacRedirect (_,{CAst.v=c}) + | VernacTime (_,{CAst.v=c}) | VernacFail c | VernacTimeout (_,c) -> under_control c let rec has_Fail = function | VernacExpr _ -> false - | VernacRedirect (_,(_,c)) - | VernacTime (_,(_,c)) + | VernacRedirect (_,{CAst.v=c}) + | VernacTime (_,{CAst.v=c}) | VernacTimeout (_,c) -> has_Fail c | VernacFail _ -> true @@ -38,8 +38,8 @@ let is_navigation_vernac c = is_navigation_vernac_expr (under_control c) let rec is_deep_navigation_vernac = function - | VernacTime (_,(_,c)) -> is_deep_navigation_vernac c - | VernacRedirect (_, (_,c)) + | VernacTime (_,{CAst.v=c}) -> is_deep_navigation_vernac c + | VernacRedirect (_, {CAst.v=c}) | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c | VernacExpr _ -> false |