From: Stefano Zacchiroli Date: Thu, 22 Jan 2004 12:25:36 +0000 (+0000) Subject: - bugfix: raise an Invalid_choice insteda of a generic exception on X-Git-Tag: V_0_5_1_4~19 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e9e00ee3e8d57c51e52fcfca9c642b8f366b8d0d;p=helm.git - bugfix: raise an Invalid_choice insteda of a generic exception on inductive constructor error - moved TEST_INTERPRETATION debug message in a better place --- diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index aa3fe97ee..b2df644d2 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -23,7 +23,10 @@ * http://helm.cs.unibo.it/ *) +open Printf + open Disambiguate_types +open UriManager exception Invalid_choice exception No_choices of domain_item @@ -59,6 +62,7 @@ type test_result = let refine metasenv context term = let metasenv, term = CicMkImplicit.expand_implicits metasenv context term in + debug_print (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term)); try let term', _, _, metasenv' = CicRefine.type_of_aux' metasenv context term in Ok (term', metasenv') @@ -78,10 +82,6 @@ let refine metasenv context term = debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ; Ko -open Printf - -open UriManager - let indtyuri_of_uri uri = let index_sharp = String.index uri '#' in let index_num = index_sharp + 3 in @@ -166,7 +166,7 @@ let interpretate ~context ~env ast = match resolve env (Id indty_ident) () with | Cic.MutInd (uri, tyno, _) -> uri, tyno | Cic.Implicit -> raise Try_again - | _ -> Parser.fail loc ("Not an inductive type: " ^ indty_ident) + | _ -> raise Invalid_choice in Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term, (List.map do_branch branches)) @@ -389,8 +389,6 @@ module Make (C: Callbacks) = let cic_term = interpretate ~context:disambiguate_context ~env:filled_env term in - debug_print - (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm cic_term)); refine metasenv context cic_term with | Try_again -> Uncertain