17 -> theory -> theory |
17 -> theory -> theory |
18 val assert_target: theory -> string -> string |
18 val assert_target: theory -> string -> string |
19 |
19 |
20 type destination |
20 type destination |
21 type serialization |
21 type serialization |
22 val parse_args: (OuterLex.token list -> 'a * OuterLex.token list) |
22 val parse_args: 'a parser -> Token.T list -> 'a |
23 -> OuterLex.token list -> 'a |
|
24 val stmt_names_of_destination: destination -> string list |
23 val stmt_names_of_destination: destination -> string list |
25 val mk_serialization: string -> ('a -> unit) option |
24 val mk_serialization: string -> ('a -> unit) option |
26 -> (Path.T option -> 'a -> unit) |
25 -> (Path.T option -> 'a -> unit) |
27 -> ('a -> string * string option list) |
26 -> ('a -> string * string option list) |
28 -> 'a -> serialization |
27 -> 'a -> serialization |
29 val serialize: theory -> string -> int option -> string option -> OuterLex.token list |
28 val serialize: theory -> string -> int option -> string option -> Token.T list |
30 -> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization |
29 -> Code_Thingol.naming -> Code_Thingol.program -> string list -> serialization |
31 val serialize_custom: theory -> string * (serializer * literals) |
30 val serialize_custom: theory -> string * (serializer * literals) |
32 -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list |
31 -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list |
33 val the_literals: theory -> string -> literals |
32 val the_literals: theory -> string -> literals |
34 val compile: serialization -> unit |
33 val compile: serialization -> unit |
103 Symtab.join (K snd) (const1, const2)) |
102 Symtab.join (K snd) (const1, const2)) |
104 ); |
103 ); |
105 |
104 |
106 type serializer = |
105 type serializer = |
107 string option (*module name*) |
106 string option (*module name*) |
108 -> OuterLex.token list (*arguments*) |
107 -> Token.T list (*arguments*) |
109 -> (string -> string) (*labelled_name*) |
108 -> (string -> string) (*labelled_name*) |
110 -> string list (*reserved symbols*) |
109 -> string list (*reserved symbols*) |
111 -> (string * Pretty.T) list (*includes*) |
110 -> (string * Pretty.T) list (*includes*) |
112 -> (string -> string option) (*module aliasses*) |
111 -> (string -> string option) (*module aliasses*) |
113 -> (string -> string option) (*class syntax*) |
112 -> (string -> string option) (*class syntax*) |
496 val add_syntax_const_cmd = gen_add_syntax_const Code.read_const ((K o K o K) ()) I; |
495 val add_syntax_const_cmd = gen_add_syntax_const Code.read_const ((K o K o K) ()) I; |
497 |
496 |
498 val allow_abort_cmd = gen_allow_abort Code.read_const; |
497 val allow_abort_cmd = gen_allow_abort Code.read_const; |
499 |
498 |
500 fun parse_args f args = |
499 fun parse_args f args = |
501 case Scan.read OuterLex.stopper f args |
500 case Scan.read Token.stopper f args |
502 of SOME x => x |
501 of SOME x => x |
503 | NONE => error "Bad serializer arguments"; |
502 | NONE => error "Bad serializer arguments"; |
504 |
503 |
505 |
504 |
506 (** Isar setup **) |
505 (** Isar setup **) |
573 val _ = |
572 val _ = |
574 OuterSyntax.command "export_code" "generate executable code for constants" |
573 OuterSyntax.command "export_code" "generate executable code for constants" |
575 K.diag (P.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of))); |
574 K.diag (P.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of))); |
576 |
575 |
577 fun shell_command thyname cmd = Toplevel.program (fn _ => |
576 fun shell_command thyname cmd = Toplevel.program (fn _ => |
578 (use_thy thyname; case Scan.read OuterLex.stopper (P.!!! code_exprP) |
577 (use_thy thyname; case Scan.read Token.stopper (P.!!! code_exprP) |
579 ((filter OuterLex.is_proper o OuterSyntax.scan Position.none) cmd) |
578 ((filter Token.is_proper o OuterSyntax.scan Position.none) cmd) |
580 of SOME f => (writeln "Now generating code..."; f (theory thyname)) |
579 of SOME f => (writeln "Now generating code..."; f (theory thyname)) |
581 | NONE => error ("Bad directive " ^ quote cmd))) |
580 | NONE => error ("Bad directive " ^ quote cmd))) |
582 handle Runtime.TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure; |
581 handle Runtime.TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure; |
583 |
582 |
584 end; (*local*) |
583 end; (*local*) |