djinn 2008.1.18 → 2008.8.10
raw patch · 20 files changed
+1900/−2411 lines, 20 filessetup-changed
Files
- Djinn/Djinn.hs +0/−387
- Djinn/HCheck.hs +0/−152
- Djinn/HTypes.hs +0/−452
- Djinn/Help.hs +0/−177
- Djinn/LJT.hs +0/−468
- Djinn/LJTFormula.hs +0/−103
- Djinn/LJTParse.hs +0/−98
- Djinn/MLJT.hs +0/−30
- Djinn/REPL.hs +0/−34
- Djinn/Util/Digraph.hs +0/−393
- Djinn/Util/Sort.hs +0/−110
- Setup.lhs +1/−1
- djinn.cabal +6/−6
- src/Djinn.hs +425/−0
- src/HCheck.hs +154/−0
- src/HTypes.hs +507/−0
- src/Help.hs +202/−0
- src/LJT.hs +468/−0
- src/LJTFormula.hs +103/−0
- src/REPL.hs +34/−0
− Djinn/Djinn.hs
@@ -1,387 +0,0 @@------ 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
@@ -1,152 +0,0 @@------ 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
@@ -1,452 +0,0 @@------ 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
@@ -1,177 +0,0 @@-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
@@ -1,468 +0,0 @@------ 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
@@ -1,103 +0,0 @@------ 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
@@ -1,98 +0,0 @@------ 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
@@ -1,30 +0,0 @@------ 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
@@ -1,34 +0,0 @@------ 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
@@ -1,393 +0,0 @@-{- |- - 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
@@ -1,110 +0,0 @@-{- 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 :)
Setup.lhs view
@@ -1,4 +1,4 @@-#!/usr/bin/runhaskell+#!/usr/bin/env runhaskell > module Main where > import Distribution.Simple
djinn.cabal view
@@ -1,5 +1,5 @@ Name: djinn-Version: 2008.1.18+Version: 2008.8.10 License: BSD3 License-file: LICENSE Author: Lennart Augustsson@@ -9,14 +9,14 @@ Category: source-tools Homepage: http://www.augustsson.net/Darcs/Djinn/ Synopsis: Generate Haskell code from a type+Build-type: Simple 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+Hs-Source-Dirs: src+Other-modules: Help, HCheck, LJT, HTypes, LJTFormula, REPL -ghc-options: -O2 -Wall -Werror -optl-Wl+--ghc-options: -O2 -Wall -Werror -optl-Wl+ghc-options: -Wall -optl-Wl ghc-prof-options: -prof -auto-all
+ src/Djinn.hs view
@@ -0,0 +1,425 @@+--+-- Copyright (c) 2005 Lennart Augustsson+-- See LICENSE for licensing details.+--+module Main(main) where+import Data.Char(isAlpha, isSpace)+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 HTypes+import HCheck(htCheckEnv, htCheckType)+import Help++--import Debug.Trace++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 = 200+ }+ 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-08-10"++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 $ prHSymbolOp 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) =+ query s i ctx g+runCmd s (Class c) = do+ return (False, s { classes = c : classes s })++query :: State -> String -> [Context] -> HType -> IO (Bool, State)+query s 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 ps' = take (cutOff s) ps+ let score 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 --trace (hPrClause c ++ " ++++ " ++ show r)+ (r, c)+ e:es = nub $ + if sorted s then+ map snd $ sortBy (\ (x,_) (y,_) -> compare x y) $ map score ps'+ else+ map (termToHClause i) ps'+ pr = putStrLn . hPrClause+ sctx = if null ctx then "" else showContexts ctx ++ " => "+ when (debug s) $ putStrLn ("+++ " ++ show (head ps))+ putStrLn $ prHSymbolOp i ++ " :: " ++ sctx ++ show g+ pr e+ when (multi s) $ mapM_ (\ x -> putStrLn "-- or" >> pr x) es+ return (False, 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) = prHSymbolOp i ++ " :: " ++ show t++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),+ (":verboseHelp", "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 <methods>", "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 +++ pHSymbolOp+ return $ Del s++pLoad :: ReadP Cmd+pLoad = do+ skipSpaces+ s <- munch1 (not . isSpace)+ return $ Load s++pAdd :: ReadP Cmd+pAdd = do+ i <- pHSymbolOp+ sstring "::"+ t <- pHType+ optional $ schar ';'+ return $ Add i t++pQuery :: ReadP Cmd+pQuery = do+ i <- pHSymbolOp+ 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)+ ctx <- + do+ schar '('+ ctx <- sepBy1 pCtx (schar ',')+ schar ')'+ return ctx+ ++++ do+ ctx <- pCtx+ return [ctx]+ sstring "=>"+ return ctx++pType :: ReadP Cmd+pType = do+ sstring "type"+ syn <- pHSymbol True+ do args <- many (pHSymbol False)+ schar '='+ t <- pHType+ return $ Type (syn, (args, t, undefined))+ ++++ do+ schar ':'; char ':'+ k <- pHKind+ return $ Type (syn, ([], HTAbstract syn k, 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))+ ++++ do+ 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+ i <- pHSymbolOp+ sstring "::"+ t <- pHType+ return (i, t)++pHSymbolOp :: ReadP HSymbol+pHSymbolOp = do+ let pOpSym = satisfy (`elem` "~!#$%^&*-+=<>.:")+ pHSymbol False +++ do schar '('; op <- many1 pOpSym; schar ')'; return op++pSet :: ReadP Cmd+pSet = pSetFlag +++ pSetVal++pSetFlag :: ReadP Cmd+pSetFlag = 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++pSetVal :: ReadP Cmd+pSetVal = do+ pPrefix "cutoff"+ schar '='+ n <- many1 (satisfy (`elem` ['0'..'9']))+ return $ Set $ \ s -> s { cutOff = read n }++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 ] +++ [ " cutoff=" ++ show (cutOff s) ++ " maximum number of solutions generated" ]+
+ src/HCheck.hs view
@@ -0,0 +1,154 @@+--+-- 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 Data.Graph(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 _ _ (HTAbstract _ k) = return k+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+iHKind _ (HTAbstract _ _) = error "iHKind HTAbstract"++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: " ++ show (k1, k2)+ 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 $ "Undefined type variable " ++ v++getConHKind :: KEnv -> HSymbol -> M HKind+getConHKind env v =+ case lookup v env of+ Just k -> return k+ Nothing -> lift $ Left $ "Undefined type " ++ v++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 ]+getHTCons (HTAbstract _ _) = []
+ src/HTypes.hs view
@@ -0,0 +1,507 @@+--+-- Copyright (c) 2005 Lennart Augustsson+-- See LICENSE for licensing details.+--+module HTypes(HKind(..), HType(..), HSymbol, hTypeToFormula, pHSymbol, pHType, pHDataType, pHTAtom, pHKind,+ prHSymbolOp,+ 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+ | HTAbstract HSymbol HKind -- XXX Uninterpreted type, like a variable but different kind checking+ 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+ showsPrec _ (HTAbstract s _) = showString s++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++pHKind :: ReadP HKind+pHKind = do+ ts <- sepBy1 pHKindA (do schar '-'; char '>')+ return $ foldr1 KArrow ts++pHKindA :: ReadP HKind+pHKindA = (do schar '*'; return KStar) +++ pParen pHKind++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 ]+substHT _ t@(HTAbstract _ _) = t+++-------------------------------+++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 (prHSymbolOp f) <+> sep [sep (map (ppPat 10) ps) <+> text "=",+ nest 2 $ ppExpr 0 e]++prHSymbolOp :: HSymbol -> String+prHSymbolOp s@(c:_) | not (isAlphaNum c) = "(" ++ s ++ ")"+prHSymbolOp s = s++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 $ collapeCase $ fixSillyAt $ 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 [ y | (x, y) <- ss, x == hs ] of+ [] -> HPVar hs+ [p] -> HPAt hs p+ ps -> HPAt hs $ foldr1 combPat ps++ combPat p p' | p == p' = p+ combPat (HPVar v) p = HPAt v p+ combPat p (HPVar v) = HPAt v p+ combPat (HPTuple ps) (HPTuple ps') = HPTuple (zipWith combPat ps ps')+ combPat p p' = error $ "unimplemented combPat: " ++ show (p, p')++ hETuple [e] = e+ hETuple es = HETuple es++-- XXX This should be integrated into some earlier phase, but this is simpler.+fixSillyAt :: HExpr -> HExpr+fixSillyAt = fixAt []+ where fixAt s (HELam ps e) = HELam ps' (fixAt (concat ss ++ s) e) where (ps', ss) = unzip $ map findSilly ps+ fixAt s (HEApply f a) = HEApply (fixAt s f) (fixAt s a)+ fixAt _ e@(HECon _) = e+ fixAt s e@(HEVar v) = maybe e HEVar $ lookup v s+ fixAt s (HETuple es) = HETuple (map (fixAt s) es)+ fixAt s (HECase e alts) = HECase (fixAt s e) (map (fixAtAlt s) alts)+ fixAtAlt s (p, e) = (p', fixAt (s' ++ s) e) where (p', s') = findSilly p+ findSilly p@(HPVar _) = (p, [])+ findSilly p@(HPCon _) = (p, [])+ findSilly (HPTuple ps) = (HPTuple ps', concat ss) where (ps', ss) = unzip $ map findSilly ps+ findSilly (HPAt v p) = case findSilly p of+ (p'@(HPVar v'), s) -> (p', (v, v'):s)+ (p', s) -> (HPAt v p', s)+ findSilly (HPApply f a) = (HPApply f' a', sf ++ sa) where (f', sf) = findSilly f; (a', sa) = findSilly a++-- XXX This shouldn't be needed. There's similar code in hECase,+-- but the fixSillyAt reveals new opportunities.+collapeCase :: HExpr -> HExpr+collapeCase (HELam ps e) = HELam ps (collapeCase e)+collapeCase (HEApply f a) = HEApply (collapeCase f) (collapeCase a)+collapeCase e@(HECon _) = e+collapeCase e@(HEVar _) = e+collapeCase (HETuple es) = HETuple (map collapeCase es)+collapeCase (HECase e alts) =+ case [(p, collapeCase b) | (p, b) <- alts ] of+ (p, b) : pes | noBound p && all (\ (p', b') -> alphaEq b b' && noBound p') pes -> b+ pes -> HECase (collapeCase e) pes+ where noBound = all (== "_") . getBinderVarsHP++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 ]
+ src/Help.hs view
@@ -0,0 +1,202 @@+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 a = a\n\+\ Djinn> sel ? ((a,b),(c,d)) -> (b,c)\n\+\ sel :: ((a, b), (c, d)) -> (b, c)\n\+\ sel ((_, a), (b, _)) = (a, b)\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 _ a = a\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 a = bar (foo a)\n\+\ This feature is not as powerful as it first might seem. Djinn does\n\+\*not* instantiate polymorphic functions. 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 a = a\n\+\\n\+\type <sym> :: <kind>\n\+\ Add an abstract (uninterpreted) type of the given type.\n\+\An uninterpreted type behaves like a type variable during deduction.\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 a = C a a a\n\+\\n\+\data <sym> <vars>\n\+\ Add an empty type.\n\+\\n\+\class <sym> <vars> where <methods>\n\+\ Add a type class. Example:\n\+\ class Ord a where compare :: a -> a -> Ordering\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\+\ cutoff=N compute at most N solutions\n\+\ The heuristic used to sort the solutions is that as many of the\n\+\bound variables as possible should be used and that the function\n\+\should be as short as possible.\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 a = CD (\\ b -> b a)\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 a b =\n\+\ case a of\n\+\ CD c -> CD (\\ d ->\n\+\ c (\\ e ->\n\+\ case b e of\n\+\ CD f -> f d))\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 a =\n\+\ CD (\\ b ->\n\+\ case a (\\ c -> CD (\\ _ -> b c)) of\n\+\ CD d -> d b)\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 a b = (a, b)\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 a b c =\n\+\ case a c of\n\+\ (d, e) -> b d e\n\+\\n\+\\n\+\ The function type may have a type class context, e.g.,\n\+\ Djinn> refl ? (Eq a) => a -> Bool\n\+\ refl :: (Eq a) => a -> Bool\n\+\ refl a = a == a\n\+\A context is simply interpreted as an additional (hidden) argument\n\+\that contains all the methods. Again, there is no instantiation of\n\+\polymorphic functions, so classes where the methods are polymorphic\n\+\do not work as expected.\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\+\sometimes called Void in Haskell, and Djinn assumes an elimination\n\+\rule for the 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 a = void (a (Right (\\ b -> a (Left b))))\n\+\ The Not type has the definition 'type Not x = x -> Void'. The\n\+\regular version of the law of excluded middle cannot be proven, of\n\+\course.\n\+\ Djinn> f ? Either x (Not x)\n\+\ -- f cannot be realized.\n\+\"
+ src/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 use 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++---------------------------
+ src/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 _ = []
+ src/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