src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
changeset 39299 e98a06145530
parent 39192 f302ed18f42f
child 39311 2bd067f80b92
     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