1(*
2 * Copyright 2016, NICTA
3 *
4 * This software may be distributed and modified according to the terms of
5 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
6 * See "LICENSE_BSD2.txt" for details.
7 *
8 * @TAG(NICTA_BSD)
9 *)
10
11theory ShowTypes_Test
12imports
13  Lib.ShowTypes
14  CLib.LemmaBucket_C
15  CParser.CTranslation
16begin
17
18text \<open>
19  Simple demo and test. The main HOL theories don't have that much
20  hidden polymorphism, so we use l4.verified.
21\<close>
22
23experiment begin
24  lemma c_guard_cast_byte: "c_guard (x :: ('a :: {mem_type}) ptr) \<Longrightarrow> c_guard (ptr_coerce x :: 8 word ptr)"
25    goal_show_types 0
26    using [[show_sorts]]
27    goal_show_types 0
28    apply (case_tac x)
29    apply (fastforce intro!: byte_ptr_guarded simp: c_guard_def dest: c_null_guard)
30    done
31
32  thm c_guard_cast_byte[where x = "Ptr (ucast (0 :: 8 word))"]
33  thm_show_types c_guard_cast_byte[where x = "Ptr (ucast (0 :: 8 word))"]
34
35  (* Round-trip test *)
36  ML \<open>
37  let val ctxt = Config.put show_sorts true @{context}
38      (* NB: this test fails if we leave some polymorphism in the term *)
39      val term = @{thm c_guard_cast_byte[where x = "Ptr (ucast (0 :: 8 word)) :: unit ptr"]} |> Thm.prop_of
40      val string_no_types = Syntax.pretty_term ctxt term
41                            |> Pretty.string_of |> YXML.content_of
42      val string_show_types = Show_Types.term_show_types true ctxt term
43
44      val _ = assert (Syntax.read_term ctxt string_no_types <> term) "Show_Types test (baseline)"
45      val _ = assert (Syntax.read_term ctxt string_show_types = term) "Show_Types test"
46  in () end
47  \<close>
48end
49
50end