{-# LANGUAGE TypeSynonymInstances #-}
module PGF.Forest( Forest(..)
, BracketedString, showBracketedString, lengthBracketedString
, linearizeWithBrackets
, getAbsTrees
) where
import PGF.CId
import PGF.Data
import PGF.Macros
import PGF.TypeCheck
import PGF.Generate
import Data.List
import Data.Array.IArray
import qualified Data.Set as Set
import qualified Data.Map as Map
import qualified Data.IntSet as IntSet
import qualified Data.IntMap as IntMap
import Control.Monad
import Control.Monad.State
import PGF.Utilities (nub')
import qualified Data.ByteString.UTF8 as UTF8
data Forest
= Forest
{ Forest -> Abstr
abstr :: Abstr
, Forest -> Concr
concr :: Concr
, Forest -> IntMap (Set Production)
forest :: IntMap.IntMap (Set.Set Production)
, Forest -> [([Symbol], [PArg])]
root :: [([Symbol],[PArg])]
}
linearizeWithBrackets :: Maybe Int -> Forest -> BracketedString
linearizeWithBrackets :: Maybe Int -> Forest -> BracketedString
linearizeWithBrackets Maybe Int
dp = [BracketedString] -> BracketedString
forall a. [a] -> a
head ([BracketedString] -> BracketedString)
-> (Forest -> [BracketedString]) -> Forest -> BracketedString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe String, [BracketedString]) -> [BracketedString]
forall a b. (a, b) -> b
snd ((Maybe String, [BracketedString]) -> [BracketedString])
-> (Forest -> (Maybe String, [BracketedString]))
-> Forest
-> [BracketedString]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe String
-> [BracketedTokn] -> (Maybe String, [BracketedString])
untokn Maybe String
forall a. Maybe a
Nothing ([BracketedTokn] -> (Maybe String, [BracketedString]))
-> (Forest -> [BracketedTokn])
-> Forest
-> (Maybe String, [BracketedString])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (BracketedTokn -> [BracketedTokn] -> [BracketedTokn]
forall a. a -> [a] -> [a]
:[]) (BracketedTokn -> [BracketedTokn])
-> (Forest -> BracketedTokn) -> Forest -> [BracketedTokn]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.Maybe Int -> Forest -> BracketedTokn
bracketedTokn Maybe Int
dp
bracketedTokn :: Maybe Int -> Forest -> BracketedTokn
bracketedTokn :: Maybe Int -> Forest -> BracketedTokn
bracketedTokn Maybe Int
dp f :: Forest
f@(Forest Abstr
abs Concr
cnc IntMap (Set Production)
forest [([Symbol], [PArg])]
root) =
case [(CncType -> Bool)
-> [Symbol]
-> [(CncType, Int, CId, [Expr], LinTable)]
-> [BracketedTokn]
computeSeq CncType -> Bool
forall a. (a, Int) -> Bool
isTrusted [Symbol]
seq ((PArg -> (CncType, Int, CId, [Expr], LinTable))
-> [PArg] -> [(CncType, Int, CId, [Expr], LinTable)]
forall a b. (a -> b) -> [a] -> [b]
map (IntMap (Set Production)
-> PArg -> (CncType, Int, CId, [Expr], LinTable)
render IntMap (Set Production)
forest) [PArg]
args) | ([Symbol]
seq,[PArg]
args) <- [([Symbol], [PArg])]
root] of
([bs :: BracketedTokn
bs@(Bracket_{})]:[[BracketedTokn]]
_) -> BracketedTokn
bs
([BracketedTokn]
bss:[[BracketedTokn]]
_) -> CId
-> Int
-> Int
-> Int
-> CId
-> [Expr]
-> [BracketedTokn]
-> BracketedTokn
Bracket_ CId
wildCId Int
0 Int
0 Int
0 CId
wildCId [] [BracketedTokn]
bss
[] -> CId
-> Int
-> Int
-> Int
-> CId
-> [Expr]
-> [BracketedTokn]
-> BracketedTokn
Bracket_ CId
wildCId Int
0 Int
0 Int
0 CId
wildCId [] []
where
isTrusted :: (a, Int) -> Bool
isTrusted (a
_,Int
fid) = Int -> IntSet -> Bool
IntSet.member Int
fid IntSet
trusted
trusted :: IntSet
trusted = (IntSet -> IntSet -> IntSet) -> [IntSet] -> IntSet
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 IntSet -> IntSet -> IntSet
IntSet.intersection [[IntSet] -> IntSet
forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions ((PArg -> IntSet) -> [PArg] -> [IntSet]
forall a b. (a -> b) -> [a] -> [b]
map (IntSet -> PArg -> IntSet
trustedSpots IntSet
IntSet.empty) [PArg]
args) | ([Symbol]
_,[PArg]
args) <- [([Symbol], [PArg])]
root]
render :: IntMap (Set Production)
-> PArg -> (CncType, Int, CId, [Expr], LinTable)
render IntMap (Set Production)
forest arg :: PArg
arg@(PArg [(Int, Int)]
hypos Int
fid) =
case Int -> IntMap (Set Production) -> Maybe (Set Production)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
fid IntMap (Set Production)
forest Maybe (Set Production)
-> (Set Production -> Maybe (Production, Set Production))
-> Maybe (Production, Set Production)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Set Production -> Maybe (Production, Set Production)
forall a. Set a -> Maybe (a, Set a)
Set.maxView of
Just (Production
p,Set Production
set) -> let (CncType
ct,Int
fid',CId
fun,[Expr]
es,([CId]
_,Array Int [BracketedTokn]
lin)) = IntMap (Set Production)
-> Production -> (CncType, Int, CId, [Expr], LinTable)
descend (if Set Production -> Bool
forall a. Set a -> Bool
Set.null Set Production
set then IntMap (Set Production)
forest else Int
-> Set Production
-> IntMap (Set Production)
-> IntMap (Set Production)
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
fid Set Production
set IntMap (Set Production)
forest) Production
p
in (CncType
ct,Int
fid',CId
fun,[Expr]
es,(((Int, Int) -> CId) -> [(Int, Int)] -> [CId]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Int) -> CId
forall b. (Int, b) -> CId
getVar [(Int, Int)]
hypos,Array Int [BracketedTokn]
lin))
Maybe (Production, Set Production)
Nothing -> String -> (CncType, Int, CId, [Expr], LinTable)
forall a. HasCallStack => String -> a
error (String
"wrong forest id " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
fid)
where
descend :: IntMap (Set Production)
-> Production -> (CncType, Int, CId, [Expr], LinTable)
descend IntMap (Set Production)
forest (PApply Int
funid [PArg]
args) = let (CncFun CId
fun UArray Int Int
_lins) = Concr -> Array Int CncFun
cncfuns Concr
cnc Array Int CncFun -> Int -> CncFun
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Int
funid
cat :: CId
cat = case CId -> Maybe CId
isLindefCId CId
fun of
Just CId
cat -> CId
cat
Maybe CId
Nothing -> 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
fun (Abstr -> Map CId (Type, Int, Maybe ([Equation], [[Instr]]), Double)
funs Abstr
abs) of
Just (DTyp [Hypo]
_ CId
cat [Expr]
_,Int
_,Maybe ([Equation], [[Instr]])
_,Double
_) -> CId
cat
largs :: [(CncType, Int, CId, [Expr], LinTable)]
largs = (PArg -> (CncType, Int, CId, [Expr], LinTable))
-> [PArg] -> [(CncType, Int, CId, [Expr], LinTable)]
forall a b. (a -> b) -> [a] -> [b]
map (IntMap (Set Production)
-> PArg -> (CncType, Int, CId, [Expr], LinTable)
render IntMap (Set Production)
forest) [PArg]
args
ltable :: LinTable
ltable = Concr
-> (CncType -> Bool)
-> [CId]
-> Int
-> [(CncType, Int, CId, [Expr], LinTable)]
-> LinTable
mkLinTable Concr
cnc CncType -> Bool
forall a. (a, Int) -> Bool
isTrusted [] Int
funid [(CncType, Int, CId, [Expr], LinTable)]
largs
in ((CId
cat,Int
fid),Int
0,CId
wildCId,([(Int, TcError)] -> [Expr])
-> ([Expr] -> [Expr]) -> Either [(Int, TcError)] [Expr] -> [Expr]
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ([Expr] -> [(Int, TcError)] -> [Expr]
forall a b. a -> b -> a
const []) [Expr] -> [Expr]
forall a. a -> a
id (Either [(Int, TcError)] [Expr] -> [Expr])
-> Either [(Int, TcError)] [Expr] -> [Expr]
forall a b. (a -> b) -> a -> b
$ Forest
-> PArg
-> Maybe Type
-> Maybe Int
-> Either [(Int, TcError)] [Expr]
getAbsTrees Forest
f PArg
arg Maybe Type
forall a. Maybe a
Nothing Maybe Int
dp,LinTable
ltable)
descend IntMap (Set Production)
forest (PCoerce Int
fid) = IntMap (Set Production)
-> PArg -> (CncType, Int, CId, [Expr], LinTable)
render IntMap (Set Production)
forest ([(Int, Int)] -> Int -> PArg
PArg [] Int
fid)
descend IntMap (Set Production)
forest (PConst CId
cat Expr
e [String]
ts) = ((CId
cat,Int
fid),Int
0,CId
wildCId,[Expr
e],([],(Int, Int) -> [[BracketedTokn]] -> Array Int [BracketedTokn]
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [e] -> a i e
listArray (Int
0,Int
0) [(String -> BracketedTokn) -> [String] -> [BracketedTokn]
forall a b. (a -> b) -> [a] -> [b]
map String -> BracketedTokn
LeafKS [String]
ts]))
getVar :: (Int, b) -> CId
getVar (Int
fid,b
_)
| Int
fid Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
fidVar = CId
wildCId
| Bool
otherwise = CId
x
where
(CId
x:[CId]
_) = [CId
x | PConst CId
_ (EFun CId
x) [String]
_ <- [Production]
-> (Set Production -> [Production])
-> Maybe (Set Production)
-> [Production]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] Set Production -> [Production]
forall a. Set a -> [a]
Set.toList (Int -> IntMap (Set Production) -> Maybe (Set Production)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
fid IntMap (Set Production)
forest)]
trustedSpots :: IntSet -> PArg -> IntSet
trustedSpots IntSet
parents (PArg [(Int, Int)]
_ Int
fid)
| Int
fid Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Concr -> Int
totalCats Concr
cnc Bool -> Bool -> Bool
||
Int -> IntSet -> Bool
IntSet.member Int
fid IntSet
parents
= IntSet
IntSet.empty
| Bool
otherwise = Int -> IntSet -> IntSet
IntSet.insert Int
fid (IntSet -> IntSet) -> IntSet -> IntSet
forall a b. (a -> b) -> a -> b
$
case Int -> IntMap (Set Production) -> Maybe (Set Production)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
fid IntMap (Set Production)
forest of
Just Set Production
prods -> (IntSet -> IntSet -> IntSet) -> [IntSet] -> IntSet
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 IntSet -> IntSet -> IntSet
IntSet.intersection [Production -> IntSet
descend Production
prod | Production
prod <- Set Production -> [Production]
forall a. Set a -> [a]
Set.toList Set Production
prods]
Maybe (Set Production)
Nothing -> IntSet
IntSet.empty
where
parents' :: IntSet
parents' = Int -> IntSet -> IntSet
IntSet.insert Int
fid IntSet
parents
descend :: Production -> IntSet
descend (PApply Int
funid [PArg]
args) = [IntSet] -> IntSet
forall (f :: * -> *). Foldable f => f IntSet -> IntSet
IntSet.unions ((PArg -> IntSet) -> [PArg] -> [IntSet]
forall a b. (a -> b) -> [a] -> [b]
map (IntSet -> PArg -> IntSet
trustedSpots IntSet
parents') [PArg]
args)
descend (PCoerce Int
fid) = IntSet -> PArg -> IntSet
trustedSpots IntSet
parents' ([(Int, Int)] -> Int -> PArg
PArg [] Int
fid)
descend (PConst CId
c Expr
e [String]
_) = IntSet
IntSet.empty
isLindefCId :: CId -> Maybe CId
isLindefCId id :: CId
id@(CId ByteString
utf8)
| Int -> String -> String
forall a. Int -> [a] -> [a]
take Int
l String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
lindef = CId -> Maybe CId
forall a. a -> Maybe a
Just (String -> CId
mkCId (Int -> String -> String
forall a. Int -> [a] -> [a]
drop Int
l String
s))
| Bool
otherwise = Maybe CId
forall a. Maybe a
Nothing
where
s :: String
s = ByteString -> String
UTF8.toString ByteString
utf8
lindef :: String
lindef = String
"lindef "
l :: Int
l = String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
lindef
getAbsTrees :: Forest -> PArg -> Maybe Type -> Maybe Int -> Either [(FId,TcError)] [Expr]
getAbsTrees :: Forest
-> PArg
-> Maybe Type
-> Maybe Int
-> Either [(Int, TcError)] [Expr]
getAbsTrees (Forest Abstr
abs Concr
cnc IntMap (Set Production)
forest [([Symbol], [PArg])]
root) arg :: PArg
arg@(PArg [(Int, Int)]
_ Int
fid) Maybe Type
ty Maybe Int
dp =
let ([(Int, TcError)]
err,[(MetaStore Int, Int, Expr)]
res) = Abstr
-> TcM Int Expr
-> MetaStore Int
-> Int
-> ([(Int, TcError)], [(MetaStore Int, Int, Expr)])
forall s a.
Abstr
-> TcM s a
-> MetaStore s
-> s
-> ([(s, TcError)], [(MetaStore s, s, a)])
runTcM Abstr
abs (do Expr
e <- Set Int -> Scope -> Maybe TType -> PArg -> TcM Int Expr
go Set Int
forall a. Set a
Set.empty Scope
emptyScope ((Type -> TType) -> Maybe Type -> Maybe TType
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Env -> Type -> TType
TTyp []) Maybe Type
ty) PArg
arg
(Scope -> TType -> TcM Int Expr) -> Expr -> TcM Int Expr
generateForForest (Maybe Int -> Scope -> TType -> TcM Int Expr
forall sel.
Selector sel =>
Maybe Int -> Scope -> TType -> TcM sel Expr
prove Maybe Int
dp) Expr
e) MetaStore Int
forall s. MetaStore s
emptyMetaStore Int
fid
in if [(MetaStore Int, Int, Expr)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(MetaStore Int, Int, Expr)]
res
then [(Int, TcError)] -> Either [(Int, TcError)] [Expr]
forall a b. a -> Either a b
Left ([(Int, TcError)] -> [(Int, TcError)]
forall a. Eq a => [a] -> [a]
nub [(Int, TcError)]
err)
else [Expr] -> Either [(Int, TcError)] [Expr]
forall a b. b -> Either a b
Right ([Expr] -> [Expr]
forall a. Ord a => [a] -> [a]
nub' [Expr
e | (MetaStore Int
_,Int
_,Expr
e) <- [(MetaStore Int, Int, Expr)]
res])
where
go :: Set Int -> Scope -> Maybe TType -> PArg -> TcM Int Expr
go Set Int
rec_ Scope
scope_ Maybe TType
mb_tty_ (PArg [(Int, Int)]
hypos Int
fid)
| Int
fid Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Concr -> Int
totalCats Concr
cnc = case Maybe TType
mb_tty of
Just TType
tty -> do Int
i <- Scope -> TType -> TcM Int Int
forall s. Scope -> TType -> TcM s Int
newMeta Scope
scope TType
tty
Expr -> TcM Int Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr
mkAbs (Int -> Expr
EMeta Int
i))
Maybe TType
Nothing -> TcM Int Expr
forall (m :: * -> *) a. MonadPlus m => m a
mzero
| Int -> Set Int -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Int
fid Set Int
rec_ = TcM Int Expr
forall (m :: * -> *) a. MonadPlus m => m a
mzero
| Bool
otherwise = do Int
fid0 <- TcM Int Int
forall s (m :: * -> *). MonadState s m => m s
get
Int -> TcM Int ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put Int
fid
Expr
x <- (Int -> [PArg] -> TcM Int Expr -> TcM Int Expr)
-> (Expr -> [String] -> TcM Int Expr -> TcM Int Expr)
-> TcM Int Expr
-> Int
-> IntMap (Set Production)
-> TcM Int Expr
forall b.
(Int -> [PArg] -> b -> b)
-> (Expr -> [String] -> b -> b)
-> b
-> Int
-> IntMap (Set Production)
-> b
foldForest (\Int
funid [PArg]
args TcM Int Expr
trees ->
do let CncFun CId
fn UArray Int Int
_lins = Concr -> Array Int CncFun
cncfuns Concr
cnc Array Int CncFun -> Int -> CncFun
forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Int
funid
case CId -> Maybe CId
isLindefCId CId
fn of
Just CId
_ -> do Expr
arg <- Set Int -> Scope -> Maybe TType -> PArg -> TcM Int Expr
go (Int -> Set Int -> Set Int
forall a. Ord a => a -> Set a -> Set a
Set.insert Int
fid Set Int
rec_) Scope
scope Maybe TType
mb_tty ([PArg] -> PArg
forall a. [a] -> a
head [PArg]
args)
Expr -> TcM Int Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr
mkAbs Expr
arg)
Maybe CId
Nothing -> do Type
ty_fn <- CId -> TcM Int Type
forall s. CId -> TcM s Type
lookupFunType CId
fn
(Expr
e,TType
tty0) <- ((Expr, TType) -> PArg -> TcM Int (Expr, TType))
-> (Expr, TType) -> [PArg] -> TcM Int (Expr, TType)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\(Expr
e1,TType
tty) PArg
arg -> Set Int
-> Scope -> Int -> Expr -> PArg -> TType -> TcM Int (Expr, TType)
goArg (Int -> Set Int -> Set Int
forall a. Ord a => a -> Set a -> Set a
Set.insert Int
fid Set Int
rec_) Scope
scope Int
fid Expr
e1 PArg
arg TType
tty)
(CId -> Expr
EFun CId
fn,Env -> Type -> TType
TTyp [] Type
ty_fn) [PArg]
args
case Maybe TType
mb_tty of
Just TType
tty -> do Int
i <- Expr -> TcM Int Int
forall s. Expr -> TcM s Int
newGuardedMeta Expr
e
Scope -> Int -> Int -> TType -> TType -> TcM Int ()
forall s. Scope -> Int -> Int -> TType -> TType -> TcM s ()
eqType Scope
scope (Scope -> Int
scopeSize Scope
scope) Int
i TType
tty TType
tty0
Maybe TType
Nothing -> () -> TcM Int ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
Expr -> TcM Int Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr
mkAbs Expr
e)
TcM Int Expr -> TcM Int Expr -> TcM Int Expr
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus`
TcM Int Expr
trees)
(\Expr
const [String]
_ TcM Int Expr
trees -> do
Expr
const <- case Maybe TType
mb_tty of
Just TType
tty -> Scope -> Expr -> TType -> TcM Int Expr
forall s. Scope -> Expr -> TType -> TcM s Expr
tcExpr Scope
scope Expr
const TType
tty
Maybe TType
Nothing -> ((Expr, TType) -> Expr) -> TcM Int (Expr, TType) -> TcM Int Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Expr, TType) -> Expr
forall a b. (a, b) -> a
fst (TcM Int (Expr, TType) -> TcM Int Expr)
-> TcM Int (Expr, TType) -> TcM Int Expr
forall a b. (a -> b) -> a -> b
$ Scope -> Expr -> TcM Int (Expr, TType)
forall s. Scope -> Expr -> TcM s (Expr, TType)
infExpr Scope
scope Expr
const
Expr -> TcM Int Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr
mkAbs Expr
const)
TcM Int Expr -> TcM Int Expr -> TcM Int Expr
forall (m :: * -> *) a. MonadPlus m => m a -> m a -> m a
`mplus`
TcM Int Expr
trees)
TcM Int Expr
forall (m :: * -> *) a. MonadPlus m => m a
mzero Int
fid IntMap (Set Production)
forest
Int -> TcM Int ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put Int
fid0
Expr -> TcM Int Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
x
where
(Scope
scope,Expr -> Expr
mkAbs,Maybe TType
mb_tty) = [(Int, Int)]
-> Scope
-> (Expr -> Expr)
-> Maybe TType
-> (Scope, Expr -> Expr, Maybe TType)
forall b c.
[(Int, b)]
-> Scope
-> (Expr -> c)
-> Maybe TType
-> (Scope, Expr -> c, Maybe TType)
updateScope [(Int, Int)]
hypos Scope
scope_ Expr -> Expr
forall a. a -> a
id Maybe TType
mb_tty_
goArg :: Set Int
-> Scope -> Int -> Expr -> PArg -> TType -> TcM Int (Expr, TType)
goArg Set Int
rec_ Scope
scope Int
fid Expr
e1 PArg
arg (TTyp Env
delta (DTyp ((BindType
bt,CId
x,Type
ty):[Hypo]
hs) CId
c [Expr]
es)) = do
Expr
e2' <- Set Int -> Scope -> Maybe TType -> PArg -> TcM Int Expr
go Set Int
rec_ Scope
scope (TType -> Maybe TType
forall a. a -> Maybe a
Just (Env -> Type -> TType
TTyp Env
delta Type
ty)) PArg
arg
let e2 :: Expr
e2 = case BindType
bt of
BindType
Explicit -> Expr
e2'
BindType
Implicit -> Expr -> Expr
EImplArg Expr
e2'
if CId
x CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
== CId
wildCId
then (Expr, TType) -> TcM Int (Expr, TType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Expr
EApp Expr
e1 Expr
e2,Env -> Type -> TType
TTyp Env
delta ([Hypo] -> CId -> [Expr] -> Type
DTyp [Hypo]
hs CId
c [Expr]
es))
else do Value
v2 <- Env -> Expr -> TcM Int Value
forall s. Env -> Expr -> TcM s Value
eval (Scope -> Env
scopeEnv Scope
scope) Expr
e2'
(Expr, TType) -> TcM Int (Expr, TType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr -> Expr
EApp Expr
e1 Expr
e2,Env -> Type -> TType
TTyp (Value
v2Value -> Env -> Env
forall a. a -> [a] -> [a]
:Env
delta) ([Hypo] -> CId -> [Expr] -> Type
DTyp [Hypo]
hs CId
c [Expr]
es))
updateScope :: [(Int, b)]
-> Scope
-> (Expr -> c)
-> Maybe TType
-> (Scope, Expr -> c, Maybe TType)
updateScope [] Scope
scope Expr -> c
mkAbs Maybe TType
mb_tty = (Scope
scope,Expr -> c
mkAbs,Maybe TType
mb_tty)
updateScope ((Int
fid,b
_):[(Int, b)]
hypos) Scope
scope Expr -> c
mkAbs Maybe TType
mb_tty =
case Maybe TType
mb_tty of
Just (TTyp Env
delta (DTyp ((BindType
bt,CId
y,Type
ty):[Hypo]
hs) CId
c [Expr]
es)) ->
if CId
y CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
== CId
wildCId
then [(Int, b)]
-> Scope
-> (Expr -> c)
-> Maybe TType
-> (Scope, Expr -> c, Maybe TType)
updateScope [(Int, b)]
hypos (CId -> TType -> Scope -> Scope
addScopedVar CId
x (Env -> Type -> TType
TTyp Env
delta Type
ty) Scope
scope)
(Expr -> c
mkAbs (Expr -> c) -> (Expr -> Expr) -> Expr -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BindType -> CId -> Expr -> Expr
EAbs BindType
bt CId
x)
(TType -> Maybe TType
forall a. a -> Maybe a
Just (Env -> Type -> TType
TTyp Env
delta ([Hypo] -> CId -> [Expr] -> Type
DTyp [Hypo]
hs CId
c [Expr]
es)))
else [(Int, b)]
-> Scope
-> (Expr -> c)
-> Maybe TType
-> (Scope, Expr -> c, Maybe TType)
updateScope [(Int, b)]
hypos (CId -> TType -> Scope -> Scope
addScopedVar CId
x (Env -> Type -> TType
TTyp Env
delta Type
ty) Scope
scope)
(Expr -> c
mkAbs (Expr -> c) -> (Expr -> Expr) -> Expr -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. BindType -> CId -> Expr -> Expr
EAbs BindType
bt CId
x)
(TType -> Maybe TType
forall a. a -> Maybe a
Just (Env -> Type -> TType
TTyp ((Int -> Env -> Value
VGen (Scope -> Int
scopeSize Scope
scope) [])Value -> Env -> Env
forall a. a -> [a] -> [a]
:Env
delta) ([Hypo] -> CId -> [Expr] -> Type
DTyp [Hypo]
hs CId
c [Expr]
es)))
Maybe TType
Nothing -> (Scope
scope,Expr -> c
mkAbs,Maybe TType
forall a. Maybe a
Nothing)
where
(CId
x:[CId]
_) | Int
fid Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
fidVar = [CId
wildCId]
| Bool
otherwise = [CId
x | PConst CId
_ (EFun CId
x) [String]
_ <- [Production]
-> (Set Production -> [Production])
-> Maybe (Set Production)
-> [Production]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [] Set Production -> [Production]
forall a. Set a -> [a]
Set.toList (Int -> IntMap (Set Production) -> Maybe (Set Production)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
fid IntMap (Set Production)
forest)]
foldForest :: (FunId -> [PArg] -> b -> b) -> (Expr -> [String] -> b -> b) -> b -> FId -> IntMap.IntMap (Set.Set Production) -> b
foldForest :: (Int -> [PArg] -> b -> b)
-> (Expr -> [String] -> b -> b)
-> b
-> Int
-> IntMap (Set Production)
-> b
foldForest Int -> [PArg] -> b -> b
f Expr -> [String] -> b -> b
g b
b Int
fcat IntMap (Set Production)
forest =
case Int -> IntMap (Set Production) -> Maybe (Set Production)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
fcat IntMap (Set Production)
forest of
Maybe (Set Production)
Nothing -> b
b
Just Set Production
set -> (Production -> b -> b) -> b -> Set Production -> b
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.foldr Production -> b -> b
foldProd b
b Set Production
set
where
foldProd :: Production -> b -> b
foldProd (PCoerce Int
fcat) b
b = (Int -> [PArg] -> b -> b)
-> (Expr -> [String] -> b -> b)
-> b
-> Int
-> IntMap (Set Production)
-> b
forall b.
(Int -> [PArg] -> b -> b)
-> (Expr -> [String] -> b -> b)
-> b
-> Int
-> IntMap (Set Production)
-> b
foldForest Int -> [PArg] -> b -> b
f Expr -> [String] -> b -> b
g b
b Int
fcat IntMap (Set Production)
forest
foldProd (PApply Int
funid [PArg]
args) b
b = Int -> [PArg] -> b -> b
f Int
funid [PArg]
args b
b
foldProd (PConst CId
_ Expr
const [String]
toks) b
b = Expr -> [String] -> b -> b
g Expr
const [String]
toks b
b
instance Selector FId where
splitSelector :: Int -> (Int, Int)
splitSelector Int
s = (Int
s,Int
s)
select :: CId -> Scope -> Maybe Int -> TcM Int (Expr, TType)
select CId
cat Scope
scope Maybe Int
dp = do
[(Double, Expr, TType)]
gens <- Scope -> CId -> TcM Int [(Double, Expr, TType)]
forall s. Scope -> CId -> TcM s [(Double, Expr, TType)]
typeGenerators Scope
scope CId
cat
(forall b.
Abstr
-> ((Expr, TType) -> MetaStore Int -> Int -> b -> b)
-> (TcError -> Int -> b -> b)
-> MetaStore Int
-> Int
-> b
-> b)
-> TcM Int (Expr, TType)
forall s a.
(forall b.
Abstr
-> (a -> MetaStore s -> s -> b -> b)
-> (TcError -> s -> b -> b)
-> MetaStore s
-> s
-> b
-> b)
-> TcM s a
TcM (\Abstr
abstr (Expr, TType) -> MetaStore Int -> Int -> b -> b
k TcError -> Int -> b -> b
h -> ((Expr, TType) -> MetaStore Int -> Int -> b -> b)
-> [(Double, Expr, TType)] -> MetaStore Int -> Int -> b -> b
forall a b t t b a.
((a, b) -> t -> t -> b -> b) -> [(a, a, b)] -> t -> t -> b -> b
iter (Expr, TType) -> MetaStore Int -> Int -> b -> b
k [(Double, Expr, TType)]
gens)
where
iter :: ((a, b) -> t -> t -> b -> b) -> [(a, a, b)] -> t -> t -> b -> b
iter (a, b) -> t -> t -> b -> b
k [] t
ms t
s = b -> b
forall a. a -> a
id
iter (a, b) -> t -> t -> b -> b
k ((a
_,a
e,b
tty):[(a, a, b)]
fns) t
ms t
s = (a, b) -> t -> t -> b -> b
k (a
e,b
tty) t
ms t
s (b -> b) -> (b -> b) -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a, b) -> t -> t -> b -> b) -> [(a, a, b)] -> t -> t -> b -> b
iter (a, b) -> t -> t -> b -> b
k [(a, a, b)]
fns t
ms t
s