primitiveTactics.cmx: proofEngineHelpers.cmx proofEngineReduction.cmx \
proofEngineTypes.cmx primitiveTactics.cmi
primitiveTactics.cmi: proofEngineTypes.cmo
+tacticals.cmo: primitiveTactics.cmi proofEngineTypes.cmo tacticals.cmi
+tacticals.cmx: primitiveTactics.cmx proofEngineTypes.cmx tacticals.cmi
+tacticals.cmi: proofEngineTypes.cmo
ring.cmo: primitiveTactics.cmi proofEngineStructuralRules.cmi \
- proofEngineTypes.cmo ring.cmi
+ proofEngineTypes.cmo tacticals.cmi ring.cmi
ring.cmx: primitiveTactics.cmx proofEngineStructuralRules.cmx \
- proofEngineTypes.cmx ring.cmi
+ proofEngineTypes.cmx tacticals.cmx ring.cmi
ring.cmi: proofEngineTypes.cmo
-fourierR.cmo: fourier.cmo fourierR.cmi
-fourierR.cmx: fourier.cmx fourierR.cmi
+fourierR.cmo: fourier.cmo primitiveTactics.cmi ring.cmi fourierR.cmi
+fourierR.cmx: fourier.cmx primitiveTactics.cmx ring.cmx fourierR.cmi
fourierR.cmi: proofEngineTypes.cmo
proofEngine.cmo: fourierR.cmi primitiveTactics.cmi proofEngineHelpers.cmi \
proofEngineReduction.cmi proofEngineStructuralRules.cmi \
DEPOBJS = xml2Gdome.ml xml2Gdome.mli proofEngineTypes.ml proofEngineHelpers.ml \
proofEngineReduction.ml proofEngineReduction.mli \
proofEngineStructuralRules.ml proofEngineStructuralRules.mli \
- primitiveTactics.ml primitiveTactics.mli ring.ml ring.mli fourier.ml fourierR.ml fourierR.mli\
+ primitiveTactics.ml primitiveTactics.mli tacticals.ml tacticals.mli \
+ ring.ml ring.mli fourier.ml fourierR.ml fourierR.mli\
proofEngine.ml proofEngine.mli \
doubleTypeInference.ml doubleTypeInference.mli cic2acic.ml \
cic2acic.mli cic2Xml.ml cic2Xml.mli logicalOperations.ml \
mQueryGenerator.ml gTopLevel.ml
TOPLEVELOBJS = xml2Gdome.cmo proofEngineTypes.cmo proofEngineHelpers.cmo \
- proofEngineReduction.cmo proofEngineStructuralRules.cmo \
- primitiveTactics.cmo ring.cmo fourier.cmo fourierR.cmo proofEngine.cmo \
+ proofEngineReduction.cmo proofEngineStructuralRules.cmo \
+ primitiveTactics.cmo tacticals.cmo ring.cmo \
+ fourier.cmo fourierR.cmo proofEngine.cmo \
doubleTypeInference.cmo cic2acic.cmo cic2Xml.cmo \
logicalOperations.cmo sequentPp.cmo mQueryGenerator.cmo \
gTopLevel.cmo
let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/_Rlt_mult_inv_pos.con") 0 ;;
-let tcl_then ~start ~continuation ~status =
- let tcl_then_aux (proof,goals) goal =
- let (newproof,newgoals) = continuation ~status:(proof,goal) in
- (newproof, goals @ newgoals)
- in
- let (proof,new_goals) = start ~status in
- List.fold_left tcl_then_aux (proof,[]) new_goals
-;;
-
let tac_zero_inf_pos gl (n,d) =
(*let cste = pf_parse_constr gl in*)
let tacn=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
for i=1 to n-1 do
- tacn:=(tcl_then ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacn); done;
+ tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacn); done;
for i=1 to d-1 do
- tacd:=(tcl_then ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); done;
- (Ring.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) ~continuations:[!tacn;!tacd])
+ tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); done;
+ (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) ~continuations:[!tacn;!tacd])
;;
(* preuve que 0<=n*1/d
[lxy_false; varmap; rtheory; t]))
aterms
-(** AUX TACTIC{,AL}S *)
-
- (**
- 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
- e ->
- match e with
- (Fail _)
- | (CicTypeChecker.NotWellTyped _)
- | (CicUnification.UnificationFailed) ->
- warn (
- "Ring.try_tactics failed with exn: " ^
- Printexc.to_string e);
- try_tactics ~tactics ~status
- | _ -> 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 then_ ~start ~continuation ~status =
- let (proof,new_goals) = start ~status in
- List.fold_left
- (fun (proof,goals) goal ->
- let (proof',new_goals') = continuation ~status:(proof,goal) in
- (proof',goals@new_goals')
- ) (proof,[]) new_goals
-
-
let id_tac ~status:(proof,goal) =
(proof,[goal])
*)
let elim_type_tac ~term ~status =
warn "in Ring.elim_type_tac";
- thens ~start:(cut_tac ~term)
+ Tacticals.thens ~start:(cut_tac ~term)
~continuations:[elim_intros_simpl_tac ~term:(Cic.Rel 1) ; id_tac] ~status
(**
*)
let elim_type2_tac ~term ~proof ~status =
warn "in Ring.elim_type2";
- thens ~start:(elim_type_tac ~term)
+ Tacticals.thens ~start:(elim_type_tac ~term)
~continuations:[id_tac ; exact_tac ~term:proof] ~status
(**
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;
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'';
val elim_type_tac: term: Cic.term -> ProofEngineTypes.tactic
val reflexivity_tac: ProofEngineTypes.tactic
val id_tac : ProofEngineTypes.tactic
-
- (* pseudo tacticals *)
-val try_tactics:
- tactics: (string * ProofEngineTypes.tactic) list -> ProofEngineTypes.tactic
-val thens:
- start: ProofEngineTypes.tactic ->
- continuations: ProofEngineTypes.tactic list -> ProofEngineTypes.tactic
-val then_:
- start: ProofEngineTypes.tactic ->
- continuation: ProofEngineTypes.tactic -> ProofEngineTypes.tactic
--- /dev/null
+(* Copyright (C) 2002, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+open CicReduction
+open PrimitiveTactics
+open ProofEngineTypes
+open UriManager
+
+(** DEBUGGING *)
+
+ (** perform debugging output? *)
+let debug = false
+
+ (** debugging print *)
+let warn s =
+ if debug then
+ prerr_endline ("TACTICALS WARNING: " ^ s)
+
+(** AUX TACTIC{,AL}S *)
+
+ (**
+ 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
+ e ->
+ match e with
+ (Fail _)
+ | (CicTypeChecker.NotWellTyped _)
+ | (CicUnification.UnificationFailed) ->
+ warn (
+ "Ring.try_tactics failed with exn: " ^
+ Printexc.to_string e);
+ try_tactics ~tactics ~status
+ | _ -> 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 then_ ~start ~continuation ~status =
+ let (proof,new_goals) = start ~status in
+ List.fold_left
+ (fun (proof,goals) goal ->
+ let (proof',new_goals') = continuation ~status:(proof,goal) in
+ (proof',goals@new_goals')
+ ) (proof,[]) new_goals
--- /dev/null
+(* Copyright (C) 2002, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+ (* pseudo tacticals *)
+val try_tactics:
+ tactics: (string * ProofEngineTypes.tactic) list -> ProofEngineTypes.tactic
+val thens:
+ start: ProofEngineTypes.tactic ->
+ continuations: ProofEngineTypes.tactic list -> ProofEngineTypes.tactic
+val then_:
+ start: ProofEngineTypes.tactic ->
+ continuation: ProofEngineTypes.tactic -> ProofEngineTypes.tactic
projects / helm.git / commitdiff