Mercurial Mercurial > wneuper > isa / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/ADDTESTS/file-depend/Build_Test.thy
author Walther Neuper <neuper@ist.tugraz.at>
Tue, 01 Mar 2011 15:23:59 +0100
branchdecompose-isar
changeset 41905 b772eb34c16c
parent 41900 8391d3789efb
child 41916 73604b24fe92
permissions -rw-r--r--
intermed.update to Isabelle2011: test/../syntax added

present problem: test/Tools/isac/ADDTESTS/filed-depend does not update 
     1 (* Title:   test/Tools/isac/ADDTESTS/file-depend

     2    Author:  Walther Neuper

     3 *)

     4 

     5 header {* Test file dependencies analogous to ISAC

     6 

     7 $ cd /usr/local/Isabelle/test/Tools/isac/ADDTESTS/file-depend

     8 $ /usr/local/Isabelle/bin/isabelle emacs Build_Test.thy &

     9 *}

    10 (*----------------------------------------------------------------------------

    11 theory Build_Test 

    12 imports 

    13   Complex_Main 

    14   "1language/Foo_Language"

    15   "3knowledge/Foo_KnowALL"

    16 begin

    17 ----------------------------------------------------------------------------*)

    18 

    19 theory Build_Test 

    20 imports 

    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 *}

    26 

    27 text {* The top 'theory ... begin' can be outcommended and done stepwise:

    28 

    29   use     "2interpreter/2foointerpreter.ML"

    30   use_thy "3knowledge/Foo_Know111"

    31   use_thy "3knowledge/Foo_Know222"

    32   use_thy "3knowledge/Foo_KnowALL"

    33 *}

    34 

    35 text {* the different theories of knowledge are recognized, Const bar*: *}

    36 ML {* 

    37 val trm = Syntax.read_term_global @{theory Foo_Know111} 

    38   "fooprog (foo111 = bar111)";

    39 val Const ("Foo_Know111.bar111", _) = foointerpret trm;

    40 

    41 val trm = Syntax.read_term_global @{theory Foo_Know222} 

    42   "fooprog (foo222 = bar222)";

    43 val Const ("Foo_Know222.bar222", _) = foointerpret trm;

    44 *}

    45 

    46 text {* the different theories of knowledge are recognized, Free bar*: *}

    47 ML {*

    48 val trm = Syntax.read_term_global @{theory Foo_Know111} 

    49   "fooprog (foo222 = bar222)";

    50 (*Const ("Foo_Language.fooprog", "bool => Foo_Language.foosource") $

    51      (Const ("op =", "'a => 'a => bool") $ Free ("foo222", "'a") $

    52        Free ("bar222", "'a"))

    53    : term*)

    54 

    55 val trm = Syntax.read_term_global @{theory Foo_Know222} 

    56   "fooprog (foo111 = bar111)";

    57 (*val trm =

    58    Const ("Foo_Language.fooprog", "bool => Foo_Language.foosource") $

    59      (Const ("op =", "'a => 'a => bool") $ Free ("foo111", "'a") $

    60        Free ("bar111", "'a"))

    61    : term*)

    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 *}
wneuper/isa