1.1 --- a/src/HOL/SPARK/Tools/fdl_lexer.ML	Mon Mar 08 10:04:37 2021 +0100
     1.2 +++ b/src/HOL/SPARK/Tools/fdl_lexer.ML	Fri Mar 12 12:48:55 2021 +0100
     1.3 @@ -7,12 +7,12 @@
     1.4  
     1.5  signature FDL_LEXER =
     1.6  sig
     1.7 -  type T
     1.8 +  datatype kind = Keyword | Ident | Long_Ident | Traceability | Number | Comment | EOF
     1.9 +  datatype T = Token of kind * string * Position.T;
    1.10    type chars
    1.11    type banner
    1.12    type date
    1.13    type time
    1.14 -  datatype kind = Keyword | Ident | Long_Ident | Traceability | Number | Comment | EOF
    1.15    val tokenize: (chars -> 'a * chars) -> (chars -> T * chars) ->
    1.16      Position.T -> string -> 'a * T list
    1.17    val position_of: T -> Position.T
    1.18 @@ -24,15 +24,35 @@
    1.19    val unparse: T -> string
    1.20    val is_proper: T -> bool
    1.21    val is_digit: string -> bool
    1.22 +  val is_char_eof: string * 'a -> bool
    1.23    val c_comment: chars -> T * chars
    1.24    val curly_comment: chars -> T * chars
    1.25    val percent_comment: chars -> T * chars
    1.26    val vcg_header: chars -> (banner * (date * time) option) * chars
    1.27    val siv_header: chars ->
    1.28 -    (banner * (date * time) * (date * time) * (string * string)) * chars
    1.29 +    (banner * (date * time) * (date * time) * (string * string)) * chars (*.. NOT [], but ..
    1.30 +    (^^^^^^^^^^^^^^^ header ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^)   ^^^^^ ..trailing line=13..117 *)
    1.31 +  val explode_pos: string -> Position.T -> chars
    1.32 +  val leq_token: T * T -> bool
    1.33 +  val lexicon: Scan.lexicon
    1.34 +  val identifier: chars -> chars * chars
    1.35 +  val long_identifier: chars -> chars * chars
    1.36 +  val banner: chars -> (string * string * string) * chars
    1.37 +  val date: chars -> (string * string * string) * chars;
    1.38 +  val whitespace: chars -> chars * chars
    1.39 +  val whitespace1: chars -> chars * chars
    1.40 +  val keyword: string -> chars -> chars * chars
    1.41 +  val number: chars -> chars * chars
    1.42 +  val any: chars -> (string * Position.T) * chars
    1.43 +  val any_line: chars -> string * chars;
    1.44 +  val !!! : string -> (chars -> 'a) -> chars -> 'a
    1.45 +  val $$$ : string -> chars -> chars * chars
    1.46 +  val scan: (chars -> 'a * chars) -> (chars -> T * chars) -> chars -> ('a * T list) * chars;
    1.47 +  val char_stopper: (string * Position.T) Scan.stopper
    1.48 +  val make_token: kind -> chars -> T
    1.49  end;
    1.50  
    1.51 -structure Fdl_Lexer: FDL_LEXER =
    1.52 +structure Fdl_Lexer(**): FDL_LEXER(**) =
    1.53  struct
    1.54  
    1.55  (** tokens **)
    1.56 @@ -40,6 +60,7 @@
    1.57  datatype kind = Keyword | Ident | Long_Ident | Traceability | Number | Comment | EOF;
    1.58  
    1.59  datatype T = Token of kind * string * Position.T;
    1.60 +(*for Formalise.T     ^^^^ NOT required?*)
    1.61  
    1.62  fun make_token k xs = Token (k, implode (map fst xs),
    1.63    case xs of [] => Position.none | (_, p) :: _ => p);
    1.64 @@ -81,6 +102,7 @@
    1.65  
    1.66  fun symbol (x : string, _ : Position.T) = x;
    1.67  
    1.68 +(* convert string s to chars ("", pos) *)
    1.69  fun explode_pos s pos = fst (fold_map (fn x => fn pos =>
    1.70    ((x, pos), Position.advance x pos)) (raw_explode s) pos);
    1.71  
    1.72 @@ -209,6 +231,14 @@
    1.73    (Scan.repeat (Scan.unless ($$$ b) any) --| $$$ b) >> make_token Comment;
    1.74  
    1.75  val c_comment = gen_comment "/*" "*/";
    1.76 +fun c_comment chars = 
    1.77 +  let
    1.78 +(** )val _ = @{print} {a = "//--- ###I Fdl_Lexer.c_comment called with", 
    1.79 +      b_lenght_chars = length chars, chars = chars};( **)
    1.80 +    val xxx as (redex, toks) = (gen_comment "/*" "*/") chars
    1.81 +(** )val _ = @{print} {z = "\\--- ###I Fdl_Lexer.c_comment \<rightarrow>",
    1.82 +      b_lenght_chars = length toks, res = xxx};( **)
    1.83 +  in xxx end;
    1.84  val curly_comment = gen_comment "{" "}";
    1.85  
    1.86  val percent_comment = $$$ "%" |-- any_line' >> make_token Comment;
    1.87 @@ -240,6 +270,7 @@
    1.88  val banner = 
    1.89    whitespace' |-- asterisks --| whitespace' --| newline :|-- (fn xs =>
    1.90      (any_line -- any_line -- any_line >>
    1.91 +(*WN:^^^^^^^^    ^^^^^^^^    ^^^^^^^^   3 lines ending with \n *)
    1.92         (fn ((l1, l2), l3) => (l1, l2, l3))) --|
    1.93      whitespace' --| prfx (map symbol xs) --| whitespace' --| newline);
    1.94  
    1.95 @@ -254,6 +285,23 @@
    1.96    newline --| newline -- (any_line -- any_line) >>
    1.97      (fn (((b, c), s), ls) => (b, c, s, ls));
    1.98  
    1.99 +(*WN: print ---vvvvv*)
   1.100 +fun siv_header chars =
   1.101 +  let
   1.102 +(** )val _ = @{print} {a = "//--- ###I Fdl_Lexer.siv_header called with", 
   1.103 +      b_lenght_chars = length chars, chars = chars};( **)
   1.104 +    val xxx as (redex, toks) = 
   1.105 +      (
   1.106 +        banner --| whitespace --
   1.107 +        ($$$ "CREATED" |-- whitespace |-- (date --| $$$ "," --| whitespace -- time)) --|
   1.108 +        whitespace --
   1.109 +        ($$$ "SIMPLIFIED" |-- whitespace |-- (date --| $$$ "," --| whitespace -- time)) --|
   1.110 +        newline --| newline -- (any_line -- any_line) >>
   1.111 +          (fn (((b, c), s), ls) => (b, c, s, ls))
   1.112 +      ) chars;
   1.113 +(** )val _ = @{print} {z = "\\--- ###I Fdl_Lexer.siv_header \<rightarrow>",
   1.114 +      b_lenght_chars = length toks, res = xxx};( **)
   1.115 +  in xxx end;
   1.116  
   1.117  (** the main tokenizer **)
   1.118  
   1.119 @@ -270,10 +318,45 @@
   1.120               (   long_identifier >> make_token Long_Ident
   1.121                || identifier >> make_token Ident)
   1.122          || number >> make_token Number) --|
   1.123 -     whitespace));
   1.124 +     whitespace) );
   1.125 +fun scan header comment chars =
   1.126 +  let
   1.127 +    (** )val _ = @{print} {a = "//--- ###I Fdl_Lexer.scan called with", 
   1.128 +      b_lenght_chars = length chars, chars = chars};( **)
   1.129 +    val xxx as (redex, toks) = 
   1.130 +      (!!! "bad header" header --| whitespace --
   1.131 +      Scan.repeat (Scan.unless (Scan.one is_char_eof)
   1.132 +        (!!! "bad input"
   1.133 +           (   comment
   1.134 +            || (keyword "For" -- whitespace1) |--
   1.135 +                  Scan.repeat1 (Scan.unless (keyword ":") any) --|
   1.136 +                  keyword ":" >> make_token Traceability             
   1.137 +            || Scan.max leq_token
   1.138 +                 (Scan.literal lexicon >> make_token Keyword)
   1.139 +                 (   long_identifier >> make_token Long_Ident
   1.140 +                  || identifier >> make_token Ident)
   1.141 +            || number >> make_token Number) --|
   1.142 +         whitespace))) chars
   1.143 +    (** )val _ = @{print} {z = "\\--- ###I Fdl_Lexer.scan \<rightarrow>",
   1.144 +      b_lenght_chars = length toks, res = xxx};( **)
   1.145 +  in xxx end;
   1.146  
   1.147  fun tokenize header comment pos s =
   1.148    fst (Scan.finite char_stopper
   1.149      (Scan.error (scan header comment)) (explode_pos s pos));
   1.150  
   1.151 +fun tokenize header(*= Fdl_Lexer.siv_header*) comment pos s =
   1.152 +((** )@{print} {a = "//--- ###I Fdl_Lexer.tokenize called with", header = header,
   1.153 +    comment = comment, pos = pos, s = s};( **)
   1.154 +  let
   1.155 +(** )val _ = @{print} {a = "###I Fdl_Lexer.tokenize: explode_pos", res = explode_pos s pos};( **)
   1.156 +(*convert string s to chars ("", pos) is ---vvvvvvvvvvv                  ^^^^^^^^^^^*)
   1.157 +    val xxx as (redex, toks) =
   1.158 +      fst (Scan.finite char_stopper
   1.159 +        (Scan.error (scan header comment)) (explode_pos s pos))
   1.160 +(** )val _ = @{print} {a = "\\--- ###I Fdl_Lexer.tokenize \<rightarrow>",
   1.161 +      b_lenght_chars = length toks, res = xxx};( **)
   1.162 +  in xxx end
   1.163 +);
   1.164 +
   1.165  end;

     2.1 --- a/src/HOL/SPARK/Tools/fdl_parser.ML	Mon Mar 08 10:04:37 2021 +0100
     2.2 +++ b/src/HOL/SPARK/Tools/fdl_parser.ML	Fri Mar 12 12:48:55 2021 +0100
     2.3 @@ -32,9 +32,11 @@
     2.4    type rules =
     2.5      ((string * int) * fdl_rule) list *
     2.6      (string * (expr * (string * string) list) list) list;
     2.7 +  val empty_rules: rules
     2.8  
     2.9    type vcs = (string * (string *
    2.10      ((string * expr) list * (string * expr) list)) list) list;
    2.11 +  val empty_vcs: (string * string) * vcs
    2.12  
    2.13    type 'a tab = 'a Symtab.table * (string * 'a) list;
    2.14  
    2.15 @@ -47,6 +49,7 @@
    2.16       vars: string tab,
    2.17       consts: string tab,
    2.18       funs: (string list * string) tab};
    2.19 +  val empty_decls: decls
    2.20  
    2.21    val parse_vcs: (Fdl_Lexer.chars -> 'a * Fdl_Lexer.chars) -> Position.T ->
    2.22      string -> 'a * ((string * string) * vcs);
    2.23 @@ -54,9 +57,19 @@
    2.24    val parse_declarations:  Position.T -> string -> (string * string) * decls;
    2.25  
    2.26    val parse_rules: Position.T -> string -> rules;
    2.27 +  val vcs: Fdl_Lexer.T list ->
    2.28 +    ((string * string) * (string * (string * ((string * expr) list * (string * expr) list)) list) list) * Fdl_Lexer.T list;
    2.29 +  val !!! : (Fdl_Lexer.T list -> 'a) -> Fdl_Lexer.T list -> 'a;
    2.30 +  val $$$ : string -> Fdl_Lexer.T list -> string * Fdl_Lexer.T list
    2.31 +  val group: string -> ('a -> 'b) -> 'a -> 'b
    2.32 +  val identifier: Fdl_Lexer.T list -> string * Fdl_Lexer.T list
    2.33 +  val enum1: string -> (Fdl_Lexer.T list -> 'a * Fdl_Lexer.T list) -> Fdl_Lexer.T list ->
    2.34 +    'a list * Fdl_Lexer.T list
    2.35 +  val list1: (Fdl_Lexer.T list -> 'a * Fdl_Lexer.T list) -> Fdl_Lexer.T list ->
    2.36 +    'a list * Fdl_Lexer.T list
    2.37  end;
    2.38  
    2.39 -structure Fdl_Parser: FDL_PARSER =
    2.40 +structure Fdl_Parser(**): FDL_PARSER(**) =
    2.41  struct
    2.42  
    2.43  (** error handling **)
    2.44 @@ -247,13 +260,26 @@
    2.45  val vcs =
    2.46    subprogram_kind -- (long_identifier || identifier) --
    2.47    parse_all (traceability -- !!! (Scan.repeat1 vc));
    2.48 +val empty_vcs = (("e_procedure", "e_G_C_D"), []: vcs)
    2.49  
    2.50  fun parse_vcs header pos s =
    2.51 -  s |>
    2.52 -  Fdl_Lexer.tokenize header Fdl_Lexer.c_comment pos ||>
    2.53 -  filter Fdl_Lexer.is_proper ||>
    2.54 -  Scan.finite Fdl_Lexer.stopper (Scan.error (!!! vcs)) ||>
    2.55 -  fst;
    2.56 +(*line_1*)s |>
    2.57 +(*line_2*)Fdl_Lexer.tokenize header Fdl_Lexer.c_comment pos ||>
    2.58 +(*line_3*)filter Fdl_Lexer.is_proper ||>
    2.59 +(*line_4*)Scan.finite Fdl_Lexer.stopper (Scan.error (!!! vcs)) ||>
    2.60 +(*line_5*)fst;
    2.61 +(*            vvvvvv-------- = Fdl_Lexer.siv_header*)
    2.62 +fun parse_vcs header pos s =
    2.63 +((** )@{print} {a = "//--- ###I Fdl_Parser.parse_vcs", header = header, pos = pos, s = s};( **)
    2.64 +  let
    2.65 +    val line_2 = Fdl_Lexer.tokenize header Fdl_Lexer.c_comment pos s
    2.66 +(** )val _ = @{print} {a = "###I Fdl_Parser.parse_vcs: ", line_2 = line_2};( **)
    2.67 +    val line_3 = apsnd (filter Fdl_Lexer.is_proper) line_2
    2.68 +    val line_4 = apsnd (Scan.finite Fdl_Lexer.stopper (Scan.error (!!! vcs))) line_3
    2.69 +    val line_5 = apsnd fst line_4
    2.70 +(** )val _ = @{print} {z = "\\--- ###I Fdl_Parser.parse_vcs \<rightarrow>", res = line_5};( **)
    2.71 +  in line_5 end
    2.72 +);
    2.73  
    2.74  
    2.75  (* fdl declarations, see section 4.3 of SPARK Proof Manual *)
    2.76 @@ -347,6 +373,9 @@
    2.77  type rules =
    2.78    ((string * int) * fdl_rule) list *
    2.79    (string * (expr * (string * string) list) list) list;
    2.80 +val empty_rules =
    2.81 +  ([]: ((string * int) * fdl_rule) list,
    2.82 +   []: (string * (expr * (string * string) list) list) list);
    2.83  
    2.84  val condition_list = $$$ "[" |-- list expression --| $$$ "]";
    2.85  val if_condition_list = $$$ "if" |-- !!! condition_list;

     3.1 --- a/src/Pure/General/position.ML	Mon Mar 08 10:04:37 2021 +0100
     3.2 +++ b/src/Pure/General/position.ML	Fri Mar 12 12:48:55 2021 +0100
     3.3 @@ -10,6 +10,7 @@
     3.4    val ord: T ord
     3.5    val make: Thread_Position.T -> T
     3.6    val dest: T -> Thread_Position.T
     3.7 +  val to_string: T -> string (*WN*)
     3.8    val line_of: T -> int option
     3.9    val offset_of: T -> int option
    3.10    val end_offset_of: T -> int option
    3.11 @@ -95,6 +96,9 @@
    3.12  fun make {line = i, offset = j, end_offset = k, props} = Pos ((i, j, k), norm_props props);
    3.13  fun dest (Pos ((i, j, k), props)) = {line = i, offset = j, end_offset = k, props = props};
    3.14  
    3.15 +(*WN*)fun to_string (Pos ((line, offset, end_offset), _)) = ("Pos ((" ^
    3.16 +  string_of_int line ^ ", " ^ string_of_int offset ^ ", " ^ string_of_int end_offset ^ "), [_])")
    3.17 +
    3.18  fun valid (i: int) = i > 0;
    3.19  fun if_valid i i' = if valid i then i' else i;
    3.20  

     4.1 --- a/src/Pure/Isar/token.ML	Mon Mar 08 10:04:37 2021 +0100
     4.2 +++ b/src/Pure/Isar/token.ML	Fri Mar 12 12:48:55 2021 +0100
     4.3 @@ -30,6 +30,7 @@
     4.4      Declaration of declaration |
     4.5      Files of file Exn.result list
     4.6    val pos_of: T -> Position.T
     4.7 +  val end_pos_of: T -> Position.T (*WN*)
     4.8    val adjust_offsets: (int -> int option) -> T -> T
     4.9    val eof: T
    4.10    val is_eof: T -> bool
    4.11 @@ -64,6 +65,7 @@
    4.12    val reports: Keyword.keywords -> T -> Position.report_text list
    4.13    val markups: Keyword.keywords -> T -> Markup.T list
    4.14    val unparse: T -> string
    4.15 +  val s_to_string: T list -> string
    4.16    val print: T -> string
    4.17    val text_of: T -> string * string
    4.18    val file_source: file -> Input.source
    4.19 @@ -357,6 +359,15 @@
    4.20    | EOF => ""
    4.21    | _ => x);
    4.22  
    4.23 +(*WN-------------------------------------------------------------------------------------------\\*)
    4.24 +fun to_string tok = ("\nToken ((" ^
    4.25 +  Position.to_string (pos_of tok) ^ ", " ^ 
    4.26 +  Position.to_string (end_pos_of tok) ^ "), " ^
    4.27 +  unparse tok ^ ", _)")
    4.28 +
    4.29 +fun s_to_string toks = fold (curry op ^) (map to_string toks |> rev |> separate ", ") "";
    4.30 +(*WN-------------------------------------------------------------------------------------------//*)
    4.31 +
    4.32  fun print tok = Markup.markups (markups Keyword.empty_keywords tok) (unparse tok);
    4.33  
    4.34  fun text_of tok =
    4.35 @@ -770,7 +781,10 @@
    4.36    in
    4.37      (case Scan.error (Scan.finite' stopper (Scan.option scan)) (context, args1) of
    4.38        (SOME x, (context', [])) =>
    4.39 -        let val _ = Output.report (reported_text ())
    4.40 +        let
    4.41 +      (** )val _ = @{print} {a = "### Token.syntax_generic, Scan.error"};( *..NOT yet available 2 *)
    4.42 +      (** )val _ = writeln "### Token.syntax_generic, Scan.error";( **)
    4.43 +          val _ = Output.report (reported_text ())
    4.44          in (x, context') end
    4.45      | (_, (context', args2)) =>
    4.46          let

     5.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy	Mon Mar 08 10:04:37 2021 +0100
     5.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy	Fri Mar 12 12:48:55 2021 +0100
     5.3 @@ -11,8 +11,8 @@
     5.4  (** )"~~/src/Tools/isac/MathEngine/MathEngine"  ( *activate after devel.of BridgeJEdit*)
     5.5  (**) "HOL-SPARK.SPARK"                             (*remove after devel.of BridgeJEdit*)
     5.6  keywords
     5.7 -    "Example" :: thy_load ("str") (* "spark_vc" :: thy_goal *)
     5.8 -  and "Problem" :: thy_decl (* root-problem + recursively in Solution;
     5.9 +(** )"Example" :: thy_load (**) (isac_example) (** ) "spark_vc" :: thy_goal *)
    5.10 +  and( **)"Problem" :: thy_decl (* root-problem + recursively in Solution;
    5.11                                 "spark_vc" :: thy_goal *)
    5.12    and "Specification" "Model" "References" :: diag
    5.13      (*TRIED: diag quasi_command qed_script thy_decl thy_defn thy_goal thy_goal_stmt thy_stmt vvv *)
    5.14 @@ -119,11 +119,13 @@
    5.15  section \<open>setup command_keyword + preliminary test\<close>
    5.16  ML \<open>                                            
    5.17  \<close> ML \<open>
    5.18 +(** )
    5.19  val _ =                                                  
    5.20    Outer_Syntax.command \<^command_keyword>\<open>Example\<close> "start a Calculation from a Formalise-file"
    5.21      (Resources.provide_parse_files "Example" -- Parse.parname
    5.22        >> (Toplevel.theory o           (*vvvvvvvvvvvvvvvvvvvv--- HACK makes test independent from session Isac*)
    5.23          (Preliminary.load_formalisation @{theory Biegelinie} ParseC.formalisation)) );
    5.24 +( **)
    5.25  \<close> ML \<open>
    5.26  (Toplevel.theory o (Preliminary.load_formalisation @{theory Biegelinie} ParseC.formalisation))
    5.27  :
    5.28 @@ -223,9 +225,9 @@
    5.29  \<close>
    5.30  
    5.31  subsection \<open>test runs with test-Example\<close>
    5.32 -(**)
    5.33 +(** )
    5.34  Example \<open>/usr/local/isabisac/src/Tools/isac/Examples/exp_Statics_Biegel_Timischl_7-70\<close>
    5.35 -
    5.36 +( **)
    5.37  Problem ("Biegelinie", ["Biegelinien"])
    5.38  (*1 collapse* )
    5.39    Specification: