diff options
Diffstat (limited to 'kernel/sign.ml')
| -rw-r--r-- | kernel/sign.ml | 31 |
1 files changed, 16 insertions, 15 deletions
diff --git a/kernel/sign.ml b/kernel/sign.ml index a4b2a2ea..7caf667f 100644 --- a/kernel/sign.ml +++ b/kernel/sign.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: sign.ml,v 1.37.2.1 2004/07/16 19:30:26 herbelin Exp $ *) +(* $Id: sign.ml 7639 2005-12-02 10:01:15Z gregoire $ *) open Names open Util @@ -53,13 +53,11 @@ let empty_rel_context = [] let add_rel_decl d ctxt = d::ctxt -let lookup_rel n sign = - let rec lookrec = function - | (1, decl :: _) -> decl - | (n, _ :: sign) -> lookrec (n-1,sign) - | (_, []) -> raise Not_found - in - lookrec (n,sign) +let rec lookup_rel n sign = + match n, sign with + | 1, decl :: _ -> decl + | n, _ :: sign -> lookup_rel (n-1) sign + | _, [] -> raise Not_found let rel_context_length = List.length @@ -73,7 +71,7 @@ let rel_context_nhyps hyps = let fold_rel_context f l ~init:x = List.fold_right f l x let fold_rel_context_reverse f ~init:x l = List.fold_left f x l -let map_rel_context f l = +let map_context f l = let map_decl (n, body_o, typ as decl) = let body_o' = option_smartmap f body_o in let typ' = f typ in @@ -82,6 +80,9 @@ let map_rel_context f l = in list_smartmap map_decl l +let map_rel_context = map_context +let map_named_context = map_context + (* Push named declarations on top of a rel context *) (* Bizarre. Should be avoided. *) let push_named_to_rel_context hyps ctxt = @@ -121,7 +122,7 @@ let destArity = match kind_of_term c with | Prod (x,t,c) -> prodec_rec ((x,None,t)::l) c | LetIn (x,b,t,c) -> prodec_rec ((x,Some b,t)::l) c - | Cast (c,_) -> prodec_rec l c + | Cast (c,_,_) -> prodec_rec l c | Sort s -> l,s | _ -> anomaly "destArity: not an arity" in @@ -133,7 +134,7 @@ let rec isArity c = match kind_of_term c with | Prod (_,_,c) -> isArity c | LetIn (_,b,_,c) -> isArity (subst1 b c) - | Cast (c,_) -> isArity c + | Cast (c,_,_) -> isArity c | Sort _ -> true | _ -> false @@ -144,7 +145,7 @@ let decompose_prod_assum = match kind_of_term c with | Prod (x,t,c) -> prodec_rec (add_rel_decl (x,None,t) l) c | LetIn (x,b,t,c) -> prodec_rec (add_rel_decl (x,Some b,t) l) c - | Cast (c,_) -> prodec_rec l c + | Cast (c,_,_) -> prodec_rec l c | _ -> l,c in prodec_rec empty_rel_context @@ -156,7 +157,7 @@ let decompose_lam_assum = match kind_of_term c with | Lambda (x,t,c) -> lamdec_rec (add_rel_decl (x,None,t) l) c | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) c - | Cast (c,_) -> lamdec_rec l c + | Cast (c,_,_) -> lamdec_rec l c | _ -> l,c in lamdec_rec empty_rel_context @@ -171,7 +172,7 @@ let decompose_prod_n_assum n = else match kind_of_term c with | Prod (x,t,c) -> prodec_rec (add_rel_decl (x,None,t) l) (n-1) c | LetIn (x,b,t,c) -> prodec_rec (add_rel_decl (x,Some b,t) l) (n-1) c - | Cast (c,_) -> prodec_rec l n c + | Cast (c,_,_) -> prodec_rec l n c | c -> error "decompose_prod_n_assum: not enough assumptions" in prodec_rec empty_rel_context n @@ -186,7 +187,7 @@ let decompose_lam_n_assum n = else match kind_of_term c with | Lambda (x,t,c) -> lamdec_rec (add_rel_decl (x,None,t) l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec (add_rel_decl (x,Some b,t) l) (n-1) c - | Cast (c,_) -> lamdec_rec l n c + | Cast (c,_,_) -> lamdec_rec l n c | c -> error "decompose_lam_n_assum: not enough abstractions" in lamdec_rec empty_rel_context n |