73 val eta_expand: term -> term list -> int -> term |
73 val eta_expand: term -> term list -> int -> term |
74 val strip_tname: string -> string |
74 val strip_tname: string -> string |
75 val mk_type: bool -> typ -> Pretty.T |
75 val mk_type: bool -> typ -> Pretty.T |
76 val mk_term_of: codegr -> string -> bool -> typ -> Pretty.T |
76 val mk_term_of: codegr -> string -> bool -> typ -> Pretty.T |
77 val mk_gen: codegr -> string -> bool -> string list -> string -> typ -> Pretty.T |
77 val mk_gen: codegr -> string -> bool -> string list -> string -> typ -> Pretty.T |
78 val test_fn: (int -> (string * term) list option) ref |
78 val test_fn: (int -> term list option) ref |
79 val test_term: Proof.context -> term -> int -> term list option |
79 val test_term: Proof.context -> term -> int -> term list option |
80 val eval_result: (unit -> term) ref |
80 val eval_result: (unit -> term) ref |
81 val eval_term: theory -> term -> term |
81 val eval_term: theory -> term -> term |
82 val evaluation_conv: cterm -> thm |
82 val evaluation_conv: cterm -> thm |
83 val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list |
83 val parse_mixfix: (string -> 'a) -> string -> 'a mixfix list |
869 mk_gen gr module true xs a U, mk_type true U] |
869 mk_gen gr module true xs a U, mk_type true U] |
870 | _ => maps (fn T => |
870 | _ => maps (fn T => |
871 [mk_gen gr module true xs a T, mk_type true T]) Ts) @ |
871 [mk_gen gr module true xs a T, mk_type true T]) Ts) @ |
872 (if member (op =) xs s then [str a] else [])))); |
872 (if member (op =) xs s then [str a] else [])))); |
873 |
873 |
874 val test_fn : (int -> (string * term) list option) ref = ref (fn _ => NONE); |
874 val test_fn : (int -> term list option) ref = ref (fn _ => NONE); |
875 |
875 |
876 fun test_term ctxt t = |
876 fun test_term ctxt t = |
877 let |
877 let |
878 val thy = ProofContext.theory_of ctxt; |
878 val thy = ProofContext.theory_of ctxt; |
879 val (code, gr) = setmp mode ["term_of", "test"] |
879 val (code, gr) = setmp mode ["term_of", "test"] |
880 (generate_code_i thy [] "Generated") [("testf", t)]; |
880 (generate_code_i thy [] "Generated") [("testf", t)]; |
881 val frees = Name.names Name.context "a" ((map snd o fst o strip_abs) t); |
881 val Ts = map snd (fst (strip_abs t)); |
882 val frees' = frees ~~ |
882 val args = map_index (fn (i, T) => ("arg" ^ string_of_int i, T)) Ts; |
883 map (fn i => "arg" ^ string_of_int i) (1 upto length frees); |
|
884 val s = "structure TestTerm =\nstruct\n\n" ^ |
883 val s = "structure TestTerm =\nstruct\n\n" ^ |
885 cat_lines (map snd code) ^ |
884 cat_lines (map snd code) ^ |
886 "\nopen Generated;\n\n" ^ string_of |
885 "\nopen Generated;\n\n" ^ string_of |
887 (Pretty.block [str "val () = Codegen.test_fn :=", |
886 (Pretty.block [str "val () = Codegen.test_fn :=", |
888 Pretty.brk 1, str ("(fn i =>"), Pretty.brk 1, |
887 Pretty.brk 1, str ("(fn i =>"), Pretty.brk 1, |
889 mk_let (map (fn ((s, T), s') => |
888 mk_let (map (fn (s, T) => |
890 (mk_tuple [str s', str (s' ^ "_t")], |
889 (mk_tuple [str s, str (s ^ "_t")], |
891 Pretty.block [mk_gen gr "Generated" false [] "" T, Pretty.brk 1, |
890 Pretty.block [mk_gen gr "Generated" false [] "" T, Pretty.brk 1, |
892 str "(i + 1)"])) frees') |
891 str "i"])) args) |
893 (Pretty.block [str "if ", |
892 (Pretty.block [str "if ", |
894 mk_app false (str "testf") (map (str o snd) frees'), |
893 mk_app false (str "testf") (map (str o fst) args), |
895 Pretty.brk 1, str "then NONE", |
894 Pretty.brk 1, str "then NONE", |
896 Pretty.brk 1, str "else ", |
895 Pretty.brk 1, str "else ", |
897 Pretty.block [str "SOME ", Pretty.block (str "[" :: |
896 Pretty.block [str "SOME ", Pretty.block (str "[" :: |
898 flat (separate [str ",", Pretty.brk 1] |
897 Pretty.commas (map (fn (s, _) => str (s ^ "_t ()")) args) @ |
899 (map (fn ((s, T), s') => [Pretty.block |
|
900 [str ("(" ^ quote (Symbol.escape s) ^ ","), Pretty.brk 1, |
|
901 str (s' ^ "_t ())")]]) frees')) @ |
|
902 [str "]"])]]), |
898 [str "]"])]]), |
903 str ");"]) ^ |
899 str ");"]) ^ |
904 "\n\nend;\n"; |
900 "\n\nend;\n"; |
905 val _ = ML_Context.eval_in (SOME ctxt) false Position.none s; |
901 val _ = ML_Context.eval_in (SOME ctxt) false Position.none s; |
906 in ! test_fn #> (Option.map o map) snd end; |
902 in ! test_fn end; |
907 |
903 |
908 |
904 |
909 |
905 |
910 (**** Evaluator for terms ****) |
906 (**** Evaluator for terms ****) |
911 |
907 |