lobby addImmutableSlot: #Types valued: Namespace clone.
Types addImmutableDelegate: #lobby valued: lobby.

Types addSlot: #Type valued: Cloneable derive.
Types Type addSlot: #rules valued: Cloneable clone.

"Types are Slate's basic type system for minimal inference purposes.
A type's rules are delegated to its supertypes' rules."

type@(Types Type traits) derive
"Arrange for and return a new subtype."
[| newType |
  newType: resend.
  newType rules: Cloneable clone.
  newType rules addImmutableDelegate: #parent valued: type rules.
  newType
].

type@(Types Type traits) deriveWith: types
"Arrange for and return a new subtype of the given types in left-to-right
order."
[| newType |
  newType: resend.
  newType rules: Cloneable clone.
  newType rules addImmutableDelegate: #parent1 valued: type rules.
  types
    doWithIndex:
      [| :type :index |
        newType rules
          addImmutableDelegate: ('parent' ; (index + 2 as: String) as: Symbol)
          valued: type rules
      ].
  newType
].

supertype@(Types Type traits) subsumes: subtype
"Returns whether the first type subsumes the second, by type-intersection."
[
  (supertype intersection: subtype) = subtype
].

_@(Types Type traits) representative
[
  Nil
].

_ satisfies: _@(Types Type traits)
"The default (safe) answer."
[
  False
].

Types addSlot: #Any valued: Types Type derive.
"Objects of type Any can be any value."
Types Any rules: Cloneable clone.

selector@(Symbol traits) inferOn: argumentTypes
"Take the selector and argument types and locate an inference rule,
and then return a type based on that as possible."
[| rule |
  rule: (selector
          findOn:
            (argumentTypes collect: [| :type | type rules])).
  rule
    ifNil: [Types Any]
    ifNotNil: [rule values: argumentTypes]
].

_ satisfies: _@(Types Any traits)
"Any object belongs to this type."
[
  True
].

_@(Types Type traits) subsumes: _@(Types Any traits)
[False].

_@(Types Any traits) intersection: type
[
  type
].

type intersection: _@(Types Any traits)
[
  type
].

any@(Types Any traits) union: _
[
  any
].

_ union: any@(Types Any traits)
[
  any
].

Types addSlot: #None valued: Types Any derive.

"Objects of type None have no value (Nil) or represent an error."

_@Nil satisfies: _@(Types None traits)
[
  True
].

_@(Types Type traits) subsumes: _@(Types None traits)
[True].

"Currently omitted due to a lack of an Error traits.
_@(Error traits) satisfies: _@(Types None traits)
[
  True
]."

_@(Types None traits) complement
[
  Types Any
].

_@(Types Any traits) complement
[
  Types None
].

_@(Types None traits) union: type
[
  type
].

type union: _@(Types None traits)
[
  type
].

none@(Types None traits) intersection: _
[
  none
].

_ intersection: none@(Types None traits)
[
  none
].

Types addSlot: #Not valued: Types Any derive.
"A complement of a type, which may reduce itself automatically."
Types Not addSlot: #argument valued: Types Any clone.
"The complemented type."

type@(Types Type traits) complement
"The most generic type-complementation."
[| newType |
  newType: Types Not clone.
  newType argument: type.
  newType
].

type@(Types Not traits) complement
"A simple reduction: the complement of a complement is the original."
[
  type argument
].

not@(Types Not traits) union: type
[
  not argument = type
    ifTrue: [Types Any]
    ifFalse: [resend]
].

not@(Types Not traits) intersection: type
[
  not argument = type
    ifTrue: [Types None]
    ifFalse: [resend]
].

Types addSlot: #Union valued: Types Any derive.
"A union of types, which may reduce itself automatically."
Types Union addSlot: #args valued: ExtensibleSequence newEmpty.
"The arguments of the Union."

union@(Types Union traits) copy
[| newU |
  newU: union clone.
  newU args: union args copy.
  newU
].

union@(Types Union traits) representative
"Pick a representative from a random argument."
[
  (union args atRandom) representative
].

type1@(Types Type traits) union: type2@(Types Type traits)
"The most generic method for union."
[| newUnion |
  newUnion: Types Union clone.
  newUnion args: ({type1. type2} as: newUnion args).
  newUnion
].

union@(Types Union traits) union: type
[| newU |
  newU: union copy.
  newU args add: type.
  newU
].

union1@(Types Union traits) union: union2@(Types Union traits)
[| newU |
  newU: union1 copy.
  newU args addAll: union2 args.
  newU
].

union@(Types Union traits) subsumes: type
"Unions subsume their arguments."
[
  (union args
     anySatisfy: [| :arg | arg = type or: [arg subsumes: type]])
    or: [resend]
].

