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