(*

$ cd /usr/local/isabisac/src/Pure/isac/smltest/Pure/Isar

$ /usr/local/isabisac/bin/isabelle emacs Struct_Deriv.thy &

$ /usr/local/isabisac/bin/isabelle jedit Struct_Deriv.thy &

*)

header {* structured derivations (SD) according to R.J.Back *}

theory Struct_Deriv

imports Main

begin

text {* table of contents

1. fun parse for SDs by minimal copy from Isabelle code

1.1. keywords and outer syntax preparing parser setup

1.1.1. keywords according to src/Pure/Isar/keyword.ML

1.1.2. outer syntax according to src/Pure/Isar/outer_syntax.ML

1.1.3. parser setup according to src/Pure/Isar/isar_syn.ML

1.2. minimalized fun parse by Stefan Berghofer

2. provisional parser for SD

2.1. parsers for the elements of a calculation

2.1.1. named_rule

2.1.2. term_rule

2.1.3. rule

2.1.4. PBLheadline

2.1.5. CASheadline

2.1.6. headline

2.1.7. calcline

2.2. combine the parsers for elements to a whole SD-parser

2.2.1. provisional SD-parser setup

2.2.2. parser applied to example 1

2.2.3. parser applied to example 2

*}

section {* 1. fun parse for SDs by minimal copy from Isabelle code *}

subsection {* 1.1. keywords, outer syntax and parser setup *}

text {* this is a minimal copy from respective Isabelle sourcefiles,

  minimal with respect to the goal to parse simple SDs, see ex1, ex2 below.

  Actually, the code below has been selected from the function calls at the bottom,

  up to the initial definitions below.

  Some functions have been simplified; code is kept as (* original *)

  Problems arising with the simplifications will teach the reasons for the original source.

*}

subsubsection {* 1.1.1. keywords according to src/Pure/Isar/keyword.ML*}

ML {*

signature KEYWORDC = (*minimal C-copy from KEYWORD*)

sig

  type T

  val kind_of: T -> string

  val calc_begin: T

  val keyword: string -> unit

  val command: string -> T -> unit

  val tag_calc: T -> T

end;

structure KeywordC: KEYWORDC =

struct

datatype T = KeywordC of string * string list;

fun kind s = KeywordC (s, []);

fun kind_of (KeywordC (s, _)) = s;

val calc_begin = kind "calc-begin";

(*

fun change_commands f = CRITICAL (fn () => Unsynchronized.change global_commands f);

fun change_lexicons f = CRITICAL (fn () => Unsynchronized.change global_lexicons f);

fun report_message s =

  (if print_mode_active keyword_status_reportN then Output.status else writeln) s;*)

fun report_message s =

  (if true (*!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!*) then Output.status else writeln) s;

fun report_keyword name =

  report_message (Markup.markup (Markup.keyword_decl name)

    ("Outer syntax keyword: " ^ quote name));

fun report_command (name, kind) =

  report_message (Markup.markup (Markup.command_decl name (kind_of kind))

    ("Outer syntax command: " ^ quote name ^ " (" ^ kind_of kind ^ ")"));

fun keyword name =

 (apfst (Scan.extend_lexicon (Symbol.explode name));

  report_keyword name);

(* see CRITICAL above

fun command name kind =

 (change_lexicons (apsnd (Scan.extend_lexicon (Symbol.explode name)));

  change_commands (Symtab.update (name, kind));

  report_command (name, kind));*)

fun command name kind =

 (apsnd (Scan.extend_lexicon (Symbol.explode name));

  Symtab.update (name, kind);

  report_command (name, kind));

fun update_tags t ts = t :: remove (op = : string * string -> bool) t ts;

fun tag t (KeywordC (s, ts)) = KeywordC (s, update_tags t ts);

val tag_calc = tag "calculation"; (* <----------------------------------------*)

end; *}

subsubsection {* 1.1.2. outer syntax according to src/Pure/Isar/outer_syntax.ML*}

