diff options
author | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-21 23:25:22 +0000 |
---|---|---|
committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-21 23:25:22 +0000 |
commit | 82b959a8f6025f84a39efb67985e6fe1a338b94b (patch) | |
tree | ebc83d26eb22d50d805462e770788ea11fc221d9 | |
parent | d01f496105de698a3ec98657e4529501c654aaeb (diff) |
refined the conversion oracle
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10960 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | contrib/interface/ascent.mli | 9 | ||||
-rw-r--r-- | contrib/interface/vtp.ml | 14 | ||||
-rw-r--r-- | contrib/interface/xlate.ml | 19 | ||||
-rw-r--r-- | contrib/setoid_ring/Field_theory.v | 2 | ||||
-rw-r--r-- | contrib/setoid_ring/Ring_polynom.v | 2 | ||||
-rw-r--r-- | doc/refman/RefMan-oth.tex | 30 | ||||
-rw-r--r-- | parsing/g_vernac.ml4 | 17 | ||||
-rw-r--r-- | parsing/ppvernac.ml | 17 | ||||
-rw-r--r-- | parsing/prettyp.ml | 6 | ||||
-rw-r--r-- | pretyping/reductionops.ml | 3 | ||||
-rw-r--r-- | pretyping/reductionops.mli | 3 | ||||
-rw-r--r-- | pretyping/tacred.ml | 6 | ||||
-rw-r--r-- | pretyping/unification.ml | 9 | ||||
-rw-r--r-- | proofs/redexpr.ml | 33 | ||||
-rw-r--r-- | proofs/redexpr.mli | 7 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 21 | ||||
-rw-r--r-- | toplevel/vernacexpr.ml | 2 |
17 files changed, 133 insertions, 67 deletions
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli index ef1d095e2..323385233 100644 --- a/contrib/interface/ascent.mli +++ b/contrib/interface/ascent.mli @@ -113,7 +113,6 @@ and ct_COMMAND = | CT_module_type_decl of ct_ID * ct_MODULE_BINDER_LIST * ct_MODULE_TYPE_OPT | CT_no_inline of ct_ID_NE_LIST | CT_omega_flag of ct_OMEGA_MODE * ct_OMEGA_FEATURE - | CT_opaque of ct_ID_NE_LIST | CT_open_scope of ct_ID | CT_print | CT_print_about of ct_ID @@ -189,13 +188,13 @@ and ct_COMMAND = | CT_show_script | CT_show_tree | CT_solve of ct_INT * ct_TACTIC_COM * ct_DOTDOT_OPT + | CT_strategy of ct_LEVEL_LIST | CT_suspend | CT_syntax_macro of ct_ID * ct_FORMULA * ct_INT_OPT | CT_tactic_definition of ct_TAC_DEF_NE_LIST | CT_test_natural_feature of ct_NATURAL_FEATURE * ct_ID | CT_theorem_struct of ct_THEOREM_GOAL * ct_PROOF_SCRIPT | CT_time of ct_COMMAND - | CT_transparent of ct_ID_NE_LIST | CT_undo of ct_INT_OPT | CT_unfocus | CT_unset_option of ct_TABLE @@ -204,6 +203,12 @@ and ct_COMMAND = | CT_user_vernac of ct_ID * ct_VARG_LIST | CT_variable of ct_VAR * ct_BINDER_NE_LIST | CT_write_module of ct_ID * ct_STRING_OPT +and ct_LEVEL_LIST = + CT_level_list of (ct_LEVEL * ct_ID_LIST) list +and ct_LEVEL = + CT_Opaque + | CT_Level of ct_INT + | CT_Expand and ct_COMMAND_LIST = CT_command_list of ct_COMMAND * ct_COMMAND list and ct_COMMENT = diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml index 76b71be42..551ad3a33 100644 --- a/contrib/interface/vtp.ml +++ b/contrib/interface/vtp.ml @@ -393,9 +393,6 @@ and fCOMMAND = function fOMEGA_MODE x1 ++ fOMEGA_FEATURE x2 ++ fNODE "omega_flag" 2 -| CT_opaque(x1) -> - fID_NE_LIST x1 ++ - fNODE "opaque" 1 | CT_open_scope(x1) -> fID x1 ++ fNODE "open_scope" 1 @@ -596,6 +593,10 @@ and fCOMMAND = function fTACTIC_COM x2 ++ fDOTDOT_OPT x3 ++ fNODE "solve" 3 +| CT_strategy(CT_level_list x1) -> + List.fold_left (++) (mt()) + (List.map (fun(l,q) -> fLEVEL l ++ fID_LIST q ++ fNODE "pair"2) x1) ++ + fNODE "strategy" (List.length x1) | CT_suspend -> fNODE "suspend" 0 | CT_syntax_macro(x1, x2, x3) -> fID x1 ++ @@ -616,9 +617,6 @@ and fCOMMAND = function | CT_time(x1) -> fCOMMAND x1 ++ fNODE "time" 1 -| CT_transparent(x1) -> - fID_NE_LIST x1 ++ - fNODE "transparent" 1 | CT_undo(x1) -> fINT_OPT x1 ++ fNODE "undo" 1 @@ -640,6 +638,10 @@ and fCOMMAND = function fID x1 ++ fSTRING_OPT x2 ++ fNODE "write_module" 2 +and fLEVEL = function +| CT_Opaque -> fNODE "opaque" 0 +| CT_Level n -> fINT n ++ fNODE "level" 1 +| CT_Expand -> fNODE "expand" 0 and fCOMMAND_LIST = function | CT_command_list(x,l) -> fCOMMAND x ++ diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 1095228b5..b3909d317 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1796,13 +1796,11 @@ let rec xlate_vernac = ctf_ID_OPT_SOME (xlate_ident s)) | VernacEndProof Admitted -> CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Admitted"), ctv_ID_OPT_NONE) - | VernacSetOpacity (false, id :: idl) -> - CT_transparent(CT_id_ne_list(loc_qualid_to_ct_ID id, - List.map loc_qualid_to_ct_ID idl)) - | VernacSetOpacity (true, id :: idl) - -> CT_opaque (CT_id_ne_list(loc_qualid_to_ct_ID id, - List.map loc_qualid_to_ct_ID idl)) - | VernacSetOpacity (_, []) -> xlate_error "Shouldn't occur" + | VernacSetOpacity l -> + CT_strategy(CT_level_list + (List.map (fun (l,q) -> + (level_to_ct_LEVEL l, + CT_id_list(List.map loc_qualid_to_ct_ID q))) l)) | VernacUndo n -> CT_undo (CT_coerce_INT_to_INT_OPT (CT_int n)) | VernacShow (ShowGoal nopt) -> CT_show_goal (xlate_int_opt nopt) | VernacShow ShowNode -> CT_show_node @@ -2196,7 +2194,12 @@ let rec xlate_vernac = | VernacBack _ | VernacBacktrack _ |VernacBackTo _|VernacRestoreState _| VernacWriteState _| VernacSolveExistential (_, _)|VernacCanonical _ | VernacTacticNotation _ | VernacUndoTo _ | VernacRemoveName _) - -> xlate_error "TODO: vernac";; + -> xlate_error "TODO: vernac" +and level_to_ct_LEVEL = function + Conv_oracle.Opaque -> CT_Opaque + | Conv_oracle.Level n -> CT_Level (CT_int n) + | Conv_oracle.Expand -> CT_Expand;; + let rec xlate_vernac_list = function diff --git a/contrib/setoid_ring/Field_theory.v b/contrib/setoid_ring/Field_theory.v index f5c550417..65a397acc 100644 --- a/contrib/setoid_ring/Field_theory.v +++ b/contrib/setoid_ring/Field_theory.v @@ -661,6 +661,8 @@ Fixpoint FEeval (l : list R) (pe : FExpr) {struct pe} : R := | FEpow x n => rpow (FEeval l x) (Cp_phi n) end. +Strategy expand [FEeval]. + (* The result of the normalisation *) Record linear : Type := mk_linear { diff --git a/contrib/setoid_ring/Ring_polynom.v b/contrib/setoid_ring/Ring_polynom.v index 45b38e2ed..d88470369 100644 --- a/contrib/setoid_ring/Ring_polynom.v +++ b/contrib/setoid_ring/Ring_polynom.v @@ -1186,6 +1186,8 @@ Proof. | PEpow pe1 n => rpow (PEeval l pe1) (Cp_phi n) end. +Strategy expand [PEeval]. + (** Correctness proofs *) Lemma mkX_ok : forall p l, nth 0 p l == (mk_X p) @ l. diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 59217b352..afe31d0d2 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -123,8 +123,6 @@ can cause changes in tactic scripts behaviour. At section or module closing, a constant recovers the status it got at the time of its definition. -%TODO: expliquer le rapport avec les sections - \begin{ErrMsgs} % \item \errindex{Can not set transparent.}\\ % It is a constant from a required module or a parameter. @@ -136,6 +134,34 @@ environment}\\ \SeeAlso sections \ref{Conversion-tactics}, \ref{Automatizing}, \ref{Theorem} + +\subsection{\tt Strategy {\it level} [ \qualid$_1$ \dots \qualid$_n$ ].\comindex{Strategy}\label{Strategy}} +This command generalizes the behaviour of {\tt Opaque} and {\tt + Transaparent} commands. It is used to fine-tune the strategy for +unfolding constants, both at the tactic level and at the kernel +level. This command associates a level to \qualid$_1$ \dots +\qualid$_n$. Whenever two expressions with two distinct head +constants are compared (for instance, this comparison can be triggered +by a type cast), the one with lower level is expanded first. In case +of a tie, the second one (appearing in the cast type) is expanded. + +Levels can be one of the following (higher to lower): +\begin{description} +\item[opaque]: level of opaque constants. They cannot be expanded by + tactics (behaves like $+\infty$, see next item). +\item[\num]: levels indexed by an integer. Level $0$ corresponds + to the default behaviour, which corresponds to transparent + constants. This level can also be referred to as {\bf transparent}. + Negative levels correspond to constants to be expanded before normal + transparent constants, while positive levels correspond to constants + to be expanded after normal transparent constants. +\item[expand]: level of constants that should be expanded first + (behaves like $-\infty$) +\end{description} + +The behaviour regarding sections and modules is the same as for the +{\tt Transparent} command. + \subsection[\tt Search {\qualid}.]{\tt Search {\qualid}.\comindex{Search}} This command displays the name and type of all theorems of the current context whose statement's conclusion has the form {\tt ({\qualid} t1 .. diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 2efe88c0c..27f80fd75 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -446,9 +446,13 @@ GEXTEND Gram gallina_ext: [ [ (* Transparent and Opaque *) - IDENT "Transparent"; l = LIST1 global -> VernacSetOpacity (false, l) - | IDENT "Opaque"; l = LIST1 global -> VernacSetOpacity (true, l) - + IDENT "Transparent"; l = LIST1 global -> + VernacSetOpacity [Conv_oracle.transparent,l] + | IDENT "Opaque"; l = LIST1 global -> + VernacSetOpacity [Conv_oracle.Opaque, l] + | IDENT "Strategy"; l = + LIST1 [ lev=strategy_level; "["; q=LIST1 global; "]" -> (lev,q)] -> + VernacSetOpacity l (* Canonical structure *) | IDENT "Canonical"; IDENT "Structure"; qid = global -> VernacCanonical qid @@ -542,6 +546,13 @@ GEXTEND Gram [ [ ":="; l = LIST1 typeclass_field_def SEP ";" -> l | -> [] ] ] ; + strategy_level: + [ [ IDENT "expand" -> Conv_oracle.Expand + | IDENT "opaque" -> Conv_oracle.Opaque + | n=INT -> Conv_oracle.Level (int_of_string n) + | "-"; n=INT -> Conv_oracle.Level (- int_of_string n) + | IDENT "transparent" -> Conv_oracle.transparent ] ] + ; END GEXTEND Gram diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index a863665a9..afa28768f 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -829,9 +829,22 @@ let rec pr_vernac = function str (if List.length idl > 1 then "s " else " ") ++ prlist_with_sep spc pr_lident idl ++ str " :" ++ spc () ++ pr_lconstr c) - | VernacSetOpacity (fl,l) -> - hov 1 ((if fl then str"Opaque" else str"Transparent") ++ + | VernacSetOpacity[k,l] when k=Conv_oracle.transparent -> + hov 1 (str"Transparent" ++ spc() ++ prlist_with_sep sep pr_reference l) + | VernacSetOpacity[Conv_oracle.Opaque,l] -> + hov 1 (str"Opaque" ++ + spc() ++ prlist_with_sep sep pr_reference l) + | VernacSetOpacity l -> + let pr_lev = function + Conv_oracle.Opaque -> str"opaque" + | Conv_oracle.Expand -> str"expand" + | l when l = Conv_oracle.transparent -> str"transparent" + | Conv_oracle.Level n -> int n in + let pr_line (l,q) = + hov 2 (pr_lev l ++ spc() ++ + str"[" ++ prlist_with_sep sep pr_reference q ++ str"]") in + hov 1 (str"Strategy" ++ spc() ++ hv 0 (prlist_with_sep sep pr_line l)) | VernacUnsetOption na -> hov 1 (str"Unset" ++ spc() ++ pr_printoption na None) | VernacSetOption (na,v) -> hov 2 (str"Set" ++ spc() ++ pr_set_option na v) diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 6ca3a5c1a..dc242e8ca 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -116,12 +116,14 @@ type opacity = let opacity env = function | VarRef v when pi2 (Environ.lookup_named v env) <> None -> - Some (TransparentMaybeOpacified (Conv_oracle.is_opaque_var v)) + Some (TransparentMaybeOpacified + (not (Reductionops.is_transparent(VarKey v)))) | ConstRef cst -> let cb = Environ.lookup_constant cst env in if cb.const_body = None then None else if cb.const_opaque then Some FullyOpaque - else Some (TransparentMaybeOpacified (Conv_oracle.is_opaque_cst cst)) + else Some (TransparentMaybeOpacified + (not(Reductionops.is_transparent(ConstKey cst)))) | _ -> None let print_opacity ref = diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 55b82e214..5f5b47783 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -601,6 +601,9 @@ let fakey = Profile.declare_profile "fhnf_apply";; let fhnf_apply info k h a = Profile.profile4 fakey fhnf_apply info k h a;; *) +let is_transparent k = + Conv_oracle.get_strategy k <> Conv_oracle.Opaque + (* Conversion utility functions *) type conversion_test = constraints -> constraints diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 7968e0db4..c9b157efd 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -190,6 +190,9 @@ val fix_recarg : fixpoint -> constr stack -> (int * constr) option val reduce_fix : local_state_reduction_function -> fixpoint -> constr stack -> fix_reduction_result +(*s Querying the kernel conversion oracle: opaque/transparent constants *) +val is_transparent : 'a tableKey -> bool + (*s Conversion Functions (uses closures, lazy strategy) *) type conversion_test = constraints -> constraints diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 3b5038766..05d108673 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -38,13 +38,11 @@ exception Redelimination let is_evaluable env ref = match ref with EvalConstRef kn -> - let (ids,kns) = Conv_oracle.freeze() in - Cpred.mem kn kns & + is_transparent (ConstKey kn) && let cb = Environ.lookup_constant kn env in cb.const_body <> None & not cb.const_opaque | EvalVarRef id -> - let (ids,sps) = Conv_oracle.freeze() in - Idpred.mem id ids & + is_transparent (VarKey id) && let (_,value,_) = Environ.lookup_named id env in value <> None diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 94468e6dc..a6de33ace 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -136,10 +136,13 @@ let default_no_delta_unify_flags = { } let expand_constant env flags c = - let (ids,csts) = Conv_oracle.freeze() in match kind_of_term c with - | Const cst when Cpred.mem cst csts && Cpred.mem cst (snd flags.modulo_delta) -> constant_opt_value env cst - | Var id when Idpred.mem id ids && Idpred.mem id (fst flags.modulo_delta) -> named_body id env + | Const cst when is_transparent (ConstKey cst) && + Cpred.mem cst (snd flags.modulo_delta) -> + constant_opt_value env cst + | Var id when is_transparent (VarKey id) && + Idpred.mem id (fst flags.modulo_delta) -> + named_body id env | _ -> None let unify_0_with_initial_metas subst conv_at_top env sigma cv_pb flags m n = diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 2f85b18e5..28e121ab2 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -26,23 +26,20 @@ let cbv_vm env _ c = let ctyp = (fst (Typeops.infer env c)).Environ.uj_type in Vnorm.cbv_vm env c ctyp - -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 set_strategy k l = + Conv_oracle.set_strategy k l; + match k,l with + ConstKey sp, Conv_oracle.Opaque -> + Csymtable.set_opaque_const sp + | ConstKey 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."); + Csymtable.set_transparent_const sp + | _ -> () let _ = Summary.declare_summary "Transparent constants and variables" @@ -70,7 +67,7 @@ let make_flag f = 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 + let red = red_add_transparent red (Conv_oracle.get_transp_state()) in List.fold_right (fun v red -> red_sub red (make_flag_constant v)) f.rConst red diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli index fee3f9813..404a8a196 100644 --- a/proofs/redexpr.mli +++ b/proofs/redexpr.mli @@ -25,13 +25,8 @@ val reduction_of_red_expr : red_expr -> reduction_function * cast_kind 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 - +val set_strategy : 'a tableKey -> Conv_oracle.level -> unit (* call by value normalisation function using the virtual machine *) val cbv_vm : reduction_function diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index c705d0287..cf123f584 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -885,15 +885,16 @@ let _ = optread=(fun () -> get_debug () <> Tactic_debug.DebugOff); optwrite=vernac_debug } -let vernac_set_opacity opaq r = - match global_with_alias r with - | ConstRef sp -> - if opaq then set_opaque_const sp - else set_transparent_const sp - | VarRef id -> - if opaq then set_opaque_var id - else set_transparent_var id - | _ -> error "cannot set an inductive type or a constructor as transparent" +let vernac_set_opacity r = + let set_one l r = + let r = + match global_with_alias r with + | ConstRef sp -> ConstKey sp + | VarRef id -> VarKey id + | _ -> error + "cannot set an inductive type or a constructor as transparent" in + set_strategy r l in + List.iter (fun (l,q) -> List.iter (set_one l) q) r let vernac_set_option key = function | StringValue s -> set_string_option_value key s @@ -1268,7 +1269,7 @@ let interp c = match c with | VernacSyntacticDefinition (id,c,l,b) ->vernac_syntactic_definition id c l b | VernacDeclareImplicits (local,qid,l) ->vernac_declare_implicits local qid l | VernacReserve (idl,c) -> vernac_reserve idl c - | VernacSetOpacity (opaq, qidl) -> List.iter (vernac_set_opacity opaq) qidl + | VernacSetOpacity qidl -> vernac_set_opacity qidl | VernacSetOption (key,v) -> vernac_set_option key v | VernacUnsetOption key -> vernac_unset_option key | VernacRemoveOption (key,v) -> vernac_remove_option key v diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 986c63c0b..fd6beb295 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -293,7 +293,7 @@ type vernac_expr = | VernacDeclareImplicits of locality_flag * lreference * (explicitation * bool * bool) list option | VernacReserve of lident list * constr_expr - | VernacSetOpacity of opacity_flag * lreference list + | VernacSetOpacity of (Conv_oracle.level * lreference list) list | VernacUnsetOption of Goptions.option_name | VernacSetOption of Goptions.option_name * option_value | VernacAddOption of Goptions.option_name * option_ref_value list |