X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=c9ebbb93e3c269782f907802956c2c89b8d98b82;hb=40ebec98f53ac1a9a1e7a462cbf0dd3e3d8d42fd;hp=936d1ec8d0c3882e37aa444c3464e16140d26eb3;hpb=499464cf99b8eb3c251a1666b929088ad3810b43;p=helm.git diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 936d1ec8d..c9ebbb93e 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -165,6 +165,8 @@ let rec lambda_intros rdb metasenv subst context argsno ty = let unopt exc = function None -> raise exc | Some x -> x ;; let fix metasenv subst is_sup test_eq_only exc t = + (*D*) inside 'f'; try let rc = + pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context:[] t)); let rec aux test_eq_only metasenv = function | NCic.Prod (n,so,ta) -> let metasenv,so = aux true metasenv so in @@ -188,66 +190,96 @@ let fix metasenv subst is_sup test_eq_only exc t = NCicUntrusted.map_term_fold_a (fun _ x -> x) test_eq_only aux metasenv t in aux test_eq_only metasenv t + (*D*) in outside None; rc with exn -> outside (Some exn); raise exn +;; + +let metasenv_to_subst n (kind,context,ty) metasenv subst = + let infos,metasenv = List.partition (fun (n',_) -> n = n') metasenv in + let attrs,octx,oty = match infos with [_,infos] -> infos | _ -> assert false in + if octx=context && oty=ty then + (n,(NCicUntrusted.set_kind kind attrs, octx, oty))::metasenv,subst + else + let metasenv, _, bo, _ = + NCicMetaSubst.mk_meta metasenv context ~attrs ~with_type:ty kind in + let subst = (n,(NCicUntrusted.set_kind kind attrs,octx,bo,oty))::subst in + metasenv,subst ;; -let rec sortfy exc metasenv subst = function - | NCic.Sort _ as orig -> metasenv, orig - | NCic.Meta (n,lc) -> +let rec sortfy exc metasenv subst context t = + let t = NCicReduction.whd ~subst context t in + let metasenv,subst = + match t with + | NCic.Sort _ -> metasenv, subst + | NCic.Meta (n,_) -> let attrs, context, ty = NCicUtils.lookup_meta n metasenv in let kind = NCicUntrusted.kind_of_meta attrs in - kindfy exc metasenv subst context n lc ty kind `IsSort - | NCic.Implicit _ -> assert false - | _ -> raise exc - -and kindfy exc metasenv subst context n lc ty kind kind2 = - match kind, ty, kind2 with - | `IsSort, _, _ -> assert(snd lc = NCic.Irl 0); metasenv, NCic.Meta(n,lc) - | k1, NCic.Implicit (`Typeof _), (`IsType|`IsTerm as k2) -> - let k = NCicUntrusted.max_kind k1 k2 in - let metasenv = - NCicUntrusted.replace_in_metasenv n - (fun attrs,cc,ty -> NCicUntrusted.set_kind k attrs, cc, ty) metasenv - in - metasenv, NCic.Meta(n,lc) - | _, NCic.Implicit (`Typeof _), `IsSort -> - let metasenv = - NCicUntrusted.replace_in_metasenv n - (fun attrs,_,ty-> NCicUntrusted.set_kind `IsSort attrs,[],ty) metasenv - in - metasenv, NCic.Meta (n,(0,NCic.Irl 0)) - | _, ty, `IsSort -> - let metasenv, ty = - sortfy exc metasenv subst (NCicReduction.whd ~subst context ty) - in - let metasenv = - NCicUntrusted.replace_in_metasenv n - (fun attrs,_,_-> NCicUntrusted.set_kind `IsSort attrs,[],ty) metasenv - in - metasenv, NCic.Meta (n,(0,NCic.Irl 0)) - | k1, _, k2 when NCicUntrusted.max_kind k1 k2 = k1-> metasenv, NCic.Meta(n,lc) - | `IsTerm, ty, `IsType -> - let metasenv, ty = - sortfy exc metasenv subst (NCicReduction.whd ~subst context ty) - in - let metasenv = - NCicUntrusted.replace_in_metasenv n - (fun attrs,cc,_-> NCicUntrusted.set_kind `IsType attrs,cc,ty) metasenv - in - metasenv, NCic.Meta (n,lc) - | _ -> assert false (* XXX *) + if kind = `IsSort then + metasenv,subst + else + (match ty with + | NCic.Implicit (`Typeof _) -> + metasenv_to_subst n (`IsSort,[],ty) metasenv subst + | ty -> + let metasenv,subst,ty = sortfy exc metasenv subst context ty in + metasenv_to_subst n (`IsSort,[],ty) metasenv subst) + | NCic.Implicit _ -> assert false + | _ -> raise exc + in + metasenv,subst,t + +let tipify exc metasenv subst context t ty = + let is_type attrs = + match NCicUntrusted.kind_of_meta attrs with + `IsType | `IsSort -> true + | `IsTerm -> false + in + let rec optimize_meta metasenv subst = + function + NCic.Meta (n,lc) -> + (try + let attrs,_,_ = NCicUtils.lookup_meta n metasenv in + if is_type attrs then + metasenv,subst,true + else + let metasenv = + NCicUntrusted.replace_in_metasenv n + (fun attrs,cc,ty -> NCicUntrusted.set_kind `IsType attrs, cc, ty) + metasenv + in + metasenv,subst,false + with + NCicUtils.Meta_not_found _ -> + let attrs, _,bo,_ = NCicUtils.lookup_subst n subst in + if is_type attrs then + metasenv,subst,true + else + let subst = + NCicUntrusted.replace_in_subst n + (fun attrs,cc,bo,ty->NCicUntrusted.set_kind `IsType attrs,cc,bo,ty) + subst + in + optimize_meta metasenv subst (NCicSubstitution.subst_meta lc bo)) + | _ -> metasenv,subst,false + in + let metasenv,subst,b = optimize_meta metasenv subst t in + if b then + metasenv,subst,t + else + let metasenv,subst,_ = sortfy exc metasenv subst context ty in + metasenv,subst,t +;; -and instantiate rdb test_eq_only metasenv subst context n lc t swap = +let rec instantiate rdb test_eq_only metasenv subst context n lc t swap = (*D*) inside 'I'; try let rc = pp (lazy(string_of_int n^" :=?= "^ppterm ~metasenv ~subst ~context t)); let exc = UnificationFailure (mk_msg metasenv subst context (NCic.Meta (n,lc)) t) in - let move_to_subst i attrs cc t ty metasenv subst = + let move_to_subst i ((_,cc,t,_) as infos) metasenv subst = let metasenv = List.remove_assoc i metasenv in - pp (lazy(string_of_int n ^ " :==> "^ - ppterm ~metasenv ~subst ~context:cc t)); - metasenv, (i,(attrs, cc, t, ty)) :: subst + pp(lazy(string_of_int n ^ " :==> "^ ppterm ~metasenv ~subst ~context:cc t)); + metasenv, (i,infos) :: subst in - let delift_to_subst test_eq_only n lc attrs cc t ty context metasenv subst = + let delift_to_subst test_eq_only n lc (attrs,cc,ty) t context metasenv subst = pp (lazy(string_of_int n ^ " := 111 = "^ ppterm ~metasenv ~subst ~context t)); let (metasenv, subst), t = @@ -278,93 +310,106 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap = (* conjecture: always fail --> occur check *) unify rdb test_eq_only metasenv subst context t oldt with NCicUtils.Subst_not_found _ -> - move_to_subst n attrs cc t ty metasenv subst + move_to_subst n (attrs,cc,t,ty) metasenv subst in - let attrs, cc, ty = NCicUtils.lookup_meta n metasenv in - match NCicUntrusted.kind_of_meta attrs, ty, t, swap with - | `IsSort, (NCic.Implicit (`Typeof _) as bot), NCic.Sort (NCic.Type u),false-> - pp(lazy("1")); - let u = NCicEnvironment.inf ~strict:false u in - let t = NCic.Sort (NCic.Type (unopt exc u)) in - move_to_subst n attrs cc t bot metasenv subst - | `IsSort, (NCic.Implicit (`Typeof _) as bot), NCic.Sort (NCic.Type u),true -> - pp(lazy("2")); - let u = NCicEnvironment.sup u in - let t = NCic.Sort (NCic.Type (unopt exc u)) in - move_to_subst n attrs cc t bot metasenv subst - | `IsSort, (NCic.Sort(NCic.Type u1) as ty), NCic.Sort (NCic.Type u2), false -> - pp(lazy("3")); - let u = - NCicEnvironment.inf ~strict:false (u1 @ - unopt exc (NCicEnvironment.inf ~strict:true u2)) - in - let t = NCic.Sort (NCic.Type (unopt exc u)) in - move_to_subst n attrs cc t ty metasenv subst - | `IsSort, (NCic.Sort(NCic.Type u1) as ty), NCic.Sort (NCic.Type u2), true -> - pp(lazy("4")); - let u = unopt exc (NCicEnvironment.sup u2) in - if NCicEnvironment.universe_lt u u1 then - let t = NCic.Sort (NCic.Type u) in - move_to_subst n attrs cc t ty metasenv subst - else (raise exc) - | _, _, NCic.Meta(m,lcm), _ when List.mem_assoc m subst -> - (* deref needed for locked metas, maybe should be done outside *) - let _,_,bo,_ = NCicUtils.lookup_subst m subst in - let bo = NCicSubstitution.subst_meta lcm bo in - instantiate rdb test_eq_only metasenv subst context n lc bo swap - | kind, (NCic.Implicit (`Typeof _) as bot), NCic.Meta(m,lcm), _ -> - pp(lazy("5")); - let attrsm, ccm, tym = NCicUtils.lookup_meta m metasenv in - let kindm = NCicUntrusted.kind_of_meta attrsm in - let metasenv, t = kindfy exc metasenv subst ccm m lcm tym kindm kind in - move_to_subst n attrs cc t bot metasenv subst - | kind, ty, (NCic.Meta(m,_) as t), _ when - let _, _, tym = NCicUtils.lookup_meta m metasenv in - (match tym with NCic.Implicit (`Typeof _) -> true | _ -> false) -> - pp(lazy("6")); - let attrsm, _, _ = NCicUtils.lookup_meta m metasenv in - let kindm = NCicUntrusted.kind_of_meta attrsm in - let metasenv, _ = kindfy exc metasenv subst cc n lc ty kind kindm in - let attrs, cc, ty = NCicUtils.lookup_meta n metasenv in - let metasenv = NCicUntrusted.replace_in_metasenv m - (fun _,_,_ -> attrs,cc,ty) metasenv - in - (* XXX *)move_to_subst n attrs cc t ty metasenv subst - | kind, ty, NCic.Meta(m,lcm), _ -> - pp(lazy("7")); - let ty_t, ccm, kindm = - let at, ccm, tym = NCicUtils.lookup_meta m metasenv in - NCicSubstitution.subst_meta lcm tym, ccm, NCicUntrusted.kind_of_meta at - in - let lty = NCicSubstitution.subst_meta lc ty in - pp (lazy ("On the types: " ^ - ppterm ~metasenv ~subst ~context lty ^ - (if test_eq_only then " === " else "=<=") ^ - ppterm ~metasenv ~subst ~context ty_t)); - let metasenv, subst = - unify rdb test_eq_only metasenv subst context ty_t lty - in - let metasenv, t = kindfy exc metasenv subst ccm m lcm ty_t kindm kind in - delift_to_subst test_eq_only n lc attrs cc t ty context metasenv subst - | _, (NCic.Implicit (`Typeof _) as bot), t, swap -> - pp(lazy("8")); - let metasenv, t = fix metasenv subst swap test_eq_only exc t in -(* let ty_t = NCicTypeChecker.typeof ~metasenv ~subst context t in *) - (* ty andrebbe deliftato *) - delift_to_subst test_eq_only n lc attrs cc t bot context metasenv subst - | _, ty, t, swap -> - pp(lazy("9")); - let lty = NCicSubstitution.subst_meta lc ty in - let metasenv, t = fix metasenv subst swap test_eq_only exc t in - let ty_t = NCicTypeChecker.typeof ~metasenv ~subst context t in - pp (lazy ("On the types: " ^ - ppterm ~metasenv ~subst ~context lty ^ - (if test_eq_only then " === " else "=<=") ^ - ppterm ~metasenv ~subst ~context ty_t)); - let metasenv, subst = - unify rdb test_eq_only metasenv subst context ty_t lty - in - delift_to_subst test_eq_only n lc attrs cc t ty context metasenv subst + let attrs,cc,ty = NCicUtils.lookup_meta n metasenv in + let kind = NCicUntrusted.kind_of_meta attrs in + let metasenv,t = fix metasenv subst swap test_eq_only exc t in + let ty_t = NCicTypeChecker.typeof ~metasenv ~subst context t in + let metasenv,subst,t = + match kind with + `IsSort -> sortfy exc metasenv subst context t + | `IsType -> tipify exc metasenv subst context t ty_t + | `IsTerm -> metasenv,subst,t in + match kind with + | `IsSort -> + (match ty,t with + NCic.Implicit (`Typeof _), NCic.Sort _ -> + move_to_subst n (attrs,cc,t,ty_t) metasenv subst + | NCic.Sort (NCic.Type u1), NCic.Sort s -> + let s = + match s,swap with + NCic.Type u2, false -> + NCic.Sort (NCic.Type + (unopt exc (NCicEnvironment.inf ~strict:false + (unopt exc (NCicEnvironment.inf ~strict:true u1) @ u2)))) + | NCic.Type u2, true -> + if NCicEnvironment.universe_lt u2 u1 then + NCic.Sort (NCic.Type u2) + else (raise exc) + | NCic.Prop,_ -> NCic.Sort NCic.Prop + in + move_to_subst n (attrs,cc,s,ty) metasenv subst + | NCic.Implicit (`Typeof _), NCic.Meta _ -> + move_to_subst n (attrs,cc,t,ty_t) metasenv subst + | _, NCic.Meta _ + | NCic.Meta _, NCic.Sort _ -> + pp (lazy ("On the types: " ^ + ppterm ~metasenv ~subst ~context ty ^ "=<=" ^ + ppterm ~metasenv ~subst ~context ty_t)); + let metasenv, subst = + unify rdb false metasenv subst context ty_t ty in + delift_to_subst test_eq_only n lc (attrs,cc,ty) t + context metasenv subst + | _ -> assert false) + | `IsType + | `IsTerm -> + (match ty,t with + NCic.Implicit (`Typeof _), _ -> + let (metasenv, subst), ty_t = + try + NCicMetaSubst.delift + ~unify:(fun m s c t1 t2 -> + let ind = !indent in + let res = try Some (unify rdb test_eq_only m s c t1 t2 ) + with UnificationFailure _ | Uncertain _ -> None + in + indent := ind; res) + metasenv subst context n lc ty_t + with NCicMetaSubst.Uncertain msg -> + pp (lazy ("delift is uncertain: " ^ Lazy.force msg)); + raise (Uncertain msg) + | NCicMetaSubst.MetaSubstFailure msg -> + pp (lazy ("delift fails: " ^ Lazy.force msg)); + raise (UnificationFailure msg) + in + delift_to_subst test_eq_only n lc (attrs,cc,ty_t) t context metasenv + subst + | _, _ -> + let lty = NCicSubstitution.subst_meta lc ty in + pp (lazy ("On the types: " ^ + ppterm ~metasenv ~subst ~context lty ^ "=<=" ^ + ppterm ~metasenv ~subst ~context ty_t)); + let metasenv, subst = + unify rdb false metasenv subst context ty_t lty + in + delift_to_subst test_eq_only n lc (attrs,cc,ty) t context metasenv + subst) +(* + | kind, ty, NCic.Meta(m,lcm), _ when List.mem_assoc m subst -> + let at,ccm,bo,tym = NCicUtils.lookup_subst m subst in + if NCicMetaSubst.is_out_scope_tag at then + begin + (* Case meta vs out-scope *) + pp(lazy("4.1")); + let ty_t, ccm, kindm = + NCicSubstitution.subst_meta lcm tym, ccm, + NCicUntrusted.kind_of_meta at in + let lty = NCicSubstitution.subst_meta lc ty in + pp (lazy ("On the types: " ^ + ppterm ~metasenv ~subst ~context lty ^ "=<=" ^ + ppterm ~metasenv ~subst ~context ty_t)); + let metasenv, subst = + unify rdb false metasenv subst context ty_t lty in + (*CSC: here I should call kindfy, but it fails since the second + meta in in the susbt, not the metasenv! *) + (* let metasenv,subst,t = kindfy exc metasenv subst ccm m lcm ty_t kindm kind in *) + delift_to_subst test_eq_only n lc attrs cc t ty context metasenv subst + end + else + let bo = NCicSubstitution.subst_meta lcm bo in + instantiate rdb test_eq_only metasenv subst context n lc bo swap +*) (*D*) in outside None; rc with exn -> outside (Some exn); raise exn and unify rdb test_eq_only metasenv subst context t1 t2 =