123 lines
3.1 KiB
Coq
123 lines
3.1 KiB
Coq
Require Import List.
|
|
Import ListNotations.
|
|
|
|
Inductive hlist {A:Type} (B: A -> Type): list A -> Type :=
|
|
| HNil: hlist _ []
|
|
| HCons: forall (t:A) (ts:list A),
|
|
B t -> hlist _ ts -> hlist _ (t::ts).
|
|
Arguments HNil {A B}.
|
|
Arguments HCons {A B t ts}.
|
|
|
|
Inductive member {A:Type} (elem:A): list A -> Type :=
|
|
| HFirst: forall l:list A, member elem (elem::l)
|
|
| HNext: forall (a:A) (l:list A),
|
|
member elem l -> member elem (a::l).
|
|
|
|
(*
|
|
Fixpoint hget {A:Type} {B:A->Type} {ts:list A}
|
|
(l: hlist B ts) (elem: A): member elem ts -> B elem :=
|
|
match l with
|
|
|
|
|
end.
|
|
*)
|
|
|
|
|
|
(* https://coq-community.org/coq-ext-lib/v0.10.3/ExtLib.Data.HList.html *)
|
|
Definition hhd {A:Type} {t:A} {ts:list A} {B:A -> Type}
|
|
(l: hlist B (t::ts)): B t :=
|
|
match l in hlist _ typs return
|
|
match typs with
|
|
| [] => unit
|
|
| ty::_ => B ty
|
|
end with
|
|
| HNil => tt
|
|
| HCons x xs => x
|
|
end.
|
|
|
|
Definition htl {A:Type} {t:A} {ts:list A} {B:A -> Type}
|
|
(l: hlist B (t::ts)) : hlist B ts :=
|
|
match l in hlist _ typs return
|
|
match typs with
|
|
| [] => unit
|
|
| _::tys => hlist _ tys
|
|
end with
|
|
| HNil => tt
|
|
| HCons x xs => xs
|
|
end.
|
|
|
|
Fixpoint happ {A:Type} {ts1 ts2: list A} {B:A -> Type}
|
|
(l1: hlist B ts1) (l2: hlist B ts2): hlist B (ts1++ts2) :=
|
|
match l1 with
|
|
| HNil => l2
|
|
| HCons x xs => HCons x (happ xs l2)
|
|
end.
|
|
|
|
(*
|
|
Fixpoint hrev {A:Type} {ts: list A} {B:A -> Type}
|
|
(l: hlist B ts): hlist B (rev ts) :=
|
|
match l in hlist _ typs return
|
|
match typs with
|
|
| [] => hlist _ []
|
|
| xs => hlist _ (rev xs)
|
|
end with
|
|
| HNil => HNil
|
|
| HCons x xs =>
|
|
happ (HCons x HNil) xs
|
|
end.
|
|
*)
|
|
|
|
Example eg1 := HCons 3 HNil: hlist (fun x:Set=>x) [nat].
|
|
Example eg2 := HCons 3 (HCons true HNil): hlist (fun x:Set=>x) [nat; bool].
|
|
Example eg3 := HCons (0,3) HNil
|
|
: hlist (fun x:Set=>(x*nat)%type) [nat].
|
|
|
|
Check HCons 0 HNil : hlist (fun x:Type=>x) [nat:Type].
|
|
Fail Check HCons 0 HNil : hlist (fun x:Type=>x) [nat].
|
|
Fail Check HCons 3 (HCons true HNil) : hlist (fun x:Set=>x) [nat; nat].
|
|
|
|
Module HListNotations.
|
|
Declare Scope hlist_scope.
|
|
Delimit Scope hlist_scope with hlist.
|
|
|
|
Notation "« »" := HNil : hlist_scope.
|
|
Notation "« x »" := (HCons x HNil) : hlist_scope.
|
|
Notation "« x ; .. ; y »" := (HCons x .. (HCons y HNil) ..) : hlist_scope.
|
|
Infix "++" := happ: hlist_scope.
|
|
End HListNotations.
|
|
|
|
|
|
Require Import String.
|
|
Open Scope string.
|
|
|
|
Import HListNotations.
|
|
Open Scope hlist.
|
|
|
|
Check «3; true» : hlist (fun x:Set=>x) [nat; bool].
|
|
(* « 3; true » : hlist (fun x : Set => x) [nat; bool] *)
|
|
|
|
Check «» : hlist (fun x:Set=>x) [].
|
|
(* « » : hlist (fun x : Set => x) [] *)
|
|
|
|
Check « "hi" » : hlist (fun x:Set=>x) [string].
|
|
(* « "hi" » : hlist (fun x : Set => x) [string] *)
|
|
|
|
Check «(0,3); (1,true)» : hlist (fun x:Set=>(nat*x)%type) [nat; bool].
|
|
(* « (0, 3); (1, true) » *)
|
|
|
|
Compute hhd eg1.
|
|
(* = 3 : nat *)
|
|
Compute hhd eg3.
|
|
(* = (0, 3) : nat * nat *)
|
|
|
|
Compute htl eg1.
|
|
(* = « » : hlist (fun x : Set => x) [] *)
|
|
Compute htl eg2.
|
|
(* = « true » : hlist (fun x : Set => x) [bool] *)
|
|
|
|
Compute eg1 ++ eg2 ++ eg2.
|
|
(* = « 3; 3; true; 3; true » *)
|
|
|
|
Require Import Extraction.
|
|
Recursive Extraction hlist.
|
|
|