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 *)
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
+ e ->
+ match e with
+ (Fail _)
+ | (CicTypeChecker.NotWellTyped _)
+ | (CicUnification.UnificationFailed) ->
warn (
"Ring.try_tactics failed with exn: " ^
Printexc.to_string e);
try_tactics ~tactics ~status
- end
- )
+ | _ -> raise e (* [e] must not be caught ; let's re-raise it *)
+ )
| [] -> raise (Fail "try_tactics: no tactics left")
+let thens ~start ~continuations ~status =
+ let (proof,new_goals) = start ~status in
+ try
+ List.fold_left2
+ (fun (proof,goals) goal tactic ->
+ let (proof',new_goals') = tactic ~status:(proof,goal) in
+ (proof',goals@new_goals')
+ ) (proof,[]) new_goals continuations
+ with
+ Invalid_argument _ -> raise (Fail "thens: wrong number of new goals")
+
+let id_tac ~status:(proof,goal) =
+ (proof,[goal])
+
+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)
+ 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))
+ 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
~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
~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
projects / helm.git / blobdiff