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