wneuper/isa: src/Tools/isac/BridgeJEdit/Calculation.thy@3c06f59b78d6

     1 (*  Title:      src/Tools/isac/BridgeJEdit/Calculation.thy

     2     Author:     Walther Neuper, JKU Linz

     3     (c) due to copyright terms

     5 Outer syntax for Isabelle/Isac's Calculation.

     6 *)

     8 theory Calculation

     9 imports

    10 (**) "~~/src/Tools/isac/Knowledge/Build_Thydata"   (*remove after devel.of BridgeJEdit*)

    11 (** )"~~/src/Tools/isac/MathEngine/MathEngine"  ( *activate after devel.of BridgeJEdit*)

    12 (**) "HOL-SPARK.SPARK"                             (*remove after devel.of BridgeJEdit*)

    13 keywords

    14     "Example" :: thy_load ("str") (* "spark_vc" :: thy_goal *)

    15   and "Problem" :: thy_decl (* root-problem + recursively in Solution;

    16                                "spark_vc" :: thy_goal *)

    17   and "Specification" "Model" :: diag

    18   and "References" "Solution" :: prf_chain (* structure only *)

    19   and "Where" "Given" "Find" "Relate" :: prf_chain (* await input of term, cp.from "from".."have" *)

    20 (*and "Where" (* only output, preliminarily *)*)

    21   and "RTheory" :: prf_chain (* await input of string; "R" distingues "Problem".."RProblem" *)

    22   and "RProblem" "RMethod" :: prf_chain (* await input of string list *)

    23   and "Tactic" (* optional for each step 0..end of calculation *)

    24 begin

    25 declare [[ML_print_depth = 99999]]

    26 (**)ML_file parseC.sml(**)

    27 (**)ML_file preliminary.sml(**)

    30 section \<open>new code for Outer_Syntax Example, Problem, ...\<close>

    31 text \<open>

    32   code for Example, Problem shifted into structure Preliminary.

    33 \<close>

    35 subsubsection \<open>cp from Pure.thy\<close>

    36 ML \<open>

    37 \<close> ML \<open> (* for "from" ~~ "Given:" *)

    38 (* original *)

    39 val facts = Parse.and_list1 Parse.thms1;

    40 facts: (Facts.ref * Token.src list) list list parser;

    41 \<close> ML \<open>

    42 val facts =

    43   (writeln "####-## from parser";

    44     Parse.$$$ ":" |-- Parse.and_list1 Parse.thms1)(** ) --| Parse.$$$ "Where"( **);

    45 facts: (Facts.ref * Token.src list) list list parser;

    46 \<close> ML \<open>

    47 \<close> ML \<open>

    48 \<close>

    50 subsubsection \<open>tools to analyse parsing in Outer_Syntax >> \<close>

    51 ML \<open>

    52 \<close> text \<open> (*original basics.ML*)

    53 op |>> : ('a * 'b) * ('a -> 'c) -> 'c * 'b;

    54 fun (x, y) |>> f = (f x, y);

    55 \<close> text \<open> (*original scan.ML*)

    56 op >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c;                              (*---vvv*)

    57 fun (scan >> f) xs = scan xs |>> f;

    58 \<close> ML \<open>

    59 \<close> ML \<open> (*cp.from originals*)

    60 infix 3 @>>;

    61 fun (scan @>> f) xs = scan xs |>> f;

    62 op @>> : ('a        -> 'b * 'c)        * ('b -> 'd) -> 'a        -> 'd * 'c;        (*---^^^*)

    63 \<close> ML \<open> (*appl.to parser*)

    64 op @>> : (Token.src -> 'b * Token.src) * ('b -> 'd) -> Token.src -> 'd * Token.src; (*---^^^*)

    65 \<close> ML \<open>

    66 \<close> ML \<open> (*add analysis*)

    67 \<close> text \<open>

    68 datatype T = Pos of (int * int * int) * Properties.T;

    70 fun s_to_string (Pos ((line, offset, end_offset), _)) = ("Pos ((" ^

    71   string_of_int line ^ ", " ^ string_of_int offset ^ ", " ^ string_of_int end_offset ^ "), [_])")

    73 s_to_string: src -> string

    74 \<close> text \<open>

    75 datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot

    76 \<close> ML \<open>

    77 Token.pos_of;        (*^^^^^^^^^^^^^^^*)

    78 Token.end_pos_of;                      (*^^^^^^^^^^^^^*)

    79 Token.unparse;                                            (*^^^^^^^^^^^^^*)

    80 \<close> ML \<open>

    81 fun string_of_tok tok = ("\nToken ((" ^

    82   Position.to_string (Token.pos_of tok) ^ ", " ^

    83   Position.to_string (Token.end_pos_of tok) ^ "), " ^

    84   Token.unparse tok ^ ", _)")

    85 \<close> ML \<open>

    86 fun string_of_toks toks = fold (curry op ^) (map string_of_tok toks |> rev |> separate ", ") "";

    87 string_of_toks:    Token.src -> string;

    88 \<close> ML \<open>

    89 Token.s_to_string: Token.src -> string; (*<-- string_of_toks WN*)

    90 \<close> ML \<open>

    91 fun (scan @>> f) xs = (@{print}{a = "_ >> ", toks = xs(*GIVES\<rightarrow>"?"*)}; scan xs) |>> f;

    92 fun (scan @>> f) xs = (writeln ("toks= " ^ Token.s_to_string xs);      scan xs) |>> f;

    93 op @>> : (Token.src -> 'b * Token.src) * ('b -> 'd) -> Token.src -> 'd * Token.src; (*---^^^*)

    94 \<close> ML \<open>

    95 op @>> : (Token.T list -> 'a * 'b) * ('a -> 'c) -> Token.T list -> 'c * 'b

    96 \<close> ML \<open>

    97 \<close> ML \<open> (*Scan < Token in bootstrap, thus we take Token.s_to_string as argument of >> *)

    98 infix 3 @@>>;

    99 \<close> ML \<open>

   100 fun ((write, scan) @@>> f) xs = (write xs;                             scan xs) |>> f;

   101 op @@>> : (('a -> 'b) * ('a -> 'c * 'd)) * ('c -> 'e) -> 'a -> 'e * 'd

   102 \<close> ML \<open>

   103 \<close> ML \<open>

   104 \<close> ML \<open>

   105 \<close> ML \<open>

   106 \<close>

   109 subsubsection \<open>TODO\<close>

   110 ML \<open>

   111 \<close> ML \<open>

   112 \<close> ML \<open>

   113 \<close> ML \<open>

   114 \<close>

   116 section \<open>setup command_keyword + preliminary test\<close>

   117 ML \<open>

   118 \<close> ML \<open>

   119 val _ =

   120   Outer_Syntax.command \<^command_keyword>\<open>Example\<close> "start a Calculation from a Formalise-file"

   121     (Resources.provide_parse_files "Example" -- Parse.parname

   122       >> (Toplevel.theory o           (*vvvvvvvvvvvvvvvvvvvv--- HACK makes test independent from session Isac*)

   123         (Preliminary.load_formalisation @{theory Biegelinie} ParseC.formalisation)) );

   124 \<close> ML \<open>

   125 (Toplevel.theory o (Preliminary.load_formalisation @{theory Biegelinie} ParseC.formalisation))

   126 :

   127   (theory -> Token.file list * theory) * (*_a*)Token.T ->

   128     Toplevel.transition -> Toplevel.transition

   129 (*  ^^^^^^^^^^^^^^^^^^^    ^^^^^^^^^^^^^^^^^^^*)

   130 \<close> ML \<open>

   131 val _ =

   132   Outer_Syntax.command \<^command_keyword>\<open>Problem\<close>

   133     "start a Specification, either from scratch or from preceding 'Example'"

   134 (** )(ParseC.problem >> (Toplevel.theory o Preliminary.init_specify));( **)

   135 (**)((writeln o Token.s_to_string, ParseC.problem_headline)

   136       @@>> (Toplevel.theory o Preliminary.init_specify));(**)

   137 \<close> ML \<open>

   138 Preliminary.init_specify: ParseC.problem_headline -> theory -> theory;

   139 (Toplevel.theory o Preliminary.init_specify)

   140   : ParseC.problem_headline -> Toplevel.transition -> Toplevel.transition;

   141 \<close> ML \<open>

   142 (**)                   Preliminary.init_specify: ParseC.problem_headline -> theory -> theory;(**)

   143 (*                                                                          ^^^^^^    ^^^^^^*)

   144 (**)(Toplevel.theory o Preliminary.init_specify):

   145       ParseC.problem_headline -> Toplevel.transition -> Toplevel.transition;(**)

   146 (*                               ^^^^^^^^^^^^^^^^^^^    ^^^^^^^^^^^^^^^^^^^*)

   147 \<close> ML \<open>

   148 \<close> ML \<open>

   149 OMod_Data.get

   150 \<close> ML \<open>

   151 fun dummy (_(*":"*): string) thy =

   152   let

   153     val refs' = Refs_Data.get thy

   154     val o_model = OMod_Data.get thy

   155     val i_model = IMod_Data.get thy

   156     val _ =

   157       @{print} {a = "### dummy Specification", refs = refs', o_model = o_model, i_model = i_model}

   158   in

   159     thy

   160   end;

   161 \<close> ML \<open>

   162 (Toplevel.theory o dummy): string -> Toplevel.transition -> Toplevel.transition

   163 \<close> ML \<open>

   164 val _ =

   165 (*Outer_Syntax.command @{command_keyword ISAC} "embedded ISAC language"

   166     (Parse.input Parse.cartouche >> (fn input =>

   167       Toplevel.keep (fn _ => ignore (ML_Lex.read_source (*true*) input))))

   168 *)Outer_Syntax.command \<^command_keyword>\<open>Specification\<close> "Specification dummy"

   169     ((writeln o Token.s_to_string, Parse.$$$ ":") @@>> (Toplevel.theory o dummy))

   170 \<close> ML \<open>

   171 val _ =

   172   Outer_Syntax.command \<^command_keyword>\<open>Model\<close> "Model dummy"

   173     ((writeln o Token.s_to_string, Parse.$$$ ":") @@>> (Toplevel.theory o dummy))

   174 \<close> ML \<open>

   175 val _ =

   176   Outer_Syntax.command \<^command_keyword>\<open>Given\<close> "input Given items to the Model of a Specification"

   177 (*                                (facts    >> (Toplevel.proof o Proof.from_thmss_cmd));*)

   178     ((writeln o Token.s_to_string, facts) @@>> (Toplevel.proof o Proof.from_thmss_cmd));

   179 val _ =

   180   Outer_Syntax.command \<^command_keyword>\<open>Where\<close> "input Find items to the Model of a Specification"

   181     (facts @>> (Toplevel.proof o Proof.from_thmss_cmd));

   182 val _ =

   183   Outer_Syntax.command \<^command_keyword>\<open>Find\<close> "input Find items to the Model of a Specification"

   184     (facts @>> (Toplevel.proof o Proof.from_thmss_cmd));

   185 val _ =

   186   Outer_Syntax.command \<^command_keyword>\<open>Relate\<close> "input Relate items to the Model of a Specification"

   187     (facts @>> (Toplevel.proof o Proof.from_thmss_cmd));

   188 \<close> ML \<open>

   189 (Toplevel.proof o Proof.from_thmss_cmd)

   190 :

   191   (Facts.ref * Token.src list) list list -> Toplevel.transition -> Toplevel.transition

   192 (*                                          ^^^^^^^^^^^^^^^^^^^    ^^^^^^^^^^^^^^^^^^^*)

   193 \<close> ML \<open>

   194 val _ =

   195   Outer_Syntax.command @{command_keyword References} "References dummy"

   196     (Parse.$$$ ":" >> (fn _ => Toplevel.keep (fn _ => ignore (writeln ""))));

   197 val _ =

   198   Outer_Syntax.command @{command_keyword RTheory} "RTheory dummy"

   199     (Parse.$$$ ":" -- Parse.string

   200       >> (fn _ => Toplevel.keep (fn _ => ignore (writeln ""))));

   201 val _ =

   202   Outer_Syntax.command @{command_keyword RProblem} "RProblem dummy"

   203    (Parse.$$$ ":" -- (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]")

   204     >> (fn _ => Toplevel.keep (fn _ => ignore (writeln ""))));

   205 val _ =

   206   Outer_Syntax.command @{command_keyword RMethod} "RMethod dummy"

   207    (Parse.$$$ ":" -- (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]")

   208     >> (fn _ => Toplevel.keep (fn _ => ignore (writeln ""))));

   209 val _ =

   210   Outer_Syntax.command @{command_keyword Solution} "Solution dummy"

   211     (Parse.$$$ ":" >> (fn _ => Toplevel.keep (fn _ => ignore (writeln ""))));

   212 \<close> ML \<open>

   213 \<close> ML \<open>

   214 \<close> text \<open> NEWS 2014

   215 * ML antiquotation @ {here} refers to its source position, which is

   216 occasionally useful for experimentation and diagnostic purposes.

   217 \<close> ML \<open>

   218 @{here}(*val it = {offset=8, end_offset=12, id=-4402}: Position.T*)

   219 \<close> ML \<open>

   220 \<close>

   222 subsection \<open>test runs with test-Example\<close>

   223 (**)

   224 Example \<open>/usr/local/isabisac/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70\<close>

   226 Problem ("Biegelinie", ["Biegelinien"])

   227 (*1 collapse* )

   228   Specification:

   229   (*2 collapse*)

   230     Model:

   231       Given: "Traegerlaenge " "Streckenlast " (*Bad context for command "Given"\<^here> -- using reset state*)

   232       Where: "q_0 ist_integrierbar_auf {| 0, L |}" "0 < L"

   233       Find: "Biegelinie "

   234       Relate: "Randbedingungen "

   235     References:

   236       (*3 collapse*)

   237       RTheory: ""

   238       RProblem: ["", ""]

   239       RMethod: ["", ""]

   240       (*3 collapse*)

   241   (*2 collapse*)

   242   Solution:

   243 ( * 1 collapse*)

   244 (*

   245   compare click on above Given: "Traegerlaenge ", "Streckenlast "

   246   with click on from \<open>0 < d\<close> in SPARK/../Greatest_Common_Divisorthy

   247 *)

   249 subsection \<open><Output> BY CLICK ON Problem..Given: Position, command-range?\<close>

   250 subsubsection \<open>on Problem\<close>

   251 text \<open>

   252 -----------------v BEGIN ---------------vv END OF -----v

   253 Token ((Pos ((0, 9, 10), [_]), Pos ((0, 10, 0), [_])), (, _),

   254 Token ((Pos ((0, 10, 22), [_]), Pos ((0, 22, 0), [_])), "Biegelinie", _),  //INCLUDING ""

   255 Token ((Pos ((0, 22, 23), [_]), Pos ((0, 23, 0), [_])), ,, _),

   256 Token ((Pos ((0, 24, 25), [_]), Pos ((0, 25, 0), [_])), [, _),

   257 Token ((Pos ((0, 25, 38), [_]), Pos ((0, 38, 0), [_])), "Biegelinien", _),

   258 Token ((Pos ((0, 38, 39), [_]), Pos ((0, 39, 0), [_])), ], _),

   259 Token ((Pos ((0, 39, 40), [_]), Pos ((0, 40, 0), [_])), ), _)

   260 {a = "//--- Spark_Commands.init_specify", headline =

   261  (((("(", "Biegelinie"), ","), ["Biegelinien"]), ")")} (line 119 of "~~/src/Tools/isac/BridgeJEdit/preliminary.sml")

   262 \<close>

   263 subsubsection \<open>on Specification:\<close>

   264 text \<open>

   265 -----------------vv BEGIN ---------------vv END OF -----v

   266 Token ((Pos ((0, 14, 15), [_]), Pos ((0, 15, 0), [_])), :, _)

   267 Bad context for command "Specification" -- using reset state

   268 \<close>

   269 subsubsection \<open>on Model:\<close>

   270 text \<open>

   271 -----------------v BEGIN --------------v END OF -----v

   272 Token ((Pos ((0, 6, 7), [_]), Pos ((0, 7, 0), [_])), :, _)

   273 \<close>

   274 subsubsection \<open>on Given:\<close>

   275 text \<open>COMPARE Greatest_Common_Divisor.thy

   276 subsubsection \<open>click on "from \<open>0 < d\<close>"\<close>

   278               line * offset * end_offset

   279        Symbol_Pos.text      * Position.range)* (kind * string) * slot

   280 -----------------------------------------------------------------------------------

   281 Token ((Pos ((0, 6, 7), [_]), Pos ((0, 7, 0), [_])), :, _),

   282 Token ((Pos ((0, 8, 24), [_]), Pos ((0, 24, 0), [_])), "Traegerlaenge ", _),

   283 Token ((Pos ((0, 25, 40), [_]), Pos ((0, 40, 0), [_])), "Streckenlast ", _),

   284 ---------------------------------------------------------- ?WHY 2nd TURN..

   285 Token ((Pos ((0, 6, 7), [_]), Pos ((0, 7, 0), [_])), :, _),

   286 Token ((Pos ((0, 8, 24), [_]), Pos ((0, 24, 0), [_])), "Traegerlaenge ", _),

   287 Token ((Pos ((0, 25, 40), [_]), Pos ((0, 40, 0), [_])), "Streckenlast ", _),

   288 Token ((Pos ((0, 40, 0), [_]), Pos ((0, 0, 0), [_])), , _)

   289 \<close>

   290 subsubsection \<open>on Where:\<close>

   291 text \<open>

   292 toks=

   293 Token ((Pos ((0, 6, 7), [_]), Pos ((0, 7, 0), [_])), :, _),

   294 Token ((Pos ((0, 8, 45), [_]), Pos ((0, 45, 0), [_])), "q_0 ist_integrierbar_auf {| 0, L |}", _),

   295 Token ((Pos ((0, 46, 53), [_]), Pos ((0, 53, 0), [_])), "0 < L", _)

   296 toks=

   297 Token ((Pos ((0, 6, 7), [_]), Pos ((0, 7, 0), [_])), :, _),

   298 Token ((Pos ((0, 8, 45), [_]), Pos ((0, 45, 0), [_])), "q_0 ist_integrierbar_auf {| 0, L |}", _),

   299 Token ((Pos ((0, 46, 53), [_]), Pos ((0, 53, 0), [_])), "0 < L", _),

   300 Token ((Pos ((0, 53, 0), [_]), Pos ((0, 0, 0), [_])), , _)

   301 \<close>

   302 subsubsection \<open>on Find:\<close>

   303 text \<open>

   304 toks=

   305 Token ((Pos ((0, 5, 6), [_]), Pos ((0, 6, 0), [_])), :, _),

   306 Token ((Pos ((0, 7, 20), [_]), Pos ((0, 20, 0), [_])), "Biegelinie ", _)

   307 toks=

   308 Token ((Pos ((0, 5, 6), [_]), Pos ((0, 6, 0), [_])), :, _),

   309 Token ((Pos ((0, 7, 20), [_]), Pos ((0, 20, 0), [_])), "Biegelinie ", _),

   310 Token ((Pos ((0, 20, 0), [_]), Pos ((0, 0, 0), [_])), , _)

   311 \<close>

   312 subsubsection \<open>on Relate:\<close>

   313 text \<open>

   314 toks=

   315 Token ((Pos ((0, 7, 8), [_]), Pos ((0, 8, 0), [_])), :, _),

   316 Token ((Pos ((0, 9, 27), [_]), Pos ((0, 27, 0), [_])), "Randbedingungen ", _)

   317 toks=

   318 Token ((Pos ((0, 7, 8), [_]), Pos ((0, 8, 0), [_])), :, _),

   319 Token ((Pos ((0, 9, 27), [_]), Pos ((0, 27, 0), [_])), "Randbedingungen ", _),

   320 Token ((Pos ((0, 27, 0), [_]), Pos ((0, 0, 0), [_])), , _)

   321 \<close>

   322 subsubsection \<open>on References, RTheory, RProblem, RMethod, Solution:\<close>

   323 text \<open>

   324 NO OUTPUT

   325 \<close>

   328 subsection \<open><Output> BY CLICK ON Problem..Solution: session Isac\<close>

   329 subsubsection \<open>(1)AFTER session Isac (after ./zcoding-to-test.sh)\<close>

   330 text \<open>

   331   Comparison of the two subsections below:

   332 (1) <Output> AFTER session Isac (after ./zcoding-to-test.sh) WITH click on Problem..Specification:

   333   ((WHILE click ON Example SHOWS NO ERROR))

   334 # headline =  ..(1) == (2)                                                     ..PARSED + Specification

   335 # i_model = Inc  ..IN 4 ELEMENTS, (1) == (2)                                   ..?!? FROM PARSED ?!?

   336 # o_model = COMPLETE WITH 7 ELEMENTS                                           ..FROM Example

   337 # refs = ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"])..FROM References

   339 (2) <Output> WITHOUT session Isac (after ./ztest-to-coding.sh) WITH click on Problem..Specification:

   340   ((WHILE click ON Example SHOWS !!! ERROR))

   341 # headline =  ..(1) == (2)                                                     ..PARSED + Specification

   342 # i_model = Inc  ..IN 4 ELEMENTS, (1) == (2)                                   ..?!? FROM PARSED ?!?

   343 # o_model = []                                                                 ..NO Example

   344 # refs = ("Biegelinie", ["Biegelinien"], ["empty_meth_id"])                    ..FROM headline ONLY

   345 \<close>

   347 subsubsection \<open>(2) WITHOUT session Isac (AFTER ./ztest-to-coding.sh)\<close>

   348 text \<open>

   349 {a = "//--- Spark_Commands.init_specify", headline =

   350  (((((("(", "Biegelinie"), ","), ["Biegelinien"]), ")"),

   351    ((((("Specification", ":"),

   352        ((((((((((((((("Model", (("", ""), "")), ":"), "Given"), ":"), ["<markup>", "<markup>"]),

   353                  "Where"),

   354                 ":"),

   355                ["<markup>", "<markup>"]),

   356               "Find"),

   357              ":"),

   358             "<markup>"),

   359            "Relate"),

   360           ":"),

   361          ["<markup>"]),

   362         (("References", ":"),

   363          (((((((("RTheory", ":"), ""), "RProblem"), ":"), ["", ""]), "RMethod"), ":"), ["", ""])))),

   364       "Solution"),

   365      ":"),

   366     [])),

   367   "")}

   368 {a = "init_specify", i_model =

   369  [(0, [], false, "#Given",

   370    Inc ((Const ("Biegelinie.Traegerlaenge", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),

   371   (0, [], false, "#Given",

   372    Inc ((Const ("Biegelinie.Streckenlast", "real \<Rightarrow> una"), []), (Const ("empty", "??.'a"), []))),

   373   (0, [], false, "#Find",

   374    Inc ((Const ("Biegelinie.Biegelinie", "(real \<Rightarrow> real) \<Rightarrow> una"), []),

   375         (Const ("empty", "??.'a"), []))),

   376   (0, [], false, "#Relate",

   377    Inc ((Const ("Biegelinie.Randbedingungen", "bool list \<Rightarrow> una"), []),

   378         (Const ("empty", "??.'a"), [])))],

   379  o_model = [], refs = ("Biegelinie", ["Biegelinien"], ["empty_meth_id"])}

   380 ### Proof_Context.gen_fixes

   381 ### Proof_Context.gen_fixes

   382 ### Proof_Context.gen_fixes

   383 ### Syntax_Phases.check_terms

   384 ### Syntax_Phases.check_typs

   385 ### Syntax_Phases.check_typs

   386 ### Syntax_Phases.check_typs

   387 ## calling Output.report

   388 #### Syntax_Phases.check_props

   389 ### Syntax_Phases.check_terms

   390 ### Syntax_Phases.check_typs

   391 ### Syntax_Phases.check_typs

   392 ## calling Output.report

   393 #### Syntax_Phases.check_props

   394 ### Syntax_Phases.check_terms

   395 ### Syntax_Phases.check_typs

   396 ### Syntax_Phases.check_typs

   397 ## calling Output.report

   398 #### Syntax_Phases.check_props

   399 ### Syntax_Phases.check_terms

   400 ### Syntax_Phases.check_typs

   401 ### Syntax_Phases.check_typs

   402 ## calling Output.report

   403 #### Syntax_Phases.check_props

   404 ### Syntax_Phases.check_terms

   405 ### Syntax_Phases.check_typs

   406 ### Syntax_Phases.check_typs

   407 ## calling Output.report

   408 #### Syntax_Phases.check_props

   409 ### Syntax_Phases.check_terms

   410 ### Syntax_Phases.check_typs

   411 ### Syntax_Phases.check_typs

   412 ## calling Output.report

   413 #### Syntax_Phases.check_props

   414 ### Syntax_Phases.check_terms

   415 ### Syntax_Phases.check_typs

   416 ### Syntax_Phases.check_typs

   417 ## calling Output.report

   418 #### Syntax_Phases.check_props

   419 ### Syntax_Phases.check_terms

   420 ### Syntax_Phases.check_typs

   421 ### Syntax_Phases.check_typs

   422 ## calling Output.report

   423 #### Syntax_Phases.check_props

   424 ### Syntax_Phases.check_terms

   425 ### Syntax_Phases.check_typs

   426 ### Syntax_Phases.check_typs

   427 ## calling Output.report

   428 #### Syntax_Phases.check_props

   429 ### Syntax_Phases.check_terms

   430 ### Syntax_Phases.check_typs

   431 ### Syntax_Phases.check_typs

   432 ## calling Output.report

   433 #### Syntax_Phases.check_props

   434 ### Syntax_Phases.check_terms

   435 ### Syntax_Phases.check_typs

   436 ### Syntax_Phases.check_typs

   437 ## calling Output.report

   438 #### Syntax_Phases.check_props

   439 ### Syntax_Phases.check_terms

   440 ### Syntax_Phases.check_typs

   441 ### Syntax_Phases.check_typs

   442 ## calling Output.report

   443 #### Syntax_Phases.check_props

   444 ### Syntax_Phases.check_terms

   445 ### Syntax_Phases.check_typs

   446 ### Syntax_Phases.check_typs

   447 ## calling Output.report

   448 #### Syntax_Phases.check_props

   449 ### Syntax_Phases.check_terms

   450 ### Syntax_Phases.check_typs

   451 ### Syntax_Phases.check_typs

   452 ## calling Output.report

   453 #### Syntax_Phases.check_props

   454 ### Syntax_Phases.check_terms

   455 ### Syntax_Phases.check_typs

   456 ### Syntax_Phases.check_typs

   457 ## calling Output.report

   458 #### Syntax_Phases.check_props

   459 ### Syntax_Phases.check_terms

   460 ### Syntax_Phases.check_typs

   461 ### Syntax_Phases.check_typs

   462 ## calling Output.report

   463 #### Syntax_Phases.check_props

   464 ### Syntax_Phases.check_terms

   465 ### Syntax_Phases.check_typs

   466 ### Syntax_Phases.check_typs

   467 ## calling Output.report

   468 #### Syntax_Phases.check_props

   469 ### Syntax_Phases.check_terms

   470 ### Syntax_Phases.check_typs

   471 ### Syntax_Phases.check_typs

   472 ## calling Output.report

   473 #### Syntax_Phases.check_props

   474 ### Syntax_Phases.check_terms

   475 ### Syntax_Phases.check_typs

   476 ### Syntax_Phases.check_typs

   477 ## calling Output.report

   478 #### Syntax_Phases.check_props

   479 ### Syntax_Phases.check_terms

   480 ### Syntax_Phases.check_typs

   481 ### Syntax_Phases.check_typs

   482 ## calling Output.report

   483 #### Syntax_Phases.check_props

   484 ### Syntax_Phases.check_terms

   485 ### Syntax_Phases.check_typs

   486 ### Syntax_Phases.check_typs

   487 ## calling Output.report

   488 #### Syntax_Phases.check_props

   489 ### Syntax_Phases.check_terms

   490 ### Syntax_Phases.check_typs

   491 ### Syntax_Phases.check_typs

   492 ## calling Output.report

   493 #### Syntax_Phases.check_props

   494 ### Syntax_Phases.check_terms

   495 ### Syntax_Phases.check_typs

   496 ### Syntax_Phases.check_typs

   497 ### Syntax_Phases.check_typs

   498 ## calling Output.report

   499 #### Syntax_Phases.check_props

   500 ### Syntax_Phases.check_terms

   501 ### Syntax_Phases.check_typs

   502 ### Syntax_Phases.check_typs

   503 ### Syntax_Phases.check_typs

   504 ## calling Output.report

   505 ### Syntax_Phases.check_terms

   506 ### Syntax_Phases.check_typs

   507 ### Syntax_Phases.check_typs

   508 ### Syntax_Phases.check_typs

   509 ## calling Output.report

   510 ### Syntax_Phases.check_terms

   511 ### Syntax_Phases.check_typs

   512 ### Syntax_Phases.check_typs

   513 ### Syntax_Phases.check_typs

   514 ## calling Output.report

   515 ### Syntax_Phases.check_terms

   516 ### Syntax_Phases.check_typs

   517 ### Syntax_Phases.check_typs

   518 ### Syntax_Phases.check_typs

   519 ## calling Output.report

   520 ### Syntax_Phases.check_terms

   521 ### Syntax_Phases.check_typs

   522 ### Syntax_Phases.check_typs

   523 ### Syntax_Phases.check_typs

   524 ## calling Output.report

   525 ### Syntax_Phases.check_terms

   526 ### Syntax_Phases.check_typs

   527 ### Syntax_Phases.check_typs

   528 ### Syntax_Phases.check_typs

   529 ## calling Output.report

   530 ### Proof_Context.gen_fixes

   531 ### Proof_Context.gen_fixes

   532 \<close>

   534 section \<open>Notes: adapt spark_vc to Problem using Naproche as model\<close>

   536 subsection \<open>survey on steps of investigation\<close>

   537 text \<open>

   538   We stopped step 3.4 going down from Outer_Syntax.local_theory_to_proof into proof.

   539   Now we go the other way: Naproche checks the input via the Isabelle/server

   540   and outputs highlighting, semantic annotations and errors via PIDE ---

   541   and we investigate the output.

   543   Investigation of Naproche showed, that annotations are ONLY sent bY

   544   Output.report: string list -> unit, where string holds markup.

   545   For Output.report @ {print} is NOT available, so we trace all respective CALLS.

   546   However, NO @ {print} available in src/Pure is reached by "spark_vc procedure_g_c_d_4",

   547   so tracing is done by writeln (which breaks build between Main and Complex_Main

   548   by writing longer strings, see Pure/General/output.ML).

   550   Tracing is implemented in (1) Isabelle_Naproche and in (2) isabisac in parallel;

   551   (1) requires only Pure, thus is built quicker, but does NOT handle proofs within ML

   552   (2) requires HOL.SPARK, there is full proof handling, but this is complex.

   554   Tracing the calls of Output.report shows some properties of handling proofs,

   555   see text in SPARK/Examples/Gcd/Greatest_Common_Divisor.thy.

   556 \<close>

   558 end(* HERE SEVERAL ERRORS SHOW UP, CAUSED FROM ABOVE..

   559 "(1) outcomment before creating session Isac" ABOVE OTHERWISE YOU HAVE..

   560     Bad context for command "end"\<^here> -- using reset state

   561     Found the end of the theory, but the last SPARK environment is still open.

   562 "(2) outcomment before creating session Isac" ABOVE OTHERWISE YOU HAVE..

   563   ERROR:

   564     Bad context for command "end"\<^here> -- using reset state*)

author	Walther Neuper <walther.neuper@jku.at>
	Mon, 01 Mar 2021 12:46:40 +0100
changeset 60161	3c06f59b78d6
parent 60160	26d08b712434
child 60162	50f655f2db4f
permissions	-rw-r--r--