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