Как реализовать типизированный интерпретатор без тегов? - PullRequest
Новая
       2

Как реализовать типизированный интерпретатор без тегов?

0 голосов
/ 03 октября 2018

[1] описывает очень интересный подход к определению синтаксиса и семантики языка.Идея состоит в том, чтобы использовать классы вместо ADT для описания синтаксиса: 

class ExpSYM =
  fixes lit :: "int ⇒ 'a"
    and neg :: "'a ⇒ 'a"
    and add :: "'a ⇒ 'a ⇒ 'a"

Семантика описывается с использованием создания экземпляра класса для некоторой области значений (int): 

instantiation int :: ExpSYM
begin
definition "lit_int (n :: int) ≡ n"
definition "neg_int (e :: int) ≡ -e"
definition "add_int (e1 :: int) (e2) ≡ e1 + e2"
instance ..
end

definition eval :: "int ⇒ int" where
  "eval ≡ id"

Вот несколько примеров: 

term "add (lit 1) (lit 2)"
term "eval (add (lit 1) (lit 2))"
value "eval (add (lit 1) (lit 2))"

Подход позволяет легко расширять язык: 

class MulSYM =
  fixes mul :: "'a ⇒ 'a ⇒ 'a"

instantiation int :: MulSYM
begin
definition "mul_int (e1 :: int) (e2) ≡ e1 * e2"
instance ..
end

term "eval (mul (add (lit 1) (lit 2)) (lit 5))"
value "eval (mul (add (lit 1) (lit 2)) (lit 5))"

Также подход позволяет определять семантику языка без тегов значений и сопоставления с образцом: 

datatype val = BoolVal bool | IntVal int | StringVal string

Проблема в том, что я не могу реализовать следующий пример Haskell из [2] в Изабель HOL: 

class Symantics repr where
    int :: Int → repr Int
    add :: repr Int → repr Int → repr Int
    lam :: (repr a → repr b) → repr (a → b)
    app :: repr (a → b) → repr a → repr b

Автор называет это s y mantics, потому что

объявление класса определяет синтаксис встроенного языка (его форм выражения);экземпляры класса определяют интерпретации или семантику.

repr - это параметр, представляющий экземпляр типа класса.Этот тип параметрический.Он может принимать Int в качестве параметра (repr Int) или стрелку типа (repr (a → b)).

Вот пример языковых выражений разных типов: 

th1 = add (int 1) (int 2)
−− th1 :: (Symantics repr) ⇒ repr Int
th2 = lam (\x → add x x)
−− th2 :: (Symantics repr) ⇒ repr (Int → Int)
th3 = lam (\x → add (app x (int 1)) (int 2))
−− th3 :: (Symantics repr) ⇒ repr ((Int → Int) → Int)

Вот переводчик языка: 

newtype R a = R{unR :: a}

instance Symantics R where
    int x = R x
    add e1 e2 = R $ unR e1 + unR e2
    lam f = R $ unR ◦ f ◦ R
    app e1 e2 = R $ (unR e1) (unR e2)

−− eval :: R a → a
eval e = unR e

Как реализовать аналогичный переводчик в Изабель HOL?Кажется, что классы и локали здесь не применимы.

Существует также похожий интерпретатор без тегов, основанный на обобщенных алгебраических типах данных в примечаниях к лекции [3]: 

data Exp env t where
    B :: Bool → Exp env Bool
    V :: Var env t → Exp env t
    L :: Exp (a,env) b → Exp env (a → b)
    A :: Exp env (a → b) → Exp env a → Exp env b

data Var env t where
    VZ :: Var (t, env) t
    VS :: Var env t → Var (a, env) t

eval :: env → Exp env t → t
eval env (V v) = lookp v env
eval env (B b) = b
eval env (L e) = \x → eval (x, env) e
eval env (A e1 e2) = (eval env e1) (eval env e2)

Не могли бы выподскажите, как реализовать эти два безметочных переводчика в Изабель Холь?

[1] Олег Киселев.Типизированные конечные переводчики без тегов

[2] - // -.Раздел 3.4. Окончательное вложение без тегов с абстрактным синтаксисом высшего порядка.Page 29

[3] - // -, раздел 3.2 Без тегов, начальные и конечные вложения.Страницы 22-23

...