helm/software/components/cic_acic/doubleTypeInference.ml

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