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