From 6beda5aa100b617b75d88a5a519b5022c99208a0 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 10 Mar 2008 13:27:00 +0000 Subject: [PATCH] Tactic reduce got rid of. Use normalize, instead. Rationale: the two tactics did the very same thing, but normalizes exploits reduction machines and so it is really faster in many cases. --- .../software/components/grafite/grafiteAst.ml | 1 - .../grafite_engine/grafiteEngine.ml | 2 - .../grafite_parser/grafiteDisambiguate.ml | 1 - .../grafite_parser/grafiteParser.ml | 1 - .../tactics/proofEngineReduction.ml | 210 ------------------ .../tactics/proofEngineReduction.mli | 1 - .../components/tactics/reductionTactics.ml | 4 - .../components/tactics/reductionTactics.mli | 1 - helm/software/components/tactics/tactics.ml | 1 - helm/software/components/tactics/tactics.mli | 1 - helm/software/matita/help/C/sec_tactics.xml | 34 --- helm/software/matita/matitaMathView.ml | 4 +- 12 files changed, 1 insertion(+), 260 deletions(-) diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 2b0f4db5f..6b20ab9c8 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -34,7 +34,6 @@ type ('term, 'lazy_term, 'ident) pattern = type 'lazy_term reduction = [ `Normalize - | `Reduce | `Simpl | `Unfold of 'lazy_term option | `Whd ] diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 409c0921a..aa056f3e2 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -126,7 +126,6 @@ let rec tactic_of_ast status ast = | `Normalize -> PET.const_lazy_reduction (CicReduction.normalize ~delta:false ~subst:[]) - | `Reduce -> PET.const_lazy_reduction ProofEngineReduction.reduce | `Simpl -> PET.const_lazy_reduction ProofEngineReduction.simpl | `Unfold None -> PET.const_lazy_reduction (ProofEngineReduction.unfold ?what:None) @@ -161,7 +160,6 @@ let rec tactic_of_ast status ast = | GrafiteAst.Reduce (_, reduction_kind, pattern) -> (match reduction_kind with | `Normalize -> Tactics.normalize ~pattern - | `Reduce -> Tactics.reduce ~pattern | `Simpl -> Tactics.simpl ~pattern | `Unfold what -> Tactics.unfold ~pattern what | `Whd -> Tactics.whd ~pattern) diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index 308144c21..dfaf5b424 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -103,7 +103,6 @@ let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function let t = disambiguate_lazy_term text prefix_len lexicon_status_ref t in `Unfold (Some t) | `Normalize - | `Reduce | `Simpl | `Unfold None | `Whd as kind -> kind diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index df18135ac..378931c14 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -78,7 +78,6 @@ EXTEND ]; reduction_kind: [ [ IDENT "normalize" -> `Normalize - | IDENT "reduce" -> `Reduce | IDENT "simplify" -> `Simpl | IDENT "unfold"; t = OPT tactic_term -> `Unfold t | IDENT "whd" -> `Whd ] diff --git a/helm/software/components/tactics/proofEngineReduction.ml b/helm/software/components/tactics/proofEngineReduction.ml index 016a7ba99..68a2a0a3d 100644 --- a/helm/software/components/tactics/proofEngineReduction.ml +++ b/helm/software/components/tactics/proofEngineReduction.ml @@ -379,216 +379,6 @@ let replace_with_rel_1_from ~equality ~what = in subst_term - - - -(* Takes a well-typed term and fully reduces it. *) -(*CSC: It does not perform reduction in a Case *) -let reduce context = - let rec reduceaux context l = - function - C.Rel n as t -> - (match List.nth context (n-1) with - Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l) - | Some (_,C.Def (bo,_)) -> reduceaux context l (S.lift n bo) - | None -> raise RelToHiddenHypothesis - ) - | C.Var (uri,exp_named_subst) -> - let exp_named_subst' = - reduceaux_exp_named_subst context l exp_named_subst - in - (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with - C.Constant _ -> raise ReferenceToConstant - | C.CurrentProof _ -> raise ReferenceToCurrentProof - | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition - | C.Variable (_,None,_,_,_) -> - let t' = C.Var (uri,exp_named_subst') in - if l = [] then t' else C.Appl (t'::l) - | C.Variable (_,Some body,_,_,_) -> - (reduceaux context l - (CicSubstitution.subst_vars exp_named_subst' body)) - ) - | C.Meta _ as t -> if l = [] then t else C.Appl (t::l) - | C.Sort _ as t -> t (* l should be empty *) - | C.Implicit _ as t -> t - | C.Cast (te,ty) -> - C.Cast (reduceaux context l te, reduceaux context l ty) - | C.Prod (name,s,t) -> - assert (l = []) ; - C.Prod (name, - reduceaux context [] s, - reduceaux ((Some (name,C.Decl s))::context) [] t) - | C.Lambda (name,s,t) -> - (match l with - [] -> - C.Lambda (name, - reduceaux context [] s, - reduceaux ((Some (name,C.Decl s))::context) [] t) - | he::tl -> reduceaux context tl (S.subst he t) - (* when name is Anonimous the substitution should be superfluous *) - ) - | C.LetIn (n,s,t) -> - reduceaux context l (S.subst (reduceaux context [] s) t) - | C.Appl (he::tl) -> - let tl' = List.map (reduceaux context []) tl in - reduceaux context (tl'@l) he - | C.Appl [] -> raise (Impossible 1) - | C.Const (uri,exp_named_subst) -> - let exp_named_subst' = - reduceaux_exp_named_subst context l exp_named_subst - in - (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with - C.Constant (_,Some body,_,_,_) -> - (reduceaux context l - (CicSubstitution.subst_vars exp_named_subst' body)) - | C.Constant (_,None,_,_,_) -> - let t' = C.Const (uri,exp_named_subst') in - if l = [] then t' else C.Appl (t'::l) - | C.Variable _ -> raise ReferenceToVariable - | C.CurrentProof (_,_,body,_,_,_) -> - (reduceaux context l - (CicSubstitution.subst_vars exp_named_subst' body)) - | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition - ) - | C.MutInd (uri,i,exp_named_subst) -> - let exp_named_subst' = - reduceaux_exp_named_subst context l exp_named_subst - in - let t' = C.MutInd (uri,i,exp_named_subst') in - if l = [] then t' else C.Appl (t'::l) - | C.MutConstruct (uri,i,j,exp_named_subst) -> - let exp_named_subst' = - reduceaux_exp_named_subst context l exp_named_subst - in - let t' = C.MutConstruct (uri,i,j,exp_named_subst') in - if l = [] then t' else C.Appl (t'::l) - | C.MutCase (mutind,i,outtype,term,pl) -> - let decofix = - function - C.CoFix (i,fl) -> - let (_,_,body) = List.nth fl i in - let body' = - let counter = ref (List.length fl) in - List.fold_right - (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl))) - fl - body - in - reduceaux context [] body' - | C.Appl (C.CoFix (i,fl) :: tl) -> - let (_,_,body) = List.nth fl i in - let body' = - let counter = ref (List.length fl) in - List.fold_right - (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl))) - fl - body - in - let tl' = List.map (reduceaux context []) tl in - reduceaux context tl' body' - | t -> t - in - (match decofix (reduceaux context [] term) with - C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1)) - | C.Appl (C.MutConstruct (_,_,j,_) :: tl) -> - let (arity, r) = - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in - match o with - C.InductiveDefinition (tl,_,r,_) -> - let (_,_,arity,_) = List.nth tl i in - (arity,r) - | _ -> raise WrongUriToInductiveDefinition - in - let ts = - let rec eat_first = - function - (0,l) -> l - | (n,he::tl) when n > 0 -> eat_first (n - 1, tl) - | _ -> raise (Impossible 5) - in - eat_first (r,tl) - in - reduceaux context (ts@l) (List.nth pl (j-1)) - | C.Cast _ | C.Implicit _ -> - raise (Impossible 2) (* we don't trust our whd ;-) *) - | _ -> - let outtype' = reduceaux context [] outtype in - let term' = reduceaux context [] term in - let pl' = List.map (reduceaux context []) pl in - let res = - C.MutCase (mutind,i,outtype',term',pl') - in - if l = [] then res else C.Appl (res::l) - ) - | C.Fix (i,fl) -> - let tys,_ = - List.fold_left - (fun (types,len) (n,_,ty,_) -> - (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, - len+1) - ) ([],0) fl - in - let t' () = - let fl' = - List.map - (function (n,recindex,ty,bo) -> - (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo) - ) fl - in - C.Fix (i, fl') - in - let (_,recindex,_,body) = List.nth fl i in - let recparam = - try - Some (List.nth l recindex) - with - _ -> None - in - (match recparam with - Some recparam -> - (match reduceaux context [] recparam with - C.MutConstruct _ - | C.Appl ((C.MutConstruct _)::_) -> - let body' = - let counter = ref (List.length fl) in - List.fold_right - (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl))) - fl - body - in - (* Possible optimization: substituting whd recparam in l*) - reduceaux context l body' - | _ -> if l = [] then t' () else C.Appl ((t' ())::l) - ) - | None -> if l = [] then t' () else C.Appl ((t' ())::l) - ) - | C.CoFix (i,fl) -> - let tys,_ = - List.fold_left - (fun (types,len) (n,ty,_) -> - (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, - len+1) - ) ([],0) fl - in - let t' = - let fl' = - List.map - (function (n,ty,bo) -> - (n,reduceaux context [] ty, reduceaux (tys@context) [] bo) - ) fl - in - C.CoFix (i, fl') - in - if l = [] then t' else C.Appl (t'::l) - and reduceaux_exp_named_subst context l = - List.map (function uri,t -> uri,reduceaux context [] t) - in - reduceaux context [] -;; - - let unfold ?what context where = let contextlen = List.length context in let first_is_the_expandable_head_of_second context' t1 t2 = diff --git a/helm/software/components/tactics/proofEngineReduction.mli b/helm/software/components/tactics/proofEngineReduction.mli index f8cdec89b..5bc5f2458 100644 --- a/helm/software/components/tactics/proofEngineReduction.mli +++ b/helm/software/components/tactics/proofEngineReduction.mli @@ -69,6 +69,5 @@ val replace_lifting_csc : val replace_with_rel_1_from : equality:(Cic.term -> Cic.term -> bool) -> what:Cic.term list -> int -> Cic.term -> Cic.term -val reduce : Cic.context -> Cic.term -> Cic.term val simpl : Cic.context -> Cic.term -> Cic.term val unfold : ?what:Cic.term -> Cic.context -> Cic.term -> Cic.term diff --git a/helm/software/components/tactics/reductionTactics.ml b/helm/software/components/tactics/reductionTactics.ml index 9c39caa6f..f8e613723 100644 --- a/helm/software/components/tactics/reductionTactics.ml +++ b/helm/software/components/tactics/reductionTactics.ml @@ -95,10 +95,6 @@ let simpl_tac ~pattern = mk_tactic (reduction_tac ~reduction:(const_lazy_reduction ProofEngineReduction.simpl) ~pattern) -let reduce_tac ~pattern = - mk_tactic (reduction_tac - ~reduction:(const_lazy_reduction ProofEngineReduction.reduce) ~pattern) - let unfold_tac what ~pattern = let reduction = match what with diff --git a/helm/software/components/tactics/reductionTactics.mli b/helm/software/components/tactics/reductionTactics.mli index f04e7dcac..004a3b3ee 100644 --- a/helm/software/components/tactics/reductionTactics.mli +++ b/helm/software/components/tactics/reductionTactics.mli @@ -24,7 +24,6 @@ *) val simpl_tac: pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic -val reduce_tac: pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic val whd_tac: pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic val normalize_tac: pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic val head_beta_reduce_tac: ?delta:bool -> ?upto:int -> pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic diff --git a/helm/software/components/tactics/tactics.ml b/helm/software/components/tactics/tactics.ml index aa2e2bf4f..b941a8752 100644 --- a/helm/software/components/tactics/tactics.ml +++ b/helm/software/components/tactics/tactics.ml @@ -57,7 +57,6 @@ let lapply = FwdSimplTactic.lapply_tac let left = IntroductionTactics.left_tac let letin = PrimitiveTactics.letin_tac let normalize = ReductionTactics.normalize_tac -let reduce = ReductionTactics.reduce_tac let reflexivity = Setoids.setoid_reflexivity_tac let replace = EqualityTactics.replace_tac let rewrite = EqualityTactics.rewrite_tac diff --git a/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli index 69f415ee1..0a0a2e0d6 100644 --- a/helm/software/components/tactics/tactics.mli +++ b/helm/software/components/tactics/tactics.mli @@ -79,7 +79,6 @@ val letin : Cic.term -> ProofEngineTypes.tactic val normalize : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic -val reduce : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic val reflexivity : ProofEngineTypes.tactic val replace : pattern:ProofEngineTypes.lazy_pattern -> diff --git a/helm/software/matita/help/C/sec_tactics.xml b/helm/software/matita/help/C/sec_tactics.xml index 364401aa5..bdfb3e5db 100644 --- a/helm/software/matita/help/C/sec_tactics.xml +++ b/helm/software/matita/help/C/sec_tactics.xml @@ -1344,40 +1344,6 @@ - - reduce - reduce - reduce patt - - - - Synopsis: - - reduce &pattern; - - - - Pre-conditions: - - None. - - - - Action: - - It replaces all the terms matched by patt - with their βδιζ-normal form. - - - - New sequents to prove: - - None. - - - - - reflexivity reflexivity diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index ff79f54ed..7f1917cfe 100644 --- a/helm/software/matita/matitaMathView.ml +++ b/helm/software/matita/matitaMathView.ml @@ -288,14 +288,13 @@ object (self) reductions_menu_item#set_submenu reductions; tactics_menu_item#set_submenu tactics; let normalize = add_menu_item ~menu:reductions ~label:"Normalize" () in - let reduce = add_menu_item ~menu:reductions ~label:"Reduce" () in let simplify = add_menu_item ~menu:reductions ~label:"Simplify" () in let whd = add_menu_item ~menu:reductions ~label:"Weak head" () in menu#append (GMenu.separator_item ()); let copy = add_menu_item ~stock:`COPY () in let gui = get_gui () in List.iter (fun item -> item#misc#set_sensitive gui#canCopy) - [ copy; check; normalize; reduce; simplify; whd ]; + [ copy; check; normalize; simplify; whd ]; let reduction_action kind () = let pat = self#tactic_text_pattern_of_selection in let statement = @@ -311,7 +310,6 @@ object (self) (MatitaScript.current ())#advance ~statement () in connect_menu_item copy gui#copy; connect_menu_item normalize (reduction_action `Normalize); - connect_menu_item reduce (reduction_action `Reduce); connect_menu_item simplify (reduction_action `Simpl); connect_menu_item whd (reduction_action `Whd); menu#popup ~button:right_button ~time -- 2.39.2