uAgda-1.0.0.0: Basics.hs

{-# LANGUAGE OverloadedStrings, GeneralizedNewtypeDeriving #-}
module Basics
       (module Data.Monoid, (<>),
        module Control.Applicative,
        Irr(..), 
        Sort(..), prettySortNam, prettyRel,
        above, oneLev, next, oneRel, zero,
        Ident, Identifier(..), DisplayContext,
        Position, dummyPosition, identPosition, 
        isDummyId, modId, synthId, dummyId, idString,
        Relevance(..), (+.),
        Lattice(..)) where

import Display
import qualified RawSyntax as A
import RawSyntax (Identifier(..))
import Control.Applicative
import Data.Monoid
import Data.Sequence (Seq)


(<>) :: Monoid a => a -> a -> a
(<>) = mappend

-----------
-- Irr

newtype Irr a = Irr {fromIrr :: a}
    deriving Show

instance Eq (Irr a) where
    x == y = True

instance Pretty x => Pretty (Irr x) where
    pretty (Irr x) = pretty x

--------------
-- Ident
instance Pretty Identifier where
    pretty (Identifier (_,x)) = text x


type Ident = Irr Identifier

isDummyId (Irr (Identifier (_,"_"))) = True
isDummyId _ = False 

synthId :: String -> Ident
synthId x = Irr (Identifier (fromIrr $ dummyPosition,x))

dummyId = synthId "_"

idString :: Ident -> String
idString (Irr (Identifier (_,name))) = name

type DisplayContext = Seq Ident

----------------
-- Position

type Position = (Int,Int)

identPosition (Irr (Identifier (p,_))) = Irr p

dummyPosition = Irr (0,0)

modId :: (String -> String) -> Ident -> Ident
modId f (Irr (Identifier (pos ,x)))  = (Irr (Identifier (pos,f x)))

------------------
-- Sort

instance Lattice Int where
    (⊔) = max

newtype Relevance = Relevance {fromRel :: Int}
  deriving (Real,Enum,Integral,Num,Ord,Eq,Show,Lattice)

class Lattice a where
    (⊔) :: a -> a -> a


data Sort = Sort {sortLevel :: Int, sortRelevance :: Relevance}
  deriving Eq

instance Show Sort where
    show s = render (prettySortNam s)


instance Pretty Relevance where
    pretty (Relevance 0) = mempty
    pretty (Relevance r) = superscriptPretty r

instance Pretty Sort where
    pretty s = "∗" <> prettySortNam s  -- ⋆★*∗
    
prettySortNam s = prettyLev s <> prettyRel s

prettyRel (Sort _ r) = pretty r

prettyLev (Sort 0 _) = mempty
prettyLev (Sort l _) = subscriptPretty l

instance Num Sort where
    Sort l1 r1 + Sort l2 r2 = Sort (l1 + l2) (r1 + r2)
    negate (Sort l r) = Sort (negate l) (negate r)

above (Sort l r) = Sort (l + 1) r
oneLev = Sort 1 0

oneRel = Sort 0 1
next :: Relevance -> Relevance
next = (+ 1)

zero = Sort 0 0 

(+.) :: Relevance -> Sort -> Relevance
r +. (Sort _ r') = r + r'