+let typecheck_context ~metasenv ~subst context =
+ ignore
+ (List.fold_right
+ (fun d context ->
+ begin
+ match d with
+ _,C.Decl t -> ignore (typeof ~metasenv ~subst:[] context t)
+ | name,C.Def (te,ty) ->
+ ignore (typeof ~metasenv ~subst:[] context ty);
+ let ty' = typeof ~metasenv ~subst:[] context te in
+ if not (R.are_convertible ~subst get_relevance context ty' ty) then
+ raise (AssertFailure (lazy (Printf.sprintf (
+ "the type of the definiens for %s in the context is not "^^
+ "convertible with the declared one.\n"^^
+ "inferred type:\n%s\nexpected type:\n%s")
+ name (PP.ppterm ~subst ~metasenv ~context ty')
+ (PP.ppterm ~subst ~metasenv ~context ty))))
+ end;
+ d::context
+ ) context [])
+;;
+
+let typecheck_metasenv metasenv =
+ ignore
+ (List.fold_left
+ (fun metasenv (i,(_,context,ty) as conj) ->
+ if List.mem_assoc i metasenv then
+ raise (TypeCheckerFailure (lazy ("duplicate meta " ^ string_of_int i ^
+ " in metasenv")));
+ typecheck_context ~metasenv ~subst:[] context;
+ ignore (typeof ~metasenv ~subst:[] context ty);
+ metasenv @ [conj]
+ ) [] metasenv)
+;;
+
+let typecheck_subst ~metasenv subst =
+ ignore
+ (List.fold_left
+ (fun subst (i,(_,context,ty,bo) as conj) ->
+ if List.mem_assoc i subst then
+ raise (AssertFailure (lazy ("duplicate meta " ^ string_of_int i ^
+ " in substitution")));
+ if List.mem_assoc i metasenv then
+ raise (AssertFailure (lazy ("meta " ^ string_of_int i ^
+ " is both in the metasenv and in the substitution")));
+ typecheck_context ~metasenv ~subst context;
+ ignore (typeof ~metasenv ~subst context ty);
+ let ty' = typeof ~metasenv ~subst context bo in
+ if not (R.are_convertible ~subst get_relevance context ty' ty) then
+ raise (AssertFailure (lazy (Printf.sprintf (
+ "the type of the definiens for %d in the substitution is not "^^
+ "convertible with the declared one.\n"^^
+ "inferred type:\n%s\nexpected type:\n%s")
+ i
+ (PP.ppterm ~subst ~metasenv ~context ty')
+ (PP.ppterm ~subst ~metasenv ~context ty))));
+ subst @ [conj]
+ ) [] subst)
+;;
+
+
+let typecheck_obj (uri,_height,metasenv,subst,kind) =
+ (* height is not checked since it is only used to implement an optimization *)
+ typecheck_metasenv metasenv;
+ typecheck_subst ~metasenv subst;