From: Claudio Sacerdoti Coen Date: Fri, 20 Sep 2002 17:30:57 +0000 (+0000) Subject: change code moved to change_tac (functional version defined in primitiveTactics) X-Git-Tag: BEFORE_METADATA_FOR_SORT_AND_REL~66 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d5c0d882413668e6569df55f501efe92cf3bf100;p=helm.git change code moved to change_tac (functional version defined in primitiveTactics) --- diff --git a/helm/gTopLevel/primitiveTactics.ml b/helm/gTopLevel/primitiveTactics.ml index 75f421ced..bf65d1a7b 100644 --- a/helm/gTopLevel/primitiveTactics.ml +++ b/helm/gTopLevel/primitiveTactics.ml @@ -477,3 +477,41 @@ da subst1!!!! Dovrei rimuoverle o sono innocue?*) in (newproof, List.map (function (i,_,_) -> i) new_uninstantiatedmetas) + + +exception NotConvertible + +(*CSC: Bug (or feature?). [with_what] is parsed in the context of the goal, *) +(*CSC: while [what] can have a richer context (because of binders) *) +(*CSC: So it is _NOT_ possible to use those binders in the [with_what] term. *) +(*CSC: Is that evident? Is that right? Or should it be changed? *) +let change_tac ~what ~with_what ~status:(proof, goal) = + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + (* are_convertible works only on well-typed terms *) + ignore (CicTypeChecker.type_of_aux' metasenv context with_what) ; + if CicReduction.are_convertible context what with_what then + begin + let replace = + ProofEngineReduction.replace ~equality:(==) ~what ~with_what + in + let ty' = replace ty in + let context' = + List.map + (function + Some (name,Cic.Def t) -> Some (name,Cic.Def (replace t)) + | Some (name,Cic.Decl t) -> Some (name,Cic.Decl (replace t)) + | None -> None + ) context + in + let metasenv' = + List.map + (function + (n,_,_) when n = metano -> (metano,context',ty') + | _ as t -> t + ) metasenv + in + (curi,metasenv',pbo,pty), [metano] + end + else + raise (ProofEngineTypes.Fail "Not convertible") diff --git a/helm/gTopLevel/primitiveTactics.mli b/helm/gTopLevel/primitiveTactics.mli index 123b3859d..93db3ea10 100644 --- a/helm/gTopLevel/primitiveTactics.mli +++ b/helm/gTopLevel/primitiveTactics.mli @@ -1,3 +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 apply_tac: term: Cic.term -> ProofEngineTypes.tactic val exact_tac: @@ -11,3 +36,6 @@ val letin_tac: val elim_intros_simpl_tac: term: Cic.term -> ProofEngineTypes.tactic + +val change_tac: + what: Cic.term -> with_what: Cic.term -> ProofEngineTypes.tactic diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index 69e8062ee..0e4de4f3b 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -246,53 +246,6 @@ let fold term = proof := Some (curi,metasenv',pbo,pty) ; goal := Some metano -exception NotConvertible - -(*CSC: Bug (or feature?). [input] is parsed in the context of the goal, *) -(*CSC: while [goal_input] can have a richer context (because of binders) *) -(*CSC: So it is _NOT_ possible to use those binders in the [input] term. *) -(*CSC: Is that evident? Is that right? Or should it be changed? *) -let change ~goal_input ~input = - let curi,metasenv,pbo,pty = - match !proof with - None -> assert false - | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty - in - let metano,context,ty = - match !goal with - None -> assert false - | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv - in - (* are_convertible works only on well-typed terms *) - ignore (CicTypeChecker.type_of_aux' metasenv context input) ; - if CicReduction.are_convertible context goal_input input then - begin - let replace = - ProofEngineReduction.replace - ~equality:(==) ~what:goal_input ~with_what:input - in - let ty' = replace ty in - let context' = - List.map - (function - Some (name,Cic.Def t) -> Some (name,Cic.Def (replace t)) - | Some (name,Cic.Decl t) -> Some (name,Cic.Decl (replace t)) - | None -> None - ) context - in - let metasenv' = - List.map - (function - (n,_,_) when n = metano -> (metano,context',ty') - | _ as t -> t - ) metasenv - in - proof := Some (curi,metasenv',pbo,pty) ; - goal := Some metano - end - else - raise NotConvertible - (************************************************************) (* Tactics defined elsewhere *) (************************************************************) @@ -307,6 +260,8 @@ 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 change ~goal_input:what ~input:with_what = + apply_tactic (PrimitiveTactics.change_tac ~what ~with_what) (* structural tactics *) diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli index f9233ea05..fed8d04ad 100644 --- a/helm/gTopLevel/proofEngine.mli +++ b/helm/gTopLevel/proofEngine.mli @@ -23,8 +23,6 @@ * http://cs.unibo.it/helm/. *) -exception NotConvertible - (* proof engine status *) val proof : ProofEngineTypes.proof option ref val goal : ProofEngineTypes.goal option ref @@ -37,7 +35,6 @@ val whd : Cic.term -> unit val reduce : Cic.term -> unit val simpl : Cic.term -> unit val fold : Cic.term -> unit -val change : goal_input:Cic.term -> input:Cic.term -> unit (* scratch area reduction tactics *) val whd_in_scratch : Cic.term -> Cic.term -> Cic.term @@ -51,6 +48,7 @@ val cut : Cic.term -> unit val letin : Cic.term -> unit val exact : Cic.term -> unit val elim_intros_simpl : Cic.term -> unit +val change : goal_input:Cic.term -> input:Cic.term -> unit (* structural tactics *) val clearbody : Cic.hypothesis -> unit