(List.map (fun (_, n, v) -> sprintf "%s=%s" n v) attrs))
| `Level (prec) -> sprintf "L(%d)" prec
| `Raw _ -> "R"
- | `Loc _ -> "@"
+ | `Loc l -> let x,y = HExtlib.loc_of_floc l in
+ "@" ^ (string_of_int x) ^ "," ^ (string_of_int y)
| `ChildPos p -> sprintf "P(%s)" (pp_pos p)
let pp_capture_variable pp_term =
| term, Some typ -> "(" ^ pp_term (* ~pp_parens:false *) term ^ ": " ^ pp_term typ ^ ")"
let rec pp_term (status : #NCic.status) ?(pp_parens = true) t =
+ let debug_printing = true in
let pp_ident = function
| Ast.Ident (id,`Ambiguous) -> "A:" ^ id
| Ast.Ident (id,`Rel) -> "R:" ^ id
match t with
| Ast.AttributedTerm (attr, term) when debug_printing ->
sprintf "%s[%s]" (pp_attribute attr) (pp_term ~pp_parens:false term)
- | Ast.AttributedTerm (`Raw text, _) -> text
+ | Ast.AttributedTerm (`Raw text, t) -> "RAW:(" ^ (pp_term t) ^ ")"
| Ast.AttributedTerm (_, term) -> pp_term ~pp_parens:false term
| Ast.Appl terms ->
sprintf "%s" (String.concat " " (List.map pp_term terms))
| None -> ""
| Some (ty, href_opt) ->
sprintf " in %s%s" ty
- (match debug_printing, href_opt with
+ (match (*debug_printing*) true, href_opt with
| true, Some uri ->
sprintf "(i.e.%s)" (NReference.string_of_reference uri)
| _ -> ""))
| Ast.Sort `Prop -> "Prop"
| Ast.Sort (`NType s)-> "Type[" ^ s ^ "]"
| Ast.Sort (`NCProp s)-> "CProp[" ^ s ^ "]"
- | Ast.Symbol (name, _) -> "'" ^ name
+ | Ast.Symbol (name, None) -> "'" ^ name
+ | Ast.Symbol (name, Some (_,desc)) -> "'" ^ name ^ ":" ^ desc
| Ast.UserInput -> "%"
- | Ast.Literal l -> pp_literal l
- | Ast.Layout l -> pp_layout status l
- | Ast.Magic m -> pp_magic status m
- | Ast.Variable v -> pp_variable v
+ | Ast.Literal l -> "literal:(" ^ (pp_literal l) ^ ")"
+ | Ast.Layout l -> "layout:(" ^ (pp_layout status l) ^ ")"
+ | Ast.Magic m -> "magic:(" ^ (pp_magic status m) ^ ")"
+ | Ast.Variable v -> "variable:" ^ (pp_variable v)
in
match pp_parens, t with
| false, _
Ast.Pattern (head, href, vars), term ->
let head_pp =
head ^
- (match debug_printing, href with
+ (match (*debug_printing*)true, href with
| true, Some uri -> sprintf "(i.e.%s)" (NReference.string_of_reference uri)
+ | true, None -> "(i.e.ambiguous)"
| _ -> "")
in
sprintf "%s \\Rightarrow %s"
| Env.OptValue (Some v) -> "Some " ^ pp_value status v
| Env.OptValue None -> "None"
| Env.ListValue l -> sprintf "[%s]" (String.concat "; " (List.map (pp_value status) l))
+ | Env.LocValue l -> sprintf "#"
let rec pp_value_type =
function
| Env.NumType -> "Number"
| Env.OptType t -> "Maybe " ^ pp_value_type t
| Env.ListType l -> "List " ^ pp_value_type l
+ | Env.NoType -> "NoType"
let pp_env status env =
String.concat "; "