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) ->
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? *)
1309                    List.length cl = 1,ugraph1
1310              | _ ->
1311                  raise (TypeCheckerFailure
1312                           ("Unknown mutual inductive definition:" ^
1313                            UriManager.string_of_uri uri))
1314              )
1315          | _ -> false,ugraph1
1316          )
1317    | ((C.Sort C.Set, C.Prod (name,so,ta))
1318    | (C.Sort C.CProp, C.Prod (name,so,ta)))
1319      when not need_dummy ->
1320        let b,ugraph1 = CicReduction.are_convertible context so ind ugraph in
1321        if not b then
1322          false,ugraph1
1323        else
1324          (match CicReduction.whd ((Some (name,(C.Decl so)))::context) ta with
1325            C.Sort C.Prop
1326          | C.Sort C.Set  -> true,ugraph1
1327          | C.Sort C.CProp -> true,ugraph1
1328          | C.Sort (C.Type _) ->
1329              (* TASSI: da verificare *)
1330              (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1331                match o with
1332                C.InductiveDefinition (itl,_,paramsno,_) ->
1333                  let (_,_,_,cl) = List.nth itl i in
1334                  let tys =
1335                    List.map
1336                      (fun (n,_,ty,_) -> Some (Cic.Name n,(Cic.Decl ty))) itl
1337                  in
1338                  (List.fold_right
1339                    (fun (_,x) (i,ugraph) ->
1340                       if i then
1341                         is_small ~logger tys paramsno x ugraph
1342                       else
1343                         false,ugraph
1344                    ) cl (true,ugraph1))
1345              | _ ->
1346                  raise (TypeCheckerFailure
1347                           ("Unknown mutual inductive definition:" ^
1348                            UriManager.string_of_uri uri))
1349              )
1350          | _ -> raise (AssertFailure "19")
1351          )
1352    | (C.Sort (C.Type _), C.Prod (_,so,_)) when not need_dummy ->
1353        (* TASSI: da verificare *)
1354        CicReduction.are_convertible context so ind ugraph
1355    | (_,_) -> false,ugraph
1356
1357 and type_of_branch context argsno need_dummy outtype term constype =
1358  let module C = Cic in
1359  let module R = CicReduction in
1360   match R.whd context constype with
1361      C.MutInd (_,_,_) ->
1362       if need_dummy then
1363        outtype
1364       else
1365        C.Appl [outtype ; term]
1366    | C.Appl (C.MutInd (_,_,_)::tl) ->
1367       let (_,arguments) = split tl argsno
1368       in
1369        if need_dummy && arguments = [] then
1370         outtype
1371        else
1372         C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
1373    | C.Prod (name,so,de) ->
1374       let term' =
1375        match CicSubstitution.lift 1 term with
1376           C.Appl l -> C.Appl (l@[C.Rel 1])
1377         | t -> C.Appl [t ; C.Rel 1]
1378       in
1379        C.Prod (C.Anonymous,so,type_of_branch
1380         ((Some (name,(C.Decl so)))::context) argsno need_dummy
1381         (CicSubstitution.lift 1 outtype) term' de)
1382   | _ -> raise (AssertFailure "20")
1383
1384 (* check_metasenv_consistency checks that the "canonical" context of a
1385 metavariable is consitent - up to relocation via the relocation list l -
1386 with the actual context *)
1387
1388
1389 and check_metasenv_consistency ~logger ?(subst=[]) metasenv context
1390   canonical_context l ugraph
1391 =
1392   let module C = Cic in
1393   let module R = CicReduction in
1394   let module S = CicSubstitution in
1395   let lifted_canonical_context =
1396     let rec aux i =
1397      function
1398          [] -> []
1399        | (Some (n,C.Decl t))::tl ->
1400            (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
1401        | (Some (n,C.Def (t,None)))::tl ->
1402            (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::(aux (i+1) tl)
1403        | None::tl -> None::(aux (i+1) tl)
1404        | (Some (n,C.Def (t,Some ty)))::tl ->
1405            (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)
1406     in
1407      aux 1 canonical_context
1408    in
1409    List.fold_left2
1410      (fun ugraph t ct ->
1411        match (t,ct) with
1412        | _,None -> ugraph
1413        | Some t,Some (_,C.Def (ct,_)) ->
1414            let b,ugraph1 =
1415              R.are_convertible ~subst ~metasenv context t ct ugraph
1416            in
1417            if not b then
1418              raise
1419                (TypeCheckerFailure
1420                   (sprintf "Not well typed metavariable local context: expected a term convertible with %s, found %s" (CicPp.ppterm ct) (CicPp.ppterm t)))
1421            else
1422              ugraph1
1423        | Some t,Some (_,C.Decl ct) ->
1424            let type_t,ugraph1 =
1425              type_of_aux' ~logger ~subst metasenv context t ugraph
1426            in
1427            let b,ugraph2 =
1428              R.are_convertible ~subst ~metasenv context type_t ct ugraph1
1429            in
1430            if not b then
1431              raise (TypeCheckerFailure
1432                       (sprintf "Not well typed metavariable local context: expected a term of type %s, found %s of type %s"
1433                          (CicPp.ppterm ct) (CicPp.ppterm t)
1434                          (CicPp.ppterm type_t)))
1435            else
1436              ugraph2
1437        | None, _  ->
1438            raise (TypeCheckerFailure
1439                     ("Not well typed metavariable local context: "^
1440                      "an hypothesis, that is not hidden, is not instantiated"))
1441      ) ugraph l lifted_canonical_context
1442
1443
1444 (*
1445    type_of_aux' is just another name (with a different scope)
1446    for type_of_aux
1447 *)
1448
1449 and type_of_aux' ~logger ?(subst = []) metasenv context t ugraph =
1450  let rec type_of_aux ~logger context t ugraph =
1451   let module C = Cic in
1452   let module R = CicReduction in
1453   let module S = CicSubstitution in
1454   let module U = UriManager in
1455    match t with
1456       C.Rel n ->
1457        (try
1458          match List.nth context (n - 1) with
1459             Some (_,C.Decl t) -> S.lift n t,ugraph
1460           | Some (_,C.Def (_,Some ty)) -> S.lift n ty,ugraph
1461           | Some (_,C.Def (bo,None)) ->
1462              debug_print "##### CASO DA INVESTIGARE E CAPIRE" ;
1463               type_of_aux ~logger context (S.lift n bo) ugraph
1464           | None -> raise
1465               (TypeCheckerFailure "Reference to deleted hypothesis")
1466         with
1467         _ ->
1468           raise (TypeCheckerFailure "unbound variable")
1469        )
1470     | C.Var (uri,exp_named_subst) ->
1471       incr fdebug ;
1472         let ugraph1 =
1473           check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
1474         in
1475         let ty,ugraph2 = type_of_variable ~logger uri ugraph1 in
1476         let ty1 = CicSubstitution.subst_vars exp_named_subst ty in
1477           decr fdebug ;
1478           ty1,ugraph2
1479     | C.Meta (n,l) ->
1480        (try
1481           let (canonical_context,term,ty) = CicUtil.lookup_subst n subst in
1482           let ugraph1 =
1483             check_metasenv_consistency ~logger
1484               ~subst metasenv context canonical_context l ugraph
1485           in
1486             (* assuming subst is well typed !!!!! *)
1487             ((CicSubstitution.subst_meta l ty), ugraph1)
1488               (* type_of_aux context (CicSubstitution.subst_meta l term) *)
1489         with CicUtil.Subst_not_found _ ->
1490           let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
1491           let ugraph1 =
1492             check_metasenv_consistency ~logger
1493               ~subst metasenv context canonical_context l ugraph
1494           in
1495             ((CicSubstitution.subst_meta l ty),ugraph1))
1496       (* TASSI: CONSTRAINTS *)
1497     | C.Sort (C.Type t) ->
1498        let t' = CicUniv.fresh() in
1499        let ugraph1 = CicUniv.add_gt t' t ugraph in
1500          (C.Sort (C.Type t')),ugraph1
1501       (* TASSI: CONSTRAINTS *)
1502     | C.Sort s -> (C.Sort (C.Type (CicUniv.fresh ()))),ugraph
1503     | C.Implicit _ -> raise (AssertFailure "21")
1504     | C.Cast (te,ty) as t ->
1505        let _,ugraph1 = type_of_aux ~logger context ty ugraph in
1506        let ty_te,ugraph2 = type_of_aux ~logger context te ugraph1 in
1507        let b,ugraph3 =
1508          R.are_convertible ~subst ~metasenv context ty_te ty ugraph2
1509        in
1510          if b then
1511            ty,ugraph3
1512          else
1513            raise (TypeCheckerFailure
1514                     (sprintf "Invalid cast %s" (CicPp.ppterm t)))
1515     | C.Prod (name,s,t) ->
1516        let sort1,ugraph1 = type_of_aux ~logger context s ugraph in
1517        let sort2,ugraph2 =
1518          type_of_aux ~logger  ((Some (name,(C.Decl s)))::context) t ugraph1
1519        in
1520        sort_of_prod ~subst context (name,s) (sort1,sort2) ugraph2
1521    | C.Lambda (n,s,t) ->
1522        let sort1,ugraph1 = type_of_aux ~logger context s ugraph in
1523        (match R.whd ~subst context sort1 with
1524            C.Meta _
1525          | C.Sort _ -> ()
1526          | _ ->
1527            raise
1528             (TypeCheckerFailure (sprintf
1529               "Not well-typed lambda-abstraction: the source %s should be a type; instead it is a term of type %s" (CicPp.ppterm s)
1530                 (CicPp.ppterm sort1)))
1531        ) ;
1532        let type2,ugraph2 =
1533          type_of_aux ~logger ((Some (n,(C.Decl s)))::context) t ugraph1
1534        in
1535          (C.Prod (n,s,type2)),ugraph2
1536    | C.LetIn (n,s,t) ->
1537       (* only to check if s is well-typed *)
1538       let ty,ugraph1 = type_of_aux ~logger context s ugraph in
1539        (* The type of a LetIn is a LetIn. Extremely slow since the computed
1540           LetIn is later reduced and maybe also re-checked.
1541        (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t))
1542        *)
1543        (* The type of the LetIn is reduced. Much faster than the previous
1544           solution. Moreover the inferred type is probably very different
1545           from the expected one.
1546        (CicReduction.whd context
1547         (C.LetIn (n,s, type_of_aux ((Some (n,(C.Def s)))::context) t)))
1548        *)
1549        (* One-step LetIn reduction. Even faster than the previous solution.
1550           Moreover the inferred type is closer to the expected one. *)
1551        let ty1,ugraph2 =
1552          type_of_aux ~logger
1553            ((Some (n,(C.Def (s,Some ty))))::context) t ugraph1
1554        in
1555        (CicSubstitution.subst s ty1),ugraph2
1556    | C.Appl (he::tl) when List.length tl > 0 ->
1557        let hetype,ugraph1 = type_of_aux ~logger context he ugraph in
1558        let tlbody_and_type,ugraph2 =
1559          List.fold_right (
1560            fun x (l,ugraph) ->
1561              let ty,ugraph1 = type_of_aux ~logger context x ugraph in
1562              let _,ugraph1 = type_of_aux ~logger  context ty ugraph1 in
1563                ((x,ty)::l,ugraph1))
1564            tl ([],ugraph1)
1565        in
1566          (* TASSI: questa c'era nel mio... ma non nel CVS... *)
1567          (* let _,ugraph2 = type_of_aux context hetype ugraph2 in *)
1568          eat_prods ~subst context hetype tlbody_and_type ugraph2
1569    | C.Appl _ -> raise (AssertFailure "Appl: no arguments")
1570    | C.Const (uri,exp_named_subst) ->
1571        incr fdebug ;
1572        let ugraph1 =
1573          check_exp_named_subst ~logger ~subst  context exp_named_subst ugraph
1574        in
1575        let cty,ugraph2 = type_of_constant ~logger uri ugraph1 in
1576        let cty1 =
1577          CicSubstitution.subst_vars exp_named_subst cty
1578        in
1579          decr fdebug ;
1580          cty1,ugraph2
1581    | C.MutInd (uri,i,exp_named_subst) ->
1582       incr fdebug ;
1583        let ugraph1 =
1584          check_exp_named_subst ~logger  ~subst context exp_named_subst ugraph
1585        in
1586          (* TASSI: da me c'era anche questa, ma in CVS no *)
1587        let mty,ugraph2 = type_of_mutual_inductive_defs ~logger uri i ugraph1 in
1588          (* fine parte dubbia *)
1589        let cty =
1590          CicSubstitution.subst_vars exp_named_subst mty
1591        in
1592          decr fdebug ;
1593          cty,ugraph2
1594    | C.MutConstruct (uri,i,j,exp_named_subst) ->
1595        let ugraph1 =
1596          check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
1597        in
1598          (* TASSI: idem come sopra *)
1599        let mty,ugraph2 =
1600          type_of_mutual_inductive_constr ~logger uri i j ugraph1
1601        in
1602        let cty =
1603          CicSubstitution.subst_vars exp_named_subst mty
1604        in
1605          cty,ugraph2
1606    | C.MutCase (uri,i,outtype,term,pl) ->
1607       let outsort,ugraph1 = type_of_aux ~logger context outtype ugraph in
1608       let (need_dummy, k) =
1609       let rec guess_args context t =
1610         let outtype = CicReduction.whd ~subst context t in
1611           match outtype with
1612               C.Sort _ -> (true, 0)
1613             | C.Prod (name, s, t) ->
1614                 let (b, n) =
1615                   guess_args ((Some (name,(C.Decl s)))::context) t in
1616                   if n = 0 then
1617                   (* last prod before sort *)
1618                     match CicReduction.whd ~subst context s with
1619 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1620                         C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
1621                           (false, 1)
1622 (*CSC: for _ see comment below about the missing named_exp_subst ?????????? *)
1623                       | C.Appl ((C.MutInd (uri',i',_)) :: _)
1624                           when U.eq uri' uri && i' = i -> (false, 1)
1625                       | _ -> (true, 1)
1626                   else
1627                     (b, n + 1)
1628             | _ ->
1629                 raise
1630                   (TypeCheckerFailure
1631                      (sprintf
1632                         "Malformed case analasys' output type %s"
1633                         (CicPp.ppterm outtype)))
1634       in
1635 (*
1636       let (parameters, arguments, exp_named_subst),ugraph2 =
1637         let ty,ugraph2 = type_of_aux context term ugraph1 in
1638           match R.whd context ty with
1639            (*CSC manca il caso dei CAST *)
1640 (*CSC: ma servono i parametri (uri,i)? Se si', perche' non serve anche il *)
1641 (*CSC: parametro exp_named_subst? Se no, perche' non li togliamo?         *)
1642 (*CSC: Hint: nella DTD servono per gli stylesheet.                        *)
1643               C.MutInd (uri',i',exp_named_subst) as typ ->
1644                 if U.eq uri uri' && i = i' then
1645                   ([],[],exp_named_subst),ugraph2
1646                 else
1647                   raise
1648                     (TypeCheckerFailure
1649                        (sprintf
1650                           ("Case analysys: analysed term type is %s, but is expected to be (an application of) %s#1/%d{_}")
1651                           (CicPp.ppterm typ) (U.string_of_uri uri) i))
1652             | C.Appl
1653                 ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
1654                 if U.eq uri uri' && i = i' then
1655                   let params,args =
1656                     split tl (List.length tl - k)
1657                   in (params,args,exp_named_subst),ugraph2
1658                 else
1659                   raise
1660                     (TypeCheckerFailure
1661                        (sprintf
1662                           ("Case analysys: analysed term type is %s, "^
1663                            "but is expected to be (an application of) "^
1664                            "%s#1/%d{_}")
1665                           (CicPp.ppterm typ') (U.string_of_uri uri) i))
1666             | _ ->
1667                 raise
1668                   (TypeCheckerFailure
1669                      (sprintf
1670                         ("Case analysis: "^
1671                          "analysed term %s is not an inductive one")
1672                         (CicPp.ppterm term)))
1673 *)
1674       let (b, k) = guess_args context outsort in
1675           if not b then (b, k - 1) else (b, k) in
1676       let (parameters, arguments, exp_named_subst),ugraph2 =
1677         let ty,ugraph2 = type_of_aux ~logger context term ugraph1 in
1678         match R.whd ~subst context ty with
1679             C.MutInd (uri',i',exp_named_subst) as typ ->
1680               if U.eq uri uri' && i = i' then
1681                 ([],[],exp_named_subst),ugraph2
1682               else raise
1683                 (TypeCheckerFailure
1684                    (sprintf
1685                       ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}")
1686                       (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i))
1687           | C.Appl
1688               ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
1689               if U.eq uri uri' && i = i' then
1690                 let params,args =
1691                   split tl (List.length tl - k)
1692                 in (params,args,exp_named_subst),ugraph2
1693               else raise
1694                 (TypeCheckerFailure
1695                    (sprintf
1696                       ("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}")
1697                       (CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i))
1698           | _ ->
1699               raise
1700                 (TypeCheckerFailure
1701                    (sprintf
1702                       "Case analysis: analysed term %s is not an inductive one"
1703                       (CicPp.ppterm term)))
1704       in
1705         (*
1706            let's control if the sort elimination is allowed:
1707            [(I q1 ... qr)|B]
1708         *)
1709       let sort_of_ind_type =
1710         if parameters = [] then
1711           C.MutInd (uri,i,exp_named_subst)
1712         else
1713           C.Appl ((C.MutInd (uri,i,exp_named_subst))::parameters)
1714       in
1715       let type_of_sort_of_ind_ty,ugraph3 =
1716         type_of_aux ~logger context sort_of_ind_type ugraph2 in
1717       let b,ugraph4 =
1718         check_allowed_sort_elimination ~logger  context uri i need_dummy
1719           sort_of_ind_type type_of_sort_of_ind_ty outsort ugraph3
1720       in
1721         if not b then
1722         raise
1723           (TypeCheckerFailure ("Case analasys: sort elimination not allowed"));
1724         (* let's check if the type of branches are right *)
1725       let parsno =
1726         let obj,_ =
1727           try
1728             CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
1729           with Not_found -> assert false
1730         in
1731         match obj with
1732             C.InductiveDefinition (_,_,parsno,_) -> parsno
1733           | _ ->
1734               raise (TypeCheckerFailure
1735                 ("Unknown mutual inductive definition:" ^
1736                   UriManager.string_of_uri uri))
1737         in
1738       let (_,branches_ok,ugraph5) =
1739         List.fold_left
1740           (fun (j,b,ugraph) p ->
1741             if b then
1742               let cons =
1743                 if parameters = [] then
1744                   (C.MutConstruct (uri,i,j,exp_named_subst))
1745                 else
1746                   (C.Appl
1747                      (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
1748               in
1749               let ty_p,ugraph1 = type_of_aux ~logger context p ugraph in
1750               let ty_cons,ugraph3 = type_of_aux ~logger context cons ugraph1 in
1751               (* 2 is skipped *)
1752               let ty_branch =
1753                 type_of_branch context parsno need_dummy outtype cons
1754                   ty_cons in
1755               let b1,ugraph4 =
1756                 R.are_convertible
1757                   ~subst ~metasenv context ty_p ty_branch ugraph3
1758               in
1759               if not b1 then
1760                 debug_print
1761                   ("#### " ^ CicPp.ppterm ty_p ^
1762                   " <==> " ^ CicPp.ppterm ty_branch);
1763               (j + 1,b1,ugraph4)
1764             else
1765               (j,false,ugraph)
1766           ) (1,true,ugraph4) pl
1767          in
1768           if not branches_ok then
1769            raise
1770             (TypeCheckerFailure "Case analysys: wrong branch type");
1771           let arguments =
1772            if not need_dummy then outtype::arguments@[term]
1773            else outtype::arguments in
1774           let outtype =
1775            if arguments = [] then outtype
1776            else CicReduction.head_beta_reduce (C.Appl arguments)
1777           in
1778            outtype,ugraph5
1779    | C.Fix (i,fl) ->
1780       let types_times_kl,ugraph1 =
1781         (* WAS: list rev list map *)
1782         List.fold_left
1783           (fun (l,ugraph) (n,k,ty,_) ->
1784             let _,ugraph1 = type_of_aux ~logger context ty ugraph in
1785             ((Some (C.Name n,(C.Decl ty)),k)::l,ugraph1)
1786           ) ([],ugraph) fl
1787       in
1788       let (types,kl) = List.split types_times_kl in
1789       let len = List.length types in
1790       let ugraph2 =
1791         List.fold_left
1792           (fun ugraph (name,x,ty,bo) ->
1793              let ty_bo,ugraph1 =
1794                type_of_aux ~logger (types@context) bo ugraph
1795              in
1796              let b,ugraph2 =
1797                R.are_convertible ~subst ~metasenv (types@context)
1798                  ty_bo (CicSubstitution.lift len ty) ugraph1 in
1799                if b then
1800                  begin
1801                    let (m, eaten, context') =
1802                      eat_lambdas ~subst (types @ context) (x + 1) bo
1803                    in
1804                      (*
1805                        let's control the guarded by
1806                        destructors conditions D{f,k,x,M}
1807                      *)
1808                      if not (guarded_by_destructors context' eaten
1809                                (len + eaten) kl 1 [] m) then
1810                        raise
1811                          (TypeCheckerFailure
1812                             ("Fix: not guarded by destructors"))
1813                      else
1814                        ugraph2
1815                  end
1816                else
1817                  raise (TypeCheckerFailure ("Fix: ill-typed bodies"))
1818           ) ugraph1 fl in
1819         (*CSC: controlli mancanti solo su D{f,k,x,M} *)
1820       let (_,_,ty,_) = List.nth fl i in
1821         ty,ugraph2
1822    | C.CoFix (i,fl) ->
1823        let types,ugraph1 =
1824          List.fold_left
1825            (fun (l,ugraph) (n,ty,_) ->
1826               let _,ugraph1 =
1827                 type_of_aux ~logger context ty ugraph in
1828                 (Some (C.Name n,(C.Decl ty))::l,ugraph1)
1829            ) ([],ugraph) fl
1830        in
1831        let len = List.length types in
1832        let ugraph2 =
1833          List.fold_left
1834            (fun ugraph (_,ty,bo) ->
1835               let ty_bo,ugraph1 =
1836                 type_of_aux ~logger (types @ context) bo ugraph
1837               in
1838               let b,ugraph2 =
1839                 R.are_convertible ~subst ~metasenv (types @ context) ty_bo
1840                   (CicSubstitution.lift len ty) ugraph1
1841               in
1842                 if b then
1843                   begin
1844                     (* let's control that the returned type is coinductive *)
1845                     match returns_a_coinductive context ty with
1846                         None ->
1847                           raise
1848                           (TypeCheckerFailure
1849                              ("CoFix: does not return a coinductive type"))
1850                       | Some uri ->
1851                           (*
1852                             let's control the guarded by constructors
1853                             conditions C{f,M}
1854                           *)
1855                           if not (guarded_by_constructors (types @ context)
1856                                     0 len false bo [] uri) then
1857                             raise
1858                               (TypeCheckerFailure
1859                                  ("CoFix: not guarded by constructors"))
1860                           else
1861                           ugraph2
1862                   end
1863                 else
1864                   raise
1865                     (TypeCheckerFailure ("CoFix: ill-typed bodies"))
1866            ) ugraph1 fl
1867        in
1868        let (_,ty,_) = List.nth fl i in
1869          ty,ugraph2
1870
1871  and check_exp_named_subst ~logger ?(subst = []) context ugraph =
1872    let rec check_exp_named_subst_aux ~logger esubsts l ugraph =
1873      match l with
1874          [] -> ugraph
1875        | ((uri,t) as item)::tl ->
1876            let ty_uri,ugraph1 = type_of_variable ~logger uri ugraph in
1877            let typeofvar =
1878              CicSubstitution.subst_vars esubsts ty_uri in
1879            let typeoft,ugraph2 = type_of_aux ~logger context t ugraph1 in
1880            let b,ugraph3 =
1881              CicReduction.are_convertible ~subst ~metasenv
1882                context typeoft typeofvar ugraph2
1883            in
1884              if b then
1885                check_exp_named_subst_aux ~logger (esubsts@[item]) tl ugraph3
1886              else
1887                begin
1888                  CicReduction.fdebug := 0 ;
1889                  ignore
1890                    (CicReduction.are_convertible
1891                       ~subst ~metasenv context typeoft typeofvar ugraph2) ;
1892                  fdebug := 0 ;
1893                  debug typeoft [typeofvar] ;
1894                  raise (TypeCheckerFailure "Wrong Explicit Named Substitution")
1895                end
1896    in
1897      check_exp_named_subst_aux ~logger [] ugraph
1898
1899  and sort_of_prod ?(subst = []) context (name,s) (t1, t2) ugraph =
1900   let module C = Cic in
1901    let t1' = CicReduction.whd ~subst context t1 in
1902    let t2' = CicReduction.whd ~subst ((Some (name,C.Decl s))::context) t2 in
1903    match (t1', t2') with
1904       (C.Sort s1, C.Sort s2)
1905         when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
1906          (* different from Coq manual!!! *)
1907          C.Sort s2,ugraph
1908     | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
1909       (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
1910        let t' = CicUniv.fresh() in
1911        let ugraph1 = CicUniv.add_ge t' t1 ugraph in
1912        let ugraph2 = CicUniv.add_ge t' t2 ugraph1 in
1913        C.Sort (C.Type t'),ugraph2
1914     | (C.Sort _,C.Sort (C.Type t1)) ->
1915         (* TASSI: CONSRTAINTS: the same in doubletypeinference, cicrefine *)
1916         C.Sort (C.Type t1),ugraph (* c'e' bisogno di un fresh? *)
1917     | (C.Meta _, C.Sort _) -> t2',ugraph
1918     | (C.Meta _, (C.Meta (_,_) as t))
1919     | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
1920         t2',ugraph
1921     | (_,_) -> raise (TypeCheckerFailure (sprintf
1922         "Prod: expected two sorts, found = %s, %s" (CicPp.ppterm t1')
1923           (CicPp.ppterm t2')))
1924
1925  and eat_prods ?(subst = []) context hetype l ugraph =
1926    (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
1927    (*CSC: cucinati                                                         *)
1928    match l with
1929        [] -> hetype,ugraph
1930      | (hete, hety)::tl ->
1931          (match (CicReduction.whd ~subst context hetype) with
1932               Cic.Prod (n,s,t) ->
1933                 let b,ugraph1 =
1934                   CicReduction.are_convertible
1935                     ~subst ~metasenv context hety s ugraph
1936                 in
1937                   if b then
1938                     begin
1939                       CicReduction.fdebug := -1 ;
1940                       eat_prods ~subst context
1941                         (CicSubstitution.subst hete t) tl ugraph1
1942                         (*TASSI: not sure *)
1943                     end
1944                   else
1945                     begin
1946                       CicReduction.fdebug := 0 ;
1947                       ignore (CicReduction.are_convertible
1948                                 ~subst ~metasenv context s hety ugraph) ;
1949                       fdebug := 0 ;
1950                       debug s [hety] ;
1951                       raise
1952                         (TypeCheckerFailure
1953                            (sprintf
1954                               ("Appl: wrong parameter-type, expected %s, found %s")
1955                               (CicPp.ppterm hetype) (CicPp.ppterm s)))
1956                     end
1957             | _ ->
1958                 raise (TypeCheckerFailure
1959                          "Appl: this is not a function, it cannot be applied")
1960          )
1961
1962  and returns_a_coinductive context ty =
1963   let module C = Cic in
1964    match CicReduction.whd context ty with
1965       C.MutInd (uri,i,_) ->
1966        (*CSC: definire una funzioncina per questo codice sempre replicato *)
1967         let obj,_ =
1968           try
1969             CicEnvironment.get_cooked_obj ~trust:false CicUniv.empty_ugraph uri
1970           with Not_found -> assert false
1971         in
1972         (match obj with
1973            C.InductiveDefinition (itl,_,_,_) ->
1974             let (_,is_inductive,_,_) = List.nth itl i in
1975              if is_inductive then None else (Some uri)
1976          | _ ->
1977             raise (TypeCheckerFailure
1978               ("Unknown mutual inductive definition:" ^
1979               UriManager.string_of_uri uri))
1980         )
1981     | C.Appl ((C.MutInd (uri,i,_))::_) ->
1982        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
1983          match o with
1984            C.InductiveDefinition (itl,_,_,_) ->
1985             let (_,is_inductive,_,_) = List.nth itl i in
1986              if is_inductive then None else (Some uri)
1987          | _ ->
1988             raise (TypeCheckerFailure
1989               ("Unknown mutual inductive definition:" ^
1990               UriManager.string_of_uri uri))
1991         )
1992     | C.Prod (n,so,de) ->
1993        returns_a_coinductive ((Some (n,C.Decl so))::context) de
1994     | _ -> None
1995
1996  in
1997 (*CSC
1998 debug_print ("INIZIO TYPE_OF_AUX " ^ CicPp.ppterm t) ; flush stderr ;
1999 let res =
2000 *)
2001   type_of_aux ~logger context t ugraph
2002 (*
2003 in debug_print "FINE TYPE_OF_AUX" ; flush stderr ; res
2004 *)
2005
2006 (* is a small constructor? *)
2007 (*CSC: ottimizzare calcolando staticamente *)
2008 and is_small ~logger context paramsno c ugraph =
2009  let rec is_small_aux ~logger context c ugraph =
2010   let module C = Cic in
2011    match CicReduction.whd context c with
2012       C.Prod (n,so,de) ->
2013        (*CSC: [] is an empty metasenv. Is it correct? *)
2014        let s,ugraph1 = type_of_aux' ~logger [] context so ugraph in
2015        let b = (s = C.Sort C.Prop || s = C.Sort C.Set || s = C.Sort C.CProp) in
2016        if b then
2017          is_small_aux ~logger ((Some (n,(C.Decl so)))::context) de ugraph1
2018        else
2019          false,ugraph1
2020     | _ -> true,ugraph (*CSC: we trust the type-checker *)
2021  in
2022   let (context',dx) = split_prods context paramsno c in
2023    is_small_aux ~logger context' dx ugraph
2024
2025 and type_of ~logger t ugraph =
2026 (*CSC
2027 debug_print ("INIZIO TYPE_OF_AUX' " ^ CicPp.ppterm t) ; flush stderr ;
2028 let res =
2029 *)
2030  type_of_aux' ~logger [] [] t ugraph
2031 (*CSC
2032 in debug_print "FINE TYPE_OF_AUX'" ; flush stderr ; res
2033 *)
2034 ;;
2035
2036 let typecheck_obj0 ~logger uri ugraph =
2037  let module C = Cic in
2038   function
2039      C.Constant (_,Some te,ty,_,_) ->
2040       let _,ugraph = type_of ~logger ty ugraph in
2041       let ty_te,ugraph = type_of ~logger te ugraph in
2042       let b,ugraph = (CicReduction.are_convertible [] ty_te ty ugraph) in
2043        if not b then
2044          raise (TypeCheckerFailure
2045           ("the type of the body is not the one expected"))
2046        else
2047         ugraph
2048    | C.Constant (_,None,ty,_,_) ->
2049       (* only to check that ty is well-typed *)
2050       let _,ugraph = type_of ~logger ty ugraph in
2051        ugraph
2052    | C.CurrentProof (_,conjs,te,ty,_,_) ->
2053       let _,ugraph =
2054        List.fold_left
2055         (fun (metasenv,ugraph) ((_,context,ty) as conj) ->
2056           let _,ugraph =
2057            type_of_aux' ~logger metasenv context ty ugraph
2058           in
2059            metasenv @ [conj],ugraph
2060         ) ([],ugraph) conjs
2061       in
2062        let _,ugraph = type_of_aux' ~logger conjs [] ty ugraph in
2063        let type_of_te,ugraph =
2064         type_of_aux' ~logger conjs [] te ugraph
2065        in
2066        let b,ugraph = CicReduction.are_convertible [] type_of_te ty ugraph in
2067         if not b then
2068           raise (TypeCheckerFailure (sprintf
2069            "the current proof is not well typed because the type %s of the body is not convertible to the declared type %s"
2070            (CicPp.ppterm type_of_te) (CicPp.ppterm ty)))
2071         else
2072          ugraph
2073    | C.Variable (_,bo,ty,_,_) ->
2074       (* only to check that ty is well-typed *)
2075       let _,ugraph = type_of ~logger ty ugraph in
2076        (match bo with
2077            None -> ugraph
2078          | Some bo ->
2079             let ty_bo,ugraph = type_of ~logger bo ugraph in
2080             let b,ugraph = CicReduction.are_convertible [] ty_bo ty ugraph in
2081              if not b then
2082               raise (TypeCheckerFailure
2083                ("the body is not the one expected"))
2084              else
2085               ugraph
2086             )
2087    | (C.InductiveDefinition _ as obj) ->
2088       check_mutual_inductive_defs ~logger uri obj ugraph
2089
2090 let typecheck uri =
2091  let module C = Cic in
2092  let module R = CicReduction in
2093  let module U = UriManager in
2094  let logger = new CicLogger.logger in
2095    (* ??? match CicEnvironment.is_type_checked ~trust:true uri with ???? *)
2096    match CicEnvironment.is_type_checked ~trust:false CicUniv.empty_ugraph uri with
2097      CicEnvironment.CheckedObj (cobj,ugraph') ->
2098        (* debug_print ("NON-INIZIO A TYPECHECKARE " ^ U.string_of_uri uri);*)
2099        cobj,ugraph'
2100    | CicEnvironment.UncheckedObj uobj ->
2101       (* let's typecheck the uncooked object *)
2102       logger#log (`Start_type_checking uri) ;
2103       (* debug_print ("INIZIO A TYPECHECKARE " ^ U.string_of_uri uri); *)
2104       let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph uobj in
2105         try
2106           CicEnvironment.set_type_checking_info uri;
2107           logger#log (`Type_checking_completed uri);
2108           match CicEnvironment.is_type_checked ~trust:false ugraph uri with
2109               CicEnvironment.CheckedObj (cobj,ugraph') -> cobj,ugraph'
2110             | _ -> raise CicEnvironmentError
2111         with
2112             (*
2113               this is raised if set_type_checking_info is called on an object
2114               that has no associated universe file. If we are in univ_maker
2115               phase this is OK since univ_maker will properly commit the
2116               object.
2117             *)
2118             Invalid_argument s ->
2119               (*debug_print s;*)
2120               uobj,ugraph
2121 ;;
2122
2123 let typecheck_obj ~logger uri obj =
2124  let ugraph = typecheck_obj0 ~logger uri CicUniv.empty_ugraph obj in
2125  let ugraph = CicUnivUtils.clean_and_fill uri obj ugraph in
2126   CicEnvironment.add_type_checked_obj uri (obj,ugraph)
2127
2128 (** wrappers which instantiate fresh loggers *)
2129
2130 let type_of_aux' ?(subst = []) metasenv context t ugraph =
2131   let logger = new CicLogger.logger in
2132   type_of_aux' ~logger ~subst metasenv context t ugraph
2133
2134 let typecheck_obj uri obj =
2135  let logger = new CicLogger.logger in
2136  typecheck_obj ~logger uri obj