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