abt.grm

open AbbotSyntax
open Util

%%

%term EOF | SORT | ABT | EQUAL | BAR | LPAREN | RPAREN | COMMA | SYMBOL | DOT | STAR | TICK | OF | BINDING
    | Name of string

%nonterm start
         of string list StringTable.table
         * StringTable.Set.set
         * (string list * AbbotSyntax.oper list) StringTable.table
         * AbbotSyntax.oper list StringTable.table
       | decls
         of string list StringTable.table
         * StringTable.Set.set
         * (string list * AbbotSyntax.oper list) StringTable.table
         * AbbotSyntax.oper list StringTable.table
       | decl of (string * string list,
                  string,
                  string * (string list * AbbotSyntax.oper list),
                  string * AbbotSyntax.oper list)
                  Util.Sum4.t
       | symbol_decl of string
       | abt_decl of string * (string list * AbbotSyntax.oper list option)
       | abt_arg of string list
       | abt_args of string list
       | sort_decl of string * AbbotSyntax.oper list
       | cases of AbbotSyntax.oper list
       | oper of AbbotSyntax.oper
       | arity of AbbotSyntax.arity
       | simple_arity of AbbotSyntax.arity
       | aritys of AbbotSyntax.arity list
       | prod_arity of AbbotSyntax.arity list

%nonassoc COMMA
%nonassoc STAR
%right DOT
%left Name

%verbose
%pos int
%start start
%eop EOF
%noshift EOF
%name Abt

%%

start: decls (decls)

decls: (* empty *) ((StringTable.empty (), StringTable.Set.empty (), StringTable.empty (), StringTable.empty ()))
     | decl decls (let
                    val (exts, symbs, abts, sorts) = decls
                  in
                    case decl of
                        Sum4.In1 ext =>
                        (StringTable.insert
                           (fn _ => raise Fail "Duplicate abt defined.")
                           ext exts,
                        symbs,
                        abts,
                        sorts)
                      | Sum4.In2 symb =>
                        (exts, StringTable.Set.insert symb symbs, abts, sorts)
                      | Sum4.In3 abt =>
                        (exts,
                         symbs,
                         StringTable.insert
                           (fn _ => raise Fail "Duplicate abt defined.")
                           abt abts,
                         sorts)
                      | Sum4.In4 sort =>
                        (exts,
                         symbs,
                         abts,
                         StringTable.insert
                           (fn _ => raise Fail "Duplicate sort defined.")
                           sort sorts)
                  end)

decl: symbol_decl (Sum4.In2 symbol_decl)
    | abt_decl (case abt_decl of
                    (abt, (args, NONE)) => Sum4.In1 (abt, args)
                  | (abt, (args, SOME opers)) => Sum4.In3 (abt, (args, opers)))
    | sort_decl (Sum4.In4 sort_decl)

symbol_decl: SYMBOL Name (Name)

abt_decl: ABT abt_arg Name ((Name, (abt_arg, NONE)))
        | ABT abt_arg Name EQUAL cases ((Name, (abt_arg, SOME cases)))
        | ABT abt_arg Name EQUAL BAR cases ((Name, (abt_arg, SOME cases)))

abt_arg: (* empty *) ([])
       | TICK Name ([Name])
       | LPAREN abt_args RPAREN (abt_args)

abt_args: TICK Name ([Name])
        | TICK Name COMMA abt_args (Name :: abt_args)

sort_decl: SORT Name EQUAL cases ((Name, cases))
         | SORT Name EQUAL BAR cases ((Name, cases))

cases: oper ([oper])
     | oper BAR cases (oper :: cases)

oper: Name ((Name, NONE))
    | Name OF arity ((Name, SOME arity))

arity: simple_arity (simple_arity)
     | prod_arity (Prod prod_arity)
     | arity DOT arity (Dot (arity1, arity2))

simple_arity: Name (Use Name)
            | TICK Name (Param Name)
            | Name BINDING (Binding Name)
            | simple_arity Name (App (Name, [simple_arity]))
            | LPAREN aritys RPAREN Name (App (Name, aritys))
            | LPAREN arity RPAREN (arity)

aritys: arity COMMA arity ([arity1, arity2])
      | arity COMMA aritys (arity :: aritys)

prod_arity: simple_arity STAR simple_arity ([simple_arity1, simple_arity2])
          | simple_arity STAR prod_arity (simple_arity :: prod_arity)