{

{-

Open Source Fixedpoint Model-Checker version 2009c

(C) Copyright IBM Corp. 2009
(C) Copyright ETH Zurich (Swiss Federal Institute of Technology) 2003,2007

All Rights Reserved.

-}

module NewIfParser where
import Char
import List
import NewIfLexer
}


%name parser
%tokentype {Token}

%token	    const		{TCONST _ $$}
	    var			{TVAR _ $$}
	    '('			{TOPENB _}
	    ')'			{TCLOSEB _}
            '['                 {TOPENSQB _}
            ']'                 {TCLOSESQB _}
	    ':'			{TCOLON _}
            '='                 {TEQ _}
	    ":="		{TDEF _}
	    "=>"		{TIMPL _}
            "(-)" {TPREVIOUS _}
	    '&'			{TAND _}
	    '.'			{TDOT _}
	    ','			{TCOMMA _}
            '*'                 {TSTAR _}
            '->'                {TARROW _}
            '/='                {TUNEQUAL _}
            exists              {TEXISTS _}
	    equ			{TEQUAL _}
	    less		{TLESS _}
	    not			{TNOT _}
	    step		{TSTEP _}
	    sect		{TSECTION _}
	    sectypes		{TSECTYPES _}
	    secsig		{TSECSIG _}
	    secprop		{TSECPROP _}
	    secinits		{TSECINITS _}
	    secrules		{TSECRULES _}
	    secgoals		{TSECGOALS _}
	    gol			{TGOAL _}
	    init		{TINIT _}
            property {TPROP _}
"[]" {TGLOBALLY _}
"/\\" {TCONJ _}
"\/" {TDISJ _}
'-' {TNEG _}
'~' {TNEG _}
"<->" {TBWEVENTUALLY _}
"[-]" {TBWGLOBALLY _}


%%



sections :: {PProt}
      : section					{[$1]}
      | section sections			{$1 : $2}

section :: {PSection}
       :  sect sectypes typedecs	{PTypeSec $3}
        | sect secsig sigdec            {PTypeSec $3}
	| sect secinits initials	{PInitSec $3}
        | sect secrules rulez		{PRuleSec $3}
	| sect secgoals goalz		{PGoalSec $3}
	| sect secprop propdec		{PTypeSec $3}

--------------- Section Properties -------------------


propdec :: {[PTypeDecl]}
         : prop				{[]}
         | prop propdec			{[]}

prop :: {[PTypeDecl]}
: property const ":=" "[]" backwardsLTL {[]}
| property const '(' vars ')' ":=" "[]" backwardsLTL {[]}

backwardsLTL :: {[PTypeDecl]}
: '(' backwardsLTL ')' {[]}
| term                 {[]}
| fact                 {[]}
| condition            {[]}
| backwardsLTL "/\\" backwardsLTL                 {[]}
| backwardsLTL "\/" backwardsLTL                 {[]}
| backwardsLTL "=>" backwardsLTL                 {[]}
| '-' backwardsLTL     {[]}
| '~' backwardsLTL     {[]}
| "<->" backwardsLTL   {[]}
| "[-]" backwardsLTL   {[]}
| "(-)" backwardsLTL   {[]}

--------------- Section Signature --------------------

sigdec::{[PTypeDecl]}
         : ftypedec				{[] --- ignore this bs.}
       | ftypedec sigdec			{[] --- ignore this bs.}

ftypedec::{PTypeDecl}
	: varcos ':' myftype			{Decl $3 $1}

myftype :: {PType}
	 : const '(' mytypes ')'		{Comp $1 $3}
	 | const				{Atomic $1}
         | mytype '*' myftype                   {$1}
         | mytype '->' mytype                   {$1}
         


--------------- Section Types ------------------------

typedecs::{[PTypeDecl]}
       : typedec				{[$1]}
       | typedec typedecs			{$1 : $2}

typedec::{PTypeDecl}
	: varcos ':' mytype			{Decl $3 $1}


mytype:: {PType}
	 : const '(' mytypes ')'		{Comp $1 $3}
	 | const				{Atomic $1}

mytypes::{[PType]}
	: mytype				{[$1]}
	| mytype ','  mytypes			{$1 : $3}



--------------- Section Init ------------------------

initials::{[(PIdent,PCNState)]}
	: initial				{[$1]}
	| initial initials			{$1 : $2}


initial::{(PIdent,PCNState)}
	: init const ":=" cnstate			{($2,$4)}


--------------- Section Rulez ------------------------

rulez::{[(PIdent,PRule)]}
	: rule					{[$1]}
	| rule rulez				{$1 : $2}

rule::{(PIdent,PRule)}
 : step const '(' vars ')' ":=" cnstate freshvar "=>" state  
						 {($2,($7,$10,$8))} 
 | step const  ":=" cnstate freshvar "=>" state  
						 {($2,($4,$7,$5))} 


