(******************************************************************************)
exception CicPpInternalError;;
+exception NotEnoughElements;;
(* Utility functions *)
| Cic.Anonimous -> "_"
;;
-(* get_nth l n returns the nth element of the list l if it exists or raise *)
-(* a CicPpInternalError if l has less than n elements or n < 1 *)
+(* get_nth l n returns the nth element of the list l if it exists or *)
+(* raises NotEnoughElements if l has less than n elements *)
let rec get_nth l n =
match (n,l) with
(1, he::_) -> he
| (n, he::tail) when n > 1 -> get_nth tail (n-1)
- | (_,_) -> raise CicPpInternalError
+ | (_,_) -> raise NotEnoughElements
;;
(* pp t l *)
let module C = Cic in
match t with
C.Rel n ->
- (match get_nth l n with
- C.Name s -> s
- | _ -> raise CicPpInternalError
- )
+ begin
+ try
+ (match get_nth l n with
+ Some (C.Name s) -> s
+ | _ -> raise CicPpInternalError
+ )
+ with
+ NotEnoughElements -> string_of_int (List.length l - n)
+ end
| C.Var uri -> UriManager.name_of_uri uri
- | C.Meta n -> "?" ^ (string_of_int n)
+ | C.Meta (n,l1) ->
+ "?" ^ (string_of_int n) ^ "[" ^
+ String.concat " ; "
+ (List.map (function None -> "_" | Some t -> pp t l) l1) ^
+ "]"
| C.Sort s ->
(match s with
C.Prop -> "Prop"
| C.Implicit -> "?"
| C.Prod (b,s,t) ->
(match b with
- C.Name n -> "(" ^ n ^ ":" ^ pp s l ^ ")" ^ pp t (b::l)
- | C.Anonimous -> "(" ^ pp s l ^ "->" ^ pp t (b::l) ^ ")"
+ C.Name n -> "(" ^ n ^ ":" ^ pp s l ^ ")" ^ pp t ((Some b)::l)
+ | C.Anonimous -> "(" ^ 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 (b::l)
+ "[" ^ string_of_name b ^ ":" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
| C.LetIn (b,s,t) ->
- "[" ^ string_of_name b ^ ":=" ^ pp s l ^ "]" ^ pp t (b::l)
+ "[" ^ string_of_name b ^ ":=" ^ pp s l ^ "]" ^ pp t ((Some b)::l)
| C.Appl li ->
"(" ^
(List.fold_right
li ""
) ^ ")"
| C.Const (uri,_) -> UriManager.name_of_uri uri
- | C.Abst uri -> UriManager.name_of_uri uri
| C.MutInd (uri,_,n) ->
- (match CicEnvironment.get_obj uri with
- C.InductiveDefinition (dl,_,_) ->
- let (name,_,_,_) = get_nth dl (n+1) in
- name
- | _ -> raise CicPpInternalError
- )
+ begin
+ try
+ (match CicEnvironment.get_obj uri with
+ C.InductiveDefinition (dl,_,_) ->
+ let (name,_,_,_) = get_nth dl (n+1) in
+ name
+ | _ -> raise CicPpInternalError
+ )
+ with
+ NotEnoughElements ->
+ UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n + 1)
+ end
| C.MutConstruct (uri,_,n1,n2) ->
- (match CicEnvironment.get_obj uri with
- C.InductiveDefinition (dl,_,_) ->
- let (_,_,_,cons) = get_nth dl (n1+1) in
- let (id,_,_) = get_nth cons n2 in
- id
- | _ -> raise CicPpInternalError
- )
+ begin
+ try
+ (match CicEnvironment.get_obj uri with
+ C.InductiveDefinition (dl,_,_) ->
+ let (_,_,_,cons) = get_nth dl (n1+1) in
+ let (id,_,_) = get_nth cons n2 in
+ id
+ | _ -> raise CicPpInternalError
+ )
+ with
+ NotEnoughElements ->
+ UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n1 + 1) ^ "/" ^
+ string_of_int n2
+ end
| C.MutCase (uri,_,n1,ty,te,patterns) ->
let connames =
(match CicEnvironment.get_obj uri with
"\nend"
| C.Fix (no, funs) ->
let snames = List.map (fun (name,_,_,_) -> name) funs in
- let names = List.rev (List.map (function name -> C.Name name) snames) in
+ let names =
+ List.rev (List.map (function name -> Some (C.Name name)) snames)
+ in
"\nFix " ^ get_nth snames (no + 1) ^ " {" ^
List.fold_right
(fun (name,ind,ty,bo) i -> "\n" ^ name ^ " / " ^ string_of_int ind ^
"}\n"
| C.CoFix (no,funs) ->
let snames = List.map (fun (name,_,_) -> name) funs in
- let names = List.rev (List.map (function name -> C.Name name) snames) in
+ let names =
+ List.rev (List.map (function name -> Some (C.Name name)) snames)
+ in
"\nCoFix " ^ get_nth snames (no + 1) ^ " {" ^
List.fold_right
(fun (name,ty,bo) i -> "\n" ^ name ^
"}\n"
;;
+let ppterm t =
+ pp t []
+;;
+
(* ppinductiveType (typename, inductive, arity, cons) names *)
(* pretty-prints a single inductive definition (typename, inductive, arity, *)
(* cons) where the cic terms in the inductive definition need to be *)
(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 []
+ 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) ^
+ string_of_name n ^ ":" ^ pp at name_context ^ " ",
+ (Some n)::name_context
+ | Some (n,C.Def at) ->
+ (separate i) ^
+ string_of_name n ^ ":= " ^ pp 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
+ ) conjectures "" ^
+ "\n" ^ pp value [] ^ " : " ^ pp ty []
| C.InductiveDefinition (l, params, nparams) ->
"Parameters = " ^
List.fold_right
) x "" ^ match i with "" -> "" | i' -> " " ^ i'
) params "" ^ "\n" ^
"NParams = " ^ string_of_int nparams ^ "\n" ^
- let names = List.rev (List.map (fun (n,_,_,_) -> C.Name n) l) in
+ let names = List.rev (List.map (fun (n,_,_,_) -> Some (C.Name n)) l) in
List.fold_right (fun x i -> ppinductiveType x names ^ i) l ""
;;