From 8ac6145d5cc14823df48698a755d8adf048f026c Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 2 Oct 2017 12:22:32 +0200 Subject: [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 Co-authored-by: Maxime Dénès Co-authored-by: Vincent Laporte --- pretyping/program.ml | 54 +++++++++++++++++++++++++++------------------------- 1 file changed, 28 insertions(+), 26 deletions(-) (limited to 'pretyping/program.ml') diff --git a/pretyping/program.ml b/pretyping/program.ml index 8cfb7966cb..bbabbefdc3 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -11,8 +11,6 @@ open CErrors open Util -let init_reference dir s () = Coqlib.coq_reference "Program" dir s - let papp evdref r args = let open EConstr in let gr = delayed_force r in @@ -20,44 +18,48 @@ let papp evdref r args = evdref := evd; mkApp (hd, args) -let sig_typ = init_reference ["Init"; "Specif"] "sig" -let sig_intro = init_reference ["Init"; "Specif"] "exist" -let sig_proj1 = init_reference ["Init"; "Specif"] "proj1_sig" - -let sigT_typ = init_reference ["Init"; "Specif"] "sigT" -let sigT_intro = init_reference ["Init"; "Specif"] "existT" -let sigT_proj1 = init_reference ["Init"; "Specif"] "projT1" -let sigT_proj2 = init_reference ["Init"; "Specif"] "projT2" - -let prod_typ = init_reference ["Init"; "Datatypes"] "prod" -let prod_intro = init_reference ["Init"; "Datatypes"] "pair" -let prod_proj1 = init_reference ["Init"; "Datatypes"] "fst" -let prod_proj2 = init_reference ["Init"; "Datatypes"] "snd" +let sig_typ () = Coqlib.lib_ref "core.sig.type" +let sig_intro () = Coqlib.lib_ref "core.sig.intro" +let sig_proj1 () = Coqlib.lib_ref "core.sig.proj1" +(* let sig_proj2 () = Coqlib.lib_ref "core.sig.proj2" *) -let coq_eq_ind = init_reference ["Init"; "Logic"] "eq" -let coq_eq_refl = init_reference ["Init"; "Logic"] "eq_refl" -let coq_eq_refl_ref = init_reference ["Init"; "Logic"] "eq_refl" -let coq_eq_rect = init_reference ["Init"; "Logic"] "eq_rect" +let sigT_typ () = Coqlib.lib_ref "core.sigT.type" +let sigT_intro () = Coqlib.lib_ref "core.sigT.intro" +let sigT_proj1 () = Coqlib.lib_ref "core.sigT.proj1" +let sigT_proj2 () = Coqlib.lib_ref "core.sigT.proj2" -let coq_JMeq_ind = init_reference ["Logic";"JMeq"] "JMeq" -let coq_JMeq_refl = init_reference ["Logic";"JMeq"] "JMeq_refl" +let prod_typ () = Coqlib.lib_ref "core.prod.type" +let prod_intro () = Coqlib.lib_ref "core.prod.intro" +let prod_proj1 () = Coqlib.lib_ref "core.prod.proj1" +let prod_proj2 () = Coqlib.lib_ref "core.prod.proj2" -let coq_not = init_reference ["Init";"Logic"] "not" -let coq_and = init_reference ["Init";"Logic"] "and" +let coq_eq_ind () = Coqlib.lib_ref "core.eq.type" +let coq_eq_refl () = Coqlib.lib_ref "core.eq.refl" +let coq_eq_refl_ref () = Coqlib.lib_ref "core.eq.refl" +let coq_eq_rect () = Coqlib.lib_ref "core.eq.rect" let mk_coq_not sigma x = - let sigma, notc = Evarutil.new_global sigma (coq_not ()) in + let sigma, notc = Evarutil.new_global sigma Coqlib.(lib_ref "core.not.type") in sigma, EConstr.mkApp (notc, [| x |]) +let coq_JMeq_ind () = + try Coqlib.lib_ref "core.JMeq.type" + with Not_found -> + user_err (Pp.str "cannot find Coq.Logic.JMeq.JMeq; maybe library Coq.Logic.JMeq has to be required first.") +let coq_JMeq_refl () = Coqlib.lib_ref "core.JMeq.refl" + +(* let coq_not () = Universes.constr_of_global @@ Coqlib.lib_ref "core.not.type" *) +(* let coq_and () = Universes.constr_of_global @@ Coqlib.lib_ref "core.and.type" *) + let unsafe_fold_right f = function hd :: tl -> List.fold_right f tl hd | [] -> invalid_arg "unsafe_fold_right" let mk_coq_and sigma l = - let sigma, and_typ = Evarutil.new_global sigma (coq_and ()) in + let sigma, and_typ = Evarutil.new_global sigma Coqlib.(lib_ref "core.and.type") in sigma, unsafe_fold_right (fun c conj -> - EConstr.mkApp (and_typ, [| c ; conj |])) + EConstr.(mkApp (and_typ, [| c ; conj |]))) l (* true = transparent by default, false = opaque if possible *) -- cgit v1.2.3