open ProofEngineTypes
open UriManager
+open HelmLibraryObjects
+
(** DEBUGGING *)
(** perform debugging output? *)
uniformity of invocation of "mkXXX" functions.
*)
-let eqt_uri = uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind"
-let refl_eqt_uri = (eqt_uri, 0, 1)
let equality_is_a_congruence_A =
- uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/A.var"
+ uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var"
let equality_is_a_congruence_x =
- uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/x.var"
+ uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var"
let equality_is_a_congruence_y =
- uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/y.var"
-let sym_eqt_uri = uri_of_string "cic:/Coq/Init/Logic_Type/sym_eqT.con"
-let bool_uri = uri_of_string "cic:/Coq/Init/Datatypes/bool.ind"
-let true_uri = (bool_uri, 0, 1)
-let false_uri = (bool_uri, 0, 2)
-
-let r_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/R.con"
-let rplus_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con"
-let rmult_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/Rmult.con"
-let ropp_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/Ropp.con"
-let r0_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con"
-let r1_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con"
-let rtheory_uri = uri_of_string "cic:/Coq/Reals/Rbase/RTheory.con"
+ uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var"
let apolynomial_uri =
uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial.ind"
*)
let uri_of_proof ~proof:(uri, _, _, _) = uri
- (**
- @param metano meta list index
- @param metasenv meta list (environment)
- @raise Failure if metano is not found in metasenv
- @return conjecture corresponding to metano in metasenv
- *)
-let conj_of_metano metano =
- try
- List.find (function (m, _, _) -> m = metano)
- with Not_found ->
- failwith (
- "Ring.conj_of_metano: " ^
- (string_of_int metano) ^ " no such meta")
-
(**
@param status current proof engine status
@raise Failure if proof is None
*)
let context_of_status ~status:(proof, goal as status) =
let metasenv = metasenv_of_status ~status:status in
- let _, context, _ = List.find (function (m,_,_) -> m=goal) metasenv in
+ let _, context, _ = CicUtil.lookup_meta goal metasenv in
context
(** CIC TERM CONSTRUCTORS *)
*)
let ringable =
let is_equality = function
- | Cic.MutInd (uri, 0, []) when (eq uri eqt_uri) -> true
+ | Cic.MutInd (uri, 0, []) when (eq uri Logic.eq_URI) -> true
| _ -> false
in
let is_real = function
- | Cic.Const (uri, _) when (eq uri r_uri) -> true
+ | Cic.Const (uri, _) when (eq uri Reals.r_URI) -> true
| _ -> false
in
function
@return a cic term representing the variable map containing vars variables
*)
let btree_of_array ~vars =
- let r = mkConst r_uri [] in (* cic objects *)
+ let r = Reals.r in
let empty_vm_r = mkCtor empty_vm_uri [quote_varmap_A_uri,r] in
let node_vm_r = mkCtor node_vm_uri [quote_varmap_A_uri,r] in
let size = Array.length vars in
let rec aux = function (* TODO not tail recursive *)
(* "bop" -> binary operator | "uop" -> unary operator *)
| Cic.Appl (bop::t1::t2::[])
- when (cic_is_const ~uri:(Some rplus_uri) bop) -> (* +. *)
+ when (cic_is_const ~uri:(Some Reals.rplus_URI) bop) -> (* +. *)
Cic.Appl [mkCtor applus_uri []; aux t1; aux t2]
| Cic.Appl (bop::t1::t2::[])
- when (cic_is_const ~uri:(Some rmult_uri) bop) -> (* *. *)
+ when (cic_is_const ~uri:(Some Reals.rmult_URI) bop) -> (* *. *)
Cic.Appl [mkCtor apmult_uri []; aux t1; aux t2]
| Cic.Appl (uop::t::[])
- when (cic_is_const ~uri:(Some ropp_uri) uop) -> (* ~-. *)
+ when (cic_is_const ~uri:(Some Reals.ropp_URI) uop) -> (* ~-. *)
Cic.Appl [mkCtor apopp_uri []; aux t]
- | t when (cic_is_const ~uri:(Some r0_uri) t) -> (* 0. *)
+ | t when (cic_is_const ~uri:(Some Reals.r0_URI) t) -> (* 0. *)
mkCtor ap0_uri []
- | t when (cic_is_const ~uri:(Some r1_uri) t) -> (* 1. *)
+ | t when (cic_is_const ~uri:(Some Reals.r1_URI) t) -> (* 1. *)
mkCtor ap1_uri []
| t -> (* variable *)
try
at is the abstract term built from t, t is a single member of aterms
*)
let build_segments ~terms =
- let r = mkConst r_uri [] in (* cic objects *)
- let rplus = mkConst rplus_uri [] in
- let rmult = mkConst rmult_uri [] in
- let ropp = mkConst ropp_uri [] in
- let r1 = mkConst r1_uri [] in
- let r0 = mkConst r0_uri [] in
let theory_args_subst varmap =
- [abstract_rings_A_uri, r ;
- abstract_rings_Aplus_uri, rplus ;
- abstract_rings_Amult_uri, rmult ;
- abstract_rings_Aone_uri, r1 ;
- abstract_rings_Azero_uri, r0 ;
- abstract_rings_Aopp_uri, ropp ;
+ [abstract_rings_A_uri, Reals.r ;
+ abstract_rings_Aplus_uri, Reals.rplus ;
+ abstract_rings_Amult_uri, Reals.rmult ;
+ abstract_rings_Aone_uri, Reals.r1 ;
+ abstract_rings_Azero_uri, Reals.r0 ;
+ abstract_rings_Aopp_uri, Reals.ropp ;
abstract_rings_vm_uri, varmap] in
let theory_args_subst' eq varmap t =
- [abstract_rings_A_uri, r ;
- abstract_rings_Aplus_uri, rplus ;
- abstract_rings_Amult_uri, rmult ;
- abstract_rings_Aone_uri, r1 ;
- abstract_rings_Azero_uri, r0 ;
- abstract_rings_Aopp_uri, ropp ;
+ [abstract_rings_A_uri, Reals.r ;
+ abstract_rings_Aplus_uri, Reals.rplus ;
+ abstract_rings_Amult_uri, Reals.rmult ;
+ abstract_rings_Aone_uri, Reals.r1 ;
+ abstract_rings_Azero_uri, Reals.r0 ;
+ abstract_rings_Aopp_uri, Reals.ropp ;
abstract_rings_Aeq_uri, eq ;
abstract_rings_vm_uri, varmap ;
abstract_rings_T_uri, t] in
let apolynomial_normalize = mkConst apolynomial_normalize_uri [] in
let apolynomial_normalize_ok eq varmap t =
mkConst apolynomial_normalize_ok_uri (theory_args_subst' eq varmap t) in
- let rtheory = mkConst rtheory_uri [] in
let lxy_false = (** Cic funcion "fun (x,y):R -> false" *)
- Cic.Lambda (Cic.Anonymous, r,
- Cic.Lambda (Cic.Anonymous, r,
- mkCtor false_uri []))
+ Cic.Lambda (Cic.Anonymous, Reals.r,
+ Cic.Lambda (Cic.Anonymous, Reals.r, Datatypes.falseb))
in
let (aterms, varmap) = abstract_poly ~terms in (* abstract polys *)
List.map (* build ring segments *)
Cic.Appl [interp_ap varmap ; t],
Cic.Appl (
[interp_sacs varmap ; Cic.Appl [apolynomial_normalize; t]]),
- Cic.Appl [apolynomial_normalize_ok lxy_false varmap rtheory ; t]
+ Cic.Appl [apolynomial_normalize_ok lxy_false varmap Reals.rtheory ; t]
) aterms
| (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left"
in
let (_, metasenv, _, _) = proof in
- let (_, context, _) = conj_of_metano goal metasenv in
+ let (_, context, _) = CicUtil.lookup_meta goal metasenv in
let proof',goal' = aux count context status in
assert (goal = goal') ;
proof',[goal']
*)
let ring_tac ~status:((proof, goal) as status) =
warn "in Ring tactic";
- let eqt = mkMutInd (eqt_uri, 0) [] in
- let r = mkConst r_uri [] in
+ let eqt = mkMutInd (Logic.eq_URI, 0) [] in
+ let r = Reals.r in
let metasenv = metasenv_of_status ~status in
- let (metano, context, ty) = conj_of_metano goal metasenv in
+ let (metano, context, ty) = CicUtil.lookup_meta goal metasenv in
let (t1, t2) = split_eq ty in (* goal like t1 = t2 *)
match (build_segments ~terms:[t1; t2]) with
| (t1', t1'', t1'_eq_t1'')::(t2', t2'', t2'_eq_t2'')::[] -> begin
"exact sym_eqt su t1 ...", exact_tac
~term:(
Cic.Appl
- [mkConst sym_eqt_uri
- [equality_is_a_congruence_A, mkConst r_uri [] ;
+ [mkConst Logic.sym_eq_URI
+ [equality_is_a_congruence_A, Reals.r;
equality_is_a_congruence_x, t1'' ;
equality_is_a_congruence_y, t1
] ;
exact_tac
~term:(
Cic.Appl
- [mkConst sym_eqt_uri
- [equality_is_a_congruence_A, mkConst r_uri [] ;
+ [mkConst Logic.sym_eq_URI
+ [equality_is_a_congruence_A, Reals.r;
equality_is_a_congruence_x, t2'' ;
equality_is_a_congruence_y, t2
] ;
projects / helm.git / blobdiff