module PGF.Expr(Tree, BindType(..), Expr(..), Literal(..), Patt(..), Equation(..),
                readExpr, showExpr, pExpr, pBinds, ppExpr, ppPatt, pattScope,

                mkAbs,    unAbs,
                mkApp,    unApp, unapply,
                mkStr,    unStr,
                mkInt,    unInt,
                mkDouble, unDouble,
                mkFloat,  unFloat,
                mkMeta,   unMeta,

                normalForm,

                -- needed in the typechecker

                Value(..), Env, Sig, eval, apply, applyValue, value2expr,

                MetaId,

                -- helpers

                pMeta,pArg,pLit,freshName,ppMeta,ppLit,ppParens
               ) where

import PGF.CId
import PGF.Type
import PGF.ByteCode

import Data.Char
--import Data.Maybe

import Data.List as List
import qualified Data.Map as Map hiding (showTree)
import Control.Monad
import qualified Text.PrettyPrint as PP
import qualified Text.ParserCombinators.ReadP as RP

type MetaId = Int

data BindType = 
    Explicit
  | Implicit
  deriving (BindType -> BindType -> Bool
(BindType -> BindType -> Bool)
-> (BindType -> BindType -> Bool) -> Eq BindType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: BindType -> BindType -> Bool
$c/= :: BindType -> BindType -> Bool
== :: BindType -> BindType -> Bool
$c== :: BindType -> BindType -> Bool
Eq,Eq BindType
Eq BindType
-> (BindType -> BindType -> Ordering)
-> (BindType -> BindType -> Bool)
-> (BindType -> BindType -> Bool)
-> (BindType -> BindType -> Bool)
-> (BindType -> BindType -> Bool)
-> (BindType -> BindType -> BindType)
-> (BindType -> BindType -> BindType)
-> Ord BindType
BindType -> BindType -> Bool
BindType -> BindType -> Ordering
BindType -> BindType -> BindType
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: BindType -> BindType -> BindType
$cmin :: BindType -> BindType -> BindType
max :: BindType -> BindType -> BindType
$cmax :: BindType -> BindType -> BindType
>= :: BindType -> BindType -> Bool
$c>= :: BindType -> BindType -> Bool
> :: BindType -> BindType -> Bool
$c> :: BindType -> BindType -> Bool
<= :: BindType -> BindType -> Bool
$c<= :: BindType -> BindType -> Bool
< :: BindType -> BindType -> Bool
$c< :: BindType -> BindType -> Bool
compare :: BindType -> BindType -> Ordering
$ccompare :: BindType -> BindType -> Ordering
$cp1Ord :: Eq BindType
Ord,Int -> BindType -> ShowS
[BindType] -> ShowS
BindType -> String
(Int -> BindType -> ShowS)
-> (BindType -> String) -> ([BindType] -> ShowS) -> Show BindType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BindType] -> ShowS
$cshowList :: [BindType] -> ShowS
show :: BindType -> String
$cshow :: BindType -> String
showsPrec :: Int -> BindType -> ShowS
$cshowsPrec :: Int -> BindType -> ShowS
Show)

-- | Tree is the abstract syntax representation of a given sentence

-- in some concrete syntax. Technically 'Tree' is a type synonym

-- of 'Expr'.

type Tree = Expr

-- | An expression in the abstract syntax of the grammar. It could be

-- both parameter of a dependent type or an abstract syntax tree for

-- for some sentence.

data Expr =
   EAbs BindType CId Expr           -- ^ lambda abstraction

 | EApp Expr Expr                   -- ^ application

 | ELit Literal                     -- ^ literal

 | EMeta  {-# UNPACK #-} !MetaId    -- ^ meta variable

 | EFun   CId                       -- ^ function or data constructor

 | EVar   {-# UNPACK #-} !Int       -- ^ variable with de Bruijn index

 | ETyped Expr Type                 -- ^ local type signature

 | EImplArg Expr                    -- ^ implicit argument in expression

  deriving (Expr -> Expr -> Bool
(Expr -> Expr -> Bool) -> (Expr -> Expr -> Bool) -> Eq Expr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Expr -> Expr -> Bool
$c/= :: Expr -> Expr -> Bool
== :: Expr -> Expr -> Bool
$c== :: Expr -> Expr -> Bool
Eq,Eq Expr
Eq Expr
-> (Expr -> Expr -> Ordering)
-> (Expr -> Expr -> Bool)
-> (Expr -> Expr -> Bool)
-> (Expr -> Expr -> Bool)
-> (Expr -> Expr -> Bool)
-> (Expr -> Expr -> Expr)
-> (Expr -> Expr -> Expr)
-> Ord Expr
Expr -> Expr -> Bool
Expr -> Expr -> Ordering
Expr -> Expr -> Expr
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Expr -> Expr -> Expr
$cmin :: Expr -> Expr -> Expr
max :: Expr -> Expr -> Expr
$cmax :: Expr -> Expr -> Expr
>= :: Expr -> Expr -> Bool
$c>= :: Expr -> Expr -> Bool
> :: Expr -> Expr -> Bool
$c> :: Expr -> Expr -> Bool
<= :: Expr -> Expr -> Bool
$c<= :: Expr -> Expr -> Bool
< :: Expr -> Expr -> Bool
$c< :: Expr -> Expr -> Bool
compare :: Expr -> Expr -> Ordering
$ccompare :: Expr -> Expr -> Ordering
$cp1Ord :: Eq Expr
Ord,Int -> Expr -> ShowS
[Expr] -> ShowS
Expr -> String
(Int -> Expr -> ShowS)
-> (Expr -> String) -> ([Expr] -> ShowS) -> Show Expr
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Expr] -> ShowS
$cshowList :: [Expr] -> ShowS
show :: Expr -> String
$cshow :: Expr -> String
showsPrec :: Int -> Expr -> ShowS
$cshowsPrec :: Int -> Expr -> ShowS
Show)

-- | The pattern is used to define equations in the abstract syntax of the grammar.

data Patt =
   PApp CId [Patt]                  -- ^ application. The identifier should be constructor i.e. defined with 'data'

 | PLit Literal                     -- ^ literal

 | PVar CId                         -- ^ variable

 | PAs  CId Patt                    -- ^ variable@pattern

 | PWild                            -- ^ wildcard

 | PImplArg Patt                    -- ^ implicit argument in pattern

 | PTilde Expr
  deriving Int -> Patt -> ShowS
[Patt] -> ShowS
Patt -> String
(Int -> Patt -> ShowS)
-> (Patt -> String) -> ([Patt] -> ShowS) -> Show Patt
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Patt] -> ShowS
$cshowList :: [Patt] -> ShowS
show :: Patt -> String
$cshow :: Patt -> String
showsPrec :: Int -> Patt -> ShowS
$cshowsPrec :: Int -> Patt -> ShowS
Show

