Skip to content

Commit

Permalink
Merge PR coq#17818: Move typed_vernac to its own file from vernacextend
Browse files Browse the repository at this point in the history 
Reviewed-by: ejgallego
Co-authored-by: ejgallego <[email protected]>
  • Loading branch information
@coqbot-app @ejgallego
coqbot-app[bot] and ejgallego authored Sep 15, 2023
2 parents cba4339 + 349ed92 commit a298694
Show file tree
Hide file tree
Showing 13 changed files with 253 additions and 230 deletions.
4 changes: 2 additions & 2 deletions coqpp/coqpp_main.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -410,11 +410,11 @@ let pr_end_wrapper fmt = function
let print_body_state state fmt r =
let state = match r.vernac_state with Some _ as s -> s | None -> state in
match state with
| None -> fprintf fmt "Vernacextend.vtdefault (fun () -> %a)" print_code r.vernac_body
| None -> fprintf fmt "Vernactypes.vtdefault (fun () -> %a)" print_code r.vernac_body
| Some "CUSTOM" -> print_code fmt r.vernac_body
| Some state ->
let state, wrap = understand_state state in
fprintf fmt "Vernacextend.%s (%a (%a)%a)" state pr_begin_wrapper wrap
fprintf fmt "Vernactypes.%s (%a (%a)%a)" state pr_begin_wrapper wrap
print_code r.vernac_body pr_end_wrapper wrap

let print_body_fun state fmt r =
Expand Down
3 changes: 3 additions & 0 deletions dev/ci/user-overlays/17818-SkySkimmer-vernactypes.sh
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
overlay tactician https://github.com/SkySkimmer/coq-tactician vernactypes 17818

overlay elpi https://github.com/SkySkimmer/coq-elpi vernactypes 17818
2 changes: 2 additions & 0 deletions dev/top_printers.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -614,6 +614,7 @@ END

let () =
let open Vernacextend in
let open Vernactypes in
let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in
let cmd_sig = TyTerminal("PrintConstr", TyNonTerminal(ty_constr, TyNil)) in
let cmd_fn c ?loc:_ ~atts () = vtdefault (fun () -> in_current_context econstr_display c) in
Expand All @@ -623,6 +624,7 @@ let () =

