(* Utility functions *)
-let string_of_name =
+let ppname =
function
Cic.Name s -> s
| Cic.Anonymous -> "_"
(match get_nth l n with
Some (C.Name s) -> s
| Some C.Anonymous -> "__" ^ string_of_int n
- | _ -> raise CicPpInternalError
+ | None -> "_hidden_" ^ string_of_int n
)
with
NotEnoughElements -> string_of_int (List.length l - n)
| C.Meta (n,l1) ->
"?" ^ (string_of_int n) ^ "[" ^
String.concat " ; "
- (List.map (function None -> "_" | Some t -> pp t l) l1) ^
+ (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
"]"
| C.Sort s ->
(match s with
- C.Prop -> "Prop"
- | C.Set -> "Set"
- | C.Type -> "Type"
+ C.Prop -> "Prop"
+ | C.Set -> "Set"
+ | C.Type -> "Type"
+ | C.CProp -> "CProp"
)
- | C.Implicit -> "?"
+ | C.Implicit _ -> "?"
| C.Prod (b,s,t) ->
(match b with
C.Name n -> "(" ^ n ^ ":" ^ pp s l ^ ")" ^ pp t ((Some b)::l)
)
| C.Cast (v,t) -> pp v l
| C.Lambda (b,s,t) ->
- "[" ^ string_of_name b ^ ":" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
+ "[" ^ ppname b ^ ":" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
| C.LetIn (b,s,t) ->
- "[" ^ string_of_name b ^ ":=" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
+ "[" ^ ppname b ^ ":=" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
| C.Appl li ->
"(" ^
(List.fold_right
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) ->
+ List.fold_right
+ (fun context_entry (i,name_context) ->
+ (match context_entry with
+ Some (n,C.Decl at) ->
(separate i) ^
- string_of_name n ^ ":" ^ pp at name_context ^ " ",
- (Some n)::name_context
- | Some (n,C.Def at) ->
+ ppname n ^ ":" ^ pp at name_context ^ " ",
+ (Some n)::name_context
+ | Some (n,C.Def (at,None)) ->
(separate i) ^
- string_of_name n ^ ":= " ^ pp at name_context ^ " ",
- (Some n)::name_context
+ ppname n ^ ":= " ^ pp at name_context ^ " ",
+ (Some n)::name_context
| None ->
- (separate i) ^ "_ :? _ ", None::name_context)
- ) context ("",[])
+ (separate i) ^ "_ :? _ ", None::name_context
+ | _ -> assert false)
+ ) context ("",[])
in
conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^
pp t name_context ^ "\n" ^ i