5832

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 
 print_thm: attributes;


15 
 'result' command;


16 
 '' (comment) option everywhere;


17 
 'chapter', 'section' etc.;


18 
*)


19 


20 
signature ISAR_SYN =


21 
sig


22 
val keywords: string list


23 
val parsers: OuterSyntax.parser list


24 
end;


25 


26 
structure IsarSyn: ISAR_SYN =


27 
struct


28 


29 
open OuterParse;


30 


31 


32 
(** init and exit **)


33 


34 
val contextP =


35 
OuterSyntax.parser false "context" "switch theory context"


36 
(name >> (fn x => Toplevel.print o Toplevel.init_theory (IsarThy.the_theory x) (K ())));


37 


38 
val theoryP =


39 
OuterSyntax.parser false "theory" "begin theory"


40 
(name  ($$$ "="  !!! (enum "+" name  (Scan.ahead eof  $$$ ":")))


41 
>> (fn x => Toplevel.print o


42 
Toplevel.init_theory (IsarThy.begin_theory x) IsarThy.end_theory));


43 


44 
(*end current theory / subproof / excursion*)


45 
val endP =


46 
OuterSyntax.parser false "end" "end current theory / subproof / excursion"


47 
(Scan.succeed (Toplevel.print o Toplevel.exit o Toplevel.proof IsarThy.end_block));


48 


49 


50 


51 
(** theory sections **)


52 


53 
(* formal comments *)


54 


55 
val textP = OuterSyntax.parser false "text" "formal comments"


56 
(text >> K (Toplevel.keep (K ())));


57 


58 


59 
(* classes and sorts *)


60 


61 
val classesP =


62 
OuterSyntax.parser false "classes" "declare type classes"


63 
(Scan.repeat1 (name  Scan.optional ($$$ "<"  !!! (list1 xname)) [])


64 
>> (Toplevel.theory o Theory.add_classes));


65 


66 
val classrelP =


67 
OuterSyntax.parser false "classrel" "state inclusion of type classes (axiomatic!)"


68 
(xname  ($$$ "<"  !!! xname) >> (Toplevel.theory o Theory.add_classrel o single));


69 


70 
val defaultsortP =


71 
OuterSyntax.parser false "defaultsort" "declare default sort"


72 
(sort >> (Toplevel.theory o Theory.add_defsort));


73 


74 


75 
(* types *)


76 


77 
val typedeclP =


78 
OuterSyntax.parser false "typedecl" "declare logical type"


79 
(type_args  name  opt_infix


80 
>> (fn ((args, a), mx) => Toplevel.theory (PureThy.add_typedecls [(a, args, mx)])));


81 


82 
val typeabbrP =


83 
OuterSyntax.parser false "types" "declare type abbreviations"


84 
(Scan.repeat1 (type_args  name  ($$$ "="  !!! (typ  opt_infix)))


85 
>> (Toplevel.theory o Theory.add_tyabbrs o


86 
map (fn ((args, a), (T, mx)) => (a, args, T, mx))));


87 


88 
val nontermP =


89 
OuterSyntax.parser false "nonterminals" "declare types treated as grammar nonterminal symbols"


90 
(Scan.repeat1 name >> (Toplevel.theory o Theory.add_nonterminals));


91 


92 
val aritiesP =


93 
OuterSyntax.parser false "arities" "state type arities (axiomatic!)"


94 
(Scan.repeat1 (xname  ($$$ "::"  !!! arity) >> triple2)


95 
>> (Toplevel.theory o Theory.add_arities));


96 


97 


98 
(* consts and syntax *)


99 


100 
val constsP =


101 
OuterSyntax.parser false "consts" "declare constants"


102 
(Scan.repeat1 const >> (Toplevel.theory o Theory.add_consts));


103 


104 
val opt_mode =


105 
Scan.optional


106 
($$$ "("  !!! (name  Scan.optional ($$$ "output" >> K false) true  $$$ ")"))


107 
("", true);


