From bf60fc57745fba8a2a22215ed1286eceae0f7700 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 11 Feb 2004 10:35:52 +0000 Subject: [PATCH] Big changes: 1. every level now catches the *Failure excecptions of the lower level and converts it to its own *Failure. The same for *Uncertain. 2. CicMetaSubst.delift now raises also Uncertain (that is converted to CicUnification.Uncertain and then to CicRefine.Uncertain). --- helm/ocaml/cic_unification/cicMetaSubst.ml | 32 +++++++++-- helm/ocaml/cic_unification/cicMetaSubst.mli | 3 +- helm/ocaml/cic_unification/cicRefine.ml | 54 +++++++------------ helm/ocaml/cic_unification/cicUnification.ml | 7 ++- helm/ocaml/cic_unification/cicUnification.mli | 5 +- 5 files changed, 59 insertions(+), 42 deletions(-) diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index a19bb2b25..96b38e424 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.ml +++ b/helm/ocaml/cic_unification/cicMetaSubst.ml @@ -1,8 +1,33 @@ +(* Copyright (C) 2004, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) open Printf -exception AssertFailure of string exception MetaSubstFailure of string +exception Uncertain of string +exception AssertFailure of string let debug_print = prerr_endline @@ -567,8 +592,9 @@ let delift n subst context metasenv l t = (* The reason is that our delift function is weaker than first *) (* order (in the sense of alpha-conversion). See comment above *) (* related to the delift function. *) -debug_print "!!!!!!!!!!! First Order UnificationFailure, but maybe it could have been successful even in a first order setting (no conversion, only alpha convertibility)! Please, implement a better delift function !!!!!!!!!!!!!!!!" ; - raise (MetaSubstFailure (sprintf +debug_print "\n!!!!!!!!!!! First Order UnificationFailure, but maybe it could have been successful even in a first order setting (no conversion, only alpha convertibility)! Please, implement a better delift function !!!!!!!!!!!!!!!!" ; +print_endline "\nCicMetaSubst: UNCERTAIN" ; + raise (Uncertain (sprintf "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables" (ppterm subst t) (String.concat "; " diff --git a/helm/ocaml/cic_unification/cicMetaSubst.mli b/helm/ocaml/cic_unification/cicMetaSubst.mli index 6034853da..2ee78a7a4 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.mli +++ b/helm/ocaml/cic_unification/cicMetaSubst.mli @@ -23,8 +23,9 @@ * http://helm.cs.unibo.it/ *) -exception AssertFailure of string exception MetaSubstFailure of string +exception Uncertain of string +exception AssertFailure of string (* The entry (i,t) in a substitution means that *) (* (META i) have been instantiated with t. *) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index fbbb10a6e..8935d867c 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -37,20 +37,16 @@ exception WrongUriToMutualInductiveDefinitions of string;; exception RelToHiddenHypothesis;; exception WrongArgumentNumber;; -let fdebug = ref 0;; -let debug t context = - let rec debug_aux t i = - let module C = Cic in - let module U = UriManager in - CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i - in - if !fdebug = 0 then - raise (NotRefinable ("\n" ^ List.fold_right debug_aux (t::context) "")) - (*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*) -;; - let debug_print = prerr_endline +let fo_unif_subst subst context metasenv t1 t2 = + try + CicUnification.fo_unif_subst subst context metasenv t1 t2 + with + (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg) + | (CicUnification.Uncertain msg) -> raise (Uncertain msg) +;; + let rec split l n = match (l,n) with (l,0) -> ([], l) @@ -122,7 +118,7 @@ and check_branch n context metasenv subst left_args_no actualtype term expectedt (match R.whd subst context actualtype with C.Prod (name',so',de') -> let subst, metasenv = - Un.fo_unif_subst subst context metasenv so so' in + fo_unif_subst subst context metasenv so so' in let term' = (match CicSubstitution.lift 1 term with C.Appl l -> C.Appl (l@[C.Rel 1]) @@ -152,13 +148,11 @@ and type_of_aux' metasenv context t = _ -> raise (NotRefinable "Not a close term") ) | C.Var (uri,exp_named_subst) -> - incr fdebug ; let subst',metasenv' = check_exp_named_subst subst metasenv context exp_named_subst in let ty = CicSubstitution.subst_vars exp_named_subst (type_of_variable uri) in - decr fdebug ; ty,subst',metasenv' | C.Meta (n,l) -> let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in @@ -178,7 +172,7 @@ and type_of_aux' metasenv context t = in (try let subst''',metasenv''' = - Un.fo_unif_subst subst'' context metasenv'' inferredty ty + fo_unif_subst subst'' context metasenv'' inferredty ty in ty,subst''',metasenv''' with @@ -225,23 +219,19 @@ and type_of_aux' metasenv context t = eat_prods subst'' metasenv'' context hetype tlbody_and_type | C.Appl _ -> raise (NotRefinable "Appl: no arguments") | C.Const (uri,exp_named_subst) -> - incr fdebug ; let subst',metasenv' = check_exp_named_subst subst metasenv context exp_named_subst in let cty = CicSubstitution.subst_vars exp_named_subst (type_of_constant uri) in - decr fdebug ; cty,subst',metasenv' | C.MutInd (uri,i,exp_named_subst) -> - incr fdebug ; let subst',metasenv' = check_exp_named_subst subst metasenv context exp_named_subst in let cty = CicSubstitution.subst_vars exp_named_subst (type_of_mutual_inductive_defs uri i) in - decr fdebug ; cty,subst',metasenv' | C.MutConstruct (uri,i,j,exp_named_subst) -> let subst',metasenv' = @@ -288,7 +278,7 @@ and type_of_aux' metasenv context t = in let actual_type = CicMetaSubst.whd subst context actual_type in let subst,metasenv = - Un.fo_unif_subst subst context metasenv expected_type actual_type + fo_unif_subst subst context metasenv expected_type actual_type in (* TODO: check if the sort elimination is allowed: [(I q1 ... qr)|B] *) let (_,outtypeinstances,subst,metasenv) = @@ -338,7 +328,7 @@ and type_of_aux' metasenv context t = *) CicMetaSubst.whd subst context appl in - Un.fo_unif_subst subst context metasenv instance instance') + fo_unif_subst subst context metasenv instance instance') (subst,metasenv) outtypeinstances in CicMetaSubst.whd subst context (C.Appl(outtype::right_args@[term])),subst,metasenv @@ -358,7 +348,7 @@ and type_of_aux' metasenv context t = let ty_of_bo,subst,metasenv = type_of_aux subst metasenv context' bo in - Un.fo_unif_subst subst context' metasenv + fo_unif_subst subst context' metasenv ty_of_bo (CicMetaSubst.lift subst len ty) ) (subst,metasenv) fl in let (_,_,ty,_) = List.nth fl i in @@ -379,7 +369,7 @@ and type_of_aux' metasenv context t = let ty_of_bo,subst,metasenv = type_of_aux subst metasenv context' bo in - Un.fo_unif_subst subst context' metasenv + fo_unif_subst subst context' metasenv ty_of_bo (CicMetaSubst.lift subst len ty) ) (subst,metasenv) fl in @@ -418,14 +408,14 @@ and type_of_aux' metasenv context t = subst,metasenv | Some t,Some (_,C.Def (ct,_)) -> (try - CicUnification.fo_unif_subst subst context metasenv t ct + 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))))) | Some t,Some (_,C.Decl ct) -> let inferredty,subst',metasenv' = type_of_aux subst metasenv context t in (try - CicUnification.fo_unif_subst + 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))))) | None, Some _ -> @@ -455,8 +445,7 @@ and type_of_aux' metasenv context t = in try let metasubst'',metasenv'' = - CicUnification.fo_unif_subst - metasubst' context metasenv' typeoft typeofvar + fo_unif_subst metasubst' context metasenv' typeoft typeofvar in check_exp_named_subst_aux metasubst'' metasenv'' (substs@[subst]) tl with _ -> @@ -486,8 +475,7 @@ and type_of_aux' metasenv context t = let (metasenv,idx) = CicMkImplicit.mk_implicit_sort metasenv in let (subst, metasenv) = - CicUnification.fo_unif_subst subst context_for_t2 metasenv - (C.Meta (idx,[])) t2'' + fo_unif_subst subst context_for_t2 metasenv (C.Meta (idx,[])) t2'' in t2'',subst,metasenv | (_,_) -> @@ -537,7 +525,7 @@ and type_of_aux' metasenv context t = let prod = Cic.Prod (name, argty, newmeta) in let (_, subst, metasenv) = type_of_aux subst metasenv context prod in let (subst, metasenv) = - CicUnification.fo_unif_subst subst context metasenv resty prod + fo_unif_subst subst context metasenv resty prod in aux context'' (Some arg :: args) (CicMetaSubst.subst subst arg newmeta, subst, metasenv) tl @@ -602,10 +590,6 @@ let type_of_aux' metasenv context term = debug_print "@@@ REFINE FAILED: CicUnification.AssertFailure:"; debug_print msg; raise e - | CicUnification.UnificationFailure msg as e -> - debug_print "@@@ REFINE FAILED: CicUnification.UnificationFailure:"; - debug_print msg; - raise e | e -> debug_print ("@@@ REFINE FAILED: " ^ Printexc.to_string e) ; raise e diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 3c8b07729..bf035d74a 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -25,8 +25,9 @@ open Printf -exception AssertFailure of string;; exception UnificationFailure of string;; +exception Uncertain of string;; +exception AssertFailure of string;; let debug_print = prerr_endline @@ -96,7 +97,11 @@ let rec fo_unif_subst subst context metasenv t1 t2 = fo_unif_subst subst context metasenv lifted_oldt t with Not_found -> let t',metasenv',subst' = + try CicMetaSubst.delift n subst context metasenv l t + with + (CicMetaSubst.MetaSubstFailure msg)-> raise(UnificationFailure msg) + | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg) in (n, t')::subst', metasenv' in diff --git a/helm/ocaml/cic_unification/cicUnification.mli b/helm/ocaml/cic_unification/cicUnification.mli index 40b9f8ef7..9956b3043 100644 --- a/helm/ocaml/cic_unification/cicUnification.mli +++ b/helm/ocaml/cic_unification/cicUnification.mli @@ -23,8 +23,9 @@ * http://cs.unibo.it/helm/. *) -exception AssertFailure of string -exception UnificationFailure of string +exception UnificationFailure of string;; +exception Uncertain of string;; +exception AssertFailure of string;; (* fo_unif metasenv context t1 t2 *) (* unifies [t1] and [t2] in a context [context]. *) -- 2.39.2