view navigation.ur @ 33:2e7f8f7d71d4

Update for Ur/Web's new tag name resolution
author Adam Chlipala <adam@chlipala.net>
date Thu, 21 Nov 2013 16:12:17 -0500
parents d32fb0f7b137
children
line wrap: on
line source
functor Make(M : sig
                 con linkPos :: {Unit}
                 val linkFolder : folder linkPos
                 con navbarPos :: {Unit}
                 con msgPos :: {Unit}
                 val msgFolder : folder msgPos
                 con linkStyles :: {Type} = mapU (option css_class) linkPos
                 con themePos :: {Unit}
                 val linkStyles : $linkStyles
                 val formatNav : $(mapU xbody navbarPos) -> $(mapU xbody linkPos) -> $(mapU xbody msgPos)
                                 -> $(mapU xbody themePos)
             end) = struct

    open Navbar

    con modeLs :: {Type} -> Type = fn r :: {Type} => $(map mode r)
    con barLs :: {Type} -> Type = fn r :: {Type} => $(map navBar r)

    con linkLs :: {Unit} -> Type = fn r :: {Unit} => $(mapU (option navItem) r)
    con msgLs :: {Unit} -> Type = fn r :: {Unit} => $(mapU (option xbody) r)

    con shape t = t -> $(mapU xbody M.navbarPos) 

    val shape_npos : shape $(mapU xbody M.navbarPos) = (fn x => x)

    con crush :: {Type} -> Type = fn r :: {Type} => $(map (fn _ => xbody) r) 

    con navigation :: {Type} -> Type = fn m :: {Type} => {Nav : barLs m,
                                                          Link : linkLs M.linkPos,
                                                          Msg : msgLs M.msgPos}

    fun mkNav [m ::: {Type}] (sh : shape (crush m)) (d : modeLs m) (n : barLs m) 
              (l : linkLs M.linkPos) (msg : msgLs M.msgPos)  =
        {Nav = n, Link = l, Msg = msg}

    fun barsToXml [m ::: {Type}] (fl : folder m) (ms : modeLs m) (ns : barLs m) = 
        @@Top.fold [fn r :: {Type} => $(map mode r) -> $(map navBar r) -> $(map (fn _ => xbody) r)]
          (fn [nm :: Name] [t :: Type] [rest :: {Type}] [[nm] ~ rest]
                           (acc : _ -> _ -> _) rm rn =>
              {nm = @@navBarToXml [t] rm.nm rn.nm} ++ (acc (rm -- nm) (rn -- nm))) 
          (fn _ _ => {}) [m] fl ms ns

    fun linksToXml (l : linkLs M.linkPos) =
        let
            fun render s ol =
                case ol of
                    None => <xml/>
                  | Some l => navItemToXml s l

        in
            @@Top.fold [fn u :: {Unit} => $(mapU (option navItem) u) -> $(mapU (option css_class) u) -> $(mapU xbody u)]
              (fn [nm :: Name] [t ::_] [rest :: {Unit}] [[nm] ~ rest]
              (acc : _ -> _ -> _) r s => {nm = render s.nm r.nm} ++ (acc (r -- nm) (s -- nm)))
              (fn _ _ => {}) [M.linkPos] M.linkFolder l M.linkStyles
        end

    fun msgToXml (msg : msgLs M.msgPos) =
        let 
            fun render om =
                case om of
                    None => <xml/>
                  | Some m => m
        in
            @@Top.mp [fn u => (option xbody)] [fn u => xbody]
              (fn [t :::_] => render) [M.msgPos] M.msgFolder msg
        end

    fun toXml [m ::: {Type}] (fl : folder m) (sh : shape (crush m)) (d : modeLs m) {Nav = nav, Link = l, Msg = msg} =
        M.formatNav (sh (@@barsToXml [m] fl d nav)) (linksToXml l) (msgToXml msg)

end