Permalink
Browse files

little wips

  • Loading branch information...
larrytheliquid committed Aug 12, 2010
1 parent b5937e0 commit a9c5f1aac5b61e0008462cb3e0b53c7d7460a577
Showing with 104 additions and 0 deletions.
  1. +38 −0 src/Parser.agda
  2. +34 −0 src/Sneaky.agda
  3. +32 −0 src/Tinker.agda
View
@@ -0,0 +1,38 @@
+module Parser where
+open import Data.Unit
+open import Data.Empty
+open import Data.Char
+open import Data.Sum
+open import Data.Product
+
+data U : Set where
+
+mutual
+ data Format : Set where
+ Bad End : Format
+ Base : U Format
+ Plus Skip : Format Format Format
+ Read : (f : Format) (⟦ f ⟧ Format) Format
+
+ ⟦_⟧ : Format Set
+ ⟦ Bad ⟧ =
+ ⟦ End ⟧ =
+ ⟦ Base u ⟧ =
+ ⟦ Plus f₁ f₂ ⟧ = ⟦ f₁ ⟧ ⊎ ⟦ f₂ ⟧
+ ⟦ Skip _ f ⟧ = ⟦ f ⟧
+ ⟦ Read f₁ f₂ ⟧ = Σ ⟦ f₁ ⟧ λ x ⟦ f₂ x ⟧
+
+-- http://tools.ietf.org/html/rfc2616#section-2.2
+
+OCTET = any-US-ASCII "8-bit sequence of data" 0 255
+CHAR = any-US-ASCII "character" 0 127
+UPALPHA = any-US-ASCII "uppercase letter" 'A' 'Z'
+LOALPHA = any-US-ASCII "lowercase letter" 'a' 'z'
+ALPHA = UPALPHA ∣ LOALPHA
+DIGIT = any-US-ASCII "digit" '0' '9'
+CTL = any-US-ASCII "control character" 0 31 ∣ US-ASCII "DEL" 127
+CR = US-ASCII "carriage return" 13
+LF = US-ASCII "linefeed" 10
+SP = US-ASCII "space" 32
+HT = US-ASCII "horizontal-tab" 9
+DQ = US-ASCII "double-quote mark" 34
View
@@ -0,0 +1,34 @@
+module Sneaky where
+open import Data.Bool
+open import Data.Nat
+open import Data.List
+open import Data.Vec
+
+data BoolPair : Set where
+ _,_ : Bool Bool BoolPair
+
+data NatPair : Set where
+ _a,_ : NatPair
+
+-- El : Bool → Set
+-- El true = BoolPair
+-- El false = NatPair
+
+-- Hmz : {b : Bool} → Set
+-- Hmz {b} = El b
+
+-- testing : Hmz
+-- testing = 0 a, 1
+
+El : Bool Set
+El true = List ℕ
+El false = (n : ℕ) Vec Bool n
+
+Hmz : {b : Bool} Set
+Hmz {b} = El b
+
+testing : Hmz {true}
+testing = 012 ∷ []
+
+test : (El false)
+test n = true ∷ false ∷ []
View
@@ -0,0 +1,32 @@
+module Tinker where
+open import Data.String
+open import Data.Nat
+open import Data.Product
+open import Data.Sum
+open import Data.Vec
+
+data METHOD : Set where
+ OPTIONS HEAD : METHOD
+
+data Req : Set where
+ Method Accept Content-Length : Req
+
+Req-El : Req Set
+Req-El Content-Length = ℕ ⊎ ((n : ℕ) Vec String n)
+Req-El _ = String
+
+-- Request = Σ Req Req-El
+
+data Resp : Set where
+ Transfer-Encoding : Resp
+
+ Content-Type : Resp
+ Content-Length : Resp
+
+ message-body : Resp
+
+-- Resp-El : Req-El Accept → Resp → Set
+-- Resp-El _ Content-Type = String
+
+-- Reponse = Σ Resp Resp-El
+

0 comments on commit a9c5f1a

Please sign in to comment.