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    | (_, _) -> raise (AssertFailure "9")
 635
 636 (*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *)
 637 and check_is_really_smaller_arg context n nn kl x safes te =
 638  (*CSC: forse la whd si puo' fare solo quando serve veramente. *)
 639  (*CSC: cfr guarded_by_destructors                             *)
 640  let module C = Cic in
 641  let module U = UriManager in
 642  match CicReduction.whd context te with
 643      C.Rel m when List.mem m safes -> true
 644    | C.Rel _ -> false
 645    | C.Var _
 646    | C.Meta _
 647    | C.Sort _
 648    | C.Implicit
 649    | C.Cast _
 650 (*   | C.Cast (te,ty) ->
 651       check_is_really_smaller_arg n nn kl x safes te &&
 652        check_is_really_smaller_arg n nn kl x safes ty*)
 653 (*   | C.Prod (_,so,ta) ->
 654       check_is_really_smaller_arg n nn kl x safes so &&
 655        check_is_really_smaller_arg (n+1) (nn+1) kl (x+1)
 656         (List.map (fun x -> x + 1) safes) ta*)
 657    | C.Prod _ -> raise (AssertFailure "10")
 658    | C.Lambda (name,so,ta) ->
 659       check_is_really_smaller_arg context n nn kl x safes so &&
 660        check_is_really_smaller_arg ((Some (name,(C.Decl so)))::context)
 661         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 662    | C.LetIn (name,so,ta) ->
 663       check_is_really_smaller_arg context n nn kl x safes so &&
 664        check_is_really_smaller_arg ((Some (name,(C.Def (so,None))))::context)
 665         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 666    | C.Appl (he::_) ->
 667       (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
 668       (*CSC: solo perche' non abbiamo trovato controesempi            *)
 669       check_is_really_smaller_arg context n nn kl x safes he
 670    | C.Appl [] -> raise (AssertFailure "11")
 671    | C.Const _
 672    | C.MutInd _ -> raise (AssertFailure "12")
 673    | C.MutConstruct _ -> false
 674    | C.MutCase (uri,i,outtype,term,pl) ->
 675       (match term with
 676           C.Rel m when List.mem m safes || m = x ->
 677            let (tys,len,isinductive,paramsno,cl) =
 678             match CicEnvironment.get_obj uri with
 679                C.InductiveDefinition (tl,_,paramsno) ->
 680                 let tys =
 681                  List.map
 682                   (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl
 683                 in
 684                  let (_,isinductive,_,cl) = List.nth tl i in
 685                   let cl' =
 686                    List.map
 687                     (fun (id,ty) ->
 688                       (id, snd (split_prods tys paramsno ty))) cl
 689                   in
 690                    (tys,List.length tl,isinductive,paramsno,cl')
 691              | _ ->
 692                 raise (TypeCheckerFailure
 693                   ("Unknown mutual inductive definition:" ^
 694                   UriManager.string_of_uri uri))
 695            in
 696             if not isinductive then
 697               List.fold_right
 698                (fun p i ->
 699                  i && check_is_really_smaller_arg context n nn kl x safes p)
 700                pl true
 701             else
 702               List.fold_right
 703                (fun (p,(_,c)) i ->
 704                  let rl' =
 705                   let debrujinedte = debrujin_constructor uri len c in
 706                    recursive_args tys 0 len debrujinedte
 707                  in
 708                   let (e,safes',n',nn',x',context') =
 709                    get_new_safes context p c rl' safes n nn x
 710                   in
 711                    i &&
 712                    check_is_really_smaller_arg context' n' nn' kl x' safes' e
 713                ) (List.combine pl cl) true
 714         | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
 715            let (tys,len,isinductive,paramsno,cl) =
 716             match CicEnvironment.get_obj uri with
 717                C.InductiveDefinition (tl,_,paramsno) ->
 718                 let (_,isinductive,_,cl) = List.nth tl i in
 719                  let tys =
 720                   List.map (fun (n,_,ty,_) ->
 721                    Some(Cic.Name n,(Cic.Decl ty))) tl
 722                  in
 723                   let cl' =
 724                    List.map
 725                     (fun (id,ty) ->
 726                       (id, snd (split_prods tys paramsno ty))) cl
 727                   in
 728                    (tys,List.length tl,isinductive,paramsno,cl')
 729              | _ ->
 730                 raise (TypeCheckerFailure
 731                   ("Unknown mutual inductive definition:" ^
 732                   UriManager.string_of_uri uri))
 733            in
 734             if not isinductive then
 735               List.fold_right
 736                (fun p i ->
 737                  i && check_is_really_smaller_arg context n nn kl x safes p)
 738                pl true
 739             else
 740               (*CSC: supponiamo come prima che nessun controllo sia necessario*)
 741               (*CSC: sugli argomenti di una applicazione                      *)
 742               List.fold_right
 743                (fun (p,(_,c)) i ->
 744                  let rl' =
 745                   let debrujinedte = debrujin_constructor uri len c in
 746                    recursive_args tys 0 len debrujinedte
 747                  in
 748                   let (e, safes',n',nn',x',context') =
 749                    get_new_safes context p c rl' safes n nn x
 750                   in
 751                    i &&
 752                    check_is_really_smaller_arg context' n' nn' kl x' safes' e
 753                ) (List.combine pl cl) true
 754         | _ ->
 755           List.fold_right
 756            (fun p i ->
 757              i && check_is_really_smaller_arg context n nn kl x safes p
 758            ) pl true
 759       )
 760    | C.Fix (_, fl) ->
 761       let len = List.length fl in
 762        let n_plus_len = n + len
 763        and nn_plus_len = nn + len
 764        and x_plus_len = x + len
 765        and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
 766        and safes' = List.map (fun x -> x + len) safes in
 767         List.fold_right
 768          (fun (_,_,ty,bo) i ->
 769            i &&
 770             check_is_really_smaller_arg (tys@context) n_plus_len nn_plus_len kl
 771              x_plus_len safes' bo
 772          ) fl true
 773    | C.CoFix (_, fl) ->
 774       let len = List.length fl in
 775        let n_plus_len = n + len
 776        and nn_plus_len = nn + len
 777        and x_plus_len = x + len
 778        and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
 779        and safes' = List.map (fun x -> x + len) safes in
 780         List.fold_right
 781          (fun (_,ty,bo) i ->
 782            i &&
 783             check_is_really_smaller_arg (tys@context) n_plus_len nn_plus_len kl
 784              x_plus_len safes' bo
 785          ) fl true
 786
 787 and guarded_by_destructors context n nn kl x safes =
 788  let module C = Cic in
 789  let module U = UriManager in
 790   function
 791      C.Rel m when m > n && m <= nn -> false
 792    | C.Rel n ->
 793       (match List.nth context (n-1) with
 794           Some (_,C.Decl _) -> true
 795         | Some (_,C.Def (bo,_)) ->
 796            guarded_by_destructors context n nn kl x safes bo
 797         | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
 798       )
 799    | C.Meta _
 800    | C.Sort _
 801    | C.Implicit -> true
 802    | C.Cast (te,ty) ->
 803       guarded_by_destructors context n nn kl x safes te &&
 804        guarded_by_destructors context n nn kl x safes ty
 805    | C.Prod (name,so,ta) ->
 806       guarded_by_destructors context n nn kl x safes so &&
 807        guarded_by_destructors ((Some (name,(C.Decl so)))::context)
 808         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 809    | C.Lambda (name,so,ta) ->
 810       guarded_by_destructors context n nn kl x safes so &&
 811        guarded_by_destructors ((Some (name,(C.Decl so)))::context)
 812         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 813    | C.LetIn (name,so,ta) ->
 814       guarded_by_destructors context n nn kl x safes so &&
 815        guarded_by_destructors ((Some (name,(C.Def (so,None))))::context)
 816         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 817    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
 818       let k = List.nth kl (m - n - 1) in
 819        if not (List.length tl > k) then false
 820        else
 821         List.fold_right
 822          (fun param i ->
 823            i && guarded_by_destructors context n nn kl x safes param
 824          ) tl true &&
 825          check_is_really_smaller_arg context n nn kl x safes (List.nth tl k)
 826    | C.Appl tl ->
 827       List.fold_right
 828        (fun t i -> i && guarded_by_destructors context n nn kl x safes t)
 829        tl true
 830    | C.Var (_,exp_named_subst)
 831    | C.Const (_,exp_named_subst)
 832    | C.MutInd (_,_,exp_named_subst)
 833    | C.MutConstruct (_,_,_,exp_named_subst) ->
 834       List.fold_right
 835        (fun (_,t) i -> i && guarded_by_destructors context n nn kl x safes t)
 836        exp_named_subst true
 837    | C.MutCase (uri,i,outtype,term,pl) ->
 838       (match term with
 839           C.Rel m when List.mem m safes || m = x ->
 840            let (tys,len,isinductive,paramsno,cl) =
 841             match CicEnvironment.get_obj uri with
 842                C.InductiveDefinition (tl,_,paramsno) ->
 843                 let (_,isinductive,_,cl) = List.nth tl i in
 844                  let tys =
 845                   List.map (fun (n,_,ty,_) ->
 846                    Some(Cic.Name n,(Cic.Decl ty))) tl
 847                  in
 848                   let cl' =
 849                    List.map
 850                     (fun (id,ty) ->
 851                       (id, snd (split_prods tys paramsno ty))) cl
 852                   in
 853                    (tys,List.length tl,isinductive,paramsno,cl')
 854              | _ ->
 855                 raise (TypeCheckerFailure
 856                   ("Unknown mutual inductive definition:" ^
 857                   UriManager.string_of_uri uri))
 858            in
 859             if not isinductive then
 860              guarded_by_destructors context n nn kl x safes outtype &&
 861               guarded_by_destructors context n nn kl x safes term &&
 862               (*CSC: manca ??? il controllo sul tipo di term? *)
 863               List.fold_right
 864                (fun p i ->
 865                  i && guarded_by_destructors context n nn kl x safes p)
 866                pl true
 867             else
 868              guarded_by_destructors context n nn kl x safes outtype &&
 869               (*CSC: manca ??? il controllo sul tipo di term? *)
 870               List.fold_right
 871                (fun (p,(_,c)) i ->
 872                  let rl' =
 873                   let debrujinedte = debrujin_constructor uri len c in
 874                    recursive_args tys 0 len debrujinedte
 875                  in
 876                   let (e,safes',n',nn',x',context') =
 877                    get_new_safes context p c rl' safes n nn x
 878                   in
 879                    i &&
 880                    guarded_by_destructors context' n' nn' kl x' safes' e
 881                ) (List.combine pl cl) true
 882         | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
 883            let (tys,len,isinductive,paramsno,cl) =
 884             match CicEnvironment.get_obj uri with
 885                C.InductiveDefinition (tl,_,paramsno) ->
 886                 let (_,isinductive,_,cl) = List.nth tl i in
 887                  let tys =
 888                   List.map
 889                    (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
 890                  in
 891                   let cl' =
 892                    List.map
 893                     (fun (id,ty) ->
 894                       (id, snd (split_prods tys paramsno ty))) cl
 895                   in
 896                    (tys,List.length tl,isinductive,paramsno,cl')
 897              | _ ->
 898                 raise (TypeCheckerFailure
 899                   ("Unknown mutual inductive definition:" ^
 900                   UriManager.string_of_uri uri))
 901            in
 902             if not isinductive then
 903              guarded_by_destructors context n nn kl x safes outtype &&
 904               guarded_by_destructors context n nn kl x safes term &&
 905               (*CSC: manca ??? il controllo sul tipo di term? *)
 906               List.fold_right
 907                (fun p i ->
 908                  i && guarded_by_destructors context n nn kl x safes p)
 909                pl true
 910             else
 911              guarded_by_destructors context n nn kl x safes outtype &&
 912               (*CSC: manca ??? il controllo sul tipo di term? *)
 913               List.fold_right
 914                (fun t i ->
 915                  i && guarded_by_destructors context n nn kl x safes t)
 916                tl true &&
 917               List.fold_right
 918                (fun (p,(_,c)) i ->
 919                  let rl' =
 920                   let debrujinedte = debrujin_constructor uri len c in
 921                    recursive_args tys 0 len debrujinedte
 922                  in
 923                   let (e, safes',n',nn',x',context') =
 924                    get_new_safes context p c rl' safes n nn x
 925                   in
 926                    i &&
 927                    guarded_by_destructors context' n' nn' kl x' safes' e
 928                ) (List.combine pl cl) true
 929         | _ ->
 930           guarded_by_destructors context n nn kl x safes outtype &&
 931            guarded_by_destructors context n nn kl x safes term &&
 932            (*CSC: manca ??? il controllo sul tipo di term? *)
 933            List.fold_right
 934             (fun p i -> i && guarded_by_destructors context n nn kl x safes p)
 935             pl true
 936       )
 937    | C.Fix (_, fl) ->
 938       let len = List.length fl in
 939        let n_plus_len = n + len
 940        and nn_plus_len = nn + len
 941        and x_plus_len = x + len
 942        and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
 943        and safes' = List.map (fun x -> x + len) safes in
 944         List.fold_right
 945          (fun (_,_,ty,bo) i ->
 946            i && guarded_by_destructors context n nn kl x_plus_len safes' ty &&
 947             guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
 948              x_plus_len safes' bo
 949          ) fl true
 950    | C.CoFix (_, fl) ->
 951       let len = List.length fl in
 952        let n_plus_len = n + len
 953        and nn_plus_len = nn + len
 954        and x_plus_len = x + len
 955        and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
 956        and safes' = List.map (fun x -> x + len) safes in
 957         List.fold_right
 958          (fun (_,ty,bo) i ->
 959            i &&
 960             guarded_by_destructors context n nn kl x_plus_len safes' ty &&
 961             guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
 962              x_plus_len safes' bo
 963          ) fl true
 964
 965 (* the boolean h means already protected *)
 966 (* args is the list of arguments the type of the constructor that may be *)
 967 (* found in head position must be applied to.                            *)
 968 (*CSC: coInductiveTypeURI non cambia mai di ricorsione in ricorsione *)
 969 and guarded_by_constructors context n nn h te args coInductiveTypeURI =
 970  let module C = Cic in
 971   (*CSC: There is a lot of code replication between the cases X and    *)
 972   (*CSC: (C.Appl X tl). Maybe it will be better to define a function   *)
 973   (*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *)
 974   match CicReduction.whd context te with
 975      C.Rel m when m > n && m <= nn -> h
 976    | C.Rel _ -> true
 977    | C.Meta _
 978    | C.Sort _
 979    | C.Implicit
 980    | C.Cast _
 981    | C.Prod _
 982    | C.LetIn _ ->
 983       (* the term has just been type-checked *)
 984       raise (AssertFailure "17")
 985    | C.Lambda (name,so,de) ->
 986       does_not_occur context n nn so &&
 987        guarded_by_constructors ((Some (name,(C.Decl so)))::context)
 988         (n + 1) (nn + 1) h de args coInductiveTypeURI
 989    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
 990       h &&
 991        List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
 992    | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) ->
 993       let consty =
 994        match CicEnvironment.get_cooked_obj ~trust:false uri with
 995           C.InductiveDefinition (itl,_,_) ->
 996            let (_,_,_,cl) = List.nth itl i in
 997             let (_,cons) = List.nth cl (j - 1) in
 998              CicSubstitution.subst_vars exp_named_subst cons
 999         | _ ->
1000             raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1001               UriManager.string_of_uri uri))
1002       in
1003        let rec analyse_branch context ty te =
1004         match CicReduction.whd context ty with
1005            C.Meta _ -> raise (AssertFailure "34")
1006          | C.Rel _
1007          | C.Var _
1008          | C.Sort _ ->
1009             does_not_occur context n nn te
1010          | C.Implicit
1011          | C.Cast _ ->
1012             raise (AssertFailure "24")(* due to type-checking *)
1013          | C.Prod (name,so,de) ->
1014             analyse_branch ((Some (name,(C.Decl so)))::context) de te
1015          | C.Lambda _
1016          | C.LetIn _ ->
1017             raise (AssertFailure "25")(* due to type-checking *)
1018          | C.Appl ((C.MutInd (uri,_,_))::_) as ty
1019             when uri == coInductiveTypeURI ->
1020              guarded_by_constructors context n nn true te [] coInductiveTypeURI
1021          | C.Appl ((C.MutInd (uri,_,_))::_) as ty ->
1022             guarded_by_constructors context n nn true te tl coInductiveTypeURI
1023          | C.Appl _ ->
1024             does_not_occur context n nn te
1025          | C.Const _ -> raise (AssertFailure "26")
1026          | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
1027             guarded_by_constructors context n nn true te [] coInductiveTypeURI
1028          | C.MutInd _ ->
1029             does_not_occur context n nn te
1030          | C.MutConstruct _ -> raise (AssertFailure "27")
1031          (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
1032          (*CSC: in head position.                                       *)
1033          | C.MutCase _
1034          | C.Fix _
1035          | C.CoFix _ ->
1036             raise (AssertFailure "28")(* due to type-checking *)
1037        in
1038        let rec analyse_instantiated_type context ty l =
1039         match CicReduction.whd context ty with
1040            C.Rel _
1041          | C.Var _
1042          | C.Meta _
1043          | C.Sort _
1044          | C.Implicit
1045          | C.Cast _ -> raise (AssertFailure "29")(* due to type-checking *)
1046          | C.Prod (name,so,de) ->
1047             begin
1048              match l with
1049                 [] -> true
1050               | he::tl ->
1051                  analyse_branch context so he &&
1052                   analyse_instantiated_type
1053                    ((Some (name,(C.Decl so)))::context) de tl
1054             end
1055          | C.Lambda _
1056          | C.LetIn _ ->
1057             raise (AssertFailure "30")(* due to type-checking *)
1058          | C.Appl _ ->
1059             List.fold_left
1060              (fun i x -> i && does_not_occur context n nn x) true l
1061          | C.Const _ -> raise (AssertFailure "31")
1062          | C.MutInd _ ->
1063             List.fold_left
1064              (fun i x -> i && does_not_occur context n nn x) true l
1065          | C.MutConstruct _ -> raise (AssertFailure "32")
1066          (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
1067          (*CSC: in head position.                                       *)
1068          | C.MutCase _
1069          | C.Fix _
1070          | C.CoFix _ ->
1071             raise (AssertFailure "33")(* due to type-checking *)
1072        in
1073         let rec instantiate_type args consty =
1074          function
1075             [] -> true
1076           | tlhe::tltl as l ->
1077              let consty' = CicReduction.whd context consty in
1078               match args with
1079                  he::tl ->
1080                   begin
1081                    match consty' with
1082                       C.Prod (_,_,de) ->
1083                        let instantiated_de = CicSubstitution.subst he de in
1084                         (*CSC: siamo sicuri che non sia troppo forte? *)
1085                         does_not_occur context n nn tlhe &
1086                          instantiate_type tl instantiated_de tltl
1087                     | _ ->
1088                       (*CSC:We do not consider backbones with a MutCase, a    *)
1089                       (*CSC:FixPoint, a CoFixPoint and so on in head position.*)
1090                       raise (AssertFailure "23")
1091                   end
1092                | [] -> analyse_instantiated_type context consty' l
1093                   (* These are all the other cases *)
1094        in
1095         instantiate_type args consty tl
1096    | C.Appl ((C.CoFix (_,fl))::tl) ->
1097       List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
1098        let len = List.length fl in
1099         let n_plus_len = n + len
1100         and nn_plus_len = nn + len
1101         (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1102         and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1103          List.fold_right
1104           (fun (_,ty,bo) i ->
1105             i && does_not_occur context n nn ty &&
1106              guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1107               args coInductiveTypeURI
1108           ) fl true
1109    | C.Appl ((C.MutCase (_,_,out,te,pl))::tl) ->
1110        List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
1111         does_not_occur context n nn out &&
1112          does_not_occur context n nn te &&
1113           List.fold_right
1114            (fun x i ->
1115              i &&
1116              guarded_by_constructors context n nn h x args coInductiveTypeURI
1117            ) pl true
1118    | C.Appl l ->
1119       List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
1120    | C.Var (_,exp_named_subst)
1121    | C.Const (_,exp_named_subst) ->
1122       List.fold_right
1123        (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
1124    | C.MutInd _ -> assert false
1125    | C.MutConstruct (_,_,_,exp_named_subst) ->
1126       List.fold_right
1127        (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
1128    | C.MutCase (_,_,out,te,pl) ->
1129        does_not_occur context n nn out &&
1130         does_not_occur context n nn te &&
1131          List.fold_right
1132           (fun x i ->
1133             i &&
1134              guarded_by_constructors context n nn h x args coInductiveTypeURI
1135           ) pl true
1136    | C.Fix (_,fl) ->
1137       let len = List.length fl in
1138        let n_plus_len = n + len
1139        and nn_plus_len = nn + len
1140        (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1141        and tys = List.map (fun (n,_,ty,_)-> Some (C.Name n,(C.Decl ty))) fl in
1142         List.fold_right
1143          (fun (_,_,ty,bo) i ->
1144            i && does_not_occur context n nn ty &&
1145             does_not_occur (tys@context) n_plus_len nn_plus_len bo
1146          ) fl true
1147    | C.CoFix (_,fl) ->
1148       let len = List.length fl in
1149        let n_plus_len = n + len
1150        and nn_plus_len = nn + len
1151        (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1152        and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1153         List.fold_right
1154          (fun (_,ty,bo) i ->
1155            i && does_not_occur context n nn ty &&
1156             guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1157              args coInductiveTypeURI
1158          ) fl true
1159
1160 and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 =
1161  let module C = Cic in
1162  let module U = UriManager in
1163   match (CicReduction.whd context arity1, CicReduction.whd context arity2) with
1164      (C.Prod (_,so1,de1), C.Prod (_,so2,de2))
1165       when CicReduction.are_convertible context so1 so2 ->
1166        check_allowed_sort_elimination context uri i need_dummy
1167         (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2
1168    | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true
1169    | (C.Sort C.Prop, C.Sort C.Set)
1170    | (C.Sort C.Prop, C.Sort C.CProp)
1171    | (C.Sort C.Prop, C.Sort C.Type) when need_dummy ->
1172 (*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *)
1173        (match CicEnvironment.get_obj uri with
1174            C.InductiveDefinition (itl,_,_) ->
1175             let (_,_,_,cl) = List.nth itl i in
1176              (* is a singleton definition or the empty proposition? *)
1177              List.length cl = 1 || List.length cl = 0
1178          | _ ->
1179             raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1180               UriManager.string_of_uri uri))
1181        )
1182    | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true
1183    | (C.Sort C.CProp, C.Sort C.Prop) when need_dummy -> true
1184    | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true
1185    | (C.Sort C.Set, C.Sort C.CProp) when need_dummy -> true
1186    | (C.Sort C.CProp, C.Sort C.Set) when need_dummy -> true
1187    | (C.Sort C.CProp, C.Sort C.CProp) when need_dummy -> true
1188    | ((C.Sort C.Set, C.Sort C.Type) | (C.Sort C.CProp, C.Sort C.Type))
1189       when need_dummy ->
1190        (match CicEnvironment.get_obj uri with
1191            C.InductiveDefinition (itl,_,paramsno) ->
1192             let tys =
1193              List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1194             in
1195              let (_,_,_,cl) = List.nth itl i in
1196               List.fold_right
1197                (fun (_,x) i -> i && is_small tys paramsno x) cl true
1198          | _ ->
1199             raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1200               UriManager.string_of_uri uri))
1201        )
1202    | (C.Sort C.Type, C.Sort _) when need_dummy -> true
1203    | (C.Sort C.Prop, C.Prod (name,so,ta)) when not need_dummy ->
1204        let res = CicReduction.are_convertible context so ind
1205        in
1206         res &&
1207         (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1208             C.Sort C.Prop -> true
1209           | (C.Sort C.Set | C.Sort C.CProp) ->
1210              (match CicEnvironment.get_obj uri with
1211                  C.InductiveDefinition (itl,_,_) ->
1212                   let (_,_,_,cl) = List.nth itl i in
1213                    (* is a singleton definition? *)
1214                    List.length cl = 1
1215                | _ ->
1216                   raise (TypeCheckerFailure
1217                     ("Unknown mutual inductive definition:" ^
1218                     UriManager.string_of_uri uri))
1219              )
1220           | _ -> false
1221         )
1222    | ((C.Sort C.Set, C.Prod (name,so,ta)) | (C.Sort C.CProp, C.Prod (name,so,ta)))
1223       when not need_dummy ->
1224        let res = CicReduction.are_convertible context so ind
1225        in
1226         res &&
1227         (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1228             C.Sort C.Prop
1229           | C.Sort C.Set  -> true
1230           | C.Sort C.CProp -> true
1231           | C.Sort C.Type ->
1232              (match CicEnvironment.get_obj uri with
1233                  C.InductiveDefinition (itl,_,paramsno) ->
1234                   let (_,_,_,cl) = List.nth itl i in
1235                    let tys =
1236                     List.map
1237                      (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1238                    in
1239                     List.fold_right
1240                      (fun (_,x) i -> i && is_small tys paramsno x) cl true
1241                | _ ->
1242                   raise (TypeCheckerFailure
1243                     ("Unknown mutual inductive definition:" ^
1244                     UriManager.string_of_uri uri))
1245              )
1246           | _ -> raise (AssertFailure "19")
1247         )
1248    | (C.Sort C.Type, C.Prod (_,so,_)) when not need_dummy ->
1249        CicReduction.are_convertible context so ind
1250    | (_,_) -> false
1251
1252 and type_of_branch context argsno need_dummy outtype term constype =
1253  let module C = Cic in
1254  let module R = CicReduction in
1255   match R.whd context constype with
1256      C.MutInd (_,_,_) ->
1257       if need_dummy then
1258        outtype
1259       else
1260        C.Appl [outtype ; term]
1261    | C.Appl (C.MutInd (_,_,_)::tl) ->
1262       let (_,arguments) = split tl argsno
1263       in
1264        if need_dummy && arguments = [] then
1265         outtype
1266        else
1267         C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
1268    | C.Prod (name,so,de) ->
1269       let term' =
1270        match CicSubstitution.lift 1 term with
1271           C.Appl l -> C.Appl (l@[C.Rel 1])
1272         | t -> C.Appl [t ; C.Rel 1]
1273       in
1274        C.Prod (C.Anonymous,so,type_of_branch
1275         ((Some (name,(C.Decl so)))::context) argsno need_dummy
1276         (CicSubstitution.lift 1 outtype) term' de)
1277   | _ -> raise (AssertFailure "20")
1278
1279 (* check_metasenv_consistency checks that the "canonical" context of a
1280 metavariable is consitent - up to relocation via the relocation list l -
1281 with the actual context *)
1282
1283 and check_metasenv_consistency metasenv context canonical_context l =
1284   let module C = Cic in
1285   let module R = CicReduction in
1286   let module S = CicSubstitution in
1287    let lifted_canonical_context =
1288     let rec aux i =
1289      function
1290         [] -> []
1291       | (Some (n,C.Decl t))::tl ->
1292          (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
1293       | (Some (n,C.Def (t,None)))::tl ->
1294          (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
1295       | None::tl -> None::(aux (i+1) tl)
1296       | (Some (n,C.Def (_,Some _)))::_ -> assert false
1297     in
1298      aux 1 canonical_context
1299    in
1300     List.iter2
1301      (fun t ct ->
1302         match (t,ct) with
1303          | _,None -> ()
1304          | Some t,Some (_,C.Def (ct,_)) ->
1305             if not (R.are_convertible context t ct) then
1306               raise (TypeCheckerFailure (sprintf
1307                 "Not well typed metavariable local context: expected a term convertible with %s, found %s"
1308                 (CicPp.ppterm ct) (CicPp.ppterm t)))
1309          | Some t,Some (_,C.Decl ct) ->
1310              let type_t = type_of_aux' metasenv context t in
1311              if not (R.are_convertible context type_t ct) then
1312               raise (TypeCheckerFailure (sprintf
1313                 "Not well typed metavariable local context: expected a term of type %s, found %s of type %s"
1314                 (CicPp.ppterm ct) (CicPp.ppterm t) (CicPp.ppterm type_t)))
1315          | None, _  ->
1316              raise (TypeCheckerFailure
1317               "Not well typed metavariable local context: an hypothesis, that is not hidden, is not instantiated")
1318      ) l lifted_canonical_context
1319
1320 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
1321 and type_of_aux' metasenv context t =
1322  let rec type_of_aux context =
1323   let module C = Cic in
1324   let module R = CicReduction in
1325   let module S = CicSubstitution in
1326   let module U = UriManager in
1327    function
1328       C.Rel n ->
1329        (try
1330          match List.nth context (n - 1) with
1331             Some (_,C.Decl t) -> S.lift n t
1332           | Some (_,C.Def (_,Some ty)) -> S.lift n ty
1333           | Some (_,C.Def (bo,None)) ->
1334              debug_print "##### CASO DA INVESTIGARE E CAPIRE" ;
1335              type_of_aux context (S.lift n bo)
1336           | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
1337         with
1338         _ ->
1339           raise (TypeCheckerFailure
1340             "unbound variable found in constructor type")
1341        )
1342     | C.Var (uri,exp_named_subst) ->
1343       incr fdebug ;
1344       check_exp_named_subst context exp_named_subst ;
1345       let ty =
1346        CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
1347       in
1348        decr fdebug ;
1349        ty
1350     | C.Meta (n,l) ->
1351        let (_,canonical_context,ty) =
1352         List.find (function (m,_,_) -> n = m) metasenv
1353        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     | (_,_) ->
1642       raise (TypeCheckerFailure (sprintf
1643         "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1')
1644           (CicPp.ppterm t2')))
1645
1646  and eat_prods context hetype =
1647   (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
1648   (*CSC: cucinati                                                         *)
1649   function
1650      [] -> hetype
1651    | (hete, hety)::tl ->
1652     (match (CicReduction.whd context hetype) with
1653         Cic.Prod (n,s,t) ->
1654          if CicReduction.are_convertible context s hety then
1655           (CicReduction.fdebug := -1 ;
1656            eat_prods context (CicSubstitution.subst hete t) tl
1657           )
1658          else
1659           begin
1660            CicReduction.fdebug := 0 ;
1661            ignore (CicReduction.are_convertible context s hety) ;
1662            fdebug := 0 ;
1663            debug s [hety] ;
1664            raise (TypeCheckerFailure (sprintf
1665             "Appl: wrong parameter-type, expected %s, found %s"
1666             (CicPp.ppterm hetype) (CicPp.ppterm s)))
1667           end
1668       | _ ->
1669           raise (TypeCheckerFailure
1670             "Appl: this is not a function, it cannot be applied")
1671     )
1672
1673  and returns_a_coinductive context ty =
1674   let module C = Cic in
1675    match CicReduction.whd context ty with
1676       C.MutInd (uri,i,_) ->
1677        (*CSC: definire una funzioncina per questo codice sempre replicato *)
1678        (match CicEnvironment.get_cooked_obj ~trust:false uri with
1679            C.InductiveDefinition (itl,_,_) ->
1680             let (_,is_inductive,_,_) = List.nth itl i in
1681              if is_inductive then None else (Some uri)
1682          | _ ->
1683             raise (TypeCheckerFailure
1684               ("Unknown mutual inductive definition:" ^
1685               UriManager.string_of_uri uri))
1686         )
1687     | C.Appl ((C.MutInd (uri,i,_))::_) ->
1688        (match CicEnvironment.get_obj uri with
1689            C.InductiveDefinition (itl,_,_) ->
1690             let (_,is_inductive,_,_) = List.nth itl i in
1691              if is_inductive then None else (Some uri)
1692          | _ ->
1693             raise (TypeCheckerFailure
1694               ("Unknown mutual inductive definition:" ^
1695               UriManager.string_of_uri uri))
1696         )
1697     | C.Prod (n,so,de) ->
1698        returns_a_coinductive ((Some (n,C.Decl so))::context) de
1699     | _ -> None
1700
1701  in
1702 (*CSC
1703 debug_print ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t) ; flush stderr ;
1704 let res =
1705 *)
1706   type_of_aux context t
1707 (*
1708 in debug_print "FINE TYPE_OF_AUX" ; flush stderr ; res
1709 *)
1710
1711 (* is a small constructor? *)
1712 (*CSC: ottimizzare calcolando staticamente *)
1713 and is_small context paramsno c =
1714  let rec is_small_aux context c =
1715   let module C = Cic in
1716    match CicReduction.whd context c with
1717       C.Prod (n,so,de) ->
1718        (*CSC: [] is an empty metasenv. Is it correct? *)
1719        let s = type_of_aux' [] context so in
1720         (s = C.Sort C.Prop || s = C.Sort C.Set || s = C.Sort C.CProp) &&
1721         is_small_aux ((Some (n,(C.Decl so)))::context) de
1722     | _ -> true (*CSC: we trust the type-checker *)
1723  in
1724   let (context',dx) = split_prods context paramsno c in
1725    is_small_aux context' dx
1726
1727 and type_of t =
1728 (*CSC
1729 debug_print ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t) ; flush stderr ;
1730 let res =
1731 *)
1732  type_of_aux' [] [] t
1733 (*CSC
1734 in debug_print "FINE TYPE_OF_AUX'" ; flush stderr ; res
1735 *)
1736 ;;
1737
1738 let typecheck uri =
1739  let module C = Cic in
1740  let module R = CicReduction in
1741  let module U = UriManager in
1742   match CicEnvironment.is_type_checked ~trust:false uri with
1743      CicEnvironment.CheckedObj _ -> ()
1744    | CicEnvironment.UncheckedObj uobj ->
1745       (* let's typecheck the uncooked object *)
1746       CicLogger.log (`Start_type_checking uri) ;
1747       (match uobj with
1748           C.Constant (_,Some te,ty,_) ->
1749            let _ = type_of ty in
1750             if not (R.are_convertible [] (type_of te ) ty) then
1751               raise (TypeCheckerFailure
1752                 ("Unknown constant:" ^ U.string_of_uri uri))
1753         | C.Constant (_,None,ty,_) ->
1754           (* only to check that ty is well-typed *)
1755           let _ = type_of ty in ()
1756         | C.CurrentProof (_,conjs,te,ty,_) ->
1757            let _ =
1758             List.fold_left
1759              (fun metasenv ((_,context,ty) as conj) ->
1760                ignore (type_of_aux' metasenv context ty) ;
1761                metasenv @ [conj]
1762              ) [] conjs
1763            in
1764             let _ = type_of_aux' conjs [] ty in
1765             let type_of_te = type_of_aux' conjs [] te in
1766              if not (R.are_convertible [] type_of_te ty)
1767              then
1768                raise (TypeCheckerFailure (sprintf
1769                 "the current proof %s is not well typed because the type %s of the body is not convertible to the declared type %s"
1770                 (U.string_of_uri uri) (CicPp.ppterm type_of_te)
1771                 (CicPp.ppterm ty)))
1772         | C.Variable (_,bo,ty,_) ->
1773            (* only to check that ty is well-typed *)
1774            let _ = type_of ty in
1775             (match bo with
1776                 None -> ()
1777               | Some bo ->
1778                  if not (R.are_convertible [] (type_of bo) ty) then
1779                   raise (TypeCheckerFailure
1780                     ("Unknown variable:" ^ U.string_of_uri uri))
1781             )
1782         | C.InductiveDefinition _ ->
1783            check_mutual_inductive_defs uri uobj
1784       ) ;
1785       CicEnvironment.set_type_checking_info uri ;
1786       CicLogger.log (`Type_checking_completed uri)
1787 ;;