| `Exists -> "exists"
| `Forall -> "forall"
-let pp_literal =
+(* XXX: ignoring the optional CSYMBOL
+ * (it's fine if this is only used for pretty printing output notations) *)
+let pp_literal (_,t) =
if debug_printing then
- (function (* debugging version *)
- | `Symbol s -> sprintf "symbol(%s)" s
- | `Keyword s -> sprintf "keyword(%s)" s
- | `Number s -> sprintf "number(%s)" s)
- else
- (function
- | `Symbol s
- | `Keyword s
- | `Number s -> s)
+ (match t with (* debugging version *)
+ | `Symbol _ ->
+ sprintf "symbol(%s)" (NotationUtil.string_of_literal t)
+ | `Keyword _ ->
+ sprintf "keyword(%s)" (NotationUtil.string_of_literal t)
+ | `Number _ -> sprintf "number(%s)" (NotationUtil.string_of_literal t))
+ else NotationUtil.string_of_literal t
let pp_pos =
function
(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
+ | Ast.Ident (id,`Uri u) -> ("U:(" ^ id ^ "," ^ u ^ ")")
+ | _ -> "E"
+ in
let pp_term = pp_term status in
let t_pp =
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))
- | Ast.Binder (`Forall, (Ast.Ident ("_", None), typ), body)
- | Ast.Binder (`Pi, (Ast.Ident ("_", None), typ), body) ->
+ | Ast.Binder (`Forall, (Ast.Ident ("_", `Ambiguous), typ), body)
+ | Ast.Binder (`Forall, (Ast.Ident ("_", `Rel), typ), body)
+ | Ast.Binder (`Pi, (Ast.Ident ("_", `Ambiguous), typ), body)
+ | Ast.Binder (`Pi, (Ast.Ident ("_", `Rel), typ), body) ->
sprintf "%s \\to %s"
(match typ with None -> "?" | Some typ -> pp_term typ)
(pp_term ~pp_parens:true body)
| Ast.Binder (kind, var, body) ->
+(*
+ * sprintf "\\%s[%s] %s.%s" (pp_binder kind) (pp_ident var) (pp_capture_variable pp_term var)
+ *)
sprintf "\\%s %s.%s" (pp_binder kind) (pp_capture_variable pp_term var)
(pp_term ~pp_parens:true body)
| Ast.Case (term, indtype, typ, patterns) ->
| 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)
| _ -> ""))
(match kind with `Inductive -> "rec" | `CoInductive -> "corec")
(String.concat " and " (List.map map definitions))
(pp_term term)
- | Ast.Ident (name, Some []) | Ast.Ident (name, None)
- | Ast.Uri (name, Some []) | Ast.Uri (name, None) -> name
+ | Ast.Ident (name, _ ) -> pp_ident t
| Ast.NRef nref -> NReference.string_of_reference nref
| Ast.NCic cic -> status#ppterm ~metasenv:[] ~context:[] ~subst:[] cic
- | Ast.Ident (name, Some substs)
- | Ast.Uri (name, Some substs) ->
- sprintf "%s \\subst [%s]" name (pp_substs status substs)
| Ast.Implicit `Vector -> "…"
| Ast.Implicit `JustOne -> "?"
| Ast.Implicit (`Tagged name) -> "?"^name
| 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, _
| true, Ast.Implicit _
| true, Ast.UserInput
| true, Ast.Sort _
- | true, Ast.Ident (_, Some [])
- | true, Ast.Ident (_, None) -> t_pp
- | _ -> sprintf "(%s)" t_pp
-
-and pp_subst status (name, term) =
- sprintf "%s \\Assign %s" name (pp_term status term)
-and pp_substs status substs = String.concat "; " (List.map (pp_subst status) substs)
+ | true, Ast.Ident _ -> t_pp
+ | _ -> sprintf "(%s)" t_pp
and pp_pattern status =
function
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"
and pp_sep_opt = function
| None -> ""
- | Some sep -> sprintf " sep %s" (pp_literal sep)
+ | Some sep -> sprintf " sep %s" (pp_literal (None,sep))
and pp_variable = function
| Ast.NumVar s -> "number " ^ 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.DisambiguationValue _ -> 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 "; "