In order to prevent useless meta extensions, we optimize the unification of one

type and one unrefined term (currently happening only in the Lambda case).

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index 784ceeea88e7a2bc358ac2977ae72685495fdebb..423c33d8eea5f61f50140270165dee062d617b3d 100644 (file)
--- 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, _ =