uAgda-1.2.0.0: AbsSynToTerm.hs

{-# LANGUAGE PackageImports #-}

module AbsSynToTerm where

import Terms 
import qualified RawSyntax as A
import RawSyntax (Identifier(..))
import Control.Monad.Trans.State (runStateT, StateT)
import Control.Monad.Trans.Reader
import Control.Monad.Trans.Error hiding (throwError)
import Control.Monad.Error
import Control.Monad.State
import Control.Applicative
import Data.Functor.Identity
import Data.List
import Basics
import Permutation
import Data.List.Split

type LocalEnv = [String]
type GlobalEnv = ()

type Resolver a = ReaderT LocalEnv (StateT GlobalEnv (ErrorT String Identity)) a


runResolver :: Resolver a -> a
runResolver x = case runIdentity $ runErrorT $ runStateT (runReaderT x []) () of
                  Left err -> error err
                  Right a -> fst a

look :: BitVector -> Identifier -> Resolver Term
look bv (ident@(Identifier (position,x))) = do
  e <- ask
  case elemIndex x e of
    Nothing -> throwError ("unknown identifier: " ++ show ident)
    Just x -> return $ Bound (Irr position) bv x

insertVar :: Identifier -> LocalEnv -> LocalEnv
insertVar (Identifier (_pos,x)) e = x:e

dummyVar :: Identifier
dummyVar = Identifier ((0,0),"_")


manyDep o binder a []     b = resolveTerm b
manyDep o binder a (x:xs) b = binder (Irr x) <$> resolveMulti o a <*> local (insertVar x) (manyDep o binder a xs b)

manyLam :: [A.Bind] -> A.Exp -> Resolver Term
manyLam []            b = resolveTerm b
manyLam (A.NoBind (A.AIdent x):xs) b = Lam Regu (Irr x) (unit $ Hole dummyPosition "") <$> local (insertVar x) (manyLam xs b)
manyLam (A.Bind (A.AIdent x) (A.Colon o) t:xs) b = Lam (toBnd o) (Irr x) <$> resolveMulti (toBnd o) t <*> local (insertVar x) (manyLam xs b)

toBnd ":" = Regu
toBnd "::" = Pred

extractVars :: A.Exp -> Resolver [Identifier]
extractVars (A.EVar (A.AIdent i)) = return [i]
extractVars (A.EApp (A.EVar (A.AIdent i)) rest) = (i:) <$> extractVars rest
extractVars _ = throwError "list of variables expected"

trailingHole Regu xs = xs
trailingHole Pred xs = xs ++ [Hole (Irr (0,0)) "⊘"]

resolveMulti :: Binder -> A.Exp -> Resolver (Cube Term)
resolveMulti o t = do
  xs <- trailingHole o <$> resolveMulti' t
  case cubeFromList xs of
    Just c -> return c
    Nothing -> throwError "incomplete cube"

resolveMulti' :: A.Exp -> Resolver [Term]
resolveMulti' (A.EMulti xs) = mapM resolveTerm xs
resolveMulti' x = (:[]) <$> resolveTerm x

resolveTerm :: A.Exp -> Resolver Term
resolveTerm (A.EMulti _) = throwError "expression list only allowed in some contexts"
-- resolveTerm (A.EDestr x (A.Natural n)) = Destroy (read n) <$> resolveTerm x
resolveTerm (A.EHole (A.Hole (p,x))) = return $ Hole (Irr p) x
resolveTerm (A.EParam x) = Param <$> resolveTerm x
resolveTerm (A.ESwap x (A.Permutation ('#':p))) = Swap (permFromString p) <$> resolveTerm x
-- resolveTerm (A.EUp x) = Shift (Sort 1) <$> resolveTerm x
resolveTerm (A.EVar (A.AIdent x)) = look nil x
resolveTerm (A.EVarI (A.AIdent x) (A.Natural ix)) = look (bvFromString ix) x
resolveTerm (A.ESet (A.Sort (p,c:s))) = return $ Star (Irr p) $ Sort level (read ('0':dim))
   where (lev:dim:_) = splitOn "|" s ++ [""]
         level = case c of
                   '#' -> (-1)
                   '*' -> read ('0':lev)
resolveTerm (A.EProj x (A.AIdent (Identifier (_,field)))) = Proj True  <$> resolveTerm x <*> pure field
resolveTerm (A.EExtr x (A.AIdent (Identifier (_,field)))) = Proj False <$> resolveTerm x <*> pure field
resolveTerm (A.EApp f x)  = App Regu <$> resolveTerm f <*> resolveMulti Regu x
resolveTerm (A.EAppP f x) = App Pred <$> resolveTerm f <*> resolveMulti Pred x
resolveTerm (A.ESigma a b) = case a of
   (A.EAnn vars colon a') -> do
     vs <- extractVars vars
     manyDep Regu (\i a b -> Sigma i (a!?nil) b) a' vs b
                          
   (A.EAbs _ _ _) -> throwError "cannot use lambda for type"
   _              -> Sigma (Irr dummyVar) <$> resolveTerm a <*> local (insertVar dummyVar) (resolveTerm b)            
resolveTerm (A.EPi a (A.Arrow arrow) b) = case a of
   (A.EAnn vars (A.Colon colon) a') -> do 
     vs <- extractVars vars
     manyDep o (Pi o) a' vs b
                          
   (A.EAbs _ _ _) -> throwError "cannot use lambda for type"
   _            -> Pi o (Irr dummyVar) <$> resolveMulti o a <*> local (insertVar dummyVar) (resolveTerm b)

 where o = case arrow of
             "->" -> Regu
             "=>" -> Pred

resolveTerm (A.EAbs ids _ b) = manyLam ids b
resolveTerm (A.EPair (A.Decl (A.AIdent i) e) rest) = Pair (Irr i) <$> resolveTerm e <*> local (insertVar i) (resolveTerm rest)
resolveTerm (A.EPair (A.PDecl (A.AIdent i) e t) rest) = 
   Pair (Irr i) <$> 
   (Ann <$> (OfParam (Irr i) <$> resolveTerm e) <*> resolveTerm t)
   <*> local (insertVar i) (resolveTerm rest)

resolveTerm (A.EAnn e1 _colon_ e2) = Ann <$> resolveTerm e1 <*> resolveTerm e2