src/HOL/Tools/recfun_codegen.ML
changeset 18220 43cf5767f992
parent 17412 e26cb20ef0cc
child 18702 7dc7dcd63224
     1.1 --- a/src/HOL/Tools/recfun_codegen.ML	Tue Nov 22 12:42:59 2005 +0100
     1.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Tue Nov 22 12:59:25 2005 +0100
     1.3 @@ -9,6 +9,7 @@
     1.4  sig
     1.5    val add: string option -> theory attribute
     1.6    val del: theory attribute
     1.7 +  val get_rec_equations: theory -> string * typ -> (term list * term) list * typ
     1.8    val setup: (theory -> theory) list
     1.9  end;
    1.10  
    1.11 @@ -79,6 +80,19 @@
    1.12               | SOME thyname => thyname)
    1.13         end);
    1.14  
    1.15 +fun get_rec_equations thy (s, T) =
    1.16 +  Symtab.lookup (CodegenData.get thy) s
    1.17 +  |> Option.map (fn thms => 
    1.18 +       List.filter (fn (thm, _) => is_instance thy T ((snd o const_of o prop_of) thm)) thms
    1.19 +       |> del_redundant thy [])
    1.20 +  |> Option.mapPartial (fn thms => if null thms then NONE else SOME thms)
    1.21 +  |> Option.map (fn thms =>
    1.22 +       (preprocess thy (map fst thms),
    1.23 +          (snd o const_of o prop_of o fst o hd) thms))
    1.24 +  |> the_default ([], dummyT)
    1.25 +  |> apfst (map prop_of)
    1.26 +  |> apfst (map (Codegen.rename_term #> HOLogic.dest_Trueprop #> HOLogic.dest_eq #> apfst (strip_comb #> snd)))
    1.27 +
    1.28  fun mk_suffix thy defs (s, T) = (case get_defn thy defs s T of
    1.29    SOME (_, SOME i) => " def" ^ string_of_int i | _ => "");
    1.30  
    1.31 @@ -165,11 +179,14 @@
    1.32    | _ => NONE);
    1.33  
    1.34  
    1.35 -val setup =
    1.36 -  [CodegenData.init,
    1.37 -   add_codegen "recfun" recfun_codegen,
    1.38 -   add_attribute ""
    1.39 -     (   Args.del |-- Scan.succeed del
    1.40 -      || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add)];
    1.41 +val setup = [
    1.42 +  CodegenData.init,
    1.43 +  add_codegen "recfun" recfun_codegen,
    1.44 +  add_attribute ""
    1.45 +    (   Args.del |-- Scan.succeed del
    1.46 +     || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add),
    1.47 +  CodegenPackage.add_defgen
    1.48 +    ("rec", CodegenPackage.defgen_recfun get_rec_equations)
    1.49 +];
    1.50  
    1.51  end;