%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Twelf Grammar Specification for LambdaYacc
% Created by Kamal Aboul-Hosn
%
% There are a few things that this grammar will
% not support that are in Twelf:
%
% - Mode declarations must have a space between
%   the "+", "-", or "*" and the variable name,e.g.,
%   %mode eval +E -V
%
% - Numbers can not be used as identifiers in defintions
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

sig twelf.
accum_sig lyaccshares,blists.

type infixt,prefixt,postfixt gs.
type nonet,leftt,rightt gs.
type namet,queryt,solvet,modet,terminatest,theoremt,provet, establisht, assertt, uset gs.
type percentt gs.
type rarrowt,larrowt,lbrace,rbrace,lbracket,rbracket,lparen,rparen gs.
type colon,period,comma,eqlt,typet,astrt,plust,minust gs.
type forallst,forallt,existst,truet gs.

% kinds
kind elfdef type.
kind adecl type.
kind aterm type.
kind fixtype type.
kind abound type.
kind atermin type.
kind atheorem type.
kind aprove type.
kind amode type.
kind modetype type.
kind aorder type.
kind acallpat type.
kind aarg type.
kind amform type.
kind quant type.
kind adec type.

% Types
type defelf (list adecl) -> gs.
type decls (list adecl) -> gs.
type sigdecl adecl -> gs.
type decl adecl -> gs.
type infn,infl,infr,pref,postf fixtype.
type term aterm -> gs.
type mode amode -> gs.
type termin atermin -> gs.
type order aorder -> gs.
type orders (list aorder) -> gs.
type marg aorder -> gs.
type idlist (list string) -> gs.
type callpats (list acallpat) -> gs.
type callpat acallpat -> gs.
type args (list aarg) -> gs.
type mform (list amform) -> gs.
type pprove aprove -> gs.
type thdecl atheorem -> gs.
type decs (list adec) -> gs.
type dec adec -> gs.
type bound abound -> gs.
type interm string -> gs.
type intermpi string -> aterm -> gs.
type telparen gs.

% Functions
type defterm string -> aterm -> aterm -> adecl.
type fixify fixtype -> int -> string -> adecl.
type defname string -> string -> adecl.
type defquery abound -> abound -> string -> aterm -> adecl.
type defsolve string -> aterm -> adecl.
type defmode amode -> adecl.
type defterminate atermin -> adecl.
type deftheorem atheorem -> adecl.
type defprove aprove -> adecl.
type defestablish aprove -> adecl.
type defassert (list acallpat) -> adecl.
type defuse string -> adecl.
type typeterm aterm.
type freevar string -> aterm.
type @ aterm -> aterm -> aterm.
infixl @ 9.
type imp aterm.
type asc aterm.
type holeterm aterm.
type forall string -> aterm -> aterm.
type starbound abound.
type ibound int -> abound.
type decmode string -> (list amode) -> amode.
type modelist (list amode) -> amode.
type inmode,outmode,bothmode  modetype.
type modearg modetype -> string -> aterm -> amode.
type noterm aterm.
type decfmode aterm -> amode -> amode.
type dectermin aorder -> (list acallpat) -> atermin.
type listorder (list aorder) -> aorder.
type makearg (list string) -> aorder.
type makecallpat string -> (list aarg) -> acallpat.
type strarg string -> aarg.
type provedec  int -> aorder -> (list acallpat) -> aprove.
type declth string -> (list amform) -> atheorem.
type forallstar,forallq,exists,trueform quant.
type mf quant -> (list adec) -> amform.
type declare string -> aterm -> adec.


type nonterminf int -> gs.
type nonterminfl int -> gs.
type nonterminfr int -> gs.
type nontermpre int -> gs.
type nontermpost int -> gs.
type nament string -> gs.
type stringnt string -> gs.
type termify (list string) -> aterm -> o.
type formlam string -> aterm -> aterm -> o.

type  abs  (string -> (aterm -> aterm) -> aterm).
type  copy  (aterm -> aterm -> o).
type  const  (aterm -> o).
type twelfpar o.