X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMetaSubst.ml;h=021e87ea5c6a6c1221566fcf42b3b0dfe6bca738;hb=17cc9a1c6353a5a57562434e9938fb54ca78b9c6;hp=db63ff5685ab23cfe2eec391a304d2caf87c651b;hpb=1592bfa20a80f2f58fe0593c019689cb32072db6;p=helm.git diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index db63ff568..021e87ea5 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.ml +++ b/helm/ocaml/cic_unification/cicMetaSubst.ml @@ -47,7 +47,7 @@ let reset_counters () = metasenv_length := 0; context_length := 0 let print_counters () = - prerr_endline (Printf.sprintf + debug_print (Printf.sprintf "apply_subst: %d apply_subst_context: %d apply_subst_metasenv: %d @@ -71,8 +71,9 @@ context length: %d (avg = %.2f) exception MetaSubstFailure of string exception Uncertain of string exception AssertFailure of string +exception DeliftingARelWouldCaptureAFreeVariable;; -let debug_print = prerr_endline +let debug_print = fun _ -> () type substitution = (int * (Cic.context * Cic.term)) list @@ -83,7 +84,7 @@ let rec deref subst = Cic.Meta(n,l) as t -> (try deref subst - (CicSubstitution.lift_meta + (CicSubstitution.subst_meta l (third (CicUtil.lookup_subst n subst))) with CicUtil.Subst_not_found _ -> t) @@ -183,7 +184,7 @@ let apply_subst_gen ~appl_fun subst term = | C.Meta (i, l) -> (try let (_, t,_) = lookup_subst i subst in - um_aux (S.lift_meta l t) + um_aux (S.subst_meta l t) with CicUtil.Subst_not_found _ -> (* unconstrained variable, i.e. free in subst*) let l' = @@ -594,10 +595,10 @@ let rec restrict subst to_be_restricted metasenv = (ppterm subst term) in (* DEBUG - prerr_endline error_msg; - prerr_endline ("metasenv = \n" ^ (ppmetasenv metasenv subst)); - prerr_endline ("subst = \n" ^ (ppsubst subst)); - prerr_endline ("context = \n" ^ (ppcontext subst context)); *) + debug_print error_msg; + debug_print ("metasenv = \n" ^ (ppmetasenv metasenv subst)); + debug_print ("subst = \n" ^ (ppsubst subst)); + debug_print ("context = \n" ^ (ppcontext subst context)); *) raise (MetaSubstFailure error_msg))) subst ([], []) in @@ -613,7 +614,7 @@ let delift n subst context metasenv l t = otherwise the occur check does not make sense *) (* - prerr_endline ("sto deliftando il termine " ^ (CicPp.ppterm t) ^ " rispetto + debug_print ("sto deliftando il termine " ^ (CicPp.ppterm t) ^ " rispetto al contesto locale " ^ (CicPp.ppterm (Cic.Meta(0,l)))); *) @@ -655,32 +656,36 @@ let delift n subst context metasenv l t = in C.Var (uri,exp_named_subst') | C.Meta (i, l1) as t -> - (* see the top level invariant *) - if (i = n) then - raise (MetaSubstFailure (sprintf - "Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)" - i (ppterm subst t))) - else - begin - (* I do not consider the term associated to ?i in subst since *) - (* in this way I can restrict if something goes wrong. *) - let rec deliftl j = - function - [] -> [] - | None::tl -> None::(deliftl (j+1) tl) - | (Some t)::tl -> - let l1' = (deliftl (j+1) tl) in - try - Some (deliftaux k t)::l1' - with - NotInTheList - | MetaSubstFailure _ -> - to_be_restricted := - (i,j)::!to_be_restricted ; None::l1' - in - let l' = deliftl 1 l1 in - C.Meta(i,l') - end + (try + let (_,t,_) = CicUtil.lookup_subst i subst in + deliftaux k (CicSubstitution.subst_meta l1 t) + with CicUtil.Subst_not_found _ -> + (* see the top level invariant *) + if (i = n) then + raise (MetaSubstFailure (sprintf + "Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)" + i (ppterm subst t))) + else + begin + (* I do not consider the term associated to ?i in subst since *) + (* in this way I can restrict if something goes wrong. *) + let rec deliftl j = + function + [] -> [] + | None::tl -> None::(deliftl (j+1) tl) + | (Some t)::tl -> + let l1' = (deliftl (j+1) tl) in + try + Some (deliftaux k t)::l1' + with + NotInTheList + | MetaSubstFailure _ -> + to_be_restricted := + (i,j)::!to_be_restricted ; None::l1' + in + let l' = deliftl 1 l1 in + C.Meta(i,l') + end) | C.Sort _ as t -> t | C.Implicit _ as t -> t | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty) @@ -734,7 +739,7 @@ let delift n subst context metasenv l t = (* order (in the sense of alpha-conversion). See comment above *) (* related to the delift function. *) (* debug_print "First Order UnificationFailure during delift" ; -prerr_endline(sprintf +debug_print(sprintf "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables" (ppterm subst t) (String.concat "; " @@ -753,6 +758,82 @@ prerr_endline(sprintf res, metasenv, subst ;; +(* delifts a term t of n levels strating from k, that is changes (Rel m) + * to (Rel (m - n)) when m > (k + n). if k <= m < k + n delift fails + *) +let delift_rels_from k n = + let rec liftaux k = + let module C = Cic in + function + C.Rel m -> + if m < k then + C.Rel m + else if m < k + n then + raise DeliftingARelWouldCaptureAFreeVariable + else + C.Rel (m - n) + | C.Var (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst + in + C.Var (uri,exp_named_subst') + | C.Meta (i,l) -> + let l' = + List.map + (function + None -> None + | Some t -> Some (liftaux k t) + ) l + in + C.Meta(i,l') + | C.Sort _ as t -> t + | C.Implicit _ as t -> t + | C.Cast (te,ty) -> C.Cast (liftaux k te, liftaux k ty) + | C.Prod (n,s,t) -> C.Prod (n, liftaux k s, liftaux (k+1) t) + | C.Lambda (n,s,t) -> C.Lambda (n, liftaux k s, liftaux (k+1) t) + | C.LetIn (n,s,t) -> C.LetIn (n, liftaux k s, liftaux (k+1) t) + | C.Appl l -> C.Appl (List.map (liftaux k) l) + | C.Const (uri,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst + in + C.Const (uri,exp_named_subst') + | C.MutInd (uri,tyno,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst + in + C.MutInd (uri,tyno,exp_named_subst') + | C.MutConstruct (uri,tyno,consno,exp_named_subst) -> + let exp_named_subst' = + List.map (function (uri,t) -> (uri,liftaux k t)) exp_named_subst + in + C.MutConstruct (uri,tyno,consno,exp_named_subst') + | C.MutCase (sp,i,outty,t,pl) -> + C.MutCase (sp, i, liftaux k outty, liftaux k t, + List.map (liftaux k) pl) + | C.Fix (i, fl) -> + let len = List.length fl in + let liftedfl = + List.map + (fun (name, i, ty, bo) -> (name, i, liftaux k ty, liftaux (k+len) bo)) + fl + in + C.Fix (i, liftedfl) + | C.CoFix (i, fl) -> + let len = List.length fl in + let liftedfl = + List.map + (fun (name, ty, bo) -> (name, liftaux k ty, liftaux (k+len) bo)) + fl + in + C.CoFix (i, liftedfl) + in + liftaux k + +let delift_rels n t = + delift_rels_from 1 n t + + (**** END OF DELIFT ****)