X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=edf116d17f08c94464887b7fb609301329e0f217;hb=f8d45b2e4fa7817d7ef8312b3bb8a7439bd7fb8c;hp=8e84c015dbed4c19508b876409678e03e523f22e;hpb=8e0e2b06cfc3fb3116e1fce632d9897fdbac9895;p=helm.git diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 8e84c015d..edf116d17 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -115,26 +115,8 @@ let ppmetasenv ~subst m = "\nmenv:\n" ^ NCicPp.ppmetasenv ~subst m;; let ppcontext ~metasenv:_metasenv ~subst:_subst _context = "";; let ppmetasenv ~subst:_subst _metasenv = "";; - -let fix_sorts swap exc t = - let rec aux () = function - | NCic.Sort (NCic.Type u) as orig -> - if swap then - match NCicEnvironment.sup u with - | None -> - prerr_endline ("no sup for " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] orig) ; - raise exc - | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1) - else - NCic.Sort (NCic.Type ( - match NCicEnvironment.sup NCicEnvironment.type0 with - | Some x -> x - | _ -> assert false)) - | NCic.Meta _ as orig -> orig - | t -> NCicUtils.map (fun _ _ -> ()) () aux t - in - aux () t -;; +let ppterm ~metasenv ~subst ~context = NCicPp.ppterm ~metasenv ~subst ~context;; +(* let ppterm ~metasenv:_ ~subst:_ ~context:_ _ = "";; *) let is_locked n subst = try @@ -162,11 +144,11 @@ let rec could_reduce = ;; let rec lambda_intros rdb metasenv subst context argsno ty = - pp (lazy ("LAMBDA INTROS: " ^ NCicPp.ppterm ~metasenv ~subst ~context ty)); + pp (lazy ("LAMBDA INTROS: " ^ ppterm ~metasenv ~subst ~context ty)); match argsno with 0 -> let metasenv, _, bo, _ = - NCicMetaSubst.mk_meta metasenv context (`WithType ty) + NCicMetaSubst.mk_meta metasenv context ~with_type:ty `IsTerm in metasenv, bo | _ -> @@ -179,181 +161,221 @@ let rec lambda_intros rdb metasenv subst context argsno ty = metasenv,C.Lambda (n,so,bo) | _ -> assert false) ;; + +let unopt exc = function None -> raise exc | Some x -> x ;; + +let fix metasenv subst is_sup test_eq_only exc t = + let rec aux test_eq_only metasenv = function + | NCic.Prod (n,so,ta) -> + let metasenv,so = aux true metasenv so in + let metasenv,ta = aux test_eq_only metasenv ta in + metasenv,NCic.Prod (n,so,ta) + | NCic.Sort (NCic.Type [(`CProp|`Type),_]) as orig when test_eq_only -> + metasenv,orig + | NCic.Sort (NCic.Type _) when test_eq_only -> raise exc + | NCic.Sort (NCic.Type u) when is_sup -> + metasenv, NCic.Sort (NCic.Type (unopt exc (NCicEnvironment.sup u))) + | NCic.Sort (NCic.Type u) -> + metasenv, NCic.Sort (NCic.Type + (unopt exc (NCicEnvironment.inf ~strict:false u))) + | NCic.Meta (n,_) as orig -> + (try + let _,_,_,_ = NCicUtils.lookup_subst n subst in metasenv,orig + with NCicUtils.Subst_not_found _ -> + let metasenv, _ = NCicMetaSubst.extend_meta metasenv n in + metasenv, orig) + | t -> + NCicUntrusted.map_term_fold_a (fun _ x -> x) test_eq_only aux metasenv t + in + aux test_eq_only metasenv t +;; + +let rec sortfy exc metasenv subst = function + | NCic.Sort _ as orig -> metasenv, orig + | NCic.Meta (n,lc) -> + 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 *) -let rec instantiate rdb test_eq_only metasenv subst context n lc t swap = +and instantiate rdb test_eq_only metasenv subst context n lc t swap = (*D*) inside 'I'; try let rc = - pp (lazy(string_of_int n ^ " :=?= "^ - NCicPp.ppterm ~metasenv ~subst ~context t)); - let unify test_eq_only m s c t1 t2 = - if swap then unify rdb test_eq_only m s c t2 t1 - else unify rdb test_eq_only m s c t1 t2 - in - let has_tag = List.exists in - let tags, _, ty = NCicUtils.lookup_meta n metasenv in - (* on the types *) - let metasenv, subst, t = - match ty with - | NCic.Implicit (`Typeof _) -> - pp(lazy("meta with no type")); - assert(has_tag ((=)`IsSort) tags); - metasenv, subst, t - | _ -> - let exc_to_be = - UnificationFailure (mk_msg metasenv subst context (NCic.Meta (n,lc)) t) - in - let t, ty_t = - try t, NCicTypeChecker.typeof ~subst ~metasenv context t - with - | NCicTypeChecker.AssertFailure msg as exn -> - pp(lazy("we try to fix the sort\n"^ - Lazy.force msg^"\n"^NCicPp.ppmetasenv ~subst metasenv)); - let ft = fix_sorts swap exc_to_be t in - pp(lazy("unable to fix the sort")); - if ft == t then raise exn; - (try ft, NCicTypeChecker.typeof ~subst ~metasenv context ft - with NCicTypeChecker.AssertFailure _ -> raise exn) - | NCicTypeChecker.TypeCheckerFailure msg -> - prerr_endline (Lazy.force msg); - prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t); - prerr_endline (ppcontext ~metasenv ~subst context); - prerr_endline (ppmetasenv ~subst metasenv); - assert false - in - match ty_t with - | NCic.Implicit (`Typeof _) -> - raise (UnificationFailure(lazy "trying to unify a term with a type")) - | _ -> - let lty = NCicSubstitution.subst_meta lc ty in - pp (lazy ("On the types: " ^ - NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === " ^ - NCicPp.ppterm ~metasenv ~subst ~context ty_t)); - let metasenv,subst = - try unify test_eq_only metasenv subst context lty ty_t - with NCicEnvironment.BadConstraint _ as exc -> - let ty_t = fix_sorts swap exc_to_be ty_t in - try unify test_eq_only metasenv subst context lty ty_t - with - | NCicEnvironment.BadConstraint _ - | UnificationFailure _ -> raise exc - in - metasenv, subst, t - in - (* viral sortification *) - let is_sort metasenv subst context t = - match NCicReduction.whd ~subst context t with - | NCic.Meta (i,_) -> - let tags, _, _ = NCicUtils.lookup_meta i metasenv in - has_tag ((=) `IsSort) tags - | NCic.Sort _ -> true - | _ -> false + 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 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 in - let rec sortify metasenv subst = function - | NCic.Implicit (`Typeof _) -> assert false - | NCic.Sort _ as t -> metasenv, subst, t, 0 - | NCic.Meta (i,_) as t -> - let tags, context, ty = NCicUtils.lookup_meta i metasenv in - if has_tag ((=) `IsSort) tags then metasenv, subst, t, i - else - let ty = NCicReduction.whd ~subst context ty in - let metasenv, subst, ty, _ = sortify metasenv subst ty in - let metasenv, j, m, _ = - NCicMetaSubst.mk_meta metasenv ~attrs:[`IsSort] [] (`WithType ty) + let delift_to_subst test_eq_only n lc attrs cc t ty context metasenv subst = + pp (lazy(string_of_int n ^ " := 111 = "^ + ppterm ~metasenv ~subst ~context t)); + let (metasenv, subst), 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 - pp(lazy("rimpiazzo " ^ string_of_int i^" con "^string_of_int j)); - let subst_entry = i, (tags, context, m, ty) in - let subst = subst_entry :: subst in - let metasenv = List.filter (fun x,_ -> i <> x) metasenv in - metasenv, subst, m, j - | NCic.Appl (NCic.Meta _ as hd :: args) as t -> - let metasenv, lambda_Mj = - lambda_intros rdb metasenv subst context (List.length args) - (NCicTypeChecker.typeof ~metasenv ~subst context hd) - in - let metasenv,subst= unify true metasenv subst context hd lambda_Mj in - let t = NCicReduction.whd ~subst context t in - let _result = sortify metasenv subst t in - (* untested, maybe dead, code *) assert false; - | t -> - if could_reduce t then raise (Uncertain(lazy "not a sort")) - else raise (UnificationFailure(lazy "not a sort")) - in - let metasenv, subst, _, n = - if has_tag ((=) `IsSort) tags then - let m,s,x,_ = sortify metasenv subst (NCicReduction.whd ~subst context t) - in m,s,x,n - else if is_sort metasenv subst context t then - sortify metasenv subst (NCic.Meta (n,lc)) - else - metasenv, subst, NCic.Rel ~-1,n - in - let tags, ctx, ty = NCicUtils.lookup_meta n metasenv in - (* instantiation *) - pp (lazy(string_of_int n ^ " := 111 = "^ - NCicPp.ppterm ~metasenv ~subst ~context t)); - let (metasenv, subst), t = - try - NCicMetaSubst.delift - ~unify:(fun m s c t1 t2 -> - let ind = !indent in - let res = - try Some (unify test_eq_only m s c t1 t2 ) - with UnificationFailure _ | Uncertain _ -> None - in - indent := ind; res) - metasenv subst context n lc t - with NCicMetaSubst.Uncertain msg -> - pp (lazy ("delift fails: " ^ Lazy.force msg)); - raise (Uncertain msg) - | NCicMetaSubst.MetaSubstFailure msg -> - pp (lazy ("delift fails: " ^ Lazy.force msg)); - raise (UnificationFailure msg) - in - pp (lazy(string_of_int n ^ " := 222 = "^ - NCicPp.ppterm ~metasenv ~subst ~context:ctx t - ^ ppmetasenv ~subst metasenv)); - (* Unifying the types may have already instantiated n. *) - try - let _, _,oldt,_ = NCicUtils.lookup_subst n subst in - let oldt = NCicSubstitution.subst_meta lc oldt in - let t = NCicSubstitution.subst_meta lc t in - (* conjecture: always fail --> occur check *) - unify test_eq_only metasenv subst context oldt t - with NCicUtils.Subst_not_found _ -> - let metasenv, tags = - let rec aux = function - | NCic.Meta (j,lc) -> - (try - let _, _, t, _ = NCicUtils.lookup_subst j subst in - aux (NCicSubstitution.subst_meta lc t) - with NCicUtils.Subst_not_found _ -> - let tags', ctx, ty = NCicUtils.lookup_meta j metasenv in - let metasenv = List.remove_assoc j metasenv in - let tags = tags @ tags' in - (j, (tags, ctx, ty)) :: metasenv, tags) - | _ -> metasenv, tags - in - aux t + indent := ind; res) + metasenv subst context n lc 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 - (* by cumulativity when unify(?,Type_i) - * we could ? := Type_j with j <= i... *) - let subst = (n, (tags, ctx, t, ty)) :: subst in - pp (lazy ("?"^string_of_int n^" := "^NCicPp.ppterm - ~metasenv ~subst ~context (NCicSubstitution.subst_meta lc t))); - let metasenv = - List.filter (fun (m,_) -> not (n = m)) metasenv - in - metasenv, subst + pp (lazy(string_of_int n ^ " := 222 = "^ + ppterm ~metasenv ~subst ~context:cc t^ppmetasenv ~subst metasenv)); + (* Unifying the types may have already instantiated n. *) + try + let _, _,oldt,_ = NCicUtils.lookup_subst n subst in + let oldt = NCicSubstitution.subst_meta lc oldt in + let t = NCicSubstitution.subst_meta lc t in + (* 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 + 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 (*D*) in outside None; rc with exn -> outside (Some exn); raise exn and unify rdb test_eq_only metasenv subst context t1 t2 = (*D*) inside 'U'; try let rc = let fo_unif test_eq_only metasenv subst (norm1,t1) (norm2,t2) = (*D*) inside 'F'; try let rc = - pp (lazy(" " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^ - NCicPp.ppterm ~metasenv ~subst ~context t2 ^ ppmetasenv + pp (lazy(" " ^ ppterm ~metasenv ~subst ~context t1 ^ " ==?== " ^ + ppterm ~metasenv ~subst ~context t2 ^ ppmetasenv ~subst metasenv)); - pp (lazy(" " ^ NCicPp.ppterm ~metasenv ~subst:[] ~context t1 ^ " ==??== " ^ - NCicPp.ppterm ~metasenv ~subst:[] ~context t2 ^ ppmetasenv + pp (lazy(" " ^ ppterm ~metasenv ~subst:[] ~context t1 ^ " ==??== " ^ + ppterm ~metasenv ~subst:[] ~context t2 ^ ppmetasenv ~subst metasenv)); if t1 === t2 then metasenv, subst @@ -614,8 +636,8 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = let try_hints metasenv subst (_,t1 as mt1) (_,t2 as mt2) (* exc*) = (*D*) inside 'H'; try let rc = pp(lazy ("\nProblema:\n" ^ - NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " =?= " ^ - NCicPp.ppterm ~metasenv ~subst ~context t2)); + ppterm ~metasenv ~subst ~context t1 ^ " =?= " ^ + ppterm ~metasenv ~subst ~context t2)); let candidates = NCicUnifHint.look_for_hint rdb metasenv subst context t1 t2 in @@ -626,11 +648,11 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = String.concat "\n" (List.map (fun (a,b) -> - NCicPp.ppterm ~metasenv ~subst ~context a ^ " =?= " ^ - NCicPp.ppterm ~metasenv ~subst ~context b) premises) ^ + ppterm ~metasenv ~subst ~context a ^ " =?= " ^ + ppterm ~metasenv ~subst ~context b) premises) ^ "\n-------------------------------------------\n"^ - NCicPp.ppterm ~metasenv ~subst ~context c1 ^ " = " ^ - NCicPp.ppterm ~metasenv ~subst ~context c2)); + ppterm ~metasenv ~subst ~context c1 ^ " = " ^ + ppterm ~metasenv ~subst ~context c2)); try (*D*) inside 'K'; try let rc = let metasenv,subst = @@ -657,7 +679,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = NCicReduction.reduce_machine ~delta:max_int ~subst context m1, NCicReduction.reduce_machine ~delta:max_int ~subst context m2 in - let fo_unif_w_hints test_eq_only metasenv subst (xx1,t1 as m1) (xx2,t2 as m2) = + let fo_unif_w_hints test_eq_only metasenv subst (_,t1 as m1) (_,t2 as m2) = try fo_unif test_eq_only metasenv subst m1 m2 with | UnificationFailure _ as exn -> raise exn @@ -703,10 +725,10 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) -> (*D*) inside 'M'; try let rc = pp (lazy("UM: " ^ - NCicPp.ppterm ~metasenv ~subst ~context + ppterm ~metasenv ~subst ~context (NCicReduction.unwind (k1,e1,t1,s1)) ^ " === " ^ - NCicPp.ppterm ~metasenv ~subst ~context + ppterm ~metasenv ~subst ~context (NCicReduction.unwind (k2,e2,t2,s2)))); pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2)); let relevance = [] (* TO BE UNDERSTOOD @@ -789,4 +811,6 @@ let unify rdb ?(test_eq_only=false) = indent := ""; unify rdb test_eq_only;; -let fix_sorts = fix_sorts true (UnificationFailure (lazy "no sup"));; +let fix_sorts m s = + fix m s true false (UnificationFailure (lazy "no sup")) +;;