- and check_metasenv_consistency context canonical_context l =
- let lifted_canonical_context =
- let rec lift_metas i = function
- | [] -> []
- | (n,C.Decl t)::tl ->
- (n,C.Decl (S.subst_meta l (S.lift i t)))::(lift_metas (i+1) tl)
- | (n,C.Def (t,ty))::tl ->
- (n,C.Def ((S.subst_meta l (S.lift i t)),
- S.subst_meta l (S.lift i ty)))::(lift_metas (i+1) tl)
- in
- lift_metas 1 canonical_context
- in
- (* we could optimize when l is an NCic.Irl *)
- let l =
- let shift, lc_kind = l in
- List.map (S.lift shift) (NCicUtils.expand_local_context lc_kind)
- in
- List.iter2
- (fun t ct ->
- match (t,ct) with
- | t, (_,C.Def (ct,_)) ->
- (*CSC: the following optimization is to avoid a possibly expensive
- reduction that can be easily avoided and that is quite
- frequent. However, this is better handled using levels to
- control reduction *)
- let optimized_t =
- match t with
- | C.Rel n ->
- (try
- match List.nth context (n - 1) with
- | (_,C.Def (te,_)) -> S.lift n te
- | _ -> t
- with Failure _ -> t)
- | _ -> t
- in
- if not (R.are_convertible ~subst ~metasenv context optimized_t ct)then
- raise
- (TypeCheckerFailure
- (lazy (Printf.sprintf
- ("Not well typed metavariable local context: " ^^
- "expected a term convertible with %s, found %s")
- (NCicPp.ppterm ct) (NCicPp.ppterm t))))
- | t, (_,C.Decl ct) ->
- let type_t = typeof_aux context t in
- if not (R.are_convertible ~subst ~metasenv context type_t ct) then
- raise (TypeCheckerFailure
- (lazy (Printf.sprintf
- ("Not well typed metavariable local context: "^^
- "expected a term of type %s, found %s of type %s")
- (NCicPp.ppterm ct) (NCicPp.ppterm t) (NCicPp.ppterm type_t))))
- ) l lifted_canonical_context
+ and check_metasenv_consistency term context canonical_context l =
+ match l with
+ | shift, NCic.Irl n ->
+ let context = snd (HExtlib.split_nth shift context) in
+ let rec compare = function
+ | 0,_,[] -> ()
+ | 0,_,_::_
+ | _,_,[] ->
+ raise (AssertFailure (lazy (Printf.sprintf
+ "Local and canonical context %s have different lengths"
+ (NCicPp.ppterm term))))
+ | m,[],_::_ ->
+ raise (TypeCheckerFailure (lazy (Printf.sprintf
+ "Unbound variable -%d in %s" m (NCicPp.ppterm term))))
+ | m,t::tl,ct::ctl ->
+ (match t,ct with
+ (_,C.Decl t1), (_,C.Decl t2)
+ | (_,C.Def (t1,_)), (_,C.Def (t2,_))
+ | (_,C.Def (_,t1)), (_,C.Decl t2) ->
+ if not (R.are_convertible ~subst ~metasenv tl t1 t2) then
+ raise
+ (TypeCheckerFailure
+ (lazy (Printf.sprintf
+ ("Not well typed metavariable local context for %s: " ^^
+ "%s expected, which is not convertible with %s")
+ (NCicPp.ppterm term) (NCicPp.ppterm t2) (NCicPp.ppterm t1)
+ )))
+ | _,_ ->
+ raise
+ (TypeCheckerFailure
+ (lazy (Printf.sprintf
+ ("Not well typed metavariable local context for %s: " ^^
+ "a definition expected, but a declaration found")
+ (NCicPp.ppterm term)))));
+ compare (m - 1,tl,ctl)
+ in
+ compare (n,context,canonical_context)
+ | shift, lc_kind ->
+ (* we avoid useless lifting by shortening the context*)
+ let l,context = (0,lc_kind), snd (HExtlib.split_nth shift context) in
+ let lifted_canonical_context =
+ let rec lift_metas i = function
+ | [] -> []
+ | (n,C.Decl t)::tl ->
+ (n,C.Decl (S.subst_meta l (S.lift i t)))::(lift_metas (i+1) tl)
+ | (n,C.Def (t,ty))::tl ->
+ (n,C.Def ((S.subst_meta l (S.lift i t)),
+ S.subst_meta l (S.lift i ty)))::(lift_metas (i+1) tl)
+ in
+ lift_metas 1 canonical_context in
+ let l = NCicUtils.expand_local_context lc_kind in
+ try
+ List.iter2
+ (fun t ct ->
+ match (t,ct) with
+ | t, (_,C.Def (ct,_)) ->
+ (*CSC: the following optimization is to avoid a possibly expensive
+ reduction that can be easily avoided and that is quite
+ frequent. However, this is better handled using levels to
+ control reduction *)
+ let optimized_t =
+ match t with
+ | C.Rel n ->
+ (try
+ match List.nth context (n - 1) with
+ | (_,C.Def (te,_)) -> S.lift n te
+ | _ -> t
+ with Failure _ -> t)
+ | _ -> t
+ in
+ if not (R.are_convertible ~subst ~metasenv context optimized_t ct)
+ then
+ raise
+ (TypeCheckerFailure
+ (lazy (Printf.sprintf
+ ("Not well typed metavariable local context: " ^^
+ "expected a term convertible with %s, found %s")
+ (NCicPp.ppterm ct) (NCicPp.ppterm t))))
+ | t, (_,C.Decl ct) ->
+ let type_t = typeof_aux context t in
+ if not (R.are_convertible ~subst ~metasenv context type_t ct) then
+ raise (TypeCheckerFailure
+ (lazy (Printf.sprintf
+ ("Not well typed metavariable local context: "^^
+ "expected a term of type %s, found %s of type %s")
+ (NCicPp.ppterm ct) (NCicPp.ppterm t) (NCicPp.ppterm type_t))))
+ ) l lifted_canonical_context
+ with
+ Invalid_argument _ ->
+ raise (AssertFailure (lazy (Printf.sprintf
+ "Local and canonical context %s have different lengths"
+ (NCicPp.ppterm term))))