diff options
| -rw-r--r-- | contrib/interface/xlate.ml | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 9 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 9 | ||||
| -rw-r--r-- | parsing/ppvernac.ml | 9 | ||||
| -rw-r--r-- | parsing/prettyp.ml | 19 | ||||
| -rw-r--r-- | proofs/redexpr.ml | 64 | ||||
| -rw-r--r-- | proofs/redexpr.mli | 6 | ||||
| -rw-r--r-- | test-suite/complexity/ring2.v | 51 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 21 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 3 |
10 files changed, 160 insertions, 33 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index b3909d317..169ec0dc2 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1796,7 +1796,7 @@ 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 l -> + | VernacSetOpacity (_,l) -> CT_strategy(CT_level_list (List.map (fun (l,q) -> (level_to_ct_LEVEL l, diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index afe31d0d2..9a17c0f3c 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -135,7 +135,8 @@ environment}\\ \ref{Theorem} -\subsection{\tt Strategy {\it level} [ \qualid$_1$ \dots \qualid$_n$ ].\comindex{Strategy}\label{Strategy}} +\subsection{\tt Strategy {\it level} [ \qualid$_1$ \dots \qualid$_n$ + ].\comindex{Strategy}\comindex{Local 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 @@ -159,8 +160,10 @@ Levels can be one of the following (higher to lower): (behaves like $-\infty$) \end{description} -The behaviour regarding sections and modules is the same as for the -{\tt Transparent} command. +These directives survive section and module closure, unless the +command is prefixed by {\tt Local}. In the latter case, the behaviour +regarding sections and modules is the same as for the {\tt + Transparent} and {\tt Opaque} commands. \subsection[\tt Search {\qualid}.]{\tt Search {\qualid}.\comindex{Search}} This command displays the name and type of all theorems of the current diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 27f80fd75..437ef58fd 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -447,12 +447,15 @@ GEXTEND Gram gallina_ext: [ [ (* Transparent and Opaque *) IDENT "Transparent"; l = LIST1 global -> - VernacSetOpacity [Conv_oracle.transparent,l] + VernacSetOpacity (true,[Conv_oracle.transparent,l]) | IDENT "Opaque"; l = LIST1 global -> - VernacSetOpacity [Conv_oracle.Opaque, l] + VernacSetOpacity (true,[Conv_oracle.Opaque, l]) | IDENT "Strategy"; l = LIST1 [ lev=strategy_level; "["; q=LIST1 global; "]" -> (lev,q)] -> - VernacSetOpacity l + VernacSetOpacity (false,l) + | IDENT "Local"; IDENT "Strategy"; l = + LIST1 [ lev=strategy_level; "["; q=LIST1 global; "]" -> (lev,q)] -> + VernacSetOpacity (true,l) (* Canonical structure *) | IDENT "Canonical"; IDENT "Structure"; qid = global -> VernacCanonical qid diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index afa28768f..c31defe09 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -829,13 +829,13 @@ 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[k,l] when k=Conv_oracle.transparent -> + | VernacSetOpacity(true,[k,l]) when k=Conv_oracle.transparent -> hov 1 (str"Transparent" ++ spc() ++ prlist_with_sep sep pr_reference l) - | VernacSetOpacity[Conv_oracle.Opaque,l] -> + | VernacSetOpacity(true,[Conv_oracle.Opaque,l]) -> hov 1 (str"Opaque" ++ spc() ++ prlist_with_sep sep pr_reference l) - | VernacSetOpacity l -> + | VernacSetOpacity (local,l) -> let pr_lev = function Conv_oracle.Opaque -> str"opaque" | Conv_oracle.Expand -> str"expand" @@ -844,7 +844,8 @@ let rec pr_vernac = function 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)) + hov 1 (pr_locality local ++ 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 dc242e8ca..bdbd74b0f 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -112,18 +112,17 @@ let need_expansion impl ref = type opacity = | FullyOpaque - | TransparentMaybeOpacified of bool + | TransparentMaybeOpacified of Conv_oracle.level let opacity env = function | VarRef v when pi2 (Environ.lookup_named v env) <> None -> - Some (TransparentMaybeOpacified - (not (Reductionops.is_transparent(VarKey v)))) + Some(TransparentMaybeOpacified (Conv_oracle.get_strategy(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 - (not(Reductionops.is_transparent(ConstKey cst)))) + else Some + (TransparentMaybeOpacified (Conv_oracle.get_strategy(ConstKey cst))) | _ -> None let print_opacity ref = @@ -132,8 +131,14 @@ let print_opacity ref = | Some s -> pr_global ref ++ str " is " ++ str (match s with | FullyOpaque -> "opaque" - | TransparentMaybeOpacified true -> "basically transparent but considered opaque for reduction" - | TransparentMaybeOpacified false -> "transparent") ++ fnl() + | TransparentMaybeOpacified Conv_oracle.Opaque -> + "basically transparent but considered opaque for reduction" + | TransparentMaybeOpacified lev when lev = Conv_oracle.transparent -> + "transparent" + | TransparentMaybeOpacified (Conv_oracle.Level n) -> + "transparent (with expansion weight "^string_of_int n^")" + | TransparentMaybeOpacified Conv_oracle.Expand -> + "transparent (with minimal expansion weight)") ++ fnl() let print_name_infos ref = let impl = implicits_of_global ref in diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 28e121ab2..27db71755 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -19,14 +19,19 @@ open Reductionops open Tacred open Closure open RedFlags - +open Libobject (* call by value normalisation function using the virtual machine *) let cbv_vm env _ c = let ctyp = (fst (Typeops.infer env c)).Environ.uj_type in Vnorm.cbv_vm env c ctyp -let set_strategy k l = + +let set_strategy_one ref l = + let k = + match ref with + | EvalConstRef sp -> ConstKey sp + | EvalVarRef id -> VarKey id in Conv_oracle.set_strategy k l; match k,l with ConstKey sp, Conv_oracle.Opaque -> @@ -41,6 +46,61 @@ let set_strategy k l = Csymtable.set_transparent_const sp | _ -> () +let cache_strategy str = + List.iter + (fun (lev,ql) -> List.iter (fun q -> set_strategy_one q lev) ql) + str + +let subst_strategy (_,subs,obj) = + list_smartmap + (fun (k,ql as entry) -> + let ql' = list_smartmap (Mod_subst.subst_evaluable_reference subs) ql in + if ql==ql' then entry else (k,ql')) + obj + + +let map_strategy f l = + let l' = List.fold_right + (fun (lev,ql) str -> + let ql' = List.fold_right + (fun q ql -> + match f q with + Some q' -> q' :: ql + | None -> ql) ql [] in + if ql'=[] then str else (lev,ql')::str) l [] in + if l'=[] then None else Some l' + +let export_strategy obj = + map_strategy (function + EvalVarRef _ -> None + | EvalConstRef _ as q -> Some q) obj + +let classify_strategy (_,obj) = Substitute obj + +let disch_ref ref = + match ref with + EvalConstRef c -> + let c' = Lib.discharge_con c in + if c==c' then Some ref else Some (EvalConstRef c') + | _ -> Some ref + +let discharge_strategy (_,obj) = + map_strategy disch_ref obj + +let (inStrategy,outStrategy) = + declare_object {(default_object "STRATEGY") with + cache_function = (fun (_,obj) -> cache_strategy obj); + load_function = (fun _ (_,obj) -> cache_strategy obj); + subst_function = subst_strategy; + discharge_function = discharge_strategy; + classify_function = classify_strategy; + export_function = export_strategy } + + +let set_strategy local str = + if local then cache_strategy str + else Lib.add_anonymous_leaf (inStrategy str) + let _ = Summary.declare_summary "Transparent constants and variables" { Summary.freeze_function = Conv_oracle.freeze; diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli index 404a8a196..68c1fd669 100644 --- a/proofs/redexpr.mli +++ b/proofs/redexpr.mli @@ -26,7 +26,11 @@ val declare_red_expr : string -> reduction_function -> unit (* Opaque and Transparent commands. *) -val set_strategy : 'a tableKey -> Conv_oracle.level -> unit +(* Sets the expansion strategy of a constant. When the boolean is + true, the effect is non-synchronous (i.e. it does not survive + section and module closure). *) +val set_strategy : + bool -> (Conv_oracle.level * evaluable_global_reference list) list -> unit (* call by value normalisation function using the virtual machine *) val cbv_vm : reduction_function diff --git a/test-suite/complexity/ring2.v b/test-suite/complexity/ring2.v new file mode 100644 index 000000000..9f9685dde --- /dev/null +++ b/test-suite/complexity/ring2.v @@ -0,0 +1,51 @@ +(* This example, checks the efficiency of the abstract machine used by ring *) +(* Expected time < 1.00s *) + +Require Import BinInt. + +Definition Zplus x y := +match x with +| 0%Z => y +| Zpos x' => + match y with + | 0%Z => x + | Zpos y' => Zpos (x' + y') + | Zneg y' => + match (x' ?= y')%positive Eq with + | Eq => 0%Z + | Lt => Zneg (y' - x') + | Gt => Zpos (x' - y') + end + end +| Zneg x' => + match y with + | 0%Z => x + | Zpos y' => + match (x' ?= y')%positive Eq with + | Eq => 0%Z + | Lt => Zpos (y' - x') + | Gt => Zneg (x' - y') + end + | Zneg y' => Zneg (x' + y') + end +end. + +Require Import Ring. + +Lemma Zth : ring_theory Z0 (Zpos xH) Zplus Zmult Zminus Zopp (@eq Z). +Admitted. + +Ltac Zcst t := + match isZcst t with + true => t + | _ => constr:NotConstant + end. + +Add Ring Zr : Zth + (decidable Zeqb_ok, constants [Zcst]). + +Open Scope Z_scope. +Infix "+" := Zplus : Z_scope. + +Goal forall a, a+a+a+a+a+a+a+a+a+a+a+a+a = a*13. +Time intro; ring. diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index cf123f584..8c92329e5 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -885,16 +885,15 @@ let _ = optread=(fun () -> get_debug () <> Tactic_debug.DebugOff); optwrite=vernac_debug } -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_opacity local str = + let glob_ref r = + match global_with_alias r with + | ConstRef sp -> EvalConstRef sp + | VarRef id -> EvalVarRef id + | _ -> error + "cannot set an inductive type or a constructor as transparent" in + let str = List.map (fun (lev,ql) -> (lev,List.map glob_ref ql)) str in + Redexpr.set_strategy local str let vernac_set_option key = function | StringValue s -> set_string_option_value key s @@ -1269,7 +1268,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 qidl -> vernac_set_opacity qidl + | VernacSetOpacity (local,qidl) -> vernac_set_opacity local 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 fd6beb295..cce6f9a62 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -293,7 +293,8 @@ type vernac_expr = | VernacDeclareImplicits of locality_flag * lreference * (explicitation * bool * bool) list option | VernacReserve of lident list * constr_expr - | VernacSetOpacity of (Conv_oracle.level * lreference list) list + | VernacSetOpacity of + locality_flag * (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 |