1.1 --- a/src/Tools/isac/Build_Isac.thy	Sun Oct 10 14:15:43 2010 +0200
     1.2 +++ b/src/Tools/isac/Build_Isac.thy	Mon Oct 11 12:55:40 2010 +0200
     1.3 @@ -1,13 +1,14 @@
     1.4 -(*  Title:   ~~~/isac/Isac_Mathengine.thy
     1.5 -    Author: Walther Neuper, TU Graz
     1.6 +(*  Title:  build and test isac
     1.7 +    Author: Walther Neuper, TU Graz, 100808
     1.8     (c) due to copyright terms
     1.9  
    1.10 -Code copied from respective parte of Build_Test_Isac.thy
    1.11 -
    1.12  $ cd /usr/local/Isabelle2009-1/src/Tools/isac
    1.13  $ /usr/local/isabisac/bin/isabelle emacs Build_Isac.thy &
    1.14  $ /usr/local/isabisac/bin/isabelle jedit Build_Isac.thy &
    1.15  
    1.16 +create a new Isac heap (via ~~/ROOT.ML) with
    1.17 +$ /usr/local/isabisac/bin/isabelle usedir -b HOL Isac
    1.18 +
    1.19  12345678901234567890123456789012345678901234567890123456789012345678901234567890
    1.20          10        20        30        40        50        60        70        80
    1.21  *)
    1.22 @@ -15,7 +16,7 @@
    1.23  header {* Loading the isac mathengine *}
    1.24  
    1.25  theory Build_Isac
    1.26 -imports Complex_Main "ProgLang/Language" (*"Knowledge/Test"*)
    1.27 +imports Complex_Main "ProgLang/Language" (*"Knowledge/Isac"*)
    1.28  begin
    1.29  
    1.30  ML {* 
    1.31 @@ -88,15 +89,11 @@
    1.32  *)
    1.33    use_thy "Knowledge/Test" (*required _only_ for ROOT.ML !?!*)
    1.34  use_thy "Knowledge/Isac"
    1.35 +
    1.36  ML {* check_guhs_unique := false; *}
    1.37  ML {* tracing "**** isac kernel = math-engine + Knowledge complete ******" *}
    1.38  
    1.39 -
    1.40 -(*
    1.41 -use "../../../test/Tools/isac/Interpret/calchead.sml" (*part.*)
    1.42 -*** get_pbt not found: ["linear","system"]
    1.43 -use"../../../test/Tools/isac/Knowledge/integrate.sml";
    1.44 -*)
    1.45 -
    1.46  end
    1.47  
    1.48 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
    1.49 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)

     2.1 --- a/src/Tools/isac/Build_Test_Isac.thy	Sun Oct 10 14:15:43 2010 +0200
     2.2 +++ b/src/Tools/isac/Build_Test_Isac.thy	Mon Oct 11 12:55:40 2010 +0200
     2.3 @@ -1,11 +1,14 @@
     2.4  (*  Title:  build and test isac
     2.5 -    Author: Walther Neuper 100808
     2.6 +    Author: Walther Neuper, TU Graz, 100808
     2.7     (c) due to copyright terms
     2.8  
     2.9 -$ cd /usr/lo!cal/Isabelle2009-1/src/Tools/isac
    2.10 +$ cd /usr/local/Isabelle2009-1/src/Tools/isac
    2.11  $ /usr/local/isabisac/bin/isabelle emacs Build_Test_Isac.thy &
    2.12  $ /usr/local/isabisac/bin/isabelle jedit Build_Test_Isac.thy &
    2.13  
    2.14 +create a new Isac heap (via ~~/ROOT.ML) with
    2.15 +$ /usr/local/isabisac/bin/isabelle usedir -b HOL Isac
    2.16 +
    2.17  12345678901234567890123456789012345678901234567890123456789012345678901234567890
    2.18          10        20        30        40        50        60        70        80
    2.19  *)
    2.20 @@ -13,81 +16,33 @@
    2.21  header {* Loading the isac mathengine *}
    2.22  
    2.23  theory Build_Test_Isac
    2.24 -imports Complex_Main "ProgLang/Language" (*"Knowledge/Test"*)
    2.25 +imports Complex_Main "ProgLang/Language" "Knowledge/Isac" "Test_Isac"
    2.26  begin
    2.27  
    2.28 -ML {* 
    2.29 -writeln "**** build the isac kernel = math-engine + Knowledge ***********";
    2.30 -writeln "**** build the math-engine *************************************" *}
    2.31 +use_thy "Build_Isac"
    2.32  
    2.33 -ML {* Toplevel.debug := true; *}
    2.34 -use "library.sml"
    2.35 -use "calcelems.sml"
    2.36 -ML {* check_guhs_unique := true *}
    2.37 -
    2.38 -use "ProgLang/termC.sml"
    2.39 -use "ProgLang/calculate.sml"
    2.40 -use "ProgLang/rewrite.sml"
    2.41 -use_thy"ProgLang/Script"    (*ListC, Tools, Script*)
    2.42 -use "ProgLang/scrtools.sml"
    2.43 -use_thy"ProgLang/Language"  (*just for integrating scrtools.sml*)
    2.44 -
    2.45 -use "Interpret/mstools.sml"
    2.46 -use "Interpret/ctree.sml"
    2.47 -use "Interpret/ptyps.sml"
    2.48 -use "Interpret/generate.sml"
    2.49 -use "Interpret/calchead.sml"
    2.50 -use "Interpret/appl.sml"
    2.51 -use "Interpret/rewtools.sml"
    2.52 -use "Interpret/script.sml"
    2.53 -use "Interpret/solve.sml"
    2.54 -use "Interpret/inform.sml"
    2.55 -use "Interpret/mathengine.sml"
    2.56 -
    2.57 -use "xmlsrc/mathml.sml"
    2.58 -use "xmlsrc/datatypes.sml"
    2.59 -use "xmlsrc/pbl-met-hierarchy.sml"
    2.60 -use "xmlsrc/thy-hierarchy.sml" 
    2.61 -use "xmlsrc/interface-xml.sml"
    2.62 -
    2.63 -use "Frontend/messages.sml"
    2.64 -use "Frontend/states.sml"
    2.65 -use "Frontend/interface.sml"
    2.66 -
    2.67 -use "print_exn_G.sml"
    2.68 -ML {* writeln "**** build math-engine complete **************************" *}
    2.69 -
    2.70 -ML {* writeln "**** build the Knowledge *********************************" *}
    2.71 -(**)use_thy "Knowledge/Delete"
    2.72 -use_thy "Knowledge/Descript"
    2.73 -use_thy "Knowledge/Atools"
    2.74 -use_thy "Knowledge/Simplify"
    2.75 -use_thy "Knowledge/Poly"
    2.76 -use_thy "Knowledge/Rational"
    2.77 -use_thy "Knowledge/PolyMinus"
    2.78 -use_thy "Knowledge/Equation"
    2.79 -use_thy "Knowledge/LinEq"
    2.80 -use_thy "Knowledge/Root"
    2.81 -use_thy "Knowledge/RootEq"
    2.82 -use_thy "Knowledge/RatEq"
    2.83 -use_thy "Knowledge/RootRat"
    2.84 -use_thy "Knowledge/RootRatEq"
    2.85 -use_thy "Knowledge/PolyEq"
    2.86 -use_thy "Knowledge/Vect"
    2.87 -use_thy "Knowledge/Calculus"
    2.88 -use_thy "Knowledge/Trig"
    2.89 -use_thy "Knowledge/LogExp"
    2.90 -use_thy "Knowledge/Diff"
    2.91 -use_thy "Knowledge/DiffApp"
    2.92 -use_thy "Knowledge/Integrate"
    2.93 -use_thy "Knowledge/EqSystem"
    2.94 -use_thy "Knowledge/Biegelinie"
    2.95 -use_thy "Knowledge/AlgEin"
    2.96 -use_thy "Knowledge/Test" (*required _only_ for ROOT.ML !?!*)
    2.97 -use_thy "Knowledge/Isac"
    2.98 -ML {* check_guhs_unique := false; *}
    2.99 -ML {* writeln "**** isac kernel = math-engine + Knowledge complete ******" *}
   2.100 +(* PROCEEDING WITH TESTS HERE DOESN'T WORK,
   2.101 +   because the 'imports "Knowledge/Isac" is required; for instance:
   2.102 +use "../../../test/Tools/isac/Interpret/calchead.sml"
   2.103 +*** get_pbt not found: ["linear","system"]
   2.104 +use"../../../test/Tools/isac/Knowledge/integrate.sml";
   2.105 +*)
   2.106  
   2.107  use_thy "Test_Isac"
   2.108  
   2.109 -end
   2.110 \ No newline at end of file
   2.111 +end
   2.112 +
   2.113 +(*=== inhibit exn ?=============================================================
   2.114 +===== inhibit exn ?===========================================================*)
   2.115 +
   2.116 +
   2.117 +(*========== inhibit exn =======================================================
   2.118 +
   2.119 +"########### testcode inserted vvv ###########################################";
   2.120 +"########### testcode inserted ^^^ ###########################################";
   2.121 +
   2.122 +============ inhibit exn =====================================================*)
   2.123 +
   2.124 +
   2.125 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
   2.126 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)

     3.1 --- a/src/Tools/isac/Knowledge/Isac.thy	Sun Oct 10 14:15:43 2010 +0200
     3.2 +++ b/src/Tools/isac/Knowledge/Isac.thy	Mon Oct 11 12:55:40 2010 +0200
     3.3 @@ -19,12 +19,12 @@
     3.4  *}
     3.5  
     3.6  ML {*
     3.7 -(**.set up a list for getting guh + theID for a thm (defined in isabelle).**)
     3.8 +(**set up a list for getting guh + theID for a thm (defined in isabelle).**)
     3.9  
    3.10  (*local*)
    3.11 -    val allthys = Theory.ancestors_of @{theory};            (*116*)
    3.12 -    val isabthys = Theory.ancestors_of first_isac_thy;      (* 86; isa02:58*)
    3.13 -    val isacthys = subtract Theory.eq_thy isabthys allthys; (* 30*)
    3.14 +    val allthys = @{theory} :: Theory.ancestors_of @{theory};
    3.15 +    val isabthys = Theory.ancestors_of first_isac_thy;
    3.16 +    val isacthys = subtract Theory.eq_thy isabthys allthys;
    3.17  
    3.18      val isacrlsthms = ((map (apsnd prop_of)) o
    3.19                         (gen_distinct eq_thmI) o (map rep_thm_G') o flat o 
    3.20 @@ -32,8 +32,8 @@
    3.21      val isacthms = 
    3.22                (flat o (map Theory.axioms_of)) isacthys : (thmID * term) list; 
    3.23  (*in*)
    3.24 +    theory' := (map Context.theory_name isacthys) ~~ isacthys;
    3.25      val rlsthmsNOTisac = gen_diff eq_thmI' (isacrlsthms, isacthms); 
    3.26 -    (*length rlsthmsNOTisac;-->45*)
    3.27  (*end;*)
    3.28  
    3.29  (*.set up the list using 'val first_isac_thy' (see ListC.ML).*)
    3.30 @@ -41,13 +41,15 @@
    3.31  
    3.32  (*.create the hierarchy of theory elements from IsacKnowledge
    3.33     including thms from Isabelle used in rls;
    3.34 -   elements store_*d in any *.ML are not overwritten.*)
    3.35 +   elements store_*d in any *.thy are not overwritten.*)
    3.36  
    3.37  thehier := the_hier (!thehier) (collect_thydata ());
    3.38  tracing("----------------------------------\n" ^
    3.39  	"*** insert: not found ... IS OK : \n" ^
    3.40  	"comes from fill_parents           \n" ^
    3.41  	"----------------------------------\n");
    3.42 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
    3.43 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
    3.44  *}
    3.45  
    3.46  end

     4.1 --- a/src/Tools/isac/ProgLang/scrtools.sml	Sun Oct 10 14:15:43 2010 +0200
     4.2 +++ b/src/Tools/isac/ProgLang/scrtools.sml	Mon Oct 11 12:55:40 2010 +0200
     4.3 @@ -300,7 +300,7 @@
     4.4    | is_calc _ = false;
     4.5  fun op_of_calc (Const ("Script.Calculate",_) $ Free (op_,_)) = op_
     4.6    | op_of_calc (Const ("Script.Calculate",_) $ Free (op_,_) $ _) = op_
     4.7 -  | op_of_calc t = error ("op_of_calc called with"^term2str t);
     4.8 +  | op_of_calc t = error ("op_of_calc called with" ^ term2str t);
     4.9  (*
    4.10   val Script sc = (#scr o rep_rls) Test_simplify;
    4.11   val stacs = stacpbls sc;
    4.12 @@ -313,19 +313,23 @@
    4.13    (filter is_calc) o stacpbls) sc):calc list;
    4.14  *)
    4.15  
    4.16 -(**.for automatic creation of scripts from rls.**)
    4.17 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
    4.18 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
    4.19 +
    4.20 +(** for automatic creation of scripts from rls **)
    4.21  (* naming of identifiers in scripts ???...
    4.22 +   not accepted !!!...
    4.23 +((inst_abs @{theory}) o term_of o the o (parse @{theory})) "(t_::'z) = t_";
    4.24 +((inst_abs @{theory}) o term_of o (the:cterm option -> cterm) o 
    4.25 +     (parse @{theory})) "(_t::'z) = _t";
    4.26 +*)
    4.27  ((inst_abs @{theory}) o term_of o the o (parse @{theory})) "(t::'z) = t";
    4.28  ((inst_abs @{theory}) o term_of o (the:cterm option -> cterm) o 
    4.29       (parse @{theory})) "(t't::'z) = t't";
    4.30  ((inst_abs @{theory}) o term_of o the o (parse @{theory})) "(t_t::'z) = t_t";
    4.31 -(* not accepted !!!...*)
    4.32 -((inst_abs @{theory}) o term_of o the o (parse @{theory})) "(t_::'z) = t_";
    4.33 -((inst_abs @{theory}) o term_of o (the:cterm option -> cterm) o 
    4.34 -     (parse @{theory})) "(_t::'z) = _t";
    4.35 -*)
    4.36 +
    4.37  ((inst_abs @{theory}) o term_of o the o (parse @{theory}))
    4.38 -"Script Stepwise (t::'z) =\
    4.39 +"Script Stepwise (t_t::'z) =\
    4.40          \(Repeat\
    4.41  	\  ((Try (Repeat (Rewrite real_diff_minus False))) @@  \
    4.42  	\   (Try (Repeat (Rewrite add_commute False))) @@ \
    4.43 @@ -333,7 +337,7 @@
    4.44  	\  t_t)";
    4.45  val ScrStep $ _ $ _ =     (*'z not affected by parse: 'a --> real*)
    4.46      ((inst_abs @{theory}) o term_of o the o (parse @{theory}))  
    4.47 -	"Script Stepwise (t::'z) =\
    4.48 +	"Script Stepwise (t_t::'z) =\
    4.49          \(Repeat\
    4.50  	\  ((Try (Repeat (Rewrite real_diff_minus False))) @@  \
    4.51  	\   (Try (Repeat (Rewrite add_commute False))) @@ \
    4.52 @@ -343,12 +347,12 @@
    4.53  are inconsistent !!!*)
    4.54  val ScrStep_inst $ Term $ Bdv $ _=(*'z not affected by parse: 'a --> real*)
    4.55      ((inst_abs @{theory}) o term_of o the o (parse @{theory})) 
    4.56 -	"Script Stepwise_inst (t::'z) (v::real) =\
    4.57 +	"Script Stepwise_inst (t_t::'z) (v::real) =\
    4.58          \(Repeat\
    4.59  	\  ((Try (Repeat (Rewrite_Inst [(bdv,v)] real_diff_minus False))) @@ \
    4.60  	\   (Try (Repeat (Rewrite_Inst [(bdv,v)] add_commute False))) @@\
    4.61  	\   (Try (Repeat (Rewrite_Inst [(bdv,v)] real_mult_commute False)))) \
    4.62 -	\  t)"; 
    4.63 +	\  t_t)"; 
    4.64  val Repeat $ _ =
    4.65      ((inst_abs @{theory}) o term_of o the o (parseN @{theory})) 
    4.66  	"Repeat (Rewrite real_diff_minus False t)";

     5.1 --- a/src/Tools/isac/Test_Isac.thy	Sun Oct 10 14:15:43 2010 +0200
     5.2 +++ b/src/Tools/isac/Test_Isac.thy	Mon Oct 11 12:55:40 2010 +0200
     5.3 @@ -100,17 +100,24 @@
     5.4  (*
     5.5  	use"eqsystem.sml";
     5.6  *)
     5.7 -use "../../../test/Tools/isac/Knowledge/polyminus.sml"; (*part.*)
     5.8 +use "../../../test/Tools/isac/Knowledge/polyminus.sml"; (* part. *)
     5.9  (*
    5.10   	use"vect.sml";  
    5.11   	use"diffapp.sml";
    5.12  	use"biegelinie.sml";
    5.13  	use"algein.sml";
    5.14 +*)
    5.15 +ML {*print_depth 5*}
    5.16 +use "../../../test/Tools/isac/Knowledge/isac.sml"; (**)
    5.17 +
    5.18 +ML {*111*}
    5.19 +
    5.20 +(*
    5.21   	cd "../..";
    5.22  *)
    5.23  (* TODO
    5.24  use_thy "../../Tools/isac/ADDTESTS/file-depend/Build_Test"
    5.25 -
    5.26 +:
    5.27  *** Could not find theory file "Foo_Language.thy" in "1language", "/usr/local/isabisac/test/Tools/isac", ".", "$ISABELLE_HOME/src/HOL/Library"
    5.28  *** Theory loader: the error(s) above occurred while examining theory "Foo_Language"
    5.29  

     6.1 --- a/test/Tools/isac/Knowledge/Isac.thy	Sun Oct 10 14:15:43 2010 +0200
     6.2 +++ b/test/Tools/isac/Knowledge/Isac.thy	Mon Oct 11 12:55:40 2010 +0200
     6.3 @@ -1,5 +1,6 @@
     6.4  (*  Title:  test/Tools/isac/Isac.thy
     6.5 -    Author: Walther Neuper, TU Graz
     6.6 +    Author: Walther Neuper, TU Graz, 2010
     6.7 +    (c) due to copyright terms
     6.8  
     6.9  12345678901234567890123456789012345678901234567890123456789012345678901234567890
    6.10          10        20        30        40        50        60        70        80
    6.11 @@ -7,7 +8,8 @@
    6.12  
    6.13  theory Isac imports Complex_Main (*TODO Build_Isac*) begin
    6.14  
    6.15 -section {* rlsthmsNOTisac from Isabelle2002-isac are all applicable to reals *}
    6.16 +text {* rlsthmsNOTisac from Isabelle2002-isac are all applicable to reals;
    6.17 +        the leading parts of longnames can be dropped with some exceptions. *}
    6.18  
    6.19  lemma "take n (x # xs) = (case n of 0 => [] | Suc m => x # take m xs)"          by (rule List.take_Cons)
    6.20  lemma "t = (t::real)"                                                           by (rule HOL.refl)

     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/test/Tools/isac/Knowledge/isac.sml	Mon Oct 11 12:55:40 2010 +0200
     7.3 @@ -0,0 +1,42 @@
     7.4 +(*  Title:  test/Tools/isac/Isac.thy
     7.5 +    Author: Walther Neuper, TU Graz, 2010
     7.6 +    (c) due to copyright terms
     7.7 +
     7.8 +12345678901234567890123456789012345678901234567890123456789012345678901234567890
     7.9 +        10        20        30        40        50        60        70        80
    7.10 +*)
    7.11 +
    7.12 +"--------------------------------------------------------";
    7.13 +"--------------------------------------------------------";
    7.14 +"table of contents --------------------------------------";
    7.15 +"--------------------------------------------------------";
    7.16 +"-------- fill ! theory' with data ----------------------";
    7.17 +"--------------------------------------------------------";
    7.18 +"--------------------------------------------------------";
    7.19 +"--------------------------------------------------------";
    7.20 +
    7.21 +
    7.22 +"-------- fill ! theory' with data ----------------------";
    7.23 +"-------- fill ! theory' with data ----------------------";
    7.24 +"-------- fill ! theory' with data ----------------------";
    7.25 +    val allthys = theory "Isac"(**@{theory}*) ::
    7.26 +                  Theory.ancestors_of (*@{theory}*) (theory "Isac");
    7.27 +    val isabthys = Theory.ancestors_of first_isac_thy;
    7.28 +    val isacthys = subtract Theory.eq_thy isabthys allthys;
    7.29 +"--------------------------------------------------------";
    7.30 +map Context.theory_name allthys;
    7.31 +map Context.theory_name isabthys;
    7.32 +if map Context.theory_name isacthys = 
    7.33 +   ["Isac", "Test", "AlgEin", "Biegelinie", "DiffApp", "Vect", "PolyMinus",
    7.34 +    "EqSystem", "Integrate", "Diff", "LogExp", "Trig", "Calculus", "PolyEq",
    7.35 +    "RootRatEq", "RootRat", "RatEq", "RootEq", "LinEq", "Root", "Equation",
    7.36 +    "Rational", "Poly", "Simplify", "Atools", "Descript", "Delete",
    7.37 +    "Language", "Script", "Tools", "ListC"] then ()
    7.38 +else error "isac.sml: names of isac theories changed";
    7.39 +"--------------------------------------------------------";
    7.40 +    val _ = theory' := (map Context.theory_name isacthys) ~~ isacthys;
    7.41 +length (! theory');
    7.42 +
    7.43 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
    7.44 +
    7.45 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)

     8.1 --- a/test/Tools/isac/Knowledge/poly.sml	Sun Oct 10 14:15:43 2010 +0200
     8.2 +++ b/test/Tools/isac/Knowledge/poly.sml	Mon Oct 11 12:55:40 2010 +0200
     8.3 @@ -558,13 +558,3 @@
     8.4  val t2 = str2term "3 * a + (2 * b + 3 * b)";
     8.5  
     8.6  ===== inhibit exn ?===========================================================*)
     8.7 -
     8.8 -
     8.9 -(*========== inhibit exn =======================================================
    8.10 -============ inhibit exn =====================================================*)
    8.11 -
    8.12 -(*========== inhibit exn ?======================================================
    8.13 -============ inhibit exn ?====================================================*)
    8.14 -
    8.15 -(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
    8.16 --.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)