mprover (empty) → 0.0.0.0
raw patch · 13 files changed
+1304/−0 lines, 13 filesdep +basedep +containersdep +haskell98setup-changed
Dependencies added: base, containers, haskell98, mtl, parsec, pretty, transformers, unbound
Files
- LICENSE +0/−0
- MProver/Checker.hs +183/−0
- MProver/Eval.hs +246/−0
- MProver/Monad.hs +56/−0
- MProver/PPrint.hs +90/−0
- MProver/Parser.hs +446/−0
- MProver/REPL.hs +27/−0
- MProver/Syntax.hs +113/−0
- Main.hs +50/−0
- README +45/−0
- Setup.hs +2/−0
- examples/Test.hs +26/−0
- mprover.cabal +20/−0
+ LICENSE view
+ MProver/Checker.hs view
@@ -0,0 +1,183 @@+module MProver.Checker where++import MProver.Syntax+import MProver.Monad+import MProver.Eval+import MProver.PPrint++import Control.Monad.Reader+import Control.Monad.Error+import Control.Monad.Identity++import qualified Data.Map as Map+import Data.List (nub)++import Unbound.LocallyNameless++import Text.PrettyPrint.HughesPJ++--import Debug.Trace (trace)++check :: (Monad m) => Proof -> MPT m Formula+check (ForallIExpr ty b) = do+ (x,pr) <- unbind b+ fopr <- localEE (bindEnv x (Just ty,Nothing)) (check pr)+ return (ForallExpr ty (bind x fopr))+check (ProofImpl fo b) = do+ (x,pr) <- unbind b+ fopr <- localPE (bindEnv x fo) (check pr)+ return (ForallProof fo fopr)+check (ProofVar x) = do+ env <- askPE+ case Map.lookup x env of+ (Just fo) -> return fo+ _ -> throwError $ "unbound proof variable " ++ name2String x+check (ProofAppProof pr1 pr2) = do+ fopr1 <- check pr1+ fopr2 <- check pr2+ case fopr1 of+ (ForallProof fo1 fo2) -> if fo1 `aeq` fopr2+ then return fo2+ else throwError "argument type mismatch when applying proof"+ _ -> throwError "attempt to apply a proof of a formula whose classifier is not universal quantification or implication"+check (ProofAppExpr pr e) = do+ fopr <- check pr+ -- FIXME: type check e?+ case fopr of+ (ForallExpr _ b) -> do+ (x,fo) <- unbind b+ return (subst x e fo)+ _ -> throwError "attempt to apply a proof of a formula whose classifier is not universal quantification or implication"+check (ProofAnno Eval fo) = case fo of+ (FormulaEq e1 e2) -> do+ env <- ask+ ok <- tryJoin e1 e2 + if ok+ then return (FormulaEq e1 e2)+ else do+ e1_ <- ppr e1+ e2_ <- ppr e2+ throwError $ show $ text "Error: could not join terms:" $+$ nest 4 e1_ $+$ text "" $+$ text "and:" $+$ nest 4 e2_+ _ -> throwError "eval formula must be an equality"+check Eval = throwError "eval must be annotated with ::: formula"+check (Trans pr1 pr2) = do+ fopr1 <- check pr1+ fopr2 <- check pr2+ case fopr1 of+ (FormulaEq e1 e2) -> case fopr2 of+ (FormulaEq e3 e4) -> if e2 `aeq` e3+ then return (FormulaEq e1 e4)+ else do+ e2_ <- ppr e2+ e3_ <- ppr e3+ throwError $ show $ text "left and right sides of trans proof are not compatible:" $+$ nest 8 e2_ $+$ text "and" $+$ nest 8 e3_+ _ -> throwError "left side of trans proof is not an equality proof"+check (Subst b) = do+ (x,(pr,e)) <- unbind b+ fopr <- check pr+ case fopr of+ (FormulaEq e1 e2) -> return (FormulaEq (subst x e1 e) (subst x e2 e))+ _ -> throwError "\"by\" clause of a case proof is not an equality proof"+check (Symm pr) = do+ fopr <- check pr+ case fopr of+ (FormulaEq e1 e2) -> return (FormulaEq e2 e1)+ _ -> throwError "symm must be applied to an equality proof"+check (ProofCase e fo b) = do+ (x,alts) <- unbind b+ tot <- checkTotality alts+ if not tot+ then throwError "Pattern matching is not exhaustive"+ else do+ mapM_ (checkAlt e fo x) alts+ return fo+check (ProofAnno pr fo) = do+ fopr <- check pr+ if fopr `aeq` fo+ then return fo+ else do+ fo_ <- ppr fo+ fopr_ <- ppr fopr+ throwError $ show $ text "type mismatch in annotated proof. Expected:" $+$ nest 8 fo_ $+$ text "Got:" $+$ nest 8 fopr_+check (ProofBisim ctor prs) = do+ -- FIXME: need to typecheck prs's fos?+ dte <- askCE+ case Map.lookup ctor dte of+ (Just (b,n)) -> do+ (xs,ConstrDecl _ tys) <- unbind b+ if length prs /= length tys+ then throwError "wrong arity in bisim"+ else do+ fos <- mapM check prs+ -- FIXME: pattern exhaustiveness here (gonna crash with pmf in some cases)+ let eql (FormulaEq e _) = e+ eqr (FormulaEq _ e) = e+ ls = map eql fos+ rs = map eqr fos+ return (FormulaEq (foldl App (Ctor ctor) ls) (foldl App (Ctor ctor) rs))+ Nothing -> throwError "invalid constructor in bisimulation proof"++checkTotality :: (Monad m) => [ProofAlt] -> MPT m Bool+checkTotality _ = return True -- FIXME FIXME++checkAlt :: (Monad m) => Expr -> Formula -> Name Proof -> ProofAlt -> MPT m ()+checkAlt e fo x a = do+ (pa,pr) <- unbind a+ let mepa = patToExpr pa+ case mepa of+ Nothing -> throwError "proof pattern contains wildcard"+ Just epa -> do+ -- FIXME: shadow the pat vars+ fopr <- localPE (bindEnv x (FormulaEq e epa)) (check pr)+ if fo `aeq` fopr+ then return ()+ else do+ fo_ <- ppr fo+ fopr_ <- ppr fopr+ throwError $ show $ text "case alternative does not prove the needed formula." $+$ text "" $+$ text "Expected:" $+$ nest 4 fo_ $+$ text "" $+$ text "Got:" $+$ nest 4 fopr_++mkInitialEE :: [Decl] -> ExprEnv+mkInitialEE [] = Map.empty+mkInitialEE (d:ds) = case d of+ (ExprDecl mety x em) -> bindEnv x (fmap unembed mety,Just (unembed em)) (mkInitialEE ds)+ _ -> mkInitialEE ds++mkInitialPE :: [Decl] -> ProofEnv+mkInitialPE [] = Map.empty+mkInitialPE (d:ds) = case d of+ (ProofDecl efo x _) -> bindEnv x (unembed efo) (mkInitialPE ds)+ _ -> mkInitialPE ds++mkInitialDTE :: [Decl] -> DTEnv+mkInitialDTE [] = Map.empty+mkInitialDTE (d:ds) = case d of+ (DataDecl n b) -> bindEnv n (unembed b) (mkInitialDTE ds)+ _ -> mkInitialDTE ds++mkInitialCE :: (Monad m) => [Decl] -> MPT m CEnv+mkInitialCE [] = return Map.empty+mkInitialCE (d:ds) = case d of+ (DataDecl n b) -> do+ (xs,cds) <- unbind (unembed b)+ ce <- mkInitialCE ds+ let ce' = foldr (\ cd@(ConstrDecl ctor tys) env -> bindEnv ctor (bind xs cd,n) env) ce cds+ return ce'+ _ -> mkInitialCE ds++checkDecl :: (Monad m) => Decl -> MPT m ()+checkDecl d@(ProofDecl efo x ep) = do+ fo <- check (unembed ep) + if unembed efo `aeq` fo+ then return ()+ else throwError $ "proof classifier and decl classifier don't match"+checkDecl _ = return ()++checkProg :: (Monad m) => Program -> MPT m ()+checkProg (Program _ tr) = do+ ds <- untrec tr+ ce <- mkInitialCE ds+ localCE (const ce) $+ localDTE (const $ mkInitialDTE ds) $+ localPE (const $ mkInitialPE ds) $+ localEE (const $ mkInitialEE ds) $+ mapM_ checkDecl ds
+ MProver/Eval.hs view
@@ -0,0 +1,246 @@+module MProver.Eval where++import MProver.Syntax+import MProver.Monad++import Control.Monad.Reader+import Control.Monad.Identity+import Control.Monad.Error (throwError)++import qualified Data.Map as Map+import qualified Data.Set as Set+import Data.Set hiding (map)+import Data.Maybe++import Unbound.LocallyNameless hiding (union,singleton,toList)++--import Debug.Trace+--trace _ = id++-- FIXME: trying to decide if some kind of let-generalization is in order here;+-- I think maybe not, because the let-bindings should be garbage collected if+-- possible.+tryJoin :: (Monad m) => Expr -> Expr -> MPT m Bool+tryJoin e1 e2 = do+ e1' <- evalCBN e1+ e2' <- evalCBN e2+ if e1' `aeq` e2'+ then return True+ else case (e1',e2') of+ (Lambda b1,Lambda b2) -> do+ mr <- unbind2 b1 b2+ case mr of+ (Just (x,e1'',_,e2'')) -> do+ localEE (unbindEnv x) (tryJoin e1'' e2'')+ Nothing -> return False+ (Var v1,Var v2) -> return (v1==v2)+ (Ctor c1,Ctor c2) -> return (c1==c2)+ (Literal l1,Literal l2) -> return (l1==l2)+ (App _ _,App _ _) -> do+ let (f1,args1) = unnestApp e1'+ (f2,args2) = unnestApp e2'+ case (f1,f2) of+ (Ctor c,Ctor c') -> if c==c' && length args1==length args2+ then do+ rs <- mapM (uncurry tryJoin) (zip args1 args2)+ return (and rs)+ else return False+ (Var x,Var y) -> if x==y && length args1==length args2+ then do+ rs <- mapM (uncurry tryJoin) (zip args1 args2)+ return (and rs)+ else return False+ _ -> return False+ _ -> return False++evalCBN :: (Monad m) => Expr -> MPT m Expr+evalCBN (Var x) = do+ ee <- askEE+ case Map.lookup x ee of+ (Just (_,Just e)) -> evalCBN e+ _ -> return (Var x)+evalCBN (App e1 e2) = do+ e1' <- evalCBN e1+ case e1' of+ (Lambda b) -> do+ (x,e) <- unbind b+ evalCBN (subst x e2 e)+ Bottom -> return Bottom+ _ -> return (App e1' e2)+evalCBN (Case e alts) = do+ r <- doAlts e alts+ case r of+ (Just e') -> evalCBN e'+ Nothing -> return (Case e alts)+evalCBN (Let b) = do+ (r,e) <- unbind b+ let bs = unrec r+ e' <- localEE (\ ee -> foldr (\ (x,e_) ee -> bindEnv x (Nothing,Just (unembed e_)) ee) ee bs) (evalCBN e)+ if any (\ v -> elem v (fv e')) (map fst bs)+ then return (Let (bind r e'))+ else return e'+evalCBN e = return e++data MR = Yes Expr | No | Poss deriving Show++doAlts :: (Monad m) => Expr -> [Alt] -> MPT m (Maybe Expr)+doAlts e (a:as) = do+ r <- doAlt e a+ case r of+ Yes e' -> return (Just e')+ No -> doAlts e as+ Poss -> return Nothing+doAlts e [] = return (Just Bottom)++doPat :: (Monad m) => Expr -> Pat -> MPT m MatchResult+doPat e (PatVar x) = return (Match [(x,e)])+doPat e (PatCtor c) = do+ e' <- evalCBN e+ case e' of+ Lambda _ -> return NoMatch+ Var _ -> return Possible+ Ctor c' -> if c==c'+ then return (Match [])+ else return NoMatch+ Literal _ -> return NoMatch+ Let _ -> return Possible+ Case _ _ -> return Possible+ App _ _ -> do+ let (f,args) = unnestApp e'+ case f of+ Ctor c' -> return NoMatch+ _ -> return Possible+ Bottom -> return Diverge+doPat e (PatLiteral l) = do+ e' <- evalCBN e+ case e' of+ Lambda _ -> return NoMatch+ Var _ -> return Possible+ Ctor _ -> return NoMatch+ Literal l' -> if l==l'+ then return (Match [])+ else return NoMatch+ Let _ -> return Possible+ Case _ _ -> return Possible+ App _ _ -> do+ let (f,args) = unnestApp e'+ case f of+ Ctor c' -> return NoMatch+ _ -> return Possible+ Bottom -> return Diverge+doPat e PatWildcard = return (Match [])+doPat e (PatApp c ps) = do+ e' <- evalCBN e+ case e' of+ Lambda _ -> return NoMatch+ Var _ -> return Possible+ Ctor _ -> return NoMatch+ Literal _ -> return NoMatch+ Let _ -> return Possible+ Case _ _ -> return Possible+ App _ _ -> do+ let (f,args) = unnestApp e'+ case f of+ Ctor c' -> if c==c' && length ps==length args+ then doPats args ps+ else return NoMatch+ _ -> return Possible+ Bottom -> return Diverge+doPat e PatBottom = throwError "bottom pattern occurs in an expression"++doPats :: (Monad m) => [Expr] -> [Pat] -> MPT m MatchResult+doPats (e:es) (p:ps) = do+ r <- doPat e p+ case r of+ Match bs -> do+ r' <- doPats es ps+ case r' of+ Match bs' -> return (Match (bs++bs'))+ NoMatch -> return NoMatch+ Possible -> return Possible+ Diverge -> return Diverge+ NoMatch -> return NoMatch+ Possible -> return Possible+ Diverge -> return Diverge+doPats [] [] = return (Match [])++doAlt :: (Monad m) => Expr -> Alt -> MPT m MR+doAlt e alt = do+ (p,body) <- unbind alt+ r <- doPat e p+ case r of+ Match bs -> return (Yes $ substs bs body)+ NoMatch -> return No+ Possible -> return Poss+ Diverge -> return (Yes Bottom)++data MatchResult = Match [(Name Expr,Expr)] | NoMatch | Possible | Diverge deriving Show++altsMatch :: (Monad m) => [Alt] -> Expr -> MPT m (Maybe Expr)+altsMatch (a:as) e = do+ (p,b) <- unbind a+ case patMatch p e of+ (Match bs) -> return (Just $ substs bs b)+ NoMatch -> altsMatch as e+ Possible -> return Nothing+ Diverge -> return (Just Bottom)+altsMatch [] _ = return (Just Bottom)++patMatch :: Pat -> Expr -> MatchResult+patMatch PatWildcard _ = Match []+patMatch (PatVar x) e = Match [(x,e)]+patMatch (PatApp ctor ps) e = case e of+ (App _ _) -> let+ (ef,es) = unnestApp e+ in+ case ef of+ (Ctor c) | ctor == c -> zipPatMatch ps es+ | otherwise -> NoMatch+ _ -> Possible+ (Lambda _) -> NoMatch+ (Ctor _) -> NoMatch+ (Literal _) -> NoMatch+ Bottom -> Diverge+ _ -> Possible+patMatch (PatCtor ctor) e = case e of+ (Ctor c) | ctor == c -> Match []+ | otherwise -> NoMatch+ (App _ _) -> let+ (ef,es) = unnestApp e+ in+ case ef of+ (Ctor _) -> NoMatch+ _ -> Possible+ (Lambda _) -> NoMatch+ (Literal _) -> NoMatch+ Bottom -> Diverge+ _ -> Possible+patMatch (PatLiteral l) e = case e of+ (Literal l') | l == l' -> Match []+ | otherwise -> NoMatch+ (App _ _) -> let+ (ef,es) = unnestApp e+ in+ case ef of+ (Ctor _) -> NoMatch+ _ -> Possible+ (Ctor _) -> NoMatch+ (Lambda _) -> NoMatch+ Bottom -> Diverge+ _ -> Possible++zipPatMatch :: [Pat] -> [Expr] -> MatchResult+zipPatMatch ps es | length ps /= length es = NoMatch+zipPatMatch (p:ps) (e:es) = case patMatch p e of+ (Match bs) -> case zipPatMatch ps es of+ (Match bs') -> Match (bs++bs')+ r -> r+ r -> r+zipPatMatch [] [] = Match []++unnestApp :: Expr -> (Expr,[Expr])+unnestApp (App e1 e2) = let+ (ef,es) = unnestApp e1+ in+ (ef,es++[e2])+unnestApp e = (e,[])
+ MProver/Monad.hs view
@@ -0,0 +1,56 @@+{-# LANGUAGE NoMonomorphismRestriction #-}++module MProver.Monad where++import MProver.Syntax++import Control.Monad.Reader+import Control.Monad.Error+import Control.Monad.Identity++import Unbound.LocallyNameless++import Data.Map (Map)+import qualified Data.Map as Map++type MPT m = ErrorT String (ReaderT Environment (FreshMT m))+type ExprEnv = Map (Name Expr) ((Maybe Ty),(Maybe Expr))+type ProofEnv = Map (Name Proof) Formula+type DTEnv = Map String (Bind [Name Ty] [ConstrDecl])+type CEnv = Map String (Bind [Name Ty] ConstrDecl,String)+type Environment = (ExprEnv,ProofEnv,DTEnv,CEnv)++askEE :: (Monad m) => MPT m ExprEnv+askEE = do+ (ee,_,_,_) <- ask+ return ee++askPE :: (Monad m) => MPT m ProofEnv+askPE = do+ (_,pe,_,_) <- ask+ return pe++askDTE :: (Monad m) => MPT m DTEnv+askDTE = do+ (_,_,dte,_) <- ask+ return dte++askCE :: (Monad m) => MPT m CEnv+askCE = do+ (_,_,_,ce) <- ask+ return ce++localEE :: (Monad m) => (ExprEnv -> ExprEnv) -> MPT m a -> MPT m a+localEE f = local (\(ee,pe,dte,ce) -> (f ee,pe,dte,ce))++localPE :: (Monad m) => (ProofEnv -> ProofEnv) -> MPT m a -> MPT m a+localPE f = local (\(ee,pe,dte,ce) -> (ee,f pe,dte,ce))++localDTE :: (Monad m) => (DTEnv -> DTEnv) -> MPT m a -> MPT m a+localDTE f = local (\(ee,pe,dte,ce) -> (ee,pe,f dte,ce))++localCE :: (Monad m) => (CEnv -> CEnv) -> MPT m a -> MPT m a+localCE f = local (\(ee,pe,dte,ce) -> (ee,pe,dte,f ce))++unbindEnv = Map.delete+bindEnv = Map.insert
+ MProver/PPrint.hs view
@@ -0,0 +1,90 @@+{-# LANGUAGE FlexibleInstances,TypeSynonymInstances #-}++module MProver.PPrint where++import MProver.Syntax+import MProver.Monad+import MProver.Eval (unnestApp)++import Unbound.LocallyNameless++import Text.PrettyPrint.HughesPJ++import Data.Char++class Ppr p where+ ppr :: (Monad m) => p -> MPT m Doc+ +isidentifier :: String -> Bool+isidentifier (c:cs) = isAlphaNum c && all (\c -> isAlphaNum c || c == '\'' || c == '_') cs++instance Ppr Expr where+ ppr (Lambda b) = do+ (x,e) <- unbind b+ e_ <- ppr e+ return $ parens $ text "\\" <+> text (name2String x) <+> text "->" <+> e_+ ppr (Var x) = if isidentifier (name2String x) then return $ text $ name2String x else return $ parens $ text $ name2String x+ ppr (Ctor c) = return $ text c+ ppr (Literal l) = ppr l+ ppr (Let b) = do+ (r,e) <- unbind b+ let ds = unrec r+ ds_ <- mapM ppr ds+ e_ <- ppr e+ return $ parens $ text "let" $+$ (nest 2 $ braces $ vcat $ punctuate semi ds_) $+$ text "in" $+$ (nest 2 e_)+ ppr (Case e as) = do+ e_ <- ppr e+ as_ <- mapM ppr as+ return $ parens $ text "case" <+> e_ <+> text "of" $+$ (nest 2 $ braces $ vcat $ punctuate semi as_)+ ppr (App e1 e2) = do+ let (f,args) = unnestApp (App e1 e2)+ args_ <- mapM ppr args+ case (f,args_) of+ (Var x,[a1_,a2_]) | not (isidentifier (name2String x)) && length args == 2 -> do+ return $ parens $ a1_ <+> text (name2String x) <+> a2_+ _ -> do+ f_ <- ppr f+ return $ parens $ f_ <+> hsep args_+ ppr Bottom = return $ text "_|_"++instance Ppr (Name Expr,Embed Expr) where+ ppr (n,em) = do+ e_ <- ppr (unembed em)+ return $ text (name2String n) <+> equals <+> e_++instance Ppr Alt where+ ppr b = do+ (p,e) <- unbind b+ p_ <- ppr p+ e_ <- ppr e+ return $ p_ <+> text "->" <+> e_++instance Ppr Pat where+ ppr (PatVar x) = return $ text $ name2String x+ ppr (PatCtor c) = return $ text c+ ppr (PatLiteral l) = ppr l+ ppr PatWildcard = return $ text "_"+ ppr (PatApp c ps) = do+ ps_ <- mapM ppr ps+ return $ parens $ text c <+> hsep ps_+ ppr PatBottom = return $ text "_|_"++instance Ppr Lit where+ ppr (LitInteger i) = return $ int (fromIntegral i)+ ppr (LitChar c) = return $ text $ show c+ ppr (LitFrac d) = return $ double d++instance Ppr Formula where+ -- FIXME: ty+ ppr (ForallExpr _ b) = do+ (x,fo) <- unbind b+ fo_ <- ppr fo+ return $ text "Forall" <+> text (name2String x) <> comma <+> fo_+ ppr (ForallProof fo1 fo2) = do+ fo1_ <- ppr fo1+ fo2_ <- ppr fo2+ return $ text "Assuming" <+> fo1_ <> comma <+> fo2_+ ppr (FormulaEq e1 e2) = do+ e1_ <- ppr e1+ e2_ <- ppr e2+ return $ lbrace <+> e1_ <+> equals <+> e2_ <+> rbrace
+ MProver/Parser.hs view
@@ -0,0 +1,446 @@+module MProver.Parser where++import MProver.Syntax++import Text.Parsec hiding (parse)+import Text.Parsec.Pos+import Text.Parsec.Expr+import Text.Parsec.Language+import qualified Text.Parsec.Token as T++import Control.Monad++import Data.Char+import Data.Ratio+import Data.Either++import Unbound.LocallyNameless hiding (Infix,Fixity,fixity)++lexer = T.makeTokenParser (haskellDef {+ T.reservedNames = ["Forall","Foralli","Assume","Assuming","eval","subst","trans","symm","proving","by"] ++ T.reservedNames haskellDef,+ T.reservedOpNames = [":::","_|_"] ++ T.reservedOpNames haskellDef})++symbol = T.symbol lexer+reserved = T.reserved lexer+reservedOp = T.reservedOp lexer+identifier = try $ do+ i <- T.identifier lexer + if isLower (head i)+ then return i+ else fail "expecting identifier"+ctor = try $ do+ i <- T.identifier lexer+ if isUpper (head i)+ then return i+ else fail "expecting constructor"+lparen = symbol "("+rparen = symbol ")"+lcurly = symbol "{"+rcurly = symbol "}"+parens = T.parens lexer+braces = T.braces lexer+brackets = T.brackets lexer+comma = T.comma lexer+operator = T.operator lexer+semi = T.semi lexer+natural = T.natural lexer+float = T.float lexer+stringLiteral = T.stringLiteral lexer+charLiteral = T.charLiteral lexer++-- Parser state is a bool indicating whether we are parsing in a context where+-- bottom is okay in expressions/patterns; and a list of fixity declarations+-- currently in scope.+type UserState = (Bool,[FixityDecl])++withBotok b m = do+ (botok,fixitydecls) <- getState+ putState (b,fixitydecls)+ r <- m+ (_,fixitydecls) <- getState+ putState (botok,fixitydecls)+ return r++program = do+ fixitydecls <- lookAhead getFixityDecls+ (botok,_) <- getState+ putState (botok,fixitydecls)+ p <- program'+ eof+ return p++getFixityDecls = do+ optionMaybe (reserved "module" >> ctor >> reserved "where")+ liftM rights (braces (topdecl `sepBy` semi))++program' = do+ reserved "module"+ modname <- ctor+ reserved "where"+ topdecls <- liftM lefts (braces (topdecl `sepBy` semi))+ return $ Program modname (trec topdecls)+ <|> do+ topdecls <- liftM lefts (braces (topdecl `sepBy` semi))+ return $ Program "Main" (trec topdecls)+ <?> "program"++topdecl = liftM Left typedecl+ <|> liftM Left datadecl+ <|> liftM Left (try defn)+ <|> liftM Left proofdecl+ <|> liftM Right fixitydecl+ <?> "top-level declaration"++typedecl = do+ reserved "type"+ typename <- ctor+ vars <- many identifier+ reservedOp "="+ t <- ty+ return $ TypeDecl typename (embed $ bind (map string2Name vars) t)+ <?> "type declaration"++datadecl = do+ reserved "data"+ typename <- ctor+ tyvars <- many identifier+ reservedOp "="+ constrs <- constrdecl `sepBy1` reservedOp "|"+ return $ DataDecl typename (embed $ bind (map string2Name tyvars) constrs)+ <?> "datatype declaration"++constrdecl = do+ constrname <- ctor+ tys <- many aty+ return $ ConstrDecl constrname tys+ <?> "constructor declaration"++defn = do+ (x,t) <- try tysig+ semi+ e <- eqnnamed x+ return (ExprDecl (Just (embed t)) (string2Name x) (embed e))+ <|> do+ (x,e) <- eqn+ return $ (ExprDecl Nothing (string2Name x) (embed e))+ <?> "expression definition"++tysig = do+ x <- identifier+ reservedOp "::"+ t <- ty+ return $ (x,t)+ <|> do+ op <- parens operator+ reservedOp "::"+ t <- ty+ return $ (op,t)+ <?> "type signature declaration"++eqn = do+ x <- identifier+ reservedOp "="+ e <- expr+ return (x,e)+ <?> "function binding pattern"++eqnnamed n = do+ symbol n+ reservedOp "="+ e <- expr+ return e+ <?> "function binding pattern for a function named " ++ n++data Fixity = InfixL | InfixR | InfixNone deriving (Eq,Show)+data FixityDecl = FixityDecl Fixity (Maybe Integer) [Identifier]++fixity = (reserved "infixl" >> return InfixL)+ <|> (reserved "infixr" >> return InfixR)+ <|> (reserved "infix" >> return InfixNone)+ <?> "fixity"++fixitydecl = do+ f <- fixity+ p <- optionMaybe natural+ ops <- many operator+ return $ FixityDecl f p ops+ <?> "fixity declaration"++ty = do+ btys <- bty `sepBy1` (reservedOp "->")+ return (foldr1 TyArrow btys)+ <?> "type"++bty = do+ atys <- many1 aty+ return (foldl1 TyApp atys)+ <?> "type application"++aty = liftM (TyVar . string2Name) identifier+ <|> liftM TyCon ctor+ <|> do+ parens (do+ tys <- ty `sepBy` comma+ case tys of+ [] -> return (TyCon "()")+ [t] -> return t+ _ -> return $ foldl TyApp (TyCon $ "(" ++ replicate (length tys - 1) ',' ++ ")") tys+ )+ <?> "atomic type"++pat = do+ (botok,_) <- getState+ (if botok+ then (reservedOp "_|_" >> return PatBottom) <|> pat'+ else pat') <?> "pattern"+ +pat' = do+ v <- identifier+ return (PatVar (string2Name v))+ <|> do+ c <- ctor+ return (PatCtor c)+ <|> do+ l <- literal+ return (PatLiteral l)+ <|> do+ reserved "_"+ return PatWildcard+ <|> try (do+ parens (do+ c <- ctor+ ps <- many1 pat+ return (PatApp c ps)+ ))+ <|> do+ parens (do+ pats <- pat `sepBy` comma+ case pats of+ [] -> return (PatCtor "()")+ [p] -> return p+ _ -> return (PatApp ("(" ++ replicate (length pats - 1) ',' ++ ")") pats)+ )++lamexpr = do+ reservedOp "\\"+ boundvar <- identifier+ reservedOp "->"+ body <- expr+ return $ Lambda (bind (string2Name boundvar) body)+ <?> "lambda expression"++letexpr = do+ reserved "let"+ lbs <- braces (lb `sepBy1` semi)+ reserved "in"+ body <- expr+ return $ Let (bind (rec lbs) body)+ <?> "let-expression"++lb = do+ x <- identifier+ reservedOp "="+ e <- expr+ return (string2Name x,embed e)++nontopdecl = defn++caseexpr = do+ reserved "case"+ scrut <- expr+ reserved "of"+ alts <- braces (alt `sepBy` semi)+ return (Case scrut alts)+ <?> "case expression"++literal = liftM LitInteger natural+ <|> liftM LitFrac float + <|> liftM LitChar charLiteral+ <?> "literal"++alt = do+ p <- pat+ reservedOp "->"+ e <- expr+ return (bind p e)++term = do+ (botok,_) <- getState+ (if botok+ then (term' <|> (reservedOp "_|_" >> return Bottom))+ else term') <?> "expression term"++term' = lamexpr+ <|> try (liftM Literal literal)+ <|> letexpr+ <|> caseexpr+ <|> liftM (Var . string2Name) identifier+ <|> liftM Ctor ctor+ <|> (try $ parens (return ()) >> return (Ctor "()"))+ <|> (try $ parens expr)+ <|> (parens $ expr `sepBy1` comma >>= \ es -> return $ foldl App (Ctor $ "(" ++ replicate (length es - 1) ',' ++ ")") es)++mkOperatorTable = do+ (_,fixitydecls) <- getState+ let fromFixity InfixL = AssocLeft+ fromFixity InfixR = AssocRight+ fromFixity InfixNone = AssocNone++ fromPrec (Just x) = x+ fromPrec Nothing = 9++ mkCols (FixityDecl fx prec ids) =+ map (\ i ->+ Infix (do { symbol i+ ; return (\ e1 e2 -> (App (App (Var $ string2Name i) e1) e2)) })+ (fromFixity fx))+ ids++ getPrec (FixityDecl _ prec _) = fromPrec prec++ getOpers (FixityDecl _ _ os) = os++ mkRow n = concat [mkCols fd | fd <- fixitydecls, getPrec fd == n]++ allBound = concatMap getOpers fixitydecls++ approw = [Infix (do { return (\ e1 e2 -> (App e1 e2)) }) AssocLeft]+ row9 = [Infix (try $ do { oper <- operator ; if oper `elem` allBound then fail "<<shouldn't see this>>" else return (\ e1 e2 -> (App (App (Var $ string2Name oper) e1) e2)) }) AssocLeft] ++ mkRow 9+ otherRows = map mkRow [8,7,6,5,4,3,2,1,0]++ return (approw:row9:otherRows)++expr = do+ table <- mkOperatorTable+ buildExpressionParser table term <?> "expression"++proofdecl = do+ (x,fo) <- try proofsig+ semi+ pr <- proofnamed x+ return (ProofDecl (embed fo) (string2Name x) (embed pr))+ +proofsig = do+ x <- identifier+ reservedOp ":::"+ fo <- formula+ return $ (x,fo)++proofnamed x = do+ symbol x+ reservedOp "="+ p <- proof+ return p+ <?> "proof named " ++ x++data ProofTerm = PTProof Proof | PTExpr Expr | PTCtor String++proofterm = do+ reserved "Foralli"+ lparen+ x <- identifier+ reservedOp "::"+ t <- ty+ rparen+ comma+ pr <- proof+ return (PTProof $ ForallIExpr t (bind (string2Name x) pr))+ <|> do+ reserved "Assume"+ lparen+ x <- identifier+ reservedOp ":::"+ fo <- formula+ rparen+ comma+ pr <- proof+ return (PTProof $ ProofImpl fo (bind (string2Name x) pr))+ <|> (liftM PTProof $ caseproof)+ <|> (reserved "eval" >> return (PTProof Eval))+ <|> do+ reserved "trans"+ (PTProof p1) <- proofterm+ (PTProof p2) <- proofterm+ return (PTProof $ Trans p1 p2)+ <|> do+ reserved "subst"+ x <- identifier+ reserved "by"+ p <- proof+ reserved "in"+ e <- withBotok True expr+ return (PTProof $ Subst (bind (string2Name x) (p,e)))+ <|> do+ reserved "symm"+ p <- proof+ return (PTProof $ Symm p)+ <|> (liftM (PTProof . ProofVar . string2Name) $ identifier)+ <|> (liftM PTCtor ctor)+ <|> (liftM PTProof $ parens proof)+ <|> (liftM PTExpr $ brackets (withBotok True expr))+ <?> "proof term"++caseproof = do+ reserved "case"+ scrut <- withBotok True expr+ reserved "proving"+ fo <- formula+ reserved "by"+ x <- identifier+ reserved "of"+ proofalts <- braces (proofalt `sepBy` semi)+ return (ProofCase scrut fo (bind (string2Name x) proofalts))+ <?> "case expression"++proofalt = do+ p <- withBotok True pat+ reservedOp "->"+ e <- proof+ return (bind p e)++formula = do+ reserved "Forall"+ lparen+ x <- identifier+ reservedOp "::"+ t <- ty+ rparen+ comma+ fo <- formula+ return (ForallExpr t (bind (string2Name x) fo))+ <|> do+ reserved "Assuming"+ fo <- formula+ comma+ fo' <- formula+ return (ForallProof fo fo')+ <|> do+ lcurly+ e <- withBotok True expr+ reservedOp "="+ e' <- withBotok True expr+ rcurly+ return (FormulaEq e e')+ <?> "formula"++proof = do+ pts <- many1 proofterm+ mr <- optionMaybe ( do+ reservedOp ":::"+ formula+ )+ let mkProofApp (PTProof p) (PTExpr e) = PTProof (ProofAppExpr p e)+ mkProofApp (PTProof p) (PTProof p') = PTProof (ProofAppProof p p')+ mkProofApp _ _ = error "Zabonga FIXME"+ (PTProof pr) = case pts of+ (PTCtor ctor:pts') -> PTProof $ ProofBisim ctor (map (\(PTProof p) -> p) pts')+ _ -> foldl1 mkProofApp pts+ case mr of+ (Just fo) -> return (ProofAnno pr fo)+ Nothing -> return pr++parse :: FilePath -> String -> Either ParseError Program+parse filename stream = runParser program (False,[]) filename stream++parseExpr :: FilePath -> String -> Either ParseError Expr+parseExpr filename stream = runParser (expr >>= \ e -> eof >> return e) (False,[]) filename stream
+ MProver/REPL.hs view
@@ -0,0 +1,27 @@+module MProver.REPL where++import MProver.Eval+import MProver.Checker+import MProver.Monad+import MProver.Parser+import MProver.PPrint+import System.IO++import Control.Monad.IO.Class++repl :: MPT IO ()+repl = do+ liftIO $ putStr "MProver> "+ liftIO $ hFlush stdout+ inp <- liftIO $ getLine+ case inp of+ ":q" -> return ()+ "" -> repl+ _ -> do+ case parseExpr "<interactive>" inp of+ (Left err) -> liftIO $ print err+ (Right e) -> do+ e' <- evalCBN e+ e'_ <- ppr e'+ liftIO $ print e'_+ repl
+ MProver/Syntax.hs view
@@ -0,0 +1,113 @@+{-# LANGUAGE MultiParamTypeClasses,TemplateHaskell,ScopedTypeVariables,FlexibleInstances,FlexibleContexts,UndecidableInstances,TypeSynonymInstances #-}++module MProver.Syntax where++import Data.Maybe+import Data.List++import Unbound.LocallyNameless++------------------------------------------+-- Abstract syntax for MProver programs --+------------------------------------------+type Identifier = String++data Program = Program Identifier (TRec [Decl])+ deriving Show++data Decl = TypeDecl Identifier (Embed (Bind [Name Ty] Ty))+ | DataDecl Identifier (Embed (Bind [Name Ty] [ConstrDecl]))+ | ExprDecl (Maybe (Embed Ty)) (Name Expr) (Embed Expr)+ | ProofDecl (Embed Formula) (Name Proof) (Embed Proof)+ deriving Show++type ProofBind = Bind [Pat] Proof++data Expr = Lambda (Bind (Name Expr) Expr)+ | Var (Name Expr)+ | Ctor Identifier+ | Literal Lit+ | Let (Bind (Rec [(Name Expr,Embed Expr)]) Expr)+ | Case Expr [Alt]+ | App Expr Expr+ | Bottom+ deriving Show++data Lit = LitInteger Integer+ | LitChar Char+ | LitFrac Double+ deriving (Ord,Eq,Show)++type Alt = Bind Pat Expr++data Ty = TyArrow Ty Ty+ | TyApp Ty Ty+ | TyCon Identifier+ | TyVar (Name Ty)+ deriving Show+ +data Proof = ForallIExpr Ty (Bind (Name Expr) Proof) -- Foralli x::t, e+ | ProofImpl Formula (Bind (Name Proof) Proof) -- Assuming p:::fo, pr -- (FIXME: don't like that notation)+ | ProofVar (Name Proof) -- x+ | ProofAppExpr Proof Expr -- p [e]+ | ProofAppProof Proof Proof -- p1 p2+ | ProofBisim Identifier [Proof] -- Ctor p1 p2 .. pn+ | Eval -- eval+ | Trans Proof Proof -- trans p1 p2+ | Subst (Bind (Name Expr) (Proof,Expr)) -- subst x by p in e+ | Symm Proof -- symm p+ | ProofCase Expr Formula (Bind (Name Proof) [ProofAlt]) -- case e proving fo by x of { pa1; pa2; pa3 }+ | ProofAnno Proof Formula -- proof ::: formula+ deriving Show++type ProofAlt = Bind Pat Proof++data Formula = ForallExpr Ty (Bind (Name Expr) Formula)+ | ForallProof Formula Formula+ | FormulaEq Expr Expr+ deriving Show++data Pat = PatVar (Name Expr)+ | PatCtor Identifier+ | PatLiteral Lit+ | PatWildcard+ | PatApp Identifier [Pat]+ | PatBottom+ deriving Show++patToExpr :: Pat -> Maybe Expr+patToExpr (PatVar x) = Just $ Var x+patToExpr (PatCtor x) = Just $ Ctor x+patToExpr (PatLiteral l) = Just $ Literal l+patToExpr PatWildcard = Nothing+patToExpr (PatApp x ps) = do+ es <- mapM patToExpr ps+ Just $ foldl App (Ctor x) es+patToExpr PatBottom = Just Bottom++data ConstrDecl = ConstrDecl Identifier [Ty] deriving Show++$(derive [''Decl,''Expr,''Lit,''Pat,''Ty,''ConstrDecl,''Proof,''Formula])++--instance Alpha Program where+instance Alpha Decl where+instance Alpha Expr where+instance Alpha Ty where+instance Alpha Proof where+instance Alpha Formula where+instance Alpha Pat where+instance Alpha ConstrDecl where++-- Not sure why this is needed, but Unbound crashes with something about+-- "compareR1 does not support Integer1"+instance Alpha Lit where+ acompare' _ = compare++instance Subst Expr Expr where+ isvar (Var n) = Just (SubstName n)+ isvar _ = Nothing++instance Subst Expr Formula where+instance Subst Expr Ty where+instance Subst Expr Lit where+instance Subst Expr Pat where
+ Main.hs view
@@ -0,0 +1,50 @@+module Main where++import MProver.Parser as Parser+import MProver.Syntax++import MProver.Eval+import MProver.Checker+import MProver.REPL++import Control.Monad+import Control.Monad.Reader+import Control.Monad.Error+import Control.Monad.Identity++import qualified Data.Map++import System (getArgs)++import Unbound.LocallyNameless++test :: FilePath -> IO ()+test filename = do+ fileContents <- readFile filename++ let pResult = Parser.parse filename fileContents++ case pResult of+ (Left err) -> putStrLn $ "Parse error: " ++ show err+ (Right p@(Program _ _)) -> do+ let result = runFreshM $ runReaderT (runErrorT (checkProg p)) (Data.Map.empty,Data.Map.empty,Data.Map.empty,Data.Map.empty)+ case result of+ (Left err) -> do+ putStr "Error: "+ putStrLn err+ (Right ()) -> putStrLn "Succeeded."++testParse :: FilePath -> IO ()+testParse filename = do+ fileContents <- readFile filename+ print (Parser.parse filename fileContents)++dorepl :: IO ()+dorepl = runFreshMT (runReaderT (runErrorT repl) (Data.Map.empty,Data.Map.empty,Data.Map.empty,Data.Map.empty)) >> return ()++main :: IO ()+main = do+ args <- getArgs+ case args of+ (filename:_) -> test filename+ [] -> dorepl
+ README view
@@ -0,0 +1,45 @@+mprover-0.0.0.0+---------------++This is a highly preliminary release of MProver, a simple (I hope!) proof+checker for equational reasoning in (a subset of) Haskell. It is released+in the spirit, though not under the exact terms, of the CRAPL[1].++To build and install, use the standard incantation, viz.:++ $ runhaskell Setup.hs configure+ $ runhaskell Setup.hs build+ $ runhaskell Setup.hs install++To launch the REPL (note that loading modules for use in the REPL is not+supported yet, so you may find this a bit useless):++ $ mp++To run the proof checker against an example MProver script:++ $ mp examples/Test.hs++If you have any questions or comments, please write:++ Adam Procter <amp269@mail.missouri.edu>++In particular, I'd be glad to send you a draft copy of a conference paper,+currently under review, that outlines MProver's design.++Enjoy at your own risk!+++Bugs/Limitations+----------------++Some particular bugs/limitations/to-do items of note:++ * The guardedness check is not implemented yet.+ * Program terms are not type checked (!)+ * Type classes are not implemented yet.+ * Case-proofs must be exhaustive; this is not actually checked for yet.++---++[1] http://matt.might.net/articles/crapl/
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ examples/Test.hs view
@@ -0,0 +1,26 @@+module Test where++--+-- As a simple case, let's prove a theorem about lazy lists: namely, that+-- map (+1) zeros = ones (paraphrasing a bit, since we're technically talking+-- about Nats rather than Ints).+--+{ data List a = Nil | Cons a (List a)+; data Nat = Z | S Nat++; map :: (a -> b) -> List a -> List b+; map = \ f -> \ l -> case l of+ { Nil -> Nil+ ; (Cons x xs) -> Cons (f x) (map f xs)+ }++; ones = Cons (S Z) ones+; zeros = Cons Z zeros++; mapPlusOne ::: { map S zeros = ones }+; mapPlusOne = trans+ (eval ::: { map S zeros = Cons (S Z) (map S zeros) })+ (trans+ (Cons (eval ::: { S Z = S Z }) (mapPlusOne ::: { map S zeros = ones }))+ (eval ::: { Cons (S Z) ones = ones }))+}
+ mprover.cabal view
@@ -0,0 +1,20 @@+Name: mprover+Version: 0.0.0.0+Synopsis: Simple equational reasoning for a Haskell-ish language+License: BSD3+License-file: LICENSE+Author: Adam Procter and Aaron Stump+Maintainer: Adam Procter <amp269@mail.missouri.edu>+Build-Type: Simple+Cabal-Version: >= 1.6+Description: MProver is a proof checker for equational reasoning in a Haskell-like language.++ This is an extremely preliminary release, so don't expect it to be terribly useful just yet!+Category: Theorem Provers+Extra-Source-Files: README, examples/*.hs++Executable mp+ Main-is: Main.hs+ Build-Depends: base < 6, haskell98, containers >= 0.4.0.0, mtl >= 2.0.1.0, parsec >= 3.1.1, unbound >= 0.3.1, transformers >= 0.2.2.0, pretty >= 1.0.1.2+ Other-Modules: MProver.Checker, MProver.Eval, MProver.Monad, MProver.PPrint, MProver.Parser, MProver.REPL, MProver.Syntax+ ghc-prof-options: -rtsopts -auto-all