From 989a5444a5162ba9259858a25a1dadab300291a3 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 4 Nov 2002 13:47:33 +0000 Subject: [PATCH] The reduction tactics are now shared between ReductionTactics and ProofEngine. --- helm/gTopLevel/fourierR.ml | 5 ++- helm/gTopLevel/primitiveTactics.ml | 3 +- helm/gTopLevel/proofEngine.ml | 65 +++++------------------------ helm/gTopLevel/reductionTactics.ml | 51 ++++++++++++++++++++++ helm/gTopLevel/reductionTactics.mli | 11 +++-- 5 files changed, 76 insertions(+), 59 deletions(-) diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index 62e5d0f9a..66e895119 100644 --- a/helm/gTopLevel/fourierR.ml +++ b/helm/gTopLevel/fourierR.ml @@ -80,7 +80,10 @@ prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred); let rewrite_simpl_tac ~term ~status = - Tacticals.then_ ~start:(rewrite_tac ~term) ~continuation:ReductionTactics.simpl_tac ~status + Tacticals.then_ ~start:(rewrite_tac ~term) + ~continuation: + (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None) + ~status ;; (******************** THE FOURIER TACTIC ***********************) diff --git a/helm/gTopLevel/primitiveTactics.ml b/helm/gTopLevel/primitiveTactics.ml index 9974577a0..8491155ad 100644 --- a/helm/gTopLevel/primitiveTactics.ml +++ b/helm/gTopLevel/primitiveTactics.ml @@ -506,7 +506,8 @@ da subst1!!!! Dovrei rimuoverle o sono innocue?*) let elim_simpl_intros_tac ~term = Tacticals.then_ ~start:(elim_tac ~term) ~continuation: - (Tacticals.then_ ~start:ReductionTactics.simpl_tac + (Tacticals.then_ + ~start:(ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None) ~continuation:(intros_tac ~name:"FOO")) ;; diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index 788e46bd1..55531c2aa 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -144,56 +144,6 @@ in incr next_fresh_index ; "fresh_name" ^ string_of_int !next_fresh_index -let reduction_tactic reduction_function term = - 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 - (* We don't know if [term] is a subterm of [ty] or a subterm of *) - (* the type of one metavariable. So we replace it everywhere. *) - (*CSC: Il vero problema e' che non sapendo dove sia il term non *) - (*CSC: sappiamo neppure quale sia il suo contesto!!!! Insomma, *) - (*CSC: e' meglio prima cercare il termine e scoprirne il *) - (*CSC: contesto, poi ridurre e infine rimpiazzare. *) - let replace context where= -(*CSC: Per il momento se la riduzione fallisce significa solamente che *) -(*CSC: siamo nel contesto errato. Metto il try, ma che schifo!!!! *) -(*CSC: Anche perche' cosi' catturo anche quelle del replace che non dovrei *) - try - let term' = reduction_function context term in - ProofEngineReduction.replace ~equality:(==) ~what:term ~with_what:term' - ~where:where - with - _ -> where - in - let ty' = replace context ty in - let context' = - List.fold_right - (fun entry context -> - match entry with - Some (name,Cic.Def t) -> - (Some (name,Cic.Def (replace context t)))::context - | Some (name,Cic.Decl t) -> - (Some (name,Cic.Decl (replace context t)))::context - | None -> None::context - ) 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 - (* Reduces [term] using [reduction_function] in the current scratch goal [ty] *) let reduction_tactic_in_scratch reduction_function term ty = let metasenv = @@ -209,10 +159,7 @@ let reduction_tactic_in_scratch reduction_function term ty = let term' = reduction_function context term in ProofEngineReduction.replace ~equality:(==) ~what:term ~with_what:term' ~where:ty - -let whd = reduction_tactic CicReduction.whd -let reduce = reduction_tactic ProofEngineReduction.reduce -let simpl = reduction_tactic ProofEngineReduction.simpl +;; let whd_in_scratch = reduction_tactic_in_scratch CicReduction.whd let reduce_in_scratch = reduction_tactic_in_scratch ProofEngineReduction.reduce @@ -243,6 +190,16 @@ let clear hyp = apply_tactic (ProofEngineStructuralRules.clear ~hyp) (* reduction tactics *) +let whd term = + apply_tactic + (ReductionTactics.whd_tac ~also_in_hypotheses:true ~term:(Some term)) +let reduce term = + apply_tactic + (ReductionTactics.reduce_tac ~also_in_hypotheses:true ~term:(Some term)) +let simpl term = + apply_tactic + (ReductionTactics.simpl_tac ~also_in_hypotheses:true ~term:(Some term)) + let fold term = apply_tactic (ReductionTactics.fold_tac ~also_in_hypotheses:true ~term) diff --git a/helm/gTopLevel/reductionTactics.ml b/helm/gTopLevel/reductionTactics.ml index c15598cac..0080e4571 100644 --- a/helm/gTopLevel/reductionTactics.ml +++ b/helm/gTopLevel/reductionTactics.ml @@ -23,6 +23,7 @@ * 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 @@ -36,6 +37,56 @@ let reduction_tac ~reduction ~status:(proof,goal) = in (curi,new_metasenv,pbo,pty), [metano] ;; +*) + +(* The default of term is the thesis of the goal to be prooved *) +let reduction_tac ~also_in_hypotheses ~reduction ~term ~status:(proof,goal) = + let curi,metasenv,pbo,pty = proof in + let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in + let term = + match term with None -> ty | Some t -> t + in + (* We don't know if [term] is a subterm of [ty] or a subterm of *) + (* the type of one metavariable. So we replace it everywhere. *) + (*CSC: Il vero problema e' che non sapendo dove sia il term non *) + (*CSC: sappiamo neppure quale sia il suo contesto!!!! Insomma, *) + (*CSC: e' meglio prima cercare il termine e scoprirne il *) + (*CSC: contesto, poi ridurre e infine rimpiazzare. *) + let replace context where= +(*CSC: Per il momento se la riduzione fallisce significa solamente che *) +(*CSC: siamo nel contesto errato. Metto il try, ma che schifo!!!! *) +(*CSC: Anche perche' cosi' catturo anche quelle del replace che non dovrei *) + try + let term' = reduction context term in + ProofEngineReduction.replace ~equality:(==) ~what:term ~with_what:term' + ~where:where + with + _ -> where + in + let ty' = replace context ty in + let context' = + if also_in_hypotheses then + List.fold_right + (fun entry context -> + match entry with + Some (name,Cic.Def t) -> + (Some (name,Cic.Def (replace context t)))::context + | Some (name,Cic.Decl t) -> + (Some (name,Cic.Decl (replace context t)))::context + | None -> None::context + ) context [] + else + context + in + let metasenv' = + List.map + (function + (n,_,_) when n = metano -> (metano,context',ty') + | _ as t -> t + ) metasenv + in + (curi,metasenv',pbo,pty), [metano] +;; let simpl_tac = reduction_tac ~reduction:ProofEngineReduction.simpl ;; let reduce_tac = reduction_tac ~reduction:ProofEngineReduction.reduce ;; diff --git a/helm/gTopLevel/reductionTactics.mli b/helm/gTopLevel/reductionTactics.mli index a4cf407f0..00784be7e 100644 --- a/helm/gTopLevel/reductionTactics.mli +++ b/helm/gTopLevel/reductionTactics.mli @@ -23,8 +23,13 @@ * http://cs.unibo.it/helm/. *) -val simpl_tac: ProofEngineTypes.tactic -val reduce_tac: ProofEngineTypes.tactic -val whd_tac: ProofEngineTypes.tactic +(* The default of term is the thesis of the goal to be prooved *) +val simpl_tac: + also_in_hypotheses:bool -> term:(Cic.term option) -> ProofEngineTypes.tactic +val reduce_tac: + also_in_hypotheses:bool -> term:(Cic.term option) -> ProofEngineTypes.tactic +val whd_tac: + also_in_hypotheses:bool -> term:(Cic.term option) -> ProofEngineTypes.tactic + val fold_tac: also_in_hypotheses:bool -> term:Cic.term -> ProofEngineTypes.tactic -- 2.39.2