type Program(pos: Meta, declarations: Declaration[])

type Metadata(doc: string[])

type Declaration =
  | ForeignType(pos: Meta, cmeta: Metadata, name: Name, target: Namespace)
  | Relation(pos: Meta, cmeta: Metadata, signature: Signature<RelationPart>)
  | Do(pos: Meta, body: Statement[])
  | Command(pos: Meta, cmeta: Metadata, signature: Signature<Parameter>, contract: Contract, body: Statement[], ttest: TrailingTest?)
  | Define(pos: Meta, cmeta: Metadata, name: Name, value: Expression)  // requires atomicity
  | AbstractType(pos: Meta, cmeta: Metadata, typ: TypeDef)
  | EnumType(pos: Meta, cmeta: Metadata, name: Name, variants: Name[])
  | SingletonType(pos: Meta, cmeta: Metadata, typ: TypeDef, init: TypeInit[])
  | Type(pos: Meta, cmeta: Metadata, typ: TypeDef, fields: TypeField[])
  | Trait(pos: Meta, cmeta: Metadata, name: Name)
  | ImplementTrait(pos: Meta, typ: TypeApp, trait: Trait)
  | Action( pos: Meta
          , cmeta: Metadata
          , self: Parameter
          , name: Name
          , title: Expression?
          , pred: Predicate
          , rank: Rank
          , body: Statement[]
          , commands: TypeInit[])
  | When(pos: Meta, cmeta: Metadata, pred: Predicate, body: Statement[])
  | Context(pos: Meta, cmeta: Metadata, name: Name, items: Declaration[])
  | Open(pos: Meta, ns: Namespace)
  | Local(pos: Meta, decl: Declaration)
  | Test(pos: Meta, title: String, body: Statement[])
  | Effect(pos: Meta, cmeta: Metadata, name: Name, cases: EffectCase[])
  | Capability(pos: Meta, cmeta: Metadata, name: Name)
  | Protect(pos: Meta, capability: Name, entity: ProtectEntity)

type ProtectEntity =
  | Type(pos: Meta, name: Name)
  | Trait(pos: Meta, name: Name)
  | Effect(pos: Meta, name: Name)
  | Definition(pos: Meta, name: Name)

type EffectCase(pos: Meta, cmeta: Metadata, name: Name, params: Parameter[])

type Handler(pos: Meta, name: Name, variant: Name, args: Name[], body: Statement[])

type TrailingTest(pos: Meta, body: Statement[])

type Contract(pos: Meta, ret: TypeConstraint?, pre: ContractCondition[], post: ContractCondition[])
type ContractCondition(pos: Meta, name: Name, expr: Expression)

type TypeDef(parent: TypeConstraint?, name: Name)
type FFI(pos: Meta, name: Namespace, args: Name[])

type TypeField(pos: Meta, visibility: FieldVisibility, parameter: Parameter)

type FieldVisibility =
  | Local()
  | Global()

type Rank =
  | Expr(expr: Expression)
  | Unranked(pos: Meta)

type TypeInit =
  | Fact(pos: Meta, sig: PartialSignature<Expression>)
  | Command(pos: Meta, cmeta: Metadata, sig: PartialSignature<Parameter>, contract: Contract, body: Statement[], ttest: TrailingTest?)

type Parameter =
  | Untyped(pos: Meta, name: Name)
  | Typed(pos: Meta, name: Name, typ: TypeConstraint)
  | TypedOnly(pos: Meta, typ: TypeConstraint)

type TypeApp =
  | Named(pos: Meta, name: Name)
  | Static(pos: Meta, typ: TypeApp)
  | Function(pos: Meta, args: TypeConstraint[], ret: TypeConstraint)
  | Any(pos: Meta)

type TypeConstraint =
  | Type(pos: Meta, typ: TypeApp)
  | Has(pos: Meta, typ: TypeConstraint, traits: Trait[])

type Trait =
  | Named(pos: Meta, name: Name)

type Statement =
  | Fact(pos: Meta, signature: Signature<Expression>)
  | Forget(pos: Meta, signature: Signature<Expression>)
  | Let(pos: Meta, name: Name, value: Expression)
  | Simulate(pos: Meta, actors: Expression, context: SimulationContext, goal: SimulationGoal, signals: Signal[])
  | Assert(pos: Meta, expr: Expression)
  | Expr(value: Expression)

type SimulationContext =
  | Global()
  | Named(pos: Meta, name: Name)

type Signal(pos: Meta, signature: Signature<Parameter>, body: Statement[])

type Expression =
  | New(pos: Meta, typ: Name, fields: Expression[])
  | Invoke(pos: Meta, signature: Signature<Expression>)
  | Global(pos: Meta, name: Name)
  | Variable(pos: Meta, name: Name)
  | Self(pos: Meta)
  | List(pos: Meta, values: Expression[])
  | Record(pos: Meta, pairs: Pair<RecordField, Expression>[])
  | Search(pos: Meta, predicate: Predicate)
  | MatchSearch(pos: Meta, cases: MatchSearchCase[])
  | Project(pos: Meta, object: Expression, field: RecordField)
  | Select(pos: Meta, object: Expression, fields: Projection[])
  | For(pos: Meta, comprehension: ForExpression)
  | Block(pos: Meta, body: Statement[])
  | Apply(pos: Meta, partial: Expression, values: Expression[])
  | Pipe(pos: Meta, left: Expression, right: Expression)
  | PipeInvoke(pos: Meta, left: Expression, right: PartialSignature<Expression>)
  | Interpolate(pos: Meta, value: Interpolation<Expression>)
  | Condition(pos: Meta, cases: ConditionCase[])
  | HasType(pos: Meta, value: Expression, typ: TypeApp)
  | HasTrait(pos: Meta, value: Expression, typ: Trait)
  | Force(pos: Meta, value: Expression)
  | Lazy(pos: Meta, value: Expression)
  | Hole(pos: Meta)
  | Return(pos: Meta)
  | Type(pos: Meta, typ: TypeApp)
  | Lambda(pos: Meta, params: Name[], body: Statement[])
  | IntrinsicEqual(pos: Meta, left: Expression, right: Expression)
  | ForeignInvoke(pos: Meta, name: Namespace, args: Expression[])
  | Parens(pos: Meta, value: Expression)
  | Lit(value: Literal)
  | Handle(pos: Meta, body: Statement[], handlers: Handler[])
  | Perform(pos: Meta, effect: Name, variant: Name, args: Expression[])
  | ContinueWith(pos: Meta, value: Expression)
  | Dsl(pos: Meta, language: TypeApp, ast: DslAst[])

