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