# HG changeset patch # User wneuper # Date 1661337427 -7200 # Node ID 5038589d3033b5c49d632462beb0ec550526c9cd # Parent d5c670beaba48be3299cf0b143bfeff1cdcddaae eliminate SPARK; as an example replaced by Outer_Syntax.command..problem diff -r d5c670beaba4 -r 5038589d3033 TODO.md --- a/TODO.md Tue Aug 23 18:05:08 2022 +0200 +++ b/TODO.md Wed Aug 24 12:37:07 2022 +0200 @@ -60,8 +60,6 @@ ***** priority of WN items is top down, most urgent/simple on top -* WN: eliminate SPARK; as an example replaced by Outer_Syntax.command..problem - * WN: polish naming in BaseDefinitions/eval-def.sml * WN: Step_Specify.initialisePIDE: remove hdl in return-value, replace Step_Specify.nxt_specify_init_calc ? which uses initialisePIDE !? diff -r d5c670beaba4 -r 5038589d3033 src/Tools/isac/BridgeJEdit/BridgeJEdit.thy --- a/src/Tools/isac/BridgeJEdit/BridgeJEdit.thy Tue Aug 23 18:05:08 2022 +0200 +++ b/src/Tools/isac/BridgeJEdit/BridgeJEdit.thy Wed Aug 24 12:37:07 2022 +0200 @@ -6,7 +6,7 @@ *) theory BridgeJEdit - imports Calculation_OLD VSCode_Example + imports VSCode_Example begin ML \ diff -r d5c670beaba4 -r 5038589d3033 src/Tools/isac/BridgeJEdit/Calculation.thy --- a/src/Tools/isac/BridgeJEdit/Calculation.thy Tue Aug 23 18:05:08 2022 +0200 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy Wed Aug 24 12:37:07 2022 +0200 @@ -9,7 +9,6 @@ imports (**)"$ISABELLE_ISAC/Knowledge/Build_Thydata" (*remove after devel.of BridgeJEdit*) (**)"$ISABELLE_ISAC/MathEngine/MathEngine" - (** )"SPARK_FDL" ( * remove after devel.of BridgeJEdit*) keywords "Example" :: thy_decl and "Specification" "Model" "References" "Solution" diff -r d5c670beaba4 -r 5038589d3033 src/Tools/isac/BridgeJEdit/Calculation_OLD.thy --- a/src/Tools/isac/BridgeJEdit/Calculation_OLD.thy Tue Aug 23 18:05:08 2022 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,222 +0,0 @@ -(* Title: src/Tools/isac/BridgeJEdit/Calculation_OLD.thy - Author: Walther Neuper, JKU Linz - (c) due to copyright terms - -Outer syntax for Isabelle/Isac's Calculation. -First trials with SPARK.. -*) - -theory Calculation_OLD -imports -(**)"$ISABELLE_ISAC/Knowledge/Build_Thydata" (*remove after devel.of BridgeJEdit*) -(**)"$ISABELLE_ISAC/MathEngine/MathEngine" -(**)"SPARK_FDL" (*remove after devel.of BridgeJEdit*) -keywords - "ExampleSPARK" :: thy_load (*(isac_example)~(spark_vcg) ..would involve registering in Isabelle/Scala*) - and(**)"Problem" :: thy_decl (*root-problem + recursively in Solution *) - and "Specification" "Model" "References" :: diag (* structure only *) - and "Solution" :: thy_decl (* structure only *) - and "Where" "Given" "Find" "Relate" :: prf_decl (* await input of term *) -(*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-OLD.sml" -ML_file "preliminary-OLD.sml" - - -section \new code for Outer_Syntax ExampleSPARK, Problem, ...\ -text \ - code for ExampleSPARK, Problem shifted into structure Preliminary. -\ - -subsubsection \cp from Pure.thy\ -ML \ -\ ML \ (* for "from" ~~ "Given:" *) -(* original *) -val facts = Parse.and_list1 Parse.thms1; -facts: (Facts.ref * Token.src list) list list parser; -\ ML \ -val facts = - (writeln "####-## from parser"; - Parse.$$$ ":" |-- Parse.and_list1 Parse.thms1)(** ) --| Parse.$$$ "Where"( **); -facts: (Facts.ref * Token.src list) list list parser; -\ ML \ -\ ML \ -\ - -subsubsection \tools to analyse parsing in Outer_Syntax >> \ -ML \ -\ text \ (*original basics.ML*) -op |>> : ('a * 'b) * ('a -> 'c) -> 'c * 'b; -fun (x, y) |>> f = (f x, y); -\ text \ (*original scan.ML*) -op >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c; (*---vvv*) -fun (scan >> f) xs = scan xs |>> f; -\ ML \ -\ ML \ (*cp.from originals*) -infix 3 @>>; -fun (scan @>> f) xs = scan xs |>> f; -op @>> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c; (*---^^^*) -\ ML \ (*appl.to parser*) -op @>> : (Token.src -> 'b * Token.src) * ('b -> 'd) -> Token.src -> 'd * Token.src; (*---^^^*) -\ ML \ -\ ML \ (*add analysis*) -\ text \ -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 -\ text \ -datatype T = Token of (Symbol_Pos.text * Position.range) * (kind * string) * slot -\ ML \ -Token.pos_of; (*^^^^^^^^^^^^^^^*) -Token.range_of; (*^^^^^^^^^^^^^*) -Token.unparse; (*^^^^^^^^^^^^^*) -\ ML \ -fun string_of_tok (tok: Token.T) = "\n" ^ @{make_string} tok -\ ML \ -fun string_of_toks toks = fold (curry op ^) (map string_of_tok toks |> rev |> separate ", ") ""; -string_of_toks: Token.src -> string; -\ ML \ -fun (scan @>> f) xs = (@{print}{a = "_ >> ", toks = xs(*GIVES\"?"*)}; scan xs) |>> f; -fun (scan @>> f) xs = (writeln ("toks= " ^ @{make_string} xs); scan xs) |>> f; -op @>> : (Token.src -> 'b * Token.src) * ('b -> 'd) -> Token.src -> 'd * Token.src; (*---^^^*) -\ ML \ -op @>> : (Token.T list -> 'a * 'b) * ('a -> 'c) -> Token.T list -> 'c * 'b -\ ML \ -\ ML \ (*Scan < Token in bootstrap, thus we take Token.s_to_string as argument of >> *) -infix 3 @@>>; -\ ML \ -fun ((write, scan) @@>> f) xs = (write xs; scan xs) |>> f; -op @@>> : (('a -> 'b) * ('a -> 'c * 'd)) * ('c -> 'e) -> 'a -> 'e * 'd -\ ML \ -\ - -subsubsection \TODO\ -ML \ -\ ML \ -\ ML \ -\ ML \ -\ - -section \setup command_keyword + preliminary test\ -ML \ -\ ML \ -val _ = - Outer_Syntax.command \<^command_keyword>\ExampleSPARK\ "start a Calculation from a Formalise-file" - (Resources.provide_parse_file -- Parse.parname - >> (Toplevel.theory o (*vvvvvvvvvvvvvvvvvvvv--- HACK makes test independent from session Isac*) - (Preliminary_OLD.load_formalisation @{theory Biegelinie} ParseC_OLD.formalisation)) ); -\ ML \ -val _ = - Outer_Syntax.command \<^command_keyword>\Problem\ - "start a Specification, either from scratch or from preceding 'Example'" - ((@{print}, ParseC_OLD.problem_headline) - @@>> (Toplevel.theory o Preliminary_OLD.init_specify)); -\ ML \ -Preliminary_OLD.init_specify: ParseC_OLD.problem_headline -> theory -> theory; -(Toplevel.theory o Preliminary_OLD.init_specify) - : ParseC_OLD.problem_headline -> Toplevel.transition -> Toplevel.transition; -\ ML \ -(**) Preliminary_OLD.init_specify: ParseC_OLD.problem_headline -> theory -> theory;(**) -(* ^^^^^^ ^^^^^^*) -(**)(Toplevel.theory o Preliminary_OLD.init_specify): - ParseC_OLD.problem_headline -> Toplevel.transition -> Toplevel.transition;(**) -(* ^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^^*) -\ ML \ -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; -\ ML \ -val _ = - Outer_Syntax.command \<^command_keyword>\Specification\ "Specification dummy" - ((@{print}, Parse.$$$ ":") @@>> (Toplevel.theory o dummy)) -\ ML \ -fun dummy2 _ (thy: theory) = thy -\ ML \ (*or*) -fun dummy2 _ (ctxt: Proof.context) = ctxt -\ ML \ -val _ = - Outer_Syntax.command \<^command_keyword>\Model\ "Model dummy" - ((@{print}, Parse.$$$ ":") @@>> (Toplevel.theory o dummy)) -\ ML \ -val _ = - Outer_Syntax.command \<^command_keyword>\Given\ "input Given items to the Model of a Specification" -(* (facts >> (Toplevel.proof o Proof.from_thmss_cmd));*) - ((@{print}, facts) @@>> (Toplevel.proof o Proof.from_thmss_cmd)); -val _ = - Outer_Syntax.command \<^command_keyword>\Where\ "input Find items to the Model of a Specification" - (facts @>> (Toplevel.proof o Proof.from_thmss_cmd)); -val _ = - Outer_Syntax.command \<^command_keyword>\Find\ "input Find items to the Model of a Specification" - (facts @>> (Toplevel.proof o Proof.from_thmss_cmd)); -val _ = - Outer_Syntax.command \<^command_keyword>\Relate\ "input Relate items to the Model of a Specification" - (facts @>> (Toplevel.proof o Proof.from_thmss_cmd)); -\ ML \ -(Toplevel.proof o Proof.from_thmss_cmd) -: - (Facts.ref * Token.src list) list list -> Toplevel.transition -> Toplevel.transition -(* ^^^^^^^^^^^^^^^^^^^ ^^^^^^^^^^^^^^^^^^^*) -\ ML \ -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 "")))); -\ ML \ -\ ML \ -\ - -subsection \runs with test-Example\ -(**) -ExampleSPARK \../Examples/exp_Statics_Biegel_Timischl_7-70.str\ -(**) -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*) -(* - TODO: compare click on above Given: "Traegerlaenge ", "Streckenlast " - with click on from \0 < d\ in SPARK/../Greatest_Common_Divisorthy -*) - -end \ No newline at end of file diff -r d5c670beaba4 -r 5038589d3033 src/Tools/isac/BridgeJEdit/SPARK_FDL.thy --- a/src/Tools/isac/BridgeJEdit/SPARK_FDL.thy Tue Aug 23 18:05:08 2022 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,8 +0,0 @@ -theory SPARK_FDL - imports Complex_Main -begin - -ML_file fdl_lexer.ML (*replace with native Isabelle*) -ML_file fdl_parser.ML (*replace with native Isabelle*) - -end \ No newline at end of file diff -r d5c670beaba4 -r 5038589d3033 src/Tools/isac/BridgeJEdit/fdl_lexer.ML --- a/src/Tools/isac/BridgeJEdit/fdl_lexer.ML Tue Aug 23 18:05:08 2022 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,362 +0,0 @@ -(* Title: HOL/SPARK/Tools/fdl_lexer.ML - Author: Stefan Berghofer - Copyright: secunet Security Networks AG - -Lexical analyzer for fdl files. -*) - -signature FDL_LEXER = -sig - datatype kind = Keyword | Ident | Long_Ident | Traceability | Number | Comment | EOF - datatype T = Token of kind * string * Position.T; - type chars - type banner - type date - type time - val tokenize: (chars -> 'a * chars) -> (chars -> T * chars) -> - Position.T -> string -> 'a * T list - val position_of: T -> Position.T - val pos_of: T -> string - val is_eof: T -> bool - val stopper: T Scan.stopper - val kind_of: T -> kind - val content_of: T -> string - val unparse: T -> string - val is_proper: T -> bool - val is_digit: string -> bool - val is_char_eof: string * 'a -> bool - val c_comment: chars -> T * chars - val curly_comment: chars -> T * chars - val percent_comment: chars -> T * chars - val vcg_header: chars -> (banner * (date * time) option) * chars - val siv_header: chars -> - (banner * (date * time) * (date * time) * (string * string)) * chars (*.. NOT [], but .. - (^^^^^^^^^^^^^^^ header ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^) ^^^^^ ..trailing line=13..117 *) - val explode_pos: string -> Position.T -> chars - val leq_token: T * T -> bool - val lexicon: Scan.lexicon - val identifier: chars -> chars * chars - val long_identifier: chars -> chars * chars - val banner: chars -> (string * string * string) * chars - val date: chars -> (string * string * string) * chars; - val whitespace: chars -> chars * chars - val whitespace1: chars -> chars * chars - val keyword: string -> chars -> chars * chars - val number: chars -> chars * chars - val any: chars -> (string * Position.T) * chars - val any_line: chars -> string * chars; - val !!! : string -> (chars -> 'a) -> chars -> 'a - val $$$ : string -> chars -> chars * chars - val scan: (chars -> 'a * chars) -> (chars -> T * chars) -> chars -> ('a * T list) * chars; - val char_stopper: (string * Position.T) Scan.stopper - val make_token: kind -> chars -> T -end; - -structure Fdl_Lexer(**): FDL_LEXER(**) = -struct - -(** tokens **) - -datatype kind = Keyword | Ident | Long_Ident | Traceability | Number | Comment | EOF; - -datatype T = Token of kind * string * Position.T; -(*for Formalise.T ^^^^ NOT required?*) - -fun make_token k xs = Token (k, implode (map fst xs), - case xs of [] => Position.none | (_, p) :: _ => p); - -fun kind_of (Token (k, _, _)) = k; - -fun is_proper (Token (Comment, _, _)) = false - | is_proper _ = true; - -fun content_of (Token (_, s, _)) = s; - -fun unparse (Token (Traceability, s, _)) = "For " ^ s ^ ":" - | unparse (Token (_, s, _)) = s; - -fun position_of (Token (_, _, pos)) = pos; - -val pos_of = Position.here o position_of; - -fun is_eof (Token (EOF, _, _)) = true - | is_eof _ = false; - -fun mk_eof pos = Token (EOF, "", pos); -val eof = mk_eof Position.none; - -val stopper = - Scan.stopper (fn [] => eof | toks => mk_eof (position_of (List.last toks))) is_eof; - -fun leq_token (Token (_, s, _), Token (_, s', _)) = size s <= size s'; - - -(** split up a string into a list of characters (with positions) **) - -type chars = (string * Position.T) list; - -fun is_char_eof ("", _) = true - | is_char_eof _ = false; - -val char_stopper = Scan.stopper (K ("", Position.none)) is_char_eof; - -fun symbol (x : string, _ : Position.T) = x; - -(* convert string s to chars ("", pos) *) -fun explode_pos s pos = fst (fold_map (fn x => fn pos => - ((x, pos), Position.symbol x pos)) (raw_explode s) pos); - - -(** scanners **) - -val any = Scan.one (not o Scan.is_stopper char_stopper); - -fun prfx [] = Scan.succeed [] - | prfx (x :: xs) = Scan.one (equal x o symbol) ::: prfx xs; - -val $$$ = prfx o raw_explode; - -val lexicon = Scan.make_lexicon (map raw_explode - ["rule_family", - "For", - ":", - "[", - "]", - "(", - ")", - ",", - "&", - ";", - "=", - ".", - "..", - "requires", - "may_be_replaced_by", - "may_be_deduced", - "may_be_deduced_from", - "are_interchangeable", - "if", - "end", - "function", - "procedure", - "type", - "var", - "const", - "array", - "record", - ":=", - "of", - "**", - "*", - "/", - "div", - "mod", - "+", - "-", - "<>", - "<", - ">", - "<=", - ">=", - "<->", - "->", - "not", - "and", - "or", - "for_some", - "for_all", - "***", - "!!!", - "element", - "update", - "pending"]); - -fun keyword s = Scan.literal lexicon :|-- - (fn xs => if map symbol xs = raw_explode s then Scan.succeed xs else Scan.fail); - -fun is_digit x = "0" <= x andalso x <= "9"; -fun is_alpha x = "a" <= x andalso x <= "z" orelse "A" <= x andalso x <= "Z"; -val is_underscore = equal "_"; -val is_tilde = equal "~"; -val is_newline = equal "\n"; -val is_tab = equal "\t"; -val is_space = equal " "; -val is_whitespace = is_space orf is_tab orf is_newline; -val is_whitespace' = is_space orf is_tab; - -val number = Scan.many1 (is_digit o symbol); - -val identifier = - Scan.one (is_alpha o symbol) ::: - Scan.many - ((is_alpha orf is_digit orf is_underscore) o symbol) @@@ - Scan.optional (Scan.one (is_tilde o symbol) >> single) []; - -val long_identifier = - identifier @@@ Scan.repeats1 ($$$ "." @@@ identifier); - -val whitespace = Scan.many (is_whitespace o symbol); -val whitespace1 = Scan.many1 (is_whitespace o symbol); -val whitespace' = Scan.many (is_whitespace' o symbol); -val newline = Scan.one (is_newline o symbol); - -fun beginning n cs = - let - val drop_blanks = drop_suffix is_whitespace; - val all_cs = drop_blanks cs; - val dots = if length all_cs > n then " ..." else ""; - in - (drop_blanks (take n all_cs) - |> map (fn c => if is_whitespace c then " " else c) - |> implode) ^ dots - end; - -fun !!! text scan = - let - fun get_pos [] = " (end-of-input)" - | get_pos ((_, pos) :: _) = Position.here pos; - - fun err (syms, msg) = fn () => - text ^ get_pos syms ^ " at " ^ beginning 10 (map symbol syms) ^ - (case msg of NONE => "" | SOME m => "\n" ^ m ()); - in Scan.!! err scan end; - -val any_line' = - Scan.many (not o (Scan.is_stopper char_stopper orf (is_newline o symbol))); - -val any_line = whitespace' |-- any_line' --| - newline >> (implode o map symbol); - -fun gen_comment a b = $$$ a |-- !!! "unclosed comment" - (Scan.repeat (Scan.unless ($$$ b) any) --| $$$ b) >> make_token Comment; - -val c_comment = gen_comment "/*" "*/"; -fun c_comment chars = - let -(** )val _ = @{print} {a = "//--- ###I Fdl_Lexer.c_comment called with", - b_lenght_chars = length chars, chars = chars};( **) - val xxx as (redex, toks) = (gen_comment "/*" "*/") chars -(** )val _ = @{print} {z = "\\--- ###I Fdl_Lexer.c_comment \", - b_lenght_chars = length toks, res = xxx};( **) - in xxx end; -val curly_comment = gen_comment "{" "}"; - -val percent_comment = $$$ "%" |-- any_line' >> make_token Comment; - -fun repeatn 0 _ = Scan.succeed [] - | repeatn n p = Scan.one p ::: repeatn (n-1) p; - - -(** header of *.vcg and *.siv files (see simplifier/load_provenance.pro) **) - -type banner = string * string * string; -type date = string * string * string; -type time = string * string * string * string option; - -val asterisks = Scan.repeat1 (Scan.one (equal "*" o symbol)); - -fun alphan n = repeatn n (is_alpha o symbol) >> (implode o map symbol); -fun digitn n = repeatn n (is_digit o symbol) >> (implode o map symbol); - -val time = - digitn 2 --| $$$ ":" -- digitn 2 --| $$$ ":" -- digitn 2 -- - Scan.option ($$$ "." |-- digitn 2) >> - (fn (((hr, mi), s), ms) => (hr, mi, s, ms)); - -val date = - digitn 2 --| $$$ "-" -- alphan 3 --| $$$ "-" -- digitn 4 >> - (fn ((d, m), y) => (d, m, y)); - -val banner = - whitespace' |-- asterisks --| whitespace' --| newline :|-- (fn xs => - (any_line -- any_line -- any_line >> -(*WN:^^^^^^^^ ^^^^^^^^ ^^^^^^^^ 3 lines ending with \n *) - (fn ((l1, l2), l3) => (l1, l2, l3))) --| - whitespace' --| prfx (map symbol xs) --| whitespace' --| newline); - -val vcg_header = banner -- Scan.option (whitespace |-- - $$$ "DATE :" |-- whitespace |-- date --| whitespace --| - Scan.option ($$$ "TIME :" -- whitespace) -- time); - -val siv_header = banner --| whitespace -- - ($$$ "CREATED" |-- whitespace |-- (date --| $$$ "," --| whitespace -- time)) --| - whitespace -- - ($$$ "SIMPLIFIED" |-- whitespace |-- (date --| $$$ "," --| whitespace -- time)) --| - newline --| newline -- (any_line -- any_line) >> - (fn (((b, c), s), ls) => (b, c, s, ls)); - -(*WN: print ---vvvvv*) -fun siv_header chars = - let -(** )val _ = @{print} {a = "//--- ###I Fdl_Lexer.siv_header called with", - b_lenght_chars = length chars, chars = chars};( **) - val xxx as (redex, toks) = - ( - banner --| whitespace -- - ($$$ "CREATED" |-- whitespace |-- (date --| $$$ "," --| whitespace -- time)) --| - whitespace -- - ($$$ "SIMPLIFIED" |-- whitespace |-- (date --| $$$ "," --| whitespace -- time)) --| - newline --| newline -- (any_line -- any_line) >> - (fn (((b, c), s), ls) => (b, c, s, ls)) - ) chars; -(** )val _ = @{print} {z = "\\--- ###I Fdl_Lexer.siv_header \", - b_lenght_chars = length toks, res = xxx};( **) - in xxx end; - -(** the main tokenizer **) - -fun scan header comment = - !!! "bad header" header --| whitespace -- - Scan.repeat (Scan.unless (Scan.one is_char_eof) - (!!! "bad input" - ( comment - || (keyword "For" -- whitespace1) |-- - Scan.repeat1 (Scan.unless (keyword ":") any) --| - keyword ":" >> make_token Traceability - || Scan.max leq_token - (Scan.literal lexicon >> make_token Keyword) - ( long_identifier >> make_token Long_Ident - || identifier >> make_token Ident) - || number >> make_token Number) --| - whitespace) ); -fun scan header comment chars = - let - (** )val _ = @{print} {a = "//--- ###I Fdl_Lexer.scan called with", - b_lenght_chars = length chars, chars = chars};( **) - val xxx as (redex, toks) = - (!!! "bad header" header --| whitespace -- - Scan.repeat (Scan.unless (Scan.one is_char_eof) - (!!! "bad input" - ( comment - || (keyword "For" -- whitespace1) |-- - Scan.repeat1 (Scan.unless (keyword ":") any) --| - keyword ":" >> make_token Traceability - || Scan.max leq_token - (Scan.literal lexicon >> make_token Keyword) - ( long_identifier >> make_token Long_Ident - || identifier >> make_token Ident) - || number >> make_token Number) --| - whitespace))) chars - (** )val _ = @{print} {z = "\\--- ###I Fdl_Lexer.scan \", - b_lenght_chars = length toks, res = xxx};( **) - in xxx end; - -fun tokenize header comment pos s = - fst (Scan.finite char_stopper - (Scan.error (scan header comment)) (explode_pos s pos)); - -fun tokenize header(*= Fdl_Lexer.siv_header*) comment pos s = -((** )@{print} {a = "//--- ###I Fdl_Lexer.tokenize called with", header = header, - comment = comment, pos = pos, s = s};( **) - let -(** )val _ = @{print} {a = "###I Fdl_Lexer.tokenize: explode_pos", res = explode_pos s pos};( **) -(*convert string s to chars ("", pos) is ---vvvvvvvvvvv ^^^^^^^^^^^*) - val xxx as (redex, toks) = - fst (Scan.finite char_stopper - (Scan.error (scan header comment)) (explode_pos s pos)) -(** )val _ = @{print} {a = "\\--- ###I Fdl_Lexer.tokenize \", - b_lenght_chars = length toks, res = xxx};( **) - in xxx end -); - -end; diff -r d5c670beaba4 -r 5038589d3033 src/Tools/isac/BridgeJEdit/fdl_parser.ML --- a/src/Tools/isac/BridgeJEdit/fdl_parser.ML Tue Aug 23 18:05:08 2022 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,415 +0,0 @@ -(* Title: HOL/SPARK/Tools/fdl_parser.ML - Author: Stefan Berghofer - Copyright: secunet Security Networks AG - -Parser for fdl files. -*) - -signature FDL_PARSER = -sig - datatype expr = - Ident of string - | Number of int - | Quantifier of string * string list * string * expr - | Funct of string * expr list - | Element of expr * expr list - | Update of expr * expr list * expr - | Record of string * (string * expr) list - | Array of string * expr option * - ((expr * expr option) list list * expr) list; - - datatype fdl_type = - Basic_Type of string - | Enum_Type of string list - | Array_Type of string list * string - | Record_Type of (string list * string) list - | Pending_Type; - - datatype fdl_rule = - Inference_Rule of expr list * expr - | Substitution_Rule of expr list * expr * expr; - - type rules = - ((string * int) * fdl_rule) list * - (string * (expr * (string * string) list) list) list; - val empty_rules: rules - - type vcs = (string * (string * - ((string * expr) list * (string * expr) list)) list) list; - val empty_vcs: (string * string) * vcs - - type 'a tab = 'a Symtab.table * (string * 'a) list; - - val lookup: 'a tab -> string -> 'a option; - val update: string * 'a -> 'a tab -> 'a tab; - val items: 'a tab -> (string * 'a) list; - - type decls = - {types: fdl_type tab, - vars: string tab, - consts: string tab, - funs: (string list * string) tab}; - val empty_decls: decls - - val parse_vcs: (Fdl_Lexer.chars -> 'a * Fdl_Lexer.chars) -> Position.T -> - string -> 'a * ((string * string) * vcs); - - val parse_declarations: Position.T -> string -> (string * string) * decls; - - val parse_rules: Position.T -> string -> rules; - val vcs: Fdl_Lexer.T list -> - ((string * string) * (string * (string * ((string * expr) list * (string * expr) list)) list) list) * Fdl_Lexer.T list; - val !!! : (Fdl_Lexer.T list -> 'a) -> Fdl_Lexer.T list -> 'a; - val $$$ : string -> Fdl_Lexer.T list -> string * Fdl_Lexer.T list - val group: string -> ('a -> 'b) -> 'a -> 'b - val identifier: Fdl_Lexer.T list -> string * Fdl_Lexer.T list - val enum1: string -> (Fdl_Lexer.T list -> 'a * Fdl_Lexer.T list) -> Fdl_Lexer.T list -> - 'a list * Fdl_Lexer.T list - val list1: (Fdl_Lexer.T list -> 'a * Fdl_Lexer.T list) -> Fdl_Lexer.T list -> - 'a list * Fdl_Lexer.T list -end; - -structure Fdl_Parser(**): FDL_PARSER(**) = -struct - -(** error handling **) - -fun beginning n cs = - let val dots = if length cs > n then " ..." else ""; - in - space_implode " " (take n cs) ^ dots - end; - -fun !!! scan = - let - fun get_pos [] = " (end-of-input)" - | get_pos (tok :: _) = Fdl_Lexer.pos_of tok; - - fun err (syms, msg) = fn () => - "Syntax error" ^ get_pos syms ^ " at " ^ - beginning 10 (map Fdl_Lexer.unparse syms) ^ - (case msg of NONE => "" | SOME m => "\n" ^ m () ^ " expected"); - in Scan.!! err scan end; - -fun parse_all p = - Scan.repeat (Scan.unless (Scan.one Fdl_Lexer.is_eof) (!!! p)); - - -(** parsers **) - -fun group s p = p || Scan.fail_with (K (fn () => s)); - -fun $$$ s = group s - (Scan.one (fn t => Fdl_Lexer.kind_of t = Fdl_Lexer.Keyword andalso - Fdl_Lexer.content_of t = s) >> K s); - -val identifier = group "identifier" - (Scan.one (fn t => Fdl_Lexer.kind_of t = Fdl_Lexer.Ident) >> - Fdl_Lexer.content_of); - -val long_identifier = group "long identifier" - (Scan.one (fn t => Fdl_Lexer.kind_of t = Fdl_Lexer.Long_Ident) >> - Fdl_Lexer.content_of); - -fun the_identifier s = group s - (Scan.one (fn t => Fdl_Lexer.kind_of t = Fdl_Lexer.Ident andalso - Fdl_Lexer.content_of t = s) >> K s); - -fun prfx_identifier g s = group g - (Scan.one (fn t => Fdl_Lexer.kind_of t = Fdl_Lexer.Ident andalso - can (unprefix s) (Fdl_Lexer.content_of t)) >> - (unprefix s o Fdl_Lexer.content_of)); - -val mk_identifier = prfx_identifier "identifier \"mk__...\"" "mk__"; -val hyp_identifier = prfx_identifier "hypothesis identifer" "H"; -val concl_identifier = prfx_identifier "conclusion identifier" "C"; - -val number = group "number" - (Scan.one (fn t => Fdl_Lexer.kind_of t = Fdl_Lexer.Number) >> - (the o Int.fromString o Fdl_Lexer.content_of)); - -val traceability = group "traceability information" - (Scan.one (fn t => Fdl_Lexer.kind_of t = Fdl_Lexer.Traceability) >> - Fdl_Lexer.content_of); - -fun enum1 sep scan = scan ::: Scan.repeat ($$$ sep |-- !!! scan); -fun enum sep scan = enum1 sep scan || Scan.succeed []; - -fun list1 scan = enum1 "," scan; -fun list scan = enum "," scan; - - -(* expressions, see section 4.4 of SPARK Proof Manual *) - -datatype expr = - Ident of string - | Number of int - | Quantifier of string * string list * string * expr - | Funct of string * expr list - | Element of expr * expr list - | Update of expr * expr list * expr - | Record of string * (string * expr) list - | Array of string * expr option * - ((expr * expr option) list list * expr) list; - -fun unop (f, x) = Funct (f, [x]); - -fun binop p q = p :|-- (fn x => Scan.optional - (q -- !!! p >> (fn (f, y) => Funct (f, [x, y]))) x); - -(* left-associative *) -fun binops opp argp = - argp -- Scan.repeat (opp -- !!! argp) >> (fn (x, fys) => - fold (fn (f, y) => fn x => Funct (f, [x, y])) fys x); - -(* right-associative *) -fun binops' f p = enum1 f p >> foldr1 (fn (x, y) => Funct (f, [x, y])); - -val multiplying_operator = $$$ "*" || $$$ "/" || $$$ "div" || $$$ "mod"; - -val adding_operator = $$$ "+" || $$$ "-"; - -val relational_operator = - $$$ "=" || $$$ "<>" - || $$$ "<" || $$$ ">" - || $$$ "<="|| $$$ ">="; - -val quantification_kind = $$$ "for_all" || $$$ "for_some"; - -val quantification_generator = - list1 identifier --| $$$ ":" -- identifier; - -fun opt_parens p = $$$ "(" |-- p --| $$$ ")" || p; - -fun expression xs = group "expression" - (binop disjunction ($$$ "->" || $$$ "<->")) xs - -and disjunction xs = binops' "or" conjunction xs - -and conjunction xs = binops' "and" negation xs - -and negation xs = - ( $$$ "not" -- !!! relation >> unop - || relation) xs - -and relation xs = binop sum relational_operator xs - -and sum xs = binops adding_operator term xs - -and term xs = binops multiplying_operator factor xs - -and factor xs = - ( $$$ "+" |-- !!! primary - || $$$ "-" -- !!! primary >> unop - || binop primary ($$$ "**")) xs - -and primary xs = group "primary" - ( number >> Number - || $$$ "(" |-- !!! (expression --| $$$ ")") - || quantified_expression - || function_designator - || identifier >> Ident) xs - -and quantified_expression xs = (quantification_kind -- - !!! ($$$ "(" |-- quantification_generator --| $$$ "," -- - expression --| $$$ ")") >> (fn (q, ((xs, T), e)) => - Quantifier (q, xs, T, e))) xs - -and function_designator xs = - ( mk_identifier --| $$$ "(" :|-- - (fn s => record_args s || array_args s) --| $$$ ")" - || $$$ "element" |-- !!! ($$$ "(" |-- expression --| $$$ "," --| $$$ "[" -- - list1 expression --| $$$ "]" --| $$$ ")") >> Element - || $$$ "update" |-- !!! ($$$ "(" |-- expression --| $$$ "," --| $$$ "[" -- - list1 expression --| $$$ "]" --| $$$ "," -- expression --| $$$ ")") >> - (fn ((A, xs), x) => Update (A, xs, x)) - || identifier --| $$$ "(" -- !!! (list1 expression --| $$$ ")") >> Funct) xs - -and record_args s xs = - (list1 (identifier --| $$$ ":=" -- !!! expression) >> (pair s #> Record)) xs - -and array_args s xs = - ( array_associations >> (fn assocs => Array (s, NONE, assocs)) - || expression -- Scan.optional ($$$ "," |-- !!! array_associations) [] >> - (fn (default, assocs) => Array (s, SOME default, assocs))) xs - -and array_associations xs = - (list1 (opt_parens (enum1 "&" ($$$ "[" |-- - !!! (list1 (expression -- Scan.option ($$$ ".." |-- !!! expression)) --| - $$$ "]"))) --| $$$ ":=" -- expression)) xs; - - -(* verification conditions *) - -type vcs = (string * (string * - ((string * expr) list * (string * expr) list)) list) list; - -val vc = - identifier --| $$$ "." -- !!! - ( $$$ "***" |-- !!! (the_identifier "true" --| $$$ ".") >> - (Ident #> pair "1" #> single #> pair []) - || $$$ "!!!" |-- !!! (the_identifier "false" --| $$$ ".") >> - (Ident #> pair "1" #> single #> pair []) - || Scan.repeat1 (hyp_identifier -- - !!! ($$$ ":" |-- expression --| $$$ ".")) --| $$$ "->" -- - Scan.repeat1 (concl_identifier -- - !!! ($$$ ":" |-- expression --| $$$ "."))); - -val subprogram_kind = $$$ "function" || $$$ "procedure"; - -val vcs = - subprogram_kind -- (long_identifier || identifier) -- - parse_all (traceability -- !!! (Scan.repeat1 vc)); -val empty_vcs = (("e_procedure", "e_G_C_D"), []: vcs) - -fun parse_vcs header pos s = -(*line_1*)s |> -(*line_2*)Fdl_Lexer.tokenize header Fdl_Lexer.c_comment pos ||> -(*line_3*)filter Fdl_Lexer.is_proper ||> -(*line_4*)Scan.finite Fdl_Lexer.stopper (Scan.error (!!! vcs)) ||> -(*line_5*)fst; -(* vvvvvv-------- = Fdl_Lexer.siv_header*) -fun parse_vcs header pos s = -((** )@{print} {a = "//--- ###I Fdl_Parser.parse_vcs", header = header, pos = pos, s = s};( **) - let - val line_2 = Fdl_Lexer.tokenize header Fdl_Lexer.c_comment pos s -(** )val _ = @{print} {a = "###I Fdl_Parser.parse_vcs: ", line_2 = line_2};( **) - val line_3 = apsnd (filter Fdl_Lexer.is_proper) line_2 - val line_4 = apsnd (Scan.finite Fdl_Lexer.stopper (Scan.error (!!! vcs))) line_3 - val line_5 = apsnd fst line_4 -(** )val _ = @{print} {z = "\\--- ###I Fdl_Parser.parse_vcs \", res = line_5};( **) - in line_5 end -); - - -(* fdl declarations, see section 4.3 of SPARK Proof Manual *) - -datatype fdl_type = - Basic_Type of string - | Enum_Type of string list - | Array_Type of string list * string - | Record_Type of (string list * string) list - | Pending_Type; - -(* also store items in a list to preserve order *) -type 'a tab = 'a Symtab.table * (string * 'a) list; - -fun lookup ((tab, _) : 'a tab) = Symtab.lookup tab; -fun update decl (tab, items) = (Symtab.update_new decl tab, decl :: items); -fun items ((_, items) : 'a tab) = rev items; - -type decls = - {types: fdl_type tab, - vars: string tab, - consts: string tab, - funs: (string list * string) tab}; - -val empty_decls : decls = - {types = (Symtab.empty, []), vars = (Symtab.empty, []), - consts = (Symtab.empty, []), funs = (Symtab.empty, [])}; - -fun add_type_decl decl {types, vars, consts, funs} = - {types = update decl types, - vars = vars, consts = consts, funs = funs} - handle Symtab.DUP s => error ("Duplicate type " ^ s); - -fun add_var_decl (vs, ty) {types, vars, consts, funs} = - {types = types, - vars = fold (update o rpair ty) vs vars, - consts = consts, funs = funs} - handle Symtab.DUP s => error ("Duplicate variable " ^ s); - -fun add_const_decl decl {types, vars, consts, funs} = - {types = types, vars = vars, - consts = update decl consts, - funs = funs} - handle Symtab.DUP s => error ("Duplicate constant " ^ s); - -fun add_fun_decl decl {types, vars, consts, funs} = - {types = types, vars = vars, consts = consts, - funs = update decl funs} - handle Symtab.DUP s => error ("Duplicate function " ^ s); - -fun type_decl x = ($$$ "type" |-- !!! (identifier --| $$$ "=" -- - ( identifier >> Basic_Type - || $$$ "(" |-- !!! (list1 identifier --| $$$ ")") >> Enum_Type - || $$$ "array" |-- !!! ($$$ "[" |-- list1 identifier --| $$$ "]" --| - $$$ "of" -- identifier) >> Array_Type - || $$$ "record" |-- !!! (enum1 ";" - (list1 identifier -- !!! ($$$ ":" |-- identifier)) --| - $$$ "end") >> Record_Type - || $$$ "pending" >> K Pending_Type)) >> add_type_decl) x; - -fun const_decl x = ($$$ "const" |-- !!! (identifier --| $$$ ":" -- identifier --| - $$$ "=" --| $$$ "pending") >> add_const_decl) x; - -fun var_decl x = ($$$ "var" |-- !!! (list1 identifier --| $$$ ":" -- identifier) >> - add_var_decl) x; - -fun fun_decl x = ($$$ "function" |-- !!! (identifier -- - (Scan.optional ($$$ "(" |-- !!! (list1 identifier --| $$$ ")")) [] --| - $$$ ":" -- identifier)) >> add_fun_decl) x; - -fun declarations x = - (the_identifier "title" |-- subprogram_kind -- identifier --| $$$ ";" -- - (Scan.repeat ((type_decl || const_decl || var_decl || fun_decl) --| - !!! ($$$ ";")) >> (fn ds => fold I ds empty_decls)) --| - $$$ "end" --| $$$ ";") x; - -fun parse_declarations pos s = - s |> - Fdl_Lexer.tokenize (Scan.succeed ()) Fdl_Lexer.curly_comment pos |> - snd |> filter Fdl_Lexer.is_proper |> - Scan.finite Fdl_Lexer.stopper (Scan.error (!!! declarations)) |> - fst; - - -(* rules, see section 5 of SPADE Proof Checker Rules Manual *) - -datatype fdl_rule = - Inference_Rule of expr list * expr - | Substitution_Rule of expr list * expr * expr; - -type rules = - ((string * int) * fdl_rule) list * - (string * (expr * (string * string) list) list) list; -val empty_rules = - ([]: ((string * int) * fdl_rule) list, - []: (string * (expr * (string * string) list) list) list); - -val condition_list = $$$ "[" |-- list expression --| $$$ "]"; -val if_condition_list = $$$ "if" |-- !!! condition_list; - -val rule = - identifier -- !!! ($$$ "(" |-- number --| $$$ ")" --| $$$ ":" -- - (expression :|-- (fn e => - $$$ "may_be_deduced" >> K (Inference_Rule ([], e)) - || $$$ "may_be_deduced_from" |-- - !!! condition_list >> (Inference_Rule o rpair e) - || $$$ "may_be_replaced_by" |-- !!! (expression -- - Scan.optional if_condition_list []) >> (fn (e', cs) => - Substitution_Rule (cs, e, e')) - || $$$ "&" |-- !!! (expression --| $$$ "are_interchangeable" -- - Scan.optional if_condition_list []) >> (fn (e', cs) => - Substitution_Rule (cs, e, e')))) --| $$$ ".") >> - (fn (id, (n, rl)) => ((id, n), rl)); - -val rule_family = - $$$ "rule_family" |-- identifier --| $$$ ":" -- - enum1 "&" (expression -- !!! ($$$ "requires" |-- $$$ "[" |-- - list (identifier -- !!! ($$$ ":" |-- identifier)) --| $$$ "]")) --| - $$$ "."; - -val rules = - parse_all (rule >> (apfst o cons) || rule_family >> (apsnd o cons)) >> - (fn rls => fold_rev I rls ([], [])); - -fun parse_rules pos s = - s |> - Fdl_Lexer.tokenize (Scan.succeed ()) - (Fdl_Lexer.c_comment || Fdl_Lexer.percent_comment) pos |> - snd |> filter Fdl_Lexer.is_proper |> - Scan.finite Fdl_Lexer.stopper (Scan.error (!!! rules)) |> - fst; - -end; diff -r d5c670beaba4 -r 5038589d3033 src/Tools/isac/BridgeJEdit/parseC-OLD.sml --- a/src/Tools/isac/BridgeJEdit/parseC-OLD.sml Tue Aug 23 18:05:08 2022 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,387 +0,0 @@ -(* Title: Tools/isac/BridgeJEdit/parseC-OLD.sml - Author: Walther Neuper, JKU Linz - (c) due to copyright terms - -Outer token syntax for Isabelle/Isac via . -*) - -signature PARSE_C_OLD = -sig - type problem - val problem: problem parser - type problem_headline - val problem_headline: problem_headline parser - -(* exclude "Problem" from parsing * ) - val read_out_headline: headline_string * Token.src -> ThyC.id * Problem.id -( * exclude "Problem" from parsing *) - val read_out_headline: problem_headline -> ThyC.id * Problem.id -(* exclude "Problem" from parsing *) - val read_out_problem: problem -> P_Spec.record - - val tokenize_formalise: Position.T -> string -> Fdl_Lexer.T list * Fdl_Lexer.chars - - type form_model = TermC.as_string list; - type form_refs = (((((string * ThyC.id) * string) * Problem.id) * string) * MethodC.id) * string - type form_model_refs = - (((((string * string) * form_model) * string) * form_refs) * string) * string - - val read_out_formalise: form_model_refs -> Formalise.T list - (*RENAME TO parse_formalise..*) - val formalisation: Fdl_Lexer.T list -> form_model_refs * Fdl_Lexer.T list; - -\<^isac_test>\ - val tokenize: string -> Token.src - val string_of_toks: Token.src -> string - val parse: (Token.src -> 'a * Token.src) -> Token.src -> 'a * Token.src - - (*Model*) - type model - val model: model parser - - (*References*) - type refs - type model_refs_dummy = model * ((string * string) * refs) - val model_refs_dummy: model_refs_dummy - val references: ((string * string) * refs) parser - val refs_dummy: refs - - (*Specification*) - type specification = (string * string) * model_refs_dummy - val specification: specification parser - - (*Tactics *) - val check_postcond: (string * string list) parser - val rewrite_set_inst: ((string * string) * string) parser - val substitute: ((string * string) * string) parser - val exec_check_postcond: string * string list -> string - val exec_rewrite_set_inst: (string * string) * string -> string - val exec_substitute: (string * string) * string -> string - - val tactic: Token.src -> (string * string) * Token.src - - (*Steps*) - val steps: (string * (string * string)) list parser - val exec_step_term: string * (string * string) -> string - val steps_subpbl: string list parser - - (*Problem*) - type body - val body: body parser - val body_dummy: body - - val tokenize_string: Fdl_Lexer.chars -> Fdl_Lexer.T * Fdl_Lexer.chars - val scan: Fdl_Lexer.chars -> Fdl_Lexer.T list * Fdl_Lexer.chars - val parse_form_refs: Fdl_Lexer.T list -> form_refs * Fdl_Lexer.T list; - val parse_form_model: Fdl_Lexer.T list -> string list * Fdl_Lexer.T list; - val parse_string : Fdl_Lexer.T list -> string * Fdl_Lexer.T list; -\ -end - -(**) -structure ParseC_OLD(**): PARSE_C_OLD(**) = -struct -(**) - -(**** Tools ****) - -\<^isac_test>\ -fun tokenize str = - filter Token.is_proper (Token.explode (Thy_Header.get_keywords' @{context}) Position.none str) - -fun parse parser toks = Scan.finite Token.stopper (Scan.error parser) toks - -fun string_of_toks toks = fold (curry op ^) (map Token.unparse toks |> rev |> separate ", ") ""; -\ - -(**** parse Calculation ****) - -(*** Problem headline ***) - -(* exclude "Problem" from parsing * ) -type problem_headline = (((((string * string) * string) * string) * string list) * string) -( * exclude "Problem" from parsing *) -type problem_headline = (((string * ThyC.id) * string) * Problem.id) * string -(* exclude "Problem" from parsing *) -val problem_headline = (*Parse.$$$ "Problem" --*) - Parse.$$$ "(" -- - Parse.string -- Parse.$$$ "," -- - (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]") -- - Parse.$$$ ")" - -(* exclude "Problem" from parsing * ) -fun string_of_headline ((((left, thy_id: ThyC.id), comm), pbl_id), right) = - left ^ thy_id ^ comm ^ Problem.id_to_string pbl_id ^ right -fun read_out_headline ((((("(", thy_id), ","), pbl_id), ")"), []) = (thy_id, pbl_id) - | read_out_headline (hdl, toks) = - raise ERROR ("read_out_headline NOT for: (" ^ string_of_headline hdl ^ ", " ^ - string_of_toks toks ^ ")") -( * exclude "Problem" from parsing *) -fun read_out_headline ((((("(", thy_id), ","), pbl_id), ")")) = (thy_id, pbl_id) - | read_out_headline arg = - (@{print} {a = "read_out_headline with", arg = arg}; raise ERROR "read_out_headline") -(**) - -(* used if at least "Problem (thy_id, pbl_id)" has been input *) -fun read_out_problem (((((( - "(", thy_id), ","), pbl_id), ")"), ((((( - _(*"Specification"*), _(*":"*)), ((((((((((((((( - _(*"Model"*), (("", ""), "")), _(*":"*)), - _(*"Given"*)), _(*":"*)), givens), - _(*"Where"*)), _(*":"*)), wheres), - _(*"Find"*)), _(*":"*)), find), - _(*"Relate"*)), _(*":"*)), relates), (( - _(*"References"*), _(*":"*)), (((((((( - _(*"RTheory"*), _(*":"*)), rthy_id), - _(*"RProblem"*)), _(*":"*)), rpbl_id), - _(*"RMethod"*)), _(*":"*)), rmet_id)))), - _(*"Solution"*)), _(*":"*)), - _(*[]*))), - _(*""*)) = - {thy_id = thy_id, pbl_id = pbl_id, - givens = givens, wheres = wheres, find = find, relates = relates, - rthy_id = rthy_id, rpbl_id = rpbl_id, rmet_id = rmet_id} - | read_out_problem arg = - (@{print} {a = "read_out_problem called with", arg = arg}; - raise ERROR "read_out_problem called with") - - -(*** Specification ***) - -(** Model **) - -type model = - ((((((((((((((string * ((string * string) * string)) * string) * string) * string) * - string list) * string) * string) * string list) * string) * string) * string) * - string) * string) * string list); -val model = ( - Parse.command_name "Model" -- - (Scan.optional (*.. show, whether the Model refers to RProblem or to RMethod *) - (Parse.$$$ "(" -- - (Parse.command_name "RProblem" || Parse.command_name "RMethod") -- Parse.$$$ ")") - (("", ""), "") ) -- - Parse.$$$ ":" -- - Parse.command_name "Given" -- Parse.$$$ ":" -- Parse.list1 Parse.term -- - Parse.command_name "Where" -- Parse.$$$ ":" -- Parse.list Parse.term -- - Parse.command_name "Find" -- Parse.$$$ ":" -- Parse.term -- - Parse.command_name "Relate" -- Parse.$$$ ":" -- Parse.list Parse.term -) - -(** References **) - -type refs = - ((((((((string * string) * string) * string) * string) * string list) * string) * string) * string list) -val refs_dummy = - (((((((("", ""), ""), ""), ""), []), ""), ""), []) - -val references = ( - Parse.command_name "References" -- Parse.$$$ ":" (**) -- - (Scan.optional - (Parse.command_name "RTheory" -- Parse.$$$ ":" -- Parse.string (**) -- - Parse.command_name "RProblem" -- Parse.$$$ ":" (**) -- - (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]") (**) -- - Parse.command_name "RMethod" -- Parse.$$$ ":" (**) -- - (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]") - ) - refs_dummy - )) - -(** compose Specification **) - -type model_refs_dummy = (model * ((string * string) * refs)) -val model_refs_dummy = ((((((((((((((("", (("", ""), "")), ""), ""), ""), - []), ""), ""), []), ""), ""), ""), ""), ""), - []), - (("", ""), (((((((("", ""), ""), ""), ""), []), - ""), ""), []))) - -type specification = (string * string) * model_refs_dummy -val specification = ( - (Parse.command_name "Specification" -- Parse.$$$ ":") -- - (Scan.optional - (model -- references) - ) - model_refs_dummy - ); - - -(*** Solution ***) -(** Tactics **) - -val substitute = Parse.reserved "Substitute" -- Parse.term -- Parse.term; -val rewrite_set_inst = Parse.reserved "Rewrite_Set_Inst" -- Parse.term -- Parse.name; -val check_postcond = Parse.reserved "Check_Postcond" -- - (Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]"); - -(* see test/../Test_Parsers.thy || requires arguments of equal type *) -fun exec_substitute ((str, tm), bdv) = - "EXEC IMMEDIATELY: " ^ str ^ " " ^ (*UnparseC.term*) tm ^ " " ^ (*UnparseC.term*) bdv; -fun exec_rewrite_set_inst ((str, tm), id) = - "EXEC IMMEDIATELY: " ^ str ^ " " ^ (*UnparseC.term*) tm ^ " " ^ (*Problem.id_to_string*) id; -fun exec_check_postcond (str, path) = - "EXEC IMMEDIATELY: " ^ str ^ " " ^ (*Problem.id_to_string*)fold (curry op ^) path ""; - -val tactic = ( (* incomplete list of tactics *) - Parse.$$$ "Tactic" -- - (substitute >> exec_substitute || - rewrite_set_inst >> exec_rewrite_set_inst || - check_postcond >> exec_check_postcond - ) - ) - -(** Step of term + tactic**) - -\<^isac_test>\ -val steps = (Scan.repeat (Parse.term -- (Scan.optional tactic ("", "")))) -\ - -fun exec_step_term (tm, (tac1, tac2)) = - "EXEC IMMEDIATELY step_term: " ^ (*UnparseC.term*) tm ^ " (" ^ tac1 ^ ", " ^ tac2 ^ ")"; -\<^isac_test>\ -val steps_subpbl = - Scan.repeat ( - ((Parse.term -- (Scan.optional tactic ("", ""))) >> exec_step_term) (** ) || - (problem >> exec_subproblem) ( **) - ) -\ - -(** Body **) - -type body = (((((string * string) * - (((((((((((((((string * ((string * string) * string)) * string) * string) * string) * string list) * string) * string) * string list) * string) * string) * string) * string) * string) * string list) * - ((string * string) * ((((((((string * string) * string) * string) * string) * string list) * string) * string) * string list)))) * - string) * string) * string list) -val body_dummy = ((((("", ""), - ((((((((((((((("", (("", ""), "")), ""), ""), ""), []), ""), ""), []), ""), ""), ""), ""), ""), []), - (("", ""), (((((((("", ""), ""), ""), ""), []), ""), ""), [])))), - ""), ""), []) -val body = - specification -- - Parse.command_name "Solution" -- Parse.$$$ ":" -- - (*/----- this will become "and steps".. *) - (Scan.repeat ( - ((Parse.term -- (Scan.optional tactic ("", ""))) >> exec_step_term) (** ) || - (problem >> exec_subproblem) ( *exec_* make types equal for both args of ||*) - )) - (*\----- ..this will become "and steps" - see Test_Parse_Isac subsubsection \trials on recursion stopped\ *) - - -(*** Problem ***) -(* exclude "Problem" from parsing * ) -type problem = - (((((((string * string) * string) * string) * string list) * string) * - (((((string * string) * - (((((((((((((((string * ((string * string) * string)) * string) * string) * string) * - string list) * string) * string) * string list) * string) * - string) * string) * string) * string) * string list) * - ((string * string) * - ((((((((string * string) * string) * string) * string) * string list) * string) * - string) * string list)))) * - string) * string) * string list)) * - string) -( * exclude "Problem" from parsing *) -type problem = - (((((string * string) * string) * string list) * string) * - (((((string * string) * - (((((((((((((((string * ((string * string) * string)) * string) * string) * string) * - string list) * string) * string) * string list) * string) * - string) * string) * string) * string) * string list) * - ((string * string) * - ((((((((string * string) * string) * string) * string) * string list) * string) - * string) * string list)))) * - string) * string) * string list)) * - string -(* exclude "Problem" from parsing *) -val problem = - problem_headline -- - (Scan.optional body) body_dummy -- - (Scan.optional Parse.term) "" - - -(**** parse Formalise ****) - -(*** Tokenizer, from HOL/SPARK/Tools/fdl_lexer.ML ***) - -val tokenize_string = Fdl_Lexer.$$$ "\"" |-- Fdl_Lexer.!!! "unclosed string" (*2*) - (Scan.repeat (Scan.unless (Fdl_Lexer.$$$ "\"") Fdl_Lexer.any) --| Fdl_Lexer.$$$ "\"") >> - Fdl_Lexer.make_token Fdl_Lexer.Comment(*!!!*); - -val scan = - Scan.repeat (Scan.unless (Scan.one Fdl_Lexer.is_char_eof) - (Fdl_Lexer.!!! "bad input" - ( tokenize_string (*.. this must be first *) - ||Scan.max Fdl_Lexer.leq_token - (Scan.literal Fdl_Lexer.lexicon >> Fdl_Lexer.make_token Fdl_Lexer.Keyword) - ( Fdl_Lexer.long_identifier >> Fdl_Lexer.make_token Fdl_Lexer.Long_Ident - || Fdl_Lexer.identifier >> Fdl_Lexer.make_token Fdl_Lexer.Ident) - ) --| - Fdl_Lexer.whitespace) ); - -fun tokenize_formalise pos str = - (Scan.finite Fdl_Lexer.char_stopper - (Scan.error scan) (Fdl_Lexer.explode_pos str pos)); - - -(*** the parser from HOL/SPARK/Tools/fdl_parser.ML ***) - -type form_model = TermC.as_string list; -type form_refs = (((((string * string) * string) * string list) * string) * string list) * string -type form_model_refs = ((((((string * string) * form_model) * string) * - ((((((string * ThyC.id) * string) * Problem.id) * string) * MethodC.id) * string)) * - string) * string) -type formalise = (((((string * string) * form_model) * string) * - ((((((string * ThyC.id) * string) * Problem.id) * string) * MethodC.id) * string)) * - string) * string; - -val parse_string = Fdl_Parser.group "string" - (Scan.one (fn t => Fdl_Lexer.kind_of t = Fdl_Lexer.Comment) >> - Fdl_Lexer.content_of); - -val parse_form_model = - (Fdl_Parser.$$$ "[" |-- Fdl_Parser.!!! ( - Fdl_Parser.list1 parse_string --| - Fdl_Parser.$$$ "]")); - -val parse_form_refs = - Fdl_Parser.$$$ "(" -- - parse_string -- (* "Biegelinie" *) - Fdl_Parser.$$$ "," -- - (Fdl_Parser.$$$ "[" |-- Fdl_Parser.!!! ( - Fdl_Parser.list1 parse_string --| (* ["Biegelinien"] *) - Fdl_Parser.$$$ "]")) -- - Fdl_Parser.$$$ "," -- - (Fdl_Parser.$$$ "[" |-- Fdl_Parser.!!! ( - Fdl_Parser.list1 parse_string --| (* ["IntegrierenUndKonstanteBestimmen2"] *) - Fdl_Parser.$$$ "]")) -- - Fdl_Parser.$$$ ")"; - -(*val parse_formalise = KEEP IDENTIFIERS CLOSE TO SPARK..*) -val formalisation = - Fdl_Parser.!!! ( - Fdl_Parser.$$$ "[" -- - Fdl_Parser.$$$ "(" -- - parse_form_model -- - Fdl_Parser.$$$ "," -- - parse_form_refs -- - Fdl_Parser.$$$ ")" -- - Fdl_Parser.$$$ "]"); - -fun read_out_formalise ((((( ( - "[", - "("), - form_model: TermC.as_string list), - ","), (((((( - "(", - thy_id: ThyC.id), - ","), - probl_id: Problem.id), - ","), - meth_id: MethodC.id), - ")")), - ")"), - "]") = [(form_model, (thy_id, probl_id, meth_id))] -| read_out_formalise _ = - raise ERROR "read_out_formalise: WRONGLY parsed"; - -(**)end(*struct*) diff -r d5c670beaba4 -r 5038589d3033 src/Tools/isac/BridgeJEdit/preliminary-OLD.sml --- a/src/Tools/isac/BridgeJEdit/preliminary-OLD.sml Tue Aug 23 18:05:08 2022 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,126 +0,0 @@ -(* Title: Tools/isac/BridgeJEdit/preliminary-OLD..sml - Author: Walther Neuper, JKU Linz - (c) due to copyright terms - -Preliminary code for start transition Libisabelle -- PIDE. -Will be distributed to several structures, most of which do not yet exist. -*) - -signature PRELIMINARY_OLD = -sig - (* for keyword ExampleSPARK *) - val store_and_show: theory -> Formalise.T list -> theory -> theory; - val load_formalisation: theory -> (Fdl_Lexer.T list -> ParseC_OLD.form_model_refs * 'a) -> - (theory -> Token.file * theory) * string -> theory -> theory - - (* for keyword Problem*) -(**)val init_specify: ParseC_OLD.problem_headline -> theory -> theory(**) -(** )val init_specify: ParseC_OLD.problem -> theory -> theory( **) -end - -(** code for keyword ExampleSPARK **) - -structure Refs_Data = Theory_Data -( - type T = References.T - val empty : T = References.empty - val extend = I - fun merge (_, refs) = refs -); -structure OMod_Data = Theory_Data -( - type T = O_Model.T - val empty : T = [] - val extend = I - fun merge (_, o_model) = o_model -); -structure IMod_Data = Theory_Data -( - type T = I_Model.T - val empty : T = [] - val extend = I - fun merge (_, i_model) = i_model -); -structure Ctxt_Data = Theory_Data -( - type T = Proof.context - val empty : T = ContextC.empty - val extend = I - fun merge (_, ctxt) = ctxt -); - -(**) -structure Preliminary_OLD(**): PRELIMINARY_OLD(**) = -struct -(**) - -fun store_and_show HACKthy formalise thy = - let -(**)val _(*file_read_correct*) = case formalise of xxx as - [(["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y", "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x", "GleichungsVariablen [c, c_2, c_3, c_4]", "AbleitungBiegelinie dy"], - ("Biegelinie", ["Biegelinien"], ["IntegrierenUndKonstanteBestimmen2"]))] => hd xxx - | _ => error "magic failed: handling file exp_Statics_Biegel_Timischl_7-70.str failed" -(**) - val formalise = hd formalise (*we expect only one Formalise.T in the list*) - val (_(*hdlPIDE*), _, refs, o_model, var_type_ctxt) = Step_Specify.initialisePIDEHACK HACKthy formalise - (* ^^ TODO remove with cleanup in nxt_specify_init_calc *) -(* - TODO: present "Problem hdlPIDE" via PIDE -*) - in - thy - |> Refs_Data.put refs - |> OMod_Data.put o_model - |> Ctxt_Data.put var_type_ctxt - end; - -(* -fun load_formalisation parser (files, _) thy = - let - val ([{lines, pos, ...}: Token.file], thy') = files thy; - in - store_and_show - (ParseC_OLD.read_out_formalise (fst (parser (fst (ParseC_OLD.tokenize_formalise pos (cat_lines lines)))))) - thy' - end; -*) -fun load_formalisation HACKthy parse (get_file: theory -> Token.file * theory, _: string) thy = - let - val (file, thy') = get_file thy; - val formalise = #lines file - |> cat_lines - |> ParseC_OLD.tokenize_formalise (#pos file) - |> fst - |> parse - |> fst - |> ParseC_OLD.read_out_formalise - |> store_and_show HACKthy -(**)val _ = @{print} {a = "### load_formalisation \", formalise = formalise}(**) - in - formalise thy' - end; - -(*** code for keyword Problem ***) - -(* -val prefer_input: ThyC.id * Problem.id -> References.T -> O_Model.T -> References.T * O_Model.T -*) -fun prefer_input (inthy, inpbl : Problem.id) (thy, pbl, met_id) o_model = - if inthy = thy andalso inpbl = pbl - then ((thy, pbl, met_id) : References.T, o_model) - else ((inthy, inpbl, MethodC.id_empty), []) - -fun init_specify problem thy = - let - val _ = @{print} {a = "//--- Spark_Commands.init_specify", headline = problem} - val (thy_id, pbl_id) = ParseC_OLD.read_out_headline problem (*how handle Position?!?*) - val refs' = Refs_Data.get thy - val ((_, pbl_id, _), _(*o_model*)) = - prefer_input (thy_id, pbl_id) refs' (OMod_Data.get thy) - val i_model = I_Model.initPIDE pbl_id -(* TODO: present Specification = i_model + refs via PIDE, if specify is done explicitly. *) - in - IMod_Data.put i_model thy (* the Model-items with Descriptor s only *) - end; -(**) -(**)end(**) diff -r d5c670beaba4 -r 5038589d3033 test/Tools/isac/BridgeJEdit/parseC.sml --- a/test/Tools/isac/BridgeJEdit/parseC.sml Tue Aug 23 18:05:08 2022 +0200 +++ b/test/Tools/isac/BridgeJEdit/parseC.sml Wed Aug 24 12:37:07 2022 +0200 @@ -6,19 +6,7 @@ "-----------------------------------------------------------------------------------------------"; "table of contents -----------------------------------------------------------------------------"; "-----------------------------------------------------------------------------------------------"; -"----------- complete Problem ------------------------------------------------------------------"; -"----------- Problem headline ------------------------------------------------------------------"; -"----------- Model -----------------------------------------------------------------------------"; -"----------- Model-items -----------------------------------------------------------------------"; -"----------- References ------------------------------------------------------------------------"; -"----------- Specification: References + Model -------------------------------------------------"; -"----------- Tactics ---------------------------------------------------------------------------"; -"----------- steps -----------------------------------------------------------------------------"; -"----------- body ------------------------------------------------------------------------------"; -"----------- Problem ---------------------------------------------------------------------------"; -"----------- fun read_out_problem --------------------------------------------------------------"; -"----------- THERE ARE TESTS with INCOMPLETE WORK IN Test_Parse_Isac.thy -----------------------"; -"----------- parser for exp_file.str -----------------------------------------------------------"; +"----------- TODO ------------------------------------------------------------------------------"; "-----------------------------------------------------------------------------------------------"; "-----------------------------------------------------------------------------------------------"; "-----------------------------------------------------------------------------------------------"; @@ -37,548 +25,6 @@ : *) -"----------- complete Problem ------------------------------------------------------------------"; -"----------- complete Problem ------------------------------------------------------------------"; -"----------- complete Problem ------------------------------------------------------------------"; -(* copy fromIsac's Java-Frontend: - -Problem ("Biegelinie", ["Biegelinien"]) - Specification: - Model: - Given: "Traegerlaenge L", "Streckenlast q_0" - Where: "q_0 ist_integrierbar_auf {| 0, L |}", "0 < L" - Find: "Biegelinie y" - Relate: "Randbedingungen [ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x y_0 = 0 ]" - References: - RTheory: "Biegelinie" - RProblem: ["Biegelinien"] - RMethod: ["Integrieren", "KonstanteBestimmen2"] - Solution: - Problem ("Biegelinie", ["vonBelastungZu", "Biegelinien"]) - "[Q x = c + -1 * q_0 * x, M_b x = c_2 + c * x + -1 * q_0 / 2 * x ^ 2, y' x = c_3 + 1 / (-1 * EI) * (c_2 * x + c / 2 * x ^ 2 + -1 * q_0 / 6 * x ^ 3), 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)]" - Problem ("Biegelinie", ["setzeRandbedingungen", "Biegelinien"]) - "[L * q_0 = c, 0 = (2 * c_2 + 2 * L * c + -1 * L ^ 2 * q_0) / 2, 0 = c_4, 0 = c_3]" - "solveSystem [L * q_0 = c, 0 = (2 * c_2 + 2 * L * c + -1 * L ^ 2 * q_0) / 2, 0 = c_4, 0 = c_3] [c, c_1, c_2, c_4]" - "[c = -1 * L * q_0 / -1, c_2 = -1 * L ^ 2 * q_0 / 2, c_3 = 0, c_4 = 0]" - "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)" - Tactic Substitute "c_4 + c_3 * x + 1 / (-1 * EI) * (c_2 / 2 * x ^ 2 + c / 6 * x ^ 3 + -1 * q_0 / 24 * x ^ 4)" "[c, c_1, c_2, c_4]" - "y x = 0 + 0 * x + 1 / (-1 * EI) * (-1 * L ^ 2 * q_0 / 2 / 2 * x ^ 2 + -1 * L * q_0 / -1 / 6 * x ^ 3 + -1 * q_0 / 24 * x ^ 4)" - Tactic Rewrite_Set_Inst "[(bdv, x)]" "make_ratpoly_in" "y x" - "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" - Tactic Check_Postcond ["Biegelinien"] -"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" -*) - -"----------- Problem headline ------------------------------------------------------------------"; -"----------- Problem headline ------------------------------------------------------------------"; -"----------- Problem headline ------------------------------------------------------------------"; -val problem_headline_str = - "( \"Biegelinie\" , [\"Biegelinien\"] )"; - -val toks = ParseC_OLD.tokenize problem_headline_str; -case ParseC_OLD.problem_headline toks of - ((((("(", "Biegelinie"), ","), ["Biegelinien"]), ")"), []) - => () | _ => error "TermC.parse problem_headline CHANGED" - - -"----------- Model-items -----------------------------------------------------------------------"; -"----------- Model-items -----------------------------------------------------------------------"; -"----------- Model-items -----------------------------------------------------------------------"; -val given_comma_str = "Given: \"Traegerlaenge L\", \"Streckenlast q_0\""; -val given_str = "Given: \"Traegerlaenge L\"(*,*) \"Streckenlast q_0\""; - -val toks = ParseC_OLD.tokenize given_str; -(* -(*given_comma_str\*)val toks = - [Token (("Given", ({}, {})), (Command, "Given"), Slot), Token ((":", ({}, {})), (Keyword, ":"), Slot), Token (("Traegerlaenge L", ({}, {})), (String, "Traegerlaenge L"), Slot), - Token ((",", ({}, {})), (Keyword, ","), Slot), Token (("Streckenlast q_0", ({}, {})), (String, "Streckenlast q_0"), Slot)] -(*given_str\*)val toks = - [Token (("Given", ({}, {})), (Command, "Given"), Slot), Token ((":", ({}, {})), (Keyword, ":"), Slot), Token (("Traegerlaenge L", ({}, {})), (String, "Traegerlaenge L"), Slot), - Token (("Streckenlast q_0", ({}, {})), (String, "Streckenlast q_0"), Slot)]: -*) -val given_comma = Parse.command_name "Given" -- Parse.$$$ ":" -- Parse.list1 Parse.term; -val given = Parse.command_name "Given" -- Parse.$$$ ":" -- Parse.list1 Parse.term; - -case ParseC_OLD.parse given_comma (ParseC_OLD.tokenize given_comma_str) of - ((("Given", ":"), [_(*""*), _(*""*)]), - []) => () - (* \ ^--------------------------------- is empty: parsing OK*) -| _ => error "TermC.parse given_comma CHANGED"; - -"----------- Parse.list1 DOES expect <,> between elements"; -case ParseC_OLD.parse given (ParseC_OLD.tokenize given_str) of - ((("Given", ":"), [_(*""*)]), - [_(*Token (("Streckenlast q_0", ({}, {})), (String, "Streckenlast q_0"), Slot)*)]) => () - (* \ \ \ \ \ \ \ \ \ \ \ \ ^ is NOT empty: parsing NOT ok*) -| _ => error "TermC.parse given CHANGED"; - - -"----------- Model -----------------------------------------------------------------------------"; -"----------- Model -----------------------------------------------------------------------------"; -"----------- Model -----------------------------------------------------------------------------"; -val model_str = ( - "Model:" ^ - (* \ \ \ \ *) - "Given: \"Traegerlaenge L\", \"Streckenlast q_0\"" ^ - "Where: \"q_0 ist_integrierbar_auf {| 0, L |}\", \"0 < L\"" ^ - "Find: \"Biegelinie y\"" ^ - "Relate: \"Randbedingungen [ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x y_0 = 0 ]\"" - ); -val model_empty_str = ( (*Model before student's input"*) - "Model:" ^ - (* \ \ \ \ *) - "Given: \"Traegerlaenge \", \"Streckenlast \"" ^ - "Where: \"_ ist_integrierbar_auf {| |}\"" ^ - "Find: \"Biegelinie \"" ^ - "Relate: \"Randbedingungen [ ]\"" - ); -val model_str_opt = ( (*Model explicitly referring to RProblem (default), not RMethod*) - "Model ( RProblem ):" ^ - (* \ \ \ \ *) - "Given: \"Traegerlaenge L\", \"Streckenlast q_0\"" ^ - "Where: \"q_0 ist_integrierbar_auf {| 0, L |}\", \"0 < L\"" ^ - "Find: \"Biegelinie y\"" ^ - "Relate: \"Randbedingungen [ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x y_0 = 0 ]\"" - ); - -val toks = ParseC_OLD.tokenize model_str; -case ParseC_OLD.parse ParseC_OLD.model toks of -((((((((((((((( - "Model", (("", ""), "")), ":"), - "Given"), ":"), [_(*""*), _(*""*)]), - "Where"), ":"), [_(*""*), _(*""*)]), - "Find"), ":"), _(*""*)), - "Relate"), ":"), [_(*""*)]), []) -=> () | _ => error "TermC.parse model CHANGED"; - -"----------- Model before student's input"; -val toks = ParseC_OLD.tokenize model_empty_str; -case ParseC_OLD.parse ParseC_OLD.model toks of -((((((((((((((( - "Model", (("", ""), "")), ":"), - "Given"), ":"), [_(*""*), _(*""*)]), - "Where"), ":"), [_(*""*) (*//, _(*""*) //*)]), - "Find"), ":"), _(*""*)), - "Relate"), ":"), [_(*""*)]), []) -=> () | _ => error "TermC.parse model_empty_str CHANGED"; - -"----------- Model explicitly referring to RProblem (default), not RMethod"; -val toks = ParseC_OLD.tokenize model_str_opt; -case ParseC_OLD.parse ParseC_OLD.model toks of -((((((((((((((( - "Model", (("(", "RProblem"), ")")), ":"), - "Given"), ":"), [_(*""*), _(*""*)]), - "Where"), ":"), [_(*""*), _(*""*)]), - "Find"), ":"), _(*""*)), - "Relate"), ":"), [_(*""*)]), []) -=> () | _ => error "TermC.parse model_str_opt CHANGED"; - - -"----------- References ------------------------------------------------------------------------"; -"----------- References ------------------------------------------------------------------------"; -"----------- References ------------------------------------------------------------------------"; -val references_collapsed_str = ( - "References:" - ); -val references_str = ( - "References:" ^ - "RTheory: \"Biegelinie\"" ^ - "RProblem: [\"Biegelinien\"]" ^ - "RMethod: [\"Integrieren\", \"KonstanteBestimmen2\"]" - ); -val references_empty_str = ( - "References:" ^ - "RTheory: \"\"" ^ - "RProblem: [\"\"]" ^ - "RMethod: [\"\"]" - ); - -case ParseC_OLD.parse ParseC_OLD.references (ParseC_OLD.tokenize references_collapsed_str) of - ((("References", ":"), (((((((("", ""), ""), ""), ""), []), ""), ""), [])), []) - => () | _ => error "TermC.parse references_collapsed CHANGED"; - -case ParseC_OLD.parse ParseC_OLD.references (ParseC_OLD.tokenize references_str) of ((( - "References", ":"), - (((((((( - "RTheory", ":"), "Biegelinie"), - "RProblem"), ":"), ["Biegelinien"]), - "RMethod"), ":"), ["Integrieren", "KonstanteBestimmen2"])), - []) - => () | _ => error "TermC.parse references CHANGED"; - -case ParseC_OLD.parse ParseC_OLD.references (ParseC_OLD.tokenize references_empty_str) of ((( - "References", ":"), (((((((( - "RTheory", ":"), ""), - "RProblem"), ":"), [""]), - "RMethod"), ":"), [""])), - []) - => () | _ => error "TermC.parse references_empty_str CHANGED" - - -"----------- Specification: References + Model -------------------------------------------------"; -"----------- Specification: References + Model -------------------------------------------------"; -"----------- Specification: References + Model -------------------------------------------------"; -val specification_str = ( - "Specification:" ^ - model_str ^ - references_str - ); -val specification_collapsed_str = ( -" Specification:" (** ) ^ -" Model:"^ -" Given: \"Traegerlaenge L\", \"Streckenlast q_0\"" ^ -" Where: \"q_0 ist_integrierbar_auf {| 0, L |}\", \"0 < L\"" ^ -" Find: \"Biegelinie y\"" ^ -" Relate: \"Randbedingungen [ Q_0 = q_0 * L, M_b L = 0, y_0 = 0, d_d x y_0 = 0 ]\"" ^ -" References:" (**) ^ -" RTheory: \"Biegelinie\"" (**) ^ -" RProblem: [\"Biegelinien\"]" (**) ^ -" RMethod: [\"Integrieren\", \"KonstanteBestimmen2\"]" ( **) -); - -case ParseC_OLD.specification (ParseC_OLD.tokenize specification_str) of ((( - "Specification", ":"), - ((((((((((((((( - "Model", (("", ""), "")), ":"), - "Given"), ":"), [_(*""*), _(*""*)]), - "Where"), ":"), [_(*""*), _(*""*)]), - "Find"), ":"), _(*""*)), - "Relate"), ":"), [_(*""*)]), - (( - "References", ":"), (((((((( - "RTheory", ":"), "Biegelinie"), - "RProblem"), ":"), ["Biegelinien"]), - "RMethod"), ":"), ["Integrieren", "KonstanteBestimmen2"])))), - []) - => () | _ => error "TermC.parse specification (expanded) changed"; - -"----------- Specification collapsed"; -case ParseC_OLD.parse ParseC_OLD.specification (ParseC_OLD.tokenize specification_collapsed_str) of ((( - "Specification", ":"), -(*model*)((((((((((((((("", (("", ""), "")), ""), ""), ""), []), ""), ""), []), ""), ""), ""), ""), ""), []), (("", ""), -(*refs?*)(((((((("", ""), ""), ""), ""), []), ""), ""), [])))), - []) - => () | _ => error "TermC.parse specification (collapsed) changed"; - - -"----------- Tactics ---------------------------------------------------------------------------"; -"----------- Tactics ---------------------------------------------------------------------------"; -"----------- Tactics ---------------------------------------------------------------------------"; -val tactic_Substitute_str = - "Tactic Substitute \"c_4 + c_3 * x + 1 / (-1 * EI)\" \"[c, c_1, c_2, c_4]\""; -val tactic_Rewrite_Set_Inst_str = - "Tactic Rewrite_Set_Inst \"[(bdv, x)]\" \"make_ratpoly_in\""; -val tactic_Check_Postcond_str = - "Tactic Check_Postcond [\"Biegelinien\", \"xxx\"]"; -val final_result_str = "\"y x = -6 * q_0 * L ^ 2 / (-24 * EI)\""; - -val toks1 = ParseC_OLD.tokenize "Substitute \"c_4 + c_3 * x + 1 / (-1 * EI)\" \"[c, c_1, c_2, c_4]\""; -case ParseC_OLD.substitute toks1 of ((("Substitute", _(**)), _(**)), []) -=> () | _ => error "TermC.parse Substitute CHANGED"; - -val toks2 = ParseC_OLD.tokenize "Rewrite_Set_Inst \"[(bdv, x)]\" \"make_ratpoly_in\""; -case ParseC_OLD.rewrite_set_inst toks2 of - ((("Rewrite_Set_Inst", _(**)), "make_ratpoly_in"), []) -=> () | _ => error "TermC.parse Rewrite_Set_Inst CHANGED"; - -val toks3 = ParseC_OLD.tokenize "Check_Postcond [\"Biegelinien\", \"xxx\"]"; -case ParseC_OLD.check_postcond toks3 of (("Check_Postcond", ["Biegelinien", "xxx"]), []) -=> () | _ => error "TermC.parse Check_Postcond CHANGED"; - -"----------- Tactics collected"; -val toks1' = ParseC_OLD.tokenize tactic_Substitute_str; -val toks2' = ParseC_OLD.tokenize tactic_Rewrite_Set_Inst_str; -val toks3' = ParseC_OLD.tokenize tactic_Check_Postcond_str; - -ParseC_OLD.parse ParseC_OLD.tactic toks1'; (* = (("Tactic", "EXEC IMMEDIATELY: Substitute "), [])*) -ParseC_OLD.parse ParseC_OLD.tactic toks2'; (* = (("Tactic", "EXEC IMMEDIATELY: Rewrite_Set_Inst make_ratpoly_in"), [])*) -ParseC_OLD.parse ParseC_OLD.tactic toks3'; (* = (("Tactic", "EXEC IMMEDIATELY: Check_Postcond xxxBiegelinien"), [])*) - -case ParseC_OLD.parse ParseC_OLD.tactic (ParseC_OLD.tokenize tactic_Substitute_str) of - (("Tactic", _(*"EXEC IMMEDIATELY: Substitute "*)), []) -=> () | _ => error "TermC.parse Tactic Substitute CHANGED"; - - -"----------- steps -----------------------------------------------------------------------------"; -"----------- steps -----------------------------------------------------------------------------"; -"----------- steps -----------------------------------------------------------------------------"; -val steps_1_str = "\"[c = -1 * L * q_0 / -1, c_2 = -1 * L ^ 2 * q_0 / 2, c_3 = 0, c_4 = 0]\""; -val steps_term_tac_str = ( - final_result_str ^ - " Tactic Check_Postcond [\"Biegelinien\"]" - ); -val steps_nonrec_str = ( - "\"[c = -1 * L * q_0 / -1, c_2 = -1 * L ^ 2 * q_0 / 2, c_3 = 0, c_4 = 0]\"" (**) ^ - "\"y x = c_4 + c_3 * x + 1 / (-1 * EI)\"" (**) ^ - tactic_Substitute_str ^ - "\"y x = 0 + 0 * x + 1 / (-1 * EI)\"" (**) ^ - tactic_Rewrite_Set_Inst_str ^ - final_result_str (**) ^ - tactic_Check_Postcond_str ^ - final_result_str (**) -); - -val toks1 = ParseC_OLD.tokenize steps_1_str; -val toks2 = ParseC_OLD.tokenize steps_term_tac_str; -val toks3 = ParseC_OLD.tokenize steps_nonrec_str; - -"----------- simple version"; -ParseC_OLD.parse ParseC_OLD.steps []; (* = ([], []): (string * (string * string)) list * Token.T list *) -ParseC_OLD.parse ParseC_OLD.steps toks1; (* = ([("", ("", ""))], [])*) -ParseC_OLD.parse ParseC_OLD.steps toks2; (* = ([("", ("Tactic", "EXEC IMMEDIATELY: Check_Postcond Biegelinien"))], [])*) -ParseC_OLD.parse ParseC_OLD.steps toks3; - -case ParseC_OLD.parse ParseC_OLD.steps toks3 of - ([(_(*""*), ("", "")), - (_(*""*), ("Tactic", _(*"EXEC IMMEDIATELY: Substitute "*))), - (_(*""*), ("Tactic", _(*"EXEC IMMEDIATELY: Rewrite_Set_Inst make_ratpoly_in"*))), - (_(*""*), ("Tactic", _(*"EXEC IMMEDIATELY: Check_Postcond Biegelinien"*))), - (_(*""*), ("", ""))], - []) -=> () | _ => error "TermC.parse steps, simple version, CHANGED"; - -"----------- version preparing subproblems"; -case ParseC_OLD.parse ParseC_OLD.steps_subpbl toks3 of - ([_(*"EXEC IMMEDIATELY step_term: (, )"*), - _(*"EXEC IMMEDIATELY step_term: (Tactic, EXEC IMMEDIATELY: Substitute )"*), - _(*"EXEC IMMEDIATELY step_term: (Tactic, EXEC IMMEDIATELY: Rewrite_Set_Inst make_ratpoly_in)"*), - _(*"EXEC IMMEDIATELY step_term: (Tactic, EXEC IMMEDIATELY: Check_Postcond xxxBiegelinien)"*), - _(*"EXEC IMMEDIATELY step_term: (, )"*)], - []) -=> () | _ => error "TermC.parse steps, with exec_step_term, CHANGED"; - - -"----------- body ------------------------------------------------------------------------------"; -"----------- body ------------------------------------------------------------------------------"; -"----------- body ------------------------------------------------------------------------------"; -val solution_str = ( - "Solution:" ^ - steps_nonrec_str - ); -val body_str = specification_str ^ solution_str; - -case ParseC_OLD.parse ParseC_OLD.body (ParseC_OLD.tokenize body_str) of (((((( - "Specification", ":"), ((((((((((((((( - "Model", (("", ""), "")), ":"), - "Given"), ":"), [_(*""*), _(*""*)]), - "Where"), ":"), [_(*""*), _(*""*)]), - "Find"), ":"), _(*""*)), - "Relate"), ":"), [_(*""*)]), (( - "References", ":"), (((((((( - "RTheory", ":"), "Biegelinie"), - "RProblem"), ":"), ["Biegelinien"]), - "RMethod"), ":"), ["Integrieren", "KonstanteBestimmen2"])))), - "Solution"), ":"), - [_(*"EXEC IMMEDIATELY step_term: (, )"*), - _(*"EXEC IMMEDIATELY step_term: (Tactic, EXEC IMMEDIATELY: Substitute )"*), - _(*"EXEC IMMEDIATELY step_term: (Tactic, EXEC IMMEDIATELY: Rewrite_Set_Inst make_ratpoly_in)"*), - _(*"EXEC IMMEDIATELY step_term: (Tactic, EXEC IMMEDIATELY: Check_Postcond xxxBiegelinien)"*), - _(*"EXEC IMMEDIATELY step_term: (, )"*)]), - []) -=> () | _ => error "TermC.parse body CHANGED"; - - -"----------- Problem ---------------------------------------------------------------------------"; -"----------- Problem ---------------------------------------------------------------------------"; -"----------- Problem ---------------------------------------------------------------------------"; -"----------- whole Problem"; -val toks = ParseC_OLD.tokenize (problem_headline_str ^ specification_str ^ solution_str); - -case ParseC_OLD.parse ParseC_OLD.problem toks of ((((((( - "(", "Biegelinie"), ","), ["Biegelinien"]), ")"), ((((( - "Specification", ":"), ((((((((((((((( - "Model", (("", ""), "")), ":"), - "Given"), ":"), [_(*""*), _(*""*)]), - "Where"), ":"), [_(*""*), _(*""*)]), - "Find"), ":"), _(*""*)), - "Relate"), ":"), [_(*""*)]), (( - "References", ":"), (((((((( - "RTheory", ":"), "Biegelinie"), - "RProblem"), ":"), ["Biegelinien"]), - "RMethod"), ":"), ["Integrieren", "KonstanteBestimmen2"])))), - "Solution"), ":"), - [_(*"EXEC IMMEDIATELY step_term: (, )"*), - _(*"EXEC IMMEDIATELY step_term: (Tactic, EXEC IMMEDIATELY: Substitute )"*), - _(*"EXEC IMMEDIATELY step_term: (Tactic, EXEC IMMEDIATELY: Rewrite_Set_Inst make_ratpoly_in)"*), - _(*"EXEC IMMEDIATELY step_term: (Tactic, EXEC IMMEDIATELY: Check_Postcond xxxBiegelinien)"*), - _(*"EXEC IMMEDIATELY step_term: (, )"*)])), - ""), -[]) - => () | _ => error "TermC.parse problem (whole) CHANGED" - -"----------- enter Specification"; -val toks = ParseC_OLD.tokenize ( - problem_headline_str ^ - "Specification:" ^ - model_empty_str ^ (* <<<----- empty *) - "References:" ^ (* <<<----- collapsed *) - "Solution:" - ); -case ParseC_OLD.parse ParseC_OLD.problem toks of ((((((( - "(", "Biegelinie"), ","), ["Biegelinien"]), ")"), ((((( - "Specification", ":"), ((((((((((((((( - "Model", (("", ""), "")), ":"), - "Given"), ":"), [_(*""*), _(*""*)]), - "Where"), ":"), [_(*""*)]), - "Find"), ":"), _(*""*)), - "Relate"), ":"), [_(*""*)]), (( - "References", ":"), (((((((("", ""), ""), ""), ""), []), ""), ""), [])))), - "Solution"), ":"), [])), - ""), -[]) -=> () | _ => error "TermC.parse enter Specification CHANGED" - -"----------- Problem-headline only"; -val toks = ParseC_OLD.tokenize problem_headline_str; - -case ParseC_OLD.parse ParseC_OLD.problem toks of ((((((( - "(", "Biegelinie"), ","), ["Biegelinien"]), ")"), ((((( - "", ""), ((((((((((((((( - "", (("", ""), "")), ""), - ""), ""), []), - ""), ""), []), - ""), ""), ""), - ""), ""), []), (( - "", ""), (((((((("", ""), ""), ""), ""), []), ""), ""), [])))), - ""), ""), [])), - ""), -[]) -=> () | _ => error "TermC.parse BEFORE enter Specification CHANGED" - -"----------- finish Specification"; -val toks = ParseC_OLD.tokenize ( - problem_headline_str ^ - "Specification:" ^ - model_str ^ - references_str ^ - "Solution:" - ); -case ParseC_OLD.parse ParseC_OLD.problem toks of ( (((((( - "(", "Biegelinie"), ","), ["Biegelinien"]), ")"), ((((( - "Specification", ":"), ((((((((((((((( - "Model", (("", ""), "")), ":"), - "Given"), ":"), [_(*""*), _(*""*)]), - "Where"), ":"), [_(*""*), _(*""*)]), - "Find"), ":"), _(*""*)), - "Relate"), ":"), [_(*""*)]), (( - "References", ":"), (((((((( - "RTheory", ":"), "Biegelinie"), - "RProblem"), ":"), ["Biegelinien"]), - "RMethod"), ":"), ["Integrieren", "KonstanteBestimmen2"])))), - "Solution"), ":"), - [])), - ""), -[]) -=> () | _ => error "TermC.parse finish specification CHANGED" - -"----------- Specification collapsed"; -case ParseC_OLD.parse ParseC_OLD.problem (ParseC_OLD.tokenize problem_headline_str) of ((((((( - "(", "Biegelinie"), ","), ["Biegelinien"]), ")"), ((((( - (*Specification*)"", ""), ((((((((((((((( - (*Model*)"", (("", ""), "")), ""), ""), ""), []), ""), ""), []), ""), ""), ""), ""), ""), []), (("", ""), (((((((( - (*References*)"", ""), ""), ""), ""), []), ""), ""), [])))), - (*Solution*)""), ""), - [])), - ""), -[]) -=> () | _ => error "TermC.parse Specification collapsed CHANGED" - -"----------- Problem with final_result, all collapsed"; -val toks = ParseC_OLD.tokenize (problem_headline_str ^ final_result_str); -case ParseC_OLD.parse ParseC_OLD.problem toks of ((((((( - "(", "Biegelinie"), ","), ["Biegelinien"]), ")"), ((((( - (*Specification*)"", ""), ((((((((((((((( - (*Model*)"", (("", ""), "")), ""), ""), ""), []), ""), ""), []), ""), ""), ""), ""), ""), []), (("", ""), (((((((( - (*References*)"", ""), ""), ""), ""), []), ""), ""), [])))), - (*Solution*)""), ""), - [])), - _(*""*)), -[]) -=> () | _ => error "TermC.parse Problem with final_result, all collapsed CHANGED" - - -"----------- fun read_out_problem --------------------------------------------------------------"; -"----------- fun read_out_problem --------------------------------------------------------------"; -"----------- fun read_out_problem --------------------------------------------------------------"; -val toks = ParseC_OLD.tokenize ( - problem_headline_str ^ - "Specification:" ^ - model_str ^ - references_str ^ - "Solution:" - ); -case ParseC_OLD.parse ParseC_OLD.problem toks |> fst |> ParseC_OLD.read_out_problem of - {thy_id = "Biegelinie", pbl_id = ["Biegelinien"], - givens = [_(*""*), _(*""*)], wheres = [_(*""*), _(*""*)], - find = _(*""*), relates = [_(*""*)], - rthy_id = "Biegelinie", rpbl_id = ["Biegelinien"], rmet_id = ["Integrieren", "KonstanteBestimmen2"] - } => () -| _ => error "read_out_problem CHANGED" - - -"----------- THERE ARE TESTS with INCOMPLETE WORK IN Test_Parse_Isac.thy -----------------------"; -"----------- THERE ARE TESTS with INCOMPLETE WORK IN Test_Parse_Isac.thy -----------------------"; -"----------- THERE ARE TESTS with INCOMPLETE WORK IN Test_Parse_Isac.thy -----------------------"; -(*TODO after Problem became recursive*) - -"----------- parser for exp_file.str -----------------------------------------------------------"; -"----------- parser for exp_file.str -----------------------------------------------------------"; -"----------- parser for exp_file.str -----------------------------------------------------------"; -(* - For keyword Example SPARK's lexer and parser are used. Respective Isac code was developed - alongside existing SPARK code, not by tests. Here are tests for code using Isabelle technologies - and preceeding the actual production code. -*) -val form_single = - Parse.$$$ "(" -- - (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]") (* Formalise.model *) -- - Parse.$$$ "," -- - Parse.$$$ "(" (* begin Formalise.spec *) -- - Parse.string -- (* ThyC.id, still not qualified *) - Parse.$$$ "," -- - (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]") (* Problem.id *) -- - Parse.$$$ "," -- - (Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]") (* MethodC.id *) -- - Parse.$$$ ")" (* end Formalise.spec *) -- - Parse.$$$ ")"; - -val form_single_str = ( - "( " ^ - " [\"Traegerlaenge L\", \"Streckenlast q_0\", \"Biegelinie y\", " ^ - " \"Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]\", " ^ - " \"FunktionsVariable x\", \"GleichungsVariablen [c, c_2, c_3, c_4]\", " ^ - " \"AbleitungBiegelinie dy\"], " ^ - " (\"Biegelinie\", [\"Biegelinien\"], [\"IntegrierenUndKonstanteBestimmen2\"])" ^ - ")"); - -val toks = ParseC_OLD.tokenize form_single_str; -case ParseC_OLD.parse form_single toks of ((((((((((( - "(", - ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y", - "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x", - "GleichungsVariablen [c, c_2, c_3, c_4]", "AbleitungBiegelinie dy"]), - ","), - "("), "Biegelinie"), ","), ["Biegelinien"]), ","), ["IntegrierenUndKonstanteBestimmen2"]), ")"), - ")"), -[]) -=> () | _ => error "TermC.parse form_single toks CHANGED"; - -(* Isac always takes a singleton here *) -val formalise = (Parse.$$$ "[" |-- Parse.list1 form_single --| Parse.$$$ "]"); -type formalise = - ((((((((((string * string list) * string) * string) * string) * string) * string list) * - string) * string list) * string) * string) list; -formalise: formalise parser; - -val toks = ParseC_OLD.tokenize ("[" ^ form_single_str ^ "]"); -case ParseC_OLD.parse formalise (ParseC_OLD.tokenize ("[" ^ form_single_str ^ "]")) of ([(((((((((( - "(", - ["Traegerlaenge L", "Streckenlast q_0", "Biegelinie y", - "Randbedingungen [y 0 = (0::real), y L = 0, M_b 0 = 0, M_b L = 0]", "FunktionsVariable x", - "GleichungsVariablen [c, c_2, c_3, c_4]", "AbleitungBiegelinie dy"]), - ","), - "("), "Biegelinie"), ","), ["Biegelinien"]), ","), ["IntegrierenUndKonstanteBestimmen2"]), ")"), - ")")], -[]) -=> () | _ => error "TermC.parse formalise CHANGED"; - +"----------- TODO ------------------------------------------------------------------------------"; +"----------- TODO ------------------------------------------------------------------------------"; +"----------- TODO ------------------------------------------------------------------------------"; diff -r d5c670beaba4 -r 5038589d3033 test/Tools/isac/BridgeJEdit/preliminary.sml --- a/test/Tools/isac/BridgeJEdit/preliminary.sml Tue Aug 23 18:05:08 2022 +0200 +++ b/test/Tools/isac/BridgeJEdit/preliminary.sml Wed Aug 24 12:37:07 2022 +0200 @@ -14,14 +14,22 @@ "----------- investigate Pure/context.ML THEORY_DATA -------------------------------------------"; "----------- investigate Pure/context.ML THEORY_DATA -------------------------------------------"; "----------- investigate Pure/context.ML THEORY_DATA -------------------------------------------"; -(* Pure/context.ML +(* Pure/context.ML * ) signature THEORY_DATA = sig type T val get: theory -> T val put: T -> theory -> theory val map: (T -> T) -> theory -> theory -end;*) +end; +( **) +structure Refs_Data = Theory_Data (*code for keyword ExampleSPARK*) +( + type T = References.T + val empty : T = References.empty + val extend = I + fun merge (_, refs) = refs +); (* Refs_Data.empty; (*in Refs_Data defined workers are hidden*) Refs_Data.extend; (*in Refs_Data defined workers are hidden*)