src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 33565 5fad8e36dfb1
parent 33558 a2db56854b83
child 33571 3655e51f9958
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Oct 29 11:41:11 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Oct 29 11:41:37 2009 +0100
     1.3 @@ -133,12 +133,14 @@
     1.4        | aux t = raise TERM ("Nitpick_Model.dest_plain_fun", [t])
     1.5    in apsnd (pairself rev) o aux end
     1.6  
     1.7 -(* typ -> term -> term list * term *)
     1.8 -fun break_in_two (Type ("*", [T1, T2]))
     1.9 -                 (Const (@{const_name Pair}, _) $ t1 $ t2) =
    1.10 -    break_in_two T2 t2 |>> cons t1
    1.11 -  | break_in_two _ (Const (@{const_name Pair}, _) $ t1 $ t2) = ([t1], t2)
    1.12 -  | break_in_two _ t = raise TERM ("Nitpick_Model.break_in_two", [t])
    1.13 +(* typ -> typ -> typ -> term -> term * term *)
    1.14 +fun break_in_two T T1 T2 t =
    1.15 +  let
    1.16 +    val ps = HOLogic.flat_tupleT_paths T
    1.17 +    val cut = length (HOLogic.strip_tupleT T1)
    1.18 +    val (ps1, ps2) = pairself HOLogic.flat_tupleT_paths (T1, T2)
    1.19 +    val (ts1, ts2) = t |> HOLogic.strip_ptuple ps |> chop cut
    1.20 +  in (HOLogic.mk_ptuple ps1 T1 ts1, HOLogic.mk_ptuple ps2 T2 ts2) end
    1.21  (* typ -> term -> term -> term *)
    1.22  fun pair_up (Type ("*", [T1', T2']))
    1.23              (t1 as Const (@{const_name Pair},
    1.24 @@ -153,12 +155,12 @@
    1.25  (* typ -> typ -> typ -> term -> term *)
    1.26  fun typecast_fun (Type ("fun", [T1', T2'])) T1 T2 t =
    1.27      let
    1.28 -      (* typ -> typ -> typ -> term -> term *)
    1.29 -      fun do_curry T1a T1b T2 t =
    1.30 +      (* typ -> typ -> typ -> typ -> term -> term *)
    1.31 +      fun do_curry T1 T1a T1b T2 t =
    1.32          let
    1.33            val (maybe_opt, ps) = dest_plain_fun t
    1.34            val ps =
    1.35 -            ps |>> map (break_in_two T1a #>> mk_flat_tuple T1a)
    1.36 +            ps |>> map (break_in_two T1 T1a T1b)
    1.37                 |> uncurry (map2 (fn (t1a, t1b) => fn t2 => (t1a, (t1b, t2))))
    1.38                 |> AList.coalesce (op =)
    1.39                 |> map (apsnd (make_plain_fun maybe_opt T1b T2))
    1.40 @@ -185,7 +187,7 @@
    1.41          case factor_out_types T1' T1 of
    1.42            ((_, NONE), (_, NONE)) => t |> do_arrow T1' T2' T1 T2
    1.43          | ((_, NONE), (T1a, SOME T1b)) =>
    1.44 -          t |> do_curry T1a T1b T2 |> do_arrow T1' T2' T1a (T1b --> T2)
    1.45 +          t |> do_curry T1 T1a T1b T2 |> do_arrow T1' T2' T1a (T1b --> T2)
    1.46          | ((T1a', SOME T1b'), (_, NONE)) =>
    1.47            t |> do_arrow T1a' (T1b' --> T2') T1 T2 |> do_uncurry T1' T2'
    1.48          | _ => raise TYPE ("Nitpick_Model.typecast_fun.do_fun", [T1, T1'], [])