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