# HG changeset patch # User haftmann # Date 1169713971 -3600 # Node ID 24bf0e403526131f98853b213e3c27d6bc0ed05f # Parent a125f38a559a8bbbd298597a244ea493f9b60887 tuned diff -r a125f38a559a -r 24bf0e403526 src/Pure/Tools/codegen_func.ML --- a/src/Pure/Tools/codegen_func.ML Thu Jan 25 09:32:50 2007 +0100 +++ b/src/Pure/Tools/codegen_func.ML Thu Jan 25 09:32:51 2007 +0100 @@ -2,22 +2,21 @@ ID: $Id$ Author: Florian Haftmann, TU Muenchen -Handling defining equations ("func"s) for code generator framework. +Basic handling of defining equations ("func"s) for code generator framework. *) signature CODEGEN_FUNC = sig - val check_rew: thm -> thm + val assert_rew: thm -> thm val mk_rew: thm -> thm list - val check_func: thm -> (CodegenConsts.const * thm) option + val assert_func: thm -> thm val mk_func: thm -> (CodegenConsts.const * thm) list + val mk_head: thm -> CodegenConsts.const * thm val dest_func: thm -> (string * typ) * term list - val mk_head: thm -> CodegenConsts.const * thm val typ_func: thm -> typ - val legacy_mk_func: thm -> (CodegenConsts.const * thm) list + val expand_eta: int -> thm -> thm val rewrite_func: thm list -> thm -> thm - val get_prim_def_funcs: theory -> string * typ list -> thm list end; structure CodegenFunc : CODEGEN_FUNC = @@ -31,7 +30,7 @@ (* making rewrite theorems *) -fun check_rew thm = +fun assert_rew thm = let val thy = Thm.theory_of_thm thm; val (lhs, rhs) = (Logic.dest_equals o Thm.prop_of) thm; @@ -59,7 +58,7 @@ val thy = Thm.theory_of_thm thm; val thms = (#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) thy thm; in - map check_rew thms + map assert_rew thms end; @@ -75,7 +74,7 @@ val mk_head = lift_thm_thy (fn thy => fn thm => ((CodegenConsts.norm_of_typ thy o fst o dest_func) thm, thm)); -fun gen_check_func strict_functyp thm = case try dest_func thm +fun assert_func thm = case try dest_func thm of SOME (c_ty as (c, ty), args) => let val thy = Thm.theory_of_thm thm; @@ -90,35 +89,10 @@ | no_abs (t1 $ t2) = (no_abs t1; no_abs t2) | no_abs _ = (); val _ = map no_abs args; - val is_classop = (is_some o AxClass.class_of_param thy) c; - val const = CodegenConsts.norm_of_typ thy c_ty; - val ty_decl = CodegenConsts.disc_typ_of_const thy - (snd o CodegenConsts.typ_of_inst thy) const; - val string_of_typ = setmp show_sorts true (Sign.string_of_typ thy); - val error_warning = if strict_functyp - then error - else warning #> K NONE - in if Sign.typ_equiv thy (ty_decl, ty) - then SOME (const, thm) - else (if is_classop - then error_warning - else if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty) - then warning #> (K o SOME) (const, thm) - else error_warning) - ("Type\n" ^ string_of_typ ty - ^ "\nof function theorem\n" - ^ string_of_thm thm - ^ "\nis strictly less general than declared function type\n" - ^ string_of_typ ty_decl) - end + in thm end | NONE => bad_thm "Not a function equation" thm; -val check_func = gen_check_func true; -val legacy_check_func = gen_check_func false; - -fun gen_mk_func check_func = map_filter check_func o mk_rew; -val mk_func = gen_mk_func check_func; -val legacy_mk_func = gen_mk_func legacy_check_func; +val mk_func = map (mk_head o assert_func) o mk_rew; (* utilities *) @@ -155,31 +129,6 @@ fold (fn refl => fn thm => Thm.combination thm refl) vs_refl thm end; -fun get_prim_def_funcs thy c = - let - fun constrain thm0 thm = case AxClass.class_of_param thy (fst c) - of SOME _ => - let - val ty_decl = CodegenConsts.disc_typ_of_classop thy c; - val max = maxidx_of_typ ty_decl + 1; - val thm = Thm.incr_indexes max thm; - val ty = typ_func thm; - val (env, _) = Sign.typ_unify thy (ty_decl, ty) (Vartab.empty, max); - 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 Thm.instantiate (instT, []) thm end - | NONE => thm - in case CodegenConsts.find_def thy c - of SOME ((_, thm), _) => - thm - |> Thm.transfer thy - |> try (map snd o mk_func) - |> these - |> map (constrain thm) - |> map (expand_eta ~1) - | NONE => [] - end; - fun rewrite_func rewrites thm = let val rewrite = MetaSimplifier.rewrite false rewrites; diff -r a125f38a559a -r 24bf0e403526 src/Pure/Tools/codegen_funcgr.ML --- a/src/Pure/Tools/codegen_funcgr.ML Thu Jan 25 09:32:50 2007 +0100 +++ b/src/Pure/Tools/codegen_funcgr.ML Thu Jan 25 09:32:51 2007 +0100 @@ -2,7 +2,7 @@ ID: $Id$ Author: Florian Haftmann, TU Muenchen -Retrieving, normalizing and structuring code function theorems +Retrieving, normalizing and structuring defining equations in graph with explicit dependencies. *) @@ -10,14 +10,16 @@ sig type T; val make: theory -> CodegenConsts.const list -> T + val make_consts: theory -> CodegenConsts.const list -> CodegenConsts.const list * T val make_term: theory -> ((thm -> thm) -> cterm -> thm -> 'a) -> cterm -> 'a * T val funcs: T -> CodegenConsts.const -> thm list val typ: T -> CodegenConsts.const -> typ val deps: T -> CodegenConsts.const list -> CodegenConsts.const list list val all: T -> CodegenConsts.const list - val norm_varnames: theory -> thm list -> thm list + val norm_varnames: thm list -> thm list val print_codethms: theory -> CodegenConsts.const list -> unit structure Constgraph : GRAPH + val timing: bool ref end; structure CodegenFuncgr: CODEGEN_FUNCGR = @@ -48,6 +50,26 @@ val _ = Context.add_setup Funcgr.init; +(** retrieval **) + +fun funcs funcgr = + these o Option.map snd o try (Constgraph.get_node funcgr); + +fun typ funcgr = + fst o Constgraph.get_node funcgr; + +fun deps funcgr cs = + let + val conn = Constgraph.strong_conn funcgr; + val order = rev conn; + in + (map o filter) (member (op =) (Constgraph.all_succs funcgr cs)) order + |> filter_out null + end; + +fun all funcgr = Constgraph.keys funcgr; + + (** theorem purification **) fun norm_args thms = @@ -104,7 +126,7 @@ val t' = Term.map_abs_vars CodegenNames.purify_var t; in Thm.rename_boundvars t t' thm end; -fun norm_varnames thy thms = +fun norm_varnames thms = let fun burrow_thms f [] = [] | burrow_thms f thms = @@ -122,52 +144,28 @@ end; - -(** retrieval **) - -fun funcs funcgr = - these o Option.map snd o try (Constgraph.get_node funcgr); - -fun typ funcgr = - fst o Constgraph.get_node funcgr; +(** generic combinators **) -fun deps funcgr cs = - let - val conn = Constgraph.strong_conn funcgr; - val order = rev conn; - in - (map o filter) (member (op =) (Constgraph.all_succs funcgr cs)) order - |> filter_out null - end; - -fun all funcgr = Constgraph.keys funcgr; - -local +fun fold_consts f thms = + thms + |> maps (op :: o swap o apfst (snd o strip_comb) o Logic.dest_equals o Drule.plain_prop_of) + |> (fold o fold_aterms) (fn Const c => f c | _ => I); -fun add_things_of thy f (c, thms) = - (fold o fold_aterms) - (fn Const c_ty => let - val c' = CodegenConsts.norm_of_typ thy c_ty - in if is_some c andalso CodegenConsts.eq_const (the c, c') then I - else f (c', c_ty) end - | _ => I) (maps (op :: o swap o apfst (snd o strip_comb) - o Logic.dest_equals o Drule.plain_prop_of) thms) +fun consts_of (const, []) = [] + | consts_of (const, thms as thm :: _) = + let + val thy = Thm.theory_of_thm thm; + val is_refl = curry CodegenConsts.eq_const const; + fun the_const c = case try (CodegenConsts.norm_of_typ thy) c + of SOME const => if is_refl const then I else insert CodegenConsts.eq_const const + | NONE => I + in fold_consts the_const thms [] end; -fun rhs_of thy (c, thms) = - Consttab.empty - |> add_things_of thy (Consttab.update o rpair () o fst) (c, thms) - |> Consttab.keys; - -fun rhs_of' thy (c, thms) = - add_things_of thy (cons o snd) (c, thms) []; - -fun insts_of thy funcgr (c, ty) = +fun insts_of thy algebra c ty_decl ty = let + val tys_decl = Sign.const_typargs thy (c, ty_decl); val tys = Sign.const_typargs thy (c, ty); - val c' = CodegenConsts.norm thy (c, tys); - val ty_decl = CodegenConsts.disc_typ_of_const thy - (fst o Constgraph.get_node funcgr o CodegenConsts.norm thy) (c, tys); - val tys_decl = Sign.const_typargs thy (c, ty_decl); + fun classrel (x, _) _ = x; fun constructor tyco xs class = (tyco, class) :: maps (maps fst) xs; fun variable (TVar (_, sort)) = map (pair []) sort @@ -177,76 +175,24 @@ | mk_inst (Type (tyco1, tys1)) (Type (tyco2, tys2)) = if tyco1 <> tyco2 then error "bad instance" else fold2 mk_inst tys1 tys2; - val pp = Sign.pp thy; - val algebra = Sign.classes_of thy; - fun classrel (x, _) _ = x; fun of_sort_deriv (ty, sort) = - Sorts.of_sort_derivation pp algebra + Sorts.of_sort_derivation (Sign.pp thy) algebra { classrel = classrel, constructor = constructor, variable = variable } (ty, sort) in flat (maps of_sort_deriv (fold2 mk_inst tys tys_decl [])) end; -exception MISSING_INSTANCE of string * string; (*FIXME provide reasonable error tracking*) -fun all_classops thy tyco class = - if can (Sign.arity_sorts thy tyco) [class] - then - try (AxClass.params_of_class thy) class - |> Option.map snd - |> these - |> map (fn (c, _) => (c, CodegenConsts.disc_typ_of_classop thy (c, [Type (tyco, [])]))) - |> map (CodegenConsts.norm_of_typ thy) - else raise MISSING_INSTANCE (tyco, class); +(** graph algorithm **) -fun instdefs_of thy insts = - let - val thy_classes = (#classes o Sorts.rep_algebra o Sign.classes_of) thy; - in - Symtab.empty - |> fold (fn (tyco, class) => - Symtab.map_default (tyco, []) (insert (op =) class)) insts - |> (fn tab => Symtab.fold (fn (tyco, classes) => append (maps (all_classops thy tyco) - (Graph.all_succs thy_classes classes))) tab []) - end; +val timing = ref false; -fun insts_of_thms thy funcgr (c, thms) = - let - val insts = add_things_of thy (fn (_, c_ty) => fold (insert (op =)) - (insts_of thy funcgr c_ty)) (SOME c, thms) []; - in - instdefs_of thy insts handle MISSING_INSTANCE (tyco, class) => - error ("No such instance: " ^ quote tyco ^ ", " ^ quote class - ^ "\nin function theorems\n" - ^ (cat_lines o map string_of_thm) thms) - end; +local -fun ensure_const thy funcgr c auxgr = - if can (Constgraph.get_node funcgr) c - then (NONE, auxgr) - else if can (Constgraph.get_node auxgr) c - then (SOME c, auxgr) - else if is_some (CodegenData.get_datatype_of_constr thy c) then - auxgr - |> Constgraph.new_node (c, []) - |> pair (SOME c) - else let - val thms = norm_varnames thy (CodegenData.these_funcs thy c); - val rhs = rhs_of thy (SOME c, thms); - in - auxgr - |> Constgraph.new_node (c, thms) - |> fold_map (ensure_const thy funcgr) rhs - |-> (fn rhs' => fold (fn SOME c' => Constgraph.add_edge (c, c') - | NONE => I) rhs') - |> pair (SOME c) - end; +exception INVALID of CodegenConsts.const list * string; -exception INVALID of CodegenConsts.const list * string; (*FIXME provide reasonable error tracking*) - -(*FIXME: clarify algorithm*) -fun specialize_typs' thy funcgr eqss = +fun specialize_typs' thy funcgr funcss = let fun max xs = fold (curry Int.max) xs 0; fun incr_indices (c, thms) maxidx = @@ -254,11 +200,14 @@ val thms' = map (Thm.incr_indexes (maxidx + 1)) thms; val maxidx' = max (maxidx :: map Thm.maxidx_of thms'); in ((c, thms'), maxidx') end; - val (eqss', maxidx) = - fold_map incr_indices eqss 0; + val (funcss', maxidx) = + fold_map incr_indices funcss 0; + fun typ_of_const (c, ty) = case try (CodegenConsts.norm_of_typ thy) (c, ty) + of SOME const => Option.map fst (try (Constgraph.get_node funcgr) const) + | NONE => NONE; fun unify_const (c, ty) (env, maxidx) = - case try (Constgraph.get_node funcgr) (CodegenConsts.norm_of_typ thy (c, ty)) - of SOME (ty_decl, _) => let + case typ_of_const (c, ty) + of SOME ty_decl => let val ty_decl' = Logic.incr_tvar (maxidx + 1) ty_decl; val maxidx' = max [maxidx, Term.maxidx_of_typ ty_decl']; in Type.unify (Sign.tsig_of thy) (ty_decl', ty) (env, maxidx') @@ -267,7 +216,7 @@ ^ (Sign.string_of_typ thy o Envir.norm_type env) ty ^ ",\nfor constant " ^ quote c ^ "\nin function theorems\n" - ^ (cat_lines o maps (map (Sign.string_of_term thy o map_types (Envir.norm_type env) o Thm.prop_of) o snd)) eqss'))) + ^ (cat_lines o maps (map (Sign.string_of_term thy o map_types (Envir.norm_type env) o Thm.prop_of) o snd)) funcss'))) end | NONE => (env, maxidx); fun apply_unifier unif (c, []) = (c, []) @@ -296,39 +245,126 @@ ^ (cat_lines o map string_of_thm) thms)) in (c, thms') end; val (unif, _) = - fold (fn (c, thms) => fold unify_const (rhs_of' thy (c, thms))) - eqss' (Vartab.empty, maxidx); - val eqss'' = map (apply_unifier unif) eqss'; - in eqss'' end; + fold (fn (_, thms) => fold unify_const (fold_consts (insert (op =)) thms [])) + funcss' (Vartab.empty, maxidx); + val funcss'' = map (apply_unifier unif) funcss'; + in funcss'' end; fun specialize_typs thy funcgr = (map o apfst) SOME #> specialize_typs' thy funcgr #> (map o apfst) the; -fun merge_eqsyss thy raw_eqss funcgr = +fun classop_const thy algebra class classop tyco = + let + val sorts = Sorts.mg_domain algebra tyco [class] + val (var, _) = try (AxClass.params_of_class thy) class |> the_default ("'a", []); + val vs = Name.names (Name.declare var Name.context) "'a" sorts; + val arity_typ = Type (tyco, map TFree vs); + in (classop, [arity_typ]) end; + +fun instances_of thy algebra insts = + let + val thy_classes = (#classes o Sorts.rep_algebra o Sign.classes_of) thy; + fun all_classops tyco class = + try (AxClass.params_of_class thy) class + |> Option.map snd + |> these + |> map (fn (c, _) => classop_const thy algebra class c tyco) + |> map (CodegenConsts.norm thy) + in + Symtab.empty + |> fold (fn (tyco, class) => + Symtab.map_default (tyco, []) (insert (op =) class)) insts + |> (fn tab => Symtab.fold (fn (tyco, classes) => append (maps (all_classops tyco) + (Graph.all_succs thy_classes classes))) tab []) + end; + +fun instances_of_consts thy algebra funcgr consts = let - val eqss = specialize_typs thy funcgr raw_eqss; - val tys = map (CodegenData.typ_funcs thy) eqss; - val rhss = map (rhs_of thy o apfst SOME) eqss; + fun inst (const as (c, ty)) = case try (CodegenConsts.norm_of_typ thy) const + of SOME const => insts_of thy algebra c (fst (Constgraph.get_node funcgr const)) ty + | NONE => []; + in + [] + |> fold (fold (insert (op =)) o inst) consts + |> instances_of thy algebra + end; + +fun ensure_const' thy algebra funcgr const auxgr = + if can (Constgraph.get_node funcgr) const + then (NONE, auxgr) + else if can (Constgraph.get_node auxgr) const + then (SOME const, auxgr) + else if is_some (CodegenData.get_datatype_of_constr thy const) then + auxgr + |> Constgraph.new_node (const, []) + |> pair (SOME const) + else let + val thms = norm_varnames (CodegenData.these_funcs thy const); + val rhs = consts_of (const, thms); + in + auxgr + |> Constgraph.new_node (const, thms) + |> fold_map (ensure_const thy algebra funcgr) rhs + |-> (fn rhs' => fold (fn SOME const' => Constgraph.add_edge (const, const') + | NONE => I) rhs') + |> pair (SOME const) + end +and ensure_const thy algebra funcgr const = + let + val timeap = if !timing + then Output.timeap_msg ("time for " ^ CodegenConsts.string_of_const thy const) + else I; + in timeap (ensure_const' thy algebra funcgr const) end; + +fun merge_funcss thy algebra raw_funcss funcgr = + let + val funcss = specialize_typs thy funcgr raw_funcss; + fun default_typ (const as (c, tys)) = case CodegenData.tap_typ thy const + of SOME ty => ty + | NONE => let + val ty = Sign.the_const_type thy c + in case AxClass.class_of_param thy c + of SOME class => let + val inst = case tys + of [Type (tyco, _)] => classop_const thy algebra class c tyco + |> snd + |> the_single + |> Logic.varifyT + | _ => TVar (("'a", 0), [class]); + in Term.map_type_tvar (K inst) ty end + | NONE => ty + end; + fun add_funcs (const, thms as thm :: _) = + Constgraph.new_node (const, (CodegenFunc.typ_func thm, thms)) + | add_funcs (const, []) = + Constgraph.new_node (const, (default_typ const, [])); + val _ = writeln ("constants " ^ (commas o map (CodegenConsts.string_of_const thy o fst)) funcss); + val _ = writeln ("funcs " ^ (cat_lines o maps (map string_of_thm o snd)) funcss); + fun add_deps (funcs as (const, thms)) funcgr = + let + val deps = consts_of funcs; + val _ = writeln ("constant " ^ CodegenConsts.string_of_const thy const); + val insts = instances_of_consts thy algebra funcgr + (fold_consts (insert (op =)) thms []); + in + funcgr + |> ensure_consts' thy algebra insts + |> fold (curry Constgraph.add_edge const) deps + |> fold (curry Constgraph.add_edge const) insts + end; in funcgr - |> fold2 (fn (c, thms) => fn ty => Constgraph.new_node (c, (ty, thms))) eqss tys - |> `(fn funcgr => map (insts_of_thms thy funcgr) eqss) - |-> (fn rhs_insts => fold2 (fn (c, _) => fn rhs_inst => - ensure_consts thy rhs_inst #> fold (curry Constgraph.add_edge c) rhs_inst) eqss rhs_insts) - |> fold2 (fn (c, _) => fn rhs => fold (curry Constgraph.add_edge c) rhs) eqss rhss + |> fold add_funcs funcss + |> fold add_deps funcss end -and merge_new_eqsyss thy raw_eqss funcgr = - if exists (member CodegenConsts.eq_const (Constgraph.keys funcgr)) (map fst raw_eqss) - then funcgr - else merge_eqsyss thy raw_eqss funcgr -and ensure_consts thy cs funcgr = - fold (snd oo ensure_const thy funcgr) cs Constgraph.empty - |> (fn auxgr => fold (merge_new_eqsyss thy) +and ensure_consts' thy algebra cs funcgr = + fold (snd oo ensure_const thy algebra funcgr) cs Constgraph.empty + |> (fn auxgr => fold (merge_funcss thy algebra) (map (AList.make (Constgraph.get_node auxgr)) (rev (Constgraph.strong_conn auxgr))) funcgr) - handle INVALID (cs', msg) => raise INVALID (cs @ cs', msg); + handle INVALID (cs', msg) => raise INVALID (fold (insert CodegenConsts.eq_const) cs' cs, msg); fun drop_classes thy tfrees thm = let @@ -344,15 +380,31 @@ |> Tactic.rule_by_tactic ((REPEAT o CHANGED o ALLGOALS o Tactic.resolve_tac) (AxClass.class_intros thy)) end; +fun ensure_consts thy consts funcgr = + let + val algebra = CodegenData.coregular_algebra thy + in ensure_consts' thy algebra consts funcgr + handle INVALID (cs', msg) => error (msg ^ ",\nwhile preprocessing equations for constant(s) " + ^ commas (map (CodegenConsts.string_of_const thy) cs')) + end; + in -val ensure_consts = (fn thy => fn cs => fn funcgr => ensure_consts thy - cs funcgr handle INVALID (cs', msg) => error (msg ^ ",\nwhile preprocessing equations for constant(s) " - ^ commas (map (CodegenConsts.string_of_const thy) cs'))); + +(** graph retrieval **) fun make thy consts = Funcgr.change thy (ensure_consts thy consts); +fun make_consts thy consts = + let + val algebra = CodegenData.coregular_algebra thy; + fun try_const const funcgr = + (SOME const, ensure_consts' thy algebra [const] funcgr) + handle INVALID (cs', msg) => (NONE, funcgr); + val (consts', funcgr) = Funcgr.change_yield thy (fold_map try_const consts); + in (map_filter I consts', funcgr) end; + fun make_term thy f ct = let val _ = Sign.no_vars (Sign.pp thy) (Thm.term_of ct); @@ -376,16 +428,16 @@ val ct'' = Drule.dest_equals_rhs (Thm.cprop_of thm6); val cs = fold_aterms (fn Const c => cons c | _ => I) (Thm.term_of ct'') []; val drop = drop_classes thy tfrees; - val instdefs = instdefs_of thy (fold (fold (insert (op =)) o insts_of thy funcgr) cs []) - handle MISSING_INSTANCE (tyco, class) => - error ("No such instance: " ^ quote tyco ^ ", " ^ quote class - ^ "\nwhile prcoessing term\n" - ^ string_of_cterm ct) + val algebra = CodegenData.coregular_algebra thy; + val instdefs = instances_of_consts thy algebra funcgr cs; val funcgr' = ensure_consts thy instdefs funcgr; in (f drop ct'' thm5, Funcgr.change thy (K funcgr')) end; end; (*local*) + +(** diagnostics **) + fun print_funcgr thy funcgr = AList.make (snd o Constgraph.get_node funcgr) (Constgraph.keys funcgr) |> (map o apfst) (CodegenConsts.string_of_const thy) @@ -405,7 +457,7 @@ print_codethms thy (map (CodegenConsts.read_const thy) cs); -(** Isar **) +(** Isar setup **) structure P = OuterParse; diff -r a125f38a559a -r 24bf0e403526 src/Pure/Tools/codegen_names.ML --- a/src/Pure/Tools/codegen_names.ML Thu Jan 25 09:32:50 2007 +0100 +++ b/src/Pure/Tools/codegen_names.ML Thu Jan 25 09:32:51 2007 +0100 @@ -261,7 +261,7 @@ | NONE => (case CodegenData.get_datatype_of_constr thy const of SOME dtco => SOME (thyname_of_tyco thy dtco) | NONE => (case CodegenConsts.find_def thy const - of SOME ((thyname, _), _) => SOME thyname + of SOME (thyname, _) => SOME thyname | NONE => NONE)); fun const_policy thy (c, tys) = diff -r a125f38a559a -r 24bf0e403526 src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Thu Jan 25 09:32:50 2007 +0100 +++ b/src/Pure/Tools/codegen_package.ML Thu Jan 25 09:32:51 2007 +0100 @@ -112,9 +112,9 @@ fun ensure_def thy = CodegenThingol.ensure_def (CodegenNames.labelled_name thy); -fun ensure_def_class thy (algbr as ((proj_sort, _), _)) funcgr strct class trns = +fun ensure_def_class thy (algbr as ((_, algebra), _)) funcgr strct class trns = let - val superclasses = (proj_sort o Sign.super_classes thy) class; + val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class; val (v, cs) = AxClass.params_of_class thy class; val class' = CodegenNames.class thy class; val classrels' = map (curry (CodegenNames.classrel thy) class) superclasses; @@ -135,7 +135,7 @@ and ensure_def_classrel thy algbr funcgr strct (subclass, superclass) trns = trns |> ensure_def_class thy algbr funcgr strct subclass - |-> (fn _ => pair (CodegenNames.classrel thy (subclass, superclass))) + |>> (fn _ => CodegenNames.classrel thy (subclass, superclass)) and ensure_def_tyco thy algbr funcgr strct tyco trns = let fun defgen_datatype trns = @@ -164,18 +164,18 @@ and exprgen_tyvar_sort thy (algbr as ((proj_sort, _), _)) funcgr strct (v, sort) trns = trns |> fold_map (ensure_def_class thy algbr funcgr strct) (proj_sort sort) - |-> (fn sort => pair (unprefix "'" v, sort)) + |>> (fn sort => (unprefix "'" v, sort)) and exprgen_type thy algbr funcgr strct (TVar _) trns = error "TVar encountered in typ during code generation" | exprgen_type thy algbr funcgr strct (TFree vs) trns = trns |> exprgen_tyvar_sort thy algbr funcgr strct vs - |-> (fn (v, sort) => pair (ITyVar v)) + |>> (fn (v, sort) => ITyVar v) | exprgen_type thy algbr funcgr strct (Type ("fun", [t1, t2])) trns = trns |> exprgen_type thy algbr funcgr strct t1 ||>> exprgen_type thy algbr funcgr strct t2 - |-> (fn (t1', t2') => pair (t1' `-> t2')) + |>> (fn (t1', t2') => t1' `-> t2') | exprgen_type thy algbr funcgr strct (Type (tyco, tys)) trns = case get_abstype thy (tyco, tys) of SOME ty => @@ -185,7 +185,7 @@ trns |> ensure_def_tyco thy algbr funcgr strct tyco ||>> fold_map (exprgen_type thy algbr funcgr strct) tys - |-> (fn (tyco, tys) => pair (tyco `%% tys)); + |>> (fn (tyco, tys) => tyco `%% tys); exception CONSTRAIN of (string * typ) * typ; val timing = ref false; @@ -213,11 +213,11 @@ trns |> ensure_def_inst thy algbr funcgr strct inst ||>> (fold_map o fold_map) mk_dict yss - |-> (fn (inst, dss) => pair (DictConst (inst, dss))) + |>> (fn (inst, dss) => DictConst (inst, dss)) | mk_dict (Local (classrels, (v, (k, sort)))) trns = trns |> fold_map (ensure_def_classrel thy algbr funcgr strct) classrels - |-> (fn classrels => pair (DictVar (classrels, (unprefix "'" v, (k, length sort))))) + |>> (fn classrels => DictVar (classrels, (unprefix "'" v, (k, length sort)))) in trns |> fold_map mk_dict typargs @@ -235,40 +235,37 @@ trns |> fold_map (exprgen_dicts thy algbr funcgr strct) insts end -and ensure_def_inst thy (algbr as ((proj_sort, _), _)) funcgr strct (class, tyco) trns = +and ensure_def_inst thy (algbr as ((_, algebra), _)) funcgr strct (class, tyco) trns = let - val (vs, classop_defs) = ((apsnd o map) Const o CodegenConsts.instance_dict thy) - (class, tyco); - val classops = (map (CodegenConsts.norm_of_typ thy) o snd - o AxClass.params_of_class thy) class; - val arity_typ = Type (tyco, (map TFree vs)); - val superclasses = (proj_sort o Sign.super_classes thy) class + val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class; + val (var, classops) = try (AxClass.params_of_class thy) class |> the_default ("'a", []) + val vs = Name.names (Name.declare var Name.context) "'a" (Sorts.mg_domain algebra tyco [class]); + val arity_typ = Type (tyco, map TFree vs); fun gen_superarity superclass trns = trns |> ensure_def_class thy algbr funcgr strct superclass ||>> ensure_def_classrel thy algbr funcgr strct (class, superclass) ||>> exprgen_dicts thy algbr funcgr strct (arity_typ, [superclass]) - |-> (fn ((superclass, classrel), [DictConst (inst, dss)]) => - pair (superclass, (classrel, (inst, dss)))); - fun gen_classop_def (classop, t) trns = + |>> (fn ((superclass, classrel), [DictConst (inst, dss)]) => + (superclass, (classrel, (inst, dss)))); + fun gen_classop_def (classop as (c, ty)) trns = trns - |> ensure_def_const thy algbr funcgr strct classop - ||>> exprgen_term thy algbr funcgr strct t; + |> ensure_def_const thy algbr funcgr strct (CodegenConsts.norm_of_typ thy classop) + ||>> exprgen_term thy algbr funcgr strct (Const (c, map_type_tfree (K arity_typ) ty)); fun defgen_inst trns = trns |> ensure_def_class thy algbr funcgr strct class ||>> ensure_def_tyco thy algbr funcgr strct tyco ||>> fold_map (exprgen_tyvar_sort thy algbr funcgr strct) vs ||>> fold_map gen_superarity superclasses - ||>> fold_map gen_classop_def (classops ~~ classop_defs) + ||>> fold_map gen_classop_def classops |-> (fn ((((class, tyco), arity), superarities), classops) => succeed (CodegenThingol.Classinst ((class, (tyco, arity)), (superarities, classops)))); val inst = CodegenNames.instance thy (class, tyco); in trns |> tracing (fn _ => "generating instance " ^ quote class ^ " / " ^ quote tyco) - |> ensure_def thy defgen_inst true - ("generating instance " ^ quote class ^ " / " ^ quote tyco) inst + |> ensure_def thy defgen_inst true ("generating instance " ^ quote class ^ " / " ^ quote tyco) inst |> pair inst end and ensure_def_const thy (algbr as (_, consts)) funcgr strct (c_tys as (c, tys)) trns = @@ -334,7 +331,7 @@ | exprgen_term thy algbr funcgr strct (Free (v, ty)) trns = trns |> exprgen_type thy algbr funcgr strct ty - |-> (fn _ => pair (IVar v)) + |>> (fn _ => IVar v) | exprgen_term thy algbr funcgr strct (Abs (raw_v, ty, raw_t)) trns = let val (v, t) = Syntax.variant_abs (raw_v, ty, raw_t); @@ -342,27 +339,25 @@ trns |> exprgen_type thy algbr funcgr strct ty ||>> exprgen_term thy algbr funcgr strct t - |-> (fn (ty, t) => pair ((v, ty) `|-> t)) + |>> (fn (ty, t) => (v, ty) `|-> t) end | exprgen_term thy algbr funcgr strct (t as _ $ _) trns = case strip_comb t of (Const (c, ty), ts) => trns |> select_appgen thy algbr funcgr strct ((c, ty), ts) - |-> (fn t => pair t) | (t', ts) => trns |> exprgen_term thy algbr funcgr strct t' ||>> fold_map (exprgen_term thy algbr funcgr strct) ts - |-> (fn (t, ts) => pair (t `$$ ts)) + |>> (fn (t, ts) => t `$$ ts) and appgen_default thy algbr funcgr strct ((c, ty), ts) trns = trns |> ensure_def_const thy algbr funcgr strct (CodegenConsts.norm_of_typ thy (c, ty)) ||>> exprgen_type thy algbr funcgr strct ty ||>> exprgen_dict_parms thy algbr funcgr strct (c, ty) ||>> fold_map (exprgen_term thy algbr funcgr strct) ts - |-> (fn (((c, ty), iss), ts) => - pair (IConst (c, (iss, ty)) `$$ ts)) + |>> (fn (((c, ty), iss), ts) => IConst (c, (iss, ty)) `$$ ts) and select_appgen thy algbr funcgr strct ((c, ty), ts) trns = case Symtab.lookup (fst (CodegenPackageData.get thy)) c of SOME (i, (appgen, _)) => @@ -377,13 +372,13 @@ trns |> fold_map (exprgen_type thy algbr funcgr strct) tys ||>> appgen thy algbr funcgr strct ((c, ty), ts @ map Free vs) - |-> (fn (tys, t) => pair (map2 (fn (v, _) => pair v) vs tys `|--> t)) + |>> (fn (tys, t) => map2 (fn (v, _) => pair v) vs tys `|--> t) end else if length ts > i then trns |> appgen thy algbr funcgr strct ((c, ty), Library.take (i, ts)) ||>> fold_map (exprgen_term thy algbr funcgr strct) (Library.drop (i, ts)) - |-> (fn (t, ts) => pair (t `$$ ts)) + |>> (fn (t, ts) => t `$$ ts) else trns |> appgen thy algbr funcgr strct ((c, ty), ts) @@ -401,6 +396,12 @@ ^ Sign.string_of_typ thy ty ^ "\noccurs with type\n" ^ Sign.string_of_typ thy ty_decl); + +fun perhaps_def_const thy algbr funcgr strct c trns = + case try (ensure_def_const thy algbr funcgr strct c) trns + of SOME (c, trns) => (SOME c, trns) + | NONE => (NONE, trns); + fun exprgen_term' thy algbr funcgr strct t trns = exprgen_term thy algbr funcgr strct t trns handle CONSTRAIN ((c, ty), ty_decl) => error ("In term " ^ (quote o Sign.string_of_term thy) t @@ -427,7 +428,7 @@ of SOME i => trns |> exprgen_type thy algbr funcgr strct ty - |-> (fn _ => pair (IChar (chr i))) + |>> (fn _ => IChar (chr i)) | NONE => trns |> appgen_default thy algbr funcgr strct app; @@ -446,7 +447,7 @@ |> exprgen_term thy algbr funcgr strct st ||>> exprgen_type thy algbr funcgr strct sty ||>> fold_map clausegen ds - |-> (fn ((se, sty), ds) => pair (ICase ((se, sty), ds))) + |>> (fn ((se, sty), ds) => ICase ((se, sty), ds)) end; fun appgen_let thy algbr funcgr strct (app as (_, [st, ct])) trns = @@ -554,20 +555,7 @@ (* generic generation combinators *) -fun operational_algebra thy = - let - fun add_iff_operational class classes = - if (not o null o these o Option.map #params o try (AxClass.get_definition thy)) class - orelse (length o gen_inter (op =)) - ((Sign.certify_sort thy o Sign.super_classes thy) class, classes) >= 2 - then class :: classes - else classes; - val operational_classes = fold add_iff_operational (Sign.all_classes thy) []; - in - Sorts.subalgebra (Sign.pp thy) (member (op =) operational_classes) (Sign.classes_of thy) - end; - -fun generate thy funcgr targets init gen it = +fun generate thy funcgr targets gen it = let val cs = map_filter (Consttab.lookup ((snd o snd o CodegenPackageData.get) thy)) (CodegenFuncgr.all funcgr); @@ -577,9 +565,9 @@ |> fold (fn c => Consts.declare qnaming ((CodegenNames.const thy c, CodegenFuncgr.typ funcgr' c), true)) (CodegenFuncgr.all funcgr'); - val algbr = (operational_algebra thy, consttab); + val algbr = (CodegenData.operational_algebra thy, consttab); in - Code.change_yield thy (CodegenThingol.start_transact init (gen thy algbr funcgr' + Code.change_yield thy (CodegenThingol.start_transact (gen thy algbr funcgr' (true, targets) it)) |> fst end; @@ -589,7 +577,7 @@ val ct = Thm.cterm_of thy t; val (ct', funcgr) = CodegenFuncgr.make_term thy (K K) ct; val t' = Thm.term_of ct'; - in generate thy funcgr (SOME []) NONE exprgen_term' t' end; + in generate thy funcgr (SOME []) exprgen_term' t' end; fun eval_term thy (ref_spec, t) = let @@ -617,18 +605,17 @@ | SOME thyname => filter (is_const thyname) consts end; -fun filter_generatable thy consts = +fun filter_generatable thy targets consts = let - fun generatable const = - case try (CodegenFuncgr.make thy) [const] - of SOME funcgr => can - (generate thy funcgr NONE NONE (fold_map oooo ensure_def_const')) [const] - | NONE => false; - in filter generatable consts end; + val (consts', funcgr) = CodegenFuncgr.make_consts thy consts; + val consts'' = generate thy funcgr targets (fold_map oooo perhaps_def_const) consts'; + val consts''' = map_filter (fn (const, SOME _) => SOME const | (_, NONE) => NONE) + (consts' ~~ consts''); + in consts''' end; -fun read_constspec thy "*" = filter_generatable thy (consts_of thy NONE) - | read_constspec thy s = if String.isSuffix ".*" s - then filter_generatable thy (consts_of thy (SOME (unsuffix ".*" s))) +fun read_constspec thy targets "*" = filter_generatable thy targets (consts_of thy NONE) + | read_constspec thy targets s = if String.isSuffix ".*" s + then filter_generatable thy targets (consts_of thy (SOME (unsuffix ".*" s))) else [CodegenConsts.read_const thy s]; @@ -641,16 +628,16 @@ fun code raw_cs seris thy = let - val cs = maps (read_constspec thy) raw_cs; - (*FIXME: assert serializer*) val seris' = map (fn (target, args as _ :: _) => (target, SOME (CodegenSerializer.get_serializer thy target args)) | (target, []) => (CodegenSerializer.assert_serializer thy target, NONE)) seris; + val targets = case map fst seris' of [] => NONE | xs => SOME xs; + val cs = maps (read_constspec thy targets) raw_cs; fun generate' thy = case cs of [] => [] | _ => - generate thy (CodegenFuncgr.make thy cs) (case map fst seris' of [] => NONE | xs => SOME xs) - NONE (fold_map oooo ensure_def_const') cs; + generate thy (CodegenFuncgr.make thy cs) targets + (fold_map oooo ensure_def_const') cs; fun serialize' [] code seri = seri NONE code | serialize' cs code seri = diff -r a125f38a559a -r 24bf0e403526 src/Pure/Tools/codegen_thingol.ML --- a/src/Pure/Tools/codegen_thingol.ML Thu Jan 25 09:32:50 2007 +0100 +++ b/src/Pure/Tools/codegen_thingol.ML Thu Jan 25 09:32:51 2007 +0100 @@ -82,7 +82,7 @@ val succeed: 'a -> transact -> 'a * code; val fail: string -> transact -> 'a * code; val message: string -> (transact -> 'a) -> transact -> 'a; - val start_transact: string option -> (transact -> 'a * transact) -> code -> 'a * code; + val start_transact: (transact -> 'a * transact) -> code -> 'a * code; val trace: bool ref; val tracing: ('a -> string) -> 'a -> 'a; @@ -344,7 +344,7 @@ | check_prep_def code (d as Datatype _) = d | check_prep_def code (Datatypecons dtco) = - error "Attempted to add bare datatype constructor" + error "Attempted to add bare term constructor" | check_prep_def code (d as Class _) = d | check_prep_def code (Classop _) = @@ -438,16 +438,14 @@ f trns handle FAIL msgs => raise FAIL (msg :: msgs); -fun start_transact init f code = +fun start_transact f code = let fun handle_fail f x = (f x handle FAIL msgs => (error o cat_lines) ("Code generation failed, while:" :: msgs)) in - code - |> (if is_some init then ensure_bot (the init) else I) - |> pair init + (NONE, code) |> handle_fail f |-> (fn x => fn (_, code) => (x, code)) end;