-- | The equation is used to define lambda function as a sequence

-- of equations with pattern matching. The list of 'Expr' represents

-- the patterns and the second 'Expr' is the function body for this

-- equation.

data Equation =
   Equ [Patt] Expr
  deriving Int -> Equation -> ShowS
[Equation] -> ShowS
Equation -> String
(Int -> Equation -> ShowS)
-> (Equation -> String) -> ([Equation] -> ShowS) -> Show Equation
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Equation] -> ShowS
$cshowList :: [Equation] -> ShowS
show :: Equation -> String
$cshow :: Equation -> String
showsPrec :: Int -> Equation -> ShowS
$cshowsPrec :: Int -> Equation -> ShowS
Show

-- | parses 'String' as an expression

readExpr :: String -> Maybe Expr
readExpr :: String -> Maybe Expr
readExpr String
s = case [Expr
x | (Expr
x,String
cs) <- ReadP Expr -> ReadS Expr
forall a. ReadP a -> ReadS a
RP.readP_to_S ReadP Expr
pExpr String
s, (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isSpace String
cs] of
               [Expr
x] -> Expr -> Maybe Expr
forall a. a -> Maybe a
Just Expr
x
               [Expr]
_   -> Maybe Expr
forall a. Maybe a
Nothing

-- | renders expression as 'String'. The list

-- of identifiers is the list of all free variables

-- in the expression in order reverse to the order

-- of binding.

showExpr :: [CId] -> Expr -> String
showExpr :: [CId] -> Expr -> String
showExpr [CId]
vars = Doc -> String
PP.render (Doc -> String) -> (Expr -> Doc) -> Expr -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [CId] -> Expr -> Doc
ppExpr Int
0 [CId]
vars

instance Read Expr where
    readsPrec :: Int -> ReadS Expr
readsPrec Int
_ = ReadP Expr -> ReadS Expr
forall a. ReadP a -> ReadS a
RP.readP_to_S ReadP Expr
pExpr

mkAbs :: BindType -> CId -> Expr -> Expr
mkAbs :: BindType -> CId -> Expr -> Expr
mkAbs = BindType -> CId -> Expr -> Expr
EAbs

unAbs :: Expr -> Maybe (BindType, CId, Expr)
unAbs :: Expr -> Maybe (BindType, CId, Expr)
unAbs (EAbs BindType
bt CId
x Expr
e) = (BindType, CId, Expr) -> Maybe (BindType, CId, Expr)
forall a. a -> Maybe a
Just (BindType
bt,CId
x,Expr
e)
unAbs (ETyped Expr
e Type
ty) = Expr -> Maybe (BindType, CId, Expr)
unAbs Expr
e
unAbs (EImplArg Expr
e)  = Expr -> Maybe (BindType, CId, Expr)
unAbs Expr
e
unAbs Expr
_             = Maybe (BindType, CId, Expr)
forall a. Maybe a
Nothing

-- | Constructs an expression by applying a function to a list of expressions

mkApp :: CId -> [Expr] -> Expr
mkApp :: CId -> [Expr] -> Expr
mkApp CId
f [Expr]
es = (Expr -> Expr -> Expr) -> Expr -> [Expr] -> Expr
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr -> Expr -> Expr
EApp (CId -> Expr
EFun CId
f) [Expr]
es

-- | Decomposes an expression into application of function

unApp :: Expr -> Maybe (CId,[Expr])
unApp :: Expr -> Maybe (CId, [Expr])
unApp Expr
e = case Expr -> (Expr, [Expr])
unapply Expr
e of
  (EFun CId
f,[Expr]
es) -> (CId, [Expr]) -> Maybe (CId, [Expr])
forall a. a -> Maybe a
Just (CId
f,[Expr]
es)
  (Expr, [Expr])
_           -> Maybe (CId, [Expr])
forall a. Maybe a
Nothing

-- | Decomposes an expression into an application of a constructor such as a constant or a metavariable

unapply :: Expr -> (Expr,[Expr])
unapply :: Expr -> (Expr, [Expr])
unapply = [Expr] -> Expr -> (Expr, [Expr])
extract []
  where
    extract :: [Expr] -> Expr -> (Expr, [Expr])
extract [Expr]
es f :: Expr
f@(EFun CId
_)   = (Expr
f,[Expr]
es)
    extract [Expr]
es (EApp Expr
e1 Expr
e2) = [Expr] -> Expr -> (Expr, [Expr])
extract (Expr
e2Expr -> [Expr] -> [Expr]
forall a. a -> [a] -> [a]
:[Expr]
es) Expr
e1
    extract [Expr]
es (ETyped Expr
e Type
ty)= [Expr] -> Expr -> (Expr, [Expr])
extract [Expr]
es Expr
e
    extract [Expr]
es (EImplArg Expr
e) = [Expr] -> Expr -> (Expr, [Expr])
extract [Expr]
es Expr
e
    extract [Expr]
es Expr
h            = (Expr
h,[Expr]
es)

-- | Constructs an expression from string literal

mkStr :: String -> Expr
mkStr :: String -> Expr
mkStr String
s = Literal -> Expr
ELit (String -> Literal
LStr String
s)

-- | Decomposes an expression into string literal

unStr :: Expr -> Maybe String
unStr :: Expr -> Maybe String
unStr (ELit (LStr String
s)) = String -> Maybe String
forall a. a -> Maybe a
Just String
s
unStr (ETyped Expr
e Type
ty)   = Expr -> Maybe String
unStr Expr
e
unStr (EImplArg Expr
e)    = Expr -> Maybe String
unStr Expr
e
unStr Expr
_               = Maybe String
forall a. Maybe a
Nothing

-- | Constructs an expression from integer literal

mkInt :: Int -> Expr
mkInt :: Int -> Expr
mkInt Int
i = Literal -> Expr
ELit (Int -> Literal
LInt Int
i)

-- | Decomposes an expression into integer literal

unInt :: Expr -> Maybe Int
unInt :: Expr -> Maybe Int
unInt (ELit (LInt Int
i)) = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i
unInt (ETyped Expr
e Type
ty)   = Expr -> Maybe Int
unInt Expr
e
unInt (EImplArg Expr
e)    = Expr -> Maybe Int
unInt Expr
e
unInt Expr
_               = Maybe Int
forall a. Maybe a
Nothing

-- | Constructs an expression from real number literal

mkDouble :: Double -> Expr
mkDouble :: Double -> Expr
mkDouble Double
f = Literal -> Expr
ELit (Double -> Literal
LFlt Double
f)

-- | Decomposes an expression into real number literal

unDouble :: Expr -> Maybe Double
unDouble :: Expr -> Maybe Double
unDouble (ELit (LFlt Double
f)) = Double -> Maybe Double
forall a. a -> Maybe a
Just Double
f
unDouble (ETyped Expr
e Type
ty)   = Expr -> Maybe Double
unDouble Expr
e
unDouble (EImplArg Expr
e)    = Expr -> Maybe Double
unDouble Expr
e
unDouble Expr
_               = Maybe Double
forall a. Maybe a
Nothing

mkFloat :: Double -> Expr
mkFloat = Double -> Expr
mkDouble
unFloat :: Expr -> Maybe Double
unFloat = Expr -> Maybe Double
unDouble

-- | Constructs an expression which is meta variable

mkMeta :: Int -> Expr
mkMeta :: Int -> Expr
mkMeta Int
i = Int -> Expr
EMeta Int
i

-- | Checks whether an expression is a meta variable

unMeta :: Expr -> Maybe Int
unMeta :: Expr -> Maybe Int
unMeta (EMeta Int
i)     = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i
unMeta (ETyped Expr
e Type
ty) = Expr -> Maybe Int
unMeta Expr
e
unMeta (EImplArg Expr
e)  = Expr -> Maybe Int
unMeta Expr
e
unMeta Expr
_             = Maybe Int
forall a. Maybe a
Nothing

-----------------------------------------------------

-- Parsing

-----------------------------------------------------


pExpr :: RP.ReadP Expr
pExpr :: ReadP Expr
pExpr = ReadP ()
RP.skipSpaces ReadP () -> ReadP Expr -> ReadP Expr
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> (ReadP Expr
pAbs ReadP Expr -> ReadP Expr -> ReadP Expr
forall a. ReadP a -> ReadP a -> ReadP a
RP.<++ ReadP Expr
pTerm)
  where
    pTerm :: ReadP Expr
pTerm = do Expr
f <- ReadP Expr
pFactor
               ReadP ()
RP.skipSpaces
               [Expr]
as <- ReadP Expr -> ReadP () -> ReadP [Expr]
forall a sep. ReadP a -> ReadP sep -> ReadP [a]
RP.sepBy ReadP Expr
pArg ReadP ()
RP.skipSpaces
               Expr -> ReadP Expr
forall (m :: * -> *) a. Monad m => a -> m a
return ((Expr -> Expr -> Expr) -> Expr -> [Expr] -> Expr
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr -> Expr -> Expr
EApp Expr
f [Expr]
as)

    pAbs :: ReadP Expr
pAbs = do [(BindType, CId)]
xs <- ReadP Char
-> ReadP String
-> ReadP [(BindType, CId)]
-> ReadP [(BindType, CId)]
forall open close a.
ReadP open -> ReadP close -> ReadP a -> ReadP a
RP.between (Char -> ReadP Char
RP.char Char
'\\') (ReadP ()
RP.skipSpaces ReadP () -> ReadP String -> ReadP String
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> ReadP String
RP.string String
"->") ReadP [(BindType, CId)]
pBinds
              Expr
e  <- ReadP Expr
pExpr
              Expr -> ReadP Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (((BindType, CId) -> Expr -> Expr)
-> Expr -> [(BindType, CId)] -> Expr
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(BindType
b,CId
x) Expr
e -> BindType -> CId -> Expr -> Expr
EAbs BindType
b CId
x Expr
e) Expr
e [(BindType, CId)]
xs)

