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