reduced the debug output functions from 2 to 1
authorbulwahn
Mon Mar 22 08:30:13 2010 +0100 (2010-03-22)
changeset 35886f5422b736c44
parent 35885 7b39120a1494
child 35887 f704ba9875f6
reduced the debug output functions from 2 to 1
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 22 08:30:13 2010 +0100
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Mar 22 08:30:13 2010 +0100
     1.3 @@ -72,13 +72,9 @@
     1.4  
     1.5  (* debug stuff *)
     1.6  
     1.7 -fun print_tac s = Seq.single;
     1.8 -
     1.9 -fun print_tac' options s = 
    1.10 +fun print_tac options s = 
    1.11    if show_proof_trace options then Tactical.print_tac s else Seq.single;
    1.12  
    1.13 -fun debug_tac msg = Seq.single; (* (fn st => (Output.tracing msg; Seq.single st)); *)
    1.14 -
    1.15  fun assert b = if not b then raise Fail "Assertion failed" else warning "Assertion holds"
    1.16  
    1.17  datatype assertion = Max_number_of_subgoals of int
    1.18 @@ -1932,9 +1928,9 @@
    1.19      | Abs _ => raise Fail "prove_param: No valid parameter term"
    1.20    in
    1.21      REPEAT_DETERM (rtac @{thm ext} 1)
    1.22 -    THEN print_tac' options "prove_param"
    1.23 +    THEN print_tac options "prove_param"
    1.24      THEN f_tac 
    1.25 -    THEN print_tac' options "after prove_param"
    1.26 +    THEN print_tac options "after prove_param"
    1.27      THEN (REPEAT_DETERM (atac 1))
    1.28      THEN (EVERY (map2 (prove_param options thy nargs) ho_args param_derivations))
    1.29      THEN REPEAT_DETERM (rtac @{thm refl} 1)
    1.30 @@ -1949,19 +1945,19 @@
    1.31          val param_derivations = param_derivations_of deriv
    1.32          val ho_args = ho_args_of mode args
    1.33        in
    1.34 -        print_tac' options "before intro rule:"
    1.35 +        print_tac options "before intro rule:"
    1.36          THEN rtac introrule 1
    1.37 -        THEN print_tac' options "after intro rule"
    1.38 +        THEN print_tac options "after intro rule"
    1.39          (* for the right assumption in first position *)
    1.40          THEN rotate_tac premposition 1
    1.41          THEN atac 1
    1.42 -        THEN print_tac' options "parameter goal"
    1.43 +        THEN print_tac options "parameter goal"
    1.44          (* work with parameter arguments *)
    1.45          THEN (EVERY (map2 (prove_param options thy nargs) ho_args param_derivations))
    1.46          THEN (REPEAT_DETERM (atac 1))
    1.47        end
    1.48    | (Free _, _) =>
    1.49 -    print_tac' options "proving parameter call.."
    1.50 +    print_tac options "proving parameter call.."
    1.51      THEN Subgoal.FOCUS_PREMS (fn {context = ctxt, params = params, prems = prems,
    1.52        asms = a, concl = cl, schematics = s} =>
    1.53          let
    1.54 @@ -1978,7 +1974,7 @@
    1.55          in
    1.56            rtac param_prem' 1
    1.57          end) (ProofContext.init thy) 1 (* FIXME: proper context handling *)
    1.58 -    THEN print_tac' options "after prove parameter call"
    1.59 +    THEN print_tac options "after prove parameter call"
    1.60  
    1.61  fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st;
    1.62  
    1.63 @@ -2012,14 +2008,14 @@
    1.64    in
    1.65       (* make this simpset better! *)
    1.66      asm_full_simp_tac (HOL_basic_ss' addsimps simprules) 1
    1.67 -    THEN print_tac' options "after prove_match:"
    1.68 +    THEN print_tac options "after prove_match:"
    1.69      THEN (DETERM (TRY (EqSubst.eqsubst_tac (ProofContext.init thy) [0] [@{thm HOL.if_P}] 1
    1.70             THEN (REPEAT_DETERM (rtac @{thm conjI} 1 THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1))))
    1.71 -           THEN print_tac' options "if condition to be solved:"
    1.72 -           THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1 THEN print_tac' options "after if simp; in SOLVED:"))
    1.73 +           THEN print_tac options "if condition to be solved:"
    1.74 +           THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1 THEN print_tac options "after if simp; in SOLVED:"))
    1.75             THEN check_format thy
    1.76 -           THEN print_tac' options "after if simplification - a TRY block")))
    1.77 -    THEN print_tac' options "after if simplification"
    1.78 +           THEN print_tac options "after if simplification - a TRY block")))
    1.79 +    THEN print_tac options "after if simplification"
    1.80    end;
    1.81  
    1.82  (* corresponds to compile_fun -- maybe call that also compile_sidecond? *)
    1.83 @@ -2048,9 +2044,9 @@
    1.84      val (in_ts, clause_out_ts) = split_mode mode ts;
    1.85      fun prove_prems out_ts [] =
    1.86        (prove_match options thy out_ts)
    1.87 -      THEN print_tac' options "before simplifying assumptions"
    1.88 +      THEN print_tac options "before simplifying assumptions"
    1.89        THEN asm_full_simp_tac HOL_basic_ss' 1
    1.90 -      THEN print_tac' options "before single intro rule"
    1.91 +      THEN print_tac options "before single intro rule"
    1.92        THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1)
    1.93      | prove_prems out_ts ((p, deriv) :: ps) =
    1.94        let
    1.95 @@ -2064,11 +2060,11 @@
    1.96                val (_, out_ts''') = split_mode mode us
    1.97                val rec_tac = prove_prems out_ts''' ps
    1.98              in
    1.99 -              print_tac' options "before clause:"
   1.100 +              print_tac options "before clause:"
   1.101                (*THEN asm_simp_tac HOL_basic_ss 1*)
   1.102 -              THEN print_tac' options "before prove_expr:"
   1.103 +              THEN print_tac options "before prove_expr:"
   1.104                THEN prove_expr options thy nargs premposition (t, deriv)
   1.105 -              THEN print_tac' options "after prove_expr:"
   1.106 +              THEN print_tac options "after prove_expr:"
   1.107                THEN rec_tac
   1.108              end
   1.109            | Negprem t =>
   1.110 @@ -2082,16 +2078,16 @@
   1.111                val param_derivations = param_derivations_of deriv
   1.112                val params = ho_args_of mode args
   1.113              in
   1.114 -              print_tac' options "before prove_neg_expr:"
   1.115 +              print_tac options "before prove_neg_expr:"
   1.116                THEN full_simp_tac (HOL_basic_ss addsimps
   1.117                  [@{thm split_eta}, @{thm split_beta}, @{thm fst_conv},
   1.118                   @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1
   1.119                THEN (if (is_some name) then
   1.120 -                  print_tac' options "before applying not introduction rule"
   1.121 +                  print_tac options "before applying not introduction rule"
   1.122                    THEN rotate_tac premposition 1
   1.123                    THEN etac (the neg_intro_rule) 1
   1.124                    THEN rotate_tac (~premposition) 1
   1.125 -                  THEN print_tac' options "after applying not introduction rule"
   1.126 +                  THEN print_tac options "after applying not introduction rule"
   1.127                    THEN (EVERY (map2 (prove_param options thy nargs) params param_derivations))
   1.128                    THEN (REPEAT_DETERM (atac 1))
   1.129                  else
   1.130 @@ -2104,16 +2100,16 @@
   1.131              end
   1.132            | Sidecond t =>
   1.133             rtac @{thm if_predI} 1
   1.134 -           THEN print_tac' options "before sidecond:"
   1.135 +           THEN print_tac options "before sidecond:"
   1.136             THEN prove_sidecond thy t
   1.137 -           THEN print_tac' options "after sidecond:"
   1.138 +           THEN print_tac options "after sidecond:"
   1.139             THEN prove_prems [] ps)
   1.140        in (prove_match options thy out_ts)
   1.141            THEN rest_tac
   1.142        end;
   1.143      val prems_tac = prove_prems in_ts moded_ps
   1.144    in
   1.145 -    print_tac' options "Proving clause..."
   1.146 +    print_tac options "Proving clause..."
   1.147      THEN rtac @{thm bindI} 1
   1.148      THEN rtac @{thm singleI} 1
   1.149      THEN prems_tac
   1.150 @@ -2130,20 +2126,20 @@
   1.151      val pred_case_rule = the_elim_of thy pred
   1.152    in
   1.153      REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"}))
   1.154 -    THEN print_tac' options "before applying elim rule"
   1.155 +    THEN print_tac options "before applying elim rule"
   1.156      THEN etac (predfun_elim_of thy pred mode) 1
   1.157      THEN etac pred_case_rule 1
   1.158 -    THEN print_tac' options "after applying elim rule"
   1.159 +    THEN print_tac options "after applying elim rule"
   1.160      THEN (EVERY (map
   1.161             (fn i => EVERY' (select_sup (length moded_clauses) i) i) 
   1.162               (1 upto (length moded_clauses))))
   1.163      THEN (EVERY (map2 (prove_clause options thy nargs mode) clauses moded_clauses))
   1.164 -    THEN print_tac' options "proved one direction"
   1.165 +    THEN print_tac options "proved one direction"
   1.166    end;
   1.167  
   1.168  (** Proof in the other direction **)
   1.169  
   1.170 -fun prove_match2 thy out_ts = let
   1.171 +fun prove_match2 options thy out_ts = let
   1.172    fun split_term_tac (Free _) = all_tac
   1.173      | split_term_tac t =
   1.174        if (is_constructor thy t) then let
   1.175 @@ -2155,11 +2151,11 @@
   1.176            | _ => PureThy.get_thms thy (((fst o dest_Type o fastype_of) t) ^ ".split_asm")
   1.177          val (_, ts) = strip_comb t
   1.178        in
   1.179 -        (print_tac ("Term " ^ (Syntax.string_of_term_global thy t) ^ 
   1.180 +        (print_tac options ("Term " ^ (Syntax.string_of_term_global thy t) ^ 
   1.181            "splitting with rules \n" ^
   1.182          commas (map (Display.string_of_thm_global thy) split_rules)))
   1.183          THEN TRY ((Splitter.split_asm_tac split_rules 1)
   1.184 -        THEN (print_tac "after splitting with split_asm rules")
   1.185 +        THEN (print_tac options "after splitting with split_asm rules")
   1.186          (* THEN (Simplifier.asm_full_simp_tac HOL_basic_ss 1)
   1.187            THEN (DETERM (TRY (etac @{thm Pair_inject} 1)))*)
   1.188            THEN (REPEAT_DETERM_N (num_of_constrs - 1)
   1.189 @@ -2179,7 +2175,7 @@
   1.190  *)
   1.191  (* TODO: remove function *)
   1.192  
   1.193 -fun prove_param2 thy t deriv =
   1.194 +fun prove_param2 options thy t deriv =
   1.195    let
   1.196      val (f, args) = strip_comb (Envir.eta_contract t)
   1.197      val mode = head_mode_of deriv
   1.198 @@ -2192,13 +2188,13 @@
   1.199        | Free _ => all_tac
   1.200        | _ => error "prove_param2: illegal parameter term"
   1.201    in
   1.202 -    print_tac "before simplification in prove_args:"
   1.203 +    print_tac options "before simplification in prove_args:"
   1.204      THEN f_tac
   1.205 -    THEN print_tac "after simplification in prove_args"
   1.206 -    THEN EVERY (map2 (prove_param2 thy) ho_args param_derivations)
   1.207 +    THEN print_tac options "after simplification in prove_args"
   1.208 +    THEN EVERY (map2 (prove_param2 options thy) ho_args param_derivations)
   1.209    end
   1.210  
   1.211 -fun prove_expr2 thy (t, deriv) = 
   1.212 +fun prove_expr2 options thy (t, deriv) = 
   1.213    (case strip_comb t of
   1.214        (Const (name, T), args) =>
   1.215          let
   1.216 @@ -2208,18 +2204,18 @@
   1.217          in
   1.218            etac @{thm bindE} 1
   1.219            THEN (REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"})))
   1.220 -          THEN print_tac "prove_expr2-before"
   1.221 +          THEN print_tac options "prove_expr2-before"
   1.222            THEN etac (predfun_elim_of thy name mode) 1
   1.223 -          THEN print_tac "prove_expr2"
   1.224 -          THEN (EVERY (map2 (prove_param2 thy) ho_args param_derivations))
   1.225 -          THEN print_tac "finished prove_expr2"
   1.226 +          THEN print_tac options "prove_expr2"
   1.227 +          THEN (EVERY (map2 (prove_param2 options thy) ho_args param_derivations))
   1.228 +          THEN print_tac options "finished prove_expr2"
   1.229          end
   1.230        | _ => etac @{thm bindE} 1)
   1.231  
   1.232  (* FIXME: what is this for? *)
   1.233  (* replace defined by has_mode thy pred *)
   1.234  (* TODO: rewrite function *)
   1.235 -fun prove_sidecond2 thy t = let
   1.236 +fun prove_sidecond2 options thy t = let
   1.237    fun preds_of t nameTs = case strip_comb t of 
   1.238      (f as Const (name, T), args) =>
   1.239        if is_registered thy name then (name, T) :: nameTs
   1.240 @@ -2234,31 +2230,31 @@
   1.241     (* only simplify the one assumption *)
   1.242     full_simp_tac (HOL_basic_ss' addsimps @{thm eval_pred} :: defs) 1 
   1.243     (* need better control here! *)
   1.244 -   THEN print_tac "after sidecond2 simplification"
   1.245 +   THEN print_tac options "after sidecond2 simplification"
   1.246     end
   1.247    
   1.248 -fun prove_clause2 thy pred mode (ts, ps) i =
   1.249 +fun prove_clause2 options thy pred mode (ts, ps) i =
   1.250    let
   1.251      val pred_intro_rule = nth (intros_of thy pred) (i - 1)
   1.252      val (in_ts, clause_out_ts) = split_mode mode ts;
   1.253      fun prove_prems2 out_ts [] =
   1.254 -      print_tac "before prove_match2 - last call:"
   1.255 -      THEN prove_match2 thy out_ts
   1.256 -      THEN print_tac "after prove_match2 - last call:"
   1.257 +      print_tac options "before prove_match2 - last call:"
   1.258 +      THEN prove_match2 options thy out_ts
   1.259 +      THEN print_tac options "after prove_match2 - last call:"
   1.260        THEN (etac @{thm singleE} 1)
   1.261        THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1))
   1.262        THEN (asm_full_simp_tac HOL_basic_ss' 1)
   1.263        THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1))
   1.264        THEN (asm_full_simp_tac HOL_basic_ss' 1)
   1.265 -      THEN SOLVED (print_tac "state before applying intro rule:"
   1.266 +      THEN SOLVED (print_tac options "state before applying intro rule:"
   1.267        THEN (rtac pred_intro_rule 1)
   1.268        (* How to handle equality correctly? *)
   1.269 -      THEN (print_tac "state before assumption matching")
   1.270 +      THEN (print_tac options "state before assumption matching")
   1.271        THEN (REPEAT (atac 1 ORELSE 
   1.272           (CHANGED (asm_full_simp_tac (HOL_basic_ss' addsimps
   1.273             [@{thm split_eta}, @{thm "split_beta"}, @{thm "fst_conv"},
   1.274               @{thm "snd_conv"}, @{thm pair_collapse}]) 1)
   1.275 -          THEN print_tac "state after simp_tac:"))))
   1.276 +          THEN print_tac options "state after simp_tac:"))))
   1.277      | prove_prems2 out_ts ((p, deriv) :: ps) =
   1.278        let
   1.279          val mode = head_mode_of deriv
   1.280 @@ -2269,7 +2265,7 @@
   1.281              val (_, out_ts''') = split_mode mode us
   1.282              val rec_tac = prove_prems2 out_ts''' ps
   1.283            in
   1.284 -            (prove_expr2 thy (t, deriv)) THEN rec_tac
   1.285 +            (prove_expr2 options thy (t, deriv)) THEN rec_tac
   1.286            end
   1.287          | Negprem t =>
   1.288            let
   1.289 @@ -2280,14 +2276,14 @@
   1.290              val param_derivations = param_derivations_of deriv
   1.291              val ho_args = ho_args_of mode args
   1.292            in
   1.293 -            print_tac "before neg prem 2"
   1.294 +            print_tac options "before neg prem 2"
   1.295              THEN etac @{thm bindE} 1
   1.296              THEN (if is_some name then
   1.297                  full_simp_tac (HOL_basic_ss addsimps
   1.298                    [predfun_definition_of thy (the name) mode]) 1
   1.299                  THEN etac @{thm not_predE} 1
   1.300                  THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1
   1.301 -                THEN (EVERY (map2 (prove_param2 thy) ho_args param_derivations))
   1.302 +                THEN (EVERY (map2 (prove_param2 options thy) ho_args param_derivations))
   1.303                else
   1.304                  etac @{thm not_predE'} 1)
   1.305              THEN rec_tac
   1.306 @@ -2295,20 +2291,20 @@
   1.307          | Sidecond t =>
   1.308            etac @{thm bindE} 1
   1.309            THEN etac @{thm if_predE} 1
   1.310 -          THEN prove_sidecond2 thy t
   1.311 +          THEN prove_sidecond2 options thy t
   1.312            THEN prove_prems2 [] ps)
   1.313 -      in print_tac "before prove_match2:"
   1.314 -         THEN prove_match2 thy out_ts
   1.315 -         THEN print_tac "after prove_match2:"
   1.316 +      in print_tac options "before prove_match2:"
   1.317 +         THEN prove_match2 options thy out_ts
   1.318 +         THEN print_tac options "after prove_match2:"
   1.319           THEN rest_tac
   1.320        end;
   1.321      val prems_tac = prove_prems2 in_ts ps 
   1.322    in
   1.323 -    print_tac "starting prove_clause2"
   1.324 +    print_tac options "starting prove_clause2"
   1.325      THEN etac @{thm bindE} 1
   1.326      THEN (etac @{thm singleE'} 1)
   1.327      THEN (TRY (etac @{thm Pair_inject} 1))
   1.328 -    THEN print_tac "after singleE':"
   1.329 +    THEN print_tac options "after singleE':"
   1.330      THEN prems_tac
   1.331    end;
   1.332   
   1.333 @@ -2316,7 +2312,7 @@
   1.334    let
   1.335      fun prove_clause clause i =
   1.336        (if i < length moded_clauses then etac @{thm supE} 1 else all_tac)
   1.337 -      THEN (prove_clause2 thy pred mode clause i)
   1.338 +      THEN (prove_clause2 options thy pred mode clause i)
   1.339    in
   1.340      (DETERM (TRY (rtac @{thm unit.induct} 1)))
   1.341       THEN (REPEAT_DETERM (CHANGED (rewtac @{thm split_paired_all})))
   1.342 @@ -2338,11 +2334,11 @@
   1.343        (if not (skip_proof options) then
   1.344          (fn _ =>
   1.345          rtac @{thm pred_iffI} 1
   1.346 -        THEN print_tac' options "after pred_iffI"
   1.347 +        THEN print_tac options "after pred_iffI"
   1.348          THEN prove_one_direction options thy clauses preds pred mode moded_clauses
   1.349 -        THEN print_tac' options "proved one direction"
   1.350 +        THEN print_tac options "proved one direction"
   1.351          THEN prove_other_direction options thy pred mode moded_clauses
   1.352 -        THEN print_tac' options "proved other direction")
   1.353 +        THEN print_tac options "proved other direction")
   1.354        else (fn _ => Skip_Proof.cheat_tac thy))
   1.355    end;
   1.356  
     2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Mon Mar 22 08:30:13 2010 +0100
     2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Mon Mar 22 08:30:13 2010 +0100
     2.3 @@ -181,8 +181,10 @@
     2.4      val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1
     2.5      val (thy3, preproc_time) =  cpu_time "predicate preprocessing"
     2.6          (fn () => Predicate_Compile.preprocess options const thy2)
     2.7 +    (* FIXME: this is just for testing the predicate compiler proof procedure! *)
     2.8 +    val thy3' = Predicate_Compile_Core.add_equations options [full_constname] thy3
     2.9      val (thy4, core_comp_time) = cpu_time "random_dseq core compilation"
    2.10 -        (fn () => Predicate_Compile_Core.add_random_dseq_equations options [full_constname] thy3)
    2.11 +        (fn () => Predicate_Compile_Core.add_random_dseq_equations options [full_constname] thy3')
    2.12      val _ = Predicate_Compile_Core.print_all_modes Pos_Random_DSeq thy4
    2.13      val modes = Predicate_Compile_Core.modes_of Pos_Random_DSeq thy4 full_constname
    2.14      val output_mode = fold_rev (curry Fun) (map (K Output) (binder_types constT)) Bool