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