{-# 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 ]