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 +++++++++++++++++++++++-----
 kernel/term.mli | 31 ++++++++++++++++++++-----------
 2 files changed, 43 insertions(+), 16 deletions(-)

(limited to 'kernel')

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 =
diff --git a/kernel/term.mli b/kernel/term.mli
index 501aaf741e..d60716410c 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -281,13 +281,15 @@ val decompose_prod : constr -> (Name.t*constr) list * constr
    {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}, where {% $ %}T{% $ %} is not a lambda. *)
 val decompose_lam : constr -> (Name.t*constr) list * constr
 
-(** Given a positive integer n, transforms a product term
+(** Given a positive integer n, decompose a product term
    {% $ %}(x_1:T_1)..(x_n:T_n)T{% $ %}
-   into the pair {% $ %}([(xn,Tn);...;(x1,T1)],T){% $ %}. *)
+   into the pair {% $ %}([(xn,Tn);...;(x1,T1)],T){% $ %}.
+   Raise a user error if not enough products. *)
 val decompose_prod_n : int -> constr -> (Name.t * constr) list * constr
 
-(** Given a positive integer {% $ %}n{% $ %}, transforms a lambda term
-   {% $ %}[x_1:T_1]..[x_n:T_n]T{% $ %} into the pair {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %} *)
+(** Given a positive integer {% $ %}n{% $ %}, decompose a lambda term
+   {% $ %}[x_1:T_1]..[x_n:T_n]T{% $ %} into the pair {% $ %}([(x_n,T_n);...;(x_1,T_1)],T){% $ %}.
+   Raise a user error if not enough lambdas. *)
 val decompose_lam_n : int -> constr -> (Name.t * constr) list * constr
 
 (** Extract the premisses and the conclusion of a term of the form
@@ -297,10 +299,15 @@ val decompose_prod_assum : types -> rel_context * types
 (** Idem with lambda's *)
 val decompose_lam_assum : constr -> rel_context * constr
 
-(** Idem but extract the first [n] premisses *)
+(** Idem but extract the first [n] premisses, counting let-ins. *)
 val decompose_prod_n_assum : int -> types -> rel_context * types
+
+(** Idem for lambdas, _not_ counting let-ins *)
 val decompose_lam_n_assum : int -> constr -> rel_context * constr
 
+(** Idem, counting let-ins *)
+val decompose_lam_n_decls : int -> constr -> rel_context * constr
+
 (** [nb_lam] {% $ %}[x_1:T_1]...[x_n:T_n]c{% $ %} where {% $ %}c{% $ %} is not an abstraction
    gives {% $ %}n{% $ %} (casts are ignored) *)
 val nb_lam : constr -> int
@@ -308,12 +315,14 @@ val nb_lam : constr -> int
 (** Similar to [nb_lam], but gives the number of products instead *)
 val nb_prod : constr -> int
 
-(** Returns the premisses/parameters of a type/term (let-in included) *)
+(** Return the premisses/parameters of a type/term (let-in included) *)
 val prod_assum : types -> rel_context
 val lam_assum : constr -> rel_context
 
-(** Returns the first n-th premisses/parameters of a type/term (let included)*)
+(** Return the first n-th premisses/parameters of a type (let included and counted) *)
 val prod_n_assum : int -> types -> rel_context
+
+(** Return the first n-th premisses/parameters of a term (let included but not counted) *)
 val lam_n_assum : int -> constr -> rel_context
 
 (** Remove the premisses/parameters of a type/term *)
@@ -328,11 +337,11 @@ val strip_lam_n : int -> constr -> constr
 val strip_prod_assum : types -> types
 val strip_lam_assum : constr -> constr
 
-(** flattens application lists *)
+(** Flattens application lists *)
 val collapse_appl : constr -> constr
 
 
-(** Removes recursively the casts around a term i.e.
+(** Remove recursively the casts around a term i.e.
    [strip_outer_cast (Cast (Cast ... (Cast c, t) ... ))] is [c]. *)
 val strip_outer_cast : constr -> constr
 
@@ -352,10 +361,10 @@ type arity = rel_context * sorts
 (** Build an "arity" from its canonical form *)
 val mkArity : arity -> types
 
-(** Destructs an "arity" into its canonical form *)
+(** Destruct an "arity" into its canonical form *)
 val destArity : types -> arity
 
-(** Tells if a term has the form of an arity *)
+(** Tell if a term has the form of an arity *)
 val isArity : types -> bool
 
 (** {5 Kind of type} *)
-- 
cgit v1.2.3


From c8b57f62f5ad12f8926f57fcdbc5bb2ee3c63eff Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 13 Oct 2015 11:40:22 +0200
Subject: Miscellaneous typos, spacing, US spelling in comments or variable
 names.

---
 kernel/typeops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 09299f31d7..4f32fdce83 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -477,7 +477,7 @@ let rec execute env cstr =
       let j' = execute env1 c3 in
         judge_of_letin env name j1 j2 j'
 
-    | Cast (c,k, t) ->
+    | Cast (c,k,t) ->
       let cj = execute env c in
       let tj = execute_type env t in
         judge_of_cast env cj k tj
-- 
cgit v1.2.3