{-# LANGUAGE GADTs, PatternGuards #-}
module Jukebox.Tools.GuessModel where

import Control.Monad
import Jukebox.Name
import Jukebox.Form
import Jukebox.TPTP.Print
import Jukebox.TPTP.ParseSnippet
import Jukebox.Utils

data Universe = Peano | Trees

universe :: Universe -> Type -> NameM ([Function], [Form])
universe :: Universe -> Type -> NameM ([Function], [Form])
universe Universe
Peano = Type -> NameM ([Function], [Form])
peano
universe Universe
Trees = Type -> NameM ([Function], [Form])
trees

peano :: Type -> NameM ([Function], [Form])
peano Type
i = do
  Function
zero <- String -> [Type] -> Type -> NameM Function
forall a. Named a => a -> [Type] -> Type -> NameM Function
newFunction String
"zero" [] Type
i
  Function
succ <- String -> [Type] -> Type -> NameM Function
forall a. Named a => a -> [Type] -> Type -> NameM Function
newFunction String
"succ" [Type
i] Type
i
  Function
pred <- String -> [Type] -> Type -> NameM Function
forall a. Named a => a -> [Type] -> Type -> NameM Function
newFunction String
"pred" [Type
i] Type
i
  let types :: [(String, Type)]
types = [(String
"$i", Type
i)]
      funs :: [(String, Function)]
funs = [(String
"zero", Function
zero),
              (String
"succ", Function
succ),
              (String
"pred", Function
pred)]
  
  let prelude :: [Form]
prelude =
        (String -> Form) -> [String] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map ([(String, Type)] -> [(String, Function)] -> String -> Form
cnf [(String, Type)]
types [(String, Function)]
funs) [
          String
"zero != succ(X)",
          String
"pred(succ(X)) = X"
        ]
  ([Function], [Form]) -> NameM ([Function], [Form])
forall a. a -> NameM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Function
zero, Function
succ], [Form]
prelude)

trees :: Type -> NameM ([Function], [Form])
trees Type
i = do
  Function
nil <- String -> [Type] -> Type -> NameM Function
forall a. Named a => a -> [Type] -> Type -> NameM Function
newFunction String
"nil" [] Type
i
  Function
bin <- String -> [Type] -> Type -> NameM Function
forall a. Named a => a -> [Type] -> Type -> NameM Function
newFunction String
"bin" [Type
i, Type
i] Type
i
  Function
left <- String -> [Type] -> Type -> NameM Function
forall a. Named a => a -> [Type] -> Type -> NameM Function
newFunction String
"left" [Type
i] Type
i
  Function
right <- String -> [Type] -> Type -> NameM Function
forall a. Named a => a -> [Type] -> Type -> NameM Function
newFunction String
"right" [Type
i] Type
i
  let types :: [(String, Type)]
types = [(String
"$i", Type
i)]
      funs :: [(String, Function)]
funs = [(String
"nil", Function
nil),
              (String
"bin", Function
bin),
              (String
"left", Function
left),
              (String
"right", Function
right)]
  
  let prelude :: [Form]
prelude =
        (String -> Form) -> [String] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map ([(String, Type)] -> [(String, Function)] -> String -> Form
cnf [(String, Type)]
types [(String, Function)]
funs) [
          String
"nil != bin(X,Y)",
          String
"left(bin(X,Y)) = X",
          String
"right(bin(X,Y)) = Y"
        ]
  ([Function], [Form]) -> NameM ([Function], [Form])
forall a. a -> NameM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Function
nil, Function
bin], [Form]
prelude)

guessModel :: [String] -> Universe -> Problem Form -> Problem Form
guessModel :: [String] -> Universe -> Problem Form -> Problem Form
guessModel [String]
expansive Universe
univ Problem Form
prob = Problem Form
-> (Problem Form -> NameM (Problem Form)) -> Problem Form
forall a b. Symbolic a => a -> (a -> NameM b) -> b
run Problem Form
prob ((Problem Form -> NameM (Problem Form)) -> Problem Form)
-> (Problem Form -> NameM (Problem Form)) -> Problem Form
forall a b. (a -> b) -> a -> b
$ \Problem Form
forms -> do
  let i :: Type
