Написание программы на Haskell для программ проверки типов, написанных на императивном языке программирования
Я пытаюсь написать программу на Хаскелле для проверки типов программ, написанных на обязательном языке программирования.
Вот абстрактный синтаксис:
type Name = String
- программа - это серия (список) объявлений переменных и серия (список) операторов.
type Prog = ([TypeEnv],[Stmt])
- объявление переменной является типом и именем переменной
type TypeEnv = (Type,Name)
- типом является либо "int", либо "bool", либо "int[]..[]" или "bool [].. []"
data Type = BaseType BT | ArrayType BT Int deriving Show
data BT = TyInt | TyBool deriving Show
- заявление либо...
data Stmt =
Assign Name Exp -- ...assignment (<name> := <exp>;)
| If Exp [Stmt] [Stmt] -- ...if-then-else (if <bexp> { <stmt>* } else { <stmt>* })
| While Exp [Stmt] -- ...a while-loop (while <bexp> { <stmt>*> })
| Let Name Exp [Stmt] -- ...let bindings (let <name>=<exp> in { <stmt> *})
| LetArray Name [Exp] Exp [Stmt] -- ...let-array binding (letarray <name> [ <exp> ] .. [ <exp> ] := <exp> in { <stmt>* })
| Case Exp [(Int,[Stmt])] -- ...a case statements
| For Name Exp Exp [Stmt] -- ...a for-loop
| ArrayAssign Name [Exp] Exp -- ...or array assignment (<name> [ <exp> ] .. [ <exp> ] := <exp>;)
deriving Show
- выражение либо...
data Exp =
Add Exp Exp -- ...addition (<exp> + <exp>)
| Sub Exp Exp -- ...subtract (<exp> - <exp>)
| Mul Exp Exp -- ...multiplication (<exp> * <exp>)
| Neg Exp -- ...negation (-<exp>)
| Var Name -- ...a variable (<name>)
| LitInt Int -- ...an integer literal (e.g. 3, 0, 42, 1999)
| VarArray Name [Exp] -- ...or an array lookup (<name> [ <exp> ])
| IsEq Exp Exp -- ...test for equality (<exp> == <exp>)
| IsNEq Exp Exp -- ...test for inequality (<exp> != <exp>)
| IsGT Exp Exp -- ...test for greater-than (<exp> > <exp>)
| IsLT Exp Exp -- ...test for less-than (<exp> < <exp>)
| IsGTE Exp Exp -- ...test for greater-or-equal (<exp> >= <exp>)
| IsLTE Exp Exp -- ...test for less-or-equal (<exp> <= <exp>)
| And Exp Exp -- ...boolean and (<bexp> && <bexp>)
| Or Exp Exp -- ...boolean or (<bexp> || <bexp>)
| Not Exp -- ...boolean negation (!<bexp>)
| LitBool Bool -- ... or a boolean literal (true or false)
deriving Show
Мне не нужен кто-то, чтобы полностью ответить на мой вопрос, но я хотел бы предоставить то, что у меня есть, и если кто-то может указать мне правильное направление или сообщить мне, если я делаю это совершенно неправильно, это было бы очень полезно,
Функция проверки типа программы начинается с проверки типа. typecheck использует typecheckstmt для проверки типов первого оператора и typecheckstmtlist для проверки типов остальной части программы. Затем эти функции используют typecheckexp для проверки типов любых выражений. Очевидно, у меня есть очень простой каркас реализации. Я просто хочу знать, двигаюсь ли я в правильном направлении, и есть ли у кого-нибудь указатели.
typecheck :: Prog -> Bool
typecheck _ = True
typecheck (types, x: xs) = (typecheckstmt types x) && (typecheckstmtlist types xs)
typecheckstmt :: [TypeEnv] -> Stmt -> Bool
typecheckstmt _ _ = True
typecheckstmt types (Assign x e) = if checkequaltypes x e
then True && typecheckexp types e
else False
typecheckstmt types (If e stmtlst1 stmtlst2) = typecheckexp types e
&& typecheckstmtlist types stmtlst1
&& typecheckstmtlist types stmtlst2
typecheckstmt types (While e stmtlst) = typecheckexp types e
&& typecheckstmtlist types stmtlst
typecheckstmt types (Let x e stmtlst) = if checkequaltype types x e
then True && typecheckexp types e
&& typecheckstmtlist types stmtlst
else False
typecheckstmt types (LetArray x es e2 stmtlst) =
typecheckstmt types (Case e cases) =
typecheckstmt types (For x e1 e2 stmtlst) = if checkequaltype types x e1
&& checkequaltype types x e2
then True && typecheckstmtlist stmtlst
else False
typecheckstmt types (ArrayAssign x es e2) =
typecheckstmtlist :: [TypeEnv] -> [Stmt] -> Bool
typecheckstmtlist _ _ = True
typecheckstmtlist types [x] = typecheckstmt types x
typecheckstmtlist types x:xs = typecheckstmt types x && typecheckstmtlist types xs
typecheckexp :: [TypeEnv] -> Exp -> Bool
typecheckexp types (Add e1 e2) =
typecheckexp types (Sub e1 e2) =
typecheckexp types (Mul e1 e2) =
typecheckexp types (Neg e1) =
typecheckexp types (Var x) =
typecheckexp types (LitInt i) =
typecheckexp types (VarArray x explist) =
typecheckexp types (IsEq e1 e2) =
typecheckexp types (IsNEq e1 e2) =
typecheckexp types (IsGT e1 e2) =
typecheckexp types (IsLT e1 e2) =
typecheckexp types (IsGTE e1 e2) =
typecheckexp types (IsLTE e1 e2) =
typecheckexp types (And e1 e2) =
typecheckexp types (Or e1 e2) =
typecheckexp types (Not e) =
typecheckexp types (LitBool Bool) =
typecheckexplist :: [TypeEnv] -> [Exp] -> Bool
typecheckexplist _ _ = True
typecheckexplist types [x] = typecheckexp types x
typecheckexplist types x:xs = typecheckexp types x && typecheckexplist types xs
checkequaltype :: [TypeEnv] -> Name -> Exp -> Bool
checkequaltype types x e = getTypeOfVar types x && getTypeOfExp types e
getTypeOfVar :: [TypeEnv] -> Name -> Type
getTypeOfExp :: [TypeEnv] -> Exp -> Type
Я также немного неясен относительно того, что нужно проверять. Очевидно, что если вы назначаете и сравниваете переменные / выражения, вы хотите, чтобы они были одного типа.
Любая помощь приветствуется.
1 ответ
Поскольку конкретного вопроса нет, я просто предложу несколько общих советов по этой проблеме.
Похоже, вы на правильном пути. Ваш подход верен, вам нужно пройтись по синтаксическому дереву и проверить каждое подвыражение, если ваши типы не совпадают.
typecheckexp :: [TypeEnv] -> Exp -> Bool
typecheckexp types (Add e1 e2) =
case (te1, te2) of
(Just TyInt, Just TyInt) -> True
_ -> False
where
te1 = getTypeOfExp e1
te2 = getTypeOfExp e2
На верхнем уровне вы примените проверку уровня выражения ко всем выражениям, а затем and все результаты вместе, чтобы получить, проверяет ли ваша программа в целом.
typecheckexplist :: [TypeEnv] -> [Exp] -> Bool
typecheckexplist env stmts = and (map (typecheckexp env) stmts)
Если все ваши типы объявлены заранее, а TypeEnv не изменен в результате перемещения по AST, тогда этот подход будет работать. Если вы создаете определения, проходя по дереву, подумайте о том, чтобы обернуть своего проверщика типов в монаду State.
Очевидно, что если вы назначаете и сравниваете переменные / выражения,
В зависимости от вашего языка интерфейса вам нужно решить, добавлять ли явные объявления типов (т.е. int a) для переменных или попытаться вывести их из контекста программы, что является отдельной задачей, называемой выводом типа. Если у вас есть явные объявления от пользователя, вы можете просто механически проверить данные типы на предмет использования переменной и определить, соответствуют ли они. Ваши типы все простые монотипии, так что это легко, как вы можете прикрепить (derving Eq) на ваш Type и получите сравнение типов.
Еще один случай, который следует рассмотреть, - это сообщение об ошибке, поскольку в заданном вами AST нет прикрепленной информации о положении, поэтому, если вы пройдете по дереву и потерпите неудачу на полпути, у вас не будет возможности сообщить пользователю, что и где не удалось. Если вы анализируете язык интерфейса из парсера, такого как Parsec, вы можете пометить каждый тип данных (Expr Pos) с информацией при построении синтаксического дерева.
data Expr t = Add t (Expr t) (Expr t) | ...
data Pos = Pos { line :: Integer , col :: Integer }
Для простоты использования вы можете заглянуть в универсальную библиотеку, такую как Uniplate, которая позволит вам применять функции и обходить AST без лишних шаблонов. Придуманный пример для извлечения всех узлов определенного типа может быть:
{-# LANGUAGE DeriveDataTypeable #-}
module Expr where
import Data.Data
import Data.Typeable
import Data.Generics.Uniplate.Data
data Expr = Val String
| Add Expr Expr
| Sub Expr Expr
| Div Expr Expr
| Mul Expr Expr
| Neg Expr
deriving (Show, Eq, Data, Typeable)
vars :: Expr -> [String]
vars ex = [i | Val i <- universe ex]
test :: [String]
test = vars (Add (Val "a") (Mul (Val "b") (Val "c")))