module Etiquette where
open import Data.Nat
open import Data.String
open import Data.Maybe

open import Data.List
open import Data.List.Any
open Data.List.Any.Membership-≡
open import Level
open import Relation.Binary.PropositionalEquality hiding ([_])
open import Data.Unit
open import Data.Empty
open import Relation.Nullary
open import Relation.Nullary.Decidable
import Relation.Binary.PropositionalEquality as PropEq
open import Data.Bool -- hiding (_∧_ ; _∨_)


open import Data.List.Any.Properties

open import Tree


-- a message: just text and a list of restrictions

Restrictions : Set
Restrictions = List String

data Message : Set where
  message : (text : String) → (restrictions : Restrictions) → Message


-- helpers

∈-sb : String → List String → Bool
∈-sb x [] = false
∈-sb x (x₁ ∷ l) = if (x == x₁) then true else (∈-sb x l)

⊆-sb : List String → List String → Bool
⊆-sb [] l₂ = true
⊆-sb (x ∷ l₁) l₂ = ∈-sb x l₂ ∧ ⊆-sb l₁ l₂


-- message tree

validate-reply : Maybe Message → Message → Bool
validate-reply (just (message _ r₁)) (message _ r₂) = ⊆-sb r₂ r₁
validate-reply nothing _ = true

MessageTree : Set
MessageTree = Tree Message validate-reply nothing

MessageForest : Restrictions → Set
MessageForest r = Forest Message validate-reply (message "" r)

user-view-property : Restrictions → Maybe Message → Message → Bool
user-view-property u (just (message t₁ r₁)) (message t₂ r₂) = (⊆-sb u r₂) ∧ (⊆-sb r₂ r₁)
user-view-property u nothing (message t₂ r₂) = ⊆-sb u r₂

MessageTreeView : Restrictions → Set
MessageTreeView user-restrictions = Tree Message (user-view-property user-restrictions) nothing

MessageForestView : Restrictions → Restrictions → Set
MessageForestView gr ur = Forest Message (user-view-property ur) (message "" gr)


-- cutting a forest of message trees, to satisfy given restrictions

view : {i u : Restrictions} → MessageForest i → MessageForestView i u
view = forest-cut

Generated at Sat Apr 12 02:14:35 2014 (original)