1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 *) 6 7(* Basic tests for the Qualify tool. *) 8 9theory Qualify_Test 10imports 11 Lib.Qualify 12begin 13 14locale qualify_test 15 16section \<open>datatype\<close> 17 18datatype leaky = leaky 19 20text \<open> 21 By default, the datatype package adds constant names to the unqualified global namespace. 22 Let's check that this is the case. 23\<close> 24ML \<open> 25 if can dest_Const @{term leaky} 26 then () 27 else error "Qualify_Test failed: datatype leaky baseline" 28\<close> 29 30text \<open> 31 When we wrap the @{command datatype} command in @{command qualify}\<dots>@{command end_qualify}, 32 the unqualified names should be removed. 33\<close> 34qualify qualify_test 35 datatype nonleaky = nonleaky 36 37 (* unqualified name still exists here *) 38 ML \<open> 39 if can dest_Const @{term nonleaky} 40 then () 41 else error "Qualify_Test failed: datatype nonleaky baseline 1" 42 \<close> 43end_qualify 44 45(* but not here *) 46ML \<open> 47 if can dest_Free @{term nonleaky} 48 then () 49 else error "Qualify_Test failed: datatype nonleaky test" 50\<close> 51 52(* qualified name exists *) 53ML \<open> 54 if can dest_Const @{term qualify_test.nonleaky} 55 then () 56 else error "Qualify_Test failed: datatype nonleaky baseline 2" 57\<close> 58 59 60section \<open>instantiation\<close> 61 62text \<open> 63 We can also qualify fact names from class instantiations. 64\<close> 65 66instantiation leaky :: ord begin 67 definition less_leaky: 68 "(x :: leaky) < y = True" 69 instance by intro_classes 70end 71 72text \<open> 73 By default, fact names are added to the unqualified global namespace. 74\<close> 75ML \<open> 76 if can (Proof_Context.get_thm @{context}) "less_leaky" 77 then () 78 else error "Qualify_Test failed: instantiation leaky baseline" 79\<close> 80 81qualify qualify_test 82 instantiation qualify_test.nonleaky :: ord begin 83 definition less_nonleaky: 84 "(x :: qualify_test.nonleaky) < y = True" 85 instance by intro_classes 86 end 87 88 (* unqualified name still exists here *) 89 ML \<open> 90 if can (Proof_Context.get_thm @{context}) "less_nonleaky" 91 then () 92 else error "Qualify_Test failed: instantiation nonleaky baseline 1" 93 \<close> 94end_qualify 95 96(* but not here *) 97ML \<open> 98 if can (Proof_Context.get_thm @{context}) "less_nonleaky" 99 then error "Qualify_Test failed: instantiation nonleaky test" 100 else () 101\<close> 102 103(* qualified name exists *) 104ML \<open> 105 if can (Proof_Context.get_thm @{context}) "qualify_test.less_nonleaky" 106 then () 107 else error "Qualify_Test failed: instantiation nonleaky baseline 2" 108\<close> 109 110end 111