diff options
| author | Yves Bertot | 2018-05-04 17:28:30 +0200 |
|---|---|---|
| committer | Yves Bertot | 2018-05-04 17:28:30 +0200 |
| commit | c3bc6e79494b03543e0c708bfa9e71d2e5d57aee (patch) | |
| tree | c855581dabc63f7d3adea1cbfbf383312f4cbf86 | |
| parent | cb20f241cc7ec686a5ae19c1e7b9eef6b26d230a (diff) | |
Now a command to access the value of a constant
| -rw-r--r-- | tuto1/_CoqProject | 4 | ||||
| -rw-r--r-- | tuto1/src/g_tuto1.ml4 | 12 | ||||
| -rw-r--r-- | tuto1/src/simple_print.ml | 14 | ||||
| -rw-r--r-- | tuto1/src/simple_print.mli | 1 | ||||
| -rw-r--r-- | tuto1/src/tuto1_plugin.mlpack | 1 | ||||
| -rw-r--r-- | tuto1/theories/Loader.v | 1 |
6 files changed, 32 insertions, 1 deletions
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 |