helm/ocaml/cic_proof_checking/cicTypeChecker.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (* TODO factorize functions to frequent errors (e.g. "Unknwon mutual inductive
  27  * ...") *)
  28
  29 open Printf
  30
  31 exception AssertFailure of string;;
  32 exception TypeCheckerFailure of string;;
  33
  34 let profiler_clean_fill =
  35   (CicUtil.profile "add_obj.typecheck_obj.clean_and_fill").CicUtil.profile
  36
  37 let fdebug = ref 0;;
  38 let debug t context =
  39  let rec debug_aux t i =
  40   let module C = Cic in
  41   let module U = UriManager in
  42    CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
  43  in
  44   if !fdebug = 0 then
  45    raise (TypeCheckerFailure (List.fold_right debug_aux (t::context) ""))
  46 ;;
  47
  48 let debug_print = fun _ -> () ;;
  49
  50 let rec split l n =
  51  match (l,n) with
  52     (l,0) -> ([], l)
  53   | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
  54   | (_,_) ->
  55       raise (TypeCheckerFailure "Parameters number < left parameters number")
  56 ;;
  57
  58 let debrujin_constructor uri number_of_types =
  59  let rec aux k =
  60   let module C = Cic in
  61    function
  62       C.Rel n as t when n <= k -> t
  63     | C.Rel _ ->
  64         raise (TypeCheckerFailure "unbound variable found in constructor type")
  65     | C.Var (uri,exp_named_subst) ->
  66        let exp_named_subst' =
  67         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
  68        in
  69         C.Var (uri,exp_named_subst')
  70     | C.Meta (i,l) ->
  71        let l' = List.map (function None -> None | Some t -> Some (aux k t)) l in
  72         C.Meta (i,l)
  73     | C.Sort _
  74     | C.Implicit _ as t -> t
  75     | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
  76     | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k+1) t)
  77     | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k+1) t)
  78     | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k+1) t)
  79     | C.Appl l -> C.Appl (List.map (aux k) l)
  80     | C.Const (uri,exp_named_subst) ->
  81        let exp_named_subst' =
  82         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
  83        in
  84         C.Const (uri,exp_named_subst')
  85     | C.MutInd (uri',tyno,exp_named_subst) when UriManager.eq uri uri' ->
  86        if exp_named_subst != [] then
  87         raise (TypeCheckerFailure
  88           ("non-empty explicit named substitution is applied to "^
  89            "a mutual inductive type which is being defined")) ;
  90        C.Rel (k + number_of_types - tyno) ;
  91     | C.MutInd (uri',tyno,exp_named_subst) ->
  92        let exp_named_subst' =
  93         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
  94        in
  95         C.MutInd (uri',tyno,exp_named_subst')
  96     | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
  97        let exp_named_subst' =
  98         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
  99        in
 100         C.MutConstruct (uri,tyno,consno,exp_named_subst')
 101     | C.MutCase (sp,i,outty,t,pl) ->
 102        C.MutCase (sp, i, aux k outty, aux k t,
 103         List.map (aux k) pl)
 104     | C.Fix (i, fl) ->
 105        let len = List.length fl in
 106        let liftedfl =
 107         List.map
 108          (fun (name, i, ty, bo) -> (name, i, aux k ty, aux (k+len) bo))
 109           fl
 110        in
 111         C.Fix (i, liftedfl)
 112     | C.CoFix (i, fl) ->
 113        let len = List.length fl in
 114        let liftedfl =
 115         List.map
 116          (fun (name, ty, bo) -> (name, aux k ty, aux (k+len) bo))
 117           fl
 118        in
 119         C.CoFix (i, liftedfl)
 120  in
 121   aux 0
 122 ;;
 123
 124 exception CicEnvironmentError;;
 125
 126 let rec type_of_constant ~logger uri ugraph =
 127  let module C = Cic in
 128  let module R = CicReduction in
 129  let module U = UriManager in
 130  let cobj,ugraph =
 131    match CicEnvironment.is_type_checked ~trust:true ugraph uri with
 132       CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
 133     | CicEnvironment.UncheckedObj uobj ->
 134        logger#log (`Start_type_checking uri) ;
 135        (* let's typecheck the uncooked obj *)
 136
 137 (****************************************************************
 138   TASSI: FIXME qui e' inutile ricordarselo,
 139   tanto poi lo richiediamo alla cache che da quello su disco
 140 *****************************************************************)
 141
 142        let ugraph_dust =
 143          (match uobj with
 144            C.Constant (_,Some te,ty,_,_) ->
 145            let _,ugraph = type_of ~logger ty ugraph in
 146            let type_of_te,ugraph' = type_of ~logger te ugraph in
 147               let b',ugraph'' = (R.are_convertible [] type_of_te ty ugraph') in
 148               if not b' then
 149                raise (TypeCheckerFailure (sprintf
 150                 "the constant %s is not well typed because the type %s of the body is not convertible to the declared type %s"
 151                 (U.string_of_uri uri) (CicPp.ppterm type_of_te)
 152                 (CicPp.ppterm ty)))
 153               else
 154                 ugraph'
 155          | C.Constant (_,None,ty,_,_) ->
 156            (* only to check that ty is well-typed *)
 157            let _,ugraph' = type_of ~logger ty ugraph in
 158            ugraph'
 159          | C.CurrentProof (_,conjs,te,ty,_,_) ->
 160              let _,ugraph1 =
 161               List.fold_left
 162                (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
 163                  let _,ugraph' =
 164                    type_of_aux' ~logger metasenv context ty ugraph
 165                  in
 166                  (metasenv @ [conj],ugraph')
 167                ) ([],ugraph) conjs
 168              in
 169               let _,ugraph2 = type_of_aux' ~logger conjs [] ty ugraph1 in
 170                let type_of_te,ugraph3 =
 171                  type_of_aux' ~logger conjs [] te ugraph2
 172                in
 173                let b,ugraph4 = (R.are_convertible [] type_of_te ty ugraph3) in
 174                if not b then
 175                  raise (TypeCheckerFailure (sprintf
 176                   "the current proof %s is not well typed because the type %s of the body is not convertible to the declared type %s"
 177                   (U.string_of_uri uri) (CicPp.ppterm type_of_te)
 178                   (CicPp.ppterm ty)))
 179                else
 180                  ugraph4
 181          | _ ->
 182              raise (TypeCheckerFailure
 183                       ("Unknown constant:" ^ U.string_of_uri uri)))
 184        in
 185          try
 186            CicEnvironment.set_type_checking_info uri;
 187            logger#log (`Type_checking_completed uri) ;
 188            match CicEnvironment.is_type_checked ~trust:false ugraph uri with
 189                CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
 190              | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
 191          with Invalid_argument s ->
 192            (*debug_print (lazy s);*)
 193            uobj,ugraph_dust
 194   in
 195    match cobj,ugraph with
 196       (C.Constant (_,_,ty,_,_)),g -> ty,g
 197     | (C.CurrentProof (_,_,_,ty,_,_)),g -> ty,g
 198     | _ ->
 199         raise (TypeCheckerFailure ("Unknown constant:" ^ U.string_of_uri uri))
 200
 201 and type_of_variable ~logger uri ugraph =
 202  let module C = Cic in
 203  let module R = CicReduction in
 204  let module U = UriManager in
 205   (* 0 because a variable is never cooked => no partial cooking at one level *)
 206   match CicEnvironment.is_type_checked ~trust:true ugraph uri with
 207      CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') -> ty,ugraph'
 208    | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_,_)) ->
 209       logger#log (`Start_type_checking uri) ;
 210       (* only to check that ty is well-typed *)
 211       let _,ugraph1 = type_of ~logger ty ugraph in
 212       let ugraph2 =
 213        (match bo with
 214            None -> ugraph
 215          | Some bo ->
 216              let ty_bo,ugraph' = type_of ~logger bo ugraph1 in
 217              let b,ugraph'' = (R.are_convertible [] ty_bo ty ugraph') in
 218              if not b then
 219               raise (TypeCheckerFailure
 220                 ("Unknown variable:" ^ U.string_of_uri uri))
 221              else
 222                ugraph'')
 223       in
 224         (try
 225            CicEnvironment.set_type_checking_info uri ;
 226            logger#log (`Type_checking_completed uri) ;
 227            match CicEnvironment.is_type_checked ~trust:false ugraph uri with
 228                CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') ->
 229                  ty,ugraph'
 230              | CicEnvironment.CheckedObj _
 231              | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
 232          with Invalid_argument s ->
 233            (*debug_print (lazy s);*)
 234            ty,ugraph2)
 235    |  _ ->
 236         raise (TypeCheckerFailure ("Unknown variable:" ^ U.string_of_uri uri))
 237
 238 and does_not_occur context n nn te =
 239  let module C = Cic in
 240    (*CSC: whd sembra essere superflua perche' un caso in cui l'occorrenza *)
 241    (*CSC: venga mangiata durante la whd sembra presentare problemi di *)
 242    (*CSC: universi                                                    *)
 243    match CicReduction.whd context te with
 244       C.Rel m when m > n && m <= nn -> false
 245     | C.Rel _
 246     | C.Meta _  (* CSC: Are we sure? No recursion?*)
 247     | C.Sort _
 248     | C.Implicit _ -> true
 249     | C.Cast (te,ty) ->
 250        does_not_occur context n nn te && does_not_occur context n nn ty
 251     | C.Prod (name,so,dest) ->
 252        does_not_occur context n nn so &&
 253         does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
 254          dest
 255     | C.Lambda (name,so,dest) ->
 256        does_not_occur context n nn so &&
 257         does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
 258          dest
 259     | C.LetIn (name,so,dest) ->
 260        does_not_occur context n nn so &&
 261         does_not_occur ((Some (name,(C.Def (so,None))))::context)
 262          (n + 1) (nn + 1) dest
 263     | C.Appl l ->
 264        List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
 265     | C.Var (_,exp_named_subst)
 266     | C.Const (_,exp_named_subst)
 267     | C.MutInd (_,_,exp_named_subst)
 268     | C.MutConstruct (_,_,_,exp_named_subst) ->
 269        List.fold_right (fun (_,x) i -> i && does_not_occur context n nn x)
 270         exp_named_subst true
 271     | C.MutCase (_,_,out,te,pl) ->
 272        does_not_occur context n nn out && does_not_occur context n nn te &&
 273         List.fold_right (fun x i -> i && does_not_occur context n nn x) pl true
 274     | C.Fix (_,fl) ->
 275        let len = List.length fl in
 276         let n_plus_len = n + len in
 277         let nn_plus_len = nn + len in
 278         let tys =
 279          List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
 280         in
 281          List.fold_right
 282           (fun (_,_,ty,bo) i ->
 283             i && does_not_occur context n nn ty &&
 284             does_not_occur (tys @ context) n_plus_len nn_plus_len bo
 285           ) fl true
 286     | C.CoFix (_,fl) ->
 287        let len = List.length fl in
 288         let n_plus_len = n + len in
 289         let nn_plus_len = nn + len in
 290         let tys =
 291          List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
 292         in
 293          List.fold_right
 294           (fun (_,ty,bo) i ->
 295             i && does_not_occur context n nn ty &&
 296             does_not_occur (tys @ context) n_plus_len nn_plus_len bo
 297           ) fl true
 298
 299 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
 300 (*CSC questa funzione e' simile alla are_all_occurrences_positive, ma fa *)
 301 (*CSC dei controlli leggermente diversi. Viene invocata solamente dalla  *)
 302 (*CSC strictly_positive                                                  *)
 303 (*CSC definizione (giusta???) tratta dalla mail di Hugo ;-)              *)
 304 and weakly_positive context n nn uri te =
 305  let module C = Cic in
 306 (*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*)
 307   let dummy_mutind =
 308    C.MutInd (HelmLibraryObjects.Datatypes.nat_URI,0,[])
 309   in
 310   (*CSC mettere in cicSubstitution *)
 311   let rec subst_inductive_type_with_dummy_mutind =
 312    function
 313       C.MutInd (uri',0,_) when UriManager.eq uri' uri ->
 314        dummy_mutind
 315     | C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri ->
 316        dummy_mutind
 317     | C.Cast (te,ty) -> subst_inductive_type_with_dummy_mutind te
 318     | C.Prod (name,so,ta) ->
 319        C.Prod (name, subst_inductive_type_with_dummy_mutind so,
 320         subst_inductive_type_with_dummy_mutind ta)
 321     | C.Lambda (name,so,ta) ->
 322        C.Lambda (name, subst_inductive_type_with_dummy_mutind so,
 323         subst_inductive_type_with_dummy_mutind ta)
 324     | C.Appl tl ->
 325        C.Appl (List.map subst_inductive_type_with_dummy_mutind tl)
 326     | C.MutCase (uri,i,outtype,term,pl) ->
 327        C.MutCase (uri,i,
 328         subst_inductive_type_with_dummy_mutind outtype,
 329         subst_inductive_type_with_dummy_mutind term,
 330         List.map subst_inductive_type_with_dummy_mutind pl)
 331     | C.Fix (i,fl) ->
 332        C.Fix (i,List.map (fun (name,i,ty,bo) -> (name,i,
 333         subst_inductive_type_with_dummy_mutind ty,
 334         subst_inductive_type_with_dummy_mutind bo)) fl)
 335     | C.CoFix (i,fl) ->
 336        C.CoFix (i,List.map (fun (name,ty,bo) -> (name,
 337         subst_inductive_type_with_dummy_mutind ty,
 338         subst_inductive_type_with_dummy_mutind bo)) fl)
 339     | C.Const (uri,exp_named_subst) ->
 340        let exp_named_subst' =
 341         List.map
 342          (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
 343          exp_named_subst
 344        in
 345         C.Const (uri,exp_named_subst')
 346     | C.MutInd (uri,typeno,exp_named_subst) ->
 347        let exp_named_subst' =
 348         List.map
 349          (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
 350          exp_named_subst
 351        in
 352         C.MutInd (uri,typeno,exp_named_subst')
 353     | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
 354        let exp_named_subst' =
 355         List.map
 356          (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
 357          exp_named_subst
 358        in
 359         C.MutConstruct (uri,typeno,consno,exp_named_subst')
 360     | t -> t
 361   in
 362   match CicReduction.whd context te with
 363      C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri -> true
 364    | C.MutInd (uri',0,_) when UriManager.eq uri' uri -> true
 365    | C.Prod (C.Anonymous,source,dest) ->
 366       strictly_positive context n nn
 367        (subst_inductive_type_with_dummy_mutind source) &&
 368        weakly_positive ((Some (C.Anonymous,(C.Decl source)))::context)
 369         (n + 1) (nn + 1) uri dest
 370    | C.Prod (name,source,dest) when
 371       does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
 372        (* dummy abstraction, so we behave as in the anonimous case *)
 373        strictly_positive context n nn
 374         (subst_inductive_type_with_dummy_mutind source) &&
 375         weakly_positive ((Some (name,(C.Decl source)))::context)
 376          (n + 1) (nn + 1) uri dest
 377    | C.Prod (name,source,dest) ->
 378       does_not_occur context n nn
 379        (subst_inductive_type_with_dummy_mutind source)&&
 380        weakly_positive ((Some (name,(C.Decl source)))::context)
 381         (n + 1) (nn + 1) uri dest
 382    | _ ->
 383      raise (TypeCheckerFailure "Malformed inductive constructor type")
 384
 385 (* instantiate_parameters ps (x1:T1)...(xn:Tn)C                             *)
 386 (* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *)
 387 and instantiate_parameters params c =
 388  let module C = Cic in
 389   match (c,params) with
 390      (c,[]) -> c
 391    | (C.Prod (_,_,ta), he::tl) ->
 392        instantiate_parameters tl
 393         (CicSubstitution.subst he ta)
 394    | (C.Cast (te,_), _) -> instantiate_parameters params te
 395    | (t,l) -> raise (AssertFailure "1")
 396
 397 and strictly_positive context n nn te =
 398  let module C = Cic in
 399  let module U = UriManager in
 400   match CicReduction.whd context te with
 401      C.Rel _ -> true
 402    | C.Cast (te,ty) ->
 403       (*CSC: bisogna controllare ty????*)
 404       strictly_positive context n nn te
 405    | C.Prod (name,so,ta) ->
 406       does_not_occur context n nn so &&
 407        strictly_positive ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) ta
 408    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
 409       List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
 410    | C.Appl ((C.MutInd (uri,i,exp_named_subst))::tl) ->
 411       let (ok,paramsno,ity,cl,name) =
 412         let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 413        match o with
 414            C.InductiveDefinition (tl,_,paramsno,_) ->
 415             let (name,_,ity,cl) = List.nth tl i in
 416              (List.length tl = 1, paramsno, ity, cl, name)
 417          | _ ->
 418            raise (TypeCheckerFailure
 419             ("Unknown inductive type:" ^ U.string_of_uri uri))
 420       in
 421        let (params,arguments) = split tl paramsno in
 422        let lifted_params = List.map (CicSubstitution.lift 1) params in
 423        let cl' =
 424         List.map
 425          (fun (_,te) ->
 426            instantiate_parameters lifted_params
 427             (CicSubstitution.subst_vars exp_named_subst te)
 428          ) cl
 429        in
 430         ok &&
 431          List.fold_right
 432           (fun x i -> i && does_not_occur context n nn x)
 433           arguments true &&
 434          (*CSC: MEGAPATCH3 (sara' quella giusta?)*)
 435          List.fold_right
 436           (fun x i ->
 437             i &&
 438              weakly_positive
 439               ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri
 440               x
 441           ) cl' true
 442    | t -> does_not_occur context n nn t
 443
 444 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
 445 and are_all_occurrences_positive context uri indparamsno i n nn te =
 446  let module C = Cic in
 447   match CicReduction.whd context te with
 448      C.Appl ((C.Rel m)::tl) when m = i ->
 449       (*CSC: riscrivere fermandosi a 0 *)
 450       (* let's check if the inductive type is applied at least to *)
 451       (* indparamsno parameters                                   *)
 452       let last =
 453        List.fold_left
 454         (fun k x ->
 455           if k = 0 then 0
 456           else
 457            match CicReduction.whd context x with
 458               C.Rel m when m = n - (indparamsno - k) -> k - 1
 459             | _ ->
 460               raise (TypeCheckerFailure
 461                 ("Non-positive occurence in mutual inductive definition(s) " ^
 462                 UriManager.string_of_uri uri))
 463         ) indparamsno tl
 464       in
 465        if last = 0 then
 466         List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
 467        else
 468         raise (TypeCheckerFailure
 469           ("Non-positive occurence in mutual inductive definition(s) " ^
 470           UriManager.string_of_uri uri))
 471    | C.Rel m when m = i ->
 472       if indparamsno = 0 then
 473        true
 474       else
 475         raise (TypeCheckerFailure
 476           ("Non-positive occurence in mutual inductive definition(s) " ^
 477           UriManager.string_of_uri uri))
 478    | C.Prod (C.Anonymous,source,dest) ->
 479       strictly_positive context n nn source &&
 480        are_all_occurrences_positive
 481         ((Some (C.Anonymous,(C.Decl source)))::context) uri indparamsno
 482         (i+1) (n + 1) (nn + 1) dest
 483    | C.Prod (name,source,dest) when
 484       does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
 485       (* dummy abstraction, so we behave as in the anonimous case *)
 486       strictly_positive context n nn source &&
 487        are_all_occurrences_positive
 488         ((Some (name,(C.Decl source)))::context) uri indparamsno
 489         (i+1) (n + 1) (nn + 1) dest
 490    | C.Prod (name,source,dest) ->
 491       does_not_occur context n nn source &&
 492        are_all_occurrences_positive ((Some (name,(C.Decl source)))::context)
 493         uri indparamsno (i+1) (n + 1) (nn + 1) dest
 494    | _ ->
 495      raise
 496       (TypeCheckerFailure ("Malformed inductive constructor type " ^
 497         (UriManager.string_of_uri uri)))
 498
 499 (* Main function to checks the correctness of a mutual *)
 500 (* inductive block definition. This is the function    *)
 501 (* exported to the proof-engine.                       *)
 502 and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph =
 503  let module U = UriManager in
 504   (* let's check if the arity of the inductive types are well *)
 505   (* formed                                                   *)
 506   let ugrap1 = List.fold_left
 507    (fun ugraph (_,_,x,_) -> let _,ugraph' =
 508       type_of ~logger x ugraph in ugraph')
 509    ugraph itl in
 510
 511   (* let's check if the types of the inductive constructors  *)
 512   (* are well formed.                                        *)
 513   (* In order not to use type_of_aux we put the types of the *)
 514   (* mutual inductive types at the head of the types of the  *)
 515   (* constructors using Prods                                *)
 516   let len = List.length itl in
 517   let tys =
 518     List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in
 519   let _,ugraph2 =
 520     List.fold_right
 521       (fun (_,_,_,cl) (i,ugraph) ->
 522         let ugraph'' =
 523           List.fold_left
 524             (fun ugraph (name,te) ->
 525               let debrujinedte = debrujin_constructor uri len te in
 526               let augmented_term =
 527                 List.fold_right
 528                   (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i))
 529                   itl debrujinedte
 530               in
 531               let _,ugraph' = type_of ~logger augmented_term ugraph in
 532               (* let's check also the positivity conditions *)
 533               if
 534                 not
 535                   (are_all_occurrences_positive tys uri indparamsno i 0 len
 536                      debrujinedte)
 537               then
 538                 raise
 539                   (TypeCheckerFailure ("Non positive occurence in " ^
 540                                        U.string_of_uri uri))
 541               else
 542                 ugraph'
 543             ) ugraph cl in
 544         (i + 1),ugraph''
 545       ) itl (1,ugraph)
 546   in
 547   ugraph2
 548
 549 (* Main function to checks the correctness of a mutual *)
 550 (* inductive block definition.                         *)
 551 and check_mutual_inductive_defs uri obj ugraph =
 552   match obj with
 553       Cic.InductiveDefinition (itl, params, indparamsno, _) ->
 554         typecheck_mutual_inductive_defs uri (itl,params,indparamsno) ugraph
 555     | _ ->
 556         raise (TypeCheckerFailure (
 557                  "Unknown mutual inductive definition:" ^
 558                  UriManager.string_of_uri uri))
 559
 560 and type_of_mutual_inductive_defs ~logger uri i ugraph =
 561  let module C = Cic in
 562  let module R = CicReduction in
 563  let module U = UriManager in
 564   let cobj,ugraph1 =
 565    match CicEnvironment.is_type_checked ~trust:true ugraph uri with
 566        CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
 567      | CicEnvironment.UncheckedObj uobj ->
 568          logger#log (`Start_type_checking uri) ;
 569          let ugraph1_dust =
 570            check_mutual_inductive_defs ~logger uri uobj ugraph
 571          in
 572            (* TASSI: FIXME: check ugraph1 == ugraph ritornato da env *)
 573            try
 574              CicEnvironment.set_type_checking_info uri ;
 575              logger#log (`Type_checking_completed uri) ;
 576              (match CicEnvironment.is_type_checked ~trust:false ugraph uri with
 577                   CicEnvironment.CheckedObj (cobj,ugraph') -> (cobj,ugraph')
 578                 | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
 579              )
 580            with
 581                Invalid_argument s ->
 582                  (*debug_print (lazy s);*)
 583                  uobj,ugraph1_dust
 584   in
 585     match cobj with
 586         C.InductiveDefinition (dl,_,_,_) ->
 587           let (_,_,arity,_) = List.nth dl i in
 588             arity,ugraph1
 589       | _ ->
 590           raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
 591                                      U.string_of_uri uri))
 592
 593 and type_of_mutual_inductive_constr ~logger uri i j ugraph =
 594  let module C = Cic in
 595  let module R = CicReduction in
 596  let module U = UriManager in
 597   let cobj,ugraph1 =
 598     match CicEnvironment.is_type_checked ~trust:true ugraph uri with
 599         CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
 600       | CicEnvironment.UncheckedObj uobj ->
 601           logger#log (`Start_type_checking uri) ;
 602           let ugraph1_dust =
 603             check_mutual_inductive_defs ~logger uri uobj ugraph
 604           in
 605             (* check ugraph1 validity ??? == ugraph' *)
 606             try
 607               CicEnvironment.set_type_checking_info uri ;
 608               logger#log (`Type_checking_completed uri) ;
 609               (match
 610                  CicEnvironment.is_type_checked ~trust:false ugraph uri
 611                with
 612                  CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
 613                | CicEnvironment.UncheckedObj _ ->
 614                        raise CicEnvironmentError)
 615             with
 616                 Invalid_argument s ->
 617                   (*debug_print (lazy s);*)
 618                   uobj,ugraph1_dust
 619   in
 620     match cobj with
 621         C.InductiveDefinition (dl,_,_,_) ->
 622           let (_,_,_,cl) = List.nth dl i in
 623           let (_,ty) = List.nth cl (j-1) in
 624             ty,ugraph1
 625       | _ ->
 626           raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
 627                                      UriManager.string_of_uri uri))
 628
 629 and recursive_args context n nn te =
 630  let module C = Cic in
 631   match CicReduction.whd context te with
 632      C.Rel _ -> []
 633    | C.Var _
 634    | C.Meta _
 635    | C.Sort _
 636    | C.Implicit _
 637    | C.Cast _ (*CSC ??? *) ->
 638       raise (AssertFailure "3") (* due to type-checking *)
 639    | C.Prod (name,so,de) ->
 640       (not (does_not_occur context n nn so)) ::
 641        (recursive_args ((Some (name,(C.Decl so)))::context) (n+1) (nn + 1) de)
 642    | C.Lambda _
 643    | C.LetIn _ ->
 644       raise (AssertFailure "4") (* due to type-checking *)
 645    | C.Appl _ -> []
 646    | C.Const _ -> raise (AssertFailure "5")
 647    | C.MutInd _
 648    | C.MutConstruct _
 649    | C.MutCase _
 650    | C.Fix _
 651    | C.CoFix _ -> raise (AssertFailure "6") (* due to type-checking *)
 652
 653 and get_new_safes ?(subst = []) context p c rl safes n nn x =
 654  let module C = Cic in
 655  let module U = UriManager in
 656  let module R = CicReduction in
 657   match (R.whd ~subst context c, R.whd ~subst context p, rl) with
 658      (C.Prod (_,so,ta1), C.Lambda (name,_,ta2), b::tl) ->
 659        (* we are sure that the two sources are convertible because we *)
 660        (* have just checked this. So let's go along ...               *)
 661        let safes' =
 662         List.map (fun x -> x + 1) safes
 663        in
 664         let safes'' =
 665          if b then 1::safes' else safes'
 666         in
 667          get_new_safes ~subst ((Some (name,(C.Decl so)))::context)
 668           ta2 ta1 tl safes'' (n+1) (nn+1) (x+1)
 669    | (C.Prod _, (C.MutConstruct _ as e), _)
 670    | (C.Prod _, (C.Rel _ as e), _)
 671    | (C.MutInd _, e, [])
 672    | (C.Appl _, e, []) -> (e,safes,n,nn,x,context)
 673    | (c,p,l) ->
 674       (* CSC: If the next exception is raised, it just means that   *)
 675       (* CSC: the proof-assistant allows to use very strange things *)
 676       (* CSC: as a branch of a case whose type is a Prod. In        *)
 677       (* CSC: particular, this means that a new (C.Prod, x,_) case  *)
 678       (* CSC: must be considered in this match. (e.g. x = MutCase)  *)
 679       raise
 680        (AssertFailure
 681          (Printf.sprintf "Get New Safes: c=%s ; p=%s"
 682            (CicPp.ppterm c) (CicPp.ppterm p)))
 683
 684 and split_prods ?(subst = []) context n te =
 685  let module C = Cic in
 686  let module R = CicReduction in
 687   match (n, R.whd context te) with
 688      (0, _) -> context,te
 689    | (n, C.Prod (name,so,ta)) when n > 0 ->
 690        split_prods ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta
 691    | (_, _) -> raise (AssertFailure "8")
 692
 693 and eat_lambdas ?(subst = []) context n te =
 694  let module C = Cic in
 695  let module R = CicReduction in
 696   match (n, R.whd ~subst context te) with
 697      (0, _) -> (te, 0, context)
 698    | (n, C.Lambda (name,so,ta)) when n > 0 ->
 699       let (te, k, context') =
 700        eat_lambdas ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta
 701       in
 702        (te, k + 1, context')
 703    | (n, te) ->
 704        raise (AssertFailure (sprintf "9 (%d, %s)" n (CicPp.ppterm te)))
 705
 706 (*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *)
 707 and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te =
 708  (*CSC: forse la whd si puo' fare solo quando serve veramente. *)
 709  (*CSC: cfr guarded_by_destructors                             *)
 710  let module C = Cic in
 711  let module U = UriManager in
 712  match CicReduction.whd context te with
 713      C.Rel m when List.mem m safes -> true
 714    | C.Rel _ -> false
 715    | C.Var _
 716    | C.Meta _
 717    | C.Sort _
 718    | C.Implicit _
 719    | C.Cast _
 720 (*   | C.Cast (te,ty) ->
 721       check_is_really_smaller_arg ~subst n nn kl x safes te &&
 722        check_is_really_smaller_arg ~subst n nn kl x safes ty*)
 723 (*   | C.Prod (_,so,ta) ->
 724       check_is_really_smaller_arg ~subst n nn kl x safes so &&
 725        check_is_really_smaller_arg ~subst (n+1) (nn+1) kl (x+1)
 726         (List.map (fun x -> x + 1) safes) ta*)
 727    | C.Prod _ -> raise (AssertFailure "10")
 728    | C.Lambda (name,so,ta) ->
 729       check_is_really_smaller_arg ~subst context n nn kl x safes so &&
 730        check_is_really_smaller_arg ~subst ((Some (name,(C.Decl so)))::context)
 731         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 732    | C.LetIn (name,so,ta) ->
 733       check_is_really_smaller_arg ~subst context n nn kl x safes so &&
 734        check_is_really_smaller_arg ~subst ((Some (name,(C.Def (so,None))))::context)
 735         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 736    | C.Appl (he::_) ->
 737       (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
 738       (*CSC: solo perche' non abbiamo trovato controesempi            *)
 739       check_is_really_smaller_arg ~subst context n nn kl x safes he
 740    | C.Appl [] -> raise (AssertFailure "11")
 741    | C.Const _
 742    | C.MutInd _ -> raise (AssertFailure "12")
 743    | C.MutConstruct _ -> false
 744    | C.MutCase (uri,i,outtype,term,pl) ->
 745       (match term with
 746           C.Rel m when List.mem m safes || m = x ->
 747            let (tys,len,isinductive,paramsno,cl) =
 748             let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 749             match o with
 750                C.InductiveDefinition (tl,_,paramsno,_) ->
 751                 let tys =
 752                  List.map
 753                   (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl
 754                 in
 755                  let (_,isinductive,_,cl) = List.nth tl i in
 756                   let cl' =
 757                    List.map
 758                     (fun (id,ty) ->
 759                       (id, snd (split_prods ~subst tys paramsno ty))) cl
 760                   in
 761                    (tys,List.length tl,isinductive,paramsno,cl')
 762              | _ ->
 763                 raise (TypeCheckerFailure
 764                   ("Unknown mutual inductive definition:" ^
 765                   UriManager.string_of_uri uri))
 766            in
 767             if not isinductive then
 768               List.fold_right
 769                (fun p i ->
 770                  i && check_is_really_smaller_arg ~subst context n nn kl x safes p)
 771                pl true
 772             else
 773              let pl_and_cl =
 774               try
 775                List.combine pl cl
 776               with
 777                Invalid_argument _ ->
 778                 raise (TypeCheckerFailure "not enough patterns")
 779              in
 780               List.fold_right
 781                (fun (p,(_,c)) i ->
 782                  let rl' =
 783                   let debrujinedte = debrujin_constructor uri len c in
 784                    recursive_args tys 0 len debrujinedte
 785                  in
 786                   let (e,safes',n',nn',x',context') =
 787                    get_new_safes ~subst context p c rl' safes n nn x
 788                   in
 789                    i &&
 790                    check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
 791                ) pl_and_cl true
 792         | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
 793            let (tys,len,isinductive,paramsno,cl) =
 794             let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 795             match o with
 796                C.InductiveDefinition (tl,_,paramsno,_) ->
 797                 let (_,isinductive,_,cl) = List.nth tl i in
 798                  let tys =
 799                   List.map (fun (n,_,ty,_) ->
 800                    Some(Cic.Name n,(Cic.Decl ty))) tl
 801                  in
 802                   let cl' =
 803                    List.map
 804                     (fun (id,ty) ->
 805                       (id, snd (split_prods ~subst tys paramsno ty))) cl
 806                   in
 807                    (tys,List.length tl,isinductive,paramsno,cl')
 808              | _ ->
 809                 raise (TypeCheckerFailure
 810                   ("Unknown mutual inductive definition:" ^
 811                   UriManager.string_of_uri uri))
 812            in
 813             if not isinductive then
 814               List.fold_right
 815                (fun p i ->
 816                  i && check_is_really_smaller_arg ~subst context n nn kl x safes p)
 817                pl true
 818             else
 819              let pl_and_cl =
 820               try
 821                List.combine pl cl
 822               with
 823                Invalid_argument _ ->
 824                 raise (TypeCheckerFailure "not enough patterns")
 825              in
 826               (*CSC: supponiamo come prima che nessun controllo sia necessario*)
 827               (*CSC: sugli argomenti di una applicazione                      *)
 828               List.fold_right
 829                (fun (p,(_,c)) i ->
 830                  let rl' =
 831                   let debrujinedte = debrujin_constructor uri len c in
 832                    recursive_args tys 0 len debrujinedte
 833                  in
 834                   let (e, safes',n',nn',x',context') =
 835                    get_new_safes context p c rl' safes n nn x
 836                   in
 837                    i &&
 838                    check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
 839                ) pl_and_cl true
 840         | _ ->
 841           List.fold_right
 842            (fun p i ->
 843              i && check_is_really_smaller_arg ~subst context n nn kl x safes p
 844            ) pl true
 845       )
 846    | C.Fix (_, fl) ->
 847       let len = List.length fl in
 848        let n_plus_len = n + len
 849        and nn_plus_len = nn + len
 850        and x_plus_len = x + len
 851        and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
 852        and safes' = List.map (fun x -> x + len) safes in
 853         List.fold_right
 854          (fun (_,_,ty,bo) i ->
 855            i &&
 856             check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl
 857              x_plus_len safes' bo
 858          ) fl true
 859    | C.CoFix (_, fl) ->
 860       let len = List.length fl in
 861        let n_plus_len = n + len
 862        and nn_plus_len = nn + len
 863        and x_plus_len = x + len
 864        and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
 865        and safes' = List.map (fun x -> x + len) safes in
 866         List.fold_right
 867          (fun (_,ty,bo) i ->
 868            i &&
 869             check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl
 870              x_plus_len safes' bo
 871          ) fl true
 872
 873 and guarded_by_destructors ?(subst = []) context n nn kl x safes =
 874  let module C = Cic in
 875  let module U = UriManager in
 876   function
 877      C.Rel m when m > n && m <= nn -> false
 878    | C.Rel m ->
 879       (match List.nth context (n-1) with
 880           Some (_,C.Decl _) -> true
 881         | Some (_,C.Def (bo,_)) ->
 882            guarded_by_destructors context m nn kl x safes
 883             (CicSubstitution.lift m bo)
 884         | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
 885       )
 886    | C.Meta _
 887    | C.Sort _
 888    | C.Implicit _ -> true
 889    | C.Cast (te,ty) ->
 890       guarded_by_destructors context n nn kl x safes te &&
 891        guarded_by_destructors context n nn kl x safes ty
 892    | C.Prod (name,so,ta) ->
 893       guarded_by_destructors context n nn kl x safes so &&
 894        guarded_by_destructors ((Some (name,(C.Decl so)))::context)
 895         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 896    | C.Lambda (name,so,ta) ->
 897       guarded_by_destructors context n nn kl x safes so &&
 898        guarded_by_destructors ((Some (name,(C.Decl so)))::context)
 899         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 900    | C.LetIn (name,so,ta) ->
 901       guarded_by_destructors context n nn kl x safes so &&
 902        guarded_by_destructors ((Some (name,(C.Def (so,None))))::context)
 903         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 904    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
 905       let k = List.nth kl (m - n - 1) in
 906        if not (List.length tl > k) then false
 907        else
 908         List.fold_right
 909          (fun param i ->
 910            i && guarded_by_destructors context n nn kl x safes param
 911          ) tl true &&
 912          check_is_really_smaller_arg ~subst context n nn kl x safes (List.nth tl k)
 913    | C.Appl tl ->
 914       List.fold_right
 915        (fun t i -> i && guarded_by_destructors context n nn kl x safes t)
 916        tl true
 917    | C.Var (_,exp_named_subst)
 918    | C.Const (_,exp_named_subst)
 919    | C.MutInd (_,_,exp_named_subst)
 920    | C.MutConstruct (_,_,_,exp_named_subst) ->
 921       List.fold_right
 922        (fun (_,t) i -> i && guarded_by_destructors context n nn kl x safes t)
 923        exp_named_subst true
 924    | C.MutCase (uri,i,outtype,term,pl) ->
 925       (match CicReduction.whd context term with
 926           C.Rel m when List.mem m safes || m = x ->
 927            let (tys,len,isinductive,paramsno,cl) =
 928             let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 929             match o with
 930                C.InductiveDefinition (tl,_,paramsno,_) ->
 931                 let len = List.length tl in
 932                  let (_,isinductive,_,cl) = List.nth tl i in
 933                   let tys =
 934                    List.map (fun (n,_,ty,_) ->
 935                     Some(Cic.Name n,(Cic.Decl ty))) tl
 936                   in
 937                    let cl' =
 938                     List.map
 939                      (fun (id,ty) ->
 940                       let debrujinedty = debrujin_constructor uri len ty in
 941                        (id, snd (split_prods ~subst tys paramsno ty),
 942                         snd (split_prods ~subst tys paramsno debrujinedty)
 943                        )) cl
 944                    in
 945                     (tys,len,isinductive,paramsno,cl')
 946              | _ ->
 947                 raise (TypeCheckerFailure
 948                   ("Unknown mutual inductive definition:" ^
 949                   UriManager.string_of_uri uri))
 950            in
 951             if not isinductive then
 952              guarded_by_destructors context n nn kl x safes outtype &&
 953               guarded_by_destructors context n nn kl x safes term &&
 954               (*CSC: manca ??? il controllo sul tipo di term? *)
 955               List.fold_right
 956                (fun p i ->
 957                  i && guarded_by_destructors context n nn kl x safes p)
 958                pl true
 959             else
 960              let pl_and_cl =
 961               try
 962                List.combine pl cl
 963               with
 964                Invalid_argument _ ->
 965                 raise (TypeCheckerFailure "not enough patterns")
 966              in
 967              guarded_by_destructors context n nn kl x safes outtype &&
 968               (*CSC: manca ??? il controllo sul tipo di term? *)
 969               List.fold_right
 970                (fun (p,(_,c,brujinedc)) i ->
 971                  let rl' = recursive_args tys 0 len brujinedc in
 972                   let (e,safes',n',nn',x',context') =
 973                    get_new_safes context p c rl' safes n nn x
 974                   in
 975                    i &&
 976                    guarded_by_destructors context' n' nn' kl x' safes' e
 977                ) pl_and_cl true
 978         | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
 979            let (tys,len,isinductive,paramsno,cl) =
 980             let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 981             match o with
 982                C.InductiveDefinition (tl,_,paramsno,_) ->
 983                 let (_,isinductive,_,cl) = List.nth tl i in
 984                  let tys =
 985                   List.map
 986                    (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
 987                  in
 988                   let cl' =
 989                    List.map
 990                     (fun (id,ty) ->
 991                       (id, snd (split_prods ~subst tys paramsno ty))) cl
 992                   in
 993                    (tys,List.length tl,isinductive,paramsno,cl')
 994              | _ ->
 995                 raise (TypeCheckerFailure
 996                   ("Unknown mutual inductive definition:" ^
 997                   UriManager.string_of_uri uri))
 998            in
 999             if not isinductive then
1000              guarded_by_destructors context n nn kl x safes outtype &&
1001               guarded_by_destructors context n nn kl x safes term &&
1002               (*CSC: manca ??? il controllo sul tipo di term? *)
1003               List.fold_right
1004                (fun p i ->
1005                  i && guarded_by_destructors context n nn kl x safes p)
1006                pl true
1007             else
1008              let pl_and_cl =
1009               try
1010                List.combine pl cl
1011               with
1012                Invalid_argument _ ->
1013                 raise (TypeCheckerFailure "not enough patterns")
1014              in
1015              guarded_by_destructors context n nn kl x safes outtype &&
1016               (*CSC: manca ??? il controllo sul tipo di term? *)
1017               List.fold_right
1018                (fun t i ->
1019                  i && guarded_by_destructors context n nn kl x safes t)
1020                tl true &&
1021               List.fold_right
1022                (fun (p,(_,c)) i ->
1023                  let rl' =
1024                   let debrujinedte = debrujin_constructor uri len c in
1025                    recursive_args tys 0 len debrujinedte
1026                  in
1027                   let (e, safes',n',nn',x',context') =
1028                    get_new_safes context p c rl' safes n nn x
1029                   in
1030                    i &&
1031                    guarded_by_destructors context' n' nn' kl x' safes' e
1032                ) pl_and_cl true
1033         | _ ->
1034           guarded_by_destructors context n nn kl x safes outtype &&
1035            guarded_by_destructors context n nn kl x safes term &&
1036            (*CSC: manca ??? il controllo sul tipo di term? *)
1037            List.fold_right
1038             (fun p i -> i && guarded_by_destructors context n nn kl x safes p)
1039             pl true
1040       )
1041    | C.Fix (_, fl) ->
1042       let len = List.length fl in
1043        let n_plus_len = n + len
1044        and nn_plus_len = nn + len
1045        and x_plus_len = x + len
1046        and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
1047        and safes' = List.map (fun x -> x + len) safes in
1048         List.fold_right
1049          (fun (_,_,ty,bo) i ->
1050            i && guarded_by_destructors context n nn kl x_plus_len safes' ty &&
1051             guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
1052              x_plus_len safes' bo
1053          ) fl true
1054    | C.CoFix (_, fl) ->
1055       let len = List.length fl in
1056        let n_plus_len = n + len
1057        and nn_plus_len = nn + len
1058        and x_plus_len = x + len
1059        and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
1060        and safes' = List.map (fun x -> x + len) safes in
1061         List.fold_right
1062          (fun (_,ty,bo) i ->
1063            i &&
1064             guarded_by_destructors context n nn kl x_plus_len safes' ty &&
1065             guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
1066              x_plus_len safes' bo
1067          ) fl true
1068
1069 (* the boolean h means already protected *)
1070 (* args is the list of arguments the type of the constructor that may be *)
1071 (* found in head position must be applied to.                            *)
1072 (*CSC: coInductiveTypeURI non cambia mai di ricorsione in ricorsione *)
1073 and guarded_by_constructors context n nn h te args coInductiveTypeURI =
1074  let module C = Cic in
1075   (*CSC: There is a lot of code replication between the cases X and    *)
1076   (*CSC: (C.Appl X tl). Maybe it will be better to define a function   *)
1077   (*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *)
1078   match CicReduction.whd context te with
1079      C.Rel m when m > n && m <= nn -> h
1080    | C.Rel _ -> true
1081    | C.Meta _
1082    | C.Sort _
1083    | C.Implicit _
1084    | C.Cast _
1085    | C.Prod _
1086    | C.LetIn _ ->
1087       (* the term has just been type-checked *)
1088       raise (AssertFailure "17")
1089    | C.Lambda (name,so,de) ->
1090       does_not_occur context n nn so &&
1091        guarded_by_constructors ((Some (name,(C.Decl so)))::context)
1092         (n + 1) (nn + 1) h de args coInductiveTypeURI
1093    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
1094       h &&
1095        List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
1096    | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) ->
1097       let consty =
1098         let obj,_ =
1099           try
1100             CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
1101           with Not_found -> assert false
1102         in
1103        match obj with
1104           C.InductiveDefinition (itl,_,_,_) ->
1105            let (_,_,_,cl) = List.nth itl i in
1106             let (_,cons) = List.nth cl (j - 1) in
1107              CicSubstitution.subst_vars exp_named_subst cons
1108         | _ ->
1109             raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1110               UriManager.string_of_uri uri))
1111       in
1112        let rec analyse_branch context ty te =
1113         match CicReduction.whd context ty with
1114            C.Meta _ -> raise (AssertFailure "34")
1115          | C.Rel _
1116          | C.Var _
1117          | C.Sort _ ->
1118             does_not_occur context n nn te
1119          | C.Implicit _
1120          | C.Cast _ ->
1121             raise (AssertFailure "24")(* due to type-checking *)
1122          | C.Prod (name,so,de) ->
1123             analyse_branch ((Some (name,(C.Decl so)))::context) de te
1124          | C.Lambda _
1125          | C.LetIn _ ->
1126             raise (AssertFailure "25")(* due to type-checking *)
1127          | C.Appl ((C.MutInd (uri,_,_))::_) as ty
1128             when uri == coInductiveTypeURI ->
1129              guarded_by_constructors context n nn true te [] coInductiveTypeURI
1130          | C.Appl ((C.MutInd (uri,_,_))::_) as ty ->
1131             guarded_by_constructors context n nn true te tl coInductiveTypeURI
1132          | C.Appl _ ->
1133             does_not_occur context n nn te
1134          | C.Const _ -> raise (AssertFailure "26")
1135          | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
1136             guarded_by_constructors context n nn true te [] coInductiveTypeURI
1137          | C.MutInd _ ->
1138             does_not_occur context n nn te
1139          | C.MutConstruct _ -> raise (AssertFailure "27")
1140          (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
1141          (*CSC: in head position.                                       *)
1142          | C.MutCase _
1143          | C.Fix _
1144          | C.CoFix _ ->
1145             raise (AssertFailure "28")(* due to type-checking *)
1146        in
1147        let rec analyse_instantiated_type context ty l =
1148         match CicReduction.whd context ty with
1149            C.Rel _
1150          | C.Var _
1151          | C.Meta _
1152          | C.Sort _
1153          | C.Implicit _
1154          | C.Cast _ -> raise (AssertFailure "29")(* due to type-checking *)
1155          | C.Prod (name,so,de) ->
1156             begin
1157              match l with
1158                 [] -> true
1159               | he::tl ->
1160                  analyse_branch context so he &&
1161                   analyse_instantiated_type
1162                    ((Some (name,(C.Decl so)))::context) de tl
1163             end
1164          | C.Lambda _
1165          | C.LetIn _ ->
1166             raise (AssertFailure "30")(* due to type-checking *)
1167          | C.Appl _ ->
1168             List.fold_left
1169              (fun i x -> i && does_not_occur context n nn x) true l
1170          | C.Const _ -> raise (AssertFailure "31")
1171          | C.MutInd _ ->
1172             List.fold_left
1173              (fun i x -> i && does_not_occur context n nn x) true l
1174          | C.MutConstruct _ -> raise (AssertFailure "32")
1175          (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
1176          (*CSC: in head position.                                       *)
1177          | C.MutCase _
1178          | C.Fix _
1179          | C.CoFix _ ->
1180             raise (AssertFailure "33")(* due to type-checking *)
1181        in
1182         let rec instantiate_type args consty =
1183          function
1184             [] -> true
1185           | tlhe::tltl as l ->
1186              let consty' = CicReduction.whd context consty in
1187               match args with
1188                  he::tl ->
1189                   begin
1190                    match consty' with
1191                       C.Prod (_,_,de) ->
1192                        let instantiated_de = CicSubstitution.subst he de in
1193                         (*CSC: siamo sicuri che non sia troppo forte? *)
1194                         does_not_occur context n nn tlhe &
1195                          instantiate_type tl instantiated_de tltl
1196                     | _ ->
1197                       (*CSC:We do not consider backbones with a MutCase, a    *)
1198                       (*CSC:FixPoint, a CoFixPoint and so on in head position.*)
1199                       raise (AssertFailure "23")
1200                   end
1201                | [] -> analyse_instantiated_type context consty' l
1202                   (* These are all the other cases *)
1203        in
1204         instantiate_type args consty tl
1205    | C.Appl ((C.CoFix (_,fl))::tl) ->
1206       List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
1207        let len = List.length fl in
1208         let n_plus_len = n + len
1209         and nn_plus_len = nn + len
1210         (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1211         and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1212          List.fold_right
1213           (fun (_,ty,bo) i ->
1214             i && does_not_occur context n nn ty &&
1215              guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1216               args coInductiveTypeURI
1217           ) fl true
1218    | C.Appl ((C.MutCase (_,_,out,te,pl))::tl) ->
1219        List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
1220         does_not_occur context n nn out &&
1221          does_not_occur context n nn te &&
1222           List.fold_right
1223            (fun x i ->
1224              i &&
1225              guarded_by_constructors context n nn h x args coInductiveTypeURI
1226            ) pl true
1227    | C.Appl l ->
1228       List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
1229    | C.Var (_,exp_named_subst)
1230    | C.Const (_,exp_named_subst) ->
1231       List.fold_right
1232        (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
1233    | C.MutInd _ -> assert false
1234    | C.MutConstruct (_,_,_,exp_named_subst) ->
1235       List.fold_right
1236        (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
1237    | C.MutCase (_,_,out,te,pl) ->
1238        does_not_occur context n nn out &&
1239         does_not_occur context n nn te &&
1240          List.fold_right
1241           (fun x i ->
1242             i &&
1243              guarded_by_constructors context n nn h x args coInductiveTypeURI
1244           ) pl true
1245    | C.Fix (_,fl) ->
1246       let len = List.length fl in
1247        let n_plus_len = n + len
1248        and nn_plus_len = nn + len
1249        (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1250        and tys = List.map (fun (n,_,ty,_)-> Some (C.Name n,(C.Decl ty))) fl in
1251         List.fold_right
1252          (fun (_,_,ty,bo) i ->
1253            i && does_not_occur context n nn ty &&
1254             does_not_occur (tys@context) n_plus_len nn_plus_len bo
1255          ) fl true
1256    | C.CoFix (_,fl) ->
1257       let len = List.length fl in
1258        let n_plus_len = n + len
1259        and nn_plus_len = nn + len
1260        (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1261        and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1262         List.fold_right
1263          (fun (_,ty,bo) i ->
1264            i && does_not_occur context n nn ty &&
1265             guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1266              args coInductiveTypeURI
1267          ) fl true
1268
1269 and check_allowed_sort_elimination ~logger context uri i need_dummy ind
1270   arity1 arity2 ugraph =
1271  let module C = Cic in
1272  let module U = UriManager in
1273   match (CicReduction.whd context arity1, CicReduction.whd context arity2) with
1274      (C.Prod (_,so1,de1), C.Prod (_,so2,de2)) ->
1275        let b,ugraph1 = CicReduction.are_convertible context so1 so2 ugraph in
1276        if b then
1277          check_allowed_sort_elimination ~logger context uri i need_dummy
1278            (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2 ugraph1
1279        else
1280          false,ugraph1
1281    | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true,ugraph
1282    | (C.Sort C.Prop, C.Sort C.Set)
1283    | (C.Sort C.Prop, C.Sort C.CProp)
1284    | (C.Sort C.Prop, C.Sort (C.Type _) ) when need_dummy ->
1285    (* TASSI: da verificare *)
1286 (*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *)
1287        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1288          match o with
1289          C.InductiveDefinition (itl,_,_,_) ->
1290            let (_,_,_,cl) = List.nth itl i in
1291            (* is a singleton definition or the empty proposition? *)
1292            (List.length cl = 1 || List.length cl = 0) , ugraph
1293          | _ ->
1294              raise (TypeCheckerFailure
1295                       ("Unknown mutual inductive definition:" ^
1296                        UriManager.string_of_uri uri))
1297        )
1298    | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true , ugraph
1299    | (C.Sort C.CProp, C.Sort C.Prop) when need_dummy -> true , ugraph
1300    | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true , ugraph
1301    | (C.Sort C.Set, C.Sort C.CProp) when need_dummy -> true , ugraph
1302    | (C.Sort C.CProp, C.Sort C.Set) when need_dummy -> true , ugraph
1303    | (C.Sort C.CProp, C.Sort C.CProp) when need_dummy -> true , ugraph
1304    | ((C.Sort C.Set, C.Sort (C.Type _)) | (C.Sort C.CProp, C.Sort (C.Type _)))
1305       (* TASSI: da verificare *)
1306       when need_dummy ->
1307        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1308          match o with
1309            C.InductiveDefinition (itl,_,paramsno,_) ->
1310             let tys =
1311              List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1312             in
1313              let (_,_,_,cl) = List.nth itl i in
1314               (List.fold_right
1315                (fun (_,x) (i,ugraph) ->
1316                  if i then
1317                    is_small ~logger tys paramsno x ugraph
1318                  else
1319                    false,ugraph
1320                     ) cl (true,ugraph))
1321            | _ ->
1322             raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1323               UriManager.string_of_uri uri))
1324        )
1325    | (C.Sort (C.Type _), C.Sort _) when need_dummy -> true , ugraph
1326      (* TASSI: da verificare *)
1327    | (C.Sort C.Prop, C.Prod (name,so,ta)) when not need_dummy ->
1328        let b,ugraph1 = CicReduction.are_convertible context so ind ugraph in
1329        if not b then
1330          false,ugraph1
1331        else
1332          (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1333               C.Sort C.Prop -> true,ugraph1
1334            | (C.Sort C.Set | C.Sort C.CProp | C.Sort (C.Type _)) ->
1335                (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1336                  match o with
1337                     C.InductiveDefinition (itl,_,_,_) ->
1338                      let (_,_,_,cl) = List.nth itl i in
1339                      (* is a singleton definition or the empty proposition? *)
1340                      (List.length cl = 1 || List.length cl = 0),ugraph1
1341                   | _ ->
1342                    raise (TypeCheckerFailure
1343                     ("Unknown mutual inductive definition:" ^
1344                        UriManager.string_of_uri uri)))
1345            | _ -> false,ugraph1)
1346    | ((C.Sort C.Set, C.Prod (name,so,ta))
1347    | (C.Sort C.CProp, C.Prod (name,so,ta)))
1348      when not need_dummy ->
1349        let b,ugraph1 = CicReduction.are_convertible context so ind ugraph in
1350        if not b then
1351          false,ugraph1
1352        else
1353          (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1354            C.Sort C.Prop
1355          | C.Sort C.Set  -> true,ugraph1
1356          | C.Sort C.CProp -> true,ugraph1
1357          | C.Sort (C.Type _) ->
1358              (* TASSI: da verificare *)
1359              (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1360                match o with
1361                C.InductiveDefinition (itl,_,paramsno,_) ->
1362                  let (_,_,_,cl) = List.nth itl i in
1363                  let tys =
1364                    List.map
1365                      (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1366                  in
1367                  (List.fold_right
1368                    (fun (_,x) (i,ugraph) ->
1369                       if i then
1370                         is_small ~logger tys paramsno x ugraph
1371                       else
1372                         false,ugraph
1373                    ) cl (true,ugraph1))
1374              | _ ->
1375                  raise (TypeCheckerFailure
1376                           ("Unknown mutual inductive definition:" ^
1377                            UriManager.string_of_uri uri))
1378              )
1379          | _ -> raise (AssertFailure "19")
1380          )
1381    | (C.Sort (C.Type _), C.Prod (_,so,_)) when not need_dummy ->
1382        (* TASSI: da verificare *)
1383        CicReduction.are_convertible context so ind ugraph
1384    | (_,_) -> false,ugraph
1385
1386 and type_of_branch context argsno need_dummy outtype term constype =
1387  let module C = Cic in
1388  let module R = CicReduction in
1389   match R.whd context constype with
1390      C.MutInd (_,_,_) ->
1391       if need_dummy then
1392        outtype
1393       else
1394        C.Appl [outtype ; term]
1395    | C.Appl (C.MutInd (_,_,_)::tl) ->
1396       let (_,arguments) = split tl argsno
1397       in
1398        if need_dummy && arguments = [] then
1399         outtype
1400        else
1401         C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
1402    | C.Prod (name,so,de) ->
1403       let term' =
1404        match CicSubstitution.lift 1 term with
1405           C.Appl l -> C.Appl (l@[C.Rel 1])
1406         | t -> C.Appl [t ; C.Rel 1]
1407       in
1408        C.Prod (C.Anonymous,so,type_of_branch
1409         ((Some (name,(C.Decl so)))::context) argsno need_dummy
1410         (CicSubstitution.lift 1 outtype) term' de)
1411   | _ -> raise (AssertFailure "20")
1412
1413 (* check_metasenv_consistency checks that the "canonical" context of a
1414 metavariable is consitent - up to relocation via the relocation list l -
1415 with the actual context *)
1416
1417
1418 and check_metasenv_consistency ~logger ?(subst=[]) metasenv context
1419   canonical_context l ugraph
1420 =
1421   let module C = Cic in
1422   let module R = CicReduction in
1423   let module S = CicSubstitution in
1424   let lifted_canonical_context =
1425     let rec aux i =
1426      function
1427          [] -> []
1428        | (Some (n,C.Decl t))::tl ->
1429            (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
1430        | (Some (n,C.Def (t,None)))::tl ->
1431            (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
1432        | None::tl -> None::(aux (i+1) tl)
1433        | (Some (n,C.Def (t,Some ty)))::tl ->
1434            (Some (n,C.Def ((S.subst_meta l (S.lift i t)),Some (S.subst_meta l (S.lift i ty)))))::(aux (i+1) tl)
1435     in
1436      aux 1 canonical_context
1437    in
1438    List.fold_left2
1439      (fun ugraph t ct ->
1440        match (t,ct) with
1441        | _,None -> ugraph
1442        | Some t,Some (_,C.Def (ct,_)) ->
1443            let b,ugraph1 =
1444              R.are_convertible ~subst ~metasenv context t ct ugraph
1445            in
1446            if not b then
1447              raise
1448                (TypeCheckerFailure
1449                   (sprintf "Not well typed metavariable local context: expected a term convertible with %s, found %s" (CicPp.ppterm ct) (CicPp.ppterm t)))
1450            else
1451              ugraph1
1452        | Some t,Some (_,C.Decl ct) ->
1453            let type_t,ugraph1 =
1454              type_of_aux' ~logger ~subst metasenv context t ugraph
1455            in
1456            let b,ugraph2 =
1457              R.are_convertible ~subst ~metasenv context type_t ct ugraph1
1458            in
1459            if not b then
1460              raise (TypeCheckerFailure
1461                       (sprintf "Not well typed metavariable local context: expected a term of type %s, found %s of type %s"
1462                          (CicPp.ppterm ct) (CicPp.ppterm t)
1463                          (CicPp.ppterm type_t)))
1464            else
1465              ugraph2
1466        | None, _  ->
1467            raise (TypeCheckerFailure
1468                     ("Not well typed metavariable local context: "^
1469                      "an hypothesis, that is not hidden, is not instantiated"))
1470      ) ugraph l lifted_canonical_context
1471
1472
1473 (*
1474    type_of_aux' is just another name (with a different scope)
1475    for type_of_aux
1476 *)
1477
1478 and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
1479  let rec type_of_aux ~logger context t ugraph =
1480   let module C = Cic in
1481   let module R = CicReduction in
1482   let module S = CicSubstitution in
1483   let module U = UriManager in
1484    match t with
1485       C.Rel n ->
1486        (try
1487          match List.nth context (n - 1) with
1488             Some (_,C.Decl t) -> S.lift n t,ugraph
1489           | Some (_,C.Def (_,Some ty)) -> S.lift n ty,ugraph
1490           | Some (_,C.Def (bo,None)) ->
1491              debug_print (lazy "##### CASO DA INVESTIGARE E CAPIRE") ;
1492               type_of_aux ~logger context (S.lift n bo) ugraph
1493           | None -> raise
1494               (TypeCheckerFailure "Reference to deleted hypothesis")
1495         with
1496         _ ->
1497           raise (TypeCheckerFailure "unbound variable")
1498        )
1499     | C.Var (uri,exp_named_subst) ->
1500       incr fdebug ;
1501         let ugraph1 =
1502           check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
1503         in
1504         let ty,ugraph2 = type_of_variable ~logger uri ugraph1 in
1505         let ty1 = CicSubstitution.subst_vars exp_named_subst ty in
1506           decr fdebug ;
1507           ty1,ugraph2
1508     | C.Meta (n,l) ->
1509        (try
1510           let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in
1511           let ugraph1 =
1512             check_metasenv_consistency ~logger
1513               ~subst metasenv context canonical_context l ugraph
1514           in
1515             (* assuming subst is well typed !!!!! *)
1516             ((CicSubstitution.subst_meta l ty), ugraph1)
1517               (* type_of_aux context (CicSubstitution.subst_meta l term) *)
1518         with CicUtil.Subst_not_found _ ->
1519           let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
1520           let ugraph1 =
1521             check_metasenv_consistency ~logger
1522               ~subst metasenv context canonical_context l ugraph
1523           in
1524             ((CicSubstitution.subst_meta l ty),ugraph1))
1525       (* TASSI: CONSTRAINTS *)
1526     | C.Sort (C.Type t) ->
1527        let t' = CicUniv.fresh() in
1528        let ugraph1 = CicUniv.add_gt t' t ugraph in
1529          (C.Sort (C.Type t')),ugraph1
1530       (* TASSI: CONSTRAINTS *)
1531     | C.Sort s -> (C.Sort (C.Type (CicUniv.fresh ()))),ugraph
1532     | C.Implicit _ -> raise (AssertFailure "21")
1533     | C.Cast (te,ty) as t ->
1534        let _,ugraph1 = type_of_aux ~logger context ty ugraph in
1535        let ty_te,ugraph2 = type_of_aux ~logger context te ugraph1 in
1536        let b,ugraph3 =
1537          R.are_convertible ~subst ~metasenv context ty_te ty ugraph2
1538        in
1539          if b then
1540            ty,ugraph3
1541          else
1542            raise (TypeCheckerFailure
1543                     (sprintf "Invalid cast %s" (CicPp.ppterm t)))
1544     | C.Prod (name,s,t) ->
1545        let sort1,ugraph1 = type_of_aux ~logger context s ugraph in
1546        let sort2,ugraph2 =
1547          type_of_aux ~logger  ((Some (name,(C.Decl s)))::context) t ugraph1
1548        in
1549        sort_of_prod ~subst context (name,s) (sort1,sort2) ugraph2
1550    | C.Lambda (n,s,t) ->
1551        let sort1,ugraph1 = type_of_aux ~logger context s ugraph in
1552        (match R.whd ~subst context sort1 with
1553            C.Meta _
1554          | C.Sort _ -> ()
1555          | _ ->
1556            raise
1557             (TypeCheckerFailure (sprintf
1558               "Not well-typed lambda-abstraction: the source %s should be a type; instead it is a term of type %s" (CicPp.ppterm s)
1559                 (CicPp.ppterm sort1)))
1560        ) ;
1561        let type2,ugraph2 =
1562          type_of_aux ~logger ((Some (n,(C.Decl s)))::context) t ugraph1
1563        in
1564          (C.Prod (n,s,type2)),ugraph2
1565    | C.LetIn (n,s,t) ->
1566       (* only to check if s is well-typed *)
1567       let ty,ugraph1 = type_of_aux ~logger context s ugraph in
1568        (* The type of a LetIn is a LetIn. Extremely slow since the computed
1569           LetIn is later reduced and maybe also re-checked.
1570        (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t))
1571        *)
1572        (* The type of the LetIn is reduced. Much faster than the previous
1573           solution. Moreover the inferred type is probably very different
1574           from the expected one.
1575        (CicReduction.whd context
1576         (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)))
1577        *)
1578        (* One-step LetIn reduction. Even faster than the previous solution.
1579           Moreover the inferred type is closer to the expected one. *)
1580        let ty1,ugraph2 =
1581          type_of_aux ~logger
1582            ((Some (n,(C.Def (s,Some ty))))::context) t ugraph1
1583        in
1584        (CicSubstitution.subst s ty1),ugraph2
1585    | C.Appl (he::tl) when List.length tl > 0 ->
1586        let hetype,ugraph1 = type_of_aux ~logger context he ugraph in
1587        let tlbody_and_type,ugraph2 =
1588          List.fold_right (
1589            fun x (l,ugraph) ->
1590              let ty,ugraph1 = type_of_aux ~logger context x ugraph in
1591              let _,ugraph1 = type_of_aux ~logger  context ty ugraph1 in
1592                ((x,ty)::l,ugraph1))
1593            tl ([],ugraph1)
1594        in
1595          (* TASSI: questa c'era nel mio... ma non nel CVS... *)
1596          (* let _,ugraph2 = type_of_aux context hetype ugraph2 in *)
1597          eat_prods ~subst context hetype tlbody_and_type ugraph2
1598    | C.Appl _ -> raise (AssertFailure "Appl: no arguments")
1599    | C.Const (uri,exp_named_subst) ->
1600        incr fdebug ;
1601        let ugraph1 =
1602          check_exp_named_subst ~logger ~subst  context exp_named_subst ugraph
1603        in
1604        let cty,ugraph2 = type_of_constant ~logger uri ugraph1 in
1605        let cty1 =
1606          CicSubstitution.subst_vars exp_named_subst cty
1607        in
1608          decr fdebug ;
1609          cty1,ugraph2
1610    | C.MutInd (uri,i,exp_named_subst) ->
1611       incr fdebug ;
1612        let ugraph1 =
1613          check_exp_named_subst ~logger  ~subst context exp_named_subst ugraph
1614        in
1615          (* TASSI: da me c'era anche questa, ma in CVS no *)
1616        let mty,ugraph2 = type_of_mutual_inductive_defs ~logger uri i ugraph1 in
1617          (* fine parte dubbia *)
1618        let cty =
1619          CicSubstitution.subst_vars exp_named_subst mty
1620        in
1621          decr fdebug ;
1622          cty,ugraph2
1623    | C.MutConstruct (uri,i,j,exp_named_subst) ->
1624        let ugraph1 =
1625          check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
1626        in
1627          (* TASSI: idem come sopra *)
1628        let mty,ugraph2 =
1629          type_of_mutual_inductive_constr ~logger uri i j ugraph1
1630        in
1631        let cty =
1632          CicSubstitution.subst_vars exp_named_subst mty
1633        in
1634          cty,ugraph2
1635    | C.MutCase (uri,i,outtype,term,pl) ->
1636       let outsort,ugraph1 = type_of_aux ~logger context outtype ugraph in
1637       let (need_dummy, k) =
1638       let rec guess_args context t =
1639         let outtype = CicReduction.whd ~subst context t in
1640           match outtype with
1641               C.Sort _ -> (true, 0)
1642             | C.Prod (name, s, t) ->
1643                 let (b, n) =
1644                   guess_args ((Some (name,(C.Decl s)))::context) t in
1645                   if n = 0 then
1646                   (* last prod before sort *)
1647                     match CicReduction.whd ~subst context s with
1648 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1649                         C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
1650                           (false, 1)
1651 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1652                       | C.Appl ((C.MutInd (uri',i',_)) :: _)
1653                           when U.eq uri' uri && i' = i -> (false, 1)
1654                       | _ -> (true, 1)
1655                   else
1656                     (b, n + 1)
1657             | _ ->
1658                 raise
1659                   (TypeCheckerFailure
1660                      (sprintf
1661                         "Malformed case analasys' output type %s"
1662                         (CicPp.ppterm outtype)))
1663       in
1664 (*
1665       let (parameters, arguments, exp_named_subst),ugraph2 =
1666         let ty,ugraph2 = type_of_aux context term ugraph1 in
1667           match R.whd context ty with
1668            (*CSC manca il caso dei CAST *)
1669 (*CSC: ma servono i parametri (uri,i)? Se si', perche' non serve anche il *)
1670 (*CSC: parametro exp_named_subst? Se no, perche' non li togliamo?         *)
1671 (*CSC: Hint: nella DTD servono per gli stylesheet.                        *)
1672               C.MutInd (uri',i',exp_named_subst) as typ ->
1673                 if U.eq uri uri' && i = i' then
1674                   ([],[],exp_named_subst),ugraph2
1675                 else
1676                   raise
1677                     (TypeCheckerFailure
1678                        (sprintf
1679                           ("Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}")
1680                           (CicPp.ppterm typ) (U.string_of_uri uri) i))
1681             | C.Appl
1682                 ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
1683                 if U.eq uri uri' && i = i' then
1684                   let params,args =
1685                     split tl (List.length tl - k)
1686                   in (params,args,exp_named_subst),ugraph2
1687                 else
1688                   raise
1689                     (TypeCheckerFailure
1690                        (sprintf
1691                           ("Case analysys: analysed term type is %s, "^
1692                            "but is expected to be (an application of) "^
1693                            "%s#1/%d{_}")
1694                           (CicPp.ppterm typ') (U.string_of_uri uri) i))
1695             | _ ->
1696                 raise
1697                   (TypeCheckerFailure
1698                      (sprintf
1699                         ("Case analysis: "^
1700                          "analysed term %s is not an inductive one")
1701                         (CicPp.ppterm term)))
1702 *)
1703       let (b, k) = guess_args context outsort in
1704           if not b then (b, k - 1) else (b, k) in
1705       let (parameters, arguments, exp_named_subst),ugraph2 =
1706         let ty,ugraph2 = type_of_aux ~logger context term ugraph1 in
1707         match R.whd ~subst context ty with
1708             C.MutInd (uri',i',exp_named_subst) as typ ->
1709               if U.eq uri uri' && i = i' then
1710                 ([],[],exp_named_subst),ugraph2
1711               else raise
1712                 (TypeCheckerFailure
1713                    (sprintf
1714                       ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}")
1715                       (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i))
1716           | C.Appl
1717               ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
1718               if U.eq uri uri' && i = i' then
1719                 let params,args =
1720                   split tl (List.length tl - k)
1721                 in (params,args,exp_named_subst),ugraph2
1722               else raise
1723                 (TypeCheckerFailure
1724                    (sprintf
1725                       ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}")
1726                       (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i))
1727           | _ ->
1728               raise
1729                 (TypeCheckerFailure
1730                    (sprintf
1731                       "Case analysis: analysed term %s is not an inductive one"
1732                       (CicPp.ppterm term)))
1733       in
1734         (*
1735            let's control if the sort elimination is allowed:
1736            [(I q1 ... qr)|B]
1737         *)
1738       let sort_of_ind_type =
1739         if parameters = [] then
1740           C.MutInd (uri,i,exp_named_subst)
1741         else
1742           C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters)
1743       in
1744       let type_of_sort_of_ind_ty,ugraph3 =
1745         type_of_aux ~logger context sort_of_ind_type ugraph2 in
1746       let b,ugraph4 =
1747         check_allowed_sort_elimination ~logger  context uri i need_dummy
1748           sort_of_ind_type type_of_sort_of_ind_ty outsort ugraph3
1749       in
1750         if not b then
1751         raise
1752           (TypeCheckerFailure ("Case analasys: sort elimination not allowed"));
1753         (* let's check if the type of branches are right *)
1754       let parsno =
1755         let obj,_ =
1756           try
1757             CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
1758           with Not_found -> assert false
1759         in
1760         match obj with
1761             C.InductiveDefinition (_,_,parsno,_) -> parsno
1762           | _ ->
1763               raise (TypeCheckerFailure
1764                 ("Unknown mutual inductive definition:" ^
1765                   UriManager.string_of_uri uri))
1766         in
1767       let (_,branches_ok,ugraph5) =
1768         List.fold_left
1769           (fun (j,b,ugraph) p ->
1770             if b then
1771               let cons =
1772                 if parameters = [] then
1773                   (C.MutConstruct (uri,i,j,exp_named_subst))
1774                 else
1775                   (C.Appl
1776                      (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
1777               in
1778               let ty_p,ugraph1 = type_of_aux ~logger context p ugraph in
1779               let ty_cons,ugraph3 = type_of_aux ~logger context cons ugraph1 in
1780               (* 2 is skipped *)
1781               let ty_branch =
1782                 type_of_branch context parsno need_dummy outtype cons
1783                   ty_cons in
1784               let b1,ugraph4 =
1785                 R.are_convertible
1786                   ~subst ~metasenv context ty_p ty_branch ugraph3
1787               in
1788               if not b1 then
1789                 debug_print (lazy
1790                   ("#### " ^ CicPp.ppterm ty_p ^
1791                   " <==> " ^ CicPp.ppterm ty_branch));
1792               (j + 1,b1,ugraph4)
1793             else
1794               (j,false,ugraph)
1795           ) (1,true,ugraph4) pl
1796          in
1797           if not branches_ok then
1798            raise
1799             (TypeCheckerFailure "Case analysys: wrong branch type");
1800           let arguments' =
1801            if not need_dummy then outtype::arguments@[term]
1802            else outtype::arguments in
1803           let outtype =
1804            if need_dummy && arguments = [] then outtype
1805            else CicReduction.head_beta_reduce (C.Appl arguments')
1806           in
1807            outtype,ugraph5
1808    | C.Fix (i,fl) ->
1809       let types_times_kl,ugraph1 =
1810         (* WAS: list rev list map *)
1811         List.fold_left
1812           (fun (l,ugraph) (n,k,ty,_) ->
1813             let _,ugraph1 = type_of_aux ~logger context ty ugraph in
1814             ((Some (C.Name n,(C.Decl ty)),k)::l,ugraph1)
1815           ) ([],ugraph) fl
1816       in
1817       let (types,kl) = List.split types_times_kl in
1818       let len = List.length types in
1819       let ugraph2 =
1820         List.fold_left
1821           (fun ugraph (name,x,ty,bo) ->
1822              let ty_bo,ugraph1 =
1823                type_of_aux ~logger (types@context) bo ugraph
1824              in
1825              let b,ugraph2 =
1826                R.are_convertible ~subst ~metasenv (types@context)
1827                  ty_bo (CicSubstitution.lift len ty) ugraph1 in
1828                if b then
1829                  begin
1830                    let (m, eaten, context') =
1831                      eat_lambdas ~subst (types @ context) (x + 1) bo
1832                    in
1833                      (*
1834                        let's control the guarded by
1835                        destructors conditions D{f,k,x,M}
1836                      *)
1837                      if not (guarded_by_destructors context' eaten
1838                                (len + eaten) kl 1 [] m) then
1839                        raise
1840                          (TypeCheckerFailure
1841                             ("Fix: not guarded by destructors"))
1842                      else
1843                        ugraph2
1844                  end
1845                else
1846                  raise (TypeCheckerFailure ("Fix: ill-typed bodies"))
1847           ) ugraph1 fl in
1848         (*CSC: controlli mancanti solo su D{f,k,x,M} *)
1849       let (_,_,ty,_) = List.nth fl i in
1850         ty,ugraph2
1851    | C.CoFix (i,fl) ->
1852        let types,ugraph1 =
1853          List.fold_left
1854            (fun (l,ugraph) (n,ty,_) ->
1855               let _,ugraph1 =
1856                 type_of_aux ~logger context ty ugraph in
1857                 (Some (C.Name n,(C.Decl ty))::l,ugraph1)
1858            ) ([],ugraph) fl
1859        in
1860        let len = List.length types in
1861        let ugraph2 =
1862          List.fold_left
1863            (fun ugraph (_,ty,bo) ->
1864               let ty_bo,ugraph1 =
1865                 type_of_aux ~logger (types @ context) bo ugraph
1866               in
1867               let b,ugraph2 =
1868                 R.are_convertible ~subst ~metasenv (types @ context) ty_bo
1869                   (CicSubstitution.lift len ty) ugraph1
1870               in
1871                 if b then
1872                   begin
1873                     (* let's control that the returned type is coinductive *)
1874                     match returns_a_coinductive context ty with
1875                         None ->
1876                           raise
1877                           (TypeCheckerFailure
1878                              ("CoFix: does not return a coinductive type"))
1879                       | Some uri ->
1880                           (*
1881                             let's control the guarded by constructors
1882                             conditions C{f,M}
1883                           *)
1884                           if not (guarded_by_constructors (types @ context)
1885                                     0 len false bo [] uri) then
1886                             raise
1887                               (TypeCheckerFailure
1888                                  ("CoFix: not guarded by constructors"))
1889                           else
1890                           ugraph2
1891                   end
1892                 else
1893                   raise
1894                     (TypeCheckerFailure ("CoFix: ill-typed bodies"))
1895            ) ugraph1 fl
1896        in
1897        let (_,ty,_) = List.nth fl i in
1898          ty,ugraph2
1899
1900  and check_exp_named_subst ~logger ?(subst = []) context ugraph =
1901    let rec check_exp_named_subst_aux ~logger esubsts l ugraph =
1902      match l with
1903          [] -> ugraph
1904        | ((uri,t) as item)::tl ->
1905            let ty_uri,ugraph1 = type_of_variable ~logger uri ugraph in
1906            let typeofvar =
1907              CicSubstitution.subst_vars esubsts ty_uri in
1908            let typeoft,ugraph2 = type_of_aux ~logger context t ugraph1 in
1909            let b,ugraph3 =
1910              CicReduction.are_convertible ~subst ~metasenv
1911                context typeoft typeofvar ugraph2
1912            in
1913              if b then
1914                check_exp_named_subst_aux ~logger (esubsts@[item]) tl ugraph3
1915              else
1916                begin
1917                  CicReduction.fdebug := 0 ;
1918                  ignore
1919                    (CicReduction.are_convertible
1920                       ~subst ~metasenv context typeoft typeofvar ugraph2) ;
1921                  fdebug := 0 ;
1922                  debug typeoft [typeofvar] ;
1923                  raise (TypeCheckerFailure "Wrong Explicit Named Substitution")
1924                end
1925    in
1926      check_exp_named_subst_aux ~logger [] ugraph
1927
1928  and sort_of_prod ?(subst = []) context (name,s) (t1, t2) ugraph =
1929   let module C = Cic in
1930    let t1' = CicReduction.whd ~subst context t1 in
1931    let t2' = CicReduction.whd ~subst ((Some (name,C.Decl s))::context) t2 in
1932    match (t1', t2') with
1933       (C.Sort s1, C.Sort s2)
1934         when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1935          (* different from Coq manual!!! *)
1936          C.Sort s2,ugraph
1937     | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1938       (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
1939        let t' = CicUniv.fresh() in
1940        let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1941        let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1942        C.Sort (C.Type t'),ugraph2
1943     | (C.Sort _,C.Sort (C.Type t1)) ->
1944         (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
1945         C.Sort (C.Type t1),ugraph (* c'e' bisogno di un fresh? *)
1946     | (C.Meta _, C.Sort _) -> t2',ugraph
1947     | (C.Meta _, (C.Meta (_,_) as t))
1948     | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
1949         t2',ugraph
1950     | (_,_) -> raise (TypeCheckerFailure (sprintf
1951         "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1')
1952           (CicPp.ppterm t2')))
1953
1954  and eat_prods ?(subst = []) context hetype l ugraph =
1955    (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
1956    (*CSC: cucinati                                                         *)
1957    match l with
1958        [] -> hetype,ugraph
1959      | (hete, hety)::tl ->
1960          (match (CicReduction.whd ~subst context hetype) with
1961               Cic.Prod (n,s,t) ->
1962                 let b,ugraph1 =
1963                   CicReduction.are_convertible
1964                     ~subst ~metasenv context hety s ugraph
1965                 in
1966                   if b then
1967                     begin
1968                       CicReduction.fdebug := -1 ;
1969                       eat_prods ~subst context
1970                         (CicSubstitution.subst hete t) tl ugraph1
1971                         (*TASSI: not sure *)
1972                     end
1973                   else
1974                     begin
1975                       CicReduction.fdebug := 0 ;
1976                       ignore (CicReduction.are_convertible
1977                                 ~subst ~metasenv context s hety ugraph) ;
1978                       fdebug := 0 ;
1979                       debug s [hety] ;
1980                       raise
1981                         (TypeCheckerFailure
1982                            (sprintf
1983                               ("Appl: wrong parameter-type, expected %s, found %s")
1984                               (CicPp.ppterm hetype) (CicPp.ppterm s)))
1985                     end
1986             | _ ->
1987                 raise (TypeCheckerFailure
1988                          "Appl: this is not a function, it cannot be applied")
1989          )
1990
1991  and returns_a_coinductive context ty =
1992   let module C = Cic in
1993    match CicReduction.whd context ty with
1994       C.MutInd (uri,i,_) ->
1995        (*CSC: definire una funzioncina per questo codice sempre replicato *)
1996         let obj,_ =
1997           try
1998             CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
1999           with Not_found -> assert false
2000         in
2001         (match obj with
2002            C.InductiveDefinition (itl,_,_,_) ->
2003             let (_,is_inductive,_,_) = List.nth itl i in
2004              if is_inductive then None else (Some uri)
2005          | _ ->
2006             raise (TypeCheckerFailure
2007               ("Unknown mutual inductive definition:" ^
2008               UriManager.string_of_uri uri))
2009         )
2010     | C.Appl ((C.MutInd (uri,i,_))::_) ->
2011        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
2012          match o with
2013            C.InductiveDefinition (itl,_,_,_) ->
2014             let (_,is_inductive,_,_) = List.nth itl i in
2015              if is_inductive then None else (Some uri)
2016          | _ ->
2017             raise (TypeCheckerFailure
2018               ("Unknown mutual inductive definition:" ^
2019               UriManager.string_of_uri uri))
2020         )
2021     | C.Prod (n,so,de) ->
2022        returns_a_coinductive ((Some (n,C.Decl so))::context) de
2023     | _ -> None
2024
2025  in
2026 (*CSC
2027 debug_print (lazy ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t)) ; flush stderr ;
2028 let res =
2029 *)
2030   type_of_aux ~logger context t ugraph
2031 (*
2032 in debug_print (lazy "FINE TYPE_OF_AUX") ; flush stderr ; res
2033 *)
2034
2035 (* is a small constructor? *)
2036 (*CSC: ottimizzare calcolando staticamente *)
2037 and is_small ~logger context paramsno c ugraph =
2038  let rec is_small_aux ~logger context c ugraph =
2039   let module C = Cic in
2040    match CicReduction.whd context c with
2041       C.Prod (n,so,de) ->
2042        (*CSC: [] is an empty metasenv. Is it correct? *)
2043        let s,ugraph1 = type_of_aux' ~logger [] context so ugraph in
2044        let b = (s = C.Sort C.Prop || s = C.Sort C.Set || s = C.Sort C.CProp) in
2045        if b then
2046          is_small_aux ~logger ((Some (n,(C.Decl so)))::context) de ugraph1
2047        else
2048          false,ugraph1
2049     | _ -> true,ugraph (*CSC: we trust the type-checker *)
2050  in
2051   let (context',dx) = split_prods context paramsno c in
2052    is_small_aux ~logger context' dx ugraph
2053
2054 and type_of ~logger t ugraph =
2055 (*CSC
2056 debug_print (lazy ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t)) ; flush stderr ;
2057 let res =
2058 *)
2059  type_of_aux' ~logger [] [] t ugraph
2060 (*CSC
2061 in debug_print (lazy "FINE TYPE_OF_AUX'") ; flush stderr ; res
2062 *)
2063 ;;
2064
2065 let typecheck_obj0 ~logger uri ugraph =
2066  let module C = Cic in
2067   function
2068      C.Constant (_,Some te,ty,_,_) ->
2069       let _,ugraph = type_of ~logger ty ugraph in
2070       let ty_te,ugraph = type_of ~logger te ugraph in
2071       let b,ugraph = (CicReduction.are_convertible [] ty_te ty ugraph) in
2072        if not b then
2073          raise (TypeCheckerFailure
2074           ("the type of the body is not the one expected"))
2075        else
2076         ugraph
2077    | C.Constant (_,None,ty,_,_) ->
2078       (* only to check that ty is well-typed *)
2079       let _,ugraph = type_of ~logger ty ugraph in
2080        ugraph
2081    | C.CurrentProof (_,conjs,te,ty,_,_) ->
2082       let _,ugraph =
2083        List.fold_left
2084         (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
2085           let _,ugraph =
2086            type_of_aux' ~logger metasenv context ty ugraph
2087           in
2088            metasenv @ [conj],ugraph
2089         ) ([],ugraph) conjs
2090       in
2091        let _,ugraph = type_of_aux' ~logger conjs [] ty ugraph in
2092        let type_of_te,ugraph =
2093         type_of_aux' ~logger conjs [] te ugraph
2094        in
2095        let b,ugraph = CicReduction.are_convertible [] type_of_te ty ugraph in
2096         if not b then
2097           raise (TypeCheckerFailure (sprintf
2098            "the current proof is not well typed because the type %s of the body is not convertible to the declared type %s"
2099            (CicPp.ppterm type_of_te) (CicPp.ppterm ty)))
2100         else
2101          ugraph
2102    | C.Variable (_,bo,ty,_,_) ->
2103       (* only to check that ty is well-typed *)
2104       let _,ugraph = type_of ~logger ty ugraph in
2105        (match bo with
2106            None -> ugraph
2107          | Some bo ->
2108             let ty_bo,ugraph = type_of ~logger bo ugraph in
2109             let b,ugraph = CicReduction.are_convertible [] ty_bo ty ugraph in
2110              if not b then
2111               raise (TypeCheckerFailure
2112                ("the body is not the one expected"))
2113              else
2114               ugraph
2115             )
2116    | (C.InductiveDefinition _ as obj) ->
2117       check_mutual_inductive_defs ~logger uri obj ugraph
2118
2119 let typecheck uri =
2120  let module C = Cic in
2121  let module R = CicReduction in
2122  let module U = UriManager in
2123  let logger = new CicLogger.logger in
2124    (* ??? match CicEnvironment.is_type_checked ~trust:true uri with ???? *)
2125    match CicEnvironment.is_type_checked ~trust:false CicUniv.empty_ugraph uri with
2126      CicEnvironment.CheckedObj (cobj,ugraph') ->
2127        (* debug_print (lazy ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri));*)
2128        cobj,ugraph'
2129    | CicEnvironment.UncheckedObj uobj ->
2130       (* let's typecheck the uncooked object *)
2131       logger#log (`Start_type_checking uri) ;
2132       (* debug_print (lazy ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri)); *)
2133       let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph uobj in
2134         try
2135           CicEnvironment.set_type_checking_info uri;
2136           logger#log (`Type_checking_completed uri);
2137           match CicEnvironment.is_type_checked ~trust:false ugraph uri with
2138               CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
2139             | _ -> raise CicEnvironmentError
2140         with
2141             (*
2142               this is raised if set_type_checking_info is called on an object
2143               that has no associated universe file. If we are in univ_maker
2144               phase this is OK since univ_maker will properly commit the
2145               object.
2146             *)
2147             Invalid_argument s ->
2148               (*debug_print (lazy s);*)
2149               uobj,ugraph
2150 ;;
2151
2152 let clean_and_fill u o g =
2153   (profiler_clean_fill (CicUnivUtils.clean_and_fill u o)) g
2154
2155 let typecheck_obj ~logger uri obj =
2156  let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph obj in
2157  let ugraph, univlist = clean_and_fill uri obj ugraph in
2158   CicEnvironment.add_type_checked_obj uri (obj,ugraph,univlist)
2159
2160 (** wrappers which instantiate fresh loggers *)
2161
2162 let type_of_aux' ?(subst = []) metasenv context t ugraph =
2163   let logger = new CicLogger.logger in
2164   type_of_aux' ~logger ~subst metasenv context t ugraph
2165
2166 let typecheck_obj uri obj =
2167  let logger = new CicLogger.logger in
2168  typecheck_obj ~logger uri obj
2169