UriManager.name_of_uri uri ^ pp_exp_named_subst exp_named_subst l
| C.MutInd (uri,n,exp_named_subst) ->
(try
- match CicEnvironment.get_obj uri with
- C.InductiveDefinition (dl,_,_) ->
+ match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+ C.InductiveDefinition (dl,_,_,_) ->
let (name,_,_,_) = get_nth dl (n+1) in
name ^ pp_exp_named_subst exp_named_subst l
| _ -> raise CicPpInternalError
)
| C.MutConstruct (uri,n1,n2,exp_named_subst) ->
(try
- match CicEnvironment.get_obj uri with
- C.InductiveDefinition (dl,_,_) ->
+ match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+ C.InductiveDefinition (dl,_,_,_) ->
let (_,_,_,cons) = get_nth dl (n1+1) in
let (id,_) = get_nth cons n2 in
id ^ pp_exp_named_subst exp_named_subst l
)
| C.MutCase (uri,n1,ty,te,patterns) ->
let connames =
- (match CicEnvironment.get_obj uri with
- C.InductiveDefinition (dl,_,_) ->
+ (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+ C.InductiveDefinition (dl,_,_,_) ->
let (_,_,_,cons) = get_nth dl (n1+1) in
List.map (fun (id,_) -> id) cons
| _ -> raise CicPpInternalError
cons ""
;;
+let ppcontext ?(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
+ | 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
+ | None ->
+ Printf.sprintf "%s_ :? _" (separate i), None::name_context
+ ) context ("",[]))
+
(* ppobj obj returns a string with describing the cic object obj in a syntax *)
(* similar to the one used by Coq *)
let ppobj obj =
let module C = Cic in
let module U = UriManager in
match obj with
- C.Constant (name, Some t1, t2, params) ->
+ 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) ->
+ | 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) ->
+ | 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) ->
+ | C.CurrentProof (name, conjectures, value, ty, params, _) ->
"Current Proof of " ^ name ^
"(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
")" ^ ":\n" ^
pp t name_context ^ "\n" ^ i
) conjectures "" ^
"\n" ^ pp value [] ^ " : " ^ pp ty []
- | C.InductiveDefinition (l, params, nparams) ->
+ | C.InductiveDefinition (l, params, nparams, _) ->
"Parameters = " ^
String.concat ";" (List.map UriManager.string_of_uri params) ^ "\n" ^
"NParams = " ^ string_of_int nparams ^ "\n" ^
List.fold_right (fun x i -> ppinductiveType x ^ i) l ""
;;
+
+let ppsort = function
+ | Cic.Prop -> "Prop"
+ | Cic.Set -> "Set"
+ | Cic.Type _ -> "Type"
+ | Cic.CProp -> "CProp"
+