diff options
Diffstat (limited to 'kernel/sign.ml')
| -rw-r--r-- | kernel/sign.ml | 122 |
1 files changed, 1 insertions, 121 deletions
diff --git a/kernel/sign.ml b/kernel/sign.ml index 8fa59809..d30d7086 100644 --- a/kernel/sign.ml +++ b/kernel/sign.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: sign.ml 10451 2008-01-18 17:20:28Z barras $ *) +(* $Id$ *) open Names open Util @@ -43,31 +43,6 @@ let fold_named_context_reverse f ~init l = List.fold_left f init l (*s Signatures of ordered section variables *) type section_context = named_context -(*s Signatures of ordered optionally named variables, intended to be - accessed by de Bruijn indices (to represent bound variables) *) - -type rel_declaration = name * constr option * types -type rel_context = rel_declaration list - -let empty_rel_context = [] - -let add_rel_decl d ctxt = d::ctxt - -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 - -let rel_context_nhyps hyps = - let rec nhyps acc = function - | [] -> acc - | (_,None,_)::hyps -> nhyps (1+acc) hyps - | (_,Some _,_)::hyps -> nhyps acc hyps in - nhyps 0 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 @@ -102,98 +77,3 @@ let push_named_to_rel_context hyps ctxt = (n+1), (map_rel_declaration (substn_vars n s) d)::ctxt | [] -> 1, hyps in snd (subst ctxt) - - -(*********************************) -(* Term constructors *) -(*********************************) - -let it_mkProd_or_LetIn = List.fold_left (fun c d -> mkProd_or_LetIn d c) -let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c) - -(*********************************) -(* Term destructors *) -(*********************************) - -type arity = rel_context * sorts - -(* Decompose an arity (i.e. a product of the form (x1:T1)..(xn:Tn)s - with s a sort) into the pair ([(xn,Tn);...;(x1,T1)],s) *) - -let destArity = - let rec prodec_rec l c = - 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 - | Sort s -> l,s - | _ -> anomaly "destArity: not an arity" - in - prodec_rec [] - -let mkArity (sign,s) = it_mkProd_or_LetIn (mkSort s) sign - -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 - | Sort _ -> true - | _ -> false - -(* Transforms a product term (x1:T1)..(xn:Tn)T into the pair - ([(xn,Tn);...;(x1,T1)],T), where T is not a product *) -let decompose_prod_assum = - let rec prodec_rec l c = - 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 - | _ -> l,c - in - prodec_rec empty_rel_context - -(* Transforms a lambda term [x1:T1]..[xn:Tn]T into the pair - ([(xn,Tn);...;(x1,T1)],T), where T is not a lambda *) -let decompose_lam_assum = - let rec lamdec_rec l c = - 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 - | _ -> l,c - in - lamdec_rec empty_rel_context - -(* Given a positive integer n, transforms a product term (x1:T1)..(xn:Tn)T - into the pair ([(xn,Tn);...;(x1,T1)],T) *) -let decompose_prod_n_assum n = - if n < 0 then - error "decompose_prod_n_assum: integer parameter must be positive"; - let rec prodec_rec l n c = - if n=0 then l,c - 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 - | c -> error "decompose_prod_n_assum: not enough assumptions" - in - prodec_rec empty_rel_context n - -(* Given a positive integer n, transforms a lambda term [x1:T1]..[xn:Tn]T - into the pair ([(xn,Tn);...;(x1,T1)],T) - Lets in between are not expanded but turn into local definitions, - but n is the actual number of destructurated lambdas. *) -let decompose_lam_n_assum n = - if n < 0 then - error "decompose_lam_n_assum: integer parameter must be positive"; - let rec lamdec_rec l n c = - if n=0 then l,c - 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 c - | Cast (c,_,_) -> lamdec_rec l n c - | c -> error "decompose_lam_n_assum: not enough abstractions" - in - lamdec_rec empty_rel_context n - |