pBinds :: RP.ReadP [(BindType,CId)]
pBinds :: ReadP [(BindType, CId)]
pBinds = do [[(BindType, CId)]]
xss <- ReadP [(BindType, CId)] -> ReadP Char -> ReadP [[(BindType, CId)]]
forall a sep. ReadP a -> ReadP sep -> ReadP [a]
RP.sepBy1 (ReadP ()
RP.skipSpaces ReadP () -> ReadP [(BindType, CId)] -> ReadP [(BindType, CId)]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ReadP [(BindType, CId)]
pBind) (ReadP ()
RP.skipSpaces ReadP () -> ReadP Char -> ReadP Char
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> ReadP Char
RP.char Char
',')
            [(BindType, CId)] -> ReadP [(BindType, CId)]
forall (m :: * -> *) a. Monad m => a -> m a
return ([[(BindType, CId)]] -> [(BindType, CId)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[(BindType, CId)]]
xss)
  where
    pCIdOrWild :: ReadP CId
pCIdOrWild = ReadP CId
pCId ReadP CId -> ReadP CId -> ReadP CId
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus` (Char -> ReadP Char
RP.char Char
'_' ReadP Char -> ReadP CId -> ReadP CId
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> CId -> ReadP CId
forall (m :: * -> *) a. Monad m => a -> m a
return CId
wildCId)

    pBind :: ReadP [(BindType, CId)]
pBind = 
      do CId
x <- ReadP CId
pCIdOrWild
         [(BindType, CId)] -> ReadP [(BindType, CId)]
forall (m :: * -> *) a. Monad m => a -> m a
return [(BindType
Explicit,CId
x)]
      ReadP [(BindType, CId)]
-> ReadP [(BindType, CId)] -> ReadP [(BindType, CId)]
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus`
      ReadP Char
-> ReadP Char -> ReadP [(BindType, CId)] -> ReadP [(BindType, CId)]
forall open close a.
ReadP open -> ReadP close -> ReadP a -> ReadP a
RP.between (Char -> ReadP Char
RP.char Char
'{')
                 (ReadP ()
RP.skipSpaces ReadP () -> ReadP Char -> ReadP Char
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> ReadP Char
RP.char Char
'}')
                 (ReadP (BindType, CId) -> ReadP Char -> ReadP [(BindType, CId)]
forall a sep. ReadP a -> ReadP sep -> ReadP [a]
RP.sepBy1 (ReadP ()
RP.skipSpaces ReadP () -> ReadP CId -> ReadP CId
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ReadP CId
pCIdOrWild ReadP CId
-> (CId -> ReadP (BindType, CId)) -> ReadP (BindType, CId)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \CId
id -> (BindType, CId) -> ReadP (BindType, CId)
forall (m :: * -> *) a. Monad m => a -> m a
return (BindType
Implicit,CId
id)) (ReadP ()
RP.skipSpaces ReadP () -> ReadP Char -> ReadP Char
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> ReadP Char
RP.char Char
','))

