# frozen_string_literal: true
require "uri"
require "value_semantics"
require "dhall/util"
require "dhall/visitor"
module Dhall
class Expression
def call(*args)
args.reduce(self) { |f, arg|
Application.new(function: f, arguments: [arg])
}.normalize
end
def to_proc
method(:call).to_proc
end
def fetch(k)
RecordSelection.new(record: self, selector: k)
end
def slice(*keys)
RecordProjection.new(record: self, selectors: keys)
end
def +(other)
Operator::Plus.new(lhs: self, rhs: other)
end
def *(other)
case other
when Natural
other * self
else
Operator::Times.new(lhs: self, rhs: other)
end
end
def <<(other)
Operator::TextConcatenate.new(lhs: self, rhs: other)
end
def concat(other)
Operator::ListConcatenate.new(lhs: self, rhs: other)
end
def &(other)
if self == other
self
elsif other.is_a?(Bool)
other & self
else
Operator::And.new(lhs: self, rhs: other)
end
end
def |(other)
if self == other
self
elsif other.is_a?(Bool)
other | self
else
Operator::Or.new(lhs: self, rhs: other)
end
end
def dhall_eq(other)
if self == other
Bool.new(value: true)
elsif other.is_a?(Bool)
other.dhall_eq(self)
else
Operator::Equal.new(lhs: self, rhs: other)
end
end
def deep_merge(other)
case other
when EmptyRecord
other.deep_merge(self)
else
Operator::RecursiveRecordMerge.new(lhs: self, rhs: other)
end
end
def merge(other)
case other
when EmptyRecord
other.merge(self)
else
Operator::RightBiasedRecordMerge.new(lhs: self, rhs: other)
end
end
def deep_merge_type(other)
case other
when EmptyRecordType
other.deep_merge_type(self)
else
Operator::RecursiveRecordTypeMerge.new(lhs: self, rhs: other)
end
end
end
class Application < Expression
include(ValueSemantics.for_attributes do
function Expression
arguments Util::ArrayOf.new(Expression, min: 1)
end)
end
class Function < Expression
include(ValueSemantics.for_attributes do
var ::String
type Either(nil, Expression) # nil is not allowed in proper Dhall
body Expression
end)
def self.of_arguments(*types, body:)
types.reverse.reduce(body) do |inner, type|
new(
var: "_",
type: type,
body: inner
)
end
end
def call(*args)
return super if args.length > 1
body.substitute(
Variable.new(name: var),
args.first.shift(1, var, 0)
).shift(-1, var, 0).normalize
end
end
class Forall < Function; end
class Bool < Expression
include(ValueSemantics.for_attributes do
value Bool()
end)
def reduce(when_true, when_false)
value ? when_true : when_false
end
def &(other)
reduce(other, with(value: false))
end
def |(other)
reduce(with(value: true), other)
end
def dhall_eq(other)
reduce(other, super)
end
end
class Variable < Expression
include(ValueSemantics.for_attributes do
name String, default: "_"
index (0..Float::INFINITY), default: 0
end)
def self.[](name, index=0)
new(name: name, index: index)
end
end
class Operator < Expression
include(ValueSemantics.for_attributes do
lhs Expression
rhs Expression
end)
class Or < Operator; end
class And < Operator; end
class Equal < Operator; end
class NotEqual < Operator; end
class Plus < Operator; end
class Times < Operator; end
class TextConcatenate < Operator; end
class ListConcatenate < Operator; end
class RecursiveRecordMerge < Operator; end
class RightBiasedRecordMerge < Operator; end
class RecursiveRecordTypeMerge < Operator; end
class ImportFallback < Operator; end
end
class List < Expression
include(ValueSemantics.for_attributes do
elements ArrayOf(Expression)
end)
def self.of(*args)
List.new(elements: args)
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
def concat(other)
if other.is_a?(List) && !other.is_a?(EmptyList)
with(elements: elements + other.elements)
else
super
end
end
end
class EmptyList < List
include(ValueSemantics.for_attributes do
type Expression
end)
def map(type: nil)
type.nil? ? self : with(type: type)
end
def reduce(z)
z
end
def length
0
end
def first
OptionalNone.new(type: type)
end
def last
OptionalNone.new(type: type)
end
def reverse
self
end
def concat(other)
other
end
end
class Optional < Expression
include(ValueSemantics.for_attributes do
value Expression
type Either(nil, Expression), default: nil
end)
def reduce(_, &block)
block[value]
end
end
class OptionalNone < Optional
include(ValueSemantics.for_attributes do
type Expression
end)
def reduce(z)
z
end
end
class Merge < Expression
include(ValueSemantics.for_attributes do
record Expression
input Expression
type Either(Expression, nil)
end)
end
class RecordType < Expression
include(ValueSemantics.for_attributes do
record Util::HashOf.new(::String, Expression, min: 1)
end)
def deep_merge_type(other)
return super unless other.is_a?(RecordType)
with(record: Hash[record.merge(other.record) { |_, v1, v2|
v1.deep_merge_type(v2)
}.sort])
end
def ==(other)
other.respond_to?(:record) && record.to_a == other.record.to_a
end
def eql?(other)
self == other
end
end
class EmptyRecordType < Expression
include(ValueSemantics.for_attributes {})
def deep_merge_type(other)
other
end
end
class Record < Expression
include(ValueSemantics.for_attributes do
record Util::HashOf.new(::String, Expression, min: 1)
end)
def fetch(k, default=nil, &block)
record.fetch(k, *default, &block)
end
def slice(*keys)
if record.respond_to?(:slice)
with(record: record.slice(*keys))
else
with(record: record.select { |k, _| keys.include?(k) })
end
end
def deep_merge(other)
return super unless other.is_a?(Record)
with(record: Hash[record.merge(other.record) { |_, v1, v2|
v1.deep_merge(v2)
}.sort])
end
def merge(other)
return super unless other.is_a?(Record)
with(record: Hash[record.merge(other.record).sort])
end
def ==(other)
other.respond_to?(:record) && record.to_a == other.record.to_a
end
def eql?(other)
self == other
end
end
class EmptyRecord < Expression
include(ValueSemantics.for_attributes {})
def fetch(k, default=nil, &block)
{}.fetch(k, *default, &block)
end
def slice(*)
self
end
def deep_merge(other)
other
end
def merge(other)
other
end
end
class RecordSelection < Expression
include(ValueSemantics.for_attributes do
record Expression
selector ::String
end)
end
class RecordProjection < Expression
include(ValueSemantics.for_attributes do
record Expression
selectors Util::ArrayOf.new(::String, min: 1)
end)
end
class EmptyRecordProjection < Expression
include(ValueSemantics.for_attributes do
record Expression
end)
end
class UnionType < Expression
include(ValueSemantics.for_attributes do
alternatives Util::HashOf.new(::String, Expression)
end)
def ==(other)
other.is_a?(UnionType) && alternatives.to_a == other.alternatives.to_a
end
def eql?(other)
self == other
end
def fetch(k)
remains = with(alternatives: alternatives.dup.tap { |r| r.delete(k) })
Function.new(
var: k,
type: alternatives.fetch(k),
body: Union.new(
tag: k,
value: Variable.new(name: k),
alternatives: remains
)
)
end
end
class Union < Expression
include(ValueSemantics.for_attributes do
tag ::String
value Expression
alternatives UnionType
end)
end
class If < Expression
include(ValueSemantics.for_attributes do
predicate Expression
self.then Expression
self.else Expression
end)
end
class Number < Expression
end
class Natural < Number
include(ValueSemantics.for_attributes do
value (0..Float::INFINITY)
end)
def +(other)
if other.is_a?(Natural)
with(value: value + other.value)
else
super
end
end
def *(other)
return self if zero?
if other.is_a?(Natural)
with(value: value * other.value)
else
super
end
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
include(ValueSemantics.for_attributes do
value ::Integer
end)
def to_s
"#{value >= 0 ? "+" : ""}#{value}"
end
end
class Double < Number
include(ValueSemantics.for_attributes do
value ::Float
end)
def to_s
value.to_s
end
end
class Text < Expression
include(ValueSemantics.for_attributes do
value ::String
end)
def <<(other)
if other.is_a?(Text)
with(value: value + other.value)
else
super
end
end
end
class TextLiteral < Expression
include(ValueSemantics.for_attributes do
chunks ArrayOf(Expression)
end)
end
class Import < Expression
def initialize(integrity_check, import_type, path)
@integrity_check = integrity_check
@import_type = import_type
@path = path
end
class URI
include(ValueSemantics.for_attributes do
headers Either(nil, Expression)
authority ::String
path ArrayOf(::String)
query Either(nil, ::String)
fragment Either(nil, ::String)
end)
def initialize(headers, authority, *path, query, fragment)
super(
headers: headers,
authority: authority,
path: path,
query: query,
fragment: fragment
)
end
def self.from_uri(uri)
(uri.scheme == "https" ? Https : Http).new(
nil,
"#{uri.host}:#{uri.port}",
*uri.path.split(/\//)[1..-1],
uri.query,
nil
)
end
def uri
URI("#{scheme}://#{authority}/#{path.join("/")}?#{query}")
end
end
class Http < URI
def resolve(resolver)
resolver.resolve_http(self)
end
def scheme
"http"
end
end
class Https < URI
def resolve(resolver)
resolver.resolve_https(self)
end
def scheme
"https"
end
end
class Path
include(ValueSemantics.for_attributes do
path ArrayOf(::String)
end)
def initialize(*path)
super(path: path)
end
def self.from_string(s)
parts = s.split(/\//)
if parts.first == ""
AbsolutePath.new(*parts[1..-1])
elsif parts.first == "~"
RelativeToHomePath.new(*parts[1..-1])
else
RelativePath.new(*parts)
end
end
def resolve(resolver)
resolver.resolve_path(self)
end
def to_s
pathname.to_s
end
end
class AbsolutePath < Path
def pathname
Pathname.new("/").join(*path)
end
def to_uri(scheme, authority)
scheme.new(nil, authority, *path, nil, nil)
end
end
class RelativePath < Path
def pathname
Pathname.new(".").join(*path)
end
end
class RelativeToParentPath < Path
def pathname
Pathname.new("..").join(*path)
end
end
class RelativeToHomePath < Path
def pathname
Pathname.new("~").join(*@path)
end
end
class EnvironmentVariable
def initialize(var)
@var = var
end
def value
ENV.fetch(@var)
end
def resolve(resolver)
val = ENV.fetch(@var)
if val =~ /\Ahttps?:\/\//
URI.from_uri(URI(value))
else
Path.from_string(val)
end.resolve(resolver)
end
end
class MissingImport
def resolve(*)
Promise.new.reject(ImportFailedException.new("missing"))
end
end
class IntegrityCheck
def initialize(protocol, data)
@protocol = protocol
@data = data
end
end
end
class Let < Expression
include(ValueSemantics.for_attributes do
var ::String
assign Expression
type Either(nil, Expression)
end)
end
class LetBlock < Expression
include(ValueSemantics.for_attributes do
lets ArrayOf(Let)
body Expression
end)
end
class TypeAnnotation < Expression
include(ValueSemantics.for_attributes do
value Expression
type Expression
end)
end
end