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