pArg :: ReadP Expr
pArg = (Expr -> Expr) -> ReadP Expr -> ReadP Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Expr -> Expr
EImplArg (ReadP Char -> ReadP Char -> ReadP Expr -> ReadP Expr
forall open close a.
ReadP open -> ReadP close -> ReadP a -> ReadP a
RP.between (Char -> ReadP Char
RP.char Char
'{') (Char -> ReadP Char
RP.char Char
'}') ReadP Expr
pExpr)
       ReadP Expr -> ReadP Expr -> ReadP Expr
forall a. ReadP a -> ReadP a -> ReadP a
RP.<++
       ReadP Expr
pFactor

pFactor :: ReadP Expr
pFactor =       (CId -> Expr) -> ReadP CId -> ReadP Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CId -> Expr
EFun  ReadP CId
pCId
        ReadP Expr -> ReadP Expr -> ReadP Expr
forall a. ReadP a -> ReadP a -> ReadP a
RP.<++  (Literal -> Expr) -> ReadP Literal -> ReadP Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Literal -> Expr
ELit  ReadP Literal
pLit
        ReadP Expr -> ReadP Expr -> ReadP Expr
forall a. ReadP a -> ReadP a -> ReadP a
RP.<++  (Int -> Expr) -> ReadP Int -> ReadP Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Expr
EMeta ReadP Int
pMeta
        ReadP Expr -> ReadP Expr -> ReadP Expr
forall a. ReadP a -> ReadP a -> ReadP a
RP.<++  ReadP Char -> ReadP Char -> ReadP Expr -> ReadP Expr
forall open close a.
ReadP open -> ReadP close -> ReadP a -> ReadP a
RP.between (Char -> ReadP Char
RP.char Char
'(') (ReadP ()
RP.skipSpaces ReadP () -> ReadP Char -> ReadP Char
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> ReadP Char
RP.char Char
')') ReadP Expr
pExpr
        ReadP Expr -> ReadP Expr -> ReadP Expr
forall a. ReadP a -> ReadP a -> ReadP a
RP.<++  ReadP Char -> ReadP Char -> ReadP Expr -> ReadP Expr
forall open close a.
ReadP open -> ReadP close -> ReadP a -> ReadP a
RP.between (Char -> ReadP Char
RP.char Char
'<') (ReadP ()
RP.skipSpaces ReadP () -> ReadP Char -> ReadP Char
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Char -> ReadP Char
RP.char Char
'>') ReadP Expr
pTyped

pTyped :: ReadP Expr
pTyped = do ReadP ()
RP.skipSpaces
            Expr
e <- ReadP Expr
pExpr
            ReadP ()
RP.skipSpaces
            Char -> ReadP Char
RP.char Char
':'
            ReadP ()
RP.skipSpaces
            Type
ty <- ReadP Type
pType
            Expr -> ReadP Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Type -> Expr
ETyped Expr
e Type
ty)

pMeta :: ReadP Int
pMeta = do Char -> ReadP Char
RP.char Char
'?'
           String
ds <- (Char -> Bool) -> ReadP String
RP.munch Char -> Bool
isDigit
           Int -> ReadP Int
forall (m :: * -> *) a. Monad m => a -> m a
return (String -> Int
forall a. Read a => String -> a
read (Char
'0'Char -> ShowS
forall a. a -> [a] -> [a]
:String
ds))

pLit :: RP.ReadP Literal
pLit :: ReadP Literal
pLit = (String -> Literal) -> ReadP String -> ReadP Literal
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM String -> Literal
LStr (ReadS String -> ReadP String
forall a. ReadS a -> ReadP a
RP.readS_to_P ReadS String
forall a. Read a => ReadS a
reads)
       ReadP Literal -> ReadP Literal -> ReadP Literal
forall a. ReadP a -> ReadP a -> ReadP a
RP.<++
       (Int -> Literal) -> ReadP Int -> ReadP Literal
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Int -> Literal
LInt (ReadS Int -> ReadP Int
forall a. ReadS a -> ReadP a
RP.readS_to_P ReadS Int
forall a. Read a => ReadS a
reads)
       ReadP Literal -> ReadP Literal -> ReadP Literal
forall a. ReadP a -> ReadP a -> ReadP a
RP.<++
       (Double -> Literal) -> ReadP Double -> ReadP Literal
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM Double -> Literal
LFlt (ReadS Double -> ReadP Double
forall a. ReadS a -> ReadP a
RP.readS_to_P ReadS Double
forall a. Read a => ReadS a
reads)


-----------------------------------------------------

-- Printing

-----------------------------------------------------


ppExpr :: Int -> [CId] -> Expr -> PP.Doc
ppExpr :: Int -> [CId] -> Expr -> Doc
ppExpr Int
d [CId]
scope (EAbs BindType
b CId
x Expr
e) = let ([BindType]
bs,[CId]
xs,Expr
e1) = [BindType] -> [CId] -> Expr -> ([BindType], [CId], Expr)
getVars [] [] (BindType -> CId -> Expr -> Expr
EAbs BindType
b CId
x Expr
e)
                              in Bool -> Doc -> Doc
ppParens (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1) (Char -> Doc
PP.char Char
'\\' Doc -> Doc -> Doc
PP.<>
                                                   [Doc] -> Doc
PP.hsep (Doc -> [Doc] -> [Doc]
PP.punctuate Doc
PP.comma ([Doc] -> [Doc]
forall a. [a] -> [a]
reverse ((BindType -> CId -> Doc) -> [BindType] -> [CId] -> [Doc]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
List.zipWith BindType -> CId -> Doc
ppBind [BindType]
bs [CId]
xs))) Doc -> Doc -> Doc
PP.<+>
                                                   String -> Doc
PP.text String
"->" Doc -> Doc -> Doc
PP.<+>
                                                   Int -> [CId] -> Expr -> Doc
ppExpr Int
1 ([CId]
xs[CId] -> [CId] -> [CId]
forall a. [a] -> [a] -> [a]
++[CId]
scope) Expr
e1)
                              where
                                getVars :: [BindType] -> [CId] -> Expr -> ([BindType], [CId], Expr)
