X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=d3c86d2816c2c9bd050bbe1b336d033d95e4c8dd;hb=1ee5193677b8e2a80d4f068ee79ecac335de1196;hp=24ab7b4afbf1129cafb2d0462a169bf26ca42913;hpb=c45a4837a6f3c9d6af14b2057389442bf6d2f32f;p=helm.git diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 24ab7b4af..d3c86d281 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -72,13 +72,23 @@ let indent = ref "";; let inside c = indent := !indent ^ String.make 1 c;; let outside () = indent := String.sub !indent 0 (String.length !indent -1);; -(* let pp s = prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s) ;; -*) -let pp _ = ();; +(* let pp _ = ();; *) + +let fix_sorts metasenv subst context meta t = + let rec aux () = function + | NCic.Sort (NCic.Type u) as orig -> + (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)) + | 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' = @@ -142,28 +152,44 @@ 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 fix_sorts t = + if swap then fix_sorts metasenv subst context (NCic.Meta (n,lc)) t + else + NCic.Sort (NCic.Type ( + match NCicEnvironment.sup NCicEnvironment.type0 with Some x ->x| _ -> + assert false)) + 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 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 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 msg -> + prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context ft); + prerr_endline (Lazy.force msg); + assert false 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)); - 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 @@ -187,16 +213,14 @@ and instantiate test_eq_only metasenv subst context n lc t swap = 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 @@ -380,7 +404,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)) @@ -411,7 +435,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) ^ @@ -446,7 +470,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 -> @@ -456,7 +480,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 =