From a4086666ce84a0a71a587cafd52d1a08b26e54f0 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 19 Dec 2008 10:12:15 +0000 Subject: [PATCH] better pps --- helm/software/components/ng_kernel/check.ml | 25 +++++++++++++------ .../components/ng_kernel/nCicEnvironment.ml | 7 +++--- .../components/ng_kernel/nCicEnvironment.mli | 2 +- 3 files changed, 22 insertions(+), 12 deletions(-) diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml index a61e6a8ff..d10b771aa 100644 --- a/helm/software/components/ng_kernel/check.ml +++ b/helm/software/components/ng_kernel/check.ml @@ -15,7 +15,7 @@ let debug = true let ignore_exc = false let rank_all_dependencies = false let trust_environment = false -let print_object = false +let print_object = true let indent = ref 0;; @@ -143,6 +143,7 @@ let _ = roots_alluris; prerr_endline "finished...."; let lll, uuu =(CicUniv.do_rank (get_graph ())) in + CicUniv.print_ugraph (get_graph ()); let lll = List.sort compare lll in List.iter (fun k -> prerr_endline (CicUniv.string_of_universe k ^ " = " ^ string_of_int (CicUniv.get_rank k))) uuu; @@ -177,13 +178,21 @@ let _ = try NCicTypeChecker.typecheck_obj o with - | NCicTypeChecker.AssertFailure s - | NCicTypeChecker.TypeCheckerFailure s - | NCicEnvironment.ObjectNotFound s - | NCicEnvironment.BadConstraint s - | NCicEnvironment.BadDependency s as e -> - prerr_endline ("######### " ^ Lazy.force s); - if not ignore_exc then raise e + exn -> + let rec aux = function + | NCicTypeChecker.AssertFailure s + | NCicTypeChecker.TypeCheckerFailure s + | NCicEnvironment.ObjectNotFound s + | NCicEnvironment.BadConstraint s as e-> + prerr_endline ("######### " ^ Lazy.force s); + if not ignore_exc then raise e + | NCicEnvironment.BadDependency (s,x) as e -> + prerr_endline ("######### " ^ Lazy.force s); + aux x; + if not ignore_exc then raise e + | e -> raise e + in + aux exn ) alluris; NCicEnvironment.invalidate (); diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml index 9cad0554c..f31c4e9b1 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.ml +++ b/helm/software/components/ng_kernel/nCicEnvironment.ml @@ -16,7 +16,7 @@ module Ref = NReference exception CircularDependency of string Lazy.t;; exception ObjectNotFound of string Lazy.t;; -exception BadDependency of string Lazy.t;; +exception BadDependency of string Lazy.t * exn;; exception BadConstraint of string Lazy.t;; let type0 = [] @@ -140,11 +140,12 @@ let get_checked_obj u = Sys.Break as e -> frozen_list := saved_frozen_list; raise e - | Propagate (u',_) as e' -> + | Propagate (u',old_exn) as e' -> frozen_list := saved_frozen_list; let exn = `Exn (BadDependency (lazy (NUri.string_of_uri u ^ " depends (recursively) on " ^ NUri.string_of_uri u' ^ - " which is not well-typed"))) in + " which is not well-typed"), + match old_exn with BadDependency (_,e) -> e | _ -> old_exn)) in NUri.UriHash.add cache u exn; if saved_frozen_list = [] then exn diff --git a/helm/software/components/ng_kernel/nCicEnvironment.mli b/helm/software/components/ng_kernel/nCicEnvironment.mli index 1c530061a..4604bd2fd 100644 --- a/helm/software/components/ng_kernel/nCicEnvironment.mli +++ b/helm/software/components/ng_kernel/nCicEnvironment.mli @@ -13,7 +13,7 @@ exception CircularDependency of string Lazy.t;; exception ObjectNotFound of string Lazy.t;; -exception BadDependency of string Lazy.t;; +exception BadDependency of string Lazy.t * exn;; exception BadConstraint of string Lazy.t;; val get_checked_obj: NUri.uri -> NCic.obj -- 2.39.2