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 = prerr_endline ;;
  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 uri ugraph 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 uri ugraph with
 184                CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
 185              | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
 186          with Invalid_argument s ->
 187            (*prerr_endline 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 uri ugraph 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 uri ugraph 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            (*prerr_endline 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 uri CicUniv.empty_ugraph 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 uri ugraph 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 uri ugraph with
 572                   CicEnvironment.CheckedObj (cobj,ugraph') -> (cobj,ugraph')
 573                 | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
 574              )
 575            with
 576                Invalid_argument s ->
 577                  (*prerr_endline 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 uri ugraph 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 CicEnvironment.is_type_checked
 605                  ~trust:false uri ugraph with
 606                      CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
 607                    | CicEnvironment.UncheckedObj _ ->
 608                        raise CicEnvironmentError)
 609             with
 610                 Invalid_argument s ->
 611                   (*prerr_endline s;*)
 612                   uobj,ugraph1_dust
 613   in
 614     match cobj with
 615         C.InductiveDefinition (dl,_,_) ->
 616           let (_,_,_,cl) = List.nth dl i in
 617           let (_,ty) = List.nth cl (j-1) in
 618             ty,ugraph1
 619       | _ ->
 620           raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
 621                                      UriManager.string_of_uri uri))
 622
 623 and recursive_args context n nn te =
 624  let module C = Cic in
 625   match CicReduction.whd context te with
 626      C.Rel _ -> []
 627    | C.Var _
 628    | C.Meta _
 629    | C.Sort _
 630    | C.Implicit _
 631    | C.Cast _ (*CSC ??? *) ->
 632       raise (AssertFailure "3") (* due to type-checking *)
 633    | C.Prod (name,so,de) ->
 634       (not (does_not_occur context n nn so)) ::
 635        (recursive_args ((Some (name,(C.Decl so)))::context) (n+1) (nn + 1) de)
 636    | C.Lambda _
 637    | C.LetIn _ ->
 638       raise (AssertFailure "4") (* due to type-checking *)
 639    | C.Appl _ -> []
 640    | C.Const _ -> raise (AssertFailure "5")
 641    | C.MutInd _
 642    | C.MutConstruct _
 643    | C.MutCase _
 644    | C.Fix _
 645    | C.CoFix _ -> raise (AssertFailure "6") (* due to type-checking *)
 646
 647 and get_new_safes ?(subst = []) context p c rl safes n nn x =
 648  let module C = Cic in
 649  let module U = UriManager in
 650  let module R = CicReduction in
 651   match (R.whd ~subst context c, R.whd ~subst context p, rl) with
 652      (C.Prod (_,so,ta1), C.Lambda (name,_,ta2), b::tl) ->
 653        (* we are sure that the two sources are convertible because we *)
 654        (* have just checked this. So let's go along ...               *)
 655        let safes' =
 656         List.map (fun x -> x + 1) safes
 657        in
 658         let safes'' =
 659          if b then 1::safes' else safes'
 660         in
 661          get_new_safes ~subst ((Some (name,(C.Decl so)))::context)
 662           ta2 ta1 tl safes'' (n+1) (nn+1) (x+1)
 663    | (C.Prod _, (C.MutConstruct _ as e), _)
 664    | (C.Prod _, (C.Rel _ as e), _)
 665    | (C.MutInd _, e, [])
 666    | (C.Appl _, e, []) -> (e,safes,n,nn,x,context)
 667    | (c,p,l) ->
 668       (* CSC: If the next exception is raised, it just means that   *)
 669       (* CSC: the proof-assistant allows to use very strange things *)
 670       (* CSC: as a branch of a case whose type is a Prod. In        *)
 671       (* CSC: particular, this means that a new (C.Prod, x,_) case  *)
 672       (* CSC: must be considered in this match. (e.g. x = MutCase)  *)
 673       raise
 674        (AssertFailure
 675          (Printf.sprintf "Get New Safes: c=%s ; p=%s"
 676            (CicPp.ppterm c) (CicPp.ppterm p)))
 677
 678 and split_prods ?(subst = []) context n te =
 679  let module C = Cic in
 680  let module R = CicReduction in
 681   match (n, R.whd context te) with
 682      (0, _) -> context,te
 683    | (n, C.Prod (name,so,ta)) when n > 0 ->
 684        split_prods ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta
 685    | (_, _) -> raise (AssertFailure "8")
 686
 687 and eat_lambdas ?(subst = []) context n te =
 688  let module C = Cic in
 689  let module R = CicReduction in
 690   match (n, R.whd ~subst context te) with
 691      (0, _) -> (te, 0, context)
 692    | (n, C.Lambda (name,so,ta)) when n > 0 ->
 693       let (te, k, context') =
 694        eat_lambdas ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta
 695       in
 696        (te, k + 1, context')
 697    | (n, te) ->
 698        raise (AssertFailure (sprintf "9 (%d, %s)" n (CicPp.ppterm te)))
 699
 700 (*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *)
 701 and check_is_really_smaller_arg ?(subst = []) context n nn kl x safes te =
 702  (*CSC: forse la whd si puo' fare solo quando serve veramente. *)
 703  (*CSC: cfr guarded_by_destructors                             *)
 704  let module C = Cic in
 705  let module U = UriManager in
 706  match CicReduction.whd context te with
 707      C.Rel m when List.mem m safes -> true
 708    | C.Rel _ -> false
 709    | C.Var _
 710    | C.Meta _
 711    | C.Sort _
 712    | C.Implicit _
 713    | C.Cast _
 714 (*   | C.Cast (te,ty) ->
 715       check_is_really_smaller_arg ~subst n nn kl x safes te &&
 716        check_is_really_smaller_arg ~subst n nn kl x safes ty*)
 717 (*   | C.Prod (_,so,ta) ->
 718       check_is_really_smaller_arg ~subst n nn kl x safes so &&
 719        check_is_really_smaller_arg ~subst (n+1) (nn+1) kl (x+1)
 720         (List.map (fun x -> x + 1) safes) ta*)
 721    | C.Prod _ -> raise (AssertFailure "10")
 722    | C.Lambda (name,so,ta) ->
 723       check_is_really_smaller_arg ~subst context n nn kl x safes so &&
 724        check_is_really_smaller_arg ~subst ((Some (name,(C.Decl so)))::context)
 725         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 726    | C.LetIn (name,so,ta) ->
 727       check_is_really_smaller_arg ~subst context n nn kl x safes so &&
 728        check_is_really_smaller_arg ~subst ((Some (name,(C.Def (so,None))))::context)
 729         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 730    | C.Appl (he::_) ->
 731       (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
 732       (*CSC: solo perche' non abbiamo trovato controesempi            *)
 733       check_is_really_smaller_arg ~subst context n nn kl x safes he
 734    | C.Appl [] -> raise (AssertFailure "11")
 735    | C.Const _
 736    | C.MutInd _ -> raise (AssertFailure "12")
 737    | C.MutConstruct _ -> false
 738    | C.MutCase (uri,i,outtype,term,pl) ->
 739       (match term with
 740           C.Rel m when List.mem m safes || m = x ->
 741            let (tys,len,isinductive,paramsno,cl) =
 742             let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
 743             match o with
 744                C.InductiveDefinition (tl,_,paramsno) ->
 745                 let tys =
 746                  List.map
 747                   (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl
 748                 in
 749                  let (_,isinductive,_,cl) = List.nth tl i in
 750                   let cl' =
 751                    List.map
 752                     (fun (id,ty) ->
 753                       (id, snd (split_prods ~subst tys paramsno ty))) cl
 754                   in
 755                    (tys,List.length tl,isinductive,paramsno,cl')
 756              | _ ->
 757                 raise (TypeCheckerFailure
 758                   ("Unknown mutual inductive definition:" ^
 759                   UriManager.string_of_uri uri))
 760            in
 761             if not isinductive then
 762               List.fold_right
 763                (fun p i ->
 764                  i && check_is_really_smaller_arg ~subst context n nn kl x safes p)
 765                pl true
 766             else
 767               List.fold_right
 768                (fun (p,(_,c)) i ->
 769                  let rl' =
 770                   let debrujinedte = debrujin_constructor uri len c in
 771                    recursive_args tys 0 len debrujinedte
 772                  in
 773                   let (e,safes',n',nn',x',context') =
 774                    get_new_safes ~subst context p c rl' safes n nn x
 775                   in
 776                    i &&
 777                    check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
 778                ) (List.combine pl cl) true
 779         | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
 780            let (tys,len,isinductive,paramsno,cl) =
 781             let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
 782             match o with
 783                C.InductiveDefinition (tl,_,paramsno) ->
 784                 let (_,isinductive,_,cl) = List.nth tl i in
 785                  let tys =
 786                   List.map (fun (n,_,ty,_) ->
 787                    Some(Cic.Name n,(Cic.Decl ty))) tl
 788                  in
 789                   let cl' =
 790                    List.map
 791                     (fun (id,ty) ->
 792                       (id, snd (split_prods ~subst tys paramsno ty))) cl
 793                   in
 794                    (tys,List.length tl,isinductive,paramsno,cl')
 795              | _ ->
 796                 raise (TypeCheckerFailure
 797                   ("Unknown mutual inductive definition:" ^
 798                   UriManager.string_of_uri uri))
 799            in
 800             if not isinductive then
 801               List.fold_right
 802                (fun p i ->
 803                  i && check_is_really_smaller_arg ~subst context n nn kl x safes p)
 804                pl true
 805             else
 806               (*CSC: supponiamo come prima che nessun controllo sia necessario*)
 807               (*CSC: sugli argomenti di una applicazione                      *)
 808               List.fold_right
 809                (fun (p,(_,c)) i ->
 810                  let rl' =
 811                   let debrujinedte = debrujin_constructor uri len c in
 812                    recursive_args tys 0 len debrujinedte
 813                  in
 814                   let (e, safes',n',nn',x',context') =
 815                    get_new_safes context p c rl' safes n nn x
 816                   in
 817                    i &&
 818                    check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
 819                ) (List.combine pl cl) true
 820         | _ ->
 821           List.fold_right
 822            (fun p i ->
 823              i && check_is_really_smaller_arg ~subst context n nn kl x safes p
 824            ) pl true
 825       )
 826    | C.Fix (_, fl) ->
 827       let len = List.length fl in
 828        let n_plus_len = n + len
 829        and nn_plus_len = nn + len
 830        and x_plus_len = x + len
 831        and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
 832        and safes' = List.map (fun x -> x + len) safes in
 833         List.fold_right
 834          (fun (_,_,ty,bo) i ->
 835            i &&
 836             check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl
 837              x_plus_len safes' bo
 838          ) fl true
 839    | C.CoFix (_, fl) ->
 840       let len = List.length fl in
 841        let n_plus_len = n + len
 842        and nn_plus_len = nn + len
 843        and x_plus_len = x + len
 844        and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
 845        and safes' = List.map (fun x -> x + len) safes in
 846         List.fold_right
 847          (fun (_,ty,bo) i ->
 848            i &&
 849             check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl
 850              x_plus_len safes' bo
 851          ) fl true
 852
 853 and guarded_by_destructors ?(subst = []) context n nn kl x safes =
 854  let module C = Cic in
 855  let module U = UriManager in
 856   function
 857      C.Rel m when m > n && m <= nn -> false
 858    | C.Rel m ->
 859       (match List.nth context (n-1) with
 860           Some (_,C.Decl _) -> true
 861         | Some (_,C.Def (bo,_)) ->
 862            guarded_by_destructors context m nn kl x safes
 863             (CicSubstitution.lift m bo)
 864         | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
 865       )
 866    | C.Meta _
 867    | C.Sort _
 868    | C.Implicit _ -> true
 869    | C.Cast (te,ty) ->
 870       guarded_by_destructors context n nn kl x safes te &&
 871        guarded_by_destructors context n nn kl x safes ty
 872    | C.Prod (name,so,ta) ->
 873       guarded_by_destructors context n nn kl x safes so &&
 874        guarded_by_destructors ((Some (name,(C.Decl so)))::context)
 875         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 876    | C.Lambda (name,so,ta) ->
 877       guarded_by_destructors context n nn kl x safes so &&
 878        guarded_by_destructors ((Some (name,(C.Decl so)))::context)
 879         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 880    | C.LetIn (name,so,ta) ->
 881       guarded_by_destructors context n nn kl x safes so &&
 882        guarded_by_destructors ((Some (name,(C.Def (so,None))))::context)
 883         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 884    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
 885       let k = List.nth kl (m - n - 1) in
 886        if not (List.length tl > k) then false
 887        else
 888         List.fold_right
 889          (fun param i ->
 890            i && guarded_by_destructors context n nn kl x safes param
 891          ) tl true &&
 892          check_is_really_smaller_arg ~subst context n nn kl x safes (List.nth tl k)
 893    | C.Appl tl ->
 894       List.fold_right
 895        (fun t i -> i && guarded_by_destructors context n nn kl x safes t)
 896        tl true
 897    | C.Var (_,exp_named_subst)
 898    | C.Const (_,exp_named_subst)
 899    | C.MutInd (_,_,exp_named_subst)
 900    | C.MutConstruct (_,_,_,exp_named_subst) ->
 901       List.fold_right
 902        (fun (_,t) i -> i && guarded_by_destructors context n nn kl x safes t)
 903        exp_named_subst true
 904    | C.MutCase (uri,i,outtype,term,pl) ->
 905       (match term with
 906           C.Rel m when List.mem m safes || m = x ->
 907            let (tys,len,isinductive,paramsno,cl) =
 908             let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
 909             match o with
 910                C.InductiveDefinition (tl,_,paramsno) ->
 911                 let len = List.length tl in
 912                  let (_,isinductive,_,cl) = List.nth tl i in
 913                   let tys =
 914                    List.map (fun (n,_,ty,_) ->
 915                     Some(Cic.Name n,(Cic.Decl ty))) tl
 916                   in
 917                    let cl' =
 918                     List.map
 919                      (fun (id,ty) ->
 920                       let debrujinedty = debrujin_constructor uri len ty in
 921                        (id, snd (split_prods ~subst tys paramsno ty),
 922                         snd (split_prods ~subst tys paramsno debrujinedty)
 923                        )) cl
 924                    in
 925                     (tys,len,isinductive,paramsno,cl')
 926              | _ ->
 927                 raise (TypeCheckerFailure
 928                   ("Unknown mutual inductive definition:" ^
 929                   UriManager.string_of_uri uri))
 930            in
 931             if not isinductive then
 932              guarded_by_destructors context n nn kl x safes outtype &&
 933               guarded_by_destructors context n nn kl x safes term &&
 934               (*CSC: manca ??? il controllo sul tipo di term? *)
 935               List.fold_right
 936                (fun p i ->
 937                  i && guarded_by_destructors context n nn kl x safes p)
 938                pl true
 939             else
 940              guarded_by_destructors context n nn kl x safes outtype &&
 941               (*CSC: manca ??? il controllo sul tipo di term? *)
 942               List.fold_right
 943                (fun (p,(_,c,brujinedc)) i ->
 944                  let rl' = recursive_args tys 0 len brujinedc in
 945                   let (e,safes',n',nn',x',context') =
 946                    get_new_safes context p c rl' safes n nn x
 947                   in
 948                    i &&
 949                    guarded_by_destructors context' n' nn' kl x' safes' e
 950                ) (List.combine pl cl) true
 951         | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
 952            let (tys,len,isinductive,paramsno,cl) =
 953             let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
 954             match o with
 955                C.InductiveDefinition (tl,_,paramsno) ->
 956                 let (_,isinductive,_,cl) = List.nth tl i in
 957                  let tys =
 958                   List.map
 959                    (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
 960                  in
 961                   let cl' =
 962                    List.map
 963                     (fun (id,ty) ->
 964                       (id, snd (split_prods ~subst tys paramsno ty))) cl
 965                   in
 966                    (tys,List.length tl,isinductive,paramsno,cl')
 967              | _ ->
 968                 raise (TypeCheckerFailure
 969                   ("Unknown mutual inductive definition:" ^
 970                   UriManager.string_of_uri uri))
 971            in
 972             if not isinductive then
 973              guarded_by_destructors context n nn kl x safes outtype &&
 974               guarded_by_destructors context n nn kl x safes term &&
 975               (*CSC: manca ??? il controllo sul tipo di term? *)
 976               List.fold_right
 977                (fun p i ->
 978                  i && guarded_by_destructors context n nn kl x safes p)
 979                pl true
 980             else
 981              guarded_by_destructors context n nn kl x safes outtype &&
 982               (*CSC: manca ??? il controllo sul tipo di term? *)
 983               List.fold_right
 984                (fun t i ->
 985                  i && guarded_by_destructors context n nn kl x safes t)
 986                tl true &&
 987               List.fold_right
 988                (fun (p,(_,c)) i ->
 989                  let rl' =
 990                   let debrujinedte = debrujin_constructor uri len c in
 991                    recursive_args tys 0 len debrujinedte
 992                  in
 993                   let (e, safes',n',nn',x',context') =
 994                    get_new_safes context p c rl' safes n nn x
 995                   in
 996                    i &&
 997                    guarded_by_destructors context' n' nn' kl x' safes' e
 998                ) (List.combine pl cl) true
 999         | _ ->
1000           guarded_by_destructors context n nn kl x safes outtype &&
1001            guarded_by_destructors context n nn kl x safes term &&
1002            (*CSC: manca ??? il controllo sul tipo di term? *)
1003            List.fold_right
1004             (fun p i -> i && guarded_by_destructors context n nn kl x safes p)
1005             pl true
1006       )
1007    | C.Fix (_, fl) ->
1008       let len = List.length fl in
1009        let n_plus_len = n + len
1010        and nn_plus_len = nn + len
1011        and x_plus_len = x + len
1012        and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
1013        and safes' = List.map (fun x -> x + len) safes in
1014         List.fold_right
1015          (fun (_,_,ty,bo) i ->
1016            i && guarded_by_destructors context n nn kl x_plus_len safes' ty &&
1017             guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
1018              x_plus_len safes' bo
1019          ) fl true
1020    | C.CoFix (_, fl) ->
1021       let len = List.length fl in
1022        let n_plus_len = n + len
1023        and nn_plus_len = nn + len
1024        and x_plus_len = x + len
1025        and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
1026        and safes' = List.map (fun x -> x + len) safes in
1027         List.fold_right
1028          (fun (_,ty,bo) i ->
1029            i &&
1030             guarded_by_destructors context n nn kl x_plus_len safes' ty &&
1031             guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
1032              x_plus_len safes' bo
1033          ) fl true
1034
1035 (* the boolean h means already protected *)
1036 (* args is the list of arguments the type of the constructor that may be *)
1037 (* found in head position must be applied to.                            *)
1038 (*CSC: coInductiveTypeURI non cambia mai di ricorsione in ricorsione *)
1039 and guarded_by_constructors context n nn h te args coInductiveTypeURI =
1040  let module C = Cic in
1041   (*CSC: There is a lot of code replication between the cases X and    *)
1042   (*CSC: (C.Appl X tl). Maybe it will be better to define a function   *)
1043   (*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *)
1044   match CicReduction.whd context te with
1045      C.Rel m when m > n && m <= nn -> h
1046    | C.Rel _ -> true
1047    | C.Meta _
1048    | C.Sort _
1049    | C.Implicit _
1050    | C.Cast _
1051    | C.Prod _
1052    | C.LetIn _ ->
1053       (* the term has just been type-checked *)
1054       raise (AssertFailure "17")
1055    | C.Lambda (name,so,de) ->
1056       does_not_occur context n nn so &&
1057        guarded_by_constructors ((Some (name,(C.Decl so)))::context)
1058         (n + 1) (nn + 1) h de args coInductiveTypeURI
1059    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
1060       h &&
1061        List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
1062    | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) ->
1063       let consty =
1064         let obj,_ =
1065           try
1066             CicEnvironment.get_cooked_obj ~trust:false uri CicUniv.empty_ugraph
1067           with Not_found -> assert false
1068         in
1069        match obj with
1070           C.InductiveDefinition (itl,_,_) ->
1071            let (_,_,_,cl) = List.nth itl i in
1072             let (_,cons) = List.nth cl (j - 1) in
1073              CicSubstitution.subst_vars exp_named_subst cons
1074         | _ ->
1075             raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1076               UriManager.string_of_uri uri))
1077       in
1078        let rec analyse_branch context ty te =
1079         match CicReduction.whd context ty with
1080            C.Meta _ -> raise (AssertFailure "34")
1081          | C.Rel _
1082          | C.Var _
1083          | C.Sort _ ->
1084             does_not_occur context n nn te
1085          | C.Implicit _
1086          | C.Cast _ ->
1087             raise (AssertFailure "24")(* due to type-checking *)
1088          | C.Prod (name,so,de) ->
1089             analyse_branch ((Some (name,(C.Decl so)))::context) de te
1090          | C.Lambda _
1091          | C.LetIn _ ->
1092             raise (AssertFailure "25")(* due to type-checking *)
1093          | C.Appl ((C.MutInd (uri,_,_))::_) as ty
1094             when uri == coInductiveTypeURI ->
1095              guarded_by_constructors context n nn true te [] coInductiveTypeURI
1096          | C.Appl ((C.MutInd (uri,_,_))::_) as ty ->
1097             guarded_by_constructors context n nn true te tl coInductiveTypeURI
1098          | C.Appl _ ->
1099             does_not_occur context n nn te
1100          | C.Const _ -> raise (AssertFailure "26")
1101          | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
1102             guarded_by_constructors context n nn true te [] coInductiveTypeURI
1103          | C.MutInd _ ->
1104             does_not_occur context n nn te
1105          | C.MutConstruct _ -> raise (AssertFailure "27")
1106          (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
1107          (*CSC: in head position.                                       *)
1108          | C.MutCase _
1109          | C.Fix _
1110          | C.CoFix _ ->
1111             raise (AssertFailure "28")(* due to type-checking *)
1112        in
1113        let rec analyse_instantiated_type context ty l =
1114         match CicReduction.whd context ty with
1115            C.Rel _
1116          | C.Var _
1117          | C.Meta _
1118          | C.Sort _
1119          | C.Implicit _
1120          | C.Cast _ -> raise (AssertFailure "29")(* due to type-checking *)
1121          | C.Prod (name,so,de) ->
1122             begin
1123              match l with
1124                 [] -> true
1125               | he::tl ->
1126                  analyse_branch context so he &&
1127                   analyse_instantiated_type
1128                    ((Some (name,(C.Decl so)))::context) de tl
1129             end
1130          | C.Lambda _
1131          | C.LetIn _ ->
1132             raise (AssertFailure "30")(* due to type-checking *)
1133          | C.Appl _ ->
1134             List.fold_left
1135              (fun i x -> i && does_not_occur context n nn x) true l
1136          | C.Const _ -> raise (AssertFailure "31")
1137          | C.MutInd _ ->
1138             List.fold_left
1139              (fun i x -> i && does_not_occur context n nn x) true l
1140          | C.MutConstruct _ -> raise (AssertFailure "32")
1141          (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
1142          (*CSC: in head position.                                       *)
1143          | C.MutCase _
1144          | C.Fix _
1145          | C.CoFix _ ->
1146             raise (AssertFailure "33")(* due to type-checking *)
1147        in
1148         let rec instantiate_type args consty =
1149          function
1150             [] -> true
1151           | tlhe::tltl as l ->
1152              let consty' = CicReduction.whd context consty in
1153               match args with
1154                  he::tl ->
1155                   begin
1156                    match consty' with
1157                       C.Prod (_,_,de) ->
1158                        let instantiated_de = CicSubstitution.subst he de in
1159                         (*CSC: siamo sicuri che non sia troppo forte? *)
1160                         does_not_occur context n nn tlhe &
1161                          instantiate_type tl instantiated_de tltl
1162                     | _ ->
1163                       (*CSC:We do not consider backbones with a MutCase, a    *)
1164                       (*CSC:FixPoint, a CoFixPoint and so on in head position.*)
1165                       raise (AssertFailure "23")
1166                   end
1167                | [] -> analyse_instantiated_type context consty' l
1168                   (* These are all the other cases *)
1169        in
1170         instantiate_type args consty tl
1171    | C.Appl ((C.CoFix (_,fl))::tl) ->
1172       List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
1173        let len = List.length fl in
1174         let n_plus_len = n + len
1175         and nn_plus_len = nn + len
1176         (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1177         and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1178          List.fold_right
1179           (fun (_,ty,bo) i ->
1180             i && does_not_occur context n nn ty &&
1181              guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1182               args coInductiveTypeURI
1183           ) fl true
1184    | C.Appl ((C.MutCase (_,_,out,te,pl))::tl) ->
1185        List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
1186         does_not_occur context n nn out &&
1187          does_not_occur context n nn te &&
1188           List.fold_right
1189            (fun x i ->
1190              i &&
1191              guarded_by_constructors context n nn h x args coInductiveTypeURI
1192            ) pl true
1193    | C.Appl l ->
1194       List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
1195    | C.Var (_,exp_named_subst)
1196    | C.Const (_,exp_named_subst) ->
1197       List.fold_right
1198        (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
1199    | C.MutInd _ -> assert false
1200    | C.MutConstruct (_,_,_,exp_named_subst) ->
1201       List.fold_right
1202        (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
1203    | C.MutCase (_,_,out,te,pl) ->
1204        does_not_occur context n nn out &&
1205         does_not_occur context n nn te &&
1206          List.fold_right
1207           (fun x i ->
1208             i &&
1209              guarded_by_constructors context n nn h x args coInductiveTypeURI
1210           ) pl true
1211    | C.Fix (_,fl) ->
1212       let len = List.length fl in
1213        let n_plus_len = n + len
1214        and nn_plus_len = nn + len
1215        (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1216        and tys = List.map (fun (n,_,ty,_)-> Some (C.Name n,(C.Decl ty))) fl in
1217         List.fold_right
1218          (fun (_,_,ty,bo) i ->
1219            i && does_not_occur context n nn ty &&
1220             does_not_occur (tys@context) n_plus_len nn_plus_len bo
1221          ) fl true
1222    | C.CoFix (_,fl) ->
1223       let len = List.length fl in
1224        let n_plus_len = n + len
1225        and nn_plus_len = nn + len
1226        (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1227        and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1228         List.fold_right
1229          (fun (_,ty,bo) i ->
1230            i && does_not_occur context n nn ty &&
1231             guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1232              args coInductiveTypeURI
1233          ) fl true
1234
1235 and check_allowed_sort_elimination ~logger context uri i need_dummy ind
1236   arity1 arity2 ugraph =
1237  let module C = Cic in
1238  let module U = UriManager in
1239   match (CicReduction.whd context arity1, CicReduction.whd context arity2) with
1240      (C.Prod (_,so1,de1), C.Prod (_,so2,de2)) ->
1241        let b,ugraph1 = CicReduction.are_convertible context so1 so2 ugraph in
1242        if b then
1243          check_allowed_sort_elimination ~logger context uri i need_dummy
1244            (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2 ugraph1
1245        else
1246          false,ugraph1
1247    | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true,ugraph
1248    | (C.Sort C.Prop, C.Sort C.Set)
1249    | (C.Sort C.Prop, C.Sort C.CProp)
1250    | (C.Sort C.Prop, C.Sort (C.Type _) ) when need_dummy ->
1251    (* TASSI: da verificare *)
1252 (*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *)
1253        (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
1254          match o with
1255          C.InductiveDefinition (itl,_,_) ->
1256            let (_,_,_,cl) = List.nth itl i in
1257            (* is a singleton definition or the empty proposition? *)
1258            (List.length cl = 1 || List.length cl = 0) , ugraph
1259          | _ ->
1260              raise (TypeCheckerFailure
1261                       ("Unknown mutual inductive definition:" ^
1262                        UriManager.string_of_uri uri))
1263        )
1264    | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true , ugraph
1265    | (C.Sort C.CProp, C.Sort C.Prop) when need_dummy -> true , ugraph
1266    | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true , ugraph
1267    | (C.Sort C.Set, C.Sort C.CProp) when need_dummy -> true , ugraph
1268    | (C.Sort C.CProp, C.Sort C.Set) when need_dummy -> true , ugraph
1269    | (C.Sort C.CProp, C.Sort C.CProp) when need_dummy -> true , ugraph
1270    | ((C.Sort C.Set, C.Sort (C.Type _)) | (C.Sort C.CProp, C.Sort (C.Type _)))
1271       (* TASSI: da verificare *)
1272       when need_dummy ->
1273        (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
1274          match o with
1275            C.InductiveDefinition (itl,_,paramsno) ->
1276             let tys =
1277              List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1278             in
1279              let (_,_,_,cl) = List.nth itl i in
1280               (List.fold_right
1281                (fun (_,x) (i,ugraph) ->
1282                  if i then
1283                    is_small ~logger tys paramsno x ugraph
1284                  else
1285                    false,ugraph
1286                     ) cl (true,ugraph))
1287            | _ ->
1288             raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1289               UriManager.string_of_uri uri))
1290        )
1291    | (C.Sort (C.Type _), C.Sort _) when need_dummy -> true , ugraph
1292      (* TASSI: da verificare *)
1293    | (C.Sort C.Prop, C.Prod (name,so,ta)) when not need_dummy ->
1294        let b,ugraph1 = CicReduction.are_convertible context so ind ugraph in
1295        if not b then
1296          false,ugraph1
1297        else
1298          (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1299            C.Sort C.Prop -> true,ugraph1
1300          | (C.Sort C.Set | C.Sort C.CProp) ->
1301              (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
1302                match o with
1303                C.InductiveDefinition (itl,_,_) ->
1304                    let (_,_,_,cl) = List.nth itl i in
1305                    (* is a singleton definition? *)
1306                    List.length cl = 1,ugraph1
1307              | _ ->
1308                  raise (TypeCheckerFailure
1309                           ("Unknown mutual inductive definition:" ^
1310                            UriManager.string_of_uri uri))
1311              )
1312          | _ -> false,ugraph1
1313          )
1314    | ((C.Sort C.Set, C.Prod (name,so,ta))
1315    | (C.Sort C.CProp, C.Prod (name,so,ta)))
1316      when not need_dummy ->
1317        let b,ugraph1 = CicReduction.are_convertible context so ind ugraph in
1318        if not b then
1319          false,ugraph1
1320        else
1321          (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1322            C.Sort C.Prop
1323          | C.Sort C.Set  -> true,ugraph1
1324          | C.Sort C.CProp -> true,ugraph1
1325          | C.Sort (C.Type _) ->
1326              (* TASSI: da verificare *)
1327              (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
1328                match o with
1329                C.InductiveDefinition (itl,_,paramsno) ->
1330                  let (_,_,_,cl) = List.nth itl i in
1331                  let tys =
1332                    List.map
1333                      (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1334                  in
1335                  (List.fold_right
1336                    (fun (_,x) (i,ugraph) ->
1337                       if i then
1338                         is_small ~logger tys paramsno x ugraph
1339                       else
1340                         false,ugraph
1341                    ) cl (true,ugraph1))
1342              | _ ->
1343                  raise (TypeCheckerFailure
1344                           ("Unknown mutual inductive definition:" ^
1345                            UriManager.string_of_uri uri))
1346              )
1347          | _ -> raise (AssertFailure "19")
1348          )
1349    | (C.Sort (C.Type _), C.Prod (_,so,_)) when not need_dummy ->
1350        (* TASSI: da verificare *)
1351        CicReduction.are_convertible context so ind ugraph
1352    | (_,_) -> false,ugraph
1353
1354 and type_of_branch context argsno need_dummy outtype term constype =
1355  let module C = Cic in
1356  let module R = CicReduction in
1357   match R.whd context constype with
1358      C.MutInd (_,_,_) ->
1359       if need_dummy then
1360        outtype
1361       else
1362        C.Appl [outtype ; term]
1363    | C.Appl (C.MutInd (_,_,_)::tl) ->
1364       let (_,arguments) = split tl argsno
1365       in
1366        if need_dummy && arguments = [] then
1367         outtype
1368        else
1369         C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
1370    | C.Prod (name,so,de) ->
1371       let term' =
1372        match CicSubstitution.lift 1 term with
1373           C.Appl l -> C.Appl (l@[C.Rel 1])
1374         | t -> C.Appl [t ; C.Rel 1]
1375       in
1376        C.Prod (C.Anonymous,so,type_of_branch
1377         ((Some (name,(C.Decl so)))::context) argsno need_dummy
1378         (CicSubstitution.lift 1 outtype) term' de)
1379   | _ -> raise (AssertFailure "20")
1380
1381 (* check_metasenv_consistency checks that the "canonical" context of a
1382 metavariable is consitent - up to relocation via the relocation list l -
1383 with the actual context *)
1384
1385
1386 and check_metasenv_consistency ~logger ?(subst=[]) metasenv context
1387   canonical_context l ugraph
1388 =
1389   let module C = Cic in
1390   let module R = CicReduction in
1391   let module S = CicSubstitution in
1392   let lifted_canonical_context =
1393     let rec aux i =
1394      function
1395          [] -> []
1396        | (Some (n,C.Decl t))::tl ->
1397            (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
1398        | (Some (n,C.Def (t,None)))::tl ->
1399            (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
1400        | None::tl -> None::(aux (i+1) tl)
1401        | (Some (n,C.Def (t,Some ty)))::tl ->
1402            (Some (n,C.Def ((S.lift_meta l (S.lift i t)),Some (S.lift_meta l (S.lift i ty)))))::(aux (i+1) tl)
1403     in
1404      aux 1 canonical_context
1405    in
1406    List.fold_left2
1407      (fun ugraph t ct ->
1408        match (t,ct) with
1409        | _,None -> ugraph
1410        | Some t,Some (_,C.Def (ct,_)) ->
1411            let b,ugraph1 =
1412              R.are_convertible ~subst ~metasenv context t ct ugraph
1413            in
1414            if not b then
1415              raise
1416                (TypeCheckerFailure
1417                   (sprintf "Not well typed metavariable local context: expected a term convertible with %s, found %s" (CicPp.ppterm ct) (CicPp.ppterm t)))
1418            else
1419              ugraph1
1420        | Some t,Some (_,C.Decl ct) ->
1421            let type_t,ugraph1 =
1422              type_of_aux' ~logger ~subst metasenv context t ugraph
1423            in
1424            let b,ugraph2 =
1425              R.are_convertible ~subst ~metasenv context type_t ct ugraph1
1426            in
1427            if not b then
1428              raise (TypeCheckerFailure
1429                       (sprintf "Not well typed metavariable local context: expected a term of type %s, found %s of type %s"
1430                          (CicPp.ppterm ct) (CicPp.ppterm t)
1431                          (CicPp.ppterm type_t)))
1432            else
1433              ugraph2
1434        | None, _  ->
1435            raise (TypeCheckerFailure
1436                     ("Not well typed metavariable local context: "^
1437                      "an hypothesis, that is not hidden, is not instantiated"))
1438      ) ugraph l lifted_canonical_context
1439
1440
1441 (*
1442    type_of_aux' is just another name (with a different scope)
1443    for type_of_aux
1444 *)
1445
1446 and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
1447  let rec type_of_aux ~logger context t ugraph =
1448   let module C = Cic in
1449   let module R = CicReduction in
1450   let module S = CicSubstitution in
1451   let module U = UriManager in
1452    match t with
1453       C.Rel n ->
1454        (try
1455          match List.nth context (n - 1) with
1456             Some (_,C.Decl t) -> S.lift n t,ugraph
1457           | Some (_,C.Def (_,Some ty)) -> S.lift n ty,ugraph
1458           | Some (_,C.Def (bo,None)) ->
1459              debug_print "##### CASO DA INVESTIGARE E CAPIRE" ;
1460               type_of_aux ~logger context (S.lift n bo) ugraph
1461           | None -> raise
1462               (TypeCheckerFailure "Reference to deleted hypothesis")
1463         with
1464         _ ->
1465           raise (TypeCheckerFailure "unbound variable")
1466        )
1467     | C.Var (uri,exp_named_subst) ->
1468       incr fdebug ;
1469         let ugraph1 =
1470           check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
1471         in
1472         let ty,ugraph2 = type_of_variable ~logger uri ugraph1 in
1473         let ty1 = CicSubstitution.subst_vars exp_named_subst ty in
1474           decr fdebug ;
1475           ty1,ugraph2
1476     | C.Meta (n,l) ->
1477        (try
1478           let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in
1479           let ugraph1 =
1480             check_metasenv_consistency ~logger
1481               ~subst metasenv context canonical_context l ugraph
1482           in
1483             (* assuming subst is well typed !!!!! *)
1484             ((CicSubstitution.lift_meta l ty), ugraph1)
1485               (* type_of_aux context (CicSubstitution.lift_meta l term) *)
1486         with CicUtil.Subst_not_found _ ->
1487           let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
1488           let ugraph1 =
1489             check_metasenv_consistency ~logger
1490               ~subst metasenv context canonical_context l ugraph
1491           in
1492             ((CicSubstitution.lift_meta l ty),ugraph1))
1493       (* TASSI: CONSTRAINTS *)
1494     | C.Sort (C.Type t) ->
1495        let t' = CicUniv.fresh() in
1496        let ugraph1 = CicUniv.add_gt t' t ugraph in
1497          (C.Sort (C.Type t')),ugraph1
1498       (* TASSI: CONSTRAINTS *)
1499     | C.Sort s -> (C.Sort (C.Type (CicUniv.fresh ()))),ugraph
1500     | C.Implicit _ -> raise (AssertFailure "21")
1501     | C.Cast (te,ty) as t ->
1502        let _,ugraph1 = type_of_aux ~logger context ty ugraph in
1503        let ty_te,ugraph2 = type_of_aux ~logger context te ugraph1 in
1504        let b,ugraph3 =
1505          R.are_convertible ~subst ~metasenv context ty_te ty ugraph2
1506        in
1507          if b then
1508            ty,ugraph3
1509          else
1510            raise (TypeCheckerFailure
1511                     (sprintf "Invalid cast %s" (CicPp.ppterm t)))
1512     | C.Prod (name,s,t) ->
1513        let sort1,ugraph1 = type_of_aux ~logger context s ugraph in
1514        let sort2,ugraph2 =
1515          type_of_aux ~logger  ((Some (name,(C.Decl s)))::context) t ugraph1
1516        in
1517        sort_of_prod ~subst context (name,s) (sort1,sort2) ugraph2
1518    | C.Lambda (n,s,t) ->
1519        let sort1,ugraph1 = type_of_aux ~logger context s ugraph in
1520        (match R.whd ~subst context sort1 with
1521            C.Meta _
1522          | C.Sort _ -> ()
1523          | _ ->
1524            raise
1525             (TypeCheckerFailure (sprintf
1526               "Not well-typed lambda-abstraction: the source %s should be a type; instead it is a term of type %s" (CicPp.ppterm s)
1527                 (CicPp.ppterm sort1)))
1528        ) ;
1529        let type2,ugraph2 =
1530          type_of_aux ~logger ((Some (n,(C.Decl s)))::context) t ugraph1
1531        in
1532          (C.Prod (n,s,type2)),ugraph2
1533    | C.LetIn (n,s,t) ->
1534       (* only to check if s is well-typed *)
1535       let ty,ugraph1 = type_of_aux ~logger context s ugraph in
1536        (* The type of a LetIn is a LetIn. Extremely slow since the computed
1537           LetIn is later reduced and maybe also re-checked.
1538        (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t))
1539        *)
1540        (* The type of the LetIn is reduced. Much faster than the previous
1541           solution. Moreover the inferred type is probably very different
1542           from the expected one.
1543        (CicReduction.whd context
1544         (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)))
1545        *)
1546        (* One-step LetIn reduction. Even faster than the previous solution.
1547           Moreover the inferred type is closer to the expected one. *)
1548        let ty1,ugraph2 =
1549          type_of_aux ~logger
1550            ((Some (n,(C.Def (s,Some ty))))::context) t ugraph1
1551        in
1552        (CicSubstitution.subst s ty1),ugraph2
1553    | C.Appl (he::tl) when List.length tl > 0 ->
1554        let hetype,ugraph1 = type_of_aux ~logger context he ugraph in
1555        let tlbody_and_type,ugraph2 =
1556          List.fold_right (
1557            fun x (l,ugraph) ->
1558              let ty,ugraph1 = type_of_aux ~logger context x ugraph in
1559              let _,ugraph1 = type_of_aux ~logger  context ty ugraph1 in
1560                ((x,ty)::l,ugraph1))
1561            tl ([],ugraph1)
1562        in
1563          (* TASSI: questa c'era nel mio... ma non nel CVS... *)
1564          (* let _,ugraph2 = type_of_aux context hetype ugraph2 in *)
1565          eat_prods ~subst context hetype tlbody_and_type ugraph2
1566    | C.Appl _ -> raise (AssertFailure "Appl: no arguments")
1567    | C.Const (uri,exp_named_subst) ->
1568        incr fdebug ;
1569        let ugraph1 =
1570          check_exp_named_subst ~logger ~subst  context exp_named_subst ugraph
1571        in
1572        let cty,ugraph2 = type_of_constant ~logger uri ugraph1 in
1573        let cty1 =
1574          CicSubstitution.subst_vars exp_named_subst cty
1575        in
1576          decr fdebug ;
1577          cty1,ugraph2
1578    | C.MutInd (uri,i,exp_named_subst) ->
1579       incr fdebug ;
1580        let ugraph1 =
1581          check_exp_named_subst ~logger  ~subst context exp_named_subst ugraph
1582        in
1583          (* TASSI: da me c'era anche questa, ma in CVS no *)
1584        let mty,ugraph2 = type_of_mutual_inductive_defs ~logger uri i ugraph1 in
1585          (* fine parte dubbia *)
1586        let cty =
1587          CicSubstitution.subst_vars exp_named_subst mty
1588        in
1589          decr fdebug ;
1590          cty,ugraph2
1591    | C.MutConstruct (uri,i,j,exp_named_subst) ->
1592        let ugraph1 =
1593          check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
1594        in
1595          (* TASSI: idem come sopra *)
1596        let mty,ugraph2 =
1597          type_of_mutual_inductive_constr ~logger uri i j ugraph1
1598        in
1599        let cty =
1600          CicSubstitution.subst_vars exp_named_subst mty
1601        in
1602          cty,ugraph2
1603    | C.MutCase (uri,i,outtype,term,pl) ->
1604       let outsort,ugraph1 = type_of_aux ~logger context outtype ugraph in
1605       let (need_dummy, k) =
1606       let rec guess_args context t =
1607         let outtype = CicReduction.whd ~subst context t in
1608           match outtype with
1609               C.Sort _ -> (true, 0)
1610             | C.Prod (name, s, t) ->
1611                 let (b, n) =
1612                   guess_args ((Some (name,(C.Decl s)))::context) t in
1613                   if n = 0 then
1614                   (* last prod before sort *)
1615                     match CicReduction.whd ~subst context s with
1616 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1617                         C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
1618                           (false, 1)
1619 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1620                       | C.Appl ((C.MutInd (uri',i',_)) :: _)
1621                           when U.eq uri' uri && i' = i -> (false, 1)
1622                       | _ -> (true, 1)
1623                   else
1624                     (b, n + 1)
1625             | _ ->
1626                 raise
1627                   (TypeCheckerFailure
1628                      (sprintf
1629                         "Malformed case analasys' output type %s"
1630                         (CicPp.ppterm outtype)))
1631       in
1632 (*
1633       let (parameters, arguments, exp_named_subst),ugraph2 =
1634         let ty,ugraph2 = type_of_aux context term ugraph1 in
1635           match R.whd context ty with
1636            (*CSC manca il caso dei CAST *)
1637 (*CSC: ma servono i parametri (uri,i)? Se si', perche' non serve anche il *)
1638 (*CSC: parametro exp_named_subst? Se no, perche' non li togliamo?         *)
1639 (*CSC: Hint: nella DTD servono per gli stylesheet.                        *)
1640               C.MutInd (uri',i',exp_named_subst) as typ ->
1641                 if U.eq uri uri' && i = i' then
1642                   ([],[],exp_named_subst),ugraph2
1643                 else
1644                   raise
1645                     (TypeCheckerFailure
1646                        (sprintf
1647                           ("Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}")
1648                           (CicPp.ppterm typ) (U.string_of_uri uri) i))
1649             | C.Appl
1650                 ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
1651                 if U.eq uri uri' && i = i' then
1652                   let params,args =
1653                     split tl (List.length tl - k)
1654                   in (params,args,exp_named_subst),ugraph2
1655                 else
1656                   raise
1657                     (TypeCheckerFailure
1658                        (sprintf
1659                           ("Case analysys: analysed term type is %s, "^
1660                            "but is expected to be (an application of) "^
1661                            "%s#1/%d{_}")
1662                           (CicPp.ppterm typ') (U.string_of_uri uri) i))
1663             | _ ->
1664                 raise
1665                   (TypeCheckerFailure
1666                      (sprintf
1667                         ("Case analysis: "^
1668                          "analysed term %s is not an inductive one")
1669                         (CicPp.ppterm term)))
1670 *)
1671       let (b, k) = guess_args context outsort in
1672           if not b then (b, k - 1) else (b, k) in
1673       let (parameters, arguments, exp_named_subst),ugraph2 =
1674         let ty,ugraph2 = type_of_aux ~logger context term ugraph1 in
1675         match R.whd ~subst context ty with
1676             C.MutInd (uri',i',exp_named_subst) as typ ->
1677               if U.eq uri uri' && i = i' then
1678                 ([],[],exp_named_subst),ugraph2
1679               else raise
1680                 (TypeCheckerFailure
1681                    (sprintf
1682                       ("Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}")
1683                       (CicPp.ppterm typ) (U.string_of_uri uri) i))
1684           | C.Appl
1685               ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
1686               if U.eq uri uri' && i = i' then
1687                 let params,args =
1688                   split tl (List.length tl - k)
1689                 in (params,args,exp_named_subst),ugraph2
1690               else raise
1691                 (TypeCheckerFailure
1692                    (sprintf
1693                       "Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}"
1694                       (CicPp.ppterm typ') (U.string_of_uri uri) i))
1695           | _ ->
1696               raise
1697                 (TypeCheckerFailure
1698                    (sprintf
1699                       "Case analysis: analysed term %s is not an inductive one"
1700                       (CicPp.ppterm term)))
1701       in
1702         (*
1703            let's control if the sort elimination is allowed:
1704            [(I q1 ... qr)|B]
1705         *)
1706       let sort_of_ind_type =
1707         if parameters = [] then
1708           C.MutInd (uri,i,exp_named_subst)
1709         else
1710           C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters)
1711       in
1712       let type_of_sort_of_ind_ty,ugraph3 =
1713         type_of_aux ~logger context sort_of_ind_type ugraph2 in
1714       let b,ugraph4 =
1715         check_allowed_sort_elimination ~logger  context uri i need_dummy
1716           sort_of_ind_type type_of_sort_of_ind_ty outsort ugraph3
1717       in
1718         if not b then
1719         raise
1720           (TypeCheckerFailure ("Case analasys: sort elimination not allowed"));
1721         (* let's check if the type of branches are right *)
1722       let parsno =
1723         let obj,_ =
1724           try
1725             CicEnvironment.get_cooked_obj ~trust:false uri CicUniv.empty_ugraph
1726           with Not_found -> assert false
1727         in
1728         match obj with
1729             C.InductiveDefinition (_,_,parsno) -> parsno
1730           | _ ->
1731               raise (TypeCheckerFailure
1732                 ("Unknown mutual inductive definition:" ^
1733                   UriManager.string_of_uri uri))
1734         in
1735       let (_,branches_ok,ugraph5) =
1736         List.fold_left
1737           (fun (j,b,ugraph) p ->
1738             if b then
1739               let cons =
1740                 if parameters = [] then
1741                   (C.MutConstruct (uri,i,j,exp_named_subst))
1742                 else
1743                   (C.Appl
1744                      (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
1745               in
1746               let ty_p,ugraph1 = type_of_aux ~logger context p ugraph in
1747               let ty_cons,ugraph3 = type_of_aux ~logger context cons ugraph1 in
1748               (* 2 is skipped *)
1749               let ty_branch =
1750                 type_of_branch context parsno need_dummy outtype cons
1751                   ty_cons in
1752               let b1,ugraph4 =
1753                 R.are_convertible
1754                   ~subst ~metasenv context ty_p ty_branch ugraph3
1755               in
1756               if not b1 then
1757                 debug_print
1758                   ("#### " ^ CicPp.ppterm ty_p ^
1759                   " <==> " ^ CicPp.ppterm ty_branch);
1760               (j + 1,b1,ugraph4)
1761             else
1762               (j,false,ugraph)
1763           ) (1,true,ugraph4) pl
1764          in
1765           if not branches_ok then
1766            raise
1767             (TypeCheckerFailure "Case analysys: wrong branch type");
1768           if not need_dummy then
1769             (C.Appl ((outtype::arguments)@[term])),ugraph5
1770           else if arguments = [] then
1771             outtype,ugraph5
1772           else
1773             (C.Appl (outtype::arguments)),ugraph5
1774    | C.Fix (i,fl) ->
1775       let types_times_kl,ugraph1 =
1776         (* WAS: list rev list map *)
1777         List.fold_left
1778           (fun (l,ugraph) (n,k,ty,_) ->
1779             let _,ugraph1 = type_of_aux ~logger context ty ugraph in
1780             ((Some (C.Name n,(C.Decl ty)),k)::l,ugraph1)
1781           ) ([],ugraph) fl
1782       in
1783       let (types,kl) = List.split types_times_kl in
1784       let len = List.length types in
1785       let ugraph2 =
1786         List.fold_left
1787           (fun ugraph (name,x,ty,bo) ->
1788              let ty_bo,ugraph1 =
1789                type_of_aux ~logger (types@context) bo ugraph
1790              in
1791              let b,ugraph2 =
1792                R.are_convertible ~subst ~metasenv (types@context)
1793                  ty_bo (CicSubstitution.lift len ty) ugraph1 in
1794                if b then
1795                  begin
1796                    let (m, eaten, context') =
1797                      eat_lambdas ~subst (types @ context) (x + 1) bo
1798                    in
1799                      (*
1800                        let's control the guarded by
1801                        destructors conditions D{f,k,x,M}
1802                      *)
1803                      if not (guarded_by_destructors context' eaten
1804                                (len + eaten) kl 1 [] m) then
1805                        raise
1806                          (TypeCheckerFailure
1807                             ("Fix: not guarded by destructors"))
1808                      else
1809                        ugraph2
1810                  end
1811                else
1812                  raise (TypeCheckerFailure ("Fix: ill-typed bodies"))
1813           ) ugraph1 fl in
1814         (*CSC: controlli mancanti solo su D{f,k,x,M} *)
1815       let (_,_,ty,_) = List.nth fl i in
1816         ty,ugraph2
1817    | C.CoFix (i,fl) ->
1818        let types,ugraph1 =
1819          List.fold_left
1820            (fun (l,ugraph) (n,ty,_) ->
1821               let _,ugraph1 =
1822                 type_of_aux ~logger context ty ugraph in
1823                 (Some (C.Name n,(C.Decl ty))::l,ugraph1)
1824            ) ([],ugraph) fl
1825        in
1826        let len = List.length types in
1827        let ugraph2 =
1828          List.fold_left
1829            (fun ugraph (_,ty,bo) ->
1830               let ty_bo,ugraph1 =
1831                 type_of_aux ~logger (types @ context) bo ugraph
1832               in
1833               let b,ugraph2 =
1834                 R.are_convertible ~subst ~metasenv (types @ context) ty_bo
1835                   (CicSubstitution.lift len ty) ugraph1
1836               in
1837                 if b then
1838                   begin
1839                     (* let's control that the returned type is coinductive *)
1840                     match returns_a_coinductive context ty with
1841                         None ->
1842                           raise
1843                           (TypeCheckerFailure
1844                              ("CoFix: does not return a coinductive type"))
1845                       | Some uri ->
1846                           (*
1847                             let's control the guarded by constructors
1848                             conditions C{f,M}
1849                           *)
1850                           if not (guarded_by_constructors (types @ context)
1851                                     0 len false bo [] uri) then
1852                             raise
1853                               (TypeCheckerFailure
1854                                  ("CoFix: not guarded by constructors"))
1855                           else
1856                           ugraph2
1857                   end
1858                 else
1859                   raise
1860                     (TypeCheckerFailure ("CoFix: ill-typed bodies"))
1861            ) ugraph1 fl
1862        in
1863        let (_,ty,_) = List.nth fl i in
1864          ty,ugraph2
1865
1866  and check_exp_named_subst ~logger ?(subst = []) context ugraph =
1867    let rec check_exp_named_subst_aux ~logger esubsts l ugraph =
1868      match l with
1869          [] -> ugraph
1870        | ((uri,t) as item)::tl ->
1871            let ty_uri,ugraph1 = type_of_variable ~logger uri ugraph in
1872            let typeofvar =
1873              CicSubstitution.subst_vars esubsts ty_uri in
1874            let typeoft,ugraph2 = type_of_aux ~logger context t ugraph1 in
1875            let b,ugraph3 =
1876              CicReduction.are_convertible ~subst ~metasenv
1877                context typeoft typeofvar ugraph2
1878            in
1879              if b then
1880                check_exp_named_subst_aux ~logger (esubsts@[item]) tl ugraph3
1881              else
1882                begin
1883                  CicReduction.fdebug := 0 ;
1884                  ignore
1885                    (CicReduction.are_convertible
1886                       ~subst ~metasenv context typeoft typeofvar ugraph2) ;
1887                  fdebug := 0 ;
1888                  debug typeoft [typeofvar] ;
1889                  raise (TypeCheckerFailure "Wrong Explicit Named Substitution")
1890                end
1891    in
1892      check_exp_named_subst_aux ~logger [] ugraph
1893
1894  and sort_of_prod ?(subst = []) context (name,s) (t1, t2) ugraph =
1895   let module C = Cic in
1896    let t1' = CicReduction.whd ~subst context t1 in
1897    let t2' = CicReduction.whd ~subst ((Some (name,C.Decl s))::context) t2 in
1898    match (t1', t2') with
1899       (C.Sort s1, C.Sort s2)
1900         when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1901          (* different from Coq manual!!! *)
1902          C.Sort s2,ugraph
1903     | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1904       (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
1905        let t' = CicUniv.fresh() in
1906        let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1907        let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1908        C.Sort (C.Type t'),ugraph2
1909     | (C.Sort _,C.Sort (C.Type t1)) ->
1910         (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
1911         C.Sort (C.Type t1),ugraph (* c'e' bisogno di un fresh? *)
1912     | (C.Meta _, C.Sort _) -> t2',ugraph
1913     | (C.Meta _, (C.Meta (_,_) as t))
1914     | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
1915         t2',ugraph
1916     | (_,_) -> raise (TypeCheckerFailure (sprintf
1917         "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1')
1918           (CicPp.ppterm t2')))
1919
1920  and eat_prods ?(subst = []) context hetype l ugraph =
1921    (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
1922    (*CSC: cucinati                                                         *)
1923    match l with
1924        [] -> hetype,ugraph
1925      | (hete, hety)::tl ->
1926          (match (CicReduction.whd ~subst context hetype) with
1927               Cic.Prod (n,s,t) ->
1928                 let b,ugraph1 =
1929                   CicReduction.are_convertible
1930                     ~subst ~metasenv context hety s ugraph
1931                 in
1932                   if b then
1933                     begin
1934                       CicReduction.fdebug := -1 ;
1935                       eat_prods ~subst context
1936                         (CicSubstitution.subst hete t) tl ugraph1
1937                         (*TASSI: not sure *)
1938                     end
1939                   else
1940                     begin
1941                       CicReduction.fdebug := 0 ;
1942                       ignore (CicReduction.are_convertible
1943                                 ~subst ~metasenv context s hety ugraph) ;
1944                       fdebug := 0 ;
1945                       debug s [hety] ;
1946                       raise
1947                         (TypeCheckerFailure
1948                            (sprintf
1949                               ("Appl: wrong parameter-type, expected %s, found %s")
1950                               (CicPp.ppterm hetype) (CicPp.ppterm s)))
1951                     end
1952             | _ ->
1953                 raise (TypeCheckerFailure
1954                          "Appl: this is not a function, it cannot be applied")
1955          )
1956
1957  and returns_a_coinductive context ty =
1958   let module C = Cic in
1959    match CicReduction.whd context ty with
1960       C.MutInd (uri,i,_) ->
1961        (*CSC: definire una funzioncina per questo codice sempre replicato *)
1962         let obj,_ =
1963           try
1964             CicEnvironment.get_cooked_obj ~trust:false uri CicUniv.empty_ugraph
1965           with Not_found -> assert false
1966         in
1967         (match obj with
1968            C.InductiveDefinition (itl,_,_) ->
1969             let (_,is_inductive,_,_) = List.nth itl i in
1970              if is_inductive then None else (Some uri)
1971          | _ ->
1972             raise (TypeCheckerFailure
1973               ("Unknown mutual inductive definition:" ^
1974               UriManager.string_of_uri uri))
1975         )
1976     | C.Appl ((C.MutInd (uri,i,_))::_) ->
1977        (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
1978          match o with
1979            C.InductiveDefinition (itl,_,_) ->
1980             let (_,is_inductive,_,_) = List.nth itl i in
1981              if is_inductive then None else (Some uri)
1982          | _ ->
1983             raise (TypeCheckerFailure
1984               ("Unknown mutual inductive definition:" ^
1985               UriManager.string_of_uri uri))
1986         )
1987     | C.Prod (n,so,de) ->
1988        returns_a_coinductive ((Some (n,C.Decl so))::context) de
1989     | _ -> None
1990
1991  in
1992 (*CSC
1993 debug_print ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t) ; flush stderr ;
1994 let res =
1995 *)
1996   type_of_aux ~logger context t ugraph
1997 (*
1998 in debug_print "FINE TYPE_OF_AUX" ; flush stderr ; res
1999 *)
2000
2001 (* is a small constructor? *)
2002 (*CSC: ottimizzare calcolando staticamente *)
2003 and is_small ~logger context paramsno c ugraph =
2004  let rec is_small_aux ~logger context c ugraph =
2005   let module C = Cic in
2006    match CicReduction.whd context c with
2007       C.Prod (n,so,de) ->
2008        (*CSC: [] is an empty metasenv. Is it correct? *)
2009        let s,ugraph1 = type_of_aux' ~logger [] context so ugraph in
2010        let b = (s = C.Sort C.Prop || s = C.Sort C.Set || s = C.Sort C.CProp) in
2011        if b then
2012          is_small_aux ~logger ((Some (n,(C.Decl so)))::context) de ugraph1
2013        else
2014          false,ugraph1
2015     | _ -> true,ugraph (*CSC: we trust the type-checker *)
2016  in
2017   let (context',dx) = split_prods context paramsno c in
2018    is_small_aux ~logger context' dx ugraph
2019
2020 and type_of ~logger t ugraph =
2021 (*CSC
2022 debug_print ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t) ; flush stderr ;
2023 let res =
2024 *)
2025  type_of_aux' ~logger [] [] t ugraph
2026 (*CSC
2027 in debug_print "FINE TYPE_OF_AUX'" ; flush stderr ; res
2028 *)
2029 ;;
2030
2031 let typecheck uri ugraph =
2032  let module C = Cic in
2033  let module R = CicReduction in
2034  let module U = UriManager in
2035  let logger = new CicLogger.logger in
2036    (* ??? match CicEnvironment.is_type_checked ~trust:true uri with ???? *)
2037    match CicEnvironment.is_type_checked ~trust:false uri ugraph with
2038      CicEnvironment.CheckedObj (cobj,ugraph') ->
2039        (* prerr_endline ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri);*)
2040        cobj,ugraph'
2041    | CicEnvironment.UncheckedObj uobj ->
2042       (* let's typecheck the uncooked object *)
2043       logger#log (`Start_type_checking uri) ;
2044       (* prerr_endline ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri); *)
2045       let ugraph1 =
2046         (match uobj with
2047          C.Constant (_,Some te,ty,_) ->
2048            let _,ugraph1 = type_of ~logger ty ugraph in
2049            let ty_te,ugraph2 = type_of ~logger te ugraph1 in
2050            let b,ugraph3 = (R.are_convertible [] ty_te ty ugraph2) in
2051            if not b then
2052               raise (TypeCheckerFailure
2053                 ("Unknown constant:" ^ U.string_of_uri uri))
2054            else
2055               ugraph3
2056         | C.Constant (_,None,ty,_) ->
2057           (* only to check that ty is well-typed *)
2058           let _,ugraph1 = type_of ~logger ty ugraph in
2059           ugraph1
2060         | C.CurrentProof (_,conjs,te,ty,_) ->
2061            let _,ugraph1 =
2062             List.fold_left
2063              (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
2064                let _,ugraph1 =
2065                  type_of_aux' ~logger metasenv context ty ugraph
2066                in
2067                metasenv @ [conj],ugraph1
2068              ) ([],ugraph) conjs
2069            in
2070             let _,ugraph2 = type_of_aux' ~logger conjs [] ty ugraph1 in
2071             let type_of_te,ugraph3 =
2072               type_of_aux' ~logger conjs [] te ugraph2
2073             in
2074             let b,ugraph4 = R.are_convertible [] type_of_te ty ugraph3 in
2075             if not b then
2076                raise (TypeCheckerFailure (sprintf
2077                 "the current proof %s is not well typed because the type %s of the body is not convertible to the declared type %s"
2078                 (U.string_of_uri uri) (CicPp.ppterm type_of_te)
2079                 (CicPp.ppterm ty)))
2080             else
2081               ugraph4
2082         | C.Variable (_,bo,ty,_) ->
2083            (* only to check that ty is well-typed *)
2084            let _,ugraph1 = type_of ~logger ty ugraph in
2085             (match bo with
2086                 None -> ugraph1
2087               | Some bo ->
2088                  let ty_bo,ugraph2 = type_of ~logger bo ugraph1 in
2089                  let b,ugraph3 = R.are_convertible [] ty_bo ty ugraph2 in
2090                  if not b then
2091                    raise (TypeCheckerFailure
2092                      ("Unknown variable:" ^ U.string_of_uri uri))
2093                  else
2094                    ugraph3
2095             )
2096         | C.InductiveDefinition _ ->
2097            check_mutual_inductive_defs ~logger uri uobj ugraph
2098       ) in
2099         try
2100           CicEnvironment.set_type_checking_info uri;
2101           logger#log (`Type_checking_completed uri);
2102           match CicEnvironment.is_type_checked ~trust:false uri ugraph with
2103               CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
2104             | _ -> raise CicEnvironmentError
2105         with
2106             (*
2107               this is raised if set_type_checking_info is called on an object
2108               that has no associated universe file. If we are in univ_maker
2109               phase this is OK since univ_maker will properly commit the
2110               object.
2111             *)
2112             Invalid_argument s ->
2113               (*prerr_endline s;*)
2114               uobj,ugraph1
2115 ;;
2116
2117 (** wrappers which instantiate fresh loggers *)
2118
2119 let type_of_aux' ?(subst = []) metasenv context t =
2120   let logger = new CicLogger.logger in
2121   type_of_aux' ~logger ~subst metasenv context t
2122
2123 let typecheck_mutual_inductive_defs uri (itl, uris, indparamsno) =
2124   let logger = new CicLogger.logger in
2125   typecheck_mutual_inductive_defs ~logger uri (itl, uris, indparamsno)
2126