diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 232 |
1 files changed, 105 insertions, 127 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index a1603d69..33928f67 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: reductionops.ml 11796 2009-01-18 13:41:39Z herbelin $ *) +(* $Id: reductionops.ml 11897 2009-02-09 19:28:02Z barras $ *) open Pp open Util @@ -114,31 +114,41 @@ type state = constr * constr stack type contextual_reduction_function = env -> evar_map -> constr -> constr type reduction_function = contextual_reduction_function -type local_reduction_function = constr -> constr +type local_reduction_function = evar_map -> constr -> constr type contextual_stack_reduction_function = env -> evar_map -> constr -> constr * constr list type stack_reduction_function = contextual_stack_reduction_function -type local_stack_reduction_function = constr -> constr * constr list +type local_stack_reduction_function = + evar_map -> constr -> constr * constr list type contextual_state_reduction_function = env -> evar_map -> state -> state type state_reduction_function = contextual_state_reduction_function -type local_state_reduction_function = state -> state +type local_state_reduction_function = evar_map -> state -> state (*************************************) (*** Reduction Functions Operators ***) (*************************************) -let rec whd_state (x, stack as s) = +let safe_evar_value sigma ev = + try Some (Evd.existential_value sigma ev) + with NotInstantiatedEvar | Not_found -> None + +let rec whd_state sigma (x, stack as s) = match kind_of_term x with - | App (f,cl) -> whd_state (f, append_stack cl stack) - | Cast (c,_,_) -> whd_state (c, stack) + | App (f,cl) -> whd_state sigma (f, append_stack cl stack) + | Cast (c,_,_) -> whd_state sigma (c, stack) + | Evar ev -> + (match safe_evar_value sigma ev with + Some c -> whd_state sigma (c,stack) + | _ -> s) | _ -> s let appterm_of_stack (f,s) = (f,list_of_stack s) -let whd_stack x = appterm_of_stack (whd_state (x, empty_stack)) +let whd_stack sigma x = + appterm_of_stack (whd_state sigma (x, empty_stack)) let whd_castapp_stack = whd_stack let stack_reduction_of_reduction red_fun env sigma s = @@ -150,14 +160,14 @@ let strong whdfun env sigma t = map_constr_with_full_binders push_rel strongrec env (whdfun env sigma t) in strongrec env t -let local_strong whdfun = - let rec strongrec t = map_constr strongrec (whdfun t) in +let local_strong whdfun sigma = + let rec strongrec t = map_constr strongrec (whdfun sigma t) in strongrec -let rec strong_prodspine redfun c = - let x = redfun c in +let rec strong_prodspine redfun sigma c = + let x = redfun sigma c in match kind_of_term x with - | Prod (na,a,b) -> mkProd (na,a,strong_prodspine redfun b) + | Prod (na,a,b) -> mkProd (na,a,strong_prodspine redfun sigma b) | _ -> x (*************************************) @@ -171,7 +181,6 @@ module type RedFlagsSig = sig type flags type flag val fbeta : flag - val fevar : flag val fdelta : flag val feta : flag val fiota : flag @@ -179,7 +188,6 @@ module type RedFlagsSig = sig val mkflags : flag list -> flags val red_beta : flags -> bool val red_delta : flags -> bool - val red_evar : flags -> bool val red_eta : flags -> bool val red_iota : flags -> bool val red_zeta : flags -> bool @@ -211,14 +219,12 @@ module RedFlags = (struct type flags = int let fbeta = 1 let fdelta = 2 - let fevar = 4 let feta = 8 let fiota = 16 let fzeta = 32 let mkflags = List.fold_left (lor) 0 let red_beta f = f land fbeta <> 0 let red_delta f = f land fdelta <> 0 - let red_evar f = f land fevar <> 0 let red_eta f = f land feta <> 0 let red_iota f = f land fiota <> 0 let red_zeta f = f land fzeta <> 0 @@ -229,20 +235,16 @@ open RedFlags (* Local *) let beta = mkflags [fbeta] let eta = mkflags [feta] -let evar = mkflags [fevar] -let betaevar = mkflags [fevar; fbeta] let betaiota = mkflags [fiota; fbeta] let betaiotazeta = mkflags [fiota; fbeta;fzeta] -let betaiotazetaevar = mkflags [fiota; fbeta;fzeta;fevar] (* Contextual *) -let delta = mkflags [fdelta;fevar] -let betadelta = mkflags [fbeta;fdelta;fzeta;fevar] -let betadeltaeta = mkflags [fbeta;fdelta;fzeta;fevar;feta] -let betadeltaiota = mkflags [fbeta;fdelta;fzeta;fevar;fiota] -let betadeltaiota_nolet = mkflags [fbeta;fdelta;fevar;fiota] -let betadeltaiotaeta = mkflags [fbeta;fdelta;fzeta;fevar;fiota;feta] -let betaiotaevar = mkflags [fbeta;fiota;fevar] +let delta = mkflags [fdelta] +let betadelta = mkflags [fbeta;fdelta;fzeta] +let betadeltaeta = mkflags [fbeta;fdelta;fzeta;feta] +let betadeltaiota = mkflags [fbeta;fdelta;fzeta;fiota] +let betadeltaiota_nolet = mkflags [fbeta;fdelta;fiota] +let betadeltaiotaeta = mkflags [fbeta;fdelta;fzeta;fiota;feta] let betaetalet = mkflags [fbeta;feta;fzeta] let betalet = mkflags [fbeta;fzeta] @@ -303,11 +305,11 @@ let fix_recarg ((recindices,bodynum),_) stack = type fix_reduction_result = NotReducible | Reduced of state -let reduce_fix whdfun fix stack = +let reduce_fix whdfun sigma fix stack = match fix_recarg fix stack with | None -> NotReducible | Some (recargnum,recarg) -> - let (recarg'hd,_ as recarg') = whdfun (recarg, empty_stack) in + let (recarg'hd,_ as recarg') = whdfun sigma (recarg, empty_stack) in let stack' = stack_assign stack recargnum (app_stack recarg') in (match kind_of_term recarg'hd with | Construct _ -> Reduced (contract_fix fix, stack') @@ -333,8 +335,8 @@ let rec whd_state_gen flags env sigma = (match lookup_named id env with | (_,Some body,_) -> whrec (body, stack) | _ -> s) - | Evar ev when red_evar flags -> - (match existential_opt_value sigma ev with + | Evar ev -> + (match safe_evar_value sigma ev with | Some body -> whrec (body, stack) | None -> s) | Const const when red_delta flags -> @@ -375,7 +377,7 @@ let rec whd_state_gen flags env sigma = (mkCase (ci, p, app_stack (c,cargs), lf), stack) | Fix fix when red_iota flags -> - (match reduce_fix whrec fix stack with + (match reduce_fix (fun _ -> whrec) sigma fix stack with | Reduced s' -> whrec s' | NotReducible -> s) @@ -383,7 +385,7 @@ let rec whd_state_gen flags env sigma = in whrec -let local_whd_state_gen flags = +let local_whd_state_gen flags sigma = let rec whrec (x, stack as s) = match kind_of_term x with | LetIn (_,b,_,c) when red_zeta flags -> stacklam whrec [b] c stack @@ -418,105 +420,91 @@ let local_whd_state_gen flags = (mkCase (ci, p, app_stack (c,cargs), lf), stack) | Fix fix when red_iota flags -> - (match reduce_fix whrec fix stack with + (match reduce_fix (fun _ ->whrec) sigma fix stack with | Reduced s' -> whrec s' | NotReducible -> s) + | Evar ev -> + (match safe_evar_value sigma ev with + Some c -> whrec (c,stack) + | None -> s) + | x -> s in whrec +let stack_red_of_state_red f sigma x = + appterm_of_stack (f sigma (x, empty_stack)) + +let red_of_state_red f sigma x = + app_stack (f sigma (x,empty_stack)) + (* 1. Beta Reduction Functions *) let whd_beta_state = local_whd_state_gen beta -let whd_beta_stack x = appterm_of_stack (whd_beta_state (x, empty_stack)) -let whd_beta x = app_stack (whd_beta_state (x,empty_stack)) +let whd_beta_stack = stack_red_of_state_red whd_beta_state +let whd_beta = red_of_state_red whd_beta_state (* Nouveau ! *) let whd_betaetalet_state = local_whd_state_gen betaetalet -let whd_betaetalet_stack x = - appterm_of_stack (whd_betaetalet_state (x, empty_stack)) -let whd_betaetalet x = app_stack (whd_betaetalet_state (x,empty_stack)) +let whd_betaetalet_stack = stack_red_of_state_red whd_betaetalet_state +let whd_betaetalet = red_of_state_red whd_betaetalet_state let whd_betalet_state = local_whd_state_gen betalet -let whd_betalet_stack x = appterm_of_stack (whd_betalet_state (x, empty_stack)) -let whd_betalet x = app_stack (whd_betalet_state (x,empty_stack)) +let whd_betalet_stack = stack_red_of_state_red whd_betalet_state +let whd_betalet = red_of_state_red whd_betalet_state (* 2. Delta Reduction Functions *) let whd_delta_state e = whd_state_gen delta e -let whd_delta_stack env sigma x = - appterm_of_stack (whd_delta_state env sigma (x, empty_stack)) -let whd_delta env sigma c = - app_stack (whd_delta_state env sigma (c, empty_stack)) +let whd_delta_stack env = stack_red_of_state_red (whd_delta_state env) +let whd_delta env = red_of_state_red (whd_delta_state env) let whd_betadelta_state e = whd_state_gen betadelta e -let whd_betadelta_stack env sigma x = - appterm_of_stack (whd_betadelta_state env sigma (x, empty_stack)) -let whd_betadelta env sigma c = - app_stack (whd_betadelta_state env sigma (c, empty_stack)) - -let whd_betaevar_state e = whd_state_gen betaevar e -let whd_betaevar_stack env sigma c = - appterm_of_stack (whd_betaevar_state env sigma (c, empty_stack)) -let whd_betaevar env sigma c = - app_stack (whd_betaevar_state env sigma (c, empty_stack)) +let whd_betadelta_stack env = + stack_red_of_state_red (whd_betadelta_state env) +let whd_betadelta env = + red_of_state_red (whd_betadelta_state env) let whd_betadeltaeta_state e = whd_state_gen betadeltaeta e -let whd_betadeltaeta_stack env sigma x = - appterm_of_stack (whd_betadeltaeta_state env sigma (x, empty_stack)) -let whd_betadeltaeta env sigma x = - app_stack (whd_betadeltaeta_state env sigma (x, empty_stack)) +let whd_betadeltaeta_stack env = + stack_red_of_state_red (whd_betadeltaeta_state env) +let whd_betadeltaeta env = + red_of_state_red (whd_betadeltaeta_state env) (* 3. Iota reduction Functions *) let whd_betaiota_state = local_whd_state_gen betaiota -let whd_betaiota_stack x = - appterm_of_stack (whd_betaiota_state (x, empty_stack)) -let whd_betaiota x = - app_stack (whd_betaiota_state (x, empty_stack)) +let whd_betaiota_stack = stack_red_of_state_red whd_betaiota_state +let whd_betaiota = red_of_state_red whd_betaiota_state let whd_betaiotazeta_state = local_whd_state_gen betaiotazeta -let whd_betaiotazeta_stack x = - appterm_of_stack (whd_betaiotazeta_state (x, empty_stack)) -let whd_betaiotazeta x = - app_stack (whd_betaiotazeta_state (x, empty_stack)) - -let whd_betaiotazetaevar_state = whd_state_gen betaiotazetaevar -let whd_betaiotazetaevar_stack env sigma x = - appterm_of_stack (whd_betaiotazetaevar_state env sigma (x, empty_stack)) -let whd_betaiotazetaevar env sigma x = - app_stack (whd_betaiotazetaevar_state env sigma (x, empty_stack)) - -let whd_betaiotaevar_state e = whd_state_gen betaiotaevar e -let whd_betaiotaevar_stack env sigma x = - appterm_of_stack (whd_betaiotaevar_state env sigma (x, empty_stack)) -let whd_betaiotaevar env sigma x = - app_stack (whd_betaiotaevar_state env sigma (x, empty_stack)) +let whd_betaiotazeta_stack = stack_red_of_state_red whd_betaiotazeta_state +let whd_betaiotazeta = red_of_state_red whd_betaiotazeta_state let whd_betadeltaiota_state e = whd_state_gen betadeltaiota e -let whd_betadeltaiota_stack env sigma x = - appterm_of_stack (whd_betadeltaiota_state env sigma (x, empty_stack)) -let whd_betadeltaiota env sigma x = - app_stack (whd_betadeltaiota_state env sigma (x, empty_stack)) +let whd_betadeltaiota_stack env = + stack_red_of_state_red (whd_betadeltaiota_state env) +let whd_betadeltaiota env = + red_of_state_red (whd_betadeltaiota_state env) let whd_betadeltaiotaeta_state e = whd_state_gen betadeltaiotaeta e -let whd_betadeltaiotaeta_stack env sigma x = - appterm_of_stack (whd_betadeltaiotaeta_state env sigma (x, empty_stack)) -let whd_betadeltaiotaeta env sigma x = - app_stack (whd_betadeltaiotaeta_state env sigma (x, empty_stack)) +let whd_betadeltaiotaeta_stack env = + stack_red_of_state_red (whd_betadeltaiotaeta_state env) +let whd_betadeltaiotaeta env = + red_of_state_red (whd_betadeltaiotaeta_state env) let whd_betadeltaiota_nolet_state e = whd_state_gen betadeltaiota_nolet e -let whd_betadeltaiota_nolet_stack env sigma x = - appterm_of_stack (whd_betadeltaiota_nolet_state env sigma (x, empty_stack)) -let whd_betadeltaiota_nolet env sigma x = - app_stack (whd_betadeltaiota_nolet_state env sigma (x, empty_stack)) +let whd_betadeltaiota_nolet_stack env = + stack_red_of_state_red (whd_betadeltaiota_nolet_state env) +let whd_betadeltaiota_nolet env = + red_of_state_red (whd_betadeltaiota_nolet_state env) (* 3. Eta reduction Functions *) -let whd_eta c = app_stack (local_whd_state_gen eta (c,empty_stack)) +let whd_eta c = app_stack (local_whd_state_gen eta Evd.empty (c,empty_stack)) (****************************************************************************) (* Reduction Functions *) @@ -526,24 +514,25 @@ let whd_eta c = app_stack (local_whd_state_gen eta (c,empty_stack)) let rec whd_evar sigma c = match kind_of_term c with | Evar ev -> - let d = - try Some (Evd.existential_value sigma ev) - with NotInstantiatedEvar | Not_found -> None in - (match d with Some c -> whd_evar sigma c | None -> c) + (match safe_evar_value sigma ev with + Some c -> whd_evar sigma c + | None -> c) | Sort s when is_sort_variable sigma s -> whd_sort_variable sigma c | _ -> collapse_appl c -let nf_evar sigma = - local_strong (whd_evar sigma) +let nf_evar = + local_strong whd_evar (* lazy reduction functions. The infos must be created for each term *) (* Note by HH [oct 08] : why would it be the job of clos_norm_flags to add a [nf_evar] here *) let clos_norm_flags flgs env sigma t = - norm_val (create_clos_infos flgs env) (inject (nf_evar sigma t)) + norm_val + (create_clos_infos ~evars:(safe_evar_value sigma) flgs env) + (inject t) -let nf_beta = clos_norm_flags Closure.beta empty_env Evd.empty -let nf_betaiota = clos_norm_flags Closure.betaiota empty_env Evd.empty +let nf_beta = clos_norm_flags Closure.beta empty_env +let nf_betaiota = clos_norm_flags Closure.betaiota empty_env let nf_betadeltaiota env sigma = clos_norm_flags Closure.betadeltaiota env sigma @@ -553,7 +542,7 @@ let nf_betadeltaiota env sigma = du type checking : (fun x => x + x) M *) -let rec whd_betaiotaevar_preserving_vm_cast env sigma t = +let rec whd_betaiota_preserving_vm_cast env sigma t = let rec stacklam_var subst t stack = match (decomp_stack stack,kind_of_term t) with | Some (h,stacktl), Lambda (_,_,c) -> @@ -568,7 +557,7 @@ let rec whd_betaiotaevar_preserving_vm_cast env sigma t = and whrec (x, stack as s) = match kind_of_term x with | Evar ev -> - (match existential_opt_value sigma ev with + (match safe_evar_value sigma ev with | Some body -> whrec (body, stack) | None -> s) | Cast (c,VMcast,t) -> @@ -594,12 +583,14 @@ let rec whd_betaiotaevar_preserving_vm_cast env sigma t = in app_stack (whrec (t,empty_stack)) -let nf_betaiotaevar_preserving_vm_cast = - strong whd_betaiotaevar_preserving_vm_cast +let nf_betaiota_preserving_vm_cast = + strong whd_betaiota_preserving_vm_cast (* lazy weak head reduction functions *) let whd_flags flgs env sigma t = - whd_val (create_clos_infos flgs env) (inject (nf_evar sigma t)) + whd_val + (create_clos_infos ~evars:(safe_evar_value sigma) flgs env) + (inject t) (********************************************************************) (* Conversion *) @@ -627,23 +618,9 @@ let pb_equal = function let sort_cmp = sort_cmp - -let nf_red_env sigma env = - let nf_decl = function - (x,Some t,ty) -> (x,Some (nf_evar sigma t),ty) - | d -> d in - let sign = named_context env in - let ctxt = rel_context env in - let env = reset_context env in - let env = Sign.fold_named_context - (fun d env -> push_named (nf_decl d) env) ~init:env sign in - Sign.fold_rel_context - (fun d env -> push_rel (nf_decl d) env) ~init:env ctxt - - -let test_conversion f env sigma x y = +let test_conversion (f:?evars:'a->'b) env sigma x y = try let _ = - f (nf_red_env sigma env) (nf_evar sigma x) (nf_evar sigma y) in true + f ~evars:(safe_evar_value sigma) env x y in true with NotConvertible -> false let is_conv env sigma = test_conversion Reduction.conv env sigma @@ -729,7 +706,8 @@ let plain_instance s c = *) let instance s c = - (* if s = [] then c else *) local_strong whd_betaiota (plain_instance s c) + (* if s = [] then c else *) + local_strong whd_betaiota Evd.empty (plain_instance s c) (* pseudo-reduction rule: * [hnf_prod_app env s (Prod(_,B)) N --> B[N] @@ -830,7 +808,7 @@ let is_sort env sigma arity = let whd_betaiota_deltazeta_for_iota_state env sigma s = let rec whrec s = - let (t, stack as s) = whd_betaiota_state s in + let (t, stack as s) = whd_betaiota_state sigma s in match kind_of_term t with | Case (ci,p,d,lf) -> let (cr,crargs) = whd_betadeltaiota_stack env sigma d in @@ -840,7 +818,7 @@ let whd_betaiota_deltazeta_for_iota_state env sigma s = else s | Fix fix -> - (match reduce_fix (whd_betadeltaiota_state env sigma) fix stack with + (match reduce_fix (whd_betadeltaiota_state env) sigma fix stack with | Reduced s -> whrec s | NotReducible -> s) | _ -> s @@ -882,7 +860,7 @@ let whd_programs_stack env sigma = else (mkCase (ci, p, app_stack(c,cargs), lf), stack) | Fix fix -> - (match reduce_fix whrec fix stack with + (match reduce_fix (fun _ ->whrec) sigma fix stack with | Reduced s' -> whrec s' | NotReducible -> s) | _ -> s @@ -952,7 +930,7 @@ let meta_reducible_instance evd b = | Some (g,(_,s)) -> (mv,(g.rebus,s))::l | None -> l) [] fm in let rec irec u = - let u = whd_betaiota u in + let u = whd_betaiota Evd.empty u in match kind_of_term u with | Case (ci,p,c,bl) when isMeta c or isCast c & isMeta (pi1 (destCast c)) -> let m = try destMeta c with _ -> destMeta (pi1 (destCast c)) in |