getVars [BindType]
bs [CId]
xs (EAbs BindType
b CId
x Expr
e) = [BindType] -> [CId] -> Expr -> ([BindType], [CId], Expr)
getVars (BindType
bBindType -> [BindType] -> [BindType]
forall a. a -> [a] -> [a]
:[BindType]
bs) ((CId -> [CId] -> CId
freshName CId
x [CId]
xs)CId -> [CId] -> [CId]
forall a. a -> [a] -> [a]
:[CId]
xs) Expr
e
                                getVars [BindType]
bs [CId]
xs Expr
e            = ([BindType]
bs,[CId]
xs,Expr
e)
ppExpr Int
d [CId]
scope (EApp Expr
e1 Expr
e2) = Bool -> Doc -> Doc
ppParens (Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
3) ((Int -> [CId] -> Expr -> Doc
ppExpr Int
3 [CId]
scope Expr
e1) Doc -> Doc -> Doc
PP.<+> (Int -> [CId] -> Expr -> Doc
ppExpr Int
4 [CId]
scope Expr
e2))
ppExpr Int
d [CId]
scope (ELit Literal
l)     = Literal -> Doc
ppLit Literal
l
ppExpr Int
d [CId]
scope (EMeta Int
n)    = Int -> Doc
ppMeta Int
n
ppExpr Int
d [CId]
scope (EFun CId
f)     = CId -> Doc
ppCId CId
f
ppExpr Int
d [CId]
scope (EVar Int
i)     = CId -> Doc
ppCId ([CId]
scope [CId] -> Int -> CId
forall a. [a] -> Int -> a
!! Int
i)
ppExpr Int
d [CId]
scope (ETyped Expr
e Type
ty)= Char -> Doc
PP.char Char
'<' Doc -> Doc -> Doc
PP.<> Int -> [CId] -> Expr -> Doc
ppExpr Int
0 [CId]
scope Expr
e Doc -> Doc -> Doc
PP.<+> Doc
PP.colon Doc -> Doc -> Doc
PP.<+> Int -> [CId] -> Type -> Doc
ppType Int
0 [CId]
scope Type
ty Doc -> Doc -> Doc
PP.<> Char -> Doc
PP.char Char
'>'
ppExpr Int
d [CId]
scope (EImplArg Expr
e) = Doc -> Doc
PP.braces (Int -> [CId] -> Expr -> Doc
ppExpr Int
0 [CId]
scope Expr
e)

ppPatt :: Int -> [CId] -> Patt -> PP.Doc
ppPatt :: Int -> [CId] -> Patt -> Doc
ppPatt Int
d [CId]
scope (PApp CId
f [Patt]
ps)  = let ds :: [Doc]
ds = (Patt -> Doc) -> [Patt] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
List.map (Int -> [CId] -> Patt -> Doc
ppPatt Int
2 [CId]
scope) [Patt]
ps
                              in Bool -> Doc -> Doc
ppParens (Bool -> Bool
not ([Patt] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
List.null [Patt]
ps) Bool -> Bool -> Bool
&& Int
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1) (CId -> Doc
ppCId CId
f Doc -> Doc -> Doc
PP.<+> [Doc] -> Doc
PP.hsep [Doc]
ds)
ppPatt Int
d [CId]
scope (PLit Literal
l)     = Literal -> Doc
ppLit Literal
l
ppPatt Int
d [CId]
scope (PVar CId
f)     = CId -> Doc
ppCId CId
f
ppPatt Int
d [CId]
scope (PAs CId
x Patt
p)    = CId -> Doc
ppCId CId
x Doc -> Doc -> Doc
PP.<> Char -> Doc
PP.char Char
'@' Doc -> Doc -> Doc
PP.<> Int -> [CId] -> Patt -> Doc
ppPatt Int
3 [CId]
scope Patt
p
ppPatt Int
d [CId]
scope Patt
PWild        = Char -> Doc
PP.char Char
'_'
ppPatt Int
d [CId]
scope (PImplArg Patt
p) = Doc -> Doc
PP.braces (Int -> [CId] -> Patt -> Doc
ppPatt Int
0 [CId]
scope Patt
p)
ppPatt Int
d [CId]
scope (PTilde Expr
e)   = Char -> Doc
PP.char Char
'~' Doc -> Doc -> Doc
PP.<> Int -> [CId] -> Expr -> Doc
ppExpr Int
6 [CId]
scope Expr
e

pattScope :: [CId] -> Patt -> [CId]
pattScope :: [CId] -> Patt -> [CId]
pattScope [CId]
scope (PApp CId
f [Patt]
ps)  = ([CId] -> Patt -> [CId]) -> [CId] -> [Patt] -> [CId]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl [CId] -> Patt -> [CId]
pattScope [CId]
scope [Patt]
ps
pattScope [CId]
scope (PLit Literal
l)     = [CId]
scope
pattScope [CId]
scope (PVar CId
f)     = CId
fCId -> [CId] -> [CId]
forall a. a -> [a] -> [a]
:[CId]
scope
pattScope [CId]
scope (PAs CId
x Patt
p)    = [CId] -> Patt -> [CId]
pattScope (CId
xCId -> [CId] -> [CId]
forall a. a -> [a] -> [a]
:[CId]
scope) Patt
p
pattScope [CId]
scope Patt
PWild        = [CId]
scope
pattScope [CId]
scope (PImplArg Patt
p) = [CId] -> Patt -> [CId]
pattScope [CId]
scope Patt
p                               
pattScope [CId]
scope (PTilde Expr
e)   = [CId]
scope

ppBind :: BindType -> CId -> Doc
ppBind BindType
Explicit CId
x = CId -> Doc
ppCId CId
x
ppBind BindType
Implicit CId
x = Doc -> Doc
PP.braces (CId -> Doc
ppCId CId
x)

ppMeta :: MetaId -> PP.Doc
ppMeta :: Int -> Doc
ppMeta Int
n
  | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0    = Char -> Doc
PP.char Char
'?'
  | Bool
otherwise = Char -> Doc
PP.char Char
'?' Doc -> Doc -> Doc
PP.<> Int -> Doc
PP.int Int
n

ppParens :: Bool -> Doc -> Doc
ppParens Bool
True  = Doc -> Doc
PP.parens
ppParens Bool
False = Doc -> Doc
forall a. a -> a
id

