From: Enrico Tassi Date: Mon, 28 Sep 2009 16:14:46 +0000 (+0000) Subject: - fixed bug in coercion application, input/output swapped in unification X-Git-Tag: make_still_working~3426 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f1c4852a4359cf278ed00d73d608856ff46bafbb;p=helm.git - fixed bug in coercion application, input/output swapped in unification - experimental automatic reduction of projections in apply-subst-metasenv --- diff --git a/helm/software/components/ng_kernel/nCicUntrusted.ml b/helm/software/components/ng_kernel/nCicUntrusted.ml index 633ecea57..fd3fd5f79 100644 --- a/helm/software/components/ng_kernel/nCicUntrusted.ml +++ b/helm/software/components/ng_kernel/nCicUntrusted.ml @@ -168,7 +168,37 @@ let clean_or_fix_dependent_abstrations ctx t = aux (List.map fst ctx) t ;; -let apply_subst subst context t = +let rec fire_projection_redex () = function + | C.Meta _ as t -> t + | C.Appl(C.Const(Ref.Ref(_,Ref.Fix(fno,rno,_)) as r)::args as ol)as ot-> + let l = List.map (fire_projection_redex ()) ol in + let t = if l == ol then ot else C.Appl l in + let ifl,(_,_,pragma),_ = NCicEnvironment.get_checked_fixes_or_cofixes r in + let conclude () = + let l' = HExtlib.sharing_map (fire_projection_redex ()) l in + if l == l' then t else C.Appl l' + in + if (*pragma <> `Projection ||*) List.length args < rno then conclude () + else + (match List.nth args rno with + | C.Appl (C.Const(Ref.Ref(_,Ref.Con _))::_) -> + let _, _, _, _, fbody = List.nth ifl fno in (* fbody is closed! *) + let t = C.Appl (fbody::args) in + (match NCicReduction.head_beta_reduce ~delta:max_int t with + | C.Match (_,_,C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno)))::kargs),[pat])-> + let _,kargs = HExtlib.split_nth leftno kargs in + NCicReduction.head_beta_reduce + ~delta:max_int (C.Appl (pat :: kargs)) + | C.Appl(C.Match(_,_,C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno)))::kargs),[pat]) :: args) -> + let _,kargs = HExtlib.split_nth leftno kargs in + NCicReduction.head_beta_reduce + ~delta:max_int (C.Appl (pat :: kargs @ args)) + | _ -> conclude ()) + | _ -> conclude ()) + | t -> NCicUtils.map (fun _ _ -> ()) () fire_projection_redex t +;; + +let apply_subst ?(fix_projections=false) subst context t = let rec apply_subst subst () = function NCic.Meta (i,lc) -> @@ -187,10 +217,12 @@ let apply_subst subst context t = apply_subst subst () (NCicSubstitution.lift n t)) l)))) | t -> NCicUtils.map (fun _ () -> ()) () (apply_subst subst) t in - clean_or_fix_dependent_abstrations context (apply_subst subst () t) + (if fix_projections then fire_projection_redex () else fun x -> x) + (clean_or_fix_dependent_abstrations context (apply_subst subst () t)) ;; -let apply_subst_context subst context = +let apply_subst_context ~fix_projections subst context = + let apply_subst = apply_subst ~fix_projections in let rec aux c = function | [] -> [] | (name,NCic.Decl t as e) :: tl -> @@ -206,6 +238,11 @@ let rec apply_subst_metasenv subst = function | [] -> [] | (i,_) :: _ when List.mem_assoc i subst -> assert false | (i,(name,ctx,ty)) :: tl -> - (i,(name,apply_subst_context subst ctx,apply_subst subst ctx ty)) :: + (i,(name,apply_subst_context ~fix_projections:true subst ctx, + apply_subst ~fix_projections:true subst ctx ty)) :: apply_subst_metasenv subst tl ;; + +(* hide optional arg *) +let apply_subst s c t = apply_subst s c t;; + diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index a1ce81470..a74946f1e 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -380,15 +380,16 @@ and try_coercions rdb (NCicPp.ppterm ~metasenv ~subst ~context expty))) exc) | (_,metasenv, newterm, newtype, meta)::tl -> try + pp (lazy("K=" ^ NCicPp.ppterm ~metasenv ~subst ~context newterm)); pp (lazy ( "UNIFICATION in CTX:\n"^ NCicPp.ppcontext ~metasenv ~subst context ^ "\nMENV: " ^ NCicPp.ppmetasenv metasenv ~subst ^ "\nOF: " ^ - NCicPp.ppterm ~metasenv ~subst ~context meta ^ " === " ^ - NCicPp.ppterm ~metasenv ~subst ~context t ^ "\n")); + NCicPp.ppterm ~metasenv ~subst ~context t ^ " === " ^ + NCicPp.ppterm ~metasenv ~subst ~context meta ^ "\n")); let metasenv, subst = - NCicUnification.unify rdb metasenv subst context meta t + NCicUnification.unify rdb metasenv subst context t meta in pp (lazy ( "UNIFICATION in CTX:\n"^ NCicPp.ppcontext ~metasenv ~subst context