X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=0e119f34b73949079b03cce21be67e0173f8d6ef;hb=a338e0effc313d4da419d6df91397232c24170d9;hp=d34e3efcc00abb6a485ecafe1de844b8ea9f902d;hpb=a981b42002f822aa49a41b3889a76b9438b093bb;p=helm.git diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index d34e3efcc..0e119f34b 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -80,6 +80,25 @@ let pp s = let pp _ = ();; +let fix_sorts swap metasenv subst context meta 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" ; + raise (fail_exc metasenv subst context meta t) + | 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 rec beta_expand num test_eq_only swap metasenv subst context t arg = let rec aux (n,context,test_eq_only as k) (metasenv, subst as acc) t' = try @@ -142,33 +161,77 @@ and beta_expand_many test_equality_only swap metasenv subst context t args = (* (*D*) in outside (); rc with exn -> outside (); raise exn *) and instantiate test_eq_only metasenv subst context n lc t swap = -(* (*D*) inside 'I'; try let rc = *) + (*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 test_eq_only m s c t2 t1 else unify test_eq_only m s c t1 t2 in - let ty_t = - try NCicTypeChecker.typeof ~subst ~metasenv context t - with NCicTypeChecker.TypeCheckerFailure msg -> - prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t); - prerr_endline (Lazy.force msg); - assert false - in let name, ctx, ty = NCicUtils.lookup_meta n metasenv in - 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 = unify test_eq_only metasenv subst context lty ty_t in + let metasenv, subst, t = + match ty with + | NCic.Implicit (`Typeof _) -> + metasenv,subst, t + (* fix_sorts swap metasenv subst context (NCic.Meta(n,lc)) t *) + | _ -> + pp (lazy ( + "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^ "\nctx:\n"^ + NCicPp.ppcontext ~metasenv ~subst context ^ "\nmenv:\n"^ + NCicPp.ppmetasenv ~subst metasenv)); + let t, ty_t = + try t, NCicTypeChecker.typeof ~subst ~metasenv context t + with + | NCicTypeChecker.AssertFailure msg -> + (pp (lazy "fine typeof (fallimento)"); + let ft = + fix_sorts swap metasenv subst context (NCic.Meta (n,lc)) t + in + if ft == t then + (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 + )); + assert false) + else + try + pp (lazy ("typeof: " ^ + NCicPp.ppterm ~metasenv ~subst ~context ft)); + ft, NCicTypeChecker.typeof ~subst ~metasenv context ft + with NCicTypeChecker.AssertFailure _ -> + assert false) + | NCicTypeChecker.TypeCheckerFailure msg -> + pp msg; assert false + in + let lty = NCicSubstitution.subst_meta lc ty in + pp (lazy("On the types: " ^ + NCicPp.ppterm ~metasenv ~subst ~context:ctx ty ^ " ~~~ " ^ + NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === " + ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t)); + let metasenv,subst= unify test_eq_only metasenv subst context lty ty_t in + metasenv, subst, t + in + pp (lazy(string_of_int n ^ " := 111 = "^ + NCicPp.ppterm ~metasenv ~subst ~context t)); let (metasenv, subst), t = try NCicMetaSubst.delift metasenv subst context n lc t - with NCicMetaSubst.Uncertain msg -> raise (Uncertain msg) - | NCicMetaSubst.MetaSubstFailure msg -> raise (UnificationFailure msg) + 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 + ^ "\n" ^ NCicPp.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 _ -> @@ -176,21 +239,19 @@ and instantiate test_eq_only metasenv subst context n lc t swap = * we could ? := Type_j with j <= i... *) let subst = (n, (name, ctx, t, ty)) :: subst in pp (lazy ("?"^string_of_int n^" := "^NCicPp.ppterm - ~metasenv ~subst ~context:ctx (NCicSubstitution.subst_meta lc t))); + ~metasenv ~subst ~context (NCicSubstitution.subst_meta lc t))); let metasenv = List.filter (fun (m,_) -> not (n = m)) metasenv in metasenv, subst -(* (*D*) in outside(); rc with exn -> outside (); raise exn *) + (*D*) in outside(); rc with exn -> outside (); raise exn and unify test_eq_only metasenv subst context t1 t2 = -(* (*D*) inside 'U'; try let rc = *) + (*D*) inside 'U'; try let rc = let fo_unif test_eq_only metasenv subst t1 t2 = -(* (*D*) inside 'F'; try let rc = *) -(* + (*D*) inside 'F'; try let rc = pp (lazy(" " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^ NCicPp.ppterm ~metasenv ~subst ~context t2)); -*) if t1 === t2 then metasenv, subst else @@ -232,10 +293,12 @@ and unify test_eq_only metasenv subst context t1 t2 = metasenv, subst, i::to_restrict, i-1) l1 l2 (metasenv, subst, [], List.length l1) in - let metasenv, subst, _ = - NCicMetaSubst.restrict metasenv subst n1 to_restrict - in - metasenv, subst + if to_restrict <> [] then + let metasenv, subst, _ = + NCicMetaSubst.restrict metasenv subst n1 to_restrict + in + metasenv, subst + else metasenv, subst with | Invalid_argument _ -> assert false | NCicMetaSubst.MetaSubstFailure msg -> @@ -374,7 +437,7 @@ and unify test_eq_only metasenv subst context t1 t2 = raise (uncert_exc metasenv subst context t1 t2)) | (C.Implicit _, _) | (_, C.Implicit _) -> assert false | _ -> raise (uncert_exc metasenv subst context t1 t2) -(* (*D*) in outside(); rc with exn -> outside (); raise exn *) + (*D*) in outside(); rc with exn -> outside (); raise exn in let height_of = function | NCic.Const (Ref.Ref (_,Ref.Def h)) @@ -405,7 +468,7 @@ and unify test_eq_only metasenv subst context t1 t2 = let rec unif_machines metasenv subst = function | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) -> -(* (*D*) inside 'M'; try let rc = *) + (*D*) inside 'M'; try let rc = (* pp (lazy((if are_normal then "*" else " ") ^ " " ^ NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m1) ^ @@ -440,7 +503,7 @@ and unify test_eq_only metasenv subst context t1 t2 = try check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst) with UnificationFailure _ | Uncertain _ when not (norm1 && norm2) -> unif_machines metasenv subst (small_delta_step m1 m2) -(* (*D*) in outside(); rc with exn -> outside (); raise exn *) + (*D*) in outside(); rc with exn -> outside (); raise exn in try fo_unif test_eq_only metasenv subst t1 t2 with UnificationFailure msg | Uncertain msg as exn -> @@ -450,7 +513,7 @@ and unify test_eq_only metasenv subst context t1 t2 = with | UnificationFailure _ -> raise (UnificationFailure msg) | Uncertain _ -> raise exn -(* (*D*) in outside(); rc with exn -> outside (); raise exn *) + (*D*) in outside(); rc with exn -> outside (); raise exn ;; let unify =