1.1 --- a/src/Tools/isac/TODO.thy	Tue Jul 28 16:17:42 2020 +0200
     1.2 +++ b/src/Tools/isac/TODO.thy	Fri Jul 31 12:21:34 2020 +0200
     1.3 @@ -224,6 +224,19 @@
     1.4  text \<open>
     1.5    \begin{itemize}
     1.6    \item xxx          
     1.7 +  \item xxx
     1.8 +  \item make parser mutually recursive for Problem .. Solution
     1.9 +    preps. in Test_Parse_Isac:
    1.10 +      Test_Parse_Isac:
    1.11 +        subsubsection "problem_mini" shows a principal issue with recursive parsing
    1.12 +        probably due to !2! arguments of parser (as shown in Cookbook)
    1.13 +      Test_Parsers_Cookbook:
    1.14 +        (* recursive parser p.140 \<section>6.1 adapted to tokens: *) shows differences,
    1.15 +        which might help understanding the principal issue
    1.16 +    see also Test_Parsers  subsection "recursive parsing"
    1.17 +  \item xxx
    1.18 +  \item xxx          
    1.19 +  \item xxx          
    1.20    \item revisit bootstrap Calcelements. rule->calcelems->termC
    1.21      would be nice, but is hard: UnparseC.terms -> TermC.s_to_string
    1.22    \item xxx

     2.1 --- a/test/Pure/Isar/Test_Parse_Isac.thy	Tue Jul 28 16:17:42 2020 +0200
     2.2 +++ b/test/Pure/Isar/Test_Parse_Isac.thy	Fri Jul 31 12:21:34 2020 +0200
     2.3 @@ -19,6 +19,10 @@
     2.4  \<close> ML \<open>
     2.5  fun parse parser toks = Scan.finite Token.stopper (Scan.error parser) toks
     2.6  \<close> ML \<open>
     2.7 +fun string_of_strs strs = fold (curry op ^) (rev strs) ""
     2.8 +\<close> ML \<open>
     2.9 +fun string_of_toks toks = fold (curry op ^) (map Token.unparse toks |> rev |> separate ", ") "";
    2.10 +\<close> ML \<open>
    2.11  \<close>
    2.12  
    2.13  section \<open>Goals for parsing\<close>
    2.14 @@ -168,8 +172,6 @@
    2.15        steps_nonrec
    2.16  )
    2.17  \<close> ML \<open>
    2.18 -problem_whole_str
    2.19 -\<close> ML \<open>
    2.20  if problem_whole_str =
    2.21    "Problem ( \"Biegelinie\" , [\"Biegelinien\"] )" ^
    2.22      "Specification:" ^
    2.23 @@ -354,9 +356,7 @@
    2.24      (model -- references) (**)
    2.25  )
    2.26  \<close> ML \<open>
    2.27 -val specification_whole' = Scan.finite Token.stopper specification_whole
    2.28 -\<close> ML \<open>
    2.29 -specification_whole toks
    2.30 +parse specification_whole toks
    2.31  (* = (((
    2.32    "Specification", ":"),
    2.33       ((((((((((((((
    2.34 @@ -616,7 +616,19 @@
    2.35  
    2.36  subsubsection \<open>enter Specification TODO\<close>
    2.37  text \<open>
    2.38 -the Model only has Descriptors and the References are empty
    2.39 +  the Model only has Descriptors and the References are empty
    2.40 +\<close> ML \<open>
    2.41 +val toks = tokenize (
    2.42 +  problem_headline_str ^
    2.43 +    "Specification:" ^
    2.44 +      model_empty_str ^ (* <<<----- empty *)
    2.45 +      "References:" ^   (* <<<----- collapsed *)
    2.46 +    "Solution:"
    2.47 +)
    2.48 +\<close> text \<open>
    2.49 +parse problem toks
    2.50 +\<close> ML \<open>
    2.51 +\<close> ML \<open>
    2.52  \<close> ML \<open>
    2.53  \<close> ML \<open>
    2.54  \<close> ML \<open>
    2.55 @@ -720,10 +732,8 @@
    2.56    problem_nonrec  parser
    2.57  (*               ^^^^^^^*)
    2.58  \<close> ML \<open>
    2.59 -parse problem_nonrec toks
    2.60 -\<close> ML \<open>
    2.61  case parse problem_nonrec toks of
    2.62 -  (((((((((("Problem", "("), "Biegelinie"), ","), ["Biegelinien"]), ")"), (* problem_headline *)
    2.63 +  (((((((((("Problem", "("), "Biegelinie"), ","), ["Biegelinien"]), ")"), (* ..problem_headline *)
    2.64        (("Specification", ":"),
    2.65         ((((((((((( (((("", (("", ""), "")), ""), ""), ""), []), ""), ""), []), ""), ""), ""), ""), ""),
    2.66           []), (((((((((("", ""), ""), ""), ""), ""), ""), []), ""), ""), []) )))
    2.67 @@ -741,10 +751,114 @@
    2.68  \<close> ML \<open>
    2.69  \<close>
    2.70  
    2.71 +subsubsection \<open>problem_mini\<close>
    2.72 +text \<open>
    2.73 +  we make a minimal problem in order to investigate types
    2.74 +  of the parser's components
    2.75 +\<close> ML \<open>
    2.76 +val problem_headline_mini = Parse.$$$ "Problem" 
    2.77 +\<close> ML \<open>
    2.78 +val specification_mini = Parse.$$$ "Specification"
    2.79 +\<close> ML \<open>
    2.80 +fun exec_name str = "EXEC IMMEDIATELY exec_name: " ^ str;
    2.81 +fun exec_int int = "EXEC IMMEDIATELY exec_int: " ^ string_of_int int;
    2.82 +\<close> ML \<open>
    2.83 +Parse.name >> exec_name: string parser;
    2.84 +Parse.int >> exec_int  : string parser
    2.85 +\<close> ML \<open>
    2.86 +\<close> ML \<open> (* nonrecursive *)
    2.87 +fun problem_mini toks =
    2.88 +  problem_headline_mini --
    2.89 +  specification_mini -- steps_mini toks
    2.90 +and steps_mini _ =
    2.91 +  Parse.name >> exec_name || Parse.int >> exec_int
    2.92 +\<close> ML \<open>
    2.93 +(problem_mini "") (tokenize "Problem Specification aaa")
    2.94 +(* = ((("Problem", "Specification"), "EXEC IMMEDIATELY exec_name: aaa"), [])*)
    2.95 +\<close> ML \<open>
    2.96 +problem_mini: 'a -> Token.T list -> ((string * string) * string) * Token.T list
    2.97 +\<close> ML \<open>
    2.98 +fun exec_problem_mini ((headl, spec), steps) =
    2.99 +  ["EXEC IMMEDIATELY exec_int: ((" ^ headl ^ ", " ^ spec ^ "0, " ^ string_of_strs steps];
   2.100 +\<close> ML \<open>
   2.101 +fun exec_name str = ["EXEC IMMEDIATELY exec_name: " ^ str];
   2.102 +\<close> ML \<open>
   2.103 +\<close> ML \<open> (* recursive *)
   2.104 +fun problem_mini toks =
   2.105 +  (problem_headline_mini --
   2.106 +  specification_mini -- steps_mini) toks
   2.107 +and steps_mini toks =
   2.108 +  (Parse.name >> exec_name || problem_mini >> exec_problem_mini) toks
   2.109 +\<close> ML \<open>
   2.110 +problem_mini: Token.T list -> ((string * string) * string list) * Token.T list ;
   2.111 +steps_mini  : Token.T list -> string list * Token.T list ;
   2.112 +\<close> ML \<open>
   2.113 +problem_mini: ((string * string) * string list) parser;
   2.114 +steps_mini  : string list parser;
   2.115 +\<close> ML \<open>
   2.116 +problem_mini (tokenize "Problem Specification aaa")
   2.117 +(* = ((("Problem", "Specification"), ["EXEC IMMEDIATELY exec_name: aaa"]), [])*)
   2.118 +\<close> text \<open> ERROR ?!?!?
   2.119 +parse problem_mini (tokenize "Problem Specification   Problem Specification")
   2.120 +exception FAIL (SOME fn) raised (line 152 of "General/scan.ML")
   2.121 +\<close> ML \<open>
   2.122 +\<close> ML \<open>
   2.123 +\<close> ML \<open> (* recursive + repeat *)
   2.124 +fun exec_name str = "EXEC IMMEDIATELY exec_name: " ^ str;
   2.125 +\<close> ML \<open>
   2.126 +fun exec_problem_mini ((headl, spec), steps) =
   2.127 +  "EXEC IMMEDIATELY exec_int: ((" ^ headl ^ ", " ^ spec ^ "0, " ^ string_of_strs steps;
   2.128 +\<close> ML \<open>
   2.129 +fun problem_mini toks =
   2.130 +  (writeln ("problem_mini " ^ string_of_toks toks); problem_headline_mini --
   2.131 +  specification_mini -- (writeln ("steps_mini   " ^ string_of_toks toks); steps_mini)) toks
   2.132 +and steps_mini toks =
   2.133 +  (Scan.repeat
   2.134 +    ((writeln ("name         " ^ string_of_toks toks); Parse.name >> exec_name) (**)||
   2.135 +     (writeln ("sub-problem  " ^ string_of_toks toks); problem_mini >> exec_problem_mini)(**))) toks
   2.136 +\<close> text \<open>
   2.137 +problem_mini (tokenize "Problem Specification")
   2.138 +(*
   2.139 +problem_mini Problem, Specification 
   2.140 +steps_mini   Problem, Specification 
   2.141 +name          
   2.142 +sub-problem   
   2.143 +exception MORE () raised (line 159 of "General/scan.ML")*)
   2.144 +\<close> text \<open>
   2.145 +problem_mini (tokenize "Problem Specification aaa")
   2.146 +(*
   2.147 +problem_mini Problem, Specification, aaa 
   2.148 +steps_mini   Problem, Specification, aaa 
   2.149 +name         aaa 
   2.150 +sub-problem  aaa 
   2.151 +exception MORE () raised (line 159 of "General/scan.ML")
   2.152 +
   2.153 +NOTE: this error persists in case outcommented (** )||
   2.154 +     (writeln ("sub-problem  " ^ string_of_toks toks); problem_mini >> exec_problem_mini)( **)
   2.155 +
   2.156 +THUS THERE IS SOMETHING NOT UNDERSTOOD, see !2! arguments in Test_Parsers_Cookbook.thy
   2.157 +see Test_Parsers_Cookbook (* recursive parser p.140 \<section>6.1 adapted to tokens: *)
   2.158 +*)
   2.159 +\<close> ML \<open>
   2.160 +\<close> ML \<open>
   2.161 +\<close> ML \<open>
   2.162 +\<close> ML \<open>
   2.163 +\<close> ML \<open>
   2.164 +\<close> ML \<open>
   2.165 +\<close> ML \<open>
   2.166 +\<close> ML \<open>
   2.167 +\<close> ML \<open>
   2.168 +\<close> ML \<open>
   2.169 +\<close> ML \<open>
   2.170 +\<close> ML \<open>
   2.171 +\<close> ML \<open>
   2.172 +\<close> ML \<open>
   2.173 +\<close> ML \<open>
   2.174 +\<close>
   2.175 +
   2.176  subsubsection \<open>recursion finalised\<close>
   2.177  ML \<open>
   2.178  \<close> ML \<open>
   2.179 -\<close> ML \<open>
   2.180  val toks = tokenize (
   2.181    problem_headline_str ^
   2.182      "Specification:" ^
   2.183 @@ -753,8 +867,7 @@
   2.184  )
   2.185  \<close> ML \<open>
   2.186  fun exec_step_term (tm, (tac1, tac2)) = exec_step_term_nonrec (tm, (tac1, tac2));
   2.187 -\<close> ML \<open>
   2.188 -(* finding the type of exec_subproblem: *)
   2.189 +\<close> ML \<open> (* finding the type of exec_subproblem: *)
   2.190  fun problem xxx =
   2.191    problem_headline --
   2.192      specification --
   2.193 @@ -766,7 +879,7 @@
   2.194        )
   2.195  \<close> ML \<open>
   2.196  problem : (problem_nonrec -> string) -> problem_nonrec parser
   2.197 -(*  xxx : ^^^^^^^^^^^^^^^^^^^^^^^^^^*)
   2.198 +(*  xxx : ^^^^^^^^^^^^^^^^^^^^^^^^^^                   ^^^^^^*)
   2.199  \<close> text \<open>
   2.200  (* type of xxx from <Output>: *)
   2.201  (((((((((string * string) * string) * string) * string list) * string) *
   2.202 @@ -783,7 +896,7 @@
   2.203          strs18), s19), s20), strs21), s22), s23), s24), s25), s26), strs27),
   2.204           ((((((((((s31, s32), s33), s34), s35), s36), s37), strs38), s39), s40), strs41) )))
   2.205       , s51), s61), strs71) =
   2.206 -  "EXEC IMMEDIATELY step_subproblem:\n " ^
   2.207 +  "EXEC IMMEDIATELY step_subproblem:\n" ^
   2.208    "(((( (((((" ^ s1 ^ ", " ^ s2 ^ "), " ^ s3 ^"), " ^ s4 ^"), " ^ LibraryC.strs2str strs5 ^ "), " ^ s6 ^")\n " ^
   2.209    "((" ^s7 ^ ", " ^s8 ^ "),\n" ^
   2.210    "  ((((((((((( ((((" ^ s11 ^", ((" ^s12 ^ ", " ^ s13 ^ "), " ^ s14 ^ ")), " ^ s15 ^"), " ^s16 ^"), " ^ s17 ^ "),\n " ^
   2.211 @@ -808,24 +921,27 @@
   2.212  \<close> ML \<open>
   2.213  exec_subproblem : problem_nonrec -> string
   2.214  \<close> ML \<open>
   2.215 -fun problem xxx =
   2.216 +\<close> ML \<open> (* exec_subproblem has right? type in problem *)
   2.217 +fun problem _ =
   2.218    problem_headline --
   2.219      specification --
   2.220 -    Parse.$$$ "Solution" -- Parse.$$$ ":" -- (steps xxx)
   2.221 -and steps xxx =
   2.222 +    Parse.$$$ "Solution" -- Parse.$$$ ":" -- (steps 1)
   2.223 +and steps _ =
   2.224        Scan.repeat (
   2.225          (
   2.226            ((Parse.term -- (Scan.optional tactic ("", ""))) >> exec_step_term) ||
   2.227 -          (problem xxx >> exec_subproblem)
   2.228 -    (*                    ^^^^^^^^^^^^^^^*)
   2.229 +          (problem 1 >> exec_subproblem)
   2.230 +    (*                  ^^^^^^^^^^^^^^^*)
   2.231          )
   2.232        )
   2.233  \<close> ML \<open>
   2.234 -problem : (problem_nonrec -> string) -> problem_nonrec parser
   2.235 -(*  xxx : ^^^^^^^^^^^^^^^^^^^^^^^^^^ ..exec_subproblem*)
   2.236 +problem : int -> problem_nonrec parser
   2.237  \<close> ML \<open>
   2.238 -\<close> ML \<open>
   2.239 -\<close> ML \<open> (* here is the attempt towards finalisation *)
   2.240 +steps   : int -> string list    parser
   2.241 +\<close> ML \<open> (* BUT: omitting the parsers' arguments does NOT work:
   2.242 +
   2.243 + *)
   2.244 +\<close> ML \<open> (* here is the attempt towards finalisation * )
   2.245  val problem =
   2.246    problem_headline --
   2.247      specification --
   2.248 @@ -837,106 +953,7 @@
   2.249            (problem >> exec_subproblem)
   2.250          )
   2.251        )
   2.252 -\<close> text \<open>
   2.253 -ML error:
   2.254 -Type error in function application.
   2.255 -   Function: -- :
   2.256 -      (Token.T list ->
   2.257 -         ((((((((string * string) * string) * string) * string list) * string) *
   2.258 -            ((string * string) *
   2.259 -             (((((((((((((((string * ((string * string) * string)) * string) * string) * string) * string list) * string) * string) * string list) * string) * string) * string) * string) * string) * string list) *
   2.260 -              ((((((((((string * string) * string) * string) * string) * string) * string) * string list) * string) * string) * string list))))
   2.261 -           *
   2.262 -           string)
   2.263 -          *
   2.264 -          string)
   2.265 -         *
   2.266 -         Token.T list)
   2.267 -      *
   2.268 -      (Token.T list -> 'a * 'b)
   2.269 -        ->
   2.270 -        Token.T list ->
   2.271 -          (((((((((string * string) * string) * string) * string list) * string) *
   2.272 -              ((string * string) *
   2.273 -               (((((((((((((((string * ((string * string) * string)) * string) * string) * string) * string list) * string) * string) * string list) * string) * string) * string) * string) * string) * string list)
   2.274 -                *
   2.275 -                ((((((((((string * string) * string) * string) * string) * string) * string) * string list) * string) * string) * string list))))
   2.276 -             *
   2.277 -             string)
   2.278 -            *
   2.279 -            string)
   2.280 -           *
   2.281 -           'a)
   2.282 -          *
   2.283 -          'b
   2.284 -   Argument: (problem_headline -- specification -- Parse.$$$ "Solution" -- Parse.$$$ ":", steps) :
   2.285 -      (Token.T list ->
   2.286 -         ((((((((string * string) * string) * string) * string list) * string) *
   2.287 -            ((string * string) *
   2.288 -             (((((((((((((((string * ((string * string) * string)) * string) * string) * string) * string list) * string) * string) * string list) * string) * string) * string) * string) * string) * string list) *
   2.289 -              ((((((((((string * string) * string) * string) * string) * string) * string) * string list) * string) * string) * string list))))
   2.290 -           *
   2.291 -           string)
   2.292 -          *
   2.293 -          string)
   2.294 -         *
   2.295 -         Token.T list)
   2.296 -      *
   2.297 -      (Token.T list -> Token.T list -> string list * Token.T list)
   2.298 -   Reason: Can't unify 'a * 'b to Token.T list -> string list * Token.T list (Incompatible types)
   2.299 -ML error:
   2.300 -Type error in function application.
   2.301 -   Function: >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
   2.302 -   Argument: (problem, exec_subproblem) :
   2.303 -      ('a ->
   2.304 -         Token.T list ->
   2.305 -           (((((((((string * string) * string) * string) * string list) * string) *
   2.306 -               ((string * string) *
   2.307 -                (((((((((((((((string * ((string * string) * string)) * string) * string) * string) * string list) * string) * string) * string list) * string) * string) * string) * string) * string) *
   2.308 -                  string list)
   2.309 -                 *
   2.310 -                 ((((((((((string * string) * string) * string) * string) * string) * string) * string list) * string) * string) * string list))))
   2.311 -              *
   2.312 -              string)
   2.313 -             *
   2.314 -             string)
   2.315 -            *
   2.316 -            string list)
   2.317 -           *
   2.318 -           Token.T list)
   2.319 -      *
   2.320 -      (((((((((string * string) * string) * string) * string list) * string) *
   2.321 -          ((string * string) *
   2.322 -           (((((((((((((((string * ((string * string) * string)) * string) * string) * string) * string list) * string) * string) * string list) * string) * string) * string) * string) * string) * string list) *
   2.323 -            ((((((((((string * string) * string) * string) * string) * string) * string) * string list) * string) * string) * string list))))
   2.324 -         *
   2.325 -         string)
   2.326 -        *
   2.327 -        string)
   2.328 -       *
   2.329 -       string list
   2.330 -         -> string)
   2.331 -   Reason:
   2.332 -      Can't unify 'a * 'b to
   2.333 -         Token.T list ->
   2.334 -           (((((((((string * string) * string) * string) * string list) * string) *
   2.335 -               ((string * string) *
   2.336 -                (((((((((((((((string * ((string * string) * string)) * string) * string) * string) * string list) * string) * string) * string list) * string) * string) * string) * string) * string) *
   2.337 -                  string list)
   2.338 -                 *
   2.339 -                 ((((((((((string * string) * string) * string) * string) * string) * string) * string list) * string) * string) * string list))))
   2.340 -              *
   2.341 -              string)
   2.342 -             *
   2.343 -             string)
   2.344 -            *
   2.345 -            string list)
   2.346 -           *
   2.347 -           Token.T list
   2.348 -         (Incompatible types)
   2.349 -\<close> ML \<open>
   2.350 -\<close> ML \<open>
   2.351 -\<close> ML \<open>
   2.352 +*)
   2.353  \<close> ML \<open>
   2.354  \<close> ML \<open>
   2.355  \<close> ML \<open>

     3.1 --- a/test/Pure/Isar/Test_Parsers.thy	Tue Jul 28 16:17:42 2020 +0200
     3.2 +++ b/test/Pure/Isar/Test_Parsers.thy	Fri Jul 31 12:21:34 2020 +0200
     3.3 @@ -187,6 +187,49 @@
     3.4  ML \<open>(*from Pure/Isar/args.ML, fun attribs*)
     3.5  Parse.$$$ "[" |-- Parse.list1 Parse.name --| Parse.$$$ "]";
     3.6  (*fn : Token.T list -> bstring list * Token.T list*)
     3.7 +\<close> ML \<open>
     3.8 +\<close> ML \<open> (* example close to lists see Cookbook p.144 \<section>6.2 *)
     3.9 +let
    3.10 +  val input = filtered_input "in , in , in"
    3.11 +  val p = Parse.enum "," (Parse.$$$ "in")
    3.12 +in
    3.13 +  Scan.finite Token.stopper p input
    3.14 +end
    3.15 +(* = (["in", "in", "in"], []) *)
    3.16 +\<close> ML \<open>
    3.17 +let
    3.18 +  val input = filtered_input "aaa , bbb , ccc"
    3.19 +  val p = Parse.enum "," Parse.name
    3.20 +in
    3.21 +  Scan.finite Token.stopper p input
    3.22 +end
    3.23 +(* = (["aaa", "bbb", "ccc"], []) *)
    3.24 +\<close> ML \<open>
    3.25 +let
    3.26 +  val input = filtered_input "\"aaa\" , \"bbb\" , \"ccc\""
    3.27 +  val p = Parse.enum "," Parse.string
    3.28 +in
    3.29 +  Scan.finite Token.stopper p input
    3.30 +end
    3.31 +(* = (["aaa", "bbb", "ccc"], []) *)
    3.32 +\<close> ML \<open>
    3.33 +let
    3.34 +  val input = filtered_input "\"aaa\" , \"bbb\" , \"ccc\""
    3.35 +  val p = Parse.list1 Parse.string
    3.36 +in
    3.37 +  Scan.finite Token.stopper p input
    3.38 +end
    3.39 +(* = (["aaa", "bbb", "ccc"], []) *)
    3.40 +\<close> ML \<open>
    3.41 +let
    3.42 +  val input = filtered_input "[\"aaa\" , \"bbb\" , \"ccc\"]"
    3.43 +  val p = Parse.$$$ "[" |-- Parse.list1 Parse.string --| Parse.$$$ "]"
    3.44 +in
    3.45 +  Scan.finite Token.stopper p input
    3.46 +end
    3.47 +(* = (["aaa", "bbb", "ccc"], []) *)
    3.48 +
    3.49 +
    3.50  
    3.51  \<close> ML \<open>
    3.52  parse (Parse.$$$ "[" |-- Parse.list Parse.name --| Parse.$$$ "]")

     4.1 --- a/test/Pure/Isar/Test_Parsers_Cookbook.thy	Tue Jul 28 16:17:42 2020 +0200
     4.2 +++ b/test/Pure/Isar/Test_Parsers_Cookbook.thy	Fri Jul 31 12:21:34 2020 +0200
     4.3 @@ -1,17 +1,9 @@
     4.4 -chapter \<open>Trials derived from NEW Isabelle Cookbook\<close>
     4.5 +(*
     4.6 +  Trials derived from NEW Isabelle Cookbook
     4.7 +*)
     4.8  
     4.9  theory Test_Parsers_Cookbook
    4.10    imports (**) Pure (** ) HOL.Complex ( *.. for inductive even BELOW*)
    4.11 -keywords (*see section \<open>Own trials ..\<close>*)
    4.12 -  (* this has a type and thus is a "major keyword" * )
    4.13 -  "ISAC" :: diag and
    4.14 -  ( * the following are without type: "minor keywords" *)
    4.15 -  "Problem" (* root-problem + recursively in Solution *)
    4.16 -  "Specification" "Model" "References" "Solution" (* structure only *) and
    4.17 -  "Given" "Find" "Relate" "Where" (* await input of term *) and
    4.18 -  "RTheory" (* await input of string; "R" distingues "Problem".."RProblem" *) and
    4.19 -  "RProblem" "RMethod" (* await input of string list *) and
    4.20 -  "Tactic" (* optionally repeated with each step 0.. end of calculation *)
    4.21  begin
    4.22  
    4.23  text \<open> trials on parsing with C.U.'s Isabelle Cookbook
    4.24 @@ -175,6 +167,205 @@
    4.25  \<close> ML \<open>
    4.26  \<close>
    4.27  
    4.28 +subsection \<open>recursive parsers\<close>
    4.29 +subsubsection \<open>recursive parser p.140 \<section>6.1\<close>
    4.30 +ML \<open>
    4.31 +\<close> ML \<open>
    4.32 +datatype tree =
    4.33 +    Lf of string
    4.34 +  | Br of tree * tree
    4.35 +\<close> ML \<open> (* this version loops *)
    4.36 +fun parse_basic s =
    4.37 +  $$ s >> Lf || $$ "(" |-- parse_tree s --| $$ ")"
    4.38 +and parse_tree s =
    4.39 +  parse_basic s --| $$ "," -- parse_tree s >> Br || parse_basic s
    4.40 +\<close> ML \<open>
    4.41 +parse_basic: string -> string list -> tree * string list;
    4.42 +parse_tree : string -> string list -> tree * string list
    4.43 +\<close> ML \<open>
    4.44 +\<close> ML \<open> (* this version works *)
    4.45 +fun parse_basic s xs =
    4.46 +  ($$ s >> Lf || $$ "(" |-- parse_tree s --| $$ ")") xs
    4.47 +and parse_tree s xs =
    4.48 +  (parse_basic s --| $$ "," -- parse_tree s >> Br || parse_basic s) xs
    4.49 +\<close> ML \<open>
    4.50 +parse_basic: string -> string list -> tree * string list;
    4.51 +parse_tree : string -> string list -> tree * string list
    4.52 +\<close> ML \<open>
    4.53 +let
    4.54 +  val input = Symbol.explode "(A,((A))),A"
    4.55 +in
    4.56 +  Scan.finite Symbol.stopper (parse_tree "A") (input)
    4.57 +end
    4.58 +(*= (Br (Br (Lf "A", Lf "A"), Lf "A"), []) *)
    4.59 +\<close> ML \<open>
    4.60 +Scan.finite Symbol.stopper (parse_tree "A") (Symbol.explode "(A,((A))),A")
    4.61 + = (Br (Br (Lf "A", Lf "A"), Lf "A"), [])
    4.62 +\<close> ML \<open>
    4.63 +Scan.finite Symbol.stopper (parse_tree "B") (Symbol.explode "(B,((B))),B")
    4.64 + = (Br (Br (Lf "B", Lf "B"), Lf "B"), [])
    4.65 +\<close> ML \<open>
    4.66 +Br (Lf "a",                Lf "b");
    4.67 +Br (Lf "a",                Br (Lf "b1", Lf "b2"));
    4.68 +Br (Br (Lf "a1", Lf "a2"), Br (Lf "b1", Lf "b2"));
    4.69 +\<close> ML \<open>
    4.70 +\<close> ML \<open>
    4.71 +Scan.finite Symbol.stopper (parse_tree "A") (Symbol.explode "A")
    4.72 + = (Lf "A", [])
    4.73 +\<close> ML \<open>
    4.74 +Scan.finite Symbol.stopper (parse_tree "A") (Symbol.explode "A A")
    4.75 + = (Lf "A", [" ", "A"])
    4.76 +\<close> ML \<open>
    4.77 +Scan.finite Symbol.stopper (parse_tree "A") (Symbol.explode "A B")
    4.78 + = (Lf "A", [" ", "B"])
    4.79 +\<close> ML \<open>
    4.80 +Scan.finite Symbol.stopper (parse_tree "A") (Symbol.explode "AB")
    4.81 + = (Lf "A", ["B"])
    4.82 +\<close> ML \<open>
    4.83 +Scan.finite Symbol.stopper (parse_tree "A") (Symbol.explode "A,")
    4.84 + = (Lf "A", [","])
    4.85 +\<close> text \<open>
    4.86 +Scan.finite Symbol.stopper (parse_tree "A") (Symbol.explode "(A,")
    4.87 +exception FAIL NONE raised (line 161 of "General/scan.ML")
    4.88 +\<close> ML \<open>
    4.89 +\<close> ML \<open>
    4.90 +\<close>
    4.91 +
    4.92 +subsubsection \<open>recursive parser p.140 \<section>6.1 + writeln\<close>
    4.93 +ML \<open>
    4.94 +\<close> ML \<open>
    4.95 +fun string_of_strs strs = fold (curry op ^) (rev strs) ""
    4.96 +\<close> ML \<open>
    4.97 +fun parse_basic s xs =
    4.98 +(
    4.99 +  writeln ("parse_basic " ^ s ^ " " ^ string_of_strs xs);
   4.100 +  ($$ s >> Lf || $$ "(" |-- parse_tree s --| $$ ")") xs
   4.101 +)
   4.102 +and parse_tree s xs =
   4.103 +(
   4.104 +  writeln ("parse_tree  " ^ s ^ " " ^ string_of_strs xs);
   4.105 +  (parse_basic s --| $$ "," -- parse_tree s >> Br || parse_basic s) xs
   4.106 +)
   4.107 +\<close> ML \<open>
   4.108 +Scan.finite Symbol.stopper (parse_tree "A") (Symbol.explode "(A,((A))),A")
   4.109 +(*
   4.110 +parse_tree  A (A,((A))),A 
   4.111 +parse_basic A (A,((A))),A 
   4.112 +parse_tree  A A,((A))),A 
   4.113 +parse_basic A A,((A))),A 
   4.114 +
   4.115 +parse_tree  A ((A))),A     ..1 + from here the version with tokenize differs
   4.116 +parse_basic A ((A))),A 
   4.117 +parse_tree  A (A))),A 
   4.118 +parse_basic A (A))),A 
   4.119 +parse_tree  A A))),A 
   4.120 +parse_basic A A))),A 
   4.121 +parse_basic A A))),A 
   4.122 +parse_basic A (A))),A 
   4.123 +parse_tree  A A))),A 
   4.124 +parse_basic A A))),A 
   4.125 +parse_basic A A))),A 
   4.126 +parse_basic A ((A))),A      ..1
   4.127 +parse_tree  A (A))),A 
   4.128 +parse_basic A (A))),A 
   4.129 +parse_tree  A A))),A 
   4.130 +parse_basic A A))),A 
   4.131 +parse_basic A A))),A 
   4.132 +parse_basic A (A))),A 
   4.133 +parse_tree  A A))),A 
   4.134 +parse_basic A A))),A 
   4.135 +parse_basic A A))),A 
   4.136 +parse_tree  A A 
   4.137 +parse_basic A A 
   4.138 +parse_basic A A 
   4.139 +val it = (Br (Br (Lf "A", Lf "A"), Lf "A"), []): tree * string list*)
   4.140 +\<close> ML \<open>
   4.141 +\<close> ML \<open>
   4.142 +\<close> ML \<open>
   4.143 +\<close> ML \<open>
   4.144 +\<close> ML \<open>
   4.145 +\<close> ML \<open>
   4.146 +\<close> ML \<open>
   4.147 +\<close>
   4.148 +
   4.149 +subsubsection \<open>recursive parser, same with tokenise + writeln\<close>
   4.150 +text \<open>
   4.151 +  Differences between Cookbook original on strings and below on tokes
   4.152 +  might help to understand principles of recursive parsing.
   4.153 +  See also Test_Parsers:  subsection "recursive parsing" 
   4.154 +\<close> ML \<open>
   4.155 +\<close> ML \<open> (* tools from Test_Parse_Isac.thy *)
   4.156 +fun tokenize str =
   4.157 +  filter Token.is_proper (Token.explode (Thy_Header.get_keywords' @{context}) Position.none str)
   4.158 +fun parse parser toks = Scan.finite Token.stopper (Scan.error parser) toks
   4.159 +\<close> ML \<open>
   4.160 +val toks = tokenize "(A,((A))),A"
   4.161 +\<close> ML \<open>
   4.162 +fun string_of_toks toks = fold (curry op ^) (map Token.unparse toks |> rev) "";
   4.163 +string_of_toks toks = "(A,((A))),A"
   4.164 +\<close> ML \<open>
   4.165 +\<close> ML \<open> (* recursive parser p.140 \<section>6.1 adapted to tokens: *)
   4.166 +fun parse_basic s xs =
   4.167 +(
   4.168 +  writeln ("parse_basic " ^ s ^ " " ^ string_of_toks xs);
   4.169 +  (Parse.$$$ s >> Lf || Parse.$$$ "(" |-- parse_tree s --| Parse.$$$ ")") xs
   4.170 +)
   4.171 +and parse_tree s xs =
   4.172 +(
   4.173 +  writeln ("parse_tree  " ^ s ^ " " ^ string_of_toks xs);
   4.174 +  (parse_basic s --| Parse.$$$ "," -- parse_tree s >> Br || parse_basic s) xs
   4.175 +)
   4.176 +\<close> ML \<open>
   4.177 +parse_basic : string -> Token.T list -> tree * Token.T list;
   4.178 +parse_tree  : string -> Token.T list -> tree * Token.T list;
   4.179 +
   4.180 +parse_basic : string -> tree parser;
   4.181 +parse_tree  : string -> tree parser;
   4.182 +\<close> text \<open>
   4.183 +(parse_tree "A") (tokenize "(A,((A))),A");
   4.184 +(* compare subsubsection \<open>recursive parser p.140 \<section>6.1 + writeln\<close> ..
   4.185 +parse_tree  A (A,((A))),A 
   4.186 +parse_basic A (A,((A))),A 
   4.187 +parse_tree  A A,((A))),A 
   4.188 +parse_basic A A,((A))),A
   4.189 +                        parser p.140 \<section>6.1: parse_tree  A ((A))),A
   4.190 +                                           :
   4.191 +parse_basic A A,((A))),A                   .. different
   4.192 +parse_basic A (A,((A))),A 
   4.193 +parse_tree  A A,((A))),A 
   4.194 +parse_basic A A,((A))),A 
   4.195 +parse_basic A A,((A))),A 
   4.196 +exception FAIL (SOME fn) raised (line 152 of "General/scan.ML")*)
   4.197 +\<close> text \<open>
   4.198 +(parse_basic "A") (tokenize "A");
   4.199 +(*
   4.200 +parse_basic A A 
   4.201 +exception FAIL (SOME fn) raised (line 152 of "General/scan.ML")*)
   4.202 +\<close> text \<open>
   4.203 +parse (parse_basic "A") (tokenize "A")
   4.204 +(*
   4.205 +parse_basic A A 
   4.206 +exception FAIL (SOME fn) raised (line 152 of "General/scan.ML")*)
   4.207 +\<close> text \<open>
   4.208 +(parse_tree "A") (tokenize "(A,A)");
   4.209 +(*
   4.210 +parse_tree  A (A,A) 
   4.211 +parse_basic A (A,A) 
   4.212 +parse_tree  A A,A) 
   4.213 +parse_basic A A,A) 
   4.214 +parse_basic A A,A) 
   4.215 +parse_basic A (A,A) 
   4.216 +parse_tree  A A,A) 
   4.217 +parse_basic A A,A) 
   4.218 +parse_basic A A,A) 
   4.219 +exception FAIL (SOME fn) raised (line 152 of "General/scan.ML")*)
   4.220 +\<close> ML \<open>
   4.221 +\<close> ML \<open>
   4.222 +\<close> ML \<open>
   4.223 +\<close> ML \<open>
   4.224 +\<close>
   4.225 +
   4.226 +
   4.227  section \<open>Own trials, NO Parse.cartouche, NO Outer_Syntax.command\<close>
   4.228  text \<open>
   4.229    compare test/../Keywords_Diag.thy
   4.230 @@ -225,26 +416,4 @@
   4.231  \<close> ML \<open>
   4.232  \<close>
   4.233  
   4.234 -subsection \<open>problem_headline\<close>
   4.235 -text \<open>
   4.236 -  -> Test_Parsers_Isac.thy
   4.237 -\<close>
   4.238 -subsection \<open>Specification\<close>
   4.239 -text \<open>
   4.240 -  -> Test_Parsers_Isac.thy
   4.241 -\<close>
   4.242 -subsection \<open>Solution\<close>
   4.243 -text \<open>
   4.244 -  -> Test_Parsers_Isac.thy
   4.245 -\<close>
   4.246 -
   4.247 -subsubsection \<open>Problem - Solution recursively\<close>
   4.248 -ML \<open>
   4.249 -\<close> ML \<open>
   4.250 -\<close> ML \<open>
   4.251 -\<close> ML \<open>
   4.252 -\<close> ML \<open>
   4.253 -\<close> ML \<open>
   4.254 -\<close>
   4.255 -
   4.256 -(**)end (* Missing outer syntax command(s) "ISAC" *)
   4.257 +(**)end(**)

     5.1 --- a/test/Tools/isac/CLEANUP	Tue Jul 28 16:17:42 2020 +0200
     5.2 +++ b/test/Tools/isac/CLEANUP	Fri Jul 31 12:21:34 2020 +0200
     5.3 @@ -69,7 +69,7 @@
     5.4        rm *.orig~
     5.5        rm *.orig~~
     5.6        rm *.orig~~~
     5.7 -     cd .. 
     5.8 +      cd .. 
     5.9      cd SignalProcess
    5.10        rm *~
    5.11        rm #*
    5.12 @@ -79,16 +79,35 @@
    5.13        rm *.orig~
    5.14        rm *.orig~~
    5.15        rm *.orig~~~
    5.16 -     cd .. 
    5.17 +      cd .. 
    5.18      cd .. 
    5.19    cd file-depend
    5.20 -      rm *~
    5.21 -      rm #*
    5.22 -      rm .\#*
    5.23 -      rm *.tar*
    5.24 -      rm *.orig*
    5.25 -      cd .. 
    5.26 +    rm *~
    5.27 +    rm #*
    5.28 +    rm .\#*
    5.29 +    rm *.tar*
    5.30 +    rm *.orig*
    5.31 +    cd .. 
    5.32    cd libisabelle
    5.33 +    rm *~
    5.34 +    rm #*
    5.35 +    rm .\#*
    5.36 +    rm *.tar*
    5.37 +    rm *.orig
    5.38 +    rm *.orig~
    5.39 +    rm *.orig~~
    5.40 +    rm *.orig~~~
    5.41 +    cd .. 
    5.42 +  cd test-depend
    5.43 +    rm *~
    5.44 +    rm #*
    5.45 +    rm .\#*
    5.46 +    rm *.tar*
    5.47 +    rm *.orig
    5.48 +    rm *.orig~
    5.49 +    rm *.orig~~
    5.50 +    rm *.orig~~~
    5.51 +    cd testdir1
    5.52        rm *~
    5.53        rm #*
    5.54        rm .\#*
    5.55 @@ -98,7 +117,7 @@
    5.56        rm *.orig~~
    5.57        rm *.orig~~~
    5.58        cd .. 
    5.59 -  cd test-depend
    5.60 +    cd testdirm
    5.61        rm *~
    5.62        rm #*
    5.63        rm .\#*
    5.64 @@ -107,27 +126,28 @@
    5.65        rm *.orig~
    5.66        rm *.orig~~
    5.67        rm *.orig~~~
    5.68 -      cd testdir1
    5.69 -          rm *~
    5.70 -          rm #*
    5.71 -          rm .\#*
    5.72 -          rm *.tar*
    5.73 -          rm *.orig
    5.74 -          rm *.orig~
    5.75 -          rm *.orig~~
    5.76 -          rm *.orig~~~
    5.77 -          cd .. 
    5.78 -      cd testdirm
    5.79 -          rm *~
    5.80 -          rm #*
    5.81 -          rm .\#*
    5.82 -          rm *.tar*
    5.83 -          rm *.orig
    5.84 -          rm *.orig~
    5.85 -          rm *.orig~~
    5.86 -          rm *.orig~~~
    5.87 -          cd .. 
    5.88        cd .. 
    5.89 +    cd .. 
    5.90 +  cd .. 
    5.91 +cd Pure
    5.92 +  rm *~
    5.93 +  rm #*
    5.94 +  rm .\#*
    5.95 +  rm *.tar*
    5.96 +  rm *.orig
    5.97 +  rm *.orig~
    5.98 +  rm *.orig~~
    5.99 +  rm *.orig~~~
   5.100 +  cd Isar
   5.101 +    rm *~
   5.102 +    rm #*
   5.103 +    rm .\#*
   5.104 +    rm *.tar*
   5.105 +    rm *.orig
   5.106 +    rm *.orig~
   5.107 +    rm *.orig~~
   5.108 +    rm *.orig~~~
   5.109 +    cd .. 
   5.110    cd .. 
   5.111  cd Minisubpbl
   5.112    rm #*

     6.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Tue Jul 28 16:17:42 2020 +0200
     6.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Fri Jul 31 12:21:34 2020 +0200
     6.3 @@ -73,6 +73,12 @@
     6.4  (**)"~~/test/Tools/isac/ADDTESTS/session-get_theory/Foo"
     6.5  (*"ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
     6.6     ADDTESTS/------------------------------------------- see end of tests *)
     6.7 +(*/--- these work independently, but create problems here ..
     6.8 +  "~~/test/Pure/Isar/Keyword_ISAC.thy"           (* Malformed theory import, "keywords" ?!? *)
     6.9 +  "~~/test/Pure/Isar/Keywords_Diag.thy"          (* Malformed theory import, "keywords" ?!? *)
    6.10 +  "~~/test/Pure/Isar/Test_Parse_Isac.thy"        (* Malformed theory import, "keywords" ?!? *)
    6.11 +  "~~/test/Pure/Isar/Test_Parsers_Cookbook.thy"  (* Malformed theory import             ?!? *)
    6.12 +  \--- .. these work independently, but create problems here *)
    6.13  (**)"~~/test/Pure/Isar/Test_Parsers"
    6.14  (**)"~~/test/Pure/Isar/Test_Parse_Term"
    6.15  (*/---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------\*)