M .rubocop.yml => .rubocop.yml +3 -0
@@ 51,3 51,6 @@ Naming/UncommunicativeMethodParamName:
List/ParenthesesAsGroupedExpression:
Enabled: false
+
+Lint/UnusedMethodArgument:
+ AllowUnusedKeywordArguments: true
A lib/dhall/.ast.rb.swp => lib/dhall/.ast.rb.swp +0 -0
A lib/dhall/.binary.rb.swp => lib/dhall/.binary.rb.swp +0 -0
A lib/dhall/.builtins.rb.swp => lib/dhall/.builtins.rb.swp +0 -0
A lib/dhall/.normalize.rb.swp => lib/dhall/.normalize.rb.swp +0 -0
M lib/dhall/ast.rb => lib/dhall/ast.rb +110 -22
@@ 2,26 2,34 @@
require "value_semantics"
+require "dhall/util"
+
module Dhall
class Expression
def map_subexpressions(&_)
# For expressions with no subexpressions
self
end
- end
- class Application < Expression
- def initialize(f, *args)
- if args.empty?
- raise ArgumentError, "Application requires at least one argument"
- end
+ def call(*args)
+ args.reduce(self) { |f, arg|
+ Application.new(function: f, arguments: [arg])
+ }.normalize
+ end
- @f = f
- @args = args
+ def to_proc
+ method(:call).to_proc
end
+ end
+
+ class Application < Expression
+ include(ValueSemantics.for_attributes do
+ function Expression
+ arguments Util::ArrayOf.new(Expression, min: 1)
+ end)
def map_subexpressions(&block)
- self.class.new(block[@f], *@args.map(&block))
+ with(function: block[function], arguments: arguments.map(&block))
end
end
@@ 88,6 96,34 @@ module Dhall
def map_subexpressions(&block)
with(elements: elements.map(&block))
end
+
+ def type
+ # TODO: inferred element type
+ end
+
+ def map(type: nil, &block)
+ with(elements: elements.each_with_index.map(&block))
+ end
+
+ def reduce(z)
+ elements.reverse.reduce(z) { |acc, x| yield x, acc }
+ end
+
+ def length
+ elements.length
+ end
+
+ def first
+ Optional.new(value: elements.first, type: type)
+ end
+
+ def last
+ Optional.new(value: elements.last, type: type)
+ end
+
+ def reverse
+ with(elements: elements.reverse)
+ end
end
class EmptyList < List
@@ 98,30 134,50 @@ module Dhall
def map_subexpressions(&block)
with(type: block[@type])
end
- end
- class Optional < Expression
- def initialize(value, type=nil)
- raise TypeError, "value must not be nil" if value.nil?
+ def map(type: nil)
+ type.nil? ? self : with(type: type)
+ end
- @value = value
- @type = type
+ def reduce(z)
+ z
end
- def map_subexpressions(&block)
- self.class.new(block[@value], block[@type])
+ def length
+ 0
+ end
+
+ def first
+ OptionalNone.new(type: type)
+ end
+
+ def last
+ OptionalNone.new(type: type)
+ end
+
+ def reverse
+ self
end
end
- class OptionalNone < Optional
- def initialize(type)
- raise TypeError, "type must not be nil" if type.nil?
+ class Optional < Expression
+ include(ValueSemantics.for_attributes do
+ value Expression
+ type Either(nil, Expression), default: nil
+ end)
- @type = type
+ def map_subexpressions(&block)
+ with(value: block[value], type: type.nil? ? type : block[type])
end
+ end
+
+ class OptionalNone < Optional
+ include(ValueSemantics.for_attributes do
+ type Expression
+ end)
def map_subexpressions(&block)
- self.class.new(block[@type])
+ with(type: block[@type])
end
end
@@ 138,6 194,8 @@ module Dhall
end
class RecordType < Expression
+ attr_reader :record
+
def initialize(record)
@record = record
end
@@ 149,9 207,15 @@ module Dhall
block[@type]
)
end
+
+ def eql?(other)
+ record == other.record
+ end
end
class Record < Expression
+ attr_reader :record
+
def initialize(record)
@record = record
end
@@ 159,6 223,10 @@ module Dhall
def map_subexpressions(&block)
self.class.new(Hash[*@record.map { |k, v| [k, block[v]] }])
end
+
+ def eql?(other)
+ record == other.record
+ end
end
class RecordFieldAccess < Expression
@@ 251,6 319,26 @@ module Dhall
include(ValueSemantics.for_attributes do
value (0..Float::INFINITY)
end)
+
+ def to_s
+ value.to_s
+ end
+
+ def even?
+ value.even?
+ end
+
+ def odd?
+ value.odd?
+ end
+
+ def zero?
+ value.zero?
+ end
+
+ def pred
+ with(value: [0, value - 1].max)
+ end
end
class Integer < Number
M lib/dhall/binary.rb => lib/dhall/binary.rb +11 -7
@@ 2,6 2,9 @@
require "cbor"
+require "dhall/ast"
+require "dhall/builtins"
+
module Dhall
def self.from_binary(cbor_binary)
data = CBOR.decode(cbor_binary)
@@ 13,8 16,6 @@ module Dhall
end
def self.decode(expression)
- return expression if expression.is_a?(Expression)
-
BINARY.each do |match, use|
return use[expression] if expression.is_a?(match)
end
@@ 32,7 33,10 @@ module Dhall
class Application
def self.decode(f, *args)
- new(Dhall.decode(f), *args.map(&Dhall.method(:decode)))
+ new(
+ function: Dhall.decode(f),
+ arguments: args.map(&Dhall.method(:decode))
+ )
end
end
@@ 82,11 86,11 @@ module Dhall
class Optional
def self.decode(type, value=nil)
if value.nil?
- OptionalNone.new(Dhall.decode(type))
+ OptionalNone.new(type: Dhall.decode(type))
else
Optional.new(
- Dhall.decode(value),
- type.nil? ? type : Dhall.decode(type)
+ value: Dhall.decode(value),
+ type: type.nil? ? type : Dhall.decode(type)
)
end
end
@@ 208,7 212,7 @@ module Dhall
::TrueClass => ->(e) { Bool.new(value: e) },
::FalseClass => ->(e) { Bool.new(value: e) },
::Float => ->(e) { Double.new(value: e) },
- ::String => ->(e) { Variable.new(name: e) },
+ ::String => ->(e) { Builtins::ALL[e]&.new || Variable.new(name: e) },
::Integer => ->(e) { Variable.new(index: e) },
::Array => lambda { |e|
if e.length == 2 && e.first.is_a?(::String)
A lib/dhall/builtins.rb => lib/dhall/builtins.rb +265 -0
@@ 0,0 1,265 @@
+# frozen_string_literal: true
+
+require "dhall/ast"
+
+module Dhall
+ class Builtin < Expression
+ def ==(other)
+ self.class == other.class
+ end
+
+ def call(*args)
+ # Do not auto-normalize builtins to avoid recursion loop
+ args.reduce(self) do |f, arg|
+ Application.new(function: f, arguments: [arg])
+ end
+ end
+ end
+
+ module Builtins
+ # rubocop:disable Style/ClassAndModuleCamelCase
+
+ class Natural_build < Builtin
+ def fusion(arg, *bogus)
+ if bogus.empty? &&
+ arg.is_a?(Application) &&
+ arg.function == Natural_fold.new &&
+ arg.arguments.length == 1
+ arg.arguments.first
+ else
+ super
+ end
+ end
+
+ def call(arg)
+ arg.call(
+ Variable.new(name: "Natural"),
+ Function.new(
+ "_",
+ Variable.new(name: "Natural"),
+ Operator::Plus.new(
+ lhs: Variable.new(name: "_"),
+ rhs: Natural.new(value: 1)
+ )
+ ),
+ Natural.new(value: 0)
+ )
+ end
+ end
+
+ class Natural_even < Builtin
+ def call(nat)
+ if nat.is_a?(Natural)
+ Bool.new(value: nat.even?)
+ else
+ super
+ end
+ end
+ end
+
+ class Natural_fold < Builtin
+ def initialize(nat=nil, type=nil, f=nil)
+ @nat = nat
+ @type = type
+ @f = f
+ end
+
+ def call(arg)
+ if @nat.nil? && arg.is_a?(Natural)
+ Natural_fold.new(arg)
+ elsif !@nat.nil? && @type.nil?
+ Natural_fold.new(@nat, arg)
+ elsif !@nat.nil? && !@type.nil? && @f.nil?
+ Natural_fold.new(@nat, @type, arg)
+ elsif !@nat.nil? && !@type.nil? && !@f.nil?
+ if @nat.zero?
+ arg.normalize
+ else
+ @f.call(Natural_fold.new(@nat.pred, @type, @f).call(arg))
+ end
+ else
+ super
+ end
+ end
+ end
+
+ class Natural_isZero < Builtin
+ def call(nat)
+ if nat.is_a?(Natural)
+ Bool.new(value: nat.zero?)
+ else
+ super
+ end
+ end
+ end
+
+ class Natural_odd < Builtin
+ def call(nat)
+ if nat.is_a?(Natural)
+ Bool.new(value: nat.odd?)
+ else
+ super
+ end
+ end
+ end
+
+ class Natural_show < Builtin
+ def call(nat)
+ if nat.is_a?(Natural)
+ Text.new(value: nat.to_s)
+ else
+ super
+ end
+ end
+ end
+
+ class Natural_toInteger < Builtin
+ def call(nat)
+ if nat.is_a?(Natural)
+ Integer.new(value: nat.value)
+ else
+ super
+ end
+ end
+ end
+
+ class List_build < Builtin
+ def fusion(*args)
+ _, arg, = args
+ if arg.is_a?(Application) &&
+ arg.function.is_a?(Application) &&
+ arg.function.function == List_fold.new &&
+ arg.arguments.length == 1
+ arg.arguments.first
+ else
+ super
+ end
+ end
+ end
+
+ class List_fold < Builtin
+ def initialize(ltype=nil, list=nil, ztype=nil, f=nil)
+ @ltype = ltype
+ @list = list
+ @ztype = ztype
+ @f = f
+ end
+
+ def call(arg)
+ if @ltype.nil?
+ List_fold.new(arg)
+ elsif @list.nil?
+ List_fold.new(@ltype, arg)
+ elsif @ztype.nil?
+ List_fold.new(@ltype, @list, arg)
+ elsif @f.nil?
+ List_fold.new(@ltype, @list, @ztype, arg)
+ else
+ @list.reduce(arg, &@f).normalize
+ end
+ end
+ end
+
+ class List_head < Builtin
+ def call(arg)
+ if arg.is_a?(List)
+ arg.first
+ else
+ super
+ end
+ end
+ end
+
+ class List_indexed < Builtin
+ def call(arg)
+ if arg.is_a?(List)
+ arg.map(type: RecordType.new(
+ "index" => Variable.new(name: "Natural"),
+ "value" => arg.type
+ )) do |x, idx|
+ Record.new(
+ "index" => Natural.new(value: idx),
+ "value" => x
+ )
+ end
+ else
+ super
+ end
+ end
+ end
+
+ class List_last < Builtin
+ def call(arg)
+ if arg.is_a?(List)
+ arg.last
+ else
+ super
+ end
+ end
+ end
+
+ class List_length < Builtin
+ def call(arg)
+ if arg.is_a?(List)
+ Natural.new(value: arg.length)
+ else
+ super
+ end
+ end
+ end
+
+ class List_reverse < Builtin
+ def call(arg)
+ if arg.is_a?(List)
+ arg.reverse
+ else
+ super
+ end
+ end
+ end
+
+ class Optional_build < Builtin
+ def fusion(*args)
+ _, arg, = args
+ if arg.is_a?(Application) &&
+ arg.function.is_a?(Application) &&
+ arg.function.function == Optional_fold.new &&
+ arg.arguments.length == 1
+ arg.arguments.first
+ else
+ super
+ end
+ end
+ end
+
+ class Optional_fold < Builtin
+ end
+
+ class Text_show < Builtin
+ ENCODE = (Hash.new { |_, x| "\\u%04x" % x.ord }).merge(
+ "\"" => "\\\"",
+ "\\" => "\\\\",
+ "\b" => "\\b",
+ "\f" => "\\f",
+ "\n" => "\\n",
+ "\r" => "\\r",
+ "\t" => "\\t"
+ )
+
+ def call(arg)
+ if arg.is_a?(Text)
+ Text.new(
+ value: "\"#{arg.value.gsub(
+ /["\$\\\b\f\n\r\t\u0000-\u001F]/,
+ &ENCODE
+ )}\""
+ )
+ else
+ super
+ end
+ end
+ end
+
+ ALL = Hash[constants.map { |c| [c.to_s.tr("_", "/"), const_get(c)] }]
+ end
+end
M lib/dhall/normalize.rb => lib/dhall/normalize.rb +24 -0
@@ 1,13 1,37 @@
# frozen_string_literal: true
+require "dhall/builtins"
+
module Dhall
class Expression
def normalize
map_subexpressions(&:normalize)
end
+
+ def fusion(*); end
end
class Application
+ def normalize
+ return fuse.normalize if fuse
+ normalized = super
+ return normalized.fuse if normalized.fuse
+
+ if normalized.function.is_a?(Builtin)
+ return normalized.function.call(*normalized.arguments)
+ end
+
+ normalized
+ end
+
+ def fuse
+ if function.is_a?(Application)
+ @fused ||= function.function.fusion(*function.arguments, *arguments)
+ return @fused if @fused
+ end
+
+ @fused ||= function.fusion(*arguments)
+ end
end
class Function
A lib/dhall/util.rb => lib/dhall/util.rb +17 -0
@@ 0,0 1,17 @@
+# frozen_string_literal: true
+
+module Dhall
+ module Util
+ class ArrayOf < ValueSemantics::ArrayOf
+ def initialize(element_validator, min: 0, max: Float::INFINITY)
+ @min = min
+ @max = max
+ super(element_validator)
+ end
+
+ def ===(other)
+ super && other.length >= @min && other.length <= @max
+ end
+ end
+ end
+end
M test/normalization/beta/ListHeadEmptyB.dhallb => test/normalization/beta/ListHeadEmptyB.dhallb +0 -0
M test/normalization/beta/ListLastEmptyB.dhallb => test/normalization/beta/ListLastEmptyB.dhallb +0 -0
M test/normalization/beta/NaturalToIntegerB.dhallb => test/normalization/beta/NaturalToIntegerB.dhallb +1 -1
@@ 1,1 1,1 @@
-�e5.0.0lNatural/show>
\ No newline at end of file
+�e5.0.0qNatural/toInteger<
\ No newline at end of file
A test/normalization/beta/NoneA.dhallb => test/normalization/beta/NoneA.dhallb +1 -0
@@ 0,0 1,1 @@
+�e5.0.0dNone<
\ No newline at end of file
A test/normalization/beta/NoneB.dhallb => test/normalization/beta/NoneB.dhallb +1 -0
@@ 0,0 1,1 @@
+�e5.0.0dNone<
\ No newline at end of file
A test/normalization/beta/NoneNaturalA.dhallb => test/normalization/beta/NoneNaturalA.dhallb +1 -0
@@ 0,0 1,1 @@
+�e5.0.0�gNatural<
\ No newline at end of file
A test/normalization/beta/NoneNaturalB.dhallb => test/normalization/beta/NoneNaturalB.dhallb +1 -0
@@ 0,0 1,1 @@
+�e5.0.0�gNatural<
\ No newline at end of file
A test/normalization/beta/OptionalA.dhallb => test/normalization/beta/OptionalA.dhallb +1 -0
@@ 0,0 1,1 @@
+�e5.0.0hOptional<
\ No newline at end of file
A test/normalization/beta/OptionalB.dhallb => test/normalization/beta/OptionalB.dhallb +1 -0
@@ 0,0 1,1 @@
+�e5.0.0hOptional<
\ No newline at end of file
A test/normalization/beta/OptionalBuildA.dhallb => test/normalization/beta/OptionalBuildA.dhallb +1 -0
@@ 0,0 1,1 @@
+�e5.0.0nOptional/build<
\ No newline at end of file
A test/normalization/beta/OptionalBuildB.dhallb => test/normalization/beta/OptionalBuildB.dhallb +1 -0
@@ 0,0 1,1 @@
+�e5.0.0nOptional/build<
\ No newline at end of file
A test/normalization/beta/OptionalBuildFoldFusionA.dhallb => test/normalization/beta/OptionalBuildFoldFusionA.dhallb +0 -0
A test/normalization/beta/OptionalBuildFoldFusionB.dhallb => test/normalization/beta/OptionalBuildFoldFusionB.dhallb +1 -0
@@ 0,0 1,1 @@
+�e5.0.0ax<
\ No newline at end of file
A test/normalization/beta/OptionalBuildImplementationA.dhallb => test/normalization/beta/OptionalBuildImplementationA.dhallb +0 -0
A test/normalization/beta/OptionalBuildImplementationB.dhallb => test/normalization/beta/OptionalBuildImplementationB.dhallb +1 -0
@@ 0,0 1,1 @@
+�e5.0.0ax<
\ No newline at end of file
A test/normalization/beta/OptionalFoldA.dhallb => test/normalization/beta/OptionalFoldA.dhallb +1 -0
@@ 0,0 1,1 @@
+�e5.0.0mOptional/fold<
\ No newline at end of file
A test/normalization/beta/OptionalFoldB.dhallb => test/normalization/beta/OptionalFoldB.dhallb +1 -0
@@ 0,0 1,1 @@
+�e5.0.0mOptional/fold<
\ No newline at end of file
A test/normalization/beta/OptionalFoldNoneA.dhallb => test/normalization/beta/OptionalFoldNoneA.dhallb +0 -0
A test/normalization/beta/OptionalFoldNoneB.dhallb => test/normalization/beta/OptionalFoldNoneB.dhallb +1 -0
@@ 0,0 1,1 @@
+�e5.0.0ax<
\ No newline at end of file
A test/normalization/beta/OptionalFoldSomeA.dhallb => test/normalization/beta/OptionalFoldSomeA.dhallb +0 -0
A test/normalization/beta/OptionalFoldSomeB.dhallb => test/normalization/beta/OptionalFoldSomeB.dhallb +1 -0
@@ 0,0 1,1 @@
+�e5.0.0ax<
\ No newline at end of file
A test/normalization/beta/SomeNormalizeArgumentsA.dhallb => test/normalization/beta/SomeNormalizeArgumentsA.dhallb +1 -0
@@ 0,0 1,1 @@
+�e5.0.0����axay<
\ No newline at end of file
A test/normalization/beta/SomeNormalizeArgumentsB.dhallb => test/normalization/beta/SomeNormalizeArgumentsB.dhallb +1 -0
@@ 0,0 1,1 @@
+�e5.0.0��ax<
\ No newline at end of file
M test/normalization/beta/TextShowAllEscapesA.dhallb => test/normalization/beta/TextShowAllEscapesA.dhallb +0 -0
M test/normalization/beta/TextShowAllEscapesB.dhallb => test/normalization/beta/TextShowAllEscapesB.dhallb +1 -1
@@ 1,1 1,1 @@
-�e5.0.0�x("\"\u0024\\\b\f\n\r\tツa\u00A0b\u00A0c">
\ No newline at end of file
+�e5.0.0�x("\"\u0024\\\b\f\n\r\tツa\u0007b\u0010c"<
\ No newline at end of file