src/Pure/Isar/outer_syntax.ML
author wenzelm
Thu Jun 08 21:53:44 2000 +0200 (2000-06-08)
changeset 9056 8f78b2aea39e
parent 9036 d9e09ef531dd
child 9132 52286129faa5
permissions -rw-r--r--
prf_open/close;
     1 (*  Title:      Pure/Isar/outer_syntax.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 The global Isabelle/Isar outer syntax.
     7 *)
     8 
     9 signature BASIC_OUTER_SYNTAX =
    10 sig
    11   val main: unit -> unit
    12   val loop: unit -> unit
    13   val sync_main: unit -> unit
    14   val sync_loop: unit -> unit
    15   val help: unit -> unit
    16 end;
    17 
    18 signature OUTER_SYNTAX =
    19 sig
    20   include BASIC_OUTER_SYNTAX
    21   structure Keyword:
    22     sig
    23       val control: string
    24       val diag: string
    25       val thy_begin: string
    26       val thy_switch: string
    27       val thy_end: string
    28       val thy_heading: string
    29       val thy_decl: string
    30       val thy_goal: string
    31       val qed: string
    32       val qed_block: string
    33       val qed_global: string
    34       val prf_goal: string
    35       val prf_block: string
    36       val prf_open: string
    37       val prf_close: string
    38       val prf_chain: string
    39       val prf_decl: string
    40       val prf_asm: string
    41       val prf_asm_goal: string
    42       val prf_script: string
    43       val kinds: string list
    44     end
    45   type token
    46   type parser
    47   val command: string -> string -> string ->
    48     (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
    49   val markup_command: string -> string -> string ->
    50     (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
    51   val markup_env_command: string -> string -> string ->
    52     (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
    53   val verbatim_command: string -> string -> string ->
    54     (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
    55   val improper_command: string -> string -> string ->
    56     (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
    57   val dest_keywords: unit -> string list
    58   val dest_parsers: unit -> (string * string * string * bool) list
    59   val print_outer_syntax: unit -> unit
    60   val print_help: Toplevel.transition -> Toplevel.transition
    61   val add_keywords: string list -> unit
    62   val add_parsers: parser list -> unit
    63   val theory_header: token list -> (string * string list * (string * bool) list) * token list
    64   val deps_thy: string -> bool -> Path.T -> string list * Path.T list
    65   val load_thy: string -> bool -> bool -> Path.T -> unit
    66   val isar: bool -> bool -> Toplevel.isar
    67 end;
    68 
    69 structure OuterSyntax: OUTER_SYNTAX =
    70 struct
    71 
    72 structure T = OuterLex;
    73 structure P = OuterParse;
    74 
    75 
    76 (** outer syntax **)
    77 
    78 (* command keyword classification *)
    79 
    80 structure Keyword =
    81 struct
    82   val control = "control";
    83   val diag = "diag";
    84   val thy_begin = "theory-begin";
    85   val thy_switch = "theory-switch";
    86   val thy_end = "theory-end";
    87   val thy_heading = "theory-heading";
    88   val thy_decl = "theory-decl";
    89   val thy_goal = "theory-goal";
    90   val qed = "qed";
    91   val qed_block = "qed-block";
    92   val qed_global = "qed-global";
    93   val prf_goal = "proof-goal";
    94   val prf_block = "proof-block";
    95   val prf_open = "proof-open";
    96   val prf_close = "proof-close";
    97   val prf_chain = "proof-chain";
    98   val prf_decl = "proof-decl";
    99   val prf_asm = "proof-asm";
   100   val prf_asm_goal = "proof-asm-goal";
   101   val prf_script = "proof-script";
   102 
   103   val kinds = [control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_goal,
   104     qed, qed_block, qed_global, prf_goal, prf_block, prf_open, prf_close, prf_chain, prf_decl,
   105     prf_asm, prf_asm_goal, prf_script];
   106 end;
   107 
   108 
   109 (* parsers *)
   110 
   111 type token = T.token;
   112 type parser_fn = token list -> (Toplevel.transition -> Toplevel.transition) * token list;
   113 
   114 datatype markup_kind = Markup | MarkupEnv | Verbatim;
   115 
   116 datatype parser =
   117   Parser of string * (string * string * markup_kind option) * bool * parser_fn;
   118 
   119 fun parser int_only markup name comment kind parse =
   120   Parser (name, (comment, kind, markup), int_only, parse);
   121 
   122 
   123 (* parse command *)
   124 
   125 local
   126 
   127 fun command_body cmd (name, _) =
   128   (case cmd name of
   129     Some (int_only, parse) => P.!!! (Scan.prompt (name ^ "# ") (parse >> pair int_only))
   130   | None => sys_error ("no parser for outer syntax command " ^ quote name));
   131 
   132 fun terminator false = Scan.succeed ()
   133   | terminator true = P.group "end of input" (Scan.option P.sync -- P.$$$ ";" >> K ());
   134 
   135 in
   136 
   137 fun command term cmd =
   138   P.$$$ ";" >> K None ||
   139   P.sync >> K None ||
   140   (P.position P.command :-- command_body cmd) --| terminator term
   141     >> (fn ((name, pos), (int_only, f)) =>
   142       Some (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |>
   143         Toplevel.interactive int_only |> f));
   144 
   145 end;
   146 
   147 
   148 
   149 (** global syntax state **)
   150 
   151 local
   152 
   153 val global_lexicons = ref (Scan.empty_lexicon, Scan.empty_lexicon);
   154 val global_parsers =
   155   ref (Symtab.empty: (((string * string) * (bool * parser_fn)) * markup_kind option) Symtab.table);
   156 val global_markups = ref ([]: (string * markup_kind) list);
   157 
   158 fun change_lexicons f =
   159   let val lexs = f (! global_lexicons) in
   160     (case (op inter_string) (pairself Scan.dest_lexicon lexs) of
   161       [] => global_lexicons := lexs
   162     | bads => error ("Clash of outer syntax commands and keywords: " ^ commas_quote bads))
   163   end;
   164 
   165 fun get_markup (ms, (name, (_, Some m))) = (name, m) :: ms
   166   | get_markup (ms, _) = ms;
   167 
   168 fun make_markups () = global_markups := Symtab.foldl get_markup ([], ! global_parsers);
   169 fun change_parsers f = (global_parsers := f (! global_parsers); make_markups ());
   170 
   171 in
   172 
   173 
   174 (* get current syntax *)
   175 
   176 (*Note: the syntax for files is statically determined at the very
   177   beginning; for interactive processing it may change dynamically.*)
   178 
   179 fun get_lexicons () = ! global_lexicons;
   180 fun get_parsers () = ! global_parsers;
   181 fun get_parser () = apsome (#2 o #1) o curry Symtab.lookup (! global_parsers);
   182 
   183 fun lookup_markup name = assoc (! global_markups, name);
   184 fun is_markup kind name = (case lookup_markup name of Some k => k = kind | None => false);
   185 
   186 
   187 (* augment syntax *)
   188 
   189 fun add_keywords keywords = change_lexicons (apfst (fn lex =>
   190   (Scan.extend_lexicon lex (map Symbol.explode keywords))));
   191 
   192 fun add_parser (tab, Parser (name, (comment, kind, markup), int_only, parse)) =
   193  (if is_none (Symtab.lookup (tab, name)) then ()
   194   else warning ("Redefined outer syntax command " ^ quote name);
   195   Symtab.update ((name, (((comment, kind), (int_only, parse)), markup)), tab));
   196 
   197 fun add_parsers parsers =
   198   (change_parsers (fn tab => foldl add_parser (tab, parsers));
   199     change_lexicons (apsnd (fn lex => Scan.extend_lexicon lex
   200       (map (fn Parser (name, _, _, _) => Symbol.explode name) parsers))));
   201 
   202 end;
   203 
   204 
   205 (* print syntax *)
   206 
   207 fun dest_keywords () = Scan.dest_lexicon (#1 (get_lexicons ()));
   208 
   209 fun dest_parsers () =
   210   map (fn (name, (((cmt, kind), (int_only, _)), _)) => (name, cmt, kind, int_only))
   211     (Symtab.dest (get_parsers ()));
   212 
   213 fun help_outer_syntax () =
   214   let
   215     fun pretty_cmd (name, comment, _, _) =
   216       Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
   217     val (int_cmds, cmds) = partition #4 (dest_parsers ());
   218   in
   219     [Pretty.strs ("syntax keywords:" :: map quote (dest_keywords ())),
   220       Pretty.big_list "proper commands:" (map pretty_cmd cmds),
   221       Pretty.big_list "improper commands (interactive-only):" (map pretty_cmd int_cmds)]
   222   end;
   223 
   224 val print_outer_syntax = Pretty.writeln o Pretty.chunks o help_outer_syntax;
   225 
   226 val print_help =
   227   Toplevel.keep (fn state =>
   228     let val opt_thy = try Toplevel.theory_of state in
   229       help_outer_syntax () @
   230       Method.help_methods opt_thy @
   231       Attrib.help_attributes opt_thy
   232       |> Pretty.chunks |> Pretty.writeln
   233     end);
   234 
   235 
   236 
   237 (** read theory **)
   238 
   239 (* special keywords *)
   240 
   241 val headerN = "header";
   242 val theoryN = "theory";
   243 
   244 val theory_keyword = P.$$$ theoryN;
   245 val header_keyword = P.$$$ headerN;
   246 val semicolon = P.$$$ ";";
   247 
   248 
   249 (* sources *)
   250 
   251 local
   252 
   253 val no_terminator =
   254   Scan.unless semicolon (Scan.one (T.not_sync andf T.not_eof));
   255 
   256 val recover = Scan.prompt "recover# " (Scan.repeat no_terminator);
   257 
   258 in
   259 
   260 fun source term do_recover cmd src =
   261   src
   262   |> Source.source T.stopper
   263     (Scan.bulk (fn xs => P.!!! (command term (cmd ())) xs))
   264     (if do_recover then Some recover else None)
   265   |> Source.mapfilter I;
   266 
   267 end;
   268 
   269 fun token_source (src, pos) =
   270   src
   271   |> Symbol.source false
   272   |> T.source false (K (get_lexicons ())) pos;
   273 
   274 fun filter_proper src =
   275   src
   276   |> Source.filter T.is_proper;
   277 
   278 
   279 (* scan header *)
   280 
   281 fun scan_header get_lex scan (src, pos) =
   282   src
   283   |> Symbol.source false
   284   |> T.source false (fn () => (get_lex (), Scan.empty_lexicon)) pos
   285   |> filter_proper
   286   |> Source.source T.stopper (Scan.single scan) None
   287   |> (fst o the o Source.get_single);
   288 
   289 
   290 (* detect new/old header *)
   291 
   292 local
   293 
   294 val check_header_lexicon = Scan.make_lexicon [Symbol.explode headerN, Symbol.explode theoryN];
   295 val check_header = Scan.option (header_keyword || theory_keyword);
   296 
   297 in
   298 
   299 fun is_old_theory src = is_none (scan_header (K check_header_lexicon) check_header src);
   300 
   301 end;
   302 
   303 
   304 (* deps_thy --- inspect theory header *)
   305 
   306 local
   307 
   308 val header_lexicon =
   309   Scan.make_lexicon (map Symbol.explode ["(", ")", "+", ":", ";", "=", "files", headerN, theoryN]);
   310 
   311 val file_name =
   312   (P.$$$ "(" |-- P.!!! (P.name --| P.$$$ ")")) >> rpair false || P.name >> rpair true;
   313 
   314 in
   315 
   316 val theory_header =
   317   (P.name -- (P.$$$ "=" |-- P.enum1 "+" P.name) --
   318     Scan.optional (P.$$$ "files" |-- P.!!! (Scan.repeat1 file_name)) [] --|  P.$$$ ":")
   319   >> (fn ((A, Bs), files) => (A, Bs, files));
   320 
   321 val new_header =
   322   header_keyword |-- (P.!!! (P.text -- Scan.option semicolon -- theory_keyword |-- theory_header))
   323     || theory_keyword |-- P.!!! theory_header;
   324 
   325 val old_header =
   326   P.!!! (P.group "theory header"
   327     (P.name -- (P.$$$ "=" |-- P.name -- Scan.repeat (P.$$$ "+" |-- P.name))))
   328   >> (fn (A, (B, Bs)) => (A, B :: Bs, []: (string * bool) list));
   329 
   330 fun deps_thy name ml path =
   331   let
   332     val src = Source.of_string (File.read path);
   333     val pos = Path.position path;
   334     val (name', parents, files) =
   335       (*unfortunately, old-style headers dynamically depend on the current lexicon*)
   336       if is_old_theory (src, pos) then
   337         scan_header ThySyn.get_lexicon (Scan.error old_header) (src, pos)
   338       else scan_header (K header_lexicon) (Scan.error new_header) (src, pos);
   339 
   340     val ml_path = ThyLoad.ml_path name;
   341     val ml_file = if ml andalso is_some (ThyLoad.check_file ml_path) then [ml_path] else [];
   342   in
   343     if name <> name' then
   344       error ("Filename " ^ quote (Path.pack path) ^
   345         " does not agree with theory name " ^ quote name')
   346     else (parents, map (Path.unpack o #1) files @ ml_file)
   347   end;
   348 
   349 end;
   350 
   351 
   352 (* present theory source *)
   353 
   354 local
   355 
   356 val is_improper = not o (T.is_proper orf T.is_begin_ignore orf T.is_end_ignore);
   357 val improper = Scan.any is_improper;
   358 
   359 val improper_keep_indent = Scan.repeat
   360   (Scan.unless (Scan.one T.is_indent -- Scan.one T.is_proper) (Scan.one is_improper));
   361 
   362 val improper_end =
   363   (improper -- semicolon) |-- improper_keep_indent ||
   364   improper_keep_indent;
   365 
   366 
   367 val ignore =
   368   Scan.depend (fn d => Scan.one T.is_begin_ignore >> pair (d + 1)) ||
   369   Scan.depend (fn 0 => Scan.fail | d => Scan.one T.is_end_ignore >> pair (d - 1)) ||
   370   Scan.lift (Scan.one (OuterLex.not_eof andf (not o OuterLex.is_end_ignore)));
   371 
   372 val opt_newline = Scan.option (Scan.one T.is_newline);
   373 
   374 val ignore_stuff =
   375   opt_newline -- Scan.one T.is_begin_ignore --
   376     P.!!!! (Scan.pass 0 (Scan.repeat ignore) -- Scan.one T.is_end_ignore -- opt_newline);
   377 
   378 fun markup_kind k = Scan.one (T.is_kind T.Command andf is_markup k o T.val_of);
   379 
   380 val markup = markup_kind Markup >> T.val_of;
   381 val markup_env = markup_kind MarkupEnv >> T.val_of;
   382 val verbatim = markup_kind Verbatim;
   383 
   384 val present_token =
   385   ignore_stuff >> K None ||
   386   (improper |-- markup -- P.!!!! (improper |-- P.text --| improper_end) >> Present.markup_token ||
   387     improper |-- markup_env -- P.!!!! (improper |-- P.text --| improper_end) >> Present.markup_env_token ||
   388     (P.$$$ "--" >> K "cmt") -- P.!!!! (improper |-- P.text) >> Present.markup_token ||
   389     (improper -- verbatim) |-- P.!!!! (improper |-- P.text --| improper_end)
   390       >> Present.verbatim_token ||
   391     Scan.one T.not_eof >> Present.basic_token) >> Some;
   392 
   393 in
   394 
   395 (*note: lazy evaluation ahead*)
   396 
   397 fun present_toks text pos () =
   398   token_source (Source.of_list (Library.untabify text), pos)
   399   |> Source.source T.stopper (Scan.bulk (Scan.error present_token)) None
   400   |> Source.mapfilter I
   401   |> Source.exhaust;
   402 
   403 fun present_text text () =
   404   Source.exhaust (Symbol.source false (Source.of_list (Library.untabify text)));
   405 
   406 end;
   407 
   408 
   409 (* load_thy --- read text (including header) *)
   410 
   411 local
   412 
   413 fun try_ml_file name time =
   414   let
   415     val path = ThyLoad.ml_path name;
   416     val tr = Toplevel.imperative (fn () => ThyInfo.load_file time path);
   417     val tr_name = if time then "time_use" else "use";
   418   in
   419     if is_none (ThyLoad.check_file path) then ()
   420     else Toplevel.excursion_error [Toplevel.empty |> Toplevel.name tr_name |> tr]
   421   end;
   422 
   423 fun parse_thy src_pos =
   424   src_pos
   425   |> token_source
   426   |> filter_proper
   427   |> source false false (K (get_parser ()))
   428   |> Source.exhaust;
   429 
   430 fun run_thy name path =
   431   let
   432     val text = explode (File.read path);
   433     val src = Source.of_list text;
   434     val pos = Path.position path;
   435   in
   436     Present.init_theory name;
   437     Present.verbatim_source name (present_text text);
   438     if is_old_theory (src, pos) then (ThySyn.load_thy name text;
   439       Present.old_symbol_source name (present_text text))   (*note: text presented twice!*)
   440     else (Toplevel.excursion_error (parse_thy (src, pos));
   441       Present.token_source name (present_toks text pos))
   442   end;
   443 
   444 in
   445 
   446 fun load_thy name ml time path =
   447  (if time then
   448     timeit (fn () =>
   449      (writeln ("\n**** Starting theory " ^ quote name ^ " ****");
   450       run_thy name path;
   451       writeln ("**** Finished theory " ^ quote name ^ " ****\n")))
   452   else run_thy name path;
   453   Context.context (ThyInfo.get_theory name);
   454   if ml then try_ml_file name time else ());
   455 
   456 end;
   457 
   458 
   459 (* interactive source of state transformers *)
   460 
   461 fun isar term no_pos =
   462   Source.tty
   463   |> Symbol.source true
   464   |> T.source true get_lexicons
   465     (if no_pos then Position.none else Position.line_name 1 "stdin")
   466   |> filter_proper
   467   |> source term true get_parser;
   468 
   469 
   470 
   471 (** the read-eval-print loop **)
   472 
   473 (* main loop *)
   474 
   475 fun gen_loop term no_pos =
   476  (Context.reset_context ();
   477   Toplevel.loop (isar term no_pos));
   478 
   479 fun gen_main term no_pos =
   480  (Toplevel.set_state Toplevel.toplevel;
   481   writeln (Session.welcome ());
   482   gen_loop term no_pos);
   483 
   484 fun main () = gen_main false false;
   485 fun loop () = gen_loop false false;
   486 fun sync_main () = gen_main true true;
   487 fun sync_loop () = gen_loop true true;
   488 
   489 
   490 (* help *)
   491 
   492 fun help () =
   493   writeln ("This is Isabelle's underlying ML system (" ^ ml_system ^ ");\n\
   494     \invoke 'loop();' to enter the Isar loop.");
   495 
   496 
   497 (*final declarations of this structure!*)
   498 val command = parser false None;
   499 val markup_command = parser false (Some Markup);
   500 val markup_env_command = parser false (Some MarkupEnv);
   501 val verbatim_command = parser false (Some Verbatim);
   502 val improper_command = parser true None;
   503 
   504 
   505 end;
   506 
   507 (*setup theory syntax dependent operations*)
   508 ThyLoad.deps_thy_fn := OuterSyntax.deps_thy;
   509 ThyLoad.load_thy_fn := OuterSyntax.load_thy;
   510 structure ThyLoad: THY_LOAD = ThyLoad;
   511 
   512 structure BasicOuterSyntax: BASIC_OUTER_SYNTAX = OuterSyntax;
   513 open BasicOuterSyntax;