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