# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1483325457 0
# Node ID 35ea84d3507978fa3b7d46161ed1f403a40d81b1
# Parent  5af5f1a930bc1d5e9e549a2e049e77eb19471dae
Trying Set with constraint...

diff -r 5af5f1a930bc -r 35ea84d35079 sandbox/SetWithConstraint.agda
--- a/sandbox/SetWithConstraint.agda	Sun Jan 01 04:36:02 2017 +0000
+++ b/sandbox/SetWithConstraint.agda	Mon Jan 02 02:50:57 2017 +0000
@@ -1,30 +1,57 @@
 module SetWithConstraint where
 
-open import Relation.Binary
-open import Relation.Binary.PropositionalEquality
-open import Function
+open import Data.Nat
 open import Data.Bool
-open import Data.Nat
-open import Data.Nat.Properties
-open import Data.List
 open import Data.Product
-open import Data.AVL 
-open import Data.AVL.Sets (Relation.Binary.StrictTotalOrder.isStrictTotalOrder Data.Nat.Properties.strictTotalOrder) as S
+open import Data.String
+open import Relation.Binary.PropositionalEquality
+open import Data.Empty
+open import Data.Maybe
 
-yo : ⟨Set⟩
-yo = S.empty
+
+data MySet (A : Set) : Set where
+  empty : MySet A
+  cons  : (String × A) -> MySet A -> MySet A
 
-empty-set : (length (S.toList  S.empty)) ≡ zero
-empty-set  = refl
+insert : {A : Set} -> (String × A) -> MySet A -> MySet A
+insert (k , v) empty        = cons (k , v) empty
+insert (k , v) (cons (sk , sv) s) with (k == sk)
+...                                  | true  = cons (sk , sv) s
+...                                  | false = cons (sk , sv) (insert (k , v) s)
+       
+length : {A : Set} -> MySet A -> ℕ
+length empty      = 0
+length (cons _ s) = suc (length s)
 
-empty-set+1 : length (S.toList (S.insert 100 S.empty)) ≡ 1
-empty-set+1 = refl
+elem : {A : Set} -> String -> MySet A -> Bool
+elem a empty      = false
+elem a (cons (k , v) s) with a == k
+...                      | true  = true
+...                      | false = elem a s
+
+head : {A : Set} -> MySet A -> Maybe (String × A)
+head empty      = nothing
+head (cons x _) = just x
+
+
+
+empty-length : {A : Set} -> (length {A} empty) ≡ 0
+empty-length = refl
+
+empty-insert-length : (s : MySet ℕ) -> length (insert ("a" , 100) empty) ≡ 1
+empty-insert-length s = refl
 
 open ≡-Reasoning
 
-non-empty-set+1 : (a : ℕ ) (s : ⟨Set⟩) {notElem : (a S.∈? s) ≡ false} -> length (S.toList (S.insert a s)) ≡ suc (length (S.toList s))
-non-empty-set+1 a (tree (Indexed.leaf l<u))         = refl
-non-empty-set+1 a (tree (Indexed.node (proj₃ , proj₄) x x₁ Height-invariants.∼+)) = {!!}
-non-empty-set+1 a (tree (Indexed.node (proj₃ , proj₄) x x₁ Height-invariants.∼0)) = {!!}
-non-empty-set+1 a (tree (Indexed.node (proj₃ , proj₄) x x₁ Height-invariants.∼-)) = {!!}
+expand-non-elem : (k : String) (s : MySet ℕ) -> (nonElem : elem k s ≡ false) -> (just k ≢ (Data.Maybe.map proj₁ (head s)))
+expand-non-elem k empty nonElem      = {!!}
+expand-non-elem k (cons x s) nonElem = {!!}
+
 
+insert-length : (k : String) (n : ℕ )(s : MySet ℕ) {nonElem : elem k s ≡ false} -> length (insert (k , n) s) ≡ suc (length s)
+insert-length k n empty              = refl
+insert-length k n (cons (ks , vs) s) {nonElem} = begin
+  length (insert (k , n) (cons (ks , vs) s))
+  ≡⟨ {!!} ⟩
+  suc (suc (length s))
+  ∎