Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7


Chronological Thread 
  • From: Matej Košík <mail AT matej-kosik.net>
  • To: coq-club AT inria.fr, kendroe AT hotmail.com
  • Subject: Re: [Coq-Club] Converting VERNAC COMMAND declaration to Coq 8.7
  • Date: Sat, 4 Nov 2017 14:30:41 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mail AT matej-kosik.net; spf=SoftFail smtp.mailfrom=mail AT matej-kosik.net; spf=SoftFail smtp.helo=postmaster AT matej-kosik.net
  • Ironport-phdr: 9a23:S+i1zxOLOe/gK5/sZu8l6mtUPXoX/o7sNwtQ0KIMzox0K/XzrarrMEGX3/hxlliBBdydsK0UzbeO+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6aj2O/9wESGwnycE9cbqSwQ9aKzpf/6+fn8JrKJg5MmTCVYLVoLRzwox+V/sobh4d4LasZyhzVp3JJf6JdwmY7C0iUmkPZ79u9/tZA9NbVuLp18sdBVY3/drg1T/lbCy8nMCYz6dG95kqLdheG+nZJCjZeqRFPGQWQqUiiBpo=
  • Openpgp: id=1CD41D0A52319DC7ABC1B79F50AFFA128CE48649; url=http://matej-kosik.net/doc/kosik.asc

Hi,

On 11/04/17 14:10, Kenneth Roe wrote:
> Didn't work.
>
> Does someone have a sample project that uses "VERNAC COMMAND EXTEND" (and
> also "TACTIC EXTEND" or what ever it became) for Coq 8.7?

The attached demo exercises some of those mechanisms.
(Compiles with the "v8.7" branch of Coq).

Let me know what you think.

---

Matej
(* This will be compilable once the following pull-request:
- https://github.com/coq/coq/pull/953
will be merged.

TODO: figure out why does Summary.Local.ref function require argument
"name" ?
(Can it be any string?
Must it be a unique string (per each state variable?)
Must it be a unique string global (for all plugins)?)
What would happen if it were an empty string?
*)

(* --------------------------------------------------------------------------
*)
(*
*)
(* Initial ritual dance
*)
(*
*)
(* --------------------------------------------------------------------------
*)

DECLARE PLUGIN "demo"

(*
Use this macro before any of the other Ocaml macros.

Each plugin has a unique name.
We have decided to name this plugin as "demo".
That means that:

(1) If we want to load this particular plugin to Coq toplevel,
we must use the following command.

Declare ML Module "demo".

(2) The above command will succeed only if there is "demo.cmxs"
in some of the directories that Coq is supposed to look
(i.e. the ones we specified via "-I ..." command line options).
*)

(* --------------------------------------------------------------------------
*)
(*
*)
(* How to define a new Vernacular command?
*)
(*
*)
(* --------------------------------------------------------------------------
*)

VERNAC COMMAND EXTEND Cmd1 CLASSIFIED AS QUERY
[ "Cmd1" ] -> [ () ]
END

(*
These:

VERNAC COMMAND EXTEND

and

END

mark the beginning and the end of the definition of a new Vernacular
command.

Cmd1 is a unique identifier (which must start with an upper-case letter)
associated with the new Vernacular command we are defining.

CLASSIFIED AS QUERY tells Coq that the new Vernacular command:
- changes neither the global environment
- nor does it modify the plugin's state.

If the new command could:
- change the global environment
- or modify a plugin's state
then one would have to use CLASSIFIED AS SIDEFF instead.

This:

[ "Cmd1" ] -> [ () ]

defines:
- the parsing rule
- the interpretation rule

The parsing rule and the interpretation rule are separated by -> token.

The parsing rule, in this case, is:

[ "Cmd1" ]

By convention, all vernacular command start with an upper-case letter.

The [ and ] characters mark the beginning and the end of the parsing rule.
The parsing rule itself says that the syntax of the newly defined command
is composed from a single terminal Cmd1.

The interpretation rule, in this case, is:

[ () ]

Like in case of the parsing rule,
[ and ] characters mark the beginning and the end of the interpretation
rule.
In this case, the following Ocaml expression:

()

defines the effect of the Vernacular command we have just defined.
That is, it behaves is no-op.
*)

(* --------------------------------------------------------------------------
*)
(*
*)
(* How to define a new Vernacular command with some terminal parameters?
*)
(*
*)
(* --------------------------------------------------------------------------
*)

VERNAC COMMAND EXTEND Cmd2 CLASSIFIED AS QUERY
[ "Cmd2" "With" "Some" "Terminal" "Parameters" ] -> [ () ]
END

(*
As shown above, the Vernacular command can be composed from
any number of terminals.

By convention, each of these terminals starts with an upper-case letter.
*)

(* --------------------------------------------------------------------------
*)
(*
*)
(* How to define a new Vernacular command with some non-terminal parameter?
*)
(*
*)
(* --------------------------------------------------------------------------
*)

open Stdarg

VERNAC COMMAND EXTEND Cmd3 CLASSIFIED AS QUERY
[ "Cmd3" int(i) ] -> [ () ]
END

