adding dependencies to IsaMakefile; increasing negative search limit for predicate_compile_quickcheck; adding tracing of introduction rules in code_prolog
authorbulwahn
Tue Sep 07 11:51:53 2010 +0200 (2010-09-07)
changeset 39183512c10416590
parent 39161 75849a560c09
child 39184 71f3f194b962
adding dependencies to IsaMakefile; increasing negative search limit for predicate_compile_quickcheck; adding tracing of introduction rules in code_prolog
src/HOL/IsaMakefile
src/HOL/New_DSequence.thy
src/HOL/Tools/Predicate_Compile/code_prolog.ML
     1.1 --- a/src/HOL/IsaMakefile	Mon Sep 06 15:01:37 2010 +0200
     1.2 +++ b/src/HOL/IsaMakefile	Tue Sep 07 11:51:53 2010 +0200
     1.3 @@ -244,6 +244,8 @@
     1.4    Map.thy \
     1.5    Nat_Numeral.thy \
     1.6    Nat_Transfer.thy \
     1.7 +  New_DSequence.thy \
     1.8 +  New_Random_Sequence.thy \
     1.9    Nitpick.thy \
    1.10    Numeral_Simprocs.thy \
    1.11    Presburger.thy \
     2.1 --- a/src/HOL/New_DSequence.thy	Mon Sep 06 15:01:37 2010 +0200
     2.2 +++ b/src/HOL/New_DSequence.thy	Tue Sep 07 11:51:53 2010 +0200
     2.3 @@ -83,7 +83,7 @@
     2.4  
     2.5  definition pos_not_seq :: "unit neg_dseq => unit pos_dseq"
     2.6  where
     2.7 -  "pos_not_seq xq = (%i. Lazy_Sequence.hb_not_seq (xq i))"
     2.8 +  "pos_not_seq xq = (%i. Lazy_Sequence.hb_not_seq (xq (3 * i)))"
     2.9  
    2.10  definition neg_not_seq :: "unit pos_dseq => unit neg_dseq"
    2.11  where
     3.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Mon Sep 06 15:01:37 2010 +0200
     3.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Tue Sep 07 11:51:53 2010 +0200
     3.3 @@ -309,6 +309,11 @@
     3.4      fst (extend' key (G, []))
     3.5    end
     3.6  
     3.7 +fun print_intros ctxt gr consts =
     3.8 +  tracing (cat_lines (map (fn const =>
     3.9 +    "Constant " ^ const ^ "has intros:\n" ^
    3.10 +    cat_lines (map (Display.string_of_thm ctxt) (Graph.get_node gr const))) consts))
    3.11 +    
    3.12  fun generate ensure_groundness ctxt const =
    3.13    let 
    3.14      fun strong_conn_of gr keys =
    3.15 @@ -316,6 +321,7 @@
    3.16      val gr = Predicate_Compile_Core.intros_graph_of ctxt
    3.17      val gr' = add_edges depending_preds_of const gr
    3.18      val scc = strong_conn_of gr' [const]
    3.19 +    val _ = print_intros ctxt gr (flat scc)
    3.20      val constant_table = declare_consts (flat scc) []
    3.21    in
    3.22      apfst flat (fold_map (translate_intros ensure_groundness ctxt gr) (flat scc) constant_table)