<html>
<head>
<style><!--
.hmmessage P
{
margin:0px;
padding:0px
}
body.hmmessage
{
font-size: 10pt;
font-family:Tahoma
}
--></style>
</head>
<body class='hmmessage'>
Hello,<br><br>I am trying to write an agda program (mySolution.agda) for the "Escape From Zurg: An Exercise in Logic Programming" ( <a href="http://web.engr.oregonstate.edu/%7Eerwig/zurg/" target="_blank">http://web.engr.oregonstate.edu/~erwig/zurg/</a> ).<br><br>This program lists all the possible options, after figuring out how to use the "<" (less-than) in agda.<br><br>Can you please let me know what agda functionality / features I can add to make this program better?<br><br>Thanks a lot<br><br><br>module mySolution where<br><br>open import Data.List -- using (List; []; _:_)<br>open import Data.Nat -- using (ℕ)<br>open import Data.Tuple<br>open import Data.Bool<br>open import Data.Maybe<br>open import Function<br><br>data Toy : Set where<br> Buzz Woody Rex Hamm : Toy<br><br>time : Toy → ℕ<br>time Buzz = 5<br>time Woody = 10<br>time Rex = 20<br>time Hamm = 25<br><br>allToys : List Toy<br>allToys = Buzz ∷ Woody ∷ Rex ∷ Hamm ∷ []<br><br>LeftToys : Set<br>LeftToys = List Toy<br><br>RightToys : Set<br>RightToys = List Toy<br><br>FirstToy : Set<br>FirstToy = Toy<br>SecondToy : Set<br>SecondToy = Toy<br><br>mutual<br> Backwards : Set<br> Backwards = List (Maybe Tree)<br> Forwards : Set<br> Forwards = List (Maybe Tree)<br> data Tree : Set where<br> treeForward : FirstToy → SecondToy<br> → LeftToys → RightToys<br> → Backwards → Tree<br> treeBackward : Toy<br> → LeftToys → RightToys<br> → Forwards → Tree<br>{-<br>record Forward : Set where<br> field firstToy : Toy<br> secondToy : Toy<br> leftToys : LeftToys<br> rightToys : RightToys<br> nextBackwardSteps : List BackwardTree<br>record Backward : Set where<br> field toy : Toy<br> leftToys : LeftToys<br> rightToys : RightToys<br> nextForwardSteps : List ForwardTree<br>mutual<br> data Forward (FirstToy : Toy) (SecondToy : Toy)<br> (LeftToys : Set) (RightToys : Set)<br> (Backwards : List Tree)<br> : Set where<br> forward : FirstToy → SecondToy<br> → LeftToys → RightToys<br> → Backwards<br> → Forward FirstToy SecondToy<br> LeftToys RightToys<br> Backwards<br> data Backward (Toy : Set)<br> (LeftToys : Set) (RightToys : Set)<br> : Set where<br> backward : Toy<br> → LeftToys → RightToys<br> → Forwards<br> → Backward Toy<br> LeftToys RightToys<br> Forwards<br>-}<br>{-<br>mutual<br> Backwards : Set<br> Backwards = List Backward<br> Forwards : Set<br> Forwards = List Forward<br> data Forward (FirstToy : Toy) (SecondToy : Toy)<br> (LeftToys : Set) (RightToys : Set)<br> (Backwards : Set)<br> : Set where<br> forward : FirstToy → SecondToy<br> → LeftToys → RightToys<br> → Backwards<br> → Forward FirstToy SecondToy<br> LeftToys RightToys<br> Backwards<br> data Backward (Toy : Set)<br> (LeftToys : Set) (RightToys : Set)<br> : Set where<br> backward : Toy<br> → LeftToys → RightToys<br> → Forwards<br> → Backward Toy<br> LeftToys RightToys<br> Forwards<br>-}<br><br>-- subsets of size k<br>combinationsOf : ℕ → List Toy → List (List Toy)<br>combinationsOf 0 _ = [ [] ]<br>combinationsOf _ [] = []<br>combinationsOf k (x ∷ xs) = map (_∷_ x) (combinationsOf (k ∸ 1) xs)<br> ++ combinationsOf k xs<br><br>toTuple : List Toy → Maybe (Toy × Toy)<br>toTuple (x ∷ y ∷ []) = just (tuple x y)<br>toTuple _ = nothing -- error "unknown combination"<br><br>_==_ : Toy → Toy → Bool<br>Buzz == Buzz = true<br>Woody == Woody = true<br>Rex == Rex = true<br>Hamm == Hamm = true<br>_ == _ = false<br><br>delete : Toy → List Toy → List Toy<br>delete toy toys = filter (λ a → not (a == toy)) toys<br><br>--fromJust : List (Maybe Toy) → List Toy<br>--fromJust xs = filter (λ a → not $ maybeToBool a) xs<br><br>mutual<br> buildTree : LeftToys → RightToys → Maybe (Toy × Toy) → Maybe Tree<br> buildTree (_ ∷ _ ∷ []) right (just (tuple firstToy secondToy))<br> = just (treeForward firstToy secondToy<br> -- toys on the left<br> []<br> -- toys on the right<br> (firstToy ∷ secondToy ∷ right)<br> -- child trees<br> [])<br> buildTree left right (just (tuple firstToy secondToy))<br> = just (treeForward firstToy secondToy<br> -- toys on the left<br> lefttoys<br> -- toys on the right<br> righttoys<br> -- child trees<br> --(fromJust ∘ map (backwardMoves<br> (map (backwardMoves<br> lefttoys<br> righttoys)<br> $ righttoys))<br> where lefttoys = delete firstToy ∘ delete secondToy $ left<br> righttoys = firstToy ∷ secondToy ∷ right<br> buildTree _ _ _ = nothing<br><br> backwardMoves : LeftToys → RightToys → Toy → Maybe Tree<br> backwardMoves left right backward<br> = just (treeBackward backward -- Backward<br> -- toys on the left<br> lefttoys<br> -- toys on the right<br> (delete backward right)<br> -- child trees<br> --(fromJust ∘ map (buildTree<br> (map (buildTree lefttoys righttoys<br> ∘ toTuple)<br> ∘ combinationsOf 2<br> $ lefttoys))<br> where lefttoys = backward ∷ left<br> righttoys = (delete backward right)<br><br>allOptions : List (Maybe Tree)<br>allOptions = map (buildTree allToys [] ∘ toTuple)<br> ∘ combinationsOf 2 $ allToys<br><br>data Move : Set where<br> moveF : FirstToy → SecondToy → Move<br> moveB : Toy → Move<br><br>Choice : Set<br>Choice = List Move<br><br>mutual<br> treesToChoices : List (Maybe Tree) → List Choice<br> treesToChoices trees = concatMap treeToChoices trees<br><br> treeToChoices : Maybe Tree → List Choice<br> treeToChoices (just (treeForward x y [] _ []))<br> = (((moveF x y) ∷ [] ) ∷ [])<br> treeToChoices (just (treeForward x y _ _ nextSteps))<br> = map (_∷_ (moveF x y)) $ treesToChoices nextSteps<br> treeToChoices (just (treeBackward x _ _ nextSteps))<br> = map (_∷_ (moveB x)) $ treesToChoices nextSteps<br> treeToChoices (nothing) = (([]) ∷ [])<br><br>Cost : Set<br>Cost = ℕ<br><br>moveCost : Move → Cost<br>moveCost (moveF x y) = (time x) ⊔ (time y)<br>moveCost (moveB x) = time x<br><br>costOfChoice : Choice → (Cost × Choice)<br>costOfChoice choice = tuple (sum ∘ map moveCost $ choice) choice<br><br>costOfChoices : List Choice → List (Cost × Choice)<br>costOfChoices = map costOfChoice<br><br>lessThan : ℕ → ℕ → Bool<br>lessThan zero (suc y) = true<br>lessThan (suc x) zero = false<br>lessThan zero zero = false<br>lessThan (suc x) (suc y) = lessThan x y<br><br>solution : List (Cost × Choice)<br>solution = filter (λ x → lessThan (fst x) 61)<br> ∘ costOfChoices ∘ treesToChoices $ allOptions<br><br>{-<br>main : IO Unit<br>--main = putStrLn ∘ groom ∘ filter (λ (cost , _) → cost < 61)<br>main = putStrLn ∘ filter (λ < cost , _ > → cost < 61)<br> ∘ costOfChoices ∘ treesToChoices $ allOptions<br>-}<br><br> </body>
</html>