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