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 _  (* CSC: Are we sure? No recursion?*)
 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 (t,Some ty)))::tl ->
1298          (Some (n,C.Def ((S.lift_meta l (S.lift i t)),Some (S.lift_meta l (S.lift i ty)))))::(aux (i+1) tl)
1299     in
1300      aux 1 canonical_context
1301    in
1302     List.iter2
1303      (fun t ct ->
1304         match (t,ct) with
1305          | _,None -> ()
1306          | Some t,Some (_,C.Def (ct,_)) ->
1307             if not (R.are_convertible context t ct) then
1308               raise (TypeCheckerFailure (sprintf
1309                 "Not well typed metavariable local context: expected a term convertible with %s, found %s"
1310                 (CicPp.ppterm ct) (CicPp.ppterm t)))
1311          | Some t,Some (_,C.Decl ct) ->
1312              let type_t = type_of_aux' metasenv context t in
1313              if not (R.are_convertible context type_t ct) then
1314               raise (TypeCheckerFailure (sprintf
1315                 "Not well typed metavariable local context: expected a term of type %s, found %s of type %s"
1316                 (CicPp.ppterm ct) (CicPp.ppterm t) (CicPp.ppterm type_t)))
1317          | None, _  ->
1318              raise (TypeCheckerFailure
1319               "Not well typed metavariable local context: an hypothesis, that is not hidden, is not instantiated")
1320      ) l lifted_canonical_context
1321
1322 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
1323 and type_of_aux' metasenv context t =
1324  let rec type_of_aux context =
1325   let module C = Cic in
1326   let module R = CicReduction in
1327   let module S = CicSubstitution in
1328   let module U = UriManager in
1329    function
1330       C.Rel n ->
1331        (try
1332          match List.nth context (n - 1) with
1333             Some (_,C.Decl t) -> S.lift n t
1334           | Some (_,C.Def (_,Some ty)) -> S.lift n ty
1335           | Some (_,C.Def (bo,None)) ->
1336              debug_print "##### CASO DA INVESTIGARE E CAPIRE" ;
1337              type_of_aux context (S.lift n bo)
1338           | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
1339         with
1340         _ ->
1341           raise (TypeCheckerFailure
1342             "unbound variable found in constructor type")
1343        )
1344     | C.Var (uri,exp_named_subst) ->
1345       incr fdebug ;
1346       check_exp_named_subst context exp_named_subst ;
1347       let ty =
1348        CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
1349       in
1350        decr fdebug ;
1351        ty
1352     | C.Meta (n,l) ->
1353        let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
1354         check_metasenv_consistency metasenv context canonical_context l;
1355         CicSubstitution.lift_meta l ty
1356     | C.Sort s -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
1357     | C.Implicit _ -> raise (AssertFailure "21")
1358     | C.Cast (te,ty) as t ->
1359        let _ = type_of_aux context ty in
1360         if R.are_convertible context (type_of_aux context te) ty then
1361           ty
1362         else
1363           raise (TypeCheckerFailure
1364             (sprintf "Invalid cast %s" (CicPp.ppterm t)))
1365     | C.Prod (name,s,t) ->
1366        let sort1 = type_of_aux context s
1367        and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in
1368         sort_of_prod context (name,s) (sort1,sort2)
1369    | C.Lambda (n,s,t) ->
1370        let sort1 = type_of_aux context s
1371        and type2 = type_of_aux ((Some (n,(C.Decl s)))::context) t in
1372         let sort2 = type_of_aux ((Some (n,(C.Decl s)))::context) type2 in
1373          (* only to check if the product is well-typed *)
1374          let _ = sort_of_prod context (n,s) (sort1,sort2) in
1375           C.Prod (n,s,type2)
1376    | C.LetIn (n,s,t) ->
1377       (* only to check if s is well-typed *)
1378       let ty = type_of_aux context s in
1379        (* The type of a LetIn is a LetIn. Extremely slow since the computed
1380           LetIn is later reduced and maybe also re-checked.
1381        (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t))
1382        *)
1383        (* The type of the LetIn is reduced. Much faster than the previous
1384           solution. Moreover the inferred type is probably very different
1385           from the expected one.
1386        (CicReduction.whd context
1387         (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)))
1388        *)
1389        (* One-step LetIn reduction. Even faster than the previous solution.
1390           Moreover the inferred type is closer to the expected one. *)
1391        (CicSubstitution.subst s
1392         (type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t))
1393    | C.Appl (he::tl) when List.length tl > 0 ->
1394       let hetype = type_of_aux context he
1395       and tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in
1396        eat_prods context hetype tlbody_and_type
1397    | C.Appl _ -> raise (AssertFailure "Appl: no arguments")
1398    | C.Const (uri,exp_named_subst) ->
1399       incr fdebug ;
1400       check_exp_named_subst context exp_named_subst ;
1401       let cty =
1402        CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
1403       in
1404        decr fdebug ;
1405        cty
1406    | C.MutInd (uri,i,exp_named_subst) ->
1407       incr fdebug ;
1408       check_exp_named_subst context exp_named_subst ;
1409       let cty =
1410        CicSubstitution.subst_vars exp_named_subst
1411         (type_of_mutual_inductive_defs uri i)
1412       in
1413        decr fdebug ;
1414        cty
1415    | C.MutConstruct (uri,i,j,exp_named_subst) ->
1416       check_exp_named_subst context exp_named_subst ;
1417       let cty =
1418        CicSubstitution.subst_vars exp_named_subst
1419         (type_of_mutual_inductive_constr uri i j)
1420       in
1421        cty
1422    | C.MutCase (uri,i,outtype,term,pl) ->
1423       let outsort = type_of_aux context outtype in
1424       let (need_dummy, k) =
1425        let rec guess_args context t =
1426          let outtype = CicReduction.whd context t in
1427          match outtype with
1428            C.Sort _ -> (true, 0)
1429          | C.Prod (name, s, t) ->
1430             let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
1431              if n = 0 then
1432               (* last prod before sort *)
1433               match CicReduction.whd context s with
1434 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1435                  C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
1436                   (false, 1)
1437 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1438                | C.Appl ((C.MutInd (uri',i',_)) :: _)
1439                   when U.eq uri' uri && i' = i -> (false, 1)
1440                | _ -> (true, 1)
1441              else
1442               (b, n + 1)
1443          | _ ->
1444              raise (TypeCheckerFailure (sprintf
1445               "Malformed case analasys' output type %s" (CicPp.ppterm outtype)))
1446        in
1447         (*CSC whd non serve dopo type_of_aux ? *)
1448         let (b, k) = guess_args context outsort in
1449          if not b then (b, k - 1) else (b, k)
1450       in
1451       let (parameters, arguments, exp_named_subst) =
1452         match R.whd context (type_of_aux context term) with
1453            (*CSC manca il caso dei CAST *)
1454 (*CSC: ma servono i parametri (uri,i)? Se si', perche' non serve anche il *)
1455 (*CSC: parametro exp_named_subst? Se no, perche' non li togliamo?         *)
1456 (*CSC: Hint: nella DTD servono per gli stylesheet.                        *)
1457            C.MutInd (uri',i',exp_named_subst) as typ ->
1458             if U.eq uri uri' && i = i' then ([],[],exp_named_subst)
1459             else raise (TypeCheckerFailure (sprintf
1460               "Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}"
1461               (CicPp.ppterm typ) (U.string_of_uri uri) i))
1462          | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
1463             if U.eq uri uri' && i = i' then
1464              let params,args =
1465               split tl (List.length tl - k)
1466              in params,args,exp_named_subst
1467             else raise (TypeCheckerFailure (sprintf
1468               "Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}"
1469               (CicPp.ppterm typ') (U.string_of_uri uri) i))
1470          | _ ->
1471              raise (TypeCheckerFailure (sprintf
1472                "Case analysis: analysed term %s is not an inductive one"
1473                 (CicPp.ppterm term)))
1474       in
1475        (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
1476        let sort_of_ind_type =
1477         if parameters = [] then
1478          C.MutInd (uri,i,exp_named_subst)
1479         else
1480          C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters)
1481        in
1482         if not (check_allowed_sort_elimination context uri i need_dummy
1483          sort_of_ind_type (type_of_aux context sort_of_ind_type) outsort)
1484         then
1485          raise
1486           (TypeCheckerFailure ("Case analasys: sort elimination not allowed"));
1487         (* let's check if the type of branches are right *)
1488         let parsno =
1489          match CicEnvironment.get_cooked_obj ~trust:false uri with
1490             C.InductiveDefinition (_,_,parsno) -> parsno
1491           | _ ->
1492               raise (TypeCheckerFailure
1493                 ("Unknown mutual inductive definition:" ^
1494                 UriManager.string_of_uri uri))
1495         in
1496          let (_,branches_ok) =
1497           List.fold_left
1498            (fun (j,b) p ->
1499              let cons =
1500               if parameters = [] then
1501                (C.MutConstruct (uri,i,j,exp_named_subst))
1502               else
1503                (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
1504              in
1505 (*
1506               (j + 1, b &&
1507 *)
1508               (j + 1,
1509 let res = b &&
1510                R.are_convertible context (type_of_aux context p)
1511                 (type_of_branch context parsno need_dummy outtype cons
1512                   (type_of_aux context cons))
1513 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
1514               )
1515            ) (1,true) pl
1516          in
1517           if not branches_ok then
1518            raise
1519             (TypeCheckerFailure "Case analysys: wrong branch type");
1520           if not need_dummy then
1521            C.Appl ((outtype::arguments)@[term])
1522           else if arguments = [] then
1523            outtype
1524           else
1525            C.Appl (outtype::arguments)
1526    | C.Fix (i,fl) ->
1527       let types_times_kl =
1528        List.rev
1529         (List.map
1530           (fun (n,k,ty,_) ->
1531             let _ = type_of_aux context ty in
1532              (Some (C.Name n,(C.Decl ty)),k)) fl)
1533       in
1534       let (types,kl) = List.split types_times_kl in
1535        let len = List.length types in
1536         List.iter
1537          (fun (name,x,ty,bo) ->
1538            if
1539             (R.are_convertible (types@context) (type_of_aux (types@context) bo)
1540              (CicSubstitution.lift len ty))
1541            then
1542             begin
1543              let (m, eaten, context') =
1544               eat_lambdas (types @ context) (x + 1) bo
1545              in
1546               (*let's control the guarded by destructors conditions D{f,k,x,M}*)
1547               if
1548                not
1549                 (guarded_by_destructors context' eaten (len + eaten) kl 1 [] m)
1550               then
1551                raise
1552                 (TypeCheckerFailure ("Fix: not guarded by destructors"))
1553             end
1554            else
1555             raise (TypeCheckerFailure ("Fix: ill-typed bodies"))
1556          ) fl ;
1557
1558         (*CSC: controlli mancanti solo su D{f,k,x,M} *)
1559         let (_,_,ty,_) = List.nth fl i in
1560         ty
1561    | C.CoFix (i,fl) ->
1562       let types =
1563        List.rev
1564         (List.map
1565           (fun (n,ty,_) ->
1566             let _ = type_of_aux context ty in Some (C.Name n,(C.Decl ty))) fl)
1567       in
1568        let len = List.length types in
1569         List.iter
1570          (fun (_,ty,bo) ->
1571            if
1572             (R.are_convertible (types @ context)
1573              (type_of_aux (types @ context) bo) (CicSubstitution.lift len ty))
1574            then
1575             begin
1576              (* let's control that the returned type is coinductive *)
1577              match returns_a_coinductive context ty with
1578                 None ->
1579                  raise
1580                   (TypeCheckerFailure
1581                     ("CoFix: does not return a coinductive type"))
1582               | Some uri ->
1583                  (*let's control the guarded by constructors conditions C{f,M}*)
1584                  if
1585                   not
1586                    (guarded_by_constructors (types @ context) 0 len false bo
1587                      [] uri)
1588                  then
1589                   raise
1590                    (TypeCheckerFailure ("CoFix: not guarded by constructors"))
1591             end
1592            else
1593             raise
1594              (TypeCheckerFailure ("CoFix: ill-typed bodies"))
1595          ) fl ;
1596
1597         let (_,ty,_) = List.nth fl i in
1598          ty
1599
1600  and check_exp_named_subst context =
1601   let rec check_exp_named_subst_aux substs =
1602    function
1603       [] -> ()
1604     | ((uri,t) as subst)::tl ->
1605        let typeofvar =
1606         CicSubstitution.subst_vars substs (type_of_variable uri) in
1607        (match CicEnvironment.get_cooked_obj ~trust:false uri with
1608            Cic.Variable (_,Some bo,_,_) ->
1609             raise
1610              (TypeCheckerFailure
1611                ("A variable with a body can not be explicit substituted"))
1612          | Cic.Variable (_,None,_,_) -> ()
1613          | _ ->
1614             raise (TypeCheckerFailure
1615               ("Unknown mutual inductive definition:" ^
1616               UriManager.string_of_uri uri))
1617        ) ;
1618        let typeoft = type_of_aux context t in
1619         if CicReduction.are_convertible context typeoft typeofvar then
1620          check_exp_named_subst_aux (substs@[subst]) tl
1621         else
1622          begin
1623           CicReduction.fdebug := 0 ;
1624           ignore (CicReduction.are_convertible context typeoft typeofvar) ;
1625           fdebug := 0 ;
1626           debug typeoft [typeofvar] ;
1627           raise (TypeCheckerFailure "Wrong Explicit Named Substitution")
1628          end
1629   in
1630    check_exp_named_subst_aux []
1631
1632  and sort_of_prod context (name,s) (t1, t2) =
1633   let module C = Cic in
1634    let t1' = CicReduction.whd context t1 in
1635    let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
1636    match (t1', t2') with
1637       (C.Sort s1, C.Sort s2)
1638         when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) -> (* different from Coq manual!!! *)
1639          C.Sort s2
1640     | (C.Sort s1, C.Sort s2) -> C.Sort C.Type (*CSC manca la gestione degli universi!!! *)
1641     | (C.Meta _, C.Sort _) -> t2'
1642     | (C.Meta _, (C.Meta (_,_) as t))
1643     | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
1644         t2'
1645     | (_,_) -> raise (TypeCheckerFailure (sprintf
1646         "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1')
1647           (CicPp.ppterm t2')))
1648
1649  and eat_prods context hetype =
1650   (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
1651   (*CSC: cucinati                                                         *)
1652   function
1653      [] -> hetype
1654    | (hete, hety)::tl ->
1655     (match (CicReduction.whd context hetype) with
1656         Cic.Prod (n,s,t) ->
1657          if CicReduction.are_convertible context s hety then
1658           (CicReduction.fdebug := -1 ;
1659            eat_prods context (CicSubstitution.subst hete t) tl
1660           )
1661          else
1662           begin
1663            CicReduction.fdebug := 0 ;
1664            ignore (CicReduction.are_convertible context s hety) ;
1665            fdebug := 0 ;
1666            debug s [hety] ;
1667            raise (TypeCheckerFailure (sprintf
1668             "Appl: wrong parameter-type, expected %s, found %s"
1669             (CicPp.ppterm hetype) (CicPp.ppterm s)))
1670           end
1671       | _ ->
1672           raise (TypeCheckerFailure
1673             "Appl: this is not a function, it cannot be applied")
1674     )
1675
1676  and returns_a_coinductive context ty =
1677   let module C = Cic in
1678    match CicReduction.whd context ty with
1679       C.MutInd (uri,i,_) ->
1680        (*CSC: definire una funzioncina per questo codice sempre replicato *)
1681        (match CicEnvironment.get_cooked_obj ~trust:false uri with
1682            C.InductiveDefinition (itl,_,_) ->
1683             let (_,is_inductive,_,_) = List.nth itl i in
1684              if is_inductive then None else (Some uri)
1685          | _ ->
1686             raise (TypeCheckerFailure
1687               ("Unknown mutual inductive definition:" ^
1688               UriManager.string_of_uri uri))
1689         )
1690     | C.Appl ((C.MutInd (uri,i,_))::_) ->
1691        (match CicEnvironment.get_obj uri with
1692            C.InductiveDefinition (itl,_,_) ->
1693             let (_,is_inductive,_,_) = List.nth itl i in
1694              if is_inductive then None else (Some uri)
1695          | _ ->
1696             raise (TypeCheckerFailure
1697               ("Unknown mutual inductive definition:" ^
1698               UriManager.string_of_uri uri))
1699         )
1700     | C.Prod (n,so,de) ->
1701        returns_a_coinductive ((Some (n,C.Decl so))::context) de
1702     | _ -> None
1703
1704  in
1705 (*CSC
1706 debug_print ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t) ; flush stderr ;
1707 let res =
1708 *)
1709   type_of_aux context t
1710 (*
1711 in debug_print "FINE TYPE_OF_AUX" ; flush stderr ; res
1712 *)
1713
1714 (* is a small constructor? *)
1715 (*CSC: ottimizzare calcolando staticamente *)
1716 and is_small context paramsno c =
1717  let rec is_small_aux context c =
1718   let module C = Cic in
1719    match CicReduction.whd context c with
1720       C.Prod (n,so,de) ->
1721        (*CSC: [] is an empty metasenv. Is it correct? *)
1722        let s = type_of_aux' [] context so in
1723         (s = C.Sort C.Prop || s = C.Sort C.Set || s = C.Sort C.CProp) &&
1724         is_small_aux ((Some (n,(C.Decl so)))::context) de
1725     | _ -> true (*CSC: we trust the type-checker *)
1726  in
1727   let (context',dx) = split_prods context paramsno c in
1728    is_small_aux context' dx
1729
1730 and type_of t =
1731 (*CSC
1732 debug_print ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t) ; flush stderr ;
1733 let res =
1734 *)
1735  type_of_aux' [] [] t
1736 (*CSC
1737 in debug_print "FINE TYPE_OF_AUX'" ; flush stderr ; res
1738 *)
1739 ;;
1740
1741 let typecheck uri =
1742  let module C = Cic in
1743  let module R = CicReduction in
1744  let module U = UriManager in
1745   match CicEnvironment.is_type_checked ~trust:false uri with
1746      CicEnvironment.CheckedObj _ -> ()
1747    | CicEnvironment.UncheckedObj uobj ->
1748       (* let's typecheck the uncooked object *)
1749       CicLogger.log (`Start_type_checking uri) ;
1750       (match uobj with
1751           C.Constant (_,Some te,ty,_) ->
1752            let _ = type_of ty in
1753             if not (R.are_convertible [] (type_of te ) ty) then
1754               raise (TypeCheckerFailure
1755                 ("Unknown constant:" ^ U.string_of_uri uri))
1756         | C.Constant (_,None,ty,_) ->
1757           (* only to check that ty is well-typed *)
1758           let _ = type_of ty in ()
1759         | C.CurrentProof (_,conjs,te,ty,_) ->
1760            let _ =
1761             List.fold_left
1762              (fun metasenv ((_,context,ty) as conj) ->
1763                ignore (type_of_aux' metasenv context ty) ;
1764                metasenv @ [conj]
1765              ) [] conjs
1766            in
1767             let _ = type_of_aux' conjs [] ty in
1768             let type_of_te = type_of_aux' conjs [] te in
1769              if not (R.are_convertible [] type_of_te ty)
1770              then
1771                raise (TypeCheckerFailure (sprintf
1772                 "the current proof %s is not well typed because the type %s of the body is not convertible to the declared type %s"
1773                 (U.string_of_uri uri) (CicPp.ppterm type_of_te)
1774                 (CicPp.ppterm ty)))
1775         | C.Variable (_,bo,ty,_) ->
1776            (* only to check that ty is well-typed *)
1777            let _ = type_of ty in
1778             (match bo with
1779                 None -> ()
1780               | Some bo ->
1781                  if not (R.are_convertible [] (type_of bo) ty) then
1782                   raise (TypeCheckerFailure
1783                     ("Unknown variable:" ^ U.string_of_uri uri))
1784             )
1785         | C.InductiveDefinition _ ->
1786            check_mutual_inductive_defs uri uobj
1787       ) ;
1788       CicEnvironment.set_type_checking_info uri ;
1789       CicLogger.log (`Type_checking_completed uri)
1790 ;;