djinn-lib (empty) → 0.0.1
raw patch · 7 files changed
+1313/−0 lines, 7 filesdep +basedep +containersdep +mtlsetup-changed
Dependencies added: base, containers, mtl, pretty
Files
- LICENSE +32/−0
- Setup.lhs +6/−0
- djinn-lib.cabal +25/−0
- src/Djinn/HCheck.hs +161/−0
- src/Djinn/HTypes.hs +523/−0
- src/Djinn/LJT.hs +459/−0
- src/Djinn/LJTFormula.hs +107/−0
+ LICENSE view
@@ -0,0 +1,32 @@+Copyright (c) 2005 Lennart Augustsson, Thomas Johnsson+ Chalmers University of Technology+All rights reserved.++This code is derived from software written by Lennart Augustsson+(lennart@augustsson.net).++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:+1. Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.+2. Redistributions in binary form must reproduce the above copyright+ notice, this list of conditions and the following disclaimer in the+ documentation and/or other materials provided with the distribution.+3. None of the names of the copyright holders may be used to endorse+ or promote products derived from this software without specific+ prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS ``AS IS'' AND ANY+EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR+PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE+LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR+CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF+SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR+BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,+WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE+OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN+IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.++*** End of disclaimer. ***
+ Setup.lhs view
@@ -0,0 +1,6 @@+#!/usr/bin/env runhaskell+> module Main where++> import Distribution.Simple++> main = defaultMain
+ djinn-lib.cabal view
@@ -0,0 +1,25 @@+name: djinn-lib+version: 0.0.1+cabal-version: >= 1.2+license: BSD3+license-file: LICENSE+author: Lennart Augustsson+maintainer: trupill@gmail.com+synopsis: Generate Haskell code from a type. Library extracted from djinn package.+description: Djinn uses an theorem prover for intuitionistic propositional logic+ to generate a Haskell expression when given a type.+ This is a library extracted from Djinn sources.+category: source-tools+homepage: http://www.augustsson.net/Darcs/Djinn/+build-type: Simple++library+ hs-source-dirs: src+ build-depends: base >= 4 && < 5,+ mtl,+ containers,+ pretty+ exposed-modules: Djinn.HCheck,+ Djinn.HTypes,+ Djinn.LJT,+ Djinn.LJTFormula
+ src/Djinn/HCheck.hs view
@@ -0,0 +1,161 @@+{-# LANGUAGE CPP #-}+--+-- Copyright (c) 2005 Lennart Augustsson+-- See LICENSE for licensing details.+--+module Djinn.HCheck (+ htCheckEnv,+ htCheckType+) where++import Data.List (union)+--import Control.Monad.Trans+#if MIN_VERSION_mtl(2,2,0)+import Control.Monad.Except ()+#else+import Control.Monad.Error ()+#endif+import Control.Monad.State+import Data.Graph (SCC (..), stronglyConnComp)+import Data.IntMap (IntMap, empty, insert, (!))++import Djinn.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/Djinn/HTypes.hs view
@@ -0,0 +1,523 @@+--+-- Copyright (c) 2005 Lennart Augustsson+-- See LICENSE for licensing details.+--+module Djinn.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 Control.Monad (zipWithM)+import Data.Char (isAlpha, isAlphaNum, isUpper)+import Data.List (union, (\\))+import Text.ParserCombinators.ReadP+import Text.PrettyPrint.HughesPJ (Doc, comma, fsep, nest, parens,+ punctuate, renderStyle, sep,+ style, text, vcat, ($$), (<+>), (<>))++import Djinn.LJTFormula++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@(c:_)) | not (isAlpha c) = showParen True $ 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) ++++ do schar '('; schar '-'; schar '>'; schar ')'; 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++hTApp :: HType -> HType -> HType+hTApp (HTApp (HTCon "->") a) b = HTArrow a b+hTApp a b = HTApp a b++-------------------------------+++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/Djinn/LJT.hs view
@@ -0,0 +1,459 @@+--+-- 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 Djinn.LJT (+ module Djinn.LJTFormula,+ provable,+ prove,+ Proof+) where++import Control.Applicative (Applicative, Alternative, pure, (<*>), empty, (<|>))+import Control.Monad+import Data.List (partition)+import Debug.Trace++import Djinn.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 Applicative P where+ pure = return+ (<*>) = ap++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 Alternative P where+ empty = mzero+ (<|>) = mplus++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.+ 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 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)++ -- 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/Djinn/LJTFormula.hs view
@@ -0,0 +1,107 @@+--+-- Copyright (c) 2005 Lennart Augustsson+-- See LICENSE for licensing details.+--+module Djinn.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+ 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 _ = []