ML {* 

signature OUTER_SYNTAXC = 

sig

  val command: string -> string -> KeywordC.T ->

    (Toplevel.transition -> Toplevel.transition) parser -> unit

  val scan: Position.T -> string -> Token.T list

end;

structure Outer_SyntaxC: OUTER_SYNTAXC =

struct

datatype command = CommandC of

 {comment: string,

  markup: Thy_Output.markup option,

  int_only: bool,

  parse: (Toplevel.transition -> Toplevel.transition) parser};

fun make_command comment markup int_only parse =

  CommandC {comment = comment, markup = markup, int_only = int_only, parse = parse};

val global_commands = Unsynchronized.ref (Symtab.empty: command Symtab.table);

val global_markups = Unsynchronized.ref ([]: (string * Thy_Output.markup) list);

fun change_commands f = CRITICAL (fn () =>

 (Unsynchronized.change global_commands f;

  global_markups :=

    Symtab.fold (fn (name, CommandC {markup = SOME m, ...}) => cons (name, m) | _ => I)

      (! global_commands) []));

fun get_commands () = ! global_commands;

fun add_command name kind cmd = CRITICAL (fn () =>

 (KeywordC.command name kind;

  if not (Symtab.defined (get_commands ()) name) then ()

  else warning ("Redefining outer syntax command " ^ quote name);

  change_commands (Symtab.update (name, cmd))));

fun command name comment kind parse =

  add_command name kind (make_command comment NONE false parse);

fun scan pos str =

  Source.of_string str

  |> Symbol.source {do_recover = false}

  |> Token.source {do_recover = SOME false} Keyword.get_lexicons pos

  |> Source.exhaust;

end; *}

subsubsection {* 1.1.3. parser setup according to src/Pure/Isar/isar_syn.ML *}

ML {* 

structure Isac_Syn: sig end =

struct

val _ = List.app (*contrib/polyml-5.3.0/src/basis/List.sml*) KeywordC.keyword

 ["(", ")", "[", "]", ",",

  "=>", "<=", 

  "==",              (* simplification without "=" in term      *)

  "equiv",           (* equations, etc                          *)

  "bullet",          (* indicates a subproblem TODO rewrite_set *)

  "CAS", "Problem",  (* "headlines" of subproblems              *)

  "dots",            (* end of subproblem TODO of rewrite_set   *)

(*"bigtriangledown",    indicates a rule *)

  "THM", "MET",      (* a ruleconcerning a theorem, a method    *)

  "Calculate", "Rewrite", "Rewrite_Set", "Rewrite_Inst", "Rewrite_Set_Inst",

                     (* rules; TODO?!? Take REFERENCE           *)

  "top",             (* term not following from previous term   *)

  "Box"              (* qed                                     *)

 ];             

val _ =

  Outer_SyntaxC.command "calculation" "begin calc" (KeywordC.tag_calc KeywordC.calc_begin)

    (Thy_Header.args >> (Toplevel.print oo Isar_Cmd.init_theory)); (*TODO*)

end; *}

subsection {* 1.2. minimalized fun parse by Stefan Berghofer *}

text {* see ~/devel/IsaDevWS/IsaDevWS-10/T05_Methods.thy by Stefan Berghofer *}

