X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_unification%2FcicMetaSubst.ml;h=f082fc23092d6aa1074e54426dbb4ad2994ac170;hb=65662e7d8de61a338b636f208d04e85eb59e6b8e;hp=5870089beda2d9f208f318cbd22789d87a60c73f;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git diff --git a/components/cic_unification/cicMetaSubst.ml b/components/cic_unification/cicMetaSubst.ml index 5870089be..f082fc230 100644 --- a/components/cic_unification/cicMetaSubst.ml +++ b/components/cic_unification/cicMetaSubst.ml @@ -1,4 +1,5 @@ (* Copyright (C) 2003, HELM Team. + * * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -97,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 *) @@ -230,7 +230,7 @@ let apply_subst_gen ~appl_fun subst term = in C.CoFix (i, fl') in - LibrarySync.merge_coercions (um_aux term) + um_aux term ;; let apply_subst = @@ -247,12 +247,22 @@ let apply_subst = | _ -> t' end in - fun s t -> + fun subst t -> (* incr apply_subst_counter; *) - apply_subst_gen ~appl_fun s t +match subst with + [] -> t + | _ -> apply_subst_gen ~appl_fun subst t ;; -let rec apply_subst_context subst context = +let profiler = HExtlib.profile "U/CicMetaSubst.apply_subst" +let apply_subst s t = + profiler.HExtlib.profile (apply_subst s) t + + +let apply_subst_context subst context = + match subst with + [] -> context + | _ -> (* incr apply_subst_context_counter; context_length := !context_length + List.length context; @@ -279,6 +289,9 @@ let apply_subst_metasenv subst metasenv = incr apply_subst_metasenv_counter; metasenv_length := !metasenv_length + List.length metasenv; *) +match subst with + [] -> metasenv + | _ -> List.map (fun (n, context, ty) -> (n, apply_subst_context subst context, apply_subst subst ty)) @@ -288,67 +301,82 @@ 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 - sprintf "%s |- ?%d:= %s" context idx - (ppterm_in_name_context subst t name_context)) + (fun (idx, (c, t,ty)) -> + let context,name_context = ppcontext' ~metasenv ~sep:"; " subst c in + sprintf "%s |- ?%d : %s := %s" context idx +(ppterm_in_name_context ~metasenv [] ty 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 - sprintf "%s |- ?%d:= %s" context idx - (ppterm_in_name_context [] t name_context)) + (fun (idx, (c, t, ty)) -> + let context,name_context = ppcontext' ~metasenv ~sep:"; " [] c in + sprintf "%s |- ?%d : %s := %s" context idx (ppterm_in_name_context ~metasenv [] ty 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)) @@ -460,6 +488,9 @@ let rec force_does_not_occur subst to_be_restricted t = (!more_to_be_restricted, res) let rec restrict subst to_be_restricted metasenv = + match to_be_restricted with + | [] -> metasenv, subst + | _ -> let names_of_context_indexes context indexes = String.concat ", " (List.map @@ -578,7 +609,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); @@ -588,9 +619,7 @@ let rec restrict subst to_be_restricted metasenv = raise (MetaSubstFailure error_msg))) subst ([], []) in - match more_to_be_restricted @ more_to_be_restricted' with - | [] -> (metasenv, subst) - | l -> restrict subst l metasenv + restrict subst (more_to_be_restricted @ more_to_be_restricted') metasenv ;; (*CSC: maybe we should rename delift in abstract, as I did in my dissertation *)(*Andrea: maybe not*) @@ -617,23 +646,25 @@ let delift n subst context metasenv l t = let rec deliftaux k = let module C = Cic in function - C.Rel m -> + | C.Rel m as t-> 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 *) + t else - (try + (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) | None -> raise (MetaSubstFailure (lazy "RelToHiddenHypothesis")) with - Failure _ -> + Failure _ -> raise (MetaSubstFailure (lazy "Unbound variable found in deliftaux")) ) | C.Var (uri,exp_named_subst) -> @@ -650,7 +681,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 *) @@ -732,13 +763,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 @@ -751,9 +792,9 @@ let delift_rels_from subst metasenv k n = let rec liftaux subst metasenv k = let module C = Cic in function - C.Rel m -> + C.Rel m as t -> if m < k then - C.Rel m, subst, metasenv + t, subst, metasenv else if m < k + n then raise DeliftingARelWouldCaptureAFreeVariable else @@ -892,7 +933,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) -