diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. *** diff --git a/Setup.lhs b/Setup.lhs new file mode 100644 --- /dev/null +++ b/Setup.lhs @@ -0,0 +1,6 @@ +#!/usr/bin/env runhaskell +> module Main where + +> import Distribution.Simple + +> main = defaultMain diff --git a/djinn-lib.cabal b/djinn-lib.cabal new file mode 100644 --- /dev/null +++ b/djinn-lib.cabal @@ -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 diff --git a/src/Djinn/HCheck.hs b/src/Djinn/HCheck.hs new file mode 100644 --- /dev/null +++ b/src/Djinn/HCheck.hs @@ -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 _ _) = [] diff --git a/src/Djinn/HTypes.hs b/src/Djinn/HTypes.hs new file mode 100644 --- /dev/null +++ b/src/Djinn/HTypes.hs @@ -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 ] + diff --git a/src/Djinn/LJT.hs b/src/Djinn/LJT.hs new file mode 100644 --- /dev/null +++ b/src/Djinn/LJT.hs @@ -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 + +--------------------------- diff --git a/src/Djinn/LJTFormula.hs b/src/Djinn/LJTFormula.hs new file mode 100644 --- /dev/null +++ b/src/Djinn/LJTFormula.hs @@ -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 _ = []