108 


109 
val syntaxP =


110 
OuterSyntax.parser false "syntax" "declare syntactic constants"


111 
(opt_mode  Scan.repeat1 const >> (Toplevel.theory o uncurry Theory.add_modesyntax));


112 


113 


114 
(* translations *)


115 


116 
val trans_pat =


117 
Scan.optional ($$$ "("  !!! (xname  $$$ ")")) "logic"  string;


118 


119 
fun trans_arrow toks =


120 
($$$ "=>" >> K Syntax.ParseRule 


121 
$$$ "<=" >> K Syntax.PrintRule 


122 
$$$ "==" >> K Syntax.ParsePrintRule) toks;


123 


124 
val trans_line =


125 
trans_pat  !!! (trans_arrow  trans_pat)


126 
>> (fn (left, (arr, right)) => arr (left, right));


127 


128 
val translationsP =


129 
OuterSyntax.parser false "translations" "declare syntax translation rules"


130 
(Scan.repeat1 trans_line >> (Toplevel.theory o Theory.add_trrules));


131 


132 


133 
(* axioms and definitions *)


134 


135 
val spec = thm_name  prop >> (fn ((x, y), z) => ((x, z), y));


136 
val spec' = opt_thm_name  prop >> (fn ((x, y), z) => ((x, z), y));


137 


138 
val axiomsP =


139 
OuterSyntax.parser false "axioms" "state arbitrary propositions (axiomatic!)"


140 
(Scan.repeat1 spec >> (Toplevel.theory o IsarThy.add_axioms));


141 


142 
val defsP =


143 
OuterSyntax.parser false "defs" "define constants"


144 
(Scan.repeat1 spec' >> (Toplevel.theory o IsarThy.add_defs));


145 


146 


147 
(* axclass *)


148 


149 
val axclassP =


150 
OuterSyntax.parser false "axclass" "define axiomatic type class"


151 
(name  Scan.optional ($$$ "<"  !!! (list1 xname)) []  Scan.repeat (spec >> fst)


152 
>> (Toplevel.theory o uncurry AxClass.add_axclass));


153 


154 


155 
(* instance *)


156 


157 
val opt_witness =


158 
Scan.optional ($$$ "("  !!! (list1 xname  $$$ ")")) [];


159 


160 
val instanceP =


161 
OuterSyntax.parser false "instance" "prove type arity"


162 
((xname  ($$$ "<"  xname) >> AxClass.add_inst_subclass 


163 
xname  ($$$ "::"  arity) >> (AxClass.add_inst_arity o triple2))


164 
 opt_witness >> (fn (f, x) => Toplevel.theory (f x [] None)));


165 


166 


167 
(* name space entry path *)


168 


169 
val globalP =


170 
OuterSyntax.parser false "global" "disable prefixing of theory name"


171 
(Scan.succeed (Toplevel.theory PureThy.global_path));


172 


173 
val localP =


174 
OuterSyntax.parser false "local" "enable prefixing of theory name"


175 
(Scan.succeed (Toplevel.theory PureThy.local_path));


176 


177 
val pathP =


178 
OuterSyntax.parser false "path" "modify namespace entry path"


179 
(xname >> (Toplevel.theory o Theory.add_path));


180 


181 


182 
(* use ML text *)


183 


184 
val useP =


185 
OuterSyntax.parser true "use" "eval ML text from file"


186 
(string >> IsarCmd.use);


187 


188 
val mlP =


189 
OuterSyntax.parser false "ML" "eval ML text"


190 
(text >> (fn txt => IsarCmd.use_mltext txt o IsarCmd.use_mltext_theory txt));


191 


192 
val setupP =


193 
OuterSyntax.parser false "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.parser false "parse_ast_translation" "install parse ast translation functions"


201 
(text >> (Toplevel.theory o IsarThy.parse_ast_translation));


202 


203 
val parse_translationP =


204 
OuterSyntax.parser false "parse_translation" "install parse translation functions"


205 
(text >> (Toplevel.theory o IsarThy.parse_translation));


206 


207 
val print_translationP =


208 
OuterSyntax.parser false "print_translation" "install print translation functions"


209 
(text >> (Toplevel.theory o IsarThy.print_translation));


210 


211 
val typed_print_translationP =


212 
OuterSyntax.parser false "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.parser false "print_ast_translation" "install print ast translation functions"


217 
(text >> (Toplevel.theory o IsarThy.print_ast_translation));


218 


219 
val token_translationP =


220 
OuterSyntax.parser false "token_translation" "install token translation functions"


221 
(text >> (Toplevel.theory o IsarThy.token_translation));


222 


223 


224 
(* oracles *)


225 


226 
val oracleP =


227 
OuterSyntax.parser false "oracle" "install oracle"


228 
(name  text >> (Toplevel.theory o IsarThy.add_oracle));


229 


230 


231 


232 
(** proof commands **)


233 


234 
(* statements *)


235 


236 
fun statement f = opt_thm_name  prop >> (fn ((x, y), z) => f x y z);


237 


238 
val theoremP =


239 
OuterSyntax.parser false "theorem" "state theorem"


240 
(statement IsarThy.theorem >> (fn f => Toplevel.print o Toplevel.theory_to_proof f));


241 


242 
val lemmaP =


243 
OuterSyntax.parser false "lemma" "state lemma"


244 
(statement IsarThy.lemma >> (fn f => Toplevel.print o Toplevel.theory_to_proof f));


245 


246 
val showP =


247 
OuterSyntax.parser false "show" "state local goal, solving current obligation"


248 
(statement IsarThy.show >> (fn f => Toplevel.print o Toplevel.proof f));


249 


250 
val haveP =


251 
OuterSyntax.parser false "have" "state local goal"


252 
(statement IsarThy.have >> (fn f => Toplevel.print o Toplevel.proof f));


253 


254 


255 
(* forward chaining *)


256 


257 
val thenP =


258 
OuterSyntax.parser false "then" "forward chaining"


259 
(Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.chain));


