module Casl-BasicItems

%% written/changed by Bjarke Wedemeijer (January 1998)
%% adapted by Mark van den Brand (Juni 1999)
%% adapted by Mark van den Brand (November 2000)
%% adapted by Christian Maeder (January 2002)
%% adapted by Christian Maeder (February 2004)

imports Casl-Lexical
exports
  sorts
	Basic-Spec Sort-S Op-S Pred-S Op-Type Pred-Type

  lexical syntax
	"."|[\183] -> Dot	

  context-free syntax

%% Basic-Items section
    "{" "}"         -> Basic-Spec
    Ann Basic-Item+ -> Basic-Spec

    Sig-Items				             -> Basic-Item 
    "free" Data-Item                                 -> Basic-Item
    "generated" Data-Item                            -> Basic-Item 
    "generated" "{" Sig-Items+ "}" Opt-Semi          -> Basic-Item 
    Var-S {Var-Decl ";"}+ Opt-Semi                   -> Basic-Item
    "forall" {Var-Decl ";"}+ Ann Dot-Item	     -> Basic-Item 
    Dot Ann Formula Opt-Semi                         -> Basic-Item

    Dot Ann {Formula (Ann Dot)}+ Opt-Semi            -> Dot-Item 

%% old style
    Axiom-S Ann {Formula (";" Ann)}+ Opt-Semi        -> Basic-Item 

%% Sig-Items
    Sort-S Ann {Sort-Item (";" Ann)}+ Opt-Semi      -> Sig-Items
    Op-S   Ann {Op-Item   (";" Ann)}+ Opt-Semi      -> Sig-Items
    Pred-S Ann {Pred-Item (";" Ann)}+ Opt-Semi      -> Sig-Items
    Data-Item                                       -> Sig-Items

%% Data-Item (abbreviation)
    Datatype-S Ann {Datatype-Decl (";" Ann)}+ Opt-Semi  -> Data-Item

%% Sort-Item
    {Sort ","}+                               -> Sort-Item
    {Sort ","}+ "<" Sort                      -> Sort-Item
    Sort "=" "{" Var ":" Sort Dot Formula "}" -> Sort-Item
    Sort "=" {Sort "="}+                      -> Sort-Item

%% Op-Item 
    {Op-Name ","}+ ":" Op-Type                    -> Op-Item
    {Op-Name ","}+ ":" Op-Type "," {Op-Attr ","}+ -> Op-Item 
    Op-Name Op-Head "=" Term                      -> Op-Item

%% Op-Type
    Some-Sorts "->" Sort  -> Op-Type
    Sort                  -> Op-Type
    Some-Sorts "->?" Sort -> Op-Type
    "?" Sort              -> Op-Type

%% Sorts
    {Sort "*"|[\215]}+ -> Some-Sorts

%% Op-Attr
    "assoc"                 -> Op-Attr
    "comm"                  -> Op-Attr
    "idem"                  -> Op-Attr
    "unit" Term             -> Op-Attr

%% Op-Head
    "(" {Arg-Decl ";"}+ ")" ":" Sort     -> Op-Head
    ":" Sort                             -> Op-Head
    "(" {Arg-Decl ";"}+ ")" ":" "?" Sort -> Op-Head
    ":" "?" Sort                         -> Op-Head

%% Arg-Decl
    {Var ","}+ ":" Sort -> Arg-Decl

%% Pred-Item
    {Pred-Name ","}+ ":" Pred-Type    -> Pred-Item
    Pred-Name Pred-Head "<=>" Formula -> Pred-Item
    Pred-Name "<=>" Formula           -> Pred-Item

%% Pred-Type
    Some-Sorts -> Pred-Type
    "(" ")"    -> Pred-Type

%% Pred-Head
    "(" {Arg-Decl ";"}+ ")" -> Pred-Head

%% Datatype-Decl
    Sort "::=" Ann {Alternative ("|" Ann)}+  -> Datatype-Decl

%% Alternative
    Op-Name"(" {Component ";"}+ ")"     -> Alternative
    Op-Name"(" {Component ";"}+ ")" "?" -> Alternative
    Op-Name                             -> Alternative
    Sort-S {Sort ","}+                  -> Alternative

