Bask in the glory of simplification

larrytheliquid · Mar 13, 2010 · 867dc76 · 867dc76
1 parent 91f4c52
commit 867dc76
Show file tree

Hide file tree

Showing 3 changed files with 19 additions and 20 deletions.
diff --git a/Lemmachine/Lemmas.agda b/Lemmachine/Lemmas.agda
@@ -1,6 +1,7 @@
 open import Lemmachine
 module Lemmachine.Lemmas (properties : Properties) where
 open import Lemmachine.Resource.Configure
+open import Data.Empty
 open import Data.String
 open import Data.Maybe
 open import Data.Function
@@ -49,6 +50,18 @@ methodIsAllowed : ∀ res req → Request.method req ∈ Resource.allowedMethods
                                   (Resource.allowedMethods res req) ≡ true
 methodIsAllowed res req p = methodIsMember req (Resource.allowedMethods res req) p
 
+notOptions : ∀ r → Request.method r ≢ OPTIONS
+                 → eqMethod (Request.method r) OPTIONS ≡ false
+notOptions r p with Request.method r
+... | HEAD = refl
+... | GET = refl
+... | PUT = refl
+... | DELETE = refl
+... | POST = refl
+... | TRACE = refl
+... | CONNECT = refl
+... | OPTIONS = ⊥-elim (p refl)
+
 private
   ==-refl : ∀ s → (s == s) ≡ true
   ==-refl s = trustMe

diff --git a/Lemmachine/Proofs.agda b/Lemmachine/Proofs.agda
@@ -76,30 +76,16 @@ optionsOK : ∀ r → Request.method r ∈ Resource.knownMethods resource r
 optionsOK r p p₂ p₃ with methodIsKnown resource r p | methodIsAllowed resource r p₂
 ... | p₄ | p₅ rewrite p₄ | p₅ | p₃ = refl
 
--- TODO: methodNotOptions like p₅
 notAcceptableResource = stub [ contentTypesProvided ⇒ const [] ]
 notAcceptable : ∀ r → Request.method r ∈ Resource.knownMethods notAcceptableResource r
                     → Request.method r ∈ Resource.allowedMethods notAcceptableResource r
                     → Request.method r ≢ OPTIONS
                     → "Accept" ∈ map proj₁ (Request.headers r)
                     → resolve notAcceptableResource r ≡ NotAcceptable
-notAcceptable r p p₂ p₃ p₄ with methodIsKnown notAcceptableResource r p | methodIsAllowed notAcceptableResource r p₂ | acceptIsHeader r p₄
-notAcceptable r _ _ _ _ | p₅ | p₆ | v , p₇ rewrite p₅ | p₆ with Request.method r
-notAcceptable r _ _ _ _ | _ | _ | _ , p₇ | HEAD with fetch "Accept" (Request.headers r) | p₇
+notAcceptable r p p₂ p₃ p₄ with methodIsKnown notAcceptableResource r p | methodIsAllowed notAcceptableResource r p₂
+                              | acceptIsHeader r p₄ | notOptions r p₃
+notAcceptable r _ _ p₃ _ | p₅ | p₆ | v , p₇ | p₈ rewrite p₅ | p₆ | p₈ with fetch "Accept" (Request.headers r) | p₇
 ... | ._ | refl = refl
-notAcceptable r _ _ _ _ | _ | _ | _ , p₇ | GET with fetch "Accept" (Request.headers r) | p₇
-... | ._ | refl = refl
-notAcceptable r _ _ _ _ | _ | _ | _ , p₇ | PUT with fetch "Accept" (Request.headers r) | p₇
-... | ._ | refl = refl
-notAcceptable r _ _ _ _ | _ | _ | _ , p₇ | DELETE with fetch "Accept" (Request.headers r) | p₇
-... | ._ | refl = refl
-notAcceptable r _ _ _ _ | _ | _ | _ , p₇ | POST with fetch "Accept" (Request.headers r) | p₇
-... | ._ | refl = refl
-notAcceptable r _ _ _ _ | _ | _ | _ , p₇ | TRACE with fetch "Accept" (Request.headers r) | p₇
-... | ._ | refl = refl
-notAcceptable r _ _ _ _ | _ | _ | _ , p₇ | CONNECT with fetch "Accept" (Request.headers r) | p₇
-... | ._ | refl = refl
-notAcceptable r _ _ p₃ _ | _ | _ | _ , _ | OPTIONS = ⊥-elim (p₃ refl)
 
 preconditionFailed : ∀ r → fetch "If-Match" (Request.headers r) ≡ just "*"
                          → H7 (stub []) r ≡ PreconditionFailed

diff --git a/Lemmachine/Resolve.agda b/Lemmachine/Resolve.agda
@@ -169,9 +169,9 @@ C3+C4 r with fetch "Accept" (Request.headers r)
 ... | nothing = NotAcceptable
 
 B3 : Request → Status
-B3 r with Request.method r
-... | OPTIONS = OK
-... | _       = C3+C4 r
+B3 r with eqMethod (Request.method r) OPTIONS
+... | true  = OK
+... | false = C3+C4 r
 
 B4 : Request → Status
 B4 r with Resource.validEntityLength c r