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