berghofe@11520: (* Title: Pure/codegen.ML berghofe@11520: ID: $Id$ wenzelm@11539: Author: Stefan Berghofer, TU Muenchen berghofe@11520: wenzelm@11539: Generic code generator. berghofe@11520: *) berghofe@11520: berghofe@11520: signature CODEGEN = berghofe@11520: sig berghofe@11520: val quiet_mode : bool ref berghofe@11520: val message : string -> unit berghofe@13753: val mode : string list ref berghofe@13886: val margin : int ref berghofe@26974: val string_of : Pretty.T -> string berghofe@26974: val str : string -> Pretty.T berghofe@11520: berghofe@12452: datatype 'a mixfix = berghofe@11520: Arg berghofe@11520: | Ignore berghofe@16769: | Module berghofe@11520: | Pretty of Pretty.T berghofe@12452: | Quote of 'a; berghofe@11520: berghofe@16649: type deftab berghofe@17144: type node berghofe@16649: type codegr berghofe@12452: type 'a codegen berghofe@12452: berghofe@12452: val add_codegen: string -> term codegen -> theory -> theory berghofe@12452: val add_tycodegen: string -> typ codegen -> theory -> theory berghofe@15261: val add_preprocessor: (theory -> thm list -> thm list) -> theory -> theory berghofe@15261: val preprocess: theory -> thm list -> thm list berghofe@17549: val preprocess_term: theory -> term -> term berghofe@11520: val print_codegens: theory -> unit berghofe@17144: val generate_code: theory -> string list -> string -> (string * string) list -> berghofe@17144: (string * string) list * codegr berghofe@17144: val generate_code_i: theory -> string list -> string -> (string * term) list -> berghofe@17144: (string * string) list * codegr haftmann@22921: val assoc_const: string * (term mixfix list * haftmann@22921: (string * string) list) -> theory -> theory haftmann@22921: val assoc_const_i: (string * typ) * (term mixfix list * haftmann@22921: (string * string) list) -> theory -> theory haftmann@22921: val assoc_type: xstring * (typ mixfix list * haftmann@22921: (string * string) list) -> theory -> theory haftmann@22921: val get_assoc_code: theory -> string * typ -> berghofe@16769: (term mixfix list * (string * string) list) option berghofe@16769: val get_assoc_type: theory -> string -> berghofe@16769: (typ mixfix list * (string * string) list) option berghofe@17144: val codegen_error: codegr -> string -> string -> 'a berghofe@16649: val invoke_codegen: theory -> deftab -> string -> string -> bool -> haftmann@28537: term -> codegr -> Pretty.T * codegr berghofe@16649: val invoke_tycodegen: theory -> deftab -> string -> string -> bool -> haftmann@28537: typ -> codegr -> Pretty.T * codegr berghofe@14858: val mk_id: string -> string berghofe@17144: val mk_qual_id: string -> string * string -> string haftmann@28537: val mk_const_id: string -> string -> codegr -> (string * string) * codegr haftmann@28537: val get_const_id: codegr -> string -> string * string haftmann@28537: val mk_type_id: string -> string -> codegr -> (string * string) * codegr haftmann@28537: val get_type_id: codegr -> string -> string * string haftmann@27398: val thyname_of_type: theory -> string -> string haftmann@27398: val thyname_of_const: theory -> string -> string berghofe@16649: val rename_terms: term list -> term list berghofe@11520: val rename_term: term -> term berghofe@15398: val new_names: term -> string list -> string list berghofe@15398: val new_name: term -> string -> string berghofe@17144: val if_library: 'a -> 'a -> 'a berghofe@16649: val get_defn: theory -> deftab -> string -> typ -> berghofe@16649: ((typ * (string * (term list * term))) * int option) option wenzelm@24908: val is_instance: typ -> typ -> bool berghofe@11520: val parens: Pretty.T -> Pretty.T berghofe@11520: val mk_app: bool -> Pretty.T -> Pretty.T list -> Pretty.T berghofe@25892: val mk_tuple: Pretty.T list -> Pretty.T berghofe@25892: val mk_let: (Pretty.T * Pretty.T) list -> Pretty.T -> Pretty.T berghofe@11520: val eta_expand: term -> term list -> int -> term berghofe@14105: val strip_tname: string -> string berghofe@13753: val mk_type: bool -> typ -> Pretty.T berghofe@17144: val mk_term_of: codegr -> string -> bool -> typ -> Pretty.T berghofe@17144: val mk_gen: codegr -> string -> bool -> string list -> string -> typ -> Pretty.T berghofe@14105: val test_fn: (int -> (string * term) list option) ref haftmann@28315: val test_term: Proof.context -> term -> int -> term list option berghofe@24655: val eval_result: (unit -> term) ref berghofe@17549: val eval_term: theory -> term -> term haftmann@20599: val evaluation_conv: cterm -> thm berghofe@12452: val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list haftmann@18102: val quotes_of: 'a mixfix list -> 'a list haftmann@18281: val num_args_of: 'a mixfix list -> int haftmann@18102: val replace_quotes: 'b list -> 'a mixfix list -> 'b mixfix list berghofe@16649: val mk_deftab: theory -> deftab haftmann@19341: val add_unfold: thm -> theory -> theory berghofe@17549: berghofe@17144: val get_node: codegr -> string -> node berghofe@17144: val add_edge: string * string -> codegr -> codegr berghofe@17144: val add_edge_acyclic: string * string -> codegr -> codegr berghofe@17144: val del_nodes: string list -> codegr -> codegr berghofe@17144: val map_node: string -> (node -> node) -> codegr -> codegr berghofe@17144: val new_node: string * node -> codegr -> codegr haftmann@28227: haftmann@28227: val setup: theory -> theory berghofe@11520: end; berghofe@11520: berghofe@11520: structure Codegen : CODEGEN = berghofe@11520: struct berghofe@11520: berghofe@11520: val quiet_mode = ref true; berghofe@11520: fun message s = if !quiet_mode then () else writeln s; berghofe@11520: berghofe@13753: val mode = ref ([] : string list); berghofe@13753: berghofe@13886: val margin = ref 80; berghofe@13886: berghofe@26974: fun string_of p = (Pretty.string_of |> berghofe@26974: PrintMode.setmp [] |> berghofe@26974: Pretty.setmp_margin (!margin)) p; berghofe@26974: berghofe@26974: val str = PrintMode.setmp [] Pretty.str; berghofe@26974: berghofe@11520: (**** Mixfix syntax ****) berghofe@11520: berghofe@12452: datatype 'a mixfix = berghofe@11520: Arg berghofe@11520: | Ignore berghofe@16769: | Module berghofe@11520: | Pretty of Pretty.T berghofe@12452: | Quote of 'a; berghofe@11520: berghofe@11520: fun is_arg Arg = true berghofe@11520: | is_arg Ignore = true berghofe@11520: | is_arg _ = false; berghofe@11520: berghofe@12452: fun quotes_of [] = [] berghofe@12452: | quotes_of (Quote q :: ms) = q :: quotes_of ms berghofe@12452: | quotes_of (_ :: ms) = quotes_of ms; berghofe@12452: berghofe@12452: fun args_of [] xs = ([], xs) berghofe@12452: | args_of (Arg :: ms) (x :: xs) = apfst (cons x) (args_of ms xs) berghofe@12452: | args_of (Ignore :: ms) (_ :: xs) = args_of ms xs berghofe@12452: | args_of (_ :: ms) xs = args_of ms xs; berghofe@11520: haftmann@18281: fun num_args_of x = length (List.filter is_arg x); berghofe@11520: berghofe@11520: berghofe@11520: (**** theory data ****) berghofe@11520: berghofe@16649: (* preprocessed definition table *) berghofe@16649: berghofe@16649: type deftab = berghofe@16649: (typ * (* type of constant *) berghofe@16649: (string * (* name of theory containing definition of constant *) berghofe@16649: (term list * (* parameters *) berghofe@16649: term))) (* right-hand side *) berghofe@16649: list Symtab.table; berghofe@16649: berghofe@16649: (* code dependency graph *) berghofe@16649: berghofe@17144: type nametab = (string * string) Symtab.table * unit Symtab.table; berghofe@17144: haftmann@28227: fun merge_nametabs ((tab, used) : nametab, (tab', used')) = berghofe@17144: (Symtab.merge op = (tab, tab'), Symtab.merge op = (used, used')); berghofe@17144: berghofe@17144: type node = berghofe@16649: (exn option * (* slot for arbitrary data *) berghofe@16649: string * (* name of structure containing piece of code *) berghofe@17144: string); (* piece of code *) berghofe@17144: berghofe@17144: type codegr = berghofe@17144: node Graph.T * berghofe@17144: (nametab * (* table for assigned constant names *) berghofe@17144: nametab); (* table for assigned type names *) berghofe@17144: berghofe@17144: val emptygr : codegr = (Graph.empty, berghofe@17144: ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty))); berghofe@16649: berghofe@14105: (* type of code generators *) berghofe@11520: berghofe@16649: type 'a codegen = berghofe@16649: theory -> (* theory in which generate_code was called *) berghofe@16649: deftab -> (* definition table (for efficiency) *) berghofe@16649: string -> (* node name of caller (for recording dependencies) *) berghofe@17144: string -> (* module name of caller (for modular code generation) *) berghofe@16649: bool -> (* whether to parenthesize generated expression *) berghofe@16649: 'a -> (* item to generate code from *) haftmann@28537: codegr -> (* code dependency graph *) haftmann@28537: (Pretty.T * codegr) option; berghofe@12452: berghofe@14105: (* parameters for random testing *) berghofe@14105: berghofe@14105: type test_params = berghofe@14105: {size: int, iterations: int, default_type: typ option}; berghofe@14105: berghofe@14105: fun merge_test_params berghofe@14105: {size = size1, iterations = iterations1, default_type = default_type1} berghofe@14105: {size = size2, iterations = iterations2, default_type = default_type2} = berghofe@14105: {size = Int.max (size1, size2), berghofe@14105: iterations = Int.max (iterations1, iterations2), berghofe@14105: default_type = case default_type1 of skalberg@15531: NONE => default_type2 berghofe@14105: | _ => default_type1}; berghofe@14105: berghofe@14105: val default_test_params : test_params = skalberg@15531: {size = 10, iterations = 100, default_type = NONE}; berghofe@14105: berghofe@14105: fun set_size size ({iterations, default_type, ...} : test_params) = berghofe@14105: {size = size, iterations = iterations, default_type = default_type}; berghofe@14105: berghofe@14105: fun set_iterations iterations ({size, default_type, ...} : test_params) = berghofe@14105: {size = size, iterations = iterations, default_type = default_type}; berghofe@14105: wenzelm@16458: fun set_default_type s thy ({size, iterations, ...} : test_params) = berghofe@14105: {size = size, iterations = iterations, wenzelm@24707: default_type = SOME (Syntax.read_typ_global thy s)}; berghofe@14105: wenzelm@22846: wenzelm@22846: (* theory data *) wenzelm@16458: wenzelm@16458: structure CodegenData = TheoryDataFun wenzelm@22846: ( berghofe@11520: type T = berghofe@12452: {codegens : (string * term codegen) list, berghofe@12452: tycodegens : (string * typ codegen) list, berghofe@16769: consts : ((string * typ) * (term mixfix list * (string * string) list)) list, berghofe@16769: types : (string * (typ mixfix list * (string * string) list)) list, berghofe@15261: preprocs: (stamp * (theory -> thm list -> thm list)) list, berghofe@17144: modules: codegr Symtab.table, berghofe@14105: test_params: test_params}; berghofe@11520: berghofe@12555: val empty = haftmann@24219: {codegens = [], tycodegens = [], consts = [], types = [], berghofe@17144: preprocs = [], modules = Symtab.empty, test_params = default_test_params}; berghofe@11520: val copy = I; wenzelm@16458: val extend = I; berghofe@11520: wenzelm@16458: fun merge _ berghofe@12555: ({codegens = codegens1, tycodegens = tycodegens1, haftmann@24219: consts = consts1, types = types1, haftmann@28227: preprocs = preprocs1, modules = modules1, test_params = test_params1} : T, berghofe@12555: {codegens = codegens2, tycodegens = tycodegens2, haftmann@24219: consts = consts2, types = types2, berghofe@17144: preprocs = preprocs2, modules = modules2, test_params = test_params2}) = haftmann@19119: {codegens = AList.merge (op =) (K true) (codegens1, codegens2), haftmann@19119: tycodegens = AList.merge (op =) (K true) (tycodegens1, tycodegens2), haftmann@21098: consts = AList.merge (op =) (K true) (consts1, consts2), haftmann@21098: types = AList.merge (op =) (K true) (types1, types2), haftmann@19119: preprocs = AList.merge (op =) (K true) (preprocs1, preprocs2), berghofe@17144: modules = Symtab.merge (K true) (modules1, modules2), berghofe@14105: test_params = merge_test_params test_params1 test_params2}; wenzelm@22846: ); berghofe@11520: wenzelm@22846: fun print_codegens thy = wenzelm@22846: let val {codegens, tycodegens, ...} = CodegenData.get thy in berghofe@12452: Pretty.writeln (Pretty.chunks berghofe@12452: [Pretty.strs ("term code generators:" :: map fst codegens), wenzelm@22846: Pretty.strs ("type code generators:" :: map fst tycodegens)]) wenzelm@22846: end; berghofe@11520: berghofe@11520: berghofe@11520: berghofe@14105: (**** access parameters for random testing ****) berghofe@14105: berghofe@14105: fun get_test_params thy = #test_params (CodegenData.get thy); berghofe@14105: berghofe@14105: fun map_test_params f thy = haftmann@24219: let val {codegens, tycodegens, consts, types, preprocs, modules, test_params} = berghofe@14105: CodegenData.get thy; berghofe@14105: in CodegenData.put {codegens = codegens, tycodegens = tycodegens, haftmann@24219: consts = consts, types = types, preprocs = preprocs, berghofe@17144: modules = modules, test_params = f test_params} thy berghofe@17144: end; berghofe@17144: berghofe@17144: berghofe@17144: (**** access modules ****) berghofe@17144: berghofe@17144: fun get_modules thy = #modules (CodegenData.get thy); berghofe@17144: berghofe@17144: fun map_modules f thy = haftmann@24219: let val {codegens, tycodegens, consts, types, preprocs, modules, test_params} = berghofe@17144: CodegenData.get thy; berghofe@17144: in CodegenData.put {codegens = codegens, tycodegens = tycodegens, haftmann@24219: consts = consts, types = types, preprocs = preprocs, berghofe@17144: modules = f modules, test_params = test_params} thy berghofe@14105: end; berghofe@14105: berghofe@14105: berghofe@12452: (**** add new code generators to theory ****) berghofe@11520: berghofe@11520: fun add_codegen name f thy = haftmann@24219: let val {codegens, tycodegens, consts, types, preprocs, modules, test_params} = berghofe@14105: CodegenData.get thy haftmann@17521: in (case AList.lookup (op =) codegens name of skalberg@15531: NONE => CodegenData.put {codegens = (name, f) :: codegens, berghofe@12555: tycodegens = tycodegens, consts = consts, types = types, haftmann@24219: preprocs = preprocs, modules = modules, berghofe@17144: test_params = test_params} thy skalberg@15531: | SOME _ => error ("Code generator " ^ name ^ " already declared")) berghofe@12452: end; berghofe@12452: berghofe@12452: fun add_tycodegen name f thy = haftmann@24219: let val {codegens, tycodegens, consts, types, preprocs, modules, test_params} = berghofe@14105: CodegenData.get thy haftmann@17521: in (case AList.lookup (op =) tycodegens name of skalberg@15531: NONE => CodegenData.put {tycodegens = (name, f) :: tycodegens, berghofe@12555: codegens = codegens, consts = consts, types = types, haftmann@24219: preprocs = preprocs, modules = modules, berghofe@17144: test_params = test_params} thy skalberg@15531: | SOME _ => error ("Code generator " ^ name ^ " already declared")) berghofe@11520: end; berghofe@11520: berghofe@11520: berghofe@15261: (**** preprocessors ****) berghofe@15261: berghofe@15261: fun add_preprocessor p thy = haftmann@24219: let val {codegens, tycodegens, consts, types, preprocs, modules, test_params} = berghofe@15261: CodegenData.get thy berghofe@15261: in CodegenData.put {tycodegens = tycodegens, berghofe@15261: codegens = codegens, consts = consts, types = types, haftmann@24219: preprocs = (stamp (), p) :: preprocs, berghofe@17144: modules = modules, test_params = test_params} thy berghofe@15261: end; berghofe@15261: haftmann@21836: fun preprocess thy = berghofe@15261: let val {preprocs, ...} = CodegenData.get thy haftmann@21836: in fold (fn (_, f) => f thy) preprocs end; berghofe@15261: berghofe@17549: fun preprocess_term thy t = berghofe@17549: let wenzelm@20071: val x = Free (Name.variant (add_term_names (t, [])) "x", fastype_of t); berghofe@17549: (* fake definition *) berghofe@17549: val eq = setmp quick_and_dirty true (SkipProof.make_thm thy) berghofe@17549: (Logic.mk_equals (x, t)); berghofe@17549: fun err () = error "preprocess_term: bad preprocessor" berghofe@17549: in case map prop_of (preprocess thy [eq]) of berghofe@17549: [Const ("==", _) $ x' $ t'] => if x = x' then t' else err () berghofe@17549: | _ => err () berghofe@17549: end; haftmann@18281: haftmann@19341: fun add_unfold eqn = berghofe@15261: let haftmann@22749: val thy = Thm.theory_of_thm eqn; haftmann@22749: val ctxt = ProofContext.init thy; haftmann@22749: val eqn' = LocalDefs.meta_rewrite_rule ctxt eqn; haftmann@22749: val names = term_consts (fst (Logic.dest_equals (prop_of eqn'))); berghofe@15261: fun prep thy = map (fn th => berghofe@17666: let val prop = prop_of th berghofe@17666: in wenzelm@28375: if forall (fn name => exists_Const (fn (c, _) => c = name) prop) names haftmann@22749: then rewrite_rule [eqn'] (Thm.transfer thy th) berghofe@17666: else th berghofe@17666: end) haftmann@19341: in add_preprocessor prep end; berghofe@15261: berghofe@15261: berghofe@11520: (**** associate constants with target language code ****) berghofe@11520: haftmann@22921: fun gen_assoc_const prep_const (raw_const, syn) thy = berghofe@11520: let haftmann@24219: val {codegens, tycodegens, consts, types, preprocs, modules, test_params} = berghofe@14105: CodegenData.get thy; haftmann@22921: val (cname, T) = prep_const thy raw_const; berghofe@11520: in haftmann@22921: if num_args_of (fst syn) > length (binder_types T) then haftmann@22921: error ("More arguments than in corresponding type of " ^ cname) haftmann@22921: else case AList.lookup (op =) consts (cname, T) of haftmann@22921: NONE => CodegenData.put {codegens = codegens, haftmann@22921: tycodegens = tycodegens, haftmann@22921: consts = ((cname, T), syn) :: consts, haftmann@24219: types = types, preprocs = preprocs, haftmann@22921: modules = modules, test_params = test_params} thy haftmann@22921: | SOME _ => error ("Constant " ^ cname ^ " already associated with code") haftmann@22921: end; berghofe@11520: haftmann@22921: val assoc_const_i = gen_assoc_const (K I); haftmann@28054: val assoc_const = gen_assoc_const Code_Unit.read_bare_const; berghofe@11520: wenzelm@15801: berghofe@11520: (**** associate types with target language types ****) berghofe@11520: haftmann@22921: fun assoc_type (s, syn) thy = berghofe@11520: let haftmann@24219: val {codegens, tycodegens, consts, types, preprocs, modules, test_params} = berghofe@14105: CodegenData.get thy; haftmann@22921: val tc = Sign.intern_type thy s; berghofe@11520: in berghofe@18320: case Symtab.lookup (snd (#types (Type.rep_tsig (Sign.tsig_of thy)))) tc of haftmann@27302: SOME ((Type.LogicalType i, _), _) => berghofe@18320: if num_args_of (fst syn) > i then berghofe@18320: error ("More arguments than corresponding type constructor " ^ s) berghofe@18320: else (case AList.lookup (op =) types tc of berghofe@18320: NONE => CodegenData.put {codegens = codegens, berghofe@18320: tycodegens = tycodegens, consts = consts, haftmann@24219: types = (tc, syn) :: types, berghofe@18320: preprocs = preprocs, modules = modules, test_params = test_params} thy berghofe@18320: | SOME _ => error ("Type " ^ tc ^ " already associated with code")) berghofe@18320: | _ => error ("Not a type constructor: " ^ s) haftmann@22921: end; berghofe@11520: haftmann@21098: fun get_assoc_type thy = AList.lookup (op =) ((#types o CodegenData.get) thy); wenzelm@11546: berghofe@11520: berghofe@11520: (**** make valid ML identifiers ****) berghofe@11520: berghofe@14858: fun is_ascii_letdig x = Symbol.is_ascii_letter x orelse berghofe@14858: Symbol.is_ascii_digit x orelse Symbol.is_ascii_quasi x; berghofe@14858: wenzelm@28375: fun dest_sym s = (case split_last (snd (take_prefix (fn c => c = "\\") (explode s))) of berghofe@14858: ("<" :: "^" :: xs, ">") => (true, implode xs) berghofe@14858: | ("<" :: xs, ">") => (false, implode xs) berghofe@14858: | _ => sys_error "dest_sym"); wenzelm@16458: berghofe@14858: fun mk_id s = if s = "" then "" else berghofe@11520: let berghofe@14858: fun check_str [] = [] berghofe@14858: | check_str xs = (case take_prefix is_ascii_letdig xs of berghofe@14858: ([], " " :: zs) => check_str zs berghofe@14858: | ([], z :: zs) => berghofe@14858: if size z = 1 then string_of_int (ord z) :: check_str zs berghofe@14858: else (case dest_sym z of berghofe@14858: (true, "isub") => check_str zs berghofe@14858: | (true, "isup") => "" :: check_str zs berghofe@14858: | (ctrl, s') => (if ctrl then "ctrl_" ^ s' else s') :: check_str zs) berghofe@14858: | (ys, zs) => implode ys :: check_str zs); wenzelm@21858: val s' = space_implode "_" (maps (check_str o Symbol.explode) (NameSpace.explode s)) berghofe@11520: in berghofe@14858: if Symbol.is_ascii_letter (hd (explode s')) then s' else "id_" ^ s' berghofe@11520: end; berghofe@11520: berghofe@17144: fun mk_long_id (p as (tab, used)) module s = berghofe@16649: let berghofe@17144: fun find_name [] = sys_error "mk_long_id" berghofe@17144: | find_name (ys :: yss) = berghofe@17144: let wenzelm@21858: val s' = NameSpace.implode ys berghofe@17144: val s'' = NameSpace.append module s' wenzelm@17412: in case Symtab.lookup used s'' of wenzelm@17261: NONE => ((module, s'), wenzelm@17412: (Symtab.update_new (s, (module, s')) tab, wenzelm@17412: Symtab.update_new (s'', ()) used)) berghofe@17144: | SOME _ => find_name yss berghofe@17144: end wenzelm@17412: in case Symtab.lookup tab s of wenzelm@21858: NONE => find_name (Library.suffixes1 (NameSpace.explode s)) berghofe@17144: | SOME name => (name, p) berghofe@16649: end; berghofe@16649: berghofe@17144: (* module: module name for caller *) berghofe@17144: (* module': module name for callee *) berghofe@17144: (* if caller and callee reside in different modules, use qualified access *) berghofe@16649: berghofe@17144: fun mk_qual_id module (module', s) = berghofe@17144: if module = module' orelse module' = "" then s else module' ^ "." ^ s; berghofe@17144: berghofe@17144: fun mk_const_id module cname (gr, (tab1, tab2)) = berghofe@16649: let berghofe@17144: val ((module, s), tab1') = mk_long_id tab1 module cname berghofe@17144: val s' = mk_id s; wenzelm@21478: val s'' = if ML_Syntax.is_reserved s' then s' ^ "_const" else s' haftmann@28537: in (((module, s'')), (gr, (tab1', tab2))) end; berghofe@13073: haftmann@28537: fun get_const_id (gr, (tab1, tab2)) cname = wenzelm@17412: case Symtab.lookup (fst tab1) cname of berghofe@17144: NONE => error ("get_const_id: no such constant: " ^ quote cname) berghofe@17144: | SOME (module, s) => berghofe@17144: let berghofe@17144: val s' = mk_id s; wenzelm@21478: val s'' = if ML_Syntax.is_reserved s' then s' ^ "_const" else s' berghofe@17144: in (module, s'') end; berghofe@17144: berghofe@17144: fun mk_type_id module tyname (gr, (tab1, tab2)) = berghofe@16649: let berghofe@17144: val ((module, s), tab2') = mk_long_id tab2 module tyname berghofe@17144: val s' = mk_id s; wenzelm@21478: val s'' = if ML_Syntax.is_reserved s' then s' ^ "_type" else s' haftmann@28537: in ((module, s''), (gr, (tab1, tab2'))) end; berghofe@16649: haftmann@28537: fun get_type_id (gr, (tab1, tab2)) tyname = wenzelm@17412: case Symtab.lookup (fst tab2) tyname of berghofe@17144: NONE => error ("get_type_id: no such type: " ^ quote tyname) berghofe@17144: | SOME (module, s) => berghofe@17144: let berghofe@17144: val s' = mk_id s; wenzelm@21478: val s'' = if ML_Syntax.is_reserved s' then s' ^ "_type" else s' berghofe@17144: in (module, s'') end; berghofe@17144: haftmann@28537: fun get_type_id' f tab tyname = apsnd f (get_type_id tab tyname); berghofe@17144: berghofe@17144: fun get_node (gr, x) k = Graph.get_node gr k; berghofe@17144: fun add_edge e (gr, x) = (Graph.add_edge e gr, x); berghofe@17144: fun add_edge_acyclic e (gr, x) = (Graph.add_edge_acyclic e gr, x); berghofe@17144: fun del_nodes ks (gr, x) = (Graph.del_nodes ks gr, x); berghofe@17144: fun map_node k f (gr, x) = (Graph.map_node k f gr, x); berghofe@17144: fun new_node p (gr, x) = (Graph.new_node p gr, x); berghofe@16649: haftmann@27398: fun thyname_of thy f x = the (AList.lookup (op =) (f x) Markup.theory_nameN); berghofe@16649: haftmann@27398: fun thyname_of_type thy = haftmann@27398: thyname_of thy (Type.the_tags (Sign.tsig_of thy)); berghofe@16649: haftmann@27398: fun thyname_of_const thy = haftmann@27398: thyname_of thy (Consts.the_tags (Sign.consts_of thy)); berghofe@11520: berghofe@13731: fun rename_terms ts = berghofe@11520: let wenzelm@23178: val names = List.foldr add_term_names wenzelm@20286: (map (fst o fst) (rev (fold Term.add_vars ts []))) ts; wenzelm@21478: val reserved = filter ML_Syntax.is_reserved names; wenzelm@19482: val (illegal, alt_names) = split_list (map_filter (fn s => skalberg@15531: let val s' = mk_id s in if s = s' then NONE else SOME (s, s') end) names) berghofe@14858: val ps = (reserved @ illegal) ~~ wenzelm@20071: Name.variant_list names (map (suffix "'") reserved @ alt_names); berghofe@11520: haftmann@17521: fun rename_id s = AList.lookup (op =) ps s |> the_default s; berghofe@14858: berghofe@14858: fun rename (Var ((a, i), T)) = Var ((rename_id a, i), T) berghofe@14858: | rename (Free (a, T)) = Free (rename_id a, T) berghofe@11520: | rename (Abs (s, T, t)) = Abs (s, T, rename t) berghofe@11520: | rename (t $ u) = rename t $ rename u berghofe@11520: | rename t = t; berghofe@11520: in berghofe@13731: map rename ts berghofe@13731: end; berghofe@13731: berghofe@13731: val rename_term = hd o rename_terms o single; berghofe@13731: berghofe@13731: berghofe@13731: (**** retrieve definition of constant ****) berghofe@13731: wenzelm@24908: fun is_instance T1 T2 = wenzelm@24908: Type.raw_instance (T1, Logic.legacy_varifyT T2); berghofe@13731: haftmann@22921: fun get_assoc_code thy (s, T) = Option.map snd (find_first (fn ((s', T'), _) => wenzelm@24908: s = s' andalso is_instance T T') (#consts (CodegenData.get thy))); berghofe@13731: wenzelm@19482: fun get_aux_code xs = map_filter (fn (m, code) => wenzelm@20665: if m = "" orelse member (op =) (!mode) m then SOME code else NONE) xs; berghofe@16769: berghofe@16649: fun mk_deftab thy = berghofe@13731: let wenzelm@22680: val axmss = map (fn thy' => (Context.theory_name thy', Theory.axiom_table thy')) berghofe@16649: (thy :: Theory.ancestors_of thy); berghofe@15261: fun prep_def def = (case preprocess thy [def] of berghofe@16649: [def'] => prop_of def' | _ => error "mk_deftab: bad preprocessor"); berghofe@15261: fun dest t = berghofe@15261: let berghofe@15261: val (lhs, rhs) = Logic.dest_equals t; berghofe@15261: val (c, args) = strip_comb lhs; berghofe@16649: val (s, T) = dest_Const c berghofe@16649: in if forall is_Var args then SOME (s, (T, (args, rhs))) else NONE skalberg@15531: end handle TERM _ => NONE; haftmann@21056: fun add_def thyname (name, t) = (case dest t of haftmann@21056: NONE => I wenzelm@24908: | SOME _ => (case dest (prep_def (Thm.get_axiom_i thy name)) of haftmann@21056: NONE => I haftmann@21056: | SOME (s, (T, (args, rhs))) => Symtab.map_default (s, []) haftmann@21056: (cons (T, (thyname, split_last (rename_terms (args @ [rhs]))))))) berghofe@13731: in haftmann@21056: fold (fn (thyname, axms) => Symtab.fold (add_def thyname) axms) axmss Symtab.empty berghofe@11520: end; berghofe@11520: wenzelm@17412: fun get_defn thy defs s T = (case Symtab.lookup defs s of berghofe@16649: NONE => NONE berghofe@16649: | SOME ds => wenzelm@24908: let val i = find_index (is_instance T o fst) ds berghofe@16649: in if i >= 0 then berghofe@16649: SOME (List.nth (ds, i), if length ds = 1 then NONE else SOME i) berghofe@16649: else NONE berghofe@16649: end); berghofe@16649: berghofe@11520: berghofe@12452: (**** invoke suitable code generator for term / type ****) berghofe@11520: berghofe@17144: fun codegen_error (gr, _) dep s = berghofe@17144: error (s ^ "\nrequired by:\n" ^ commas (Graph.all_succs gr [dep])); berghofe@17144: haftmann@28537: fun invoke_codegen thy defs dep module brack t gr = (case get_first haftmann@28537: (fn (_, f) => f thy defs dep module brack t gr) (#codegens (CodegenData.get thy)) of berghofe@17144: NONE => codegen_error gr dep ("Unable to generate code for term:\n" ^ wenzelm@26939: Syntax.string_of_term_global thy t) skalberg@15531: | SOME x => x); berghofe@12452: haftmann@28537: fun invoke_tycodegen thy defs dep module brack T gr = (case get_first haftmann@28537: (fn (_, f) => f thy defs dep module brack T gr ) (#tycodegens (CodegenData.get thy)) of berghofe@17144: NONE => codegen_error gr dep ("Unable to generate code for type:\n" ^ wenzelm@26939: Syntax.string_of_typ_global thy T) skalberg@15531: | SOME x => x); berghofe@11520: berghofe@11520: berghofe@11520: (**** code generator for mixfix expressions ****) berghofe@11520: berghofe@26974: fun parens p = Pretty.block [str "(", p, str ")"]; berghofe@11520: berghofe@11520: fun pretty_fn [] p = [p] berghofe@26974: | pretty_fn (x::xs) p = str ("fn " ^ x ^ " =>") :: berghofe@11520: Pretty.brk 1 :: pretty_fn xs p; berghofe@11520: berghofe@16769: fun pretty_mixfix _ _ [] [] _ = [] berghofe@16769: | pretty_mixfix module module' (Arg :: ms) (p :: ps) qs = berghofe@16769: p :: pretty_mixfix module module' ms ps qs berghofe@16769: | pretty_mixfix module module' (Ignore :: ms) ps qs = berghofe@16769: pretty_mixfix module module' ms ps qs berghofe@16769: | pretty_mixfix module module' (Module :: ms) ps qs = berghofe@17144: (if module <> module' berghofe@26974: then cons (str (module' ^ ".")) else I) berghofe@16769: (pretty_mixfix module module' ms ps qs) berghofe@16769: | pretty_mixfix module module' (Pretty p :: ms) ps qs = berghofe@16769: p :: pretty_mixfix module module' ms ps qs berghofe@16769: | pretty_mixfix module module' (Quote _ :: ms) ps (q :: qs) = berghofe@16769: q :: pretty_mixfix module module' ms ps qs; berghofe@11520: haftmann@18102: fun replace_quotes [] [] = [] haftmann@18102: | replace_quotes xs (Arg :: ms) = haftmann@18102: Arg :: replace_quotes xs ms haftmann@18102: | replace_quotes xs (Ignore :: ms) = haftmann@18102: Ignore :: replace_quotes xs ms haftmann@18102: | replace_quotes xs (Module :: ms) = haftmann@18102: Module :: replace_quotes xs ms haftmann@18102: | replace_quotes xs (Pretty p :: ms) = haftmann@18102: Pretty p :: replace_quotes xs ms haftmann@18102: | replace_quotes (x::xs) (Quote _ :: ms) = haftmann@18102: Quote x :: replace_quotes xs ms; haftmann@18102: berghofe@11520: berghofe@12452: (**** default code generators ****) berghofe@11520: berghofe@11520: fun eta_expand t ts i = berghofe@11520: let berghofe@24456: val k = length ts; berghofe@24456: val Ts = Library.drop (k, binder_types (fastype_of t)); berghofe@24456: val j = i - k berghofe@11520: in wenzelm@23178: List.foldr (fn (T, t) => Abs ("x", T, t)) skalberg@15574: (list_comb (t, ts @ map Bound (j-1 downto 0))) (Library.take (j, Ts)) berghofe@11520: end; berghofe@11520: berghofe@11520: fun mk_app _ p [] = p berghofe@11520: | mk_app brack p ps = if brack then berghofe@26974: Pretty.block (str "(" :: berghofe@26974: separate (Pretty.brk 1) (p :: ps) @ [str ")"]) berghofe@11520: else Pretty.block (separate (Pretty.brk 1) (p :: ps)); berghofe@11520: wenzelm@20071: fun new_names t xs = Name.variant_list wenzelm@20071: (map (fst o fst o dest_Var) (term_vars t) union wenzelm@21719: add_term_names (t, ML_Syntax.reserved_names)) (map mk_id xs); berghofe@11520: berghofe@11520: fun new_name t x = hd (new_names t [x]); berghofe@11520: wenzelm@20665: fun if_library x y = if member (op =) (!mode) "library" then x else y; berghofe@17144: haftmann@28537: fun default_codegen thy defs dep module brack t gr = berghofe@11520: let berghofe@11520: val (u, ts) = strip_comb t; haftmann@28537: fun codegens brack = fold_map (invoke_codegen thy defs dep module brack) berghofe@11520: in (case u of berghofe@14105: Var ((s, i), T) => berghofe@14105: let haftmann@28537: val (ps, gr') = codegens true ts gr; haftmann@28537: val (_, gr'') = invoke_tycodegen thy defs dep module false T gr' haftmann@28537: in SOME (mk_app brack (str (s ^ haftmann@28537: (if i=0 then "" else string_of_int i))) ps, gr'') berghofe@11520: end berghofe@11520: berghofe@14105: | Free (s, T) => berghofe@14105: let haftmann@28537: val (ps, gr') = codegens true ts gr; haftmann@28537: val (_, gr'') = invoke_tycodegen thy defs dep module false T gr' haftmann@28537: in SOME (mk_app brack (str s) ps, gr'') end berghofe@11520: berghofe@11520: | Const (s, T) => haftmann@22921: (case get_assoc_code thy (s, T) of berghofe@16769: SOME (ms, aux) => haftmann@18281: let val i = num_args_of ms berghofe@11520: in if length ts < i then haftmann@28537: default_codegen thy defs dep module brack (eta_expand u ts i) gr berghofe@11520: else berghofe@11520: let berghofe@12452: val (ts1, ts2) = args_of ms ts; haftmann@28537: val (ps1, gr1) = codegens false ts1 gr; haftmann@28537: val (ps2, gr2) = codegens true ts2 gr1; haftmann@28537: val (ps3, gr3) = codegens false (quotes_of ms) gr2; haftmann@28537: val (_, gr4) = invoke_tycodegen thy defs dep module false haftmann@28537: (funpow (length ts) (hd o tl o snd o dest_Type) T) gr3; berghofe@17144: val (module', suffix) = (case get_defn thy defs s T of haftmann@27398: NONE => (if_library (thyname_of_const thy s) module, "") berghofe@17144: | SOME ((U, (module', _)), NONE) => berghofe@17144: (if_library module' module, "") berghofe@17144: | SOME ((U, (module', _)), SOME i) => berghofe@17144: (if_library module' module, " def" ^ string_of_int i)); berghofe@16769: val node_id = s ^ suffix; berghofe@17144: fun p module' = mk_app brack (Pretty.block berghofe@17144: (pretty_mixfix module module' ms ps1 ps3)) ps2 berghofe@17549: in SOME (case try (get_node gr4) node_id of berghofe@16769: NONE => (case get_aux_code aux of haftmann@28537: [] => (p module, gr4) haftmann@28537: | xs => (p module', add_edge (node_id, dep) (new_node haftmann@28537: (node_id, (NONE, module', cat_lines xs ^ "\n")) gr4))) berghofe@17144: | SOME (_, module'', _) => haftmann@28537: (p module'', add_edge (node_id, dep) gr4)) berghofe@11520: end berghofe@11520: end berghofe@16649: | NONE => (case get_defn thy defs s T of skalberg@15531: NONE => NONE berghofe@17144: | SOME ((U, (thyname, (args, rhs))), k) => berghofe@11520: let berghofe@17144: val module' = if_library thyname module; berghofe@17144: val suffix = (case k of NONE => "" | SOME i => " def" ^ string_of_int i); berghofe@16649: val node_id = s ^ suffix; haftmann@28537: val ((ps, def_id), gr') = gr |> codegens true ts haftmann@28537: ||>> mk_const_id module' (s ^ suffix); berghofe@26974: val p = mk_app brack (str (mk_qual_id module def_id)) ps berghofe@17144: in SOME (case try (get_node gr') node_id of berghofe@17144: NONE => berghofe@17144: let berghofe@17144: val _ = message ("expanding definition of " ^ s); berghofe@18788: val (Ts, _) = strip_type U; berghofe@17144: val (args', rhs') = berghofe@17144: if not (null args) orelse null Ts then (args, rhs) else berghofe@17144: let val v = Free (new_name rhs "x", hd Ts) berghofe@17144: in ([v], betapply (rhs, v)) end; haftmann@28537: val (p', gr1) = invoke_codegen thy defs node_id module' false haftmann@28537: rhs' (add_edge (node_id, dep) haftmann@28537: (new_node (node_id, (NONE, "", "")) gr')); haftmann@28537: val (xs, gr2) = codegens false args' gr1; haftmann@28537: val (_, gr3) = invoke_tycodegen thy defs dep module false T gr2; haftmann@28537: val (ty, gr4) = invoke_tycodegen thy defs node_id module' false U gr3; haftmann@28537: in (p, map_node node_id (K (NONE, module', string_of berghofe@17144: (Pretty.block (separate (Pretty.brk 1) berghofe@17144: (if null args' then berghofe@26974: [str ("val " ^ snd def_id ^ " :"), ty] berghofe@26974: else str ("fun " ^ snd def_id) :: xs) @ haftmann@28537: [str " =", Pretty.brk 1, p', str ";"])) ^ "\n\n")) gr4) berghofe@17144: end haftmann@28537: | SOME _ => (p, add_edge (node_id, dep) gr')) berghofe@11520: end)) berghofe@11520: berghofe@11520: | Abs _ => berghofe@11520: let berghofe@11520: val (bs, Ts) = ListPair.unzip (strip_abs_vars u); berghofe@11520: val t = strip_abs_body u berghofe@11520: val bs' = new_names t bs; haftmann@28537: val (ps, gr1) = codegens true ts gr; haftmann@28537: val (p, gr2) = invoke_codegen thy defs dep module false haftmann@28537: (subst_bounds (map Free (rev (bs' ~~ Ts)), t)) gr1; berghofe@11520: in haftmann@28537: SOME (mk_app brack (Pretty.block (str "(" :: pretty_fn bs' p @ haftmann@28537: [str ")"])) ps, gr2) berghofe@11520: end berghofe@11520: skalberg@15531: | _ => NONE) berghofe@11520: end; berghofe@11520: haftmann@28537: fun default_tycodegen thy defs dep module brack (TVar ((s, i), _)) gr = haftmann@28537: SOME (str (s ^ (if i = 0 then "" else string_of_int i)), gr) haftmann@28537: | default_tycodegen thy defs dep module brack (TFree (s, _)) gr = haftmann@28537: SOME (str s, gr) haftmann@28537: | default_tycodegen thy defs dep module brack (Type (s, Ts)) gr = haftmann@17521: (case AList.lookup (op =) ((#types o CodegenData.get) thy) s of skalberg@15531: NONE => NONE berghofe@16769: | SOME (ms, aux) => berghofe@12452: let haftmann@28537: val (ps, gr') = fold_map berghofe@17144: (invoke_tycodegen thy defs dep module false) haftmann@28537: (fst (args_of ms Ts)) gr; haftmann@28537: val (qs, gr'') = fold_map berghofe@17144: (invoke_tycodegen thy defs dep module false) haftmann@28537: (quotes_of ms) gr'; haftmann@27398: val module' = if_library (thyname_of_type thy s) module; berghofe@16769: val node_id = s ^ " (type)"; berghofe@17144: fun p module' = Pretty.block (pretty_mixfix module module' ms ps qs) berghofe@17144: in SOME (case try (get_node gr'') node_id of berghofe@16769: NONE => (case get_aux_code aux of haftmann@28537: [] => (p module', gr'') haftmann@28537: | xs => (p module', snd (mk_type_id module' s berghofe@17144: (add_edge (node_id, dep) (new_node (node_id, haftmann@28537: (NONE, module', cat_lines xs ^ "\n")) gr''))))) berghofe@17144: | SOME (_, module'', _) => haftmann@28537: (p module'', add_edge (node_id, dep) gr'')) berghofe@16769: end); berghofe@12452: berghofe@25892: fun mk_tuple [p] = p berghofe@26974: | mk_tuple ps = Pretty.block (str "(" :: berghofe@26974: List.concat (separate [str ",", Pretty.brk 1] (map single ps)) @ berghofe@26974: [str ")"]); berghofe@25892: berghofe@25892: fun mk_let bindings body = berghofe@26974: Pretty.blk (0, [str "let", Pretty.brk 1, berghofe@25892: Pretty.blk (0, separate Pretty.fbrk (map (fn (pat, rhs) => berghofe@26974: Pretty.block [str "val ", pat, str " =", Pretty.brk 1, berghofe@26974: rhs, str ";"]) bindings)), berghofe@26974: Pretty.brk 1, str "in", Pretty.brk 1, body, berghofe@26974: Pretty.brk 1, str "end"]); berghofe@25892: berghofe@16649: fun mk_struct name s = "structure " ^ name ^ " =\nstruct\n\n" ^ s ^ "end;\n"; berghofe@16649: haftmann@28227: fun add_to_module name s = AList.map_entry (op =) (name : string) (suffix s); berghofe@16649: berghofe@17144: fun output_code gr module xs = berghofe@16649: let wenzelm@19482: val code = map_filter (fn s => berghofe@17144: let val c as (_, module', _) = Graph.get_node gr s berghofe@17144: in if module = "" orelse module = module' then SOME (s, c) else NONE end) berghofe@17144: (rev (Graph.all_preds gr xs)); berghofe@16649: fun string_of_cycle (a :: b :: cs) = berghofe@16649: let val SOME (x, y) = get_first (fn (x, (_, a', _)) => berghofe@16649: if a = a' then Option.map (pair x) wenzelm@28375: (find_first ((fn (_, b', _) => b' = b) o Graph.get_node gr) berghofe@16649: (Graph.imm_succs gr x)) berghofe@16649: else NONE) code berghofe@16649: in x ^ " called by " ^ y ^ "\n" ^ string_of_cycle (b :: cs) end berghofe@16649: | string_of_cycle _ = "" berghofe@16649: in berghofe@17144: if module = "" then berghofe@16649: let wenzelm@19046: val modules = distinct (op =) (map (#2 o snd) code); wenzelm@23178: val mod_gr = fold_rev Graph.add_edge_acyclic wenzelm@19482: (maps (fn (s, (_, module, _)) => map (pair module) wenzelm@28375: (filter_out (fn s => s = module) (map (#2 o Graph.get_node gr) wenzelm@23178: (Graph.imm_succs gr s)))) code) wenzelm@23178: (fold_rev (Graph.new_node o rpair ()) modules Graph.empty); berghofe@16649: val modules' = berghofe@16649: rev (Graph.all_preds mod_gr (map (#2 o Graph.get_node gr) xs)) berghofe@16649: in wenzelm@23178: List.foldl (fn ((_, (_, module, s)), ms) => add_to_module module s ms) berghofe@16649: (map (rpair "") modules') code berghofe@16649: end handle Graph.CYCLES (cs :: _) => berghofe@16649: error ("Cyclic dependency of modules:\n" ^ commas cs ^ berghofe@16649: "\n" ^ string_of_cycle cs) berghofe@17144: else [(module, implode (map (#3 o snd) code))] berghofe@16649: end; berghofe@11520: berghofe@26974: fun gen_generate_code prep_term thy modules module xs = berghofe@11520: let wenzelm@21858: val _ = (module <> "" orelse wenzelm@28375: member (op =) (!mode) "library" andalso forall (fn (s, _) => s = "") xs) wenzelm@21858: orelse error "missing module name"; berghofe@17144: val graphs = get_modules thy; berghofe@16649: val defs = mk_deftab thy; berghofe@17144: val gr = new_node ("", (NONE, module, "")) wenzelm@23178: (List.foldl (fn ((gr, (tab1, tab2)), (gr', (tab1', tab2'))) => berghofe@17144: (Graph.merge (fn ((_, module, _), (_, module', _)) => berghofe@17144: module = module') (gr, gr'), berghofe@17144: (merge_nametabs (tab1, tab1'), merge_nametabs (tab2, tab2')))) emptygr wenzelm@17412: (map (fn s => case Symtab.lookup graphs s of berghofe@17144: NONE => error ("Undefined code module: " ^ s) berghofe@17144: | SOME gr => gr) modules)) wenzelm@23655: handle Graph.DUP k => error ("Duplicate code for " ^ k); berghofe@16649: fun expand (t as Abs _) = t berghofe@16649: | expand t = (case fastype_of t of berghofe@16649: Type ("fun", [T, U]) => Abs ("x", T, t $ Bound 0) | _ => t); haftmann@28537: val (ps, gr') = fold_map (fn (s, t) => fn gr => apfst (pair s) haftmann@28537: (invoke_codegen thy defs "" module false t gr)) haftmann@28537: (map (apsnd (expand o preprocess_term thy o prep_term thy)) xs) gr; wenzelm@19482: val code = map_filter berghofe@17144: (fn ("", _) => NONE berghofe@26974: | (s', p) => SOME (string_of (Pretty.block berghofe@26974: [str ("val " ^ s' ^ " ="), Pretty.brk 1, p, str ";"]))) ps; berghofe@17144: val code' = space_implode "\n\n" code ^ "\n\n"; berghofe@17144: val code'' = wenzelm@19482: map_filter (fn (name, s) => wenzelm@20665: if member (op =) (!mode) "library" andalso name = module andalso null code berghofe@17144: then NONE berghofe@17144: else SOME (name, mk_struct name s)) berghofe@17144: ((if null code then I berghofe@17144: else add_to_module module code') berghofe@17144: (output_code (fst gr') (if_library "" module) [""])) berghofe@16649: in berghofe@17144: (code'', del_nodes [""] gr') berghofe@26974: end; berghofe@11520: wenzelm@22680: val generate_code_i = gen_generate_code Sign.cert_term; wenzelm@27251: val generate_code = gen_generate_code OldGoals.read_term; berghofe@11520: berghofe@12452: berghofe@13753: (**** Reflection ****) berghofe@13753: berghofe@13753: val strip_tname = implode o tl o explode; berghofe@13753: berghofe@26974: fun pretty_list xs = Pretty.block (str "[" :: berghofe@26974: flat (separate [str ",", Pretty.brk 1] (map single xs)) @ berghofe@26974: [str "]"]); berghofe@13753: berghofe@26974: fun mk_type p (TVar ((s, i), _)) = str berghofe@13753: (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "T") berghofe@26974: | mk_type p (TFree (s, _)) = str (strip_tname s ^ "T") berghofe@13753: | mk_type p (Type (s, Ts)) = (if p then parens else I) (Pretty.block berghofe@26974: [str "Type", Pretty.brk 1, str ("(\"" ^ s ^ "\","), berghofe@26974: Pretty.brk 1, pretty_list (map (mk_type false) Ts), str ")"]); berghofe@13753: berghofe@26974: fun mk_term_of gr module p (TVar ((s, i), _)) = str berghofe@13753: (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "F") berghofe@26974: | mk_term_of gr module p (TFree (s, _)) = str (strip_tname s ^ "F") berghofe@17144: | mk_term_of gr module p (Type (s, Ts)) = (if p then parens else I) berghofe@16649: (Pretty.block (separate (Pretty.brk 1) berghofe@26974: (str (mk_qual_id module haftmann@28537: (get_type_id' (fn s' => "term_of_" ^ s') gr s)) :: wenzelm@19482: maps (fn T => wenzelm@19482: [mk_term_of gr module true T, mk_type true T]) Ts))); berghofe@13753: berghofe@13753: berghofe@14105: (**** Test data generators ****) berghofe@14105: berghofe@26974: fun mk_gen gr module p xs a (TVar ((s, i), _)) = str berghofe@14105: (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "G") berghofe@26974: | mk_gen gr module p xs a (TFree (s, _)) = str (strip_tname s ^ "G") berghofe@25892: | mk_gen gr module p xs a (Type (tyc as (s, Ts))) = (if p then parens else I) berghofe@16649: (Pretty.block (separate (Pretty.brk 1) haftmann@28537: (str (mk_qual_id module (get_type_id' (fn s' => "gen_" ^ s') gr s) ^ wenzelm@20665: (if member (op =) xs s then "'" else "")) :: berghofe@25892: (case tyc of berghofe@25892: ("fun", [T, U]) => berghofe@25892: [mk_term_of gr module true T, mk_type true T, berghofe@25892: mk_gen gr module true xs a U, mk_type true U] berghofe@25892: | _ => maps (fn T => berghofe@25892: [mk_gen gr module true xs a T, mk_type true T]) Ts) @ berghofe@26974: (if member (op =) xs s then [str a] else [])))); berghofe@14105: skalberg@15531: val test_fn : (int -> (string * term) list option) ref = ref (fn _ => NONE); berghofe@14105: haftmann@28315: fun test_term ctxt t = haftmann@28309: let haftmann@28309: val thy = ProofContext.theory_of ctxt; haftmann@28309: val (code, gr) = setmp mode ["term_of", "test"] haftmann@28309: (generate_code_i thy [] "Generated") [("testf", t)]; haftmann@28309: val frees = Name.names Name.context "a" ((map snd o fst o strip_abs) t); haftmann@28309: val frees' = frees ~~ haftmann@28309: map (fn i => "arg" ^ string_of_int i) (1 upto length frees); haftmann@28309: val s = "structure TestTerm =\nstruct\n\n" ^ haftmann@28309: cat_lines (map snd code) ^ haftmann@28309: "\nopen Generated;\n\n" ^ string_of haftmann@28309: (Pretty.block [str "val () = Codegen.test_fn :=", haftmann@28309: Pretty.brk 1, str ("(fn i =>"), Pretty.brk 1, haftmann@28309: mk_let (map (fn ((s, T), s') => haftmann@28309: (mk_tuple [str s', str (s' ^ "_t")], haftmann@28309: Pretty.block [mk_gen gr "Generated" false [] "" T, Pretty.brk 1, haftmann@28309: str "(i + 1)"])) frees') haftmann@28309: (Pretty.block [str "if ", haftmann@28309: mk_app false (str "testf") (map (str o snd) frees'), haftmann@28309: Pretty.brk 1, str "then NONE", haftmann@28309: Pretty.brk 1, str "else ", haftmann@28309: Pretty.block [str "SOME ", Pretty.block (str "[" :: haftmann@28309: flat (separate [str ",", Pretty.brk 1] haftmann@28309: (map (fn ((s, T), s') => [Pretty.block haftmann@28309: [str ("(" ^ quote (Symbol.escape s) ^ ","), Pretty.brk 1, haftmann@28309: str (s' ^ "_t ())")]]) frees')) @ haftmann@28309: [str "]"])]]), haftmann@28309: str ");"]) ^ haftmann@28309: "\n\nend;\n"; haftmann@28309: val _ = ML_Context.eval_in (SOME ctxt) false Position.none s; haftmann@28309: in ! test_fn #> (Option.map o map) snd end; haftmann@28309: berghofe@24456: berghofe@14105: berghofe@17549: (**** Evaluator for terms ****) berghofe@17549: berghofe@24655: val eval_result = ref (fn () => Bound 0); berghofe@17549: wenzelm@25009: fun eval_term thy t = wenzelm@28271: let wenzelm@28271: val ctxt = ProofContext.init thy; wenzelm@28271: val e = wenzelm@28271: let wenzelm@28271: val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse wenzelm@28271: error "Term to be evaluated contains type variables"; wenzelm@28271: val _ = (null (term_vars t) andalso null (term_frees t)) orelse wenzelm@28271: error "Term to be evaluated contains variables"; wenzelm@28271: val (code, gr) = setmp mode ["term_of"] wenzelm@28271: (generate_code_i thy [] "Generated") wenzelm@28271: [("result", Abs ("x", TFree ("'a", []), t))]; wenzelm@28271: val s = "structure EvalTerm =\nstruct\n\n" ^ wenzelm@28271: cat_lines (map snd code) ^ wenzelm@28271: "\nopen Generated;\n\n" ^ string_of wenzelm@28271: (Pretty.block [str "val () = Codegen.eval_result := (fn () =>", wenzelm@28271: Pretty.brk 1, wenzelm@28271: mk_app false (mk_term_of gr "Generated" false (fastype_of t)) wenzelm@28271: [str "(result ())"], wenzelm@28271: str ");"]) ^ wenzelm@28271: "\n\nend;\n"; wenzelm@28293: val _ = NAMED_CRITICAL "codegen" (fn () => wenzelm@28293: ML_Context.eval_in (SOME ctxt) false Position.none s); wenzelm@28271: in !eval_result end; wenzelm@25009: in e () end; berghofe@17549: wenzelm@28293: val (_, evaluation_conv) = Context.>>> (Context.map_theory_result wenzelm@28293: (Thm.add_oracle ("evaluation", fn ct => wenzelm@28293: let wenzelm@28293: val thy = Thm.theory_of_cterm ct; wenzelm@28293: val t = Thm.term_of ct; wenzelm@28293: in Thm.cterm_of thy (Logic.mk_equals (t, eval_term thy t)) end))); haftmann@20599: berghofe@17549: berghofe@12452: (**** Interface ****) berghofe@12452: berghofe@11520: fun parse_mixfix rd s = berghofe@11520: (case Scan.finite Symbol.stopper (Scan.repeat berghofe@11520: ( $$ "_" >> K Arg berghofe@11520: || $$ "?" >> K Ignore berghofe@16769: || $$ "\\" >> K Module berghofe@11520: || $$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length) berghofe@11520: || $$ "{" |-- $$ "*" |-- Scan.repeat1 wenzelm@23784: ( $$ "'" |-- Scan.one Symbol.is_regular wenzelm@23784: || Scan.unless ($$ "*" -- $$ "}") (Scan.one Symbol.is_regular)) --| berghofe@12452: $$ "*" --| $$ "}" >> (Quote o rd o implode) berghofe@11520: || Scan.repeat1 wenzelm@23784: ( $$ "'" |-- Scan.one Symbol.is_regular berghofe@16769: || Scan.unless ($$ "_" || $$ "?" || $$ "\\" || $$ "/" || $$ "{" |-- $$ "*") wenzelm@23784: (Scan.one Symbol.is_regular)) >> (Pretty o str o implode))) berghofe@11520: (Symbol.explode s) of berghofe@11520: (p, []) => p berghofe@11520: | _ => error ("Malformed annotation: " ^ quote s)); berghofe@11520: wenzelm@15801: wenzelm@17057: structure P = OuterParse and K = OuterKeyword; berghofe@11520: wenzelm@27353: val _ = List.app OuterKeyword.keyword ["attach", "file", "contains"]; wenzelm@24867: wenzelm@28375: fun strip_whitespace s = implode (fst (take_suffix (fn c => c = "\n" orelse c = " ") wenzelm@28375: (snd (take_prefix (fn c => c = "\n" orelse c = " ") (explode s))))) ^ "\n"; berghofe@16769: berghofe@16769: val parse_attach = Scan.repeat (P.$$$ "attach" |-- berghofe@16769: Scan.optional (P.$$$ "(" |-- P.xname --| P.$$$ ")") "" -- berghofe@17144: (P.verbatim >> strip_whitespace)); berghofe@16769: wenzelm@24867: val _ = berghofe@11520: OuterSyntax.command "types_code" wenzelm@11546: "associate types with target language types" K.thy_decl berghofe@16769: (Scan.repeat1 (P.xname --| P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >> haftmann@22921: (fn xs => Toplevel.theory (fn thy => fold (assoc_type o haftmann@22921: (fn ((name, mfx), aux) => (name, (parse_mixfix wenzelm@24707: (Syntax.read_typ_global thy) mfx, aux)))) xs thy))); berghofe@11520: wenzelm@24867: val _ = berghofe@11520: OuterSyntax.command "consts_code" wenzelm@11546: "associate constants with target language code" K.thy_decl berghofe@11520: (Scan.repeat1 haftmann@22921: (P.term --| berghofe@16769: P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >> wenzelm@25376: (fn xs => Toplevel.theory (fn thy => fold (assoc_const o haftmann@22921: (fn ((const, mfx), aux) => wenzelm@27251: (const, (parse_mixfix (OldGoals.read_term thy) mfx, aux)))) xs thy))); berghofe@11520: berghofe@17144: fun parse_code lib = berghofe@17144: Scan.optional (P.$$$ "(" |-- P.enum "," P.xname --| P.$$$ ")") (!mode) -- berghofe@17144: (if lib then Scan.optional P.name "" else P.name) -- berghofe@17144: Scan.option (P.$$$ "file" |-- P.name) -- berghofe@17144: (if lib then Scan.succeed [] berghofe@17144: else Scan.optional (P.$$$ "imports" |-- Scan.repeat1 P.name) []) --| berghofe@17144: P.$$$ "contains" -- berghofe@17144: ( Scan.repeat1 (P.name --| P.$$$ "=" -- P.term) berghofe@17144: || Scan.repeat1 (P.term >> pair "")) >> berghofe@17144: (fn ((((mode', module), opt_fname), modules), xs) => Toplevel.theory (fn thy => wenzelm@28271: let wenzelm@28271: val mode'' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode'); wenzelm@28271: val (code, gr) = setmp mode mode'' (generate_code thy modules module) xs; wenzelm@28271: val thy' = thy |> Context.theory_map (ML_Context.exec (fn () => wenzelm@28271: (case opt_fname of wenzelm@28271: NONE => ML_Context.eval false Position.none (cat_lines (map snd code)) wenzelm@28271: | SOME fname => wenzelm@28271: if lib then app (fn (name, s) => File.write wenzelm@28271: (Path.append (Path.explode fname) (Path.basic (name ^ ".ML"))) s) wenzelm@28271: (("ROOT", implode (map (fn (name, _) => wenzelm@28271: "use \"" ^ name ^ ".ML\";\n") code)) :: code) wenzelm@28271: else File.write (Path.explode fname) (snd (hd code))))); wenzelm@28271: in wenzelm@28271: if lib then thy' wenzelm@28271: else map_modules (Symtab.update (module, gr)) thy' wenzelm@28271: end)); berghofe@17144: haftmann@28227: val setup = add_codegen "default" default_codegen haftmann@28227: #> add_tycodegen "default" default_tycodegen haftmann@28227: #> Value.add_evaluator ("SML", eval_term o ProofContext.theory_of) haftmann@28315: #> Quickcheck.add_generator ("SML", test_term) haftmann@28227: #> Code.add_attribute ("unfold", Scan.succeed (Thm.declaration_attribute haftmann@28227: (fn thm => Context.mapping (add_unfold thm #> Code.add_inline thm) I))); haftmann@28227: wenzelm@24867: val _ = berghofe@17144: OuterSyntax.command "code_library" berghofe@17144: "generates code for terms (one structure for each theory)" K.thy_decl berghofe@17144: (parse_code true); berghofe@17144: wenzelm@24867: val _ = berghofe@17144: OuterSyntax.command "code_module" berghofe@17144: "generates code for terms (single structure, incremental)" K.thy_decl berghofe@17144: (parse_code false); berghofe@11520: berghofe@11520: end;