aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/interface/ascent.mli9
-rw-r--r--contrib/interface/vtp.ml14
-rw-r--r--contrib/interface/xlate.ml19
-rw-r--r--contrib/setoid_ring/Field_theory.v2
-rw-r--r--contrib/setoid_ring/Ring_polynom.v2
-rw-r--r--doc/refman/RefMan-oth.tex30
-rw-r--r--parsing/g_vernac.ml417
-rw-r--r--parsing/ppvernac.ml17
-rw-r--r--parsing/prettyp.ml6
-rw-r--r--pretyping/reductionops.ml3
-rw-r--r--pretyping/reductionops.mli3
-rw-r--r--pretyping/tacred.ml6
-rw-r--r--pretyping/unification.ml9
-rw-r--r--proofs/redexpr.ml33
-rw-r--r--proofs/redexpr.mli7
-rw-r--r--toplevel/vernacentries.ml21
-rw-r--r--toplevel/vernacexpr.ml2
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 23:16:59 +0000