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