michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

directory cleanup

Browse source
This commit is contained in:
wadler 2018-05-19 07:03:08 -03:00
parent eba540bbc5
commit 977b94ba2c
4 changed files with 37 additions and 74 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

0
src/TypedDB.lagda → src/DeBruijn.lagda
View file

43
src/TakeDropDec.agda
View file

@ -1,43 +0,0 @@
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.List using (List; []; _∷_)
open import Data.List.All using (All; []; _∷_)
open import Data.Bool using (Bool; true; false; T)
open import Data.Unit using (⊤; tt)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Nullary.Decidable using ()
open import Function using (_∘_)
module TakeDropDec2 {A : Set} {P : A → Set} (P? : ∀ (x : A) → Dec (P x)) where
takeWhile : List A → List A
takeWhile [] = []
takeWhile (x ∷ xs) with P? x
... | yes _ = x ∷ takeWhile xs
... | no _ = []
dropWhile : List A → List A
dropWhile [] = []
dropWhile (x ∷ xs) with P? x
... | yes _ = dropWhile xs
... | no _ = x ∷ xs
Head : (A → Set) → List A → Set
Head P [] = ⊥
Head P (x ∷ xs) = P x
takeWhile-lemma : ∀ (xs : List A) → All P (takeWhile xs)
takeWhile-lemma [] = []
takeWhile-lemma (x ∷ xs) with P? x
... | yes px = px ∷ takeWhile-lemma xs
... | no _ = []
dropWhile-lemma : ∀ (xs : List A) → ¬ Head P (dropWhile xs)
dropWhile-lemma [] = λ()
dropWhile-lemma (x ∷ xs) with P? x
... | yes _ = dropWhile-lemma xs
... | no ¬px = ¬px

5
src/TakeDropDecTest.agda
View file

@ -5,10 +5,5 @@ open import Data.List using (List; []; _∷_)
open import Relation.Nullary using (Dec; yes; no)
open import TakeDropDec2
_ : takeWhile (0 ≟_) (0 ∷ 0 ∷ 1 ∷ []) ≡ (0 ∷ 0 ∷ [])
_ = refl
_ : dropWhile (0 ≟_) (0 ∷ 0 ∷ 1 ∷ []) ≡ (1 ∷ [])
_ = refl

63
src/extra/TakeDropDec.agda
View file

@ -1,3 +1,5 @@
module TakeDropDec where
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_)
open import Data.Empty using (⊥; ⊥-elim)
@ -9,35 +11,44 @@ open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Nullary.Decidable using ()
open import Function using (_∘_)
module TakeDropDec {A : Set} {P : A → Set} where
module TakeDrop {A : Set} {P : A → Set} (P? : ∀ (x : A) → Dec (P x)) where
Decidable : (A → Set) → Set
Decidable P = ∀ (x : A) → Dec (P x)
takeWhile : List A → List A
takeWhile [] = []
takeWhile (x ∷ xs) with P? x
... | yes _ = x ∷ takeWhile xs
... | no _ = []
takeWhile : Decidable P → List A → List A
takeWhile P? [] = []
takeWhile P? (x ∷ xs) with P? x
... | yes _ = x ∷ takeWhile P? xs
... | no _ = []
dropWhile : List A → List A
dropWhile [] = []
dropWhile (x ∷ xs) with P? x
... | yes _ = dropWhile xs
... | no _ = x ∷ xs
dropWhile : Decidable P → List A → List A
dropWhile P? [] = []
dropWhile P? (x ∷ xs) with P? x
... | yes _ = dropWhile P? xs
... | no _ = x ∷ xs
Head : (A → Set) → List A → Set
Head P [] = ⊥
Head P (x ∷ xs) = P x
takeWhile-lemma : ∀ (xs : List A) → All P (takeWhile xs)
takeWhile-lemma [] = []
takeWhile-lemma (x ∷ xs) with P? x
... | yes px = px ∷ takeWhile-lemma xs
... | no _ = []
dropWhile-lemma : ∀ (xs : List A) → ¬ Head P (dropWhile xs)
dropWhile-lemma [] = λ()
dropWhile-lemma (x ∷ xs) with P? x
... | yes _ = dropWhile-lemma xs
... | no ¬px = ¬px
open TakeDrop
open import Data.Nat using (ℕ; zero; suc; _≟_)
_ : takeWhile (0 ≟_) (0 ∷ 0 ∷ 1 ∷ []) ≡ (0 ∷ 0 ∷ [])
_ = refl
_ : dropWhile (0 ≟_) (0 ∷ 0 ∷ 1 ∷ []) ≡ (1 ∷ [])
_ = refl
Head : (A → Set) → List A → Set
Head P [] = ⊥
Head P (x ∷ xs) = P x
takeWhile-lemma : ∀ (P? : Decidable P) (xs : List A) → All P (takeWhile P? xs)
takeWhile-lemma P? [] = []
takeWhile-lemma P? (x ∷ xs) with P? x
... | yes px = px ∷ takeWhile-lemma P? xs
... | no _ = []
dropWhile-lemma : ∀ (P? : Decidable P) (xs : List A) → ¬ Head P (dropWhile P? xs)
dropWhile-lemma P? [] = λ()
dropWhile-lemma P? (x ∷ xs) with P? x
... | yes _ = dropWhile-lemma P? xs
... | no ¬px = ¬px