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