i = Problem Form -> Type
forall a. Symbolic a => a -> Type
ind Problem Form
forms
  Type
answerType <- String -> NameM Type
forall a. Named a => a -> NameM Type
newType String
"answer"
  Function
answer <- String -> [Type] -> Type -> NameM Function
forall a. Named a => a -> [Type] -> Type -> NameM Function
newFunction String
"$answer" [Type
answerType] Type
O
  let withExpansive :: (Function -> Bool -> Function -> NameM [Form])
-> Function -> NameM [Form]
withExpansive Function -> Bool -> Function -> NameM [Form]
f Function
func = Function -> Bool -> Function -> NameM [Form]
f Function
func (Name -> String
forall a. Named a => a -> String
base (Function -> Name
forall a. Named a => a -> Name
name Function
func) String -> [String] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
expansive) Function
answer
  ([Function]
constructors, [Form]
prelude) <- Universe -> Type -> NameM ([Function], [Form])
universe Universe
univ Type
i
  [Form]
program <- ([[Form]] -> [Form]) -> NameM [[Form]] -> NameM [Form]
forall a b. (a -> b) -> NameM a -> NameM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[Form]] -> [Form]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ((Function -> NameM [Form]) -> [Function] -> NameM [[Form]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((Function -> Bool -> Function -> NameM [Form])
-> Function -> NameM [Form]
withExpansive ([Function] -> Function -> Bool -> Function -> NameM [Form]
function [Function]
constructors)) (Problem Form -> [Function]
forall a. Symbolic a => a -> [Function]
functions Problem Form
forms))
  Problem Form -> NameM (Problem Form)
forall a. a -> NameM a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Form -> Input Form) -> [Form] -> Problem Form
forall a b. (a -> b) -> [a] -> [b]
map (String -> Kind -> InputSource -> Form -> Input Form
forall a. String -> Kind -> InputSource -> a -> Input a
Input String
"adt" (AxKind -> Kind
Ax AxKind
Axiom) InputSource
Unknown) [Form]
prelude Problem Form -> Problem Form -> Problem Form
forall a. [a] -> [a] -> [a]
++
          (Form -> Input Form) -> [Form] -> Problem Form
forall a b. (a -> b) -> [a] -> [b]
map (String -> Kind -> InputSource -> Form -> Input Form
forall a. String -> Kind -> InputSource -> a -> Input a
Input String
"program" (AxKind -> Kind
Ax AxKind
Axiom) InputSource
Unknown) [Form]
program Problem Form -> Problem Form -> Problem Form
forall a. [a] -> [a] -> [a]
++
          Problem Form
forms)

ind :: Symbolic a => a -> Type
ind :: forall a. Symbolic a => a -> Type
ind a
x =
  case a -> [Type]
forall a. Symbolic a => a -> [Type]
types' a
x of
    [Type
ty] -> Type
ty
    [] -> Type
indType
    [Type]
_ -> String -> Type
forall a. HasCallStack => String -> a
error String
"GuessModel: can't deal with many-typed problems"

function :: [Function] -> Function -> Bool -> Function -> NameM [Form]
function :: [Function] -> Function -> Bool -> Function -> NameM [Form]
function [Function]
constructors Function
f Bool
expansive Function
answerP = ([[Form]] -> [Form]) -> NameM [[Form]] -> NameM [Form]
forall a b. (a -> b) -> NameM a -> NameM b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [[Form]] -> [Form]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (NameM [[Form]] -> NameM [Form]) -> NameM [[Form]] -> NameM [Form]
forall a b. (a -> b) -> a -> b
$ do
  [[Term]]
