From 0189703896b7a3392797132720e5c72fc83eb38e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 3 Dec 2002 14:30:58 +0000 Subject: [PATCH] An exception was raised when a MutInd or MutConstruct had an uri to a non-existing object. The whole URI + XPointer is now printed. --- helm/ocaml/cic_proof_checking/cicPp.ml | 47 ++++++++++++++------------ 1 file changed, 25 insertions(+), 22 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicPp.ml b/helm/ocaml/cic_proof_checking/cicPp.ml index 05c964370..30b91760d 100644 --- a/helm/ocaml/cic_proof_checking/cicPp.ml +++ b/helm/ocaml/cic_proof_checking/cicPp.ml @@ -107,19 +107,27 @@ let rec pp t l = | C.Const (uri,exp_named_subst) -> UriManager.name_of_uri uri ^ pp_exp_named_subst exp_named_subst l | C.MutInd (uri,n,exp_named_subst) -> - (match CicEnvironment.get_obj uri with - C.InductiveDefinition (dl,_,_) -> - let (name,_,_,_) = get_nth dl (n+1) in - name ^ pp_exp_named_subst exp_named_subst l - | _ -> raise CicPpInternalError + (try + match CicEnvironment.get_obj uri with + C.InductiveDefinition (dl,_,_) -> + let (name,_,_,_) = get_nth dl (n+1) in + name ^ pp_exp_named_subst exp_named_subst l + | _ -> raise CicPpInternalError + with + _ -> UriManager.string_of_uri uri ^ "#1/" ^ string_of_int n ) | C.MutConstruct (uri,n1,n2,exp_named_subst) -> - (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 ^ pp_exp_named_subst exp_named_subst l - | _ -> raise CicPpInternalError + (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 ^ pp_exp_named_subst exp_named_subst l + | _ -> raise CicPpInternalError + with + _ -> + UriManager.string_of_uri uri ^ "#1/" ^ string_of_int n1 ^ "/" ^ + string_of_int n2 ) | C.MutCase (uri,n1,ty,te,patterns) -> let connames = @@ -172,18 +180,14 @@ 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 *) -(* evaluated in the environment names that is the list of typenames of the *) -(* mutual inductive definitions defined in the block of mutual inductive *) -(* definitions to which this one belongs to *) -let ppinductiveType (typename, inductive, arity, cons) names = +(* ppinductiveType (typename, inductive, arity, cons) *) +(* pretty-prints a single inductive definition *) +(* (typename, inductive, arity, cons) *) +let ppinductiveType (typename, inductive, arity, cons) = (if inductive then "\nInductive " else "\nCoInductive ") ^ typename ^ ": " ^ - (*CSC: bug found: was pp arity names ^ " =\n " ^*) pp arity [] ^ " =\n " ^ List.fold_right - (fun (id,ty) i -> id ^ " : " ^ pp ty names ^ + (fun (id,ty) i -> id ^ " : " ^ pp ty [] ^ (if i = "" then "\n" else "\n | ") ^ i) cons "" ;; @@ -239,6 +243,5 @@ let ppobj obj = "Parameters = " ^ String.concat ";" (List.map UriManager.string_of_uri params) ^ "\n" ^ "NParams = " ^ string_of_int nparams ^ "\n" ^ - 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 "" + List.fold_right (fun x i -> ppinductiveType x ^ i) l "" ;; -- 2.39.2