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

    Author:     Walther Neuper, JKU Linz

    (c) due to copyright terms

Outer syntax for Isabelle/Isac's Calculation.

*)

theory Calculation

imports

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

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

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

keywords

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

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

                               "spark_vc" :: thy_goal *)

  and "Specification" "Model" "References" :: diag

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

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

   (* ^^^^^^ :: before_command quasi_command thy_decl thy_defn thy_stmt diag prf_decl *)

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

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

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

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

begin

declare [[ML_print_depth = 99999]]

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

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

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

text \<open>

  code for Example, Problem shifted into structure Preliminary.

\<close>

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

ML \<open>

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

(* original *)

val facts = Parse.and_list1 Parse.thms1;

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

\<close> ML \<open>

val facts =

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

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

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

\<close> ML \<open>

\<close> ML \<open>

\<close>

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

ML \<open>

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

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

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

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

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

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

\<close> ML \<open>

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

infix 3 @>>;

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

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

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

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

\<close> ML \<open>

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

\<close> text \<open>

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

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

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

s_to_string: src -> string

\<close> text \<open>

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

\<close> ML \<open>

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

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

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

\<close> ML \<open>

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

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

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

  Token.unparse tok ^ ", _)")

\<close> ML \<open>

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

string_of_toks:    Token.src -> string;

\<close> ML \<open>

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

\<close> ML \<open>

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

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

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

\<close> ML \<open>

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

\<close> ML \<open>

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

infix 3 @@>>;

\<close> ML \<open>

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

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

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close>

subsubsection \<open>TODO\<close>

ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close> ML \<open>

\<close>

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

ML \<open>                                            

\<close> ML \<open>

val _ =                                                  

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

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

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

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

\<close> ML \<open>

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

:

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

    Toplevel.transition -> Toplevel.transition

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

\<close> ML \<open>

val _ =

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

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

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

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

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

\<close> ML \<open>

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

(Toplevel.theory o Preliminary.init_specify)

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

\<close> ML \<open>

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

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

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

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

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

\<close> ML \<open>

\<close> ML \<open>

OMod_Data.get

\<close> ML \<open>

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

  let

    val refs' = Refs_Data.get thy

    val o_model = OMod_Data.get thy

    val i_model = IMod_Data.get thy

    val _ =

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

  in

    thy

  end;

\<close> ML \<open>

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

\<close> ML \<open>

val _ =

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

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

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

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

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

\<close> ML \<open>

val _ =

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

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

\<close> ML \<open>

val _ =

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

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

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

val _ =

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

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

val _ =

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

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

val _ =

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

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

\<close> ML \<open>

(Toplevel.proof o Proof.from_thmss_cmd)

:

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

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

\<close> ML \<open>

val _ =

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

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

val _ =

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

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

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

val _ =

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

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

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

val _ =

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

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

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

val _ =

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

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

\<close> ML \<open>

\<close> ML \<open>

\<close> text \<open> NEWS 2014

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

occasionally useful for experimentation and diagnostic purposes.

\<close> ML \<open>

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

\<close> ML \<open>

\<close>

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

(**)

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

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

(*1 collapse* )

  Specification:

  (*2 collapse*)

    Model:

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

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

      Find: "Biegelinie "

      Relate: "Randbedingungen "

    References:

      (*3 collapse*)

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

      RProblem: ["", ""]

      RMethod: ["", ""]

      (*3 collapse*)

  (*2 collapse*)

  Solution:

( * 1 collapse*)

(*

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

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

*)

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

subsubsection \<open>on Problem\<close>

text \<open>

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

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

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

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

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

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

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

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

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

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

\<close>

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

text \<open>

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

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

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

\<close>

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

text \<open>

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

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

\<close>

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

text \<open>COMPARE Greatest_Common_Divisor.thy

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

              line * offset * end_offset

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

-----------------------------------------------------------------------------------

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

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

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

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

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

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

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

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

\<close>

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

text \<open>

toks= 

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

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

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

toks= 

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

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

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

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

\<close>

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

text \<open>

toks= 

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

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

toks= 

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

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

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

\<close>

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

text \<open>

toks= 

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

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

toks= 

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

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

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

\<close>

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

text \<open>

NO OUTPUT

\<close>

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

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

text \<open>

  Comparison of the two subsections below:

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

  ((WHILE click ON Example SHOWS NO ERROR))

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

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

# o_model = COMPLETE WITH 7 ELEMENTS                                           ..FROM Example

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

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

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

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

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

# o_model = []                                                                 ..NO Example

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

\<close>

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

text \<open>

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

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

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

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

                 "Where"),

                ":"),

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

              "Find"),

             ":"),

            "<markup>"),

           "Relate"),

          ":"),

         ["<markup>"]),

        (("References", ":"),

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

      "Solution"),

     ":"),

    [])),

  "")}

{a = "init_specify", i_model =

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

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

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

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

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

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

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

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

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

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

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

### Proof_Context.gen_fixes 

### Proof_Context.gen_fixes 

### Proof_Context.gen_fixes 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

#### Syntax_Phases.check_props 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

### Syntax_Phases.check_terms 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

### Syntax_Phases.check_typs 

## calling Output.report 

### Proof_Context.gen_fixes 

### Proof_Context.gen_fixes

\<close>

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

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

text \<open>

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

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

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

  and we investigate the output.

  Investigation of Naproche showed, that annotations are ONLY sent bY

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

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

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

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

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

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

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

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

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

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

\<close>

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

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

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

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

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

  ERROR:                         

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