X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_unification%2FcicMetaSubst.ml;h=a86bc471a06f3a2f3a97b3b0082c965dd0ce8d12;hb=da7f6fd7cc9658cfb2423db0d619811b43552976;hp=53efcf96edfad1adeb23704626206dbcaaa9feab;hpb=9393a9f9370014c904244358abe4ec6e11a9d158;p=helm.git diff --git a/components/cic_unification/cicMetaSubst.ml b/components/cic_unification/cicMetaSubst.ml index 53efcf96e..a86bc471a 100644 --- a/components/cic_unification/cicMetaSubst.ml +++ b/components/cic_unification/cicMetaSubst.ml @@ -98,7 +98,6 @@ let rec deref subst = let lookup_subst = CicUtil.lookup_subst ;; - (* clean_up_meta take a metasenv and a term and make every local context of each occurrence of a metavariable consistent with its canonical context, with respect to the hidden hipothesis *) @@ -253,6 +252,11 @@ let apply_subst = apply_subst_gen ~appl_fun s t ;; +let profiler = HExtlib.profile "U/CicMetaSubst.apply_subst" +let apply_subst s t = + profiler.HExtlib.profile (apply_subst s) t + + let rec apply_subst_context subst context = (* incr apply_subst_context_counter; @@ -289,67 +293,81 @@ let apply_subst_metasenv subst metasenv = (***** Pretty printing functions ******) -let ppterm subst term = CicPp.ppterm (apply_subst subst term) +let ppterm ~metasenv subst term = + CicPp.ppterm ~metasenv (apply_subst subst term) -let ppterm_in_name_context subst term name_context = - CicPp.pp (apply_subst subst term) name_context +let ppterm_in_name_context ~metasenv subst term name_context = + CicPp.pp ~metasenv (apply_subst subst term) name_context -let ppterm_in_context subst term context = +let ppterm_in_context ~metasenv subst term context = let name_context = List.map (function None -> None | Some (n,_) -> Some n) context in - ppterm_in_name_context subst term name_context + ppterm_in_name_context ~metasenv subst term name_context + +let ppterm_in_context_ref = ref ppterm_in_context +let set_ppterm_in_context f = + ppterm_in_context_ref := f +let use_low_level_ppterm_in_context = ref false -let ppcontext' ?(sep = "\n") subst context = +let ppterm_in_context ~metasenv subst term context = + if !use_low_level_ppterm_in_context then + ppterm_in_context ~metasenv subst term context + else + !ppterm_in_context_ref ~metasenv subst term context + +let ppcontext' ~metasenv ?(sep = "\n") subst context = let separate s = if s = "" then "" else s ^ sep in List.fold_right (fun context_entry (i,name_context) -> match context_entry with Some (n,Cic.Decl t) -> sprintf "%s%s : %s" (separate i) (CicPp.ppname n) - (ppterm_in_name_context subst t name_context), (Some n)::name_context + (ppterm_in_name_context ~metasenv subst t name_context), + (Some n)::name_context | Some (n,Cic.Def (bo,ty)) -> sprintf "%s%s : %s := %s" (separate i) (CicPp.ppname n) (match ty with None -> "_" - | Some ty -> ppterm_in_name_context subst ty name_context) - (ppterm_in_name_context subst bo name_context), (Some n)::name_context + | Some ty -> ppterm_in_name_context ~metasenv subst ty name_context) + (ppterm_in_name_context ~metasenv subst bo name_context), (Some n)::name_context | None -> sprintf "%s_ :? _" (separate i), None::name_context ) context ("",[]) -let ppsubst_unfolded subst = +let ppsubst_unfolded ~metasenv subst = String.concat "\n" (List.map (fun (idx, (c, t,_)) -> - let context,name_context = ppcontext' ~sep:"; " subst c in + let context,name_context = ppcontext' ~metasenv ~sep:"; " subst c in sprintf "%s |- ?%d:= %s" context idx - (ppterm_in_name_context subst t name_context)) + (ppterm_in_name_context ~metasenv subst t name_context)) subst) (* Printf.sprintf "?%d := %s" idx (CicPp.ppterm term)) subst) *) ;; -let ppsubst subst = +let ppsubst ~metasenv subst = String.concat "\n" (List.map (fun (idx, (c, t, _)) -> - let context,name_context = ppcontext' ~sep:"; " [] c in + let context,name_context = ppcontext' ~metasenv ~sep:"; " [] c in sprintf "%s |- ?%d:= %s" context idx - (ppterm_in_name_context [] t name_context)) + (ppterm_in_name_context ~metasenv [] t name_context)) subst) ;; -let ppcontext ?sep subst context = fst (ppcontext' ?sep subst context) +let ppcontext ~metasenv ?sep subst context = + fst (ppcontext' ~metasenv ?sep subst context) let ppmetasenv ?(sep = "\n") subst metasenv = String.concat sep (List.map (fun (i, c, t) -> - let context,name_context = ppcontext' ~sep:"; " subst c in + let context,name_context = ppcontext' ~metasenv ~sep:"; " subst c in sprintf "%s |- ?%d: %s" context i - (ppterm_in_name_context subst t name_context)) + (ppterm_in_name_context ~metasenv subst t name_context)) (List.filter (fun (i, _, _) -> not (List.mem_assoc i subst)) metasenv)) @@ -579,7 +597,7 @@ let rec restrict subst to_be_restricted metasenv = 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 ~metasenv subst term)) in (* DEBUG debug_print (lazy error_msg); @@ -620,15 +638,17 @@ let delift n subst context metasenv l t = function C.Rel m -> if m <=k then - C.Rel m (*CSC: che succede se c'e' un Def? Dovrebbe averlo gia' *) - (*CSC: deliftato la regola per il LetIn *) - (*CSC: FALSO! La regola per il LetIn non lo fa *) + C.Rel m else (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? *) + (*CSC: ANSWER: it hurts performances since it is possible to *) + (*CSC: have an exponential explosion of the size of the proof.*) + (*CSC: However, without this bit of reduction some "apply" in *) + (*CSC: the library fail (e.g. nat/nth_prime.ma). *) deliftaux k (S.lift m t) | Some (_,C.Decl t) -> C.Rel ((position (m-k) l) + k) @@ -651,7 +671,7 @@ let delift n subst context metasenv l t = if (i = n) then 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 ~metasenv subst t)))) else begin (* I do not consider the term associated to ?i in subst since *) @@ -733,13 +753,23 @@ debug_print(lazy (sprintf (List.map (function Some t -> ppterm subst t | None -> "_") l )))); *) - raise (Uncertain (lazy (sprintf + let msg = (lazy (sprintf "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables" - (ppterm subst t) + (ppterm ~metasenv subst t) (String.concat "; " (List.map - (function Some t -> ppterm subst t | None -> "_") - l))))) + (function Some t -> ppterm ~metasenv subst t | None -> "_") + l)))) + in + if + List.exists + (function + Some t -> CicUtil.is_meta_closed (apply_subst subst t) + | None -> true) l + then + raise (Uncertain msg) + else + raise (MetaSubstFailure msg) in let (metasenv, subst) = restrict subst !to_be_restricted metasenv in res, metasenv, subst @@ -893,7 +923,6 @@ let fpp_gen ppf s = Format.pp_print_newline ppf (); Format.pp_print_flush ppf () -let fppsubst ppf subst = fpp_gen ppf (ppsubst subst) +let fppsubst ppf subst = fpp_gen ppf (ppsubst ~metasenv:[] subst) let fppterm ppf term = fpp_gen ppf (CicPp.ppterm term) let fppmetasenv ppf metasenv = fpp_gen ppf (ppmetasenv [] metasenv) -