summaryrefslogtreecommitdiff
path: root/kernel/sign.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/sign.ml')
-rw-r--r--kernel/sign.ml192
1 files changed, 192 insertions, 0 deletions
diff --git a/kernel/sign.ml b/kernel/sign.ml
new file mode 100644
index 00000000..a4b2a2ea
--- /dev/null
+++ b/kernel/sign.ml
@@ -0,0 +1,192 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id: sign.ml,v 1.37.2.1 2004/07/16 19:30:26 herbelin Exp $ *)
+
+open Names
+open Util
+open Term
+
+(*s Signatures of named hypotheses. Used for section variables and
+ goal assumptions. *)
+
+type named_context = named_declaration list
+
+let empty_named_context = []
+
+let add_named_decl d sign = d::sign
+
+let rec lookup_named id = function
+ | (id',_,_ as decl) :: _ when id=id' -> decl
+ | _ :: sign -> lookup_named id sign
+ | [] -> raise Not_found
+
+let named_context_length = List.length
+
+let vars_of_named_context = List.map (fun (id,_,_) -> id)
+
+let instance_from_named_context sign =
+ let rec inst_rec = function
+ | (id,None,_) :: sign -> mkVar id :: inst_rec sign
+ | _ :: sign -> inst_rec sign
+ | [] -> [] in
+ Array.of_list (inst_rec sign)
+
+let fold_named_context f l ~init = List.fold_right f l init
+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 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 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
+
+let map_rel_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
+ if body_o' == body_o && typ' == typ then decl else
+ (n, body_o', typ')
+ in
+ list_smartmap map_decl l
+
+(* Push named declarations on top of a rel context *)
+(* Bizarre. Should be avoided. *)
+let push_named_to_rel_context hyps ctxt =
+ let rec push = function
+ | (id,b,t) :: l ->
+ let s, hyps = push l in
+ let d = (Name id, option_app (subst_vars s) b, type_app (subst_vars s) t) in
+ id::s, d::hyps
+ | [] -> [],[] in
+ let s, hyps = push hyps in
+ let rec subst = function
+ | d :: l ->
+ let n, ctxt = subst l in
+ (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) *)
+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-1) c
+ | Cast (c,_) -> lamdec_rec l n c
+ | c -> error "decompose_lam_n_assum: not enough abstractions"
+ in
+ lamdec_rec empty_rel_context n
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 19:37:20 +0000