let () =
let open Vernacextend in
let open Vernactypes in
let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in
let cmd_sig = TyTerminal("PrintPureConstr", TyNonTerminal(ty_constr, TyNil)) in
let cmd_fn c ?loc:_ ~atts () = vtdefault (fun () -> in_current_context print_pure_econstr c) in
Expand Down
4 changes: 2 additions & 2 deletions plugins/funind/g_indfun.mlg
View file
Original file line number Diff line number Diff line change
Expand Up @@ -211,11 +211,11 @@ VERNAC COMMAND EXTEND Function STATE CUSTOM
-> {
let warn = "-unused-pattern-matching-variable,-non-recursive" in
if is_interactive recsl then
Vernacextend.vtopenproof (fun () ->
Vernactypes.vtopenproof (fun () ->
CWarnings.with_warn warn
Gen_principle.do_generate_principle_interactive (List.map snd recsl))
else
Vernacextend.vtdefault (fun () ->
Vernactypes.vtdefault (fun () ->
CWarnings.with_warn warn
Gen_principle.do_generate_principle (List.map snd recsl))
}
Expand Down
2 changes: 1 addition & 1 deletion vernac/synterp.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -108,7 +108,7 @@ type synterp_entry =
| EVernacInclude of Declaremods.module_expr list
| EVernacSetOption of { export : bool; key : Goptions.option_name; value : Vernacexpr.option_setting }
| EVernacLoad of Vernacexpr.verbose_flag * (vernac_control_entry * Vernacstate.Synterp.t) list
| EVernacExtend of Vernacextend.typed_vernac
| EVernacExtend of Vernactypes.typed_vernac

and vernac_entry = synterp_entry Vernacexpr.vernac_expr_gen

Expand Down
2 changes: 1 addition & 1 deletion vernac/synterp.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ type synterp_entry =
| EVernacInclude of Declaremods.module_expr list
| EVernacSetOption of { export : bool; key : Goptions.option_name; value : Vernacexpr.option_setting }
| EVernacLoad of Vernacexpr.verbose_flag * (vernac_control_entry * Vernacstate.Synterp.t) list
| EVernacExtend of Vernacextend.typed_vernac
| EVernacExtend of Vernactypes.typed_vernac

and vernac_entry = synterp_entry Vernacexpr.vernac_expr_gen

Expand Down
12 changes: 6 additions & 6 deletions vernac/vernacentries.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1368,17 +1368,17 @@ let vernac_end_segment ~pm ~proof ({v=id} as lid) =
| _ -> assert false

let vernac_end_segment lid =
Vernacextend.TypedVernac {
Vernactypes.TypedVernac {
inprog = Use; outprog = Pop; inproof = UseOpt; outproof = No;
run = (fun ~pm ~proof ->
let () = vernac_end_segment ~pm ~proof lid in
(), ())
}

let vernac_begin_segment ~interactive f =
let inproof = Vernacextend.InProof.(if interactive then Reject else Ignore) in
let outprog = Vernacextend.OutProg.(if interactive then Push else No) in
Vernacextend.TypedVernac {
let inproof = Vernactypes.InProof.(if interactive then Reject else Ignore) in
let outprog = Vernactypes.OutProg.(if interactive then Push else No) in
Vernactypes.TypedVernac {
inprog = Ignore; outprog; inproof; outproof = No;
run = (fun ~pm ~proof ->
let () = f () in
Expand Down Expand Up @@ -2213,7 +2213,7 @@ let vernac_validate_proof ~pstate =
str "No issues found."
else prlist_with_sep fnl snd (Evar.Map.bindings evar_issues)

let translate_vernac_synterp ?loc ~atts v = let open Vernacextend in match v with
let translate_vernac_synterp ?loc ~atts v = let open Vernactypes in match v with
| EVernacNotation { local; decl } ->
vtdefault(fun () -> Metasyntax.add_notation_interpretation ~local (Global.env()) decl)

Expand Down Expand Up @@ -2273,7 +2273,7 @@ let translate_vernac_synterp ?loc ~atts v = let open Vernacextend in match v wit
(* Extensions *)
| EVernacExtend f -> f

let translate_pure_vernac ?loc ~atts v = let open Vernacextend in match v with
let translate_pure_vernac ?loc ~atts v = let open Vernactypes in match v with
| VernacAbortAll
| VernacRestart
| VernacUndo _
Expand Down
2 changes: 1 addition & 1 deletion vernac/vernacentries.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ val translate_vernac
: ?loc:Loc.t
-> atts:Attributes.vernac_flags
-> Synterp.vernac_entry
-> Vernacextend.typed_vernac
-> Vernactypes.typed_vernac

(** Vernacular require command, used by the command line *)
val vernac_require
Expand Down
145 changes: 1 addition & 144 deletions vernac/vernacextend.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@
open Util
open Pp
open CErrors
open Vernactypes

type vernac_keep_as = VtKeepAxiom | VtKeepDefined | VtKeepOpaque

Expand Down Expand Up @@ -51,150 +52,6 @@ and anon_abstracting_tac = bool (** abstracting anonymously its result *)

and proof_block_name = string (** open type of delimiters *)

module InProg = struct
type _ t =
| Ignore : unit t
| Use : Declare.OblState.t t

let cast (type a) (x:Declare.OblState.t) (ty:a t) : a =
match ty with
| Ignore -> ()
| Use -> x
end

module OutProg = struct
type _ t =
| No : unit t
| Yes : Declare.OblState.t t
| Push
| Pop

let cast (type a) (x:a) (ty:a t) (orig:Declare.OblState.t NeList.t) : Declare.OblState.t NeList.t =
match ty with
| No -> orig
| Yes -> NeList.map_head (fun _ -> x) orig
| Push -> NeList.push Declare.OblState.empty (Some orig)
| Pop -> (match NeList.tail orig with Some tl -> tl | None -> assert false)
end

module InProof = struct
type _ t =
| Ignore : unit t
| Reject : unit t
| Use : Declare.Proof.t t
| UseOpt : Declare.Proof.t option t

let cast (type a) (x:Declare.Proof.t option) (ty:a t) : a =
match x, ty with
| _, Ignore -> ()
| None, Reject -> ()
| Some _, Reject -> CErrors.user_err (Pp.str "Command not supported (Open proofs remain).")
| Some x, Use -> x
| None, Use -> CErrors.user_err (Pp.str "Command not supported (No proof-editing in progress).")
| _, UseOpt -> x
end

module OutProof = struct
type _ t =
| No : unit t
| Close : unit t
| Update : Declare.Proof.t t
| New : Declare.Proof.t t

end

type ('inprog,'outprog,'inproof,'outproof) vernac_type = {
inprog : 'inprog InProg.t;
outprog : 'outprog InProg.t;
inproof : 'inproof InProof.t;
outproof : 'outproof OutProof.t;
}

type typed_vernac =
TypedVernac : {
inprog : 'inprog InProg.t;
outprog : 'outprog OutProg.t;
inproof : 'inproof InProof.t;
outproof : 'outproof OutProof.t;
run : pm:'inprog -> proof:'inproof -> 'outprog * 'outproof;
} -> typed_vernac

let vtdefault f =
TypedVernac { inprog = Ignore; outprog = No; inproof = Ignore; outproof = No;
run = (fun ~pm:() ~proof:() ->
let () = f () in
(), ()) }

let vtnoproof f =
TypedVernac { inprog = Ignore; outprog = No; inproof = Ignore; outproof = No;
run = (fun ~pm:() ~proof:() ->
let () = f () in
(), ())
}

let vtcloseproof f =
TypedVernac { inprog = Use; outprog = Yes; inproof = Use; outproof = Close;
run = (fun ~pm ~proof ->
let pm = f ~lemma:proof ~pm in
pm, ())
}

let vtopenproof f =
TypedVernac { inprog = Ignore; outprog = No; inproof = Ignore; outproof = New;
run = (fun ~pm:() ~proof:() ->
let proof = f () in
(), proof)
}

let vtmodifyproof f =
TypedVernac { inprog = Ignore; outprog = No; inproof = Use; outproof = Update;
run = (fun ~pm:() ~proof ->
let proof = f ~pstate:proof in
(), proof)
}

let vtreadproofopt f =
TypedVernac { inprog = Ignore; outprog = No; inproof = UseOpt; outproof = No;
run = (fun ~pm:() ~proof ->
let () = f ~pstate:proof in
(), ())
}

let vtreadproof f =
TypedVernac { inprog = Ignore; outprog = No; inproof = Use; outproof = No;
run = (fun ~pm:() ~proof ->
let () = f ~pstate:proof in
(), ())
}

let vtreadprogram f =
TypedVernac { inprog = Use; outprog = No; inproof = Ignore; outproof = No;
run = (fun ~pm ~proof:() ->
let () = f ~pm in
(), ())
}

let vtmodifyprogram f =
TypedVernac { inprog = Use; outprog = Yes; inproof = Ignore; outproof = No;
run = (fun ~pm ~proof:() ->
let pm = f ~pm in
pm, ())
}

let vtdeclareprogram f =
TypedVernac { inprog = Use; outprog = No; inproof = Ignore; outproof = New;
run = (fun ~pm ~proof:() ->
let proof = f ~pm in
(), proof)
}

let vtopenproofprogram f =
TypedVernac { inprog = Use; outprog = Yes; inproof = Ignore; outproof = New;
run = (fun ~pm ~proof:() ->
let pm, proof = f ~pm in
pm, proof)
}

type vernac_command = ?loc:Loc.t -> atts:Attributes.vernac_flags -> unit -> typed_vernac

type plugin_args = Genarg.raw_generic_argument list
Expand Down
72 changes: 1 addition & 71 deletions vernac/vernacextend.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -67,77 +67,7 @@ and anon_abstracting_tac = bool (** abstracting anonymously its result *)

and proof_block_name = string (** open type of delimiters *)

(** Interpretation of extended vernac phrases. *)

module InProg : sig
type _ t =
| Ignore : unit t
| Use : Declare.OblState.t t

val cast : Declare.OblState.t -> 'a t -> 'a
end

module OutProg : sig
type _ t =
| No : unit t
| Yes : Declare.OblState.t t
| Push
| Pop

val cast : 'a -> 'a t -> Declare.OblState.t NeList.t -> Declare.OblState.t NeList.t
end

module InProof : sig
type _ t =
| Ignore : unit t
| Reject : unit t
| Use : Declare.Proof.t t
| UseOpt : Declare.Proof.t option t

val cast : Declare.Proof.t option -> 'a t -> 'a
end

module OutProof : sig

type _ t =
| No : unit t
| Close : unit t
| Update : Declare.Proof.t t
| New : Declare.Proof.t t

end

type ('inprog,'outprog,'inproof,'outproof) vernac_type = {
inprog : 'inprog InProg.t;
outprog : 'outprog InProg.t;
inproof : 'inproof InProof.t;
outproof : 'outproof OutProof.t;
}

type typed_vernac =
TypedVernac : {
inprog : 'inprog InProg.t;
outprog : 'outprog OutProg.t;
inproof : 'inproof InProof.t;
outproof : 'outproof OutProof.t;
run : pm:'inprog -> proof:'inproof -> 'outprog * 'outproof;
} -> typed_vernac

(** Some convenient typed_vernac constructors. Keep in sync with coqpp. *)

val vtdefault : (unit -> unit) -> typed_vernac
val vtnoproof : (unit -> unit) -> typed_vernac
val vtcloseproof : (lemma:Declare.Proof.t -> pm:Declare.OblState.t -> Declare.OblState.t) -> typed_vernac
val vtopenproof : (unit -> Declare.Proof.t) -> typed_vernac
val vtmodifyproof : (pstate:Declare.Proof.t -> Declare.Proof.t) -> typed_vernac
val vtreadproofopt : (pstate:Declare.Proof.t option -> unit) -> typed_vernac
val vtreadproof : (pstate:Declare.Proof.t -> unit) -> typed_vernac
val vtreadprogram : (pm:Declare.OblState.t -> unit) -> typed_vernac
val vtmodifyprogram : (pm:Declare.OblState.t -> Declare.OblState.t) -> typed_vernac
val vtdeclareprogram : (pm:Declare.OblState.t -> Declare.Proof.t) -> typed_vernac
val vtopenproofprogram : (pm:Declare.OblState.t -> Declare.OblState.t * Declare.Proof.t) -> typed_vernac

type vernac_command = ?loc:Loc.t -> atts:Attributes.vernac_flags -> unit -> typed_vernac
type vernac_command = ?loc:Loc.t -> atts:Attributes.vernac_flags -> unit -> Vernactypes.typed_vernac

type plugin_args = Genarg.raw_generic_argument list

Expand Down
4 changes: 2 additions & 2 deletions vernac/vernacinterp.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,9 +13,9 @@ open Synterp

let vernac_pperr_endline = CDebug.create ~name:"vernacinterp" ()

let interp_typed_vernac (Vernacextend.TypedVernac { inprog; outprog; inproof; outproof; run })
let interp_typed_vernac (Vernactypes.TypedVernac { inprog; outprog; inproof; outproof; run })
~pm ~stack =
let open Vernacextend in
let open Vernactypes in
let module LStack = Vernacstate.LemmaStack in
let proof = Option.map LStack.get_top stack in
let pm', proof' = run
Expand Down
Loading

0 comments on commit a298694

Please sign in to comment.