improving overlord option and partial_term_of derivation; changing Narrowing_Engine to print partial terms
authorbulwahn
Mon May 30 17:55:34 2011 +0200 (2011-05-30)
changeset 430794022892a2f28
parent 43078 e2631aaf1e1e
child 43080 73a1d6a7ef1d
improving overlord option and partial_term_of derivation; changing Narrowing_Engine to print partial terms
src/HOL/Tools/Quickcheck/Narrowing_Engine.hs
src/HOL/Tools/Quickcheck/narrowing_generators.ML
     1.1 --- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Mon May 30 16:15:37 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Mon May 30 17:55:34 2011 +0200
     1.3 @@ -43,7 +43,7 @@
     1.4  str_of_list (x:xs) = "(" ++ x ++ " :: " ++ str_of_list xs ++ ")";
     1.5  
     1.6  report :: Result -> [Narrowing_term] -> IO Int;
     1.7 -report r xs = putStrLn ("SOME (" ++ (str_of_list $ zipWith ($) (showArgs r) $ head [ys | ys <- mapM total xs]) ++ ")") >> hFlush stdout >> exitWith ExitSuccess;
     1.8 +report r xs = putStrLn ("SOME (" ++ (str_of_list $ zipWith ($) (showArgs r) xs) ++ ")") >> hFlush stdout >> exitWith ExitSuccess;
     1.9  
    1.10  eval :: Bool -> (Bool -> IO a) -> (Pos -> IO a) -> IO a;
    1.11  eval p k u = answer p (\p -> answer p k u) u;
    1.12 @@ -67,7 +67,8 @@
    1.13  instance Show Term where {
    1.14    show (Const c t) = "Const (\"" ++ c ++ "\", " ++ show t ++ ")";
    1.15    show (App s t) = "(" ++ show s ++ ") $ (" ++ show t ++ ")";
    1.16 -  show (Abs s ty t) = "Abs (\"" ++ s ++ "\", " ++ show ty ++ ", " ++ show t ++ ")";  
    1.17 +  show (Abs s ty t) = "Abs (\"" ++ s ++ "\", " ++ show ty ++ ", " ++ show t ++ ")";
    1.18 +  show (Free s ty) = "Free (\"" ++ s ++  "\", " ++ show ty ++ ")";
    1.19  };
    1.20  
    1.21  data Result =
    1.22 @@ -89,12 +90,12 @@
    1.23    property app = P $ \n d -> Result [] [] (app . reverse);
    1.24  };
    1.25  
    1.26 -instance (Term_of a, Narrowing a, Testable b) => Testable (a -> b) where {
    1.27 +instance (Partial_term_of a, Narrowing a, Testable b) => Testable (a -> b) where {
    1.28    property f = P $ \n d ->
    1.29      let C t c = narrowing d
    1.30          c' = conv c
    1.31          r = run (\(x:xs) -> f xs (c' x)) (n+1) d
    1.32 -    in  r { args = Var [n] t : args r, showArgs = (show . term_of . c') : showArgs r };
    1.33 +    in  r { args = Var [n] t : args r, showArgs = (show . partial_term_of (Type :: Itself a)) : showArgs r };
    1.34  };
    1.35  
    1.36  -- Top-level interface
     2.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon May 30 16:15:37 2011 +0100
     2.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon May 30 17:55:34 2011 +0200
     2.3 @@ -10,6 +10,7 @@
     2.4      Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
     2.5    val put_counterexample: (unit -> term list option) -> Proof.context -> Proof.context
     2.6    val finite_functions : bool Config.T
     2.7 +  val overlord : bool Config.T
     2.8    val setup: theory -> theory
     2.9  end;
    2.10  
    2.11 @@ -63,7 +64,7 @@
    2.12    let
    2.13      val frees = map Free (Name.names Name.context "a" (map (K @{typ narrowing_term}) tys))
    2.14      val narrowing_term = @{term "Quickcheck_Narrowing.Ctr"} $ HOLogic.mk_number @{typ code_int} i
    2.15 -      $ (HOLogic.mk_list @{typ narrowing_term} frees)
    2.16 +      $ (HOLogic.mk_list @{typ narrowing_term} (rev frees))
    2.17      val rhs = fold (fn u => fn t => @{term "Code_Evaluation.App"} $ t $ u)
    2.18          (map mk_partial_term_of (frees ~~ tys))
    2.19          (@{term "Code_Evaluation.Const"} $ HOLogic.mk_literal c $ HOLogic.mk_typerep (tys ---> ty))
    2.20 @@ -86,7 +87,14 @@
    2.21      val cs = (map o apsnd o apsnd o map o map_atyps)
    2.22        (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
    2.23      val const = AxClass.param_of_inst thy (@{const_name partial_term_of}, tyco);
    2.24 -    val eqs = map_index (mk_partial_term_of_eq thy ty) cs;
    2.25 +    val var_insts = map (SOME o Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global)
    2.26 +        [Free ("ty", Term.itselfT ty), @{term "Quickcheck_Narrowing.Var p tt"},
    2.27 +          @{term "Code_Evaluation.Free (STR ''_'')"} $ HOLogic.mk_typerep ty]
    2.28 +    val var_eq =
    2.29 +      @{thm partial_term_of_anything}
    2.30 +      |> Drule.instantiate' [SOME (Thm.ctyp_of thy ty)] var_insts
    2.31 +      |> Thm.varifyT_global
    2.32 +    val eqs = var_eq :: map_index (mk_partial_term_of_eq thy ty) cs;
    2.33   in
    2.34      thy
    2.35      |> Code.del_eqns const
    2.36 @@ -183,7 +191,7 @@
    2.37  fun exec verbose code =
    2.38    ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code)
    2.39  
    2.40 -fun with_tmp_dir name f =
    2.41 +fun with_overlord_dir name f =
    2.42    let
    2.43      val path = Path.append (Path.explode "~/.isabelle") (Path.basic (name ^ serial_string ()))
    2.44      val _ = Isabelle_System.mkdirs path;
    2.45 @@ -192,8 +200,8 @@
    2.46  fun value ctxt (get, put, put_ml) (code, value) size =
    2.47    let
    2.48      val tmp_prefix = "Quickcheck_Narrowing"
    2.49 -    val with_tmp_dir = if Config.get ctxt overlord 
    2.50 -      then Isabelle_System.with_tmp_dir else Quickcheck_Narrowing.with_tmp_dir 
    2.51 +    val with_tmp_dir =
    2.52 +      if Config.get ctxt overlord then with_overlord_dir else Isabelle_System.with_tmp_dir 
    2.53      fun run in_path = 
    2.54        let
    2.55          val code_file = Path.append in_path (Path.basic "Code.hs")