diff options
Diffstat (limited to 'kernel/names.ml')
| -rw-r--r-- | kernel/names.ml | 38 |
1 files changed, 38 insertions, 0 deletions
diff --git a/kernel/names.ml b/kernel/names.ml index 09c98eafc3..c153169ab4 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -332,3 +332,41 @@ type id_key = inv_rel_key tableKey +(* spiwack : internal representation printing *) + +let string_of_identifier id = id +let string_of_module_ident id = id +let string_of_label lbl = lbl (* not public *) +let string_of_dir_path path = "["^String.concat "; " (List.map string_of_module_ident path)^"]" +let string_of_name = + function + | Name id -> "Name "^id + | Anonymous -> "Anonymous" + +let rec string_of_module_path = (* not public *) + function + | MPfile path -> "MPfile "^string_of_dir_path path + | MPbound _ -> "MPbound "^"?" (*of mod_bound_id*) + | MPself _ -> "MPself "^"?" (* of mod_self_id *) + | MPdot (mpath, lbl) -> + "MPdot ("^string_of_module_path mpath^", "^string_of_label lbl^")" + (* of module_path * label *) + +let string_of_kernel_name = (* not public *) + function + |(mpath, path, lbl) -> + "("^string_of_module_path mpath^", "^ + string_of_dir_path path^", "^ + string_of_label lbl ^")" + +let string_of_constant = string_of_kernel_name +let string_of_mutual_inductive = string_of_kernel_name +let string_of_inductive = + function + | (mind, i) -> "("^string_of_mutual_inductive mind^", "^string_of_int i^")" +let string_of_constructor = + function + | (ind, i) -> "("^string_of_inductive ind^", "^string_of_int i^")" + + +(* /spiwack *) |