From: Enrico Tassi Date: Mon, 28 Sep 2009 14:38:54 +0000 (+0000) Subject: 2 lift related bugs fixed! X-Git-Tag: make_still_working~3427 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0771f484b17fbe61f17c03288cfdc1124698f161;p=helm.git 2 lift related bugs fixed! --- diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index 60abe85c3..52d2e4594 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.ml +++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml @@ -227,7 +227,10 @@ let rec flexible_arg context subst = function (NCicSubstitution.lift i bo) | _ -> false with - | Failure _ -> assert false + | Failure _ -> + prerr_endline (Printf.sprintf "Rel %d inside context:\n%s" i + (NCicPp.ppcontext ~subst ~metasenv:[] context)); + assert false | Invalid_argument _ -> assert false) | _ -> false ;; @@ -276,11 +279,15 @@ let delift ~unify metasenv subst context n l t = | _, NCic.Irl _ -> fun _ _ _ _ _ -> None | shift, NCic.Ctx l -> fun metasenv subst context k t -> if flexible_arg context subst t || contains_in_scope subst t then None else - let lb = List.map (fun t -> t, flexible_arg context subst t) l in + let lb = + List.map (fun t -> + let t = NCicSubstitution.lift (k+shift) t in + t, flexible_arg context subst t) + l + in HExtlib.list_findopt (fun (li,flexible) i -> if flexible || i < in_scope then None else - let li = NCicSubstitution.lift (k+shift) li in match unify metasenv subst context li t with | Some (metasenv,subst) -> Some ((metasenv, subst), NCic.Rel (i+1+k)) @@ -295,7 +302,7 @@ let delift ~unify metasenv subst context n l t = | NCic.Rel n as t when n <= k -> ms, t | NCic.Rel n -> (try - match List.nth context (n-k-1) with + match List.nth context (n-1) with | _,NCic.Def (bo,_) -> (try ms, NCic.Rel ((position in_scope (n-k) l) + k) with NotInTheList -> @@ -422,6 +429,15 @@ let delift ~unify metasenv subst context n l t = NCicUntrusted.map_term_fold_a (fun e (c,k,s) -> (e::c,k+1,s)) (context,k,in_scope) aux ms t in +(* + prerr_endline ( + "DELIFTO " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^ " w.r.t. " ^ + String.concat ", " (List.map (NCicPp.ppterm ~metasenv ~subst ~context) ( + let shift, lc = l in + (List.map (NCicSubstitution.lift shift) + (NCicUtils.expand_local_context lc)) + ))); +*) try aux (context,0,0) (metasenv,subst) t with NotInTheList -> (* This is the case where we fail even first order unification. *)