src/HOL/Eisbach/parse_tools.ML
author wenzelm
Fri Oct 27 13:50:08 2017 +0200 (23 months ago)
changeset 66924 b4d4027f743b
parent 63185 08369e33c185
permissions -rw-r--r--
more permissive;
wenzelm@60248
     1
(*  Title:      HOL/Eisbach/parse_tools.ML
wenzelm@60119
     2
    Author:     Daniel Matichuk, NICTA/UNSW
wenzelm@60119
     3
wenzelm@60119
     4
Simple tools for deferred stateful token values.
wenzelm@60119
     5
*)
wenzelm@60119
     6
wenzelm@60119
     7
signature PARSE_TOOLS =
wenzelm@60119
     8
sig
wenzelm@60119
     9
  datatype ('a, 'b) parse_val =
wenzelm@60119
    10
    Real_Val of 'a
wenzelm@60285
    11
  | Parse_Val of 'b * ('a -> unit);
wenzelm@60119
    12
wenzelm@60119
    13
  val is_real_val : ('a, 'b) parse_val -> bool
wenzelm@60119
    14
wenzelm@60119
    15
  val the_real_val : ('a, 'b) parse_val -> 'a
wenzelm@60119
    16
  val the_parse_val : ('a, 'b) parse_val -> 'b
wenzelm@60119
    17
  val the_parse_fun : ('a, 'b) parse_val -> ('a -> unit)
wenzelm@60285
    18
wenzelm@60285
    19
  val parse_val_cases: ('b -> 'a) -> ('a, 'b) parse_val -> ('a * ('a -> unit))
wenzelm@60285
    20
wenzelm@60285
    21
  val parse_term_val : 'b parser -> (term, 'b) parse_val parser
wenzelm@60285
    22
  val name_term : (term, string) parse_val parser
daniel@63185
    23
daniel@63185
    24
  val parse_thm_val : 'b parser -> (thm, 'b) parse_val parser
wenzelm@60119
    25
end;
wenzelm@60119
    26
wenzelm@60119
    27
structure Parse_Tools: PARSE_TOOLS =
wenzelm@60119
    28
struct
wenzelm@60119
    29
wenzelm@60119
    30
datatype ('a, 'b) parse_val =
wenzelm@60119
    31
  Real_Val of 'a
wenzelm@60119
    32
| Parse_Val of 'b * ('a -> unit);
wenzelm@60119
    33
wenzelm@60119
    34
fun parse_term_val scan =
wenzelm@60119
    35
  Scan.ahead Parse.not_eof -- Scan.ahead (Scan.option Args.internal_term) -- scan >>
wenzelm@60119
    36
    (fn ((_, SOME t), _) => Real_Val t
wenzelm@61814
    37
      | ((tok, NONE), v) => Parse_Val (v, fn t => ignore (Token.assign (SOME (Token.Term t)) tok)));
wenzelm@60119
    38
wenzelm@63120
    39
val name_term = parse_term_val Args.embedded_inner_syntax;
wenzelm@60119
    40
daniel@63185
    41
fun parse_thm_val scan =
daniel@63185
    42
  Scan.ahead Parse.not_eof -- Scan.ahead (Scan.option (Args.internal_fact >> the_single)) -- scan >>
daniel@63185
    43
    (fn ((_, SOME t), _) => Real_Val t
daniel@63185
    44
      | ((tok, NONE), v) => Parse_Val (v, fn t => ignore (Token.assign (SOME (Token.Fact (NONE, [t]))) tok)));
daniel@63185
    45
wenzelm@60119
    46
fun is_real_val (Real_Val _) = true
wenzelm@60119
    47
  | is_real_val _ = false;
wenzelm@60119
    48
wenzelm@60119
    49
fun the_real_val (Real_Val t) = t
wenzelm@60119
    50
  | the_real_val _ = raise Fail "Expected close parsed value";
wenzelm@60119
    51
wenzelm@60119
    52
fun the_parse_val (Parse_Val (b, _)) = b
wenzelm@60119
    53
  | the_parse_val _ = raise Fail "Expected open parsed value";
wenzelm@60119
    54
wenzelm@60119
    55
fun the_parse_fun (Parse_Val (_, f)) = f
wenzelm@60119
    56
  | the_parse_fun _ = raise Fail "Expected open parsed value";
wenzelm@60119
    57
wenzelm@60285
    58
fun parse_val_cases g (Parse_Val (b, f)) = (g b, f)
wenzelm@60285
    59
  | parse_val_cases _ (Real_Val v) = (v, K ());
wenzelm@60285
    60
wenzelm@60119
    61
end;