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