systemqfw

system Q F omega elaborator
git clone git://git.rr3.xyz/systemqfw
Log | Files | Refs | Submodules | README | LICENSE

Surface.hs (1077B)

      1 module Surface where
      2 import Data.ByteString (ByteString)
      3 
      4 import Common
      5 
      6 --------------------------------------------------------------------------------
      7 -- Types
      8 
      9 newtype TypeName = TypeName ByteString deriving (Eq, Ord, Show)
     10 
     11 data Type q
     12     = TypeVar TypeName
     13     | TypeAnnot (Type q) Kind
     14 
     15     | TypeTArrow (Type q) (Type q)
     16     | TypeTForall TypeName Kind (Type q)
     17 
     18     | TypeQ q
     19     | TypeQAdd (Type q) (Type q)
     20     | TypeQMul (Type q) (Type q)
     21 
     22     | TypeQTPair (Type q) (Type q)
     23     | TypeQTFst (Type q)
     24     | TypeQTSnd (Type q)
     25 
     26     | TypeArrowAbs TypeName (Type q)
     27     | TypeArrowApp (Type q) (Type q)
     28     deriving Show
     29 
     30 --------------------------------------------------------------------------------
     31 -- Terms
     32 
     33 newtype TermName = TermName ByteString deriving (Eq, Ord, Show)
     34 
     35 data Term q
     36     = TermVar TermName
     37     | TermAnnot (Term q) (Type q)
     38     | TermLet TermName (Term q) (Type q) (Term q)
     39 
     40     | TermArrowAbs TermName (Term q)
     41     | TermArrowApp (Term q) (Term q)
     42 
     43     | TermForallAbs TypeName (Term q)
     44     | TermForallApp (Term q) (Type q)
     45     deriving Show