sprintf " in %s%s" ty
(match debug_printing, href_opt with
| true, Some uri ->
- sprintf "(i.e.%s)" (UriManager.string_of_uri uri)
+ sprintf "(i.e.%s)" (NReference.string_of_reference uri)
| _ -> ""))
(match typ with None -> "" | Some t -> sprintf " return %s" (pp_term t))
(pp_patterns patterns)
| Ast.Num (num, _) -> num
| Ast.Sort `Set -> "Set"
| Ast.Sort `Prop -> "Prop"
- | Ast.Sort (`Type _) -> "Type"
- | Ast.Sort (`CProp _)-> "CProp"
| Ast.Sort (`NType s)-> "Type[" ^ s ^ "]"
| Ast.Sort (`NCProp s)-> "CProp[" ^ s ^ "]"
| Ast.Symbol (name, _) -> "'" ^ name
let head_pp =
head ^
(match debug_printing, href with
- | true, Some uri -> sprintf "(i.e.%s)" (UriManager.string_of_uri uri)
+ | true, Some uri -> sprintf "(i.e.%s)" (NReference.string_of_reference uri)
| _ -> "")
in
sprintf "%s \\Rightarrow %s"
| [] -> ""
| params -> " " ^ String.concat " " (List.map (pp_capture_variable pp_term) params)
-let pp_flavour = function
- | `Definition -> "definition"
- | `MutualDefinition -> assert false
- | `Fact -> "fact"
- | `Goal -> "goal"
- | `Lemma -> "lemma"
- | `Remark -> "remark"
- | `Theorem -> "theorem"
- | `Variant -> "variant"
- | `Axiom -> "axiom"
-
let pp_fields pp_term fields =
(if fields <> [] then "\n" else "") ^
String.concat ";\n"
(pp_term typ) (pp_constructors constructors)
in
fst_typ_pp ^ String.concat "" (List.map pp_type tl))
- | Ast.Theorem (`MutualDefinition, name, typ, body,_) ->
- sprintf "<<pretty printing of mutual definitions not implemented yet>>"
| Ast.Theorem (flavour, name, typ, body,_) ->
sprintf "%s %s:\n %s\n%s"
- (pp_flavour flavour)
+ (NCicPp.string_of_flavour flavour)
name
(pp_term typ)
(match body with
env)
let rec pp_cic_appl_pattern = function
- | Ast.UriPattern uri -> UriManager.string_of_uri uri
| Ast.NRefPattern nref -> NReference.string_of_reference nref
| Ast.VarPattern name -> name
| Ast.ImplicitPattern -> "?"