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