(* pretty-prints a term t of cic in an environment l where l is a list of *)
(* identifier names used to resolve DeBrujin indexes. The head of l is the *)
(* name associated to the greatest DeBrujin index in t *)
+let pp ?metasenv =
let rec pp t l =
let module C = Cic in
match t with
| C.Var (uri,exp_named_subst) ->
UriManager.string_of_uri (*UriManager.name_of_uri*) uri ^ pp_exp_named_subst exp_named_subst l
| C.Meta (n,l1) ->
- "?" ^ (string_of_int n) ^ "[" ^
- String.concat " ; "
- (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
- "]"
+ (match metasenv with
+ None ->
+ "?" ^ (string_of_int n) ^ "[" ^
+ String.concat " ; "
+ (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
+ "]"
+ | Some metasenv ->
+ try
+ let _,context,_ = CicUtil.lookup_meta n metasenv in
+ "?" ^ (string_of_int n) ^ "[" ^
+ String.concat " ; "
+ (List.rev
+ (List.map2
+ (fun x y ->
+ match x,y with
+ _, None
+ | None, _ -> "_"
+ | Some _, Some t -> pp t l
+ ) context l1)) ^
+ "]"
+ with
+ CicUtil.Meta_not_found _
+ | Invalid_argument _ ->
+ "???" ^ (string_of_int n) ^ "[" ^
+ String.concat " ; "
+ (List.rev_map (function None -> "_" | Some t -> pp t l) l1) ^
+ "]"
+ )
| C.Sort s ->
(match s with
C.Prop -> "Prop"
| C.MutCase (uri,n1,ty,te,patterns) ->
let connames_and_argsno =
(match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
- C.InductiveDefinition (dl,_,_,_) ->
+ C.InductiveDefinition (dl,_,paramsno,_) ->
let (_,_,_,cons) = get_nth dl (n1+1) in
List.map
- (fun id,ty ->
+ (fun (id,ty) ->
(* this is just an approximation since we do not have
reduction yet! *)
- let rec count_prods =
+ let rec count_prods toskip =
function
- C.Prod (_,_,bo) -> 1 + count_prods bo
+ C.Prod (_,_,bo) when toskip > 0 ->
+ count_prods (toskip - 1) bo
+ | C.Prod (_,_,bo) -> 1 + count_prods 0 bo
| _ -> 0
in
- id, count_prods ty
+ id, count_prods paramsno ty
) cons
| _ -> raise CicPpInternalError
)
(function (uri,t) -> UriManager.name_of_uri uri ^ " \\Assign " ^ pp t l)
exp_named_subst
) ^ "]"
+in
+ pp
;;
-let ppterm t =
- pp t []
+let ppterm ?metasenv t =
+ pp ?metasenv t []
;;
(* ppinductiveType (typename, inductive, arity, cons) *)
cons ""
;;
-let ppcontext ?(sep = "\n") context =
+let ppcontext ?metasenv ?(sep = "\n") context =
let separate s = if s = "" then "" else s ^ sep in
fst (List.fold_right
(fun context_entry (i,name_context) ->
match context_entry with
Some (n,Cic.Decl t) ->
Printf.sprintf "%s%s : %s" (separate i) (ppname n)
- (pp t name_context), (Some n)::name_context
+ (pp ?metasenv t name_context), (Some n)::name_context
| Some (n,Cic.Def (bo,ty)) ->
Printf.sprintf "%s%s : %s := %s" (separate i) (ppname n)
(match ty with
None -> "_"
- | Some ty -> pp ty name_context)
- (pp bo name_context), (Some n)::name_context
+ | Some ty -> pp ?metasenv ty name_context)
+ (pp ?metasenv bo name_context), (Some n)::name_context
| None ->
Printf.sprintf "%s_ :? _" (separate i), None::name_context
) context ("",[]))
(match context_entry with
Some (n,C.Decl at) ->
(separate i) ^
- ppname n ^ ":" ^ pp at name_context ^ " ",
+ ppname n ^ ":" ^
+ pp ~metasenv:conjectures at name_context ^ " ",
(Some n)::name_context
| Some (n,C.Def (at,None)) ->
(separate i) ^
- ppname n ^ ":= " ^ pp at name_context ^ " ",
+ ppname n ^ ":= " ^ pp ~metasenv:conjectures
+ at name_context ^ " ",
(Some n)::name_context
| None ->
(separate i) ^ "_ :? _ ", None::name_context
) context ("",[])
in
conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^
- pp t name_context ^ "\n" ^ i
+ pp ~metasenv:conjectures t name_context ^ "\n" ^ i
) conjectures "" ^
- "\n" ^ pp value [] ^ " : " ^ pp ty []
+ "\n" ^ pp ~metasenv:conjectures value [] ^ " : " ^
+ pp ~metasenv:conjectures ty []
| C.InductiveDefinition (l, params, nparams, _) ->
"Parameters = " ^
String.concat ";" (List.map UriManager.string_of_uri params) ^ "\n" ^