+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 ^ "}"
+
+
+let pp_command = function
+ | Qed _ -> "qed"
+ | Drop _ -> "drop"
+ | Set (_, name, value) -> sprintf "Set \"%s\" \"%s\"" name value
+ | Coercion (_,_) -> "Coercion IMPLEMENT ME!!!!!"
+ | Alias (_,s) -> pp_alias s
+ | Obj (_,obj) -> pp_obj obj
+
+let rec pp_tactical = function
+ | Tactic (_, tac) -> pp_tactic tac
+ | Do (_, count, tac) -> sprintf "do %d %s" count (pp_tactical tac)
+ | Repeat (_, tac) -> "repeat " ^ pp_tactical tac
+ | Seq (_, tacs) -> pp_tacticals tacs
+ | Then (_, tac, tacs) ->
+ sprintf "%s [%s]" (pp_tactical tac) (pp_tacticals tacs)
+ | Tries (_, tacs) -> sprintf "tries [%s]" (pp_tacticals tacs)
+ | Try (_, tac) -> "try " ^ pp_tactical tac