let t1 = R.whd ~subst context t1 in
let t2 = R.whd ~subst ((name,C.Decl s)::context) t2 in
match t1, t2 with
- | C.Sort s1, C.Sort s2
- (* different from Coq manual, Impredicative Set! *)
- when (s2 = C.Prop || s2 = C.Set || s2 = C.CProp) -> C.Sort s2
- | C.Sort (C.Type t1), C.Sort (C.Type t2) -> C.Sort (C.Type (max t1 t2))
- | C.Sort _,C.Sort (C.Type t1) -> C.Sort (C.Type t1)
- | C.Meta _, C.Sort _ -> t2
- | C.Meta _, ((C.Meta _) as t)
- | C.Sort _, ((C.Meta _) as t) when U.is_closed t -> t2
+ | C.Sort s1, C.Sort C.Prop -> t2
+ | C.Sort (C.Type u1), C.Sort (C.Type u2) -> C.Sort (C.Type (max u1 u2))
+ | C.Sort _,C.Sort (C.Type _) -> t2
+ | C.Sort (C.Type _) , C.Sort C.CProp -> t1
+ | C.Sort _, C.Sort C.CProp -> t2
+ | C.Meta _, C.Sort _
+ | C.Meta _, C.Meta _
+ | C.Sort _, C.Meta _ when U.is_closed t2 -> t2
| _ ->
raise (TypeCheckerFailure (lazy (Printf.sprintf
"Prod: expected two sorts, found = %s, %s"
;;
-let typeof ~subst ~metasenv context term =
+let rec typeof ~subst ~metasenv context term =
let rec typeof_aux context = function
| C.Rel n ->
(try
| C.Sort (C.Type i) -> C.Sort (C.Type (i+1))
| C.Sort s -> C.Sort (C.Type 0)
| C.Implicit _ -> raise (AssertFailure (lazy "Implicit found"))
+ | C.Meta (n,l) as t ->
+ let canonical_context,ty =
+ try
+ let _,c,_,ty = NCicUtils.lookup_subst n subst in c,ty
+ with NCicUtils.Subst_not_found _ -> try
+ let _,_,c,ty = NCicUtils.lookup_meta n metasenv in c,ty
+ with NCicUtils.Meta_not_found _ ->
+ raise (AssertFailure (lazy (Printf.sprintf
+ "%s not found" (NCicPp.ppterm t))))
+ in
+ check_metasenv_consistency t context canonical_context l;
+ S.subst_meta l ty
+ | C.Const ref -> type_of_constant ref
| C.Prod (name,s,t) ->
let sort1 = typeof_aux context s in
let sort2 = typeof_aux ((name,(C.Decl s))::context) t in
sort_of_prod ~subst context (name,s) (sort1,sort2)
| C.Lambda (n,s,t) ->
- let sort1 = typeof_aux context s in
- (match R.whd ~subst context sort1 with
+ let sort = typeof_aux context s in
+ (match R.whd ~subst context sort with
| C.Meta _ | C.Sort _ -> ()
| _ ->
raise
(TypeCheckerFailure (lazy (Printf.sprintf
("Not well-typed lambda-abstraction: " ^^
"the source %s should be a type; instead it is a term " ^^
- "of type %s") (NCicPp.ppterm s) (NCicPp.ppterm sort1)))));
- let type2 =
- typeof_aux ((n,(C.Decl s))::context) t
- in
- C.Prod (n,s,type2)
+ "of type %s") (NCicPp.ppterm s) (NCicPp.ppterm sort)))));
+ let ty = typeof_aux ((n,(C.Decl s))::context) t in
+ C.Prod (n,s,ty)
| C.LetIn (n,ty,t,bo) ->
let ty_t = typeof_aux context t in
if not (R.are_convertible ~subst ~metasenv context ty ty_t) then
"The type of %s is %s but it is expected to be %s"
(NCicPp.ppterm t) (NCicPp.ppterm ty_t) (NCicPp.ppterm ty))))
else
- (* Alternatives:
- 1) The type of a LetIn is a LetIn, extremely slow since the computed
- LetIn may be later reduced.
- 2) The type of the LetIn is reduced, much faster than the previous
- solution, moreover the inferred type is probably very different
- from the expected one.
- 3) One-step LetIn reduction, even faster than the previous solution,
- moreover the inferred type is closer to the expected one. *)
let ty_bo = typeof_aux ((n,C.Def (t,ty))::context) bo in
S.subst ~avoid_beta_redexes:true t ty_bo
| C.Appl (he::(_::_ as args)) ->
let args_with_ty = List.map (fun t -> t, typeof_aux context t) args in
eat_prods ~subst ~metasenv context ty_he args_with_ty
| C.Appl _ -> raise (AssertFailure (lazy "Appl of length < 2"))
- | C.Meta (n,l) ->
- (try
- let _,canonical_context,term,ty = NCicUtils.lookup_subst n subst in
- check_metasenv_consistency context canonical_context l;
- (* assuming subst is well typed !!!!! *)
- S.subst_meta l ty
- with NCicUtils.Subst_not_found _ ->
- let _,_,canonical_context,ty = NCicUtils.lookup_meta n metasenv in
- check_metasenv_consistency context canonical_context l;
- S.subst_meta l ty)
| C.Match (r,outtype,term,pl) ->
- let outsort = typeof_aux context outtype in
assert false (* FINQUI
+ let outsort = typeof_aux context outtype in
let (need_dummy, k) =
let rec guess_args context t =
let outtype = R.whd ~subst context t in
in
outtype,ugraph5
*)
- 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))))
in
typeof_aux context term
+
+and type_of_constant ref = assert false
(*
- | C.Const (uri,exp_named_subst) ->
- incr fdebug ;
- let ugraph1 =
- check_exp_named_subst ~logger ~subst context exp_named_subst ugraph
- in
- let cty,ugraph2 = type_of_constant ~logger uri ugraph1 in
- let cty1 =
- CicSubstitution.subst_vars exp_named_subst cty
- in
- decr fdebug ;
- cty1,ugraph2
| C.Fix (i,fl) ->
let types,kl,ugraph1,len =
List.fold_left
projects / helm.git / commitdiff