repackage with an extra ml file, add a usage of new_type_evar

5 files changed, 74 insertions, 24 deletions

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