src/Pure/ProofGeneral/pgip_parser.ML
author haftmann
Tue Oct 20 16:13:01 2009 +0200 (2009-10-20)
changeset 33037 b22e44496dc2
parent 32466 a393b7e2a2f8
child 33038 8f9594c31de4
permissions -rw-r--r--
replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
     1 (*  Title:      Pure/ProofGeneral/pgip_parser.ML
     2     Author:     David Aspinall and Makarius
     3 
     4 Parsing theory sources without execution (via keyword classification).
     5 *)
     6 
     7 signature PGIP_PARSER =
     8 sig
     9   val pgip_parser: Position.T -> string -> PgipMarkup.pgipdocument
    10 end
    11 
    12 structure PgipParser: PGIP_PARSER =
    13 struct
    14 
    15 structure K = OuterKeyword;
    16 structure D = PgipMarkup;
    17 structure I = PgipIsabelle;
    18 
    19 
    20 fun badcmd text = [D.Badcmd {text = text}];
    21 
    22 fun thy_begin text =
    23   (case try (Thy_Header.read Position.none) (Source.of_string text) of
    24     NONE => D.Opentheory {thyname = NONE, parentnames = [], text = text}
    25   | SOME (name, imports, _) =>
    26        D.Opentheory {thyname = SOME name, parentnames = imports, text = text})
    27   :: [D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjTheoryBody}];
    28 
    29 fun thy_heading text =
    30   [D.Closeblock {},
    31    D.Doccomment {text = text},
    32    D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjTheoryBody}];
    33 
    34 fun thy_decl text =
    35   [D.Theoryitem {name = NONE, objtype = SOME I.ObjTheoryDecl, text = text}];
    36 
    37 fun goal text =
    38   [D.Opengoal {thmname = NONE, text = text},
    39    D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjProofBody}];
    40 
    41 fun prf_block text =
    42   [D.Closeblock {},
    43    D.Proofstep {text = text},
    44    D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjProofBody}];
    45 
    46 fun prf_open text =
    47  [D.Openblock {metavarid = NONE, name = NONE, objtype = SOME I.ObjProofBody},
    48   D.Proofstep {text = text}];
    49 
    50 fun proofstep text = [D.Proofstep {text = text}];
    51 fun closegoal text = [D.Closegoal {text = text}, D.Closeblock {}];
    52 
    53 
    54 fun command k f = Symtab.update_new (OuterKeyword.kind_of k, f);
    55 
    56 val command_keywords = Symtab.empty
    57   |> command K.control          badcmd
    58   |> command K.diag             (fn text => [D.Spuriouscmd {text = text}])
    59   |> command K.thy_begin        thy_begin
    60   |> command K.thy_switch       badcmd
    61   |> command K.thy_end          (fn text => [D.Closeblock {}, D.Closetheory {text = text}])
    62   |> command K.thy_heading      thy_heading
    63   |> command K.thy_decl         thy_decl
    64   |> command K.thy_script       thy_decl
    65   |> command K.thy_goal         goal
    66   |> command K.qed              closegoal
    67   |> command K.qed_block        closegoal
    68   |> command K.qed_global       (fn text => [D.Giveupgoal {text = text}])
    69   |> command K.prf_heading      (fn text => [D.Doccomment {text = text}])
    70   |> command K.prf_goal         goal
    71   |> command K.prf_block        prf_block
    72   |> command K.prf_open         prf_open
    73   |> command K.prf_close        (fn text => [D.Proofstep {text = text}, D.Closeblock {}])
    74   |> command K.prf_chain        proofstep
    75   |> command K.prf_decl         proofstep
    76   |> command K.prf_asm          proofstep
    77   |> command K.prf_asm_goal     goal
    78   |> command K.prf_script       proofstep;
    79 
    80 val _ = gen_subset (op =) (OuterKeyword.kinds, Symtab.keys command_keywords)
    81   orelse sys_error "Incomplete coverage of command keywords";
    82 
    83 fun parse_command "sorry" text = [D.Postponegoal {text = text}, D.Closeblock {}]
    84   | parse_command name text =
    85       (case OuterKeyword.command_keyword name of
    86         NONE => [D.Unparseable {text = text}]
    87       | SOME k =>
    88           (case Symtab.lookup command_keywords (OuterKeyword.kind_of k) of
    89             NONE => [D.Unparseable {text = text}]
    90           | SOME f => f text));
    91 
    92 fun parse_span span =
    93   let
    94     val kind = ThySyntax.span_kind span;
    95     val toks = ThySyntax.span_content span;
    96     val text = implode (map (PrintMode.setmp [] ThySyntax.present_token) toks);
    97   in
    98     (case kind of
    99       ThySyntax.Command name => parse_command name text
   100     | ThySyntax.Ignored => [D.Whitespace {text = text}]
   101     | ThySyntax.Malformed => [D.Unparseable {text = text}])
   102   end;
   103 
   104 
   105 fun pgip_parser pos str =
   106   maps parse_span (ThySyntax.parse_spans (OuterKeyword.get_lexicons ()) pos str);
   107 
   108 end;