datatype Either<+L, +R> = Left(l: L) | Right(r: R)

datatype Lang<!A> = Lang(mem: (string, A) -> bool, repr: iset<A>)

function Atom<A>(s: string, value: A): Lang<A> {
  Lang((input, a) => s == input && a == value, iset{})
}

function Char(c: char): Lang<char> {
  Atom([c], c)
}

function EitherL<A, B>(l: Lang<A>, r: Lang<B>): Lang<Either<A, B>> {
  Lang((input, ab: Either<A, B>) =>
    || (exists a | a in l.repr :: ab == Left(a) && l.mem(input, a))
    || (exists b | b in r.repr :: ab == Right(b) && r.mem(input, b)),
    (iset a | a in l.repr :: Left(a)) + (iset b | b in r.repr :: Right(b))
  )
}

// Nondeterministic in general
function ConcatL<A, B> (l: Lang<A>, r: Lang<B>): Lang<(A, B)> {
  Lang((input, p) =>
    exists s1, s2, a, b | a in l.repr && b in r.repr::
      input == s1 + s2 && p == (a, b),
    iset a, b | a in l.repr && b in r.repr :: (a,b)
  )
}

function Empty<A>(): Lang<A> { Lang((_, _) => false, iset{}) }

function MapL<A, B> (l: Lang<A>, f: A -> B): Lang<B> {
  Lang((input, b) =>
    exists a: A | a in l.repr :: b == f(a) && l.mem(input, a),
    iset a | a in l.repr :: f(a)
  )
}

function Ignore<A>(l: Lang<A>): Lang<()> { MapL(l, (_) => ()) }

function Epsilon(): Lang<()> {
  Lang((input, _) => input == "", iset{})
}

function RepeatAux<A>(pred : (string, A) -> bool, repr: iset<A>, input: string, output: seq<A>): bool
  decreases |output|
{
  || (input == "" && output == [])
  || (exists init, tail, a, alist | a in repr ::
      && input == init + tail
      && output == [a] + alist
      && pred(a, init)
      && RepeatAux(pred, repr, tail, alist))
}

Unhandled exception. System.AggregateException: One or more errors occurred. (Index was out of range. Must be non-negative and less than the size of the collection. (Parameter 'index'))
 ---> System.ArgumentOutOfRangeException: Index was out of range. Must be non-negative and less than the size of the collection. (Parameter 'index')
   at Microsoft.Dafny.Resolver.ImposeSubtypingConstraint(Type super, Type sub, ErrorMsg errorMsg)
   at Microsoft.Dafny.Resolver.AssignProxyAndHandleItsConstraints_aux(TypeProxy proxy, Type t, Boolean keepConstraints)
   at Microsoft.Dafny.Resolver.AssignProxyAndHandleItsConstraints_aux(TypeProxy proxy, Type t, Boolean keepConstraints)
   at Microsoft.Dafny.Resolver.AssignProxyAndHandleItsConstraints_aux(TypeProxy proxy, Type t, Boolean keepConstraints)
   at Microsoft.Dafny.Resolver.AssignKnownEndsFullstrength_SuperDirection(TypeProxy proxy)
   at Microsoft.Dafny.Resolver.ProcessFullStrength_SuperDirection(Type t, ISet`1 processed, Boolean& anyNewConstraints)
   at Microsoft.Dafny.Resolver.PartiallySolveTypeConstraints(Boolean allowDecisions)
   at Microsoft.Dafny.Resolver.SolveAllTypeConstraints()
   at Microsoft.Dafny.Resolver.ResolveFunction(Function f)
   at Microsoft.Dafny.Resolver.ResolveClassMemberBodies(TopLevelDeclWithMembers cl)
   at Microsoft.Dafny.Resolver.ResolveTopLevelDecls_Core(List`1 declarations, Graph`1 datatypeDependencies, Graph`1 codatatypeDependencies, Boolean isAnExport)
   at Microsoft.Dafny.Resolver.ResolveModuleDefinition(ModuleDefinition m, ModuleSignature sig, Boolean isAnExport)
   at Microsoft.Dafny.Resolver.ResolveProgram(Program prog)
   at Microsoft.Dafny.Main.Resolve(Program program, ErrorReporter reporter)
   at Microsoft.Dafny.DafnyDriver.ProcessFiles(IList`1 dafnyFiles, ReadOnlyCollection`1 otherFileNames, ErrorReporter reporter, Boolean lookForSnapshots, String programId)
   --- End of inner exception stack trace ---
   at System.Threading.Tasks.Task.ThrowIfExceptional(Boolean includeTaskCanceledExceptions)
   at System.Threading.Tasks.Task`1.GetResultCore(Boolean waitCompletionNotification)
   at System.Threading.Tasks.Task`1.get_Result()
   at Microsoft.Dafny.DafnyDriver.ThreadMain(String[] args)
   at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass9_0.<Main>b__0()
   at System.Threading.Thread.StartCallback()