type DslAst =
  | Node(pos: Meta, sig: DslSignature<DslAst>[], attrs: DslAttr[])
  | Lit(pos: Meta, value: Literal)
  | Var(pos: Meta, name: Name)
  | List(pos: Meta, values: DslAst[])
  | Interpolation(pos: Meta, parts: Interpolation<DslAst>)
  | Dynamic(pos: Meta, value: Expression)

type DslSignature<T> =
  | Name(name: Name)
  | Child(value: T)

type DslAttr(pos: Meta, key: Name, value: DslAst)

type ForExpression =
  | Map(pos: Meta, name: Name, stream: Expression, body: ForExpression)
  | If(pos: Meta, condition: Expression, body: ForExpression)
  | Do(pos: Meta, body: Expression)

type MatchSearchCase(pos: Meta, predicate: Predicate, body: Statement[])
type ConditionCase(pos: Meta, guard: Expression, body: Statement[])

type RecordField =
  | FName(value: Name)
  | FText(value: String)
  | FComputed(value: Expression)

type Projection(pos: Meta, name: RecordField, alias: RecordField)

type Interpolation<T>(pos: Meta, parts: InterpolationPart<T>[])

type InterpolationPart<T> =
  | Escape(pos: Meta, character: string)
  | Static(pos: Meta, text: string)
  | Dynamic(pos: Meta, value: T)

type Literal =
  | False(pos: Meta)
  | True(pos: Meta)
  | Nothing(pos: Meta)
  | Text(pos: Meta, value: String)
  | Integer(pos: Meta, digits: string)
  | Float(pos: Meta, digits: string)

type SimulationGoal =
  | ActionQuiescence(pos: Meta)
  | EventQuiescence(pos: Meta)
  | TotalQuiescence(pos: Meta)
  | CustomGoal(pos: Meta, pred: Predicate)

type Predicate =
  | And(pos: Meta, left: Predicate, right: Predicate)
  | Or(pos: Meta, left: Predicate, right: Predicate)
  | Not(pos: Meta, pred: Predicate)
  | Has(pos: Meta, signature: Signature<Pattern>)
  | Sample(pos: Meta, size: Literal, pool: SamplingPool)
  | Constrain(pos: Meta, pred: Predicate, constraint: Expression)
  | Let(pos: Meta, name: Name, value: Expression)
  | Typed(pos: Meta, name: Name, typ: TypeApp)
  | Always(pos: Meta)
  | Parens(pos: Meta, pred: Predicate)

type SamplingPool =
  | Relation(pos: Meta, signature: Signature<Pattern>)
  | Type(pos: Meta, name: Name, typ: TypeApp)

type Pattern =
  | HasType(pos: Meta, typ: TypeApp, name: Pattern)
  | StaticType(pos: Meta, typ: TypeApp)
  | Global(pos: Meta, name: Name)
  | Variable(pos: Meta, name: Name)
  | Self(pos: Meta)
  | Wildcard(pos: Meta)
  | Lit(lit: Literal)

type Signature<T> =
  | Unary(pos: Meta, self: T, name: Name)
  | Binary(pos: Meta, op: Name, left: T, right: T)
  | Keyword(pos: Meta, self: T, pairs: Pair<Name, T>[])
  | KeywordSelfless(pos: Meta, pairs: Pair<Name, T>[])

type PartialSignature<T> =
  | Unary(pos: Meta, name: Name)
  | Binary(pos: Meta, op: Name, right: T)
  | Keyword(pos: Meta, pairs: Pair<Name, T>[])

type RelationPart =
  | Many(pos: Meta, name: Name)
  | One(pos: Meta, name: Name)

type Pair<K, V>(pos: Meta, key: K, value: V)
type Name(pos: Meta, name: string)
type Namespace(pos: Meta, names: string[])
type String(pos: Meta, text: string)

type REPL =
  | Declarations(x: Declaration[])
  | Statements(x: Statement[])
  | Command(x: ReplCommand)

type ReplCommand =
  | Rollback(sig: Signature<Expression>)
  | HelpCommand(sig: Signature<Parameter>)
  | HelpType(typ: TypeApp)

