{-# 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 <- [Char] -> [Type] -> Type -> NameM Function
forall a. Named a => a -> [Type] -> Type -> NameM Function
newFunction [Char]
"zero" [] Type
i
  Function
succ <- [Char] -> [Type] -> Type -> NameM Function
forall a. Named a => a -> [Type] -> Type -> NameM Function
newFunction [Char]
"succ" [Type
i] Type
i
  Function
pred <- [Char] -> [Type] -> Type -> NameM Function
forall a. Named a => a -> [Type] -> Type -> NameM Function
newFunction [Char]
"pred" [Type
i] Type
i
  let types :: [([Char], Type)]
types = [([Char]
"$i", Type
i)]
      funs :: [([Char], Function)]
funs = [([Char]
"zero", Function
zero),
              ([Char]
"succ", Function
succ),
              ([Char]
"pred", Function
pred)]
  
  let prelude :: [Form]
prelude =
        ([Char] -> Form) -> [[Char]] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map ([([Char], Type)] -> [([Char], Function)] -> [Char] -> Form
cnf [([Char], Type)]
types [([Char], Function)]
funs) [
          [Char]
"zero != succ(X)",
          [Char]
"pred(succ(X)) = X"
        ]
  ([Function], [Form]) -> NameM ([Function], [Form])
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 <- [Char] -> [Type] -> Type -> NameM Function
forall a. Named a => a -> [Type] -> Type -> NameM Function
newFunction [Char]
"nil" [] Type
i
  Function
bin <- [Char] -> [Type] -> Type -> NameM Function
forall a. Named a => a -> [Type] -> Type -> NameM Function
newFunction [Char]
"bin" [Type
i, Type
i] Type
i
  Function
left <- [Char] -> [Type] -> Type -> NameM Function
forall a. Named a => a -> [Type] -> Type -> NameM Function
newFunction [Char]
"left" [Type
i] Type
i
  Function
right <- [Char] -> [Type] -> Type -> NameM Function
forall a. Named a => a -> [Type] -> Type -> NameM Function
newFunction [Char]
"right" [Type
i] Type
i
  let types :: [([Char], Type)]
types = [([Char]
"$i", Type
i)]
      funs :: [([Char], Function)]
funs = [([Char]
"nil", Function
nil),
              ([Char]
"bin", Function
bin),
              ([Char]
"left", Function
left),
              ([Char]
"right", Function
right)]
  
  let prelude :: [Form]
prelude =
        ([Char] -> Form) -> [[Char]] -> [Form]
forall a b. (a -> b) -> [a] -> [b]
map ([([Char], Type)] -> [([Char], Function)] -> [Char] -> Form
cnf [([Char], Type)]
types [([Char], Function)]
funs) [
          [Char]
"nil != bin(X,Y)",
          [Char]
"left(bin(X,Y)) = X",
          [Char]
"right(bin(X,Y)) = Y"
        ]
  ([Function], [Form]) -> NameM ([Function], [Form])
forall (m :: * -> *) a. Monad m => a -> m a
return ([Function
nil, Function
bin], [Form]
prelude)

guessModel :: [String] -> Universe -> Problem Form -> Problem Form
guessModel :: [[Char]] -> Universe -> Problem Form -> Problem Form
guessModel [[Char]]
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 <- [Char] -> NameM Type
forall a. Named a => a -> NameM Type
newType [Char]
"answer"
  Function
answer <- [Char] -> [Type] -> Type -> NameM Function
forall a. Named a => a -> [Type] -> Type -> NameM Function
newFunction [Char]
"$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 -> [Char]
forall a. Named a => a -> [Char]
base (Function -> Name
forall a. Named a => a -> Name
name Function
func) [Char] -> [[Char]] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [[Char]]
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 (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)
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 (m :: * -> *) a. Monad m => a -> m a
return ((Form -> Input Form) -> [Form] -> Problem Form
forall a b. (a -> b) -> [a] -> [b]
map ([Char] -> Kind -> InputSource -> Form -> Input Form
forall a. [Char] -> Kind -> InputSource -> a -> Input a
Input [Char]
"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 ([Char] -> Kind -> InputSource -> Form -> Input Form
forall a. [Char] -> Kind -> InputSource -> a -> Input a
Input [Char]
"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 :: 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]
_ -> [Char] -> Type
forall a. HasCallStack => [Char] -> a
error [Char]
"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 (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 <- [Char] -> [Type] -> Type -> NameM Function
forall a. Named a => a -> [Type] -> Type -> NameM Function
newFunction ([Char]
"exhausted_" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Name -> [Char]
forall a. Named a => a -> [Char]
base (Function -> Name
forall a. Named a => a -> Name
name Function
f) [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
"_case")
               [] ([Type] -> Type
forall a. [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 <- [Char] -> [Type] -> Type -> NameM Function
forall a. Named a => a -> [Type] -> Type -> NameM Function
newFunction ([[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([Char] -> [[Char]]
lines (Form -> [Char]
forall a. Pretty a => a -> [Char]
prettyShow Form
rhs))) [] Type
O
      Form -> NameM Form
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 (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 (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)
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 (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 (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 (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 :: [[Char]]
varNames = Int -> [[Char]] -> [[Char]]
forall a. Int -> [a] -> [a]
take Int
maxArity ([[Char]] -> [[Char]]
forall a. [a] -> [a]
cycle [[Char]
"X", [Char]
"Y", [Char]
"Z"])
  [Name ::: Type]
vars <- ([Char] -> NameM (Name ::: Type))
-> [[Char]] -> NameM [Name ::: Type]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (([Char] -> Type -> NameM (Name ::: Type))
-> Type -> [Char] -> NameM (Name ::: Type)
forall a b c. (a -> b -> c) -> b -> a -> c
flip [Char] -> Type -> NameM (Name ::: Type)
forall a b. Named a => a -> b -> NameM (Name ::: b)
newSymbol Type
ty) [[Char]]
varNames
  [Term] -> NameM [Term]
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 ]