package gen;
import edu.neu.ccs.demeterf.lib.*;
import edu.neu.ccs.demeterf.*;

nogen List(X) = Cons(X) | Empty(X).
nogen Cons(X) = <first> X <rest> List(X).
nogen Empty(X) = .

nogen Option(X)= Some(X) | None(X).
nogen Some(X) = <just> X.
nogen None(X) = .

// The logic of the Scientific Community Game
TestClaim = <claims> List(Claim) EOF.

Claim = SimpleClaim | CompoundClaim <args> Option(Args).
// Alice claims

SimpleClaim = <cn> ClaimName.
// whether Bob refutes, defends, strengthens or agrees
// is determined by a protocol based on refutation.

ClaimName = <v> ident.
// SimpleClaim  = <d> Domain <is> InstanceSet <rp> RefutationProtocol <q> Quality <c> Confidence.
CompoundClaim = AndClaim | OrClaim | ImplicationClaim |
  NegatedClaim | ForAllClaim | ExistsClaim.

AndClaim = "(and" <c1> Claim <c2> Claim ")".
// if Bob refutes c1 or Bob refutes c2, he refutes (and c1 c2)
//   in the dialog, Bob chooses one of c1 and c2 and refutes it
// if Alice defends c1 and Ailce defends c2, Alice defends (and c1 c2)
// if Bob strengthens c1 or Bob strengthens c2, he strengthens (and c1 c2)
// if Bob agrees with c1 and Bob agrees with c2, he agrees with (and c1 c2)

// if Alice proposes a logical conjunction and Bob decides
// to refute, he chooses either c1 (left) or c2 (right) to refute.

// Bob refutes c1
// --------------
// Bob refutes c1 and c2

// Bob refutes c1
// --------------
// Bob refutes c1 and c2
OrClaim = "(or" <c1> Claim <c2> Claim ")".
// if Bob refutes c1 and Bob refutes c2, he refutes (or c1 c2)
// if Bob defends c1 or Bob defends c2, he defends (or c1 c2)
// if Bob strengthens c1 and Bob strengthens c2, he strengthens (or c1 c2)
// if Bob agrees with c1 or Bob agrees with c2, he agrees with (or c1 c2)

// If Alice proposes a logical disjunction, Bob may refute it
// by stating ?. Alice defends it by choosing either c1 or c2
// to defend.

ImplicationClaim = "(->" <premise> Claim <consequent> Claim ")".
// if Bob defends premise and refutes !consequent, he refutes (premise -> consequent) 
// if Bob defends premise and Alice defends consequent, Alice defends (premise -> consequent)

NegatedClaim = "(not" <c1> Claim ")".
// if Bob refutes (not c1), he defends c1.
// if Bob defends c1, he refutes (not c1)

ForAllClaim = "(ForAll" <var> Variable "in" <d> VarDomain
 <c> Claim ")".
// if Bob provides a d so that Alice refutes c(d), Bob refutes (ForAll ...)
// if Bob provides a d so that Alice defends c(d), Alice defends (ForAll ...)
// if Alice strengthens c to c' and Bob provides a d' so that Alice defends c'(d'),
//    Alice strengthens (ForAll ... c ...) to (ForAll ... c' ...) 

ExistsClaim = "(Exists" <var> Variable "in" <d> VarDomain
 <c> Claim ")".
// if Alice provides a d so that Bob refutes c(d), Bob refutes (Exists ...)
// if Alice provides a d so that Bob defends c(d), Alice defends (Exists ...)

Variable = <v> ident.
VarDomain = Instance | Solution.
Instance = "instance".
Solution = "solution".
Predicate = <pn> PredicateName "(" <args> List(Variable) ")".
Args = "(" <args> List(Variable) ")".
PredicateName = <v> ident.