HOLogic.strip_psplits: types are ordered after syntactic appearance, not after corresponding de-Bruin index (closer correspondence to similar strip operations)
authorhaftmann
Fri Jan 22 16:56:51 2010 +0100 (2010-01-22)
changeset 34962807f6ce0273d
parent 34947 e1b8f2736404
child 34963 366a1a44aac2
HOLogic.strip_psplits: types are ordered after syntactic appearance, not after corresponding de-Bruin index (closer correspondence to similar strip operations)
NEWS
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/hologic.ML
src/HOL/Tools/inductive_codegen.ML
     1.1 --- a/NEWS	Fri Jan 22 13:39:00 2010 +0100
     1.2 +++ b/NEWS	Fri Jan 22 16:56:51 2010 +0100
     1.3 @@ -12,6 +12,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* HOLogic.strip_psplit: types are returned in syntactic order, similar
     1.8 +to other strip and tuple operations.  INCOMPATIBILITY.
     1.9 +
    1.10  * Various old-style primrec specifications in the HOL theories have been
    1.11  replaced by new-style primrec, especially in theory List.  The corresponding
    1.12  constants now have authentic syntax.  INCOMPATIBILITY.
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Jan 22 13:39:00 2010 +0100
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Fri Jan 22 16:56:51 2010 +0100
     2.3 @@ -2562,9 +2562,9 @@
     2.4      val t_eval = if null outargs then t_pred else
     2.5        let
     2.6          val outargs_bounds = map (fn Bound i => i) outargs;
     2.7 -        val outargsTs = map (nth Ts) outargs_bounds;
     2.8 +        val outargsTs = map (fn i => nth Ts (length Ts - i - 1)) outargs_bounds;
     2.9          val T_pred = HOLogic.mk_tupleT outargsTs;
    2.10 -        val T_compr = HOLogic.mk_ptupleT fp (rev Ts);
    2.11 +        val T_compr = HOLogic.mk_ptupleT fp Ts;
    2.12          val k = length outargs - 1;
    2.13          val arrange_bounds = map_index (fn (i, j) => (k-i, k-j)) outargs_bounds
    2.14            |> sort (prod_ord (K EQUAL) int_ord)
     3.1 --- a/src/HOL/Tools/hologic.ML	Fri Jan 22 13:39:00 2010 +0100
     3.2 +++ b/src/HOL/Tools/hologic.ML	Fri Jan 22 16:56:51 2010 +0100
     3.3 @@ -426,7 +426,7 @@
     3.4  
     3.5  val strip_psplits =
     3.6    let
     3.7 -    fun strip [] qs Ts t = (t, Ts, qs)
     3.8 +    fun strip [] qs Ts t = (t, rev Ts, qs)
     3.9        | strip (p :: ps) qs Ts (Const ("split", _) $ t) =
    3.10            strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) Ts t
    3.11        | strip (p :: ps) qs Ts (Abs (s, T, t)) = strip ps qs (T :: Ts) t
     4.1 --- a/src/HOL/Tools/inductive_codegen.ML	Fri Jan 22 13:39:00 2010 +0100
     4.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Fri Jan 22 16:56:51 2010 +0100
     4.3 @@ -724,7 +724,7 @@
     4.4                  let
     4.5                    val (ts1, ts2) = chop k ts;
     4.6                    val ts2' = map
     4.7 -                    (fn Bound i => Term.dummy_pattern (nth Ts i) | t => t) ts2;
     4.8 +                    (fn Bound i => Term.dummy_pattern (nth Ts (length Ts - i - 1)) | t => t) ts2;
     4.9                    val (ots, its) = List.partition is_Bound ts2;
    4.10                    val no_loose = forall (fn t => not (loose_bvar (t, 0)))
    4.11                  in