- C.Definition (id, t1, t2, params) ->
- "Definition of " ^ id ^
- "(" ^
- List.fold_right
- (fun (_,x) i ->
- List.fold_right
- (fun x i ->
- U.string_of_uri x ^ match i with "" -> "" | i' -> " " ^ i'
- ) x "" ^ match i with "" -> "" | i' -> " " ^ i'
- ) params "" ^ ")" ^
- ":\n" ^ pp t1 [] ^ " : " ^ pp t2 []
- | C.Axiom (id, ty, params) ->
- "Axiom " ^ id ^ "(" ^
- List.fold_right
- (fun (_,x) i ->
- List.fold_right
- (fun x i ->
- U.string_of_uri x ^ match i with "" -> "" | i' -> " " ^ i'
- ) x "" ^ match i with "" -> "" | i' -> " " ^ i'
- ) params "" ^
- "):\n" ^ pp ty []
- | C.Variable (name, bo, ty) ->
- "Variable " ^ name ^ ":\n" ^ pp ty [] ^ "\n" ^
- (match bo with None -> "" | Some bo -> ":= " ^ pp bo [])
- | C.CurrentProof (name, conjectures, value, ty) ->
- "Current Proof:\n" ^
- List.fold_right
- (fun (n, t) i -> "?" ^ (string_of_int n) ^ ": " ^ pp t [] ^ "\n" ^ i)
- conjectures "" ^
- "\n" ^ pp value [] ^ " : " ^ pp ty []
+ C.Constant (name, Some t1, t2, params) ->
+ "Definition of " ^ name ^
+ "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
+ ")" ^ ":\n" ^ pp t1 [] ^ " : " ^ pp t2 []
+ | C.Constant (name, None, ty, params) ->
+ "Axiom " ^ name ^
+ "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
+ "):\n" ^ pp ty []
+ | C.Variable (name, bo, ty, params) ->
+ "Variable " ^ name ^
+ "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
+ ")" ^ ":\n" ^
+ pp ty [] ^ "\n" ^
+ (match bo with None -> "" | Some bo -> ":= " ^ pp bo [])
+ | C.CurrentProof (name, conjectures, value, ty, params) ->
+ "Current Proof of " ^ name ^
+ "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
+ ")" ^ ":\n" ^
+ let separate s = if s = "" then "" else s ^ " ; " in
+ List.fold_right
+ (fun (n, context, t) i ->
+ let conjectures',name_context =
+ List.fold_right
+ (fun context_entry (i,name_context) ->
+ (match context_entry with
+ Some (n,C.Decl at) ->
+ (separate i) ^
+ ppname n ^ ":" ^ pp at name_context ^ " ",
+ (Some n)::name_context
+ | Some (n,C.Def (at,None)) ->
+ (separate i) ^
+ ppname n ^ ":= " ^ pp at name_context ^ " ",
+ (Some n)::name_context
+ | None ->
+ (separate i) ^ "_ :? _ ", None::name_context
+ | _ -> assert false)
+ ) context ("",[])
+ in
+ conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^
+ pp t name_context ^ "\n" ^ i
+ ) conjectures "" ^
+ "\n" ^ pp value [] ^ " : " ^ pp ty []