Nf.hs

{-# LANGUAGE UndecidableInstances, MultiParamTypeClasses, FunctionalDependencies,
             TypeSynonymInstances, FlexibleInstances #-}
module PiSigma.Nf where

{- Implementation of a normalisation function.
   Useful for testing.
-}

import Control.Monad

import PiSigma.Syntax
import PiSigma.Evaluation

type Vars = [String]

fresh :: Name -> Vars -> Name
fresh x xs = if x/="" && elem x xs then fresh (x++"'") xs
             else x

class Nf a b | a -> b where
    nf :: Env e => Vars -> a -> Eval e b
    nf = nf' True
    quote :: Env e => Vars -> a -> Eval e b
    quote = nf' False
    nf' :: Env e => Bool -> Vars -> a -> Eval e b


instance Nf (Clos Term) Term where
    nf' True xs t = do t' <- eval t
                       nf' True xs t'
    nf' False xs t = qq xs t

instance Nf Id Term where
    nf' b xs i = do e <- getEnv
                    let (PrtInfo x exp) = prtE e i
                    case getE e i of
                      (Id _) -> return (Var x) 
                      (Closure t) -> if exp then nf' b xs t
                                     -- this is bad, we should not
                                     -- expand inside a box!
                                     else return (Var x) 

qq :: Env e => Vars -> Clos Term -> Eval e Term
qq xs (Var x,s) = do i <- getId x s
                     quote xs i
qq xs (Let g t, s) = fail "quote let: not implemented!"
{-do s' <- evalProg (g,s)
                        qq xs (t,s')  
                       -- this seems wrong! we should return a Let
                       -- and we should extend xs!
-}
qq xs (Q ps (a,(x,b)),s) = 
    do a' <- qq xs (a,s)
       xb' <- quote xs (x,(b,s))
       return (Q ps (a',xb'))
qq xs (Lift t,s) = liftM Lift (qq xs (t,s))
qq xs (Lam (x,t), s) = liftM Lam (quote xs (x,(t,s)))
qq xs (t :. u ,s) = do t' <- qq xs (t,s)
                       u' <- qq xs (u,s)
                       return (t' :. u')
qq xs (Pair (t,u),s) = do t' <- qq xs (t,s)
                          u' <- qq xs (u,s)
                          return (Pair (t',u'))
qq xs (Split t (x,(y,u)),s) = do t' <- qq xs (t,s)
                                 xyu' <- quote xs (x,(y,(u,s)))
                                 return (Split t' xyu')
qq xs (Case t lts,s) = do t' <- qq xs (t,s)
                          lts' <- mapM (\ (l,t) -> 
                                            do t' <- qq xs (t,s)
                                               return (l,t')) lts
                          return (Case t' lts')              
qq xs (Box t,s) = liftM Box (qq xs (t,s))
qq xs (Force t,s) = liftM Force (qq xs (t,s))
qq xs (t,s) = return t -- Type, Enum, Label

instance (Closure a,Nf a b) => Nf (Bind a) (Bind b) where
    nf' b xs (x,t)  = do let x' = fresh x xs
                         (i,s') <- decl x (PrtInfo x' True) (getScope t) Nothing
                         t' <- nf' b (x':xs) (putScope t s')
                         return (x',t')

instance Nf Val Term where
    nf' b xs (Ne n) = nf' b xs n
    nf' b xs VType = return Type
    nf' b xs (VQ ps ((a,(x,c)),s)) = do a' <- nf' b xs (a,s) 
                                        xc' <- nf' b xs (x,(c,s))
                                        return (Q ps (a',xc'))
    nf' b xs (VLift c) = liftM Lift (nf' b xs c)
    nf' b xs (VLam xt) = liftM Lam (nf' b xs xt)
    nf' b xs (VPair ((t,u),s)) = do t' <- nf' b xs (t,s)
                                    u' <- nf' b xs (u,s)
                                    return (Pair (t',u'))
    nf' b xs (VBox (Boxed c)) = liftM Box (nf' False xs c)
    nf' b xs (VEnum ls) = return (Enum ls)
    nf' b xs (VLabel l) = return (Label l)


instance Nf Ne Term where
    nf' b xs (NVar i) = nf' b xs i
    nf' b xs (t' :.. u) = do t <- nf' b xs t'
                             u' <- nf' b xs u
                             return (t :. u')
    nf' b xs (NSplit t xyu) = do t' <- nf' b xs t
                                 xyu' <- nf' b xs xyu
                                 return (Split t' xyu')
    nf' b xs (NCase t (lus,s)) = do t' <- nf xs t
                                    lus' <- mapM (\ (l,u) -> 
                                                   do u' <- nf' b xs (u,s)
                                                      return (l,u')) lus
                                    return (Case t' lus')
    nf' b xs (NForce t) = liftM Force (nf xs t)