From 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Wed, 21 Jul 2010 09:46:51 +0200 Subject: Imported Upstream snapshot 8.3~beta0+13298 --- kernel/term.ml | 325 ++++++++++++++++++++++++++++++++++++++++----------------- 1 file changed, 229 insertions(+), 96 deletions(-) (limited to 'kernel/term.ml') diff --git a/kernel/term.ml b/kernel/term.ml index 1f3d2635..68565659 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: term.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id$ *) (* This module instantiates the structure of generic deBruijn terms to Coq *) @@ -26,7 +26,7 @@ type metavariable = int (* This defines Cases annotations *) type case_style = LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle type case_printing = - { ind_nargs : int; (* number of real args of the inductive type *) + { ind_nargs : int; (* length of the arity of the inductive type *) style : case_style } type case_info = { ci_ind : inductive; @@ -42,7 +42,7 @@ type contents = Pos | Null type sorts = | Prop of contents (* proposition types *) | Type of universe - + let prop_sort = Prop Null let set_sort = Prop Pos let type1_sort = Type type1_univ @@ -58,7 +58,7 @@ let family_of_sort = function (* Constructions as implemented *) (********************************************************************) -type cast_kind = VMcast | DEFAULTcast +type cast_kind = VMcast | DEFAULTcast (* [constr array] is an instance matching definitional [named_context] in the same order (i.e. last argument first) *) @@ -93,7 +93,7 @@ type ('constr, 'types) kind_of_term = (* Experimental *) type ('constr, 'types) kind_of_type = | SortType of sorts - | CastType of 'types * 'types + | CastType of 'types * 'types | ProdType of name * 'types * 'types | LetInType of name * 'constr * 'types * 'types | AtomicType of 'constr * 'constr array @@ -118,7 +118,7 @@ type fixpoint = (int array * int) * rec_declaration type cofixpoint = int * rec_declaration (***************************) -(* hash-consing functions *) +(* hash-consing functions *) (***************************) let comp_term t1 t2 = @@ -184,7 +184,7 @@ module Hconstr = type t = constr type u = (constr -> constr) * ((sorts -> sorts) * (constant -> constant) * - (kernel_name -> kernel_name) * (name -> name) * + (mutual_inductive -> mutual_inductive) * (name -> name) * (identifier -> identifier)) let hash_sub = hash_term let equal = comp_term @@ -211,7 +211,7 @@ let mkVar id = Var id let mkSort s = Sort s (* Constructs the term t1::t2, i.e. the term t1 casted with the type t2 *) -(* (that means t2 is declared as the type of t1) +(* (that means t2 is declared as the type of t1) [s] is the strategy to use when *) let mkCast (t1,k2,t2) = match t1 with @@ -230,14 +230,14 @@ let mkLetIn (x,c1,t,c2) = LetIn (x,c1,t,c2) (* If lt = [t1; ...; tn], constructs the application (t1 ... tn) *) (* We ensure applicative terms have at least one argument and the function is not itself an applicative term *) -let mkApp (f, a) = +let mkApp (f, a) = if Array.length a = 0 then f else match f with | App (g, cl) -> App (g, Array.append cl a) | _ -> App (f, a) -(* Constructs a constant *) +(* Constructs a constant *) (* The array of terms correspond to the variables introduced in the section *) let mkConst c = Const c @@ -248,7 +248,7 @@ let mkEvar e = Evar e (* The array of terms correspond to the variables introduced in the section *) let mkInd m = Ind m -(* Constructs the jth constructor of the ith (co)inductive type of the +(* Constructs the jth constructor of the ith (co)inductive type of the block named kn. The array of terms correspond to the variables introduced in the section *) let mkConstruct c = Construct c @@ -261,6 +261,7 @@ let mkFix fix = Fix fix let mkCoFix cofix = CoFix cofix let kind_of_term c = c +let kind_of_term2 c = c (************************************************************************) (* kind_of_term = constructions as seen by the user *) @@ -284,7 +285,7 @@ type hnftype = (* Non primitive term destructors *) (**********************************************************************) -(* Destructor operations : partial functions +(* Destructor operations : partial functions Raise invalid_arg "dest*" if the const has not the expected form *) (* Destructs a DeBrujin index *) @@ -348,8 +349,12 @@ let same_kind c1 c2 = (isprop c1 & isprop c2) or (is_Type c1 & is_Type c2) (* Tests if an evar *) let isEvar c = match kind_of_term c with Evar _ -> true | _ -> false +let isEvar_or_Meta c = match kind_of_term c with + | Evar _ | Meta _ -> true + | _ -> false + (* Destructs a casted term *) -let destCast c = match kind_of_term c with +let destCast c = match kind_of_term c with | Cast (t1,k,t2) -> (t1,k,t2) | _ -> invalid_arg "destCast" @@ -366,22 +371,22 @@ let isVar c = match kind_of_term c with Var _ -> true | _ -> false let isInd c = match kind_of_term c with Ind _ -> true | _ -> false (* Destructs the product (x:t1)t2 *) -let destProd c = match kind_of_term c with - | Prod (x,t1,t2) -> (x,t1,t2) +let destProd c = match kind_of_term c with + | Prod (x,t1,t2) -> (x,t1,t2) | _ -> invalid_arg "destProd" let isProd c = match kind_of_term c with | Prod _ -> true | _ -> false (* Destructs the abstraction [x:t1]t2 *) -let destLambda c = match kind_of_term c with - | Lambda (x,t1,t2) -> (x,t1,t2) +let destLambda c = match kind_of_term c with + | Lambda (x,t1,t2) -> (x,t1,t2) | _ -> invalid_arg "destLambda" let isLambda c = match kind_of_term c with | Lambda _ -> true | _ -> false (* Destructs the let [x:=b:t1]t2 *) -let destLetIn c = match kind_of_term c with - | LetIn (x,b,t1,t2) -> (x,b,t1,t2) +let destLetIn c = match kind_of_term c with + | LetIn (x,b,t1,t2) -> (x,b,t1,t2) | _ -> invalid_arg "destProd" let isLetIn c = match kind_of_term c with LetIn _ -> true | _ -> false @@ -430,13 +435,13 @@ let destCase c = match kind_of_term c with let isCase c = match kind_of_term c with Case _ -> true | _ -> false -let destFix c = match kind_of_term c with +let destFix c = match kind_of_term c with | Fix fix -> fix | _ -> invalid_arg "destFix" let isFix c = match kind_of_term c with Fix _ -> true | _ -> false -let destCoFix c = match kind_of_term c with +let destCoFix c = match kind_of_term c with | CoFix cofix -> cofix | _ -> invalid_arg "destCoFix" @@ -466,7 +471,7 @@ let rec under_casts f c = match kind_of_term c with (* flattens application lists throwing casts in-between *) let rec collapse_appl c = match kind_of_term c with - | App (f,cl) -> + | App (f,cl) -> let rec collapse_rec f cl2 = match kind_of_term (strip_outer_cast f) with | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2) @@ -482,12 +487,12 @@ let decompose_app c = (* strips head casts and flattens head applications *) let rec strip_head_cast c = match kind_of_term c with - | App (f,cl) -> + | App (f,cl) -> let rec collapse_rec f cl2 = match kind_of_term f with | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2) | Cast (c,_,_) -> collapse_rec c cl2 | _ -> if Array.length cl2 = 0 then f else mkApp (f,cl2) - in + in collapse_rec f cl | Cast (c,_,_) -> strip_head_cast c | _ -> c @@ -550,7 +555,7 @@ let iter_constr_with_binders g f n c = match kind_of_term c with | App (c,l) -> f n c; Array.iter (f n) l | Evar (_,l) -> Array.iter (f n) l | Case (_,p,c,bl) -> f n p; f n c; Array.iter (f n) bl - | Fix (_,(_,tl,bl)) -> + | Fix (_,(_,tl,bl)) -> Array.iter (f n) tl; Array.iter (f (iterate g (Array.length tl) n)) bl | CoFix (_,(_,tl,bl)) -> @@ -604,6 +609,7 @@ let map_constr_with_binders g f l c = match kind_of_term c with application associativity, binders name and Cases annotations are not taken into account *) + let compare_constr f t1 t2 = match kind_of_term t1, kind_of_term t2 with | Rel n1, Rel n2 -> n1 = n2 @@ -619,15 +625,15 @@ let compare_constr f t1 t2 = if Array.length l1 = Array.length l2 then f c1 c2 & array_for_all2 f l1 l2 else - let (h1,l1) = decompose_app t1 in + let (h1,l1) = decompose_app t1 in let (h2,l2) = decompose_app t2 in if List.length l1 = List.length l2 then f h1 h2 & List.for_all2 f l1 l2 else false | Evar (e1,l1), Evar (e2,l2) -> e1 = e2 & array_for_all2 f l1 l2 - | Const c1, Const c2 -> c1 = c2 - | Ind c1, Ind c2 -> c1 = c2 - | Construct c1, Construct c2 -> c1 = c2 + | Const c1, Const c2 -> eq_constant c1 c2 + | Ind c1, Ind c2 -> eq_ind c1 c2 + | Construct c1, Construct c2 -> eq_constructor c1 c2 | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> f p1 p2 & f c1 c2 & array_for_all2 f bl1 bl2 | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) -> @@ -642,7 +648,7 @@ let compare_constr f t1 t2 = type types = constr -type strategy = types option +type strategy = types option type named_declaration = identifier * constr option * types type rel_declaration = name * constr option * types @@ -653,6 +659,34 @@ let map_rel_declaration = map_named_declaration let fold_named_declaration f (_, v, ty) a = f ty (Option.fold_right f v a) let fold_rel_declaration = fold_named_declaration +(***************************************************************************) +(* Type of local contexts (telescopes) *) +(***************************************************************************) + +(*s Signatures of ordered optionally named variables, intended to be + accessed by de Bruijn indices (to represent bound variables) *) + +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 + (****************************************************************************) (* Functions for dealing with constr terms *) (****************************************************************************) @@ -666,11 +700,11 @@ exception LocalOccur (* (closedn n M) raises FreeVar if a variable of height greater than n occurs in M, returns () otherwise *) -let closedn n c = +let closedn n c = let rec closed_rec n c = match kind_of_term c with | Rel m -> if m>n then raise LocalOccur | _ -> iter_constr_with_binders succ closed_rec n c - in + in try closed_rec n c; true with LocalOccur -> false (* [closed0 M] is true iff [M] is a (deBruijn) closed term *) @@ -679,21 +713,21 @@ let closed0 = closedn 0 (* (noccurn n M) returns true iff (Rel n) does NOT occur in term M *) -let noccurn n term = +let noccurn n term = let rec occur_rec n c = match kind_of_term c with | Rel m -> if m = n then raise LocalOccur | _ -> iter_constr_with_binders succ occur_rec n c - in + in try occur_rec n term; true with LocalOccur -> false -(* (noccur_between n m M) returns true iff (Rel p) does NOT occur in term M +(* (noccur_between n m M) returns true iff (Rel p) does NOT occur in term M for n <= p < n+m *) -let noccur_between n m term = +let noccur_between n m term = let rec occur_rec n c = match kind_of_term c with | Rel(p) -> if n<=p && p iter_constr_with_binders succ occur_rec n c - in + in try occur_rec n term; true with LocalOccur -> false (* Checking function for terms containing existential variables. @@ -703,7 +737,7 @@ let noccur_between n m term = which may contain the CoFix variables. These occurrences of CoFix variables are not considered *) -let noccur_with_meta n m term = +let noccur_with_meta n m term = let rec occur_rec n c = match kind_of_term c with | Rel p -> if n<=p & p @@ -728,18 +762,18 @@ let rec exliftn el c = match kind_of_term c with (* Lifting the binding depth across k bindings *) -let liftn k n = +let liftn k n = match el_liftn (pred n) (el_shft k ELID) with | ELID -> (fun c -> c) | el -> exliftn el - + let lift k = liftn k 1 (*********************) (* Substituting *) (*********************) -(* (subst1 M c) substitutes M for Rel(1) in c +(* (subst1 M c) substitutes M for Rel(1) in c we generalise it to (substl [M1,...,Mn] c) which substitutes in parallel M1,...,Mn for respectively Rel(1),...,Rel(n) in c *) @@ -759,15 +793,15 @@ let rec lift_substituend depth s = let make_substituend c = { sinfo=Unknown; sit=c } let substn_many lamv n c = - let lv = Array.length lamv in + let lv = Array.length lamv in if lv = 0 then c - else + else let rec substrec depth c = match kind_of_term c with | Rel k -> if k<=depth then c else if k-depth <= lv then lift_substituend depth lamv.(k-depth-1) else mkRel (k-lv) - | _ -> map_constr_with_binders succ substrec depth c in + | _ -> map_constr_with_binders succ substrec depth c in substrec n c (* @@ -791,21 +825,21 @@ let substl_named_decl = substl_decl let rec thin_val = function | [] -> [] - | (((id,{ sit = v }) as s)::tl) when isVar v -> + | (((id,{ sit = v }) as s)::tl) when isVar v -> if id = destVar v then thin_val tl else s::(thin_val tl) | h::tl -> h::(thin_val tl) (* (replace_vars sigma M) applies substitution sigma to term M *) -let replace_vars var_alist = +let replace_vars var_alist = let var_alist = List.map (fun (str,c) -> (str,make_substituend c)) var_alist in - let var_alist = thin_val var_alist in + let var_alist = thin_val var_alist in let rec substrec n c = match kind_of_term c with | Var x -> (try lift_substituend n (List.assoc x var_alist) with Not_found -> c) | _ -> map_constr_with_binders succ substrec n c - in + in if var_alist = [] then (function x -> x) else substrec 0 (* @@ -910,7 +944,7 @@ let mkAppA v = if l=0 then anomaly "mkAppA received an empty array" else mkApp (v.(0), Array.sub v 1 (Array.length v -1)) -(* Constructs a constant *) +(* Constructs a constant *) (* The array of terms correspond to the variables introduced in the section *) let mkConst = mkConst @@ -921,7 +955,7 @@ let mkEvar = mkEvar (* The array of terms correspond to the variables introduced in the section *) let mkInd = mkInd -(* Constructs the jth constructor of the ith (co)inductive type of the +(* Constructs the jth constructor of the ith (co)inductive type of the block named kn. The array of terms correspond to the variables introduced in the section *) let mkConstruct = mkConstruct @@ -930,15 +964,15 @@ let mkConstruct = mkConstruct let mkCase = mkCase let mkCaseL (ci, p, c, ac) = mkCase (ci, p, c, Array.of_list ac) -(* If recindxs = [|i1,...in|] +(* If recindxs = [|i1,...in|] funnames = [|f1,...fn|] typarray = [|t1,...tn|] bodies = [|b1,...bn|] - then + then mkFix ((recindxs,i),(funnames,typarray,bodies)) - - constructs the ith function of the block + + constructs the ith function of the block Fixpoint f1 [ctx1] : t1 := b1 with f2 [ctx2] : t2 := b2 @@ -953,12 +987,12 @@ let mkFix = mkFix (* If funnames = [|f1,...fn|] typarray = [|t1,...tn|] bodies = [|b1,...bn|] - then + then mkCoFix (i,(funnames,typsarray,bodies)) - constructs the ith function of the block - + constructs the ith function of the block + CoFixpoint f1 : t1 := b1 with f2 : t2 := b2 ... @@ -984,7 +1018,7 @@ let prodn n env b = | (0, env, b) -> b | (n, ((v,t)::l), b) -> prodrec (n-1, l, mkProd (v,t,b)) | _ -> assert false - in + in prodrec (n,env,b) (* compose_prod [xn:Tn;..;x1:T1] b = (x1:T1)..(xn:Tn)b *) @@ -996,7 +1030,7 @@ let lamn n env b = | (0, env, b) -> b | (n, ((v,t)::l), b) -> lamrec (n-1, l, mkLambda (v,t,b)) | _ -> assert false - in + in lamrec (n,env,b) (* compose_lam [xn:Tn;..;x1:T1] b = [x1:T1]..[xn:Tn]b *) @@ -1007,29 +1041,29 @@ let applist (f,l) = mkApp (f, Array.of_list l) let applistc f l = mkApp (f, Array.of_list l) let appvect = mkApp - + let appvectc f l = mkApp (f,l) - + (* to_lambda n (x1:T1)...(xn:Tn)T = * [x1:T1]...[xn:Tn]T *) let rec to_lambda n prod = - if n = 0 then - prod - else - match kind_of_term prod with + if n = 0 then + prod + else + match kind_of_term prod with | Prod (na,ty,bd) -> mkLambda (na,ty,to_lambda (n-1) bd) | Cast (c,_,_) -> to_lambda n c - | _ -> errorlabstrm "to_lambda" (mt ()) + | _ -> errorlabstrm "to_lambda" (mt ()) let rec to_prod n lam = - if n=0 then + if n=0 then lam - else - match kind_of_term lam with + else + match kind_of_term lam with | Lambda (na,ty,bd) -> mkProd (na,ty,to_prod (n-1) bd) | Cast (c,_,_) -> to_prod n c - | _ -> errorlabstrm "to_prod" (mt ()) - + | _ -> errorlabstrm "to_prod" (mt ()) + (* pseudo-reduction rule: * [prod_app s (Prod(_,B)) N --> B[N] * with an strip_outer_cast on the first argument to produce a product *) @@ -1048,91 +1082,190 @@ let prod_appvect t nL = Array.fold_left prod_app t nL (* prod_applist T [ a1 ; ... ; an ] -> (T a1 ... an) *) let prod_applist t nL = List.fold_left prod_app t nL +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) + (*********************************) (* Other term destructors *) (*********************************) (* 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 = +let decompose_prod = let rec prodec_rec l c = match kind_of_term c with | Prod (x,t,c) -> prodec_rec ((x,t)::l) c | Cast (c,_,_) -> prodec_rec l c | _ -> l,c - in + in prodec_rec [] (* 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 = +let decompose_lam = let rec lamdec_rec l c = match kind_of_term c with | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) c | Cast (c,_,_) -> lamdec_rec l c | _ -> l,c - in + in lamdec_rec [] -(* Given a positive integer n, transforms a product term (x1:T1)..(xn:Tn)T +(* 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 n = if n < 0 then error "decompose_prod_n: 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 + 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 ((x,t)::l) (n-1) c | Cast (c,_,_) -> prodec_rec l n c | _ -> error "decompose_prod_n: not enough products" - in - prodec_rec [] n + in + prodec_rec [] n -(* Given a positive integer n, transforms a lambda term [x1:T1]..[xn:Tn]T +(* 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 n = if n < 0 then error "decompose_lam_n: 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 + 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 ((x,t)::l) (n-1) c | Cast (c,_,_) -> lamdec_rec l n c | _ -> error "decompose_lam_n: not enough abstractions" - in - lamdec_rec [] n + in + lamdec_rec [] n + +(* 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 (* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction * gives n (casts are ignored) *) -let nb_lam = +let nb_lam = let rec nbrec n c = match kind_of_term c with | Lambda (_,_,c) -> nbrec (n+1) c | Cast (c,_,_) -> nbrec n c | _ -> n - in + in nbrec 0 - + (* similar to nb_lam, but gives the number of products instead *) -let nb_prod = +let nb_prod = let rec nbrec n c = match kind_of_term c with | Prod (_,_,c) -> nbrec (n+1) c | Cast (c,_,_) -> nbrec n c | _ -> n - in + in nbrec 0 -(* Rem: end of import from old module Generic *) +let prod_assum t = fst (decompose_prod_assum t) +let prod_n_assum n t = fst (decompose_prod_n_assum n t) +let strip_prod_assum t = snd (decompose_prod_assum t) +let strip_prod t = snd (decompose_prod t) +let strip_prod_n n t = snd (decompose_prod_n n t) +let lam_assum t = fst (decompose_lam_assum t) +let lam_n_assum n t = fst (decompose_lam_n_assum n t) +let strip_lam_assum t = snd (decompose_lam_assum t) +let strip_lam t = snd (decompose_lam t) +let strip_lam_n n t = snd (decompose_lam_n n t) + +(***************************) +(* Arities *) +(***************************) + +(* An "arity" is a term of the form [[x1:T1]...[xn:Tn]s] with [s] a sort. + Such a term can canonically be seen as the pair of a context of types + and of a sort *) + +type arity = rel_context * sorts + +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 (*******************************) -(* alpha conversion functions *) +(* alpha conversion functions *) (*******************************) (* alpha conversion : ignore print names and casts *) -let rec eq_constr m n = +let rec eq_constr m n = (m==n) or compare_constr eq_constr m n let eq_constr m n = eq_constr m n (* to avoid tracing a recursive fun *) (*******************) -(* hash-consing *) +(* hash-consing *) (*******************) module Htype = -- cgit v1.2.3