X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicRefiner.ml;h=8476119ad081c24489559e5e2e566ea0318f13bb;hb=e62111335574a6ec78e5a4367a540e0529a00404;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..8476119ad 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,13 +408,31 @@ 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 
 =
+  let cs_subst = NCicSubstitution.subst ~avoid_beta_redexes:true in
+  try 
+    pp (lazy "WWW: trying coercions -- preliminary unification");
+    let metasenv, subst = 
+      NCicUnification.unify rdb metasenv subst context infty expty
+    in metasenv, subst, t, expty
+  with
+  | exn ->
   (* we try with a coercion *)
   let rec first exc = function
-  | [] ->         
+  | [] ->   
+      pp (lazy "WWW: no more coercions!");      
       raise (wrap_exc (lazy (localise orig_t, Printf.sprintf
         "The term\n%s\nhas type\n%s\nbut is here used with type\n%s"
         (NCicPp.ppterm ~metasenv ~subst ~context t)
@@ -441,7 +467,332 @@ and try_coercions rdb
       with 
       | NCicUnification.UnificationFailure _ -> first exc tl
       | NCicUnification.Uncertain _ as exc -> first exc tl
-  in 
+  in
+  
+  try 
+    pp (lazy "WWW: trying coercions -- inner check");
+    match infty, expty, t with
+    | _,_, NCic.Match (Ref.Ref (_,Ref.Ind (_,tyno,leftno)) as r,outty,m,pl) ->
+        (*{{{*) pp (lazy "CASE");
+        (* {{{ helper functions *)
+        let get_cl_and_left_p refit outty =
+          match refit with
+          | NReference.Ref (uri, NReference.Ind (_,tyno,leftno)) ->
+             let _, leftno, itl, _, _ = NCicEnvironment.get_checked_indtys r in
+             let _, _, ty, cl = List.nth itl tyno in
+             let constructorsno = List.length cl in
+              let count_pis t =
+                let rec aux ctx t = 
+                  match NCicReduction.whd ~subst ~delta:max_int ctx t with
+                  | NCic.Prod (name,src,tgt) ->
+                      let ctx = (name, (NCic.Decl src)) :: ctx in
+                      1 + aux ctx tgt
+                  | _ -> 0
+                in
+                  aux [] t
+              in
+              let rec skip_lambda_delifting t n =
+                match t,n with
+                | _,0 -> t
+                | NCic.Lambda (_,_,t),n ->
+                    pp (lazy ("WWW: failing term? "^ NCicPp.ppterm ~subst:[] ~metasenv:[] ~context:[] t)); 
+                    skip_lambda_delifting
+                      (* substitute dangling indices with a dummy *)
+                      (NCicSubstitution.subst (NCic.Sort NCic.Prop) t) (n - 1)
+                | _ -> assert false
+              in
+              let get_l_r_p n = function
+                | NCic.Lambda (_,NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_))),_) -> [],[]
+                | NCic.Lambda (_,NCic.Appl 
+                    (NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_))) :: args),_) ->
+                    HExtlib.split_nth n args
+                | _ -> assert false
+              in
+              let pis = count_pis ty in
+              let rno = pis - leftno in
+              let t = skip_lambda_delifting outty rno in
+              let left_p, _ = get_l_r_p leftno t in
+              let instantiate_with_left cl =
+                List.map 
+                  (fun ty -> 
+                    List.fold_left 
+                      (fun t p -> match t with
+                        | NCic.Prod (_,_,t) ->
+                            cs_subst p t
+                        | _-> assert false)
+                      ty left_p) 
+                  cl 
+              in
+              let cl = instantiate_with_left (List.map (fun (_,_,x) -> x) cl) in
+              cl, left_p, leftno, rno
+          | _ -> raise exn
+        in
+        let rec keep_lambdas_and_put_expty ctx t bo right_p matched n =
+          match t,n with
+          | _,0 ->
+            let rec mkr n = function 
+              | [] -> [] | _::tl -> NCic.Rel n :: mkr (n+1) tl
+            in
+            pp (lazy ("input replace: " ^ NCicPp.ppterm ~context:ctx ~metasenv:[] ~subst:[] bo));
+            let bo =
+            NCicRefineUtil.replace_lifting
+              ~equality:(fun _ -> NCicRefineUtil.alpha_equivalence)
+              ~context:ctx
+              ~what:(matched::right_p)
+              ~with_what:(NCic.Rel 1::List.rev (mkr 2 right_p))
+              ~where:bo
+            in
+            pp (lazy ("output replace: " ^ NCicPp.ppterm ~context:ctx ~metasenv:[] ~subst:[] bo));
+            bo
+          | NCic.Lambda (name, src, tgt),_ ->
+              NCic.Lambda (name, src,
+               keep_lambdas_and_put_expty 
+                ((name, NCic.Decl src)::ctx) tgt (NCicSubstitution.lift 1 bo)
+                (List.map (NCicSubstitution.lift 1) right_p) (NCicSubstitution.lift 1 matched) (n-1))
+          | _ -> assert false
+        in
+        (*let eq = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/equality/eq.ind(1,0,2)")) in
+        let eq_refl = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/equality/eq.con(0,1,2)")) in*)
+        let eq = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/jmeq/jmeq.ind(1,0,2)")) in
+        let eq_refl = NCic.Const (NReference.reference_of_string ("cic:/matita/ng/Plogic/jmeq/jmeq.con(0,1,2)")) in
+        let add_params 
+          metasenv subst context cty outty mty m i 
+        =
+          let rec aux context outty par j mty m = function
+            | NCic.Prod (name, src, tgt) ->
+                let t,k = 
+                  aux 
+                    ((name, NCic.Decl src) :: context)
+                    (NCicSubstitution.lift 1 outty) (NCic.Rel j::par) (j+1) 
+                    (NCicSubstitution.lift 1 mty) (NCicSubstitution.lift 1 m) tgt
+                in
+                NCic.Prod (name, src, t), k
+            | NCic.Const (Ref.Ref (_,Ref.Ind (_,_,leftno)) as r) ->
+                let k = 
+                  let k = NCic.Const(Ref.mk_constructor i r) in
+                  NCicUntrusted.mk_appl k par
+                in
+                (* the type has no parameters, so kty = mty
+                let kty = 
+                  try NCicTypechecker.typeof ~subst ~metasenv context k
+                  with NCicTypeChecker.TypeCheckerFailure _ -> assert false
+                in *)
+                NCic.Prod ("p", 
+                 NCic.Appl [eq; mty; m; mty; k],
+                 (NCicSubstitution.lift 1
+                  (NCicReduction.head_beta_reduce ~delta:max_int 
+                   (NCicUntrusted.mk_appl outty [k])))),[mty,m,mty,k]
+            | NCic.Appl (NCic.Const (Ref.Ref (_,Ref.Ind (_,_,leftno)) as r)::pl) ->
+                let left_p,right_p = HExtlib.split_nth leftno pl in
+                let has_rights = right_p <> [] in
+                let k = 
+                  let k = NCic.Const(Ref.mk_constructor i r) in
+                  NCicUntrusted.mk_appl k (left_p@par)
+                in
+                let right_p = 
+                  try match 
+                    NCicTypeChecker.typeof ~subst ~metasenv context k
+                  with
+                  | NCic.Appl (NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_)))::args) ->
+                      snd (HExtlib.split_nth leftno args)
+                  | _ -> assert false
+                  with NCicTypeChecker.TypeCheckerFailure _-> assert false
+                in
+                let orig_right_p =
+                  match mty with
+                  | NCic.Appl (NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_)))::args) ->
+                      snd (HExtlib.split_nth leftno args)
+                  | _ -> assert false
+                in
+                List.fold_right2 
+                  (fun x y (tacc,pacc) ->
+                    let xty = 
+          	    try NCicTypeChecker.typeof ~subst ~metasenv context x
+                      with NCicTypeChecker.TypeCheckerFailure _ -> assert false
+                    in
+                    let yty = 
+          	    try NCicTypeChecker.typeof ~subst ~metasenv context y
+                      with NCicTypeChecker.TypeCheckerFailure _ -> assert false
+                    in
+                    NCic.Prod ("_", NCic.Appl [eq;xty;x;yty;y],
+                     NCicSubstitution.lift 1 tacc), (xty,x,yty,y)::pacc) 
+                  (orig_right_p @ [m]) (right_p @ [k]) 
+                  (NCicReduction.head_beta_reduce ~delta:max_int
+                      (NCicUntrusted.mk_appl outty (right_p@[k])), [])  
+
+  (*              if has_rights then
+                  NCicReduction.head_beta_reduce ~delta:max_int
+                    (NCic.Appl (outty ::right_p @ [k])),k
+                else
+                  NCic.Prod ("p", 
+                   NCic.Appl [eq; mty; m; k],
+                   (NCicSubstitution.lift 1
+                    (NCicReduction.head_beta_reduce ~delta:max_int 
+                     (NCic.Appl (outty ::right_p @ [k]))))),k*)
+            | _ -> assert false
+          in
+            aux context outty [] 1 mty m cty
+        in
+        let add_lambda_for_refl_m pbo eqs cty =
+          (* k lives in the right context *)
+          (* if rno <> 0 then pbo else *)
+          let rec aux = function 
+            | NCic.Lambda (name,src,bo), NCic.Prod (_,_,ty) ->
+                NCic.Lambda (name,src,
+                (aux (bo,ty)))
+            | t,_ -> snd (List.fold_right
+                (fun (xty,x,yty,y) (n,acc) -> n+1, NCic.Lambda ("p" ^ string_of_int n,
+                  NCic.Appl [eq; xty; x; yty; y],
+                  NCicSubstitution.lift 1 acc)) eqs (1,t))
+                (*NCic.Lambda ("p",
+                  NCic.Appl [eq; mty; m; k],NCicSubstitution.lift 1 t)*)
+          in
+          aux (pbo,cty)
+        in
+        let add_pi_for_refl_m context new_outty mty m lno rno =
+          (*if rno <> 0 then new_outty else*)
+            let rec aux context mty m = function
+              | NCic.Lambda (name, src, tgt) ->
+                  let context = (name, NCic.Decl src)::context in
+                  NCic.Lambda (name, src, aux context (NCicSubstitution.lift 1 mty) (NCicSubstitution.lift 1 m) tgt)
+              | t -> 
+                  let lhs =
+                    match mty with
+                    | NCic.Appl (_::params) -> (snd (HExtlib.split_nth lno params))@[m]
+                    | _ -> [m]
+                  in
+                  let rhs = 
+                    List.map (fun x -> NCic.Rel x) 
+                      (List.rev (HExtlib.list_seq 1 (rno+2))) in
+                  List.fold_right2
+                    (fun x y acc ->
+                      let xty = 
+    		    try NCicTypeChecker.typeof ~subst ~metasenv context x
+                        with NCicTypeChecker.TypeCheckerFailure _ -> assert false
+                      in
+                      let yty = 
+    		    try NCicTypeChecker.typeof ~subst ~metasenv context y
+                        with NCicTypeChecker.TypeCheckerFailure _ -> assert false
+                      in
+                      NCic.Prod
+                      ("_", NCic.Appl [eq;xty;x;yty;y],
+                       (NCicSubstitution.lift 1 acc)))
+                    lhs rhs t
+  (*                NCic.Prod 
+                    ("_", NCic.Appl [eq;mty;m;NCic.Rel 1],
+                    NCicSubstitution.lift 1 t)*)
+            in
+              aux context mty m new_outty
+        in (* }}} end helper functions *)
+        (* constructors types with left params already instantiated *)
+        let outty = NCicUntrusted.apply_subst subst context outty in
+        let cl, left_p, leftno,rno = 
+          get_cl_and_left_p r outty
+        in
+        let right_p, mty = 
+          try
+            match 
+              NCicTypeChecker.typeof ~subst ~metasenv context m
+            with
+            | (NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_))) | NCic.Meta _) as mty -> [], mty
+            | NCic.Appl ((NCic.Const (Ref.Ref (_,Ref.Ind (_,_,_)))|NCic.Meta _)::args) as mty ->
+                snd (HExtlib.split_nth leftno args), mty
+            | _ -> assert false
+          with NCicTypeChecker.TypeCheckerFailure _ -> 
+             raise (AssertFailure(lazy "already ill-typed matched term"))
+        in
+        let mty = NCicUntrusted.apply_subst subst context mty in
+        let outty = NCicUntrusted.apply_subst subst context outty in
+        let expty = NCicUntrusted.apply_subst subst context expty in
+        let new_outty =
+         keep_lambdas_and_put_expty context outty expty right_p m (rno+1)
+        in
+        pp 
+          (lazy ("CASE: new_outty: " ^ NCicPp.ppterm 
+           ~context ~metasenv ~subst new_outty));
+        let _,pl,subst,metasenv = 
+          List.fold_right2
+            (fun cty pbo (i, acc, s, menv) -> 
+               pp (lazy ("begin iteration"));
+              (* Pi k_par, (Pi H:m=(K_i left_par k_par)), 
+               *   (new_)outty right_par (K_i left_par k_par) *)
+               let infty_pbo, _ = 
+                 add_params menv s context cty outty mty m i in
+               pp 
+                (lazy ("CASE: infty_pbo: "^ NCicPp.ppterm
+                 ~context ~metasenv ~subst infty_pbo));
+               let expty_pbo, eqs = (* k is (K_i left_par k_par) *)
+                 add_params menv s context cty new_outty mty m i in
+               pp 
+                (lazy ("CASE: expty_pbo: "^ NCicPp.ppterm
+                 ~context ~metasenv ~subst expty_pbo));
+               let pbo = add_lambda_for_refl_m pbo eqs cty in
+               pp 
+                 (lazy ("CASE: pbo: " ^ NCicPp.ppterm
+                 ~context ~metasenv ~subst pbo));
+               let metasenv, subst, pbo, _ =
+                 try_coercions rdb ~localise menv s context pbo 
+          	 orig_t (*??*) infty_pbo expty_pbo perform_unification exc
+               in
+               pp 
+                 (lazy ("CASE: pbo2: " ^ NCicPp.ppterm 
+                 ~context ~metasenv ~subst pbo));
+               (i-1, pbo::acc, subst, metasenv))
+            cl pl (List.length pl, [], subst, metasenv)
+        in
+        (*let metasenv, subst = 
+          try 
+            NCicUnification.unify rdb metasenv subst context outty new_outty 
+          with _ -> raise (RefineFailure (lazy (localise orig_t, "try_coercions")))
+        in*)
+        let new_outty = add_pi_for_refl_m context new_outty mty m leftno rno in
+        pp (lazy ("CASE: new_outty: " ^ (NCicPp.ppterm 
+           ~metasenv ~subst ~context new_outty)));
+        let right_tys = 
+          List.map 
+            (fun t -> NCicTypeChecker.typeof ~subst ~metasenv context t) right_p in
+        let eqs = 
+          List.map2 (fun x y -> NCic.Appl[eq_refl;x;y]) (right_tys@[mty]) 
+            (right_p@[m]) in
+        let t = NCic.Appl (NCic.Match(r,new_outty,m,pl) :: eqs) 
+        in
+        metasenv, subst, t, expty (*}}}*)
+    | NCic.Prod (nameprod, src, ty),NCic.Prod (_, src2, ty2), _ -> 
+        let rec mk_fresh_name ctx firstch n =
+          let candidate = (String.make 1 firstch) ^ (string_of_int n) in
+          if (List.for_all (fun (s,_) -> s <> candidate) ctx) then candidate
+          else mk_fresh_name ctx firstch (n+1)
+        in
+        (*{{{*) pp (lazy "LAM");
+        pp (lazy ("LAM: t = " ^ NCicPp.ppterm ~metasenv ~subst ~context t));
+        let name_con = mk_fresh_name context 'c' 0
+          (*FreshNamesGenerator.mk_fresh_name 
+            ~subst metasenv context ~typ:src2 Cic.Anonymous*)
+        in
+        let context_src2 = ((name_con, NCic.Decl src2) :: context) in
+        (* contravariant part: the argument of f:src->ty *)
+        let metasenv, subst, rel1, _ = 
+          try_coercions rdb ~localise metasenv subst context_src2
+           (NCic.Rel 1) orig_t (NCicSubstitution.lift 1 src2) 
+           (NCicSubstitution.lift 1 src) perform_unification exc
+        in
+        (* covariant part: the result of f(c x); x:src2; (c x):src *)
+        let name_t, bo = 
+          match t with
+          | NCic.Lambda (n,_,bo) -> n, cs_subst rel1 (NCicSubstitution.lift_from 2 1 bo)
+          | _ -> name_con, NCicUntrusted.mk_appl (NCicSubstitution.lift 1 t) [rel1]
+        in
+        (* we fix the possible dependency problem in the source ty *)
+        let ty = cs_subst rel1 (NCicSubstitution.lift_from 2 1 ty) in
+        let metasenv, subst, bo, _ = 
+          try_coercions rdb ~localise metasenv subst context_src2
+            bo orig_t ty ty2 perform_unification exc
+        in
+        let coerced = NCic.Lambda (name_t,src2, bo) in
+        pp (lazy ("LAM: coerced = " ^ NCicPp.ppterm ~metasenv ~subst ~context coerced));
+        metasenv, subst, coerced, expty (*}}}*)
+    | _ -> raise exc
+  with exc2 ->    
   pp(lazy("try_coercion " ^ 
     NCicPp.ppterm ~metasenv ~subst ~context infty ^ " |---> " ^
     NCicPp.ppterm ~metasenv ~subst ~context expty));
@@ -450,29 +801,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 +1007,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 +1027,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 +1064,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 +1080,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