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 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 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 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 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               List.fold_right
 771                (fun (p,(_,c)) i ->
 772                  let rl' =
 773                   let debrujinedte = debrujin_constructor uri len c in
 774                    recursive_args tys 0 len debrujinedte
 775                  in
 776                   let (e,safes',n',nn',x',context') =
 777                    get_new_safes ~subst context p c rl' safes n nn x
 778                   in
 779                    i &&
 780                    check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
 781                ) (List.combine pl cl) true
 782         | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
 783            let (tys,len,isinductive,paramsno,cl) =
 784             let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 785             match o with
 786                C.InductiveDefinition (tl,_,paramsno,_) ->
 787                 let (_,isinductive,_,cl) = List.nth tl i in
 788                  let tys =
 789                   List.map (fun (n,_,ty,_) ->
 790                    Some(Cic.Name n,(Cic.Decl ty))) tl
 791                  in
 792                   let cl' =
 793                    List.map
 794                     (fun (id,ty) ->
 795                       (id, snd (split_prods ~subst tys paramsno ty))) cl
 796                   in
 797                    (tys,List.length tl,isinductive,paramsno,cl')
 798              | _ ->
 799                 raise (TypeCheckerFailure
 800                   ("Unknown mutual inductive definition:" ^
 801                   UriManager.string_of_uri uri))
 802            in
 803             if not isinductive then
 804               List.fold_right
 805                (fun p i ->
 806                  i && check_is_really_smaller_arg ~subst context n nn kl x safes p)
 807                pl true
 808             else
 809               (*CSC: supponiamo come prima che nessun controllo sia necessario*)
 810               (*CSC: sugli argomenti di una applicazione                      *)
 811               List.fold_right
 812                (fun (p,(_,c)) i ->
 813                  let rl' =
 814                   let debrujinedte = debrujin_constructor uri len c in
 815                    recursive_args tys 0 len debrujinedte
 816                  in
 817                   let (e, safes',n',nn',x',context') =
 818                    get_new_safes context p c rl' safes n nn x
 819                   in
 820                    i &&
 821                    check_is_really_smaller_arg ~subst context' n' nn' kl x' safes' e
 822                ) (List.combine pl cl) true
 823         | _ ->
 824           List.fold_right
 825            (fun p i ->
 826              i && check_is_really_smaller_arg ~subst context n nn kl x safes p
 827            ) pl true
 828       )
 829    | C.Fix (_, fl) ->
 830       let len = List.length fl in
 831        let n_plus_len = n + len
 832        and nn_plus_len = nn + len
 833        and x_plus_len = x + len
 834        and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
 835        and safes' = List.map (fun x -> x + len) safes in
 836         List.fold_right
 837          (fun (_,_,ty,bo) i ->
 838            i &&
 839             check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl
 840              x_plus_len safes' bo
 841          ) fl true
 842    | C.CoFix (_, fl) ->
 843       let len = List.length fl in
 844        let n_plus_len = n + len
 845        and nn_plus_len = nn + len
 846        and x_plus_len = x + len
 847        and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
 848        and safes' = List.map (fun x -> x + len) safes in
 849         List.fold_right
 850          (fun (_,ty,bo) i ->
 851            i &&
 852             check_is_really_smaller_arg ~subst (tys@context) n_plus_len nn_plus_len kl
 853              x_plus_len safes' bo
 854          ) fl true
 855
 856 and guarded_by_destructors ?(subst = []) context n nn kl x safes =
 857  let module C = Cic in
 858  let module U = UriManager in
 859   function
 860      C.Rel m when m > n && m <= nn -> false
 861    | C.Rel m ->
 862       (match List.nth context (n-1) with
 863           Some (_,C.Decl _) -> true
 864         | Some (_,C.Def (bo,_)) ->
 865            guarded_by_destructors context m nn kl x safes
 866             (CicSubstitution.lift m bo)
 867         | None -> raise (TypeCheckerFailure "Reference to deleted hypothesis")
 868       )
 869    | C.Meta _
 870    | C.Sort _
 871    | C.Implicit _ -> true
 872    | C.Cast (te,ty) ->
 873       guarded_by_destructors context n nn kl x safes te &&
 874        guarded_by_destructors context n nn kl x safes ty
 875    | C.Prod (name,so,ta) ->
 876       guarded_by_destructors context n nn kl x safes so &&
 877        guarded_by_destructors ((Some (name,(C.Decl so)))::context)
 878         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 879    | C.Lambda (name,so,ta) ->
 880       guarded_by_destructors context n nn kl x safes so &&
 881        guarded_by_destructors ((Some (name,(C.Decl so)))::context)
 882         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 883    | C.LetIn (name,so,ta) ->
 884       guarded_by_destructors context n nn kl x safes so &&
 885        guarded_by_destructors ((Some (name,(C.Def (so,None))))::context)
 886         (n+1) (nn+1) kl (x+1) (List.map (fun x -> x + 1) safes) ta
 887    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
 888       let k = List.nth kl (m - n - 1) in
 889        if not (List.length tl > k) then false
 890        else
 891         List.fold_right
 892          (fun param i ->
 893            i && guarded_by_destructors context n nn kl x safes param
 894          ) tl true &&
 895          check_is_really_smaller_arg ~subst context n nn kl x safes (List.nth tl k)
 896    | C.Appl tl ->
 897       List.fold_right
 898        (fun t i -> i && guarded_by_destructors context n nn kl x safes t)
 899        tl true
 900    | C.Var (_,exp_named_subst)
 901    | C.Const (_,exp_named_subst)
 902    | C.MutInd (_,_,exp_named_subst)
 903    | C.MutConstruct (_,_,_,exp_named_subst) ->
 904       List.fold_right
 905        (fun (_,t) i -> i && guarded_by_destructors context n nn kl x safes t)
 906        exp_named_subst true
 907    | C.MutCase (uri,i,outtype,term,pl) ->
 908       (match CicReduction.whd context term with
 909           C.Rel m when List.mem m safes || m = x ->
 910            let (tys,len,isinductive,paramsno,cl) =
 911             let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 912             match o with
 913                C.InductiveDefinition (tl,_,paramsno,_) ->
 914                 let len = List.length tl in
 915                  let (_,isinductive,_,cl) = List.nth tl i in
 916                   let tys =
 917                    List.map (fun (n,_,ty,_) ->
 918                     Some(Cic.Name n,(Cic.Decl ty))) tl
 919                   in
 920                    let cl' =
 921                     List.map
 922                      (fun (id,ty) ->
 923                       let debrujinedty = debrujin_constructor uri len ty in
 924                        (id, snd (split_prods ~subst tys paramsno ty),
 925                         snd (split_prods ~subst tys paramsno debrujinedty)
 926                        )) cl
 927                    in
 928                     (tys,len,isinductive,paramsno,cl')
 929              | _ ->
 930                 raise (TypeCheckerFailure
 931                   ("Unknown mutual inductive definition:" ^
 932                   UriManager.string_of_uri uri))
 933            in
 934             if not isinductive then
 935              guarded_by_destructors context n nn kl x safes outtype &&
 936               guarded_by_destructors context n nn kl x safes term &&
 937               (*CSC: manca ??? il controllo sul tipo di term? *)
 938               List.fold_right
 939                (fun p i ->
 940                  i && guarded_by_destructors context n nn kl x safes p)
 941                pl true
 942             else
 943              guarded_by_destructors context n nn kl x safes outtype &&
 944               (*CSC: manca ??? il controllo sul tipo di term? *)
 945               List.fold_right
 946                (fun (p,(_,c,brujinedc)) i ->
 947                  let rl' = recursive_args tys 0 len brujinedc in
 948                   let (e,safes',n',nn',x',context') =
 949                    get_new_safes context p c rl' safes n nn x
 950                   in
 951                    i &&
 952                    guarded_by_destructors context' n' nn' kl x' safes' e
 953                ) (List.combine pl cl) true
 954         | C.Appl ((C.Rel m)::tl) when List.mem m safes || m = x ->
 955            let (tys,len,isinductive,paramsno,cl) =
 956             let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 957             match o with
 958                C.InductiveDefinition (tl,_,paramsno,_) ->
 959                 let (_,isinductive,_,cl) = List.nth tl i in
 960                  let tys =
 961                   List.map
 962                    (fun (n,_,ty,_) -> Some(Cic.Name n,(Cic.Decl ty))) tl
 963                  in
 964                   let cl' =
 965                    List.map
 966                     (fun (id,ty) ->
 967                       (id, snd (split_prods ~subst tys paramsno ty))) cl
 968                   in
 969                    (tys,List.length tl,isinductive,paramsno,cl')
 970              | _ ->
 971                 raise (TypeCheckerFailure
 972                   ("Unknown mutual inductive definition:" ^
 973                   UriManager.string_of_uri uri))
 974            in
 975             if not isinductive then
 976              guarded_by_destructors context n nn kl x safes outtype &&
 977               guarded_by_destructors context n nn kl x safes term &&
 978               (*CSC: manca ??? il controllo sul tipo di term? *)
 979               List.fold_right
 980                (fun p i ->
 981                  i && guarded_by_destructors context n nn kl x safes p)
 982                pl true
 983             else
 984              guarded_by_destructors context n nn kl x safes outtype &&
 985               (*CSC: manca ??? il controllo sul tipo di term? *)
 986               List.fold_right
 987                (fun t i ->
 988                  i && guarded_by_destructors context n nn kl x safes t)
 989                tl true &&
 990               List.fold_right
 991                (fun (p,(_,c)) i ->
 992                  let rl' =
 993                   let debrujinedte = debrujin_constructor uri len c in
 994                    recursive_args tys 0 len debrujinedte
 995                  in
 996                   let (e, safes',n',nn',x',context') =
 997                    get_new_safes context p c rl' safes n nn x
 998                   in
 999                    i &&
1000                    guarded_by_destructors context' n' nn' kl x' safes' e
1001                ) (List.combine pl cl) true
1002         | _ ->
1003           guarded_by_destructors context n nn kl x safes outtype &&
1004            guarded_by_destructors context n nn kl x safes term &&
1005            (*CSC: manca ??? il controllo sul tipo di term? *)
1006            List.fold_right
1007             (fun p i -> i && guarded_by_destructors context n nn kl x safes p)
1008             pl true
1009       )
1010    | C.Fix (_, fl) ->
1011       let len = List.length fl in
1012        let n_plus_len = n + len
1013        and nn_plus_len = nn + len
1014        and x_plus_len = x + len
1015        and tys = List.map (fun (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
1016        and safes' = List.map (fun x -> x + len) safes in
1017         List.fold_right
1018          (fun (_,_,ty,bo) i ->
1019            i && guarded_by_destructors context n nn kl x_plus_len safes' ty &&
1020             guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
1021              x_plus_len safes' bo
1022          ) fl true
1023    | C.CoFix (_, fl) ->
1024       let len = List.length fl in
1025        let n_plus_len = n + len
1026        and nn_plus_len = nn + len
1027        and x_plus_len = x + len
1028        and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl
1029        and safes' = List.map (fun x -> x + len) safes in
1030         List.fold_right
1031          (fun (_,ty,bo) i ->
1032            i &&
1033             guarded_by_destructors context n nn kl x_plus_len safes' ty &&
1034             guarded_by_destructors (tys@context) n_plus_len nn_plus_len kl
1035              x_plus_len safes' bo
1036          ) fl true
1037
1038 (* the boolean h means already protected *)
1039 (* args is the list of arguments the type of the constructor that may be *)
1040 (* found in head position must be applied to.                            *)
1041 (*CSC: coInductiveTypeURI non cambia mai di ricorsione in ricorsione *)
1042 and guarded_by_constructors context n nn h te args coInductiveTypeURI =
1043  let module C = Cic in
1044   (*CSC: There is a lot of code replication between the cases X and    *)
1045   (*CSC: (C.Appl X tl). Maybe it will be better to define a function   *)
1046   (*CSC: that maps X into (C.Appl X []) when X is not already a C.Appl *)
1047   match CicReduction.whd context te with
1048      C.Rel m when m > n && m <= nn -> h
1049    | C.Rel _ -> true
1050    | C.Meta _
1051    | C.Sort _
1052    | C.Implicit _
1053    | C.Cast _
1054    | C.Prod _
1055    | C.LetIn _ ->
1056       (* the term has just been type-checked *)
1057       raise (AssertFailure "17")
1058    | C.Lambda (name,so,de) ->
1059       does_not_occur context n nn so &&
1060        guarded_by_constructors ((Some (name,(C.Decl so)))::context)
1061         (n + 1) (nn + 1) h de args coInductiveTypeURI
1062    | C.Appl ((C.Rel m)::tl) when m > n && m <= nn ->
1063       h &&
1064        List.fold_right (fun x i -> i && does_not_occur context n nn x) tl true
1065    | C.Appl ((C.MutConstruct (uri,i,j,exp_named_subst))::tl) ->
1066       let consty =
1067         let obj,_ =
1068           try
1069             CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
1070           with Not_found -> assert false
1071         in
1072        match obj with
1073           C.InductiveDefinition (itl,_,_,_) ->
1074            let (_,_,_,cl) = List.nth itl i in
1075             let (_,cons) = List.nth cl (j - 1) in
1076              CicSubstitution.subst_vars exp_named_subst cons
1077         | _ ->
1078             raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1079               UriManager.string_of_uri uri))
1080       in
1081        let rec analyse_branch context ty te =
1082         match CicReduction.whd context ty with
1083            C.Meta _ -> raise (AssertFailure "34")
1084          | C.Rel _
1085          | C.Var _
1086          | C.Sort _ ->
1087             does_not_occur context n nn te
1088          | C.Implicit _
1089          | C.Cast _ ->
1090             raise (AssertFailure "24")(* due to type-checking *)
1091          | C.Prod (name,so,de) ->
1092             analyse_branch ((Some (name,(C.Decl so)))::context) de te
1093          | C.Lambda _
1094          | C.LetIn _ ->
1095             raise (AssertFailure "25")(* due to type-checking *)
1096          | C.Appl ((C.MutInd (uri,_,_))::_) as ty
1097             when uri == coInductiveTypeURI ->
1098              guarded_by_constructors context n nn true te [] coInductiveTypeURI
1099          | C.Appl ((C.MutInd (uri,_,_))::_) as ty ->
1100             guarded_by_constructors context n nn true te tl coInductiveTypeURI
1101          | C.Appl _ ->
1102             does_not_occur context n nn te
1103          | C.Const _ -> raise (AssertFailure "26")
1104          | C.MutInd (uri,_,_) when uri == coInductiveTypeURI ->
1105             guarded_by_constructors context n nn true te [] coInductiveTypeURI
1106          | C.MutInd _ ->
1107             does_not_occur context n nn te
1108          | C.MutConstruct _ -> raise (AssertFailure "27")
1109          (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
1110          (*CSC: in head position.                                       *)
1111          | C.MutCase _
1112          | C.Fix _
1113          | C.CoFix _ ->
1114             raise (AssertFailure "28")(* due to type-checking *)
1115        in
1116        let rec analyse_instantiated_type context ty l =
1117         match CicReduction.whd context ty with
1118            C.Rel _
1119          | C.Var _
1120          | C.Meta _
1121          | C.Sort _
1122          | C.Implicit _
1123          | C.Cast _ -> raise (AssertFailure "29")(* due to type-checking *)
1124          | C.Prod (name,so,de) ->
1125             begin
1126              match l with
1127                 [] -> true
1128               | he::tl ->
1129                  analyse_branch context so he &&
1130                   analyse_instantiated_type
1131                    ((Some (name,(C.Decl so)))::context) de tl
1132             end
1133          | C.Lambda _
1134          | C.LetIn _ ->
1135             raise (AssertFailure "30")(* due to type-checking *)
1136          | C.Appl _ ->
1137             List.fold_left
1138              (fun i x -> i && does_not_occur context n nn x) true l
1139          | C.Const _ -> raise (AssertFailure "31")
1140          | C.MutInd _ ->
1141             List.fold_left
1142              (fun i x -> i && does_not_occur context n nn x) true l
1143          | C.MutConstruct _ -> raise (AssertFailure "32")
1144          (*CSC: we do not consider backbones with a MutCase, Fix, Cofix *)
1145          (*CSC: in head position.                                       *)
1146          | C.MutCase _
1147          | C.Fix _
1148          | C.CoFix _ ->
1149             raise (AssertFailure "33")(* due to type-checking *)
1150        in
1151         let rec instantiate_type args consty =
1152          function
1153             [] -> true
1154           | tlhe::tltl as l ->
1155              let consty' = CicReduction.whd context consty in
1156               match args with
1157                  he::tl ->
1158                   begin
1159                    match consty' with
1160                       C.Prod (_,_,de) ->
1161                        let instantiated_de = CicSubstitution.subst he de in
1162                         (*CSC: siamo sicuri che non sia troppo forte? *)
1163                         does_not_occur context n nn tlhe &
1164                          instantiate_type tl instantiated_de tltl
1165                     | _ ->
1166                       (*CSC:We do not consider backbones with a MutCase, a    *)
1167                       (*CSC:FixPoint, a CoFixPoint and so on in head position.*)
1168                       raise (AssertFailure "23")
1169                   end
1170                | [] -> analyse_instantiated_type context consty' l
1171                   (* These are all the other cases *)
1172        in
1173         instantiate_type args consty tl
1174    | C.Appl ((C.CoFix (_,fl))::tl) ->
1175       List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
1176        let len = List.length fl in
1177         let n_plus_len = n + len
1178         and nn_plus_len = nn + len
1179         (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1180         and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1181          List.fold_right
1182           (fun (_,ty,bo) i ->
1183             i && does_not_occur context n nn ty &&
1184              guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1185               args coInductiveTypeURI
1186           ) fl true
1187    | C.Appl ((C.MutCase (_,_,out,te,pl))::tl) ->
1188        List.fold_left (fun i x -> i && does_not_occur context n nn x) true tl &&
1189         does_not_occur context n nn out &&
1190          does_not_occur context n nn te &&
1191           List.fold_right
1192            (fun x i ->
1193              i &&
1194              guarded_by_constructors context n nn h x args coInductiveTypeURI
1195            ) pl true
1196    | C.Appl l ->
1197       List.fold_right (fun x i -> i && does_not_occur context n nn x) l true
1198    | C.Var (_,exp_named_subst)
1199    | C.Const (_,exp_named_subst) ->
1200       List.fold_right
1201        (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
1202    | C.MutInd _ -> assert false
1203    | C.MutConstruct (_,_,_,exp_named_subst) ->
1204       List.fold_right
1205        (fun (_,x) i -> i && does_not_occur context n nn x) exp_named_subst true
1206    | C.MutCase (_,_,out,te,pl) ->
1207        does_not_occur context n nn out &&
1208         does_not_occur context n nn te &&
1209          List.fold_right
1210           (fun x i ->
1211             i &&
1212              guarded_by_constructors context n nn h x args coInductiveTypeURI
1213           ) pl true
1214    | C.Fix (_,fl) ->
1215       let len = List.length fl in
1216        let n_plus_len = n + len
1217        and nn_plus_len = nn + len
1218        (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1219        and tys = List.map (fun (n,_,ty,_)-> Some (C.Name n,(C.Decl ty))) fl in
1220         List.fold_right
1221          (fun (_,_,ty,bo) i ->
1222            i && does_not_occur context n nn ty &&
1223             does_not_occur (tys@context) n_plus_len nn_plus_len bo
1224          ) fl true
1225    | C.CoFix (_,fl) ->
1226       let len = List.length fl in
1227        let n_plus_len = n + len
1228        and nn_plus_len = nn + len
1229        (*CSC: Is a Decl of the ty ok or should I use Def of a Fix? *)
1230        and tys = List.map (fun (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl in
1231         List.fold_right
1232          (fun (_,ty,bo) i ->
1233            i && does_not_occur context n nn ty &&
1234             guarded_by_constructors (tys@context) n_plus_len nn_plus_len h bo
1235              args coInductiveTypeURI
1236          ) fl true
1237
1238 and check_allowed_sort_elimination ~logger context uri i need_dummy ind
1239   arity1 arity2 ugraph =
1240  let module C = Cic in
1241  let module U = UriManager in
1242   match (CicReduction.whd context arity1, CicReduction.whd context arity2) with
1243      (C.Prod (_,so1,de1), C.Prod (_,so2,de2)) ->
1244        let b,ugraph1 = CicReduction.are_convertible context so1 so2 ugraph in
1245        if b then
1246          check_allowed_sort_elimination ~logger context uri i need_dummy
1247            (C.Appl [CicSubstitution.lift 1 ind ; C.Rel 1]) de1 de2 ugraph1
1248        else
1249          false,ugraph1
1250    | (C.Sort C.Prop, C.Sort C.Prop) when need_dummy -> true,ugraph
1251    | (C.Sort C.Prop, C.Sort C.Set)
1252    | (C.Sort C.Prop, C.Sort C.CProp)
1253    | (C.Sort C.Prop, C.Sort (C.Type _) ) when need_dummy ->
1254    (* TASSI: da verificare *)
1255 (*CSC: WRONG. MISSING CONDITIONS ON THE ARGUMENTS OF THE CONSTRUTOR *)
1256        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1257          match o with
1258          C.InductiveDefinition (itl,_,_,_) ->
1259            let (_,_,_,cl) = List.nth itl i in
1260            (* is a singleton definition or the empty proposition? *)
1261            (List.length cl = 1 || List.length cl = 0) , ugraph
1262          | _ ->
1263              raise (TypeCheckerFailure
1264                       ("Unknown mutual inductive definition:" ^
1265                        UriManager.string_of_uri uri))
1266        )
1267    | (C.Sort C.Set, C.Sort C.Prop) when need_dummy -> true , ugraph
1268    | (C.Sort C.CProp, C.Sort C.Prop) when need_dummy -> true , ugraph
1269    | (C.Sort C.Set, C.Sort C.Set) when need_dummy -> true , ugraph
1270    | (C.Sort C.Set, C.Sort C.CProp) when need_dummy -> true , ugraph
1271    | (C.Sort C.CProp, C.Sort C.Set) when need_dummy -> true , ugraph
1272    | (C.Sort C.CProp, C.Sort C.CProp) when need_dummy -> true , ugraph
1273    | ((C.Sort C.Set, C.Sort (C.Type _)) | (C.Sort C.CProp, C.Sort (C.Type _)))
1274       (* TASSI: da verificare *)
1275       when need_dummy ->
1276        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1277          match o with
1278            C.InductiveDefinition (itl,_,paramsno,_) ->
1279             let tys =
1280              List.map (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1281             in
1282              let (_,_,_,cl) = List.nth itl i in
1283               (List.fold_right
1284                (fun (_,x) (i,ugraph) ->
1285                  if i then
1286                    is_small ~logger tys paramsno x ugraph
1287                  else
1288                    false,ugraph
1289                     ) cl (true,ugraph))
1290            | _ ->
1291             raise (TypeCheckerFailure ("Unknown mutual inductive definition:" ^
1292               UriManager.string_of_uri uri))
1293        )
1294    | (C.Sort (C.Type _), C.Sort _) when need_dummy -> true , ugraph
1295      (* TASSI: da verificare *)
1296    | (C.Sort C.Prop, C.Prod (name,so,ta)) when not need_dummy ->
1297        let b,ugraph1 = CicReduction.are_convertible context so ind ugraph in
1298        if not b then
1299          false,ugraph1
1300        else
1301          (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1302               C.Sort C.Prop -> true,ugraph1
1303            | (C.Sort C.Set | C.Sort C.CProp | C.Sort (C.Type _)) ->
1304                (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1305                  match o with
1306                     C.InductiveDefinition (itl,_,_,_) ->
1307                      let (_,_,_,cl) = List.nth itl i in
1308                      (* is a singleton definition or the empty proposition? *)
1309                      (List.length cl = 1 || List.length cl = 0),ugraph1
1310                   | _ ->
1311                    raise (TypeCheckerFailure
1312                     ("Unknown mutual inductive definition:" ^
1313                        UriManager.string_of_uri uri)))
1314            | _ -> false,ugraph1)
1315    | ((C.Sort C.Set, C.Prod (name,so,ta))
1316    | (C.Sort C.CProp, C.Prod (name,so,ta)))
1317      when not need_dummy ->
1318        let b,ugraph1 = CicReduction.are_convertible context so ind ugraph in
1319        if not b then
1320          false,ugraph1
1321        else
1322          (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1323            C.Sort C.Prop
1324          | C.Sort C.Set  -> true,ugraph1
1325          | C.Sort C.CProp -> true,ugraph1
1326          | C.Sort (C.Type _) ->
1327              (* TASSI: da verificare *)
1328              (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1329                match o with
1330                C.InductiveDefinition (itl,_,paramsno,_) ->
1331                  let (_,_,_,cl) = List.nth itl i in
1332                  let tys =
1333                    List.map
1334                      (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1335                  in
1336                  (List.fold_right
1337                    (fun (_,x) (i,ugraph) ->
1338                       if i then
1339                         is_small ~logger tys paramsno x ugraph
1340                       else
1341                         false,ugraph
1342                    ) cl (true,ugraph1))
1343              | _ ->
1344                  raise (TypeCheckerFailure
1345                           ("Unknown mutual inductive definition:" ^
1346                            UriManager.string_of_uri uri))
1347              )
1348          | _ -> raise (AssertFailure "19")
1349          )
1350    | (C.Sort (C.Type _), C.Prod (_,so,_)) when not need_dummy ->
1351        (* TASSI: da verificare *)
1352        CicReduction.are_convertible context so ind ugraph
1353    | (_,_) -> false,ugraph
1354
1355 and type_of_branch context argsno need_dummy outtype term constype =
1356  let module C = Cic in
1357  let module R = CicReduction in
1358   match R.whd context constype with
1359      C.MutInd (_,_,_) ->
1360       if need_dummy then
1361        outtype
1362       else
1363        C.Appl [outtype ; term]
1364    | C.Appl (C.MutInd (_,_,_)::tl) ->
1365       let (_,arguments) = split tl argsno
1366       in
1367        if need_dummy && arguments = [] then
1368         outtype
1369        else
1370         C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
1371    | C.Prod (name,so,de) ->
1372       let term' =
1373        match CicSubstitution.lift 1 term with
1374           C.Appl l -> C.Appl (l@[C.Rel 1])
1375         | t -> C.Appl [t ; C.Rel 1]
1376       in
1377        C.Prod (C.Anonymous,so,type_of_branch
1378         ((Some (name,(C.Decl so)))::context) argsno need_dummy
1379         (CicSubstitution.lift 1 outtype) term' de)
1380   | _ -> raise (AssertFailure "20")
1381
1382 (* check_metasenv_consistency checks that the "canonical" context of a
1383 metavariable is consitent - up to relocation via the relocation list l -
1384 with the actual context *)
1385
1386
1387 and check_metasenv_consistency ~logger ?(subst=[]) metasenv context
1388   canonical_context l ugraph
1389 =
1390   let module C = Cic in
1391   let module R = CicReduction in
1392   let module S = CicSubstitution in
1393   let lifted_canonical_context =
1394     let rec aux i =
1395      function
1396          [] -> []
1397        | (Some (n,C.Decl t))::tl ->
1398            (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
1399        | (Some (n,C.Def (t,None)))::tl ->
1400            (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
1401        | None::tl -> None::(aux (i+1) tl)
1402        | (Some (n,C.Def (t,Some ty)))::tl ->
1403            (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)
1404     in
1405      aux 1 canonical_context
1406    in
1407    List.fold_left2
1408      (fun ugraph t ct ->
1409        match (t,ct) with
1410        | _,None -> ugraph
1411        | Some t,Some (_,C.Def (ct,_)) ->
1412            let b,ugraph1 =
1413              R.are_convertible ~subst ~metasenv context t ct ugraph
1414            in
1415            if not b then
1416              raise
1417                (TypeCheckerFailure
1418                   (sprintf "Not well typed metavariable local context: expected a term convertible with %s, found %s" (CicPp.ppterm ct) (CicPp.ppterm t)))
1419            else
1420              ugraph1
1421        | Some t,Some (_,C.Decl ct) ->
1422            let type_t,ugraph1 =
1423              type_of_aux' ~logger ~subst metasenv context t ugraph
1424            in
1425            let b,ugraph2 =
1426              R.are_convertible ~subst ~metasenv context type_t ct ugraph1
1427            in
1428            if not b then
1429              raise (TypeCheckerFailure
1430                       (sprintf "Not well typed metavariable local context: expected a term of type %s, found %s of type %s"
1431                          (CicPp.ppterm ct) (CicPp.ppterm t)
1432                          (CicPp.ppterm type_t)))
1433            else
1434              ugraph2
1435        | None, _  ->
1436            raise (TypeCheckerFailure
1437                     ("Not well typed metavariable local context: "^
1438                      "an hypothesis, that is not hidden, is not instantiated"))
1439      ) ugraph l lifted_canonical_context
1440
1441
1442 (*
1443    type_of_aux' is just another name (with a different scope)
1444    for type_of_aux
1445 *)
1446
1447 and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
1448  let rec type_of_aux ~logger context t ugraph =
1449   let module C = Cic in
1450   let module R = CicReduction in
1451   let module S = CicSubstitution in
1452   let module U = UriManager in
1453    match t with
1454       C.Rel n ->
1455        (try
1456          match List.nth context (n - 1) with
1457             Some (_,C.Decl t) -> S.lift n t,ugraph
1458           | Some (_,C.Def (_,Some ty)) -> S.lift n ty,ugraph
1459           | Some (_,C.Def (bo,None)) ->
1460              debug_print "##### CASO DA INVESTIGARE E CAPIRE" ;
1461               type_of_aux ~logger context (S.lift n bo) ugraph
1462           | None -> raise
1463               (TypeCheckerFailure "Reference to deleted hypothesis")
1464         with
1465         _ ->
1466           raise (TypeCheckerFailure "unbound variable")
1467        )
1468     | C.Var (uri,exp_named_subst) ->
1469       incr fdebug ;
1470         let ugraph1 =
1471           check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
1472         in
1473         let ty,ugraph2 = type_of_variable ~logger uri ugraph1 in
1474         let ty1 = CicSubstitution.subst_vars exp_named_subst ty in
1475           decr fdebug ;
1476           ty1,ugraph2
1477     | C.Meta (n,l) ->
1478        (try
1479           let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in
1480           let ugraph1 =
1481             check_metasenv_consistency ~logger
1482               ~subst metasenv context canonical_context l ugraph
1483           in
1484             (* assuming subst is well typed !!!!! *)
1485             ((CicSubstitution.subst_meta l ty), ugraph1)
1486               (* type_of_aux context (CicSubstitution.subst_meta l term) *)
1487         with CicUtil.Subst_not_found _ ->
1488           let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
1489           let ugraph1 =
1490             check_metasenv_consistency ~logger
1491               ~subst metasenv context canonical_context l ugraph
1492           in
1493             ((CicSubstitution.subst_meta l ty),ugraph1))
1494       (* TASSI: CONSTRAINTS *)
1495     | C.Sort (C.Type t) ->
1496        let t' = CicUniv.fresh() in
1497        let ugraph1 = CicUniv.add_gt t' t ugraph in
1498          (C.Sort (C.Type t')),ugraph1
1499       (* TASSI: CONSTRAINTS *)
1500     | C.Sort s -> (C.Sort (C.Type (CicUniv.fresh ()))),ugraph
1501     | C.Implicit _ -> raise (AssertFailure "21")
1502     | C.Cast (te,ty) as t ->
1503        let _,ugraph1 = type_of_aux ~logger context ty ugraph in
1504        let ty_te,ugraph2 = type_of_aux ~logger context te ugraph1 in
1505        let b,ugraph3 =
1506          R.are_convertible ~subst ~metasenv context ty_te ty ugraph2
1507        in
1508          if b then
1509            ty,ugraph3
1510          else
1511            raise (TypeCheckerFailure
1512                     (sprintf "Invalid cast %s" (CicPp.ppterm t)))
1513     | C.Prod (name,s,t) ->
1514        let sort1,ugraph1 = type_of_aux ~logger context s ugraph in
1515        let sort2,ugraph2 =
1516          type_of_aux ~logger  ((Some (name,(C.Decl s)))::context) t ugraph1
1517        in
1518        sort_of_prod ~subst context (name,s) (sort1,sort2) ugraph2
1519    | C.Lambda (n,s,t) ->
1520        let sort1,ugraph1 = type_of_aux ~logger context s ugraph in
1521        (match R.whd ~subst context sort1 with
1522            C.Meta _
1523          | C.Sort _ -> ()
1524          | _ ->
1525            raise
1526             (TypeCheckerFailure (sprintf
1527               "Not well-typed lambda-abstraction: the source %s should be a type; instead it is a term of type %s" (CicPp.ppterm s)
1528                 (CicPp.ppterm sort1)))
1529        ) ;
1530        let type2,ugraph2 =
1531          type_of_aux ~logger ((Some (n,(C.Decl s)))::context) t ugraph1
1532        in
1533          (C.Prod (n,s,type2)),ugraph2
1534    | C.LetIn (n,s,t) ->
1535       (* only to check if s is well-typed *)
1536       let ty,ugraph1 = type_of_aux ~logger context s ugraph in
1537        (* The type of a LetIn is a LetIn. Extremely slow since the computed
1538           LetIn is later reduced and maybe also re-checked.
1539        (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t))
1540        *)
1541        (* The type of the LetIn is reduced. Much faster than the previous
1542           solution. Moreover the inferred type is probably very different
1543           from the expected one.
1544        (CicReduction.whd context
1545         (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)))
1546        *)
1547        (* One-step LetIn reduction. Even faster than the previous solution.
1548           Moreover the inferred type is closer to the expected one. *)
1549        let ty1,ugraph2 =
1550          type_of_aux ~logger
1551            ((Some (n,(C.Def (s,Some ty))))::context) t ugraph1
1552        in
1553        (CicSubstitution.subst s ty1),ugraph2
1554    | C.Appl (he::tl) when List.length tl > 0 ->
1555        let hetype,ugraph1 = type_of_aux ~logger context he ugraph in
1556        let tlbody_and_type,ugraph2 =
1557          List.fold_right (
1558            fun x (l,ugraph) ->
1559              let ty,ugraph1 = type_of_aux ~logger context x ugraph in
1560              let _,ugraph1 = type_of_aux ~logger  context ty ugraph1 in
1561                ((x,ty)::l,ugraph1))
1562            tl ([],ugraph1)
1563        in
1564          (* TASSI: questa c'era nel mio... ma non nel CVS... *)
1565          (* let _,ugraph2 = type_of_aux context hetype ugraph2 in *)
1566          eat_prods ~subst context hetype tlbody_and_type ugraph2
1567    | C.Appl _ -> raise (AssertFailure "Appl: no arguments")
1568    | C.Const (uri,exp_named_subst) ->
1569        incr fdebug ;
1570        let ugraph1 =
1571          check_exp_named_subst ~logger ~subst  context exp_named_subst ugraph
1572        in
1573        let cty,ugraph2 = type_of_constant ~logger uri ugraph1 in
1574        let cty1 =
1575          CicSubstitution.subst_vars exp_named_subst cty
1576        in
1577          decr fdebug ;
1578          cty1,ugraph2
1579    | C.MutInd (uri,i,exp_named_subst) ->
1580       incr fdebug ;
1581        let ugraph1 =
1582          check_exp_named_subst ~logger  ~subst context exp_named_subst ugraph
1583        in
1584          (* TASSI: da me c'era anche questa, ma in CVS no *)
1585        let mty,ugraph2 = type_of_mutual_inductive_defs ~logger uri i ugraph1 in
1586          (* fine parte dubbia *)
1587        let cty =
1588          CicSubstitution.subst_vars exp_named_subst mty
1589        in
1590          decr fdebug ;
1591          cty,ugraph2
1592    | C.MutConstruct (uri,i,j,exp_named_subst) ->
1593        let ugraph1 =
1594          check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
1595        in
1596          (* TASSI: idem come sopra *)
1597        let mty,ugraph2 =
1598          type_of_mutual_inductive_constr ~logger uri i j ugraph1
1599        in
1600        let cty =
1601          CicSubstitution.subst_vars exp_named_subst mty
1602        in
1603          cty,ugraph2
1604    | C.MutCase (uri,i,outtype,term,pl) ->
1605       let outsort,ugraph1 = type_of_aux ~logger context outtype ugraph in
1606       let (need_dummy, k) =
1607       let rec guess_args context t =
1608         let outtype = CicReduction.whd ~subst context t in
1609           match outtype with
1610               C.Sort _ -> (true, 0)
1611             | C.Prod (name, s, t) ->
1612                 let (b, n) =
1613                   guess_args ((Some (name,(C.Decl s)))::context) t in
1614                   if n = 0 then
1615                   (* last prod before sort *)
1616                     match CicReduction.whd ~subst context s with
1617 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1618                         C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
1619                           (false, 1)
1620 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1621                       | C.Appl ((C.MutInd (uri',i',_)) :: _)
1622                           when U.eq uri' uri && i' = i -> (false, 1)
1623                       | _ -> (true, 1)
1624                   else
1625                     (b, n + 1)
1626             | _ ->
1627                 raise
1628                   (TypeCheckerFailure
1629                      (sprintf
1630                         "Malformed case analasys' output type %s"
1631                         (CicPp.ppterm outtype)))
1632       in
1633 (*
1634       let (parameters, arguments, exp_named_subst),ugraph2 =
1635         let ty,ugraph2 = type_of_aux context term ugraph1 in
1636           match R.whd context ty with
1637            (*CSC manca il caso dei CAST *)
1638 (*CSC: ma servono i parametri (uri,i)? Se si', perche' non serve anche il *)
1639 (*CSC: parametro exp_named_subst? Se no, perche' non li togliamo?         *)
1640 (*CSC: Hint: nella DTD servono per gli stylesheet.                        *)
1641               C.MutInd (uri',i',exp_named_subst) as typ ->
1642                 if U.eq uri uri' && i = i' then
1643                   ([],[],exp_named_subst),ugraph2
1644                 else
1645                   raise
1646                     (TypeCheckerFailure
1647                        (sprintf
1648                           ("Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}")
1649                           (CicPp.ppterm typ) (U.string_of_uri uri) i))
1650             | C.Appl
1651                 ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
1652                 if U.eq uri uri' && i = i' then
1653                   let params,args =
1654                     split tl (List.length tl - k)
1655                   in (params,args,exp_named_subst),ugraph2
1656                 else
1657                   raise
1658                     (TypeCheckerFailure
1659                        (sprintf
1660                           ("Case analysys: analysed term type is %s, "^
1661                            "but is expected to be (an application of) "^
1662                            "%s#1/%d{_}")
1663                           (CicPp.ppterm typ') (U.string_of_uri uri) i))
1664             | _ ->
1665                 raise
1666                   (TypeCheckerFailure
1667                      (sprintf
1668                         ("Case analysis: "^
1669                          "analysed term %s is not an inductive one")
1670                         (CicPp.ppterm term)))
1671 *)
1672       let (b, k) = guess_args context outsort in
1673           if not b then (b, k - 1) else (b, k) in
1674       let (parameters, arguments, exp_named_subst),ugraph2 =
1675         let ty,ugraph2 = type_of_aux ~logger context term ugraph1 in
1676         match R.whd ~subst context ty with
1677             C.MutInd (uri',i',exp_named_subst) as typ ->
1678               if U.eq uri uri' && i = i' then
1679                 ([],[],exp_named_subst),ugraph2
1680               else raise
1681                 (TypeCheckerFailure
1682                    (sprintf
1683                       ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}")
1684                       (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i))
1685           | C.Appl
1686               ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
1687               if U.eq uri uri' && i = i' then
1688                 let params,args =
1689                   split tl (List.length tl - k)
1690                 in (params,args,exp_named_subst),ugraph2
1691               else raise
1692                 (TypeCheckerFailure
1693                    (sprintf
1694                       ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}")
1695                       (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i))
1696           | _ ->
1697               raise
1698                 (TypeCheckerFailure
1699                    (sprintf
1700                       "Case analysis: analysed term %s is not an inductive one"
1701                       (CicPp.ppterm term)))
1702       in
1703         (*
1704            let's control if the sort elimination is allowed:
1705            [(I q1 ... qr)|B]
1706         *)
1707       let sort_of_ind_type =
1708         if parameters = [] then
1709           C.MutInd (uri,i,exp_named_subst)
1710         else
1711           C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters)
1712       in
1713       let type_of_sort_of_ind_ty,ugraph3 =
1714         type_of_aux ~logger context sort_of_ind_type ugraph2 in
1715       let b,ugraph4 =
1716         check_allowed_sort_elimination ~logger  context uri i need_dummy
1717           sort_of_ind_type type_of_sort_of_ind_ty outsort ugraph3
1718       in
1719         if not b then
1720         raise
1721           (TypeCheckerFailure ("Case analasys: sort elimination not allowed"));
1722         (* let's check if the type of branches are right *)
1723       let parsno =
1724         let obj,_ =
1725           try
1726             CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
1727           with Not_found -> assert false
1728         in
1729         match obj with
1730             C.InductiveDefinition (_,_,parsno,_) -> parsno
1731           | _ ->
1732               raise (TypeCheckerFailure
1733                 ("Unknown mutual inductive definition:" ^
1734                   UriManager.string_of_uri uri))
1735         in
1736       let (_,branches_ok,ugraph5) =
1737         List.fold_left
1738           (fun (j,b,ugraph) p ->
1739             if b then
1740               let cons =
1741                 if parameters = [] then
1742                   (C.MutConstruct (uri,i,j,exp_named_subst))
1743                 else
1744                   (C.Appl
1745                      (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
1746               in
1747               let ty_p,ugraph1 = type_of_aux ~logger context p ugraph in
1748               let ty_cons,ugraph3 = type_of_aux ~logger context cons ugraph1 in
1749               (* 2 is skipped *)
1750               let ty_branch =
1751                 type_of_branch context parsno need_dummy outtype cons
1752                   ty_cons in
1753               let b1,ugraph4 =
1754                 R.are_convertible
1755                   ~subst ~metasenv context ty_p ty_branch ugraph3
1756               in
1757               if not b1 then
1758                 debug_print
1759                   ("#### " ^ CicPp.ppterm ty_p ^
1760                   " <==> " ^ CicPp.ppterm ty_branch);
1761               (j + 1,b1,ugraph4)
1762             else
1763               (j,false,ugraph)
1764           ) (1,true,ugraph4) pl
1765          in
1766           if not branches_ok then
1767            raise
1768             (TypeCheckerFailure "Case analysys: wrong branch type");
1769           let arguments =
1770            if not need_dummy then outtype::arguments@[term]
1771            else outtype::arguments in
1772           let outtype =
1773            if arguments = [] then outtype
1774            else CicReduction.head_beta_reduce (C.Appl arguments)
1775           in
1776            outtype,ugraph5
1777    | C.Fix (i,fl) ->
1778       let types_times_kl,ugraph1 =
1779         (* WAS: list rev list map *)
1780         List.fold_left
1781           (fun (l,ugraph) (n,k,ty,_) ->
1782             let _,ugraph1 = type_of_aux ~logger context ty ugraph in
1783             ((Some (C.Name n,(C.Decl ty)),k)::l,ugraph1)
1784           ) ([],ugraph) fl
1785       in
1786       let (types,kl) = List.split types_times_kl in
1787       let len = List.length types in
1788       let ugraph2 =
1789         List.fold_left
1790           (fun ugraph (name,x,ty,bo) ->
1791              let ty_bo,ugraph1 =
1792                type_of_aux ~logger (types@context) bo ugraph
1793              in
1794              let b,ugraph2 =
1795                R.are_convertible ~subst ~metasenv (types@context)
1796                  ty_bo (CicSubstitution.lift len ty) ugraph1 in
1797                if b then
1798                  begin
1799                    let (m, eaten, context') =
1800                      eat_lambdas ~subst (types @ context) (x + 1) bo
1801                    in
1802                      (*
1803                        let's control the guarded by
1804                        destructors conditions D{f,k,x,M}
1805                      *)
1806                      if not (guarded_by_destructors context' eaten
1807                                (len + eaten) kl 1 [] m) then
1808                        raise
1809                          (TypeCheckerFailure
1810                             ("Fix: not guarded by destructors"))
1811                      else
1812                        ugraph2
1813                  end
1814                else
1815                  raise (TypeCheckerFailure ("Fix: ill-typed bodies"))
1816           ) ugraph1 fl in
1817         (*CSC: controlli mancanti solo su D{f,k,x,M} *)
1818       let (_,_,ty,_) = List.nth fl i in
1819         ty,ugraph2
1820    | C.CoFix (i,fl) ->
1821        let types,ugraph1 =
1822          List.fold_left
1823            (fun (l,ugraph) (n,ty,_) ->
1824               let _,ugraph1 =
1825                 type_of_aux ~logger context ty ugraph in
1826                 (Some (C.Name n,(C.Decl ty))::l,ugraph1)
1827            ) ([],ugraph) fl
1828        in
1829        let len = List.length types in
1830        let ugraph2 =
1831          List.fold_left
1832            (fun ugraph (_,ty,bo) ->
1833               let ty_bo,ugraph1 =
1834                 type_of_aux ~logger (types @ context) bo ugraph
1835               in
1836               let b,ugraph2 =
1837                 R.are_convertible ~subst ~metasenv (types @ context) ty_bo
1838                   (CicSubstitution.lift len ty) ugraph1
1839               in
1840                 if b then
1841                   begin
1842                     (* let's control that the returned type is coinductive *)
1843                     match returns_a_coinductive context ty with
1844                         None ->
1845                           raise
1846                           (TypeCheckerFailure
1847                              ("CoFix: does not return a coinductive type"))
1848                       | Some uri ->
1849                           (*
1850                             let's control the guarded by constructors
1851                             conditions C{f,M}
1852                           *)
1853                           if not (guarded_by_constructors (types @ context)
1854                                     0 len false bo [] uri) then
1855                             raise
1856                               (TypeCheckerFailure
1857                                  ("CoFix: not guarded by constructors"))
1858                           else
1859                           ugraph2
1860                   end
1861                 else
1862                   raise
1863                     (TypeCheckerFailure ("CoFix: ill-typed bodies"))
1864            ) ugraph1 fl
1865        in
1866        let (_,ty,_) = List.nth fl i in
1867          ty,ugraph2
1868
1869  and check_exp_named_subst ~logger ?(subst = []) context ugraph =
1870    let rec check_exp_named_subst_aux ~logger esubsts l ugraph =
1871      match l with
1872          [] -> ugraph
1873        | ((uri,t) as item)::tl ->
1874            let ty_uri,ugraph1 = type_of_variable ~logger uri ugraph in
1875            let typeofvar =
1876              CicSubstitution.subst_vars esubsts ty_uri in
1877            let typeoft,ugraph2 = type_of_aux ~logger context t ugraph1 in
1878            let b,ugraph3 =
1879              CicReduction.are_convertible ~subst ~metasenv
1880                context typeoft typeofvar ugraph2
1881            in
1882              if b then
1883                check_exp_named_subst_aux ~logger (esubsts@[item]) tl ugraph3
1884              else
1885                begin
1886                  CicReduction.fdebug := 0 ;
1887                  ignore
1888                    (CicReduction.are_convertible
1889                       ~subst ~metasenv context typeoft typeofvar ugraph2) ;
1890                  fdebug := 0 ;
1891                  debug typeoft [typeofvar] ;
1892                  raise (TypeCheckerFailure "Wrong Explicit Named Substitution")
1893                end
1894    in
1895      check_exp_named_subst_aux ~logger [] ugraph
1896
1897  and sort_of_prod ?(subst = []) context (name,s) (t1, t2) ugraph =
1898   let module C = Cic in
1899    let t1' = CicReduction.whd ~subst context t1 in
1900    let t2' = CicReduction.whd ~subst ((Some (name,C.Decl s))::context) t2 in
1901    match (t1', t2') with
1902       (C.Sort s1, C.Sort s2)
1903         when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1904          (* different from Coq manual!!! *)
1905          C.Sort s2,ugraph
1906     | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1907       (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
1908        let t' = CicUniv.fresh() in
1909        let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1910        let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1911        C.Sort (C.Type t'),ugraph2
1912     | (C.Sort _,C.Sort (C.Type t1)) ->
1913         (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
1914         C.Sort (C.Type t1),ugraph (* c'e' bisogno di un fresh? *)
1915     | (C.Meta _, C.Sort _) -> t2',ugraph
1916     | (C.Meta _, (C.Meta (_,_) as t))
1917     | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
1918         t2',ugraph
1919     | (_,_) -> raise (TypeCheckerFailure (sprintf
1920         "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1')
1921           (CicPp.ppterm t2')))
1922
1923  and eat_prods ?(subst = []) context hetype l ugraph =
1924    (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
1925    (*CSC: cucinati                                                         *)
1926    match l with
1927        [] -> hetype,ugraph
1928      | (hete, hety)::tl ->
1929          (match (CicReduction.whd ~subst context hetype) with
1930               Cic.Prod (n,s,t) ->
1931                 let b,ugraph1 =
1932                   CicReduction.are_convertible
1933                     ~subst ~metasenv context hety s ugraph
1934                 in
1935                   if b then
1936                     begin
1937                       CicReduction.fdebug := -1 ;
1938                       eat_prods ~subst context
1939                         (CicSubstitution.subst hete t) tl ugraph1
1940                         (*TASSI: not sure *)
1941                     end
1942                   else
1943                     begin
1944                       CicReduction.fdebug := 0 ;
1945                       ignore (CicReduction.are_convertible
1946                                 ~subst ~metasenv context s hety ugraph) ;
1947                       fdebug := 0 ;
1948                       debug s [hety] ;
1949                       raise
1950                         (TypeCheckerFailure
1951                            (sprintf
1952                               ("Appl: wrong parameter-type, expected %s, found %s")
1953                               (CicPp.ppterm hetype) (CicPp.ppterm s)))
1954                     end
1955             | _ ->
1956                 raise (TypeCheckerFailure
1957                          "Appl: this is not a function, it cannot be applied")
1958          )
1959
1960  and returns_a_coinductive context ty =
1961   let module C = Cic in
1962    match CicReduction.whd context ty with
1963       C.MutInd (uri,i,_) ->
1964        (*CSC: definire una funzioncina per questo codice sempre replicato *)
1965         let obj,_ =
1966           try
1967             CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
1968           with Not_found -> assert false
1969         in
1970         (match obj with
1971            C.InductiveDefinition (itl,_,_,_) ->
1972             let (_,is_inductive,_,_) = List.nth itl i in
1973              if is_inductive then None else (Some uri)
1974          | _ ->
1975             raise (TypeCheckerFailure
1976               ("Unknown mutual inductive definition:" ^
1977               UriManager.string_of_uri uri))
1978         )
1979     | C.Appl ((C.MutInd (uri,i,_))::_) ->
1980        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1981          match o with
1982            C.InductiveDefinition (itl,_,_,_) ->
1983             let (_,is_inductive,_,_) = List.nth itl i in
1984              if is_inductive then None else (Some uri)
1985          | _ ->
1986             raise (TypeCheckerFailure
1987               ("Unknown mutual inductive definition:" ^
1988               UriManager.string_of_uri uri))
1989         )
1990     | C.Prod (n,so,de) ->
1991        returns_a_coinductive ((Some (n,C.Decl so))::context) de
1992     | _ -> None
1993
1994  in
1995 (*CSC
1996 debug_print ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t) ; flush stderr ;
1997 let res =
1998 *)
1999   type_of_aux ~logger context t ugraph
2000 (*
2001 in debug_print "FINE TYPE_OF_AUX" ; flush stderr ; res
2002 *)
2003
2004 (* is a small constructor? *)
2005 (*CSC: ottimizzare calcolando staticamente *)
2006 and is_small ~logger context paramsno c ugraph =
2007  let rec is_small_aux ~logger context c ugraph =
2008   let module C = Cic in
2009    match CicReduction.whd context c with
2010       C.Prod (n,so,de) ->
2011        (*CSC: [] is an empty metasenv. Is it correct? *)
2012        let s,ugraph1 = type_of_aux' ~logger [] context so ugraph in
2013        let b = (s = C.Sort C.Prop || s = C.Sort C.Set || s = C.Sort C.CProp) in
2014        if b then
2015          is_small_aux ~logger ((Some (n,(C.Decl so)))::context) de ugraph1
2016        else
2017          false,ugraph1
2018     | _ -> true,ugraph (*CSC: we trust the type-checker *)
2019  in
2020   let (context',dx) = split_prods context paramsno c in
2021    is_small_aux ~logger context' dx ugraph
2022
2023 and type_of ~logger t ugraph =
2024 (*CSC
2025 debug_print ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t) ; flush stderr ;
2026 let res =
2027 *)
2028  type_of_aux' ~logger [] [] t ugraph
2029 (*CSC
2030 in debug_print "FINE TYPE_OF_AUX'" ; flush stderr ; res
2031 *)
2032 ;;
2033
2034 let typecheck_obj0 ~logger uri ugraph =
2035  let module C = Cic in
2036   function
2037      C.Constant (_,Some te,ty,_,_) ->
2038       let _,ugraph = type_of ~logger ty ugraph in
2039       let ty_te,ugraph = type_of ~logger te ugraph in
2040       let b,ugraph = (CicReduction.are_convertible [] ty_te ty ugraph) in
2041        if not b then
2042          raise (TypeCheckerFailure
2043           ("the type of the body is not the one expected"))
2044        else
2045         ugraph
2046    | C.Constant (_,None,ty,_,_) ->
2047       (* only to check that ty is well-typed *)
2048       let _,ugraph = type_of ~logger ty ugraph in
2049        ugraph
2050    | C.CurrentProof (_,conjs,te,ty,_,_) ->
2051       let _,ugraph =
2052        List.fold_left
2053         (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
2054           let _,ugraph =
2055            type_of_aux' ~logger metasenv context ty ugraph
2056           in
2057            metasenv @ [conj],ugraph
2058         ) ([],ugraph) conjs
2059       in
2060        let _,ugraph = type_of_aux' ~logger conjs [] ty ugraph in
2061        let type_of_te,ugraph =
2062         type_of_aux' ~logger conjs [] te ugraph
2063        in
2064        let b,ugraph = CicReduction.are_convertible [] type_of_te ty ugraph in
2065         if not b then
2066           raise (TypeCheckerFailure (sprintf
2067            "the current proof is not well typed because the type %s of the body is not convertible to the declared type %s"
2068            (CicPp.ppterm type_of_te) (CicPp.ppterm ty)))
2069         else
2070          ugraph
2071    | C.Variable (_,bo,ty,_,_) ->
2072       (* only to check that ty is well-typed *)
2073       let _,ugraph = type_of ~logger ty ugraph in
2074        (match bo with
2075            None -> ugraph
2076          | Some bo ->
2077             let ty_bo,ugraph = type_of ~logger bo ugraph in
2078             let b,ugraph = CicReduction.are_convertible [] ty_bo ty ugraph in
2079              if not b then
2080               raise (TypeCheckerFailure
2081                ("the body is not the one expected"))
2082              else
2083               ugraph
2084             )
2085    | (C.InductiveDefinition _ as obj) ->
2086       check_mutual_inductive_defs ~logger uri obj ugraph
2087
2088 let typecheck uri =
2089  let module C = Cic in
2090  let module R = CicReduction in
2091  let module U = UriManager in
2092  let logger = new CicLogger.logger in
2093    (* ??? match CicEnvironment.is_type_checked ~trust:true uri with ???? *)
2094    match CicEnvironment.is_type_checked ~trust:false CicUniv.empty_ugraph uri with
2095      CicEnvironment.CheckedObj (cobj,ugraph') ->
2096        (* debug_print ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri);*)
2097        cobj,ugraph'
2098    | CicEnvironment.UncheckedObj uobj ->
2099       (* let's typecheck the uncooked object *)
2100       logger#log (`Start_type_checking uri) ;
2101       (* debug_print ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri); *)
2102       let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph uobj in
2103         try
2104           CicEnvironment.set_type_checking_info uri;
2105           logger#log (`Type_checking_completed uri);
2106           match CicEnvironment.is_type_checked ~trust:false ugraph uri with
2107               CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
2108             | _ -> raise CicEnvironmentError
2109         with
2110             (*
2111               this is raised if set_type_checking_info is called on an object
2112               that has no associated universe file. If we are in univ_maker
2113               phase this is OK since univ_maker will properly commit the
2114               object.
2115             *)
2116             Invalid_argument s ->
2117               (*debug_print s;*)
2118               uobj,ugraph
2119 ;;
2120
2121 let typecheck_obj ~logger uri obj =
2122  let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph obj in
2123  let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in
2124   CicEnvironment.add_type_checked_obj uri (obj,ugraph)
2125
2126 (** wrappers which instantiate fresh loggers *)
2127
2128 let type_of_aux' ?(subst = []) metasenv context t ugraph =
2129   let logger = new CicLogger.logger in
2130   type_of_aux' ~logger ~subst metasenv context t ugraph
2131
2132 let typecheck_obj uri obj =
2133  let logger = new CicLogger.logger in
2134  typecheck_obj ~logger uri obj