src/Pure/codegen.ML
changeset 28309 c24bc53c815c
parent 28293 f15c2e2ffe1b
child 28315 d3cf88fe77bc
     1.1 --- a/src/Pure/codegen.ML	Mon Sep 22 08:00:24 2008 +0200
     1.2 +++ b/src/Pure/codegen.ML	Mon Sep 22 08:00:26 2008 +0200
     1.3 @@ -78,6 +78,7 @@
     1.4    val mk_gen: codegr -> string -> bool -> string list -> string -> typ -> Pretty.T
     1.5    val test_fn: (int -> (string * term) list option) ref
     1.6    val test_term: theory -> bool -> int -> int -> term -> (string * term) list option
     1.7 +  val test_term': Proof.context -> term -> int -> term list option
     1.8    val auto_quickcheck: bool ref
     1.9    val auto_quickcheck_time_limit: int ref
    1.10    val eval_result: (unit -> term) ref
    1.11 @@ -917,6 +918,38 @@
    1.12  
    1.13  val test_fn : (int -> (string * term) list option) ref = ref (fn _ => NONE);
    1.14  
    1.15 +fun test_term' ctxt t =
    1.16 +  let
    1.17 +    val thy = ProofContext.theory_of ctxt;
    1.18 +    val (code, gr) = setmp mode ["term_of", "test"]
    1.19 +      (generate_code_i thy [] "Generated") [("testf", t)];
    1.20 +    val frees = Name.names Name.context "a" ((map snd o fst o strip_abs) t);
    1.21 +    val frees' = frees ~~
    1.22 +      map (fn i => "arg" ^ string_of_int i) (1 upto length frees);
    1.23 +    val s = "structure TestTerm =\nstruct\n\n" ^
    1.24 +      cat_lines (map snd code) ^
    1.25 +      "\nopen Generated;\n\n" ^ string_of
    1.26 +        (Pretty.block [str "val () = Codegen.test_fn :=",
    1.27 +          Pretty.brk 1, str ("(fn i =>"), Pretty.brk 1,
    1.28 +          mk_let (map (fn ((s, T), s') =>
    1.29 +              (mk_tuple [str s', str (s' ^ "_t")],
    1.30 +               Pretty.block [mk_gen gr "Generated" false [] "" T, Pretty.brk 1,
    1.31 +                 str "(i + 1)"])) frees')
    1.32 +            (Pretty.block [str "if ",
    1.33 +              mk_app false (str "testf") (map (str o snd) frees'),
    1.34 +              Pretty.brk 1, str "then NONE",
    1.35 +              Pretty.brk 1, str "else ",
    1.36 +              Pretty.block [str "SOME ", Pretty.block (str "[" ::
    1.37 +                flat (separate [str ",", Pretty.brk 1]
    1.38 +                  (map (fn ((s, T), s') => [Pretty.block
    1.39 +                    [str ("(" ^ quote (Symbol.escape s) ^ ","), Pretty.brk 1,
    1.40 +                     str (s' ^ "_t ())")]]) frees')) @
    1.41 +                  [str "]"])]]),
    1.42 +          str ");"]) ^
    1.43 +      "\n\nend;\n";
    1.44 +    val _ = ML_Context.eval_in (SOME ctxt) false Position.none s;
    1.45 +  in ! test_fn #> (Option.map o map) snd end;
    1.46 +
    1.47  fun test_term thy quiet sz i t =
    1.48    let
    1.49      val ctxt = ProofContext.init thy;
    1.50 @@ -1132,6 +1165,7 @@
    1.51  val setup = add_codegen "default" default_codegen
    1.52    #> add_tycodegen "default" default_tycodegen
    1.53    #> Value.add_evaluator ("SML", eval_term o ProofContext.theory_of)
    1.54 +  #> Quickcheck.add_generator ("SML", test_term')
    1.55    #> Code.add_attribute ("unfold", Scan.succeed (Thm.declaration_attribute
    1.56         (fn thm => Context.mapping (add_unfold thm #> Code.add_inline thm) I)));
    1.57