File size: 2,053 Bytes
56de343 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 | module Language.Elaborator (elaborate, ElabError(..)) where
import Language.AST
import qualified IR.Boolean as B
import qualified Data.Map.Strict as Map
data ElabError
= UnboundVariable String
| UndefinedFunction String
| ArityMismatch String Int Int
deriving (Show)
type Env = Map.Map String ([String], Expr)
elaborate :: Module -> Either ElabError [B.Circuit]
elaborate (Module _ stmts) = do
let env = buildEnv stmts
mapM (elabStmt env) (filter isVerifiable stmts)
buildEnv :: [Stmt] -> Env
buildEnv = foldl addDef Map.empty
where
addDef env (SDef (Ident name) params body) =
Map.insert name (map identName params, body) env
addDef env _ = env
isVerifiable :: Stmt -> Bool
isVerifiable (SAssert _) = True
isVerifiable (SProve _ _) = True
isVerifiable _ = False
elabStmt :: Env -> Stmt -> Either ElabError B.Circuit
elabStmt env (SAssert expr) = do
bexpr <- elabExpr env Map.empty expr
Right (B.Circuit "assert" [] bexpr)
elabStmt env (SProve (Ident name) expr) = do
bexpr <- elabExpr env Map.empty expr
Right (B.Circuit name [] bexpr)
elabStmt _ _ = Right (B.Circuit "_skip" [] B.BTrue)
elabExpr :: Env -> Map.Map String B.BExpr -> Expr -> Either ElabError B.BExpr
elabExpr _ locals (EVar (Ident v)) =
case Map.lookup v locals of
Just bv -> Right bv
Nothing -> Left (UnboundVariable v)
elabExpr _ _ (ELit True) = Right B.BTrue
elabExpr _ _ (ELit False) = Right B.BFalse
elabExpr env locals (ENand l r) = do
bl <- elabExpr env locals l
br <- elabExpr env locals r
Right (B.BNand bl br)
elabExpr env locals (EApp (Ident fname) args) =
case Map.lookup fname env of
Nothing -> Left (UndefinedFunction fname)
Just (params, body) -> do
if length params /= length args
then Left (ArityMismatch fname (length params) (length args))
else do
bargs <- mapM (elabExpr env locals) args
let newLocals = Map.union (Map.fromList (zip params bargs)) locals
elabExpr env newLocals body
|