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 (HelmLibraryObjects.Datatypes.nat_URI,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    | (c,p,l) ->
 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
 614        (AssertFailure
 615          (Printf.sprintf "Get New Safes: c=%s ; p=%s"
 616            (CicPp.ppterm c) (CicPp.ppterm p)))
 617
 618 and split_prods context n te =
 619  let module C = Cic in
 620  let module R = CicReduction in
 621   match (n, R.whd context te) with
 622      (0, _) -> context,te
 623    | (n, C.Prod (name,so,ta)) when n > 0 ->
 624        split_prods ((Some (name,(C.Decl so)))::context) (n - 1) ta
 625    | (_, _) -> raise (AssertFailure "8")
 626
 627 and eat_lambdas context n te =
 628  let module C = Cic in
 629  let module R = CicReduction in
 630   match (n, R.whd context te) with
 631      (0, _) -> (te, 0, context)
 632    | (n, C.Lambda (name,so,ta)) when n > 0 ->
 633       let (te, k, context') =
 634        eat_lambdas ((Some (name,(C.Decl so)))::context) (n - 1) ta
 635       in
 636        (te, k + 1, context')
 637    | (n, te) ->
 638        raise (AssertFailure (sprintf "9 (%d, %s)" n (CicPp.ppterm te)))
 639
 640 (*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *)
 641 and check_is_really_smaller_arg context n nn kl x safes te =
 642  (*CSC: forse la whd si puo' fare solo quando serve veramente. *)
 643  (*CSC: cfr guarded_by_destructors                             *)
 644  let module C = Cic in
 645  let module U = UriManager in
 646  match CicReduction.whd context te with
 647      C.Rel m when List.mem m safes -> true
 648    | C.Rel _ -> false
 649    | C.Var _
 650    | C.Meta _
 651    | C.Sort _
 652    | C.Implicit _
 653    | C.Cast _
 654 (*   | C.Cast (te,ty) ->
 655       check_is_really_smaller_arg n nn kl x safes te &&
 656        check_is_really_smaller_arg n nn kl x safes ty*)
 657 (*   | C.Prod (_,so,ta) ->
 658       check_is_really_smaller_arg n nn kl x safes so &&
 659        check_is_really_smaller_arg (n+1) (nn+1) kl (x+1)
 660         (List.map (fun x -> x + 1) safes) ta*)
 661    | C.Prod _ -> raise (AssertFailure "10")
 662    | C.Lambda (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.Decl so)))::context)
 665         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 666    | C.LetIn (name,so,ta) ->
 667       check_is_really_smaller_arg context n nn kl x safes so &&
 668        check_is_really_smaller_arg ((Some (name,(C.Def (so,None))))::context)
 669         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 670    | C.Appl (he::_) ->
 671       (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
 672       (*CSC: solo perche' non abbiamo trovato controesempi            *)
 673       check_is_really_smaller_arg context n nn kl x safes he
 674    | C.Appl [] -> raise (AssertFailure "11")
 675    | C.Const _
 676    | C.MutInd _ -> raise (AssertFailure "12")
 677    | C.MutConstruct _ -> false
 678    | C.MutCase (uri,i,outtype,term,pl) ->
 679       (match term with
 680           C.Rel m when List.mem m safes || m = x ->
 681            let (tys,len,isinductive,paramsno,cl) =
 682             match CicEnvironment.get_obj uri with
 683                C.InductiveDefinition (tl,_,paramsno) ->
 684                 let tys =
 685                  List.map
 686                   (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl
 687                 in
 688                  let (_,isinductive,_,cl) = List.nth tl i in
 689                   let cl' =
 690                    List.map
 691                     (fun (id,ty) ->
 692                       (id, snd (split_prods tys paramsno ty))) cl
 693                   in
 694                    (tys,List.length tl,isinductive,paramsno,cl')
 695              | _ ->
 696                 raise (TypeCheckerFailure
 697                   ("Unknown mutual inductive definition:" ^
 698                   UriManager.string_of_uri uri))
 699            in
 700             if not isinductive then
 701               List.fold_right
 702                (fun p i ->
 703                  i && check_is_really_smaller_arg context n nn kl x safes p)
 704                pl true
 705             else
 706               List.fold_right
 707                (fun (p,(_,c)) i ->
 708                  let rl' =
 709                   let debrujinedte = debrujin_constructor uri len c in
 710                    recursive_args tys 0 len debrujinedte
 711                  in
 712                   let (e,safes',n',nn',x',context') =
 713                    get_new_safes context p c rl' safes n nn x
 714                   in
 715                    i &&
 716                    check_is_really_smaller_arg context' n' nn' kl x' safes' e
 717                ) (List.combine pl cl) true
 718         | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
 719            let (tys,len,isinductive,paramsno,cl) =
 720             match CicEnvironment.get_obj uri with
 721                C.InductiveDefinition (tl,_,paramsno) ->
 722                 let (_,isinductive,_,cl) = List.nth tl i in
 723                  let tys =
 724                   List.map (fun (n,_,ty,_) ->
 725                    Some(Cic.Name n,(Cic.Decl ty))) tl
 726                  in
 727                   let cl' =
 728                    List.map
 729                     (fun (id,ty) ->
 730                       (id, snd (split_prods tys paramsno ty))) cl
 731                   in
 732                    (tys,List.length tl,isinductive,paramsno,cl')
 733              | _ ->
 734                 raise (TypeCheckerFailure
 735                   ("Unknown mutual inductive definition:" ^
 736                   UriManager.string_of_uri uri))
 737            in
 738             if not isinductive then
 739               List.fold_right
 740                (fun p i ->
 741                  i && check_is_really_smaller_arg context n nn kl x safes p)
 742                pl true
 743             else
 744               (*CSC: supponiamo come prima che nessun controllo sia necessario*)
 745               (*CSC: sugli argomenti di una applicazione                      *)
 746               List.fold_right
 747                (fun (p,(_,c)) i ->
 748                  let rl' =
 749                   let debrujinedte = debrujin_constructor uri len c in
 750                    recursive_args tys 0 len debrujinedte
 751                  in
 752                   let (e, safes',n',nn',x',context') =
 753                    get_new_safes context p c rl' safes n nn x
 754                   in
 755                    i &&
 756                    check_is_really_smaller_arg context' n' nn' kl x' safes' e
 757                ) (List.combine pl cl) true
 758         | _ ->
 759           List.fold_right
 760            (fun p i ->
 761              i && check_is_really_smaller_arg context n nn kl x safes p
 762            ) pl true
 763       )
 764    | C.Fix (_, fl) ->
 765       let len = List.length fl in
 766        let n_plus_len = n + len
 767        and nn_plus_len = nn + len
 768        and x_plus_len = x + len
 769        and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
 770        and safes' = List.map (fun x -> x + len) safes in
 771         List.fold_right
 772          (fun (_,_,ty,bo) i ->
 773            i &&
 774             check_is_really_smaller_arg (tys@context) n_plus_len nn_plus_len kl
 775              x_plus_len safes' bo
 776          ) fl true
 777    | C.CoFix (_, fl) ->
 778       let len = List.length fl in
 779        let n_plus_len = n + len
 780        and nn_plus_len = nn + len
 781        and x_plus_len = x + len
 782        and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
 783        and safes' = List.map (fun x -> x + len) safes in
 784         List.fold_right
 785          (fun (_,ty,bo) i ->
 786            i &&
 787             check_is_really_smaller_arg (tys@context) n_plus_len nn_plus_len kl
 788              x_plus_len safes' bo
 789          ) fl true
 790
 791 and guarded_by_destructors context n nn kl x safes =
 792  let module C = Cic in
 793  let module U = UriManager in
 794   function
 795      C.Rel m when m > n && m <= nn -> false
 796    | C.Rel m ->
 797       (match List.nth context (n-1) with
 798           Some (_,C.Decl _) -> true
 799         | Some (_,C.Def (bo,_)) ->
 800            guarded_by_destructors context m nn kl x safes
 801             (CicSubstitution.lift m bo)
 802         | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
 803       )
 804    | C.Meta _
 805    | C.Sort _
 806    | C.Implicit _ -> true
 807    | C.Cast (te,ty) ->
 808       guarded_by_destructors context n nn kl x safes te &&
 809        guarded_by_destructors context n nn kl x safes ty
 810    | C.Prod (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.Lambda (name,so,ta) ->
 815       guarded_by_destructors context n nn kl x safes so &&
 816        guarded_by_destructors ((Some (name,(C.Decl so)))::context)
 817         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 818    | C.LetIn (name,so,ta) ->
 819       guarded_by_destructors context n nn kl x safes so &&
 820        guarded_by_destructors ((Some (name,(C.Def (so,None))))::context)
 821         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 822    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
 823       let k = List.nth kl (m - n - 1) in
 824        if not (List.length tl > k) then false
 825        else
 826         List.fold_right
 827          (fun param i ->
 828            i && guarded_by_destructors context n nn kl x safes param
 829          ) tl true &&
 830          check_is_really_smaller_arg context n nn kl x safes (List.nth tl k)
 831    | C.Appl tl ->
 832       List.fold_right
 833        (fun t i -> i && guarded_by_destructors context n nn kl x safes t)
 834        tl true
 835    | C.Var (_,exp_named_subst)
 836    | C.Const (_,exp_named_subst)
 837    | C.MutInd (_,_,exp_named_subst)
 838    | C.MutConstruct (_,_,_,exp_named_subst) ->
 839       List.fold_right
 840        (fun (_,t) i -> i && guarded_by_destructors context n nn kl x safes t)
 841        exp_named_subst true
 842    | C.MutCase (uri,i,outtype,term,pl) ->
 843       (match term with
 844           C.Rel m when List.mem m safes || m = x ->
 845            let (tys,len,isinductive,paramsno,cl) =
 846             match CicEnvironment.get_obj uri with
 847                C.InductiveDefinition (tl,_,paramsno) ->
 848                 let len = List.length tl in
 849                  let (_,isinductive,_,cl) = List.nth tl i in
 850                   let tys =
 851                    List.map (fun (n,_,ty,_) ->
 852                     Some(Cic.Name n,(Cic.Decl ty))) tl
 853                   in
 854                    let cl' =
 855                     List.map
 856                      (fun (id,ty) ->
 857                       let debrujinedty = debrujin_constructor uri len ty in
 858                        (id, snd (split_prods tys paramsno ty),
 859                         snd (split_prods tys paramsno debrujinedty)
 860                        )) cl
 861                    in
 862                     (tys,len,isinductive,paramsno,cl')
 863              | _ ->
 864                 raise (TypeCheckerFailure
 865                   ("Unknown mutual inductive definition:" ^
 866                   UriManager.string_of_uri uri))
 867            in
 868             if not isinductive then
 869              guarded_by_destructors context n nn kl x safes outtype &&
 870               guarded_by_destructors context n nn kl x safes term &&
 871               (*CSC: manca ??? il controllo sul tipo di term? *)
 872               List.fold_right
 873                (fun p i ->
 874                  i && guarded_by_destructors context n nn kl x safes p)
 875                pl true
 876             else
 877              guarded_by_destructors context n nn kl x safes outtype &&
 878               (*CSC: manca ??? il controllo sul tipo di term? *)
 879               List.fold_right
 880                (fun (p,(_,c,brujinedc)) i ->
 881                  let rl' = recursive_args tys 0 len brujinedc in
 882                   let (e,safes',n',nn',x',context') =
 883                    get_new_safes context p c rl' safes n nn x
 884                   in
 885                    i &&
 886                    guarded_by_destructors context' n' nn' kl x' safes' e
 887                ) (List.combine pl cl) true
 888         | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
 889            let (tys,len,isinductive,paramsno,cl) =
 890             match CicEnvironment.get_obj uri with
 891                C.InductiveDefinition (tl,_,paramsno) ->
 892                 let (_,isinductive,_,cl) = List.nth tl i in
 893                  let tys =
 894                   List.map
 895                    (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
 896                  in
 897                   let cl' =
 898                    List.map
 899                     (fun (id,ty) ->
 900                       (id, snd (split_prods tys paramsno ty))) cl
 901                   in
 902                    (tys,List.length tl,isinductive,paramsno,cl')
 903              | _ ->
 904                 raise (TypeCheckerFailure
 905                   ("Unknown mutual inductive definition:" ^
 906                   UriManager.string_of_uri uri))
 907            in
 908             if not isinductive then
 909              guarded_by_destructors context n nn kl x safes outtype &&
 910               guarded_by_destructors context n nn kl x safes term &&
 911               (*CSC: manca ??? il controllo sul tipo di term? *)
 912               List.fold_right
 913                (fun p i ->
 914                  i && guarded_by_destructors context n nn kl x safes p)
 915                pl true
 916             else
 917              guarded_by_destructors context n nn kl x safes outtype &&
 918               (*CSC: manca ??? il controllo sul tipo di term? *)
 919               List.fold_right
 920                (fun t i ->
 921                  i && guarded_by_destructors context n nn kl x safes t)
 922                tl true &&
 923               List.fold_right
 924                (fun (p,(_,c)) i ->
 925                  let rl' =
 926                   let debrujinedte = debrujin_constructor uri len c in
 927                    recursive_args tys 0 len debrujinedte
 928                  in
 929                   let (e, safes',n',nn',x',context') =
 930                    get_new_safes context p c rl' safes n nn x
 931                   in
 932                    i &&
 933                    guarded_by_destructors context' n' nn' kl x' safes' e
 934                ) (List.combine pl cl) true
 935         | _ ->
 936           guarded_by_destructors context n nn kl x safes outtype &&
 937            guarded_by_destructors context n nn kl x safes term &&
 938            (*CSC: manca ??? il controllo sul tipo di term? *)
 939            List.fold_right
 940             (fun p i -> i && guarded_by_destructors context n nn kl x safes p)
 941             pl true
 942       )
 943    | C.Fix (_, fl) ->
 944       let len = List.length fl in
 945        let n_plus_len = n + len
 946        and nn_plus_len = nn + len
 947        and x_plus_len = x + len
 948        and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
 949        and safes' = List.map (fun x -> x + len) safes in
 950         List.fold_right
 951          (fun (_,_,ty,bo) i ->
 952            i && guarded_by_destructors context n nn kl x_plus_len safes' ty &&
 953             guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
 954              x_plus_len safes' bo
 955          ) fl true
 956    | C.CoFix (_, fl) ->
 957       let len = List.length fl in
 958        let n_plus_len = n + len
 959        and nn_plus_len = nn + len
 960        and x_plus_len = x + len
 961        and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
 962        and safes' = List.map (fun x -> x + len) safes in
 963         List.fold_right
 964          (fun (_,ty,bo) i ->
 965            i &&
 966             guarded_by_destructors context n nn kl x_plus_len safes' ty &&
 967             guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
 968              x_plus_len safes' bo
 969          ) fl true
 970
 971 (* the boolean h means already protected *)
 972 (* args is the list of arguments the type of the constructor that may be *)
 973 (* found in head position must be applied to.                            *)
 974 (*CSC: coInductiveTypeURI non cambia mai di ricorsione in ricorsione *)
 975 and guarded_by_constructors context n nn h te args coInductiveTypeURI =
 976  let module C = Cic in
 977   (*CSC: There is a lot of code replication between the cases X and    *)
 978   (*CSC: (C.Appl X tl). Maybe it will be better to define a function   *)
 979   (*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *)
 980   match CicReduction.whd context te with
 981      C.Rel m when m > n && m <= nn -> h
 982    | C.Rel _ -> true
 983    | C.Meta _
 984    | C.Sort _
 985    | C.Implicit _
 986    | C.Cast _
 987    | C.Prod _
 988    | C.LetIn _ ->
 989       (* the term has just been type-checked *)
 990       raise (AssertFailure "17")
 991    | C.Lambda (name,so,de) ->
 992       does_not_occur context n nn so &&
 993        guarded_by_constructors ((Some (name,(C.Decl so)))::context)
 994         (n + 1) (nn + 1) h de args coInductiveTypeURI
 995    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
 996       h &&
 997        List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
 998    | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) ->
 999       let consty =
1000        match CicEnvironment.get_cooked_obj ~trust:false uri with
1001           C.InductiveDefinition (itl,_,_) ->
1002            let (_,_,_,cl) = List.nth itl i in
1003             let (_,cons) = List.nth cl (j - 1) in
1004              CicSubstitution.subst_vars exp_named_subst cons
1005         | _ ->
1006             raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1007               UriManager.string_of_uri uri))
1008       in
1009        let rec analyse_branch context ty te =
1010         match CicReduction.whd context ty with
1011            C.Meta _ -> raise (AssertFailure "34")
1012          | C.Rel _
1013          | C.Var _
1014          | C.Sort _ ->
1015             does_not_occur context n nn te
1016          | C.Implicit _
1017          | C.Cast _ ->
1018             raise (AssertFailure "24")(* due to type-checking *)
1019          | C.Prod (name,so,de) ->
1020             analyse_branch ((Some (name,(C.Decl so)))::context) de te
1021          | C.Lambda _
1022          | C.LetIn _ ->
1023             raise (AssertFailure "25")(* due to type-checking *)
1024          | C.Appl ((C.MutInd (uri,_,_))::_) as ty
1025             when uri == coInductiveTypeURI ->
1026              guarded_by_constructors context n nn true te [] coInductiveTypeURI
1027          | C.Appl ((C.MutInd (uri,_,_))::_) as ty ->
1028             guarded_by_constructors context n nn true te tl coInductiveTypeURI
1029          | C.Appl _ ->
1030             does_not_occur context n nn te
1031          | C.Const _ -> raise (AssertFailure "26")
1032          | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
1033             guarded_by_constructors context n nn true te [] coInductiveTypeURI
1034          | C.MutInd _ ->
1035             does_not_occur context n nn te
1036          | C.MutConstruct _ -> raise (AssertFailure "27")
1037          (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
1038          (*CSC: in head position.                                       *)
1039          | C.MutCase _
1040          | C.Fix _
1041          | C.CoFix _ ->
1042             raise (AssertFailure "28")(* due to type-checking *)
1043        in
1044        let rec analyse_instantiated_type context ty l =
1045         match CicReduction.whd context ty with
1046            C.Rel _
1047          | C.Var _
1048          | C.Meta _
1049          | C.Sort _
1050          | C.Implicit _
1051          | C.Cast _ -> raise (AssertFailure "29")(* due to type-checking *)
1052          | C.Prod (name,so,de) ->
1053             begin
1054              match l with
1055                 [] -> true
1056               | he::tl ->
1057                  analyse_branch context so he &&
1058                   analyse_instantiated_type
1059                    ((Some (name,(C.Decl so)))::context) de tl
1060             end
1061          | C.Lambda _
1062          | C.LetIn _ ->
1063             raise (AssertFailure "30")(* due to type-checking *)
1064          | C.Appl _ ->
1065             List.fold_left
1066              (fun i x -> i && does_not_occur context n nn x) true l
1067          | C.Const _ -> raise (AssertFailure "31")
1068          | C.MutInd _ ->
1069             List.fold_left
1070              (fun i x -> i && does_not_occur context n nn x) true l
1071          | C.MutConstruct _ -> raise (AssertFailure "32")
1072          (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
1073          (*CSC: in head position.                                       *)
1074          | C.MutCase _
1075          | C.Fix _
1076          | C.CoFix _ ->
1077             raise (AssertFailure "33")(* due to type-checking *)
1078        in
1079         let rec instantiate_type args consty =
1080          function
1081             [] -> true
1082           | tlhe::tltl as l ->
1083              let consty' = CicReduction.whd context consty in
1084               match args with
1085                  he::tl ->
1086                   begin
1087                    match consty' with
1088                       C.Prod (_,_,de) ->
1089                        let instantiated_de = CicSubstitution.subst he de in
1090                         (*CSC: siamo sicuri che non sia troppo forte? *)
1091                         does_not_occur context n nn tlhe &
1092                          instantiate_type tl instantiated_de tltl
1093                     | _ ->
1094                       (*CSC:We do not consider backbones with a MutCase, a    *)
1095                       (*CSC:FixPoint, a CoFixPoint and so on in head position.*)
1096                       raise (AssertFailure "23")
1097                   end
1098                | [] -> analyse_instantiated_type context consty' l
1099                   (* These are all the other cases *)
1100        in
1101         instantiate_type args consty tl
1102    | C.Appl ((C.CoFix (_,fl))::tl) ->
1103       List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
1104        let len = List.length fl in
1105         let n_plus_len = n + len
1106         and nn_plus_len = nn + len
1107         (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1108         and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1109          List.fold_right
1110           (fun (_,ty,bo) i ->
1111             i && does_not_occur context n nn ty &&
1112              guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1113               args coInductiveTypeURI
1114           ) fl true
1115    | C.Appl ((C.MutCase (_,_,out,te,pl))::tl) ->
1116        List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
1117         does_not_occur context n nn out &&
1118          does_not_occur context n nn te &&
1119           List.fold_right
1120            (fun x i ->
1121              i &&
1122              guarded_by_constructors context n nn h x args coInductiveTypeURI
1123            ) pl true
1124    | C.Appl l ->
1125       List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
1126    | C.Var (_,exp_named_subst)
1127    | C.Const (_,exp_named_subst) ->
1128       List.fold_right
1129        (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
1130    | C.MutInd _ -> assert false
1131    | C.MutConstruct (_,_,_,exp_named_subst) ->
1132       List.fold_right
1133        (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
1134    | C.MutCase (_,_,out,te,pl) ->
1135        does_not_occur context n nn out &&
1136         does_not_occur context n nn te &&
1137          List.fold_right
1138           (fun x i ->
1139             i &&
1140              guarded_by_constructors context n nn h x args coInductiveTypeURI
1141           ) pl true
1142    | C.Fix (_,fl) ->
1143       let len = List.length fl in
1144        let n_plus_len = n + len
1145        and nn_plus_len = nn + len
1146        (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1147        and tys = List.map (fun (n,_,ty,_)-> Some (C.Name n,(C.Decl ty))) fl in
1148         List.fold_right
1149          (fun (_,_,ty,bo) i ->
1150            i && does_not_occur context n nn ty &&
1151             does_not_occur (tys@context) n_plus_len nn_plus_len bo
1152          ) fl true
1153    | C.CoFix (_,fl) ->
1154       let len = List.length fl in
1155        let n_plus_len = n + len
1156        and nn_plus_len = nn + len
1157        (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1158        and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1159         List.fold_right
1160          (fun (_,ty,bo) i ->
1161            i && does_not_occur context n nn ty &&
1162             guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1163              args coInductiveTypeURI
1164          ) fl true
1165
1166 and check_allowed_sort_elimination context uri i need_dummy ind arity1 arity2 =
1167  let module C = Cic in
1168  let module U = UriManager in
1169   match (CicReduction.whd context arity1, CicReduction.whd context arity2) with
1170      (C.Prod (_,so1,de1), C.Prod (_,so2,de2))
1171       when CicReduction.are_convertible context so1 so2 ->
1172        check_allowed_sort_elimination context uri i need_dummy
1173         (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2
1174    | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true
1175    | (C.Sort C.Prop, C.Sort C.Set)
1176    | (C.Sort C.Prop, C.Sort C.CProp)
1177    | (C.Sort C.Prop, C.Sort (C.Type _) ) when need_dummy ->
1178    (* TASSI: da verificare *)
1179 (*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *)
1180        (match CicEnvironment.get_obj uri with
1181            C.InductiveDefinition (itl,_,_) ->
1182             let (_,_,_,cl) = List.nth itl i in
1183              (* is a singleton definition or the empty proposition? *)
1184              List.length cl = 1 || List.length cl = 0
1185          | _ ->
1186             raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1187               UriManager.string_of_uri uri))
1188        )
1189    | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true
1190    | (C.Sort C.CProp, C.Sort C.Prop) when need_dummy -> true
1191    | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true
1192    | (C.Sort C.Set, C.Sort C.CProp) when need_dummy -> true
1193    | (C.Sort C.CProp, C.Sort C.Set) when need_dummy -> true
1194    | (C.Sort C.CProp, C.Sort C.CProp) when need_dummy -> true
1195    | ((C.Sort C.Set, C.Sort (C.Type _)) | (C.Sort C.CProp, C.Sort (C.Type _)))
1196       (* TASSI: da verificare *)
1197       when need_dummy ->
1198        (match CicEnvironment.get_obj uri with
1199            C.InductiveDefinition (itl,_,paramsno) ->
1200             let tys =
1201              List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1202             in
1203              let (_,_,_,cl) = List.nth itl i in
1204               List.fold_right
1205                (fun (_,x) i -> i && is_small tys paramsno x) cl true
1206          | _ ->
1207             raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1208               UriManager.string_of_uri uri))
1209        )
1210    | (C.Sort (C.Type _), C.Sort _) when need_dummy -> true
1211      (* TASSI: da verificare *)
1212    | (C.Sort C.Prop, C.Prod (name,so,ta)) when not need_dummy ->
1213        let res = CicReduction.are_convertible context so ind
1214        in
1215         res &&
1216         (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1217             C.Sort C.Prop -> true
1218           | (C.Sort C.Set | C.Sort C.CProp) ->
1219              (match CicEnvironment.get_obj uri with
1220                  C.InductiveDefinition (itl,_,_) ->
1221                   let (_,_,_,cl) = List.nth itl i in
1222                    (* is a singleton definition? *)
1223                    List.length cl = 1
1224                | _ ->
1225                   raise (TypeCheckerFailure
1226                     ("Unknown mutual inductive definition:" ^
1227                     UriManager.string_of_uri uri))
1228              )
1229           | _ -> false
1230         )
1231    | ((C.Sort C.Set, C.Prod (name,so,ta)) | (C.Sort C.CProp, C.Prod (name,so,ta)))
1232       when not need_dummy ->
1233        let res = CicReduction.are_convertible context so ind
1234        in
1235         res &&
1236         (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1237             C.Sort C.Prop
1238           | C.Sort C.Set  -> true
1239           | C.Sort C.CProp -> true
1240           | C.Sort (C.Type _) ->
1241             (* TASSI: da verificare *)
1242              (match CicEnvironment.get_obj uri with
1243                  C.InductiveDefinition (itl,_,paramsno) ->
1244                   let (_,_,_,cl) = List.nth itl i in
1245                    let tys =
1246                     List.map
1247                      (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1248                    in
1249                     List.fold_right
1250                      (fun (_,x) i -> i && is_small tys paramsno x) cl true
1251                | _ ->
1252                   raise (TypeCheckerFailure
1253                     ("Unknown mutual inductive definition:" ^
1254                     UriManager.string_of_uri uri))
1255              )
1256           | _ -> raise (AssertFailure "19")
1257         )
1258    | (C.Sort (C.Type _), C.Prod (_,so,_)) when not need_dummy ->
1259      (* TASSI: da verificare *)
1260        CicReduction.are_convertible context so ind
1261    | (_,_) -> false
1262
1263 and type_of_branch context argsno need_dummy outtype term constype =
1264  let module C = Cic in
1265  let module R = CicReduction in
1266   match R.whd context constype with
1267      C.MutInd (_,_,_) ->
1268       if need_dummy then
1269        outtype
1270       else
1271        C.Appl [outtype ; term]
1272    | C.Appl (C.MutInd (_,_,_)::tl) ->
1273       let (_,arguments) = split tl argsno
1274       in
1275        if need_dummy && arguments = [] then
1276         outtype
1277        else
1278         C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
1279    | C.Prod (name,so,de) ->
1280       let term' =
1281        match CicSubstitution.lift 1 term with
1282           C.Appl l -> C.Appl (l@[C.Rel 1])
1283         | t -> C.Appl [t ; C.Rel 1]
1284       in
1285        C.Prod (C.Anonymous,so,type_of_branch
1286         ((Some (name,(C.Decl so)))::context) argsno need_dummy
1287         (CicSubstitution.lift 1 outtype) term' de)
1288   | _ -> raise (AssertFailure "20")
1289
1290 (* check_metasenv_consistency checks that the "canonical" context of a
1291 metavariable is consitent - up to relocation via the relocation list l -
1292 with the actual context *)
1293
1294 and check_metasenv_consistency metasenv context canonical_context l =
1295   let module C = Cic in
1296   let module R = CicReduction in
1297   let module S = CicSubstitution in
1298    let lifted_canonical_context =
1299     let rec aux i =
1300      function
1301         [] -> []
1302       | (Some (n,C.Decl t))::tl ->
1303          (Some (n,C.Decl (S.lift_meta l (S.lift i t))))::(aux (i+1) tl)
1304       | (Some (n,C.Def (t,None)))::tl ->
1305          (Some (n,C.Def ((S.lift_meta l (S.lift i t)),None)))::(aux (i+1) tl)
1306       | None::tl -> None::(aux (i+1) tl)
1307       | (Some (n,C.Def (t,Some ty)))::tl ->
1308          (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)
1309     in
1310      aux 1 canonical_context
1311    in
1312     List.iter2
1313      (fun t ct ->
1314         match (t,ct) with
1315          | _,None -> ()
1316          | Some t,Some (_,C.Def (ct,_)) ->
1317             if not (R.are_convertible context t ct) then
1318               raise (TypeCheckerFailure (sprintf
1319                 "Not well typed metavariable local context: expected a term convertible with %s, found %s"
1320                 (CicPp.ppterm ct) (CicPp.ppterm t)))
1321          | Some t,Some (_,C.Decl ct) ->
1322              let type_t = type_of_aux' metasenv context t in
1323              if not (R.are_convertible context type_t ct) then
1324               raise (TypeCheckerFailure (sprintf
1325                 "Not well typed metavariable local context: expected a term of type %s, found %s of type %s"
1326                 (CicPp.ppterm ct) (CicPp.ppterm t) (CicPp.ppterm type_t)))
1327          | None, _  ->
1328              raise (TypeCheckerFailure
1329               "Not well typed metavariable local context: an hypothesis, that is not hidden, is not instantiated")
1330      ) l lifted_canonical_context
1331
1332 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
1333 and type_of_aux' metasenv context t =
1334  let rec type_of_aux context =
1335   let module C = Cic in
1336   let module R = CicReduction in
1337   let module S = CicSubstitution in
1338   let module U = UriManager in
1339    function
1340       C.Rel n ->
1341        (try
1342          match List.nth context (n - 1) with
1343             Some (_,C.Decl t) -> S.lift n t
1344           | Some (_,C.Def (_,Some ty)) -> S.lift n ty
1345           | Some (_,C.Def (bo,None)) ->
1346              debug_print "##### CASO DA INVESTIGARE E CAPIRE" ;
1347              type_of_aux context (S.lift n bo)
1348           | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
1349         with
1350         _ ->
1351           raise (TypeCheckerFailure "unbound variable")
1352        )
1353     | C.Var (uri,exp_named_subst) ->
1354       incr fdebug ;
1355       check_exp_named_subst context exp_named_subst ;
1356       let ty =
1357        CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
1358       in
1359        decr fdebug ;
1360        ty
1361     | C.Meta (n,l) ->
1362        let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
1363         check_metasenv_consistency metasenv context canonical_context l;
1364         CicSubstitution.lift_meta l ty
1365       (* TASSI: CONSTRAINTS *)
1366     | C.Sort (C.Type t) ->
1367        let t' = CicUniv.fresh() in
1368         if not (CicUniv.add_gt t' t ) then
1369           assert false (* t' is fresh! an error in CicUniv *)
1370         else
1371           C.Sort (C.Type t')
1372       (* TASSI: CONSTRAINTS *)
1373     | C.Sort s -> C.Sort (C.Type (CicUniv.fresh ()))
1374     | C.Implicit _ -> raise (AssertFailure "21")
1375     | C.Cast (te,ty) as t ->
1376        let _ = type_of_aux context ty in
1377         if R.are_convertible context (type_of_aux context te) ty then
1378           ty
1379         else
1380           raise (TypeCheckerFailure
1381             (sprintf "Invalid cast %s" (CicPp.ppterm t)))
1382     | C.Prod (name,s,t) ->
1383        let sort1 = type_of_aux context s
1384        and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t in
1385         sort_of_prod context (name,s) (sort1,sort2)
1386    | C.Lambda (n,s,t) ->
1387        let sort1 = type_of_aux context s in
1388        (match R.whd context sort1 with
1389            C.Meta _
1390          | C.Sort _ -> ()
1391          | _ ->
1392            raise
1393             (TypeCheckerFailure (sprintf
1394               "Not well-typed lambda-abstraction: the source %s should be a
1395                type; instead it is a term of type %s" (CicPp.ppterm s)
1396                 (CicPp.ppterm sort1)))
1397        ) ;
1398        let type2 = type_of_aux ((Some (n,(C.Decl s)))::context) t in
1399         C.Prod (n,s,type2)
1400    | C.LetIn (n,s,t) ->
1401       (* only to check if s is well-typed *)
1402       let ty = type_of_aux context s in
1403        (* The type of a LetIn is a LetIn. Extremely slow since the computed
1404           LetIn is later reduced and maybe also re-checked.
1405        (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t))
1406        *)
1407        (* The type of the LetIn is reduced. Much faster than the previous
1408           solution. Moreover the inferred type is probably very different
1409           from the expected one.
1410        (CicReduction.whd context
1411         (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)))
1412        *)
1413        (* One-step LetIn reduction. Even faster than the previous solution.
1414           Moreover the inferred type is closer to the expected one. *)
1415        (CicSubstitution.subst s
1416         (type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t))
1417    | C.Appl (he::tl) when List.length tl > 0 ->
1418       let hetype = type_of_aux context he
1419       and tlbody_and_type = List.map (fun x -> (x, type_of_aux context x)) tl in
1420        eat_prods context hetype tlbody_and_type
1421    | C.Appl _ -> raise (AssertFailure "Appl: no arguments")
1422    | C.Const (uri,exp_named_subst) ->
1423       incr fdebug ;
1424       check_exp_named_subst context exp_named_subst ;
1425       let cty =
1426        CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
1427       in
1428        decr fdebug ;
1429        cty
1430    | C.MutInd (uri,i,exp_named_subst) ->
1431       incr fdebug ;
1432       check_exp_named_subst context exp_named_subst ;
1433       let cty =
1434        CicSubstitution.subst_vars exp_named_subst
1435         (type_of_mutual_inductive_defs uri i)
1436       in
1437        decr fdebug ;
1438        cty
1439    | C.MutConstruct (uri,i,j,exp_named_subst) ->
1440       check_exp_named_subst context exp_named_subst ;
1441       let cty =
1442        CicSubstitution.subst_vars exp_named_subst
1443         (type_of_mutual_inductive_constr uri i j)
1444       in
1445        cty
1446    | C.MutCase (uri,i,outtype,term,pl) ->
1447       let outsort = type_of_aux context outtype in
1448       let (need_dummy, k) =
1449        let rec guess_args context t =
1450          let outtype = CicReduction.whd context t in
1451          match outtype with
1452            C.Sort _ -> (true, 0)
1453          | C.Prod (name, s, t) ->
1454             let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
1455              if n = 0 then
1456               (* last prod before sort *)
1457               match CicReduction.whd context s with
1458 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1459                  C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
1460                   (false, 1)
1461 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1462                | C.Appl ((C.MutInd (uri',i',_)) :: _)
1463                   when U.eq uri' uri && i' = i -> (false, 1)
1464                | _ -> (true, 1)
1465              else
1466               (b, n + 1)
1467          | _ ->
1468              raise (TypeCheckerFailure (sprintf
1469               "Malformed case analasys' output type %s" (CicPp.ppterm outtype)))
1470        in
1471         (*CSC whd non serve dopo type_of_aux ? *)
1472         let (b, k) = guess_args context outsort in
1473          if not b then (b, k - 1) else (b, k)
1474       in
1475       let (parameters, arguments, exp_named_subst) =
1476         match R.whd context (type_of_aux context term) with
1477            (*CSC manca il caso dei CAST *)
1478 (*CSC: ma servono i parametri (uri,i)? Se si', perche' non serve anche il *)
1479 (*CSC: parametro exp_named_subst? Se no, perche' non li togliamo?         *)
1480 (*CSC: Hint: nella DTD servono per gli stylesheet.                        *)
1481            C.MutInd (uri',i',exp_named_subst) as typ ->
1482             if U.eq uri uri' && i = i' then ([],[],exp_named_subst)
1483             else raise (TypeCheckerFailure (sprintf
1484               "Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}"
1485               (CicPp.ppterm typ) (U.string_of_uri uri) i))
1486          | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
1487             if U.eq uri uri' && i = i' then
1488              let params,args =
1489               split tl (List.length tl - k)
1490              in params,args,exp_named_subst
1491             else raise (TypeCheckerFailure (sprintf
1492               "Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}"
1493               (CicPp.ppterm typ') (U.string_of_uri uri) i))
1494          | _ ->
1495              raise (TypeCheckerFailure (sprintf
1496                "Case analysis: analysed term %s is not an inductive one"
1497                 (CicPp.ppterm term)))
1498       in
1499        (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
1500        let sort_of_ind_type =
1501         if parameters = [] then
1502          C.MutInd (uri,i,exp_named_subst)
1503         else
1504          C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters)
1505        in
1506         if not (check_allowed_sort_elimination context uri i need_dummy
1507          sort_of_ind_type (type_of_aux context sort_of_ind_type) outsort)
1508         then
1509          raise
1510           (TypeCheckerFailure ("Case analasys: sort elimination not allowed"));
1511         (* let's check if the type of branches are right *)
1512         let parsno =
1513          match CicEnvironment.get_cooked_obj ~trust:false uri with
1514             C.InductiveDefinition (_,_,parsno) -> parsno
1515           | _ ->
1516               raise (TypeCheckerFailure
1517                 ("Unknown mutual inductive definition:" ^
1518                 UriManager.string_of_uri uri))
1519         in
1520          let (_,branches_ok) =
1521           List.fold_left
1522            (fun (j,b) p ->
1523              let cons =
1524               if parameters = [] then
1525                (C.MutConstruct (uri,i,j,exp_named_subst))
1526               else
1527                (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
1528              in
1529 (*
1530               (j + 1, b &&
1531 *)
1532               (j + 1,
1533 let res = b &&
1534                R.are_convertible context (type_of_aux context p)
1535                 (type_of_branch context parsno need_dummy outtype cons
1536                   (type_of_aux context cons))
1537 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
1538               )
1539            ) (1,true) pl
1540          in
1541           if not branches_ok then
1542            raise
1543             (TypeCheckerFailure "Case analysys: wrong branch type");
1544           if not need_dummy then
1545            C.Appl ((outtype::arguments)@[term])
1546           else if arguments = [] then
1547            outtype
1548           else
1549            C.Appl (outtype::arguments)
1550    | C.Fix (i,fl) ->
1551       let types_times_kl =
1552        List.rev
1553         (List.map
1554           (fun (n,k,ty,_) ->
1555             let _ = type_of_aux context ty in
1556              (Some (C.Name n,(C.Decl ty)),k)) fl)
1557       in
1558       let (types,kl) = List.split types_times_kl in
1559        let len = List.length types in
1560         List.iter
1561          (fun (name,x,ty,bo) ->
1562            if
1563             (R.are_convertible (types@context) (type_of_aux (types@context) bo)
1564              (CicSubstitution.lift len ty))
1565            then
1566             begin
1567              let (m, eaten, context') =
1568               eat_lambdas (types @ context) (x + 1) bo
1569              in
1570               (*let's control the guarded by destructors conditions D{f,k,x,M}*)
1571               if
1572                not
1573                 (guarded_by_destructors context' eaten (len + eaten) kl 1 [] m)
1574               then
1575                raise
1576                 (TypeCheckerFailure ("Fix: not guarded by destructors"))
1577             end
1578            else
1579             raise (TypeCheckerFailure ("Fix: ill-typed bodies"))
1580          ) fl ;
1581
1582         (*CSC: controlli mancanti solo su D{f,k,x,M} *)
1583         let (_,_,ty,_) = List.nth fl i in
1584         ty
1585    | C.CoFix (i,fl) ->
1586       let types =
1587        List.rev
1588         (List.map
1589           (fun (n,ty,_) ->
1590             let _ = type_of_aux context ty in Some (C.Name n,(C.Decl ty))) fl)
1591       in
1592        let len = List.length types in
1593         List.iter
1594          (fun (_,ty,bo) ->
1595            if
1596             (R.are_convertible (types @ context)
1597              (type_of_aux (types @ context) bo) (CicSubstitution.lift len ty))
1598            then
1599             begin
1600              (* let's control that the returned type is coinductive *)
1601              match returns_a_coinductive context ty with
1602                 None ->
1603                  raise
1604                   (TypeCheckerFailure
1605                     ("CoFix: does not return a coinductive type"))
1606               | Some uri ->
1607                  (*let's control the guarded by constructors conditions C{f,M}*)
1608                  if
1609                   not
1610                    (guarded_by_constructors (types @ context) 0 len false bo
1611                      [] uri)
1612                  then
1613                   raise
1614                    (TypeCheckerFailure ("CoFix: not guarded by constructors"))
1615             end
1616            else
1617             raise
1618              (TypeCheckerFailure ("CoFix: ill-typed bodies"))
1619          ) fl ;
1620
1621         let (_,ty,_) = List.nth fl i in
1622          ty
1623
1624  and check_exp_named_subst context =
1625   let rec check_exp_named_subst_aux substs =
1626    function
1627       [] -> ()
1628     | ((uri,t) as subst)::tl ->
1629        let typeofvar =
1630         CicSubstitution.subst_vars substs (type_of_variable uri) in
1631        (match CicEnvironment.get_cooked_obj ~trust:false uri with
1632            Cic.Variable (_,Some bo,_,_) ->
1633             raise
1634              (TypeCheckerFailure
1635                ("A variable with a body can not be explicit substituted"))
1636          | Cic.Variable (_,None,_,_) -> ()
1637          | _ ->
1638             raise (TypeCheckerFailure
1639               ("Unknown variable definition:" ^
1640               UriManager.string_of_uri uri))
1641        ) ;
1642        let typeoft = type_of_aux context t in
1643         if CicReduction.are_convertible context typeoft typeofvar then
1644          check_exp_named_subst_aux (substs@[subst]) tl
1645         else
1646          begin
1647           CicReduction.fdebug := 0 ;
1648           ignore (CicReduction.are_convertible context typeoft typeofvar) ;
1649           fdebug := 0 ;
1650           debug typeoft [typeofvar] ;
1651           raise (TypeCheckerFailure "Wrong Explicit Named Substitution")
1652          end
1653   in
1654    check_exp_named_subst_aux []
1655
1656  and sort_of_prod context (name,s) (t1, t2) =
1657   let module C = Cic in
1658    let t1' = CicReduction.whd context t1 in
1659    let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
1660    match (t1', t2') with
1661       (C.Sort s1, C.Sort s2)
1662         when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1663          (* different from Coq manual!!! *)
1664          C.Sort s2
1665     | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1666       (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
1667        let t' = CicUniv.fresh() in
1668        if not (CicUniv.add_ge t' t1) || not (CicUniv.add_ge t' t2) then
1669          assert false ; (* not possible, error in CicUniv *)
1670        C.Sort (C.Type t')
1671     | (C.Sort _,C.Sort (C.Type t1)) ->
1672         (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
1673         C.Sort (C.Type t1) (* c'e' bisogno di un fresh? *)
1674     | (C.Meta _, C.Sort _) -> t2'
1675     | (C.Meta _, (C.Meta (_,_) as t))
1676     | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
1677         t2'
1678     | (_,_) -> raise (TypeCheckerFailure (sprintf
1679         "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1')
1680           (CicPp.ppterm t2')))
1681
1682  and eat_prods context hetype =
1683   (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
1684   (*CSC: cucinati                                                         *)
1685   function
1686      [] -> hetype
1687    | (hete, hety)::tl ->
1688     (match (CicReduction.whd context hetype) with
1689         Cic.Prod (n,s,t) ->
1690          if CicReduction.are_convertible context hety s then
1691           (CicReduction.fdebug := -1 ;
1692            eat_prods context (CicSubstitution.subst hete t) tl
1693           )
1694          else
1695           begin
1696            CicReduction.fdebug := 0 ;
1697            ignore (CicReduction.are_convertible context s hety) ;
1698            fdebug := 0 ;
1699            debug s [hety] ;
1700            raise (TypeCheckerFailure (sprintf
1701             "Appl: wrong parameter-type, expected %s, found %s"
1702             (CicPp.ppterm hetype) (CicPp.ppterm s)))
1703           end
1704       | _ ->
1705           raise (TypeCheckerFailure
1706             "Appl: this is not a function, it cannot be applied")
1707     )
1708
1709  and returns_a_coinductive context ty =
1710   let module C = Cic in
1711    match CicReduction.whd context ty with
1712       C.MutInd (uri,i,_) ->
1713        (*CSC: definire una funzioncina per questo codice sempre replicato *)
1714        (match CicEnvironment.get_cooked_obj ~trust:false uri with
1715            C.InductiveDefinition (itl,_,_) ->
1716             let (_,is_inductive,_,_) = List.nth itl i in
1717              if is_inductive then None else (Some uri)
1718          | _ ->
1719             raise (TypeCheckerFailure
1720               ("Unknown mutual inductive definition:" ^
1721               UriManager.string_of_uri uri))
1722         )
1723     | C.Appl ((C.MutInd (uri,i,_))::_) ->
1724        (match CicEnvironment.get_obj uri with
1725            C.InductiveDefinition (itl,_,_) ->
1726             let (_,is_inductive,_,_) = List.nth itl i in
1727              if is_inductive then None else (Some uri)
1728          | _ ->
1729             raise (TypeCheckerFailure
1730               ("Unknown mutual inductive definition:" ^
1731               UriManager.string_of_uri uri))
1732         )
1733     | C.Prod (n,so,de) ->
1734        returns_a_coinductive ((Some (n,C.Decl so))::context) de
1735     | _ -> None
1736
1737  in
1738 (*CSC
1739 debug_print ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t) ; flush stderr ;
1740 let res =
1741 *)
1742   type_of_aux context t
1743 (*
1744 in debug_print "FINE TYPE_OF_AUX" ; flush stderr ; res
1745 *)
1746
1747 (* is a small constructor? *)
1748 (*CSC: ottimizzare calcolando staticamente *)
1749 and is_small context paramsno c =
1750  let rec is_small_aux context c =
1751   let module C = Cic in
1752    match CicReduction.whd context c with
1753       C.Prod (n,so,de) ->
1754        (*CSC: [] is an empty metasenv. Is it correct? *)
1755        let s = type_of_aux' [] context so in
1756         (s = C.Sort C.Prop || s = C.Sort C.Set || s = C.Sort C.CProp) &&
1757         is_small_aux ((Some (n,(C.Decl so)))::context) de
1758     | _ -> true (*CSC: we trust the type-checker *)
1759  in
1760   let (context',dx) = split_prods context paramsno c in
1761    is_small_aux context' dx
1762
1763 and type_of t =
1764 (*CSC
1765 debug_print ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t) ; flush stderr ;
1766 let res =
1767 *)
1768  type_of_aux' [] [] t
1769 (*CSC
1770 in debug_print "FINE TYPE_OF_AUX'" ; flush stderr ; res
1771 *)
1772 ;;
1773
1774 let typecheck uri =
1775  let module C = Cic in
1776  let module R = CicReduction in
1777  let module U = UriManager in
1778   match CicEnvironment.is_type_checked ~trust:false uri with
1779      CicEnvironment.CheckedObj _ -> ()
1780    | CicEnvironment.UncheckedObj uobj ->
1781       (* let's typecheck the uncooked object *)
1782       CicLogger.log (`Start_type_checking uri) ;
1783       (match uobj with
1784           C.Constant (_,Some te,ty,_) ->
1785            let _ = type_of ty in
1786             if not (R.are_convertible [] (type_of te ) ty) then
1787               raise (TypeCheckerFailure
1788                 ("Unknown constant:" ^ U.string_of_uri uri))
1789         | C.Constant (_,None,ty,_) ->
1790           (* only to check that ty is well-typed *)
1791           let _ = type_of ty in ()
1792         | C.CurrentProof (_,conjs,te,ty,_) ->
1793            let _ =
1794             List.fold_left
1795              (fun metasenv ((_,context,ty) as conj) ->
1796                ignore (type_of_aux' metasenv context ty) ;
1797                metasenv @ [conj]
1798              ) [] conjs
1799            in
1800             let _ = type_of_aux' conjs [] ty in
1801             let type_of_te = type_of_aux' conjs [] te in
1802              if not (R.are_convertible [] type_of_te ty)
1803              then
1804                raise (TypeCheckerFailure (sprintf
1805                 "the current proof %s is not well typed because the type %s of the body is not convertible to the declared type %s"
1806                 (U.string_of_uri uri) (CicPp.ppterm type_of_te)
1807                 (CicPp.ppterm ty)))
1808         | C.Variable (_,bo,ty,_) ->
1809            (* only to check that ty is well-typed *)
1810            let _ = type_of ty in
1811             (match bo with
1812                 None -> ()
1813               | Some bo ->
1814                  if not (R.are_convertible [] (type_of bo) ty) then
1815                   raise (TypeCheckerFailure
1816                     ("Unknown variable:" ^ U.string_of_uri uri))
1817             )
1818         | C.InductiveDefinition _ ->
1819            check_mutual_inductive_defs uri uobj
1820       ) ;
1821       CicEnvironment.set_type_checking_info uri ;
1822       CicLogger.log (`Type_checking_completed uri)
1823 ;;