haftmann@37745: (* Title: Tools/Code/code_target.ML haftmann@24219: Author: Florian Haftmann, TU Muenchen haftmann@24219: haftmann@38910: Generic infrastructure for target language data. haftmann@24219: *) haftmann@24219: haftmann@24219: signature CODE_TARGET = haftmann@24219: sig haftmann@55757: val cert_tyco: Proof.context -> string -> string haftmann@55757: val read_tyco: Proof.context -> string -> string haftmann@36471: haftmann@55757: val export_code_for: Proof.context -> Path.T option -> string -> int option -> string -> Token.T list haftmann@55683: -> Code_Thingol.program -> bool -> Code_Symbol.T list -> unit haftmann@55757: val produce_code_for: Proof.context -> string -> int option -> string -> Token.T list haftmann@55683: -> Code_Thingol.program -> bool -> Code_Symbol.T list -> (string * string) list * string option list haftmann@55757: val present_code_for: Proof.context -> string -> int option -> string -> Token.T list haftmann@55150: -> Code_Thingol.program -> Code_Symbol.T list * Code_Symbol.T list -> string haftmann@55757: val check_code_for: Proof.context -> string -> bool -> Token.T list haftmann@55683: -> Code_Thingol.program -> bool -> Code_Symbol.T list -> unit haftmann@38918: haftmann@55757: val export_code: Proof.context -> bool -> string list haftmann@38933: -> (((string * string) * Path.T option) * Token.T list) list -> unit haftmann@55757: val produce_code: Proof.context -> bool -> string list haftmann@48568: -> string -> int option -> string -> Token.T list -> (string * string) list * string option list haftmann@55757: val present_code: Proof.context -> string list -> Code_Symbol.T list haftmann@38933: -> string -> int option -> string -> Token.T list -> string haftmann@55757: val check_code: Proof.context -> bool -> string list haftmann@38918: -> ((string * bool) * Token.T list) list -> unit haftmann@38918: haftmann@48568: val generatedN: string haftmann@55757: val evaluator: Proof.context -> string -> Code_Thingol.program haftmann@55684: -> Code_Symbol.T list -> bool -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm haftmann@48568: -> (string * string) list * string haftmann@41344: haftmann@28054: type serializer haftmann@34152: type literals = Code_Printer.literals haftmann@37822: val add_target: string * { serializer: serializer, literals: literals, wenzelm@41940: check: { env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string } } wenzelm@41940: -> theory -> theory haftmann@28663: val extend_target: string * haftmann@55147: (string * (Code_Thingol.program -> Code_Thingol.program)) haftmann@28054: -> theory -> theory haftmann@55757: val assert_target: Proof.context -> string -> string haftmann@55757: val the_literals: Proof.context -> string -> literals haftmann@28054: type serialization wenzelm@36959: val parse_args: 'a parser -> Token.T list -> 'a haftmann@38916: val serialization: (int -> Path.T option -> 'a -> unit) haftmann@55150: -> (Code_Symbol.T list -> int -> 'a -> (string * string) list * (Code_Symbol.T -> string option)) haftmann@38925: -> 'a -> serialization haftmann@38918: val set_default_code_width: int -> theory -> theory haftmann@38917: haftmann@52137: type ('a, 'b, 'c, 'd, 'e, 'f) symbol_attr_decl haftmann@52138: type identifier_data haftmann@52138: val set_identifiers: (string, string, string, string, string, string) symbol_attr_decl haftmann@52138: -> theory -> theory haftmann@55372: val set_printings: (Code_Printer.raw_const_syntax, Code_Printer.tyco_syntax, string, unit, unit, (string * string list)) symbol_attr_decl haftmann@52137: -> theory -> theory haftmann@28054: val add_reserved: string -> string -> theory -> theory haftmann@39646: haftmann@39750: val codegen_tool: string (*theory name*) -> string (*export_code expr*) -> unit wenzelm@43564: wenzelm@43564: val setup: theory -> theory haftmann@24219: end; haftmann@24219: haftmann@28054: structure Code_Target : CODE_TARGET = haftmann@24219: struct haftmann@24219: haftmann@55150: open Basic_Code_Symbol; haftmann@28054: open Basic_Code_Thingol; haftmann@34152: haftmann@34152: type literals = Code_Printer.literals; haftmann@52137: type ('a, 'b, 'c, 'd, 'e, 'f) symbol_attr_decl = haftmann@52137: (string * (string * 'a option) list, string * (string * 'b option) list, haftmann@52137: class * (string * 'c option) list, (class * class) * (string * 'd option) list, haftmann@52137: (class * string) * (string * 'e option) list, haftmann@52137: string * (string * 'f option) list) Code_Symbol.attr; haftmann@55291: type identifier_data = (string list * string, string list * string, string list * string, string list * string, haftmann@55291: string list * string, string list * string) Code_Symbol.data; haftmann@52137: haftmann@34152: type tyco_syntax = Code_Printer.tyco_syntax; haftmann@55153: type raw_const_syntax = Code_Printer.raw_const_syntax; haftmann@34152: haftmann@24219: haftmann@52377: (** checking and parsing of symbols **) haftmann@52377: haftmann@55757: fun cert_const ctxt const = haftmann@52377: let haftmann@55757: val _ = if Sign.declared_const (Proof_Context.theory_of ctxt) const then () haftmann@52377: else error ("No such constant: " ^ quote const); haftmann@52377: in const end; haftmann@52377: haftmann@55757: fun read_const ctxt = Code.read_const (Proof_Context.theory_of ctxt); haftmann@55757: haftmann@55757: fun cert_tyco ctxt tyco = haftmann@52377: let haftmann@55757: val _ = if Sign.declared_tyname (Proof_Context.theory_of ctxt) tyco then () haftmann@52377: else error ("No such type constructor: " ^ quote tyco); haftmann@52377: in tyco end; haftmann@52377: wenzelm@55951: fun read_tyco ctxt = wenzelm@56002: #1 o dest_Type o Proof_Context.read_type_name {proper = true, strict = true} ctxt; haftmann@52377: haftmann@55757: fun cert_class ctxt class = haftmann@52377: let haftmann@55757: val _ = Axclass.get_info (Proof_Context.theory_of ctxt) class; haftmann@52377: in class end; haftmann@52377: haftmann@52377: val parse_classrel_ident = Parse.class --| @{keyword "<"} -- Parse.class; haftmann@52377: haftmann@55757: fun cert_inst ctxt (class, tyco) = haftmann@55757: (cert_class ctxt class, cert_tyco ctxt tyco); haftmann@52377: haftmann@55757: fun read_inst ctxt (raw_tyco, raw_class) = haftmann@55757: (read_tyco ctxt raw_tyco, Proof_Context.read_class ctxt raw_class); haftmann@52377: haftmann@52377: val parse_inst_ident = Parse.xname --| @{keyword "::"} -- Parse.class; haftmann@52377: haftmann@55757: fun cert_syms ctxt = haftmann@55757: Code_Symbol.map_attr (apfst (cert_const ctxt)) (apfst (cert_tyco ctxt)) haftmann@55757: (apfst (cert_class ctxt)) ((apfst o pairself) (cert_class ctxt)) (apfst (cert_inst ctxt)) I; haftmann@52377: haftmann@55757: fun read_syms ctxt = haftmann@55757: Code_Symbol.map_attr (apfst (read_const ctxt)) (apfst (read_tyco ctxt)) haftmann@55757: (apfst (Proof_Context.read_class ctxt)) ((apfst o pairself) (Proof_Context.read_class ctxt)) (apfst (read_inst ctxt)) I; haftmann@52377: haftmann@52377: fun check_name is_module s = haftmann@52377: let haftmann@52377: val _ = if s = "" then error "Bad empty code name" else (); haftmann@52377: val xs = Long_Name.explode s; haftmann@52377: val xs' = if is_module haftmann@56811: then map (Name.desymbolize (SOME true)) xs haftmann@52377: else if length xs < 2 haftmann@52377: then error ("Bad code name without module component: " ^ quote s) haftmann@52377: else haftmann@52377: let haftmann@52377: val (ys, y) = split_last xs; haftmann@56811: val ys' = map (Name.desymbolize (SOME true)) ys; haftmann@56811: val y' = Name.desymbolize (SOME false) y; haftmann@52377: in ys' @ [y'] end; haftmann@52377: in if xs' = xs haftmann@55291: then if is_module then (xs, "") else split_last xs haftmann@52377: else error ("Invalid code name: " ^ quote s ^ "\n" haftmann@52377: ^ "better try " ^ quote (Long_Name.implode xs')) haftmann@52377: end; haftmann@52377: haftmann@52377: haftmann@52137: (** serializations and serializer **) haftmann@52137: haftmann@52137: (* serialization: abstract nonsense to cover different destinies for generated code *) haftmann@24219: haftmann@55150: datatype destination = Export of Path.T option | Produce | Present of Code_Symbol.T list; haftmann@55150: type serialization = int -> destination -> ((string * string) list * (Code_Symbol.T -> string option)) option; haftmann@27014: haftmann@39659: fun serialization output _ content width (Export some_path) = haftmann@39661: (output width some_path content; NONE) haftmann@39661: | serialization _ string content width Produce = haftmann@39661: string [] width content |> SOME haftmann@55147: | serialization _ string content width (Present syms) = haftmann@55147: string syms width content haftmann@48568: |> (apfst o map o apsnd) (Pretty.output (SOME width) o Pretty.str) haftmann@39661: |> SOME; haftmann@39659: haftmann@39661: fun export some_path f = (f (Export some_path); ()); haftmann@39661: fun produce f = the (f Produce); haftmann@55147: fun present syms f = space_implode "\n\n" (map snd (fst (the (f (Present syms))))); haftmann@38917: haftmann@24219: haftmann@52137: (* serializers: functions producing serializations *) haftmann@28054: haftmann@39142: type serializer = Token.T list haftmann@52138: -> Proof.context haftmann@39142: -> { haftmann@52138: module_name: string, haftmann@38926: reserved_syms: string list, haftmann@52138: identifiers: identifier_data, haftmann@38926: includes: (string * Pretty.T) list, haftmann@38926: class_syntax: string -> string option, haftmann@38926: tyco_syntax: string -> Code_Printer.tyco_syntax option, haftmann@55153: const_syntax: string -> Code_Printer.const_syntax option } haftmann@55683: -> Code_Symbol.T list haftmann@41342: -> Code_Thingol.program haftmann@28054: -> serialization; haftmann@27000: haftmann@52137: datatype description = haftmann@52137: Fundamental of { serializer: serializer, haftmann@38910: literals: literals, haftmann@37822: check: { env_var: string, make_destination: Path.T -> Path.T, wenzelm@41940: make_command: string -> string } } haftmann@38909: | Extension of string * haftmann@55147: (Code_Thingol.program -> Code_Thingol.program); haftmann@28054: haftmann@52137: haftmann@52137: (** theory data **) haftmann@52137: haftmann@28054: datatype target = Target of { haftmann@28054: serial: serial, haftmann@37821: description: description, haftmann@28054: reserved: string list, haftmann@52138: identifiers: identifier_data, haftmann@55153: printings: (Code_Printer.const_syntax, Code_Printer.tyco_syntax, string, unit, unit, haftmann@52137: (Pretty.T * string list)) Code_Symbol.data haftmann@28054: }; haftmann@27103: haftmann@52138: fun make_target ((serial, description), (reserved, (identifiers, printings))) = wenzelm@43564: Target { serial = serial, description = description, reserved = reserved, haftmann@52138: identifiers = identifiers, printings = printings }; haftmann@52138: fun map_target f (Target { serial, description, reserved, identifiers, printings }) = haftmann@52138: make_target (f ((serial, description), (reserved, (identifiers, printings)))); haftmann@37821: fun merge_target strict target (Target { serial = serial1, description = description, haftmann@52138: reserved = reserved1, identifiers = identifiers1, printings = printings1 }, haftmann@37821: Target { serial = serial2, description = _, haftmann@52138: reserved = reserved2, identifiers = identifiers2, printings = printings2 }) = haftmann@28054: if serial1 = serial2 orelse not strict then haftmann@52138: make_target ((serial1, description), (merge (op =) (reserved1, reserved2), haftmann@52138: (Code_Symbol.merge_data (identifiers1, identifiers2), haftmann@52138: Code_Symbol.merge_data (printings1, printings2)))) haftmann@28054: else haftmann@37821: error ("Incompatible targets: " ^ quote target); haftmann@27103: haftmann@37821: fun the_description (Target { description, ... }) = description; haftmann@28054: fun the_reserved (Target { reserved, ... }) = reserved; haftmann@52138: fun the_identifiers (Target { identifiers , ... }) = identifiers; haftmann@52137: fun the_printings (Target { printings, ... }) = printings; haftmann@27437: haftmann@34248: structure Targets = Theory_Data haftmann@34071: ( haftmann@54890: type T = target Symtab.table * int; haftmann@54890: val empty = (Symtab.empty, 80); haftmann@34071: val extend = I; haftmann@54890: fun merge ((target1, width1), (target2, width2)) : T = haftmann@54890: (Symtab.join (merge_target true) (target1, target2), Int.max (width1, width2)); haftmann@34071: ); haftmann@27436: haftmann@55757: fun assert_target ctxt target = haftmann@55757: if Symtab.defined (fst (Targets.get (Proof_Context.theory_of ctxt))) target haftmann@33969: then target haftmann@33969: else error ("Unknown code target language: " ^ quote target); haftmann@28054: haftmann@28054: fun put_target (target, seri) thy = haftmann@27304: let haftmann@54890: val lookup_target = Symtab.lookup (fst (Targets.get thy)); haftmann@28054: val _ = case seri haftmann@37821: of Extension (super, _) => if is_some (lookup_target super) then () haftmann@28054: else error ("Unknown code target language: " ^ quote super) haftmann@28054: | _ => (); haftmann@37821: val overwriting = case (Option.map the_description o lookup_target) target haftmann@28663: of NONE => false haftmann@37821: | SOME (Extension _) => true haftmann@37821: | SOME (Fundamental _) => (case seri haftmann@37821: of Extension _ => error ("Will not overwrite existing target " ^ quote target) haftmann@28663: | _ => true); haftmann@28663: val _ = if overwriting haftmann@28054: then warning ("Overwriting existing target " ^ quote target) wenzelm@43564: else (); haftmann@28054: in haftmann@28054: thy haftmann@54890: |> (Targets.map o apfst o Symtab.update) haftmann@52138: (target, make_target ((serial (), seri), haftmann@52138: ([], (Code_Symbol.empty_data, Code_Symbol.empty_data)))) haftmann@28054: end; haftmann@27436: haftmann@37821: fun add_target (target, seri) = put_target (target, Fundamental seri); haftmann@28054: fun extend_target (target, (super, modify)) = haftmann@37821: put_target (target, Extension (super, modify)); haftmann@27436: haftmann@28054: fun map_target_data target f thy = haftmann@27436: let haftmann@55757: val _ = assert_target (Proof_Context.init_global thy) target; haftmann@28054: in haftmann@28054: thy haftmann@54890: |> (Targets.map o apfst o Symtab.map_entry target o map_target o apsnd) f haftmann@28054: end; haftmann@27304: haftmann@28054: fun map_reserved target = haftmann@52138: map_target_data target o apfst; haftmann@52138: fun map_identifiers target = haftmann@52138: map_target_data target o apsnd o apfst; haftmann@52137: fun map_printings target = haftmann@52137: map_target_data target o apsnd o apsnd; haftmann@27000: haftmann@34248: fun set_default_code_width k = (Targets.map o apsnd) (K k); haftmann@34071: haftmann@27000: haftmann@34021: (** serializer usage **) haftmann@34021: haftmann@34021: (* montage *) haftmann@34021: haftmann@55757: fun the_fundamental ctxt = haftmann@34021: let haftmann@55757: val (targets, _) = Targets.get (Proof_Context.theory_of ctxt); haftmann@37822: fun fundamental target = case Symtab.lookup targets target haftmann@37821: of SOME data => (case the_description data haftmann@37822: of Fundamental data => data haftmann@37822: | Extension (super, _) => fundamental super) haftmann@34021: | NONE => error ("Unknown code target language: " ^ quote target); haftmann@37822: in fundamental end; haftmann@37822: haftmann@55757: fun the_literals ctxt = #literals o the_fundamental ctxt; haftmann@34021: haftmann@55757: fun collapse_hierarchy ctxt = haftmann@38927: let haftmann@55757: val (targets, _) = Targets.get (Proof_Context.theory_of ctxt); wenzelm@43564: fun collapse target = haftmann@38927: let haftmann@38927: val data = case Symtab.lookup targets target haftmann@38927: of SOME data => data haftmann@38927: | NONE => error ("Unknown code target language: " ^ quote target); haftmann@38927: in case the_description data haftmann@55147: of Fundamental _ => (I, data) haftmann@38927: | Extension (super, modify) => let haftmann@39817: val (modify', data') = collapse super haftmann@55147: in (modify' #> modify, merge_target false target (data', data)) end haftmann@38927: end; haftmann@39817: in collapse end; haftmann@39817: haftmann@39817: local haftmann@39817: haftmann@55757: fun activate_target ctxt target = haftmann@39817: let haftmann@55757: val thy = Proof_Context.theory_of ctxt; haftmann@54890: val (_, default_width) = Targets.get thy; haftmann@55757: val (modify, data) = collapse_hierarchy ctxt target; haftmann@54890: in (default_width, data, modify) end; haftmann@38927: haftmann@55757: fun project_program ctxt syms_hidden syms1 program2 = haftmann@38927: let haftmann@55147: val syms2 = subtract (op =) syms_hidden syms1; haftmann@55147: val program3 = Code_Symbol.Graph.restrict (not o member (op =) syms_hidden) program2; haftmann@55147: val syms4 = Code_Symbol.Graph.all_succs program3 syms2; haftmann@54890: val unimplemented = Code_Thingol.unimplemented program3; wenzelm@42359: val _ = haftmann@54889: if null unimplemented then () wenzelm@42359: else error ("No code equations for " ^ wenzelm@55304: commas (map (Proof_Context.markup_const ctxt) unimplemented)); haftmann@55147: val program4 = Code_Symbol.Graph.restrict (member (op =) syms4) program3; haftmann@55147: in (syms4, program4) end; haftmann@38927: haftmann@55757: fun prepare_serializer ctxt (serializer : serializer) reserved identifiers haftmann@55147: printings module_name args proto_program syms = haftmann@38927: let haftmann@55149: val syms_hidden = Code_Symbol.symbols_of printings; haftmann@55757: val (syms_all, program) = project_program ctxt syms_hidden syms proto_program; haftmann@39484: fun select_include (name, (content, cs)) = haftmann@55150: if null cs orelse exists (fn c => member (op =) syms_all (Constant c)) cs haftmann@39484: then SOME (name, content) else NONE; haftmann@52137: val includes = map_filter select_include (Code_Symbol.dest_module_data printings); haftmann@34021: in haftmann@55757: (serializer args ctxt { haftmann@52138: module_name = module_name, haftmann@38926: reserved_syms = reserved, haftmann@52138: identifiers = identifiers, haftmann@38926: includes = includes, haftmann@55149: const_syntax = Code_Symbol.lookup_constant_data printings, haftmann@55149: tyco_syntax = Code_Symbol.lookup_type_constructor_data printings, haftmann@55149: class_syntax = Code_Symbol.lookup_type_class_data printings }, haftmann@55776: (subtract (op =) syms_hidden syms, program)) haftmann@34021: end; haftmann@34021: haftmann@55757: fun mount_serializer ctxt target some_width module_name args program syms = haftmann@34021: let haftmann@55757: val (default_width, data, modify) = activate_target ctxt target; haftmann@38921: val serializer = case the_description data haftmann@38927: of Fundamental seri => #serializer seri; haftmann@55683: val (prepared_serializer, (prepared_syms, prepared_program)) = haftmann@55757: prepare_serializer ctxt serializer haftmann@52138: (the_reserved data) (the_identifiers data) (the_printings data) haftmann@55147: module_name args (modify program) syms haftmann@34071: val width = the_default default_width some_width; haftmann@55683: in (fn program => fn syms => prepared_serializer syms program width, (prepared_syms, prepared_program)) end; haftmann@41344: haftmann@55757: fun invoke_serializer ctxt target some_width raw_module_name args program all_public syms = haftmann@41344: let haftmann@55291: val module_name = if raw_module_name = "" then "" haftmann@55291: else (check_name true raw_module_name; raw_module_name) haftmann@55757: val (mounted_serializer, (prepared_syms, prepared_program)) = haftmann@55757: mount_serializer ctxt target some_width module_name args program syms; haftmann@55776: in mounted_serializer prepared_program (if all_public then [] else prepared_syms) end; haftmann@34021: haftmann@52138: fun assert_module_name "" = error "Empty module name not allowed here" haftmann@38933: | assert_module_name module_name = module_name; haftmann@38933: haftmann@55757: fun using_master_directory ctxt = wenzelm@56208: Option.map (Path.append (File.pwd ()) o wenzelm@56208: Path.append (Resources.master_directory (Proof_Context.theory_of ctxt))); haftmann@48371: haftmann@34021: in haftmann@34021: haftmann@48568: val generatedN = "Generated_Code"; haftmann@48568: haftmann@55757: fun export_code_for ctxt some_path target some_width module_name args = haftmann@55757: export (using_master_directory ctxt some_path) haftmann@55757: ooo invoke_serializer ctxt target some_width module_name args; haftmann@38918: haftmann@55757: fun produce_code_for ctxt target some_width module_name args = haftmann@39102: let haftmann@55757: val serializer = invoke_serializer ctxt target some_width (assert_module_name module_name) args; haftmann@55683: in fn program => fn all_public => fn syms => haftmann@55683: produce (serializer program all_public syms) |> apsnd (fn deresolve => map deresolve syms) haftmann@39484: end; haftmann@38929: haftmann@55757: fun present_code_for ctxt target some_width module_name args = haftmann@39484: let haftmann@55757: val serializer = invoke_serializer ctxt target some_width (assert_module_name module_name) args; haftmann@55147: in fn program => fn (syms, selects) => haftmann@55683: present selects (serializer program false syms) haftmann@39484: end; haftmann@38918: haftmann@55757: fun check_code_for ctxt target strict args program all_public syms = haftmann@37824: let haftmann@37824: val { env_var, make_destination, make_command } = haftmann@55757: (#check o the_fundamental ctxt) target; wenzelm@41939: fun ext_check p = wenzelm@43564: let haftmann@37824: val destination = make_destination p; haftmann@55757: val _ = export (SOME destination) (invoke_serializer ctxt target (SOME 80) haftmann@55683: generatedN args program all_public syms); haftmann@48568: val cmd = make_command generatedN; wenzelm@43850: in wenzelm@43850: if Isabelle_System.bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0 haftmann@37824: then error ("Code check failed for " ^ target ^ ": " ^ cmd) haftmann@37824: else () haftmann@37824: end; wenzelm@43850: in wenzelm@43850: if getenv env_var = "" haftmann@37825: then if strict haftmann@37825: then error (env_var ^ " not set; cannot check code for " ^ target) haftmann@37825: else warning (env_var ^ " not set; skipped checking code for " ^ target) wenzelm@41939: else Isabelle_System.with_tmp_dir "Code_Test" ext_check haftmann@37824: end; haftmann@37824: haftmann@55684: fun evaluation mounted_serializer prepared_program syms all_public ((vs, ty), t) = haftmann@41344: let haftmann@41344: val _ = if Code_Thingol.contains_dict_var t then haftmann@41344: error "Term to be evaluated contains free dictionaries" else (); wenzelm@43324: val v' = singleton (Name.variant_list (map fst vs)) "a"; haftmann@41344: val vs' = (v', []) :: vs; haftmann@55147: val ty' = ITyVar v' `-> ty; haftmann@41344: val program = prepared_program haftmann@55147: |> Code_Symbol.Graph.new_node (Code_Symbol.value, haftmann@55147: Code_Thingol.Fun (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE)) haftmann@55147: |> fold (curry (perhaps o try o haftmann@55147: Code_Symbol.Graph.add_edge) Code_Symbol.value) syms; haftmann@55683: val (program_code, deresolve) = haftmann@55684: produce (mounted_serializer program (if all_public then [] else [Code_Symbol.value])); haftmann@55147: val value_name = the (deresolve Code_Symbol.value); haftmann@55147: in (program_code, value_name) end; haftmann@41344: haftmann@55757: fun evaluator ctxt target program syms = haftmann@41344: let haftmann@55683: val (mounted_serializer, (_, prepared_program)) = haftmann@55757: mount_serializer ctxt target NONE generatedN [] program syms; haftmann@55147: in evaluation mounted_serializer prepared_program syms end; haftmann@41344: haftmann@34021: end; (* local *) haftmann@34021: haftmann@34021: haftmann@34021: (* code generation *) haftmann@34021: haftmann@38918: fun prep_destination "" = NONE haftmann@38918: | prep_destination s = SOME (Path.explode s); haftmann@38918: haftmann@55757: fun export_code ctxt all_public cs seris = haftmann@34021: let haftmann@55757: val thy = Proof_Context.theory_of ctxt; haftmann@55188: val program = Code_Thingol.consts_program thy cs; haftmann@38918: val _ = map (fn (((target, module_name), some_path), args) => haftmann@55757: export_code_for ctxt some_path target NONE module_name args program all_public (map Constant cs)) seris; haftmann@34021: in () end; haftmann@34021: haftmann@55757: fun export_code_cmd all_public raw_cs seris ctxt = haftmann@55757: export_code ctxt all_public haftmann@55757: (Code_Thingol.read_const_exprs ctxt raw_cs) haftmann@55683: ((map o apfst o apsnd) prep_destination seris); haftmann@38918: haftmann@55757: fun produce_code ctxt all_public cs target some_width some_module_name args = haftmann@38918: let haftmann@55757: val thy = Proof_Context.theory_of ctxt; haftmann@55188: val program = Code_Thingol.consts_program thy cs; haftmann@55757: in produce_code_for ctxt target some_width some_module_name args program all_public (map Constant cs) end; haftmann@38929: haftmann@55757: fun present_code ctxt cs syms target some_width some_module_name args = haftmann@38929: let haftmann@55757: val thy = Proof_Context.theory_of ctxt; haftmann@55188: val program = Code_Thingol.consts_program thy cs; haftmann@55757: in present_code_for ctxt target some_width some_module_name args program (map Constant cs, syms) end; haftmann@34021: haftmann@55757: fun check_code ctxt all_public cs seris = haftmann@37824: let haftmann@55757: val thy = Proof_Context.theory_of ctxt; haftmann@55188: val program = Code_Thingol.consts_program thy cs; haftmann@38918: val _ = map (fn ((target, strict), args) => haftmann@55757: check_code_for ctxt target strict args program all_public (map Constant cs)) seris; haftmann@37824: in () end; haftmann@37824: haftmann@55757: fun check_code_cmd all_public raw_cs seris ctxt = haftmann@55757: check_code ctxt all_public haftmann@55757: (Code_Thingol.read_const_exprs ctxt raw_cs) seris; haftmann@37824: haftmann@39480: local haftmann@39480: haftmann@39480: val parse_const_terms = Scan.repeat1 Args.term haftmann@55757: >> (fn ts => fn ctxt => map (Code.check_const (Proof_Context.theory_of ctxt)) ts); haftmann@39480: haftmann@55147: fun parse_names category parse internalize mark_symbol = haftmann@39480: Scan.lift (Args.parens (Args.$$$ category)) |-- Scan.repeat1 parse haftmann@55757: >> (fn xs => fn ctxt => map (mark_symbol o internalize ctxt) xs); wenzelm@43564: haftmann@39480: val parse_consts = parse_names "consts" Args.term haftmann@55757: (Code.check_const o Proof_Context.theory_of) Constant; haftmann@39480: haftmann@39480: val parse_types = parse_names "types" (Scan.lift Args.name) haftmann@55757: (Sign.intern_type o Proof_Context.theory_of) Type_Constructor; haftmann@39480: haftmann@39480: val parse_classes = parse_names "classes" (Scan.lift Args.name) haftmann@55757: (Sign.intern_class o Proof_Context.theory_of) Type_Class; haftmann@39480: haftmann@39480: val parse_instances = parse_names "instances" (Scan.lift (Args.name --| Args.$$$ "::" -- Args.name)) haftmann@55757: (fn ctxt => fn (raw_tyco, raw_class) => haftmann@55757: let haftmann@55757: val thy = Proof_Context.theory_of ctxt; haftmann@55757: in (Sign.intern_class thy raw_tyco, Sign.intern_type thy raw_class) end) Class_Instance; haftmann@39480: haftmann@39480: in haftmann@39480: wenzelm@43564: val antiq_setup = wenzelm@43564: Thy_Output.antiquotation @{binding code_stmts} wenzelm@43564: (parse_const_terms -- wenzelm@43564: Scan.repeat (parse_consts || parse_types || parse_classes || parse_instances) wenzelm@43564: -- Scan.lift (Args.parens (Args.name -- Scan.option Parse.int))) wenzelm@43564: (fn {context = ctxt, ...} => fn ((mk_cs, mk_stmtss), (target, some_width)) => haftmann@55757: present_code ctxt (mk_cs ctxt) haftmann@55757: (maps (fn f => f ctxt) mk_stmtss) haftmann@55757: target some_width "Example" []); haftmann@39480: haftmann@39480: end; haftmann@39480: haftmann@34021: haftmann@28054: (** serializer configuration **) haftmann@27000: haftmann@52138: (* reserved symbol names *) haftmann@52138: haftmann@52138: fun add_reserved target sym thy = haftmann@52138: let haftmann@55757: val (_, data) = collapse_hierarchy (Proof_Context.init_global thy) target; haftmann@52138: val _ = if member (op =) (the_reserved data) sym haftmann@52138: then error ("Reserved symbol " ^ quote sym ^ " already declared") haftmann@52138: else (); haftmann@52138: in haftmann@52138: thy haftmann@52138: |> map_reserved target (insert (op =) sym) haftmann@52138: end; haftmann@52138: haftmann@52138: haftmann@52377: (* checking of syntax *) haftmann@52138: haftmann@55757: fun check_const_syntax ctxt target c syn = haftmann@55757: if Code_Printer.requires_args syn > Code.args_number (Proof_Context.theory_of ctxt) c haftmann@52137: then error ("Too many arguments in syntax for constant " ^ quote c) haftmann@55757: else Code_Printer.prep_const_syntax (Proof_Context.theory_of ctxt) (the_literals ctxt target) c syn; haftmann@52137: haftmann@55757: fun check_tyco_syntax ctxt target tyco syn = haftmann@55757: if fst syn <> Sign.arity_number (Proof_Context.theory_of ctxt) tyco haftmann@52137: then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco) haftmann@52137: else syn; haftmann@34071: haftmann@52138: haftmann@52138: (* custom symbol names *) haftmann@52138: wenzelm@52218: fun arrange_name_decls x = haftmann@52138: let haftmann@52138: fun arrange is_module (sym, target_names) = map (fn (target, some_name) => haftmann@52138: (target, (sym, Option.map (check_name is_module) some_name))) target_names; haftmann@52138: in haftmann@52138: Code_Symbol.maps_attr' (arrange false) (arrange false) (arrange false) wenzelm@52218: (arrange false) (arrange false) (arrange true) x haftmann@52138: end; haftmann@52138: haftmann@55757: fun cert_name_decls ctxt = cert_syms ctxt #> arrange_name_decls; haftmann@52138: haftmann@55757: fun read_name_decls ctxt = read_syms ctxt #> arrange_name_decls; haftmann@52138: haftmann@52138: fun set_identifier (target, sym_name) = map_identifiers target (Code_Symbol.set_data sym_name); haftmann@52138: haftmann@52138: fun gen_set_identifiers prep_name_decl raw_name_decls thy = haftmann@55757: fold set_identifier (prep_name_decl (Proof_Context.init_global thy) raw_name_decls) thy; haftmann@52138: haftmann@52138: val set_identifiers = gen_set_identifiers cert_name_decls; haftmann@52138: val set_identifiers_cmd = gen_set_identifiers read_name_decls; haftmann@52138: haftmann@52138: haftmann@52138: (* custom printings *) haftmann@52138: haftmann@55757: fun arrange_printings prep_const ctxt = haftmann@52137: let haftmann@52137: fun arrange check (sym, target_syns) = haftmann@55757: map (fn (target, some_syn) => (target, (sym, Option.map (check ctxt target sym) some_syn))) target_syns; haftmann@52137: in haftmann@52137: Code_Symbol.maps_attr' haftmann@52137: (arrange check_const_syntax) (arrange check_tyco_syntax) haftmann@55149: (arrange ((K o K o K) I)) (arrange ((K o K o K) I)) (arrange ((K o K o K) I)) haftmann@55757: (arrange (fn ctxt => fn _ => fn _ => fn (raw_content, raw_cs) => haftmann@55757: (Code_Printer.str raw_content, map (prep_const ctxt) raw_cs))) haftmann@52137: end; haftmann@52137: haftmann@55757: fun cert_printings ctxt = cert_syms ctxt #> arrange_printings cert_const ctxt; haftmann@24219: haftmann@55757: fun read_printings ctxt = read_syms ctxt #> arrange_printings read_const ctxt; haftmann@52137: haftmann@52137: fun set_printing (target, sym_syn) = map_printings target (Code_Symbol.set_data sym_syn); haftmann@52137: haftmann@52137: fun gen_set_printings prep_print_decl raw_print_decls thy = haftmann@55757: fold set_printing (prep_print_decl (Proof_Context.init_global thy) raw_print_decls) thy; haftmann@52137: haftmann@52137: val set_printings = gen_set_printings cert_printings; haftmann@52137: val set_printings_cmd = gen_set_printings read_printings; haftmann@52137: haftmann@52137: haftmann@27103: (* concrete syntax *) haftmann@27000: haftmann@28054: fun parse_args f args = wenzelm@36959: case Scan.read Token.stopper f args haftmann@28054: of SOME x => x haftmann@28054: | NONE => error "Bad serializer arguments"; haftmann@28054: haftmann@28054: haftmann@27304: (** Isar setup **) haftmann@27103: haftmann@52137: fun parse_single_symbol_pragma parse_keyword parse_isa parse_target = haftmann@52434: parse_keyword |-- Parse.!!! (parse_isa --| (@{keyword "\"} || @{keyword "=>"}) haftmann@52434: -- Parse.and_list1 (@{keyword "("} |-- (Parse.name --| @{keyword ")"} -- Scan.option parse_target))); haftmann@52137: haftmann@52137: fun parse_symbol_pragma parse_const parse_tyco parse_class parse_classrel parse_inst parse_module = wenzelm@52801: parse_single_symbol_pragma @{keyword "constant"} Parse.term parse_const haftmann@55150: >> Constant haftmann@52377: || parse_single_symbol_pragma @{keyword "type_constructor"} Parse.type_const parse_tyco haftmann@55150: >> Type_Constructor haftmann@52377: || parse_single_symbol_pragma @{keyword "type_class"} Parse.class parse_class haftmann@55150: >> Type_Class haftmann@52137: || parse_single_symbol_pragma @{keyword "class_relation"} parse_classrel_ident parse_classrel haftmann@55150: >> Class_Relation haftmann@52137: || parse_single_symbol_pragma @{keyword "class_instance"} parse_inst_ident parse_inst haftmann@55150: >> Class_Instance haftmann@52137: || parse_single_symbol_pragma @{keyword "code_module"} Parse.name parse_module haftmann@52137: >> Code_Symbol.Module; haftmann@52137: haftmann@52137: fun parse_symbol_pragmas parse_const parse_tyco parse_class parse_classrel parse_inst parse_module = haftmann@52137: Parse.enum1 "|" (Parse.group (fn () => "code symbol pragma") haftmann@52137: (parse_symbol_pragma parse_const parse_tyco parse_class parse_classrel parse_inst parse_module)); haftmann@52137: wenzelm@56201: val code_expr_argsP = Scan.optional (@{keyword "("} |-- Parse.args --| @{keyword ")"}) []; haftmann@52138: haftmann@55683: fun code_expr_inP all_public raw_cs = haftmann@52434: Scan.repeat (@{keyword "in"} |-- Parse.!!! (Parse.name haftmann@52434: -- Scan.optional (@{keyword "module_name"} |-- Parse.name) "" haftmann@52434: -- Scan.optional (@{keyword "file"} |-- Parse.name) "" haftmann@52434: -- code_expr_argsP)) haftmann@55683: >> (fn seri_args => export_code_cmd all_public raw_cs seri_args); haftmann@52434: haftmann@55683: fun code_expr_checkingP all_public raw_cs = haftmann@52434: (@{keyword "checking"} |-- Parse.!!! haftmann@52434: (Scan.repeat (Parse.name -- ((@{keyword "?"} |-- Scan.succeed false) || Scan.succeed true) haftmann@52434: -- code_expr_argsP))) haftmann@55683: >> (fn seri_args => check_code_cmd all_public raw_cs seri_args); haftmann@52434: haftmann@55683: val code_exprP = (Scan.optional (@{keyword "open"} |-- Scan.succeed true) false haftmann@55683: -- Scan.repeat1 Parse.term) haftmann@55683: :|-- (fn (all_public, raw_cs) => (code_expr_checkingP all_public raw_cs || code_expr_inP all_public raw_cs)); haftmann@52138: haftmann@52138: val _ = haftmann@52138: Outer_Syntax.command @{command_spec "code_reserved"} haftmann@52138: "declare words as reserved for target language" haftmann@52138: (Parse.name -- Scan.repeat1 Parse.name haftmann@52138: >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds)); haftmann@52138: haftmann@52138: val _ = haftmann@52138: Outer_Syntax.command @{command_spec "code_identifier"} "declare mandatory names for code symbols" haftmann@52138: (parse_symbol_pragmas Parse.name Parse.name Parse.name Parse.name Parse.name Parse.name haftmann@52138: >> (Toplevel.theory o fold set_identifiers_cmd)); haftmann@52138: haftmann@52138: val _ = haftmann@52137: Outer_Syntax.command @{command_spec "code_printing"} "declare dedicated printing for code symbols" haftmann@52137: (parse_symbol_pragmas (Code_Printer.parse_const_syntax) (Code_Printer.parse_tyco_syntax) haftmann@52137: Parse.string (Parse.minus >> K ()) (Parse.minus >> K ()) haftmann@52137: (Parse.text -- Scan.optional (@{keyword "attach"} |-- Scan.repeat1 Parse.term) []) haftmann@52137: >> (Toplevel.theory o fold set_printings_cmd)); haftmann@52137: haftmann@52137: val _ = wenzelm@46961: Outer_Syntax.command @{command_spec "export_code"} "generate executable code for constants" haftmann@55757: (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.context_of))); haftmann@30494: haftmann@39646: haftmann@39646: (** external entrance point -- for codegen tool **) haftmann@39646: haftmann@39750: fun codegen_tool thyname cmd_expr = haftmann@39646: let haftmann@55757: val ctxt = Proof_Context.init_global (Thy_Info.get_theory thyname); haftmann@39646: val parse = Scan.read Token.stopper (Parse.!!! code_exprP) o haftmann@39646: (filter Token.is_proper o Outer_Syntax.scan Position.none); haftmann@39646: in case parse cmd_expr haftmann@55757: of SOME f => (writeln "Now generating code..."; f ctxt) haftmann@39646: | NONE => error ("Bad directive " ^ quote cmd_expr) haftmann@39646: end; haftmann@39646: wenzelm@43564: wenzelm@43564: (** theory setup **) wenzelm@43564: wenzelm@43564: val setup = antiq_setup; wenzelm@43564: haftmann@24219: end; (*struct*)