X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_unification%2FcicMetaSubst.ml;h=dfa47e469bbd97d12ddbf6e83ce39935bd90c526;hb=656cb59b98db21ef50afef7677ae03282bd8aad1;hp=3b8e4ad221646ba6f0e949eb1250e2ba04e477bb;hpb=ed9af5a10b66343f817a1f9eac3add29e4b2baae;p=helm.git diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index 3b8e4ad22..dfa47e469 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 () = - debug_print (Printf.sprintf + debug_print (lazy (Printf.sprintf "apply_subst: %d apply_subst_context: %d apply_subst_metasenv: %d @@ -64,13 +64,13 @@ context length: %d (avg = %.2f) ((float !metasenv_length) /. (float !apply_subst_metasenv_counter)) !context_length ((float !context_length) /. (float !apply_subst_context_counter)) - )*) + ))*) -exception MetaSubstFailure of string -exception Uncertain of string -exception AssertFailure of string +exception MetaSubstFailure of string Lazy.t +exception Uncertain of string Lazy.t +exception AssertFailure of string Lazy.t exception DeliftingARelWouldCaptureAFreeVariable;; let debug_print = fun _ -> () @@ -334,7 +334,7 @@ let ppsubst subst = let ppcontext ?sep subst context = fst (ppcontext' ?sep subst context) -let ppmetasenv ?(sep = "\n") metasenv subst = +let ppmetasenv ?(sep = "\n") subst metasenv = String.concat sep (List.map (fun (i, c, t) -> @@ -536,10 +536,10 @@ let rec restrict subst to_be_restricted metasenv = (more @ more_to_be_restricted @ more_to_be_restricted', metasenv') with Occur -> - raise (MetaSubstFailure (sprintf + raise (MetaSubstFailure (lazy (sprintf "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since metavariable's type depends on at least one of them" - n (names_of_context_indexes context to_be_restricted)))) - metasenv ([], []) + n (names_of_context_indexes context to_be_restricted))))) + metasenv ([], []) in let (more_to_be_restricted', subst) = (* restrict subst *) List.fold_right @@ -567,16 +567,16 @@ let rec restrict subst to_be_restricted metasenv = @ more_to_be_restricted'@more_to_be_restricted'' in (more, subst') with Occur -> - let error_msg = sprintf + let error_msg = lazy (sprintf "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since ?%d is already instantiated with %s and at least one of the hypotheses occurs in the substituted term" n (names_of_context_indexes context to_be_restricted) n - (ppterm subst term) + (ppterm subst term)) in (* DEBUG - debug_print error_msg; - debug_print ("metasenv = \n" ^ (ppmetasenv metasenv subst)); - debug_print ("subst = \n" ^ (ppsubst subst)); - debug_print ("context = \n" ^ (ppcontext subst context)); *) + debug_print (lazy error_msg); + debug_print (lazy ("metasenv = \n" ^ (ppmetasenv metasenv subst))); + debug_print (lazy ("subst = \n" ^ (ppsubst subst))); + debug_print (lazy ("context = \n" ^ (ppcontext subst context))); *) raise (MetaSubstFailure error_msg))) subst ([], []) in @@ -592,8 +592,8 @@ let delift n subst context metasenv l t = otherwise the occur check does not make sense *) (* - debug_print ("sto deliftando il termine " ^ (CicPp.ppterm t) ^ " rispetto - al contesto locale " ^ (CicPp.ppterm (Cic.Meta(0,l)))); + debug_print (lazy ("sto deliftando il termine " ^ (CicPp.ppterm t) ^ " rispetto + al contesto locale " ^ (CicPp.ppterm (Cic.Meta(0,l))))); *) let module S = CicSubstitution in @@ -623,10 +623,10 @@ let delift n subst context metasenv l t = deliftaux k (S.lift m t) | Some (_,C.Decl t) -> C.Rel ((position (m-k) l) + k) - | None -> raise (MetaSubstFailure "RelToHiddenHypothesis") + | None -> raise (MetaSubstFailure (lazy "RelToHiddenHypothesis")) with Failure _ -> - raise (MetaSubstFailure "Unbound variable found in deliftaux") + raise (MetaSubstFailure (lazy "Unbound variable found in deliftaux")) ) | C.Var (uri,exp_named_subst) -> let exp_named_subst' = @@ -640,9 +640,9 @@ let delift n subst context metasenv l t = with CicUtil.Subst_not_found _ -> (* see the top level invariant *) if (i = n) then - raise (MetaSubstFailure (sprintf + raise (MetaSubstFailure (lazy (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))) + i (ppterm subst t)))) else begin (* I do not consider the term associated to ?i in subst since *) @@ -716,21 +716,21 @@ 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 during delift" ; -debug_print(sprintf +(* debug_print (lazy "First Order UnificationFailure during delift") ; +debug_print(lazy (sprintf "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables" (ppterm subst t) (String.concat "; " (List.map (function Some t -> ppterm subst t | None -> "_") l - ))); *) - raise (Uncertain (sprintf + )))); *) + raise (Uncertain (lazy (sprintf "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables" (ppterm subst t) (String.concat "; " (List.map (function Some t -> ppterm subst t | None -> "_") - l)))) + l))))) in let (metasenv, subst) = restrict subst !to_be_restricted metasenv in res, metasenv, subst @@ -886,5 +886,5 @@ let fpp_gen ppf s = let fppsubst ppf subst = fpp_gen ppf (ppsubst subst) let fppterm ppf term = fpp_gen ppf (CicPp.ppterm term) -let fppmetasenv ppf metasenv = fpp_gen ppf (ppmetasenv metasenv []) +let fppmetasenv ppf metasenv = fpp_gen ppf (ppmetasenv [] metasenv)