aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-11-20 18:17:58 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-11-27 19:47:52 +0100
commit9243166490e8c939bbf6aa0316e99025b25e6398 (patch)
tree391e1d205ee7a378774228404e5a7c00416e2d97 /vernac
parent6f240e9b15f2b6f6622c811933c4f5ffdf78cceb (diff)
[vernac] Adjust `interp` to pass polymorphic in the attributes.
Diffstat (limited to 'vernac')
-rw-r--r--vernac/vernacentries.ml88
-rw-r--r--vernac/vernacentries.mli2
2 files changed, 53 insertions, 37 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index c176312e0..c737707cf 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2114,7 +2114,7 @@ let check_vernac_supports_polymorphism c p =
| None, _ -> ()
| Some _, (
VernacDefinition _ | VernacFixpoint _ | VernacCoFixpoint _
- | VernacAssumption _ | VernacInductive _
+ | VernacAssumption _ | VernacInductive _
| VernacStartTheoremProof _
| VernacCoercion _ | VernacIdentityCoercion _
| VernacInstance _ | VernacDeclareInstances _
@@ -2123,7 +2123,7 @@ let check_vernac_supports_polymorphism c p =
| Some _, _ -> user_err Pp.(str "This command does not support Polymorphism")
let enforce_polymorphism = function
- | None -> Flags.is_universe_polymorphism ()
+ | None -> Flags.is_universe_polymorphism ()
| Some b -> Flags.make_polymorphic_flag b; b
(** A global default timeout, controlled by option "Set Default Timeout n".
@@ -2191,43 +2191,57 @@ let with_fail st b f =
| _ -> assert false
end
-let interp ?(verbosely=true) ?proof st (loc,c) =
+let interp ?(verbosely=true) ?proof ~st (loc,c) =
let orig_program_mode = Flags.is_program_mode () in
- let rec aux ?locality ?polymorphism isprogcmd = function
-
- | VernacProgram c when not isprogcmd -> aux ?locality ?polymorphism true c
- | VernacProgram _ -> user_err Pp.(str "Program mode specified twice")
- | VernacLocal (b, c) when Option.is_empty locality ->
- aux ~locality:b ?polymorphism isprogcmd c
- | VernacPolymorphic (b, c) when polymorphism = None ->
- aux ?locality ~polymorphism:b isprogcmd c
- | VernacPolymorphic (b, c) -> user_err Pp.(str "Polymorphism specified twice")
- | VernacLocal _ -> user_err Pp.(str "Locality specified twice")
+ let rec aux ?polymorphism ~atts isprogcmd = function
+
+ | VernacProgram c when not isprogcmd ->
+ aux ?polymorphism ~atts true c
+
+ | VernacProgram _ ->
+ user_err Pp.(str "Program mode specified twice")
+
+ | VernacPolymorphic (b, c) when polymorphism = None ->
+ aux ~polymorphism:b ~atts:atts isprogcmd c
+
+ | VernacPolymorphic (b, c) ->
+ user_err Pp.(str "Polymorphism specified twice")
+
+ | VernacLocal (b, c) when Option.is_empty atts.locality ->
+ aux ?polymorphism ~atts:{atts with locality = Some b} isprogcmd c
+
+ | VernacLocal _ ->
+ user_err Pp.(str "Locality specified twice")
+
| VernacFail v ->
- with_fail st true (fun () -> aux ?locality ?polymorphism isprogcmd v)
+ with_fail st true (fun () -> aux ?polymorphism ~atts isprogcmd v)
+
| VernacTimeout (n,v) ->
- current_timeout := Some n;
- aux ?locality ?polymorphism isprogcmd v
+ current_timeout := Some n;
+ aux ?polymorphism ~atts isprogcmd v
+
| VernacRedirect (s, (_,v)) ->
- Topfmt.with_output_to_file s (aux ?locality ?polymorphism isprogcmd) v
+ Topfmt.with_output_to_file s (aux ?polymorphism ~atts isprogcmd) v
+
| VernacTime (_,v) ->
- System.with_time !Flags.time
- (aux ?locality ?polymorphism isprogcmd) v;
- | VernacLoad (_,fname) -> vernac_load (aux false) fname
- | c ->
- check_vernac_supports_locality c locality;
- check_vernac_supports_polymorphism c polymorphism;
- let polymorphic = enforce_polymorphism polymorphism in
- Obligations.set_program_mode isprogcmd;
- try
- vernac_timeout begin fun () ->
- let atts = { loc; locality; polymorphic } in
- if verbosely
- then Flags.verbosely (interp ?proof ~atts ~st) c
- else Flags.silently (interp ?proof ~atts ~st) c;
+ System.with_time !Flags.time (aux ?polymorphism ~atts isprogcmd) v;
+
+ | VernacLoad (_,fname) -> vernac_load (aux ?polymorphism ~atts false) fname
+
+ | c ->
+ check_vernac_supports_locality c atts.locality;
+ check_vernac_supports_polymorphism c polymorphism;
+ let polymorphic = enforce_polymorphism polymorphism in
+ Obligations.set_program_mode isprogcmd;
+ try
+ vernac_timeout begin fun () ->
+ let atts = { atts with polymorphic } in
+ if verbosely
+ then Flags.verbosely (interp ?proof ~atts ~st) c
+ else Flags.silently (interp ?proof ~atts ~st) c;
if orig_program_mode || not !Flags.program_mode || isprogcmd then
Flags.program_mode := orig_program_mode;
- ignore (Flags.use_polymorphic_flag ())
+ ignore (Flags.use_polymorphic_flag ())
end
with
| reraise when
@@ -2242,12 +2256,14 @@ let interp ?(verbosely=true) ?proof st (loc,c) =
ignore (Flags.use_polymorphic_flag ());
iraise e
in
- if verbosely then Flags.verbosely (aux false) c
- else aux false c
+ let atts = { loc; locality = None; polymorphic = false; } in
+ if verbosely
+ then Flags.verbosely (aux ~atts orig_program_mode) c
+ else aux ~atts orig_program_mode c
(* XXX: There is a bug here in case of an exception, see @gares
comments on the PR *)
-let interp ?verbosely ?proof st cmd =
+let interp ?verbosely ?proof ~st cmd =
Vernacstate.unfreeze_interp_state st;
- interp ?verbosely ?proof st cmd;
+ interp ?verbosely ?proof ~st cmd;
Vernacstate.freeze_interp_state `No
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 67001bc24..a559912a0 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -18,7 +18,7 @@ val vernac_require :
val interp :
?verbosely:bool ->
?proof:Proof_global.closed_proof ->
- Vernacstate.t -> Vernacexpr.vernac_expr Loc.located -> Vernacstate.t
+ st:Vernacstate.t -> Vernacexpr.vernac_expr Loc.located -> Vernacstate.t
(** Prepare a "match" template for a given inductive type.
For each branch of the match, we list the constructor name