helm/software/components/cic_proof_checking/cicTypeChecker.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (* $Id$ *)
  27
  28 (* TODO factorize functions to frequent errors (e.g. "Unknwon mutual inductive
  29  * ...") *)
  30
  31 open Printf
  32
  33 exception AssertFailure of string Lazy.t;;
  34 exception TypeCheckerFailure of string Lazy.t;;
  35
  36 let fdebug = ref 0;;
  37 let debug t context =
  38  let rec debug_aux t i =
  39   let module C = Cic in
  40   let module U = UriManager in
  41    CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
  42  in
  43   if !fdebug = 0 then
  44    raise (TypeCheckerFailure (lazy (List.fold_right debug_aux (t::context) "")))
  45 ;;
  46
  47 let debug_print = fun _ -> ();;
  48
  49 let rec split l n =
  50  match (l,n) with
  51     (l,0) -> ([], l)
  52   | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
  53   | (_,_) ->
  54       raise (TypeCheckerFailure (lazy "Parameters number < left parameters number"))
  55 ;;
  56
  57 (* XXX: bug *)
  58 let ugraph_convertibility ug1 ug2 ul2 = true;;
  59
  60 let check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri obj =
  61  match unchecked_ugraph with
  62  | Some (ug,ul) ->
  63      if not (ugraph_convertibility inferred_ugraph ug ul) then
  64        raise (TypeCheckerFailure (lazy
  65          ("inferred univ graph not equal with declared ugraph")))
  66      else
  67       ug,ul,obj
  68  | None ->
  69      CicUnivUtils.clean_and_fill uri obj inferred_ugraph
  70 ;;
  71
  72 let debrujin_constructor ?(cb=fun _ _ -> ()) ?(check_exp_named_subst=true) uri number_of_types context =
  73  let rec aux k t =
  74   let module C = Cic in
  75   let res =
  76    match t with
  77       C.Rel n as t when n <= k -> t
  78     | C.Rel _ ->
  79         raise (TypeCheckerFailure (lazy "unbound variable found in constructor type"))
  80     | C.Var (uri,exp_named_subst) ->
  81        let exp_named_subst' =
  82         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
  83        in
  84         C.Var (uri,exp_named_subst')
  85     | C.Meta (i,l) ->
  86        let l' = List.map (function None -> None | Some t -> Some (aux k t)) l in
  87         C.Meta (i,l')
  88     | C.Sort _
  89     | C.Implicit _ as t -> t
  90     | C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
  91     | C.Prod (n,s,t) -> C.Prod (n, aux k s, aux (k+1) t)
  92     | C.Lambda (n,s,t) -> C.Lambda (n, aux k s, aux (k+1) t)
  93     | C.LetIn (n,s,ty,t) -> C.LetIn (n, aux k s, aux k ty, aux (k+1) t)
  94     | C.Appl l -> C.Appl (List.map (aux k) l)
  95     | C.Const (uri,exp_named_subst) ->
  96        let exp_named_subst' =
  97         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
  98        in
  99         C.Const (uri,exp_named_subst')
 100     | C.MutInd (uri',tyno,exp_named_subst) when UriManager.eq uri uri' ->
 101        if check_exp_named_subst && exp_named_subst != [] then
 102         raise (TypeCheckerFailure
 103           (lazy ("non-empty explicit named substitution is applied to "^
 104            "a mutual inductive type which is being defined"))) ;
 105        C.Rel (k + number_of_types - tyno) ;
 106     | C.MutInd (uri',tyno,exp_named_subst) ->
 107        let exp_named_subst' =
 108         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
 109        in
 110         C.MutInd (uri',tyno,exp_named_subst')
 111     | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
 112        let exp_named_subst' =
 113         List.map (function (uri,t) -> (uri,aux k t)) exp_named_subst
 114        in
 115         C.MutConstruct (uri,tyno,consno,exp_named_subst')
 116     | C.MutCase (sp,i,outty,t,pl) ->
 117        C.MutCase (sp, i, aux k outty, aux k t,
 118         List.map (aux k) pl)
 119     | C.Fix (i, fl) ->
 120        let len = List.length fl in
 121        let liftedfl =
 122         List.map
 123          (fun (name, i, ty, bo) -> (name, i, aux k ty, aux (k+len) bo))
 124           fl
 125        in
 126         C.Fix (i, liftedfl)
 127     | C.CoFix (i, fl) ->
 128        let len = List.length fl in
 129        let liftedfl =
 130         List.map
 131          (fun (name, ty, bo) -> (name, aux k ty, aux (k+len) bo))
 132           fl
 133        in
 134         C.CoFix (i, liftedfl)
 135   in
 136    cb t res;
 137    res
 138  in
 139   aux (List.length context)
 140 ;;
 141
 142 exception CicEnvironmentError;;
 143
 144 let check_homogeneous_call context indparamsno n uri reduct tl =
 145  let last =
 146   List.fold_left
 147    (fun k x ->
 148      if k = 0 then 0
 149      else
 150       match CicReduction.whd context x with
 151       | Cic.Rel m when m = n - (indparamsno - k) -> k - 1
 152       | _ -> raise (TypeCheckerFailure (lazy
 153          ("Argument "^string_of_int (indparamsno - k + 1) ^ " (of " ^
 154          string_of_int indparamsno ^ " fixed) is not homogeneous in "^
 155          "appl:\n"^ CicPp.ppterm reduct))))
 156    indparamsno tl
 157  in
 158   if last <> 0 then
 159    raise (TypeCheckerFailure
 160     (lazy ("Non-positive occurence in mutual inductive definition(s) [2]"^
 161      UriManager.string_of_uri uri)))
 162 ;;
 163
 164
 165 let rec type_of_constant ~logger uri orig_ugraph =
 166  let module C = Cic in
 167  let module R = CicReduction in
 168  let module U = UriManager in
 169  let cobj,ugraph =
 170    match CicEnvironment.is_type_checked ~trust:true orig_ugraph uri with
 171       CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
 172     | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) ->
 173        logger#log (`Start_type_checking uri) ;
 174        (* let's typecheck the uncooked obj *)
 175        let inferred_ugraph =
 176          match uobj with
 177            C.Constant (_,Some te,ty,_,_) ->
 178            let _,ugraph = type_of ~logger ty CicUniv.empty_ugraph in
 179            let type_of_te,ugraph = type_of ~logger te ugraph in
 180               let b,ugraph = R.are_convertible [] type_of_te ty ugraph in
 181               if not b then
 182                raise (TypeCheckerFailure (lazy (sprintf
 183                 "the constant %s is not well typed because the type %s of the body is not convertible to the declared type %s"
 184                 (U.string_of_uri uri) (CicPp.ppterm type_of_te)
 185                 (CicPp.ppterm ty))))
 186               else
 187                 ugraph
 188          | C.Constant (_,None,ty,_,_) ->
 189            (* only to check that ty is well-typed *)
 190            let _,ugraph = type_of ~logger ty CicUniv.empty_ugraph in
 191            ugraph
 192          | C.CurrentProof (_,conjs,te,ty,_,_) ->
 193              let _,ugraph =
 194               List.fold_left
 195                (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
 196                  let _,ugraph =
 197                   type_of_aux' ~logger metasenv context ty ugraph
 198                  in
 199                  (metasenv @ [conj],ugraph)
 200                ) ([],CicUniv.empty_ugraph) conjs
 201              in
 202              let _,ugraph = type_of_aux' ~logger conjs [] ty ugraph in
 203              let type_of_te,ugraph = type_of_aux' ~logger conjs [] te ugraph in
 204              let b,ugraph = R.are_convertible [] type_of_te ty ugraph in
 205                if not b then
 206                  raise (TypeCheckerFailure (lazy (sprintf
 207                   "the current proof %s is not well typed because the type %s of the body is not convertible to the declared type %s"
 208                   (U.string_of_uri uri) (CicPp.ppterm type_of_te)
 209                   (CicPp.ppterm ty))))
 210                else
 211                  ugraph
 212          | _ ->
 213              raise
 214               (TypeCheckerFailure (lazy ("Unknown constant:" ^ U.string_of_uri uri)))
 215        in
 216        let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj in
 217        CicEnvironment.set_type_checking_info uri (obj, ugraph, ul);
 218        logger#log (`Type_checking_completed uri) ;
 219        match CicEnvironment.is_type_checked ~trust:false orig_ugraph uri with
 220            CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
 221          | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
 222   in
 223    match cobj,ugraph with
 224       (C.Constant (_,_,ty,_,_)),g -> ty,g
 225     | (C.CurrentProof (_,_,_,ty,_,_)),g -> ty,g
 226     | _ ->
 227         raise (TypeCheckerFailure (lazy ("Unknown constant:" ^ U.string_of_uri uri)))
 228
 229 and type_of_variable ~logger uri orig_ugraph =
 230  let module C = Cic in
 231  let module R = CicReduction in
 232  let module U = UriManager in
 233   (* 0 because a variable is never cooked => no partial cooking at one level *)
 234   match CicEnvironment.is_type_checked ~trust:true orig_ugraph uri with
 235   | CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),ugraph') -> ty,ugraph'
 236   | CicEnvironment.UncheckedObj
 237      (C.Variable (_,bo,ty,_,_) as uobj, unchecked_ugraph)
 238     ->
 239       logger#log (`Start_type_checking uri) ;
 240       (* only to check that ty is well-typed *)
 241       let _,ugraph = type_of ~logger ty CicUniv.empty_ugraph in
 242       let inferred_ugraph =
 243        match bo with
 244            None -> ugraph
 245          | Some bo ->
 246              let ty_bo,ugraph = type_of ~logger bo ugraph in
 247              let b,ugraph = R.are_convertible [] ty_bo ty ugraph in
 248              if not b then
 249               raise (TypeCheckerFailure
 250                 (lazy ("Unknown variable:" ^ U.string_of_uri uri)))
 251              else
 252                ugraph
 253       in
 254        let ugraph, ul, obj =
 255          check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj
 256        in
 257        CicEnvironment.set_type_checking_info uri (obj, ugraph, ul);
 258        logger#log (`Type_checking_completed uri) ;
 259        (match CicEnvironment.is_type_checked ~trust:false orig_ugraph uri with
 260            CicEnvironment.CheckedObj((C.Variable(_,_,ty,_,_)),ugraph)->ty,ugraph
 261          | CicEnvironment.CheckedObj _
 262          | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError)
 263    |  _ ->
 264         raise (TypeCheckerFailure (lazy
 265           ("Unknown variable:" ^ U.string_of_uri uri)))
 266
 267 and does_not_occur ?(subst=[]) context n nn te =
 268  let module C = Cic in
 269    match te with
 270       C.Rel m when m > n && m <= nn -> false
 271     | C.Rel m ->
 272        (try
 273          (match List.nth context (m-1) with
 274              Some (_,C.Def (bo,_)) ->
 275               does_not_occur ~subst context n nn (CicSubstitution.lift m bo)
 276            | _ -> true)
 277         with
 278          Failure _ -> assert false)
 279     | C.Sort _
 280     | C.Implicit _ -> true
 281     | C.Meta (mno,l) ->
 282        List.fold_right
 283         (fun x i ->
 284           match x with
 285              None -> i
 286            | Some x -> i && does_not_occur ~subst context n nn x) l true &&
 287        (try
 288          let (canonical_context,term,ty) = CicUtil.lookup_subst mno subst in
 289           does_not_occur ~subst context n nn (CicSubstitution.subst_meta l term)
 290         with
 291          CicUtil.Subst_not_found _ -> true)
 292     | C.Cast (te,ty) ->
 293        does_not_occur ~subst context n nn te &&
 294        does_not_occur ~subst context n nn ty
 295     | C.Prod (name,so,dest) ->
 296        does_not_occur ~subst context n nn so &&
 297         does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n + 1)
 298          (nn + 1) dest
 299     | C.Lambda (name,so,dest) ->
 300        does_not_occur ~subst context n nn so &&
 301         does_not_occur ~subst ((Some (name,(C.Decl so)))::context) (n+1) (nn+1)
 302          dest
 303     | C.LetIn (name,so,ty,dest) ->
 304        does_not_occur ~subst context n nn so &&
 305         does_not_occur ~subst context n nn ty &&
 306          does_not_occur ~subst ((Some (name,(C.Def (so,ty))))::context)
 307           (n + 1) (nn + 1) dest
 308     | C.Appl l ->
 309        List.for_all (does_not_occur ~subst context n nn) l
 310     | C.Var (_,exp_named_subst)
 311     | C.Const (_,exp_named_subst)
 312     | C.MutInd (_,_,exp_named_subst)
 313     | C.MutConstruct (_,_,_,exp_named_subst) ->
 314        List.for_all (fun (_,x) -> does_not_occur ~subst context n nn x)
 315         exp_named_subst
 316     | C.MutCase (_,_,out,te,pl) ->
 317        does_not_occur ~subst context n nn out &&
 318        does_not_occur ~subst context n nn te &&
 319        List.for_all (does_not_occur ~subst context n nn) pl
 320     | C.Fix (_,fl) ->
 321        let len = List.length fl in
 322         let n_plus_len = n + len in
 323         let nn_plus_len = nn + len in
 324         let tys,_ =
 325          List.fold_left
 326           (fun (types,len) (n,_,ty,_) ->
 327              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
 328               len+1)
 329           ) ([],0) fl
 330         in
 331          List.fold_right
 332           (fun (_,_,ty,bo) i ->
 333             i && does_not_occur ~subst context n nn ty &&
 334             does_not_occur ~subst (tys @ context) n_plus_len nn_plus_len bo
 335           ) fl true
 336     | C.CoFix (_,fl) ->
 337        let len = List.length fl in
 338         let n_plus_len = n + len in
 339         let nn_plus_len = nn + len in
 340         let tys,_ =
 341          List.fold_left
 342           (fun (types,len) (n,ty,_) ->
 343              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
 344               len+1)
 345           ) ([],0) fl
 346         in
 347          List.fold_right
 348           (fun (_,ty,bo) i ->
 349             i && does_not_occur ~subst context n nn ty &&
 350             does_not_occur ~subst (tys @ context) n_plus_len nn_plus_len bo
 351           ) fl true
 352
 353 (* Inductive types being checked for positivity have *)
 354 (* indexes x s.t. n < x <= nn.                       *)
 355 and weakly_positive context n nn uri indparamsno posuri te =
 356  let module C = Cic in
 357   (*CSC: Not very nice. *)
 358   let leftno =
 359     match CicEnvironment.get_obj CicUniv.oblivion_ugraph uri with
 360     | Cic.InductiveDefinition (_,_,leftno,_), _ -> leftno
 361     | _ -> assert false
 362   in
 363   let dummy = Cic.Sort Cic.Prop in
 364   (*CSC: to be moved in cicSubstitution? *)
 365   let rec subst_inductive_type_with_dummy =
 366    function
 367       C.MutInd (uri',0,_) when UriManager.eq uri' uri ->
 368        dummy
 369     | C.Appl ((C.MutInd (uri',0,_))::tl) when UriManager.eq uri' uri ->
 370        let _, rargs = HExtlib.split_nth leftno tl in
 371        if rargs = [] then dummy else Cic.Appl (dummy :: rargs)
 372     | C.Cast (te,ty) -> subst_inductive_type_with_dummy te
 373     | C.Prod (name,so,ta) ->
 374        C.Prod (name, subst_inductive_type_with_dummy so,
 375         subst_inductive_type_with_dummy ta)
 376     | C.Lambda (name,so,ta) ->
 377        C.Lambda (name, subst_inductive_type_with_dummy so,
 378         subst_inductive_type_with_dummy ta)
 379     | C.LetIn (name,so,ty,ta) ->
 380        C.LetIn (name, subst_inductive_type_with_dummy so,
 381         subst_inductive_type_with_dummy ty,
 382         subst_inductive_type_with_dummy ta)
 383     | C.Appl tl ->
 384        C.Appl (List.map subst_inductive_type_with_dummy tl)
 385     | C.MutCase (uri,i,outtype,term,pl) ->
 386        C.MutCase (uri,i,
 387         subst_inductive_type_with_dummy outtype,
 388         subst_inductive_type_with_dummy term,
 389         List.map subst_inductive_type_with_dummy pl)
 390     | C.Fix (i,fl) ->
 391        C.Fix (i,List.map (fun (name,i,ty,bo) -> (name,i,
 392         subst_inductive_type_with_dummy ty,
 393         subst_inductive_type_with_dummy bo)) fl)
 394     | C.CoFix (i,fl) ->
 395        C.CoFix (i,List.map (fun (name,ty,bo) -> (name,
 396         subst_inductive_type_with_dummy ty,
 397         subst_inductive_type_with_dummy bo)) fl)
 398     | C.Const (uri,exp_named_subst) ->
 399        let exp_named_subst' =
 400         List.map
 401          (function (uri,t) -> (uri,subst_inductive_type_with_dummy t))
 402          exp_named_subst
 403        in
 404         C.Const (uri,exp_named_subst')
 405     | C.Var (uri,exp_named_subst) ->
 406        let exp_named_subst' =
 407         List.map
 408          (function (uri,t) -> (uri,subst_inductive_type_with_dummy t))
 409          exp_named_subst
 410        in
 411         C.Var (uri,exp_named_subst')
 412     | C.MutInd (uri,typeno,exp_named_subst) ->
 413        let exp_named_subst' =
 414         List.map
 415          (function (uri,t) -> (uri,subst_inductive_type_with_dummy t))
 416          exp_named_subst
 417        in
 418         C.MutInd (uri,typeno,exp_named_subst')
 419     | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
 420        let exp_named_subst' =
 421         List.map
 422          (function (uri,t) -> (uri,subst_inductive_type_with_dummy t))
 423          exp_named_subst
 424        in
 425         C.MutConstruct (uri,typeno,consno,exp_named_subst')
 426     | t -> t
 427   in
 428   (* this function has the same semantics of are_all_occurrences_positive
 429      but the i-th context entry role is played by dummy and some checks
 430      are skipped because we already know that are_all_occurrences_positive
 431      of uri in te. *)
 432   let rec aux context n nn te =
 433     match CicReduction.whd context te with
 434      | C.Appl (C.Sort C.Prop::tl) ->
 435          List.for_all (does_not_occur context n nn) tl
 436      | C.Sort C.Prop -> true
 437      | C.Prod (name,source,dest) when
 438         does_not_occur ((Some (name,(C.Decl source)))::context) 0 1 dest ->
 439          (* dummy abstraction, so we behave as in the anonimous case *)
 440          strictly_positive context n nn indparamsno posuri source &&
 441            aux ((Some (name,(C.Decl source)))::context)
 442            (n + 1) (nn + 1) dest
 443      | C.Prod (name,source,dest) ->
 444          does_not_occur context n nn source &&
 445            aux ((Some (name,(C.Decl source)))::context)
 446            (n + 1) (nn + 1) dest
 447      | _ ->
 448        raise (TypeCheckerFailure (lazy "Malformed inductive constructor type"))
 449  in
 450    aux context n nn (subst_inductive_type_with_dummy te)
 451
 452 (* instantiate_parameters ps (x1:T1)...(xn:Tn)C                             *)
 453 (* returns ((x_|ps|:T_|ps|)...(xn:Tn)C){ps_1 / x1 ; ... ; ps_|ps| / x_|ps|} *)
 454 and instantiate_parameters params c =
 455  let module C = Cic in
 456   match (c,params) with
 457      (c,[]) -> c
 458    | (C.Prod (_,_,ta), he::tl) ->
 459        instantiate_parameters tl
 460         (CicSubstitution.subst he ta)
 461    | (C.Cast (te,_), _) -> instantiate_parameters params te
 462    | (t,l) -> raise (AssertFailure (lazy "1"))
 463
 464 and strictly_positive context n nn indparamsno posuri te =
 465  let module C = Cic in
 466  let module U = UriManager in
 467   match CicReduction.whd context te with
 468    | t when does_not_occur context n nn t -> true
 469    | C.Rel _ when indparamsno = 0 -> true
 470    | C.Cast (te,ty) ->
 471       (*CSC: bisogna controllare ty????*)
 472       strictly_positive context n nn indparamsno posuri te
 473    | C.Prod (name,so,ta) ->
 474       does_not_occur context n nn so &&
 475        strictly_positive ((Some (name,(C.Decl so)))::context) (n+1) (nn+1)
 476         indparamsno posuri ta
 477    | C.Appl ((C.Rel m)::tl) as reduct when m > n && m <= nn ->
 478       check_homogeneous_call context indparamsno n posuri reduct tl;
 479       List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
 480    | C.Appl ((C.MutInd (uri,i,exp_named_subst))::_)
 481    | (C.MutInd (uri,i,exp_named_subst)) as t ->
 482       let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in
 483       let (ok,paramsno,ity,cl,name) =
 484         let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 485           match o with
 486               C.InductiveDefinition (tl,_,paramsno,_) ->
 487                 let (name,_,ity,cl) = List.nth tl i in
 488                 (List.length tl = 1, paramsno, ity, cl, name)
 489                 (* (true, paramsno, ity, cl, name) *)
 490             | _ ->
 491                 raise
 492                   (TypeCheckerFailure
 493                      (lazy ("Unknown inductive type:" ^ U.string_of_uri uri)))
 494       in
 495       let (params,arguments) = split tl paramsno in
 496       let lifted_params = List.map (CicSubstitution.lift 1) params in
 497       let cl' =
 498         List.map
 499           (fun (_,te) ->
 500              instantiate_parameters lifted_params
 501                (CicSubstitution.subst_vars exp_named_subst te)
 502           ) cl
 503       in
 504         ok &&
 505           List.fold_right
 506           (fun x i -> i && does_not_occur context n nn x)
 507           arguments true &&
 508           List.fold_right
 509           (fun x i ->
 510              i &&
 511                weakly_positive
 512                 ((Some (C.Name name,(Cic.Decl ity)))::context) (n+1) (nn+1) uri
 513                 indparamsno posuri x
 514           ) cl' true
 515    | t -> false
 516
 517 (* the inductive type indexes are s.t. n < x <= nn *)
 518 and are_all_occurrences_positive context uri indparamsno i n nn te =
 519  let module C = Cic in
 520   match CicReduction.whd context te with
 521      C.Appl ((C.Rel m)::tl) as reduct when m = i ->
 522       check_homogeneous_call context indparamsno n uri reduct tl;
 523       List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
 524    | C.Rel m when m = i ->
 525       if indparamsno = 0 then
 526        true
 527       else
 528         raise (TypeCheckerFailure
 529          (lazy ("Non-positive occurence in mutual inductive definition(s) [3]"^
 530           UriManager.string_of_uri uri)))
 531    | C.Prod (name,source,dest) when
 532       does_not_occur ((Some (name,(C.Decl source)))::context) 0 1 dest ->
 533       (* dummy abstraction, so we behave as in the anonimous case *)
 534       strictly_positive context n nn indparamsno uri source &&
 535        are_all_occurrences_positive
 536         ((Some (name,(C.Decl source)))::context) uri indparamsno
 537         (i+1) (n + 1) (nn + 1) dest
 538    | C.Prod (name,source,dest) ->
 539       does_not_occur context n nn source &&
 540        are_all_occurrences_positive ((Some (name,(C.Decl source)))::context)
 541         uri indparamsno (i+1) (n + 1) (nn + 1) dest
 542    | _ ->
 543      raise
 544       (TypeCheckerFailure (lazy ("Malformed inductive constructor type " ^
 545         (UriManager.string_of_uri uri))))
 546
 547 (* Main function to checks the correctness of a mutual *)
 548 (* inductive block definition. This is the function    *)
 549 (* exported to the proof-engine.                       *)
 550 and typecheck_mutual_inductive_defs ~logger uri (itl,_,indparamsno) ugraph =
 551  let module U = UriManager in
 552   (* let's check if the arity of the inductive types are well *)
 553   (* formed                                                   *)
 554   let ugrap1 = List.fold_left
 555    (fun ugraph (_,_,x,_) -> let _,ugraph' =
 556       type_of ~logger x ugraph in ugraph')
 557    ugraph itl in
 558
 559   (* let's check if the types of the inductive constructors  *)
 560   (* are well formed.                                        *)
 561   (* In order not to use type_of_aux we put the types of the *)
 562   (* mutual inductive types at the head of the types of the  *)
 563   (* constructors using Prods                                *)
 564   let len = List.length itl in
 565   let tys =
 566     List.rev_map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl in
 567   let _,ugraph2 =
 568     List.fold_right
 569       (fun (_,_,ty,cl) (i,ugraph) ->
 570         let _,ty_sort = split_prods ~subst:[] [] ~-1 ty in
 571         let ugraph'' =
 572           List.fold_left
 573             (fun ugraph (name,te) ->
 574               let te = debrujin_constructor uri len [] te in
 575               let context,te = split_prods ~subst:[] tys indparamsno te in
 576               let con_sort,ugraph = type_of_aux' ~logger [] context te ugraph in
 577               let ugraph =
 578                match
 579                 CicReduction.whd context con_sort, CicReduction.whd [] ty_sort
 580                with
 581                   Cic.Sort (Cic.Type u1), Cic.Sort (Cic.Type u2)
 582                 | Cic.Sort (Cic.CProp u1), Cic.Sort (Cic.CProp u2)
 583                 | Cic.Sort (Cic.Type u1), Cic.Sort (Cic.CProp u2)
 584                 | Cic.Sort (Cic.CProp u1), Cic.Sort (Cic.Type u2) ->
 585                    CicUniv.add_ge u2 u1 ugraph
 586                 | Cic.Sort _, Cic.Sort Cic.Prop
 587                 | Cic.Sort _, Cic.Sort Cic.CProp _
 588                 | Cic.Sort _, Cic.Sort Cic.Set
 589                 | Cic.Sort _, Cic.Sort Cic.Type _ -> ugraph
 590                 | a,b ->
 591                    raise
 592                     (TypeCheckerFailure
 593                       (lazy ("Wrong constructor or inductive arity shape: "^
 594                         CicPp.ppterm a ^ " --- " ^ CicPp.ppterm b))) in
 595               (* let's check also the positivity conditions *)
 596               if
 597                 not
 598                   (are_all_occurrences_positive context uri indparamsno
 599                     (i+indparamsno) indparamsno (len+indparamsno) te)
 600               then
 601                 raise
 602                   (TypeCheckerFailure
 603                     (lazy ("Non positive occurence in " ^ U.string_of_uri uri)))
 604               else
 605                 ugraph
 606             ) ugraph cl in
 607         (i + 1),ugraph''
 608       ) itl (1,ugrap1)
 609   in
 610   ugraph2
 611
 612 (* Main function to checks the correctness of a mutual *)
 613 (* inductive block definition.                         *)
 614 and check_mutual_inductive_defs uri obj ugraph =
 615   match obj with
 616       Cic.InductiveDefinition (itl, params, indparamsno, _) ->
 617         typecheck_mutual_inductive_defs uri (itl,params,indparamsno) ugraph
 618     | _ ->
 619         raise (TypeCheckerFailure (
 620                 lazy ("Unknown mutual inductive definition:" ^
 621                  UriManager.string_of_uri uri)))
 622
 623 and type_of_mutual_inductive_defs ~logger uri i orig_ugraph =
 624  let module C = Cic in
 625  let module R = CicReduction in
 626  let module U = UriManager in
 627   let cobj,ugraph1 =
 628    match CicEnvironment.is_type_checked ~trust:true orig_ugraph uri with
 629        CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
 630      | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) ->
 631          logger#log (`Start_type_checking uri) ;
 632          let inferred_ugraph =
 633            check_mutual_inductive_defs ~logger uri uobj CicUniv.empty_ugraph
 634          in
 635          let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj in
 636          CicEnvironment.set_type_checking_info uri (obj,ugraph,ul);
 637          logger#log (`Type_checking_completed uri) ;
 638          (match CicEnvironment.is_type_checked ~trust:false orig_ugraph uri with
 639               CicEnvironment.CheckedObj (cobj,ugraph') -> (cobj,ugraph')
 640             | CicEnvironment.UncheckedObj _ -> raise CicEnvironmentError
 641          )
 642   in
 643   match cobj with
 644   | C.InductiveDefinition (dl,_,_,_) ->
 645       let (_,_,arity,_) = List.nth dl i in
 646         arity,ugraph1
 647   | _ ->
 648      raise (TypeCheckerFailure
 649       (lazy ("Unknown mutual inductive definition:" ^ U.string_of_uri uri)))
 650
 651 and type_of_mutual_inductive_constr ~logger uri i j orig_ugraph =
 652  let module C = Cic in
 653  let module R = CicReduction in
 654  let module U = UriManager in
 655   let cobj,ugraph1 =
 656     match CicEnvironment.is_type_checked ~trust:true orig_ugraph uri with
 657         CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
 658       | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) ->
 659           logger#log (`Start_type_checking uri) ;
 660           let inferred_ugraph =
 661             check_mutual_inductive_defs ~logger uri uobj CicUniv.empty_ugraph
 662           in
 663           let ugraph, ul, obj = check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri uobj in
 664           CicEnvironment.set_type_checking_info uri (obj, ugraph, ul);
 665           logger#log (`Type_checking_completed uri) ;
 666           (match
 667              CicEnvironment.is_type_checked ~trust:false orig_ugraph uri
 668            with
 669                  CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
 670                | CicEnvironment.UncheckedObj _ ->
 671                        raise CicEnvironmentError)
 672   in
 673     match cobj with
 674         C.InductiveDefinition (dl,_,_,_) ->
 675           let (_,_,_,cl) = List.nth dl i in
 676           let (_,ty) = List.nth cl (j-1) in
 677             ty,ugraph1
 678       | _ ->
 679           raise (TypeCheckerFailure
 680            (lazy ("Unknown mutual inductive definition:" ^ UriManager.string_of_uri uri)))
 681
 682 and recursive_args context n nn te =
 683  let module C = Cic in
 684  match CicReduction.whd context te with
 685     C.Rel _
 686   | C.MutInd _ -> []
 687   | C.Var _
 688   | C.Meta _
 689   | C.Sort _
 690   | C.Implicit _
 691   | C.Cast _ (*CSC ??? *) ->
 692      raise (AssertFailure (lazy "3")) (* due to type-checking *)
 693   | C.Prod (name,so,de) ->
 694      (not (does_not_occur context n nn so)) ::
 695       (recursive_args ((Some (name,(C.Decl so)))::context) (n+1) (nn + 1) de)
 696   | C.Lambda _
 697   | C.LetIn _ ->
 698      raise (AssertFailure (lazy "4")) (* due to type-checking *)
 699   | C.Appl _ -> []
 700   | C.Const _ -> raise (AssertFailure (lazy "5"))
 701   | C.MutConstruct _
 702   | C.MutCase _
 703   | C.Fix _
 704   | C.CoFix _ -> raise (AssertFailure (lazy "6")) (* due to type-checking *)
 705
 706 and get_new_safes ~subst context p rl safes n nn x =
 707  let module C = Cic in
 708  let module U = UriManager in
 709  let module R = CicReduction in
 710   match R.whd ~subst context p, rl with
 711    | C.Lambda (name,so,ta), b::tl ->
 712        let safes = List.map (fun x -> x + 1) safes in
 713        let safes = if b then 1::safes else safes in
 714        get_new_safes ~subst ((Some (name,(C.Decl so)))::context)
 715           ta tl safes (n+1) (nn+1) (x+1)
 716    | C.MutConstruct _ as e, _
 717    | (C.Rel _ as e), _
 718    | e, [] -> (e,safes,n,nn,x,context)
 719    | p,_::_ ->
 720       raise
 721        (AssertFailure (lazy
 722          (Printf.sprintf "Get New Safes: p=%s" (CicPp.ppterm p))))
 723
 724 and split_prods ~subst context n te =
 725  let module C = Cic in
 726  let module R = CicReduction in
 727   match (n, R.whd ~subst context te) with
 728      (0, _) -> context,te
 729    | (n, C.Sort _) when n <= 0 -> context,te
 730    | (n, C.Prod (name,so,ta)) ->
 731        split_prods ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta
 732    | (_, _) -> raise (AssertFailure (lazy "8"))
 733
 734 and eat_lambdas ~subst context n te =
 735  let module C = Cic in
 736  let module R = CicReduction in
 737   match (n, R.whd ~subst context te) with
 738      (0, _) -> (te, 0, context)
 739    | (n, C.Lambda (name,so,ta)) when n > 0 ->
 740       let (te, k, context') =
 741        eat_lambdas ~subst ((Some (name,(C.Decl so)))::context) (n - 1) ta
 742       in
 743        (te, k + 1, context')
 744    | (n, te) ->
 745        raise (AssertFailure (lazy (sprintf "9 (%d, %s)" n (CicPp.ppterm te))))
 746
 747 and specialize_inductive_type ~logger ~subst ~metasenv context t =
 748   let ty,_= type_of_aux' ~logger ~subst metasenv context t CicUniv.oblivion_ugraph in
 749   match CicReduction.whd ~subst context ty with
 750   | Cic.MutInd (uri,_,exp)
 751   | Cic.Appl (Cic.MutInd (uri,_,exp) :: _) as ty ->
 752       let args = match ty with Cic.Appl (_::tl) -> tl | _ -> [] in
 753       let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
 754       (match o with
 755       | Cic.InductiveDefinition (tl,_,paramsno,_) ->
 756           let left_args,_ = HExtlib.split_nth paramsno args in
 757           List.map (fun (name, isind, arity, cl) ->
 758             let arity = CicSubstitution.subst_vars exp arity in
 759             let arity = instantiate_parameters left_args arity in
 760             let cl =
 761               List.map
 762                (fun (id,ty) ->
 763                  let ty = CicSubstitution.subst_vars exp ty in
 764                  id, instantiate_parameters left_args ty)
 765                cl
 766             in
 767             name, isind, arity, cl)
 768           tl, paramsno
 769       | _ -> assert false)
 770   | _ -> assert false
 771
 772 and check_is_really_smaller_arg
 773   ~logger ~metasenv ~subst rec_uri rec_uri_len context n nn kl x safes te
 774 =
 775  let module C = Cic in
 776  let module U = UriManager in
 777  (*CSC: we could perform beta-iota(-zeta?) immediately, and
 778    delta only on-demand when it fails without *)
 779  match CicReduction.whd ~subst context te with
 780      C.Rel m when List.mem m safes -> true
 781    | C.Rel _
 782    | C.MutConstruct _
 783    | C.Const _
 784    | C.Var _ -> false
 785    | C.Appl (he::_) ->
 786         check_is_really_smaller_arg rec_uri rec_uri_len
 787           ~logger ~metasenv ~subst context n nn kl x safes he
 788    | C.Lambda (name,ty,ta) ->
 789       check_is_really_smaller_arg rec_uri rec_uri_len
 790         ~logger ~metasenv ~subst (Some (name,Cic.Decl ty)::context)
 791         (n+1) (nn+1) kl (x+1) (List.map (fun n -> n+1) safes) ta
 792    | C.MutCase (uri,i,outtype,term,pl) ->
 793       (match term with
 794       | C.Rel m | C.Appl ((C.Rel m)::_) when List.mem m safes || m = x ->
 795          let tys,_ =
 796            specialize_inductive_type ~logger ~subst ~metasenv context term
 797          in
 798          let tys_ctx,_ =
 799            List.fold_left
 800              (fun (types,len) (n,_,ty,_) ->
 801                Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
 802                len+1)
 803              ([],0) tys
 804          in
 805          let _,isinductive,_,cl = List.nth tys i in
 806          if not isinductive then
 807            List.for_all
 808             (check_is_really_smaller_arg rec_uri rec_uri_len
 809               ~logger ~metasenv ~subst context n nn kl x safes)
 810             pl
 811          else
 812            List.for_all2
 813             (fun p (_,c) ->
 814               let rec_params =
 815                let c =
 816                  debrujin_constructor ~check_exp_named_subst:false
 817                   rec_uri rec_uri_len context c in
 818                let len_ctx = List.length context in
 819                recursive_args (context@tys_ctx) len_ctx (len_ctx+rec_uri_len) c
 820               in
 821               let (e, safes',n',nn',x',context') =
 822                 get_new_safes ~subst context p rec_params safes n nn x
 823               in
 824                check_is_really_smaller_arg rec_uri rec_uri_len
 825                 ~logger ~metasenv ~subst context' n' nn' kl x' safes' e
 826             ) pl cl
 827         | _ ->
 828           List.for_all
 829            (check_is_really_smaller_arg
 830              rec_uri rec_uri_len ~logger ~metasenv ~subst
 831              context n nn kl x safes) pl
 832       )
 833    | C.Fix (_, fl) ->
 834       let len = List.length fl in
 835        let n_plus_len = n + len
 836        and nn_plus_len = nn + len
 837        and x_plus_len = x + len
 838        and tys,_ =
 839         List.fold_left
 840           (fun (types,len) (n,_,ty,_) ->
 841              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
 842               len+1)
 843           ) ([],0) fl
 844        and safes' = List.map (fun x -> x + len) safes in
 845         List.for_all
 846          (fun (_,_,_,bo) ->
 847             check_is_really_smaller_arg
 848               rec_uri rec_uri_len ~logger ~metasenv ~subst
 849                 (tys@context) n_plus_len nn_plus_len kl
 850              x_plus_len safes' bo
 851          ) fl
 852    | t ->
 853       raise (AssertFailure (lazy ("An inhabitant of an inductive type in normal form cannot have this shape: " ^ CicPp.ppterm t)))
 854
 855 and guarded_by_destructors
 856   ~logger ~metasenv ~subst rec_uri rec_uri_len context n nn kl x safes t
 857 =
 858  let module C = Cic in
 859  let module U = UriManager in
 860   let t = CicReduction.whd ~delta:false ~subst context t in
 861   let res =
 862    match t with
 863      C.Rel m when m > n && m <= nn -> false
 864    | C.Rel m ->
 865       (match List.nth context (m-1) with
 866           Some (_,C.Decl _) -> true
 867         | Some (_,C.Def (bo,_)) ->
 868            guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes
 869             (CicSubstitution.lift m bo)
 870         | None -> raise (TypeCheckerFailure (lazy "Reference to deleted hypothesis"))
 871       )
 872    | C.Meta _
 873    | C.Sort _
 874    | C.Implicit _ -> true
 875    | C.Cast (te,ty) ->
 876       guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes te &&
 877        guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes ty
 878    | C.Prod (name,so,ta) ->
 879       guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes so &&
 880        guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst ((Some (name,(C.Decl so)))::context)
 881         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 882    | C.Lambda (name,so,ta) ->
 883       guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes so &&
 884        guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst ((Some (name,(C.Decl so)))::context)
 885         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 886    | C.LetIn (name,so,ty,ta) ->
 887       guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes so &&
 888        guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes ty &&
 889         guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst ((Some (name,(C.Def (so,ty))))::context)
 890          (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 891    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
 892       let k = List.nth kl (m - n - 1) in
 893        if not (List.length tl > k) then false
 894        else
 895         List.for_all
 896          (guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes) tl &&
 897         check_is_really_smaller_arg
 898           rec_uri rec_uri_len
 899           ~logger ~metasenv ~subst context n nn kl x safes (List.nth tl k)
 900    | C.Var (_,exp_named_subst)
 901    | C.Const (_,exp_named_subst)
 902    | C.MutInd (_,_,exp_named_subst)
 903    | C.MutConstruct (_,_,_,exp_named_subst) ->
 904       List.for_all
 905        (fun (_,t) -> guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes t)
 906        exp_named_subst
 907    | C.MutCase (uri,i,outtype,term,pl) ->
 908       (match CicReduction.whd ~subst context term with
 909         | C.Rel m
 910         | C.Appl ((C.Rel m)::_) as t when List.mem m safes || m = x ->
 911            let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in
 912            List.for_all
 913              (guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes)
 914              tl &&
 915            let tys,_ =
 916              specialize_inductive_type ~logger ~subst ~metasenv context t
 917            in
 918            let tys_ctx,_ =
 919              List.fold_left
 920                (fun (types,len) (n,_,ty,_) ->
 921                  Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
 922                  len+1)
 923                ([],0) tys
 924            in
 925            let _,isinductive,_,cl = List.nth tys i in
 926             if not isinductive then
 927              guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes outtype &&
 928               guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes term &&
 929               List.for_all
 930                (guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes)
 931                pl
 932             else
 933              guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes outtype &&
 934              List.for_all2
 935               (fun p (_,c) ->
 936                let rec_params =
 937                 let c =
 938                  debrujin_constructor ~check_exp_named_subst:false
 939                   rec_uri rec_uri_len context c in
 940                 let len_ctx = List.length context in
 941                 recursive_args (context@tys_ctx) len_ctx (len_ctx+rec_uri_len) c
 942                in
 943                let (e, safes',n',nn',x',context') =
 944                 get_new_safes ~subst context p rec_params safes n nn x
 945                in
 946                 guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context' n' nn' kl x' safes' e
 947                ) pl cl
 948         | _ ->
 949           guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes outtype &&
 950            guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes term &&
 951            (*CSC: manca ??? il controllo sul tipo di term? *)
 952            List.fold_right
 953             (fun p i -> i && guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes p)
 954             pl true
 955       )
 956    | C.Appl (C.Fix (fixno, fl)::_) | C.Fix (fixno,fl) as t->
 957       let l = match t with C.Appl (_::tl) -> tl | _ -> [] in
 958       let len = List.length fl in
 959       let n_plus_len = n + len in
 960       let nn_plus_len = nn + len in
 961       let x_plus_len = x + len in
 962       let tys,_ =
 963         List.fold_left
 964           (fun (types,len) (n,_,ty,_) ->
 965              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
 966               len+1)
 967           ) ([],0) fl in
 968        let safes' = List.map (fun x -> x + len) safes in
 969         List.for_all
 970          (guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes) l &&
 971         snd (List.fold_left
 972          (fun (fixno',i) (_,recno,ty,bo) ->
 973            fixno'+1,
 974            i &&
 975            guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x_plus_len safes' ty &&
 976            if
 977             fixno' = fixno &&
 978             List.length l > recno &&
 979             (*case where the recursive argument is already really_smaller *)
 980             check_is_really_smaller_arg
 981               rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes
 982               (List.nth l recno)
 983            then
 984             let bo_without_lambdas,_,context =
 985              eat_lambdas ~subst (tys@context) (recno+1) bo
 986             in
 987              (* we assume the formal argument to be safe *)
 988              guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context (n_plus_len+recno+1)
 989               (nn_plus_len+recno+1) kl (x_plus_len+recno+1)
 990               (1::List.map (fun x -> x+recno+1) safes')
 991               bo_without_lambdas
 992            else
 993             guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst (tys@context) n_plus_len nn_plus_len
 994              kl x_plus_len safes' bo
 995          ) (0,true) fl)
 996    | C.CoFix (_, fl) ->
 997       let len = List.length fl in
 998        let n_plus_len = n + len
 999        and nn_plus_len = nn + len
1000        and x_plus_len = x + len
1001        and tys,_ =
1002         List.fold_left
1003           (fun (types,len) (n,ty,_) ->
1004              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
1005               len+1)
1006           ) ([],0) fl
1007        and safes' = List.map (fun x -> x + len) safes in
1008         List.fold_right
1009          (fun (_,ty,bo) i ->
1010            i &&
1011             guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x_plus_len safes' ty &&
1012             guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst (tys@context) n_plus_len nn_plus_len kl
1013              x_plus_len safes' bo
1014          ) fl true
1015    | C.Appl tl ->
1016       List.fold_right
1017        (fun t i -> i && guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes t)
1018        tl true
1019   in
1020    if res then res
1021    else
1022     let t' = CicReduction.whd ~subst context t in
1023      if t = t' then
1024       false
1025      else
1026       guarded_by_destructors rec_uri rec_uri_len ~logger ~metasenv ~subst context n nn kl x safes t'
1027
1028 (* the boolean h means already protected *)
1029 (* args is the list of arguments the type of the constructor that may be *)
1030 (* found in head position must be applied to.                            *)
1031 and guarded_by_constructors ~logger ~subst ~metasenv indURI =
1032  let module C = Cic in
1033  let rec aux context n nn h te =
1034   match CicReduction.whd ~subst context te with
1035    | C.Rel m when m > n && m <= nn -> h
1036    | C.Rel _
1037    | C.Meta _ -> true
1038    | C.Sort _
1039    | C.Implicit _
1040    | C.Cast _
1041    | C.Prod _
1042    | C.MutInd _
1043    | C.LetIn _ -> raise (AssertFailure (lazy "17"))
1044    | C.Lambda (name,so,de) ->
1045       does_not_occur ~subst context n nn so &&
1046       aux ((Some (name,(C.Decl so)))::context) (n + 1) (nn + 1) h de
1047    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
1048       h && List.for_all (does_not_occur ~subst context n nn) tl
1049    | C.MutConstruct (_,_,_,exp_named_subst) ->
1050       List.for_all
1051         (fun (_,x) -> does_not_occur ~subst context n nn x) exp_named_subst
1052    | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) as t ->
1053       List.for_all
1054         (fun (_,x) -> does_not_occur ~subst context n nn x) exp_named_subst &&
1055       let consty, len_tys, tys_ctx, paramsno =
1056        let tys, paramsno =
1057          specialize_inductive_type ~logger ~subst ~metasenv context t in
1058        let _,_,_,cl = List.nth tys i in
1059        let _,ty = List.nth cl (j-1) in
1060          ty, List.length tys,
1061          fst(List.fold_left
1062           (fun (types,len) (n,_,ty,_) ->
1063            Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, len+1)
1064           ([],0) tys), paramsno
1065       in
1066       let rec_params =
1067        let c =
1068          debrujin_constructor ~check_exp_named_subst:false
1069            indURI len_tys context consty
1070        in
1071        let len_ctx = List.length context in
1072        recursive_args (context@tys_ctx) len_ctx (len_ctx+len_tys) c
1073       in
1074       let rec analyse_instantiated_type rec_spec args =
1075        match rec_spec, args with
1076        | h::rec_spec, he::args ->
1077            aux context n nn h he &&
1078            analyse_instantiated_type rec_spec args
1079        | _,[] -> true
1080        | _ -> raise (AssertFailure (lazy
1081          ("Too many args for constructor: " ^ String.concat " "
1082          (List.map (fun x-> CicPp.ppterm x) args))))
1083       in
1084       let left, args = HExtlib.split_nth paramsno tl in
1085       List.for_all (does_not_occur ~subst context n nn) left &&
1086       analyse_instantiated_type rec_params args
1087    | C.Appl ((C.MutCase (_,_,out,te,pl))::_)
1088    | C.MutCase (_,_,out,te,pl) as t ->
1089        let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in
1090        List.for_all (does_not_occur ~subst context n nn) tl &&
1091        does_not_occur ~subst context n nn out &&
1092        does_not_occur ~subst context n nn te &&
1093        List.for_all (aux context n nn h ) pl
1094    | C.Fix (_,fl)
1095    | C.Appl (C.Fix (_,fl)::_) as t ->
1096        let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in
1097       let len = List.length fl in
1098        let n_plus_len = n + len
1099        and nn_plus_len = nn + len
1100        and tys,_ =
1101         List.fold_left
1102           (fun (types,len) (n,_,ty,_) ->
1103              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
1104               len+1)
1105           ) ([],0) fl
1106        in
1107         List.for_all (does_not_occur ~subst context n nn) tl &&
1108         List.for_all
1109          (fun (_,_,ty,bo) ->
1110            does_not_occur ~subst context n nn ty &&
1111            aux (tys@context) n_plus_len nn_plus_len h bo)
1112          fl
1113    | C.Appl ((C.CoFix (_,fl))::_)
1114    | C.CoFix (_,fl) as t ->
1115        let tl = match t with C.Appl (_::tl) -> tl | _ -> [] in
1116        let len = List.length fl in
1117        let n_plus_len = n + len
1118        and nn_plus_len = nn + len
1119        and tys,_ =
1120           List.fold_left
1121             (fun (types,len) (n,ty,_) ->
1122                (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
1123                 len+1)
1124             ) ([],0) fl
1125        in
1126        List.for_all (does_not_occur ~subst context n nn) tl &&
1127        List.for_all
1128          (fun (_,ty,bo) ->
1129             does_not_occur ~subst context n nn ty &&
1130             aux (tys@context) n_plus_len nn_plus_len h bo)
1131          fl
1132    | C.Var _
1133    | C.Const _
1134    | C.Appl _ as t -> does_not_occur ~subst context n nn t
1135  in
1136    aux
1137
1138 and is_non_recursive ctx paramsno t uri =
1139   let t = debrujin_constructor uri 1 [] t in
1140 (*   let ctx, t =  split_prods ~subst:[] ctx paramsno t in *)
1141   let len = List.length ctx in
1142   let rec aux ctx n nn t =
1143     match CicReduction.whd ctx t with
1144     | Cic.Prod (name,src,tgt) ->
1145         does_not_occur ctx n nn src &&
1146          aux (Some (name,Cic.Decl src) :: ctx) (n+1) (nn+1) tgt
1147     | (Cic.Rel k)
1148     | Cic.Appl (Cic.Rel k :: _) when k = nn -> true
1149     | t -> assert false
1150   in
1151     aux ctx (len-1) len t
1152
1153 and check_allowed_sort_elimination ~subst ~metasenv ~logger context uri i
1154   need_dummy ind arity1 arity2 ugraph =
1155  let module C = Cic in
1156  let module U = UriManager in
1157   let arity1 = CicReduction.whd ~subst context arity1 in
1158   let rec check_allowed_sort_elimination_aux ugraph context arity2 need_dummy =
1159    match arity1, CicReduction.whd ~subst context arity2 with
1160      (C.Prod (name,so1,de1), C.Prod (_,so2,de2)) ->
1161        let b,ugraph1 =
1162         CicReduction.are_convertible ~subst ~metasenv context so1 so2 ugraph in
1163        if b then
1164          check_allowed_sort_elimination ~subst ~metasenv ~logger
1165            ((Some (name,C.Decl so1))::context) uri i
1166           need_dummy (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2
1167           ugraph1
1168        else
1169          false,ugraph1
1170    | (C.Sort _, C.Prod (name,so,ta)) when not need_dummy ->
1171        let b,ugraph1 =
1172         CicReduction.are_convertible ~subst ~metasenv context so ind ugraph in
1173        if not b then
1174          false,ugraph1
1175        else
1176         check_allowed_sort_elimination_aux ugraph1
1177          ((Some (name,C.Decl so))::context) ta true
1178    | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true,ugraph
1179    | (C.Sort C.Prop, C.Sort C.Set)
1180    | (C.Sort C.Prop, C.Sort (C.CProp _))
1181    | (C.Sort C.Prop, C.Sort (C.Type _) ) when need_dummy ->
1182        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1183          match o with
1184          C.InductiveDefinition (itl,_,paramsno,_) ->
1185            let itl_len = List.length itl in
1186            let (name,_,ty,cl) = List.nth itl i in
1187            let cl_len = List.length cl in
1188             if (cl_len = 0 || (itl_len = 1 && cl_len = 1)) then
1189              let non_informative,ugraph =
1190               if cl_len = 0 then true,ugraph
1191               else
1192                let b, ug =
1193                 is_non_informative ~logger [Some (C.Name name,C.Decl ty)]
1194                  paramsno (snd (List.nth cl 0)) ugraph
1195                in
1196                 b &&
1197                 is_non_recursive [Some (C.Name name,C.Decl ty)]
1198                   paramsno  (snd (List.nth cl 0)) uri, ug
1199              in
1200               (* is it a singleton or empty non recursive and non informative
1201                  definition? *)
1202               non_informative, ugraph
1203             else
1204               false,ugraph
1205          | _ ->
1206              raise (TypeCheckerFailure
1207                      (lazy ("Unknown mutual inductive definition:" ^
1208                        UriManager.string_of_uri uri)))
1209        )
1210    | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true , ugraph
1211    | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true , ugraph
1212    | (C.Sort C.Set, C.Sort (C.Type _))
1213    | (C.Sort C.Set, C.Sort (C.CProp _))
1214       when need_dummy ->
1215        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1216          match o with
1217            C.InductiveDefinition (itl,_,paramsno,_) ->
1218             let tys =
1219              List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1220             in
1221              let (_,_,_,cl) = List.nth itl i in
1222               (List.fold_right
1223                (fun (_,x) (i,ugraph) ->
1224                  if i then
1225                           is_small ~logger tys paramsno x ugraph
1226                  else
1227                    false,ugraph
1228                     ) cl (true,ugraph))
1229            | _ ->
1230             raise (TypeCheckerFailure
1231              (lazy ("Unknown mutual inductive definition:" ^
1232               UriManager.string_of_uri uri)))
1233        )
1234    | (C.Sort (C.Type _), C.Sort _) when need_dummy -> true , ugraph
1235    | (C.Sort (C.CProp _), C.Sort _) when need_dummy -> true , ugraph
1236    | (_,_) -> false,ugraph
1237  in
1238   check_allowed_sort_elimination_aux ugraph context arity2 need_dummy
1239
1240 and type_of_branch ~subst context argsno need_dummy outtype term constype =
1241  let module C = Cic in
1242  let module R = CicReduction in
1243   match R.whd ~subst context constype with
1244      C.MutInd (_,_,_) ->
1245       if need_dummy then
1246        outtype
1247       else
1248        C.Appl [outtype ; term]
1249    | C.Appl (C.MutInd (_,_,_)::tl) ->
1250       let (_,arguments) = split tl argsno
1251       in
1252        if need_dummy && arguments = [] then
1253         outtype
1254        else
1255         C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
1256    | C.Prod (name,so,de) ->
1257       let term' =
1258        match CicSubstitution.lift 1 term with
1259           C.Appl l -> C.Appl (l@[C.Rel 1])
1260         | t -> C.Appl [t ; C.Rel 1]
1261       in
1262        C.Prod (name,so,type_of_branch ~subst
1263         ((Some (name,(C.Decl so)))::context) argsno need_dummy
1264         (CicSubstitution.lift 1 outtype) term' de)
1265    | _ -> raise (AssertFailure (lazy "20"))
1266
1267 (* check_metasenv_consistency checks that the "canonical" context of a
1268 metavariable is consitent - up to relocation via the relocation list l -
1269 with the actual context *)
1270
1271
1272 and check_metasenv_consistency ~logger ~subst metasenv context
1273   canonical_context l ugraph
1274 =
1275   let module C = Cic in
1276   let module R = CicReduction in
1277   let module S = CicSubstitution in
1278   let lifted_canonical_context =
1279     let rec aux i =
1280      function
1281          [] -> []
1282        | (Some (n,C.Decl t))::tl ->
1283            (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
1284        | None::tl -> None::(aux (i+1) tl)
1285        | (Some (n,C.Def (t,ty)))::tl ->
1286            (Some (n,C.Def ((S.subst_meta l (S.lift i t)),S.subst_meta l (S.lift i ty))))::(aux (i+1) tl)
1287     in
1288      aux 1 canonical_context
1289    in
1290    List.fold_left2
1291      (fun ugraph t ct ->
1292        match (t,ct) with
1293        | _,None -> ugraph
1294        | Some t,Some (_,C.Def (ct,_)) ->
1295           (*CSC: the following optimization is to avoid a possibly expensive
1296                  reduction that can be easily avoided and that is quite
1297                  frequent. However, this is better handled using levels to
1298                  control reduction *)
1299           let optimized_t =
1300            match t with
1301               Cic.Rel n ->
1302                (try
1303                  match List.nth context (n - 1) with
1304                     Some (_,C.Def (te,_)) -> S.lift n te
1305                   | _ -> t
1306                 with
1307                  Failure _ -> t)
1308             | _ -> t
1309           in
1310 (*if t <> optimized_t && optimized_t = ct then prerr_endline "!!!!!!!!!!!!!!!"
1311 else if t <> optimized_t then prerr_endline ("@@ " ^ CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm optimized_t ^ " <==> " ^ CicPp.ppterm ct);*)
1312            let b,ugraph1 =
1313              R.are_convertible ~subst ~metasenv context optimized_t ct ugraph
1314            in
1315            if not b then
1316              raise
1317                (TypeCheckerFailure
1318                   (lazy (sprintf "Not well typed metavariable local context: expected a term convertible with %s, found %s" (CicPp.ppterm ct) (CicPp.ppterm t))))
1319            else
1320              ugraph1
1321        | Some t,Some (_,C.Decl ct) ->
1322            let type_t,ugraph1 =
1323              type_of_aux' ~logger ~subst metasenv context t ugraph
1324            in
1325            let b,ugraph2 =
1326              R.are_convertible ~subst ~metasenv context type_t ct ugraph1
1327            in
1328            if not b then
1329              raise (TypeCheckerFailure
1330                      (lazy (sprintf "Not well typed metavariable local context: expected a term of type %s, found %s of type %s"
1331                          (CicPp.ppterm ct) (CicPp.ppterm t)
1332                          (CicPp.ppterm type_t))))
1333            else
1334              ugraph2
1335        | None, _  ->
1336            raise (TypeCheckerFailure
1337                    (lazy ("Not well typed metavariable local context: "^
1338                      "an hypothesis, that is not hidden, is not instantiated")))
1339      ) ugraph l lifted_canonical_context
1340
1341
1342 (*
1343    type_of_aux' is just another name (with a different scope)
1344    for type_of_aux
1345 *)
1346
1347 and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
1348  let rec type_of_aux ~logger context t ugraph =
1349   let module C = Cic in
1350   let module R = CicReduction in
1351   let module S = CicSubstitution in
1352   let module U = UriManager in
1353 (* FG: DEBUG ONLY
1354    prerr_endline ("TC: context:\n" ^ CicPp.ppcontext ~metasenv context);
1355    prerr_endline ("TC: term   :\n" ^ CicPp.ppterm ~metasenv t ^ "\n");
1356 *)
1357    match t with
1358       C.Rel n ->
1359        (try
1360          match List.nth context (n - 1) with
1361             Some (_,C.Decl t) -> S.lift n t,ugraph
1362           | Some (_,C.Def (_,ty)) -> S.lift n ty,ugraph
1363           | None -> raise
1364               (TypeCheckerFailure (lazy "Reference to deleted hypothesis"))
1365         with
1366         Failure _ ->
1367           raise (TypeCheckerFailure (lazy "unbound variable"))
1368        )
1369     | C.Var (uri,exp_named_subst) ->
1370       incr fdebug ;
1371         let ugraph1 =
1372           check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph
1373         in
1374         let ty,ugraph2 = type_of_variable ~logger uri ugraph1 in
1375         let ty1 = CicSubstitution.subst_vars exp_named_subst ty in
1376           decr fdebug ;
1377           ty1,ugraph2
1378     | C.Meta (n,l) ->
1379        (try
1380           let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in
1381           let ugraph1 =
1382             check_metasenv_consistency ~logger
1383               ~subst metasenv context canonical_context l ugraph
1384           in
1385             (* assuming subst is well typed !!!!! *)
1386             ((CicSubstitution.subst_meta l ty), ugraph1)
1387               (* type_of_aux context (CicSubstitution.subst_meta l term) *)
1388         with CicUtil.Subst_not_found _ ->
1389           let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
1390           let ugraph1 =
1391             check_metasenv_consistency ~logger
1392               ~subst metasenv context canonical_context l ugraph
1393           in
1394             ((CicSubstitution.subst_meta l ty),ugraph1))
1395       (* TASSI: CONSTRAINTS *)
1396     | C.Sort (C.CProp t) ->
1397        let t' = CicUniv.fresh() in
1398        (try
1399          let ugraph1 = CicUniv.add_gt t' t ugraph in
1400            (C.Sort (C.Type t')),ugraph1
1401         with
1402          CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
1403     | C.Sort (C.Type t) ->
1404        let t' = CicUniv.fresh() in
1405        (try
1406          let ugraph1 = CicUniv.add_gt t' t ugraph in
1407            (C.Sort (C.Type t')),ugraph1
1408         with
1409          CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
1410     | C.Sort (C.Prop|C.Set) -> (C.Sort (C.Type (CicUniv.fresh ()))),ugraph
1411     | C.Implicit _ -> raise (AssertFailure (lazy "Implicit found"))
1412     | C.Cast (te,ty) as t ->
1413        let _,ugraph1 = type_of_aux ~logger context ty ugraph in
1414        let ty_te,ugraph2 = type_of_aux ~logger context te ugraph1 in
1415        let b,ugraph3 =
1416          R.are_convertible ~subst ~metasenv context ty_te ty ugraph2
1417        in
1418          if b then
1419            ty,ugraph3
1420          else
1421            raise (TypeCheckerFailure
1422                     (lazy (sprintf "Invalid cast %s" (CicPp.ppterm t))))
1423     | C.Prod (name,s,t) ->
1424        let sort1,ugraph1 = type_of_aux ~logger context s ugraph in
1425        let sort2,ugraph2 =
1426          type_of_aux ~logger  ((Some (name,(C.Decl s)))::context) t ugraph1
1427        in
1428        sort_of_prod ~subst context (name,s) (sort1,sort2) ugraph2
1429    | C.Lambda (n,s,t) ->
1430        let sort1,ugraph1 = type_of_aux ~logger context s ugraph in
1431        (match R.whd ~subst context sort1 with
1432            C.Meta _
1433          | C.Sort _ -> ()
1434          | _ ->
1435            raise
1436             (TypeCheckerFailure (lazy (sprintf
1437               "Not well-typed lambda-abstraction: the source %s should be a type; instead it is a term of type %s" (CicPp.ppterm s)
1438                 (CicPp.ppterm sort1))))
1439        ) ;
1440        let type2,ugraph2 =
1441          type_of_aux ~logger ((Some (n,(C.Decl s)))::context) t ugraph1
1442        in
1443          (C.Prod (n,s,type2)),ugraph2
1444    | C.LetIn (n,s,ty,t) ->
1445       (* only to check if s is well-typed *)
1446       let ty',ugraph1 = type_of_aux ~logger context s ugraph in
1447       let _,ugraph1 = type_of_aux ~logger context ty ugraph1 in
1448       let b,ugraph1 =
1449        R.are_convertible ~subst ~metasenv context ty' ty ugraph1
1450       in
1451        if not b then
1452         raise
1453          (TypeCheckerFailure
1454            (lazy (sprintf
1455              "The type of %s is %s but it is expected to be %s"
1456                (CicPp.ppterm s) (CicPp.ppterm ty') (CicPp.ppterm ty))))
1457        else
1458        (* The type of a LetIn is a LetIn. Extremely slow since the computed
1459           LetIn is later reduced and maybe also re-checked.
1460        (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t))
1461        *)
1462        (* The type of the LetIn is reduced. Much faster than the previous
1463           solution. Moreover the inferred type is probably very different
1464           from the expected one.
1465        (CicReduction.whd ~subst context
1466         (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)))
1467        *)
1468        (* One-step LetIn reduction. Even faster than the previous solution.
1469           Moreover the inferred type is closer to the expected one. *)
1470        let ty1,ugraph2 =
1471          type_of_aux ~logger
1472            ((Some (n,(C.Def (s,ty))))::context) t ugraph1
1473        in
1474        (CicSubstitution.subst ~avoid_beta_redexes:true s ty1),ugraph2
1475    | C.Appl (he::tl) when List.length tl > 0 ->
1476        let hetype,ugraph1 = type_of_aux ~logger context he ugraph in
1477        let tlbody_and_type,ugraph2 =
1478          List.fold_right (
1479            fun x (l,ugraph) ->
1480              let ty,ugraph1 = type_of_aux ~logger context x ugraph in
1481              (*let _,ugraph1 = type_of_aux ~logger  context ty ugraph1 in*)
1482                ((x,ty)::l,ugraph1))
1483            tl ([],ugraph1)
1484        in
1485          (* TASSI: questa c'era nel mio... ma non nel CVS... *)
1486          (* let _,ugraph2 = type_of_aux context hetype ugraph2 in *)
1487          eat_prods ~subst context hetype tlbody_and_type ugraph2
1488    | C.Appl _ -> raise (AssertFailure (lazy "Appl: no arguments"))
1489    | C.Const (uri,exp_named_subst) ->
1490        incr fdebug ;
1491        let ugraph1 =
1492          check_exp_named_subst uri ~logger ~subst  context exp_named_subst ugraph
1493        in
1494        let cty,ugraph2 = type_of_constant ~logger uri ugraph1 in
1495        let cty1 =
1496          CicSubstitution.subst_vars exp_named_subst cty
1497        in
1498          decr fdebug ;
1499          cty1,ugraph2
1500    | C.MutInd (uri,i,exp_named_subst) ->
1501       incr fdebug ;
1502        let ugraph1 =
1503          check_exp_named_subst uri ~logger  ~subst context exp_named_subst ugraph
1504        in
1505        let mty,ugraph2 = type_of_mutual_inductive_defs ~logger uri i ugraph1 in
1506        let cty =
1507          CicSubstitution.subst_vars exp_named_subst mty
1508        in
1509          decr fdebug ;
1510          cty,ugraph2
1511    | C.MutConstruct (uri,i,j,exp_named_subst) ->
1512        let ugraph1 =
1513          check_exp_named_subst uri ~logger ~subst context exp_named_subst ugraph
1514        in
1515        let mty,ugraph2 =
1516          type_of_mutual_inductive_constr ~logger uri i j ugraph1
1517        in
1518        let cty =
1519          CicSubstitution.subst_vars exp_named_subst mty
1520        in
1521          cty,ugraph2
1522    | C.MutCase (uri,i,outtype,term,pl) ->
1523       let outsort,ugraph1 = type_of_aux ~logger context outtype ugraph in
1524       let (need_dummy, k) =
1525       let rec guess_args context t =
1526         let outtype = CicReduction.whd ~subst context t in
1527           match outtype with
1528               C.Sort _ -> (true, 0)
1529             | C.Prod (name, s, t) ->
1530                 let (b, n) =
1531                   guess_args ((Some (name,(C.Decl s)))::context) t in
1532                   if n = 0 then
1533                   (* last prod before sort *)
1534                     match CicReduction.whd ~subst context s with
1535 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1536                         C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
1537                           (false, 1)
1538 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1539                       | C.Appl ((C.MutInd (uri',i',_)) :: _)
1540                           when U.eq uri' uri && i' = i -> (false, 1)
1541                       | _ -> (true, 1)
1542                   else
1543                     (b, n + 1)
1544             | _ ->
1545                 raise
1546                   (TypeCheckerFailure
1547                      (lazy (sprintf
1548                         "Malformed case analasys' output type %s"
1549                         (CicPp.ppterm outtype))))
1550       in
1551 (*
1552       let (parameters, arguments, exp_named_subst),ugraph2 =
1553         let ty,ugraph2 = type_of_aux context term ugraph1 in
1554           match R.whd ~subst context ty with
1555            (*CSC manca il caso dei CAST *)
1556 (*CSC: ma servono i parametri (uri,i)? Se si', perche' non serve anche il *)
1557 (*CSC: parametro exp_named_subst? Se no, perche' non li togliamo?         *)
1558 (*CSC: Hint: nella DTD servono per gli stylesheet.                        *)
1559               C.MutInd (uri',i',exp_named_subst) as typ ->
1560                 if U.eq uri uri' && i = i' then
1561                   ([],[],exp_named_subst),ugraph2
1562                 else
1563                   raise
1564                     (TypeCheckerFailure
1565                       (lazy (sprintf
1566                           ("Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}")
1567                           (CicPp.ppterm typ) (U.string_of_uri uri) i)))
1568             | C.Appl
1569                 ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
1570                 if U.eq uri uri' && i = i' then
1571                   let params,args =
1572                     split tl (List.length tl - k)
1573                   in (params,args,exp_named_subst),ugraph2
1574                 else
1575                   raise
1576                     (TypeCheckerFailure
1577                       (lazy (sprintf
1578                           ("Case analysys: analysed term type is %s, "^
1579                            "but is expected to be (an application of) "^
1580                            "%s#1/%d{_}")
1581                           (CicPp.ppterm typ') (U.string_of_uri uri) i)))
1582             | _ ->
1583                 raise
1584                   (TypeCheckerFailure
1585                     (lazy (sprintf
1586                         ("Case analysis: "^
1587                          "analysed term %s is not an inductive one")
1588                         (CicPp.ppterm term))))
1589 *)
1590       let (b, k) = guess_args context outsort in
1591           if not b then (b, k - 1) else (b, k) in
1592       let (parameters, arguments, exp_named_subst),ugraph2 =
1593         let ty,ugraph2 = type_of_aux ~logger context term ugraph1 in
1594         match R.whd ~subst context ty with
1595             C.MutInd (uri',i',exp_named_subst) as typ ->
1596               if U.eq uri uri' && i = i' then
1597                 ([],[],exp_named_subst),ugraph2
1598               else raise
1599                 (TypeCheckerFailure
1600                   (lazy (sprintf
1601                       ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}")
1602                       (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i)))
1603           | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) ->
1604               if U.eq uri uri' && i = i' then
1605                 let params,args =
1606                   split tl (List.length tl - k)
1607                 in (params,args,exp_named_subst),ugraph2
1608               else raise
1609                 (TypeCheckerFailure
1610                   (lazy (sprintf
1611                       ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}")
1612                       (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i)))
1613           | _ ->
1614               raise
1615                 (TypeCheckerFailure
1616                   (lazy (sprintf
1617                       "Case analysis: analysed term %s is not an inductive one"
1618                       (CicPp.ppterm term))))
1619       in
1620         (*
1621            let's control if the sort elimination is allowed:
1622            [(I q1 ... qr)|B]
1623         *)
1624       let sort_of_ind_type =
1625         if parameters = [] then
1626           C.MutInd (uri,i,exp_named_subst)
1627         else
1628           C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters)
1629       in
1630       let type_of_sort_of_ind_ty,ugraph3 =
1631         type_of_aux ~logger context sort_of_ind_type ugraph2 in
1632       let b,ugraph4 =
1633         check_allowed_sort_elimination ~subst ~metasenv ~logger  context uri i
1634           need_dummy sort_of_ind_type type_of_sort_of_ind_ty outsort ugraph3
1635       in
1636         if not b then
1637         raise
1638           (TypeCheckerFailure (lazy ("Case analysis: sort elimination not allowed")));
1639         (* let's check if the type of branches are right *)
1640       let parsno,constructorsno =
1641         let obj,_ =
1642           try
1643             CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
1644           with Not_found -> assert false
1645         in
1646         match obj with
1647             C.InductiveDefinition (il,_,parsno,_) ->
1648              let _,_,_,cl =
1649               try List.nth il i with Failure _ -> assert false
1650              in
1651               parsno, List.length cl
1652           | _ ->
1653               raise (TypeCheckerFailure
1654                 (lazy ("Unknown mutual inductive definition:" ^
1655                   UriManager.string_of_uri uri)))
1656       in
1657       if List.length pl <> constructorsno then
1658        raise (TypeCheckerFailure
1659         (lazy ("Wrong number of cases in case analysis"))) ;
1660       let (_,branches_ok,ugraph5) =
1661         List.fold_left
1662           (fun (j,b,ugraph) p ->
1663             if b then
1664               let cons =
1665                 if parameters = [] then
1666                   (C.MutConstruct (uri,i,j,exp_named_subst))
1667                 else
1668                   (C.Appl
1669                      (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
1670               in
1671               let ty_p,ugraph1 = type_of_aux ~logger context p ugraph in
1672               let ty_cons,ugraph3 = type_of_aux ~logger context cons ugraph1 in
1673               (* 2 is skipped *)
1674               let ty_branch =
1675                 type_of_branch ~subst context parsno need_dummy outtype cons
1676                   ty_cons in
1677               let b1,ugraph4 =
1678                 R.are_convertible
1679                   ~subst ~metasenv context ty_p ty_branch ugraph3
1680               in
1681 (* Debugging code
1682 if not b1 then
1683 begin
1684 prerr_endline ("\n!OUTTYPE= " ^ CicPp.ppterm outtype);
1685 prerr_endline ("!CONS= " ^ CicPp.ppterm cons);
1686 prerr_endline ("!TY_CONS= " ^ CicPp.ppterm ty_cons);
1687 prerr_endline ("#### " ^ CicPp.ppterm ty_p ^ "\n<==>\n" ^ CicPp.ppterm ty_branch);
1688 end;
1689 *)
1690               if not b1 then
1691                 debug_print (lazy
1692                   ("#### " ^ CicPp.ppterm ty_p ^
1693                   " <==> " ^ CicPp.ppterm ty_branch));
1694               (j + 1,b1,ugraph4)
1695             else
1696               (j,false,ugraph)
1697           ) (1,true,ugraph4) pl
1698          in
1699           if not branches_ok then
1700            raise
1701             (TypeCheckerFailure (lazy "Case analysys: wrong branch type"));
1702           let arguments' =
1703            if not need_dummy then outtype::arguments@[term]
1704            else outtype::arguments in
1705           let outtype =
1706            if need_dummy && arguments = [] then outtype
1707            else CicReduction.head_beta_reduce (C.Appl arguments')
1708           in
1709            outtype,ugraph5
1710    | C.Fix (i,fl) ->
1711       let types,kl,ugraph1,len =
1712         List.fold_left
1713           (fun (types,kl,ugraph,len) (n,k,ty,_) ->
1714             let _,ugraph1 = type_of_aux ~logger context ty ugraph in
1715              (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
1716               k::kl,ugraph1,len+1)
1717           ) ([],[],ugraph,0) fl
1718       in
1719       let ugraph2 =
1720         List.fold_left
1721           (fun ugraph (name,x,ty,bo) ->
1722              let ty_bo,ugraph1 =
1723                type_of_aux ~logger (types@context) bo ugraph
1724              in
1725              let b,ugraph2 =
1726                R.are_convertible ~subst ~metasenv (types@context)
1727                  ty_bo (CicSubstitution.lift len ty) ugraph1 in
1728                if b then
1729                  begin
1730                    let (m, eaten, context') =
1731                      eat_lambdas ~subst (types @ context) (x + 1) bo
1732                    in
1733                    let rec_uri, rec_uri_len =
1734                     let he =
1735                      match List.hd context' with
1736                         Some (_,Cic.Decl he) -> he
1737                       | _ -> assert false
1738                     in
1739                      match CicReduction.whd ~subst (List.tl context') he with
1740                      | Cic.MutInd (uri,_,_)
1741                      | Cic.Appl (Cic.MutInd (uri,_,_)::_) ->
1742                          uri,
1743                            (match
1744                             CicEnvironment.get_obj
1745                              CicUniv.oblivion_ugraph uri
1746                            with
1747                            | Cic.InductiveDefinition (tl,_,_,_), _ ->
1748                                List.length tl
1749                            | _ -> assert false)
1750                      | _ -> assert false
1751                    in
1752                      (*
1753                        let's control the guarded by
1754                        destructors conditions D{f,k,x,M}
1755                      *)
1756                      if not (guarded_by_destructors ~logger ~metasenv ~subst
1757                        rec_uri rec_uri_len context' eaten (len + eaten) kl
1758                        1 [] m)
1759                      then
1760                        raise
1761                          (TypeCheckerFailure
1762                            (lazy ("Fix: not guarded by destructors:"^CicPp.ppterm t)))
1763                      else
1764                        ugraph2
1765                  end
1766                else
1767                  raise (TypeCheckerFailure (lazy ("Fix: ill-typed bodies")))
1768           ) ugraph1 fl in
1769         (*CSC: controlli mancanti solo su D{f,k,x,M} *)
1770       let (_,_,ty,_) = List.nth fl i in
1771         ty,ugraph2
1772    | C.CoFix (i,fl) ->
1773        let types,ugraph1,len =
1774          List.fold_left
1775            (fun (l,ugraph,len) (n,ty,_) ->
1776               let _,ugraph1 =
1777                 type_of_aux ~logger context ty ugraph in
1778                 (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::l,
1779                  ugraph1,len+1)
1780            ) ([],ugraph,0) fl
1781        in
1782        let ugraph2 =
1783          List.fold_left
1784            (fun ugraph (_,ty,bo) ->
1785               let ty_bo,ugraph1 =
1786                 type_of_aux ~logger (types @ context) bo ugraph
1787               in
1788               let b,ugraph2 =
1789                 R.are_convertible ~subst ~metasenv (types @ context) ty_bo
1790                   (CicSubstitution.lift len ty) ugraph1
1791               in
1792                 if b then
1793                   begin
1794                     (* let's control that the returned type is coinductive *)
1795                     match returns_a_coinductive ~subst context ty with
1796                         None ->
1797                           raise
1798                           (TypeCheckerFailure
1799                             (lazy "CoFix: does not return a coinductive type"))
1800                       | Some uri ->
1801                           (*
1802                             let's control the guarded by constructors
1803                             conditions C{f,M}
1804                           *)
1805                           if not (guarded_by_constructors ~logger ~subst ~metasenv uri
1806                  (types @ context) 0 len false bo) then
1807                             raise
1808                               (TypeCheckerFailure
1809                                 (lazy "CoFix: not guarded by constructors"))
1810                           else
1811                           ugraph2
1812                   end
1813                 else
1814                   raise
1815                     (TypeCheckerFailure (lazy "CoFix: ill-typed bodies"))
1816            ) ugraph1 fl
1817        in
1818        let (_,ty,_) = List.nth fl i in
1819          ty,ugraph2
1820
1821  and check_exp_named_subst uri ~logger ~subst context ens ugraph =
1822    let params =
1823     let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1824     (match obj with
1825         Cic.Constant (_,_,_,params,_) -> params
1826       | Cic.Variable (_,_,_,params,_) -> params
1827       | Cic.CurrentProof (_,_,_,_,params,_) -> params
1828       | Cic.InductiveDefinition (_,params,_,_) -> params
1829     ) in
1830    let rec check_same_order params ens =
1831     match params,ens with
1832      | _,[] -> ()
1833      | [],_::_ ->
1834         raise (TypeCheckerFailure (lazy "Bad explicit named substitution"))
1835      | uri::tl,(uri',_)::tl' when UriManager.eq uri uri' ->
1836         check_same_order tl tl'
1837      | _::tl,l -> check_same_order tl l
1838    in
1839    let rec check_exp_named_subst_aux ~logger esubsts l ugraph =
1840      match l with
1841          [] -> ugraph
1842        | ((uri,t) as item)::tl ->
1843            let ty_uri,ugraph1 = type_of_variable ~logger uri ugraph in
1844            let typeofvar =
1845              CicSubstitution.subst_vars esubsts ty_uri in
1846            let typeoft,ugraph2 = type_of_aux ~logger context t ugraph1 in
1847            let b,ugraph3 =
1848              CicReduction.are_convertible ~subst ~metasenv
1849                context typeoft typeofvar ugraph2
1850            in
1851              if b then
1852                check_exp_named_subst_aux ~logger (esubsts@[item]) tl ugraph3
1853              else
1854                begin
1855                  CicReduction.fdebug := 0 ;
1856                  ignore
1857                    (CicReduction.are_convertible
1858                       ~subst ~metasenv context typeoft typeofvar ugraph2) ;
1859                  fdebug := 0 ;
1860                  debug typeoft [typeofvar] ;
1861                  raise (TypeCheckerFailure (lazy "Wrong Explicit Named Substitution"))
1862                end
1863    in
1864     check_same_order params ens ;
1865     check_exp_named_subst_aux ~logger [] ens ugraph
1866
1867  and sort_of_prod ~subst context (name,s) (t1, t2) ugraph =
1868   let module C = Cic in
1869    let t1' = CicReduction.whd ~subst context t1 in
1870    let t2' = CicReduction.whd ~subst ((Some (name,C.Decl s))::context) t2 in
1871    match (t1', t2') with
1872     | (C.Sort s1, C.Sort (C.Prop | C.Set)) ->
1873          (* different from Coq manual!!! *)
1874          t2',ugraph
1875     | (C.Sort (C.Type t1 | C.CProp t1), C.Sort (C.Type t2)) ->
1876        let t' = CicUniv.fresh() in
1877         (try
1878          let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1879          let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1880           C.Sort (C.Type t'),ugraph2
1881         with
1882          CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
1883     | (C.Sort (C.CProp t1 | C.Type t1), C.Sort (C.CProp t2)) ->
1884        let t' = CicUniv.fresh() in
1885         (try
1886          let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1887          let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1888           C.Sort (C.CProp t'),ugraph2
1889         with
1890          CicUniv.UniverseInconsistency msg -> raise (TypeCheckerFailure msg))
1891     | (C.Sort _,C.Sort (C.Type t1)) -> C.Sort (C.Type t1),ugraph
1892     | (C.Sort _,C.Sort (C.CProp t1)) -> C.Sort (C.CProp t1),ugraph
1893     | (C.Meta _, C.Sort _) -> t2',ugraph
1894     | (C.Meta _, (C.Meta (_,_) as t))
1895     | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
1896         t2',ugraph
1897     | (_,_) -> raise (TypeCheckerFailure (lazy (sprintf
1898         "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1')
1899           (CicPp.ppterm t2'))))
1900
1901  and eat_prods ~subst context hetype l ugraph =
1902    (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
1903    (*CSC: cucinati                                                         *)
1904    match l with
1905        [] -> hetype,ugraph
1906      | (hete, hety)::tl ->
1907          (match (CicReduction.whd ~subst context hetype) with
1908               Cic.Prod (n,s,t) ->
1909                 let b,ugraph1 =
1910 (*if (match hety,s with Cic.Sort _,Cic.Sort _ -> false | _,_ -> true) && hety <> s then(
1911 prerr_endline ("AAA22: " ^ CicPp.ppterm hete ^ ": " ^ CicPp.ppterm hety ^ " <==> " ^ CicPp.ppterm s); let res = CicReduction.are_convertible ~subst ~metasenv context hety s ugraph in prerr_endline "#"; res) else*)
1912                   CicReduction.are_convertible
1913                     ~subst ~metasenv context hety s ugraph
1914                 in
1915                   if b then
1916                     begin
1917                       CicReduction.fdebug := -1 ;
1918                       eat_prods ~subst context
1919                         (CicSubstitution.subst ~avoid_beta_redexes:true hete t)
1920                          tl ugraph1
1921                         (*TASSI: not sure *)
1922                     end
1923                   else
1924                     begin
1925                       CicReduction.fdebug := 0 ;
1926                       ignore (CicReduction.are_convertible
1927                                 ~subst ~metasenv context s hety ugraph) ;
1928                       fdebug := 0 ;
1929                       debug s [hety] ;
1930                       raise
1931                         (TypeCheckerFailure
1932                           (lazy (sprintf
1933                               ("Appl: wrong parameter-type, expected %s, found %s")
1934                               (CicPp.ppterm hetype) (CicPp.ppterm s))))
1935                     end
1936             | _ ->
1937                 raise (TypeCheckerFailure
1938                         (lazy "Appl: this is not a function, it cannot be applied"))
1939          )
1940
1941  and returns_a_coinductive ~subst context ty =
1942   let module C = Cic in
1943    match CicReduction.whd ~subst context ty with
1944       C.MutInd (uri,i,_) ->
1945        (*CSC: definire una funzioncina per questo codice sempre replicato *)
1946         let obj,_ =
1947           try
1948             CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
1949           with Not_found -> assert false
1950         in
1951         (match obj with
1952            C.InductiveDefinition (itl,_,_,_) ->
1953             let (_,is_inductive,_,_) = List.nth itl i in
1954              if is_inductive then None else (Some uri)
1955          | _ ->
1956             raise (TypeCheckerFailure
1957               (lazy ("Unknown mutual inductive definition:" ^
1958               UriManager.string_of_uri uri)))
1959         )
1960     | C.Appl ((C.MutInd (uri,i,_))::_) ->
1961        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1962          match o with
1963            C.InductiveDefinition (itl,_,_,_) ->
1964             let (_,is_inductive,_,_) = List.nth itl i in
1965              if is_inductive then None else (Some uri)
1966          | _ ->
1967             raise (TypeCheckerFailure
1968               (lazy ("Unknown mutual inductive definition:" ^
1969               UriManager.string_of_uri uri)))
1970         )
1971     | C.Prod (n,so,de) ->
1972        returns_a_coinductive ~subst ((Some (n,C.Decl so))::context) de
1973     | _ -> None
1974
1975  in
1976 (*CSC
1977 debug_print (lazy ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t)) ; flush stderr ;
1978 let res =
1979 *)
1980   type_of_aux ~logger context t ugraph
1981 (*
1982 in debug_print (lazy "FINE TYPE_OF_AUX") ; flush stderr ; res
1983 *)
1984
1985 (* is a small constructor? *)
1986 (*CSC: ottimizzare calcolando staticamente *)
1987 and is_small_or_non_informative ~condition ~logger context paramsno c ugraph =
1988  let rec is_small_or_non_informative_aux ~logger context c ugraph =
1989   let module C = Cic in
1990    match CicReduction.whd context c with
1991       C.Prod (n,so,de) ->
1992        let s,ugraph1 = type_of_aux' ~logger [] context so ugraph in
1993        let b = condition s in
1994        if b then
1995          is_small_or_non_informative_aux
1996           ~logger ((Some (n,(C.Decl so)))::context) de ugraph1
1997        else
1998                 false,ugraph1
1999     | _ -> true,ugraph (*CSC: we trust the type-checker *)
2000  in
2001   let (context',dx) = split_prods ~subst:[] context paramsno c in
2002    is_small_or_non_informative_aux ~logger context' dx ugraph
2003
2004 and is_small ~logger =
2005  is_small_or_non_informative
2006   ~condition:(fun s -> s=Cic.Sort Cic.Prop || s=Cic.Sort Cic.Set)
2007   ~logger
2008
2009 and is_non_informative ~logger =
2010  is_small_or_non_informative
2011   ~condition:(fun s -> s=Cic.Sort Cic.Prop)
2012   ~logger
2013
2014 and type_of ~logger t ugraph =
2015 (*CSC
2016 debug_print (lazy ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t)) ; flush stderr ;
2017 let res =
2018 *)
2019  type_of_aux' ~logger [] [] t ugraph
2020 (*CSC
2021 in debug_print (lazy "FINE TYPE_OF_AUX'") ; flush stderr ; res
2022 *)
2023 ;;
2024
2025 let typecheck_obj0 ~logger uri (obj,unchecked_ugraph) =
2026  let module C = Cic in
2027  let ugraph = CicUniv.empty_ugraph in
2028  let inferred_ugraph =
2029    match obj with
2030     | C.Constant (_,Some te,ty,_,_) ->
2031         let _,ugraph = type_of ~logger ty ugraph in
2032         let ty_te,ugraph = type_of ~logger te ugraph in
2033         let b,ugraph = (CicReduction.are_convertible [] ty_te ty ugraph) in
2034          if not b then
2035            raise (TypeCheckerFailure
2036             (lazy
2037               ("the type of the body is not the one expected:\n" ^
2038                CicPp.ppterm ty_te ^ "\nvs\n" ^
2039                CicPp.ppterm ty)))
2040          else
2041           ugraph
2042      | C.Constant (_,None,ty,_,_) ->
2043         (* only to check that ty is well-typed *)
2044         let _,ugraph = type_of ~logger ty ugraph in
2045          ugraph
2046      | C.CurrentProof (_,conjs,te,ty,_,_) ->
2047         (* this block is broken since the metasenv should
2048          * be topologically sorted before typing metas *)
2049         ignore(assert false);
2050         let _,ugraph =
2051          List.fold_left
2052           (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
2053             let _,ugraph =
2054              type_of_aux' ~logger metasenv context ty ugraph
2055             in
2056              metasenv @ [conj],ugraph
2057           ) ([],ugraph) conjs
2058         in
2059          let _,ugraph = type_of_aux' ~logger conjs [] ty ugraph in
2060          let type_of_te,ugraph =
2061           type_of_aux' ~logger conjs [] te ugraph
2062          in
2063          let b,ugraph = CicReduction.are_convertible [] type_of_te ty ugraph in
2064           if not b then
2065             raise (TypeCheckerFailure (lazy (sprintf
2066              "the current proof is not well typed because the type %s of the body is not convertible to the declared type %s"
2067              (CicPp.ppterm type_of_te) (CicPp.ppterm ty))))
2068           else
2069            ugraph
2070      | C.Variable (_,bo,ty,_,_) ->
2071         (* only to check that ty is well-typed *)
2072         let _,ugraph = type_of ~logger ty ugraph in
2073          (match bo with
2074              None -> ugraph
2075            | Some bo ->
2076               let ty_bo,ugraph = type_of ~logger bo ugraph in
2077                 let b,ugraph = CicReduction.are_convertible [] ty_bo ty ugraph in
2078                if not b then
2079                 raise (TypeCheckerFailure
2080                  (lazy "the body is not the one expected"))
2081                else
2082                 ugraph
2083               )
2084      | (C.InductiveDefinition _ as obj) ->
2085         check_mutual_inductive_defs ~logger uri obj ugraph
2086  in
2087    check_and_clean_ugraph inferred_ugraph unchecked_ugraph uri obj
2088 ;;
2089
2090 let typecheck ?(trust=true) uri =
2091  let module C = Cic in
2092  let module R = CicReduction in
2093  let module U = UriManager in
2094  let logger = new CicLogger.logger in
2095    match CicEnvironment.is_type_checked ~trust CicUniv.empty_ugraph uri with
2096    | CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
2097    | CicEnvironment.UncheckedObj (uobj,unchecked_ugraph) ->
2098       (* let's typecheck the uncooked object *)
2099       logger#log (`Start_type_checking uri) ;
2100       let ugraph, ul, obj = typecheck_obj0 ~logger uri (uobj,unchecked_ugraph) in
2101       CicEnvironment.set_type_checking_info uri (obj,ugraph,ul);
2102       logger#log (`Type_checking_completed uri);
2103       match CicEnvironment.is_type_checked ~trust CicUniv.empty_ugraph uri with
2104       | CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
2105       | _ -> raise CicEnvironmentError
2106 ;;
2107
2108 let typecheck_obj ~logger uri obj =
2109  let ugraph,univlist,obj = typecheck_obj0 ~logger uri (obj,None) in
2110  CicEnvironment.add_type_checked_obj uri (obj,ugraph,univlist)
2111
2112 (** wrappers which instantiate fresh loggers *)
2113
2114 let profiler = HExtlib.profile "K/CicTypeChecker.type_of_aux'"
2115
2116 let type_of_aux' ?(subst = []) metasenv context t ugraph =
2117   let logger = new CicLogger.logger in
2118   profiler.HExtlib.profile
2119     (type_of_aux' ~logger ~subst metasenv context t) ugraph
2120
2121 let typecheck_obj uri obj =
2122  let logger = new CicLogger.logger in
2123  typecheck_obj ~logger uri obj
2124
2125 (* check_allowed_sort_elimination uri i s1 s2
2126    This function is used outside the kernel to determine in advance whether
2127    a MutCase will be allowed or not.
2128    [uri,i] is the type of the term to match
2129    [s1] is the sort of the term to eliminate (i.e. the head of the arity
2130         of the inductive type [uri,i])
2131    [s2] is the sort of the goal (i.e. the head of the type of the outtype
2132         of the MutCase) *)
2133 let check_allowed_sort_elimination uri i s1 s2 =
2134  fst (check_allowed_sort_elimination ~subst:[] ~metasenv:[]
2135   ~logger:(new CicLogger.logger) [] uri i true
2136   (Cic.Implicit None) (* never used *) (Cic.Sort s1) (Cic.Sort s2)
2137   CicUniv.empty_ugraph)
2138 ;;
2139
2140 Deannotate.type_of_aux' :=
2141  fun context t ->
2142   ignore (
2143   List.fold_right
2144    (fun el context ->
2145       (match el with
2146           None -> ()
2147         | Some (_,Cic.Decl ty) ->
2148            ignore (type_of_aux' [] context ty CicUniv.empty_ugraph)
2149         | Some (_,Cic.Def (bo,ty)) ->
2150            ignore (type_of_aux' [] context ty CicUniv.empty_ugraph);
2151            ignore (type_of_aux' [] context bo CicUniv.empty_ugraph));
2152       el::context
2153    ) context []);
2154   fst (type_of_aux' [] context t CicUniv.empty_ugraph);;