src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 41963 d8c3b26b3da4
parent 41953 994d088fbfbc
child 42019 a9445d87bc3e
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Mar 14 12:34:09 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Mon Mar 14 12:34:10 2011 +0100
     1.3 @@ -15,6 +15,100 @@
     1.4  structure Narrowing_Generators : NARROWING_GENERATORS =
     1.5  struct
     1.6  
     1.7 +fun mk_undefined T = Const(@{const_name undefined}, T)
     1.8 +
     1.9 +(* narrowing specific names and types *)
    1.10 +
    1.11 +exception FUNCTION_TYPE;
    1.12 +
    1.13 +val narrowingN = "narrowing";
    1.14 +
    1.15 +fun narrowingT T =
    1.16 +  @{typ Quickcheck_Narrowing.code_int} --> Type (@{type_name Quickcheck_Narrowing.cons}, [T])
    1.17 +
    1.18 +fun mk_empty T = Const (@{const_name Quickcheck_Narrowing.empty}, narrowingT T)
    1.19 +
    1.20 +fun mk_cons c T = Const (@{const_name Quickcheck_Narrowing.cons}, T --> narrowingT T) $ Const (c, T)
    1.21 +
    1.22 +fun mk_apply (T, t) (U, u) =
    1.23 +  let
    1.24 +    val (_, U') = dest_funT U
    1.25 +  in
    1.26 +    (U', Const (@{const_name Quickcheck_Narrowing.apply},
    1.27 +      narrowingT U --> narrowingT T --> narrowingT U') $ u $ t)
    1.28 +  end
    1.29 +  
    1.30 +fun mk_sum (t, u) =
    1.31 +  let
    1.32 +    val T = fastype_of t
    1.33 +  in
    1.34 +    Const (@{const_name Quickcheck_Narrowing.sum}, T --> T --> T) $ t $ u
    1.35 +  end
    1.36 +
    1.37 +(* creating narrowing instances *)
    1.38 +
    1.39 +fun mk_equations descr vs tycos narrowings (Ts, Us) =
    1.40 +  let
    1.41 +    fun mk_call T =
    1.42 +      let
    1.43 +        val narrowing =
    1.44 +          Const (@{const_name "Quickcheck_Narrowing.narrowing_class.narrowing"}, narrowingT T)
    1.45 +      in
    1.46 +        (T, narrowing)
    1.47 +      end
    1.48 +    fun mk_aux_call fTs (k, _) (tyco, Ts) =
    1.49 +      let
    1.50 +        val T = Type (tyco, Ts)
    1.51 +        val _ = if not (null fTs) then raise FUNCTION_TYPE else ()
    1.52 +      in
    1.53 +        (T, nth narrowings k)
    1.54 +      end
    1.55 +    fun mk_consexpr simpleT (c, xs) =
    1.56 +      let
    1.57 +        val Ts = map fst xs
    1.58 +      in snd (fold mk_apply xs (Ts ---> simpleT, mk_cons c (Ts ---> simpleT))) end
    1.59 +    fun mk_rhs exprs = foldr1 mk_sum exprs
    1.60 +    val rhss =
    1.61 +      Datatype_Aux.interpret_construction descr vs
    1.62 +        { atyp = mk_call, dtyp = mk_aux_call }
    1.63 +      |> (map o apfst) Type
    1.64 +      |> map (fn (T, cs) => map (mk_consexpr T) cs)
    1.65 +      |> map mk_rhs
    1.66 +    val lhss = narrowings
    1.67 +    val eqs = map (HOLogic.mk_Trueprop o HOLogic.mk_eq) (lhss ~~ rhss)
    1.68 +  in
    1.69 +    eqs
    1.70 +  end
    1.71 +
    1.72 +
    1.73 +fun instantiate_narrowing_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy =
    1.74 +  let
    1.75 +    val _ = Datatype_Aux.message config "Creating narrowing generators ...";
    1.76 +    val narrowingsN = map (prefix (narrowingN ^ "_")) (names @ auxnames);
    1.77 +  in
    1.78 +    thy
    1.79 +    |> Class.instantiation (tycos, vs, @{sort narrowing})
    1.80 +    |> (fold_map (fn (name, T) => Local_Theory.define
    1.81 +          ((Binding.conceal (Binding.name name), NoSyn),
    1.82 +            (apfst Binding.conceal Attrib.empty_binding, mk_undefined (narrowingT T)))
    1.83 +        #> apfst fst) (narrowingsN ~~ (Ts @ Us))
    1.84 +      #> (fn (narrowings, lthy) =>
    1.85 +        let
    1.86 +          val eqs_t = mk_equations descr vs tycos narrowings (Ts, Us)
    1.87 +          val eqs = map (fn eq => Goal.prove lthy ["f", "i"] [] eq
    1.88 +            (fn _ => Skip_Proof.cheat_tac (ProofContext.theory_of lthy))) eqs_t
    1.89 +        in
    1.90 +          fold (fn (name, eq) => Local_Theory.note
    1.91 +          ((Binding.conceal (Binding.qualify true prfx
    1.92 +             (Binding.qualify true name (Binding.name "simps"))),
    1.93 +             Code.add_default_eqn_attrib :: map (Attrib.internal o K)
    1.94 +               [Simplifier.simp_add, Nitpick_Simps.add]), [eq]) #> snd) (narrowingsN ~~ eqs) lthy
    1.95 +        end))
    1.96 +    |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))
    1.97 +  end;
    1.98 +
    1.99 +(* testing framework *)
   1.100 +
   1.101  val target = "Haskell"
   1.102  
   1.103  (* invocation of Haskell interpreter *)
   1.104 @@ -43,9 +137,10 @@
   1.105          val _ = File.write narrowing_engine_file narrowing_engine
   1.106          val _ = File.write main_file main
   1.107          val executable = File.shell_path (Path.append in_path (Path.basic "isa_lsc"))
   1.108 -        val cmd = "exec \"$ISABELLE_GHC\" -fglasgow-exts " ^
   1.109 +        val cmd = "\"$ISABELLE_GHC\" -fglasgow-exts " ^
   1.110            (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
   1.111            " -o " ^ executable ^ " && " ^ executable
   1.112 +          (* FIXME: should use bash command exec but does not work with && *) 
   1.113        in
   1.114          bash_output cmd
   1.115        end
   1.116 @@ -97,7 +192,9 @@
   1.117  
   1.118  
   1.119  val setup =
   1.120 -  Context.theory_map
   1.121 +  Datatype.interpretation
   1.122 +    (Quickcheck_Common.ensure_sort_datatype (@{sort narrowing}, instantiate_narrowing_datatype))
   1.123 +  #> Context.theory_map
   1.124      (Quickcheck.add_generator ("narrowing", compile_generator_expr))
   1.125      
   1.126  end;
   1.127 \ No newline at end of file