module PGF.Generate 
         ( generateAll,         generateAllDepth
         , generateFrom,        generateFromDepth
         , generateRandom,      generateRandomDepth
         , generateRandomFrom,  generateRandomFromDepth
         , generateOntology,    generateOntologyDepth
         , prove
         ) where

import PGF.CId
import PGF.Data
import PGF.TypeCheck
import Control.Monad
import Control.Monad.State
import Control.Monad.Identity
import System.Random
import Data.Maybe(isNothing)

------------------------------------------------------------------------------
-- The API

-- | Generates an exhaustive possibly infinite list of
-- abstract syntax expressions.
generateAll :: PGF -> Type -> [Expr]
generateAll :: PGF -> Type -> [Expr]
generateAll PGF
pgf Type
ty = PGF -> Type -> Maybe Int -> [Expr]
generateAllDepth PGF
pgf Type
ty Maybe Int
forall a. Maybe a
Nothing

-- | A variant of 'generateAll' which also takes as argument
-- the upper limit of the depth of the generated expression.
generateAllDepth :: PGF -> Type -> Maybe Int -> [Expr]
generateAllDepth :: PGF -> Type -> Maybe Int -> [Expr]
generateAllDepth PGF
pgf Type
ty Maybe Int
dp = () -> PGF -> Type -> Maybe Int -> [Expr]
forall sel.
Selector sel =>
sel -> PGF -> Type -> Maybe Int -> [Expr]
generate () PGF
pgf Type
ty Maybe Int
dp

-- | Generates a list of abstract syntax expressions
-- in a way similar to 'generateAll' but instead of
-- generating all instances of a given type, this
-- function uses a template. 
generateFrom :: PGF -> Expr -> [Expr]
generateFrom :: PGF -> Expr -> [Expr]
generateFrom PGF
pgf Expr
ex = PGF -> Expr -> Maybe Int -> [Expr]
generateFromDepth PGF
pgf Expr
ex Maybe Int
forall a. Maybe a
Nothing

-- | A variant of 'generateFrom' which also takes as argument
-- the upper limit of the depth of the generated subexpressions.
generateFromDepth :: PGF -> Expr -> Maybe Int -> [Expr]
generateFromDepth :: PGF -> Expr -> Maybe Int -> [Expr]
generateFromDepth PGF
pgf Expr
e Maybe Int
dp = 
  [Expr
e | (MetaStore ()
_,()
_,Expr
e) <- ([((), TcError)], [(MetaStore (), (), Expr)])
-> [(MetaStore (), (), Expr)]
forall a b. (a, b) -> b
snd (([((), TcError)], [(MetaStore (), (), Expr)])
 -> [(MetaStore (), (), Expr)])
-> ([((), TcError)], [(MetaStore (), (), Expr)])
-> [(MetaStore (), (), Expr)]
forall a b. (a -> b) -> a -> b
$ Abstr
-> TcM () Expr
-> MetaStore ()
-> ()
-> ([((), TcError)], [(MetaStore (), (), Expr)])
forall s a.
Abstr
-> TcM s a
-> MetaStore s
-> s
-> ([(s, TcError)], [(MetaStore s, s, a)])
runTcM (PGF -> Abstr
abstract PGF
pgf)
                               ((Scope -> TType -> TcM () Expr) -> Expr -> TcM () Expr
forall s.
Selector s =>
(Scope -> TType -> TcM s Expr) -> Expr -> TcM s Expr
generateForMetas (Maybe Int -> Scope -> TType -> TcM () Expr
forall sel.
Selector sel =>
Maybe Int -> Scope -> TType -> TcM sel Expr
prove Maybe Int
dp) Expr
e)
                               MetaStore ()
forall s. MetaStore s
emptyMetaStore ()]

-- | Generates an infinite list of random abstract syntax expressions.
-- This is usefull for tree bank generation which after that can be used
-- for grammar testing.
generateRandom :: RandomGen g => g -> PGF -> Type -> [Expr]
generateRandom :: g -> PGF -> Type -> [Expr]
generateRandom g
g PGF
pgf Type
ty = g -> PGF -> Type -> Maybe Int -> [Expr]
forall g. RandomGen g => g -> PGF -> Type -> Maybe Int -> [Expr]
generateRandomDepth g
g PGF
pgf Type
ty Maybe Int
forall a. Maybe a
Nothing

-- | A variant of 'generateRandom' which also takes as argument
-- the upper limit of the depth of the generated expression.
generateRandomDepth :: RandomGen g => g -> PGF -> Type -> Maybe Int -> [Expr]
generateRandomDepth :: g -> PGF -> Type -> Maybe Int -> [Expr]
generateRandomDepth g
g PGF
pgf Type
ty Maybe Int
dp = g -> (g -> [Expr]) -> [Expr]
forall g a. RandomGen g => g -> (g -> [a]) -> [a]
restart g
g (\g
g -> Identity g -> PGF -> Type -> Maybe Int -> [Expr]
forall sel.
Selector sel =>
sel -> PGF -> Type -> Maybe Int -> [Expr]
generate (g -> Identity g
forall a. a -> Identity a
Identity g
g) PGF
pgf Type
ty Maybe Int
dp)

