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