%% Component
    {Op-Name ","}+ ":" Sort     -> Component
    {Op-Name ","}+ ":" "?" Sort -> Component
    Sort                        -> Component

%% Var-Decl
    {Var ","}+  ":" Sort -> Var-Decl

%% Var-S
    "var" -> Var-S
    "vars" -> Var-S

%% Axiom-S
    "axiom"  -> Axiom-S
    "axioms" -> Axiom-S

%% Sort-S
    "sort"  -> Sort-S
    "sorts" -> Sort-S

%% Op-S
    "op"  -> Op-S
    "ops" -> Op-S

%% Pred-S
    "pred"  -> Pred-S
    "preds" -> Pred-S

%% Datatype-S
    "type"  -> Datatype-S
    "types" -> Datatype-S

%% Opt-Semi
    ";"? Ann               -> Opt-Semi

%% Formula
    Quantifier {Var-Decl ";"}+ Dot Formula -> Formula-Quant
    Formula-Quant -> Formula		

    Formula-2 "<=>" Formula-2             -> Formula-1
    Formula-2 "<=>" Formula-Quant         -> Formula-1
    Formula-2                             -> Formula-1
    Formula-1                             -> Formula

    Formula-3  "=>" Formula-3             -> Formula-2a
    Formula-3  "=>" Formula-2a            -> Formula-2a
    Formula-3  "=>" Formula-Quant         -> Formula-1
    Formula-3  "if" Formula-3             -> Formula-2b
    Formula-2b "if" Formula-3             -> Formula-2b
    Formula-2b "if" Formula-Quant         -> Formula-1
    Formula-3  "if" Formula-Quant         -> Formula-1
    Formula-2a                            -> Formula-2	
    Formula-2b                            -> Formula-2	
    Formula-3                             -> Formula-2

    Formula-4  "/\\" Formula-4            -> Formula-3a
    Formula-3a "/\\" Formula-4            -> Formula-3a
    Formula-3a "/\\" Formula-Quant        -> Formula-1
    Formula-3  "/\\" Formula-Quant        -> Formula-1
    Formula-4  "\\/" Formula-4            -> Formula-3b
    Formula-3b "\\/" Formula-4            -> Formula-3b
    Formula-3b "\\/" Formula-Quant        -> Formula-1
    Formula-4  "\\/" Formula-Quant        -> Formula-1
    Formula-4                             -> Formula-3			
    Formula-3a                            -> Formula-3
    Formula-3b                            -> Formula-3
								
    "not"|[\172] Formula-4     -> Formula-4
    "not"|[\172] Formula-Quant -> Formula-Quant
    "(" Formula ")"            -> Formula-5
    Formula-5                  -> Formula-4
    Atom                       -> Formula-5

    "true"                          -> Atom
    "false"                         -> Atom
    "def" Term                      -> Atom
    Term "=e="|"=" Term             -> Atom
    Term "in" Sort                  -> Atom
    Term                            -> Atom

%% Quantifier
    "forall"     -> Quantifier
    "exists"     -> Quantifier
    "exists" "!" -> Quantifier


%% Terms
    {Term ","}+ -> Terms

%% Term
    MixFix+     -> Term
    Term "when" Formula "else" Term     -> Term {right}

%% MixFix
    Token                               -> MixFix
    Literal				-> MixFix
    Place                               -> MixFix
    QualPredName                        -> MixFix
    QualVarName                         -> MixFix
    QualOpName                          -> MixFix
    MixFix ":"|"as" Sort                -> MixFix
    "(" Terms ")"                       -> MixFix
    "[" Terms? "]"                      -> MixFix
    "{" Terms? "}"                      -> MixFix

%% QualPredName 
    "(" "pred" Pred-Name ":" Pred-Type ")" -> QualPredName

%% QualVarName
    "(" "var" Var ":" Sort ")"          -> QualVarName

%% QualOpName
    "(" "op"  Op-Name ":" Op-Type ")"   -> QualOpName

%% Various small definitions
    Sort-Id   -> Sort

    Id        -> Op-Name

    Id        -> Pred-Name

    Simple-Id -> Var

  context-free priorities
    MixFix+     -> Term >
    Term "when" Formula "else" Term     -> Term