equal
deleted
inserted
replaced
63 |
63 |
64 fun is_alpha_space_digit_or_neg ch = |
64 fun is_alpha_space_digit_or_neg ch = |
65 (ch = "~") orelse (ReconOrderClauses.is_alpha ch) orelse |
65 (ch = "~") orelse (ReconOrderClauses.is_alpha ch) orelse |
66 (ReconOrderClauses.is_digit ch) orelse ( ch = " "); |
66 (ReconOrderClauses.is_digit ch) orelse ( ch = " "); |
67 |
67 |
68 fun lit_string_with_nums t = let val termstr = Term.str_of_term t |
68 fun string_of_term (Const(s,_)) = s |
|
69 | string_of_term (Free(s,_)) = s |
|
70 | string_of_term (Var(ix,_)) = Term.string_of_vname ix |
|
71 | string_of_term (Bound i) = string_of_int i |
|
72 | string_of_term (Abs(x,_,t)) = "%" ^ x ^ ". " ^ string_of_term t |
|
73 | string_of_term (s $ t) = |
|
74 "(" ^ string_of_term s ^ " " ^ string_of_term t ^ ")" |
|
75 |
|
76 (* FIXME string_of_term is quite unreliable here *) |
|
77 fun lit_string_with_nums t = let val termstr = string_of_term t |
69 val exp_term = explode termstr |
78 val exp_term = explode termstr |
70 in |
79 in |
71 implode(List.filter is_alpha_space_digit_or_neg exp_term) |
80 implode(List.filter is_alpha_space_digit_or_neg exp_term) |
72 end |
81 end |
73 |
82 |