Грамматическая структура: «поле типа линеаризации не может быть Int»;Как написать конкретный синтаксис для грамматики с арифметическими выражениями? - PullRequest
Новая
       36

Грамматическая структура: «поле типа линеаризации не может быть Int»;Как написать конкретный синтаксис для грамматики с арифметическими выражениями?

1 голос
/ 27 апреля 2019

Я пытаюсь написать конкретный синтаксис для этой грамматики (из главы 6 в Грамматическая структура: программирование с многоязычными грамматиками ): 

abstract Arithm = {
  flags startcat = Prop ;
  cat
    Prop ;                        -- proposition
    Nat ;                         -- natural number
  fun
    Zero : Nat ;                  -- 0
    Succ : Nat -> Nat ;           -- the successor of x
    Even : Nat -> Prop ;          -- x is even
    And  : Prop -> Prop -> Prop ; -- A and B
}

Существуют предопределенные категории для целочисленных, плавающих и строковых литералов (Int, Float и String), и они могут быть использованы в качестве аргументов для функций , но они могут не иметь значения типы любой функции.

Кроме того, они не могут использоваться в качестве поля в типе линеаризации. Это то, что я хотел бы сделать, используя plus , определенный в Predef.gf : 

concrete ArithmEng of Arithm =
  open Predef, SymbolicEng, SyntaxEng, ParadigmsEng in
  lincat
    Prop = S ;
    Nat  = {s : NP ; n : Int} ;
  lin
    Zero     = mkNat 0 ;
    Succ nat = let n' : Int = Predef.plus nat.n 1 in mkNat n' ;
    Even nat = mkS (mkCl nat.s (mkA "even")) ;
    And p q  = mkS and_Conj p q ;
  oper
    mkNat  : Int -> Nat ;
    mkNat int = lin Nat {s = symb int ; n = int} ;
} ;

Но, конечно, это не работает: я получаю ошибку "поле типа линеаризации не может быть Int".

Возможно, правильный ответ на мой вопрос - использовать другой язык программирования, но мне любопытно, потому что этот пример оставлен в качестве упражнения для читателя в книге GF, поэтому я ожидаю, что он будет решаем.

Я могу написать унарное решение, используя категорию Digits из Numeral.gf: 

concrete ArithmEng of Arithm =
  open SyntaxEng, ParadigmsEng, NumeralEng, SymbolicEng, Prelude in {
  lincat
    Prop = S ;
    Nat = {s : NP ; d : Digits ; isZero : Bool} ;
  lin
    Zero = {s = mkNP (mkN "zero") ; d = IDig D_0 ; isZero = True} ;
    Succ nat = case nat.isZero of {
                 True  => mkNat (IDig D_1) ;
                 False => mkNat (IIDig D_1 nat.d) } ;
    Even nat = mkS (mkCl nat.s (mkA "even")) ;
    And p q  = mkS and_Conj p q ;
  oper
    mkNat : Digits -> Nat ;
    mkNat digs = lin Nat {s = symb (mkN "number") digs ; d = digs ; isZero = False} ;
} ;

Это дает следующие результаты: 

Arithm> l -bind Even Zero
zero is even

0 msec
Arithm> l -bind Even (Succ Zero)
number 1 is even

0 msec
Arithm> l -bind Even (Succ (Succ (Succ Zero)))
number 111 is even

Это, конечно, возможный ответ, но я подозреваю, что это было не так, как было задумано упражнение. Интересно, я что-то упускаю или язык GF раньше поддерживал больше операций над Ints?

...