76 val mk_type: bool -> typ -> Pretty.T |
76 val mk_type: bool -> typ -> Pretty.T |
77 val mk_term_of: codegr -> string -> bool -> typ -> Pretty.T |
77 val mk_term_of: codegr -> string -> bool -> typ -> Pretty.T |
78 val mk_gen: codegr -> string -> bool -> string list -> string -> typ -> Pretty.T |
78 val mk_gen: codegr -> string -> bool -> string list -> string -> typ -> Pretty.T |
79 val test_fn: (int -> (string * term) list option) ref |
79 val test_fn: (int -> (string * term) list option) ref |
80 val test_term: theory -> bool -> int -> int -> term -> (string * term) list option |
80 val test_term: theory -> bool -> int -> int -> term -> (string * term) list option |
|
81 val test_term': Proof.context -> term -> int -> term list option |
81 val auto_quickcheck: bool ref |
82 val auto_quickcheck: bool ref |
82 val auto_quickcheck_time_limit: int ref |
83 val auto_quickcheck_time_limit: int ref |
83 val eval_result: (unit -> term) ref |
84 val eval_result: (unit -> term) ref |
84 val eval_term: theory -> term -> term |
85 val eval_term: theory -> term -> term |
85 val evaluation_conv: cterm -> thm |
86 val evaluation_conv: cterm -> thm |
915 [mk_gen gr module true xs a T, mk_type true T]) Ts) @ |
916 [mk_gen gr module true xs a T, mk_type true T]) Ts) @ |
916 (if member (op =) xs s then [str a] else [])))); |
917 (if member (op =) xs s then [str a] else [])))); |
917 |
918 |
918 val test_fn : (int -> (string * term) list option) ref = ref (fn _ => NONE); |
919 val test_fn : (int -> (string * term) list option) ref = ref (fn _ => NONE); |
919 |
920 |
|
921 fun test_term' ctxt t = |
|
922 let |
|
923 val thy = ProofContext.theory_of ctxt; |
|
924 val (code, gr) = setmp mode ["term_of", "test"] |
|
925 (generate_code_i thy [] "Generated") [("testf", t)]; |
|
926 val frees = Name.names Name.context "a" ((map snd o fst o strip_abs) t); |
|
927 val frees' = frees ~~ |
|
928 map (fn i => "arg" ^ string_of_int i) (1 upto length frees); |
|
929 val s = "structure TestTerm =\nstruct\n\n" ^ |
|
930 cat_lines (map snd code) ^ |
|
931 "\nopen Generated;\n\n" ^ string_of |
|
932 (Pretty.block [str "val () = Codegen.test_fn :=", |
|
933 Pretty.brk 1, str ("(fn i =>"), Pretty.brk 1, |
|
934 mk_let (map (fn ((s, T), s') => |
|
935 (mk_tuple [str s', str (s' ^ "_t")], |
|
936 Pretty.block [mk_gen gr "Generated" false [] "" T, Pretty.brk 1, |
|
937 str "(i + 1)"])) frees') |
|
938 (Pretty.block [str "if ", |
|
939 mk_app false (str "testf") (map (str o snd) frees'), |
|
940 Pretty.brk 1, str "then NONE", |
|
941 Pretty.brk 1, str "else ", |
|
942 Pretty.block [str "SOME ", Pretty.block (str "[" :: |
|
943 flat (separate [str ",", Pretty.brk 1] |
|
944 (map (fn ((s, T), s') => [Pretty.block |
|
945 [str ("(" ^ quote (Symbol.escape s) ^ ","), Pretty.brk 1, |
|
946 str (s' ^ "_t ())")]]) frees')) @ |
|
947 [str "]"])]]), |
|
948 str ");"]) ^ |
|
949 "\n\nend;\n"; |
|
950 val _ = ML_Context.eval_in (SOME ctxt) false Position.none s; |
|
951 in ! test_fn #> (Option.map o map) snd end; |
|
952 |
920 fun test_term thy quiet sz i t = |
953 fun test_term thy quiet sz i t = |
921 let |
954 let |
922 val ctxt = ProofContext.init thy; |
955 val ctxt = ProofContext.init thy; |
923 val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse |
956 val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse |
924 error "Term to be tested contains type variables"; |
957 error "Term to be tested contains type variables"; |
1130 end)); |
1163 end)); |
1131 |
1164 |
1132 val setup = add_codegen "default" default_codegen |
1165 val setup = add_codegen "default" default_codegen |
1133 #> add_tycodegen "default" default_tycodegen |
1166 #> add_tycodegen "default" default_tycodegen |
1134 #> Value.add_evaluator ("SML", eval_term o ProofContext.theory_of) |
1167 #> Value.add_evaluator ("SML", eval_term o ProofContext.theory_of) |
|
1168 #> Quickcheck.add_generator ("SML", test_term') |
1135 #> Code.add_attribute ("unfold", Scan.succeed (Thm.declaration_attribute |
1169 #> Code.add_attribute ("unfold", Scan.succeed (Thm.declaration_attribute |
1136 (fn thm => Context.mapping (add_unfold thm #> Code.add_inline thm) I))); |
1170 (fn thm => Context.mapping (add_unfold thm #> Code.add_inline thm) I))); |
1137 |
1171 |
1138 val _ = Context.>> (Specification.add_theorem_hook test_goal'); |
1172 val _ = Context.>> (Specification.add_theorem_hook test_goal'); |
1139 |
1173 |