argss <- [Function] -> [Type] -> NameM [[Term]]
cases [Function]
constructors (Function -> [Type]
funArgs Function
f)
  [[Term]] -> ([Term] -> NameM [Form]) -> NameM [[Form]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [[Term]]
argss (([Term] -> NameM [Form]) -> NameM [[Form]])
-> ([Term] -> NameM [Form]) -> NameM [[Form]]
forall a b. (a -> b) -> a -> b
$ \[Term]
args -> do
    Function
fname <- String -> [Type] -> Type -> NameM Function
forall a. Named a => a -> [Type] -> Type -> NameM Function
newFunction (String
"exhausted_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Name -> String
forall a. Named a => a -> String
base (Function -> Name
forall a. Named a => a -> Name
name Function
f) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_case")
               [] ([Type] -> Type
forall a. HasCallStack => [a] -> a
head (Function -> [Type]
funArgs Function
answerP))
    let answer :: Form
answer = Literal -> Form
Literal (Atomic -> Literal
forall a. a -> Signed a
Pos (Term -> Atomic
Tru (Function
answerP Function -> [Term] -> Term
:@: [Function
fname Function -> [Term] -> Term
:@: []])))
    let theRhss :: [Form]
theRhss = [Function] -> [Term] -> Function -> Bool -> Form -> [Form]
rhss [Function]
constructors [Term]
args Function
f Bool
expansive Form
answer
    [Form]
alts <- [Form] -> (Form -> NameM Form) -> NameM [Form]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Form]
theRhss ((Form -> NameM Form) -> NameM [Form])
-> (Form -> NameM Form) -> NameM [Form]
forall a b. (a -> b) -> a -> b
$ \Form
rhs -> do
      Function
pred <- String -> [Type] -> Type -> NameM Function
forall a. Named a => a -> [Type] -> Type -> NameM Function
newFunction ([String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat (String -> [String]
lines (Form -> String
forall a. Pretty a => a -> String
prettyShow Form
rhs))) [] Type
O
      Form -> NameM Form
forall a. a -> NameM a
forall (m :: * -> *) a. Monad m => a -> m a
return (Literal -> Form
Literal (Atomic -> Literal
forall a. a -> Signed a
Pos (Term -> Atomic
Tru (Function
pred Function -> [Term] -> Term
:@: []))))
    [Form] -> NameM [Form]
forall a. a -> NameM a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Form] -> NameM [Form]) -> [Form] -> NameM [Form]
forall a b. (a -> b) -> a -> b
$
      (Form -> Form -> Form) -> Form -> [Form] -> Form
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Form -> Form -> Form
(\/) Form
false [Form]
altsForm -> [Form] -> [Form]
forall a. a -> [a] -> [a]
:
      [ Form -> Form
closeForm (Connective -> Form -> Form -> Form
Connective Connective
Implies Form
alt Form
rhs)
      | (Form
alt, Form
rhs) <- [Form] -> [Form] -> [(Form, Form)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Form]
alts [Form]
theRhss ]

rhss :: [Function] -> [Term] -> Function -> Bool -> Form -> [Form]
rhss :: [Function] -> [Term] -> Function -> Bool -> Form -> [Form]
rhss [Function]
constructors [Term]
args Function
f Bool
expansive Form
answer =
  case Function -> Type
forall a. Typed a => a -> Type
typ Function
f of
    Type
O ->
      Literal -> Form
Literal (Atomic -> Literal
forall a. a -> Signed a
Pos (Term -> Atomic
Tru (Function
f Function -> [Term] -> Term
:@: [Term]
args)))Form -> [Form] -> [Form]
forall a. a -> [a] -> [a]
:
      Literal -> Form
Literal (Atomic -> Literal
forall a. a -> Signed a
Neg (Term -> Atomic
Tru (Function
f Function -> [Term] -> Term
:@: [Term]
args)))Form -> [Form] -> [Form]
forall a. a -> [a] -> [a]
:
      (Term -> Form) -> [Term] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Form
its (([Term] -> Term) -> [[Term]] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Function
f Function -> [Term] -> Term
:@:) ([Term] -> [[Term]]
recursive [Term]
args))
    Type
_ | Bool
expansive -> (Term -> Form) -> [Term] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Form
its ([Term] -> [Term]
forall a. Ord a => [a] -> [a]
usort ([Term]
unconditional [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term]
constructor))
      | Bool
otherwise -> (Term -> Form) -> [Term] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Form
its ([Term] -> [Term]
forall a. Ord a => [a] -> [a]
usort [Term]
unconditional) [Form] -> [Form] -> [Form]
forall a. [a] -> [a] -> [a]
++ [Form
answer]
  where recursive :: [Term] -> [[Term]]
