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