src/Pure/Tools/codegen_func.ML
author haftmann
Tue Mar 20 08:27:20 2007 +0100 (2007-03-20)
changeset 22475 bd3378255cc8
parent 22462 2a93fb199302
child 22484 25dfebd7b4c8
permissions -rw-r--r--
adjusted definition of defining equation
     1 (*  Title:      Pure/Tools/codegen_func.ML
     2     ID:         $Id$
     3     Author:     Florian Haftmann, TU Muenchen
     4 
     5 Basic handling of defining equations ("func"s) for code generator framework.
     6 *)
     7 
     8 signature CODEGEN_FUNC =
     9 sig
    10   val assert_rew: thm -> thm
    11   val mk_rew: thm -> thm list
    12   val assert_func: thm -> thm
    13   val mk_func: thm -> (CodegenConsts.const * thm) list
    14   val mk_head: thm -> CodegenConsts.const * thm
    15   val dest_func: thm -> (string * typ) * term list
    16   val typ_func: thm -> typ
    17 
    18   val inst_thm: sort Vartab.table -> thm -> thm
    19   val expand_eta: int -> thm -> thm
    20   val rewrite_func: thm list -> thm -> thm
    21   val norm_args: thm list -> thm list 
    22   val norm_varnames: (string -> string) -> (string -> string) -> thm list -> thm list 
    23 end;
    24 
    25 structure CodegenFunc : CODEGEN_FUNC =
    26 struct
    27 
    28 fun lift_thm_thy f thm = f (Thm.theory_of_thm thm) thm;
    29 
    30 fun bad_thm msg thm =
    31   error (msg ^ ": " ^ string_of_thm thm);
    32 
    33 
    34 (* making rewrite theorems *)
    35 
    36 fun assert_rew thm =
    37   let
    38     val thy = Thm.theory_of_thm thm;
    39     val (lhs, rhs) = (Logic.dest_equals o Thm.prop_of) thm;
    40     fun vars_of t = fold_aterms
    41      (fn Var (v, _) => insert (op =) v
    42        | Free _ => bad_thm "Illegal free variable in rewrite theorem" thm
    43        | _ => I) t [];
    44     fun tvars_of t = fold_term_types
    45      (fn _ => fold_atyps (fn TVar (v, _) => insert (op =) v
    46                           | TFree _ => bad_thm "Illegal free type variable in rewrite theorem" thm)) t [];
    47     val lhs_vs = vars_of lhs;
    48     val rhs_vs = vars_of rhs;
    49     val lhs_tvs = tvars_of lhs;
    50     val rhs_tvs = tvars_of lhs;
    51     val _ = if null (subtract (op =) lhs_vs rhs_vs)
    52       then ()
    53       else bad_thm "Free variables on right hand side of rewrite theorems" thm
    54     val _ = if null (subtract (op =) lhs_tvs rhs_tvs)
    55       then ()
    56       else bad_thm "Free type variables on right hand side of rewrite theorems" thm
    57   in thm end;
    58 
    59 fun mk_rew thm =
    60   let
    61     val thy = Thm.theory_of_thm thm;
    62     val thms = (#mk o #mk_rews o snd o MetaSimplifier.rep_ss o Simplifier.simpset_of) thy thm;
    63   in
    64     map assert_rew thms
    65   end;
    66 
    67 
    68 (* making defining equations *)
    69 
    70 val typ_func = lift_thm_thy (fn thy => snd o dest_Const o fst o strip_comb
    71   o fst o Logic.dest_equals o ObjectLogic.drop_judgment thy o Drule.plain_prop_of);
    72 
    73 val dest_func = lift_thm_thy (fn thy => apfst dest_Const o strip_comb
    74   o fst o Logic.dest_equals o ObjectLogic.drop_judgment thy o Drule.plain_prop_of
    75   o Drule.fconv_rule Drule.beta_eta_conversion);
    76 
    77 val mk_head = lift_thm_thy (fn thy => fn thm =>
    78   ((CodegenConsts.norm_of_typ thy o fst o dest_func) thm, thm));
    79 
    80 fun assert_func thm = case try dest_func thm
    81  of SOME (c_ty as (c, ty), args) =>
    82       let
    83         val thy = Thm.theory_of_thm thm;
    84         val _ =
    85           if has_duplicates (op =)
    86             ((fold o fold_aterms) (fn Var (v, _) => cons v
    87               | _ => I
    88             ) args [])
    89           then bad_thm "Repeated variables on left hand side of defining equation" thm
    90           else ()
    91         fun check _ (Abs _) = bad_thm
    92               "Abstraction on left hand side of defining equation" thm
    93           | check 0 (Var _) = ()
    94           | check _ (Var _) = bad_thm
    95               "Variable with application on left hand side of defining equation" thm
    96           | check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
    97           | check n (Const (_, ty)) = if n <> (length o fst o strip_type) ty
    98               then bad_thm
    99                 ("Partially applied constant on left hand side of defining equation") thm
   100               else ();
   101         val _ = map (check 0) args;
   102       in thm end
   103   | NONE => bad_thm "Not a defining equation" thm;
   104 
   105 val mk_func = map (mk_head o assert_func) o mk_rew;
   106 
   107 
   108 (* utilities *)
   109 
   110 fun inst_thm tvars' thm =
   111   let
   112     val thy = Thm.theory_of_thm thm;
   113     val tvars = (Term.add_tvars o Thm.prop_of) thm [];
   114     fun mk_inst (tvar as (v, _)) = case Vartab.lookup tvars' v
   115      of SOME sort => SOME (pairself (Thm.ctyp_of thy o TVar) (tvar, (v, sort)))
   116       | NONE => NONE;
   117     val insts = map_filter mk_inst tvars;
   118   in Thm.instantiate (insts, []) thm end;
   119 
   120 fun expand_eta k thm =
   121   let
   122     val thy = Thm.theory_of_thm thm;
   123     val (lhs, rhs) = (Logic.dest_equals o Drule.plain_prop_of) thm;
   124     val (head, args) = strip_comb lhs;
   125     val l = if k = ~1
   126       then (length o fst o strip_abs) rhs
   127       else Int.max (0, k - length args);
   128     val used = Name.make_context (map (fst o fst) (Term.add_vars lhs []));
   129     fun get_name _ 0 used = ([], used)
   130       | get_name (Abs (v, ty, t)) k used =
   131           used
   132           |> Name.variants [v]
   133           ||>> get_name t (k - 1)
   134           |>> (fn ([v'], vs') => (v', ty) :: vs')
   135       | get_name t k used = 
   136           let
   137             val (tys, _) = (strip_type o fastype_of) t
   138           in case tys
   139            of [] => raise TERM ("expand_eta", [t])
   140             | ty :: _ =>
   141                 used
   142                 |> Name.variants [""]
   143                 |-> (fn [v] => get_name (t $ Var ((v, 0), ty)) (k - 1)
   144                 #>> (fn vs' => (v, ty) :: vs'))
   145           end;
   146     val (vs, _) = get_name rhs l used;
   147     val vs_refl = map (fn (v, ty) => Thm.reflexive (Thm.cterm_of thy (Var ((v, 0), ty)))) vs;
   148   in
   149     fold (fn refl => fn thm => Thm.combination thm refl) vs_refl thm
   150   end;
   151 
   152 fun rewrite_func rewrites thm =
   153   let
   154     val rewrite = MetaSimplifier.rewrite false rewrites;
   155     val (ct_eq, [ct_lhs, ct_rhs]) = (Drule.strip_comb o Thm.cprop_of) thm;
   156     val Const ("==", _) = Thm.term_of ct_eq;
   157     val (ct_f, ct_args) = Drule.strip_comb ct_lhs;
   158     val rhs' = rewrite ct_rhs;
   159     val args' = map rewrite ct_args;
   160     val lhs' = Thm.symmetric (fold (fn th1 => fn th2 => Thm.combination th2 th1)
   161       args' (Thm.reflexive ct_f));
   162   in Thm.transitive (Thm.transitive lhs' thm) rhs' end;
   163 
   164 fun norm_args thms =
   165   let
   166     val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals;
   167     val k = fold (curry Int.max o num_args_of o Drule.plain_prop_of) thms 0;
   168   in
   169     thms
   170     |> map (expand_eta k)
   171     |> map (Drule.fconv_rule Drule.beta_eta_conversion)
   172   end;
   173 
   174 fun canonical_tvars purify_tvar thm =
   175   let
   176     val ctyp = Thm.ctyp_of (Thm.theory_of_thm thm);
   177     fun tvars_subst_for thm = (fold_types o fold_atyps)
   178       (fn TVar (v_i as (v, _), sort) => let
   179             val v' = purify_tvar v
   180           in if v = v' then I
   181           else insert (op =) (v_i, (v', sort)) end
   182         | _ => I) (prop_of thm) [];
   183     fun mk_inst (v_i, (v', sort)) (maxidx, acc) =
   184       let
   185         val ty = TVar (v_i, sort)
   186       in
   187         (maxidx + 1, (ctyp ty, ctyp (TVar ((v', maxidx), sort))) :: acc)
   188       end;
   189     val maxidx = Thm.maxidx_of thm + 1;
   190     val (_, inst) = fold mk_inst (tvars_subst_for thm) (maxidx + 1, []);
   191   in Thm.instantiate (inst, []) thm end;
   192 
   193 fun canonical_vars purify_var thm =
   194   let
   195     val cterm = Thm.cterm_of (Thm.theory_of_thm thm);
   196     fun vars_subst_for thm = fold_aterms
   197       (fn Var (v_i as (v, _), ty) => let
   198             val v' = purify_var v
   199           in if v = v' then I
   200           else insert (op =) (v_i, (v', ty)) end
   201         | _ => I) (prop_of thm) [];
   202     fun mk_inst (v_i as (v, i), (v', ty)) (maxidx, acc) =
   203       let
   204         val t = Var (v_i, ty)
   205       in
   206         (maxidx + 1, (cterm t, cterm (Var ((v', maxidx), ty))) :: acc)
   207       end;
   208     val maxidx = Thm.maxidx_of thm + 1;
   209     val (_, inst) = fold mk_inst (vars_subst_for thm) (maxidx + 1, []);
   210   in Thm.instantiate ([], inst) thm end;
   211 
   212 fun canonical_absvars purify_var thm =
   213   let
   214     val t = Thm.prop_of thm;
   215     val t' = Term.map_abs_vars purify_var t;
   216   in Thm.rename_boundvars t t' thm end;
   217 
   218 fun norm_varnames purify_tvar purify_var thms =
   219   let
   220     fun burrow_thms f [] = []
   221       | burrow_thms f thms =
   222           thms
   223           |> Conjunction.intr_list
   224           |> f
   225           |> Conjunction.elim_list;
   226   in
   227     thms
   228     |> burrow_thms (canonical_tvars purify_tvar)
   229     |> map (canonical_vars purify_var)
   230     |> map (canonical_absvars purify_var)
   231     |> map Drule.zero_var_indexes
   232   end;
   233 
   234 end;