1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory ShowTypes_Test
8imports
9  Lib.ShowTypes
10  CLib.LemmaBucket_C
11  CParser.CTranslation
12begin
13
14text \<open>
15  Simple demo and test. The main HOL theories don't have that much
16  hidden polymorphism, so we use l4.verified.
17\<close>
18
19experiment
20  (* The point of this test is to confirm that the generic 'show types' feature
21     shows enough type information to fully reconstruct a term; the pointer type
22     feature does something similar so we disable it here. *)
23  notes [[show_ptr_types = false]]
24begin
25  lemma c_guard_cast_byte: "c_guard (x :: ('a :: {mem_type}) ptr) \<Longrightarrow> c_guard (ptr_coerce x :: 8 word ptr)"
26    goal_show_types 0
27    using [[show_sorts]]
28    goal_show_types 0
29    apply (case_tac x)
30    apply (fastforce intro!: byte_ptr_guarded simp: c_guard_def dest: c_null_guard)
31    done
32
33  thm c_guard_cast_byte[where x = "Ptr (ucast (0 :: 8 word))"]
34  thm_show_types c_guard_cast_byte[where x = "Ptr (ucast (0 :: 8 word))"]
35
36  (* Round-trip test *)
37  ML \<open>
38  let val ctxt = Config.put show_sorts true @{context}
39      (* NB: this test fails if we leave some polymorphism in the term *)
40      val term = @{thm c_guard_cast_byte[where x = "Ptr (ucast (0 :: 8 word)) :: unit ptr"]} |> Thm.prop_of
41      val string_no_types = Syntax.pretty_term ctxt term
42                            |> Pretty.string_of |> YXML.content_of
43      val string_show_types = Show_Types.term_show_types true ctxt term
44
45      val _ = assert (Syntax.read_term ctxt string_no_types <> term) "Show_Types test (baseline)"
46      val _ = assert (Syntax.read_term ctxt string_show_types = term) "Show_Types test"
47  in () end
48  \<close>
49end
50
51end