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

Question

Я пытаюсь написать конкретный синтаксис для этой грамматики (из главы 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?

Answer 1

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

Обратите внимание на разницу: Intэто буквальный тип , как и Float. Все литералы имеют {s : Str}как их линкат в каждом конкретном синтаксисе, и вы не можете его никаким образом изменить. Поскольку линкат содержит Str( не <tcode id="4432571"></tcode>), сопоставление с шаблоном во время выполнения невозможно .

Представляем: тип параметра

Однако это тип параметра, поскольку он конечен. Возможно, вы видели в старых языках RGL, например, следующую финскую грамматику :

      -- from the Finnish resource grammar
oper
  NForms : Type = Predef.Ints 10 => Str ;

  nForms10 : (x1,_,_,_,_,_,_,_,_,x10 : Str) -> NForms =
    \ukko,ukon,ukkoa,ukkona,ukkoon,
       ukkojen,ukkoja,ukkoina,ukoissa,ukkoihin -> table {
    0 => ukko ;   1 => ukon ;    2 => ukkoa ;
    3 => ukkona ; 4 => ukkoon ;  5 => ukkojen ;
    6 => ukkoja ; 7 => ukkoina ; 8 => ukoissa ;
    9 => ukkoihin ; 10 => Ukko
    } ;

На мой взгляд, это довольно глупо; почему бы просто не назвать параметры как SgNom, SgGenи так далее, совершенно произвольно пытаться отладить этот код и помнить, что «5» - это родительный падеж множественного числа. Может быть, в старые времена уникальные названия параметров были предметом роскоши или чем-то в этом роде. :-P Если бы я писал этот код, я бы написал его так:

      -- another way to write the example from the Finnish RG
param
  NForm = SgNom | SgGen | ... | PlGen | PlIll ;
oper
  NForms : Type = NForm => Str ;

  nForms10 : (x1,_,_,_,_,_,_,_,_,x10 : Str) -> NForms =
    \ukko,ukon,ukkoa,ukkona,ukkoon,
       ukkojen,ukkoja,ukkoina,ukoissa,ukkoihin -> table {
    SgNom => ukko ; 
    SgGen => ukon ;
    ...
    PlGen => ukkojen ;
    PlIll => ukkoihin
    } ;

Как видите, целое число работает как левая часть списка: 5 => ukkojen является таким же допустимым GF, как PlGen => ukkojen. В этом конкретном случае 5 имеет тип Ints 10.

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

Мое (пока еще довольно неудовлетворительное) решение

Итак, вот мое решение, использующее для некоторого конечного n. Надеюсь, вы поймете, почему это неудовлетворительно.

      concrete ArithmConcrete of Arithm = open Predef, Prelude in {
  lincat
    Nat = {n : Ints 10} ;
  lin
    Zero = {n = 0} ;
    Succ x = {n = myPlus1 ! x.n} ;

  oper

    -- We can't use Predef.plus, but we can make our own!
    myPlus1 : Ints 10 => Ints 10 = table {
      0 => 1 ;
      1 => 2 ;
      2 => 3 ;
      3 => 4 ;
      4 => 5 ;
      5 => 6 ;
      6 => 7 ;
      7 => 8 ;
      8 => 9 ;
      _ => 10
      } ;
}

Как видно из myPlus1, определенно возможно сопоставление с образцом Ints nво время выполнения. К сожалению, он ограничен конечным числом n и писать очень утомительно.

Давайте проверим это в оболочке GF:

      $ gf
…

> i -retain ArithmConcrete.gf 

> cc Zero
{n = 0; lock_Nat = <>}

> cc Succ Zero
{n = 1; lock_Nat = <>}

> cc Succ (Succ (Succ (Succ (Succ Zero))))
{n = 5; lock_Nat = <>}

Технически работает, если можно так выразиться.

Другие решения

Вот решение от daherb , где Zero выводит строку "0" и Succ выводит строку "+1", а окончательный результат оценивается на внешнем языке программирования.