X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngine.ml;fp=helm%2FgTopLevel%2FproofEngine.ml;h=0000000000000000000000000000000000000000;hp=491fe5224f2098cf1fc87765a52c62e5e99db4f4;hb=3ef089a4c58fbe429dd539af6215991ecbe11ee2;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml deleted file mode 100644 index 491fe5224..000000000 --- a/helm/gTopLevel/proofEngine.ml +++ /dev/null @@ -1,257 +0,0 @@ -(* Copyright (C) 2000, 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 ProofEngineHelpers -open ProofEngineTypes - - (* proof assistant status *) - -let proof = ref (None : proof option) -let goal = ref (None : goal option) - -let get_current_status_as_xml () = - match !proof with - None -> assert false - | Some (uri, metasenv, bo, ty) -> - let currentproof = - (*CSC: Wrong: [] is just plainly wrong *) - Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[]) - in - let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) = - Cic2acic.acic_object_of_cic_object currentproof - in - let xml, bodyxml = - match - Cic2Xml.print_object uri ~ids_to_inner_sorts - ~ask_dtd_to_the_getter:true acurrentproof - with - xml,Some bodyxml -> xml,bodyxml - | _,None -> assert false - in - (xml, bodyxml) -;; - -let apply_tactic ~tactic = - match !proof,!goal with - | None,_ - | _,None -> assert false - | Some proof', Some goal' -> - let (newproof, newgoals) = tactic ~status:(proof', goal') in - proof := Some newproof; - goal := - (match newgoals, newproof with - goal::_, _ -> Some goal - | [], (_,(goal,_,_)::_,_,_) -> - (* the tactic left no open goal ; let's choose the first open goal *) - (*CSC: here we could implement and use a proof-tree like notion... *) - Some goal - | _, _ -> None) -;; - -(* metas_in_term term *) -(* Returns the ordered list of the metas that occur in [term]. *) -(* Duplicates are removed. The implementation is not very efficient. *) -let metas_in_term term = - let module C = Cic in - let rec aux = - function - C.Rel _ -> [] - | C.Meta (n,_) -> [n] - | C.Sort _ - | C.Implicit -> [] - | C.Cast (te,ty) -> (aux te) @ (aux ty) - | C.Prod (_,s,t) -> (aux s) @ (aux t) - | C.Lambda (_,s,t) -> (aux s) @ (aux t) - | C.LetIn (_,s,t) -> (aux s) @ (aux t) - | C.Appl l -> List.fold_left (fun i t -> i @ (aux t)) [] l - | C.Var (_,exp_named_subst) - | C.Const (_,exp_named_subst) - | C.MutInd (_,_,exp_named_subst) - | C.MutConstruct (_,_,_,exp_named_subst) -> - List.fold_left (fun i (_,t) -> i @ (aux t)) [] exp_named_subst - | C.MutCase (_,_,outt,t,pl) -> - (aux outt) @ (aux t) @ - (List.fold_left (fun i t -> i @ (aux t)) [] pl) - | C.Fix (_,fl) -> - List.fold_left (fun i (_,_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl - | C.CoFix (_,fl) -> - List.fold_left (fun i (_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl - in - let metas = aux term in - let rec elim_duplicates = - function - [] -> [] - | he::tl -> - he::(elim_duplicates (List.filter (function el -> he <> el) tl)) - in - elim_duplicates metas - -(* perforate context term ty *) -(* replaces the term [term] in the proof with a new metavariable whose type *) -(* is [ty]. [context] must be the context of [term] in the whole proof. This *) -(* could be easily computed; so the only reasons to have it as an argument *) -(* are efficiency reasons. *) -let perforate context term ty = - let module C = Cic in - match !proof with - None -> assert false - | Some (uri,metasenv,bo,gty as proof') -> - let newmeta = new_meta proof' in - (* We push the new meta at the end of the list for pretty-printing *) - (* purposes: in this way metas are ordered. *) - let metasenv' = metasenv@[newmeta,context,ty] in - let irl = identity_relocation_list_for_metavariable context in -(*CSC: Bug: se ci sono due term uguali nella prova dovrei bucarne uno solo!!!*) - let bo' = - ProofEngineReduction.replace (==) [term] [C.Meta (newmeta,irl)] bo - in - (* It may be possible that some metavariables occurred only in *) - (* the term we are perforating and they now occurs no more. We *) - (* get rid of them, collecting the really useful metavariables *) - (* in metasenv''. *) -(*CSC: Bug: una meta potrebbe non comparire in bo', ma comparire nel tipo *) -(*CSC: di una metavariabile che compare in bo'!!!!!!! *) - let newmetas = metas_in_term bo' in - let metasenv'' = - List.filter (function (n,_,_) -> List.mem n newmetas) metasenv' - in - proof := Some (uri,metasenv'',bo',gty) ; - goal := Some newmeta - - -(************************************************************) -(* Some easy tactics. *) -(************************************************************) - -(* Reduces [term] using [reduction_function] in the current scratch goal [ty] *) -let reduction_tactic_in_scratch reduction_function terms ty = - let metasenv = - match !proof with - None -> [] - | Some (_,metasenv,_,_) -> metasenv - in - let metano,context,_ = - match !goal with - None -> assert false - | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv - in - let terms' = List.map (reduction_function context) terms in - ProofEngineReduction.replace - ~equality:(==) ~what:terms ~with_what:terms' ~where:ty -;; - -let whd_in_scratch = reduction_tactic_in_scratch CicReduction.whd -let reduce_in_scratch = reduction_tactic_in_scratch ProofEngineReduction.reduce -let simpl_in_scratch = reduction_tactic_in_scratch ProofEngineReduction.simpl - -(************************************************************) -(* Tactics defined elsewhere *) -(************************************************************) - - (* primitive tactics *) - -let apply term = apply_tactic (PrimitiveTactics.apply_tac ~term) -let intros ?mk_fresh_name_callback () = - apply_tactic (PrimitiveTactics.intros_tac ?mk_fresh_name_callback ()) -let cut ?mk_fresh_name_callback term = - apply_tactic (PrimitiveTactics.cut_tac ?mk_fresh_name_callback term) -let letin ?mk_fresh_name_callback term = - apply_tactic (PrimitiveTactics.letin_tac ?mk_fresh_name_callback term) -let exact term = apply_tactic (PrimitiveTactics.exact_tac ~term) -let elim_intros_simpl term = - apply_tactic (PrimitiveTactics.elim_intros_simpl_tac ~term) -let change ~goal_input:what ~input:with_what = - apply_tactic (PrimitiveTactics.change_tac ~what ~with_what) - - (* structural tactics *) - -let clearbody hyp = apply_tactic (ProofEngineStructuralRules.clearbody ~hyp) -let clear hyp = apply_tactic (ProofEngineStructuralRules.clear ~hyp) - - (* reduction tactics *) - -let whd terms = - apply_tactic - (ReductionTactics.whd_tac ~also_in_hypotheses:true ~terms:(Some terms)) -let reduce terms = - apply_tactic - (ReductionTactics.reduce_tac ~also_in_hypotheses:true ~terms:(Some terms)) -let simpl terms = - apply_tactic - (ReductionTactics.simpl_tac ~also_in_hypotheses:true ~terms:(Some terms)) - -let fold_whd term = - apply_tactic - (ReductionTactics.fold_tac ~reduction:CicReduction.whd - ~also_in_hypotheses:true ~term) -let fold_reduce term = - apply_tactic - (ReductionTactics.fold_tac ~reduction:ProofEngineReduction.reduce - ~also_in_hypotheses:true ~term) -let fold_simpl term = - apply_tactic - (ReductionTactics.fold_tac ~reduction:ProofEngineReduction.simpl - ~also_in_hypotheses:true ~term) - - (* other tactics *) - -let elim_type term = apply_tactic (EliminationTactics.elim_type_tac ~term) -let ring () = apply_tactic Ring.ring_tac -let fourier () = apply_tactic FourierR.fourier_tac - -let rewrite_simpl term = apply_tactic (EqualityTactics.rewrite_simpl_tac ~term) -let rewrite_back_simpl term = apply_tactic (EqualityTactics.rewrite_back_simpl_tac ~term) -let replace ~goal_input:what ~input:with_what = - apply_tactic (EqualityTactics.replace_tac ~what ~with_what) - -let reflexivity () = apply_tactic EqualityTactics.reflexivity_tac -let symmetry () = apply_tactic EqualityTactics.symmetry_tac -let transitivity term = apply_tactic (EqualityTactics.transitivity_tac ~term) - -let exists () = apply_tactic IntroductionTactics.exists_tac -let split () = apply_tactic IntroductionTactics.split_tac -let left () = apply_tactic IntroductionTactics.left_tac -let right () = apply_tactic IntroductionTactics.right_tac - -let assumption () = apply_tactic VariousTactics.assumption_tac - -let generalize ?mk_fresh_name_callback terms = - apply_tactic (VariousTactics.generalize_tac ?mk_fresh_name_callback terms) - -let absurd term = apply_tactic (NegationTactics.absurd_tac ~term) -let contradiction () = apply_tactic NegationTactics.contradiction_tac - -let decompose ~uris_choice_callback term = - apply_tactic (EliminationTactics.decompose_tac ~uris_choice_callback term) - -let injection term = apply_tactic (DiscriminationTactics.injection_tac ~term) -let discriminate term = apply_tactic (DiscriminationTactics.discriminate_tac ~term) -let decide_equality () = apply_tactic DiscriminationTactics.decide_equality_tac -let compare term = apply_tactic (DiscriminationTactics.compare_tac ~term) - -(* -let prova_tatticali () = apply_tactic Tacticals.prova_tac -*) -