uri_of_string
"cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize_ok.con"
-(** HELPERS *)
-
- (**
- "Some" constructor's inverse
- @raise Failure "unsome" if None is passed
- *)
-let unsome = function None -> failwith "unsome" | Some item -> item
-
(** CIC PREDICATES *)
(**
@raise Failure if proof is None
@return current goal's metasenv
*)
-let metasenv_of_status ~status:(proof, goal) =
- match proof with
- | None -> failwith "Ring.metasenv_of_status invoked on None goal"
- | Some (_, m, _, _) -> m
+let metasenv_of_status ~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) =
- let metasenv = metasenv_of_status ~status:(proof, goal) in
- let _, context, _ =
- match goal with
- | None -> failwith "Ring.context_of_status invoked on None goal"
- | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
- in
- context
+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
+ context
(** CIC TERM CONSTRUCTORS *)
[lxy_false; varmap; rtheory; t]))
aterms
-(** AUX TACTIC{,AL}S *)
+let id_tac ~status:(proof,goal) =
+ (proof,[goal])
- (**
- naive implementation of ORELSE tactical, try a sequence of tactics in turn:
- if one fails pass to the next one and so on, eventually raises (failure "no
- tactics left")
- TODO warning: not tail recursive due to "try .. with" boxing
- *)
-let rec try_tactics ~(tactics: (string * tactic) list) ~status =
- warn "in Ring.try_tactics";
- match tactics with
- | (descr, tac)::tactics ->
- warn ("Ring.try_tactics IS TRYING " ^ descr);
- (try
- let res = tac ~status in
- warn ("Ring.try_tactics: " ^ descr ^ " succedeed!!!");
- res
- with
- | (Fail _) as e -> begin (* TODO: codice replicato perche' non funge il
- binding multiplo con "as" *)
- warn (
- "Ring.try_tactics failed with exn: " ^
- Printexc.to_string e);
- try_tactics ~tactics ~status
- end
- | (CicTypeChecker.NotWellTyped _) as e -> begin (* TODO: si puo' togliere? *)
- warn (
- "Ring.try_tactics failed with exn: " ^
- Printexc.to_string e);
- try_tactics ~tactics ~status
- end
- | (CicUnification.UnificationFailed) as e -> begin
- warn (
- "Ring.try_tactics failed with exn: " ^
- Printexc.to_string e);
- try_tactics ~tactics ~status
- end
- )
- | [] -> raise (Fail "try_tactics: no tactics left")
+let status_of_single_goal_tactic_result =
+ function
+ proof,[goal] -> proof,goal
+ | _ ->
+ raise (Fail "status_of_single_goal_tactic_result: the tactic did not produce exactly a new goal")
(**
auxiliary tactic "elim_type"
@param status current proof engine status
@param term term to cut
*)
-let elim_type_tac ~status ~term =
+let elim_type_tac ~term ~status =
warn "in Ring.elim_type_tac";
- let status' = cut_tac ~term ~status in
- elim_intros_simpl_tac ~term:(Cic.Rel 1) ~status:status'
-
- (**
- move to next goal
- @param status current proof engine status
- *)
-let next_goal ~status =
- warn "in Ring.next_goal";
- (match status with
- | ((Some (_, metasenv, _, _)) as proof, goal) ->
- (match metasenv with
- | _::(n, _, _)::_ -> (proof, Some n)
- | _ -> raise (Fail "No other goal available"))
- | _ -> assert false)
+ Tacticals.thens ~start:(cut_tac ~term)
+ ~continuations:[elim_intros_simpl_tac ~term:(Cic.Rel 1) ; id_tac] ~status
(**
auxiliary tactic, use elim_type and try to close 2nd subgoal using proof
@param term term to cut
@param proof term used to prove second subgoal generated by elim_type
*)
-let elim_type2_tac ~status ~term ~proof =
+let elim_type2_tac ~term ~proof ~status =
warn "in Ring.elim_type2";
- exact_tac ~term:proof ~status:(next_goal (elim_type_tac ~term ~status))
+ Tacticals.thens ~start:(elim_type_tac ~term)
+ ~continuations:[id_tac ; exact_tac ~term:proof] ~status
(**
Reflexivity tactic, try to solve current goal using "refl_eqT"
*)
let reflexivity_tac ~status:(proof, goal) =
warn "in Ring.reflexivity_tac";
- let refl_eqt = mkCtor ~uri:refl_eqt_uri ~proof:(unsome proof) in
+ let refl_eqt = mkCtor ~uri:refl_eqt_uri ~proof:proof in
try
apply_tac ~status:(proof, goal) ~term:refl_eqt
with (Fail _) as e ->
@param count number of hypotheses to remove
@param status current proof engine status
*)
-let purge_hyps ~count ~status:(proof, goal) =
+let purge_hyps_tac ~count ~status:(proof, goal as status) =
let module S = ProofEngineStructuralRules in
let rec aux n context status =
assert(n>=0);
match (n, context) with
| (0, _) -> status
- | (n, hd::tl) -> aux (n-1) tl (S.clear ~status ~hyp:hd)
- | (_, []) -> failwith "Ring.purge_hyps: no hypotheses left"
- in
- let metano =
- match goal with
- | None -> failwith "Ring.purge_hyps invoked on None goal"
- | Some n -> n
+ | (n, hd::tl) ->
+ aux (n-1) tl
+ (status_of_single_goal_tactic_result (S.clear ~hyp:hd ~status))
+ | (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left"
in
- match proof with
- | None -> failwith "Ring.purge_hyps invoked on None proof"
- | Some (_, metasenv, _, _) ->
- let (_, context, _) = conj_of_metano metano metasenv in
- aux count context (proof, goal)
+ let (_, metasenv, _, _) = proof in
+ let (_, context, _) = conj_of_metano goal metasenv in
+ let proof',goal' = aux count context status in
+ assert (goal = goal') ;
+ proof',[goal']
(** THE TACTIC! *)
let ring_tac ~status:(proof, goal) =
warn "in Ring tactic";
let status = (proof, goal) in
- let (proof, goal) = (unsome proof), (unsome goal) in
let eqt = mkMutInd (eqt_uri, 0) proof in
let r = mkConst r_uri proof in
let metasenv = metasenv_of_status ~status in
t2; t2'; t2''; t2'_eq_t2'']);
try
let new_hyps = ref 0 in (* number of new hypotheses created *)
- try_tactics
+ Tacticals.try_tactics
~status
~tactics:[
"reflexivity", reflexivity_tac;
~status ~proof:t1'_eq_t1''
~term:(Cic.Appl [eqt; r; t1''; t1])
in
- incr new_hyps; (* elim_type add an hyp *)
- newstatus
+ incr new_hyps; (* elim_type add an hyp *)
+ match newstatus with
+ (proof,[goal]) -> proof,goal
+ | _ -> assert false
end else begin
warn "t1'' and t1 are CONVERTIBLE";
status
lift 1 (t1,t1',t1'',t1'_eq_t1'', t2,t2',t2'',t2'_eq_t2'')
in
let status'' =
- try_tactics (* try to solve 1st subgoal *)
+ Tacticals.try_tactics (* try to solve 1st subgoal *)
~status:status'
~tactics:[
"exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'';
~term:(Cic.Appl [eqt; r; t2''; t2])
in
incr new_hyps; (* elim_type add an hyp *)
- newstatus
+ match newstatus with
+ (proof,[goal]) -> proof,goal
+ | _ -> assert false
end else begin
warn "t2'' and t2 are CONVERTIBLE";
status
reflexivity_tac ~status:status'
with (Fail _) -> (* leave conclusion to the user *)
warn "reflexivity failed, solution's left as an ex :-)";
- purge_hyps ~count:!new_hyps ~status:status')]
+ purge_hyps_tac ~count:!new_hyps ~status:status')]
in
status'')]
- with (Fail _) ->
- raise (Fail "Ring failure")
+ with (Fail s) ->
+ raise (Fail ("Ring failure: " ^ s))
end
| _ -> (* impossible: we are applying ring exacty to 2 terms *)
assert false