HOLOps.hs

-- $Id: HOLOps.hs,v 1.3 2001/07/19 22:17:37 wlh Exp $

module HOLOps (getHOLTyCon, getHOLOp) where

holOps = [ ("===",   (True, "=")),
           ("==>",   (True, "==>")),
           ("&&&",   (True, "/\\")),
           ("|||",   (True, "\\/")),
           (".",     (True, "o")),
           ("==",    (True, "=")),
           ("$",     (False, "(\\ f . \\ x . f x)")),
           ("True",  (False, "true")),
           ("False", (False, "false"))
         ]

holTyCons = [ ("[]",  "list"),
              ("()",  "unit"),
              ("Int", "int"),
              ("Nat", "num")
            ]

-- lookup n db = filter ((== n) . fst) db

getHOLTyCon :: String -> Maybe String
getHOLTyCon con = lookup con holTyCons

getHOLOp :: String -> Maybe (Bool, String)
getHOLOp n = lookup n holOps