260 


261 
val fromP =


262 
OuterSyntax.parser false "from" "forward chaining, from given facts"


263 
(enum1 "," xname >> (fn x => Toplevel.print o Toplevel.proof (IsarThy.from_facts x)));


264 


265 


266 
(* proof context *)


267 


268 
val assumeP =


269 
OuterSyntax.parser false "assume" "assume propositions"


270 
(opt_thm_name  enum1 "," prop >>


271 
(fn ((x, y), z) => Toplevel.print o Toplevel.proof (IsarThy.assume x y z)));


272 


273 
val fixP =


274 
OuterSyntax.parser false "fix" "fix variables (Skolem constants)"


275 
(enum1 "," (name  Scan.option ($$$ "::"  typ))


276 
>> (fn xs => Toplevel.print o Toplevel.proof (IsarThy.fix xs)));


277 


278 
val letP =


279 
OuterSyntax.parser false "let" "bind text variables"


280 
(enum1 "and" (term  ($$$ "="  term))


281 
>> (fn bs => Toplevel.print o Toplevel.proof (IsarThy.match_bind bs)));


282 


283 


284 
(* proof structure *)


285 


286 
val beginP =


287 
OuterSyntax.parser false "begin" "begin block"


288 
(Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.begin_block));


289 


290 
val nextP =


291 
OuterSyntax.parser false "next" "enter next block"


292 
(Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.next_block));


293 


294 


295 
(* end proof *)


296 


297 
val qedP =


298 
OuterSyntax.parser false "qed" "conclude proof"


299 
(Scan.succeed (Toplevel.proof_to_theory IsarThy.qed));


300 


301 
val qed_withP =


302 
OuterSyntax.parser true "qed_with" "conclude proof, may patch name and attributes"


303 
(Scan.option name  Scan.option attribs >> (Toplevel.proof_to_theory o IsarThy.qed_with));


304 


