Mercurial > urweb
annotate lib/ur/monad.urs @ 917:321a2d6feb40
dragList demo working, save for Gecko load delay and highlighting
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Tue, 08 Sep 2009 10:55:49 -0400 |
parents | 8e540df3294d |
children | 37dd42935dad |
rev | line source |
---|---|
adamc@834 | 1 val exec : m ::: (Type -> Type) -> monad m -> ts ::: {Type} |
adamc@834 | 2 -> $(map m ts) -> folder ts -> m $ts |
adamc@898 | 3 |
adamc@898 | 4 val ignore : m ::: (Type -> Type) -> monad m -> t ::: Type |
adamc@898 | 5 -> m t -> m unit |
adamc@905 | 6 |
adamc@917 | 7 val mp : m ::: (Type -> Type) -> monad m -> a ::: Type -> b ::: Type |
adamc@917 | 8 -> (a -> b) -> m a -> m b |
adamc@917 | 9 |
adamc@905 | 10 val foldR : K --> m ::: (Type -> Type) -> monad m |
adamc@905 | 11 -> tf :: (K -> Type) |
adamc@905 | 12 -> tr :: ({K} -> Type) |
adamc@905 | 13 -> (nm :: Name -> t :: K -> rest :: {K} |
adamc@905 | 14 -> [[nm] ~ rest] => |
adamc@905 | 15 tf t -> tr rest -> m (tr ([nm = t] ++ rest))) |
adamc@905 | 16 -> tr [] |
adamc@905 | 17 -> r :: {K} -> folder r -> $(map tf r) -> m (tr r) |
adamc@905 | 18 |
adamc@905 | 19 val foldR2 : K --> m ::: (Type -> Type) -> monad m |
adamc@905 | 20 -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) |
adamc@905 | 21 -> tr :: ({K} -> Type) |
adamc@905 | 22 -> (nm :: Name -> t :: K -> rest :: {K} |
adamc@905 | 23 -> [[nm] ~ rest] => |
adamc@905 | 24 tf1 t -> tf2 t -> tr rest -> m (tr ([nm = t] ++ rest))) |
adamc@905 | 25 -> tr [] |
adamc@905 | 26 -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> m (tr r) |
adamc@905 | 27 |
adamc@910 | 28 val foldR3 : K --> m ::: (Type -> Type) -> monad m |
adamc@910 | 29 -> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> tf3 :: (K -> Type) |
adamc@910 | 30 -> tr :: ({K} -> Type) |
adamc@910 | 31 -> (nm :: Name -> t :: K -> rest :: {K} |
adamc@910 | 32 -> [[nm] ~ rest] => |
adamc@910 | 33 tf1 t -> tf2 t -> tf3 t -> tr rest -> m (tr ([nm = t] ++ rest))) |
adamc@910 | 34 -> tr [] |
adamc@910 | 35 -> r :: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> m (tr r) |
adamc@910 | 36 |
adamc@905 | 37 val mapR : K --> m ::: (Type -> Type) -> monad m |
adamc@905 | 38 -> tf :: (K -> Type) |
adamc@905 | 39 -> tr :: (K -> Type) |
adamc@905 | 40 -> (nm :: Name -> t :: K -> tf t -> m (tr t)) |
adamc@905 | 41 -> r :: {K} -> folder r -> $(map tf r) -> m ($(map tr r)) |