src/HOL/Tools/recfun_codegen.ML
changeset 32358 98c00ee9e786
parent 32353 0ac26087464b
child 32927 7a20fd22ba01
     1.1 --- a/src/HOL/Tools/recfun_codegen.ML	Tue Aug 11 10:05:53 2009 +0200
     1.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Tue Aug 11 10:43:43 2009 +0200
     1.3 @@ -14,6 +14,8 @@
     1.4  
     1.5  open Codegen;
     1.6  
     1.7 +val const_of = dest_Const o head_of o fst o Logic.dest_equals;
     1.8 +
     1.9  structure ModuleData = TheoryDataFun
    1.10  (
    1.11    type T = string Symtab.table;
    1.12 @@ -31,36 +33,32 @@
    1.13      |> ModuleData.map (Symtab.update (fst (Code.const_typ_eqn thy thm'), module_name))
    1.14    end;
    1.15  
    1.16 -fun retrieve_equations thy (c, T) = if c = @{const_name "op ="} then NONE else
    1.17 -  let
    1.18 -    val c' = AxClass.unoverload_const thy (c, T);
    1.19 -    val opt_name = Symtab.lookup (ModuleData.get thy) c';
    1.20 -    val raw_thms = Code.these_eqns thy c'
    1.21 -      |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE);
    1.22 -  in if null raw_thms then NONE else
    1.23 -    raw_thms
    1.24 -    |> Code_Thingol.clean_thms thy (snd (Code.const_typ_eqn thy (hd raw_thms)))
    1.25 -    |> map (rpair opt_name)
    1.26 -    |> SOME
    1.27 -  end;
    1.28 +fun avoid_value thy [thm] =
    1.29 +      let val (_, T) = Code.const_typ_eqn thy thm
    1.30 +      in if null (Term.add_tvarsT T []) orelse (null o fst o strip_type) T
    1.31 +        then [thm]
    1.32 +        else [Code_Thingol.expand_eta thy 1 thm]
    1.33 +      end
    1.34 +  | avoid_value thy thms = thms;
    1.35  
    1.36 -val dest_eqn = Logic.dest_equals;
    1.37 -val const_of = dest_Const o head_of o fst o dest_eqn;
    1.38 -
    1.39 -fun get_equations thy defs (s, T) =
    1.40 -  (case retrieve_equations thy (s, T) of
    1.41 -     NONE => ([], "")
    1.42 -   | SOME thms => 
    1.43 -       let val thms' = filter (fn (thm, _) => is_instance T
    1.44 -           (snd (const_of (prop_of thm)))) thms
    1.45 -       in if null thms' then ([], "")
    1.46 -         else (preprocess thy (map fst thms'),
    1.47 -           case snd (snd (split_last thms')) of
    1.48 -               NONE => (case get_defn thy defs s T of
    1.49 -                   NONE => Codegen.thyname_of_const thy s
    1.50 -                 | SOME ((_, (thyname, _)), _) => thyname)
    1.51 -             | SOME thyname => thyname)
    1.52 -       end);
    1.53 +fun get_equations thy defs (raw_c, T) = if raw_c = @{const_name "op ="} then ([], "") else
    1.54 +  let
    1.55 +    val c = AxClass.unoverload_const thy (raw_c, T);
    1.56 +    val raw_thms = Code.these_eqns thy c
    1.57 +      |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE)
    1.58 +      |> filter (is_instance T o snd o const_of o prop_of);
    1.59 +    val module_name = case Symtab.lookup (ModuleData.get thy) c
    1.60 +     of SOME module_name => module_name
    1.61 +      | NONE => case get_defn thy defs c T
    1.62 +         of SOME ((_, (thyname, _)), _) => thyname
    1.63 +          | NONE => Codegen.thyname_of_const thy c;
    1.64 +  in if null raw_thms then ([], "") else
    1.65 +    raw_thms
    1.66 +    |> preprocess thy
    1.67 +    |> avoid_value thy
    1.68 +    |> Code_Thingol.clean_thms thy
    1.69 +    |> rpair module_name
    1.70 +  end;
    1.71  
    1.72  fun mk_suffix thy defs (s, T) = (case get_defn thy defs s T of
    1.73    SOME (_, SOME i) => " def" ^ string_of_int i | _ => "");
    1.74 @@ -74,7 +72,7 @@
    1.75  fun add_rec_funs thy defs dep module eqs gr =
    1.76    let
    1.77      fun dest_eq t = (fst (const_of t) ^ mk_suffix thy defs (const_of t),
    1.78 -      dest_eqn (rename_term t));
    1.79 +      Logic.dest_equals (rename_term t));
    1.80      val eqs' = map dest_eq eqs;
    1.81      val (dname, _) :: _ = eqs';
    1.82      val (s, T) = const_of (hd eqs);