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