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