X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=202e68e4c86c3d056a8914451a70b6c4b25aae13;hb=e1ffde2ba67b8a2f7d4d97898ba28afd65d96ea7;hp=10bc29a62d2ca398aa9b092859fea079b1d6f5db;hpb=023b925489d007fc1a39087e2770aac4b2740159;p=helm.git diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 10bc29a62..202e68e4c 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -80,6 +80,24 @@ 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 -> 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,28 +160,40 @@ 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 = 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 name, ctx, ty = NCicUtils.lookup_meta n metasenv in - let metasenv, subst = + let metasenv, subst, t = match ty with - | NCic.Implicit (`Typeof _) -> metasenv, subst + | NCic.Implicit (`Typeof _) -> + metasenv,subst,fix_sorts swap metasenv subst context (NCic.Meta(n,lc)) t | _ -> - let lty = NCicSubstitution.subst_meta lc ty 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 + pp (lazy ("typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t)); + let t, ty_t = + try t, NCicTypeChecker.typeof ~subst ~metasenv context t + with NCicTypeChecker.TypeCheckerFailure _ -> + let ft = + fix_sorts swap metasenv subst context (NCic.Meta (n,lc)) t + in + if ft == t then assert false + else + try + pp (lazy ("typeof: " ^ + NCicPp.ppterm ~metasenv ~subst ~context ft)); + ft, NCicTypeChecker.typeof ~subst ~metasenv context ft + with NCicTypeChecker.TypeCheckerFailure _ -> + 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)); - unify test_eq_only metasenv subst context lty ty_t + let metasenv,subst= unify test_eq_only metasenv subst context lty ty_t in + metasenv, subst, t in let (metasenv, subst), t = try NCicMetaSubst.delift metasenv subst context n lc t @@ -174,6 +204,7 @@ and instantiate test_eq_only metasenv subst context n lc t swap = 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 _ -> @@ -181,21 +212,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 @@ -379,7 +408,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)) @@ -410,7 +439,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) ^ @@ -445,7 +474,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 -> @@ -455,7 +484,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 =