dropped dead code
authorhaftmann
Thu Apr 19 19:18:11 2012 +0200 (2012-04-19)
changeset 47609b3dab1892cda
parent 47608 572d7e51de4d
child 47610 261f9de35b18
dropped dead code
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_runtime.ML
src/Tools/Code/code_scala.ML
src/Tools/nbe.ML
src/Tools/quickcheck.ML
     1.1 --- a/src/Tools/Code/code_haskell.ML	Thu Apr 19 18:24:40 2012 +0200
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Thu Apr 19 19:18:11 2012 +0200
     1.3 @@ -34,7 +34,7 @@
     1.4  
     1.5  (** Haskell serializer **)
     1.6  
     1.7 -fun print_haskell_stmt labelled_name class_syntax tyco_syntax const_syntax
     1.8 +fun print_haskell_stmt class_syntax tyco_syntax const_syntax
     1.9      reserved deresolve deriving_show =
    1.10    let
    1.11      fun class_name class = case class_syntax class
    1.12 @@ -52,9 +52,9 @@
    1.13            (map (str o lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
    1.14      fun print_tyco_expr tyvars fxy (tyco, tys) =
    1.15        brackify fxy (str tyco :: map (print_typ tyvars BR) tys)
    1.16 -    and print_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case tyco_syntax tyco
    1.17 +    and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco
    1.18           of NONE => print_tyco_expr tyvars fxy (deresolve tyco, tys)
    1.19 -          | SOME (i, print) => print (print_typ tyvars) fxy tys)
    1.20 +          | SOME (_, print) => print (print_typ tyvars) fxy tys)
    1.21        | print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
    1.22      fun print_typdecl tyvars (vs, tycoexpr) =
    1.23        Pretty.block (print_typcontext tyvars vs @| print_tyco_expr tyvars NOBR tycoexpr);
    1.24 @@ -101,7 +101,7 @@
    1.25      and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
    1.26            let
    1.27              val (binds, body) = Code_Thingol.unfold_let (ICase cases);
    1.28 -            fun print_match ((pat, ty), t) vars =
    1.29 +            fun print_match ((pat, _), t) vars =
    1.30                vars
    1.31                |> print_bind tyvars some_thm BR pat
    1.32                |>> (fn p => semicolon [p, str "=", print_term tyvars some_thm vars NOBR t])
    1.33 @@ -325,7 +325,7 @@
    1.34                andalso forall (deriv' tycos) tys
    1.35            | deriv' _ (ITyVar _) = true
    1.36        in deriv [] tyco end;
    1.37 -    fun print_stmt deresolve = print_haskell_stmt labelled_name
    1.38 +    fun print_stmt deresolve = print_haskell_stmt
    1.39        class_syntax tyco_syntax const_syntax (make_vars reserved)
    1.40        deresolve (if string_classes then deriving_show else K false);
    1.41  
     2.1 --- a/src/Tools/Code/code_ml.ML	Thu Apr 19 18:24:40 2012 +0200
     2.2 +++ b/src/Tools/Code/code_ml.ML	Thu Apr 19 19:18:11 2012 +0200
     2.3 @@ -39,9 +39,6 @@
     2.4    | ML_Datas of (string * ((vname * sort) list * ((string * vname list) * itype list) list)) list
     2.5    | ML_Class of string * (vname * ((class * string) list * (string * itype) list));
     2.6  
     2.7 -fun stmt_name_of_binding (ML_Function (name, _)) = name
     2.8 -  | stmt_name_of_binding (ML_Instance (name, _)) = name;
     2.9 -
    2.10  fun print_product _ [] = NONE
    2.11    | print_product print [x] = SOME (print x)
    2.12    | print_product print xs = (SOME o enum " *" "" "") (map print xs);
    2.13 @@ -55,16 +52,16 @@
    2.14  
    2.15  fun print_sml_stmt tyco_syntax const_syntax reserved is_cons deresolve =
    2.16    let
    2.17 -    fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco
    2.18 -      | print_tyco_expr fxy (tyco, [ty]) =
    2.19 +    fun print_tyco_expr (tyco, []) = (str o deresolve) tyco
    2.20 +      | print_tyco_expr (tyco, [ty]) =
    2.21            concat [print_typ BR ty, (str o deresolve) tyco]
    2.22 -      | print_tyco_expr fxy (tyco, tys) =
    2.23 +      | print_tyco_expr (tyco, tys) =
    2.24            concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
    2.25      and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
    2.26 -         of NONE => print_tyco_expr fxy (tyco, tys)
    2.27 -          | SOME (i, print) => print print_typ fxy tys)
    2.28 +         of NONE => print_tyco_expr (tyco, tys)
    2.29 +          | SOME (_, print) => print print_typ fxy tys)
    2.30        | print_typ fxy (ITyVar v) = str ("'" ^ v);
    2.31 -    fun print_dicttyp (class, ty) = print_tyco_expr NOBR (class, [ty]);
    2.32 +    fun print_dicttyp (class, ty) = print_tyco_expr (class, [ty]);
    2.33      fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
    2.34        (map_filter (fn (v, sort) =>
    2.35          (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
    2.36 @@ -129,7 +126,7 @@
    2.37      and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
    2.38            let
    2.39              val (binds, body) = Code_Thingol.unfold_let (ICase cases);
    2.40 -            fun print_match ((pat, ty), t) vars =
    2.41 +            fun print_match ((pat, _), t) vars =
    2.42                vars
    2.43                |> print_bind is_pseudo_fun some_thm NOBR pat
    2.44                |>> (fn p => semicolon [str "val", p, str "=",
    2.45 @@ -170,7 +167,7 @@
    2.46        in
    2.47          concat (
    2.48            str definer
    2.49 -          :: print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs)
    2.50 +          :: print_tyco_expr (tyco, map (ITyVar o fst) vs)
    2.51            :: str "="
    2.52            :: separate (str "|") (map print_co cos)
    2.53          )
    2.54 @@ -236,7 +233,7 @@
    2.55                  (map print_super_instance super_instances
    2.56                    @ map print_classparam_instance classparam_instances)
    2.57                :: str ":"
    2.58 -              @@ print_tyco_expr NOBR (class, [tyco `%% map (ITyVar o fst) vs])
    2.59 +              @@ print_tyco_expr (class, [tyco `%% map (ITyVar o fst) vs])
    2.60              ))
    2.61            end;
    2.62      fun print_stmt (ML_Exc (name, (vs_ty, n))) = pair
    2.63 @@ -276,7 +273,7 @@
    2.64            end
    2.65       | print_stmt (ML_Datas [(tyco, (vs, []))]) =
    2.66            let
    2.67 -            val ty_p = print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs);
    2.68 +            val ty_p = print_tyco_expr (tyco, map (ITyVar o fst) vs);
    2.69            in
    2.70              pair
    2.71              [concat [str "type", ty_p]]
    2.72 @@ -359,16 +356,16 @@
    2.73  
    2.74  fun print_ocaml_stmt tyco_syntax const_syntax reserved is_cons deresolve =
    2.75    let
    2.76 -    fun print_tyco_expr fxy (tyco, []) = (str o deresolve) tyco
    2.77 -      | print_tyco_expr fxy (tyco, [ty]) =
    2.78 +    fun print_tyco_expr (tyco, []) = (str o deresolve) tyco
    2.79 +      | print_tyco_expr (tyco, [ty]) =
    2.80            concat [print_typ BR ty, (str o deresolve) tyco]
    2.81 -      | print_tyco_expr fxy (tyco, tys) =
    2.82 +      | print_tyco_expr (tyco, tys) =
    2.83            concat [enum "," "(" ")" (map (print_typ BR) tys), (str o deresolve) tyco]
    2.84      and print_typ fxy (tyco `%% tys) = (case tyco_syntax tyco
    2.85 -         of NONE => print_tyco_expr fxy (tyco, tys)
    2.86 +         of NONE => print_tyco_expr (tyco, tys)
    2.87            | SOME (_, print) => print print_typ fxy tys)
    2.88        | print_typ fxy (ITyVar v) = str ("'" ^ v);
    2.89 -    fun print_dicttyp (class, ty) = print_tyco_expr NOBR (class, [ty]);
    2.90 +    fun print_dicttyp (class, ty) = print_tyco_expr (class, [ty]);
    2.91      fun print_typscheme_prefix (vs, p) = enum " ->" "" ""
    2.92        (map_filter (fn (v, sort) =>
    2.93          (print_product (fn class => print_dicttyp (class, ITyVar v)) sort)) vs @| p);
    2.94 @@ -465,7 +462,7 @@
    2.95        in
    2.96          concat (
    2.97            str definer
    2.98 -          :: print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs)
    2.99 +          :: print_tyco_expr (tyco, map (ITyVar o fst) vs)
   2.100            :: str "="
   2.101            :: separate (str "|") (map print_co cos)
   2.102          )
   2.103 @@ -576,7 +573,7 @@
   2.104                  enum_default "()" ";" "{" "}" (map print_super_instance super_instances
   2.105                    @ map print_classparam_instance classparam_instances),
   2.106                  str ":",
   2.107 -                print_tyco_expr NOBR (class, [tyco `%% map (ITyVar o fst) vs])
   2.108 +                print_tyco_expr (class, [tyco `%% map (ITyVar o fst) vs])
   2.109                ]
   2.110              ))
   2.111            end;
   2.112 @@ -616,7 +613,7 @@
   2.113            end
   2.114       | print_stmt (ML_Datas [(tyco, (vs, []))]) =
   2.115            let
   2.116 -            val ty_p = print_tyco_expr NOBR (tyco, map (ITyVar o fst) vs);
   2.117 +            val ty_p = print_tyco_expr (tyco, map (ITyVar o fst) vs);
   2.118            in
   2.119              pair
   2.120              [concat [str "type", ty_p]]
     3.1 --- a/src/Tools/Code/code_runtime.ML	Thu Apr 19 18:24:40 2012 +0200
     3.2 +++ b/src/Tools/Code/code_runtime.ML	Thu Apr 19 19:18:11 2012 +0200
     3.3 @@ -149,7 +149,7 @@
     3.4  
     3.5  local
     3.6  
     3.7 -fun check_holds thy evaluator vs_t deps ct =
     3.8 +fun check_holds thy evaluator vs_t ct =
     3.9    let
    3.10      val t = Thm.term_of ct;
    3.11      val _ = if fastype_of t <> propT
    3.12 @@ -165,10 +165,10 @@
    3.13  
    3.14  val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result
    3.15    (Thm.add_oracle (@{binding holds_by_evaluation},
    3.16 -  fn (thy, evaluator, vs_t, deps, ct) => check_holds thy evaluator vs_t deps ct)));
    3.17 +  fn (thy, evaluator, vs_t, ct) => check_holds thy evaluator vs_t ct)));
    3.18  
    3.19  fun check_holds_oracle thy evaluator ((_, vs_ty), t) deps ct =
    3.20 -  raw_check_holds_oracle (thy, evaluator, (vs_ty, t), deps, ct);
    3.21 +  raw_check_holds_oracle (thy, evaluator, (vs_ty, t), ct);
    3.22  
    3.23  in
    3.24  
     4.1 --- a/src/Tools/Code/code_scala.ML	Thu Apr 19 18:24:40 2012 +0200
     4.2 +++ b/src/Tools/Code/code_scala.ML	Thu Apr 19 19:18:11 2012 +0200
     4.3 @@ -24,7 +24,7 @@
     4.4  
     4.5  (** Scala serializer **)
     4.6  
     4.7 -fun print_scala_stmt labelled_name tyco_syntax const_syntax reserved
     4.8 +fun print_scala_stmt tyco_syntax const_syntax reserved
     4.9      args_num is_singleton_constr (deresolve, deresolve_full) =
    4.10    let
    4.11      fun lookup_tyvar tyvars = lookup_var tyvars o first_upper;
    4.12 @@ -33,7 +33,7 @@
    4.13            (print_typ tyvars NOBR) fxy ((str o deresolve) tyco) tys
    4.14      and print_typ tyvars fxy (tyco `%% tys) = (case tyco_syntax tyco
    4.15           of NONE => print_tyco_expr tyvars fxy (tyco, tys)
    4.16 -          | SOME (i, print) => print (print_typ tyvars) fxy tys)
    4.17 +          | SOME (_, print) => print (print_typ tyvars) fxy tys)
    4.18        | print_typ tyvars fxy (ITyVar v) = (str o lookup_tyvar tyvars) v;
    4.19      fun print_dicttyp tyvars (class, ty) = print_tyco_expr tyvars NOBR (class, [ty]);
    4.20      fun print_tupled_typ tyvars ([], ty) =
    4.21 @@ -362,7 +362,7 @@
    4.22      fun is_singleton_constr c = case Graph.get_node program c
    4.23       of Code_Thingol.Datatypecons (_, tyco) => null (lookup_constr tyco c)
    4.24        | _ => false;
    4.25 -    fun print_stmt prefix_fragments = print_scala_stmt labelled_name
    4.26 +    fun print_stmt prefix_fragments = print_scala_stmt
    4.27        tyco_syntax const_syntax (make_vars reserved_syms) args_num
    4.28        is_singleton_constr (deresolver prefix_fragments, deresolver []);
    4.29  
     5.1 --- a/src/Tools/nbe.ML	Thu Apr 19 18:24:40 2012 +0200
     5.2 +++ b/src/Tools/nbe.ML	Thu Apr 19 19:18:11 2012 +0200
     5.3 @@ -119,7 +119,7 @@
     5.4    in
     5.5      ct
     5.6      |> (Drule.cterm_fun o map_types o map_type_tfree)
     5.7 -        (fn (v, sort) => TFree (v, (fst o the o AList.lookup (op =) vs_tab) v))
     5.8 +        (fn (v, _) => TFree (v, (fst o the o AList.lookup (op =) vs_tab) v))
     5.9      |> conv
    5.10      |> Thm.strip_shyps
    5.11      |> Thm.varifyT_global
    5.12 @@ -240,7 +240,6 @@
    5.13  local
    5.14    val prefix =     "Nbe.";
    5.15    val name_put =   prefix ^ "put_result";
    5.16 -  val name_ref =   prefix ^ "univs_ref";
    5.17    val name_const = prefix ^ "Const";
    5.18    val name_abss =  prefix ^ "abss";
    5.19    val name_apps =  prefix ^ "apps";
     6.1 --- a/src/Tools/quickcheck.ML	Thu Apr 19 18:24:40 2012 +0200
     6.2 +++ b/src/Tools/quickcheck.ML	Thu Apr 19 19:18:11 2012 +0200
     6.3 @@ -390,24 +390,6 @@
     6.4                 Pretty.block [Syntax.pretty_term ctxt t, Pretty.str " =", Pretty.brk 1,
     6.5                   Syntax.pretty_term ctxt u]) (rev eval_terms))));
     6.6  
     6.7 -fun pretty_report (Report {iterations = iterations, raised_match_errors = raised_match_errors,
     6.8 -    satisfied_assms = satisfied_assms, positive_concl_tests = positive_concl_tests}) =
     6.9 -  let
    6.10 -    fun pretty_stat s i = Pretty.block ([Pretty.str (s ^ ": " ^ string_of_int i)])
    6.11 -  in
    6.12 -     ([pretty_stat "iterations" iterations,
    6.13 -     pretty_stat "match exceptions" raised_match_errors]
    6.14 -     @ map_index
    6.15 -       (fn (i, n) => pretty_stat ("satisfied " ^ string_of_int (i + 1) ^ ". assumption") n)
    6.16 -       satisfied_assms
    6.17 -     @ [pretty_stat "positive conclusion tests" positive_concl_tests])
    6.18 -  end
    6.19 -
    6.20 -fun pretty_timings timings =
    6.21 -  Pretty.chunks (Pretty.fbrk :: Pretty.str "timings:" ::
    6.22 -    maps (fn (label, time) =>
    6.23 -      Pretty.str (label ^ ": " ^ string_of_int time ^ " ms") :: Pretty.brk 1 :: []) (rev timings))
    6.24 -
    6.25  (* Isar commands *)
    6.26  
    6.27  fun read_nat s = case (Library.read_int o Symbol.explode) s