components/cic_acic/doubleTypeInference.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 (* $Id$ *)
  27
  28 exception Impossible of int;;
  29 exception NotWellTyped of string;;
  30 exception WrongUriToConstant of string;;
  31 exception WrongUriToVariable of string;;
  32 exception WrongUriToMutualInductiveDefinitions of string;;
  33 exception ListTooShort;;
  34 exception RelToHiddenHypothesis;;
  35
  36 (*CSC: must alfa-conversion be considered or not? *)
  37
  38 let xxx_type_of_aux' m c t =
  39  try
  40    Some (fst (CicTypeChecker.type_of_aux' m c t CicUniv.empty_ugraph))
  41  with
  42  | CicTypeChecker.TypeCheckerFailure _ -> None (* because eta_expansion *)
  43 ;;
  44
  45 type types = {synthesized : Cic.term ; expected : Cic.term option};;
  46
  47 (* does_not_occur n te                              *)
  48 (* returns [true] if [Rel n] does not occur in [te] *)
  49 let rec does_not_occur n =
  50  let module C = Cic in
  51   function
  52      C.Rel m when m = n -> false
  53    | C.Rel _
  54    | C.Meta _
  55    | C.Sort _
  56    | C.Implicit _ -> true
  57    | C.Cast (te,ty) ->
  58       does_not_occur n te && does_not_occur n ty
  59    | C.Prod (name,so,dest) ->
  60       does_not_occur n so &&
  61        does_not_occur (n + 1) dest
  62    | C.Lambda (name,so,dest) ->
  63       does_not_occur n so &&
  64        does_not_occur (n + 1) dest
  65    | C.LetIn (name,so,dest) ->
  66       does_not_occur n so &&
  67        does_not_occur (n + 1) dest
  68    | C.Appl l ->
  69       List.fold_right (fun x i -> i && does_not_occur n x) l true
  70    | C.Var (_,exp_named_subst)
  71    | C.Const (_,exp_named_subst)
  72    | C.MutInd (_,_,exp_named_subst)
  73    | C.MutConstruct (_,_,_,exp_named_subst) ->
  74       List.fold_right (fun (_,x) i -> i && does_not_occur n x)
  75        exp_named_subst true
  76    | C.MutCase (_,_,out,te,pl) ->
  77       does_not_occur n out && does_not_occur n te &&
  78        List.fold_right (fun x i -> i && does_not_occur n x) pl true
  79    | C.Fix (_,fl) ->
  80       let len = List.length fl in
  81        let n_plus_len = n + len in
  82         List.fold_right
  83          (fun (_,_,ty,bo) i ->
  84            i && does_not_occur n ty &&
  85            does_not_occur n_plus_len bo
  86          ) fl true
  87    | C.CoFix (_,fl) ->
  88       let len = List.length fl in
  89        let n_plus_len = n + len in
  90         List.fold_right
  91          (fun (_,ty,bo) i ->
  92            i && does_not_occur n ty &&
  93            does_not_occur n_plus_len bo
  94          ) fl true
  95 ;;
  96
  97 let rec beta_reduce =
  98  let module S = CicSubstitution in
  99  let module C = Cic in
 100   function
 101       C.Rel _ as t -> t
 102     | C.Var (uri,exp_named_subst) ->
 103        let exp_named_subst' =
 104         List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
 105        in
 106         C.Var (uri,exp_named_subst')
 107     | C.Meta (n,l) ->
 108        C.Meta (n,
 109         List.map
 110          (function None -> None | Some t -> Some (beta_reduce t)) l
 111        )
 112     | C.Sort _ as t -> t
 113     | C.Implicit _ -> assert false
 114     | C.Cast (te,ty) ->
 115        C.Cast (beta_reduce te, beta_reduce ty)
 116     | C.Prod (n,s,t) ->
 117        C.Prod (n, beta_reduce s, beta_reduce t)
 118     | C.Lambda (n,s,t) ->
 119        C.Lambda (n, beta_reduce s, beta_reduce t)
 120     | C.LetIn (n,s,t) ->
 121        C.LetIn (n, beta_reduce s, beta_reduce t)
 122     | C.Appl ((C.Lambda (name,s,t))::he::tl) ->
 123        let he' = S.subst he t in
 124         if tl = [] then
 125          beta_reduce he'
 126         else
 127          (match he' with
 128              C.Appl l -> beta_reduce (C.Appl (l@tl))
 129            | _ -> beta_reduce (C.Appl (he'::tl)))
 130     | C.Appl l ->
 131        C.Appl (List.map beta_reduce l)
 132     | C.Const (uri,exp_named_subst) ->
 133        let exp_named_subst' =
 134         List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
 135        in
 136         C.Const (uri,exp_named_subst')
 137     | C.MutInd (uri,i,exp_named_subst) ->
 138        let exp_named_subst' =
 139         List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
 140        in
 141         C.MutInd (uri,i,exp_named_subst')
 142     | C.MutConstruct (uri,i,j,exp_named_subst) ->
 143        let exp_named_subst' =
 144         List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
 145        in
 146         C.MutConstruct (uri,i,j,exp_named_subst')
 147     | C.MutCase (sp,i,outt,t,pl) ->
 148        C.MutCase (sp,i,beta_reduce outt,beta_reduce t,
 149         List.map beta_reduce pl)
 150     | C.Fix (i,fl) ->
 151        let fl' =
 152         List.map
 153          (function (name,i,ty,bo) ->
 154            name,i,beta_reduce ty,beta_reduce bo
 155          ) fl
 156        in
 157         C.Fix (i,fl')
 158     | C.CoFix (i,fl) ->
 159        let fl' =
 160         List.map
 161          (function (name,ty,bo) ->
 162            name,beta_reduce ty,beta_reduce bo
 163          ) fl
 164        in
 165         C.CoFix (i,fl')
 166 ;;
 167
 168 let rec split l n =
 169  match (l,n) with
 170     (l,0) -> ([], l)
 171   | (he::tl, n) -> let (l1,l2) = split tl (n-1) in (he::l1,l2)
 172   | (_,_) -> raise ListTooShort
 173 ;;
 174
 175 let type_of_constant uri =
 176  let module C = Cic in
 177  let module R = CicReduction in
 178  let module U = UriManager in
 179   let cobj =
 180    match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
 181       CicEnvironment.CheckedObj (cobj,_) -> cobj
 182     | CicEnvironment.UncheckedObj uobj ->
 183        raise (NotWellTyped "Reference to an unchecked constant")
 184   in
 185    match cobj with
 186       C.Constant (_,_,ty,_,_) -> ty
 187     | C.CurrentProof (_,_,_,ty,_,_) -> ty
 188     | _ -> raise (WrongUriToConstant (U.string_of_uri uri))
 189 ;;
 190
 191 let type_of_variable uri =
 192  let module C = Cic in
 193  let module R = CicReduction in
 194  let module U = UriManager in
 195   match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
 196      CicEnvironment.CheckedObj ((C.Variable (_,_,ty,_,_)),_) -> ty
 197    | CicEnvironment.UncheckedObj (C.Variable _) ->
 198       raise (NotWellTyped "Reference to an unchecked variable")
 199    |  _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
 200 ;;
 201
 202 let type_of_mutual_inductive_defs uri i =
 203  let module C = Cic in
 204  let module R = CicReduction in
 205  let module U = UriManager in
 206   let cobj =
 207    match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
 208       CicEnvironment.CheckedObj (cobj,_) -> cobj
 209     | CicEnvironment.UncheckedObj uobj ->
 210        raise (NotWellTyped "Reference to an unchecked inductive type")
 211   in
 212    match cobj with
 213       C.InductiveDefinition (dl,_,_,_) ->
 214        let (_,_,arity,_) = List.nth dl i in
 215         arity
 216     | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
 217 ;;
 218
 219 let type_of_mutual_inductive_constr uri i j =
 220  let module C = Cic in
 221  let module R = CicReduction in
 222  let module U = UriManager in
 223   let cobj =
 224    match CicEnvironment.is_type_checked CicUniv.empty_ugraph uri with
 225       CicEnvironment.CheckedObj (cobj,_) -> cobj
 226     | CicEnvironment.UncheckedObj uobj ->
 227        raise (NotWellTyped "Reference to an unchecked constructor")
 228   in
 229    match cobj with
 230       C.InductiveDefinition (dl,_,_,_) ->
 231        let (_,_,_,cl) = List.nth dl i in
 232         let (_,ty) = List.nth cl (j-1) in
 233          ty
 234     | _ -> raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
 235 ;;
 236
 237 let pack_coercion = ref (fun _ _ _ -> assert false);;
 238
 239 let profiler_for_find = HExtlib.profile "CicHash ADD" ;;
 240
 241 let cic_CicHash_add a b c =
 242   profiler_for_find.HExtlib.profile (Cic.CicHash.add a b) c
 243 ;;
 244
 245 let profiler_for_find1 = HExtlib.profile "CicHash MEM" ;;
 246
 247 let cic_CicHash_mem a b =
 248   profiler_for_find1.HExtlib.profile (Cic.CicHash.mem a) b
 249 ;;
 250
 251 (* type_of_aux' is just another name (with a different scope) for type_of_aux *)
 252 let rec type_of_aux' subterms_to_types metasenv context t expectedty =
 253  (* Coscoy's double type-inference algorithm             *)
 254  (* It computes the inner-types of every subterm of [t], *)
 255  (* even when they are not needed to compute the types   *)
 256  (* of other terms.                                      *)
 257  let rec type_of_aux context t expectedty =
 258   let module C = Cic in
 259   let module R = CicReduction in
 260   let module S = CicSubstitution in
 261   let module U = UriManager in
 262    let expectedty =
 263     match expectedty with
 264        None -> None
 265      | Some t -> Some (!pack_coercion metasenv context t) in
 266    let synthesized =
 267     match t with
 268        C.Rel n ->
 269         (try
 270           match List.nth context (n - 1) with
 271              Some (_,C.Decl t) -> S.lift n t
 272            | Some (_,C.Def (_,Some ty)) -> S.lift n ty
 273            | Some (_,C.Def (bo,None)) ->
 274               type_of_aux context (S.lift n bo) expectedty
 275                  | None -> raise RelToHiddenHypothesis
 276          with
 277           _ -> raise (NotWellTyped "Not a close term")
 278         )
 279      | C.Var (uri,exp_named_subst) ->
 280         visit_exp_named_subst context uri exp_named_subst ;
 281         CicSubstitution.subst_vars exp_named_subst (type_of_variable uri)
 282      | C.Meta (n,l) ->
 283         (* Let's visit all the subterms that will not be visited later *)
 284         let (_,canonical_context,_) = CicUtil.lookup_meta n metasenv in
 285          let lifted_canonical_context =
 286           let rec aux i =
 287            function
 288               [] -> []
 289             | (Some (n,C.Decl t))::tl ->
 290                (Some (n,C.Decl (S.subst_meta l (S.lift i t))))::(aux (i+1) tl)
 291             | (Some (n,C.Def (t,None)))::tl ->
 292                (Some (n,C.Def ((S.subst_meta l (S.lift i t)),None)))::
 293                 (aux (i+1) tl)
 294             | None::tl -> None::(aux (i+1) tl)
 295             | (Some (_,C.Def (_,Some _)))::_ -> assert false
 296           in
 297            aux 1 canonical_context
 298          in
 299           let _ =
 300            List.iter2
 301             (fun t ct ->
 302               match t,ct with
 303                  _,None -> ()
 304                | Some t,Some (_,C.Def (ct,_)) ->
 305                   let expected_type =
 306                     match xxx_type_of_aux' metasenv context ct with
 307                     | None -> None
 308                     | Some t -> Some (R.whd context t)
 309                   in
 310                    (* Maybe I am a bit too paranoid, because   *)
 311                    (* if the term is well-typed than t and ct  *)
 312                    (* are convertible. Nevertheless, I compute *)
 313                    (* the expected type.                       *)
 314                    ignore (type_of_aux context t expected_type)
 315                | Some t,Some (_,C.Decl ct) ->
 316                   ignore (type_of_aux context t (Some ct))
 317                | _,_ -> assert false (* the term is not well typed!!! *)
 318             ) l lifted_canonical_context
 319           in
 320            let (_,canonical_context,ty) = CicUtil.lookup_meta n metasenv in
 321             (* Checks suppressed *)
 322             CicSubstitution.subst_meta l ty
 323      | C.Sort (C.Type t) -> (* TASSI: CONSTRAINT *)
 324          C.Sort (C.Type (CicUniv.fresh()))
 325      | C.Sort _ -> C.Sort (C.Type (CicUniv.fresh())) (* TASSI: CONSTRAINT *)
 326      | C.Implicit _ -> raise (Impossible 21)
 327      | C.Cast (te,ty) ->
 328         (* Let's visit all the subterms that will not be visited later *)
 329         let _ = type_of_aux context te (Some (beta_reduce ty)) in
 330         let _ = type_of_aux context ty None in
 331          (* Checks suppressed *)
 332          ty
 333      | C.Prod (name,s,t) ->
 334         let sort1 = type_of_aux context s None
 335         and sort2 = type_of_aux ((Some (name,(C.Decl s)))::context) t None in
 336          sort_of_prod context (name,s) (sort1,sort2)
 337      | C.Lambda (n,s,t) ->
 338         (* Let's visit all the subterms that will not be visited later *)
 339          let _ = type_of_aux context s None in
 340          let expected_target_type =
 341           match expectedty with
 342              None -> None
 343            | Some expectedty' ->
 344               let ty =
 345                match R.whd context expectedty' with
 346                   C.Prod (_,_,expected_target_type) ->
 347                    beta_reduce expected_target_type
 348                 | _ -> assert false
 349               in
 350                Some ty
 351          in
 352           let type2 =
 353            type_of_aux ((Some (n,(C.Decl s)))::context) t expected_target_type
 354           in
 355            (* Checks suppressed *)
 356            C.Prod (n,s,type2)
 357      | C.LetIn (n,s,t) ->
 358 (*CSC: What are the right expected types for the source and *)
 359 (*CSC: target of a LetIn? None used.                        *)
 360         (* Let's visit all the subterms that will not be visited later *)
 361         let ty = type_of_aux context s None in
 362          let t_typ =
 363           (* Checks suppressed *)
 364           type_of_aux ((Some (n,(C.Def (s,Some ty))))::context) t None
 365          in  (* CicSubstitution.subst s t_typ *)
 366           if does_not_occur 1 t_typ then
 367            (* since [Rel 1] does not occur in typ, substituting any term *)
 368            (* in place of [Rel 1] is equivalent to delifting once        *)
 369            CicSubstitution.subst (C.Implicit None) t_typ
 370           else
 371            C.LetIn (n,s,t_typ)
 372      | C.Appl (he::tl) when List.length tl > 0 ->
 373         (*
 374         let expected_hetype =
 375          (* Inefficient, the head is computed twice. But I know *)
 376          (* of no other solution. *)
 377          (beta_reduce
 378           (R.whd context (xxx_type_of_aux' metasenv context he)))
 379         in
 380          let hetype = type_of_aux context he (Some expected_hetype) in
 381          let tlbody_and_type =
 382           let rec aux =
 383            function
 384               _,[] -> []
 385             | C.Prod (n,s,t),he::tl ->
 386                (he, type_of_aux context he (Some (beta_reduce s)))::
 387                 (aux (R.whd context (S.subst he t), tl))
 388             | _ -> assert false
 389           in
 390            aux (expected_hetype, tl) *)
 391          let hetype = R.whd context (type_of_aux context he None) in
 392          let tlbody_and_type =
 393           let rec aux =
 394            function
 395               _,[] -> []
 396             | C.Prod (n,s,t),he::tl ->
 397                (he, type_of_aux context he (Some (beta_reduce s)))::
 398                 (aux (R.whd context (S.subst he t), tl))
 399             | _ -> assert false
 400           in
 401            aux (hetype, tl)
 402          in
 403           eat_prods context hetype tlbody_and_type
 404      | C.Appl _ -> raise (NotWellTyped "Appl: no arguments")
 405      | C.Const (uri,exp_named_subst) ->
 406         visit_exp_named_subst context uri exp_named_subst ;
 407         CicSubstitution.subst_vars exp_named_subst (type_of_constant uri)
 408      | C.MutInd (uri,i,exp_named_subst) ->
 409         visit_exp_named_subst context uri exp_named_subst ;
 410         CicSubstitution.subst_vars exp_named_subst
 411          (type_of_mutual_inductive_defs uri i)
 412      | C.MutConstruct (uri,i,j,exp_named_subst) ->
 413         visit_exp_named_subst context uri exp_named_subst ;
 414         CicSubstitution.subst_vars exp_named_subst
 415          (type_of_mutual_inductive_constr uri i j)
 416      | C.MutCase (uri,i,outtype,term,pl) ->
 417         let outsort = type_of_aux context outtype None in
 418         let (need_dummy, k) =
 419          let rec guess_args context t =
 420           match CicReduction.whd context t with
 421              C.Sort _ -> (true, 0)
 422            | C.Prod (name, s, t) ->
 423               let (b, n) = guess_args ((Some (name,(C.Decl s)))::context) t in
 424                if n = 0 then
 425                 (* last prod before sort *)
 426                 match CicReduction.whd context s with
 427                    C.MutInd (uri',i',_) when U.eq uri' uri && i' = i ->
 428                     (false, 1)
 429                  | C.Appl ((C.MutInd (uri',i',_)) :: _)
 430                     when U.eq uri' uri && i' = i -> (false, 1)
 431                  | _ -> (true, 1)
 432                else
 433                 (b, n + 1)
 434            | _ -> raise (NotWellTyped "MutCase: outtype ill-formed")
 435          in
 436           let (b, k) = guess_args context outsort in
 437            if not b then (b, k - 1) else (b, k)
 438         in
 439         let (parameters, arguments,exp_named_subst) =
 440          let type_of_term =
 441            match xxx_type_of_aux' metasenv context term with
 442            | None -> None
 443            | Some t -> Some (beta_reduce t)
 444          in
 445           match
 446            R.whd context (type_of_aux context term type_of_term)
 447           with
 448              (*CSC manca il caso dei CAST *)
 449              C.MutInd (uri',i',exp_named_subst) ->
 450               (* Checks suppressed *)
 451               [],[],exp_named_subst
 452            | C.Appl (C.MutInd (uri',i',exp_named_subst) :: tl) ->
 453              let params,args =
 454               split tl (List.length tl - k)
 455              in params,args,exp_named_subst
 456            | _ ->
 457              raise (NotWellTyped "MutCase: the term is not an inductive one")
 458         in
 459          (* Checks suppressed *)
 460          (* Let's visit all the subterms that will not be visited later *)
 461          let (cl,parsno) =
 462            let obj,_ =
 463              try
 464                CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
 465              with Not_found -> assert false
 466            in
 467           match obj with
 468              C.InductiveDefinition (tl,_,parsno,_) ->
 469               let (_,_,_,cl) = List.nth tl i in (cl,parsno)
 470            | _ ->
 471              raise (WrongUriToMutualInductiveDefinitions (U.string_of_uri uri))
 472          in
 473           let _ =
 474            List.fold_left
 475             (fun j (p,(_,c)) ->
 476               let cons =
 477                if parameters = [] then
 478                 (C.MutConstruct (uri,i,j,exp_named_subst))
 479                else
 480                 (C.Appl (C.MutConstruct (uri,i,j,exp_named_subst)::parameters))
 481               in
 482                let expectedtype =
 483                  match xxx_type_of_aux' metasenv context cons with
 484                  | None -> None
 485                  | Some t ->
 486                      Some
 487                        (beta_reduce
 488                          (type_of_branch context parsno need_dummy outtype
 489                            cons t))
 490                in
 491                 ignore (type_of_aux context p expectedtype);
 492                 j+1
 493             ) 1 (List.combine pl cl)
 494           in
 495            if not need_dummy then
 496             C.Appl ((outtype::arguments)@[term])
 497            else if arguments = [] then
 498             outtype
 499            else
 500             C.Appl (outtype::arguments)
 501      | C.Fix (i,fl) ->
 502         (* Let's visit all the subterms that will not be visited later *)
 503         let context' =
 504          List.rev
 505           (List.map
 506             (fun (n,_,ty,_) ->
 507               let _ = type_of_aux context ty None in
 508                (Some (C.Name n,(C.Decl ty)))
 509             ) fl
 510           ) @
 511           context
 512         in
 513          let _ =
 514           List.iter
 515            (fun (_,_,ty,bo) ->
 516              let expectedty =
 517               beta_reduce (CicSubstitution.lift (List.length fl) ty)
 518              in
 519               ignore (type_of_aux context' bo (Some expectedty))
 520            ) fl
 521          in
 522           (* Checks suppressed *)
 523           let (_,_,ty,_) = List.nth fl i in
 524            ty
 525      | C.CoFix (i,fl) ->
 526         (* Let's visit all the subterms that will not be visited later *)
 527         let context' =
 528          List.rev
 529           (List.map
 530             (fun (n,ty,_) ->
 531               let _ = type_of_aux context ty None in
 532                (Some (C.Name n,(C.Decl ty)))
 533             ) fl
 534           ) @
 535           context
 536         in
 537          let _ =
 538           List.iter
 539            (fun (_,ty,bo) ->
 540              let expectedty =
 541               beta_reduce (CicSubstitution.lift (List.length fl) ty)
 542              in
 543               ignore (type_of_aux context' bo (Some expectedty))
 544            ) fl
 545          in
 546           (* Checks suppressed *)
 547           let (_,ty,_) = List.nth fl i in
 548            ty
 549    in
 550     let synthesized' = beta_reduce synthesized in
 551     let synthesized' = !pack_coercion metasenv context synthesized' in
 552      let types,res =
 553       match expectedty with
 554          None ->
 555           (* No expected type *)
 556           {synthesized = synthesized' ; expected = None}, synthesized
 557        | Some ty when CicUtil.alpha_equivalence synthesized' ty ->
 558           (* The expected type is synthactically equal to *)
 559           (* the synthesized type. Let's forget it.       *)
 560           {synthesized = synthesized' ; expected = None}, synthesized
 561        | Some expectedty' ->
 562           {synthesized = synthesized' ; expected = Some expectedty'},
 563           expectedty'
 564      in
 565 (*      assert (not (cic_CicHash_mem subterms_to_types t));*)
 566       cic_CicHash_add subterms_to_types t types ;
 567       res
 568
 569  and visit_exp_named_subst context uri exp_named_subst =
 570   let uris_and_types =
 571      let obj,_ =
 572        try
 573          CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
 574        with Not_found -> assert false
 575      in
 576     let params = CicUtil.params_of_obj obj in
 577      List.map
 578       (function uri ->
 579          let obj,_ =
 580            try
 581              CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
 582            with Not_found -> assert false
 583          in
 584          match obj with
 585            Cic.Variable (_,None,ty,_,_) -> uri,ty
 586          | _ -> assert false (* the theorem is well-typed *)
 587       ) params
 588   in
 589    let rec check uris_and_types subst =
 590     match uris_and_types,subst with
 591        _,[] -> []
 592      | (uri,ty)::tytl,(uri',t)::substtl when uri = uri' ->
 593         ignore (type_of_aux context t (Some ty)) ;
 594         let tytl' =
 595          List.map
 596           (function uri,t' -> uri,(CicSubstitution.subst_vars [uri',t] t')) tytl
 597         in
 598          check tytl' substtl
 599      | _,_ -> assert false (* the theorem is well-typed *)
 600    in
 601     check uris_and_types exp_named_subst
 602
 603  and sort_of_prod context (name,s) (t1, t2) =
 604   let module C = Cic in
 605    let t1' = CicReduction.whd context t1 in
 606    let t2' = CicReduction.whd ((Some (name,C.Decl s))::context) t2 in
 607    match (t1', t2') with
 608       (C.Sort _, C.Sort s2)
 609         when (s2 = C.Prop or s2 = C.Set or s2 = C.CProp) ->
 610          (* different from Coq manual!!! *)
 611          C.Sort s2
 612     | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
 613         C.Sort (C.Type (CicUniv.fresh()))
 614     | (C.Sort _,C.Sort (C.Type t1)) ->
 615         (* TASSI: CONSRTAINTS: the same in cictypechecker,cicrefine *)
 616         C.Sort (C.Type t1) (* c'e' bisogno di un fresh? *)
 617     | (C.Meta _, C.Sort _) -> t2'
 618     | (C.Meta _, (C.Meta (_,_) as t))
 619     | (C.Sort _, (C.Meta (_,_) as t)) when CicUtil.is_closed t ->
 620         t2'
 621     | (_,_) ->
 622       raise
 623        (NotWellTyped
 624         ("Prod: sort1= " ^ CicPp.ppterm t1' ^ " ; sort2= " ^ CicPp.ppterm t2'))
 625
 626  and eat_prods context hetype =
 627   (*CSC: siamo sicuri che le are_convertible non lavorino con termini non *)
 628   (*CSC: cucinati                                                         *)
 629   function
 630      [] -> hetype
 631    | (hete, hety)::tl ->
 632     (match (CicReduction.whd context hetype) with
 633         Cic.Prod (n,s,t) ->
 634          (* Checks suppressed *)
 635          eat_prods context (CicSubstitution.subst hete t) tl
 636       | _ -> raise (NotWellTyped "Appl: wrong Prod-type")
 637     )
 638
 639 and type_of_branch context argsno need_dummy outtype term constype =
 640  let module C = Cic in
 641  let module R = CicReduction in
 642   match R.whd context constype with
 643      C.MutInd (_,_,_) ->
 644       if need_dummy then
 645        outtype
 646       else
 647        C.Appl [outtype ; term]
 648    | C.Appl (C.MutInd (_,_,_)::tl) ->
 649       let (_,arguments) = split tl argsno
 650       in
 651        if need_dummy && arguments = [] then
 652         outtype
 653        else
 654         C.Appl (outtype::arguments@(if need_dummy then [] else [term]))
 655    | C.Prod (name,so,de) ->
 656       let term' =
 657        match CicSubstitution.lift 1 term with
 658           C.Appl l -> C.Appl (l@[C.Rel 1])
 659         | t -> C.Appl [t ; C.Rel 1]
 660       in
 661        C.Prod (C.Anonymous,so,type_of_branch
 662         ((Some (name,(C.Decl so)))::context) argsno need_dummy
 663         (CicSubstitution.lift 1 outtype) term' de)
 664   | _ -> raise (Impossible 20)
 665
 666  in
 667   type_of_aux context t expectedty
 668 ;;
 669
 670 let double_type_of metasenv context t expectedty =
 671  let subterms_to_types = Cic.CicHash.create 503 in
 672   ignore (type_of_aux' subterms_to_types metasenv context t expectedty) ;
 673   subterms_to_types
 674 ;;