helm/ocaml/cic_proof_checking/cicTypeChecker.ml

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