diff options
167 files changed, 1547 insertions, 1262 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 9e87d2ca7..3a762b42a 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -53,6 +53,9 @@ /doc/ @maximedenes # Secondary maintainer @silene @Zimmi48 +/doc/tools/coqrst/ @maximedenes +# Secondary maintainer @cpitclaudel + /man/ @silene # Secondary maintainer @maximedenes diff --git a/.travis.yml b/.travis.yml index 86a2aea66..627334690 100644 --- a/.travis.yml +++ b/.travis.yml @@ -82,11 +82,6 @@ matrix: - TEST_TARGET="ci-coquelicot" - if: NOT (type = pull_request) env: - - TEST_TARGET="ci-elpi" EXTRA_OPAM="elpi" - # ppx_tools_versioned requires a specific version findlib - - FINDLIB_VER="" - - if: NOT (type = pull_request) - env: - TEST_TARGET="ci-equations" - if: NOT (type = pull_request) env: @@ -28,6 +28,12 @@ Tactics - The `simple apply` tactic now respects the `Opaque` flag when called from Ltac (`auto` still does not respect it). +- Tactic `constr_eq` now adds universe constraints needed for the + identity to the context (it used to ignore them). New tactic + `constr_eq_strict` checks that the required constraints already hold + without adding new ones. Preexisting tactic `constr_eq_nounivs` can + still be used if you really want to ignore universe constraints. + Tools - Coq_makefile lets one override or extend the following variables from diff --git a/INSTALL.ide b/INSTALL.ide index 26c192baa..c4da84048 100644 --- a/INSTALL.ide +++ b/INSTALL.ide @@ -22,7 +22,7 @@ Else, read the rest of this document to compile your own CoqIde. COMPILATION REQUIREMENTS -- OCaml >= 4.02.1 with native threads support. +- OCaml >= 4.02.3 with native threads support. - make world must succeed. - The graphical toolkit GTK+ 2.x. See http://www.gtk.org. The official supported version is at least 2.24.x. diff --git a/checker/check.mllib b/checker/check.mllib index f79ba66e3..139fa765b 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -3,7 +3,6 @@ Coq_config Analyze Hook Terminal -Canary Hashset Hashcons CSet diff --git a/checker/cic.mli b/checker/cic.mli index 7ec345768..3304b032e 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -211,8 +211,6 @@ type projection_body = { proj_npars : int; proj_arg : int; proj_type : constr; (* Type under params *) - proj_eta : constr * constr; (* Eta-expanded term and type *) - proj_body : constr; (* For compatibility, the match version *) } type constant_def = @@ -241,7 +239,6 @@ type constant_body = { const_type : constr; const_body_code : to_patch_substituted; const_universes : constant_universes; - const_proj : bool; const_inline_code : bool; const_typing_flags : typing_flags; } diff --git a/checker/environ.ml b/checker/environ.ml index 809150cea..3d5fac806 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -166,9 +166,6 @@ let evaluable_constant cst env = try let _ = constant_value env (cst, Univ.Instance.empty) in true with Not_found | NotEvaluableConst _ -> false -let is_projection cst env = - (lookup_constant cst env).const_proj - let lookup_projection p env = Cmap_env.find (Projection.constant p) env.env_globals.env_projections diff --git a/checker/environ.mli b/checker/environ.mli index 4a7597249..acb29d7d2 100644 --- a/checker/environ.mli +++ b/checker/environ.mli @@ -58,7 +58,6 @@ exception NotEvaluableConst of const_evaluation_result val constant_value : env -> Constant.t puniverses -> constr val evaluable_constant : Constant.t -> env -> bool -val is_projection : Constant.t -> env -> bool val lookup_projection : Projection.t -> env -> projection_body (* Inductives *) diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 5c672d04a..f4ae02084 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -130,9 +130,7 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= check (==) (fun x -> x.proj_npars); check (==) (fun x -> x.proj_arg); check (eq_constr) (fun x -> x.proj_type); - check (eq_constr) (fun x -> fst x.proj_eta); - check (eq_constr) (fun x -> snd x.proj_eta); - check (eq_constr) (fun x -> x.proj_body); true + true in let check_inductive_type t1 t2 = diff --git a/checker/values.ml b/checker/values.ml index 67032bd1b..31e65729b 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -15,7 +15,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 fb80632357e3ffa988c6bba3fa6ade64 checker/cic.mli +MD5 07651f61f86d91b22ff7056c6a8d86bc checker/cic.mli *) @@ -91,7 +91,7 @@ let rec v_mp = Sum("module_path",0, [|[|v_dp|]; [|v_uid|]; [|v_mp;v_id|]|]) -let v_kn = v_tuple "kernel_name" [|Any;v_mp;v_dp;v_id;Int|] +let v_kn = v_tuple "kernel_name" [|v_mp;v_dp;v_id;Int|] let v_cst = v_sum "cst|mind" 0 [|[|v_kn|];[|v_kn;v_kn|]|] let v_ind = v_tuple "inductive" [|v_cst;Int|] let v_cons = v_tuple "constructor" [|v_ind;Int|] @@ -225,9 +225,7 @@ let v_cst_def = let v_projbody = v_tuple "projection_body" - [|v_cst;Int;Int;v_constr; - v_tuple "proj_eta" [|v_constr;v_constr|]; - v_constr|] + [|v_cst;Int;Int;v_constr|] let v_typing_flags = v_tuple "typing_flags" [|v_bool; v_bool; v_oracle|] @@ -241,7 +239,6 @@ let v_cb = v_tuple "constant_body" Any; v_const_univs; v_bool; - v_bool; v_typing_flags|] let v_recarg = v_sum "recarg" 1 (* Norec *) diff --git a/clib/cArray.ml b/clib/cArray.ml index b26dae729..fc87a74cf 100644 --- a/clib/cArray.ml +++ b/clib/cArray.ml @@ -280,7 +280,7 @@ let fold_left2_i f a v1 v2 = let rec fold a n = if n >= lv1 then a else fold (f n a (uget v1 n) (uget v2 n)) (succ n) in - if Array.length v2 <> lv1 then invalid_arg "Array.fold_left2"; + if Array.length v2 <> lv1 then invalid_arg "Array.fold_left2_i"; fold a 0 let fold_left3 f a v1 v2 v3 = @@ -290,7 +290,7 @@ let fold_left3 f a v1 v2 v3 = else fold (f a (uget v1 n) (uget v2 n) (uget v3 n)) (succ n) in if Array.length v2 <> lv1 || Array.length v3 <> lv1 then - invalid_arg "Array.fold_left2"; + invalid_arg "Array.fold_left3"; fold a 0 let fold_left4 f a v1 v2 v3 v4 = diff --git a/clib/canary.ml b/clib/canary.ml deleted file mode 100644 index b8b79ed7f..000000000 --- a/clib/canary.ml +++ /dev/null @@ -1,28 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -type t = Obj.t - -let obj = Obj.new_block Obj.closure_tag 0 - (** This is an empty closure block. In the current implementation, it is - sufficient to allow marshalling but forbid equality. Sadly still allows - hash. *) - (** FIXME : use custom blocks somehow. *) - -module type Obj = sig type t end - -module Make(M : Obj) = -struct - type canary = t - type t = (canary * M.t) - - let prj (_, x) = x - let inj x = (obj, x) -end diff --git a/clib/canary.mli b/clib/canary.mli deleted file mode 100644 index d993eabcf..000000000 --- a/clib/canary.mli +++ /dev/null @@ -1,27 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -type t -(** Type of canaries. Canaries are used to ensure that an object does not use - generic operations. *) - -val obj : t -(** Canary. In the current implementation, this object is marshallable, - forbids generic comparison but still allows generic hashes. *) - -module type Obj = sig type t end - -module Make(M : Obj) : -sig - type t - val prj : t -> M.t - val inj : M.t -> t -end -(** Adds a canary to any type. *) diff --git a/clib/clib.mllib b/clib/clib.mllib index c9b4d72fc..afece4074 100644 --- a/clib/clib.mllib +++ b/clib/clib.mllib @@ -1,4 +1,3 @@ -Canary CObj CEphemeron diff --git a/clib/dyn.ml b/clib/dyn.ml index e9b041988..6c4576724 100644 --- a/clib/dyn.ml +++ b/clib/dyn.ml @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -module type TParam = +module type ValueS = sig type 'a t end @@ -16,40 +16,38 @@ end module type MapS = sig type t - type 'a obj type 'a key + type 'a value val empty : t - val add : 'a key -> 'a obj -> t -> t + val add : 'a key -> 'a value -> t -> t val remove : 'a key -> t -> t - val find : 'a key -> t -> 'a obj + val find : 'a key -> t -> 'a value val mem : 'a key -> t -> bool - type any = Any : 'a key * 'a obj -> any - - type map = { map : 'a. 'a key -> 'a obj -> 'a obj } + type map = { map : 'a. 'a key -> 'a value -> 'a value } val map : map -> t -> t + type any = Any : 'a key * 'a value -> any val iter : (any -> unit) -> t -> unit val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r end module type PreS = sig -type 'a tag -type t = Dyn : 'a tag * 'a -> t - -val create : string -> 'a tag -val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option -val repr : 'a tag -> string + type 'a tag + type t = Dyn : 'a tag * 'a -> t -type any = Any : 'a tag -> any + val create : string -> 'a tag + val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option + val repr : 'a tag -> string -val name : string -> any option + val dump : unit -> (int * string) list -module Map(M : TParam) : MapS with type 'a obj = 'a M.t with type 'a key = 'a tag - -val dump : unit -> (int * string) list + type any = Any : 'a tag -> any + val name : string -> any option + module Map(Value : ValueS) : + MapS with type 'a key = 'a tag and type 'a value = 'a Value.t end module type S = @@ -57,104 +55,100 @@ sig include PreS module Easy : sig - val make_dyn_tag : string -> ('a -> t) * (t -> 'a) * 'a tag val make_dyn : string -> ('a -> t) * (t -> 'a) val inj : 'a -> 'a tag -> t val prj : t -> 'a tag -> 'a option end - end module Make () = struct -module Self : PreS = struct -(* Dynamics, programmed with DANGER !!! *) - -type 'a tag = int -type t = Dyn : 'a tag * 'a -> t - -type any = Any : 'a tag -> any - -let dyntab = ref (Int.Map.empty : string Int.Map.t) -(** Instead of working with tags as strings, which are costly, we use their - hash. We ensure unicity of the hash in the [create] function. If ever a - collision occurs, which is unlikely, it is sufficient to tweak the offending - dynamic tag. *) - -let create (s : string) = - let hash = Hashtbl.hash s in - let () = - if Int.Map.mem hash !dyntab then - let old = Int.Map.find hash !dyntab in - let () = Printf.eprintf "Dynamic tag collision: %s vs. %s\n%!" s old in +module Self : PreS = struct + (* Dynamics, programmed with DANGER !!! *) + + type 'a tag = int + + type t = Dyn : 'a tag * 'a -> t + + type any = Any : 'a tag -> any + + let dyntab = ref (Int.Map.empty : string Int.Map.t) + (** Instead of working with tags as strings, which are costly, we use their + hash. We ensure unicity of the hash in the [create] function. If ever a + collision occurs, which is unlikely, it is sufficient to tweak the offending + dynamic tag. *) + + let create (s : string) = + let hash = Hashtbl.hash s in + let () = + if Int.Map.mem hash !dyntab then + let old = Int.Map.find hash !dyntab in + let () = Printf.eprintf "Dynamic tag collision: %s vs. %s\n%!" s old in + assert false + in + let () = dyntab := Int.Map.add hash s !dyntab in + hash + + let eq : 'a 'b. 'a tag -> 'b tag -> ('a, 'b) CSig.eq option = + fun h1 h2 -> if Int.equal h1 h2 then Some (Obj.magic CSig.Refl) else None + + let repr s = + try Int.Map.find s !dyntab + with Not_found -> + let () = Printf.eprintf "Unknown dynamic tag %i\n%!" s in assert false - in - let () = dyntab := Int.Map.add hash s !dyntab in - hash - -let eq : 'a 'b. 'a tag -> 'b tag -> ('a, 'b) CSig.eq option = - fun h1 h2 -> if Int.equal h1 h2 then Some (Obj.magic CSig.Refl) else None - -let repr s = - try Int.Map.find s !dyntab - with Not_found -> - let () = Printf.eprintf "Unknown dynamic tag %i\n%!" s in - assert false - -let name s = - let hash = Hashtbl.hash s in - if Int.Map.mem hash !dyntab then Some (Any hash) else None - -let dump () = Int.Map.bindings !dyntab - -module Map(M : TParam) = -struct -type t = Obj.t M.t Int.Map.t -type 'a obj = 'a M.t -type 'a key = 'a tag -let cast : 'a M.t -> 'b M.t = Obj.magic -let empty = Int.Map.empty -let add tag v m = Int.Map.add tag (cast v) m -let remove tag m = Int.Map.remove tag m -let find tag m = cast (Int.Map.find tag m) -let mem = Int.Map.mem - -type any = Any : 'a tag * 'a M.t -> any - -type map = { map : 'a. 'a tag -> 'a M.t -> 'a M.t } -let map f m = Int.Map.mapi f.map m - -let iter f m = Int.Map.iter (fun k v -> f (Any (k, v))) m -let fold f m accu = Int.Map.fold (fun k v accu -> f (Any (k, v)) accu) m accu -end + let name s = + let hash = Hashtbl.hash s in + if Int.Map.mem hash !dyntab then Some (Any hash) else None + + let dump () = Int.Map.bindings !dyntab + + module Map(Value: ValueS) = + struct + type t = Obj.t Value.t Int.Map.t + type 'a key = 'a tag + type 'a value = 'a Value.t + let cast : 'a value -> 'b value = Obj.magic + let empty = Int.Map.empty + let add tag v m = Int.Map.add tag (cast v) m + let remove tag m = Int.Map.remove tag m + let find tag m = cast (Int.Map.find tag m) + let mem = Int.Map.mem + + type map = { map : 'a. 'a tag -> 'a value -> 'a value } + let map f m = Int.Map.mapi f.map m + + type any = Any : 'a tag * 'a value -> any + let iter f m = Int.Map.iter (fun k v -> f (Any (k, v))) m + let fold f m accu = Int.Map.fold (fun k v accu -> f (Any (k, v)) accu) m accu + end end include Self module Easy = struct - -(* now tags are opaque, we can do the trick *) -let make_dyn_tag (s : string) = - (fun (type a) (tag : a tag) -> - let infun : (a -> t) = fun x -> Dyn (tag, x) in - let outfun : (t -> a) = fun (Dyn (t, x)) -> - match eq tag t with - | None -> assert false - | Some CSig.Refl -> x - in - infun, outfun, tag) - (create s) - -let make_dyn (s : string) = - let inf, outf, _ = make_dyn_tag s in inf, outf - -let inj x tag = Dyn(tag,x) -let prj : type a. t -> a tag -> a option = + (* now tags are opaque, we can do the trick *) + let make_dyn_tag (s : string) = + (fun (type a) (tag : a tag) -> + let infun : (a -> t) = fun x -> Dyn (tag, x) in + let outfun : (t -> a) = fun (Dyn (t, x)) -> + match eq tag t with + | None -> assert false + | Some CSig.Refl -> x + in + infun, outfun, tag) + (create s) + + let make_dyn (s : string) = + let inf, outf, _ = make_dyn_tag s in inf, outf + + let inj x tag = Dyn(tag,x) + let prj : type a. t -> a tag -> a option = fun (Dyn(tag',x)) tag -> - match eq tag tag' with - | None -> None - | Some CSig.Refl -> Some x + match eq tag tag' with + | None -> None + | Some CSig.Refl -> Some x end end diff --git a/clib/dyn.mli b/clib/dyn.mli index 51d309142..ff9762bd6 100644 --- a/clib/dyn.mli +++ b/clib/dyn.mli @@ -10,7 +10,7 @@ (** Dynamically typed values *) -module type TParam = +module type ValueS = sig type 'a t end @@ -18,51 +18,66 @@ end module type MapS = sig type t - type 'a obj type 'a key + type 'a value val empty : t - val add : 'a key -> 'a obj -> t -> t + val add : 'a key -> 'a value -> t -> t val remove : 'a key -> t -> t - val find : 'a key -> t -> 'a obj + val find : 'a key -> t -> 'a value val mem : 'a key -> t -> bool - type any = Any : 'a key * 'a obj -> any - - type map = { map : 'a. 'a key -> 'a obj -> 'a obj } + type map = { map : 'a. 'a key -> 'a value -> 'a value } val map : map -> t -> t + type any = Any : 'a key * 'a value -> any val iter : (any -> unit) -> t -> unit val fold : (any -> 'r -> 'r) -> t -> 'r -> 'r end module type S = sig -type 'a tag -type t = Dyn : 'a tag * 'a -> t + type 'a tag + (** Type of dynamic tags *) -val create : string -> 'a tag -val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option -val repr : 'a tag -> string + type t = Dyn : 'a tag * 'a -> t + (** Type of dynamic values *) -type any = Any : 'a tag -> any + val create : string -> 'a tag + (** [create n] returns a tag describing a type called [n]. + [create] raises an exception if [n] is already registered. + Type names are hashed, so [create] may raise even if no type with + the exact same name was registered due to a collision. *) -val name : string -> any option + val eq : 'a tag -> 'b tag -> ('a, 'b) CSig.eq option + (** [eq t1 t2] returns [Some witness] if [t1] is the same as [t2], [None] otherwise. *) -module Map(M : TParam) : MapS with type 'a obj = 'a M.t with type 'a key = 'a tag + val repr : 'a tag -> string + (** [repr tag] returns the name of the type represented by [tag]. *) -val dump : unit -> (int * string) list + val dump : unit -> (int * string) list + (** [dump ()] returns a list of (tag, name) pairs for every type tag registered + in this [Dyn.Make] instance. *) -module Easy : sig + type any = Any : 'a tag -> any + (** Type of boxed dynamic tags *) - (* To create a dynamic type on the fly *) - val make_dyn_tag : string -> ('a -> t) * (t -> 'a) * 'a tag - val make_dyn : string -> ('a -> t) * (t -> 'a) + val name : string -> any option + (** [name n] returns [Some t] where t is a boxed tag previously registered + with [create n], or [None] if there is no such tag. *) - (* For types declared with the [create] function above *) - val inj : 'a -> 'a tag -> t - val prj : t -> 'a tag -> 'a option -end + module Map(Value : ValueS) : + MapS with type 'a key = 'a tag and type 'a value = 'a Value.t + (** Map from type tags to values parameterized by the tag type *) + + module Easy : sig + (* To create a dynamic type on the fly *) + val make_dyn_tag : string -> ('a -> t) * (t -> 'a) * 'a tag + val make_dyn : string -> ('a -> t) * (t -> 'a) + (* For types declared with the [create] function above *) + val inj : 'a -> 'a tag -> t + val prj : t -> 'a tag -> 'a option + end end module Make () : S diff --git a/clib/hashcons.ml b/clib/hashcons.ml index ec73c6d93..39969ebf7 100644 --- a/clib/hashcons.ml +++ b/clib/hashcons.ml @@ -10,8 +10,6 @@ (* Hash consing of datastructures *) -(* The generic hash-consing functions (does not use Obj) *) - (* [t] is the type of object to hash-cons * [u] is the type of hash-cons functions for the sub-structures * of objects of type t (u usually has the form (t1->t1)*(t2->t2)*...). @@ -148,41 +146,3 @@ module Hstring = Make( let len = String.length s in hash len s 0 0 end) - -(* Obj.t *) -exception NotEq - -(* From CAMLLIB/caml/mlvalues.h *) -let no_scan_tag = 251 -let tuple_p obj = Obj.is_block obj && (Obj.tag obj < no_scan_tag) - -let comp_obj o1 o2 = - if tuple_p o1 && tuple_p o2 then - let n1 = Obj.size o1 and n2 = Obj.size o2 in - if n1=n2 then - try - for i = 0 to pred n1 do - if not (Obj.field o1 i == Obj.field o2 i) then raise NotEq - done; true - with NotEq -> false - else false - else o1=o2 - -let hash_obj hrec o = - begin - if tuple_p o then - let n = Obj.size o in - for i = 0 to pred n do - Obj.set_field o i (hrec (Obj.field o i)) - done - end; - o - -module Hobj = Make( - struct - type t = Obj.t - type u = (Obj.t -> Obj.t) * unit - let hashcons (hrec,_) = hash_obj hrec - let eq = comp_obj - let hash = Hashtbl.hash - end) diff --git a/clib/hashcons.mli b/clib/hashcons.mli index 3e396ff23..223dd2a4d 100644 --- a/clib/hashcons.mli +++ b/clib/hashcons.mli @@ -87,6 +87,3 @@ module Hstring : (S with type t = string and type u = unit) module Hlist (D:HashedType) : (S with type t = D.t list and type u = (D.t list -> D.t list)*(D.t->D.t)) (** Hashconsing of lists. *) - -module Hobj : (S with type t = Obj.t and type u = (Obj.t -> Obj.t) * unit) -(** Hashconsing of OCaml values. *) diff --git a/configure.ml b/configure.ml index 9d959b9af..b5d5a2419 100644 --- a/configure.ml +++ b/configure.ml @@ -601,14 +601,14 @@ let caml_version_nums = "Is it installed properly?") let check_caml_version () = - if caml_version_nums >= [4;2;1] then + if caml_version_nums >= [4;2;3] then cprintf "You have OCaml %s. Good!" caml_version else let () = cprintf "Your version of OCaml is %s." caml_version in if !prefs.force_caml_version then warn "Your version of OCaml is outdated." else - die "You need OCaml 4.02.1 or later." + die "You need OCaml 4.02.3 or later." let _ = check_caml_version () diff --git a/dev/base_include b/dev/base_include index 574bc097e..6f54ecb24 100644 --- a/dev/base_include +++ b/dev/base_include @@ -229,7 +229,7 @@ let pf_e gl s = let _ = Flags.in_debugger := false let _ = Flags.in_toplevel := true let _ = Constrextern.set_extern_reference - (fun ?loc _ r -> CAst.make ?loc @@ Libnames.Qualid (Nametab.shortest_qualid_of_global Id.Set.empty r));; + (fun ?loc _ r -> Nametab.shortest_qualid_of_global ?loc Id.Set.empty r);; let go () = Coqloop.(loop ~opts:Option.(get !drop_args) ~state:Option.(get !drop_last_doc)) diff --git a/dev/ci/README.md b/dev/ci/README.md index 665b3768a..08364c897 100644 --- a/dev/ci/README.md +++ b/dev/ci/README.md @@ -47,16 +47,13 @@ CI. ### Add your development by submitting a pull request -Add a new `ci-mydev.sh` script to [`dev/ci`](.) (have a look at -[`ci-coq-dpdgraph.sh`](ci-coq-dpdgraph.sh) or -[`ci-fiat-parsers.sh`](ci-fiat-parsers.sh) for simple examples); -set the corresponding variables in -[`ci-basic-overlay.sh`](ci-basic-overlay.sh); add the corresponding -target to [`Makefile.ci`](../../Makefile.ci); add new jobs to -[`.gitlab-ci.yml`](../../.gitlab-ci.yml), -[`.circleci/config.yml`](../../.circleci/config.yml) and -[`.travis.yml`](../../.travis.yml) so that this new target is run. **Do not -hesitate to submit an incomplete pull request if you need help to finish it.** +Add a new `ci-mydev.sh` script to [`dev/ci`](.); set the corresponding +variables in [`ci-basic-overlay.sh`](ci-basic-overlay.sh); add the +corresponding target to [`Makefile.ci`](../../Makefile.ci) and a new job to +[`.gitlab-ci.yml`](../../.gitlab-ci.yml) so that this new target is run. +Have a look at [#7656](https://github.com/coq/coq/pull/7656/files) for an +example. **Do not hesitate to submit an incomplete pull request if you need +help to finish it.** You may also be interested in having your development tested in our performance benchmark. Currently this is done by providing an OPAM package diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 87d837b38..3807ff90c 100755 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -119,7 +119,7 @@ ######################################################################## # coq-dpdgraph ######################################################################## -: "${coq_dpdgraph_CI_BRANCH:=coq-trunk}" +: "${coq_dpdgraph_CI_BRANCH:=coq-master}" : "${coq_dpdgraph_CI_GITURL:=https://github.com/Karmaki/coq-dpdgraph.git}" ######################################################################## diff --git a/dev/ci/user-overlays/07797-rm-reference.sh b/dev/ci/user-overlays/07797-rm-reference.sh new file mode 100644 index 000000000..f7811cd6f --- /dev/null +++ b/dev/ci/user-overlays/07797-rm-reference.sh @@ -0,0 +1,20 @@ +_OVERLAY_BRANCH=rm-reference + +if [ "$CI_PULL_REQUEST" = "7797" ] || [ "$CI_BRANCH" = "_OVERLAY_BRANCH" ]; then + + Equations_CI_BRANCH="$_OVERLAY_BRANCH" + Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations.git + + ltac2_CI_BRANCH="fix-7797" + ltac2_CI_GITURL=https://github.com/ppedrot/Ltac2.git + + quickchick_CI_BRANCH="$_OVERLAY_BRANCH" + quickchick_CI_GITURL=https://github.com/maximedenes/QuickChick.git + + coq_dpdgraph_CI_BRANCH="$_OVERLAY_BRANCH" + coq_dpdgraph_CI_GITURL=https://github.com/maximedenes/coq-dpdgraph.git + + Elpi_CI_BRANCH="$_OVERLAY_BRANCH" + Elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi.git + +fi diff --git a/dev/doc/changes.md b/dev/doc/changes.md index bb8189efc..f3fc126f9 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -2,6 +2,14 @@ ### ML API +Names + +- In `Libnames`, the type `reference` and its two constructors `Qualid` and + `Ident` have been removed in favor of `qualid`. `Qualid` is now the identity, + `Ident` can be replaced by `qualid_of_ident`. Matching over `reference` can be + replaced by a test using `qualid_is_ident`. Extracting the ident part of a + qualid can be done using `qualid_basename`. + Misctypes - Syntax for universe sorts and kinds has been moved from `Misctypes` diff --git a/dev/doc/profiling.txt b/dev/doc/profiling.txt index 9d2ebf0d4..b5dd8445d 100644 --- a/dev/doc/profiling.txt +++ b/dev/doc/profiling.txt @@ -7,7 +7,7 @@ want to profile time or memory consumption. AFAIK, this only works for Linux. In Coq source folder: -opam switch 4.02.1+fp +opam switch 4.02.3+fp ./configure -local -debug make perf record -g bin/coqtop -compile file.v diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 10a7a4158..844ad9188 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -549,8 +549,8 @@ let encode_path ?loc prefix mpdir suffix id = | Some (mp,dir) -> (DirPath.repr (dirpath_of_string (ModPath.to_string mp))@ DirPath.repr dir) in - CAst.make ?loc @@ Qualid (make_qualid - (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id) + make_qualid ?loc + (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id let raw_string_of_ref ?loc _ = function | ConstRef cst -> @@ -569,9 +569,9 @@ let raw_string_of_ref ?loc _ = function encode_path ?loc "SECVAR" None [] id let short_string_of_ref ?loc _ = function - | VarRef id -> CAst.make ?loc @@ Ident id - | ConstRef cst -> CAst.make ?loc @@ Ident (Label.to_id (pi3 (Constant.repr3 cst))) - | IndRef (kn,0) -> CAst.make ?loc @@ Ident (Label.to_id (pi3 (MutInd.repr3 kn))) + | VarRef id -> qualid_of_ident ?loc id + | ConstRef cst -> qualid_of_ident ?loc (Label.to_id (pi3 (Constant.repr3 cst))) + | IndRef (kn,0) -> qualid_of_ident ?loc (Label.to_id (pi3 (MutInd.repr3 kn))) | IndRef (kn,i) -> encode_path ?loc "IND" None [Label.to_id (pi3 (MutInd.repr3 kn))] (Id.of_string ("_"^string_of_int i)) diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index 35a605ddd..32de15ee3 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -123,11 +123,24 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica :cmd:`Variant` and :cmd:`Record` get an automatic declaration of the induction principles. -``.. prodn::`` :black_nib: Grammar productions. +``.. prodn::`` A grammar production. This is useful if you intend to document individual grammar productions. Otherwise, use Sphinx's `production lists <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_. + Unlike ``.. productionlist``\ s, this directive accepts notation syntax. + + + Usage:: + + .. prodn:: token += production + .. prodn:: token ::= production + + Example:: + + .. prodn:: term += let: @pattern := @term in @term + .. prodn:: occ_switch ::= { {? + %| - } {* @num } } + ``.. tacn::`` :black_nib: A tactic, or a tactic notation. Example:: diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index e10e16c10..e4d24a1f7 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -106,7 +106,7 @@ argument. Morphisms can also be contravariant in one or more of their arguments. A morphism is contravariant on an argument associated to the relation -instance :math`R` if it is covariant on the same argument when the inverse +instance :math:`R` if it is covariant on the same argument when the inverse relation :math:`R^{−1}` (``inverse R`` in Coq) is considered. The special arrow ``-->`` is used in signatures for contravariant morphisms. diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 47d3a7d7c..6a9b343ba 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -310,16 +310,15 @@ The :n:`@ident` is not relevant. It is just used for error messages. The axioms. The optional list of modifiers is used to tailor the behavior of the tactic. The following list describes their syntax and effects: -.. prodn:: - ring_mod ::= abstract %| decidable @term %| morphism @term - %| setoid @term @term - %| constants [@ltac] - %| preprocess [@ltac] - %| postprocess [@ltac] - %| power_tac @term [@ltac] - %| sign @term - %| div @term - +.. productionlist:: coq + ring_mod : abstract | decidable `term` | morphism `term` + : | setoid `term` `term` + : | constants [`ltac`] + : | preprocess [`ltac`] + : | postprocess [`ltac`] + : | power_tac `term` [`ltac`] + : | sign `term` + : | div `term` abstract declares the ring as abstract. This is the default. @@ -663,8 +662,8 @@ messages. :n:`@term` is a proof that the field signature satisfies the (semi-)field axioms. The optional list of modifiers is used to tailor the behavior of the tactic. -.. prodn:: - field_mod := @ring_mod %| completeness @term +.. productionlist:: coq + field_mod : `ring_mod` | completeness `term` Since field tactics are built upon ``ring`` tactics, all modifiers of the ``Add Ring`` apply. There is only one diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index f65400e88..8127d3df3 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -104,7 +104,6 @@ exclude_patterns = [ 'Thumbs.db', '.DS_Store', 'introduction.rst', - 'credits.rst', 'README.rst', 'README.template.rst' ] @@ -201,9 +200,9 @@ html_static_path = ['_static'] # The empty string is equivalent to '%b %d, %Y'. #html_last_updated_fmt = None -# If true, SmartyPants will be used to convert quotes and dashes to -# typographically correct entities. -html_use_smartypants = False # FIXME wrap code in <code> tags, otherwise quotesget converted in there +# FIXME: this could be re-enabled after ensuring that smart quotes are locally +# disabled for all relevant directives +smartquotes = False # Custom sidebar templates, maps document names to template names. #html_sidebars = {} diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst index a75659798..2562dec46 100644 --- a/doc/sphinx/credits.rst +++ b/doc/sphinx/credits.rst @@ -1,3 +1,8 @@ +.. include:: preamble.rst +.. include:: replaces.rst + +.. _credits: + ------------------------------------------- Credits ------------------------------------------- diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst index 136f9088b..f3ae49381 100644 --- a/doc/sphinx/index.rst +++ b/doc/sphinx/index.rst @@ -1,16 +1,31 @@ -.. _introduction: - .. include:: preamble.rst .. include:: replaces.rst .. include:: introduction.rst -.. include:: credits.rst ------------------ Table of contents ------------------ .. toctree:: + :caption: Indexes + + genindex + coq-cmdindex + coq-tacindex + coq-optindex + coq-exnindex + +.. No entries yet + * :index:`thmindex` + +.. toctree:: + :caption: Preamble + + self + credits + +.. toctree:: :caption: The language language/gallina-specification-language @@ -65,18 +80,6 @@ Table of contents zebibliography -.. toctree:: - :caption: Indexes - - genindex - coq-cmdindex - coq-tacindex - coq-optindex - coq-exnindex - -.. No entries yet - * :index:`thmindex` - This material (the Coq Reference Manual) may be distributed only subject to the terms and conditions set forth in the Open Publication License, v1.0 or later (the latest version is presently available at diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index 75ff72c4d..20e4069f4 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -1,3 +1,5 @@ +.. _introduction: + ------------------------ Introduction ------------------------ diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 3b2009657..ab52c2ce7 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1484,7 +1484,7 @@ The abstract tactic ``````````````````` .. tacn:: abstract: {+ d_item} - :name abstract (ssreflect) + :name: abstract (ssreflect) This tactic assigns an abstract constant previously introduced with the ``[: name ]`` intro pattern (see section :ref:`introduction_ssr`). @@ -2402,7 +2402,7 @@ tactic: The behavior of the defective have tactic makes it possible to generalize it in the following general construction: -.. tacn:: have {* @i_item } {? @i_pattern } {? @s_item | {+ @binder } } {? : @term } {? := @term | by @tactic } +.. tacn:: have {* @i_item } {? @i_pattern } {? @s_item | {+ @ssr_binder } } {? : @term } {? := @term | by @tactic } Open syntax is supported for both :token:`term`. For the description of :token:`i_item` and :token:`s_item` see section @@ -3657,7 +3657,8 @@ selective rewriting, blocking on the fly the reduction in the term ``t``. .. coqtop:: reset - From Coq Require Import ssreflect ssrfun ssrbool List. + From Coq Require Import ssreflect ssrfun ssrbool. + From Coq Require Import List. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -5241,7 +5242,7 @@ Notation scope Module name -.. prodn:: name ::= @qualid +.. prodn:: modname ::= @qualid Natural number @@ -5251,14 +5252,10 @@ where :token:`ident` is an Ltac variable denoting a standard |Coq| numeral (should not be the name of a tactic which can be followed by a bracket ``[``, like ``do``, ``have``,…) -Pattern - -.. prodn:: pattern ::= @term - Items and switches ~~~~~~~~~~~~~~~~~~ -.. prodn:: binder ::= @ident %| ( @ident {? : @term } ) +.. prodn:: ssr_binder ::= @ident %| ( @ident {? : @term } ) binder see :ref:`abbreviations_ssr`. @@ -5353,8 +5350,8 @@ case analysis see :ref:`the_defective_tactics_ssr` rewrite see :ref:`rewriting_ssr` -.. tacn:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @binder } } {? : @term } := @term -.. tacv:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @binder } } : @term {? by @tactic } +.. tacn:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } {? : @term } := @term +.. tacv:: have {* @i_item } {? @i_pattern } {? @s_item %| {+ @ssr_binder } } : @term {? by @tactic } .. tacn:: have suff {? @clear_switch } {? @i_pattern } {? : @term } := @term .. tacv:: have suff {? @clear_switch } {? @i_pattern } : @term {? by @tactic } .. tacv:: gen have {? @ident , } {? @i_pattern } : {+ @gen_item } / @term {? by @tactic } @@ -5368,9 +5365,9 @@ forward chaining see :ref:`structure_ssr` specializing see :ref:`structure_ssr` -.. tacn:: suff {* @i_item } {? @i_pattern } {+ @binder } : @term {? by @tactic } +.. tacn:: suff {* @i_item } {? @i_pattern } {+ @ssr_binder } : @term {? by @tactic } :name: suff -.. tacv:: suffices {* @i_item } {? @i_pattern } {+ @binder } : @term {? by @tactic } +.. tacv:: suffices {* @i_item } {? @i_pattern } {+ @ssr_binder } : @term {? by @tactic } :name: suffices .. tacv:: suff {? have } {? @clear_switch } {? @i_pattern } : @term {? by @tactic } .. tacv:: suffices {? have } {? @clear_switch } {? @i_pattern } : @term {? by @tactic } @@ -5381,7 +5378,7 @@ backchaining see :ref:`structure_ssr` local definition :ref:`definitions_ssr` -.. tacv:: pose @ident {+ @binder } := @term +.. tacv:: pose @ident {+ @ssr_binder } := @term local function definition diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 29c2f8b81..d0a0d568e 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3949,9 +3949,20 @@ succeeds, and results in an error otherwise. :name: constr_eq This tactic checks whether its arguments are equal modulo alpha - conversion and casts. + conversion, casts and universe constraints. It may unify universes. .. exn:: Not equal. +.. exn:: Not equal (due to universes). + +.. tacn:: constr_eq_strict @term @term + :name: constr_eq_strict + + This tactic checks whether its arguments are equal modulo alpha + conversion, casts and universe constraints. It does not add new + constraints. + +.. exn:: Not equal. +.. exn:: Not equal (due to universes). .. tacn:: unify @term @term :name: unify diff --git a/doc/tools/coqrst/coqdoc/main.py b/doc/tools/coqrst/coqdoc/main.py index cedd60d3b..57adcb287 100644 --- a/doc/tools/coqrst/coqdoc/main.py +++ b/doc/tools/coqrst/coqdoc/main.py @@ -20,6 +20,7 @@ lexer. """ import os +import platform from tempfile import mkstemp from subprocess import check_output @@ -36,6 +37,9 @@ def coqdoc(coq_code, coqdoc_bin=None): """Get the output of coqdoc on coq_code.""" coqdoc_bin = coqdoc_bin or os.path.join(os.getenv("COQBIN"), "coqdoc") fd, filename = mkstemp(prefix="coqdoc-", suffix=".v") + if platform.system().startswith("CYGWIN"): + # coqdoc currently doesn't accept cygwin style paths in the form "/cygdrive/c/..." + filename = check_output(["cygpath", "-w", filename]).decode("utf-8").strip() try: os.write(fd, COQDOC_HEADER.encode("utf-8")) os.write(fd, coq_code.encode("utf-8")) diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index ab3a485b2..c9487abf0 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -28,6 +28,7 @@ from docutils.parsers.rst.directives.admonitions import BaseAdmonition from sphinx import addnodes from sphinx.roles import XRefRole +from sphinx.errors import ExtensionError from sphinx.util.nodes import set_source_info, set_role_source_info, make_refnode from sphinx.util.logging import getLogger from sphinx.directives import ObjectDescription @@ -103,10 +104,16 @@ class CoqObject(ObjectDescription): 'undocumented': directives.flag } - def _subdomain(self): + def subdomain_data(self): if self.subdomain is None: raise ValueError() - return self.subdomain + return self.env.domaindata['coq']['objects'][self.subdomain] + + def _render_annotation(self, signode): + if self.annotation: + annot_node = nodes.inline(self.annotation, self.annotation, classes=['sigannot']) + signode += addnodes.desc_annotation(self.annotation, '', annot_node) + signode += nodes.Text(' ') def handle_signature(self, signature, signode): """Prefix signature with the proper annotation, then render it using @@ -114,29 +121,32 @@ class CoqObject(ObjectDescription): :returns: the name given to the resulting node, if any """ - if self.annotation: - annotation = self.annotation + ' ' - signode += addnodes.desc_annotation(annotation, annotation) + self._render_annotation(signode) self._render_signature(signature, signode) return self._names.get(signature) or self._name_from_signature(signature) + def _warn_if_duplicate_name(self, objects, name): + """Check that two objects in the same domain don't have the same name.""" + if name in objects: + MSG = 'Duplicate object: {}; other is at {}' + msg = MSG.format(name, self.env.doc2path(objects[name][0])) + self.state_machine.reporter.warning(msg, line=self.lineno) + def _record_name(self, name, target_id): """Record a name, mapping it to target_id Warns if another object of the same name already exists. """ - names_in_subdomain = self.env.domaindata['coq']['objects'][self._subdomain()] - # Check that two objects in the same domain don't have the same name - if name in names_in_subdomain: - self.state_machine.reporter.warning( - 'Duplicate Coq object: {}; other is at {}'.format( - name, self.env.doc2path(names_in_subdomain[name][0])), - line=self.lineno) + names_in_subdomain = self.subdomain_data() + self._warn_if_duplicate_name(names_in_subdomain, name) names_in_subdomain[name] = (self.env.docname, self.objtype, target_id) + def _target_id(self, name): + return make_target(self.objtype, nodes.make_id(name)) + def _add_target(self, signode, name): """Register a link target ‘name’, pointing to signode.""" - targetid = make_target(self.objtype, nodes.make_id(name)) + targetid = self._target_id(name) if targetid not in self.state.document.ids: signode['ids'].append(targetid) signode['names'].append(name) @@ -314,50 +324,71 @@ class OptionObject(NotationObject): def _name_from_signature(self, signature): return stringify_with_ellipses(signature) -class ProductionObject(NotationObject): - """Grammar productions. +class ProductionObject(CoqObject): + r"""A grammar production. This is useful if you intend to document individual grammar productions. Otherwise, use Sphinx's `production lists <http://www.sphinx-doc.org/en/stable/markup/para.html#directive-productionlist>`_. + + Unlike ``.. productionlist``\ s, this directive accepts notation syntax. + + + Usage:: + + .. prodn:: token += production + .. prodn:: token ::= production + + Example:: + + .. prodn:: term += let: @pattern := @term in @term + .. prodn:: occ_switch ::= { {? + %| - } {* @num } } + """ - # FIXME (CPC): I have no idea what this does :/ Someone should add an example. subdomain = "prodn" - index_suffix = None - annotation = None + #annotation = "Grammar production" - # override to create link targets for production left-hand sides - def run(self): + def _render_signature(self, signature, signode): + raise NotImplementedError(self) + + SIG_ERROR = ("Invalid syntax in ``.. prodn::`` directive" + + "\nExpected ``name ::= ...`` or ``name += ...``" + + " (e.g. ``pattern += constr:(@ident)``)") + + def handle_signature(self, signature, signode): + nsplits = 2 + parts = signature.split(maxsplit=nsplits) + if len(parts) != 3: + raise ExtensionError(ProductionObject.SIG_ERROR) + + lhs, op, rhs = (part.strip() for part in parts) + if op not in ["::=", "+="]: + raise ExtensionError(ProductionObject.SIG_ERROR) + + self._render_annotation(signode) + + lhs_op = '{} {} '.format(lhs, op) + lhs_node = nodes.literal(lhs_op, lhs_op) + + position = self.state_machine.get_source_and_line(self.lineno) + rhs_node = parse_notation(rhs, *position) + signode += addnodes.desc_name(signature, '', lhs_node, rhs_node) + + return ('token', lhs) if op == '::=' else None + + def _add_index_entry(self, name, target): + pass + + def _target_id(self, name): + # Use `name[1]` instead of ``nodes.make_id(name[1])`` to work around + # https://github.com/sphinx-doc/sphinx/issues/4983 + return 'grammar-token-{}'.format(name[1]) + + def _record_name(self, name, targetid): env = self.state.document.settings.env objects = env.domaindata['std']['objects'] - - class ProdnError(Exception): - """Exception for ill-formed prodn""" - pass - - [idx, node] = super().run() - try: - # find LHS of production - inline_lhs = node[0][0][0][0] # may be fragile !!! - lhs_str = str(inline_lhs) - if lhs_str[0:7] != "<inline": - raise ProdnError("Expected atom on LHS") - lhs = inline_lhs[0] - # register link target - subnode = addnodes.production() - subnode['tokenname'] = lhs - idname = 'grammar-token-%s' % subnode['tokenname'] - if idname not in self.state.document.ids: - subnode['ids'].append(idname) - self.state.document.note_implicit_target(subnode, subnode) - objects['token', subnode['tokenname']] = env.docname, idname - subnode.extend(token_xrefs(lhs)) - # patch in link target - inline_lhs['ids'].append(idname) - except ProdnError as err: - getLogger(__name__).warning("Could not create link target for prodn: " + str(err) + - "\nSphinx represents the prodn as: " + str(node) + "\n") - return [idx, node] + self._warn_if_duplicate_name(objects, name) + objects[name] = env.docname, targetid class ExceptionObject(NotationObject): """An error raised by a Coq command or tactic. @@ -841,11 +872,6 @@ class CoqOptionIndex(CoqSubdomainsIndex): class CoqGallinaIndex(CoqSubdomainsIndex): name, localname, shortname, subdomains = "thmindex", "Gallina Index", "theorems", ["thm"] -# we specify an index to make productions fit into the framework of notations -# but not likely to include a link to this index -class CoqProductionIndex(CoqSubdomainsIndex): - name, localname, shortname, subdomains = "prodnindex", "Production Index", "productions", ["prodn"] - class CoqExceptionIndex(CoqSubdomainsIndex): name, localname, shortname, subdomains = "exnindex", "Errors and Warnings Index", "errors", ["exn", "warn"] @@ -952,7 +978,7 @@ class CoqDomain(Domain): 'g': CoqCodeRole } - indices = [CoqVernacIndex, CoqTacticIndex, CoqOptionIndex, CoqGallinaIndex, CoqProductionIndex, CoqExceptionIndex] + indices = [CoqVernacIndex, CoqTacticIndex, CoqOptionIndex, CoqGallinaIndex, CoqExceptionIndex] data_version = 1 initial_data = { @@ -1047,7 +1073,7 @@ def setup(app): # A few sanity checks: subdomains = set(obj.subdomain for obj in CoqDomain.directives.values()) - assert subdomains == set(chain(*(idx.subdomains for idx in CoqDomain.indices))) + assert subdomains.issuperset(chain(*(idx.subdomains for idx in CoqDomain.indices))) assert subdomains.issubset(CoqDomain.roles.keys()) # Add domain, directives, and roles diff --git a/engine/evd.ml b/engine/evd.ml index 0c9c3a29b..f56f9662d 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -894,6 +894,9 @@ let check_eq evd s s' = let check_leq evd s s' = UGraph.check_leq (UState.ugraph evd.universes) s s' +let check_constraints evd csts = + UGraph.check_constraints csts (UState.ugraph evd.universes) + let fix_undefined_variables evd = { evd with universes = UState.fix_undefined_variables evd.universes } diff --git a/engine/evd.mli b/engine/evd.mli index c40e925d8..405fcc403 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -552,6 +552,8 @@ val set_eq_instances : ?flex:bool -> val check_eq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool val check_leq : evar_map -> Univ.Universe.t -> Univ.Universe.t -> bool +val check_constraints : evar_map -> Univ.Constraint.t -> bool + val evar_universe_context : evar_map -> UState.t val universe_context_set : evar_map -> Univ.ContextSet.t val universe_subst : evar_map -> UnivSubst.universe_opt_subst diff --git a/engine/termops.ml b/engine/termops.ml index eacc36107..2db2e07bf 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -297,7 +297,7 @@ let has_no_evar sigma = with Exit -> false let pr_evd_level evd = UState.pr_uctx_level (Evd.evar_universe_context evd) -let reference_of_level evd l = UState.reference_of_level (Evd.evar_universe_context evd) l +let reference_of_level evd l = UState.qualid_of_level (Evd.evar_universe_context evd) l let pr_evar_universe_context ctx = let open UState in diff --git a/engine/termops.mli b/engine/termops.mli index 255494031..f9aa6ba63 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -282,7 +282,7 @@ val is_Prop : Evd.evar_map -> constr -> bool val is_Set : Evd.evar_map -> constr -> bool val is_Type : Evd.evar_map -> constr -> bool -val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.reference +val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid (** Combinators on judgments *) diff --git a/engine/uState.ml b/engine/uState.ml index 0e3ecdbf5..81ab3dd66 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -295,15 +295,15 @@ let constrain_variables diff ctx = in { ctx with uctx_local = (univs, local); uctx_univ_variables = vars } -let reference_of_level uctx = +let qualid_of_level uctx = let map, map_rev = uctx.uctx_names in fun l -> - try CAst.make @@ Libnames.Ident (Option.get (Univ.LMap.find l map_rev).uname) + try Libnames.qualid_of_ident (Option.get (Univ.LMap.find l map_rev).uname) with Not_found | Option.IsNone -> - UnivNames.reference_of_level l + UnivNames.qualid_of_level l let pr_uctx_level uctx l = - Libnames.pr_reference (reference_of_level uctx l) + Libnames.pr_qualid (qualid_of_level uctx l) type ('a, 'b) gen_universe_decl = { univdecl_instance : 'a; (* Declared universes *) diff --git a/engine/uState.mli b/engine/uState.mli index e7e5b39e0..a59e61b89 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -171,6 +171,6 @@ val update_sigma_env : t -> Environ.env -> t (** {5 Pretty-printing} *) val pr_uctx_level : t -> Univ.Level.t -> Pp.t -val reference_of_level : t -> Univ.Level.t -> Libnames.reference +val qualid_of_level : t -> Univ.Level.t -> Libnames.qualid val pr_weak : (Univ.Level.t -> Pp.t) -> t -> Pp.t diff --git a/engine/univNames.ml b/engine/univNames.ml index 6ffb4bcf0..a68840174 100644 --- a/engine/univNames.ml +++ b/engine/univNames.ml @@ -14,18 +14,19 @@ open Globnames open Nametab -let reference_of_level l = CAst.make @@ +let qualid_of_level l = match Level.name l with | Some (d, n as na) -> - let qid = - try Nametab.shortest_qualid_of_universe na - with Not_found -> - let name = Id.of_string_soft (string_of_int n) in - Libnames.make_qualid d name - in Libnames.Qualid qid - | None -> Libnames.Ident Id.(of_string_soft (Level.to_string l)) - -let pr_with_global_universes l = Libnames.pr_reference (reference_of_level l) + begin + try Nametab.shortest_qualid_of_universe na + with Not_found -> + let name = Id.of_string_soft (string_of_int n) in + Libnames.make_qualid d name + end + | None -> + Libnames.qualid_of_ident @@ Id.of_string_soft (Level.to_string l) + +let pr_with_global_universes l = Libnames.pr_qualid (qualid_of_level l) (** Global universe information outside the kernel, to handle polymorphic universe names in sections that have to be discharged. *) diff --git a/engine/univNames.mli b/engine/univNames.mli index c19aa19d5..837beac26 100644 --- a/engine/univNames.mli +++ b/engine/univNames.mli @@ -11,7 +11,7 @@ open Univ val pr_with_global_universes : Level.t -> Pp.t -val reference_of_level : Level.t -> Libnames.reference +val qualid_of_level : Level.t -> Libnames.qualid (** Global universe information outside the kernel, to handle polymorphic universes in sections that have to be discharged. *) diff --git a/engine/universes.ml b/engine/universes.ml index 70601987c..ee9668433 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -17,7 +17,7 @@ type universe_binders = UnivNames.universe_binders type univ_name_list = UnivNames.univ_name_list let pr_with_global_universes = UnivNames.pr_with_global_universes -let reference_of_level = UnivNames.reference_of_level +let reference_of_level = UnivNames.qualid_of_level let add_global_universe = UnivNames.add_global_universe diff --git a/engine/universes.mli b/engine/universes.mli index 46ff33a47..29673de1e 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -22,8 +22,8 @@ open Univ val pr_with_global_universes : Level.t -> Pp.t [@@ocaml.deprecated "Use [UnivNames.pr_with_global_universes]"] -val reference_of_level : Level.t -> Libnames.reference -[@@ocaml.deprecated "Use [UnivNames.reference_of_level]"] +val reference_of_level : Level.t -> Libnames.qualid +[@@ocaml.deprecated "Use [UnivNames.qualid_of_level]"] val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit [@@ocaml.deprecated "Use [UnivNames.add_global_universe]"] diff --git a/ide/idetop.ml b/ide/idetop.ml index ba69c4185..7abbf239b 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -290,8 +290,7 @@ let pattern_of_string ?env s = let dirpath_of_string_list s = let path = String.concat "." s in - let m = Pcoq.parse_string Pcoq.Constr.global path in - let {CAst.v=qid} = Libnames.qualid_of_reference m in + let qid = Pcoq.parse_string Pcoq.Constr.global path in let id = try Nametab.full_name_module qid with Not_found -> diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index d725f5afa..521eeb8e9 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -61,17 +61,17 @@ type instance_expr = Glob_term.glob_level list type cases_pattern_expr_r = | CPatAlias of cases_pattern_expr * lname - | CPatCstr of reference + | CPatCstr of qualid * cases_pattern_expr list option * cases_pattern_expr list (** [CPatCstr (_, c, Some l1, l2)] represents [(@ c l1) l2] *) - | CPatAtom of reference option + | CPatAtom of qualid option | CPatOr of cases_pattern_expr list | CPatNotation of notation * cases_pattern_notation_substitution * cases_pattern_expr list (** CPatNotation (_, n, l1 ,l2) represents (notation n applied with substitution l1) applied to arguments l2 *) | CPatPrim of prim_token - | CPatRecord of (reference * cases_pattern_expr) list + | CPatRecord of (qualid * cases_pattern_expr) list | CPatDelimiters of string * cases_pattern_expr | CPatCast of cases_pattern_expr * constr_expr and cases_pattern_expr = cases_pattern_expr_r CAst.t @@ -81,16 +81,16 @@ and cases_pattern_notation_substitution = cases_pattern_expr list list (** for recursive notations *) and constr_expr_r = - | CRef of reference * instance_expr option + | CRef of qualid * instance_expr option | 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 lname * constr_expr * constr_expr option * constr_expr - | CAppExpl of (proj_flag * reference * instance_expr option) * constr_expr list + | CAppExpl of (proj_flag * qualid * instance_expr option) * constr_expr list | CApp of (proj_flag * constr_expr) * (constr_expr * explicitation CAst.t option) list - | CRecord of (reference * constr_expr) list + | CRecord of (qualid * constr_expr) list (* representation of the "let" and "match" constructs *) | CCases of Constr.case_style (* determines whether this value represents "let" or "match" construct *) @@ -111,7 +111,7 @@ and constr_expr_r = | CGeneralization of binding_kind * abstraction_kind option * constr_expr | CPrim of prim_token | CDelimiters of string * constr_expr - | CProj of reference * constr_expr + | CProj of qualid * constr_expr and constr_expr = constr_expr_r CAst.t and case_expr = constr_expr (* expression that is being matched *) @@ -150,7 +150,7 @@ type constr_pattern_expr = constr_expr (** Concrete syntax for modules and module types *) type with_declaration_ast = - | CWith_Module of Id.t list CAst.t * qualid CAst.t + | CWith_Module of Id.t list CAst.t * qualid | CWith_Definition of Id.t list CAst.t * universe_decl_expr option * constr_expr type module_ast_r = diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index d626630ef..4b1af9147 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -10,7 +10,6 @@ open Pp open Util -open CAst open Names open Nameops open Libnames @@ -73,11 +72,11 @@ let rec cases_pattern_expr_eq p1 p2 = | CPatAlias(a1,i1), CPatAlias(a2,i2) -> eq_ast Name.equal i1 i2 && cases_pattern_expr_eq a1 a2 | CPatCstr(c1,a1,b1), CPatCstr(c2,a2,b2) -> - eq_reference c1 c2 && + qualid_eq c1 c2 && Option.equal (List.equal cases_pattern_expr_eq) a1 a2 && List.equal cases_pattern_expr_eq b1 b2 | CPatAtom(r1), CPatAtom(r2) -> - Option.equal eq_reference r1 r2 + Option.equal qualid_eq r1 r2 | CPatOr a1, CPatOr a2 -> List.equal cases_pattern_expr_eq a1 a2 | CPatNotation (n1, s1, l1), CPatNotation (n2, s2, l2) -> @@ -88,7 +87,7 @@ let rec cases_pattern_expr_eq p1 p2 = prim_token_eq i1 i2 | CPatRecord l1, CPatRecord l2 -> let equal (r1, e1) (r2, e2) = - eq_reference r1 r2 && cases_pattern_expr_eq e1 e2 + qualid_eq r1 r2 && cases_pattern_expr_eq e1 e2 in List.equal equal l1 l2 | CPatDelimiters(s1,e1), CPatDelimiters(s2,e2) -> @@ -108,7 +107,7 @@ let eq_universes u1 u2 = let rec constr_expr_eq e1 e2 = if CAst.(e1.v == e2.v) then true else match CAst.(e1.v, e2.v) with - | CRef (r1,u1), CRef (r2,u2) -> eq_reference r1 r2 && eq_universes u1 u2 + | CRef (r1,u1), CRef (r2,u2) -> qualid_eq r1 r2 && eq_universes u1 u2 | CFix(id1,fl1), CFix(id2,fl2) -> eq_ast Id.equal id1 id2 && List.equal fix_expr_eq fl1 fl2 @@ -128,7 +127,7 @@ let rec constr_expr_eq e1 e2 = constr_expr_eq b1 b2 | CAppExpl((proj1,r1,_),al1), CAppExpl((proj2,r2,_),al2) -> Option.equal Int.equal proj1 proj2 && - eq_reference r1 r2 && + qualid_eq r1 r2 && List.equal constr_expr_eq al1 al2 | CApp((proj1,e1),al1), CApp((proj2,e2),al2) -> Option.equal Int.equal proj1 proj2 && @@ -136,7 +135,7 @@ let rec constr_expr_eq e1 e2 = List.equal args_eq al1 al2 | CRecord l1, CRecord l2 -> let field_eq (r1, e1) (r2, e2) = - eq_reference r1 r2 && constr_expr_eq e1 e2 + qualid_eq r1 r2 && constr_expr_eq e1 e2 in List.equal field_eq l1 l2 | CCases(_,r1,a1,brl1), CCases(_,r2,a2,brl2) -> @@ -178,7 +177,7 @@ let rec constr_expr_eq e1 e2 = String.equal s1 s2 && constr_expr_eq e1 e2 | CProj(p1,c1), CProj(p2,c2) -> - eq_reference p1 p2 && constr_expr_eq c1 c2 + qualid_eq p1 p2 && constr_expr_eq c1 c2 | (CRef _ | CFix _ | CCoFix _ | CProdN _ | CLambdaN _ | CLetIn _ | CAppExpl _ | CApp _ | CRecord _ | CCases _ | CLetTuple _ | CIf _ | CHole _ | CPatVar _ | CEvar _ | CSort _ | CCast _ | CNotation _ | CPrim _ @@ -280,7 +279,9 @@ let rec cases_pattern_fold_names f a pt = match CAst.(pt.v) with List.fold_left (cases_pattern_fold_names f) (List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll)) patl' | CPatDelimiters (_,pat) -> cases_pattern_fold_names f a pat - | CPatAtom (Some {v=Ident id}) when not (is_constructor id) -> f id a + | CPatAtom (Some qid) + when qualid_is_ident qid && not (is_constructor @@ qualid_basename qid) -> + f (qualid_basename qid) a | CPatPrim _ | CPatAtom _ -> a | CPatCast ({CAst.loc},_) -> CErrors.user_err ?loc ~hdr:"cases_pattern_fold_names" @@ -363,7 +364,9 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function let free_vars_of_constr_expr c = let rec aux bdvars l = function - | { CAst.v = CRef ({v=Ident id},_) } -> if Id.List.mem id bdvars then l else Id.Set.add id l + | { CAst.v = CRef (qid, _) } when qualid_is_ident qid -> + let id = qualid_basename qid in + if Id.List.mem id bdvars then l else Id.Set.add id l | c -> fold_constr_expr_with_binders (fun a l -> a::l) aux bdvars l c in aux [] Id.Set.empty c @@ -440,11 +443,13 @@ let map_constr_expr_with_binders g f e = CAst.map (function ) (* Used in constrintern *) -let rec replace_vars_constr_expr l = function - | { CAst.loc; v = CRef ({v=Ident id},us) } as x -> - (try CAst.make ?loc @@ CRef (make ?loc @@ Ident (Id.Map.find id l),us) with Not_found -> x) - | c -> map_constr_expr_with_binders Id.Map.remove - replace_vars_constr_expr l c +let rec replace_vars_constr_expr l r = + match r with + | { CAst.loc; v = CRef (qid,us) } as x when qualid_is_ident qid -> + let id = qualid_basename qid in + (try CAst.make ?loc @@ CRef (qualid_of_ident ?loc (Id.Map.find id l),us) + with Not_found -> x) + | cn -> map_constr_expr_with_binders Id.Map.remove replace_vars_constr_expr l cn (* Returns the ranges of locs of the notation that are not occupied by args *) (* and which are then occupied by proper symbols of the notation (or spaces) *) @@ -513,7 +518,7 @@ let split_at_annot bl na = (** Pseudo-constructors *) -let mkIdentC id = CAst.make @@ CRef (make @@ Ident id,None) +let mkIdentC id = CAst.make @@ CRef (qualid_of_ident id,None) let mkRefC r = CAst.make @@ CRef (r,None) let mkCastC (a,k) = CAst.make @@ CCast (a,k) let mkLambdaC (idl,bk,a,b) = CAst.make @@ CLambdaN ([CLocalAssum (idl,bk,a)],b) @@ -532,20 +537,22 @@ let mkCProdN ?loc bll c = let mkCLambdaN ?loc bll c = CAst.make ?loc @@ CLambdaN (bll,c) -let coerce_reference_to_id = CAst.with_loc_val (fun ?loc -> function - | Ident id -> id - | Qualid _ -> - CErrors.user_err ?loc ~hdr:"coerce_reference_to_id" - (str "This expression should be a simple identifier.")) +let coerce_reference_to_id qid = + if qualid_is_ident qid then qualid_basename qid + else + CErrors.user_err ?loc:qid.CAst.loc ~hdr:"coerce_reference_to_id" + (str "This expression should be a simple identifier.") let coerce_to_id = function - | { CAst.loc; v = CRef ({v=Ident id},None) } -> CAst.make ?loc id + | { CAst.loc; v = CRef (qid,None) } when qualid_is_ident qid -> + CAst.make ?loc @@ qualid_basename qid | { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_id" (str "This expression should be a simple identifier.") let coerce_to_name = function - | { CAst.loc; v = CRef ({v=Ident id},None) } -> CAst.make ?loc @@ Name id + | { CAst.loc; v = CRef (qid,None) } when qualid_is_ident qid -> + CAst.make ?loc @@ Name (qualid_basename qid) | { CAst.loc; v = CHole (None,IntroAnonymous,None) } -> CAst.make ?loc Anonymous | { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_name" (str "This expression should be a name.") @@ -572,7 +579,8 @@ let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function CPatAtom (Some r) | CHole (None,IntroAnonymous,None) -> CPatAtom None - | CLetIn ({CAst.loc;v=Name id},b,None,{ CAst.v = CRef ({v=Ident id'},None) }) when Id.equal id id' -> + | CLetIn ({CAst.loc;v=Name id},b,None,{ CAst.v = CRef (qid,None) }) + when qualid_is_ident qid && Id.equal id (qualid_basename qid) -> 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 diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 1c2348457..46aef1c78 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -41,7 +41,7 @@ val local_binders_loc : local_binder_expr list -> Loc.t option (** {6 Constructors}*) val mkIdentC : Id.t -> constr_expr -val mkRefC : reference -> constr_expr +val mkRefC : qualid -> constr_expr val mkAppC : constr_expr * constr_expr list -> constr_expr val mkCastC : constr_expr * constr_expr Glob_term.cast_type -> constr_expr val mkLambdaC : lname list * binder_kind * constr_expr * constr_expr -> constr_expr @@ -61,7 +61,7 @@ val mkAppPattern : ?loc:Loc.t -> cases_pattern_expr -> cases_pattern_expr list - (** {6 Destructors}*) -val coerce_reference_to_id : reference -> Id.t +val coerce_reference_to_id : qualid -> Id.t (** FIXME: nothing to do here *) val coerce_to_id : constr_expr -> lident diff --git a/interp/constrextern.ml b/interp/constrextern.ml index c613effcd..2538c7772 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -270,7 +270,7 @@ let extern_evar n l = CEvar (n,l) may be inaccurate *) let default_extern_reference ?loc vars r = - make @@ Qualid (shortest_qualid_of_global vars r) + shortest_qualid_of_global ?loc vars r let my_extern_reference = ref default_extern_reference @@ -388,7 +388,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = (uninterp_cases_pattern_notations pat) with No_match -> lift (fun ?loc -> function - | PatVar (Name id) -> CPatAtom (Some (make ?loc @@ Ident id)) + | PatVar (Name id) -> CPatAtom (Some (qualid_of_ident ?loc id)) | PatVar (Anonymous) -> CPatAtom None | PatCstr(cstrsp,args,na) -> let args = List.map (extern_cases_pattern_in_scope scopes vars) args in @@ -457,7 +457,7 @@ and apply_notation_to_pattern ?loc gr ((subst,substlist),(nb_to_drop,more_args)) (make_pat_notation ?loc ntn (l,ll) l2') key end | SynDefRule kn -> - let qid = make ?loc @@ Qualid (shortest_qualid_of_syndef vars kn) in + let qid = shortest_qualid_of_syndef ?loc vars kn in let l1 = List.rev_map (fun (c,(scopt,scl)) -> extern_cases_pattern_in_scope (scopt,scl@scopes) vars c) @@ -484,7 +484,7 @@ and extern_notation_pattern (tmp_scope,scopes as allscopes) vars t = function (match_notation_constr_cases_pattern t pat) allscopes vars keyrule in insert_pat_alias ?loc p na | PatVar Anonymous -> CAst.make ?loc @@ CPatAtom None - | PatVar (Name id) -> CAst.make ?loc @@ CPatAtom (Some (make ?loc @@ Ident id)) + | PatVar (Name id) -> CAst.make ?loc @@ CPatAtom (Some (qualid_of_ident ?loc id)) with No_match -> extern_notation_pattern allscopes vars t rules @@ -753,7 +753,7 @@ let rec extern inctx scopes vars r = extern_global (select_stronger_impargs (implicits_of_global ref)) (extern_reference vars ref) (extern_universes us) - | GVar id -> CRef (make ?loc @@ Ident id,None) + | GVar id -> CRef (qualid_of_ident ?loc id,None) | GEvar (n,[]) when !print_meta_as_hole -> CHole (None, IntroAnonymous, None) @@ -1095,7 +1095,7 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function List.map (fun (c,(scopt,scl)) -> extern true (scopt,scl@scopes) vars c, None) terms in - let a = CRef (make ?loc @@ Qualid (shortest_qualid_of_syndef vars kn),None) in + let a = CRef (shortest_qualid_of_syndef ?loc vars kn,None) in CAst.make ?loc @@ if List.is_empty l then a else CApp ((None, CAst.make a),l) in if List.is_empty args then e else diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 73c108319..f09b316cd 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -38,7 +38,7 @@ val extern_closed_glob : ?lax:bool -> bool -> env -> Evd.evar_map -> closed_glob val extern_constr : ?lax:bool -> bool -> env -> Evd.evar_map -> constr -> constr_expr val extern_constr_in_scope : bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr -val extern_reference : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> reference +val extern_reference : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr val extern_sort : Evd.evar_map -> Sorts.t -> glob_sort val extern_rel_context : constr option -> env -> Evd.evar_map -> @@ -56,9 +56,9 @@ val print_projections : bool ref (** Customization of the global_reference printer *) val set_extern_reference : - (?loc:Loc.t -> Id.Set.t -> GlobRef.t -> reference) -> unit + (?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid) -> unit val get_extern_reference : - unit -> (?loc:Loc.t -> Id.Set.t -> GlobRef.t -> reference) + unit -> (?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid) (** WARNING: The following functions are evil due to side-effects. Think of the following case as used in the printer: diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 47ae64d47..4e217b2cd 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -96,8 +96,8 @@ let is_global id = with Not_found -> false -let global_reference_of_reference ref = - locate_reference (qualid_of_reference ref).CAst.v +let global_reference_of_reference qid = + locate_reference qid let global_reference id = locate_reference (qualid_of_ident id) @@ -117,7 +117,7 @@ let global_reference_in_absolute_module dir id = type internalization_error = | VariableCapture of Id.t * Id.t | IllegalMetavariable - | NotAConstructor of reference + | NotAConstructor of qualid | UnboundFixName of bool * Id.t | NonLinearPattern of Id.t | BadPatternsNumber of int * int @@ -131,8 +131,8 @@ let explain_variable_capture id id' = let explain_illegal_metavariable = str "Metavariables allowed only in patterns" -let explain_not_a_constructor ref = - str "Unknown constructor: " ++ pr_reference ref +let explain_not_a_constructor qid = + str "Unknown constructor: " ++ pr_qualid qid let explain_unbound_fix_name is_cofix id = str "The name" ++ spc () ++ Id.print id ++ @@ -404,7 +404,8 @@ let intern_generalized_binder ?(global_level=false) intern_type ntnvars let name = let id = match ty with - | { v = CApp ((_, { v = CRef ({v=Ident id},_) } ), _) } -> id + | { v = CApp ((_, { v = CRef (qid,_) } ), _) } when qualid_is_ident qid -> + qualid_basename qid | _ -> default_non_dependent_ident in Implicit_quantifiers.make_fresh ids' (Global.env ()) id in Name name @@ -556,7 +557,8 @@ let is_var store pat = let out_var pat = match pat.v with - | CPatAtom (Some ({v=Ident id})) -> Name id + | CPatAtom (Some qid) when qualid_is_ident qid -> + Name (qualid_basename qid) | CPatAtom None -> Anonymous | _ -> assert false @@ -622,18 +624,18 @@ let error_cannot_coerce_disjunctive_pattern_term ?loc () = let terms_of_binders bl = let rec term_of_pat pt = dmap_with_loc (fun ?loc -> function - | PatVar (Name id) -> CRef (make @@ Ident id, None) + | PatVar (Name id) -> CRef (qualid_of_ident id, None) | PatVar (Anonymous) -> error_cannot_coerce_wildcard_term ?loc () | PatCstr (c,l,_) -> - let r = make ?loc @@ Qualid (qualid_of_path (path_of_global (ConstructRef c))) in + let qid = qualid_of_path ?loc (path_of_global (ConstructRef c)) in let hole = CAst.make ?loc @@ CHole (None,IntroAnonymous,None) in let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in - CAppExpl ((None,r,None),params @ List.map term_of_pat l)) pt in + CAppExpl ((None,qid,None),params @ List.map term_of_pat l)) pt in let rec extract_variables l = match l with | bnd :: l -> let loc = bnd.loc in begin match DAst.get bnd with - | GLocalAssum (Name id,_,_) -> (CAst.make ?loc @@ CRef (make ?loc @@ Ident id, None)) :: extract_variables l + | GLocalAssum (Name id,_,_) -> (CAst.make ?loc @@ CRef (qualid_of_ident ?loc id, None)) :: extract_variables l | GLocalDef (Name id,_,_,_) -> extract_variables l | GLocalDef (Anonymous,_,_,_) | GLocalAssum (Anonymous,_,_) -> user_err Pp.(str "Cannot turn \"_\" into a term.") @@ -806,7 +808,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = distinction *) let cases_pattern_of_name {loc;v=na} = - let atom = match na with Name id -> Some (make ?loc @@ Ident id) | Anonymous -> None in + let atom = match na with Name id -> Some (qualid_of_ident ?loc id) | Anonymous -> None in CAst.make ?loc (CPatAtom atom) let split_by_type ids subst = @@ -903,7 +905,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 (make ?loc @@ Ident id,None), Some (make ?loc @@ ExplByName id)) expl_impls in + (fun id -> CAst.make ?loc @@ CRef (qualid_of_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 @@ -970,18 +972,17 @@ let dump_extended_global loc = function | TrueGlobal ref -> (*feedback_global loc ref;*) Dumpglob.add_glob ?loc ref | SynDef sp -> Dumpglob.add_glob_kn ?loc sp -let intern_extended_global_of_qualid {loc;v=qid} = - let r = Nametab.locate_extended qid in dump_extended_global loc r; r +let intern_extended_global_of_qualid qid = + let r = Nametab.locate_extended qid in dump_extended_global qid.CAst.loc r; r -let intern_reference ref = - let qid = qualid_of_reference ref in +let intern_reference qid = let r = try intern_extended_global_of_qualid qid with Not_found -> error_global_not_found qid in Smartlocate.global_of_extended_global r -let sort_info_of_level_info (info: level_info) : (Libnames.reference * int) option = +let sort_info_of_level_info (info: level_info) : (Libnames.qualid * int) option = match info with | UAnonymous -> None | UUnknown -> None @@ -1014,7 +1015,7 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args = let c = instantiate_notation_constr loc intern intern_cases_pattern_as_binder ntnvars subst infos c in let loc = c.loc in let err () = - user_err ?loc (str "Notation " ++ pr_qualid qid.v + user_err ?loc (str "Notation " ++ pr_qualid qid ++ str " cannot have a universe instance," ++ str " its expanded head does not start with a reference") in @@ -1031,34 +1032,32 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args = | Some [s], GSort (GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s) | Some [_old_level], GSort _new_sort -> (* TODO: add old_level and new_sort to the error message *) - user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid.v) + user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid) | Some _, _ -> err () in c, projapp, args2 -let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args = -function - | {loc; v=Qualid qid} -> - let qid = make ?loc qid in - let r,projapp,args2 = - try intern_qualid qid intern env ntnvars us args - with Not_found -> error_global_not_found qid - in - let x, imp, scopes, l = find_appl_head_data r in - (x,imp,scopes,l), args2 - | {loc; v=Ident id} -> - try intern_var env lvar namedctx loc id us, args +let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args qid = + let loc = qid.CAst.loc in + if qualid_is_ident qid then + try intern_var env lvar namedctx loc (qualid_basename qid) us, args with Not_found -> - let qid = make ?loc @@ qualid_of_ident id in try let r, projapp, args2 = intern_qualid ~no_secvar:true qid intern env ntnvars us args in let x, imp, scopes, l = find_appl_head_data r in (x,imp,scopes,l), args2 with Not_found -> - (* Extra allowance for non globalizing functions *) - if !interning_grammar || env.unb then - (gvar (loc,id) us, [], [], []), args + (* Extra allowance for non globalizing functions *) + if !interning_grammar || env.unb then + (gvar (loc,qualid_basename qid) us, [], [], []), args else error_global_not_found qid + else + let r,projapp,args2 = + try intern_qualid qid intern env ntnvars us args + with Not_found -> error_global_not_found qid + in + let x, imp, scopes, l = find_appl_head_data r in + (x,imp,scopes,l), args2 let interp_reference vars r = let (r,_,_,_),_ = @@ -1262,18 +1261,18 @@ let find_constructor loc add_params ref = List.make nb ([], [(Id.Map.empty, DAst.make @@ PatVar Anonymous)]) | None -> [] -let find_pattern_variable = function - | {v=Ident id} -> id - | {loc;v=Qualid _} as x -> raise (InternalizationError(loc,NotAConstructor x)) +let find_pattern_variable qid = + if qualid_is_ident qid then qualid_basename qid + else raise (InternalizationError(qid.CAst.loc,NotAConstructor qid)) let check_duplicate loc fields = - let eq (ref1, _) (ref2, _) = eq_reference ref1 ref2 in + let eq (ref1, _) (ref2, _) = qualid_eq ref1 ref2 in let dups = List.duplicates eq fields in match dups with | [] -> () | (r, _) :: _ -> user_err ?loc (str "This record defines several times the field " ++ - pr_reference r ++ str ".") + pr_qualid r ++ str ".") (** [sort_fields ~complete loc fields completer] expects a list [fields] of field assignments [f = e1; g = e2; ...], where [f, g] @@ -1298,14 +1297,14 @@ let sort_fields ~complete loc fields completer = (gr, Recordops.find_projection gr) with Not_found -> user_err ?loc ~hdr:"intern" - (pr_reference first_field_ref ++ str": Not a projection") + (pr_qualid first_field_ref ++ str": Not a projection") in (* the number of parameters *) let nparams = record.Recordops.s_EXPECTEDPARAM in (* the reference constructor of the record *) let base_constructor = let global_record_id = ConstructRef record.Recordops.s_CONST in - try make ?loc @@ Qualid (shortest_qualid_of_global Id.Set.empty global_record_id) + try shortest_qualid_of_global ?loc Id.Set.empty global_record_id with Not_found -> anomaly (str "Environment corruption for records.") in let () = check_duplicate loc fields in @@ -1356,7 +1355,7 @@ let sort_fields ~complete loc fields completer = let field_glob_ref = try global_reference_of_reference field_ref with Not_found -> user_err ?loc ~hdr:"intern" - (str "The field \"" ++ pr_reference field_ref ++ str "\" does not exist.") in + (str "The field \"" ++ pr_qualid field_ref ++ str "\" does not exist.") in let remaining_projs, (field_index, _) = let the_proj (idx, glob_id) = GlobRef.equal field_glob_ref (ConstRef glob_id) in try CList.extract_first the_proj remaining_projs @@ -1483,10 +1482,9 @@ let drop_notations_pattern looked_for genv = end | _ -> CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr."))) x in - let rec drop_syndef top scopes re pats = - let qid = qualid_of_reference re in + let rec drop_syndef top scopes qid pats = try - match locate_extended qid.v with + match locate_extended qid with | SynDef sp -> let (vars,a) = Syntax_def.search_syntactic_definition sp in (match a with @@ -1542,10 +1540,10 @@ let drop_notations_pattern looked_for genv = | Some (a,b,c) -> DAst.make ?loc @@ RCPatCstr(a, b, c) | None -> raise (InternalizationError (loc,NotAConstructor head)) end - | CPatCstr (r, Some expl_pl, pl) -> - let g = try locate (qualid_of_reference r).v + | CPatCstr (qid, Some expl_pl, pl) -> + let g = try locate qid with Not_found -> - raise (InternalizationError (loc,NotAConstructor r)) in + raise (InternalizationError (loc,NotAConstructor qid)) in if expl_pl == [] then (* Convention: (@r) deactivates all further implicit arguments and scopes *) DAst.make ?loc @@ RCPatCstr (g, List.map (in_pat false scopes) pl, []) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 12f77af30..dd0944cc4 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -141,10 +141,10 @@ val intern_constr_pattern : constr_pattern_expr -> patvar list * constr_pattern (** Raise Not_found if syndef not bound to a name and error if unexisting ref *) -val intern_reference : reference -> GlobRef.t +val intern_reference : qualid -> GlobRef.t (** Expands abbreviations (syndef); raise an error if not existing *) -val interp_reference : ltac_sign -> reference -> glob_constr +val interp_reference : ltac_sign -> qualid -> glob_constr (** Interpret binders *) diff --git a/interp/declare.ml b/interp/declare.ml index bc2d2068a..aa737239b 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -382,17 +382,34 @@ let inInductive : inductive_obj -> obj = discharge_function = discharge_inductive; rebuild_function = infer_inductive_subtyping } -let declare_projections mind = - let spec,_ = Inductive.lookup_mind_specif (Global.env ()) (mind,0) in +let declare_projections univs mind = + let env = Global.env () in + let spec,_ = Inductive.lookup_mind_specif env (mind,0) in match spec.mind_record with - | Some (Some (_, kns, pjs)) -> - Array.iteri (fun i kn -> + | Some (Some (_, kns, _)) -> + let projs = Inductiveops.compute_projections env (mind, 0) in + Array.iter2 (fun kn (term, types) -> let id = Label.to_id (Constant.label kn) in - let entry = {proj_entry_ind = mind; proj_entry_arg = i} in - let kn' = declare_constant id (ProjectionEntry entry, - IsDefinition StructureComponent) - in - assert(Constant.equal kn kn')) kns; true,true + let univs = match univs with + | Monomorphic_ind_entry _ -> + (** Global constraints already defined through the inductive *) + Monomorphic_const_entry Univ.ContextSet.empty + | Polymorphic_ind_entry ctx -> + Polymorphic_const_entry ctx + | Cumulative_ind_entry ctx -> + Polymorphic_const_entry (Univ.CumulativityInfo.univ_context ctx) + in + let term, types = match univs with + | Monomorphic_const_entry _ -> term, types + | Polymorphic_const_entry ctx -> + let u = Univ.UContext.instance ctx in + Vars.subst_instance_constr u term, Vars.subst_instance_constr u types + in + let entry = definition_entry ~types ~univs term in + let kn' = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in + assert (Constant.equal kn kn') + ) kns projs; + true, true | Some None -> true,false | None -> false,false @@ -403,7 +420,7 @@ let declare_mind mie = | [] -> anomaly (Pp.str "cannot declare an empty list of inductives.") in let (sp,kn as oname) = add_leaf id (inInductive ([],mie)) in let mind = Global.mind_of_delta_kn kn in - let isrecord,isprim = declare_projections mind in + let isrecord,isprim = declare_projections mie.mind_entry_universes mind in declare_mib_implicits mind; declare_inductive_argument_scopes mind mie; oname, isprim diff --git a/interp/genredexpr.ml b/interp/genredexpr.ml index 42c1fe429..607f2258f 100644 --- a/interp/genredexpr.ml +++ b/interp/genredexpr.ml @@ -60,6 +60,6 @@ open Constrexpr type r_trm = constr_expr type r_pat = constr_pattern_expr -type r_cst = reference or_by_notation +type r_cst = qualid or_by_notation type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index b54e2badd..83ad9af33 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -96,9 +96,11 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = else l in let rec aux bdvars l c = match CAst.(c.v) with - | CRef ({CAst.v=Ident id},_) -> found c.CAst.loc id bdvars l - | CNotation ("{ _ : _ | _ }", ({ CAst.v = CRef ({CAst.v=Ident id},_) } :: _, [], [], [])) when not (Id.Set.mem id bdvars) -> - Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add id bdvars) l c + | CRef (qid,_) when qualid_is_ident qid -> + found c.CAst.loc (qualid_basename qid) bdvars l + | CNotation ("{ _ : _ | _ }", ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when + qualid_is_ident qid && not (Id.Set.mem (qualid_basename qid) bdvars) -> + Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add (qualid_basename qid) bdvars) l c | _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c in aux bound l c @@ -196,7 +198,7 @@ let combine_params avoid fn applied needed = let combine_params_freevar = fun avoid (_, decl) -> let id' = next_name_away_from (RelDecl.get_name decl) avoid in - (CAst.make @@ CRef (CAst.make @@ Ident id',None), Id.Set.add id' avoid) + (CAst.make @@ CRef (qualid_of_ident id',None), Id.Set.add id' avoid) let destClassApp cl = let open CAst in @@ -218,9 +220,8 @@ let destClassAppExpl cl = let implicit_application env ?(allow_partial=true) f ty = let is_class = try - let ({CAst.v=(r, _, _)} as clapp) = destClassAppExpl ty in - let qid = qualid_of_reference r in - let gr = Nametab.locate qid.CAst.v in + let ({CAst.v=(qid, _, _)} as clapp) = destClassAppExpl ty in + let gr = Nametab.locate qid in if Typeclasses.is_class gr then Some (clapp, gr) else None with Not_found -> None in diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index 25394fc0d..a8492095e 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -16,8 +16,8 @@ open Libnames val declare_generalizable : local:bool -> 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) CAst.t -val destClassAppExpl : constr_expr -> (reference * (constr_expr * explicitation CAst.t option) list * instance_expr option) CAst.t +val destClassApp : constr_expr -> (qualid * constr_expr list * instance_expr option) CAst.t +val destClassAppExpl : constr_expr -> (qualid * (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 *) diff --git a/interp/modintern.ml b/interp/modintern.ml index 33c07d551..c27cc9cc0 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -45,8 +45,9 @@ let error_application_to_module_type loc = or both are searched. The returned kind is never ModAny, and it is equal to the input kind when this one isn't ModAny. *) -let lookup_module_or_modtype kind {CAst.loc;v=qid} = +let lookup_module_or_modtype kind qid = let open Declaremods in + let loc = qid.CAst.loc in try if kind == ModType then raise Not_found; let mp = Nametab.locate_module qid in @@ -84,7 +85,7 @@ let loc_of_module l = l.CAst.loc let rec interp_module_ast env kind m cst = match m with | {CAst.loc;v=CMident qid} -> - let (mp,kind) = lookup_module_or_modtype kind CAst.(make ?loc qid) in + let (mp,kind) = lookup_module_or_modtype kind qid in (MEident mp, kind, cst) | {CAst.loc;v=CMapply (me1,me2)} -> let me1',kind1, cst = interp_module_ast env kind me1 cst in diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index e1fbdba87..91491bdf8 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -41,26 +41,24 @@ let global_of_extended_global = function | [],NApp (NRef ref,[]) -> ref | _ -> raise Not_found -let locate_global_with_alias ?(head=false) {CAst.loc; v=qid} = +let locate_global_with_alias ?(head=false) qid = let ref = Nametab.locate_extended qid in try if head then global_of_extended_global_head ref else global_of_extended_global ref with Not_found -> - user_err ?loc (pr_qualid qid ++ + user_err ?loc:qid.CAst.loc (pr_qualid qid ++ str " is bound to a notation that does not denote a reference.") -let global_inductive_with_alias ({CAst.loc} as lr) = - let qid = qualid_of_reference lr in +let global_inductive_with_alias qid = try match locate_global_with_alias qid with | IndRef ind -> ind | ref -> - user_err ?loc ~hdr:"global_inductive" - (pr_reference lr ++ spc () ++ str "is not an inductive type.") + user_err ?loc:qid.CAst.loc ~hdr:"global_inductive" + (pr_qualid qid ++ spc () ++ str "is not an inductive type.") with Not_found -> Nametab.error_global_not_found qid -let global_with_alias ?head r = - let qid = qualid_of_reference r in +let global_with_alias ?head qid = try locate_global_with_alias ?head qid with Not_found -> Nametab.error_global_not_found qid diff --git a/interp/smartlocate.mli b/interp/smartlocate.mli index 6b574d7b5..e41ef7891 100644 --- a/interp/smartlocate.mli +++ b/interp/smartlocate.mli @@ -17,7 +17,7 @@ open Globnames if not bound in the global env; raise a [UserError] if bound to a syntactic def that does not denote a reference *) -val locate_global_with_alias : ?head:bool -> qualid CAst.t -> GlobRef.t +val locate_global_with_alias : ?head:bool -> qualid -> GlobRef.t (** Extract a global_reference from a reference that can be an "alias" *) val global_of_extended_global : extended_global_reference -> GlobRef.t @@ -26,13 +26,13 @@ val global_of_extended_global : extended_global_reference -> GlobRef.t May raise [Nametab.GlobalizationError _] for an unknown reference, or a [UserError] if bound to a syntactic def that does not denote a reference. *) -val global_with_alias : ?head:bool -> reference -> GlobRef.t +val global_with_alias : ?head:bool -> qualid -> GlobRef.t (** The same for inductive types *) -val global_inductive_with_alias : reference -> inductive +val global_inductive_with_alias : qualid -> inductive (** Locate a reference taking into account notations and "aliases" *) -val smart_global : ?head:bool -> reference Constrexpr.or_by_notation -> GlobRef.t +val smart_global : ?head:bool -> qualid Constrexpr.or_by_notation -> GlobRef.t (** The same for inductive types *) -val smart_global_inductive : reference Constrexpr.or_by_notation -> inductive +val smart_global_inductive : qualid Constrexpr.or_by_notation -> inductive diff --git a/interp/stdarg.mli b/interp/stdarg.mli index 4792cda08..5e5e43ed3 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -41,7 +41,7 @@ val wit_ident : Id.t uniform_genarg_type val wit_var : (lident, lident, Id.t) genarg_type -val wit_ref : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type +val wit_ref : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type val wit_sort_family : (Sorts.family, unit, unit) genarg_type @@ -53,7 +53,7 @@ val wit_open_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type val wit_red_expr : - ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, + ((constr_expr,qualid or_by_notation,constr_expr) red_expr_gen, (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 @@ -63,10 +63,10 @@ val wit_clause_dft_concl : (lident Locus.clause_expr, lident Locus.clause_expr, val wit_integer : int uniform_genarg_type val wit_preident : string uniform_genarg_type -val wit_reference : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type -val wit_global : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type +val wit_reference : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type +val wit_global : (qualid, GlobRef.t located or_var, GlobRef.t) genarg_type val wit_clause : (lident Locus.clause_expr, lident Locus.clause_expr, Names.Id.t Locus.clause_expr) genarg_type val wit_redexpr : - ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, + ((constr_expr,qualid or_by_notation,constr_expr) red_expr_gen, (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 diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 5783453e6..68057b389 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -156,7 +156,6 @@ type inline = bool type result = { cook_body : constant_def; cook_type : types; - cook_proj : bool; cook_universes : constant_universes; cook_inline : inline; cook_context : Context.Named.t option; @@ -230,7 +229,6 @@ let cook_constant ~hcons env { from = cb; info } = { cook_body = body; cook_type = typ; - cook_proj = cb.const_proj; cook_universes = univs; cook_inline = cb.const_inline_code; cook_context = Some const_hyps; diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 0d907f3de..76c79335f 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -21,7 +21,6 @@ type inline = bool type result = { cook_body : constant_def; cook_type : types; - cook_proj : bool; cook_universes : constant_universes; cook_inline : inline; cook_context : Context.Named.t option; diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 7bd70c050..7bd7d6c9c 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -54,8 +54,6 @@ type projection_body = { proj_npars : int; proj_arg : int; (** Projection index, starting from 0 *) proj_type : types; (* Type under params *) - proj_eta : constr * types; (* Eta-expanded term and type *) - proj_body : constr; (* For compatibility with VMs only, the match version *) } (* Global declarations (i.e. constants) can be either: *) @@ -87,7 +85,6 @@ type constant_body = { const_type : types; const_body_code : Cemitcodes.to_patch_substituted option; const_universes : constant_universes; - const_proj : bool; const_inline_code : bool; const_typing_flags : typing_flags; (** The typing options which were used for diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 75c0e5b4c..1b73096f7 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -86,7 +86,7 @@ let subst_const_def sub def = match def with let subst_const_proj sub pb = { pb with proj_ind = subst_mind sub pb.proj_ind; proj_type = subst_mps sub pb.proj_type; - proj_body = subst_const_type sub pb.proj_body } + } let subst_const_body sub cb = assert (List.is_empty cb.const_hyps); (* we're outside sections *) @@ -100,7 +100,6 @@ let subst_const_body sub cb = { const_hyps = []; const_body = body'; const_type = type'; - const_proj = cb.const_proj; const_body_code = Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code; const_universes = cb.const_universes; diff --git a/kernel/entries.ml b/kernel/entries.ml index 94da00c7e..3c555f8c7 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -95,14 +95,9 @@ type inline = int option (* inlining level, None for no inlining *) type parameter_entry = Context.Named.t option * types in_constant_universes_entry * inline -type projection_entry = { - proj_entry_ind : MutInd.t; - proj_entry_arg : int } - type 'a constant_entry = | DefinitionEntry of 'a definition_entry | ParameterEntry of parameter_entry - | ProjectionEntry of projection_entry (** {6 Modules } *) diff --git a/kernel/environ.ml b/kernel/environ.ml index fb89576dd..2d6c9117b 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -490,7 +490,7 @@ let lookup_projection cst env = Cmap_env.find (Projection.constant cst) env.env_globals.env_projections let is_projection cst env = - (lookup_constant cst env).const_proj + Cmap_env.mem cst env.env_globals.env_projections (* Mutual Inductives *) let polymorphic_ind (mind,i) env = diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 439acd15b..14f2a3d8f 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -797,16 +797,13 @@ exception UndefinableExpansion build an expansion function. The term built is expecting to be substituted first by a substitution of the form [params, x : ind params] *) -let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params +let compute_projections ((kn, _ as ind), u) nparamargs params mind_consnrealdecls mind_consnrealargs paramslet ctx = let mp, dp, l = MutInd.repr3 kn in (** We build a substitution smashing the lets in the record parameters so that typechecking projections requires just a substitution and not matching with a parameter context. *) - let indty, paramsletsubst = - (* [ty] = [Ind inst] is typed in context [params] *) - let inst = Context.Rel.to_extended_vect mkRel 0 paramslet in - let ty = mkApp (mkIndU indu, inst) in + let paramsletsubst = (* [Ind inst] is typed in context [params-wo-let] *) let inst' = rel_list 0 nparamargs in (* {params-wo-let |- subst:params] *) @@ -814,48 +811,21 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params (* {params-wo-let, x:Ind inst' |- subst':(params,x:Ind inst)] *) let subst = (* For the record parameter: *) mkRel 1 :: List.map (lift 1) subst in - ty, subst + subst in - let ci = - let print_info = - { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in - { ci_ind = ind; - ci_npar = nparamargs; - ci_cstr_ndecls = mind_consnrealdecls; - ci_cstr_nargs = mind_consnrealargs; - ci_pp_info = print_info } - in - let len = List.length ctx in - let x = Name x in - let compat_body ccl i = - (* [ccl] is defined in context [params;x:indty] *) - (* [ccl'] is defined in context [params;x:indty;x:indty] *) - let ccl' = liftn 1 2 ccl in - let p = mkLambda (x, lift 1 indty, ccl') in - let branch = it_mkLambda_or_LetIn (mkRel (len - i)) ctx in - let body = mkCase (ci, p, mkRel 1, [|lift 1 branch|]) in - it_mkLambda_or_LetIn (mkLambda (x,indty,body)) params - in - let projections decl (i, j, kns, pbs, subst, letsubst) = + let projections decl (i, j, kns, pbs, letsubst) = match decl with | LocalDef (na,c,t) -> (* From [params, field1,..,fieldj |- c(params,field1,..,fieldj)] to [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] *) let c = liftn 1 j c in (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] - to [params, x:I |- c(params,proj1 x,..,projj x)] *) - let c1 = substl subst c in - (* From [params, x:I |- subst:field1,..,fieldj] - to [params, x:I |- subst:field1,..,fieldj+1] where [subst] - is represented with instance of field1 last *) - let subst = c1 :: subst in - (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] to [params-wo-let, x:I |- c(params,proj1 x,..,projj x)] *) let c2 = substl letsubst c in (* From [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj)] to [params-wo-let, x:I |- subst:(params, x:I, field1,..,fieldj+1)] *) let letsubst = c2 :: letsubst in - (i, j+1, kns, pbs, subst, letsubst) + (i, j+1, kns, pbs, letsubst) | LocalAssum (na,t) -> match na with | Name id -> @@ -868,21 +838,14 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params let projty = substl letsubst t in (* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)] to [params, x:I |- t(proj1 x,..,projj x)] *) - let ty = substl subst t in - let term = mkProj (Projection.make kn true, mkRel 1) in let fterm = mkProj (Projection.make kn false, mkRel 1) in - let compat = compat_body ty (j - 1) in - let etab = it_mkLambda_or_LetIn (mkLambda (x, indty, term)) params in - let etat = it_mkProd_or_LetIn (mkProd (x, indty, ty)) params in let body = { proj_ind = fst ind; proj_npars = nparamargs; - proj_arg = i; proj_type = projty; proj_eta = etab, etat; - proj_body = compat } in - (i + 1, j + 1, kn :: kns, body :: pbs, - fterm :: subst, fterm :: letsubst) + proj_arg = i; proj_type = projty; } in + (i + 1, j + 1, kn :: kns, body :: pbs, fterm :: letsubst) | Anonymous -> raise UndefinableExpansion in - let (_, _, kns, pbs, subst, letsubst) = - List.fold_right projections ctx (0, 1, [], [], [], paramsletsubst) + let (_, _, kns, pbs, letsubst) = + List.fold_right projections ctx (0, 1, [], [], paramsletsubst) in Array.of_list (List.rev kns), Array.of_list (List.rev pbs) @@ -987,7 +950,7 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r (try let fields, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in let kns, projs = - compute_projections indsp pkt.mind_typename rid nparamargs paramsctxt + compute_projections indsp nparamargs paramsctxt pkt.mind_consnrealdecls pkt.mind_consnrealargs paramslet fields in Some (Some (rid, kns, projs)) with UndefinableExpansion -> Some None) diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 5a38172c2..45228e35e 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -43,7 +43,7 @@ val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_induct val enforce_indices_matter : unit -> unit val is_indices_matter : unit -> bool -val compute_projections : pinductive -> Id.t -> Id.t -> +val compute_projections : pinductive -> int -> Context.Rel.t -> int array -> int array -> Context.Rel.t -> Context.Rel.t -> (Constant.t array * projection_body array) diff --git a/kernel/names.ml b/kernel/names.ml index 597061278..1d2a7c4ce 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -17,7 +17,7 @@ the module system, Aug 2002 *) (* Abstraction over the type of constant for module inlining by Claudio Sacerdoti, Nov 2004 *) -(* Miscellaneous features or improvements by Hugo Herbelin, +(* Miscellaneous features or improvements by Hugo Herbelin, Élie Soubiran, ... *) open Pp @@ -364,7 +364,6 @@ module MPmap = CMap.Make(ModPath) module KerName = struct type t = { - canary : Canary.t; modpath : ModPath.t; dirpath : DirPath.t; knlabel : Label.t; @@ -372,16 +371,14 @@ module KerName = struct (** Lazily computed hash. If unset, it is set to negative values. *) } - let canary = Canary.obj - type kernel_name = t let make modpath dirpath knlabel = - { modpath; dirpath; knlabel; refhash = -1; canary; } + { modpath; dirpath; knlabel; refhash = -1; } let repr kn = (kn.modpath, kn.dirpath, kn.knlabel) let make2 modpath knlabel = - { modpath; dirpath = DirPath.empty; knlabel; refhash = -1; canary; } + { modpath; dirpath = DirPath.empty; knlabel; refhash = -1; } let modpath kn = kn.modpath let label kn = kn.knlabel @@ -437,7 +434,7 @@ module KerName = struct * (string -> string) let hashcons (hmod,hdir,hstr) kn = let { modpath = mp; dirpath = dp; knlabel = l; refhash; } = kn in - { modpath = hmod mp; dirpath = hdir dp; knlabel = hstr l; refhash; canary; } + { modpath = hmod mp; dirpath = hdir dp; knlabel = hstr l; refhash; } let eq kn1 kn2 = kn1.modpath == kn2.modpath && kn1.dirpath == kn2.dirpath && kn1.knlabel == kn2.knlabel diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index db1109e75..37bf679c5 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -250,7 +250,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = Undef nl; cook_type = t; - cook_proj = false; cook_universes = univs; cook_inline = false; cook_context = ctx; @@ -291,7 +290,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = def; cook_type = typ; - cook_proj = false; cook_universes = Monomorphic_const univs; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; @@ -343,39 +341,11 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = def; cook_type = typ; - cook_proj = false; cook_universes = univs; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; } - | ProjectionEntry {proj_entry_ind = ind; proj_entry_arg = i} -> - let mib, _ = Inductive.lookup_mind_specif env (ind,0) in - let kn, pb = - match mib.mind_record with - | Some (Some (id, kns, pbs)) -> - if i < Array.length pbs then - kns.(i), pbs.(i) - else assert false - | _ -> assert false - in - let univs = - match mib.mind_universes with - | Monomorphic_ind ctx -> Monomorphic_const ctx - | Polymorphic_ind auctx -> Polymorphic_const auctx - | Cumulative_ind acumi -> - Polymorphic_const (Univ.ACumulativityInfo.univ_context acumi) - in - let term, typ = pb.proj_eta in - { - Cooking.cook_body = Def (Mod_subst.from_val (Constr.hcons term)); - cook_type = typ; - cook_proj = true; - cook_universes = univs; - cook_inline = false; - cook_context = None; - } - let record_aux env s_ty s_bo = let in_ty = keep_hyps env s_ty in let v = @@ -464,7 +434,6 @@ let build_constant_declaration kn env result = { const_hyps = hyps; const_body = def; const_type = typ; - const_proj = result.cook_proj; const_body_code = tps; const_universes = univs; const_inline_code = result.cook_inline; diff --git a/lib/spawn.ml b/lib/spawn.ml index 63e9e452c..0652623b7 100644 --- a/lib/spawn.ml +++ b/lib/spawn.ml @@ -15,14 +15,12 @@ let accept_timeout = 10.0 let pr_err s = Printf.eprintf "(Spawn ,%d) %s\n%!" (Unix.getpid ()) s let prerr_endline s = if !Flags.debug then begin pr_err s end else () -type req = ReqDie | ReqStats | Hello of int * int -type resp = RespStats of Gc.stat +type req = ReqDie | Hello of int * int module type Control = sig type handle val kill : handle -> unit - val stats : handle -> Gc.stat val wait : handle -> Unix.process_status val unixpid : handle -> int val uid : handle -> string @@ -43,7 +41,6 @@ module type MainLoopModel = sig end (* Common code *) -let assert_ b s = if not b then CErrors.anomaly (Pp.str s) (* According to http://caml.inria.fr/mantis/view.php?id=5325 * you can't use the same socket for both writing and reading (may change @@ -125,14 +122,26 @@ let filter_args args = Array.of_list (aux (Array.to_list args)) let spawn_with_control prefer_sock env prog args = - let control_sock, control_sock_name = mk_socket_channel () in - let extra = [| "-control-channel"; control_sock_name |] in - let args = Array.append extra (filter_args args) in + (* on non-Unix systems we create a control channel *) + let not_Unix = Sys.os_type <> "Unix" in + let args = filter_args args in + let args, control_sock = + if not_Unix then + let control_sock, control_sock_name = mk_socket_channel () in + let extra = [| "-control-channel"; control_sock_name |] in + Array.append extra args, Some control_sock + else + args, None in let (pid, cin, cout, s), is_sock = - if Sys.os_type <> "Unix" || prefer_sock + if not_Unix (* pipes only work well on Unix *) || prefer_sock then spawn_sock env prog args, true else spawn_pipe env prog args, false in - let _, oob_resp, oob_req = accept control_sock in + let oob_resp, oob_req = + if not_Unix then + let _, oob_resp, oob_req = accept (Option.get control_sock) in + Some oob_resp, Some oob_req + else + None, None in pid, oob_resp, oob_req, cin, cout, s, is_sock let output_death_sentence pid oob_req = @@ -146,8 +155,8 @@ module Async(ML : MainLoopModel) = struct type process = { cin : in_channel; cout : out_channel; - oob_resp : in_channel; - oob_req : out_channel; + oob_resp : in_channel option; + oob_req : out_channel option; gchan : ML.async_chan; pid : int; mutable watch : ML.watch_id option; @@ -166,11 +175,11 @@ let kill ({ pid = unixpid; oob_resp; oob_req; cin; cout; alive; watch } as p) = if not alive then prerr_endline "This process is already dead" else begin try Option.iter ML.remove_watch watch; - output_death_sentence (uid p) oob_req; + Option.iter (output_death_sentence (uid p)) oob_req; close_in_noerr cin; close_out_noerr cout; - close_in_noerr oob_resp; - close_out_noerr oob_req; + Option.iter close_in_noerr oob_resp; + Option.iter close_out_noerr oob_req; if Sys.os_type = "Unix" then Unix.kill unixpid 9; p.watch <- None with e -> prerr_endline ("kill: "^Printexc.to_string e) end @@ -199,12 +208,6 @@ let spawn ?(prefer_sock=prefer_sock) ?(env=Unix.environment ()) ); p, cout -let stats { oob_req; oob_resp; alive } = - assert_ alive "This process is dead."; - output_value oob_req ReqStats; - flush oob_req; - input_value oob_resp - let rec wait p = (* On windows kill is not reliable, so wait may never return. *) if Sys.os_type = "Unix" then @@ -221,8 +224,8 @@ module Sync () = struct type process = { cin : in_channel; cout : out_channel; - oob_resp : in_channel; - oob_req : out_channel; + oob_resp : in_channel option; + oob_req : out_channel option; pid : int; mutable alive : bool; } @@ -242,20 +245,14 @@ let kill ({ pid = unixpid; oob_req; oob_resp; cin; cout; alive } as p) = p.alive <- false; if not alive then prerr_endline "This process is already dead" else begin try - output_death_sentence (uid p) oob_req; + Option.iter (output_death_sentence (uid p)) oob_req; close_in_noerr cin; close_out_noerr cout; - close_in_noerr oob_resp; - close_out_noerr oob_req; + Option.iter close_in_noerr oob_resp; + Option.iter close_out_noerr oob_req; if Sys.os_type = "Unix" then Unix.kill unixpid 9; with e -> prerr_endline ("kill: "^Printexc.to_string e) end -let stats { oob_req; oob_resp; alive } = - assert_ alive "This process is dead."; - output_value oob_req ReqStats; - flush oob_req; - let RespStats g = input_value oob_resp in g - let rec wait p = (* On windows kill is not reliable, so wait may never return. *) if Sys.os_type = "Unix" then diff --git a/lib/spawn.mli b/lib/spawn.mli index c7a56349c..944aa27a7 100644 --- a/lib/spawn.mli +++ b/lib/spawn.mli @@ -25,7 +25,6 @@ module type Control = sig type handle val kill : handle -> unit - val stats : handle -> Gc.stat val wait : handle -> Unix.process_status val unixpid : handle -> int @@ -76,6 +75,5 @@ end (* This is exported to separate the Spawned module, that for simplicity assumes * Threads so it is in a separate file *) -type req = ReqDie | ReqStats | Hello of int * int +type req = ReqDie | Hello of int * int val proto_version : int -type resp = RespStats of Gc.stat diff --git a/library/goptions.ml b/library/goptions.ml index 76071ebcc..f14ad333e 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -161,7 +161,7 @@ module type RefConvertArg = sig type t val compare : t -> t -> int - val encode : reference -> t + val encode : qualid -> t val subst : substitution -> t -> t val printer : t -> Pp.t val key : option_name @@ -172,7 +172,7 @@ end module RefConvert = functor (A : RefConvertArg) -> struct type t = A.t - type key = reference + type key = qualid let compare = A.compare let table = ref_table let encode = A.encode diff --git a/library/goptions.mli b/library/goptions.mli index 6c14d19ee..3d7df18fe 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -89,7 +89,7 @@ module MakeRefTable : (A : sig type t val compare : t -> t -> int - val encode : reference -> t + val encode : qualid -> t val subst : substitution -> t -> t val printer : t -> Pp.t val key : option_name @@ -147,9 +147,9 @@ val get_string_table : val get_ref_table : option_name -> - < add : reference -> unit; - remove : reference -> unit; - mem : reference -> unit; + < add : qualid -> unit; + remove : qualid -> unit; + mem : qualid -> unit; print : unit > (** The first argument is a locality flag. *) diff --git a/library/heads.ml b/library/heads.ml index 3d5f6a6ff..d9d650ac0 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -129,7 +129,7 @@ let compute_head = function let cb = Environ.lookup_constant cst env in let is_Def = function Declarations.Def _ -> true | _ -> false in let body = - if not cb.Declarations.const_proj && is_Def cb.Declarations.const_body + if not (Environ.is_projection cst env) && is_Def cb.Declarations.const_body then Global.body_of_constant cst else None in (match body with diff --git a/library/libnames.ml b/library/libnames.ml index 8d5a02a29..23085048a 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -134,23 +134,33 @@ let restrict_path n sp = make_path (DirPath.make dir') s (*s qualified names *) -type qualid = full_path +type qualid_r = full_path +type qualid = qualid_r CAst.t -let make_qualid = make_path -let repr_qualid = repr_path +let make_qualid ?loc pa id = CAst.make ?loc (make_path pa id) +let repr_qualid {CAst.v=qid} = repr_path qid -let qualid_eq = eq_full_path +let qualid_eq qid1 qid2 = eq_full_path qid1.CAst.v qid2.CAst.v -let string_of_qualid = string_of_path -let pr_qualid = pr_path +let string_of_qualid qid = string_of_path qid.CAst.v +let pr_qualid qid = pr_path qid.CAst.v -let qualid_of_string = path_of_string +let qualid_of_string ?loc s = CAst.make ?loc @@ path_of_string s -let qualid_of_path sp = sp -let qualid_of_ident id = make_qualid DirPath.empty id -let qualid_of_dirpath dir = +let qualid_of_path ?loc sp = CAst.make ?loc sp +let qualid_of_ident ?loc id = make_qualid ?loc DirPath.empty id +let qualid_of_dirpath ?loc dir = let (l,a) = split_dirpath dir in - make_qualid l a + make_qualid ?loc l a + +let qualid_is_ident qid = + DirPath.is_empty qid.CAst.v.dirpath + +let qualid_basename qid = + qid.CAst.v.basename + +let qualid_path qid = + qid.CAst.v.dirpath type object_name = full_path * KerName.t @@ -183,52 +193,6 @@ let eq_global_dir_reference r1 r2 = match r1, r2 with | DirModule op1, DirModule op2 -> eq_op op1 op2 | _ -> false -type reference_r = - | Qualid of qualid - | Ident of Id.t -type reference = reference_r CAst.t - -let qualid_of_reference = CAst.map (function - | Qualid qid -> qid - | Ident id -> qualid_of_ident id) - -let string_of_reference = CAst.with_val (function - | Qualid qid -> string_of_qualid qid - | Ident id -> Id.to_string id) - -let pr_reference = CAst.with_val (function - | Qualid qid -> pr_qualid qid - | Ident id -> Id.print id) - -let eq_reference {CAst.v=r1} {CAst.v=r2} = match r1, r2 with -| Qualid q1, Qualid q2 -> qualid_eq q1 q2 -| Ident id1, Ident id2 -> Id.equal id1 id2 -| _ -> false - -let join_reference {CAst.loc=l1;v=ns} {CAst.loc=l2;v=r} = - CAst.make ?loc:(Loc.merge_opt l1 l2) ( - match ns , r with - Qualid q1, Qualid q2 -> - let (dp1,id1) = repr_qualid q1 in - let (dp2,id2) = repr_qualid q2 in - Qualid (make_qualid - (append_dirpath (append_dirpath dp1 (dirpath_of_string (Names.Id.to_string id1))) dp2) - id2) - | Qualid q1, Ident id2 -> - let (dp1,id1) = repr_qualid q1 in - Qualid (make_qualid - (append_dirpath dp1 (dirpath_of_string (Names.Id.to_string id1))) - id2) - | Ident id1, Qualid q2 -> - let (dp2,id2) = repr_qualid q2 in - Qualid (make_qualid - (append_dirpath (dirpath_of_string (Names.Id.to_string id1)) dp2) - id2) - | Ident id1, Ident id2 -> - Qualid (make_qualid - (dirpath_of_string (Names.Id.to_string id1)) id2) - ) - (* Default paths *) let default_library = Names.DirPath.initial (* = ["Top"] *) diff --git a/library/libnames.mli b/library/libnames.mli index 5f69b1f0f..447eecbb5 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -65,23 +65,28 @@ val restrict_path : int -> full_path -> full_path qualifications of absolute names, including single identifiers. The [qualid] are used to access the name table. *) -type qualid +type qualid_r +type qualid = qualid_r CAst.t -val make_qualid : DirPath.t -> Id.t -> qualid +val make_qualid : ?loc:Loc.t -> DirPath.t -> Id.t -> qualid val repr_qualid : qualid -> DirPath.t * Id.t val qualid_eq : qualid -> qualid -> bool val pr_qualid : qualid -> Pp.t val string_of_qualid : qualid -> string -val qualid_of_string : string -> qualid +val qualid_of_string : ?loc:Loc.t -> string -> qualid (** Turns an absolute name, a dirpath, or an Id.t into a qualified name denoting the same name *) -val qualid_of_path : full_path -> qualid -val qualid_of_dirpath : DirPath.t -> qualid -val qualid_of_ident : Id.t -> qualid +val qualid_of_path : ?loc:Loc.t -> full_path -> qualid +val qualid_of_dirpath : ?loc:Loc.t -> DirPath.t -> qualid +val qualid_of_ident : ?loc:Loc.t -> Id.t -> qualid + +val qualid_is_ident : qualid -> bool +val qualid_path : qualid -> DirPath.t +val qualid_basename : qualid -> Id.t (** Both names are passed to objects: a "semantic" [kernel_name], which can be substituted and a "syntactic" [full_path] which can be printed @@ -124,20 +129,6 @@ val eq_global_dir_reference : global_dir_reference -> global_dir_reference -> bool (** {6 ... } *) -(** A [reference] is the user-level notion of name. It denotes either a - global name (referred either by a qualified name or by a single - name) or a variable *) - -type reference_r = - | Qualid of qualid - | Ident of Id.t -type reference = reference_r CAst.t - -val eq_reference : reference -> reference -> bool -val qualid_of_reference : reference -> qualid CAst.t -val string_of_reference : reference -> string -val pr_reference : reference -> Pp.t -val join_reference : reference -> reference -> reference (** some preset paths *) val default_library : DirPath.t diff --git a/library/library.ml b/library/library.ml index 56d2709d5..400f3dcf1 100644 --- a/library/library.ml +++ b/library/library.ml @@ -577,10 +577,10 @@ let require_library_from_dirpath modrefl export = (* the function called by Vernacentries.vernac_import *) -let safe_locate_module {CAst.loc;v=qid} = +let safe_locate_module qid = try Nametab.locate_module qid with Not_found -> - user_err ?loc ~hdr:"import_library" + user_err ?loc:qid.CAst.loc ~hdr:"import_library" (pr_qualid qid ++ str " is not a module") let import_module export modl = @@ -595,18 +595,18 @@ let import_module export modl = | [] -> () | modl -> add_anonymous_leaf (in_import_library (List.rev modl, export)) in let rec aux acc = function - | ({CAst.loc; v=dir} as m) :: l -> + | qid :: l -> let m,acc = - try Nametab.locate_module dir, acc - with Not_found-> flush acc; safe_locate_module m, [] in + try Nametab.locate_module qid, acc + with Not_found-> flush acc; safe_locate_module qid, [] in (match m with | MPfile dir -> aux (dir::acc) l | mp -> flush acc; try Declaremods.import_module export mp; aux [] l with Not_found -> - user_err ?loc ~hdr:"import_library" - (pr_qualid dir ++ str " is not a module")) + user_err ?loc:qid.CAst.loc ~hdr:"import_library" + (pr_qualid qid ++ str " is not a module")) | [] -> flush acc in aux [] modl diff --git a/library/library.mli b/library/library.mli index 0877ebb5a..d5815afc4 100644 --- a/library/library.mli +++ b/library/library.mli @@ -36,7 +36,7 @@ type seg_proofs = Constr.constr Future.computation array (** Open a module (or a library); if the boolean is true then it's also an export otherwise just a simple import *) -val import_module : bool -> qualid CAst.t list -> unit +val import_module : bool -> qualid list -> unit (** Start the compilation of a file as a library. The first argument must be output file, and the diff --git a/library/nametab.ml b/library/nametab.ml index 995f44706..a3b3ca6e7 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -18,8 +18,8 @@ open Globnames exception GlobalizationError of qualid -let error_global_not_found {CAst.loc;v} = - Loc.raise ?loc (GlobalizationError v) +let error_global_not_found qid = + Loc.raise ?loc:qid.CAst.loc (GlobalizationError qid) (* The visibility can be registered either - for all suffixes not shorter then a given int - when the object @@ -69,7 +69,7 @@ module type NAMETREE = sig val find : user_name -> t -> elt val exists : user_name -> t -> bool val user_name : qualid -> t -> user_name - val shortest_qualid : Id.Set.t -> user_name -> t -> qualid + val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid val find_prefixes : qualid -> t -> elt list end @@ -220,7 +220,7 @@ let exists uname tab = with Not_found -> false -let shortest_qualid ctx uname tab = +let shortest_qualid ?loc ctx uname tab = let id,dir = U.repr uname in let hidden = Id.Set.mem id ctx in let rec find_uname pos dir tree = @@ -235,7 +235,7 @@ let shortest_qualid ctx uname tab = in let ptab = Id.Map.find id tab in let found_dir = find_uname [] dir ptab in - make_qualid (DirPath.make found_dir) id + make_qualid ?loc (DirPath.make found_dir) id let push_node node l = match node with @@ -458,14 +458,13 @@ let global_of_path sp = let extended_global_of_path sp = ExtRefTab.find sp !the_ccitab -let global ({CAst.loc;v=r} as lr)= - let {CAst.loc; v} as qid = qualid_of_reference lr in - try match locate_extended v with +let global qid = + try match locate_extended qid with | TrueGlobal ref -> ref | SynDef _ -> - user_err ?loc ~hdr:"global" + user_err ?loc:qid.CAst.loc ~hdr:"global" (str "Unexpected reference to a notation: " ++ - pr_qualid v) + pr_qualid qid) with Not_found -> error_global_not_found qid @@ -510,40 +509,40 @@ let path_of_universe mp = (* Shortest qualid functions **********************************************) -let shortest_qualid_of_global ctx ref = +let shortest_qualid_of_global ?loc ctx ref = match ref with - | VarRef id -> make_qualid DirPath.empty id + | VarRef id -> make_qualid ?loc DirPath.empty id | _ -> let sp = Globrevtab.find (TrueGlobal ref) !the_globrevtab in - ExtRefTab.shortest_qualid ctx sp !the_ccitab + ExtRefTab.shortest_qualid ?loc ctx sp !the_ccitab -let shortest_qualid_of_syndef ctx kn = +let shortest_qualid_of_syndef ?loc ctx kn = let sp = path_of_syndef kn in - ExtRefTab.shortest_qualid ctx sp !the_ccitab + ExtRefTab.shortest_qualid ?loc ctx sp !the_ccitab -let shortest_qualid_of_module mp = +let shortest_qualid_of_module ?loc mp = let dir = MPmap.find mp !the_modrevtab in - DirTab.shortest_qualid Id.Set.empty dir !the_dirtab + DirTab.shortest_qualid ?loc Id.Set.empty dir !the_dirtab -let shortest_qualid_of_modtype kn = +let shortest_qualid_of_modtype ?loc kn = let sp = MPmap.find kn !the_modtyperevtab in - MPTab.shortest_qualid Id.Set.empty sp !the_modtypetab + MPTab.shortest_qualid ?loc Id.Set.empty sp !the_modtypetab -let shortest_qualid_of_universe kn = +let shortest_qualid_of_universe ?loc kn = let sp = UnivIdMap.find kn !the_univrevtab in - UnivTab.shortest_qualid Id.Set.empty sp !the_univtab + UnivTab.shortest_qualid ?loc Id.Set.empty sp !the_univtab let pr_global_env env ref = try pr_qualid (shortest_qualid_of_global env ref) with Not_found as e -> if !Flags.debug then Feedback.msg_debug (Pp.str "pr_global_env not found"); raise e -let global_inductive ({CAst.loc; v=r} as lr) = - match global lr with +let global_inductive qid = + match global qid with | IndRef ind -> ind | ref -> - user_err ?loc ~hdr:"global_inductive" - (pr_reference lr ++ spc () ++ str "is not an inductive type") + user_err ?loc:qid.CAst.loc ~hdr:"global_inductive" + (pr_qualid qid ++ spc () ++ str "is not an inductive type") (********************************************************************) diff --git a/library/nametab.mli b/library/nametab.mli index 2ec73a986..57e9141db 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -61,7 +61,7 @@ open Globnames exception GlobalizationError of qualid (** Raises a globalization error *) -val error_global_not_found : qualid CAst.t -> 'a +val error_global_not_found : qualid -> 'a (** {6 Register visibility of things } *) @@ -105,8 +105,8 @@ val locate_universe : qualid -> universe_id references, like [locate] and co, but raise a nice error message in case of failure *) -val global : reference -> GlobRef.t -val global_inductive : reference -> inductive +val global : qualid -> GlobRef.t +val global_inductive : qualid -> inductive (** These functions locate all global references with a given suffix; if [qualid] is valid as such, it comes first in the list *) @@ -168,11 +168,11 @@ val pr_global_env : Id.Set.t -> GlobRef.t -> Pp.t Coq.A.B.x that denotes the same object. @raise Not_found for unknown objects. *) -val shortest_qualid_of_global : Id.Set.t -> GlobRef.t -> qualid -val shortest_qualid_of_syndef : Id.Set.t -> syndef_name -> qualid -val shortest_qualid_of_modtype : ModPath.t -> qualid -val shortest_qualid_of_module : ModPath.t -> qualid -val shortest_qualid_of_universe : universe_id -> qualid +val shortest_qualid_of_global : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid +val shortest_qualid_of_syndef : ?loc:Loc.t -> Id.Set.t -> syndef_name -> qualid +val shortest_qualid_of_modtype : ?loc:Loc.t -> ModPath.t -> qualid +val shortest_qualid_of_module : ?loc:Loc.t -> ModPath.t -> qualid +val shortest_qualid_of_universe : ?loc:Loc.t -> universe_id -> qualid (** Deprecated synonyms *) @@ -207,7 +207,7 @@ module type NAMETREE = sig val find : user_name -> t -> elt val exists : user_name -> t -> bool val user_name : qualid -> t -> user_name - val shortest_qualid : Id.Set.t -> user_name -> t -> qualid + val shortest_qualid : ?loc:Loc.t -> Id.Set.t -> user_name -> t -> qualid val find_prefixes : qualid -> t -> elt list end diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 94149a085..1fa26b455 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -202,11 +202,11 @@ GEXTEND Gram | "@"; f=global; i = instance; args=LIST0 NEXT -> CAst.make ~loc:!@loc @@ CAppExpl((None,f,i),args) | "@"; lid = pattern_identref; args=LIST1 identref -> let { CAst.loc = locid; v = id } = lid in - let args = List.map (fun x -> CAst.make @@ CRef (CAst.make ?loc:x.CAst.loc @@ Ident x.CAst.v, None), None) args in + let args = List.map (fun x -> CAst.make @@ CRef (qualid_of_ident ?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"; ".." -> - CAst.make ~loc:!@loc @@ CAppExpl ((None, CAst.make ~loc:!@loc @@ Ident ldots_var, None),[c]) ] + CAst.make ~loc:!@loc @@ CAppExpl ((None, (qualid_of_ident ~loc:!@loc ldots_var), None),[c]) ] | "8" [ ] | "1" LEFTA [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" -> diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4 index 08bcd0f8c..91dce27fe 100644 --- a/parsing/g_prim.ml4 +++ b/parsing/g_prim.ml4 @@ -18,7 +18,7 @@ let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"] let _ = List.iter CLexer.add_keyword prim_kw -let local_make_qualid l id = make_qualid (DirPath.make l) id +let local_make_qualid loc l id = make_qualid ~loc (DirPath.make l) id let my_int_of_string loc s = try @@ -67,8 +67,8 @@ GEXTEND Gram ] ] ; basequalid: - [ [ id = ident; (l,id')=fields -> local_make_qualid (l@[id]) id' - | id = ident -> qualid_of_ident id + [ [ id = ident; (l,id')=fields -> local_make_qualid !@loc (l@[id]) id' + | id = ident -> qualid_of_ident ~loc:!@loc id ] ] ; name: @@ -77,8 +77,8 @@ GEXTEND Gram ; reference: [ [ id = ident; (l,id') = fields -> - CAst.make ~loc:!@loc @@ Qualid (local_make_qualid (l@[id]) id') - | id = ident -> CAst.make ~loc:!@loc @@ Ident id + local_make_qualid !@loc (l@[id]) id' + | id = ident -> local_make_qualid !@loc [] id ] ] ; by_notation: @@ -89,7 +89,7 @@ GEXTEND Gram | ntn = by_notation -> CAst.make ~loc:!@loc @@ Constrexpr.ByNotation ntn ] ] ; qualid: - [ [ qid = basequalid -> CAst.make ~loc:!@loc qid ] ] + [ [ qid = basequalid -> qid ] ] ; ne_string: [ [ s = STRING -> diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 9a45bc973..f959bd80c 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -213,11 +213,11 @@ module Prim : val integer : int Gram.entry val string : string Gram.entry val lstring : lstring Gram.entry - val qualid : qualid CAst.t Gram.entry + val reference : qualid Gram.entry + val qualid : qualid Gram.entry val fullyqualid : Id.t list CAst.t Gram.entry - val reference : reference Gram.entry val by_notation : (string * string option) Gram.entry - val smart_global : reference or_by_notation Gram.entry + val smart_global : qualid or_by_notation Gram.entry val dirpath : DirPath.t Gram.entry val ne_string : string Gram.entry val ne_lstring : lstring Gram.entry @@ -232,7 +232,7 @@ module Constr : val binder_constr : constr_expr Gram.entry val operconstr : constr_expr Gram.entry val ident : Id.t Gram.entry - val global : reference Gram.entry + val global : qualid Gram.entry val universe_level : Glob_term.glob_level Gram.entry val sort : Glob_term.glob_sort Gram.entry val sort_family : Sorts.family Gram.entry diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 1e0589fac..4ede11b5c 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -596,19 +596,18 @@ let warns () = let rec locate_ref = function | [] -> [],[] - | r::l -> - let q = qualid_of_reference r in - let mpo = try Some (Nametab.locate_module q.CAst.v) with Not_found -> None + | qid::l -> + let mpo = try Some (Nametab.locate_module qid) with Not_found -> None and ro = - try Some (Smartlocate.global_with_alias r) + try Some (Smartlocate.global_with_alias qid) with Nametab.GlobalizationError _ | UserError _ -> None in match mpo, ro with - | None, None -> Nametab.error_global_not_found q + | None, None -> Nametab.error_global_not_found qid | None, Some r -> let refs,mps = locate_ref l in r::refs,mps | Some mp, None -> let refs,mps = locate_ref l in refs,mp::mps | Some mp, Some r -> - warning_ambiguous_name (q.CAst.v,mp,r); + warning_ambiguous_name (qid,mp,r); let refs,mps = locate_ref l in refs,mp::mps (*s Recursive extraction in the Coq toplevel. The vernacular command is diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 77f1fb5ef..54fde2ca4 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -13,14 +13,14 @@ open Names open Libnames -val simple_extraction : reference -> unit -val full_extraction : string option -> reference list -> unit -val separate_extraction : reference list -> unit +val simple_extraction : qualid -> unit +val full_extraction : string option -> qualid list -> unit +val separate_extraction : qualid list -> unit val extraction_library : bool -> Id.t -> unit (* For the test-suite : extraction to a temporary file + ocamlc on it *) -val extract_and_compile : reference list -> unit +val extract_and_compile : qualid list -> unit (* For debug / external output via coqtop.byte + Drop : *) diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 5aee70194..3a61c7747 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -1065,11 +1065,15 @@ let extract_constant env kn cb = (match cb.const_body with | Undef _ -> warn_info (); mk_typ_ax () | Def c -> - (match cb.const_proj with + (match Environ.is_projection kn env with | false -> mk_typ (get_body c) | true -> let pb = lookup_projection (Projection.make kn false) env in - mk_typ (EConstr.of_constr pb.proj_body)) + (** FIXME: handle mutual records *) + let ind = (pb.Declarations.proj_ind, 0) in + let bodies = Inductiveops.legacy_match_projection env ind in + let body = bodies.(pb.Declarations.proj_arg) in + mk_typ (EConstr.of_constr body)) | OpaqueDef c -> add_opaque r; if access_opaque () then mk_typ (get_opaque env c) @@ -1078,11 +1082,15 @@ let extract_constant env kn cb = (match cb.const_body with | Undef _ -> warn_info (); mk_ax () | Def c -> - (match cb.const_proj with + (match Environ.is_projection kn env with | false -> mk_def (get_body c) | true -> let pb = lookup_projection (Projection.make kn false) env in - mk_def (EConstr.of_constr pb.proj_body)) + (** FIXME: handle mutual records *) + let ind = (pb.Declarations.proj_ind, 0) in + let bodies = Inductiveops.legacy_match_projection env ind in + let body = bodies.(pb.Declarations.proj_arg) in + mk_def (EConstr.of_constr body)) | OpaqueDef c -> add_opaque r; if access_opaque () then mk_def (get_opaque env c) diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 5bf944434..a8baeaf1b 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -194,17 +194,17 @@ val find_custom_match : ml_branch array -> string (*s Extraction commands. *) val extraction_language : lang -> unit -val extraction_inline : bool -> reference list -> unit +val extraction_inline : bool -> qualid list -> unit val print_extraction_inline : unit -> Pp.t val reset_extraction_inline : unit -> unit val extract_constant_inline : - bool -> reference -> string list -> string -> unit + bool -> qualid -> string list -> string -> unit val extract_inductive : - reference -> string -> string list -> string option -> unit + qualid -> string -> string list -> string option -> unit type int_or_id = ArgInt of int | ArgId of Id.t -val extraction_implicit : reference -> int_or_id list -> unit +val extraction_implicit : qualid -> int_or_id list -> unit (*s Table of blacklisted filenames *) diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 30deb6f49..7e54bc8ad 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -17,7 +17,6 @@ open Goptions open Tacmach.New open Tacticals.New open Tacinterp -open Libnames open Stdarg open Tacarg open Pcoq.Prim @@ -127,7 +126,7 @@ let normalize_evaluables= open Genarg open Ppconstr open Printer -let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_reference +let pr_firstorder_using_raw _ _ _ = Pptactic.pr_auto_using pr_qualid let pr_firstorder_using_glob _ _ _ = Pptactic.pr_auto_using (pr_or_var (fun x -> pr_global (snd x))) let pr_firstorder_using_typed _ _ _ = Pptactic.pr_auto_using pr_global diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index a158fc8ff..31496513a 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -627,7 +627,7 @@ let build_scheme fas = Smartlocate.global_with_alias f with Not_found -> user_err ~hdr:"FunInd.build_scheme" - (str "Cannot find " ++ Libnames.pr_reference f) + (str "Cannot find " ++ Libnames.pr_qualid f) in let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in let _ = evd := evd' in @@ -668,7 +668,7 @@ let build_case_scheme fa = try fst (Global.constr_of_global_in_context (Global.env ()) (Smartlocate.global_with_alias f)) with Not_found -> user_err ~hdr:"FunInd.build_case_scheme" - (str "Cannot find " ++ Libnames.pr_reference f) in + (str "Cannot find " ++ Libnames.pr_qualid f) in let first_fun,u = destConst funs in let funs_mp,funs_dp,_ = Constant.repr3 first_fun in let first_fun_kn = try fst (find_Function_infos first_fun).graph_ind with Not_found -> raise No_graph_found in diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index 33aeafef8..97f9acdb3 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -36,5 +36,5 @@ exception No_graph_found val make_scheme : Evd.evar_map ref -> (pconstant*Sorts.family) list -> Safe_typing.private_constants Entries.definition_entry list -val build_scheme : (Id.t*Libnames.reference*Sorts.family) list -> unit -val build_case_scheme : (Id.t*Libnames.reference*Sorts.family) -> unit +val build_scheme : (Id.t*Libnames.qualid*Sorts.family) list -> unit +val build_case_scheme : (Id.t*Libnames.qualid*Sorts.family) -> unit diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 9899b7b21..a2d31780d 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -168,7 +168,7 @@ END let pr_fun_scheme_arg (princ_name,fun_name,s) = Names.Id.print princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++ - Libnames.pr_reference fun_name ++ spc() ++ str "Sort " ++ + Libnames.pr_qualid fun_name ++ spc() ++ str "Sort " ++ Termops.pr_sort_family s VERNAC ARGUMENT EXTEND fun_scheme_arg @@ -181,11 +181,11 @@ let warning_error names e = let (e, _) = ExplainErr.process_vernac_interp_error (e, Exninfo.null) in match e with | Building_graph e -> - let names = pr_enum Libnames.pr_reference names in + let names = pr_enum Libnames.pr_qualid names in let error = if do_observe () then (spc () ++ CErrors.print e) else mt () in warn_cannot_define_graph (names,error) | Defining_principle e -> - let names = pr_enum Libnames.pr_reference names in + let names = pr_enum Libnames.pr_qualid names in let error = if do_observe () then CErrors.print e else mt () in warn_cannot_define_principle (names,error) | _ -> raise e diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index cd640eebd..489a40ed0 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -362,17 +362,17 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error (*i The next call to mk_rel_id is valid since we have just construct the graph Ensures by : do_built i*) - let f_R_mut = CAst.make @@ Ident (mk_rel_id (List.nth names 0)) in + let f_R_mut = qualid_of_ident @@ mk_rel_id (List.nth names 0) in let ind_kn = fst (locate_with_msg - (pr_reference f_R_mut++str ": Not an inductive type!") + (pr_qualid f_R_mut++str ": Not an inductive type!") locate_ind f_R_mut) in let fname_kn (((fname,_),_,_,_,_),_) = - let f_ref = CAst.map (fun n -> Ident n) fname in - locate_with_msg - (pr_reference f_ref++str ": Not an inductive type!") + let f_ref = qualid_of_ident ?loc:fname.CAst.loc fname.CAst.v in + locate_with_msg + (pr_qualid f_ref++str ": Not an inductive type!") locate_constant f_ref in @@ -477,7 +477,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas let unbounded_eq = let f_app_args = CAst.make @@ Constrexpr.CAppExpl( - (None,CAst.make @@ Ident fname,None) , + (None,qualid_of_ident fname,None) , (List.map (function | {CAst.v=Anonymous} -> assert false @@ -487,7 +487,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas ) ) in - CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (CAst.make @@ Qualid (qualid_of_string "Logic.eq"))), + CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (qualid_of_string "Logic.eq")), [(f_app_args,None);(body,None)]) in let eq = Constrexpr_ops.mkCProdN args unbounded_eq in @@ -544,9 +544,9 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas | None -> let ltof = let make_dir l = DirPath.make (List.rev_map Id.of_string l) in - CAst.make @@ Libnames.Qualid (Libnames.qualid_of_path - (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof"))) - in + Libnames.qualid_of_path + (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (Id.of_string "ltof")) + in let fun_from_mes = let applied_mes = Constrexpr_ops.mkAppC(wf_mes_expr,[Constrexpr_ops.mkIdentC wf_arg]) in @@ -727,12 +727,10 @@ let do_generate_principle pconstants on_error register_built interactive_proof () let rec add_args id new_args = CAst.map (function - | CRef (r,_) as b -> - begin match r with - | {CAst.v=Libnames.Ident fname} when Id.equal fname id -> - CAppExpl((None,r,None),new_args) - | _ -> b - end + | CRef (qid,_) as b -> + if qualid_is_ident qid && Id.equal (qualid_basename qid) id then + CAppExpl((None,qid,None),new_args) + else b | CFix _ | CCoFix _ -> anomaly ~label:"add_args " (Pp.str "todo.") | CProdN(nal,b1) -> CProdN(List.map (function CLocalAssum (nal,k,b2) -> CLocalAssum (nal,k,add_args id new_args b2) @@ -746,13 +744,10 @@ let rec add_args id new_args = CAst.map (function add_args id new_args b1) | CLetIn(na,b1,t,b2) -> CLetIn(na,add_args id new_args b1,Option.map (add_args id new_args) t,add_args id new_args b2) - | CAppExpl((pf,r,us),exprl) -> - begin - match r with - | {CAst.v=Libnames.Ident fname} when Id.equal fname id -> - CAppExpl((pf,r,us),new_args@(List.map (add_args id new_args) exprl)) - | _ -> CAppExpl((pf,r,us),List.map (add_args id new_args) exprl) - end + | CAppExpl((pf,qid,us),exprl) -> + if qualid_is_ident qid && Id.equal (qualid_basename qid) id then + CAppExpl((pf,qid,us),new_args@(List.map (add_args id new_args) exprl)) + else CAppExpl((pf,qid,us),List.map (add_args id new_args) exprl) | CApp((pf,b),bl) -> CApp((pf,add_args id new_args b), List.map (fun (e,o) -> add_args id new_args e,o) bl) @@ -888,7 +883,7 @@ let make_graph (f_ref : GlobRef.t) = | Constrexpr.CLocalAssum (nal,_,_) -> List.map (fun {CAst.loc;v=n} -> CAst.make ?loc @@ - CRef(CAst.make ?loc @@ Libnames.Ident(Nameops.Name.get_id n),None)) + CRef(Libnames.qualid_of_ident ?loc @@ Nameops.Name.get_id n,None)) nal | Constrexpr.CLocalPattern _ -> assert false ) diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index c6faa142a..4eee2c7a4 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -31,9 +31,7 @@ let id_of_name = function Name id -> id | _ -> raise Not_found -let locate ref = - let {CAst.v=qid} = qualid_of_reference ref in - Nametab.locate qid +let locate qid = Nametab.locate qid let locate_ind ref = match locate ref with diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 346b21ef2..7e52ee224 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -20,11 +20,11 @@ val array_get_start : 'a array -> 'a array val id_of_name : Name.t -> Id.t -val locate_ind : Libnames.reference -> inductive -val locate_constant : Libnames.reference -> Constant.t +val locate_ind : Libnames.qualid -> inductive +val locate_constant : Libnames.qualid -> Constant.t val locate_with_msg : - Pp.t -> (Libnames.reference -> 'a) -> - Libnames.reference -> 'a + Pp.t -> (Libnames.qualid -> 'a) -> + Libnames.qualid -> 'a val filter_map : ('a -> bool) -> ('a -> 'b) -> 'a list -> 'b list val list_union_eq : diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index aa49148fc..7298342e1 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1325,7 +1325,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials"); let hook _ _ = let opacity = - let na_ref = CAst.make @@ Libnames.Ident na in + let na_ref = qualid_of_ident na in let na_global = Smartlocate.global_with_alias na_ref in match na_global with ConstRef c -> is_opaque_constant c @@ -1577,7 +1577,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let hook _ _ = let term_ref = Nametab.locate (qualid_of_ident term_id) in let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in - let _ = Extraction_plugin.Table.extraction_inline true [CAst.make @@ Ident term_id] in + let _ = Extraction_plugin.Table.extraction_inline true [qualid_of_ident term_id] in (* message "start second proof"; *) let stop = try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type); diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index f2899ab63..660e29ca8 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -793,17 +793,12 @@ END (* ********************************************************************* *) -let eq_constr x y = - Proofview.Goal.enter begin fun gl -> - let env = Tacmach.New.pf_env gl in - let evd = Tacmach.New.project gl in - match EConstr.eq_constr_universes env evd x y with - | Some _ -> Proofview.tclUNIT () - | None -> Tacticals.New.tclFAIL 0 (str "Not equal") - end - TACTIC EXTEND constr_eq -| [ "constr_eq" constr(x) constr(y) ] -> [ eq_constr x y ] +| [ "constr_eq" constr(x) constr(y) ] -> [ Tactics.constr_eq ~strict:false x y ] +END + +TACTIC EXTEND constr_eq_strict +| [ "constr_eq_strict" constr(x) constr(y) ] -> [ Tactics.constr_eq ~strict:true x y ] END TACTIC EXTEND constr_eq_nounivs diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 642e52155..35ed14fc1 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -173,7 +173,7 @@ TACTIC EXTEND convert_concl_no_check | ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check x DEFAULTcast ] END -let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_reference +let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_qualid let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Printer.pr_global let glob_hints_path_atom ist = Hints.glob_hints_path_atom @@ -189,7 +189,7 @@ ARGUMENT EXTEND hints_path_atom END let pr_hints_path prc prx pry c = Hints.pp_hints_path c -let pr_pre_hints_path prc prx pry c = Hints.pp_hints_path_gen Libnames.pr_reference c +let pr_pre_hints_path prc prx pry c = Hints.pp_hints_path_gen Libnames.pr_qualid c let glob_hints_path ist = Hints.glob_hints_path ARGUMENT EXTEND hints_path diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index d7d642e50..620f14707 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -39,11 +39,12 @@ let genarg_of_ipattern pat = in_gen (rawwit Tacarg.wit_intro_pattern) pat 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 = CAst.map_with_loc (fun ?loc -> function - | Libnames.Ident id -> id - | Libnames.Qualid _ -> - CErrors.user_err ?loc - (str "This expression should be a simple identifier.")) +let reference_to_id qid = + if Libnames.qualid_is_ident qid then + CAst.make ?loc:qid.CAst.loc @@ Libnames.qualid_basename qid + else + CErrors.user_err ?loc:qid.CAst.loc + (str "This expression should be a simple identifier.") let tactic_mode = Gram.entry_create "vernac:tactic_command" @@ -199,8 +200,7 @@ GEXTEND Gram verbose most of the time. *) fresh_id: [ [ s = STRING -> Locus.ArgArg s (*| id = ident -> Locus.ArgVar (!@loc,id)*) - | qid = qualid -> let (_pth,id) = Libnames.repr_qualid qid.CAst.v in - Locus.ArgVar (CAst.make ~loc:!@loc id) ] ] + | qid = qualid -> Locus.ArgVar (CAst.make ~loc:!@loc @@ Libnames.qualid_basename qid) ] ] ; constr_eval: [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr -> @@ -475,7 +475,7 @@ END VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY | [ "Print" "Ltac" reference(r) ] -> - [ Feedback.msg_notice (Tacintern.print_ltac (Libnames.qualid_of_reference r).CAst.v) ] + [ Feedback.msg_notice (Tacintern.print_ltac r) ] END VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY @@ -483,7 +483,7 @@ VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY [ Tacentries.print_located_tactic r ] END -let pr_ltac_ref = Libnames.pr_reference +let pr_ltac_ref = Libnames.pr_qualid let pr_tacdef_body tacdef_body = let id, redef, body = @@ -510,8 +510,7 @@ VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTacticDefinition | [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => [ VtSideff (List.map (function | TacticDefinition ({CAst.v=r},_) -> r - | TacticRedefinition ({CAst.v=Ident r},_) -> r - | TacticRedefinition ({CAst.v=Qualid q},_) -> snd(repr_qualid q)) l), VtLater + | TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater ] -> [ fun ~atts ~st -> let open Vernacinterp in Tacentries.register_ltac (Locality.make_module_locality atts.locality) l; st diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 index 352e92c2a..1f56244c7 100644 --- a/plugins/ltac/g_obligations.ml4 +++ b/plugins/ltac/g_obligations.ml4 @@ -12,7 +12,6 @@ Syntax for the subtac terms and types. Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliâtre *) -open Libnames open Constrexpr open Constrexpr_ops open Stdarg @@ -49,7 +48,7 @@ module Tactic = Pltac open Pcoq -let sigref = mkRefC (CAst.make @@ Qualid (Libnames.qualid_of_string "Coq.Init.Specif.sig")) +let sigref loc = mkRefC (Libnames.qualid_of_string ~loc "Coq.Init.Specif.sig") type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type @@ -68,7 +67,7 @@ GEXTEND Gram Constr.closed_binder: [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> - let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in + let typ = mkAppC (sigref !@loc, [mkLambdaC ([id], default_binder_kind, t, c)]) in [CLocalAssum ([id], default_binder_kind, typ)] ] ]; diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index 2189e224f..f1634f156 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -67,13 +67,13 @@ let subst_strategy s str = str let pr_strategy _ _ _ (s : strategy) = Pp.str "<strategy>" let pr_raw_strategy prc prlc _ (s : raw_strategy) = - let prr = Pptactic.pr_red_expr (prc, prlc, Pputils.pr_or_by_notation Libnames.pr_reference, prc) in + let prr = Pptactic.pr_red_expr (prc, prlc, Pputils.pr_or_by_notation Libnames.pr_qualid, prc) in Rewrite.pr_strategy prc prr s let pr_glob_strategy prc prlc _ (s : glob_strategy) = let prr = Pptactic.pr_red_expr (Ppconstr.pr_constr_expr, Ppconstr.pr_lconstr_expr, - Pputils.pr_or_by_notation Libnames.pr_reference, + Pputils.pr_or_by_notation Libnames.pr_qualid, Ppconstr.pr_constr_expr) in Rewrite.pr_strategy prc prr s diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index 05005c733..31bc34a32 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -156,7 +156,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 -> - TacCase (with_evar,(clear,(CAst.make @@ CRef (CAst.make ?loc:id.CAst.loc @@ Ident id.CAst.v,None),NoBindings))) + TacCase (with_evar,(clear,(CAst.make @@ CRef (qualid_of_ident ?loc:id.CAst.loc id.CAst.v,None),NoBindings))) | ic -> if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic) then diff --git a/plugins/ltac/pltac.mli b/plugins/ltac/pltac.mli index 4c075d413..c5aa542fd 100644 --- a/plugins/ltac/pltac.mli +++ b/plugins/ltac/pltac.mli @@ -21,8 +21,8 @@ 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 : (Names.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 constr_may_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Gram.entry +val constr_eval : (constr_expr,qualid or_by_notation,constr_expr) may_eval Gram.entry val uconstr : constr_expr Gram.entry val quantified_hypothesis : quantified_hypothesis Gram.entry val destruction_arg : constr_expr with_bindings Tactics.destruction_arg Gram.entry diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index e19a95e84..09179dad3 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -17,7 +17,6 @@ open Constrexpr open Genarg open Geninterp open Stdarg -open Libnames open Notation_gram open Tactypes open Locus @@ -1109,8 +1108,8 @@ let pr_goal_selector ~toplevel s = pr_lconstr = pr_lconstr_expr; pr_pattern = pr_constr_pattern_expr; pr_lpattern = pr_lconstr_pattern_expr; - pr_constant = pr_or_by_notation pr_reference; - pr_reference = pr_reference; + pr_constant = pr_or_by_notation pr_qualid; + pr_reference = pr_qualid; pr_name = pr_lident; pr_generic = (fun arg -> Pputils.pr_raw_generic (Global.env ()) arg); pr_extend = pr_raw_extend_rec pr_constr_expr pr_lconstr_expr pr_raw_tactic_level pr_constr_pattern_expr; @@ -1323,7 +1322,7 @@ let () = let open Genprint in register_basic_print0 wit_int_or_var (pr_or_var int) (pr_or_var int) int; register_basic_print0 wit_ref - pr_reference (pr_or_var (pr_located pr_global)) pr_global; + pr_qualid (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_lident pr_lident pr_id; register_print0 @@ -1357,7 +1356,7 @@ let () = ; Genprint.register_print0 wit_red_expr - (lift (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_reference, pr_constr_pattern_expr))) + (lift (pr_red_expr (pr_constr_expr, pr_lconstr_expr, pr_or_by_notation pr_qualid, pr_constr_pattern_expr))) (lift (pr_red_expr (pr_and_constr_expr pr_glob_constr_pptac, pr_and_constr_expr pr_lglob_constr_pptac, pr_or_var (pr_and_short_name pr_evaluable_reference), pr_pat_and_constr_expr pr_glob_constr_pptac))) pr_red_expr_env ; diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index cd04f4ae9..01c52c413 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1773,11 +1773,11 @@ let rec strategy_of_ast = function (* By default the strategy for "rewrite_db" is top-down *) -let mkappc s l = CAst.make @@ CAppExpl ((None,CAst.make @@ Libnames.Ident (Id.of_string s),None),l) +let mkappc s l = CAst.make @@ CAppExpl ((None,qualid_of_ident (Id.of_string s),None),l) let declare_an_instance n s args = (((CAst.make @@ Name n),None), Explicit, - CAst.make @@ CAppExpl ((None, CAst.make @@ Qualid (qualid_of_string s),None), args)) + CAst.make @@ CAppExpl ((None, qualid_of_string s,None), args)) let declare_instance a aeq n s = declare_an_instance n s [a;aeq] @@ -1791,17 +1791,17 @@ let anew_instance global binders instance fields = let declare_instance_refl global binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive" in anew_instance global binders instance - [(CAst.make @@ Ident (Id.of_string "reflexivity"),lemma)] + [(qualid_of_ident (Id.of_string "reflexivity"),lemma)] let declare_instance_sym global binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Symmetric") "Coq.Classes.RelationClasses.Symmetric" in anew_instance global binders instance - [(CAst.make @@ Ident (Id.of_string "symmetry"),lemma)] + [(qualid_of_ident (Id.of_string "symmetry"),lemma)] let declare_instance_trans global binders a aeq n lemma = let instance = declare_instance a aeq (add_suffix n "_Transitive") "Coq.Classes.RelationClasses.Transitive" in anew_instance global binders instance - [(CAst.make @@ Ident (Id.of_string "transitivity"),lemma)] + [(qualid_of_ident (Id.of_string "transitivity"),lemma)] let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans = init_setoid (); @@ -1825,16 +1825,16 @@ let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans = let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PreOrder" in ignore( anew_instance global binders instance - [(CAst.make @@ Ident (Id.of_string "PreOrder_Reflexive"), lemma1); - (CAst.make @@ Ident (Id.of_string "PreOrder_Transitive"),lemma3)]) + [(qualid_of_ident (Id.of_string "PreOrder_Reflexive"), lemma1); + (qualid_of_ident (Id.of_string "PreOrder_Transitive"),lemma3)]) | (None, Some lemma2, Some lemma3) -> let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in let _lemma_trans = declare_instance_trans global binders a aeq n lemma3 in let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.PER" in ignore( anew_instance global binders instance - [(CAst.make @@ Ident (Id.of_string "PER_Symmetric"), lemma2); - (CAst.make @@ Ident (Id.of_string "PER_Transitive"),lemma3)]) + [(qualid_of_ident (Id.of_string "PER_Symmetric"), lemma2); + (qualid_of_ident (Id.of_string "PER_Transitive"),lemma3)]) | (Some lemma1, Some lemma2, Some lemma3) -> let _lemma_refl = declare_instance_refl global binders a aeq n lemma1 in let _lemma_sym = declare_instance_sym global binders a aeq n lemma2 in @@ -1842,9 +1842,9 @@ let declare_relation ?locality ?(binders=[]) a aeq n refl symm trans = let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in ignore( anew_instance global binders instance - [(CAst.make @@ Ident (Id.of_string "Equivalence_Reflexive"), lemma1); - (CAst.make @@ Ident (Id.of_string "Equivalence_Symmetric"), lemma2); - (CAst.make @@ Ident (Id.of_string "Equivalence_Transitive"), lemma3)]) + [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), lemma1); + (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), lemma2); + (qualid_of_ident (Id.of_string "Equivalence_Transitive"), lemma3)]) let cHole = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None) @@ -1949,16 +1949,15 @@ let add_setoid global binders a aeq t n = let instance = declare_instance a aeq n "Coq.Classes.RelationClasses.Equivalence" in ignore( anew_instance global binders instance - [(CAst.make @@ Ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]); - (CAst.make @@ Ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]); - (CAst.make @@ Ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])]) + [(qualid_of_ident (Id.of_string "Equivalence_Reflexive"), mkappc "Seq_refl" [a;aeq;t]); + (qualid_of_ident (Id.of_string "Equivalence_Symmetric"), mkappc "Seq_sym" [a;aeq;t]); + (qualid_of_ident (Id.of_string "Equivalence_Transitive"), mkappc "Seq_trans" [a;aeq;t])]) let make_tactic name = let open Tacexpr in - let tacpath = Libnames.qualid_of_string name in - let tacname = CAst.make @@ Qualid tacpath in - TacArg (Loc.tag @@ (TacCall (Loc.tag (tacname, [])))) + let tacqid = Libnames.qualid_of_string name in + TacArg (Loc.tag @@ (TacCall (Loc.tag (tacqid, [])))) let warn_add_morphism_deprecated = CWarnings.create ~name:"add-morphism" ~category:"deprecated" (fun () -> @@ -2008,7 +2007,7 @@ let add_morphism glob binders m s n = let instance = (((CAst.make @@ Name instance_id),None), Explicit, CAst.make @@ CAppExpl ( - (None, CAst.make @@ Qualid (Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None), + (None, Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper",None), [cHole; s; m])) in let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index fada7424c..98d451536 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -449,12 +449,12 @@ let register_ltac local tacl = in let () = if is_shadowed then warn_unusable_identifier id in NewTac id, body - | Tacexpr.TacticRedefinition (ident, body) -> + | Tacexpr.TacticRedefinition (qid, body) -> let kn = - try Tacenv.locate_tactic (qualid_of_reference ident).CAst.v + try Tacenv.locate_tactic qid with Not_found -> - CErrors.user_err ?loc:ident.CAst.loc - (str "There is no Ltac named " ++ pr_reference ident ++ str ".") + CErrors.user_err ?loc:qid.CAst.loc + (str "There is no Ltac named " ++ pr_qualid qid ++ str ".") in UpdateTac kn, body in diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 3f804ee8d..2bfbbe2e1 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -65,7 +65,7 @@ val create_ltac_quotation : string -> val print_ltacs : unit -> unit (** Display the list of ltac definitions currently available. *) -val print_located_tactic : Libnames.reference -> unit +val print_located_tactic : Libnames.qualid -> unit (** Display the absolute name of a tactic. *) type _ ty_sig = diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index d51de8c65..06d2711ad 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -333,8 +333,8 @@ type glob_tactic_arg = type r_trm = constr_expr type r_pat = constr_pattern_expr -type r_cst = reference or_by_notation -type r_ref = reference +type r_cst = qualid or_by_notation +type r_ref = qualid type r_nam = lident type r_lev = rlevel @@ -399,4 +399,4 @@ type ltac_trace = ltac_call_kind Loc.located list type tacdef_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 *) + | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 01eead164..71e1edfd7 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -333,8 +333,8 @@ type glob_tactic_arg = type r_trm = constr_expr type r_pat = constr_pattern_expr -type r_cst = reference or_by_notation -type r_ref = reference +type r_cst = qualid or_by_notation +type r_ref = qualid type r_nam = lident type r_lev = rlevel @@ -399,4 +399,4 @@ type ltac_trace = ltac_call_kind Loc.located list type tacdef_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 *) + | TacticRedefinition of qualid * raw_tactic_expr (* indicates that user employed '::=' in Ltac body *) diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index cef5bb1b8..481fc30df 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -92,88 +92,83 @@ let intern_or_var f ist = function 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 - | {CAst.loc;v=Ident id} when find_var id ist -> - ArgVar (make ?loc id) - | r -> - let {CAst.loc} as lqid = qualid_of_reference r in - try ArgArg (loc,locate_global_with_alias lqid) - with Not_found -> error_global_not_found lqid - -let intern_ltac_variable ist = function - | {loc;v=Ident id} -> - if find_var id ist then - (* A local variable of any type *) - ArgVar (make ?loc id) - else raise Not_found - | _ -> - raise Not_found - -let intern_constr_reference strict ist = function - | {v=Ident id} as r when not strict && find_hyp id ist -> - (DAst.make @@ GVar id), Some (make @@ CRef (r,None)) - | {v=Ident id} as r when find_var id ist -> - (DAst.make @@ GVar id), if strict then None else Some (make @@ CRef (r,None)) - | r -> - let {loc} as lqid = qualid_of_reference r in - DAst.make @@ GRef (locate_global_with_alias lqid,None), - if strict then None else Some (make @@ CRef (r,None)) +let intern_global_reference ist qid = + if qualid_is_ident qid && find_var (qualid_basename qid) ist then + ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid) + else + try ArgArg (qid.CAst.loc,locate_global_with_alias qid) + with Not_found -> error_global_not_found qid + +let intern_ltac_variable ist qid = + if qualid_is_ident qid && find_var (qualid_basename qid) ist then + (* A local variable of any type *) + ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid) + else raise Not_found + +let intern_constr_reference strict ist qid = + let id = qualid_basename qid in + if qualid_is_ident qid && not strict && find_hyp (qualid_basename qid) ist then + (DAst.make @@ GVar id), Some (make @@ CRef (qid,None)) + else if qualid_is_ident qid && find_var (qualid_basename qid) ist then + (DAst.make @@ GVar id), if strict then None else Some (make @@ CRef (qid,None)) + else + DAst.make @@ GRef (locate_global_with_alias qid,None), + if strict then None else Some (make @@ CRef (qid,None)) (* Internalize an isolated reference in position of tactic *) -let intern_isolated_global_tactic_reference r = - let {loc;v=qid} = qualid_of_reference r in +let intern_isolated_global_tactic_reference qid = + let loc = qid.CAst.loc in TacCall (Loc.tag ?loc (ArgArg (loc,Tacenv.locate_tactic qid),[])) -let intern_isolated_tactic_reference strict ist r = +let intern_isolated_tactic_reference strict ist qid = (* An ltac reference *) - try Reference (intern_ltac_variable ist r) + try Reference (intern_ltac_variable ist qid) with Not_found -> (* A global tactic *) - try intern_isolated_global_tactic_reference r + try intern_isolated_global_tactic_reference qid with Not_found -> (* Tolerance for compatibility, allow not to use "constr:" *) - try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r)) + try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist qid)) with Not_found -> (* Reference not found *) - error_global_not_found (qualid_of_reference r) + error_global_not_found qid (* Internalize an applied tactic reference *) -let intern_applied_global_tactic_reference r = - let {loc;v=qid} = qualid_of_reference r in - ArgArg (loc,Tacenv.locate_tactic qid) +let intern_applied_global_tactic_reference qid = + ArgArg (qid.CAst.loc,Tacenv.locate_tactic qid) -let intern_applied_tactic_reference ist r = +let intern_applied_tactic_reference ist qid = (* An ltac reference *) - try intern_ltac_variable ist r + try intern_ltac_variable ist qid with Not_found -> (* A global tactic *) - try intern_applied_global_tactic_reference r + try intern_applied_global_tactic_reference qid with Not_found -> (* Reference not found *) - error_global_not_found (qualid_of_reference r) + error_global_not_found qid (* Intern a reference parsed in a non-tactic entry *) -let intern_non_tactic_reference strict ist r = +let intern_non_tactic_reference strict ist qid = (* An ltac reference *) - try Reference (intern_ltac_variable ist r) + try Reference (intern_ltac_variable ist qid) with Not_found -> (* A constr reference *) - try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r)) + try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist qid)) with Not_found -> (* Tolerance for compatibility, allow not to use "ltac:" *) - try intern_isolated_global_tactic_reference r + try intern_isolated_global_tactic_reference qid with Not_found -> (* By convention, use IntroIdentifier for unbound ident, when not in a def *) - match r with - | {loc;v=Ident id} when not strict -> - let ipat = in_gen (glbwit wit_intro_pattern) (make ?loc @@ IntroNaming (IntroIdentifier id)) in + if qualid_is_ident qid && not strict then + let id = qualid_basename qid in + let ipat = in_gen (glbwit wit_intro_pattern) (make ?loc:qid.CAst.loc @@ IntroNaming (IntroIdentifier id)) in TacGeneric ipat - | _ -> - (* Reference not found *) - error_global_not_found (qualid_of_reference r) + else + (* Reference not found *) + error_global_not_found qid let intern_message_token ist = function | (MsgString _ | MsgInt _ as x) -> x @@ -269,7 +264,7 @@ let intern_destruction_arg ist = function | clear,ElimOnIdent {loc;v=id} -> if !strict_check then (* If in a defined tactic, no intros-until *) - let c, p = intern_constr ist (make @@ CRef (make @@ Ident id, None)) in + let c, p = intern_constr ist (make @@ CRef (qualid_of_ident id, None)) in match DAst.get c with | GVar id -> clear,ElimOnIdent (make ?loc:c.loc id) | _ -> clear,ElimOnConstr ((c, p), NoBindings) @@ -277,16 +272,15 @@ let intern_destruction_arg ist = function clear,ElimOnIdent (make ?loc id) let short_name = function - | {v=AN {loc;v=Ident id}} when not !strict_check -> Some (make ?loc id) + | {v=AN qid} when qualid_is_ident qid && not !strict_check -> + Some (make ?loc:qid.CAst.loc @@ qualid_basename qid) | _ -> None -let intern_evaluable_global_reference ist r = - let lqid = qualid_of_reference r in - try evaluable_of_global_reference ist.genv (locate_global_with_alias ~head:true lqid) +let intern_evaluable_global_reference ist qid = + try evaluable_of_global_reference ist.genv (locate_global_with_alias ~head:true qid) with Not_found -> - match r with - | {loc;v=Ident id} when not !strict_check -> EvalVarRef id - | _ -> error_global_not_found lqid + if qualid_is_ident qid && not !strict_check then EvalVarRef (qualid_basename qid) + else error_global_not_found qid let intern_evaluable_reference_or_by_notation ist = function | {v=AN r} -> intern_evaluable_global_reference ist r @@ -296,14 +290,19 @@ let intern_evaluable_reference_or_by_notation ist = function (function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc) (* Globalize a reduction expression *) -let intern_evaluable ist = function - | {loc;v=AN {v=Ident id}} when find_var id ist -> ArgVar (make ?loc id) - | {loc;v=AN {v=Ident id}} when not !strict_check && find_hyp id ist -> - ArgArg (EvalVarRef id, Some (make ?loc id)) - | r -> - let e = intern_evaluable_reference_or_by_notation ist r in - let na = short_name r in - ArgArg (e,na) +let intern_evaluable ist r = + let f ist r = + let e = intern_evaluable_reference_or_by_notation ist r in + let na = short_name r in + ArgArg (e,na) + in + match r with + | {v=AN qid} when qualid_is_ident qid && find_var (qualid_basename qid) ist -> + ArgVar (make ?loc:qid.CAst.loc @@ qualid_basename qid) + | {v=AN qid} when qualid_is_ident qid && not !strict_check && find_hyp (qualid_basename qid) ist -> + let id = qualid_basename qid in + ArgArg (EvalVarRef id, Some (make ?loc:qid.CAst.loc id)) + | _ -> f ist r let intern_unfold ist (l,qid) = (l,intern_evaluable ist qid) @@ -356,7 +355,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) = subterm matched when a pattern *) let r = match r with | {v=AN r} -> r - | {loc} -> make ?loc @@ Qualid (qualid_of_path (path_of_global (smart_global r))) in + | {loc} -> (qualid_of_path ?loc (path_of_global (smart_global r))) in let sign = { Constrintern.ltac_vars = ist.ltacvars; ltac_bound = Id.Set.empty; diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 04dd7d6e9..9d1cc1643 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -361,7 +361,7 @@ let interp_reference ist env sigma = function with Not_found -> try VarRef (get_id (Environ.lookup_named id env)) - with Not_found -> error_global_not_found (make ?loc @@ qualid_of_ident id) + with Not_found -> error_global_not_found (qualid_of_ident ?loc id) let try_interp_evaluable env (loc, id) = let v = Environ.lookup_named id env in @@ -377,14 +377,14 @@ let interp_evaluable ist env sigma = function with Not_found -> match r with | EvalConstRef _ -> r - | _ -> error_global_not_found (make ?loc @@ qualid_of_ident id) + | _ -> error_global_not_found (qualid_of_ident ?loc id) end | ArgArg (r,None) -> r | 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 (make ?loc @@ qualid_of_ident id) + with Not_found -> error_global_not_found (qualid_of_ident ?loc id) (* Interprets an hypothesis name *) let interp_occurrences ist occs = @@ -643,7 +643,7 @@ let interp_closed_typed_pattern_with_occurrences ist env sigma (occs, a) = 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)) (make ?loc id) with Not_found -> - error_global_not_found (make ?loc @@ qualid_of_ident id)) + error_global_not_found (qualid_of_ident ?loc id)) | Inl (ArgArg _ as b) -> Inl (interp_evaluable ist env sigma b) | Inr c -> Inr (interp_typed_pattern ist env sigma c) in interp_occurrences ist occs, p @@ -925,7 +925,7 @@ let interp_destruction_arg ist gl arg = if Tactics.is_quantified_hypothesis id gl then keep,ElimOnIdent (make ?loc id) else - let c = (DAst.make ?loc @@ GVar id,Some (make @@ CRef (make ?loc @@ Ident id,None))) in + let c = (DAst.make ?loc @@ GVar id,Some (make @@ CRef (qualid_of_ident ?loc id,None))) in let f env sigma = let (sigma,c) = interp_open_constr ist env sigma c in (sigma, (c,NoBindings)) diff --git a/plugins/setoid_ring/g_newring.ml4 b/plugins/setoid_ring/g_newring.ml4 index 5e4c9214a..e9ce306e8 100644 --- a/plugins/setoid_ring/g_newring.ml4 +++ b/plugins/setoid_ring/g_newring.ml4 @@ -42,11 +42,11 @@ let pr_ring_mod = function | Ring_kind Abstract -> str "abstract" | Ring_kind (Morphism morph) -> str "morphism" ++ pr_arg pr_constr_expr morph | Const_tac (CstTac cst_tac) -> str "constants" ++ spc () ++ str "[" ++ pr_raw_tactic cst_tac ++ str "]" - | Const_tac (Closed l) -> str "closed" ++ spc () ++ str "[" ++ prlist_with_sep spc pr_reference l ++ str "]" + | Const_tac (Closed l) -> str "closed" ++ spc () ++ str "[" ++ prlist_with_sep spc pr_qualid l ++ str "]" | Pre_tac t -> str "preprocess" ++ spc () ++ str "[" ++ pr_raw_tactic t ++ str "]" | Post_tac t -> str "postprocess" ++ spc () ++ str "[" ++ pr_raw_tactic t ++ str "]" | Setoid(sth,ext) -> str "setoid" ++ pr_arg pr_constr_expr sth ++ pr_arg pr_constr_expr ext - | Pow_spec(Closed l,spec) -> str "power_tac" ++ pr_arg pr_constr_expr spec ++ spc () ++ str "[" ++ prlist_with_sep spc pr_reference l ++ str "]" + | Pow_spec(Closed l,spec) -> str "power_tac" ++ pr_arg pr_constr_expr spec ++ spc () ++ str "[" ++ prlist_with_sep spc pr_qualid l ++ str "]" | Pow_spec(CstTac cst_tac,spec) -> str "power_tac" ++ pr_arg pr_constr_expr spec ++ spc () ++ str "[" ++ pr_raw_tactic cst_tac ++ str "]" | Sign_spec t -> str "sign" ++ pr_arg pr_constr_expr t | Div_spec t -> str "div" ++ pr_arg pr_constr_expr t diff --git a/plugins/setoid_ring/newring_ast.ml b/plugins/setoid_ring/newring_ast.ml index 3eb68b518..a83c79d11 100644 --- a/plugins/setoid_ring/newring_ast.ml +++ b/plugins/setoid_ring/newring_ast.ml @@ -22,7 +22,7 @@ type 'constr coeff_spec = type cst_tac_spec = CstTac of raw_tactic_expr - | Closed of reference list + | Closed of qualid list type 'constr ring_mod = Ring_kind of 'constr coeff_spec diff --git a/plugins/setoid_ring/newring_ast.mli b/plugins/setoid_ring/newring_ast.mli index 3eb68b518..a83c79d11 100644 --- a/plugins/setoid_ring/newring_ast.mli +++ b/plugins/setoid_ring/newring_ast.mli @@ -22,7 +22,7 @@ type 'constr coeff_spec = type cst_tac_spec = CstTac of raw_tactic_expr - | Closed of reference list + | Closed of qualid list type 'constr ring_mod = Ring_kind of 'constr coeff_spec diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 2a31157be..54f3f9c71 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -858,7 +858,7 @@ open Util (** Constructors for constr_expr *) let mkCProp loc = CAst.make ?loc @@ CSort GProp let mkCType loc = CAst.make ?loc @@ CSort (GType []) -let mkCVar ?loc id = CAst.make ?loc @@ CRef (CAst.make ?loc @@ Ident id, None) +let mkCVar ?loc id = CAst.make ?loc @@ CRef (qualid_of_ident ?loc id, None) let rec mkCHoles ?loc n = if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None)) :: mkCHoles ?loc (n - 1) let mkCHole loc = CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None) diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 2c046190f..7fe2421f9 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -47,6 +47,7 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) gl = let cl = EConstr.Unsafe.to_constr cl in try fill_occ_pattern ~raise_NoMatch:true env sigma cl pat occ 1 with NoMatch -> redex_of_pattern ~resolve_typeclasses:true env pat, cl in + let gl = pf_merge_uc ucst gl in let c = EConstr.of_constr c in let cl = EConstr.of_constr cl in if Termops.occur_existential sigma c then errorstrm(str"The pattern"++spc()++ @@ -56,7 +57,6 @@ let ssrsettac id ((_, (pat, pty)), (_, occ)) gl = | Cast(t, DEFAULTcast, ty) -> t, (gl, ty) | _ -> c, pfe_type_of gl c in let cl' = EConstr.mkLetIn (Name id, c, cty, cl) in - let gl = pf_merge_uc ucst gl in Tacticals.tclTHEN (Proofview.V82.of_tactic (convert_concl cl')) (introid id) gl open Util diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 352f88bb3..7a1d06fdc 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -1154,7 +1154,8 @@ ARGUMENT EXTEND ssrbvar TYPED AS constr PRINTED BY pr_ssrbvar END let bvar_lname = let open CAst in function - | { v = CRef ({loc;v=Ident id}, _) } -> CAst.make ?loc @@ Name id + | { v = CRef (qid, _) } when qualid_is_ident qid -> + CAst.make ?loc:qid.CAst.loc @@ Name (qualid_basename qid) | { loc = loc } -> CAst.make ?loc Anonymous let pr_ssrbinder prc _ _ (_, c) = prc c @@ -1246,7 +1247,8 @@ END let pr_ssrfixfwd _ _ _ (id, fwd) = str " fix " ++ pr_id id ++ pr_fwd fwd let bvar_locid = function - | { CAst.v = CRef ({CAst.loc=loc;v=Ident id}, _) } -> CAst.make ?loc id + | { CAst.v = CRef (qid, _) } when qualid_is_ident qid -> + CAst.make ?loc:qid.CAst.loc (qualid_basename qid) | _ -> CErrors.user_err (Pp.str "Missing identifier after \"(co)fix\"") diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 939e97866..7ce2dd64a 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -28,7 +28,6 @@ open Globnames open Stdarg open Genarg open Decl_kinds -open Libnames open Pp open Ppconstr open Printer @@ -143,21 +142,21 @@ END let declare_one_prenex_implicit locality f = let fref = try Smartlocate.global_with_alias f - with _ -> errorstrm (pr_reference f ++ str " is not declared") in + with _ -> errorstrm (pr_qualid f ++ str " is not declared") in let rec loop = function | a :: args' when Impargs.is_status_implicit a -> (ExplByName (Impargs.name_of_implicit a), (true, true, true)) :: loop args' | args' when List.exists Impargs.is_status_implicit args' -> - errorstrm (str "Expected prenex implicits for " ++ pr_reference f) + errorstrm (str "Expected prenex implicits for " ++ pr_qualid f) | _ -> [] in let impls = match Impargs.implicits_of_global fref with | [cond,impls] -> impls - | [] -> errorstrm (str "Expected some implicits for " ++ pr_reference f) + | [] -> errorstrm (str "Expected some implicits for " ++ pr_qualid f) | _ -> errorstrm (str "Multiple implicits not supported") in match loop impls with | [] -> - errorstrm (str "Expected some implicits for " ++ pr_reference f) + errorstrm (str "Expected some implicits for " ++ pr_qualid f) | impls -> Impargs.declare_manual_implicits locality fref ~enriching:false [impls] @@ -415,7 +414,7 @@ let interp_search_arg arg = (* Module path postfilter *) -let pr_modloc (b, m) = if b then str "-" ++ pr_reference m else pr_reference m +let pr_modloc (b, m) = if b then str "-" ++ pr_qualid m else pr_qualid m let wit_ssrmodloc = add_genarg "ssrmodloc" pr_modloc @@ -433,10 +432,9 @@ GEXTEND Gram END let interp_modloc mr = - let interp_mod (_, mr) = - let {CAst.loc=loc; v=qid} = qualid_of_reference mr in + let interp_mod (_, qid) = try Nametab.full_name_module qid with Not_found -> - CErrors.user_err ?loc (str "No Module " ++ pr_qualid qid) in + CErrors.user_err ?loc:qid.CAst.loc (str "No Module " ++ pr_qualid qid) in let mr_out, mr_in = List.partition fst mr in let interp_bmod b = function | [] -> fun _ _ _ -> true diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 69d944fa1..9d9b1b2e8 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -131,9 +131,12 @@ let add_genarg tag pr = (** Constructors for cast type *) let dC t = CastConv t (** Constructors for constr_expr *) -let isCVar = function { CAst.v = CRef ({CAst.v=Ident _},_) } -> true | _ -> false -let destCVar = function { CAst.v = CRef ({CAst.v=Ident id},_) } -> id | _ -> - CErrors.anomaly (str"not a CRef.") +let isCVar = function { CAst.v = CRef (qid,_) } -> qualid_is_ident qid | _ -> false +let destCVar = function + | { CAst.v = CRef (qid,_) } when qualid_is_ident qid -> + qualid_basename qid + | _ -> + CErrors.anomaly (str"not a CRef.") let isGLambda c = match DAst.get c with GLambda (Name _, _, _, _) -> true | _ -> false let destGLambda c = match DAst.get c with GLambda (Name id, _, _, c) -> (id, c) | _ -> CErrors.anomaly (str "not a GLambda") @@ -558,8 +561,8 @@ let filter_upat i0 f n u fpats = let na = Array.length u.up_a in if n < na then fpats else let np = match u.up_k with - | KpatConst when equal u.up_f f -> na - | KpatFixed when equal u.up_f f -> na + | KpatConst when eq_constr_nounivs u.up_f f -> na + | KpatFixed when eq_constr_nounivs u.up_f f -> na | KpatEvar k when isEvar_k k f -> na | KpatLet when isLetIn f -> na | KpatLam when isLambda f -> na @@ -579,8 +582,8 @@ let filter_upat_FO i0 f n u fpats = let np = nb_args u.up_FO in if n < np then fpats else let ok = match u.up_k with - | KpatConst -> equal u.up_f f - | KpatFixed -> equal u.up_f f + | KpatConst -> eq_constr_nounivs u.up_f f + | KpatFixed -> eq_constr_nounivs u.up_f f | KpatEvar k -> isEvar_k k f | KpatLet -> isLetIn f | KpatLam -> isLambda f @@ -761,8 +764,8 @@ let mk_tpattern_matcher ?(all_instances=false) let match_let f = match kind f with | LetIn (_, v, _, b) -> unif_EQ env sigma pv v && unif_EQ env' sigma pb b | _ -> false in match_let - | KpatFixed -> equal u.up_f - | KpatConst -> equal u.up_f + | KpatFixed -> eq_constr_nounivs u.up_f + | KpatConst -> eq_constr_nounivs u.up_f | KpatLam -> fun c -> (match kind c with | Lambda _ -> unif_EQ env sigma u.up_f c @@ -1019,8 +1022,10 @@ type pattern = Evd.evar_map * (constr, constr) ssrpattern let id_of_cpattern (_, (c1, c2), _) = let open CAst in match DAst.get c1, c2 with - | _, Some { v = CRef ({CAst.v=Ident x}, _) } -> Some x - | _, Some { v = CAppExpl ((_, {CAst.v=Ident x}, _), []) } -> Some x + | _, Some { v = CRef (qid, _) } when qualid_is_ident qid -> + Some (qualid_basename qid) + | _, Some { v = CAppExpl ((_, qid, _), []) } when qualid_is_ident qid -> + Some (qualid_basename qid) | GRef (VarRef x, _), None -> Some x | _ -> None let id_of_Cterm t = match id_of_cpattern t with diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 0dd3c5944..93ca9dc5e 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1425,7 +1425,7 @@ and match_current pb (initial,tomatch) = let ci = make_case_info pb.env (fst mind) pb.casestyle in let pred = nf_betaiota pb.env !(pb.evdref) pred in let case = - make_case_or_project pb.env !(pb.evdref) indf ci pred current brvals + make_case_or_project pb.env !(pb.evdref) indf ci pred current brvals in let _ = Evarutil.evd_comb1 (Typing.type_of pb.env) pb.evdref pred in Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred; diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index df89d9eac..fe49d64c7 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -87,7 +87,7 @@ let encode_tuple ({CAst.loc} as r) = module PrintingInductiveMake = functor (Test : sig - val encode : reference -> inductive + val encode : qualid -> inductive val member_message : Pp.t -> bool -> Pp.t val field : string val title : string @@ -690,7 +690,10 @@ and detype_r d flags avoid env sigma t = let c' = try let pb = Environ.lookup_projection p (snd env) in - let body = pb.Declarations.proj_body in + (** FIXME: handle mutual records *) + let ind = (pb.Declarations.proj_ind, 0) in + let bodies = Inductiveops.legacy_match_projection (snd env) ind in + let body = bodies.(pb.Declarations.proj_arg) in let ty = Retyping.get_type_of (snd env) sigma c in let ((ind,u), args) = Inductiveops.find_mrectype (snd env) sigma ty in let body' = strip_lam_assum body in diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 5310455fe..8695d52b1 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -87,7 +87,7 @@ val subst_genarg_hook : module PrintingInductiveMake : functor (Test : sig - val encode : Libnames.reference -> Names.inductive + val encode : Libnames.qualid -> Names.inductive val member_message : Pp.t -> bool -> Pp.t val field : string val title : string @@ -95,7 +95,7 @@ module PrintingInductiveMake : sig type t = Names.inductive val compare : t -> t -> int - val encode : Libnames.reference -> Names.inductive + val encode : Libnames.qualid -> Names.inductive val subst : substitution -> t -> t val printer : t -> Pp.t val key : Goptions.option_name diff --git a/pretyping/geninterp.mli b/pretyping/geninterp.mli index fa522e9c3..606a6ebea 100644 --- a/pretyping/geninterp.mli +++ b/pretyping/geninterp.mli @@ -42,8 +42,8 @@ sig end -module ValTMap (M : Dyn.TParam) : - Dyn.MapS with type 'a obj = 'a M.t with type 'a key = 'a Val.typ +module ValTMap (Value : Dyn.ValueS) : + Dyn.MapS with type 'a key = 'a Val.typ and type 'a value = 'a Value.t (** Dynamic types for toplevel values. While the generic types permit to relate objects at various levels of interpretation, toplevel values are wearing diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 8ecec30cf..ba193da60 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -51,7 +51,7 @@ let glob_sort_eq g1 g2 = let open Glob_term in match g1, g2 with | GProp, GProp -> true | GSet, GSet -> true | GType l1, GType l2 -> - List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.eq_reference x y && Int.equal m n)) l1 l2 + List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.qualid_eq x y && Int.equal m n)) l1 l2 | _ -> false let binding_kind_eq bk1 bk2 = match bk1, bk2 with @@ -414,8 +414,10 @@ let loc_of_glob_constr c = c.CAst.loc (**********************************************************************) (* Alpha-renaming *) +exception UnsoundRenaming + let collide_id l id = List.exists (fun (id',id'') -> Id.equal id id' || Id.equal id id'') l -let test_id l id = if collide_id l id then raise Not_found +let test_id l id = if collide_id l id then raise UnsoundRenaming let test_na l na = Name.iter (test_id l) na let update_subst na l = @@ -429,8 +431,6 @@ let update_subst na l = else na,l) na (na,l) -exception UnsoundRenaming - let rename_var l id = try let id' = Id.List.assoc id l in diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 54fa5328f..86245d479 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -33,11 +33,11 @@ type 'a universe_kind = | UUnknown | UNamed of 'a -type level_info = Libnames.reference universe_kind +type level_info = Libnames.qualid universe_kind type glob_level = level_info glob_sort_gen type glob_constraint = glob_level * Univ.constraint_type * glob_level -type sort_info = (Libnames.reference * int) option list +type sort_info = (Libnames.qualid * int) option list type glob_sort = sort_info glob_sort_gen (** Casts *) diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 27b029aad..4ab932723 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -304,7 +304,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs = process_constr env 0 f (List.rev cstr.cs_args, recargs) (* Main function *) -let mis_make_indrec env sigma listdepkind mib u = +let mis_make_indrec env sigma ?(force_mutual=false) listdepkind mib u = let nparams = mib.mind_nparams in let nparrec = mib.mind_nparams_rec in let evdref = ref sigma in @@ -469,7 +469,7 @@ let mis_make_indrec env sigma listdepkind mib u = (* Body on make_one_rec *) let ((indi,u),mibi,mipi,dep,kind) = List.nth listdepkind p in - if (mis_is_recursive_subset + if force_mutual || (mis_is_recursive_subset (List.map (fun ((indi,u),_,_,_,_) -> snd indi) listdepkind) mipi.mind_recargs) then @@ -558,7 +558,7 @@ let check_arities env listdepkind = [] listdepkind in true -let build_mutual_induction_scheme env sigma = function +let build_mutual_induction_scheme env sigma ?(force_mutual=false) = function | ((mind,u),dep,s)::lrecspec -> let (mib,mip) = lookup_mind_specif env mind in if dep && not (Inductiveops.has_dependent_elim mib) then @@ -577,7 +577,7 @@ let build_mutual_induction_scheme env sigma = function lrecspec) in let _ = check_arities env listdepkind in - mis_make_indrec env sigma listdepkind mib u + mis_make_indrec env sigma ~force_mutual listdepkind mib u | _ -> anomaly (Pp.str "build_induction_scheme expects a non empty list of inductive types.") let build_induction_scheme env sigma pind dep kind = diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index d87a19d28..de9d3a0ab 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -47,7 +47,8 @@ val build_induction_scheme : env -> evar_map -> pinductive -> (** Builds mutual (recursive) induction schemes *) val build_mutual_induction_scheme : - env -> evar_map -> (pinductive * dep_flag * Sorts.family) list -> evar_map * constr list + env -> evar_map -> ?force_mutual:bool -> + (pinductive * dep_flag * Sorts.family) list -> evar_map * constr list (** Scheme combinators *) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index b1ab2d2b7..1003f86c5 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -356,8 +356,8 @@ let make_case_or_project env sigma indf ci pred c branches = | None -> (mkCase (ci, pred, c, branches)) | Some ps -> assert(Array.length branches == 1); + let na, ty, t = destLambda sigma pred in let () = - let _, _, t = destLambda sigma pred in let (ind, _), _ = dest_ind_family indf in let mib, _ = Inductive.lookup_mind_specif env ind in if (* dependent *) not (Vars.noccurn sigma 1 t) && @@ -368,16 +368,18 @@ let make_case_or_project env sigma indf ci pred c branches = in let branch = branches.(0) in let ctx, br = decompose_lam_n_assum sigma (Array.length ps) branch in - let n, subst = + let n, len, ctx = List.fold_right - (fun decl (i, subst) -> + (fun decl (i, j, ctx) -> match decl with - | LocalAssum (na, t) -> - let t = mkProj (Projection.make ps.(i) true, c) in - (i + 1, t :: subst) - | LocalDef (na, b, t) -> (i, Vars.substl subst b :: subst)) - ctx (0, []) - in Vars.substl subst br + | LocalAssum (na, ty) -> + let t = mkProj (Projection.make ps.(i) true, mkRel j) in + (i + 1, j + 1, LocalDef (na, t, Vars.liftn 1 j ty) :: ctx) + | LocalDef (na, b, ty) -> + (i, j + 1, LocalDef (na, Vars.liftn 1 j b, Vars.liftn 1 j ty) :: ctx)) + ctx (0, 1, []) + in + mkLetIn (na, c, ty, it_mkLambda_or_LetIn (Vars.liftn 1 (Array.length ps + 1) br) ctx) (* substitution in a signature *) @@ -454,6 +456,110 @@ let build_branch_type env sigma dep p cs = (**************************************************) +(** From a rel context describing the constructor arguments, + build an expansion function. + The term built is expecting to be substituted first by + a substitution of the form [params, x : ind params] *) +let compute_projections env (kn, _ as ind) = + let open Term in + let mib = Environ.lookup_mind kn env in + let indu = match mib.mind_universes with + | Monomorphic_ind _ -> mkInd ind + | Polymorphic_ind ctx -> mkIndU (ind, make_abstract_instance ctx) + | Cumulative_ind ctx -> + mkIndU (ind, make_abstract_instance (ACumulativityInfo.univ_context ctx)) + in + let x = match mib.mind_record with + | None | Some None -> + anomaly Pp.(str "Trying to build primitive projections for a non-primitive record") + | Some (Some (id, _, _)) -> Name id + in + (** FIXME: handle mutual records *) + let pkt = mib.mind_packets.(0) in + let { mind_consnrealargs; mind_consnrealdecls } = pkt in + let { mind_nparams = nparamargs; mind_params_ctxt = params } = mib in + let rctx, _ = decompose_prod_assum (subst1 indu pkt.mind_nf_lc.(0)) in + let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in + let mp, dp, l = MutInd.repr3 kn in + (** We build a substitution smashing the lets in the record parameters so + that typechecking projections requires just a substitution and not + matching with a parameter context. *) + let indty = + (* [ty] = [Ind inst] is typed in context [params] *) + let inst = Context.Rel.to_extended_vect mkRel 0 paramslet in + let ty = mkApp (indu, inst) in + (* [Ind inst] is typed in context [params-wo-let] *) + ty + in + let ci = + let print_info = + { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in + { ci_ind = ind; + ci_npar = nparamargs; + ci_cstr_ndecls = mind_consnrealdecls; + ci_cstr_nargs = mind_consnrealargs; + ci_pp_info = print_info } + in + let len = List.length ctx in + let compat_body ccl i = + (* [ccl] is defined in context [params;x:indty] *) + (* [ccl'] is defined in context [params;x:indty;x:indty] *) + let ccl' = liftn 1 2 ccl in + let p = mkLambda (x, lift 1 indty, ccl') in + let branch = it_mkLambda_or_LetIn (mkRel (len - i)) ctx in + let body = mkCase (ci, p, mkRel 1, [|lift 1 branch|]) in + it_mkLambda_or_LetIn (mkLambda (x,indty,body)) params + in + let projections decl (j, pbs, subst) = + match decl with + | LocalDef (na,c,t) -> + (* From [params, field1,..,fieldj |- c(params,field1,..,fieldj)] + to [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] *) + let c = liftn 1 j c in + (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] + to [params, x:I |- c(params,proj1 x,..,projj x)] *) + let c1 = substl subst c in + (* From [params, x:I |- subst:field1,..,fieldj] + to [params, x:I |- subst:field1,..,fieldj+1] where [subst] + is represented with instance of field1 last *) + let subst = c1 :: subst in + (j+1, pbs, subst) + | LocalAssum (na,t) -> + match na with + | Name id -> + let kn = Constant.make1 (KerName.make mp dp (Label.of_id id)) in + (* from [params, field1,..,fieldj |- t(params,field1,..,fieldj)] + to [params, x:I, field1,..,fieldj |- t(params,field1,..,fieldj] *) + let t = liftn 1 j t in + (* from [params, x:I, field1,..,fieldj |- t(params,field1,..,fieldj)] + to [params-wo-let, x:I |- t(params,proj1 x,..,projj x)] *) + (* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)] + to [params, x:I |- t(proj1 x,..,projj x)] *) + let ty = substl subst t in + let term = mkProj (Projection.make kn true, mkRel 1) in + let fterm = mkProj (Projection.make kn false, mkRel 1) in + let compat = compat_body ty (j - 1) in + let etab = it_mkLambda_or_LetIn (mkLambda (x, indty, term)) params in + let etat = it_mkProd_or_LetIn (mkProd (x, indty, ty)) params in + let body = (etab, etat, compat) in + (j + 1, body :: pbs, fterm :: subst) + | Anonymous -> + anomaly Pp.(str "Trying to build primitive projections for a non-primitive record") + in + let (_, pbs, subst) = + List.fold_right projections ctx (1, [], []) + in + Array.rev_of_list pbs + +let legacy_match_projection env ind = + Array.map pi3 (compute_projections env ind) + +let compute_projections ind mib = + let ans = compute_projections ind mib in + Array.map (fun (prj, ty, _) -> (prj, ty)) ans + +(**************************************************) + let extract_mrectype sigma t = let open EConstr in let (t, l) = decompose_app sigma t in diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index b0d714b03..aa53f7e67 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -194,6 +194,18 @@ val make_case_or_project : val make_default_case_info : env -> case_style -> inductive -> case_info i*) +val compute_projections : Environ.env -> inductive -> (constr * types) array +(** Given a primitive record type, for every field computes the eta-expanded + projection and its type. *) + +val legacy_match_projection : Environ.env -> inductive -> constr array +(** Given a record type, computes the legacy match-based projection of the + projections. + + BEWARE: such terms are ill-typed, and should thus only be used in upper + layers. The kernel will probably badly fail if presented with one of + those. *) + (********************) val type_of_inductive_knowing_conclusion : diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 9e024b1c2..57c4d363b 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -171,38 +171,37 @@ let _ = (** Miscellaneous interpretation functions *) -let interp_known_universe_level evd r = - let qid = Libnames.qualid_of_reference r in +let interp_known_universe_level evd qid = try - match r.CAst.v with - | Libnames.Ident id -> Evd.universe_of_name evd id - | Libnames.Qualid _ -> raise Not_found + let open Libnames in + if qualid_is_ident qid then Evd.universe_of_name evd @@ qualid_basename qid + else raise Not_found with Not_found -> - let univ, k = Nametab.locate_universe qid.CAst.v in + let univ, k = Nametab.locate_universe qid in Univ.Level.make univ k -let interp_universe_level_name ~anon_rigidity evd r = - try evd, interp_known_universe_level evd r +let interp_universe_level_name ~anon_rigidity evd qid = + try evd, interp_known_universe_level evd qid with Not_found -> - match r with (* Qualified generated name *) - | {CAst.loc; v=Libnames.Qualid qid} -> - let dp, i = Libnames.repr_qualid qid in - let num = - try int_of_string (Id.to_string i) - with Failure _ -> - user_err ?loc ~hdr:"interp_universe_level_name" - (Pp.(str "Undeclared global universe: " ++ Libnames.pr_reference r)) - in - let level = Univ.Level.make dp num in - let evd = - try Evd.add_global_univ evd level - with UGraph.AlreadyDeclared -> evd - in evd, level - | {CAst.loc; v=Libnames.Ident id} -> (* Undeclared *) - if not (is_strict_universe_declarations ()) then - new_univ_level_variable ?loc ~name:id univ_rigid evd - else user_err ?loc ~hdr:"interp_universe_level_name" - (Pp.(str "Undeclared universe: " ++ Id.print id)) + if Libnames.qualid_is_ident qid then (* Undeclared *) + let id = Libnames.qualid_basename qid in + if not (is_strict_universe_declarations ()) then + new_univ_level_variable ?loc:qid.CAst.loc ~name:id univ_rigid evd + else user_err ?loc:qid.CAst.loc ~hdr:"interp_universe_level_name" + (Pp.(str "Undeclared universe: " ++ Id.print id)) + else + let dp, i = Libnames.repr_qualid qid in + let num = + try int_of_string (Id.to_string i) + with Failure _ -> + user_err ?loc:qid.CAst.loc ~hdr:"interp_universe_level_name" + (Pp.(str "Undeclared global universe: " ++ Libnames.pr_qualid qid)) + in + let level = Univ.Level.make dp num in + let evd = + try Evd.add_global_univ evd level + with UGraph.AlreadyDeclared -> evd + in evd, level let interp_universe ?loc evd = function | [] -> let evd, l = new_univ_level_variable ?loc univ_rigid evd in @@ -232,10 +231,10 @@ let interp_known_level_info ?loc evd = function | UUnknown | UAnonymous -> user_err ?loc ~hdr:"interp_known_level_info" (str "Anonymous universes not allowed here.") - | UNamed ref -> - try interp_known_universe_level evd ref + | UNamed qid -> + try interp_known_universe_level evd qid with Not_found -> - user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_reference ref) + user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_qualid qid) let interp_level_info ?loc evd : level_info -> _ = function | UUnknown -> new_univ_level_variable ?loc univ_rigid evd diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 605781993..e38da45b9 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -159,7 +159,7 @@ let tag_var = tag Tag.variable let pr_univ_expr = function | Some (x,n) -> - pr_reference x ++ (match n with 0 -> mt () | _ -> str"+" ++ int n) + pr_qualid x ++ (match n with 0 -> mt () | _ -> str"+" ++ int n) | None -> str"_" let pr_univ l = @@ -180,7 +180,7 @@ let tag_var = tag Tag.variable | GSet -> tag_type (str "Set") | GType UUnknown -> tag_type (str "Type") | GType UAnonymous -> tag_type (str "_") - | GType (UNamed u) -> tag_type (pr_reference u) + | GType (UNamed u) -> tag_type (pr_qualid u) let pr_qualid sp = let (sl, id) = repr_qualid sp in @@ -205,16 +205,16 @@ let tag_var = tag Tag.variable tag_type (str "Set") | GType u -> (match u with - | UNamed u -> pr_reference u + | UNamed u -> pr_qualid u | UAnonymous -> tag_type (str "Type") | UUnknown -> tag_type (str "_")) let pr_universe_instance l = pr_opt_no_spc (pr_univ_annot (prlist_with_sep spc pr_glob_sort_instance)) l - let pr_reference = CAst.with_val (function - | Qualid qid -> pr_qualid qid - | Ident id -> tag_var (pr_id id)) + let pr_reference qid = + if qualid_is_ident qid then tag_var (pr_id @@ qualid_basename qid) + else pr_qualid qid let pr_cref ref us = pr_reference ref ++ pr_universe_instance us @@ -564,9 +564,9 @@ let tag_var = tag Tag.variable return (p ++ prlist (pr spc (lapp,L)) l2, lapp) else return (p, lproj) - | CAppExpl ((None,{v=Ident var},us),[t]) - | CApp ((_, {v = CRef({v=Ident var},us)}),[t,None]) - when Id.equal var Notation_ops.ldots_var -> + | CAppExpl ((None,qid,us),[t]) + | CApp ((_, {v = CRef(qid,us)}),[t,None]) + when qualid_is_ident qid && Id.equal (qualid_basename qid) Notation_ops.ldots_var -> return ( hov 0 (str ".." ++ pr spc (latom,E) t ++ spc () ++ str ".."), larg diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index ce37c3614..bca419c9a 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -47,7 +47,7 @@ val pr_guard_annot : (constr_expr -> Pp.t) -> lident option * recursion_order_expr -> Pp.t -val pr_record_body : (reference * constr_expr) list -> Pp.t +val pr_record_body : (qualid * constr_expr) list -> Pp.t val pr_binders : local_binder_expr list -> Pp.t val pr_constr_pattern_expr : constr_pattern_expr -> Pp.t val pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t diff --git a/printing/prettyp.ml b/printing/prettyp.ml index fe6cf73c7..5e5d00362 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -344,8 +344,7 @@ let register_locatable name f = exception ObjFound of logical_name -let locate_any_name ref = - let {v=qid} = qualid_of_reference ref in +let locate_any_name qid = try Term (Nametab.locate qid) with Not_found -> try Syntactic (Nametab.locate_syndef qid) @@ -452,8 +451,7 @@ type locatable_kind = | LocOther of string | LocAny -let print_located_qualid name flags ref = - let {v=qid} = qualid_of_reference ref in +let print_located_qualid name flags qid = let located = match flags with | LocTerm -> locate_term qid | LocModule -> locate_modtype qid @ locate_module qid @@ -787,10 +785,9 @@ let print_full_pure_context env sigma = follows the definition of the inductive type *) (* This is designed to print the contents of an opened section *) -let read_sec_context r = - let qid = qualid_of_reference r in +let read_sec_context qid = let dir = - try Nametab.locate_section qid.v + try Nametab.locate_section qid with Not_found -> user_err ?loc:qid.loc ~hdr:"read_sec_context" (str "Unknown section.") in let rec get_cxt in_cxt = function diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 0375cfc92..8dd729610 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -24,20 +24,20 @@ val print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node val print_full_context : env -> Evd.evar_map -> Pp.t val print_full_context_typ : env -> Evd.evar_map -> Pp.t val print_full_pure_context : env -> Evd.evar_map -> Pp.t -val print_sec_context : env -> Evd.evar_map -> reference -> Pp.t -val print_sec_context_typ : env -> Evd.evar_map -> reference -> Pp.t +val print_sec_context : env -> Evd.evar_map -> qualid -> Pp.t +val print_sec_context_typ : env -> Evd.evar_map -> qualid -> Pp.t val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> Pp.t val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> Pp.t val print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t -val print_name : env -> Evd.evar_map -> reference Constrexpr.or_by_notation -> +val print_name : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation -> UnivNames.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 Constrexpr.or_by_notation -> +val print_opaque_name : env -> Evd.evar_map -> qualid -> Pp.t +val print_about : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation -> UnivNames.univ_name_list option -> Pp.t -val print_impargs : reference Constrexpr.or_by_notation -> Pp.t +val print_impargs : qualid Constrexpr.or_by_notation -> Pp.t (** Pretty-printing functions for classes and coercions *) val print_graph : env -> evar_map -> Pp.t @@ -77,10 +77,10 @@ val register_locatable : string -> 'a locatable_info -> unit name describing the kind of objects considered and that is added as a grammar command prefix for vernacular commands Locate. *) -val print_located_qualid : reference -> Pp.t -val print_located_term : reference -> Pp.t -val print_located_module : reference -> Pp.t -val print_located_other : string -> reference -> Pp.t +val print_located_qualid : qualid -> Pp.t +val print_located_term : qualid -> Pp.t +val print_located_module : qualid -> Pp.t +val print_located_other : string -> qualid -> Pp.t type object_pr = { print_inductive : MutInd.t -> UnivNames.univ_name_list option -> Pp.t; diff --git a/printing/printer.ml b/printing/printer.ml index 72030dc9f..d76bd1e2b 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -229,15 +229,15 @@ let dirpath_of_global = function dirpath_of_mp (MutInd.modpath kn) | VarRef _ -> DirPath.empty -let qualid_of_global env r = - Libnames.make_qualid (dirpath_of_global r) (id_of_global env r) +let qualid_of_global ?loc env r = + Libnames.make_qualid ?loc (dirpath_of_global r) (id_of_global env r) let safe_gen f env sigma c = let orig_extern_ref = Constrextern.get_extern_reference () in let extern_ref ?loc vars r = try orig_extern_ref vars r with e when CErrors.noncritical e -> - CAst.make ?loc @@ Libnames.Qualid (qualid_of_global env r) + qualid_of_global ?loc env r in Constrextern.set_extern_reference extern_ref; try diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 544175c6d..ba4cde6d6 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -87,7 +87,7 @@ let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv = let evd' = if has_typeclass then Typeclasses.resolve_typeclasses ~fast_path:false ~filter:Typeclasses.all_evars - ~fail:(not with_evars) clenv.env clenv.evd + ~fail:(not with_evars) ~split:false clenv.env clenv.evd else clenv.evd in if has_resolvable then diff --git a/stm/spawned.ml b/stm/spawned.ml index 3833c8026..a5d6ea96f 100644 --- a/stm/spawned.ml +++ b/stm/spawned.ml @@ -28,13 +28,11 @@ let controller h pr pw = prerr_endline "starting controller thread"; let main () = let ic, oc = open_bin_connection h pr pw in - let rec loop () = + let loop () = try match CThread.thread_friendly_input_value ic with | Hello _ -> prerr_endline "internal protocol error"; exit 1 | ReqDie -> prerr_endline "death sentence received"; exit 0 - | ReqStats -> - output_value oc (RespStats (Gc.quick_stat ())); flush oc; loop () with | e -> prerr_endline ("control channel broken: " ^ Printexc.to_string e); diff --git a/stm/stm.ml b/stm/stm.ml index c394be22e..0aed88a53 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2558,8 +2558,8 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = let load_objs libs = let rq_file (dir, from, exp) = - let mp = CAst.make @@ Libnames.(Qualid (qualid_of_string dir)) in - let mfrom = Option.map (fun fr -> CAst.make @@ Libnames.(Qualid (qualid_of_string fr))) from in + let mp = Libnames.qualid_of_string dir in + let mfrom = Option.map Libnames.qualid_of_string from in Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in List.(iter rq_file (rev libs)) in diff --git a/tactics/hints.ml b/tactics/hints.ml index d49c8aaa5..85ff02824 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -125,7 +125,7 @@ type 'a hints_path_gen = | PathEmpty | PathEpsilon -type pre_hints_path = Libnames.reference hints_path_gen +type pre_hints_path = Libnames.qualid hints_path_gen type hints_path = GlobRef.t hints_path_gen type hint_term = @@ -157,7 +157,7 @@ type hint_entry = GlobRef.t option * raw_hint hint_ast with_uid with_metadata type reference_or_constr = - | HintsReference of reference + | HintsReference of qualid | HintsConstr of Constrexpr.constr_expr type hint_mode = @@ -167,12 +167,12 @@ type hint_mode = type hints_expr = | HintsResolve of (hint_info_expr * bool * reference_or_constr) list - | HintsResolveIFF of bool * reference list * int option + | HintsResolveIFF of bool * qualid list * int option | HintsImmediate of reference_or_constr list - | HintsUnfold of reference list - | HintsTransparency of reference list * bool - | HintsMode of reference * hint_mode list - | HintsConstructors of reference list + | HintsUnfold of qualid list + | HintsTransparency of qualid list * bool + | HintsMode of qualid * hint_mode list + | HintsConstructors of qualid list | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument type import_level = [ `LAX | `WARN | `STRICT ] @@ -1360,7 +1360,7 @@ let interp_hints poly = let constr_hints_of_ind qid = let ind = global_inductive_with_alias qid in let mib,_ = Global.lookup_inductive ind in - Dumpglob.dump_reference ?loc:qid.CAst.loc "<>" (string_of_reference qid) "ind"; + Dumpglob.dump_reference ?loc:qid.CAst.loc "<>" (string_of_qualid qid) "ind"; List.init (nconstructors ind) (fun i -> let c = (ind,i+1) in let gr = ConstructRef c in diff --git a/tactics/hints.mli b/tactics/hints.mli index e958f986e..ca18f835a 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -73,7 +73,7 @@ type search_entry type hint_entry type reference_or_constr = - | HintsReference of Libnames.reference + | HintsReference of Libnames.qualid | HintsConstr of Constrexpr.constr_expr type hint_mode = @@ -83,12 +83,12 @@ type hint_mode = type hints_expr = | HintsResolve of (hint_info_expr * bool * reference_or_constr) list - | HintsResolveIFF of bool * Libnames.reference list * int option + | HintsResolveIFF of bool * Libnames.qualid list * int option | HintsImmediate of reference_or_constr list - | HintsUnfold of Libnames.reference list - | HintsTransparency of Libnames.reference list * bool - | HintsMode of Libnames.reference * hint_mode list - | HintsConstructors of Libnames.reference list + | HintsUnfold of Libnames.qualid list + | HintsTransparency of Libnames.qualid list * bool + | HintsMode of Libnames.qualid * hint_mode list + | HintsConstructors of Libnames.qualid list | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument type 'a hints_path_gen = @@ -99,7 +99,7 @@ type 'a hints_path_gen = | PathEmpty | PathEpsilon -type pre_hints_path = Libnames.reference hints_path_gen +type pre_hints_path = Libnames.qualid hints_path_gen type hints_path = GlobRef.t hints_path_gen val normalize_path : hints_path -> hints_path @@ -110,9 +110,9 @@ val pp_hints_path_atom : ('a -> Pp.t) -> 'a hints_path_atom_gen -> Pp.t val pp_hints_path : hints_path -> Pp.t val pp_hint_mode : hint_mode -> Pp.t val glob_hints_path_atom : - Libnames.reference hints_path_atom_gen -> GlobRef.t hints_path_atom_gen + Libnames.qualid hints_path_atom_gen -> GlobRef.t hints_path_atom_gen val glob_hints_path : - Libnames.reference hints_path_gen -> GlobRef.t hints_path_gen + Libnames.qualid hints_path_gen -> GlobRef.t hints_path_gen module Hint_db : sig diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 770e31fea..c430edf2e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -5034,6 +5034,26 @@ let tclABSTRACT ?(opaque=true) name_op tac = else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in abstract_subproof ~opaque s gk tac +let constr_eq ~strict x y = + let fail = Tacticals.New.tclFAIL 0 (str "Not equal") in + let fail_universes = Tacticals.New.tclFAIL 0 (str "Not equal (due to universes)") in + Proofview.Goal.enter begin fun gl -> + let env = Tacmach.New.pf_env gl in + let evd = Tacmach.New.project gl in + match EConstr.eq_constr_universes env evd x y with + | Some csts -> + let csts = UnivProblem.to_constraints ~force_weak:false (Evd.universes evd) csts in + if strict then + if Evd.check_constraints evd csts then Proofview.tclUNIT () + else fail_universes + else + (match Evd.add_constraints evd csts with + | evd -> Proofview.Unsafe.tclEVARS evd + | exception Univ.UniverseInconsistency _ -> + fail_universes) + | None -> fail + end + let unify ?(state=full_transparent_state) x y = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 8d4302450..57f20d2ff 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -409,6 +409,11 @@ val generalize_dep : ?with_let:bool (** Don't lose let bindings *) -> constr - (** {6 Other tactics. } *) +(** Syntactic equality up to universes. With [strict] the universe + constraints must be already true to succeed, without [strict] they + are added to the evar map. *) +val constr_eq : strict:bool -> constr -> constr -> unit Proofview.tactic + val unify : ?state:Names.transparent_state -> constr -> constr -> unit Proofview.tactic val cache_term_by_tactic_then : opaque:bool -> ?goal_type:(constr option) -> Id.t -> Decl_kinds.goal_kind -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic diff --git a/test-suite/bugs/closed/7421.v b/test-suite/bugs/closed/7421.v new file mode 100644 index 000000000..afcdd35fc --- /dev/null +++ b/test-suite/bugs/closed/7421.v @@ -0,0 +1,39 @@ + + +Universe i j. + +Goal False. +Proof. + Check Type@{i} : Type@{j}. + Fail constr_eq_strict Type@{i} Type@{j}. + assert_succeeds constr_eq Type@{i} Type@{j}. (* <- i=j is forgotten after assert_succeeds *) + Fail constr_eq_strict Type@{i} Type@{j}. + + constr_eq Type@{i} Type@{j}. (* <- i=j is retained *) + constr_eq_strict Type@{i} Type@{j}. + Fail Check Type@{i} : Type@{j}. + + Fail constr_eq Prop Set. + Fail constr_eq Prop Type. + + Fail constr_eq_strict Type Type. + constr_eq Type Type. + + constr_eq_strict Set Set. + constr_eq Set Set. + constr_eq Prop Prop. + + let x := constr:(Type) in constr_eq_strict x x. + let x := constr:(Type) in constr_eq x x. + + Fail lazymatch type of prod with + | ?A -> ?B -> _ => constr_eq_strict A B + end. + lazymatch type of prod with + | ?A -> ?B -> _ => constr_eq A B + end. + lazymatch type of prod with + | ?A -> ?B -> ?C => constr_eq A C + end. + +Abort. diff --git a/test-suite/bugs/closed/7811.v b/test-suite/bugs/closed/7811.v new file mode 100644 index 000000000..fee330f22 --- /dev/null +++ b/test-suite/bugs/closed/7811.v @@ -0,0 +1,114 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-top" "atomic" "-Q" "." "iris" "-R" "." "stdpp") -*- *) +(* File reduced by coq-bug-finder from original input, then from 140 lines to 26 lines, then from 141 lines to 27 lines, then from 142 lines to 27 lines, then from 272 lines to 61 lines, then from 291 lines to 94 lines, then from 678 lines to 142 lines, then from 418 lines to 161 lines, then from 538 lines to 189 lines, then from 840 lines to 493 lines, then from 751 lines to 567 lines, then from 913 lines to 649 lines, then from 875 lines to 666 lines, then from 784 lines to 568 lines, then from 655 lines to 173 lines, then from 317 lines to 94 lines, then from 172 lines to 86 lines, then from 102 lines to 86 lines, then from 130 lines to 86 lines, then from 332 lines to 112 lines, then from 279 lines to 111 lines, then from 3996 lines to 5697 lines, then from 153 lines to 117 lines, then from 146 lines to 108 lines, then from 124 lines to 108 lines *) +(* coqc version 8.8.0 (May 2018) compiled on May 2 2018 16:49:46 with OCaml 4.02.3 + coqtop version 8.8.0 (May 2018) *) + +(* This was triggering a "Not_found" at the time of printing/showing the goal *) + +Require Coq.Unicode.Utf8. + +Notation "t $ r" := (t r) + (at level 65, right associativity, only parsing). + +Inductive tele : Type := + | TeleO : tele + | TeleS {X} (binder : X -> tele) : tele. + +Fixpoint tele_fun (TT : tele) (T : Type) : Type := + match TT with + | TeleO => T + | TeleS b => forall x, tele_fun (b x) T + end. + +Inductive tele_arg : tele -> Type := +| TargO : tele_arg TeleO +| TargS {X} {binder} (x : X) : tele_arg (binder x) -> tele_arg (TeleS binder). + +Axiom tele_app : forall {TT : tele} {T} (f : tele_fun TT T), tele_arg TT -> T. + +Coercion tele_arg : tele >-> Sortclass. + +Inductive val := + | LitV + | PairV (v1 v2 : val) + | InjLV (v : val) + | InjRV (v : val). +Axiom coPset : Set. +Axiom atomic_update : forall {PROP : Type} {TA TB : tele}, coPset -> coPset -> (TA -> PROP) -> (TA -> TB -> PROP) -> (TA -> TB -> PROP) -> PROP. +Import Coq.Unicode.Utf8. +Notation "'AU' '<<' ∀ x1 .. xn , α '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" := + (atomic_update (TA:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) + (TB:=TeleO) + Eo Ei + (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $ + λ x1, .. (λ xn, α) ..) + (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $ + λ x1, .. (λ xn, tele_app (TT:=TeleO) β) .. ) + (tele_app (TT:=TeleS (λ x1, .. (TeleS (λ xn, TeleO)) .. )) $ + λ x1, .. (λ xn, tele_app (TT:=TeleO) Φ) .. ) + ) + (at level 20, Eo, Ei, α, β, Φ at level 200, x1 binder, xn binder, + format "'[ ' 'AU' '<<' ∀ x1 .. xn , α '>>' '/' @ Eo , Ei '/' '[ ' '<<' β , '/' COMM Φ '>>' ']' ']'") : bi_scope. + +Axiom ident : Set. +Inductive env (A : Type) : Type := Enil : env A | Esnoc : env A → ident → A → env A. +Record envs (PROP : Type) : Type + := Envs { env_spatial : env PROP }. +Axiom positive : Set. +Axiom Qp : Set. +Axiom one : positive. +Goal forall (T : Type) (T0 : forall _ : T, Type) (P : Set) + (u : T) (γs : P) (Q : T0 u) (Φ o : forall _ : val, T0 u) + (stack_content0 : forall (_ : P) (_ : list val), T0 u) + (c c0 : coPset) (l : forall (A : Type) (_ : list A), list A) + (e0 : forall (_ : env (T0 u)) (_ : positive), envs (T0 u)) + (i0 : ident) (o1 : forall (_ : Qp) (_ : val), T0 u) + (b0 : forall _ : env (T0 u), T0 u) (P0 : forall _ : T0 u, Type) + (u0 : forall (_ : T0 u) (_ : T0 u), T0 u), + P0 + (@atomic_update (T0 u) + (@TeleS val (fun _ : val => @TeleS Qp (fun _ : Qp => TeleO))) TeleO c c0 + (@tele_app (@TeleS val (fun _ : val => @TeleS Qp (fun _ : Qp => TeleO))) + (T0 u) (fun (v : val) (q : Qp) => o1 q v)) + (@tele_app (@TeleS val (fun _ : val => @TeleS Qp (fun _ : Qp => TeleO))) + (forall _ : tele_arg TeleO, T0 u) + (fun (v : val) (q : Qp) => @tele_app TeleO (T0 u) (o1 q v))) + (@tele_app (@TeleS val (fun _ : val => @TeleS Qp (fun _ : Qp => TeleO))) + (forall _ : tele_arg TeleO, T0 u) + (fun (x : val) (_ : Qp) => + @tele_app TeleO (T0 u) + (u0 + (b0 + match + e0 + (@Esnoc (T0 u) (@Enil (T0 u)) i0 + (@atomic_update (T0 u) + (@TeleS (list val) (fun _ : list val => TeleO)) TeleO + c c0 + (@tele_app + (@TeleS (list val) (fun _ : list val => TeleO)) + (T0 u) (fun l0 : list val => stack_content0 γs l0)) + (@tele_app + (@TeleS (list val) (fun _ : list val => TeleO)) + (forall _ : tele_arg TeleO, T0 u) + (fun l0 : list val => + @tele_app TeleO (T0 u) + (stack_content0 γs (l val l0)))) + (@tele_app + (@TeleS (list val) (fun _ : list val => TeleO)) + (forall _ : tele_arg TeleO, T0 u) + (fun x1 : list val => + @tele_app TeleO (T0 u) + (u0 Q + (Φ + match x1 return val with + | nil => InjLV LitV + | cons v _ => InjRV v + end)))))) one + return (env (T0 u)) + with + | Envs _ env_spatial0 => env_spatial0 + end) (o x))))) +. + Show. +Abort. diff --git a/test-suite/ssr/rew_polyuniv.v b/test-suite/ssr/rew_polyuniv.v new file mode 100644 index 000000000..e2bbbc9ec --- /dev/null +++ b/test-suite/ssr/rew_polyuniv.v @@ -0,0 +1,90 @@ +From Coq Require Import Utf8 Setoid ssreflect. +Set Default Proof Using "Type". + +Local Set Universe Polymorphism. + +(** Telescopes *) +Inductive tele : Type := + | TeleO : tele + | TeleS {X} (binder : X → tele) : tele. + +Arguments TeleS {_} _. + +(** The telescope version of Coq's function type *) +Fixpoint tele_fun (TT : tele) (T : Type) : Type := + match TT with + | TeleO => T + | TeleS b => ∀ x, tele_fun (b x) T + end. + +Notation "TT -t> A" := + (tele_fun TT A) (at level 99, A at level 200, right associativity). + +(** A sigma-like type for an "element" of a telescope, i.e. the data it + takes to get a [T] from a [TT -t> T]. *) +Inductive tele_arg : tele → Type := +| TargO : tele_arg TeleO +(* the [x] is the only relevant data here *) +| TargS {X} {binder} (x : X) : tele_arg (binder x) → tele_arg (TeleS binder). + +Definition tele_app {TT : tele} {T} (f : TT -t> T) : tele_arg TT → T := + λ a, (fix rec {TT} (a : tele_arg TT) : (TT -t> T) → T := + match a in tele_arg TT return (TT -t> T) → T with + | TargO => λ t : T, t + | TargS x a => λ f, rec a (f x) + end) TT a f. +Arguments tele_app {!_ _} _ !_ /. + +Coercion tele_arg : tele >-> Sortclass. +Coercion tele_app : tele_fun >-> Funclass. + +(** Inversion lemma for [tele_arg] *) +Lemma tele_arg_inv {TT : tele} (a : TT) : + match TT as TT return TT → Prop with + | TeleO => λ a, a = TargO + | TeleS f => λ a, ∃ x a', a = TargS x a' + end a. +Proof. induction a; eauto. Qed. +Lemma tele_arg_O_inv (a : TeleO) : a = TargO. +Proof. exact (tele_arg_inv a). Qed. +Lemma tele_arg_S_inv {X} {f : X → tele} (a : TeleS f) : + ∃ x a', a = TargS x a'. +Proof. exact (tele_arg_inv a). Qed. + +(** Operate below [tele_fun]s with argument telescope [TT]. *) +Fixpoint tele_bind {U} {TT : tele} : (TT → U) → TT -t> U := + match TT as TT return (TT → U) → TT -t> U with + | TeleO => λ F, F TargO + | @TeleS X b => λ (F : TeleS b → U) (x : X), (* b x -t> U *) + tele_bind (λ a, F (TargS x a)) + end. +Arguments tele_bind {_ !_} _ /. + +(* Show that tele_app ∘ tele_bind is the identity. *) +Lemma tele_app_bind {U} {TT : tele} (f : TT → U) x : + (tele_app (tele_bind f)) x = f x. +Proof. + induction TT as [|X b IH]; simpl in *. + - rewrite (tele_arg_O_inv x). auto. + - destruct (tele_arg_S_inv x) as [x' [a' ->]]. simpl. + rewrite IH. auto. +Qed. + +(** Notation-compatible telescope mapping *) +(* This adds (tele_app ∘ tele_bind), which is an identity function, around every + binder so that, after simplifying, this matches the way we typically write + notations involving telescopes. *) +Notation "'λ..' x .. y , e" := + (tele_app (tele_bind (λ x, .. (tele_app (tele_bind (λ y, e))) .. ))) + (at level 200, x binder, y binder, right associativity, + format "'[ ' 'λ..' x .. y ']' , e"). + +(* The testcase *) +Lemma test {TA TB : tele} {X} (α' β' γ' : X → Prop) (Φ : TA → TB → Prop) x' : + (forall P Q, ((P /\ Q) = Q) * ((P -> Q) = Q)) -> + ∀ a b, Φ a b = (λ.. x y, β' x' ∧ (γ' x' → Φ x y)) a b. +Proof. +intros cheat a b. +rewrite !tele_app_bind. +by rewrite !cheat. +Qed. diff --git a/test-suite/ssr/set_polyuniv.v b/test-suite/ssr/set_polyuniv.v new file mode 100644 index 000000000..436eeafc7 --- /dev/null +++ b/test-suite/ssr/set_polyuniv.v @@ -0,0 +1,11 @@ +From Coq Require Import ssreflect. +Set Default Proof Using "Type". + +Local Set Universe Polymorphism. + +Axiom foo : Type -> Prop. + +Lemma test : foo nat. +Proof. +set x := foo _. (* key @foo{i} matches @foo{j} *) +Abort. diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v index 8d08f5975..717dc0deb 100644 --- a/test-suite/success/Hints.v +++ b/test-suite/success/Hints.v @@ -169,7 +169,7 @@ Proof. Hint Cut [_* (a_is_b | b_is_c | c_is_d | d_is_e) (a_compose | b_compose | c_compose | d_compose | e_compose)] : typeclass_instances. - Timeout 1 Fail apply _. (* 0.06s *) +Timeout 1 Fail apply _. (* 0.06s *) Abort. End HintCut. diff --git a/test-suite/success/letproj.v b/test-suite/success/letproj.v index de2857b43..2f0d8bf8c 100644 --- a/test-suite/success/letproj.v +++ b/test-suite/success/letproj.v @@ -7,3 +7,5 @@ Definition test (A : Type) (f : Foo A) := Scheme foo_case := Case for Foo Sort Type. +Definition test' (A : Type) (f : Foo A) := + let 'Build_Foo _ x y := f in x. diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v index 31a1608c4..7ca2767a5 100644 --- a/test-suite/success/primitiveproj.v +++ b/test-suite/success/primitiveproj.v @@ -199,3 +199,24 @@ split. reflexivity. Qed. *) + +(* Primitive projection match compilation *) +Require Import List. +Set Primitive Projections. + +Record prod (A B : Type) := pair { fst : A ; snd : B }. +Arguments pair {_ _} _ _. + +Fixpoint split_at {A} (l : list A) (n : nat) : prod (list A) (list A) := + match n with + | 0 => pair nil l + | S n => + match l with + | nil => pair nil nil + | x :: l => let 'pair l1 l2 := split_at l n in pair (x :: l1) l2 + end + end. + +Time Eval vm_compute in split_at (repeat 0 20) 10. (* Takes 0s *) +Time Eval vm_compute in split_at (repeat 0 40) 20. (* Takes 0.001s *) +Timeout 1 Time Eval vm_compute in split_at (repeat 0 60) 30. (* Used to take 60s, now takes 0.001s *) diff --git a/tools/inferior-coq.el b/tools/inferior-coq.el index b79d97d66..453bd1391 100644 --- a/tools/inferior-coq.el +++ b/tools/inferior-coq.el @@ -265,7 +265,7 @@ With argument, position cursor at end of buffer." (let ((end (point))) (beginning-of-line) (coq-send-region (point) end))) - (next-line 1)) + (forward-line 1)) (defun coq-send-abort () "Send the command \"Abort.\" to the inferior Coq process." diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index e61f830f3..e1d35e537 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -92,6 +92,14 @@ let libs_init_load_path ~load_init = let coqpath = Envars.coqpath in let coq_path = Names.DirPath.make [Libnames.coq_root] in + (* current directory (not recursively!) *) + [ { recursive = false; + path_spec = VoPath { unix_path = "."; + coq_path = Libnames.default_root_prefix; + implicit = false; + has_ml = AddTopML } + } ] @ + (* then standard library and plugins *) [build_stdlib_path ~load_init ~unix_path:(coqlib/"theories") ~coq_path ~with_ml:false; build_stdlib_path ~load_init ~unix_path:(coqlib/"plugins") ~coq_path ~with_ml:true ] @ @@ -102,15 +110,7 @@ let libs_init_load_path ~load_init = ) @ (* then directories in XDG_DATA_DIRS and XDG_DATA_HOME and COQPATH *) - List.map (fun s -> build_userlib_path ~unix_path:s) (xdg_dirs @ coqpath) @ - - (* then current directory (not recursively!) *) - [ { recursive = false; - path_spec = VoPath { unix_path = "."; - coq_path = Libnames.default_root_prefix; - implicit = false; - has_ml = AddTopML } - } ] + List.map (fun s -> build_userlib_path ~unix_path:s) (xdg_dirs @ coqpath) (* Initialises the Ocaml toplevel before launching it, so that it can find the "include" file in the *source* directory *) diff --git a/vernac/classes.ml b/vernac/classes.ml index 8cf3895fb..382d18b09 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -229,10 +229,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) let sigma, c = interp_casted_constr_evars env' sigma term cty in Some (Inr (c, subst)), sigma | Some (Inl props) -> - let get_id = CAst.map (function - | Ident id' -> id' - | Qualid id' -> snd (repr_qualid id')) - in + let get_id qid = CAst.make ?loc:qid.CAst.loc @@ qualid_basename qid in let props, rest = List.fold_left (fun (props, rest) decl -> diff --git a/vernac/classes.mli b/vernac/classes.mli index eea2a211d..bd30b2d60 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -22,7 +22,7 @@ val mismatched_props : env -> constr_expr list -> Context.Rel.t -> 'a (** Instance declaration *) -val existing_instance : bool -> reference -> Hints.hint_info_expr option -> unit +val existing_instance : bool -> qualid -> Hints.hint_info_expr option -> unit (** globality, reference, optional priority and pattern information *) val declare_instance_constant : diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index b93e8d9ac..6057c05f5 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -44,8 +44,8 @@ let rec complete_conclusion a cs = CAst.map_with_loc (fun ?loc -> function user_err ?loc (strbrk"Cannot infer the non constant arguments of the conclusion of " ++ Id.print cs ++ str "."); - let args = List.map (fun id -> CAst.(make ?loc @@ CRef(make ?loc @@ Ident id,None))) params in - CAppExpl ((None,CAst.make ?loc @@ Ident name,None),List.rev args) + let args = List.map (fun id -> CAst.(make ?loc @@ CRef(qualid_of_ident ?loc id,None))) params in + CAppExpl ((None,qualid_of_ident ?loc name,None),List.rev args) | c -> c ) diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index a6d7fccf3..eef7afbfb 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -44,7 +44,7 @@ let mkSubset sigma name typ prop = let sigT = Lazy.from_fun build_sigma_type -let make_qref s = CAst.make @@ Qualid (qualid_of_string s) +let make_qref s = qualid_of_string s let lt_ref = make_qref "Init.Peano.lt" let rec telescope sigma l = diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index 434e836d8..cc9be7b0e 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -229,7 +229,7 @@ type prod_info = production_level * production_position type (_, _) entry = | TTName : ('self, lname) entry -| TTReference : ('self, reference) entry +| TTReference : ('self, qualid) entry | TTBigint : ('self, Constrexpr.raw_natural_number) entry | TTConstr : prod_info * 'r target -> ('r, 'r) entry | TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry @@ -312,7 +312,7 @@ let interp_entry forpat e = match e with let cases_pattern_expr_of_name { CAst.loc; v = na } = CAst.make ?loc @@ match na with | Anonymous -> CPatAtom None - | Name id -> CPatAtom (Some (CAst.make ?loc @@ Ident id)) + | Name id -> CPatAtom (Some (qualid_of_ident ?loc id)) type 'r env = { constrs : 'r list; diff --git a/vernac/g_vernac.ml4 b/vernac/g_vernac.ml4 index 3a59242de..16934fc86 100644 --- a/vernac/g_vernac.ml4 +++ b/vernac/g_vernac.ml4 @@ -549,7 +549,7 @@ GEXTEND Gram ] ] ; module_expr_atom: - [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (qid.CAst.v) | "("; me = module_expr; ")" -> me ] ] + [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident qid | "("; me = module_expr; ")" -> me ] ] ; with_declaration: [ [ "Definition"; fqid = fullyqualid; udecl = OPT univ_decl; ":="; c = Constr.lconstr -> @@ -559,7 +559,7 @@ GEXTEND Gram ] ] ; module_type: - [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (qid.CAst.v) + [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident qid | "("; mt = module_type; ")" -> mt | mty = module_type; me = module_expr_atom -> CAst.make ~loc:!@loc @@ CMapply (mty,me) diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 2deca1e06..e86e10877 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -370,7 +370,7 @@ requested | 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 do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort = let lrecnames = List.map (fun ({CAst.v},_,_,_) -> v) lnamedepindsort and env0 = Global.env() in let sigma, lrecspec, _ = @@ -388,7 +388,7 @@ let do_mutual_induction_scheme lnamedepindsort = (evd, (indu,dep,sort) :: l, inst)) lnamedepindsort (Evd.from_env env0,[],None) in - let sigma, listdecl = Indrec.build_mutual_induction_scheme env0 sigma lrecspec in + let sigma, listdecl = Indrec.build_mutual_induction_scheme env0 sigma ~force_mutual lrecspec in let declare decl fi lrecref = let decltype = Retyping.get_type_of env0 sigma (EConstr.of_constr decl) in let decltype = EConstr.to_constr sigma decltype in diff --git a/vernac/indschemes.mli b/vernac/indschemes.mli index 261c3d813..ebfc76de9 100644 --- a/vernac/indschemes.mli +++ b/vernac/indschemes.mli @@ -29,9 +29,13 @@ val declare_congr_scheme : inductive -> unit val declare_rewriting_schemes : inductive -> unit -(** Mutual Minimality/Induction scheme *) +(** Mutual Minimality/Induction scheme. + [force_mutual] forces the construction of eliminators having the same predicates and + methods even if some of the inductives are not recursive. + By default it is [false] and some of the eliminators are defined as simple case analysis. + *) -val do_mutual_induction_scheme : +val do_mutual_induction_scheme : ?force_mutual:bool -> (lident * bool * inductive * Sorts.family) list -> unit (** Main calls to interpret the Scheme command *) diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 8f64f5519..da14358ef 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1449,7 +1449,7 @@ let add_notation_extra_printing_rule df k v = (* Infix notations *) -let inject_var x = CAst.make @@ CRef (CAst.make @@ Ident (Id.of_string x),None) +let inject_var x = CAst.make @@ CRef (qualid_of_ident (Id.of_string x),None) let add_infix local env ({CAst.loc;v=inf},modifiers) pr sc = check_infix_modifiers modifiers; diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index d0c423650..56dfaa54a 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -16,7 +16,6 @@ open Util open CAst open Extend -open Libnames open Decl_kinds open Constrexpr open Constrexpr_ops @@ -79,13 +78,13 @@ open Pputils let pr_lname_decl (n, u) = pr_lname n ++ pr_universe_decl u - let pr_smart_global = Pputils.pr_or_by_notation pr_reference + let pr_smart_global = Pputils.pr_or_by_notation pr_qualid - let pr_ltac_ref = Libnames.pr_reference + let pr_ltac_ref = Libnames.pr_qualid - let pr_module = Libnames.pr_reference + let pr_module = Libnames.pr_qualid - let pr_import_module = Libnames.pr_reference + let pr_import_module = Libnames.pr_qualid let sep_end = function | VernacBullet _ @@ -157,7 +156,7 @@ open Pputils let pr_locality local = if local then keyword "Local" else keyword "Global" let pr_option_ref_value = function - | QualidRefValue id -> pr_reference id + | QualidRefValue id -> pr_qualid id | StringRefValue s -> qs s let pr_printoption table b = @@ -180,7 +179,7 @@ open Pputils | _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z let pr_reference_or_constr pr_c = function - | HintsReference r -> pr_reference r + | HintsReference r -> pr_qualid r | HintsConstr c -> pr_c c let pr_hint_mode = function @@ -202,24 +201,24 @@ open Pputils l | HintsResolveIFF (l2r, l, n) -> keyword "Resolve " ++ str (if l2r then "->" else "<-") - ++ prlist_with_sep sep pr_reference l + ++ prlist_with_sep sep pr_qualid l | HintsImmediate l -> keyword "Immediate" ++ spc() ++ prlist_with_sep sep (fun c -> pr_reference_or_constr pr_c c) l | HintsUnfold l -> - keyword "Unfold" ++ spc () ++ prlist_with_sep sep pr_reference l + keyword "Unfold" ++ spc () ++ prlist_with_sep sep pr_qualid l | HintsTransparency (l, b) -> keyword (if b then "Transparent" else "Opaque") ++ spc () - ++ prlist_with_sep sep pr_reference l + ++ prlist_with_sep sep pr_qualid l | HintsMode (m, l) -> keyword "Mode" ++ spc () - ++ pr_reference m ++ spc() ++ + ++ pr_qualid m ++ spc() ++ prlist_with_sep spc pr_hint_mode l | HintsConstructors c -> keyword "Constructors" - ++ spc() ++ prlist_with_sep spc pr_reference c + ++ spc() ++ prlist_with_sep spc pr_qualid c | HintsExtern (n,c,tac) -> let pat = match c with None -> mt () | Some pat -> pr_pat pat in keyword "Extern" ++ spc() ++ int n ++ spc() ++ pat ++ str" =>" ++ @@ -233,7 +232,7 @@ open Pputils keyword "Definition" ++ spc() ++ pr_lfqid id ++ pr_universe_decl udecl ++ str" := " ++ p | CWith_Module (id,qid) -> keyword "Module" ++ spc() ++ pr_lfqid id ++ str" := " ++ - pr_ast pr_qualid qid + pr_qualid qid let rec pr_module_ast leading_space pr_c = function | { loc ; v = CMident qid } -> @@ -451,7 +450,7 @@ open Pputils | PrintFullContext -> keyword "Print All" | PrintSectionContext s -> - keyword "Print Section" ++ spc() ++ Libnames.pr_reference s + keyword "Print Section" ++ spc() ++ Libnames.pr_qualid s | PrintGrammar ent -> keyword "Print Grammar" ++ spc() ++ str ent | PrintLoadPath dir -> @@ -499,9 +498,9 @@ open Pputils | PrintName (qid,udecl) -> keyword "Print" ++ spc() ++ pr_smart_global qid ++ pr_univ_name_list udecl | PrintModuleType qid -> - keyword "Print Module Type" ++ spc() ++ pr_reference qid + keyword "Print Module Type" ++ spc() ++ pr_qualid qid | PrintModule qid -> - keyword "Print Module" ++ spc() ++ pr_reference qid + keyword "Print Module" ++ spc() ++ pr_qualid qid | PrintInspect n -> keyword "Inspect" ++ spc() ++ int n | PrintScopes -> @@ -604,7 +603,7 @@ open Pputils | ShowUniverses -> keyword "Show Universes" | ShowProofNames -> keyword "Show Conjectures" | ShowIntros b -> keyword "Show " ++ (if b then keyword "Intros" else keyword "Intro") - | ShowMatch id -> keyword "Show Match " ++ pr_reference id + | ShowMatch id -> keyword "Show Match " ++ pr_qualid id in return (pr_showable s) | VernacCheckGuard -> @@ -901,7 +900,7 @@ open Pputils | VernacDeclareInstances insts -> let pr_inst (id, info) = - pr_reference id ++ pr_hint_info pr_constr_pattern_expr info + pr_qualid id ++ pr_hint_info pr_constr_pattern_expr info in return ( hov 1 (keyword "Existing" ++ spc () ++ @@ -911,7 +910,7 @@ open Pputils | VernacDeclareClass id -> return ( - hov 1 (keyword "Existing" ++ spc () ++ keyword "Class" ++ spc () ++ pr_reference id) + hov 1 (keyword "Existing" ++ spc () ++ keyword "Class" ++ spc () ++ pr_qualid id) ) (* Modules and Module Types *) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 94eb45fd3..479482095 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -183,29 +183,27 @@ let print_modules () = pr_vertical_list DirPath.print only_loaded -let print_module r = - let qid = qualid_of_reference r in +let print_module qid = try - let globdir = Nametab.locate_dir qid.v in + let globdir = Nametab.locate_dir qid in match globdir with DirModule { obj_dir; obj_mp; _ } -> Printmod.print_module (Printmod.printable_body obj_dir) obj_mp | _ -> raise Not_found with - Not_found -> user_err (str"Unknown Module " ++ pr_qualid qid.v) + Not_found -> user_err (str"Unknown Module " ++ pr_qualid qid) -let print_modtype r = - let qid = qualid_of_reference r in +let print_modtype qid = try - let kn = Nametab.locate_modtype qid.v in + let kn = Nametab.locate_modtype qid in Printmod.print_modtype kn with Not_found -> (* Is there a module of this name ? If yes we display its type *) try - let mp = Nametab.locate_module qid.v in + let mp = Nametab.locate_module qid in Printmod.print_module false mp with Not_found -> - user_err (str"Unknown Module Type or Module " ++ pr_qualid qid.v) + user_err (str"Unknown Module Type or Module " ++ pr_qualid qid) let print_namespace ns = let ns = List.rev (Names.DirPath.repr ns) in @@ -367,33 +365,32 @@ let msg_found_library = function | Library.LibInPath, fulldir, file -> hov 0 (DirPath.print fulldir ++ strbrk " is bound to file " ++ str file) -let err_unmapped_library ?loc ?from qid = +let err_unmapped_library ?from qid = let dir = fst (repr_qualid qid) in let prefix = match from with | None -> str "." | Some from -> str " and prefix " ++ DirPath.print from ++ str "." in - user_err ?loc + user_err ?loc:qid.CAst.loc ~hdr:"locate_library" (strbrk "Cannot find a physical path bound to logical path matching suffix " ++ DirPath.print dir ++ prefix) -let err_notfound_library ?loc ?from qid = +let err_notfound_library ?from qid = let prefix = match from with | None -> str "." | Some from -> str " with prefix " ++ DirPath.print from ++ str "." in - user_err ?loc ~hdr:"locate_library" + user_err ?loc:qid.CAst.loc ~hdr:"locate_library" (strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix) -let print_located_library r = - let {loc;v=qid} = qualid_of_reference r in +let print_located_library qid = try msg_found_library (Library.locate_qualified_library ~warn:false qid) with - | Library.LibUnmappedDir -> err_unmapped_library ?loc qid - | Library.LibNotFound -> err_notfound_library ?loc qid + | Library.LibUnmappedDir -> err_unmapped_library qid + | Library.LibNotFound -> err_notfound_library qid let smart_global r = let gr = Smartlocate.smart_global r in @@ -636,7 +633,7 @@ let vernac_scheme l = let vernac_combined_scheme lid l = if Dumpglob.dump () then (Dumpglob.dump_definition lid false "def"; - List.iter (fun {loc;v=id} -> dump_global (make ?loc @@ AN (make ?loc @@ Ident id))) l); + List.iter (fun {loc;v=id} -> dump_global (make ?loc @@ AN (qualid_of_ident ?loc id))) l); Indschemes.do_combined_scheme lid l let vernac_universe ~atts l = @@ -657,7 +654,7 @@ let vernac_constraint ~atts l = (* Modules *) let vernac_import export refl = - Library.import_module export (List.map qualid_of_reference refl) + Library.import_module export refl let vernac_declare_module export {loc;v=id} binders_ast mty_ast = (* We check the state of the system (in section, in module type) @@ -675,7 +672,7 @@ let vernac_declare_module export {loc;v=id} binders_ast mty_ast = in Dumpglob.dump_moddef ?loc mp "mod"; Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is declared"); - Option.iter (fun export -> vernac_import export [make @@ Ident id]) export + Option.iter (fun export -> vernac_import export [qualid_of_ident id]) export 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) @@ -700,7 +697,7 @@ let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mt List.iter (fun (export,id) -> Option.iter - (fun export -> vernac_import export [make @@ Ident id]) export + (fun export -> vernac_import export [qualid_of_ident id]) export ) argsexport | _::_ -> let binders_ast = List.map @@ -715,14 +712,14 @@ let vernac_define_module export {loc;v=id} (binders_ast : module_binder list) mt Dumpglob.dump_moddef ?loc mp "mod"; Flags.if_verbose Feedback.msg_info (str "Module " ++ Id.print id ++ str " is defined"); - Option.iter (fun export -> vernac_import export [make @@ Ident id]) + Option.iter (fun export -> vernac_import export [qualid_of_ident id]) export 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 [make ?loc @@ Ident id]) export + Option.iter (fun export -> vernac_import export [qualid_of_ident ?loc id]) export let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l = if Lib.sections_are_opened () then @@ -747,7 +744,7 @@ let vernac_declare_module_type {loc;v=id} binders_ast mty_sign mty_ast_l = List.iter (fun (export,id) -> Option.iter - (fun export -> vernac_import export [make ?loc @@ Ident id]) export + (fun export -> vernac_import export [qualid_of_ident ?loc id]) export ) argsexport | _ :: _ -> @@ -809,22 +806,20 @@ let warn_require_in_section = let vernac_require from import qidl = if Lib.sections_are_opened () then warn_require_in_section (); - let qidl = List.map qualid_of_reference qidl in let root = match from with | None -> None | Some from -> - let qid = Libnames.qualid_of_reference from in - let (hd, tl) = Libnames.repr_qualid qid.v in + let (hd, tl) = Libnames.repr_qualid from in Some (Libnames.add_dirpath_suffix hd tl) in - let locate {loc;v=qid} = + let locate qid = try let warn = not !Flags.quiet in let (_, dir, f) = Library.locate_qualified_library ?root ~warn qid in (dir, f) with - | Library.LibUnmappedDir -> err_unmapped_library ?loc ?from:root qid - | Library.LibNotFound -> err_notfound_library ?loc ?from:root qid + | Library.LibUnmappedDir -> err_unmapped_library ?from:root qid + | Library.LibNotFound -> err_notfound_library ?from:root qid in let modrefl = List.map locate qidl in if Dumpglob.dump () then @@ -1687,10 +1682,10 @@ let print_about_hyp_globs ?loc ref_or_by_not udecl glopt = let glnumopt = query_command_selector ?loc glopt in let gl,id = match glnumopt, ref_or_by_not.v with - | None,AN {v=Ident id} -> (* goal number not given, catch any failure *) - (try get_nth_goal 1,id with _ -> raise NoHyp) - | Some n,AN {v=Ident id} -> (* goal number given, catch if wong *) - (try get_nth_goal n,id + | None,AN qid when qualid_is_ident qid -> (* goal number not given, catch any failure *) + (try get_nth_goal 1, qualid_basename qid with _ -> raise NoHyp) + | Some n,AN qid when qualid_is_ident qid -> (* goal number given, catch if wong *) + (try get_nth_goal n, qualid_basename qid with Failure _ -> user_err ?loc ~hdr:"print_about_hyp_globs" (str "No such goal: " ++ int n ++ str ".")) @@ -1771,11 +1766,10 @@ let vernac_print ~atts env sigma = Printer.pr_assumptionset env sigma nassums | PrintStrategy r -> print_strategy r -let global_module r = - let {loc;v=qid} = qualid_of_reference r in +let global_module qid = try Nametab.full_name_module qid with Not_found -> - user_err ?loc ~hdr:"global_module" + user_err ?loc:qid.CAst.loc ~hdr:"global_module" (str "Module/section " ++ pr_qualid qid ++ str " not found.") let interp_search_restriction = function diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 3c88a3443..02a3b2bd6 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -8,11 +8,11 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -val dump_global : Libnames.reference Constrexpr.or_by_notation -> unit +val dump_global : Libnames.qualid Constrexpr.or_by_notation -> unit (** Vernacular entries *) val vernac_require : - Libnames.reference option -> bool option -> Libnames.reference list -> unit + Libnames.qualid option -> bool option -> Libnames.qualid list -> unit (** The main interpretation function of vernacular expressions *) val interp : diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 5acac9e25..f74383b02 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -13,7 +13,7 @@ open Constrexpr open Libnames (** Vernac expressions, produced by the parser *) -type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation +type class_rawexpr = FunClass | SortClass | RefClass of qualid or_by_notation type goal_selector = Goal_select.t = | SelectAlreadyFocused @@ -37,37 +37,37 @@ type univ_name_list = UnivNames.univ_name_list type printable = | PrintTables | PrintFullContext - | PrintSectionContext of reference + | PrintSectionContext of qualid | PrintInspect of int | PrintGrammar of string | PrintLoadPath of DirPath.t option | PrintModules - | PrintModule of reference - | PrintModuleType of reference + | PrintModule of qualid + | PrintModuleType of qualid | PrintNamespace of DirPath.t | PrintMLLoadPath | PrintMLModules | PrintDebugGC - | PrintName of reference or_by_notation * UnivNames.univ_name_list option + | PrintName of qualid or_by_notation * UnivNames.univ_name_list option | PrintGraph | PrintClasses | PrintTypeClasses - | PrintInstances of reference or_by_notation + | PrintInstances of qualid or_by_notation | PrintCoercions | PrintCoercionPaths of class_rawexpr * class_rawexpr | PrintCanonicalConversions | PrintUniverses of bool * string option - | PrintHint of reference or_by_notation + | PrintHint of qualid or_by_notation | PrintHintGoal | PrintHintDbName of string | PrintHintDb | PrintScopes | PrintScope of string | PrintVisibility of string option - | PrintAbout of reference or_by_notation * UnivNames.univ_name_list option * Goal_select.t option - | PrintImplicit of reference or_by_notation - | PrintAssumptions of bool * bool * reference or_by_notation - | PrintStrategy of reference or_by_notation option + | PrintAbout of qualid or_by_notation * UnivNames.univ_name_list option * Goal_select.t option + | PrintImplicit of qualid or_by_notation + | PrintAssumptions of bool * bool * qualid or_by_notation + | PrintStrategy of qualid or_by_notation option type search_about_item = | SearchSubPattern of constr_pattern_expr @@ -80,11 +80,11 @@ type searchable = | SearchAbout of (bool * search_about_item) list type locatable = - | LocateAny of reference or_by_notation - | LocateTerm of reference or_by_notation - | LocateLibrary of reference - | LocateModule of reference - | LocateOther of string * reference + | LocateAny of qualid or_by_notation + | LocateTerm of qualid or_by_notation + | LocateLibrary of qualid + | LocateModule of qualid + | LocateOther of string * qualid | LocateFile of string type showable = @@ -95,7 +95,7 @@ type showable = | ShowUniverses | ShowProofNames | ShowIntros of bool - | ShowMatch of reference + | ShowMatch of qualid type comment = | CommentConstr of constr_expr @@ -103,7 +103,7 @@ type comment = | CommentInt of int type reference_or_constr = Hints.reference_or_constr = - | HintsReference of reference + | HintsReference of qualid | HintsConstr of constr_expr [@@ocaml.deprecated "Please use [Hints.reference_or_constr]"] @@ -123,18 +123,18 @@ type hint_info_expr = Hints.hint_info_expr type hints_expr = Hints.hints_expr = | HintsResolve of (Hints.hint_info_expr * bool * Hints.reference_or_constr) list - | HintsResolveIFF of bool * reference list * int option + | HintsResolveIFF of bool * qualid list * int option | HintsImmediate of Hints.reference_or_constr list - | HintsUnfold of reference list - | HintsTransparency of reference list * bool - | HintsMode of reference * Hints.hint_mode list - | HintsConstructors of reference list + | HintsUnfold of qualid list + | HintsTransparency of qualid list * bool + | HintsMode of qualid * Hints.hint_mode list + | HintsConstructors of qualid list | HintsExtern of int * constr_expr option * Genarg.raw_generic_argument [@@ocaml.deprecated "Please use [Hints.hints_expr]"] type search_restriction = - | SearchInside of reference list - | SearchOutside of reference list + | SearchInside of qualid list + | SearchOutside of qualid list type rec_flag = bool (* true = Rec; false = NoRec *) type verbose_flag = bool (* true = Verbose; false = Silent *) @@ -159,7 +159,7 @@ type option_value = Goptions.option_value = type option_ref_value = | StringRefValue of string - | QualidRefValue of reference + | QualidRefValue of qualid (** Identifier and optional list of bound universes and constraints. *) @@ -222,9 +222,9 @@ type proof_end = | Proved of Proof_global.opacity_flag * lident option type scheme = - | InductionScheme of bool * reference or_by_notation * sort_expr - | CaseScheme of bool * reference or_by_notation * sort_expr - | EqualityScheme of reference or_by_notation + | InductionScheme of bool * qualid or_by_notation * sort_expr + | CaseScheme of bool * qualid or_by_notation * sort_expr + | EqualityScheme of qualid or_by_notation type section_subset_expr = | SsEmpty @@ -348,10 +348,10 @@ type nonrec vernac_expr = | VernacBeginSection of lident | VernacEndSegment of lident | VernacRequire of - reference option * export_flag option * reference list - | VernacImport of export_flag * reference list - | VernacCanonical of reference or_by_notation - | VernacCoercion of reference or_by_notation * + qualid option * export_flag option * qualid list + | VernacImport of export_flag * qualid list + | VernacCanonical of qualid or_by_notation + | VernacCoercion of qualid or_by_notation * class_rawexpr * class_rawexpr | VernacIdentityCoercion of lident * class_rawexpr * class_rawexpr | VernacNameSectionHypSet of lident * section_subset_expr @@ -367,9 +367,9 @@ type nonrec vernac_expr = | VernacContext of local_binder_expr list | VernacDeclareInstances of - (reference * Hints.hint_info_expr) list (* instances names, priorities and patterns *) + (qualid * Hints.hint_info_expr) list (* instances names, priorities and patterns *) - | VernacDeclareClass of reference (* inductive or definition name *) + | VernacDeclareClass of qualid (* inductive or definition name *) (* Modules and Module Types *) | VernacDeclareModule of bool option * lident * @@ -403,11 +403,11 @@ type nonrec vernac_expr = (* Commands *) | VernacCreateHintDb of string * bool - | VernacRemoveHints of string list * reference list + | VernacRemoveHints of string list * qualid list | VernacHints of string list * Hints.hints_expr | VernacSyntacticDefinition of lident * (Id.t list * constr_expr) * onlyparsing_flag - | VernacArguments of reference or_by_notation * + | VernacArguments of qualid or_by_notation * vernac_argument_status list (* Main arguments status list *) * (Name.t * vernac_implicit_status) list list (* Extra implicit status lists *) * int option (* Number of args to trigger reduction *) * @@ -416,9 +416,9 @@ type nonrec vernac_expr = `DefaultImplicits ] list | VernacReserve of simple_binder list | VernacGeneralizable of (lident list) option - | VernacSetOpacity of (Conv_oracle.level * reference or_by_notation list) + | VernacSetOpacity of (Conv_oracle.level * qualid or_by_notation list) | VernacSetStrategy of - (Conv_oracle.level * reference or_by_notation list) list + (Conv_oracle.level * qualid or_by_notation list) list | VernacUnsetOption of export_flag * Goptions.option_name | VernacSetOption of export_flag * Goptions.option_name * option_value | VernacAddOption of Goptions.option_name * option_ref_value list |