From 146f8a58cd8c9aebe3d49df7f09e921f43c0c0e8 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 29 Jan 2003 13:20:00 +0000 Subject: [PATCH] All the reduction tactics have been modified to reduce several (sub)terms at once. --- helm/ocaml/tactics/equalityTactics.ml | 4 +- helm/ocaml/tactics/primitiveTactics.ml | 5 +- helm/ocaml/tactics/proofEngineReduction.ml | 104 +++++++++++--------- helm/ocaml/tactics/proofEngineReduction.mli | 3 +- helm/ocaml/tactics/reductionTactics.ml | 12 +-- helm/ocaml/tactics/reductionTactics.mli | 9 +- 6 files changed, 78 insertions(+), 59 deletions(-) diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml index 29df82c08..c1212360c 100644 --- a/helm/ocaml/tactics/equalityTactics.ml +++ b/helm/ocaml/tactics/equalityTactics.ml @@ -81,7 +81,7 @@ let rewrite_simpl_tac ~term ~status = Tacticals.then_ ~start:(rewrite_tac ~term) ~continuation: - (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None) + (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None) ~status ;; @@ -144,7 +144,7 @@ let rewrite_back_simpl_tac ~term ~status = Tacticals.then_ ~start:(rewrite_back_tac ~term) ~continuation: - (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None) + (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None) ~status ;; diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index 8abaae1b8..91cd6198e 100644 --- a/helm/ocaml/tactics/primitiveTactics.ml +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -523,7 +523,7 @@ let elim_intros_simpl_tac ~term = (Tacticals.thens ~start:(intros_tac ()) ~continuations: - [ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None]) + [ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None]) ;; exception NotConvertible @@ -540,7 +540,8 @@ let change_tac ~what ~with_what ~status:(proof, goal) = if CicReduction.are_convertible context what with_what then begin let replace = - ProofEngineReduction.replace ~equality:(==) ~what ~with_what + ProofEngineReduction.replace + ~equality:(==) ~what:[what] ~with_what:[with_what] in let ty' = replace ty in let context' = diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml index 710a48164..a51ab3909 100644 --- a/helm/ocaml/tactics/proofEngineReduction.ml +++ b/helm/ocaml/tactics/proofEngineReduction.ml @@ -117,53 +117,67 @@ let alpha_equivalence = aux ;; -(* "textual" replacement of a subterm with another one *) +exception WhatAndWithWhatDoNotHaveTheSameLength;; + +(* "textual" replacement of several subterms with other ones *) let replace ~equality ~what ~with_what ~where = let module C = Cic in - let rec aux = - function - t when (equality t what) -> with_what - | C.Rel _ as t -> t - | C.Var (uri,exp_named_subst) -> - C.Var (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst) - | C.Meta _ as t -> t - | C.Sort _ as t -> t - | C.Implicit as t -> t - | C.Cast (te,ty) -> C.Cast (aux te, aux ty) - | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t) - | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t) - | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t) - | C.Appl l -> - (* Invariant enforced: no application of an application *) - (match List.map aux l with - (C.Appl l')::tl -> C.Appl (l'@tl) - | l' -> C.Appl l') - | C.Const (uri,exp_named_subst) -> - C.Const (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst) - | C.MutInd (uri,i,exp_named_subst) -> - C.MutInd - (uri,i,List.map (function (uri,t) -> uri, aux t) exp_named_subst) - | C.MutConstruct (uri,i,j,exp_named_subst) -> - C.MutConstruct - (uri,i,j,List.map (function (uri,t) -> uri, aux t) exp_named_subst) - | C.MutCase (sp,i,outt,t,pl) -> - C.MutCase (sp,i,aux outt, aux t,List.map aux pl) - | C.Fix (i,fl) -> - let substitutedfl = - List.map - (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo)) - fl - in - C.Fix (i, substitutedfl) - | C.CoFix (i,fl) -> - let substitutedfl = - List.map - (fun (name,ty,bo) -> (name, aux ty, aux bo)) - fl - in - C.CoFix (i, substitutedfl) + let find_image t = + let rec find_image_aux = + function + [],[] -> raise Not_found + | what::tl1,with_what::tl2 -> + if equality t what then with_what else find_image_aux (tl1,tl2) + | _,_ -> raise WhatAndWithWhatDoNotHaveTheSameLength + in + find_image_aux (what,with_what) in - aux where + let rec aux t = + try + find_image t + with Not_found -> + match t with + C.Rel _ -> t + | C.Var (uri,exp_named_subst) -> + C.Var (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst) + | C.Meta _ -> t + | C.Sort _ -> t + | C.Implicit as t -> t + | C.Cast (te,ty) -> C.Cast (aux te, aux ty) + | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t) + | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t) + | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t) + | C.Appl l -> + (* Invariant enforced: no application of an application *) + (match List.map aux l with + (C.Appl l')::tl -> C.Appl (l'@tl) + | l' -> C.Appl l') + | C.Const (uri,exp_named_subst) -> + C.Const (uri,List.map (function (uri,t) -> uri, aux t) exp_named_subst) + | C.MutInd (uri,i,exp_named_subst) -> + C.MutInd + (uri,i,List.map (function (uri,t) -> uri, aux t) exp_named_subst) + | C.MutConstruct (uri,i,j,exp_named_subst) -> + C.MutConstruct + (uri,i,j,List.map (function (uri,t) -> uri, aux t) exp_named_subst) + | C.MutCase (sp,i,outt,t,pl) -> + C.MutCase (sp,i,aux outt, aux t,List.map aux pl) + | C.Fix (i,fl) -> + let substitutedfl = + List.map + (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo)) + fl + in + C.Fix (i, substitutedfl) + | C.CoFix (i,fl) -> + let substitutedfl = + List.map + (fun (name,ty,bo) -> (name, aux ty, aux bo)) + fl + in + C.CoFix (i, substitutedfl) + in + aux where ;; (* replaces in a term a term with another one. *) @@ -810,7 +824,7 @@ let simpl context = let simplified_term_to_fold = reduceaux context [] delta_expanded_term_to_fold in - replace (=) simplified_term_to_fold term_to_fold res + replace (=) [simplified_term_to_fold] [term_to_fold] res with WrongShape -> (* The constant does not unfold to a Fix lambda-abstracted *) diff --git a/helm/ocaml/tactics/proofEngineReduction.mli b/helm/ocaml/tactics/proofEngineReduction.mli index 91bce1a39..2c210b677 100644 --- a/helm/ocaml/tactics/proofEngineReduction.mli +++ b/helm/ocaml/tactics/proofEngineReduction.mli @@ -32,11 +32,12 @@ exception WrongUriToInductiveDefinition exception RelToHiddenHypothesis exception WrongShape exception AlreadySimplified +exception WhatAndWithWhatDoNotHaveTheSameLength;; val alpha_equivalence: Cic.term -> Cic.term -> bool val replace : equality:(Cic.term -> 'a -> bool) -> - what:'a -> with_what:Cic.term -> where:Cic.term -> Cic.term + what:'a list -> with_what:Cic.term list -> where:Cic.term -> Cic.term val replace_lifting : equality:(Cic.term -> Cic.term -> bool) -> what:Cic.term -> with_what:Cic.term -> where:Cic.term -> Cic.term diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml index 54b439b25..b29873a1f 100644 --- a/helm/ocaml/tactics/reductionTactics.ml +++ b/helm/ocaml/tactics/reductionTactics.ml @@ -40,11 +40,11 @@ let reduction_tac ~reduction ~status:(proof,goal) = *) (* 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 reduction_tac ~also_in_hypotheses ~reduction ~terms ~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 + let terms = + match terms with None -> [ty] | Some l -> l 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. *) @@ -57,8 +57,8 @@ let reduction_tac ~also_in_hypotheses ~reduction ~term ~status:(proof,goal) = (*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' + let terms' = List.map (reduction context) terms in + ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms' ~where:where with _ -> where @@ -101,7 +101,7 @@ let fold_tac ~reduction ~also_in_hypotheses ~term ~status:(proof,goal) = (*CSC: ma si potrebbe ovviare al problema. Ma non credo *) (*CSC: che si guadagni nulla in fatto di efficienza. *) let replace = - ProofEngineReduction.replace ~equality:(=) ~what:term' ~with_what:term + ProofEngineReduction.replace ~equality:(=) ~what:[term'] ~with_what:[term] in let ty' = replace ty in let metasenv' = diff --git a/helm/ocaml/tactics/reductionTactics.mli b/helm/ocaml/tactics/reductionTactics.mli index 8df6c2468..f97b4cf63 100644 --- a/helm/ocaml/tactics/reductionTactics.mli +++ b/helm/ocaml/tactics/reductionTactics.mli @@ -25,11 +25,14 @@ (* 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 + also_in_hypotheses:bool -> terms:(Cic.term list option) -> + ProofEngineTypes.tactic val reduce_tac: - also_in_hypotheses:bool -> term:(Cic.term option) -> ProofEngineTypes.tactic + also_in_hypotheses:bool -> terms:(Cic.term list option) -> + ProofEngineTypes.tactic val whd_tac: - also_in_hypotheses:bool -> term:(Cic.term option) -> ProofEngineTypes.tactic + also_in_hypotheses:bool -> terms:(Cic.term list option) -> + ProofEngineTypes.tactic val fold_tac: reduction:(Cic.context -> Cic.term -> Cic.term) -> -- 2.39.2