87 val axclassP = |
87 val axclassP = |
88 OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl |
88 OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl |
89 (P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- |
89 (P.name -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- |
90 P.!!! (P.list1 P.xname)) [] |
90 P.!!! (P.list1 P.xname)) [] |
91 -- Scan.repeat (SpecParse.thm_name ":" -- (P.prop >> single)) |
91 -- Scan.repeat (SpecParse.thm_name ":" -- (P.prop >> single)) |
92 >> (fn (x, y) => Toplevel.theory (snd o ClassPackage.axclass_cmd x y))); |
92 >> (fn (x, y) => Toplevel.theory (snd o Class.axclass_cmd x y))); |
93 |
93 |
94 |
94 |
95 (* types *) |
95 (* types *) |
96 |
96 |
97 val typedeclP = |
97 val typedeclP = |
420 || class_subP >> rpair [] |
420 || class_subP >> rpair [] |
421 || class_bodyP >> pair []) |
421 || class_bodyP >> pair []) |
422 -- P.opt_begin |
422 -- P.opt_begin |
423 >> (fn (((bname, add_consts), (supclasses, elems)), begin) => |
423 >> (fn (((bname, add_consts), (supclasses, elems)), begin) => |
424 Toplevel.begin_local_theory begin |
424 Toplevel.begin_local_theory begin |
425 (ClassPackage.class_cmd bname supclasses elems add_consts #-> TheoryTarget.begin))); |
425 (Class.class_cmd bname supclasses elems add_consts #-> TheoryTarget.begin))); |
426 |
426 |
427 val instanceP = |
427 val instanceP = |
428 OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal (( |
428 OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal (( |
429 P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) |
429 P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) |
430 >> ClassPackage.instance_class_cmd |
430 >> Class.instance_class_cmd |
431 || P.$$$ "advanced" |-- P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) |
431 || P.$$$ "advanced" |-- P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) |
432 >> ClassPackage.instance_sort_cmd |
432 >> Class.instance_sort_cmd |
433 || P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop) |
433 || P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop) |
434 >> (fn (arities, defs) => ClassPackage.instance_arity_cmd arities defs) |
434 >> (fn (arities, defs) => Class.instance_arity_cmd arities defs) |
435 ) >> (Toplevel.print oo Toplevel.theory_to_proof)); |
435 ) >> (Toplevel.print oo Toplevel.theory_to_proof)); |
436 |
436 |
437 end; |
437 end; |
438 |
438 |
439 |
439 |
440 (* code generation *) |
440 (* code generation *) |
441 |
441 |
442 val code_datatypeP = |
442 val code_datatypeP = |
443 OuterSyntax.command "code_datatype" "define set of code datatype constructors" K.thy_decl |
443 OuterSyntax.command "code_datatype" "define set of code datatype constructors" K.thy_decl |
444 (Scan.repeat1 P.term >> (Toplevel.theory o CodegenData.add_datatype_consts_cmd)); |
444 (Scan.repeat1 P.term >> (Toplevel.theory o Code.add_datatype_consts_cmd)); |
445 |
445 |
446 |
446 |
447 |
447 |
448 (** proof commands **) |
448 (** proof commands **) |
449 |
449 |
761 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_locales)); |
761 (Scan.succeed (Toplevel.no_timing o IsarCmd.print_locales)); |
762 |
762 |
763 val print_classesP = |
763 val print_classesP = |
764 OuterSyntax.improper_command "print_classes" "print classes of this theory" K.diag |
764 OuterSyntax.improper_command "print_classes" "print classes of this theory" K.diag |
765 (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory |
765 (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory |
766 o Toplevel.keep (ClassPackage.print_classes o Toplevel.theory_of))); |
766 o Toplevel.keep (Class.print_classes o Toplevel.theory_of))); |
767 |
767 |
768 val print_localeP = |
768 val print_localeP = |
769 OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag |
769 OuterSyntax.improper_command "print_locale" "print locale expression in this theory" K.diag |
770 (opt_bang -- locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale)); |
770 (opt_bang -- locale_val >> (Toplevel.no_timing oo IsarCmd.print_locale)); |
771 |
771 |
882 |
882 |
883 val print_codesetupP = |
883 val print_codesetupP = |
884 OuterSyntax.improper_command "print_codesetup" "print code generator setup of this theory" K.diag |
884 OuterSyntax.improper_command "print_codesetup" "print code generator setup of this theory" K.diag |
885 (Scan.succeed |
885 (Scan.succeed |
886 (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep |
886 (Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep |
887 (CodegenData.print_codesetup o Toplevel.theory_of))); |
887 (Code.print_codesetup o Toplevel.theory_of))); |
888 |
888 |
889 |
889 |
890 (** system commands (for interactive mode only) **) |
890 (** system commands (for interactive mode only) **) |
891 |
891 |
892 val cdP = |
892 val cdP = |