From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Wed, 18 Nov 2009 14:03:54 +0000 (+0000)
Subject: Code factorization for check_type.
X-Git-Tag: make_still_working~3204
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=11e1e0a1396377e3944827474444e43db0d9fbfc;p=helm.git

Code factorization for check_type.
---

diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml
index d75fd6ab0..415afdc1d 100644
--- a/helm/software/components/ng_refiner/nCicRefiner.ml
+++ b/helm/software/components/ng_refiner/nCicRefiner.ml
@@ -236,11 +236,8 @@ 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, s = 
+         check_type rdb ~localise metasenv subst context s in
        let (metasenv,subst), exp_ty_t = 
          match exp_s with 
          | Some exp_s -> 
@@ -264,11 +261,8 @@ let rec typeof rdb
        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
+       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 +394,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 
@@ -664,18 +667,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 +687,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 +724,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 +740,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