From: Claudio Sacerdoti Coen Date: Thu, 31 Oct 2002 14:09:52 +0000 (+0000) Subject: - ElimIntrosSimpl now implemented using tacticals. It becomes an X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3066e4dcb7270a5eb20020a91d45da9eb87e2f2e;p=helm.git - ElimIntrosSimpl now implemented using tacticals. It becomes an ElimSimplIntros (which does lambda-abstraction with the reduced type ;-((( To be fixed. - reductionTactics now also have the usual interface for tactics --- diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend index 2b88f0c85..bcf5bbd72 100644 --- a/helm/gTopLevel/.depend +++ b/helm/gTopLevel/.depend @@ -9,14 +9,19 @@ proofEngineStructuralRules.cmo: proofEngineTypes.cmo \ proofEngineStructuralRules.cmx: proofEngineTypes.cmx \ proofEngineStructuralRules.cmi proofEngineStructuralRules.cmi: proofEngineTypes.cmo +tacticals.cmo: proofEngineTypes.cmo tacticals.cmi +tacticals.cmx: proofEngineTypes.cmx tacticals.cmi +tacticals.cmi: proofEngineTypes.cmo +reductionTactics.cmo: proofEngineReduction.cmi reductionTactics.cmi +reductionTactics.cmx: proofEngineReduction.cmx reductionTactics.cmi +reductionTactics.cmi: proofEngineTypes.cmo primitiveTactics.cmo: proofEngineHelpers.cmi proofEngineReduction.cmi \ - proofEngineTypes.cmo primitiveTactics.cmi + proofEngineTypes.cmo reductionTactics.cmi tacticals.cmi \ + primitiveTactics.cmi primitiveTactics.cmx: proofEngineHelpers.cmx proofEngineReduction.cmx \ - proofEngineTypes.cmx primitiveTactics.cmi + proofEngineTypes.cmx reductionTactics.cmx tacticals.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 tacticals.cmi ring.cmi ring.cmx: primitiveTactics.cmx proofEngineStructuralRules.cmx \ diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index 403b8b180..b2680c27b 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -17,7 +17,8 @@ opt: gTopLevel.opt DEPOBJS = xml2Gdome.ml xml2Gdome.mli proofEngineTypes.ml proofEngineHelpers.ml \ proofEngineReduction.ml proofEngineReduction.mli \ proofEngineStructuralRules.ml proofEngineStructuralRules.mli \ - primitiveTactics.ml primitiveTactics.mli tacticals.ml tacticals.mli \ + tacticals.ml tacticals.mli reductionTactics.ml reductionTactics.mli \ + primitiveTactics.ml primitiveTactics.mli \ ring.ml ring.mli fourier.ml fourierR.ml fourierR.mli\ proofEngine.ml proofEngine.mli \ doubleTypeInference.ml doubleTypeInference.mli cic2acic.ml \ @@ -27,8 +28,8 @@ DEPOBJS = xml2Gdome.ml xml2Gdome.mli proofEngineTypes.ml proofEngineHelpers.ml \ TOPLEVELOBJS = xml2Gdome.cmo proofEngineTypes.cmo proofEngineHelpers.cmo \ proofEngineReduction.cmo proofEngineStructuralRules.cmo \ - primitiveTactics.cmo tacticals.cmo ring.cmo \ - fourier.cmo fourierR.cmo proofEngine.cmo \ + tacticals.cmo reductionTactics.cmo primitiveTactics.cmo \ + ring.cmo fourier.cmo fourierR.cmo proofEngine.cmo \ doubleTypeInference.cmo cic2acic.cmo cic2Xml.cmo \ logicalOperations.cmo sequentPp.cmo mQueryGenerator.cmo \ gTopLevel.cmo diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index 670978e5c..c8c856459 100644 --- a/helm/gTopLevel/fourierR.ml +++ b/helm/gTopLevel/fourierR.ml @@ -78,33 +78,9 @@ prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred); (proof',[fresh_meta]) ;; - - -let simpl_tac ~status:(proof,goal) = - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in - -prerr_endline("simpl_tac su "^CicPp.ppterm ty); - - let new_ty = ProofEngineReduction.simpl context ty in - -prerr_endline("ritorna "^CicPp.ppterm new_ty); - - let new_metasenv = - List.map - (function - (n,_,_) when n = metano -> (metano,context,new_ty) - | _ as t -> t - ) metasenv - in - (curi,new_metasenv,pbo,pty), [metano] - -;; - -let rewrite_simpl_tac ~term ~status = - - Tacticals.then_ ~start:(rewrite_tac ~term) ~continuation:simpl_tac ~status - +let rewrite_simpl_tac ~term = + Tacticals.then_ ~start:(rewrite_tac ~term) + ~continuation:ReductionTactics.simpl_tac ;; (******************** THE FOURIER TACTIC ***********************) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 85f56c155..d0aef1a04 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -707,8 +707,8 @@ let exact rendering_window = let apply rendering_window = call_tactic_with_input ProofEngine.apply rendering_window ;; -let elimintrossimpl rendering_window = - call_tactic_with_input ProofEngine.elim_intros_simpl rendering_window +let elimsimplintros rendering_window = + call_tactic_with_input ProofEngine.elim_simpl_intros rendering_window ;; let elimtype rendering_window = call_tactic_with_input ProofEngine.elim_type rendering_window @@ -1548,8 +1548,8 @@ class rendering_window output proofw (label : GMisc.label) = let applyb = GButton.button ~label:"Apply" ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in - let elimintrossimplb = - GButton.button ~label:"ElimIntrosSimpl" + let elimsimplintrosb = + GButton.button ~label:"ElimSimplIntros" ~packing:(hbox3#pack ~expand:false ~fill:false ~padding:5) () in let elimtypeb = GButton.button ~label:"ElimType" @@ -1633,7 +1633,7 @@ object(self) ignore(searchpatternb#connect#clicked (searchPattern self)) ; ignore(exactb#connect#clicked (exact self)) ; ignore(applyb#connect#clicked (apply self)) ; - ignore(elimintrossimplb#connect#clicked (elimintrossimpl self)) ; + ignore(elimsimplintrosb#connect#clicked (elimsimplintros self)) ; ignore(elimtypeb#connect#clicked (elimtype self)) ; ignore(whdb#connect#clicked (whd self)) ; ignore(reduceb#connect#clicked (reduce self)) ; diff --git a/helm/gTopLevel/primitiveTactics.ml b/helm/gTopLevel/primitiveTactics.ml index 25d8899d7..21d5d67c6 100644 --- a/helm/gTopLevel/primitiveTactics.ml +++ b/helm/gTopLevel/primitiveTactics.ml @@ -31,9 +31,6 @@ exception NotTheRightEliminatorShape exception NoHypothesesFound exception WrongUriToVariable of string -(* TODO problemone del fresh_name, aggiungerlo allo status? *) -let fresh_name () = "FOO" - (* lambda_abstract newmeta ty *) (* returns a triple [bo],[context],[ty'] where *) (* [ty] = Pi/LetIn [context].[ty'] ([context] is a vector!) *) @@ -122,36 +119,6 @@ let eta_expand metasenv context t arg = in (C.Appl [C.Lambda ((C.Name "dummy"),argty,aux 0 t) ; arg]) -(*CSC: The call to the Intros tactic is embedded inside the code of the *) -(*CSC: Elim tactic. Do we already need tacticals? *) -(* Auxiliary function for apply: given a type (a backbone), it returns its *) -(* head, a META environment in which there is new a META for each hypothesis,*) -(* a list of arguments for the new applications and the indexes of the first *) -(* and last new METAs introduced. The nth argument in the list of arguments *) -(* is the nth new META lambda-abstracted as much as possible. Hence, this *) -(* functions already provides the behaviour of Intros on the new goals. *) -let new_metasenv_for_apply_intros proof context ty = - let module C = Cic in - let module S = CicSubstitution in - let rec aux newmeta = - function - C.Cast (he,_) -> aux newmeta he - | C.Prod (name,s,t) -> - let newcontext,ty',newargument = - lambda_abstract context newmeta s (fresh_name ()) - in - let (res,newmetasenv,arguments,lastmeta) = - aux (newmeta + 1) (S.subst newargument t) - in - res,(newmeta,newcontext,ty')::newmetasenv,newargument::arguments,lastmeta - | t -> t,[],[],newmeta - in - let newmeta = new_meta ~proof in - (* WARNING: here we are using the invariant that above the most *) - (* recente new_meta() there are no used metas. *) - let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in - res,newmetasenv,arguments,newmeta,lastmeta - (*CSC: ma serve solamente la prima delle new_uninst e l'unione delle due!!! *) let classify_metas newmeta in_subst_domain subst_in metasenv = List.fold_right @@ -409,9 +376,9 @@ let exact_tac ~term ~status:(proof, goal) = raise (Fail "The type of the provided term is not the one expected.") -(* not really "primite" tactics .... *) +(* not really "primitive" tactics .... *) -let elim_intros_simpl_tac ~term ~status:(proof, goal) = +let elim_tac ~term ~status:(proof, goal) = let module T = CicTypeChecker in let module U = UriManager in let module R = CicReduction in @@ -424,10 +391,7 @@ let elim_intros_simpl_tac ~term ~status:(proof, goal) = C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[]) | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) -> (uri,exp_named_subst,typeno,args) - | _ -> - prerr_endline ("MALFATTORE" ^ (CicPp.ppterm termty)); - flush stderr; - raise NotAnInductiveTypeToEliminate + | _ -> raise NotAnInductiveTypeToEliminate in let eliminator_uri = let buri = U.buri_of_uri uri in @@ -447,16 +411,11 @@ let elim_intros_simpl_tac ~term ~status:(proof, goal) = in U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con") in -(*CSC: BUG HERE!!! [] MUST BE COMPUTED SOMEHOW. USING UNIFICATION? *) - let eliminator_ref = C.Const (eliminator_uri,[]) in - let ety = - T.type_of_aux' [] [] eliminator_ref - in - let (econclusion,newmetas,arguments,newmeta,lastmeta) = -(* - new_metasenv_for_apply context ety -*) - new_metasenv_for_apply_intros proof context ety + let eliminator_ref = C.Const (eliminator_uri,exp_named_subst) in + let ety = T.type_of_aux' metasenv context eliminator_ref in + let newmeta = new_meta ~proof in + let (econclusion,newmetas,arguments,lastmeta) = + new_metasenv_for_apply newmeta proof context ety in (* Here we assume that we have only one inductive hypothesis to *) (* eliminate and that it is the last hypothesis of the theorem. *) @@ -485,22 +444,8 @@ let elim_intros_simpl_tac ~term ~status:(proof, goal) = (* to refine the term. *) let emeta, fargs = match ueconclusion with -(*CSC: Code to be used for Apply C.Appl ((C.Meta (emeta,_))::fargs) -> emeta,fargs | C.Meta (emeta,_) -> emeta,[] -*) -(*CSC: Code to be used for ApplyIntros *) - C.Appl (he::fargs) -> - let rec find_head = - function - C.Meta (emeta,_) -> emeta - | C.Lambda (_,_,t) -> find_head t - | C.LetIn (_,_,t) -> find_head t - | _ ->raise NotTheRightEliminatorShape - in - find_head he,fargs - | C.Meta (emeta,_) -> emeta,[] -(* *) | _ -> raise NotTheRightEliminatorShape in let ty' = CicUnification.apply_subst subst1 ty in @@ -519,7 +464,6 @@ da subst1!!!! Dovrei rimuoverle o sono innocue?*) List.exists eq_to_i subst1 || List.exists eq_to_i subst2 in -(*CSC: codice per l'elim (* When unwinding the META that corresponds to the elimination *) (* predicate (which is emeta), we must also perform one-step *) (* beta-reduction. apply_subst doesn't need the context. Hence *) @@ -529,13 +473,6 @@ da subst1!!!! Dovrei rimuoverle o sono innocue?*) CicUnification.apply_subst_reducing subst2 (Some (emeta,List.length fargs)) t' in -*) -(*CSC: codice per l'elim_intros_simpl. Non effettua semplificazione. *) - let apply_subst context t = - let t' = CicUnification.apply_subst (subst1@subst2) t in - ProofEngineReduction.simpl context t' - in -(* *) let old_uninstantiatedmetas,new_uninstantiatedmetas = classify_metas newmeta in_subst_domain apply_subst newmetasenv'' @@ -553,25 +490,25 @@ da subst1!!!! Dovrei rimuoverle o sono innocue?*) (* we also substitute metano with bo'. *) (*CSC: Nota: sostituire nuovamente subst1 e' superfluo, *) (*CSC: no? *) -(*CSC: codice per l'elim let apply_subst' t = let t' = CicUnification.apply_subst subst1 t in CicUnification.apply_subst_reducing ((metano,bo')::subst2) (Some (emeta,List.length fargs)) t' in -*) -(*CSC: codice per l'elim_intros_simpl *) - let apply_subst' t = - CicUnification.apply_subst - ((metano,bo')::(subst1@subst2)) t - in -(* *) subst_meta_and_metasenv_in_proof proof metano apply_subst' newmetasenv''' in (newproof, List.map (function (i,_,_) -> i) new_uninstantiatedmetas) +;; + +let elim_simpl_intros_tac ~term = + Tacticals.then_ ~start:(elim_tac ~term) + ~continuation: + (Tacticals.then_ ~start:ReductionTactics.simpl_tac + ~continuation:(intros_tac ~name:"FOO")) +;; exception NotConvertible diff --git a/helm/gTopLevel/primitiveTactics.mli b/helm/gTopLevel/primitiveTactics.mli index 93db3ea10..b23e4005f 100644 --- a/helm/gTopLevel/primitiveTactics.mli +++ b/helm/gTopLevel/primitiveTactics.mli @@ -34,7 +34,7 @@ val cut_tac: val letin_tac: term: Cic.term -> ProofEngineTypes.tactic -val elim_intros_simpl_tac: +val elim_simpl_intros_tac: term: Cic.term -> ProofEngineTypes.tactic val change_tac: diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index 94cc5bd5e..972ae962a 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -272,8 +272,8 @@ let intros () = let cut term = apply_tactic (PrimitiveTactics.cut_tac ~term) let letin term = apply_tactic (PrimitiveTactics.letin_tac ~term) let exact term = apply_tactic (PrimitiveTactics.exact_tac ~term) -let elim_intros_simpl term = - apply_tactic (PrimitiveTactics.elim_intros_simpl_tac ~term) +let elim_simpl_intros term = + apply_tactic (PrimitiveTactics.elim_simpl_intros_tac ~term) let change ~goal_input:what ~input:with_what = apply_tactic (PrimitiveTactics.change_tac ~what ~with_what) diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli index b17ba48ba..c3b623c08 100644 --- a/helm/gTopLevel/proofEngine.mli +++ b/helm/gTopLevel/proofEngine.mli @@ -48,7 +48,7 @@ val intros : unit -> unit val cut : Cic.term -> unit val letin : Cic.term -> unit val exact : Cic.term -> unit -val elim_intros_simpl : Cic.term -> unit +val elim_simpl_intros : Cic.term -> unit val change : goal_input:Cic.term -> input:Cic.term -> unit (* structural tactics *) diff --git a/helm/gTopLevel/reductionTactics.ml b/helm/gTopLevel/reductionTactics.ml new file mode 100644 index 000000000..0e5688e02 --- /dev/null +++ b/helm/gTopLevel/reductionTactics.ml @@ -0,0 +1,42 @@ +(* 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 reduction_tac ~reduction ~status:(proof,goal) = + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let new_ty = reduction context ty in + let new_metasenv = + List.map + (function + (n,_,_) when n = metano -> (metano,context,new_ty) + | _ as t -> t + ) metasenv + in + (curi,new_metasenv,pbo,pty), [metano] +;; + +let simpl_tac = reduction_tac ~reduction:ProofEngineReduction.simpl ;; +let reduce_tac = reduction_tac ~reduction:ProofEngineReduction.reduce ;; +let whd_tac = reduction_tac ~reduction:CicReduction.whd ;; diff --git a/helm/gTopLevel/reductionTactics.mli b/helm/gTopLevel/reductionTactics.mli new file mode 100644 index 000000000..97418b4da --- /dev/null +++ b/helm/gTopLevel/reductionTactics.mli @@ -0,0 +1,28 @@ +(* 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 simpl_tac: ProofEngineTypes.tactic +val reduce_tac: ProofEngineTypes.tactic +val whd_tac: ProofEngineTypes.tactic diff --git a/helm/gTopLevel/ring.ml b/helm/gTopLevel/ring.ml index 1d614b6f6..d30df1aaa 100644 --- a/helm/gTopLevel/ring.ml +++ b/helm/gTopLevel/ring.ml @@ -414,7 +414,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_intros_simpl_tac ~term:(Cic.Rel 1) ; id_tac] ~status + ~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; id_tac] ~status (** auxiliary tactic, use elim_type and try to close 2nd subgoal using proof diff --git a/helm/gTopLevel/tacticals.ml b/helm/gTopLevel/tacticals.ml index b8490f059..2c1b1883b 100644 --- a/helm/gTopLevel/tacticals.ml +++ b/helm/gTopLevel/tacticals.ml @@ -24,14 +24,13 @@ *) open CicReduction -open PrimitiveTactics open ProofEngineTypes open UriManager (** DEBUGGING *) (** perform debugging output? *) -let debug = true +let debug = false (** debugging print *) let warn s =