directly computing the values of interest instead of composing functions in an unintelligent way that causes exponential much garbage; using the latest theory
authorbulwahn
Fri Sep 10 17:53:25 2010 +0200 (2010-09-10)
changeset 39299e98a06145530
parent 39282 7c69964c6d74
child 39300 ad79b89b4351
directly computing the values of interest instead of composing functions in an unintelligent way that causes exponential much garbage; using the latest theory
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Sep 10 15:48:43 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Fri Sep 10 17:53:25 2010 +0200
     1.3 @@ -27,6 +27,8 @@
     1.4    val ho_arg_modes_of : mode -> mode list
     1.5    val ho_argsT_of : mode -> typ list -> typ list
     1.6    val ho_args_of : mode -> term list -> term list
     1.7 +  val ho_args_of_typ : typ -> term list -> term list
     1.8 +  val ho_argsT_of_typ : typ list -> typ list
     1.9    val split_map_mode : (mode -> term -> term option * term option)
    1.10      -> mode -> term list -> term list * term list
    1.11    val split_map_modeT : (mode -> typ -> typ option * typ option)
    1.12 @@ -262,6 +264,31 @@
    1.13      flat (map2_optional ho_arg (strip_fun_mode mode) ts)
    1.14    end
    1.15  
    1.16 +fun ho_args_of_typ T ts =
    1.17 +  let
    1.18 +    fun ho_arg (Type("fun", [_,_])) (SOME t) = [t]
    1.19 +      | ho_arg (Type("fun", [_,_])) NONE = raise Fail "mode and term do not match"
    1.20 +      | ho_arg (Type(@{type_name "Product_Type.prod"}, [T1, T2]))
    1.21 +         (SOME (Const (@{const_name Pair}, _) $ t1 $ t2)) =
    1.22 +          ho_arg T1 (SOME t1) @ ho_arg T2 (SOME t2)
    1.23 +      | ho_arg (Type(@{type_name "Product_Type.prod"}, [T1, T2])) NONE =
    1.24 +          ho_arg T1 NONE @ ho_arg T2 NONE
    1.25 +      | ho_arg _ _ = []
    1.26 +  in
    1.27 +    flat (map2_optional ho_arg (binder_types T) ts)
    1.28 +  end
    1.29 +
    1.30 +fun ho_argsT_of_typ Ts =
    1.31 +  let
    1.32 +    fun ho_arg (T as Type("fun", [_,_])) = [T]
    1.33 +      | ho_arg (Type(@{type_name "Product_Type.prod"}, [T1, T2])) =
    1.34 +          ho_arg T1 @ ho_arg T2
    1.35 +      | ho_arg _ = []
    1.36 +  in
    1.37 +    maps ho_arg Ts
    1.38 +  end
    1.39 +  
    1.40 +
    1.41  (* temporary function should be replaced by unsplit_input or so? *)
    1.42  fun replace_ho_args mode hoargs ts =
    1.43    let
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Sep 10 15:48:43 2010 +0200
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Sep 10 17:53:25 2010 +0200
     2.3 @@ -446,8 +446,7 @@
     2.4    let
     2.5      val ([outp_pred], ctxt') = Variable.import_terms true [inp_pred] ctxt
     2.6      val T = fastype_of outp_pred
     2.7 -    (* TODO: put in a function for this next line! *)
     2.8 -    val paramTs = ho_argsT_of (hd (all_modes_of_typ T)) (binder_types T)
     2.9 +    val paramTs = ho_argsT_of_typ (binder_types T)
    2.10      val (param_names, ctxt'') = Variable.variant_fixes
    2.11        (map (fn i => "p" ^ (string_of_int i)) (1 upto (length paramTs))) ctxt'
    2.12      val params = map2 (curry Free) param_names paramTs
    2.13 @@ -460,7 +459,7 @@
    2.14        val thy = ProofContext.theory_of ctxt'
    2.15        val (pred, args) = strip_intro_concl th'
    2.16        val T = fastype_of pred
    2.17 -      val ho_args = ho_args_of (hd (all_modes_of_typ T)) args
    2.18 +      val ho_args = ho_args_of_typ T args
    2.19        fun subst_of (pred', pred) =
    2.20          let
    2.21            val subst = Sign.typ_match thy (fastype_of pred', fastype_of pred) Vartab.empty
    2.22 @@ -474,7 +473,7 @@
    2.23        fun instantiate_ho_args th =
    2.24          let
    2.25            val (_, args') = (strip_comb o HOLogic.dest_Trueprop o Logic.strip_imp_concl o prop_of) th
    2.26 -          val ho_args' = map dest_Var (ho_args_of (hd (all_modes_of_typ T)) args')
    2.27 +          val ho_args' = map dest_Var (ho_args_of_typ T args')
    2.28          in Thm.certify_instantiate ([], ho_args' ~~ ho_args) th end
    2.29        val outp_pred =
    2.30          Term_Subst.instantiate (subst_of (inp_pred, pred), []) inp_pred
    2.31 @@ -2710,7 +2709,7 @@
    2.32            let
    2.33              val T = snd (hd preds)
    2.34              val paramTs =
    2.35 -              ho_argsT_of (hd (all_modes_of_typ T)) (binder_types T)
    2.36 +              ho_argsT_of_typ (binder_types T)
    2.37              val param_names = Name.variant_list [] (map (fn i => "p" ^ string_of_int i)
    2.38                (1 upto length paramTs))
    2.39            in
    2.40 @@ -3067,7 +3066,7 @@
    2.41      val preds = Graph.all_succs (PredData.get thy') [const] |> filter_out (has_elim ctxt')
    2.42      fun mk_cases const =
    2.43        let
    2.44 -        val T = Sign.the_const_type thy const
    2.45 +        val T = Sign.the_const_type thy' const
    2.46          val pred = Const (const, T)
    2.47          val intros = intros_of ctxt' const
    2.48        in mk_casesrule lthy' pred intros end