X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_unification%2FcicMetaSubst.ml;h=f082fc23092d6aa1074e54426dbb4ad2994ac170;hb=76735c56a213efa570fd98336aac2524ff4d36e5;hp=96efe2e3cb7ff5f72442593effbc70d461452680;hpb=982a3285c2f8b554ceae11b46c204bf61bfba1ed;p=helm.git diff --git a/helm/software/components/cic_unification/cicMetaSubst.ml b/helm/software/components/cic_unification/cicMetaSubst.ml index 96efe2e3c..f082fc230 100644 --- a/helm/software/components/cic_unification/cicMetaSubst.ml +++ b/helm/software/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 *) @@ -248,9 +247,11 @@ 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 profiler = HExtlib.profile "U/CicMetaSubst.apply_subst" @@ -258,7 +259,10 @@ let apply_subst s t = profiler.HExtlib.profile (apply_subst s) t -let rec apply_subst_context subst context = +let apply_subst_context subst context = + match subst with + [] -> context + | _ -> (* incr apply_subst_context_counter; context_length := !context_length + List.length context; @@ -285,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)) @@ -294,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 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' ?(sep = "\n") subst 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)) @@ -466,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 @@ -584,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); @@ -594,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*) @@ -623,11 +646,11 @@ 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 + 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 *) @@ -641,7 +664,7 @@ let delift n subst context metasenv l 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) -> @@ -658,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 *) @@ -742,22 +765,21 @@ debug_print(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 -> "_") + (function Some t -> ppterm ~metasenv subst t | None -> "_") l)))) in if - (*CSC: WARNING: if we are working up to reduction (I do not think so), - the following test should be replaced with "all the terms in l are - meta-closed" *) - not - (List.exists (function Some (Cic.Meta _) -> true | _ -> false ) l) + List.exists + (function + Some t -> CicUtil.is_meta_closed (apply_subst subst t) + | None -> true) l then - raise (MetaSubstFailure msg) - else raise (Uncertain msg) + else + raise (MetaSubstFailure msg) in let (metasenv, subst) = restrict subst !to_be_restricted metasenv in res, metasenv, subst @@ -770,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 @@ -911,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) -