1.1 --- a/src/Tools/isac/Build_Isac.thy Sun Sep 22 14:51:29 2019 +0200
1.2 +++ b/src/Tools/isac/Build_Isac.thy Sun Sep 22 15:15:37 2019 +0200
1.3 @@ -1,74 +1,79 @@
1.4 -(* Title: build the Isac Mathengine & Knowledge
1.5 +(* Title: build the Isac-Kernel: MathEngine & Knowledge
1.6 Author: Walther Neuper, TU Graz, 100808
1.7 (c) due to copyright terms
1.8
1.9 For creating a heap image of isac see ~~/ROOT.
1.10 -For debugging see text at begin below (theory dependencies!)
1.11 +For debugging see text at begin below, e.g. theory dependencies:
1.12 + ~$ evince file:///home/wneuper/.isabelle/isabisac/browser_info/Unsorted/Isac/session_graph.pdf &
1.13
1.14 ATTENTION: no errors in this theory do not mean that there are no errors in Isac ..
1.15 .. open theories collecting files from folders: CalcElements.thy, ProgLang.thy etc.
1.16 -Errors are rigorously detected when creating a heap.
1.17 +Errors are rigorously detected by isabelle build.
1.18 *)
1.19
1.20 theory Build_Isac
1.21 imports
1.22 -(* see dependency graph
1.23 - ~$ evince file:///home/wneuper/.isabelle/isabisac/browser_info/Unsorted/Isac/session_graph.pdf &
1.24 -*)
1.25 -(* theory KEStore imports Complex_Main
1.26 - ML_file "~~/src/Tools/isac/CalcElements/libraryC.sml"
1.27 - ML_file "~~/src/Tools/isac/CalcElements/rule.sml"
1.28 - ML_file "~~/src/Tools/isac/CalcElements/calcelems.sml"
1.29 - theory ListC imports KEStore
1.30 - ML_file "~~/src/Tools/isac/CalcElements/termC.sml"
1.31 - ML_file "~~/src/Tools/isac/CalcElements/contextC.sml"
1.32 - theory CalcElements imports ListC
1.33 +(* theory KEStore imports Complex_Main
1.34 + ML_file libraryC.sml
1.35 + ML_file rule.sml
1.36 + ML_file calcelems.sml
1.37 + theory CalcElements imports KEStore
1.38 + ML_file termC.sml
1.39 + ML_file contextC.sml
1.40 *) "CalcElements/CalcElements"
1.41
1.42 -(* theory Tools imports CalcElements begin
1.43 - ML_file "~~/src/Tools/isac/ProgLang/calculate.sml"
1.44 - ML_file "~~/src/Tools/isac/ProgLang/rewrite.sml"
1.45 - theory Program imports Tools begin
1.46 - ML_file "~~/src/Tools/isac/ProgLang/program.sml" ? really separate?
1.47 - theory Atools imports Program
1.48 - ML_file "~~/src/Tools/isac/ProgLang/scrtools.sml"
1.49 - theory ProgLang imports Atools
1.50 +(* theory Calculate imports "~~/src/Tools/isac/CalcElements/CalcElements"
1.51 + ML_file calculate.sml
1.52 + theory ListC imports "~~/src/Tools/isac/CalcElements/CalcElements"
1.53 + theory Prog_Expr imports Calculate ListC
1.54 +
1.55 + theory Program imports "~~/src/Tools/isac/CalcElements/CalcElements"
1.56 + theory Prog_Tac imports "~~/src/Tools/isac/CalcElements/CalcElements"
1.57 + theory Tactical imports "~~/src/Tools/isac/CalcElements/CalcElements"
1.58 + theory Auto_Prog imports Program Prog_Tac Tactical begin
1.59 + theory ProgLang imports Prog_Expr Auto_Prog
1.60 + ML_file rewrite.sml
1.61 *) "ProgLang/ProgLang"
1.62 (*
1.63 - ML_file model.sml
1.64 - ML_file mstools.sml
1.65 - ML_file "specification-elems.sml"
1.66 - ML_file istate.sml
1.67 - ML_file tactic.sml
1.68 - ML_file "ctree-basic.sml" (*shift to base in common with Interpret*)
1.69 - ML_file "ctree-access.sml"(*shift to base in common with Interpret*)
1.70 - ML_file "ctree-navi.sml" (*shift to base in common with Interpret*)
1.71 - ML_file ctree.sml (*shift to base in common with Interpret*)
1.72 - ML_file ptyps.sml
1.73 - ML_file generate.sml
1.74 - ML_file calchead.sml
1.75 - ML_file appl.sml
1.76 + theory Input_Descript imports "~~/src/Tools/isac/CalcElements/CalcElements"
1.77 + theory Specify imports "~~/src/Tools/isac/ProgLang/ProgLang" Input_Descript
1.78 + ML_file model.sml
1.79 + ML_file mstools.sml
1.80 + ML_file "specification-elems.sml"
1.81 + ML_file istate.sml
1.82 + ML_file tactic.sml
1.83 + ML_file "ctree-basic.sml" (*shift to base in common with Interpret*)
1.84 + ML_file "ctree-access.sml"(*shift to base in common with Interpret*)
1.85 + ML_file "ctree-navi.sml" (*shift to base in common with Interpret*)
1.86 + ML_file ctree.sml (*shift to base in common with Interpret*)
1.87 + ML_file ptyps.sml
1.88 + ML_file generate.sml
1.89 + ML_file calchead.sml
1.90 + ML_file appl.sml
1.91 *) "Specify/Specify"
1.92 (*
1.93 - ML_file rewtools.sml
1.94 - ML_file script.sml
1.95 - ML_file inform.sml
1.96 - ML_file "lucas-interpreter.sml"
1.97 + theory Interpret imports "~~/src/Tools/isac/Specify/Specify"
1.98 + ML_file rewtools.sml
1.99 + ML_file script.sml
1.100 + ML_file inform.sml
1.101 + ML_file "lucas-interpreter.sml"
1.102 *) "Interpret/Interpret"
1.103 (*
1.104 - ML_file solve.sml
1.105 - ML_file mathengine.sml
1.106 - ML_file "~~/src/Tools/isac/Frontend/messages.sml"
1.107 - ML_file messages.sml
1.108 - ML_file states.sml
1.109 + theory MathEngine imports "~~/src/Tools/isac/Interpret/Interpret"
1.110 + ML_file solve.sml
1.111 + ML_file mathengine.sml
1.112 + ML_file "~~/src/Tools/isac/Frontend/messages.sml"
1.113 + ML_file messages.sml
1.114 + ML_file states.sml
1.115 *) "MathEngine/MathEngine"
1.116 (*
1.117 - ML_file mathml.sml
1.118 - ML_file datatypes.sml
1.119 - ML_file "pbl-met-hierarchy.sml"
1.120 - ML_file "thy-hierarchy.sml"
1.121 - ML_file "interface-xml.sml"
1.122 - ML_file interface.sml
1.123 + theory BridgeLibisabelle imports "~~/src/Tools/isac/MathEngine/MathEngine"
1.124 + ML_file mathml.sml
1.125 + ML_file datatypes.sml
1.126 + ML_file "pbl-met-hierarchy.sml"
1.127 + ML_file "thy-hierarchy.sml"
1.128 + ML_file "interface-xml.sml"
1.129 + ML_file interface.sml
1.130 *) "BridgeLibisabelle/BridgeLibisabelle"
1.131
1.132 "Knowledge/Build_Thydata" (*imports Isac.thy etc*)