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