-- | Random generation based on template
generateRandomFrom :: RandomGen g => g -> PGF -> Expr -> [Expr]
generateRandomFrom :: g -> PGF -> Expr -> [Expr]
generateRandomFrom g
g PGF
pgf Expr
e = g -> PGF -> Expr -> Maybe Int -> [Expr]
forall g. RandomGen g => g -> PGF -> Expr -> Maybe Int -> [Expr]
generateRandomFromDepth g
g PGF
pgf Expr
e Maybe Int
forall a. Maybe a
Nothing

-- | Random generation based on template with a limitation in the depth.
generateRandomFromDepth :: RandomGen g => g -> PGF -> Expr -> Maybe Int -> [Expr]
generateRandomFromDepth :: g -> PGF -> Expr -> Maybe Int -> [Expr]
generateRandomFromDepth g
g PGF
pgf Expr
e Maybe Int
dp = 
  g -> (g -> [Expr]) -> [Expr]
forall g a. RandomGen g => g -> (g -> [a]) -> [a]
restart g
g (\g
g -> [Expr
e | (MetaStore (Identity g)
_,Identity g
ms,Expr
e) <- ([(Identity g, TcError)],
 [(MetaStore (Identity g), Identity g, Expr)])
-> [(MetaStore (Identity g), Identity g, Expr)]
forall a b. (a, b) -> b
snd (([(Identity g, TcError)],
  [(MetaStore (Identity g), Identity g, Expr)])
 -> [(MetaStore (Identity g), Identity g, Expr)])
-> ([(Identity g, TcError)],
    [(MetaStore (Identity g), Identity g, Expr)])
-> [(MetaStore (Identity g), Identity g, Expr)]
forall a b. (a -> b) -> a -> b
$ Abstr
-> TcM (Identity g) Expr
-> MetaStore (Identity g)
-> Identity g
-> ([(Identity g, TcError)],
    [(MetaStore (Identity g), Identity g, Expr)])
forall s a.
Abstr
-> TcM s a
-> MetaStore s
-> s
-> ([(s, TcError)], [(MetaStore s, s, a)])
runTcM (PGF -> Abstr
abstract PGF
pgf)
                                                 ((Scope -> TType -> TcM (Identity g) Expr)
-> Expr -> TcM (Identity g) Expr
forall s.
Selector s =>
(Scope -> TType -> TcM s Expr) -> Expr -> TcM s Expr
generateForMetas (Maybe Int -> Scope -> TType -> TcM (Identity g) Expr
forall sel.
Selector sel =>
Maybe Int -> Scope -> TType -> TcM sel Expr
prove Maybe Int
dp) Expr
e)
                                                 MetaStore (Identity g)
forall s. MetaStore s
emptyMetaStore (g -> Identity g
forall a. a -> Identity a
Identity g
g)])

generateOntology :: RandomGen g => g -> PGF -> Type -> [(Maybe Expr, Type)] -> [Expr]
generateOntology :: g -> PGF -> Type -> [(Maybe Expr, Type)] -> [Expr]
generateOntology g
g PGF
pgf Type
ty [(Maybe Expr, Type)]
args = g -> PGF -> Type -> [(Maybe Expr, Type)] -> Maybe Int -> [Expr]
forall g.
RandomGen g =>
g -> PGF -> Type -> [(Maybe Expr, Type)] -> Maybe Int -> [Expr]
generateOntologyDepth g
g PGF
pgf Type
ty [(Maybe Expr, Type)]
args Maybe Int
forall a. Maybe a
Nothing

generateOntologyDepth :: RandomGen g => g -> PGF -> Type -> [(Maybe Expr, Type)] -> Maybe Int -> [Expr]
generateOntologyDepth :: g -> PGF -> Type -> [(Maybe Expr, Type)] -> Maybe Int -> [Expr]
generateOntologyDepth g
g PGF
pgf Type
ty [(Maybe Expr, Type)]
args Maybe Int
dp =
  g -> (g -> [Expr]) -> [Expr]
