From e57aab0559297cff3875931258674cfe2cfbbba3 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 30 Jun 2016 14:22:02 +0200 Subject: Separate flags for fix/cofix/match reduction and clean reduction function names. This is a reimplementation of Hugo's PR#117. We are trying to address the problem that the name of some reduction functions was not saying what they were doing (e.g. whd_betadeltaiota was doing let-in reduction). Like PR#117, we are careful that no function changed semantics without changing the names. Porting existing ML code should be a matter of renamings a few function calls. Also, we introduce more precise reduction flags fMATCH, fFIX, fCOFIX collectively denominated iota. We renamed the following functions: Closure.betadeltaiota -> Closure.all Closure.betadeltaiotanolet -> Closure.allnolet Reductionops.beta -> Closure.beta Reductionops.zeta -> Closure.zeta Reductionops.betaiota -> Closure.betaiota Reductionops.betaiotazeta -> Closure.betaiotazeta Reductionops.delta -> Closure.delta Reductionops.betalet -> Closure.betazeta Reductionops.betadelta -> Closure.betadeltazeta Reductionops.betadeltaiota -> Closure.all Reductionops.betadeltaiotanolet -> Closure.allnolet Closure.no_red -> Closure.nored Reductionops.nored -> Closure.nored Reductionops.nf_betadeltaiota -> Reductionops.nf_all Reductionops.whd_betadelta -> Reductionops.whd_betadeltazeta Reductionops.whd_betadeltaiota -> Reductionops.whd_all Reductionops.whd_betadeltaiota_nolet -> Reductionops.whd_allnolet Reductionops.whd_betadelta_stack -> Reductionops.whd_betadeltazeta_stack Reductionops.whd_betadeltaiota_stack -> Reductionops.whd_all_stack Reductionops.whd_betadeltaiota_nolet_stack -> Reductionops.whd_allnolet_stack Reductionops.whd_betadelta_state -> Reductionops.whd_betadeltazeta_state Reductionops.whd_betadeltaiota_state -> Reductionops.whd_all_state Reductionops.whd_betadeltaiota_nolet_state -> Reductionops.whd_allnolet_state Reductionops.whd_eta -> Reductionops.shrink_eta Tacmach.pf_whd_betadeltaiota -> Tacmach.pf_whd_all Tacmach.New.pf_whd_betadeltaiota -> Tacmach.New.pf_whd_all And removed the following ones: Reductionops.whd_betaetalet Reductionops.whd_betaetalet_stack Reductionops.whd_betaetalet_state Reductionops.whd_betadeltaeta_stack Reductionops.whd_betadeltaeta_state Reductionops.whd_betadeltaeta Reductionops.whd_betadeltaiotaeta_stack Reductionops.whd_betadeltaiotaeta_state Reductionops.whd_betadeltaiotaeta They were unused and having some reduction functions perform eta is confusing as whd_all and nf_all don't do it. --- library/impargs.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'library') diff --git a/library/impargs.ml b/library/impargs.ml index feb3bf0187..52d5c9c91e 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -188,7 +188,7 @@ let is_reversible_pattern bound depth f l = (* Precondition: rels in env are for inductive types only *) let add_free_rels_until strict strongly_strict revpat bound env m pos acc = let rec frec rig (env,depth as ed) c = - let hd = if strict then whd_betadeltaiota env c else c in + let hd = if strict then whd_all env c else c in let c = if strongly_strict then hd else c in match kind_of_term hd with | Rel n when (n < bound+depth) && (n >= depth) -> @@ -236,7 +236,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t = let rigid = ref true in let open Context.Rel.Declaration in let rec aux env avoid n names t = - let t = whd_betadeltaiota env t in + let t = whd_all env t in match kind_of_term t with | Prod (na,a,b) -> let na',avoid' = find_displayed_name_in all avoid na (names,b) in @@ -250,7 +250,7 @@ let compute_implicits_gen strict strongly_strict revpat contextual all env t = add_free_rels_until strict strongly_strict revpat n env t Conclusion v else v in - match kind_of_term (whd_betadeltaiota env t) with + match kind_of_term (whd_all env t) with | Prod (na,a,b) -> let na',avoid = find_displayed_name_in all [] na ([],b) in let v = aux (push_rel (LocalAssum (na',a)) env) avoid 1 [na'] b in -- cgit v1.2.3