ML {*

fun filtered_input str =

  filter Token.is_proper (Outer_SyntaxC.scan Position.none str);

(*################################ fun parse ###############################################*)

fun parse p str = Scan.finite Token.stopper p (filtered_input str);

(*################################ fun parse ###############################################*)

*}

section {* 2. provisional parser for SD *}

subsection {* 2.1. parsers for the elements of a calculation *}

subsubsection {* 2.1.1. named_rule *}

ML {*

"---1----------------------------------------";

val named_rule' = (Args.$$$ "Calculate" || Args.$$$ "Rewrite" || Args.$$$ "Rewrite_Set"

                || Args.$$$ "Rewrite_Inst" || Args.$$$ "Rewrite_Set_Inst")

               -- Args.name;

parse named_rule' "Calculate times";

(*(("Calculate", "times"), []) : (string * string) * Token.T list*)

fun exec2 (nam, rul) = 

  "*** notebook->ML: " ^ nam ^ " " ^ rul

  |> (fn x => (x, x))

  |>> writeln

  |> #2;

(*fn : string * string -> string*)

val named_rule = named_rule' >> exec2;

"---2----------------------------------------";

parse named_rule "Calculate times";

(*("*** notebook->ML: Calculate times", []) : string * Token.T list*)

"---3--- output on top ----------------------";

(*** notebook->ML: Calculate times*)

*}

subsubsection {* 2.1.2. term_rule *}

ML {*

"---1----------------------------------------";

val term_rule' = Args.$$$ "THM" -- Parse.term;

parse term_rule' "THM \"(a+x=b)=(x=-a*b)\"  ";

(*(("THM", "\^E\^Ftoken\^Ea+x=b = x=-a*b\^E\^F\^E"), []) : (string * string) * Token.T list*)

val term_rule = term_rule' >> exec2;

"---2----------------------------------------";

parse term_rule "THM \"(a+x=b)=(x=-a*b)\"  ";

(*("*** notebook->ML: THM \^E\^Ftoken\^E(a+x=b)=(x=-a*b)\^E\^F\^E", []) : string * Token.T list*)

"---3--- output on top ----------------------";

(*** notebook->ML: THM (a+x=b)=(x=-a*b)*)

*}

subsubsection {* 2.1.3. rule *}

ML {*

val rule = named_rule || term_rule;

*}

subsubsection {* 2.1.4. PBLheadline *}

ML {*

"---1----------------------------------------";

val PBLheadline' = Args.$$$ "Problem" -- Args.$$$ "(" -- Args.name -- Args.$$$ ","

  -- (Parse.$$$ "[" |-- Parse.list Parse.name --| Parse.$$$ "]") 

  -- Args.$$$ ")";

parse PBLheadline' "Problem (Biegelinie.thy, [Biegelinien])";

(*val it = (((((("Problem", "("), "Biegelinie.thy"), ","), ["Biegelinien"]), ")"), [])

   : (((((string * string) * string) * string) * bstring list) * string) * Token.T list*)

fun execN ((((("Problem", "("), thy             ), ","), pbl            ), ")") =

  "*** notebook->ML: Problem (" ^ thy ^ ", " ^ ((fn ss => "[" ^ commas ss ^ "]") pbl) ^ ")"

  |> (fn x => (x, x))

  |>> writeln

  |> #2;

(*fn : ((((string * string) * string) * string) * string list) * string -> string*)

"---2----------------------------------------";

execN     ((((("Problem", "("), "Biegelinie.thy"), ","), ["Biegelinien"]), ")");

(*"*** notebook->ML: Problem (Biegelinie.thy, [Biegelinien])" : string

 +see top*)

val PBLheadline = PBLheadline' >> execN;

parse PBLheadline "Problem (Biegelinie.thy, [Biegelinien])";

(*("*** notebook->ML: Problem (Biegelinie.thy, [Biegelinien])", []) : string * Token.T list

 +see top*)

parse PBLheadline "Problem (Biegelinie.thy, [setzeRandbedingungen, Biegelinien])";

(*("*** notebook->ML: Problem (Biegelinie.thy, [setzeRandbedingungen, Biegelinien])", [])

 +see top*)

"---3--- output on top ----------------------";

(** notebook->ML: Problem (Biegelinie.thy, [Biegelinien])

*** notebook->ML: Problem (Biegelinie.thy, [Biegelinien])

*** notebook->ML: Problem (Biegelinie.thy, [setzeRandbedingungen, Biegelinien])*)

*}

subsubsection {* 2.1.5. CASheadline *}

ML {*

"---1----------------------------------------";

val CASheadline' = Args.$$$ "CAS" -- Parse.term;

parse CASheadline' "CAS \"solve(x+1=2,x)\"";

(*(("CAS", "\^E\^Ftoken\^Esolve(x+1=2,x)\^E\^F\^E"), []) : (string * string) * Token.T list*)

fun exec2b ("CAS", trm) = 

  "*** notebook->ML: \"" ^ trm ^ "\""

  |> (fn x => (x, x))

  |>> writeln

  |> #2;

(*fn : string * string -> string*)

val CASheadline = CASheadline' >> exec2b;

"---2----------------------------------------";

parse CASheadline "CAS \"solve(x+1=2,x)\"";

(*("*** notebook->ML: \^E\^Ftoken\^Esolve(x+1=2,x)\^E\^F\^E", []) : string * Token.T list*)

"---3--- output on top ----------------------";

(*** notebook->ML: solve(x+1=2,x)*)

*}

subsubsection {* 2.1.6. headline *}

ML {*

val headline = (PBLheadline || CASheadline) -- Scan.option rule;

parse headline "Problem (Biegelinie.thy, [setzeRandbedingungen, Biegelinien])";

parse headline "CAS \"solve(x+1=2,x)\"";

parse headline "CAS \"solve(x+1=2,x)\" Calculate times";

parse headline "CAS \"solve(x+1=2,x)\" THM \"(a+x=b)=(x=-a*b)\" ";

*}

subsubsection {* 2.1.7. calcline *}

ML {*

"---1----------------------------------------";

val calcline' = Parse.term ;

parse calcline' "  \"-1 + x = 0\"  ";

(*("\^E\^Ftoken\^E-1 + x = 0\^E\^F\^E", []) : string * Token.T list*)

fun exec1 trm = 

  "*** notebook->ML: \"" ^ trm ^ "\""

  |> (fn x => (x, x))

  |>> writeln

  |> #2;

(*fn : string -> string*)

val calcline = calcline' >> exec1;

"---2----------------------------------------";

parse calcline "  \"-1 + x = 0\"  ";

(*("*** notebook->ML: \"\^E\^Ftoken\^E-1 + x = 0\^E\^F\^E\"", []) : string * Token.T list*)

"---3--- output on top ----------------------";

(*** notebook->ML: "-1 + x = 0"*)

*}

subsection {* 2.2. combine the parsers for elements to a whole SD-parser *}

subsubsection {* 2.2.1. provisional SD-parser setup *}

text {* Prefixes, which are complete enough to trigger a semantic action,

        have already be handled by exec*.

        Thus combining such prefixes allows to drop these prefixes. *}

ML {*

fun drop_prefixes _ = "DROPPED PREFIXES";

*}

ML {*

(*val line = headline || calcline; ...this would prevent separation of rewrite_set *)

val level_up = Args.$$$ "dots" -- calcline;

*}

ML {* (* see IsaDevWS-10/T06_System.thy "recursive parsers" *)

fun body _ source = 

   (  Scan.repeat(    Args.$$$ "top" -- calcline -- 

                        (Scan.repeat (Args.$$$ "equiv" -- calcline)) >> drop_prefixes

(* GOON            || (Scan.repeat (Args.$$$ "equiv" -- calcline))   >> drop_prefixes  *)

                   || Args.$$$ "bullet" -- headline -- body ""       >> drop_prefixes

                 ) 

      -- level_up

   ) source;

writeln "---0-------";

parse (body "") "top \"1+2\" equiv \"3+4\" dots \"5+6\" ";

writeln "---1-------";

parse (body "") "bullet CAS \"solve(x+1=2,x)\" \

                \top \"1+2\" equiv \"3+4\" dots \"5+6\" dots \"999\" ";

writeln "---2-------";

parse (body "") "    bullet CAS \"solve (-1 + x = 0, x)\"          \n\

                \       top \"-1 + x = 0\"                         \n\

                \       equiv \"[x = 1]\"                          \n\

                \    dots \"[x = 1]\"                              \n\

                \ dots \"[x = 1]\"                                 ";

*}

ML {*

(*################################ the parser ##############################################*)

val SD = Args.$$$ "calculation" -- Args.$$$ "bullet" -- headline 

         -- (body "") 

         -- (Scan.option (Args.$$$ "Box"));

(*################################ the parser ##############################################*)

writeln "---0----------------------------------------";

parse SD "calculation                      \n\

         \ bullet CAS \"solve(x+1=2,x)\"   \n\

         \ dots \"[x = 1]\"                ";

writeln "---1-----------------------------------------";

parse SD "calculation                              \n\

         \ bullet CAS \"solve(x+1=2,x)\"           \n\

         \    top \"x + 1 = 2\"                    \n\

         \    equiv \"-1 + x = 0\"                 \n\

         \    bullet CAS \"solve (-1 + x = 0, x)\" \n\

         \       top \"-1 + x = 0\"                \n\

         \       equiv \"[x = 1]\"                 \n\

         \    dots \"[x = 1]\"                     \n\

         \ dots \"[x = 1]\"                        \n\

         \ Box                                     ";

writeln "---2-----------------------------------------";

(* TODO ?!?

parse SD "calculation                              \n\

         \ bullet CAS \"solve(x+1=2,x)\"           \n\

         \                Calculate times          \n\

         \    top \"x + 1 = 2\"                    \n\

         \    equiv \"-1 + x = 0\"                 \n\

         \                THM \"(a+x=b)=(x=-a*b)\" \n\

         \ dots \"[x = 1]\"                        \n\

         \ Box                                     ";

*)

writeln "---3-----------------------------------------";

(* GOON: make equiv a viable prefix at this position !

parse SD "calculation                              \n\

         \ bullet CAS \"solve(x+1=2,x)\"           \n\

         \    bullet CAS \"solve (-1 + x = 0, x)\" \n\

         \    dots \"[x = 1]\"                     \n\

         \    equiv \"-1 + x = 0\"                 \n\

         \ dots \"[x = 1]\"                        \n\

         \ Box                                     ";

*)

writeln "---4-----------------------------------------";

*}

subsubsection {* 2.2.2. parser applied to example 1 *}

ML {*

val ex1 = "calculation                      \n\

  \ bullet CAS \"solve(x+1=2,x)\"           \n\

  \    top \"x + 1 = 2\"                    \n\

  \    equiv \"x + 1 - 2 = 0\"              \n\

  \    equiv \"-1 + x = 0\"                 \n\

  \    bullet CAS \"solve (-1 + x = 0, x)\" \n\

  \       top \"-1 + x = 0\"                \n\

  \       equiv \"x = -1 * -1\"             \n\

  \       equiv \"x = 1\"                   \n\

  \       equiv \"[x = 1]\"                 \n\

  \    dots \"[x = 1]\"                     \n\

  \ dots \"[x = 1]\"                        \n\

  \ Box ";

parse SD ex1;

*}

subsubsection {* 2.2.3. parser applied to example 2 *}

ML {*

val ex2 = "calculation                                                                                                             \n\

  \ bullet Problem (Biegelinie.thy, [Biegelinien])                                                                                 \n\

  \    bullet Problem (Biegelinie.thy, [vonBelastungZu, Biegelinien])                                                              \n\

  \    dots \"[Q x = c + -1 * q_0 * x, M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^ 2,                                                 \n\

  \          y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^ 2 + -1 * q_0 / 6 * x ^ 3),                                        \n\

  \          y x = c_4 + c_3 * x + 1 / (-1 * EI) * (c_2 / 2 * x ^ 2 + c / 6 * x ^ 3 + -1 * q_0 / 24 * x ^ 4)]\"                    \n\

  \    bullet Problem (Biegelinie.thy, [setzeRandbedingungen, Biegelinien])                                                        \n\

  \    dots \"[L * q_0 = c, 0 = (2 * c_2 + 2 * L * c + -1 * L ^ 2 * q_0) / 2, 0 = c_4, 0 = c_3]\"                                  \n\

  \    bullet CAS \"solveSystem [0 = c_3] [c_4]\"                                                                                  \n\

  \    dots \"[c = L * q_0, c_2 = -1 * L ^ 2 * q_0 / 2, c_3 = 0, c_4 = 0]\"                                                        \n\

  \    top \"y x = c_4 + c_3 * x + 1 / (-1 * EI) * (c_2 / 2 * x ^ 2 + c / 6 * x ^ 3 + -1 * q_0 / 24 * x ^ 4)\"                     \n\

  \    equiv \"y x = 0 + 0 * x + 1 / (-1 * EI) * (-1 * L ^ 2 * q_0 / 2 / 2 * x ^ 2 + L * q_0 / 6 * x ^ 3 + -1 * q_0 / 24 * x ^ 4)\"\n\

  \    equiv \"y x = -6 * q_0 * L ^ 2 / (-24 * EI) * x ^ 2 + 4 * L * q_0 / (-24 * EI) * x ^ 3 + -1 * q_0 / (-24 * EI) * x ^ 4\"    \n\

  \ dots \"y x = -6 * q_0 * L ^ 2 / (-24 * EI) * x ^ 2 + 4 * L * q_0 / (-24 * EI) * x ^ 3 + -1 * q_0 / (-24 * EI) * x ^ 4\"        \n\

  \ Box";

parse SD ex2;

*}

end