From: Michele Galatà Date: Thu, 31 Oct 2002 14:49:40 +0000 (+0000) Subject: Added variousTactic with Constructor, Left, Right, Exists, Reflexivity, Symmetry... X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=373eaf73bebec626e031a4a534ddfdd4f1c1b474;p=helm.git Added variousTactic with Constructor, Left, Right, Exists, Reflexivity, Symmetry, Transitivity Added tacticals Repeat, Do, Try, Solve --- diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend index bcf5bbd72..88a318793 100644 --- a/helm/gTopLevel/.depend +++ b/helm/gTopLevel/.depend @@ -22,24 +22,31 @@ primitiveTactics.cmx: proofEngineHelpers.cmx proofEngineReduction.cmx \ proofEngineTypes.cmx reductionTactics.cmx tacticals.cmx \ primitiveTactics.cmi primitiveTactics.cmi: proofEngineTypes.cmo +variousTactics.cmo: primitiveTactics.cmi proofEngineTypes.cmo tacticals.cmi \ + variousTactics.cmi +variousTactics.cmx: primitiveTactics.cmx proofEngineTypes.cmx tacticals.cmx \ + variousTactics.cmi +variousTactics.cmi: proofEngineTypes.cmo ring.cmo: primitiveTactics.cmi proofEngineStructuralRules.cmi \ - proofEngineTypes.cmo tacticals.cmi ring.cmi + proofEngineTypes.cmo tacticals.cmi variousTactics.cmi ring.cmi ring.cmx: primitiveTactics.cmx proofEngineStructuralRules.cmx \ - proofEngineTypes.cmx tacticals.cmx ring.cmi + proofEngineTypes.cmx tacticals.cmx variousTactics.cmx ring.cmi ring.cmi: proofEngineTypes.cmo fourierR.cmo: fourier.cmo primitiveTactics.cmi proofEngineHelpers.cmi \ - proofEngineReduction.cmi proofEngineTypes.cmo ring.cmi tacticals.cmi \ - fourierR.cmi + proofEngineReduction.cmi proofEngineTypes.cmo reductionTactics.cmi \ + ring.cmi tacticals.cmi fourierR.cmi fourierR.cmx: fourier.cmx primitiveTactics.cmx proofEngineHelpers.cmx \ - proofEngineReduction.cmx proofEngineTypes.cmx ring.cmx tacticals.cmx \ - fourierR.cmi + proofEngineReduction.cmx proofEngineTypes.cmx reductionTactics.cmx \ + ring.cmx tacticals.cmx fourierR.cmi fourierR.cmi: proofEngineTypes.cmo proofEngine.cmo: fourierR.cmi primitiveTactics.cmi proofEngineHelpers.cmi \ proofEngineReduction.cmi proofEngineStructuralRules.cmi \ - proofEngineTypes.cmo ring.cmi proofEngine.cmi + proofEngineTypes.cmo ring.cmi tacticals.cmi variousTactics.cmi \ + proofEngine.cmi proofEngine.cmx: fourierR.cmx primitiveTactics.cmx proofEngineHelpers.cmx \ proofEngineReduction.cmx proofEngineStructuralRules.cmx \ - proofEngineTypes.cmx ring.cmx proofEngine.cmi + proofEngineTypes.cmx ring.cmx tacticals.cmx variousTactics.cmx \ + proofEngine.cmi proofEngine.cmi: proofEngineTypes.cmo doubleTypeInference.cmo: doubleTypeInference.cmi doubleTypeInference.cmx: doubleTypeInference.cmi diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index b2680c27b..200305cbe 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -18,7 +18,7 @@ DEPOBJS = xml2Gdome.ml xml2Gdome.mli proofEngineTypes.ml proofEngineHelpers.ml \ proofEngineReduction.ml proofEngineReduction.mli \ proofEngineStructuralRules.ml proofEngineStructuralRules.mli \ tacticals.ml tacticals.mli reductionTactics.ml reductionTactics.mli \ - primitiveTactics.ml primitiveTactics.mli \ + primitiveTactics.ml primitiveTactics.mli variousTactics.ml variousTactics.mli \ ring.ml ring.mli fourier.ml fourierR.ml fourierR.mli\ proofEngine.ml proofEngine.mli \ doubleTypeInference.ml doubleTypeInference.mli cic2acic.ml \ @@ -29,6 +29,7 @@ DEPOBJS = xml2Gdome.ml xml2Gdome.mli proofEngineTypes.ml proofEngineHelpers.ml \ TOPLEVELOBJS = xml2Gdome.cmo proofEngineTypes.cmo proofEngineHelpers.cmo \ proofEngineReduction.cmo proofEngineStructuralRules.cmo \ tacticals.cmo reductionTactics.cmo primitiveTactics.cmo \ + variousTactics.cmo \ ring.cmo fourier.cmo fourierR.cmo proofEngine.cmo \ doubleTypeInference.cmo cic2acic.cmo cic2Xml.cmo \ logicalOperations.cmo sequentPp.cmo mQueryGenerator.cmo \ diff --git a/helm/gTopLevel/esempi/various.cic b/helm/gTopLevel/esempi/various.cic new file mode 100644 index 000000000..11141d4ab --- /dev/null +++ b/helm/gTopLevel/esempi/various.cic @@ -0,0 +1,7 @@ + +!n:nat.(eq nat n n) + +!n:nat.!m:nat.(eq nat n m)->(eq nat m n) + +!n:nat.!m:nat.!p:nat.(eq nat n p)->(eq nat p m)->(eq nat n m) + diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index c8c856459..247a47248 100644 --- a/helm/gTopLevel/fourierR.ml +++ b/helm/gTopLevel/fourierR.ml @@ -1048,7 +1048,7 @@ theoreme,so let's parse our thesis *) " disequazioni\n"); let res=fourier_lineq (!lineq) in - let tac=ref Ring.id_tac in + let tac=ref Tacticals.id_tac in if res=[] then (print_string "Tactic Fourier fails.\n";flush stdout; failwith "fourier_tac fails") @@ -1234,7 +1234,7 @@ theoreme,so let's parse our thesis *) let r = Ring.ring_tac ~status in debug ("end RING\n"); r) - ; "id", Ring.id_tac] + ; "id", Tacticals.id_tac] ]) (* CSC: NOW THE BUG IS HERE: tac2 DOES NOT WORK ANY MORE *) ;tac2])) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index d0aef1a04..4a7302832 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -61,15 +61,21 @@ let htmlfooter = (* let prooffile = "/home/tassi/miohelm/tmp/currentproof";; -*) let prooffile = "/public/sacerdot/currentproof";; -let prooffiletype = "/public/sacerdot/currentprooftype";; +*) + +let prooffile = "/home/galata/miohelm/currentproof";; +let prooffiletype = "/home/galata/miohelm/currentprooftype";; + (*CSC: the getter should handle the innertypes, not the FS *) (* let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";; -*) let innertypesfile = "/public/sacerdot/innertypes";; -let constanttypefile = "/public/sacerdot/constanttype";; +*) + +let innertypesfile = "/home/galata/miohelm/innertypes";; +let constanttypefile = "/home/galata/miohelm/constanttype";; + (* GLOBAL REFERENCES (USED BY CALLBACKS) *) @@ -747,7 +753,29 @@ let fourier rendering_window = let rewritesimpl rendering_window = call_tactic_with_input ProofEngine.rewrite_simpl rendering_window ;; - +let reflexivity rendering_window = + call_tactic ProofEngine.reflexivity rendering_window +;; +let symmetry rendering_window = + call_tactic ProofEngine.symmetry rendering_window +;; +let transitivity rendering_window = + call_tactic_with_input ProofEngine.transitivity rendering_window +;; +let left rendering_window = + call_tactic ProofEngine.left rendering_window +;; +let right rendering_window = + call_tactic ProofEngine.right rendering_window +;; +let assumption rendering_window = + call_tactic ProofEngine.assumption rendering_window +;; +(* +let prova_tatticali rendering_window = + call_tactic ProofEngine.prova_tatticali rendering_window +;; +*) let whd_in_scratch scratch_window = @@ -1592,6 +1620,27 @@ class rendering_window output proofw (label : GMisc.label) = let rewritesimplb = GButton.button ~label:"RewriteSimpl ->" ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let reflexivityb = + GButton.button ~label:"Reflexivity" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let symmetryb = + GButton.button ~label:"Symmetry" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let transitivityb = + GButton.button ~label:"Transitivity" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let leftb = + GButton.button ~label:"Left" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let rightb = + GButton.button ~label:"Right" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let assumptionb = + GButton.button ~label:"Assumption" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in + let prova_tatticalib = + GButton.button ~label:"Prova_tatticali" + ~packing:(hbox4#pack ~expand:false ~fill:false ~padding:5) () in let outputhtml = GHtml.xmhtml ~source:"" @@ -1647,6 +1696,15 @@ object(self) ignore(clearb#connect#clicked (clear self)) ; ignore(fourierb#connect#clicked (fourier self)) ; ignore(rewritesimplb#connect#clicked (rewritesimpl self)) ; + ignore(reflexivityb#connect#clicked (reflexivity self)) ; + ignore(symmetryb#connect#clicked (symmetry self)) ; + ignore(transitivityb#connect#clicked (transitivity self)) ; + ignore(leftb#connect#clicked (left self)) ; + ignore(rightb#connect#clicked (right self)) ; + ignore(assumptionb#connect#clicked (assumption self)) ; +(* + ignore(prova_tatticalib#connect#clicked (prova_tatticali self)) ; +*) ignore(introsb#connect#clicked (intros self)) ; Logger.log_callback := (Logger.log_to_html ~print_and_flush:(output_html outputhtml)) diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index 972ae962a..b47f8856a 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -288,3 +288,16 @@ let elim_type term = apply_tactic (Ring.elim_type_tac ~term) let ring () = apply_tactic Ring.ring_tac let fourier () = apply_tactic FourierR.fourier_tac let rewrite_simpl term = apply_tactic (FourierR.rewrite_simpl_tac ~term) + +let reflexivity () = apply_tactic VariousTactics.reflexivity_tac +let symmetry () = apply_tactic VariousTactics.symmetry_tac +let transitivity term = apply_tactic (VariousTactics.transitivity_tac ~term) + +let left () = apply_tactic VariousTactics.left_tac +let right () = apply_tactic VariousTactics.right_tac + +let assumption () = apply_tactic VariousTactics.assumption_tac +(* +let prova_tatticali () = apply_tactic Tacticals.prova_tac +*) + diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli index c3b623c08..cbe4c8bc5 100644 --- a/helm/gTopLevel/proofEngine.mli +++ b/helm/gTopLevel/proofEngine.mli @@ -60,3 +60,16 @@ val elim_type : Cic.term -> unit val ring : unit -> unit val fourier : unit -> unit val rewrite_simpl : Cic.term -> unit + +val reflexivity : unit -> unit +val symmetry : unit -> unit +val transitivity : Cic.term -> unit + +val left : unit -> unit +val right : unit -> unit + +val assumption : unit -> unit + +(* +val prova_tatticali : unit -> unit +*) diff --git a/helm/gTopLevel/ring.ml b/helm/gTopLevel/ring.ml index d30df1aaa..399d2c289 100644 --- a/helm/gTopLevel/ring.ml +++ b/helm/gTopLevel/ring.ml @@ -397,8 +397,6 @@ let build_segments ~terms = Cic.Appl [apolynomial_normalize_ok lxy_false varmap rtheory ; t] ) aterms -let id_tac ~status:(proof,goal) = - (proof,[goal]) let status_of_single_goal_tactic_result = function @@ -414,7 +412,7 @@ let status_of_single_goal_tactic_result = 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) ; id_tac] ~status + ~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; Tacticals.id_tac] ~status (** auxiliary tactic, use elim_type and try to close 2nd subgoal using proof @@ -425,8 +423,9 @@ let elim_type_tac ~term ~status = let elim_type2_tac ~term ~proof ~status = warn "in Ring.elim_type2"; Tacticals.thens ~start:(elim_type_tac ~term) - ~continuations:[id_tac ; exact_tac ~term:proof] ~status + ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof] ~status +(* spostata in variousTactics.ml (** Reflexivity tactic, try to solve current goal using "refl_eqT" Warning: this isn't equale to the coq's Reflexivity because this one tries @@ -441,6 +440,7 @@ let reflexivity_tac ~status:(proof, goal) = with (Fail _) as e -> let e_str = Printexc.to_string e in raise (Fail ("Reflexivity failed with exception: " ^ e_str)) +*) (** lift an 8-uple of debrujins indexes of n *) let lift ~n (a,b,c,d,e,f,g,h) = @@ -498,7 +498,7 @@ let ring_tac ~status:((proof, goal) as status) = Tacticals.try_tactics ~status ~tactics:[ - "reflexivity", reflexivity_tac ; + "reflexivity", VariousTactics.reflexivity_tac ; "exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ; "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'' ; "exact sym_eqt su t1 ...", exact_tac @@ -570,7 +570,7 @@ let ring_tac ~status:((proof, goal) as status) = in try (* try to solve main goal *) warn "trying reflexivity ...."; - reflexivity_tac ~status:status' + VariousTactics.reflexivity_tac ~status: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')] diff --git a/helm/gTopLevel/ring.mli b/helm/gTopLevel/ring.mli index 224f150cc..79cb6f559 100644 --- a/helm/gTopLevel/ring.mli +++ b/helm/gTopLevel/ring.mli @@ -4,5 +4,7 @@ val ring_tac: ProofEngineTypes.tactic (* auxiliary tactics *) val elim_type_tac: term: Cic.term -> ProofEngineTypes.tactic + +(* spostata in variousTactics.ml val reflexivity_tac: ProofEngineTypes.tactic -val id_tac : ProofEngineTypes.tactic +*) diff --git a/helm/gTopLevel/tacticals.ml b/helm/gTopLevel/tacticals.ml index 2c1b1883b..d48b6a02c 100644 --- a/helm/gTopLevel/tacticals.ml +++ b/helm/gTopLevel/tacticals.ml @@ -37,22 +37,32 @@ let warn s = if debug then prerr_endline ("TACTICALS WARNING: " ^ s) -(** AUX TACTIC{,AL}S *) + +(** TACTIC{,AL}S *) + + (* not a tactical, but it's used only here (?) *) + +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 + + Galla: is this exactly Coq's "First"? + *) let rec try_tactics ~(tactics: (string * tactic) list) ~status = - warn "in Ring.try_tactics"; + warn "in Tacticals.try_tactics"; match tactics with | (descr, tac)::tactics -> - warn ("Ring.try_tactics IS TRYING " ^ descr); + warn ("Tacticals.try_tactics IS TRYING " ^ descr); (try let res = tac ~status in - warn ("Ring.try_tactics: " ^ descr ^ " succedeed!!!"); + warn ("Tacticals.try_tactics: " ^ descr ^ " succedeed!!!"); res with e -> @@ -61,13 +71,15 @@ let rec try_tactics ~(tactics: (string * tactic) list) ~status = | (CicTypeChecker.NotWellTyped _) | (CicUnification.UnificationFailed) -> warn ( - "Ring.try_tactics failed with exn: " ^ + "Tacticals.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 @@ -79,6 +91,8 @@ let thens ~start ~continuations ~status = 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 @@ -86,3 +100,145 @@ let then_ ~start ~continuation ~status = let (proof',new_goals') = continuation ~status:(proof,goal) in (proof',goals@new_goals') ) (proof,[]) new_goals + + +(* Galla *) +(* si suppone che tutte le tattiche sollevano solamente Fail? *) + +(* TODO: x debug: i due tatticali seguenti non contano quante volte hanno applicato la tattica *) + +(* This keep on appling tactic until it fails *) +(* When generates more than one goal, you have a tree of + application on the tactic, repeat_tactic works in depth on this tree *) + +let rec repeat_tactic ~tactic ~status = + warn "in repeat_tactic"; + try let (proof, goallist) = tactic ~status in + let rec step proof goallist = + match goallist with + [] -> (proof, []) + | head::tail -> + let (proof', goallist') = repeat_tactic ~tactic ~status:(proof, head) in + let (proof'', goallist'') = step proof' tail in + proof'', goallist'@goallist'' + in + step proof goallist + with + (Fail _) as e -> + warn ("Tacticals.repeat_tactic failed after nth time with exception: " ^ Printexc.to_string e) ; + id_tac ~status +;; + + + +(* This tries to apply tactic n times *) + +let rec do_tactic ~n ~tactic ~status = + warn "in do_tactic"; + try + let (proof, goallist) = + if (n>0) then tactic ~status + else id_tac ~status in +(* else (proof, []) in *)(* perche' non va bene questo? stessa questione di ##### ? *) + let rec step proof goallist = + match goallist with + [] -> (proof, []) + | head::tail -> + let (proof', goallist') = do_tactic ~n:(n-1) ~tactic ~status:(proof, head) in + let (proof'', goallist'') = step proof' tail in + proof'', goallist'@goallist'' + in + step proof goallist + with + (Fail _) as e -> + warn ("Tacticals.do_tactic failed after nth time with exception: " ^ Printexc.to_string e) ; + id_tac ~status +;; + + + +(* This applies tactic and catches its possible failure *) + +let rec try_tactic ~tactic ~status = + warn "in Tacticals.try_tactic"; + try + tactic ~status + with + (Fail _) as e -> + warn ( "Tacticals.try_tactic failed with exn: " ^ Printexc.to_string e); + id_tac ~status +;; + + +(* This tries tactics until one of them doesn't _solve_ the goal *) +(* TODO: si puo' unificare le 2(due) chiamate ricorsive? *) + +let rec solve_tactics ~(tactics: (string * tactic) list) ~status = + warn "in Tacticals.solve_tactics"; + match tactics with + | (descr, currenttactic)::moretactics -> + warn ("Tacticals.solve_tactics is trying " ^ descr); + (try + let (proof, goallist) = currenttactic ~status in + match goallist with + [] -> warn ("Tacticals.solve_tactics: " ^ descr ^ " solved the goal!!!"); +(* questo significa che non ci sono piu' goal, o che current_tactic non ne ha aperti di nuovi? (la 2a!) ##### *) +(* nel secondo caso basta per dire che solve_tactics has solved the goal? (si!) *) + (proof, goallist) + | _ -> warn ("Tacticals.solve_tactics: try the next tactic"); + solve_tactics ~tactics:(moretactics) ~status + with + (Fail _) as e -> + warn ("Tacticals.solve_tactics: current tactic failed with exn: " ^ Printexc.to_string e); + solve_tactics ~tactics ~status + ) + | [] -> raise (Fail "solve_tactics cannot solve the goal"); + id_tac ~status +;; + + + + + + + (** tattica di prova per debuggare i tatticali *) +(* +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 prova_tac = + let apply_T_tac ~status:((proof,goal) as status) = + let curi,metasenv,pbo,pty = proof in + let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in + let rel = + let rec find n = + function + [] -> assert false + | (Some (Cic.Name name,_))::_ when name = "T" -> n + | _::tl -> find (n+1) tl + in + prerr_endline ("eseguo find"); + find 1 context + in + prerr_endline ("eseguo apply"); + apply_tac ~term:(Cic.Rel rel) ~status + in +(* do_tactic ~n:2 *) + repeat_tactic + ~tactic: + (then_ + ~start:(intros_tac ~name:"pippo") + ~continuation:(thens' ~start:apply_T_tac ~continuations:[id_tac ; apply_tac ~term:(Cic.Rel 1)])) +(* id_tac *) +;; +*) + + diff --git a/helm/gTopLevel/tacticals.mli b/helm/gTopLevel/tacticals.mli index d2cadf4c8..b1861b5fa 100644 --- a/helm/gTopLevel/tacticals.mli +++ b/helm/gTopLevel/tacticals.mli @@ -23,12 +23,39 @@ * http://cs.unibo.it/helm/. *) + +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 + + +val repeat_tactic: + tactic: ProofEngineTypes.tactic -> ProofEngineTypes.tactic + +val do_tactic: + n: int -> + tactic: ProofEngineTypes.tactic -> ProofEngineTypes.tactic + +val try_tactic: + tactic: ProofEngineTypes.tactic -> ProofEngineTypes.tactic + +val solve_tactics: + tactics: (string * ProofEngineTypes.tactic) list -> ProofEngineTypes.tactic + + + +(* +val prova_tac : ProofEngineTypes.tactic +*) diff --git a/helm/gTopLevel/variousTactics.ml b/helm/gTopLevel/variousTactics.ml new file mode 100644 index 000000000..d2f168ce9 --- /dev/null +++ b/helm/gTopLevel/variousTactics.ml @@ -0,0 +1,155 @@ +(* 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/. + *) + + +let constructor_tac ~n ~status:(proof, goal) = + let module C = Cic in + let module R = CicReduction in + let (_,metasenv,_,_) = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + match (R.whd context ty) with + (C.MutInd (uri,typeno,exp_named_subst)) + | (C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::_)) -> + PrimitiveTactics.apply_tac ~status:(proof,goal) + ~term: (C.MutConstruct (uri, typeno, n, exp_named_subst)) + | _ -> raise (ProofEngineTypes.Fail "Constructor failed") +;; + + +let exists_tac ~status = + constructor_tac ~n:1 ~status +;; + + +let split_tac ~status = + constructor_tac ~n:1 ~status +;; + + +let left_tac ~status = + constructor_tac ~n:1 ~status +;; + + +let right_tac ~status = + constructor_tac ~n:2 ~status +;; + + +let reflexivity_tac = + constructor_tac ~n:1 +;; + + +let symmetry_tac ~status:(proof, goal) = + let module C = Cic in + let module R = CicReduction in + let module U = UriManager in + let (_,metasenv,_,_) = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + match (R.whd context ty) with + (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/Equality/eq.ind")) -> + PrimitiveTactics.apply_tac ~status:(proof,goal) + ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/sym_eq.con", [])) + + | (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> + PrimitiveTactics.apply_tac ~status:(proof,goal) + ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con", [])) + + | _ -> raise (ProofEngineTypes.Fail "Symmetry failed") +;; + + +let transitivity_tac ~term ~status:((proof, goal) as status) = + let module C = Cic in + let module R = CicReduction in + let module U = UriManager in + let module Tl = Tacticals in + let (_,metasenv,_,_) = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + match (R.whd context ty) with + (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic/Equality/eq.ind")) -> + Tl.thens + ~start:(PrimitiveTactics.apply_tac + ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/equality/trans_eq.con", []))) + ~continuations: [(PrimitiveTactics.exact_tac ~term); Tl.id_tac; Tl.id_tac] + ~status + + | (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> + Tl.thens + ~start:(PrimitiveTactics.apply_tac + ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/trans_eqT.con", []))) + ~continuations: [(PrimitiveTactics.exact_tac ~term); Tl.id_tac; Tl.id_tac] + ~status + + | _ -> raise (ProofEngineTypes.Fail "Transitivity failed") +;; + + +(* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio chiedere *) + +let assumption_tac ~status:((proof,goal) as status) = + let module C = Cic in + let module R = CicReduction in + let module T = CicTypeChecker in + let _,metasenv,_,_ = proof in + let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let rec find n = function + hd::tl -> +(* (let hdd = hd in + match hdd with + Some (name, termine) -> prerr_endline("####" ^ name ^ CicPp.ppterm termine) + | None -> prerr_endline("#### None") + ); +*) (match hd with + (Some (_, C.Decl t)) when (R.are_convertible context t ty) -> n + | (Some (_, C.Def t)) when (R.are_convertible context (T.type_of_aux' metasenv context t) ty) -> n + | _ -> find (n+1) tl + ) + | [] -> raise (ProofEngineTypes.Fail "No such assumption") + in PrimitiveTactics.apply_tac ~status ~term:(C.Rel (find 1 context)) +;; + +(* +let generalize_tac ~term ~status:((proof,goal) as status) = + let module C = Cic in + let module R = CicReduction in + let module T = CicTypeChecker in + let module P = PrimitiveTactics in + let module Tl = Tacticals in + let _,metasenv,_,_ = proof in + let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in + Tl.thens + ~start:(P.cut_tac ~term:(C.Lambda ("dummy_for_gen", (T.type_of_aux' metasenv context term), (R.replace ?????? (C.Name "dummy_for_gen") term ))) + ~continuations: [(P.apply_tac (C.Appl [(C.Rel 1); term])); Tl.id_tac] (* in quest'ordine o viceversa? provare *) + ~status +;; + + +let absurd_tac ~term ~status:((proof,goal) as status) = + PrimitiveTactics.cut_tac +;; +*) + diff --git a/helm/gTopLevel/variousTactics.mli b/helm/gTopLevel/variousTactics.mli new file mode 100644 index 000000000..660ac17f5 --- /dev/null +++ b/helm/gTopLevel/variousTactics.mli @@ -0,0 +1,40 @@ +(* 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/. + *) + +val reflexivity_tac: ProofEngineTypes.tactic +val symmetry_tac: ProofEngineTypes.tactic +val transitivity_tac: term:Cic.term -> ProofEngineTypes.tactic + +val constructor_tac: n:int -> ProofEngineTypes.tactic +val exists_tac: ProofEngineTypes.tactic +val split_tac: ProofEngineTypes.tactic +val left_tac: ProofEngineTypes.tactic +val right_tac: ProofEngineTypes.tactic + +val assumption_tac: ProofEngineTypes.tactic + +(* +val generalize_tac: Cic.term -> ProofEnginrTypes.tactic +*)