*)
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"
+ 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
@return current goal's metasenv
*)
-let metasenv_of_status ~status:((_,m,_,_), _) = m
+let metasenv_of_status ((_,m,_,_), _) = m
(**
@param status a proof engine status
@raise Failure when proof or goal are None
@return context corresponding to current goal
*)
-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_of_status status =
+ let (proof, goal) = status in
+ let metasenv = metasenv_of_status status 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 Logic_Type.eqt_URI) -> true
+ | Cic.MutInd (uri, 0, []) when (eq uri Logic.eq_URI) -> true
| _ -> false
in
let is_real = function
@param status current proof engine status
@param term term to cut
*)
-let elim_type_tac ~term ~status =
+let elim_type_tac ~term status =
warn "in Ring.elim_type_tac";
Tacticals.thens ~start:(cut_tac ~term)
- ~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; Tacticals.id_tac] ~status
+ ~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; Tacticals.id_tac] status
*)
(**
@param term term to cut
@param proof term used to prove second subgoal generated by elim_type
*)
-let elim_type2_tac ~term ~proof ~status =
+let elim_type2_tac ~term ~proof status =
let module E = EliminationTactics in
warn "in Ring.elim_type2";
Tacticals.thens ~start:(E.elim_type_tac ~term)
- ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof] ~status
+ ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof] status
(* Galla: spostata in variousTactics.ml
(**
only refl_eqT, coq's one also try "refl_equal"
@param status current proof engine status
*)
-let reflexivity_tac ~status:(proof, goal) =
+let reflexivity_tac (proof, goal) =
warn "in Ring.reflexivity_tac";
let refl_eqt = mkCtor ~uri:refl_eqt_uri ~exp_named_subst:[] in
try
- apply_tac ~status:(proof, goal) ~term:refl_eqt
+ apply_tac (proof, goal) ~term:refl_eqt
with (Fail _) as e ->
let e_str = Printexc.to_string e in
raise (Fail ("Reflexivity failed with exception: " ^ e_str))
@param count number of hypotheses to remove
@param status current proof engine status
*)
-let purge_hyps_tac ~count ~status:(proof, goal as status) =
+let purge_hyps_tac ~count status =
let module S = ProofEngineStructuralRules in
+ let (proof, goal) = status in
let rec aux n context status =
assert(n>=0);
match (n, context) with
| (0, _) -> status
| (n, hd::tl) ->
aux (n-1) tl
- (status_of_single_goal_tactic_result (S.clear ~hyp:hd ~status))
+ (status_of_single_goal_tactic_result (S.clear ~hyp:hd status))
| (_, []) -> 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']
Ring tactic, does associative and commutative rewritings in Reals ring
@param status current proof engine status
*)
-let ring_tac ~status:((proof, goal) as status) =
+let ring_tac status =
+ let (proof, goal) = status in
warn "in Ring tactic";
- let eqt = mkMutInd (Logic_Type.eqt_URI, 0) [] 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 metasenv = metasenv_of_status status 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
try
let new_hyps = ref 0 in (* number of new hypotheses created *)
Tacticals.try_tactics
- ~status
+ status
~tactics:[
"reflexivity", EqualityTactics.reflexivity_tac ;
"exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ;
"exact sym_eqt su t1 ...", exact_tac
~term:(
Cic.Appl
- [mkConst Logic_Type.sym_eqt_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
] ;
t1'_eq_t1''
]) ;
- "elim_type eqt su t1 ...", (fun ~status ->
+ "elim_type eqt su t1 ...", (fun status ->
let status' = (* status after 1st elim_type use *)
- let context = context_of_status ~status in
+ let context = context_of_status status in
if not (are_convertible context t1'' t1) then begin
warn "t1'' and t1 are NOT CONVERTIBLE";
let newstatus =
elim_type2_tac (* 1st elim_type use *)
- ~status ~proof:t1'_eq_t1''
+ status ~proof:t1'_eq_t1''
~term:(Cic.Appl [eqt; r; t1''; t1])
in
incr new_hyps; (* elim_type add an hyp *)
in
let status'' =
Tacticals.try_tactics (* try to solve 1st subgoal *)
- ~status:status'
+ status'
~tactics:[
"exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'';
"exact sym_eqt su t2 ...",
exact_tac
~term:(
Cic.Appl
- [mkConst Logic_Type.sym_eqt_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
] ;
t2'_eq_t2''
]) ;
- "elim_type eqt su t2 ...", (fun ~status ->
+ "elim_type eqt su t2 ...", (fun status ->
let status' =
- let context = context_of_status ~status in
+ let context = context_of_status status in
if not (are_convertible context t2'' t2) then begin
warn "t2'' and t2 are NOT CONVERTIBLE";
let newstatus =
elim_type2_tac (* 2nd elim_type use *)
- ~status ~proof:t2'_eq_t2''
+ status ~proof:t2'_eq_t2''
~term:(Cic.Appl [eqt; r; t2''; t2])
in
incr new_hyps; (* elim_type add an hyp *)
in
try (* try to solve main goal *)
warn "trying reflexivity ....";
- EqualityTactics.reflexivity_tac ~status:status'
+ EqualityTactics.reflexivity_tac status'
with (Fail _) -> (* leave conclusion to the user *)
warn "reflexivity failed, solution's left as an ex :-)";
- purge_hyps_tac ~count:!new_hyps ~status:status')]
+ purge_hyps_tac ~count:!new_hyps status')]
in
status'')]
with (Fail s) ->
assert false
(* wrap ring_tac catching GoalUnringable and raising Fail *)
-let ring_tac ~status =
+let ring_tac status =
try
- ring_tac ~status
+ ring_tac status
with GoalUnringable ->
raise (Fail "goal unringable")
projects / helm.git / blobdiff