choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
authorbulwahn
Fri Mar 02 09:35:35 2012 +0100 (2012-03-02)
changeset 467584106258260b3
parent 46757 ad878aff9c15
child 46759 a6ea1c68fa52
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing
src/HOL/Quickcheck_Narrowing.thy
src/HOL/Rat.thy
src/HOL/Tools/Quickcheck/Narrowing_Engine.hs
src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs
src/HOL/Tools/Quickcheck/narrowing_generators.ML
     1.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Fri Mar 02 09:35:33 2012 +0100
     1.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Fri Mar 02 09:35:35 2012 +0100
     1.3 @@ -202,13 +202,13 @@
     1.4  
     1.5  subsubsection {* Narrowing's deep representation of types and terms *}
     1.6  
     1.7 -datatype narrowing_type = SumOfProd "narrowing_type list list"
     1.8 -datatype narrowing_term = Var "code_int list" narrowing_type | Ctr code_int "narrowing_term list"
     1.9 -datatype 'a cons = C narrowing_type "(narrowing_term list => 'a) list"
    1.10 +datatype narrowing_type = Narrowing_sum_of_products "narrowing_type list list"
    1.11 +datatype narrowing_term = Narrowing_variable "code_int list" narrowing_type | Narrowing_constructor code_int "narrowing_term list"
    1.12 +datatype 'a narrowing_cons = Narrowing_cons narrowing_type "(narrowing_term list => 'a) list"
    1.13  
    1.14 -primrec map_cons :: "('a => 'b) => 'a cons => 'b cons"
    1.15 +primrec map_cons :: "('a => 'b) => 'a narrowing_cons => 'b narrowing_cons"
    1.16  where
    1.17 -  "map_cons f (C ty cs) = C ty (map (%c. f o c) cs)"
    1.18 +  "map_cons f (Narrowing_cons ty cs) = Narrowing_cons ty (map (%c. f o c) cs)"
    1.19  
    1.20  subsubsection {* From narrowing's deep representation of terms to @{theory Code_Evaluation}'s terms *}
    1.21  
    1.22 @@ -238,46 +238,46 @@
    1.23  
    1.24  subsubsection {* Narrowing's basic operations *}
    1.25  
    1.26 -type_synonym 'a narrowing = "code_int => 'a cons"
    1.27 +type_synonym 'a narrowing = "code_int => 'a narrowing_cons"
    1.28  
    1.29  definition empty :: "'a narrowing"
    1.30  where
    1.31 -  "empty d = C (SumOfProd []) []"
    1.32 +  "empty d = Narrowing_cons (Narrowing_sum_of_products []) []"
    1.33    
    1.34  definition cons :: "'a => 'a narrowing"
    1.35  where
    1.36 -  "cons a d = (C (SumOfProd [[]]) [(%_. a)])"
    1.37 +  "cons a d = (Narrowing_cons (Narrowing_sum_of_products [[]]) [(%_. a)])"
    1.38  
    1.39  fun conv :: "(narrowing_term list => 'a) list => narrowing_term => 'a"
    1.40  where
    1.41 -  "conv cs (Var p _) = error (marker # map toEnum p)"
    1.42 -| "conv cs (Ctr i xs) = (nth cs i) xs"
    1.43 +  "conv cs (Narrowing_variable p _) = error (marker # map toEnum p)"
    1.44 +| "conv cs (Narrowing_constructor i xs) = (nth cs i) xs"
    1.45  
    1.46 -fun nonEmpty :: "narrowing_type => bool"
    1.47 +fun non_empty :: "narrowing_type => bool"
    1.48  where
    1.49 -  "nonEmpty (SumOfProd ps) = (\<not> (List.null ps))"
    1.50 +  "non_empty (Narrowing_sum_of_products ps) = (\<not> (List.null ps))"
    1.51  
    1.52  definition "apply" :: "('a => 'b) narrowing => 'a narrowing => 'b narrowing"
    1.53  where
    1.54    "apply f a d =
    1.55 -     (case f d of C (SumOfProd ps) cfs =>
    1.56 -       case a (d - 1) of C ta cas =>
    1.57 +     (case f d of Narrowing_cons (Narrowing_sum_of_products ps) cfs =>
    1.58 +       case a (d - 1) of Narrowing_cons ta cas =>
    1.59         let
    1.60 -         shallow = (d > 0 \<and> nonEmpty ta);
    1.61 +         shallow = (d > 0 \<and> non_empty ta);
    1.62           cs = [(%xs'. (case xs' of [] => undefined | x # xs => cf xs (conv cas x))). shallow, cf <- cfs]
    1.63 -       in C (SumOfProd [ta # p. shallow, p <- ps]) cs)"
    1.64 +       in Narrowing_cons (Narrowing_sum_of_products [ta # p. shallow, p <- ps]) cs)"
    1.65  
    1.66  definition sum :: "'a narrowing => 'a narrowing => 'a narrowing"
    1.67  where
    1.68    "sum a b d =
    1.69 -    (case a d of C (SumOfProd ssa) ca => 
    1.70 -      case b d of C (SumOfProd ssb) cb =>
    1.71 -      C (SumOfProd (ssa @ ssb)) (ca @ cb))"
    1.72 +    (case a d of Narrowing_cons (Narrowing_sum_of_products ssa) ca => 
    1.73 +      case b d of Narrowing_cons (Narrowing_sum_of_products ssb) cb =>
    1.74 +      Narrowing_cons (Narrowing_sum_of_products (ssa @ ssb)) (ca @ cb))"
    1.75  
    1.76  lemma [fundef_cong]:
    1.77    assumes "a d = a' d" "b d = b' d" "d = d'"
    1.78    shows "sum a b d = sum a' b' d'"
    1.79 -using assms unfolding sum_def by (auto split: cons.split narrowing_type.split)
    1.80 +using assms unfolding sum_def by (auto split: narrowing_cons.split narrowing_type.split)
    1.81  
    1.82  lemma [fundef_cong]:
    1.83    assumes "f d = f' d" "(\<And>d'. 0 <= d' & d' < d ==> a d' = a' d')"
    1.84 @@ -291,24 +291,24 @@
    1.85    have "int_of (of_int (int_of d' - int_of (of_int 1))) < int_of d'"
    1.86      by (simp add: of_int_inverse)
    1.87    ultimately show ?thesis
    1.88 -    unfolding apply_def by (auto split: cons.split narrowing_type.split simp add: Let_def)
    1.89 +    unfolding apply_def by (auto split: narrowing_cons.split narrowing_type.split simp add: Let_def)
    1.90  qed
    1.91  
    1.92  subsubsection {* Narrowing generator type class *}
    1.93  
    1.94  class narrowing =
    1.95 -  fixes narrowing :: "code_int => 'a cons"
    1.96 +  fixes narrowing :: "code_int => 'a narrowing_cons"
    1.97  
    1.98  datatype property = Universal narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Existential narrowing_type "(narrowing_term => property)" "narrowing_term => Code_Evaluation.term" | Property bool
    1.99  
   1.100  (* FIXME: hard-wired maximal depth of 100 here *)
   1.101  definition exists :: "('a :: {narrowing, partial_term_of} => property) => property"
   1.102  where
   1.103 -  "exists f = (case narrowing (100 :: code_int) of C ty cs => Existential ty (\<lambda> t. f (conv cs t)) (partial_term_of (TYPE('a))))"
   1.104 +  "exists f = (case narrowing (100 :: code_int) of Narrowing_cons ty cs => Existential ty (\<lambda> t. f (conv cs t)) (partial_term_of (TYPE('a))))"
   1.105  
   1.106  definition "all" :: "('a :: {narrowing, partial_term_of} => property) => property"
   1.107  where
   1.108 -  "all f = (case narrowing (100 :: code_int) of C ty cs => Universal ty (\<lambda>t. f (conv cs t)) (partial_term_of (TYPE('a))))"
   1.109 +  "all f = (case narrowing (100 :: code_int) of Narrowing_cons ty cs => Universal ty (\<lambda>t. f (conv cs t)) (partial_term_of (TYPE('a))))"
   1.110  
   1.111  subsubsection {* class @{text is_testable} *}
   1.112  
   1.113 @@ -356,14 +356,14 @@
   1.114  where
   1.115    "narrowing_dummy_partial_term_of = partial_term_of"
   1.116  
   1.117 -definition narrowing_dummy_narrowing :: "code_int => ('a :: narrowing) cons"
   1.118 +definition narrowing_dummy_narrowing :: "code_int => ('a :: narrowing) narrowing_cons"
   1.119  where
   1.120    "narrowing_dummy_narrowing = narrowing"
   1.121  
   1.122  lemma [code]:
   1.123    "ensure_testable f =
   1.124      (let
   1.125 -      x = narrowing_dummy_narrowing :: code_int => bool cons;
   1.126 +      x = narrowing_dummy_narrowing :: code_int => bool narrowing_cons;
   1.127        y = narrowing_dummy_partial_term_of :: bool itself => narrowing_term => term;
   1.128        z = (conv :: _ => _ => unit)  in f)"
   1.129  unfolding Let_def ensure_testable_def ..
   1.130 @@ -382,8 +382,8 @@
   1.131  subsection {* Narrowing for integers *}
   1.132  
   1.133  
   1.134 -definition drawn_from :: "'a list => 'a cons"
   1.135 -where "drawn_from xs = C (SumOfProd (map (%_. []) xs)) (map (%x y. x) xs)"
   1.136 +definition drawn_from :: "'a list => 'a narrowing_cons"
   1.137 +where "drawn_from xs = Narrowing_cons (Narrowing_sum_of_products (map (%_. []) xs)) (map (%x y. x) xs)"
   1.138  
   1.139  function around_zero :: "int => int list"
   1.140  where
   1.141 @@ -419,8 +419,8 @@
   1.142  by (rule partial_term_of_anything)+
   1.143  
   1.144  lemma [code]:
   1.145 -  "partial_term_of (ty :: int itself) (Var p t) == Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Int.int'') [])"
   1.146 -  "partial_term_of (ty :: int itself) (Ctr i []) == (if i mod 2 = 0 then
   1.147 +  "partial_term_of (ty :: int itself) (Narrowing_variable p t) == Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Int.int'') [])"
   1.148 +  "partial_term_of (ty :: int itself) (Narrowing_constructor i []) == (if i mod 2 = 0 then
   1.149       Code_Evaluation.term_of (- (int_of i) div 2) else Code_Evaluation.term_of ((int_of i + 1) div 2))"
   1.150  by (rule partial_term_of_anything)+
   1.151  
   1.152 @@ -459,9 +459,9 @@
   1.153  
   1.154  subsection {* Closing up *}
   1.155  
   1.156 -hide_type code_int narrowing_type narrowing_term cons property
   1.157 -hide_const int_of of_int nat_of map_cons nth error toEnum marker empty C conv nonEmpty ensure_testable all exists drawn_from around_zero
   1.158 -hide_const (open) Var Ctr "apply" sum cons
   1.159 -hide_fact empty_def cons_def conv.simps nonEmpty.simps apply_def sum_def ensure_testable_def all_def exists_def
   1.160 +hide_type code_int narrowing_type narrowing_term narrowing_cons property
   1.161 +hide_const int_of of_int nat_of map_cons nth error toEnum marker empty Narrowing_cons conv non_empty ensure_testable all exists drawn_from around_zero
   1.162 +hide_const (open) Narrowing_variable Narrowing_constructor "apply" sum cons
   1.163 +hide_fact empty_def cons_def conv.simps non_empty.simps apply_def sum_def ensure_testable_def all_def exists_def
   1.164  
   1.165  end
     2.1 --- a/src/HOL/Rat.thy	Fri Mar 02 09:35:33 2012 +0100
     2.2 +++ b/src/HOL/Rat.thy	Fri Mar 02 09:35:35 2012 +0100
     2.3 @@ -1184,8 +1184,8 @@
     2.4  end
     2.5  
     2.6  lemma [code]:
     2.7 -  "partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Var p tt) == Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Rat.rat'') [])"
     2.8 -  "partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Ctr 0 [l, k]) ==
     2.9 +  "partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Narrowing_variable p tt) == Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Rat.rat'') [])"
    2.10 +  "partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Narrowing_constructor 0 [l, k]) ==
    2.11       Code_Evaluation.App (Code_Evaluation.Const (STR ''Rat.Frct'')
    2.12       (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Product_Type.prod'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''Int.int'') []],
    2.13          Typerep.Typerep (STR ''Rat.rat'') []])) (Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.Const (STR ''Product_Type.Pair'') (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''Product_Type.prod'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''Int.int'') []]]])) (partial_term_of (TYPE(int)) l)) (partial_term_of (TYPE(int)) k))"
     3.1 --- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Fri Mar 02 09:35:33 2012 +0100
     3.2 +++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Fri Mar 02 09:35:35 2012 +0100
     3.3 @@ -11,12 +11,12 @@
     3.4  -- Term refinement
     3.5  
     3.6  new :: Pos -> [[Generated_Code.Narrowing_type]] -> [Generated_Code.Narrowing_term];
     3.7 -new p ps = [ Generated_Code.Ctr c (zipWith (\i t -> Generated_Code.Var (p++[i]) t) [0..] ts)
     3.8 +new p ps = [ Generated_Code.Narrowing_constructor c (zipWith (\i t -> Generated_Code.Narrowing_variable (p++[i]) t) [0..] ts)
     3.9             | (c, ts) <- zip [0..] ps ];
    3.10  
    3.11  refine :: Generated_Code.Narrowing_term -> Pos -> [Generated_Code.Narrowing_term];
    3.12 -refine (Generated_Code.Var p (Generated_Code.SumOfProd ss)) [] = new p ss;
    3.13 -refine (Generated_Code.Ctr c xs) p = map (Generated_Code.Ctr c) (refineList xs p);
    3.14 +refine (Generated_Code.Narrowing_variable p (Generated_Code.Narrowing_sum_of_products ss)) [] = new p ss;
    3.15 +refine (Generated_Code.Narrowing_constructor c xs) p = map (Generated_Code.Narrowing_constructor c) (refineList xs p);
    3.16  
    3.17  refineList :: [Generated_Code.Narrowing_term] -> Pos -> [[Generated_Code.Narrowing_term]];
    3.18  refineList xs (i:is) = let (ls, x:rs) = splitAt i xs in [ls ++ y:rs | y <- refine x is];
    3.19 @@ -24,8 +24,8 @@
    3.20  -- Find total instantiations of a partial value
    3.21  
    3.22  total :: Generated_Code.Narrowing_term -> [Generated_Code.Narrowing_term];
    3.23 -total (Generated_Code.Ctr c xs) = [Generated_Code.Ctr c ys | ys <- mapM total xs];
    3.24 -total (Generated_Code.Var p (Generated_Code.SumOfProd ss)) = [y | x <- new p ss, y <- total x];
    3.25 +total (Generated_Code.Narrowing_constructor c xs) = [Generated_Code.Narrowing_constructor c ys | ys <- mapM total xs];
    3.26 +total (Generated_Code.Narrowing_variable p (Generated_Code.Narrowing_sum_of_products ss)) = [y | x <- new p ss, y <- total x];
    3.27  
    3.28  -- Answers
    3.29  
    3.30 @@ -99,10 +99,10 @@
    3.31  
    3.32  instance (Generated_Code.Partial_term_of a, Generated_Code.Narrowing a, Testable b) => Testable (a -> b) where {
    3.33    property f = P $ \n d ->
    3.34 -    let Generated_Code.C t c = Generated_Code.narrowing d
    3.35 +    let Generated_Code.Narrowing_cons t c = Generated_Code.narrowing d
    3.36          c' = Generated_Code.conv c
    3.37          r = run (\(x:xs) -> f xs (c' x)) (n+1) d
    3.38 -    in  r { args = Generated_Code.Var [n] t : args r,
    3.39 +    in  r { args = Generated_Code.Narrowing_variable [n] t : args r,
    3.40        showArgs = (show . Generated_Code.partial_term_of (Generated_Code.Type :: Generated_Code.Itself a)) : showArgs r };
    3.41  };
    3.42  
     4.1 --- a/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs	Fri Mar 02 09:35:33 2012 +0100
     4.2 +++ b/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs	Fri Mar 02 09:35:35 2012 +0100
     4.3 @@ -27,8 +27,8 @@
     4.4  tailPosEdge (CtrB pos ts) = CtrB (tail pos) ts
     4.5  
     4.6  termOf :: Pos -> Path -> Generated_Code.Narrowing_term
     4.7 -termOf pos (CtrB [] i : es) = Generated_Code.Ctr i (termListOf pos es)
     4.8 -termOf pos [VN [] ty] = Generated_Code.Var pos ty
     4.9 +termOf pos (CtrB [] i : es) = Generated_Code.Narrowing_constructor i (termListOf pos es)
    4.10 +termOf pos [VN [] ty] = Generated_Code.Narrowing_variable pos ty
    4.11  
    4.12  termListOf :: Pos -> Path -> [Generated_Code.Narrowing_term]
    4.13  termListOf pos es = termListOf' 0 es
    4.14 @@ -149,7 +149,7 @@
    4.15  refineTree es p t = updateTree refine (pathPrefix p es) t
    4.16    where
    4.17      pathPrefix p es = takeWhile (\e -> posOf e /= p) es  
    4.18 -    refine (VarNode q r p (Generated_Code.SumOfProd ps) t) =
    4.19 +    refine (VarNode q r p (Generated_Code.Narrowing_sum_of_products ps) t) =
    4.20        CtrBranch q r p [ foldr (\(i,ty) t -> VarNode q r (p++[i]) ty t) t (zip [0..] ts) | ts <- ps ]
    4.21  
    4.22  -- refute
    4.23 @@ -230,7 +230,7 @@
    4.24  termlist_of :: Pos -> ([Generated_Code.Narrowing_term], QuantTree) -> ([Generated_Code.Narrowing_term], QuantTree)
    4.25  termlist_of p' (terms, Node b) = (terms, Node b) 
    4.26  termlist_of p' (terms, VarNode q r p ty t) = if p' == take (length p') p then
    4.27 -    termlist_of p' (terms ++ [Generated_Code.Var p ty], t)
    4.28 +    termlist_of p' (terms ++ [Generated_Code.Narrowing_variable p ty], t)
    4.29    else
    4.30      (terms, VarNode q r p ty t)
    4.31  termlist_of p' (terms, CtrBranch q r p ts) = if p' == take (length p') p then
    4.32 @@ -238,7 +238,7 @@
    4.33        Just i = findIndex (\t -> evalOf t == Eval False) ts
    4.34        (subterms, t') = fixp (\j -> termlist_of (p ++ [j])) 0 ([], ts !! i)
    4.35      in
    4.36 -      (terms ++ [Generated_Code.Ctr i subterms], t')
    4.37 +      (terms ++ [Generated_Code.Narrowing_constructor i subterms], t')
    4.38    else
    4.39      (terms, CtrBranch q r p ts)
    4.40    where
    4.41 @@ -248,7 +248,7 @@
    4.42  alltermlist_of :: Pos -> ([Generated_Code.Narrowing_term], QuantTree) -> [([Generated_Code.Narrowing_term], QuantTree)]
    4.43  alltermlist_of p' (terms, Node b) = [(terms, Node b)] 
    4.44  alltermlist_of p' (terms, VarNode q r p ty t) = if p' == take (length p') p then
    4.45 -    alltermlist_of p' (terms ++ [Generated_Code.Var p ty], t)
    4.46 +    alltermlist_of p' (terms ++ [Generated_Code.Narrowing_variable p ty], t)
    4.47    else
    4.48      [(terms, VarNode q r p ty t)]
    4.49  alltermlist_of p' (terms, CtrBranch q r p ts) =
    4.50 @@ -257,7 +257,7 @@
    4.51        its = filter (\(i, t) -> evalOf t == Eval False) (zip [0..] ts)
    4.52      in
    4.53        concatMap
    4.54 -        (\(i, t) -> map (\(subterms, t') -> (terms ++ [Generated_Code.Ctr i subterms], t'))
    4.55 +        (\(i, t) -> map (\(subterms, t') -> (terms ++ [Generated_Code.Narrowing_constructor i subterms], t'))
    4.56             (fixp (\j -> alltermlist_of (p ++ [j])) 0 ([], t))) its
    4.57    else
    4.58      [(terms, CtrBranch q r p ts)]
     5.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 02 09:35:33 2012 +0100
     5.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 02 09:35:35 2012 +0100
     5.3 @@ -68,7 +68,7 @@
     5.4  fun mk_partial_term_of_eq thy ty (i, (c, (_, tys))) =
     5.5    let
     5.6      val frees = map Free (Name.invent_names Name.context "a" (map (K @{typ narrowing_term}) tys))
     5.7 -    val narrowing_term = @{term "Quickcheck_Narrowing.Ctr"} $ HOLogic.mk_number @{typ code_int} i
     5.8 +    val narrowing_term = @{term "Quickcheck_Narrowing.Narrowing_constructor"} $ HOLogic.mk_number @{typ code_int} i
     5.9        $ (HOLogic.mk_list @{typ narrowing_term} (rev frees))
    5.10      val rhs = fold (fn u => fn t => @{term "Code_Evaluation.App"} $ t $ u)
    5.11          (map mk_partial_term_of (frees ~~ tys))
    5.12 @@ -94,7 +94,7 @@
    5.13      val const = AxClass.param_of_inst thy (@{const_name partial_term_of}, tyco);
    5.14      val var_insts =
    5.15        map (SOME o Thm.cterm_of thy o Logic.unvarify_types_global o Logic.varify_global)
    5.16 -        [Free ("ty", Term.itselfT ty), @{term "Quickcheck_Narrowing.Var p tt"},
    5.17 +        [Free ("ty", Term.itselfT ty), @{term "Quickcheck_Narrowing.Narrowing_variable p tt"},
    5.18            @{term "Code_Evaluation.Free (STR ''_'')"} $ HOLogic.mk_typerep ty];
    5.19      val var_eq =
    5.20        @{thm partial_term_of_anything}
    5.21 @@ -122,7 +122,7 @@
    5.22  val narrowingN = "narrowing";
    5.23  
    5.24  fun narrowingT T =
    5.25 -  @{typ Quickcheck_Narrowing.code_int} --> Type (@{type_name Quickcheck_Narrowing.cons}, [T])
    5.26 +  @{typ Quickcheck_Narrowing.code_int} --> Type (@{type_name Quickcheck_Narrowing.narrowing_cons}, [T])
    5.27  
    5.28  fun mk_empty T = Const (@{const_name Quickcheck_Narrowing.empty}, narrowingT T)
    5.29