305 
val kill_proofP =


306 
OuterSyntax.parser true "kill" "abort current proof"


307 
(Scan.succeed (Toplevel.print o Toplevel.proof_to_theory IsarThy.kill_proof));


308 


309 


310 
(* proof steps *)


311 


312 
fun gen_stepP meth int name cmt f =


313 
OuterSyntax.parser int name cmt


314 
(meth >> (fn txt => Toplevel.print o Toplevel.proof (f txt)));


315 


316 
val stepP = gen_stepP method;


317 


318 
val tacP = stepP true "tac" "unstructured backward proof step, ignoring facts" IsarThy.tac;


319 
val etacP = stepP true "etac" "unstructured backward proof step, using facts" IsarThy.etac;


320 


321 


322 
val proofP = gen_stepP (Scan.option method) false "proof" "backward proof" IsarThy.proof;


323 
val terminal_proofP = stepP false "by" "terminal backward proof" IsarThy.terminal_proof;


324 


325 
val trivial_proofP =


326 
OuterSyntax.parser false "." "trivial proof"


327 
(Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.trivial_proof));


328 


329 
val default_proofP =


330 
OuterSyntax.parser false ".." "default proof"


331 
(Scan.succeed (Toplevel.print o Toplevel.proof IsarThy.default_proof));


332 


333 


334 
(* proof history *)


335 


336 
val clear_undoP =


337 
OuterSyntax.parser true "clear_undo" "clear proof command undo information"


338 
(Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.clear));


339 


340 
val undoP =


341 
OuterSyntax.parser true "undo" "undo proof command"


342 
(Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.undo));


343 


344 
val redoP =


345 
OuterSyntax.parser true "redo" "redo proof command"


346 
(Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.redo));


347 


348 
val backP =


349 
OuterSyntax.parser true "back" "backtracking of proof command"


350 
(Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.back));


351 


352 
val prevP =


353 
OuterSyntax.parser true "prev" "previous proof state"


354 
(Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.prev));


355 


356 
val upP =


357 
OuterSyntax.parser true "up" "upper proof state"


358 
(Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.up));


359 


360 
val topP =


361 
OuterSyntax.parser true "top" "to initial proof state"


362 
(Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.top));


363 


364 


365 


366 
(** diagnostic commands (for interactive mode only) **)


367 


368 
val print_commandsP =


369 
OuterSyntax.parser true "help" "print outer syntax (global)"


370 
(Scan.succeed (Toplevel.imperative OuterSyntax.print_outer_syntax));


371 


372 
val print_theoryP =


373 
OuterSyntax.parser true "print_theory" "print logical theory contents (verbose!)"


374 
(Scan.succeed IsarCmd.print_theory);


375 


376 
val print_syntaxP =


377 
OuterSyntax.parser true "print_syntax" "print inner syntax of theory (verbose!)"


378 
(Scan.succeed IsarCmd.print_syntax);


379 


380 
val print_attributesP =


381 
OuterSyntax.parser true "print_attributes" "print attributes known in theory"


382 
(Scan.succeed IsarCmd.print_attributes);


383 


384 
val print_methodsP =


385 
OuterSyntax.parser true "print_methods" "print methods known in theory"


386 
(Scan.succeed IsarCmd.print_methods);


387 


388 
val print_bindsP =


389 
OuterSyntax.parser true "print_binds" "print term bindings of proof context"


390 
(Scan.succeed IsarCmd.print_binds);


391 


392 
val print_lthmsP =


393 
OuterSyntax.parser true "print_facts" "print local theorems of proof context"


394 
(Scan.succeed IsarCmd.print_lthms);


395 


396 
val print_thmP =


397 
OuterSyntax.parser true "print_thm" "print stored theorem(s)"


398 
(xname >> IsarCmd.print_thms);


399 


400 
val print_propP =


401 
OuterSyntax.parser true "print_prop" "read and print proposition"


402 
(term >> IsarCmd.print_prop);


403 


404 
val print_termP =


