open CicNotationEnv
open CicNotationPt
-let print_attributes = true
+ (* when set to true debugging information, not in sync with input syntax, will
+ * be added to the output of pp_term.
+ * set to false if you need, for example, cut and paste from matitac output to
+ * matitatop *)
+let debug_printing = false
let pp_binder = function
| `Lambda -> "lambda"
| `Exists -> "exists"
| `Forall -> "forall"
-(* let pp_literal = function (* debugging version *)
+let pp_literal = function (* debugging version *)
| `Symbol s -> sprintf "symbol(%s)" s
| `Keyword s -> sprintf "keyword(%s)" s
- | `Number s -> sprintf "number(%s)" s *)
+ | `Number s -> sprintf "number(%s)" s
-let pp_literal = function
+(* let pp_literal = function
| `Symbol s
| `Keyword s
- | `Number s -> s
+ | `Number s -> s *)
let rec pp_term ?(pp_parens = true) t =
let t_pp =
match t with
-(* | AttributedTerm (`Href _, term) when print_attributes ->
- sprintf "#[%s]" (pp_term term)
- | AttributedTerm (_, term) when print_attributes ->
- sprintf "@[%s]" (pp_term term) *)
- | AttributedTerm (`Raw (text, None), _) -> text
- | AttributedTerm (`Raw (text, Some `Ast), _) -> sprintf "@{%s}" text
- | AttributedTerm (`Raw (text, Some `Meta), _) -> sprintf "${%s}" text
+ | AttributedTerm (`Href _, term) when debug_printing ->
+ sprintf "#[%s]" (pp_term ~pp_parens:false term)
+ | AttributedTerm (`IdRef id, term) when debug_printing ->
+ sprintf "x(%s)[%s]" id (pp_term ~pp_parens:false term)
+ | AttributedTerm (_, term) when debug_printing ->
+ sprintf "@[%s]" (pp_term ~pp_parens:false term)
+ | AttributedTerm (`Raw text, _) -> text
| AttributedTerm (_, term) -> pp_term ~pp_parens:false term
| Appl terms ->
| Sort `Prop -> "Prop"
| Sort `Type -> "Type"
| Sort `CProp -> "CProp"
- | Symbol (name, _) -> name
+ | Symbol (name, _) -> "'" ^ name
| UserInput -> ""