helm/interface/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 NotImplemented;;
  27 exception Impossible;;
  28 exception NotWellTyped of string;;
  29 exception WrongUriToConstant of string;;
  30 exception WrongUriToVariable of string;;
  31 exception WrongUriToMutualInductiveDefinitions of string;;
  32 exception ListTooShort;;
  33 exception NotPositiveOccurrences of string;;
  34 exception NotWellFormedTypeOfInductiveConstructor of string;;
  35 exception WrongRequiredArgument of string;;
  36
  37 let fdebug = ref 0;;
  38 let debug t env =
  39  let rec debug_aux t i =
  40   let module C = Cic in
  41   let module U = UriManager in
  42    CicPp.ppobj (C.Variable ("DEBUG", None,
  43     C.Prod (C.Name "-15", C.Const (U.uri_of_string "cic:/dummy-15",0),
  44     C.Prod (C.Name "-14", C.Const (U.uri_of_string "cic:/dummy-14",0),
  45     C.Prod (C.Name "-13", C.Const (U.uri_of_string "cic:/dummy-13",0),
  46     C.Prod (C.Name "-12", C.Const (U.uri_of_string "cic:/dummy-12",0),
  47     C.Prod (C.Name "-11", C.Const (U.uri_of_string "cic:/dummy-11",0),
  48     C.Prod (C.Name "-10", C.Const (U.uri_of_string "cic:/dummy-10",0),
  49     C.Prod (C.Name "-9", C.Const (U.uri_of_string "cic:/dummy-9",0),
  50     C.Prod (C.Name "-8", C.Const (U.uri_of_string "cic:/dummy-8",0),
  51     C.Prod (C.Name "-7", C.Const (U.uri_of_string "cic:/dummy-7",0),
  52     C.Prod (C.Name "-6", C.Const (U.uri_of_string "cic:/dummy-6",0),
  53      C.Prod (C.Name "-5", C.Const (U.uri_of_string "cic:/dummy-5",0),
  54       C.Prod (C.Name "-4", C.Const (U.uri_of_string "cic:/dummy-4",0),
  55        C.Prod (C.Name "-3", C.Const (U.uri_of_string "cic:/dummy-3",0),
  56         C.Prod (C.Name "-2", C.Const (U.uri_of_string "cic:/dummy-2",0),
  57          C.Prod (C.Name "-1", C.Const (U.uri_of_string "cic:/dummy-1",0),
  58           t
  59          )
  60         )
  61        )
  62       )
  63      )
  64     )
  65     )
  66     )
  67     )))))))
  68     )) ^ "\n" ^ i
  69  in
  70   if !fdebug = 0 then
  71    raise (NotWellTyped ("\n" ^ List.fold_right debug_aux (t::env) ""))
  72    (*print_endline ("\n" ^ List.fold_right debug_aux (t::env) "") ; flush stdout*)
  73 ;;
  74
  75 let rec split l n =
  76  match (l,n) with
  77     (l,0) -> ([], l)
  78   | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
  79   | (_,_) -> raise ListTooShort
  80 ;;
  81
  82 exception CicCacheError;;
  83
  84 let rec cooked_type_of_constant uri cookingsno =
  85  let module C = Cic in
  86  let module R = CicReduction in
  87  let module U = UriManager in
  88   let cobj =
  89    match CicCache.is_type_checked uri cookingsno with
  90       CicCache.CheckedObj cobj -> cobj
  91     | CicCache.UncheckedObj uobj ->
  92        (* let's typecheck the uncooked obj *)
  93        (match uobj with
  94            C.Definition (_,te,ty,_) ->
  95              let _ = type_of ty in
  96               if not (R.are_convertible (type_of te) ty) then
  97                raise (NotWellTyped ("Constant " ^ (U.string_of_uri uri)))
  98          | C.Axiom (_,ty,_) ->
  99            (* only to check that ty is well-typed *)
 100            let _ = type_of ty in ()
 101          | C.CurrentProof (_,_,te,ty) ->
 102              let _ = type_of ty in
 103               if not (R.are_convertible (type_of te) ty) then
 104                raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))
 105          | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
 106        ) ;
 107        CicCache.set_type_checking_info uri ;
 108        match CicCache.is_type_checked uri cookingsno with
 109           CicCache.CheckedObj cobj -> cobj
 110         | CicCache.UncheckedObj _ -> raise CicCacheError
 111   in
 112    match cobj with
 113       C.Definition (_,_,ty,_) -> ty
 114     | C.Axiom (_,ty,_) -> ty
 115     | C.CurrentProof (_,_,_,ty) -> ty
 116     | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
 117
 118 and type_of_variable uri =
 119  let module C = Cic in
 120  let module R = CicReduction in
 121  let module U = UriManager in
 122   (* 0 because a variable is never cooked => no partial cooking at one level *)
 123   match CicCache.is_type_checked uri 0 with
 124      CicCache.CheckedObj (C.Variable (_,_,ty)) -> ty
 125    | CicCache.UncheckedObj (C.Variable (_,bo,ty)) ->
 126       (* only to check that ty is well-typed *)
 127       let _ = type_of ty in
 128        (match bo with
 129            None -> ()
 130          | Some bo ->
 131             if not (R.are_convertible (type_of bo) ty) then
 132              raise (NotWellTyped ("Variable " ^ (U.string_of_uri uri)))
 133        ) ;
 134        CicCache.set_type_checking_info uri ;
 135        ty
 136    |  _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
 137
 138 and does_not_occur n nn te =
 139  let module C = Cic in
 140    (*CSC: whd sembra essere superflua perche' un caso in cui l'occorrenza *)
 141    (*CSC: venga mangiata durante la whd sembra presentare problemi di *)
 142    (*CSC: universi                                                    *)
 143    match CicReduction.whd te with
 144       C.Rel m when m > n && m <= nn -> false
 145     | C.Rel _
 146     | C.Var _
 147     | C.Meta _
 148     | C.Sort _
 149     | C.Implicit -> true
 150     | C.Cast (te,ty) -> does_not_occur n nn te && does_not_occur n nn ty
 151     | C.Prod (_,so,dest) ->
 152        does_not_occur n nn so && does_not_occur (n + 1) (nn + 1) dest
 153     | C.Lambda (_,so,dest) ->
 154        does_not_occur n nn so && does_not_occur (n + 1) (nn + 1) dest
 155     | C.LetIn (_,so,dest) ->
 156        does_not_occur n nn so && does_not_occur (n + 1) (nn + 1) dest
 157     | C.Appl l ->
 158        List.fold_right (fun x i -> i && does_not_occur n nn x) l true
 159     | C.Const _
 160     | C.Abst _
 161     | C.MutInd _
 162     | C.MutConstruct _ -> true
 163     | C.MutCase (_,_,_,out,te,pl) ->
 164        does_not_occur n nn out && does_not_occur n nn te &&
 165         List.fold_right (fun x i -> i && does_not_occur n nn x) pl true
 166     | C.Fix (_,fl) ->
 167        let len = List.length fl in
 168         let n_plus_len = n + len in
 169         let nn_plus_len = nn + len in
 170          List.fold_right
 171           (fun (_,_,ty,bo) i ->
 172             i && does_not_occur n_plus_len nn_plus_len ty &&
 173             does_not_occur n_plus_len nn_plus_len bo
 174           ) fl true
 175     | C.CoFix (_,fl) ->
 176        let len = List.length fl in
 177         let n_plus_len = n + len in
 178         let nn_plus_len = nn + len in
 179          List.fold_right
 180           (fun (_,ty,bo) i ->
 181             i && does_not_occur n_plus_len nn_plus_len ty &&
 182             does_not_occur n_plus_len nn_plus_len bo
 183           ) fl true
 184
 185 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
 186 (*CSC questa funzione e' simile alla are_all_occurrences_positive, ma fa *)
 187 (*CSC dei controlli leggermente diversi. Viene invocata solamente dalla  *)
 188 (*CSC strictly_positive                                                  *)
 189 (*CSC definizione (giusta???) tratta dalla mail di Hugo ;-)              *)
 190 and weakly_positive n nn uri te =
 191  let module C = Cic in
 192   (*CSC mettere in cicSubstitution *)
 193   let rec subst_inductive_type_with_dummy_rel =
 194    function
 195       C.MutInd (uri',_,0) when UriManager.eq uri' uri ->
 196        C.Rel 0 (* dummy rel *)
 197     | C.Appl ((C.MutInd (uri',_,0))::tl) when UriManager.eq uri' uri ->
 198        C.Rel 0 (* dummy rel *)
 199     | C.Cast (te,ty) -> subst_inductive_type_with_dummy_rel te
 200     | C.Prod (name,so,ta) ->
 201        C.Prod (name, subst_inductive_type_with_dummy_rel so,
 202         subst_inductive_type_with_dummy_rel ta)
 203     | C.Lambda (name,so,ta) ->
 204        C.Lambda (name, subst_inductive_type_with_dummy_rel so,
 205         subst_inductive_type_with_dummy_rel ta)
 206     | C.Appl tl ->
 207        C.Appl (List.map subst_inductive_type_with_dummy_rel tl)
 208     | C.MutCase (uri,cookingsno,i,outtype,term,pl) ->
 209        C.MutCase (uri,cookingsno,i,
 210         subst_inductive_type_with_dummy_rel outtype,
 211         subst_inductive_type_with_dummy_rel term,
 212         List.map subst_inductive_type_with_dummy_rel pl)
 213     | C.Fix (i,fl) ->
 214        C.Fix (i,List.map (fun (name,i,ty,bo) -> (name,i,
 215         subst_inductive_type_with_dummy_rel ty,
 216         subst_inductive_type_with_dummy_rel bo)) fl)
 217     | C.CoFix (i,fl) ->
 218        C.CoFix (i,List.map (fun (name,ty,bo) -> (name,
 219         subst_inductive_type_with_dummy_rel ty,
 220         subst_inductive_type_with_dummy_rel bo)) fl)
 221     | t -> t
 222   in
 223   match CicReduction.whd te with
 224      C.Appl ((C.MutInd (uri',_,0))::tl) when UriManager.eq uri' uri -> true
 225    | C.MutInd (uri',_,0) when UriManager.eq uri' uri -> true
 226    | C.Prod (C.Anonimous,source,dest) ->
 227       strictly_positive n nn (subst_inductive_type_with_dummy_rel source) &&
 228        weakly_positive (n + 1) (nn + 1) uri dest
 229    | C.Prod (name,source,dest) when does_not_occur 0 n dest ->
 230       (* dummy abstraction, so we behave as in the anonimous case *)
 231       strictly_positive n nn (subst_inductive_type_with_dummy_rel source) &&
 232        weakly_positive (n + 1) (nn + 1) uri dest
 233    | C.Prod (_,source,dest) ->
 234       does_not_occur n nn (subst_inductive_type_with_dummy_rel source) &&
 235        weakly_positive (n + 1) (nn + 1) uri dest
 236    | _ -> raise (NotWellFormedTypeOfInductiveConstructor ("Guess where the error is ;-)"))
 237
 238 (* instantiate_parameters ps (x1:T1)...(xn:Tn)C                             *)
 239 (* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *)
 240 and instantiate_parameters params c =
 241  let module C = Cic in
 242   match (c,params) with
 243      (c,[]) -> c
 244    | (C.Prod (_,_,ta), he::tl) ->
 245        instantiate_parameters tl
 246         (CicSubstitution.subst he ta)
 247    | (C.Cast (te,_), _) -> instantiate_parameters params te
 248    | (t,l) -> raise Impossible
 249
 250 and strictly_positive n nn te =
 251  let module C = Cic in
 252  let module U = UriManager in
 253   match CicReduction.whd te with
 254      C.Rel _ -> true
 255    | C.Cast (te,ty) ->
 256       (*CSC: bisogna controllare ty????*)
 257       strictly_positive n nn te
 258    | C.Prod (_,so,ta) ->
 259       does_not_occur n nn so &&
 260        strictly_positive (n+1) (nn+1) ta
 261    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
 262       List.fold_right (fun x i -> i && does_not_occur n nn x) tl true
 263    | C.Appl ((C.MutInd (uri,_,i))::tl) ->
 264       let (ok,paramsno,cl) =
 265        match CicCache.get_obj uri with
 266            C.InductiveDefinition (tl,_,paramsno) ->
 267             let (_,_,_,cl) = List.nth tl i in
 268              (List.length tl = 1, paramsno, cl)
 269          | _ -> raise(WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
 270       in
 271        let (params,arguments) = split tl paramsno in
 272        let lifted_params = List.map (CicSubstitution.lift 1) params in
 273        let cl' =
 274         List.map (fun (_,te,_) -> instantiate_parameters lifted_params te) cl
 275        in
 276         ok &&
 277          List.fold_right
 278           (fun x i -> i && does_not_occur n nn x)
 279           arguments true &&
 280          (*CSC: MEGAPATCH3 (sara' quella giusta?)*)
 281          List.fold_right
 282           (fun x i ->
 283             i &&
 284              weakly_positive (n+1) (nn+1) uri x
 285           ) cl' true
 286    | C.MutInd (uri,_,i) ->
 287       (match CicCache.get_obj uri with
 288           C.InductiveDefinition (tl,_,_) ->
 289            List.length tl = 1
 290         | _ -> raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
 291       )
 292    | t -> does_not_occur n nn t
 293
 294 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
 295 and are_all_occurrences_positive uri indparamsno i n nn te =
 296  let module C = Cic in
 297   match CicReduction.whd te with
 298      C.Appl ((C.Rel m)::tl) when m = i ->
 299       (*CSC: riscrivere fermandosi a 0 *)
 300       (* let's check if the inductive type is applied at least to *)
 301       (* indparamsno parameters                                   *)
 302       let last =
 303        List.fold_left
 304         (fun k x ->
 305           if k = 0 then 0
 306           else
 307            match CicReduction.whd x with
 308               C.Rel m when m = n - (indparamsno - k) -> k - 1
 309             | _ -> raise (WrongRequiredArgument (UriManager.string_of_uri uri))
 310         ) indparamsno tl
 311       in
 312        if last = 0 then
 313         List.fold_right (fun x i -> i && does_not_occur n nn x) tl true
 314        else
 315         raise (WrongRequiredArgument (UriManager.string_of_uri uri))
 316    | C.Rel m when m = i ->
 317       if indparamsno = 0 then
 318        true
 319       else
 320        raise (WrongRequiredArgument (UriManager.string_of_uri uri))
 321    | C.Prod (C.Anonimous,source,dest) ->
 322       strictly_positive n nn source &&
 323        are_all_occurrences_positive uri indparamsno (i+1) (n + 1) (nn + 1) dest
 324    | C.Prod (name,source,dest) when does_not_occur 0 n dest ->
 325       (* dummy abstraction, so we behave as in the anonimous case *)
 326       strictly_positive n nn source &&
 327        are_all_occurrences_positive uri indparamsno (i+1) (n + 1) (nn + 1) dest
 328    | C.Prod (_,source,dest) ->
 329       does_not_occur n nn source &&
 330        are_all_occurrences_positive uri indparamsno (i+1) (n + 1) (nn + 1) dest
 331    | _ -> raise (NotWellFormedTypeOfInductiveConstructor (UriManager.string_of_uri uri))
 332
 333 (*CSC: cambiare il nome, torna unit! *)
 334 and cooked_mutual_inductive_defs uri =
 335  let module U = UriManager in
 336   function
 337      Cic.InductiveDefinition (itl, _, indparamsno) ->
 338       (* let's check if the arity of the inductive types are well *)
 339       (* formed                                                   *)
 340       List.iter (fun (_,_,x,_) -> let _ = type_of x in ()) itl ;
 341
 342       (* let's check if the types of the inductive constructors  *)
 343       (* are well formed.                                        *)
 344       (* In order not to use type_of_aux we put the types of the *)
 345       (* mutual inductive types at the head of the types of the  *)
 346       (* constructors using Prods                                *)
 347       (*CSC: piccola??? inefficienza                             *)
 348       let len = List.length itl in
 349        let _ =
 350         List.fold_right
 351          (fun (_,_,_,cl) i ->
 352            List.iter
 353             (fun (name,te,r) ->
 354               let augmented_term =
 355                List.fold_right
 356                 (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i))
 357                 itl te
 358               in
 359                let _ = type_of augmented_term in
 360                 (* let's check also the positivity conditions *)
 361                 if not (are_all_occurrences_positive uri indparamsno i 0 len te)
 362                 then
 363                  raise (NotPositiveOccurrences (U.string_of_uri uri))
 364                 else
 365                  match !r with
 366                     Some _ -> raise Impossible
 367                   | None -> r := Some (recursive_args 0 len te)
 368             ) cl ;
 369            (i + 1)
 370         ) itl 1
 371        in
 372         ()
 373    | _ ->
 374      raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
 375
 376 and cooked_type_of_mutual_inductive_defs uri cookingsno i =
 377  let module C = Cic in
 378  let module R = CicReduction in
 379  let module U = UriManager in
 380   let cobj =
 381    match CicCache.is_type_checked uri cookingsno with
 382       CicCache.CheckedObj cobj -> cobj
 383     | CicCache.UncheckedObj uobj ->
 384        cooked_mutual_inductive_defs uri uobj ;
 385        CicCache.set_type_checking_info uri ;
 386        (match CicCache.is_type_checked uri cookingsno with
 387           CicCache.CheckedObj cobj -> cobj
 388         | CicCache.UncheckedObj _ -> raise CicCacheError
 389        )
 390   in
 391    match cobj with
 392       C.InductiveDefinition (dl,_,_) ->
 393        let (_,_,arity,_) = List.nth dl i in
 394         arity
 395     | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
 396
 397 and cooked_type_of_mutual_inductive_constr uri cookingsno i j =
 398  let module C = Cic in
 399  let module R = CicReduction in
 400  let module U = UriManager in
 401   let cobj =
 402    match CicCache.is_type_checked uri cookingsno with
 403       CicCache.CheckedObj cobj -> cobj
 404     | CicCache.UncheckedObj uobj ->
 405        cooked_mutual_inductive_defs uri uobj ;
 406        CicCache.set_type_checking_info uri ;
 407        (match CicCache.is_type_checked uri cookingsno with
 408           CicCache.CheckedObj cobj -> cobj
 409         | CicCache.UncheckedObj _ -> raise CicCacheError
 410        )
 411   in
 412    match cobj with
 413       C.InductiveDefinition (dl,_,_) ->
 414        let (_,_,_,cl) = List.nth dl i in
 415         let (_,ty,_) = List.nth cl (j-1) in
 416          ty
 417     | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
 418
 419 and recursive_args n nn te =
 420  let module C = Cic in
 421   match CicReduction.whd te with
 422      C.Rel _ -> []
 423    | C.Var _
 424    | C.Meta _
 425    | C.Sort _
 426    | C.Implicit
 427    | C.Cast _ (*CSC ??? *) -> raise Impossible (* due to type-checking *)
 428    | C.Prod (_,so,de) ->
 429       (not (does_not_occur n nn so))::(recursive_args (n+1) (nn + 1) de)
 430    | C.Lambda _ -> raise Impossible (* due to type-checking *)
 431    | C.LetIn _ -> raise NotImplemented
 432    | C.Appl _ -> []
 433    | C.Const _
 434    | C.Abst _ -> raise Impossible
 435    | C.MutInd _
 436    | C.MutConstruct _
 437    | C.MutCase _
 438    | C.Fix _
 439    | C.CoFix _ -> raise Impossible (* due to type-checking *)
 440
 441 and get_new_safes p c rl safes n nn x =
 442  let module C = Cic in
 443  let module U = UriManager in
 444  let module R = CicReduction in
 445   match (R.whd c, R.whd p, rl) with
 446      (C.Prod (_,_,ta1), C.Lambda (_,_,ta2), b::tl) ->
 447        (* we are sure that the two sources are convertible because we *)
 448        (* have just checked this. So let's go along ...               *)
 449        let safes' =
 450         List.map (fun x -> x + 1) safes
 451        in
 452         let safes'' =
 453          if b then 1::safes' else safes'
 454         in
 455          get_new_safes ta2 ta1 tl safes'' (n+1) (nn+1) (x+1)
 456    | (C.MutInd _, e, []) -> (e,safes,n,nn,x)
 457    | (C.Appl _, e, []) -> (e,safes,n,nn,x)
 458    | (_,_,_) -> raise Impossible
 459
 460 and eat_prods n te =
 461  let module C = Cic in
 462  let module R = CicReduction in
 463   match (n, R.whd te) with
 464      (0, _) -> te
 465    | (n, C.Prod (_,_,ta)) when n > 0 -> eat_prods (n - 1) ta
 466    | (_, _) -> raise Impossible
 467
 468 and eat_lambdas n te =
 469  let module C = Cic in
 470  let module R = CicReduction in
 471   match (n, R.whd te) with
 472      (0, _) -> (te, 0)
 473    | (n, C.Lambda (_,_,ta)) when n > 0 ->
 474       let (te, k) = eat_lambdas (n - 1) ta in
 475        (te, k + 1)
 476    | (_, _) -> raise Impossible
 477
 478 (*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *)
 479 and check_is_really_smaller_arg n nn kl x safes te =
 480  (*CSC: forse la whd si puo' fare solo quando serve veramente. *)
 481  (*CSC: cfr guarded_by_destructors                             *)
 482  let module C = Cic in
 483  let module U = UriManager in
 484  match CicReduction.whd te with
 485      C.Rel m when List.mem m safes -> true
 486    | C.Rel _ -> false
 487    | C.Var _
 488    | C.Meta _
 489    | C.Sort _
 490    | C.Implicit
 491    | C.Cast _
 492 (*   | C.Cast (te,ty) ->
 493       check_is_really_smaller_arg n nn kl x safes te &&
 494        check_is_really_smaller_arg n nn kl x safes ty*)
 495 (*   | C.Prod (_,so,ta) ->
 496       check_is_really_smaller_arg n nn kl x safes so &&
 497        check_is_really_smaller_arg (n+1) (nn+1) kl (x+1)
 498         (List.map (fun x -> x + 1) safes) ta*)
 499    | C.Prod _ -> raise Impossible
 500    | C.Lambda (_,so,ta) ->
 501       check_is_really_smaller_arg n nn kl x safes so &&
 502        check_is_really_smaller_arg (n+1) (nn+1) kl (x+1)
 503         (List.map (fun x -> x + 1) safes) ta
 504    | C.LetIn (_,so,ta) ->
 505       check_is_really_smaller_arg n nn kl x safes so &&
 506        check_is_really_smaller_arg (n+1) (nn+1) kl (x+1)
 507         (List.map (fun x -> x + 1) safes) ta
 508    | C.Appl (he::_) ->
 509       (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
 510       (*CSC: solo perche' non abbiamo trovato controesempi            *)
 511       check_is_really_smaller_arg n nn kl x safes he
 512    | C.Appl [] -> raise Impossible
 513    | C.Const _
 514    | C.Abst _
 515    | C.MutInd _ -> raise Impossible
 516    | C.MutConstruct _ -> false
 517    | C.MutCase (uri,_,i,outtype,term,pl) ->
 518       (match term with
 519           C.Rel m when List.mem m safes || m = x ->
 520            let (isinductive,paramsno,cl) =
 521             match CicCache.get_obj uri with
 522                C.InductiveDefinition (tl,_,paramsno) ->
 523                 let (_,isinductive,_,cl) = List.nth tl i in
 524                  let cl' =
 525                   List.map (fun (id,ty,r) -> (id, eat_prods paramsno ty, r)) cl
 526                  in
 527                   (isinductive,paramsno,cl')
 528              | _ ->
 529                raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
 530            in
 531             if not isinductive then
 532               List.fold_right
 533                (fun p i -> i && check_is_really_smaller_arg n nn kl x safes p)
 534                pl true
 535             else
 536               List.fold_right
 537                (fun (p,(_,c,rl)) i ->
 538                  let rl' =
 539                   match !rl with
 540                      Some rl' ->
 541                       let (_,rl'') = split rl' paramsno in
 542                        rl''
 543                    | None -> raise Impossible
 544                  in
 545                   let (e,safes',n',nn',x') =
 546                    get_new_safes p c rl' safes n nn x
 547                   in
 548                    i &&
 549                    check_is_really_smaller_arg n' nn' kl x' safes' e
 550                ) (List.combine pl cl) true
 551         | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
 552            let (isinductive,paramsno,cl) =
 553             match CicCache.get_obj uri with
 554                C.InductiveDefinition (tl,_,paramsno) ->
 555                 let (_,isinductive,_,cl) = List.nth tl i in
 556                  let cl' =
 557                   List.map (fun (id,ty,r) -> (id, eat_prods paramsno ty, r)) cl
 558                  in
 559                   (isinductive,paramsno,cl')
 560              | _ ->
 561                raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
 562            in
 563             if not isinductive then
 564               List.fold_right
 565                (fun p i -> i && check_is_really_smaller_arg n nn kl x safes p)
 566                pl true
 567             else
 568               (*CSC: supponiamo come prima che nessun controllo sia necessario*)
 569               (*CSC: sugli argomenti di una applicazione                      *)
 570               List.fold_right
 571                (fun (p,(_,c,rl)) i ->
 572                  let rl' =
 573                   match !rl with
 574                      Some rl' ->
 575                       let (_,rl'') = split rl' paramsno in
 576                        rl''
 577                    | None -> raise Impossible
 578                  in
 579                   let (e, safes',n',nn',x') =
 580                    get_new_safes p c rl' safes n nn x
 581                   in
 582                    i &&
 583                    check_is_really_smaller_arg n' nn' kl x' safes' e
 584                ) (List.combine pl cl) true
 585         | _ ->
 586           List.fold_right
 587            (fun p i -> i && check_is_really_smaller_arg n nn kl x safes p)
 588            pl true
 589       )
 590    | C.Fix (_, fl) ->
 591       let len = List.length fl in
 592        let n_plus_len = n + len
 593        and nn_plus_len = nn + len
 594        and x_plus_len = x + len
 595        and safes' = List.map (fun x -> x + len) safes in
 596         List.fold_right
 597          (fun (_,_,ty,bo) i ->
 598            i &&
 599             check_is_really_smaller_arg n_plus_len nn_plus_len kl x_plus_len
 600              safes' bo
 601          ) fl true
 602    | C.CoFix (_, fl) ->
 603       let len = List.length fl in
 604        let n_plus_len = n + len
 605        and nn_plus_len = nn + len
 606        and x_plus_len = x + len
 607        and safes' = List.map (fun x -> x + len) safes in
 608         List.fold_right
 609          (fun (_,ty,bo) i ->
 610            i &&
 611             check_is_really_smaller_arg n_plus_len nn_plus_len kl x_plus_len
 612              safes' bo
 613          ) fl true
 614
 615 and guarded_by_destructors n nn kl x safes =
 616  let module C = Cic in
 617  let module U = UriManager in
 618   function
 619      C.Rel m when m > n && m <= nn -> false
 620    | C.Rel _
 621    | C.Var _
 622    | C.Meta _
 623    | C.Sort _
 624    | C.Implicit -> true
 625    | C.Cast (te,ty) ->
 626       guarded_by_destructors n nn kl x safes te &&
 627        guarded_by_destructors n nn kl x safes ty
 628    | C.Prod (_,so,ta) ->
 629       guarded_by_destructors n nn kl x safes so &&
 630        guarded_by_destructors (n+1) (nn+1) kl (x+1)
 631         (List.map (fun x -> x + 1) safes) ta
 632    | C.Lambda (_,so,ta) ->
 633       guarded_by_destructors n nn kl x safes so &&
 634        guarded_by_destructors (n+1) (nn+1) kl (x+1)
 635         (List.map (fun x -> x + 1) safes) ta
 636    | C.LetIn (_,so,ta) ->
 637       guarded_by_destructors n nn kl x safes so &&
 638        guarded_by_destructors (n+1) (nn+1) kl (x+1)
 639         (List.map (fun x -> x + 1) safes) ta
 640    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
 641       let k = List.nth kl (m - n - 1) in
 642        if not (List.length tl > k) then false
 643        else
 644         List.fold_right
 645          (fun param i ->
 646            i && guarded_by_destructors n nn kl x safes param
 647          ) tl true &&
 648          check_is_really_smaller_arg n nn kl x safes (List.nth tl k)
 649    | C.Appl tl ->
 650       List.fold_right (fun t i -> i && guarded_by_destructors n nn kl x safes t)
 651        tl true
 652    | C.Const _
 653    | C.Abst _
 654    | C.MutInd _
 655    | C.MutConstruct _ -> true
 656    | C.MutCase (uri,_,i,outtype,term,pl) ->
 657       (match term with
 658           C.Rel m when List.mem m safes || m = x ->
 659            let (isinductive,paramsno,cl) =
 660             match CicCache.get_obj uri with
 661                C.InductiveDefinition (tl,_,paramsno) ->
 662                 let (_,isinductive,_,cl) = List.nth tl i in
 663                  let cl' =
 664                   List.map (fun (id,ty,r) -> (id, eat_prods paramsno ty, r)) cl
 665                  in
 666                   (isinductive,paramsno,cl')
 667              | _ ->
 668                raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
 669            in
 670             if not isinductive then
 671              guarded_by_destructors n nn kl x safes outtype &&
 672               guarded_by_destructors n nn kl x safes term &&
 673               (*CSC: manca ??? il controllo sul tipo di term? *)
 674               List.fold_right
 675                (fun p i -> i && guarded_by_destructors n nn kl x safes p)
 676                pl true
 677             else
 678              guarded_by_destructors n nn kl x safes outtype &&
 679               (*CSC: manca ??? il controllo sul tipo di term? *)
 680               List.fold_right
 681                (fun (p,(_,c,rl)) i ->
 682                  let rl' =
 683                   match !rl with
 684                      Some rl' ->
 685                       let (_,rl'') = split rl' paramsno in
 686                        rl''
 687                    | None -> raise Impossible
 688                  in
 689                   let (e,safes',n',nn',x') =
 690                    get_new_safes p c rl' safes n nn x
 691                   in
 692                    i &&
 693                    guarded_by_destructors n' nn' kl x' safes' e
 694                ) (List.combine pl cl) true
 695         | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
 696            let (isinductive,paramsno,cl) =
 697             match CicCache.get_obj uri with
 698                C.InductiveDefinition (tl,_,paramsno) ->
 699                 let (_,isinductive,_,cl) = List.nth tl i in
 700                  let cl' =
 701                   List.map (fun (id,ty,r) -> (id, eat_prods paramsno ty, r)) cl
 702                  in
 703                   (isinductive,paramsno,cl')
 704              | _ ->
 705                raise (WrongUriToMutualInductiveDefinitions(U.string_of_uri uri))
 706            in
 707             if not isinductive then
 708              guarded_by_destructors n nn kl x safes outtype &&
 709               guarded_by_destructors n nn kl x safes term &&
 710               (*CSC: manca ??? il controllo sul tipo di term? *)
 711               List.fold_right
 712                (fun p i -> i && guarded_by_destructors n nn kl x safes p)
 713                pl true
 714             else
 715              guarded_by_destructors n nn kl x safes outtype &&
 716               (*CSC: manca ??? il controllo sul tipo di term? *)
 717               List.fold_right
 718                (fun t i -> i && guarded_by_destructors n nn kl x safes t)
 719                tl true &&
 720               List.fold_right
 721                (fun (p,(_,c,rl)) i ->
 722                  let rl' =
 723                   match !rl with
 724                      Some rl' ->
 725                       let (_,rl'') = split rl' paramsno in
 726                        rl''
 727                    | None -> raise Impossible
 728                  in
 729                   let (e, safes',n',nn',x') =
 730                    get_new_safes p c rl' safes n nn x
 731                   in
 732                    i &&
 733                    guarded_by_destructors n' nn' kl x' safes' e
 734                ) (List.combine pl cl) true
 735         | _ ->
 736           guarded_by_destructors n nn kl x safes outtype &&
 737            guarded_by_destructors n nn kl x safes term &&
 738            (*CSC: manca ??? il controllo sul tipo di term? *)
 739            List.fold_right
 740             (fun p i -> i && guarded_by_destructors n nn kl x safes p)
 741             pl true
 742       )
 743    | C.Fix (_, fl) ->
 744       let len = List.length fl in
 745        let n_plus_len = n + len
 746        and nn_plus_len = nn + len
 747        and x_plus_len = x + len
 748        and safes' = List.map (fun x -> x + len) safes in
 749         List.fold_right
 750          (fun (_,_,ty,bo) i ->
 751            i && guarded_by_destructors n_plus_len nn_plus_len kl x_plus_len
 752             safes' ty &&
 753             guarded_by_destructors n_plus_len nn_plus_len kl x_plus_len
 754              safes' bo
 755          ) fl true
 756    | C.CoFix (_, fl) ->
 757       let len = List.length fl in
 758        let n_plus_len = n + len
 759        and nn_plus_len = nn + len
 760        and x_plus_len = x + len
 761        and safes' = List.map (fun x -> x + len) safes in
 762         List.fold_right
 763          (fun (_,ty,bo) i ->
 764            i && guarded_by_destructors n_plus_len nn_plus_len kl x_plus_len
 765             safes' ty &&
 766             guarded_by_destructors n_plus_len nn_plus_len kl x_plus_len safes'
 767              bo
 768          ) fl true
 769
 770 (*CSC h = 0 significa non ancora protetto *)
 771 and guarded_by_constructors n nn h =
 772  let module C = Cic in
 773   function
 774      C.Rel m when m > n && m <= nn -> h = 1
 775    | C.Rel _
 776    | C.Var _
 777    | C.Meta _
 778    | C.Sort _
 779    | C.Implicit -> true (*CSC: ma alcuni sono impossibili!!!! vedi Prod *)
 780    | C.Cast (te,ty) ->
 781       guarded_by_constructors n nn h te &&
 782        guarded_by_constructors n nn h ty
 783    | C.Prod (_,so,de) ->
 784       raise Impossible (* the term has just been type-checked *)
 785    | C.Lambda (_,so,de) ->
 786       does_not_occur n nn so &&
 787        guarded_by_constructors (n + 1) (nn + 1) h de
 788    | C.LetIn (_,so,de) ->
 789       does_not_occur n nn so &&
 790        guarded_by_constructors (n + 1) (nn + 1) h de
 791    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
 792       h = 1 &&
 793        List.fold_right (fun x i -> i && does_not_occur n nn x) tl true
 794    | C.Appl ((C.MutConstruct (uri,cookingsno,i,j))::tl) ->
 795       let (is_coinductive, rl) =
 796        match CicCache.get_cooked_obj uri cookingsno with
 797           C.InductiveDefinition (itl,_,_) ->
 798            let (_,is_inductive,_,cl) = List.nth itl i in
 799             let (_,cons,rrec_args) = List.nth cl (j - 1) in
 800              (match !rrec_args with
 801                  None -> raise Impossible
 802                | Some rec_args -> (not is_inductive, rec_args)
 803              )
 804         | _ ->
 805          raise (WrongUriToMutualInductiveDefinitions
 806           (UriManager.string_of_uri uri))
 807       in
 808        is_coinductive &&
 809        List.fold_right
 810         (fun (x,r) i ->
 811           i &&
 812            if r then
 813             guarded_by_constructors n nn 1 x
 814            else
 815             does_not_occur n nn x
 816         ) (List.combine tl rl) true
 817    | C.Appl l ->
 818       List.fold_right (fun x i -> i && does_not_occur n nn x) l true
 819    | C.Const _
 820    | C.Abst _
 821    | C.MutInd _
 822    | C.MutConstruct _ -> true (*CSC: ma alcuni sono impossibili!!!! vedi Prod *)
 823    | C.MutCase (_,_,_,out,te,pl) ->
 824       let rec returns_a_coinductive =
 825        function
 826           (*CSC: per le regole di tipaggio, la chiamata ricorsiva verra' *)
 827           (*CSC: effettata solo una volta, per mangiarsi l'astrazione    *)
 828           (*CSC: non dummy                                               *)
 829           C.Lambda (_,_,de) -> returns_a_coinductive de
 830         | C.MutInd (uri,_,i) ->
 831            (*CSC: definire una funzioncina per questo codice sempre replicato *)
 832            (match CicCache.get_obj uri with
 833                C.InductiveDefinition (itl,_,_) ->
 834                 let (_,is_inductive,_,_) = List.nth itl i in
 835                  not is_inductive
 836              | _ ->
 837                raise (WrongUriToMutualInductiveDefinitions
 838                 (UriManager.string_of_uri uri))
 839             )
 840         (*CSC: bug nella prossima riga (manca la whd) *)
 841         | C.Appl ((C.MutInd (uri,_,i))::_) ->
 842            (match CicCache.get_obj uri with
 843                C.InductiveDefinition (itl,_,_) ->
 844                 let (_,is_inductive,_,_) = List.nth itl i in
 845                  not is_inductive
 846              | _ ->
 847                raise (WrongUriToMutualInductiveDefinitions
 848                 (UriManager.string_of_uri uri))
 849             )
 850         | _ -> false
 851       in
 852        does_not_occur n nn out &&
 853         does_not_occur n nn te &&
 854         if returns_a_coinductive out then
 855          List.fold_right
 856           (fun x i -> i && guarded_by_constructors n nn h x) pl true
 857         else
 858          List.fold_right (fun x i -> i && does_not_occur n nn x) pl true
 859    | C.Fix (_,fl) ->
 860       let len = List.length fl in
 861        let n_plus_len = n + len
 862        and nn_plus_len = nn + len in
 863         List.fold_right
 864          (fun (_,_,ty,bo) i ->
 865            i && does_not_occur n_plus_len nn_plus_len ty &&
 866             does_not_occur n_plus_len nn_plus_len bo
 867          ) fl true
 868    | C.CoFix (_,fl) ->
 869       let len = List.length fl in
 870        let n_plus_len = n + len
 871        and nn_plus_len = nn + len in
 872         List.fold_right
 873          (fun (_,ty,bo) i ->
 874            i && does_not_occur n_plus_len nn_plus_len ty &&
 875             does_not_occur n_plus_len nn_plus_len bo
 876          ) fl true
 877
 878 and check_allowed_sort_elimination uri i need_dummy ind arity1 arity2 =
 879  let module C = Cic in
 880  let module U = UriManager in
 881   match (CicReduction.whd arity1, CicReduction.whd arity2) with
 882      (C.Prod (_,so1,de1), C.Prod (_,so2,de2))
 883       when CicReduction.are_convertible so1 so2 ->
 884        check_allowed_sort_elimination uri i need_dummy
 885         (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2
 886    | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true
 887    | (C.Sort C.Prop, C.Sort C.Set) when need_dummy ->
 888        (match CicCache.get_obj uri with
 889            C.InductiveDefinition (itl,_,_) ->
 890             let (_,_,_,cl) = List.nth itl i in
 891              (* is a singleton definition? *)
 892              List.length cl = 1
 893          | _ ->
 894            raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
 895        )
 896    | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true
 897    | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true
 898    | (C.Sort C.Set, C.Sort C.Type) when need_dummy ->
 899        (match CicCache.get_obj uri with
 900            C.InductiveDefinition (itl,_,_) ->
 901             let (_,_,_,cl) = List.nth itl i in
 902              (* is a small inductive type? *)
 903              (*CSC: ottimizzare calcolando staticamente *)
 904              let rec is_small =
 905               function
 906                  C.Prod (_,so,de) ->
 907                   let s = type_of so in
 908                    (s = C.Sort C.Prop || s = C.Sort C.Set) &&
 909                    is_small de
 910                | _ -> true (*CSC: we trust the type-checker *)
 911              in
 912               List.fold_right (fun (_,x,_) i -> i && is_small x) cl true
 913          | _ ->
 914            raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
 915        )
 916    | (C.Sort C.Type, C.Sort _) when need_dummy -> true
 917    | (C.Sort C.Prop, C.Prod (_,so,ta)) when not need_dummy ->
 918        let res = CicReduction.are_convertible so ind
 919        in
 920         res &&
 921         (match CicReduction.whd ta with
 922             C.Sort C.Prop -> true
 923           | C.Sort C.Set ->
 924              (match CicCache.get_obj uri with
 925                  C.InductiveDefinition (itl,_,_) ->
 926                   let (_,_,_,cl) = List.nth itl i in
 927                    (* is a singleton definition? *)
 928                    List.length cl = 1
 929                | _ ->
 930                  raise (WrongUriToMutualInductiveDefinitions
 931                   (U.string_of_uri uri))
 932              )
 933           | _ -> false
 934         )
 935    | (C.Sort C.Set, C.Prod (_,so,ta)) when not need_dummy ->
 936        let res = CicReduction.are_convertible so ind
 937        in
 938         res &&
 939         (match CicReduction.whd ta with
 940             C.Sort C.Prop
 941           | C.Sort C.Set  -> true
 942           | C.Sort C.Type ->
 943              (match CicCache.get_obj uri with
 944                  C.InductiveDefinition (itl,_,_) ->
 945                   let (_,_,_,cl) = List.nth itl i in
 946                    (* is a small inductive type? *)
 947                    let rec is_small =
 948                     function
 949                        C.Prod (_,so,de) ->
 950                         let s = type_of so in
 951                          (s = C.Sort C.Prop || s = C.Sort C.Set) &&
 952                          is_small de
 953                      | _ -> true (*CSC: we trust the type-checker *)
 954                    in
 955                     List.fold_right (fun (_,x,_) i -> i && is_small x) cl true
 956                | _ ->
 957                  raise (WrongUriToMutualInductiveDefinitions
 958                   (U.string_of_uri uri))
 959              )
 960           | _ -> raise Impossible
 961         )
 962    | (C.Sort C.Type, C.Prod (_,so,_)) when not need_dummy ->
 963        CicReduction.are_convertible so ind
 964    | (_,_) -> false
 965
 966 and type_of_branch argsno need_dummy outtype term constype =
 967  let module C = Cic in
 968  let module R = CicReduction in
 969   match R.whd constype with
 970      C.MutInd (_,_,_) ->
 971       if need_dummy then
 972        outtype
 973       else
 974        C.Appl [outtype ; term]
 975    | C.Appl (C.MutInd (_,_,_)::tl) ->
 976       let (_,arguments) = split tl argsno
 977       in
 978        if need_dummy && arguments = [] then
 979         outtype
 980        else
 981         C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
 982    | C.Prod (name,so,de) ->
 983       C.Prod (C.Name "pippo",so,type_of_branch argsno need_dummy
 984        (CicSubstitution.lift 1 outtype)
 985        (C.Appl [CicSubstitution.lift 1 term ; C.Rel 1]) de)
 986   | _ -> raise Impossible
 987
 988
 989 and type_of t =
 990  let rec type_of_aux env =
 991   let module C = Cic in
 992   let module R = CicReduction in
 993   let module S = CicSubstitution in
 994   let module U = UriManager in
 995    function
 996       C.Rel n -> S.lift n (List.nth env (n - 1))
 997     | C.Var uri ->
 998       incr fdebug ;
 999       let ty = type_of_variable uri in
1000        decr fdebug ;
1001        ty
1002     | C.Meta n -> raise NotImplemented
1003     | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
1004     | C.Implicit -> raise Impossible
1005     | C.Cast (te,ty) ->
1006        let _ = type_of ty in
1007         if R.are_convertible (type_of_aux env te) ty then ty
1008         else raise (NotWellTyped "Cast")
1009     | C.Prod (_,s,t) ->
1010        let sort1 = type_of_aux env s
1011        and sort2 = type_of_aux (s::env) t in
1012         sort_of_prod (sort1,sort2)
1013    | C.Lambda (n,s,t) ->
1014        let sort1 = type_of_aux env s
1015        and type2 = type_of_aux (s::env) t in
1016         let sort2 = type_of_aux (s::env) type2 in
1017          (* only to check if the product is well-typed *)
1018          let _ = sort_of_prod (sort1,sort2) in
1019           C.Prod (n,s,type2)
1020    | C.LetIn (n,s,t) ->
1021        let type1 = type_of_aux env s in
1022        let type2 = type_of_aux (type1::env) t in
1023         type2
1024    | C.Appl (he::tl) when List.length tl > 0 ->
1025       let hetype = type_of_aux env he
1026       and tlbody_and_type = List.map (fun x -> (x, type_of_aux env x)) tl in
1027        (try
1028         eat_prods hetype tlbody_and_type
1029        with _ -> debug (C.Appl (he::tl)) env ; C.Implicit)
1030    | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
1031    | C.Const (uri,cookingsno) ->
1032       incr fdebug ;
1033       let cty = cooked_type_of_constant uri cookingsno in
1034        decr fdebug ;
1035        cty
1036    | C.Abst _ -> raise Impossible
1037    | C.MutInd (uri,cookingsno,i) ->
1038       incr fdebug ;
1039       let cty = cooked_type_of_mutual_inductive_defs uri cookingsno i in
1040        decr fdebug ;
1041        cty
1042    | C.MutConstruct (uri,cookingsno,i,j) ->
1043       let cty = cooked_type_of_mutual_inductive_constr uri cookingsno i j
1044       in
1045        cty
1046    | C.MutCase (uri,cookingsno,i,outtype,term,pl) ->
1047       let outsort = type_of_aux env outtype in
1048       let (need_dummy, k) =
1049        let rec guess_args t =
1050         match decast t with
1051            C.Sort _ -> (true, 0)
1052          | C.Prod (_, s, t) ->
1053             let (b, n) = guess_args t in
1054              if n = 0 then
1055               (* last prod before sort *)
1056               match CicReduction.whd s with
1057                  (*CSC vedi nota delirante su cookingsno in cicReduction.ml *)
1058                  C.MutInd (uri',_,i') when U.eq uri' uri && i' = i -> (false, 1)
1059                | C.Appl ((C.MutInd (uri',_,i')) :: _)
1060                   when U.eq uri' uri && i' = i -> (false, 1)
1061                | _ -> (true, 1)
1062              else
1063               (b, n + 1)
1064          | _ -> raise (NotWellTyped "MutCase: outtype ill-formed")
1065        in
1066         (*CSC whd non serve dopo type_of_aux ? *)
1067         let (b, k) = guess_args outsort in
1068          if not b then (b, k - 1) else (b, k)
1069       in
1070       let (parameters, arguments) =
1071         match R.whd (type_of_aux env term) with
1072            (*CSC manca il caso dei CAST *)
1073            C.MutInd (uri',_,i') ->
1074             (*CSC vedi nota delirante sui cookingsno in cicReduction.ml*)
1075             if U.eq uri uri' && i = i' then ([],[])
1076             else raise (NotWellTyped ("MutCase: the term is of type " ^
1077              (U.string_of_uri uri') ^ "," ^ string_of_int i' ^
1078              " instead of type " ^ (U.string_of_uri uri') ^ "," ^
1079              string_of_int i))
1080          | C.Appl (C.MutInd (uri',_,i') :: tl) ->
1081             if U.eq uri uri' && i = i' then split tl (List.length tl - k)
1082             else raise (NotWellTyped ("MutCase: the term is of type " ^
1083              (U.string_of_uri uri') ^ "," ^ string_of_int i' ^
1084              " instead of type " ^ (U.string_of_uri uri) ^ "," ^
1085              string_of_int i))
1086          | _ -> raise (NotWellTyped "MutCase: the term is not an inductive one")
1087       in
1088        (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
1089        let sort_of_ind_type =
1090         if parameters = [] then
1091          C.MutInd (uri,cookingsno,i)
1092         else
1093          C.Appl ((C.MutInd (uri,cookingsno,i))::parameters)
1094        in
1095         if not (check_allowed_sort_elimination uri i need_dummy
1096          sort_of_ind_type (type_of_aux env sort_of_ind_type) outsort)
1097         then
1098          raise (NotWellTyped "MutCase: not allowed sort elimination") ;
1099
1100         (* let's check if the type of branches are right *)
1101         let (cl,parsno) =
1102          match CicCache.get_cooked_obj uri cookingsno with
1103             C.InductiveDefinition (tl,_,parsno) ->
1104              let (_,_,_,cl) = List.nth tl i in (cl,parsno)
1105           | _ ->
1106             raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
1107         in
1108          let (_,branches_ok) =
1109           List.fold_left
1110            (fun (j,b) (p,(_,c,_)) ->
1111              let cons =
1112               if parameters = [] then
1113                (C.MutConstruct (uri,cookingsno,i,j))
1114               else
1115                (C.Appl (C.MutConstruct (uri,cookingsno,i,j)::parameters))
1116              in
1117               (j + 1, b &&
1118                R.are_convertible (type_of_aux env p)
1119                 (type_of_branch parsno need_dummy outtype cons
1120                   (type_of_aux env cons))
1121               )
1122            ) (1,true) (List.combine pl cl)
1123          in
1124           if not branches_ok then
1125            raise (NotWellTyped "MutCase: wrong type of a branch") ;
1126
1127           if not need_dummy then
1128            C.Appl ((outtype::arguments)@[term])
1129           else if arguments = [] then
1130            outtype
1131           else
1132            C.Appl (outtype::arguments)
1133    | C.Fix (i,fl) ->
1134       let types_times_kl =
1135        List.rev
1136         (List.map (fun (_,k,ty,_) -> let _ = type_of_aux env ty in (ty,k)) fl)
1137       in
1138       let (types,kl) = List.split types_times_kl in
1139        let len = List.length types in
1140         List.iter
1141          (fun (name,x,ty,bo) ->
1142            if (R.are_convertible (type_of_aux (types @ env) bo)
1143             (CicSubstitution.lift len ty))
1144            then
1145             begin
1146              let (m, eaten) = eat_lambdas (x + 1) bo in
1147               (*let's control the guarded by destructors conditions D{f,k,x,M}*)
1148               if not (guarded_by_destructors eaten (len + eaten) kl 1 [] m) then
1149                raise (NotWellTyped "Fix: not guarded by destructors")
1150             end
1151            else
1152             raise (NotWellTyped "Fix: ill-typed bodies")
1153          ) fl ;
1154
1155         (*CSC: controlli mancanti solo su D{f,k,x,M} *)
1156         let (_,_,ty,_) = List.nth fl i in
1157         ty
1158    | C.CoFix (i,fl) ->
1159       let types =
1160        List.rev (List.map (fun (_,ty,_) -> let _ = type_of_aux env ty in ty) fl)
1161       in
1162        let len = List.length types in
1163         List.iter
1164          (fun (_,ty,bo) ->
1165            if (R.are_convertible (type_of_aux (types @ env) bo)
1166             (CicSubstitution.lift len ty))
1167            then
1168             begin
1169              (* let's control the guarded by constructors conditions C{f,M} *)
1170              if not (guarded_by_constructors 0 len 0 bo) then
1171               raise (NotWellTyped "CoFix: not guarded by constructors")
1172             end
1173            else
1174             raise (NotWellTyped "CoFix: ill-typed bodies")
1175          ) fl ;
1176
1177         let (_,ty,_) = List.nth fl i in
1178          ty
1179
1180  and decast =
1181   let module C = Cic in
1182    function
1183       C.Cast (t,_) -> t
1184     | t -> t
1185
1186  and sort_of_prod (t1, t2) =
1187   let module C = Cic in
1188    match (decast t1, decast t2) with
1189       (C.Sort s1, C.Sort s2)
1190         when (s2 = C.Prop or s2 = C.Set) -> (* different from Coq manual!!! *)
1191          C.Sort s2
1192     | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
1193     | (_,_) -> raise (NotWellTyped "Prod")
1194
1195  and eat_prods hetype =
1196   (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
1197   (*CSC: cucinati                                                         *)
1198   function
1199      [] -> hetype
1200    | (hete, hety)::tl ->
1201     (match (CicReduction.whd hetype) with
1202         Cic.Prod (n,s,t) ->
1203          if CicReduction.are_convertible s hety then
1204           (CicReduction.fdebug := -1 ;
1205           eat_prods (CicSubstitution.subst hete t) tl
1206           )
1207          else
1208           (
1209           CicReduction.fdebug := 0 ;
1210           let _ = CicReduction.are_convertible s hety in
1211           debug hete [hety ; s] ;
1212           raise (NotWellTyped "Appl: wrong parameter-type")
1213 )
1214       | _ -> raise (NotWellTyped "Appl: wrong Prod-type")
1215     )
1216  in
1217   type_of_aux [] t
1218 ;;
1219
1220 let typecheck uri =
1221  let module C = Cic in
1222  let module R = CicReduction in
1223  let module U = UriManager in
1224   match CicCache.is_type_checked uri 0 with
1225      CicCache.CheckedObj _ -> ()
1226    | CicCache.UncheckedObj uobj ->
1227       (* let's typecheck the uncooked object *)
1228       (match uobj with
1229           C.Definition (_,te,ty,_) ->
1230            let _ = type_of ty in
1231             if not (R.are_convertible (type_of te ) ty) then
1232              raise (NotWellTyped ("Constant " ^ (U.string_of_uri uri)))
1233         | C.Axiom (_,ty,_) ->
1234           (* only to check that ty is well-typed *)
1235           let _ = type_of ty in ()
1236         | C.CurrentProof (_,_,te,ty) ->
1237            (*CSC [] wrong *)
1238            let _ = type_of ty in
1239             debug (type_of te) [] ;
1240             if not (R.are_convertible (type_of te) ty) then
1241              raise (NotWellTyped ("CurrentProof" ^ (U.string_of_uri uri)))
1242         | C.Variable (_,bo,ty) ->
1243            (* only to check that ty is well-typed *)
1244            let _ = type_of ty in
1245             (match bo with
1246                 None -> ()
1247               | Some bo ->
1248                  if not (R.are_convertible (type_of bo) ty) then
1249                   raise (NotWellTyped ("Variable" ^ (U.string_of_uri uri)))
1250             )
1251         | C.InductiveDefinition _ ->
1252            cooked_mutual_inductive_defs uri uobj
1253       ) ;
1254       CicCache.set_type_checking_info uri
1255 ;;