405 
OuterSyntax.parser true "print_term" "read and print term"


406 
(term >> IsarCmd.print_term);


407 


408 
val print_typeP =


409 
OuterSyntax.parser true "print_type" "read and print type"


410 
(typ >> IsarCmd.print_type);


411 


412 


413 


414 
(** system commands (for interactive mode only) **)


415 


416 
val cdP =


417 
OuterSyntax.parser true "cd" "change current working directory"


418 
(string >> IsarCmd.cd);


419 


420 
val pwdP =


421 
OuterSyntax.parser true "pwd" "print current working directory"


422 
(Scan.succeed IsarCmd.pwd);


423 


424 
val use_thyP =


425 
OuterSyntax.parser true "use_thy" "use_thy theory file"


426 
(string >> IsarCmd.use_thy);


427 


428 
val loadP =


429 
OuterSyntax.parser true "load" "load theory file"


430 
(string >> IsarCmd.load);


431 


432 
val prP =


433 
OuterSyntax.parser true "pr" "print current toplevel state"


434 
(Scan.succeed (Toplevel.print o Toplevel.imperative (K ())));


435 


436 


437 
val opt_unit = Scan.optional ($$$ "("  $$$ ")" >> (K ())) ();


438 


439 
val commitP =


440 
OuterSyntax.parser true "commit" "commit current session to ML database"


441 
(opt_unit >> (K IsarCmd.use_commit));


442 


443 
val quitP =


444 
OuterSyntax.parser true "quit" "quit Isabelle"


445 
(opt_unit >> (K IsarCmd.quit));


446 


447 
val exitP =


448 
OuterSyntax.parser true "exit" "exit Isar loop"


449 
(Scan.succeed IsarCmd.exit);


450 


451 
val breakP =


452 
OuterSyntax.parser true "break" "discontinue execution"


453 
(Scan.succeed IsarCmd.break);


454 


455 


456 


457 
(** the Pure outer syntax **)


458 


459 
(*keep keywords consistent with the parsers, including those in


460 
outer_parse.ML, otherwise be prepared for unexpected errors*)


461 


462 
val keywords =


463 
["(", ")", "*", "+", ",", ":", "::", ";", "<", "<=", "=", "==", "=>",


464 
"?", "[", "]", "and", "binder", "infixl", "infixr", "mixfix", "output",


465 
"{", "", "}"];


466 


467 
val parsers = [


468 
(*theory structure*)


469 
contextP, theoryP, endP,


470 
(*theory sections*)


471 
textP, classesP, classrelP, defaultsortP, typedeclP, typeabbrP,


472 
nontermP, aritiesP, constsP, syntaxP, translationsP, axiomsP, defsP,


473 
axclassP, instanceP, globalP, localP, pathP, useP, mlP, setupP,


474 
parse_ast_translationP, parse_translationP, print_translationP,


475 
typed_print_translationP, print_ast_translationP,


476 
token_translationP, oracleP,


477 
(*proof commands*)


478 
theoremP, lemmaP, showP, haveP, assumeP, fixP, letP, thenP, fromP,


479 
beginP, nextP, qedP, qed_withP, kill_proofP, tacP, etacP, proofP,


480 
terminal_proofP, trivial_proofP, default_proofP, clear_undoP, undoP,


481 
redoP, backP, prevP, upP, topP,


482 
(*diagnostic commands*)


483 
print_commandsP, print_theoryP, print_syntaxP, print_attributesP,


484 
print_methodsP, print_bindsP, print_lthmsP, print_thmP, print_propP,


485 
print_termP, print_typeP,


486 
(*system commands*)


487 
cdP, pwdP, use_thyP, loadP, prP, commitP, quitP, exitP, breakP];


488 


489 


490 
end;


491 


492 


493 
(* install the Pure outer syntax *)


494 


495 
OuterSyntax.add_keywords IsarSyn.keywords;


496 
OuterSyntax.add_parsers IsarSyn.parsers;