freshvar::{[PSubst]}
	: {--empty--}				{[]}
	| '=' '[' exists substs ']'		{$4}


substs::{[PSubst]}
        : subst				{[$1]}
	| subst ',' substs              {$1 : $3}

subst::{PSubst}
     : var					{($1,Nothing)}
     | var ":=" term				{($1,Just $3)}


--------------- Section Goalz ------------------------


goalz::{[(PIdent, PCNState)]}
	: goal					{[$1]}
	| goal goalz				{$1 : $2}

goal::{(PIdent, PCNState)}
	: gol const '(' vars ')' ":=" cnstate	{($2,$7)}
	| gol const ":=" cnstate	{($2,$4)}


---------------- Facts, States, Conditions, etc  -----------------



cnstate::{PCNState}
--	: nstate conditions	                {($1 , $2)}
	: nstate  	                        {$1}

nstate::{(PNState,[PCondition])}
	:nfacts					{$1}
--        :nfacts negfacts                        {$1 ++ $2}

state::{PState}
       :facts					{$1}

nfact::{PNFact}
 	: fact					{Plain $1}
	| negfact			        {$1}

negfact::{PNFact}
          : not '(' fact ')'			{Not $3}
          | '~' '(' fact ')'			{Not $3}

--negfacts::{[PNFact]}
--          :{--empty--}                            {[]}
--	  | negfacts '&' negfact                  {$3 : $1}

nfacts::{([PNFact],[PCondition])}
        :{--empty--}                            {([],[])}
         |nfact					{([$1],[])}
         |nfact '.' nfacts			{($1 : fst $3,snd $3)}
         |nfact '&' nfacts			{($1 : fst $3,snd $3)}
         |nfact '&' conditions                  {([$1],$3)}


fact :: {PFact}
     : const '(' terms ')'			{($1, $3)}

facts::{[PFact]}
        :{--empty--}                            {[]}
        |fact					{[$1]}
	|fact '.' facts				{$1 : $3}

term :: {PTerm}
     :	const '(' terms ')'			{PCompT $1 $3}
     |	var					{PVar $1}
     |	const					{PConst $1}

terms :: {[PTerm]}
	 :term					{[$1]}
	 |term ',' terms			{$1 : $3}


conditions::{[PCondition]}
        : condition                             {[$1]}
        | condition '&' conditions		{$1 : $3}

--conditions::{[PCondition]}
--        : {--empty--}                         {[]}
--        | conditions '&' condition		{$3 : $1}

condition::{PCondition}
        : equ '(' term ',' term ')'		{PEq $3 $5}
        | var '=' term                          {PEq (PVar $1) $3}
        | var '/=' term                         {PNot (PEq (PVar $1) $3)}
	| less '(' term ',' term ')'		{PLess $3 $5}
	| not '(' condition ')'			{PNot $3}
	| '~' '(' condition ')'			{PNot $3}




--------------Contants, Variables, Lists of both--------------


vars::{[PIdent]}
	: var					{[$1]}
	| var ',' vars				{$1 : $3}


varcos::{[PIdent]}
         : var                          {[$1]}
	 | const                        {[$1]}
	 | var ',' varcos 		{$1 : $3}
	 | const ',' varcos		{$1 : $3}




---------------------------------------------
------- data for parsed expressions  --------
---------------------------------------------

{
happyError :: [Token] -> a
happyError tks = error ("Parse error at " ++ lcn ++ "\n" )
	where
	lcn = 	case tks of
		  [] -> "end of file"
		  tk:_ -> "line " ++ show l ++ ", column " ++ show c
			where
			AlexPn _ l c = token_posn tk


type PProt = [PSection]

data PSection= PTypeSec [PTypeDecl]
	      |PInitSec [(PIdent,PCNState)]  
	      |PRuleSec [(PIdent,PRule)]
              |PGoalSec [(PIdent,PCNState)]
              deriving (Eq,Show)

data PTypeDecl=Decl PType [PIdent]  
	    deriving (Eq,Show)

data PType=Atomic PIdent
	  |Comp PIdent [PType]
	    deriving (Eq,Show)

type PRule=(PCNState,PState,[PSubst])

type PState=[PFact]
type PNState=[PNFact]
type PCNState=(PNState,[PCondition])


---- Terms, Facts, NFacts & Conditions


data PTerm=  PConst PIdent
	     | PVar PIdent
	     | PCompT PIdent [PTerm]
	    deriving (Eq,Show)

type PFact=(PIdent,[PTerm])

type PSubst=(PIdent, Maybe PTerm)

data PNFact=Not PFact
	   |Plain PFact
	    deriving (Eq,Show)

data PCondition=PEq PTerm PTerm
	       |PLess PTerm PTerm
	       |PNot PCondition
	    deriving (Eq,Show)



 }
