X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=423c33d8eea5f61f50140270165dee062d617b3d;hb=0920a5755553774f5b41d7603318ea997ecbdca5;hp=fdb9c2137332b3c5196b3b10349f1a046b983723;hpb=0bcc03be833e8f177850e6b9785713d7975ee8bd;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index fdb9c2137..423c33d8e 100644
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -236,23 +236,34 @@ let rec typeof rdb
              | C.Prod (_,s,t) -> Some s, Some t, false
              | _ -> None, None, true 
        in
-       let metasenv, subst, s, ty_s = 
-         typeof_aux metasenv subst context None s in
-       let metasenv, subst, s, _ = 
-         force_to_sort rdb 
-           metasenv subst context s orig_s localise ty_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 = 
@@ -263,12 +274,9 @@ 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) ->
-       let metasenv, subst, ty, ty_ty = 
-         typeof_aux metasenv subst context None ty in
-       let metasenv, subst, ty, _ = 
-         force_to_sort rdb
-           metasenv subst context ty orig_ty localise ty_ty in
+    | C.LetIn (n,ty,t,bo) ->
+       let metasenv, subst, ty = 
+         check_type rdb ~localise metasenv subst context ty in
        let metasenv, subst, t, _ = 
          typeof_aux metasenv subst context (Some ty) t in
        let context1 = (n, C.Def (t,ty)) :: context in
@@ -400,6 +408,15 @@ let rec typeof rdb
   in
     typeof_aux metasenv subst context expty term
 
+and check_type rdb ~localise metasenv subst context (ty as orig_ty) =
+  let metasenv, subst, ty, sort = 
+    typeof rdb ~localise metasenv subst context ty None
+  in
+  let metasenv, subst, ty, _ = 
+    force_to_sort rdb metasenv subst context ty orig_ty localise sort
+  in
+    metasenv, subst, ty
+
 and try_coercions rdb 
   ~localise 
   metasenv subst context t orig_t infty expty perform_unification exc 
@@ -450,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) 
@@ -664,18 +673,10 @@ let undebruijnate inductive ref t rev_fl =
 let typeof_obj 
   rdb ?(localise=fun _ -> Stdpp.dummy_loc) (uri,height,metasenv,subst,obj)
 = 
-  let check_type metasenv subst context (ty as orig_ty) =  (* XXX fattorizza *)
-    let metasenv, subst, ty, sort = 
-      typeof rdb ~localise metasenv subst context ty None
-    in
-    let metasenv, subst, ty, sort = 
-      force_to_sort rdb metasenv subst context ty orig_ty localise sort
-    in
-      metasenv, subst, ty, sort
-  in
   match obj with 
-  | C.Constant (relevance, name, bo, ty , attr) ->
-       let metasenv, subst, ty, _ = check_type metasenv subst [] ty in
+  | C.Constant (relevance, name, bo, ty, attr) ->
+       let metasenv, subst, ty = 
+         check_type rdb ~localise metasenv subst [] ty in
        let metasenv, subst, bo, ty, height = 
          match bo with
          | Some bo ->
@@ -692,7 +693,8 @@ let typeof_obj
       let types, metasenv, subst, rev_fl =
         List.fold_left
          (fun (types, metasenv, subst, fl) (relevance,name,k,ty,bo) ->
-           let metasenv, subst, ty, _ = check_type metasenv subst [] ty in
+           let metasenv, subst, ty = 
+             check_type rdb ~localise metasenv subst [] ty in
            let dbo = NCicTypeChecker.debruijn uri len [] ~subst bo in
            let localise = relocalise localise dbo bo in
             (name,C.Decl ty)::types,
@@ -728,7 +730,8 @@ let typeof_obj
      let metasenv,subst,rev_itl,tys =
       List.fold_left
        (fun (metasenv,subst,res,ctx) (relevance,n,ty,cl) ->
-          let metasenv, subst, ty, _ = check_type metasenv subst [] ty in
+          let metasenv, subst, ty = 
+            check_type rdb ~localise metasenv subst [] ty in
           metasenv,subst,(relevance,n,ty,cl)::res,(n,NCic.Decl ty)::ctx
        ) (metasenv,subst,[],[]) itl in
      let metasenv,subst,itl,_ =
@@ -743,7 +746,8 @@ let typeof_obj
               try snd (HExtlib.split_nth leftno k_relev)
               with Failure _ -> k_relev in
              let te = NCicTypeChecker.debruijn uri len [] ~subst te in
-             let metasenv, subst, te, _ = check_type metasenv subst tys te in
+             let metasenv, subst, te = 
+               check_type rdb ~localise metasenv subst tys te in
              let context,te = NCicReduction.split_prods ~subst tys leftno te in
              let _,chopped_context_rev =
               HExtlib.split_nth (List.length tys) (List.rev context) in