recursive [] = []
        recursive (Term
a:[Term]
as) = Term -> [[Term]]
reduce Term
a [[Term]] -> [[Term]] -> [[Term]]
forall a. [a] -> [a] -> [a]
++ ([Term] -> [Term]) -> [[Term]] -> [[Term]]
forall a b. (a -> b) -> [a] -> [b]
map (Term
aTerm -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:) ([Term] -> [[Term]]
recursive [Term]
as)
          where reduce :: Term -> [[Term]]
reduce (Function
_f :@: [Term]
xs) = [ Term
xTerm -> [Term] -> [Term]
forall a. a -> [a] -> [a]
:[Term]
as' | Term
x <- [Term]
xs, [Term]
as' <- [Term]
as[Term] -> [[Term]] -> [[Term]]
forall a. a -> [a] -> [a]
:[Term] -> [[Term]]
recursive [Term]
as ]
                reduce Term
_ = []
        constructor :: [Term]
constructor = [ Function
c Function -> [Term] -> Term
:@: [Term]
xs
                      | Function
c <- [Function]
constructors,
                        [Term]
xs <- [[Term]] -> [[Term]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence (Int -> [Term] -> [[Term]]
forall a. Int -> a -> [a]
replicate (Function -> Int
arity Function
c) [Term]
unconditional) ]
        
        subterm :: [Term]
subterm = [Term] -> [Term]
forall a. Symbolic a => a -> [Term]
terms [Term]
args
        its :: Term -> Form
its Term
t = Function
f Function -> [Term] -> Term
:@: [Term]
args Term -> Term -> Form
.=. Term
t
        unconditional :: [Term]
unconditional = ([Term] -> Term) -> [[Term]] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Function
f Function -> [Term] -> Term
:@:) ([Term] -> [[Term]]
recursive [Term]
args) [Term] -> [Term] -> [Term]
forall a. [a] -> [a] -> [a]
++ [Term]
subterm

cases :: [Function] -> [Type] -> NameM [[Term]]
cases :: [Function] -> [Type] -> NameM [[Term]]
cases [Function]
_constructors [] = [[Term]] -> NameM [[Term]]
forall a. a -> NameM a
forall (m :: * -> *) a. Monad m => a -> m a
return [[]]
cases [Function]
constructors (Type
ty:[Type]
tys) = do
  [Term]
ts <- [Function] -> Type -> NameM [Term]
cases1 [Function]
constructors Type
ty
  [[Term]]
tss <- [Function] -> [Type] -> NameM [[Term]]
cases [Function]
constructors [Type]
tys
  [[Term]] -> NameM [[Term]]
forall a. a -> NameM a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Term -> [Term] -> [Term]) -> [Term] -> [[Term]] -> [[Term]]
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (:) [Term]
ts [[Term]]
tss)

cases1 :: [Function] -> Type -> NameM [Term]
cases1 :: [Function] -> Type -> NameM [Term]
cases1 [Function]
constructors Type
ty = do
  let maxArity :: Int
maxArity = [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ((Function -> Int) -> [Function] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Function -> Int
arity [Function]
constructors)
      varNames :: [String]
varNames = Int -> [String] -> [String]
forall a. Int -> [a] -> [a]
take Int
maxArity ([String] -> [String]
forall a. HasCallStack => [a] -> [a]
cycle [String
"X", String
"Y", String
"Z"])
  [Name ::: Type]
vars <- (String -> NameM (Name ::: Type))
-> [String] -> NameM [Name ::: Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((String -> Type -> NameM (Name ::: Type))
-> Type -> String -> NameM (Name ::: Type)
forall a b c. (a -> b -> c) -> b -> a -> c
flip String -> Type -> NameM (Name ::: Type)
forall a b. Named a => a -> b -> NameM (Name ::: b)
newSymbol Type
ty) [String]
varNames
  [Term] -> NameM [Term]
forall a. a -> NameM a
forall (m :: * -> *) a. Monad m => a -> m a
return [ Function
c Function -> [Term] -> Term
:@: Int -> [Term] -> [Term]
forall a. Int -> [a] -> [a]
take (Function -> Int
arity Function
c) (((Name ::: Type) -> Term) -> [Name ::: Type] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Name ::: Type) -> Term
Var [Name ::: Type]
vars)
         | Function
c <- [Function]
constructors ]