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@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 wenzelm@18728: val add_attribute: string -> (Args.T list -> attribute * Args.T list) -> 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 berghofe@16769: val assoc_consts: (xstring * string option * (term mixfix list * berghofe@16769: (string * string) list)) list -> theory -> theory berghofe@16769: val assoc_consts_i: (xstring * typ option * (term mixfix list * berghofe@16769: (string * string) list)) list -> theory -> theory berghofe@16769: val assoc_types: (xstring * (typ mixfix list * berghofe@16769: (string * string) list)) list -> theory -> theory berghofe@16769: 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 -> berghofe@16649: codegr * term -> codegr * Pretty.T berghofe@16649: val invoke_tycodegen: theory -> deftab -> string -> string -> bool -> berghofe@16649: codegr * typ -> codegr * Pretty.T berghofe@14858: val mk_id: string -> string berghofe@17144: val mk_qual_id: string -> string * string -> string berghofe@17144: val mk_const_id: string -> string -> codegr -> codegr * (string * string) berghofe@17144: val get_const_id: string -> codegr -> string * string berghofe@17144: val mk_type_id: string -> string -> codegr -> codegr * (string * string) berghofe@17144: val get_type_id: string -> codegr -> string * string berghofe@16649: val thyname_of_type: string -> theory -> string berghofe@16649: val thyname_of_const: string -> theory -> 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 berghofe@11520: val is_instance: theory -> 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@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 berghofe@14105: val test_term: theory -> int -> int -> term -> (string * term) list option berghofe@17549: val eval_result: 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 haftmann@18702: val fillin_mixfix: ('a -> Pretty.T) -> 'a mixfix list -> 'a list -> Pretty.T 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 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@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: berghofe@17144: fun merge_nametabs ((tab, used), (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: codegr -> (* code dependency graph *) 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 *) berghofe@16649: (codegr * Pretty.T) 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@16458: default_type = SOME (typ_of (read_ctyp thy s))}; berghofe@14105: berghofe@14105: (* data kind 'Pure/codegen' *) wenzelm@16458: wenzelm@16458: structure CodegenData = TheoryDataFun wenzelm@16458: (struct berghofe@11520: val name = "Pure/codegen"; 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, wenzelm@18728: attrs: (string * (Args.T list -> attribute * Args.T 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 = berghofe@14105: {codegens = [], tycodegens = [], consts = [], types = [], attrs = [], 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, berghofe@14105: consts = consts1, types = types1, attrs = attrs1, berghofe@17144: preprocs = preprocs1, modules = modules1, test_params = test_params1}, berghofe@12555: {codegens = codegens2, tycodegens = tycodegens2, berghofe@14105: consts = consts2, types = types2, attrs = attrs2, 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@21098: attrs = AList.merge (op =) (K true) (attrs1, attrs2), 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}; berghofe@11520: wenzelm@16458: fun print _ ({codegens, tycodegens, ...} : T) = berghofe@12452: Pretty.writeln (Pretty.chunks berghofe@12452: [Pretty.strs ("term code generators:" :: map fst codegens), berghofe@12452: Pretty.strs ("type code generators:" :: map fst tycodegens)]); wenzelm@16458: end); berghofe@11520: wenzelm@18708: val _ = Context.add_setup CodegenData.init; berghofe@11520: val print_codegens = CodegenData.print; 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 = berghofe@17144: let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} = berghofe@14105: CodegenData.get thy; berghofe@14105: in CodegenData.put {codegens = codegens, tycodegens = tycodegens, berghofe@15261: consts = consts, types = types, attrs = attrs, 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 = berghofe@17144: let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} = berghofe@17144: CodegenData.get thy; berghofe@17144: in CodegenData.put {codegens = codegens, tycodegens = tycodegens, berghofe@17144: consts = consts, types = types, attrs = attrs, 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 = berghofe@17144: let val {codegens, tycodegens, consts, types, attrs, 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, berghofe@17144: attrs = attrs, 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 = berghofe@17144: let val {codegens, tycodegens, consts, types, attrs, 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, berghofe@17144: attrs = attrs, 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@12555: (**** code attribute ****) berghofe@12555: berghofe@12555: fun add_attribute name att thy = berghofe@17144: let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} = berghofe@14105: CodegenData.get thy haftmann@17521: in (case AList.lookup (op =) attrs name of skalberg@15531: NONE => CodegenData.put {tycodegens = tycodegens, berghofe@12555: codegens = codegens, consts = consts, types = types, berghofe@15261: attrs = if name = "" then attrs @ [(name, att)] else (name, att) :: attrs, berghofe@17144: preprocs = preprocs, modules = modules, berghofe@15261: test_params = test_params} thy skalberg@15531: | SOME _ => error ("Code attribute " ^ name ^ " already declared")) berghofe@12555: end; berghofe@12555: berghofe@14197: fun mk_parser (a, p) = (if a = "" then Scan.succeed "" else Args.$$$ a) |-- p; berghofe@14197: berghofe@12555: val code_attr = wenzelm@18728: Attrib.syntax (Scan.peek (fn context => foldr op || Scan.fail (map mk_parser wenzelm@18728: (#attrs (CodegenData.get (Context.theory_of context)))))); berghofe@12555: wenzelm@15801: val _ = Context.add_setup wenzelm@18728: (Attrib.add_attributes [("code", code_attr, "declare theorems for code generation")]); wenzelm@15801: berghofe@12555: berghofe@15261: (**** preprocessors ****) berghofe@15261: berghofe@15261: fun add_preprocessor p thy = berghofe@17144: let val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} = berghofe@15261: CodegenData.get thy berghofe@15261: in CodegenData.put {tycodegens = tycodegens, berghofe@15261: codegens = codegens, consts = consts, types = types, berghofe@15261: attrs = attrs, 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 wenzelm@18728: 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 berghofe@17666: if forall (fn name => exists_Const (equal name o fst) prop) names berghofe@17666: then rewrite_rule [eqn] (Thm.transfer thy th) berghofe@17666: else th berghofe@17666: end) haftmann@19341: in add_preprocessor prep end; berghofe@15261: wenzelm@15801: berghofe@15261: berghofe@11520: (**** associate constants with target language code ****) berghofe@11520: skalberg@15570: fun gen_assoc_consts prep_type xs thy = Library.foldl (fn (thy, (s, tyopt, syn)) => berghofe@11520: let berghofe@17144: val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} = berghofe@14105: CodegenData.get thy; wenzelm@16458: val cname = Sign.intern_const thy s; berghofe@11520: in wenzelm@16458: (case Sign.const_type thy cname of skalberg@15531: SOME T => berghofe@11520: let val T' = (case tyopt of skalberg@15531: NONE => T skalberg@15531: | SOME ty => wenzelm@16458: let val U = prep_type thy ty wenzelm@19419: in if Type.raw_instance (U, T) then U berghofe@11520: else error ("Illegal type constraint for constant " ^ cname) berghofe@11520: end) berghofe@18320: in berghofe@18320: if num_args_of (fst syn) > length (binder_types T') then berghofe@18320: error ("More arguments than in corresponding type of " ^ s) berghofe@18320: else (case AList.lookup (op =) consts (cname, T') of skalberg@15531: NONE => CodegenData.put {codegens = codegens, berghofe@12452: tycodegens = tycodegens, berghofe@12555: consts = ((cname, T'), syn) :: consts, berghofe@15261: types = types, attrs = attrs, preprocs = preprocs, berghofe@17144: modules = modules, test_params = test_params} thy skalberg@15531: | SOME _ => error ("Constant " ^ cname ^ " already associated with code")) berghofe@11520: end berghofe@11520: | _ => error ("Not a constant: " ^ s)) berghofe@11520: end) (thy, xs); berghofe@11520: berghofe@11520: val assoc_consts_i = gen_assoc_consts (K I); wenzelm@16458: val assoc_consts = gen_assoc_consts (typ_of oo read_ctyp); berghofe@11520: wenzelm@15801: berghofe@11520: (**** associate types with target language types ****) berghofe@11520: skalberg@15570: fun assoc_types xs thy = Library.foldl (fn (thy, (s, syn)) => berghofe@11520: let berghofe@17144: val {codegens, tycodegens, consts, types, attrs, preprocs, modules, test_params} = berghofe@14105: CodegenData.get thy; berghofe@16649: 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 berghofe@18320: 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, berghofe@18320: types = (tc, syn) :: types, attrs = attrs, 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) berghofe@11520: end) (thy, xs); 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: berghofe@14858: fun dest_sym s = (case split_last (snd (take_prefix (equal "\\") (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' berghofe@17144: in ((gr, (tab1', tab2)), (module, s'')) end; berghofe@13073: berghofe@17144: fun get_const_id cname (gr, (tab1, tab2)) = 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' berghofe@17144: in ((gr, (tab1, tab2')), (module, s'')) end; berghofe@16649: berghofe@17144: fun get_type_id tyname (gr, (tab1, tab2)) = 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: berghofe@17144: fun get_type_id' f tyname tab = apsnd f (get_type_id tyname tab); 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@18281: fun theory_of_type s thy = berghofe@16649: if Sign.declared_tyname thy s wenzelm@19473: then SOME (the_default thy (get_first (theory_of_type s) (Theory.parents_of thy))) berghofe@16649: else NONE; berghofe@16649: haftmann@18281: fun theory_of_const s thy = berghofe@16649: if Sign.declared_const thy s wenzelm@19473: then SOME (the_default thy (get_first (theory_of_const s) (Theory.parents_of thy))) berghofe@16649: else NONE; berghofe@16649: berghofe@16649: fun thyname_of_type s thy = (case theory_of_type s thy of berghofe@16649: NONE => error ("thyname_of_type: no such type: " ^ quote s) berghofe@16649: | SOME thy' => Context.theory_name thy'); berghofe@16649: berghofe@16649: fun thyname_of_const s thy = (case theory_of_const s thy of berghofe@16649: NONE => error ("thyname_of_const: no such constant: " ^ quote s) berghofe@16649: | SOME thy' => Context.theory_name thy'); berghofe@11520: berghofe@13731: fun rename_terms ts = berghofe@11520: let skalberg@15574: val names = 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: berghofe@13731: fun is_instance thy T1 T2 = wenzelm@19806: Sign.typ_instance thy (T1, Logic.legacy_varifyT T2); berghofe@13731: haftmann@21056: fun get_assoc_code thy s T = Option.map snd (find_first (fn ((s', T'), _) => berghofe@13731: s = s' andalso is_instance thy 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 berghofe@16649: val axmss = map (fn thy' => berghofe@16649: (Context.theory_name thy', snd (#axioms (Theory.rep_theory 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 berghofe@16649: | SOME _ => (case dest (prep_def (Thm.get_axiom 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 => berghofe@16649: let val i = find_index (is_instance thy 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: berghofe@17144: fun invoke_codegen thy defs dep module brack (gr, t) = (case get_first berghofe@17144: (fn (_, f) => f thy defs gr dep module brack t) (#codegens (CodegenData.get thy)) of berghofe@17144: NONE => codegen_error gr dep ("Unable to generate code for term:\n" ^ berghofe@17144: Sign.string_of_term thy t) skalberg@15531: | SOME x => x); berghofe@12452: berghofe@17144: fun invoke_tycodegen thy defs dep module brack (gr, T) = (case get_first berghofe@17144: (fn (_, f) => f thy defs gr dep module brack T) (#tycodegens (CodegenData.get thy)) of berghofe@17144: NONE => codegen_error gr dep ("Unable to generate code for type:\n" ^ berghofe@17144: Sign.string_of_typ thy T) skalberg@15531: | SOME x => x); berghofe@11520: berghofe@11520: berghofe@11520: (**** code generator for mixfix expressions ****) berghofe@11520: berghofe@11520: fun parens p = Pretty.block [Pretty.str "(", p, Pretty.str ")"]; berghofe@11520: berghofe@11520: fun pretty_fn [] p = [p] berghofe@11520: | pretty_fn (x::xs) p = Pretty.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@16769: then cons (Pretty.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: haftmann@18702: fun fillin_mixfix f ms args = haftmann@18098: let haftmann@18281: fun fillin [] [] = haftmann@18281: [] haftmann@18281: | fillin (Arg :: ms) (a :: args) = haftmann@18702: f a :: fillin ms args haftmann@18281: | fillin (Ignore :: ms) args = haftmann@18281: fillin ms args haftmann@18281: | fillin (Module :: ms) args = haftmann@18281: fillin ms args haftmann@18281: | fillin (Pretty p :: ms) args = haftmann@18281: p :: fillin ms args haftmann@18281: | fillin (Quote q :: ms) args = haftmann@18702: f q :: fillin ms args haftmann@18281: in Pretty.block (fillin ms args) end; haftmann@18098: berghofe@11520: berghofe@12452: (**** default code generators ****) berghofe@11520: berghofe@11520: fun eta_expand t ts i = berghofe@11520: let berghofe@11520: val (Ts, _) = strip_type (fastype_of t); berghofe@11520: val j = i - length ts berghofe@11520: in skalberg@15574: 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@11520: Pretty.block (Pretty.str "(" :: berghofe@11520: separate (Pretty.brk 1) (p :: ps) @ [Pretty.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: berghofe@17144: fun default_codegen thy defs gr dep module brack t = berghofe@11520: let berghofe@11520: val (u, ts) = strip_comb t; berghofe@17144: fun codegens brack = foldl_map (invoke_codegen thy defs dep module brack) berghofe@11520: in (case u of berghofe@14105: Var ((s, i), T) => berghofe@14105: let berghofe@14105: val (gr', ps) = codegens true (gr, ts); berghofe@17144: val (gr'', _) = invoke_tycodegen thy defs dep module false (gr', T) skalberg@15531: in SOME (gr'', mk_app brack (Pretty.str (s ^ berghofe@11520: (if i=0 then "" else string_of_int i))) ps) berghofe@11520: end berghofe@11520: berghofe@14105: | Free (s, T) => berghofe@14105: let berghofe@14105: val (gr', ps) = codegens true (gr, ts); berghofe@17144: val (gr'', _) = invoke_tycodegen thy defs dep module false (gr', T) skalberg@15531: in SOME (gr'', mk_app brack (Pretty.str s) ps) end berghofe@11520: berghofe@11520: | Const (s, T) => berghofe@11520: (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 berghofe@17144: default_codegen thy defs gr dep module brack (eta_expand u ts i) berghofe@11520: else berghofe@11520: let berghofe@12452: val (ts1, ts2) = args_of ms ts; berghofe@12452: val (gr1, ps1) = codegens false (gr, ts1); berghofe@12452: val (gr2, ps2) = codegens true (gr1, ts2); berghofe@12452: val (gr3, ps3) = codegens false (gr2, quotes_of ms); berghofe@17549: val (gr4, _) = invoke_tycodegen thy defs dep module false berghofe@17549: (gr3, funpow (length ts) (hd o tl o snd o dest_Type) T); berghofe@17144: val (module', suffix) = (case get_defn thy defs s T of berghofe@17144: NONE => (if_library (thyname_of_const s thy) 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 berghofe@17549: [] => (gr4, p module) berghofe@17144: | xs => (add_edge (node_id, dep) (new_node berghofe@17549: (node_id, (NONE, module', space_implode "\n" xs ^ "\n")) gr4), berghofe@17144: p module')) berghofe@17144: | SOME (_, module'', _) => berghofe@17549: (add_edge (node_id, dep) gr4, p module'')) 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; berghofe@17144: val (gr', (ps, def_id)) = codegens true (gr, ts) |>>> berghofe@17144: mk_const_id module' (s ^ suffix); berghofe@17144: val p = mk_app brack (Pretty.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; berghofe@17144: val (gr1, p') = invoke_codegen thy defs node_id module' false berghofe@17144: (add_edge (node_id, dep) berghofe@17144: (new_node (node_id, (NONE, "", "")) gr'), rhs'); berghofe@17144: val (gr2, xs) = codegens false (gr1, args'); berghofe@17144: val (gr3, _) = invoke_tycodegen thy defs dep module false (gr2, T); berghofe@17144: val (gr4, ty) = invoke_tycodegen thy defs node_id module' false (gr3, U); berghofe@17144: in (map_node node_id (K (NONE, module', Pretty.string_of berghofe@17144: (Pretty.block (separate (Pretty.brk 1) berghofe@17144: (if null args' then berghofe@17144: [Pretty.str ("val " ^ snd def_id ^ " :"), ty] berghofe@17144: else Pretty.str ("fun " ^ snd def_id) :: xs) @ berghofe@17144: [Pretty.str " =", Pretty.brk 1, p', Pretty.str ";"])) ^ "\n\n")) gr4, berghofe@17144: p) berghofe@17144: end berghofe@17144: | SOME _ => (add_edge (node_id, dep) gr', p)) 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; berghofe@12452: val (gr1, ps) = codegens true (gr, ts); berghofe@17144: val (gr2, p) = invoke_codegen thy defs dep module false berghofe@12452: (gr1, subst_bounds (map Free (rev (bs' ~~ Ts)), t)); berghofe@11520: in skalberg@15531: SOME (gr2, mk_app brack (Pretty.block (Pretty.str "(" :: pretty_fn bs' p @ berghofe@11520: [Pretty.str ")"])) ps) berghofe@11520: end berghofe@11520: skalberg@15531: | _ => NONE) berghofe@11520: end; berghofe@11520: berghofe@17144: fun default_tycodegen thy defs gr dep module brack (TVar ((s, i), _)) = skalberg@15531: SOME (gr, Pretty.str (s ^ (if i = 0 then "" else string_of_int i))) berghofe@17144: | default_tycodegen thy defs gr dep module brack (TFree (s, _)) = berghofe@16649: SOME (gr, Pretty.str s) berghofe@17144: | default_tycodegen thy defs gr dep module brack (Type (s, Ts)) = 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 berghofe@12452: val (gr', ps) = foldl_map berghofe@17144: (invoke_tycodegen thy defs dep module false) berghofe@16649: (gr, fst (args_of ms Ts)); berghofe@12452: val (gr'', qs) = foldl_map berghofe@17144: (invoke_tycodegen thy defs dep module false) berghofe@16769: (gr', quotes_of ms); berghofe@17144: val module' = if_library (thyname_of_type s thy) 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 berghofe@17144: [] => (gr'', p module') berghofe@17144: | xs => (fst (mk_type_id module' s berghofe@17144: (add_edge (node_id, dep) (new_node (node_id, berghofe@17144: (NONE, module', space_implode "\n" xs ^ "\n")) gr''))), berghofe@17144: p module')) berghofe@17144: | SOME (_, module'', _) => berghofe@17144: (add_edge (node_id, dep) gr'', p module'')) berghofe@16769: end); berghofe@12452: wenzelm@15801: val _ = Context.add_setup wenzelm@18708: (add_codegen "default" default_codegen #> wenzelm@18708: add_tycodegen "default" default_tycodegen); wenzelm@15801: berghofe@11520: berghofe@16649: fun mk_struct name s = "structure " ^ name ^ " =\nstruct\n\n" ^ s ^ "end;\n"; berghofe@16649: haftmann@17521: fun add_to_module name s = AList.map_entry (op =) name (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) haftmann@21056: (find_first (equal b o #2 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); berghofe@16649: val mod_gr = foldr (uncurry Graph.add_edge_acyclic) berghofe@16649: (foldr (uncurry (Graph.new_node o rpair ())) Graph.empty modules) wenzelm@19482: (maps (fn (s, (_, module, _)) => map (pair module) berghofe@17144: (filter_out (equal module) (map (#2 o Graph.get_node gr) wenzelm@19482: (Graph.imm_succs gr s)))) code); berghofe@16649: val modules' = berghofe@16649: rev (Graph.all_preds mod_gr (map (#2 o Graph.get_node gr) xs)) berghofe@16649: in berghofe@17144: 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@17144: fun gen_generate_code prep_term thy modules module = berghofe@14598: setmp print_mode [] (Pretty.setmp_margin (!margin) (fn xs => berghofe@11520: let wenzelm@21858: val _ = (module <> "" orelse wenzelm@20665: member (op =) (!mode) "library" andalso forall (equal "" o fst) 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, "")) berghofe@17144: (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)) berghofe@17144: handle Graph.DUPS ks => error ("Duplicate code for " ^ commas ks); 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); berghofe@11520: val (gr', ps) = foldl_map (fn (gr, (s, t)) => apsnd (pair s) berghofe@17144: (invoke_codegen thy defs "" module false (gr, t))) berghofe@17549: (gr, map (apsnd (expand o preprocess_term thy o prep_term thy)) xs); wenzelm@19482: val code = map_filter berghofe@17144: (fn ("", _) => NONE berghofe@17144: | (s', p) => SOME (Pretty.string_of (Pretty.block berghofe@17144: [Pretty.str ("val " ^ s' ^ " ="), Pretty.brk 1, p, Pretty.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@16649: end)); berghofe@11520: berghofe@11520: val generate_code_i = gen_generate_code (K I); berghofe@11520: val generate_code = gen_generate_code wenzelm@16458: (fn thy => term_of o read_cterm thy o rpair TypeInfer.logicT); berghofe@11520: berghofe@12452: berghofe@13753: (**** Reflection ****) berghofe@13753: berghofe@13753: val strip_tname = implode o tl o explode; berghofe@13753: berghofe@13753: fun pretty_list xs = Pretty.block (Pretty.str "[" :: wenzelm@19482: flat (separate [Pretty.str ",", Pretty.brk 1] (map single xs)) @ berghofe@13753: [Pretty.str "]"]); berghofe@13753: berghofe@13753: fun mk_type p (TVar ((s, i), _)) = Pretty.str berghofe@13753: (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "T") berghofe@13753: | mk_type p (TFree (s, _)) = Pretty.str (strip_tname s ^ "T") berghofe@13753: | mk_type p (Type (s, Ts)) = (if p then parens else I) (Pretty.block berghofe@13753: [Pretty.str "Type", Pretty.brk 1, Pretty.str ("(\"" ^ s ^ "\","), berghofe@13753: Pretty.brk 1, pretty_list (map (mk_type false) Ts), Pretty.str ")"]); berghofe@13753: berghofe@17144: fun mk_term_of gr module p (TVar ((s, i), _)) = Pretty.str berghofe@13753: (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "F") berghofe@17144: | mk_term_of gr module p (TFree (s, _)) = Pretty.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@17144: (Pretty.str (mk_qual_id module berghofe@17144: (get_type_id' (fn s' => "term_of_" ^ s') s gr)) :: 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@17144: fun mk_gen gr module p xs a (TVar ((s, i), _)) = Pretty.str berghofe@14105: (strip_tname s ^ (if i = 0 then "" else string_of_int i) ^ "G") berghofe@17144: | mk_gen gr module p xs a (TFree (s, _)) = Pretty.str (strip_tname s ^ "G") berghofe@17144: | mk_gen gr module p xs a (Type (s, Ts)) = (if p then parens else I) berghofe@16649: (Pretty.block (separate (Pretty.brk 1) berghofe@17144: (Pretty.str (mk_qual_id module (get_type_id' (fn s' => "gen_" ^ s') s gr) ^ wenzelm@20665: (if member (op =) xs s then "'" else "")) :: berghofe@17144: map (mk_gen gr module true xs a) Ts @ wenzelm@20665: (if member (op =) xs s then [Pretty.str a] else [])))); berghofe@14105: skalberg@15531: val test_fn : (int -> (string * term) list option) ref = ref (fn _ => NONE); berghofe@14105: berghofe@17638: fun test_term thy sz i t = berghofe@14105: let wenzelm@21858: val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse wenzelm@21858: error "Term to be tested contains type variables"; wenzelm@21858: val _ = null (term_vars t) orelse wenzelm@21858: error "Term to be tested contains schematic variables"; berghofe@14105: val frees = map dest_Free (term_frees t); berghofe@17549: val frees' = frees ~~ berghofe@17549: map (fn i => "arg" ^ string_of_int i) (1 upto length frees); berghofe@17144: val (code, gr) = setmp mode ["term_of", "test"] berghofe@17144: (generate_code_i thy [] "Generated") [("testf", list_abs_free (frees, t))]; berghofe@17638: val s = setmp print_mode [] (fn () => "structure TestTerm =\nstruct\n\n" ^ berghofe@17144: space_implode "\n" (map snd code) ^ berghofe@16649: "\nopen Generated;\n\n" ^ Pretty.string_of berghofe@14105: (Pretty.block [Pretty.str "val () = Codegen.test_fn :=", berghofe@17549: Pretty.brk 1, Pretty.str ("(fn i =>"), Pretty.brk 1, berghofe@14105: Pretty.blk (0, [Pretty.str "let", Pretty.brk 1, berghofe@17549: Pretty.blk (0, separate Pretty.fbrk (map (fn ((s, T), s') => berghofe@17549: Pretty.block [Pretty.str ("val " ^ s' ^ " ="), Pretty.brk 1, berghofe@17144: mk_gen gr "Generated" false [] "" T, Pretty.brk 1, berghofe@17549: Pretty.str "i;"]) frees')), berghofe@14105: Pretty.brk 1, Pretty.str "in", Pretty.brk 1, berghofe@14105: Pretty.block [Pretty.str "if ", berghofe@17549: mk_app false (Pretty.str "testf") (map (Pretty.str o snd) frees'), skalberg@15531: Pretty.brk 1, Pretty.str "then NONE", berghofe@14105: Pretty.brk 1, Pretty.str "else ", skalberg@15531: Pretty.block [Pretty.str "SOME ", Pretty.block (Pretty.str "[" :: wenzelm@19482: flat (separate [Pretty.str ",", Pretty.brk 1] berghofe@17549: (map (fn ((s, T), s') => [Pretty.block haftmann@21056: [Pretty.str ("(" ^ quote (Symbol.escape s) ^ ","), Pretty.brk 1, berghofe@17144: mk_app false (mk_term_of gr "Generated" false T) berghofe@17549: [Pretty.str s'], Pretty.str ")"]]) frees')) @ berghofe@14105: [Pretty.str "]"])]], wenzelm@14980: Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"]) ^ berghofe@17638: "\n\nend;\n") (); wenzelm@20926: val _ = use_text Output.ml_output false s; skalberg@15531: fun iter f k = if k > i then NONE berghofe@14135: else (case (f () handle Match => skalberg@15531: (warning "Exception Match raised in generated code"; NONE)) of skalberg@15531: NONE => iter f (k+1) | SOME x => SOME x); skalberg@15531: fun test k = if k > sz then NONE berghofe@14105: else (priority ("Test data size: " ^ string_of_int k); berghofe@14105: case iter (fn () => !test_fn k) 1 of skalberg@15531: NONE => test (k+1) | SOME x => SOME x); berghofe@17638: in test 0 end; berghofe@14105: berghofe@14105: fun test_goal ({size, iterations, default_type}, tvinsts) i st = berghofe@14105: let wenzelm@16458: val thy = Toplevel.theory_of st; berghofe@14105: fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t berghofe@14105: | strip t = t; berghofe@14105: val (gi, frees) = Logic.goal_params berghofe@14105: (prop_of (snd (snd (Proof.get_goal (Toplevel.proof_of st))))) i; wenzelm@20548: val gi' = ObjectLogic.atomize_term thy (map_types wenzelm@19502: (map_type_tfree (fn p as (s, _) => wenzelm@19502: the_default (the_default (TFree p) default_type) wenzelm@19502: (AList.lookup (op =) tvinsts s))) (subst_bounds (frees, strip gi))); berghofe@14105: in case test_term (Toplevel.theory_of st) size iterations gi' of skalberg@15531: NONE => writeln "No counterexamples found." skalberg@15531: | SOME cex => writeln ("Counterexample found:\n" ^ berghofe@14105: Pretty.string_of (Pretty.chunks (map (fn (s, t) => berghofe@14105: Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, wenzelm@16458: Sign.pretty_term thy t]) cex))) berghofe@14105: end; berghofe@14105: berghofe@14105: berghofe@17549: (**** Evaluator for terms ****) berghofe@17549: berghofe@17549: val eval_result = ref (Bound 0); berghofe@17549: berghofe@17549: fun eval_term thy = setmp print_mode [] (fn t => berghofe@17549: let wenzelm@21858: val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse wenzelm@21858: error "Term to be evaluated contains type variables"; wenzelm@21858: val _ = (null (term_vars t) andalso null (term_frees t)) orelse wenzelm@21858: error "Term to be evaluated contains variables"; berghofe@17549: val (code, gr) = setmp mode ["term_of"] berghofe@17549: (generate_code_i thy [] "Generated") [("result", t)]; berghofe@17549: val s = "structure EvalTerm =\nstruct\n\n" ^ berghofe@17549: space_implode "\n" (map snd code) ^ berghofe@17549: "\nopen Generated;\n\n" ^ Pretty.string_of berghofe@17549: (Pretty.block [Pretty.str "val () = Codegen.eval_result :=", berghofe@17549: Pretty.brk 1, berghofe@17549: mk_app false (mk_term_of gr "Generated" false (fastype_of t)) berghofe@17549: [Pretty.str "result"], berghofe@17549: Pretty.str ";"]) ^ berghofe@17549: "\n\nend;\n"; wenzelm@20926: val _ = use_text Output.ml_output false s berghofe@17549: in !eval_result end); berghofe@17549: berghofe@17549: fun print_evaluated_term s = Toplevel.keep (fn state => berghofe@17549: let wenzelm@21506: val ctxt = Toplevel.context_of state; wenzelm@21002: val thy = ProofContext.theory_of ctxt; wenzelm@21002: val t = eval_term thy (ProofContext.read_term ctxt s); berghofe@17549: val T = Term.type_of t; berghofe@17549: in berghofe@17549: writeln (Pretty.string_of berghofe@17549: (Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t), Pretty.fbrk, berghofe@17549: Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt T)])) berghofe@17549: end); berghofe@17549: haftmann@20599: exception Evaluation of term; haftmann@20599: haftmann@20599: fun evaluation_oracle (thy, Evaluation t) = haftmann@20599: Logic.mk_equals (t, eval_term thy t); haftmann@20599: haftmann@20599: fun evaluation_conv ct = haftmann@20599: let val {sign, t, ...} = rep_cterm ct wenzelm@20665: in Thm.invoke_oracle_i sign "Pure.evaluation" (sign, Evaluation t) end; haftmann@20599: haftmann@20599: val _ = Context.add_setup wenzelm@20665: (Theory.add_oracle ("evaluation", evaluation_oracle)); berghofe@17549: berghofe@12452: (**** Interface ****) berghofe@12452: berghofe@13731: val str = setmp print_mode [] Pretty.str; berghofe@13731: 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 berghofe@11520: ( $$ "'" |-- Scan.one Symbol.not_eof berghofe@11520: || Scan.unless ($$ "*" -- $$ "}") (Scan.one Symbol.not_eof)) --| berghofe@12452: $$ "*" --| $$ "}" >> (Quote o rd o implode) berghofe@11520: || Scan.repeat1 berghofe@11520: ( $$ "'" |-- Scan.one Symbol.not_eof berghofe@16769: || Scan.unless ($$ "_" || $$ "?" || $$ "\\" || $$ "/" || $$ "{" |-- $$ "*") berghofe@13731: (Scan.one Symbol.not_eof)) >> (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: val _ = Context.add_setup wenzelm@18708: (assoc_types [("fun", (parse_mixfix (K dummyT) "(_ ->/ _)", berghofe@16769: [("term_of", berghofe@16769: "fun term_of_fun_type _ T _ U _ = Free (\"\", T --> U);\n"), berghofe@16769: ("test", berghofe@16769: "fun gen_fun_type _ G i =\n\ berghofe@16769: \ let\n\ wenzelm@18679: \ val f = ref (fn x => raise Match);\n\ berghofe@16769: \ val _ = (f := (fn x =>\n\ berghofe@16769: \ let\n\ berghofe@16769: \ val y = G i;\n\ berghofe@16769: \ val f' = !f\n\ berghofe@16769: \ in (f := (fn x' => if x = x' then y else f' x'); y) end))\n\ wenzelm@18708: \ in (fn x => !f x) end;\n")]))]); wenzelm@15801: wenzelm@15801: wenzelm@17057: structure P = OuterParse and K = OuterKeyword; berghofe@11520: berghofe@17144: fun strip_whitespace s = implode (fst (take_suffix (equal "\n" orf equal " ") berghofe@17144: (snd (take_prefix (equal "\n" orf equal " ") (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: berghofe@11520: val assoc_typeP = 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) >> berghofe@12452: (fn xs => Toplevel.theory (fn thy => assoc_types berghofe@16769: (map (fn ((name, mfx), aux) => (name, (parse_mixfix berghofe@16769: (typ_of o read_ctyp thy) mfx, aux))) xs) thy))); berghofe@11520: berghofe@11520: val assoc_constP = berghofe@11520: OuterSyntax.command "consts_code" wenzelm@11546: "associate constants with target language code" K.thy_decl berghofe@11520: (Scan.repeat1 wenzelm@13003: (P.xname -- (Scan.option (P.$$$ "::" |-- P.typ)) --| berghofe@16769: P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >> berghofe@11520: (fn xs => Toplevel.theory (fn thy => assoc_consts berghofe@16769: (map (fn (((name, optype), mfx), aux) => (name, optype, (parse_mixfix berghofe@16769: (term_of o read_cterm thy o rpair TypeInfer.logicT) mfx, aux))) berghofe@11520: 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 => berghofe@17144: let wenzelm@19299: val mode'' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode'); berghofe@17144: val (code, gr) = setmp mode mode'' (generate_code thy modules module) xs berghofe@17144: in ((case opt_fname of wenzelm@20926: NONE => use_text Output.ml_output false berghofe@17144: (space_implode "\n" (map snd code)) berghofe@17144: | SOME fname => berghofe@17144: if lib then berghofe@17144: app (fn (name, s) => File.write wenzelm@21858: (Path.append (Path.explode fname) (Path.basic (name ^ ".ML"))) s) berghofe@17144: (("ROOT", implode (map (fn (name, _) => berghofe@17144: "use \"" ^ name ^ ".ML\";\n") code)) :: code) wenzelm@21858: else File.write (Path.explode fname) (snd (hd code))); berghofe@17144: if lib then thy wenzelm@17412: else map_modules (Symtab.update (module, gr)) thy) berghofe@17144: end)); berghofe@17144: berghofe@17144: val code_libraryP = 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: berghofe@17144: val code_moduleP = 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@14105: val params = berghofe@14105: [("size", P.nat >> (K o set_size)), berghofe@14105: ("iterations", P.nat >> (K o set_iterations)), berghofe@14105: ("default_type", P.typ >> set_default_type)]; berghofe@14105: berghofe@14105: val parse_test_params = P.short_ident :-- (fn s => haftmann@17521: P.$$$ "=" |-- (AList.lookup (op =) params s |> the_default Scan.fail)) >> snd; berghofe@14105: berghofe@14105: fun parse_tyinst xs = wenzelm@16458: (P.type_ident --| P.$$$ "=" -- P.typ >> (fn (v, s) => fn thy => wenzelm@16458: fn (x, ys) => (x, (v, typ_of (read_ctyp thy s)) :: ys))) xs; berghofe@14105: berghofe@14105: fun app [] x = x berghofe@14105: | app (f :: fs) x = app fs (f x); berghofe@14105: berghofe@14105: val test_paramsP = berghofe@14105: OuterSyntax.command "quickcheck_params" "set parameters for random testing" K.thy_decl berghofe@14105: (P.$$$ "[" |-- P.list1 parse_test_params --| P.$$$ "]" >> berghofe@14105: (fn fs => Toplevel.theory (fn thy => berghofe@16649: map_test_params (app (map (fn f => f thy) fs)) thy))); berghofe@14105: berghofe@14105: val testP = berghofe@14105: OuterSyntax.command "quickcheck" "try to find counterexample for subgoal" K.diag berghofe@14105: (Scan.option (P.$$$ "[" |-- P.list1 wenzelm@16458: ( parse_test_params >> (fn f => fn thy => apfst (f thy)) berghofe@14105: || parse_tyinst) --| P.$$$ "]") -- Scan.optional P.nat 1 >> berghofe@14105: (fn (ps, g) => Toplevel.keep (fn st => wenzelm@19502: test_goal (app (the_default [] (Option.map (map (fn f => f (Toplevel.theory_of st))) ps)) berghofe@14105: (get_test_params (Toplevel.theory_of st), [])) g st))); berghofe@14105: berghofe@17549: val valueP = berghofe@17549: OuterSyntax.improper_command "value" "read, evaluate and print term" K.diag berghofe@17549: (P.term >> (Toplevel.no_timing oo print_evaluated_term)); berghofe@17549: berghofe@17144: val _ = OuterSyntax.add_keywords ["attach", "file", "contains"]; berghofe@16769: wenzelm@15801: val _ = OuterSyntax.add_parsers berghofe@17549: [assoc_typeP, assoc_constP, code_libraryP, code_moduleP, test_paramsP, testP, valueP]; berghofe@11520: berghofe@11520: end;