+let rec fomega_conv_kind k1 k2 =
+ match k1,k2 with
+ Type,Type -> true
+ | KArrow (s1,t1), KArrow (s2,t2) ->
+ fomega_conv_kind s1 s2 && fomega_conv_kind t1 t2
+ | KSkip k1, KSkip k2 -> fomega_conv_kind k1 k2
+ | _,_ -> false
+
+let rec fomega_conv status t1 t2 =
+ match fomega_whd status t1, fomega_whd status t2 with
+ Var n, Var m -> n=m
+ | Unit, Unit -> true
+ | Top, Top -> true
+ | TConst r1, TConst r2 -> NReference.eq r1 r2
+ | Arrow (s1,t1), Arrow (s2,t2) ->
+ fomega_conv status s1 s2 && fomega_conv status t1 t2
+ | TSkip t1, TSkip t2 -> fomega_conv status t1 t2
+ | Forall (_,k1,t1), Forall (_,k2,t2) ->
+ fomega_conv_kind k1 k2 && fomega_conv status t1 t2
+ | TAppl tl1, TAppl tl2 ->
+ (try
+ List.fold_left2 (fun b t1 t2 -> b && fomega_conv status t1 t2)
+ true tl1 tl2
+ with
+ Invalid_argument _ -> false)
+ | _,_ -> false
+
+exception PatchMe (* BUG: constructor of singleton type :-( *)
+
+let type_of_constructor status ref =
+ try
+ match snd (ReferenceMap.find ref (fst status#extraction_db)) with
+ `Constructor ty -> ty
+ | _ -> assert false
+ with
+ Not_found -> raise PatchMe (* BUG: constructor of singleton type :-( *)
+
+let type_of_appl_he status ~metasenv context =
+ function
+ NCic.Const (NReference.Ref (_,NReference.Con _) as ref)
+ | NCic.Const (NReference.Ref (_,NReference.Def _) as ref)
+ | NCic.Const (NReference.Ref (_,NReference.Decl) as ref)
+ | NCic.Const (NReference.Ref (_,NReference.Fix _) as ref)
+ | NCic.Const (NReference.Ref (_,NReference.CoFix _) as ref) ->
+ (try
+ match snd (ReferenceMap.find ref (fst status#extraction_db)) with
+ `Type _ -> assert false
+ | `Constructor ty
+ | `Function ty -> ty
+ with
+ Not_found -> assert false)
+ | NCic.Const (NReference.Ref (_,NReference.Ind _)) ->
+ assert false (* IMPOSSIBLE *)
+ | NCic.Rel n ->
+ (match List.nth context (n-1) with
+ _,NCic.Decl typ
+ | _,NCic.Def (_,typ) ->
+ (* recomputed every time *)
+ typ_of status ~metasenv context
+ (NCicSubstitution.lift status n typ))
+ | (NCic.Lambda _
+ | NCic.LetIn _
+ | NCic.Match _) as t ->
+ (* BUG: here we should implement a real type-checker since we are
+ trusting the translation of the Cic one that could be wrong
+ (e.g. pruned abstractions, etc.) *)
+ (typ_of status ~metasenv context
+ (NCicTypeChecker.typeof status ~metasenv ~subst:[] context t))
+ | NCic.Meta _ -> assert false (* TODO *)
+ | NCic.Sort _ | NCic.Implicit _ | NCic.Appl _ | NCic.Prod _ ->
+ assert false (* IMPOSSIBLE *)
+