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