X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMetaSubst.ml;h=30069cdfec88d12f6549922d14d0c1a6561adf90;hb=a886fdf011c202071e76c5716d59a335ec5d321d;hp=ba8ae7d98cd04606ee60fa7cf779f333482e0eca;hpb=e874af2d785b2b383ae8444fdd32bb5344fb914f;p=helm.git diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml index ba8ae7d98..30069cdfe 100644 --- a/helm/ocaml/cic_unification/cicMetaSubst.ml +++ b/helm/ocaml/cic_unification/cicMetaSubst.ml @@ -51,24 +51,24 @@ let rec force_does_not_occur subst to_be_restricted t = | C.Sort _ as t -> t | C.Implicit -> assert false | C.Meta (n, l) -> - (try - aux k (CicSubstitution.lift_meta l (List.assoc n subst)) - with Not_found -> - let l' = - let i = ref 0 in - List.map - (function - | None -> None - | Some t -> - incr i; - try - Some (aux k t) - with Occur -> - more_to_be_restricted := (n,!i) :: !more_to_be_restricted; - None) - l - in - C.Meta (n, l')) + (* we do not retrieve the term associated to ?n in subst since *) + (* in this way we can restrict if something goes wrong *) + let l' = + let i = ref 0 in + List.map + (function t -> + incr i ; + match t with + None -> None + | Some t -> + try + Some (aux k t) + with Occur -> + more_to_be_restricted := (n,!i) :: !more_to_be_restricted; + None) + l + in + C.Meta (n, l') | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty) | C.Prod (name,so,dest) -> C.Prod (name, aux k so, aux (k+1) dest) | C.Lambda (name,so,dest) -> C.Lambda (name, aux k so, aux (k+1) dest) @@ -205,7 +205,7 @@ let rec restrict subst to_be_restricted metasenv = "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 (CicPp.ppterm s))) - with Not_found -> (more @ more_to_be_restricted, metasenv', subst)) + with Not_found -> (more @ more_to_be_restricted @ more_to_be_restricted', metasenv', subst)) with Occur -> raise (MetaSubstFailure (sprintf "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since metavariable's type depends on at least one of them" @@ -219,14 +219,6 @@ let rec restrict subst to_be_restricted metasenv = (*CSC: maybe we should rename delift in abstract, as I did in my dissertation *) let delift n subst context metasenv l t = - let l = - let (_, canonical_context, _) = CicUtil.lookup_meta n metasenv in - List.map2 (fun ct lt -> - match (ct, lt) with - | None, _ -> None - | Some _, _ -> lt) - canonical_context l - in let module S = CicSubstitution in let to_be_restricted = ref [] in let rec deliftaux k = @@ -267,24 +259,23 @@ let delift n subst context metasenv l t = "Cannot unify the metavariable ?%d with a term that has as subterm %s in which the same metavariable occurs (occur check)" i (CicPp.ppterm t))) else - (try - deliftaux k (S.lift_meta l (List.assoc i subst)) - with Not_found -> - let rec deliftl j = - function - [] -> [] - | None::tl -> None::(deliftl (j+1) tl) - | (Some t)::tl -> - let l1' = (deliftl (j+1) tl) in - try - Some (deliftaux k t)::l1' - with - NotInTheList - | MetaSubstFailure _ -> - to_be_restricted := (i,j)::!to_be_restricted ; None::l1' - in - let l' = deliftl 1 l1 in - C.Meta(i,l')) + (* I do not consider the term associated to ?i in subst since *) + (* in this way I can restrict if something goes wrong. *) + let rec deliftl j = + function + [] -> [] + | None::tl -> None::(deliftl (j+1) tl) + | (Some t)::tl -> + let l1' = (deliftl (j+1) tl) in + try + Some (deliftaux k t)::l1' + with + NotInTheList + | MetaSubstFailure _ -> + to_be_restricted := (i,j)::!to_be_restricted ; None::l1' + in + let l' = deliftl 1 l1 in + C.Meta(i,l') | C.Sort _ as t -> t | C.Implicit as t -> t | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty) @@ -485,25 +476,36 @@ let apply_subst_metasenv subst metasenv = let ppterm subst term = CicPp.ppterm (apply_subst subst term) -let ppcontext ?(sep = "\n") subst context = - String.concat sep - (List.rev_map (function - | Some (n, Cic.Decl t) -> - sprintf "%s : %s" (CicPp.ppname n) (ppterm subst t) - | Some (n, Cic.Def (t, ty)) -> - sprintf "%s : %s := %s" - (CicPp.ppname n) - (match ty with None -> "_" | Some ty -> ppterm subst ty) - (ppterm subst t) - | None -> "_") - context) +let ppterm_in_context subst term name_context = + CicPp.pp (apply_subst subst term) name_context + +let ppcontext' ?(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_context 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_context subst ty name_context) + (ppterm_in_context subst bo name_context), (Some n)::name_context + | None -> + sprintf "%s_ :? _" (separate i), None::name_context + ) context ("",[]) + +let ppcontext ?sep subst context = fst (ppcontext' ?sep subst context) let ppmetasenv ?(sep = "\n") metasenv subst = String.concat sep (List.map (fun (i, c, t) -> - sprintf "%s |- ?%d: %s" (ppcontext ~sep:"; " subst c) i - (ppterm subst t)) + let context,name_context = ppcontext' ~sep:"; " subst c in + sprintf "%s |- ?%d: %s" context i + (ppterm_in_context subst t name_context)) (List.filter (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst)) metasenv))