freshName :: CId -> [CId] -> CId
freshName :: CId -> [CId] -> CId
freshName CId
x [CId]
xs0 = Integer -> CId -> CId
forall a. (Num a, Show a) => a -> CId -> CId
loop Integer
1 CId
x
  where
    xs :: [CId]
xs = CId
wildCId CId -> [CId] -> [CId]
forall a. a -> [a] -> [a]
: [CId]
xs0

    loop :: a -> CId -> CId
loop a
i CId
y
      | CId -> [CId] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem CId
y [CId]
xs = a -> CId -> CId
loop (a
ia -> a -> a
forall a. Num a => a -> a -> a
+a
1) (String -> CId
mkCId (CId -> String
forall a. Show a => a -> String
show CId
xString -> ShowS
forall a. [a] -> [a] -> [a]
++a -> String
forall a. Show a => a -> String
show a
i))
      | Bool
otherwise = CId
y


-----------------------------------------------------

-- Computation

-----------------------------------------------------


-- | Compute an expression to normal form

normalForm :: Sig -> Int -> Env -> Expr -> Expr
normalForm :: Sig -> Int -> Env -> Expr -> Expr
normalForm Sig
sig Int
k Env
env Expr
e = Sig -> Int -> Value -> Expr
value2expr Sig
sig Int
k (Sig -> Env -> Expr -> Value
eval Sig
sig Env
env Expr
e)

value2expr :: Sig -> Int -> Value -> Expr
value2expr Sig
sig Int
i (VApp CId
f Env
vs)                 = (Expr -> Expr -> Expr) -> Expr -> [Expr] -> Expr
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr -> Expr -> Expr
EApp (CId -> Expr
EFun CId
f)       ((Value -> Expr) -> Env -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
List.map (Sig -> Int -> Value -> Expr
value2expr Sig
sig Int
i) Env
vs)
value2expr Sig
sig Int
i (VGen Int
j Env
vs)                 = (Expr -> Expr -> Expr) -> Expr -> [Expr] -> Expr
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr -> Expr -> Expr
EApp (Int -> Expr
EVar (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
jInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)) ((Value -> Expr) -> Env -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
List.map (Sig -> Int -> Value -> Expr
value2expr Sig
sig Int
i) Env
vs)
value2expr Sig
sig Int
i (VMeta Int
j Env
env Env
vs)            = case Sig -> Int -> Maybe Expr
forall a b. (a, b) -> b
snd Sig
sig Int
j of
                                                 Just Expr
e  -> Sig -> Int -> Value -> Expr
value2expr Sig
sig Int
i (Sig -> Env -> Expr -> Env -> Value
apply Sig
sig Env
env Expr
e Env
vs)
                                                 Maybe Expr
Nothing -> (Expr -> Expr -> Expr) -> Expr -> [Expr] -> Expr
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr -> Expr -> Expr
EApp (Int -> Expr
EMeta Int
j) ((Value -> Expr) -> Env -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
List.map (Sig -> Int -> Value -> Expr
value2expr Sig
sig Int
i) Env
vs)
value2expr Sig
sig Int
i (VSusp Int
j Env
env Env
vs Value -> Value
k)          = Sig -> Int -> Value -> Expr
value2expr Sig
sig Int
i (Value -> Value
k (Int -> Env -> Value
VGen Int
j Env
vs))
value2expr Sig
sig Int
i (VConst CId
f Env
vs)               = (Expr -> Expr -> Expr) -> Expr -> [Expr] -> Expr
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Expr -> Expr -> Expr
EApp (CId -> Expr
EFun CId
f)       ((Value -> Expr) -> Env -> [Expr]
forall a b. (a -> b) -> [a] -> [b]
List.map (Sig -> Int -> Value -> Expr
value2expr Sig
sig Int
i) Env
vs)
value2expr Sig
sig Int
i (VLit Literal
l)                    = Literal -> Expr
ELit Literal
l
value2expr Sig
sig Int
i (VClosure Env
env (EAbs BindType
b CId
x Expr
e)) = BindType -> CId -> Expr -> Expr
EAbs BindType
b (String -> CId
mkCId (Char
'v'Char -> ShowS
forall a. a -> [a] -> [a]
:Int -> String
forall a. Show a => a -> String
show Int
i)) (Sig -> Int -> Value -> Expr
value2expr Sig
sig (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) (Sig -> Env -> Expr -> Value
eval Sig
sig ((Int -> Env -> Value
VGen Int
i [])Value -> Env -> Env
forall a. a -> [a] -> [a]
:Env
env) Expr
e))
value2expr Sig
sig Int
i (VImplArg Value
v)                = Expr -> Expr
EImplArg (Sig -> Int -> Value -> Expr
value2expr Sig
sig Int
i Value
v)

