X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fcic_unification%2FcicMetaSubst.ml;h=c097eacf281869b9ff532d8e127ec80ac5d75d82;hb=b20889b47bf949b17a6297ac39a5c0df0301de9e;hp=96efe2e3cb7ff5f72442593effbc70d461452680;hpb=7d748bd1d68d5e47413b411cd8c82ccb5307b0e9;p=helm.git diff --git a/components/cic_unification/cicMetaSubst.ml b/components/cic_unification/cicMetaSubst.ml index 96efe2e3c..c097eacf2 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 *) @@ -294,67 +293,70 @@ 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 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 + 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)) @@ -584,7 +586,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); @@ -658,7 +660,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 +744,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 @@ -911,7 +912,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) -