From ef096e387122799ab2e6c1eda50261c58088438c Mon Sep 17 00:00:00 2001
From: Japheth Lim <Japheth.Lim@nicta.com.au>
Date: Wed, 20 Apr 2016 18:24:51 +1000
Subject: [PATCH] autocorres: add demo for AutoCorresFunctionInfo, etc.

---
 .../tests/examples/FunctionInfoDemo.thy       | 81 +++++++++++++++++++
 .../autocorres/tests/examples/function_info.c | 11 +++
 2 files changed, 92 insertions(+)
 create mode 100644 tools/autocorres/tests/examples/FunctionInfoDemo.thy
 create mode 100644 tools/autocorres/tests/examples/function_info.c

diff --git a/tools/autocorres/tests/examples/FunctionInfoDemo.thy b/tools/autocorres/tests/examples/FunctionInfoDemo.thy
new file mode 100644
index 000000000..c52c3ed9c
--- /dev/null
+++ b/tools/autocorres/tests/examples/FunctionInfoDemo.thy
@@ -0,0 +1,81 @@
+text \<open>
+  In addition to named theorems, AutoCorres also stores definitions,
+  theorems and other data in ML data structures.
+  These can be useful for writing tools to process the AutoCorres output.
+
+  See also: TraceDemo
+\<close>
+theory FunctionInfoDemo imports
+  "../../AutoCorres"
+begin
+
+text \<open>Process a source file to populate our data structures.\<close>
+install_C_file "function_info.c"
+autocorres "function_info.c"
+context function_info begin
+
+section \<open>Function info\<close>
+text \<open>
+  Information about all AutoCorres-processed functions is stored in the
+  AutoCorresFunctionInfo structure.
+\<close>
+ML \<open>
+  val fn_info: FunctionInfo.fn_info =
+      the (Symtab.lookup (AutoCorresFunctionInfo.get @{theory}) "function_info.c")
+\<close>
+  
+text \<open>
+  One FunctionInfo.fn_info structure is generated for each translated file.
+  See the FunctionInfo structure for details about the stored data.
+  As a start, we can show all function definitions:
+\<close>
+ML \<open>
+  FunctionInfo.get_functions fn_info |> Symtab.dest |> map snd
+  |> app (fn f => writeln ("Definition of " ^ #name f ^ ":\n" ^
+                    Syntax.string_of_term @{context} (Thm.prop_of (#definition f))))
+\<close>
+
+section \<open>Heap info\<close>
+text \<open>
+  Information about the abstracted heap (if heap_abs is enabled) is also stored
+  to the HeapInfo structure.
+  See heap_lift_base.ML for which fields are contained in the structure.
+\<close>
+ML \<open>
+  the (Symtab.lookup (HeapInfo.get @{theory}) "function_info.c")
+\<close>
+
+section \<open>Intermediate function info\<close>
+text \<open>
+  AutoCorres performs a translation in multiple stages; the intermediate definitions
+  and correspondence theorems are also stored in AutoCorresData.
+  Definitions are tagged with the name (phase ^ "def") and corres theorems with
+  the name (phase ^ "corres").
+
+  This data is probably not useful outside of debugging AutoCorres itself.
+\<close>
+ML \<open>
+  let val fn_name = "rec"
+      val phases = [
+        "L1", (* translation from SIMPL syntax *)
+        "L2", (* lift local variables *)
+        "HL", (* heap abstraction *)
+        "WA", (* word abstraction *)
+        "TS"  (* type lifting *)
+       ]
+  in (
+      (* defs *)
+      map (fn phase =>
+        AutoCorresData.get_def @{theory} "function_info.c" (phase ^ "def") fn_name)
+        phases,
+    
+      (* corres *)
+      map (fn phase =>
+        AutoCorresData.get_thm @{theory} "function_info.c" (phase ^ "corres") fn_name)
+        phases
+    )
+  end
+\<close>
+
+end
+end
\ No newline at end of file
diff --git a/tools/autocorres/tests/examples/function_info.c b/tools/autocorres/tests/examples/function_info.c
new file mode 100644
index 000000000..12ecdbf46
--- /dev/null
+++ b/tools/autocorres/tests/examples/function_info.c
@@ -0,0 +1,11 @@
+/*
+ * The exact behaviour of these functions is unimportant for our example.
+ */
+
+void rec() {
+  rec();
+}
+
+void f() {
+  rec();
+}