aux metasenv subst [] he ty_he args
(*D*)in outside(); rc with exc -> outside (); raise exc
;;
+
+let rec first f l1 l2 =
+ match l1,l2 with
+ | x1::tl1, x2::tl2 ->
+ (try f x1 x2 with Not_found -> first f tl1 tl2)
+ | _ -> raise Not_found
+;;
+
+let rec find add dt t =
+ if dt == add then t
+ else
+ let dl, l =
+ match dt, t with
+ | C.Meta (_,(_,C.Ctx dl)), C.Meta (_,(_,C.Ctx l))
+ | C.Appl dl,C.Appl l -> dl,l
+ | C.Lambda (_,ds,dt), C.Lambda (_,s,t)
+ | C.Prod (_,ds,dt), C.Prod (_,s,t) -> [ds;dt],[s;t]
+ | C.LetIn (_,ds,db,dt), C.LetIn (_,s,b,t) -> [ds;db;dt],[s;b;t]
+ | C.Match (_,dot,dt,dl), C.Match (_,ot,t,l) -> (dot::dt::dl),(ot::t::l)
+ | _ -> raise Not_found
+ in
+ first (find add) dl l
+;;
+
+let relocalise old_localise dt t add =
+ old_localise
+ (try find add dt t with Not_found -> assert false)
+;;
+
+let undebruijnate inductive ref t rev_fl =
+ NCicSubstitution.psubst (fun x -> x)
+ (HExtlib.list_mapi
+ (fun (_,_,rno,_,_,_) i ->
+ NCic.Const
+ (if inductive then NReference.mk_fix i rno ref
+ else NReference.mk_cofix i ref))
+ rev_fl)
+ t
+;;
+
+
+let typeof_obj hdb
+ ?(localise=fun _ -> Stdpp.dummy_loc)
+ ~look_for_coercion (uri,height,metasenv,subst, obj)
+=
+ let check_type metasenv subst (ty as orig_ty) = (* XXX fattorizza *)
+ let metasenv, subst, ty, sort =
+ typeof hdb ~localise ~look_for_coercion metasenv subst [] ty None
+ in
+ let metasenv, subst, ty, _ =
+ force_to_sort hdb ~look_for_coercion
+ metasenv subst [] ty orig_ty localise sort
+ in
+ metasenv, subst, ty
+ in
+ match obj with
+ | C.Constant (relevance, name, bo, ty , attr) ->
+ let metasenv, subst, ty = check_type metasenv subst ty in
+ let metasenv, subst, bo, ty, height =
+ match bo with
+ | Some bo ->
+ let metasenv, subst, bo, ty =
+ typeof hdb ~localise ~look_for_coercion
+ metasenv subst [] bo (Some ty)
+ in
+ let height = (* XXX recalculate *) height in
+ metasenv, subst, Some bo, ty, height
+ | None -> metasenv, subst, None, ty, 0
+ in
+ uri, height, metasenv, subst,
+ C.Constant (relevance, name, bo, ty, attr)
+ | C.Fixpoint (inductive, fl, attr) ->
+ let len = List.length fl in
+ let types, metasenv, subst, rev_fl =
+ List.fold_left
+ (fun (types, metasenv, subst, fl) (relevance,name,k,ty,bo) ->
+ let metasenv, subst, ty = check_type metasenv subst ty in
+ let dbo = NCicTypeChecker.debruijn uri len [] bo in
+ let localise = relocalise localise dbo bo in
+ (name,C.Decl ty)::types,
+ metasenv, subst, (relevance,name,k,ty,dbo,localise)::fl
+ ) ([], metasenv, subst, []) fl (* XXX kl rimosso nel nucleo *)
+ in
+ let metasenv, subst, fl =
+ List.fold_left
+ (fun (metasenv,subst,fl) (relevance,name,k,ty,dbo,localise) ->
+ let metasenv, subst, dbo, ty =
+ typeof hdb ~localise ~look_for_coercion
+ metasenv subst types dbo (Some ty)
+ in
+ metasenv, subst, (relevance,name,k,ty,dbo)::fl)
+ (metasenv, subst, []) rev_fl
+ in
+ let height = (* XXX recalculate *) height in
+ let fl =
+ List.map
+ (fun (relevance,name,k,ty,dbo) ->
+ let bo =
+ undebruijnate inductive
+ (NReference.reference_of_spec uri
+ (if inductive then NReference.Fix (0,k,0)
+ else NReference.CoFix 0)) dbo rev_fl
+ in
+ relevance,name,k,ty,bo)
+ fl
+ in
+ uri, height, metasenv, subst,
+ C.Fixpoint (inductive, fl, attr)
+
+ | C.Inductive (ind, leftno, itl, attr) -> assert false
+(*
+ (* let's check if the arity of the inductive types are well formed *)
+ List.iter (fun (_,_,x,_) -> ignore (typeof ~subst ~metasenv [] x)) tyl;
+ (* let's check if the types of the inductive constructors are well formed. *)
+ let len = List.length tyl in
+ let tys = List.rev_map (fun (_,n,ty,_) -> (n,(C.Decl ty))) tyl in
+ ignore
+ (List.fold_right
+ (fun (it_relev,_,ty,cl) i ->
+ let context,ty_sort = split_prods ~subst [] ~-1 ty in
+ let sx_context_ty_rev,_ = HExtlib.split_nth leftno (List.rev context) in
+ List.iter
+ (fun (k_relev,_,te) ->
+ let _,k_relev = HExtlib.split_nth leftno k_relev in
+ let te = debruijn uri len [] te in
+ let context,te = split_prods ~subst tys leftno te in
+ let _,chopped_context_rev =
+ HExtlib.split_nth (List.length tys) (List.rev context) in
+ let sx_context_te_rev,_ =
+ HExtlib.split_nth leftno chopped_context_rev in
+ (try
+ ignore (List.fold_left2
+ (fun context item1 item2 ->
+ let convertible =
+ match item1,item2 with
+ (n1,C.Decl ty1),(n2,C.Decl ty2) ->
+ n1 = n2 &&
+ R.are_convertible ~metasenv ~subst context ty1 ty2
+ | (n1,C.Def (bo1,ty1)),(n2,C.Def (bo2,ty2)) ->
+ n1 = n2
+ && R.are_convertible ~metasenv ~subst context ty1 ty2
+ && R.are_convertible ~metasenv ~subst context bo1 bo2
+ | _,_ -> false
+ in
+ if not convertible then
+ raise (TypeCheckerFailure (lazy
+ ("Mismatch between the left parameters of the constructor " ^
+ "and those of its inductive type")))
+ else
+ item1::context
+ ) [] sx_context_ty_rev sx_context_te_rev)
+ with Invalid_argument "List.fold_left2" -> assert false);
+ let con_sort = typeof ~subst ~metasenv context te in
+ (match R.whd ~subst context con_sort, R.whd ~subst [] ty_sort with
+ (C.Sort (C.Type u1) as s1), (C.Sort (C.Type u2) as s2) ->
+ if not (E.universe_leq u1 u2) then
+ raise
+ (TypeCheckerFailure
+ (lazy ("The type " ^ PP.ppterm ~metasenv ~subst ~context s1^
+ " of the constructor is not included in the inductive" ^
+ " type sort " ^ PP.ppterm ~metasenv ~subst ~context s2)))
+ | C.Sort _, C.Sort C.Prop
+ | C.Sort _, C.Sort C.Type _ -> ()
+ | _, _ ->
+ raise
+ (TypeCheckerFailure
+ (lazy ("Wrong constructor or inductive arity shape"))));
+ (* let's check also the positivity conditions *)
+ if
+ not
+ (are_all_occurrences_positive ~subst context uri leftno
+ (i+leftno) leftno (len+leftno) te)
+ then
+ raise
+ (TypeCheckerFailure
+ (lazy ("Non positive occurence in "^NUri.string_of_uri
+ uri)))
+ else check_relevance ~subst ~metasenv context k_relev te)
+ cl;
+ check_relevance ~subst ~metasenv [] it_relev ty;
+ i+1)
+ tyl 1)
+*)
+
+
+;;
+
+
+
(* vim:set foldmethod=marker: *)
projects / helm.git / blobdiff