Types addSlot: #Intersection valued: Types Any derive.
"An intersection of types, which may reduce itself automatically."
Types Intersection addSlot: #args valued: ExtensibleSequence newEmpty.
"The arguments of the Intersection."

intersection@(Types Intersection traits) copy
[| newI |
  newI: intersection clone.
  newI args: intersection args copy.
  newI
].

type1@(Types Type traits) intersection: type2@(Types Type traits)
"The most generic method for intersection."
[| newType |
  newType: Types Intersection clone.
  newType args: ({type1. type2} as: newType args).
  newType
].

intersection@(Types Intersection traits) intersection: type
[| newI |
  newI: intersection copy.
  newI args add: type.
  newI
].

int1@(Types Intersection traits) intersection: int2@(Types Intersection traits)
[| newI |
  newI: intersection copy.
  newI args addAll: int2 args.
  newI
].

type subsumes: intersection@(Types Intersection traits)
"Each argument of an intersection subsumes it."
[
  (intersection args
     anySatisfy: [| :arg | arg = type or: [arg subsumes: type]])
    or: [resend]
].

Types addSlot: #Clone valued: Types Any derive.
Types Clone addSlot: #prototype.

"The Clone type represents clone families, tracking some original prototype."

x@(Types Clone traits) = y@(Types Clone traits)
[
  x prototype == y prototype
].

c@(Types Clone traits) of: prototype
"Create a new Clone type using the given object as a prototype."
[| newC |
  newC: c clone.
  newC prototype: prototype.
  newC
].

x@(Types Clone traits) union: y@(Types Clone traits)
[
  x prototype == y prototype 
    ifTrue: [x]
    ifFalse: [Types Any]
].

x@(Types Clone traits) intersection: y@(Types Clone traits)
[
  x prototype == y prototype
    ifTrue: [x]
    ifFalse: [Types None]
].

c@(Types Clone traits) representative
"Use the prototype as a representative of the Clone family."
[
  c prototype
].

Types addSlot: #Range valued: Types Any derive.
Types Range addSlot: #type.
Types Range addSlot: #start.
Types Range addSlot: #end.

"Ranges are parametrizable types over linearly-ordered domains (Magnitudes,
such as Numbers, Integers, and Characters(?)). They express a range of values."

range@(Types Range traits) representative
"Use the base type's representative."
[
  range type representative
].

x@(Types Range traits) = y@(Types Range traits)
"Equal Range types must have a same basis and boundaries."
[
  x type = y type
    and: [x start = y start]
    and: [x end = y end]
].

range@(Types Range traits) of: type from: start to: end
"Create a new Range type for the type, between the given boundaries."
[| newRange |
  newRange: range clone.
  newRange rules: range rules clone.
  newRange rules parent: type rules.
  newRange type: type.
  newRange start: start.
  newRange end: end.
  newRange
].

x@(Types Range traits) union: y@(Types Range traits)
"Create a new Range type over the base Types' union if applicable."
"TODO: this depends on x and y's boundaries being comparable. Fixing this
may be necessary."
[| type |
  type: (x type union: y type).
  type == Types Any ifTrue: [^ Types Any].
  x 
    of: type
    from: (x start min: y start)
    to: (x end max: y end)
].

x@(Types Range traits) intersection: y@(Types Range traits)
"Create a new Range type over the base Types' intersection if applicable."
"TODO: this depends on x and y's boundaries being comparable. Fix this."
[| type start end |
  type: (x type intersection: y type).
  type == Types None ifTrue: [^ Types None].
  start: (x start min: y start).
  end: (x end max: y end).
  start > end ifTrue: [^ Types None].
  x of: type from: start to: end
].

Types addSlot: #Member valued: Types Any derive.
Types Member addSlot: #elements.

"The Member type represents the elements of some finite set."

member@(Types Member traits) representative
"Take any element and call it a representative."
[
  member elements anyOne
].

x@(Types Member traits) = y@(Types Member traits)
"Equality as a collection."
[
  x elements = y elements
].

member@(Types Member traits) of: elements
"Create a new Member type over the given collection, implicitly copying it
with as:-conversion."
[| newMember representative |
  representative: elements anyOne.
  elements
    do:
      [| :element |
        element traits == representative traits
          ifFalse: [^ Types Any]
      ].
  newMember: member clone.
  newMember elements: (elements as: Set).
  newMember
].

x@(Types Member traits) union: y@(Types Member traits)
[
  x elements anyOne traits == y elements anyOne traits
    ifTrue: [x of: (x elements \/ y elements)]
    ifFalse: [Types Any]
].

x@(Types Member traits) intersection: y@(Types Member traits)
[
  x elements anyOne traits == y elements anyOne traits
    ifTrue: [x of: (x elements /\ y elements)]
    ifFalse: [Types None]
].

