% This file was generated by 'rail' from 'ref.rai'
\rail@t {lbrace}
\rail@t {rbrace}
\rail@i {1}{ \par theoryDef : id '=' (name + '+') ('+' extension | ()) ; \par name: id | string ; \par extension : (section +) 'end' ( () | ml ) ; \par section : classes | default | types | arities | consts | syntax | trans | defs | constdefs | rules | axclass | instance | oracle ; \par classes : 'classes' ( classDecl + ) ; \par classDecl : (id (() | '<' (id + ','))) ; \par default : 'default' sort ; \par sort : id | lbrace (id * ',') rbrace ; \par types : 'types' ( ( typeDecl ( () | '(' infix ')' ) ) + ) ; \par infix : ( 'infixr' | 'infixl' ) nat ; \par typeDecl : typevarlist name ( () | '=' ( string | type ) ); \par typevarlist : () | tid | '(' ( tid + ',' ) ')'; \par type : simpleType | '(' type ')' | type '=>' type | '[' ( type + "," ) ']' '=>' type; \par simpleType: id | ( tid ( () | '::' id ) ) | '(' ( type + "," ) ')' id | simpleType id ; \par arities : 'arities' ((name + ',') '::' arity +) ; \par arity : ( () | '(' (sort + ',') ')' ) sort ; \par consts : 'consts' ( mixfixConstDecl + ) ; \par syntax : 'syntax' (() | mode) ( mixfixConstDecl + ); \par mode : '(' name (() | 'output') ')' ; \par mixfixConstDecl : constDecl (() | ( '(' mixfix ')' )) ; \par constDecl : ( name + ',') '::' (string | type); \par mixfix : string ( () | ( () | ('[' (nat + ',') ']')) nat ) | ( 'infixr' | 'infixl' ) (() | string) nat | 'binder' string nat ; \par trans : 'translations' ( pat ( '==' | '=>' | '<=' ) pat + ) ; \par pat : ( () | ( '(' id ')' ) ) string; \par rules : 'rules' (( id string ) + ) ; \par defs : 'defs' (( id string ) + ) ; \par constdefs : 'constdefs' (id '::' (string | type) string +) ; \par axclass : 'axclass' classDecl (() | ( id string ) +) ; \par instance : 'instance' ( name '<' name | name '::' arity) witness ; \par witness : (() | '(' ((string | longident) + ',') ')') (() | verbatim) ; \par oracle : 'oracle' name ; \par ml : 'ML' text ; \par }
\rail@o {1}{
\rail@begin{2}{theoryDef}
\rail@nont{id}[]
\rail@term{=}[]
\rail@plus
\rail@nont{name}[]
\rail@nextplus{1}
\rail@cterm{+}[]
\rail@endplus
\rail@bar
\rail@term{+}[]
\rail@nont{extension}[]
\rail@nextbar{1}
\rail@endbar
\rail@end
\rail@begin{2}{name}
\rail@bar
\rail@nont{id}[]
\rail@nextbar{1}
\rail@nont{string}[]
\rail@endbar
\rail@end
\rail@begin{2}{extension}
\rail@plus
\rail@nont{section}[]
\rail@nextplus{1}
\rail@endplus
\rail@term{end}[]
\rail@bar
\rail@nextbar{1}
\rail@nont{ml}[]
\rail@endbar
\rail@end
\rail@begin{13}{section}
\rail@bar
\rail@nont{classes}[]
\rail@nextbar{1}
\rail@nont{default}[]
\rail@nextbar{2}
\rail@nont{types}[]
\rail@nextbar{3}
\rail@nont{arities}[]
\rail@nextbar{4}
\rail@nont{consts}[]
\rail@nextbar{5}
\rail@nont{syntax}[]
\rail@nextbar{6}
\rail@nont{trans}[]
\rail@nextbar{7}
\rail@nont{defs}[]
\rail@nextbar{8}
\rail@nont{constdefs}[]
\rail@nextbar{9}
\rail@nont{rules}[]
\rail@nextbar{10}
\rail@nont{axclass}[]
\rail@nextbar{11}
\rail@nont{instance}[]
\rail@nextbar{12}
\rail@nont{oracle}[]
\rail@endbar
\rail@end
\rail@begin{2}{classes}
\rail@term{classes}[]
\rail@plus
\rail@nont{classDecl}[]
\rail@nextplus{1}
\rail@endplus
\rail@end
\rail@begin{3}{classDecl}
\rail@nont{id}[]
\rail@bar
\rail@nextbar{1}
\rail@term{<}[]
\rail@plus
\rail@nont{id}[]
\rail@nextplus{2}
\rail@cterm{,}[]
\rail@endplus
\rail@endbar
\rail@end
\rail@begin{1}{default}
\rail@term{default}[]
\rail@nont{sort}[]
\rail@end
\rail@begin{4}{sort}
\rail@bar
\rail@nont{id}[]
\rail@nextbar{1}
\rail@token{lbrace}[]
\rail@bar
\rail@nextbar{2}
\rail@plus
\rail@nont{id}[]
\rail@nextplus{3}
\rail@cterm{,}[]
\rail@endplus
\rail@endbar
\rail@token{rbrace}[]
\rail@endbar
\rail@end
\rail@begin{3}{types}
\rail@term{types}[]
\rail@plus
\rail@nont{typeDecl}[]
\rail@bar
\rail@nextbar{1}
\rail@term{(}[]
\rail@nont{infix}[]
\rail@term{)}[]
\rail@endbar
\rail@nextplus{2}
\rail@endplus
\rail@end
\rail@begin{2}{infix}
\rail@bar
\rail@term{infixr}[]
\rail@nextbar{1}
\rail@term{infixl}[]
\rail@endbar
\rail@nont{nat}[]
\rail@end
\rail@begin{3}{typeDecl}
\rail@nont{typevarlist}[]
\rail@nont{name}[]
\rail@bar
\rail@nextbar{1}
\rail@term{=}[]
\rail@bar
\rail@nont{string}[]
\rail@nextbar{2}
\rail@nont{type}[]
\rail@endbar
\rail@endbar
\rail@end
\rail@begin{4}{typevarlist}
\rail@bar
\rail@nextbar{1}
\rail@nont{tid}[]
\rail@nextbar{2}
\rail@term{(}[]
\rail@plus
\rail@nont{tid}[]
\rail@nextplus{3}
\rail@cterm{,}[]
\rail@endplus
\rail@term{)}[]
\rail@endbar
\rail@end
\rail@begin{5}{type}
\rail@bar
\rail@nont{simpleType}[]
\rail@nextbar{1}
\rail@term{(}[]
\rail@nont{type}[]
\rail@term{)}[]
\rail@nextbar{2}
\rail@nont{type}[]
\rail@term{=>}[]
\rail@nont{type}[]
\rail@nextbar{3}
\rail@term{[}[]
\rail@plus
\rail@nont{type}[]
\rail@nextplus{4}
\rail@cterm{,}[]
\rail@endplus
\rail@term{]}[]
\rail@term{=>}[]
\rail@nont{type}[]
\rail@endbar
\rail@end
\rail@begin{6}{simpleType}
\rail@bar
\rail@nont{id}[]
\rail@nextbar{1}
\rail@nont{tid}[]
\rail@bar
\rail@nextbar{2}
\rail@term{::}[]
\rail@nont{id}[]
\rail@endbar
\rail@nextbar{3}
\rail@term{(}[]
\rail@plus
\rail@nont{type}[]
\rail@nextplus{4}
\rail@cterm{,}[]
\rail@endplus
\rail@term{)}[]
\rail@nont{id}[]
\rail@nextbar{5}
\rail@nont{simpleType}[]
\rail@nont{id}[]
\rail@endbar
\rail@end
\rail@begin{3}{arities}
\rail@term{arities}[]
\rail@plus
\rail@plus
\rail@nont{name}[]
\rail@nextplus{1}
\rail@cterm{,}[]
\rail@endplus
\rail@term{::}[]
\rail@nont{arity}[]
\rail@nextplus{2}
\rail@endplus
\rail@end
\rail@begin{3}{arity}
\rail@bar
\rail@nextbar{1}
\rail@term{(}[]
\rail@plus
\rail@nont{sort}[]
\rail@nextplus{2}
\rail@cterm{,}[]
\rail@endplus
\rail@term{)}[]
\rail@endbar
\rail@nont{sort}[]
\rail@end
\rail@begin{2}{consts}
\rail@term{consts}[]
\rail@plus
\rail@nont{mixfixConstDecl}[]
\rail@nextplus{1}
\rail@endplus
\rail@end
\rail@begin{2}{syntax}
\rail@term{syntax}[]
\rail@bar
\rail@nextbar{1}
\rail@nont{mode}[]
\rail@endbar
\rail@plus
\rail@nont{mixfixConstDecl}[]
\rail@nextplus{1}
\rail@endplus
\rail@end
\rail@begin{2}{mode}
\rail@term{(}[]
\rail@nont{name}[]
\rail@bar
\rail@nextbar{1}
\rail@term{output}[]
\rail@endbar
\rail@term{)}[]
\rail@end
\rail@begin{2}{mixfixConstDecl}
\rail@nont{constDecl}[]
\rail@bar
\rail@nextbar{1}
\rail@term{(}[]
\rail@nont{mixfix}[]
\rail@term{)}[]
\rail@endbar
\rail@end
\rail@begin{2}{constDecl}
\rail@plus
\rail@nont{name}[]
\rail@nextplus{1}
\rail@cterm{,}[]
\rail@endplus
\rail@term{::}[]
\rail@bar
\rail@nont{string}[]
\rail@nextbar{1}
\rail@nont{type}[]
\rail@endbar
\rail@end
\rail@begin{7}{mixfix}
\rail@bar
\rail@nont{string}[]
\rail@bar
\rail@nextbar{1}
\rail@bar
\rail@nextbar{2}
\rail@term{[}[]
\rail@plus
\rail@nont{nat}[]
\rail@nextplus{3}
\rail@cterm{,}[]
\rail@endplus
\rail@term{]}[]
\rail@endbar
\rail@nont{nat}[]
\rail@endbar
\rail@nextbar{4}
\rail@bar
\rail@term{infixr}[]
\rail@nextbar{5}
\rail@term{infixl}[]
\rail@endbar
\rail@bar
\rail@nextbar{5}
\rail@nont{string}[]
\rail@endbar
\rail@nont{nat}[]
\rail@nextbar{6}
\rail@term{binder}[]
\rail@nont{string}[]
\rail@nont{nat}[]
\rail@endbar
\rail@end
\rail@begin{4}{trans}
\rail@term{translations}[]
\rail@plus
\rail@nont{pat}[]
\rail@bar
\rail@term{==}[]
\rail@nextbar{1}
\rail@term{=>}[]
\rail@nextbar{2}
\rail@term{<=}[]
\rail@endbar
\rail@nont{pat}[]
\rail@nextplus{3}
\rail@endplus
\rail@end
\rail@begin{2}{pat}
\rail@bar
\rail@nextbar{1}
\rail@term{(}[]
\rail@nont{id}[]
\rail@term{)}[]
\rail@endbar
\rail@nont{string}[]
\rail@end
\rail@begin{2}{rules}
\rail@term{rules}[]
\rail@plus
\rail@nont{id}[]
\rail@nont{string}[]
\rail@nextplus{1}
\rail@endplus
\rail@end
\rail@begin{2}{defs}
\rail@term{defs}[]
\rail@plus
\rail@nont{id}[]
\rail@nont{string}[]
\rail@nextplus{1}
\rail@endplus
\rail@end
\rail@begin{3}{constdefs}
\rail@term{constdefs}[]
\rail@plus
\rail@nont{id}[]
\rail@term{::}[]
\rail@bar
\rail@nont{string}[]
\rail@nextbar{1}
\rail@nont{type}[]
\rail@endbar
\rail@nont{string}[]
\rail@nextplus{2}
\rail@endplus
\rail@end
\rail@begin{3}{axclass}
\rail@term{axclass}[]
\rail@nont{classDecl}[]
\rail@bar
\rail@nextbar{1}
\rail@plus
\rail@nont{id}[]
\rail@nont{string}[]
\rail@nextplus{2}
\rail@endplus
\rail@endbar
\rail@end
\rail@begin{2}{instance}
\rail@term{instance}[]
\rail@bar
\rail@nont{name}[]
\rail@term{<}[]
\rail@nont{name}[]
\rail@nextbar{1}
\rail@nont{name}[]
\rail@term{::}[]
\rail@nont{arity}[]
\rail@endbar
\rail@nont{witness}[]
\rail@end
\rail@begin{4}{witness}
\rail@bar
\rail@nextbar{1}
\rail@term{(}[]
\rail@plus
\rail@bar
\rail@nont{string}[]
\rail@nextbar{2}
\rail@nont{longident}[]
\rail@endbar
\rail@nextplus{3}
\rail@cterm{,}[]
\rail@endplus
\rail@term{)}[]
\rail@endbar
\rail@bar
\rail@nextbar{1}
\rail@nont{verbatim}[]
\rail@endbar
\rail@end
\rail@begin{1}{oracle}
\rail@term{oracle}[]
\rail@nont{name}[]
\rail@end
\rail@begin{1}{ml}
\rail@term{ML}[]
\rail@nont{text}[]
\rail@end
}