{-# LANGUAGE TypeSynonymInstances #-}

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

-- |

-- Module      : PGF

-- Maintainer  : Krasimir Angelov

-- Stability   : stable

-- Portability : portable

--

-- Forest is a compact representation of a set

-- of parse trees. This let us to efficiently

-- represent local ambiguities

--

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


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])]
      }

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

-- Rendering of bracketed strings

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


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

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

-- Internally we have to do everything with Tokn first because

-- we must handle the pre {...} construction.

--


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
||                  -- forest ids from the grammar correspond to metavariables

        Int -> IntSet -> Bool
IntSet.member Int
fid IntSet
parents               -- this avoids loops in the grammar

                  = 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

-- | This function extracts the list of all completed parse trees

-- that spans the whole input consumed so far. The trees are also

-- limited by the category specified, which is usually

-- the same as the startup category.

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


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

-- Selectors


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