forall g a. RandomGen g => g -> (g -> [a]) -> [a]
restart g
g (\g
g -> [Expr
e | (MetaStore (Ontology g)
_,(Ontology [(Maybe Expr, Type)]
args' g
_),Expr
e) <- ([(Ontology g, TcError)],
 [(MetaStore (Ontology g), Ontology g, Expr)])
-> [(MetaStore (Ontology g), Ontology g, Expr)]
forall a b. (a, b) -> b
snd (([(Ontology g, TcError)],
  [(MetaStore (Ontology g), Ontology g, Expr)])
 -> [(MetaStore (Ontology g), Ontology g, Expr)])
-> ([(Ontology g, TcError)],
    [(MetaStore (Ontology g), Ontology g, Expr)])
-> [(MetaStore (Ontology g), Ontology g, Expr)]
forall a b. (a -> b) -> a -> b
$ Abstr
-> TcM (Ontology g) Expr
-> MetaStore (Ontology g)
-> Ontology g
-> ([(Ontology g, TcError)],
    [(MetaStore (Ontology g), Ontology g, Expr)])
forall s a.
Abstr
-> TcM s a
-> MetaStore s
-> s
-> ([(s, TcError)], [(MetaStore s, s, a)])
runTcM (PGF -> Abstr
abstract PGF
pgf)
                                                                 (Maybe Int -> Scope -> TType -> TcM (Ontology g) Expr
forall sel.
Selector sel =>
Maybe Int -> Scope -> TType -> TcM sel Expr
prove Maybe Int
dp Scope
emptyScope (Env -> Type -> TType
TTyp [] Type
ty) TcM (Ontology g) Expr
-> (Expr -> TcM (Ontology g) Expr) -> TcM (Ontology g) Expr
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Scope -> Expr -> TcM (Ontology g) Expr
forall s. Scope -> Expr -> TcM s Expr
checkResolvedMetaStore Scope
emptyScope)
                                                                 MetaStore (Ontology g)
forall s. MetaStore s
emptyMetaStore
                                                                 ([(Maybe Expr, Type)] -> g -> Ontology g
forall a. [(Maybe Expr, Type)] -> a -> Ontology a
Ontology [(Maybe Expr, Type)]
args g
g),
                        ((Maybe Expr, Type) -> Bool) -> [(Maybe Expr, Type)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Maybe Expr -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe Expr -> Bool)
-> ((Maybe Expr, Type) -> Maybe Expr) -> (Maybe Expr, Type) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Expr, Type) -> Maybe Expr
forall a b. (a, b) -> a
fst) [(Maybe Expr, Type)]
args'])

------------------------------------------------------------------------------
-- The main generation algorithm

generate :: Selector sel => sel -> PGF -> Type -> Maybe Int -> [Expr]
generate :: sel -> PGF -> Type -> Maybe Int -> [Expr]
generate sel
sel PGF
pgf Type
ty Maybe Int
dp =
  [Expr
e | (MetaStore sel
_,sel
ms,Expr
e) <- ([(sel, TcError)], [(MetaStore sel, sel, Expr)])
-> [(MetaStore sel, sel, Expr)]
forall a b. (a, b) -> b
snd (([(sel, TcError)], [(MetaStore sel, sel, Expr)])
 -> [(MetaStore sel, sel, Expr)])
-> ([(sel, TcError)], [(MetaStore sel, sel, Expr)])
-> [(MetaStore sel, sel, Expr)]
forall a b. (a -> b) -> a -> b
$ Abstr
-> TcM sel Expr
-> MetaStore sel
-> sel
-> ([(sel, TcError)], [(MetaStore sel, sel, Expr)])
forall s a.
Abstr
-> TcM s a
-> MetaStore s
-> s
-> ([(s, TcError)], [(MetaStore s, s, a)])
runTcM (PGF -> Abstr
abstract PGF
pgf)
                                (Maybe Int -> Scope -> TType -> TcM sel Expr
forall sel.
Selector sel =>
Maybe Int -> Scope -> TType -> TcM sel Expr
prove Maybe Int
dp Scope
emptyScope (Env -> Type -> TType
TTyp [] Type
ty) TcM sel Expr -> (Expr -> TcM sel Expr) -> TcM sel Expr
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Scope -> Expr -> TcM sel Expr
forall s. Scope -> Expr -> TcM s Expr
checkResolvedMetaStore Scope
emptyScope)
                                MetaStore sel
forall s. MetaStore s
emptyMetaStore sel
sel]


prove :: Selector sel => Maybe Int -> Scope -> TType -> TcM sel Expr
prove :: Maybe Int -> Scope -> TType -> TcM sel Expr
prove Maybe Int
dp Scope
scope (TTyp Env
env1 (DTyp [Hypo]
hypos1 CId
cat [Expr]
es1)) = do
  Env
vs1 <- (Expr -> TcM sel Value) -> [Expr] -> TcM sel Env
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Env -> Expr -> TcM sel Value
forall s. Env -> Expr -> TcM s Value
PGF.TypeCheck.eval Env
env1) [Expr]
es1
  let scope' :: Scope
