diff --git a/djinn.cabal b/djinn.cabal --- a/djinn.cabal +++ b/djinn.cabal @@ -1,17 +1,17 @@ +Cabal-version: 3.0 Name: djinn -Version: 2014.9.7 +Version: 2025.2.21 Synopsis: Generate Haskell code from a type Description: Djinn uses an theorem prover for intuitionistic propositional logic to generate a Haskell expression when given a type. -Bug-reports: https://github.com/haskell/augustss/djinn/issues -License: BSD3 +Bug-reports: https://github.com/augustss/djinn/issues +License: BSD-3-Clause License-File: LICENSE Author: Lennart Augustsson Maintainer: Lennart Augustsson Copyright: 2014 Lennart Augustsson Category: source-tools Build-type: Simple -Cabal-Version: >= 1.8 Stability: experimental source-repository head @@ -19,9 +19,15 @@ location: https://github.com/augustss/djinn executable djinn + Default-Language: Haskell98 Main-Is: Djinn.hs - Build-Depends: base >= 4 && < 6, mtl, haskeline -any, pretty, array, containers + Build-Depends: base >= 4 && < 6, + mtl < 10, + haskeline < 10, + pretty < 10, + array < 10, + containers < 10 Other-modules: Help, HCheck, LJT, HTypes, LJTFormula, REPL diff --git a/src/Djinn.hs b/src/Djinn.hs --- a/src/Djinn.hs +++ b/src/Djinn.hs @@ -9,7 +9,7 @@ import Data.Ratio import Text.ParserCombinators.ReadP import Control.Monad(when) -import Control.Monad.Error() +import Control.Monad.Except() import System.Exit import System.Environment @@ -149,16 +149,16 @@ putStr $ helpText ++ unlines (map getHelp commands) ++ getSettings s when verbose $ putStr verboseHelp return (False, s) -runCmd s Quit = +runCmd s Quit = return (True, s) runCmd s (Load f) = loadFile s f -runCmd s (Add i t) = +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) : filter ((/= i) . fst) (axioms s) }) runCmd _ Clear = return (False, startState) -runCmd s (Del i) = +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) }) @@ -210,21 +210,21 @@ putStrLn $ "-- " ++ i ++ " cannot be realized." return (False, s) ps -> do - let ps' = take (cutOff s) ps + 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 $ + 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)) + when (debug s) $ putStrLn ("+++ " ++ show (ps !! 0)) when prType $ putStrLn $ prHSymbolOp i ++ " :: " ++ sctx ++ show g pr e when (multi s) $ mapM_ (\ x -> putStrLn "-- or" >> pr x) es @@ -350,7 +350,7 @@ pContext :: ReadP [Context] pContext = do let pCtx = do c <- pHSymbol True; ts <- many pHTAtom; return (c, ts) - ctx <- + ctx <- do schar '(' ctx <- sepBy1 pCtx (schar ',') @@ -417,7 +417,7 @@ pSetFlag :: ReadP Cmd pSetFlag = do - val <- (do schar '+'; return True) +++ (do schar '-'; return False) + val <- (do schar '+'; return True) +++ (do schar '-'; return False) f <- foldr (+++) pfail [ do pPrefix s; return (set val) | (s, _, _, set) <- options ] return $ Set $ f @@ -463,4 +463,3 @@ "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" ] - diff --git a/src/HCheck.hs b/src/HCheck.hs --- a/src/HCheck.hs +++ b/src/HCheck.hs @@ -4,8 +4,8 @@ -- module HCheck(htCheckEnv, htCheckType) where import Data.List(union) ---import Control.Monad.Trans -import Control.Monad.Error() +import Control.Monad(liftM2) +import Control.Monad.Except() import Control.Monad.State import Data.IntMap(IntMap, insert, (!), empty) import Data.Graph(stronglyConnComp, SCC(..)) @@ -48,7 +48,7 @@ let vs = getHTVars t ks <- mapM (const newKVar) vs let env = zip vs ks ++ [(i, k) | (i, (_, _, k)) <- its ] - iHKindStar env t + iHKindStar env t htCheckEnv :: [(HSymbol, ([HSymbol], HType, a))] -> Either String [(HSymbol, ([HSymbol], HType, HKind))] htCheckEnv its = @@ -107,7 +107,7 @@ unifyK :: HKind -> HKind -> M () unifyK k1 k2 = do - let follow k@(KVar i) = getVar i >>= return . maybe k id + 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 @@ -121,7 +121,7 @@ k1' <- follow k1 k2' <- follow k2 unify k1' k2' - + getVarHKind :: KEnv -> HSymbol -> M HKind getVarHKind env v = diff --git a/src/HTypes.hs b/src/HTypes.hs --- a/src/HTypes.hs +++ b/src/HTypes.hs @@ -7,6 +7,7 @@ prHSymbolOp, htNot, isHTUnion, getHTVars, substHT, HClause, HPat, HExpr(HEVar), hPrClause, termToHExpr, termToHClause, getBinderVars) where +import Prelude hiding ((<>)) import Text.PrettyPrint.HughesPJ(Doc, renderStyle, style, text, (<>), parens, ($$), vcat, punctuate, sep, fsep, nest, comma, (<+>)) import Data.Char(isAlphaNum, isAlpha, isUpper) @@ -14,6 +15,7 @@ import Control.Monad(zipWithM) import Text.ParserCombinators.ReadP import LJTFormula +import Prelude hiding ((<>)) --import Debug.Trace @@ -32,7 +34,7 @@ | 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 + | HTAbstract HSymbol HKind -- XXX Uninterpreted type, like a variable but different kind checking deriving (Eq) isHTUnion :: HType -> Bool @@ -161,7 +163,7 @@ 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 = +hTypeToFormula ss t = case expandSyn ss t [] of Nothing -> PVar $ Symbol $ show t Just t' -> hTypeToFormula ss t' @@ -208,7 +210,7 @@ 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] + nest 2 $ ppExpr 0 e] prHSymbolOp :: HSymbol -> String prHSymbolOp s@(c:_) | not (isAlphaNum c) = "(" ++ s ++ ")" @@ -249,7 +251,7 @@ 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) = + conv vs (Lam s te) = let hs = unSymbol s (te', ss) = conv (hs : vs) te in (hELam [convV hs ss] te', ss) @@ -298,8 +300,8 @@ 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 = + + convAp vs f as = let (es, sss) = unzip $ map (conv vs) (f:as) in (foldl1 HEApply es, concat sss) @@ -310,10 +312,10 @@ 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') + 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 @@ -323,18 +325,18 @@ 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 + 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. diff --git a/src/LJT.hs b/src/LJT.hs --- a/src/LJT.hs +++ b/src/LJT.hs @@ -140,11 +140,11 @@ newtype P a = P { unP :: PS -> [(PS, a)] } instance Applicative P where - pure = return + pure x = P $ \ s -> [(s, x)] (<*>) = ap instance Monad P where - return x = P $ \ s -> [(s, x)] + return = pure P m >>= f = P $ \ s -> [ y | (s',x) <- m s, y <- unP (f x) s' ]