X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMetaSubst.ml;h=d5262f44ba8520739a54d16de52890a2df6304c1;hb=9945374a5594c068883fa6c775f17b640fcac64d;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..d5262f44b 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.ml +++ b/helm/ocaml/cic_unification/cicMetaSubst.ml @@ -1,8 +1,34 @@ +(* 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 +42,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 +57,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) @@ -67,6 +97,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 +107,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 +116,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 @@ -220,6 +240,7 @@ let are_convertible subst context t1 t2 = CicReduction.are_convertible context t1 t2 let tempi_type_of_aux_subst = ref 0.0;; +let tempi_subst = ref 0.0;; let tempi_type_of_aux = ref 0.0;; let type_of_aux' metasenv subst context term = @@ -242,7 +263,8 @@ let res = in let time3 = Unix.gettimeofday () in tempi_type_of_aux_subst := !tempi_type_of_aux_subst +. time3 -. time1 ; - tempi_type_of_aux := !tempi_type_of_aux +. time2 -. time1 ; + tempi_subst := !tempi_subst +. time2 -. time1 ; + tempi_type_of_aux := !tempi_type_of_aux +. time3 -. time2 ; res (**** DELIFT ****) @@ -280,7 +302,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 +501,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 +543,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 +594,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 "; "