src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 43079 4022892a2f28
parent 43047 26774ccb1c74
child 43114 b9fca691addd
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon May 30 16:15:37 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon May 30 17:55:34 2011 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4      Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
     1.5    val put_counterexample: (unit -> term list option) -> Proof.context -> Proof.context
     1.6    val finite_functions : bool Config.T
     1.7 +  val overlord : bool Config.T
     1.8    val setup: theory -> theory
     1.9  end;
    1.10  
    1.11 @@ -63,7 +64,7 @@
    1.12    let
    1.13      val frees = map Free (Name.names Name.context "a" (map (K @{typ narrowing_term}) tys))
    1.14      val narrowing_term = @{term "Quickcheck_Narrowing.Ctr"} $ HOLogic.mk_number @{typ code_int} i
    1.15 -      $ (HOLogic.mk_list @{typ narrowing_term} frees)
    1.16 +      $ (HOLogic.mk_list @{typ narrowing_term} (rev frees))
    1.17      val rhs = fold (fn u => fn t => @{term "Code_Evaluation.App"} $ t $ u)
    1.18          (map mk_partial_term_of (frees ~~ tys))
    1.19          (@{term "Code_Evaluation.Const"} $ HOLogic.mk_literal c $ HOLogic.mk_typerep (tys ---> ty))
    1.20 @@ -86,7 +87,14 @@
    1.21      val cs = (map o apsnd o apsnd o map o map_atyps)
    1.22        (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs;
    1.23      val const = AxClass.param_of_inst thy (@{const_name partial_term_of}, tyco);
    1.24 -    val eqs = map_index (mk_partial_term_of_eq thy ty) cs;
    1.25 +    val var_insts = map (SOME o Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global)
    1.26 +        [Free ("ty", Term.itselfT ty), @{term "Quickcheck_Narrowing.Var p tt"},
    1.27 +          @{term "Code_Evaluation.Free (STR ''_'')"} $ HOLogic.mk_typerep ty]
    1.28 +    val var_eq =
    1.29 +      @{thm partial_term_of_anything}
    1.30 +      |> Drule.instantiate' [SOME (Thm.ctyp_of thy ty)] var_insts
    1.31 +      |> Thm.varifyT_global
    1.32 +    val eqs = var_eq :: map_index (mk_partial_term_of_eq thy ty) cs;
    1.33   in
    1.34      thy
    1.35      |> Code.del_eqns const
    1.36 @@ -183,7 +191,7 @@
    1.37  fun exec verbose code =
    1.38    ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code)
    1.39  
    1.40 -fun with_tmp_dir name f =
    1.41 +fun with_overlord_dir name f =
    1.42    let
    1.43      val path = Path.append (Path.explode "~/.isabelle") (Path.basic (name ^ serial_string ()))
    1.44      val _ = Isabelle_System.mkdirs path;
    1.45 @@ -192,8 +200,8 @@
    1.46  fun value ctxt (get, put, put_ml) (code, value) size =
    1.47    let
    1.48      val tmp_prefix = "Quickcheck_Narrowing"
    1.49 -    val with_tmp_dir = if Config.get ctxt overlord 
    1.50 -      then Isabelle_System.with_tmp_dir else Quickcheck_Narrowing.with_tmp_dir 
    1.51 +    val with_tmp_dir =
    1.52 +      if Config.get ctxt overlord then with_overlord_dir else Isabelle_System.with_tmp_dir 
    1.53      fun run in_path = 
    1.54        let
    1.55          val code_file = Path.append in_path (Path.basic "Code.hs")