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