src/Pure/Isar/isar_syn.ML
author wenzelm
Fri Apr 30 18:06:35 1999 +0200 (1999-04-30 ago)
changeset 6551 de4047b03017
parent 6530 473305b71b74
child 6687 134df1440f6e
permissions -rw-r--r--
comment sections;
made "%" a keyword;
     1 (*  Title:      Pure/Isar/isar_syn.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Isar/Pure outer syntax.
     6 *)
     7 
     8 signature ISAR_SYN =
     9 sig
    10   val keywords: string list
    11   val parsers: OuterSyntax.parser list
    12 end;
    13 
    14 structure IsarSyn: ISAR_SYN =
    15 struct
    16 
    17 open OuterParse;
    18 
    19 
    20 (** init and exit **)
    21 
    22 val theoryP =
    23   OuterSyntax.command "theory" "begin theory"
    24     (OuterSyntax.theory_header >> (Toplevel.print oo IsarThy.theory));
    25 
    26 (*end current theory / sub-proof / excursion*)
    27 val endP =
    28   OuterSyntax.command "end" "end current block / theory / excursion"
    29     (Scan.succeed (Toplevel.print o Toplevel.exit o Toplevel.proof IsarThy.end_block));
    30 
    31 val contextP =
    32   OuterSyntax.improper_command "context" "switch theory context"
    33     (name >> (Toplevel.print oo IsarThy.context));
    34 
    35 val update_contextP =
    36   OuterSyntax.improper_command "update_context" "switch theory context, forcing update"
    37     (name >> (Toplevel.print oo IsarThy.update_context));
    38 
    39 
    40 
    41 (** theory sections **)
    42 
    43 (* formal comments *)
    44 
    45 val textP = OuterSyntax.command "text" "formal comments"
    46   (comment >> (Toplevel.theory o IsarThy.add_text));
    47 
    48 val titleP = OuterSyntax.command "title" "document title"
    49   ((comment -- Scan.optional comment Comment.empty -- Scan.optional comment Comment.empty)
    50     >> (fn ((x, y), z) => Toplevel.theory (IsarThy.add_title x y z)));
    51 
    52 val chapterP = OuterSyntax.command "chapter" "chapter heading"
    53   (comment >> (Toplevel.theory o IsarThy.add_chapter));
    54 
    55 val sectionP = OuterSyntax.command "section" "section heading"
    56   (comment >> (Toplevel.theory o IsarThy.add_section));
    57 
    58 val subsectionP = OuterSyntax.command "subsection" "subsection heading"
    59   (comment >> (Toplevel.theory o IsarThy.add_subsection));
    60 
    61 val subsubsectionP = OuterSyntax.command "subsubsection" "subsubsection heading"
    62   (comment >> (Toplevel.theory o IsarThy.add_subsubsection));
    63 
    64 
    65 (* classes and sorts *)
    66 
    67 val classesP =
    68   OuterSyntax.command "classes" "declare type classes"
    69     (Scan.repeat1 (name -- Scan.optional ($$$ "<" |-- !!! (list1 xname)) [])
    70       >> (Toplevel.theory o Theory.add_classes));
    71 
    72 val classrelP =
    73   OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)"
    74     (xname -- ($$$ "<" |-- !!! xname) >> (Toplevel.theory o Theory.add_classrel o single));
    75 
    76 val defaultsortP =
    77   OuterSyntax.command "defaultsort" "declare default sort"
    78     (sort >> (Toplevel.theory o Theory.add_defsort));
    79 
    80 
    81 (* types *)
    82 
    83 val typedeclP =
    84   OuterSyntax.command "typedecl" "Pure type declaration"
    85     (type_args -- name -- opt_infix
    86       >> (fn ((args, a), mx) => Toplevel.theory (PureThy.add_typedecls [(a, args, mx)])));
    87 
    88 val typeabbrP =
    89   OuterSyntax.command "types" "declare type abbreviations"
    90     (Scan.repeat1 (type_args -- name -- ($$$ "=" |-- !!! (typ -- opt_infix)))
    91       >> (Toplevel.theory o Theory.add_tyabbrs o
    92         map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
    93 
    94 val nontermP =
    95   OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
    96     (Scan.repeat1 name >> (Toplevel.theory o Theory.add_nonterminals));
    97 
    98 val aritiesP =
    99   OuterSyntax.command "arities" "state type arities (axiomatic!)"
   100     (Scan.repeat1 (xname -- ($$$ "::" |-- !!! arity) >> triple2)
   101       >> (Toplevel.theory o Theory.add_arities));
   102 
   103 
   104 (* consts and syntax *)
   105 
   106 val constsP =
   107   OuterSyntax.command "consts" "declare constants"
   108     (Scan.repeat1 const >> (Toplevel.theory o Theory.add_consts));
   109 
   110 val opt_mode =
   111   Scan.optional
   112     ($$$ "(" |-- !!! (name -- Scan.optional ($$$ "output" >> K false) true --| $$$ ")"))
   113     ("", true);
   114 
   115 val syntaxP =
   116   OuterSyntax.command "syntax" "declare syntactic constants"
   117     (opt_mode -- Scan.repeat1 const >> (Toplevel.theory o uncurry Theory.add_modesyntax));
   118 
   119 
   120 (* translations *)
   121 
   122 val trans_pat =
   123   Scan.optional ($$$ "(" |-- !!! (xname --| $$$ ")")) "logic" -- string;
   124 
   125 fun trans_arrow toks =
   126   ($$$ "=>" >> K Syntax.ParseRule ||
   127     $$$ "<=" >> K Syntax.PrintRule ||
   128     $$$ "==" >> K Syntax.ParsePrintRule) toks;
   129 
   130 val trans_line =
   131   trans_pat -- !!! (trans_arrow -- trans_pat)
   132     >> (fn (left, (arr, right)) => arr (left, right));
   133 
   134 val translationsP =
   135   OuterSyntax.command "translations" "declare syntax translation rules"
   136     (Scan.repeat1 trans_line >> (Toplevel.theory o Theory.add_trrules));
   137 
   138 
   139 (* axioms and definitions *)
   140 
   141 val axiomsP =
   142   OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)"
   143     (Scan.repeat1 spec_name >> (Toplevel.theory o IsarThy.add_axioms));
   144 
   145 val defsP =
   146   OuterSyntax.command "defs" "define constants"
   147     (Scan.repeat1 spec_opt_name >> (Toplevel.theory o IsarThy.add_defs));
   148 
   149 val constdefsP =
   150   OuterSyntax.command "constdefs" "declare and define constants"
   151     (Scan.repeat1 (const -- term) >> (Toplevel.theory o IsarThy.add_constdefs));
   152 
   153 
   154 (* theorems *)
   155 
   156 val facts = opt_thm_name "=" -- xthms1;
   157 
   158 val theoremsP =
   159   OuterSyntax.command "theorems" "define theorems"
   160     (facts >> (Toplevel.theory o IsarThy.have_theorems));
   161 
   162 val lemmasP =
   163   OuterSyntax.command "lemmas" "define lemmas"
   164     (facts >> (Toplevel.theory o IsarThy.have_lemmas));
   165 
   166 
   167 (* name space entry path *)
   168 
   169 val globalP =
   170   OuterSyntax.command "global" "disable prefixing of theory name"
   171     (Scan.succeed (Toplevel.theory PureThy.global_path));
   172 
   173 val localP =
   174   OuterSyntax.command "local" "enable prefixing of theory name"
   175     (Scan.succeed (Toplevel.theory PureThy.local_path));
   176 
   177 val pathP =
   178   OuterSyntax.command "path" "modify name-space entry path"
   179     (xname >> (Toplevel.theory o Theory.add_path));
   180 
   181 
   182 (* use ML text *)
   183 
   184 val useP =
   185   OuterSyntax.command "use" "eval ML text from file"
   186     (name >> IsarCmd.use);
   187 
   188 val mlP =
   189   OuterSyntax.command "ML" "eval ML text"
   190     (text >> (fn txt => IsarCmd.use_mltext txt o IsarCmd.use_mltext_theory txt));
   191 
   192 val setupP =
   193   OuterSyntax.command "setup" "apply ML theory transformer"
   194     (text >> (Toplevel.theory o IsarThy.use_setup));
   195 
   196 
   197 (* translation functions *)
   198 
   199 val parse_ast_translationP =
   200   OuterSyntax.command "parse_ast_translation" "install parse ast translation functions"
   201     (text >> (Toplevel.theory o IsarThy.parse_ast_translation));
   202 
   203 val parse_translationP =
   204   OuterSyntax.command "parse_translation" "install parse translation functions"
   205     (text >> (Toplevel.theory o IsarThy.parse_translation));
   206 
   207 val print_translationP =
   208   OuterSyntax.command "print_translation" "install print translation functions"
   209     (text >> (Toplevel.theory o IsarThy.print_translation));
   210 
   211 val typed_print_translationP =
   212   OuterSyntax.command "typed_print_translation" "install typed print translation functions"
   213     (text >> (Toplevel.theory o IsarThy.typed_print_translation));
   214 
   215 val print_ast_translationP =
   216   OuterSyntax.command "print_ast_translation" "install print ast translation functions"
   217     (text >> (Toplevel.theory o IsarThy.print_ast_translation));
   218 
   219 val token_translationP =
   220   OuterSyntax.command "token_translation" "install token translation functions"
   221     (text >> (Toplevel.theory o IsarThy.token_translation));
   222 
   223 
   224 (* oracles *)
   225 
   226 val oracleP =
   227   OuterSyntax.command "oracle" "install oracle"
   228     (name -- text >> (Toplevel.theory o IsarThy.add_oracle));
   229 
   230 
   231 
   232 (** proof commands **)
   233 
   234 (* statements *)
   235 
   236 val is_props = $$$ "(" |-- !!! (Scan.repeat1 ($$$ "is" |-- prop) --| $$$ ")");
   237 val propp = prop -- Scan.optional is_props [];
   238 fun statement f = opt_thm_name ":" -- propp >> (fn ((x, y), z) => f x y z);
   239 
   240 val theoremP =
   241   OuterSyntax.command "theorem" "state theorem"
   242     (statement IsarThy.theorem >> (fn f => Toplevel.print o Toplevel.theory_to_proof f));
   243 
   244 val lemmaP =
   245   OuterSyntax.command "lemma" "state lemma"
   246     (statement IsarThy.lemma >> (fn f => Toplevel.print o Toplevel.theory_to_proof f));
   247 
   248 val showP =
   249   OuterSyntax.command "show" "state local goal, solving current obligation"
   250     (statement IsarThy.show >> (fn f => Toplevel.print o Toplevel.proof f));
   251 
   252 val haveP =
   253   OuterSyntax.command "have" "state local goal"
   254     (statement IsarThy.have >> (fn f => Toplevel.print o Toplevel.proof f));
   255 
   256 val thusP =
   257   OuterSyntax.command "thus" "abbreviates \"then show\""
   258     (statement IsarThy.thus >> (fn f => Toplevel.print o Toplevel.proof f));
   259 
   260 val henceP =
   261   OuterSyntax.command "hence" "abbreviates \"then have\""
   262     (statement IsarThy.hence >> (fn f => Toplevel.print o Toplevel.proof f));
   263 
   264 
   265 (* facts *)
   266 
   267 val thenP =
   268   OuterSyntax.command "then" "forward chaining"
   269     (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.chain));
   270 
   271 val fromP =
   272   OuterSyntax.command "from" "forward chaining from given facts"
   273     (xthms1 >> (fn x => Toplevel.print o Toplevel.proof (IsarThy.from_facts x)));
   274 
   275 val factsP =
   276   OuterSyntax.command "note" "define facts"
   277     (facts >> (Toplevel.proof o IsarThy.have_facts));
   278 
   279 
   280 (* proof context *)
   281 
   282 val assumeP =
   283   OuterSyntax.command "assume" "assume propositions"
   284     (opt_thm_name ":" -- Scan.repeat1 propp >>
   285       (fn ((x, y), z) => Toplevel.print o Toplevel.proof (IsarThy.assume x y z)));
   286 
   287 val fixP =
   288   OuterSyntax.command "fix" "fix variables (Skolem constants)"
   289     (Scan.repeat1 (name -- Scan.option ($$$ "::" |-- typ))
   290       >> (fn xs => Toplevel.print o Toplevel.proof (IsarThy.fix xs)));
   291 
   292 val letP =
   293   OuterSyntax.command "let" "bind text variables"
   294     (and_list1 (enum1 "as" term -- ($$$ "=" |-- term))
   295       >> (fn bs => Toplevel.print o Toplevel.proof (IsarThy.match_bind bs)));
   296 
   297 
   298 (* proof structure *)
   299 
   300 val beginP =
   301   OuterSyntax.command "begin" "begin block"
   302     (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.begin_block));
   303 
   304 val nextP =
   305   OuterSyntax.command "next" "enter next block"
   306     (Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.next_block));
   307 
   308 
   309 (* end proof *)
   310 
   311 val kill_proofP =
   312   OuterSyntax.improper_command "kill" "abort current proof"
   313     (Scan.succeed (Toplevel.print o Toplevel.proof_to_theory IsarThy.kill_proof));
   314 
   315 val qed_withP =
   316   OuterSyntax.improper_command "qed_with" "conclude proof, may patch name and attributes"
   317     (Scan.option name -- Scan.option attribs -- Scan.option method
   318       >> (uncurry IsarThy.global_qed_with));
   319 
   320 val qedP =
   321   OuterSyntax.command "qed" "conclude (sub-)proof"
   322     (Scan.option method >> IsarThy.qed);
   323 
   324 val terminal_proofP =
   325   OuterSyntax.command "by" "terminal backward proof"
   326     (method >> IsarThy.terminal_proof)
   327 
   328 val immediate_proofP =
   329   OuterSyntax.command "." "immediate proof"
   330     (Scan.succeed IsarThy.immediate_proof);
   331 
   332 val default_proofP =
   333   OuterSyntax.command ".." "default proof"
   334     (Scan.succeed IsarThy.default_proof);
   335 
   336 
   337 (* proof steps *)
   338 
   339 val refineP =
   340   OuterSyntax.improper_command "refine" "unstructured backward proof step, ignoring facts"
   341     (method >> (Toplevel.print oo (Toplevel.proof o IsarThy.tac)));
   342 
   343 val then_refineP =
   344   OuterSyntax.improper_command "then_refine" "unstructured backward proof step, using facts"
   345     (method >> (Toplevel.print oo (Toplevel.proof o IsarThy.then_tac)));
   346 
   347 val proofP =
   348   OuterSyntax.command "proof" "backward proof"
   349     (Scan.option method >> (Toplevel.print oo (Toplevel.proof o IsarThy.proof)));
   350 
   351 
   352 (* proof history *)
   353 
   354 val clear_undoP =
   355   OuterSyntax.improper_command "clear_undo" "clear proof command undo information"
   356     (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.clear));
   357 
   358 val undoP =
   359   OuterSyntax.improper_command "undo" "undo proof command"
   360     (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.undo));
   361 
   362 val redoP =
   363   OuterSyntax.improper_command "redo" "redo proof command"
   364     (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.redo));
   365 
   366 val undosP =
   367   OuterSyntax.improper_command "undos" "undo proof commands"
   368     (nat >> (fn n => Toplevel.print o Toplevel.proof (ProofHistory.undos n)));
   369 
   370 val redosP =
   371   OuterSyntax.improper_command "redos" "redo proof commands"
   372     (nat >> (fn n => Toplevel.print o Toplevel.proof (ProofHistory.redos n)));
   373 
   374 val backP =
   375   OuterSyntax.improper_command "back" "backtracking of proof command"
   376     (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.back));
   377 
   378 val prevP =
   379   OuterSyntax.improper_command "prev" "previous proof state"
   380     (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.prev));
   381 
   382 val upP =
   383   OuterSyntax.improper_command "up" "upper proof state"
   384     (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.up));
   385 
   386 val topP =
   387   OuterSyntax.improper_command "top" "to initial proof state"
   388     (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.top));
   389 
   390 
   391 
   392 (** diagnostic commands (for interactive mode only) **)
   393 
   394 val print_commandsP =
   395   OuterSyntax.improper_command "help" "print outer syntax (global)"
   396     (Scan.succeed (Toplevel.imperative OuterSyntax.print_outer_syntax));
   397 
   398 val print_theoryP =
   399   OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)"
   400     (Scan.succeed IsarCmd.print_theory);
   401 
   402 val print_syntaxP =
   403   OuterSyntax.improper_command "print_syntax" "print inner syntax of theory (verbose!)"
   404     (Scan.succeed IsarCmd.print_syntax);
   405 
   406 val print_theoremsP =
   407   OuterSyntax.improper_command "print_theorems" "print theorems known in this theory"
   408     (Scan.succeed IsarCmd.print_theorems);
   409 
   410 val print_attributesP =
   411   OuterSyntax.improper_command "print_attributes" "print attributes known in this theory"
   412     (Scan.succeed IsarCmd.print_attributes);
   413 
   414 val print_methodsP =
   415   OuterSyntax.improper_command "print_methods" "print methods known in this theory"
   416     (Scan.succeed IsarCmd.print_methods);
   417 
   418 val print_bindsP =
   419   OuterSyntax.improper_command "print_binds" "print term bindings of proof context"
   420     (Scan.succeed IsarCmd.print_binds);
   421 
   422 val print_lthmsP =
   423   OuterSyntax.improper_command "print_facts" "print local theorems of proof context"
   424     (Scan.succeed IsarCmd.print_lthms);
   425 
   426 val print_thmsP =
   427   OuterSyntax.improper_command "thm" "print theorems" (xthm >> IsarCmd.print_thms);
   428 
   429 val print_propP =
   430   OuterSyntax.improper_command "prop" "read and print proposition"
   431     (term >> IsarCmd.print_prop);
   432 
   433 val print_termP =
   434   OuterSyntax.improper_command "term" "read and print term"
   435     (term >> IsarCmd.print_term);
   436 
   437 val print_typeP =
   438   OuterSyntax.improper_command "type" "read and print type"
   439     (typ >> IsarCmd.print_type);
   440 
   441 
   442 
   443 (** system commands (for interactive mode only) **)
   444 
   445 val cdP =
   446   OuterSyntax.improper_command "cd" "change current working directory"
   447     (name >> IsarCmd.cd);
   448 
   449 val pwdP =
   450   OuterSyntax.improper_command "pwd" "print current working directory"
   451     (Scan.succeed IsarCmd.pwd);
   452 
   453 val use_thyP =
   454   OuterSyntax.improper_command "use_thy" "use theory file"
   455     (name >> IsarCmd.use_thy);
   456 
   457 val update_thyP =
   458   OuterSyntax.improper_command "update_thy" "update theory file"
   459     (name >> IsarCmd.update_thy);
   460 
   461 val prP =
   462   OuterSyntax.improper_command "pr" "print current toplevel state"
   463     (Scan.succeed (Toplevel.print o Toplevel.imperative (K ())));
   464 
   465 
   466 val opt_unit = Scan.optional ($$$ "(" -- $$$ ")" >> (K ())) ();
   467 
   468 val commitP =
   469   OuterSyntax.improper_command "commit" "commit current session to ML database"
   470     (opt_unit >> (K IsarCmd.use_commit));
   471 
   472 val quitP =
   473   OuterSyntax.improper_command "quit" "quit Isabelle"
   474     (opt_unit >> (K IsarCmd.quit));
   475 
   476 val exitP =
   477   OuterSyntax.improper_command "exit" "exit Isar loop"
   478     (Scan.succeed IsarCmd.exit);
   479 
   480 val restartP =
   481   OuterSyntax.improper_command "restart" "restart Isar loop"
   482     (Scan.succeed IsarCmd.restart);
   483 
   484 val breakP =
   485   OuterSyntax.improper_command "break" "discontinue excursion (keep current state)"
   486     (Scan.succeed IsarCmd.break);
   487 
   488 
   489 
   490 (** the Pure outer syntax **)
   491 
   492 (*keep keywords consistent with the parsers, including those in
   493   outer_parse.ML, otherwise be prepared for unexpected errors*)
   494 
   495 val keywords =
   496  ["!", "%", "(", ")", "*", "+", ",", "--", ":", "::", ";", "<", "<=",
   497   "=", "==", "=>", "?", "[", "]", "and", "as", "binder", "files",
   498   "infixl", "infixr", "is", "output", "{", "|", "}"];
   499 
   500 val parsers = [
   501   (*theory structure*)
   502   theoryP, endP, contextP, update_contextP,
   503   (*theory sections*)
   504   textP, titleP, chapterP, sectionP, subsectionP, subsubsectionP,
   505   classesP, classrelP, defaultsortP, typedeclP, typeabbrP, nontermP,
   506   aritiesP, constsP, syntaxP, translationsP, axiomsP, defsP,
   507   constdefsP, theoremsP, lemmasP, globalP, localP, pathP, useP, mlP,
   508   setupP, parse_ast_translationP, parse_translationP,
   509   print_translationP, typed_print_translationP,
   510   print_ast_translationP, token_translationP, oracleP,
   511   (*proof commands*)
   512   theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, fixP, letP,
   513   thenP, fromP, factsP, beginP, nextP, kill_proofP, qed_withP, qedP,
   514   terminal_proofP, immediate_proofP, default_proofP, refineP,
   515   then_refineP, proofP, clear_undoP, undoP, redoP, undosP, redosP,
   516   backP, prevP, upP, topP,
   517   (*diagnostic commands*)
   518   print_commandsP, print_theoryP, print_syntaxP, print_attributesP,
   519   print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,
   520   print_thmsP, print_propP, print_termP, print_typeP,
   521   (*system commands*)
   522   cdP, pwdP, use_thyP, update_thyP, prP, commitP, quitP, exitP,
   523   restartP, breakP];
   524 
   525 
   526 end;
   527 
   528 
   529 (*install the Pure outer syntax*)
   530 OuterSyntax.add_keywords IsarSyn.keywords;
   531 OuterSyntax.add_parsers IsarSyn.parsers;