diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 91 |
1 files changed, 73 insertions, 18 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 117ed338ee..c2a6483012 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -40,6 +40,54 @@ let _ = Goptions.declare_bool_option { let get_refolding_in_reduction () = !refolding_in_reduction let set_refolding_in_reduction = (:=) refolding_in_reduction +(** Support for reduction effects *) + +open Mod_subst +open Libobject + +type effect_name = string + +(** create a persistent set to store effect functions *) +module ConstrMap = Map.Make (Constr) + +(* Table bindings a constant to an effect *) +let constant_effect_table = Summary.ref ~name:"reduction-side-effect" ConstrMap.empty + +(* Table bindings function key to effective functions *) +let effect_table = Summary.ref ~name:"reduction-function-effect" String.Map.empty + +(** a test to know whether a constant is actually the effect function *) +let reduction_effect_hook env sigma termkey c = + try + let funkey = ConstrMap.find termkey !constant_effect_table in + let effect = String.Map.find funkey !effect_table in + effect env sigma (Lazy.force c) + with Not_found -> () + +let cache_reduction_effect (_,(termkey,funkey)) = + constant_effect_table := ConstrMap.add termkey funkey !constant_effect_table + +let subst_reduction_effect (subst,(termkey,funkey)) = + (subst_mps subst termkey,funkey) + +let inReductionEffect : Constr.constr * string -> obj = + declare_object {(default_object "REDUCTION-EFFECT") with + cache_function = cache_reduction_effect; + open_function = (fun i o -> if Int.equal i 1 then cache_reduction_effect o); + subst_function = subst_reduction_effect; + classify_function = (fun o -> Substitute o) } + +let declare_reduction_effect funkey f = + if String.Map.mem funkey !effect_table then + CErrors.anomaly Pp.(str "Cannot redeclare effect function " ++ qstring funkey ++ str "."); + effect_table := String.Map.add funkey f !effect_table + +(** A function to set the value of the print function *) +let set_reduction_effect x funkey = + let termkey = Universes.constr_of_global x in + Lib.add_anonymous_leaf (inReductionEffect (termkey,funkey)) + + (** Machinery to custom the behavior of the reduction *) module ReductionBehaviour = struct open Globnames @@ -595,7 +643,7 @@ type state = constr * constr Stack.t type contextual_reduction_function = env -> evar_map -> constr -> constr type reduction_function = contextual_reduction_function type local_reduction_function = evar_map -> constr -> constr -type e_reduction_function = { e_redfun : 'r. env -> 'r Sigma.t -> constr -> (constr, 'r) Sigma.sigma } +type e_reduction_function = env -> evar_map -> constr -> evar_map * constr type contextual_stack_reduction_function = env -> evar_map -> constr -> constr * constr list @@ -777,7 +825,7 @@ let contract_fix ?env sigma ?reference ((recindices,bodynum),(names,types,bodies context" in contract_fix *) let reduce_and_refold_fix recfun env sigma refold cst_l fix sk = let raw_answer = - let env = if refold then None else Some env in + let env = if refold then Some env else None in contract_fix ?env sigma ?reference:(Cst_stack.reference sigma cst_l) fix in apply_subst (fun sigma x (t,sk') -> @@ -859,9 +907,12 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = (match safe_meta_value sigma ev with | Some body -> whrec cst_l (EConstr.of_constr body, stack) | None -> fold ()) - | Const (c,u as const) when CClosure.RedFlags.red_set flags (CClosure.RedFlags.fCONST c) -> - let u' = EInstance.kind sigma u in - (match constant_opt_value_in env (fst const, u') with + | Const (c,u as const) -> + reduction_effect_hook env sigma (EConstr.to_constr sigma x) + (lazy (EConstr.to_constr sigma (Stack.zip sigma (x,stack)))); + if CClosure.RedFlags.red_set flags (CClosure.RedFlags.fCONST c) then + let u' = EInstance.kind sigma u in + (match constant_opt_value_in env (c, u') with | None -> fold () | Some body -> let body = EConstr.of_constr body in @@ -901,7 +952,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = | Some (bef,arg,s') -> whrec Cst_stack.empty (arg,Stack.Cst(Stack.Cst_const (fst const, u'),curr,remains,bef,cst_l)::s') - ) + ) else fold () | Proj (p, c) when CClosure.RedFlags.red_projection flags p -> (let pb = lookup_projection p env in let kn = Projection.constant p in @@ -1035,7 +1086,7 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = |_ -> fold () else fold () - | Rel _ | Var _ | Const _ | LetIn _ | Proj _ -> fold () + | Rel _ | Var _ | LetIn _ | Proj _ -> fold () | Sort _ | Ind _ | Prod _ -> fold () in fun xs -> @@ -1219,7 +1270,7 @@ let clos_norm_flags flgs env sigma t = EConstr.of_constr (CClosure.norm_val (CClosure.create_clos_infos ~evars flgs env) (CClosure.inject (EConstr.Unsafe.to_constr t))) - with e when is_anomaly e -> error "Tried to normalize ill-typed term" + with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term") let clos_whd_flags flgs env sigma t = try @@ -1227,7 +1278,7 @@ let clos_whd_flags flgs env sigma t = EConstr.of_constr (CClosure.whd_val (CClosure.create_clos_infos ~evars flgs env) (CClosure.inject (EConstr.Unsafe.to_constr t))) - with e when is_anomaly e -> error "Tried to normalize ill-typed term" + with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term") let nf_beta = clos_norm_flags CClosure.beta (Global.env ()) let nf_betaiota = clos_norm_flags CClosure.betaiota (Global.env ()) @@ -1317,19 +1368,23 @@ let sigma_univ_state = let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = (** FIXME *) + let open Universes in let x = EConstr.Unsafe.to_constr x in let y = EConstr.Unsafe.to_constr y in try - let fold cstr sigma = - try Some (Evd.add_universe_constraints sigma cstr) - with Univ.UniverseInconsistency _ | Evd.UniversesDiffer -> None - in + let fold cstr accu = Some (Constraints.fold Constraints.add cstr accu) in let b, sigma = let ans = if pb == Reduction.CUMUL then - Universes.leq_constr_univs_infer (Evd.universes sigma) fold x y sigma + Universes.leq_constr_univs_infer (Evd.universes sigma) fold x y Constraints.empty else - Universes.eq_constr_univs_infer (Evd.universes sigma) fold x y sigma + Universes.eq_constr_univs_infer (Evd.universes sigma) fold x y Constraints.empty + in + let ans = match ans with + | None -> None + | Some cstr -> + try Some (Evd.add_universe_constraints sigma cstr) + with Univ.UniverseInconsistency _ | Evd.UniversesDiffer -> None in match ans with | None -> false, sigma @@ -1441,7 +1496,7 @@ let instance sigma s c = let hnf_prod_app env sigma t n = match EConstr.kind sigma (whd_all env sigma t) with | Prod (_,_,b) -> subst1 n b - | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product") + | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product.") let hnf_prod_appvect env sigma t nl = Array.fold_left (fun acc t -> hnf_prod_app env sigma acc t) t nl @@ -1452,7 +1507,7 @@ let hnf_prod_applist env sigma t nl = let hnf_lam_app env sigma t n = match EConstr.kind sigma (whd_all env sigma t) with | Lambda (_,_,b) -> subst1 n b - | _ -> anomaly ~label:"hnf_lam_app" (Pp.str "Need an abstraction") + | _ -> anomaly ~label:"hnf_lam_app" (Pp.str "Need an abstraction.") let hnf_lam_appvect env sigma t nl = Array.fold_left (fun acc t -> hnf_lam_app env sigma acc t) t nl @@ -1689,5 +1744,5 @@ let betazetaevar_applist sigma n c l = | Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl | LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack | Evar _, _ -> applist (substl env t, stack) - | _ -> anomaly (Pp.str "Not enough lambda/let's") in + | _ -> anomaly (Pp.str "Not enough lambda/let's.") in stacklam n [] c l |