equal
deleted
inserted
replaced
673 |
673 |
674 fun rename_vars_term renaming = map_vars (fn v => the (AList.lookup (op =) renaming v)) |
674 fun rename_vars_term renaming = map_vars (fn v => the (AList.lookup (op =) renaming v)) |
675 |
675 |
676 fun rename_vars_prem renaming = map_term_prem (rename_vars_term renaming) |
676 fun rename_vars_prem renaming = map_term_prem (rename_vars_term renaming) |
677 |
677 |
678 fun is_prolog_conform v = |
|
679 forall (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s) (Symbol.explode v) |
|
680 |
|
681 fun mk_renaming v renaming = |
678 fun mk_renaming v renaming = |
682 (v, mk_conform first_upper "Var" (map snd renaming) v) :: renaming |
679 (v, mk_conform first_upper "Var" (map snd renaming) v) :: renaming |
683 |
680 |
684 fun rename_vars_clause ((rel, args), prem) = |
681 fun rename_vars_clause ((rel, args), prem) = |
685 let |
682 let |
842 |
839 |
843 val scan_var = |
840 val scan_var = |
844 Scan.many1 |
841 Scan.many1 |
845 (fn s => Symbol.is_ascii_upper s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s) |
842 (fn s => Symbol.is_ascii_upper s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s) |
846 |
843 |
847 val scan_ident = |
|
848 Scan.repeat (Scan.one |
|
849 (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s)) |
|
850 |
|
851 fun dest_Char (Symbol.Char s) = s |
844 fun dest_Char (Symbol.Char s) = s |
852 |
845 |
853 val string_of = implode o map (dest_Char o Symbol.decode) |
846 val string_of = implode o map (dest_Char o Symbol.decode) |
854 |
|
855 val is_atom_ident = forall Symbol.is_ascii_lower |
|
856 |
|
857 val is_var_ident = |
|
858 forall (fn s => |
|
859 Symbol.is_ascii_upper s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s) |
|
860 |
847 |
861 fun int_of_symbol_list xs = fold (fn x => fn s => s * 10 + (ord x - ord "0")) xs 0 |
848 fun int_of_symbol_list xs = fold (fn x => fn s => s * 10 + (ord x - ord "0")) xs 0 |
862 |
849 |
863 fun scan_terms xs = (((scan_term --| $$ ",") ::: scan_terms) |
850 fun scan_terms xs = (((scan_term --| $$ ",") ::: scan_terms) |
864 || (scan_term >> single)) xs |
851 || (scan_term >> single)) xs |