From b5c0be9687aad69913e24354a041f188ee25efaf Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Tue, 1 May 2018 21:30:53 +0200
Subject: a first project on how to organize files and define a simple query
---
tuto0/Makefile | 14 ++++++++++++++
tuto0/_CoqProject | 5 +++++
tuto0/src/g_tuto0.ml4 | 5 +++++
tuto0/src/tuto0_plugin.mlpack | 1 +
4 files changed, 25 insertions(+)
create mode 100644 tuto0/Makefile
create mode 100644 tuto0/_CoqProject
create mode 100644 tuto0/src/g_tuto0.ml4
create mode 100644 tuto0/src/tuto0_plugin.mlpack
diff --git a/tuto0/Makefile b/tuto0/Makefile
new file mode 100644
index 0000000000..e0e197650d
--- /dev/null
+++ b/tuto0/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/tuto0/_CoqProject b/tuto0/_CoqProject
new file mode 100644
index 0000000000..2871fcd549
--- /dev/null
+++ b/tuto0/_CoqProject
@@ -0,0 +1,5 @@
+-R theories/ Tuto0
+-I src
+
+src/g_tuto0.ml4
+src/tuto0_plugin.mlpack
\ No newline at end of file
diff --git a/tuto0/src/g_tuto0.ml4 b/tuto0/src/g_tuto0.ml4
new file mode 100644
index 0000000000..5e0fa36e51
--- /dev/null
+++ b/tuto0/src/g_tuto0.ml4
@@ -0,0 +1,5 @@
+open Pp
+
+VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY
+| [ "HelloWorld" ] -> [ Feedback.msg_notice (strbrk "Hello World!") ]
+END
\ No newline at end of file
diff --git a/tuto0/src/tuto0_plugin.mlpack b/tuto0/src/tuto0_plugin.mlpack
new file mode 100644
index 0000000000..9360e6036e
--- /dev/null
+++ b/tuto0/src/tuto0_plugin.mlpack
@@ -0,0 +1 @@
+G_tuto0
\ No newline at end of file
--
cgit v1.2.3
From 7ea3de67a88949c026f9715780f4fc3c5c5875f3 Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Tue, 1 May 2018 21:34:48 +0200
Subject: add a simple explanation in the README file
---
README.md | 7 +++++++
1 file changed, 7 insertions(+)
create mode 100644 README.md
diff --git a/README.md b/README.md
new file mode 100644
index 0000000000..568a56bf37
--- /dev/null
+++ b/README.md
@@ -0,0 +1,7 @@
+How to write plugins in Coq
+===========================
+
+ * tuto0 : package a ml4 file in a plugin, organize a Makefile, _CoqProject
+ Example of syntax to add a new toplevel command
+ Example of function call to print a simple message.
+
--
cgit v1.2.3
From 3df17ed7972dc404cc8519ae9bfd42f75e278e0b Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Tue, 1 May 2018 21:45:22 +0200
Subject: add usage explanations
---
README.md | 7 ++++++-
1 file changed, 6 insertions(+), 1 deletion(-)
diff --git a/README.md b/README.md
index 568a56bf37..d6100c8a75 100644
--- a/README.md
+++ b/README.md
@@ -1,7 +1,12 @@
How to write plugins in Coq
===========================
- * tuto0 : package a ml4 file in a plugin, organize a Makefile, _CoqProject
+ * tuto0 : package a ml4 file in a plugin, organize a `Makefile`, `_CoqProject`
Example of syntax to add a new toplevel command
Example of function call to print a simple message.
+ To use it:
+ `cd tuto0; make`
+ `coqtop -I src`
+
+ Dans la session Coq, taper `Require ML Module "tuto0_plugin". HelloWorld.`
--
cgit v1.2.3
From f893ebe4189bb2ecb085e6e139e13c9dadd4611a Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Wed, 2 May 2018 14:18:39 +0200
Subject: first examples of commands taking arguments
---
tuto1/Makefile | 14 ++++++++++++++
tuto1/_CoqProject | 5 +++++
tuto1/src/g_tuto1.ml4 | 24 ++++++++++++++++++++++++
tuto1/src/tuto1_plugin.mlpack | 1 +
4 files changed, 44 insertions(+)
create mode 100644 tuto1/Makefile
create mode 100644 tuto1/_CoqProject
create mode 100644 tuto1/src/g_tuto1.ml4
create mode 100644 tuto1/src/tuto1_plugin.mlpack
diff --git a/tuto1/Makefile b/tuto1/Makefile
new file mode 100644
index 0000000000..e0e197650d
--- /dev/null
+++ b/tuto1/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/tuto1/_CoqProject b/tuto1/_CoqProject
new file mode 100644
index 0000000000..7a191a961d
--- /dev/null
+++ b/tuto1/_CoqProject
@@ -0,0 +1,5 @@
+-R theories/ Tuto0
+-I src
+
+src/g_tuto1.ml4
+src/tuto1_plugin.mlpack
\ No newline at end of file
diff --git a/tuto1/src/g_tuto1.ml4 b/tuto1/src/g_tuto1.ml4
new file mode 100644
index 0000000000..6ff97ae5cf
--- /dev/null
+++ b/tuto1/src/g_tuto1.ml4
@@ -0,0 +1,24 @@
+open Pp
+(* This one is necessary, to avoid message about missing wit_string *)
+open Stdarg
+
+VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY
+| [ "Hello" string(s)] ->
+ [ Feedback.msg_notice (strbrk "Hello " ++ str s) ]
+END
+
+(* reference is allowed as a syntactic entry, but so are all the entries
+ found the signature of module Prim in file coq/parsing/pcoq.mli *)
+
+VERNAC COMMAND EXTEND HelloAgain CLASSIFIED AS QUERY
+| [ "HelloAgain" reference(r)] ->
+(* The function Libnames.pr_reference was found by searchin all mli files
+ for a function of type reference -> Pp.t *)
+ [ Feedback.msg_notice
+ (strbrk "Hello again " ++ Libnames.pr_reference r)]
+END
+
+VERNAC COMMAND EXTEND TakingConstr CLASSIFIED AS QUERY
+| [ "Cmd1" constr(e) ] ->
+ [ Feedback.msg_notice (strbrk "Cmd1 parsed something") ]
+END
diff --git a/tuto1/src/tuto1_plugin.mlpack b/tuto1/src/tuto1_plugin.mlpack
new file mode 100644
index 0000000000..3b46ea79bf
--- /dev/null
+++ b/tuto1/src/tuto1_plugin.mlpack
@@ -0,0 +1 @@
+G_tuto1
\ No newline at end of file
--
cgit v1.2.3
From 3da6c143c9d9b8d419d5445f2ee906ca2e21648c Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Thu, 3 May 2018 17:21:04 +0200
Subject: This version contains a simple command that defines a new constant
---
.gitignore | 6 +++++
README.md | 23 ++++++++++++-----
tuto1/_CoqProject | 4 ++-
tuto1/src/g_tuto1.ml4 | 58 ++++++++++++++++++++++++++++++++++++++++---
tuto1/src/simple_declare.ml | 21 ++++++++++++++++
tuto1/src/simple_declare.mli | 5 ++++
tuto1/src/tuto1_plugin.mlpack | 1 +
7 files changed, 108 insertions(+), 10 deletions(-)
create mode 100644 .gitignore
create mode 100644 tuto1/src/simple_declare.ml
create mode 100644 tuto1/src/simple_declare.mli
diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000000..73640ea8f7
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,6 @@
+*.ml*.d
+*.cm[ix]*
+Makefile.coq*
+*~
+*.[ao]
+.coqdeps.d
\ No newline at end of file
diff --git a/README.md b/README.md
index d6100c8a75..715019c268 100644
--- a/README.md
+++ b/README.md
@@ -1,12 +1,23 @@
How to write plugins in Coq
===========================
-
- * tuto0 : package a ml4 file in a plugin, organize a `Makefile`, `_CoqProject`
- Example of syntax to add a new toplevel command
- Example of function call to print a simple message.
- To use it:
+ # Working environment : merlin, tuareg (open question)
+ # tuto0 : basics of project organization
+ * package a ml4 file in a plugin, organize a `Makefile`, `_CoqProject`
+ - Example of syntax to add a new toplevel command
+ - Example of function call to print a simple message.
+ - To use it:
`cd tuto0; make`
`coqtop -I src`
- Dans la session Coq, taper `Require ML Module "tuto0_plugin". HelloWorld.`
+ In the Coq section type: `Require ML Module "tuto0_plugin". HelloWorld.`
+
+ # tuto1 : Ocaml to Coq communication
+ * Explore the memory of Coq, modify it
+ - Commands that take arguments: strings, symbols, expressions of the calculus of constructions
+ - Commands that interact with type-checking in Coq
+ - A command that adds a new definition or theorem
+ - A command that uses a name and exploits the existing definitions or theorems
+ - A command that exploits an existing ongoing proof
+ - A commandthat defines a new tactic
+
diff --git a/tuto1/_CoqProject b/tuto1/_CoqProject
index 7a191a961d..3f087e48d7 100644
--- a/tuto1/_CoqProject
+++ b/tuto1/_CoqProject
@@ -1,5 +1,7 @@
--R theories/ Tuto0
+-R theories Tuto1
-I src
+src/simple_declare.mli
+src/simple_declare.ml
src/g_tuto1.ml4
src/tuto1_plugin.mlpack
\ No newline at end of file
diff --git a/tuto1/src/g_tuto1.ml4 b/tuto1/src/g_tuto1.ml4
index 6ff97ae5cf..d00da08b2d 100644
--- a/tuto1/src/g_tuto1.ml4
+++ b/tuto1/src/g_tuto1.ml4
@@ -3,7 +3,7 @@ open Pp
open Stdarg
VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY
-| [ "Hello" string(s)] ->
+| [ "Hello" string(s) ] ->
[ Feedback.msg_notice (strbrk "Hello " ++ str s) ]
END
@@ -12,13 +12,65 @@ END
VERNAC COMMAND EXTEND HelloAgain CLASSIFIED AS QUERY
| [ "HelloAgain" reference(r)] ->
-(* The function Libnames.pr_reference was found by searchin all mli files
+(* The function Libnames.pr_reference was found by searching all mli files
for a function of type reference -> Pp.t *)
[ Feedback.msg_notice
(strbrk "Hello again " ++ Libnames.pr_reference r)]
END
+(* According to parsing/pcoq.mli, e has type constr_expr *)
+(* this type is defined in pretyping/constrexpr.ml *)
+(* Question for the developers: why is the file constrexpr.ml and not
+ constrexpr.mli --> Easier for packing the software in components. *)
VERNAC COMMAND EXTEND TakingConstr CLASSIFIED AS QUERY
| [ "Cmd1" constr(e) ] ->
- [ Feedback.msg_notice (strbrk "Cmd1 parsed something") ]
+ [ let _ = e in Feedback.msg_notice (strbrk "Cmd1 parsed something") ]
+END
+
+(* The next step is to make something of parsed expression.
+ Interesting information in interp/constrintern.mli *)
+
+(* There are several phases of transforming a parsed expression into
+ the final internal data-type (constr). There exists a collection of
+ functions that combine all the phases *)
+
+VERNAC COMMAND EXTEND TakingConstr2 CLASSIFIED AS QUERY
+| [ "Cmd2" constr(e) ] ->
+ [ let _ = Constrintern.interp_constr
+ (Global.env())
+ (* Make sure you don't use Evd.empty here, as this does not
+ check consistency with existing universe constraints. *)
+ (Evd.from_env (Global.env())) e in
+ Feedback.msg_notice (strbrk "Cmd2 parsed something legitimate") ]
+END
+
+(* This is to show what happens when typing in an empty environment
+ with an empty evd.
+ Question for the developers: why does "Cmd3 (fun x : nat => x)."
+ raise an anomaly, not the same error as "Cmd3 (fun x : a => x)." *)
+
+VERNAC COMMAND EXTEND TakingConstr3 CLASSIFIED AS QUERY
+| [ "Cmd3" constr(e) ] ->
+ [ let _ = Constrintern.interp_constr Environ.empty_env
+ Evd.empty e in
+ Feedback.msg_notice
+ (strbrk "Cmd3 accepted something in the empty context")]
+END
+
+(* When adding a definition, we have to be careful that just
+ the operation of constructing a well-typed term may already change
+ the environment, at the level of universe constraints (which
+ are recorded in the evd component). The fonction
+ Constrintern.interp_constr ignores this side-effect, so it should
+ not be used here. *)
+
+(* Looking at the interface file interp/constrintern.ml4, I lost
+ some time because I did not see that the "constr" type appearing
+ there was "EConstr.constr" and not "Constr.constr". *)
+
+VERNAC COMMAND EXTEND Define1 CLASSIFIED AS SIDEFF
+| [ "Cmd4" ident(i) constr(e) ] ->
+ [ let v = Constrintern.interp_constr (Global.env())
+ (Evd.from_env (Global.env())) e in
+ Simple_declare.packed_declare_definition i v ]
END
diff --git a/tuto1/src/simple_declare.ml b/tuto1/src/simple_declare.ml
new file mode 100644
index 0000000000..932c4c9bb3
--- /dev/null
+++ b/tuto1/src/simple_declare.ml
@@ -0,0 +1,21 @@
+let packed_declare_definition ident
+ (value_with_constraints : EConstr.constr Evd.in_evar_universe_context) =
+ begin
+ let evalue, st = value_with_constraints in
+ let evd = Evd.from_ctx st in
+ let value = EConstr.to_constr evd evalue in
+ let evd = Evd.minimize_universes evd in
+ let used = Univops.universes_of_constr (Global.env()) value in
+ let norm_used = Evd.restrict_universe_context evd used in
+ let decl = Univdecls.default_univ_decl in
+ let uctx = Evd.check_univ_decl ~poly:true norm_used decl in
+ let ce = Declare.definition_entry ~univs:uctx value in
+ let _ =
+ Pretyping.check_evars_are_solved (Global.env ()) norm_used Evd.empty in
+ let k = (Decl_kinds.Global,
+ true (* polymorphic *), Decl_kinds.Definition) in
+ let binders = Evd.universe_binders evd in
+ let implicits = [] in
+ let hook = Lemmas.mk_hook (fun _ x -> x) in
+ ignore(DeclareDef.declare_definition ident k ce binders implicits hook)
+ end
\ No newline at end of file
diff --git a/tuto1/src/simple_declare.mli b/tuto1/src/simple_declare.mli
new file mode 100644
index 0000000000..7a28626d88
--- /dev/null
+++ b/tuto1/src/simple_declare.mli
@@ -0,0 +1,5 @@
+open Names
+open EConstr
+
+val packed_declare_definition :
+ Id.t -> constr Evd.in_evar_universe_context -> unit
\ No newline at end of file
diff --git a/tuto1/src/tuto1_plugin.mlpack b/tuto1/src/tuto1_plugin.mlpack
index 3b46ea79bf..17a27da09e 100644
--- a/tuto1/src/tuto1_plugin.mlpack
+++ b/tuto1/src/tuto1_plugin.mlpack
@@ -1 +1,2 @@
+Simple_declare
G_tuto1
\ No newline at end of file
--
cgit v1.2.3
From 93273e29708ff5c24024bde0e4b9955cb94a0dc0 Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Thu, 3 May 2018 22:57:55 +0200
Subject: little cleanup on the defining command, and question in comments
---
tuto1/src/simple_declare.ml | 12 ++++++++----
1 file changed, 8 insertions(+), 4 deletions(-)
diff --git a/tuto1/src/simple_declare.ml b/tuto1/src/simple_declare.ml
index 932c4c9bb3..4740de435f 100644
--- a/tuto1/src/simple_declare.ml
+++ b/tuto1/src/simple_declare.ml
@@ -4,18 +4,22 @@ let packed_declare_definition ident
let evalue, st = value_with_constraints in
let evd = Evd.from_ctx st in
let value = EConstr.to_constr evd evalue in
+(* Question to developers: could the next 3 lines be removed:
+ similar stuff present in comDefinition and elpi, but not in Mtac2 *)
let evd = Evd.minimize_universes evd in
let used = Univops.universes_of_constr (Global.env()) value in
- let norm_used = Evd.restrict_universe_context evd used in
+ let evd = Evd.restrict_universe_context evd used in
let decl = Univdecls.default_univ_decl in
- let uctx = Evd.check_univ_decl ~poly:true norm_used decl in
+ let uctx = Evd.check_univ_decl ~poly:true evd decl in
let ce = Declare.definition_entry ~univs:uctx value in
let _ =
- Pretyping.check_evars_are_solved (Global.env ()) norm_used Evd.empty in
+ Pretyping.check_evars_are_solved (Global.env ()) evd Evd.empty in
let k = (Decl_kinds.Global,
true (* polymorphic *), Decl_kinds.Definition) in
let binders = Evd.universe_binders evd in
let implicits = [] in
let hook = Lemmas.mk_hook (fun _ x -> x) in
ignore(DeclareDef.declare_definition ident k ce binders implicits hook)
- end
\ No newline at end of file
+ end
+
+(* But this definition cannot be undone by Reset ident *)
\ No newline at end of file
--
cgit v1.2.3
From 673f55be2b5139f154bbd84e72550a7c7c58341a Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Fri, 4 May 2018 09:12:06 +0200
Subject: This revision contains a simple Check command.
---
tuto1/_CoqProject | 2 ++
tuto1/src/g_tuto1.ml4 | 11 +++++++++++
tuto1/src/simple_check.ml | 9 +++++++++
tuto1/src/simple_check.mli | 1 +
tuto1/src/tuto1_plugin.mlpack | 1 +
5 files changed, 24 insertions(+)
create mode 100644 tuto1/src/simple_check.ml
create mode 100644 tuto1/src/simple_check.mli
diff --git a/tuto1/_CoqProject b/tuto1/_CoqProject
index 3f087e48d7..554893e739 100644
--- a/tuto1/_CoqProject
+++ b/tuto1/_CoqProject
@@ -1,6 +1,8 @@
-R theories Tuto1
-I src
+src/simple_check.mli
+src/simple_check.ml
src/simple_declare.mli
src/simple_declare.ml
src/g_tuto1.ml4
diff --git a/tuto1/src/g_tuto1.ml4 b/tuto1/src/g_tuto1.ml4
index d00da08b2d..26a27b4c63 100644
--- a/tuto1/src/g_tuto1.ml4
+++ b/tuto1/src/g_tuto1.ml4
@@ -74,3 +74,14 @@ VERNAC COMMAND EXTEND Define1 CLASSIFIED AS SIDEFF
(Evd.from_env (Global.env())) e in
Simple_declare.packed_declare_definition i v ]
END
+
+VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY
+| [ "Cmd5" constr(e) ] ->
+ [ let v = Constrintern.interp_constr (Global.env())
+ (Evd.from_env (Global.env())) e in
+ let (a, ctx) = v in
+ let evd = Evd.from_ctx ctx in
+ Feedback.msg_notice
+ (Termops.print_constr_env (Global.env()) evd
+ (Simple_check.simple_check v)) ]
+END
\ No newline at end of file
diff --git a/tuto1/src/simple_check.ml b/tuto1/src/simple_check.ml
new file mode 100644
index 0000000000..05be6632a0
--- /dev/null
+++ b/tuto1/src/simple_check.ml
@@ -0,0 +1,9 @@
+let simple_check value_with_constraints =
+ begin
+ let evalue, st = value_with_constraints in
+ let evd = Evd.from_ctx st in
+ let j = Termops.on_judgment EConstr.of_constr
+ (Arguments_renaming.rename_typing (Global.env())
+ (EConstr.to_constr evd evalue)) in
+ let {Environ.uj_type=x}=j in x
+ end
\ No newline at end of file
diff --git a/tuto1/src/simple_check.mli b/tuto1/src/simple_check.mli
new file mode 100644
index 0000000000..d745e68f6d
--- /dev/null
+++ b/tuto1/src/simple_check.mli
@@ -0,0 +1 @@
+val simple_check : EConstr.constr Evd.in_evar_universe_context -> EConstr.constr
\ No newline at end of file
diff --git a/tuto1/src/tuto1_plugin.mlpack b/tuto1/src/tuto1_plugin.mlpack
index 17a27da09e..ccb4b6a538 100644
--- a/tuto1/src/tuto1_plugin.mlpack
+++ b/tuto1/src/tuto1_plugin.mlpack
@@ -1,2 +1,3 @@
+Simple_check
Simple_declare
G_tuto1
\ No newline at end of file
--
cgit v1.2.3
From 2053402c665d6d80d78d1ce4a62b7b7b3090e5ca Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Fri, 4 May 2018 13:28:38 +0200
Subject: A modified version that includes code proposed by G. Gilbert
---
tuto1/src/simple_declare.ml | 46 ++++++++++++++++++++++-----------------------
1 file changed, 23 insertions(+), 23 deletions(-)
diff --git a/tuto1/src/simple_declare.ml b/tuto1/src/simple_declare.ml
index 4740de435f..c05907ad4f 100644
--- a/tuto1/src/simple_declare.ml
+++ b/tuto1/src/simple_declare.ml
@@ -1,25 +1,25 @@
-let packed_declare_definition ident
- (value_with_constraints : EConstr.constr Evd.in_evar_universe_context) =
- begin
- let evalue, st = value_with_constraints in
- let evd = Evd.from_ctx st in
- let value = EConstr.to_constr evd evalue in
-(* Question to developers: could the next 3 lines be removed:
- similar stuff present in comDefinition and elpi, but not in Mtac2 *)
- let evd = Evd.minimize_universes evd in
- let used = Univops.universes_of_constr (Global.env()) value in
- let evd = Evd.restrict_universe_context evd used in
- let decl = Univdecls.default_univ_decl in
- let uctx = Evd.check_univ_decl ~poly:true evd decl in
- let ce = Declare.definition_entry ~univs:uctx value in
- let _ =
- Pretyping.check_evars_are_solved (Global.env ()) evd Evd.empty in
- let k = (Decl_kinds.Global,
- true (* polymorphic *), Decl_kinds.Definition) in
- let binders = Evd.universe_binders evd in
- let implicits = [] in
- let hook = Lemmas.mk_hook (fun _ x -> x) in
- ignore(DeclareDef.declare_definition ident k ce binders implicits hook)
- end
+let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook =
+ let open EConstr in
+ let env = Global.env () in
+ let sigma = Evd.minimize_universes sigma in
+ let body = to_constr sigma body in
+ let tyopt = Option.map (to_constr sigma) tyopt in
+ let uvars_fold uvars c =
+ Univ.LSet.union uvars (Univops.universes_of_constr env c) in
+ let uvars = List.fold_left uvars_fold Univ.LSet.empty
+ (Option.List.cons tyopt [body]) in
+ let sigma = Evd.restrict_universe_context sigma uvars in
+ let univs = Evd.check_univ_decl ~poly sigma udecl in
+ let ubinders = Evd.universe_binders sigma in
+ let ce = Declare.definition_entry ?types:tyopt ~univs body in
+ DeclareDef.declare_definition ident k ce ubinders imps hook
+
+let packed_declare_definition ident value_with_constraints =
+ let body, ctx = value_with_constraints in
+ let sigma = Evd.from_ctx ctx in
+ let k = (Decl_kinds.Global, true, Decl_kinds.Definition) in
+ let udecl = Univdecls.default_univ_decl in
+ let nohook = Lemmas.mk_hook (fun _ x -> x) in
+ ignore (edeclare ident k ~opaque:false sigma udecl body None [] nohook)
(* But this definition cannot be undone by Reset ident *)
\ No newline at end of file
--
cgit v1.2.3
From dcdb59e6f51b11f9804ea0a9cd9566303df2c2b9 Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Fri, 4 May 2018 13:31:56 +0200
Subject: follows G. Gilbert's suggestion to have polymorphism following a flag
---
tuto1/src/simple_declare.ml | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/tuto1/src/simple_declare.ml b/tuto1/src/simple_declare.ml
index c05907ad4f..5fd0b2e84b 100644
--- a/tuto1/src/simple_declare.ml
+++ b/tuto1/src/simple_declare.ml
@@ -17,7 +17,8 @@ let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook =
let packed_declare_definition ident value_with_constraints =
let body, ctx = value_with_constraints in
let sigma = Evd.from_ctx ctx in
- let k = (Decl_kinds.Global, true, Decl_kinds.Definition) in
+ let k = (Decl_kinds.Global,
+ Flags.is_universe_polymorphism(), Decl_kinds.Definition) in
let udecl = Univdecls.default_univ_decl in
let nohook = Lemmas.mk_hook (fun _ x -> x) in
ignore (edeclare ident k ~opaque:false sigma udecl body None [] nohook)
--
cgit v1.2.3
From eba06e2192d88af463fb6dec85e2f039a0a13694 Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Fri, 4 May 2018 15:03:49 +0200
Subject: finished type-checking examples
---
tuto1/src/g_tuto1.ml4 | 22 +++++++++++++++++++++-
tuto1/src/simple_check.ml | 27 +++++++++++++++++++++++++--
tuto1/src/simple_check.mli | 9 ++++++++-
3 files changed, 54 insertions(+), 4 deletions(-)
diff --git a/tuto1/src/g_tuto1.ml4 b/tuto1/src/g_tuto1.ml4
index 26a27b4c63..ff07a8f3d0 100644
--- a/tuto1/src/g_tuto1.ml4
+++ b/tuto1/src/g_tuto1.ml4
@@ -77,11 +77,31 @@ END
VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY
| [ "Cmd5" constr(e) ] ->
+ [ let v = Constrintern.interp_constr (Global.env())
+ (Evd.from_env (Global.env())) e in
+ let (_, ctx) = v in
+ let evd = Evd.from_ctx ctx in
+ Feedback.msg_notice
+ (Termops.print_constr_env (Global.env()) evd
+ (Simple_check.simple_check1 v)) ]
+END
+
+VERNAC COMMAND EXTEND Check2 CLASSIFIED AS QUERY
+| [ "Cmd6" constr(e) ] ->
+ [ let v = Constrintern.interp_constr (Global.env())
+ (Evd.from_env (Global.env())) e in
+ let evd, ty = Simple_check.simple_check2 v in
+ Feedback.msg_notice
+ (Termops.print_constr_env (Global.env()) evd ty) ]
+END
+
+VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY
+| [ "Cmd7" constr(e) ] ->
[ let v = Constrintern.interp_constr (Global.env())
(Evd.from_env (Global.env())) e in
let (a, ctx) = v in
let evd = Evd.from_ctx ctx in
Feedback.msg_notice
(Termops.print_constr_env (Global.env()) evd
- (Simple_check.simple_check v)) ]
+ (Simple_check.simple_check3 v)) ]
END
\ No newline at end of file
diff --git a/tuto1/src/simple_check.ml b/tuto1/src/simple_check.ml
index 05be6632a0..e949e08a7c 100644
--- a/tuto1/src/simple_check.ml
+++ b/tuto1/src/simple_check.ml
@@ -1,9 +1,32 @@
-let simple_check value_with_constraints =
+let simple_check1 value_with_constraints =
begin
let evalue, st = value_with_constraints in
let evd = Evd.from_ctx st in
+(* This is reverse engineered from vernacentries.ml *)
+(* The point of renaming is to make sure the bound names printed by Check
+ can be re-used in `apply with` tactics that use bound names to
+ refer to arguments. *)
let j = Termops.on_judgment EConstr.of_constr
(Arguments_renaming.rename_typing (Global.env())
(EConstr.to_constr evd evalue)) in
let {Environ.uj_type=x}=j in x
- end
\ No newline at end of file
+ end
+
+let simple_check2 value_with_constraints =
+ let evalue, st = value_with_constraints in
+ let evd = Evd.from_ctx st in
+(* This version should be preferred if bound variable names are not so
+ important, you want to really verify that the input is well-typed,
+ and if you want to obtain the type. *)
+(* Note that the output value is a pair containing a new evar_map:
+ typing will fill out blanks in the term by add evar bindings. *)
+ Typing.type_of (Global.env()) evd evalue
+
+let simple_check3 value_with_constraints =
+ let evalue, st = value_with_constraints in
+ let evd = Evd.from_ctx st in
+(* This version should be preferred if bound variable names are not so
+ important and you already expect the input to have been type-checked
+ before. Set ~lax to false if you want an anomaly to be raised in
+ case of a type error. Otherwise a ReTypeError exception is raised. *)
+ Retyping.get_type_of ~lax:true (Global.env()) evd evalue
\ No newline at end of file
diff --git a/tuto1/src/simple_check.mli b/tuto1/src/simple_check.mli
index d745e68f6d..7079ca925d 100644
--- a/tuto1/src/simple_check.mli
+++ b/tuto1/src/simple_check.mli
@@ -1 +1,8 @@
-val simple_check : EConstr.constr Evd.in_evar_universe_context -> EConstr.constr
\ No newline at end of file
+val simple_check1 :
+ EConstr.constr Evd.in_evar_universe_context -> EConstr.constr
+
+val simple_check2 :
+ EConstr.constr Evd.in_evar_universe_context -> Evd.evar_map * EConstr.constr
+
+val simple_check3 :
+ EConstr.constr Evd.in_evar_universe_context -> EConstr.constr
\ No newline at end of file
--
cgit v1.2.3
From cb20f241cc7ec686a5ae19c1e7b9eef6b26d230a Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Fri, 4 May 2018 16:04:54 +0200
Subject: adds more packaging boilerplate in tuto0
---
tuto0/_CoqProject | 3 +++
tuto0/src/g_tuto0.ml4 | 4 +++-
tuto0/src/tuto0_main.ml | 1 +
tuto0/src/tuto0_main.mli | 1 +
tuto0/src/tuto0_plugin.mlpack | 1 +
tuto0/theories/Loader.v | 1 +
6 files changed, 10 insertions(+), 1 deletion(-)
create mode 100644 tuto0/src/tuto0_main.ml
create mode 100644 tuto0/src/tuto0_main.mli
create mode 100644 tuto0/theories/Loader.v
diff --git a/tuto0/_CoqProject b/tuto0/_CoqProject
index 2871fcd549..ca0c0588a4 100644
--- a/tuto0/_CoqProject
+++ b/tuto0/_CoqProject
@@ -1,5 +1,8 @@
-R theories/ Tuto0
-I src
+theories/Loader.v
+src/tuto0_main.ml
+src/tuto0_main.mli
src/g_tuto0.ml4
src/tuto0_plugin.mlpack
\ No newline at end of file
diff --git a/tuto0/src/g_tuto0.ml4 b/tuto0/src/g_tuto0.ml4
index 5e0fa36e51..e3656fc986 100644
--- a/tuto0/src/g_tuto0.ml4
+++ b/tuto0/src/g_tuto0.ml4
@@ -1,5 +1,7 @@
+DECLARE PLUGIN "tuto0"
+
open Pp
VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY
-| [ "HelloWorld" ] -> [ Feedback.msg_notice (strbrk "Hello World!") ]
+| [ "HelloWorld" ] -> [ Feedback.msg_notice (strbrk Tuto0_main.message) ]
END
\ No newline at end of file
diff --git a/tuto0/src/tuto0_main.ml b/tuto0/src/tuto0_main.ml
new file mode 100644
index 0000000000..93a807a800
--- /dev/null
+++ b/tuto0/src/tuto0_main.ml
@@ -0,0 +1 @@
+let message = "Hello world!"
diff --git a/tuto0/src/tuto0_main.mli b/tuto0/src/tuto0_main.mli
new file mode 100644
index 0000000000..00d981ad75
--- /dev/null
+++ b/tuto0/src/tuto0_main.mli
@@ -0,0 +1 @@
+val message : string
\ No newline at end of file
diff --git a/tuto0/src/tuto0_plugin.mlpack b/tuto0/src/tuto0_plugin.mlpack
index 9360e6036e..02bc329591 100644
--- a/tuto0/src/tuto0_plugin.mlpack
+++ b/tuto0/src/tuto0_plugin.mlpack
@@ -1 +1,2 @@
+Tuto0_main
G_tuto0
\ No newline at end of file
diff --git a/tuto0/theories/Loader.v b/tuto0/theories/Loader.v
new file mode 100644
index 0000000000..583b77dc3b
--- /dev/null
+++ b/tuto0/theories/Loader.v
@@ -0,0 +1 @@
+Declare ML Module "tuto0_plugin".
\ No newline at end of file
--
cgit v1.2.3
From c3bc6e79494b03543e0c708bfa9e71d2e5d57aee Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Fri, 4 May 2018 17:28:30 +0200
Subject: Now a command to access the value of a constant
---
tuto1/_CoqProject | 4 ++++
tuto1/src/g_tuto1.ml4 | 12 +++++++++++-
tuto1/src/simple_print.ml | 14 ++++++++++++++
tuto1/src/simple_print.mli | 1 +
tuto1/src/tuto1_plugin.mlpack | 1 +
tuto1/theories/Loader.v | 1 +
6 files changed, 32 insertions(+), 1 deletion(-)
create mode 100644 tuto1/src/simple_print.ml
create mode 100644 tuto1/src/simple_print.mli
create mode 100644 tuto1/theories/Loader.v
diff --git a/tuto1/_CoqProject b/tuto1/_CoqProject
index 554893e739..ce14ee2b87 100644
--- a/tuto1/_CoqProject
+++ b/tuto1/_CoqProject
@@ -1,9 +1,13 @@
-R theories Tuto1
-I src
+theories/Loader.v
+
src/simple_check.mli
src/simple_check.ml
src/simple_declare.mli
src/simple_declare.ml
+src/simple_print.ml
+src/simple_print.mli
src/g_tuto1.ml4
src/tuto1_plugin.mlpack
\ No newline at end of file
diff --git a/tuto1/src/g_tuto1.ml4 b/tuto1/src/g_tuto1.ml4
index ff07a8f3d0..22bcfe8adb 100644
--- a/tuto1/src/g_tuto1.ml4
+++ b/tuto1/src/g_tuto1.ml4
@@ -104,4 +104,14 @@ VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY
Feedback.msg_notice
(Termops.print_constr_env (Global.env()) evd
(Simple_check.simple_check3 v)) ]
-END
\ No newline at end of file
+END
+
+VERNAC COMMAND EXTEND ExamplePrint CLASSIFIED AS QUERY
+| [ "Cmd8" reference(r) ] ->
+ [ let env = Global.env() in
+ let evd = Evd.from_env env in
+ Feedback.msg_notice
+ (Termops.print_constr_env env evd
+ (EConstr.of_constr
+ (Simple_print.simple_body_access (Nametab.global r)))) ]
+END
diff --git a/tuto1/src/simple_print.ml b/tuto1/src/simple_print.ml
new file mode 100644
index 0000000000..5c4910d98e
--- /dev/null
+++ b/tuto1/src/simple_print.ml
@@ -0,0 +1,14 @@
+let simple_body_access gref =
+ match gref with
+ | Globnames.VarRef _ ->
+ failwith "variables are not covered in this example"
+ | Globnames.IndRef _ ->
+ failwith "inductive types are not covered in this example"
+ | Globnames.ConstructRef _ ->
+ failwith "constructors are not covered in this example"
+ | Globnames.ConstRef cst ->
+ let cb = Environ.lookup_constant cst (Global.env()) in
+ match Global.body_of_constant_body cb with
+ | Some(e, _) -> e
+ | None -> failwith "This term has no value"
+
diff --git a/tuto1/src/simple_print.mli b/tuto1/src/simple_print.mli
new file mode 100644
index 0000000000..c59316e84b
--- /dev/null
+++ b/tuto1/src/simple_print.mli
@@ -0,0 +1 @@
+val simple_body_access : Globnames.global_reference -> Constr.constr
diff --git a/tuto1/src/tuto1_plugin.mlpack b/tuto1/src/tuto1_plugin.mlpack
index ccb4b6a538..39db9e487d 100644
--- a/tuto1/src/tuto1_plugin.mlpack
+++ b/tuto1/src/tuto1_plugin.mlpack
@@ -1,3 +1,4 @@
Simple_check
Simple_declare
+Simple_print
G_tuto1
\ No newline at end of file
diff --git a/tuto1/theories/Loader.v b/tuto1/theories/Loader.v
new file mode 100644
index 0000000000..3bff2e48d7
--- /dev/null
+++ b/tuto1/theories/Loader.v
@@ -0,0 +1 @@
+Declare ML Module "tuto1_plugin".
\ No newline at end of file
--
cgit v1.2.3
From 3365fb1c5fa3d37f23775e7fb3ee4a2a341bb2ef Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Fri, 4 May 2018 17:30:44 +0200
Subject: .gitignore fine-tuning
---
.gitignore | 5 ++++-
1 file changed, 4 insertions(+), 1 deletion(-)
diff --git a/.gitignore b/.gitignore
index 73640ea8f7..be4ea26f86 100644
--- a/.gitignore
+++ b/.gitignore
@@ -3,4 +3,7 @@
Makefile.coq*
*~
*.[ao]
-.coqdeps.d
\ No newline at end of file
+.coqdeps.d
+*.vo
+*.glob
+*.aux
--
cgit v1.2.3
From 6e9ee6b1cd9290951fe1f53bbb28f313aca45712 Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Fri, 4 May 2018 17:35:17 +0200
Subject: adds a comment in simple_print.ml and a plugin declaration in
g_tuto1.ml4
---
tuto1/src/g_tuto1.ml4 | 2 ++
tuto1/src/simple_print.ml | 3 +++
2 files changed, 5 insertions(+)
diff --git a/tuto1/src/g_tuto1.ml4 b/tuto1/src/g_tuto1.ml4
index 22bcfe8adb..b12ae3a073 100644
--- a/tuto1/src/g_tuto1.ml4
+++ b/tuto1/src/g_tuto1.ml4
@@ -1,3 +1,5 @@
+DECLARE PLUGIN "tuto1_plugin"
+
open Pp
(* This one is necessary, to avoid message about missing wit_string *)
open Stdarg
diff --git a/tuto1/src/simple_print.ml b/tuto1/src/simple_print.ml
index 5c4910d98e..cfc38ff9c9 100644
--- a/tuto1/src/simple_print.ml
+++ b/tuto1/src/simple_print.ml
@@ -1,3 +1,6 @@
+(* A more advanced example of how to explore the structure of terms of
+ type constr is given in the coq-dpdgraph plugin. *)
+
let simple_body_access gref =
match gref with
| Globnames.VarRef _ ->
--
cgit v1.2.3
From 61bf9d47bbcfde7123f800311c6cb6817e37ff38 Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Fri, 4 May 2018 17:43:28 +0200
Subject: remove errors in the documentation
---
README.md | 7 ++++---
1 file changed, 4 insertions(+), 3 deletions(-)
diff --git a/README.md b/README.md
index 715019c268..86eeef5fd2 100644
--- a/README.md
+++ b/README.md
@@ -8,16 +8,17 @@ How to write plugins in Coq
- To use it:
`cd tuto0; make`
- `coqtop -I src`
+ `coqtop -I src -R theories Tuto0`
- In the Coq section type: `Require ML Module "tuto0_plugin". HelloWorld.`
+ In the Coq session type: `Require Tuto0.Loader. HelloWorld.`
# tuto1 : Ocaml to Coq communication
* Explore the memory of Coq, modify it
- Commands that take arguments: strings, symbols, expressions of the calculus of constructions
- Commands that interact with type-checking in Coq
- A command that adds a new definition or theorem
- - A command that uses a name and exploits the existing definitions or theorems
+ - A command that uses a name and exploits the existing definitions
+ or theorems
- A command that exploits an existing ongoing proof
- A commandthat defines a new tactic
--
cgit v1.2.3
From a4afe13c9d1498953584607940918a8f450488d6 Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Fri, 4 May 2018 17:43:28 +0200
Subject: remove errors in the documentation
---
README.md | 7 ++++---
1 file changed, 4 insertions(+), 3 deletions(-)
diff --git a/README.md b/README.md
index 715019c268..86eeef5fd2 100644
--- a/README.md
+++ b/README.md
@@ -8,16 +8,17 @@ How to write plugins in Coq
- To use it:
`cd tuto0; make`
- `coqtop -I src`
+ `coqtop -I src -R theories Tuto0`
- In the Coq section type: `Require ML Module "tuto0_plugin". HelloWorld.`
+ In the Coq session type: `Require Tuto0.Loader. HelloWorld.`
# tuto1 : Ocaml to Coq communication
* Explore the memory of Coq, modify it
- Commands that take arguments: strings, symbols, expressions of the calculus of constructions
- Commands that interact with type-checking in Coq
- A command that adds a new definition or theorem
- - A command that uses a name and exploits the existing definitions or theorems
+ - A command that uses a name and exploits the existing definitions
+ or theorems
- A command that exploits an existing ongoing proof
- A commandthat defines a new tactic
--
cgit v1.2.3
From dd660f27e2ff7247a52c1f80a7fc1b6cc286bae5 Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Fri, 4 May 2018 17:45:59 +0200
Subject: remove a typo
---
README.md | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/README.md b/README.md
index 86eeef5fd2..a1ca482a5f 100644
--- a/README.md
+++ b/README.md
@@ -20,5 +20,5 @@ How to write plugins in Coq
- A command that uses a name and exploits the existing definitions
or theorems
- A command that exploits an existing ongoing proof
- - A commandthat defines a new tactic
+ - A command that defines a new tactic
--
cgit v1.2.3
From c2658eb76dbd4e616bfb449566fa6645f63777ed Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Fri, 4 May 2018 17:46:28 +0200
Subject: adds an explanation to Cmd8
---
tuto1/src/g_tuto1.ml4 | 5 +++++
1 file changed, 5 insertions(+)
diff --git a/tuto1/src/g_tuto1.ml4 b/tuto1/src/g_tuto1.ml4
index b12ae3a073..e71c880d01 100644
--- a/tuto1/src/g_tuto1.ml4
+++ b/tuto1/src/g_tuto1.ml4
@@ -108,6 +108,11 @@ VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY
(Simple_check.simple_check3 v)) ]
END
+(* This command takes a name and return its value. It does less
+ than Print, because it fails on constructors, axioms, and inductive types.
+ This should be improved, because the error message is an anomaly.
+ Anomalies should never appear even when using a command outside of its
+ intended use. *)
VERNAC COMMAND EXTEND ExamplePrint CLASSIFIED AS QUERY
| [ "Cmd8" reference(r) ] ->
[ let env = Global.env() in
--
cgit v1.2.3
From d663a1b5c2bc10fa125ae485ce53d2ec5bc691a6 Mon Sep 17 00:00:00 2001
From: Matej Košík
Date: Mon, 7 May 2018 10:38:24 +0200
Subject: add some more material (preliminary provided in "tuto2" directory)
As it is, it probably need to be edited:
(it may be a good idea to drop redundant part;
it may be a good idea to make the style of the new information
consistent with the already existing material;
...)
---
tuto2/Makefile | 14 ++
tuto2/_CoqProject | 6 +
tuto2/src/demo.ml4 | 356 +++++++++++++++++++++++++++++++++++++++++++
tuto2/src/tuto_plugin.mlpack | 1 +
tuto2/theories/Test.v | 19 +++
5 files changed, 396 insertions(+)
create mode 100644 tuto2/Makefile
create mode 100644 tuto2/_CoqProject
create mode 100644 tuto2/src/demo.ml4
create mode 100644 tuto2/src/tuto_plugin.mlpack
create mode 100644 tuto2/theories/Test.v
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..ca139558ed
--- /dev/null
+++ b/tuto2/_CoqProject
@@ -0,0 +1,6 @@
+-R theories/ Tuto
+-I src
+
+theories/Test.v
+src/demo.ml4
+src/tuto_plugin.mlpack
\ No newline at end of file
diff --git a/tuto2/src/demo.ml4 b/tuto2/src/demo.ml4
new file mode 100644
index 0000000000..cf6a367867
--- /dev/null
+++ b/tuto2/src/demo.ml4
@@ -0,0 +1,356 @@
+(* This will be compilable once the following pull-requests:
+ - https://github.com/coq/coq/pull/759
+ - https://github.com/coq/coq/pull/761
+ will be merged.
+
+ TODO: update the part related to "Cmd6" once I get an answer to this question:
+ https://sympa.inria.fr/sympa/arc/coqdev/2017-06/msg00037.html
+
+ TODO: figure out why does Summary.Local.ref function requre 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
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.
--
cgit v1.2.3
From a7bf1793f1e570097a745060f04bc9ad8fb1d752 Mon Sep 17 00:00:00 2001
From: Matej Košík
Date: Mon, 7 May 2018 11:09:48 +0200
Subject: fix some details
---
tuto2/_CoqProject | 2 +-
tuto2/src/demo.ml4 | 6 +-----
2 files changed, 2 insertions(+), 6 deletions(-)
diff --git a/tuto2/_CoqProject b/tuto2/_CoqProject
index ca139558ed..f38ee8d6a6 100644
--- a/tuto2/_CoqProject
+++ b/tuto2/_CoqProject
@@ -3,4 +3,4 @@
theories/Test.v
src/demo.ml4
-src/tuto_plugin.mlpack
\ No newline at end of file
+src/tuto_plugin.mlpack
diff --git a/tuto2/src/demo.ml4 b/tuto2/src/demo.ml4
index cf6a367867..082e5cfa97 100644
--- a/tuto2/src/demo.ml4
+++ b/tuto2/src/demo.ml4
@@ -6,11 +6,7 @@
TODO: update the part related to "Cmd6" once I get an answer to this question:
https://sympa.inria.fr/sympa/arc/coqdev/2017-06/msg00037.html
- TODO: figure out why does Summary.Local.ref function requre 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?
+ TODO: figure out why does Summary.Local.ref function requires argument "name" ?
*)
(* -------------------------------------------------------------------------- *)
--
cgit v1.2.3
From 42bd3548b84283259eae452c7bce56dfa02fb3c4 Mon Sep 17 00:00:00 2001
From: Matej Košík
Date: Mon, 7 May 2018 13:11:34 +0200
Subject: fix some details
---
tuto2/src/demo.ml4 | 11 -----------
1 file changed, 11 deletions(-)
diff --git a/tuto2/src/demo.ml4 b/tuto2/src/demo.ml4
index 082e5cfa97..3d165a6302 100644
--- a/tuto2/src/demo.ml4
+++ b/tuto2/src/demo.ml4
@@ -1,14 +1,3 @@
-(* This will be compilable once the following pull-requests:
- - https://github.com/coq/coq/pull/759
- - https://github.com/coq/coq/pull/761
- will be merged.
-
- TODO: update the part related to "Cmd6" once I get an answer to this question:
- https://sympa.inria.fr/sympa/arc/coqdev/2017-06/msg00037.html
-
- TODO: figure out why does Summary.Local.ref function requires argument "name" ?
-*)
-
(* -------------------------------------------------------------------------- *)
(* *)
(* Initial ritual dance *)
--
cgit v1.2.3
From bcca8dbc865747a62541c602f28ac8d99f84504d Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Mon, 7 May 2018 21:03:41 +0200
Subject: adds a copy of the show_proof command
---
tuto1/src/g_tuto1.ml4 | 24 ++++++++++++++++++++++++
1 file changed, 24 insertions(+)
diff --git a/tuto1/src/g_tuto1.ml4 b/tuto1/src/g_tuto1.ml4
index e71c880d01..da14d03842 100644
--- a/tuto1/src/g_tuto1.ml4
+++ b/tuto1/src/g_tuto1.ml4
@@ -1,5 +1,11 @@
DECLARE PLUGIN "tuto1_plugin"
+(* If we forget this line and include our own tactic definition using
+ TACTIC EXTEND, as below, then we get the strage error message
+ no implementation available for Tacentries, only when compiling
+ theories/Loader.v
+*)
+open Ltac_plugin
open Pp
(* This one is necessary, to avoid message about missing wit_string *)
open Stdarg
@@ -122,3 +128,21 @@ VERNAC COMMAND EXTEND ExamplePrint CLASSIFIED AS QUERY
(EConstr.of_constr
(Simple_print.simple_body_access (Nametab.global r)))) ]
END
+
+TACTIC EXTEND my_intro
+| [ "my_intro" ident(i) ] ->
+ [ Tactics.introduction ~check:false i]
+END
+
+(* if one write this:
+ VERNAC COMMAND EXTEND exploreproof CLASSIFIED AS QUERY
+ it gives an error message that is basically impossible to understand. *)
+
+VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY
+| [ "Cmd9" ] ->
+ [ let p = Proof_global.give_me_the_proof () in
+ let sigma, env = Pfedit.get_current_context () in
+ let pprf = Proof.partial_proof p in
+ Feedback.msg_notice
+ (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf) ]
+END
--
cgit v1.2.3
From 281fc90700926bd7eb80727bb9e752472d276ba2 Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Tue, 8 May 2018 08:47:58 +0200
Subject: attempt to make code inclusions appear correctly
---
README.md | 24 ++++++++++++++++++++----
1 file changed, 20 insertions(+), 4 deletions(-)
diff --git a/README.md b/README.md
index a1ca482a5f..636fe265e0 100644
--- a/README.md
+++ b/README.md
@@ -2,18 +2,20 @@ How to write plugins in Coq
===========================
# Working environment : merlin, tuareg (open question)
# tuto0 : basics of project organization
- * package a ml4 file in a plugin, organize a `Makefile`, `_CoqProject`
+ package a ml4 file in a plugin, organize a `Makefile`, `_CoqProject`
- Example of syntax to add a new toplevel command
- Example of function call to print a simple message.
- To use it:
- `cd tuto0; make`
- `coqtop -I src -R theories Tuto0`
+
+ cd tuto0; make
+ coqtop -I src -R theories Tuto0
+
In the Coq session type: `Require Tuto0.Loader. HelloWorld.`
# tuto1 : Ocaml to Coq communication
- * Explore the memory of Coq, modify it
+ Explore the memory of Coq, modify it
- Commands that take arguments: strings, symbols, expressions of the calculus of constructions
- Commands that interact with type-checking in Coq
- A command that adds a new definition or theorem
@@ -22,3 +24,17 @@ How to write plugins in Coq
- A command that exploits an existing ongoing proof
- A command that defines a new tactic
+ # tuto2 : Ocaml to Coq communication
+ A more step by step introduction to writing commands
+ - Explanation of the syntax of entries
+ - Adding a new type to and parsing to the available choices
+ - Handling commands that store information in user-chosen registers and tables
+
+
+ # tuto3 : manipulating terms of the calculus of constructions
+ obtaining existing values from memory and composing them, making sure
+ they are well-typed, and using them in new definitions and proofs.
+ -
+
+
+
\ No newline at end of file
--
cgit v1.2.3
From 95f9fe8090c2a1fc0bbcb9b8ec3b9a4a7c2f45ee Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Tue, 8 May 2018 08:52:45 +0200
Subject: try with triple backticks
---
README.md | 9 ++++++---
1 file changed, 6 insertions(+), 3 deletions(-)
diff --git a/README.md b/README.md
index 636fe265e0..5e4e566fce 100644
--- a/README.md
+++ b/README.md
@@ -7,12 +7,15 @@ How to write plugins in Coq
- Example of function call to print a simple message.
- To use it:
-
+```bash
cd tuto0; make
coqtop -I src -R theories Tuto0
-
+```
- In the Coq session type: `Require Tuto0.Loader. HelloWorld.`
+ In the Coq session type:
+```coq
+ Require Tuto0.Loader. HelloWorld.
+```
# tuto1 : Ocaml to Coq communication
Explore the memory of Coq, modify it
--
cgit v1.2.3
From f5b772c0b299442ff730a3ee3064897ea62c1cec Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Tue, 8 May 2018 08:58:07 +0200
Subject: problems with bullet lists
---
README.md | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/README.md b/README.md
index 5e4e566fce..94a0b9da34 100644
--- a/README.md
+++ b/README.md
@@ -3,9 +3,9 @@ How to write plugins in Coq
# Working environment : merlin, tuareg (open question)
# tuto0 : basics of project organization
package a ml4 file in a plugin, organize a `Makefile`, `_CoqProject`
- - Example of syntax to add a new toplevel command
- - Example of function call to print a simple message.
- - To use it:
+ - Example of syntax to add a new toplevel command
+ - Example of function call to print a simple message.
+ - To use it:
```bash
cd tuto0; make
--
cgit v1.2.3
From 1b420e583d731e8d22ceb44dd0bdc7bd6d7fd10a Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Tue, 8 May 2018 09:10:49 +0200
Subject: corrects a problem in documenting how to run the demo
---
README.md | 39 ++++++++++++++++++++++++---------------
1 file changed, 24 insertions(+), 15 deletions(-)
diff --git a/README.md b/README.md
index 94a0b9da34..406bb1083c 100644
--- a/README.md
+++ b/README.md
@@ -14,30 +14,39 @@ How to write plugins in Coq
In the Coq session type:
```coq
- Require Tuto0.Loader. HelloWorld.
+ Require Import Tuto0.Loader. HelloWorld.
```
# tuto1 : Ocaml to Coq communication
Explore the memory of Coq, modify it
- - Commands that take arguments: strings, symbols, expressions of the calculus of constructions
- - Commands that interact with type-checking in Coq
- - A command that adds a new definition or theorem
- - A command that uses a name and exploits the existing definitions
- or theorems
- - A command that exploits an existing ongoing proof
- - A command that defines a new tactic
+ - Commands that take arguments: strings, symbols, expressions of the calculus of constructions
+ - Commands that interact with type-checking in Coq
+ - A command that adds a new definition or theorem
+ - A command that uses a name and exploits the existing definitions
+ or theorems
+ - A command that exploits an existing ongoing proof
+ - A command that defines a new tactic
+ Compilation and loading must be performed as for `tuto0`.
+
# tuto2 : Ocaml to Coq communication
A more step by step introduction to writing commands
- - Explanation of the syntax of entries
- - Adding a new type to and parsing to the available choices
- - Handling commands that store information in user-chosen registers and tables
+ - Explanation of the syntax of entries
+ - Adding a new type to and parsing to the available choices
+ - Handling commands that store information in user-chosen registers and tables
+ Compilation and loading must be performed as for `tuto1`.
# tuto3 : manipulating terms of the calculus of constructions
- obtaining existing values from memory and composing them, making sure
- they are well-typed, and using them in new definitions and proofs.
- -
-
+ Manipulating terms, inside commands and tactics.
+ - Obtaining existing values from memory
+ - Composing values
+ - Verifying types
+ - Leveraging type inference
+ - Leveraging coercion
+ - Using these terms in commands
+ - Using these terms in tactics
+
+ compilation and loading must be performed as for `tuto0`.
\ No newline at end of file
--
cgit v1.2.3
From 9bd7f64e1a1d3d2b055a7df23d31f0ed76f28649 Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Tue, 8 May 2018 12:24:30 +0200
Subject: intermediary stage with an EConstr containing a hand-made evar, fauty
---
tuto3/_CoqProject | 7 +++++++
tuto3/src/g_tuto3.ml4 | 37 +++++++++++++++++++++++++++++++++++++
tuto3/src/tuto3_plugin.mlpack | 1 +
tuto3/theories/Loader.v | 1 +
4 files changed, 46 insertions(+)
create mode 100644 tuto3/_CoqProject
create mode 100644 tuto3/src/g_tuto3.ml4
create mode 100644 tuto3/src/tuto3_plugin.mlpack
create mode 100644 tuto3/theories/Loader.v
diff --git a/tuto3/_CoqProject b/tuto3/_CoqProject
new file mode 100644
index 0000000000..22d357542a
--- /dev/null
+++ b/tuto3/_CoqProject
@@ -0,0 +1,7 @@
+-R theories Tuto3
+-I src
+
+theories/Loader.v
+
+src/g_tuto3.ml4
+src/tuto3_plugin.mlpack
\ No newline at end of file
diff --git a/tuto3/src/g_tuto3.ml4 b/tuto3/src/g_tuto3.ml4
new file mode 100644
index 0000000000..fbd93e593c
--- /dev/null
+++ b/tuto3/src/g_tuto3.ml4
@@ -0,0 +1,37 @@
+DECLARE PLUGIN "tuto3_plugin"
+
+open Ltac_plugin
+open Pp
+(* This one is necessary, to avoid message about missing wit_string *)
+open Stdarg
+
+VERNAC COMMAND EXTEND ShowOneConstruction CLASSIFIED AS QUERY
+| [ "Tuto3_1" ] ->
+ [ let gr_S =
+ Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "S" in
+ (* the long name of "S" was found with the command "About S." *)
+ let gr_O =
+ Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in
+ let c_S = EConstr.of_constr (Universes.constr_of_global gr_S) in
+ let c_O = EConstr.of_constr (Universes.constr_of_global gr_O) in
+ let c_v = EConstr.mkApp (c_S, [| c_O |]) in
+ let env = Global.env () in
+ let evd = Evd.from_env env in
+ let evd, s = Evd.new_sort_variable Evd.univ_rigid evd in
+ let new_type_2 = Constr.mkSort s in
+ let evd, bare_evar = Evd.new_evar evd
+ (Evd.make_evar (Environ.named_context_val env) new_type_2) in
+ let arg_type = EConstr.mkEvar (bare_evar, [| |]) in
+ let c_f =
+ EConstr.mkLambda(Names.Name (Names.Id.of_string "x"), arg_type,
+ EConstr.mkRel 1) in
+ let c_1 = EConstr.mkApp (c_f, [| c_v |]) in
+ (* type verification happens here. In this case, we don't care about
+ the type, but usually, typing will update existential variables and
+ universes, all this being stored in the new "evar_map" object *)
+ let evd, _ =
+ Typing.type_of (Global.env()) (Evd.from_env (Global.env())) c_1 in
+ ()
+(* Feedback.msg_notice
+ (Termops.print_constr_env (Global.env()) evd c_1) *) ]
+END
diff --git a/tuto3/src/tuto3_plugin.mlpack b/tuto3/src/tuto3_plugin.mlpack
new file mode 100644
index 0000000000..7aa7cdb9ee
--- /dev/null
+++ b/tuto3/src/tuto3_plugin.mlpack
@@ -0,0 +1 @@
+G_tuto3
\ No newline at end of file
diff --git a/tuto3/theories/Loader.v b/tuto3/theories/Loader.v
new file mode 100644
index 0000000000..cff239af41
--- /dev/null
+++ b/tuto3/theories/Loader.v
@@ -0,0 +1 @@
+Declare ML Module "tuto3_plugin".
\ No newline at end of file
--
cgit v1.2.3
From f30878bfd1e602fd793beb70b5b1fff8f0cc826e Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Wed, 9 May 2018 11:00:42 +0200
Subject: makefile is necessary
---
tuto3/Makefile | 14 ++++++++++++++
1 file changed, 14 insertions(+)
create mode 100644 tuto3/Makefile
diff --git a/tuto3/Makefile b/tuto3/Makefile
new file mode 100644
index 0000000000..e0e197650d
--- /dev/null
+++ b/tuto3/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
--
cgit v1.2.3
From c057f59599872b9ef98d5e2f4ffa9a7e5095916c Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Wed, 9 May 2018 11:01:35 +0200
Subject: typo
---
README.md | 2 --
1 file changed, 2 deletions(-)
diff --git a/README.md b/README.md
index 406bb1083c..00ff146e46 100644
--- a/README.md
+++ b/README.md
@@ -48,5 +48,3 @@ How to write plugins in Coq
- Using these terms in tactics
compilation and loading must be performed as for `tuto0`.
-
-
\ No newline at end of file
--
cgit v1.2.3
From 499d48cba16ce5f42eff82e99cf8e0e08c796f8b Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Wed, 9 May 2018 11:10:23 +0200
Subject: typo
---
tuto1/src/g_tuto1.ml4 | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/tuto1/src/g_tuto1.ml4 b/tuto1/src/g_tuto1.ml4
index da14d03842..78deabed94 100644
--- a/tuto1/src/g_tuto1.ml4
+++ b/tuto1/src/g_tuto1.ml4
@@ -1,7 +1,7 @@
DECLARE PLUGIN "tuto1_plugin"
(* If we forget this line and include our own tactic definition using
- TACTIC EXTEND, as below, then we get the strage error message
+ TACTIC EXTEND, as below, then we get the strange error message
no implementation available for Tacentries, only when compiling
theories/Loader.v
*)
--
cgit v1.2.3
From 6f0cfb0e6176fa16eb7ee9a374fedab62d56d486 Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Wed, 9 May 2018 11:10:51 +0200
Subject: decompose construction of typed term containing evars
---
tuto3/src/g_tuto3.ml4 | 40 ++++++++++++++++++++++++----------------
1 file changed, 24 insertions(+), 16 deletions(-)
diff --git a/tuto3/src/g_tuto3.ml4 b/tuto3/src/g_tuto3.ml4
index fbd93e593c..aaeabcf34f 100644
--- a/tuto3/src/g_tuto3.ml4
+++ b/tuto3/src/g_tuto3.ml4
@@ -5,33 +5,41 @@ open Pp
(* This one is necessary, to avoid message about missing wit_string *)
open Stdarg
-VERNAC COMMAND EXTEND ShowOneConstruction CLASSIFIED AS QUERY
+VERNAC COMMAND EXTEND ShowTypeConstruction CLASSIFIED AS QUERY
| [ "Tuto3_1" ] ->
+ [ let env = Global.env () in
+ let evd = Evd.from_env env in
+ let evd, s = Evd.new_sort_variable Evd.univ_rigid evd in
+ let new_type_2 = EConstr.mkSort s in
+ let evd, _ =
+ Typing.type_of (Global.env()) (Evd.from_env (Global.env())) new_type_2 in
+ Feedback.msg_notice
+ (Termops.print_constr_env env evd new_type_2) ]
+END
+
+VERNAC COMMAND EXTEND ShowOneConstruction CLASSIFIED AS QUERY
+| [ "Tuto3_2" ] ->
[ let gr_S =
Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "S" in
(* the long name of "S" was found with the command "About S." *)
let gr_O =
Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in
- let c_S = EConstr.of_constr (Universes.constr_of_global gr_S) in
let c_O = EConstr.of_constr (Universes.constr_of_global gr_O) in
- let c_v = EConstr.mkApp (c_S, [| c_O |]) in
let env = Global.env () in
let evd = Evd.from_env env in
let evd, s = Evd.new_sort_variable Evd.univ_rigid evd in
- let new_type_2 = Constr.mkSort s in
- let evd, bare_evar = Evd.new_evar evd
- (Evd.make_evar (Environ.named_context_val env) new_type_2) in
- let arg_type = EConstr.mkEvar (bare_evar, [| |]) in
+ let new_type_2 = EConstr.mkSort s in
+ let evd, arg_type = Evarutil.new_evar env evd new_type_2 in
let c_f =
EConstr.mkLambda(Names.Name (Names.Id.of_string "x"), arg_type,
EConstr.mkRel 1) in
- let c_1 = EConstr.mkApp (c_f, [| c_v |]) in
- (* type verification happens here. In this case, we don't care about
- the type, but usually, typing will update existential variables and
- universes, all this being stored in the new "evar_map" object *)
- let evd, _ =
- Typing.type_of (Global.env()) (Evd.from_env (Global.env())) c_1 in
- ()
-(* Feedback.msg_notice
- (Termops.print_constr_env (Global.env()) evd c_1) *) ]
+ let c_1 = EConstr.mkApp (c_f, [| c_O |]) in
+ (* type verification happens here. Type verification will update
+ existential variable information in the evd part. *)
+ let evd, the_type =
+ Typing.type_of (Global.env()) evd c_1 in
+ Feedback.msg_notice
+ ((Termops.print_constr_env env evd c_1) ++
+ str " has type " ++
+ (Termops.print_constr_env env evd the_type)) ]
END
--
cgit v1.2.3
From 007b88166833bb4c8de494306ff62de396510091 Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Wed, 9 May 2018 13:06:56 +0200
Subject: repackage with an extra ml file, add a usage of new_type_evar
---
tuto3/_CoqProject | 2 ++
tuto3/src/construction_game.ml | 65 +++++++++++++++++++++++++++++++++++++++++
tuto3/src/construction_game.mli | 1 +
tuto3/src/g_tuto3.ml4 | 29 ++++--------------
tuto3/src/tuto3_plugin.mlpack | 1 +
5 files changed, 74 insertions(+), 24 deletions(-)
create mode 100644 tuto3/src/construction_game.ml
create mode 100644 tuto3/src/construction_game.mli
diff --git a/tuto3/_CoqProject b/tuto3/_CoqProject
index 22d357542a..5f1bd0450c 100644
--- a/tuto3/_CoqProject
+++ b/tuto3/_CoqProject
@@ -3,5 +3,7 @@
theories/Loader.v
+src/construction_game.ml
+src/construction_game.mli
src/g_tuto3.ml4
src/tuto3_plugin.mlpack
\ No newline at end of file
diff --git a/tuto3/src/construction_game.ml b/tuto3/src/construction_game.ml
new file mode 100644
index 0000000000..df3bfd5d21
--- /dev/null
+++ b/tuto3/src/construction_game.ml
@@ -0,0 +1,65 @@
+open Pp
+
+let example_sort evd =
+(* creating a new sort requires that universes should be recorded
+ in the evd datastructure, so this datastructure also needs to be
+ passed around. *)
+ let evd, s = Evd.new_sort_variable Evd.univ_rigid evd in
+ let new_type = EConstr.mkSort s in
+ evd, new_type
+
+let c_one () =
+(* What happens in constructing a new natural number from the datatype
+ constructors does not require any handling of existential variables
+ or universes, so evd datastructures don't appear here. *)
+ let gr_S =
+ Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "S" in
+(* the long name of "S" was found with the command "About S." *)
+ let gr_O =
+ Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in
+ let c_O = EConstr.of_constr (Universes.constr_of_global gr_O) in
+ let c_S = EConstr.of_constr (Universes.constr_of_global gr_S) in
+(* Here is the construction of a new term by applying functions to argument. *)
+ EConstr.mkApp (c_S, [| c_O |])
+
+let dangling_identity env evd =
+(* I call this a dangling identity, because it is not polymorph, but
+ the type on which it applies is left unspecified, as it is
+ represented by an existential variable. The declaration for this
+ existential variable needs to be added in the evd datastructure. *)
+ let evd, type_type = example_sort evd in
+ let evd, arg_type = Evarutil.new_evar env evd type_type in
+(* Notice the use of a De Bruijn index for the inner occurrence of the
+ bound variable. *)
+ evd, EConstr.mkLambda(Names.Name (Names.Id.of_string "x"), arg_type,
+ EConstr.mkRel 1)
+
+let dangling_identity2 env evd =
+(* This example uses directly a function that produces an evar that
+ is meant to be a type. *)
+ let evd, (arg_type, type_type) =
+ Evarutil.new_type_evar env evd Evd.univ_rigid in
+ evd, EConstr.mkLambda(Names.Name (Names.Id.of_string "x"), arg_type,
+ EConstr.mkRel 1)
+
+let example_sort_app_lambda () =
+(* Next, I wish to construct a lambda-abstraction without giving precisely
+ the type for the abstracted variable. *)
+ let env = Global.env () in
+ let evd = Evd.from_env env in
+ let c_v = c_one () in
+ let evd, c_f = dangling_identity env evd in
+ let c_1 = EConstr.mkApp (c_f, [| c_v |]) in
+ let _ = Feedback.msg_notice
+ (Termops.print_constr_env env evd c_1) in
+ (* type verification happens here. Type verification will update
+ existential variable information in the evd part. *)
+ let evd, the_type =
+ Typing.type_of (Global.env()) evd c_1 in
+(* At display time, you will notice that the system knows about the
+ existential variable being instantiated to the "nat" type, even
+ though c_1 still contains the meta-variable. *)
+ Feedback.msg_notice
+ ((Termops.print_constr_env env evd c_1) ++
+ str " has type " ++
+ (Termops.print_constr_env env evd the_type))
\ No newline at end of file
diff --git a/tuto3/src/construction_game.mli b/tuto3/src/construction_game.mli
new file mode 100644
index 0000000000..dbd33c0f1c
--- /dev/null
+++ b/tuto3/src/construction_game.mli
@@ -0,0 +1 @@
+val example_sort_app_lambda : unit -> unit
\ No newline at end of file
diff --git a/tuto3/src/g_tuto3.ml4 b/tuto3/src/g_tuto3.ml4
index aaeabcf34f..2c9bd5b121 100644
--- a/tuto3/src/g_tuto3.ml4
+++ b/tuto3/src/g_tuto3.ml4
@@ -2,6 +2,9 @@ DECLARE PLUGIN "tuto3_plugin"
open Ltac_plugin
open Pp
+
+open Construction_game
+
(* This one is necessary, to avoid message about missing wit_string *)
open Stdarg
@@ -18,28 +21,6 @@ VERNAC COMMAND EXTEND ShowTypeConstruction CLASSIFIED AS QUERY
END
VERNAC COMMAND EXTEND ShowOneConstruction CLASSIFIED AS QUERY
-| [ "Tuto3_2" ] ->
- [ let gr_S =
- Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "S" in
- (* the long name of "S" was found with the command "About S." *)
- let gr_O =
- Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in
- let c_O = EConstr.of_constr (Universes.constr_of_global gr_O) in
- let env = Global.env () in
- let evd = Evd.from_env env in
- let evd, s = Evd.new_sort_variable Evd.univ_rigid evd in
- let new_type_2 = EConstr.mkSort s in
- let evd, arg_type = Evarutil.new_evar env evd new_type_2 in
- let c_f =
- EConstr.mkLambda(Names.Name (Names.Id.of_string "x"), arg_type,
- EConstr.mkRel 1) in
- let c_1 = EConstr.mkApp (c_f, [| c_O |]) in
- (* type verification happens here. Type verification will update
- existential variable information in the evd part. *)
- let evd, the_type =
- Typing.type_of (Global.env()) evd c_1 in
- Feedback.msg_notice
- ((Termops.print_constr_env env evd c_1) ++
- str " has type " ++
- (Termops.print_constr_env env evd the_type)) ]
+| [ "Tuto3_2" ] -> [ example_sort_app_lambda() ]
END
+
diff --git a/tuto3/src/tuto3_plugin.mlpack b/tuto3/src/tuto3_plugin.mlpack
index 7aa7cdb9ee..3b6ce58e45 100644
--- a/tuto3/src/tuto3_plugin.mlpack
+++ b/tuto3/src/tuto3_plugin.mlpack
@@ -1 +1,2 @@
+Construction_game
G_tuto3
\ No newline at end of file
--
cgit v1.2.3
From bcb59435d92b09ecf87b747a6b449743f7735bd8 Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Wed, 9 May 2018 14:41:53 +0200
Subject: an example with type classes, but no class inference triggered yet
---
tuto3/_CoqProject | 1 +
tuto3/src/construction_game.ml | 65 ++++++++++++++++++++++++++++++++++++++---
tuto3/src/construction_game.mli | 3 +-
tuto3/src/g_tuto3.ml4 | 6 +++-
tuto3/theories/Data.v | 9 ++++++
tuto3/theories/Loader.v | 2 ++
6 files changed, 80 insertions(+), 6 deletions(-)
create mode 100644 tuto3/theories/Data.v
diff --git a/tuto3/_CoqProject b/tuto3/_CoqProject
index 5f1bd0450c..23ba975de4 100644
--- a/tuto3/_CoqProject
+++ b/tuto3/_CoqProject
@@ -1,6 +1,7 @@
-R theories Tuto3
-I src
+theories/Data.v
theories/Loader.v
src/construction_game.ml
diff --git a/tuto3/src/construction_game.ml b/tuto3/src/construction_game.ml
index df3bfd5d21..953687cce2 100644
--- a/tuto3/src/construction_game.ml
+++ b/tuto3/src/construction_game.ml
@@ -43,12 +43,11 @@ let dangling_identity2 env evd =
EConstr.mkRel 1)
let example_sort_app_lambda () =
-(* Next, I wish to construct a lambda-abstraction without giving precisely
- the type for the abstracted variable. *)
let env = Global.env () in
let evd = Evd.from_env env in
let c_v = c_one () in
- let evd, c_f = dangling_identity env evd in
+(* dangling_identity and dangling_identity2 can be used interchangeably here *)
+ let evd, c_f = dangling_identity2 env evd in
let c_1 = EConstr.mkApp (c_f, [| c_v |]) in
let _ = Feedback.msg_notice
(Termops.print_constr_env env evd c_1) in
@@ -62,4 +61,62 @@ let example_sort_app_lambda () =
Feedback.msg_notice
((Termops.print_constr_env env evd c_1) ++
str " has type " ++
- (Termops.print_constr_env env evd the_type))
\ No newline at end of file
+ (Termops.print_constr_env env evd the_type))
+
+let constants = ref ([] : EConstr.constr list)
+
+let collect_constants () =
+ if (!constants = []) then
+ let open Coqlib in
+ let open EConstr in
+ let open Universes in
+ let gr_S = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "S" in
+ let gr_O = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in
+ let gr_E = find_reference "Tuto3" ["Tuto3"; "Data"] "EvenNat" in
+ let gr_D = find_reference "Tuto3" ["Tuto3"; "Data"] "tuto_div2" in
+ constants := List.map (fun x -> of_constr (constr_of_global x))
+ [gr_S; gr_O; gr_E; gr_D];
+ !constants
+ else
+ !constants
+
+let c_S () =
+ match collect_constants () with
+ it :: _ -> it
+ | _ -> failwith "could not obtain an internal representation of S : nat"
+
+let c_O () =
+ match collect_constants () with
+ _ :: it :: _ -> it
+ | _ -> failwith "could not obtain an internal representation of 0 : nat"
+
+let c_E () =
+ match collect_constants () with
+ _ :: _ :: it :: _ -> it
+ | _ -> failwith "could not obtain an internal representation of EvenNat"
+
+let c_D () =
+ match collect_constants () with
+ _ :: _ :: _ :: it :: _ -> it
+ | _ -> failwith "could not obtain an internal representation of tuto_div2"
+
+let mk_nat n =
+ let c_S = c_S () in
+ let c_O = c_O () in
+ let rec buildup = function
+ | 0 -> c_O
+ | n -> EConstr.mkApp (c_S, [| buildup (n - 1) |]) in
+ if n <= 0 then c_O else buildup n
+
+let example_classes n =
+ let c_n = mk_nat n in
+ let c_div = c_D () in
+ let c_even = c_E () in
+ let arg_type = EConstr.mkApp (c_even, [| c_n |]) in
+ let env = Global.env () in
+ let evd = Evd.from_env env in
+ let evd, instance = Evarutil.new_evar env evd arg_type in
+ let c_1 = EConstr.mkApp (c_div, [|c_n; instance|]) in
+ let _ = Feedback.msg_notice (Termops.print_constr_env env evd c_1) in
+ let evd, the_type = Typing.type_of env evd c_1 in
+ Feedback.msg_notice (Termops.print_constr_env env evd c_1)
\ No newline at end of file
diff --git a/tuto3/src/construction_game.mli b/tuto3/src/construction_game.mli
index dbd33c0f1c..a4172734fd 100644
--- a/tuto3/src/construction_game.mli
+++ b/tuto3/src/construction_game.mli
@@ -1 +1,2 @@
-val example_sort_app_lambda : unit -> unit
\ No newline at end of file
+val example_sort_app_lambda : unit -> unit
+val example_classes : int -> unit
diff --git a/tuto3/src/g_tuto3.ml4 b/tuto3/src/g_tuto3.ml4
index 2c9bd5b121..e0f60b34c8 100644
--- a/tuto3/src/g_tuto3.ml4
+++ b/tuto3/src/g_tuto3.ml4
@@ -21,6 +21,10 @@ VERNAC COMMAND EXTEND ShowTypeConstruction CLASSIFIED AS QUERY
END
VERNAC COMMAND EXTEND ShowOneConstruction CLASSIFIED AS QUERY
-| [ "Tuto3_2" ] -> [ example_sort_app_lambda() ]
+| [ "Tuto3_2" ] -> [ example_sort_app_lambda () ]
+END
+
+VERNAC COMMAND EXTEND TriggerClasses CLASSIFIED AS QUERY
+| [ "Tuto3_3" int(n) ] -> [ example_classes n ]
END
diff --git a/tuto3/theories/Data.v b/tuto3/theories/Data.v
new file mode 100644
index 0000000000..15e36bc6ec
--- /dev/null
+++ b/tuto3/theories/Data.v
@@ -0,0 +1,9 @@
+Class EvenNat n := {half : nat; half_prop : 2 * half = n}.
+
+Instance EvenNat2 : EvenNat 2 := {half := 1; half_prop := eq_refl}.
+
+Instance EvenNat4 : EvenNat 4 := {half := 2; half_prop := eq_refl}.
+
+Definition tuto_div2 n (p : EvenNat n) := @half n p.
+
+
diff --git a/tuto3/theories/Loader.v b/tuto3/theories/Loader.v
index cff239af41..eb3182cdaa 100644
--- a/tuto3/theories/Loader.v
+++ b/tuto3/theories/Loader.v
@@ -1 +1,3 @@
+From Tuto3 Require Import Data.
+
Declare ML Module "tuto3_plugin".
\ No newline at end of file
--
cgit v1.2.3
From 178d7414cc1ba0c951f7240a839ce2a8afb78bbc Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Wed, 9 May 2018 15:26:42 +0200
Subject: trying to force the resolution of type classes by using a cast
---
tuto3/src/construction_game.ml | 39 +++++++++++++++++++++++++++++++++------
1 file changed, 33 insertions(+), 6 deletions(-)
diff --git a/tuto3/src/construction_game.ml b/tuto3/src/construction_game.ml
index 953687cce2..86731c48ac 100644
--- a/tuto3/src/construction_game.ml
+++ b/tuto3/src/construction_game.ml
@@ -74,8 +74,11 @@ let collect_constants () =
let gr_O = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in
let gr_E = find_reference "Tuto3" ["Tuto3"; "Data"] "EvenNat" in
let gr_D = find_reference "Tuto3" ["Tuto3"; "Data"] "tuto_div2" in
+ let gr_Q = find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq" in
+ let gr_R = find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq_refl" in
+ let gr_N = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "nat" in
constants := List.map (fun x -> of_constr (constr_of_global x))
- [gr_S; gr_O; gr_E; gr_D];
+ [gr_S; gr_O; gr_E; gr_D; gr_Q; gr_R; gr_N];
!constants
else
!constants
@@ -100,8 +103,23 @@ let c_D () =
_ :: _ :: _ :: it :: _ -> it
| _ -> failwith "could not obtain an internal representation of tuto_div2"
+let c_Q () =
+ match collect_constants () with
+ _ :: _ :: _ :: _ :: it :: _ -> it
+ | _ -> failwith "could not obtain an internal representation of eq"
+
+let c_R () =
+ match collect_constants () with
+ _ :: _ :: _ :: _ :: _ :: it :: _ -> it
+ | _ -> failwith "could not obtain an internal representation of eq_refl"
+
+let c_N () =
+ match collect_constants () with
+ _ :: _ :: _ :: _ :: _ :: _ :: it :: _ -> it
+ | _ -> failwith "could not obtain an internal representation of nat"
+
let mk_nat n =
- let c_S = c_S () in
+ let c_S = c_S () in
let c_O = c_O () in
let rec buildup = function
| 0 -> c_O
@@ -110,13 +128,22 @@ let mk_nat n =
let example_classes n =
let c_n = mk_nat n in
+ let n_half = mk_nat (n / 2) in
+ let c_N = c_N () in
let c_div = c_D () in
let c_even = c_E () in
+ let c_Q = c_Q () in
+ let c_R = c_R () in
let arg_type = EConstr.mkApp (c_even, [| c_n |]) in
let env = Global.env () in
let evd = Evd.from_env env in
let evd, instance = Evarutil.new_evar env evd arg_type in
- let c_1 = EConstr.mkApp (c_div, [|c_n; instance|]) in
- let _ = Feedback.msg_notice (Termops.print_constr_env env evd c_1) in
- let evd, the_type = Typing.type_of env evd c_1 in
- Feedback.msg_notice (Termops.print_constr_env env evd c_1)
\ No newline at end of file
+ let c_half = EConstr.mkApp (c_div, [|c_n; instance|]) in
+ let _ = Feedback.msg_notice (Termops.print_constr_env env evd c_half) in
+ let evd, the_type = Typing.type_of env evd c_half in
+ let _ = Feedback.msg_notice (Termops.print_constr_env env evd c_half) in
+ let proved_equality =
+ EConstr.mkCast(EConstr.mkApp (c_R, [| c_N; c_half |]), DEFAULTcast,
+ EConstr.mkApp (c_Q, [| c_N; c_half; n_half|])) in
+ let evd, final_type = Typing.type_of env evd proved_equality in
+ Feedback.msg_notice (Termops.print_constr_env env evd proved_equality)
\ No newline at end of file
--
cgit v1.2.3
From 4459f8cc7e1c3e4204b5a833e8c9e722609bf355 Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Wed, 9 May 2018 17:44:50 +0200
Subject: checkpoint
---
tuto3/src/construction_game.ml | 22 ++++++++++++++++++++++
tuto3/theories/Data.v | 30 ++++++++++++++++++++++++++----
tuto3/theories/Loader.v | 2 +-
3 files changed, 49 insertions(+), 5 deletions(-)
diff --git a/tuto3/src/construction_game.ml b/tuto3/src/construction_game.ml
index 86731c48ac..4ca59ddd36 100644
--- a/tuto3/src/construction_game.ml
+++ b/tuto3/src/construction_game.ml
@@ -127,6 +127,28 @@ let mk_nat n =
if n <= 0 then c_O else buildup n
let example_classes n =
+ let c_n = mk_nat n in
+ let n_half = mk_nat (n / 2) in
+ let c_N = c_N () in
+ let c_div = c_D () in
+ let c_even = c_E () in
+ let c_Q = c_Q () in
+ let c_R = c_R () in
+ let arg_type = EConstr.mkApp (c_even, [| c_n |]) in
+ let env = Global.env () in
+ let evd = Evd.from_env env in
+ let evd, instance = Evarutil.new_evar env evd arg_type in
+ let c_half = EConstr.mkApp (c_div, [|c_n; instance|]) in
+ let _ = Feedback.msg_notice (Termops.print_constr_env env evd c_half) in
+ let evd, the_type = Typing.type_of env evd c_half in
+ let _ = Feedback.msg_notice (Termops.print_constr_env env evd c_half) in
+ let proved_equality =
+ EConstr.mkCast(EConstr.mkApp (c_R, [| c_N; c_half |]), DEFAULTcast,
+ EConstr.mkApp (c_Q, [| c_N; c_half; n_half|])) in
+ let evd, final_type = Typing.type_of env evd proved_equality in
+ Feedback.msg_notice (Termops.print_constr_env env evd proved_equality)
+
+let example_canonical n =
let c_n = mk_nat n in
let n_half = mk_nat (n / 2) in
let c_N = c_N () in
diff --git a/tuto3/theories/Data.v b/tuto3/theories/Data.v
index 15e36bc6ec..c6ed5c66da 100644
--- a/tuto3/theories/Data.v
+++ b/tuto3/theories/Data.v
@@ -1,9 +1,31 @@
-Class EvenNat n := {half : nat; half_prop : 2 * half = n}.
+Require Import ArithRing.
-Instance EvenNat2 : EvenNat 2 := {half := 1; half_prop := eq_refl}.
+Class EvenNat the_even := {half : nat; half_prop : 2 * half = the_even}.
-Instance EvenNat4 : EvenNat 4 := {half := 2; half_prop := eq_refl}.
+Instance EvenNat0 : EvenNat 0 := {half := 0; half_prop := eq_refl}.
-Definition tuto_div2 n (p : EvenNat n) := @half n p.
+Lemma even_rec n h : 2 * h = n -> 2 * S h = S (S n).
+Proof. intros H; ring [H]. Qed.
+Instance EvenNat_rec n (p : EvenNat n) : EvenNat (S (S n)) :=
+ {half := S (@half _ p); half_prop := even_rec n (@half _ p) (@half_prop _ p)}.
+
+
+Definition tuto_div2 n (p : EvenNat n) := @half _ p.
+
+Record S_ev n := Build_S_ev {double_of : nat; s_h_prop : 2 * n = double_of}.
+
+Canonical Structure can_ev0 : S_ev 0 :=
+ Build_S_ev 0 0 (@eq_refl _ 0).
+
+Lemma can_ev_rec n : forall (s : S_ev n), S_ev (S n).
+Proof.
+intros s; exists (S (S (double_of _ s))).
+destruct s as [a P]. simpl. ring [P].
+Defined.
+
+Canonical Structure can_ev_rec.
+
+Canonical Structure can_ev_default n d (Pd : 2 * n = d) : S_ev n :=
+ Build_S_ev n d Pd.
diff --git a/tuto3/theories/Loader.v b/tuto3/theories/Loader.v
index eb3182cdaa..952565dbea 100644
--- a/tuto3/theories/Loader.v
+++ b/tuto3/theories/Loader.v
@@ -1,3 +1,3 @@
-From Tuto3 Require Import Data.
+From Tuto3 Require Export Data.
Declare ML Module "tuto3_plugin".
\ No newline at end of file
--
cgit v1.2.3
From a3f8e01c9e705fcc2d73187ebf3f26d586b47f8d Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Wed, 9 May 2018 17:44:50 +0200
Subject: This version contains an example of using canonical structures so
that type-checking actually triggers the automatic build of a proof.
---
tuto3/src/construction_game.ml | 67 +++++++++++++++++++++++++++++++++++++++--
tuto3/src/construction_game.mli | 1 +
tuto3/src/g_tuto3.ml4 | 4 +++
tuto3/theories/Data.v | 44 ++++++++++++++++++++++++---
tuto3/theories/Loader.v | 2 +-
5 files changed, 110 insertions(+), 8 deletions(-)
diff --git a/tuto3/src/construction_game.ml b/tuto3/src/construction_game.ml
index 86731c48ac..9a3d046cf5 100644
--- a/tuto3/src/construction_game.ml
+++ b/tuto3/src/construction_game.ml
@@ -77,8 +77,11 @@ let collect_constants () =
let gr_Q = find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq" in
let gr_R = find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq_refl" in
let gr_N = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "nat" in
+ let gr_C = find_reference "Tuto3" ["Tuto3"; "Data"] "C" in
+ let gr_F = find_reference "Tuto3" ["Tuto3"; "Data"] "S_ev" in
+ let gr_P = find_reference "Tuto3" ["Tuto3"; "Data"] "s_half_proof" in
constants := List.map (fun x -> of_constr (constr_of_global x))
- [gr_S; gr_O; gr_E; gr_D; gr_Q; gr_R; gr_N];
+ [gr_S; gr_O; gr_E; gr_D; gr_Q; gr_R; gr_N; gr_C; gr_F; gr_P];
!constants
else
!constants
@@ -118,6 +121,21 @@ let c_N () =
_ :: _ :: _ :: _ :: _ :: _ :: it :: _ -> it
| _ -> failwith "could not obtain an internal representation of nat"
+let c_C () =
+ match collect_constants () with
+ _ :: _ :: _ :: _ :: _ :: _ :: _ :: it :: _ -> it
+ | _ -> failwith "could not obtain an internal representation of cmp"
+
+let c_F () =
+ match collect_constants () with
+ _ :: _ :: _ :: _ :: _ :: _ :: _ :: _ :: it :: _ -> it
+ | _ -> failwith "could not obtain an internal representation of S_ev"
+
+let c_P () =
+ match collect_constants () with
+ _ :: _ :: _ :: _ :: _ :: _ :: _ :: _ :: _ :: it :: _ -> it
+ | _ -> failwith "could not obtain an internal representation of s_half_proof"
+
let mk_nat n =
let c_S = c_S () in
let c_O = c_O () in
@@ -143,7 +161,50 @@ let example_classes n =
let evd, the_type = Typing.type_of env evd c_half in
let _ = Feedback.msg_notice (Termops.print_constr_env env evd c_half) in
let proved_equality =
- EConstr.mkCast(EConstr.mkApp (c_R, [| c_N; c_half |]), DEFAULTcast,
+ EConstr.mkCast(EConstr.mkApp (c_R, [| c_N; c_half |]), Constr.DEFAULTcast,
EConstr.mkApp (c_Q, [| c_N; c_half; n_half|])) in
let evd, final_type = Typing.type_of env evd proved_equality in
- Feedback.msg_notice (Termops.print_constr_env env evd proved_equality)
\ No newline at end of file
+ Feedback.msg_notice (Termops.print_constr_env env evd proved_equality)
+
+(* This function, together with definitions in Data.v, shows how to
+ trigger automatic proofs at the time of typechecking.
+
+ n is a number for which we want to find the half (and a proof that
+ this half is indeed the half)
+*)
+let example_canonical n =
+(* Construct a natural representation of this integer. *)
+ let c_n = mk_nat n in
+(* terms for "nat", "eq", "S_ev", "eq_refl", "C" *)
+ let c_N = c_N () in
+ let c_Q = c_Q () in
+ let c_F = c_F () in
+ let c_R = c_R () in
+ let c_C = c_C () in
+ let c_P = c_P () in
+(* the last argument of C *)
+ let refl_term = EConstr.mkApp (c_R, [|c_N; c_n |]) in
+ let env = Global.env () in
+ let evd = Evd.from_env env in
+(* Now we build two existential variables, for the value of the half and for
+ the "S_ev" structure that triggers the proof search. *)
+ let evd, ev1 = Evarutil.new_evar env evd c_N in
+(* This is the type for the second existential variable *)
+ let csev = EConstr.mkApp (c_F, [| ev1 |]) in
+ let evd, ev2 = Evarutil.new_evar env evd csev in
+(* Now we build the C structure. *)
+ let test_term = EConstr.mkApp (c_C, [| c_n; ev1; ev2; refl_term |]) in
+(* Type-checking this term will compute values for the existential variables *)
+ let evd, final_type = Typing.type_of env evd test_term in
+(* The computed type has two parameters, the second one is the proof. *)
+ let value = match EConstr.kind evd final_type with
+ | App(_, [| _; the_half |]) -> the_half
+ | _ -> failwith "expecting the whole type to be ""cmp _ the_half""" in
+ let _ = Feedback.msg_notice (Termops.print_constr_env env evd value) in
+(* I wish for a nicer way to get the value of ev2 in the evar_map *)
+ let prf_struct = EConstr.of_constr (EConstr.to_constr evd ev2) in
+ let the_prf = EConstr.mkApp (c_P, [| ev1; prf_struct |]) in
+ let evd, the_statement = Typing.type_of env evd the_prf in
+ Feedback.msg_notice
+ (Termops.print_constr_env env evd the_prf ++ str " has type " ++
+ Termops.print_constr_env env evd the_statement)
\ No newline at end of file
diff --git a/tuto3/src/construction_game.mli b/tuto3/src/construction_game.mli
index a4172734fd..302aec1de9 100644
--- a/tuto3/src/construction_game.mli
+++ b/tuto3/src/construction_game.mli
@@ -1,2 +1,3 @@
val example_sort_app_lambda : unit -> unit
val example_classes : int -> unit
+val example_canonical : int -> unit
diff --git a/tuto3/src/g_tuto3.ml4 b/tuto3/src/g_tuto3.ml4
index e0f60b34c8..963662895a 100644
--- a/tuto3/src/g_tuto3.ml4
+++ b/tuto3/src/g_tuto3.ml4
@@ -28,3 +28,7 @@ VERNAC COMMAND EXTEND TriggerClasses CLASSIFIED AS QUERY
| [ "Tuto3_3" int(n) ] -> [ example_classes n ]
END
+VERNAC COMMAND EXTEND TriggerClasses CLASSIFIED AS QUERY
+| [ "Tuto3_4" int(n) ] -> [ example_canonical n ]
+END
+
diff --git a/tuto3/theories/Data.v b/tuto3/theories/Data.v
index 15e36bc6ec..c288d5d452 100644
--- a/tuto3/theories/Data.v
+++ b/tuto3/theories/Data.v
@@ -1,9 +1,45 @@
-Class EvenNat n := {half : nat; half_prop : 2 * half = n}.
+Require Import ArithRing.
-Instance EvenNat2 : EvenNat 2 := {half := 1; half_prop := eq_refl}.
+Class EvenNat the_even := {half : nat; half_prop : 2 * half = the_even}.
-Instance EvenNat4 : EvenNat 4 := {half := 2; half_prop := eq_refl}.
+Instance EvenNat0 : EvenNat 0 := {half := 0; half_prop := eq_refl}.
-Definition tuto_div2 n (p : EvenNat n) := @half n p.
+Lemma even_rec n h : 2 * h = n -> 2 * S h = S (S n).
+Proof. intros H; ring [H]. Qed.
+Instance EvenNat_rec n (p : EvenNat n) : EvenNat (S (S n)) :=
+ {half := S (@half _ p); half_prop := even_rec n (@half _ p) (@half_prop _ p)}.
+
+Definition tuto_div2 n (p : EvenNat n) := @half _ p.
+
+Record S_ev n := Build_S_ev {double_of : nat; _ : 2 * n = double_of}.
+
+Definition s_half_proof n (r : S_ev n) : 2 * n = double_of n r :=
+ match r with Build_S_ev _ _ h => h end.
+
+Canonical Structure can_ev_default n d (Pd : 2 * n = d) : S_ev n :=
+ Build_S_ev n d Pd.
+
+Canonical Structure can_ev0 : S_ev 0 :=
+ Build_S_ev 0 0 (@eq_refl _ 0).
+
+
+Lemma can_ev_rec n : forall (s : S_ev n), S_ev (S n).
+Proof.
+intros s; exists (S (S (double_of _ s))).
+destruct s as [a P]. simpl. ring [P].
+Defined.
+
+Canonical Structure can_ev_rec.
+
+Record cmp (n : nat) (k : nat) :=
+ C {h : S_ev k; _ : double_of k h = n}.
+
+(* To be used in, e.g.,
+
+Check (C _ _ _ eq_refl : cmp 6 _).
+
+Check (C _ _ _ eq_refl : cmp 7 _).
+
+*)
diff --git a/tuto3/theories/Loader.v b/tuto3/theories/Loader.v
index eb3182cdaa..952565dbea 100644
--- a/tuto3/theories/Loader.v
+++ b/tuto3/theories/Loader.v
@@ -1,3 +1,3 @@
-From Tuto3 Require Import Data.
+From Tuto3 Require Export Data.
Declare ML Module "tuto3_plugin".
\ No newline at end of file
--
cgit v1.2.3
From cb49f4c22261174f4c0a7f1a26fa795af8ed2155 Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Thu, 10 May 2018 08:21:40 +0200
Subject: finished the example where type class resolution is forced
---
tuto3/src/construction_game.ml | 6 ++++++
tuto3/src/g_tuto3.ml4 | 2 +-
2 files changed, 7 insertions(+), 1 deletion(-)
diff --git a/tuto3/src/construction_game.ml b/tuto3/src/construction_game.ml
index 9a3d046cf5..0a94419e83 100644
--- a/tuto3/src/construction_game.ml
+++ b/tuto3/src/construction_game.ml
@@ -155,6 +155,7 @@ let example_classes n =
let arg_type = EConstr.mkApp (c_even, [| c_n |]) in
let env = Global.env () in
let evd = Evd.from_env env in
+ let evd0 = evd in
let evd, instance = Evarutil.new_evar env evd arg_type in
let c_half = EConstr.mkApp (c_div, [|c_n; instance|]) in
let _ = Feedback.msg_notice (Termops.print_constr_env env evd c_half) in
@@ -163,6 +164,11 @@ let example_classes n =
let proved_equality =
EConstr.mkCast(EConstr.mkApp (c_R, [| c_N; c_half |]), Constr.DEFAULTcast,
EConstr.mkApp (c_Q, [| c_N; c_half; n_half|])) in
+(* This is where we force the system to compute with type classes. *)
+(* Question to coq developers: why do we pass two evd arguments to
+ solve_remaining_evars? Is the choice of evd0 relevant here? *)
+ let evd = Pretyping.solve_remaining_evars
+ (Pretyping.default_inference_flags true) env evd evd0 in
let evd, final_type = Typing.type_of env evd proved_equality in
Feedback.msg_notice (Termops.print_constr_env env evd proved_equality)
diff --git a/tuto3/src/g_tuto3.ml4 b/tuto3/src/g_tuto3.ml4
index 963662895a..f028880087 100644
--- a/tuto3/src/g_tuto3.ml4
+++ b/tuto3/src/g_tuto3.ml4
@@ -28,7 +28,7 @@ VERNAC COMMAND EXTEND TriggerClasses CLASSIFIED AS QUERY
| [ "Tuto3_3" int(n) ] -> [ example_classes n ]
END
-VERNAC COMMAND EXTEND TriggerClasses CLASSIFIED AS QUERY
+VERNAC COMMAND EXTEND TriggerCanonical CLASSIFIED AS QUERY
| [ "Tuto3_4" int(n) ] -> [ example_canonical n ]
END
--
cgit v1.2.3
From c74ead36e32c49dbbf030083ba150e10bb1c74cf Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Fri, 11 May 2018 11:34:35 +0200
Subject: Use the more colloquial EConstr.t type instead of EConstr.constr
---
tuto3/src/construction_game.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/tuto3/src/construction_game.ml b/tuto3/src/construction_game.ml
index df761b4505..c893952d6a 100644
--- a/tuto3/src/construction_game.ml
+++ b/tuto3/src/construction_game.ml
@@ -63,7 +63,7 @@ let example_sort_app_lambda () =
str " has type " ++
(Termops.print_constr_env env evd the_type))
-let constants = ref ([] : EConstr.constr list)
+let constants = ref ([] : EConstr.t list)
let collect_constants () =
if (!constants = []) then
--
cgit v1.2.3
From 9559285108ec87ad7a813bcb208145a04e86ab5c Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Fri, 11 May 2018 11:35:37 +0200
Subject: Adds a tactic that hides the contents of an hypothesis from view
---
tuto3/_CoqProject | 2 ++
tuto3/src/g_tuto3.ml4 | 4 +++
tuto3/src/tuto3_plugin.mlpack | 1 +
tuto3/src/tuto_tactic.ml | 62 +++++++++++++++++++++++++++++++++++++++++++
tuto3/src/tuto_tactic.mli | 1 +
tuto3/theories/Data.v | 7 +++++
6 files changed, 77 insertions(+)
create mode 100644 tuto3/src/tuto_tactic.ml
create mode 100644 tuto3/src/tuto_tactic.mli
diff --git a/tuto3/_CoqProject b/tuto3/_CoqProject
index 23ba975de4..6a3c1978a7 100644
--- a/tuto3/_CoqProject
+++ b/tuto3/_CoqProject
@@ -4,6 +4,8 @@
theories/Data.v
theories/Loader.v
+src/tuto_tactic.ml
+src/tuto_tactic.mli
src/construction_game.ml
src/construction_game.mli
src/g_tuto3.ml4
diff --git a/tuto3/src/g_tuto3.ml4 b/tuto3/src/g_tuto3.ml4
index f028880087..a4095ae2e7 100644
--- a/tuto3/src/g_tuto3.ml4
+++ b/tuto3/src/g_tuto3.ml4
@@ -32,3 +32,7 @@ VERNAC COMMAND EXTEND TriggerCanonical CLASSIFIED AS QUERY
| [ "Tuto3_4" int(n) ] -> [ example_canonical n ]
END
+TACTIC EXTEND collapse_hyps
+| [ "hide" "hypothesis" ident(i) ] ->
+ [ Tuto_tactic.hide_tactic i ]
+END
\ No newline at end of file
diff --git a/tuto3/src/tuto3_plugin.mlpack b/tuto3/src/tuto3_plugin.mlpack
index 3b6ce58e45..d6fc1d509a 100644
--- a/tuto3/src/tuto3_plugin.mlpack
+++ b/tuto3/src/tuto3_plugin.mlpack
@@ -1,2 +1,3 @@
Construction_game
+Tuto_tactic
G_tuto3
\ No newline at end of file
diff --git a/tuto3/src/tuto_tactic.ml b/tuto3/src/tuto_tactic.ml
new file mode 100644
index 0000000000..a0ac967731
--- /dev/null
+++ b/tuto3/src/tuto_tactic.ml
@@ -0,0 +1,62 @@
+open Proofview
+
+let constants = ref ([] : EConstr.t list)
+
+let collect_constants () =
+ if (!constants = []) then
+ let open Coqlib in
+ let open EConstr in
+ let open Universes in
+ let gr_H = find_reference "Tuto3" ["Tuto3"; "Data"] "hide" in
+ let gr_M = find_reference "Tuto3" ["Tuto3"; "Data"] "hide_marker" in
+ constants := List.map (fun x -> of_constr (constr_of_global x))
+ [gr_H; gr_M];
+ !constants
+ else
+ !constants
+
+let c_H () =
+ match collect_constants () with
+ it :: _ -> it
+ | _ -> failwith "could not obtain an internal representation of hide"
+
+let c_M () =
+ match collect_constants () with
+ _ :: it :: _ -> it
+ | _ -> failwith "could not obtain an internal representation of hide_marker"
+
+let package i = Goal.enter begin fun gl ->
+ Tactics.apply_in true false i
+ [None, (CAst.make (c_M (), Misctypes.NoBindings))] None
+ end
+(*
+let package i = Goal.enter begin fun gl ->
+ let h_hyps_id = (Names.Id.of_string "hidden_hyps") in
+ let env = Goal.env gl in
+ let store = Goal.extra gl in
+ let concl = Tacmach.New.pf_concl in
+
+ let ty_i = ... in
+ let ev = Evarutil.new_evar in
+ mkApp (mkLambda(h_hyps_id, mkApp(c_h, [|ty_i|] , ev),
+ [| mkApp (c_hm, [| ty_ev; EConstr.mkVar i |]) |])
+end
+ *)
+
+let repackage _ = failwith "todo"
+
+let hide_tactic i =
+ let h_hyps_id = (Names.Id.of_string "hidden_hyps") in
+ Proofview.Goal.enter begin fun gl ->
+ let hyps = Environ.named_context_val (Proofview.Goal.env gl) in
+ if not (Termops.mem_named_context_val i hyps) then
+ (CErrors.user_err
+ (Pp.str ("no hypothesis named" ^ (Names.Id.to_string i))))
+ else
+ if Termops.mem_named_context_val h_hyps_id hyps then
+ tclTHEN (Tactics.revert [i; h_hyps_id]) (repackage ())
+ else
+ package i
+ end
+
+
diff --git a/tuto3/src/tuto_tactic.mli b/tuto3/src/tuto_tactic.mli
new file mode 100644
index 0000000000..13f905ed8a
--- /dev/null
+++ b/tuto3/src/tuto_tactic.mli
@@ -0,0 +1 @@
+val hide_tactic : Names.Id.t -> unit Proofview.tactic
diff --git a/tuto3/theories/Data.v b/tuto3/theories/Data.v
index b2afffed68..4de0a9a0f9 100644
--- a/tuto3/theories/Data.v
+++ b/tuto3/theories/Data.v
@@ -41,3 +41,10 @@ Check (C _ _ _ eq_refl : cmp 6 _).
Check (C _ _ _ eq_refl : cmp 7 _).
*)
+
+Inductive hide (A: Type) : Type :=
+ hide_marker : A -> hide A.
+
+Arguments hide_marker {A}.
+
+Notation "!!!" := (hide _) (at level 0, only printing).
\ No newline at end of file
--
cgit v1.2.3
From 1117a348c1ca11833ae12361500d08c62fd8f76b Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Fri, 11 May 2018 17:19:37 +0200
Subject: This version contains documentation for the code of the packing
tactic warning have been removed Examples for the use of type classes and
canonical structures in automatic proof have been moved to the end.
---
tuto3/src/g_tuto3.ml4 | 14 +++--
tuto3/src/tuto_tactic.ml | 134 +++++++++++++++++++++++++++++++++++++---------
tuto3/src/tuto_tactic.mli | 4 +-
tuto3/theories/Data.v | 32 ++++++++---
tuto3/theories/test.v | 23 ++++++++
5 files changed, 168 insertions(+), 39 deletions(-)
create mode 100644 tuto3/theories/test.v
diff --git a/tuto3/src/g_tuto3.ml4 b/tuto3/src/g_tuto3.ml4
index a4095ae2e7..8b123eb7b0 100644
--- a/tuto3/src/g_tuto3.ml4
+++ b/tuto3/src/g_tuto3.ml4
@@ -1,7 +1,6 @@
DECLARE PLUGIN "tuto3_plugin"
open Ltac_plugin
-open Pp
open Construction_game
@@ -24,15 +23,20 @@ VERNAC COMMAND EXTEND ShowOneConstruction CLASSIFIED AS QUERY
| [ "Tuto3_2" ] -> [ example_sort_app_lambda () ]
END
+TACTIC EXTEND collapse_hyps
+| [ "pack" "hypothesis" ident(i) ] ->
+ [ Tuto_tactic.pack_tactic i ]
+END
+
+(* More advanced examples, where automatic proof happens but
+ no tactic is being called explicitely. The first one uses
+ type classes. *)
VERNAC COMMAND EXTEND TriggerClasses CLASSIFIED AS QUERY
| [ "Tuto3_3" int(n) ] -> [ example_classes n ]
END
+(* The second one uses canonical structures. *)
VERNAC COMMAND EXTEND TriggerCanonical CLASSIFIED AS QUERY
| [ "Tuto3_4" int(n) ] -> [ example_canonical n ]
END
-TACTIC EXTEND collapse_hyps
-| [ "hide" "hypothesis" ident(i) ] ->
- [ Tuto_tactic.hide_tactic i ]
-END
\ No newline at end of file
diff --git a/tuto3/src/tuto_tactic.ml b/tuto3/src/tuto_tactic.ml
index a0ac967731..fbb6863f7e 100644
--- a/tuto3/src/tuto_tactic.ml
+++ b/tuto3/src/tuto_tactic.ml
@@ -2,15 +2,21 @@ open Proofview
let constants = ref ([] : EConstr.t list)
+(* This is a pattern to collect terms from the Coq memory of valid terms
+ and proofs. This pattern extends all the way to the definition of function
+ c_U *)
let collect_constants () =
if (!constants = []) then
let open Coqlib in
let open EConstr in
let open Universes in
- let gr_H = find_reference "Tuto3" ["Tuto3"; "Data"] "hide" in
- let gr_M = find_reference "Tuto3" ["Tuto3"; "Data"] "hide_marker" in
+ let gr_H = find_reference "Tuto3" ["Tuto3"; "Data"] "pack" in
+ let gr_M = find_reference "Tuto3" ["Tuto3"; "Data"] "packer" in
+ let gr_R = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "pair" in
+ let gr_P = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "prod" in
+ let gr_U = find_reference "Tuto3" ["Tuto3"; "Data"] "uncover" in
constants := List.map (fun x -> of_constr (constr_of_global x))
- [gr_H; gr_M];
+ [gr_H; gr_M; gr_R; gr_P; gr_U];
!constants
else
!constants
@@ -18,35 +24,109 @@ let collect_constants () =
let c_H () =
match collect_constants () with
it :: _ -> it
- | _ -> failwith "could not obtain an internal representation of hide"
+ | _ -> failwith "could not obtain an internal representation of pack"
let c_M () =
match collect_constants () with
_ :: it :: _ -> it
- | _ -> failwith "could not obtain an internal representation of hide_marker"
+ | _ -> failwith "could not obtain an internal representation of pack_marker"
+let c_R () =
+ match collect_constants () with
+ _ :: _ :: it :: _ -> it
+ | _ -> failwith "could not obtain an internal representation of pair"
+
+let c_P () =
+ match collect_constants () with
+ _ :: _ :: _ :: it :: _ -> it
+ | _ -> failwith "could not obtain an internal representation of prod"
+
+let c_U () =
+ match collect_constants () with
+ _ :: _ :: _ :: _ :: it :: _ -> it
+ | _ -> failwith "could not obtain an internal representation of prod"
+
+(* The following tactic is meant to pack an hypothesis when no other
+ data is already packed.
+
+ The main difficulty in defining this tactic is to understand how to
+ construct the input expected by apply_in. *)
let package i = Goal.enter begin fun gl ->
Tactics.apply_in true false i
- [None, (CAst.make (c_M (), Misctypes.NoBindings))] None
+ [(* this means that the applied theorem is not to be cleared. *)
+ None, (CAst.make (c_M (),
+ (* we don't specialize the theorem with extra values. *)
+ Misctypes.NoBindings))]
+ (* we don't destruct the result according to any intro_pattern *)
+ None
end
-(*
-let package i = Goal.enter begin fun gl ->
- let h_hyps_id = (Names.Id.of_string "hidden_hyps") in
+
+(* This function is meant to observe a type of shape (f a)
+ and return the value a. *)
+
+(* Remark by Maxime: look for destApp combinator. *)
+let unpack_type evd term =
+ let report () =
+ CErrors.user_err (Pp.str "expecting a packed type") in
+ match EConstr.kind evd term with
+ | Constr.App (_, [| ty |]) -> ty
+ | _ -> report ()
+
+(* This function is meant to observe a type of shape
+ A -> pack B -> C and return A, B, C
+ but it is not used in the current version of our tactic.
+ It is kept as an example. *)
+let two_lambda_pattern evd term =
+ let report () =
+ CErrors.user_err (Pp.str "expecting two nested implications") in
+(* Note that pattern-matching is always done through the EConstr.kind function,
+ which only provides one-level deep patterns. *)
+ match EConstr.kind evd term with
+ (* Here we recognize the outer implication *)
+ | Constr.Prod (_, ty1, l1) ->
+ (* Here we recognize the inner implication *)
+ (match EConstr.kind evd l1 with
+ | Constr.Prod (n2, packed_ty2, deep_conclusion) ->
+ (* Here we recognized that the second type is an application *)
+ ty1, unpack_type evd packed_ty2, deep_conclusion
+ | _ -> report ())
+ | _ -> report ()
+
+(* In the environment of the goal, we can get the type of an assumption
+ directly by a lookup. The other solution is to call a low-cost retyping
+ function like *)
+let get_type_of_hyp env id =
+ match EConstr.lookup_named id env with
+ | Context.Named.Declaration.LocalAssum (_, ty) -> ty
+ | _ -> CErrors.user_err (let open Pp in
+ str (Names.Id.to_string id) ++
+ str " is not a plain hypothesis")
+
+let repackage i h_hyps_id = Goal.enter begin fun gl ->
let env = Goal.env gl in
let store = Goal.extra gl in
- let concl = Tacmach.New.pf_concl in
-
- let ty_i = ... in
- let ev = Evarutil.new_evar in
- mkApp (mkLambda(h_hyps_id, mkApp(c_h, [|ty_i|] , ev),
- [| mkApp (c_hm, [| ty_ev; EConstr.mkVar i |]) |])
-end
- *)
-
-let repackage _ = failwith "todo"
-
-let hide_tactic i =
- let h_hyps_id = (Names.Id.of_string "hidden_hyps") in
+ let evd = Tacmach.New.project gl in
+ let concl = Tacmach.New.pf_concl gl in
+ let (ty1 : EConstr.t) = get_type_of_hyp env i in
+ let (packed_ty2 : EConstr.t) = get_type_of_hyp env h_hyps_id in
+ let ty2 = unpack_type evd packed_ty2 in
+ let new_packed_type = EConstr.mkApp (c_P (), [| ty1; ty2 |]) in
+ let open EConstr in
+ let new_packed_value =
+ mkApp (c_R (), [| ty1; ty2; mkVar i;
+ mkApp (c_U (), [| ty2; mkVar h_hyps_id|]) |]) in
+ Refine.refine ~typecheck:true begin fun evd ->
+ let evd, new_goal = Evarutil.new_evar env evd ~store
+ (mkProd (Names.Name.Anonymous,
+ mkApp(c_H (), [| new_packed_type |]),
+ Vars.lift 1 concl)) in
+ evd, mkApp (new_goal,
+ [|mkApp(c_M (), [|new_packed_type; new_packed_value |]) |])
+ end
+ end
+
+let pack_tactic i =
+ let h_hyps_id = (Names.Id.of_string "packed_hyps") in
Proofview.Goal.enter begin fun gl ->
let hyps = Environ.named_context_val (Proofview.Goal.env gl) in
if not (Termops.mem_named_context_val i hyps) then
@@ -54,9 +134,11 @@ let hide_tactic i =
(Pp.str ("no hypothesis named" ^ (Names.Id.to_string i))))
else
if Termops.mem_named_context_val h_hyps_id hyps then
- tclTHEN (Tactics.revert [i; h_hyps_id]) (repackage ())
+ tclTHEN (repackage i h_hyps_id)
+ (tclTHEN (Tactics.clear [h_hyps_id; i])
+ (Tactics.introduction h_hyps_id))
else
- package i
+ tclTHEN (package i)
+ (tclTHEN (Tactics.rename_hyp [i, h_hyps_id])
+ (Tactics.move_hyp h_hyps_id Misctypes.MoveLast))
end
-
-
diff --git a/tuto3/src/tuto_tactic.mli b/tuto3/src/tuto_tactic.mli
index 13f905ed8a..dbf6cf48e2 100644
--- a/tuto3/src/tuto_tactic.mli
+++ b/tuto3/src/tuto_tactic.mli
@@ -1 +1,3 @@
-val hide_tactic : Names.Id.t -> unit Proofview.tactic
+val two_lambda_pattern :
+ Evd.evar_map -> EConstr.t -> EConstr.t * EConstr.t * EConstr.t
+val pack_tactic : Names.Id.t -> unit Proofview.tactic
diff --git a/tuto3/theories/Data.v b/tuto3/theories/Data.v
index 4de0a9a0f9..0b07fee4f2 100644
--- a/tuto3/theories/Data.v
+++ b/tuto3/theories/Data.v
@@ -1,5 +1,18 @@
Require Import ArithRing.
+Inductive pack (A: Type) : Type :=
+ packer : A -> pack A.
+
+Arguments packer {A}.
+
+Definition uncover (A : Type) (packed : pack A) : A :=
+ match packed with packer v => v end.
+
+Notation "!!!" := (pack _) (at level 0, only printing).
+
+(* The following data is used as material for automatic proofs
+ based on type classes. *)
+
Class EvenNat the_even := {half : nat; half_prop : 2 * half = the_even}.
Instance EvenNat0 : EvenNat 0 := {half := 0; half_prop := eq_refl}.
@@ -12,6 +25,18 @@ Instance EvenNat_rec n (p : EvenNat n) : EvenNat (S (S n)) :=
Definition tuto_div2 n (p : EvenNat n) := @half _ p.
+(* to be used in the following examples
+Compute (@half 8 _).
+
+Check (@half_prop 8 _).
+
+Check (@half_prop 7 _).
+
+and in command Tuto3_3 8. *)
+
+(* The following data is used as material for automatic proofs
+ based on canonical structures. *)
+
Record S_ev n := Build_S_ev {double_of : nat; _ : 2 * n = double_of}.
Definition s_half_proof n (r : S_ev n) : 2 * n = double_of n r :=
@@ -41,10 +66,3 @@ Check (C _ _ _ eq_refl : cmp 6 _).
Check (C _ _ _ eq_refl : cmp 7 _).
*)
-
-Inductive hide (A: Type) : Type :=
- hide_marker : A -> hide A.
-
-Arguments hide_marker {A}.
-
-Notation "!!!" := (hide _) (at level 0, only printing).
\ No newline at end of file
diff --git a/tuto3/theories/test.v b/tuto3/theories/test.v
new file mode 100644
index 0000000000..43204ddf34
--- /dev/null
+++ b/tuto3/theories/test.v
@@ -0,0 +1,23 @@
+(* to be used e.g. in : coqtop -I src -R theories Tuto3 < theories/test.v *)
+
+Require Import Tuto3.Loader.
+
+(* This should print Type. *)
+Tuto3_1.
+
+(* This should print a term that contains an existential variable. *)
+(* And then print the same term, where the variable has been correctly
+ instantiated. *)
+Tuto3_2.
+
+Lemma tutu x y (A : 0 < x) (B : 10 < y) : True.
+Proof.
+pack hypothesis A.
+(* Hypothesis A should have disappeared and a "packed_hyps" hypothesis
+ should have appeared, with unreadable content. *)
+pack hypothesis B.
+(* Hypothesis B should have disappeared *)
+destruct packed_hyps as [unpacked_hyps].
+(* Hypothesis unpacked_hyps should contain the previous contents of A and B. *)
+exact I.
+Qed.
--
cgit v1.2.3
From d558653e3a0ecc0b182f5e84a8db474d7a5aa1f8 Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Fri, 11 May 2018 17:24:18 +0200
Subject: Updates the contents of the third tutorial
---
README.md | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
diff --git a/README.md b/README.md
index 00ff146e46..417a511f82 100644
--- a/README.md
+++ b/README.md
@@ -42,9 +42,8 @@ How to write plugins in Coq
- Obtaining existing values from memory
- Composing values
- Verifying types
- - Leveraging type inference
- - Leveraging coercion
- Using these terms in commands
- Using these terms in tactics
+ - Automatic proofs without tactics using type classes and canonical structures
compilation and loading must be performed as for `tuto0`.
--
cgit v1.2.3
From 679140212d704885f91ec4a23d60628f85bf830a Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Sat, 12 May 2018 22:05:23 +0200
Subject: adds a hello world tactic in tuto0
---
README.md | 4 +++-
tuto0/src/g_tuto0.ml4 | 9 ++++++++-
2 files changed, 11 insertions(+), 2 deletions(-)
diff --git a/README.md b/README.md
index 417a511f82..64d4241360 100644
--- a/README.md
+++ b/README.md
@@ -4,7 +4,9 @@ How to write plugins in Coq
# tuto0 : basics of project organization
package a ml4 file in a plugin, organize a `Makefile`, `_CoqProject`
- Example of syntax to add a new toplevel command
- - Example of function call to print a simple message.
+ - Example of function call to print a simple message
+ - Example of syntax to add a simple tactic
+ (that does nothing and prints a message)
- To use it:
```bash
diff --git a/tuto0/src/g_tuto0.ml4 b/tuto0/src/g_tuto0.ml4
index e3656fc986..df6e187d52 100644
--- a/tuto0/src/g_tuto0.ml4
+++ b/tuto0/src/g_tuto0.ml4
@@ -1,7 +1,14 @@
DECLARE PLUGIN "tuto0"
open Pp
+open Ltac_plugin
VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY
| [ "HelloWorld" ] -> [ Feedback.msg_notice (strbrk Tuto0_main.message) ]
-END
\ No newline at end of file
+END
+
+TACTIC EXTEND hello_world_tactic
+| [ "hello_world" ] ->
+ [ let _ = Feedback.msg_notice (str Tuto0_main.message) in
+ Tacticals.New.tclIDTAC ]
+END
--
cgit v1.2.3
From 64b9e9fd6290024431fbcfdbb8aaad4d4b9cc1f9 Mon Sep 17 00:00:00 2001
From: Enrico
Date: Thu, 17 May 2018 17:08:09 +0200
Subject: [tuto1] Minor fixes to comments
---
tuto1/src/g_tuto1.ml4 | 5 +++--
1 file changed, 3 insertions(+), 2 deletions(-)
diff --git a/tuto1/src/g_tuto1.ml4 b/tuto1/src/g_tuto1.ml4
index 78deabed94..bd53053ec7 100644
--- a/tuto1/src/g_tuto1.ml4
+++ b/tuto1/src/g_tuto1.ml4
@@ -7,7 +7,8 @@ DECLARE PLUGIN "tuto1_plugin"
*)
open Ltac_plugin
open Pp
-(* This one is necessary, to avoid message about missing wit_string *)
+(* This module defines the types of arguments to be used in the
+ EXTEND directives below, for example the string one. *)
open Stdarg
VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY
@@ -68,7 +69,7 @@ END
(* When adding a definition, we have to be careful that just
the operation of constructing a well-typed term may already change
the environment, at the level of universe constraints (which
- are recorded in the evd component). The fonction
+ are recorded in the evd component). The function
Constrintern.interp_constr ignores this side-effect, so it should
not be used here. *)
--
cgit v1.2.3
From cf6317101ab537f982fa8694be305be41709ae97 Mon Sep 17 00:00:00 2001
From: Enrico
Date: Thu, 17 May 2018 17:19:36 +0200
Subject: Add some setup instructions
---
README.md | 35 +++++++++++++++++++++++++++++++++++
1 file changed, 35 insertions(+)
diff --git a/README.md b/README.md
index 64d4241360..f82edb2352 100644
--- a/README.md
+++ b/README.md
@@ -1,6 +1,41 @@
How to write plugins in Coq
===========================
# Working environment : merlin, tuareg (open question)
+
+ ## OCaml & related tools
+
+ These instructions use [OPAM](http://opam.ocaml.org/doc/Install.html)
+
+```shell
+opam init --root=$PWD/CIW2018 --compiler=4.06.0 -j2
+eval `opam config env --root=$PWD/CIW2018`
+opam install camlp5 ocamlfind num # Coq's dependencies
+opam install lablgtk # Coqide's dependencies (optional)
+opam install merlin # prints instructions for vim and emacs
+```
+
+ ## Coq
+
+```shell
+git clone git@github.com:coq/coq.git
+cd coq
+./configure -profile devel
+make -j2
+cd ..
+export PATH=$PWD/coq/bin:$PATH
+```
+
+ ## This tutorial
+
+```shell
+git clone git@github.com:ybertot/plugin_tutorials.git
+cd plugin_tutorials/tuto0
+make .merlin # run before opening .ml files in your editor
+make # build
+```
+
+
+
# tuto0 : basics of project organization
package a ml4 file in a plugin, organize a `Makefile`, `_CoqProject`
- Example of syntax to add a new toplevel command
--
cgit v1.2.3
From b88102233366b9290fc8819443764a15c109e00c Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 17 May 2018 17:23:21 +0200
Subject: DECLARE PLUGIN "$name" === Declare ML Module "$name"
---
tuto0/src/g_tuto0.ml4 | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/tuto0/src/g_tuto0.ml4 b/tuto0/src/g_tuto0.ml4
index df6e187d52..d6e95ba0f7 100644
--- a/tuto0/src/g_tuto0.ml4
+++ b/tuto0/src/g_tuto0.ml4
@@ -1,4 +1,4 @@
-DECLARE PLUGIN "tuto0"
+DECLARE PLUGIN "tuto0_plugin"
open Pp
open Ltac_plugin
--
cgit v1.2.3
From 127e40a28d2659e2e2197b87cf043a375647fe3b Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 17 May 2018 17:25:28 +0200
Subject: add little test
- tests the plugin can actually be loaded (eg with the wrong DECLARE PLUGIN
it loads but then the tactic is not in scope)
- sine is listed in _CoqProject one can open it with CoqIDE/PG and get
the -I -R flags from the _CoqProject automatically
---
tuto0/_CoqProject | 4 +++-
tuto0/theories/Demo.v | 8 ++++++++
2 files changed, 11 insertions(+), 1 deletion(-)
create mode 100644 tuto0/theories/Demo.v
diff --git a/tuto0/_CoqProject b/tuto0/_CoqProject
index ca0c0588a4..dd93e1fa79 100644
--- a/tuto0/_CoqProject
+++ b/tuto0/_CoqProject
@@ -2,7 +2,9 @@
-I src
theories/Loader.v
+theories/Demo.v
+
src/tuto0_main.ml
src/tuto0_main.mli
src/g_tuto0.ml4
-src/tuto0_plugin.mlpack
\ No newline at end of file
+src/tuto0_plugin.mlpack
diff --git a/tuto0/theories/Demo.v b/tuto0/theories/Demo.v
new file mode 100644
index 0000000000..bdc61986af
--- /dev/null
+++ b/tuto0/theories/Demo.v
@@ -0,0 +1,8 @@
+From Tuto0 Require Import Loader.
+
+HelloWorld.
+
+Lemma test : True.
+Proof.
+hello_world.
+Abort.
--
cgit v1.2.3
From 7f31b7f1ee4d4857aaed86ad7fd6bcbb83e2a705 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 17 May 2018 17:36:44 +0200
Subject: [tuto2] Clarify where the name of the ML plugin is used
---
tuto2/_CoqProject | 2 +-
tuto2/src/demo.ml4 | 16 +++++++++++-----
tuto2/src/demo_plugin.mlpack | 1 +
tuto2/src/tuto_plugin.mlpack | 1 -
tuto2/theories/Test.v | 2 +-
5 files changed, 14 insertions(+), 8 deletions(-)
create mode 100644 tuto2/src/demo_plugin.mlpack
delete mode 100644 tuto2/src/tuto_plugin.mlpack
diff --git a/tuto2/_CoqProject b/tuto2/_CoqProject
index f38ee8d6a6..bdafdb5f04 100644
--- a/tuto2/_CoqProject
+++ b/tuto2/_CoqProject
@@ -3,4 +3,4 @@
theories/Test.v
src/demo.ml4
-src/tuto_plugin.mlpack
+src/demo_plugin.mlpack
diff --git a/tuto2/src/demo.ml4 b/tuto2/src/demo.ml4
index 3d165a6302..981d41fa5c 100644
--- a/tuto2/src/demo.ml4
+++ b/tuto2/src/demo.ml4
@@ -4,23 +4,29 @@
(* *)
(* -------------------------------------------------------------------------- *)
-DECLARE PLUGIN "demo"
+DECLARE PLUGIN "demo_plugin"
(*
- Use this macro before any of the other Ocaml macros.
+ 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".
+ We have decided to name this plugin as "demo_plugin".
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".
+ Declare ML Module "demo_plugin".
- (2) The above command will succeed only if there is "demo.cmxs"
+ (2) The above command will succeed only if there is "demo_plugin.cmxs"
in some of the directories that Coq is supposed to look
(i.e. the ones we specified via "-I ..." command line options).
+
+ (3) The file "demo_plugin.mlpack" lists the OCaml modules to be linked in
+ "demo_plugin.cmxs".
+
+ (4) The file "demo_plugin.mlpack" as well as all .ml, .mli and .ml4 files
+ are listed in the "_CoqProject" file.
*)
(* -------------------------------------------------------------------------- *)
diff --git a/tuto2/src/demo_plugin.mlpack b/tuto2/src/demo_plugin.mlpack
new file mode 100644
index 0000000000..043a3b4633
--- /dev/null
+++ b/tuto2/src/demo_plugin.mlpack
@@ -0,0 +1 @@
+Demo
\ No newline at end of file
diff --git a/tuto2/src/tuto_plugin.mlpack b/tuto2/src/tuto_plugin.mlpack
deleted file mode 100644
index 043a3b4633..0000000000
--- a/tuto2/src/tuto_plugin.mlpack
+++ /dev/null
@@ -1 +0,0 @@
-Demo
\ No newline at end of file
diff --git a/tuto2/theories/Test.v b/tuto2/theories/Test.v
index 5522a3444a..38e83bfff1 100644
--- a/tuto2/theories/Test.v
+++ b/tuto2/theories/Test.v
@@ -1,4 +1,4 @@
-Declare ML Module "demo".
+Declare ML Module "demo_plugin".
Cmd1.
Cmd2 With Some Terminal Parameters.
--
cgit v1.2.3
From 34d32da819739e795ba2b4fac96652f1fa27d969 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 28 May 2018 16:29:42 +0200
Subject: Use user printer for terms instead of debug printer
---
tuto1/src/g_tuto1.ml4 | 8 ++++----
tuto3/src/construction_game.ml | 18 +++++++++---------
tuto3/src/g_tuto3.ml4 | 2 +-
3 files changed, 14 insertions(+), 14 deletions(-)
diff --git a/tuto1/src/g_tuto1.ml4 b/tuto1/src/g_tuto1.ml4
index bd53053ec7..b152583824 100644
--- a/tuto1/src/g_tuto1.ml4
+++ b/tuto1/src/g_tuto1.ml4
@@ -91,7 +91,7 @@ VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY
let (_, ctx) = v in
let evd = Evd.from_ctx ctx in
Feedback.msg_notice
- (Termops.print_constr_env (Global.env()) evd
+ (Printer.pr_econstr_env (Global.env()) evd
(Simple_check.simple_check1 v)) ]
END
@@ -101,7 +101,7 @@ VERNAC COMMAND EXTEND Check2 CLASSIFIED AS QUERY
(Evd.from_env (Global.env())) e in
let evd, ty = Simple_check.simple_check2 v in
Feedback.msg_notice
- (Termops.print_constr_env (Global.env()) evd ty) ]
+ (Printer.pr_econstr_env (Global.env()) evd ty) ]
END
VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY
@@ -111,7 +111,7 @@ VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY
let (a, ctx) = v in
let evd = Evd.from_ctx ctx in
Feedback.msg_notice
- (Termops.print_constr_env (Global.env()) evd
+ (Printer.pr_econstr_env (Global.env()) evd
(Simple_check.simple_check3 v)) ]
END
@@ -125,7 +125,7 @@ VERNAC COMMAND EXTEND ExamplePrint CLASSIFIED AS QUERY
[ let env = Global.env() in
let evd = Evd.from_env env in
Feedback.msg_notice
- (Termops.print_constr_env env evd
+ (Printer.pr_econstr_env env evd
(EConstr.of_constr
(Simple_print.simple_body_access (Nametab.global r)))) ]
END
diff --git a/tuto3/src/construction_game.ml b/tuto3/src/construction_game.ml
index c893952d6a..cce4941419 100644
--- a/tuto3/src/construction_game.ml
+++ b/tuto3/src/construction_game.ml
@@ -50,7 +50,7 @@ let example_sort_app_lambda () =
let evd, c_f = dangling_identity2 env evd in
let c_1 = EConstr.mkApp (c_f, [| c_v |]) in
let _ = Feedback.msg_notice
- (Termops.print_constr_env env evd c_1) in
+ (Printer.pr_econstr_env env evd c_1) in
(* type verification happens here. Type verification will update
existential variable information in the evd part. *)
let evd, the_type =
@@ -59,9 +59,9 @@ let example_sort_app_lambda () =
existential variable being instantiated to the "nat" type, even
though c_1 still contains the meta-variable. *)
Feedback.msg_notice
- ((Termops.print_constr_env env evd c_1) ++
+ ((Printer.pr_econstr_env env evd c_1) ++
str " has type " ++
- (Termops.print_constr_env env evd the_type))
+ (Printer.pr_econstr_env env evd the_type))
let constants = ref ([] : EConstr.t list)
@@ -158,9 +158,9 @@ let example_classes n =
let evd0 = evd in
let evd, instance = Evarutil.new_evar env evd arg_type in
let c_half = EConstr.mkApp (c_div, [|c_n; instance|]) in
- let _ = Feedback.msg_notice (Termops.print_constr_env env evd c_half) in
+ let _ = Feedback.msg_notice (Printer.pr_econstr_env env evd c_half) in
let evd, the_type = Typing.type_of env evd c_half in
- let _ = Feedback.msg_notice (Termops.print_constr_env env evd c_half) in
+ let _ = Feedback.msg_notice (Printer.pr_econstr_env env evd c_half) in
let proved_equality =
EConstr.mkCast(EConstr.mkApp (c_R, [| c_N; c_half |]), Constr.DEFAULTcast,
EConstr.mkApp (c_Q, [| c_N; c_half; n_half|])) in
@@ -170,7 +170,7 @@ let example_classes n =
let evd = Pretyping.solve_remaining_evars
(Pretyping.default_inference_flags true) env evd evd0 in
let evd, final_type = Typing.type_of env evd proved_equality in
- Feedback.msg_notice (Termops.print_constr_env env evd proved_equality)
+ Feedback.msg_notice (Printer.pr_econstr_env env evd proved_equality)
(* This function, together with definitions in Data.v, shows how to
trigger automatic proofs at the time of typechecking, based on
@@ -207,11 +207,11 @@ let example_canonical n =
let value = match EConstr.kind evd final_type with
| App(_, [| _; the_half |]) -> the_half
| _ -> failwith "expecting the whole type to be ""cmp _ the_half""" in
- let _ = Feedback.msg_notice (Termops.print_constr_env env evd value) in
+ let _ = Feedback.msg_notice (Printer.pr_econstr_env env evd value) in
(* I wish for a nicer way to get the value of ev2 in the evar_map *)
let prf_struct = EConstr.of_constr (EConstr.to_constr evd ev2) in
let the_prf = EConstr.mkApp (c_P, [| ev1; prf_struct |]) in
let evd, the_statement = Typing.type_of env evd the_prf in
Feedback.msg_notice
- (Termops.print_constr_env env evd the_prf ++ str " has type " ++
- Termops.print_constr_env env evd the_statement)
+ (Printer.pr_econstr_env env evd the_prf ++ str " has type " ++
+ Printer.pr_econstr_env env evd the_statement)
diff --git a/tuto3/src/g_tuto3.ml4 b/tuto3/src/g_tuto3.ml4
index 8b123eb7b0..71c6be16c8 100644
--- a/tuto3/src/g_tuto3.ml4
+++ b/tuto3/src/g_tuto3.ml4
@@ -16,7 +16,7 @@ VERNAC COMMAND EXTEND ShowTypeConstruction CLASSIFIED AS QUERY
let evd, _ =
Typing.type_of (Global.env()) (Evd.from_env (Global.env())) new_type_2 in
Feedback.msg_notice
- (Termops.print_constr_env env evd new_type_2) ]
+ (Printer.pr_econstr_env env evd new_type_2) ]
END
VERNAC COMMAND EXTEND ShowOneConstruction CLASSIFIED AS QUERY
--
cgit v1.2.3
From 46f908ab5a03998fa96c1a599b44e6e2b3fd9a10 Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Wed, 30 May 2018 15:25:26 +0200
Subject: this version has no warnings when compiling
---
tuto3/src/construction_game.ml | 5 ++---
tuto3/src/construction_game.mli | 1 +
2 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/tuto3/src/construction_game.ml b/tuto3/src/construction_game.ml
index c893952d6a..1bbfc70cb5 100644
--- a/tuto3/src/construction_game.ml
+++ b/tuto3/src/construction_game.ml
@@ -184,7 +184,6 @@ let example_canonical n =
let c_n = mk_nat n in
(* terms for "nat", "eq", "S_ev", "eq_refl", "C" *)
let c_N = c_N () in
- let c_Q = c_Q () in
let c_F = c_F () in
let c_R = c_R () in
let c_C = c_C () in
@@ -205,8 +204,8 @@ let example_canonical n =
let evd, final_type = Typing.type_of env evd test_term in
(* The computed type has two parameters, the second one is the proof. *)
let value = match EConstr.kind evd final_type with
- | App(_, [| _; the_half |]) -> the_half
- | _ -> failwith "expecting the whole type to be ""cmp _ the_half""" in
+ | Constr.App(_, [| _; the_half |]) -> the_half
+ | _ -> failwith "expecting the whole type to be \"cmp _ the_half\"" in
let _ = Feedback.msg_notice (Termops.print_constr_env env evd value) in
(* I wish for a nicer way to get the value of ev2 in the evar_map *)
let prf_struct = EConstr.of_constr (EConstr.to_constr evd ev2) in
diff --git a/tuto3/src/construction_game.mli b/tuto3/src/construction_game.mli
index 302aec1de9..1832ed6630 100644
--- a/tuto3/src/construction_game.mli
+++ b/tuto3/src/construction_game.mli
@@ -1,3 +1,4 @@
+val dangling_identity : Environ.env -> Evd.evar_map -> Evd.evar_map * EConstr.t
val example_sort_app_lambda : unit -> unit
val example_classes : int -> unit
val example_canonical : int -> unit
--
cgit v1.2.3
From ef843bc9794242d1cec2d30ec1825dc2cde6ef1b Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Wed, 30 May 2018 17:31:01 +0200
Subject: remove uses of Universes.constr_of_global
---
tuto3/src/construction_game.ml | 174 +++++++++++++++++------------------------
1 file changed, 71 insertions(+), 103 deletions(-)
diff --git a/tuto3/src/construction_game.ml b/tuto3/src/construction_game.ml
index 1bbfc70cb5..e69d65f975 100644
--- a/tuto3/src/construction_game.ml
+++ b/tuto3/src/construction_game.ml
@@ -8,19 +8,18 @@ let example_sort evd =
let new_type = EConstr.mkSort s in
evd, new_type
-let c_one () =
-(* What happens in constructing a new natural number from the datatype
- constructors does not require any handling of existential variables
- or universes, so evd datastructures don't appear here. *)
+let c_one evd =
+(* In the general case, global references may refer to universe polymorphic
+ objects, and their universe has to be made afresh when creating an instance. *)
let gr_S =
Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "S" in
(* the long name of "S" was found with the command "About S." *)
let gr_O =
Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in
- let c_O = EConstr.of_constr (Universes.constr_of_global gr_O) in
- let c_S = EConstr.of_constr (Universes.constr_of_global gr_S) in
+ let evd, c_O = Evarutil.new_global evd gr_O in
+ let evd, c_S = Evarutil.new_global evd gr_S in
(* Here is the construction of a new term by applying functions to argument. *)
- EConstr.mkApp (c_S, [| c_O |])
+ evd, EConstr.mkApp (c_S, [| c_O |])
let dangling_identity env evd =
(* I call this a dangling identity, because it is not polymorph, but
@@ -45,7 +44,7 @@ let dangling_identity2 env evd =
let example_sort_app_lambda () =
let env = Global.env () in
let evd = Evd.from_env env in
- let c_v = c_one () in
+ let evd, c_v = c_one evd in
(* dangling_identity and dangling_identity2 can be used interchangeably here *)
let evd, c_f = dangling_identity2 env evd in
let c_1 = EConstr.mkApp (c_f, [| c_v |]) in
@@ -53,8 +52,7 @@ let example_sort_app_lambda () =
(Termops.print_constr_env env evd c_1) in
(* type verification happens here. Type verification will update
existential variable information in the evd part. *)
- let evd, the_type =
- Typing.type_of (Global.env()) evd c_1 in
+ let evd, the_type = Typing.type_of env evd c_1 in
(* At display time, you will notice that the system knows about the
existential variable being instantiated to the "nat" type, even
though c_1 still contains the meta-variable. *)
@@ -63,98 +61,68 @@ let example_sort_app_lambda () =
str " has type " ++
(Termops.print_constr_env env evd the_type))
-let constants = ref ([] : EConstr.t list)
-
-let collect_constants () =
- if (!constants = []) then
- let open Coqlib in
- let open EConstr in
- let open Universes in
- let gr_S = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "S" in
- let gr_O = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in
- let gr_E = find_reference "Tuto3" ["Tuto3"; "Data"] "EvenNat" in
- let gr_D = find_reference "Tuto3" ["Tuto3"; "Data"] "tuto_div2" in
- let gr_Q = find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq" in
- let gr_R = find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq_refl" in
- let gr_N = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "nat" in
- let gr_C = find_reference "Tuto3" ["Tuto3"; "Data"] "C" in
- let gr_F = find_reference "Tuto3" ["Tuto3"; "Data"] "S_ev" in
- let gr_P = find_reference "Tuto3" ["Tuto3"; "Data"] "s_half_proof" in
- constants := List.map (fun x -> of_constr (constr_of_global x))
- [gr_S; gr_O; gr_E; gr_D; gr_Q; gr_R; gr_N; gr_C; gr_F; gr_P];
- !constants
- else
- !constants
-
-let c_S () =
- match collect_constants () with
- it :: _ -> it
- | _ -> failwith "could not obtain an internal representation of S : nat"
-
-let c_O () =
- match collect_constants () with
- _ :: it :: _ -> it
- | _ -> failwith "could not obtain an internal representation of 0 : nat"
-
-let c_E () =
- match collect_constants () with
- _ :: _ :: it :: _ -> it
- | _ -> failwith "could not obtain an internal representation of EvenNat"
-
-let c_D () =
- match collect_constants () with
- _ :: _ :: _ :: it :: _ -> it
- | _ -> failwith "could not obtain an internal representation of tuto_div2"
-
-let c_Q () =
- match collect_constants () with
- _ :: _ :: _ :: _ :: it :: _ -> it
- | _ -> failwith "could not obtain an internal representation of eq"
-
-let c_R () =
- match collect_constants () with
- _ :: _ :: _ :: _ :: _ :: it :: _ -> it
- | _ -> failwith "could not obtain an internal representation of eq_refl"
-
-let c_N () =
- match collect_constants () with
- _ :: _ :: _ :: _ :: _ :: _ :: it :: _ -> it
- | _ -> failwith "could not obtain an internal representation of nat"
-
-let c_C () =
- match collect_constants () with
- _ :: _ :: _ :: _ :: _ :: _ :: _ :: it :: _ -> it
- | _ -> failwith "could not obtain an internal representation of cmp"
-
-let c_F () =
- match collect_constants () with
- _ :: _ :: _ :: _ :: _ :: _ :: _ :: _ :: it :: _ -> it
- | _ -> failwith "could not obtain an internal representation of S_ev"
-
-let c_P () =
- match collect_constants () with
- _ :: _ :: _ :: _ :: _ :: _ :: _ :: _ :: _ :: it :: _ -> it
- | _ -> failwith "could not obtain an internal representation of s_half_proof"
-
-let mk_nat n =
- let c_S = c_S () in
- let c_O = c_O () in
+
+let c_S evd =
+ let gr = Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "S" in
+ Evarutil.new_global evd gr
+
+let c_O evd =
+ let gr = Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "O" in
+ Evarutil.new_global evd gr
+
+let c_E evd =
+ let gr = Coqlib.find_reference "Tuto3" ["Tuto3"; "Data"] "EvenNat" in
+ Evarutil.new_global evd gr
+
+let c_D evd =
+ let gr = Coqlib.find_reference "Tuto3" ["Tuto3"; "Data"] "tuto_div2" in
+ Evarutil.new_global evd gr
+
+let c_Q evd =
+ let gr = Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq" in
+ Evarutil.new_global evd gr
+
+let c_R evd =
+ let gr = Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Logic"] "eq_refl" in
+ Evarutil.new_global evd gr
+
+let c_N evd =
+ let gr = Coqlib.find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "nat" in
+ Evarutil.new_global evd gr
+
+let c_C evd =
+ let gr = Coqlib.find_reference "Tuto3" ["Tuto3"; "Data"] "C" in
+ Evarutil.new_global evd gr
+
+let c_F evd =
+ let gr = Coqlib.find_reference "Tuto3" ["Tuto3"; "Data"] "S_ev" in
+ Evarutil.new_global evd gr
+
+let c_P evd =
+ let gr = Coqlib.find_reference "Tuto3" ["Tuto3"; "Data"] "s_half_proof" in
+ Evarutil.new_global evd gr
+
+(* If c_S was universe polymorphic, we should have created a new constant
+ at each iteration of buildup. *)
+let mk_nat evd n =
+ let evd, c_S = c_S evd in
+ let evd, c_O = c_O evd in
let rec buildup = function
| 0 -> c_O
| n -> EConstr.mkApp (c_S, [| buildup (n - 1) |]) in
- if n <= 0 then c_O else buildup n
+ if n <= 0 then evd, c_O else evd, buildup n
let example_classes n =
- let c_n = mk_nat n in
- let n_half = mk_nat (n / 2) in
- let c_N = c_N () in
- let c_div = c_D () in
- let c_even = c_E () in
- let c_Q = c_Q () in
- let c_R = c_R () in
- let arg_type = EConstr.mkApp (c_even, [| c_n |]) in
let env = Global.env () in
let evd = Evd.from_env env in
+ let evd, c_n = mk_nat evd n in
+ let evd, n_half = mk_nat evd (n / 2) in
+ let evd, c_N = c_N evd in
+ let evd, c_div = c_D evd in
+ let evd, c_even = c_E evd in
+ let evd, c_Q = c_Q evd in
+ let evd, c_R = c_R evd in
+ let arg_type = EConstr.mkApp (c_even, [| c_n |]) in
let evd0 = evd in
let evd, instance = Evarutil.new_evar env evd arg_type in
let c_half = EConstr.mkApp (c_div, [|c_n; instance|]) in
@@ -180,18 +148,18 @@ let example_classes n =
this half is indeed the half)
*)
let example_canonical n =
+ let env = Global.env () in
+ let evd = Evd.from_env env in
(* Construct a natural representation of this integer. *)
- let c_n = mk_nat n in
+ let evd, c_n = mk_nat evd n in
(* terms for "nat", "eq", "S_ev", "eq_refl", "C" *)
- let c_N = c_N () in
- let c_F = c_F () in
- let c_R = c_R () in
- let c_C = c_C () in
- let c_P = c_P () in
+ let evd, c_N = c_N evd in
+ let evd, c_F = c_F evd in
+ let evd, c_R = c_R evd in
+ let evd, c_C = c_C evd in
+ let evd, c_P = c_P evd in
(* the last argument of C *)
let refl_term = EConstr.mkApp (c_R, [|c_N; c_n |]) in
- let env = Global.env () in
- let evd = Evd.from_env env in
(* Now we build two existential variables, for the value of the half and for
the "S_ev" structure that triggers the proof search. *)
let evd, ev1 = Evarutil.new_evar env evd c_N in
--
cgit v1.2.3
From b303b75c18734accc9cd7efe82307b0424426e3f Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Wed, 18 Jul 2018 16:11:43 +0200
Subject: the same license as for the coq development
---
LICENSE | 458 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 458 insertions(+)
create mode 100644 LICENSE
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000000..27950e8d20
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,458 @@
+ GNU LESSER GENERAL PUBLIC LICENSE
+ Version 2.1, February 1999
+
+ Copyright (C) 1991, 1999 Free Software Foundation, Inc.
+ 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
+ Everyone is permitted to copy and distribute verbatim copies
+ of this license document, but changing it is not allowed.
+
+[This is the first released version of the Lesser GPL. It also counts
+ as the successor of the GNU Library Public License, version 2, hence
+ the version number 2.1.]
+
+ Preamble
+
+ The licenses for most software are designed to take away your
+freedom to share and change it. By contrast, the GNU General Public
+Licenses are intended to guarantee your freedom to share and change
+free software--to make sure the software is free for all its users.
+
+ This license, the Lesser General Public License, applies to some
+specially designated software packages--typically libraries--of the
+Free Software Foundation and other authors who decide to use it. You
+can use it too, but we suggest you first think carefully about whether
+this license or the ordinary General Public License is the better
+strategy to use in any particular case, based on the explanations below.
+
+ When we speak of free software, we are referring to freedom of use,
+not price. Our General Public Licenses are designed to make sure that
+you have the freedom to distribute copies of free software (and charge
+for this service if you wish); that you receive source code or can get
+it if you want it; that you can change the software and use pieces of
+it in new free programs; and that you are informed that you can do
+these things.
+
+ To protect your rights, we need to make restrictions that forbid
+distributors to deny you these rights or to ask you to surrender these
+rights. These restrictions translate to certain responsibilities for
+you if you distribute copies of the library or if you modify it.
+
+ For example, if you distribute copies of the library, whether gratis
+or for a fee, you must give the recipients all the rights that we gave
+you. You must make sure that they, too, receive or can get the source
+code. If you link other code with the library, you must provide
+complete object files to the recipients, so that they can relink them
+with the library after making changes to the library and recompiling
+it. And you must show them these terms so they know their rights.
+
+ We protect your rights with a two-step method: (1) we copyright the
+library, and (2) we offer you this license, which gives you legal
+permission to copy, distribute and/or modify the library.
+
+ To protect each distributor, we want to make it very clear that
+there is no warranty for the free library. Also, if the library is
+modified by someone else and passed on, the recipients should know
+that what they have is not the original version, so that the original
+author's reputation will not be affected by problems that might be
+introduced by others.
+
+ Finally, software patents pose a constant threat to the existence of
+any free program. We wish to make sure that a company cannot
+effectively restrict the users of a free program by obtaining a
+restrictive license from a patent holder. Therefore, we insist that
+any patent license obtained for a version of the library must be
+consistent with the full freedom of use specified in this license.
+
+ Most GNU software, including some libraries, is covered by the
+ordinary GNU General Public License. This license, the GNU Lesser
+General Public License, applies to certain designated libraries, and
+is quite different from the ordinary General Public License. We use
+this license for certain libraries in order to permit linking those
+libraries into non-free programs.
+
+ When a program is linked with a library, whether statically or using
+a shared library, the combination of the two is legally speaking a
+combined work, a derivative of the original library. The ordinary
+General Public License therefore permits such linking only if the
+entire combination fits its criteria of freedom. The Lesser General
+Public License permits more lax criteria for linking other code with
+the library.
+
+ We call this license the "Lesser" General Public License because it
+does Less to protect the user's freedom than the ordinary General
+Public License. It also provides other free software developers Less
+of an advantage over competing non-free programs. These disadvantages
+are the reason we use the ordinary General Public License for many
+libraries. However, the Lesser license provides advantages in certain
+special circumstances.
+
+ For example, on rare occasions, there may be a special need to
+encourage the widest possible use of a certain library, so that it becomes
+a de-facto standard. To achieve this, non-free programs must be
+allowed to use the library. A more frequent case is that a free
+library does the same job as widely used non-free libraries. In this
+case, there is little to gain by limiting the free library to free
+software only, so we use the Lesser General Public License.
+
+ In other cases, permission to use a particular library in non-free
+programs enables a greater number of people to use a large body of
+free software. For example, permission to use the GNU C Library in
+non-free programs enables many more people to use the whole GNU
+operating system, as well as its variant, the GNU/Linux operating
+system.
+
+ Although the Lesser General Public License is Less protective of the
+users' freedom, it does ensure that the user of a program that is
+linked with the Library has the freedom and the wherewithal to run
+that program using a modified version of the Library.
+
+ The precise terms and conditions for copying, distribution and
+modification follow. Pay close attention to the difference between a
+"work based on the library" and a "work that uses the library". The
+former contains code derived from the library, whereas the latter must
+be combined with the library in order to run.
+
+ GNU LESSER GENERAL PUBLIC LICENSE
+ TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION
+
+ 0. This License Agreement applies to any software library or other
+program which contains a notice placed by the copyright holder or
+other authorized party saying it may be distributed under the terms of
+this Lesser General Public License (also called "this License").
+Each licensee is addressed as "you".
+
+ A "library" means a collection of software functions and/or data
+prepared so as to be conveniently linked with application programs
+(which use some of those functions and data) to form executables.
+
+ The "Library", below, refers to any such software library or work
+which has been distributed under these terms. A "work based on the
+Library" means either the Library or any derivative work under
+copyright law: that is to say, a work containing the Library or a
+portion of it, either verbatim or with modifications and/or translated
+straightforwardly into another language. (Hereinafter, translation is
+included without limitation in the term "modification".)
+
+ "Source code" for a work means the preferred form of the work for
+making modifications to it. For a library, complete source code means
+all the source code for all modules it contains, plus any associated
+interface definition files, plus the scripts used to control compilation
+and installation of the library.
+
+ Activities other than copying, distribution and modification are not
+covered by this License; they are outside its scope. The act of
+running a program using the Library is not restricted, and output from
+such a program is covered only if its contents constitute a work based
+on the Library (independent of the use of the Library in a tool for
+writing it). Whether that is true depends on what the Library does
+and what the program that uses the Library does.
+
+ 1. You may copy and distribute verbatim copies of the Library's
+complete source code as you receive it, in any medium, provided that
+you conspicuously and appropriately publish on each copy an
+appropriate copyright notice and disclaimer of warranty; keep intact
+all the notices that refer to this License and to the absence of any
+warranty; and distribute a copy of this License along with the
+Library.
+
+ You may charge a fee for the physical act of transferring a copy,
+and you may at your option offer warranty protection in exchange for a
+fee.
+
+ 2. You may modify your copy or copies of the Library or any portion
+of it, thus forming a work based on the Library, and copy and
+distribute such modifications or work under the terms of Section 1
+above, provided that you also meet all of these conditions:
+
+ a) The modified work must itself be a software library.
+
+ b) You must cause the files modified to carry prominent notices
+ stating that you changed the files and the date of any change.
+
+ c) You must cause the whole of the work to be licensed at no
+ charge to all third parties under the terms of this License.
+
+ d) If a facility in the modified Library refers to a function or a
+ table of data to be supplied by an application program that uses
+ the facility, other than as an argument passed when the facility
+ is invoked, then you must make a good faith effort to ensure that,
+ in the event an application does not supply such function or
+ table, the facility still operates, and performs whatever part of
+ its purpose remains meaningful.
+
+ (For example, a function in a library to compute square roots has
+ a purpose that is entirely well-defined independent of the
+ application. Therefore, Subsection 2d requires that any
+ application-supplied function or table used by this function must
+ be optional: if the application does not supply it, the square
+ root function must still compute square roots.)
+
+These requirements apply to the modified work as a whole. If
+identifiable sections of that work are not derived from the Library,
+and can be reasonably considered independent and separate works in
+themselves, then this License, and its terms, do not apply to those
+sections when you distribute them as separate works. But when you
+distribute the same sections as part of a whole which is a work based
+on the Library, the distribution of the whole must be on the terms of
+this License, whose permissions for other licensees extend to the
+entire whole, and thus to each and every part regardless of who wrote
+it.
+
+Thus, it is not the intent of this section to claim rights or contest
+your rights to work written entirely by you; rather, the intent is to
+exercise the right to control the distribution of derivative or
+collective works based on the Library.
+
+In addition, mere aggregation of another work not based on the Library
+with the Library (or with a work based on the Library) on a volume of
+a storage or distribution medium does not bring the other work under
+the scope of this License.
+
+ 3. You may opt to apply the terms of the ordinary GNU General Public
+License instead of this License to a given copy of the Library. To do
+this, you must alter all the notices that refer to this License, so
+that they refer to the ordinary GNU General Public License, version 2,
+instead of to this License. (If a newer version than version 2 of the
+ordinary GNU General Public License has appeared, then you can specify
+that version instead if you wish.) Do not make any other change in
+these notices.
+
+ Once this change is made in a given copy, it is irreversible for
+that copy, so the ordinary GNU General Public License applies to all
+subsequent copies and derivative works made from that copy.
+
+ This option is useful when you wish to copy part of the code of
+the Library into a program that is not a library.
+
+ 4. You may copy and distribute the Library (or a portion or
+derivative of it, under Section 2) in object code or executable form
+under the terms of Sections 1 and 2 above provided that you accompany
+it with the complete corresponding machine-readable source code, which
+must be distributed under the terms of Sections 1 and 2 above on a
+medium customarily used for software interchange.
+
+ If distribution of object code is made by offering access to copy
+from a designated place, then offering equivalent access to copy the
+source code from the same place satisfies the requirement to
+distribute the source code, even though third parties are not
+compelled to copy the source along with the object code.
+
+ 5. A program that contains no derivative of any portion of the
+Library, but is designed to work with the Library by being compiled or
+linked with it, is called a "work that uses the Library". Such a
+work, in isolation, is not a derivative work of the Library, and
+therefore falls outside the scope of this License.
+
+ However, linking a "work that uses the Library" with the Library
+creates an executable that is a derivative of the Library (because it
+contains portions of the Library), rather than a "work that uses the
+library". The executable is therefore covered by this License.
+Section 6 states terms for distribution of such executables.
+
+ When a "work that uses the Library" uses material from a header file
+that is part of the Library, the object code for the work may be a
+derivative work of the Library even though the source code is not.
+Whether this is true is especially significant if the work can be
+linked without the Library, or if the work is itself a library. The
+threshold for this to be true is not precisely defined by law.
+
+ If such an object file uses only numerical parameters, data
+structure layouts and accessors, and small macros and small inline
+functions (ten lines or less in length), then the use of the object
+file is unrestricted, regardless of whether it is legally a derivative
+work. (Executables containing this object code plus portions of the
+Library will still fall under Section 6.)
+
+ Otherwise, if the work is a derivative of the Library, you may
+distribute the object code for the work under the terms of Section 6.
+Any executables containing that work also fall under Section 6,
+whether or not they are linked directly with the Library itself.
+
+ 6. As an exception to the Sections above, you may also combine or
+link a "work that uses the Library" with the Library to produce a
+work containing portions of the Library, and distribute that work
+under terms of your choice, provided that the terms permit
+modification of the work for the customer's own use and reverse
+engineering for debugging such modifications.
+
+ You must give prominent notice with each copy of the work that the
+Library is used in it and that the Library and its use are covered by
+this License. You must supply a copy of this License. If the work
+during execution displays copyright notices, you must include the
+copyright notice for the Library among them, as well as a reference
+directing the user to the copy of this License. Also, you must do one
+of these things:
+
+ a) Accompany the work with the complete corresponding
+ machine-readable source code for the Library including whatever
+ changes were used in the work (which must be distributed under
+ Sections 1 and 2 above); and, if the work is an executable linked
+ with the Library, with the complete machine-readable "work that
+ uses the Library", as object code and/or source code, so that the
+ user can modify the Library and then relink to produce a modified
+ executable containing the modified Library. (It is understood
+ that the user who changes the contents of definitions files in the
+ Library will not necessarily be able to recompile the application
+ to use the modified definitions.)
+
+ b) Use a suitable shared library mechanism for linking with the
+ Library. A suitable mechanism is one that (1) uses at run time a
+ copy of the library already present on the user's computer system,
+ rather than copying library functions into the executable, and (2)
+ will operate properly with a modified version of the library, if
+ the user installs one, as long as the modified version is
+ interface-compatible with the version that the work was made with.
+
+ c) Accompany the work with a written offer, valid for at
+ least three years, to give the same user the materials
+ specified in Subsection 6a, above, for a charge no more
+ than the cost of performing this distribution.
+
+ d) If distribution of the work is made by offering access to copy
+ from a designated place, offer equivalent access to copy the above
+ specified materials from the same place.
+
+ e) Verify that the user has already received a copy of these
+ materials or that you have already sent this user a copy.
+
+ For an executable, the required form of the "work that uses the
+Library" must include any data and utility programs needed for
+reproducing the executable from it. However, as a special exception,
+the materials to be distributed need not include anything that is
+normally distributed (in either source or binary form) with the major
+components (compiler, kernel, and so on) of the operating system on
+which the executable runs, unless that component itself accompanies
+the executable.
+
+ It may happen that this requirement contradicts the license
+restrictions of other proprietary libraries that do not normally
+accompany the operating system. Such a contradiction means you cannot
+use both them and the Library together in an executable that you
+distribute.
+
+ 7. You may place library facilities that are a work based on the
+Library side-by-side in a single library together with other library
+facilities not covered by this License, and distribute such a combined
+library, provided that the separate distribution of the work based on
+the Library and of the other library facilities is otherwise
+permitted, and provided that you do these two things:
+
+ a) Accompany the combined library with a copy of the same work
+ based on the Library, uncombined with any other library
+ facilities. This must be distributed under the terms of the
+ Sections above.
+
+ b) Give prominent notice with the combined library of the fact
+ that part of it is a work based on the Library, and explaining
+ where to find the accompanying uncombined form of the same work.
+
+ 8. You may not copy, modify, sublicense, link with, or distribute
+the Library except as expressly provided under this License. Any
+attempt otherwise to copy, modify, sublicense, link with, or
+distribute the Library is void, and will automatically terminate your
+rights under this License. However, parties who have received copies,
+or rights, from you under this License will not have their licenses
+terminated so long as such parties remain in full compliance.
+
+ 9. You are not required to accept this License, since you have not
+signed it. However, nothing else grants you permission to modify or
+distribute the Library or its derivative works. These actions are
+prohibited by law if you do not accept this License. Therefore, by
+modifying or distributing the Library (or any work based on the
+Library), you indicate your acceptance of this License to do so, and
+all its terms and conditions for copying, distributing or modifying
+the Library or works based on it.
+
+ 10. Each time you redistribute the Library (or any work based on the
+Library), the recipient automatically receives a license from the
+original licensor to copy, distribute, link with or modify the Library
+subject to these terms and conditions. You may not impose any further
+restrictions on the recipients' exercise of the rights granted herein.
+You are not responsible for enforcing compliance by third parties with
+this License.
+
+ 11. If, as a consequence of a court judgment or allegation of patent
+infringement or for any other reason (not limited to patent issues),
+conditions are imposed on you (whether by court order, agreement or
+otherwise) that contradict the conditions of this License, they do not
+excuse you from the conditions of this License. If you cannot
+distribute so as to satisfy simultaneously your obligations under this
+License and any other pertinent obligations, then as a consequence you
+may not distribute the Library at all. For example, if a patent
+license would not permit royalty-free redistribution of the Library by
+all those who receive copies directly or indirectly through you, then
+the only way you could satisfy both it and this License would be to
+refrain entirely from distribution of the Library.
+
+If any portion of this section is held invalid or unenforceable under any
+particular circumstance, the balance of the section is intended to apply,
+and the section as a whole is intended to apply in other circumstances.
+
+It is not the purpose of this section to induce you to infringe any
+patents or other property right claims or to contest validity of any
+such claims; this section has the sole purpose of protecting the
+integrity of the free software distribution system which is
+implemented by public license practices. Many people have made
+generous contributions to the wide range of software distributed
+through that system in reliance on consistent application of that
+system; it is up to the author/donor to decide if he or she is willing
+to distribute software through any other system and a licensee cannot
+impose that choice.
+
+This section is intended to make thoroughly clear what is believed to
+be a consequence of the rest of this License.
+
+ 12. If the distribution and/or use of the Library is restricted in
+certain countries either by patents or by copyrighted interfaces, the
+original copyright holder who places the Library under this License may add
+an explicit geographical distribution limitation excluding those countries,
+so that distribution is permitted only in or among countries not thus
+excluded. In such case, this License incorporates the limitation as if
+written in the body of this License.
+
+ 13. The Free Software Foundation may publish revised and/or new
+versions of the Lesser General Public License from time to time.
+Such new versions will be similar in spirit to the present version,
+but may differ in detail to address new problems or concerns.
+
+Each version is given a distinguishing version number. If the Library
+specifies a version number of this License which applies to it and
+"any later version", you have the option of following the terms and
+conditions either of that version or of any later version published by
+the Free Software Foundation. If the Library does not specify a
+license version number, you may choose any version ever published by
+the Free Software Foundation.
+
+ 14. If you wish to incorporate parts of the Library into other free
+programs whose distribution conditions are incompatible with these,
+write to the author to ask for permission. For software which is
+copyrighted by the Free Software Foundation, write to the Free
+Software Foundation; we sometimes make exceptions for this. Our
+decision will be guided by the two goals of preserving the free status
+of all derivatives of our free software and of promoting the sharing
+and reuse of software generally.
+
+ NO WARRANTY
+
+ 15. BECAUSE THE LIBRARY IS LICENSED FREE OF CHARGE, THERE IS NO
+WARRANTY FOR THE LIBRARY, TO THE EXTENT PERMITTED BY APPLICABLE LAW.
+EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR
+OTHER PARTIES PROVIDE THE LIBRARY "AS IS" WITHOUT WARRANTY OF ANY
+KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
+PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE
+LIBRARY IS WITH YOU. SHOULD THE LIBRARY PROVE DEFECTIVE, YOU ASSUME
+THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
+
+ 16. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN
+WRITING WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY
+AND/OR REDISTRIBUTE THE LIBRARY AS PERMITTED ABOVE, BE LIABLE TO YOU
+FOR DAMAGES, INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR
+CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THE
+LIBRARY (INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA BEING
+RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD PARTIES OR A
+FAILURE OF THE LIBRARY TO OPERATE WITH ANY OTHER SOFTWARE), EVEN IF
+SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH
+DAMAGES.
+
+ END OF TERMS AND CONDITIONS
--
cgit v1.2.3
From ed3e5e036ee72f40ffca92775339dcc227d58f79 Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Mon, 1 Oct 2018 13:43:36 +0200
Subject: adapts to master on Oct. 1st 2018, but warnings remain
---
tuto1/src/g_tuto1.ml4 | 8 ++++----
tuto1/src/simple_declare.ml | 7 +++----
tuto1/src/simple_print.mli | 2 +-
tuto3/src/tuto_tactic.ml | 2 +-
4 files changed, 9 insertions(+), 10 deletions(-)
diff --git a/tuto1/src/g_tuto1.ml4 b/tuto1/src/g_tuto1.ml4
index b152583824..e171688083 100644
--- a/tuto1/src/g_tuto1.ml4
+++ b/tuto1/src/g_tuto1.ml4
@@ -21,10 +21,10 @@ END
VERNAC COMMAND EXTEND HelloAgain CLASSIFIED AS QUERY
| [ "HelloAgain" reference(r)] ->
-(* The function Libnames.pr_reference was found by searching all mli files
- for a function of type reference -> Pp.t *)
+(* The function Ppconstr.pr_qualid was found by searching all mli files
+ for a function of type qualid -> Pp.t *)
[ Feedback.msg_notice
- (strbrk "Hello again " ++ Libnames.pr_reference r)]
+ (strbrk "Hello again " ++ Ppconstr.pr_qualid r)]
END
(* According to parsing/pcoq.mli, e has type constr_expr *)
@@ -132,7 +132,7 @@ END
TACTIC EXTEND my_intro
| [ "my_intro" ident(i) ] ->
- [ Tactics.introduction ~check:false i]
+ [ Tactics.introduction i]
END
(* if one write this:
diff --git a/tuto1/src/simple_declare.ml b/tuto1/src/simple_declare.ml
index 5fd0b2e84b..10fa640548 100644
--- a/tuto1/src/simple_declare.ml
+++ b/tuto1/src/simple_declare.ml
@@ -1,11 +1,10 @@
let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook =
let open EConstr in
- let env = Global.env () in
let sigma = Evd.minimize_universes sigma in
let body = to_constr sigma body in
let tyopt = Option.map (to_constr sigma) tyopt in
let uvars_fold uvars c =
- Univ.LSet.union uvars (Univops.universes_of_constr env c) in
+ Univ.LSet.union uvars (Univops.universes_of_constr c) in
let uvars = List.fold_left uvars_fold Univ.LSet.empty
(Option.List.cons tyopt [body]) in
let sigma = Evd.restrict_universe_context sigma uvars in
@@ -19,8 +18,8 @@ let packed_declare_definition ident value_with_constraints =
let sigma = Evd.from_ctx ctx in
let k = (Decl_kinds.Global,
Flags.is_universe_polymorphism(), Decl_kinds.Definition) in
- let udecl = Univdecls.default_univ_decl in
+ let udecl = UState.default_univ_decl in
let nohook = Lemmas.mk_hook (fun _ x -> x) in
ignore (edeclare ident k ~opaque:false sigma udecl body None [] nohook)
-(* But this definition cannot be undone by Reset ident *)
\ No newline at end of file
+(* But this definition cannot be undone by Reset ident *)
diff --git a/tuto1/src/simple_print.mli b/tuto1/src/simple_print.mli
index c59316e84b..254b56ff79 100644
--- a/tuto1/src/simple_print.mli
+++ b/tuto1/src/simple_print.mli
@@ -1 +1 @@
-val simple_body_access : Globnames.global_reference -> Constr.constr
+val simple_body_access : Names.GlobRef.t -> Constr.constr
diff --git a/tuto3/src/tuto_tactic.ml b/tuto3/src/tuto_tactic.ml
index fbb6863f7e..3e926ad7f2 100644
--- a/tuto3/src/tuto_tactic.ml
+++ b/tuto3/src/tuto_tactic.ml
@@ -9,7 +9,7 @@ let collect_constants () =
if (!constants = []) then
let open Coqlib in
let open EConstr in
- let open Universes in
+ let open UnivGen in
let gr_H = find_reference "Tuto3" ["Tuto3"; "Data"] "pack" in
let gr_M = find_reference "Tuto3" ["Tuto3"; "Data"] "packer" in
let gr_R = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "pair" in
--
cgit v1.2.3
From d54cfa6a006002cafeee3aca684dcca5e88edb39 Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Mon, 1 Oct 2018 14:28:33 +0200
Subject: fix deprecation warnings
---
tuto3/src/tuto_tactic.ml | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/tuto3/src/tuto_tactic.ml b/tuto3/src/tuto_tactic.ml
index 3e926ad7f2..708b9c1877 100644
--- a/tuto3/src/tuto_tactic.ml
+++ b/tuto3/src/tuto_tactic.ml
@@ -56,7 +56,7 @@ let package i = Goal.enter begin fun gl ->
[(* this means that the applied theorem is not to be cleared. *)
None, (CAst.make (c_M (),
(* we don't specialize the theorem with extra values. *)
- Misctypes.NoBindings))]
+ Tactypes.NoBindings))]
(* we don't destruct the result according to any intro_pattern *)
None
end
@@ -140,5 +140,5 @@ let pack_tactic i =
else
tclTHEN (package i)
(tclTHEN (Tactics.rename_hyp [i, h_hyps_id])
- (Tactics.move_hyp h_hyps_id Misctypes.MoveLast))
+ (Tactics.move_hyp h_hyps_id Logic.MoveLast))
end
--
cgit v1.2.3
From 14b2976cdf67db788b79d9421ce1e89bd15c7313 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 11 Oct 2018 05:35:43 +0200
Subject: [coq] Adapt for PR #8704.
---
tuto1/src/simple_declare.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/tuto1/src/simple_declare.ml b/tuto1/src/simple_declare.ml
index 10fa640548..2737793d69 100644
--- a/tuto1/src/simple_declare.ml
+++ b/tuto1/src/simple_declare.ml
@@ -19,7 +19,7 @@ let packed_declare_definition ident value_with_constraints =
let k = (Decl_kinds.Global,
Flags.is_universe_polymorphism(), Decl_kinds.Definition) in
let udecl = UState.default_univ_decl in
- let nohook = Lemmas.mk_hook (fun _ x -> x) in
+ let nohook = Lemmas.mk_hook (fun _ x -> ()) in
ignore (edeclare ident k ~opaque:false sigma udecl body None [] nohook)
(* But this definition cannot be undone by Reset ident *)
--
cgit v1.2.3
From e3157aa44ba2ebec266e16ae0da78d735d21e779 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 12 Oct 2018 14:43:43 +0200
Subject: PR 8671: Remove store / goal extra argument
---
tuto3/src/tuto_tactic.ml | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
diff --git a/tuto3/src/tuto_tactic.ml b/tuto3/src/tuto_tactic.ml
index 708b9c1877..cb73a4486b 100644
--- a/tuto3/src/tuto_tactic.ml
+++ b/tuto3/src/tuto_tactic.ml
@@ -104,7 +104,6 @@ let get_type_of_hyp env id =
let repackage i h_hyps_id = Goal.enter begin fun gl ->
let env = Goal.env gl in
- let store = Goal.extra gl in
let evd = Tacmach.New.project gl in
let concl = Tacmach.New.pf_concl gl in
let (ty1 : EConstr.t) = get_type_of_hyp env i in
@@ -116,7 +115,7 @@ let repackage i h_hyps_id = Goal.enter begin fun gl ->
mkApp (c_R (), [| ty1; ty2; mkVar i;
mkApp (c_U (), [| ty2; mkVar h_hyps_id|]) |]) in
Refine.refine ~typecheck:true begin fun evd ->
- let evd, new_goal = Evarutil.new_evar env evd ~store
+ let evd, new_goal = Evarutil.new_evar env evd
(mkProd (Names.Name.Anonymous,
mkApp(c_H (), [| new_packed_type |]),
Vars.lift 1 concl)) in
--
cgit v1.2.3
From 3e71cbf27f18fc494caaea6a20631da5ef9e7d2b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 30 Oct 2018 11:55:27 +0100
Subject: Adapting to Coq PR #8718: declare_definition now takes a UState.t.
Also use new predefined Lemmas.no_kook.
---
tuto1/src/simple_declare.ml | 7 +++----
1 file changed, 3 insertions(+), 4 deletions(-)
diff --git a/tuto1/src/simple_declare.ml b/tuto1/src/simple_declare.ml
index 2737793d69..4130bab2f4 100644
--- a/tuto1/src/simple_declare.ml
+++ b/tuto1/src/simple_declare.ml
@@ -9,9 +9,9 @@ let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook =
(Option.List.cons tyopt [body]) in
let sigma = Evd.restrict_universe_context sigma uvars in
let univs = Evd.check_univ_decl ~poly sigma udecl in
- let ubinders = Evd.universe_binders sigma in
+ let ucontext = Evd.evar_universe_context sigma in
let ce = Declare.definition_entry ?types:tyopt ~univs body in
- DeclareDef.declare_definition ident k ce ubinders imps hook
+ DeclareDef.declare_definition ident k ce ucontext imps hook
let packed_declare_definition ident value_with_constraints =
let body, ctx = value_with_constraints in
@@ -19,7 +19,6 @@ let packed_declare_definition ident value_with_constraints =
let k = (Decl_kinds.Global,
Flags.is_universe_polymorphism(), Decl_kinds.Definition) in
let udecl = UState.default_univ_decl in
- let nohook = Lemmas.mk_hook (fun _ x -> ()) in
- ignore (edeclare ident k ~opaque:false sigma udecl body None [] nohook)
+ ignore (edeclare ident k ~opaque:false sigma udecl body None [] Lemmas.no_hook)
(* But this definition cannot be undone by Reset ident *)
--
cgit v1.2.3
From 58b9174b229863c694ad65984b86b112c689ae10 Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Wed, 31 Oct 2018 08:16:30 +0100
Subject: Revert "Merge pull request #13 from
herbelin/master+adapt-coq8718-declaration-hooks"
This reverts commit 9e8d0b077d8021e468ec0bc117438695c0b243bf, reversing
changes made to 56c3ae6296994cc288d4931110118617bb5bb978.
---
tuto1/src/simple_declare.ml | 7 ++++---
1 file changed, 4 insertions(+), 3 deletions(-)
diff --git a/tuto1/src/simple_declare.ml b/tuto1/src/simple_declare.ml
index 4130bab2f4..2737793d69 100644
--- a/tuto1/src/simple_declare.ml
+++ b/tuto1/src/simple_declare.ml
@@ -9,9 +9,9 @@ let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook =
(Option.List.cons tyopt [body]) in
let sigma = Evd.restrict_universe_context sigma uvars in
let univs = Evd.check_univ_decl ~poly sigma udecl in
- let ucontext = Evd.evar_universe_context sigma in
+ let ubinders = Evd.universe_binders sigma in
let ce = Declare.definition_entry ?types:tyopt ~univs body in
- DeclareDef.declare_definition ident k ce ucontext imps hook
+ DeclareDef.declare_definition ident k ce ubinders imps hook
let packed_declare_definition ident value_with_constraints =
let body, ctx = value_with_constraints in
@@ -19,6 +19,7 @@ let packed_declare_definition ident value_with_constraints =
let k = (Decl_kinds.Global,
Flags.is_universe_polymorphism(), Decl_kinds.Definition) in
let udecl = UState.default_univ_decl in
- ignore (edeclare ident k ~opaque:false sigma udecl body None [] Lemmas.no_hook)
+ let nohook = Lemmas.mk_hook (fun _ x -> ()) in
+ ignore (edeclare ident k ~opaque:false sigma udecl body None [] nohook)
(* But this definition cannot be undone by Reset ident *)
--
cgit v1.2.3
From e6c64a54f8f52ff555a0857a2909f5f70b22e591 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 16 Oct 2018 16:45:13 +0200
Subject: Fix for coq/coq#8515 (command driven attributes)
---
tuto1/src/g_tuto1.ml4 | 2 +-
tuto1/src/simple_declare.ml | 5 ++---
tuto1/src/simple_declare.mli | 2 +-
3 files changed, 4 insertions(+), 5 deletions(-)
diff --git a/tuto1/src/g_tuto1.ml4 b/tuto1/src/g_tuto1.ml4
index e171688083..1f4660d1f0 100644
--- a/tuto1/src/g_tuto1.ml4
+++ b/tuto1/src/g_tuto1.ml4
@@ -81,7 +81,7 @@ VERNAC COMMAND EXTEND Define1 CLASSIFIED AS SIDEFF
| [ "Cmd4" ident(i) constr(e) ] ->
[ let v = Constrintern.interp_constr (Global.env())
(Evd.from_env (Global.env())) e in
- Simple_declare.packed_declare_definition i v ]
+ Simple_declare.packed_declare_definition ~poly:(Attributes.(parse polymorphic atts)) i v ]
END
VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY
diff --git a/tuto1/src/simple_declare.ml b/tuto1/src/simple_declare.ml
index 2737793d69..af4dd5bddf 100644
--- a/tuto1/src/simple_declare.ml
+++ b/tuto1/src/simple_declare.ml
@@ -13,11 +13,10 @@ let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook =
let ce = Declare.definition_entry ?types:tyopt ~univs body in
DeclareDef.declare_definition ident k ce ubinders imps hook
-let packed_declare_definition ident value_with_constraints =
+let packed_declare_definition ~poly ident value_with_constraints =
let body, ctx = value_with_constraints in
let sigma = Evd.from_ctx ctx in
- let k = (Decl_kinds.Global,
- Flags.is_universe_polymorphism(), Decl_kinds.Definition) in
+ let k = (Decl_kinds.Global, poly, Decl_kinds.Definition) in
let udecl = UState.default_univ_decl in
let nohook = Lemmas.mk_hook (fun _ x -> ()) in
ignore (edeclare ident k ~opaque:false sigma udecl body None [] nohook)
diff --git a/tuto1/src/simple_declare.mli b/tuto1/src/simple_declare.mli
index 7a28626d88..fd74e81526 100644
--- a/tuto1/src/simple_declare.mli
+++ b/tuto1/src/simple_declare.mli
@@ -2,4 +2,4 @@ open Names
open EConstr
val packed_declare_definition :
- Id.t -> constr Evd.in_evar_universe_context -> unit
\ No newline at end of file
+ poly:bool -> Id.t -> constr Evd.in_evar_universe_context -> unit
--
cgit v1.2.3
From 0fe2b5d4d63bcbc63d48a386949094c23e4c274e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 31 Oct 2018 17:57:47 +0100
Subject: Port to coqpp.
---
tuto0/_CoqProject | 2 +-
tuto0/src/g_tuto0.ml4 | 14 --
tuto0/src/g_tuto0.mlg | 18 +++
tuto1/_CoqProject | 4 +-
tuto1/src/g_tuto1.ml4 | 149 --------------------
tuto1/src/g_tuto1.mlg | 154 +++++++++++++++++++++
tuto2/_CoqProject | 2 +-
tuto2/src/demo.ml4 | 347 ----------------------------------------------
tuto2/src/demo.mlg | 375 ++++++++++++++++++++++++++++++++++++++++++++++++++
tuto3/_CoqProject | 4 +-
tuto3/src/g_tuto3.ml4 | 42 ------
tuto3/src/g_tuto3.mlg | 46 +++++++
12 files changed, 599 insertions(+), 558 deletions(-)
delete mode 100644 tuto0/src/g_tuto0.ml4
create mode 100644 tuto0/src/g_tuto0.mlg
delete mode 100644 tuto1/src/g_tuto1.ml4
create mode 100644 tuto1/src/g_tuto1.mlg
delete mode 100644 tuto2/src/demo.ml4
create mode 100644 tuto2/src/demo.mlg
delete mode 100644 tuto3/src/g_tuto3.ml4
create mode 100644 tuto3/src/g_tuto3.mlg
diff --git a/tuto0/_CoqProject b/tuto0/_CoqProject
index dd93e1fa79..76368e3ac7 100644
--- a/tuto0/_CoqProject
+++ b/tuto0/_CoqProject
@@ -6,5 +6,5 @@ theories/Demo.v
src/tuto0_main.ml
src/tuto0_main.mli
-src/g_tuto0.ml4
+src/g_tuto0.mlg
src/tuto0_plugin.mlpack
diff --git a/tuto0/src/g_tuto0.ml4 b/tuto0/src/g_tuto0.ml4
deleted file mode 100644
index d6e95ba0f7..0000000000
--- a/tuto0/src/g_tuto0.ml4
+++ /dev/null
@@ -1,14 +0,0 @@
-DECLARE PLUGIN "tuto0_plugin"
-
-open Pp
-open Ltac_plugin
-
-VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY
-| [ "HelloWorld" ] -> [ Feedback.msg_notice (strbrk Tuto0_main.message) ]
-END
-
-TACTIC EXTEND hello_world_tactic
-| [ "hello_world" ] ->
- [ let _ = Feedback.msg_notice (str Tuto0_main.message) in
- Tacticals.New.tclIDTAC ]
-END
diff --git a/tuto0/src/g_tuto0.mlg b/tuto0/src/g_tuto0.mlg
new file mode 100644
index 0000000000..5c633fe862
--- /dev/null
+++ b/tuto0/src/g_tuto0.mlg
@@ -0,0 +1,18 @@
+DECLARE PLUGIN "tuto0_plugin"
+
+{
+
+open Pp
+open Ltac_plugin
+
+}
+
+VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY
+| [ "HelloWorld" ] -> { Feedback.msg_notice (strbrk Tuto0_main.message) }
+END
+
+TACTIC EXTEND hello_world_tactic
+| [ "hello_world" ] ->
+ { let _ = Feedback.msg_notice (str Tuto0_main.message) in
+ Tacticals.New.tclIDTAC }
+END
diff --git a/tuto1/_CoqProject b/tuto1/_CoqProject
index ce14ee2b87..585d1360be 100644
--- a/tuto1/_CoqProject
+++ b/tuto1/_CoqProject
@@ -9,5 +9,5 @@ src/simple_declare.mli
src/simple_declare.ml
src/simple_print.ml
src/simple_print.mli
-src/g_tuto1.ml4
-src/tuto1_plugin.mlpack
\ No newline at end of file
+src/g_tuto1.mlg
+src/tuto1_plugin.mlpack
diff --git a/tuto1/src/g_tuto1.ml4 b/tuto1/src/g_tuto1.ml4
deleted file mode 100644
index 1f4660d1f0..0000000000
--- a/tuto1/src/g_tuto1.ml4
+++ /dev/null
@@ -1,149 +0,0 @@
-DECLARE PLUGIN "tuto1_plugin"
-
-(* If we forget this line and include our own tactic definition using
- TACTIC EXTEND, as below, then we get the strange error message
- no implementation available for Tacentries, only when compiling
- theories/Loader.v
-*)
-open Ltac_plugin
-open Pp
-(* This module defines the types of arguments to be used in the
- EXTEND directives below, for example the string one. *)
-open Stdarg
-
-VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY
-| [ "Hello" string(s) ] ->
- [ Feedback.msg_notice (strbrk "Hello " ++ str s) ]
-END
-
-(* reference is allowed as a syntactic entry, but so are all the entries
- found the signature of module Prim in file coq/parsing/pcoq.mli *)
-
-VERNAC COMMAND EXTEND HelloAgain CLASSIFIED AS QUERY
-| [ "HelloAgain" reference(r)] ->
-(* The function Ppconstr.pr_qualid was found by searching all mli files
- for a function of type qualid -> Pp.t *)
- [ Feedback.msg_notice
- (strbrk "Hello again " ++ Ppconstr.pr_qualid r)]
-END
-
-(* According to parsing/pcoq.mli, e has type constr_expr *)
-(* this type is defined in pretyping/constrexpr.ml *)
-(* Question for the developers: why is the file constrexpr.ml and not
- constrexpr.mli --> Easier for packing the software in components. *)
-VERNAC COMMAND EXTEND TakingConstr CLASSIFIED AS QUERY
-| [ "Cmd1" constr(e) ] ->
- [ let _ = e in Feedback.msg_notice (strbrk "Cmd1 parsed something") ]
-END
-
-(* The next step is to make something of parsed expression.
- Interesting information in interp/constrintern.mli *)
-
-(* There are several phases of transforming a parsed expression into
- the final internal data-type (constr). There exists a collection of
- functions that combine all the phases *)
-
-VERNAC COMMAND EXTEND TakingConstr2 CLASSIFIED AS QUERY
-| [ "Cmd2" constr(e) ] ->
- [ let _ = Constrintern.interp_constr
- (Global.env())
- (* Make sure you don't use Evd.empty here, as this does not
- check consistency with existing universe constraints. *)
- (Evd.from_env (Global.env())) e in
- Feedback.msg_notice (strbrk "Cmd2 parsed something legitimate") ]
-END
-
-(* This is to show what happens when typing in an empty environment
- with an empty evd.
- Question for the developers: why does "Cmd3 (fun x : nat => x)."
- raise an anomaly, not the same error as "Cmd3 (fun x : a => x)." *)
-
-VERNAC COMMAND EXTEND TakingConstr3 CLASSIFIED AS QUERY
-| [ "Cmd3" constr(e) ] ->
- [ let _ = Constrintern.interp_constr Environ.empty_env
- Evd.empty e in
- Feedback.msg_notice
- (strbrk "Cmd3 accepted something in the empty context")]
-END
-
-(* When adding a definition, we have to be careful that just
- the operation of constructing a well-typed term may already change
- the environment, at the level of universe constraints (which
- are recorded in the evd component). The function
- Constrintern.interp_constr ignores this side-effect, so it should
- not be used here. *)
-
-(* Looking at the interface file interp/constrintern.ml4, I lost
- some time because I did not see that the "constr" type appearing
- there was "EConstr.constr" and not "Constr.constr". *)
-
-VERNAC COMMAND EXTEND Define1 CLASSIFIED AS SIDEFF
-| [ "Cmd4" ident(i) constr(e) ] ->
- [ let v = Constrintern.interp_constr (Global.env())
- (Evd.from_env (Global.env())) e in
- Simple_declare.packed_declare_definition ~poly:(Attributes.(parse polymorphic atts)) i v ]
-END
-
-VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY
-| [ "Cmd5" constr(e) ] ->
- [ let v = Constrintern.interp_constr (Global.env())
- (Evd.from_env (Global.env())) e in
- let (_, ctx) = v in
- let evd = Evd.from_ctx ctx in
- Feedback.msg_notice
- (Printer.pr_econstr_env (Global.env()) evd
- (Simple_check.simple_check1 v)) ]
-END
-
-VERNAC COMMAND EXTEND Check2 CLASSIFIED AS QUERY
-| [ "Cmd6" constr(e) ] ->
- [ let v = Constrintern.interp_constr (Global.env())
- (Evd.from_env (Global.env())) e in
- let evd, ty = Simple_check.simple_check2 v in
- Feedback.msg_notice
- (Printer.pr_econstr_env (Global.env()) evd ty) ]
-END
-
-VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY
-| [ "Cmd7" constr(e) ] ->
- [ let v = Constrintern.interp_constr (Global.env())
- (Evd.from_env (Global.env())) e in
- let (a, ctx) = v in
- let evd = Evd.from_ctx ctx in
- Feedback.msg_notice
- (Printer.pr_econstr_env (Global.env()) evd
- (Simple_check.simple_check3 v)) ]
-END
-
-(* This command takes a name and return its value. It does less
- than Print, because it fails on constructors, axioms, and inductive types.
- This should be improved, because the error message is an anomaly.
- Anomalies should never appear even when using a command outside of its
- intended use. *)
-VERNAC COMMAND EXTEND ExamplePrint CLASSIFIED AS QUERY
-| [ "Cmd8" reference(r) ] ->
- [ let env = Global.env() in
- let evd = Evd.from_env env in
- Feedback.msg_notice
- (Printer.pr_econstr_env env evd
- (EConstr.of_constr
- (Simple_print.simple_body_access (Nametab.global r)))) ]
-END
-
-TACTIC EXTEND my_intro
-| [ "my_intro" ident(i) ] ->
- [ Tactics.introduction i]
-END
-
-(* if one write this:
- VERNAC COMMAND EXTEND exploreproof CLASSIFIED AS QUERY
- it gives an error message that is basically impossible to understand. *)
-
-VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY
-| [ "Cmd9" ] ->
- [ let p = Proof_global.give_me_the_proof () in
- let sigma, env = Pfedit.get_current_context () in
- let pprf = Proof.partial_proof p in
- Feedback.msg_notice
- (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf) ]
-END
diff --git a/tuto1/src/g_tuto1.mlg b/tuto1/src/g_tuto1.mlg
new file mode 100644
index 0000000000..4df284d2d9
--- /dev/null
+++ b/tuto1/src/g_tuto1.mlg
@@ -0,0 +1,154 @@
+DECLARE PLUGIN "tuto1_plugin"
+
+{
+
+(* If we forget this line and include our own tactic definition using
+ TACTIC EXTEND, as below, then we get the strange error message
+ no implementation available for Tacentries, only when compiling
+ theories/Loader.v
+*)
+open Ltac_plugin
+open Attributes
+open Pp
+(* This module defines the types of arguments to be used in the
+ EXTEND directives below, for example the string one. *)
+open Stdarg
+
+}
+
+VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY
+| [ "Hello" string(s) ] ->
+ { Feedback.msg_notice (strbrk "Hello " ++ str s) }
+END
+
+(* reference is allowed as a syntactic entry, but so are all the entries
+ found the signature of module Prim in file coq/parsing/pcoq.mli *)
+
+VERNAC COMMAND EXTEND HelloAgain CLASSIFIED AS QUERY
+| [ "HelloAgain" reference(r)] ->
+(* The function Ppconstr.pr_qualid was found by searching all mli files
+ for a function of type qualid -> Pp.t *)
+ { Feedback.msg_notice
+ (strbrk "Hello again " ++ Ppconstr.pr_qualid r)}
+END
+
+(* According to parsing/pcoq.mli, e has type constr_expr *)
+(* this type is defined in pretyping/constrexpr.ml *)
+(* Question for the developers: why is the file constrexpr.ml and not
+ constrexpr.mli --> Easier for packing the software in components. *)
+VERNAC COMMAND EXTEND TakingConstr CLASSIFIED AS QUERY
+| [ "Cmd1" constr(e) ] ->
+ { let _ = e in Feedback.msg_notice (strbrk "Cmd1 parsed something") }
+END
+
+(* The next step is to make something of parsed expression.
+ Interesting information in interp/constrintern.mli *)
+
+(* There are several phases of transforming a parsed expression into
+ the final internal data-type (constr). There exists a collection of
+ functions that combine all the phases *)
+
+VERNAC COMMAND EXTEND TakingConstr2 CLASSIFIED AS QUERY
+| [ "Cmd2" constr(e) ] ->
+ { let _ = Constrintern.interp_constr
+ (Global.env())
+ (* Make sure you don't use Evd.empty here, as this does not
+ check consistency with existing universe constraints. *)
+ (Evd.from_env (Global.env())) e in
+ Feedback.msg_notice (strbrk "Cmd2 parsed something legitimate") }
+END
+
+(* This is to show what happens when typing in an empty environment
+ with an empty evd.
+ Question for the developers: why does "Cmd3 (fun x : nat => x)."
+ raise an anomaly, not the same error as "Cmd3 (fun x : a => x)." *)
+
+VERNAC COMMAND EXTEND TakingConstr3 CLASSIFIED AS QUERY
+| [ "Cmd3" constr(e) ] ->
+ { let _ = Constrintern.interp_constr Environ.empty_env
+ Evd.empty e in
+ Feedback.msg_notice
+ (strbrk "Cmd3 accepted something in the empty context")}
+END
+
+(* When adding a definition, we have to be careful that just
+ the operation of constructing a well-typed term may already change
+ the environment, at the level of universe constraints (which
+ are recorded in the evd component). The function
+ Constrintern.interp_constr ignores this side-effect, so it should
+ not be used here. *)
+
+(* Looking at the interface file interp/constrintern.ml4, I lost
+ some time because I did not see that the "constr" type appearing
+ there was "EConstr.constr" and not "Constr.constr". *)
+
+VERNAC COMMAND EXTEND Define1 CLASSIFIED AS SIDEFF
+| #[ poly = polymorphic ] [ "Cmd4" ident(i) constr(e) ] ->
+ { let v = Constrintern.interp_constr (Global.env())
+ (Evd.from_env (Global.env())) e in
+ Simple_declare.packed_declare_definition ~poly i v }
+END
+
+VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY
+| [ "Cmd5" constr(e) ] ->
+ { let v = Constrintern.interp_constr (Global.env())
+ (Evd.from_env (Global.env())) e in
+ let (_, ctx) = v in
+ let evd = Evd.from_ctx ctx in
+ Feedback.msg_notice
+ (Printer.pr_econstr_env (Global.env()) evd
+ (Simple_check.simple_check1 v)) }
+END
+
+VERNAC COMMAND EXTEND Check2 CLASSIFIED AS QUERY
+| [ "Cmd6" constr(e) ] ->
+ { let v = Constrintern.interp_constr (Global.env())
+ (Evd.from_env (Global.env())) e in
+ let evd, ty = Simple_check.simple_check2 v in
+ Feedback.msg_notice
+ (Printer.pr_econstr_env (Global.env()) evd ty) }
+END
+
+VERNAC COMMAND EXTEND Check1 CLASSIFIED AS QUERY
+| [ "Cmd7" constr(e) ] ->
+ { let v = Constrintern.interp_constr (Global.env())
+ (Evd.from_env (Global.env())) e in
+ let (a, ctx) = v in
+ let evd = Evd.from_ctx ctx in
+ Feedback.msg_notice
+ (Printer.pr_econstr_env (Global.env()) evd
+ (Simple_check.simple_check3 v)) }
+END
+
+(* This command takes a name and return its value. It does less
+ than Print, because it fails on constructors, axioms, and inductive types.
+ This should be improved, because the error message is an anomaly.
+ Anomalies should never appear even when using a command outside of its
+ intended use. *)
+VERNAC COMMAND EXTEND ExamplePrint CLASSIFIED AS QUERY
+| [ "Cmd8" reference(r) ] ->
+ { let env = Global.env() in
+ let evd = Evd.from_env env in
+ Feedback.msg_notice
+ (Printer.pr_econstr_env env evd
+ (EConstr.of_constr
+ (Simple_print.simple_body_access (Nametab.global r)))) }
+END
+
+TACTIC EXTEND my_intro
+| [ "my_intro" ident(i) ] ->
+ { Tactics.introduction i }
+END
+
+(* if one write this:
+ VERNAC COMMAND EXTEND exploreproof CLASSIFIED AS QUERY
+ it gives an error message that is basically impossible to understand. *)
+
+VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY
+| [ "Cmd9" ] ->
+ { let p = Proof_global.give_me_the_proof () in
+ let sigma, env = Pfedit.get_current_context () in
+ let pprf = Proof.partial_proof p in
+ Feedback.msg_notice
+ (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf) }
+END
diff --git a/tuto2/_CoqProject b/tuto2/_CoqProject
index bdafdb5f04..cf9cb5cc26 100644
--- a/tuto2/_CoqProject
+++ b/tuto2/_CoqProject
@@ -2,5 +2,5 @@
-I src
theories/Test.v
-src/demo.ml4
+src/demo.mlg
src/demo_plugin.mlpack
diff --git a/tuto2/src/demo.ml4 b/tuto2/src/demo.ml4
deleted file mode 100644
index 981d41fa5c..0000000000
--- a/tuto2/src/demo.ml4
+++ /dev/null
@@ -1,347 +0,0 @@
-(* -------------------------------------------------------------------------- *)
-(* *)
-(* Initial ritual dance *)
-(* *)
-(* -------------------------------------------------------------------------- *)
-
-DECLARE PLUGIN "demo_plugin"
-
-(*
- 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_plugin".
- 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_plugin".
-
- (2) The above command will succeed only if there is "demo_plugin.cmxs"
- in some of the directories that Coq is supposed to look
- (i.e. the ones we specified via "-I ..." command line options).
-
- (3) The file "demo_plugin.mlpack" lists the OCaml modules to be linked in
- "demo_plugin.cmxs".
-
- (4) The file "demo_plugin.mlpack" as well as all .ml, .mli and .ml4 files
- are listed in the "_CoqProject" file.
-*)
-
-(* -------------------------------------------------------------------------- *)
-(* *)
-(* 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/demo.mlg b/tuto2/src/demo.mlg
new file mode 100644
index 0000000000..966c05acdc
--- /dev/null
+++ b/tuto2/src/demo.mlg
@@ -0,0 +1,375 @@
+(* -------------------------------------------------------------------------- *)
+(* *)
+(* Initial ritual dance *)
+(* *)
+(* -------------------------------------------------------------------------- *)
+
+DECLARE PLUGIN "demo_plugin"
+
+(*
+ 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_plugin".
+ 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_plugin".
+
+ (2) The above command will succeed only if there is "demo_plugin.cmxs"
+ in some of the directories that Coq is supposed to look
+ (i.e. the ones we specified via "-I ..." command line options).
+
+ (3) The file "demo_plugin.mlpack" lists the OCaml modules to be linked in
+ "demo_plugin.cmxs".
+
+ (4) The file "demo_plugin.mlpack" as well as all .ml, .mli and .mlg files
+ are listed in the "_CoqProject" file.
+*)
+
+(* -------------------------------------------------------------------------- *)
+(* *)
+(* 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:
+
+ { () }
+
+ Similarly to the 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/tuto3/_CoqProject b/tuto3/_CoqProject
index 6a3c1978a7..e2a60a430f 100644
--- a/tuto3/_CoqProject
+++ b/tuto3/_CoqProject
@@ -8,5 +8,5 @@ src/tuto_tactic.ml
src/tuto_tactic.mli
src/construction_game.ml
src/construction_game.mli
-src/g_tuto3.ml4
-src/tuto3_plugin.mlpack
\ No newline at end of file
+src/g_tuto3.mlg
+src/tuto3_plugin.mlpack
diff --git a/tuto3/src/g_tuto3.ml4 b/tuto3/src/g_tuto3.ml4
deleted file mode 100644
index 71c6be16c8..0000000000
--- a/tuto3/src/g_tuto3.ml4
+++ /dev/null
@@ -1,42 +0,0 @@
-DECLARE PLUGIN "tuto3_plugin"
-
-open Ltac_plugin
-
-open Construction_game
-
-(* This one is necessary, to avoid message about missing wit_string *)
-open Stdarg
-
-VERNAC COMMAND EXTEND ShowTypeConstruction CLASSIFIED AS QUERY
-| [ "Tuto3_1" ] ->
- [ let env = Global.env () in
- let evd = Evd.from_env env in
- let evd, s = Evd.new_sort_variable Evd.univ_rigid evd in
- let new_type_2 = EConstr.mkSort s in
- let evd, _ =
- Typing.type_of (Global.env()) (Evd.from_env (Global.env())) new_type_2 in
- Feedback.msg_notice
- (Printer.pr_econstr_env env evd new_type_2) ]
-END
-
-VERNAC COMMAND EXTEND ShowOneConstruction CLASSIFIED AS QUERY
-| [ "Tuto3_2" ] -> [ example_sort_app_lambda () ]
-END
-
-TACTIC EXTEND collapse_hyps
-| [ "pack" "hypothesis" ident(i) ] ->
- [ Tuto_tactic.pack_tactic i ]
-END
-
-(* More advanced examples, where automatic proof happens but
- no tactic is being called explicitely. The first one uses
- type classes. *)
-VERNAC COMMAND EXTEND TriggerClasses CLASSIFIED AS QUERY
-| [ "Tuto3_3" int(n) ] -> [ example_classes n ]
-END
-
-(* The second one uses canonical structures. *)
-VERNAC COMMAND EXTEND TriggerCanonical CLASSIFIED AS QUERY
-| [ "Tuto3_4" int(n) ] -> [ example_canonical n ]
-END
-
diff --git a/tuto3/src/g_tuto3.mlg b/tuto3/src/g_tuto3.mlg
new file mode 100644
index 0000000000..82ba45726e
--- /dev/null
+++ b/tuto3/src/g_tuto3.mlg
@@ -0,0 +1,46 @@
+DECLARE PLUGIN "tuto3_plugin"
+
+{
+
+open Ltac_plugin
+
+open Construction_game
+
+(* This one is necessary, to avoid message about missing wit_string *)
+open Stdarg
+
+}
+
+VERNAC COMMAND EXTEND ShowTypeConstruction CLASSIFIED AS QUERY
+| [ "Tuto3_1" ] ->
+ { let env = Global.env () in
+ let evd = Evd.from_env env in
+ let evd, s = Evd.new_sort_variable Evd.univ_rigid evd in
+ let new_type_2 = EConstr.mkSort s in
+ let evd, _ =
+ Typing.type_of (Global.env()) (Evd.from_env (Global.env())) new_type_2 in
+ Feedback.msg_notice
+ (Printer.pr_econstr_env env evd new_type_2) }
+END
+
+VERNAC COMMAND EXTEND ShowOneConstruction CLASSIFIED AS QUERY
+| [ "Tuto3_2" ] -> { example_sort_app_lambda () }
+END
+
+TACTIC EXTEND collapse_hyps
+| [ "pack" "hypothesis" ident(i) ] ->
+ { Tuto_tactic.pack_tactic i }
+END
+
+(* More advanced examples, where automatic proof happens but
+ no tactic is being called explicitely. The first one uses
+ type classes. *)
+VERNAC COMMAND EXTEND TriggerClasses CLASSIFIED AS QUERY
+| [ "Tuto3_3" int(n) ] -> { example_classes n }
+END
+
+(* The second one uses canonical structures. *)
+VERNAC COMMAND EXTEND TriggerCanonical CLASSIFIED AS QUERY
+| [ "Tuto3_4" int(n) ] -> { example_canonical n }
+END
+
--
cgit v1.2.3
From 9e5447b196804fd9ce754931e21802e5d02031d9 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 6 Nov 2018 12:23:12 +0100
Subject: [travis] Add Travis File.
We only test dev for master.
---
.travis.yml | 38 ++++++++++++++++++++++++++++++++++++++
1 file changed, 38 insertions(+)
create mode 100644 .travis.yml
diff --git a/.travis.yml b/.travis.yml
new file mode 100644
index 0000000000..556e0ac45a
--- /dev/null
+++ b/.travis.yml
@@ -0,0 +1,38 @@
+dist: trusty
+sudo: required
+language: generic
+
+services:
+ - docker
+
+env:
+ global:
+ - NJOBS="2"
+ - CONTRIB_NAME="plugin_tutorials"
+ matrix:
+ - COQ_IMAGE="coqorg/coq:dev"
+
+install: |
+ # Prepare the COQ container
+ docker run -d -i --init --name=COQ -v ${TRAVIS_BUILD_DIR}:/home/coq/$CONTRIB_NAME -w /home/coq/$CONTRIB_NAME ${COQ_IMAGE}
+ docker exec COQ /bin/bash --login -c "
+ # This bash script is double-quoted to interpolate Travis CI env vars:
+ echo \"Build triggered by ${TRAVIS_EVENT_TYPE}\"
+ export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m '
+ set -ex # -e = exit on failure; -x = trace for debug
+ opam list
+ "
+script:
+- echo -e "${ANSI_YELLOW}Building $CONTRIB_NAME...${ANSI_RESET}" && echo -en 'travis_fold:start:testbuild\\r'
+- |
+ docker exec COQ /bin/bash --login -c "
+ export PS4='+ \e[33;1m(\$0 @ line \$LINENO) \$\e[0m '
+ set -ex
+ sudo chown -R coq:coq /home/coq/$CONTRIB_NAME
+ ( cd tuto0 && make )
+ ( cd tuto1 && make )
+ ( cd tuto2 && make )
+ ( cd tuto3 && make )
+ "
+- docker stop COQ # optional
+- echo -en 'travis_fold:end:testbuild\\r'
--
cgit v1.2.3
From b39a7c75a9d90b0fa4446fcefd6708d32271dad2 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 7 Nov 2018 01:21:25 +0100
Subject: [dune] Add support for building with Dune for the ML part.
This allows to drop the plugin_tutorials in the coq tree and have the
build compose.
---
.gitignore | 1 +
tuto0/src/dune | 9 +++++++++
tuto1/src/dune | 9 +++++++++
tuto2/src/dune | 9 +++++++++
tuto3/src/dune | 9 +++++++++
5 files changed, 37 insertions(+)
create mode 100644 tuto0/src/dune
create mode 100644 tuto1/src/dune
create mode 100644 tuto2/src/dune
create mode 100644 tuto3/src/dune
diff --git a/.gitignore b/.gitignore
index be4ea26f86..6efd03647c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -7,3 +7,4 @@ Makefile.coq*
*.vo
*.glob
*.aux
+*/*/.merlin
diff --git a/tuto0/src/dune b/tuto0/src/dune
new file mode 100644
index 0000000000..79d561061d
--- /dev/null
+++ b/tuto0/src/dune
@@ -0,0 +1,9 @@
+(library
+ (name tuto0_plugin)
+ (public_name coq.plugins.tutorial.p0)
+ (libraries coq.plugins.ltac))
+
+(rule
+ (targets g_tuto0.ml)
+ (deps (:pp-file g_tuto0.mlg) )
+ (action (run coqpp %{pp-file})))
diff --git a/tuto1/src/dune b/tuto1/src/dune
new file mode 100644
index 0000000000..cf9c674b14
--- /dev/null
+++ b/tuto1/src/dune
@@ -0,0 +1,9 @@
+(library
+ (name tuto1_plugin)
+ (public_name coq.plugins.tutorial.p1)
+ (libraries coq.plugins.ltac))
+
+(rule
+ (targets g_tuto1.ml)
+ (deps (:pp-file g_tuto1.mlg) )
+ (action (run coqpp %{pp-file})))
diff --git a/tuto2/src/dune b/tuto2/src/dune
new file mode 100644
index 0000000000..f2bc405455
--- /dev/null
+++ b/tuto2/src/dune
@@ -0,0 +1,9 @@
+(library
+ (name tuto2_plugin)
+ (public_name coq.plugins.tutorial.p2)
+ (libraries coq.plugins.ltac))
+
+(rule
+ (targets demo.ml)
+ (deps (:pp-file demo.mlg) )
+ (action (run coqpp %{pp-file})))
diff --git a/tuto3/src/dune b/tuto3/src/dune
new file mode 100644
index 0000000000..6b09d5d98b
--- /dev/null
+++ b/tuto3/src/dune
@@ -0,0 +1,9 @@
+(library
+ (name tuto3_plugin)
+ (public_name coq.plugins.tutorial.p3)
+ (libraries coq.plugins.ltac))
+
+(rule
+ (targets g_tuto3.ml)
+ (deps (:pp-file g_tuto3.mlg))
+ (action (run coqpp %{pp-file})))
--
cgit v1.2.3
From 6cc40e73879aec50227c9576100a381cc11ade30 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 7 Nov 2018 13:55:14 +0100
Subject: [warnings] Fix couple of warnings related to API..
Changes in declare following @SkySkimmer's advice.
---
tuto1/src/simple_declare.ml | 8 ++++----
tuto3/src/tuto_tactic.ml | 2 +-
2 files changed, 5 insertions(+), 5 deletions(-)
diff --git a/tuto1/src/simple_declare.ml b/tuto1/src/simple_declare.ml
index af4dd5bddf..50fd170663 100644
--- a/tuto1/src/simple_declare.ml
+++ b/tuto1/src/simple_declare.ml
@@ -1,10 +1,10 @@
+(* Ideally coq/coq#8811 would get merged and then this function could be much simpler. *)
let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook =
- let open EConstr in
let sigma = Evd.minimize_universes sigma in
- let body = to_constr sigma body in
- let tyopt = Option.map (to_constr sigma) tyopt in
+ let body = EConstr.to_constr sigma body in
+ let tyopt = Option.map (EConstr.to_constr sigma) tyopt in
let uvars_fold uvars c =
- Univ.LSet.union uvars (Univops.universes_of_constr c) in
+ Univ.LSet.union uvars (Vars.universes_of_constr c) in
let uvars = List.fold_left uvars_fold Univ.LSet.empty
(Option.List.cons tyopt [body]) in
let sigma = Evd.restrict_universe_context sigma uvars in
diff --git a/tuto3/src/tuto_tactic.ml b/tuto3/src/tuto_tactic.ml
index cb73a4486b..9818867621 100644
--- a/tuto3/src/tuto_tactic.ml
+++ b/tuto3/src/tuto_tactic.ml
@@ -15,7 +15,7 @@ let collect_constants () =
let gr_R = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "pair" in
let gr_P = find_reference "Tuto3" ["Coq"; "Init"; "Datatypes"] "prod" in
let gr_U = find_reference "Tuto3" ["Tuto3"; "Data"] "uncover" in
- constants := List.map (fun x -> of_constr (constr_of_global x))
+ constants := List.map (fun x -> of_constr (constr_of_monomorphic_global x))
[gr_H; gr_M; gr_R; gr_P; gr_U];
!constants
else
--
cgit v1.2.3
From 01a673e8d8e22e7aaebe5dc4e801d36ce29941b7 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 9 Nov 2018 15:58:52 +0100
Subject: Adapt to coq/coq#8933 (Make initial evar map argument to
check_evars_are_solved optional)
---
tuto3/src/construction_game.ml | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/tuto3/src/construction_game.ml b/tuto3/src/construction_game.ml
index 831349c8cc..22b02f6893 100644
--- a/tuto3/src/construction_game.ml
+++ b/tuto3/src/construction_game.ml
@@ -136,7 +136,7 @@ let example_classes n =
(* Question to coq developers: why do we pass two evd arguments to
solve_remaining_evars? Is the choice of evd0 relevant here? *)
let evd = Pretyping.solve_remaining_evars
- (Pretyping.default_inference_flags true) env evd evd0 in
+ (Pretyping.default_inference_flags true) env evd ~initial:evd0 in
let evd, final_type = Typing.type_of env evd proved_equality in
Feedback.msg_notice (Printer.pr_econstr_env env evd proved_equality)
--
cgit v1.2.3
From 5e5817678b8678997a479f5585ed5e6373da8559 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 9 Nov 2018 16:00:28 +0100
Subject: Add .cmt and generated ml files to gitignore
---
.gitignore | 5 ++++-
tuto2/src/.gitignore | 1 +
2 files changed, 5 insertions(+), 1 deletion(-)
create mode 100644 tuto2/src/.gitignore
diff --git a/.gitignore b/.gitignore
index 6efd03647c..3e4978fac4 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,5 +1,5 @@
*.ml*.d
-*.cm[ix]*
+*.cm[ixt]*
Makefile.coq*
*~
*.[ao]
@@ -8,3 +8,6 @@ Makefile.coq*
*.glob
*.aux
*/*/.merlin
+
+# by convention g_foo.ml is generated
+g_*.ml
diff --git a/tuto2/src/.gitignore b/tuto2/src/.gitignore
new file mode 100644
index 0000000000..5b1b6a902e
--- /dev/null
+++ b/tuto2/src/.gitignore
@@ -0,0 +1 @@
+/demo.ml
--
cgit v1.2.3
From df40307f70d7a03b03af7ae4360a15349abc1bd0 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 28 Nov 2018 02:47:20 +0100
Subject: [coq overlay] Adapt to coq/coq#8705
Please apply when indicated.
---
tuto1/src/simple_declare.ml | 2 +-
tuto3/src/dune | 1 +
2 files changed, 2 insertions(+), 1 deletion(-)
diff --git a/tuto1/src/simple_declare.ml b/tuto1/src/simple_declare.ml
index 50fd170663..9d10a8ba72 100644
--- a/tuto1/src/simple_declare.ml
+++ b/tuto1/src/simple_declare.ml
@@ -11,7 +11,7 @@ let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook =
let univs = Evd.check_univ_decl ~poly sigma udecl in
let ubinders = Evd.universe_binders sigma in
let ce = Declare.definition_entry ?types:tyopt ~univs body in
- DeclareDef.declare_definition ident k ce ubinders imps hook
+ DeclareDef.declare_definition ident k ce ubinders imps ~hook
let packed_declare_definition ~poly ident value_with_constraints =
let body, ctx = value_with_constraints in
diff --git a/tuto3/src/dune b/tuto3/src/dune
index 6b09d5d98b..ba6d8b288f 100644
--- a/tuto3/src/dune
+++ b/tuto3/src/dune
@@ -1,6 +1,7 @@
(library
(name tuto3_plugin)
(public_name coq.plugins.tutorial.p3)
+ (flags :standard -warn-error -3)
(libraries coq.plugins.ltac))
(rule
--
cgit v1.2.3
From d139debf0ea444c5dd7b654a5d2c47c2d9bec534 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 20 Dec 2018 18:34:24 +0100
Subject: Relicense to Unlicense
This was agreed during the 2018-12-19 Coq Working Group.
See eg https://github.com/coq/coq/pull/8778#issuecomment-448932003
Close #7.
---
LICENSE | 482 ++++------------------------------------------------------------
1 file changed, 24 insertions(+), 458 deletions(-)
diff --git a/LICENSE b/LICENSE
index 27950e8d20..cf1ab25da0 100644
--- a/LICENSE
+++ b/LICENSE
@@ -1,458 +1,24 @@
- GNU LESSER GENERAL PUBLIC LICENSE
- Version 2.1, February 1999
-
- Copyright (C) 1991, 1999 Free Software Foundation, Inc.
- 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
- Everyone is permitted to copy and distribute verbatim copies
- of this license document, but changing it is not allowed.
-
-[This is the first released version of the Lesser GPL. It also counts
- as the successor of the GNU Library Public License, version 2, hence
- the version number 2.1.]
-
- Preamble
-
- The licenses for most software are designed to take away your
-freedom to share and change it. By contrast, the GNU General Public
-Licenses are intended to guarantee your freedom to share and change
-free software--to make sure the software is free for all its users.
-
- This license, the Lesser General Public License, applies to some
-specially designated software packages--typically libraries--of the
-Free Software Foundation and other authors who decide to use it. You
-can use it too, but we suggest you first think carefully about whether
-this license or the ordinary General Public License is the better
-strategy to use in any particular case, based on the explanations below.
-
- When we speak of free software, we are referring to freedom of use,
-not price. Our General Public Licenses are designed to make sure that
-you have the freedom to distribute copies of free software (and charge
-for this service if you wish); that you receive source code or can get
-it if you want it; that you can change the software and use pieces of
-it in new free programs; and that you are informed that you can do
-these things.
-
- To protect your rights, we need to make restrictions that forbid
-distributors to deny you these rights or to ask you to surrender these
-rights. These restrictions translate to certain responsibilities for
-you if you distribute copies of the library or if you modify it.
-
- For example, if you distribute copies of the library, whether gratis
-or for a fee, you must give the recipients all the rights that we gave
-you. You must make sure that they, too, receive or can get the source
-code. If you link other code with the library, you must provide
-complete object files to the recipients, so that they can relink them
-with the library after making changes to the library and recompiling
-it. And you must show them these terms so they know their rights.
-
- We protect your rights with a two-step method: (1) we copyright the
-library, and (2) we offer you this license, which gives you legal
-permission to copy, distribute and/or modify the library.
-
- To protect each distributor, we want to make it very clear that
-there is no warranty for the free library. Also, if the library is
-modified by someone else and passed on, the recipients should know
-that what they have is not the original version, so that the original
-author's reputation will not be affected by problems that might be
-introduced by others.
-
- Finally, software patents pose a constant threat to the existence of
-any free program. We wish to make sure that a company cannot
-effectively restrict the users of a free program by obtaining a
-restrictive license from a patent holder. Therefore, we insist that
-any patent license obtained for a version of the library must be
-consistent with the full freedom of use specified in this license.
-
- Most GNU software, including some libraries, is covered by the
-ordinary GNU General Public License. This license, the GNU Lesser
-General Public License, applies to certain designated libraries, and
-is quite different from the ordinary General Public License. We use
-this license for certain libraries in order to permit linking those
-libraries into non-free programs.
-
- When a program is linked with a library, whether statically or using
-a shared library, the combination of the two is legally speaking a
-combined work, a derivative of the original library. The ordinary
-General Public License therefore permits such linking only if the
-entire combination fits its criteria of freedom. The Lesser General
-Public License permits more lax criteria for linking other code with
-the library.
-
- We call this license the "Lesser" General Public License because it
-does Less to protect the user's freedom than the ordinary General
-Public License. It also provides other free software developers Less
-of an advantage over competing non-free programs. These disadvantages
-are the reason we use the ordinary General Public License for many
-libraries. However, the Lesser license provides advantages in certain
-special circumstances.
-
- For example, on rare occasions, there may be a special need to
-encourage the widest possible use of a certain library, so that it becomes
-a de-facto standard. To achieve this, non-free programs must be
-allowed to use the library. A more frequent case is that a free
-library does the same job as widely used non-free libraries. In this
-case, there is little to gain by limiting the free library to free
-software only, so we use the Lesser General Public License.
-
- In other cases, permission to use a particular library in non-free
-programs enables a greater number of people to use a large body of
-free software. For example, permission to use the GNU C Library in
-non-free programs enables many more people to use the whole GNU
-operating system, as well as its variant, the GNU/Linux operating
-system.
-
- Although the Lesser General Public License is Less protective of the
-users' freedom, it does ensure that the user of a program that is
-linked with the Library has the freedom and the wherewithal to run
-that program using a modified version of the Library.
-
- The precise terms and conditions for copying, distribution and
-modification follow. Pay close attention to the difference between a
-"work based on the library" and a "work that uses the library". The
-former contains code derived from the library, whereas the latter must
-be combined with the library in order to run.
-
- GNU LESSER GENERAL PUBLIC LICENSE
- TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION
-
- 0. This License Agreement applies to any software library or other
-program which contains a notice placed by the copyright holder or
-other authorized party saying it may be distributed under the terms of
-this Lesser General Public License (also called "this License").
-Each licensee is addressed as "you".
-
- A "library" means a collection of software functions and/or data
-prepared so as to be conveniently linked with application programs
-(which use some of those functions and data) to form executables.
-
- The "Library", below, refers to any such software library or work
-which has been distributed under these terms. A "work based on the
-Library" means either the Library or any derivative work under
-copyright law: that is to say, a work containing the Library or a
-portion of it, either verbatim or with modifications and/or translated
-straightforwardly into another language. (Hereinafter, translation is
-included without limitation in the term "modification".)
-
- "Source code" for a work means the preferred form of the work for
-making modifications to it. For a library, complete source code means
-all the source code for all modules it contains, plus any associated
-interface definition files, plus the scripts used to control compilation
-and installation of the library.
-
- Activities other than copying, distribution and modification are not
-covered by this License; they are outside its scope. The act of
-running a program using the Library is not restricted, and output from
-such a program is covered only if its contents constitute a work based
-on the Library (independent of the use of the Library in a tool for
-writing it). Whether that is true depends on what the Library does
-and what the program that uses the Library does.
-
- 1. You may copy and distribute verbatim copies of the Library's
-complete source code as you receive it, in any medium, provided that
-you conspicuously and appropriately publish on each copy an
-appropriate copyright notice and disclaimer of warranty; keep intact
-all the notices that refer to this License and to the absence of any
-warranty; and distribute a copy of this License along with the
-Library.
-
- You may charge a fee for the physical act of transferring a copy,
-and you may at your option offer warranty protection in exchange for a
-fee.
-
- 2. You may modify your copy or copies of the Library or any portion
-of it, thus forming a work based on the Library, and copy and
-distribute such modifications or work under the terms of Section 1
-above, provided that you also meet all of these conditions:
-
- a) The modified work must itself be a software library.
-
- b) You must cause the files modified to carry prominent notices
- stating that you changed the files and the date of any change.
-
- c) You must cause the whole of the work to be licensed at no
- charge to all third parties under the terms of this License.
-
- d) If a facility in the modified Library refers to a function or a
- table of data to be supplied by an application program that uses
- the facility, other than as an argument passed when the facility
- is invoked, then you must make a good faith effort to ensure that,
- in the event an application does not supply such function or
- table, the facility still operates, and performs whatever part of
- its purpose remains meaningful.
-
- (For example, a function in a library to compute square roots has
- a purpose that is entirely well-defined independent of the
- application. Therefore, Subsection 2d requires that any
- application-supplied function or table used by this function must
- be optional: if the application does not supply it, the square
- root function must still compute square roots.)
-
-These requirements apply to the modified work as a whole. If
-identifiable sections of that work are not derived from the Library,
-and can be reasonably considered independent and separate works in
-themselves, then this License, and its terms, do not apply to those
-sections when you distribute them as separate works. But when you
-distribute the same sections as part of a whole which is a work based
-on the Library, the distribution of the whole must be on the terms of
-this License, whose permissions for other licensees extend to the
-entire whole, and thus to each and every part regardless of who wrote
-it.
-
-Thus, it is not the intent of this section to claim rights or contest
-your rights to work written entirely by you; rather, the intent is to
-exercise the right to control the distribution of derivative or
-collective works based on the Library.
-
-In addition, mere aggregation of another work not based on the Library
-with the Library (or with a work based on the Library) on a volume of
-a storage or distribution medium does not bring the other work under
-the scope of this License.
-
- 3. You may opt to apply the terms of the ordinary GNU General Public
-License instead of this License to a given copy of the Library. To do
-this, you must alter all the notices that refer to this License, so
-that they refer to the ordinary GNU General Public License, version 2,
-instead of to this License. (If a newer version than version 2 of the
-ordinary GNU General Public License has appeared, then you can specify
-that version instead if you wish.) Do not make any other change in
-these notices.
-
- Once this change is made in a given copy, it is irreversible for
-that copy, so the ordinary GNU General Public License applies to all
-subsequent copies and derivative works made from that copy.
-
- This option is useful when you wish to copy part of the code of
-the Library into a program that is not a library.
-
- 4. You may copy and distribute the Library (or a portion or
-derivative of it, under Section 2) in object code or executable form
-under the terms of Sections 1 and 2 above provided that you accompany
-it with the complete corresponding machine-readable source code, which
-must be distributed under the terms of Sections 1 and 2 above on a
-medium customarily used for software interchange.
-
- If distribution of object code is made by offering access to copy
-from a designated place, then offering equivalent access to copy the
-source code from the same place satisfies the requirement to
-distribute the source code, even though third parties are not
-compelled to copy the source along with the object code.
-
- 5. A program that contains no derivative of any portion of the
-Library, but is designed to work with the Library by being compiled or
-linked with it, is called a "work that uses the Library". Such a
-work, in isolation, is not a derivative work of the Library, and
-therefore falls outside the scope of this License.
-
- However, linking a "work that uses the Library" with the Library
-creates an executable that is a derivative of the Library (because it
-contains portions of the Library), rather than a "work that uses the
-library". The executable is therefore covered by this License.
-Section 6 states terms for distribution of such executables.
-
- When a "work that uses the Library" uses material from a header file
-that is part of the Library, the object code for the work may be a
-derivative work of the Library even though the source code is not.
-Whether this is true is especially significant if the work can be
-linked without the Library, or if the work is itself a library. The
-threshold for this to be true is not precisely defined by law.
-
- If such an object file uses only numerical parameters, data
-structure layouts and accessors, and small macros and small inline
-functions (ten lines or less in length), then the use of the object
-file is unrestricted, regardless of whether it is legally a derivative
-work. (Executables containing this object code plus portions of the
-Library will still fall under Section 6.)
-
- Otherwise, if the work is a derivative of the Library, you may
-distribute the object code for the work under the terms of Section 6.
-Any executables containing that work also fall under Section 6,
-whether or not they are linked directly with the Library itself.
-
- 6. As an exception to the Sections above, you may also combine or
-link a "work that uses the Library" with the Library to produce a
-work containing portions of the Library, and distribute that work
-under terms of your choice, provided that the terms permit
-modification of the work for the customer's own use and reverse
-engineering for debugging such modifications.
-
- You must give prominent notice with each copy of the work that the
-Library is used in it and that the Library and its use are covered by
-this License. You must supply a copy of this License. If the work
-during execution displays copyright notices, you must include the
-copyright notice for the Library among them, as well as a reference
-directing the user to the copy of this License. Also, you must do one
-of these things:
-
- a) Accompany the work with the complete corresponding
- machine-readable source code for the Library including whatever
- changes were used in the work (which must be distributed under
- Sections 1 and 2 above); and, if the work is an executable linked
- with the Library, with the complete machine-readable "work that
- uses the Library", as object code and/or source code, so that the
- user can modify the Library and then relink to produce a modified
- executable containing the modified Library. (It is understood
- that the user who changes the contents of definitions files in the
- Library will not necessarily be able to recompile the application
- to use the modified definitions.)
-
- b) Use a suitable shared library mechanism for linking with the
- Library. A suitable mechanism is one that (1) uses at run time a
- copy of the library already present on the user's computer system,
- rather than copying library functions into the executable, and (2)
- will operate properly with a modified version of the library, if
- the user installs one, as long as the modified version is
- interface-compatible with the version that the work was made with.
-
- c) Accompany the work with a written offer, valid for at
- least three years, to give the same user the materials
- specified in Subsection 6a, above, for a charge no more
- than the cost of performing this distribution.
-
- d) If distribution of the work is made by offering access to copy
- from a designated place, offer equivalent access to copy the above
- specified materials from the same place.
-
- e) Verify that the user has already received a copy of these
- materials or that you have already sent this user a copy.
-
- For an executable, the required form of the "work that uses the
-Library" must include any data and utility programs needed for
-reproducing the executable from it. However, as a special exception,
-the materials to be distributed need not include anything that is
-normally distributed (in either source or binary form) with the major
-components (compiler, kernel, and so on) of the operating system on
-which the executable runs, unless that component itself accompanies
-the executable.
-
- It may happen that this requirement contradicts the license
-restrictions of other proprietary libraries that do not normally
-accompany the operating system. Such a contradiction means you cannot
-use both them and the Library together in an executable that you
-distribute.
-
- 7. You may place library facilities that are a work based on the
-Library side-by-side in a single library together with other library
-facilities not covered by this License, and distribute such a combined
-library, provided that the separate distribution of the work based on
-the Library and of the other library facilities is otherwise
-permitted, and provided that you do these two things:
-
- a) Accompany the combined library with a copy of the same work
- based on the Library, uncombined with any other library
- facilities. This must be distributed under the terms of the
- Sections above.
-
- b) Give prominent notice with the combined library of the fact
- that part of it is a work based on the Library, and explaining
- where to find the accompanying uncombined form of the same work.
-
- 8. You may not copy, modify, sublicense, link with, or distribute
-the Library except as expressly provided under this License. Any
-attempt otherwise to copy, modify, sublicense, link with, or
-distribute the Library is void, and will automatically terminate your
-rights under this License. However, parties who have received copies,
-or rights, from you under this License will not have their licenses
-terminated so long as such parties remain in full compliance.
-
- 9. You are not required to accept this License, since you have not
-signed it. However, nothing else grants you permission to modify or
-distribute the Library or its derivative works. These actions are
-prohibited by law if you do not accept this License. Therefore, by
-modifying or distributing the Library (or any work based on the
-Library), you indicate your acceptance of this License to do so, and
-all its terms and conditions for copying, distributing or modifying
-the Library or works based on it.
-
- 10. Each time you redistribute the Library (or any work based on the
-Library), the recipient automatically receives a license from the
-original licensor to copy, distribute, link with or modify the Library
-subject to these terms and conditions. You may not impose any further
-restrictions on the recipients' exercise of the rights granted herein.
-You are not responsible for enforcing compliance by third parties with
-this License.
-
- 11. If, as a consequence of a court judgment or allegation of patent
-infringement or for any other reason (not limited to patent issues),
-conditions are imposed on you (whether by court order, agreement or
-otherwise) that contradict the conditions of this License, they do not
-excuse you from the conditions of this License. If you cannot
-distribute so as to satisfy simultaneously your obligations under this
-License and any other pertinent obligations, then as a consequence you
-may not distribute the Library at all. For example, if a patent
-license would not permit royalty-free redistribution of the Library by
-all those who receive copies directly or indirectly through you, then
-the only way you could satisfy both it and this License would be to
-refrain entirely from distribution of the Library.
-
-If any portion of this section is held invalid or unenforceable under any
-particular circumstance, the balance of the section is intended to apply,
-and the section as a whole is intended to apply in other circumstances.
-
-It is not the purpose of this section to induce you to infringe any
-patents or other property right claims or to contest validity of any
-such claims; this section has the sole purpose of protecting the
-integrity of the free software distribution system which is
-implemented by public license practices. Many people have made
-generous contributions to the wide range of software distributed
-through that system in reliance on consistent application of that
-system; it is up to the author/donor to decide if he or she is willing
-to distribute software through any other system and a licensee cannot
-impose that choice.
-
-This section is intended to make thoroughly clear what is believed to
-be a consequence of the rest of this License.
-
- 12. If the distribution and/or use of the Library is restricted in
-certain countries either by patents or by copyrighted interfaces, the
-original copyright holder who places the Library under this License may add
-an explicit geographical distribution limitation excluding those countries,
-so that distribution is permitted only in or among countries not thus
-excluded. In such case, this License incorporates the limitation as if
-written in the body of this License.
-
- 13. The Free Software Foundation may publish revised and/or new
-versions of the Lesser General Public License from time to time.
-Such new versions will be similar in spirit to the present version,
-but may differ in detail to address new problems or concerns.
-
-Each version is given a distinguishing version number. If the Library
-specifies a version number of this License which applies to it and
-"any later version", you have the option of following the terms and
-conditions either of that version or of any later version published by
-the Free Software Foundation. If the Library does not specify a
-license version number, you may choose any version ever published by
-the Free Software Foundation.
-
- 14. If you wish to incorporate parts of the Library into other free
-programs whose distribution conditions are incompatible with these,
-write to the author to ask for permission. For software which is
-copyrighted by the Free Software Foundation, write to the Free
-Software Foundation; we sometimes make exceptions for this. Our
-decision will be guided by the two goals of preserving the free status
-of all derivatives of our free software and of promoting the sharing
-and reuse of software generally.
-
- NO WARRANTY
-
- 15. BECAUSE THE LIBRARY IS LICENSED FREE OF CHARGE, THERE IS NO
-WARRANTY FOR THE LIBRARY, TO THE EXTENT PERMITTED BY APPLICABLE LAW.
-EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR
-OTHER PARTIES PROVIDE THE LIBRARY "AS IS" WITHOUT WARRANTY OF ANY
-KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE
-IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
-PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE
-LIBRARY IS WITH YOU. SHOULD THE LIBRARY PROVE DEFECTIVE, YOU ASSUME
-THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
-
- 16. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN
-WRITING WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY
-AND/OR REDISTRIBUTE THE LIBRARY AS PERMITTED ABOVE, BE LIABLE TO YOU
-FOR DAMAGES, INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR
-CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THE
-LIBRARY (INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA BEING
-RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD PARTIES OR A
-FAILURE OF THE LIBRARY TO OPERATE WITH ANY OTHER SOFTWARE), EVEN IF
-SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH
-DAMAGES.
-
- END OF TERMS AND CONDITIONS
+This is free and unencumbered software released into the public domain.
+
+Anyone is free to copy, modify, publish, use, compile, sell, or
+distribute this software, either in source code form or as a compiled
+binary, for any purpose, commercial or non-commercial, and by any
+means.
+
+In jurisdictions that recognize copyright laws, the author or authors
+of this software dedicate any and all copyright interest in the
+software to the public domain. We make this dedication for the benefit
+of the public at large and to the detriment of our heirs and
+successors. We intend this dedication to be an overt act of
+relinquishment in perpetuity of all present and future rights to this
+software under copyright law.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY CLAIM, DAMAGES OR
+OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
+ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR
+OTHER DEALINGS IN THE SOFTWARE.
+
+For more information, please refer to
--
cgit v1.2.3