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. --- plugins/cc/cctac.ml | 2 +- plugins/decl_mode/decl_interp.ml | 2 +- plugins/decl_mode/decl_proof_instr.ml | 2 +- plugins/extraction/extraction.ml | 12 ++++++------ plugins/extraction/table.ml | 4 ++-- plugins/firstorder/instances.ml | 2 +- plugins/funind/functional_principles_proofs.ml | 2 +- plugins/rtauto/refl_tauto.ml | 2 +- plugins/setoid_ring/newring.ml | 2 +- 9 files changed, 15 insertions(+), 15 deletions(-) (limited to 'plugins') diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index bd788a425..de64368e2 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -42,7 +42,7 @@ let whd env= (fun t -> Closure.whd_val infos (Closure.inject t)) let whd_delta env= - let infos=Closure.create_clos_infos Closure.betadeltaiota env in + let infos=Closure.create_clos_infos Closure.all env in (fun t -> Closure.whd_val infos (Closure.inject t)) (* decompose member of equality in an applicative format *) diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 34307a358..c0ef34305 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -153,7 +153,7 @@ let interp_constr check_sort env sigma c = fst (understand env sigma (fst c)) let special_whd env = - let infos=Closure.create_clos_infos Closure.betadeltaiota env in + let infos=Closure.create_clos_infos Closure.all env in (fun t -> Closure.whd_val infos (Closure.inject t)) let _eq = lazy (Universes.constr_of_global (Coqlib.glob_eq)) diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 836f1982d..b6c34d270 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -84,7 +84,7 @@ let tcl_erase_info gls = tcl_change_info_gen info_gen gls let special_whd gl= - let infos=Closure.create_clos_infos Closure.betadeltaiota (pf_env gl) in + let infos=Closure.create_clos_infos Closure.all (pf_env gl) in (fun t -> Closure.whd_val infos (Closure.inject t)) let special_nf gl= diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 0153348de..4308b4633 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -74,7 +74,7 @@ type flag = info * scheme Really important function. *) let rec flag_of_type env t : flag = - let t = whd_betadeltaiota env none t in + let t = whd_all env none t in match kind_of_term t with | Prod (x,t,c) -> flag_of_type (push_rel (LocalAssum (x,t)) env) c | Sort s when Sorts.is_prop s -> (Logic,TypeScheme) @@ -102,14 +102,14 @@ let is_info_scheme env t = match flag_of_type env t with (*s [type_sign] gernerates a signature aimed at treating a type application. *) let rec type_sign env c = - match kind_of_term (whd_betadeltaiota env none c) with + match kind_of_term (whd_all env none c) with | Prod (n,t,d) -> (if is_info_scheme env t then Keep else Kill Kprop) :: (type_sign (push_rel_assum (n,t) env) d) | _ -> [] let rec type_scheme_nb_args env c = - match kind_of_term (whd_betadeltaiota env none c) with + match kind_of_term (whd_all env none c) with | Prod (n,t,d) -> let n = type_scheme_nb_args (push_rel_assum (n,t) env) d in if is_info_scheme env t then n+1 else n @@ -135,7 +135,7 @@ let make_typvar n vl = next_ident_away id' vl let rec type_sign_vl env c = - match kind_of_term (whd_betadeltaiota env none c) with + match kind_of_term (whd_all env none c) with | Prod (n,t,d) -> let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in if not (is_info_scheme env t) then Kill Kprop::s, vl @@ -143,7 +143,7 @@ let rec type_sign_vl env c = | _ -> [],[] let rec nb_default_params env c = - match kind_of_term (whd_betadeltaiota env none c) with + match kind_of_term (whd_all env none c) with | Prod (n,t,d) -> let n = nb_default_params (push_rel_assum (n,t) env) d in if is_default env t then n+1 else n @@ -489,7 +489,7 @@ and extract_really_ind env kn mib = *) and extract_type_cons env db dbmap c i = - match kind_of_term (whd_betadeltaiota env none c) with + match kind_of_term (whd_all env none c) with | Prod (n,t,d) -> let env' = push_rel_assum (n,t) env in let db' = (try Int.Map.find i dbmap with Not_found -> 0) :: db in diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 81dfa603d..3a9ecc9ff 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -441,7 +441,7 @@ let error_MPfile_as_mod mp b = let argnames_of_global r = let typ = Global.type_of_global_unsafe r in let rels,_ = - decompose_prod (Reduction.whd_betadeltaiota (Global.env ()) typ) in + decompose_prod (Reduction.whd_all (Global.env ()) typ) in List.rev_map fst rels let msg_of_implicit = function @@ -880,7 +880,7 @@ let extract_constant_inline inline r ids s = | ConstRef kn -> let env = Global.env () in let typ = Global.type_of_global_unsafe (ConstRef kn) in - let typ = Reduction.whd_betadeltaiota env typ in + let typ = Reduction.whd_all env typ in if Reduction.is_arity env typ then begin let nargs = Hook.get use_type_scheme_nb_args env typ in diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml index 5eff2f277..1394f4764 100644 --- a/plugins/firstorder/instances.ml +++ b/plugins/firstorder/instances.ml @@ -107,7 +107,7 @@ let mk_open_instance id idc gl m t= let typ=pf_unsafe_type_of gl idc in (* since we know we will get a product, reduction is not too expensive *) - let (nam,_,_)=destProd (whd_betadeltaiota env evmap typ) in + let (nam,_,_)=destProd (whd_all env evmap typ) in match nam with Name id -> id | Anonymous -> dummy_bvid in diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 52094cf08..146749d32 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -281,7 +281,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type = List.fold_left2 compute_substitution sub args1 args2 end else - if (eq_constr t1 t2) then sub else nochange ~t':(make_refl_eq constructor (Reduction.whd_betadeltaiota env t1) t2) "cannot solve (diff)" + if (eq_constr t1 t2) then sub else nochange ~t':(make_refl_eq constructor (Reduction.whd_all env t1) t2) "cannot solve (diff)" in let sub = compute_substitution Int.Map.empty (snd t1) (snd t2) in let sub = compute_substitution sub (fst t1) (fst t2) in diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 0a0b45915..bb9266db1 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -67,7 +67,7 @@ let l_D_Or = lazy (constant "D_Or") let special_whd gl= - let infos=Closure.create_clos_infos Closure.betadeltaiota (pf_env gl) in + let infos=Closure.create_clos_infos Closure.all (pf_env gl) in (fun t -> Closure.whd_val infos (Closure.inject t)) let special_nf gl= diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index 55241ab2b..a6744916a 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -82,7 +82,7 @@ let lookup_map map = errorlabstrm"lookup_map"(str"map "++qs map++str"not found") let protect_red map env sigma c = - kl (create_clos_infos betadeltaiota env) + kl (create_clos_infos all env) (mk_clos_but (lookup_map map c) (Esubst.subs_id 0) c);; let protect_tac map = -- cgit v1.2.3