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
authorbulwahn
Mon May 30 13:57:59 2011 +0200 (2011-05-30)
changeset 4304726774ccb1c74
parent 43046 2a1b01680505
child 43048 c62bed03fbce
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
src/HOL/Library/Quickcheck_Narrowing.thy
src/HOL/Tools/Quickcheck/Narrowing_Engine.hs
src/HOL/Tools/Quickcheck/narrowing_generators.ML
     1.1 --- a/src/HOL/Library/Quickcheck_Narrowing.thy	Mon May 30 12:20:04 2011 +0100
     1.2 +++ b/src/HOL/Library/Quickcheck_Narrowing.thy	Mon May 30 13:57:59 2011 +0200
     1.3 @@ -86,7 +86,7 @@
     1.4    "nat_of i = nat (int_of i)"
     1.5  
     1.6  
     1.7 -code_datatype "number_of \<Colon> int \<Rightarrow> code_numeral"
     1.8 +code_datatype "number_of \<Colon> int \<Rightarrow> code_int"
     1.9    
    1.10    
    1.11  instantiation code_int :: "{minus, linordered_semidom, semiring_div, linorder}"
    1.12 @@ -200,16 +200,19 @@
    1.13  
    1.14  subsubsection {* Narrowing's deep representation of types and terms *}
    1.15  
    1.16 -datatype type = SumOfProd "type list list"
    1.17 +datatype narrowing_type = SumOfProd "narrowing_type list list"
    1.18  
    1.19 -datatype "term" = Var "code_int list" type | Ctr code_int "term list"
    1.20 -
    1.21 -datatype 'a cons = C type "(term list => 'a) list"
    1.22 +datatype narrowing_term = Var "code_int list" narrowing_type | Ctr code_int "narrowing_term list"
    1.23 +datatype 'a cons = C narrowing_type "(narrowing_term list => 'a) list"
    1.24  
    1.25  subsubsection {* From narrowing's deep representation of terms to Code_Evaluation's terms *}
    1.26  
    1.27  class partial_term_of = typerep +
    1.28 -  fixes partial_term_of :: "'a itself => term => Code_Evaluation.term"
    1.29 +  fixes partial_term_of :: "'a itself => narrowing_term => Code_Evaluation.term"
    1.30 +
    1.31 +lemma partial_term_of_anything: "partial_term_of x nt \<equiv> t"
    1.32 +  by (rule eq_reflection) (cases "partial_term_of x nt", cases t, simp)
    1.33 +
    1.34  
    1.35  subsubsection {* Auxilary functions for Narrowing *}
    1.36  
    1.37 @@ -241,12 +244,12 @@
    1.38  where
    1.39    "cons a d = (C (SumOfProd [[]]) [(%_. a)])"
    1.40  
    1.41 -fun conv :: "(term list => 'a) list => term => 'a"
    1.42 +fun conv :: "(narrowing_term list => 'a) list => narrowing_term => 'a"
    1.43  where
    1.44    "conv cs (Var p _) = error (Char Nibble0 Nibble0 # map toEnum p)"
    1.45  | "conv cs (Ctr i xs) = (nth cs i) xs"
    1.46  
    1.47 -fun nonEmpty :: "type => bool"
    1.48 +fun nonEmpty :: "narrowing_type => bool"
    1.49  where
    1.50    "nonEmpty (SumOfProd ps) = (\<not> (List.null ps))"
    1.51  
    1.52 @@ -270,7 +273,7 @@
    1.53  lemma [fundef_cong]:
    1.54    assumes "a d = a' d" "b d = b' d" "d = d'"
    1.55    shows "sum a b d = sum a' b' d'"
    1.56 -using assms unfolding sum_def by (auto split: cons.split type.split)
    1.57 +using assms unfolding sum_def by (auto split: cons.split narrowing_type.split)
    1.58  
    1.59  lemma [fundef_cong]:
    1.60    assumes "f d = f' d" "(\<And>d'. 0 <= d' & d' < d ==> a d' = a' d')"
    1.61 @@ -284,7 +287,7 @@
    1.62    have "int_of (of_int (int_of d' - int_of (of_int 1))) < int_of d'"
    1.63      by (simp add: of_int_inverse)
    1.64    ultimately show ?thesis
    1.65 -    unfolding apply_def by (auto split: cons.split type.split simp add: Let_def)
    1.66 +    unfolding apply_def by (auto split: cons.split narrowing_type.split simp add: Let_def)
    1.67  qed
    1.68  
    1.69  type_synonym pos = "code_int list"
    1.70 @@ -459,7 +462,7 @@
    1.71  
    1.72  instance bool :: is_testable ..
    1.73  
    1.74 -instance "fun" :: ("{term_of, narrowing}", is_testable) is_testable ..
    1.75 +instance "fun" :: ("{term_of, narrowing, partial_term_of}", is_testable) is_testable ..
    1.76  
    1.77  definition ensure_testable :: "'a :: is_testable => 'a :: is_testable"
    1.78  where
    1.79 @@ -494,8 +497,8 @@
    1.80  
    1.81  setup {* Narrowing_Generators.setup *}
    1.82  
    1.83 -hide_type (open) code_int type "term" cons
    1.84 +hide_type (open) code_int narrowing_type narrowing_term cons
    1.85  hide_const (open) int_of of_int nth error toEnum map_index split_At empty
    1.86 -  cons conv nonEmpty "apply" sum cons1 cons2 ensure_testable
    1.87 +  C cons conv nonEmpty "apply" sum cons1 cons2 ensure_testable
    1.88  
    1.89  end
    1.90 \ No newline at end of file
     2.1 --- a/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Mon May 30 12:20:04 2011 +0100
     2.2 +++ b/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs	Mon May 30 13:57:59 2011 +0200
     2.3 @@ -10,20 +10,20 @@
     2.4  
     2.5  -- Term refinement
     2.6  
     2.7 -new :: Pos -> [[Type]] -> [Terma];
     2.8 +new :: Pos -> [[Narrowing_type]] -> [Narrowing_term];
     2.9  new p ps = [ Ctr c (zipWith (\i t -> Var (p++[i]) t) [0..] ts)
    2.10             | (c, ts) <- zip [0..] ps ];
    2.11  
    2.12 -refine :: Terma -> Pos -> [Terma];
    2.13 +refine :: Narrowing_term -> Pos -> [Narrowing_term];
    2.14  refine (Var p (SumOfProd ss)) [] = new p ss;
    2.15  refine (Ctr c xs) p = map (Ctr c) (refineList xs p);
    2.16  
    2.17 -refineList :: [Terma] -> Pos -> [[Terma]];
    2.18 +refineList :: [Narrowing_term] -> Pos -> [[Narrowing_term]];
    2.19  refineList xs (i:is) = let (ls, x:rs) = splitAt i xs in [ls ++ y:rs | y <- refine x is];
    2.20  
    2.21  -- Find total instantiations of a partial value
    2.22  
    2.23 -total :: Terma -> [Terma];
    2.24 +total :: Narrowing_term -> [Narrowing_term];
    2.25  total (Ctr c xs) = [Ctr c ys | ys <- mapM total xs];
    2.26  total (Var p (SumOfProd ss)) = [y | x <- new p ss, y <- total x];
    2.27  
    2.28 @@ -42,13 +42,13 @@
    2.29  str_of_list [] = "[]";
    2.30  str_of_list (x:xs) = "(" ++ x ++ " :: " ++ str_of_list xs ++ ")";
    2.31  
    2.32 -report :: Result -> [Terma] -> IO Int;
    2.33 +report :: Result -> [Narrowing_term] -> IO Int;
    2.34  report r xs = putStrLn ("SOME (" ++ (str_of_list $ zipWith ($) (showArgs r) $ head [ys | ys <- mapM total xs]) ++ ")") >> hFlush stdout >> exitWith ExitSuccess;
    2.35  
    2.36  eval :: Bool -> (Bool -> IO a) -> (Pos -> IO a) -> IO a;
    2.37  eval p k u = answer p (\p -> answer p k u) u;
    2.38  
    2.39 -ref :: Result -> [Terma] -> IO Int;
    2.40 +ref :: Result -> [Narrowing_term] -> IO Int;
    2.41  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));
    2.42            
    2.43  refute :: Result -> IO Int;
    2.44 @@ -71,18 +71,18 @@
    2.45  };
    2.46  
    2.47  data Result =
    2.48 -  Result { args     :: [Terma]
    2.49 -         , showArgs :: [Terma -> String]
    2.50 -         , apply_fun    :: [Terma] -> Bool
    2.51 +  Result { args     :: [Narrowing_term]
    2.52 +         , showArgs :: [Narrowing_term -> String]
    2.53 +         , apply_fun    :: [Narrowing_term] -> Bool
    2.54           };
    2.55  
    2.56  data P = P (Int -> Int -> Result);
    2.57  
    2.58 -run :: Testable a => ([Terma] -> a) -> Int -> Int -> Result;
    2.59 +run :: Testable a => ([Narrowing_term] -> a) -> Int -> Int -> Result;
    2.60  run a = let P f = property a in f;
    2.61  
    2.62  class Testable a where {
    2.63 -  property :: ([Terma] -> a) -> P;
    2.64 +  property :: ([Narrowing_term] -> a) -> P;
    2.65  };
    2.66  
    2.67  instance Testable Bool where {
     3.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon May 30 12:20:04 2011 +0100
     3.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon May 30 13:57:59 2011 +0200
     3.3 @@ -19,8 +19,89 @@
     3.4  (* configurations *)
     3.5  
     3.6  val finite_functions = Attrib.setup_config_bool @{binding quickcheck_finite_functions} (K true)
     3.7 +val overlord = Attrib.setup_config_bool @{binding quickcheck_narrowing_overlord} (K false)
     3.8  
     3.9 -(* narrowing specific names and types *)
    3.10 +(* partial_term_of instances *)
    3.11 +
    3.12 +fun mk_partial_term_of (x, T) =
    3.13 +  Const (@{const_name Quickcheck_Narrowing.partial_term_of_class.partial_term_of},
    3.14 +    Term.itselfT T --> @{typ narrowing_term} --> @{typ Code_Evaluation.term})
    3.15 +      $ Const ("TYPE", Term.itselfT T) $ x
    3.16 +
    3.17 +(** formal definition **)
    3.18 +
    3.19 +fun add_partial_term_of tyco raw_vs thy =
    3.20 +  let
    3.21 +    val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs;
    3.22 +    val ty = Type (tyco, map TFree vs);
    3.23 +    val lhs = Const (@{const_name partial_term_of},
    3.24 +        Term.itselfT ty --> @{typ narrowing_term} --> @{typ Code_Evaluation.term})
    3.25 +      $ Free ("x", Term.itselfT ty) $ Free ("t", @{typ narrowing_term});
    3.26 +    val rhs = @{term "undefined :: Code_Evaluation.term"};
    3.27 +    val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
    3.28 +    fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst
    3.29 +      o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
    3.30 +  in
    3.31 +    thy
    3.32 +    |> Class.instantiation ([tyco], vs, @{sort partial_term_of})
    3.33 +    |> `(fn lthy => Syntax.check_term lthy eq)
    3.34 +    |-> (fn eq => Specification.definition (NONE, ((Binding.name (triv_name_of eq), []), eq)))
    3.35 +    |> snd
    3.36 +    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    3.37 +  end;
    3.38 +
    3.39 +fun ensure_partial_term_of (tyco, (raw_vs, _)) thy =
    3.40 +  let
    3.41 +    val need_inst = not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort partial_term_of})
    3.42 +      andalso can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort typerep};
    3.43 +  in if need_inst then add_partial_term_of tyco raw_vs thy else thy end;
    3.44 +
    3.45 +
    3.46 +(** code equations for datatypes **)
    3.47 +
    3.48 +fun mk_partial_term_of_eq thy ty (i, (c, (_, tys))) =
    3.49 +  let
    3.50 +    val frees = map Free (Name.names Name.context "a" (map (K @{typ narrowing_term}) tys))
    3.51 +    val narrowing_term = @{term "Quickcheck_Narrowing.Ctr"} $ HOLogic.mk_number @{typ code_int} i
    3.52 +      $ (HOLogic.mk_list @{typ narrowing_term} frees)
    3.53 +    val rhs = fold (fn u => fn t => @{term "Code_Evaluation.App"} $ t $ u)
    3.54 +        (map mk_partial_term_of (frees ~~ tys))
    3.55 +        (@{term "Code_Evaluation.Const"} $ HOLogic.mk_literal c $ HOLogic.mk_typerep (tys ---> ty))
    3.56 +    val insts =
    3.57 +      map (SOME o Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global)
    3.58 +        [Free ("ty", Term.itselfT ty), narrowing_term, rhs]
    3.59 +    val cty = Thm.ctyp_of thy ty;
    3.60 +  in
    3.61 +    @{thm partial_term_of_anything}
    3.62 +    |> Drule.instantiate' [SOME cty] insts
    3.63 +    |> Thm.varifyT_global
    3.64 +  end
    3.65 +
    3.66 +fun add_partial_term_of_code tyco raw_vs raw_cs thy =
    3.67 +  let
    3.68 +    val algebra = Sign.classes_of thy;
    3.69 +    val vs = map (fn (v, sort) =>
    3.70 +      (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs;
    3.71 +    val ty = Type (tyco, map TFree vs);
    3.72 +    val cs = (map o apsnd o apsnd o map o map_atyps)
    3.73 +      (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
    3.74 +    val const = AxClass.param_of_inst thy (@{const_name partial_term_of}, tyco);
    3.75 +    val eqs = map_index (mk_partial_term_of_eq thy ty) cs;
    3.76 + in
    3.77 +    thy
    3.78 +    |> Code.del_eqns const
    3.79 +    |> fold Code.add_eqn eqs
    3.80 +  end;
    3.81 +
    3.82 +fun ensure_partial_term_of_code (tyco, (raw_vs, cs)) thy =
    3.83 +  let
    3.84 +    val has_inst = can (Sorts.mg_domain (Sign.classes_of thy) tyco) @{sort partial_term_of};
    3.85 +  in if has_inst then add_partial_term_of_code tyco raw_vs cs thy else thy end;
    3.86 +
    3.87 +
    3.88 +(* narrowing generators *)
    3.89 +
    3.90 +(** narrowing specific names and types **)
    3.91  
    3.92  exception FUNCTION_TYPE;
    3.93  
    3.94 @@ -48,7 +129,7 @@
    3.95      Const (@{const_name Quickcheck_Narrowing.sum}, T --> T --> T) $ t $ u
    3.96    end
    3.97  
    3.98 -(* creating narrowing instances *)
    3.99 +(** deriving narrowing instances **)
   3.100  
   3.101  fun mk_equations descr vs tycos narrowings (Ts, Us) =
   3.102    let
   3.103 @@ -95,16 +176,24 @@
   3.104  
   3.105  val target = "Haskell"
   3.106  
   3.107 -(* invocation of Haskell interpreter *)
   3.108 +(** invocation of Haskell interpreter **)
   3.109  
   3.110  val narrowing_engine = File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")
   3.111  
   3.112  fun exec verbose code =
   3.113    ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code)
   3.114  
   3.115 +fun with_tmp_dir name f =
   3.116 +  let
   3.117 +    val path = Path.append (Path.explode "~/.isabelle") (Path.basic (name ^ serial_string ()))
   3.118 +    val _ = Isabelle_System.mkdirs path;
   3.119 +  in Exn.release (Exn.capture f path) end;
   3.120 +  
   3.121  fun value ctxt (get, put, put_ml) (code, value) size =
   3.122    let
   3.123      val tmp_prefix = "Quickcheck_Narrowing"
   3.124 +    val with_tmp_dir = if Config.get ctxt overlord 
   3.125 +      then Isabelle_System.with_tmp_dir else Quickcheck_Narrowing.with_tmp_dir 
   3.126      fun run in_path = 
   3.127        let
   3.128          val code_file = Path.append in_path (Path.basic "Code.hs")
   3.129 @@ -127,7 +216,7 @@
   3.130        in
   3.131          bash_output cmd
   3.132        end
   3.133 -    val result = Isabelle_System.with_tmp_dir tmp_prefix run
   3.134 +    val result = with_tmp_dir tmp_prefix run
   3.135      val output_value = the_default "NONE"
   3.136        (try (snd o split_last o filter_out (fn s => s = "") o split_lines o fst) result)
   3.137        |> translate_string (fn s => if s = "\\" then "\\\\" else s)
   3.138 @@ -152,7 +241,7 @@
   3.139        evaluation cookie thy (Code_Target.evaluator thy target naming program deps) (vs_ty, t) args size;
   3.140    in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
   3.141  
   3.142 -(* counterexample generator *)
   3.143 +(** counterexample generator **)
   3.144    
   3.145  structure Counterexample = Proof_Data
   3.146  (
   3.147 @@ -203,9 +292,12 @@
   3.148      (result, NONE)
   3.149    end;
   3.150  
   3.151 +(* setup *)
   3.152  
   3.153  val setup =
   3.154 -  Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
   3.155 +  Code.datatype_interpretation ensure_partial_term_of
   3.156 +  #> Code.datatype_interpretation ensure_partial_term_of_code
   3.157 +  #> Datatype.interpretation (Quickcheck_Common.ensure_sort_datatype
   3.158      (((@{sort typerep}, @{sort term_of}), @{sort narrowing}), instantiate_narrowing_datatype))
   3.159    #> Context.theory_map
   3.160      (Quickcheck.add_generator ("narrowing", compile_generator_expr))