src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 55399 5c8e91f884af
parent 54742 7a86358a3c0b
child 55440 721b4561007a
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Feb 12 08:35:56 2014 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Feb 12 08:35:56 2014 +0100
     1.3 @@ -47,6 +47,7 @@
     1.4    val is_pred_equation : thm -> bool
     1.5    val is_intro : string -> thm -> bool
     1.6    val is_predT : typ -> bool
     1.7 +  val get_constrs : theory -> (string * (int * string)) list
     1.8    val is_constrt : theory -> term -> bool
     1.9    val is_constr : Proof.context -> string -> bool
    1.10    val strip_ex : term -> (string * typ) list * term
    1.11 @@ -477,15 +478,22 @@
    1.12  fun is_predT (T as Type("fun", [_, _])) = (body_type T = @{typ bool})
    1.13    | is_predT _ = false
    1.14  
    1.15 +fun get_constrs thy =
    1.16 +  let
    1.17 +    val ctxt = Proof_Context.init_global thy
    1.18 +  in
    1.19 +    Ctr_Sugar.ctr_sugars_of ctxt
    1.20 +    |> maps (map_filter (try dest_Const) o #ctrs)
    1.21 +    |> map (apsnd (fn T => (BNF_Util.num_binder_types T, fst (dest_Type (body_type T)))))
    1.22 +  end
    1.23 +
    1.24  (*** check if a term contains only constructor functions ***)
    1.25  (* TODO: another copy in the core! *)
    1.26  (* FIXME: constructor terms are supposed to be seen in the way the code generator
    1.27    sees constructors.*)
    1.28  fun is_constrt thy =
    1.29    let
    1.30 -    val cnstrs = flat (maps
    1.31 -      (map (fn (_, (Tname, _, cs)) => map (apsnd (rpair Tname o length)) cs) o #descr o snd)
    1.32 -      (Symtab.dest (Datatype.get_all thy)));
    1.33 +    val cnstrs = get_constrs thy
    1.34      fun check t = (case strip_comb t of
    1.35          (Var _, []) => true
    1.36        | (Free _, []) => true
    1.37 @@ -495,23 +503,6 @@
    1.38        | _ => false)
    1.39    in check end;
    1.40  
    1.41 -(* returns true if t is an application of an datatype constructor *)
    1.42 -(* which then consequently would be splitted *)
    1.43 -(* else false *)
    1.44 -(*
    1.45 -fun is_constructor thy t =
    1.46 -  if (is_Type (fastype_of t)) then
    1.47 -    (case DatatypePackage.get_datatype thy ((fst o dest_Type o fastype_of) t) of
    1.48 -      NONE => false
    1.49 -    | SOME info => (let
    1.50 -      val constr_consts = maps (fn (_, (_, _, constrs)) => map fst constrs) (#descr info)
    1.51 -      val (c, _) = strip_comb t
    1.52 -      in (case c of
    1.53 -        Const (name, _) => name mem_string constr_consts
    1.54 -        | _ => false) end))
    1.55 -  else false
    1.56 -*)
    1.57 -
    1.58  val is_constr = Code.is_constr o Proof_Context.theory_of;
    1.59  
    1.60  fun strip_all t = (Term.strip_all_vars t, Term.strip_all_body t)
    1.61 @@ -601,7 +592,8 @@
    1.62      |> Local_Defs.unfold ctxt [@{thm atomize_conjL[symmetric]},
    1.63        @{thm atomize_all[symmetric]}, @{thm atomize_imp[symmetric]}]
    1.64  
    1.65 -fun find_split_thm thy (Const (name, _)) = Option.map #split (Datatype.info_of_case thy name)
    1.66 +fun find_split_thm thy (Const (name, _)) =
    1.67 +    Option.map #split (Ctr_Sugar.ctr_sugar_of_case (Proof_Context.init_global thy) name)
    1.68    | find_split_thm thy _ = NONE
    1.69  
    1.70  (* lifting term operations to theorems *)
    1.71 @@ -880,76 +872,72 @@
    1.72  (** making case distributivity rules **)
    1.73  (*** this should be part of the datatype package ***)
    1.74  
    1.75 -fun datatype_names_of_case_name thy case_name =
    1.76 -  map (#1 o #2) (#descr (the (Datatype.info_of_case thy case_name)))
    1.77 +fun datatype_name_of_case_name thy =
    1.78 +  Ctr_Sugar.ctr_sugar_of_case (Proof_Context.init_global thy)
    1.79 +  #> the #> #ctrs #> hd #> fastype_of #> body_type #> dest_Type #> fst
    1.80  
    1.81 -fun make_case_distribs case_names descr thy =
    1.82 +fun make_case_comb thy Tcon =
    1.83    let
    1.84 -    val case_combs = Datatype_Prop.make_case_combs case_names descr thy "f";
    1.85 -    fun make comb =
    1.86 -      let
    1.87 -        val Type ("fun", [T, T']) = fastype_of comb;
    1.88 -        val (Const (case_name, _), fs) = strip_comb comb
    1.89 -        val used = Term.add_tfree_names comb []
    1.90 -        val U = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS)
    1.91 -        val x = Free ("x", T)
    1.92 -        val f = Free ("f", T' --> U)
    1.93 -        fun apply_f f' =
    1.94 -          let
    1.95 -            val Ts = binder_types (fastype_of f')
    1.96 -            val bs = map Bound ((length Ts - 1) downto 0)
    1.97 -          in
    1.98 -            fold_rev absdummy Ts (f $ (list_comb (f', bs)))
    1.99 -          end
   1.100 -        val fs' = map apply_f fs
   1.101 -        val case_c' = Const (case_name, (map fastype_of fs') @ [T] ---> U)
   1.102 -      in
   1.103 -        HOLogic.mk_eq (f $ (comb $ x), list_comb (case_c', fs') $ x)
   1.104 -      end
   1.105 +    val ctxt = Proof_Context.init_global thy
   1.106 +    val SOME {casex, ...} = Ctr_Sugar.ctr_sugar_of ctxt Tcon
   1.107 +    val casex' = Type.legacy_freeze casex
   1.108 +    val Ts = BNF_Util.binder_fun_types (fastype_of casex')
   1.109    in
   1.110 -    map make case_combs
   1.111 +    list_comb (casex', map_index (fn (j, T) => Free ("f" ^ string_of_int j,  T)) Ts)
   1.112    end
   1.113  
   1.114 -fun case_rewrites thy Tcon =
   1.115 +fun make_case_distrib thy Tcon =
   1.116    let
   1.117 -    val {descr, case_name, ...} = Datatype.the_info thy Tcon
   1.118 +    val comb = make_case_comb thy Tcon;
   1.119 +    val Type ("fun", [T, T']) = fastype_of comb;
   1.120 +    val (Const (case_name, _), fs) = strip_comb comb
   1.121 +    val used = Term.add_tfree_names comb []
   1.122 +    val U = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS)
   1.123 +    val x = Free ("x", T)
   1.124 +    val f = Free ("f", T' --> U)
   1.125 +    fun apply_f f' =
   1.126 +      let
   1.127 +        val Ts = binder_types (fastype_of f')
   1.128 +        val bs = map Bound ((length Ts - 1) downto 0)
   1.129 +      in
   1.130 +        fold_rev absdummy Ts (f $ (list_comb (f', bs)))
   1.131 +      end
   1.132 +    val fs' = map apply_f fs
   1.133 +    val case_c' = Const (case_name, (map fastype_of fs') @ [T] ---> U)
   1.134    in
   1.135 -    map (Drule.export_without_context o Skip_Proof.make_thm thy o HOLogic.mk_Trueprop)
   1.136 -      (make_case_distribs [case_name] [descr] thy)
   1.137 +    HOLogic.mk_eq (f $ (comb $ x), list_comb (case_c', fs') $ x)
   1.138    end
   1.139  
   1.140 -fun instantiated_case_rewrites thy Tcon =
   1.141 +fun case_rewrite thy Tcon =
   1.142 +  (Drule.export_without_context o Skip_Proof.make_thm thy o HOLogic.mk_Trueprop)
   1.143 +    (make_case_distrib thy Tcon)
   1.144 +
   1.145 +fun instantiated_case_rewrite thy Tcon =
   1.146    let
   1.147 -    val rew_ths = case_rewrites thy Tcon
   1.148 +    val th = case_rewrite thy Tcon
   1.149      val ctxt = Proof_Context.init_global thy
   1.150 -    fun instantiate th =
   1.151 -    let
   1.152 -      val f = (fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th))))))
   1.153 -      val Type ("fun", [uninst_T, uninst_T']) = fastype_of f
   1.154 -      val ([_, tname', uname, yname], ctxt') = Variable.add_fixes ["'t", "'t'", "'u", "y"] ctxt
   1.155 -      val T' = TFree (tname', HOLogic.typeS)
   1.156 -      val U = TFree (uname, HOLogic.typeS)
   1.157 -      val y = Free (yname, U)
   1.158 -      val f' = absdummy (U --> T') (Bound 0 $ y)
   1.159 -      val th' = Thm.certify_instantiate
   1.160 -        ([(dest_TVar uninst_T, U --> T'), (dest_TVar uninst_T', T')],
   1.161 -         [((fst (dest_Var f), (U --> T') --> T'), f')]) th
   1.162 -      val [th'] = Variable.export ctxt' ctxt [th']
   1.163 -   in
   1.164 -     th'
   1.165 -   end
   1.166 - in
   1.167 -   map instantiate rew_ths
   1.168 - end
   1.169 +    val f = (fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th))))))
   1.170 +    val Type ("fun", [uninst_T, uninst_T']) = fastype_of f
   1.171 +    val ([_, tname', uname, yname], ctxt') = Variable.add_fixes ["'t", "'t'", "'u", "y"] ctxt
   1.172 +    val T' = TFree (tname', HOLogic.typeS)
   1.173 +    val U = TFree (uname, HOLogic.typeS)
   1.174 +    val y = Free (yname, U)
   1.175 +    val f' = absdummy (U --> T') (Bound 0 $ y)
   1.176 +    val th' = Thm.certify_instantiate
   1.177 +      ([(dest_TVar uninst_T, U --> T'), (dest_TVar uninst_T', T')],
   1.178 +       [((fst (dest_Var f), (U --> T') --> T'), f')]) th
   1.179 +    val [th'] = Variable.export ctxt' ctxt [th']
   1.180 +  in
   1.181 +    th'
   1.182 +  end
   1.183  
   1.184  fun case_betapply thy t =
   1.185    let
   1.186      val case_name = fst (dest_Const (fst (strip_comb t)))
   1.187 -    val Tcons = datatype_names_of_case_name thy case_name
   1.188 -    val ths = maps (instantiated_case_rewrites thy) Tcons
   1.189 +    val Tcon = datatype_name_of_case_name thy case_name
   1.190 +    val th = instantiated_case_rewrite thy Tcon
   1.191    in
   1.192 -    Raw_Simplifier.rewrite_term thy
   1.193 -      (map (fn th => th RS @{thm eq_reflection}) ths) [] t
   1.194 +    Raw_Simplifier.rewrite_term thy [th RS @{thm eq_reflection}] [] t
   1.195    end
   1.196  
   1.197  (*** conversions ***)