1.1 --- a/src/Tools/isac/BridgeJEdit/Calculation.thy	Thu Nov 19 16:58:42 2020 +0100
     1.2 +++ b/src/Tools/isac/BridgeJEdit/Calculation.thy	Sun Nov 22 13:41:51 2020 +0100
     1.3 @@ -1124,11 +1124,13 @@
     1.4    From c.f.2b9b4b38ab96 we have found Fdl_Lexer.scan as the very model
     1.5    for scanning/parsing Formalise.T.
     1.6  \<close>
     1.7 -subsection \<open>testbed separating Fdl_Lexer.scan from SPARK code\<close>
     1.8 -ML_file "~~/test/HOL/SPARK/test-data.sml"  ML \<open>(*..:*)g_c_d_siv_content\<close>
     1.9 -declare [[ML_print_depth = 10]] (* 3 7 10 9999999999 *)
    1.10 +
    1.11 +subsection \<open>testbed separates Fdl_Lexer.scan + Fdl_Parser from SPARK code\<close>
    1.12 +ML_file "~~/test/HOL/SPARK/test-data.sml" (*..:*)ML \<open>g_c_d_siv_content\<close>
    1.13 +declare [[ML_print_depth = 7]] (* 3 7 10 20 999999999 *)
    1.14  ML \<open>
    1.15  open Fdl_Lexer
    1.16 +(** )open Fdl_Parser( *conflict with some of Fdl_Lexer.* *)
    1.17  (*
    1.18    step 1: go top down and keep respective results according to trace from
    1.19            spark_open \<open>greatest_common_divisor/g_c_d\<close> SPARK/../Greatest_Common_Divisor.thy.
    1.20 @@ -1141,6 +1143,7 @@
    1.21            in order to reduce noise and to focus the code under actual consideration.
    1.22    step 2: at bottom gather the most elementary funs for transformation
    1.23             of g_c_d_siv_content to args of Fdl_Lexer.scan
    1.24 +  step 3: parse the tokens created by  Fdl_Lexer.scan
    1.25  *)
    1.26  \<close> ML \<open>
    1.27  \<close> ML \<open> (** high start level: parsing to header + VCs **)
    1.28 @@ -1160,8 +1163,17 @@
    1.29    then () else error "Fdl_Parser.parse_vcs header CHANGED";
    1.30  if length vcss = 11 (* verification conditions (VCs) from g_c_d_siv_content *) then
    1.31    case vcss of
    1.32 -    ("path(s) from start to run-time check associated with statement of line 8",
    1.33 -      [("procedure_g_c_d_1", ([], [("1", _(*Ident "true": Fdl_Parser.expr*))]))]) :: _ => ()
    1.34 +    ("path(s) from start to run-time check associated with statement of line 8", 
    1.35 +      [("procedure_g_c_d_1", ([], [("1", Fdl_Parser.Ident "true")]))]) ::
    1.36 +    ("path(s) from start to run-time check associated with statement of line 8", 
    1.37 +      [("procedure_g_c_d_2", ([], [("1", Fdl_Parser.Ident "true")]))]) ::
    1.38 +    ("path(s) from start to assertion of line 10", 
    1.39 +      [("procedure_g_c_d_3", ([], [("1", Fdl_Parser.Ident "true")]))]) :: 
    1.40 +    ("path(s) from assertion of line 10 to assertion of line 10",
    1.41 +      [("procedure_g_c_d_4",
    1.42 +        (("1", Fdl_Parser.Funct (">=", [Fdl_Parser.Ident "c", Fdl_Parser.Number 0])) :: 
    1.43 +         ("2", Fdl_Parser.Funct (">", [Fdl_Parser.Ident "d", Fdl_Parser.Number 0])) :: _,
    1.44 +         _))]) :: _ => ()
    1.45    | _ => error "Fdl_Parser.parse_vcs vcss CHANGED 1"
    1.46  else error "Fdl_Parser.parse_vcs vcss CHANGED 2";
    1.47  \<close> ML \<open>
    1.48 @@ -1191,7 +1203,7 @@
    1.49  else error "Fdl_Lexer.tokenize header CHANGED 2";
    1.50  \<close> ML \<open>
    1.51  \<close> ML \<open>
    1.52 -\<close> ML \<open> (* lower level 2: lexing the string *)
    1.53 +\<close> ML \<open> (* lower level 2: tokenize the string *)
    1.54  val chars = Fdl_Lexer.explode_pos g_c_d_siv_content(*_content*) Position.start;
    1.55  if length chars = 2886 then () else error "Fdl_Lexer.explode_pos g_c_d_siv_content CHANGED";
    1.56  val level2_header_toks = (Scan.finite char_stopper (*..from tokenize..*)
    1.57 @@ -1215,6 +1227,24 @@
    1.58     []) => ()
    1.59  | _ => error "Fdl_Lexer.scan level2 CHANGED";
    1.60  \<close> ML \<open>
    1.61 +\<close> ML \<open>
    1.62 +\<close> ML \<open> (* lower level 2: parse the tokens *)
    1.63 +val ((_, tokens), _) = level2_header_toks;
    1.64 +\<close> ML \<open>
    1.65 +Fdl_Parser.vcs: T list ->
    1.66 +  ((string * string) * (string * (string * ((string * Fdl_Parser.expr) list * (string * Fdl_Parser.expr) list)) list) list)
    1.67 +  * T list;
    1.68 +(filter Fdl_Lexer.is_proper): T list -> T list;
    1.69 +\<close> ML \<open>
    1.70 +val (parsed', _) =
    1.71 +  Scan.finite Fdl_Lexer.stopper (Scan.error (Fdl_Parser.!!! Fdl_Parser.vcs))
    1.72 +    (filter Fdl_Lexer.is_proper (*|*)tokens(*|*))
    1.73 +(* ---------------------------------------------------------------------------\
    1.74 +                 Fdl_Parser.vcs (*|*)tokens(*|*)
    1.75 +exception ABORT fn raised (line 109 of "General/scan.ML") --------------------/ *)
    1.76 +\<close> ML \<open>
    1.77 +if parsed' = ((str, str2), vcss) then () else error "Fdl_Parser.parse_vcs level 2 CHANGED 2";
    1.78 +\<close> ML \<open>
    1.79  \<close>
    1.80  
    1.81  end