module alloy/paragraphs/CmdDecl
imports
  alloy/Names
  alloy/expressions/Block
  alloy/Lexical
exports
  sorts CmdDecl Expect TypeScope Scope

context-free syntax
  (Name ":")? Cmd (Name|Block) Scope  -> CmdDecl {cons("ACmdDecl")}

  "for"              {TypeScope ","}+ Expect? -> Scope {cons("AScope")}
                                 Expect? -> Scope {cons("AScope")}
  "for" Number "but" {TypeScope ","}+ Expect? -> Scope {cons("AScope")}

  "expect" "0" -> Expect {cons("AExpect0")}
  "expect" "1" -> Expect {cons("AExpect1")}


  "exactly" Number Name? -> TypeScope {cons("AExactCustomTypeScope")}
  Number Name -> TypeScope {cons("ACustomTypeScope")}
  "exactly" Number ("int"|"seq") -> TypeScope {cons("AExactTypeScope")}
  Number ("int"|"seq")? -> TypeScope {cons("ATypeScope")}