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