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)
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
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
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
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 ()]
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
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)
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
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'])
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
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
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