Class: Dhall::TypeChecker::Variable

Inherits:
Object
  • Object
show all
Defined in:
lib/dhall/typecheck.rb

Constant Summary collapse

BUILTIN =
{
  "Type"     => Dhall::Variable["Kind"],
  "Kind"     => Dhall::Variable["Sort"],
  "Bool"     => Dhall::Variable["Type"],
  "Natural"  => Dhall::Variable["Type"],
  "Integer"  => Dhall::Variable["Type"],
  "Double"   => Dhall::Variable["Type"],
  "Text"     => Dhall::Variable["Type"],
  "List"     => Dhall::Forall.of_arguments(
    Dhall::Variable["Type"],
    body: Dhall::Variable["Type"]
  ),
  "Optional" => Dhall::Forall.of_arguments(
    Dhall::Variable["Type"],
    body: Dhall::Variable["Type"]
  ),
  "None"     => Dhall::Forall.new(
    var:  "A",
    type: Dhall::Variable["Type"],
    body: Dhall::Application.new(
      function: Dhall::Variable["Optional"],
      argument: Dhall::Variable["A"]
    )
  )
}.freeze

Instance Method Summary collapse

Constructor Details

#initialize(var) ⇒ Variable

Returns a new instance of Variable.



83
84
85
# File 'lib/dhall/typecheck.rb', line 83

def initialize(var)
  @var = var
end

Instance Method Details

#annotate(context) ⇒ Object

Raises:

  • (TypeError)


113
114
115
116
117
118
119
120
# File 'lib/dhall/typecheck.rb', line 113

def annotate(context)
  raise TypeError, "Sort has no Type, Kind, or Sort" if @var.name == "Sort"

  Dhall::TypeAnnotation.new(
    value: @var,
    type:  BUILTIN.fetch(@var.name) { context.fetch(@var) }
  )
end