From c6cd7c39fc0da9c578cac57c9d06ddb28f0586fd Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 19 Sep 2018 14:14:03 +0200 Subject: Move attributes out of vernacinterp to new attributes module --- stm/vernac_classifier.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'stm') diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 85babd922b..b393093601 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -194,8 +194,8 @@ let classify_vernac e = in let rec static_control_classifier ~poly = function | VernacExpr (f, e) -> - let _, atts = Vernacentries.attributes_of_flags f Vernacinterp.(mk_atts ~polymorphic:poly ()) in - let poly = atts.Vernacinterp.polymorphic in + let _, atts = Vernacentries.attributes_of_flags f Attributes.(mk_atts ~polymorphic:poly ()) in + let poly = atts.Attributes.polymorphic in static_classifier ~poly e | VernacTimeout (_,e) -> static_control_classifier ~poly e | VernacTime (_,{v=e}) | VernacRedirect (_, {v=e}) -> -- cgit v1.2.3 From 80785aee7924309ab21b8ce1dcf7964559531216 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 19 Sep 2018 14:26:22 +0200 Subject: {Vernacentries -> Attributes}.attributes_of_flags --- stm/vernac_classifier.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index b393093601..037c63ef03 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -194,7 +194,7 @@ let classify_vernac e = in let rec static_control_classifier ~poly = function | VernacExpr (f, e) -> - let _, atts = Vernacentries.attributes_of_flags f Attributes.(mk_atts ~polymorphic:poly ()) in + let _, atts = Attributes.attributes_of_flags f Attributes.(mk_atts ~polymorphic:poly ()) in let poly = atts.Attributes.polymorphic in static_classifier ~poly e | VernacTimeout (_,e) -> static_control_classifier ~poly e -- cgit v1.2.3 From 8db938764d87cceee6669b339e0f995edd40fc3e Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 20 Sep 2018 16:48:54 +0200 Subject: Command driven attributes. Commands need to request the attributes they use, with the API encouraging them to error on unsupported attributes. --- stm/vernac_classifier.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'stm') diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 037c63ef03..4958f17212 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -194,9 +194,8 @@ let classify_vernac e = in let rec static_control_classifier ~poly = function | VernacExpr (f, e) -> - let _, atts = Attributes.attributes_of_flags f Attributes.(mk_atts ~polymorphic:poly ()) in - let poly = atts.Attributes.polymorphic in - static_classifier ~poly e + let poly' = Attributes.(parse_drop_extra polymorphic f) in + static_classifier ~poly:(Option.default poly poly') e | VernacTimeout (_,e) -> static_control_classifier ~poly e | VernacTime (_,{v=e}) | VernacRedirect (_, {v=e}) -> static_control_classifier ~poly e -- cgit v1.2.3 From cc95e2f89f88a6e37f1d98ce55e479491c40145a Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 9 Oct 2018 15:01:38 +0200 Subject: Make attributes more general to make defining #[universes(...)] easy --- stm/vernac_classifier.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'stm') diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 4958f17212..f3961327d8 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -194,7 +194,7 @@ let classify_vernac e = in let rec static_control_classifier ~poly = function | VernacExpr (f, e) -> - let poly' = Attributes.(parse_drop_extra polymorphic f) in + let poly' = Attributes.(parse_drop_extra polymorphic_nowarn f) in static_classifier ~poly:(Option.default poly poly') e | VernacTimeout (_,e) -> static_control_classifier ~poly e | VernacTime (_,{v=e}) | VernacRedirect (_, {v=e}) -> -- cgit v1.2.3 From 9a1e658860b6320830698f197b69694c661ecfa0 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 11 Oct 2018 18:21:29 +0200 Subject: Add comment in stm to unsupport attributes for special commands --- stm/stm.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 19915b1600..07049815ef 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1077,6 +1077,7 @@ let stm_vernac_interp ?proof ?route id st { verbose; loc; expr } : Vernacstate.t | _ -> false in let aux_interp st expr = + (* XXX unsupported attributes *) let cmd = Vernacprop.under_control expr in if is_filtered_command cmd then (stm_pperr_endline Pp.(fun () -> str "ignoring " ++ Ppvernac.pr_vernac expr); st) -- cgit v1.2.3 From c44080b74f4ea1e4b7ae88dfe5a440364bed3fca Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 11 Oct 2018 19:08:33 +0200 Subject: Universe Polymorphism is a normal attribute modulo the stm (no Flags) --- stm/stm.ml | 2 +- stm/vernac_classifier.ml | 16 ++++++++-------- 2 files changed, 9 insertions(+), 9 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 07049815ef..cfadada104 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2133,7 +2133,7 @@ and Reach : sig end = struct (* {{{ *) let async_policy () = - if Flags.is_universe_polymorphism () then false + if Attributes.is_universe_polymorphism () then false else if VCS.is_interactive () = `Yes then (async_proofs_is_master !cur_opt || !cur_opt.async_proofs_mode = APonLazy) else diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index f3961327d8..c93487d377 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -50,7 +50,7 @@ let idents_of_name : Names.Name.t -> Names.Id.t list = let stm_allow_nested_proofs_option_name = ["Nested";"Proofs";"Allowed"] let options_affecting_stm_scheduling = - [ Vernacentries.universe_polymorphism_option_name; + [ Attributes.universe_polymorphism_option_name; stm_allow_nested_proofs_option_name ] let classify_vernac e = @@ -192,15 +192,15 @@ let classify_vernac e = try Vernacentries.get_vernac_classifier s l with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".") in - let rec static_control_classifier ~poly = function + let rec static_control_classifier = function | VernacExpr (f, e) -> - let poly' = Attributes.(parse_drop_extra polymorphic_nowarn f) in - static_classifier ~poly:(Option.default poly poly') e - | VernacTimeout (_,e) -> static_control_classifier ~poly e + let poly = Attributes.(parse_drop_extra polymorphic_nowarn f) in + static_classifier ~poly e + | VernacTimeout (_,e) -> static_control_classifier e | VernacTime (_,{v=e}) | VernacRedirect (_, {v=e}) -> - static_control_classifier ~poly e + static_control_classifier e | VernacFail e -> (* Fail Qed or Fail Lemma must not join/fork the DAG *) - (match static_control_classifier ~poly e with + (match static_control_classifier e with | ( VtQuery | VtProofStep _ | VtSideff _ | VtProofMode _ | VtMeta), _ as x -> x | VtQed _, _ -> @@ -208,7 +208,7 @@ let classify_vernac e = VtNow | (VtStartProof _ | VtUnknown), _ -> VtUnknown, VtNow) in - static_control_classifier ~poly:(Flags.is_universe_polymorphism ()) e + static_control_classifier e let classify_as_query = VtQuery, VtLater let classify_as_sideeff = VtSideff [], VtLater -- cgit v1.2.3