X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMetaSubst.ml;h=9695d714b7658940392fc4401af71d3701d7298f;hb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;hp=bd6eca4a51a377ac95096ae4a27c10516d0efa3b;hpb=34dfcf625e3ee6fac4ad4f7199055dee4edc5abb;p=helm.git diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index bd6eca4a5..9695d714b 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 @@ -16,7 +41,11 @@ let apply_subst_gen ~appl_fun subst term = let module S = CicSubstitution in function C.Rel _ as t -> t - | C.Var _ as t -> t + | C.Var (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst + in + C.Var (uri, exp_named_subst') | C.Meta (i, l) -> (try let t = List.assoc i subst in @@ -27,7 +56,7 @@ let apply_subst_gen ~appl_fun subst term = in C.Meta (i,l')) | C.Sort _ as t -> t - | C.Implicit -> assert false + | C.Implicit _ -> assert false | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty) | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t) | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t) @@ -280,7 +309,7 @@ let rec force_does_not_occur subst to_be_restricted t = C.Rel r when List.mem (r - k) to_be_restricted -> raise Occur | C.Rel _ | C.Sort _ as t -> t - | C.Implicit -> assert false + | C.Implicit _ -> assert false | C.Meta (n, l) -> (* we do not retrieve the term associated to ?n in subst since *) (* in this way we can restrict if something goes wrong *) @@ -479,24 +508,19 @@ let delift n subst context metasenv l t = (*CSC: deliftato la regola per il LetIn *) (*CSC: FALSO! La regola per il LetIn non lo fa *) else - (match List.nth context (m-k-1) with - Some (_,C.Def (t,_)) -> - (*CSC: Hmmm. This bit of reduction is not in the spirit of *) - (*CSC: first order unification. Does it help or does it harm? *) - deliftaux k (S.lift m t) - | Some (_,C.Decl t) -> - (*CSC: The following check seems to be wrong! *) - (*CSC: B:Set |- ?2 : Set *) - (*CSC: A:Set ; x:?2[A/B] |- ?1[x/A] =?= x *) - (*CSC: Why should I restrict ?2 over B? The instantiation *) - (*CSC: ?1 := A is perfectly reasonable and well-typed. *) - (*CSC: Thus I comment out the following two lines that *) - (*CSC: are the incriminated ones. *) - (*(* It may augment to_be_restricted *) - ignore (deliftaux k (S.lift m t)) ;*) - (*CSC: end of bug commented out *) - C.Rel ((position (m-k) l) + k) - | None -> raise (MetaSubstFailure "RelToHiddenHypothesis")) + (try + match List.nth context (m-k-1) with + Some (_,C.Def (t,_)) -> + (*CSC: Hmmm. This bit of reduction is not in the spirit of *) + (*CSC: first order unification. Does it help or does it harm? *) + deliftaux k (S.lift m t) + | Some (_,C.Decl t) -> + C.Rel ((position (m-k) l) + k) + | None -> raise (MetaSubstFailure "RelToHiddenHypothesis") + with + Failure _ -> + raise (MetaSubstFailure "Unbound variable found in deliftaux") + ) | C.Var (uri,exp_named_subst) -> let exp_named_subst' = List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst @@ -526,7 +550,7 @@ let delift n subst context metasenv l t = let l' = deliftl 1 l1 in C.Meta(i,l') | C.Sort _ as t -> t - | C.Implicit as t -> t + | C.Implicit _ as t -> t | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty) | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t) | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t) @@ -577,8 +601,8 @@ 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 !!!!!!!!!!!!!!!!" ; + raise (Uncertain (sprintf "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables" (ppterm subst t) (String.concat "; "