Merge pull request #1 from matejkosik/master

add some more material (preliminary provided in "tuto2" directory)

5 files changed, 381 insertions, 0 deletions

diff --git a/tuto2/Makefile b/tuto2/Makefile
new file mode 100644
index 0000000000..e0e197650d
--- /dev/null
+++ b/tuto2/Makefile
@@ -0,0 +1,14 @@
+ifeq "$(COQBIN)" ""
+  COQBIN=$(dir $(shell which coqtop))/
+endif
+
+%: Makefile.coq
+
+Makefile.coq: _CoqProject
+	$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
+
+tests: all
+	@$(MAKE) -C tests -s clean
+	@$(MAKE) -C tests -s all
+
+-include Makefile.coq
diff --git a/tuto2/_CoqProject b/tuto2/_CoqProject
new file mode 100644
index 0000000000..f38ee8d6a6
--- /dev/null
+++ b/tuto2/_CoqProject
@@ -0,0 +1,6 @@
+-R theories/ Tuto
+-I src
+
+theories/Test.v
+src/demo.ml4
+src/tuto_plugin.mlpack
diff --git a/tuto2/src/demo.ml4 b/tuto2/src/demo.ml4
new file mode 100644
index 0000000000..3d165a6302
--- /dev/null
+++ b/tuto2/src/demo.ml4
@@ -0,0 +1,341 @@
+(* -------------------------------------------------------------------------- *)
+(*                                                                            *)
+(*                            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
diff --git a/tuto2/src/tuto_plugin.mlpack b/tuto2/src/tuto_plugin.mlpack
new file mode 100644
index 0000000000..043a3b4633
--- /dev/null
+++ b/tuto2/src/tuto_plugin.mlpack
@@ -0,0 +1 @@
+Demo
\ No newline at end of file
diff --git a/tuto2/theories/Test.v b/tuto2/theories/Test.v
new file mode 100644
index 0000000000..5522a3444a
--- /dev/null
+++ b/tuto2/theories/Test.v
@@ -0,0 +1,19 @@
+Declare ML Module "demo".
+
+Cmd1.
+Cmd2 With Some Terminal Parameters.
+Cmd3 42.
+Cmd4 100 200 300 400.
+Cmd5 Foo_5.
+Cmd5 Bar_5.
+Cmd6.
+Cmd7.
+Cmd7.
+Cmd7.
+
+Goal True.
+Proof.
+  tactic1.
+  tactic2 Foo_2.
+  tactic2 Bar_2.
+Abort.