From 7090733367302ff4f9c53e8b3a1b82109a086fbf Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 2 Feb 2004 16:30:06 +0000 Subject: [PATCH] - added SortExpectedMetaFound exception (huge hack) - more information along with assertion failed "9" --- helm/ocaml/cic_proof_checking/cicTypeChecker.ml | 8 +++++--- helm/ocaml/cic_proof_checking/cicTypeChecker.mli | 3 ++- 2 files changed, 7 insertions(+), 4 deletions(-) diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml index b034e3928..19ee778f5 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.ml +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.ml @@ -30,6 +30,7 @@ open Printf exception AssertFailure of string;; exception TypeCheckerFailure of string;; +exception SortExpectedMetaFound of string;; (* TODO temp *) let fdebug = ref 0;; let debug t context = @@ -631,7 +632,8 @@ and eat_lambdas context n te = eat_lambdas ((Some (name,(C.Decl so)))::context) (n - 1) ta in (te, k + 1, context') - | (_, _) -> raise (AssertFailure "9") + | (n, te) -> + raise (AssertFailure (sprintf "9 (%d, %s)" n (CicPp.ppterm te))) (*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *) and check_is_really_smaller_arg context n nn kl x safes te = @@ -1636,10 +1638,10 @@ in if not res then debug_print ("#### " ^ CicPp.ppterm (type_of_aux context p) ^ when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *) C.Sort s2 | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *) - | (_,_) -> - raise (TypeCheckerFailure (sprintf + | (_,_) -> raise (SortExpectedMetaFound (sprintf "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1') (CicPp.ppterm t2'))) +(* raise (TypeCheckerFailure (sprintf *) and eat_prods context hetype = (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *) diff --git a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli index d3db80a46..b267429d4 100644 --- a/helm/ocaml/cic_proof_checking/cicTypeChecker.mli +++ b/helm/ocaml/cic_proof_checking/cicTypeChecker.mli @@ -23,9 +23,10 @@ * http://cs.unibo.it/helm/. *) -(* This is the only exception that will be raised *) +(* These are the only exceptions that will be raised *) exception TypeCheckerFailure of string exception AssertFailure of string +exception SortExpectedMetaFound of string val typecheck : UriManager.uri -> unit -- 2.39.2