# HG changeset patch
# User bulwahn
# Date 1330677335 -3600
# Node ID 4106258260b3af90a7199ff20017bf9a445bf765
# Parent  ad878aff9c15e2b13366ae7c04cb1e52e404849a
choosing longer constant names in Quickcheck_Narrowing to reduce the chances of name clashes in Quickcheck-Narrowing

diff -r ad878aff9c15 -r 4106258260b3 src/HOL/Quickcheck_Narrowing.thy
--- a/src/HOL/Quickcheck_Narrowing.thy	Fri Mar 02 09:35:33 2012 +0100
+++ b/src/HOL/Quickcheck_Narrowing.thy	Fri Mar 02 09:35:35 2012 +0100
@@ -202,13 +202,13 @@
 
 subsubsection {* Narrowing's deep representation of types and terms *}
 
-datatype narrowing_type = SumOfProd "narrowing_type list list"
-datatype narrowing_term = Var "code_int list" narrowing_type | Ctr code_int "narrowing_term list"
-datatype 'a cons = C narrowing_type "(narrowing_term list => 'a) list"
+datatype narrowing_type = Narrowing_sum_of_products "narrowing_type list list"
+datatype narrowing_term = Narrowing_variable "code_int list" narrowing_type | Narrowing_constructor code_int "narrowing_term list"
+datatype 'a narrowing_cons = Narrowing_cons narrowing_type "(narrowing_term list => 'a) list"
 
-primrec map_cons :: "('a => 'b) => 'a cons => 'b cons"
+primrec map_cons :: "('a => 'b) => 'a narrowing_cons => 'b narrowing_cons"
 where
-  "map_cons f (C ty cs) = C ty (map (%c. f o c) cs)"
+  "map_cons f (Narrowing_cons ty cs) = Narrowing_cons ty (map (%c. f o c) cs)"
 
 subsubsection {* From narrowing's deep representation of terms to @{theory Code_Evaluation}'s terms *}
 
