src/Pure/Isar/code.ML
changeset 34895 19fd499cddff
parent 34894 fadbdd350dd1
child 34901 0d6a2ae86525
     1.1 --- a/src/Pure/Isar/code.ML	Wed Jan 13 10:18:45 2010 +0100
     1.2 +++ b/src/Pure/Isar/code.ML	Wed Jan 13 12:20:37 2010 +0100
     1.3 @@ -29,12 +29,15 @@
     1.4    val mk_eqn_liberal: theory -> thm -> (thm * bool) option
     1.5    val assert_eqn: theory -> thm * bool -> thm * bool
     1.6    val const_typ_eqn: theory -> thm -> string * typ
     1.7 -  type cert = thm * bool list
     1.8 +  val expand_eta: theory -> int -> thm -> thm
     1.9 +  type cert
    1.10    val empty_cert: theory -> string -> cert
    1.11    val cert_of_eqns: theory -> string -> (thm * bool) list -> cert
    1.12    val constrain_cert: theory -> sort list -> cert -> cert
    1.13 -  val eqns_of_cert: theory -> cert -> (thm * bool) list
    1.14 -  val dest_cert: theory -> cert -> ((string * sort) list * typ) * ((term list * term) * (thm * bool)) list
    1.15 +  val typscheme_cert: theory -> cert -> (string * sort) list * typ
    1.16 +  val equations_cert: theory -> cert -> ((string * sort) list * typ) * (term list * term) list
    1.17 +  val equations_thms_cert: theory -> cert -> ((string * sort) list * typ) * ((term list * term) * (thm * bool)) list
    1.18 +  val pretty_cert: theory -> cert -> Pretty.T list
    1.19  
    1.20    (*executable code*)
    1.21    val add_type: string -> theory -> theory
    1.22 @@ -511,20 +514,71 @@
    1.23  
    1.24  fun typscheme thy (c, ty) = logical_typscheme thy (c, subst_signature thy c ty);
    1.25  
    1.26 -fun assert_eqns_const thy c eqns =
    1.27 +
    1.28 +(* technical transformations of code equations *)
    1.29 +
    1.30 +fun expand_eta thy k thm =
    1.31 +  let
    1.32 +    val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm;
    1.33 +    val (_, args) = strip_comb lhs;
    1.34 +    val l = if k = ~1
    1.35 +      then (length o fst o strip_abs) rhs
    1.36 +      else Int.max (0, k - length args);
    1.37 +    val (raw_vars, _) = Term.strip_abs_eta l rhs;
    1.38 +    val vars = burrow_fst (Name.variant_list (map (fst o fst) (Term.add_vars lhs [])))
    1.39 +      raw_vars;
    1.40 +    fun expand (v, ty) thm = Drule.fun_cong_rule thm
    1.41 +      (Thm.cterm_of thy (Var ((v, 0), ty)));
    1.42 +  in
    1.43 +    thm
    1.44 +    |> fold expand vars
    1.45 +    |> Conv.fconv_rule Drule.beta_eta_conversion
    1.46 +  end;
    1.47 +
    1.48 +fun same_arity thy thms =
    1.49    let
    1.50 -    fun cert (eqn as (thm, _)) = if c = const_eqn thy thm
    1.51 -      then eqn else error ("Wrong head of code equation,\nexpected constant "
    1.52 -        ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm_global thy thm)
    1.53 -  in map (cert o assert_eqn thy) eqns end;
    1.54 +    val num_args_of = length o snd o strip_comb o fst o Logic.dest_equals;
    1.55 +    val k = fold (Integer.max o num_args_of o Thm.prop_of) thms 0;
    1.56 +  in map (expand_eta thy k) thms end;
    1.57 +
    1.58 +fun mk_desymbolization pre post mk vs =
    1.59 +  let
    1.60 +    val names = map (pre o fst o fst) vs
    1.61 +      |> map (Name.desymbolize false)
    1.62 +      |> Name.variant_list []
    1.63 +      |> map post;
    1.64 +  in map_filter (fn (((v, i), x), v') =>
    1.65 +    if v = v' andalso i = 0 then NONE
    1.66 +    else SOME (((v, i), x), mk ((v', 0), x))) (vs ~~ names)
    1.67 +  end;
    1.68 +
    1.69 +fun desymbolize_tvars thy thms =
    1.70 +  let
    1.71 +    val tvs = fold (Term.add_tvars o Thm.prop_of) thms [];
    1.72 +    val tvar_subst = mk_desymbolization (unprefix "'") (prefix "'") TVar tvs;
    1.73 +  in map (Thm.certify_instantiate (tvar_subst, [])) thms end;
    1.74 +
    1.75 +fun desymbolize_vars thy thm =
    1.76 +  let
    1.77 +    val vs = Term.add_vars (Thm.prop_of thm) [];
    1.78 +    val var_subst = mk_desymbolization I I Var vs;
    1.79 +  in Thm.certify_instantiate ([], var_subst) thm end;
    1.80 +
    1.81 +fun canonize_thms thy = desymbolize_tvars thy #> same_arity thy #> map (desymbolize_vars thy);
    1.82  
    1.83  
    1.84  (* code equation certificates *)
    1.85  
    1.86 -type cert = thm * bool list;
    1.87 +fun build_head thy (c, ty) =
    1.88 +  Thm.cterm_of thy (Logic.mk_equals (Free ("HEAD", ty), Const (c, ty)));
    1.89  
    1.90 -fun mk_head_cterm thy (c, ty) =
    1.91 -  Thm.cterm_of thy (Logic.mk_equals (Free ("HEAD", ty), Const (c, ty)));
    1.92 +fun get_head thy cert_thm =
    1.93 +  let
    1.94 +    val [head] = (#hyps o Thm.crep_thm) cert_thm;
    1.95 +    val (_, Const (c, ty)) = (Logic.dest_equals o Thm.term_of) head;
    1.96 +  in (typscheme thy (c, ty), head) end;
    1.97 +
    1.98 +abstype cert = Cert of thm * bool list with
    1.99  
   1.100  fun empty_cert thy c = 
   1.101    let
   1.102 @@ -535,14 +589,18 @@
   1.103        | NONE => Name.invent_list [] Name.aT (length tvars)
   1.104            |> map (fn v => TFree (v, []));
   1.105      val ty = typ_subst_TVars (tvars ~~ tvars') raw_ty;
   1.106 -    val chead = mk_head_cterm thy (c, ty);
   1.107 -  in (Thm.weaken chead Drule.dummy_thm, []) end;
   1.108 +    val chead = build_head thy (c, ty);
   1.109 +  in Cert (Thm.weaken chead Drule.dummy_thm, []) end;
   1.110  
   1.111  fun cert_of_eqns thy c [] = empty_cert thy c
   1.112 -  | cert_of_eqns thy c eqns = 
   1.113 +  | cert_of_eqns thy c raw_eqns = 
   1.114        let
   1.115 -        val _ = assert_eqns_const thy c eqns;
   1.116 +        val eqns = burrow_fst (canonize_thms thy) raw_eqns;
   1.117 +        val _ = map (assert_eqn thy) eqns;
   1.118          val (thms, propers) = split_list eqns;
   1.119 +        val _ = map (fn thm => if c = const_eqn thy thm then ()
   1.120 +          else error ("Wrong head of code equation,\nexpected constant "
   1.121 +            ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm_global thy thm)) thms;
   1.122          fun tvars_of T = rev (Term.add_tvarsT T []);
   1.123          val vss = map (tvars_of o snd o head_eqn) thms;
   1.124          fun inter_sorts vs =
   1.125 @@ -551,55 +609,59 @@
   1.126          val vts = Name.names Name.context Name.aT sorts;
   1.127          val thms as thm :: _ =
   1.128            map2 (fn vs => Thm.certify_instantiate (vs ~~ map TFree vts, [])) vss thms;
   1.129 -        val head_thm = Thm.symmetric (Thm.assume (mk_head_cterm thy (head_eqn (hd thms))));
   1.130 +        val head_thm = Thm.symmetric (Thm.assume (build_head thy (head_eqn (hd thms))));
   1.131          fun head_conv ct = if can Thm.dest_comb ct
   1.132            then Conv.fun_conv head_conv ct
   1.133            else Conv.rewr_conv head_thm ct;
   1.134          val rewrite_head = Conv.fconv_rule (Conv.arg1_conv head_conv);
   1.135          val cert_thm = Conjunction.intr_balanced (map rewrite_head thms);
   1.136 -      in (cert_thm, propers) end;
   1.137 -
   1.138 -fun head_cert thy cert_thm =
   1.139 -  let
   1.140 -    val [head] = Thm.hyps_of cert_thm;
   1.141 -    val (Free (h, _), Const (c, ty)) = Logic.dest_equals head;
   1.142 -  in ((c, typscheme thy (c, ty)), (head, h)) end;
   1.143 +      in Cert (cert_thm, propers) end;
   1.144  
   1.145 -fun constrain_cert thy sorts (cert_thm, propers) =
   1.146 +fun constrain_cert thy sorts (Cert (cert_thm, propers)) =
   1.147    let
   1.148 -    val ((c, (vs, _)), (head, _)) = head_cert thy cert_thm;
   1.149 -    val subst = map2 (fn (v, _) => fn sort => (v, sort)) vs sorts;
   1.150 -    val head' = (map_types o map_atyps)
   1.151 -      (fn TFree (v, _) => TFree (v, the (AList.lookup (op =) subst v))) head;
   1.152 -    val inst = (map2 (fn (v, sort) => fn sort' =>
   1.153 -      pairself (Thm.ctyp_of thy) (TVar ((v, 0), sort), TFree (v, sort'))) vs sorts, []);
   1.154 +    val ((vs, _), head) = get_head thy cert_thm;
   1.155 +    val subst = map2 (fn (v, sort) => fn sort' =>
   1.156 +      (v, Sorts.inter_sort (Sign.classes_of thy) (sort, sort'))) vs sorts;
   1.157 +    val head' = Thm.term_of head
   1.158 +      |> (map_types o map_atyps)
   1.159 +          (fn TFree (v, _) => TFree (v, the (AList.lookup (op =) subst v)))
   1.160 +      |> Thm.cterm_of thy;
   1.161 +    val inst = map2 (fn (v, sort) => fn (_, sort') =>
   1.162 +      (((v, 0), sort), TFree (v, sort'))) vs subst;
   1.163      val cert_thm' = cert_thm
   1.164 -      |> Thm.implies_intr (Thm.cterm_of thy head)
   1.165 +      |> Thm.implies_intr head
   1.166        |> Thm.varifyT
   1.167 -      |> Thm.instantiate inst
   1.168 -      |> Thm.elim_implies (Thm.assume (Thm.cterm_of thy head'));
   1.169 -  in (cert_thm', propers) end;
   1.170 +      |> Thm.certify_instantiate (inst, [])
   1.171 +      |> Thm.elim_implies (Thm.assume head');
   1.172 +  in (Cert (cert_thm', propers)) end;
   1.173  
   1.174 -fun eqns_of_cert thy (cert_thm, []) = []
   1.175 -  | eqns_of_cert thy (cert_thm, propers) =
   1.176 -      let
   1.177 -        val (_, (head, _)) = head_cert thy cert_thm;
   1.178 -        val thms = cert_thm
   1.179 -          |> LocalDefs.expand [Thm.cterm_of thy head]
   1.180 -          |> Thm.varifyT
   1.181 -          |> Conjunction.elim_balanced (length propers)
   1.182 -      in thms ~~ propers end;
   1.183 +fun typscheme_cert thy (Cert (cert_thm, _)) =
   1.184 +  fst (get_head thy cert_thm);
   1.185  
   1.186 -fun dest_cert thy (cert as (cert_thm, propers)) =
   1.187 +fun equations_cert thy (cert as Cert (cert_thm, propers)) =
   1.188    let
   1.189 -    val eqns = eqns_of_cert thy cert;
   1.190 -    val ((_, vs_ty), _) = head_cert thy cert_thm;
   1.191 -    val equations = if null propers then [] else cert_thm
   1.192 -      |> Thm.prop_of
   1.193 +    val tyscm = typscheme_cert thy cert;
   1.194 +    val equations = if null propers then [] else
   1.195 +      Thm.prop_of cert_thm
   1.196        |> Logic.dest_conjunction_balanced (length propers)
   1.197        |> map Logic.dest_equals
   1.198        |> (map o apfst) (snd o strip_comb)
   1.199 -  in (vs_ty, equations ~~ eqns) end;
   1.200 +  in (tyscm, equations) end;
   1.201 +
   1.202 +fun equations_thms_cert thy (cert as Cert (cert_thm, propers)) =
   1.203 +  let
   1.204 +    val (tyscm, equations) = equations_cert thy cert;
   1.205 +    val thms = if null propers then [] else
   1.206 +      cert_thm
   1.207 +      |> LocalDefs.expand [snd (get_head thy cert_thm)]
   1.208 +      |> Thm.varifyT
   1.209 +      |> Conjunction.elim_balanced (length propers)
   1.210 +  in (tyscm, equations ~~ (thms ~~ propers)) end;
   1.211 +
   1.212 +fun pretty_cert thy = map (Display.pretty_thm_global thy o AxClass.overload thy o fst o snd)
   1.213 +  o snd o equations_thms_cert thy;
   1.214 +
   1.215 +end;
   1.216  
   1.217  
   1.218  (* code equation access *)