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 (* web interface stuff *)
  15
  16 let logger =
  17   ref (function (`Start_type_checking _|`Type_checking_completed _) -> ())
  18 ;;
  19
  20 let set_logger f = logger := f;;
  21
  22 exception TypeCheckerFailure of string Lazy.t
  23 exception AssertFailure of string Lazy.t
  24
  25 type recf_entry =
  26   | Evil of int (* rno *)
  27   | UnfFix of bool list (* fixed arguments *)
  28   | Safe
  29 ;;
  30
  31 let is_dangerous i l =
  32   List.exists (function (j,Evil _) when j=i -> true | _ -> false) l
  33 ;;
  34
  35 let is_unfolded i l =
  36   List.exists (function (j,UnfFix _) when j=i -> true | _ -> false) l
  37 ;;
  38
  39 let is_safe i l =
  40   List.exists (function (j,Safe) when j=i -> true | _ -> false) l
  41 ;;
  42
  43 let get_recno i l =
  44   try match List.assoc i l with Evil rno -> rno | _ -> assert false
  45   with Not_found -> assert false
  46 ;;
  47
  48 let get_fixed_args i l =
  49   try match List.assoc i l with UnfFix fa -> fa | _ -> assert false
  50   with Not_found -> assert false
  51 ;;
  52
  53 let shift_k e (c,rf,x) = e::c,List.map (fun (k,v) -> k+1,v) rf,x+1;;
  54
  55 let string_of_recfuns ~subst ~metasenv ~context l =
  56   let pp = NCicPp.ppterm ~subst ~metasenv ~context in
  57   let safe, rest = List.partition (function (_,Safe) -> true | _ -> false) l in
  58   let dang, unf = List.partition (function (_,UnfFix _) -> false | _->true)rest in
  59   "\n\tsafes: "^String.concat "," (List.map (fun (i,_)->pp (NCic.Rel i)) safe) ^
  60   "\n\tfix  : "^String.concat ","
  61    (List.map
  62      (function (i,UnfFix l)-> pp(NCic.Rel i)^"/"^String.concat "," (List.map
  63        string_of_bool l)
  64      | _ ->assert false) unf) ^
  65   "\n\trec  : "^String.concat ","
  66    (List.map
  67      (function (i,Evil rno)->pp(NCic.Rel i)^"/"^string_of_int rno
  68      | _ -> assert false) dang)
  69 ;;
  70
  71 let fixed_args bos j n nn =
  72  let rec aux k acc = function
  73   | NCic.Appl (NCic.Rel i::args) when i-k > n && i-k <= nn ->
  74      let rec combine l1 l2 =
  75       match l1,l2 with
  76          [],[] -> []
  77        | he1::tl1, he2::tl2 -> (he1,he2)::combine tl1 tl2
  78        | he::tl, [] -> (false,NCic.Rel ~-1)::combine tl [] (* dummy term *)
  79        | [],_::_ -> assert false
  80      in
  81      let lefts, _ = HExtlib.split_nth (min j (List.length args)) args in
  82       List.map (fun ((b,x),i) -> b && x = NCic.Rel (k-i))
  83        (HExtlib.list_mapi (fun x i -> x,i) (combine acc lefts))
  84   | t -> NCicUtils.fold (fun _ k -> k+1) k aux acc t
  85  in
  86   List.fold_left (aux 0)
  87    (let rec f = function 0 -> [] | n -> true :: f (n-1) in f j) bos
  88 ;;
  89
  90 let rec list_iter_default2 f l1 def l2 =
  91   match l1,l2 with
  92     | [], _ -> ()
  93     | a::ta, b::tb -> f a b; list_iter_default2 f ta def tb
  94     | a::ta, [] -> f a def; list_iter_default2 f ta def []
  95 ;;
  96
  97
  98 (*
  99 (* the boolean h means already protected *)
 100 (* args is the list of arguments the type of the constructor that may be *)
 101 (* found in head position must be applied to.                            *)
 102 and guarded_by_constructors ~subst context n nn h te args coInductiveTypeURI =
 103  let module C = Cic in
 104   (*CSC: There is a lot of code replication between the cases X and    *)
 105   (*CSC: (C.Appl X tl). Maybe it will be better to define a function   *)
 106   (*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *)
 107   match CicReduction.whd ~subst context te with
 108      C.Rel m when m > n && m <= nn -> h
 109    | C.Rel _ -> true
 110    | C.Meta _
 111    | C.Sort _
 112    | C.Implicit _
 113    | C.Cast _
 114    | C.Prod _
 115    | C.LetIn _ ->
 116       (* the term has just been type-checked *)
 117       raise (AssertFailure (lazy "17"))
 118    | C.Lambda (name,so,de) ->
 119       does_not_occur ~subst context n nn so &&
 120        guarded_by_constructors ~subst ((Some (name,(C.Decl so)))::context)
 121         (n + 1) (nn + 1) h de args coInductiveTypeURI
 122    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
 123       h &&
 124        List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) tl true
 125    | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) ->
 126       let consty =
 127         let obj,_ =
 128           try
 129             CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
 130           with Not_found -> assert false
 131         in
 132        match obj with
 133           C.InductiveDefinition (itl,_,_,_) ->
 134            let (_,_,_,cl) = List.nth itl i in
 135             let (_,cons) = List.nth cl (j - 1) in
 136              CicSubstitution.subst_vars exp_named_subst cons
 137         | _ ->
 138             raise (TypeCheckerFailure
 139              (lazy ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri)))
 140       in
 141        let rec analyse_branch context ty te =
 142         match CicReduction.whd ~subst context ty with
 143            C.Meta _ -> raise (AssertFailure (lazy "34"))
 144          | C.Rel _
 145          | C.Var _
 146          | C.Sort _ ->
 147             does_not_occur ~subst context n nn te
 148          | C.Implicit _
 149          | C.Cast _ ->
 150             raise (AssertFailure (lazy "24"))(* due to type-checking *)
 151          | C.Prod (name,so,de) ->
 152             analyse_branch ((Some (name,(C.Decl so)))::context) de te
 153          | C.Lambda _
 154          | C.LetIn _ ->
 155             raise (AssertFailure (lazy "25"))(* due to type-checking *)
 156          | C.Appl ((C.MutInd (uri,_,_))::_) when uri == coInductiveTypeURI ->
 157              guarded_by_constructors ~subst context n nn true te []
 158               coInductiveTypeURI
 159          | C.Appl ((C.MutInd (uri,_,_))::_) ->
 160             guarded_by_constructors ~subst context n nn true te tl
 161              coInductiveTypeURI
 162          | C.Appl _ ->
 163             does_not_occur ~subst context n nn te
 164          | C.Const _ -> raise (AssertFailure (lazy "26"))
 165          | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
 166             guarded_by_constructors ~subst context n nn true te []
 167              coInductiveTypeURI
 168          | C.MutInd _ ->
 169             does_not_occur ~subst context n nn te
 170          | C.MutConstruct _ -> raise (AssertFailure (lazy "27"))
 171          (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
 172          (*CSC: in head position.                                       *)
 173          | C.MutCase _
 174          | C.Fix _
 175          | C.CoFix _ ->
 176             raise (AssertFailure (lazy "28"))(* due to type-checking *)
 177        in
 178        let rec analyse_instantiated_type context ty l =
 179         match CicReduction.whd ~subst context ty with
 180            C.Rel _
 181          | C.Var _
 182          | C.Meta _
 183          | C.Sort _
 184          | C.Implicit _
 185          | C.Cast _ -> raise (AssertFailure (lazy "29"))(* due to type-checking *)
 186          | C.Prod (name,so,de) ->
 187             begin
 188              match l with
 189                 [] -> true
 190               | he::tl ->
 191                  analyse_branch context so he &&
 192                   analyse_instantiated_type
 193                    ((Some (name,(C.Decl so)))::context) de tl
 194             end
 195          | C.Lambda _
 196          | C.LetIn _ ->
 197             raise (AssertFailure (lazy "30"))(* due to type-checking *)
 198          | C.Appl _ ->
 199             List.fold_left
 200              (fun i x -> i && does_not_occur ~subst context n nn x) true l
 201          | C.Const _ -> raise (AssertFailure (lazy "31"))
 202          | C.MutInd _ ->
 203             List.fold_left
 204              (fun i x -> i && does_not_occur ~subst context n nn x) true l
 205          | C.MutConstruct _ -> raise (AssertFailure (lazy "32"))
 206          (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
 207          (*CSC: in head position.                                       *)
 208          | C.MutCase _
 209          | C.Fix _
 210          | C.CoFix _ ->
 211             raise (AssertFailure (lazy "33"))(* due to type-checking *)
 212        in
 213         let rec instantiate_type args consty =
 214          function
 215             [] -> true
 216           | tlhe::tltl as l ->
 217              let consty' = CicReduction.whd ~subst context consty in
 218               match args with
 219                  he::tl ->
 220                   begin
 221                    match consty' with
 222                       C.Prod (_,_,de) ->
 223                        let instantiated_de = CicSubstitution.subst he de in
 224                         (*CSC: siamo sicuri che non sia troppo forte? *)
 225                         does_not_occur ~subst context n nn tlhe &
 226                          instantiate_type tl instantiated_de tltl
 227                     | _ ->
 228                       (*CSC:We do not consider backbones with a MutCase, a    *)
 229                       (*CSC:FixPoint, a CoFixPoint and so on in head position.*)
 230                       raise (AssertFailure (lazy "23"))
 231                   end
 232                | [] -> analyse_instantiated_type context consty' l
 233                   (* These are all the other cases *)
 234        in
 235         instantiate_type args consty tl
 236    | C.Appl ((C.CoFix (_,fl))::tl) ->
 237       List.fold_left (fun i x -> i && does_not_occur ~subst context n nn x) true tl &&
 238        let len = List.length fl in
 239         let n_plus_len = n + len
 240         and nn_plus_len = nn + len
 241         (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
 242         and tys,_ =
 243           List.fold_left
 244             (fun (types,len) (n,ty,_) ->
 245                (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
 246                 len+1)
 247             ) ([],0) fl
 248         in
 249          List.fold_right
 250           (fun (_,ty,bo) i ->
 251             i && does_not_occur ~subst context n nn ty &&
 252              guarded_by_constructors ~subst (tys@context) n_plus_len nn_plus_len
 253               h bo args coInductiveTypeURI
 254           ) fl true
 255    | C.Appl ((C.MutCase (_,_,out,te,pl))::tl) ->
 256        List.fold_left (fun i x -> i && does_not_occur ~subst context n nn x) true tl &&
 257         does_not_occur ~subst context n nn out &&
 258          does_not_occur ~subst context n nn te &&
 259           List.fold_right
 260            (fun x i ->
 261              i &&
 262              guarded_by_constructors ~subst context n nn h x args
 263               coInductiveTypeURI
 264            ) pl true
 265    | C.Appl l ->
 266       List.fold_right (fun x i -> i && does_not_occur ~subst context n nn x) l true
 267    | C.Var (_,exp_named_subst)
 268    | C.Const (_,exp_named_subst) ->
 269       List.fold_right
 270        (fun (_,x) i -> i && does_not_occur ~subst context n nn x) exp_named_subst true
 271    | C.MutInd _ -> assert false
 272    | C.MutConstruct (_,_,_,exp_named_subst) ->
 273       List.fold_right
 274        (fun (_,x) i -> i && does_not_occur ~subst context n nn x) exp_named_subst true
 275    | C.MutCase (_,_,out,te,pl) ->
 276        does_not_occur ~subst context n nn out &&
 277         does_not_occur ~subst context n nn te &&
 278          List.fold_right
 279           (fun x i ->
 280             i &&
 281              guarded_by_constructors ~subst context n nn h x args
 282               coInductiveTypeURI
 283           ) pl true
 284    | C.Fix (_,fl) ->
 285       let len = List.length fl in
 286        let n_plus_len = n + len
 287        and nn_plus_len = nn + len
 288        (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
 289        and tys,_ =
 290         List.fold_left
 291           (fun (types,len) (n,_,ty,_) ->
 292              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
 293               len+1)
 294           ) ([],0) fl
 295        in
 296         List.fold_right
 297          (fun (_,_,ty,bo) i ->
 298            i && does_not_occur ~subst context n nn ty &&
 299             does_not_occur ~subst (tys@context) n_plus_len nn_plus_len bo
 300          ) fl true
 301    | C.CoFix (_,fl) ->
 302       let len = List.length fl in
 303        let n_plus_len = n + len
 304        and nn_plus_len = nn + len
 305        (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
 306        and tys,_ =
 307         List.fold_left
 308           (fun (types,len) (n,ty,_) ->
 309              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
 310               len+1)
 311           ) ([],0) fl
 312        in
 313         List.fold_right
 314          (fun (_,ty,bo) i ->
 315            i && does_not_occur ~subst context n nn ty &&
 316             guarded_by_constructors ~subst (tys@context) n_plus_len nn_plus_len
 317              h bo
 318              args coInductiveTypeURI
 319          ) fl true
 320
 321  in
 322   type_of_aux ~logger context t ugraph
 323
 324 ;;
 325
 326 (** wrappers which instantiate fresh loggers *)
 327
 328 (* check_allowed_sort_elimination uri i s1 s2
 329    This function is used outside the kernel to determine in advance whether
 330    a MutCase will be allowed or not.
 331    [uri,i] is the type of the term to match
 332    [s1] is the sort of the term to eliminate (i.e. the head of the arity
 333         of the inductive type [uri,i])
 334    [s2] is the sort of the goal (i.e. the head of the type of the outtype
 335         of the MutCase) *)
 336 let check_allowed_sort_elimination uri i s1 s2 =
 337  fst (check_allowed_sort_elimination ~subst:[] ~metasenv:[]
 338   ~logger:(new CicLogger.logger) [] uri i true
 339   (Cic.Implicit None) (* never used *) (Cic.Sort s1) (Cic.Sort s2)
 340   CicUniv.empty_ugraph)
 341 ;;
 342
 343 Deannotate.type_of_aux' := fun context t -> fst (type_of_aux' [] context t CicUniv.oblivion_ugraph);;
 344
 345 *)
 346
 347 module C = NCic
 348 module R = NCicReduction
 349 module Ref = NReference
 350 module S = NCicSubstitution
 351 module U = NCicUtils
 352 module E = NCicEnvironment
 353
 354 let rec split_prods ~subst context n te =
 355   match (n, R.whd ~subst context te) with
 356    | (0, _) -> context,te
 357    | (n, C.Prod (name,so,ta)) when n > 0 ->
 358        split_prods ~subst ((name,(C.Decl so))::context) (n - 1) ta
 359    | (_, _) -> raise (AssertFailure (lazy "split_prods"))
 360 ;;
 361
 362 let debruijn ?(cb=fun _ _ -> ()) uri number_of_types context =
 363  let rec aux k t =
 364   let res =
 365    match t with
 366     | C.Meta (i,(s,C.Ctx l)) ->
 367        let l1 = NCicUtils.sharing_map (aux (k-s)) l in
 368        if l1 == l then t else C.Meta (i,(s,C.Ctx l1))
 369     | C.Meta _ -> t
 370     | C.Const (Ref.Ref (_,uri1,(Ref.Fix (no,_) | Ref.CoFix no)))
 371     | C.Const (Ref.Ref (_,uri1,Ref.Ind no)) when NUri.eq uri uri1 ->
 372        C.Rel (k + number_of_types - no)
 373     | t -> NCicUtils.map (fun _ k -> k+1) k aux t
 374   in
 375    cb t res; res
 376  in
 377   aux (List.length context)
 378 ;;
 379
 380 let sort_of_prod ~metasenv ~subst context (name,s) (t1, t2) =
 381    let t1 = R.whd ~subst context t1 in
 382    let t2 = R.whd ~subst ((name,C.Decl s)::context) t2 in
 383    match t1, t2 with
 384    | C.Sort s1, C.Sort C.Prop -> t2
 385    | C.Sort (C.Type u1), C.Sort (C.Type u2) -> C.Sort (C.Type (max u1 u2))
 386    | C.Sort _,C.Sort (C.Type _) -> t2
 387    | C.Sort (C.Type _) , C.Sort C.CProp -> t1
 388    | C.Sort _, C.Sort C.CProp -> t2
 389    | C.Meta _, C.Sort _
 390    | C.Meta _, C.Meta _
 391    | C.Sort _, C.Meta _ when U.is_closed t2 -> t2
 392    | _ ->
 393       raise (TypeCheckerFailure (lazy (Printf.sprintf
 394         "Prod: expected two sorts, found = %s, %s"
 395          (NCicPp.ppterm ~subst ~metasenv ~context t1)
 396          (NCicPp.ppterm ~subst ~metasenv ~context t2))))
 397 ;;
 398
 399 let eat_prods ~subst ~metasenv context he ty_he args_with_ty =
 400   let rec aux ty_he = function
 401   | [] -> ty_he
 402   | (arg, ty_arg)::tl ->
 403       match R.whd ~subst context ty_he with
 404       | C.Prod (n,s,t) ->
 405 (*
 406           prerr_endline (NCicPp.ppterm ~subst ~metasenv ~context s ^ " - Vs - "
 407           ^ NCicPp.ppterm ~subst ~metasenv
 408           ~context ty_arg);
 409           prerr_endline (NCicPp.ppterm ~subst ~metasenv ~context (S.subst ~avoid_beta_redexes:true arg t));
 410 *)
 411           if R.are_convertible ~subst ~metasenv context ty_arg s then
 412             aux (S.subst ~avoid_beta_redexes:true arg t) tl
 413           else
 414             raise
 415               (TypeCheckerFailure
 416                 (lazy (Printf.sprintf
 417                   ("Appl: wrong application of %s: the parameter %s has type"^^
 418                    "\n%s\nbut it should have type \n%s\nContext:\n%s\n")
 419                   (NCicPp.ppterm ~subst ~metasenv ~context he)
 420                   (NCicPp.ppterm ~subst ~metasenv ~context arg)
 421                   (NCicPp.ppterm ~subst ~metasenv ~context ty_arg)
 422                   (NCicPp.ppterm ~subst ~metasenv ~context s)
 423                   (NCicPp.ppcontext ~subst ~metasenv context))))
 424        | _ ->
 425           raise
 426             (TypeCheckerFailure
 427               (lazy (Printf.sprintf
 428                 "Appl: %s is not a function, it cannot be applied"
 429                 (NCicPp.ppterm ~subst ~metasenv ~context
 430                  (let res = List.length tl in
 431                   let eaten = List.length args_with_ty - res in
 432                    (NCic.Appl
 433                     (he::List.map fst
 434                      (fst (HExtlib.split_nth eaten args_with_ty)))))))))
 435   in
 436     aux ty_he args_with_ty
 437 ;;
 438
 439 (* instantiate_parameters ps (x1:T1)...(xn:Tn)C                             *)
 440 (* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *)
 441 let rec instantiate_parameters params c =
 442   match c, params with
 443   | c,[] -> c
 444   | C.Prod (_,_,ta), he::tl -> instantiate_parameters tl (S.subst he ta)
 445   | t,l -> raise (AssertFailure (lazy "1"))
 446 ;;
 447
 448 let specialize_inductive_type ~subst context ty_term =
 449   match R.whd ~subst context ty_term with
 450   | C.Const (Ref.Ref (_,uri,Ref.Ind i) as ref)
 451   | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind i) as ref) :: _ ) as ty ->
 452       let args = match ty with C.Appl (_::tl) -> tl | _ -> [] in
 453       let is_ind, leftno, itl, attrs, i = E.get_checked_indtys ref in
 454       let left_args,_ = HExtlib.split_nth leftno args in
 455       let itl =
 456         List.map (fun (rel, name, arity, cl) ->
 457           let arity = instantiate_parameters left_args arity in
 458           let cl =
 459             List.map (fun (rel, name, ty) ->
 460               rel, name, instantiate_parameters left_args ty)
 461               cl
 462           in
 463             rel, name, arity, cl)
 464           itl
 465       in
 466         is_ind, leftno, itl, attrs, i
 467   | _ -> assert false
 468 ;;
 469
 470 let fix_lefts_in_constrs ~subst r_uri r_len context ty_term =
 471   let _,_,itl,_,i = specialize_inductive_type ~subst context ty_term in
 472   let _,_,_,cl = List.nth itl i in
 473   let cl =
 474     List.map (fun (_,id,ty) -> id, debruijn r_uri r_len context ty) cl
 475   in
 476   List.map (fun (_,name,arity,_) -> name, C.Decl arity) itl, cl
 477 ;;
 478
 479 exception DoesOccur;;
 480
 481 let does_not_occur ~subst context n nn t =
 482   let rec aux (context,n,nn as k) _ = function
 483     | C.Rel m when m > n && m <= nn -> raise DoesOccur
 484     | C.Rel m ->
 485         (try (match List.nth context (m-1) with
 486           | _,C.Def (bo,_) -> aux k () (S.lift m bo)
 487           | _ -> ())
 488          with Failure _ -> assert false)
 489     | C.Meta (_,(_,(C.Irl 0 | C.Ctx []))) -> (* closed meta *) ()
 490     | C.Meta (mno,(s,l)) ->
 491          (try
 492            let _,_,term,_ = U.lookup_subst mno subst in
 493            aux (context,n+s,nn+s) () (S.subst_meta (0,l) term)
 494           with CicUtil.Subst_not_found _ -> match l with
 495           | C.Irl len -> if not (n >= s+len || s > nn) then raise DoesOccur
 496           | C.Ctx lc -> List.iter (aux (context,n+s,nn+s) ()) lc)
 497     | t -> U.fold (fun e (ctx,n,nn) -> (e::ctx,n+1,nn+1)) k aux () t
 498   in
 499    try aux (context,n,nn) () t; true
 500    with DoesOccur -> false
 501 ;;
 502
 503 (*CSC l'indice x dei tipi induttivi e' t.c. n < x <= nn *)
 504 (*CSC questa funzione e' simile alla are_all_occurrences_positive, ma fa *)
 505 (*CSC dei controlli leggermente diversi. Viene invocata solamente dalla  *)
 506 (*CSC strictly_positive                                                  *)
 507 (*CSC definizione (giusta???) tratta dalla mail di Hugo ;-)              *)
 508 let rec weakly_positive ~subst context n nn uri te =
 509 (*CSC: Che schifo! Bisogna capire meglio e trovare una soluzione ragionevole!*)
 510   let dummy = C.Sort (C.Type ~-1) in
 511   (*CSC: mettere in cicSubstitution *)
 512   let rec subst_inductive_type_with_dummy _ = function
 513     | C.Const (Ref.Ref (_,uri',Ref.Ind 0)) when NUri.eq uri' uri -> dummy
 514     | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind 0)))::tl)
 515         when NUri.eq uri' uri -> dummy
 516     | t -> U.map (fun _ x->x) () subst_inductive_type_with_dummy t
 517   in
 518   match R.whd context te with
 519    | C.Const (Ref.Ref (_,uri',Ref.Ind _))
 520    | C.Appl ((C.Const (Ref.Ref (_,uri',Ref.Ind _)))::_)
 521       when NUri.eq uri' uri -> true
 522    | C.Prod (name,source,dest) when
 523       does_not_occur ~subst ((name,C.Decl source)::context) 0 1 dest ->
 524        (* dummy abstraction, so we behave as in the anonimous case *)
 525        strictly_positive ~subst context n nn
 526         (subst_inductive_type_with_dummy () source) &&
 527        weakly_positive ~subst ((name,C.Decl source)::context)
 528         (n + 1) (nn + 1) uri dest
 529    | C.Prod (name,source,dest) ->
 530        does_not_occur ~subst context n nn
 531         (subst_inductive_type_with_dummy () source)&&
 532        weakly_positive ~subst ((name,C.Decl source)::context)
 533         (n + 1) (nn + 1) uri dest
 534    | _ ->
 535      raise (TypeCheckerFailure (lazy "Malformed inductive constructor type"))
 536
 537 and strictly_positive ~subst context n nn te =
 538   match R.whd context te with
 539    | t when does_not_occur ~subst context n nn t -> true
 540    | C.Rel _ -> true
 541    | C.Prod (name,so,ta) ->
 542       does_not_occur ~subst context n nn so &&
 543        strictly_positive ~subst ((name,C.Decl so)::context) (n+1) (nn+1) ta
 544    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
 545       List.for_all (does_not_occur ~subst context n nn) tl
 546    | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind i) as r)::tl) ->
 547       let _,paramsno,tyl,_,i = E.get_checked_indtys r in
 548       let _,name,ity,cl = List.nth tyl i in
 549       let ok = List.length tyl = 1 in
 550       let params, arguments = HExtlib.split_nth paramsno tl in
 551       let lifted_params = List.map (S.lift 1) params in
 552       let cl =
 553         List.map (fun (_,_,te) -> instantiate_parameters lifted_params te) cl
 554       in
 555       ok &&
 556       List.for_all (does_not_occur ~subst context n nn) arguments &&
 557       List.for_all
 558         (weakly_positive ~subst ((name,C.Decl ity)::context) (n+1) (nn+1) uri) cl
 559    | _ -> false
 560
 561 (* the inductive type indexes are s.t. n < x <= nn *)
 562 and are_all_occurrences_positive ~subst context uri indparamsno i n nn te =
 563   match R.whd context te with
 564   |  C.Appl ((C.Rel m)::tl) as reduct when m = i ->
 565       let last =
 566        List.fold_left
 567         (fun k x ->
 568           if k = 0 then 0
 569           else
 570            match R.whd context x with
 571            |  C.Rel m when m = n - (indparamsno - k) -> k - 1
 572            | y -> raise (TypeCheckerFailure (lazy
 573               ("Argument "^string_of_int (indparamsno - k + 1) ^ " (of " ^
 574               string_of_int indparamsno ^ " fixed) is not homogeneous in "^
 575               "appl:\n"^ NCicPp.ppterm ~context ~subst ~metasenv:[] reduct))))
 576         indparamsno tl
 577       in
 578        if last = 0 then
 579         List.for_all (does_not_occur ~subst context n nn) tl
 580        else
 581         raise (TypeCheckerFailure
 582          (lazy ("Non-positive occurence in mutual inductive definition(s) [2]"^
 583           NUri.string_of_uri uri)))
 584   | C.Rel m when m = i ->
 585       if indparamsno = 0 then
 586        true
 587       else
 588         raise (TypeCheckerFailure
 589          (lazy ("Non-positive occurence in mutual inductive definition(s) [3]"^
 590           NUri.string_of_uri uri)))
 591   | C.Prod (name,source,dest) when
 592       does_not_occur ~subst ((name,C.Decl source)::context) 0 1 dest ->
 593       strictly_positive ~subst context n nn source &&
 594        are_all_occurrences_positive ~subst
 595         ((name,C.Decl source)::context) uri indparamsno
 596         (i+1) (n + 1) (nn + 1) dest
 597    | C.Prod (name,source,dest) ->
 598        if not (does_not_occur ~subst context n nn source) then
 599          raise (TypeCheckerFailure (lazy ("Non-positive occurrence in "^
 600          NCicPp.ppterm ~context ~metasenv:[] ~subst te)));
 601        are_all_occurrences_positive ~subst ((name,C.Decl source)::context)
 602         uri indparamsno (i+1) (n + 1) (nn + 1) dest
 603    | _ ->
 604      raise
 605       (TypeCheckerFailure (lazy ("Malformed inductive constructor type " ^
 606         (NUri.string_of_uri uri))))
 607 ;;
 608
 609 exception NotGuarded of string Lazy.t;;
 610
 611 let rec typeof ~subst ~metasenv context term =
 612   let rec typeof_aux context =
 613     fun t -> (*prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);*)
 614     match t with
 615     | C.Rel n ->
 616        (try
 617          match List.nth context (n - 1) with
 618          | (_,C.Decl ty) -> S.lift n ty
 619          | (_,C.Def (_,ty)) -> S.lift n ty
 620         with Failure _ -> raise (TypeCheckerFailure (lazy "unbound variable")))
 621     | C.Sort (C.Type i) -> C.Sort (C.Type (i+1))
 622     | C.Sort s -> C.Sort (C.Type 0)
 623     | C.Implicit _ -> raise (AssertFailure (lazy "Implicit found"))
 624     | C.Meta (n,l) as t ->
 625        let canonical_ctx,ty =
 626         try
 627          let _,c,_,ty = U.lookup_subst n subst in c,ty
 628         with U.Subst_not_found _ -> try
 629          let _,_,c,ty = U.lookup_meta n metasenv in c,ty
 630         with U.Meta_not_found _ ->
 631          raise (AssertFailure (lazy (Printf.sprintf
 632           "%s not found" (NCicPp.ppterm ~subst ~metasenv ~context t))))
 633        in
 634         check_metasenv_consistency t ~subst ~metasenv context canonical_ctx l;
 635         S.subst_meta l ty
 636     | C.Const ref -> type_of_constant ref
 637     | C.Prod (name,s,t) ->
 638        let sort1 = typeof_aux context s in
 639        let sort2 = typeof_aux ((name,(C.Decl s))::context) t in
 640        sort_of_prod ~metasenv ~subst context (name,s) (sort1,sort2)
 641     | C.Lambda (n,s,t) ->
 642        let sort = typeof_aux context s in
 643        (match R.whd ~subst context sort with
 644        | C.Meta _ | C.Sort _ -> ()
 645        | _ ->
 646          raise
 647            (TypeCheckerFailure (lazy (Printf.sprintf
 648              ("Not well-typed lambda-abstraction: " ^^
 649              "the source %s should be a type; instead it is a term " ^^
 650              "of type %s") (NCicPp.ppterm ~subst ~metasenv ~context s)
 651              (NCicPp.ppterm ~subst ~metasenv ~context sort)))));
 652        let ty = typeof_aux ((n,(C.Decl s))::context) t in
 653          C.Prod (n,s,ty)
 654     | C.LetIn (n,ty,t,bo) ->
 655        let ty_t = typeof_aux context t in
 656        let _ = typeof_aux context ty in
 657        if not (R.are_convertible ~subst ~metasenv context ty ty_t) then
 658          raise
 659           (TypeCheckerFailure
 660             (lazy (Printf.sprintf
 661               "The type of %s is %s but it is expected to be %s"
 662                 (NCicPp.ppterm ~subst ~metasenv ~context t)
 663                 (NCicPp.ppterm ~subst ~metasenv ~context ty_t)
 664                 (NCicPp.ppterm ~subst ~metasenv ~context ty))))
 665        else
 666          let ty_bo = typeof_aux  ((n,C.Def (t,ty))::context) bo in
 667          S.subst ~avoid_beta_redexes:true t ty_bo
 668     | C.Appl (he::(_::_ as args)) ->
 669        let ty_he = typeof_aux context he in
 670        let args_with_ty = List.map (fun t -> t, typeof_aux context t) args in
 671 (*
 672        prerr_endline ("HEAD: " ^ NCicPp.ppterm ~subst ~metasenv ~context ty_he);
 673        prerr_endline ("TARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm
 674        ~subst ~metasenv ~context) (List.map snd args_with_ty)));
 675        prerr_endline ("ARGS: " ^ String.concat " | " (List.map (NCicPp.ppterm
 676        ~subst ~metasenv ~context) (List.map fst args_with_ty)));
 677 *)
 678        eat_prods ~subst ~metasenv context he ty_he args_with_ty
 679    | C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
 680    | C.Match (Ref.Ref (_,_,Ref.Ind tyno) as r,outtype,term,pl) ->
 681       let outsort = typeof_aux context outtype in
 682       let inductive,leftno,itl,_,_ = E.get_checked_indtys r in
 683       let constructorsno =
 684         let _,_,_,cl = List.nth itl tyno in List.length cl
 685       in
 686       let parameters, arguments =
 687         let ty = R.whd ~subst context (typeof_aux context term) in
 688         let r',tl =
 689          match ty with
 690             C.Const (Ref.Ref (_,_,Ref.Ind _) as r') -> r',[]
 691           | C.Appl (C.Const (Ref.Ref (_,_,Ref.Ind _) as r') :: tl) -> r',tl
 692           | _ ->
 693              raise
 694                (TypeCheckerFailure (lazy (Printf.sprintf
 695                  "Case analysis: analysed term %s is not an inductive one"
 696                  (NCicPp.ppterm ~subst ~metasenv ~context term)))) in
 697         if not (Ref.eq r r') then
 698          raise
 699           (TypeCheckerFailure (lazy (Printf.sprintf
 700             ("Case analysys: analysed term type is %s, but is expected " ^^
 701              "to be (an application of) %s")
 702             (NCicPp.ppterm ~subst ~metasenv ~context ty)
 703             (NCicPp.ppterm ~subst ~metasenv ~context (C.Const r')))))
 704         else
 705          try HExtlib.split_nth leftno tl
 706          with
 707           Failure _ ->
 708            raise (TypeCheckerFailure (lazy (Printf.sprintf
 709            "%s is partially applied"
 710            (NCicPp.ppterm  ~subst ~metasenv ~context ty)))) in
 711       (* let's control if the sort elimination is allowed: [(I q1 ... qr)|B] *)
 712       let sort_of_ind_type =
 713         if parameters = [] then C.Const r
 714         else C.Appl ((C.Const r)::parameters) in
 715       let type_of_sort_of_ind_ty = typeof_aux context sort_of_ind_type in
 716       check_allowed_sort_elimination ~subst ~metasenv r context
 717        sort_of_ind_type type_of_sort_of_ind_ty outsort;
 718       (* let's check if the type of branches are right *)
 719       if List.length pl <> constructorsno then
 720        raise (TypeCheckerFailure (lazy ("Wrong number of cases in a match")));
 721       let j,branches_ok,p_ty, exp_p_ty =
 722         List.fold_left
 723           (fun (j,b,old_p_ty,old_exp_p_ty) p ->
 724             if b then
 725               let cons =
 726                 let cons = Ref.mk_constructor j r in
 727                 if parameters = [] then C.Const cons
 728                 else C.Appl (C.Const cons::parameters)
 729               in
 730               let ty_p = typeof_aux context p in
 731               let ty_cons = typeof_aux context cons in
 732               let ty_branch =
 733                 type_of_branch ~subst context leftno outtype cons ty_cons 0
 734               in
 735               j+1, R.are_convertible ~subst ~metasenv context ty_p ty_branch,
 736               ty_p, ty_branch
 737             else
 738               j,false,old_p_ty,old_exp_p_ty
 739           ) (1,true,C.Sort C.Prop,C.Sort C.Prop) pl
 740       in
 741       if not branches_ok then
 742         raise
 743          (TypeCheckerFailure
 744           (lazy (Printf.sprintf ("Branch for constructor %s :=\n%s\n"^^
 745           "has type %s\nnot convertible with %s")
 746           (NCicPp.ppterm  ~subst ~metasenv ~context
 747             (C.Const (Ref.mk_constructor (j-1) r)))
 748           (NCicPp.ppterm ~metasenv ~subst ~context (List.nth pl (j-2)))
 749           (NCicPp.ppterm ~metasenv ~subst ~context p_ty)
 750           (NCicPp.ppterm ~metasenv ~subst ~context exp_p_ty))));
 751       let res = outtype::arguments@[term] in
 752       R.head_beta_reduce (C.Appl res)
 753     | C.Match _ -> assert false
 754
 755   and type_of_branch ~subst context leftno outty cons tycons liftno =
 756     match R.whd ~subst context tycons with
 757     | C.Const (Ref.Ref (_,_,Ref.Ind _)) -> C.Appl [S.lift liftno outty ; cons]
 758     | C.Appl (C.Const (Ref.Ref (_,_,Ref.Ind _))::tl) ->
 759         let _,arguments = HExtlib.split_nth leftno tl in
 760         C.Appl (S.lift liftno outty::arguments@[cons])
 761     | C.Prod (name,so,de) ->
 762         let cons =
 763          match S.lift 1 cons with
 764          | C.Appl l -> C.Appl (l@[C.Rel 1])
 765          | t -> C.Appl [t ; C.Rel 1]
 766         in
 767          C.Prod (name,so,
 768            type_of_branch ~subst ((name,(C.Decl so))::context)
 769             leftno outty cons de (liftno+1))
 770     | _ -> raise (AssertFailure (lazy "type_of_branch"))
 771
 772   (* check_metasenv_consistency checks that the "canonical" context of a
 773      metavariable is consitent - up to relocation via the relocation list l -
 774      with the actual context *)
 775   and check_metasenv_consistency
 776     ~subst ~metasenv term context canonical_context l
 777   =
 778    match l with
 779     | shift, NCic.Irl n ->
 780        let context = snd (HExtlib.split_nth shift context) in
 781         let rec compare = function
 782          | 0,_,[] -> ()
 783          | 0,_,_::_
 784          | _,_,[] ->
 785             raise (AssertFailure (lazy (Printf.sprintf
 786              "Local and canonical context %s have different lengths"
 787              (NCicPp.ppterm ~subst ~context ~metasenv term))))
 788          | m,[],_::_ ->
 789             raise (TypeCheckerFailure (lazy (Printf.sprintf
 790              "Unbound variable -%d in %s" m
 791              (NCicPp.ppterm ~subst ~metasenv ~context term))))
 792          | m,t::tl,ct::ctl ->
 793             (match t,ct with
 794                 (_,C.Decl t1), (_,C.Decl t2)
 795               | (_,C.Def (t1,_)), (_,C.Def (t2,_))
 796               | (_,C.Def (_,t1)), (_,C.Decl t2) ->
 797                  if not (R.are_convertible ~subst ~metasenv tl t1 t2) then
 798                   raise
 799                       (TypeCheckerFailure
 800                         (lazy (Printf.sprintf
 801                       ("Not well typed metavariable local context for %s: " ^^
 802                        "%s expected, which is not convertible with %s")
 803                       (NCicPp.ppterm ~subst ~metasenv ~context term)
 804                       (NCicPp.ppterm ~subst ~metasenv ~context t2)
 805                       (NCicPp.ppterm ~subst ~metasenv ~context t1))))
 806               | _,_ ->
 807                raise
 808                    (TypeCheckerFailure (lazy (Printf.sprintf
 809                     ("Not well typed metavariable local context for %s: " ^^
 810                      "a definition expected, but a declaration found")
 811                     (NCicPp.ppterm ~subst ~metasenv ~context term)))));
 812             compare (m - 1,tl,ctl)
 813         in
 814          compare (n,context,canonical_context)
 815     | shift, lc_kind ->
 816        (* we avoid useless lifting by shortening the context*)
 817        let l,context = (0,lc_kind), snd (HExtlib.split_nth shift context) in
 818        let lifted_canonical_context =
 819          let rec lift_metas i = function
 820            | [] -> []
 821            | (n,C.Decl t)::tl ->
 822                (n,C.Decl (S.subst_meta l (S.lift i t)))::(lift_metas (i+1) tl)
 823            | (n,C.Def (t,ty))::tl ->
 824                (n,C.Def ((S.subst_meta l (S.lift i t)),
 825                           S.subst_meta l (S.lift i ty)))::(lift_metas (i+1) tl)
 826          in
 827           lift_metas 1 canonical_context in
 828        let l = U.expand_local_context lc_kind in
 829        try
 830         List.iter2
 831         (fun t ct ->
 832           match (t,ct) with
 833           | t, (_,C.Def (ct,_)) ->
 834              (*CSC: the following optimization is to avoid a possibly expensive
 835                     reduction that can be easily avoided and that is quite
 836                     frequent. However, this is better handled using levels to
 837                     control reduction *)
 838              let optimized_t =
 839               match t with
 840               | C.Rel n ->
 841                   (try
 842                     match List.nth context (n - 1) with
 843                     | (_,C.Def (te,_)) -> S.lift n te
 844                     | _ -> t
 845                     with Failure _ -> t)
 846               | _ -> t
 847              in
 848              if not (R.are_convertible ~subst ~metasenv context optimized_t ct)
 849              then
 850                raise
 851                  (TypeCheckerFailure
 852                    (lazy (Printf.sprintf
 853                      ("Not well typed metavariable local context: " ^^
 854                       "expected a term convertible with %s, found %s")
 855                      (NCicPp.ppterm ~subst ~metasenv ~context ct)
 856                      (NCicPp.ppterm ~subst ~metasenv ~context t))))
 857           | t, (_,C.Decl ct) ->
 858               let type_t = typeof_aux context t in
 859               if not (R.are_convertible ~subst ~metasenv context type_t ct) then
 860                 raise (TypeCheckerFailure
 861                  (lazy (Printf.sprintf
 862                   ("Not well typed metavariable local context: "^^
 863                   "expected a term of type %s, found %s of type %s")
 864                   (NCicPp.ppterm ~subst ~metasenv ~context ct)
 865                   (NCicPp.ppterm ~subst ~metasenv ~context t)
 866                   (NCicPp.ppterm ~subst ~metasenv ~context type_t))))
 867         ) l lifted_canonical_context
 868        with
 869         Invalid_argument _ ->
 870           raise (AssertFailure (lazy (Printf.sprintf
 871            "Local and canonical context %s have different lengths"
 872            (NCicPp.ppterm ~subst ~metasenv ~context term))))
 873
 874   and is_non_informative context paramsno c =
 875    let rec aux context c =
 876      match R.whd context c with
 877       | C.Prod (n,so,de) ->
 878          let s = typeof_aux context so in
 879          s = C.Sort C.Prop && aux ((n,(C.Decl so))::context) de
 880       | _ -> true in
 881    let context',dx = split_prods ~subst:[] context paramsno c in
 882     aux context' dx
 883
 884   and check_allowed_sort_elimination ~subst ~metasenv r =
 885    let mkapp he arg =
 886      match he with
 887      | C.Appl l -> C.Appl (l @ [arg])
 888      | t -> C.Appl [t;arg] in
 889    let rec aux context ind arity1 arity2 =
 890     let arity1 = R.whd ~subst context arity1 in
 891     let arity2 = R.whd ~subst context arity2 in
 892       match arity1,arity2 with
 893        | C.Prod (name,so1,de1), C.Prod (_,so2,de2) ->
 894           if not (R.are_convertible ~subst ~metasenv context so1 so2) then
 895            raise (TypeCheckerFailure (lazy (Printf.sprintf
 896             "In outtype: expected %s, found %s"
 897             (NCicPp.ppterm ~subst ~metasenv ~context so1)
 898             (NCicPp.ppterm ~subst ~metasenv ~context so2)
 899             )));
 900           aux ((name, C.Decl so1)::context)
 901            (mkapp (S.lift 1 ind) (C.Rel 1)) de1 de2
 902        | C.Sort _, C.Prod (name,so,ta) ->
 903           if not (R.are_convertible ~subst ~metasenv context so ind) then
 904            raise (TypeCheckerFailure (lazy (Printf.sprintf
 905             "In outtype: expected %s, found %s"
 906             (NCicPp.ppterm ~subst ~metasenv ~context ind)
 907             (NCicPp.ppterm ~subst ~metasenv ~context so)
 908             )));
 909           (match arity1,ta with
 910             | (C.Sort (C.CProp | C.Type _), C.Sort _)
 911             | (C.Sort C.Prop, C.Sort C.Prop) -> ()
 912             | (C.Sort C.Prop, C.Sort (C.CProp | C.Type _)) ->
 913         (* TODO: we should pass all these parameters since we
 914          * have them already *)
 915                 let inductive,leftno,itl,_,i = E.get_checked_indtys r in
 916                 let itl_len = List.length itl in
 917                 let _,name,ty,cl = List.nth itl i in
 918                 let cl_len = List.length cl in
 919                  (* is it a singleton or empty non recursive and non informative
 920                     definition? *)
 921                  if not
 922                   (cl_len = 0 ||
 923                    (itl_len = 1 && cl_len = 1 &&
 924                     is_non_informative [name,C.Decl ty] leftno
 925                      (let _,_,x = List.nth cl 0 in x)))
 926                  then
 927                   raise (TypeCheckerFailure (lazy
 928                    ("Sort elimination not allowed")));
 929           | _,_ -> ())
 930        | _,_ -> ()
 931    in
 932     aux
 933
 934  in
 935    typeof_aux context term
 936
 937 and check_mutual_inductive_defs uri ~metasenv ~subst is_ind leftno tyl =
 938   (* let's check if the arity of the inductive types are well formed *)
 939   List.iter (fun (_,_,x,_) -> ignore (typeof ~subst ~metasenv [] x)) tyl;
 940   (* let's check if the types of the inductive constructors are well formed. *)
 941   let len = List.length tyl in
 942   let tys = List.rev (List.map (fun (_,n,ty,_) -> (n,(C.Decl ty))) tyl) in
 943   ignore
 944    (List.fold_right
 945     (fun (_,_,_,cl) i ->
 946        List.iter
 947          (fun (_,name,te) ->
 948            let debruijnedte = debruijn uri len [] te in
 949            ignore (typeof ~subst ~metasenv tys debruijnedte);
 950            (* let's check also the positivity conditions *)
 951            if
 952              not
 953                (are_all_occurrences_positive ~subst tys uri leftno i 0 len
 954                   debruijnedte)
 955            then
 956              raise
 957                (TypeCheckerFailure
 958                  (lazy ("Non positive occurence in "^NUri.string_of_uri uri))))
 959          cl;
 960         i + 1)
 961     tyl 1)
 962
 963 and eat_lambdas ~subst ~metasenv context n te =
 964   match (n, R.whd ~subst context te) with
 965   | (0, _) -> (te, context)
 966   | (n, C.Lambda (name,so,ta)) when n > 0 ->
 967       eat_lambdas ~subst ~metasenv ((name,(C.Decl so))::context) (n - 1) ta
 968    | (n, te) ->
 969       raise (AssertFailure (lazy (Printf.sprintf "eat_lambdas (%d, %s)" n
 970         (NCicPp.ppterm ~subst ~metasenv ~context te))))
 971
 972 and eat_or_subst_lambdas ~subst ~metasenv n te to_be_subst args
 973      (context, recfuns, x as k)
 974 =
 975   match n, R.whd ~subst context te, to_be_subst, args with
 976   | (n, C.Lambda (name,so,ta),true::to_be_subst,arg::args) when n > 0 ->
 977       eat_or_subst_lambdas ~subst ~metasenv (n - 1) (S.subst arg ta)
 978        to_be_subst args k
 979   | (n, C.Lambda (name,so,ta),false::to_be_subst,arg::args) when n > 0 ->
 980       eat_or_subst_lambdas ~subst ~metasenv (n - 1) ta to_be_subst args
 981        (shift_k (name,(C.Decl so)) k)
 982   | (_, te, _, _) -> te, k
 983
 984 and guarded_by_destructors r_uri r_len ~subst ~metasenv context recfuns t =
 985  let recursor f k t = NCicUtils.fold shift_k k (fun k () -> f k) () t in
 986  let rec aux (context, recfuns, x as k) t =
 987   let t = R.whd ~delta:max_int ~subst context t in
 988 (*
 989    prerr_endline ("GB:\n" ^
 990      NCicPp.ppcontext ~subst ~metasenv context^
 991      NCicPp.ppterm ~metasenv ~subst ~context t^
 992        string_of_recfuns ~subst ~metasenv ~context recfuns);
 993 *)
 994   try
 995   match t with
 996   | C.Rel m as t when is_dangerous m recfuns ->
 997       raise (NotGuarded (lazy
 998         (NCicPp.ppterm ~subst ~metasenv ~context t ^
 999          " is a partial application of a fix")))
1000   | C.Appl ((C.Rel m)::tl) as t when is_dangerous m recfuns ->
1001      let rec_no = get_recno m recfuns in
1002      if not (List.length tl > rec_no) then
1003        raise (NotGuarded (lazy
1004          (NCicPp.ppterm ~context ~subst ~metasenv t ^
1005          " is a partial application of a fix")))
1006      else
1007        let rec_arg = List.nth tl rec_no in
1008        if not (is_really_smaller r_uri r_len ~subst ~metasenv k rec_arg) then
1009          raise (NotGuarded (lazy (Printf.sprintf ("Recursive call %s, %s is not"
1010           ^^ " smaller.\ncontext:\n%s") (NCicPp.ppterm ~context ~subst ~metasenv
1011           t) (NCicPp.ppterm ~context ~subst ~metasenv rec_arg)
1012           (NCicPp.ppcontext ~subst ~metasenv context))));
1013        List.iter (aux k) tl
1014   | C.Appl ((C.Rel m)::tl) when is_unfolded m recfuns ->
1015        let fixed_args = get_fixed_args m recfuns in
1016        list_iter_default2 (fun x b -> if not b then aux k x) tl false fixed_args
1017   | C.Rel m ->
1018      (match List.nth context (m-1) with
1019      | _,C.Decl _ -> ()
1020      | _,C.Def (bo,_) -> aux k (S.lift m bo))
1021   | C.Meta _ -> ()
1022   | C.Appl (C.Const ((Ref.Ref (_,uri,Ref.Fix (i,recno))) as r)::args) ->
1023       if List.exists (fun t -> try aux k t;false with NotGuarded _ -> true) args
1024       then
1025       let fl,_,_ = E.get_checked_fixes r in
1026       let ctx_tys, bos =
1027         List.split (List.map (fun (_,name,_,ty,bo) -> (name, C.Decl ty), bo) fl)
1028       in
1029       let fl_len = List.length fl in
1030       let bos = List.map (debruijn uri fl_len context) bos in
1031       let j = List.fold_left min max_int (List.map (fun (_,_,i,_,_)->i) fl) in
1032       let ctx_len = List.length context in
1033         (* we may look for fixed params not only up to j ... *)
1034       let fa = fixed_args bos j ctx_len (ctx_len + fl_len) in
1035       list_iter_default2 (fun x b -> if not b then aux k x) args false fa;
1036       let context = context@ctx_tys in
1037       let ctx_len = List.length context in
1038       let extra_recfuns =
1039         HExtlib.list_mapi (fun _ i -> ctx_len - i, UnfFix fa) ctx_tys
1040       in
1041       let new_k = context, extra_recfuns@recfuns, x in
1042       let bos_and_ks =
1043         HExtlib.list_mapi
1044          (fun bo fno ->
1045           let bo_and_k =
1046             eat_or_subst_lambdas ~subst ~metasenv j bo fa args new_k
1047           in
1048            if
1049             fno = i &&
1050             List.length args > recno &&
1051             (*case where the recursive argument is already really_smaller *)
1052             is_really_smaller r_uri r_len ~subst ~metasenv k
1053              (List.nth args recno)
1054            then
1055             let bo,(context, _, _ as new_k) = bo_and_k in
1056             let bo, context' =
1057              eat_lambdas ~subst ~metasenv context (recno + 1 - j) bo in
1058             let new_context_part,_ =
1059              HExtlib.split_nth (List.length context' - List.length context)
1060               context' in
1061             let k = List.fold_right shift_k new_context_part new_k in
1062             let context, recfuns, x = k in
1063             let k = context, (1,Safe)::recfuns, x in
1064               bo,k
1065            else
1066             bo_and_k
1067          ) bos
1068       in
1069        List.iter (fun (bo,k) -> aux k bo) bos_and_ks
1070   | C.Match (Ref.Ref (_,uri,_) as ref,outtype,term,pl) as t ->
1071      (match R.whd ~subst context term with
1072      | C.Rel m | C.Appl (C.Rel m :: _ ) as t when is_safe m recfuns || m = x ->
1073         (* TODO: add CoInd to references so that this call is useless *)
1074         let isinductive, _, _, _, _ = E.get_checked_indtys ref in
1075         if not isinductive then recursor aux k t
1076         else
1077          let ty = typeof ~subst ~metasenv context term in
1078          let itl_ctx,dcl = fix_lefts_in_constrs ~subst r_uri r_len context ty in
1079          let args = match t with C.Appl (_::tl) -> tl | _ -> [] in
1080          let dc_ctx = context @ itl_ctx in
1081          let start, stop = List.length context, List.length context + r_len in
1082          aux k outtype;
1083          List.iter (aux k) args;
1084          List.iter2
1085            (fun p (_,dc) ->
1086              let rl = recursive_args ~subst ~metasenv dc_ctx start stop dc in
1087              let p, k = get_new_safes ~subst k p rl in
1088              aux k p)
1089            pl dcl
1090      | _ -> recursor aux k t)
1091   | t -> recursor aux k t
1092   with
1093    NotGuarded _ as exc ->
1094     let t' = R.whd ~delta:0 ~subst context t in
1095     if t = t' then raise exc
1096     else aux k t'
1097  in
1098   try aux (context, recfuns, 1) t
1099   with NotGuarded s -> raise (TypeCheckerFailure s)
1100
1101 (*
1102  | C.Fix (_, fl) ->
1103     let len = List.length fl in
1104      let n_plus_len = n + len
1105      and nn_plus_len = nn + len
1106      and x_plus_len = x + len
1107      and tys,_ =
1108       List.fold_left
1109         (fun (types,len) (n,_,ty,_) ->
1110            (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
1111             len+1)
1112         ) ([],0) fl
1113      and safes' = List.map (fun x -> x + len) safes in
1114       List.fold_right
1115        (fun (_,_,ty,bo) i ->
1116          i && guarded_by_destructors ~subst context n nn kl x_plus_len safes' ty &&
1117           guarded_by_destructors ~subst (tys@context) n_plus_len nn_plus_len kl
1118            x_plus_len safes' bo
1119        ) fl true
1120  | C.CoFix (_, fl) ->
1121     let len = List.length fl in
1122      let n_plus_len = n + len
1123      and nn_plus_len = nn + len
1124      and x_plus_len = x + len
1125      and tys,_ =
1126       List.fold_left
1127         (fun (types,len) (n,ty,_) ->
1128            (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
1129             len+1)
1130         ) ([],0) fl
1131      and safes' = List.map (fun x -> x + len) safes in
1132       List.fold_right
1133        (fun (_,ty,bo) i ->
1134          i &&
1135           guarded_by_destructors ~subst context n nn kl x_plus_len safes' ty &&
1136           guarded_by_destructors ~subst (tys@context) n_plus_len nn_plus_len kl
1137            x_plus_len safes' bo
1138        ) fl true
1139 *)
1140
1141 and guarded_by_constructors ~subst ~metasenv _ _ _ _ _ _ _ = true
1142
1143 and recursive_args ~subst ~metasenv context n nn te =
1144   match R.whd context te with
1145   | C.Rel _ | C.Appl _ | C.Const _ -> []
1146   | C.Prod (name,so,de) ->
1147      (not (does_not_occur ~subst context n nn so)) ::
1148       (recursive_args ~subst ~metasenv
1149         ((name,(C.Decl so))::context) (n+1) (nn + 1) de)
1150   | t ->
1151      raise (AssertFailure (lazy ("recursive_args:" ^ NCicPp.ppterm ~subst
1152      ~metasenv ~context:[] t)))
1153
1154 and get_new_safes ~subst (context, recfuns, x as k) p rl =
1155   match R.whd ~subst context p, rl with
1156   | C.Lambda (name,so,ta), b::tl ->
1157       let recfuns = (if b then [0,Safe] else []) @ recfuns in
1158       get_new_safes ~subst
1159         (shift_k (name,(C.Decl so)) (context, recfuns, x)) ta tl
1160   | C.Meta _ as e, _ | e, [] -> e, k
1161   | _ -> raise (AssertFailure (lazy "Ill formed pattern"))
1162
1163 and split_prods ~subst context n te =
1164   match n, R.whd ~subst context te with
1165   | 0, _ -> context,te
1166   | n, C.Prod (name,so,ta) when n > 0 ->
1167        split_prods ~subst ((name,(C.Decl so))::context) (n - 1) ta
1168   | _ -> raise (AssertFailure (lazy "split_prods"))
1169
1170 and is_really_smaller
1171   r_uri r_len ~subst ~metasenv (context, recfuns, x as k) te
1172 =
1173  match R.whd ~subst context te with
1174  | C.Rel m when is_safe m recfuns -> true
1175  | C.Lambda (name, s, t) ->
1176     is_really_smaller r_uri r_len ~subst ~metasenv (shift_k (name,C.Decl s) k) t
1177  | C.Appl (he::_) ->
1178     is_really_smaller r_uri r_len ~subst ~metasenv k he
1179  | C.Appl _
1180  | C.Rel _
1181  | C.Const (Ref.Ref (_,_,Ref.Con _)) -> false
1182  | C.Const (Ref.Ref (_,_,Ref.Fix _)) -> assert false
1183    (*| C.Fix (_, fl) ->
1184       let len = List.length fl in
1185        let n_plus_len = n + len
1186        and nn_plus_len = nn + len
1187        and x_plus_len = x + len
1188        and tys,_ =
1189         List.fold_left
1190           (fun (types,len) (n,_,ty,_) ->
1191              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
1192               len+1)
1193           ) ([],0) fl
1194        and safes' = List.map (fun x -> x + len) safes in
1195         List.fold_right
1196          (fun (_,_,ty,bo) i ->
1197            i &&
1198             is_really_smaller ~subst (tys@context) n_plus_len nn_plus_len kl
1199              x_plus_len safes' bo
1200          ) fl true*)
1201  | C.Meta _ -> true
1202  | C.Match (Ref.Ref (_,uri,_) as ref,outtype,term,pl) ->
1203     (match term with
1204     | C.Rel m | C.Appl (C.Rel m :: _ ) when is_safe m recfuns || m = x ->
1205         (* TODO: add CoInd to references so that this call is useless *)
1206         let isinductive, _, _, _, _ = E.get_checked_indtys ref in
1207         if not isinductive then
1208           List.for_all (is_really_smaller r_uri r_len ~subst ~metasenv k) pl
1209         else
1210           let ty = typeof ~subst ~metasenv context term in
1211           let itl_ctx,dcl= fix_lefts_in_constrs ~subst r_uri r_len context ty in
1212           let start, stop = List.length context, List.length context + r_len in
1213           let dc_ctx = context @ itl_ctx in
1214           List.for_all2
1215            (fun p (_,dc) ->
1216              let rl = recursive_args ~subst ~metasenv dc_ctx start stop dc in
1217              let e, k = get_new_safes ~subst k p rl in
1218              is_really_smaller r_uri r_len ~subst ~metasenv k e)
1219            pl dcl
1220     | _ -> List.for_all (is_really_smaller r_uri r_len ~subst ~metasenv k) pl)
1221  | _ -> assert false
1222
1223 and returns_a_coinductive ~subst context ty =
1224   match R.whd ~subst context ty with
1225   | C.Const (Ref.Ref (_,uri,Ref.Ind _) as ref)
1226   | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind _) as ref)::_) ->
1227      let isinductive, _, _, _, _ = E.get_checked_indtys ref in
1228      if isinductive then None else (Some uri)
1229   | C.Prod (n,so,de) ->
1230      returns_a_coinductive ~subst ((n,C.Decl so)::context) de
1231   | _ -> None
1232
1233 and type_of_constant ((Ref.Ref (_,uri,_)) as ref) =
1234   let cobj =
1235     match E.get_obj uri with
1236     | true, cobj -> cobj
1237     | false, uobj ->
1238        !logger (`Start_type_checking uri);
1239        check_obj_well_typed uobj;
1240        E.add_obj uobj;
1241        !logger (`Type_checking_completed uri);
1242        uobj
1243   in
1244   match cobj, ref with
1245   | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,_,Ref.Ind i)  ->
1246       let _,_,arity,_ = List.nth tl i in arity
1247   | (_,_,_,_,C.Inductive (_,_,tl,_)), Ref.Ref (_,_,Ref.Con (i,j))  ->
1248       let _,_,_,cl = List.nth tl i in
1249       let _,_,arity = List.nth cl (j-1) in
1250       arity
1251   | (_,_,_,_,C.Fixpoint (_,fl,_)), Ref.Ref (_,_,(Ref.Fix (i,_)|Ref.CoFix i)) ->
1252       let _,_,_,arity,_ = List.nth fl i in
1253       arity
1254   | (_,_,_,_,C.Constant (_,_,_,ty,_)), Ref.Ref (_,_,(Ref.Def |Ref.Decl)) -> ty
1255   | _ -> raise (AssertFailure (lazy "type_of_constant: environment/reference"))
1256
1257 and check_obj_well_typed (uri,height,metasenv,subst,kind) =
1258  (* CSC: here we should typecheck the metasenv and the subst *)
1259  assert (metasenv = [] && subst = []);
1260  match kind with
1261    | C.Constant (_,_,Some te,ty,_) ->
1262       let _ = typeof ~subst ~metasenv [] ty in
1263       let ty_te = typeof ~subst ~metasenv [] te in
1264       if not (R.are_convertible ~subst ~metasenv [] ty_te ty) then
1265        raise (TypeCheckerFailure (lazy (Printf.sprintf (
1266         "the type of the body is not convertible with the declared one.\n"^^
1267         "inferred type:\n%s\nexpected type:\n%s")
1268         (NCicPp.ppterm ~subst ~metasenv ~context:[] ty_te)
1269         (NCicPp.ppterm ~subst ~metasenv ~context:[] ty))))
1270    | C.Constant (_,_,None,ty,_) -> ignore (typeof ~subst ~metasenv [] ty)
1271    | C.Inductive (is_ind, leftno, tyl, _) ->
1272        check_mutual_inductive_defs uri ~metasenv ~subst is_ind leftno tyl
1273    | C.Fixpoint (inductive,fl,_) ->
1274       let types, kl, len =
1275         List.fold_left
1276          (fun (types,kl,len) (_,name,k,ty,_) ->
1277            let _ = typeof ~subst ~metasenv [] ty in
1278             ((name,(C.Decl (S.lift len ty)))::types, k::kl,len+1)
1279          ) ([],[],0) fl
1280       in
1281       let dfl, kl =
1282         List.split (List.map2
1283           (fun (_,_,_,_,bo) rno ->
1284              let dbo = debruijn uri len [] bo in
1285              dbo, Evil rno)
1286           fl kl)
1287       in
1288       List.iter2 (fun (_,name,x,ty,_) bo ->
1289        let ty_bo = typeof ~subst ~metasenv types bo in
1290        if not (R.are_convertible ~subst ~metasenv types ty_bo (S.lift len ty))
1291        then raise (TypeCheckerFailure (lazy ("(Co)Fix: ill-typed bodies")))
1292        else
1293         if inductive then begin
1294           let m, context = eat_lambdas ~subst ~metasenv types (x + 1) bo in
1295           let r_uri, r_len =
1296             let he =
1297              match List.hd context with _,C.Decl t -> t | _ -> assert false
1298             in
1299             match R.whd ~subst (List.tl context) he with
1300             | C.Const (Ref.Ref (_,uri,Ref.Ind _) as ref)
1301             | C.Appl (C.Const (Ref.Ref (_,uri,Ref.Ind _) as ref) :: _) ->
1302                 let _,_,itl,_,_ = E.get_checked_indtys ref in
1303                   uri, List.length itl
1304             | _ -> assert false
1305           in
1306           (* guarded by destructors conditions D{f,k,x,M} *)
1307           let rec enum_from k =
1308             function [] -> [] | v::tl -> (k,v)::enum_from (k+1) tl
1309           in
1310           guarded_by_destructors r_uri r_len
1311            ~subst ~metasenv context (enum_from (x+2) kl) m
1312         end else
1313          match returns_a_coinductive ~subst [] ty with
1314           | None ->
1315               raise (TypeCheckerFailure
1316                 (lazy "CoFix: does not return a coinductive type"))
1317           | Some uri ->
1318               (* guarded by constructors conditions C{f,M} *)
1319               if not (guarded_by_constructors ~subst ~metasenv
1320                   types 0 len false bo [] uri)
1321               then
1322                 raise (TypeCheckerFailure
1323                  (lazy "CoFix: not guarded by constructors"))
1324         ) fl dfl
1325
1326 let typecheck_obj = check_obj_well_typed;;
1327
1328 (* EOF *)