From 14edc57ac5ad75bbc4ea8559111606aea8978f48 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 18 Oct 2015 19:35:57 +0200 Subject: Adding a function to mirror decompose_prod_n_assum in that it counts let-ins, to compensate decompose_lam_n_assum which does not count let-ins. Any idea on a uniform and clear naming scheme for this kind of decomposition functions? --- kernel/term.ml | 28 +++++++++++++++++++++++----- 1 file changed, 23 insertions(+), 5 deletions(-) (limited to 'kernel/term.ml') diff --git a/kernel/term.ml b/kernel/term.ml index 7bf4c8182d..33ed25fe1b 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -566,8 +566,10 @@ let decompose_lam_assum = 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) *) +(* Given a positive integer n, decompose a product or let-in term + of the form [forall (x1:T1)..(xi:=ci:Ti)..(xn:Tn), T] into the pair + of the quantifying context [(xn,None,Tn);..;(xi,Some + ci,Ti);..;(x1,None,T1)] and of the inner type [T]) *) let decompose_prod_n_assum n = if n < 0 then error "decompose_prod_n_assum: integer parameter must be positive"; @@ -581,10 +583,12 @@ let decompose_prod_n_assum n = 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) +(* Given a positive integer n, decompose a lambda or let-in term [fun + (x1:T1)..(xi:=ci:Ti)..(xn:Tn) => T] into the pair of the abstracted + context [(xn,None,Tn);...;(xi,Some ci,Ti);...;(x1,None,T1)] and of + the inner body [T]. Lets in between are not expanded but turn into local definitions, - but n is the actual number of destructurated lambdas. *) + 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"; @@ -598,6 +602,20 @@ let decompose_lam_n_assum n = in lamdec_rec empty_rel_context n +(* Same, counting let-in *) +let decompose_lam_n_decls n = + if n < 0 then + error "decompose_lam_n_decls: integer parameter must be positive"; + let rec lamdec_rec l n c = + if Int.equal 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_decls: 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 = -- cgit v1.2.3 From 2e3ee15b03cf4b7428e1a7453385d79f434ec4a7 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 8 Nov 2015 09:54:42 +0100 Subject: Moving three related small half-general half-ad-hoc utility functions next to each other, waiting for possible integration into a more uniform API. --- kernel/term.ml | 19 ------------------- 1 file changed, 19 deletions(-) (limited to 'kernel/term.ml') diff --git a/kernel/term.ml b/kernel/term.ml index 33ed25fe1b..7d47c46097 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -616,25 +616,6 @@ let decompose_lam_n_decls n = 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 rec nbrec n c = match kind_of_term c with - | Lambda (_,_,c) -> nbrec (n+1) c - | Cast (c,_,_) -> nbrec n c - | _ -> n - in - nbrec 0 - -(* similar to nb_lam, but gives the number of products instead *) -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 - nbrec 0 - 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) -- cgit v1.2.3 From e8c47b652a0b53f8d3f7eaa877e81910c8de55d0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 22 Nov 2015 17:11:39 +0100 Subject: Unifying betazeta_applist and prod_applist into a clearer interface. - prod_applist - prod_applist_assum - lambda_applist - lambda_applist_assum expect an instance matching the quantified context. They are now in term.ml, with "list" being possibly "vect". Names are a bit arbitrary. Better propositions are welcome. They are put in term.ml in that reduction is after all not needed, because the intent is not to do β or ι on the fly but rather to substitute a λΓ.c or ∀Γ.c (seen as internalization of a Γ⊢c) into one step, independently of the idea of reducing. On the other side: - beta_applist - beta_appvect are seen as optimizations of application doing reduction on the fly only if possible. They are then kept as functions relevant for reduction.ml. --- kernel/term.ml | 63 ++++++++++++++++++++++++++++++++++++++++++++++++---------- 1 file changed, 53 insertions(+), 10 deletions(-) (limited to 'kernel/term.ml') diff --git a/kernel/term.ml b/kernel/term.ml index 7d47c46097..455248dd52 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -471,6 +471,36 @@ let rec to_prod n lam = | Cast (c,_,_) -> to_prod n c | _ -> errorlabstrm "to_prod" (mt ()) +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) + +(* Application with expected on-the-fly reduction *) + +let lambda_applist c l = + let rec app subst c l = + match kind_of_term c, l with + | Lambda(_,_,c), arg::l -> app (arg::subst) c l + | _, [] -> substl subst c + | _ -> anomaly (Pp.str "Not enough lambda's") in + app [] c l + +let lambda_appvect c v = lambda_applist c (Array.to_list v) + +let lambda_app c a = lambda_applist c [a] + +let lambda_applist_assum n c l = + let rec app n subst t l = + if Int.equal n 0 then + if l == [] then substl subst t + else anomaly (Pp.str "Not enough arguments") + else match kind_of_term t, l with + | Lambda(_,_,c), arg::l -> app (n-1) (arg::subst) c l + | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l + | _ -> anomaly (Pp.str "Not enough lambda/let's") in + app n [] c l + +let lambda_appvect_assum n c v = lambda_applist_assum n c (Array.to_list v) + (* pseudo-reduction rule: * [prod_app s (Prod(_,B)) N --> B[N] * with an strip_outer_cast on the first argument to produce a product *) @@ -478,19 +508,32 @@ let rec to_prod n lam = let prod_app t n = match kind_of_term (strip_outer_cast t) with | Prod (_,_,b) -> subst1 n b - | _ -> - errorlabstrm "prod_app" - (str"Needed a product, but didn't find one" ++ fnl ()) - - -(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *) -let prod_appvect t nL = Array.fold_left prod_app t nL + | _ -> anomaly (str"Needed a product, but didn't find one") (* prod_applist T [ a1 ; ... ; an ] -> (T a1 ... an) *) -let prod_applist t nL = List.fold_left prod_app t nL +let prod_applist c l = + let rec app subst c l = + match kind_of_term c, l with + | Prod(_,_,c), arg::l -> app (arg::subst) c l + | _, [] -> substl subst c + | _ -> anomaly (Pp.str "Not enough prod's") in + app [] c l -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) +(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *) +let prod_appvect c v = prod_applist c (Array.to_list v) + +let prod_applist_assum n c l = + let rec app n subst t l = + if Int.equal n 0 then + if l == [] then substl subst t + else anomaly (Pp.str "Not enough arguments") + else match kind_of_term t, l with + | Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l + | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l + | _ -> anomaly (Pp.str "Not enough prod/let's") in + app n [] c l + +let prod_appvect_assum n c v = prod_applist_assum n c (Array.to_list v) (*********************************) (* Other term destructors *) -- cgit v1.2.3 From 80bbdf335be5657f5ab33b4aa02e21420d341de2 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 2 Jan 2016 17:11:03 +0100 Subject: Remove some unused functions. Note: they do not even seem to have a debugging purpose, so better remove them before they bitrot. --- kernel/term.ml | 11 ----------- 1 file changed, 11 deletions(-) (limited to 'kernel/term.ml') diff --git a/kernel/term.ml b/kernel/term.ml index 455248dd52..2060c7b6e9 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -486,8 +486,6 @@ let lambda_applist c l = let lambda_appvect c v = lambda_applist c (Array.to_list v) -let lambda_app c a = lambda_applist c [a] - let lambda_applist_assum n c l = let rec app n subst t l = if Int.equal n 0 then @@ -501,15 +499,6 @@ let lambda_applist_assum n c l = let lambda_appvect_assum n c v = lambda_applist_assum n c (Array.to_list v) -(* pseudo-reduction rule: - * [prod_app s (Prod(_,B)) N --> B[N] - * with an strip_outer_cast on the first argument to produce a product *) - -let prod_app t n = - match kind_of_term (strip_outer_cast t) with - | Prod (_,_,b) -> subst1 n b - | _ -> anomaly (str"Needed a product, but didn't find one") - (* prod_applist T [ a1 ; ... ; an ] -> (T a1 ... an) *) let prod_applist c l = let rec app subst c l = -- cgit v1.2.3 From 9d991d36c07efbb6428e277573bd43f6d56788fc Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 8 Jan 2016 10:00:21 +0100 Subject: CLEANUP: kernel/context.ml{,i} The structure of the Context module was refined in such a way that: - Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module. - Types and functions related to rel-context were put into the Context.Rel module. - Types and functions related to named-context declarations were put into the Context.Named.Declaration module. - Types and functions related to named-context were put into the Context.Named module. - Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module. - Types and functions related to named-list-context were put into Context.NamedList module. Some missing comments were added to the *.mli file. The output of ocamldoc was checked whether it looks in a reasonable way. "TODO: cleanup" was removed The order in which are exported functions listed in the *.mli file was changed. (as in a mature modules, this order usually is not random) The order of exported functions in Context.{Rel,Named} modules is now consistent. (as there is no special reason why that order should be different) The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file. (as there is no special reason to define them in a different order) The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do. (Now they are called Context.{Rel,Named}.fold_{inside,outside}) The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated. Thrown exceptions are now documented. Naming of formal parameters was made more consistent across different functions. Comments of similar functions in different modules are now consistent. Comments from *.mli files were copied to *.ml file. (We need that information in *.mli files because that is were ocamldoc needs it. It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function, we can see the comments also there and do not need to open a different file if we want to see it.) When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1. (UTF-8 characters are used in our ocamldoc markup) "open Context" was removed from all *.mli and *.ml files. (Originally, it was OK to do that. Now it is not.) An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed. --- kernel/term.ml | 33 ++++++++++++++++----------------- 1 file changed, 16 insertions(+), 17 deletions(-) (limited to 'kernel/term.ml') diff --git a/kernel/term.ml b/kernel/term.ml index 455248dd52..19f4b7a234 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -10,7 +10,6 @@ open Util open Pp open Errors open Names -open Context open Vars (**********************************************************************) @@ -590,24 +589,24 @@ let decompose_lam_n n = 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 + | Prod (x,t,c) -> prodec_rec (Context.Rel.add (x,None,t) l) c + | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (x,Some b,t) l) c | Cast (c,_,_) -> prodec_rec l c | _ -> l,c in - prodec_rec empty_rel_context + prodec_rec Context.Rel.empty (* 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 + | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (x,None,t) l) c + | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (x,Some b,t) l) c | Cast (c,_,_) -> lamdec_rec l c | _ -> l,c in - lamdec_rec empty_rel_context + lamdec_rec Context.Rel.empty (* Given a positive integer n, decompose a product or let-in term of the form [forall (x1:T1)..(xi:=ci:Ti)..(xn:Tn), T] into the pair @@ -619,12 +618,12 @@ let decompose_prod_n_assum n = let rec prodec_rec l n c = if Int.equal 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 + | Prod (x,t,c) -> prodec_rec (Context.Rel.add (x,None,t) l) (n-1) c + | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (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 + prodec_rec Context.Rel.empty n (* Given a positive integer n, decompose a lambda or let-in term [fun (x1:T1)..(xi:=ci:Ti)..(xn:Tn) => T] into the pair of the abstracted @@ -638,12 +637,12 @@ let decompose_lam_n_assum n = let rec lamdec_rec l n c = if Int.equal 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 + | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (x,None,t) l) (n-1) c + | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (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 + lamdec_rec Context.Rel.empty n (* Same, counting let-in *) let decompose_lam_n_decls n = @@ -652,12 +651,12 @@ let decompose_lam_n_decls n = let rec lamdec_rec l n c = if Int.equal 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 + | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (x,None,t) l) (n-1) c + | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (x,Some b,t) l) (n-1) c | Cast (c,_,_) -> lamdec_rec l n c | c -> error "decompose_lam_n_decls: not enough abstractions" in - lamdec_rec empty_rel_context n + lamdec_rec Context.Rel.empty n let prod_assum t = fst (decompose_prod_assum t) let prod_n_assum n t = fst (decompose_prod_n_assum n t) @@ -678,7 +677,7 @@ let strip_lam_n n t = snd (decompose_lam_n n t) Such a term can canonically be seen as the pair of a context of types and of a sort *) -type arity = rel_context * sorts +type arity = Context.Rel.t * sorts let destArity = let rec prodec_rec l c = -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- kernel/term.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/term.ml') diff --git a/kernel/term.ml b/kernel/term.ml index 33ed25fe1b..ad8ae3be74 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc Suppose that you do not know about rel-context and named-context. (that is the case of people who just started to read the source code) Merlin would tell you that the type of the value you are destructing by "match" is: 'a * 'b option * Constr.t (* worst-case scenario *) or Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *) To me, this is akin to wearing an opaque veil. It is hard to figure out the meaning of the values you are looking at. In particular, it is hard to discover the connection between the value we are destructing above and the datatypes and functions defined in the "kernel/context.ml" file. In this case, the connection is there, but it is not visible (between the function above and the "Context" module). ------------------------------------------------------------------------ Now consider, what happens when the reader see the same function presented in the following form: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc If the reader haven't seen "LocalAssum" before, (s)he can use Merlin to jump to the corresponding definition and learn more. In this case, the connection is there, and it is directly visible (between the function above and the "Context" module). (2) Also, if we already have the concepts such as: - local declaration - local assumption - local definition and we describe these notions meticulously in the Reference Manual, then it is a real pity not to reinforce the connection of the actual code with the abstract description we published. --- kernel/term.ml | 111 ++++++++++++++++++++++++++++++++------------------------- 1 file changed, 63 insertions(+), 48 deletions(-) (limited to 'kernel/term.ml') diff --git a/kernel/term.ml b/kernel/term.ml index 9ba45f5403..4416770fe4 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -383,40 +383,46 @@ let mkNamedLambda id typ c = mkLambda (Name id, typ, subst_var id c) let mkNamedLetIn id c1 t c2 = mkLetIn (Name id, c1, t, subst_var id c2) (* Constructs either [(x:t)c] or [[x=b:t]c] *) -let mkProd_or_LetIn (na,body,t) c = - match body with - | None -> mkProd (na, t, c) - | Some b -> mkLetIn (na, b, t, c) - -let mkNamedProd_or_LetIn (id,body,t) c = - match body with - | None -> mkNamedProd id t c - | Some b -> mkNamedLetIn id b t c +let mkProd_or_LetIn decl c = + let open Context.Rel.Declaration in + match decl with + | LocalAssum (na,t) -> mkProd (na, t, c) + | LocalDef (na,b,t) -> mkLetIn (na, b, t, c) + +let mkNamedProd_or_LetIn decl c = + let open Context.Named.Declaration in + match decl with + | LocalAssum (id,t) -> mkNamedProd id t c + | LocalDef (id,b,t) -> mkNamedLetIn id b t c (* Constructs either [(x:t)c] or [c] where [x] is replaced by [b] *) -let mkProd_wo_LetIn (na,body,t) c = - match body with - | None -> mkProd (na, t, c) - | Some b -> subst1 b c - -let mkNamedProd_wo_LetIn (id,body,t) c = - match body with - | None -> mkNamedProd id t c - | Some b -> subst1 b (subst_var id c) +let mkProd_wo_LetIn decl c = + let open Context.Rel.Declaration in + match decl with + | LocalAssum (na,t) -> mkProd (na, t, c) + | LocalDef (na,b,t) -> subst1 b c + +let mkNamedProd_wo_LetIn decl c = + let open Context.Named.Declaration in + match decl with + | LocalAssum (id,t) -> mkNamedProd id t c + | LocalDef (id,b,t) -> subst1 b (subst_var id c) (* non-dependent product t1 -> t2 *) let mkArrow t1 t2 = mkProd (Anonymous, t1, t2) (* Constructs either [[x:t]c] or [[x=b:t]c] *) -let mkLambda_or_LetIn (na,body,t) c = - match body with - | None -> mkLambda (na, t, c) - | Some b -> mkLetIn (na, b, t, c) - -let mkNamedLambda_or_LetIn (id,body,t) c = - match body with - | None -> mkNamedLambda id t c - | Some b -> mkNamedLetIn id b t c +let mkLambda_or_LetIn decl c = + let open Context.Rel.Declaration in + match decl with + | LocalAssum (na,t) -> mkLambda (na, t, c) + | LocalDef (na,b,t) -> mkLetIn (na, b, t, c) + +let mkNamedLambda_or_LetIn decl c = + let open Context.Named.Declaration in + match decl with + | LocalAssum (id,t) -> mkNamedLambda id t c + | LocalDef (id,b,t) -> mkNamedLetIn id b t c (* prodn n [xn:Tn;..;x1:T1;Gamma] b = (x1:T1)..(xn:Tn)b *) let prodn n env b = @@ -576,10 +582,11 @@ let decompose_lam_n 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 open Context.Rel.Declaration in let rec prodec_rec l c = match kind_of_term c with - | Prod (x,t,c) -> prodec_rec (Context.Rel.add (x,None,t) l) c - | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (x,Some b,t) l) c + | Prod (x,t,c) -> prodec_rec (Context.Rel.add (LocalAssum (x,t)) l) c + | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (LocalDef (x,b,t)) l) c | Cast (c,_,_) -> prodec_rec l c | _ -> l,c in @@ -589,9 +596,10 @@ let decompose_prod_assum = ([(xn,Tn);...;(x1,T1)],T), where T is not a lambda *) let decompose_lam_assum = let rec lamdec_rec l c = + let open Context.Rel.Declaration in match kind_of_term c with - | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (x,None,t) l) c - | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (x,Some b,t) l) c + | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) c + | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) c | Cast (c,_,_) -> lamdec_rec l c | _ -> l,c in @@ -606,11 +614,13 @@ let decompose_prod_n_assum n = error "decompose_prod_n_assum: integer parameter must be positive"; let rec prodec_rec l n c = if Int.equal n 0 then l,c - else match kind_of_term c with - | Prod (x,t,c) -> prodec_rec (Context.Rel.add (x,None,t) l) (n-1) c - | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (x,Some b,t) l) (n-1) c - | Cast (c,_,_) -> prodec_rec l n c - | c -> error "decompose_prod_n_assum: not enough assumptions" + else + let open Context.Rel.Declaration in + match kind_of_term c with + | Prod (x,t,c) -> prodec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c + | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (LocalDef (x,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 Context.Rel.empty n @@ -625,11 +635,13 @@ let decompose_lam_n_assum n = error "decompose_lam_n_assum: integer parameter must be positive"; let rec lamdec_rec l n c = if Int.equal n 0 then l,c - else match kind_of_term c with - | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (x,None,t) l) (n-1) c - | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (x,Some b,t) l) n c - | Cast (c,_,_) -> lamdec_rec l n c - | c -> error "decompose_lam_n_assum: not enough abstractions" + else + let open Context.Rel.Declaration in + match kind_of_term c with + | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c + | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) n c + | Cast (c,_,_) -> lamdec_rec l n c + | c -> error "decompose_lam_n_assum: not enough abstractions" in lamdec_rec Context.Rel.empty n @@ -639,11 +651,13 @@ let decompose_lam_n_decls n = error "decompose_lam_n_decls: integer parameter must be positive"; let rec lamdec_rec l n c = if Int.equal n 0 then l,c - else match kind_of_term c with - | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (x,None,t) l) (n-1) c - | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (x,Some b,t) l) (n-1) c - | Cast (c,_,_) -> lamdec_rec l n c - | c -> error "decompose_lam_n_decls: not enough abstractions" + else + let open Context.Rel.Declaration in + match kind_of_term c with + | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c + | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c + | Cast (c,_,_) -> lamdec_rec l n c + | c -> error "decompose_lam_n_decls: not enough abstractions" in lamdec_rec Context.Rel.empty n @@ -669,10 +683,11 @@ let strip_lam_n n t = snd (decompose_lam_n n t) type arity = Context.Rel.t * sorts let destArity = + let open Context.Rel.Declaration in 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 + | Prod (x,t,c) -> prodec_rec (LocalAssum (x,t) :: l) c + | LetIn (x,b,t,c) -> prodec_rec (LocalDef (x,b,t) :: l) c | Cast (c,_,_) -> prodec_rec l c | Sort s -> l,s | _ -> anomaly ~label:"destArity" (Pp.str "not an arity") -- cgit v1.2.3