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