- restored old setup
authorberghofe
Tue Aug 28 18:12:00 2007 +0200 (2007-08-28)
changeset 244568eb0f4a36d04
parent 24455 cd8e14100c00
child 24457 a33258c78ed2
- restored old setup
- new infrastructure for auto quickcheck
- fixed bug in eta_expand that caused argument types to get mixed up
src/Pure/codegen.ML
     1.1 --- a/src/Pure/codegen.ML	Tue Aug 28 18:07:25 2007 +0200
     1.2 +++ b/src/Pure/codegen.ML	Tue Aug 28 18:12:00 2007 +0200
     1.3 @@ -73,7 +73,8 @@
     1.4    val mk_term_of: codegr -> string -> bool -> typ -> Pretty.T
     1.5    val mk_gen: codegr -> string -> bool -> string list -> string -> typ -> Pretty.T
     1.6    val test_fn: (int -> (string * term) list option) ref
     1.7 -  val test_term: theory -> int -> int -> term -> (string * term) list option
     1.8 +  val test_term: theory -> bool -> int -> int -> term -> (string * term) list option
     1.9 +  val auto_quickcheck: bool ref
    1.10    val eval_result: term ref
    1.11    val eval_term: theory -> term -> term
    1.12    val evaluation_conv: cterm -> thm
    1.13 @@ -85,8 +86,6 @@
    1.14    val mk_deftab: theory -> deftab
    1.15    val add_unfold: thm -> theory -> theory
    1.16  
    1.17 -  val setup: theory -> theory
    1.18 -
    1.19    val get_node: codegr -> string -> node
    1.20    val add_edge: string * string -> codegr -> codegr
    1.21    val add_edge_acyclic: string * string -> codegr -> codegr
    1.22 @@ -338,6 +337,13 @@
    1.23        end)
    1.24    in add_preprocessor prep end;
    1.25  
    1.26 +val _ = Context.add_setup
    1.27 +  (let
    1.28 +    fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
    1.29 +  in
    1.30 +    Code.add_attribute ("unfold", Scan.succeed (mk_attribute
    1.31 +      (fn thm => add_unfold thm #> Code.add_inline thm)))
    1.32 +  end);
    1.33  
    1.34  
    1.35  (**** associate constants with target language code ****)
    1.36 @@ -639,8 +645,9 @@
    1.37  
    1.38  fun eta_expand t ts i =
    1.39    let
    1.40 -    val (Ts, _) = strip_type (fastype_of t);
    1.41 -    val j = i - length ts
    1.42 +    val k = length ts;
    1.43 +    val Ts = Library.drop (k, binder_types (fastype_of t));
    1.44 +    val j = i - k
    1.45    in
    1.46      List.foldr (fn (T, t) => Abs ("x", T, t))
    1.47        (list_comb (t, ts @ map Bound (j-1 downto 0))) (Library.take (j, Ts))
    1.48 @@ -793,6 +800,11 @@
    1.49                   (add_edge (node_id, dep) gr'', p module''))
    1.50             end);
    1.51  
    1.52 +val _ = Context.add_setup
    1.53 + (add_codegen "default" default_codegen #>
    1.54 +  add_tycodegen "default" default_tycodegen);
    1.55 +
    1.56 +
    1.57  fun mk_struct name s = "structure " ^ name ^ " =\nstruct\n\n" ^ s ^ "end;\n";
    1.58  
    1.59  fun add_to_module name s = AList.map_entry (op =) name (suffix s);
    1.60 @@ -915,7 +927,7 @@
    1.61  
    1.62  val test_fn : (int -> (string * term) list option) ref = ref (fn _ => NONE);
    1.63  
    1.64 -fun test_term thy sz i t =
    1.65 +fun test_term thy quiet sz i t =
    1.66    let
    1.67      val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse
    1.68        error "Term to be tested contains type variables";
    1.69 @@ -950,36 +962,56 @@
    1.70                    [Pretty.str "]"])]],
    1.71              Pretty.brk 1, Pretty.str "end"]), Pretty.str ");"]) ^
    1.72        "\n\nend;\n") ();
    1.73 -    val _ = use_text "" Output.ml_output false s;
    1.74 +    val _ = use_text "" (K (), error) false s;
    1.75      fun iter f k = if k > i then NONE
    1.76        else (case (f () handle Match =>
    1.77 -          (warning "Exception Match raised in generated code"; NONE)) of
    1.78 +          (if quiet then ()
    1.79 +           else warning "Exception Match raised in generated code"; NONE)) of
    1.80          NONE => iter f (k+1) | SOME x => SOME x);
    1.81      fun test k = if k > sz then NONE
    1.82 -      else (priority ("Test data size: " ^ string_of_int k);
    1.83 +      else (if quiet then () else priority ("Test data size: " ^ string_of_int k);
    1.84          case iter (fn () => !test_fn k) 1 of
    1.85            NONE => test (k+1) | SOME x => SOME x);
    1.86    in test 0 end;
    1.87  
    1.88 -fun test_goal ({size, iterations, default_type}, tvinsts) i st =
    1.89 +fun test_goal out quiet ({size, iterations, default_type}, tvinsts) i assms state =
    1.90    let
    1.91 -    val thy = Toplevel.theory_of st;
    1.92 +    val thy = Proof.theory_of state;
    1.93      fun strip (Const ("all", _) $ Abs (_, _, t)) = strip t
    1.94        | strip t = t;
    1.95      val (gi, frees) = Logic.goal_params
    1.96 -      (prop_of (snd (snd (Proof.get_goal (Toplevel.proof_of st))))) i;
    1.97 +      (prop_of (snd (snd (Proof.get_goal state)))) i;
    1.98      val gi' = ObjectLogic.atomize_term thy (map_types
    1.99        (map_type_tfree (fn p as (s, _) =>
   1.100          the_default (the_default (TFree p) default_type)
   1.101 -          (AList.lookup (op =) tvinsts s))) (subst_bounds (frees, strip gi)));
   1.102 -  in case test_term (Toplevel.theory_of st) size iterations gi' of
   1.103 +          (AList.lookup (op =) tvinsts s)))
   1.104 +      (Logic.list_implies (assms, subst_bounds (frees, strip gi))));
   1.105 +  in case test_term thy quiet size iterations gi' of
   1.106        NONE => writeln "No counterexamples found."
   1.107 -    | SOME cex => writeln ("Counterexample found:\n" ^
   1.108 +    | SOME cex => out ("Counterexample found:\n" ^
   1.109          Pretty.string_of (Pretty.chunks (map (fn (s, t) =>
   1.110            Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1,
   1.111              Sign.pretty_term thy t]) cex)))
   1.112    end;
   1.113  
   1.114 +exception Counterex of string;
   1.115 +
   1.116 +val auto_quickcheck = ref true;
   1.117 +
   1.118 +fun test_goal' int state =
   1.119 +  let val assms = map term_of (Assumption.assms_of (Proof.context_of state))
   1.120 +  in
   1.121 +    (if int andalso !auto_quickcheck andalso not (!Toplevel.quiet)
   1.122 +     then
   1.123 +       (test_goal (fn s => raise Counterex s) true
   1.124 +          (get_test_params (Proof.theory_of state), []) 1 assms state
   1.125 +        handle ERROR _ => () | Counterex s => error s)
   1.126 +     else (); state)
   1.127 +  end;
   1.128 +
   1.129 +val _ = Context.add_setup
   1.130 +  (Context.theory_map (Specification.add_theorem_hook test_goal'));
   1.131 +
   1.132  
   1.133  (**** Evaluator for terms ****)
   1.134  
   1.135 @@ -1024,8 +1056,10 @@
   1.136  
   1.137  fun evaluation_conv ct =
   1.138    let val {thy, t, ...} = rep_cterm ct
   1.139 -  in Thm.invoke_oracle_i thy "HOL.evaluation" (thy, Evaluation t) end;
   1.140 -  (*FIXME get rid of hardwired theory name*)
   1.141 +  in Thm.invoke_oracle_i thy "Pure.evaluation" (thy, Evaluation t) end;
   1.142 +
   1.143 +val _ = Context.add_setup
   1.144 +  (Theory.add_oracle ("evaluation", evaluation_oracle));
   1.145  
   1.146  
   1.147  (**** Interface ****)
   1.148 @@ -1050,6 +1084,21 @@
   1.149       (p, []) => p
   1.150     | _ => error ("Malformed annotation: " ^ quote s));
   1.151  
   1.152 +val _ = Context.add_setup
   1.153 +  (fold assoc_type [("fun", (parse_mixfix (K dummyT) "(_ ->/ _)",
   1.154 +     [("term_of",
   1.155 +       "fun term_of_fun_type _ T _ U _ = Free (\"<function>\", T --> U);\n"),
   1.156 +      ("test",
   1.157 +       "fun gen_fun_type _ G i =\n\
   1.158 +       \  let\n\
   1.159 +       \    val f = ref (fn x => raise Match);\n\
   1.160 +       \    val _ = (f := (fn x =>\n\
   1.161 +       \      let\n\
   1.162 +       \        val y = G i;\n\
   1.163 +       \        val f' = !f\n\
   1.164 +       \      in (f := (fn x' => if x = x' then y else f' x'); y) end))\n\
   1.165 +       \  in (fn x => !f x) end;\n")]))]);
   1.166 +
   1.167  
   1.168  structure P = OuterParse and K = OuterKeyword;
   1.169  
   1.170 @@ -1127,23 +1176,20 @@
   1.171    (P.type_ident --| P.$$$ "=" -- P.typ >> (fn (v, s) => fn thy =>
   1.172      fn (x, ys) => (x, (v, Sign.read_typ thy s) :: ys))) xs;
   1.173  
   1.174 -fun app [] x = x
   1.175 -  | app (f :: fs) x = app fs (f x);
   1.176 -
   1.177  val test_paramsP =
   1.178    OuterSyntax.command "quickcheck_params" "set parameters for random testing" K.thy_decl
   1.179      (P.$$$ "[" |-- P.list1 parse_test_params --| P.$$$ "]" >>
   1.180        (fn fs => Toplevel.theory (fn thy =>
   1.181 -         map_test_params (app (map (fn f => f thy) fs)) thy)));
   1.182 +         map_test_params (Library.apply (map (fn f => f thy) fs)) thy)));
   1.183  
   1.184  val testP =
   1.185    OuterSyntax.command "quickcheck" "try to find counterexample for subgoal" K.diag
   1.186    (Scan.option (P.$$$ "[" |-- P.list1
   1.187      (   parse_test_params >> (fn f => fn thy => apfst (f thy))
   1.188       || parse_tyinst) --| P.$$$ "]") -- Scan.optional P.nat 1 >>
   1.189 -    (fn (ps, g) => Toplevel.keep (fn st =>
   1.190 -      test_goal (app (the_default [] (Option.map (map (fn f => f (Toplevel.theory_of st))) ps))
   1.191 -        (get_test_params (Toplevel.theory_of st), [])) g st)));
   1.192 +    (fn (ps, g) => Toplevel.keep (fn st => test_goal writeln false
   1.193 +      (Library.apply (the_default [] (Option.map (map (fn f => f (Toplevel.theory_of st))) ps))
   1.194 +        (get_test_params (Toplevel.theory_of st), [])) g [] (Toplevel.proof_of st))));
   1.195  
   1.196  val valueP =
   1.197    OuterSyntax.improper_command "value" "read, evaluate and print term" K.diag
   1.198 @@ -1154,28 +1200,4 @@
   1.199  val _ = OuterSyntax.add_parsers
   1.200    [assoc_typeP, assoc_constP, code_libraryP, code_moduleP, test_paramsP, testP, valueP];
   1.201  
   1.202 -val setup = 
   1.203 -  let
   1.204 -    fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I);
   1.205 -  in
   1.206 -    Code.add_attribute ("unfold", Scan.succeed (mk_attribute
   1.207 -      (fn thm => add_unfold thm #> Code.add_inline thm)))
   1.208 -    #> add_codegen "default" default_codegen
   1.209 -    #> add_tycodegen "default" default_tycodegen
   1.210 -    #> Theory.add_oracle ("evaluation", evaluation_oracle)
   1.211 -    #> fold assoc_type [("fun", (parse_mixfix (K dummyT) "(_ ->/ _)",
   1.212 -        [("term_of",
   1.213 -            "fun term_of_fun_type _ T _ U _ = Free (\"<function>\", T --> U);\n"),
   1.214 -        ("test",
   1.215 -           "fun gen_fun_type _ G i =\n\
   1.216 -           \  let\n\
   1.217 -           \    val f = ref (fn x => raise Match);\n\
   1.218 -           \    val _ = (f := (fn x =>\n\
   1.219 -           \      let\n\
   1.220 -           \        val y = G i;\n\
   1.221 -           \        val f' = !f\n\
   1.222 -           \      in (f := (fn x' => if x = x' then y else f' x'); y) end))\n\
   1.223 -           \  in (fn x => !f x) end;\n")]))]
   1.224 -  end;
   1.225 -
   1.226  end;