757 |
757 |
758 structure P = OuterParse and K = OuterKeyword; |
758 structure P = OuterParse and K = OuterKeyword; |
759 |
759 |
760 val parse_vars = Scan.optional (P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") []; |
760 val parse_vars = Scan.optional (P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") []; |
761 |
761 |
762 val realizersP = |
762 val _ = |
763 OuterSyntax.command "realizers" |
763 OuterSyntax.command "realizers" |
764 "specify realizers for primitive axioms / theorems, together with correctness proof" |
764 "specify realizers for primitive axioms / theorems, together with correctness proof" |
765 K.thy_decl |
765 K.thy_decl |
766 (Scan.repeat1 (P.xname -- parse_vars --| P.$$$ ":" -- P.string -- P.string) >> |
766 (Scan.repeat1 (P.xname -- parse_vars --| P.$$$ ":" -- P.string -- P.string) >> |
767 (fn xs => Toplevel.theory (fn thy => add_realizers |
767 (fn xs => Toplevel.theory (fn thy => add_realizers |
768 (map (fn (((a, vs), s1), s2) => |
768 (map (fn (((a, vs), s1), s2) => |
769 (PureThy.get_thm thy (Name a), (vs, s1, s2))) xs) thy))); |
769 (PureThy.get_thm thy (Name a), (vs, s1, s2))) xs) thy))); |
770 |
770 |
771 val realizabilityP = |
771 val _ = |
772 OuterSyntax.command "realizability" |
772 OuterSyntax.command "realizability" |
773 "add equations characterizing realizability" K.thy_decl |
773 "add equations characterizing realizability" K.thy_decl |
774 (Scan.repeat1 P.string >> (Toplevel.theory o add_realizes_eqns)); |
774 (Scan.repeat1 P.string >> (Toplevel.theory o add_realizes_eqns)); |
775 |
775 |
776 val typeofP = |
776 val _ = |
777 OuterSyntax.command "extract_type" |
777 OuterSyntax.command "extract_type" |
778 "add equations characterizing type of extracted program" K.thy_decl |
778 "add equations characterizing type of extracted program" K.thy_decl |
779 (Scan.repeat1 P.string >> (Toplevel.theory o add_typeof_eqns)); |
779 (Scan.repeat1 P.string >> (Toplevel.theory o add_typeof_eqns)); |
780 |
780 |
781 val extractP = |
781 val _ = |
782 OuterSyntax.command "extract" "extract terms from proofs" K.thy_decl |
782 OuterSyntax.command "extract" "extract terms from proofs" K.thy_decl |
783 (Scan.repeat1 (P.xname -- parse_vars) >> (fn xs => Toplevel.theory |
783 (Scan.repeat1 (P.xname -- parse_vars) >> (fn xs => Toplevel.theory |
784 (fn thy => extract (map (apfst (PureThy.get_thm thy o Name)) xs) thy))); |
784 (fn thy => extract (map (apfst (PureThy.get_thm thy o Name)) xs) thy))); |
785 |
785 |
786 val _ = OuterSyntax.add_parsers [realizersP, realizabilityP, typeofP, extractP]; |
|
787 |
|
788 val etype_of = etype_of o add_syntax; |
786 val etype_of = etype_of o add_syntax; |
789 |
787 |
790 end; |
788 end; |