djinn (empty) → 2008.1.18
raw patch · 14 files changed
+2464/−0 lines, 14 filesdep +arraydep +basedep +containersbuild-type:Customsetup-changed
Dependencies added: array, base, containers, mtl, pretty, readline
Files
- Djinn/Djinn.hs +387/−0
- Djinn/HCheck.hs +152/−0
- Djinn/HTypes.hs +452/−0
- Djinn/Help.hs +177/−0
- Djinn/LJT.hs +468/−0
- Djinn/LJTFormula.hs +103/−0
- Djinn/LJTParse.hs +98/−0
- Djinn/MLJT.hs +30/−0
- Djinn/REPL.hs +34/−0
- Djinn/Util/Digraph.hs +393/−0
- Djinn/Util/Sort.hs +110/−0
- LICENSE +32/−0
- Setup.lhs +6/−0
- djinn.cabal +22/−0
+ Djinn/Djinn.hs view
@@ -0,0 +1,387 @@+--+-- Copyright (c) 2005 Lennart Augustsson+-- See LICENSE for licensing details.+--+module Main(main) where+import Data.Char(isAlpha, isSpace, isAlphaNum)+import Data.List(sortBy, nub, intersperse)+import Data.Ratio+import Text.ParserCombinators.ReadP+import Control.Monad(when)+import Control.Monad.Error()+import System.IO+import System.Exit+import System.Environment++import REPL+import LJT+--import MJ+import HTypes+import HCheck(htCheckEnv, htCheckType)+import Help++main :: IO ()+main = do+ args <- getArgs+ let decodeOptions (('-':cs) : as) st = decodeOption cs >>= \f -> decodeOptions as (f False st)+ decodeOptions (('+':cs) : as) st = decodeOption cs >>= \f -> decodeOptions as (f True st)+ decodeOptions as st = return (as, st)+ decodeOption cs = case [ set | (cmd, _, _, set) <- options, isPrefix cs cmd ] of+ [] -> do usage; exitWith (ExitFailure 1)+ set : _ -> return set+ (args', state) <- decodeOptions args startState+ case args' of+ [] -> repl (hsGenRepl state)+ _ -> loop state args'+ where loop _ [] = return ()+ loop s (a:as) = do+ putStrLn $ "-- loading file " ++ a+ (q, s') <- loadFile s a+ if q then+ return ()+ else+ loop s' as++usage :: IO ()+usage = putStrLn "Usage: djinn [option ...] [file ...]"++hsGenRepl :: State -> REPL State+hsGenRepl state = REPL {+ repl_init = inIt state,+ repl_eval = eval,+ repl_exit = exit+ }++data State = State {+ synonyms :: [(HSymbol, ([HSymbol], HType, HKind))],+ axioms :: [(HSymbol, HType)],+ classes :: [ClassDef],+ multi :: Bool,+ sorted :: Bool,+ debug :: Bool,+ cutOff :: Int+ }+ deriving (Show)++startState :: State+startState = State {+ synonyms = syns,+ classes = clss,+ axioms = [],+ multi = False,+ sorted = True,+ debug = False,+ cutOff = 100+ }+ where syns = either (const $ error "Bad initial environment") id $ htCheckEnv $ reverse [+ ("()", ([], HTUnion [("()",[])], undefined)),+ ("Either", (["a","b"], HTUnion [("Left", [HTVar "a"]), ("Right", [HTVar "b"])], undefined)),+ ("Maybe", (["a"], HTUnion [("Nothing", []), ("Just", [HTVar "a"])], undefined)),+ ("Bool", ([], HTUnion [("False", []), ("True", [])], undefined)),+ ("Void", ([], HTUnion [], undefined)),+ ("Not", (["x"], htNot "x", undefined))+ ]+ clss = [("Eq", (["a"], [("==", a `HTArrow` (a `HTArrow` HTCon "Bool"))]))]+ a = HTVar "a"+++version :: String+version = "version 2008-01-18"++inIt :: State -> IO (String, State)+inIt state = do+ putStrLn $ "Welcome to Djinn " ++ version ++ "."+ putStrLn $ "Type :h to get help."+ return ("Djinn> ", state)++eval :: State -> String -> IO (Bool, State)+eval s line =+ case filter (null . snd) (readP_to_S pCmd line) of+ [] -> do+ putStrLn $ "Cannot parse command"+ return (False, s)+ (cmd, "") : _ -> runCmd s cmd+ _ -> error "eval"++exit :: State -> IO ()+exit _s = do+ putStrLn "Bye."+ return ()++type Context = (HSymbol, [HType])+type ClassDef = (HSymbol, ([HSymbol], [Method]))++data Cmd = Help Bool | Quit | Add HSymbol HType | Query HSymbol [Context] HType | Del HSymbol | Load HSymbol | Noop | Env |+ Type (HSymbol, ([HSymbol], HType, HKind)) | Set (State -> State) | Clear | Class ClassDef++pCmd :: ReadP Cmd+pCmd = do+ skipSpaces+ let adds (':':s) p = do schar ':'; pPrefix (takeWhile (/= ' ') s); c <- p; skipSpaces; return c+ adds _ p = do c <- p; skipSpaces; return c+ cmd <- foldr1 (+++) [ adds s p | (s, _, p) <- commands ]+ skipSpaces+ return cmd++pPrefix :: String -> ReadP String+pPrefix s = do+ skipSpaces+ cs <- look+ let w = takeWhile isAlpha cs+ if isPrefix w s then+ string w+ else+ pfail++isPrefix :: String -> String -> Bool+isPrefix p s = not (null p) && length p <= length s && take (length p) s == p++runCmd :: State -> Cmd -> IO (Bool, State)+runCmd s Noop = return (False, s)+runCmd s (Help verbose) = do+ putStr $ helpText ++ unlines (map getHelp commands) ++ getSettings s+ when verbose $ putStr verboseHelp+ return (False, s)+runCmd s Quit = + return (True, s)+runCmd s (Load f) = loadFile s f+runCmd s (Add i t) = + case htCheckType (synonyms s) t of+ Left msg -> do putStrLn $ "Error: " ++ msg; return (False, s)+ Right _ -> return (False, s { axioms = (i, t) : axioms s })+runCmd _ Clear =+ return (False, startState)+runCmd s (Del i) = + return (False, s { axioms = filter ((i /=) . fst) (axioms s)+ , synonyms = filter ((i /=) . fst) (synonyms s)+ , classes = filter ((i /=) . fst) (classes s) })+runCmd s Env = do+-- print s+ let tname t = if isHTUnion t then "data" else "type"+ showd (HTUnion []) = ""+ showd t = " = " ++ show t+ mapM_ (\ (i, (vs, t, _)) -> putStrLn $ tname t ++ " " ++ unwords (i:vs) ++ showd t) (reverse $ synonyms s)+ mapM_ (\ (i, t) -> putStrLn $ i ++ " :: " ++ show t) (reverse $ axioms s)+ mapM_ (putStrLn . showClass) (reverse $ classes s)+ return (False, s)+runCmd s (Type syn) = do+ case htCheckEnv (syn : synonyms s) of+ Left msg -> do putStrLn $ "Error: " ++ msg; return (False, s)+ Right syns -> return (False, s { synonyms = syns })+runCmd s (Set f) =+ return (False, f s)+runCmd s (Query i ctx g) =+ case htCheckType (synonyms s) g >> mapM (ctxLookup (classes s)) ctx of+ Left msg -> do putStrLn $ "Error: " ++ msg; return (False, s)+ Right mss -> do+ let form = hTypeToFormula (synonyms s) g+ env = [ (Symbol v, hTypeToFormula (synonyms s) t) | (v, t) <- axioms s ] ++ ctxEnv+ ctxEnv = [ (Symbol v, hTypeToFormula (synonyms s) t) | ms <- mss, (v, t) <- ms ]+ mpr = prove (multi s || sorted s) env form+ when (debug s) $ putStrLn ("*** " ++ show form)+ case mpr of+ [] -> do+ putStrLn $ "-- " ++ i ++ " cannot be realized."+ return (False, s)+ ps -> do+ let f p =+ let c = termToHClause i p+ bvs = getBinderVars c+ r = if null bvs then (0, 0) else (length (filter (== "_") bvs) % length bvs, length bvs)+ in (r, c)+ e:es = nub $ + if sorted s then+ map snd $ sortBy (\ (x,_) (y,_) -> compare x y) $ map f $ take (cutOff s) ps+ else+ map (termToHClause i) $ take (cutOff s) ps+ pr = putStrLn . hPrClause+ sctx = if null ctx then "" else showContexts ctx ++ " => "+ when (debug s) $ putStrLn ("+++ " ++ show (head ps))+ putStrLn $ i ++ " :: " ++ sctx ++ show g+ pr e+ when (multi s) $ mapM_ (\ x -> putStrLn "-- or" >> pr x) es+ return (False, s)+runCmd s (Class c) = do+ return (False, s { classes = c : classes s })++loadFile :: State -> String -> IO (Bool, State)+loadFile s name = do+ file <- readFile name+ evalCmds s $ lines $ stripComments file++stripComments :: String -> String+stripComments "" = ""+stripComments ('-':'-':cs) = skip cs+ where skip "" = ""+ skip s@('\n':_) = stripComments s+ skip (_:s) = skip s+stripComments (c:cs) = c : stripComments cs++showClass :: ClassDef -> String+showClass (c, (as, ms)) = "class " ++ showContext (c, map HTVar as) ++ " where " ++ concat (intersperse "; " $ map sm ms)+ where sm (i, t) = pp i ++ " :: " ++ show t+ pp i@(ch:_) | not (isAlphaNum ch) = "(" ++ i ++ ")"+ pp i = i++showContext :: Context -> String+showContext (c, as) = show $ foldl HTApp (HTCon c) as++showContexts :: [Context] -> String+showContexts [] = ""+showContexts cs = "(" ++ concat (intersperse ", " $ map showContext cs) ++ ")"++ctxLookup :: [ClassDef] -> Context -> Either String [Method]+ctxLookup clss (c, as) =+ case lookup c clss of+ Nothing -> Left $ "Class not found: " ++ c+ Just (ps, ms) -> Right [(m, substHT (zip ps as) t) | (m, t) <- ms ]++evalCmds :: State -> [String] -> IO (Bool, State)+evalCmds state [] = return (False, state)+evalCmds state (l:ls) = do+ qs@(q, state') <- eval state l+ if q then+ return qs+ else+ evalCmds state' ls++commands :: [(String, String, ReadP Cmd)]+commands = [+ (":clear", "Clear the envirnment", return Clear),+ (":delete <sym>", "Delete from environment.", pDel),+ (":environment", "Show environment", return Env),+ (":help", "Print this message.", return (Help False)),+ (":load <file>", "Load a file", pLoad),+ (":quit", "Quit program.", return Quit),+ (":set <option>", "Set options", pSet),+ (":verbose-help", "Print verbose help.", return (Help True)),+ ("type <sym> <vars> = <type>", "Add a type synonym", pType),+ ("data <sym> <vars> = <datatype>", "Add a data type", pData),+ ("class <sym> <vars> where <method>...", "Add a class", pClass),+ ("<sym> :: <type>", "Add to environment", pAdd),+ ("<sym> ? <type>", "Query", pQuery),+ ("", "", return Noop)+ ]++options :: [(String, String, State->Bool, Bool->State->State)]+options = [+ ("multi", "print multiple solutions", multi, \ v s -> s { multi = v }),+ ("sorted", "sort solutions", sorted, \ v s -> s { sorted = v }),+ ("debug", "debug mode", debug, \ v s -> s { debug = v })+ ]++getHelp :: (String, String, a) -> String+getHelp (cmd, help, _) = cmd ++ replicate (35 - length cmd) ' ' ++ help++pDel :: ReadP Cmd+pDel = do+ s <- pHSymbol True +++ pHSymbol False+ return $ Del s++pLoad :: ReadP Cmd+pLoad = do+ skipSpaces+ s <- munch1 (not . isSpace)+ return $ Load s++pAdd :: ReadP Cmd+pAdd = do+ i <- pHSymbol False+ sstring "::"+ t <- pHType+ optional $ schar ';'+ return $ Add i t++pQuery :: ReadP Cmd+pQuery = do+ i <- pHSymbol False+ schar '?'+ c <- option [] pContext+ t <- pHType+ optional $ schar ';'+ return $ Query i c t++pContext :: ReadP [Context]+pContext = do+ let pCtx = do c <- pHSymbol True; ts <- many pHTAtom; return (c, ts)+ schar '('+ ctx <- sepBy1 pCtx (schar ',')+ schar ')'+ sstring "=>"+ return ctx++pType :: ReadP Cmd+pType = do+ sstring "type"+ syn <- pHSymbol True+ args <- many (pHSymbol False)+ schar '='+ t <- pHType+ return $ Type (syn, (args, t, undefined))++pData :: ReadP Cmd+pData = do+ sstring "data"+ syn <- pHSymbol True+ args <- many (pHSymbol False)+ (do schar '='; t <- pHDataType; return $ Type (syn, (args, t, undefined))) +++ (return $ Type (syn, (args, HTUnion [], undefined)))++pClass :: ReadP Cmd+pClass = do+ sstring "class"+ cls <- pHSymbol True+ args <- many (pHSymbol False)+ sstring "where"+ mets <- sepBy pMethod (schar ';')+ return $ Class (cls, (args, mets))++type Method = (HSymbol, HType)++pMethod :: ReadP Method+pMethod = do+ let pOpSym = satisfy (`elem` "~!#$%^&*-+=<>.:")+ i <- pHSymbol False +++ do schar '('; op <- many1 pOpSym; schar ')'; return op+ sstring "::"+ t <- pHType+ return (i, t)++pSet :: ReadP Cmd+pSet = do+ val <- (do schar '+'; return True) +++ (do schar '-'; return False) + f <- foldr (+++) pfail [ do pPrefix s; return (set val) | (s, _, _, set) <- options ]+ return $ Set $ f++schar :: Char -> ReadP ()+schar c = do+ skipSpaces+ char c+ return ()++sstring :: String -> ReadP ()+sstring s = do+ skipSpaces+ string s+ return ()++helpText :: String+helpText = "\+\Djinn is a program that generates Haskell code from a type.\n\+\Given a type the program will deduce an expression of this type,\n\+\if one exists. If the Djinn says the type is not realizable it is\n\+\because there is no (total) expression of the given type.\n\+\Djinn only knows about tuples, ->, and some data types in the\n\+\initial environment (do :e for a list).\n\+\\n\+\Caveat emptor: The expression will have the right type, but it\n\+\may not be what you were looking for.\n\+\\n\+\Send any comments and feedback to lennart@augustsson.net\n\+\\n\+\Commands (may be abbreviated):\n\+\"++getSettings :: State -> String+getSettings s = unlines $ [+ "",+ "Current settings" ] ++ [ " " ++ (if gett s then "+" else "-") ++ name ++ replicate (10 - length name) ' ' ++ descr |+ (name, descr, gett, _set) <- options ]
+ Djinn/HCheck.hs view
@@ -0,0 +1,152 @@+--+-- Copyright (c) 2005 Lennart Augustsson+-- See LICENSE for licensing details.+--+module HCheck(htCheckEnv, htCheckType) where+import Data.List(union)+--import Control.Monad.Trans+import Control.Monad.Error()+import Control.Monad.State+import Data.IntMap(IntMap, insert, (!), empty)++import Util.Digraph(stronglyConnComp, SCC(..))++import HTypes++--import Debug.Trace++type KState = (Int, IntMap (Maybe HKind))+initState :: KState+initState = (0, empty)++type M a = StateT KState (Either String) a++type KEnv = [(HSymbol, HKind)]++newKVar :: M HKind+newKVar = do+ (i, m) <- get+ put (i+1, insert i Nothing m)+ return $ KVar i++getVar :: Int -> M (Maybe HKind)+getVar i = do+ (_, m) <- get+ case m!i of+ Just (KVar i') -> getVar i'+ mk -> return mk++addMap :: Int -> HKind -> M ()+addMap i k = do+ (n, m) <- get+ put (n, insert i (Just k) m)++clearState :: M ()+clearState = put initState++htCheckType :: [(HSymbol, ([HSymbol], HType, HKind))] -> HType -> Either String ()+htCheckType its t = flip evalStateT initState $ do+ let vs = getHTVars t+ ks <- mapM (const newKVar) vs+ let env = zip vs ks ++ [(i, k) | (i, (_, _, k)) <- its ]+ iHKindStar env t ++htCheckEnv :: [(HSymbol, ([HSymbol], HType, a))] -> Either String [(HSymbol, ([HSymbol], HType, HKind))]+htCheckEnv its =+ let graph = [ (n, i, getHTCons t) | n@(i, (_, t, _)) <- its ]+ order = stronglyConnComp graph+ in case [ c | CyclicSCC c <- order ] of+ c : _ -> Left $ "Recursive types are not allowed: " ++ unwords [ i | (i, _) <- c ]+ [] -> flip evalStateT initState $ addKinds+ where addKinds = do+ env <- inferHKinds [] $ map (\ (AcyclicSCC n) -> n) order+ let getK i = maybe (error $ "htCheck " ++ i) id $ lookup i env+ return [ (i, (vs, t, getK i)) | (i, (vs, t, _)) <- its ]++inferHKinds :: KEnv -> [(HSymbol, ([HSymbol], HType, a))] -> M KEnv+inferHKinds env [] = return env+inferHKinds env ((i, (vs, t, _)) : its) = do+ k <- inferHKind env vs t+ inferHKinds ((i, k) : env) its++inferHKind :: KEnv -> [HSymbol] -> HType -> M HKind+inferHKind env vs t = do+ clearState+ ks <- mapM (const newKVar) vs+ let env' = zip vs ks ++ env+ k <- iHKind env' t+ ground $ foldr KArrow k ks++iHKind :: KEnv -> HType -> M HKind+iHKind env (HTApp f a) = do+ kf <- iHKind env f+ ka <- iHKind env a+ r <- newKVar+ unifyK (KArrow ka r) kf+ return r+iHKind env (HTVar v) = do+ getVarHKind env v+iHKind env (HTCon c) = do+ getConHKind env c+iHKind env (HTTuple ts) = do+ mapM_ (iHKindStar env) ts+ return KStar+iHKind env (HTArrow f a) = do+ iHKindStar env f+ iHKindStar env a+ return KStar+iHKind env (HTUnion cs) = do+ mapM_ (\ (_, ts) -> mapM_ (iHKindStar env) ts) cs+ return KStar++iHKindStar :: KEnv -> HType -> M ()+iHKindStar env t = do+ k <- iHKind env t+ unifyK k KStar++unifyK :: HKind -> HKind -> M ()+unifyK k1 k2 = do+ let follow k@(KVar i) = getVar i >>= return . maybe k id + follow k = return k+ unify KStar KStar = return ()+ unify (KArrow k11 k12) (KArrow k21 k22) = do unifyK k11 k21; unifyK k12 k22+ unify (KVar i1) (KVar i2) | i1 == i2 = return ()+ unify (KVar i) k = do occurs i k; addMap i k+ unify k (KVar i) = do occurs i k; addMap i k+ unify _ _ = lift $ Left "kind error"+ occurs _ KStar = return ()+ occurs i (KArrow f a) = do follow f >>= occurs i; follow a >>= occurs i+ occurs i (KVar i') = if i == i' then lift $ Left "cyclic kind" else return ()+ k1' <- follow k1+ k2' <- follow k2+ unify k1' k2'+ ++getVarHKind :: KEnv -> HSymbol -> M HKind+getVarHKind env v =+ case lookup v env of+ Just k -> return k+ Nothing -> lift $ Left $ "type variable not bound " ++ v++getConHKind :: KEnv -> HSymbol -> M HKind+getConHKind env v =+ case lookup v env of+ Just k -> return k+ Nothing -> newKVar -- allow uninterpreted type constructors++ground :: HKind -> M HKind+ground KStar = return KStar+ground (KArrow k1 k2) = liftM2 KArrow (ground k1) (ground k2)+ground (KVar i) = do+ mk <- getVar i+ case mk of+ Just k -> return k+ Nothing -> return KStar++getHTCons :: HType -> [HSymbol]+getHTCons (HTApp f a) = getHTCons f `union` getHTCons a+getHTCons (HTVar _) = []+getHTCons (HTCon s) = [s]+getHTCons (HTTuple ts) = foldr union [] (map getHTCons ts)+getHTCons (HTArrow f a) = getHTCons f `union` getHTCons a+getHTCons (HTUnion alts) = foldr union [] [ getHTCons t | (_, ts) <- alts, t <- ts ]
+ Djinn/HTypes.hs view
@@ -0,0 +1,452 @@+--+-- Copyright (c) 2005 Lennart Augustsson+-- See LICENSE for licensing details.+--+module HTypes(HKind(..), HType(..), HSymbol, hTypeToFormula, pHSymbol, pHType, pHDataType, pHTAtom,+ htNot, isHTUnion, getHTVars, substHT,+ HClause, HPat, HExpr(HEVar), hPrClause, termToHExpr, termToHClause, getBinderVars) where+import Text.PrettyPrint.HughesPJ(Doc, renderStyle, style, text, (<>), parens, ($$), vcat, punctuate,+ sep, fsep, nest, comma, (<+>))+import Data.Char(isAlphaNum, isAlpha, isUpper)+import Data.List(union, (\\))+import Control.Monad(zipWithM)+import Text.ParserCombinators.ReadP+import LJTFormula++--import Debug.Trace++type HSymbol = String++data HKind+ = KStar+ | KArrow HKind HKind+ | KVar Int+ deriving (Eq, Show)++data HType+ = HTApp HType HType+ | HTVar HSymbol+ | HTCon HSymbol+ | HTTuple [HType]+ | HTArrow HType HType+ | HTUnion [(HSymbol, [HType])] -- Only for data types; only at top level+ deriving (Eq)++isHTUnion :: HType -> Bool+isHTUnion (HTUnion _) = True+isHTUnion _ = False++htNot :: HSymbol -> HType+htNot x = HTArrow (HTVar x) (HTCon "Void")++instance Show HType where+ showsPrec _ (HTApp (HTCon "[]") t) = showString "[" . showsPrec 0 t . showString "]"+ showsPrec p (HTApp f a) = showParen (p > 2) $ showsPrec 2 f . showString " " . showsPrec 3 a+ showsPrec _ (HTVar s) = showString s+ showsPrec _ (HTCon s) = showString s+ showsPrec _ (HTTuple ss) = showParen True $ f ss+ where f [] = error "showsPrec HType"+ f [t] = showsPrec 0 t+ f (t:ts) = showsPrec 0 t . showString ", " . f ts+ showsPrec p (HTArrow s t) = showParen (p > 0) $ showsPrec 1 s . showString " -> " . showsPrec 0 t+ showsPrec _ (HTUnion cs) = f cs+ where f [] = id+ f [cts] = scts cts+ f (cts : ctss) = scts cts . showString " | " . f ctss+ scts (c, ts) = foldl (\ s t -> s . showString " " . showsPrec 10 t) (showString c) ts++instance Read HType where+ readsPrec _ = readP_to_S pHType'++pHType' :: ReadP HType+pHType' = do+ t <- pHType+ skipSpaces+ return t++pHType :: ReadP HType+pHType = do+ ts <- sepBy1 pHTypeApp (do schar '-'; char '>')+ return $ foldr1 HTArrow ts++pHDataType :: ReadP HType+pHDataType = do+ let con = do+ c <- pHSymbol True+ ts <- many pHTAtom+ return (c, ts)+ cts <- sepBy con (schar '|')+ return $ HTUnion cts++pHTAtom :: ReadP HType+pHTAtom = pHTVar +++ pHTCon +++ pHTList +++ pParen pHTTuple +++ pParen pHType +++ pUnit++pUnit :: ReadP HType+pUnit = do+ schar '('+ char ')'+ return $ HTCon "()"++pHTCon :: ReadP HType+pHTCon = pHSymbol True >>= return . HTCon++pHTVar :: ReadP HType+pHTVar = pHSymbol False >>= return . HTVar++pHSymbol :: Bool -> ReadP HSymbol+pHSymbol con = do+ skipSpaces+ c <- satisfy $ \ c -> isAlpha c && isUpper c == con+ let isSym d = isAlphaNum d || d == '\'' || d == '.'+ cs <- munch isSym+ return $ c:cs++pHTTuple :: ReadP HType+pHTTuple = do+ t <- pHType+ ts <- many1 (do schar ','; pHType)+ return $ HTTuple $ t:ts++pHTypeApp :: ReadP HType+pHTypeApp = do+ ts <- many1 pHTAtom+ return $ foldl1 HTApp ts++pHTList :: ReadP HType+pHTList = do+ schar '['+ t <- pHType+ schar ']'+ return $ HTApp (HTCon "[]") t++pParen :: ReadP a -> ReadP a+pParen p = do+ schar '('+ e <- p+ schar ')'+ return e++schar :: Char -> ReadP ()+schar c = do+ skipSpaces+ char c+ return ()++getHTVars :: HType -> [HSymbol]+getHTVars (HTApp f a) = getHTVars f `union` getHTVars a+getHTVars (HTVar v) = [v]+getHTVars (HTCon _) = []+getHTVars (HTTuple ts) = foldr union [] (map getHTVars ts)+getHTVars (HTArrow f a) = getHTVars f `union` getHTVars a+getHTVars _ = error "getHTVars"++-------------------------------++hTypeToFormula :: [(HSymbol, ([HSymbol], HType, a))] -> HType -> Formula+hTypeToFormula ss (HTTuple ts) = Conj (map (hTypeToFormula ss) ts)+hTypeToFormula ss (HTArrow t1 t2) = hTypeToFormula ss t1 :-> hTypeToFormula ss t2+hTypeToFormula ss (HTUnion ctss) = Disj [ (ConsDesc c (length ts), hTypeToFormula ss (HTTuple ts)) | (c, ts) <- ctss ]+hTypeToFormula ss t = + case expandSyn ss t [] of+ Nothing -> PVar $ Symbol $ show t+ Just t' -> hTypeToFormula ss t'++expandSyn :: [(HSymbol, ([HSymbol], HType, a))] -> HType -> [HType] -> Maybe HType+expandSyn ss (HTApp f a) as = expandSyn ss f (a:as)+expandSyn ss (HTCon c) as =+ case lookup c ss of+ Just (vs, t, _) | length vs == length as -> Just $ substHT (zip vs as) t+ _ -> Nothing+expandSyn _ _ _ = Nothing++substHT :: [(HSymbol, HType)] -> HType -> HType+substHT r (HTApp f a) = HTApp (substHT r f) (substHT r a)+substHT r t@(HTVar v) =+ case lookup v r of+ Nothing -> t+ Just t' -> t'+substHT _ t@(HTCon _) = t+substHT r (HTTuple ts) = HTTuple (map (substHT r) ts)+substHT r (HTArrow f a) = HTArrow (substHT r f) (substHT r a)+substHT r (HTUnion (ctss)) = HTUnion [ (c, map (substHT r) ts) | (c, ts) <- ctss ]+++-------------------------------+++data HClause = HClause HSymbol [HPat] HExpr+ deriving (Show, Eq)++data HPat = HPVar HSymbol | HPCon HSymbol | HPTuple [HPat] | HPAt HSymbol HPat | HPApply HPat HPat+ deriving (Show, Eq)++data HExpr = HELam [HPat] HExpr | HEApply HExpr HExpr | HECon HSymbol | HEVar HSymbol | HETuple [HExpr] |+ HECase HExpr [(HPat, HExpr)]+ deriving (Show, Eq)++hPrClause :: HClause -> String+hPrClause c = renderStyle style $ ppClause 0 c++ppClause :: Int -> HClause -> Doc+ppClause _p (HClause f ps e) = text f <+> sep [sep (map (ppPat 10) ps) <+> text "=",+ nest 2 $ ppExpr 0 e]++ppPat :: Int -> HPat -> Doc+ppPat _ (HPVar s) = text s+ppPat _ (HPCon s) = text s+ppPat _ (HPTuple ps) = parens $ fsep $ punctuate comma (map (ppPat 0) ps)+ppPat _ (HPAt s p) = text s <> text "@" <> ppPat 10 p+ppPat p (HPApply a b) = pparens (p > 1) $ ppPat 1 a <+> ppPat 2 b++ppExpr :: Int -> HExpr -> Doc+ppExpr p (HELam ps e) = pparens (p > 0) $ sep [ text "\\" <+> sep (map (ppPat 10) ps) <+> text "->",+ ppExpr 0 e]+ppExpr p (HEApply (HEApply (HEVar f@(c:_)) a1) a2) | not (isAlphaNum c) =+ pparens (p > 4) $ ppExpr 5 a1 <+> text f <+> ppExpr 5 a2+ppExpr p (HEApply f a) = pparens (p > 11) $ ppExpr 11 f <+> ppExpr 12 a+ppExpr _ (HECon s) = text s+ppExpr _ (HEVar s@(c:_)) | not (isAlphaNum c) = pparens True $ text s+ppExpr _ (HEVar s) = text s+ppExpr _ (HETuple es) = parens $ fsep $ punctuate comma (map (ppExpr 0) es)+ppExpr p (HECase s alts) = pparens (p > 0) $ (text "case" <+> ppExpr 0 s <+> text "of") $$+ vcat (map ppAlt alts)+ where ppAlt (pp, e) = ppPat 0 pp <+> text "->" <+> ppExpr 0 e+++pparens :: Bool -> Doc -> Doc+pparens True d = parens d+pparens False d = d++-------------------------------+++unSymbol :: Symbol -> HSymbol+unSymbol (Symbol s) = s++termToHExpr :: Term -> HExpr+termToHExpr term = niceNames $ etaReduce $ remUnusedVars $ fst $ conv [] term+ where conv _vs (Var s) = (HEVar $ unSymbol s, [])+ conv vs (Lam s te) = + let hs = unSymbol s+ (te', ss) = conv (hs : vs) te+ in (hELam [convV hs ss] te', ss)+ conv vs (Apply (Cinj (ConsDesc s n) _) a) = (f $ foldl HEApply (HECon s) as, ss)+ where (f, as) = unTuple n ha+ (ha, ss) = conv vs a+ conv vs (Apply te1 te2) = convAp vs te1 [te2]+ conv _vs (Ctuple 0) = (HECon "()", [])+ conv _vs e = error $ "termToHExpr " ++ show e++ unTuple 0 _ = (id, [])+ unTuple 1 a = (id, [a])+ unTuple n (HETuple as) | length as == n = (id, as)+ unTuple n e = error $ "unTuple: unimplemented " ++ show (n, e)++ unTupleP 0 _ = []+-- unTupleP 1 p = [p]+ unTupleP n (HPTuple ps) | length ps == n = ps+ unTupleP n p = error $ "unTupleP: unimplemented " ++ show (n, p)++ convAp vs (Apply te1 te2) as = convAp vs te1 (te2:as)+ convAp vs (Ctuple n) as | length as == n =+ let (es, sss) = unzip $ map (conv vs) as+ in (hETuple es, concat sss)+ convAp vs (Ccases cds) (se : es) =+ let (alts, ass) = unzip $ zipWith cAlt es cds+ cAlt (Lam v e) (ConsDesc c n) =+ let hv = unSymbol v+ (he, ss) = conv (hv : vs) e+ ps = case lookup hv ss of+ Nothing -> replicate n (HPVar "_")+ Just p -> unTupleP n p+ in ((foldl HPApply (HPCon c) ps, he), ss)+ cAlt e _ = error $ "cAlt " ++ show e+ (e', ess) = conv vs se+ in (hECase e' alts, ess ++ concat ass)+ convAp vs (Csplit n) (b : a : as) =+ let (hb, sb) = conv vs b+ (a', sa) = conv vs a+ (as', sss) = unzip $ map (conv vs) as+ (ps, b') = unLam n hb+ unLam 0 e = ([], e)+ unLam k (HELam ps0 e) | length ps0 >= n = let (ps1, ps2) = splitAt k ps0 in (ps1, hELam ps2 e)+ unLam k e = error $ "unLam: unimplemented" ++ show (k, e)+ in case a' of+ HEVar v | v `elem` vs && null as -> (b', [(v, HPTuple ps)] ++ sb ++ sa)+ _ -> (foldr HEApply (hECase a' [(HPTuple ps, b')]) as',+ sb ++ sa ++ concat sss)+ + convAp vs f as = + let (es, sss) = unzip $ map (conv vs) (f:as)+ in (foldl1 HEApply es, concat sss)++ convV hs ss =+ case lookup hs ss of+ Nothing -> HPVar hs+ Just p -> HPAt hs p++ hETuple [e] = e+ hETuple es = HETuple es++niceNames :: HExpr -> HExpr+niceNames e =+ let bvars = filter (/= "_") $ getBinderVarsHE e+ nvars = [[c] | c <- ['a'..'z']] ++ [ "x" ++ show i | i <- [1::Integer ..]]+ freevars = getAllVars e \\ bvars+ vars = nvars \\ freevars+ sub = zip bvars vars+ in hESubst sub e++hELam :: [HPat] -> HExpr -> HExpr+hELam [] e = e+hELam ps (HELam ps' e) = HELam (ps ++ ps') e+hELam ps e = HELam ps e++hECase :: HExpr -> [(HPat, HExpr)] -> HExpr+hECase e [] = HEApply (HEVar "void") e+hECase _ [(HPCon "()", e)] = e+hECase e pes | all (uncurry eqPatExpr) pes = e+hECase e [(p, HELam ps b)] = HELam ps $ hECase e [(p, b)]+hECase se alts@((_, HELam ops _):_) | m > 0 = HELam (take m ops) $ hECase se alts'+ where m = minimum (map (numBind . snd) alts)+ numBind (HELam ps _) = length (takeWhile isPVar ps)+ numBind _ = 0+ isPVar (HPVar _) = True+ isPVar _ = False+ alts' = [ let (ps1, ps2) = splitAt m ps in (cps, hELam ps2 $ hESubst (zipWith (\ (HPVar v) n -> (v, n)) ps1 ns) e)+ | (cps, HELam ps e) <- alts ]+ ns = [ n | HPVar n <- take m ops ]+-- if all arms are equal and there are at least two alternatives there can be no bound vars+-- from the patterns+hECase _ ((_,e):alts@(_:_)) | all (alphaEq e . snd) alts = e+hECase e alts = HECase e alts++eqPatExpr :: HPat -> HExpr -> Bool+eqPatExpr (HPVar s) (HEVar s') = s == s'+eqPatExpr (HPCon s) (HECon s') = s == s'+eqPatExpr (HPTuple ps) (HETuple es) = and (zipWith eqPatExpr ps es)+eqPatExpr (HPApply pf pa) (HEApply ef ea) = eqPatExpr pf ef && eqPatExpr pa ea+eqPatExpr _ _ = False++alphaEq :: HExpr -> HExpr -> Bool+alphaEq e1 e2 | e1 == e2 = True+alphaEq (HELam ps1 e1) (HELam ps2 e2) =+ Nothing /= do+ s <- matchPat (HPTuple ps1) (HPTuple ps2)+ if alphaEq (hESubst s e1) e2 then+ return ()+ else+ Nothing+alphaEq (HEApply f1 a1) (HEApply f2 a2) = alphaEq f1 f2 && alphaEq a1 a2+alphaEq (HECon s1) (HECon s2) = s1 == s2+alphaEq (HEVar s1) (HEVar s2) = s1 == s2+alphaEq (HETuple es1) (HETuple es2) | length es1 == length es2 = and (zipWith alphaEq es1 es2)+alphaEq (HECase e1 alts1) (HECase e2 alts2) =+ alphaEq e1 e2 && and (zipWith alphaEq [ HELam [p] e | (p, e) <- alts1 ] [ HELam [p] e | (p, e) <- alts2 ])+alphaEq _ _ = False++matchPat :: HPat -> HPat -> Maybe [(HSymbol, HSymbol)]+matchPat (HPVar s1) (HPVar s2) = return [(s1, s2)]+matchPat (HPCon s1) (HPCon s2) | s1 == s2 = return []+matchPat (HPTuple ps1) (HPTuple ps2) | length ps1 == length ps2 = do+ ss <- zipWithM matchPat ps1 ps2+ return $ concat ss+matchPat (HPAt s1 p1) (HPAt s2 p2) = do+ s <- matchPat p1 p2+ return $ (s1, s2) : s+matchPat (HPApply f1 a1) (HPApply f2 a2) = do+ s1 <- matchPat f1 f2+ s2 <- matchPat a1 a2+ return $ s1 ++ s2+matchPat _ _ = Nothing++hESubst :: [(HSymbol, HSymbol)] -> HExpr -> HExpr+hESubst s (HELam ps e) = HELam (map (hPSubst s) ps) (hESubst s e)+hESubst s (HEApply f a) = HEApply (hESubst s f) (hESubst s a)+hESubst _ e@(HECon _) = e+hESubst s (HEVar v) = HEVar $ maybe v id $ lookup v s+hESubst s (HETuple es) = HETuple (map (hESubst s) es)+hESubst s (HECase e alts) = HECase (hESubst s e) [(hPSubst s p, hESubst s b) | (p, b) <- alts]++hPSubst :: [(HSymbol, HSymbol)] -> HPat -> HPat+hPSubst s (HPVar v) = HPVar $ maybe v id $ lookup v s+hPSubst _ p@(HPCon _) = p+hPSubst s (HPTuple ps) = HPTuple (map (hPSubst s) ps)+hPSubst s (HPAt v p) = HPAt (maybe v id $ lookup v s) (hPSubst s p)+hPSubst s (HPApply f a) = HPApply (hPSubst s f) (hPSubst s a)+++termToHClause :: HSymbol -> Term -> HClause+termToHClause i term =+ case termToHExpr term of+ HELam ps e -> HClause i ps e+ e -> HClause i [] e++remUnusedVars :: HExpr -> HExpr+remUnusedVars expr = fst $ remE expr+ where remE (HELam ps e) =+ let (e', vs) = remE e+ in (HELam (map (remP vs) ps) e', vs)+ remE (HEApply f a) =+ let (f', fs) = remE f+ (a', as) = remE a+ in (HEApply f' a', fs ++ as)+ remE (HETuple es) =+ let (es', sss) = unzip (map remE es)+ in (HETuple es', concat sss)+ remE (HECase e alts) =+ let (e', es) = remE e+ (alts', sss) = unzip [ let (ee', ss) = remE ee in ((remP ss p, ee'), ss) | (p, ee) <- alts ]+ in case alts' of+ [(HPVar "_", b)] -> (b, concat sss)+ _ -> (hECase e' alts', es ++ concat sss)+ remE e@(HECon _) = (e, [])+ remE e@(HEVar v) = (e, [v])+ remP vs p@(HPVar v) = if v `elem` vs then p else HPVar "_"+ remP _vs p@(HPCon _) = p+ remP vs (HPTuple ps) = hPTuple (map (remP vs) ps)+ remP vs (HPAt v p) = if v `elem` vs then HPAt v (remP vs p) else remP vs p+ remP vs (HPApply f a) = HPApply (remP vs f) (remP vs a)+ hPTuple ps | all (== HPVar "_") ps = HPVar "_"+ hPTuple ps = HPTuple ps++getBinderVars :: HClause -> [HSymbol]+getBinderVars (HClause _ pats expr) = concatMap getBinderVarsHP pats ++ getBinderVarsHE expr++getBinderVarsHE :: HExpr -> [HSymbol]+getBinderVarsHE expr = gbExp expr+ where gbExp (HELam ps e) = concatMap getBinderVarsHP ps ++ gbExp e+ gbExp (HEApply f a) = gbExp f ++ gbExp a+ gbExp (HETuple es) = concatMap gbExp es+ gbExp (HECase se alts) = gbExp se ++ concatMap (\ (p, e) -> getBinderVarsHP p ++ gbExp e) alts+ gbExp _ = []++getBinderVarsHP :: HPat -> [HSymbol]+getBinderVarsHP pat = gbPat pat+ where gbPat (HPVar s) = [s]+ gbPat (HPCon _) = []+ gbPat (HPTuple ps) = concatMap gbPat ps+ gbPat (HPAt s p) = s : gbPat p+ gbPat (HPApply f a) = gbPat f ++ gbPat a++getAllVars :: HExpr -> [HSymbol]+getAllVars expr = gaExp expr+ where gaExp (HELam _ps e) = gaExp e+ gaExp (HEApply f a) = gaExp f `union` gaExp a+ gaExp (HETuple es) = foldr union [] (map gaExp es)+ gaExp (HECase se alts) = foldr union (gaExp se) (map (\ (_p, e) -> gaExp e) alts)+ gaExp (HEVar s) = [s]+ gaExp _ = []++etaReduce :: HExpr -> HExpr+etaReduce expr = fst $ eta expr+ where eta (HELam [HPVar v] (HEApply f (HEVar v'))) | v == v' && v `notElem` vs = (f', vs)+ where (f', vs) = eta f+ eta (HELam ps e) = (HELam ps e', vs) where (e', vs) = eta e+ eta (HEApply f a) = (HEApply f' a', fvs++avs) where (f', fvs) = eta f; (a', avs) = eta a+ eta e@(HECon _) = (e, [])+ eta e@(HEVar s) = (e, [s])+ eta (HETuple es) = (HETuple es', concat vss) where (es', vss) = unzip $ map eta es+ eta (HECase e alts) = (HECase e' alts', vs ++ concat vss) where (e', vs) = eta e+ (alts', vss) = unzip $ [ let (a', ss) = eta a in ((p, a'), ss)+ | (p, a) <- alts ]
+ Djinn/Help.hs view
@@ -0,0 +1,177 @@+module Help where+verboseHelp :: String+verboseHelp = "\+\\n\+\\n\+\Djinn commands explained\n\+\========================\n\+\\n\+\<sym> ? <type>\n\+\ Try to find a function of the specified type. Djinn knows about the\n\+\function type, tuples, Either, Maybe, (), and can be given new type\n\+\definitions. (Djinn also knows about the empty type, Void, but this\n\+\is less useful.) Further functions, type synonyms, and data types can\n\+\be added by using the commands below. If a function can be found it\n\+\is printed in a style suitable for inclusion in a Haskell program. If\n\+\no function can be found this will be reported as well. Examples:\n\+\ Djinn> f ? a->a\n\+\ f :: a -> a\n\+\ f x1 = x1\n\+\ Djinn> sel ? ((a,b),(c,d)) -> (b,c)\n\+\ sel :: ((a, b), (c, d)) -> (b, c)\n\+\ sel ((_, v5), (v6, _)) = (v5, v6)\n\+\ Djinn> cast ? a->b\n\+\ -- cast cannot be realized.\n\+\ Djinn will always find a (total) function if one exists. (The worst\n\+\case complexity is bad, but unlikely for typical examples.) If no\n\+\function exists Djinn will always terminate and say so.\n\+\ When multiple implementations of the type exists Djinn will only\n\+\give one of them. Example:\n\+\ Djinn> f ? a->a->a\n\+\ f :: a -> a -> a\n\+\ f _ x2 = x2\n\+\\n\+\Warning: The given type expression is not checked in any way (i.e., no\n\+\kind checking).\n\+\\n\+\\n\+\<sym> :: <type>\n\+\ Add a new function available for Djinn to construct the result.\n\+\Example:\n\+\ Djinn> foo :: Int -> Char\n\+\ Djinn> bar :: Char -> Bool\n\+\ Djinn> f ? Int -> Bool\n\+\ f :: Int -> Bool\n\+\ f x3 = bar (foo x3)\n\+\This feature is not as powerful as it first might seem. Djinn does\n\+\*not* instantiate polymorphic function. It will only use the function\n\+\with exactly the given type. Example:\n\+\ Djinn> cast :: a -> b\n\+\ Djinn> f ? c->d\n\+\ -- f cannot be realized.\n\+\\n\+\type <sym> <vars> = <type>\n\+\ Add a Haskell style type synonym. Type synonyms are expanded before\n\+\Djinn starts looking for a realization.\n\+\ Example:\n\+\ Djinn> type Id a = a->a\n\+\ Djinn> f ? Id a\n\+\ f :: Id a\n\+\ f x1 = x1\n\+\\n\+\data <sym> <vars> = <type>\n\+\ Add a Haskell style data type.\n\+\ Example:\n\+\ Djinn> data Foo a = C a a a\n\+\ Djinn> f ? a -> Foo a\n\+\ f :: a -> Foo a\n\+\ f x1 = C x1 x1 x1\n\+\\n\+\\n\+\:clear\n\+\ Set the environment to the start environment.\n\+\\n\+\\n\+\:delete <sym>\n\+\ Remove a symbol that has been added with the add command.\n\+\\n\+\\n\+\:environment\n\+\ List all added symbols and their types.\n\+\\n\+\\n\+\:help\n\+\ Show a short help message.\n\+\\n\+\\n\+\:load <file>\n\+\ Read and execute a file with commands. The file may include Haskell\n\+\style -- comments.\n\+\\n\+\\n\+\:quit\n\+\ Quit Djinn.\n\+\\n\+\\n\+\:set\n\+\ Set runtime options.\n\+\ +multi show multiple solutions\n\+\ This will not show all solutions since there might be\n\+\ infinitly many.\n\+\ -multi show one solution\n\+\ +sorted sort solutions according to a heuristic criterion\n\+\ -sorted do not sort solutions\n\+\ The heuristic used to sort the solutions is that as many of the\n\+\bound variables as possible should be used.\n\+\\n\+\:verbose-help\n\+\ Print this message.\n\+\\n\+\\n\+\Further examples\n\+\================\n\+\ calvin% djinn\n\+\ Welcome to Djinn version 2005-12-11.\n\+\ Type :h to get help.\n\+\\n\+\ -- return, bind, and callCC in the continuation monad\n\+\ Djinn> data CD r a = CD ((a -> r) -> r)\n\+\ Djinn> returnCD ? a -> CD r a\n\+\ returnCD :: a -> CD r a\n\+\ returnCD x1 = CD (\\ c15 -> c15 x1)\n\+\\n\+\ Djinn> bindCD ? CD r a -> (a -> CD r b) -> CD r b\n\+\ bindCD :: CD r a -> (a -> CD r b) -> CD r b\n\+\ bindCD x1 x4 =\n\+\ case x1 of\n\+\ CD v3 -> CD (\\ c49 ->\n\+\ v3 (\\ c50 ->\n\+\ case x4 c50 of\n\+\ CD c52 -> c52 c49))\n\+\\n\+\ Djinn> callCCD ? ((a -> CD r b) -> CD r a) -> CD r a\n\+\ callCCD :: ((a -> CD r b) -> CD r a) -> CD r a\n\+\ callCCD x1 =\n\+\ CD (\\ c68 ->\n\+\ case x1 (\\ c69 -> CD (\\ _ -> c68 c69)) of\n\+\ CD c72 -> c72 c68)\n\+\\n\+\\n\+\ -- return and bind in the state monad\n\+\ Djinn> type S s a = (s -> (a, s))\n\+\ Djinn> returnS ? a -> S s a\n\+\ returnS :: a -> S s a\n\+\ returnS x1 x2 = (x1, x2)\n\+\ Djinn> bindS ? S s a -> (a -> S s b) -> S s b\n\+\ bindS :: S s a -> (a -> S s b) -> S s b\n\+\ bindS x1 x2 x3 =\n\+\ case x1 x3 of\n\+\ (v4, v5) -> x2 v4 v5\n\+\\n\+\\n\+\Theory\n\+\======\n\+\ Djinn interprets a Haskell type as a logic formula using the\n\+\Curry-Howard isomorphism and then uses a decision procedure for\n\+\Intuitionistic Propositional Calculus. This decision procedure is\n\+\based on Gentzen's LJ sequent calculus, but in a modified form, LJT,\n\+\that ensures termination. This variation on LJ has a long history,\n\+\but the particular formulation used in Djinn is due to Roy Dyckhoff.\n\+\The decision procedure has been extended to generate a proof object\n\+\(i.e., a lambda term). It is this lambda term (in normal form) that\n\+\constitutes the Haskell code.\n\+\ See http://www.dcs.st-and.ac.uk/~rd/publications/jsl57.pdf for more\n\+\on the exact method used by Djinn.\n\+\\n\+\ Since Djinn handles propositional calculus it also knows about the\n\+\absurd proposition, corresponding to the empty set. This set is\n\+\called Void in Haskell, and Djinn assumes an elimination rule for the\n\+\Void type:\n\+\ void :: Void -> a\n\+\Using Void is of little use for programming, but can be interesting\n\+\for theorem proving. Example, the double negation of the law of\n\+\excluded middle:\n\+\ Djinn> f ? Not (Not (Either x (Not x)))\n\+\ f :: Not (Not (Either x (Not x)))\n\+\ f x1 = void (x1 (Right (\\ c23 -> void (x1 (Left c23)))))\n\+\"
+ Djinn/LJT.hs view
@@ -0,0 +1,468 @@+--+-- Copyright (c) 2005, 2008 Lennart Augustsson+-- See LICENSE for licensing details.+--+-- Intuitionistic theorem prover+-- Written by Roy Dyckhoff, Summer 1991+-- Modified to use the LWB syntax Summer 1997+-- and simplified in various ways...+--+-- Translated to Haskell by Lennart Augustsson December 2005+--+-- Incorporates the Vorob'ev-Hudelmaier etc calculus (I call it LJT)+-- See RD's paper in JSL 1992:+-- "Contraction-free calculi for intuitionistic logic"+--+-- Torkel Franzen (at SICS) gave me good ideas about how to write this+-- properly, taking account of first-argument indexing,+-- and I learnt a trick or two from Neil Tennant's "Autologic" book.++module LJT (module LJTFormula, provable,+ prove, Proof) where++import Control.Monad+import Data.List (partition)+import Debug.Trace++import LJTFormula++mtrace :: String -> a -> a+mtrace m x = if debug then trace m x else x+-- wrap :: (Show a, Show b) => String -> a -> b -> b+-- wrap fun args ret = mtrace (fun ++ ": " ++ show args) $+-- let o = show ret in seq o $+-- mtrace (fun ++ " returns: " ++ o) ret+wrapM :: (Show a, Show b, Monad m) => String -> a -> m b -> m b+wrapM fun args mret = do+ () <- mtrace (fun ++ ": " ++ show args) $ return ()+ ret <- mret+ () <- mtrace (fun ++ " returns: " ++ show ret) $ return ()+ return ret+debug :: Bool+debug = False++type MoreSolutions = Bool++provable :: Formula -> Bool+provable a = not $ null $ prove False [] a++prove :: MoreSolutions -> [(Symbol, Formula)] -> Formula -> [Proof]+prove more env a = runP $ redtop more env a++redtop :: MoreSolutions -> [(Symbol, Formula)] -> Formula -> P Proof+redtop more ifs a = do+ let form = foldr (:->) a (map snd ifs)+ p <- redant more [] [] [] [] form+ nf (foldl Apply p (map (Var . fst) ifs))++------------------------------+-----+type Proof = Term++subst :: Term -> Symbol -> Term -> P Term+subst b x term = sub term+ where sub t@(Var s') = if x == s' then copy [] b else return t+ sub (Lam s t) = liftM (Lam s) (sub t)+ sub (Apply t1 t2) = liftM2 Apply (sub t1) (sub t2)+ sub t = return t++copy :: [(Symbol, Symbol)] -> Term -> P Term+copy r (Var s) = return $ Var $ maybe s id $ lookup s r+copy r (Lam s t) = do+ s' <- newSym "c"+ liftM (Lam s') $ copy ((s, s'):r) t+copy r (Apply t1 t2) = liftM2 Apply (copy r t1) (copy r t2)+copy _r t = return t++------------------------------++-- XXX The symbols used in the functions below must not clash+-- XXX with any symbols from newSym.++applyAtom :: Term -> Term -> Term+applyAtom f a = Apply f a++curryt :: Int -> Term -> Term+curryt n p = foldr Lam (Apply p (applys (Ctuple n) (map Var xs))) xs+ where xs = [ Symbol ("x_" ++ show i) | i <- [0 .. n-1] ]++inj :: ConsDesc -> Int -> Term -> Term+inj cd i p = Lam x $ Apply p (Apply (Cinj cd i) (Var x))+ where x = Symbol "x"++applyImp :: Term -> Term -> Term+applyImp p q = Apply p (Apply q (Lam y $ Apply p (Lam x (Var y))))+ where x = Symbol "x"+ y = Symbol "y"++-- ((c->d)->false) -> ((c->false)->false, d->false)+-- p : (c->d)->false)+-- replace p1 and p2 with the components of the pair+cImpDImpFalse :: Symbol -> Symbol -> Term -> Term -> P Term+cImpDImpFalse p1 p2 cdf gp = do+ let p1b = Lam cf $ Apply cdf $ Lam x $ Apply (Ccases []) $ Apply (Var cf) (Var x)+ p2b = Lam d $ Apply cdf $ Lam c $ Var d+ cf = Symbol "cf"+ x = Symbol "x"+ d = Symbol "d"+ c = Symbol "c"+ subst p1b p1 gp >>= subst p2b p2++------------------------------++-- More simplifications:+-- split where no variables used can be removed+-- either with equal RHS can me merged.++-- Compute the normal form+nf :: Term -> P Term+nf ee = spine ee []+ where spine (Apply f a) as = do a' <- nf a; spine f (a' : as)+ spine (Lam s e) [] = liftM (Lam s) (nf e)+ spine (Lam s e) (a : as) = do e' <- subst a s e; spine e' as+ spine (Csplit n) (b : tup : args) | istup && n <= length xs = spine (applys b xs) args+ where (istup, xs) = getTup tup+ getTup (Ctuple _) = (True, [])+ getTup (Apply f a) = let (tf, as) = getTup f in (tf, a:as)+ getTup _ = (False, [])+ spine (Ccases []) (e@(Apply (Ccases []) _) : as) = spine e as+ spine (Ccases cds) (Apply (Cinj _ i) x : as) | length as >= n = spine (Apply (as!!i) x) (drop n as)+ where n = length cds+ spine f as = return $ applys f as+++------------------------------+----- Our Proof monad, P, a monad with state and multiple results++-- Note, this is the non-standard way to combine state with multiple+-- results. But this is much better for backtracking.+newtype P a = P { unP :: PS -> [(PS, a)] }++instance Monad P where+ return x = P $ \ s -> [(s, x)]+ P m >>= f = P $ \ s ->+ [ y | (s',x) <- m s, y <- unP (f x) s' ]++instance Functor P where+ fmap f (P m) = P $ \ s ->+ [ (s', f x) | (s', x) <- m s ]++instance MonadPlus P where+ mzero = P $ \ _s -> []+ P fxs `mplus` P fys = P $ \ s -> fxs s ++ fys s++-- The state, just an integer for generating new variables+data PS = PS !Integer+startPS :: PS+startPS = PS 1++nextInt :: P Integer+nextInt = P $ \ (PS i) -> [(PS (i+1), i)]++none :: P a+none = mzero++many :: [a] -> P a+many xs = P $ \ s -> zip (repeat s) xs++atMostOne :: P a -> P a+atMostOne (P f) = P $ \ s -> take 1 (f s)++runP :: P a -> [a]+runP (P m) = map snd (m startPS)+++------------------------------+----- Atomic formulae+data AtomF = AtomF Term Symbol+ deriving (Eq)+instance Show AtomF where+ show (AtomF p s) = show p ++ ":" ++ show s++type AtomFs = [AtomF]++findAtoms :: Symbol -> AtomFs -> [Term]+findAtoms s atoms = [ p | AtomF p s' <- atoms, s == s' ]++--removeAtom :: Symbol -> AtomFs -> AtomFs+--removeAtom s atoms = [ a | a@(AtomF _ s') <- atoms, s /= s' ]++addAtom :: AtomF -> AtomFs -> AtomFs+addAtom a as = if a `elem` as then as else a : as++------------------------------+----- Implications of one atom++data AtomImp = AtomImp Symbol Antecedents+ deriving (Show)+type AtomImps = [AtomImp]++extract :: AtomImps -> Symbol -> ([Antecedent], AtomImps)+extract aatomImps@(atomImp@(AtomImp a' bs) : atomImps) a =+ case compare a a' of+ GT -> let (rbs, restImps) = extract atomImps a in (rbs, atomImp : restImps)+ EQ -> (bs, atomImps)+ LT -> ([], aatomImps)+extract _ _ = ([], [])++insert :: AtomImps -> AtomImp -> AtomImps+insert [] ai = [ ai ]+insert aatomImps@(atomImp@(AtomImp a' bs') : atomImps) ai@(AtomImp a bs) =+ case compare a a' of+ GT -> atomImp : insert atomImps ai+ EQ -> AtomImp a (bs ++ bs') : atomImps+ LT -> ai : aatomImps++------------------------------+----- Nested implications, (a -> b) -> c++data NestImp = NestImp Term Formula Formula Formula -- NestImp a b c represents (a :-> b) :-> c+ deriving (Eq)+instance Show NestImp where+ show (NestImp _ a b c) = show $ (a :-> b) :-> c++type NestImps = [NestImp]++addNestImp :: NestImp -> NestImps -> NestImps+addNestImp n ns = if n `elem` ns then ns else n : ns++------------------------------+----- Ordering of nested implications+heuristics :: Bool+heuristics = True++order :: NestImps -> Formula -> AtomImps -> NestImps+order nestImps g atomImps =+ if heuristics then+ nestImps+ else+ let+ good_for (NestImp _ _ _ (Disj [])) = True+ good_for (NestImp _ _ _ g') = g == g'+ nice_for (NestImp _ _ _ (PVar s)) =+ case extract atomImps s of+ (bs', _) -> let bs = [ b | A _ b <- bs'] in g `elem` bs || false `elem` bs+ nice_for _ = False+ (good, ok) = partition good_for nestImps+ (nice, bad) = partition nice_for ok+ in good ++ nice ++ bad++------------------------------+----- Generate a new unique variable+newSym :: String -> P Symbol+newSym pre = do+ i <- nextInt+ return $ Symbol $ pre ++ show i++------------------------------+----- Generate all ways to select one element of a list+select :: [a] -> P (a, [a])+select zs = many [ del n zs | n <- [0 .. length zs - 1] ]+ where del 0 (x:xs) = (x, xs)+ del n (x:xs) = let (y,ys) = del (n-1) xs in (y, x:ys)+ del _ _ = error "select"++------------------------------+-----++data Antecedent = A Term Formula deriving (Show)+type Antecedents = [Antecedent]++type Goal = Formula++--+-- This is the main loop of the proof search.+--+-- The redant functions reduce antecedents and the redsucc+-- function reduces the goal (succedent).+--+-- The antecedents are kept in four groups: Antecedents, AtomImps, NestImps, AtomFs+-- Antecedents contains as yet unclassified antecedents; the redant functions+-- go through them one by one and reduces and classifies them.+-- AtomImps contains implications of the form (a -> b), where `a' is an atom.+-- To speed up the processing it is stored as a map from the `a' to all the+-- formulae it implies.+-- NestImps contains implications of the form ((b -> c) -> d)+-- AtomFs contains atomic formulae.+--+-- There is also a proof object associated with each antecedent.+--+redant :: MoreSolutions -> Antecedents -> AtomImps -> NestImps -> AtomFs -> Goal -> P Proof+redant more antes atomImps nestImps atoms goal =+ wrapM "redant" (antes, atomImps, nestImps, atoms, goal) $+ case antes of+ [] -> redsucc goal+ a:l -> redant1 a l goal+ where redant0 l g = redant more l atomImps nestImps atoms g+ redant1 :: Antecedent -> Antecedents -> Goal -> P Proof+ redant1 a@(A p f) l g =+ wrapM "redant1" ((a, l), atomImps, nestImps, atoms, g) $+ if f == g then+ -- The goal is the antecedent, we're done.+ -- XXX But we might want more?+ if more then+ return p `mplus` redant1' a l g+ else+ return p+ else+ redant1' a l g++ -- Reduce the first antecedent+ redant1' :: Antecedent -> Antecedents -> Goal -> P Proof+ redant1' (A p (PVar s)) l g =+ let af = AtomF p s+ (bs, restAtomImps) = extract atomImps s+ in redant more ([A (Apply f p) b | A f b <- bs] ++ l) restAtomImps nestImps (addAtom af atoms) g+ redant1' (A p (Conj bs)) l g = do+ vs <- mapM (const (newSym "v")) bs+ gp <- redant0 (zipWith (\ v a -> A (Var v) a) vs bs ++ l) g+ return $ applys (Csplit (length bs)) [foldr Lam gp vs, p]+ redant1' (A p (Disj ds)) l g = do+ vs <- mapM (const (newSym "d")) ds+ ps <- mapM (\ (v, (_, d)) -> redant1 (A (Var v) d) l g) (zip vs ds)+ if null ds && g == Disj [] then+ -- We are about to construct `void p : Void', so we shortcut+ -- it with just `p'.+ return p+ else+ return $ applys (Ccases (map fst ds)) (p : zipWith Lam vs ps)+ redant1' (A p (a :-> b)) l g = redantimp p a b l g++ redantimp :: Term -> Formula -> Formula -> Antecedents -> Goal -> P Proof+ redantimp t c d a g =+ wrapM "redantimp" (c,d,a,g) $+ redantimp' t c d a g++ -- Reduce an implication antecedent+ redantimp' :: Term -> Formula -> Formula -> Antecedents -> Goal -> P Proof+ -- p : PVar s -> b+ redantimp' p (PVar s) b l g = redantimpatom p s b l g+ -- p : (c & d) -> b+ redantimp' p (Conj cs) b l g = do+ x <- newSym "x"+ let imp = foldr (:->) b cs+ gp <- redant1 (A (Var x) imp) l g+ subst (curryt (length cs) p) x gp+ -- p : (c | d) -> b+ redantimp' p (Disj ds) b l g = do+ vs <- mapM (const (newSym "d")) ds+ gp <- redant0 (zipWith (\ v (_, d) -> A (Var v) (d :-> b)) vs ds ++ l) g+ foldM (\ r (i, v, (cd, _)) -> subst (inj cd i p) v r) gp (zip3 [0..] vs ds)+ -- p : (c -> d) -> b+ redantimp' p (c :-> d) b l g = redantimpimp p c d b l g++ redantimpimp :: Term -> Formula -> Formula -> Formula -> Antecedents -> Goal -> P Proof+ redantimpimp f b c d a g =+ wrapM "redantimpimp" (b,c,d,a,g) $+ redantimpimp' f b c d a g++ -- Reduce a double implication antecedent+ redantimpimp' :: Term -> Formula -> Formula -> Formula -> Antecedents -> Goal -> P Proof+ -- next clause exploits ~(C->D) <=> (~~C & ~D)+ -- which isn't helpful when D = false+ redantimpimp' p c d (Disj []) l g | d /= false = do+ x <- newSym "x"+ y <- newSym "y"+ gp <- redantimpimp (Var x) c false false (A (Var y) (d :-> false) : l) g+ cImpDImpFalse x y p gp+ -- p : (c -> d) -> b+ redantimpimp' p c d b l g = redant more l atomImps (addNestImp (NestImp p c d b) nestImps) atoms g++ -- Reduce an atomic implication+ redantimpatom :: Term -> Symbol -> Formula -> Antecedents -> Goal -> P Proof+ redantimpatom p s b l g =+ wrapM "redantimpatom" (s,b,l,g) $+ redantimpatom' p s b l g++ redantimpatom' :: Term -> Symbol -> Formula -> Antecedents -> Goal -> P Proof+ redantimpatom' p s b l g =+ do+ a <- cutSearch more $ many (findAtoms s atoms)+ x <- newSym "x"+ gp <- redant1 (A (Var x) b) l g+ mtrace "redantimpatom: LLL" $+ subst (applyAtom p a) x gp+ `mplus`+ (mtrace "redantimpatom: RRR" $+ redant more l (insert atomImps (AtomImp s [A p b])) nestImps atoms g)+{-+ let ps = wrap "redantimpatom findAtoms" atoms $ findAtoms s atoms+ in if not (null ps) then do+ a <- cutSearch more $ many ps+ x <- newSym "x"+ gp <- redant1 (A (Var x) b) l g+ mtrace "redantimpatom: LLL" $+ subst (applyAtom p a) x gp+ else+ mtrace "redantimpatom: RRR" $+ redant more l (insert atomImps (AtomImp s [A p b])) nestImps atoms g+-}+ -- Reduce the goal, with all antecedents already being classified+ redsucc :: Goal -> P Proof+ redsucc g =+ wrapM "redsucc" (g, atomImps, nestImps, atoms) $+ redsucc' g++ redsucc' :: Goal -> P Proof+ redsucc' a@(PVar s) =+ (cutSearch more $ many (findAtoms s atoms))+ `mplus`+ -- The posin check is an optimization. It gets a little slower without the test.+ (if posin s atomImps nestImps then+ redsucc_choice a+ else+ none)+ redsucc' (Conj cs) = do+ ps <- mapM redsucc cs+ return $ applys (Ctuple (length cs)) ps+ -- next clause deals with succedent (A v B) by pushing the+ -- non-determinism into the treatment of implication on the left+ redsucc' (Disj ds) = do+ s1 <- newSym "_"+ let v = PVar s1+ redant0 [ A (Cinj cd i) $ d :-> v | (i, (cd, d)) <- zip [0..] ds ] v+ redsucc' (a :-> b) = do+ s <- newSym "x"+ p <- redant1 (A (Var s) a) [] b+ return $ Lam s p++ -- Now we have the hard part; maybe lots of formulae+ -- of form (C->D)->B in nestImps to choose from!+ -- Which one to take first? We user the order heuristic.+ redsucc_choice :: Goal -> P Proof+ redsucc_choice g =+ wrapM "redsucc_choice" g $+ redsucc_choice' g++ redsucc_choice' :: Goal -> P Proof+ redsucc_choice' g = do+ let ordImps = order nestImps g atomImps+ (NestImp p c d b, restImps) <-+ mtrace ("redsucc_choice: order=" ++ show ordImps) $+ select ordImps+ x <- newSym "x"+ z <- newSym "z"+ qz <- redant more [A (Var z) $ d :-> b] atomImps restImps atoms (c :-> d)+ gp <- redant more [A (Var x) b] atomImps restImps atoms g+ subst (applyImp p (Lam z qz)) x gp++posin :: Symbol -> AtomImps -> NestImps -> Bool+posin g atomImps nestImps = posin1 g atomImps || posin2 g [ (a :-> b) :-> c | NestImp _ a b c <- nestImps ]++posin1 :: Symbol -> AtomImps -> Bool+posin1 g atomImps = any (\ (AtomImp _ bs) -> posin2 g [ b | A _ b <- bs]) atomImps++posin2 :: Symbol -> [Formula] -> Bool+posin2 g bs = any (posin3 g) bs++posin3 :: Symbol -> Formula -> Bool+posin3 g (Disj as) = all (posin3 g) (map snd as)+posin3 g (Conj as) = any (posin3 g) as+posin3 g (_ :-> b) = posin3 g b+posin3 s (PVar s') = s == s'++cutSearch :: MoreSolutions -> P a -> P a+cutSearch False p = atMostOne p+cutSearch True p = p++---------------------------
+ Djinn/LJTFormula.hs view
@@ -0,0 +1,103 @@+--+-- Copyright (c) 2005 Lennart Augustsson+-- See LICENSE for licensing details.+--+module LJTFormula(Symbol(..), Formula(..), (<->), (&), (|:), fnot, false, true,+ ConsDesc(..),+ Term(..), applys, freeVars+ ) where+import Data.List(union, (\\))++infixr 2 :->+infix 2 <->+infixl 3 |:+infixl 4 &++newtype Symbol = Symbol String+ deriving (Eq, Ord)++instance Show Symbol where+ show (Symbol s) = s++data ConsDesc = ConsDesc String Int -- name and arity+ deriving (Eq, Ord, Show)++data Formula+ = Conj [Formula]+ | Disj [(ConsDesc, Formula)]+ | Formula :-> Formula+ | PVar Symbol+ deriving (Eq, Ord)++(<->) :: Formula -> Formula -> Formula+x <-> y = (x:->y) & (y:->x)++(&) :: Formula -> Formula -> Formula+x & y = Conj [x, y]++(|:) :: Formula -> Formula -> Formula+x |: y = Disj [((ConsDesc "Left" 1), x), ((ConsDesc "Right" 1), y)]++fnot :: Formula -> Formula+fnot x = x :-> false++false :: Formula+false = Disj []++true :: Formula+true = Conj []++-- Show formulae the LJT way+instance Show Formula where+ showsPrec _ (Conj []) = showString "true"+ showsPrec _ (Conj [c]) = showParen True $ showString "&" . showsPrec 0 c+ showsPrec p (Conj cs) =+ showParen (p>40) $ loop cs+ where loop [f] = showsPrec 41 f+ loop (f : fs) = showsPrec 41 f . showString " & " . loop fs+ loop [] = error "showsPrec Conj"+ showsPrec _ (Disj []) = showString "false"+ showsPrec _ (Disj [(_,c)]) = showParen True $ showString "|" . showsPrec 0 c+ showsPrec p (Disj ds) =+ showParen (p>30) $ loop ds+ where loop [(_,f)] = showsPrec 31 f+ loop ((_,f) : fs) = showsPrec 31 f . showString " v " . loop fs+ loop [] = error "showsPrec Disj"+ showsPrec _ (f1 :-> Disj []) =+ showString "~" . showsPrec 100 f1+ showsPrec p (f1 :-> f2) =+ showParen (p>20) $ showsPrec 21 f1 . showString " -> " . showsPrec 20 f2+ showsPrec p (PVar s) = showsPrec p s++------------------------------++data Term+ = Var Symbol+ | Lam Symbol Term+ | Apply Term Term+ | Ctuple Int+ | Csplit Int+ | Cinj ConsDesc Int+ | Ccases [ConsDesc]+ | Xsel Int Int Term --- XXX just temporary by MJ+ deriving (Eq, Ord)++instance Show Term where+ showsPrec p (Var s) = showsPrec p s+ showsPrec p (Lam s e) = showParen (p > 0) $ showString "\\" . showsPrec 0 s . showString "." . showsPrec 0 e+ showsPrec p (Apply f a) = showParen (p > 1) $ showsPrec 1 f . showString " " . showsPrec 2 a+ showsPrec _ (Cinj _ i) = showString $ "Inj" ++ show i+ showsPrec _ (Ctuple i) = showString $ "Tuple" ++ show i+ showsPrec _ (Csplit n) = showString $ "split" ++ show n+ showsPrec _ (Ccases cds) = showString $ "cases" ++ show (length cds)+ showsPrec p (Xsel i n e) = showParen (p > 0) $ showString ("sel_" ++ show i ++ "_" ++ show n) . showString " " . showsPrec 2 e++applys :: Term -> [Term] -> Term+applys f as = foldl Apply f as++freeVars :: Term -> [Symbol]+freeVars (Var s) = [s]+freeVars (Lam s e) = freeVars e \\ [s]+freeVars (Apply f a) = freeVars f `union` freeVars a+freeVars (Xsel _ _ e) = freeVars e+freeVars _ = []
+ Djinn/LJTParse.hs view
@@ -0,0 +1,98 @@+--+-- Copyright (c) 2005 Lennart Augustsson+-- See LICENSE for licensing details.+--+module LJTParse(parseFormula, parseLJT) where+import Data.Char(isAlphaNum)+import Text.ParserCombinators.ReadP(ReadP, (+++), char, sepBy1, readP_to_S, skipSpaces, munch1, many)+import LJTFormula++parseFormula :: String -> Formula+parseFormula = parser pTop++parseLJT :: String -> Formula+parseLJT = parser pLJT++parser :: (Show a) => ReadP a -> String -> a+parser p s =+ let ess = readP_to_S p (removeComments s)+ in case filter (null . snd) ess of+ [(e, "")] -> e+ _ -> error ("bad parse: " ++ show ess)++removeComments :: String -> String+removeComments "" = ""+removeComments ('%':cs) = skip cs+ where skip "" = ""+ skip s@('\n':_) = removeComments s+ skip (_:s) = skip s+removeComments (c:cs) = c : removeComments cs++pTop :: ReadP Formula+pTop = do+ f <- pFormula+ skipSpaces+ return f++pLJT :: ReadP Formula+pLJT = do+ schar 'f'+ f <- pFormula+ schar '.'+ skipSpaces+ return f++pFormula :: ReadP Formula+pFormula = do+ f1 <- pDisjuction+ ods <- many (do o <- pArrow; d <- pDisjuction; return (o, d))+ let (op, f2) = foldr (\ (no, d) (oo, r) -> (no, d `oo` r)) (const, undefined) ods+ return $ f1 `op` f2++pArrow :: ReadP (Formula -> Formula -> Formula)+pArrow =+ (do schar '-'; char '>'; return (:->))+ ++++ (do schar '<'; char '-'; char '>'; return (<->))++pDisjuction :: ReadP Formula+pDisjuction = do+ fs <- sepBy1 pConjunction (schar 'v')+ return $ foldl1 (|:) fs++pConjunction :: ReadP Formula+pConjunction = do+ fs <- sepBy1 pAtomic (schar '&')+ return $ foldl1 (&) fs++pAtomic :: ReadP Formula+pAtomic = pNegation +++ pParen pFormula +++ pVar++pNegation :: ReadP Formula+pNegation = do+ schar '~'+ f <- pAtomic+ return $ fnot f++pVar :: ReadP Formula+pVar = do+ skipSpaces+ cs <- munch1 isAlphaNum+ case cs of+ "false" -> return false+ "true" -> return true+ _ -> return $ PVar $ Symbol cs++pParen :: ReadP a -> ReadP a+pParen p = do+ schar '('+ e <- p+ schar ')'+ return e++schar :: Char -> ReadP ()+schar c = do+ skipSpaces+ char c+ return ()+
+ Djinn/MLJT.hs view
@@ -0,0 +1,30 @@+--+-- Copyright (c) 2005 Lennart Augustsson+-- See LICENSE for licensing details.+--+import System.IO+import LJTParse+import MJ++main :: IO ()+main = do+ hSetBuffering stdout NoBuffering+ hSetBuffering stderr NoBuffering+ args <- getArgs+ file <-+ case args of+ [a] -> readFile a+ _ -> hGetContents stdin+ let form = parseLJT file+-- pr = provable form+-- cpr = provable (fnot (fnot form))+ mpr = take 25 $ prove False [] form+ print form+-- putStrLn $ "Classical " ++ show cpr+-- putStrLn $ "Intuitionistic " ++ show pr+-- putStrLn $ show mpr+ case mpr of+ [] -> return ()+ terms -> do+ putStrLn $ "proof : " ++ show form+ putStrLn $ unlines (map (("proof = " ++) . show) terms)
+ Djinn/REPL.hs view
@@ -0,0 +1,34 @@+--+-- Copyright (c) 2005 Lennart Augustsson+-- See LICENSE for licensing details.+--+module REPL(REPL(..), repl) where+import qualified Control.Exception+import System.Console.Readline(readline, addHistory)++data REPL s = REPL {+ repl_init :: IO (String, s), -- prompt and initial state+ repl_eval :: s -> String -> IO (Bool, s), -- quit flag and new state+ repl_exit :: s -> IO ()+ }++repl :: REPL s -> IO ()+repl p = do+ (prompt, state) <- repl_init p+ let loop s = (do+ mline <- readline prompt+ case mline of+ Nothing -> loop s+ Just line -> do+ (quit, s') <- repl_eval p s line+ if quit then+ repl_exit p s'+ else do+ addHistory line+ loop s'+ ) `Control.Exception.catch` ( \ exc ->+ do+ putStrLn $ "\nInterrupted (" ++ show exc ++ ")"+ loop s+ )+ loop state
+ Djinn/Util/Digraph.hs view
@@ -0,0 +1,393 @@+{- |+ + Module : Util.Digraph+ Copyright : ++ Maintainer : lib@galois.com+ Stability : + Portability : + + Functional graph algorithms; code taken from King+ and Launchbury's POPL paper (via GHC sources.)+-}+module Util.Digraph(++ -- At present the only one with a "nice" external interface+ stronglyConnComp, stronglyConnCompR, SCC(..),++ Graph, Vertex, + graphFromEdges, buildG, transposeG, reverseE, outdegree, indegree,++ Tree(..), Forest,+ showTree, showForest,++ dfs, dff,+ topSort,+ components,+ scc,+ back, cross, forward,+ reachable, path,+ bcc++ ) where++------------------------------------------------------------------------------+-- A version of the graph algorithms described in:+-- +-- ``Lazy Depth-First Search and Linear Graph Algorithms in Haskell''+-- by David King and John Launchbury+-- +-- Also included is some additional code for printing tree structures ...+------------------------------------------------------------------------------+++import Util.Sort ( sortLe ) -- merge sosrt++import Control.Monad.ST+import Data.Array.ST ( STArray, newArray, writeArray, readArray )++-- std interfaces+import Data.Maybe+import Data.Array+import Data.List ( (\\) )++{-+%************************************************************************+%* *+%* External interface+%* *+%************************************************************************+-}++data SCC vertex = AcyclicSCC vertex+ | CyclicSCC [vertex] deriving Show++stronglyConnComp+ :: Ord key+ => [(node, key, [key])] -- The graph; its ok for the+ -- out-list to contain keys which arent+ -- a vertex key, they are ignored+ -> [SCC node]++stronglyConnComp edges1+ = map get_node (stronglyConnCompR edges1)+ where+ get_node (AcyclicSCC (n, _, _)) = AcyclicSCC n+ get_node (CyclicSCC triples) = CyclicSCC [n | (n,_,_) <- triples]++-- The "R" interface is used when you expect to apply SCC to+-- the (some of) the result of SCC, so you dont want to lose the dependency info+stronglyConnCompR+ :: Ord key+ => [(node, key, [key])] -- The graph; its ok for the+ -- out-list to contain keys which arent+ -- a vertex key, they are ignored+ -> [SCC (node, key, [key])]++stronglyConnCompR [] = [] -- added to avoid creating empty array in graphFromEdges -- SOF+stronglyConnCompR edges1+ = map decode forest+ where+ (graph, vertex_fn) = graphFromEdges edges1+ forest = scc graph+ decode (Node v []) | mentions_itself v = CyclicSCC [vertex_fn v]+ | otherwise = AcyclicSCC (vertex_fn v)+ decode other = CyclicSCC (dec other [])+ where+ dec (Node v ts) vs = vertex_fn v : foldr dec vs ts+ mentions_itself v = v `elem` (graph ! v)++{-+%************************************************************************+%* *+%* Graphs+%* *+%************************************************************************+-}++type Vertex = Int+type Table a = Array Vertex a+type Graph = Table [Vertex]+type Bounds = (Vertex, Vertex)+type Edge = (Vertex, Vertex)+++vertices :: Graph -> [Vertex]+vertices = indices++edges :: Graph -> [Edge]+edges g = [ (v, w) | v <- vertices g, w <- g!v ]++mapT :: (Vertex -> a -> b) -> Table a -> Table b+mapT f t = array (bounds t) [ (,) v (f v (t!v)) | v <- indices t ]++buildG :: Bounds -> [Edge] -> Graph+buildG bounds1 edges1+ = accumArray (flip (:)) [] bounds1 [(,) k v | (k,v) <- edges1]++transposeG :: Graph -> Graph+transposeG g = buildG (bounds g) (reverseE g)++reverseE :: Graph -> [Edge]+reverseE g = [ (w, v) | (v, w) <- edges g ]++outdegree :: Graph -> Table Int+outdegree = mapT numEdges+ where numEdges _ ws = length ws++indegree :: Graph -> Table Int+indegree = outdegree . transposeG+++graphFromEdges+ :: Ord key+ => [(node, key, [key])]+ -> (Graph, Vertex -> (node, key, [key]))+graphFromEdges edgs+ = (graph, \v -> vertex_map ! v)+ where+ max_v = length edgs - 1+ bounds1 = (0,max_v) :: (Vertex, Vertex)+ sorted_edges = sortLe le edgs+ where+ (_,k1,_) `le` (_,k2,_) = case k1 `compare` k2 of { GT -> False; _other -> True }+ edges1 = zipWith (,) [0..] sorted_edges++ graph = array bounds1 [(,) v (mapMaybe key_vertex ks) | (,) v (_, _, ks) <- edges1]+ key_map = array bounds1 [(,) v k | (,) v (_, k, _ ) <- edges1]+ vertex_map = array bounds1 edges1++ -- key_vertex :: key -> Maybe Vertex+ -- returns Nothing for non-interesting vertices+ key_vertex k = find 0 max_v + where+ find a b | a > b + = Nothing+ find a b = case compare k (key_map ! mid) of+ LT -> find a (mid-1)+ EQ -> Just mid+ GT -> find (mid+1) b+ where+ mid = (a + b) `div` 2++{-+%************************************************************************+%* *+%* Trees and forests+%* *+%************************************************************************+-}++data Tree a = Node a (Forest a)+type Forest a = [Tree a]++mapTree :: (a -> b) -> (Tree a -> Tree b)+mapTree f (Node x ts) = Node (f x) (map (mapTree f) ts)+++instance Show a => Show (Tree a) where+ show t = showTree t++showTree :: Show a => Tree a -> String+showTree = drawTree . mapTree show++showForest :: Show a => Forest a -> String+showForest = unlines . map showTree++drawTree :: Tree String -> String+drawTree = unlines . draw+ where+ draw (Node x ts) = grp this (space (length this)) (stLoop ts)+ where+ this = s1 ++ x ++ " "+ space n = take n (repeat ' ')++ stLoop [] = [""]+ stLoop [t] = grp s2 " " (draw t)+ stLoop (t:xs) = grp s3 s4 (draw t) ++ [s4] ++ rsLoop xs++ rsLoop [] = []+ rsLoop [t] = grp s5 " " (draw t)+ rsLoop (t:xs) = grp s6 s4 (draw t) ++ [s4] ++ rsLoop xs++ grp a rst = zipWith (++) (a:repeat rst)++ [s1,s2,s3,s4,s5,s6] = ["- ", "--", "-+", " |", " `", " +"]+++{-+%************************************************************************+%* *+%* Depth first search+%* *+%************************************************************************+-}++--type Set s = MutableArray s Vertex Bool+type Set s = STArray s Vertex Bool++mkEmpty :: Bounds -> ST s (Set s)+mkEmpty bnds = newArray bnds False++contains :: Set s -> Vertex -> ST s Bool+contains m v = readArray m v++include :: Set s -> Vertex -> ST s ()+include m v = writeArray m v True+++dff :: Graph -> Forest Vertex+dff g = dfs g (vertices g)++dfs :: Graph -> [Vertex] -> Forest Vertex+dfs g vs = prune (bounds g) (map (generate g) vs)++generate :: Graph -> Vertex -> Tree Vertex+generate g v = Node v (map (generate g) (g!v))++prune :: Bounds -> Forest Vertex -> Forest Vertex+prune bnds ts = runST (mkEmpty bnds >>= \m ->+ chop m ts)++chop :: Set s -> Forest Vertex -> ST s (Forest Vertex)+chop _ [] = return []+chop m (Node v ts : us)+ = contains m v >>= \visited ->+ if visited then+ chop m us+ else+ include m v >>= \_ ->+ chop m ts >>= \as ->+ chop m us >>= \bs ->+ return (Node v as : bs)+++{-+%************************************************************************+%* *+%* Algorithms+%* *+%************************************************************************+-}++------------------------------------------------------------+-- Algorithm 1: depth first search numbering+------------------------------------------------------------++preorder :: Tree a -> [a]+preorder (Node a ts) = a : preorderF ts++preorderF :: Forest a -> [a]+preorderF ts = concat (map preorder ts)++{- UNUSED:+preOrd :: Graph -> [Vertex]+preOrd = preorderF . dff+-}++tabulate :: Bounds -> [Vertex] -> Table Int+tabulate bnds vs = array bnds (zipWith (,) vs [1..])++preArr :: Bounds -> Forest Vertex -> Table Int+preArr bnds = tabulate bnds . preorderF+++------------------------------------------------------------+-- Algorithm 2: topological sorting+------------------------------------------------------------++postorder :: Tree a -> [a]+postorder (Node a ts) = postorderF ts ++ [a]++postorderF :: Forest a -> [a]+postorderF ts = concat (map postorder ts)++postOrd :: Graph -> [Vertex]+postOrd = postorderF . dff++topSort :: Graph -> [Vertex]+topSort = reverse . postOrd+++------------------------------------------------------------+-- Algorithm 3: connected components+------------------------------------------------------------++components :: Graph -> Forest Vertex+components = dff . undirected++undirected :: Graph -> Graph+undirected g = buildG (bounds g) (edges g ++ reverseE g)+++------------------------------------------------------------+-- Algorithm 4: strongly connected components+------------------------------------------------------------++scc :: Graph -> Forest Vertex+scc g = dfs g (reverse (postOrd (transposeG g)))+++------------------------------------------------------------+-- Algorithm 5: Classifying edges+------------------------------------------------------------++{- UNUSED:+tree :: Bounds -> Forest Vertex -> Graph+tree bnds ts = buildG bnds (concat (map flat ts))+ where+ flat (Node v rs) = [ (v, w) | Node w us <- ts ] +++ concat (map flat ts)++-}++back :: Graph -> Table Int -> Graph+back g post = mapT select g+ where select v ws = [ w | w <- ws, post!v < post!w ]++cross :: Graph -> Table Int -> Table Int -> Graph+cross g pre post = mapT select g+ where select v ws = [ w | w <- ws, post!v > post!w, pre!v > pre!w ]++forward :: Graph -> Graph -> Table Int -> Graph+forward g tree pre = mapT select g+ where select v ws = [ w | w <- ws, pre!v < pre!w ] \\ tree!v+++------------------------------------------------------------+-- Algorithm 6: Finding reachable vertices+------------------------------------------------------------++reachable :: Graph -> Vertex -> [Vertex]+reachable g v = preorderF (dfs g [v])++path :: Graph -> Vertex -> Vertex -> Bool+path g v w = w `elem` (reachable g v)++------------------------------------------------------------+-- Algorithm 7: Biconnected components+------------------------------------------------------------+++bcc :: Graph -> Forest [Vertex]+bcc g = (concat . map bicomps . map (label g dnum)) forest+ where forest = dff g+ dnum = preArr (bounds g) forest++label :: Graph -> Table Int -> Tree Vertex -> Tree (Vertex,Int,Int)+label g dnum (Node v ts) = Node (v,dnum!v,lv) us+ where us = map (label g dnum) ts+ lv = minimum ([dnum!v] ++ [dnum!w | w <- g!v]+ ++ [lu | Node (_, _, lu) _ <- us])++bicomps :: Tree (Vertex,Int,Int) -> Forest [Vertex]+bicomps (Node (v,_,_) ts)+ = [ Node (v:vs) us | (_, Node vs us) <- map collect ts]++collect :: Tree (Vertex,Int,Int) -> (Int, Tree [Vertex])+collect (Node (v,dv,lv) ts) = (lv, Node (v:vs) cs)+ where collected = map collect ts+ vs = concat [ ws | (lw, Node ws _) <- collected, lw<dv]+ cs = concat [ if lw<dv then us else [Node (v:ws) us]+ | (lw, Node ws us) <- collected ]+
+ Djinn/Util/Sort.hs view
@@ -0,0 +1,110 @@+{- Copyright (c) 2001,2002 Galois Connections, Inc.+ -}+{- |+ + Module : Util.Sort+ Copyright : (c) Galois Connections 2001, 2002++ Maintainer : lib@galois.com+ Stability : + Portability : + + Extra sorting functions - copied from GHC compiler sources (util\/Util.lhs)+-}+module Util.Sort where++sortLt :: (a -> a -> Bool) -- Less-than predicate+ -> [a] -- Input list+ -> [a] -- Result list++sortLt lt l = qsort lt l []++-- qsort is stable and does not concatenate.+qsort :: (a -> a -> Bool) -- Less-than predicate+ -> [a] -- xs, Input list+ -> [a] -- r, Concatenate this list to the sorted input list+ -> [a] -- Result = sort xs ++ r++qsort _ [] r = r+qsort _ [x] r = x:r+qsort lt (x:xs) r = qpart lt x xs [] [] r++-- qpart partitions and sorts the sublists+-- rlt contains things less than x,+-- rge contains the ones greater than or equal to x.+-- Both have equal elements reversed with respect to the original list.++qpart :: (a -> a -> Bool) -> a -> [a] -> [a] -> [a] -> [a] -> [a]+qpart lt x [] rlt rge r =+ -- rlt and rge are in reverse order and must be sorted with an+ -- anti-stable sorting+ rqsort lt rlt (x : rqsort lt rge r)++qpart lt x (y:ys) rlt rge r =+ if lt y x then+ -- y < x+ qpart lt x ys (y:rlt) rge r+ else+ -- y >= x+ qpart lt x ys rlt (y:rge) r++-- rqsort is as qsort but anti-stable, i.e. reverses equal elements+rqsort :: (a -> a -> Bool) -- Less-than predicate+ -> [a] -- xs, Input list+ -> [a] -- r, Concatenate this list to the sorted input+ -> [a] -- Result = sort xs ++ r+rqsort _ [] r = r+rqsort _ [x] r = x:r+rqsort lt (x:xs) r = rqpart lt x xs [] [] r++rqpart :: (a -> a -> Bool) -> a -> [a] -> [a] -> [a] -> [a] -> [a]+rqpart lt x [] rle rgt r =+ qsort lt rle (x : qsort lt rgt r)++rqpart lt x (y:ys) rle rgt r =+ if lt x y then+ -- y > x+ rqpart lt x ys rle (y:rgt) r+ else+ -- y <= x+ rqpart lt x ys (y:rle) rgt r++sortLe :: (a->a->Bool) -> [a] -> [a]+sortLe le = generalNaturalMergeSort le++mergeSort, naturalMergeSort :: Ord a => [a] -> [a]+mergeSort = generalMergeSort (<=)+naturalMergeSort = generalNaturalMergeSort (<=)++generalMergeSort :: (a->a->Bool) -> [a] -> [a]+generalMergeSort _ [] = []+generalMergeSort p xs = (balancedFold (generalMerge p) . map (: [])) xs++generalMerge :: (a -> a -> Bool) -> [a] -> [a] -> [a]+generalMerge _ xs [] = xs+generalMerge _ [] ys = ys+generalMerge p (x:xs) (y:ys) | x `p` y = x : generalMerge p xs (y:ys)+ | otherwise = y : generalMerge p (x:xs) ys++balancedFold :: (a -> a -> a) -> [a] -> a+balancedFold _ [] = error "Util.Sort.balancedFold: can't reduce an empty list"+balancedFold _ [x] = x+balancedFold f l = balancedFold f (balancedFold' f l)++balancedFold' :: (a -> a -> a) -> [a] -> [a]+balancedFold' f (x:y:xs) = f x y : balancedFold' f xs+balancedFold' _ xs = xs++generalNaturalMergeSort :: (a -> a -> Bool) -> [a] -> [a]+generalNaturalMergeSort _ [] = []+generalNaturalMergeSort prd rs = (balancedFold (generalMerge prd) . group prd) rs+ where+ --group :: (a -> a -> Bool) -> [a] -> [[a]]+ group _ [] = []+ group p (l:ls) = group' ls l l (l:)+ where+ group' [] _ _ s = [s []]+ group' (x:xs) x_min x_max s + | not (x `p` x_max) = group' xs x_min x (s . (x :)) + | x `p` x_min = group' xs x x_max ((x :) . s) + | otherwise = s [] : group' xs x x (x :)
+ LICENSE view
@@ -0,0 +1,32 @@+Copyright (c) 2005 Lennart Augustsson, Thomas Johnsson+ Chalmers University of Technology+All rights reserved.++This code is derived from software written by Lennart Augustsson+(lennart@augustsson.net).++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:+1. Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.+2. Redistributions in binary form must reproduce the above copyright+ notice, this list of conditions and the following disclaimer in the+ documentation and/or other materials provided with the distribution.+3. None of the names of the copyright holders may be used to endorse+ or promote products derived from this software without specific+ prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS ``AS IS'' AND ANY+EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR+PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE+LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR+CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF+SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR+BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,+WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE+OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN+IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.++*** End of disclaimer. ***
+ Setup.lhs view
@@ -0,0 +1,6 @@+#!/usr/bin/runhaskell+> module Main where++> import Distribution.Simple++> main = defaultMain
+ djinn.cabal view
@@ -0,0 +1,22 @@+Name: djinn+Version: 2008.1.18+License: BSD3+License-file: LICENSE+Author: Lennart Augustsson+Maintainer: lennart@augustsson.net+Description: Djinn uses an theorem prover for intuitionistic propositional logic+ to generate a Haskell expression when given a type.+Category: source-tools+Homepage: http://www.augustsson.net/Darcs/Djinn/+Synopsis: Generate Haskell code from a type+Build-Depends: base, mtl, readline, pretty, array, containers++Executable: djinn+Main-Is: Djinn.hs+Hs-Source-Dirs: Djinn/+Other-modules: Help, LJTParse, HCheck, LJT, MLJT+ HTypes, LJTFormula, REPL,+ Util.Digraph, Util.Sort++ghc-options: -O2 -Wall -Werror -optl-Wl+ghc-prof-options: -prof -auto-all