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