(* Title:   test/Tools/isac/ADDTESTS/file-depend

   Author:  Walther Neuper

*)

header {* Test file dependencies analogous to ISAC

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

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

*}

(*----------------------------------------------------------------------------

theory Build_Test 

imports 

  Complex_Main 

  "1language/Foo_Language"

  "3knowledge/Foo_KnowALL"

begin

----------------------------------------------------------------------------*)

theory Build_Test 

imports 

  Complex_Main 

begin

  use     "0foolibrary.ML"                    ML {* foolibrhs *}

  use_thy "1language/Foo_Language"          (*ML {* @{const fooprog} *}*)

  use     "2interpreter/2foointerpreter.ML"   ML {* foointerpret *}

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

  use     "2interpreter/2foointerpreter.ML"

  use_thy "3knowledge/Foo_Know111"

  use_thy "3knowledge/Foo_Know222"

  use_thy "3knowledge/Foo_KnowALL"

*}

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

ML {* 

val trm = Syntax.read_term_global @{theory Foo_Know111} 

  "fooprog (foo111 = bar111)";

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

val trm = Syntax.read_term_global @{theory Foo_Know222} 

  "fooprog (foo222 = bar222)";

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

*}

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

ML {*

val trm = Syntax.read_term_global @{theory Foo_Know111} 

  "fooprog (foo222 = bar222)";

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

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

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

   : term*)

val trm = Syntax.read_term_global @{theory Foo_Know222} 

  "fooprog (foo111 = bar111)";

(*val trm =

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

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

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

   : term*)

*}

text {* dir structure reflects ISAC, see Build_Isac.thy:

/file-depend/0foolibrary.ML

/file-depend/Build_Test.thy

/file-depend/README

/file-depend/1language/Foo_Language.thy

/file-depend/2interpreter/2foointerpreter.ML

/file-depend/3knowledge/Foo_Know111.thy

/file-depend/3knowledge/Foo_Know222.thy

/file-depend/3knowledge/Foo_KnowALL.thy

*}