Syntax.hs

{-# LANGUAGE TypeSynonymInstances #-}
module PiSigma.Syntax where

import Prelude hiding (pi)

-- * Abstract syntax

data Phrase = Prog Prog | Term Term
  deriving (Show,Eq)

type Name = String

type Label = String

data Entry = Decl Name Type | Defn Name Term
  deriving (Show,Eq)

type Prog = [Entry]

{-
Maybe better
data Prog = Decl Type (Bind Prog) | Defn Name Term Prog
-}

type Type = Term

-- | The use of Bind indicates the scope of the
-- bound identifier.
type Bind a = (Name,a)

-- | For treating quantifiers in a uniform way.
data PiSigma = Pi | Sigma
  deriving (Show,Eq)

data Term =
    Var   String
  | Let   Prog Term
  | Type
  | Q     PiSigma (Type,Bind Type)
  | Lam   (Bind Term)
  | Term :. Term
  | Pair  (Term,Term)
  | Split Term (Bind (Bind Term)) -- split t with (x,y) -> u
  | Enum  [Label]
  | Label Label
  | Case  Term [(Label,Term)]     -- case t of { L -> u }
  | Lift  Term
  | Box   Term
  | Force Term
  deriving (Show,Eq)

-- * Smart constructors

-- | Smart constructor for lambda abstractions.
lam :: [Name] -> Term -> Term
lam []     t = t
lam (x:xs) t = Lam (x,lam xs t)

-- | Smart constructor for split.
split :: Term -> Name -> Name -> Term -> Term
split t1 x y t2 = Split t1 (x,(y,t2))

-- | Smart constructor for quantifiers.
q :: PiSigma -> [(Name,Type)] -> Type -> Type
q ps []          b = b
q ps ((x,a):xas) b = Q ps (a,(x,q ps xas b))

-- | Smart constructor for multiple Pi applications.
pis' :: [(Name,Type)] -> Type -> Type
pis'    = q Pi

-- | Smart constructor for multiple Pi applications.
pis :: [Name] -> Type -> Type -> Type
pis ns t = pis' (map (\ n -> (n,t)) ns)

-- | Smart constructor for Pi.
pi :: Name -> Type -> Type -> Type
pi n t = pis' [(n,t)]

-- | Smart constructor for multiple Sigma applications.
sigmas' :: [(Name,Type)] -> Type -> Type
sigmas' = q Sigma

-- | Smart constructor for multiple Sigma applications.
sigmas :: [Name] -> Type -> Type -> Type
sigmas ns t = sigmas' (map (\ n -> (n,t)) ns)

-- | Smart constructor for Sigma.
sigma :: Name -> Type -> Type -> Type
sigma n t = sigmas' [(n,t)]

-- | Smart constructor for function space.
(->-) :: Type -> Type -> Type
(->-) = pi ""

-- | Smart constructor for product.
(-*-) :: Type -> Type -> Type
(-*-) = sigma ""

-- * Values (well-scoped WHNFs) and environments

-- ** Identifiers

type Id = Int -- index in (potentially multiple) environments

-- ** Scopes

data Scope = Scope [(Name,(Id,Maybe (Clos Type)))]
  deriving (Show,Eq)

{-

TODO:

Perhaps return to the following types for scopes:

data Sc a = Scope [(Name,(Id, a))]

type Scope = Sc ()
type Ctx   = Sc (Clos Type)

We then need a forgetful mapping:

fog :: Ctx -> Scope
fog c = map (\ (x,(i,a)) -> (x,(i,()))) c 

Alternatively, we can try to make Scopes
existential, essentially:

type Scope = exists a. Sc a

-}

emptyScope :: Scope
emptyScope = Scope []

extendScope :: Scope -> Name -> (Id,Maybe (Clos Type)) -> Scope
extendScope (Scope s) x (i,a) = Scope ((x,(i,a)) : s)

lookupScope :: Scope -> Name -> Maybe Id
lookupScope (Scope s) x = do (i,_) <- lookup x s
                             return i

lookupCon :: Scope -> Name -> Maybe (Clos Type)
lookupCon (Scope s) x = do (_,Just a) <- lookup x s
                           return a

-- ** Closures

type Clos a = (a,Scope)

--type C a = (Con,a)

--c2clos :: C a -> Clos a
--c2clos (g,a) = (a,fog g)

-- fix order, name of C...

class Closure a where 
    getScope :: a -> Scope
    putScope :: a -> Scope -> a

instance Closure (Clos a) where
    getScope (_,s)   = s
    putScope (a,_) s = (a,s)

instance Closure a => Closure (Bind a) where
    getScope (_,a)   = getScope a
    putScope (x,a) s = (x,putScope a s)

instance Closure Boxed where
    getScope (Boxed c)   = getScope c
    putScope (Boxed c) s = Boxed (putScope c s)

{- could be used to refactor the code using bindings. -}

ty :: Clos Type
ty = (Type,emptyScope)

label :: String -> Clos Term
label s = (Label s,emptyScope)

type VType = Val

newtype Boxed = Boxed (Clos Term) deriving (Show,Eq)

-- ** Values

data Val =
    Ne Ne
  | VType 
  | VQ PiSigma (Clos (Type,Bind Type))
  | VLift (Clos Type)
  | VLam (Bind (Clos Term))
  | VPair (Clos (Term, Term))
  | VEnum [Label]
  | VLabel Label 
  | VBox Boxed
  deriving (Show,Eq)

-- | Neutral terms.
data Ne =
    NVar Id
  | Ne :.. (Clos Term)
  | NSplit Ne (Bind (Bind (Clos Term)))
  | NCase Ne (Clos [(Label,Term)])
  | NForce Ne
  deriving (Show,Eq)

-- ** Environments

data EnvEntry = Id Id | Closure (Clos Term) deriving Show

data PrtInfo = PrtInfo {name :: Name, expand :: Bool}

class Env e where 
    emptyE :: e
    extE   :: e -> PrtInfo -> (Id,e)
    setE   :: e -> Id -> EnvEntry -> e
    getE   :: e -> Id -> EnvEntry
    prtE   :: e -> Id -> PrtInfo

set :: [a] -> Int -> a -> [a]
set (a:as) 0 b = b:as
set (a:as) i b = a:set as (i-1) b
 
type EnvEntries = [(EnvEntry,PrtInfo)]

instance Env EnvEntries where
    emptyE     = []
    extE e x   = let i = length e in (i,e++[(Id i,x)])
    setE e i v = let (_,x) = e!!i in set e i (v,x)
    getE e i   = let (v,_) = e!!i in v
    prtE e i   = let (_,x) = e!!i in x