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

     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"

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

    13 keywords

    14   "Example" :: thy_load (*(isac_example)~(spark_vcg) ..would involve registering in Isabelle/Scala*)

    15   and(**)"Problem" :: thy_decl (*r oot-problem + recursively in Solution *)

    16   and "Specification" "Model" "References" :: diag (* structure only *)

    17   and "Solution" :: thy_decl (* structure only *)

    18   and "Where" "Given" "Find" "Relate" :: prf_decl (* await input of term *)

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

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

    21   and "RProblem" "RMethod" :: thy_decl (* await input of string list *)

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

    23 begin

    24 (** )declare [[ML_print_depth = 99999]]( **)

    25 ML_file parseC.sml

    26 ML_file preliminary.sml

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

    30 text \<open>

    31   code for Example, Problem shifted into structure Preliminary.

    32 \<close>

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

    35 ML \<open>

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

    37 (* original *)

    38 val facts = Parse.and_list1 Parse.thms1;

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

    40 \<close> ML \<open>

    41 val facts =

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

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

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

    45 \<close> ML \<open>

    46 \<close> ML \<open>

    47 \<close>

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

    50 ML \<open>

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

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

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

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

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

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

    57 \<close> ML \<open>

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

    59 infix 3 @>>;

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

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

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

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

    64 \<close> ML \<open>

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

    66 \<close> text \<open>

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

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

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

    72 s_to_string: src -> string

    73 \<close> text \<open>

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

    75 \<close> ML \<open>

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

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

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

    79 \<close> ML \<open>

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

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

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

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

    84 \<close> ML \<open>

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

    86 string_of_toks:    Token.src -> string;

    87 \<close> ML \<open>

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

    89 \<close> ML \<open>

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

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

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

    93 \<close> ML \<open>

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

    95 \<close> ML \<open>

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

    97 infix 3 @@>>;

    98 \<close> ML \<open>

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

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

   101 \<close> ML \<open>

   102 \<close>

   104 subsubsection \<open>TODO\<close>

   105 ML \<open>

   106 \<close> ML \<open>

   107 \<close> ML \<open>

   108 \<close> ML \<open>

   109 \<close>

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

   112 ML \<open>

   113 \<close> ML \<open>

   114 val _ =

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

   116     (Resources.provide_parse_file -- Parse.parname

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

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

   119 \<close> ML \<open>

   120 val _ =

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

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

   123     ((writeln o Token.s_to_string, ParseC.problem_headline)

   124        @@>> (Toplevel.theory o Preliminary.init_specify));

   125 \<close> ML \<open>

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

   127 (Toplevel.theory o Preliminary.init_specify)

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

   129 \<close> ML \<open>

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

   131 (*                                                                          ^^^^^^    ^^^^^^*)

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

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

   134 (*                               ^^^^^^^^^^^^^^^^^^^    ^^^^^^^^^^^^^^^^^^^*)

   135 \<close> ML \<open>

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

   137   let

   138     val refs' = Refs_Data.get thy

   139     val o_model = OMod_Data.get thy

   140     val i_model = IMod_Data.get thy

   141     val _ =

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

   143   in thy end;

   144 \<close> ML \<open>

   145 val _ =

   146   Outer_Syntax.command \<^command_keyword>\<open>Specification\<close> "Specification dummy"

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

   148 \<close> ML \<open>

   149 val _ =

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

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

   152 \<close> ML \<open>

   153 val _ =

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

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

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

   157 val _ =

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

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

   160 val _ =

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

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

   163 val _ =

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

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

   166 \<close> ML \<open>

   167 (Toplevel.proof o Proof.from_thmss_cmd)

   168 :

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

   170 (*                                          ^^^^^^^^^^^^^^^^^^^    ^^^^^^^^^^^^^^^^^^^*)

   171 \<close> ML \<open>

   172 val _ =

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

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

   175 val _ =

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

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

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

   179 val _ =

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

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

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

   183 val _ =

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

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

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

   187 val _ =

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

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

   190 \<close> ML \<open>

   191 \<close> ML \<open>

   192 \<close>

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

   195 (**)

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

   197 (**)

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

   199 (*1 collapse* )

   200   Specification:

   201   (*2 collapse*)

   202     Model:

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

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

   205       Find: "Biegelinie "

   206       Relate: "Randbedingungen "

   207     References:

   208       (*3 collapse*)

   209       RTheory: ""                           (*Bad context for command "RTheory"\<^here> -- using reset state*)

   210       RProblem: ["", ""]

   211       RMethod: ["", ""]

   212       (*3 collapse*)

   213   (*2 collapse*)

   214   Solution:

   215 ( * 1 collapse*)

   216 (*

   217   TODO: compare click on above Given: "Traegerlaenge ", "Streckenlast "

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

   219 *)

   221 subsection \<open>try combinations of keyword types\<close>

   222 subsubsection \<open>"Where" "Given" "Find" "Relate" :: prf_decl\<close>

   223 text \<open>

   224 keywords

   225   and "Specification" "Model" "References" :: XXX

   226   and "Where" "Given" "Find" "Relate" :: prf_decl

   227 CAUSE THESE ERRORS (EXHAUSTIVE ENUMERATION):

   229 XXX = diag, thy_stmt

   230   Bad context for command "Given" -- using reset state

   231   Bad context for command "RTheory" -- using reset state

   232 XXX = thy_decl, thy_defn, thy_goal, thy_goal_stmt

   233   Bad context for command "Given" -- using reset state

   234   Bad context for command "References" -- using reset state

   235 XXX = qed_script

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

   237   Bad context for command "Model" -- using reset state

   238   Bad context for command "Given" -- using reset state

   239 XXX = quasi_command: SCAN NOT DELIMITED PROPERLY..

   240   Outer syntax error: command expected, but keyword Specification was found

   241 XXX = thy_goal_stmt

   242 \<close>

   243 subsubsection \<open>"Where" "Given" "Find" "Relate" :: prf_decl\<close>

   244 text \<open>

   245 keywords

   246   and "Specification" "Model" "References" :: thy_stmt

   247   and "Where" "Given" "Find" "Relate" :: XXX

   248 CAUSE THESE ERRORS (EXHAUSTIVE ENUMERATION):

   250 XXX = prf_decl ((Where, Find, Relate ARE SCANNED PROPERLY))

   251   Bad context for command "Given" -- using reset state

   252   Bad context for command "References" -- using reset state

   253 XXX = thy_stmt ((Where, Find, Relate ARE SCANNED PROPERLY))

   254   Bad context for command "Given"

   255   Bad context for command "Where"

   256   Bad context for command "Find"

   257   Bad context for command "Relate"

   258 \<close>

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

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

   262 text \<open>

   263 -----------------v BEGIN ---------------vv END OF -----v

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

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

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

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

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

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

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

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

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

   273 \<close>

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

   275 text \<open>

   276 -----------------vv BEGIN ---------------vv END OF -----v

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

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

   279 \<close>

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

   281 text \<open>

   282 -----------------v BEGIN --------------v END OF -----v

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

   284 \<close>

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

   286 text \<open>COMPARE Greatest_Common_Divisor.thy

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

   289               line * offset * end_offset

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

   291 -----------------------------------------------------------------------------------

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

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

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

   295 ---------------------------------------------------------- ?WHY 2nd TURN..

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

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

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

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

   300 \<close>

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

   302 text \<open>

   303 toks=

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

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

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

   307 toks=

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

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

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

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

   312 \<close>

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

   314 text \<open>

   315 toks=

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

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

   318 toks=

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

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

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

   322 \<close>

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

   324 text \<open>

   325 toks=

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

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

   328 toks=

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

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

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

   332 \<close>

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

   334 text \<open>

   335 NO OUTPUT

   336 \<close>

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

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

   341 text \<open>

   342   Comparison of the two subsections below:

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

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

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

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

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

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

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

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

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

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

   354 # o_model = []                                                                 ..NO Example

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

   356 \<close>

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

   359 text \<open>

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

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

   362    ((((("Specification", ":"),

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

   364                  "Where"),

   365                 ":"),

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

   367               "Find"),

   368              ":"),

   369             "<markup>"),

   370            "Relate"),

   371           ":"),

   372          ["<markup>"]),

   373         (("References", ":"),

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

   375       "Solution"),

   376      ":"),

   377     [])),

   378   "")}

   379 {a = "init_specify", i_model =

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

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

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

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

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

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

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

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

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

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

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

   391 ### Proof_Context.gen_fixes

   392 ### Proof_Context.gen_fixes

   393 ### Proof_Context.gen_fixes

   394 ### Syntax_Phases.check_terms

   395 ### Syntax_Phases.check_typs

   396 ### Syntax_Phases.check_typs

   397 ### Syntax_Phases.check_typs

   398 ## calling Output.report

   399 #### Syntax_Phases.check_props

   400 ### Syntax_Phases.check_terms

   401 ### Syntax_Phases.check_typs

   402 ### Syntax_Phases.check_typs

   403 ## calling Output.report

   404 #### Syntax_Phases.check_props

   405 ### Syntax_Phases.check_terms

   406 ### Syntax_Phases.check_typs

   407 ### Syntax_Phases.check_typs

   408 ## calling Output.report

   409 #### Syntax_Phases.check_props

   410 ### Syntax_Phases.check_terms

   411 ### Syntax_Phases.check_typs

   412 ### Syntax_Phases.check_typs

   413 ## calling Output.report

   414 #### Syntax_Phases.check_props

   415 ### Syntax_Phases.check_terms

   416 ### Syntax_Phases.check_typs

   417 ### Syntax_Phases.check_typs

   418 ## calling Output.report

   419 #### Syntax_Phases.check_props

   420 ### Syntax_Phases.check_terms

   421 ### Syntax_Phases.check_typs

   422 ### Syntax_Phases.check_typs

   423 ## calling Output.report

   424 #### Syntax_Phases.check_props

   425 ### Syntax_Phases.check_terms

   426 ### Syntax_Phases.check_typs

   427 ### Syntax_Phases.check_typs

   428 ## calling Output.report

   429 #### Syntax_Phases.check_props

   430 ### Syntax_Phases.check_terms

   431 ### Syntax_Phases.check_typs

   432 ### Syntax_Phases.check_typs

   433 ## calling Output.report

   434 #### Syntax_Phases.check_props

   435 ### Syntax_Phases.check_terms

   436 ### Syntax_Phases.check_typs

   437 ### Syntax_Phases.check_typs

   438 ## calling Output.report

   439 #### Syntax_Phases.check_props

   440 ### Syntax_Phases.check_terms

   441 ### Syntax_Phases.check_typs

   442 ### Syntax_Phases.check_typs

   443 ## calling Output.report

   444 #### Syntax_Phases.check_props

   445 ### Syntax_Phases.check_terms

   446 ### Syntax_Phases.check_typs

   447 ### Syntax_Phases.check_typs

   448 ## calling Output.report

   449 #### Syntax_Phases.check_props

   450 ### Syntax_Phases.check_terms

   451 ### Syntax_Phases.check_typs

   452 ### Syntax_Phases.check_typs

   453 ## calling Output.report

   454 #### Syntax_Phases.check_props

   455 ### Syntax_Phases.check_terms

   456 ### Syntax_Phases.check_typs

   457 ### Syntax_Phases.check_typs

   458 ## calling Output.report

   459 #### Syntax_Phases.check_props

   460 ### Syntax_Phases.check_terms

   461 ### Syntax_Phases.check_typs

   462 ### Syntax_Phases.check_typs

   463 ## calling Output.report

   464 #### Syntax_Phases.check_props

   465 ### Syntax_Phases.check_terms

   466 ### Syntax_Phases.check_typs

   467 ### Syntax_Phases.check_typs

   468 ## calling Output.report

   469 #### Syntax_Phases.check_props

   470 ### Syntax_Phases.check_terms

   471 ### Syntax_Phases.check_typs

   472 ### Syntax_Phases.check_typs

   473 ## calling Output.report

   474 #### Syntax_Phases.check_props

   475 ### Syntax_Phases.check_terms

   476 ### Syntax_Phases.check_typs

   477 ### Syntax_Phases.check_typs

   478 ## calling Output.report

   479 #### Syntax_Phases.check_props

   480 ### Syntax_Phases.check_terms

   481 ### Syntax_Phases.check_typs

   482 ### Syntax_Phases.check_typs

   483 ## calling Output.report

   484 #### Syntax_Phases.check_props

   485 ### Syntax_Phases.check_terms

   486 ### Syntax_Phases.check_typs

   487 ### Syntax_Phases.check_typs

   488 ## calling Output.report

   489 #### Syntax_Phases.check_props

   490 ### Syntax_Phases.check_terms

   491 ### Syntax_Phases.check_typs

   492 ### Syntax_Phases.check_typs

   493 ## calling Output.report

   494 #### Syntax_Phases.check_props

   495 ### Syntax_Phases.check_terms

   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 ## calling Output.report

   504 #### Syntax_Phases.check_props

   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_props

   511 ### Syntax_Phases.check_terms

   512 ### Syntax_Phases.check_typs

   513 ### Syntax_Phases.check_typs

   514 ### Syntax_Phases.check_typs

   515 ## calling Output.report

   516 ### Syntax_Phases.check_terms

   517 ### Syntax_Phases.check_typs

   518 ### Syntax_Phases.check_typs

   519 ### Syntax_Phases.check_typs

   520 ## calling Output.report

   521 ### Syntax_Phases.check_terms

   522 ### Syntax_Phases.check_typs

   523 ### Syntax_Phases.check_typs

   524 ### Syntax_Phases.check_typs

   525 ## calling Output.report

   526 ### Syntax_Phases.check_terms

   527 ### Syntax_Phases.check_typs

   528 ### Syntax_Phases.check_typs

   529 ### Syntax_Phases.check_typs

   530 ## calling Output.report

   531 ### Syntax_Phases.check_terms

   532 ### Syntax_Phases.check_typs

   533 ### Syntax_Phases.check_typs

   534 ### Syntax_Phases.check_typs

   535 ## calling Output.report

   536 ### Syntax_Phases.check_terms

   537 ### Syntax_Phases.check_typs

   538 ### Syntax_Phases.check_typs

   539 ### Syntax_Phases.check_typs

   540 ## calling Output.report

   541 ### Proof_Context.gen_fixes

   542 ### Proof_Context.gen_fixes

   543 \<close>

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

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

   548 text \<open>

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

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

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

   552   and we investigate the output.

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

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

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

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

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

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

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

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

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

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

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

   567 \<close>

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

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

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

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

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

   574   ERROR:

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

author	Walther Neuper <walther.neuper@jku.at>
	Mon, 22 Mar 2021 08:31:30 +0100
changeset 60178	c224a76494ba
parent 60177	f7ad91ea1f2f
child 60179	74cb63ac3538
permissions	-rw-r--r--