equal
deleted
inserted
replaced
25 val T_to_string_eqs: T -> as_string_eqs |
25 val T_to_string_eqs: T -> as_string_eqs |
26 val T_to_input: T -> input |
26 val T_to_input: T -> input |
27 val T_from_string_eqs: theory -> as_string_eqs -> T |
27 val T_from_string_eqs: theory -> as_string_eqs -> T |
28 val T_from_input: Proof.context -> input -> T |
28 val T_from_input: Proof.context -> input -> T |
29 |
29 |
30 val input_to_terms: input -> term list |
30 val input_to_terms: Proof.context -> input -> as_eqs |
31 val eqs_to_input: as_eqs -> as_string_eqs |
31 val eqs_to_input: as_eqs -> as_string_eqs |
32 val program_to_input: program -> input |
32 val program_to_input: program -> input |
33 val for_bdv: program -> T -> input option * T |
33 val for_bdv: program -> T -> input option * T |
34 \<^isac_test>\<open> |
34 \<^isac_test>\<open> |
35 val string_eqs_empty: as_string_eqs |
35 val string_eqs_empty: as_string_eqs |
76 |> map (apfst HOLogic.dest_string) |
76 |> map (apfst HOLogic.dest_string) |
77 |> map (apfst (fn str => (TermC.mk_Free (str, HOLogic.realT))))) |
77 |> map (apfst (fn str => (TermC.mk_Free (str, HOLogic.realT))))) |
78 handle TERM _ => raise TERM ("T_from_input: wrong argument " ^ strs2str' input, []) |
78 handle TERM _ => raise TERM ("T_from_input: wrong argument " ^ strs2str' input, []) |
79 |
79 |
80 val eqs_to_input = map UnparseC.term; |
80 val eqs_to_input = map UnparseC.term; |
81 (*TODO: input requires parse _: _ -> _ option*) |
81 |
82 val input_to_terms = map TermC.str2term; |
82 (* TermC.parse ctxt fails with "c_2 = 0" \<longrightarrow> \<open>c_2 = (0 :: 'a)\<close> and thus requires adapt_to_type *) |
|
83 fun input_to_terms ctxt strs = strs |
|
84 |> map (TermC.parse ctxt) |
|
85 |> map (Model_Pattern.adapt_term_to_type ctxt) |
83 |
86 |
84 fun program_to_input sub = (sub |
87 fun program_to_input sub = (sub |
85 |> HOLogic.dest_list |
88 |> HOLogic.dest_list |
86 |> map HOLogic.dest_prod |
89 |> map HOLogic.dest_prod |
87 |> map (fn (e1, e2) => (HOLogic.dest_string e1, UnparseC.term e2)) |
90 |> map (fn (e1, e2) => (HOLogic.dest_string e1, UnparseC.term e2)) |