Types addSlot: #Singleton valued: Types Any derive.
Types Singleton addSlot: #identity.

"The singleton type, representing single objects only."

singleton@(Types Singleton traits) representative
"Answer the only possible element."
[
  singleton identity
].

x@(Types Singleton traits) = y@(Types Singleton traits)
"Equality by the one element's unique identity."
[
  x identity == y identity
].

singleton@(Types Singleton traits) of: identity
"Create a new Singleton type over the given object."
[| newSingleton |
  newSingleton: singleton clone.
  newSingleton identity: identity.
  newSingleton
].

member@(Types Member traits) union: singleton@(Types Singleton traits)
"Create a new type between a Member and a Singleton type, a new Member type
or the existing one if the Member type is a supertype of the singleton."
[| newMember |
  (member elements includes: singleton) ifTrue: [^ member].
  member elements anyOne traits == singleton identity traits
    ifFalse: [^ Types Any].
  newMember: member clone.
  newMember elements: member elements copy.
  newMember elements add: singleton identity.
  newMember
].

singleton@(Types Singleton traits) union: member@(Types Member traits)
"Commutation."
[
  member union: singleton
].

x@(Types Singleton traits) union: y@(Types Singleton traits)
"Create a new Member type of the two as necessary."
[
  x identity == y identity 
    ifTrue: [x]
    ifFalse: 
      [
        x identity traits == y identity traits
         ifTrue: [Types Member of: { x identity. y identity }]
         ifFalse: [Types Any]
      ]
].

member@(Types Member traits) intersection: singleton@(Types Singleton traits)
"Based on inclusion of the Singleton in the Member, return the Singleton or
None type as intersection."
[
  (member elements includes: singleton) ifTrue: [singleton] ifFalse: [Types None]
].

singleton@(Types Singleton traits) intersection: member@(Types Member traits)
"Commutation."
[ 
  member intersection: singleton 
]. 

x@(Types Singleton traits) intersection: y@(Types Singleton traits)
"Return the intersection, None if not equal, either one if equal."
[ 
  x identity == y identity 
    ifTrue: [x]
    ifFalse: [Types None] 
].

Types addSlot: #Array valued: Types Any derive.
Types Array addSlot: #type.

"Array types are parametrized by their element types, and cover arrays of all
lengths with that element type."

array@(Types Array traits) representative
"Answer an empty Array literal."
"TODO: parametrize even the empty array?"
[
  {}
].

array@(Types Array traits) of: type
"Answer a new Array type over the given element type."
[| newArray |
  newArray: array clone.
  newArray type: type.
  newArray
].

x@(Types Array traits) = y@(Types Array traits)
"Array types are equal simple on their underlying types."
[
  x type = y type
].

x@(Types Array traits) union: y@(Types Array traits)
"The union of Array types is the Array type of the union of the element types."
[
  x of: (x type union: y type)
].

x@(Types Array traits) intersection y@(Types Array traits)
"The intersection of Array types is the Array type of the intersection of the
element types, or None if the intersection is None."
[| type | 
  type: (x type intersection: y type).
  type = Types None ifTrue: [^ Types None].
  x of: type
].

Types addSlot: #Block valued: Types Any derive.
Types Block addSlot: #argumentTypes.
Types Block addSlot: #resultType.

"The Block type represents code closures, with input types and a return type,
optionally."

block@(Types Block traits) representative
"The representative block is the do-nothing block."
[
  []
].

block@(Types Block traits) from: argumentTypes to: resultType
"Return a new Block type with the given type-signature."
[| newBlock |
  newBlock: block clone.
  newBlock argumentTypes: (argumentTypes as: Array).
  newBlock resultType: resultType.
  newBlock
].

x@(Types Block traits) = y@(Types Block traits)
"Equal Block types must have equal type-signatures."
[
  x resultType = y resultType and: [x argumentTypes = y argumenTypes]
].

x@(Types Block traits) union: y@(Types Block traits)
"x and y must have the same number of arguments. This returns a Block type
with a union of their signature types."
[
  x argumentTypes size = y argumentTypes size ifFalse: [^ Types Any].
  x 
    from:
      (x argumentTypes
        with: y argumentTypes
        collect:
          [| :t :u | t union: u])
    to: (x resultType union: y resultType)
].

x@(Types Block traits) intersection: y@(Types Block traits)
"x and y must have the same number of arguments. This returns a Block type
with an intersection of their signature types."
[| resultType |
  x argumentTypes size = y argumentTypes size ifFalse: [^ Types None].
  resultType: (x resultType intersection: y resultType).
  resultType == Types None ifTrue: [^ Types None].
  x 
    from:
      (x argumentTypes
        with: y argumentTypes
        collect:
          [| :t :u | t intersection: u])
    to: resultType
].