diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE diff --git a/MProver/Checker.hs b/MProver/Checker.hs new file mode 100644 --- /dev/null +++ b/MProver/Checker.hs @@ -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 diff --git a/MProver/Eval.hs b/MProver/Eval.hs new file mode 100644 --- /dev/null +++ b/MProver/Eval.hs @@ -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,[]) diff --git a/MProver/Monad.hs b/MProver/Monad.hs new file mode 100644 --- /dev/null +++ b/MProver/Monad.hs @@ -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 diff --git a/MProver/PPrint.hs b/MProver/PPrint.hs new file mode 100644 --- /dev/null +++ b/MProver/PPrint.hs @@ -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 diff --git a/MProver/Parser.hs b/MProver/Parser.hs new file mode 100644 --- /dev/null +++ b/MProver/Parser.hs @@ -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 "<>" 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 diff --git a/MProver/REPL.hs b/MProver/REPL.hs new file mode 100644 --- /dev/null +++ b/MProver/REPL.hs @@ -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 "" inp of + (Left err) -> liftIO $ print err + (Right e) -> do + e' <- evalCBN e + e'_ <- ppr e' + liftIO $ print e'_ + repl diff --git a/MProver/Syntax.hs b/MProver/Syntax.hs new file mode 100644 --- /dev/null +++ b/MProver/Syntax.hs @@ -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 diff --git a/Main.hs b/Main.hs new file mode 100644 --- /dev/null +++ b/Main.hs @@ -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 diff --git a/README b/README new file mode 100644 --- /dev/null +++ b/README @@ -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 + +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/ diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/examples/Test.hs b/examples/Test.hs new file mode 100644 --- /dev/null +++ b/examples/Test.hs @@ -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 })) +} diff --git a/mprover.cabal b/mprover.cabal new file mode 100644 --- /dev/null +++ b/mprover.cabal @@ -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 +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