lobby ensureNamespace: #Types.
Types addImmutableDelegate: #lobby valued: lobby.
"This ensures that type annotation expressions can occur in this namespace and
be arbitrary."

Types addPrototype: #Type derivedFrom: {Cloneable}.
"Types are Slate's basic type system for minimal inference purposes.
A type's rules object delegates to its supertypes' rules objects."
Types Type addSlot: #rules valued: (Cloneable clone removeSlot: #traits).
"KLUGE: The rules object is a faux-Cloneable object to avoid name clashes
with the methods being defined on it. After instantiation and initialize 
its traits slot is removed. Any further dispatches on it must be done 
via sendTo:through:."

type@(Types Type traits) clone
[| newType |
  newType: resend.
  newType rules: (#clone sendTo: {type rules} through: {Cloneable}).
  newType
].

type@(Types Type traits) derive
"Arrange for and return a new subtype."
[| newType |
  newType: resend.
  "Use the canonical prototype to avoid dealing with the effects on rules."
  newType rules: Cloneable clone.
  newType rules addImmutableDelegate: #parent1 valued: type rules.
  newType rules removeSlot: #traits.
  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.
  "Use the canonical prototype to avoid dealing with the effects on rules."
  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].
  newTypes rules removeSlot: #traits.
  newType
].

selector@(Symbol traits) inferOn: types
"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: (types collect: [| :type | type rules])).
  rule
    ifNil: [Types Any]
    ifNotNil: [rule applyTo: types]
].

x@(Types Type traits) union: y@(Types Type traits)
"Returns the type-theoretic union of the two types. Everything satisfying
either of the component types should satisfy the union."
[
  x == y
    ifTrue: [x]
    ifFalse: [Types Any]
].

x@(Types Type traits) intersection: y@(Types Type traits)
"Returns the type-theoretic intersection of the two types. Everything
satisfying both of the component types should satisfy the intersection."
[
  x == y
    ifTrue: [x]
    ifFalse: [Types None]
].

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
"Return some representative object satisfying the Type."
[
  Nil
].

_ satisfies: _@(Types Type traits)
"The default (safe) answer to whether an object satisfies, or belongs to,
a Type."
[False].

Types addPrototype: #Any derivedFrom: {Types Type}.
"Objects of type Any can be any value."

_ 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 addPrototype: #None derivedFrom: {Types Any}.
"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 None traits) union: type
[type].

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

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

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

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

type@(Types Any traits) complement
"The most generic type-complementation."
[
  type == Types Any
    ifTrue: [Types None]
    ifFalse:
      [| 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 addPrototype: #Union derivedFrom: {Types Any}.
"A union of types, which may reduce itself automatically."
Types Union addSlot: #args valued: ExtensibleArray 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 Any traits) union: type2@(Types Any traits)
"The most generic method for union."
[| newUnion |
  (type1 == Types Any
    or: [type2 == Types Any])
    ifTrue: [^ Types Any].
  type1 == Types None
    ifTrue: [^ type2].
  type2 == Types None
    ifTrue: [^ type1].
  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 addPrototype: #Intersection derivedFrom: {Types Any}.
"An intersection of types, which may reduce itself automatically."
Types Intersection addSlot: #args valued: ExtensibleArray newEmpty.
"The arguments of the Intersection."

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

type1@(Types Any traits) intersection: type2@(Types Any traits)
"The most generic method for intersection."
[| newType |
  (type1 == Types None
    or: [type2 == Types None])
    ifTrue: [^ Types None].
  type1 == Types Any
    ifTrue: [^ type2].
  type2 == Types Any
    ifTrue: [^ type1].
  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 addPrototype: #Clone derivedFrom: {Types Any}.
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 addPrototype: #Range derivedFrom: {Types Any}.
"Ranges are parametrizable types over linearly-ordered domains (Magnitudes,
such as Numbers, Integers, and Characters(?)). They express a range of values."
Types Range addSlot: #type.
Types Range addSlot: #start.
Types Range addSlot: #end.

range@(Types Range traits) representative
"Use the range's start, coerced to be of the same prototype as the base type's representative."
[
  range start as: 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 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 addPrototype: #Member derivedFrom: {Types Any}.
"The Member type represents the elements of some finite set."
Types Member addSlot: #elements valued: {}.

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 isSameAs: representative)
          ifFalse: [^ Types Any]].
  newMember: member clone.
  newMember elements: (elements as: Set).
  newMember
].

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

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

Types addPrototype: #Singleton derivedFrom: {Types Any}.
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 isSameAs: singleton identity)
    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 isSameAs: y identity)
         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 addPrototype: #Array derivedFrom: {Types Any}.
"Array types are parametrized by their element types, and cover arrays of all
lengths with that element type."
Types Array addSlot: #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 addPrototype: #Block derivedFrom: {Types Any}.
"The Block type represents code closures, with input types and a return type,
optionally."
Types Block addSlot: #argumentTypes.
Types Block addSlot: #resultType.

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 argumentTypes]
].

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
].