65 |> map (apfst (enclose "''" "''"))) |
65 |> map (apfst (enclose "''" "''"))) |
66 |> map pair2str |
66 |> map pair2str |
67 handle TERM _ => raise TERM ("T_to_input: wrong argument " ^ to_string subst_rew, []) |
67 handle TERM _ => raise TERM ("T_to_input: wrong argument " ^ to_string subst_rew, []) |
68 |
68 |
69 fun T_from_string_eqs thy s = map (TermC.dest_equals o (TermC.parse_patt thy)) s; |
69 fun T_from_string_eqs thy s = map (TermC.dest_equals o (TermC.parse_patt thy)) s; |
|
70 (*TODO: input requires parse _: _ -> _ option*) |
70 fun T_from_input thy input = (input |
71 fun T_from_input thy input = (input |
71 |> map (TermC.parse_patt thy(*FIXME use context, get type of snd (e.g. x,y,z), copy to fst*)) |
72 |> map (TermC.parse_patt thy(*FIXME use context, get type of snd (e.g. x,y,z), copy to fst*)) |
72 |> map TermC.isapair2pair |
73 |> map TermC.isapair2pair |
73 |> map (apfst HOLogic.dest_string) |
74 |> map (apfst HOLogic.dest_string) |
74 |> map (apfst (fn str => (TermC.mk_Free (str, HOLogic.realT))))) |
75 |> map (apfst (fn str => (TermC.mk_Free (str, HOLogic.realT))))) |
75 handle TERM _ => raise TERM ("T_from_input: wrong argument " ^ strs2str' input, []) |
76 handle TERM _ => raise TERM ("T_from_input: wrong argument " ^ strs2str' input, []) |
76 |
77 |
|
78 val eqs_to_input = map UnparseC.term; |
|
79 (*TODO: input requires parse _: _ -> _ option*) |
77 val input_to_terms = map TermC.str2term; |
80 val input_to_terms = map TermC.str2term; |
78 val eqs_to_input = map UnparseC.term; |
|
79 |
81 |
80 fun program_to_input sub = (sub |
82 fun program_to_input sub = (sub |
81 |> HOLogic.dest_list |
83 |> HOLogic.dest_list |
82 |> map HOLogic.dest_prod |
84 |> map HOLogic.dest_prod |
83 |> map (fn (e1, e2) => (HOLogic.dest_string e1, UnparseC.term e2)) |
85 |> map (fn (e1, e2) => (HOLogic.dest_string e1, UnparseC.term e2)) |