1.1 --- a/src/Tools/isac/BridgeJEdit/Calculation_OLD.thy Tue Aug 23 18:05:08 2022 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,222 +0,0 @@
1.4 -(* Title: src/Tools/isac/BridgeJEdit/Calculation_OLD.thy
1.5 - Author: Walther Neuper, JKU Linz
1.6 - (c) due to copyright terms
1.7 -
1.8 -Outer syntax for Isabelle/Isac's Calculation.
1.9 -First trials with SPARK..
1.10 -*)
1.11 -
1.12 -theory Calculation_OLD
1.13 -imports
1.14 -(**)"$ISABELLE_ISAC/Knowledge/Build_Thydata" (*remove after devel.of BridgeJEdit*)
1.15 -(**)"$ISABELLE_ISAC/MathEngine/MathEngine"
1.16 -(**)"SPARK_FDL" (*remove after devel.of BridgeJEdit*)
1.17 -keywords
1.18 - "ExampleSPARK" :: thy_load (*(isac_example)~(spark_vcg) ..would involve registering in Isabelle/Scala*)
1.19 - and(**)"Problem" :: thy_decl (*root-problem + recursively in Solution *)
1.20 - and "Specification" "Model" "References" :: diag (* structure only *)
1.21 - and "Solution" :: thy_decl (* structure only *)
1.22 - and "Where" "Given" "Find" "Relate" :: prf_decl (* await input of term *)
1.23 -(*and "Where" (* only output, preliminarily *)*)
1.24 - and "RTheory" :: thy_decl (* await input of string; "R" distingues "Problem".."RProblem" *)
1.25 - and "RProblem" "RMethod" :: thy_decl (* await input of string list *)
1.26 - and "Tactic" (* optional for each step 0..end of calculation *)
1.27 -begin
1.28 -(** )declare [[ML_print_depth = 99999]]( **)
1.29 -
1.30 -ML_file "parseC-OLD.sml"
1.31 -ML_file "preliminary-OLD.sml"
1.32 -
1.33 -
1.34 -section \<open>new code for Outer_Syntax ExampleSPARK, Problem, ...\<close>
1.35 -text \<open>
1.36 - code for ExampleSPARK, Problem shifted into structure Preliminary.
1.37 -\<close>
1.38 -
1.39 -subsubsection \<open>cp from Pure.thy\<close>
1.40 -ML \<open>
1.41 -\<close> ML \<open> (* for "from" ~~ "Given:" *)
1.42 -(* original *)
1.43 -val facts = Parse.and_list1 Parse.thms1;
1.44 -facts: (Facts.ref * Token.src list) list list parser;
1.45 -\<close> ML \<open>
1.46 -val facts =
1.47 - (writeln "####-## from parser";
1.48 - Parse.$$$ ":" |-- Parse.and_list1 Parse.thms1)(** ) --| Parse.$$$ "Where"( **);
1.49 -facts: (Facts.ref * Token.src list) list list parser;
1.50 -\<close> ML \<open>
1.51 -\<close> ML \<open>
1.52 -\<close>
1.53 -
1.54 -subsubsection \<open>tools to analyse parsing in Outer_Syntax >> \<close>
1.55 -ML \<open>
1.56 -\<close> text \<open> (*original basics.ML*)
1.57 -op |>> : ('a * 'b) * ('a -> 'c) -> 'c * 'b;
1.58 -fun (x, y) |>> f = (f x, y);
1.59 -\<close> text \<open> (*original scan.ML*)
1.60 -op >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c; (*---vvv*)
1.61 -fun (scan >> f) xs = scan xs |>> f;
1.62 -\<close> ML \<open>
1.63 -\<close> ML \<open> (*cp.from originals*)
1.64 -infix 3 @>>;
1.65 -fun (scan @>> f) xs = scan xs |>> f;
1.66 -op @>> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c; (*---^^^*)
1.67 -\<close> ML \<open> (*appl.to parser*)
1.68 -op @>> : (Token.src -> 'b * Token.src) * ('b -> 'd) -> Token.src -> 'd * Token.src; (*---^^^*)
1.69 -\<close> ML \<open>
1.70 -\<close> ML \<open> (*add analysis*)
1.71 -\<close> text \<open>
1.72 -datatype T = Pos of (int * int * int) * Properties.T;
1.73 -
1.74 -fun s_to_string (Pos ((line, offset, end_offset), _)) = ("Pos ((" ^
1.75 - string_of_int line ^ ", " ^ string_of_int offset ^ ", " ^ string_of_int end_offset ^ "), [_])")
1.76 -
1.77 -s_to_string: src -> string
1.78 -\<close> text \<open>
1.79 -datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot
1.80 -\<close> ML \<open>
1.81 -Token.pos_of; (*^^^^^^^^^^^^^^^*)
1.82 -Token.range_of; (*^^^^^^^^^^^^^*)
1.83 -Token.unparse; (*^^^^^^^^^^^^^*)
1.84 -\<close> ML \<open>
1.85 -fun string_of_tok (tok: Token.T) = "\n" ^ @{make_string} tok
1.86 -\<close> ML \<open>
1.87 -fun string_of_toks toks = fold (curry op ^) (map string_of_tok toks |> rev |> separate ", ") "";
1.88 -string_of_toks: Token.src -> string;
1.89 -\<close> ML \<open>
1.90 -fun (scan @>> f) xs = (@{print}{a = "_ >> ", toks = xs(*GIVES\<rightarrow>"?"*)}; scan xs) |>> f;
1.91 -fun (scan @>> f) xs = (writeln ("toks= " ^ @{make_string} xs); scan xs) |>> f;
1.92 -op @>> : (Token.src -> 'b * Token.src) * ('b -> 'd) -> Token.src -> 'd * Token.src; (*---^^^*)
1.93 -\<close> ML \<open>
1.94 -op @>> : (Token.T list -> 'a * 'b) * ('a -> 'c) -> Token.T list -> 'c * 'b
1.95 -\<close> ML \<open>
1.96 -\<close> ML \<open> (*Scan < Token in bootstrap, thus we take Token.s_to_string as argument of >> *)
1.97 -infix 3 @@>>;
1.98 -\<close> ML \<open>
1.99 -fun ((write, scan) @@>> f) xs = (write xs; scan xs) |>> f;
1.100 -op @@>> : (('a -> 'b) * ('a -> 'c * 'd)) * ('c -> 'e) -> 'a -> 'e * 'd
1.101 -\<close> ML \<open>
1.102 -\<close>
1.103 -
1.104 -subsubsection \<open>TODO\<close>
1.105 -ML \<open>
1.106 -\<close> ML \<open>
1.107 -\<close> ML \<open>
1.108 -\<close> ML \<open>
1.109 -\<close>
1.110 -
1.111 -section \<open>setup command_keyword + preliminary test\<close>
1.112 -ML \<open>
1.113 -\<close> ML \<open>
1.114 -val _ =
1.115 - Outer_Syntax.command \<^command_keyword>\<open>ExampleSPARK\<close> "start a Calculation from a Formalise-file"
1.116 - (Resources.provide_parse_file -- Parse.parname
1.117 - >> (Toplevel.theory o (*vvvvvvvvvvvvvvvvvvvv--- HACK makes test independent from session Isac*)
1.118 - (Preliminary_OLD.load_formalisation @{theory Biegelinie} ParseC_OLD.formalisation)) );
1.119 -\<close> ML \<open>
1.120 -val _ =
1.121 - Outer_Syntax.command \<^command_keyword>\<open>Problem\<close>
1.122 - "start a Specification, either from scratch or from preceding 'Example'"
1.123 - ((@{print}, ParseC_OLD.problem_headline)
1.124 - @@>> (Toplevel.theory o Preliminary_OLD.init_specify));
1.125 -\<close> ML \<open>
1.126 -Preliminary_OLD.init_specify: ParseC_OLD.problem_headline -> theory -> theory;
1.127 -(Toplevel.theory o Preliminary_OLD.init_specify)
1.128 - : ParseC_OLD.problem_headline -> Toplevel.transition -> Toplevel.transition;
1.129 -\<close> ML \<open>
1.130 -(**) Preliminary_OLD.init_specify: ParseC_OLD.problem_headline -> theory -> theory;(**)
1.131 -(* ^^^^^^ ^^^^^^*)
1.132 -(**)(Toplevel.theory o Preliminary_OLD.init_specify):
1.133 - ParseC_OLD.problem_headline -> Toplevel.transition -> Toplevel.transition;(**)
1.134 -(* ^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^^*)
1.135 -\<close> ML \<open>
1.136 -fun dummy (_(*":"*): string) thy =
1.137 - let
1.138 - val refs' = Refs_Data.get thy
1.139 - val o_model = OMod_Data.get thy
1.140 - val i_model = IMod_Data.get thy
1.141 - val _ =
1.142 - @{print} {a = "### dummy Specification", refs = refs', o_model = o_model, i_model = i_model}
1.143 - in thy end;
1.144 -\<close> ML \<open>
1.145 -val _ =
1.146 - Outer_Syntax.command \<^command_keyword>\<open>Specification\<close> "Specification dummy"
1.147 - ((@{print}, Parse.$$$ ":") @@>> (Toplevel.theory o dummy))
1.148 -\<close> ML \<open>
1.149 -fun dummy2 _ (thy: theory) = thy
1.150 -\<close> ML \<open> (*or*)
1.151 -fun dummy2 _ (ctxt: Proof.context) = ctxt
1.152 -\<close> ML \<open>
1.153 -val _ =
1.154 - Outer_Syntax.command \<^command_keyword>\<open>Model\<close> "Model dummy"
1.155 - ((@{print}, Parse.$$$ ":") @@>> (Toplevel.theory o dummy))
1.156 -\<close> ML \<open>
1.157 -val _ =
1.158 - Outer_Syntax.command \<^command_keyword>\<open>Given\<close> "input Given items to the Model of a Specification"
1.159 -(* (facts >> (Toplevel.proof o Proof.from_thmss_cmd));*)
1.160 - ((@{print}, facts) @@>> (Toplevel.proof o Proof.from_thmss_cmd));
1.161 -val _ =
1.162 - Outer_Syntax.command \<^command_keyword>\<open>Where\<close> "input Find items to the Model of a Specification"
1.163 - (facts @>> (Toplevel.proof o Proof.from_thmss_cmd));
1.164 -val _ =
1.165 - Outer_Syntax.command \<^command_keyword>\<open>Find\<close> "input Find items to the Model of a Specification"
1.166 - (facts @>> (Toplevel.proof o Proof.from_thmss_cmd));
1.167 -val _ =
1.168 - Outer_Syntax.command \<^command_keyword>\<open>Relate\<close> "input Relate items to the Model of a Specification"
1.169 - (facts @>> (Toplevel.proof o Proof.from_thmss_cmd));
1.170 -\<close> ML \<open>
1.171 -(Toplevel.proof o Proof.from_thmss_cmd)
1.172 -:
1.173 - (Facts.ref * Token.src list) list list -> Toplevel.transition -> Toplevel.transition
1.174 -(* ^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^^*)
1.175 -\<close> ML \<open>
1.176 -val _ =
1.177 - Outer_Syntax.command @{command_keyword References} "References dummy"
1.178 - (Parse.$$$ ":" >> (fn _ => Toplevel.keep (fn _ => ignore (writeln ""))));
1.179 -val _ =
1.180 - Outer_Syntax.command @{command_keyword RTheory} "RTheory dummy"
1.181 - (Parse.$$$ ":" -- Parse.string
1.182 - >> (fn _ => Toplevel.keep (fn _ => ignore (writeln ""))));
1.183 -val _ =
1.184 - Outer_Syntax.command @{command_keyword RProblem} "RProblem dummy"
1.185 - (Parse.$$$ ":" -- (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]")
1.186 - >> (fn _ => Toplevel.keep (fn _ => ignore (writeln ""))));
1.187 -val _ =
1.188 - Outer_Syntax.command @{command_keyword RMethod} "RMethod dummy"
1.189 - (Parse.$$$ ":" -- (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]")
1.190 - >> (fn _ => Toplevel.keep (fn _ => ignore (writeln ""))));
1.191 -val _ =
1.192 - Outer_Syntax.command @{command_keyword Solution} "Solution dummy"
1.193 - (Parse.$$$ ":" >> (fn _ => Toplevel.keep (fn _ => ignore (writeln ""))));
1.194 -\<close> ML \<open>
1.195 -\<close> ML \<open>
1.196 -\<close>
1.197 -
1.198 -subsection \<open>runs with test-Example\<close>
1.199 -(**)
1.200 -ExampleSPARK \<open>../Examples/exp_Statics_Biegel_Timischl_7-70.str\<close>
1.201 -(**)
1.202 -Problem ("Biegelinie", ["Biegelinien"])
1.203 -(*1 collapse* )
1.204 - Specification:
1.205 - (*2 collapse*)
1.206 - Model:
1.207 - Given: "Traegerlaenge " "Streckenlast " (*Bad context for command "Given"\<^here> -- using reset state*)
1.208 - Where: "q_0 ist_integrierbar_auf {| 0, L |}" "0 < L"
1.209 - Find: "Biegelinie "
1.210 - Relate: "Randbedingungen "
1.211 - References:
1.212 - (*3 collapse*)
1.213 - RTheory: "" (*Bad context for command "RTheory"\<^here> -- using reset state*)
1.214 - RProblem: ["", ""]
1.215 - RMethod: ["", ""]
1.216 - (*3 collapse*)
1.217 - (*2 collapse*)
1.218 - Solution:
1.219 -( * 1 collapse*)
1.220 -(*
1.221 - TODO: compare click on above Given: "Traegerlaenge ", "Streckenlast "
1.222 - with click on from \<open>0 < d\<close> in SPARK/../Greatest_Common_Divisorthy
1.223 -*)
1.224 -
1.225 -end
1.226 \ No newline at end of file