From: Claudio Sacerdoti Coen Date: Fri, 5 Mar 2004 16:20:42 +0000 (+0000) Subject: Refine now raises only RefineFailure, AssertFailure or Uncertain. X-Git-Tag: v0_0_4~41 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c0e0ae45ee6fba4118f519b9d07169ed6a7edc8c;p=helm.git Refine now raises only RefineFailure, AssertFailure or Uncertain. --- diff --git a/helm/gTopLevel/oldDisambiguate.ml b/helm/gTopLevel/oldDisambiguate.ml index 9b1d4937c..82d0f36f5 100644 --- a/helm/gTopLevel/oldDisambiguate.ml +++ b/helm/gTopLevel/oldDisambiguate.ml @@ -168,7 +168,7 @@ module Make(C:Callbacks) = CicRefine.Uncertain _ -> prerr_endline ("%%% UNCERTAIN!!! " ^ CicPp.ppterm expr) ; Uncertain - | _ -> + | CicRefine.RefineFailure _ -> prerr_endline ("%%% PRUNED!!! " ^ CicPp.ppterm expr) ; Ko in diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index e7d703663..b09f0a8ef 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -57,8 +57,7 @@ let refine metasenv context term = | CicRefine.Uncertain _ -> debug_print ("%%% UNCERTAIN!!! " ^ CicPp.ppterm term) ; Uncertain - | _ -> - (* TODO we should catch only the RefineFailure excecption *) + | CicRefine.RefineFailure _ -> debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ; Ko diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index d33230eb0..36a25a6c2 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -26,16 +26,8 @@ open Printf exception RefineFailure of string;; - -exception Impossible of int;; -exception NotRefinable of string;; exception Uncertain of string;; -exception WrongUriToConstant of string;; -exception WrongUriToVariable of string;; -exception ListTooShort;; -exception WrongUriToMutualInductiveDefinitions of string;; -exception RelToHiddenHypothesis;; -exception WrongArgumentNumber;; +exception AssertFailure of string;; let debug_print = prerr_endline @@ -51,7 +43,7 @@ let rec split l n = match (l,n) with (l,0) -> ([], l) | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2) - | (_,_) -> raise ListTooShort + | (_,_) -> raise (AssertFailure "split: list too short") ;; let rec type_of_constant uri = @@ -61,7 +53,9 @@ let rec type_of_constant uri = match CicEnvironment.get_cooked_obj uri with C.Constant (_,_,ty,_) -> ty | C.CurrentProof (_,_,_,ty,_) -> ty - | _ -> raise (WrongUriToConstant (U.string_of_uri uri)) + | _ -> + raise + (RefineFailure ("Unknown constant definition " ^ U.string_of_uri uri)) and type_of_variable uri = let module C = Cic in @@ -69,7 +63,10 @@ and type_of_variable uri = let module U = UriManager in match CicEnvironment.get_cooked_obj uri with C.Variable (_,_,ty,_) -> ty - | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri)) + | _ -> + raise + (RefineFailure + ("Unknown variable definition " ^ UriManager.string_of_uri uri)) and type_of_mutual_inductive_defs uri i = let module C = Cic in @@ -79,7 +76,10 @@ and type_of_mutual_inductive_defs uri i = C.InductiveDefinition (dl,_,_) -> let (_,_,arity,_) = List.nth dl i in arity - | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) + | _ -> + raise + (RefineFailure + ("Unknown mutual inductive definition " ^ U.string_of_uri uri)) and type_of_mutual_inductive_constr uri i j = let module C = Cic in @@ -90,7 +90,10 @@ and type_of_mutual_inductive_constr uri i j = let (_,_,_,cl) = List.nth dl i in let (_,ty) = List.nth cl (j-1) in ty - | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) + | _ -> + raise + (RefineFailure + ("Unkown mutual inductive definition " ^ U.string_of_uri uri)) (* type_of_aux' is just another name (with a different scope) for type_of_aux *) @@ -105,7 +108,6 @@ and type_of_mutual_inductive_constr uri i j = and check_branch n context metasenv subst left_args_no actualtype term expectedtype = let module C = Cic in let module R = CicMetaSubst in - let module Un = CicUnification in match R.whd subst context expectedtype with C.MutInd (_,_,_) -> (n,context,actualtype, [term]), subst, metasenv @@ -126,15 +128,14 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt (* we should also check that the name variable is anonymous in the actual type de' ?? *) check_branch (n+1) ((Some (name,(C.Decl so)))::context) metasenv subst left_args_no de' term' de - | _ -> raise WrongArgumentNumber) - | _ -> raise (NotRefinable "Prod or MutInd expected") + | _ -> raise (AssertFailure "Wrong number of arguments")) + | _ -> raise (AssertFailure "Prod or MutInd expected") and type_of_aux' metasenv context t = let rec type_of_aux subst metasenv context = let module C = Cic in let module S = CicSubstitution in let module U = UriManager in - let module Un = CicUnification in function C.Rel n -> (try @@ -143,9 +144,9 @@ and type_of_aux' metasenv context t = | Some (_,C.Def (_,Some ty)) -> S.lift n ty,subst,metasenv | Some (_,C.Def (bo,None)) -> type_of_aux subst metasenv context (S.lift n bo) - | None -> raise RelToHiddenHypothesis + | None -> raise (RefineFailure "Rel to hidden hypothesis") with - _ -> raise (NotRefinable "Not a close term") + _ -> raise (RefineFailure "Not a close term") ) | C.Var (uri,exp_named_subst) -> let subst',metasenv' = @@ -163,7 +164,7 @@ and type_of_aux' metasenv context t = | C.Sort s -> C.Sort C.Type, (*CSC manca la gestione degli universi!!! *) subst,metasenv - | C.Implicit _ -> raise (Impossible 21) + | C.Implicit _ -> raise (AssertFailure "21") | C.Cast (te,ty) -> let _,subst',metasenv' = type_of_aux subst metasenv context ty in @@ -176,7 +177,7 @@ and type_of_aux' metasenv context t = in ty,subst''',metasenv''' with - _ -> raise (NotRefinable "Cast")) + _ -> raise (RefineFailure "Cast")) | C.Prod (name,s,t) -> let sort1,subst',metasenv' = type_of_aux subst metasenv context s in let sort2,subst'',metasenv'' = @@ -189,7 +190,7 @@ and type_of_aux' metasenv context t = C.Meta _ | C.Sort _ -> () | _ -> - raise (NotRefinable (sprintf + raise (RefineFailure (sprintf "Not well-typed lambda-abstraction: the source %s should be a type; instead it is a term of type %s" (CicPp.ppterm s) (CicPp.ppterm sort1))) @@ -219,7 +220,7 @@ and type_of_aux' metasenv context t = ) tl ([],subst',metasenv') in eat_prods subst'' metasenv'' context hetype tlbody_and_type - | C.Appl _ -> raise (NotRefinable "Appl: no arguments") + | C.Appl _ -> raise (RefineFailure "Appl: no arguments") | C.Const (uri,exp_named_subst) -> let subst',metasenv' = check_exp_named_subst subst metasenv context exp_named_subst in @@ -251,7 +252,8 @@ and type_of_aux' metasenv context t = List.nth l i , expl_params, parsno | _ -> raise - (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri)) in + (RefineFailure + ("Unkown mutual inductive definition " ^ U.string_of_uri uri)) in let rec count_prod t = match CicMetaSubst.whd subst context t with C.Prod (_, _, t) -> 1 + (count_prod t) @@ -412,7 +414,7 @@ and type_of_aux' metasenv context t = | Some t,Some (_,C.Def (ct,_)) -> (try fo_unif_subst subst context metasenv t ct - with e -> raise (NotRefinable (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct) (match e with CicUnification.AssertFailure msg -> msg | _ -> (Printexc.to_string e))))) + with e -> raise (RefineFailure (sprintf "The local context is not consistent with the canonical context, since %s cannot be unified with %s. Reason: %s" (CicMetaSubst.ppterm subst t) (CicMetaSubst.ppterm subst ct) (match e with AssertFailure msg -> msg | _ -> (Printexc.to_string e))))) | Some t,Some (_,C.Decl ct) -> let inferredty,subst',metasenv' = type_of_aux subst metasenv context t @@ -420,9 +422,9 @@ and type_of_aux' metasenv context t = (try fo_unif_subst subst' context metasenv' inferredty ct - with e -> raise (NotRefinable (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with CicUnification.AssertFailure msg -> msg | _ -> (Printexc.to_string e))))) + with e -> raise (RefineFailure (sprintf "The local context is not consistent with the canonical context, since the type %s of %s cannot be unified with the expected type %s. Reason: %s" (CicMetaSubst.ppterm subst' inferredty) (CicMetaSubst.ppterm subst' t) (CicMetaSubst.ppterm subst' ct) (match e with AssertFailure msg -> msg | _ -> (Printexc.to_string e))))) | None, Some _ -> - raise (NotRefinable (sprintf + raise (RefineFailure (sprintf "Not well typed metavariable instance %s: the local context does not instantiate an hypothesis even if the hypothesis is not restricted in the canonical context %s" (CicMetaSubst.ppterm subst (Cic.Meta (metano, l))) (CicMetaSubst.ppcontext subst canonical_context))) @@ -430,7 +432,7 @@ and type_of_aux' metasenv context t = with Invalid_argument _ -> raise - (NotRefinable + (RefineFailure (sprintf "Not well typed metavariable instance %s: the length of the local context does not match the length of the canonical context %s" (CicMetaSubst.ppterm subst (Cic.Meta (metano, l))) @@ -446,10 +448,13 @@ and type_of_aux' metasenv context t = (match CicEnvironment.get_cooked_obj ~trust:false uri with Cic.Variable (_,Some bo,_,_) -> raise - (NotRefinable + (RefineFailure "A variable with a body can not be explicit substituted") | Cic.Variable (_,None,_,_) -> () - | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri)) + | _ -> + raise + (RefineFailure + ("Unkown variable definition " ^ UriManager.string_of_uri uri)) ) ; let typeoft,metasubst',metasenv' = type_of_aux metasubst metasenv context t @@ -460,7 +465,7 @@ and type_of_aux' metasenv context t = in check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl with _ -> - raise (NotRefinable "Wrong Explicit Named Substitution") + raise (RefineFailure "Wrong Explicit Named Substitution") in check_exp_named_subst_aux metasubst metasenv [] @@ -490,7 +495,7 @@ and type_of_aux' metasenv context t = in t2'',subst,metasenv | (_,_) -> - raise (NotRefinable (sprintf + raise (RefineFailure (sprintf "Two sorts were expected, found %s (that reduces to %s) and %s (that reduces to %s)" (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2) (CicPp.ppterm t2''))) @@ -534,7 +539,7 @@ and type_of_aux' metasenv context t = in let metasenv,hetype' = mk_prod metasenv context tlbody_and_type in let (subst, metasenv) = - CicUnification.fo_unif_subst subst context metasenv hetype hetype' + fo_unif_subst subst context metasenv hetype hetype' in let rec eat_prods metasenv subst context hetype = function @@ -542,20 +547,11 @@ and type_of_aux' metasenv context t = | (hete, hety)::tl -> (match hetype with Cic.Prod (n,s,t) -> -(* - (try -*) let subst,metasenv = - CicUnification.fo_unif_subst subst context metasenv s hety + fo_unif_subst subst context metasenv s hety in eat_prods metasenv subst context (CicMetaSubst.subst subst hete t) tl -(* - with - e -> - raise - (RefineFailure ("XXX " ^ Printexc.to_string e))) -*) | _ -> assert false ) in @@ -667,12 +663,10 @@ let type_of_aux' metasenv context term = *) (t,ty,m) with - | CicUnification.AssertFailure msg as e -> - debug_print "@@@ REFINE FAILED: CicUnification.AssertFailure:"; - debug_print msg; + | RefineFailure msg as e -> + debug_print ("@@@ REFINE FAILED: " ^ msg); + raise e + | Uncertain msg as e -> + debug_print ("@@@ REFINE UNCERTAIN: " ^ msg); raise e - | e -> - debug_print ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ; - raise e ;; - diff --git a/helm/ocaml/cic_unification/cicRefine.mli b/helm/ocaml/cic_unification/cicRefine.mli index 28a34f5ff..395799b31 100644 --- a/helm/ocaml/cic_unification/cicRefine.mli +++ b/helm/ocaml/cic_unification/cicRefine.mli @@ -23,11 +23,9 @@ * http://cs.unibo.it/helm/. *) -exception NotRefinable of string -exception Uncertain of string -exception WrongUriToConstant of string -exception WrongUriToVariable of string -exception WrongUriToMutualInductiveDefinitions of string +exception RefineFailure of string;; +exception Uncertain of string;; +exception AssertFailure of string;; (* type_of_aux' metasenv context term *) (* refines [term] and returns the refined form of [term], *)