more direct use of binder_types/body_type;
authorwenzelm
Wed Dec 01 15:03:44 2010 +0100 (2010-12-01)
changeset 408445895c525739d
parent 40843 b254814a094c
child 40845 15b97bd4b5c0
more direct use of binder_types/body_type;
src/CCL/CCL.thy
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Tools/Datatype/datatype_codegen.ML
src/HOL/Tools/Datatype/datatype_data.ML
src/HOL/Tools/Datatype/datatype_prop.ML
src/HOL/Tools/Datatype/datatype_realizer.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/recfun_codegen.ML
src/HOL/Tools/record.ML
src/Pure/Isar/code.ML
src/Pure/Proof/extraction.ML
src/Pure/codegen.ML
src/Pure/term.ML
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/CCL/CCL.thy	Wed Dec 01 15:02:39 2010 +0100
     1.2 +++ b/src/CCL/CCL.thy	Wed Dec 01 15:03:44 2010 +0100
     1.3 @@ -233,7 +233,7 @@
     1.4           | arg_str 1 a s = "(" ^ a ^ "a" ^ s ^ ")"
     1.5           | arg_str n a s = arg_str (n-1) a ("," ^ a ^ (chr((ord "a")+n-1)) ^ s)
     1.6             val T = Sign.the_const_type thy (Sign.intern_const thy sy);
     1.7 -           val arity = length (fst (strip_type T))
     1.8 +           val arity = length (binder_types T)
     1.9         in sy ^ (arg_str arity name "") end
    1.10  
    1.11    fun mk_thm_str thy a b = "~ " ^ (saturate thy a "a") ^ " = " ^ (saturate thy b "b")
     2.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Wed Dec 01 15:02:39 2010 +0100
     2.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Dec 01 15:03:44 2010 +0100
     2.3 @@ -274,7 +274,7 @@
     2.4            fun perm_arg (dt, x) =
     2.5              let val T = type_of x
     2.6              in if is_rec_type dt then
     2.7 -                let val (Us, _) = strip_type T
     2.8 +                let val Us = binder_types T
     2.9                  in list_abs (map (pair "x") Us,
    2.10                    Free (nth perm_names_types' (body_index dt)) $ pi $
    2.11                      list_comb (x, map (fn (i, U) =>
     3.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Wed Dec 01 15:02:39 2010 +0100
     3.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Wed Dec 01 15:03:44 2010 +0100
     3.3 @@ -334,14 +334,14 @@
     3.4          val t :: ts2 = drop i ts;
     3.5          val names = List.foldr OldTerm.add_term_names
     3.6            (map (fst o fst o dest_Var) (List.foldr OldTerm.add_term_vars [] ts1)) ts1;
     3.7 -        val (Ts, dT) = split_last (take (i+1) (fst (strip_type T)));
     3.8 +        val (Ts, dT) = split_last (take (i+1) (binder_types T));
     3.9  
    3.10          fun pcase [] [] [] gr = ([], gr)
    3.11            | pcase ((cname, cargs)::cs) (t::ts) (U::Us) gr =
    3.12                let
    3.13                  val j = length cargs;
    3.14                  val xs = Name.variant_list names (replicate j "x");
    3.15 -                val Us' = take j (fst (strip_type U));
    3.16 +                val Us' = take j (binder_types U);
    3.17                  val frees = map2 (curry Free) xs Us';
    3.18                  val (cp, gr0) = invoke_codegen thy defs dep module false
    3.19                    (list_comb (Const (cname, Us' ---> dT), frees)) gr;
    3.20 @@ -385,26 +385,33 @@
    3.21  
    3.22  (* code generators for terms and types *)
    3.23  
    3.24 -fun datatype_codegen thy defs dep module brack t gr = (case strip_comb t of
    3.25 -   (c as Const (s, T), ts) =>
    3.26 -     (case Datatype_Data.info_of_case thy s of
    3.27 +fun datatype_codegen thy defs dep module brack t gr =
    3.28 +  (case strip_comb t of
    3.29 +    (c as Const (s, T), ts) =>
    3.30 +      (case Datatype_Data.info_of_case thy s of
    3.31          SOME {index, descr, ...} =>
    3.32 -          if is_some (get_assoc_code thy (s, T)) then NONE else
    3.33 -          SOME (pretty_case thy defs dep module brack
    3.34 -            (#3 (the (AList.lookup op = descr index))) c ts gr )
    3.35 -      | NONE => case (Datatype_Data.info_of_constr thy (s, T), strip_type T) of
    3.36 -        (SOME {index, descr, ...}, (_, U as Type (tyname, _))) =>
    3.37 -          if is_some (get_assoc_code thy (s, T)) then NONE else
    3.38 -          let
    3.39 -            val SOME (tyname', _, constrs) = AList.lookup op = descr index;
    3.40 -            val SOME args = AList.lookup op = constrs s
    3.41 -          in
    3.42 -            if tyname <> tyname' then NONE
    3.43 -            else SOME (pretty_constr thy defs
    3.44 -              dep module brack args c ts (snd (invoke_tycodegen thy defs dep module false U gr)))
    3.45 -          end
    3.46 -      | _ => NONE)
    3.47 - | _ => NONE);
    3.48 +          if is_some (get_assoc_code thy (s, T)) then NONE
    3.49 +          else
    3.50 +            SOME (pretty_case thy defs dep module brack
    3.51 +              (#3 (the (AList.lookup op = descr index))) c ts gr)
    3.52 +      | NONE =>
    3.53 +          (case (Datatype_Data.info_of_constr thy (s, T), body_type T) of
    3.54 +            (SOME {index, descr, ...}, U as Type (tyname, _)) =>
    3.55 +              if is_some (get_assoc_code thy (s, T)) then NONE
    3.56 +              else
    3.57 +                let
    3.58 +                  val SOME (tyname', _, constrs) = AList.lookup op = descr index;
    3.59 +                  val SOME args = AList.lookup op = constrs s;
    3.60 +                in
    3.61 +                  if tyname <> tyname' then NONE
    3.62 +                  else
    3.63 +                    SOME
    3.64 +                      (pretty_constr thy defs
    3.65 +                        dep module brack args c ts
    3.66 +                        (snd (invoke_tycodegen thy defs dep module false U gr)))
    3.67 +                end
    3.68 +          | _ => NONE))
    3.69 +  | _ => NONE);
    3.70  
    3.71  fun datatype_tycodegen thy defs dep module brack (Type (s, Ts)) gr =
    3.72        (case Datatype_Data.get_info thy s of
     4.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Wed Dec 01 15:02:39 2010 +0100
     4.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Wed Dec 01 15:03:44 2010 +0100
     4.3 @@ -72,7 +72,7 @@
     4.4  fun info_of_constr thy (c, T) =
     4.5    let
     4.6      val tab = Symtab.lookup_list ((#constrs o DatatypesData.get) thy) c;
     4.7 -    val hint = case strip_type T of (_, Type (tyco, _)) => SOME tyco | _ => NONE;
     4.8 +    val hint = case body_type T of Type (tyco, _) => SOME tyco | _ => NONE;
     4.9      val default = if null tab then NONE
    4.10        else SOME (snd (Library.last_elem tab))
    4.11          (*conservative wrt. overloaded constructors*);
    4.12 @@ -387,7 +387,7 @@
    4.13      fun type_of_constr (cT as (_, T)) =
    4.14        let
    4.15          val frees = OldTerm.typ_tfrees T;
    4.16 -        val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) T
    4.17 +        val (tyco, vs) = (apsnd o map) dest_TFree (dest_Type (body_type T))
    4.18            handle TYPE _ => no_constr cT
    4.19          val _ = if has_duplicates (eq_fst (op =)) vs then no_constr cT else ();
    4.20          val _ = if length frees <> length vs then no_constr cT else ();
    4.21 @@ -412,8 +412,8 @@
    4.22        (TFree o (the o AList.lookup (op =) (map fst raw_vs ~~ vs)) o fst o dest_TFree) T);
    4.23  
    4.24      val cs = map (apsnd (map norm_constr)) raw_cs;
    4.25 -    val dtyps_of_typ = map (dtyp_of_typ (map (rpair (map fst vs) o fst) cs))
    4.26 -      o fst o strip_type;
    4.27 +    val dtyps_of_typ =
    4.28 +      map (dtyp_of_typ (map (rpair (map fst vs) o fst) cs)) o binder_types;
    4.29      val dt_names = map fst cs;
    4.30  
    4.31      fun mk_spec (i, (tyco, constr)) = (i, (tyco,
     5.1 --- a/src/HOL/Tools/Datatype/datatype_prop.ML	Wed Dec 01 15:02:39 2010 +0100
     5.2 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML	Wed Dec 01 15:03:44 2010 +0100
     5.3 @@ -385,7 +385,7 @@
     5.4  
     5.5          fun mk_clause ((f, g), (cname, _)) =
     5.6            let
     5.7 -            val (Ts, _) = strip_type (fastype_of f);
     5.8 +            val Ts = binder_types (fastype_of f);
     5.9              val tnames = Name.variant_list used (make_tnames Ts);
    5.10              val frees = map Free (tnames ~~ Ts)
    5.11            in
     6.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Wed Dec 01 15:02:39 2010 +0100
     6.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Wed Dec 01 15:03:44 2010 +0100
     6.3 @@ -25,7 +25,7 @@
     6.4  fun prf_of thm =
     6.5    Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
     6.6  
     6.7 -fun is_unit t = snd (strip_type (fastype_of t)) = HOLogic.unitT;
     6.8 +fun is_unit t = body_type (fastype_of t) = HOLogic.unitT;
     6.9  
    6.10  fun tname_of (Type (s, _)) = s
    6.11    | tname_of _ = "";
     7.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Dec 01 15:02:39 2010 +0100
     7.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Dec 01 15:03:44 2010 +0100
     7.3 @@ -485,7 +485,7 @@
     7.4  
     7.5  fun is_pred thy constname = (body_type (Sign.the_const_type thy constname) = HOLogic.boolT);
     7.6  
     7.7 -fun is_predT (T as Type("fun", [_, _])) = (snd (strip_type T) = @{typ bool})
     7.8 +fun is_predT (T as Type("fun", [_, _])) = (body_type T = @{typ bool})
     7.9    | is_predT _ = false
    7.10  
    7.11  (*** check if a term contains only constructor functions ***)
     8.1 --- a/src/HOL/Tools/recfun_codegen.ML	Wed Dec 01 15:02:39 2010 +0100
     8.2 +++ b/src/HOL/Tools/recfun_codegen.ML	Wed Dec 01 15:03:44 2010 +0100
     8.3 @@ -34,7 +34,8 @@
     8.4  
     8.5  fun avoid_value thy [thm] =
     8.6        let val (_, T) = Code.const_typ_eqn thy thm
     8.7 -      in if null (Term.add_tvarsT T []) orelse (null o fst o strip_type) T
     8.8 +      in
     8.9 +        if null (Term.add_tvarsT T []) orelse null (binder_types T)
    8.10          then [thm]
    8.11          else [Code.expand_eta thy 1 thm]
    8.12        end
     9.1 --- a/src/HOL/Tools/record.ML	Wed Dec 01 15:02:39 2010 +0100
     9.2 +++ b/src/HOL/Tools/record.ML	Wed Dec 01 15:03:44 2010 +0100
     9.3 @@ -1869,7 +1869,7 @@
     9.4           (fn _ => fn eq_def => tac eq_def) eq_def)
     9.5      |-> (fn eq_def => fn thy => thy |> Code.del_eqn eq_def |> Code.add_default_eqn (mk_eq thy eq_def))
     9.6      |> (fn thy => Code.add_nbe_default_eqn (mk_eq_refl thy) thy)
     9.7 -    |> ensure_random_record ext_tyco vs (fst ext) ((fst o strip_type o snd) ext)
     9.8 +    |> ensure_random_record ext_tyco vs (fst ext) (binder_types (snd ext))
     9.9    end;
    9.10  
    9.11  
    10.1 --- a/src/Pure/Isar/code.ML	Wed Dec 01 15:02:39 2010 +0100
    10.2 +++ b/src/Pure/Isar/code.ML	Wed Dec 01 15:03:44 2010 +0100
    10.3 @@ -358,7 +358,7 @@
    10.4   of SOME ty => ty
    10.5    | NONE => (Type.strip_sorts o Sign.the_const_type thy) c;
    10.6  
    10.7 -fun args_number thy = length o fst o strip_type o const_typ thy;
    10.8 +fun args_number thy = length o binder_types o const_typ thy;
    10.9  
   10.10  fun subst_signature thy c ty =
   10.11    let
   10.12 @@ -391,7 +391,7 @@
   10.13      fun last_typ c_ty ty =
   10.14        let
   10.15          val tfrees = Term.add_tfreesT ty [];
   10.16 -        val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) ty
   10.17 +        val (tyco, vs) = (apsnd o map) dest_TFree (dest_Type (body_type ty))
   10.18            handle TYPE _ => no_constr thy "bad type" c_ty
   10.19          val _ = if tyco = "fun" then no_constr thy "bad type" c_ty else ();
   10.20          val _ = if has_duplicates (eq_fst (op =)) vs
   10.21 @@ -420,7 +420,7 @@
   10.22          val the_v = the o AList.lookup (op =) (vs ~~ vs');
   10.23          val ty' = map_type_tfree (fn (v, _) => TFree (the_v v)) ty;
   10.24          val (vs'', _) = logical_typscheme thy (c, ty');
   10.25 -      in (c, (vs'', (fst o strip_type) ty')) end;
   10.26 +      in (c, (vs'', binder_types ty')) end;
   10.27      val c' :: cs' = map (analyze_constructor thy) cs;
   10.28      val ((tyco, sorts), cs'') = fold add cs' (apsnd single c');
   10.29      val vs = Name.names Name.context Name.aT sorts;
   10.30 @@ -444,7 +444,7 @@
   10.31    | _ => error ("Not an abstract type: " ^ tyco);
   10.32   
   10.33  fun get_type_of_constr_or_abstr thy c =
   10.34 -  case (snd o strip_type o const_typ thy) c
   10.35 +  case (body_type o const_typ thy) c
   10.36     of Type (tyco, _) => let val ((_, cos), abstract) = get_type thy tyco
   10.37          in if member (op =) (map fst cos) c then SOME (tyco, abstract) else NONE end
   10.38      | _ => NONE;
   10.39 @@ -517,7 +517,7 @@
   10.40        | check n (Const (c_ty as (c, ty))) =
   10.41            if allow_pats then let
   10.42              val c' = AxClass.unoverload_const thy c_ty
   10.43 -          in if n = (length o fst o strip_type o subst_signature thy c') ty
   10.44 +          in if n = (length o binder_types o subst_signature thy c') ty
   10.45              then if allow_consts orelse is_constr thy c'
   10.46                then ()
   10.47                else bad (quote c ^ " is not a constructor, on left hand side of equation")
   10.48 @@ -1139,7 +1139,7 @@
   10.49      val (zs, _) = Name.variants (replicate (num_args - 1) "") ctxt;
   10.50      val (ws, vs) = chop pos zs;
   10.51      val T = Logic.unvarifyT_global (Sign.the_const_type thy case_const);
   10.52 -    val Ts = (fst o strip_type) T;
   10.53 +    val Ts = binder_types T;
   10.54      val T_cong = nth Ts pos;
   10.55      fun mk_prem z = Free (z, T_cong);
   10.56      fun mk_concl z = list_comb (Const (case_const, T), map2 (curry Free) (ws @ z :: vs) Ts);
    11.1 --- a/src/Pure/Proof/extraction.ML	Wed Dec 01 15:02:39 2010 +0100
    11.2 +++ b/src/Pure/Proof/extraction.ML	Wed Dec 01 15:03:44 2010 +0100
    11.3 @@ -135,11 +135,13 @@
    11.4  
    11.5  val prf_subst_TVars = Proofterm.map_proof_types o typ_subst_TVars;
    11.6  
    11.7 -fun relevant_vars types prop = List.foldr (fn
    11.8 -      (Var ((a, _), T), vs) => (case strip_type T of
    11.9 -        (_, Type (s, _)) => if member (op =) types s then a :: vs else vs
   11.10 -      | _ => vs)
   11.11 -    | (_, vs) => vs) [] (vars_of prop);
   11.12 +fun relevant_vars types prop =
   11.13 +  List.foldr
   11.14 +    (fn (Var ((a, _), T), vs) =>
   11.15 +        (case body_type T of
   11.16 +          Type (s, _) => if member (op =) types s then a :: vs else vs
   11.17 +        | _ => vs)
   11.18 +      | (_, vs) => vs) [] (vars_of prop);
   11.19  
   11.20  fun tname_of (Type (s, _)) = s
   11.21    | tname_of _ = "";
    12.1 --- a/src/Pure/codegen.ML	Wed Dec 01 15:02:39 2010 +0100
    12.2 +++ b/src/Pure/codegen.ML	Wed Dec 01 15:03:44 2010 +0100
    12.3 @@ -664,7 +664,7 @@
    12.4                   NONE =>
    12.5                     let
    12.6                       val _ = message ("expanding definition of " ^ s);
    12.7 -                     val (Ts, _) = strip_type U;
    12.8 +                     val Ts = binder_types U;
    12.9                       val (args', rhs') =
   12.10                         if not (null args) orelse null Ts then (args, rhs) else
   12.11                           let val v = Free (new_name rhs "x", hd Ts)
    13.1 --- a/src/Pure/term.ML	Wed Dec 01 15:02:39 2010 +0100
    13.2 +++ b/src/Pure/term.ML	Wed Dec 01 15:03:44 2010 +0100
    13.3 @@ -712,7 +712,7 @@
    13.4              val (vs, t') = expand_eta Ts (t $ Free (v, T)) used';
    13.5            in ((v, T) :: vs, t') end;
    13.6      val ((vs1, t'), (k', used')) = strip_abs t (k, used);
    13.7 -    val Ts = (fst o chop k' o fst o strip_type o fastype_of) t';
    13.8 +    val Ts = fst (chop k' (binder_types (fastype_of t')));
    13.9      val (vs2, t'') = expand_eta Ts t' used';
   13.10    in (vs1 @ vs2, t'') end;
   13.11  
    14.1 --- a/src/Tools/Code/code_thingol.ML	Wed Dec 01 15:02:39 2010 +0100
    14.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Dec 01 15:03:44 2010 +0100
    14.3 @@ -710,7 +710,7 @@
    14.4        else ()
    14.5      val arg_typs = Sign.const_typargs thy (c, ty);
    14.6      val sorts = Code_Preproc.sortargs eqngr c;
    14.7 -    val function_typs = (fst o Term.strip_type) ty;
    14.8 +    val function_typs = Term.binder_types ty;
    14.9    in
   14.10      ensure_const thy algbr eqngr permissive c
   14.11      ##>> fold_map (translate_typ thy algbr eqngr permissive) arg_typs
   14.12 @@ -724,7 +724,7 @@
   14.13    #>> (fn (t, ts) => t `$$ ts)
   14.14  and translate_case thy algbr eqngr permissive some_thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
   14.15    let
   14.16 -    fun arg_types num_args ty = (fst o chop num_args o fst o strip_type) ty;
   14.17 +    fun arg_types num_args ty = fst (chop num_args (binder_types ty));
   14.18      val tys = arg_types num_args (snd c_ty);
   14.19      val ty = nth tys t_pos;
   14.20      fun mk_constr c t = let val n = Code.args_number thy c