From 00d66d5ac17cc72d525d8b2cd089a963e1fef3bf Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 20 Jul 2009 09:57:32 +0000 Subject: [PATCH] =?utf8?q?1)=20ppmetasenv=20and=20ppcontext=20to=20reduce?= =?utf8?q?=20the=20amount=20of=20printed=20information=20during=20=20=20?= =?utf8?q?=20debugging=202)=20BUG=20FIXED:=20boxes=20(in=20particular=20ou?= =?utf8?q?t=5Fscope=20ones)=20could=20happear=20in=20the=20=20=20=20substi?= =?utf8?q?tution=20after=20unification.=20In=20particular,=20this=20happen?= =?utf8?q?ed=20when=20the=20goal=20=20=20=20had=20the=20form=20=20=20H:=20?= =?utf8?q?False=20|-=20C=20=20and=20we=20tried=20to=20"nelim=20H".=20After?= =?utf8?q?=20the=20=20=20=20unification,=20some=20meta=20=3F1=20was=20inst?= =?utf8?q?antiated=20with=20=3Fos=20where=20=3Fos=20:=3D=20C.=20This=20=20?= =?utf8?q?=20=20triggered=20a=20unification=20C=20=3D=3F=3D=20=3F1=20befor?= =?utf8?q?e=20the=20end=20of=20the=20tactic=20(hence=20=20=20=20before=20t?= =?utf8?q?he=20apply=5Fsubst).=20As=20a=20result,=20the=20ad-hoc=20unifica?= =?utf8?q?tion=20case=20for=20=20=20=20in=5Fscope/out=5Fscope=20was=20trig?= =?utf8?q?gered=20on=20inputs=20of=20the=20bad=20shape=20and=20an=20assert?= =?utf8?q?=20=20=20=20false=20was=20raised.?= --- .../components/ng_refiner/nCicUnification.ml | 34 +++++++++++++++---- 1 file changed, 27 insertions(+), 7 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index bfa1388a9..13ddac96d 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -84,7 +84,13 @@ let outside () = indent := String.sub !indent 0 (String.length !indent -1);; let pp s = prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s) -;; +;; + +let ppcontext = NCicPp.ppcontext;; +let ppmetasenv = NCicPp.ppmetasenv;; + +(*let ppcontext ~metasenv ~subst context = "...";; +let ppmetasenv ~subst metasenv = "...";;*) let pp _ = ();; @@ -151,8 +157,8 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap = | _ -> pp (lazy ( "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^ "\nctx:\n"^ - NCicPp.ppcontext ~metasenv ~subst context ^ "\nmenv:\n"^ - NCicPp.ppmetasenv ~subst metasenv)); + ppcontext ~metasenv ~subst context ^ "\nmenv:\n"^ + ppmetasenv ~subst metasenv)); let t, ty_t = try t, NCicTypeChecker.typeof ~subst ~metasenv context t with @@ -163,8 +169,8 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap = (prerr_endline ( ("ILLTYPED: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^ "\nBECAUSE:" ^ Lazy.force msg ^ "\nCONTEXT:\n" ^ - NCicPp.ppcontext ~metasenv ~subst context ^ "\nMENV:\n" ^ - NCicPp.ppmetasenv ~subst metasenv + ppcontext ~metasenv ~subst context ^ "\nMENV:\n" ^ + ppmetasenv ~subst metasenv )); assert false) else @@ -214,7 +220,7 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap = in pp (lazy(string_of_int n ^ " := 222 = "^ NCicPp.ppterm ~metasenv ~subst ~context:ctx t - ^ "\n" ^ NCicPp.ppmetasenv ~subst metasenv)); + ^ "\n" ^ ppmetasenv ~subst metasenv)); (* Unifying the types may have already instantiated n. *) try let _, _,oldt,_ = NCicUtils.lookup_subst n subst in @@ -239,7 +245,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = let fo_unif test_eq_only metasenv subst t1 t2 = (*D*) inside 'F'; try let rc = pp (lazy(" " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^ - NCicPp.ppterm ~metasenv ~subst ~context t2 ^ "\n" ^ NCicPp.ppmetasenv + NCicPp.ppterm ~metasenv ~subst ~context t2 ^ "\n" ^ ppmetasenv ~subst metasenv)); if t1 === t2 then metasenv, subst @@ -324,6 +330,20 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = let metasenv, subst = instantiate rdb test_eq_only metasenv subst context j lj t2 true in + (* We need to remove the out_scope_tags to avoid propagation of + them that triggers again the ad-hoc case *) + let subst = + List.map (fun (i,(tag,ctx,bo,ty)) -> + let tag = + match tag with + Some tag when + tag = NCicMetaSubst.in_scope_tag + || NCicMetaSubst.is_out_scope_tag tag -> None + | _ -> tag + in + i,(tag,ctx,bo,ty) + ) subst + in (try let name, ctx, term, ty = NCicUtils.lookup_subst i subst in let term = eta_reduce subst term in -- 2.39.2