Fixed old bug: selection of constant to be split should depend not just on
authornipkow
Thu Jan 14 13:20:02 1999 +0100 (1999-01-14)
changeset 613030b84ad2131d
parent 6129 0f5ecd633c2f
child 6131 2d9e609abcdb
Fixed old bug: selection of constant to be split should depend not just on
the name but also on the type.
src/Provers/splitter.ML
     1.1 --- a/src/Provers/splitter.ML	Thu Jan 14 13:19:12 1999 +0100
     1.2 +++ b/src/Provers/splitter.ML	Thu Jan 14 13:20:02 1999 +0100
     1.3 @@ -185,23 +185,28 @@
     1.4     t    : the term to be scanned
     1.5  ******************************************************************************)
     1.6  
     1.7 -fun split_posns cmap Ts t =
     1.8 -  let fun posns Ts pos apsns (Abs(_,T,t)) =
     1.9 -            let val U = fastype_of1(T::Ts,t)
    1.10 -            in posns (T::Ts) (0::pos) ((T,U,pos)::apsns) t end
    1.11 -        | posns Ts pos apsns t =
    1.12 -            let val (h,ts) = strip_comb t
    1.13 -                fun iter((i,a),t) = (i+1, (posns Ts (i::pos) apsns t) @ a);
    1.14 -                val a = case h of
    1.15 -                  Const(c,_) =>
    1.16 -                    (case assoc(cmap,c) of
    1.17 -                       Some(thm, T, n) =>
    1.18 -                         let val t2 = list_comb (h, take (n, ts)) in
    1.19 -                           mk_split_pack(thm,T,n,ts,apsns,pos,type_of1(Ts, t2),t2)
    1.20 -                         end
    1.21 -                     | None => [])
    1.22 -                | _ => []
    1.23 -             in snd(foldl iter ((0,a),ts)) end
    1.24 +fun split_posns cmap sg Ts t =
    1.25 +  let
    1.26 +    fun posns Ts pos apsns (Abs(_,T,t)) =
    1.27 +          let val U = fastype_of1(T::Ts,t)
    1.28 +          in posns (T::Ts) (0::pos) ((T,U,pos)::apsns) t end
    1.29 +      | posns Ts pos apsns t =
    1.30 +          let
    1.31 +            val (h,ts) = strip_comb t
    1.32 +            fun iter((i,a),t) = (i+1, (posns Ts (i::pos) apsns t) @ a);
    1.33 +            val a = case h of
    1.34 +              Const(c,cT) =>
    1.35 +                (case assoc(cmap,c) of
    1.36 +                   Some(gcT, thm, T, n) =>
    1.37 +                     if Type.typ_instance(Sign.tsig_of sg, cT, gcT)
    1.38 +                     then
    1.39 +                       let val t2 = list_comb (h, take (n, ts))
    1.40 +                       in mk_split_pack(thm,T,n,ts,apsns,pos,type_of1(Ts, t2),t2)
    1.41 +                       end
    1.42 +                     else []
    1.43 +                 | None => [])
    1.44 +            | _ => []
    1.45 +          in snd(foldl iter ((0,a),ts)) end
    1.46    in posns Ts [] [] t end;
    1.47  
    1.48  
    1.49 @@ -218,10 +223,11 @@
    1.50  *************************************************************)
    1.51  
    1.52  fun select cmap state i =
    1.53 -  let val goali = nth_subgoal i state
    1.54 +  let val sg = #sign(rep_thm state)
    1.55 +      val goali = nth_subgoal i state
    1.56        val Ts = rev(map #2 (Logic.strip_params goali))
    1.57        val _ $ t $ _ = Logic.strip_assums_concl goali;
    1.58 -  in (Ts,t, sort shorter (split_posns cmap Ts t)) end;
    1.59 +  in (Ts,t, sort shorter (split_posns cmap sg Ts t)) end;
    1.60  
    1.61  
    1.62  (*************************************************************
    1.63 @@ -291,8 +297,8 @@
    1.64    let val splits = map Data.mk_eq splits;
    1.65        fun const(thm) =
    1.66              (case concl_of thm of _$(t as _$lhs)$_ =>
    1.67 -               (case strip_comb lhs of (Const(a,_),args) =>
    1.68 -                  (a,(thm,fastype_of t,length args))
    1.69 +               (case strip_comb lhs of (Const(a,aT),args) =>
    1.70 +                  (a,(aT,thm,fastype_of t,length args))
    1.71                  | _ => split_format_err())
    1.72               | _ => split_format_err())
    1.73        val cmap = map const splits;