systemqfw

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

Core.hs (864B)

      1 module Core where
      2 
      3 import Common
      4 
      5 --------------------------------------------------------------------------------
      6 -- Types
      7 
      8 newtype TypeIdx = TypeIdx Int deriving (Show, IsInt)
      9 
     10 data Type q
     11     = TypeVar TypeIdx
     12 
     13     | TypeTArrow (Type q) (Type q)
     14     | TypeTForall Kind (Type q)
     15 
     16     | TypeQ q
     17     | TypeQAdd (Type q) (Type q)
     18     | TypeQMul (Type q) (Type q)
     19 
     20     | TypeQTPair (Type q) (Type q)
     21     | TypeQTFst (Type q)
     22     | TypeQTSnd (Type q)
     23 
     24     | TypeArrowAbs (Type q)
     25     | TypeArrowApp (Type q) (Type q)
     26     deriving Show
     27 
     28 --------------------------------------------------------------------------------
     29 -- Terms
     30 
     31 newtype TermIdx = TermIdx Int deriving (Show, IsInt)
     32 
     33 data Term q
     34     = TermVar TermIdx
     35 
     36     | TermArrowAbs (Term q)
     37     | TermArrowApp (Term q) (Term q)
     38 
     39     | TermForallAbs (Term q)
     40     | TermForallApp (Term q) (Type q)
     41     deriving Show