[coqlib] Move `Coqlib` to `library/`.

We move Coqlib to library in preparation for the late binding of
Gallina-level references. Placing `Coqlib` in `library/` is convenient
as some components such as pretyping need to depend on it.

By moving we lose the ability to locate references by syntactic
abbreviations, but IMHO it makes to require ML code to refer to
a true constant instead of an abbreviation/notation.

Unfortunately this change means that we break the `Coqlib`
API (providing a compatibility function is not possible), however we
do so for a good reason.

The main changes are:

- move `Coqlib` to `library/`.
- remove reference -> term from `Coqlib`. In particular, clients will
  have different needs with regards to universes/evar_maps, so we
  force them to call the (not very safe) `Universes.constr_of_global`
  explicitly so the users are marked.
- move late binding of impossible case from `Termops` to
  `pretying/Evarconv`. Remove hook.
- `Coqlib.find_reference` doesn't support syntactic abbreviations
  anymore.
- remove duplication of `Coqlib` code in `Program`.
- remove duplication of `Coqlib` code in `Ltac.Rewrite`.
- A special note about bug 5066 and commit 6e87877 . This case
  illustrates the danger of duplication in the code base; the solution
  chosen there was to transform the not-found anomaly into an error
  message, however the general policy was far from clear. The long
  term solution is indeed make `find_reference` emit `Not_found` and
  let the client handle the error maybe non-fatally. (so they can test
  for constants.

1 files changed, 383 insertions, 0 deletions

diff --git a/library/coqlib.ml b/library/coqlib.ml
new file mode 100644
index 000000000..955ff4c08
--- /dev/null
+++ b/library/coqlib.ml
@@ -0,0 +1,383 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open CErrors
+open Util
+open Pp
+open Names
+open Libnames
+open Globnames
+open Nametab
+
+let coq = Nameops.coq_string (* "Coq" *)
+
+(************************************************************************)
+(* Generic functions to find Coq objects *)
+
+type message = string
+
+let make_dir l = DirPath.make (List.rev_map Id.of_string l)
+
+let find_reference locstr dir s =
+  let dp = make_dir dir in
+  let sp = Libnames.make_path dp (Id.of_string s) in
+  try Nametab.global_of_path sp
+  with Not_found ->
+    (* Following bug 5066 we are more permissive with the handling
+       of not found errors here *)
+    user_err ~hdr:locstr
+      Pp.(str "cannot find " ++ Libnames.pr_path sp ++
+          str "; maybe library " ++ Libnames.pr_dirpath dp ++
+          str " has to be required first.")
+
+let coq_reference locstr dir s = find_reference locstr (coq::dir) s
+
+let has_suffix_in_dirs dirs ref =
+  let dir = dirpath (path_of_global ref) in
+  List.exists (fun d -> is_dirpath_prefix_of d dir) dirs
+
+let gen_reference_in_modules locstr dirs s =
+  let dirs = List.map make_dir dirs in
+  let qualid = qualid_of_string s in
+  let all = Nametab.locate_all qualid in
+  let all = List.sort_uniquize RefOrdered_env.compare all in
+  let these = List.filter (has_suffix_in_dirs dirs) all in
+  match these with
+    | [x] -> x
+    | [] ->
+	anomaly ~label:locstr (str "cannot find " ++ str s ++
+	str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++
+	prlist_with_sep pr_comma pr_dirpath dirs)
+    | l ->
+      anomaly ~label:locstr
+	(str "ambiguous name " ++ str s ++ str " can represent " ++
+	   prlist_with_sep pr_comma
+	   (fun x -> Libnames.pr_path (Nametab.path_of_global x)) l ++
+	   str " in module" ++ str (if List.length dirs > 1 then "s " else " ") ++
+	   prlist_with_sep pr_comma pr_dirpath dirs)
+
+(* For tactics/commands requiring vernacular libraries *)
+
+let check_required_library d =
+  let dir = make_dir d in
+  if Library.library_is_loaded dir then ()
+  else
+    let in_current_dir = match Lib.current_mp () with
+      | MPfile dp -> DirPath.equal dir dp
+      | _ -> false
+    in
+    if not in_current_dir then
+(* Loading silently ...
+    let m, prefix = List.sep_last d' in
+    read_library
+     (Loc.ghost,make_qualid (DirPath.make (List.rev prefix)) m)
+*)
+(* or failing ...*)
+      user_err ~hdr:"Coqlib.check_required_library"
+        (str "Library " ++ pr_dirpath dir ++ str " has to be required first.")
+
+(************************************************************************)
+(* Specific Coq objects *)
+
+let init_reference dir s =
+  let d = coq::"Init"::dir in
+  check_required_library d; find_reference "Coqlib" d s
+
+let logic_reference dir s =
+  let d = coq::"Logic"::dir in
+  check_required_library d; find_reference "Coqlib" d s
+
+let arith_dir = [coq;"Arith"]
+let arith_modules = [arith_dir]
+
+let numbers_dir = [coq;"Numbers"]
+let parith_dir = [coq;"PArith"]
+let narith_dir = [coq;"NArith"]
+let zarith_dir = [coq;"ZArith"]
+
+let zarith_base_modules = [numbers_dir;parith_dir;narith_dir;zarith_dir]
+
+let init_dir = [coq;"Init"]
+let init_modules = [
+  init_dir@["Datatypes"];
+  init_dir@["Logic"];
+  init_dir@["Specif"];
+  init_dir@["Logic_Type"];
+  init_dir@["Nat"];
+  init_dir@["Peano"];
+  init_dir@["Wf"]
+]
+
+let prelude_module_name = init_dir@["Prelude"]
+let prelude_module = make_dir prelude_module_name
+
+let logic_module_name = init_dir@["Logic"]
+let logic_module = make_dir logic_module_name
+
+let logic_type_module_name = init_dir@["Logic_Type"]
+let logic_type_module = make_dir logic_type_module_name
+
+let datatypes_module_name = init_dir@["Datatypes"]
+let datatypes_module = make_dir datatypes_module_name
+
+let jmeq_module_name = [coq;"Logic";"JMeq"]
+let jmeq_module = make_dir jmeq_module_name
+
+(* TODO: temporary hack. Works only if the module isn't an alias *)
+let make_ind dir id = Globnames.encode_mind dir (Id.of_string id)
+let make_con dir id = Globnames.encode_con dir (Id.of_string id)
+
+(** Identity *)
+
+let id = make_con datatypes_module "idProp"
+let type_of_id = make_con datatypes_module "IDProp"
+
+(** Natural numbers *)
+let nat_kn = make_ind datatypes_module "nat"
+let nat_path = Libnames.make_path datatypes_module (Id.of_string "nat")
+
+let glob_nat = IndRef (nat_kn,0)
+
+let path_of_O = ((nat_kn,0),1)
+let path_of_S = ((nat_kn,0),2)
+let glob_O = ConstructRef path_of_O
+let glob_S = ConstructRef path_of_S
+
+(** Booleans *)
+let bool_kn = make_ind datatypes_module "bool"
+
+let glob_bool = IndRef (bool_kn,0)
+
+let path_of_true = ((bool_kn,0),1)
+let path_of_false = ((bool_kn,0),2)
+let glob_true  = ConstructRef path_of_true
+let glob_false  = ConstructRef path_of_false
+
+(** Equality *)
+let eq_kn = make_ind logic_module "eq"
+let glob_eq = IndRef (eq_kn,0)
+
+let identity_kn = make_ind datatypes_module "identity"
+let glob_identity = IndRef (identity_kn,0)
+
+let jmeq_kn = make_ind jmeq_module "JMeq"
+let glob_jmeq = IndRef (jmeq_kn,0)
+
+type coq_sigma_data = {
+  proj1 : global_reference;
+  proj2 : global_reference;
+  elim  : global_reference;
+  intro : global_reference;
+  typ   : global_reference }
+
+type coq_bool_data  = {
+  andb : global_reference;
+  andb_prop : global_reference;
+  andb_true_intro : global_reference}
+
+let build_bool_type () =
+  { andb =  init_reference ["Datatypes"] "andb";
+    andb_prop =  init_reference ["Datatypes"] "andb_prop";
+    andb_true_intro =  init_reference ["Datatypes"] "andb_true_intro" }
+
+let build_sigma_set () = anomaly (Pp.str "Use build_sigma_type")
+
+let build_sigma_type () =
+  { proj1 = init_reference ["Specif"] "projT1";
+    proj2 = init_reference ["Specif"] "projT2";
+    elim = init_reference ["Specif"] "sigT_rect";
+    intro = init_reference ["Specif"] "existT";
+    typ = init_reference ["Specif"] "sigT" }
+
+let build_sigma () =
+  { proj1 = init_reference ["Specif"] "proj1_sig";
+    proj2 = init_reference ["Specif"] "proj2_sig";
+    elim = init_reference ["Specif"] "sig_rect";
+    intro = init_reference ["Specif"] "exist";
+    typ = init_reference ["Specif"] "sig" }
+
+
+let build_prod () =
+  { proj1 = init_reference ["Datatypes"] "fst";
+    proj2 = init_reference ["Datatypes"] "snd";
+    elim = init_reference ["Datatypes"] "prod_rec";
+    intro = init_reference ["Datatypes"] "pair";
+    typ = init_reference ["Datatypes"] "prod" }
+
+(* Equalities *)
+type coq_eq_data = {
+  eq   : global_reference;
+  ind  : global_reference;
+  refl : global_reference;
+  sym  : global_reference;
+  trans: global_reference;
+  congr: global_reference }
+
+(* Data needed for discriminate and injection *)
+type coq_inversion_data = {
+  inv_eq   : global_reference; (* : forall params, t -> Prop *)
+  inv_ind  : global_reference; (* : forall params P y, eq params y -> P y *)
+  inv_congr: global_reference  (* : forall params B (f:t->B) y, eq params y -> f c=f y *)
+}
+
+let lazy_init_reference dir id = lazy (init_reference dir id)
+let lazy_logic_reference dir id = lazy (logic_reference dir id)
+
+(* Leibniz equality on Type *)
+
+let coq_eq_eq = lazy_init_reference ["Logic"] "eq"
+let coq_eq_refl = lazy_init_reference ["Logic"] "eq_refl"
+let coq_eq_ind = lazy_init_reference ["Logic"] "eq_ind"
+let coq_eq_congr = lazy_init_reference ["Logic"] "f_equal"
+let coq_eq_sym  = lazy_init_reference ["Logic"] "eq_sym"
+let coq_eq_trans  = lazy_init_reference ["Logic"] "eq_trans"
+let coq_f_equal2 = lazy_init_reference ["Logic"] "f_equal2"
+let coq_eq_congr_canonical =
+  lazy_init_reference ["Logic"] "f_equal_canonical_form"
+
+let build_coq_eq_data () =
+  let _ = check_required_library logic_module_name in {
+  eq = Lazy.force coq_eq_eq;
+  ind = Lazy.force coq_eq_ind;
+  refl = Lazy.force coq_eq_refl;
+  sym = Lazy.force coq_eq_sym;
+  trans = Lazy.force coq_eq_trans;
+  congr = Lazy.force coq_eq_congr }
+
+let build_coq_eq () = Lazy.force coq_eq_eq
+let build_coq_eq_refl () = Lazy.force coq_eq_refl
+let build_coq_eq_sym () = Lazy.force coq_eq_sym
+let build_coq_f_equal2 () = Lazy.force coq_f_equal2
+
+let build_coq_inversion_eq_data () =
+  let _ = check_required_library logic_module_name in {
+  inv_eq = Lazy.force coq_eq_eq;
+  inv_ind = Lazy.force coq_eq_ind;
+  inv_congr = Lazy.force coq_eq_congr_canonical }
+
+(* Heterogenous equality on Type *)
+
+let coq_jmeq_eq = lazy_logic_reference ["JMeq"] "JMeq"
+let coq_jmeq_hom = lazy_logic_reference ["JMeq"] "JMeq_hom"
+let coq_jmeq_refl = lazy_logic_reference ["JMeq"] "JMeq_refl"
+let coq_jmeq_ind = lazy_logic_reference ["JMeq"] "JMeq_ind"
+let coq_jmeq_sym  = lazy_logic_reference ["JMeq"] "JMeq_sym"
+let coq_jmeq_congr  = lazy_logic_reference ["JMeq"] "JMeq_congr"
+let coq_jmeq_trans  = lazy_logic_reference ["JMeq"] "JMeq_trans"
+let coq_jmeq_congr_canonical =
+  lazy_logic_reference ["JMeq"] "JMeq_congr_canonical_form"
+
+let build_coq_jmeq_data () =
+  let _ = check_required_library jmeq_module_name in {
+  eq = Lazy.force coq_jmeq_eq;
+  ind = Lazy.force coq_jmeq_ind;
+  refl = Lazy.force coq_jmeq_refl;
+  sym = Lazy.force coq_jmeq_sym;
+  trans = Lazy.force coq_jmeq_trans;
+  congr = Lazy.force coq_jmeq_congr }
+
+let build_coq_inversion_jmeq_data () =
+  let _ = check_required_library logic_module_name in {
+  inv_eq = Lazy.force coq_jmeq_hom;
+  inv_ind = Lazy.force coq_jmeq_ind;
+  inv_congr = Lazy.force coq_jmeq_congr_canonical }
+
+(* Specif *)
+let coq_sumbool  = lazy_init_reference ["Specif"] "sumbool"
+
+let build_coq_sumbool () = Lazy.force coq_sumbool
+
+(* Equality on Type as a Type *)
+let coq_identity_eq = lazy_init_reference ["Datatypes"] "identity"
+let coq_identity_refl = lazy_init_reference ["Datatypes"] "identity_refl"
+let coq_identity_ind = lazy_init_reference ["Datatypes"] "identity_ind"
+let coq_identity_congr = lazy_init_reference ["Logic_Type"] "identity_congr"
+let coq_identity_sym = lazy_init_reference ["Logic_Type"] "identity_sym"
+let coq_identity_trans = lazy_init_reference ["Logic_Type"] "identity_trans"
+let coq_identity_congr_canonical = lazy_init_reference ["Logic_Type"] "identity_congr_canonical_form"
+
+let build_coq_identity_data () =
+  let _ = check_required_library datatypes_module_name in {
+  eq = Lazy.force coq_identity_eq;
+  ind = Lazy.force coq_identity_ind;
+  refl = Lazy.force coq_identity_refl;
+  sym = Lazy.force coq_identity_sym;
+  trans = Lazy.force coq_identity_trans;
+  congr = Lazy.force coq_identity_congr }
+
+let build_coq_inversion_identity_data () =
+  let _ = check_required_library datatypes_module_name in
+  let _ = check_required_library logic_type_module_name in {
+  inv_eq = Lazy.force coq_identity_eq;
+  inv_ind = Lazy.force coq_identity_ind;
+  inv_congr = Lazy.force coq_identity_congr_canonical }
+
+(* Equality to true *)
+let coq_eq_true_eq = lazy_init_reference ["Datatypes"] "eq_true"
+let coq_eq_true_ind = lazy_init_reference ["Datatypes"] "eq_true_ind"
+let coq_eq_true_congr = lazy_init_reference ["Logic"] "eq_true_congr"
+
+let build_coq_inversion_eq_true_data () =
+  let _ = check_required_library datatypes_module_name in
+  let _ = check_required_library logic_module_name in {
+  inv_eq = Lazy.force coq_eq_true_eq;
+  inv_ind = Lazy.force coq_eq_true_ind;
+  inv_congr = Lazy.force coq_eq_true_congr }
+
+(* The False proposition *)
+let coq_False  = lazy_init_reference ["Logic"] "False"
+
+(* The True proposition and its unique proof *)
+let coq_True   = lazy_init_reference ["Logic"] "True"
+let coq_I      = lazy_init_reference ["Logic"] "I"
+
+(* Connectives *)
+let coq_not = lazy_init_reference ["Logic"] "not"
+let coq_and = lazy_init_reference ["Logic"] "and"
+let coq_conj = lazy_init_reference ["Logic"] "conj"
+let coq_or = lazy_init_reference ["Logic"] "or"
+let coq_ex = lazy_init_reference ["Logic"] "ex"
+let coq_iff = lazy_init_reference ["Logic"] "iff"
+
+let coq_iff_left_proj  = lazy_init_reference ["Logic"] "proj1"
+let coq_iff_right_proj = lazy_init_reference ["Logic"] "proj2"
+
+(* Runtime part *)
+let build_coq_True ()  = Lazy.force coq_True
+let build_coq_I ()     = Lazy.force coq_I
+
+let build_coq_False () = Lazy.force coq_False
+let build_coq_not ()   = Lazy.force coq_not
+let build_coq_and ()   = Lazy.force coq_and
+let build_coq_conj ()  = Lazy.force coq_conj
+let build_coq_or ()    = Lazy.force coq_or
+let build_coq_ex ()    = Lazy.force coq_ex
+let build_coq_iff ()   = Lazy.force coq_iff
+
+let build_coq_iff_left_proj ()  = Lazy.force coq_iff_left_proj
+let build_coq_iff_right_proj () = Lazy.force coq_iff_right_proj
+
+
+(* The following is less readable but does not depend on parsing *)
+let coq_eq_ref      = lazy (init_reference ["Logic"] "eq")
+let coq_identity_ref = lazy (init_reference ["Datatypes"] "identity")
+let coq_jmeq_ref     = lazy (find_reference "Coqlib" [coq;"Logic";"JMeq"] "JMeq")
+let coq_eq_true_ref = lazy (find_reference "Coqlib" [coq;"Init";"Datatypes"] "eq_true")
+let coq_existS_ref  = lazy (anomaly (Pp.str "use coq_existT_ref"))
+let coq_existT_ref  = lazy (init_reference ["Specif"] "existT")
+let coq_exist_ref  = lazy (init_reference ["Specif"] "exist")
+let coq_not_ref     = lazy (init_reference ["Logic"] "not")
+let coq_False_ref   = lazy (init_reference ["Logic"] "False")
+let coq_sumbool_ref = lazy (init_reference ["Specif"] "sumbool")
+let coq_sig_ref = lazy (init_reference ["Specif"] "sig")
+let coq_or_ref     = lazy (init_reference ["Logic"] "or")
+let coq_iff_ref    = lazy (init_reference ["Logic"] "iff")
+
+(* Deprecated *)
+let gen_reference = coq_reference
+