- | Inductive (params, types) ->
- let pp_params = function
- | [] -> ""
- | params ->
- " " ^
- String.concat " "
- (List.map
- (fun (name, typ) -> sprintf "(%s:%s)" name (pp_term typ))
- params)
- in
- let pp_constructors constructors =
- String.concat "\n"
- (List.map (fun (name, typ) -> sprintf "| %s: %s" name (pp_term typ))
- constructors)
- in
- let pp_type (name, _, typ, constructors) =
- sprintf "\nwith %s: %s \\def\n%s" name (pp_term typ)
- (pp_constructors constructors)
- in
- (match types with
- | [] -> assert false
- | (name, inductive, typ, constructors) :: tl ->
- let fst_typ_pp =
- sprintf "%sinductive %s%s: %s \\def\n%s"
- (if inductive then "" else "co") name (pp_params params)
- (pp_term typ) (pp_constructors constructors)
- in
- fst_typ_pp ^ String.concat "" (List.map pp_type tl))
- | Theorem (flavour, name, typ, body) ->
- sprintf "%s %s: %s %s"
- (pp_flavour flavour)
- (match name with None -> "" | Some name -> name)
- (pp_term typ)
- (match body with
- | None -> ""
- | Some body -> "\\def " ^ pp_term body)
- | Undo None -> "Undo"
- | Undo (Some n) -> sprintf "Undo %d" n
+(* | Undo (_, None) -> "Undo"
+ | Undo (_, Some n) -> sprintf "Undo %d" n *)
+ | Print (_, name) -> sprintf "Print \"%s\"" name
+ | Quit _ -> "Quit"
+
+let pp_macro_ast = pp_macro pp_term_ast
+let pp_macro_cic = pp_macro pp_term_cic
+
+let pp_alias = function
+ | Ident_alias (id, uri) -> sprintf "alias id \"%s\" = \"%s\"" id uri
+ | Symbol_alias (symb, instance, desc) ->
+ sprintf "alias symbol \"%s\" (instance %d) = \"%s\""
+ symb instance desc
+ | Number_alias (instance,desc) ->
+ sprintf "alias num (instance %d) = \"%s\"" instance desc
+
+let pp_params = function
+ | [] -> ""
+ | params ->
+ " " ^
+ String.concat " "
+ (List.map
+ (fun (name, typ) -> sprintf "(%s:%s)" name (pp_term_ast typ))
+ params)
+
+let pp_fields fields =
+ (if fields <> [] then "\n" else "") ^
+ String.concat ";\n"
+ (List.map (fun (name,ty) -> " " ^ name ^ ": " ^ pp_term_ast ty) fields)
+
+let pp_obj = function
+ | Inductive (params, types) ->
+ let pp_constructors constructors =
+ String.concat "\n"
+ (List.map (fun (name, typ) -> sprintf "| %s: %s" name (pp_term_ast typ))
+ constructors)
+ in
+ let pp_type (name, _, typ, constructors) =
+ sprintf "\nwith %s: %s \\def\n%s" name (pp_term_ast typ)
+ (pp_constructors constructors)
+ in
+ (match types with
+ | [] -> assert false
+ | (name, inductive, typ, constructors) :: tl ->
+ let fst_typ_pp =
+ sprintf "%sinductive %s%s: %s \\def\n%s"
+ (if inductive then "" else "co") name (pp_params params)
+ (pp_term_ast typ) (pp_constructors constructors)
+ in
+ fst_typ_pp ^ String.concat "" (List.map pp_type tl))
+ | Theorem (flavour, name, typ, body) ->
+ sprintf "%s %s: %s %s"
+ (pp_flavour flavour)
+ name
+ (pp_term_ast typ)
+ (match body with
+ | None -> ""
+ | Some body -> "\\def " ^ pp_term_ast body)
+ | Record (params,name,ty,fields) ->
+ "record " ^ name ^ " " ^ pp_params params ^ " \\def {" ^
+ pp_fields fields ^ "}"