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