From: Claudio Sacerdoti Coen Date: Wed, 8 Feb 2006 13:38:43 +0000 (+0000) Subject: Never implemented tactics compare and decide equality purged from the code. X-Git-Tag: make_still_working~7593 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8c19127e7ee6c71006838f89583a3283451b664c;p=helm.git Never implemented tactics compare and decide equality purged from the code. --- diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 6c51fc80a..20635bd64 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -53,11 +53,9 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic = | Change of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_term | Clear of loc * 'ident | ClearBody of loc * 'ident - | Compare of loc * 'term | Constructor of loc * int | Contradiction of loc | Cut of loc * 'ident option * 'term - | DecideEquality of loc | Decompose of loc * ('term, 'ident) type_spec list * 'ident * 'ident list | Discriminate of loc * 'term | Elim of loc * 'term * 'term option * int option * 'ident list diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 8bd5c96f1..d6502aca8 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -78,13 +78,11 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = sprintf "change %s with %s" (pp_tactic_pattern where) (lazy_term_pp with_what) | Clear (_,id) -> sprintf "clear %s" id | ClearBody (_,id) -> sprintf "clearbody %s" id - | Compare (_,term) -> "compare " ^ term_pp term | Constructor (_,n) -> "constructor " ^ string_of_int n | Contradiction _ -> "contradiction" | Cut (_, ident, term) -> "cut " ^ term_pp term ^ (match ident with None -> "" | Some id -> " as " ^ id) - | DecideEquality _ -> "decide equality" | Decompose (_, [], what, names) -> sprintf "decompose %s%s" what (pp_intros_specs (None, names)) | Decompose (_, types, what, names) -> diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 65dd17b6a..c55bf8d9e 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -67,12 +67,10 @@ let tactic_of_ast ast = | GrafiteAst.Clear (_,id) -> Tactics.clear id | GrafiteAst.ClearBody (_,id) -> Tactics.clearbody id | GrafiteAst.Contradiction _ -> Tactics.contradiction - | GrafiteAst.Compare (_, term) -> Tactics.compare term | GrafiteAst.Constructor (_, n) -> Tactics.constructor n | GrafiteAst.Cut (_, ident, term) -> let names = match ident with None -> [] | Some id -> [id] in Tactics.cut ~mk_fresh_name_callback:(namer_of names) term - | GrafiteAst.DecideEquality _ -> Tactics.decide_equality | GrafiteAst.Decompose (_, types, what, names) -> let to_type = function | GrafiteAst.Type (uri, typeno) -> uri, typeno diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index f5ea66f2f..26c74e657 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -112,9 +112,6 @@ let disambiguate_tactic lexicon_status_ref context metasenv tactic = metasenv,GrafiteAst.Clear (loc,id) | GrafiteAst.ClearBody (loc,id) -> metasenv,GrafiteAst.ClearBody (loc,id) - | GrafiteAst.Compare (loc,term) -> - let metasenv,term = disambiguate_term context metasenv term in - metasenv,GrafiteAst.Compare (loc,term) | GrafiteAst.Constructor (loc,n) -> metasenv,GrafiteAst.Constructor (loc,n) | GrafiteAst.Contradiction loc -> @@ -122,8 +119,6 @@ let disambiguate_tactic lexicon_status_ref context metasenv tactic = | GrafiteAst.Cut (loc, ident, term) -> let metasenv,cic = disambiguate_term context metasenv term in metasenv,GrafiteAst.Cut (loc, ident, cic) - | GrafiteAst.DecideEquality loc -> - metasenv,GrafiteAst.DecideEquality loc | GrafiteAst.Decompose (loc, types, what, names) -> let disambiguate (metasenv,types) = function | GrafiteAst.Type _ -> assert false diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index e480efd34..73d6bf66a 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -140,16 +140,12 @@ EXTEND GrafiteAst.ClearBody (loc,id) | IDENT "change"; what = pattern_spec; "with"; t = tactic_term -> GrafiteAst.Change (loc, what, t) - | IDENT "compare"; t = tactic_term -> - GrafiteAst.Compare (loc,t) | IDENT "constructor"; n = int -> GrafiteAst.Constructor (loc, n) | IDENT "contradiction" -> GrafiteAst.Contradiction loc | IDENT "cut"; t = tactic_term; ident = OPT [ "as"; id = IDENT -> id] -> GrafiteAst.Cut (loc, ident, t) - | IDENT "decide"; IDENT "equality" -> - GrafiteAst.DecideEquality loc | IDENT "decompose"; types = OPT ident_list0; what = IDENT; (num, idents) = intros_spec -> let types = match types with None -> [] | Some types -> types in diff --git a/helm/software/components/tactics/discriminationTactics.ml b/helm/software/components/tactics/discriminationTactics.ml index 9e5bc7f43..0ffa2c52b 100644 --- a/helm/software/components/tactics/discriminationTactics.ml +++ b/helm/software/components/tactics/discriminationTactics.ml @@ -341,66 +341,6 @@ let discriminate_tac ~term = in ProofEngineTypes.mk_tactic (discriminate_tac ~term) -let decide_equality_tac = -(* il goal e' un termine della forma t1=t2\/~t1=t2; la tattica decide se l'uguaglianza -e' vera o no e lo risolve *) - Tacticals.id_tac - -let compare_tac ~term = Tacticals.id_tac - (* -(* term is in the form t1=t2; the tactic leaves two goals: in the first you have to *) -(* demonstrate the goal with the additional hyp that t1=t2, in the second the hyp is ~t1=t2 *) - let module C = Cic in - let module U = UriManager in - let module P = PrimitiveTactics in - let module T = Tacticals in - let _,metasenv,_,_ = proof in - let _,context,gty = CicUtil.lookup_meta goal metasenv in - let termty = (CicTypeChecker.type_of_aux' metasenv context term) in - match termty with - (C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) -> - - let term' = (* (t1=t2)\/~(t1=t2) *) - C.Appl [ - (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/or.ind"), 0, [])) ; - term ; - C.Appl [ - (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"), 1, [])) ; - t1 ; - C.Appl [C.Const ((U.uri_of_string "cic:/Coq/Init/Logic/not.con"), []) ; t2] - ] - ] - in - T.thens - ~start:(P.cut_tac ~term:term') - ~continuations:[ - T.then_ ~start:(P.intros_tac) ~continuation:(P.elim_intros_simpl_tac ~term:(C.Rel 1)) ; - decide_equality_tac] - status - | (C.Appl [(C.MutInd (uri, 0, [])); _; t1; t2]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) -> - let term' = (* (t1=t2) \/ ~(t1=t2) *) - C.Appl [ - (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/or.ind"), 0, [])) ; - term ; - C.Appl [ - (C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind"), 1, [])) ; - t1 ; - C.Appl [C.Const ((U.uri_of_string "cic:/Coq/Init/Logic/not.con"), []) ; t2] - ] - ] - in - T.thens - ~start:(P.cut_tac ~term:term') - ~continuations:[ - T.then_ ~start:(P.intros_tac) ~continuation:(P.elim_intros_simpl_tac ~term:(C.Rel 1)) ; - decide_equality_tac] - status - | _ -> raise (ProofEngineTypes.Fail "Compare: Not an equality") -*) -;; - - - (* DISCRIMINTATE SENZA INJECTION exception TwoDifferentSubtermsFound of (Cic.term * Cic.term * int) diff --git a/helm/software/components/tactics/discriminationTactics.mli b/helm/software/components/tactics/discriminationTactics.mli index f1153256f..5815bb551 100644 --- a/helm/software/components/tactics/discriminationTactics.mli +++ b/helm/software/components/tactics/discriminationTactics.mli @@ -25,6 +25,3 @@ val injection_tac: term:Cic.term -> ProofEngineTypes.tactic val discriminate_tac: term:Cic.term -> ProofEngineTypes.tactic -val decide_equality_tac: ProofEngineTypes.tactic -val compare_tac: term:Cic.term -> ProofEngineTypes.tactic - diff --git a/helm/software/components/tactics/tactics.ml b/helm/software/components/tactics/tactics.ml index fe8adc549..4d5272589 100644 --- a/helm/software/components/tactics/tactics.ml +++ b/helm/software/components/tactics/tactics.ml @@ -32,11 +32,9 @@ let auto = AutoTactic.auto_tac let change = ReductionTactics.change_tac let clear = ProofEngineStructuralRules.clear let clearbody = ProofEngineStructuralRules.clearbody -let compare = DiscriminationTactics.compare_tac let constructor = IntroductionTactics.constructor_tac let contradiction = NegationTactics.contradiction_tac let cut = PrimitiveTactics.cut_tac -let decide_equality = DiscriminationTactics.decide_equality_tac let decompose = EliminationTactics.decompose_tac let demodulate = Saturation.demodulate_tac let discriminate = DiscriminationTactics.discriminate_tac diff --git a/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli index c8c225cdd..211897a8a 100644 --- a/helm/software/components/tactics/tactics.mli +++ b/helm/software/components/tactics/tactics.mli @@ -12,13 +12,11 @@ val change : Cic.lazy_term -> ProofEngineTypes.tactic val clear : hyp:string -> ProofEngineTypes.tactic val clearbody : hyp:string -> ProofEngineTypes.tactic -val compare : term:Cic.term -> ProofEngineTypes.tactic val constructor : n:int -> ProofEngineTypes.tactic val contradiction : ProofEngineTypes.tactic val cut : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> Cic.term -> ProofEngineTypes.tactic -val decide_equality : ProofEngineTypes.tactic val decompose : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> ?user_types:(UriManager.uri * int) list -> diff --git a/helm/software/matita/matita.lang b/helm/software/matita/matita.lang index d02231588..f53d833b6 100644 --- a/helm/software/matita/matita.lang +++ b/helm/software/matita/matita.lang @@ -87,11 +87,9 @@ clear clearbody change - compare constructor contradiction cut - decide equality decompose discriminate elim