diff options
Diffstat (limited to 'theories/Numbers/NaryFunctions.v')
| -rw-r--r-- | theories/Numbers/NaryFunctions.v | 70 |
1 files changed, 35 insertions, 35 deletions
diff --git a/theories/Numbers/NaryFunctions.v b/theories/Numbers/NaryFunctions.v index 04a48d51..417463eb 100644 --- a/theories/Numbers/NaryFunctions.v +++ b/theories/Numbers/NaryFunctions.v @@ -8,27 +8,27 @@ (* Pierre Letouzey, Jerome Vouillon, PPS, Paris 7, 2008 *) (************************************************************************) -(*i $Id: NaryFunctions.v 10967 2008-05-22 12:59:38Z letouzey $ i*) +(*i $Id$ i*) -Open Local Scope type_scope. +Local Open Scope type_scope. Require Import List. (** * Generic dependently-typed operators about [n]-ary functions *) -(** The type of [n]-ary function: [nfun A n B] is +(** The type of [n]-ary function: [nfun A n B] is [A -> ... -> A -> B] with [n] occurences of [A] in this type. *) -Fixpoint nfun A n B := +Fixpoint nfun A n B := match n with - | O => B + | O => B | S n => A -> (nfun A n B) - end. + end. Notation " A ^^ n --> B " := (nfun A n B) (at level 50, n at next level) : type_scope. -(** [napply_cst _ _ a n f] iterates [n] times the application of a +(** [napply_cst _ _ a n f] iterates [n] times the application of a particular constant [a] to the [n]-ary function [f]. *) Fixpoint napply_cst (A B:Type)(a:A) n : (A^^n-->B) -> B := @@ -40,47 +40,47 @@ Fixpoint napply_cst (A B:Type)(a:A) n : (A^^n-->B) -> B := (** A generic transformation from an n-ary function to another one.*) -Fixpoint nfun_to_nfun (A B C:Type)(f:B -> C) n : +Fixpoint nfun_to_nfun (A B C:Type)(f:B -> C) n : (A^^n-->B) -> (A^^n-->C) := - match n return (A^^n-->B) -> (A^^n-->C) with + match n return (A^^n-->B) -> (A^^n-->C) with | O => f | S n => fun g a => nfun_to_nfun _ _ _ f n (g a) end. -(** [napply_except_last _ _ n f] expects [n] arguments of type [A], - applies [n-1] of them to [f] and discard the last one. *) +(** [napply_except_last _ _ n f] expects [n] arguments of type [A], + applies [n-1] of them to [f] and discard the last one. *) -Definition napply_except_last (A B:Type) := +Definition napply_except_last (A B:Type) := nfun_to_nfun A B (A->B) (fun b a => b). -(** [napply_then_last _ _ a n f] expects [n] arguments of type [A], - applies them to [f] and then apply [a] to the result. *) +(** [napply_then_last _ _ a n f] expects [n] arguments of type [A], + applies them to [f] and then apply [a] to the result. *) -Definition napply_then_last (A B:Type)(a:A) := +Definition napply_then_last (A B:Type)(a:A) := nfun_to_nfun A (A->B) B (fun fab => fab a). -(** [napply_discard _ b n] expects [n] arguments, discards then, +(** [napply_discard _ b n] expects [n] arguments, discards then, and returns [b]. *) Fixpoint napply_discard (A B:Type)(b:B) n : A^^n-->B := - match n return A^^n-->B with + match n return A^^n-->B with | O => b | S n => fun _ => napply_discard _ _ b n end. (** A fold function *) -Fixpoint nfold A B (f:A->B->B)(b:B) n : (A^^n-->B) := - match n return (A^^n-->B) with +Fixpoint nfold A B (f:A->B->B)(b:B) n : (A^^n-->B) := + match n return (A^^n-->B) with | O => b | S n => fun a => (nfold _ _ f (f a b) n) end. -(** [n]-ary products : [nprod A n] is [A*...*A*unit], +(** [n]-ary products : [nprod A n] is [A*...*A*unit], with [n] occurrences of [A] in this type. *) -Fixpoint nprod A n : Type := match n with +Fixpoint nprod A n : Type := match n with | O => unit | S n => (A * nprod A n)%type end. @@ -89,54 +89,54 @@ Notation "A ^ n" := (nprod A n) : type_scope. (** [n]-ary curryfication / uncurryfication *) -Fixpoint ncurry (A B:Type) n : (A^n -> B) -> (A^^n-->B) := - match n return (A^n -> B) -> (A^^n-->B) with +Fixpoint ncurry (A B:Type) n : (A^n -> B) -> (A^^n-->B) := + match n return (A^n -> B) -> (A^^n-->B) with | O => fun x => x tt | S n => fun f a => ncurry _ _ n (fun p => f (a,p)) end. -Fixpoint nuncurry (A B:Type) n : (A^^n-->B) -> (A^n -> B) := +Fixpoint nuncurry (A B:Type) n : (A^^n-->B) -> (A^n -> B) := match n return (A^^n-->B) -> (A^n -> B) with | O => fun x _ => x | S n => fun f p => let (x,p) := p in nuncurry _ _ n (f x) p end. -(** Earlier functions can also be defined via [ncurry/nuncurry]. +(** Earlier functions can also be defined via [ncurry/nuncurry]. For instance : *) Definition nfun_to_nfun_bis A B C (f:B->C) n : - (A^^n-->B) -> (A^^n-->C) := + (A^^n-->B) -> (A^^n-->C) := fun anb => ncurry _ _ n (fun an => f ((nuncurry _ _ n anb) an)). -(** We can also us it to obtain another [fold] function, +(** We can also us it to obtain another [fold] function, equivalent to the previous one, but with a nicer expansion (see for instance Int31.iszero). *) -Fixpoint nfold_bis A B (f:A->B->B)(b:B) n : (A^^n-->B) := - match n return (A^^n-->B) with +Fixpoint nfold_bis A B (f:A->B->B)(b:B) n : (A^^n-->B) := + match n return (A^^n-->B) with | O => b - | S n => fun a => + | S n => fun a => nfun_to_nfun_bis _ _ _ (f a) n (nfold_bis _ _ f b n) end. (** From [nprod] to [list] *) -Fixpoint nprod_to_list (A:Type) n : A^n -> list A := - match n with +Fixpoint nprod_to_list (A:Type) n : A^n -> list A := + match n with | O => fun _ => nil | S n => fun p => let (x,p) := p in x::(nprod_to_list _ n p) end. (** From [list] to [nprod] *) -Fixpoint nprod_of_list (A:Type)(l:list A) : A^(length l) := - match l return A^(length l) with +Fixpoint nprod_of_list (A:Type)(l:list A) : A^(length l) := + match l return A^(length l) with | nil => tt | x::l => (x, nprod_of_list _ l) end. (** This gives an additional way to write the fold *) -Definition nfold_list (A B:Type)(f:A->B->B)(b:B) n : (A^^n-->B) := +Definition nfold_list (A B:Type)(f:A->B->B)(b:B) n : (A^^n-->B) := ncurry _ _ n (fun p => fold_right f b (nprod_to_list _ _ p)). |