--- a/src/Pure/Isar/isar_syn.ML Wed Mar 17 13:33:13 1999 +0100
+++ b/src/Pure/Isar/isar_syn.ML Wed Mar 17 13:34:49 1999 +0100
@@ -5,16 +5,11 @@
Isar/Pure outer syntax.
TODO:
+ - '--' (comment) option almost everywhere:
- add_parsers: warn if command name coincides with other keyword (if
not already present) (!?);
- - constdefs;
- - axclass axioms: attribs;
- - instance: theory_to_proof (with special attribute to add result arity);
- - witness: eliminate (!);
- - result (interactive): print current result (?);
+ - 'result' (interactive): print current result (?);
- check evaluation of transformers (exns!);
- - 'result' command;
- - '--' (comment) option almost everywhere:
- 'thms': xthms1 (vs. 'thm' (!?));
*)
@@ -33,20 +28,20 @@
(** init and exit **)
val theoryP =
- OuterSyntax.parser false "theory" "begin theory"
+ OuterSyntax.command "theory" "begin theory"
(OuterSyntax.theory_header >> (Toplevel.print oo IsarThy.theory));
(*end current theory / sub-proof / excursion*)
val endP =
- OuterSyntax.parser false "end" "end current theory / sub-proof / excursion"
+ OuterSyntax.command "end" "end current theory / sub-proof / excursion"
(Scan.succeed (Toplevel.print o Toplevel.exit o Toplevel.proof IsarThy.end_block));
val contextP =
- OuterSyntax.parser true "context" "switch theory context"
+ OuterSyntax.improper_command "context" "switch theory context"
(name >> (Toplevel.print oo IsarThy.context));
val update_contextP =
- OuterSyntax.parser true "update_context" "switch theory context, forcing update"
+ OuterSyntax.improper_command "update_context" "switch theory context, forcing update"
(name >> (Toplevel.print oo IsarThy.update_context));
@@ -55,61 +50,61 @@
(* formal comments *)
-val textP = OuterSyntax.parser false "text" "formal comments"
+val textP = OuterSyntax.command "text" "formal comments"
(text >> (Toplevel.theory o IsarThy.add_text));
-val titleP = OuterSyntax.parser false "title" "document title"
+val titleP = OuterSyntax.command "title" "document title"
((text -- Scan.optional text "" -- Scan.optional text "")
>> (fn ((x, y), z) => Toplevel.theory (IsarThy.add_title x y z)));
-val chapterP = OuterSyntax.parser false "chapter" "chapter heading"
+val chapterP = OuterSyntax.command "chapter" "chapter heading"
(text >> (Toplevel.theory o IsarThy.add_chapter));
-val sectionP = OuterSyntax.parser false "section" "section heading"
+val sectionP = OuterSyntax.command "section" "section heading"
(text >> (Toplevel.theory o IsarThy.add_section));
-val subsectionP = OuterSyntax.parser false "subsection" "subsection heading"
+val subsectionP = OuterSyntax.command "subsection" "subsection heading"
(text >> (Toplevel.theory o IsarThy.add_subsection));
-val subsubsectionP = OuterSyntax.parser false "subsubsection" "subsubsection heading"
+val subsubsectionP = OuterSyntax.command "subsubsection" "subsubsection heading"
(text >> (Toplevel.theory o IsarThy.add_subsubsection));
(* classes and sorts *)
val classesP =
- OuterSyntax.parser false "classes" "declare type classes"
+ OuterSyntax.command "classes" "declare type classes"
(Scan.repeat1 (name -- Scan.optional ($$$ "<" |-- !!! (list1 xname)) [])
>> (Toplevel.theory o Theory.add_classes));
val classrelP =
- OuterSyntax.parser false "classrel" "state inclusion of type classes (axiomatic!)"
+ OuterSyntax.command "classrel" "state inclusion of type classes (axiomatic!)"
(xname -- ($$$ "<" |-- !!! xname) >> (Toplevel.theory o Theory.add_classrel o single));
val defaultsortP =
- OuterSyntax.parser false "defaultsort" "declare default sort"
+ OuterSyntax.command "defaultsort" "declare default sort"
(sort >> (Toplevel.theory o Theory.add_defsort));
(* types *)
val typedeclP =
- OuterSyntax.parser false "typedecl" "Pure type declaration"
+ OuterSyntax.command "typedecl" "Pure type declaration"
(type_args -- name -- opt_infix
>> (fn ((args, a), mx) => Toplevel.theory (PureThy.add_typedecls [(a, args, mx)])));
val typeabbrP =
- OuterSyntax.parser false "types" "declare type abbreviations"
+ OuterSyntax.command "types" "declare type abbreviations"
(Scan.repeat1 (type_args -- name -- ($$$ "=" |-- !!! (typ -- opt_infix)))
>> (Toplevel.theory o Theory.add_tyabbrs o
map (fn ((args, a), (T, mx)) => (a, args, T, mx))));
val nontermP =
- OuterSyntax.parser false "nonterminals" "declare types treated as grammar nonterminal symbols"
+ OuterSyntax.command "nonterminals" "declare types treated as grammar nonterminal symbols"
(Scan.repeat1 name >> (Toplevel.theory o Theory.add_nonterminals));
val aritiesP =
- OuterSyntax.parser false "arities" "state type arities (axiomatic!)"
+ OuterSyntax.command "arities" "state type arities (axiomatic!)"
(Scan.repeat1 (xname -- ($$$ "::" |-- !!! arity) >> triple2)
>> (Toplevel.theory o Theory.add_arities));
@@ -117,7 +112,7 @@
(* consts and syntax *)
val constsP =
- OuterSyntax.parser false "consts" "declare constants"
+ OuterSyntax.command "consts" "declare constants"
(Scan.repeat1 const >> (Toplevel.theory o Theory.add_consts));
val opt_mode =
@@ -126,7 +121,7 @@
("", true);
val syntaxP =
- OuterSyntax.parser false "syntax" "declare syntactic constants"
+ OuterSyntax.command "syntax" "declare syntactic constants"
(opt_mode -- Scan.repeat1 const >> (Toplevel.theory o uncurry Theory.add_modesyntax));
@@ -145,22 +140,23 @@
>> (fn (left, (arr, right)) => arr (left, right));
val translationsP =
- OuterSyntax.parser false "translations" "declare syntax translation rules"
+ OuterSyntax.command "translations" "declare syntax translation rules"
(Scan.repeat1 trans_line >> (Toplevel.theory o Theory.add_trrules));
(* axioms and definitions *)
-val spec = thm_name ":" -- prop >> (fn ((x, y), z) => ((x, z), y));
-val spec' = opt_thm_name ":" -- prop >> (fn ((x, y), z) => ((x, z), y));
-
val axiomsP =
- OuterSyntax.parser false "axioms" "state arbitrary propositions (axiomatic!)"
- (Scan.repeat1 spec >> (Toplevel.theory o IsarThy.add_axioms));
+ OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)"
+ (Scan.repeat1 spec_name >> (Toplevel.theory o IsarThy.add_axioms));
val defsP =
- OuterSyntax.parser false "defs" "define constants"
- (Scan.repeat1 spec' >> (Toplevel.theory o IsarThy.add_defs));
+ OuterSyntax.command "defs" "define constants"
+ (Scan.repeat1 spec_opt_name >> (Toplevel.theory o IsarThy.add_defs));
+
+val constdefsP =
+ OuterSyntax.command "constdefs" "declare and define constants"
+ (Scan.repeat1 (const -- term) >> (Toplevel.theory o IsarThy.add_constdefs));
(* theorems *)
@@ -168,95 +164,75 @@
val facts = opt_thm_name "=" -- xthms1;
val theoremsP =
- OuterSyntax.parser false "theorems" "define theorems"
+ OuterSyntax.command "theorems" "define theorems"
(facts >> (Toplevel.theory o IsarThy.have_theorems));
val lemmasP =
- OuterSyntax.parser false "lemmas" "define lemmas"
+ OuterSyntax.command "lemmas" "define lemmas"
(facts >> (Toplevel.theory o IsarThy.have_lemmas));
-(* axclass *)
-
-val axclassP =
- OuterSyntax.parser false "axclass" "define axiomatic type class"
- (name -- Scan.optional ($$$ "<" |-- !!! (list1 xname)) [] -- Scan.repeat (spec >> fst)
- >> (Toplevel.theory o uncurry AxClass.add_axclass));
-
-
-(* instance *)
-
-val opt_witness =
- Scan.optional ($$$ "(" |-- !!! (list1 xname --| $$$ ")")) [];
-
-val instanceP =
- OuterSyntax.parser false "instance" "prove type arity"
- ((xname -- ($$$ "<" |-- xname) >> AxClass.add_inst_subclass ||
- xname -- ($$$ "::" |-- arity) >> (AxClass.add_inst_arity o triple2))
- -- opt_witness >> (fn (f, x) => Toplevel.theory (f x [] None)));
-
-
(* name space entry path *)
val globalP =
- OuterSyntax.parser false "global" "disable prefixing of theory name"
+ OuterSyntax.command "global" "disable prefixing of theory name"
(Scan.succeed (Toplevel.theory PureThy.global_path));
val localP =
- OuterSyntax.parser false "local" "enable prefixing of theory name"
+ OuterSyntax.command "local" "enable prefixing of theory name"
(Scan.succeed (Toplevel.theory PureThy.local_path));
val pathP =
- OuterSyntax.parser false "path" "modify name-space entry path"
+ OuterSyntax.command "path" "modify name-space entry path"
(xname >> (Toplevel.theory o Theory.add_path));
(* use ML text *)
val useP =
- OuterSyntax.parser false "use" "eval ML text from file"
+ OuterSyntax.command "use" "eval ML text from file"
(name >> IsarCmd.use);
val mlP =
- OuterSyntax.parser false "ML" "eval ML text"
+ OuterSyntax.command "ML" "eval ML text"
(text >> (fn txt => IsarCmd.use_mltext txt o IsarCmd.use_mltext_theory txt));
val setupP =
- OuterSyntax.parser false "setup" "apply ML theory transformer"
+ OuterSyntax.command "setup" "apply ML theory transformer"
(text >> (Toplevel.theory o IsarThy.use_setup));
(* translation functions *)
val parse_ast_translationP =
- OuterSyntax.parser false "parse_ast_translation" "install parse ast translation functions"
+ OuterSyntax.command "parse_ast_translation" "install parse ast translation functions"
(text >> (Toplevel.theory o IsarThy.parse_ast_translation));
val parse_translationP =
- OuterSyntax.parser false "parse_translation" "install parse translation functions"
+ OuterSyntax.command "parse_translation" "install parse translation functions"
(text >> (Toplevel.theory o IsarThy.parse_translation));
val print_translationP =
- OuterSyntax.parser false "print_translation" "install print translation functions"
+ OuterSyntax.command "print_translation" "install print translation functions"
(text >> (Toplevel.theory o IsarThy.print_translation));
val typed_print_translationP =
- OuterSyntax.parser false "typed_print_translation" "install typed print translation functions"
+ OuterSyntax.command "typed_print_translation" "install typed print translation functions"
(text >> (Toplevel.theory o IsarThy.typed_print_translation));
val print_ast_translationP =
- OuterSyntax.parser false "print_ast_translation" "install print ast translation functions"
+ OuterSyntax.command "print_ast_translation" "install print ast translation functions"
(text >> (Toplevel.theory o IsarThy.print_ast_translation));
val token_translationP =
- OuterSyntax.parser false "token_translation" "install token translation functions"
+ OuterSyntax.command "token_translation" "install token translation functions"
(text >> (Toplevel.theory o IsarThy.token_translation));
(* oracles *)
val oracleP =
- OuterSyntax.parser false "oracle" "install oracle"
+ OuterSyntax.command "oracle" "install oracle"
(name -- text >> (Toplevel.theory o IsarThy.add_oracle));
@@ -270,51 +246,51 @@
fun statement f = opt_thm_name ":" -- propp >> (fn ((x, y), z) => f x y z);
val theoremP =
- OuterSyntax.parser false "theorem" "state theorem"
+ OuterSyntax.command "theorem" "state theorem"
(statement IsarThy.theorem >> (fn f => Toplevel.print o Toplevel.theory_to_proof f));
val lemmaP =
- OuterSyntax.parser false "lemma" "state lemma"
+ OuterSyntax.command "lemma" "state lemma"
(statement IsarThy.lemma >> (fn f => Toplevel.print o Toplevel.theory_to_proof f));
val showP =
- OuterSyntax.parser false "show" "state local goal, solving current obligation"
+ OuterSyntax.command "show" "state local goal, solving current obligation"
(statement IsarThy.show >> (fn f => Toplevel.print o Toplevel.proof f));
val haveP =
- OuterSyntax.parser false "have" "state local goal"
+ OuterSyntax.command "have" "state local goal"
(statement IsarThy.have >> (fn f => Toplevel.print o Toplevel.proof f));
(* facts *)
val thenP =
- OuterSyntax.parser false "then" "forward chaining"
+ OuterSyntax.command "then" "forward chaining"
(Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.chain));
val fromP =
- OuterSyntax.parser false "from" "forward chaining from given facts"
+ OuterSyntax.command "from" "forward chaining from given facts"
(xthms1 >> (fn x => Toplevel.print o Toplevel.proof (IsarThy.from_facts x)));
val factsP =
- OuterSyntax.parser false "note" "define facts"
+ OuterSyntax.command "note" "define facts"
(facts >> (Toplevel.proof o IsarThy.have_facts));
(* proof context *)
val assumeP =
- OuterSyntax.parser false "assume" "assume propositions"
- (opt_thm_name ":" -- and_list1 propp >>
+ OuterSyntax.command "assume" "assume propositions"
+ (opt_thm_name ":" -- Scan.repeat1 propp >>
(fn ((x, y), z) => Toplevel.print o Toplevel.proof (IsarThy.assume x y z)));
val fixP =
- OuterSyntax.parser false "fix" "fix variables (Skolem constants)"
- (and_list1 (name -- Scan.option ($$$ "::" |-- typ))
+ OuterSyntax.command "fix" "fix variables (Skolem constants)"
+ (Scan.repeat1 (name -- Scan.option ($$$ "::" |-- typ))
>> (fn xs => Toplevel.print o Toplevel.proof (IsarThy.fix xs)));
val letP =
- OuterSyntax.parser false "let" "bind text variables"
+ OuterSyntax.command "let" "bind text variables"
(and_list1 (enum1 "as" term -- ($$$ "=" |-- term))
>> (fn bs => Toplevel.print o Toplevel.proof (IsarThy.match_bind bs)));
@@ -322,26 +298,26 @@
(* proof structure *)
val beginP =
- OuterSyntax.parser false "begin" "begin block"
+ OuterSyntax.command "begin" "begin block"
(Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.begin_block));
val nextP =
- OuterSyntax.parser false "next" "enter next block"
+ OuterSyntax.command "next" "enter next block"
(Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.next_block));
(* end proof *)
val qedP =
- OuterSyntax.parser false "qed" "conclude proof"
+ OuterSyntax.command "qed" "conclude proof"
(Scan.succeed (Toplevel.proof_to_theory IsarThy.qed));
val qed_withP =
- OuterSyntax.parser true "qed_with" "conclude proof, may patch name and attributes"
+ OuterSyntax.improper_command "qed_with" "conclude proof, may patch name and attributes"
(Scan.option name -- Scan.option attribs >> (Toplevel.proof_to_theory o IsarThy.qed_with));
val kill_proofP =
- OuterSyntax.parser true "kill" "abort current proof"
+ OuterSyntax.improper_command "kill" "abort current proof"
(Scan.succeed (Toplevel.print o Toplevel.proof_to_theory IsarThy.kill_proof));
@@ -362,50 +338,50 @@
val terminal_proofP = stepP false "by" "terminal backward proof" IsarThy.terminal_proof;
val immediate_proofP =
- OuterSyntax.parser false "." "immediate proof"
+ OuterSyntax.command "." "immediate proof"
(Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.immediate_proof));
val default_proofP =
- OuterSyntax.parser false ".." "default proof"
+ OuterSyntax.command ".." "default proof"
(Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.default_proof));
(* proof history *)
val clear_undoP =
- OuterSyntax.parser true "clear_undo" "clear proof command undo information"
+ OuterSyntax.improper_command "clear_undo" "clear proof command undo information"
(Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.clear));
val undoP =
- OuterSyntax.parser true "undo" "undo proof command"
+ OuterSyntax.improper_command "undo" "undo proof command"
(Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.undo));
val redoP =
- OuterSyntax.parser true "redo" "redo proof command"
+ OuterSyntax.improper_command "redo" "redo proof command"
(Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.redo));
val undosP =
- OuterSyntax.parser true "undos" "undo proof commands"
+ OuterSyntax.improper_command "undos" "undo proof commands"
(nat >> (fn n => Toplevel.print o Toplevel.proof (ProofHistory.undos n)));
val redosP =
- OuterSyntax.parser true "redos" "redo proof commands"
+ OuterSyntax.improper_command "redos" "redo proof commands"
(nat >> (fn n => Toplevel.print o Toplevel.proof (ProofHistory.redos n)));
val backP =
- OuterSyntax.parser true "back" "backtracking of proof command"
+ OuterSyntax.improper_command "back" "backtracking of proof command"
(Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.back));
val prevP =
- OuterSyntax.parser true "prev" "previous proof state"
+ OuterSyntax.improper_command "prev" "previous proof state"
(Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.prev));
val upP =
- OuterSyntax.parser true "up" "upper proof state"
+ OuterSyntax.improper_command "up" "upper proof state"
(Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.up));
val topP =
- OuterSyntax.parser true "top" "to initial proof state"
+ OuterSyntax.improper_command "top" "to initial proof state"
(Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.top));
@@ -413,50 +389,50 @@
(** diagnostic commands (for interactive mode only) **)
val print_commandsP =
- OuterSyntax.parser true "help" "print outer syntax (global)"
+ OuterSyntax.improper_command "help" "print outer syntax (global)"
(Scan.succeed (Toplevel.imperative OuterSyntax.print_outer_syntax));
val print_theoryP =
- OuterSyntax.parser true "print_theory" "print logical theory contents (verbose!)"
+ OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)"
(Scan.succeed IsarCmd.print_theory);
val print_syntaxP =
- OuterSyntax.parser true "print_syntax" "print inner syntax of theory (verbose!)"
+ OuterSyntax.improper_command "print_syntax" "print inner syntax of theory (verbose!)"
(Scan.succeed IsarCmd.print_syntax);
val print_theoremsP =
- OuterSyntax.parser true "print_theorems" "print theorems known in this theory"
+ OuterSyntax.improper_command "print_theorems" "print theorems known in this theory"
(Scan.succeed IsarCmd.print_theorems);
val print_attributesP =
- OuterSyntax.parser true "print_attributes" "print attributes known in this theory"
+ OuterSyntax.improper_command "print_attributes" "print attributes known in this theory"
(Scan.succeed IsarCmd.print_attributes);
val print_methodsP =
- OuterSyntax.parser true "print_methods" "print methods known in this theory"
+ OuterSyntax.improper_command "print_methods" "print methods known in this theory"
(Scan.succeed IsarCmd.print_methods);
val print_bindsP =
- OuterSyntax.parser true "print_binds" "print term bindings of proof context"
+ OuterSyntax.improper_command "print_binds" "print term bindings of proof context"
(Scan.succeed IsarCmd.print_binds);
val print_lthmsP =
- OuterSyntax.parser true "print_facts" "print local theorems of proof context"
+ OuterSyntax.improper_command "print_facts" "print local theorems of proof context"
(Scan.succeed IsarCmd.print_lthms);
val print_thmsP =
- OuterSyntax.parser true "thm" "print theorems" (xthm >> IsarCmd.print_thms);
+ OuterSyntax.improper_command "thm" "print theorems" (xthm >> IsarCmd.print_thms);
val print_propP =
- OuterSyntax.parser true "prop" "read and print proposition"
+ OuterSyntax.improper_command "prop" "read and print proposition"
(term >> IsarCmd.print_prop);
val print_termP =
- OuterSyntax.parser true "term" "read and print term"
+ OuterSyntax.improper_command "term" "read and print term"
(term >> IsarCmd.print_term);
val print_typeP =
- OuterSyntax.parser true "type" "read and print type"
+ OuterSyntax.improper_command "type" "read and print type"
(typ >> IsarCmd.print_type);
@@ -464,46 +440,46 @@
(** system commands (for interactive mode only) **)
val cdP =
- OuterSyntax.parser true "cd" "change current working directory"
+ OuterSyntax.improper_command "cd" "change current working directory"
(name >> IsarCmd.cd);
val pwdP =
- OuterSyntax.parser true "pwd" "print current working directory"
+ OuterSyntax.improper_command "pwd" "print current working directory"
(Scan.succeed IsarCmd.pwd);
val use_thyP =
- OuterSyntax.parser true "use_thy" "use theory file"
+ OuterSyntax.improper_command "use_thy" "use theory file"
(name >> IsarCmd.use_thy);
val update_thyP =
- OuterSyntax.parser true "update_thy" "update theory file"
+ OuterSyntax.improper_command "update_thy" "update theory file"
(name >> IsarCmd.update_thy);
val prP =
- OuterSyntax.parser true "pr" "print current toplevel state"
+ OuterSyntax.improper_command "pr" "print current toplevel state"
(Scan.succeed (Toplevel.print o Toplevel.imperative (K ())));
val opt_unit = Scan.optional ($$$ "(" -- $$$ ")" >> (K ())) ();
val commitP =
- OuterSyntax.parser true "commit" "commit current session to ML database"
+ OuterSyntax.improper_command "commit" "commit current session to ML database"
(opt_unit >> (K IsarCmd.use_commit));
val quitP =
- OuterSyntax.parser true "quit" "quit Isabelle"
+ OuterSyntax.improper_command "quit" "quit Isabelle"
(opt_unit >> (K IsarCmd.quit));
val exitP =
- OuterSyntax.parser true "exit" "exit Isar loop"
+ OuterSyntax.improper_command "exit" "exit Isar loop"
(Scan.succeed IsarCmd.exit);
val restartP =
- OuterSyntax.parser true "restart" "restart Isar loop"
+ OuterSyntax.improper_command "restart" "restart Isar loop"
(Scan.succeed IsarCmd.restart);
val breakP =
- OuterSyntax.parser true "break" "discontinue excursion (keep current state)"
+ OuterSyntax.improper_command "break" "discontinue excursion (keep current state)"
(Scan.succeed IsarCmd.break);
@@ -522,13 +498,13 @@
(*theory structure*)
theoryP, endP, contextP, update_contextP,
(*theory sections*)
- textP, titleP, chapterP, sectionP, subsectionP, subsubsectionP, classesP,
- classrelP, defaultsortP, typedeclP, typeabbrP, nontermP, aritiesP,
- constsP, syntaxP, translationsP, axiomsP, defsP, theoremsP, lemmasP,
- axclassP, instanceP, globalP, localP, pathP, useP, mlP, setupP,
- parse_ast_translationP, parse_translationP, print_translationP,
- typed_print_translationP, print_ast_translationP,
- token_translationP, oracleP,
+ textP, titleP, chapterP, sectionP, subsectionP, subsubsectionP,
+ classesP, classrelP, defaultsortP, typedeclP, typeabbrP, nontermP,
+ aritiesP, constsP, syntaxP, translationsP, axiomsP, defsP,
+ constdefsP, theoremsP, lemmasP, globalP, localP, pathP, useP, mlP,
+ setupP, parse_ast_translationP, parse_translationP,
+ print_translationP, typed_print_translationP,
+ print_ast_translationP, token_translationP, oracleP,
(*proof commands*)
theoremP, lemmaP, showP, haveP, assumeP, fixP, letP, thenP, fromP,
factsP, beginP, nextP, qedP, qed_withP, kill_proofP, refineP,