Now a command to access the value of a constant

4 files changed, 27 insertions, 1 deletions

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