# HG changeset patch # User bulwahn # Date 1306756679 -7200 # Node ID 26774ccb1c7434be076776999be6fa3625ec15cc # Parent 2a1b01680505ae028b3d0e5e00e59b203ee1afd5 automatic derivation of partial_term_of functions; renaming type and term to longer names narrowing_type and narrowing_term; hiding constant C; adding overlord option diff -r 2a1b01680505 -r 26774ccb1c74 src/HOL/Library/Quickcheck_Narrowing.thy --- a/src/HOL/Library/Quickcheck_Narrowing.thy Mon May 30 12:20:04 2011 +0100 +++ b/src/HOL/Library/Quickcheck_Narrowing.thy Mon May 30 13:57:59 2011 +0200 @@ -86,7 +86,7 @@ "nat_of i = nat (int_of i)" -code_datatype "number_of \ int \ code_numeral" +code_datatype "number_of \ int \ code_int" instantiation code_int :: "{minus, linordered_semidom, semiring_div, linorder}" @@ -200,16 +200,19 @@ subsubsection {* Narrowing's deep representation of types and terms *} -datatype type = SumOfProd "type list list" +datatype narrowing_type = SumOfProd "narrowing_type list list" -datatype "term" = Var "code_int list" type | Ctr code_int "term list" - -datatype 'a cons = C type "(term list => 'a) 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" subsubsection {* From narrowing's deep representation of terms to Code_Evaluation's terms *} class partial_term_of = typerep + - fixes partial_term_of :: "'a itself => term => Code_Evaluation.term" + fixes partial_term_of :: "'a itself => narrowing_term => Code_Evaluation.term" + +lemma partial_term_of_anything: "partial_term_of x nt \ t" + by (rule eq_reflection) (cases "partial_term_of x nt", cases t, simp) + subsubsection {* Auxilary functions for Narrowing *} @@ -241,12 +244,12 @@ where "cons a d = (C (SumOfProd [[]]) [(%_. a)])" -fun conv :: "(term list => 'a) list => term => 'a" +fun conv :: "(narrowing_term list => 'a) list => narrowing_term => 'a" where "conv cs (Var p _) = error (Char Nibble0 Nibble0 # map toEnum p)" | "conv cs (Ctr i xs) = (nth cs i) xs" -fun nonEmpty :: "type => bool" +fun nonEmpty :: "narrowing_type => bool" where "nonEmpty (SumOfProd ps) = (\ (List.null ps))" @@ -270,7 +273,7 @@ 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 type.split) +using assms unfolding sum_def by (auto split: cons.split narrowing_type.split) lemma [fundef_cong]: assumes "f d = f' d" "(\d'. 0 <= d' & d' < d ==> a d' = a' d')" @@ -284,7 +287,7 @@ 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 type.split simp add: Let_def) + unfolding apply_def by (auto split: cons.split narrowing_type.split simp add: Let_def) qed type_synonym pos = "code_int list" @@ -459,7 +462,7 @@ instance bool :: is_testable .. -instance "fun" :: ("{term_of, narrowing}", is_testable) is_testable .. +instance "fun" :: ("{term_of, narrowing, partial_term_of}", is_testable) is_testable .. definition ensure_testable :: "'a :: is_testable => 'a :: is_testable" where @@ -494,8 +497,8 @@ setup {* Narrowing_Generators.setup *} -hide_type (open) code_int type "term" cons +hide_type (open) code_int narrowing_type narrowing_term cons hide_const (open) int_of of_int nth error toEnum map_index split_At empty - cons conv nonEmpty "apply" sum cons1 cons2 ensure_testable + C cons conv nonEmpty "apply" sum cons1 cons2 ensure_testable end \ No newline at end of file diff -r 2a1b01680505 -r 26774ccb1c74 src/HOL/Tools/Quickcheck/Narrowing_Engine.hs --- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs Mon May 30 12:20:04 2011 +0100 +++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs Mon May 30 13:57:59 2011 +0200 @@ -10,20 +10,20 @@ -- Term refinement -new :: Pos -> [[Type]] -> [Terma]; +new :: Pos -> [[Narrowing_type]] -> [Narrowing_term]; new p ps = [ Ctr c (zipWith (\i t -> Var (p++[i]) t) [0..] ts) | (c, ts) <- zip [0..] ps ]; -refine :: Terma -> Pos -> [Terma]; +refine :: Narrowing_term -> Pos -> [Narrowing_term]; refine (Var p (SumOfProd ss)) [] = new p ss; refine (Ctr c xs) p = map (Ctr c) (refineList xs p); -refineList :: [Terma] -> Pos -> [[Terma]]; +refineList :: [Narrowing_term] -> Pos -> [[Narrowing_term]]; refineList xs (i:is) = let (ls, x:rs) = splitAt i xs in [ls ++ y:rs | y <- refine x is]; -- Find total instantiations of a partial value -total :: Terma -> [Terma]; +total :: Narrowing_term -> [Narrowing_term]; total (Ctr c xs) = [Ctr c ys | ys <- mapM total xs]; total (Var p (SumOfProd ss)) = [y | x <- new p ss, y <- total x]; @@ -42,13 +42,13 @@ str_of_list [] = "[]"; str_of_list (x:xs) = "(" ++ x ++ " :: " ++ str_of_list xs ++ ")"; -report :: Result -> [Terma] -> IO Int; +report :: Result -> [Narrowing_term] -> IO Int; report r xs = putStrLn ("SOME (" ++ (str_of_list $ zipWith ($) (showArgs r) $ head [ys | ys <- mapM total xs]) ++ ")") >> hFlush stdout >> exitWith ExitSuccess; eval :: Bool -> (Bool -> IO a) -> (Pos -> IO a) -> IO a; eval p k u = answer p (\p -> answer p k u) u; -ref :: Result -> [Terma] -> IO Int; +ref :: Result -> [Narrowing_term] -> IO Int; ref r xs = eval (apply_fun r xs) (\res -> if res then return 1 else report r xs) (\p -> sumMapM (ref r) 1 (refineList xs p)); refute :: Result -> IO Int; @@ -71,18 +71,18 @@ }; data Result = - Result { args :: [Terma] - , showArgs :: [Terma -> String] - , apply_fun :: [Terma] -> Bool + Result { args :: [Narrowing_term] + , showArgs :: [Narrowing_term -> String] + , apply_fun :: [Narrowing_term] -> Bool }; data P = P (Int -> Int -> Result); -run :: Testable a => ([Terma] -> a) -> Int -> Int -> Result; +run :: Testable a => ([Narrowing_term] -> a) -> Int -> Int -> Result; run a = let P f = property a in f; class Testable a where { - property :: ([Terma] -> a) -> P; + property :: ([Narrowing_term] -> a) -> P; }; instance Testable Bool where { diff -r 2a1b01680505 -r 26774ccb1c74 src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon May 30 12:20:04 2011 +0100 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon May 30 13:57:59 2011 +0200 @@ -19,8 +19,89 @@ (* configurations *) val finite_functions = Attrib.setup_config_bool @{binding quickcheck_finite_functions} (K true) +val overlord = Attrib.setup_config_bool @{binding quickcheck_narrowing_overlord} (K false) -(* narrowing specific names and types *) +(* partial_term_of instances *) + +fun mk_partial_term_of (x, T) = + Const (@{const_name Quickcheck_Narrowing.partial_term_of_class.partial_term_of}, + Term.itselfT T --> @{typ narrowing_term} --> @{typ Code_Evaluation.term}) + $ Const ("TYPE", Term.itselfT T) $ x + +(** formal definition **) + +fun add_partial_term_of tyco raw_vs thy = + let + val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs; + val ty = Type (tyco, map TFree vs); + val lhs = Const (@{const_name partial_term_of}, + Term.itselfT ty --> @{typ narrowing_term} --> @{typ Code_Evaluation.term}) + $ Free ("x", Term.itselfT ty) $ Free ("t", @{typ narrowing_term}); + val rhs = @{term "undefined :: Code_Evaluation.term"}; + val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); + fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst + o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv"; + in + thy + |> Class.instantiation ([tyco], vs, @{sort partial_term_of}) + |> `(fn lthy => Syntax.check_term lthy eq) + |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq))) + |> snd + |> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])) + end; + +fun ensure_partial_term_of (tyco, (raw_vs, _)) thy = + let + val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort partial_term_of}) + andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep}; + in if need_inst then add_partial_term_of tyco raw_vs thy else thy end; + + +(** code equations for datatypes **) + +fun mk_partial_term_of_eq thy ty (i, (c, (_, tys))) = + let + val frees = map Free (Name.names Name.context "a" (map (K @{typ narrowing_term}) tys)) + val narrowing_term = @{term "Quickcheck_Narrowing.Ctr"} $ HOLogic.mk_number @{typ code_int} i + $ (HOLogic.mk_list @{typ narrowing_term} frees) + val rhs = fold (fn u => fn t => @{term "Code_Evaluation.App"} $ t $ u) + (map mk_partial_term_of (frees ~~ tys)) + (@{term "Code_Evaluation.Const"} $ HOLogic.mk_literal c $ HOLogic.mk_typerep (tys ---> ty)) + val insts = + map (SOME o Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global) + [Free ("ty", Term.itselfT ty), narrowing_term, rhs] + val cty = Thm.ctyp_of thy ty; + in + @{thm partial_term_of_anything} + |> Drule.instantiate' [SOME cty] insts + |> Thm.varifyT_global + end + +fun add_partial_term_of_code tyco raw_vs raw_cs thy = + let + val algebra = Sign.classes_of thy; + val vs = map (fn (v, sort) => + (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs; + val ty = Type (tyco, map TFree vs); + val cs = (map o apsnd o apsnd o map o map_atyps) + (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs; + val const = AxClass.param_of_inst thy (@{const_name partial_term_of}, tyco); + val eqs = map_index (mk_partial_term_of_eq thy ty) cs; + in + thy + |> Code.del_eqns const + |> fold Code.add_eqn eqs + end; + +fun ensure_partial_term_of_code (tyco, (raw_vs, cs)) thy = + let + val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort partial_term_of}; + in if has_inst then add_partial_term_of_code tyco raw_vs cs thy else thy end; + + +(* narrowing generators *) + +(** narrowing specific names and types **) exception FUNCTION_TYPE; @@ -48,7 +129,7 @@ Const (@{const_name Quickcheck_Narrowing.sum}, T --> T --> T) $ t $ u end -(* creating narrowing instances *) +(** deriving narrowing instances **) fun mk_equations descr vs tycos narrowings (Ts, Us) = let @@ -95,16 +176,24 @@ val target = "Haskell" -(* invocation of Haskell interpreter *) +(** invocation of Haskell interpreter **) val narrowing_engine = File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs") fun exec verbose code = ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code) +fun with_tmp_dir name f = + let + val path = Path.append (Path.explode "~/.isabelle") (Path.basic (name ^ serial_string ())) + val _ = Isabelle_System.mkdirs path; + in Exn.release (Exn.capture f path) end; + fun value ctxt (get, put, put_ml) (code, value) size = let val tmp_prefix = "Quickcheck_Narrowing" + val with_tmp_dir = if Config.get ctxt overlord + then Isabelle_System.with_tmp_dir else Quickcheck_Narrowing.with_tmp_dir fun run in_path = let val code_file = Path.append in_path (Path.basic "Code.hs") @@ -127,7 +216,7 @@ in bash_output cmd end - val result = Isabelle_System.with_tmp_dir tmp_prefix run + val result = with_tmp_dir tmp_prefix run val output_value = the_default "NONE" (try (snd o split_last o filter_out (fn s => s = "") o split_lines o fst) result) |> translate_string (fn s => if s = "\\" then "\\\\" else s) @@ -152,7 +241,7 @@ evaluation cookie thy (Code_Target.evaluator thy target naming program deps) (vs_ty, t) args size; in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end; -(* counterexample generator *) +(** counterexample generator **) structure Counterexample = Proof_Data ( @@ -203,9 +292,12 @@ (result, NONE) end; +(* setup *) val setup = - Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype + Code.datatype_interpretation ensure_partial_term_of + #> Code.datatype_interpretation ensure_partial_term_of_code + #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype (((@{sort typerep}, @{sort term_of}), @{sort narrowing}), instantiate_narrowing_datatype)) #> Context.theory_map (Quickcheck.add_generator ("narrowing", compile_generator_expr))