1 (* |
1 (* Title: test/Tools/isac/ADDTESTS/file-depend |
|
2 Author: Walther Neuper |
|
3 *) |
|
4 |
|
5 header {* Test file dependencies analogous to ISAC |
|
6 |
2 $ cd /usr/local/Isabelle/test/Tools/isac/ADDTESTS/file-depend |
7 $ cd /usr/local/Isabelle/test/Tools/isac/ADDTESTS/file-depend |
3 $ /usr/local/Isabelle/bin/isabelle emacs Build_Test.thy & |
8 $ /usr/local/Isabelle/bin/isabelle emacs Build_Test.thy & |
4 |
9 *} |
5 *) |
10 (*---------------------------------------------------------------------------- |
6 |
|
7 theory Build_Test |
11 theory Build_Test |
8 imports |
12 imports |
9 Complex_Main |
13 Complex_Main |
10 "1language/Foo_Language" |
14 "1language/Foo_Language" |
11 "3knowledge/Foo_KnowALL" |
15 "3knowledge/Foo_KnowALL" |
12 begin |
16 begin |
|
17 ----------------------------------------------------------------------------*) |
13 |
18 |
14 use "0foolibrary.ML" |
19 theory Build_Test |
15 use_thy "1language/Foo_Language" |
20 imports |
16 use "2interpreter/2foointerpreter.ML" |
21 Complex_Main |
|
22 begin |
|
23 use "0foolibrary.ML" ML {* foolibrhs *} |
|
24 use_thy "1language/Foo_Language" (*ML {* @{const fooprog} *}*) |
|
25 use "2interpreter/2foointerpreter.ML" ML {* foointerpret *} |
17 |
26 |
18 (*vvvvvvv can be bypassed with Foo_KnowALL |
27 text {* The top 'theory ... begin' can be outcommended and done stepwise: |
19 use_thy "3knowledge/Foo_Know111" |
28 |
20 use_thy "3knowledge/Foo_Know222" |
29 use "2interpreter/2foointerpreter.ML" |
21 ^^^^^^^ can be bypassed with Foo_KnowALL*) |
30 use_thy "3knowledge/Foo_Know111" |
22 use_thy "3knowledge/Foo_KnowALL" |
31 use_thy "3knowledge/Foo_Know222" |
|
32 use_thy "3knowledge/Foo_KnowALL" |
|
33 *} |
23 |
34 |
24 text {* the different theories of knowledge are recognized, Const bar*: *} |
35 text {* the different theories of knowledge are recognized, Const bar*: *} |
25 ML {* |
36 ML {* |
26 val trm = Syntax.read_term_global @{theory Foo_Know111} |
37 val trm = Syntax.read_term_global @{theory Foo_Know111} |
27 "fooprog (foo111 = bar111)"; |
38 "fooprog (foo111 = bar111)"; |
47 Const ("Foo_Language.fooprog", "bool => Foo_Language.foosource") $ |
58 Const ("Foo_Language.fooprog", "bool => Foo_Language.foosource") $ |
48 (Const ("op =", "'a => 'a => bool") $ Free ("foo111", "'a") $ |
59 (Const ("op =", "'a => 'a => bool") $ Free ("foo111", "'a") $ |
49 Free ("bar111", "'a")) |
60 Free ("bar111", "'a")) |
50 : term*) |
61 : term*) |
51 *} |
62 *} |
|
63 |
|
64 text {* dir structure reflects ISAC, see Build_Isac.thy: |
|
65 /file-depend/0foolibrary.ML |
|
66 /file-depend/Build_Test.thy |
|
67 /file-depend/README |
|
68 |
|
69 /file-depend/1language/Foo_Language.thy |
|
70 |
|
71 /file-depend/2interpreter/2foointerpreter.ML |
|
72 |
|
73 /file-depend/3knowledge/Foo_Know111.thy |
|
74 /file-depend/3knowledge/Foo_Know222.thy |
|
75 /file-depend/3knowledge/Foo_KnowALL.thy |
|
76 *} |