[Agda] Agda features/functionality that I can use

[Sivaram Gowkanapalli]

 Hello,

I am trying to write an agda program (mySolution.agda) for the "Escape From Zurg: An Exercise in Logic Programming" ( http://web.engr.oregonstate.edu/~erwig/zurg/ ).

This program lists all the possible options, after figuring out how to use the "<" (less-than) in agda.

Can you please let me know what agda functionality / features I can add to make this program better?

Thanks a lot


module mySolution where

open import Data.List --   using (List; []; _:_)
open import Data.Nat  --   using (ℕ)
open import Data.Tuple
open import Data.Bool
open import Data.Maybe
open import Function

data Toy : Set where
   Buzz   Woody   Rex   Hamm : Toy

time : Toy → ℕ
time Buzz   = 5
time Woody  = 10
time Rex    = 20
time Hamm   = 25

allToys : List Toy
allToys = Buzz ∷ Woody ∷ Rex ∷ Hamm ∷ []

LeftToys : Set
LeftToys = List Toy

RightToys : Set
RightToys = List Toy

FirstToy : Set
FirstToy = Toy
SecondToy : Set
SecondToy = Toy

mutual
   Backwards : Set
   Backwards = List (Maybe Tree)
   Forwards : Set
   Forwards = List (Maybe Tree)
   data Tree : Set where
      treeForward : FirstToy    → SecondToy
                    → LeftToys  → RightToys
                    → Backwards → Tree
      treeBackward : Toy
                     → LeftToys  → RightToys
                     → Forwards → Tree
{-
record Forward : Set where
   field firstToy  : Toy
         secondToy : Toy
         leftToys  : LeftToys
         rightToys : RightToys
         nextBackwardSteps : List BackwardTree
record Backward : Set where
   field toy       : Toy
         leftToys  : LeftToys
         rightToys : RightToys
         nextForwardSteps : List ForwardTree
mutual
   data Forward (FirstToy : Toy) (SecondToy : Toy)
                (LeftToys : Set) (RightToys : Set)
                (Backwards : List Tree)
            : Set where
      forward : FirstToy   → SecondToy
                → LeftToys → RightToys
                → Backwards
                → Forward FirstToy SecondToy
                          LeftToys RightToys
                          Backwards
   data Backward (Toy : Set)
                 (LeftToys : Set) (RightToys : Set)
            : Set where
      backward : Toy
                 → LeftToys → RightToys
                 → Forwards
                 → Backward Toy
                            LeftToys RightToys
                            Forwards
-}
{-
mutual
   Backwards : Set
   Backwards = List Backward
   Forwards : Set
   Forwards = List Forward
   data Forward (FirstToy : Toy) (SecondToy : Toy)
                (LeftToys : Set) (RightToys : Set)
                (Backwards : Set)
            : Set where
      forward : FirstToy   → SecondToy
                → LeftToys → RightToys
                → Backwards
                → Forward FirstToy SecondToy
                          LeftToys RightToys
                          Backwards
   data Backward (Toy : Set)
                 (LeftToys : Set) (RightToys : Set)
            : Set where
      backward : Toy
                 → LeftToys → RightToys
                 → Forwards
                 → Backward Toy
                            LeftToys RightToys
                            Forwards
-}

-- subsets of size k
combinationsOf : ℕ → List Toy → List (List Toy)
combinationsOf 0 _   = [ [] ]
combinationsOf _ []  = []
combinationsOf k (x ∷ xs) = map (_∷_ x) (combinationsOf (k ∸ 1) xs)
                            ++ combinationsOf k xs

toTuple : List Toy → Maybe (Toy × Toy)
toTuple (x ∷ y ∷ []) = just (tuple x y)
toTuple _ = nothing -- error "unknown combination"

_==_ : Toy → Toy → Bool
Buzz  == Buzz  = true
Woody == Woody = true
Rex   == Rex   = true
Hamm  == Hamm  = true
_     == _     = false

delete : Toy → List Toy → List Toy
delete toy toys = filter (λ a → not (a == toy)) toys

--fromJust : List (Maybe Toy) → List Toy
--fromJust xs = filter (λ a → not $ maybeToBool a) xs

mutual
   buildTree : LeftToys → RightToys → Maybe (Toy × Toy) → Maybe Tree
   buildTree (_ ∷ _ ∷ []) right (just (tuple firstToy secondToy))
      = just  (treeForward firstToy secondToy
                           -- toys on the left
                           []
                           -- toys on the right
                           (firstToy ∷ secondToy ∷ right)
                           -- child trees
                           [])
   buildTree left right (just (tuple firstToy secondToy))
      = just  (treeForward firstToy secondToy
                           -- toys on the left
                           lefttoys
                           -- toys on the right
                           righttoys
                           -- child trees
                           --(fromJust ∘ map (backwardMoves
                           (map (backwardMoves
                                             lefttoys
                                             righttoys)
                                     $ righttoys))
      where lefttoys  = delete firstToy ∘ delete secondToy $ left
            righttoys = firstToy ∷ secondToy ∷ right
   buildTree _ _ _ = nothing

   backwardMoves : LeftToys → RightToys → Toy → Maybe Tree
   backwardMoves left right backward
      = just  (treeBackward backward -- Backward
                            -- toys on the left
                            lefttoys
                            -- toys on the right
                            (delete backward right)
                            -- child trees
                            --(fromJust ∘ map (buildTree
                            (map (buildTree lefttoys righttoys
                                  ∘ toTuple)
                             ∘ combinationsOf 2
                             $ lefttoys))
      where lefttoys = backward ∷ left
            righttoys = (delete backward right)

allOptions : List (Maybe Tree)
allOptions = map (buildTree allToys [] ∘ toTuple)
                 ∘ combinationsOf 2 $ allToys

data Move : Set where
   moveF : FirstToy → SecondToy → Move
   moveB : Toy → Move

Choice : Set
Choice = List Move

mutual
   treesToChoices : List (Maybe Tree) → List Choice
   treesToChoices trees = concatMap treeToChoices trees

   treeToChoices : Maybe Tree → List Choice
   treeToChoices (just (treeForward x y [] _ []))
      = (((moveF x y) ∷ [] ) ∷ [])
   treeToChoices (just (treeForward x y _ _ nextSteps))
      = map (_∷_ (moveF x y)) $ treesToChoices nextSteps
   treeToChoices (just (treeBackward x _ _ nextSteps))
      = map (_∷_ (moveB x)) $ treesToChoices nextSteps
   treeToChoices (nothing) = (([]) ∷ [])

Cost : Set
Cost = ℕ

moveCost : Move → Cost
moveCost (moveF x y) = (time x) ⊔ (time y)
moveCost (moveB x) = time x

costOfChoice : Choice → (Cost × Choice)
costOfChoice choice = tuple (sum ∘ map moveCost $ choice) choice

costOfChoices : List Choice → List (Cost × Choice)
costOfChoices = map costOfChoice

lessThan : ℕ → ℕ → Bool
lessThan zero (suc y)    = true
lessThan (suc x) zero    = false
lessThan zero zero       = false
lessThan (suc x) (suc y) = lessThan x y

solution : List (Cost × Choice)
solution = filter (λ x → lessThan (fst x) 61)
           ∘ costOfChoices ∘ treesToChoices $ allOptions

{-
main : IO Unit
--main = putStrLn ∘ groom ∘ filter (λ (cost , _) → cost < 61)
main = putStrLn ∘ filter (λ < cost , _ > → cost < 61)
       ∘ costOfChoices ∘ treesToChoices $ allOptions
-}

 		 	   		  
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110330/c16c0739/attachment-0001.html