# HG changeset patch # User haftmann # Date 1155017970 -7200 # Node ID d73e49780ef25a75a8243048a18ee27708ac598a # Parent bb56a6cbacacbce0c23430e6e6841e687d88aae9 code generator refinements diff -r bb56a6cbacac -r d73e49780ef2 src/Pure/Tools/ROOT.ML --- a/src/Pure/Tools/ROOT.ML Tue Aug 08 08:19:18 2006 +0200 +++ b/src/Pure/Tools/ROOT.ML Tue Aug 08 08:19:30 2006 +0200 @@ -12,6 +12,7 @@ use "../codegen.ML"; (*code generator, 2nd generation*) +use "codegen_names.ML"; use "codegen_theorems.ML"; use "codegen_thingol.ML"; use "codegen_serializer.ML"; diff -r bb56a6cbacac -r d73e49780ef2 src/Pure/Tools/class_package.ML --- a/src/Pure/Tools/class_package.ML Tue Aug 08 08:19:18 2006 +0200 +++ b/src/Pure/Tools/class_package.ML Tue Aug 08 08:19:30 2006 +0200 @@ -61,15 +61,18 @@ fun instantiations_of thy (ty, ty') = let +(* val _ = writeln "A"; *) val vartab = typ_tvars ty; +(* val _ = writeln "B"; *) fun prep_vartab (v, (_, ty)) = case (the o AList.lookup (op =) vartab) v of [] => NONE | sort => SOME ((v, sort), ty); +(* val _ = writeln "C"; *) in case try (Sign.typ_match thy (ty, ty')) Vartab.empty - of NONE => NONE + of NONE => ((*writeln "D";*)NONE) | SOME vartab => - SOME ((map_filter prep_vartab o Vartab.dest) vartab) + ((*writeln "E";*)SOME ((map_filter prep_vartab o Vartab.dest) vartab)) end; @@ -640,16 +643,25 @@ fun sortlookups_const thy (c, typ_ctxt) = let +(* val _ = writeln c *) val typ_decl = case AxClass.class_of_param thy c of NONE => Sign.the_const_type thy c | SOME class => case the_consts_sign thy class of (v, cs) => (Logic.legacy_varifyT o subst_clsvar v (TFree (v, [class]))) ((the o AList.lookup (op =) cs) c) +(* val _ = writeln "DECL" *) +(* val _ = (writeln o Display.raw_string_of_typ) typ_decl; *) +(* val _ = writeln "CTXT" *) +(* val _ = (writeln o Display.raw_string_of_typ) typ_ctxt; *) +(* val _ = writeln "(0)" *) in instantiations_of thy (typ_decl, typ_ctxt) |> the +(* |> tap (fn _ => writeln "(1)") *) |> map (fn ((_, sort), ty) => sortlookup thy (sort, ty)) +(* |> tap (fn _ => writeln "(2)") *) |> filter_out null +(* |> tap (fn _ => writeln "(3)") *) end; diff -r bb56a6cbacac -r d73e49780ef2 src/Pure/Tools/codegen_names.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Tools/codegen_names.ML Tue Aug 08 08:19:30 2006 +0200 @@ -0,0 +1,387 @@ +(* Title: Pure/Tools/codegen_names.ML + ID: $Id$ + Author: Florian Haftmann, TU Muenchen + +Name policies for code generation: dissolving ad-hoc overloaded +constants, prefixing any name by corresponding theory name, +conversion to alphanumeric representation. +Mappings are incrementally cached. +*) + +signature CODEGEN_NAMES = +sig + type tyco = string; + type const = string; + val class: theory -> class -> class + val class_rev: theory -> class -> class + val tyco: theory -> tyco -> tyco + val tyco_rev: theory -> tyco -> tyco + val instance: theory -> class * tyco -> string + val instance_rev: theory -> string -> class * tyco + val const: theory -> string * typ -> const + val const_rev: theory -> const -> string * typ + val force: (string * typ) * const -> theory -> theory + val read_const_typ: theory -> string -> string * typ + val read_const: theory -> string -> const + val purify_var: string -> string +end; + +structure CodegenNames: CODEGEN_NAMES = +struct + + +(* theory data *) + +type tyco = string; +type const = string; +val inst_ord = prod_ord fast_string_ord fast_string_ord; +val eq_inst = is_equal o inst_ord; +val const_ord = prod_ord fast_string_ord (list_ord Term.typ_ord); +val eq_const = is_equal o const_ord; + +structure Insttab = + TableFun( + type key = class * tyco; + val ord = inst_ord; + ); + +structure Consttab = + TableFun( + type key = string * typ list; + val ord = const_ord; + ); + +datatype names = Names of { + class: class Symtab.table * class Symtab.table, + tyco: tyco Symtab.table * tyco Symtab.table, + instance: string Insttab.table * (class * tyco) Symtab.table, + const: const Consttab.table * (string * typ list) Symtab.table +} + +val empty_names = Names { + class = (Symtab.empty, Symtab.empty), + tyco = (Symtab.empty, Symtab.empty), + instance = (Insttab.empty, Symtab.empty), + const = (Consttab.empty, Symtab.empty) +}; + +local + fun mk_names (class, tyco, instance, const) = + Names { class = class, tyco = tyco, instance = instance, const = const}; + fun map_names f (Names { class, tyco, instance, const }) = + mk_names (f (class, tyco, instance, const)); + val eq_string = op = : string * string -> bool; +in + fun merge_names (Names { class = (class1, classrev1), tyco = (tyco1, tycorev1), + instance = (instance1, instancerev1), const = (const1, constrev1) }, + Names { class = (class2, classrev2), tyco = (tyco2, tycorev2), + instance = (instance2, instancerev2), const = (const2, constrev2) }) = + mk_names ((Symtab.merge eq_string (class1, class2), Symtab.merge eq_string (classrev1, classrev2)), + (Symtab.merge eq_string (tyco1, tyco2), Symtab.merge eq_string (tycorev1, tycorev2)), + (Insttab.merge eq_string (instance1, instance2), Symtab.merge eq_inst (instancerev1, instancerev2)), + (Consttab.merge eq_string (const1, const2), Symtab.merge eq_const (constrev1, constrev2))); + fun map_class f = map_names + (fn (class, tyco, inst, const) => (f class, tyco, inst, const)); + fun map_tyco f = map_names + (fn (class, tyco, inst, const) => (class, f tyco, inst, const)); + fun map_inst f = map_names + (fn (class, tyco, inst, const) => (class, tyco, f inst, const)); + fun map_const f = map_names + (fn (class, tyco, inst, const) => (class, tyco, inst, f const)); + +end; (*local*) + +structure CodegenNamesData = TheoryDataFun +(struct + val name = "Pure/codegen_names"; + type T = names ref; + val empty = ref empty_names; + fun copy (ref names) = ref names; + val extend = copy; + fun merge _ (ref names1, ref names2) = ref (merge_names (names1, names2)); + fun print _ _ = (); +end); + +val _ = Context.add_setup CodegenNamesData.init; + + +(* forward lookup with cache update *) + +fun get thy get_tabs get upd_names upd policy x = + let + val names_ref = CodegenNamesData.get thy + val (Names names) = ! names_ref; + fun mk_unique used name = + let + fun mk_name 0 = name + | mk_name i = name ^ "_" ^ string_of_int i + fun find_name i = + let + val name = mk_name i + in + if used name + then find_name (i+1) + else name + end; + val name = find_name 0; + in name end; + val tabs = get_tabs names; + fun declare name = + let + val names' = upd_names (K (upd (x, name) (fst tabs), + Symtab.update_new (name, x) (snd tabs))) (Names names) + in (names_ref := names'; name) end; + in case get (fst tabs) x + of SOME name => name + | NONE => let + val used = Symtab.defined (snd tabs); + val raw_name = policy thy x; + val name = mk_unique used raw_name; + in declare name end + end; + + +(* backward lookup *) + +fun rev thy get_tabs errname name = + let + val names_ref = CodegenNamesData.get thy + val (Names names) = ! names_ref; + val tab = (snd o get_tabs) names; + in case Symtab.lookup tab name + of SOME x => x + | NONE => error ("no such " ^ errname ^ ": " ^ quote name) + end; + + +(* theory name lookup *) + +fun thyname_of thy f errmsg x = + let + fun thy_of thy = + if f thy x then case get_first thy_of (Theory.parents_of thy) + of NONE => SOME thy + | thy => thy + else NONE; + in case thy_of thy + of SOME thy => Context.theory_name thy + | NONE => error (errmsg x) end; + +fun thyname_of_class thy = + thyname_of thy (fn thy => member (op =) (Sign.classes thy)) + (fn class => "thyname_of_class: no such class: " ^ quote class); + +fun thyname_of_tyco thy = + thyname_of thy Sign.declared_tyname + (fn tyco => "thyname_of_tyco: no such type constructor: " ^ quote tyco); + +fun thyname_of_instance thy = + let + fun test_instance thy (class, tyco) = + can (Sorts.mg_domain (Sign.classes_of thy) tyco) [class] + in thyname_of thy test_instance + (fn (class, tyco) => "thyname_of_instance: no such instance: " ^ quote class ^ ", " ^ quote tyco) + end; + +fun thyname_of_const thy = + thyname_of thy Sign.declared_const + (fn c => "thyname_of_const: no such constant: " ^ quote c); + + +(* dissolving of ad-hoc overloading *) + +fun typinst_of_typ thy (c, ty) = + let + fun disciplined _ [(Type (tyco, _))] = + [Type (tyco, map (fn v => TFree (v, Sign.defaultS thy)) (*for monotonicity*) + (Name.invents Name.context "'a" (Sign.arity_number thy tyco)))] + | disciplined sort _ = + [TFree ("'a", sort)]; + fun ad_hoc c tys = + let + val def_tyinsts = + map (#lhs o snd) (Defs.specifications_of (Theory.defs_of thy) c); + val tyinst = find_first + (fn tys' => forall (Sign.typ_instance thy) (tys' ~~ tys)) def_tyinsts; + in case tyinst + of SOME tys => tys + | NONE => Consts.typargs (Sign.consts_of thy) + (c, (Logic.unvarifyT o Sign.the_const_type thy) c) + end; + val tyinsts = Consts.typargs (Sign.consts_of thy) (c, ty); + in if c = "op =" then (c, disciplined (Sign.defaultS thy) tyinsts) + else case AxClass.class_of_param thy c + of SOME class => (c, disciplined [class] tyinsts) + | _ => (c, ad_hoc c tyinsts) + end; + +fun get_overl_def_module thy ("op =", [Type (tyco, _)]) = + SOME (thyname_of_tyco thy tyco) + | get_overl_def_module thy (c, tys) = + get_first (fn (_, { lhs, module, ...}) => + if forall (Sign.typ_instance thy) (lhs ~~ tys) then SOME module else NONE) + (Defs.specifications_of (Theory.defs_of thy) c); + +fun typ_of_typinst thy (c, tys) = + (c, Consts.instance (Sign.consts_of thy) (c, tys)); + + +(* purification of identifiers *) + +val purify_name = + let + fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse s = "'"; + val is_junk = not o is_valid andf Symbol.not_eof; + val junk = Scan.any is_junk; + val scan_valids = Symbol.scanner "Malformed input" + ((junk |-- + (Scan.optional (Scan.one Symbol.is_ascii_letter) "x" ^^ (Scan.any is_valid >> implode) + --| junk)) + -- Scan.repeat ((Scan.any1 is_valid >> implode) --| junk) >> op ::); + in explode #> scan_valids #> space_implode "_" end; + +fun purify_op "0" = "zero" + | purify_op "1" = "one" + | purify_op s = + let + fun rep_op "+" = SOME "sum" + | rep_op "-" = SOME "diff" + | rep_op "*" = SOME "prod" + | rep_op "/" = SOME "quotient" + | rep_op "&" = SOME "conj" + | rep_op "|" = SOME "disj" + | rep_op "=" = SOME "eq" + | rep_op "~" = SOME "inv" + | rep_op "@" = SOME "append" + | rep_op s = NONE; + val scan_valids = Symbol.scanner "Malformed input" + (Scan.repeat (Scan.some rep_op || Scan.one (K true))); + in (explode #> scan_valids #> implode) s end; + +val purify_lower = explode #> nth_map 0 Symbol.to_ascii_lower #> implode; +val purify_upper = explode #> nth_map 0 Symbol.to_ascii_upper #> implode; + +fun purify_var v = + if nth (explode v) 0 = "'" + then "'" ^ (purify_name #> purify_lower #> unprefix "'") v + else (purify_name #> purify_lower) v; + +val purify_idf = purify_op #> purify_name; +val purify_prefix = map (purify_idf #> purify_upper); +val purify_base = purify_idf #> purify_lower; + + +(* explicit given constant names with cache update *) + +fun force (c_ty, name) thy = + let + val names = NameSpace.unpack name; + val (prefix, base) = split_last (NameSpace.unpack name); + val prefix' = purify_prefix prefix; + val base' = purify_base base; + val _ = if (base' = base) andalso forall (op =) (prefix' ~~ prefix) + then () + else + error ("name violates naming conventions: " ^ quote name + ^ "; perhaps try with " ^ quote (NameSpace.pack (prefix' @ [base']))) + val names_ref = CodegenNamesData.get thy; + val (Names names) = ! names_ref; + val (const, constrev) = #const names; + val c_tys as (c, _) = typinst_of_typ thy c_ty; + val _ = if Consttab.defined const c_tys + then error ("constant already named: " ^ + quote (c ^ "::" ^ (Sign.string_of_typ thy o snd o typ_of_typinst thy) c_tys)) + else (); + val _ = if Symtab.defined constrev name + then error ("name already given to constant: " ^ quote name) + else (); + val _ = names_ref := map_const (K (Consttab.update_new (c_tys, name) const, + Symtab.update_new (name, c_tys) constrev)) (Names names); + in + thy + end; + + +(* naming policies *) + +fun policy thy get_basename get_thyname name = + let + val prefix = (purify_prefix o NameSpace.unpack o get_thyname thy) name; + val base = (purify_base o get_basename) name; + in NameSpace.pack (prefix @ [base]) end; + +fun class_policy thy = policy thy NameSpace.base thyname_of_class; +fun tyco_policy thy = policy thy NameSpace.base thyname_of_tyco; +fun instance_policy thy = policy thy (fn (class, tyco) => + NameSpace.base class ^ "_" ^ NameSpace.base tyco) thyname_of_instance; + +fun const_policy thy (c, tys) = + case get_overl_def_module thy (c, tys) + of NONE => policy thy NameSpace.base thyname_of_const c + | SOME thyname => let + val prefix = (purify_prefix o NameSpace.unpack) thyname; + val base = (purify_base o NameSpace.base) c; + val tycos = map_filter (fn Type (tyco, _) => SOME tyco | _ => NONE) tys; + val base' = space_implode "_" (base :: tycos); + in NameSpace.pack (prefix @ [base']) end; + + +(* external interfaces *) + +fun class thy = + get thy #class Symtab.lookup map_class Symtab.update class_policy; +fun tyco thy = + get thy #tyco Symtab.lookup map_tyco Symtab.update tyco_policy; +fun instance thy = + get thy #instance Insttab.lookup map_inst Insttab.update instance_policy; +fun const thy = + get thy #const Consttab.lookup map_const Consttab.update const_policy + o typinst_of_typ thy; + +fun class_rev thy = rev thy #class "class"; +fun tyco_rev thy = rev thy #tyco "type constructor"; +fun instance_rev thy = rev thy #instance "instance"; +fun const_rev thy = rev thy #const "constant" #> typ_of_typinst thy; + + +(* reading constants as terms *) + +fun read_const_typ thy raw_t = + let + val t = Sign.read_term thy raw_t + in case try dest_Const t + of SOME c_ty => c_ty + | NONE => error ("not a constant: " ^ Sign.string_of_term thy t) + end; + +fun read_const thy = + const thy o read_const_typ thy; + + +(* outer syntax *) + +local + +structure P = OuterParse +and K = OuterKeyword + +fun force_e (raw_c, name) thy = + force (read_const_typ thy raw_c, name) thy; + +val constnameK = "code_constname"; + +val constnameP = + OuterSyntax.command constnameK "declare code name for constant" K.thy_decl ( + P.term -- P.name + >> (fn (raw_c, name) => + Toplevel.theory (force_e (raw_c, name))) + ); + +in + +val _ = OuterSyntax.add_parsers [constnameP]; + + +end; (*local*) + +end; diff -r bb56a6cbacac -r d73e49780ef2 src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Tue Aug 08 08:19:18 2006 +0200 +++ b/src/Pure/Tools/codegen_package.ML Tue Aug 08 08:19:30 2006 +0200 @@ -29,7 +29,7 @@ val add_appconst: xstring * appgen -> theory -> theory; val add_appconst_i: string * appgen -> theory -> theory; val appgen_default: appgen; - val appgen_number_of: (theory -> term -> IntInf.int) -> appgen; + val appgen_rep_bin: (theory -> term -> IntInf.int) -> appgen; val appgen_char: (term -> int option) -> appgen; val appgen_case: (theory -> term -> ((string * typ) list * ((term * typ) * (term * term) list)) option) @@ -46,7 +46,7 @@ structure DatatypeconsNameMangler: NAME_MANGLER; structure CodegenData: THEORY_DATA; type auxtab; - val mk_tabs: theory -> string list option -> auxtab; + val mk_tabs: theory -> string list option -> (string * typ) list -> auxtab; val alias_get: theory -> string -> string; val idf_of_name: theory -> string -> string -> string; val idf_of_const: theory -> auxtab -> string * typ -> string; @@ -143,8 +143,6 @@ (* code generator basics *) -type deftab = (typ * thm) list Symtab.table; - fun is_overloaded thy c = case Theory.definitions_of thy c of [] => true (* FIXME false (!?) *) | [{lhs = ty, ...}] => not (Sign.typ_equiv thy (ty, Sign.the_const_type thy c)) @@ -231,7 +229,7 @@ fun re_mangle _ dst = error ("no such datatype constructor: " ^ quote dst); ); -type auxtab = (bool * string list option * deftab) +type auxtab = (bool * string list option * CodegenTheorems.thmtab) * ((InstNameMangler.T * string Symtab.table Symtab.table) * (typ list Symtab.table * ConstNameMangler.T) * DatatypeconsNameMangler.T); type eqextr = theory -> auxtab @@ -392,9 +390,9 @@ val _ = alias_ref := (perhaps o Symtab.lookup o fst o #alias o #logic_data o CodegenData.get, perhaps o Symtab.lookup o snd o #alias o #logic_data o CodegenData.get); -fun idf_of_co thy (tabs as (_, (_, _, dtcontab))) (co, dtco) = - case CodegenTheorems.get_datatypes thy dtco - of SOME ((_, cos), _) => if AList.defined (op =) cos co +fun idf_of_co thy (tabs as ((_, _, thmtab), (_, _, dtcontab))) (co, dtco) = + case CodegenTheorems.get_dtyp_spec thmtab dtco + of SOME (_, cos) => if AList.defined (op =) cos co then try (DatatypeconsNameMangler.get thy dtcontab) (co, dtco) |> the_default co |> idf_of_name thy nsp_dtcon @@ -496,7 +494,7 @@ of NONE => [] | SOME (f, _) => f thy; -fun const_of_idf thy (tabs as (_, (_, _, dtcontab))) idf = +fun const_of_idf thy (tabs as ((_, _, thmtab), (_, _, dtcontab))) idf = case recconst_of_idf thy tabs idf of SOME c_ty => SOME c_ty | NONE => case dest_nsp nsp_mem idf @@ -522,7 +520,7 @@ | check_strict thy f x ((true, _, _), _) = true; -fun no_strict ((_, targets, deftab), tabs') = ((false, targets, deftab), tabs'); +fun no_strict ((_, targets, thmtab), tabs') = ((false, targets, thmtab), tabs'); fun ensure_def_class thy tabs cls trns = let @@ -552,15 +550,15 @@ |> ensure_def (defgen_class thy tabs) true ("generating class " ^ quote cls) cls' |> pair cls' end -and ensure_def_tyco thy tabs tyco trns = +and ensure_def_tyco thy (tabs as ((_, _, thmtab), _)) tyco trns = let val tyco' = idf_of_name thy nsp_tyco tyco; val strict = check_strict thy #syntax_tyco tyco' tabs; fun defgen_datatype thy (tabs as (_, (_, _, dtcontab))) dtco trns = case name_of_idf thy nsp_tyco dtco of SOME dtco => - (case CodegenTheorems.get_datatypes thy dtco - of SOME ((vars, cos), _) => + (case CodegenTheorems.get_dtyp_spec thmtab dtco + of SOME (vars, cos) => trns |> debug_msg (fn _ => "trying defgen datatype for " ^ quote dtco) |> fold_map (exprgen_tyvar_sort thy tabs) vars @@ -611,8 +609,8 @@ trns |> fold_map (ensure_def_class thy tabs) clss |-> (fn clss => pair (Lookup (clss, (v |> unprefix "'", if j = 1 then ~1 else i)))) -and mk_fun thy tabs (c, ty) trns = - case CodegenTheorems.get_funs thy (c, Logic.legacy_varifyT ty) (* FIXME *) +and mk_fun thy (tabs as ((_, _, thmtab), _)) (c, ty) trns = + case CodegenTheorems.get_fun_thms thmtab (c, Logic.legacy_varifyT ty) (*FIXME*) of eq_thms as eq_thm :: _ => let val msg = cat_lines ("generating code for theorems " :: map string_of_thm eq_thms); @@ -706,7 +704,7 @@ |> mk_fun thy tabs (c, ty) |-> (fn SOME (funn, _) => succeed (Fun funn) | NONE => fail ("no defining equations found for " ^ - (quote o Display.raw_string_of_term o Const) (c, ty))) + (quote (c ^ " :: " ^ Sign.string_of_typ thy ty)))) | NONE => trns |> fail ("not a constant: " ^ quote c); @@ -742,7 +740,7 @@ val strict = check_strict thy #syntax_const idf tabs; in trns - |> debug_msg (fn _ => "generating constant " ^ (quote o Display.raw_string_of_term o Const) (c, ty)) + |> debug_msg (fn _ => "generating constant " ^ (quote (c ^ " :: " ^ Sign.string_of_typ thy ty))) |> ensure_def (get_defgen tabs idf) strict ("generating constant " ^ quote c) idf |> pair idf end @@ -816,16 +814,16 @@ (* parametrized generators, for instantiation in HOL *) -fun appgen_number_of int_of_bin thy tabs (app as (c as (_, ty), [bin])) trns = - case try (int_of_bin thy) bin - of SOME i => if i < 0 then error ("negative numeral: " ^ IntInf.toString i) - (*preprocessor eliminates nat and negative numerals*) +fun appgen_rep_bin int_of_numeral thy tabs (app as (c as (_, ty), [bin])) trns = + case try (int_of_numeral thy) bin + of SOME i => if i < 0 then (*preprocessor eliminates negative numerals*) + trns + |> appgen_default thy (no_strict tabs) app else trns - |> pair (CodegenThingol.INum (i, IVar "")) - (*|> exprgen_term thy (no_strict tabs) (Const c) + |> exprgen_term thy (no_strict tabs) (Const c) ||>> exprgen_term thy (no_strict tabs) bin - |-> (fn (e1, e2) => pair (CodegenThingol.INum (i, e1 `$ e2)))*) + |-> (fn (e1, e2) => pair (CodegenThingol.INum (i, e1 `$ e2))) | NONE => trns |> appgen_default thy tabs app; @@ -890,7 +888,7 @@ (** theory interface **) -fun mk_tabs thy targets = +fun mk_tabs thy targets cs = let fun mk_insttab thy = let @@ -966,7 +964,7 @@ val insttab = mk_insttab thy; val overltabs = mk_overltabs thy; val dtcontab = mk_dtcontab thy; - in ((true, targets, Symtab.empty), (insttab, overltabs, dtcontab)) end; + in ((true, targets, CodegenTheorems.mk_thmtab thy cs), (insttab, overltabs, dtcontab)) end; fun get_serializer target = case Symtab.lookup (!serializers) target @@ -992,12 +990,12 @@ map_module (purge idfs) thy end;*) -fun expand_module targets init gen arg thy = +fun expand_module targets cs init gen arg thy = thy |> CodegenTheorems.notify_dirty |> `(#modl o CodegenData.get) |> (fn (modl, thy) => - (start_transact init (gen thy (mk_tabs thy targets) arg) modl, thy)) + (start_transact init (gen thy (mk_tabs thy targets cs) arg) modl, thy)) |-> (fn (x, modl) => map_module (K modl) #> pair x); fun rename_inconsistent thy = @@ -1024,17 +1022,26 @@ else add_alias (src, dst) thy in fold add inconsistent thy end; +fun consts_of t = + fold_aterms (fn Const c => cons c | _ => I) t []; + fun codegen_term t thy = - thy - |> expand_module (SOME [] (*(Symtab.keys (#target_data (CodegenData.get thy)))*)) NONE exprgen_term t; + let + val _ = Thm.cterm_of thy t; +(* val _ = writeln "STARTING GENERATION"; *) +(* val _ = (writeln o Sign.string_of_term thy) t; *) + in + thy + |> expand_module (SOME [] (*(Symtab.keys (#target_data (CodegenData.get thy)))*)) (consts_of t) NONE exprgen_term t + end; val is_dtcon = has_nsp nsp_dtcon; fun consts_of_idfs thy = - map (the o const_of_idf thy (mk_tabs thy NONE)); + map (the o const_of_idf thy (mk_tabs thy NONE [])); -fun idfs_of_consts thy = - map (idf_of_const thy (mk_tabs thy NONE)); +fun idfs_of_consts thy cs = + map (idf_of_const thy (mk_tabs thy NONE cs)) cs; fun get_root_module thy = thy @@ -1083,11 +1090,16 @@ | NONE => error ("not a constant: " ^ Sign.string_of_term thy t) end; -fun read_quote get reader gen raw thy = - thy - |> expand_module (SOME (Symtab.keys (#target_data (CodegenData.get thy)))) ((SOME o get) thy) - (fn thy => fn tabs => gen thy tabs o single o reader thy) raw - |-> (fn [x] => pair x); +fun read_quote get reader consts_of gen raw thy = + let + val it = reader thy raw; + val cs = consts_of it; + in + thy + |> expand_module (SOME (Symtab.keys (#target_data (CodegenData.get thy)))) cs ((SOME o get) thy) + (fn thy => fn tabs => gen thy tabs) [it] + |-> (fn [x] => pair x) + end; fun gen_add_syntax_class prep_class class target pretty thy = thy @@ -1138,7 +1150,7 @@ end; in CodegenSerializer.parse_syntax (fn thy => no_args_tyco thy raw_tyco) - (read_quote (fn thy => prep_tyco thy raw_tyco) read_typ + (read_quote (fn thy => prep_tyco thy raw_tyco) read_typ (K []) (fn thy => fn tabs => fold_map (exprgen_type thy tabs))) #-> (fn reader => pair (mk reader)) end; @@ -1159,7 +1171,9 @@ fun parse_syntax_const raw_const = let fun prep_const thy raw_const = - idf_of_const thy (mk_tabs thy NONE) (read_const thy raw_const); + let + val c_ty = read_const thy raw_const + in idf_of_const thy (mk_tabs thy NONE [c_ty]) c_ty end; fun no_args_const thy raw_const = (length o fst o strip_type o snd o read_const thy) raw_const; fun mk reader target thy = @@ -1173,7 +1187,7 @@ end; in CodegenSerializer.parse_syntax (fn thy => no_args_const thy raw_const) - (read_quote (fn thy => prep_const thy raw_const) Sign.read_term + (read_quote (fn thy => prep_const thy raw_const) Sign.read_term consts_of (fn thy => fn tabs => fold_map (exprgen_term thy tabs))) #-> (fn reader => pair (mk reader)) end; @@ -1181,17 +1195,21 @@ fun add_pretty_list raw_nil raw_cons (target, seri) thy = let val _ = get_serializer target; - val tabs = mk_tabs thy NONE; - fun mk_const raw_name = + fun prep_const raw = let - val name = Sign.intern_const thy raw_name; - in idf_of_const thy tabs (name, Sign.the_const_type thy name) end; - val nil' = mk_const raw_nil; - val cons' = mk_const raw_cons; - val pr' = CodegenSerializer.pretty_list nil' cons' seri; + val c = Sign.intern_const thy raw + in (c, Sign.the_const_type thy c) end; + val nil' = prep_const raw_nil; + val cons' = prep_const raw_cons; + val tabs = mk_tabs thy NONE [nil', cons']; + fun mk_const c_ty = + idf_of_const thy tabs c_ty; + val nil'' = mk_const nil'; + val cons'' = mk_const cons'; + val pr = CodegenSerializer.pretty_list nil'' cons'' seri; in thy - |> add_pretty_syntax_const cons' target pr' + |> add_pretty_syntax_const cons'' target pr end; @@ -1212,7 +1230,7 @@ val _ = case targets of SOME targets => (map get_serializer targets; ()) | _ => (); in thy - |> expand_module targets NONE (fold_map oo ensure_def_const) consts + |> expand_module targets consts NONE (fold_map oo ensure_def_const) consts |-> (fn cs => pair (SOME cs)) end | generate_code _ NONE thy = diff -r bb56a6cbacac -r d73e49780ef2 src/Pure/Tools/codegen_serializer.ML --- a/src/Pure/Tools/codegen_serializer.ML Tue Aug 08 08:19:18 2006 +0200 +++ b/src/Pure/Tools/codegen_serializer.ML Tue Aug 08 08:19:30 2006 +0200 @@ -746,11 +746,13 @@ in mk_memdefs (map from_supclass suparities) memdefs |> SOME end - | ml_from_def (name, CodegenThingol.Classinstmember) = NONE; + | ml_from_def (name, CodegenThingol.Classinstmember) = NONE + | ml_from_def (name, def) = error ("illegal definition for " ^ quote name ^ ": " ^ + (Pretty.output o CodegenThingol.pretty_def) def); in case defs - of (_, CodegenThingol.Fun _)::_ => (SOME o ml_from_funs o map (fn (name, CodegenThingol.Fun info) => (name, info))) defs - | (_, CodegenThingol.Datatypecons _)::_ => (SOME o ml_from_datatypes o filter_datatype) defs - | (_, CodegenThingol.Datatype _)::_ => (SOME o ml_from_datatypes o filter_datatype) defs + of (_, CodegenThingol.Fun _)::_ => ((*writeln "FUN";*) (SOME o ml_from_funs o map (fn (name, CodegenThingol.Fun info) => (name, info))) defs) + | (_, CodegenThingol.Datatypecons _)::_ => ((*writeln "DTCO";*) (SOME o ml_from_datatypes o filter_datatype) defs) + | (_, CodegenThingol.Datatype _)::_ => ((*writeln "DT";*) (SOME o ml_from_datatypes o filter_datatype) defs) | (_, CodegenThingol.Class _)::_ => (SOME o ml_from_class o filter_class) defs | (_, CodegenThingol.Classmember _)::_ => (SOME o ml_from_class o filter_class) defs | [def] => ml_from_def def diff -r bb56a6cbacac -r d73e49780ef2 src/Pure/Tools/codegen_theorems.ML --- a/src/Pure/Tools/codegen_theorems.ML Tue Aug 08 08:19:18 2006 +0200 +++ b/src/Pure/Tools/codegen_theorems.ML Tue Aug 08 08:19:30 2006 +0200 @@ -24,12 +24,11 @@ val common_typ: theory -> (thm -> typ) -> thm list -> thm list; val preprocess: theory -> thm list -> thm list; - val get_funs: theory -> string * typ -> thm list; val get_datatypes: theory -> string -> (((string * sort) list * (string * typ list) list) * thm list) option; type thmtab; - val mk_thmtab: (string * typ) list -> theory -> thmtab * theory; + val mk_thmtab: theory -> (string * typ) list -> thmtab; val norm_typ: theory -> string * typ -> string * typ; val get_sortalgebra: thmtab -> Sorts.algebra; val get_dtyp_of_cons: thmtab -> string * typ -> string option; @@ -42,7 +41,8 @@ val init_obj: (thm * thm) * (thm * thm) -> theory -> theory; val debug: bool ref; val debug_msg: ('a -> string) -> 'a -> 'a; - + structure ConstTab: TABLE; + structure ConstGraph: GRAPH; end; structure CodegenTheorems: CODEGEN_THEOREMS = @@ -412,7 +412,7 @@ (*) *) @ [ Pretty.fbrk, Pretty.block ( - Pretty.str "unfolding theorems:" + Pretty.str "inlined theorems:" :: Pretty.fbrk :: (Pretty.fbreaks o map pretty_thm) unfolds )]) @@ -610,6 +610,7 @@ #> Drule.zero_var_indexes ) |> drop_redundant thy + |> debug_msg (fn _ => "[cg_thm] preprocessing done") end; @@ -635,7 +636,7 @@ Theory.definitions_of thy c |> debug_msg (fn _ => "[cg_thm] trying spec") (* FIXME avoid dynamic name space lookup!? (via Thm.get_axiom_i etc.??) *) - |> maps (PureThy.get_thms thy o Name o #name) + |> maps (fn { name, ... } => these (try (PureThy.get_thms thy) (Name name))) |> map_filter (try (dest_fun thy)) |> filter_typ; in @@ -693,6 +694,33 @@ | _ => [] else []; +fun check_thms c thms = + let + fun check_head_lhs thm (lhs, rhs) = + case strip_comb lhs + of (Const (c', _), _) => if c' = c then () + else error ("illegal function equation for " ^ quote c + ^ ", actually defining " ^ quote c' ^ ": " ^ Display.string_of_thm thm) + | _ => error ("illegal function equation: " ^ Display.string_of_thm thm); + fun check_vars_lhs thm (lhs, rhs) = + if has_duplicates (op =) + (fold_aterms (fn Free (v, _) => cons v | _ => I) lhs []) + then error ("repeated variables on left hand side of function equation:" + ^ Display.string_of_thm thm) + else (); + fun check_vars_rhs thm (lhs, rhs) = + if null (subtract (op =) + (fold_aterms (fn Free (v, _) => cons v | _ => I) lhs []) + (fold_aterms (fn Free (v, _) => cons v | _ => I) rhs [])) + then () + else error ("free variables on right hand side of function equation:" + ^ Display.string_of_thm thm) + val tts = map (Logic.dest_equals o Logic.unvarify o Thm.prop_of) thms; + in + (map2 check_head_lhs thms tts; map2 check_vars_lhs thms tts; + map2 check_vars_rhs thms tts; thms) + end; + structure ConstTab = TableFun(type key = string * typ val ord = prod_ord fast_string_ord Term.typ_ord); structure ConstGraph = GraphFun(type key = string * typ val ord = prod_ord fast_string_ord Term.typ_ord); @@ -729,14 +757,10 @@ fun get_fun_thms (thy, (fungr, _), _) (c, ty) = let val (_, ty') = norm_typ thy (c, ty); - in these (try (ConstGraph.get_node fungr) (c, ty')) end; + in these (try (ConstGraph.get_node fungr) (c, ty')) |> check_thms c end; -fun mk_thmtab' thy cs = +fun mk_thmtab thy cs = let - fun get_dtco_candidate ty = - case strip_type ty - of (_, Type (tyco, _)) => SOME tyco - | _ => NONE; fun add_tycos (Type (tyco, tys)) = insert (op =) tyco #> fold add_tycos tys | add_tycos _ = I; val add_consts = fold_aterms @@ -745,7 +769,7 @@ fun add_dtyps_of_type ty thmtab = let val tycos = add_tycos ty []; - val tycos_new = filter (is_some o get_dtyp_spec thmtab) tycos; + val tycos_new = filter (is_none o get_dtyp_spec thmtab) tycos; fun add_dtyp_spec dtco (dtyp_spec as (vs, cs)) ((thy, (fungr, dtcotab), (algebra, dttab))) = let fun mk_co (c, tys) = @@ -777,66 +801,14 @@ val (_, ty') = norm_typ thy (c, ty); in thmtab - |> add_dtyps_of_type ty - |> add_funthms (c, ty) - end; - fun narrow_typs fungr = - let - (* - (*!!!remember whether any instantiation had been applied!!!*) - fun narrow_thms insts thms = - let - val (c_def, ty_def) = - (norm_typ thy o dest_Const o fst o Logic.dest_equals o Thm.prop_of o hd) thms; - val cs = fold (add_consts o snd o Logic.dest_equals o Thm.prop_of) thms []; - fun eval_inst c (inst, ty) = - let - val inst_ctxt = Sign.const_typargs thy (c, ty); - val inst_zip = fold (fn (v, ty) => (ty, (the o AList.lookup (op =) inst_ctxt) v)) inst - fun add_inst (ty_inst, ty_ctxt) = - if Sign.typ_instance thy (ty_inst, ty_ctxt) - then I - else Sign.typ_match thy (ty_ctxt, ty_inst); - in fold add_inst inst_zip end; - val inst = - Vartab.empty - |> fold (fn c_ty as (c, ty) => - case ConstTab.lookup insts (norm_typ thy c_ty) - of NONE => I - | SOME inst => eval_inst c (inst, ty)) cs - |> Vartab.dest - |> map (fn (v, (_, ty)) => (v, ty)); - val instT = map (fn (v, ty) => - (Thm.ctyp_of thy (TVar v, Thm.ctyp_of thy ty))) inst; - val thms' = - if null inst then NONE thms else - map Thm.instantiate (instT, []) thms; - val inst' = if null inst then NONE - else SOME inst; - in (inst', thms') end; - fun narrow_css [c] (insts, fungr) = - (* HIER GEHTS WEITER *) - (insts, fungr) - | narrow_css css (insts, fungr) = - (insts, fungr) - *) - val css = rev (Graph.strong_conn fungr); - in - (ConstTab.empty, fungr) - (*|> fold narrow_css css*) - |> snd + |> add_dtyps_of_type ty' + |> add_funthms (c, ty') end; in thmtab_empty thy |> fold add_c cs -(* |> (apfst o apfst) narrow_typs *) end; -fun mk_thmtab cs thy = - thy - |> get_reset_dirty - |> snd - |> `(fn thy => mk_thmtab' thy cs); (** code attributes and setup **) @@ -848,9 +820,10 @@ in val _ = map (Context.add_setup o add_simple_attribute) [ ("fun", add_fun), + ("nofun", del_fun), ("unfold", (fn thm => Codegen.add_unfold thm #> add_unfold thm)), ("inline", add_unfold), - ("nofold", del_unfold) + ("noinline", del_unfold) ] end; (*local*) diff -r bb56a6cbacac -r d73e49780ef2 src/Pure/Tools/codegen_thingol.ML --- a/src/Pure/Tools/codegen_thingol.ML Tue Aug 08 08:19:18 2006 +0200 +++ b/src/Pure/Tools/codegen_thingol.ML Tue Aug 08 08:19:30 2006 +0200 @@ -305,8 +305,8 @@ f e | map_pure f (e as _ `|-> _) = f e - | map_pure _ (INum _) = - error ("sorry, no pure representation for numerals so far") + | map_pure f (INum (_, e0)) = + f e0 | map_pure f (IChar (_, e0)) = f e0 | map_pure f (ICase (_, e0)) = @@ -808,10 +808,10 @@ @ maps (fn (name, modl) => (map o pairself) (NameSpace.append name) (alldeps modl)) modls end; val names = subtract (op =) hidden (allnames modl); - (*val _ = writeln "HIDDEN"; - val _ = (writeln o commas) hidden; - val _ = writeln "NAMES"; - val _ = (writeln o commas) names;*) +(* val _ = writeln "HIDDEN"; *) +(* val _ = (writeln o commas) hidden; *) +(* val _ = writeln "NAMES"; *) +(* val _ = (writeln o commas) names; *) fun is_bot name = case get_def modl name of Bot => true | _ => false; val bots = filter is_bot names; @@ -825,10 +825,10 @@ val selected = subtract (op =) bots' names; (* val deps = filter (fn (x, y) => member (op =) selected x andalso member (op =) selected y) *) val adddeps = maps (fn (n, ns) => map (pair n) ns) (expldeps |> Graph.del_nodes bots' |> Graph.dest); - (*val _ = writeln "SELECTED"; +(* val _ = writeln "SELECTED"; val _ = (writeln o commas) selected; val _ = writeln "DEPS"; - val _ = (writeln o cat_lines o map (fn (x, y) => x ^ " -> " ^ y)) adddeps;*) + val _ = (writeln o cat_lines o map (fn (x, y) => x ^ " -> " ^ y)) adddeps; *) in empty_module |> fold (fn name => add_def (name, get_def modl name)) selected