grammar Crochet : Program {
  program =
    | header ds:declaration* space* end
      -> Program(meta, ds)

  repl =
    | ws ds:declaration+ ws end -> REPL.Declarations(ds)
    | ws xs:statements1 ws end -> REPL.Statements(xs)
    | ws x:replCommand ws end -> REPL.Command(x)

  replCommand =
    | ":rollback" hs+ s:signature<hole> -> ReplCommand.Rollback(s)
    | ":help" hs+ command_ s:signature<parameter> -> ReplCommand.HelpCommand(s)
    | ":help" hs+ type_ t:typeApp -> ReplCommand.HelpType(t)

  declarationMeta =
    | ws d:meta_doc -> Metadata(d)

  meta_doc =
    | d:doc -> d
    |       -> []

  declaration =
    | relationDeclaration
    | doDeclaration
    | commandDeclaration
    | typeDeclaration
    | defineDeclaration
    | actionDeclaration
    | whenDeclaration
    | contextDeclaration
    | openDeclaration
    | localDeclaration
    | testDeclaration
    | effectDeclaration
    | traitDeclaration
    | traitImplementDeclaration
    | capabilityDeclaration
    | protectDeclaration

  capabilityDeclaration =
    | m:declarationMeta capability_ n:atom s<";">
      -> Declaration.Capability(meta, m, n)

  protectDeclaration =
    | protect_ e:protectEntity with_ c:atom s<";">
      -> Declaration.Protect(meta, c, e)

  protectEntity =
    | type_ n:atom    -> ProtectEntity.Type(meta, n)
    | effect_ n:atom  -> ProtectEntity.Effect(meta, n)
    | global_ n:atom  -> ProtectEntity.Definition(meta, n)
    | trait_ n:atom   -> ProtectEntity.Trait(meta, n)

  traitDeclaration =
    | m:declarationMeta trait_ n:atom with_ cs:traitInstruction+ end_
      -> Declaration.Trait(meta, m, n)
    | m:declarationMeta trait_ n:atom s<";">
      -> Declaration.Trait(meta, m, n)

  // Currently ignored
  traitInstruction =
    | traitCommand
    | traitRequires

  traitCommand =
    | declarationMeta command_ signature<parameter> contractDefinition s<";">
      -> null

  traitRequires =
    | requires_ trait_ n:traitName s<";">
      -> null
  
  traitImplementDeclaration =
    | implement_ tr:traitName for_ tp:typeApp s<";">
      -> Declaration.ImplementTrait(meta, tp, tr)

  effectDeclaration =
    | m:declarationMeta effect_ n:atom with_ cs:effectCase+ end_
      -> Declaration.Effect(meta, m, n, cs)

  effectCase =
    | m:declarationMeta s:atom xs:effectCaseParams s<";">
      -> EffectCase(meta, m, s, xs)

  effectCaseParams =
    | s<"("> xs:list0<typeParameter, s<",">> s<")"> -> xs

  testDeclaration =
    | test_ s:string do_ b:statements end_
      -> Declaration.Test(meta, s, b)

  trailingTest =
    | oneTrailingTest
    | s<";">  -> null

  oneTrailingTest =
    | test_ b:statements end_
      -> TrailingTest(meta, b)

  localDeclaration =
    | local_ d:defineDeclaration
      -> Declaration.Local(meta, d)
    | local_ t:typeDeclaration
      -> Declaration.Local(meta, t)

  openDeclaration =
    | open_ ns:namespace s<";">
      -> Declaration.Open(meta, ns)

  relationDeclaration =
    | m:declarationMeta ws relation_ s:logicSignature<relationPart> s<";">
      -> Declaration.Relation(meta, m, s)

  relationPart =
    | n:name s<"*"> -> RelationPart.Many(meta, n)
    | n:name        -> RelationPart.One(meta, n)

  doDeclaration =
    | prelude_ xs:statements end_
      -> Declaration.Do(meta, xs)

  commandDeclaration =
    | m:declarationMeta ws command_ s:signature<parameter> c:contractDefinition s<"="> e:expression t:trailingTest 
      -> Declaration.Command(meta, m, s, c, [Statement.Expr(e)], t)

    | m:declarationMeta ws command_ s:signature<parameter> c:contractDefinition do_ b:statements t:oneTrailingTest
      -> Declaration.Command(meta, m, s, c, b, t)

    | m:declarationMeta ws command_ s:signature<parameter> c:contractDefinition do_ b:statements end_
      -> Declaration.Command(meta, m, s, c, b, null)

  contractDefinition =
    | ret:retContractDefinition pre:preContractDefinition post:postContractDefinition
      -> Contract(meta, ret, pre, post)

  retContractDefinition =
    | s<"->"> t:typeConstraintPrimary
      -> t
    | -> null

  preContractDefinition =
    | requires_ cs:list1<contractCondition, s<",">>
      -> cs
    | -> []
  
  postContractDefinition =
    | ensures_ cs:list1<contractCondition, s<",">>
      -> cs
    | -> []

  contractCondition =
    | n:atom s<"::"> e:expression
      -> ContractCondition(meta, n, e)

  parameter =
    | n:name
      -> Parameter.Untyped(meta, n)
    | s<"("> n:name is_ t:typeConstraint s<")"> 
      -> Parameter.Typed(meta, n, t)
    | s<"("> n:name has_ trs:list1<traitName, s<",">> s<")">
      -> Parameter.Typed(meta, n, TypeConstraint.Has(meta, TypeConstraint.Type(meta, TypeApp.Any(meta)), trs))
    | t:typeAppStatic
      -> Parameter.TypedOnly(meta, TypeConstraint.Type(meta, t))

  typeConstraint =
    | t:typeConstraint1 has_ trs:list1<traitName, s<",">>
        -> TypeConstraint.Has(meta, t, trs)
    | typeConstraint1

  typeConstraint1 =
    | n:name is_ c:typeApp -> TypeConstraint.Type(meta, c)
    | typeConstraintPrimary

  typeConstraintPrimary =
    | n:name                         -> TypeConstraint.Type(meta, TypeApp.Any(meta))
    | t:typeApp1                     -> TypeConstraint.Type(meta, t)
    | s<"("> t:typeConstraint s<")"> -> t
  
  typeApp =
    | ts:typeAppArgs s<"->"> t:typeConstraintPrimary -> TypeApp.Function(meta, ts, t)
    | typeApp1

  typeAppArgs =
    | s<"("> ts:list0<typeConstraint, s<",">> s<")"> -> ts
    | t:typeConstraintPrimary -> [t]

  typeApp1 =
    | t:typeAppStatic s<"<"> list0<typeConstraint, s<",">> s<">"> -> t
    | typeAppStatic

  typeAppStatic =
    | s<"#"> t:typeAppPrimary     -> TypeApp.Static(meta, t)
    | typeAppPrimary

  typeAppPrimary =
    | t:typeName                -> TypeApp.Named(meta, t)
    | s<"("> t:typeApp s<")">   -> t

  typeName =
    | atom
    | x:nothing_  -> Name(meta, x)
    | x:true_     -> Name(meta, x)
    | x:false_    -> Name(meta, x)

  traitName =
    | x:atom -> Trait.Named(meta, x)

  typeDeclaration =
    | m:declarationMeta ws type_ t:typeName s<"="> foreign_ n:namespace s<";">
      -> Declaration.ForeignType(meta, m, t, n)

    | m:declarationMeta ws enum_ t:typeName s<"="> vs:nonemptyListOf<typeName, s<",">> s<";">
      -> Declaration.EnumType(meta, m, t, vs)

    | m:declarationMeta ws abstract_ t:basicType s<";">
      -> Declaration.AbstractType(meta, m, t)

    | m:declarationMeta ws singleton_ t:basicType i:typeInitBlock
      -> Declaration.SingletonType(meta, m, t, i)

    | m:declarationMeta ws type_ n:atom fs:typeFields p:typeDefParent s<";">
      -> Declaration.Type(meta, m, TypeDef(p, n), fs)

  basicType =
    | n:atom p:typeDefParent    -> TypeDef(p, n)

  typeDefParent =
    | is_ t:typeConstraint   -> t
    |                        -> null

  typeInitBlock =
    | with_ x:typeInit* end_    -> x
    | s<";">                    -> []

  typeFields =
    | s<"("> fs:list1<typeField, s<",">> s<")">  -> fs
    |                                            -> []

  typeField =
    | v:fieldVisibility p:typeParameter -> TypeField(meta, v, p)
    
  typeParameter =
    | n:typeFieldName is_ t:typeConstraint                -> Parameter.Typed(meta, n, t)
    | n:typeFieldName                                     -> Parameter.Untyped(meta, n)

  fieldVisibility =
    | global_ -> FieldVisibility.Global()
    |         -> FieldVisibility.Local()

  typeFieldName = name | atom

  typeInit =
    | s:partialLogicSignature<invokePostfix> s<";">
      -> TypeInit.Fact(meta, s)
    | typeInitCommand

  typeInitCommand =
    | m:declarationMeta ws command_ s:partialSignature<parameter> c:contractDefinition s<"="> e:s<expression> t:trailingTest
      -> TypeInit.Command(meta, m, s, c, [Statement.Expr(e)], t)
    | m:declarationMeta ws command_ s:partialSignature<parameter> c:contractDefinition do_ b:statements t:oneTrailingTest
      -> TypeInit.Command(meta, m, s, c, b, t)
    | m:declarationMeta ws command_ s:partialSignature<parameter> c:contractDefinition do_ b:statements end_
      -> TypeInit.Command(meta, m, s, c, b, null)

  defineDeclaration =
    | m:declarationMeta ws define_ n:atom s<"="> e:s<atomicExpression> s<";">
      -> Declaration.Define(meta, m, n, e)

  actionDeclaration =
    | m:declarationMeta ws action_
        t:parameter
        n:atom
        title:interpolateExpression?
        p:actionPredicate
        r:actionRank
        do_ b:statements 
        c:actionInit
        end_ 
      -> Declaration.Action(meta, m, t, n, title, p, r, b, c)

  actionPredicate =
    | when_ p:predicate -> p
    |                   -> Predicate.Always(meta)

  actionRank =
    | rank_ e:s<expression> -> Rank.Expr(e)
    |                       -> Rank.Unranked(meta)

  actionInit =
    | with_ cs:typeInitCommand* -> cs
    |                           -> []

  whenDeclaration =
    | m:declarationMeta ws when_ p:predicate do_ b:statements end_
      -> Declaration.When(meta, m, p, b)

  contextDeclaration =
    | m:declarationMeta ws context_ n:atom with_ xs:contextItem* end_
      -> Declaration.Context(meta, m, n, xs)

  contextItem =
    | actionDeclaration
    | whenDeclaration

  // -- Logic
  predicate =
    | predicateBinary

  predicateBinary =
    | predicateAnd
    | predicateOr
    | predicateNot

  predicateAnd =
    | l:predicateNot s<","> r:predicateAnd1   -> Predicate.And(meta, l, r)
  
  predicateAnd1 =
    | l:predicateNot s<","> r:predicateAnd1   -> Predicate.And(meta, l, r)
    | predicateNot

  predicateOr =
    | l:predicateNot s<"|"> r:predicateOr1    -> Predicate.Or(meta, l, r)
  
  predicateOr1 =
    | l:predicateNot s<"|"> r:predicateOr1    -> Predicate.Or(meta, l, r)
    | predicateNot
  
  predicateNot =
    | not_ p:predicateConstrain               -> Predicate.Not(meta, p)
    | predicateConstrain

  predicateConstrain =
    | p:predicateLet if_ c:s<expression>      -> Predicate.Constrain(meta, p, c)
    | if_ c:s<expression>                     -> Predicate.Constrain(meta, Predicate.Always(meta), c)
    | predicateLet
    | predicateSample
    | predicateType
    | predicatePrimary

  predicateType =
    | n:name is_ t:typeApp                    -> Predicate.Typed(meta, n, t)

  predicateLet =
    | let_ n:name s<"="> e:s<expression>      -> Predicate.Let(meta, n, e)

  predicateSample =
    | sample_ n:integer of_ p:samplingPool
      -> Predicate.Sample(meta, n, p)

  samplingPool =
    | r:logicSignature<pattern>
      -> SamplingPool.Relation(meta, r)
    | l:name is_ t:typeApp
      -> SamplingPool.Type(meta, l, t)

  predicatePrimary =
    | always_                                 -> Predicate.Always(meta)
    | r:logicSignature<pattern>               -> Predicate.Has(meta, r)
    | s<"("> p:predicate s<")">               -> Predicate.Parens(meta, p)

  pattern =
    | s<"("> c:patternComplex s<")">  -> c
    | s<"#"> p:typeAppPrimary -> Pattern.StaticType(meta, p)
    | n:atom                  -> Pattern.Global(meta, n)
    | self_                   -> Pattern.Self(meta)
    | l:literal               -> Pattern.Lit(l)
    | patternName

  patternComplex =
    | n:patternName is_ t:typeApp   -> Pattern.HasType(meta, t, n)

  patternName =
    | s<"_">        -> Pattern.Wildcard(meta)
    | n:name        -> Pattern.Variable(meta, n)


  // -- Statement
  statement =
    | s<letStatement>
    | s<factStatement>
    | s<forgetStatement>
    | s<simulateStatement>
    | s<assertStatement>
    | e:s<expression>    -> Statement.Expr(e)

  blockStatement =
    | x:blockExpression -> Statement.Expr(x)

  letStatement =
    | let_ n:name s<"="> e:s<expression>
      -> Statement.Let(meta, n, e)
  
  factStatement =
    | fact_ s:logicSignature<primaryExpression> 
      -> Statement.Fact(meta, s)
  
  forgetStatement =
    | forget_ s:logicSignature<primaryExpression>
      -> Statement.Forget(meta, s)

  simulateStatement =
    | simulate_ for_ e:expression c:simulateContext until_ g:simulateGoal s:signal*
      -> Statement.Simulate(meta, e, c, g, s)

  simulateContext =
    | in_ n:atom    -> SimulationContext.Named(meta, n)
    |               -> SimulationContext.Global()

  simulateGoal =
    | action_ quiescence_ -> SimulationGoal.ActionQuiescence(meta)
    | event_ quiescence_  -> SimulationGoal.EventQuiescence(meta)
    | quiescence_         -> SimulationGoal.TotalQuiescence(meta)
    | p:predicate         -> SimulationGoal.CustomGoal(meta, p)

  signal =
    | on_ s:signature<parameter> do_ b:statements end_
      -> Signal(meta, s, b)

  assertStatement =
    | assert_ e:expression
      -> Statement.Assert(meta, e)

  // -- Expressions
  expression =
    | blockExpression
    | s<searchExpression>
    | s<lazyExpression>
    | s<forceExpression>
    | s<foreignExpression>
    | s<continueWithExpression>
    | s<assignExpression>
    | s<pipeExpression>

  searchExpression =
    | search_ p:predicate
      -> Expression.Search(meta, p)

  lazyExpression =
    | lazy_ e:expression -> Expression.Lazy(meta, e)

  forceExpression =
    | force_ e:expression -> Expression.Force(meta, e)

  foreignExpression =
    | foreign_ ns:namespace s<"("> xs:list0<expression, s<",">> s<")">
      -> Expression.ForeignInvoke(meta, ns, xs)

  continueWithExpression =
    | continue_ with_ e:pipeExpression
      -> Expression.ContinueWith(meta, e)

  expressionBlock =
    | do_ b:statements end_ -> Expression.Block(meta, b)

  assignExpression =
    | l:invokePostfix op:named<"<-"> r:pipeExpression
      -> Expression.Invoke(meta, Signature.Binary(meta, op, l, r))

  pipeExpression =
    | l:pipeExpression s<"|>"> r:invokeMixfix
      -> Expression.Pipe(meta, l, r)
    | l:pipeExpression s<"|"> r:partialSignature<invokePostfix>
      -> Expression.PipeInvoke(meta, l, r)
    | invokeMixfix

  invokeMixfix =
    | s:invokeInfixExpression ps:signaturePair<invokeInfixExpression>+
      -> Expression.Invoke(meta, Signature.Keyword(meta, s, ps))
    | ps:signaturePair<invokeInfixExpression>+
      -> Expression.Invoke(meta, Signature.KeywordSelfless(meta, ps))
    | invokeInfixExpression

  invokeInfixExpression =
    | l:invokePostfix s<"=:="> r:invokePostfix
      -> Expression.IntrinsicEqual(meta, l, r)
    | l:invokePostfix op:named<t_relational_op> r:invokePostfix
      -> Expression.Invoke(meta, Signature.Binary(meta, op, l, r))
    | invokeInfixSequence<named<"++">>
    | invokeInfixSequence<named<"+">>
    | invokeInfixSequence<named<"-">>
    | invokeInfixSequence<named<"**">>
    | invokeInfixSequence<named<"*">>
    | invokeInfixSequence<named<"/">>
    | invokeInfixSequence<named<"%">>
    | invokeInfixSequence<and>
    | invokeInfixSequence<or>
    | castExpression

  invokeInfixSequence<op> =
    | l:invokeInfixSequence<op> x:op r:invokePostfix
      -> Expression.Invoke(meta, Signature.Binary(meta, x, l, r))
    | l:invokePostfix x:op r:invokePostfix
      -> Expression.Invoke(meta, Signature.Binary(meta, x, l, r))

  castExpression =
    | s:invokePrePost op:as t:castType
      -> Expression.Invoke(meta, Signature.Binary(meta, op, s, t))
    | s:invokePrePost is_ t:typeAppPrimary
      -> Expression.HasType(meta, s, t)
    | invokePrePost

  castType =
    | t:typeAppPrimary -> Expression.Type(meta, t)

  invokePrePost =
    | invokePrefix

  invokePrefix =
    | n:not p:invokePostfix
      -> Expression.Invoke(meta, Signature.Unary(meta, p, n))
    | invokePostfix

  invokePostfix =
    | s:invokePostfix n:atom
      -> Expression.Invoke(meta, Signature.Unary(meta, s, n))
    | applyExpression

  applyExpression =
    | f:applyExpression s<"("> xs:list0<expression, s<",">> s<")">
      -> Expression.Apply(meta, f, xs)
    | memberExpression

  memberExpression =
    | o:memberExpression s<"."> f:recordField
      -> Expression.Project(meta, o, f)
    | o:memberExpression s<"."> p:memberSelection
      -> Expression.Select(meta, o, p)
    | primaryExpression

  memberSelection =
    | s<"("> xs:list1<fieldSelection, s<",">> s<")">
      -> xs

  fieldSelection =
    | n:recordField as_ a:recordField
      -> Projection(meta, n, a)
    | n:recordField
      -> Projection(meta, n, n)

  primaryExpression =
    | newExpression<expression>
    | interpolateExpression
    | literalExpression
    | recordExpression<expression>
    | listExpression<expression>
    | lambdaExpression
    | performExpression
    | hole
    | s<"#"> t:typeAppPrimary       -> Expression.Type(meta, t)
    | return_                       -> Expression.Return(meta)
    | self_                         -> Expression.Self(meta)
    | n:atom                        -> Expression.Global(meta, n)
    | n:name                        -> Expression.Variable(meta, n)
    | s<"("> e:expression s<")">    -> Expression.Parens(meta, e)

  conditionExpression =
    | condition_ cs:conditionCase+ end_
      -> Expression.Condition(meta, cs)

  conditionCase =
    | when_ e:expression b:eblock
      -> ConditionCase(meta, e, b)
    | otherwise_ b:eblock
      -> ConditionCase(meta, Expression.Lit(Literal.True(meta)), b)

  matchSearchExpression =
    | match_ c:matchSearchCase+ end_
      -> Expression.MatchSearch(meta, c)

  matchSearchCase =
    | when_ p:predicate b:eblock
      -> MatchSearchCase(meta, p, b)
    | otherwise_ b:eblock
      -> MatchSearchCase(meta, Predicate.Always(meta), b)

  forExpression =
    | for_ b:forExprMap
      -> Expression.For(meta, b)

  forExprMap =
    | n:name in_ e:expression r:forExprMap1
      -> ForExpression.Map(meta, n, e, r)
  
  forExprMap1 =
    | s<","> b:forExprMap             -> b
    | if_ e:expression b:forExprDo    -> ForExpression.If(meta, e, b)
    | forExprDo
  
  forExprDo =
    | b:expressionBlock -> ForExpression.Do(meta, b)

  performExpression =
    | perform_ n:atom s<"."> v:atom s<"("> xs:list0<expression, s<",">> s<")">
      -> Expression.Perform(meta, n, v, xs)

  newExpression<e> =
    | new_ n:atom fs:newFields<e>   -> Expression.New(meta, n, fs)

  newFields<e> =
    | s<"("> fs:list1<e, s<",">> s<")">    -> fs
    |                                      -> []

  listExpression<e> =
    | s<"["> xs:list0<e, s<",">> s<"]">
      -> Expression.List(meta, xs)

  recordExpression<e> =
    | s<"["> s<"->"> s<"]">                            -> Expression.Record(meta, [])
    | s<"["> xs:list1<recordPair<e>, s<",">> s<"]">    -> Expression.Record(meta, xs)

  recordPair<e> =
    | n:recordField s<"->"> v:e -> Pair(meta, n, v)

  recordField =
    | n:(name | atom)               -> RecordField.FName(n)
    | t:string                      -> RecordField.FText(t)
    | s<"["> e:expression s<"]">    -> RecordField.FComputed(e)

  literalExpression =
    | l:literal             -> Expression.Lit(l)

  lambdaExpression =
    | s<"{"> e:statements s<"}">
      -> Expression.Lambda(meta, [], e)
    | s<"{"> p:list1<name, s<",">> in_ e:statements s<"}">
      -> Expression.Lambda(meta, p, e)

  handleExpression =
    | handle_ b:statements with_ hs:handlers end_
      -> Expression.Handle(meta, b, hs)

  handlers =
    | xs:one_handler+ -> xs

  one_handler =
    | on_ n:atom s<"."> v:atom s<"("> xs:list0<name, s<",">> s<")"> b:eblock
      -> Handler(meta, n, v, xs, b)

  atomicExpression =
    | a:atom                                -> Expression.Global(meta, a)
    | lazyExpression
    | newExpression<atomicExpression>
    | literalExpression
    | recordExpression<atomicExpression>
    | listExpression<atomicExpression>

  blockExpression =
    | expressionBlock
    | conditionExpression
    | matchSearchExpression
    | forExpression
    | handleExpression
    | dslExpression

  interpolateExpression =
    | x:interpolateText<expression> -> Expression.Interpolate(meta, x)

  interpolateText<t> =
    | s<"<<"> xs:interpolatePart<t, ">>">* ">>"
      -> Interpolation(meta, xs)
    | s<"\""> xs:interpolatePart<t, "\"">* "\""
      -> Interpolation(meta, xs)

  interpolatePart<p, e> =
    | "\\" c:escape_sequence     -> InterpolationPart.Escape(meta, c)
    | "[" x:s<p> s<"]">          -> InterpolationPart.Dynamic(meta, x)
    | c:interpolateStatic<e>     -> InterpolationPart.Static(meta, c)

  token interpolateStatic<e> =
    | (~(e | "\\" | "[") any)+ 


  // -- DSLs
  dslExpression =
    | dsl_ t:typeApp with_ x:dslNodeSeq end_
      -> Expression.Dsl(meta, t, x)

  dslNodeSeq =
    | xs:list0<dslNode, s<";">> -> xs

  dslNode =
    | s:dslSignature<dslPrimary> o:dslAttribute*
      -> DslAst.Node(meta, s, o)
    | dslPrimary

  dslPrimary =
    | n:name                      -> DslAst.Var(meta, n)
    | x:interpolateText<dslNode>  -> DslAst.Interpolation(meta, x)
    | l:literal                   -> DslAst.Lit(meta, l)
    | x:dslCrochet                -> DslAst.Dynamic(meta, x)
    | xs:dslNodeList             -> DslAst.List(meta, xs)
    | s<"("> x:dslNode s<")">     -> x

  dslNodeList =
    | s<"["> xs:dslNodeSeq s<"]"> -> xs

  dslCrochet =
    | s<"@("> x:expression s<")"> -> x

  dslAttribute =
    | k:attribute v:dslPrimary  -> DslAttr(meta, k, v)

  dslSignature<t> =
    | n:atom xs:dslSignatureComponent<t>+ -> [DslSignature.Name(n), ...xs]

  dslSignatureComponent<t> =
    | x:atom          -> DslSignature.Name(x)
    | n:dslPrimary    -> DslSignature.Child(n)

  // -- Literals
  literal =
    | text
    | float
    | integer
    | boolean
    | nothing

  nothing = nothing_ -> Literal.Nothing(meta)

  boolean =
    | true_                 -> Literal.True(meta)
    | false_                -> Literal.False(meta)

  text =
    | x:string              -> Literal.Text(meta, x)

  integer =
    | x:s<t_integer>        -> Literal.Integer(meta, x)

  float =
    | x:s<t_float>          -> Literal.Float(meta, x)

  string =
    | x:s<t_text>           -> String(meta, x)
  
  hole =
    | x:s<"_"> ~name_rest   -> Expression.Hole(meta)

  // -- Token -> Rule & Basics
  atom =
    | s<"'"> x:t_atom               -> Name(meta, x)
    | ~reserved x:s<t_atom> ~":"    -> Name(meta, x)

  name = x:s<t_name>                          -> Name(meta, x)
  keyword = x:s<t_keyword>                    -> Name(meta, x)
  attribute = x:s<t_attribute>                -> Name(meta, x)
  infix_symbol = x:s<t_infix_symbol>          -> Name(meta, x)
  not = x:not_                                -> Name(meta, x)
  and = x:and_                                -> Name(meta, x)
  or = x:or_                                  -> Name(meta, x)
  as = x:as_                                  -> Name(meta, x)

  namespace = x:s<nonemptyListOf<t_atom, s<".">>>  -> Namespace(meta, x)

  // -- Higher-order
  named<n> = x:s<n> -> Name(meta, x)

  logicSignature<t> =
    | s:t kws:signaturePair<t>+       -> Signature.Keyword(meta, s, kws)
    | s:t n:atom                      -> Signature.Unary(meta, s, n)
    | kws:signaturePair<t>+           -> Signature.KeywordSelfless(meta, kws)

  signaturePair<t> =
    | kw:keyword v:t  -> Pair(meta, kw, v)

  partialLogicSignature<t> =
    | kws:signaturePair<t>+       -> PartialSignature.Keyword(meta, kws)
    | n:atom                      -> PartialSignature.Unary(meta, n)

  partialSignature<t> =
    | kws:signaturePair<t>+       -> PartialSignature.Keyword(meta, kws)
    | op:infix_symbol r:t         -> PartialSignature.Binary(meta, op, r)
    | n:atom                      -> PartialSignature.Unary(meta, n)
    | n:not                       -> PartialSignature.Unary(meta, n)

  signature<t> =
    | l:t op:as r:asParameter         -> Signature.Binary(meta, op, l, r)
    | l:t op:infix_symbol r:t         -> Signature.Binary(meta, op, l, r)
    | s:t kws:signaturePair<t>+       -> Signature.Keyword(meta, s, kws)
    | s:t n:atom                      -> Signature.Unary(meta, s, n)
    | n:not s:t                       -> Signature.Unary(meta, s, n)
    | kws:signaturePair<t>+           -> Signature.KeywordSelfless(meta, kws)

  asParameter =
    | t:typeAppPrimary -> Parameter.TypedOnly(meta, TypeConstraint.Type(meta, TypeApp.Static(meta, t)))

  list0<t, s> =
    | xs:listOf<t, s> s? -> xs

  list1<t, s> =
    | xs:nonemptyListOf<t, s> s? -> xs

  block<t> =
    | do_ xs:t* end_ -> xs

  statements =
    | h:blockStatement s<";">? ws t:statements1 -> [h, ...t]
    | h:statement ws ";" ws t:statements1       -> [h, ...t]
    | x:statement s<";">?                       -> [x]
    |                                           -> []

  statements1 =
    | h:blockStatement s<";">? ws t:statements1   -> [h, ...t]
    | h:statement ws ";" ws t:statements1         -> [h, ...t]
    | x:statement s<";">?                         -> [x]

  eblock =
    | do_ b:statements end_             -> b
    | s<"=>"> e:expression s<";">       -> [Statement.Expr(e)]

  s<p> = space* x:p -> x
  ws = space*


  // -- Lexical
  token header (a file header) = space* "%" hs* "crochet" nl
  token hs = " " | "\t"
  token nl = "\r\n" | "\n" | "\r"
  token line = (~nl any)*
  token comment (a comment) = "//" ~"/" line
  space += comment

  doc (a documentation comment) = xs:doc_line+ -> xs
  doc_line (a documentation comment) = hs* "///" hs? x:line nl -> x

  semi = s<";">

  token atom_start = "a".."z"
  token atom_rest = letter | digit | "-"
  token t_atom (an atom) = atom_start atom_rest*

  token t_keyword (a keyword) = t_atom ":"

  token t_attribute (an attribute) = "--" ~"-" t_atom

  token name_start = "A".."Z" | "_"
  token name_rest = letter | digit | "-"
  token t_name (a name) = name_start name_rest*

  token t_infix_symbol =
    | x:t_any_infix ~infix_character  -> x
    | and_
    | or_
    | as_

  token t_any_infix =
    | "<-"
    | t_relational_op
    | t_arithmetic_op

  token t_relational_op =
    | "===" | "=/="
    | ">=" | ">"
    | "<=" | "<"

  token t_arithmetic_op =
    | "++" | "+"
    | "-"
    | "**" | "*"
    | "/"
    | "%"

  token infix_character = "+" | "-" | "*" | "/" | "<" | ">" | "=" | "%"

  // -- Literals
  token dec_digit = "0".."9" | "_"
  token hex_digit = "0".."9" | "a".."f" | "A".."F"

  token t_integer (an integer) =
    | ~"_" "-"? dec_digit+

  token t_float (a floating point number) =
    | ~"_" "-"? dec_digit+ "." dec_digit+

  token text_character =
    | "\\" escape_sequence
    | ~"\"" any

  token escape_sequence =
    | "u" hex_digit hex_digit hex_digit hex_digit
    | "x" hex_digit hex_digit
    | any

  token t_text (a text) =
    | "\"" text_character* "\""


  // -- Reserved words
  kw<w> = x:s<w> ~atom_rest -> x

  relation_ = kw<"relation">
  predicate_ = kw<"predicate">
  when_ = kw<"when">
  do_ = kw<"do">
  command_ = kw<"command">
  type_ = kw<"type">
  enum_ = kw<"enum">
  define_ = kw<"define">
  singleton_ = kw<"singleton">
  action_ = kw<"action">
  let_ = kw<"let">
  return_ = kw<"return">
  fact_ = kw<"fact">
  forget_ = kw<"forget">
  new_ = kw<"new">
  search_ = kw<"search">
  if_ = kw<"if">
  then_ = kw<"then">
  else_ = kw<"else">
  goto_ = kw<"goto">
  call_ = kw<"call">
  simulate_ = kw<"simulate">
  match_ = kw<"match">
  true_ = kw<"true">
  false_ = kw<"false">
  not_ = kw<"not">
  and_ = kw<"and">
  or_ = kw<"or">
  is_ = kw<"is">
  self_ = kw<"self">
  as_ = kw<"as">
  event_ = kw<"event">
  quiescence_ = kw<"quiescence">
  for_ = kw<"for">
  until_ = kw<"until">
  in_ = kw<"in">
  foreign_ = kw<"foreign">
  on_ = kw<"on">
  always_ = kw<"always">
  condition_ = kw<"condition">
  end_ = kw<"end">
  prelude_ = kw<"prelude">
  with_ = kw<"with">
  tags_ = kw<"tags">
  rank_ = kw<"rank">
  abstract_ = kw<"abstract">
  lazy_ = kw<"lazy">
  force_ = kw<"force">
  context_ = kw<"context">
  sample_ = kw<"sample">
  of_ = kw<"of">
  open_ = kw<"open">
  local_ = kw<"local">
  test_ = kw<"test">
  assert_ = kw<"assert">
  requires_ = kw<"requires">
  ensures_ = kw<"ensures">
  nothing_ = kw<"nothing">
  effect_ = kw<"effect">
  handle_ = kw<"handle">
  continue_ = kw<"continue">
  perform_ = kw<"perform">
  dsl_ = kw<"dsl">
  trait_ = kw<"trait">
  implement_ = kw<"implement">
  has_ = kw<"has">
  global_ = kw<"global">
  capability_ = kw<"capability">
  protect_ = kw<"protect">
  otherwise_ = kw<"otherwise">

  reserved =
    | relation_ | predicate_ | when_ | do_ | command_ | action_
    | type_ | enum_ | define_ | singleton_ | goto_ | call_
    | let_ | return_ | fact_ | forget_ | new_ | search_ | if_ | simulate_
    | true_ | false_ | not_ | and_ | or_ | is_ | self_ | as_
    | event_ | quiescence_ | for_ | until_ | in_ | foreign_ | on_
    | always_ | match_ | then_ | else_ | condition_ | end_ | prelude_ | with_
    | tags_ | rank_ | abstract_ | lazy_ | force_ | context_ | sample_ | of_
    | open_ | local_ | test_ | assert_ | requires_ | ensures_ | nothing_
    | effect_ | handle_ | continue_ | perform_ | dsl_ | trait_ | implement_ | has_
    | global_ | capability_ | protect_ | otherwise_
}