(*
This:

open Stdarg

is needed as some identifiers in the Ocaml code generated by the

VERNAC COMMAND EXTEND ... END

macros are not fully qualified.

This:

int(i)

means that the new command is expected to be followed by an integer.
The integer is bound in the parsing rule to variable i.
This variable i then can be used in the interpretation rule.

To see value of which Ocaml types can be bound this way,
look at the wit_* function declared in interp/stdarg.mli
(in the Coq's codebase).

If we drop the wit_ prefix, we will get the token
that we can use in the parsing rule.
That is, since there exists wit_int, we know that
we can write:

int(i)

By looking at the signature of the wit_int function:

val wit_int : int uniform_genarg_type

we also know that variable i will have the type int.

The types of wit_* functions are either:

'c uniform_genarg_type

or

('a,'b,'c) genarg_type

In both cases, the bound variable will have type 'c.
*)

(* --------------------------------------------------------------------------
*)
(*
*)
(* How to define a new Vernacular command with variable number of arguments?
*)
(*
*)
(* --------------------------------------------------------------------------
*)

VERNAC COMMAND EXTEND Cmd4 CLASSIFIED AS QUERY
[ "Cmd4" int_list(l) ] -> [ () ]
END

(*
This:

int_list(l)

means that the new Vernacular command is expected to be followed
by a (whitespace separated) list of integers.
This list of integers is bound to the indicated l.

In this case, as well as in the cases we point out below, instead of int
in int_list we could use any other supported type, e.g. ident, bool, ...

To see which other Ocaml type constructors (in addition to list)
are supported, have a look at the parse_user_entry function defined
in grammar/q_util.mlp file.

E.g.:
- ne_int_list(x) would represent a non-empty list of integers,
- int_list(x) would represent a list of integers,
- int_opt(x) would represent a value of type int option,
- ···
*)

(* --------------------------------------------------------------------------
*)
(*
*)
(* How to define a new Vernacular command that takes values of a custom type?
*)
(*
*)
(* --------------------------------------------------------------------------
*)

open Ltac_plugin

(*
If we want to avoid a compilation failure

"no implementation available for Tacenv"

then we have to open the Ltac_plugin module.
*)

(*
Pp module must be opened because some of the macros that are part of the
API
do not expand to fully qualified names.
*)

type type_5 = Foo_5 | Bar_5

(*
We define a type of values that we want to pass to our Vernacular command.
*)

(*
By default, we are able to define new Vernacular commands that can take
parameters of some of the supported types. Which types are supported,
that was discussed earlier.

If we want to be able to define Vernacular command that takes parameters
of a type that is not supported by default, we must use the following
macro:
*)

open Pp

VERNAC ARGUMENT EXTEND custom5
| [ "Foo_5" ] -> [ Foo_5 ]
| [ "Bar_5" ] -> [ Bar_5 ]
END

(*
where:

custom5

indicates that, from now on, in our parsing rules we can write:

custom5(some_variable)

in those places where we expect user to provide an input
that can be parsed by the parsing rules above
(and interpreted by the interpretations rules above).
*)

(* Here: *)

VERNAC COMMAND EXTEND Cmd5 CLASSIFIED AS QUERY
[ "Cmd5" custom5(x) ] -> [ () ]
END

(*
we define a new Vernacular command whose parameters, provided by the user,
can be mapped to values of type_5.
*)

(* --------------------------------------------------------------------------
*)
(*
*)
(* How to give a feedback to the user?
*)
(*
*)
(* --------------------------------------------------------------------------
*)

VERNAC COMMAND EXTEND Cmd6 CLASSIFIED AS QUERY
[ "Cmd6" ] -> [ Feedback.msg_notice (Pp.str "Everything is awesome!") ]
END

(*
The following functions:

- Feedback.msg_info : Pp.t -> unit
- Feedback.msg_notice : Pp.t -> unit
- Feedback.msg_warning : Pp.t -> unit
- Feedback.msg_error : Pp.t -> unit
- Feedback.msg_debug : Pp.t -> unit

enable us to give user a textual feedback.

Pp module enable us to represent and construct pretty-printing
instructions.
The concepts defined and the services provided by the Pp module are in
various respects related to the concepts and services provided
by the Format module that is part of the Ocaml standard library.
*)

(* --------------------------------------------------------------------------
*)
(*
*)
(* How to implement a Vernacular command with (undoable) side-effects?
*)
(*
*)
(* --------------------------------------------------------------------------
*)

open Summary.Local

(*
By opening Summary.Local module we shadow the original functions
that we traditionally use for implementing stateful behavior.

ref
!
:=

are now shadowed by their counterparts in Summary.Local. *)

let counter = ref ~name:"counter" 0

VERNAC COMMAND EXTEND Cmd7 CLASSIFIED AS SIDEFF
[ "Cmd7" ] -> [ counter := succ !counter;
Feedback.msg_notice (Pp.str "counter = " ++ Pp.str
(string_of_int (!counter))) ]
END

TACTIC EXTEND tactic1
[ "tactic1" ] -> [ Proofview.tclUNIT () ]
END

(* ---- *)

type custom = Foo_2 | Bar_2

let pr_custom _ _ _ = function
| Foo_2 -> Pp.str "Foo_2"
| Bar_2 -> Pp.str "Bar_2"

ARGUMENT EXTEND custom2 PRINTED BY pr_custom
| [ "Foo_2" ] -> [ Foo_2 ]
| [ "Bar_2" ] -> [ Bar_2 ]
END

TACTIC EXTEND tactic2
[ "tactic2" custom2(x) ] -> [ Proofview.tclUNIT () ]
END

Attachment: signature.asc
Description: OpenPGP digital signature




Archive powered by MHonArc 2.6.18.

Top of Page