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 exception Impossible of int;;
  27 exception NotWellTyped of string;;
  28 exception WrongUriToConstant of string;;
  29 exception WrongUriToVariable of string;;
  30 exception WrongUriToMutualInductiveDefinitions of string;;
  31 exception ListTooShort;;
  32 exception NotPositiveOccurrences of string;;
  33 exception NotWellFormedTypeOfInductiveConstructor of string;;
  34 exception WrongRequiredArgument of string;;
  35 exception RelToHiddenHypothesis;;
  36 exception MetasenvInconsistency;;
  37
  38 let fdebug = ref 0;;
  39 let debug t context =
  40  let rec debug_aux t i =
  41   let module C = Cic in
  42   let module U = UriManager in
  43    CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
  44  in
  45   if !fdebug = 0 then
  46    raise (NotWellTyped ("\n" ^ List.fold_right debug_aux (t::context) ""))
  47    (*print_endline ("\n" ^ List.fold_right debug_aux (t::context) "") ; flush stdout*)
  48 ;;
  49
  50 let rec split l n =
  51  match (l,n) with
  52     (l,0) -> ([], l)
  53   | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
  54   | (_,_) -> raise ListTooShort
  55 ;;
  56
  57 let debrujin_constructor uri number_of_types =
  58  let rec aux k =
  59   let module C = Cic in
  60    function
  61       C.Rel n as t when n <= k -> t
  62     | C.Rel _ ->
  63         raise (NotWellTyped ("Debrujin: open term found"))
  64     | C.Var (uri,exp_named_subst) ->
  65        let exp_named_subst' =
  66         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
  67        in
  68         C.Var (uri,exp_named_subst')
  69     | C.Meta _ -> assert false
  70     | C.Sort _
  71     | C.Implicit as t -> t
  72     | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
  73     | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k+1) t)
  74     | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k+1) t)
  75     | C.LetIn (n,s,t) -> C.LetIn (n, aux k s, aux (k+1) t)
  76     | C.Appl l -> C.Appl (List.map (aux k) l)
  77     | C.Const (uri,exp_named_subst) ->
  78        let exp_named_subst' =
  79         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
  80        in
  81         C.Const (uri,exp_named_subst')
  82     | C.MutInd (uri',tyno,exp_named_subst) when UriManager.eq uri uri' ->
  83        if exp_named_subst != [] then
  84         raise
  85          (NotWellTyped
  86            ("Debrujin: a non-empty explicit named substitution is applied to " ^
  87             "a mutual inductive type which is being defined")) ;
  88        C.Rel (k + number_of_types - tyno) ;
  89     | C.MutInd (uri',tyno,exp_named_subst) ->
  90        let exp_named_subst' =
  91         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
  92        in
  93         C.MutInd (uri',tyno,exp_named_subst')
  94     | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
  95        let exp_named_subst' =
  96         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
  97        in
  98         C.MutConstruct (uri,tyno,consno,exp_named_subst')
  99     | C.MutCase (sp,i,outty,t,pl) ->
 100        C.MutCase (sp, i, aux k outty, aux k t,
 101         List.map (aux k) pl)
 102     | C.Fix (i, fl) ->
 103        let len = List.length fl in
 104        let liftedfl =
 105         List.map
 106          (fun (name, i, ty, bo) -> (name, i, aux k ty, aux (k+len) bo))
 107           fl
 108        in
 109         C.Fix (i, liftedfl)
 110     | C.CoFix (i, fl) ->
 111        let len = List.length fl in
 112        let liftedfl =
 113         List.map
 114          (fun (name, ty, bo) -> (name, aux k ty, aux (k+len) bo))
 115           fl
 116        in
 117         C.CoFix (i, liftedfl)
 118  in
 119   aux 0
 120 ;;
 121
 122 exception CicEnvironmentError;;
 123
 124 let rec type_of_constant uri =
 125  let module C = Cic in
 126  let module R = CicReduction in
 127  let module U = UriManager in
 128   let cobj =
 129    match CicEnvironment.is_type_checked ~trust:true uri with
 130       CicEnvironment.CheckedObj cobj -> cobj
 131     | CicEnvironment.UncheckedObj uobj ->
 132        Logger.log (`Start_type_checking uri) ;
 133        (* let's typecheck the uncooked obj *)
 134        (match uobj with
 135            C.Constant (_,Some te,ty,_) ->
 136              let _ = type_of ty in
 137               if not (R.are_convertible [] (type_of te) ty) then
 138                raise (NotWellTyped ("Constant " ^ (U.string_of_uri uri)))
 139          | C.Constant (_,None,ty,_) ->
 140            (* only to check that ty is well-typed *)
 141            let _ = type_of ty in ()
 142          | C.CurrentProof (_,conjs,te,ty,_) ->
 143              let _ =
 144               List.fold_left
 145                (fun metasenv ((_,context,ty) as conj) ->
 146                  ignore (type_of_aux' metasenv context ty) ;
 147                  metasenv @ [conj]
 148                ) [] conjs
 149              in
 150               let _ = type_of_aux' conjs [] ty in
 151                if not (R.are_convertible [] (type_of_aux' conjs [] te) ty)
 152                then
 153                 raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))
 154          | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
 155        ) ;
 156        CicEnvironment.set_type_checking_info uri ;
 157        Logger.log (`Type_checking_completed uri) ;
 158        match CicEnvironment.is_type_checked ~trust:false uri with
 159           CicEnvironment.CheckedObj cobj -> cobj
 160         | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
 161   in
 162    match cobj with
 163       C.Constant (_,_,ty,_) -> ty
 164     | C.CurrentProof (_,_,_,ty,_) -> ty
 165     | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
 166
 167 and type_of_variable uri =
 168  let module C = Cic in
 169  let module R = CicReduction in
 170  let module U = UriManager in
 171   (* 0 because a variable is never cooked => no partial cooking at one level *)
 172   match CicEnvironment.is_type_checked ~trust:true uri with
 173      CicEnvironment.CheckedObj (C.Variable (_,_,ty,_)) -> ty
 174    | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_)) ->
 175       Logger.log (`Start_type_checking uri) ;
 176       (* only to check that ty is well-typed *)
 177       let _ = type_of ty in
 178        (match bo with
 179            None -> ()
 180          | Some bo ->
 181             if not (R.are_convertible [] (type_of bo) ty) then
 182              raise (NotWellTyped ("Variable " ^ (U.string_of_uri uri)))
 183        ) ;
 184        CicEnvironment.set_type_checking_info uri ;
 185        Logger.log (`Type_checking_completed uri) ;
 186        ty
 187    |  _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
 188
 189 and does_not_occur context n nn te =
 190  let module C = Cic in
 191    (*CSC: whd sembra essere superflua perche' un caso in cui l'occorrenza *)
 192    (*CSC: venga mangiata durante la whd sembra presentare problemi di *)
 193    (*CSC: universi                                                    *)
 194    match CicReduction.whd context te with
 195       C.Rel m when m > n && m <= nn -> false
 196     | C.Rel _
 197     | C.Meta _
 198     | C.Sort _
 199     | C.Implicit -> true
 200     | C.Cast (te,ty) ->
 201        does_not_occur context n nn te && does_not_occur context n nn ty
 202     | C.Prod (name,so,dest) ->
 203        does_not_occur context n nn so &&
 204         does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) dest
 205     | C.Lambda (name,so,dest) ->
 206        does_not_occur context n nn so &&
 207         does_not_occur((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) dest
 208     | C.LetIn (name,so,dest) ->
 209        does_not_occur context n nn so &&
 210         does_not_occur ((Some (name,(C.Def so)))::context) (n + 1) (nn + 1) dest
 211     | C.Appl l ->
 212        List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
 213     | C.Var (_,exp_named_subst)
 214     | C.Const (_,exp_named_subst)
 215     | C.MutInd (_,_,exp_named_subst)
 216     | C.MutConstruct (_,_,_,exp_named_subst) ->
 217        List.fold_right (fun (_,x) i -> i && does_not_occur context n nn x)
 218         exp_named_subst true
 219     | C.MutCase (_,_,out,te,pl) ->
 220        does_not_occur context n nn out && does_not_occur context n nn te &&
 221         List.fold_right (fun x i -> i && does_not_occur context n nn x) pl true
 222     | C.Fix (_,fl) ->
 223        let len = List.length fl in
 224         let n_plus_len = n + len in
 225         let nn_plus_len = nn + len in
 226         let tys =
 227          List.map (fun (n,_,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
 228         in
 229          List.fold_right
 230           (fun (_,_,ty,bo) i ->
 231             i && does_not_occur context n nn ty &&
 232             does_not_occur (tys @ context) n_plus_len nn_plus_len bo
 233           ) fl true
 234     | C.CoFix (_,fl) ->
 235        let len = List.length fl in
 236         let n_plus_len = n + len in
 237         let nn_plus_len = nn + len in
 238         let tys =
 239          List.map (fun (n,ty,_) -> Some (C.Name n,(Cic.Decl ty))) fl
 240         in
 241          List.fold_right
 242           (fun (_,ty,bo) i ->
 243             i && does_not_occur context n nn ty &&
 244             does_not_occur (tys @ context) n_plus_len nn_plus_len bo
 245           ) fl true
 246
 247 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
 248 (*CSC questa funzione e' simile alla are_all_occurrences_positive, ma fa *)
 249 (*CSC dei controlli leggermente diversi. Viene invocata solamente dalla  *)
 250 (*CSC strictly_positive                                                  *)
 251 (*CSC definizione (giusta???) tratta dalla mail di Hugo ;-)              *)
 252 and weakly_positive context n nn uri te =
 253  let module C = Cic in
 254 (*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*)
 255   let dummy_mutind =
 256    C.MutInd (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind",0,[])
 257   in
 258   (*CSC mettere in cicSubstitution *)
 259   let rec subst_inductive_type_with_dummy_mutind =
 260    function
 261       C.MutInd (uri',0,_) when UriManager.eq uri' uri ->
 262        dummy_mutind
 263     | C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri ->
 264        dummy_mutind
 265     | C.Cast (te,ty) -> subst_inductive_type_with_dummy_mutind te
 266     | C.Prod (name,so,ta) ->
 267        C.Prod (name, subst_inductive_type_with_dummy_mutind so,
 268         subst_inductive_type_with_dummy_mutind ta)
 269     | C.Lambda (name,so,ta) ->
 270        C.Lambda (name, subst_inductive_type_with_dummy_mutind so,
 271         subst_inductive_type_with_dummy_mutind ta)
 272     | C.Appl tl ->
 273        C.Appl (List.map subst_inductive_type_with_dummy_mutind tl)
 274     | C.MutCase (uri,i,outtype,term,pl) ->
 275        C.MutCase (uri,i,
 276         subst_inductive_type_with_dummy_mutind outtype,
 277         subst_inductive_type_with_dummy_mutind term,
 278         List.map subst_inductive_type_with_dummy_mutind pl)
 279     | C.Fix (i,fl) ->
 280        C.Fix (i,List.map (fun (name,i,ty,bo) -> (name,i,
 281         subst_inductive_type_with_dummy_mutind ty,
 282         subst_inductive_type_with_dummy_mutind bo)) fl)
 283     | C.CoFix (i,fl) ->
 284        C.CoFix (i,List.map (fun (name,ty,bo) -> (name,
 285         subst_inductive_type_with_dummy_mutind ty,
 286         subst_inductive_type_with_dummy_mutind bo)) fl)
 287     | C.Const (uri,exp_named_subst) ->
 288        let exp_named_subst' =
 289         List.map
 290          (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
 291          exp_named_subst
 292        in
 293         C.Const (uri,exp_named_subst')
 294     | C.MutInd (uri,typeno,exp_named_subst) ->
 295        let exp_named_subst' =
 296         List.map
 297          (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
 298          exp_named_subst
 299        in
 300         C.MutInd (uri,typeno,exp_named_subst')
 301     | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
 302        let exp_named_subst' =
 303         List.map
 304          (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
 305          exp_named_subst
 306        in
 307         C.MutConstruct (uri,typeno,consno,exp_named_subst')
 308     | t -> t
 309   in
 310   match CicReduction.whd context te with
 311      C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri -> true
 312    | C.MutInd (uri',0,_) when UriManager.eq uri' uri -> true
 313    | C.Prod (C.Anonymous,source,dest) ->
 314       strictly_positive context n nn
 315        (subst_inductive_type_with_dummy_mutind source) &&
 316        weakly_positive ((Some (C.Anonymous,(C.Decl source)))::context)
 317         (n + 1) (nn + 1) uri dest
 318    | C.Prod (name,source,dest) when
 319       does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
 320        (* dummy abstraction, so we behave as in the anonimous case *)
 321        strictly_positive context n nn
 322         (subst_inductive_type_with_dummy_mutind source) &&
 323         weakly_positive ((Some (name,(C.Decl source)))::context)
 324          (n + 1) (nn + 1) uri dest
 325    | C.Prod (name,source,dest) ->
 326       does_not_occur context n nn
 327        (subst_inductive_type_with_dummy_mutind source)&&
 328        weakly_positive ((Some (name,(C.Decl source)))::context)
 329         (n + 1) (nn + 1) uri dest
 330    | _ -> raise (NotWellFormedTypeOfInductiveConstructor ("Guess where the error is ;-)"))
 331
 332 (* instantiate_parameters ps (x1:T1)...(xn:Tn)C                             *)
 333 (* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *)
 334 and instantiate_parameters params c =
 335  let module C = Cic in
 336   match (c,params) with
 337      (c,[]) -> c
 338    | (C.Prod (_,_,ta), he::tl) ->
 339        instantiate_parameters tl
 340         (CicSubstitution.subst he ta)
 341    | (C.Cast (te,_), _) -> instantiate_parameters params te
 342    | (t,l) -> raise (Impossible 1)
 343
 344 and strictly_positive context n nn te =
 345  let module C = Cic in
 346  let module U = UriManager in
 347   match CicReduction.whd context te with
 348      C.Rel _ -> true
 349    | C.Cast (te,ty) ->
 350       (*CSC: bisogna controllare ty????*)
 351       strictly_positive context n nn te
 352    | C.Prod (name,so,ta) ->
 353       does_not_occur context n nn so &&
 354        strictly_positive ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) ta
 355    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
 356       List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
 357    | C.Appl ((C.MutInd (uri,i,exp_named_subst))::tl) ->
 358       let (ok,paramsno,ity,cl,name) =
 359        match CicEnvironment.get_obj uri with
 360            C.InductiveDefinition (tl,_,paramsno) ->
 361             let (name,_,ity,cl) = List.nth tl i in
 362              (List.length tl = 1, paramsno, ity, cl, name)
 363          | _ -> raise(WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
 364       in
 365        let (params,arguments) = split tl paramsno in
 366        let lifted_params = List.map (CicSubstitution.lift 1) params in
 367        let cl' =
 368         List.map
 369          (fun (_,te) ->
 370            instantiate_parameters lifted_params
 371             (CicSubstitution.subst_vars exp_named_subst te)
 372          ) cl
 373        in
 374         ok &&
 375          List.fold_right
 376           (fun x i -> i && does_not_occur context n nn x)
 377           arguments true &&
 378          (*CSC: MEGAPATCH3 (sara' quella giusta?)*)
 379          List.fold_right
 380           (fun x i ->
 381             i &&
 382              weakly_positive
 383               ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri x
 384           ) cl' true
 385    | t -> does_not_occur context n nn t
 386
 387 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
 388 and are_all_occurrences_positive context uri indparamsno i n nn te =
 389  let module C = Cic in
 390   match CicReduction.whd context te with
 391      C.Appl ((C.Rel m)::tl) when m = i ->
 392       (*CSC: riscrivere fermandosi a 0 *)
 393       (* let's check if the inductive type is applied at least to *)
 394       (* indparamsno parameters                                   *)
 395       let last =
 396        List.fold_left
 397         (fun k x ->
 398           if k = 0 then 0
 399           else
 400            match CicReduction.whd context x with
 401               C.Rel m when m = n - (indparamsno - k) -> k - 1
 402             | _ -> raise (WrongRequiredArgument (UriManager.string_of_uri uri))
 403         ) indparamsno tl
 404       in
 405        if last = 0 then
 406         List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
 407        else
 408         raise (WrongRequiredArgument (UriManager.string_of_uri uri))
 409    | C.Rel m when m = i ->
 410       if indparamsno = 0 then
 411        true
 412       else
 413        raise (WrongRequiredArgument (UriManager.string_of_uri uri))
 414    | C.Prod (C.Anonymous,source,dest) ->
 415       strictly_positive context n nn source &&
 416        are_all_occurrences_positive
 417         ((Some (C.Anonymous,(C.Decl source)))::context) uri indparamsno
 418         (i+1) (n + 1) (nn + 1) dest
 419    | C.Prod (name,source,dest) when
 420       does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
 421       (* dummy abstraction, so we behave as in the anonimous case *)
 422       strictly_positive context n nn source &&
 423        are_all_occurrences_positive
 424         ((Some (name,(C.Decl source)))::context) uri indparamsno
 425         (i+1) (n + 1) (nn + 1) dest
 426    | C.Prod (name,source,dest) ->
 427       does_not_occur context n nn source &&
 428        are_all_occurrences_positive ((Some (name,(C.Decl source)))::context)
 429         uri indparamsno (i+1) (n + 1) (nn + 1) dest
 430    | _ -> raise (NotWellFormedTypeOfInductiveConstructor (UriManager.string_of_uri uri))
 431
 432 (* Main function to checks the correctness of a mutual *)
 433 (* inductive block definition. This is the function    *)
 434 (* exported to the proof-engine.                       *)
 435 and typecheck_mutual_inductive_defs uri (itl,_,indparamsno) =
 436  let module U = UriManager in
 437   (* let's check if the arity of the inductive types are well *)
 438   (* formed                                                   *)
 439   List.iter (fun (_,_,x,_) -> let _ = type_of x in ()) itl ;
 440
 441   (* let's check if the types of the inductive constructors  *)
 442   (* are well formed.                                        *)
 443   (* In order not to use type_of_aux we put the types of the *)
 444   (* mutual inductive types at the head of the types of the  *)
 445   (* constructors using Prods                                *)
 446   let len = List.length itl in
 447    let tys =
 448     List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in
 449    let _ =
 450     List.fold_right
 451      (fun (_,_,_,cl) i ->
 452        List.iter
 453         (fun (name,te) ->
 454           let debrujinedte = debrujin_constructor uri len te in
 455           let augmented_term =
 456            List.fold_right
 457             (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i))
 458             itl debrujinedte
 459           in
 460            let _ = type_of augmented_term in
 461             (* let's check also the positivity conditions *)
 462             if
 463              not
 464               (are_all_occurrences_positive tys uri indparamsno i 0 len
 465                 debrujinedte)
 466             then
 467              raise (NotPositiveOccurrences (U.string_of_uri uri))
 468         ) cl ;
 469        (i + 1)
 470     ) itl 1
 471    in
 472     ()
 473
 474 (* Main function to checks the correctness of a mutual *)
 475 (* inductive block definition.                         *)
 476 and check_mutual_inductive_defs uri =
 477  function
 478     Cic.InductiveDefinition (itl, params, indparamsno) ->
 479      typecheck_mutual_inductive_defs uri (itl,params,indparamsno)
 480   | _ ->
 481     raise (WrongUriToMutualInductiveDefinitions (UriManager.string_of_uri uri))
 482
 483 and type_of_mutual_inductive_defs uri i =
 484  let module C = Cic in
 485  let module R = CicReduction in
 486  let module U = UriManager in
 487   let cobj =
 488    match CicEnvironment.is_type_checked ~trust:true uri with
 489       CicEnvironment.CheckedObj cobj -> cobj
 490     | CicEnvironment.UncheckedObj uobj ->
 491        Logger.log (`Start_type_checking uri) ;
 492        check_mutual_inductive_defs uri uobj ;
 493        CicEnvironment.set_type_checking_info uri ;
 494        Logger.log (`Type_checking_completed uri) ;
 495        (match CicEnvironment.is_type_checked ~trust:false uri with
 496           CicEnvironment.CheckedObj cobj -> cobj
 497         | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
 498        )
 499   in
 500    match cobj with
 501       C.InductiveDefinition (dl,_,_) ->
 502        let (_,_,arity,_) = List.nth dl i in
 503         arity
 504     | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
 505
 506 and type_of_mutual_inductive_constr uri i j =
 507  let module C = Cic in
 508  let module R = CicReduction in
 509  let module U = UriManager in
 510   let cobj =
 511    match CicEnvironment.is_type_checked ~trust:true uri with
 512       CicEnvironment.CheckedObj cobj -> cobj
 513     | CicEnvironment.UncheckedObj uobj ->
 514        Logger.log (`Start_type_checking uri) ;
 515        check_mutual_inductive_defs uri uobj ;
 516        CicEnvironment.set_type_checking_info uri ;
 517        Logger.log (`Type_checking_completed uri) ;
 518        (match CicEnvironment.is_type_checked ~trust:false uri with
 519           CicEnvironment.CheckedObj cobj -> cobj
 520         | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
 521        )
 522   in
 523    match cobj with
 524       C.InductiveDefinition (dl,_,_) ->
 525        let (_,_,_,cl) = List.nth dl i in
 526         let (_,ty) = List.nth cl (j-1) in
 527          ty
 528     | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
 529
 530 and recursive_args context n nn te =
 531  let module C = Cic in
 532   match CicReduction.whd context te with
 533      C.Rel _ -> []
 534    | C.Var _
 535    | C.Meta _
 536    | C.Sort _
 537    | C.Implicit
 538    | C.Cast _ (*CSC ??? *) -> raise (Impossible 3) (* due to type-checking *)
 539    | C.Prod (name,so,de) ->
 540       (not (does_not_occur context n nn so)) ::
 541        (recursive_args ((Some (name,(C.Decl so)))::context) (n+1) (nn + 1) de)
 542    | C.Lambda _
 543    | C.LetIn _ -> raise (Impossible 4) (* due to type-checking *)
 544    | C.Appl _ -> []
 545    | C.Const _ -> raise (Impossible 5)
 546    | C.MutInd _
 547    | C.MutConstruct _
 548    | C.MutCase _
 549    | C.Fix _
 550    | C.CoFix _ -> raise (Impossible 6) (* due to type-checking *)
 551
 552 and get_new_safes context p c rl safes n nn x =
 553  let module C = Cic in
 554  let module U = UriManager in
 555  let module R = CicReduction in
 556   match (R.whd context c, R.whd context p, rl) with
 557      (C.Prod (_,so,ta1), C.Lambda (name,_,ta2), b::tl) ->
 558        (* we are sure that the two sources are convertible because we *)
 559        (* have just checked this. So let's go along ...               *)
 560        let safes' =
 561         List.map (fun x -> x + 1) safes
 562        in
 563         let safes'' =
 564          if b then 1::safes' else safes'
 565         in
 566          get_new_safes ((Some (name,(C.Decl so)))::context)
 567           ta2 ta1 tl safes'' (n+1) (nn+1) (x+1)
 568    | (C.Prod _, (C.MutConstruct _ as e), _)
 569    | (C.Prod _, (C.Rel _ as e), _)
 570    | (C.MutInd _, e, [])
 571    | (C.Appl _, e, []) -> (e,safes,n,nn,x,context)
 572    | (_,_,_) ->
 573       (* CSC: If the next exception is raised, it just means that   *)
 574       (* CSC: the proof-assistant allows to use very strange things *)
 575       (* CSC: as a branch of a case whose type is a Prod. In        *)
 576       (* CSC: particular, this means that a new (C.Prod, x,_) case  *)
 577       (* CSC: must be considered in this match. (e.g. x = MutCase)  *)
 578       raise (Impossible 7)
 579
 580 and split_prods context n te =
 581  let module C = Cic in
 582  let module R = CicReduction in
 583   match (n, R.whd context te) with
 584      (0, _) -> context,te
 585    | (n, C.Prod (name,so,ta)) when n > 0 ->
 586        split_prods ((Some (name,(C.Decl so)))::context) (n - 1) ta
 587    | (_, _) -> raise (Impossible 8)
 588
 589 and eat_lambdas context n te =
 590  let module C = Cic in
 591  let module R = CicReduction in
 592   match (n, R.whd context te) with
 593      (0, _) -> (te, 0, context)
 594    | (n, C.Lambda (name,so,ta)) when n > 0 ->
 595       let (te, k, context') =
 596        eat_lambdas ((Some (name,(C.Decl so)))::context) (n - 1) ta
 597       in
 598        (te, k + 1, context')
 599    | (_, _) -> raise (Impossible 9)
 600
 601 (*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *)
 602 and check_is_really_smaller_arg context n nn kl x safes te =
 603  (*CSC: forse la whd si puo' fare solo quando serve veramente. *)
 604  (*CSC: cfr guarded_by_destructors                             *)
 605  let module C = Cic in
 606  let module U = UriManager in
 607  match CicReduction.whd context te with
 608      C.Rel m when List.mem m safes -> true
 609    | C.Rel _ -> false
 610    | C.Var _
 611    | C.Meta _
 612    | C.Sort _
 613    | C.Implicit
 614    | C.Cast _
 615 (*   | C.Cast (te,ty) ->
 616       check_is_really_smaller_arg n nn kl x safes te &&
 617        check_is_really_smaller_arg n nn kl x safes ty*)
 618 (*   | C.Prod (_,so,ta) ->
 619       check_is_really_smaller_arg n nn kl x safes so &&
 620        check_is_really_smaller_arg (n+1) (nn+1) kl (x+1)
 621         (List.map (fun x -> x + 1) safes) ta*)
 622    | C.Prod _ -> raise (Impossible 10)
 623    | C.Lambda (name,so,ta) ->
 624       check_is_really_smaller_arg context n nn kl x safes so &&
 625        check_is_really_smaller_arg ((Some (name,(C.Decl so)))::context)
 626         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 627    | C.LetIn (name,so,ta) ->
 628       check_is_really_smaller_arg context n nn kl x safes so &&
 629        check_is_really_smaller_arg ((Some (name,(C.Def so)))::context)
 630         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 631    | C.Appl (he::_) ->
 632       (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
 633       (*CSC: solo perche' non abbiamo trovato controesempi            *)
 634       check_is_really_smaller_arg context n nn kl x safes he
 635    | C.Appl [] -> raise (Impossible 11)
 636    | C.Const _
 637    | C.MutInd _ -> raise (Impossible 12)
 638    | C.MutConstruct _ -> false
 639    | C.MutCase (uri,i,outtype,term,pl) ->
 640       (match term with
 641           C.Rel m when List.mem m safes || m = x ->
 642            let (tys,len,isinductive,paramsno,cl) =
 643             match CicEnvironment.get_obj uri with
 644                C.InductiveDefinition (tl,_,paramsno) ->
 645                 let tys =
 646                  List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl
 647                 in
 648                  let (_,isinductive,_,cl) = List.nth tl i in
 649                   let cl' =
 650                    List.map
 651                     (fun (id,ty) ->
 652                       (id, snd (split_prods tys paramsno ty))) cl
 653                   in
 654                    (tys,List.length tl,isinductive,paramsno,cl')
 655              | _ ->
 656                raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
 657            in
 658             if not isinductive then
 659               List.fold_right
 660                (fun p i ->
 661                  i && check_is_really_smaller_arg context n nn kl x safes p)
 662                pl true
 663             else
 664               List.fold_right
 665                (fun (p,(_,c)) i ->
 666                  let rl' =
 667                   let debrujinedte = debrujin_constructor uri len c in
 668                    recursive_args tys 0 len debrujinedte
 669                  in
 670                   let (e,safes',n',nn',x',context') =
 671                    get_new_safes context p c rl' safes n nn x
 672                   in
 673                    i &&
 674                    check_is_really_smaller_arg context' n' nn' kl x' safes' e
 675                ) (List.combine pl cl) true
 676         | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
 677            let (tys,len,isinductive,paramsno,cl) =
 678             match CicEnvironment.get_obj uri with
 679                C.InductiveDefinition (tl,_,paramsno) ->
 680                 let (_,isinductive,_,cl) = List.nth tl i in
 681                  let tys =
 682                   List.map (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
 683                  in
 684                   let cl' =
 685                    List.map
 686                     (fun (id,ty) ->
 687                       (id, snd (split_prods tys paramsno ty))) cl
 688                   in
 689                    (tys,List.length tl,isinductive,paramsno,cl')
 690              | _ ->
 691                raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
 692            in
 693             if not isinductive then
 694               List.fold_right
 695                (fun p i ->
 696                  i && check_is_really_smaller_arg context n nn kl x safes p)
 697                pl true
 698             else
 699               (*CSC: supponiamo come prima che nessun controllo sia necessario*)
 700               (*CSC: sugli argomenti di una applicazione                      *)
 701               List.fold_right
 702                (fun (p,(_,c)) i ->
 703                  let rl' =
 704                   let debrujinedte = debrujin_constructor uri len c in
 705                    recursive_args tys 0 len debrujinedte
 706                  in
 707                   let (e, safes',n',nn',x',context') =
 708                    get_new_safes context p c rl' safes n nn x
 709                   in
 710                    i &&
 711                    check_is_really_smaller_arg context' n' nn' kl x' safes' e
 712                ) (List.combine pl cl) true
 713         | _ ->
 714           List.fold_right
 715            (fun p i ->
 716              i && check_is_really_smaller_arg context n nn kl x safes p
 717            ) pl true
 718       )
 719    | C.Fix (_, fl) ->
 720       let len = List.length fl in
 721        let n_plus_len = n + len
 722        and nn_plus_len = nn + len
 723        and x_plus_len = x + len
 724        and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
 725        and safes' = List.map (fun x -> x + len) safes in
 726         List.fold_right
 727          (fun (_,_,ty,bo) i ->
 728            i &&
 729             check_is_really_smaller_arg (tys@context) n_plus_len nn_plus_len kl
 730              x_plus_len safes' bo
 731          ) fl true
 732    | C.CoFix (_, fl) ->
 733       let len = List.length fl in
 734        let n_plus_len = n + len
 735        and nn_plus_len = nn + len
 736        and x_plus_len = x + len
 737        and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
 738        and safes' = List.map (fun x -> x + len) safes in
 739         List.fold_right
 740          (fun (_,ty,bo) i ->
 741            i &&
 742             check_is_really_smaller_arg (tys@context) n_plus_len nn_plus_len kl
 743              x_plus_len safes' bo
 744          ) fl true
 745
 746 and guarded_by_destructors context n nn kl x safes =
 747  let module C = Cic in
 748  let module U = UriManager in
 749   function
 750      C.Rel m when m > n && m <= nn -> false
 751    | C.Rel n ->
 752       (match List.nth context (n-1) with
 753           Some (_,C.Decl _) -> true
 754         | Some (_,C.Def bo) -> guarded_by_destructors context n nn kl x safes bo
 755         | None -> raise RelToHiddenHypothesis
 756       )
 757    | C.Meta _
 758    | C.Sort _
 759    | C.Implicit -> true
 760    | C.Cast (te,ty) ->
 761       guarded_by_destructors context n nn kl x safes te &&
 762        guarded_by_destructors context n nn kl x safes ty
 763    | C.Prod (name,so,ta) ->
 764       guarded_by_destructors context n nn kl x safes so &&
 765        guarded_by_destructors ((Some (name,(C.Decl so)))::context)
 766         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 767    | C.Lambda (name,so,ta) ->
 768       guarded_by_destructors context n nn kl x safes so &&
 769        guarded_by_destructors ((Some (name,(C.Decl so)))::context)
 770         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 771    | C.LetIn (name,so,ta) ->
 772       guarded_by_destructors context n nn kl x safes so &&
 773        guarded_by_destructors ((Some (name,(C.Def so)))::context)
 774         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 775    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
 776       let k = List.nth kl (m - n - 1) in
 777        if not (List.length tl > k) then false
 778        else
 779         List.fold_right
 780          (fun param i ->
 781            i && guarded_by_destructors context n nn kl x safes param
 782          ) tl true &&
 783          check_is_really_smaller_arg context n nn kl x safes (List.nth tl k)
 784    | C.Appl tl ->
 785       List.fold_right
 786        (fun t i -> i && guarded_by_destructors context n nn kl x safes t)
 787        tl true
 788    | C.Var (_,exp_named_subst)
 789    | C.Const (_,exp_named_subst)
 790    | C.MutInd (_,_,exp_named_subst)
 791    | C.MutConstruct (_,_,_,exp_named_subst) ->
 792       List.fold_right
 793        (fun (_,t) i -> i && guarded_by_destructors context n nn kl x safes t)
 794        exp_named_subst true
 795    | C.MutCase (uri,i,outtype,term,pl) ->
 796       (match term with
 797           C.Rel m when List.mem m safes || m = x ->
 798            let (tys,len,isinductive,paramsno,cl) =
 799             match CicEnvironment.get_obj uri with
 800                C.InductiveDefinition (tl,_,paramsno) ->
 801                 let (_,isinductive,_,cl) = List.nth tl i in
 802                  let tys =
 803                   List.map (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
 804                  in
 805                   let cl' =
 806                    List.map
 807                     (fun (id,ty) ->
 808                       (id, snd (split_prods tys paramsno ty))) cl
 809                   in
 810                    (tys,List.length tl,isinductive,paramsno,cl')
 811              | _ ->
 812                raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
 813            in
 814             if not isinductive then
 815              guarded_by_destructors context n nn kl x safes outtype &&
 816               guarded_by_destructors context n nn kl x safes term &&
 817               (*CSC: manca ??? il controllo sul tipo di term? *)
 818               List.fold_right
 819                (fun p i ->
 820                  i && guarded_by_destructors context n nn kl x safes p)
 821                pl true
 822             else
 823              guarded_by_destructors context n nn kl x safes outtype &&
 824               (*CSC: manca ??? il controllo sul tipo di term? *)
 825               List.fold_right
 826                (fun (p,(_,c)) i ->
 827                  let rl' =
 828                   let debrujinedte = debrujin_constructor uri len c in
 829                    recursive_args tys 0 len debrujinedte
 830                  in
 831                   let (e,safes',n',nn',x',context') =
 832                    get_new_safes context p c rl' safes n nn x
 833                   in
 834                    i &&
 835                    guarded_by_destructors context' n' nn' kl x' safes' e
 836                ) (List.combine pl cl) true
 837         | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
 838            let (tys,len,isinductive,paramsno,cl) =
 839             match CicEnvironment.get_obj uri with
 840                C.InductiveDefinition (tl,_,paramsno) ->
 841                 let (_,isinductive,_,cl) = List.nth tl i in
 842                  let tys =
 843                   List.map (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
 844                  in
 845                   let cl' =
 846                    List.map
 847                     (fun (id,ty) ->
 848                       (id, snd (split_prods tys paramsno ty))) cl
 849                   in
 850                    (tys,List.length tl,isinductive,paramsno,cl')
 851              | _ ->
 852                raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
 853            in
 854             if not isinductive then
 855              guarded_by_destructors context n nn kl x safes outtype &&
 856               guarded_by_destructors context n nn kl x safes term &&
 857               (*CSC: manca ??? il controllo sul tipo di term? *)
 858               List.fold_right
 859                (fun p i ->
 860                  i && guarded_by_destructors context n nn kl x safes p)
 861                pl true
 862             else
 863              guarded_by_destructors context n nn kl x safes outtype &&
 864               (*CSC: manca ??? il controllo sul tipo di term? *)
 865               List.fold_right
 866                (fun t i ->
 867                  i && guarded_by_destructors context n nn kl x safes t)
 868                tl true &&
 869               List.fold_right
 870                (fun (p,(_,c)) i ->
 871                  let rl' =
 872                   let debrujinedte = debrujin_constructor uri len c in
 873                    recursive_args tys 0 len debrujinedte
 874                  in
 875                   let (e, safes',n',nn',x',context') =
 876                    get_new_safes context p c rl' safes n nn x
 877                   in
 878                    i &&
 879                    guarded_by_destructors context' n' nn' kl x' safes' e
 880                ) (List.combine pl cl) true
 881         | _ ->
 882           guarded_by_destructors context n nn kl x safes outtype &&
 883            guarded_by_destructors context n nn kl x safes term &&
 884            (*CSC: manca ??? il controllo sul tipo di term? *)
 885            List.fold_right
 886             (fun p i -> i && guarded_by_destructors context n nn kl x safes p)
 887             pl true
 888       )
 889    | C.Fix (_, fl) ->
 890       let len = List.length fl in
 891        let n_plus_len = n + len
 892        and nn_plus_len = nn + len
 893        and x_plus_len = x + len
 894        and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
 895        and safes' = List.map (fun x -> x + len) safes in
 896         List.fold_right
 897          (fun (_,_,ty,bo) i ->
 898            i && guarded_by_destructors context n nn kl x_plus_len safes' ty &&
 899             guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
 900              x_plus_len safes' bo
 901          ) fl true
 902    | C.CoFix (_, fl) ->
 903       let len = List.length fl in
 904        let n_plus_len = n + len
 905        and nn_plus_len = nn + len
 906        and x_plus_len = x + len
 907        and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
 908        and safes' = List.map (fun x -> x + len) safes in
 909         List.fold_right
 910          (fun (_,ty,bo) i ->
 911            i &&
 912             guarded_by_destructors context n nn kl x_plus_len safes' ty &&
 913             guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
 914              x_plus_len safes' bo
 915          ) fl true
 916
 917 (* the boolean h means already protected *)
 918 (* args is the list of arguments the type of the constructor that may be *)
 919 (* found in head position must be applied to.                            *)
 920 (*CSC: coInductiveTypeURI non cambia mai di ricorsione in ricorsione *)
 921 and guarded_by_constructors context n nn h te args coInductiveTypeURI =
 922  let module C = Cic in
 923   (*CSC: There is a lot of code replication between the cases X and    *)
 924   (*CSC: (C.Appl X tl). Maybe it will be better to define a function   *)
 925   (*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *)
 926   match CicReduction.whd context te with
 927      C.Rel m when m > n && m <= nn -> h
 928    | C.Rel _ -> true
 929    | C.Meta _
 930    | C.Sort _
 931    | C.Implicit
 932    | C.Cast _
 933    | C.Prod _
 934    | C.LetIn _ ->
 935       raise (Impossible 17) (* the term has just been type-checked *)
 936    | C.Lambda (name,so,de) ->
 937       does_not_occur context n nn so &&
 938        guarded_by_constructors ((Some (name,(C.Decl so)))::context)
 939         (n + 1) (nn + 1) h de args coInductiveTypeURI
 940    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
 941       h &&
 942        List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
 943    | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) ->
 944       let consty =
 945        match CicEnvironment.get_cooked_obj ~trust:false uri with
 946           C.InductiveDefinition (itl,_,_) ->
 947            let (_,_,_,cl) = List.nth itl i in
 948             let (_,cons) = List.nth cl (j - 1) in
 949              CicSubstitution.subst_vars exp_named_subst cons
 950         | _ ->
 951          raise (WrongUriToMutualInductiveDefinitions
 952           (UriManager.string_of_uri uri))
 953       in
 954        let rec analyse_branch context ty te =
 955         match CicReduction.whd context ty with
 956            C.Meta _ -> raise (Impossible 34)
 957          | C.Rel _
 958          | C.Var _
 959          | C.Sort _ ->
 960             does_not_occur context n nn te
 961          | C.Implicit
 962          | C.Cast _ -> raise (Impossible 24) (* due to type-checking *)
 963          | C.Prod (name,so,de) ->
 964             analyse_branch ((Some (name,(C.Decl so)))::context) de te
 965          | C.Lambda _
 966          | C.LetIn _ -> raise (Impossible 25) (* due to type-checking *)
 967          | C.Appl ((C.MutInd (uri,_,_))::_) as ty
 968             when uri == coInductiveTypeURI ->
 969              guarded_by_constructors context n nn true te [] coInductiveTypeURI
 970          | C.Appl ((C.MutInd (uri,_,_))::_) as ty ->
 971             guarded_by_constructors context n nn true te tl coInductiveTypeURI
 972          | C.Appl _ ->
 973             does_not_occur context n nn te
 974          | C.Const _ -> raise (Impossible 26)
 975          | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
 976             guarded_by_constructors context n nn true te [] coInductiveTypeURI
 977          | C.MutInd _ ->
 978             does_not_occur context n nn te
 979          | C.MutConstruct _ -> raise (Impossible 27)
 980          (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
 981          (*CSC: in head position.                                       *)
 982          | C.MutCase _
 983          | C.Fix _
 984          | C.CoFix _ -> raise (Impossible 28) (* due to type-checking *)
 985        in
 986        let rec analyse_instantiated_type context ty l =
 987         match CicReduction.whd context ty with
 988            C.Rel _
 989          | C.Var _
 990          | C.Meta _
 991          | C.Sort _
 992          | C.Implicit
 993          | C.Cast _ -> raise (Impossible 29) (* due to type-checking *)
 994          | C.Prod (name,so,de) ->
 995             begin
 996              match l with
 997                 [] -> true
 998               | he::tl ->
 999                  analyse_branch context so he &&
1000                   analyse_instantiated_type ((Some (name,(C.Decl so)))::context)
1001                    de tl
1002             end
1003          | C.Lambda _
1004          | C.LetIn _ -> raise (Impossible 30) (* due to type-checking *)
1005          | C.Appl _ ->
1006             List.fold_left
1007              (fun i x -> i && does_not_occur context n nn x) true l
1008          | C.Const _ -> raise (Impossible 31)
1009          | C.MutInd _ ->
1010             List.fold_left
1011              (fun i x -> i && does_not_occur context n nn x) true l
1012          | C.MutConstruct _ -> raise (Impossible 32)
1013          (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
1014          (*CSC: in head position.                                       *)
1015          | C.MutCase _
1016          | C.Fix _
1017          | C.CoFix _ -> raise (Impossible 33) (* due to type-checking *)
1018        in
1019         let rec instantiate_type args consty =
1020          function
1021             [] -> true
1022           | tlhe::tltl as l ->
1023              let consty' = CicReduction.whd context consty in
1024               match args with
1025                  he::tl ->
1026                   begin
1027                    match consty' with
1028                       C.Prod (_,_,de) ->
1029                        let instantiated_de = CicSubstitution.subst he de in
1030                         (*CSC: siamo sicuri che non sia troppo forte? *)
1031                         does_not_occur context n nn tlhe &
1032                          instantiate_type tl instantiated_de tltl
1033                     | _ ->
1034                       (*CSC:We do not consider backbones with a MutCase, a    *)
1035                       (*CSC:FixPoint, a CoFixPoint and so on in head position.*)
1036                       raise (Impossible 23)
1037                   end
1038                | [] -> analyse_instantiated_type context consty' l
1039                   (* These are all the other cases *)
1040        in
1041         instantiate_type args consty tl
1042    | C.Appl ((C.CoFix (_,fl))::tl) ->
1043       List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
1044        let len = List.length fl in
1045         let n_plus_len = n + len
1046         and nn_plus_len = nn + len
1047         (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1048         and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1049          List.fold_right
1050           (fun (_,ty,bo) i ->
1051             i && does_not_occur context n nn ty &&
1052              guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1053               args coInductiveTypeURI
1054           ) fl true
1055    | C.Appl ((C.MutCase (_,_,out,te,pl))::tl) ->
1056        List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
1057         does_not_occur context n nn out &&
1058          does_not_occur context n nn te &&
1059           List.fold_right
1060            (fun x i ->
1061              i &&
1062              guarded_by_constructors context n nn h x args coInductiveTypeURI
1063            ) pl true
1064    | C.Appl l ->
1065       List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
1066    | C.Var (_,exp_named_subst)
1067    | C.Const (_,exp_named_subst) ->
1068       List.fold_right
1069        (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
1070    | C.MutInd _ -> assert false
1071    | C.MutConstruct (_,_,_,exp_named_subst) ->
1072       List.fold_right
1073        (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
1074    | C.MutCase (_,_,out,te,pl) ->
1075        does_not_occur context n nn out &&
1076         does_not_occur context n nn te &&
1077          List.fold_right
1078           (fun x i ->
1079             i &&
1080              guarded_by_constructors context n nn h x args coInductiveTypeURI
1081           ) pl true
1082    | C.Fix (_,fl) ->
1083       let len = List.length fl in
1084        let n_plus_len = n + len
1085        and nn_plus_len = nn + len
1086        (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1087        and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1088         List.fold_right
1089          (fun (_,_,ty,bo) i ->
1090            i && does_not_occur context n nn ty &&
1091             does_not_occur (tys@context) n_plus_len nn_plus_len bo
1092          ) fl true
1093    | C.CoFix (_,fl) ->
1094       let len = List.length fl in
1095        let n_plus_len = n + len
1096        and nn_plus_len = nn + len
1097        (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1098        and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1099         List.fold_right
1100          (fun (_,ty,bo) i ->
1101            i && does_not_occur context n nn ty &&
1102             guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1103              args coInductiveTypeURI
1104          ) fl true
1105
1106 and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 =
1107  let module C = Cic in
1108  let module U = UriManager in
1109   match (CicReduction.whd context arity1, CicReduction.whd context arity2) with
1110      (C.Prod (_,so1,de1), C.Prod (_,so2,de2))
1111       when CicReduction.are_convertible context so1 so2 ->
1112        check_allowed_sort_elimination context uri i need_dummy
1113         (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2
1114    | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true
1115    | (C.Sort C.Prop, C.Sort C.Set)
1116    | (C.Sort C.Prop, C.Sort C.Type) when need_dummy ->
1117 (*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *)
1118        (match CicEnvironment.get_obj uri with
1119            C.InductiveDefinition (itl,_,_) ->
1120             let (_,_,_,cl) = List.nth itl i in
1121              (* is a singleton definition or the empty proposition? *)
1122              List.length cl = 1 || List.length cl = 0
1123          | _ ->
1124            raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
1125        )
1126    | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true
1127    | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true
1128    | (C.Sort C.Set, C.Sort C.Type) when need_dummy ->
1129        (match CicEnvironment.get_obj uri with
1130            C.InductiveDefinition (itl,_,paramsno) ->
1131             let tys =
1132              List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1133             in
1134              let (_,_,_,cl) = List.nth itl i in
1135               List.fold_right
1136                (fun (_,x) i -> i && is_small tys paramsno x) cl true
1137          | _ ->
1138            raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
1139        )
1140    | (C.Sort C.Type, C.Sort _) when need_dummy -> true
1141    | (C.Sort C.Prop, C.Prod (name,so,ta)) when not need_dummy ->
1142        let res = CicReduction.are_convertible context so ind
1143        in
1144         res &&
1145         (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1146             C.Sort C.Prop -> true
1147           | C.Sort C.Set ->
1148              (match CicEnvironment.get_obj uri with
1149                  C.InductiveDefinition (itl,_,_) ->
1150                   let (_,_,_,cl) = List.nth itl i in
1151                    (* is a singleton definition? *)
1152                    List.length cl = 1
1153                | _ ->
1154                  raise (WrongUriToMutualInductiveDefinitions
1155                   (U.string_of_uri uri))
1156              )
1157           | _ -> false
1158         )
1159    | (C.Sort C.Set, C.Prod (name,so,ta)) when not need_dummy ->
1160        let res = CicReduction.are_convertible context so ind
1161        in
1162         res &&
1163         (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1164             C.Sort C.Prop
1165           | C.Sort C.Set  -> true
1166           | C.Sort C.Type ->
1167              (match CicEnvironment.get_obj uri with
1168                  C.InductiveDefinition (itl,_,paramsno) ->
1169                   let (_,_,_,cl) = List.nth itl i in
1170                    let tys =
1171                     List.map
1172                      (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1173                    in
1174                     List.fold_right
1175                      (fun (_,x) i -> i && is_small tys paramsno x) cl true
1176                | _ ->
1177                  raise (WrongUriToMutualInductiveDefinitions
1178                   (U.string_of_uri uri))
1179              )
1180           | _ -> raise (Impossible 19)
1181         )
1182    | (C.Sort C.Type, C.Prod (_,so,_)) when not need_dummy ->
1183        CicReduction.are_convertible context so ind
1184    | (_,_) -> false
1185
1186 and type_of_branch context argsno need_dummy outtype term constype =
1187  let module C = Cic in
1188  let module R = CicReduction in
1189   match R.whd context constype with
1190      C.MutInd (_,_,_) ->
1191       if need_dummy then
1192        outtype
1193       else
1194        C.Appl [outtype ; term]
1195    | C.Appl (C.MutInd (_,_,_)::tl) ->
1196       let (_,arguments) = split tl argsno
1197       in
1198        if need_dummy && arguments = [] then
1199         outtype
1200        else
1201         C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
1202    | C.Prod (name,so,de) ->
1203       let term' =
1204        match CicSubstitution.lift 1 term with
1205           C.Appl l -> C.Appl (l@[C.Rel 1])
1206         | t -> C.Appl [t ; C.Rel 1]
1207       in
1208        C.Prod (C.Anonymous,so,type_of_branch
1209         ((Some (name,(C.Decl so)))::context) argsno need_dummy
1210         (CicSubstitution.lift 1 outtype) term' de)
1211   | _ -> raise (Impossible 20)
1212
1213 (* check_metasenv_consistency checks that the "canonical" context of a
1214 metavariable is consitent - up to relocation via the relocation list l -
1215 with the actual context *)
1216
1217 and check_metasenv_consistency metasenv context canonical_context l =
1218   let module C = Cic in
1219   let module R = CicReduction in
1220   let module S = CicSubstitution in
1221    let lifted_canonical_context =
1222     let rec aux i =
1223      function
1224         [] -> []
1225       | (Some (n,C.Decl t))::tl ->
1226          (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
1227       | (Some (n,C.Def t))::tl ->
1228          (Some (n,C.Def (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
1229       | None::tl -> None::(aux (i+1) tl)
1230     in
1231      aux 1 canonical_context
1232    in
1233     List.iter2
1234      (fun t ct ->
1235        let res =
1236         match (t,ct) with
1237            _,None -> true
1238          | Some t,Some (_,C.Def ct) ->
1239             R.are_convertible context t ct
1240          | Some t,Some (_,C.Decl ct) ->
1241             R.are_convertible context (type_of_aux' metasenv context t) ct
1242          | _, _  -> false
1243        in
1244         if not res then raise MetasenvInconsistency
1245      ) l lifted_canonical_context
1246
1247 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
1248 and type_of_aux' metasenv context t =
1249  let rec type_of_aux context =
1250   let module C = Cic in
1251   let module R = CicReduction in
1252   let module S = CicSubstitution in
1253   let module U = UriManager in
1254    function
1255       C.Rel n ->
1256        (try
1257          match List.nth context (n - 1) with
1258             Some (_,C.Decl t) -> S.lift n t
1259           | Some (_,C.Def bo) -> type_of_aux context (S.lift n bo)
1260           | None -> raise RelToHiddenHypothesis
1261         with
1262          _ -> raise (NotWellTyped "Not a close term")
1263        )
1264     | C.Var (uri,exp_named_subst) ->
1265       incr fdebug ;
1266       check_exp_named_subst context exp_named_subst ;
1267       let ty =
1268        CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
1269       in
1270        decr fdebug ;
1271        ty
1272     | C.Meta (n,l) ->
1273        let (_,canonical_context,ty) =
1274         List.find (function (m,_,_) -> n = m) metasenv
1275        in
1276         check_metasenv_consistency metasenv context canonical_context l;
1277         CicSubstitution.lift_meta l ty
1278     | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
1279     | C.Implicit -> raise (Impossible 21)
1280     | C.Cast (te,ty) ->
1281        let _ = type_of_aux context ty in
1282         if R.are_convertible context (type_of_aux context te) ty then ty
1283         else raise (NotWellTyped "Cast")
1284     | C.Prod (name,s,t) ->
1285        let sort1 = type_of_aux context s
1286        and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in
1287         sort_of_prod context (name,s) (sort1,sort2)
1288    | C.Lambda (n,s,t) ->
1289        let sort1 = type_of_aux context s
1290        and type2 = type_of_aux ((Some (n,(C.Decl s)))::context) t in
1291         let sort2 = type_of_aux ((Some (n,(C.Decl s)))::context) type2 in
1292          (* only to check if the product is well-typed *)
1293          let _ = sort_of_prod context (n,s) (sort1,sort2) in
1294           C.Prod (n,s,type2)
1295    | C.LetIn (n,s,t) ->
1296       (* only to check if s is well-typed *)
1297       let _ = type_of_aux context s in
1298        (* The type of a LetIn is a LetIn. Extremely slow since the computed
1299           LetIn is later reduced and maybe also re-checked.
1300        (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t))
1301        *)
1302        (* The type of the LetIn is reduced. Much faster than the previous
1303           solution. Moreover the inferred type is probably very different
1304           from the expected one.
1305        (CicReduction.whd context
1306         (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)))
1307        *)
1308        (* One-step LetIn reduction. Even faster than the previous solution.
1309           Moreover the inferred type is closer to the expected one. *)
1310        (CicSubstitution.subst s
1311         (type_of_aux ((Some (n,(C.Def s)))::context) t))
1312    | C.Appl (he::tl) when List.length tl > 0 ->
1313       let hetype = type_of_aux context he
1314       and tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in
1315        eat_prods context hetype tlbody_and_type
1316    | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
1317    | C.Const (uri,exp_named_subst) ->
1318       incr fdebug ;
1319       check_exp_named_subst context exp_named_subst ;
1320       let cty =
1321        CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
1322       in
1323        decr fdebug ;
1324        cty
1325    | C.MutInd (uri,i,exp_named_subst) ->
1326       incr fdebug ;
1327       check_exp_named_subst context exp_named_subst ;
1328       let cty =
1329        CicSubstitution.subst_vars exp_named_subst
1330         (type_of_mutual_inductive_defs uri i)
1331       in
1332        decr fdebug ;
1333        cty
1334    | C.MutConstruct (uri,i,j,exp_named_subst) ->
1335       check_exp_named_subst context exp_named_subst ;
1336       let cty =
1337        CicSubstitution.subst_vars exp_named_subst
1338         (type_of_mutual_inductive_constr uri i j)
1339       in
1340        cty
1341    | C.MutCase (uri,i,outtype,term,pl) ->
1342       let outsort = type_of_aux context outtype in
1343       let (need_dummy, k) =
1344        let rec guess_args context t =
1345         match CicReduction.whd context t with
1346            C.Sort _ -> (true, 0)
1347          | C.Prod (name, s, t) ->
1348             let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
1349              if n = 0 then
1350               (* last prod before sort *)
1351               match CicReduction.whd context s with
1352 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1353                  C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
1354                   (false, 1)
1355 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1356                | C.Appl ((C.MutInd (uri',i',_)) :: _)
1357                   when U.eq uri' uri && i' = i -> (false, 1)
1358                | _ -> (true, 1)
1359              else
1360               (b, n + 1)
1361          | _ -> raise (NotWellTyped "MutCase: outtype ill-formed")
1362        in
1363         (*CSC whd non serve dopo type_of_aux ? *)
1364         let (b, k) = guess_args context outsort in
1365          if not b then (b, k - 1) else (b, k)
1366       in
1367       let (parameters, arguments, exp_named_subst) =
1368         match R.whd context (type_of_aux context term) with
1369            (*CSC manca il caso dei CAST *)
1370 (*CSC: ma servono i parametri (uri,i)? Se si', perche' non serve anche il *)
1371 (*CSC: parametro exp_named_subst? Se no, perche' non li togliamo?         *)
1372 (*CSC: Hint: nella DTD servono per gli stylesheet.                        *)
1373            C.MutInd (uri',i',exp_named_subst) as typ ->
1374             if U.eq uri uri' && i = i' then ([],[],exp_named_subst)
1375             else raise (NotWellTyped ("MutCase: the term is of type " ^
1376              CicPp.ppterm typ ^
1377              " instead of type " ^ (U.string_of_uri uri) ^ "#1/" ^
1378              string_of_int i ^ "{_}"))
1379          | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) ->
1380             if U.eq uri uri' && i = i' then
1381              let params,args =
1382               split tl (List.length tl - k)
1383              in params,args,exp_named_subst
1384             else raise (NotWellTyped ("MutCase: the term is of type " ^
1385              CicPp.ppterm typ ^
1386              " instead of type " ^ (U.string_of_uri uri) ^ "#1/" ^
1387              string_of_int i ^ "{_}"))
1388          | _ -> raise (NotWellTyped "MutCase: the term is not an inductive one")
1389       in
1390        (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
1391        let sort_of_ind_type =
1392         if parameters = [] then
1393          C.MutInd (uri,i,exp_named_subst)
1394         else
1395          C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters)
1396        in
1397         if not (check_allowed_sort_elimination context uri i need_dummy
1398          sort_of_ind_type (type_of_aux context sort_of_ind_type) outsort)
1399         then
1400          raise (NotWellTyped "MutCase: not allowed sort elimination") ;
1401
1402         (* let's check if the type of branches are right *)
1403         let parsno =
1404          match CicEnvironment.get_cooked_obj ~trust:false uri with
1405             C.InductiveDefinition (_,_,parsno) -> parsno
1406           | _ ->
1407             raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
1408         in
1409          let (_,branches_ok) =
1410           List.fold_left
1411            (fun (j,b) p ->
1412              let cons =
1413               if parameters = [] then
1414                (C.MutConstruct (uri,i,j,exp_named_subst))
1415               else
1416                (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
1417              in
1418 (*
1419               (j + 1, b &&
1420 *)
1421               (j + 1,
1422 let res = b &&
1423                R.are_convertible context (type_of_aux context p)
1424                 (type_of_branch context parsno need_dummy outtype cons
1425                   (type_of_aux context cons))
1426 in if not res then prerr_endline ("#### " ^ CicPp.ppterm (type_of_aux context p) ^ " <==> " ^ CicPp.ppterm (type_of_branch context parsno need_dummy outtype cons (type_of_aux context cons))) ; res
1427               )
1428            ) (1,true) pl
1429          in
1430           if not branches_ok then
1431            raise (NotWellTyped "MutCase: wrong type of a branch") ;
1432
1433           if not need_dummy then
1434            C.Appl ((outtype::arguments)@[term])
1435           else if arguments = [] then
1436            outtype
1437           else
1438            C.Appl (outtype::arguments)
1439    | C.Fix (i,fl) ->
1440       let types_times_kl =
1441        List.rev
1442         (List.map
1443           (fun (n,k,ty,_) ->
1444             let _ = type_of_aux context ty in
1445              (Some (C.Name n,(C.Decl ty)),k)) fl)
1446       in
1447       let (types,kl) = List.split types_times_kl in
1448        let len = List.length types in
1449         List.iter
1450          (fun (name,x,ty,bo) ->
1451            if
1452             (R.are_convertible (types@context) (type_of_aux (types@context) bo)
1453              (CicSubstitution.lift len ty))
1454            then
1455             begin
1456              let (m, eaten, context') =
1457               eat_lambdas (types @ context) (x + 1) bo
1458              in
1459               (*let's control the guarded by destructors conditions D{f,k,x,M}*)
1460               if
1461                not
1462                 (guarded_by_destructors context' eaten (len + eaten) kl 1 [] m)
1463               then
1464                raise (NotWellTyped "Fix: not guarded by destructors")
1465             end
1466            else
1467             raise (NotWellTyped "Fix: ill-typed bodies")
1468          ) fl ;
1469
1470         (*CSC: controlli mancanti solo su D{f,k,x,M} *)
1471         let (_,_,ty,_) = List.nth fl i in
1472         ty
1473    | C.CoFix (i,fl) ->
1474       let types =
1475        List.rev
1476         (List.map
1477           (fun (n,ty,_) ->
1478             let _ = type_of_aux context ty in Some (C.Name n,(C.Decl ty))) fl)
1479       in
1480        let len = List.length types in
1481         List.iter
1482          (fun (_,ty,bo) ->
1483            if
1484             (R.are_convertible (types @ context)
1485              (type_of_aux (types @ context) bo) (CicSubstitution.lift len ty))
1486            then
1487             begin
1488              (* let's control that the returned type is coinductive *)
1489              match returns_a_coinductive context ty with
1490                 None ->
1491                  raise(NotWellTyped "CoFix: does not return a coinductive type")
1492               | Some uri ->
1493                  (*let's control the guarded by constructors conditions C{f,M}*)
1494                  if
1495                   not
1496                    (guarded_by_constructors (types @ context) 0 len false bo
1497                      [] uri)
1498                  then
1499                   raise (NotWellTyped "CoFix: not guarded by constructors")
1500             end
1501            else
1502             raise (NotWellTyped "CoFix: ill-typed bodies")
1503          ) fl ;
1504
1505         let (_,ty,_) = List.nth fl i in
1506          ty
1507
1508  and check_exp_named_subst context =
1509   let rec check_exp_named_subst_aux substs =
1510    function
1511       [] -> ()
1512     | ((uri,t) as subst)::tl ->
1513        let typeofvar =
1514         CicSubstitution.subst_vars substs (type_of_variable uri) in
1515        (match CicEnvironment.get_cooked_obj ~trust:false uri with
1516            Cic.Variable (_,Some bo,_,_) ->
1517             raise
1518              (NotWellTyped
1519                "A variable with a body can not be explicit substituted")
1520          | Cic.Variable (_,None,_,_) -> ()
1521          | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
1522        ) ;
1523        let typeoft = type_of_aux context t in
1524         if CicReduction.are_convertible context typeoft typeofvar then
1525          check_exp_named_subst_aux (substs@[subst]) tl
1526         else
1527          begin
1528           CicReduction.fdebug := 0 ;
1529           ignore (CicReduction.are_convertible context typeoft typeofvar) ;
1530           fdebug := 0 ;
1531           debug typeoft [typeofvar] ;
1532           raise (NotWellTyped "Wrong Explicit Named Substitution")
1533          end
1534   in
1535    check_exp_named_subst_aux []
1536
1537  and sort_of_prod context (name,s) (t1, t2) =
1538   let module C = Cic in
1539    let t1' = CicReduction.whd context t1 in
1540    let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
1541    match (t1', t2') with
1542       (C.Sort s1, C.Sort s2)
1543         when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *)
1544          C.Sort s2
1545     | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
1546     | (_,_) ->
1547       raise
1548        (NotWellTyped
1549         ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= " ^ CicPp.ppterm t2'))
1550
1551  and eat_prods context hetype =
1552   (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
1553   (*CSC: cucinati                                                         *)
1554   function
1555      [] -> hetype
1556    | (hete, hety)::tl ->
1557     (match (CicReduction.whd context hetype) with
1558         Cic.Prod (n,s,t) ->
1559          if CicReduction.are_convertible context s hety then
1560           (CicReduction.fdebug := -1 ;
1561            eat_prods context (CicSubstitution.subst hete t) tl
1562           )
1563          else
1564           begin
1565            CicReduction.fdebug := 0 ;
1566            ignore (CicReduction.are_convertible context s hety) ;
1567            fdebug := 0 ;
1568            debug s [hety] ;
1569            raise (NotWellTyped "Appl: wrong parameter-type")
1570           end
1571       | _ -> raise (NotWellTyped "Appl: wrong Prod-type")
1572     )
1573
1574  and returns_a_coinductive context ty =
1575   let module C = Cic in
1576    match CicReduction.whd context ty with
1577       C.MutInd (uri,i,_) ->
1578        (*CSC: definire una funzioncina per questo codice sempre replicato *)
1579        (match CicEnvironment.get_cooked_obj ~trust:false uri with
1580            C.InductiveDefinition (itl,_,_) ->
1581             let (_,is_inductive,_,_) = List.nth itl i in
1582              if is_inductive then None else (Some uri)
1583          | _ ->
1584            raise (WrongUriToMutualInductiveDefinitions
1585             (UriManager.string_of_uri uri))
1586         )
1587     | C.Appl ((C.MutInd (uri,i,_))::_) ->
1588        (match CicEnvironment.get_obj uri with
1589            C.InductiveDefinition (itl,_,_) ->
1590             let (_,is_inductive,_,_) = List.nth itl i in
1591              if is_inductive then None else (Some uri)
1592          | _ ->
1593            raise (WrongUriToMutualInductiveDefinitions
1594             (UriManager.string_of_uri uri))
1595         )
1596     | C.Prod (n,so,de) ->
1597        returns_a_coinductive ((Some (n,C.Decl so))::context) de
1598     | _ -> None
1599
1600  in
1601 (*CSC
1602 prerr_endline ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t) ; flush stderr ;
1603 let res =
1604 *)
1605   type_of_aux context t
1606 (*
1607 in prerr_endline "FINE TYPE_OF_AUX" ; flush stderr ; res
1608 *)
1609
1610 (* is a small constructor? *)
1611 (*CSC: ottimizzare calcolando staticamente *)
1612 and is_small context paramsno c =
1613  let rec is_small_aux context c =
1614   let module C = Cic in
1615    match CicReduction.whd context c with
1616       C.Prod (n,so,de) ->
1617        (*CSC: [] is an empty metasenv. Is it correct? *)
1618        let s = type_of_aux' [] context so in
1619         (s = C.Sort C.Prop || s = C.Sort C.Set) &&
1620         is_small_aux ((Some (n,(C.Decl so)))::context) de
1621     | _ -> true (*CSC: we trust the type-checker *)
1622  in
1623   let (context',dx) = split_prods context paramsno c in
1624    is_small_aux context' dx
1625
1626 and type_of t =
1627 (*CSC
1628 prerr_endline ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t) ; flush stderr ;
1629 let res =
1630 *)
1631  type_of_aux' [] [] t
1632 (*CSC
1633 in prerr_endline "FINE TYPE_OF_AUX'" ; flush stderr ; res
1634 *)
1635 ;;
1636
1637 let typecheck uri =
1638  let module C = Cic in
1639  let module R = CicReduction in
1640  let module U = UriManager in
1641   match CicEnvironment.is_type_checked ~trust:false uri with
1642      CicEnvironment.CheckedObj _ -> ()
1643    | CicEnvironment.UncheckedObj uobj ->
1644       (* let's typecheck the uncooked object *)
1645       Logger.log (`Start_type_checking uri) ;
1646       (match uobj with
1647           C.Constant (_,Some te,ty,_) ->
1648            let _ = type_of ty in
1649             if not (R.are_convertible [] (type_of te ) ty) then
1650              raise (NotWellTyped ("Constant " ^ (U.string_of_uri uri)))
1651         | C.Constant (_,None,ty,_) ->
1652           (* only to check that ty is well-typed *)
1653           let _ = type_of ty in ()
1654         | C.CurrentProof (_,conjs,te,ty,_) ->
1655            let _ =
1656             List.fold_left
1657              (fun metasenv ((_,context,ty) as conj) ->
1658                ignore (type_of_aux' metasenv context ty) ;
1659                metasenv @ [conj]
1660              ) [] conjs
1661            in
1662             let _ = type_of_aux' conjs [] ty in
1663              if not (R.are_convertible [] (type_of_aux' conjs [] te) ty)
1664              then
1665               raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))
1666         | C.Variable (_,bo,ty,_) ->
1667            (* only to check that ty is well-typed *)
1668            let _ = type_of ty in
1669             (match bo with
1670                 None -> ()
1671               | Some bo ->
1672                  if not (R.are_convertible [] (type_of bo) ty) then
1673                   raise (NotWellTyped ("Variable" ^ (U.string_of_uri uri)))
1674             )
1675         | C.InductiveDefinition _ ->
1676            check_mutual_inductive_defs uri uobj
1677       ) ;
1678       CicEnvironment.set_type_checking_info uri ;
1679       Logger.log (`Type_checking_completed uri)
1680 ;;