# HG changeset patch # User haftmann # Date 1144332505 -7200 # Node ID 3414c04fbc39df35a3e3cdfb2f6d7639276243b9 # Parent a4fe025ecd907502630c2a4162d1289c4dda80bc added definitional code generator module: codegen_theorems.ML diff -r a4fe025ecd90 -r 3414c04fbc39 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Thu Apr 06 16:08:22 2006 +0200 +++ b/src/Pure/IsaMakefile Thu Apr 06 16:08:25 2006 +0200 @@ -59,7 +59,7 @@ Thy/latex.ML Thy/present.ML Thy/thm_database.ML Thy/thm_deps.ML \ Thy/thy_info.ML Thy/thy_load.ML Tools/ROOT.ML Tools/class_package.ML \ Tools/codegen_thingol.ML Tools/codegen_serializer.ML Tools/codegen_package.ML \ - Tools/am_compiler.ML \ + Tools/codegen_theorems.ML Tools/am_compiler.ML \ Tools/am_interpreter.ML Tools/am_util.ML Tools/compute.ML axclass.ML \ Tools/nbe.ML Tools/nbe_eval.ML Tools/nbe_codegen.ML \ codegen.ML compress.ML consts.ML context.ML defs.ML display.ML \ diff -r a4fe025ecd90 -r 3414c04fbc39 src/Pure/Tools/ROOT.ML --- a/src/Pure/Tools/ROOT.ML Thu Apr 06 16:08:22 2006 +0200 +++ b/src/Pure/Tools/ROOT.ML Thu Apr 06 16:08:25 2006 +0200 @@ -7,12 +7,12 @@ (*class package*) use "class_package.ML"; +(*code generator, 1st generation*) +use "../codegen.ML"; + (*code generator theorems*) use "codegen_theorems.ML"; -(*code generator, 1st generation*) -use "../codegen.ML"; - (*code generator, 2nd generation*) use "codegen_thingol.ML"; use "codegen_serializer.ML"; diff -r a4fe025ecd90 -r 3414c04fbc39 src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Thu Apr 06 16:08:22 2006 +0200 +++ b/src/Pure/Tools/codegen_package.ML Thu Apr 06 16:08:25 2006 +0200 @@ -9,18 +9,12 @@ signature CODEGEN_PACKAGE = sig type auxtab; - type eqextr = theory -> auxtab - -> string * typ -> (thm list * typ) option; - type eqextr_default = theory -> auxtab - -> string * typ -> ((thm list * term option) * typ) option; type appgen = theory -> auxtab -> (string * typ) * term list -> CodegenThingol.transact -> CodegenThingol.iexpr * CodegenThingol.transact; val add_appconst: string * ((int * int) * appgen) -> theory -> theory; val add_appconst_i: xstring * ((int * int) * appgen) -> theory -> theory; - val add_eqextr: string * eqextr -> theory -> theory; - val add_eqextr_default: string * eqextr_default -> theory -> theory; val add_prim_class: xstring -> (string * string) -> theory -> theory; val add_prim_tyco: xstring -> (string * string) @@ -55,8 +49,6 @@ val appgen_number_of: (term -> term) -> (theory -> term -> IntInf.int) -> string -> string -> appgen; val appgen_wfrec: appgen; - val eqextr_eq: (theory -> string -> thm list) -> term - -> eqextr_default; val add_case_const: (theory -> string -> (string * int) list option) -> xstring -> theory -> theory; val add_case_const_i: (theory -> string -> (string * int) list option) -> string @@ -77,6 +69,7 @@ val alias_get: theory -> string -> string; val idf_of_name: theory -> string -> string -> string; val idf_of_const: theory -> auxtab -> string * typ -> string; + val idf_of_co: theory -> auxtab -> string * string -> string option; end; structure CodegenPackage : CODEGEN_PACKAGE = @@ -132,7 +125,7 @@ (* code generator basics *) -type deftab = (typ * (thm * string)) list Symtab.table; +type deftab = (typ * thm) list Symtab.table; fun eq_typ thy (ty1, ty2) = Sign.typ_instance thy (ty1, ty2) @@ -165,7 +158,7 @@ val prefix = case (AList.lookup (eq_typ thy) (Defs.specifications_of (Theory.defs_of thy) c)) ty - of SOME thyname => NameSpace.append thyname nsp_overl + of SOME (_, thyname) => NameSpace.append thyname nsp_overl | NONE => if c = "op =" then NameSpace.append @@ -368,7 +361,12 @@ logic_data = merge_logic_data (logic_data1, logic_data2), target_data = Symtab.join (K merge_target_data) (target_data1, target_data2) }; - fun print _ _ = (); + fun print thy (data : T) = + let + val module = #modl data + in + (Pretty.writeln o Pretty.chunks) [pretty_module module, pretty_deps module] + end; end); val _ = Context.add_setup CodegenData.init; @@ -381,13 +379,7 @@ in CodegenData.put { modl = modl, gens = gens, target_data = target_data, logic_data = logic_data } thy end; -fun print_code thy = - let - val module = (#modl o CodegenData.get) thy; - in - (Pretty.writeln o Pretty.chunks) [pretty_module module, pretty_deps module] - end; - +val print_code = CodegenData.print; (* advanced name handling *) @@ -403,7 +395,28 @@ 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_const thy (tabs as (deftab, (_, (overltab1, overltab2), dtcontab))) +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 + then try (DatatypeconsNameMangler.get thy dtcontab) (co, dtco) + |> the_default co + |> idf_of_name thy nsp_dtcon + |> SOME + else NONE + | NONE => NONE; + +fun co_of_idf thy (tabs as (_, (_, _, dtcontab))) idf = + case name_of_idf thy nsp_dtcon idf + of SOME idf' => let + val (c, dtco) = case try (DatatypeconsNameMangler.rev thy dtcontab) idf' + of SOME c_dtco => c_dtco + | NONE => case (snd o strip_type o Sign.the_const_type thy) idf' + of Type (dtco, _) => (idf', dtco) + | _ => (idf', "nat") (*a hack*) + in SOME (c, dtco) end + | NONE => NONE; + +fun idf_of_const thy (tabs as (deftab, (_, (overltab1, overltab2), _))) (c, ty) = let fun get_overloaded (c, ty) = @@ -416,11 +429,10 @@ | _ => NONE) fun get_datatypecons (c, ty) = case (snd o strip_type) ty - of Type (tyco, _) => - try (DatatypeconsNameMangler.get thy dtcontab) (c, tyco) + of Type (tyco, _) => idf_of_co thy tabs (c, tyco) | _ => NONE; in case get_datatypecons (c, ty) - of SOME c' => idf_of_name thy nsp_dtcon c' + of SOME idf => idf | NONE => case get_overloaded (c, ty) of SOME idf => idf | NONE => case ClassPackage.lookup_const_class thy c @@ -440,16 +452,6 @@ | NONE => NONE ); -fun const_of_idf thy (tabs as (_, (_, _, dtcontab))) idf = - case recconst_of_idf thy tabs idf - of SOME c_ty => SOME c_ty - | NONE => case dest_nsp nsp_mem idf - of SOME c => SOME (c, Sign.the_const_constraint thy c) - | NONE => case name_of_idf thy nsp_dtcon idf - of SOME idf' => let - val c = (fst o DatatypeconsNameMangler.rev thy dtcontab) idf' - in SOME (c, Sign.the_const_type thy c) end - | NONE => NONE; (* further theory data accessors *) @@ -469,31 +471,6 @@ val add_appconst = gen_add_appconst Sign.intern_const; val add_appconst_i = gen_add_appconst (K I); -fun add_eqextr (name, eqx) = - map_codegen_data - (fn (modl, gens, target_data, logic_data) => - (modl, - gens |> map_gens - (fn (appconst, eqextrs) => - (appconst, eqextrs - |> Output.update_warn (op =) ("overwriting existing equation extractor " ^ name) - (name, ((Option.map o apfst o rpair) NONE ooo eqx , stamp ())))), - target_data, logic_data)); - -fun add_eqextr_default (name, eqx) = - map_codegen_data - (fn (modl, gens, target_data, logic_data) => - (modl, - gens |> map_gens - (fn (appconst, eqextrs) => - (appconst, eqextrs - |> Output.update_warn (op =) ("overwriting existing equation extractor " ^ name) - (name, (eqx, stamp ())))), - target_data, logic_data)); - -fun get_eqextrs thy tabs = - (map (fn (name, (eqx, _)) => (name, eqx thy tabs)) o #eqextrs o #gens o CodegenData.get) thy; - fun set_get_all_datatype_cons f = map_codegen_data (fn (modl, gens, target_data, logic_data) => @@ -520,6 +497,15 @@ of NONE => K NONE | SOME (f, _) => f thy; +fun const_of_idf thy (tabs as (_, (_, _, dtcontab))) idf = + case recconst_of_idf thy tabs idf + of SOME c_ty => SOME c_ty + | NONE => case dest_nsp nsp_mem idf + of SOME c => SOME (c, Sign.the_const_constraint thy c) + | NONE => case co_of_idf thy tabs idf + of SOME (c, dtco) => SOME (c, Type (dtco, (the o AList.lookup (op =) ((snd o fst o the o CodegenTheorems.get_datatypes thy) dtco)) c)) + | NONE => NONE; + fun set_int_tyco tyco thy = (serializers := ( ! serializers @@ -533,75 +519,6 @@ ); thy); -(* sophisticated devarification *) - -fun devarify_typs tys = - let - fun add_rename (vi as (v, _), sorts) used = - let - val v' = "'" ^ variant used (unprefix "'" v) - in (map (fn sort => (((vi, sort), TFree (v', sort)), (v', TVar (vi, sort)))) sorts, v' :: used) end; - fun typ_names (Type (tyco, tys)) (vars, names) = - (vars, names |> insert (op =) (NameSpace.base tyco)) - |> fold typ_names tys - | typ_names (TFree (v, _)) (vars, names) = - (vars, names |> insert (op =) (unprefix "'" v)) - | typ_names (TVar (vi, sort)) (vars, names) = - (vars - |> AList.default (op =) (vi, []) - |> AList.map_entry (op =) vi (cons sort), - names); - val (vars, used) = fold typ_names tys ([], []); - val (renames, reverse) = fold_map add_rename vars used |> fst |> Library.flat |> split_list; - in - (reverse, map (Term.instantiateT renames) tys) - end; - -fun burrow_typs_yield f ts = - let - val typtab = - fold (fold_types (fn ty => Typtab.update (ty, dummyT))) - ts Typtab.empty; - val typs = Typtab.keys typtab; - val (x, typs') = f typs; - val typtab' = fold2 (Typtab.update oo pair) typs typs' typtab; - in - (x, (map o map_term_types) (the o Typtab.lookup typtab') ts) - end; - -fun devarify_terms ts = - let - fun add_rename (vi as (v, _), tys) used = - let - val v' = variant used v - in (map (fn ty => (((vi, ty), Free (v', ty)), (v', Var (vi, ty)))) tys, v' :: used) end; - fun term_names (Const (c, _)) (vars, names) = - (vars, names |> insert (op =) (NameSpace.base c)) - | term_names (Free (v, _)) (vars, names) = - (vars, names |> insert (op =) v) - | term_names (Var (vi, ty)) (vars, names) = - (vars - |> AList.default (op =) (vi, []) - |> AList.map_entry (op =) vi (cons ty), - names) - | term_names (Bound _) vars_names = - vars_names - | term_names (Abs (v, _, _)) (vars, names) = - (vars, names |> insert (op =) v) - | term_names (t1 $ t2) vars_names = - vars_names |> term_names t1 |> term_names t2 - val (vars, used) = fold term_names ts ([], []); - val (renames, reverse) = fold_map add_rename vars used |> fst |> Library.flat |> split_list; - in - (reverse, map (Term.instantiate ([], renames)) ts) - end; - -fun devarify_term_typs ts = - ts - |> devarify_terms - |-> (fn reverse => burrow_typs_yield devarify_typs - #-> (fn reverseT => pair (reverseT, reverse))); - (* definition and expression generators *) fun ensure_def_class thy tabs cls trns = @@ -615,7 +532,7 @@ val idfs = map (idf_of_name thy nsp_mem o fst) cs; in trns - |> debug 5 (fn _ => "trying defgen class declaration for " ^ quote cls) + |> debug_msg (fn _ => "trying defgen class declaration for " ^ quote cls) |> fold_map (ensure_def_class thy tabs) (ClassPackage.the_superclasses thy cls) ||>> (exprsgen_type thy tabs o map snd) cs ||>> (fold_map o fold_map) (exprgen_tyvar_sort thy tabs) sortctxts @@ -628,7 +545,7 @@ val cls' = idf_of_name thy nsp_class cls; in trns - |> debug 4 (fn _ => "generating class " ^ quote cls) + |> debug_msg (fn _ => "generating class " ^ quote cls) |> ensure_def [("class", defgen_class thy tabs)] ("generating class " ^ quote cls) cls' |> pair cls' end @@ -637,19 +554,16 @@ fun defgen_datatype thy (tabs as (_, (_, _, dtcontab))) dtco trns = case name_of_idf thy nsp_tyco dtco of SOME dtco => - (case get_datatype thy dtco - of SOME (vars, cos) => - let - val cos' = map (fn (co, tys) => (DatatypeconsNameMangler.get thy dtcontab (co, dtco) |> - idf_of_name thy nsp_dtcon, tys)) cos; - in - trns - |> debug 5 (fn _ => "trying defgen datatype for " ^ quote dtco) - |> fold_map (exprgen_tyvar_sort thy tabs) vars - ||>> fold_map (fn (c, ty) => exprsgen_type thy tabs ty #-> (fn ty' => pair (c, ty'))) cos' - |-> (fn (sorts, cos'') => succeed (Datatype - (sorts, cos''))) - end + (case CodegenTheorems.get_datatypes thy dtco + of SOME ((vars, cos), _) => + trns + |> debug_msg (fn _ => "trying defgen datatype for " ^ quote dtco) + |> fold_map (exprgen_tyvar_sort thy tabs) vars + ||>> fold_map (fn (c, ty) => + exprsgen_type thy tabs ty + #-> (fn ty' => pair ((the o idf_of_co thy tabs) (c, dtco), ty'))) cos + |-> (fn (vars, cos) => succeed (Datatype + (vars, cos))) | NONE => trns |> fail ("no datatype found for " ^ quote dtco)) @@ -659,7 +573,7 @@ val tyco' = idf_of_name thy nsp_tyco tyco; in trns - |> debug 4 (fn _ => "generating type constructor " ^ quote tyco) + |> debug_msg (fn _ => "generating type constructor " ^ quote tyco) |> ensure_def [("datatype", defgen_datatype thy tabs)] ("generating type constructor " ^ quote tyco) tyco' |> pair tyco' end @@ -684,7 +598,7 @@ ||>> fold_map (exprgen_type thy tabs) tys |-> (fn (tyco, tys) => pair (tyco `%% tys)) and exprsgen_type thy tabs = - fold_map (exprgen_type thy tabs) o snd o devarify_typs; + fold_map (exprgen_type thy tabs); fun exprgen_classlookup thy tabs (ClassPackage.Instance (inst, ls)) trns = trns @@ -695,46 +609,28 @@ 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 restrict (c, ty1) trns = - case get_first (fn (name, eqx) => (eqx (c, ty1))) (get_eqextrs thy tabs) - of SOME ((eq_thms, default), ty2) => +and mk_fun thy tabs (c, ty) trns = + case CodegenTheorems.get_funs thy (c, Type.varifyT ty) + of SOME (ty, eq_thms) => let - val ty3 = if restrict then ty1 else ty2; - val sortctxt = ClassPackage.extract_sortctxt thy ty3; - val instantiate = if restrict - then - let - val tab_lookup = snd o the o Vartab.lookup (Sign.typ_match thy (ty2, ty1) Vartab.empty); - in map_term_types (map_atyps (fn (TVar (vi, _)) => tab_lookup vi - | ty => ty)) end - else I + val sortctxt = ClassPackage.extract_sortctxt thy ty; fun dest_eqthm eq_thm = let val ((t, args), rhs) = - (apfst strip_comb o Logic.dest_equals o instantiate - o prop_of o Drule.zero_var_indexes) eq_thm; + (apfst strip_comb o Logic.dest_equals + o prop_of) eq_thm; in case t of Const (c', _) => if c' = c then (args, rhs) else error ("illegal function equation for " ^ quote c ^ ", actually defining " ^ quote c') | _ => error ("illegal function equation for " ^ quote c) end; - fun mk_default t = - let - val (tys, ty') = strip_type ty3; - val vs = Term.invent_names (add_term_names (t, [])) "x" (length tys); - in - if (not o eq_typ thy) (type_of t, ty') - then error ("inconsistent type for default rule") - else (map2 (curry Free) vs tys, t) - end; in trns |> (exprsgen_eqs thy tabs o map dest_eqthm) eq_thms - ||>> (exprsgen_eqs thy tabs o the_list o Option.map mk_default) default - ||>> exprsgen_type thy tabs [ty3] + ||>> exprsgen_type thy tabs [ty] ||>> fold_map (exprgen_tyvar_sort thy tabs) sortctxt - |-> (fn (((eqs, eq_default), [ty]), sortctxt) => (pair o SOME) ((eqs @ eq_default, (sortctxt, ty)), ty3)) + |-> (fn ((eqs, [ity]), sortctxt) => (pair o SOME) ((eqs, (sortctxt, ity)), ty)) end | NONE => (NONE, trns) and ensure_def_inst thy (tabs as (_, (insttab, _, _))) (cls, tyco) trns = @@ -753,17 +649,16 @@ |-> (fn ((supclass, inst), lss) => pair (supclass, (inst, lss))); fun gen_membr (m, ty) trns = trns - |> mk_fun thy tabs true (m, ty) + |> mk_fun thy tabs (m, ty) |-> (fn NONE => error ("could not derive definition for member " ^ quote m ^ " :: " ^ Sign.string_of_typ thy ty) - | SOME (funn, ty_use) => - (fold_map o fold_map) (exprgen_classlookup thy tabs) - (ClassPackage.extract_classlookup_member thy (ty, ty_use)) + | SOME (funn, ty_decl) => (fold_map o fold_map) (exprgen_classlookup thy tabs) + (ClassPackage.extract_classlookup_member thy (ty_decl, ty)) #-> (fn lss => pair (idf_of_name thy nsp_mem m, ((idf_of_name thy nsp_instmem m, funn), lss)))); in trns - |> debug 5 (fn _ => "trying defgen class instance for (" ^ quote cls + |> debug_msg (fn _ => "trying defgen class instance for (" ^ quote cls ^ ", " ^ quote tyco ^ ")") |> ensure_def_class thy tabs class ||>> ensure_def_tyco thy tabs tyco @@ -779,7 +674,7 @@ val inst = idf_of_name thy nsp_inst (InstNameMangler.get thy insttab (thyname, (cls, tyco))); in trns - |> debug 4 (fn _ => "generating instance " ^ quote cls ^ " / " ^ quote tyco) + |> debug_msg (fn _ => "generating instance " ^ quote cls ^ " / " ^ quote tyco) |> ensure_def [("instance", defgen_inst thy tabs)] ("generating instance " ^ quote cls ^ " / " ^ quote tyco) inst |> pair inst @@ -790,7 +685,7 @@ case recconst_of_idf thy tabs c of SOME (c, ty) => trns - |> mk_fun thy tabs false (c, ty) + |> mk_fun thy tabs (c, ty) |-> (fn SOME (funn, _) => succeed (Fun funn) | NONE => fail ("no defining equations found for " ^ quote c)) | NONE => @@ -800,16 +695,16 @@ case name_of_idf thy nsp_mem m of SOME m => trns - |> debug 5 (fn _ => "trying defgen class member for " ^ quote m) + |> debug_msg (fn _ => "trying defgen class member for " ^ quote m) |> ensure_def_class thy tabs ((the o ClassPackage.lookup_const_class thy) m) |-> (fn cls => succeed Undef) | _ => trns |> fail ("no class member found for " ^ quote m) fun defgen_datatypecons thy (tabs as (_, (_, _, dtcontab))) co trns = - case Option.map (DatatypeconsNameMangler.rev thy dtcontab) (name_of_idf thy nsp_dtcon co) + case co_of_idf thy tabs co of SOME (co, dtco) => trns - |> debug 5 (fn _ => "trying defgen datatype constructor for " ^ quote co) + |> debug_msg (fn _ => "trying defgen datatype constructor for " ^ quote co) |> ensure_def_tyco thy tabs dtco |-> (fn dtco => succeed Undef) | _ => @@ -827,7 +722,7 @@ val idf = idf_of_const thy tabs (c, ty); in trns - |> debug 4 (fn _ => "generating constant " ^ quote c) + |> debug_msg (fn _ => "generating constant " ^ quote c) |> ensure_def ((single o get_defgen) idf) ("generating constant " ^ quote c) idf |> pair idf end @@ -865,7 +760,7 @@ |-> (fn (e, es) => pair (e `$$ es)) end and exprsgen_term thy tabs = - fold_map (exprgen_term thy tabs) o snd o devarify_term_typs + fold_map (exprgen_term thy tabs) and exprsgen_eqs thy tabs = apfst (map (fn (rhs::args) => (args, rhs))) oo fold_burrow (exprsgen_term thy tabs) @@ -889,37 +784,23 @@ val tys = Library.take (d, ((fst o strip_type) ty)); in trns - |> debug 10 (fn _ => "eta-expanding") |> fold_map (exprgen_type thy tabs) tys ||>> ag thy tabs ((f, ty), ts @ map2 (curry Free) vs tys) |-> (fn (tys, e) => pair (vs ~~ tys `|--> e)) end else if length ts > imax then trns - |> debug 10 (fn _ => "splitting arguments (" ^ string_of_int imax ^ ", " - ^ string_of_int (length ts) ^ ")") |> ag thy tabs ((f, ty), Library.take (imax, ts)) ||>> fold_map (exprgen_term thy tabs) (Library.drop (imax, ts)) |-> (fn (e, es) => pair (e `$$ es)) else trns - |> debug 10 (fn _ => "keeping arguments") |> ag thy tabs ((f, ty), ts) | NONE => trns |> appgen_default thy tabs ((f, ty), ts); -(* function extractors *) - -fun eqextr_defs thy (deftab, _) (c, ty) = - Option.mapPartial (get_first (fn (ty', (thm, _)) => - if Sign.typ_instance thy (ty, ty') - then SOME ([thm], ty') - else NONE - )) (Symtab.lookup deftab c); - - (* parametrized generators, for instantiation in HOL *) fun appgen_split strip_abs thy tabs (app as (c_ty, [t])) trns = @@ -987,9 +868,9 @@ of Type ("fun", [Type (dtco, _), _]) => (case f thy dtco of [] => NONE - | [eq] => SOME ((Codegen.preprocess thy [eq], NONE), ty) - | eqs => SOME ((Codegen.preprocess thy eqs, SOME fals), ty)) - | _ => NONE) + | [eq] => SOME ((the o CodegenTheorems.preprocess_fun thy) [eq], NONE) + | eqs => SOME ((the o CodegenTheorems.preprocess_fun thy) eqs, SOME fals)) + | _ => NONE) |> Option.map (fn ((ty, eqs), default) => ((eqs, default), ty)) | eqextr_eq f fals thy tabs _ = NONE; @@ -1041,32 +922,6 @@ fun mk_tabs thy = let - fun extract_defs thy = - let - fun dest thm = - let - val (lhs, rhs) = Logic.dest_equals (prop_of thm); - val (t, args) = strip_comb lhs; - val (c, ty) = dest_Const t - in if forall is_Var args then SOME ((c, ty), thm) else NONE - end handle TERM _ => NONE; - fun prep_def def = (case Codegen.preprocess thy [def] of - [def'] => def' | _ => error "mk_tabs: bad preprocessor"); - fun add_def thyname (name, _) = - case (dest o prep_def o Thm.get_axiom thy) name - of SOME ((c, ty), thm) => - Symtab.default (c, []) - #> Symtab.map_entry c (cons (ty, (thm, thyname))) - | NONE => I - fun get_defs thy = - let - val thyname = Context.theory_name thy; - val defs = (snd o #axioms o Theory.rep_theory) thy; - in Symtab.fold (add_def thyname) defs end; - in - Symtab.empty - |> fold get_defs (thy :: Theory.ancestors_of thy) - end; fun mk_insttab thy = InstNameMangler.empty |> Symtab.fold_map @@ -1096,11 +951,20 @@ let val c = "op ="; val ty = Sign.the_const_type thy c; - fun inst dtco = - map_atyps (fn _ => Type (dtco, - (map (fn (v, sort) => TVar ((v, 0), sort)) o fst o the o get_datatype thy) dtco)) ty - val dtcos = fold (insert (op =) o snd) (get_all_datatype_cons thy) []; - val tys = map inst dtcos; + fun inst tyco = + let + val ty_inst = + tyco + |> Symtab.lookup ((snd o #types o Type.rep_tsig o Sign.tsig_of) thy) + |> (fn SOME (Type.LogicalType i, _) => i) + |> Term.invent_names [] "'a" + |> map (fn v => (TVar ((v, 0), Sign.defaultS thy))) + |> (fn tys => Type (tyco, tys)) + in map_atyps (fn _ => ty_inst) ty end; + val tys = + (Type.logical_types o Sign.tsig_of) thy + |> filter (fn tyco => (is_some oo try) (Sorts.mg_domain (Sign.classes_of thy, Sign.arities_of thy) tyco) (Sign.defaultS thy)) + |> map inst in (overltab1 |> Symtab.update_new (c, tys), @@ -1117,11 +981,10 @@ in AList.default (op =) (key, []) #> AList.map_entry (op =) key (cons (co, dtco)) end ) (get_all_datatype_cons thy) []) |-> (fn _ => I); - val deftab = extract_defs thy; val insttab = mk_insttab thy; val overltabs = mk_overltabs thy; val dtcontab = mk_dtcontab thy; - in (deftab, (insttab, overltabs, dtcontab)) end; + in (Symtab.empty, (insttab, overltabs, dtcontab)) end; fun get_serializer target = case Symtab.lookup (!serializers) target @@ -1132,6 +995,20 @@ map_codegen_data (fn (modl, gens, target_data, logic_data) => (f modl, gens, target_data, logic_data)); +(*fun delete_defs NONE thy = + map_module (K CodegenThingol.empty_module) thy + | delete_defs (SOME c) thy = + let + val tabs = mk_tabs thy; + in + map_module (CodegenThingol.purge_module []) thy + end; +does not make sense: +* primitve definitions have to be kept +* *all* overloaded defintitions for a constant have to be purged +* precondition: improved representation of definitions hidden by customary serializations +*) + fun expand_module init gen arg thy = (#modl o CodegenData.get) thy |> start_transact init (gen thy (mk_tabs thy) arg) @@ -1176,7 +1053,7 @@ fun codegen_term t thy = thy - |> expand_module NONE exprsgen_term [Codegen.preprocess_term thy t] + |> expand_module NONE exprsgen_term [CodegenTheorems.preprocess_term thy t] |-> (fn [t] => pair t); val is_dtcon = has_nsp nsp_dtcon; @@ -1208,8 +1085,13 @@ fun read_typ thy = Sign.read_typ (thy, K NONE); -fun read_const thy = - (dest_Const o Sign.read_term thy); +fun read_const thy raw_t = + let + val t = Sign.read_term thy raw_t + in case try dest_Const t + of SOME c => c + | NONE => error ("not a constant: " ^ Sign.string_of_term thy t) + end; fun read_quote get reader gen raw thy = thy @@ -1389,6 +1271,11 @@ |-> (fn cs => serialize cs) end; +fun purge_consts raw_ts thy = + let + val cs = map (read_const thy) raw_ts; + in fold CodegenTheorems.purge_defs cs thy end; + structure P = OuterParse and K = OuterKeyword @@ -1396,10 +1283,12 @@ val (generateK, serializeK, primclassK, primtycoK, primconstK, - syntax_classK, syntax_tycoK, syntax_constK, aliasK) = + syntax_classK, syntax_tycoK, syntax_constK, + purgeK, aliasK) = ("code_generate", "code_serialize", "code_primclass", "code_primtyco", "code_primconst", - "code_syntax_class", "code_syntax_tyco", "code_syntax_const", "code_alias"); + "code_syntax_class", "code_syntax_tyco", "code_syntax_const", + "code_purge", "code_alias"); val generateP = OuterSyntax.command generateK "generate executable code for constants" K.thy_decl ( @@ -1421,14 +1310,8 @@ )) ); -val aliasP = - OuterSyntax.command aliasK "declare an alias for a theory identifier" K.thy_decl ( - Scan.repeat1 (P.name -- P.name) - >> (Toplevel.theory oo fold) add_alias - ); - val primclassP = - OuterSyntax.command primclassK "define target-lanugage specific class" K.thy_decl ( + OuterSyntax.command primclassK "define target-language specific class" K.thy_decl ( P.xname -- Scan.repeat1 (P.name -- P.text) >> (fn (raw_class, primdefs) => @@ -1436,7 +1319,7 @@ ); val primtycoP = - OuterSyntax.command primtycoK "define target-lanugage specific type constructor" K.thy_decl ( + OuterSyntax.command primtycoK "define target-language specific type constructor" K.thy_decl ( P.xname -- Scan.repeat1 (P.name -- P.text) >> (fn (raw_tyco, primdefs) => @@ -1444,7 +1327,7 @@ ); val primconstP = - OuterSyntax.command primconstK "define target-lanugage specific constant" K.thy_decl ( + OuterSyntax.command primconstK "define target-language specific constant" K.thy_decl ( P.term -- Scan.repeat1 (P.name -- P.text) >> (fn (raw_const, primdefs) => @@ -1487,16 +1370,21 @@ (fn (target, modifier) => modifier target) ); -val _ = OuterSyntax.add_parsers [generateP, serializeP, aliasP, - primclassP, primtycoP, primconstP, syntax_tycoP, syntax_constP]; - - +val purgeP = + OuterSyntax.command purgeK "purge all defintions for constant" K.thy_decl ( + Scan.repeat1 P.term + >> (Toplevel.theory o purge_consts) + ); -(** theory setup **) +val aliasP = + OuterSyntax.command aliasK "declare an alias for a theory identifier" K.thy_decl ( + Scan.repeat1 (P.name -- P.name) + >> (Toplevel.theory oo fold) add_alias + ); -val _ = Context.add_setup ( - add_eqextr ("defs", eqextr_defs) -); +val _ = OuterSyntax.add_parsers [generateP, serializeP, + primclassP, primtycoP, primconstP, syntax_tycoP, syntax_constP, + purgeP, aliasP]; end; (* local *) diff -r a4fe025ecd90 -r 3414c04fbc39 src/Pure/Tools/codegen_serializer.ML --- a/src/Pure/Tools/codegen_serializer.ML Thu Apr 06 16:08:22 2006 +0200 +++ b/src/Pure/Tools/codegen_serializer.ML Thu Apr 06 16:08:25 2006 +0200 @@ -39,7 +39,7 @@ struct open BasicCodegenThingol; -val debug = CodegenThingol.debug; +val debug_msg = CodegenThingol.debug_msg; (** generic serialization **) @@ -244,15 +244,16 @@ of [] => NONE | ps => (SOME o Pretty.block) ps) end; - fun from_module' imps ((name_qual, name), defs) = - from_module imps ((name_qual, name), defs) |> postprocess name_qual; + fun from_module' resolv imps ((name_qual, name), defs) = + from_module resolv imps ((name_qual, name), defs) + |> postprocess (resolv name_qual); in module - |> debug 3 (fn _ => "selecting submodule...") - |> (if is_some select then (CodegenThingol.partof o the) select else I) - |> debug 3 (fn _ => "preprocessing...") + |> debug_msg (fn _ => "selecting submodule...") + |> (if is_some select then (CodegenThingol.project_module o the) select else I) + |> debug_msg (fn _ => "preprocessing...") |> preprocess - |> debug 3 (fn _ => "serializing...") + |> debug_msg (fn _ => "serializing...") |> CodegenThingol.serialize (from_defs (pretty_of_prim, (class_syntax : string -> string option, tyco_syntax, const_syntax))) from_module' validator postproc nspgrp name_root |> K () @@ -416,7 +417,10 @@ fun ml_from_sortlookup fxy lss = let fun from_label l = - Pretty.block [str "#", ml_from_label l]; + Pretty.block [str "#", + if (is_some o Int.fromString) l then str l + else ml_from_label l + ]; fun from_lookup fxy [] p = p | from_lookup fxy [l] p = brackify fxy [ @@ -552,10 +556,11 @@ ml_from_expr NOBR be ] in brackify fxy ( - str "case" + str "(case" :: typify dty (ml_from_expr NOBR de) :: mk_clause "of" bse :: map (mk_clause "|") bses + @ [str ")"] ) end | ml_from_expr _ e = error ("dubious expression: " ^ (Pretty.output o CodegenThingol.pretty_iexpr) e) @@ -806,7 +811,7 @@ fun ml_from_thingol target (nsp_dtcon, nsp_class, is_int_tyco) nspgrp = let - fun ml_from_module _ ((_, name), ps) = + fun ml_from_module resolv _ ((_, name), ps) = Pretty.chunks ([ str ("structure " ^ name ^ " = "), str "struct", @@ -832,12 +837,12 @@ else 0; fun preprocess const_syntax module = module - |> debug 3 (fn _ => "eta-expanding...") + |> debug_msg (fn _ => "eta-expanding...") |> CodegenThingol.eta_expand (eta_expander module const_syntax) - |> debug 3 (fn _ => "eta-expanding polydefs...") + |> debug_msg (fn _ => "eta-expanding polydefs...") |> CodegenThingol.eta_expand_poly - |> debug 3 (fn _ => "unclashing expression/type variables...") - |> CodegenThingol.unclash_vars_tvars; + (*|> debug 3 (fn _ => "unclashing expression/type variables...") + |> CodegenThingol.unclash_vars_tvars*); val parse_multi = OuterParse.name #-> (fn "dir" => @@ -871,12 +876,8 @@ fun hs_from_defs with_typs (from_prim, (class_syntax, tyco_syntax, const_syntax)) resolver prefix defs = let - fun resolv s = if NameSpace.is_qualified s - then resolver "" s - else if nth_string s 0 = "~" - then enclose "(" ")" ("negate " ^ unprefix "~" s) - else s; - val resolv_here = (resolver o NameSpace.base) prefix; + val resolv = resolver ""; + val resolv_here = resolver prefix; fun hs_from_sctxt vs = let fun from_class cls = @@ -895,11 +896,11 @@ |> from_sctxt end; fun hs_from_tycoexpr fxy (tyco, tys) = - brackify fxy ((str o resolv) tyco :: map (hs_from_type BR) tys) + brackify fxy (str tyco :: map (hs_from_type BR) tys) and hs_from_type fxy (tycoexpr as tyco `%% tys) = (case tyco_syntax tyco of NONE => - hs_from_tycoexpr fxy (tyco, tys) + hs_from_tycoexpr fxy (resolv tyco, tys) | SOME ((i, k), pr) => if not (i <= length tys andalso length tys <= k) then error ("number of argument mismatch in customary serialization: " @@ -944,7 +945,8 @@ end | hs_from_expr fxy (INum ((n, ty), _)) = brackify BR [ - (str o IntInf.toString) n, + (str o (fn s => if nth_string s 0 = "~" + then enclose "(" ")" ("negate " ^ unprefix "~" s) else s) o IntInf.toString) n, str "::", hs_from_type NOBR ty ] @@ -1099,7 +1101,7 @@ ] @ [ "Bool", "Integer", "Maybe", "True", "False", "Nothing", "Just", "not", "negate" ]; - fun hs_from_module imps ((_, name), ps) = + fun hs_from_module resolv imps ((_, name), ps) = (Pretty.chunks) ( str ("module " ^ name ^ " where") :: map (str o prefix "import qualified ") imps @ ( @@ -1121,7 +1123,7 @@ |> the_default 0; fun preprocess const_syntax module = module - |> debug 3 (fn _ => "eta-expanding...") + |> debug_msg (fn _ => "eta-expanding...") |> CodegenThingol.eta_expand (eta_expander const_syntax) in (Scan.optional (OuterParse.name >> (fn "no_typs" => false | s => Scan.fail_with (fn _ => "illegal flag: " ^ quote s) true)) true diff -r a4fe025ecd90 -r 3414c04fbc39 src/Pure/Tools/codegen_theorems.ML --- a/src/Pure/Tools/codegen_theorems.ML Thu Apr 06 16:08:22 2006 +0200 +++ b/src/Pure/Tools/codegen_theorems.ML Thu Apr 06 16:08:25 2006 +0200 @@ -1,4 +1,4 @@ -(* Title: Pure/Tools/CODEGEN_THEOREMS.ML +(* Title: Pure/Tools/codegen_theorems.ML ID: $Id$ Author: Florian Haftmann, TU Muenchen @@ -9,11 +9,31 @@ sig val add_notify: (string option -> theory -> theory) -> theory -> theory; val add_preproc: (theory -> thm list -> thm list) -> theory -> theory; - val add_funn: thm -> theory -> theory; + val add_fun_extr: (theory -> string * typ -> thm list) -> theory -> theory; + val add_datatype_extr: (theory -> string + -> (((string * sort) list * (string * typ list) list) * tactic) option) + -> theory -> theory; + val add_fun: thm -> theory -> theory; val add_pred: thm -> theory -> theory; val add_unfold: thm -> theory -> theory; - val preprocess: theory -> thm list -> thm list; + val del_def: thm -> theory -> theory; + val del_unfold: thm -> theory -> theory; + val purge_defs: string * typ -> theory -> theory; + + val common_typ: theory -> (thm -> typ) -> thm list -> thm list; + val preprocess: theory -> (thm -> typ) option -> thm list -> thm list; + val preprocess_fun: theory -> thm list -> (typ * thm list) option; val preprocess_term: theory -> term -> term; + val get_funs: theory -> string * typ -> (typ * thm list) option; + val get_datatypes: theory -> string + -> (((string * sort) list * (string * typ list) list) * thm list) option; + + val debug: bool ref; + val debug_msg: ('a -> string) -> 'a -> 'a; + + val print_thms: theory -> unit; + val init_obj: theory -> string -> string * (thm list -> tactic) -> string * (thm list -> tactic) + -> string * (thm list -> tactic) -> string * (thm list -> tactic) -> unit; end; structure CodegenTheorems: CODEGEN_THEOREMS = @@ -21,16 +41,126 @@ (** auxiliary **) -fun dest_funn thm = - case try (fst o dest_Const o fst o strip_comb o fst o Logic.dest_equals o prop_of) thm - of SOME c => SOME (c, thm) +val debug = ref false; +fun debug_msg f x = (if !debug then Output.debug (f x) else (); x); + + +(** object logic **) + +val obj_bool_ref : string option ref = ref NONE; +val obj_true_ref : string option ref = ref NONE; +val obj_false_ref : string option ref = ref NONE; +val obj_and_ref : string option ref = ref NONE; +val obj_eq_ref : string option ref = ref NONE; +val obj_eq_elim_ref : thm option ref = ref NONE; +fun idem c = (the o !) c; + +fun mk_tf sel = + let + val bool_typ = Type (idem obj_bool_ref, []); + val name = idem + (if sel then obj_true_ref else obj_false_ref); + in + Const (name, bool_typ) + end handle Option => error "no object logic setup for code theorems"; + +fun mk_obj_conj (x, y) = + let + val bool_typ = Type (idem obj_bool_ref, []); + in + Const (idem obj_and_ref, bool_typ --> bool_typ --> bool_typ) $ x $ y + end handle Option => error "no object logic setup for code theorems"; + +fun mk_obj_eq (x, y) = + let + val bool_typ = Type (idem obj_bool_ref, []); + in + Const (idem obj_eq_ref, type_of x --> type_of y --> bool_typ) $ x $ y + end handle Option => error "no object logic setup for code theorems"; + +fun is_obj_eq c = + c = idem obj_eq_ref + handle Option => error "no object logic setup for code theorems"; + +fun mk_bool_eq ((x, y), rhs) = + let + val bool_typ = Type (idem obj_bool_ref, []); + in + Logic.mk_equals ( + (mk_obj_eq (x, y)), + rhs + ) + end handle Option => error "no object logic setup for code theorems"; + +fun elim_obj_eq thm = rewrite_rule [idem obj_eq_elim_ref] thm + handle Option => error "no object logic setup for code theorems"; + +fun init_obj thy bohl (truh, truh_tac) (fals, fals_tac) (ant, ant_tac) (eq, eq_tac) = + let + val _ = if (is_some o !) obj_bool_ref + then error "already set" else () + val bool_typ = Type (bohl, []); + val free_typ = TFree ("'a", Sign.defaultS thy); + val var_x = Free ("x", free_typ); + val var_y = Free ("y", free_typ); + val prop_P = Free ("P", bool_typ); + val prop_Q = Free ("Q", bool_typ); + val _ = Goal.prove thy [] [] + (ObjectLogic.ensure_propT thy (Const (truh, bool_typ))) truh_tac; + val _ = Goal.prove thy ["P"] [ObjectLogic.ensure_propT thy (Const (fals, bool_typ))] + (ObjectLogic.ensure_propT thy prop_P) fals_tac; + val _ = Goal.prove thy ["P", "Q"] [ObjectLogic.ensure_propT thy prop_P, ObjectLogic.ensure_propT thy prop_Q] + (ObjectLogic.ensure_propT thy (Const (ant, bool_typ --> bool_typ --> bool_typ) $ prop_P $ prop_Q)) ant_tac; + val atomize_eq = Goal.prove thy ["x", "y"] [] + (Logic.mk_equals ( + Logic.mk_equals (var_x, var_y), + ObjectLogic.ensure_propT thy + (Const (eq, free_typ --> free_typ --> bool_typ) $ var_x $ var_y))) eq_tac; + in + obj_bool_ref := SOME bohl; + obj_true_ref := SOME truh; + obj_false_ref := SOME fals; + obj_and_ref := SOME ant; + obj_eq_ref := SOME eq; + obj_eq_elim_ref := SOME (Thm.symmetric atomize_eq) + end; + + +(** auxiliary **) + +fun destr_fun thy thm = + case try ( + prop_of + #> ObjectLogic.drop_judgment thy + #> Logic.dest_equals + #> fst + #> strip_comb + #> fst + #> dest_Const + ) (elim_obj_eq thm) + of SOME c_ty => SOME (c_ty, thm) | NONE => NONE; +fun dest_fun thy thm = + case destr_fun thy thm + of SOME x => x + | NONE => error ("not a function equation: " ^ string_of_thm thm); + fun dest_pred thm = case try (fst o dest_Const o fst o strip_comb o snd o Logic.dest_implies o prop_of) thm of SOME c => SOME (c, thm) | NONE => NONE; +fun getf_first [] _ = NONE + | getf_first (f::fs) x = case f x + of NONE => getf_first fs x + | y as SOME x => y; + +fun getf_first_list [] x = [] + | getf_first_list (f::fs) x = case f x + of [] => getf_first_list fs x + | xs => xs; + (** theory data **) @@ -46,49 +176,113 @@ mk_procs (AList.merge (op =) (K true) (preprocs1, preprocs2), AList.merge (op =) (K true) (notify1, notify2)); +datatype extrs = Extrs of { + funs: (serial * (theory -> string * typ -> thm list)) list, + datatypes: (serial * (theory -> string -> (((string * sort) list * (string * typ list) list) * tactic) option)) list +}; + +fun mk_extrs (funs, datatypes) = Extrs { funs = funs, datatypes = datatypes }; +fun map_extrs f (Extrs { funs, datatypes }) = mk_extrs (f (funs, datatypes)); +fun merge_extrs _ (Extrs { funs = funs1, datatypes = datatypes1 }, + Extrs { funs = funs2, datatypes = datatypes2 }) = + mk_extrs (AList.merge (op =) (K true) (funs1, funs2), + AList.merge (op =) (K true) (datatypes1, datatypes2)); + datatype codethms = Codethms of { - funns: thm list Symtab.table, + funs: thm list Symtab.table, preds: thm list Symtab.table, unfolds: thm list }; -fun mk_codethms ((funns, preds), unfolds) = - Codethms { funns = funns, preds = preds, unfolds = unfolds }; -fun map_codethms f (Codethms { funns, preds, unfolds }) = - mk_codethms (f ((funns, preds), unfolds)); -fun merge_codethms _ (Codethms { funns = funns1, preds = preds1, unfolds = unfolds1 }, - Codethms { funns = funns2, preds = preds2, unfolds = unfolds2 }) = - mk_codethms ((Symtab.join (K (uncurry (fold (insert eq_thm)))) (funns1, funns2), +fun mk_codethms ((funs, preds), unfolds) = + Codethms { funs = funs, preds = preds, unfolds = unfolds }; +fun map_codethms f (Codethms { funs, preds, unfolds }) = + mk_codethms (f ((funs, preds), unfolds)); +fun merge_codethms _ (Codethms { funs = funs1, preds = preds1, unfolds = unfolds1 }, + Codethms { funs = funs2, preds = preds2, unfolds = unfolds2 }) = + mk_codethms ((Symtab.join (K (uncurry (fold (insert eq_thm)))) (funs1, funs2), Symtab.join (K (uncurry (fold (insert eq_thm)))) (preds1, preds2)), fold (insert eq_thm) unfolds1 unfolds2); +datatype codecache = Codecache of { + funs: thm list Symtab.table, + datatypes: (string * typ list) list Symtab.table +}; + +fun mk_codecache (funs, datatypes) = Codecache { funs = funs, datatypes = datatypes }; +fun map_codecache f (Extrs { funs, datatypes }) = Codecache (f (funs, datatypes)); +fun merge_codecache _ (Codecache { funs = funs1, datatypes = datatypes1 }, + Extrs { funs = funs2, datatypes = datatypes2 }) = + mk_codecache (Symtab.empty, Symtab.empty); + datatype T = T of { procs: procs, + extrs: extrs, codethms: codethms }; -fun mk_T (procs, codethms) = T { procs = procs, codethms = codethms }; -fun map_T f (T { procs, codethms }) = mk_T (f (procs, codethms)); -fun merge_T pp (T { procs = procs1, codethms = codethms1 }, - T { procs = procs2, codethms = codethms2 }) = - mk_T (merge_procs pp (procs1, procs2), merge_codethms pp (codethms1, codethms2)); +fun mk_T (procs, (extrs, codethms)) = T { procs = procs, extrs = extrs, codethms = codethms }; +fun map_T f (T { procs, extrs, codethms }) = mk_T (f (procs, (extrs, codethms))); +fun merge_T pp (T { procs = procs1, extrs = extrs1, codethms = codethms1 }, + T { procs = procs2, extrs = extrs2, codethms = codethms2 }) = + mk_T (merge_procs pp (procs1, procs2), (merge_extrs pp (extrs1, extrs2), merge_codethms pp (codethms1, codethms2))); structure CodegenTheorems = TheoryDataFun (struct val name = "Pure/CodegenTheorems"; type T = T; val empty = mk_T (mk_procs ([], []), - mk_codethms ((Symtab.empty, Symtab.empty), [])); + (mk_extrs ([], []), mk_codethms ((Symtab.empty, Symtab.empty), []))); val copy = I; val extend = I; val merge = merge_T; - fun print _ _ = (); + fun print (thy : theory) (data : T) = + let + val codethms = (fn T { codethms, ... } => codethms) data; + val funs = (Symtab.dest o (fn Codethms { funs, ... } => funs)) codethms; + val preds = (Symtab.dest o (fn Codethms { preds, ... } => preds)) codethms; + val unfolds = (fn Codethms { unfolds, ... } => unfolds) codethms; + in + (Pretty.writeln o Pretty.block o Pretty.fbreaks) ([ + Pretty.str "code generation theorems:", + Pretty.str "function theorems:" ] @ + Pretty.fbreaks ( + map (fn (c, thms) => + (Pretty.block o Pretty.fbreaks) ( + Pretty.str c :: map Display.pretty_thm thms + ) + ) funs + ) @ [ + Pretty.str "predicate theorems:" ] @ + Pretty.fbreaks ( + map (fn (c, thms) => + (Pretty.block o Pretty.fbreaks) ( + Pretty.str c :: map Display.pretty_thm thms + ) + ) preds + ) @ [ + Pretty.str "unfolding theorems:", + (Pretty.block o Pretty.fbreaks o map Display.pretty_thm) unfolds + ]) + end; end); val _ = Context.add_setup CodegenTheorems.init; - +val print_thms = CodegenTheorems.print; -(** notifiers and preprocessors **) +local + val the_procs = (fn T { procs = Procs procs, ... } => procs) o CodegenTheorems.get + val the_extrs = (fn T { extrs = Extrs extrs, ... } => extrs) o CodegenTheorems.get + val the_codethms = (fn T { codethms = Codethms codethms, ... } => codethms) o CodegenTheorems.get +in + val the_preprocs = (fn { preprocs, ... } => map snd preprocs) o the_procs; + val the_notify = (fn { notify, ... } => map snd notify) o the_procs; + val the_funs_extrs = (fn { funs, ... } => map snd funs) o the_extrs; + val the_datatypes_extrs = (fn { datatypes, ... } => map snd datatypes) o the_extrs; + val the_funs = (fn { funs, ... } => funs) o the_codethms; + val the_preds = (fn { preds, ... } => preds) o the_codethms; + val the_unfolds = (fn { unfolds, ... } => unfolds) o the_codethms; +end (*local*); fun add_notify f = CodegenTheorems.map (map_T (fn (procs, codethms) => @@ -96,8 +290,7 @@ (preprocs, (serial (), f) :: notify)), codethms))); fun notify_all c thy = - fold (fn f => f c) (((fn Procs { notify, ... } => map snd notify) - o (fn T { procs, ... } => procs) o CodegenTheorems.get) thy) thy; + fold (fn f => f c) (the_notify thy) thy; fun add_preproc f = CodegenTheorems.map (map_T (fn (procs, codethms) => @@ -105,44 +298,220 @@ ((serial (), f) :: preprocs, notify)), codethms))) #> notify_all NONE; -fun preprocess thy = - fold (fn f => f thy) (((fn Procs { preprocs, ... } => map snd preprocs) - o (fn T { procs, ... } => procs) o CodegenTheorems.get) thy); +fun add_fun_extr f = + CodegenTheorems.map (map_T (fn (procs, (extrs, codethms)) => + (procs, (extrs |> map_extrs (fn (funs, datatypes) => + ((serial (), f) :: funs, datatypes)), codethms)))) + #> notify_all NONE; + +fun add_datatype_extr f = + CodegenTheorems.map (map_T (fn (procs, (extrs, codethms)) => + (procs, (extrs |> map_extrs (fn (funs, datatypes) => + (funs, (serial (), f) :: datatypes)), codethms)))) + #> notify_all NONE; + +fun add_fun thm thy = + case destr_fun thy thm + of SOME ((c, _), _) => + thy + |> CodegenTheorems.map (map_T (fn (procs, (extrs, codethms)) => + (procs, (extrs, codethms |> map_codethms (fn ((funs, preds), unfolds) => + ((funs |> Symtab.default (c, []) |> Symtab.map_entry c (fn thms => thms @ [thm]), preds), unfolds)))))) + |> notify_all (SOME c) + | NONE => tap (fn _ => warning ("not a function equation: " ^ string_of_thm thm)) thy; + +fun add_pred thm thy = + case dest_pred thm + of SOME (c, _) => + thy + |> CodegenTheorems.map (map_T (fn (procs, (extrs, codethms)) => + (procs, (extrs, codethms |> map_codethms (fn ((funs, preds), unfolds) => + ((funs, preds |> Symtab.default (c, []) |> Symtab.map_entry c (fn thms => thms @ [thm])), unfolds)))))) + |> notify_all (SOME c) + | NONE => tap (fn _ => warning ("not a predicate clause: " ^ string_of_thm thm)) thy; + +fun add_unfold thm = + CodegenTheorems.map (map_T (fn (procs, (extrs, codethms)) => + (procs, (extrs, codethms |> map_codethms (fn (defs, unfolds) => + (defs, thm :: unfolds)))))) + #> notify_all NONE; + +fun del_def thm thy = + case destr_fun thy thm + of SOME ((c, _), thm) => + thy + |> CodegenTheorems.map (map_T (fn (procs, (extrs, codethms)) => + (procs, (extrs, codethms |> map_codethms (fn ((funs, preds), unfolds) => + ((funs |> Symtab.map_entry c (remove eq_thm thm), preds), unfolds)))))) + |> notify_all (SOME c) + | NONE => case dest_pred thm + of SOME (c, thm) => + thy + |> CodegenTheorems.map (map_T (fn (procs, (extrs, codethms)) => + (procs, (extrs, codethms |> map_codethms (fn ((funs, preds), unfolds) => + ((funs, preds |> Symtab.map_entry c (remove eq_thm thm)), unfolds)))))) + |> notify_all (SOME c) + | NONE => error ("no code theorem to delete"); + +fun del_unfold thm = + CodegenTheorems.map (map_T (fn (procs, (extrs, codethms)) => + (procs, (extrs, codethms |> map_codethms (fn (defs, unfolds) => + (defs, remove eq_thm thm unfolds)))))) + #> notify_all NONE; + +fun purge_defs (c, ty) thy = + thy + |> CodegenTheorems.map (map_T (fn (procs, (extrs, codethms)) => + (procs, (extrs, codethms |> map_codethms (fn ((funs, preds), unfolds) => + ((funs |> Symtab.map_entry c + (filter (fn thm => Sign.typ_instance thy ((snd o fst o dest_fun thy) thm, ty))), + preds |> Symtab.update (c, [])), unfolds)))))) + |> notify_all (SOME c); + + +(** preprocessing **) + +fun common_typ thy _ [] = [] + | common_typ thy _ [thm] = [thm] + | common_typ thy extract_typ thms = + let + fun incr_thm thm max = + let + val thm' = incr_indexes max thm; + val max' = (maxidx_of_typ o type_of o prop_of) thm' + 1; + in (thm', max') end; + val (thms', maxidx) = fold_map incr_thm thms 0; + val (ty1::tys) = map extract_typ thms; + fun unify ty = Type.unify (Sign.tsig_of thy) (ty1, ty); + val (env, _) = fold unify tys (Vartab.empty, maxidx) + val instT = Vartab.fold (fn (x_i, (sort, ty)) => + cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env []; + in map (Thm.instantiate (instT, [])) thms end; + +fun preprocess thy extract_typ thms = + thms + |> map (Thm.transfer thy) + |> fold (fn f => f thy) (the_preprocs thy) + |> map (rewrite_rule (the_unfolds thy)) + |> (if is_some extract_typ then common_typ thy (the extract_typ) else I) + |> Drule.conj_intr_list + |> Drule.zero_var_indexes + |> Drule.conj_elim_list + |> map Drule.unvarifyT + |> map Drule.unvarify; + +fun preprocess_fun thy thms = + let + fun tap_typ [] = NONE + | tap_typ (thms as (thm::_)) = SOME ((snd o fst o dest_fun thy) thm, thms) + in + thms + |> map elim_obj_eq + |> preprocess thy (SOME (snd o fst o dest_fun thy)) + |> tap_typ + end; fun preprocess_term thy t = let - val x = Free (variant (add_term_names (t, [])) "x", fastype_of t); - (* fake definition *) + val x = Free (variant (add_term_names (t, [])) "a", fastype_of t); + (*fake definition*) val eq = setmp quick_and_dirty true (SkipProof.make_thm thy) (Logic.mk_equals (x, t)); fun err () = error "preprocess_term: bad preprocessor" - in case map prop_of (preprocess thy [eq]) of + in case map prop_of (preprocess thy NONE [eq]) of [Const ("==", _) $ x' $ t'] => if x = x' then t' else err () | _ => err () end; -fun add_unfold thm = - CodegenTheorems.map (map_T (fn (procs, codethms) => - (procs, codethms |> map_codethms (fn (defs, unfolds) => - (defs, thm :: unfolds))))) + +(** retrieval **) + +fun get_funs thy (c, ty) = + let + val filter_typ = Library.mapfilter (fn ((_, ty'), thm) => + if Sign.typ_instance thy (ty', ty) + orelse Sign.typ_instance thy (ty, ty') + then SOME thm else debug_msg (fn _ => "dropping " ^ string_of_thm thm) NONE); + val thms_funs = + (these o Symtab.lookup (the_funs thy)) c + |> map (dest_fun thy) + |> filter_typ; + val thms = case thms_funs + of [] => + Defs.specifications_of (Theory.defs_of thy) c + |> map (PureThy.get_thms thy o Name o fst o snd) + |> Library.flat + |> append (getf_first_list (map (fn f => f thy) (the_funs_extrs thy)) (c, ty)) + |> map (dest_fun thy) + |> filter_typ + | thms => thms + in + thms + |> preprocess_fun thy + end; -fun add_funn thm = - case dest_funn thm - of SOME (c, thm) => - CodegenTheorems.map (map_T (fn (procs, codethms) => - (procs, codethms |> map_codethms (fn ((funns, preds), unfolds) => - ((funns |> Symtab.default (c, []) |> Symtab.map (fn thms => thms @ [thm]), preds), unfolds))))) - | NONE => error ("not a function equation: " ^ string_of_thm thm); +fun get_datatypes thy dtco = + let + val truh = mk_tf true; + val fals = mk_tf false; + fun mk_lhs vs ((co1, tys1), (co2, tys2)) = + let + val dty = Type (dtco, map TFree vs); + val (xs1, xs2) = chop (length tys1) (Term.invent_names [] "x" (length tys1 + length tys2)); + val frees1 = map2 (fn x => fn ty => Free (x, ty)) xs1 tys1; + val frees2 = map2 (fn x => fn ty => Free (x, ty)) xs2 tys2; + fun zip_co co xs tys = list_comb (Const (co, + tys ---> dty), map2 (fn x => fn ty => Free (x, ty)) xs tys); + in + ((frees1, frees2), (zip_co co1 xs1 tys1, zip_co co2 xs2 tys2)) + end; + fun mk_rhs [] [] = truh + | mk_rhs xs ys = foldr1 mk_obj_conj (map2 (curry mk_obj_eq) xs ys); + fun mk_eq vs (args as ((co1, _), (co2, _))) (inj, dist) = + if co1 = co2 + then let + val ((fs1, fs2), lhs) = mk_lhs vs args; + val rhs = mk_rhs fs1 fs2; + in (mk_bool_eq (lhs, rhs) :: inj, dist) end + else let + val (_, lhs) = mk_lhs vs args; + in (inj, mk_bool_eq (lhs, fals) :: dist) end; + fun mk_eqs (vs, cos) = + let val cos' = rev cos + in (op @) (fold (mk_eq vs) (product cos' cos') ([], [])) end; + fun mk_eq_thms tac vs_cos = + map (fn t => (Goal.prove thy [] [] + (ObjectLogic.ensure_propT thy t) (K tac))) (mk_eqs vs_cos); + in + case getf_first (map (fn f => f thy) (the_datatypes_extrs thy)) dtco + of NONE => NONE + | SOME (vs_cos, tac) => SOME (vs_cos, mk_eq_thms tac vs_cos) + end; -fun add_pred thm = - case dest_pred thm - of SOME (c, thm) => - CodegenTheorems.map (map_T (fn (procs, codethms) => - (procs, codethms |> map_codethms (fn ((funns, preds), unfolds) => - ((funns, preds |> Symtab.default (c, []) |> Symtab.map (fn thms => thms @ [thm])), unfolds))))) - | NONE => error ("not a predicate clause: " ^ string_of_thm thm); +fun get_eq thy (c, ty) = + if is_obj_eq c + then case get_datatypes thy ((fst o dest_Type o hd o fst o strip_type) ty) + of SOME (_, thms) => thms + | _ => [] + else []; -(** isar **) +(** code attributes and setup **) -end; (* struct *) +local + fun add_simple_attribute (name, f) = + (Codegen.add_attribute name o (Scan.succeed o Thm.declaration_attribute)) + (Context.map_theory o f); +in + val _ = map (Context.add_setup o add_simple_attribute) [ + ("fun", add_fun), + ("pred", add_pred), + ("unfold", (fn thm => Codegen.add_unfold thm #> add_unfold thm)), + ("unfolt", add_unfold), + ("nofold", del_unfold) + ] +end; (*local*) + +val _ = Context.add_setup (add_fun_extr get_eq); + +end; (*struct*) diff -r a4fe025ecd90 -r 3414c04fbc39 src/Pure/Tools/codegen_thingol.ML --- a/src/Pure/Tools/codegen_thingol.ML Thu Apr 06 16:08:22 2006 +0200 +++ b/src/Pure/Tools/codegen_thingol.ML Thu Apr 06 16:08:25 2006 +0200 @@ -84,12 +84,13 @@ val pretty_module: module -> Pretty.T; val pretty_deps: module -> Pretty.T; val empty_module: module; + val get_def: module -> string -> def; val add_prim: string -> (string * prim list) -> module -> module; val ensure_prim: string -> string -> module -> module; - val get_def: module -> string -> def; val merge_module: module * module -> module; val diff_module: module * module -> (string * def) list; - val partof: string list -> module -> module; + val project_module: string list -> module -> module; + val purge_module: string list -> module -> module; val has_nsp: string -> string -> bool; val succeed: 'a -> transact -> 'a transact_fin; val fail: string -> transact -> 'a transact_fin; @@ -101,13 +102,13 @@ val eta_expand_poly: module -> module; val unclash_vars_tvars: module -> module; - val debug_level: int ref; - val debug: int -> ('a -> string) -> 'a -> 'a; + val debug: bool ref; + val debug_msg: ('a -> string) -> 'a -> 'a; val soft_exc: bool ref; val serialize: ((string -> string -> string) -> string -> (string * def) list -> 'a option) - -> (string list -> (string * string) * 'a list -> 'a option) + -> ((string -> string) -> string list -> (string * string) * 'a list -> 'a option) -> (string -> string option) -> (string * string -> string) -> string list list -> string -> module -> 'a option; @@ -118,8 +119,8 @@ (** auxiliary **) -val debug_level = ref 0; -fun debug d f x = (if d <= !debug_level then Output.debug (f x) else (); x); +val debug = ref false; +fun debug_msg f x = (if !debug then Output.debug (f x) else (); x); val soft_exc = ref true; fun unfoldl dest x = @@ -204,11 +205,11 @@ val op `|--> = Library.foldr (op `|->); val pretty_sortcontext = - Pretty.commas o map (fn (v, sort) => (Pretty.block o Pretty.breaks) + Pretty.list "(" ")" o Pretty.commas o map (fn (v, sort) => (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "::", Pretty.enum "&" "" "" (map Pretty.str sort)]); fun pretty_itype (tyco `%% tys) = - Pretty.block (Pretty.str tyco :: map pretty_itype tys) + Pretty.enum "" "(" ")" (Pretty.str tyco :: map pretty_itype tys) | pretty_itype (ty1 `-> ty2) = Pretty.enum "" "(" ")" [pretty_itype ty1, Pretty.str "->", pretty_itype ty2] | pretty_itype (ITyVar v) = @@ -437,7 +438,7 @@ Pretty.str "" | pretty_def (Prim prims) = Pretty.str ("") - | pretty_def (Fun (eqs, (_, ty))) = + | pretty_def (Fun (eqs, (sortctxt, ty))) = Pretty.enum " |" "" "" ( map (fn (ps, body) => Pretty.block [ @@ -446,18 +447,20 @@ Pretty.brk 1, pretty_iexpr body, Pretty.str "::", + pretty_sortcontext sortctxt, + Pretty.str "/", pretty_itype ty ]) eqs ) | pretty_def (Typesyn (vs, ty)) = Pretty.block [ - Pretty.list "(" ")" (pretty_sortcontext vs), + pretty_sortcontext vs, Pretty.str " |=> ", pretty_itype ty ] | pretty_def (Datatype (vs, cs)) = Pretty.block [ - Pretty.list "(" ")" (pretty_sortcontext vs), + pretty_sortcontext vs, Pretty.str " |=> ", Pretty.enum " |" "" "" (map (fn (c, tys) => (Pretty.block o Pretty.breaks) @@ -715,7 +718,9 @@ ((AList.make (Graph.get_node modl1) o Library.flat o Graph.strong_conn) modl1) in diff_modl [] modl12 [] end; -fun partof names modl = +local + +fun project_trans f names modl = let datatype pathnode = PN of (string list * (string * pathnode) list); fun mk_ipath ([], base) (PN (defs, modls)) = @@ -727,7 +732,7 @@ |> (pair defs #> PN); fun select (PN (defs, modls)) (Module module) = module - |> Graph.subgraph (Graph.all_succs module (defs @ map fst modls)) + |> f (Graph.all_succs module (defs @ map fst modls)) |> fold (fn (name, modls) => Graph.map_node name (select modls)) modls |> Module; in @@ -737,16 +742,34 @@ |> dest_modl end; +in + +val project_module = project_trans Graph.subgraph; +val purge_module = project_trans Graph.del_nodes; + +end; (*local*) + fun imports_of modl name = let + (*fun submodules prfx modl = + cons prfx + #> Graph.fold_nodes + (fn (m, Module modl) => submodules (prfx @ [m]) modl + | (_, Def _) => I) modl; + fun get_modl name = + fold (fn n => fn modl => (dest_modl oo Graph.get_node) modl n) name modl*) fun imports prfx [] modl = [] | imports prfx (m::ms) modl = map (cons m) (imports (prfx @ [m]) ms ((dest_modl oo Graph.get_node) modl m)) - @ map single (Graph.imm_succs modl m); + @ map single (Graph.imm_succs modl m) in modl |> imports [] name + (*|> cons name + |> map (fn name => submodules name (get_modl name) []) + |> Library.flat + |> remove (op =) name*) |> map NameSpace.pack end; @@ -808,11 +831,11 @@ else error ("inconsistent type for member definition " ^ quote m ^ " [" ^ v ^ "]: " ^ (Pretty.output o Pretty.block o Pretty.breaks) [ - Pretty.list "(" ")" (pretty_sortcontext sortctxt''), + pretty_sortcontext sortctxt'', Pretty.str "|=>", pretty_itype ty'' ] ^ " vs. " ^ (Pretty.output o Pretty.block o Pretty.breaks) [ - Pretty.list "(" ")" (pretty_sortcontext sortctxt'), + pretty_sortcontext sortctxt', Pretty.str "|=>", pretty_itype ty' ] @@ -888,7 +911,7 @@ | SOME dep => msg ^ ", with dependency " ^ quote dep; fun add_dp NONE = I | add_dp (SOME dep) = - debug 9 (fn _ => "adding dependency " ^ quote dep ^ " -> " ^ quote name) + debug_msg (fn _ => "adding dependency " ^ quote dep ^ " -> " ^ quote name) #> add_dep (dep, name); fun prep_def def modl = (check_prep_def modl def, modl); @@ -896,26 +919,25 @@ modl |> (if can (get_def modl) name then - debug 9 (fn _ => "asserting node " ^ quote name) + debug_msg (fn _ => "asserting node " ^ quote name) #> add_dp dep else - debug 9 (fn _ => "allocating node " ^ quote name) + debug_msg (fn _ => "allocating node " ^ quote name) #> add_def (name, Undef) #> add_dp dep - #> debug 9 (fn _ => "creating node " ^ quote name) + #> debug_msg (fn _ => "creating node " ^ quote name) #> select_generator (fn gname => "trying code generator " ^ gname ^ " for definition of " ^ quote name) name defgens - #> debug 9 (fn _ => "checking creation of node " ^ quote name) + #> debug_msg (fn _ => "checking creation of node " ^ quote name) #> check_fail msg' #-> (fn def => prep_def def) #-> (fn def => - debug 10 (fn _ => "addition of " ^ name - ^ " := " ^ (Pretty.output o pretty_def) def) - #> debug 10 (fn _ => "adding") + debug_msg (fn _ => "addition of " ^ name ^ " := " ^ (Pretty.output o pretty_def) def) + #> debug_msg (fn _ => "adding") #> add_def_incr (name, def) - #> debug 10 (fn _ => "postprocessing") + #> debug_msg (fn _ => "postprocessing") #> postprocess_def (name, def) - #> debug 10 (fn _ => "adding done") + #> debug_msg (fn _ => "adding done") )) |> pair dep end; @@ -1080,9 +1102,7 @@ val (ps', tab'') = get_path_name ps tab' in (p' :: ps', tab'') end; fun deresolv tab prefix name = - if (is_some o Int.fromString) name - then name - else let + let val (common, (_, rem)) = get_prefix (op =) (prefix, NameSpace.unpack name); val (_, SOME tab') = get_path_name common tab; val (name', _) = get_path_name rem tab'; @@ -1104,13 +1124,14 @@ List.mapPartial (seri prfx) ((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module) and seri prfx ([(name, Module modl)]) = - seri_module (map (resolver []) (imports_of module (prfx @ [name]))) + seri_module (resolver []) (map (resolver []) (imports_of module (prfx @ [name]))) (mk_name prfx name, mk_contents (prfx @ [name]) modl) | seri prfx ds = seri_defs sresolver (NameSpace.pack prfx) (map (fn (name, Def def) => (fst (mk_name prfx name), def)) ds) in - seri_module (map (resolver []) (Graph.strong_conn module |> List.concat |> rev)) + seri_module (resolver []) (imports_of module []) + (*map (resolver []) (Graph.strong_conn module |> List.concat |> rev)*) (("", name_root), (mk_contents [] module)) end; diff -r a4fe025ecd90 -r 3414c04fbc39 src/Pure/Tools/nbe.ML --- a/src/Pure/Tools/nbe.ML Thu Apr 06 16:08:22 2006 +0200 +++ b/src/Pure/Tools/nbe.ML Thu Apr 06 16:08:25 2006 +0200 @@ -41,7 +41,7 @@ fun norm_by_eval_i t thy = let val nbe_tab = NBE_Data.get thy; - val modl_old = CodegenThingol.partof (Symtab.keys nbe_tab) + val modl_old = CodegenThingol.project_module (Symtab.keys nbe_tab) (CodegenPackage.get_root_module thy); val (t', thy') = CodegenPackage.codegen_term t thy; val modl_new = CodegenPackage.get_root_module thy'; diff -r a4fe025ecd90 -r 3414c04fbc39 src/Pure/Tools/nbe_codegen.ML --- a/src/Pure/Tools/nbe_codegen.ML Thu Apr 06 16:08:22 2006 +0200 +++ b/src/Pure/Tools/nbe_codegen.ML Thu Apr 06 16:08:25 2006 +0200 @@ -150,9 +150,8 @@ | consts_of (A (t1, t2)) = consts_of t1 #> consts_of t2 | consts_of (AbsN (_, t)) = consts_of t; val consts = consts_of t []; - val the_const = AList.lookup (op =) - (consts ~~ CodegenPackage.consts_of_idfs thy consts) - #> the_default ("", dummyT); + val the_const = the o AList.lookup (op =) + (consts ~~ CodegenPackage.consts_of_idfs thy consts); fun to_term bounds (C s) = Const (the_const s) | to_term bounds (V s) = Free (s, dummyT) | to_term bounds (B i) = Bound (find_index (fn j => i = j) bounds) diff -r a4fe025ecd90 -r 3414c04fbc39 src/Pure/codegen.ML --- a/src/Pure/codegen.ML Thu Apr 06 16:08:22 2006 +0200 +++ b/src/Pure/codegen.ML Thu Apr 06 16:08:25 2006 +0200 @@ -83,6 +83,7 @@ val replace_quotes: 'b list -> 'a mixfix list -> 'b mixfix list val fillin_mixfix: ('a -> Pretty.T) -> 'a mixfix list -> 'a list -> Pretty.T val mk_deftab: theory -> deftab + val add_unfold: thm -> theory -> theory val get_node: codegr -> string -> node val add_edge: string * string -> codegr -> codegr @@ -346,7 +347,7 @@ | _ => err () end; -val unfold_attr = Thm.declaration_attribute (fn eqn => Context.map_theory +fun add_unfold eqn = let val names = term_consts (fst (Logic.dest_equals (prop_of eqn))); fun prep thy = map (fn th => @@ -356,9 +357,8 @@ then rewrite_rule [eqn] (Thm.transfer thy th) else th end) - in add_preprocessor prep end); + in add_preprocessor prep end; -val _ = Context.add_setup (add_attribute "unfold" (Scan.succeed unfold_attr)); (**** associate constants with target language code ****)