diff options
| -rw-r--r-- | contrib/xml/doubleTypeInference.ml | 2 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 91 | ||||
| -rw-r--r-- | pretyping/tacred.mli | 20 | ||||
| -rw-r--r-- | proofs/redexpr.ml | 106 | ||||
| -rw-r--r-- | proofs/redexpr.mli | 31 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 5 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 4 | ||||
| -rw-r--r-- | tactics/hiddentac.mli | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.mli | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 4 | ||||
| -rw-r--r-- | tactics/tactics.mli | 2 | ||||
| -rw-r--r-- | toplevel/command.mli | 3 |
13 files changed, 157 insertions, 117 deletions
diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml index cf975b437..728c7ac9a 100644 --- a/contrib/xml/doubleTypeInference.ml +++ b/contrib/xml/doubleTypeInference.ml @@ -42,7 +42,7 @@ prerr_endline "###whd_betadeltaiotacprop:" ; let xxx = (*Pp.msgerr (Printer.prterm_env env ty);*) prerr_endline ""; - Tacred.reduction_of_redexp red_exp env evar_map ty + Redexpr.reduction_of_red_expr red_exp env evar_map ty in prerr_endline "###FINE" ; (* diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index cae0705c0..ce09bf8aa 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -26,31 +26,6 @@ open Rawterm exception Elimconst exception Redelimination -let set_opaque_const sp = - Conv_oracle.set_opaque_const sp; - Csymtable.set_opaque_const sp - -let set_transparent_const sp = - let cb = Global.lookup_constant sp in - if cb.const_body <> None & cb.const_opaque then - errorlabstrm "set_transparent_const" - (str "Cannot make" ++ spc () ++ - Nametab.pr_global_env Idset.empty (ConstRef sp) ++ - spc () ++ str "transparent because it was declared opaque."); - Conv_oracle.set_transparent_const sp; - Csymtable.set_transparent_const sp - -let set_opaque_var = Conv_oracle.set_opaque_var -let set_transparent_var = Conv_oracle.set_transparent_var - -let _ = - Summary.declare_summary "Transparent constants and variables" - { Summary.freeze_function = Conv_oracle.freeze; - Summary.unfreeze_function = Conv_oracle.unfreeze; - Summary.init_function = Conv_oracle.init; - Summary.survive_module = false; - Summary.survive_section = false } - let is_evaluable env ref = match ref with EvalConstRef kn -> @@ -503,7 +478,7 @@ and construct_const env sigma = (* Red reduction tactic: reduction to a product *) -let internal_red_product env sigma c = +let try_red_product env sigma c = let simpfun = clos_norm_flags betaiotazeta env sigma in let rec redrec env x = match kind_of_term x with @@ -533,11 +508,9 @@ let internal_red_product env sigma c = in redrec env c let red_product env sigma c = - try internal_red_product env sigma c + try try_red_product env sigma c with Redelimination -> error "Not reducible" -(* Hnf reduction tactic: *) - let hnf_constr env sigma c = let rec redrec (x, largs as s) = match kind_of_term x with @@ -610,9 +583,6 @@ let whd_nf env sigma c = let nf env sigma c = strong whd_nf env sigma c -let is_reference c = - try let r = reference_of_constr c in true with _ -> false - let is_head c t = match kind_of_term t with | App (f,_) -> f = c @@ -804,11 +774,6 @@ let cbv_betadeltaiota env sigma = cbv_norm_flags betadeltaiota env sigma let compute = cbv_betadeltaiota -(* call by value reduction functions using virtual machine *) -let cbv_vm env _ c = - let ctyp = (fst (Typeops.infer env c)).uj_type in - Vconv.cbv_vm env c ctyp - (* Pattern *) (* gives [na:ta]c' such that c converts to ([na:ta]c' a), abstracting only @@ -828,58 +793,6 @@ let pattern_occs loccs_trm env sigma c = let _ = Typing.type_of env sigma abstr_trm in applist(abstr_trm, List.map snd loccs_trm) -(* Generic reduction: reduction functions used in reduction tactics *) - -type red_expr = (constr, evaluable_global_reference) red_expr_gen - -open RedFlags - -let make_flag_constant = function - | EvalVarRef id -> fVAR id - | EvalConstRef sp -> fCONST sp - -let make_flag f = - let red = no_red in - let red = if f.rBeta then red_add red fBETA else red in - let red = if f.rIota then red_add red fIOTA else red in - let red = if f.rZeta then red_add red fZETA else red in - let red = - if f.rDelta then (* All but rConst *) - let red = red_add red fDELTA in - let red = red_add_transparent red (Conv_oracle.freeze ()) in - List.fold_right - (fun v red -> red_sub red (make_flag_constant v)) - f.rConst red - else (* Only rConst *) - let red = red_add_transparent (red_add red fDELTA) all_opaque in - List.fold_right - (fun v red -> red_add red (make_flag_constant v)) - f.rConst red - in red - -let red_expr_tab = ref Stringmap.empty - -let declare_red_expr s f = - try - let _ = Stringmap.find s !red_expr_tab in - error ("There is already a reduction expression of name "^s) - with Not_found -> - red_expr_tab := Stringmap.add s f !red_expr_tab - -let reduction_of_redexp = function - | Red internal -> if internal then internal_red_product else red_product - | Hnf -> hnf_constr - | Simpl (Some (_,c as lp)) -> contextually (is_reference c) lp nf - | Simpl None -> nf - | Cbv f -> cbv_norm_flags (make_flag f) - | Lazy f -> clos_norm_flags (make_flag f) - | Unfold ubinds -> unfoldn ubinds - | Fold cl -> fold_commands cl - | Pattern lp -> pattern_occs lp - | ExtraRedExpr s -> - (try Stringmap.find s !red_expr_tab - with Not_found -> error("unknown user-defined reduction \""^s^"\"")) - | CbvVm -> cbv_vm (* Used in several tactics. *) exception NotStepReducible diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 0c093694c..b7d8c1b85 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -24,9 +24,12 @@ val is_evaluable : env -> evaluable_global_reference -> bool exception Redelimination -(* Red (raise Redelimination if nothing reducible) *) +(* Red (raise user error if nothing reducible) *) val red_product : reduction_function +(* Red (raise Redelimination if nothing reducible) *) +val try_red_product : reduction_function + (* Hnf *) val hnf_constr : reduction_function @@ -51,9 +54,6 @@ val cbv_norm_flags : Closure.RedFlags.reds -> reduction_function val cbv_betadeltaiota : reduction_function val compute : reduction_function (* = [cbv_betadeltaiota] *) -(* Call by value strategy (uses virtual machine) *) -val cbv_vm : reduction_function - (* [reduce_to_atomic_ind env sigma t] puts [t] in the form [t'=(I args)] with [I] an inductive definition; returns [I] and [t'] or fails with a user error *) @@ -72,17 +72,5 @@ val reduce_to_quantified_ref : val reduce_to_atomic_ref : env -> evar_map -> Libnames.global_reference -> types -> types -type red_expr = (constr, evaluable_global_reference) red_expr_gen - val contextually : bool -> constr occurrences -> reduction_function -> reduction_function -val reduction_of_redexp : red_expr -> reduction_function - -val declare_red_expr : string -> reduction_function -> unit - -(* Opaque and Transparent commands. *) -val set_opaque_const : constant -> unit -val set_transparent_const : constant -> unit - -val set_opaque_var : identifier -> unit -val set_transparent_var : identifier -> unit diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml new file mode 100644 index 000000000..47d468bd3 --- /dev/null +++ b/proofs/redexpr.ml @@ -0,0 +1,106 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +open Pp +open Util +open Names +open Term +open Declarations +open Libnames +open Rawterm +open Reductionops +open Tacred +open Closure +open RedFlags + +let set_opaque_const sp = + Conv_oracle.set_opaque_const sp; + Csymtable.set_opaque_const sp + +let set_transparent_const sp = + let cb = Global.lookup_constant sp in + if cb.const_body <> None & cb.const_opaque then + errorlabstrm "set_transparent_const" + (str "Cannot make" ++ spc () ++ + Nametab.pr_global_env Idset.empty (ConstRef sp) ++ + spc () ++ str "transparent because it was declared opaque."); + Conv_oracle.set_transparent_const sp; + Csymtable.set_transparent_const sp + +let set_opaque_var = Conv_oracle.set_opaque_var +let set_transparent_var = Conv_oracle.set_transparent_var + +let _ = + Summary.declare_summary "Transparent constants and variables" + { Summary.freeze_function = Conv_oracle.freeze; + Summary.unfreeze_function = Conv_oracle.unfreeze; + Summary.init_function = Conv_oracle.init; + Summary.survive_module = false; + Summary.survive_section = false } + +(* call by value reduction functions using virtual machine *) +let cbv_vm env _ c = + let ctyp = (fst (Typeops.infer env c)).Environ.uj_type in + Vconv.cbv_vm env c ctyp + +(* Generic reduction: reduction functions used in reduction tactics *) + +type red_expr = (constr, evaluable_global_reference) red_expr_gen + + +let make_flag_constant = function + | EvalVarRef id -> fVAR id + | EvalConstRef sp -> fCONST sp + +let make_flag f = + let red = no_red in + let red = if f.rBeta then red_add red fBETA else red in + let red = if f.rIota then red_add red fIOTA else red in + let red = if f.rZeta then red_add red fZETA else red in + let red = + if f.rDelta then (* All but rConst *) + let red = red_add red fDELTA in + let red = red_add_transparent red (Conv_oracle.freeze ()) in + List.fold_right + (fun v red -> red_sub red (make_flag_constant v)) + f.rConst red + else (* Only rConst *) + let red = red_add_transparent (red_add red fDELTA) all_opaque in + List.fold_right + (fun v red -> red_add red (make_flag_constant v)) + f.rConst red + in red + +let is_reference c = + try let r = reference_of_constr c in true with _ -> false + +let red_expr_tab = ref Stringmap.empty + +let declare_red_expr s f = + try + let _ = Stringmap.find s !red_expr_tab in + error ("There is already a reduction expression of name "^s) + with Not_found -> + red_expr_tab := Stringmap.add s f !red_expr_tab + +let reduction_of_red_expr = function + | Red internal -> if internal then try_red_product else red_product + | Hnf -> hnf_constr + | Simpl (Some (_,c as lp)) -> contextually (is_reference c) lp nf + | Simpl None -> nf + | Cbv f -> cbv_norm_flags (make_flag f) + | Lazy f -> clos_norm_flags (make_flag f) + | Unfold ubinds -> unfoldn ubinds + | Fold cl -> fold_commands cl + | Pattern lp -> pattern_occs lp + | ExtraRedExpr s -> + (try Stringmap.find s !red_expr_tab + with Not_found -> error("unknown user-defined reduction \""^s^"\"")) + | CbvVm -> cbv_vm diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli new file mode 100644 index 000000000..a0b7100b6 --- /dev/null +++ b/proofs/redexpr.mli @@ -0,0 +1,31 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +open Names +open Term +open Closure +open Rawterm +open Reductionops + +(* Call by value strategy (uses virtual machine) *) +val cbv_vm : reduction_function + +type red_expr = (constr, evaluable_global_reference) red_expr_gen + +val reduction_of_red_expr : red_expr -> reduction_function + +val declare_red_expr : string -> reduction_function -> unit + +(* Opaque and Transparent commands. *) +val set_opaque_const : constant -> unit +val set_transparent_const : constant -> unit + +val set_opaque_var : identifier -> unit +val set_transparent_var : identifier -> unit diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 0ddcd6116..37dc016c9 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -18,6 +18,7 @@ open Environ open Reductionops open Evd open Typing +open Redexpr open Tacred open Proof_trees open Proof_type @@ -90,8 +91,8 @@ let pf_global gls id = Constrintern.construct_reference (pf_hyps gls) id let pf_parse_const gls = compose (pf_global gls) id_of_string -let pf_reduction_of_redexp gls re c = - reduction_of_redexp re (pf_env gls) (project gls) c +let pf_reduction_of_red_expr gls re c = + reduction_of_red_expr re (pf_env gls) (project gls) c let pf_apply f gls = f (pf_env gls) (project gls) let pf_reduce = pf_apply diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 4fbc102cc..22b9de0b7 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -18,7 +18,7 @@ open Reduction open Proof_trees open Proof_type open Refiner -open Tacred +open Redexpr open Tacexpr open Rawterm (*i*) @@ -62,7 +62,7 @@ val pf_get_hyp_typ : goal sigma -> identifier -> types val pf_get_new_id : identifier -> goal sigma -> identifier val pf_get_new_ids : identifier list -> goal sigma -> identifier list -val pf_reduction_of_redexp : goal sigma -> red_expr -> constr -> constr +val pf_reduction_of_red_expr : goal sigma -> red_expr -> constr -> constr val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index ddfb9bd12..f5b35e57d 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -94,7 +94,7 @@ val h_simplest_right : tactic (* Conversion *) -val h_reduce : Tacred.red_expr -> Tacticals.clause -> tactic +val h_reduce : Redexpr.red_expr -> Tacticals.clause -> tactic val h_change : constr occurrences option -> constr -> Tacticals.clause -> tactic diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index a4360e5ea..8eb798212 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1242,7 +1242,7 @@ let pf_redexp_interp ist gl = redexp_interp ist (project gl) (pf_env gl) let interp_may_eval f ist gl = function | ConstrEval (r,c) -> let redexp = pf_redexp_interp ist gl r in - pf_reduction_of_redexp gl redexp (f ist gl c) + pf_reduction_of_red_expr gl redexp (f ist gl c) | ConstrContext ((loc,s),c) -> (try let ic = f ist gl c diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 8d8d12fb4..2173b058c 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -105,7 +105,7 @@ val val_interp : interp_sign -> goal sigma -> glob_tactic_expr -> value (* Interprets redexp arguments *) val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr - -> Tacred.red_expr + -> Redexpr.red_expr (* Interprets tactic expressions *) val interp_tac_gen : (identifier * value) list -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 872baa179..bc91ddb3e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -226,7 +226,7 @@ let pattern_option l = reduct_option (pattern_occs l) as the command Eval does. *) let reduce redexp cl goal = - redin_combinator (reduction_of_redexp redexp) cl goal + redin_combinator (Redexpr.reduction_of_red_expr redexp) cl goal (* Unfolding occurrences of a constant *) @@ -338,7 +338,7 @@ let pf_lookup_hypothesis_as_renamed_gen red h gl = let rec aux ccl = match pf_lookup_hypothesis_as_renamed env ccl h with | None when red -> - aux (reduction_of_redexp (Red true) env (project gl) ccl) + aux (Redexpr.reduction_of_red_expr (Red true) env (project gl) ccl) | x -> x in try aux (pf_concl gl) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index a6b906b34..418c3095f 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -19,7 +19,7 @@ open Reduction open Evd open Evar_refiner open Clenv -open Tacred +open Redexpr open Tacticals open Libnames open Genarg diff --git a/toplevel/command.mli b/toplevel/command.mli index cd97ec5f8..d6eb9cfc5 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -22,6 +22,7 @@ open Vernacexpr open Rawterm open Topconstr open Decl_kinds +open Redexpr (*i*) (*s Declaration functions. The following functions take ASTs, @@ -30,7 +31,7 @@ open Decl_kinds defined object *) val declare_definition : identifier -> definition_kind -> - local_binder list -> Tacred.red_expr option -> constr_expr -> + local_binder list -> red_expr option -> constr_expr -> constr_expr option -> declaration_hook -> unit val syntax_definition : identifier -> constr_expr -> bool -> bool -> unit |