djinn 2014.9.7 → 2025.2.21
raw patch · 5 files changed
+51/−44 lines, 5 filesdep ~arraydep ~containersdep ~haskeline
Dependency ranges changed: array, containers, haskeline, mtl, pretty
Files
- djinn.cabal +11/−5
- src/Djinn.hs +9/−10
- src/HCheck.hs +5/−5
- src/HTypes.hs +24/−22
- src/LJT.hs +2/−2
djinn.cabal view
@@ -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
src/Djinn.hs view
@@ -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" ]-
src/HCheck.hs view
@@ -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 =
src/HTypes.hs view
@@ -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.
src/LJT.hs view
@@ -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' ]