scope' = Scope -> Env -> [Hypo] -> Scope
forall a. Scope -> Env -> [(a, CId, Type)] -> Scope
exScope Scope
scope Env
env1 [Hypo]
hypos1
  (Expr
fe,TTyp Env
env2 (DTyp [Hypo]
hypos2 CId
_ [Expr]
es2)) <- CId -> Scope -> Maybe Int -> TcM sel (Expr, TType)
forall s.
Selector s =>
CId -> Scope -> Maybe Int -> TcM s (Expr, TType)
select CId
cat Scope
scope' Maybe Int
dp
  case Maybe Int
dp of
    Just Int
0 | Bool -> Bool
not ([Hypo] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Hypo]
hypos2) -> TcM sel ()
forall (m :: * -> *) a. MonadPlus m => m a
mzero
    Maybe Int
_                          -> () -> TcM sel ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  (Env
env2,[(BindType, Either TType Expr)]
args) <- Scope
-> Env -> [Hypo] -> TcM sel (Env, [(BindType, Either TType Expr)])
forall a s.
Scope
-> Env -> [(a, CId, Type)] -> TcM s (Env, [(a, Either TType Expr)])
mkEnv Scope
scope' Env
env2 [Hypo]
hypos2
  Env
vs2 <- (Expr -> TcM sel Value) -> [Expr] -> TcM sel Env
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Env -> Expr -> TcM sel Value
forall s. Env -> Expr -> TcM s Value
PGF.TypeCheck.eval Env
env2) [Expr]
es2
  [TcM sel ()] -> TcM sel ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [(forall a. TcM sel a)
-> (Int -> (Expr -> TcM sel ()) -> TcM sel ())
-> Int
-> Value
-> Value
-> TcM sel ()
forall s.
(forall a. TcM s a)
-> (Int -> (Expr -> TcM s ()) -> TcM s ())
-> Int
-> Value
-> Value
-> TcM s ()
eqValue forall a. TcM sel a
forall (m :: * -> *) a. MonadPlus m => m a
mzero Int -> (Expr -> TcM sel ()) -> TcM sel ()
forall s. Int -> (Expr -> TcM s ()) -> TcM s ()
suspend (Scope -> Int
scopeSize Scope
scope') Value
v1 Value
v2 | (Value
v1,Value
v2) <- Env -> Env -> [(Value, Value)]
forall a b. [a] -> [b] -> [(a, b)]
zip Env
vs1 Env
vs2]
  [Expr]
es <- ((BindType, Either TType Expr) -> TcM sel Expr)
-> [(BindType, Either TType Expr)] -> TcM sel [Expr]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Scope -> (BindType, Either TType Expr) -> TcM sel Expr
forall sel.
Selector sel =>
Scope -> (BindType, Either TType Expr) -> TcM sel Expr
descend Scope
scope') [(BindType, Either TType Expr)]
args
  Expr -> TcM sel Expr
forall (m :: * -> *) a. Monad m => a -> m a
return ([Hypo] -> Expr -> Expr
forall c. [(BindType, CId, c)] -> Expr -> Expr
abs [Hypo]
hypos1 ((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
fe [Expr]
es))
  where
    suspend :: Int -> (Expr -> TcM s ()) -> TcM s ()
suspend Int
i Expr -> TcM s ()
c = do
      MetaValue s
mv <- Int -> TcM s (MetaValue s)
forall s. Int -> TcM s (MetaValue s)
getMeta Int
i
      case MetaValue s
mv of
        MBound Expr
e -> Expr -> TcM s ()
c Expr
e
        MUnbound s
x Scope
scope TType
tty [Expr -> TcM s ()]
cs -> Int -> MetaValue s -> TcM s ()
forall s. Int -> MetaValue s -> TcM s ()
setMeta Int
i (s -> Scope -> TType -> [Expr -> TcM s ()] -> MetaValue s
forall s. s -> Scope -> TType -> [Expr -> TcM s ()] -> MetaValue s
MUnbound s
x Scope
scope TType
tty (Expr -> TcM s ()
c(Expr -> TcM s ()) -> [Expr -> TcM s ()] -> [Expr -> TcM s ()]
forall a. a -> [a] -> [a]
:[Expr -> TcM s ()]
cs))

    abs :: [(BindType, CId, c)] -> Expr -> Expr
abs []                Expr
e = Expr
e
    abs ((BindType
bt,CId
x,c
ty):[(BindType, CId, c)]
hypos) Expr
e = BindType -> CId -> Expr -> Expr
EAbs BindType
bt CId
x ([(BindType, CId, c)] -> Expr -> Expr
abs [(BindType, CId, c)]
hypos Expr
e)

    exScope :: Scope -> Env -> [(a, CId, Type)] -> Scope
exScope Scope
scope Env
env []                = Scope
scope
    exScope Scope
scope Env
env ((a
bt,CId
x,Type
ty):[(a, CId, Type)]
hypos) = 
       let env' :: Env
env' | CId
x CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
/= CId
wildCId = Int -> Env -> Value
VGen (Scope -> Int
scopeSize Scope
scope) [] Value -> Env -> Env
forall a. a -> [a] -> [a]
: Env
env
                | Bool
otherwise    = Env
env
       in Scope -> Env -> [(a, CId, Type)] -> Scope
exScope (CId -> TType -> Scope -> Scope
addScopedVar CId
x (Env -> Type -> TType
TTyp Env
env Type
ty) Scope
scope) Env
env' [(a, CId, Type)]
hypos

    mkEnv :: Scope
-> Env -> [(a, CId, Type)] -> TcM s (Env, [(a, Either TType Expr)])
mkEnv Scope
scope Env
env []                = (Env, [(a, Either TType Expr)])
-> TcM s (Env, [(a, Either TType Expr)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Env
env,[])
    mkEnv Scope
scope Env
env ((a
bt,CId
x,Type
ty):[(a, CId, Type)]
hypos) = do
      (Env
env,Either TType Expr
arg) <- if CId
x CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
/= CId
wildCId
                    then do Int
i <- Scope -> TType -> TcM s Int
forall s. Scope -> TType -> TcM s Int
newMeta Scope
scope (Env -> Type -> TType
TTyp Env
env Type
ty)
                            (Env, Either TType Expr) -> TcM s (Env, Either TType Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> Env -> Env -> Value
VMeta Int
i (Scope -> Env
scopeEnv Scope
scope) [] Value -> Env -> Env
forall a. a -> [a] -> [a]
: Env
env,Expr -> Either TType Expr
forall a b. b -> Either a b
Right (Int -> Expr
EMeta Int
i))
                    else (Env, Either TType Expr) -> TcM s (Env, Either TType Expr)
forall (m :: * -> *) a. Monad m => a -> m a
return (Env
env,TType -> Either TType Expr
forall a b. a -> Either a b
Left (Env -> Type -> TType
TTyp Env
env Type
ty))
      (Env
env,[(a, Either TType Expr)]
args) <- Scope
-> Env -> [(a, CId, Type)] -> TcM s (Env, [(a, Either TType Expr)])
mkEnv Scope
scope Env
env [(a, CId, Type)]
hypos
      (Env, [(a, Either TType Expr)])
-> TcM s (Env, [(a, Either TType Expr)])
forall (m :: * -> *) a. Monad m => a -> m a
return (Env
env,(a
bt,Either TType Expr
arg)(a, Either TType Expr)
-> [(a, Either TType Expr)] -> [(a, Either TType Expr)]
forall a. a -> [a] -> [a]
:[(a, Either TType Expr)]
args)

    descend :: Scope -> (BindType, Either TType Expr) -> TcM sel Expr
descend Scope
scope (BindType
bt,Either TType Expr
arg) = do
      let dp' :: Maybe Int
dp' = (Int -> Int) -> Maybe Int -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Int -> Int -> Int) -> Int -> Int -> Int
forall a b c. (a -> b -> c) -> b -> a -> c
flip (-) Int
1) Maybe Int
dp
      Expr
e <- case Either TType Expr
arg of
             Right Expr
e  -> Expr -> TcM sel Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
             Left TType
tty -> Maybe Int -> Scope -> TType -> TcM sel Expr
forall sel.
Selector sel =>
Maybe Int -> Scope -> TType -> TcM sel Expr
prove Maybe Int
dp' Scope
scope TType
tty
      Expr
e <- case BindType
bt of
             BindType
Implicit -> Expr -> TcM sel Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Expr
EImplArg Expr
e)
             BindType
Explicit -> Expr -> TcM sel Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e
      Expr -> TcM sel Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e


-- Helper function for random generation. After every
-- success we must restart the search to find sufficiently different solution.
restart :: RandomGen g => g -> (g -> [a]) -> [a]
restart :: g -> (g -> [a]) -> [a]
restart g
g g -> [a]
f =
  let (g
g1,g
g2) = g -> (g, g)
forall g. RandomGen g => g -> (g, g)
split g
g
  in case g -> [a]
f g
g1 of
       []     -> []
       (a
x:[a]
xs) -> a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: g -> (g -> [a]) -> [a]
forall g a. RandomGen g => g -> (g -> [a]) -> [a]
restart g
g2 g -> [a]
f


------------------------------------------------------------------------------
-- Selectors

instance Selector () where
  splitSelector :: () -> ((), ())
splitSelector ()
s = (()
s,()
s)
  select :: CId -> Scope -> Maybe Int -> TcM () (Expr, TType)
select CId
cat Scope
scope Maybe Int
dp = do
    [(Double, Expr, TType)]
gens <- Scope -> CId -> TcM () [(Double, Expr, TType)]
forall s. Scope -> CId -> TcM s [(Double, Expr, TType)]
typeGenerators Scope
scope CId
cat
    (forall b.
 Abstr
 -> ((Expr, TType) -> MetaStore () -> () -> b -> b)
 -> (TcError -> () -> b -> b)
 -> MetaStore ()
 -> ()
 -> b
 -> b)
-> TcM () (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 () -> () -> b -> b
k TcError -> () -> b -> b
h -> ((Expr, TType) -> MetaStore () -> () -> b -> b)
-> [(Double, Expr, TType)] -> MetaStore () -> () -> 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 () -> () -> 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


instance RandomGen g => Selector (Identity g) where
  splitSelector :: Identity g -> (Identity g, Identity g)
splitSelector (Identity g
g) = let (g
g1,g
g2) = g -> (g, g)
forall g. RandomGen g => g -> (g, g)
split g
g
                               in (g -> Identity g
forall a. a -> Identity a
Identity g
g1, g -> Identity g
forall a. a -> Identity a
Identity g
g2)

  select :: CId -> Scope -> Maybe Int -> TcM (Identity g) (Expr, TType)
select CId
cat Scope
scope Maybe Int
dp = do
    [(Double, Expr, TType)]
gens <- Scope -> CId -> TcM (Identity g) [(Double, Expr, TType)]
forall s. Scope -> CId -> TcM s [(Double, Expr, TType)]
typeGenerators Scope
scope CId
cat
    (forall b.
 Abstr
 -> ((Expr, TType)
     -> MetaStore (Identity g) -> Identity g -> b -> b)
 -> (TcError -> Identity g -> b -> b)
 -> MetaStore (Identity g)
 -> Identity g
 -> b
 -> b)
-> TcM (Identity g) (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 (Identity g) -> Identity g -> b -> b
k TcError -> Identity g -> b -> b
h -> ((Expr, TType) -> MetaStore (Identity g) -> Identity g -> b -> b)
-> Double
-> [(Double, Expr, TType)]
-> MetaStore (Identity g)
-> Identity g
-> b
-> b
forall a t b.
RandomGen a =>
((Expr, TType) -> t -> Identity a -> b -> b)
-> Double -> [(Double, Expr, TType)] -> t -> Identity a -> b -> b
iter (Expr, TType) -> MetaStore (Identity g) -> Identity g -> b -> b
k Double
1.0 [(Double, Expr, TType)]
gens)
    where
      iter :: ((Expr, TType) -> t -> Identity a -> b -> b)
-> Double -> [(Double, Expr, TType)] -> t -> Identity a -> b -> b
iter (Expr, TType) -> t -> Identity a -> b -> b
k Double
p []   t
ms (Identity a
g) = b -> b
forall a. a -> a
id
      iter (Expr, TType) -> t -> Identity a -> b -> b
k Double
p [(Double, Expr, TType)]
gens t
ms (Identity a
g) = let (Double
d,a
g')    = (Double, Double) -> a -> (Double, a)
forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (Double
0.0,Double
p) a
g
                                          (a
g1,a
g2)   = a -> (a, a)
forall g. RandomGen g => g -> (g, g)
split a
g'
                                          (Double
p',(Expr, TType)
e_ty,[(Double, Expr, TType)]
gens') = Double
-> [(Double, Expr, TType)]
-> (Double, (Expr, TType), [(Double, Expr, TType)])
hit Double
d [(Double, Expr, TType)]
gens
                                      in (Expr, TType) -> t -> Identity a -> b -> b
k (Expr, TType)
e_ty t
ms (a -> Identity a
forall a. a -> Identity a
Identity a
g1) (b -> b) -> (b -> b) -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Expr, TType) -> t -> Identity a -> b -> b)
-> Double -> [(Double, Expr, TType)] -> t -> Identity a -> b -> b
iter (Expr, TType) -> t -> Identity a -> b -> b
k (Double
pDouble -> Double -> Double
forall a. Num a => a -> a -> a
-Double
p') [(Double, Expr, TType)]
gens' t
ms (a -> Identity a
forall a. a -> Identity a
Identity a
g2)

      hit :: Double -> [(Double,Expr,TType)] -> (Double,(Expr,TType),[(Double,Expr,TType)])
      hit :: Double
-> [(Double, Expr, TType)]
-> (Double, (Expr, TType), [(Double, Expr, TType)])
hit Double
d (gen :: (Double, Expr, TType)
gen@(Double
p,Expr
e,TType
ty):[(Double, Expr, TType)]
gens)
        | Double
d Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< Double
p Bool -> Bool -> Bool
|| [(Double, Expr, TType)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Double, Expr, TType)]
gens = (Double
p,(Expr
e,TType
ty),[(Double, Expr, TType)]
gens)
        | Bool
otherwise = let (Double
p',(Expr, TType)
e_ty',[(Double, Expr, TType)]
gens') = Double
-> [(Double, Expr, TType)]
-> (Double, (Expr, TType), [(Double, Expr, TType)])
hit (Double
dDouble -> Double -> Double
forall a. Num a => a -> a -> a
-Double
p) [(Double, Expr, TType)]
gens
                      in (Double
p',(Expr, TType)
e_ty',(Double, Expr, TType)
gen(Double, Expr, TType)
-> [(Double, Expr, TType)] -> [(Double, Expr, TType)]
forall a. a -> [a] -> [a]
:[(Double, Expr, TType)]
gens')


data Ontology a = Ontology [(Maybe Expr, Type)] a

instance RandomGen g => Selector (Ontology g) where
  splitSelector :: Ontology g -> (Ontology g, Ontology g)
splitSelector (Ontology [(Maybe Expr, Type)]
args g
g) = let (g
g1,g
g2) = g -> (g, g)
forall g. RandomGen g => g -> (g, g)
split g
g
                                    in ([(Maybe Expr, Type)] -> g -> Ontology g
forall a. [(Maybe Expr, Type)] -> a -> Ontology a
Ontology [(Maybe Expr, Type)]
args g
g1, [(Maybe Expr, Type)] -> g -> Ontology g
forall a. [(Maybe Expr, Type)] -> a -> Ontology a
Ontology [(Maybe Expr, Type)]
args g
g2)

  select :: CId -> Scope -> Maybe Int -> TcM (Ontology g) (Expr, TType)
select CId
cat Scope
scope Maybe Int
dp = do
    Ontology [(Maybe Expr, Type)]
args g
g <- TcM (Ontology g) (Ontology g)
forall s (m :: * -> *). MonadState s m => m s
get
    case [(Maybe Expr, Type)]
-> CId
-> [(Maybe Expr, Type)]
-> [(Maybe Expr, Type, [(Maybe Expr, Type)])]
forall a.
[(a, Type)] -> CId -> [(a, Type)] -> [(a, Type, [(a, Type)])]
pickArg [] CId
cat [(Maybe Expr, Type)]
args of
      []   -> do [(Double, Expr, TType)]
gens <- Scope -> CId -> TcM (Ontology g) [(Double, Expr, TType)]
forall s. Scope -> CId -> TcM s [(Double, Expr, TType)]
typeGenerators Scope
scope CId
cat
                 (forall b.
 Abstr
 -> ((Expr, TType)
     -> MetaStore (Ontology g) -> Ontology g -> b -> b)
 -> (TcError -> Ontology g -> b -> b)
 -> MetaStore (Ontology g)
 -> Ontology g
 -> b
 -> b)
-> TcM (Ontology g) (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 (Ontology g) -> Ontology g -> b -> b
k TcError -> Ontology g -> b -> b
h -> ((Expr, TType) -> MetaStore (Ontology g) -> Ontology g -> b -> b)
-> Double
-> [(Double, Expr, TType)]
-> MetaStore (Ontology g)
-> Ontology g
-> b
-> b
forall a t b.
RandomGen a =>
((Expr, TType) -> t -> Ontology a -> b -> b)
-> Double -> [(Double, Expr, TType)] -> t -> Ontology a -> b -> b
iter (Expr, TType) -> MetaStore (Ontology g) -> Ontology g -> b -> b
k Double
1.0 [(Double, Expr, TType)]
gens)
      [(Maybe Expr, Type, [(Maybe Expr, Type)])]
alts -> [TcM (Ontology g) (Expr, TType)] -> TcM (Ontology g) (Expr, TType)
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum [  case Maybe Expr
mb_e of
                        Just Expr
e  -> do Ontology g -> TcM (Ontology g) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put ([(Maybe Expr, Type)] -> g -> Ontology g
forall a. [(Maybe Expr, Type)] -> a -> Ontology a
Ontology [(Maybe Expr, Type)]
args g
g)
                                      (Expr, TType) -> TcM (Ontology g) (Expr, TType)
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr
e, Env -> Type -> TType
TTyp [] Type
ty)
                        Maybe Expr
Nothing -> TcM (Ontology g) (Expr, TType)
forall (m :: * -> *) a. MonadPlus m => m a
mzero
                    | (Maybe Expr
mb_e,Type
ty,[(Maybe Expr, Type)]
args) <- [(Maybe Expr, Type, [(Maybe Expr, Type)])]
alts]
    where
      iter :: ((Expr, TType) -> t -> Ontology a -> b -> b)
-> Double -> [(Double, Expr, TType)] -> t -> Ontology a -> b -> b
iter (Expr, TType) -> t -> Ontology a -> b -> b
k Double
p []   t
ms (Ontology [(Maybe Expr, Type)]
ce a
g) = b -> b
forall a. a -> a
id
      iter (Expr, TType) -> t -> Ontology a -> b -> b
k Double
p [(Double, Expr, TType)]
gens t
ms (Ontology [(Maybe Expr, Type)]
ce a
g) =
        let (Double
d,a
g')    = (Double, Double) -> a -> (Double, a)
forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (Double
0.0,Double
p) a
g
            (a
g1,a
g2)   = a -> (a, a)
forall g. RandomGen g => g -> (g, g)
split a
g'
            (Double
p',(Expr, TType)
e_ty,[(Double, Expr, TType)]
gens') = Double
-> [(Double, Expr, TType)]
-> (Double, (Expr, TType), [(Double, Expr, TType)])
hit Double
d [(Double, Expr, TType)]
gens
        in (Expr, TType) -> t -> Ontology a -> b -> b
k (Expr, TType)
e_ty t
ms ([(Maybe Expr, Type)] -> a -> Ontology a
forall a. [(Maybe Expr, Type)] -> a -> Ontology a
Ontology [(Maybe Expr, Type)]
ce a
g1) (b -> b) -> (b -> b) -> b -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Expr, TType) -> t -> Ontology a -> b -> b)
-> Double -> [(Double, Expr, TType)] -> t -> Ontology a -> b -> b
iter (Expr, TType) -> t -> Ontology a -> b -> b
k (Double
pDouble -> Double -> Double
forall a. Num a => a -> a -> a
-Double
p') [(Double, Expr, TType)]
gens' t
ms ([(Maybe Expr, Type)] -> a -> Ontology a
forall a. [(Maybe Expr, Type)] -> a -> Ontology a
Ontology [(Maybe Expr, Type)]
ce a
g2)

      hit :: Double -> [(Double,Expr,TType)] -> (Double,(Expr,TType),[(Double,Expr,TType)])
      hit :: Double
-> [(Double, Expr, TType)]
-> (Double, (Expr, TType), [(Double, Expr, TType)])
hit Double
d (gen :: (Double, Expr, TType)
gen@(Double
p,Expr
e,TType
ty):[(Double, Expr, TType)]
gens) | Double
d Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
< Double
p Bool -> Bool -> Bool
|| [(Double, Expr, TType)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Double, Expr, TType)]
gens = (Double
p,(Expr
e,TType
ty),[(Double, Expr, TType)]
gens)
                                | Bool
otherwise          = let (Double
p',(Expr, TType)
e_ty',[(Double, Expr, TType)]
gens') = Double
-> [(Double, Expr, TType)]
-> (Double, (Expr, TType), [(Double, Expr, TType)])
hit (Double
dDouble -> Double -> Double
forall a. Num a => a -> a -> a
-Double
p) [(Double, Expr, TType)]
gens
                                                       in (Double
p',(Expr, TType)
e_ty',(Double, Expr, TType)
gen(Double, Expr, TType)
-> [(Double, Expr, TType)] -> [(Double, Expr, TType)]
forall a. a -> [a] -> [a]
:[(Double, Expr, TType)]
gens')

      pickArg :: [(a, Type)] -> CId -> [(a, Type)] -> [(a, Type, [(a, Type)])]
pickArg [(a, Type)]
args' CId
cat' [] = []
      pickArg [(a, Type)]
args' CId
cat' (arg :: (a, Type)
arg@(a
mb_e,ty :: Type
ty@(DTyp [Hypo]
_ CId
cat [Expr]
_)):[(a, Type)]
args)
        | CId
cat' CId -> CId -> Bool
forall a. Eq a => a -> a -> Bool
== CId
cat = (a
mb_e, Type
ty, ([(a, Type)] -> (a, Type) -> [(a, Type)])
-> [(a, Type)] -> [(a, Type)] -> [(a, Type)]
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (((a, Type) -> [(a, Type)] -> [(a, Type)])
-> [(a, Type)] -> (a, Type) -> [(a, Type)]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (:)) [(a, Type)]
args [(a, Type)]
args') (a, Type, [(a, Type)])
-> [(a, Type, [(a, Type)])] -> [(a, Type, [(a, Type)])]
forall a. a -> [a] -> [a]
: 
                        [(a, Type)] -> CId -> [(a, Type)] -> [(a, Type, [(a, Type)])]
pickArg ((a, Type)
arg(a, Type) -> [(a, Type)] -> [(a, Type)]
forall a. a -> [a] -> [a]
:[(a, Type)]
args') CId
cat' [(a, Type)]
args
        | Bool
otherwise   = [(a, Type)] -> CId -> [(a, Type)] -> [(a, Type, [(a, Type)])]
pickArg ((a, Type)
arg(a, Type) -> [(a, Type)] -> [(a, Type)]
forall a. a -> [a] -> [a]
:[(a, Type)]
args') CId
cat' [(a, Type)]
args