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,
Value(..), Env, Sig, eval, apply, applyValue, value2expr,
MetaId,
pMeta,pArg,pLit,freshName,ppMeta,ppLit,ppParens
) where
import PGF.CId
import PGF.Type
import PGF.ByteCode
import Data.Char
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)
type Tree = Expr
data Expr =
EAbs BindType CId Expr
| EApp Expr Expr
| ELit Literal
| EMeta {-# UNPACK #-} !MetaId
| EFun CId
| EVar {-# UNPACK #-} !Int
| ETyped Expr Type
| EImplArg Expr
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)
data Patt =
PApp CId [Patt]
| PLit Literal
| PVar CId
| PAs CId Patt
| PWild
| PImplArg Patt
| 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
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
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
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
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
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
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)
mkStr :: String -> Expr
mkStr :: String -> Expr
mkStr String
s = Literal -> Expr
ELit (String -> Literal
LStr String
s)
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
mkInt :: Int -> Expr
mkInt :: Int -> Expr
mkInt Int
i = Literal -> Expr
ELit (Int -> Literal
LInt Int
i)
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
mkDouble :: Double -> Expr
mkDouble :: Double -> Expr
mkDouble Double
f = Literal -> Expr
ELit (Double -> Literal
LFlt Double
f)
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
mkMeta :: Int -> Expr
mkMeta :: Int -> Expr
mkMeta Int
i = Int -> Expr
EMeta Int
i
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
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)
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
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)
, Int -> Maybe Expr
)
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"
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