fixed situation in 'primrec' whereby the original value of a constructor argument of nested type was not translated correctly to a 'map fst'
authorblanchet
Thu Sep 11 18:54:36 2014 +0200 (2014-09-11)
changeset 58301de95aeedf49e
parent 58300 055afb5f7df8
child 58302 c59f6a31001e
fixed situation in 'primrec' whereby the original value of a constructor argument of nested type was not translated correctly to a 'map fst'
src/HOL/Library/RBT_Set.thy
src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
     1.1 --- a/src/HOL/Library/RBT_Set.thy	Thu Sep 11 18:54:36 2014 +0200
     1.2 +++ b/src/HOL/Library/RBT_Set.thy	Thu Sep 11 18:54:36 2014 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5  (*
     1.6    Users should be aware that by including this file all code equations
     1.7 -  outside of List.thy using 'a list as an implenentation of sets cannot be
     1.8 +  outside of List.thy using 'a list as an implementation of sets cannot be
     1.9    used for code generation. If such equations are not needed, they can be
    1.10    deleted from the code generator. Otherwise, a user has to provide their 
    1.11    own equations using RBT trees. 
     2.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Thu Sep 11 18:54:36 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Thu Sep 11 18:54:36 2014 +0200
     2.3 @@ -296,25 +296,27 @@
     2.4  
     2.5      fun subst bound_Ts (t as g' $ y) =
     2.6          let
     2.7 -          fun subst_rec () = subst bound_Ts g' $ subst bound_Ts y;
     2.8 +          fun subst_rec (h $ z) = subst bound_Ts h $ subst bound_Ts z
     2.9 +            | subst_rec t = t;
    2.10 +
    2.11            val y_head = head_of y;
    2.12          in
    2.13            if not (member (op =) ctr_args y_head) then
    2.14 -            subst_rec ()
    2.15 +            subst_rec t
    2.16            else
    2.17              (case try_nested_rec bound_Ts y_head t of
    2.18 -              SOME t' => t'
    2.19 +              SOME t' => subst_rec t'
    2.20              | NONE =>
    2.21                let val (g, g_args) = strip_comb g' in
    2.22                  (case try (get_ctr_pos o fst o dest_Free) g of
    2.23 -                  SOME ~1 => subst_rec ()
    2.24 +                  SOME ~1 => subst_rec t
    2.25                  | SOME ctr_pos =>
    2.26                    (length g_args >= ctr_pos orelse
    2.27                     raise PRIMREC ("too few arguments in recursive call", [t]);
    2.28                     (case AList.lookup (op =) mutual_calls y of
    2.29                       SOME y' => list_comb (y', g_args)
    2.30 -                   | NONE => subst_rec ()))
    2.31 -                | NONE => subst_rec ())
    2.32 +                   | NONE => subst_rec t))
    2.33 +                | NONE => subst_rec t)
    2.34                end)
    2.35          end
    2.36        | subst bound_Ts (Abs (v, T, b)) = Abs (v, T, subst (T :: bound_Ts) b)