X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMetaSubst.ml;h=512c65d986fa2c48015309faca2a908c7501a654;hb=fb0f22004d533abca8d157ed89665dbf1041e0e2;hp=a19bb2b25e405a83b6de8026c0c7b9b2f9795c9d;hpb=e626927b4c1c77bdcd6b545203a0a9c17a9ff136;p=helm.git diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index a19bb2b25..512c65d98 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 @@ -67,6 +96,7 @@ let apply_subst_gen ~appl_fun subst term = ;; let apply_subst = +(* CSC: old code that never performs beta reduction let appl_fun um_aux he tl = let tl' = List.map um_aux tl in begin @@ -76,19 +106,7 @@ let apply_subst = end in apply_subst_gen ~appl_fun -;; - -(* apply_subst_reducing subst (Some (mtr,reductions_no)) t *) -(* performs as (apply_subst subst t) until it finds an application of *) -(* (META [meta_to_reduce]) that, once unwinding is performed, creates *) -(* a new beta-redex; in this case up to [reductions_no] consecutive *) -(* beta-reductions are performed. *) -(* Hint: this function is usually called when [reductions_no] *) -(* eta-expansions have been performed and the head of the new *) -(* application has been unified with (META [meta_to_reduce]): *) -(* during the unwinding the eta-expansions are undone. *) - -let apply_subst_reducing meta_to_reduce = +*) let appl_fun um_aux he tl = let tl' = List.map um_aux tl in let t' = @@ -97,23 +115,24 @@ let apply_subst_reducing meta_to_reduce = | he' -> Cic.Appl (he'::tl') in begin - match meta_to_reduce, he with - Some (mtr,reductions_no), Cic.Meta (m,_) when m = mtr -> + match he with + Cic.Meta (m,_) -> let rec beta_reduce = function - (n,(Cic.Appl (Cic.Lambda (_,_,t)::he'::tl'))) when n > 0 -> + (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) -> let he'' = CicSubstitution.subst he' t in if tl' = [] then he'' else - beta_reduce (n-1,Cic.Appl(he''::tl')) - | (_,t) -> t + beta_reduce (Cic.Appl(he''::tl')) + | t -> t in - beta_reduce (reductions_no,t') - | _,_ -> t' + beta_reduce t' + | _ -> t' end in apply_subst_gen ~appl_fun +;; let rec apply_subst_context subst context = List.fold_right @@ -479,14 +498,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) -> - 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 @@ -567,8 +591,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 "; "