X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=423c33d8eea5f61f50140270165dee062d617b3d;hb=bca340f9c590e6530f8346fddd61c9fa0ae7f411;hp=415afdc1de2773129b8f9156758e6ab2cf6031fa;hpb=11e1e0a1396377e3944827474444e43db0d9fbfc;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 415afdc1d..423c33d8e 100644
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -236,20 +236,34 @@ let rec typeof rdb
              | C.Prod (_,s,t) -> Some s, Some t, false
              | _ -> None, None, true 
        in
-       let metasenv, subst, s = 
-         check_type rdb ~localise metasenv subst context s in
-       let (metasenv,subst), exp_ty_t = 
+       let (metasenv,subst), s = 
          match exp_s with 
-         | Some exp_s -> 
-             (try 
-               pp(lazy("Force source to: "^NCicPp.ppterm ~metasenv ~subst
-                  ~context exp_s));
-               NCicUnification.unify ~test_eq_only:true rdb metasenv subst context s exp_s,exp_ty_t
-             with exc -> raise (wrap_exc (lazy (localise orig_s, Printf.sprintf
-               "Source type %s was expected to be %s" (NCicPp.ppterm ~metasenv
-               ~subst ~context s) (NCicPp.ppterm ~metasenv ~subst ~context
-               exp_s))) exc))
-         | None -> (metasenv, subst), None
+         | Some exp_s ->
+             (* optimized case: implicit and implicitly typed meta
+              * the optimization prevents proliferation of metas  *)
+             (match s with
+              | C.Implicit _ -> (metasenv,subst),exp_s
+              | _ ->
+                  let metasenv, subst, s = match s with 
+                    | C.Meta (n,_) 
+                        when (try (match NCicUtils.lookup_meta n metasenv with
+                              | _,_,C.Implicit (`Typeof _) -> true
+                              | _ -> false)
+                        with 
+                          | _ -> false) -> metasenv, subst, s
+                    | _ ->  check_type rdb ~localise metasenv subst context s in
+                  (try 
+                    pp(lazy("Force source to: "^NCicPp.ppterm ~metasenv ~subst
+                       ~context exp_s));
+                    NCicUnification.unify ~test_eq_only:true rdb metasenv subst context s exp_s,s
+                  with exc -> raise (wrap_exc (lazy (localise orig_s, Printf.sprintf
+                    "Source type %s was expected to be %s" (NCicPp.ppterm ~metasenv
+                    ~subst ~context s) (NCicPp.ppterm ~metasenv ~subst ~context
+                    exp_s))) exc)))
+         | None -> 
+             let metasenv, subst, s = 
+               check_type rdb ~localise metasenv subst context s in
+             (metasenv, subst), s
        in
        let context_for_t = (n,C.Decl s) :: context in
        let metasenv, subst, t, ty_t = 
@@ -260,7 +274,7 @@ let rec typeof rdb
            (C.Lambda(n,s,t)) (C.Prod (n,s,ty_t)) expty
        else 
          metasenv, subst, C.Lambda(n,s,t), C.Prod (n,s,ty_t)
-    | C.LetIn (n,(ty as orig_ty),t,bo) ->
+    | C.LetIn (n,ty,t,bo) ->
        let metasenv, subst, ty = 
          check_type rdb ~localise metasenv subst context ty in
        let metasenv, subst, t, _ = 
@@ -453,29 +467,21 @@ and try_coercions rdb
         rdb metasenv subst context infty expty)
 
 and force_to_sort rdb metasenv subst context t orig_t localise ty =
-  match NCicReduction.whd ~subst context ty with
-  | C.Meta (_,(0,(C.Irl 0 | C.Ctx []))) as ty -> 
-     metasenv, subst, t, ty
-  | C.Meta (_i,(_,(C.Irl 0 | C.Ctx []))) -> assert false (*CSC: ???
-     metasenv, subst, t, C.Meta(i,(0,C.Irl 0)) *)
-  | C.Meta (i,(_,lc)) ->
-     let len = match lc with C.Irl len->len | C.Ctx l->List.length l in
-     let metasenv, subst, newmeta, _ = 
-       if len > 0 then
-         NCicMetaSubst.restrict metasenv subst i (HExtlib.list_seq 1 (len+1))
-       else metasenv, subst, i, []
-     in
-     metasenv, subst, t, C.Meta (newmeta,(0,C.Irl 0))
-  | C.Sort _ as ty -> metasenv, subst, t, ty 
-  | ty -> 
-      try_coercions rdb ~localise metasenv subst context
-        t orig_t ty (NCic.Sort (NCic.Type 
-          (match NCicEnvironment.get_universes () with
-           | x::_ -> x 
-           | _ -> assert false))) false 
-         (Uncertain (lazy (localise orig_t, 
-         "The type of " ^ NCicPp.ppterm ~metasenv ~subst ~context t
-         ^ " is not a sort: " ^ NCicPp.ppterm ~metasenv ~subst ~context ty)))
+  try 
+    let metasenv, subst, ty = 
+      NCicUnification.sortfy (Failure "sortfy") metasenv subst context ty in
+      metasenv, subst, t, ty
+  with
+      Failure _ -> 
+        let ty = NCicReduction.whd ~subst context ty in
+          try_coercions rdb ~localise metasenv subst context
+            t orig_t ty (NCic.Sort (NCic.Type 
+              (match NCicEnvironment.get_universes () with
+               | x::_ -> x 
+               | _ -> assert false))) false 
+             (Uncertain (lazy (localise orig_t, 
+             "The type of " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^
+             " is not a sort: " ^ NCicPp.ppterm ~metasenv ~subst ~context ty)))
 
 and sort_of_prod 
   localise metasenv subst context orig_s orig_t (name,s) t (t1, t2)