diff options
author | Jason Gross <jgross@mit.edu> | 2016-11-01 16:41:59 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-11-01 16:41:59 -0400 |
commit | cca0eb7decb313fc22865881c6923d7e48258c69 (patch) | |
tree | 3ced916f6762daefea7820c527e96668b0c683dd /src | |
parent | 0a9d86b63f93254271f4ff9ca41df5c04af2cdef (diff) |
Move hlist to new file
Diffstat (limited to 'src')
-rw-r--r-- | src/Util/HList.v | 33 | ||||
-rw-r--r-- | src/Util/Tuple.v | 13 |
2 files changed, 33 insertions, 13 deletions
diff --git a/src/Util/HList.v b/src/Util/HList.v new file mode 100644 index 000000000..addb0e40d --- /dev/null +++ b/src/Util/HList.v @@ -0,0 +1,33 @@ +Require Import Coq.Classes.Morphisms. +Require Import Coq.Relations.Relation_Definitions. +Require Import Coq.Lists.List. +Require Import Crypto.Util.Decidable. +Require Import Crypto.Util.ListUtil. +Require Import Crypto.Util.Tuple. +Require Export Crypto.Util.FixCoqMistakes. + +Fixpoint hlist' T n (f : T -> Type) : tuple' T n -> Type := + match n return tuple' _ n -> Type with + | 0 => fun T => f T + | S n' => fun Ts => (hlist' T n' f (fst Ts) * f (snd Ts))%type + end. +Global Arguments hlist' {T n} f _. + +Definition hlist {T n} (f : T -> Type) : forall (Ts : tuple T n), Type := + match n return tuple _ n -> Type with + | 0 => fun _ => unit + | S n' => @hlist' T n' f + end. + +(* tuple map *) +Fixpoint mapt' {n A F B} (f : forall x : A, F x -> B) : forall ts : tuple' A n, hlist' F ts -> tuple' B n + := match n return forall ts : tuple' A n, hlist' F ts -> tuple' B n with + | 0 => fun ts v => f _ v + | S n' => fun ts v => (@mapt' n' A F B f _ (fst v), f _ (snd v)) + end. +Definition mapt {n A F B} (f : forall x : A, F x -> B) + : forall ts : tuple A n, hlist F ts -> tuple B n + := match n return forall ts : tuple A n, hlist F ts -> tuple B n with + | 0 => fun ts v => tt + | S n' => @mapt' n' A F B f + end. diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v index 65f1f868e..2e9f7b0ad 100644 --- a/src/Util/Tuple.v +++ b/src/Util/Tuple.v @@ -17,19 +17,6 @@ Definition tuple T n : Type := | S n' => tuple' T n' end. -Fixpoint hlist' T n (f : T -> Type) : tuple' T n -> Type := - match n return tuple' _ n -> Type with - | 0 => fun T => f T - | S n' => fun Ts => (hlist' T n' f (fst Ts) * f (snd Ts))%type - end. -Global Arguments hlist' {T n} f _. - -Definition hlist {T n} (f : T -> Type) : forall (Ts : tuple T n), Type := - match n return tuple _ n -> Type with - | 0 => fun _ => unit - | S n' => @hlist' T n' f - end. - Fixpoint to_list' {T} (n:nat) {struct n} : tuple' T n -> list T := match n with | 0 => fun x => (x::nil)%list |