This version contains a simple command that defines a new constant

7 files changed, 108 insertions, 10 deletions

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