[coqlib] Rebindable Coqlib namespace.

We refactor the `Coqlib` API to locate objects over a namespace
`module.object.property`.

This introduces the vernacular command `Register g as n` to expose the
Coq constant `g` under the name `n` (through the `register_ref`
function). The constant can then be dynamically located using the
`lib_ref` function.

Co-authored-by: Emilio Jesús Gallego Arias <e+git@x80.org>
Co-authored-by: Maxime Dénès <mail@maximedenes.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>

2 files changed, 42 insertions, 41 deletions

diff --git a/plugins/btauto/Reflect.v b/plugins/btauto/Reflect.v
index d82e8ae8ad..4cde08872f 100644
--- a/plugins/btauto/Reflect.v
+++ b/plugins/btauto/Reflect.v
@@ -396,3 +396,16 @@ lazymatch goal with
   end
 | _ => fail "Cannot recognize a boolean equality"
 end. *)
+
+Register formula_var as plugins.btauto.f_var.
+Register formula_btm as plugins.btauto.f_btm.
+Register formula_top as plugins.btauto.f_top.
+Register formula_cnj as plugins.btauto.f_cnj.
+Register formula_dsj as plugins.btauto.f_dsj.
+Register formula_neg as plugins.btauto.f_neg.
+Register formula_xor as plugins.btauto.f_xor.
+Register formula_ifb as plugins.btauto.f_ifb.
+
+Register formula_eval as plugins.btauto.eval.
+Register boolean_witness as plugins.btauto.witness.
+Register reduce_poly_of_formula_sound_alt as plugins.btauto.soundness.
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index b0f97c59b8..ac0a875229 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -12,17 +12,7 @@ open Constr
 
 let contrib_name = "btauto"
 
-let init_constant dir s =
-  let find_constant contrib dir s =
-    UnivGen.constr_of_global (Coqlib.find_reference contrib dir s)
-  in
-  find_constant contrib_name dir s
-
-let get_constant dir s = lazy (UnivGen.constr_of_global @@ Coqlib.coq_reference contrib_name dir s)
-
-let get_inductive dir s =
-  let glob_ref () = Coqlib.find_reference contrib_name ("Coq" :: dir) s in
-  Lazy.from_fun (fun () -> Globnames.destIndRef (glob_ref ()))
+let bt_lib_constr n = lazy (UnivGen.constr_of_global @@ Coqlib.lib_ref n)
 
 let decomp_term sigma (c : Constr.t) =
   Constr.kind (EConstr.Unsafe.to_constr (Termops.strip_outer_cast sigma (EConstr.of_constr c)))
@@ -31,11 +21,11 @@ let lapp c v  = Constr.mkApp (Lazy.force c, v)
 
 let (===) = Constr.equal
 
+
 module CoqList = struct
-  let path = ["Init"; "Datatypes"]
-  let typ = get_constant path "list"
-  let _nil = get_constant path "nil"
-  let _cons = get_constant path "cons"
+  let typ  =  bt_lib_constr "core.list.type"
+  let _nil =  bt_lib_constr "core.list.nil"
+  let _cons = bt_lib_constr "core.list.cons"
 
   let cons ty h t = lapp _cons [|ty; h ; t|]
   let nil ty = lapp _nil [|ty|]
@@ -47,11 +37,10 @@ module CoqList = struct
 end
 
 module CoqPositive = struct
-  let path = ["Numbers"; "BinNums"]
-  let typ = get_constant path "positive"
-  let _xH = get_constant path "xH"
-  let _xO = get_constant path "xO"
-  let _xI = get_constant path "xI"
+  let typ = bt_lib_constr "num.pos.type"
+  let _xH = bt_lib_constr "num.pos.xH"
+  let _xO = bt_lib_constr "num.pos.xO"
+  let _xI = bt_lib_constr "num.pos.xI"
 
   (* A coq nat from an int *)
   let rec of_int n =
@@ -91,14 +80,14 @@ end
 
 module Bool = struct
 
-  let typ = get_constant ["Init"; "Datatypes"] "bool"
-  let ind = get_inductive ["Init"; "Datatypes"] "bool"
-  let trueb = get_constant ["Init"; "Datatypes"] "true"
-  let falseb = get_constant ["Init"; "Datatypes"] "false"
-  let andb = get_constant ["Init"; "Datatypes"] "andb"
-  let orb = get_constant ["Init"; "Datatypes"] "orb"
-  let xorb = get_constant ["Init"; "Datatypes"] "xorb"
-  let negb = get_constant ["Init"; "Datatypes"] "negb"
+  let ind    = lazy (Globnames.destIndRef (Coqlib.lib_ref "core.bool.type"))
+  let typ    = bt_lib_constr "core.bool.type"
+  let trueb  = bt_lib_constr "core.bool.true"
+  let falseb = bt_lib_constr "core.bool.false"
+  let andb   = bt_lib_constr "core.bool.andb"
+  let orb    = bt_lib_constr "core.bool.orb"
+  let xorb   = bt_lib_constr "core.bool.xorb"
+  let negb   = bt_lib_constr "core.bool.negb"
 
   type t =
   | Var of int
@@ -150,21 +139,20 @@ module Btauto = struct
 
   open Pp
 
-  let eq = get_constant ["Init"; "Logic"]  "eq"
-
-  let f_var = get_constant ["btauto"; "Reflect"] "formula_var"
-  let f_btm = get_constant ["btauto"; "Reflect"] "formula_btm"
-  let f_top = get_constant ["btauto"; "Reflect"] "formula_top"
-  let f_cnj = get_constant ["btauto"; "Reflect"] "formula_cnj"
-  let f_dsj = get_constant ["btauto"; "Reflect"] "formula_dsj"
-  let f_neg = get_constant ["btauto"; "Reflect"] "formula_neg"
-  let f_xor = get_constant ["btauto"; "Reflect"] "formula_xor"
-  let f_ifb = get_constant ["btauto"; "Reflect"] "formula_ifb"
+  let eq = bt_lib_constr "core.eq.type"
 
-  let eval = get_constant ["btauto"; "Reflect"] "formula_eval"
-  let witness = get_constant ["btauto"; "Reflect"] "boolean_witness"
+  let f_var = bt_lib_constr "plugins.btauto.f_var"
+  let f_btm = bt_lib_constr "plugins.btauto.f_btm"
+  let f_top = bt_lib_constr "plugins.btauto.f_top"
+  let f_cnj = bt_lib_constr "plugins.btauto.f_cnj"
+  let f_dsj = bt_lib_constr "plugins.btauto.f_dsj"
+  let f_neg = bt_lib_constr "plugins.btauto.f_neg"
+  let f_xor = bt_lib_constr "plugins.btauto.f_xor"
+  let f_ifb = bt_lib_constr "plugins.btauto.f_ifb"
 
-  let soundness = get_constant ["btauto"; "Reflect"] "reduce_poly_of_formula_sound_alt"
+  let eval = bt_lib_constr "plugins.btauto.eval"
+  let witness = bt_lib_constr "plugins.btauto.witness"
+  let soundness = bt_lib_constr "plugins.btauto.soundness"
 
   let rec convert = function
   | Bool.Var n -> lapp f_var [|CoqPositive.of_int n|]