helm/software/components/ng_kernel/nCicTypeChecker.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 (* $Id: nCicReduction.ml 8250 2008-03-25 17:56:20Z tassi $ *)
  13
  14 exception TypeCheckerFailure of string Lazy.t
  15 exception AssertFailure of string Lazy.t
  16
  17 (* $Id: cicTypeChecker.ml 8213 2008-03-13 18:48:26Z sacerdot $ *)
  18
  19 (*
  20 let debrujin_constructor ?(cb=fun _ _ -> ()) uri number_of_types =
  21  let rec aux k t =
  22   let module C = Cic in
  23   let res =
  24    match t with
  25       C.Rel n as t when n <= k -> t
  26     | C.Rel _ ->
  27         raise (TypeCheckerFailure (lazy "unbound variable found in constructor type"))
  28     | C.Var (uri,exp_named_subst) ->
  29        let exp_named_subst' =
  30         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
  31        in
  32         C.Var (uri,exp_named_subst')
  33     | C.Meta (i,l) ->
  34        let l' = List.map (function None -> None | Some t -> Some (aux k t)) l in
  35         C.Meta (i,l')
  36     | C.Sort _
  37     | C.Implicit _ as t -> t
  38     | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
  39     | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k+1) t)
  40     | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k+1) t)
  41     | C.LetIn (n,s,ty,t) -> C.LetIn (n, aux k s, aux k ty, aux (k+1) t)
  42     | C.Appl l -> C.Appl (List.map (aux k) l)
  43     | C.Const (uri,exp_named_subst) ->
  44        let exp_named_subst' =
  45         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
  46        in
  47         C.Const (uri,exp_named_subst')
  48     | C.MutInd (uri',tyno,exp_named_subst) when UriManager.eq uri uri' ->
  49        if exp_named_subst != [] then
  50         raise (TypeCheckerFailure
  51           (lazy ("non-empty explicit named substitution is applied to "^
  52            "a mutual inductive type which is being defined"))) ;
  53        C.Rel (k + number_of_types - tyno) ;
  54     | C.MutInd (uri',tyno,exp_named_subst) ->
  55        let exp_named_subst' =
  56         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
  57        in
  58         C.MutInd (uri',tyno,exp_named_subst')
  59     | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
  60        let exp_named_subst' =
  61         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
  62        in
  63         C.MutConstruct (uri,tyno,consno,exp_named_subst')
  64     | C.MutCase (sp,i,outty,t,pl) ->
  65        C.MutCase (sp, i, aux k outty, aux k t,
  66         List.map (aux k) pl)
  67     | C.Fix (i, fl) ->
  68        let len = List.length fl in
  69        let liftedfl =
  70         List.map
  71          (fun (name, i, ty, bo) -> (name, i, aux k ty, aux (k+len) bo))
  72           fl
  73        in
  74         C.Fix (i, liftedfl)
  75     | C.CoFix (i, fl) ->
  76        let len = List.length fl in
  77        let liftedfl =
  78         List.map
  79          (fun (name, ty, bo) -> (name, aux k ty, aux (k+len) bo))
  80           fl
  81        in
  82         C.CoFix (i, liftedfl)
  83   in
  84    cb t res;
  85    res
  86  in
  87   aux 0
  88 ;;
  89
  90 exception CicEnvironmentError;;
  91
  92 let rec type_of_constant ~logger uri ugraph =
  93  let module C = Cic in
  94  let module R = CicReduction in
  95  let module U = UriManager in
  96  let cobj,ugraph =
  97    match CicEnvironment.is_type_checked ~trust:true ugraph uri with
  98       CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
  99     | CicEnvironment.UncheckedObj uobj ->
 100        logger#log (`Start_type_checking uri) ;
 101        (* let's typecheck the uncooked obj *)
 102
 103 (****************************************************************
 104   TASSI: FIXME qui e' inutile ricordarselo,
 105   tanto poi lo richiediamo alla cache che da quello su disco
 106 *****************************************************************)
 107
 108        let ugraph_dust =
 109          (match uobj with
 110            C.Constant (_,Some te,ty,_,_) ->
 111            let _,ugraph = type_of ~logger ty ugraph in
 112            let type_of_te,ugraph' = type_of ~logger te ugraph in
 113               let b',ugraph'' = (R.are_convertible [] type_of_te ty ugraph') in
 114               if not b' then
 115                raise (TypeCheckerFailure (lazy (sprintf
 116                 "the constant %s is not well typed because the type %s of the body is not convertible to the declared type %s"
 117                 (U.string_of_uri uri) (CicPp.ppterm type_of_te)
 118                 (CicPp.ppterm ty))))
 119               else
 120                 ugraph'
 121          | C.Constant (_,None,ty,_,_) ->
 122            (* only to check that ty is well-typed *)
 123            let _,ugraph' = type_of ~logger ty ugraph in
 124            ugraph'
 125          | C.CurrentProof (_,conjs,te,ty,_,_) ->
 126              let _,ugraph1 =
 127               List.fold_left
 128                (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
 129                  let _,ugraph' =
 130                    type_of_aux' ~logger metasenv context ty ugraph
 131                  in
 132                  (metasenv @ [conj],ugraph')
 133                ) ([],ugraph) conjs
 134              in
 135               let _,ugraph2 = type_of_aux' ~logger conjs [] ty ugraph1 in
 136                let type_of_te,ugraph3 =
 137                  type_of_aux' ~logger conjs [] te ugraph2
 138                in
 139                let b,ugraph4 = (R.are_convertible [] type_of_te ty ugraph3) in
 140                if not b then
 141                  raise (TypeCheckerFailure (lazy (sprintf
 142                   "the current proof %s is not well typed because the type %s of the body is not convertible to the declared type %s"
 143                   (U.string_of_uri uri) (CicPp.ppterm type_of_te)
 144                   (CicPp.ppterm ty))))
 145                else
 146                  ugraph4
 147          | _ ->
 148              raise
 149               (TypeCheckerFailure (lazy ("Unknown constant:" ^ U.string_of_uri uri))))
 150        in
 151          try
 152            CicEnvironment.set_type_checking_info uri;
 153            logger#log (`Type_checking_completed uri) ;
 154            match CicEnvironment.is_type_checked ~trust:false ugraph uri with
 155                CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
 156              | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
 157          with Invalid_argument s ->
 158            (*debug_print (lazy s);*)
 159            uobj,ugraph_dust
 160   in
 161    match cobj,ugraph with
 162       (C.Constant (_,_,ty,_,_)),g -> ty,g
 163     | (C.CurrentProof (_,_,_,ty,_,_)),g -> ty,g
 164     | _ ->
 165         raise (TypeCheckerFailure (lazy ("Unknown constant:" ^ U.string_of_uri uri)))
 166
 167 and type_of_variable ~logger uri ugraph =
 168  let module C = Cic in
 169  let module R = CicReduction in
 170  let module U = UriManager in
 171   (* 0 because a variable is never cooked => no partial cooking at one level *)
 172   match CicEnvironment.is_type_checked ~trust:true ugraph uri with
 173      CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') -> ty,ugraph'
 174    | CicEnvironment.UncheckedObj (C.Variable (_,bo,ty,_,_)) ->
 175       logger#log (`Start_type_checking uri) ;
 176       (* only to check that ty is well-typed *)
 177       let _,ugraph1 = type_of ~logger ty ugraph in
 178       let ugraph2 =
 179        (match bo with
 180            None -> ugraph
 181          | Some bo ->
 182              let ty_bo,ugraph' = type_of ~logger bo ugraph1 in
 183              let b,ugraph'' = (R.are_convertible [] ty_bo ty ugraph') in
 184              if not b then
 185               raise (TypeCheckerFailure
 186                 (lazy ("Unknown variable:" ^ U.string_of_uri uri)))
 187              else
 188                ugraph'')
 189       in
 190         (try
 191            CicEnvironment.set_type_checking_info uri ;
 192            logger#log (`Type_checking_completed uri) ;
 193            match CicEnvironment.is_type_checked ~trust:false ugraph uri with
 194                CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') ->
 195                  ty,ugraph'
 196              | CicEnvironment.CheckedObj _
 197              | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
 198          with Invalid_argument s ->
 199            (*debug_print (lazy s);*)
 200            ty,ugraph2)
 201    |  _ ->
 202         raise (TypeCheckerFailure (lazy ("Unknown variable:" ^ U.string_of_uri uri)))
 203
 204 and does_not_occur ?(subst=[]) context n nn te =
 205  let module C = Cic in
 206    match te with
 207       C.Rel m when m > n && m <= nn -> false
 208     | C.Rel m ->
 209        (try
 210          (match List.nth context (m-1) with
 211              Some (_,C.Def (bo,_)) ->
 212               does_not_occur ~subst context n nn (CicSubstitution.lift m bo)
 213            | _ -> true)
 214         with
 215          Failure _ -> assert false)
 216     | C.Sort _
 217     | C.Implicit _ -> true
 218     | C.Meta (_,l) ->
 219        List.fold_right
 220         (fun x i ->
 221           match x with
 222              None -> i
 223            | Some x -> i && does_not_occur ~subst context n nn x) l true &&
 224        (try
 225          let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in
 226           does_not_occur ~subst context n nn (CicSubstitution.subst_meta l term)
 227         with
 228          CicUtil.Subst_not_found _ -> true)
 229     | C.Cast (te,ty) ->
 230        does_not_occur ~subst context n nn te && does_not_occur ~subst context n nn ty
 231     | C.Prod (name,so,dest) ->
 232        does_not_occur ~subst context n nn so &&
 233         does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n + 1)
 234          (nn + 1) dest
 235     | C.Lambda (name,so,dest) ->
 236        does_not_occur ~subst context n nn so &&
 237         does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1)
 238          dest
 239     | C.LetIn (name,so,ty,dest) ->
 240        does_not_occur ~subst context n nn so &&
 241         does_not_occur ~subst context n nn ty &&
 242          does_not_occur ~subst ((Some (name,(C.Def (so,ty))))::context)
 243           (n + 1) (nn + 1) dest
 244     | C.Appl l ->
 245        List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) l true
 246     | C.Var (_,exp_named_subst)
 247     | C.Const (_,exp_named_subst)
 248     | C.MutInd (_,_,exp_named_subst)
 249     | C.MutConstruct (_,_,_,exp_named_subst) ->
 250        List.fold_right (fun (_,x) i -> i && does_not_occur ~subst context n nn x)
 251         exp_named_subst true
 252     | C.MutCase (_,_,out,te,pl) ->
 253        does_not_occur ~subst context n nn out && does_not_occur ~subst context n nn te &&
 254         List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) pl true
 255     | C.Fix (_,fl) ->
 256        let len = List.length fl in
 257         let n_plus_len = n + len in
 258         let nn_plus_len = nn + len in
 259         let tys,_ =
 260          List.fold_left
 261           (fun (types,len) (n,_,ty,_) ->
 262              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
 263               len+1)
 264           ) ([],0) fl
 265         in
 266          List.fold_right
 267           (fun (_,_,ty,bo) i ->
 268             i && does_not_occur ~subst context n nn ty &&
 269             does_not_occur ~subst (tys @ context) n_plus_len nn_plus_len bo
 270           ) fl true
 271     | C.CoFix (_,fl) ->
 272        let len = List.length fl in
 273         let n_plus_len = n + len in
 274         let nn_plus_len = nn + len in
 275         let tys,_ =
 276          List.fold_left
 277           (fun (types,len) (n,ty,_) ->
 278              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
 279               len+1)
 280           ) ([],0) fl
 281         in
 282          List.fold_right
 283           (fun (_,ty,bo) i ->
 284             i && does_not_occur ~subst context n nn ty &&
 285             does_not_occur ~subst (tys @ context) n_plus_len nn_plus_len bo
 286           ) fl true
 287
 288 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
 289 (*CSC questa funzione e' simile alla are_all_occurrences_positive, ma fa *)
 290 (*CSC dei controlli leggermente diversi. Viene invocata solamente dalla  *)
 291 (*CSC strictly_positive                                                  *)
 292 (*CSC definizione (giusta???) tratta dalla mail di Hugo ;-)              *)
 293 and weakly_positive context n nn uri te =
 294  let module C = Cic in
 295 (*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*)
 296   let dummy_mutind =
 297    C.MutInd (HelmLibraryObjects.Datatypes.nat_URI,0,[])
 298   in
 299   (*CSC: mettere in cicSubstitution *)
 300   let rec subst_inductive_type_with_dummy_mutind =
 301    function
 302       C.MutInd (uri',0,_) when UriManager.eq uri' uri ->
 303        dummy_mutind
 304     | C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri ->
 305        dummy_mutind
 306     | C.Cast (te,ty) -> subst_inductive_type_with_dummy_mutind te
 307     | C.Prod (name,so,ta) ->
 308        C.Prod (name, subst_inductive_type_with_dummy_mutind so,
 309         subst_inductive_type_with_dummy_mutind ta)
 310     | C.Lambda (name,so,ta) ->
 311        C.Lambda (name, subst_inductive_type_with_dummy_mutind so,
 312         subst_inductive_type_with_dummy_mutind ta)
 313     | C.Appl tl ->
 314        C.Appl (List.map subst_inductive_type_with_dummy_mutind tl)
 315     | C.MutCase (uri,i,outtype,term,pl) ->
 316        C.MutCase (uri,i,
 317         subst_inductive_type_with_dummy_mutind outtype,
 318         subst_inductive_type_with_dummy_mutind term,
 319         List.map subst_inductive_type_with_dummy_mutind pl)
 320     | C.Fix (i,fl) ->
 321        C.Fix (i,List.map (fun (name,i,ty,bo) -> (name,i,
 322         subst_inductive_type_with_dummy_mutind ty,
 323         subst_inductive_type_with_dummy_mutind bo)) fl)
 324     | C.CoFix (i,fl) ->
 325        C.CoFix (i,List.map (fun (name,ty,bo) -> (name,
 326         subst_inductive_type_with_dummy_mutind ty,
 327         subst_inductive_type_with_dummy_mutind bo)) fl)
 328     | C.Const (uri,exp_named_subst) ->
 329        let exp_named_subst' =
 330         List.map
 331          (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
 332          exp_named_subst
 333        in
 334         C.Const (uri,exp_named_subst')
 335     | C.MutInd (uri,typeno,exp_named_subst) ->
 336        let exp_named_subst' =
 337         List.map
 338          (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
 339          exp_named_subst
 340        in
 341         C.MutInd (uri,typeno,exp_named_subst')
 342     | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
 343        let exp_named_subst' =
 344         List.map
 345          (function (uri,t) -> (uri,subst_inductive_type_with_dummy_mutind t))
 346          exp_named_subst
 347        in
 348         C.MutConstruct (uri,typeno,consno,exp_named_subst')
 349     | t -> t
 350   in
 351   match CicReduction.whd context te with
 352 (*
 353      C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri -> true
 354 *)
 355      C.Appl ((C.MutInd (uri',_,_))::tl) when UriManager.eq uri' uri -> true
 356    | C.MutInd (uri',0,_) when UriManager.eq uri' uri -> true
 357    | C.Prod (C.Anonymous,source,dest) ->
 358       strictly_positive context n nn
 359        (subst_inductive_type_with_dummy_mutind source) &&
 360        weakly_positive ((Some (C.Anonymous,(C.Decl source)))::context)
 361         (n + 1) (nn + 1) uri dest
 362    | C.Prod (name,source,dest) when
 363       does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
 364        (* dummy abstraction, so we behave as in the anonimous case *)
 365        strictly_positive context n nn
 366         (subst_inductive_type_with_dummy_mutind source) &&
 367          weakly_positive ((Some (name,(C.Decl source)))::context)
 368          (n + 1) (nn + 1) uri dest
 369    | C.Prod (name,source,dest) ->
 370        does_not_occur context n nn
 371          (subst_inductive_type_with_dummy_mutind source)&&
 372          weakly_positive ((Some (name,(C.Decl source)))::context)
 373          (n + 1) (nn + 1) uri dest
 374    | _ ->
 375      raise (TypeCheckerFailure (lazy "Malformed inductive constructor type"))
 376
 377 (* instantiate_parameters ps (x1:T1)...(xn:Tn)C                             *)
 378 (* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *)
 379 and instantiate_parameters params c =
 380  let module C = Cic in
 381   match (c,params) with
 382      (c,[]) -> c
 383    | (C.Prod (_,_,ta), he::tl) ->
 384        instantiate_parameters tl
 385         (CicSubstitution.subst he ta)
 386    | (C.Cast (te,_), _) -> instantiate_parameters params te
 387    | (t,l) -> raise (AssertFailure (lazy "1"))
 388
 389 and strictly_positive context n nn te =
 390  let module C = Cic in
 391  let module U = UriManager in
 392   match CicReduction.whd context te with
 393    | t when does_not_occur context n nn t -> true
 394    | C.Rel _ -> true
 395    | C.Cast (te,ty) ->
 396       (*CSC: bisogna controllare ty????*)
 397       strictly_positive context n nn te
 398    | C.Prod (name,so,ta) ->
 399       does_not_occur context n nn so &&
 400        strictly_positive ((Some (name,(C.Decl so)))::context) (n+1) (nn+1) ta
 401    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
 402       List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
 403    | C.Appl ((C.MutInd (uri,i,exp_named_subst))::tl) ->
 404       let (ok,paramsno,ity,cl,name) =
 405         let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 406           match o with
 407               C.InductiveDefinition (tl,_,paramsno,_) ->
 408                 let (name,_,ity,cl) = List.nth tl i in
 409                 (List.length tl = 1, paramsno, ity, cl, name)
 410                 (* (true, paramsno, ity, cl, name) *)
 411             | _ ->
 412                 raise
 413                   (TypeCheckerFailure
 414                      (lazy ("Unknown inductive type:" ^ U.string_of_uri uri)))
 415       in
 416       let (params,arguments) = split tl paramsno in
 417       let lifted_params = List.map (CicSubstitution.lift 1) params in
 418       let cl' =
 419         List.map
 420           (fun (_,te) ->
 421              instantiate_parameters lifted_params
 422                (CicSubstitution.subst_vars exp_named_subst te)
 423           ) cl
 424       in
 425         ok &&
 426           List.fold_right
 427           (fun x i -> i && does_not_occur context n nn x)
 428           arguments true &&
 429          (*CSC: MEGAPATCH3 (sara' quella giusta?)*)
 430           List.fold_right
 431           (fun x i ->
 432              i &&
 433                weakly_positive
 434                ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri
 435                x
 436           ) cl' true
 437    | t -> false
 438
 439 (* the inductive type indexes are s.t. n < x <= nn *)
 440 and are_all_occurrences_positive context uri indparamsno i n nn te =
 441  let module C = Cic in
 442   match CicReduction.whd context te with
 443      C.Appl ((C.Rel m)::tl) when m = i ->
 444       (*CSC: riscrivere fermandosi a 0 *)
 445       (* let's check if the inductive type is applied at least to *)
 446       (* indparamsno parameters                                   *)
 447       let last =
 448        List.fold_left
 449         (fun k x ->
 450           if k = 0 then 0
 451           else
 452            match CicReduction.whd context x with
 453               C.Rel m when m = n - (indparamsno - k) -> k - 1
 454             | _ ->
 455               raise (TypeCheckerFailure
 456                (lazy
 457                ("Non-positive occurence in mutual inductive definition(s) [1]" ^
 458                 UriManager.string_of_uri uri)))
 459         ) indparamsno tl
 460       in
 461        if last = 0 then
 462         List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
 463        else
 464         raise (TypeCheckerFailure
 465          (lazy ("Non-positive occurence in mutual inductive definition(s) [2]"^
 466           UriManager.string_of_uri uri)))
 467    | C.Rel m when m = i ->
 468       if indparamsno = 0 then
 469        true
 470       else
 471         raise (TypeCheckerFailure
 472          (lazy ("Non-positive occurence in mutual inductive definition(s) [3]"^
 473           UriManager.string_of_uri uri)))
 474    | C.Prod (C.Anonymous,source,dest) ->
 475        let b = strictly_positive context n nn source in
 476        b &&
 477        are_all_occurrences_positive
 478         ((Some (C.Anonymous,(C.Decl source)))::context) uri indparamsno
 479         (i+1) (n + 1) (nn + 1) dest
 480    | C.Prod (name,source,dest) when
 481       does_not_occur ((Some (name,(C.Decl source)))::context) 0 n dest ->
 482       (* dummy abstraction, so we behave as in the anonimous case *)
 483       strictly_positive context n nn source &&
 484        are_all_occurrences_positive
 485         ((Some (name,(C.Decl source)))::context) uri indparamsno
 486         (i+1) (n + 1) (nn + 1) dest
 487    | C.Prod (name,source,dest) ->
 488       does_not_occur context n nn source &&
 489        are_all_occurrences_positive ((Some (name,(C.Decl source)))::context)
 490         uri indparamsno (i+1) (n + 1) (nn + 1) dest
 491    | _ ->
 492      raise
 493       (TypeCheckerFailure (lazy ("Malformed inductive constructor type " ^
 494         (UriManager.string_of_uri uri))))
 495
 496 (* Main function to checks the correctness of a mutual *)
 497 (* inductive block definition. This is the function    *)
 498 (* exported to the proof-engine.                       *)
 499 and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph =
 500  let module U = UriManager in
 501   (* let's check if the arity of the inductive types are well *)
 502   (* formed                                                   *)
 503   let ugrap1 = List.fold_left
 504    (fun ugraph (_,_,x,_) -> let _,ugraph' =
 505       type_of ~logger x ugraph in ugraph')
 506    ugraph itl in
 507
 508   (* let's check if the types of the inductive constructors  *)
 509   (* are well formed.                                        *)
 510   (* In order not to use type_of_aux we put the types of the *)
 511   (* mutual inductive types at the head of the types of the  *)
 512   (* constructors using Prods                                *)
 513   let len = List.length itl in
 514   let tys =
 515     List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in
 516   let _,ugraph2 =
 517     List.fold_right
 518       (fun (_,_,_,cl) (i,ugraph) ->
 519         let ugraph'' =
 520           List.fold_left
 521             (fun ugraph (name,te) ->
 522               let debrujinedte = debrujin_constructor uri len te in
 523               let augmented_term =
 524                 List.fold_right
 525                   (fun (name,_,ty,_) i -> Cic.Prod (Cic.Name name, ty, i))
 526                   itl debrujinedte
 527               in
 528               let _,ugraph' = type_of ~logger augmented_term ugraph in
 529               (* let's check also the positivity conditions *)
 530               if
 531                 not
 532                   (are_all_occurrences_positive tys uri indparamsno i 0 len
 533                      debrujinedte)
 534               then
 535                 begin
 536                 prerr_endline (UriManager.string_of_uri uri);
 537                 prerr_endline (string_of_int (List.length tys));
 538                 raise
 539                   (TypeCheckerFailure
 540                     (lazy ("Non positive occurence in " ^ U.string_of_uri uri)))                end
 541               else
 542                 ugraph'
 543             ) ugraph cl in
 544         (i + 1),ugraph''
 545       ) itl (1,ugrap1)
 546   in
 547   ugraph2
 548
 549 (* Main function to checks the correctness of a mutual *)
 550 (* inductive block definition.                         *)
 551 and check_mutual_inductive_defs uri obj ugraph =
 552   match obj with
 553       Cic.InductiveDefinition (itl, params, indparamsno, _) ->
 554         typecheck_mutual_inductive_defs uri (itl,params,indparamsno) ugraph
 555     | _ ->
 556         raise (TypeCheckerFailure (
 557                 lazy ("Unknown mutual inductive definition:" ^
 558                  UriManager.string_of_uri uri)))
 559
 560 and type_of_mutual_inductive_defs ~logger uri i ugraph =
 561  let module C = Cic in
 562  let module R = CicReduction in
 563  let module U = UriManager in
 564   let cobj,ugraph1 =
 565    match CicEnvironment.is_type_checked ~trust:true ugraph uri with
 566        CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
 567      | CicEnvironment.UncheckedObj uobj ->
 568          logger#log (`Start_type_checking uri) ;
 569          let ugraph1_dust =
 570            check_mutual_inductive_defs ~logger uri uobj ugraph
 571          in
 572            (* TASSI: FIXME: check ugraph1 == ugraph ritornato da env *)
 573            try
 574              CicEnvironment.set_type_checking_info uri ;
 575              logger#log (`Type_checking_completed uri) ;
 576              (match CicEnvironment.is_type_checked ~trust:false ugraph uri with
 577                   CicEnvironment.CheckedObj (cobj,ugraph') -> (cobj,ugraph')
 578                 | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
 579              )
 580            with
 581                Invalid_argument s ->
 582                  (*debug_print (lazy s);*)
 583                  uobj,ugraph1_dust
 584   in
 585     match cobj with
 586         C.InductiveDefinition (dl,_,_,_) ->
 587           let (_,_,arity,_) = List.nth dl i in
 588             arity,ugraph1
 589       | _ ->
 590           raise (TypeCheckerFailure
 591            (lazy ("Unknown mutual inductive definition:" ^ U.string_of_uri uri)))
 592
 593 and type_of_mutual_inductive_constr ~logger uri i j ugraph =
 594  let module C = Cic in
 595  let module R = CicReduction in
 596  let module U = UriManager in
 597   let cobj,ugraph1 =
 598     match CicEnvironment.is_type_checked ~trust:true ugraph uri with
 599         CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
 600       | CicEnvironment.UncheckedObj uobj ->
 601           logger#log (`Start_type_checking uri) ;
 602           let ugraph1_dust =
 603             check_mutual_inductive_defs ~logger uri uobj ugraph
 604           in
 605             (* check ugraph1 validity ??? == ugraph' *)
 606             try
 607               CicEnvironment.set_type_checking_info uri ;
 608               logger#log (`Type_checking_completed uri) ;
 609               (match
 610                  CicEnvironment.is_type_checked ~trust:false ugraph uri
 611                with
 612                  CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
 613                | CicEnvironment.UncheckedObj _ ->
 614                        raise CicEnvironmentError)
 615             with
 616                 Invalid_argument s ->
 617                   (*debug_print (lazy s);*)
 618                   uobj,ugraph1_dust
 619   in
 620     match cobj with
 621         C.InductiveDefinition (dl,_,_,_) ->
 622           let (_,_,_,cl) = List.nth dl i in
 623           let (_,ty) = List.nth cl (j-1) in
 624             ty,ugraph1
 625       | _ ->
 626           raise (TypeCheckerFailure
 627            (lazy ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri)))
 628
 629 and recursive_args context n nn te =
 630  let module C = Cic in
 631   match CicReduction.whd context te with
 632      C.Rel _ -> []
 633    | C.Var _
 634    | C.Meta _
 635    | C.Sort _
 636    | C.Implicit _
 637    | C.Cast _ (*CSC ??? *) ->
 638       raise (AssertFailure (lazy "3")) (* due to type-checking *)
 639    | C.Prod (name,so,de) ->
 640       (not (does_not_occur context n nn so)) ::
 641        (recursive_args ((Some (name,(C.Decl so)))::context) (n+1) (nn + 1) de)
 642    | C.Lambda _
 643    | C.LetIn _ ->
 644       raise (AssertFailure (lazy "4")) (* due to type-checking *)
 645    | C.Appl _ -> []
 646    | C.Const _ -> raise (AssertFailure (lazy "5"))
 647    | C.MutInd _
 648    | C.MutConstruct _
 649    | C.MutCase _
 650    | C.Fix _
 651    | C.CoFix _ -> raise (AssertFailure (lazy "6")) (* due to type-checking *)
 652
 653 and get_new_safes ~subst context p c rl safes n nn x =
 654  let module C = Cic in
 655  let module U = UriManager in
 656  let module R = CicReduction in
 657   match (R.whd ~subst context c, R.whd ~subst context p, rl) with
 658      (C.Prod (_,so,ta1), C.Lambda (name,_,ta2), b::tl) ->
 659        (* we are sure that the two sources are convertible because we *)
 660        (* have just checked this. So let's go along ...               *)
 661        let safes' =
 662         List.map (fun x -> x + 1) safes
 663        in
 664         let safes'' =
 665          if b then 1::safes' else safes'
 666         in
 667          get_new_safes ~subst ((Some (name,(C.Decl so)))::context)
 668           ta2 ta1 tl safes'' (n+1) (nn+1) (x+1)
 669    | (C.Prod _, (C.MutConstruct _ as e), _)
 670    | (C.Prod _, (C.Rel _ as e), _)
 671    | (C.MutInd _, e, [])
 672    | (C.Appl _, e, []) -> (e,safes,n,nn,x,context)
 673    | (c,p,l) ->
 674       (* CSC: If the next exception is raised, it just means that   *)
 675       (* CSC: the proof-assistant allows to use very strange things *)
 676       (* CSC: as a branch of a case whose type is a Prod. In        *)
 677       (* CSC: particular, this means that a new (C.Prod, x,_) case  *)
 678       (* CSC: must be considered in this match. (e.g. x = MutCase)  *)
 679       raise
 680        (AssertFailure (lazy
 681          (Printf.sprintf "Get New Safes: c=%s ; p=%s"
 682            (CicPp.ppterm c) (CicPp.ppterm p))))
 683
 684 and split_prods ~subst context n te =
 685  let module C = Cic in
 686  let module R = CicReduction in
 687   match (n, R.whd ~subst context te) with
 688      (0, _) -> context,te
 689    | (n, C.Prod (name,so,ta)) when n > 0 ->
 690        split_prods ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta
 691    | (_, _) -> raise (AssertFailure (lazy "8"))
 692
 693 and eat_lambdas ~subst context n te =
 694  let module C = Cic in
 695  let module R = CicReduction in
 696   match (n, R.whd ~subst context te) with
 697      (0, _) -> (te, 0, context)
 698    | (n, C.Lambda (name,so,ta)) when n > 0 ->
 699       let (te, k, context') =
 700        eat_lambdas ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta
 701       in
 702        (te, k + 1, context')
 703    | (n, te) ->
 704        raise (AssertFailure (lazy (sprintf "9 (%d, %s)" n (CicPp.ppterm te))))
 705
 706 (*CSC: Tutto quello che segue e' l'intuzione di luca ;-) *)
 707 and check_is_really_smaller_arg ~subst context n nn kl x safes te =
 708  (*CSC: forse la whd si puo' fare solo quando serve veramente. *)
 709  (*CSC: cfr guarded_by_destructors                             *)
 710  let module C = Cic in
 711  let module U = UriManager in
 712  match CicReduction.whd ~subst context te with
 713      C.Rel m when List.mem m safes -> true
 714    | C.Rel _ -> false
 715    | C.Var _
 716    | C.Meta _
 717    | C.Sort _
 718    | C.Implicit _
 719    | C.Cast _
 720 (*   | C.Cast (te,ty) ->
 721       check_is_really_smaller_arg ~subst n nn kl x safes te &&
 722        check_is_really_smaller_arg ~subst n nn kl x safes ty*)
 723 (*   | C.Prod (_,so,ta) ->
 724       check_is_really_smaller_arg ~subst n nn kl x safes so &&
 725        check_is_really_smaller_arg ~subst (n+1) (nn+1) kl (x+1)
 726         (List.map (fun x -> x + 1) safes) ta*)
 727    | C.Prod _ -> raise (AssertFailure (lazy "10"))
 728    | C.Lambda (name,so,ta) ->
 729       check_is_really_smaller_arg ~subst context n nn kl x safes so &&
 730        check_is_really_smaller_arg ~subst ((Some (name,(C.Decl so)))::context)
 731         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 732    | C.LetIn (name,so,ty,ta) ->
 733       check_is_really_smaller_arg ~subst context n nn kl x safes so &&
 734        check_is_really_smaller_arg ~subst context n nn kl x safes ty &&
 735         check_is_really_smaller_arg ~subst ((Some (name,(C.Def (so,ty))))::context)
 736         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 737    | C.Appl (he::_) ->
 738       (*CSC: sulla coda ci vogliono dei controlli? secondo noi no, ma *)
 739       (*CSC: solo perche' non abbiamo trovato controesempi            *)
 740       check_is_really_smaller_arg ~subst context n nn kl x safes he
 741    | C.Appl [] -> raise (AssertFailure (lazy "11"))
 742    | C.Const _
 743    | C.MutInd _ -> raise (AssertFailure (lazy "12"))
 744    | C.MutConstruct _ -> false
 745    | C.MutCase (uri,i,outtype,term,pl) ->
 746       (match term with
 747           C.Rel m when List.mem m safes || m = x ->
 748            let (lefts_and_tys,len,isinductive,paramsno,cl) =
 749             let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 750             match o with
 751                C.InductiveDefinition (tl,_,paramsno,_) ->
 752                 let tys =
 753                  List.map
 754                   (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) tl
 755                 in
 756                  let (_,isinductive,_,cl) = List.nth tl i in
 757                   let cl' =
 758                    List.map
 759                     (fun (id,ty) ->
 760                       (id, snd (split_prods ~subst tys paramsno ty))) cl in
 761                   let lefts =
 762                    match tl with
 763                       [] -> assert false
 764                     | (_,_,ty,_)::_ ->
 765                        fst (split_prods ~subst [] paramsno ty)
 766                   in
 767                    (tys@lefts,List.length tl,isinductive,paramsno,cl')
 768              | _ ->
 769                 raise (TypeCheckerFailure
 770                   (lazy ("Unknown mutual inductive definition:" ^
 771                   UriManager.string_of_uri uri)))
 772            in
 773             if not isinductive then
 774               List.fold_right
 775                (fun p i ->
 776                  i && check_is_really_smaller_arg ~subst context n nn kl x safes p)
 777                pl true
 778             else
 779              let pl_and_cl =
 780               try
 781                List.combine pl cl
 782               with
 783                Invalid_argument _ ->
 784                 raise (TypeCheckerFailure (lazy "not enough patterns"))
 785              in
 786               List.fold_right
 787                (fun (p,(_,c)) i ->
 788                  let rl' =
 789                   let debrujinedte = debrujin_constructor uri len c in
 790                    recursive_args lefts_and_tys 0 len debrujinedte
 791                  in
 792                   let (e,safes',n',nn',x',context') =
 793                    get_new_safes ~subst context p c rl' safes n nn x
 794                   in
 795                    i &&
 796                    check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
 797                ) pl_and_cl true
 798         | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
 799            let (lefts_and_tys,len,isinductive,paramsno,cl) =
 800             let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 801             match o with
 802                C.InductiveDefinition (tl,_,paramsno,_) ->
 803                 let (_,isinductive,_,cl) = List.nth tl i in
 804                  let tys =
 805                   List.map (fun (n,_,ty,_) ->
 806                    Some(Cic.Name n,(Cic.Decl ty))) tl
 807                  in
 808                   let cl' =
 809                    List.map
 810                     (fun (id,ty) ->
 811                       (id, snd (split_prods ~subst tys paramsno ty))) cl in
 812                   let lefts =
 813                    match tl with
 814                       [] -> assert false
 815                     | (_,_,ty,_)::_ ->
 816                        fst (split_prods ~subst [] paramsno ty)
 817                   in
 818                    (tys@lefts,List.length tl,isinductive,paramsno,cl')
 819              | _ ->
 820                 raise (TypeCheckerFailure
 821                   (lazy ("Unknown mutual inductive definition:" ^
 822                   UriManager.string_of_uri uri)))
 823            in
 824             if not isinductive then
 825               List.fold_right
 826                (fun p i ->
 827                  i && check_is_really_smaller_arg ~subst context n nn kl x safes p)
 828                pl true
 829             else
 830              let pl_and_cl =
 831               try
 832                List.combine pl cl
 833               with
 834                Invalid_argument _ ->
 835                 raise (TypeCheckerFailure (lazy "not enough patterns"))
 836              in
 837               (*CSC: supponiamo come prima che nessun controllo sia necessario*)
 838               (*CSC: sugli argomenti di una applicazione                      *)
 839               List.fold_right
 840                (fun (p,(_,c)) i ->
 841                  let rl' =
 842                   let debrujinedte = debrujin_constructor uri len c in
 843                    recursive_args lefts_and_tys 0 len debrujinedte
 844                  in
 845                   let (e, safes',n',nn',x',context') =
 846                    get_new_safes ~subst context p c rl' safes n nn x
 847                   in
 848                    i &&
 849                    check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
 850                ) pl_and_cl true
 851         | _ ->
 852           List.fold_right
 853            (fun p i ->
 854              i && check_is_really_smaller_arg ~subst context n nn kl x safes p
 855            ) pl true
 856       )
 857    | C.Fix (_, fl) ->
 858       let len = List.length fl in
 859        let n_plus_len = n + len
 860        and nn_plus_len = nn + len
 861        and x_plus_len = x + len
 862        and tys,_ =
 863         List.fold_left
 864           (fun (types,len) (n,_,ty,_) ->
 865              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
 866               len+1)
 867           ) ([],0) fl
 868        and safes' = List.map (fun x -> x + len) safes in
 869         List.fold_right
 870          (fun (_,_,ty,bo) i ->
 871            i &&
 872             check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl
 873              x_plus_len safes' bo
 874          ) fl true
 875    | C.CoFix (_, fl) ->
 876       let len = List.length fl in
 877        let n_plus_len = n + len
 878        and nn_plus_len = nn + len
 879        and x_plus_len = x + len
 880        and tys,_ =
 881         List.fold_left
 882           (fun (types,len) (n,ty,_) ->
 883              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
 884               len+1)
 885           ) ([],0) fl
 886        and safes' = List.map (fun x -> x + len) safes in
 887         List.fold_right
 888          (fun (_,ty,bo) i ->
 889            i &&
 890             check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl
 891              x_plus_len safes' bo
 892          ) fl true
 893
 894 and guarded_by_destructors ~subst context n nn kl x safes =
 895  let module C = Cic in
 896  let module U = UriManager in
 897   function
 898      C.Rel m when m > n && m <= nn -> false
 899    | C.Rel m ->
 900       (match List.nth context (n-1) with
 901           Some (_,C.Decl _) -> true
 902         | Some (_,C.Def (bo,_)) ->
 903            guarded_by_destructors ~subst context m nn kl x safes
 904             (CicSubstitution.lift m bo)
 905         | None -> raise (TypeCheckerFailure (lazy "Reference to deleted hypothesis"))
 906       )
 907    | C.Meta _
 908    | C.Sort _
 909    | C.Implicit _ -> true
 910    | C.Cast (te,ty) ->
 911       guarded_by_destructors ~subst context n nn kl x safes te &&
 912        guarded_by_destructors ~subst context n nn kl x safes ty
 913    | C.Prod (name,so,ta) ->
 914       guarded_by_destructors ~subst context n nn kl x safes so &&
 915        guarded_by_destructors ~subst ((Some (name,(C.Decl so)))::context)
 916         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 917    | C.Lambda (name,so,ta) ->
 918       guarded_by_destructors ~subst context n nn kl x safes so &&
 919        guarded_by_destructors ~subst ((Some (name,(C.Decl so)))::context)
 920         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 921    | C.LetIn (name,so,ty,ta) ->
 922       guarded_by_destructors ~subst context n nn kl x safes so &&
 923        guarded_by_destructors ~subst context n nn kl x safes ty &&
 924         guarded_by_destructors ~subst ((Some (name,(C.Def (so,ty))))::context)
 925          (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 926    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
 927       let k = List.nth kl (m - n - 1) in
 928        if not (List.length tl > k) then false
 929        else
 930         List.fold_right
 931          (fun param i ->
 932            i && guarded_by_destructors ~subst context n nn kl x safes param
 933          ) tl true &&
 934          check_is_really_smaller_arg ~subst context n nn kl x safes (List.nth tl k)
 935    | C.Appl tl ->
 936       List.fold_right
 937        (fun t i -> i && guarded_by_destructors ~subst context n nn kl x safes t)
 938        tl true
 939    | C.Var (_,exp_named_subst)
 940    | C.Const (_,exp_named_subst)
 941    | C.MutInd (_,_,exp_named_subst)
 942    | C.MutConstruct (_,_,_,exp_named_subst) ->
 943       List.fold_right
 944        (fun (_,t) i -> i && guarded_by_destructors ~subst context n nn kl x safes t)
 945        exp_named_subst true
 946    | C.MutCase (uri,i,outtype,term,pl) ->
 947       (match CicReduction.whd ~subst context term with
 948           C.Rel m when List.mem m safes || m = x ->
 949            let (lefts_and_tys,len,isinductive,paramsno,cl) =
 950             let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 951             match o with
 952                C.InductiveDefinition (tl,_,paramsno,_) ->
 953                 let len = List.length tl in
 954                  let (_,isinductive,_,cl) = List.nth tl i in
 955                   let tys =
 956                    List.map (fun (n,_,ty,_) ->
 957                     Some(Cic.Name n,(Cic.Decl ty))) tl
 958                   in
 959                    let cl' =
 960                     List.map
 961                      (fun (id,ty) ->
 962                       let debrujinedty = debrujin_constructor uri len ty in
 963                        (id, snd (split_prods ~subst tys paramsno ty),
 964                         snd (split_prods ~subst tys paramsno debrujinedty)
 965                        )) cl in
 966                    let lefts =
 967                     match tl with
 968                        [] -> assert false
 969                      | (_,_,ty,_)::_ ->
 970                         fst (split_prods ~subst [] paramsno ty)
 971                    in
 972                     (tys@lefts,len,isinductive,paramsno,cl')
 973              | _ ->
 974                 raise (TypeCheckerFailure
 975                   (lazy ("Unknown mutual inductive definition:" ^
 976                   UriManager.string_of_uri uri)))
 977            in
 978             if not isinductive then
 979              guarded_by_destructors ~subst context n nn kl x safes outtype &&
 980               guarded_by_destructors ~subst context n nn kl x safes term &&
 981               (*CSC: manca ??? il controllo sul tipo di term? *)
 982               List.fold_right
 983                (fun p i ->
 984                  i && guarded_by_destructors ~subst context n nn kl x safes p)
 985                pl true
 986             else
 987              let pl_and_cl =
 988               try
 989                List.combine pl cl
 990               with
 991                Invalid_argument _ ->
 992                 raise (TypeCheckerFailure (lazy "not enough patterns"))
 993              in
 994              guarded_by_destructors ~subst context n nn kl x safes outtype &&
 995               (*CSC: manca ??? il controllo sul tipo di term? *)
 996               List.fold_right
 997                (fun (p,(_,c,brujinedc)) i ->
 998                  let rl' = recursive_args lefts_and_tys 0 len brujinedc in
 999                   let (e,safes',n',nn',x',context') =
1000                    get_new_safes ~subst context p c rl' safes n nn x
1001                   in
1002                    i &&
1003                    guarded_by_destructors ~subst context' n' nn' kl x' safes' e
1004                ) pl_and_cl true
1005         | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
1006            let (lefts_and_tys,len,isinductive,paramsno,cl) =
1007             let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1008             match o with
1009                C.InductiveDefinition (tl,_,paramsno,_) ->
1010                 let (_,isinductive,_,cl) = List.nth tl i in
1011                  let tys =
1012                   List.map
1013                    (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
1014                  in
1015                   let cl' =
1016                    List.map
1017                     (fun (id,ty) ->
1018                       (id, snd (split_prods ~subst tys paramsno ty))) cl in
1019                   let lefts =
1020                    match tl with
1021                       [] -> assert false
1022                     | (_,_,ty,_)::_ ->
1023                        fst (split_prods ~subst [] paramsno ty)
1024                   in
1025                    (tys@lefts,List.length tl,isinductive,paramsno,cl')
1026              | _ ->
1027                 raise (TypeCheckerFailure
1028                   (lazy ("Unknown mutual inductive definition:" ^
1029                   UriManager.string_of_uri uri)))
1030            in
1031             if not isinductive then
1032              guarded_by_destructors ~subst context n nn kl x safes outtype &&
1033               guarded_by_destructors ~subst context n nn kl x safes term &&
1034               (*CSC: manca ??? il controllo sul tipo di term? *)
1035               List.fold_right
1036                (fun p i ->
1037                  i && guarded_by_destructors ~subst context n nn kl x safes p)
1038                pl true
1039             else
1040              let pl_and_cl =
1041               try
1042                List.combine pl cl
1043               with
1044                Invalid_argument _ ->
1045                 raise (TypeCheckerFailure (lazy "not enough patterns"))
1046              in
1047              guarded_by_destructors ~subst context n nn kl x safes outtype &&
1048               (*CSC: manca ??? il controllo sul tipo di term? *)
1049               List.fold_right
1050                (fun t i ->
1051                  i && guarded_by_destructors ~subst context n nn kl x safes t)
1052                tl true &&
1053               List.fold_right
1054                (fun (p,(_,c)) i ->
1055                  let rl' =
1056                   let debrujinedte = debrujin_constructor uri len c in
1057                    recursive_args lefts_and_tys 0 len debrujinedte
1058                  in
1059                   let (e, safes',n',nn',x',context') =
1060                    get_new_safes ~subst context p c rl' safes n nn x
1061                   in
1062                    i &&
1063                    guarded_by_destructors ~subst context' n' nn' kl x' safes' e
1064                ) pl_and_cl true
1065         | _ ->
1066           guarded_by_destructors ~subst context n nn kl x safes outtype &&
1067            guarded_by_destructors ~subst context n nn kl x safes term &&
1068            (*CSC: manca ??? il controllo sul tipo di term? *)
1069            List.fold_right
1070             (fun p i -> i && guarded_by_destructors ~subst context n nn kl x safes p)
1071             pl true
1072       )
1073    | C.Fix (_, fl) ->
1074       let len = List.length fl in
1075        let n_plus_len = n + len
1076        and nn_plus_len = nn + len
1077        and x_plus_len = x + len
1078        and tys,_ =
1079         List.fold_left
1080           (fun (types,len) (n,_,ty,_) ->
1081              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
1082               len+1)
1083           ) ([],0) fl
1084        and safes' = List.map (fun x -> x + len) safes in
1085         List.fold_right
1086          (fun (_,_,ty,bo) i ->
1087            i && guarded_by_destructors ~subst context n nn kl x_plus_len safes' ty &&
1088             guarded_by_destructors ~subst (tys@context) n_plus_len nn_plus_len kl
1089              x_plus_len safes' bo
1090          ) fl true
1091    | C.CoFix (_, fl) ->
1092       let len = List.length fl in
1093        let n_plus_len = n + len
1094        and nn_plus_len = nn + len
1095        and x_plus_len = x + len
1096        and tys,_ =
1097         List.fold_left
1098           (fun (types,len) (n,ty,_) ->
1099              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
1100               len+1)
1101           ) ([],0) fl
1102        and safes' = List.map (fun x -> x + len) safes in
1103         List.fold_right
1104          (fun (_,ty,bo) i ->
1105            i &&
1106             guarded_by_destructors ~subst context n nn kl x_plus_len safes' ty &&
1107             guarded_by_destructors ~subst (tys@context) n_plus_len nn_plus_len kl
1108              x_plus_len safes' bo
1109          ) fl true
1110
1111 (* the boolean h means already protected *)
1112 (* args is the list of arguments the type of the constructor that may be *)
1113 (* found in head position must be applied to.                            *)
1114 and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI =
1115  let module C = Cic in
1116   (*CSC: There is a lot of code replication between the cases X and    *)
1117   (*CSC: (C.Appl X tl). Maybe it will be better to define a function   *)
1118   (*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *)
1119   match CicReduction.whd ~subst context te with
1120      C.Rel m when m > n && m <= nn -> h
1121    | C.Rel _ -> true
1122    | C.Meta _
1123    | C.Sort _
1124    | C.Implicit _
1125    | C.Cast _
1126    | C.Prod _
1127    | C.LetIn _ ->
1128       (* the term has just been type-checked *)
1129       raise (AssertFailure (lazy "17"))
1130    | C.Lambda (name,so,de) ->
1131       does_not_occur ~subst context n nn so &&
1132        guarded_by_constructors ~subst ((Some (name,(C.Decl so)))::context)
1133         (n + 1) (nn + 1) h de args coInductiveTypeURI
1134    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
1135       h &&
1136        List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) tl true
1137    | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) ->
1138       let consty =
1139         let obj,_ =
1140           try
1141             CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
1142           with Not_found -> assert false
1143         in
1144        match obj with
1145           C.InductiveDefinition (itl,_,_,_) ->
1146            let (_,_,_,cl) = List.nth itl i in
1147             let (_,cons) = List.nth cl (j - 1) in
1148              CicSubstitution.subst_vars exp_named_subst cons
1149         | _ ->
1150             raise (TypeCheckerFailure
1151              (lazy ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri)))
1152       in
1153        let rec analyse_branch context ty te =
1154         match CicReduction.whd ~subst context ty with
1155            C.Meta _ -> raise (AssertFailure (lazy "34"))
1156          | C.Rel _
1157          | C.Var _
1158          | C.Sort _ ->
1159             does_not_occur ~subst context n nn te
1160          | C.Implicit _
1161          | C.Cast _ ->
1162             raise (AssertFailure (lazy "24"))(* due to type-checking *)
1163          | C.Prod (name,so,de) ->
1164             analyse_branch ((Some (name,(C.Decl so)))::context) de te
1165          | C.Lambda _
1166          | C.LetIn _ ->
1167             raise (AssertFailure (lazy "25"))(* due to type-checking *)
1168          | C.Appl ((C.MutInd (uri,_,_))::_) when uri == coInductiveTypeURI ->
1169              guarded_by_constructors ~subst context n nn true te []
1170               coInductiveTypeURI
1171          | C.Appl ((C.MutInd (uri,_,_))::_) ->
1172             guarded_by_constructors ~subst context n nn true te tl
1173              coInductiveTypeURI
1174          | C.Appl _ ->
1175             does_not_occur ~subst context n nn te
1176          | C.Const _ -> raise (AssertFailure (lazy "26"))
1177          | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
1178             guarded_by_constructors ~subst context n nn true te []
1179              coInductiveTypeURI
1180          | C.MutInd _ ->
1181             does_not_occur ~subst context n nn te
1182          | C.MutConstruct _ -> raise (AssertFailure (lazy "27"))
1183          (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
1184          (*CSC: in head position.                                       *)
1185          | C.MutCase _
1186          | C.Fix _
1187          | C.CoFix _ ->
1188             raise (AssertFailure (lazy "28"))(* due to type-checking *)
1189        in
1190        let rec analyse_instantiated_type context ty l =
1191         match CicReduction.whd ~subst context ty with
1192            C.Rel _
1193          | C.Var _
1194          | C.Meta _
1195          | C.Sort _
1196          | C.Implicit _
1197          | C.Cast _ -> raise (AssertFailure (lazy "29"))(* due to type-checking *)
1198          | C.Prod (name,so,de) ->
1199             begin
1200              match l with
1201                 [] -> true
1202               | he::tl ->
1203                  analyse_branch context so he &&
1204                   analyse_instantiated_type
1205                    ((Some (name,(C.Decl so)))::context) de tl
1206             end
1207          | C.Lambda _
1208          | C.LetIn _ ->
1209             raise (AssertFailure (lazy "30"))(* due to type-checking *)
1210          | C.Appl _ ->
1211             List.fold_left
1212              (fun i x -> i && does_not_occur ~subst context n nn x) true l
1213          | C.Const _ -> raise (AssertFailure (lazy "31"))
1214          | C.MutInd _ ->
1215             List.fold_left
1216              (fun i x -> i && does_not_occur ~subst context n nn x) true l
1217          | C.MutConstruct _ -> raise (AssertFailure (lazy "32"))
1218          (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
1219          (*CSC: in head position.                                       *)
1220          | C.MutCase _
1221          | C.Fix _
1222          | C.CoFix _ ->
1223             raise (AssertFailure (lazy "33"))(* due to type-checking *)
1224        in
1225         let rec instantiate_type args consty =
1226          function
1227             [] -> true
1228           | tlhe::tltl as l ->
1229              let consty' = CicReduction.whd ~subst context consty in
1230               match args with
1231                  he::tl ->
1232                   begin
1233                    match consty' with
1234                       C.Prod (_,_,de) ->
1235                        let instantiated_de = CicSubstitution.subst he de in
1236                         (*CSC: siamo sicuri che non sia troppo forte? *)
1237                         does_not_occur ~subst context n nn tlhe &
1238                          instantiate_type tl instantiated_de tltl
1239                     | _ ->
1240                       (*CSC:We do not consider backbones with a MutCase, a    *)
1241                       (*CSC:FixPoint, a CoFixPoint and so on in head position.*)
1242                       raise (AssertFailure (lazy "23"))
1243                   end
1244                | [] -> analyse_instantiated_type context consty' l
1245                   (* These are all the other cases *)
1246        in
1247         instantiate_type args consty tl
1248    | C.Appl ((C.CoFix (_,fl))::tl) ->
1249       List.fold_left (fun i x -> i && does_not_occur ~subst context n nn x) true tl &&
1250        let len = List.length fl in
1251         let n_plus_len = n + len
1252         and nn_plus_len = nn + len
1253         (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1254         and tys,_ =
1255           List.fold_left
1256             (fun (types,len) (n,ty,_) ->
1257                (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
1258                 len+1)
1259             ) ([],0) fl
1260         in
1261          List.fold_right
1262           (fun (_,ty,bo) i ->
1263             i && does_not_occur ~subst context n nn ty &&
1264              guarded_by_constructors ~subst (tys@context) n_plus_len nn_plus_len
1265               h bo args coInductiveTypeURI
1266           ) fl true
1267    | C.Appl ((C.MutCase (_,_,out,te,pl))::tl) ->
1268        List.fold_left (fun i x -> i && does_not_occur ~subst context n nn x) true tl &&
1269         does_not_occur ~subst context n nn out &&
1270          does_not_occur ~subst context n nn te &&
1271           List.fold_right
1272            (fun x i ->
1273              i &&
1274              guarded_by_constructors ~subst context n nn h x args
1275               coInductiveTypeURI
1276            ) pl true
1277    | C.Appl l ->
1278       List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) l true
1279    | C.Var (_,exp_named_subst)
1280    | C.Const (_,exp_named_subst) ->
1281       List.fold_right
1282        (fun (_,x) i -> i && does_not_occur ~subst context n nn x) exp_named_subst true
1283    | C.MutInd _ -> assert false
1284    | C.MutConstruct (_,_,_,exp_named_subst) ->
1285       List.fold_right
1286        (fun (_,x) i -> i && does_not_occur ~subst context n nn x) exp_named_subst true
1287    | C.MutCase (_,_,out,te,pl) ->
1288        does_not_occur ~subst context n nn out &&
1289         does_not_occur ~subst context n nn te &&
1290          List.fold_right
1291           (fun x i ->
1292             i &&
1293              guarded_by_constructors ~subst context n nn h x args
1294               coInductiveTypeURI
1295           ) pl true
1296    | C.Fix (_,fl) ->
1297       let len = List.length fl in
1298        let n_plus_len = n + len
1299        and nn_plus_len = nn + len
1300        (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1301        and tys,_ =
1302         List.fold_left
1303           (fun (types,len) (n,_,ty,_) ->
1304              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
1305               len+1)
1306           ) ([],0) fl
1307        in
1308         List.fold_right
1309          (fun (_,_,ty,bo) i ->
1310            i && does_not_occur ~subst context n nn ty &&
1311             does_not_occur ~subst (tys@context) n_plus_len nn_plus_len bo
1312          ) fl true
1313    | C.CoFix (_,fl) ->
1314       let len = List.length fl in
1315        let n_plus_len = n + len
1316        and nn_plus_len = nn + len
1317        (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1318        and tys,_ =
1319         List.fold_left
1320           (fun (types,len) (n,ty,_) ->
1321              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
1322               len+1)
1323           ) ([],0) fl
1324        in
1325         List.fold_right
1326          (fun (_,ty,bo) i ->
1327            i && does_not_occur ~subst context n nn ty &&
1328             guarded_by_constructors ~subst (tys@context) n_plus_len nn_plus_len
1329              h bo
1330              args coInductiveTypeURI
1331          ) fl true
1332
1333 and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
1334   need_dummy ind arity1 arity2 ugraph =
1335  let module C = Cic in
1336  let module U = UriManager in
1337   let arity1 = CicReduction.whd ~subst context arity1 in
1338   let rec check_allowed_sort_elimination_aux ugraph context arity2 need_dummy =
1339    match arity1, CicReduction.whd ~subst context arity2 with
1340      (C.Prod (_,so1,de1), C.Prod (_,so2,de2)) ->
1341        let b,ugraph1 =
1342         CicReduction.are_convertible ~subst ~metasenv context so1 so2 ugraph in
1343        if b then
1344          check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
1345           need_dummy (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2
1346           ugraph1
1347        else
1348          false,ugraph1
1349    | (C.Sort _, C.Prod (name,so,ta)) when not need_dummy ->
1350        let b,ugraph1 =
1351         CicReduction.are_convertible ~subst ~metasenv context so ind ugraph in
1352        if not b then
1353          false,ugraph1
1354        else
1355         check_allowed_sort_elimination_aux ugraph1
1356          ((Some (name,C.Decl so))::context) ta true
1357    | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true,ugraph
1358    | (C.Sort C.Prop, C.Sort C.Set)
1359    | (C.Sort C.Prop, C.Sort C.CProp)
1360    | (C.Sort C.Prop, C.Sort (C.Type _) ) when need_dummy ->
1361        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1362          match o with
1363          C.InductiveDefinition (itl,_,paramsno,_) ->
1364            let itl_len = List.length itl in
1365            let (name,_,ty,cl) = List.nth itl i in
1366            let cl_len = List.length cl in
1367             if (cl_len = 0 || (itl_len = 1 && cl_len = 1)) then
1368              let non_informative,ugraph =
1369               if cl_len = 0 then true,ugraph
1370               else
1371                is_non_informative ~logger [Some (C.Name name,C.Decl ty)]
1372                 paramsno (snd (List.nth cl 0)) ugraph
1373              in
1374               (* is it a singleton or empty non recursive and non informative
1375                  definition? *)
1376               non_informative, ugraph
1377             else
1378               false,ugraph
1379          | _ ->
1380              raise (TypeCheckerFailure
1381                      (lazy ("Unknown mutual inductive definition:" ^
1382                        UriManager.string_of_uri uri)))
1383        )
1384    | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true , ugraph
1385    | (C.Sort C.CProp, C.Sort C.Prop) when need_dummy -> true , ugraph
1386    | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true , ugraph
1387    | (C.Sort C.Set, C.Sort C.CProp) when need_dummy -> true , ugraph
1388    | (C.Sort C.CProp, C.Sort C.Set) when need_dummy -> true , ugraph
1389    | (C.Sort C.CProp, C.Sort C.CProp) when need_dummy -> true , ugraph
1390    | ((C.Sort C.Set, C.Sort (C.Type _)) | (C.Sort C.CProp, C.Sort (C.Type _)))
1391       when need_dummy ->
1392        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1393          match o with
1394            C.InductiveDefinition (itl,_,paramsno,_) ->
1395             let tys =
1396              List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1397             in
1398              let (_,_,_,cl) = List.nth itl i in
1399               (List.fold_right
1400                (fun (_,x) (i,ugraph) ->
1401                  if i then
1402                    is_small ~logger tys paramsno x ugraph
1403                  else
1404                    false,ugraph
1405                     ) cl (true,ugraph))
1406            | _ ->
1407             raise (TypeCheckerFailure
1408              (lazy ("Unknown mutual inductive definition:" ^
1409               UriManager.string_of_uri uri)))
1410        )
1411    | (C.Sort (C.Type _), C.Sort _) when need_dummy -> true , ugraph
1412    | (_,_) -> false,ugraph
1413  in
1414   check_allowed_sort_elimination_aux ugraph context arity2 need_dummy
1415
1416 and type_of_branch ~subst context argsno need_dummy outtype term constype =
1417  let module C = Cic in
1418  let module R = CicReduction in
1419   match R.whd ~subst context constype with
1420      C.MutInd (_,_,_) ->
1421       if need_dummy then
1422        outtype
1423       else
1424        C.Appl [outtype ; term]
1425    | C.Appl (C.MutInd (_,_,_)::tl) ->
1426       let (_,arguments) = split tl argsno
1427       in
1428        if need_dummy && arguments = [] then
1429         outtype
1430        else
1431         C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
1432    | C.Prod (name,so,de) ->
1433       let term' =
1434        match CicSubstitution.lift 1 term with
1435           C.Appl l -> C.Appl (l@[C.Rel 1])
1436         | t -> C.Appl [t ; C.Rel 1]
1437       in
1438        C.Prod (name,so,type_of_branch ~subst
1439         ((Some (name,(C.Decl so)))::context) argsno need_dummy
1440         (CicSubstitution.lift 1 outtype) term' de)
1441    | _ -> raise (AssertFailure (lazy "20"))
1442
1443 (* check_metasenv_consistency checks that the "canonical" context of a
1444 metavariable is consitent - up to relocation via the relocation list l -
1445 with the actual context *)
1446
1447
1448 and check_metasenv_consistency ~logger ~subst metasenv context
1449   canonical_context l ugraph
1450 =
1451   let module C = Cic in
1452   let module R = CicReduction in
1453   let module S = CicSubstitution in
1454   let lifted_canonical_context =
1455     let rec aux i =
1456      function
1457          [] -> []
1458        | (Some (n,C.Decl t))::tl ->
1459            (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
1460        | None::tl -> None::(aux (i+1) tl)
1461        | (Some (n,C.Def (t,ty)))::tl ->
1462            (Some (n,C.Def ((S.subst_meta l (S.lift i t)),S.subst_meta l (S.lift i ty))))::(aux (i+1) tl)
1463     in
1464      aux 1 canonical_context
1465    in
1466    List.fold_left2
1467      (fun ugraph t ct ->
1468        match (t,ct) with
1469        | _,None -> ugraph
1470        | Some t,Some (_,C.Def (ct,_)) ->
1471           (*CSC: the following optimization is to avoid a possibly expensive
1472                  reduction that can be easily avoided and that is quite
1473                  frequent. However, this is better handled using levels to
1474                  control reduction *)
1475           let optimized_t =
1476            match t with
1477               Cic.Rel n ->
1478                (try
1479                  match List.nth context (n - 1) with
1480                     Some (_,C.Def (te,_)) -> S.lift n te
1481                   | _ -> t
1482                 with
1483                  Failure _ -> t)
1484             | _ -> t
1485           in
1486 (*if t <> optimized_t && optimized_t = ct then prerr_endline "!!!!!!!!!!!!!!!"
1487 else if t <> optimized_t then prerr_endline ("@@ " ^ CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm optimized_t ^ " <==> " ^ CicPp.ppterm ct);*)
1488            let b,ugraph1 =
1489              R.are_convertible ~subst ~metasenv context optimized_t ct ugraph
1490            in
1491            if not b then
1492              raise
1493                (TypeCheckerFailure
1494                   (lazy (sprintf "Not well typed metavariable local context: expected a term convertible with %s, found %s" (CicPp.ppterm ct) (CicPp.ppterm t))))
1495            else
1496              ugraph1
1497        | Some t,Some (_,C.Decl ct) ->
1498            let type_t,ugraph1 =
1499              type_of_aux' ~logger ~subst metasenv context t ugraph
1500            in
1501            let b,ugraph2 =
1502              R.are_convertible ~subst ~metasenv context type_t ct ugraph1
1503            in
1504            if not b then
1505              raise (TypeCheckerFailure
1506                      (lazy (sprintf "Not well typed metavariable local context: expected a term of type %s, found %s of type %s"
1507                          (CicPp.ppterm ct) (CicPp.ppterm t)
1508                          (CicPp.ppterm type_t))))
1509            else
1510              ugraph2
1511        | None, _  ->
1512            raise (TypeCheckerFailure
1513                    (lazy ("Not well typed metavariable local context: "^
1514                      "an hypothesis, that is not hidden, is not instantiated")))
1515      ) ugraph l lifted_canonical_context
1516
1517
1518 (*
1519    type_of_aux' is just another name (with a different scope)
1520    for type_of_aux
1521 *)
1522
1523 and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
1524  let rec type_of_aux ~logger context t ugraph =
1525   let module C = Cic in
1526   let module R = CicReduction in
1527   let module S = CicSubstitution in
1528   let module U = UriManager in
1529    match t with
1530       C.Rel n ->
1531        (try
1532          match List.nth context (n - 1) with
1533             Some (_,C.Decl t) -> S.lift n t,ugraph
1534           | Some (_,C.Def (_,ty)) -> S.lift n ty,ugraph
1535           | None -> raise
1536               (TypeCheckerFailure (lazy "Reference to deleted hypothesis"))
1537         with
1538         Failure _ ->
1539           raise (TypeCheckerFailure (lazy "unbound variable"))
1540        )
1541     | C.Var (uri,exp_named_subst) ->
1542       incr fdebug ;
1543         let ugraph1 =
1544           check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
1545         in
1546         let ty,ugraph2 = type_of_variable ~logger uri ugraph1 in
1547         let ty1 = CicSubstitution.subst_vars exp_named_subst ty in
1548           decr fdebug ;
1549           ty1,ugraph2
1550     | C.Meta (n,l) ->
1551        (try
1552           let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in
1553           let ugraph1 =
1554             check_metasenv_consistency ~logger
1555               ~subst metasenv context canonical_context l ugraph
1556           in
1557             (* assuming subst is well typed !!!!! *)
1558             ((CicSubstitution.subst_meta l ty), ugraph1)
1559               (* type_of_aux context (CicSubstitution.subst_meta l term) *)
1560         with CicUtil.Subst_not_found _ ->
1561           let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
1562           let ugraph1 =
1563             check_metasenv_consistency ~logger
1564               ~subst metasenv context canonical_context l ugraph
1565           in
1566             ((CicSubstitution.subst_meta l ty),ugraph1))
1567       (* TASSI: CONSTRAINTS *)
1568     | C.Sort (C.Type t) ->
1569        let t' = CicUniv.fresh() in
1570        (try
1571          let ugraph1 = CicUniv.add_gt t' t ugraph in
1572            (C.Sort (C.Type t')),ugraph1
1573         with
1574          CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
1575     | C.Sort s -> (C.Sort (C.Type (CicUniv.fresh ()))),ugraph
1576     | C.Implicit _ -> raise (AssertFailure (lazy "Implicit found"))
1577     | C.Cast (te,ty) as t ->
1578        let _,ugraph1 = type_of_aux ~logger context ty ugraph in
1579        let ty_te,ugraph2 = type_of_aux ~logger context te ugraph1 in
1580        let b,ugraph3 =
1581          R.are_convertible ~subst ~metasenv context ty_te ty ugraph2
1582        in
1583          if b then
1584            ty,ugraph3
1585          else
1586            raise (TypeCheckerFailure
1587                     (lazy (sprintf "Invalid cast %s" (CicPp.ppterm t))))
1588     | C.Prod (name,s,t) ->
1589        let sort1,ugraph1 = type_of_aux ~logger context s ugraph in
1590        let sort2,ugraph2 =
1591          type_of_aux ~logger  ((Some (name,(C.Decl s)))::context) t ugraph1
1592        in
1593        sort_of_prod ~subst context (name,s) (sort1,sort2) ugraph2
1594    | C.Lambda (n,s,t) ->
1595        let sort1,ugraph1 = type_of_aux ~logger context s ugraph in
1596        (match R.whd ~subst context sort1 with
1597            C.Meta _
1598          | C.Sort _ -> ()
1599          | _ ->
1600            raise
1601             (TypeCheckerFailure (lazy (sprintf
1602               "Not well-typed lambda-abstraction: the source %s should be a type; instead it is a term of type %s" (CicPp.ppterm s)
1603                 (CicPp.ppterm sort1))))
1604        ) ;
1605        let type2,ugraph2 =
1606          type_of_aux ~logger ((Some (n,(C.Decl s)))::context) t ugraph1
1607        in
1608          (C.Prod (n,s,type2)),ugraph2
1609    | C.LetIn (n,s,ty,t) ->
1610       (* only to check if s is well-typed *)
1611       let ty',ugraph1 = type_of_aux ~logger context s ugraph in
1612       let b,ugraph1 =
1613        R.are_convertible ~subst ~metasenv context ty ty' ugraph1
1614       in
1615        if not b then
1616         raise
1617          (TypeCheckerFailure
1618            (lazy (sprintf
1619              "The type of %s is %s but it is expected to be %s"
1620                (CicPp.ppterm s) (CicPp.ppterm ty') (CicPp.ppterm ty))))
1621        else
1622        (* The type of a LetIn is a LetIn. Extremely slow since the computed
1623           LetIn is later reduced and maybe also re-checked.
1624        (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t))
1625        *)
1626        (* The type of the LetIn is reduced. Much faster than the previous
1627           solution. Moreover the inferred type is probably very different
1628           from the expected one.
1629        (CicReduction.whd ~subst context
1630         (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)))
1631        *)
1632        (* One-step LetIn reduction. Even faster than the previous solution.
1633           Moreover the inferred type is closer to the expected one. *)
1634        let ty1,ugraph2 =
1635          type_of_aux ~logger
1636            ((Some (n,(C.Def (s,ty))))::context) t ugraph1
1637        in
1638        (CicSubstitution.subst ~avoid_beta_redexes:true s ty1),ugraph2
1639    | C.Appl (he::tl) when List.length tl > 0 ->
1640        let hetype,ugraph1 = type_of_aux ~logger context he ugraph in
1641        let tlbody_and_type,ugraph2 =
1642          List.fold_right (
1643            fun x (l,ugraph) ->
1644              let ty,ugraph1 = type_of_aux ~logger context x ugraph in
1645              (*let _,ugraph1 = type_of_aux ~logger  context ty ugraph1 in*)
1646                ((x,ty)::l,ugraph1))
1647            tl ([],ugraph1)
1648        in
1649          (* TASSI: questa c'era nel mio... ma non nel CVS... *)
1650          (* let _,ugraph2 = type_of_aux context hetype ugraph2 in *)
1651          eat_prods ~subst context hetype tlbody_and_type ugraph2
1652    | C.Appl _ -> raise (AssertFailure (lazy "Appl: no arguments"))
1653    | C.Const (uri,exp_named_subst) ->
1654        incr fdebug ;
1655        let ugraph1 =
1656          check_exp_named_subst ~logger ~subst  context exp_named_subst ugraph
1657        in
1658        let cty,ugraph2 = type_of_constant ~logger uri ugraph1 in
1659        let cty1 =
1660          CicSubstitution.subst_vars exp_named_subst cty
1661        in
1662          decr fdebug ;
1663          cty1,ugraph2
1664    | C.MutInd (uri,i,exp_named_subst) ->
1665       incr fdebug ;
1666        let ugraph1 =
1667          check_exp_named_subst ~logger  ~subst context exp_named_subst ugraph
1668        in
1669          (* TASSI: da me c'era anche questa, ma in CVS no *)
1670        let mty,ugraph2 = type_of_mutual_inductive_defs ~logger uri i ugraph1 in
1671          (* fine parte dubbia *)
1672        let cty =
1673          CicSubstitution.subst_vars exp_named_subst mty
1674        in
1675          decr fdebug ;
1676          cty,ugraph2
1677    | C.MutConstruct (uri,i,j,exp_named_subst) ->
1678        let ugraph1 =
1679          check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
1680        in
1681          (* TASSI: idem come sopra *)
1682        let mty,ugraph2 =
1683          type_of_mutual_inductive_constr ~logger uri i j ugraph1
1684        in
1685        let cty =
1686          CicSubstitution.subst_vars exp_named_subst mty
1687        in
1688          cty,ugraph2
1689    | C.MutCase (uri,i,outtype,term,pl) ->
1690       let outsort,ugraph1 = type_of_aux ~logger context outtype ugraph in
1691       let (need_dummy, k) =
1692       let rec guess_args context t =
1693         let outtype = CicReduction.whd ~subst context t in
1694           match outtype with
1695               C.Sort _ -> (true, 0)
1696             | C.Prod (name, s, t) ->
1697                 let (b, n) =
1698                   guess_args ((Some (name,(C.Decl s)))::context) t in
1699                   if n = 0 then
1700                   (* last prod before sort *)
1701                     match CicReduction.whd ~subst context s with
1702 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1703                         C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
1704                           (false, 1)
1705 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1706                       | C.Appl ((C.MutInd (uri',i',_)) :: _)
1707                           when U.eq uri' uri && i' = i -> (false, 1)
1708                       | _ -> (true, 1)
1709                   else
1710                     (b, n + 1)
1711             | _ ->
1712                 raise
1713                   (TypeCheckerFailure
1714                      (lazy (sprintf
1715                         "Malformed case analasys' output type %s"
1716                         (CicPp.ppterm outtype))))
1717       in
1718 (*
1719       let (parameters, arguments, exp_named_subst),ugraph2 =
1720         let ty,ugraph2 = type_of_aux context term ugraph1 in
1721           match R.whd ~subst context ty with
1722            (*CSC manca il caso dei CAST *)
1723 (*CSC: ma servono i parametri (uri,i)? Se si', perche' non serve anche il *)
1724 (*CSC: parametro exp_named_subst? Se no, perche' non li togliamo?         *)
1725 (*CSC: Hint: nella DTD servono per gli stylesheet.                        *)
1726               C.MutInd (uri',i',exp_named_subst) as typ ->
1727                 if U.eq uri uri' && i = i' then
1728                   ([],[],exp_named_subst),ugraph2
1729                 else
1730                   raise
1731                     (TypeCheckerFailure
1732                       (lazy (sprintf
1733                           ("Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}")
1734                           (CicPp.ppterm typ) (U.string_of_uri uri) i)))
1735             | C.Appl
1736                 ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
1737                 if U.eq uri uri' && i = i' then
1738                   let params,args =
1739                     split tl (List.length tl - k)
1740                   in (params,args,exp_named_subst),ugraph2
1741                 else
1742                   raise
1743                     (TypeCheckerFailure
1744                       (lazy (sprintf
1745                           ("Case analysys: analysed term type is %s, "^
1746                            "but is expected to be (an application of) "^
1747                            "%s#1/%d{_}")
1748                           (CicPp.ppterm typ') (U.string_of_uri uri) i)))
1749             | _ ->
1750                 raise
1751                   (TypeCheckerFailure
1752                     (lazy (sprintf
1753                         ("Case analysis: "^
1754                          "analysed term %s is not an inductive one")
1755                         (CicPp.ppterm term))))
1756 *)
1757       let (b, k) = guess_args context outsort in
1758           if not b then (b, k - 1) else (b, k) in
1759       let (parameters, arguments, exp_named_subst),ugraph2 =
1760         let ty,ugraph2 = type_of_aux ~logger context term ugraph1 in
1761         match R.whd ~subst context ty with
1762             C.MutInd (uri',i',exp_named_subst) as typ ->
1763               if U.eq uri uri' && i = i' then
1764                 ([],[],exp_named_subst),ugraph2
1765               else raise
1766                 (TypeCheckerFailure
1767                   (lazy (sprintf
1768                       ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}")
1769                       (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i)))
1770           | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) ->
1771               if U.eq uri uri' && i = i' then
1772                 let params,args =
1773                   split tl (List.length tl - k)
1774                 in (params,args,exp_named_subst),ugraph2
1775               else raise
1776                 (TypeCheckerFailure
1777                   (lazy (sprintf
1778                       ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}")
1779                       (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i)))
1780           | _ ->
1781               raise
1782                 (TypeCheckerFailure
1783                   (lazy (sprintf
1784                       "Case analysis: analysed term %s is not an inductive one"
1785                       (CicPp.ppterm term))))
1786       in
1787         (*
1788            let's control if the sort elimination is allowed:
1789            [(I q1 ... qr)|B]
1790         *)
1791       let sort_of_ind_type =
1792         if parameters = [] then
1793           C.MutInd (uri,i,exp_named_subst)
1794         else
1795           C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters)
1796       in
1797       let type_of_sort_of_ind_ty,ugraph3 =
1798         type_of_aux ~logger context sort_of_ind_type ugraph2 in
1799       let b,ugraph4 =
1800         check_allowed_sort_elimination ~subst ~metasenv ~logger  context uri i
1801           need_dummy sort_of_ind_type type_of_sort_of_ind_ty outsort ugraph3
1802       in
1803         if not b then
1804         raise
1805           (TypeCheckerFailure (lazy ("Case analysis: sort elimination not allowed")));
1806         (* let's check if the type of branches are right *)
1807       let parsno,constructorsno =
1808         let obj,_ =
1809           try
1810             CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
1811           with Not_found -> assert false
1812         in
1813         match obj with
1814             C.InductiveDefinition (il,_,parsno,_) ->
1815              let _,_,_,cl =
1816               try List.nth il i with Failure _ -> assert false
1817              in
1818               parsno, List.length cl
1819           | _ ->
1820               raise (TypeCheckerFailure
1821                 (lazy ("Unknown mutual inductive definition:" ^
1822                   UriManager.string_of_uri uri)))
1823       in
1824       if List.length pl <> constructorsno then
1825        raise (TypeCheckerFailure
1826         (lazy ("Wrong number of cases in case analysis"))) ;
1827       let (_,branches_ok,ugraph5) =
1828         List.fold_left
1829           (fun (j,b,ugraph) p ->
1830             if b then
1831               let cons =
1832                 if parameters = [] then
1833                   (C.MutConstruct (uri,i,j,exp_named_subst))
1834                 else
1835                   (C.Appl
1836                      (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
1837               in
1838               let ty_p,ugraph1 = type_of_aux ~logger context p ugraph in
1839               let ty_cons,ugraph3 = type_of_aux ~logger context cons ugraph1 in
1840               (* 2 is skipped *)
1841               let ty_branch =
1842                 type_of_branch ~subst context parsno need_dummy outtype cons
1843                   ty_cons in
1844               let b1,ugraph4 =
1845                 R.are_convertible
1846                   ~subst ~metasenv context ty_p ty_branch ugraph3
1847               in
1848 (* Debugging code
1849 if not b1 then
1850 begin
1851 prerr_endline ("\n!OUTTYPE= " ^ CicPp.ppterm outtype);
1852 prerr_endline ("!CONS= " ^ CicPp.ppterm cons);
1853 prerr_endline ("!TY_CONS= " ^ CicPp.ppterm ty_cons);
1854 prerr_endline ("#### " ^ CicPp.ppterm ty_p ^ "\n<==>\n" ^ CicPp.ppterm ty_branch);
1855 end;
1856 *)
1857               if not b1 then
1858                 debug_print (lazy
1859                   ("#### " ^ CicPp.ppterm ty_p ^
1860                   " <==> " ^ CicPp.ppterm ty_branch));
1861               (j + 1,b1,ugraph4)
1862             else
1863               (j,false,ugraph)
1864           ) (1,true,ugraph4) pl
1865          in
1866           if not branches_ok then
1867            raise
1868             (TypeCheckerFailure (lazy "Case analysys: wrong branch type"));
1869           let arguments' =
1870            if not need_dummy then outtype::arguments@[term]
1871            else outtype::arguments in
1872           let outtype =
1873            if need_dummy && arguments = [] then outtype
1874            else CicReduction.head_beta_reduce (C.Appl arguments')
1875           in
1876            outtype,ugraph5
1877    | C.Fix (i,fl) ->
1878       let types,kl,ugraph1,len =
1879         List.fold_left
1880           (fun (types,kl,ugraph,len) (n,k,ty,_) ->
1881             let _,ugraph1 = type_of_aux ~logger context ty ugraph in
1882              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
1883               k::kl,ugraph1,len+1)
1884           ) ([],[],ugraph,0) fl
1885       in
1886       let ugraph2 =
1887         List.fold_left
1888           (fun ugraph (name,x,ty,bo) ->
1889              let ty_bo,ugraph1 =
1890                type_of_aux ~logger (types@context) bo ugraph
1891              in
1892              let b,ugraph2 =
1893                R.are_convertible ~subst ~metasenv (types@context)
1894                  ty_bo (CicSubstitution.lift len ty) ugraph1 in
1895                if b then
1896                  begin
1897                    let (m, eaten, context') =
1898                      eat_lambdas ~subst (types @ context) (x + 1) bo
1899                    in
1900                      (*
1901                        let's control the guarded by
1902                        destructors conditions D{f,k,x,M}
1903                      *)
1904                      if not (guarded_by_destructors ~subst context' eaten
1905                                (len + eaten) kl 1 [] m) then
1906                        raise
1907                          (TypeCheckerFailure
1908                            (lazy ("Fix: not guarded by destructors")))
1909                      else
1910                        ugraph2
1911                  end
1912                else
1913                  raise (TypeCheckerFailure (lazy ("Fix: ill-typed bodies")))
1914           ) ugraph1 fl in
1915         (*CSC: controlli mancanti solo su D{f,k,x,M} *)
1916       let (_,_,ty,_) = List.nth fl i in
1917         ty,ugraph2
1918    | C.CoFix (i,fl) ->
1919        let types,ugraph1,len =
1920          List.fold_left
1921            (fun (l,ugraph,len) (n,ty,_) ->
1922               let _,ugraph1 =
1923                 type_of_aux ~logger context ty ugraph in
1924                 (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::l,
1925                  ugraph1,len+1)
1926            ) ([],ugraph,0) fl
1927        in
1928        let ugraph2 =
1929          List.fold_left
1930            (fun ugraph (_,ty,bo) ->
1931               let ty_bo,ugraph1 =
1932                 type_of_aux ~logger (types @ context) bo ugraph
1933               in
1934               let b,ugraph2 =
1935                 R.are_convertible ~subst ~metasenv (types @ context) ty_bo
1936                   (CicSubstitution.lift len ty) ugraph1
1937               in
1938                 if b then
1939                   begin
1940                     (* let's control that the returned type is coinductive *)
1941                     match returns_a_coinductive ~subst context ty with
1942                         None ->
1943                           raise
1944                           (TypeCheckerFailure
1945                             (lazy "CoFix: does not return a coinductive type"))
1946                       | Some uri ->
1947                           (*
1948                             let's control the guarded by constructors
1949                             conditions C{f,M}
1950                           *)
1951                           if not (guarded_by_constructors ~subst
1952                               (types @ context) 0 len false bo [] uri) then
1953                             raise
1954                               (TypeCheckerFailure
1955                                 (lazy "CoFix: not guarded by constructors"))
1956                           else
1957                           ugraph2
1958                   end
1959                 else
1960                   raise
1961                     (TypeCheckerFailure (lazy "CoFix: ill-typed bodies"))
1962            ) ugraph1 fl
1963        in
1964        let (_,ty,_) = List.nth fl i in
1965          ty,ugraph2
1966
1967  and check_exp_named_subst ~logger ~subst context ugraph =
1968    let rec check_exp_named_subst_aux ~logger esubsts l ugraph =
1969      match l with
1970          [] -> ugraph
1971        | ((uri,t) as item)::tl ->
1972            let ty_uri,ugraph1 = type_of_variable ~logger uri ugraph in
1973            let typeofvar =
1974              CicSubstitution.subst_vars esubsts ty_uri in
1975            let typeoft,ugraph2 = type_of_aux ~logger context t ugraph1 in
1976            let b,ugraph3 =
1977              CicReduction.are_convertible ~subst ~metasenv
1978                context typeoft typeofvar ugraph2
1979            in
1980              if b then
1981                check_exp_named_subst_aux ~logger (esubsts@[item]) tl ugraph3
1982              else
1983                begin
1984                  CicReduction.fdebug := 0 ;
1985                  ignore
1986                    (CicReduction.are_convertible
1987                       ~subst ~metasenv context typeoft typeofvar ugraph2) ;
1988                  fdebug := 0 ;
1989                  debug typeoft [typeofvar] ;
1990                  raise (TypeCheckerFailure (lazy "Wrong Explicit Named Substitution"))
1991                end
1992    in
1993      check_exp_named_subst_aux ~logger [] ugraph
1994
1995  and sort_of_prod ~subst context (name,s) (t1, t2) ugraph =
1996   let module C = Cic in
1997    let t1' = CicReduction.whd ~subst context t1 in
1998    let t2' = CicReduction.whd ~subst ((Some (name,C.Decl s))::context) t2 in
1999    match (t1', t2') with
2000       (C.Sort s1, C.Sort s2)
2001         when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
2002          (* different from Coq manual!!! *)
2003          C.Sort s2,ugraph
2004     | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
2005       (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
2006        let t' = CicUniv.fresh() in
2007         (try
2008          let ugraph1 = CicUniv.add_ge t' t1 ugraph in
2009          let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
2010           C.Sort (C.Type t'),ugraph2
2011         with
2012          CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
2013     | (C.Sort _,C.Sort (C.Type t1)) ->
2014         (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
2015         C.Sort (C.Type t1),ugraph (* c'e' bisogno di un fresh? *)
2016     | (C.Meta _, C.Sort _) -> t2',ugraph
2017     | (C.Meta _, (C.Meta (_,_) as t))
2018     | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
2019         t2',ugraph
2020     | (_,_) -> raise (TypeCheckerFailure (lazy (sprintf
2021         "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1')
2022           (CicPp.ppterm t2'))))
2023
2024  and eat_prods ~subst context hetype l ugraph =
2025    (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
2026    (*CSC: cucinati                                                         *)
2027    match l with
2028        [] -> hetype,ugraph
2029      | (hete, hety)::tl ->
2030          (match (CicReduction.whd ~subst context hetype) with
2031               Cic.Prod (n,s,t) ->
2032                 let b,ugraph1 =
2033 (*if (match hety,s with Cic.Sort _,Cic.Sort _ -> false | _,_ -> true) && hety <> s then(
2034 prerr_endline ("AAA22: " ^ CicPp.ppterm hete ^ ": " ^ CicPp.ppterm hety ^ " <==> " ^ CicPp.ppterm s); let res = CicReduction.are_convertible ~subst ~metasenv context hety s ugraph in prerr_endline "#"; res) else*)
2035                   CicReduction.are_convertible
2036                     ~subst ~metasenv context hety s ugraph
2037                 in
2038                   if b then
2039                     begin
2040                       CicReduction.fdebug := -1 ;
2041                       eat_prods ~subst context
2042                         (CicSubstitution.subst ~avoid_beta_redexes:true hete t)
2043                          tl ugraph1
2044                         (*TASSI: not sure *)
2045                     end
2046                   else
2047                     begin
2048                       CicReduction.fdebug := 0 ;
2049                       ignore (CicReduction.are_convertible
2050                                 ~subst ~metasenv context s hety ugraph) ;
2051                       fdebug := 0 ;
2052                       debug s [hety] ;
2053                       raise
2054                         (TypeCheckerFailure
2055                           (lazy (sprintf
2056                               ("Appl: wrong parameter-type, expected %s, found %s")
2057                               (CicPp.ppterm hetype) (CicPp.ppterm s))))
2058                     end
2059             | _ ->
2060                 raise (TypeCheckerFailure
2061                         (lazy "Appl: this is not a function, it cannot be applied"))
2062          )
2063
2064  and returns_a_coinductive ~subst context ty =
2065   let module C = Cic in
2066    match CicReduction.whd ~subst context ty with
2067       C.MutInd (uri,i,_) ->
2068        (*CSC: definire una funzioncina per questo codice sempre replicato *)
2069         let obj,_ =
2070           try
2071             CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
2072           with Not_found -> assert false
2073         in
2074         (match obj with
2075            C.InductiveDefinition (itl,_,_,_) ->
2076             let (_,is_inductive,_,_) = List.nth itl i in
2077              if is_inductive then None else (Some uri)
2078          | _ ->
2079             raise (TypeCheckerFailure
2080               (lazy ("Unknown mutual inductive definition:" ^
2081               UriManager.string_of_uri uri)))
2082         )
2083     | C.Appl ((C.MutInd (uri,i,_))::_) ->
2084        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
2085          match o with
2086            C.InductiveDefinition (itl,_,_,_) ->
2087             let (_,is_inductive,_,_) = List.nth itl i in
2088              if is_inductive then None else (Some uri)
2089          | _ ->
2090             raise (TypeCheckerFailure
2091               (lazy ("Unknown mutual inductive definition:" ^
2092               UriManager.string_of_uri uri)))
2093         )
2094     | C.Prod (n,so,de) ->
2095        returns_a_coinductive ~subst ((Some (n,C.Decl so))::context) de
2096     | _ -> None
2097
2098  in
2099 (*CSC
2100 debug_print (lazy ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t)) ; flush stderr ;
2101 let res =
2102 *)
2103   type_of_aux ~logger context t ugraph
2104 (*
2105 in debug_print (lazy "FINE TYPE_OF_AUX") ; flush stderr ; res
2106 *)
2107
2108 (* is a small constructor? *)
2109 (*CSC: ottimizzare calcolando staticamente *)
2110 and is_small_or_non_informative ~condition ~logger context paramsno c ugraph =
2111  let rec is_small_or_non_informative_aux ~logger context c ugraph =
2112   let module C = Cic in
2113    match CicReduction.whd context c with
2114       C.Prod (n,so,de) ->
2115        let s,ugraph1 = type_of_aux' ~logger [] context so ugraph in
2116        let b = condition s in
2117        if b then
2118          is_small_or_non_informative_aux
2119           ~logger ((Some (n,(C.Decl so)))::context) de ugraph1
2120        else
2121          false,ugraph1
2122     | _ -> true,ugraph (*CSC: we trust the type-checker *)
2123  in
2124   let (context',dx) = split_prods ~subst:[] context paramsno c in
2125    is_small_or_non_informative_aux ~logger context' dx ugraph
2126
2127 and is_small ~logger =
2128  is_small_or_non_informative
2129   ~condition:(fun s -> s=Cic.Sort Cic.Prop || s=Cic.Sort Cic.Set)
2130   ~logger
2131
2132 and is_non_informative ~logger =
2133  is_small_or_non_informative
2134   ~condition:(fun s -> s=Cic.Sort Cic.Prop)
2135   ~logger
2136
2137 and type_of ~logger t ugraph =
2138 (*CSC
2139 debug_print (lazy ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t)) ; flush stderr ;
2140 let res =
2141 *)
2142  type_of_aux' ~logger [] [] t ugraph
2143 (*CSC
2144 in debug_print (lazy "FINE TYPE_OF_AUX'") ; flush stderr ; res
2145 *)
2146 ;;
2147
2148 let typecheck_obj0 ~logger uri ugraph =
2149  let module C = Cic in
2150   function
2151      C.Constant (_,Some te,ty,_,_) ->
2152       let _,ugraph = type_of ~logger ty ugraph in
2153       let ty_te,ugraph = type_of ~logger te ugraph in
2154       let b,ugraph = (CicReduction.are_convertible [] ty_te ty ugraph) in
2155        if not b then
2156          raise (TypeCheckerFailure
2157           (lazy
2158             ("the type of the body is not the one expected:\n" ^
2159              CicPp.ppterm ty_te ^ "\nvs\n" ^
2160              CicPp.ppterm ty)))
2161        else
2162         ugraph
2163    | C.Constant (_,None,ty,_,_) ->
2164       (* only to check that ty is well-typed *)
2165       let _,ugraph = type_of ~logger ty ugraph in
2166        ugraph
2167    | C.CurrentProof (_,conjs,te,ty,_,_) ->
2168       let _,ugraph =
2169        List.fold_left
2170         (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
2171           let _,ugraph =
2172            type_of_aux' ~logger metasenv context ty ugraph
2173           in
2174            metasenv @ [conj],ugraph
2175         ) ([],ugraph) conjs
2176       in
2177        let _,ugraph = type_of_aux' ~logger conjs [] ty ugraph in
2178        let type_of_te,ugraph =
2179         type_of_aux' ~logger conjs [] te ugraph
2180        in
2181        let b,ugraph = CicReduction.are_convertible [] type_of_te ty ugraph in
2182         if not b then
2183           raise (TypeCheckerFailure (lazy (sprintf
2184            "the current proof is not well typed because the type %s of the body is not convertible to the declared type %s"
2185            (CicPp.ppterm type_of_te) (CicPp.ppterm ty))))
2186         else
2187          ugraph
2188    | C.Variable (_,bo,ty,_,_) ->
2189       (* only to check that ty is well-typed *)
2190       let _,ugraph = type_of ~logger ty ugraph in
2191        (match bo with
2192            None -> ugraph
2193          | Some bo ->
2194             let ty_bo,ugraph = type_of ~logger bo ugraph in
2195             let b,ugraph = CicReduction.are_convertible [] ty_bo ty ugraph in
2196              if not b then
2197               raise (TypeCheckerFailure
2198                (lazy "the body is not the one expected"))
2199              else
2200               ugraph
2201             )
2202    | (C.InductiveDefinition _ as obj) ->
2203       check_mutual_inductive_defs ~logger uri obj ugraph
2204
2205 let typecheck uri =
2206  let module C = Cic in
2207  let module R = CicReduction in
2208  let module U = UriManager in
2209  let logger = new CicLogger.logger in
2210    (* ??? match CicEnvironment.is_type_checked ~trust:true uri with ???? *)
2211    match CicEnvironment.is_type_checked ~trust:false CicUniv.empty_ugraph uri with
2212      CicEnvironment.CheckedObj (cobj,ugraph') ->
2213        (* debug_print (lazy ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri));*)
2214        cobj,ugraph'
2215    | CicEnvironment.UncheckedObj uobj ->
2216       (* let's typecheck the uncooked object *)
2217       logger#log (`Start_type_checking uri) ;
2218       (* debug_print (lazy ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri)); *)
2219       let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph uobj in
2220         try
2221           CicEnvironment.set_type_checking_info uri;
2222           logger#log (`Type_checking_completed uri);
2223           match CicEnvironment.is_type_checked ~trust:false ugraph uri with
2224               CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
2225             | _ -> raise CicEnvironmentError
2226         with
2227             (*
2228               this is raised if set_type_checking_info is called on an object
2229               that has no associated universe file. If we are in univ_maker
2230               phase this is OK since univ_maker will properly commit the
2231               object.
2232             *)
2233             Invalid_argument s ->
2234               (*debug_print (lazy s);*)
2235               uobj,ugraph
2236 ;;
2237
2238 let typecheck_obj ~logger uri obj =
2239  let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph obj in
2240  let ugraph, univlist, obj = CicUnivUtils.clean_and_fill uri obj ugraph in
2241   CicEnvironment.add_type_checked_obj uri (obj,ugraph,univlist)
2242
2243 (** wrappers which instantiate fresh loggers *)
2244
2245 let profiler = HExtlib.profile "K/CicTypeChecker.type_of_aux'"
2246
2247 let type_of_aux' ?(subst = []) metasenv context t ugraph =
2248   let logger = new CicLogger.logger in
2249   profiler.HExtlib.profile
2250     (type_of_aux' ~logger ~subst metasenv context t) ugraph
2251
2252 let typecheck_obj uri obj =
2253  let logger = new CicLogger.logger in
2254  typecheck_obj ~logger uri obj
2255
2256 (* check_allowed_sort_elimination uri i s1 s2
2257    This function is used outside the kernel to determine in advance whether
2258    a MutCase will be allowed or not.
2259    [uri,i] is the type of the term to match
2260    [s1] is the sort of the term to eliminate (i.e. the head of the arity
2261         of the inductive type [uri,i])
2262    [s2] is the sort of the goal (i.e. the head of the type of the outtype
2263         of the MutCase) *)
2264 let check_allowed_sort_elimination uri i s1 s2 =
2265  fst (check_allowed_sort_elimination ~subst:[] ~metasenv:[]
2266   ~logger:(new CicLogger.logger) [] uri i true
2267   (Cic.Implicit None) (* never used *) (Cic.Sort s1) (Cic.Sort s2)
2268   CicUniv.empty_ugraph)
2269 ;;
2270
2271 Deannotate.type_of_aux' := fun context t -> fst (type_of_aux' [] context t CicUniv.oblivion_ugraph);;
2272
2273 *)
2274
2275 module C = NCic
2276 module R = NCicReduction
2277 module S = NCicSubstitution
2278 module U = NCicUtils
2279
2280
2281 let sort_of_prod ~subst context (name,s) (t1, t2) =
2282    let t1 = R.whd ~subst context t1 in
2283    let t2 = R.whd ~subst ((name,C.Decl s)::context) t2 in
2284    match t1, t2 with
2285    | C.Sort s1, C.Sort s2
2286       (* different from Coq manual, Impredicative Set! *)
2287       when (s2 = C.Prop || s2 = C.Set || s2 = C.CProp) -> C.Sort s2
2288    | C.Sort (C.Type t1), C.Sort (C.Type t2) -> C.Sort (C.Type (max t1 t2))
2289    | C.Sort _,C.Sort (C.Type t1) -> C.Sort (C.Type t1)
2290    | C.Meta _, C.Sort _ -> t2
2291    | C.Meta _, ((C.Meta _) as t)
2292    | C.Sort _, ((C.Meta _) as t) when U.is_closed t -> t2
2293    | _ ->
2294       raise (TypeCheckerFailure (lazy (Printf.sprintf
2295         "Prod: expected two sorts, found = %s, %s"
2296          (NCicPp.ppterm t1) (NCicPp.ppterm t2))))
2297 ;;
2298
2299
2300 let typeof ~subst ~metasenv context term =
2301   let rec aux context = function
2302     | C.Rel n ->
2303        (try
2304          match List.nth context (n - 1) with
2305          | (_,C.Decl ty) -> S.lift n ty
2306          | (_,C.Def (_,ty)) -> S.lift n ty
2307         with Failure _ -> raise (TypeCheckerFailure (lazy "unbound variable")))
2308     | C.Sort (C.Type i) -> C.Sort (C.Type (i+1))
2309     | C.Sort s -> C.Sort (C.Type 0)
2310     | C.Implicit _ -> raise (AssertFailure (lazy "Implicit found"))
2311     | C.Prod (name,s,t) ->
2312        let sort1 = aux context s in
2313        let sort2 = aux ((name,(C.Decl s))::context) t in
2314        sort_of_prod ~subst context (name,s) (sort1,sort2)
2315     | C.Lambda (n,s,t) ->
2316        let sort1 = aux context s in
2317        (match R.whd ~subst context sort1 with
2318        | C.Meta _ | C.Sort _ -> ()
2319        | _ ->
2320          raise
2321            (TypeCheckerFailure (lazy (Printf.sprintf
2322              ("Not well-typed lambda-abstraction: " ^^
2323              "the source %s should be a type; instead it is a term " ^^
2324              "of type %s") (NCicPp.ppterm s) (NCicPp.ppterm sort1)))));
2325        let type2 =
2326          aux ((n,(C.Decl s))::context) t
2327        in
2328          C.Prod (n,s,type2)
2329     | C.LetIn (n,ty,t,bo) ->
2330        let ty_t = aux context t in
2331        if not (R.are_convertible ~subst ~metasenv context ty ty_t) then
2332          raise
2333           (TypeCheckerFailure
2334             (lazy (Printf.sprintf
2335               "The type of %s is %s but it is expected to be %s"
2336                 (NCicPp.ppterm t) (NCicPp.ppterm ty_t) (NCicPp.ppterm ty))))
2337        else
2338          (* Alternatives:
2339            1) The type of a LetIn is a LetIn, extremely slow since the computed
2340               LetIn may be later reduced.
2341            2) The type of the LetIn is reduced, much faster than the previous
2342               solution, moreover the inferred type is probably very different
2343               from the expected one.
2344            3) One-step LetIn reduction, even faster than the previous solution,
2345               moreover the inferred type is closer to the expected one. *)
2346          let ty_bo = aux  ((n,C.Def (t,ty))::context) bo in
2347          S.subst ~avoid_beta_redexes:true t ty_bo
2348  in
2349    aux context term
2350 (*
2351     | C.Meta (n,l) ->
2352        (try
2353           let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in
2354           let ugraph1 =
2355             check_metasenv_consistency ~logger
2356               ~subst metasenv context canonical_context l ugraph
2357           in
2358             (* assuming subst is well typed !!!!! *)
2359             ((CicSubstitution.subst_meta l ty), ugraph1)
2360               (* type_of_aux context (CicSubstitution.subst_meta l term) *)
2361         with CicUtil.Subst_not_found _ ->
2362           let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
2363           let ugraph1 =
2364             check_metasenv_consistency ~logger
2365               ~subst metasenv context canonical_context l ugraph
2366           in
2367             ((CicSubstitution.subst_meta l ty),ugraph1))
2368    | C.Appl (he::tl) when List.length tl > 0 ->
2369        let hetype,ugraph1 = type_of_aux ~logger context he ugraph in
2370        let tlbody_and_type,ugraph2 =
2371          List.fold_right (
2372            fun x (l,ugraph) ->
2373              let ty,ugraph1 = type_of_aux ~logger context x ugraph in
2374              (*let _,ugraph1 = type_of_aux ~logger  context ty ugraph1 in*)
2375                ((x,ty)::l,ugraph1))
2376            tl ([],ugraph1)
2377        in
2378          (* TASSI: questa c'era nel mio... ma non nel CVS... *)
2379          (* let _,ugraph2 = type_of_aux context hetype ugraph2 in *)
2380          eat_prods ~subst context hetype tlbody_and_type ugraph2
2381    | C.Appl _ -> raise (AssertFailure (lazy "Appl: no arguments"))
2382    | C.Const (uri,exp_named_subst) ->
2383        incr fdebug ;
2384        let ugraph1 =
2385          check_exp_named_subst ~logger ~subst  context exp_named_subst ugraph
2386        in
2387        let cty,ugraph2 = type_of_constant ~logger uri ugraph1 in
2388        let cty1 =
2389          CicSubstitution.subst_vars exp_named_subst cty
2390        in
2391          decr fdebug ;
2392          cty1,ugraph2
2393    | C.MutInd (uri,i,exp_named_subst) ->
2394       incr fdebug ;
2395        let ugraph1 =
2396          check_exp_named_subst ~logger  ~subst context exp_named_subst ugraph
2397        in
2398          (* TASSI: da me c'era anche questa, ma in CVS no *)
2399        let mty,ugraph2 = type_of_mutual_inductive_defs ~logger uri i ugraph1 in
2400          (* fine parte dubbia *)
2401        let cty =
2402          CicSubstitution.subst_vars exp_named_subst mty
2403        in
2404          decr fdebug ;
2405          cty,ugraph2
2406    | C.MutConstruct (uri,i,j,exp_named_subst) ->
2407        let ugraph1 =
2408          check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
2409        in
2410          (* TASSI: idem come sopra *)
2411        let mty,ugraph2 =
2412          type_of_mutual_inductive_constr ~logger uri i j ugraph1
2413        in
2414        let cty =
2415          CicSubstitution.subst_vars exp_named_subst mty
2416        in
2417          cty,ugraph2
2418    | C.MutCase (uri,i,outtype,term,pl) ->
2419       let outsort,ugraph1 = type_of_aux ~logger context outtype ugraph in
2420       let (need_dummy, k) =
2421       let rec guess_args context t =
2422         let outtype = CicReduction.whd ~subst context t in
2423           match outtype with
2424               C.Sort _ -> (true, 0)
2425             | C.Prod (name, s, t) ->
2426                 let (b, n) =
2427                   guess_args ((Some (name,(C.Decl s)))::context) t in
2428                   if n = 0 then
2429                   (* last prod before sort *)
2430                     match CicReduction.whd ~subst context s with
2431 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
2432                         C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
2433                           (false, 1)
2434 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
2435                       | C.Appl ((C.MutInd (uri',i',_)) :: _)
2436                           when U.eq uri' uri && i' = i -> (false, 1)
2437                       | _ -> (true, 1)
2438                   else
2439                     (b, n + 1)
2440             | _ ->
2441                 raise
2442                   (TypeCheckerFailure
2443                      (lazy (sprintf
2444                         "Malformed case analasys' output type %s"
2445                         (CicPp.ppterm outtype))))
2446       in
2447 (*
2448       let (parameters, arguments, exp_named_subst),ugraph2 =
2449         let ty,ugraph2 = type_of_aux context term ugraph1 in
2450           match R.whd ~subst context ty with
2451            (*CSC manca il caso dei CAST *)
2452 (*CSC: ma servono i parametri (uri,i)? Se si', perche' non serve anche il *)
2453 (*CSC: parametro exp_named_subst? Se no, perche' non li togliamo?         *)
2454 (*CSC: Hint: nella DTD servono per gli stylesheet.                        *)
2455               C.MutInd (uri',i',exp_named_subst) as typ ->
2456                 if U.eq uri uri' && i = i' then
2457                   ([],[],exp_named_subst),ugraph2
2458                 else
2459                   raise
2460                     (TypeCheckerFailure
2461                       (lazy (sprintf
2462                           ("Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}")
2463                           (CicPp.ppterm typ) (U.string_of_uri uri) i)))
2464             | C.Appl
2465                 ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
2466                 if U.eq uri uri' && i = i' then
2467                   let params,args =
2468                     split tl (List.length tl - k)
2469                   in (params,args,exp_named_subst),ugraph2
2470                 else
2471                   raise
2472                     (TypeCheckerFailure
2473                       (lazy (sprintf
2474                           ("Case analysys: analysed term type is %s, "^
2475                            "but is expected to be (an application of) "^
2476                            "%s#1/%d{_}")
2477                           (CicPp.ppterm typ') (U.string_of_uri uri) i)))
2478             | _ ->
2479                 raise
2480                   (TypeCheckerFailure
2481                     (lazy (sprintf
2482                         ("Case analysis: "^
2483                          "analysed term %s is not an inductive one")
2484                         (CicPp.ppterm term))))
2485 *)
2486       let (b, k) = guess_args context outsort in
2487           if not b then (b, k - 1) else (b, k) in
2488       let (parameters, arguments, exp_named_subst),ugraph2 =
2489         let ty,ugraph2 = type_of_aux ~logger context term ugraph1 in
2490         match R.whd ~subst context ty with
2491             C.MutInd (uri',i',exp_named_subst) as typ ->
2492               if U.eq uri uri' && i = i' then
2493                 ([],[],exp_named_subst),ugraph2
2494               else raise
2495                 (TypeCheckerFailure
2496                   (lazy (sprintf
2497                       ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}")
2498                       (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i)))
2499           | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) ->
2500               if U.eq uri uri' && i = i' then
2501                 let params,args =
2502                   split tl (List.length tl - k)
2503                 in (params,args,exp_named_subst),ugraph2
2504               else raise
2505                 (TypeCheckerFailure
2506                   (lazy (sprintf
2507                       ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}")
2508                       (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i)))
2509           | _ ->
2510               raise
2511                 (TypeCheckerFailure
2512                   (lazy (sprintf
2513                       "Case analysis: analysed term %s is not an inductive one"
2514                       (CicPp.ppterm term))))
2515       in
2516         (*
2517            let's control if the sort elimination is allowed:
2518            [(I q1 ... qr)|B]
2519         *)
2520       let sort_of_ind_type =
2521         if parameters = [] then
2522           C.MutInd (uri,i,exp_named_subst)
2523         else
2524           C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters)
2525       in
2526       let type_of_sort_of_ind_ty,ugraph3 =
2527         type_of_aux ~logger context sort_of_ind_type ugraph2 in
2528       let b,ugraph4 =
2529         check_allowed_sort_elimination ~subst ~metasenv ~logger  context uri i
2530           need_dummy sort_of_ind_type type_of_sort_of_ind_ty outsort ugraph3
2531       in
2532         if not b then
2533         raise
2534           (TypeCheckerFailure (lazy ("Case analysis: sort elimination not allowed")));
2535         (* let's check if the type of branches are right *)
2536       let parsno,constructorsno =
2537         let obj,_ =
2538           try
2539             CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
2540           with Not_found -> assert false
2541         in
2542         match obj with
2543             C.InductiveDefinition (il,_,parsno,_) ->
2544              let _,_,_,cl =
2545               try List.nth il i with Failure _ -> assert false
2546              in
2547               parsno, List.length cl
2548           | _ ->
2549               raise (TypeCheckerFailure
2550                 (lazy ("Unknown mutual inductive definition:" ^
2551                   UriManager.string_of_uri uri)))
2552       in
2553       if List.length pl <> constructorsno then
2554        raise (TypeCheckerFailure
2555         (lazy ("Wrong number of cases in case analysis"))) ;
2556       let (_,branches_ok,ugraph5) =
2557         List.fold_left
2558           (fun (j,b,ugraph) p ->
2559             if b then
2560               let cons =
2561                 if parameters = [] then
2562                   (C.MutConstruct (uri,i,j,exp_named_subst))
2563                 else
2564                   (C.Appl
2565                      (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
2566               in
2567               let ty_p,ugraph1 = type_of_aux ~logger context p ugraph in
2568               let ty_cons,ugraph3 = type_of_aux ~logger context cons ugraph1 in
2569               (* 2 is skipped *)
2570               let ty_branch =
2571                 type_of_branch ~subst context parsno need_dummy outtype cons
2572                   ty_cons in
2573               let b1,ugraph4 =
2574                 R.are_convertible
2575                   ~subst ~metasenv context ty_p ty_branch ugraph3
2576               in
2577 (* Debugging code
2578 if not b1 then
2579 begin
2580 prerr_endline ("\n!OUTTYPE= " ^ CicPp.ppterm outtype);
2581 prerr_endline ("!CONS= " ^ CicPp.ppterm cons);
2582 prerr_endline ("!TY_CONS= " ^ CicPp.ppterm ty_cons);
2583 prerr_endline ("#### " ^ CicPp.ppterm ty_p ^ "\n<==>\n" ^ CicPp.ppterm ty_branch);
2584 end;
2585 *)
2586               if not b1 then
2587                 debug_print (lazy
2588                   ("#### " ^ CicPp.ppterm ty_p ^
2589                   " <==> " ^ CicPp.ppterm ty_branch));
2590               (j + 1,b1,ugraph4)
2591             else
2592               (j,false,ugraph)
2593           ) (1,true,ugraph4) pl
2594          in
2595           if not branches_ok then
2596            raise
2597             (TypeCheckerFailure (lazy "Case analysys: wrong branch type"));
2598           let arguments' =
2599            if not need_dummy then outtype::arguments@[term]
2600            else outtype::arguments in
2601           let outtype =
2602            if need_dummy && arguments = [] then outtype
2603            else CicReduction.head_beta_reduce (C.Appl arguments')
2604           in
2605            outtype,ugraph5
2606    | C.Fix (i,fl) ->
2607       let types,kl,ugraph1,len =
2608         List.fold_left
2609           (fun (types,kl,ugraph,len) (n,k,ty,_) ->
2610             let _,ugraph1 = type_of_aux ~logger context ty ugraph in
2611              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
2612               k::kl,ugraph1,len+1)
2613           ) ([],[],ugraph,0) fl
2614       in
2615       let ugraph2 =
2616         List.fold_left
2617           (fun ugraph (name,x,ty,bo) ->
2618              let ty_bo,ugraph1 =
2619                type_of_aux ~logger (types@context) bo ugraph
2620              in
2621              let b,ugraph2 =
2622                R.are_convertible ~subst ~metasenv (types@context)
2623                  ty_bo (CicSubstitution.lift len ty) ugraph1 in
2624                if b then
2625                  begin
2626                    let (m, eaten, context') =
2627                      eat_lambdas ~subst (types @ context) (x + 1) bo
2628                    in
2629                      (*
2630                        let's control the guarded by
2631                        destructors conditions D{f,k,x,M}
2632                      *)
2633                      if not (guarded_by_destructors ~subst context' eaten
2634                                (len + eaten) kl 1 [] m) then
2635                        raise
2636                          (TypeCheckerFailure
2637                            (lazy ("Fix: not guarded by destructors")))
2638                      else
2639                        ugraph2
2640                  end
2641                else
2642                  raise (TypeCheckerFailure (lazy ("Fix: ill-typed bodies")))
2643           ) ugraph1 fl in
2644         (*CSC: controlli mancanti solo su D{f,k,x,M} *)
2645       let (_,_,ty,_) = List.nth fl i in
2646         ty,ugraph2
2647    | C.CoFix (i,fl) ->
2648        let types,ugraph1,len =
2649          List.fold_left
2650            (fun (l,ugraph,len) (n,ty,_) ->
2651               let _,ugraph1 =
2652                 type_of_aux ~logger context ty ugraph in
2653                 (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::l,
2654                  ugraph1,len+1)
2655            ) ([],ugraph,0) fl
2656        in
2657        let ugraph2 =
2658          List.fold_left
2659            (fun ugraph (_,ty,bo) ->
2660               let ty_bo,ugraph1 =
2661                 type_of_aux ~logger (types @ context) bo ugraph
2662               in
2663               let b,ugraph2 =
2664                 R.are_convertible ~subst ~metasenv (types @ context) ty_bo
2665                   (CicSubstitution.lift len ty) ugraph1
2666               in
2667                 if b then
2668                   begin
2669                     (* let's control that the returned type is coinductive *)
2670                     match returns_a_coinductive ~subst context ty with
2671                         None ->
2672                           raise
2673                           (TypeCheckerFailure
2674                             (lazy "CoFix: does not return a coinductive type"))
2675                       | Some uri ->
2676                           (*
2677                             let's control the guarded by constructors
2678                             conditions C{f,M}
2679                           *)
2680                           if not (guarded_by_constructors ~subst
2681                               (types @ context) 0 len false bo [] uri) then
2682                             raise
2683                               (TypeCheckerFailure
2684                                 (lazy "CoFix: not guarded by constructors"))
2685                           else
2686                           ugraph2
2687                   end
2688                 else
2689                   raise
2690                     (TypeCheckerFailure (lazy "CoFix: ill-typed bodies"))
2691            ) ugraph1 fl
2692        in
2693        let (_,ty,_) = List.nth fl i in
2694          ty,ugraph2
2695
2696 *)
2697 ;;
2698
2699 (* typechecks the object, raising an exception if illtyped *)
2700 let typecheck_obj obj = match obj with _ -> ()