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