helm/interface/cicTypeChecker.ml

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