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