helm/ocaml/cic_proof_checking/cicTypeChecker.ml

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