lib: test cases for Insulin and ShowTypes tools

lib/Insulin.thy

@@ -50,8 +50,10 @@
  *)
 
 theory Insulin
-  imports Main
-  keywords "desugar_term" "desugar_thm" "desugar_goal" :: diag
+imports
+  Pure
+keywords
+  "desugar_term" "desugar_thm" "desugar_goal" :: diag
 begin
 
 (*

lib/Insulin_Test.thy

@@ -0,0 +1,55 @@
+(*
+ * Copyright 2018, Data61
+ * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
+ * ABN 41 687 119 230.
+
+ * This software may be distributed and modified according to the terms of
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
+
+ * @TAG(DATA61_BSD)
+ *)
+
+(* Basic tests for the Insulin desugar tool. *)
+
+theory Insulin_Test
+imports
+  Lib.Insulin
+  Main
+begin
+
+ML \<open>
+(*
+ * To be considered successful, desugaring should do two things:
+ *   - remove the unwanted syntax strings
+ *   - return an equivalent term
+ * The following code just checks those two conditions.
+ *)
+
+fun test_desugar ctxt (term, bad_strings) = let
+  val text = (* function being tested *)
+             Insulin.desugar_term ctxt term bad_strings
+             (* strip markup from result *)
+             |> YXML.parse_body
+             |> XML.content_of
+  val remaining_bads = filter (fn bs => String.isSubstring bs text) bad_strings
+  val _ = if null remaining_bads then () else
+          raise TERM ("failed to desugar these strings: [" ^ commas bad_strings ^ "]\n" ^
+                      "output: " ^ text, [term])
+  val term' = Syntax.read_term ctxt text
+  val _ = if term = term' then () else
+          raise TERM ("desugared term not equal to original",
+                      [term, term'])
+  in () end
+\<close>
+
+ML \<open>
+(* The test cases. *)
+[ (@{term "A \<and> B"}, ["\<and>"])
+, (@{term "a + 0 = a * 1"}, ["+", "0", "1"])
+, (@{term "(f(x := y)) z = (if z = x then y else f z)"}, [":="])
+, (@{term "(f(x := y)) z = (if z = x then y else f z)"}, ["="])
+] |> app (test_desugar @{context})
+\<close>
+
+end

lib/ROOT

@@ -149,6 +149,8 @@ session LibTest (lib) = Refine +
     Match_Abbreviation_Test
     Apply_Debug_Test
     AutoLevity_Test
+    Insulin_Test
+    ShowTypes_Test
     Time_Methods_Cmd_Test
     Trace_Schematic_Insts_Test
     Local_Method_Tests

lib/ShowTypes.thy

@@ -116,39 +116,4 @@ Outer_Syntax.command @{command_keyword goal_show_types}
 end;
 *}
 
-
-text \<open>
-  Simple demo. The main HOL theories don't have that much
-  hidden polymorphism, so we use l4.verified.
-\<close>
-
-(*
-experiment begin
-  lemma c_guard_cast_byte: "c_guard (x :: ('a :: {mem_type}) ptr) \<Longrightarrow> c_guard (ptr_coerce x :: 8 word ptr)"
-    goal_show_types 0
-    using [[show_sorts]]
-    goal_show_types 0
-    apply (case_tac x)
-    apply (fastforce intro!: byte_ptr_guarded simp: c_guard_def dest: c_null_guard)
-    done
-
-  thm c_guard_cast_byte[where x = "Ptr (ucast (0 :: 8 word))"]
-  thm_show_types c_guard_cast_byte[where x = "Ptr (ucast (0 :: 8 word))"]
-
-  (* Round-trip test *)
-  ML {*
-  let val ctxt = Config.put show_sorts true @{context}
-      (* NB: this test fails if we leave some polymorphism in the term *)
-      val term = @{thm c_guard_cast_byte[where x = "Ptr (ucast (0 :: 8 word)) :: unit ptr"]} |> Thm.prop_of
-      val string_no_types = Syntax.pretty_term ctxt term
-                            |> Pretty.string_of |> YXML.content_of
-      val string_show_types = Show_Types.term_show_types true ctxt term
-
-      val _ = assert (Syntax.read_term ctxt string_no_types <> term) "Show_Types test (baseline)"
-      val _ = assert (Syntax.read_term ctxt string_show_types = term) "Show_Types test"
-  in () end
-  *}
-end
-*)
-
 end

lib/ShowTypes_Test.thy

@@ -0,0 +1,50 @@
+(*
+ * Copyright 2016, NICTA
+ *
+ * This software may be distributed and modified according to the terms of
+ * the BSD 2-Clause license. Note that NO WARRANTY is provided.
+ * See "LICENSE_BSD2.txt" for details.
+ *
+ * @TAG(NICTA_BSD)
+ *)
+
+theory ShowTypes_Test
+imports
+  Lib.ShowTypes
+  CLib.LemmaBucket_C
+  CParser.CTranslation
+begin
+
+text \<open>
+  Simple demo and test. The main HOL theories don't have that much
+  hidden polymorphism, so we use l4.verified.
+\<close>
+
+experiment begin
+  lemma c_guard_cast_byte: "c_guard (x :: ('a :: {mem_type}) ptr) \<Longrightarrow> c_guard (ptr_coerce x :: 8 word ptr)"
+    goal_show_types 0
+    using [[show_sorts]]
+    goal_show_types 0
+    apply (case_tac x)
+    apply (fastforce intro!: byte_ptr_guarded simp: c_guard_def dest: c_null_guard)
+    done
+
+  thm c_guard_cast_byte[where x = "Ptr (ucast (0 :: 8 word))"]
+  thm_show_types c_guard_cast_byte[where x = "Ptr (ucast (0 :: 8 word))"]
+
+  (* Round-trip test *)
+  ML \<open>
+  let val ctxt = Config.put show_sorts true @{context}
+      (* NB: this test fails if we leave some polymorphism in the term *)
+      val term = @{thm c_guard_cast_byte[where x = "Ptr (ucast (0 :: 8 word)) :: unit ptr"]} |> Thm.prop_of
+      val string_no_types = Syntax.pretty_term ctxt term
+                            |> Pretty.string_of |> YXML.content_of
+      val string_show_types = Show_Types.term_show_types true ctxt term
+
+      val _ = assert (Syntax.read_term ctxt string_no_types <> term) "Show_Types test (baseline)"
+      val _ = assert (Syntax.read_term ctxt string_show_types = term) "Show_Types test"
+  in () end
+  \<close>
+end
+
+end