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