Class: Dhall::TypeChecker::Assertion

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

Instance Method Summary collapse

Constructor Details

#initialize(expr) ⇒ Assertion

Returns a new instance of Assertion.



1040
1041
1042
1043
 
# File 'lib/dhall/typecheck.rb', line 1040

def initialize(expr)
  @expr = expr
  @type = expr.type
end

Instance Method Details

#annotate(context) ⇒ Object 



1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
 
# File 'lib/dhall/typecheck.rb', line 1045

def annotate(context)
  TypeChecker.assert @type, Dhall::Operator::Equivalent,
                     "assert expected === got: #{@type.class}"

  TypeChecker.assert_type @type, Builtins[:Type],
                          "=== expected to have type Type",
                          context: context

  TypeChecker.assert @type.lhs.normalize.to_binary,
                     @type.rhs.normalize.to_binary,
                     "assert equivalence not equivalent"

  @expr.with(type: @type.normalize)
end