From e1bef6ce2386a214fd62d7b1119cdd31e191e512 Mon Sep 17 00:00:00 2001
From: Philipp Panzer <philipp.panzer@fau.de>
Date: Tue, 5 Mar 2019 15:13:44 +0100
Subject: [PATCH] add unions
---
README.md | 5 +++-
lib/DhallishGrammar.treetop | 42 ++++++++++++++++++++++++++++
lib/ast.rb | 56 +++++++++++++++++++++++++++++++++++++
lib/types.rb | 46 ++++++++++++++++++++++++++++--
4 files changed, 146 insertions(+), 3 deletions(-)
diff --git a/README.md b/README.md
index 2b788d0..97b4901 100644
--- a/README.md
+++ b/README.md
@@ -32,4 +32,7 @@ ruby ./tests/test.rb
- [ ] disallow Type Names like `Natural` or `let` as labels
- [ ] more tests and tests for expected failure
- [ ] "n-1": currently interpreted as label, but should be a subtraction (sometimes)
-- [ ] Warum funktionieren Typannotationen in lets mit verschiedenen Typvariablen?
+- [ ] Bignums for Integers?
+- [ ] Multi Line strings
+- [ ] quoted labels
+- [ ] MORE UNICODE!
diff --git a/lib/DhallishGrammar.treetop b/lib/DhallishGrammar.treetop
index f88c58e..875427a 100644
--- a/lib/DhallishGrammar.treetop
+++ b/lib/DhallishGrammar.treetop
@@ -166,6 +166,46 @@ grammar DhallishGrammar
}
end
+ ## Union Literals
+ rule union_literal_one_member
+ "<" space? label space? "=" space? expression ">"
+ end
+
+ rule union_literal
+ "<" space? start:(lb:label space? ":" space? type:expression space? "|" space?)* lb:label space? "=" space? expr:expression tail:(space? "|" space? lb:label space? ":" space? type:expression)* space? ">"
+ {
+ def to_node(ctx)
+ typed_labels = {}
+ start.elements.each { |node|
+ typed_labels[node.lb.text_value] = node.type.to_node(ctx)
+ }
+ tail.elements.each { |node|
+ typed_labels[node.lb.text_value] = node.type.to_node(ctx)
+ }
+ Dhallish::Ast::UnionLiteral.new(typed_labels, lb.text_value, expr.to_node(ctx))
+ end
+ }
+ end
+
+ rule empty_union_type_literal
+ "<" space? ">"
+ end
+
+ rule union_type_literal
+ empty_union_type_literal { def to_node(ctx) Dhallish::Ast::UnionType.new({}) end } /
+ "<" space? lb:label space? ":" space? type:expression tail:(space? "|" space? lb:label space? ":" space? type:expression)* space? ">"
+ {
+ def to_node(ctx)
+ type_map = {lb.text_value => type.to_node(ctx)}
+ tail.elements.each { |node|
+ type_map[node.lb.text_value] = node.type.to_node(ctx)
+ }
+ Dhallish::Ast::UnionType.new(type_map)
+ end
+ }
+
+ end
+
## Rules for operator expressions
## rules are reversely ordered by their precedence
## e.g. if rule X is over rule Y, the operator associated with rule Y has a stronger precedence than Xs operator
@@ -371,6 +411,8 @@ grammar DhallishGrammar
exp:label { def to_node(ctx) exp.to_node(ctx) end } /
exp:record_literal { def to_node(ctx) exp.to_node(ctx) end } /
exp:record_type_literal { def to_node(ctx) exp.to_node(ctx) end } /
+ exp:union_literal { def to_node(ctx) exp.to_node(ctx) end } /
+ exp:union_type_literal { def to_node(ctx) exp.to_node(ctx) end } /
"(" space? exp:expression space? ")" { def to_node(ctx) exp.to_node(ctx) end }
end
diff --git a/lib/ast.rb b/lib/ast.rb
index 744fce8..36a8c2e 100644
--- a/lib/ast.rb
+++ b/lib/ast.rb
@@ -656,6 +656,62 @@ module Dhallish
def evaluate(ctx) @buf end
end
+ class UnionLiteral
+ # map: label -> type, can be empty
+ attr_accessor :map
+ attr_accessor :init_label
+ attr_accessor :init_val
+ def initialize(map, init_label, init_val)
+ @map = map
+ @init_label = init_label
+ @init_val = init_val
+ end
+
+ def compute_type(ctx)
+ types = {}
+ @map.each { |key, node|
+ assert ("duplicate labels not allowed in union literals") { !types.include? key }
+ types[key] = node.compute_type(ctx)
+ }
+ assert ("duplicate labels not allowed in union literals") { !types.include? @init_label }
+ types[@init_label] = @init_val.compute_type(ctx)
+ Types::Union.new(types)
+ end
+
+ def evaluate(ctx)
+ res = {@init_label => @init_val.evaluate(ctx)}
+ res
+ end
+ end
+
+ class UnionType
+ # map: maps labels to ast-nodes that should be types
+ attr_accessor :map
+
+ def initialize(map)
+ @map = map
+ end
+
+ def compute_type(ctx)
+ types_map = {}
+ @map.each { |key, type|
+ assert ("Duplicate labels in Union Types are not allowed") { !types_map.include? key }
+ type_type = type.compute_type ctx
+ assert ("annotated type in union type not a type") { type_type.is_a? Types::Type }
+ types_map[key] = type_type.metadata
+ }
+ Types::Type.new(Types::Union.new types_map)
+ end
+
+ def evaluate(ctx)
+ res = {}
+ @map.each { |key, node|
+ res[key] = node.evaluate ctx
+ }
+ Types::Union.new(res)
+ end
+ end
+
class Import_Alternative
attr_accessor :lhs
attr_accessor :rhs
diff --git a/lib/types.rb b/lib/types.rb
index 0224f9e..2b2a86a 100644
--- a/lib/types.rb
+++ b/lib/types.rb
@@ -119,6 +119,29 @@ module Dhallish
def ==(otype) otype.is_a? Unresolved and otype.name == @name end
def to_s() "Unresolved(#{@name})" end
end
+ class Union
+ # types: label -> Type
+ attr_accessor :types
+ def initialize(types)
+ @types = types
+ end
+
+ def ==(otype)
+ if !otype.is_a? Union
+ return false
+ end
+
+ @types.keys.reduce(true) { |isequal, key|
+ isequal and (otype.types.include? key and @types[key] == otype.types[key])
+ }
+ end
+
+ def to_s()
+ "< #{@types.keys.map { |key|
+ "#{key}: #{@types[key].to_s}"
+ }.join(" | ")} >"
+ end
+ end
def resolve(orgtype, name, newtype)
case orgtype
@@ -148,6 +171,8 @@ module Dhallish
List.new(resolve(orgtype.type, name, newtype))
when Record
Record.new(orgtype.types.map{ |key, val| [key, resolve(val, name, newtype)] }.to_h)
+ when Union
+ Union.new(orgtype.types.map{ |key, val| [key, resolve(val, name, newtype)] }.to_h)
else
orgtype
end
@@ -214,6 +239,19 @@ module Dhallish
else
nil
end
+ when Union
+ if b.is_a? Union and a.types.keys.length == b.types.keys.length
+ for key in a.types.keys
+ aelm = a.types[key]
+ belm = b.types[key]
+ if belm.nil?; return nil end
+ ret = unification(aelm, belm, mapping)
+ if ret.nil?; return nil end
+ end
+ mapping
+ else
+ nil
+ end
else
if a == b
mapping
@@ -228,7 +266,7 @@ module Dhallish
if x.is_a? Symbol
x != Natural and x != Integer and x != Double and x != Bool and x != Text
else
- !x.is_a? Optional and !x.is_a? List and !x.is_a? Record and !x.is_a? Function and !x.is_a? Unresolved and !x.is_a? Type
+ !x.is_a? Optional and !x.is_a? List and !x.is_a? Record and !x.is_a? Function and !x.is_a? Unresolved and !x.is_a? Type and !x.is_a? Union
end
end
module_function :not_a_type?
@@ -260,7 +298,11 @@ module Dhallish
when nil
"null"
else
- "\"Dhallish-Internal: #{escape_str(dhallval.inspect)}\""
+ if Types::is_a_type? dhallval
+ "\"#{dhallval.to_s}\""
+ else
+ "\"Dhallish-Internal: #{escape_str(dhallval.inspect)}\""
+ end
end
end
module_function :to_json
--
GitLab