add missing adaptation for narrowing to work with variables of type integer => integer
authorAndreas Lochbihler
Fri, 04 Apr 2014 13:22:15 +0200
changeset 56401 3b2db6132bfd
parent 56396 91a8561a8e35
child 56402 6d9a24f87460
add missing adaptation for narrowing to work with variables of type integer => integer
src/HOL/Quickcheck_Narrowing.thy
--- a/src/HOL/Quickcheck_Narrowing.thy	Thu Apr 03 22:04:57 2014 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy	Fri Apr 04 13:22:15 2014 +0200
@@ -275,6 +275,26 @@
      else Code_Evaluation.term_of ((i + 1) div 2))"
   by (rule partial_term_of_anything)+
 
+code_printing constant "Code_Evaluation.term_of :: integer \<Rightarrow> term" \<rightharpoonup> (Haskell_Quickcheck) 
+  "(let { t = Typerep.Typerep \"Code'_Numeral.integer\" [];
+     mkFunT s t = Typerep.Typerep \"fun\" [s, t];
+     numT = Typerep.Typerep \"Num.num\" [];
+     mkBit 0 = Generated'_Code.Const \"Num.num.Bit0\" (mkFunT numT numT);
+     mkBit 1 = Generated'_Code.Const \"Num.num.Bit1\" (mkFunT numT numT);
+     mkNumeral 1 = Generated'_Code.Const \"Num.num.One\" numT;
+     mkNumeral i = let { q = i `Prelude.div` 2; r = i `Prelude.mod` 2 }
+       in Generated'_Code.App (mkBit r) (mkNumeral q);
+     mkNumber 0 = Generated'_Code.Const \"Groups.zero'_class.zero\" t;
+     mkNumber 1 = Generated'_Code.Const \"Groups.one'_class.one\" t;
+     mkNumber i = if i > 0 then
+         Generated'_Code.App
+           (Generated'_Code.Const \"Num.numeral'_class.numeral\"
+              (mkFunT numT t))
+           (mkNumeral i)
+       else
+         Generated'_Code.App
+           (Generated'_Code.Const \"Groups.uminus'_class.uminus\" (mkFunT t t))
+           (mkNumber (- i)); } in mkNumber)"
 
 subsection {* The @{text find_unused_assms} command *}