src/Tools/Code/code_target.ML
changeset 39057 c6d146ed07ae
parent 39056 fa197571676b
child 39058 551fe1af03b0
equal deleted inserted replaced
39056:fa197571676b 39057:c6d146ed07ae
     6 
     6 
     7 signature CODE_TARGET =
     7 signature CODE_TARGET =
     8 sig
     8 sig
     9   val cert_tyco: theory -> string -> string
     9   val cert_tyco: theory -> string -> string
    10   val read_tyco: theory -> string -> string
    10   val read_tyco: theory -> string -> string
       
    11   val read_const_exprs: theory -> string list -> string list
    11 
    12 
    12   val export_code_for: theory -> Path.T option -> string -> int option -> string -> Token.T list
    13   val export_code_for: theory -> Path.T option -> string -> int option -> string -> Token.T list
    13     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit
    14     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit
    14   val produce_code_for: theory -> string -> int option -> string -> Token.T list
    15   val produce_code_for: theory -> string -> int option -> string -> Token.T list
    15     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
    16     -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
    75 fun stmt_names_of_destination (Present stmt_names) = stmt_names
    76 fun stmt_names_of_destination (Present stmt_names) = stmt_names
    76   | stmt_names_of_destination _ = [];
    77   | stmt_names_of_destination _ = [];
    77 
    78 
    78 fun serialization output _ content width (Export some_path) = (output width some_path content; NONE)
    79 fun serialization output _ content width (Export some_path) = (output width some_path content; NONE)
    79   | serialization _ string content width Produce = SOME (string [] width content)
    80   | serialization _ string content width Produce = SOME (string [] width content)
    80   | serialization _ string content width (Present _) = SOME (string [] width content);
    81   | serialization _ string content width (Present stmt_names) = SOME (string stmt_names width content);
    81 
    82 
    82 fun export some_path f = (f (Export some_path); ());
    83 fun export some_path f = (f (Export some_path); ());
    83 fun produce f = the (f Produce);
    84 fun produce f = the (f Produce);
    84 fun present stmt_names f = fst (the (f (Present stmt_names)));
    85 fun present stmt_names f = fst (the (f (Present stmt_names)));
    85 
    86