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

     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 end

author	Walther Neuper <walther.neuper@jku.at>
	Mon, 22 Mar 2021 16:20:56 +0100
changeset 60179	74cb63ac3538
parent 60178	c224a76494ba
child 60180	c2960a5b1204
permissions	-rw-r--r--