@@ -238,46 +238,46 @@
 
 subsubsection {* Narrowing's basic operations *}
 
-type_synonym 'a narrowing = "code_int => 'a cons"
+type_synonym 'a narrowing = "code_int => 'a narrowing_cons"
 
 definition empty :: "'a narrowing"
 where
-  "empty d = C (SumOfProd []) []"
+  "empty d = Narrowing_cons (Narrowing_sum_of_products []) []"
   
 definition cons :: "'a => 'a narrowing"
 where
-  "cons a d = (C (SumOfProd [[]]) [(%_. a)])"
+  "cons a d = (Narrowing_cons (Narrowing_sum_of_products [[]]) [(%_. a)])"
 
 fun conv :: "(narrowing_term list => 'a) list => narrowing_term => 'a"
 where
-  "conv cs (Var p _) = error (marker # map toEnum p)"
-| "conv cs (Ctr i xs) = (nth cs i) xs"
+  "conv cs (Narrowing_variable p _) = error (marker # map toEnum p)"
+| "conv cs (Narrowing_constructor i xs) = (nth cs i) xs"
 
-fun nonEmpty :: "narrowing_type => bool"
+fun non_empty :: "narrowing_type => bool"
 where
-  "nonEmpty (SumOfProd ps) = (\<not> (List.null ps))"
+  "non_empty (Narrowing_sum_of_products ps) = (\<not> (List.null ps))"
 
 definition "apply" :: "('a => 'b) narrowing => 'a narrowing => 'b narrowing"
 where
   "apply f a d =
-     (case f d of C (SumOfProd ps) cfs =>
-       case a (d - 1) of C ta cas =>
+     (case f d of Narrowing_cons (Narrowing_sum_of_products ps) cfs =>
+       case a (d - 1) of Narrowing_cons ta cas =>
        let
-         shallow = (d > 0 \<and> nonEmpty ta);
+         shallow = (d > 0 \<and> non_empty ta);
          cs = [(%xs'. (case xs' of [] => undefined | x # xs => cf xs (conv cas x))). shallow, cf <- cfs]
-       in C (SumOfProd [ta # p. shallow, p <- ps]) cs)"
+       in Narrowing_cons (Narrowing_sum_of_products [ta # p. shallow, p <- ps]) cs)"
 
 definition sum :: "'a narrowing => 'a narrowing => 'a narrowing"
 where
   "sum a b d =
-    (case a d of C (SumOfProd ssa) ca => 
-      case b d of C (SumOfProd ssb) cb =>
-      C (SumOfProd (ssa @ ssb)) (ca @ cb))"
+    (case a d of Narrowing_cons (Narrowing_sum_of_products ssa) ca => 
+      case b d of Narrowing_cons (Narrowing_sum_of_products ssb) cb =>
+      Narrowing_cons (Narrowing_sum_of_products (ssa @ ssb)) (ca @ cb))"
 
 lemma [fundef_cong]:
   assumes "a d = a' d" "b d = b' d" "d = d'"
   shows "sum a b d = sum a' b' d'"
-using assms unfolding sum_def by (auto split: cons.split narrowing_type.split)
+using assms unfolding sum_def by (auto split: narrowing_cons.split narrowing_type.split)
 
 lemma [fundef_cong]:
   assumes "f d = f' d" "(\<And>d'. 0 <= d' & d' < d ==> a d' = a' d')"
@@ -291,24 +291,24 @@
   have "int_of (of_int (int_of d' - int_of (of_int 1))) < int_of d'"
     by (simp add: of_int_inverse)
   ultimately show ?thesis
-    unfolding apply_def by (auto split: cons.split narrowing_type.split simp add: Let_def)
+    unfolding apply_def by (auto split: narrowing_cons.split narrowing_type.split simp add: Let_def)
 qed
 
 subsubsection {* Narrowing generator type class *}
 
 class narrowing =
-  fixes narrowing :: "code_int => 'a cons"
+  fixes narrowing :: "code_int => 'a narrowing_cons"
 
 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
 
 (* FIXME: hard-wired maximal depth of 100 here *)
 definition exists :: "('a :: {narrowing, partial_term_of} => property) => property"
 where
-  "exists f = (case narrowing (100 :: code_int) of C ty cs => Existential ty (\<lambda> t. f (conv cs t)) (partial_term_of (TYPE('a))))"
+  "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))))"
 
 definition "all" :: "('a :: {narrowing, partial_term_of} => property) => property"
 where
-  "all f = (case narrowing (100 :: code_int) of C ty cs => Universal ty (\<lambda>t. f (conv cs t)) (partial_term_of (TYPE('a))))"
+  "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))))"
 
 subsubsection {* class @{text is_testable} *}
 
@@ -356,14 +356,14 @@
 where
   "narrowing_dummy_partial_term_of = partial_term_of"
 
-definition narrowing_dummy_narrowing :: "code_int => ('a :: narrowing) cons"
+definition narrowing_dummy_narrowing :: "code_int => ('a :: narrowing) narrowing_cons"
 where
   "narrowing_dummy_narrowing = narrowing"
 
 lemma [code]:
   "ensure_testable f =
     (let
-      x = narrowing_dummy_narrowing :: code_int => bool cons;
+      x = narrowing_dummy_narrowing :: code_int => bool narrowing_cons;
       y = narrowing_dummy_partial_term_of :: bool itself => narrowing_term => term;
       z = (conv :: _ => _ => unit)  in f)"
 unfolding Let_def ensure_testable_def ..
@@ -382,8 +382,8 @@
 subsection {* Narrowing for integers *}
 
 
-definition drawn_from :: "'a list => 'a cons"
-where "drawn_from xs = C (SumOfProd (map (%_. []) xs)) (map (%x y. x) xs)"
+definition drawn_from :: "'a list => 'a narrowing_cons"
+where "drawn_from xs = Narrowing_cons (Narrowing_sum_of_products (map (%_. []) xs)) (map (%x y. x) xs)"
 
 function around_zero :: "int => int list"
 where
@@ -419,8 +419,8 @@
 by (rule partial_term_of_anything)+
 
 lemma [code]:
-  "partial_term_of (ty :: int itself) (Var p t) == Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Int.int'') [])"
-  "partial_term_of (ty :: int itself) (Ctr i []) == (if i mod 2 = 0 then
+  "partial_term_of (ty :: int itself) (Narrowing_variable p t) == Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Int.int'') [])"
+  "partial_term_of (ty :: int itself) (Narrowing_constructor i []) == (if i mod 2 = 0 then
      Code_Evaluation.term_of (- (int_of i) div 2) else Code_Evaluation.term_of ((int_of i + 1) div 2))"
 by (rule partial_term_of_anything)+
 
@@ -459,9 +459,9 @@
 
 subsection {* Closing up *}
 
-hide_type code_int narrowing_type narrowing_term cons property
-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
-hide_const (open) Var Ctr "apply" sum cons
-hide_fact empty_def cons_def conv.simps nonEmpty.simps apply_def sum_def ensure_testable_def all_def exists_def
+hide_type code_int narrowing_type narrowing_term narrowing_cons property
+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
+hide_const (open) Narrowing_variable Narrowing_constructor "apply" sum cons
+hide_fact empty_def cons_def conv.simps non_empty.simps apply_def sum_def ensure_testable_def all_def exists_def
 
 end
diff -r ad878aff9c15 -r 4106258260b3 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Fri Mar 02 09:35:33 2012 +0100
+++ b/src/HOL/Rat.thy	Fri Mar 02 09:35:35 2012 +0100
@@ -1184,8 +1184,8 @@
 end
 
 lemma [code]:
-  "partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Var p tt) == Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Rat.rat'') [])"
-  "partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Ctr 0 [l, k]) ==
+  "partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Narrowing_variable p tt) == Code_Evaluation.Free (STR ''_'') (Typerep.Typerep (STR ''Rat.rat'') [])"
+  "partial_term_of (ty :: rat itself) (Quickcheck_Narrowing.Narrowing_constructor 0 [l, k]) ==
      Code_Evaluation.App (Code_Evaluation.Const (STR ''Rat.Frct'')
      (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Product_Type.prod'') [Typerep.Typerep (STR ''Int.int'') [], Typerep.Typerep (STR ''Int.int'') []],
         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))"
diff -r ad878aff9c15 -r 4106258260b3 src/HOL/Tools/Quickcheck/Narrowing_Engine.hs
--- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Fri Mar 02 09:35:33 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Fri Mar 02 09:35:35 2012 +0100
@@ -11,12 +11,12 @@
 -- Term refinement
 
 new :: Pos -> [[Generated_Code.Narrowing_type]] -> [Generated_Code.Narrowing_term];
-new p ps = [ Generated_Code.Ctr c (zipWith (\i t -> Generated_Code.Var (p++[i]) t) [0..] ts)
+new p ps = [ Generated_Code.Narrowing_constructor c (zipWith (\i t -> Generated_Code.Narrowing_variable (p++[i]) t) [0..] ts)
            | (c, ts) <- zip [0..] ps ];
 
 refine :: Generated_Code.Narrowing_term -> Pos -> [Generated_Code.Narrowing_term];
-refine (Generated_Code.Var p (Generated_Code.SumOfProd ss)) [] = new p ss;
-refine (Generated_Code.Ctr c xs) p = map (Generated_Code.Ctr c) (refineList xs p);
+refine (Generated_Code.Narrowing_variable p (Generated_Code.Narrowing_sum_of_products ss)) [] = new p ss;
+refine (Generated_Code.Narrowing_constructor c xs) p = map (Generated_Code.Narrowing_constructor c) (refineList xs p);
 
 refineList :: [Generated_Code.Narrowing_term] -> Pos -> [[Generated_Code.Narrowing_term]];
 refineList xs (i:is) = let (ls, x:rs) = splitAt i xs in [ls ++ y:rs | y <- refine x is];
@@ -24,8 +24,8 @@
 -- Find total instantiations of a partial value
 
 total :: Generated_Code.Narrowing_term -> [Generated_Code.Narrowing_term];
-total (Generated_Code.Ctr c xs) = [Generated_Code.Ctr c ys | ys <- mapM total xs];
-total (Generated_Code.Var p (Generated_Code.SumOfProd ss)) = [y | x <- new p ss, y <- total x];
+total (Generated_Code.Narrowing_constructor c xs) = [Generated_Code.Narrowing_constructor c ys | ys <- mapM total xs];
+total (Generated_Code.Narrowing_variable p (Generated_Code.Narrowing_sum_of_products ss)) = [y | x <- new p ss, y <- total x];
 
 -- Answers
 
@@ -99,10 +99,10 @@
 
 instance (Generated_Code.Partial_term_of a, Generated_Code.Narrowing a, Testable b) => Testable (a -> b) where {
   property f = P $ \n d ->
-    let Generated_Code.C t c = Generated_Code.narrowing d
+    let Generated_Code.Narrowing_cons t c = Generated_Code.narrowing d
         c' = Generated_Code.conv c
         r = run (\(x:xs) -> f xs (c' x)) (n+1) d
-    in  r { args = Generated_Code.Var [n] t : args r,
+    in  r { args = Generated_Code.Narrowing_variable [n] t : args r,
       showArgs = (show . Generated_Code.partial_term_of (Generated_Code.Type :: Generated_Code.Itself a)) : showArgs r };
 };
 
diff -r ad878aff9c15 -r 4106258260b3 src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs
--- a/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs	Fri Mar 02 09:35:33 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs	Fri Mar 02 09:35:35 2012 +0100
@@ -27,8 +27,8 @@
 tailPosEdge (CtrB pos ts) = CtrB (tail pos) ts
 
 termOf :: Pos -> Path -> Generated_Code.Narrowing_term
-termOf pos (CtrB [] i : es) = Generated_Code.Ctr i (termListOf pos es)
-termOf pos [VN [] ty] = Generated_Code.Var pos ty
+termOf pos (CtrB [] i : es) = Generated_Code.Narrowing_constructor i (termListOf pos es)
+termOf pos [VN [] ty] = Generated_Code.Narrowing_variable pos ty
 
 termListOf :: Pos -> Path -> [Generated_Code.Narrowing_term]
 termListOf pos es = termListOf' 0 es
@@ -149,7 +149,7 @@
 refineTree es p t = updateTree refine (pathPrefix p es) t
   where
     pathPrefix p es = takeWhile (\e -> posOf e /= p) es  
-    refine (VarNode q r p (Generated_Code.SumOfProd ps) t) =
+    refine (VarNode q r p (Generated_Code.Narrowing_sum_of_products ps) t) =
       CtrBranch q r p [ foldr (\(i,ty) t -> VarNode q r (p++[i]) ty t) t (zip [0..] ts) | ts <- ps ]
 
 -- refute
@@ -230,7 +230,7 @@
 termlist_of :: Pos -> ([Generated_Code.Narrowing_term], QuantTree) -> ([Generated_Code.Narrowing_term], QuantTree)
 termlist_of p' (terms, Node b) = (terms, Node b) 
 termlist_of p' (terms, VarNode q r p ty t) = if p' == take (length p') p then
-    termlist_of p' (terms ++ [Generated_Code.Var p ty], t)
+    termlist_of p' (terms ++ [Generated_Code.Narrowing_variable p ty], t)
   else
     (terms, VarNode q r p ty t)
 termlist_of p' (terms, CtrBranch q r p ts) = if p' == take (length p') p then
@@ -238,7 +238,7 @@
       Just i = findIndex (\t -> evalOf t == Eval False) ts
       (subterms, t') = fixp (\j -> termlist_of (p ++ [j])) 0 ([], ts !! i)
     in
-      (terms ++ [Generated_Code.Ctr i subterms], t')
+      (terms ++ [Generated_Code.Narrowing_constructor i subterms], t')
   else
     (terms, CtrBranch q r p ts)
   where
@@ -248,7 +248,7 @@
 alltermlist_of :: Pos -> ([Generated_Code.Narrowing_term], QuantTree) -> [([Generated_Code.Narrowing_term], QuantTree)]
 alltermlist_of p' (terms, Node b) = [(terms, Node b)] 
 alltermlist_of p' (terms, VarNode q r p ty t) = if p' == take (length p') p then
-    alltermlist_of p' (terms ++ [Generated_Code.Var p ty], t)
+    alltermlist_of p' (terms ++ [Generated_Code.Narrowing_variable p ty], t)
   else
     [(terms, VarNode q r p ty t)]
 alltermlist_of p' (terms, CtrBranch q r p ts) =
@@ -257,7 +257,7 @@
       its = filter (\(i, t) -> evalOf t == Eval False) (zip [0..] ts)
     in
       concatMap
-        (\(i, t) -> map (\(subterms, t') -> (terms ++ [Generated_Code.Ctr i subterms], t'))
+        (\(i, t) -> map (\(subterms, t') -> (terms ++ [Generated_Code.Narrowing_constructor i subterms], t'))
            (fixp (\j -> alltermlist_of (p ++ [j])) 0 ([], t))) its
   else
     [(terms, CtrBranch q r p ts)]
diff -r ad878aff9c15 -r 4106258260b3 src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 02 09:35:33 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 02 09:35:35 2012 +0100
@@ -68,7 +68,7 @@
 fun mk_partial_term_of_eq thy ty (i, (c, (_, tys))) =
   let
     val frees = map Free (Name.invent_names Name.context "a" (map (K @{typ narrowing_term}) tys))
-    val narrowing_term = @{term "Quickcheck_Narrowing.Ctr"} $ HOLogic.mk_number @{typ code_int} i
+    val narrowing_term = @{term "Quickcheck_Narrowing.Narrowing_constructor"} $ HOLogic.mk_number @{typ code_int} i
       $ (HOLogic.mk_list @{typ narrowing_term} (rev frees))
     val rhs = fold (fn u => fn t => @{term "Code_Evaluation.App"} $ t $ u)
         (map mk_partial_term_of (frees ~~ tys))
@@ -94,7 +94,7 @@
     val const = AxClass.param_of_inst thy (@{const_name partial_term_of}, tyco);
     val var_insts =
       map (SOME o Thm.cterm_of thy o Logic.unvarify_types_global o Logic.varify_global)
-        [Free ("ty", Term.itselfT ty), @{term "Quickcheck_Narrowing.Var p tt"},
+        [Free ("ty", Term.itselfT ty), @{term "Quickcheck_Narrowing.Narrowing_variable p tt"},
           @{term "Code_Evaluation.Free (STR ''_'')"} $ HOLogic.mk_typerep ty];
     val var_eq =
       @{thm partial_term_of_anything}
@@ -122,7 +122,7 @@
 val narrowingN = "narrowing";
 
 fun narrowingT T =
-  @{typ Quickcheck_Narrowing.code_int} --> Type (@{type_name Quickcheck_Narrowing.cons}, [T])
+  @{typ Quickcheck_Narrowing.code_int} --> Type (@{type_name Quickcheck_Narrowing.narrowing_cons}, [T])
 
 fun mk_empty T = Const (@{const_name Quickcheck_Narrowing.empty}, narrowingT T)