data Value
  = VApp CId [Value]
  | VLit Literal
  | VMeta {-# UNPACK #-} !MetaId Env [Value]
  | VSusp {-# UNPACK #-} !MetaId Env [Value] (Value -> Value)
  | VGen  {-# UNPACK #-} !Int [Value]
  | VConst CId [Value]
  | VClosure Env Expr
  | VImplArg Value

type Sig = ( Map.Map CId (Type,Int,Maybe ([Equation],[[Instr]]),Double) -- type and def of a fun

           , Int -> Maybe Expr                                          -- lookup for metavariables

           )
type Env = [Value]

eval :: Sig -> Env -> Expr -> Value
eval :: Sig -> Env -> Expr -> Value
eval Sig
sig Env
env (EVar Int
i)     = Env
env Env -> Int -> Value
forall a. [a] -> Int -> a
!! Int
i
eval Sig
sig Env
env (EFun CId
f)     = case CId
-> Map CId (Type, Int, Maybe ([Equation], [[Instr]]), Double)
-> Maybe (Type, Int, Maybe ([Equation], [[Instr]]), Double)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup CId
f (Sig -> Map CId (Type, Int, Maybe ([Equation], [[Instr]]), Double)
forall a b. (a, b) -> a
fst Sig
sig) of
                              Just (Type
_,Int
a,Maybe ([Equation], [[Instr]])
meqs,Double
_) -> case Maybe ([Equation], [[Instr]])
meqs of
                                                       Just ([Equation]
eqs,[[Instr]]
_)
                                                               -> if Int
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
                                                                    then case [Equation]
eqs of
                                                                           Equ [] Expr
e : [Equation]
_ -> Sig -> Env -> Expr -> Value
eval Sig
sig [] Expr
e
                                                                           [Equation]
_            -> CId -> Env -> Value
VConst CId
f []
                                                                    else CId -> Env -> Value
VApp CId
f []
                                                       Maybe ([Equation], [[Instr]])
Nothing -> CId -> Env -> Value
VApp CId
f []
                              Maybe (Type, Int, Maybe ([Equation], [[Instr]]), Double)
Nothing             -> String -> Value
forall a. HasCallStack => String -> a
error (String
"unknown function "String -> ShowS
forall a. [a] -> [a] -> [a]
++CId -> String
showCId CId
f)
eval Sig
sig Env
env (EApp Expr
e1 Expr
e2) = Sig -> Env -> Expr -> Env -> Value
apply Sig
sig Env
env Expr
e1 [Sig -> Env -> Expr -> Value
eval Sig
sig Env
env Expr
e2]
eval Sig
sig Env
env (EAbs BindType
b CId
x Expr
e) = Env -> Expr -> Value
VClosure Env
env (BindType -> CId -> Expr -> Expr
EAbs BindType
b CId
x Expr
e)
eval Sig
sig Env
env (EMeta Int
i)    = case Sig -> Int -> Maybe Expr
forall a b. (a, b) -> b
snd Sig
sig Int
i of
                              Just Expr
e  -> Sig -> Env -> Expr -> Value
eval Sig
sig Env
env Expr
e
                              Maybe Expr
Nothing -> Int -> Env -> Env -> Value
VMeta Int
i Env
env []
eval Sig
sig Env
env (ELit Literal
l)     = Literal -> Value
VLit Literal
l
eval Sig
sig Env
env (ETyped Expr
e Type
_) = Sig -> Env -> Expr -> Value
eval Sig
sig Env
env Expr
e
eval Sig
sig Env
env (EImplArg Expr
e) = Value -> Value
VImplArg (Sig -> Env -> Expr -> Value
eval Sig
sig Env
env Expr
e)

apply :: Sig -> Env -> Expr -> [Value] -> Value
apply :: Sig -> Env -> Expr -> Env -> Value
apply Sig
sig Env
env Expr
e            []     = Sig -> Env -> Expr -> Value
eval Sig
sig Env
env Expr
e
apply Sig
sig Env
env (EVar Int
i)     Env
vs     = Sig -> Value -> Env -> Value
applyValue Sig
sig (Env
env Env -> Int -> Value
forall a. [a] -> Int -> a
!! Int
i) Env
vs
apply Sig
sig Env
env (EFun CId
f)     Env
vs     = case CId
-> Map CId (Type, Int, Maybe ([Equation], [[Instr]]), Double)
-> Maybe (Type, Int, Maybe ([Equation], [[Instr]]), Double)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup CId
f (Sig -> Map CId (Type, Int, Maybe ([Equation], [[Instr]]), Double)
forall a b. (a, b) -> a
fst Sig
sig) of
                                      Just (Type
_,Int
a,Maybe ([Equation], [[Instr]])
meqs,Double
_) -> case Maybe ([Equation], [[Instr]])
meqs of
                                                             Just ([Equation]
eqs,[[Instr]]
_) -> if Int
a Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Env -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Env
vs
                                                                               then Sig -> CId -> [Equation] -> Env -> Value
match Sig
sig CId
f [Equation]
eqs Env
vs
                                                                               else CId -> Env -> Value
VApp CId
f Env
vs
                                                             Maybe ([Equation], [[Instr]])
Nothing      -> CId -> Env -> Value
VApp CId
f Env
vs
                                      Maybe (Type, Int, Maybe ([Equation], [[Instr]]), Double)
Nothing           -> String -> Value
forall a. HasCallStack => String -> a
error (String
"unknown function "String -> ShowS
forall a. [a] -> [a] -> [a]
++CId -> String
showCId CId
f)
apply Sig
sig Env
env (EApp Expr
e1 Expr
e2) Env
vs     = Sig -> Env -> Expr -> Env -> Value
apply Sig
sig Env
env Expr
e1 (Sig -> Env -> Expr -> Value
eval Sig
sig Env
env Expr
e2 Value -> Env -> Env
forall a. a -> [a] -> [a]
: Env
vs)
apply Sig
sig Env
env (EAbs BindType
b CId
x Expr
e) (Value
v:Env
vs) = case (BindType
b,Value
v) of
                                      (BindType
Implicit,VImplArg Value
v) -> Sig -> Env -> Expr -> Env -> Value
apply Sig
sig (Value
vValue -> Env -> Env
forall a. a -> [a] -> [a]
:Env
env) Expr
e Env
vs
                                      (BindType
Explicit,         Value
v) -> Sig -> Env -> Expr -> Env -> Value
apply Sig
sig (Value
vValue -> Env -> Env
forall a. a -> [a] -> [a]
:Env
env) Expr
e Env
vs
apply Sig
sig Env
env (EMeta Int
i)    Env
vs     = case Sig -> Int -> Maybe Expr
forall a b. (a, b) -> b
snd Sig
sig Int
i of
                                      Just Expr
e  -> Sig -> Env -> Expr -> Env -> Value
apply Sig
sig Env
env Expr
e Env
vs
                                      Maybe Expr
Nothing -> Int -> Env -> Env -> Value
VMeta Int
i Env
env Env
vs
apply Sig
sig Env
env (ELit Literal
l)     Env
vs     = String -> Value
forall a. HasCallStack => String -> a
error String
"literal of function type"
apply Sig
sig Env
env (ETyped Expr
e Type
_) Env
vs     = Sig -> Env -> Expr -> Env -> Value
apply Sig
sig Env
env Expr
e Env
vs
apply Sig
sig Env
env (EImplArg Expr
_) Env
vs     = String -> Value
forall a. HasCallStack => String -> a
error String
"implicit argument in function position"

applyValue :: Sig -> Value -> Env -> Value
applyValue Sig
sig Value
v                         []       = Value
v
applyValue Sig
sig (VApp CId
f  Env
vs0)             Env
vs       = Sig -> Env -> Expr -> Env -> Value
apply Sig
sig [] (CId -> Expr
EFun CId
f) (Env
vs0Env -> Env -> Env
forall a. [a] -> [a] -> [a]
++Env
vs)
applyValue Sig
sig (VLit Literal
_)                  Env
vs       = String -> Value
forall a. HasCallStack => String -> a
error String
"literal of function type"
applyValue Sig
sig (VMeta Int
i Env
env Env
vs0)         Env
vs       = Int -> Env -> Env -> Value
VMeta Int
i Env
env (Env
vs0Env -> Env -> Env
forall a. [a] -> [a] -> [a]
++Env
vs)
applyValue Sig
sig (VGen  Int
i Env
vs0)             Env
vs       = Int -> Env -> Value
VGen  Int
i (Env
vs0Env -> Env -> Env
forall a. [a] -> [a] -> [a]
++Env
vs)
applyValue Sig
sig (VSusp Int
i Env
env Env
vs0 Value -> Value
k)       Env
vs       = Int -> Env -> Env -> (Value -> Value) -> Value
VSusp Int
i Env
env Env
vs0 (\Value
v -> Sig -> Value -> Env -> Value
applyValue Sig
sig (Value -> Value
k Value
v) Env
vs)
applyValue Sig
sig (VConst CId
f Env
vs0)            Env
vs       = CId -> Env -> Value
VConst CId
f (Env
vs0Env -> Env -> Env
forall a. [a] -> [a] -> [a]
++Env
vs)
applyValue Sig
sig (VClosure Env
env (EAbs BindType
b CId
x Expr
e)) (Value
v:Env
vs) = case (BindType
b,Value
v) of
                                                      (BindType
Implicit,VImplArg Value
v) -> Sig -> Env -> Expr -> Env -> Value
apply Sig
sig (Value
vValue -> Env -> Env
forall a. a -> [a] -> [a]
:Env
env) Expr
e Env
vs
                                                      (BindType
Explicit,         Value
v) -> Sig -> Env -> Expr -> Env -> Value
apply Sig
sig (Value
vValue -> Env -> Env
forall a. a -> [a] -> [a]
:Env
env) Expr
e Env
vs
applyValue Sig
sig (VImplArg Value
_)              Env
vs       = String -> Value
forall a. HasCallStack => String -> a
error String
"implicit argument in function position"

-----------------------------------------------------

-- Pattern matching

-----------------------------------------------------


match :: Sig -> CId -> [Equation] -> [Value] -> Value
match :: Sig -> CId -> [Equation] -> Env -> Value
match Sig
sig CId
f [Equation]
eqs Env
as0 =
  case [Equation]
eqs of
    []               -> CId -> Env -> Value
VConst CId
f Env
as0
    (Equ [Patt]
ps Expr
res):[Equation]
eqs -> [Equation] -> [Patt] -> Env -> Expr -> Env -> Value
tryMatches [Equation]
eqs [Patt]
ps Env
as0 Expr
res []
  where
    tryMatches :: [Equation] -> [Patt] -> Env -> Expr -> Env -> Value
tryMatches [Equation]
eqs []     Env
as     Expr
res Env
env = Sig -> Env -> Expr -> Env -> Value
apply Sig
sig Env
env Expr
res Env
as
    tryMatches [Equation]
eqs (Patt
p:[Patt]
ps) (Value
a:Env
as) Expr
res Env
env = Patt -> Value -> Env -> Value
tryMatch Patt
p Value
a Env
env
      where
        tryMatch :: Patt -> Value -> Env -> Value
tryMatch (PVar CId
x     ) (Value
v                ) Env
env            = [Equation] -> [Patt] -> Env -> Expr -> Env -> Value
tryMatches [Equation]
eqs  [Patt]
ps        Env
as  Expr
res (Value
vValue -> Env -> Env
forall a. a -> [a] -> [a]
:Env
env)
        tryMatch (PAs  CId
x Patt
p   ) (Value
v                ) Env
env            = Patt -> Value -> Env -> Value
tryMatch Patt
p Value
v (Value
vValue -> Env -> Env
forall a. a -> [a] -> [a]
:Env
env)
        tryMatch (Patt
PWild      ) (Value
_                ) Env
env            = [Equation] -> [Patt] -> Env -> Expr -> Env -> Value
tryMatches [Equation]
eqs  [Patt]
ps        Env
as  Expr
res Env
env
        tryMatch (Patt
p          ) (VMeta Int
i Env
envi Env
vs  ) Env
env            = Int -> Env -> Env -> (Value -> Value) -> Value
VSusp Int
i Env
envi Env
vs (\Value
v -> Patt -> Value -> Env -> Value
tryMatch Patt
p Value
v Env
env)
        tryMatch (Patt
p          ) (VGen  Int
i Env
vs       ) Env
env            = CId -> Env -> Value
VConst CId
f Env
as0
        tryMatch (Patt
p          ) (VSusp Int
i Env
envi Env
vs Value -> Value
k) Env
env            = Int -> Env -> Env -> (Value -> Value) -> Value
VSusp Int
i Env
envi Env
vs (\Value
v -> Patt -> Value -> Env -> Value
tryMatch Patt
p (Value -> Value
k Value
v) Env
env)
        tryMatch (Patt
p          ) v :: Value
v@(VConst CId
_ Env
_     ) Env
env            = CId -> Env -> Value
VConst CId
f Env
as0
        tryMatch (PApp CId
f1 [Patt]
ps1) (VApp CId
f2 Env
vs2      ) Env
env | CId
f1 CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
== CId
f2 = [Equation] -> [Patt] -> Env -> Expr -> Env -> Value
tryMatches [Equation]
eqs ([Patt]
ps1[Patt] -> [Patt] -> [Patt]
forall a. [a] -> [a] -> [a]
++[Patt]
ps) (Env
vs2Env -> Env -> Env
forall a. [a] -> [a] -> [a]
++Env
as) Expr
res Env
env
        tryMatch (PLit Literal
l1    ) (VLit Literal
l2          ) Env
env | Literal
l1 Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
== Literal
l2 = [Equation] -> [Patt] -> Env -> Expr -> Env -> Value
tryMatches [Equation]
eqs  [Patt]
ps        Env
as  Expr
res Env
env
        tryMatch (PImplArg Patt
p ) (VImplArg Value
v       ) Env
env            = Patt -> Value -> Env -> Value
tryMatch Patt
p Value
v Env
env
        tryMatch (PTilde Expr
_   ) (Value
_                ) Env
env            = [Equation] -> [Patt] -> Env -> Expr -> Env -> Value
tryMatches [Equation]
eqs  [Patt]
ps        Env
as  Expr
res Env
env
        tryMatch Patt
_             Value
_                   Env
env            = Sig -> CId -> [Equation] -> Env -> Value
match Sig
sig CId
f [Equation]
eqs Env
as0