* http://cs.unibo.it/helm/.
*)
+open HelmLibraryObjects
let rec injection_tac ~term ~status:((proof, goal) as status) =
let module C = Cic in
let termty = (CicTypeChecker.type_of_aux' metasenv context term) in
(match termty with
(C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
- when (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"))
- or (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> (
+ when (U.eq equri Logic.eq_URI)
+ or (U.eq equri Logic_Type.eqt_URI) -> (
match tty with
(C.MutInd (turi,typeno,exp_named_subst))
| (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) -> (
let termty = (CicTypeChecker.type_of_aux' metasenv context term) in
match termty with (* an equality *)
(C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
- when (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"))
- or (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> (
+ when (U.eq equri Logic.eq_URI) or
+ (U.eq equri Logic_Type.eqt_URI) -> (
match tty with (* some inductive type *)
(C.MutInd (turi,typeno,exp_named_subst))
| (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) ->
let termty = (CicTypeChecker.type_of_aux' metasenv context term) in
match termty with
(C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2])
- when (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"))
- or (U.eq equri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> (
+ when (U.eq equri Logic.eq_URI) or (U.eq equri Logic_Type.eqt_URI) -> (
match tty with
(C.MutInd (turi,typeno,exp_named_subst))
| (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::_)) ->
C.Lambda (binder,source,(aux target (k+1)))
| _ ->
if (id = false_constr_id)
- then (C.MutInd((U.uri_of_string "cic:/Coq/Init/Logic/False.ind"),0,[]))
- else (C.MutInd((U.uri_of_string "cic:/Coq/Init/Logic/True.ind"),0,[]))
+ then (C.MutInd(Logic.false_URI,0,[]))
+ else (C.MutInd(Logic.true_URI,0,[]))
in aux red_ty 1
)
constructor_list
let (proof',goals') =
EliminationTactics.elim_type_tac
- ~term:(C.MutInd((U.uri_of_string "cic:/Coq/Init/Logic/False.ind"),0,[]))
+ ~term:(C.MutInd(Logic.false_URI,0,[]))
~status
in
(match goals' with
let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) =
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
- let fresh_meta = ProofEngineHelpers.new_meta proof in
+ let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
let irl =
- ProofEngineHelpers.identity_relocation_list_for_metavariable context in
+ CicMkImplicit.identity_relocation_list_for_metavariable context in
let metasenv' = (fresh_meta,context,t)::metasenv in
let proof' = curi,metasenv',pbo,pty in
let proof'',goals =
debug("my_cut di "^CicPp.ppterm c^"\n");
- let fresh_meta = ProofEngineHelpers.new_meta proof in
+ let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
let irl =
- ProofEngineHelpers.identity_relocation_list_for_metavariable context in
+ CicMkImplicit.identity_relocation_list_for_metavariable context in
let metasenv' = (fresh_meta,context,c)::metasenv in
let proof' = curi,metasenv',pbo,pty in
let proof'',goals =
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in
- let fresh_meta = ProofEngineHelpers.new_meta proof in
+ let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
let irl =
- ProofEngineHelpers.identity_relocation_list_for_metavariable context in
+ CicMkImplicit.identity_relocation_list_for_metavariable context in
let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
let (proof,goals) =
try_next 1
;;
-(* identity_relocation_list_for_metavariable i canonical_context *)
-(* returns the identity relocation list, which is the list [1 ; ... ; n] *)
-(* where n = List.length [canonical_context] *)
-(*CSC: ma mi basta la lunghezza del contesto canonico!!!*)
-let identity_relocation_list_for_metavariable canonical_context =
- let canonical_context_length = List.length canonical_context in
- let rec aux =
- function
- (_,[]) -> []
- | (n,None::tl) -> None::(aux ((n+1),tl))
- | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl))
- in
- aux (1,canonical_context)
-
-(* Returns the first meta whose number is above the *)
-(* number of the higher meta. *)
-let new_meta ~proof =
- let (_,metasenv,_,_) = proof in
- let rec aux =
- function
- None,[] -> 1
- | Some n,[] -> n
- | None,(n,_,_)::tl -> aux (Some n,tl)
- | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
- in
- 1 + aux (None,metasenv)
+let new_meta_of_proof ~proof:(_, metasenv, _, _) =
+ CicMkImplicit.new_meta metasenv
let subst_meta_in_proof proof meta term newmetasenv =
let uri,metasenv,bo,ty = proof in
- let subst_in = CicUnification.apply_subst [meta,term] in
+ let subst_in = CicMetaSubst.apply_subst [meta,term] in
let metasenv' =
newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv)
in
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"
let equality_is_a_congruence_x =
uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/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"
let apolynomial_uri =
uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial.ind"
*)
let ringable =
let is_equality = function
- | Cic.MutInd (uri, 0, []) when (eq uri eqt_uri) -> true
+ | Cic.MutInd (uri, 0, []) when (eq uri Logic_Type.eqt_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
*)
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_Type.eqt_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 (t1, t2) = split_eq ty in (* goal like t1 = t2 *)
"exact sym_eqt su t1 ...", exact_tac
~term:(
Cic.Appl
- [mkConst sym_eqt_uri
- [equality_is_a_congruence_A, mkConst r_uri [] ;
+ [mkConst Logic_Type.sym_eqt_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_Type.sym_eqt_URI
+ [equality_is_a_congruence_A, Reals.r;
equality_is_a_congruence_x, t2'' ;
equality_is_a_congruence_y, t2
] ;
projects / helm.git / commitdiff