From bff8aa4ca6bb901a10c293711758c620ea3d24ed Mon Sep 17 00:00:00 2001
From: Lou Knauer <lou.knauer@gmx.de>
Date: Mon, 11 Mar 2019 11:48:01 +0100
Subject: [PATCH] changes from friday, first try at new unification
This should not be as important any more as philipp fixed this
issue in the master branch allready using another aproach, but at some point in the future i
would like to fix all of this.
---
.gitmodules | 3 +
dhall-lang | 1 +
lib/ast.rb | 4 +-
lib/stdlib.rb | 193 +++++++++++++++++++++++++++++++++++++++++++++++++-
lib/types.rb | 166 ++++++++++++++++++++++++-------------------
lib/utils.rb | 2 +-
tests/test.rb | 11 ++-
7 files changed, 304 insertions(+), 76 deletions(-)
create mode 100644 .gitmodules
create mode 160000 dhall-lang
diff --git a/.gitmodules b/.gitmodules
new file mode 100644
index 0000000..6f9fbd8
--- /dev/null
+++ b/.gitmodules
@@ -0,0 +1,3 @@
+[submodule "dhall-lang"]
+ path = dhall-lang
+ url = https://github.com/dhall-lang/dhall-lang.git
diff --git a/dhall-lang b/dhall-lang
new file mode 160000
index 0000000..b583925
--- /dev/null
+++ b/dhall-lang
@@ -0,0 +1 @@
+Subproject commit b583925f00ef787e201bb07bed0e6fef0db9463d
diff --git a/lib/ast.rb b/lib/ast.rb
index e4a5e35..8c57919 100644
--- a/lib/ast.rb
+++ b/lib/ast.rb
@@ -636,7 +636,7 @@ module Dhallish
new_path = File.dirname src
else
opath = basedir.path
- basedir.path = File.join basedir.path, (@prefix + src)
+ basedir.path = File.join basedir.path, (@prefix + src)
src = basedir.to_s
basedir.path = File.dirname basedir.path
new_path = URI basedir.to_s
@@ -652,6 +652,8 @@ module Dhallish
new_path.path = File.dirname new_path.path
end
+ # STDERR.puts "import src: #{src}"
+
file = open(src)
text = file.read
diff --git a/lib/stdlib.rb b/lib/stdlib.rb
index 48a0505..cd5f24b 100644
--- a/lib/stdlib.rb
+++ b/lib/stdlib.rb
@@ -21,6 +21,12 @@ module Dhallish
end
module_function :make_fn_type
+ def define(ctx, name, value, type)
+ ctx["<#TYPES#>"][name.to_s] = type
+ ctx["<#VALS#>"][name.to_s] = value
+ end
+ module_function :define
+
def fill_context(globalctx, types)
# Types:
@@ -78,7 +84,7 @@ module Dhallish
globalctx["Double/toInteger"] = douToInt
types["Double/toInteger"] = Types::Function.new(Types::Double, Types::Integer)
-
+=begin
# Lists:
globalctx["List"] = BuiltinFunction.new { |a| Types::List.new(a) }
types["List"] = make_fn_type([:list_a], Types::Type.new(Types::List.new(Types::Unresolved.new(:list_a))))
@@ -262,6 +268,191 @@ module Dhallish
f.call(Types::Natural).call(succ).call(zero)
}
types["Natural/build"] = make_fn_type(make_fn_type([:nat_build_a], make_fn_type(:nat_build_a, :nat_build_a), :nat_build_a, :nat_build_a), Types::Natural)
+=end
+
+ # Lists:
+ globalctx["List"] = BuiltinFunction.new { |a| Types::List.new(a) }
+ types["List"] = make_fn_type([:a], Types::Type.new(Types::List.new(Types::Unresolved.new(:a))))
+
+ list_length_type = make_fn_type([:a], Types::List.new(Types::Unresolved.new(:a)), Types::Natural)
+ globalctx["List/length"] = BuiltinFunction.new{ |a|
+ BuiltinFunction.new { |list|
+ list.length
+ }
+ }
+ types["List/length"] = list_length_type
+
+ list_fold_type = make_fn_type(
+ [:a],
+ Types::List.new(Types::Unresolved.new(:a)),
+ [:b],
+ make_fn_type(:a, :b, :b),
+ :b, :b)
+ globalctx["List/fold"] = BuiltinFunction.new { |a|
+ BuiltinFunction.new { |list|
+ BuiltinFunction.new { |b|
+ BuiltinFunction.new { |f|
+ BuiltinFunction.new { |x|
+ acc = x
+ list.reverse_each { |elm| acc = f.call(elm).call(acc) }
+ acc
+ }
+ }
+ }
+ }
+ }
+ types["List/fold"] = list_fold_type
+
+ list_head_type = make_fn_type(
+ [:a],
+ Types::List.new(Types::Unresolved.new(:a)),
+ Types::Optional.new(Types::Unresolved.new(:a)))
+ globalctx["List/head"] = BuiltinFunction.new { |a|
+ BuiltinFunction.new { |list|
+ list.first
+ }
+ }
+ types["List/head"] = list_head_type
+
+ list_last_type = make_fn_type(
+ [:a],
+ Types::List.new(Types::Unresolved.new(:a)),
+ Types::Optional.new(Types::Unresolved.new(:a)))
+ globalctx["List/last"] = BuiltinFunction.new { |a|
+ BuiltinFunction.new { |list|
+ list.last
+ }
+ }
+ types["List/last"] = list_last_type
+
+ list_tail_type = make_fn_type(
+ [:a],
+ Types::List.new(Types::Unresolved.new(:a)),
+ Types::List.new(Types::Unresolved.new(:a)))
+ globalctx["List/tail"] = BuiltinFunction.new { |a|
+ BuiltinFunction.new { |list|
+ if list.empty?
+ []
+ else
+ list[1..list.length]
+ end
+ }
+ }
+ types["List/tail"] = list_tail_type
+
+ types["List/reverse"] = make_fn_type(
+ [:a],
+ Types::List.new(Types::Unresolved.new(:a)),
+ Types::List.new(Types::Unresolved.new(:a)))
+ globalctx["List/reverse"] = BuiltinFunction.new { |a|
+ BuiltinFunction.new { |list| list.reverse }
+ }
+
+ types["List/build"] = make_fn_type(
+ [:a],
+ make_fn_type(
+ [:b],
+ make_fn_type(:a, :b, :b), :b, :b),
+ Types::List.new(Types::Unresolved.new(:a)))
+ globalctx["List/build"] = BuiltinFunction.new { |a|
+ BuiltinFunction.new { |f|
+ cons = BuiltinFunction.new { |x|
+ BuiltinFunction.new { |list| [x] + list }
+ }
+ f.call(Types::List.new(a)).call(cons).call([])
+ }
+ }
+
+ types["List/indexed"] = make_fn_type(
+ [:a],
+ Types::List.new(Types::Unresolved.new(:a)),
+ Types::List.new(Types::Record.new({
+ "index" => Types::Natural,
+ "value" => Types::Unresolved.new(:a)})))
+ globalctx["List/indexed"] = BuiltinFunction.new { |a|
+ BuiltinFunction.new { |list|
+ list.map.with_index { |val, idx|
+ { "index" => idx, "value" => val }
+ }
+ }
+ }
+
+ # Optionals:
+ globalctx["Optional"] = BuiltinFunction.new { |a|
+ Types::Optional.new(a)
+ }
+ types["Optional"] = make_fn_type([:opt_a], Types::Type.new(Types::Optional.new(Types::Unresolved.new(:opt_a))))
+
+ optional_fold_type = make_fn_type(
+ [:a],
+ Types::Optional.new(Types::Unresolved.new(:a)),
+ [:b],
+ make_fn_type(:a, :b),
+ :b, :b)
+ globalctx["Optional/fold"] = BuiltinFunction.new { |a|
+ BuiltinFunction.new { |opt|
+ BuiltinFunction.new { |b|
+ BuiltinFunction.new { |f|
+ BuiltinFunction.new { |x|
+ if opt.nil?
+ x
+ else
+ f.call(opt)
+ end
+ }
+ }
+ }
+ }
+ }
+ types["Optional/fold"] = optional_fold_type
+
+ types["Optional/build"] = make_fn_type(
+ [:a],
+ make_fn_type([:b],
+ make_fn_type(:a, :b), :b, :b),
+ Types::Optional.new(Types::Unresolved.new(:a)))
+ globalctx["Optional/build"] = BuiltinFunction.new { |a|
+ BuiltinFunction.new { |f|
+ just = BuiltinFunction.new { |x| x }
+ f.call(Types::Optional.new(a)).call(just).call(nil)
+ }
+ }
+
+
+ # Naturals:
+ natural_fold_type = make_fn_type(
+ Types::Natural,
+ [:a],
+ make_fn_type(:a, :a),
+ :a, :a)
+ globalctx["Natural/fold"] = BuiltinFunction.new { |n|
+ BuiltinFunction.new { |a|
+ BuiltinFunction.new { |succ|
+ BuiltinFunction.new { |zero|
+ res = zero
+ n.times { res = succ.call(res) }
+ res
+ }
+ }
+ }
+ }
+ types["Natural/fold"] = natural_fold_type
+
+ types["Natural/even"] = make_fn_type(Types::Natural, Types::Bool)
+ globalctx["Natural/even"] = BuiltinFunction.new { |n| n % 2 == 0 }
+
+ types["Natural/odd"] = make_fn_type(Types::Natural, Types::Bool)
+ globalctx["Natural/odd"] = BuiltinFunction.new { |n| n % 2 == 1 }
+
+ types["Natural/isZero"] = make_fn_type(Types::Natural, Types::Bool)
+ globalctx["Natural/isZero"] = BuiltinFunction.new { |n| n == 0 }
+
+ globalctx["Natural/build"] = BuiltinFunction.new { |f|
+ zero = 0
+ succ = BuiltinFunction.new { |n| n + 1 }
+ f.call(Types::Natural).call(succ).call(zero)
+ }
+ types["Natural/build"] = make_fn_type(make_fn_type([:a], make_fn_type(:a, :a), :a, :a), Types::Natural)
end
module_function :fill_context
diff --git a/lib/types.rb b/lib/types.rb
index 1e6bbee..b36499e 100644
--- a/lib/types.rb
+++ b/lib/types.rb
@@ -23,7 +23,7 @@ module Dhallish
end
end
def to_s()
- if @metadata.nil? or @metadata.is_a? Unresolved
+ if @metadata.nil?
"Type"
else
"Type(#{@metadata.to_s})"
@@ -149,10 +149,16 @@ module Dhallish
end
end
+ # basically a substitution
def resolve(orgtype, name, newtype)
+ puts "resolve[#{name} => #{newtype}]:\t#{orgtype}"
case orgtype
when Type
- Type.new(resolve(orgtype.metadata, name, newtype))
+ if !orgtype.metadata.nil?
+ Type.new(resolve(orgtype.metadata, name, newtype))
+ else
+ Type.new(nil)
+ end
when Unresolved
if name == orgtype.name
newtype
@@ -160,17 +166,25 @@ module Dhallish
orgtype
end
when Function
- if orgtype.restype.nil?
- Function.new(resolve(orgtype.argtype, name, newtype), nil, orgtype.unres)
- else
- restype = orgtype.restype
- argtype = orgtype.argtype
- if orgtype.unres.nil? or orgtype.unres != name
- restype = resolve(orgtype.restype, name, newtype)
- argtype = resolve(orgtype.argtype, name, newtype)
- end
- Function.new(argtype, restype, orgtype.unres)
+ restype = orgtype.restype
+ argtype = orgtype.argtype
+ unres = orgtype.unres
+ if orgtype.unres.nil? or orgtype.unres != name
+ restype = resolve(orgtype.restype, name, newtype)
+ argtype = resolve(orgtype.argtype, name, newtype)
+ elsif !orgtype.unres.nil?
+ assert("debug: #{orgtype}") {
+ argtype == Type.new(Unresolved.new(orgtype.unres))
+ }
+ # TODO: resolve bug?
+ # Bug vielleicht in call node?
+ # `dhalltest.rb`
+ #puts "1--> #{Function.new(argtype, restype, unres)}"
+ #argtype = resolve(orgtype.argtype, name, newtype)
+ #unres = name
+ #puts "2--> #{Function.new(argtype, restype, unres)}"
end
+ Function.new(argtype, restype, unres)
when Optional
Optional.new(resolve(orgtype.type, name, newtype))
when List
@@ -180,6 +194,7 @@ module Dhallish
when Union
Union.new(orgtype.types.map{ |key, val| [key, resolve(val, name, newtype)] }.to_h)
else
+ assert("debug: #{orgtype}") { is_a_type?(orgtype) }
orgtype
end
end
@@ -188,82 +203,87 @@ module Dhallish
def unification(a, b, mapping={})
case a
when Type
- if b.is_a? Type
+ if !b.is_a? Type; return nil end
+ # I think those Kinds dhall has might be important here.
+ # `Type` is actually of type `Kind`?
+ # TODO: There is stuff to be done here i think...
+ if !a.metadata.nil? and !b.metadata.nil?
unification(a.metadata, b.metadata, mapping)
+ elsif b.metadata.nil?
+ mapping
else
nil
end
+ when Natural, Integer, Double, Text, Bool
+ if a == b; mapping else nil end
+ when List
+ if !b.is_a? List; return nil end
+ unification(a.type, b.type, mapping)
+ when Optional
+ if !b.is_a? Optional; return nil end
+ unification(a.type, b.type, mapping)
+ when Record
+ if !b.is_a? Record or a.types.length != b.types.length; return nil end
+ for key in a.types.keys
+ afield = a.types[key]
+ bfield = b.types[key]
+ if bfield.nil? or unification(afield, bfield, mapping).nil?
+ return nil
+ end
+ end
+ mapping
+ when Union
+ if !b.is_a? Union or a.types.length != b.types.length; return nil end
+ for key in a.types.keys
+ afield = a.types[key]
+ bfield = b.types[key]
+ if bfield.nil? or unification(afield, bfield, mapping).nil?
+ return nil
+ end
+ end
+ mapping
when Unresolved
- if b.is_a? Unresolved
- if mapping[a.name] == nil
- mapping[a.name] = b.name
+ if !b.is_a? Unresolved; return nil end
+ if mapping[a.name] != nil
+ if mapping[a.name] == b.name
mapping
- elsif mapping[a.name] != b.name
- nil
else
- mapping
+ nil
end
else
- nil
+ mapping[a.name] = b.name
+ mapping
end
when Function
- if b.is_a? Function
- if unification(a.argtype, b.argtype, mapping).nil?
- nil
- else
- arestype = a.restype
- brestype = b.restype
- if !a.unres.nil?; arestype = resolve(a.restype, a.unres, Unresolved.new(get_new_sym())) end
- if !b.unres.nil?; brestype = resolve(b.restype, b.unres, Unresolved.new(get_new_sym())) end
- unification(arestype, brestype, mapping)
+ if !b.is_a? Function; return nil end
+ if !a.unres.nil?
+ assert("debug: #{a}") { a.argtype.is_a? Type and a.argtype.metadata == Unresolved.new(a.unres) }
+ if b.unres.nil?; return nil end
+ assert("debug: #{b}") { b.argtype.is_a? Type and b.argtype.metadata == Unresolved.new(b.unres) }
+
+ # TODO: Update mapping?
+ # TODO: keys and values swapped?
+
+ arestype = a.restype
+ brestype = b.restype
+ if mapping.keys.include? a.unres
+ sym = get_new_sym()
+ arestype = resolve(arestype, a.unres, Unresolved.new(sym))
end
- else
- nil
- end
- when Optional
- if b.is_a? Optional
- unification(a.type, b.type, mapping)
- else
- nil
- end
- when List
- if b.is_a? List
- unification(a.type, b.type, mapping)
- else
- nil
- end
- when Record
- if b.is_a? Record 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
+ if mapping.values.include? b.unres
+ sym = get_new_sym()
+ brestype = resolve(brestype, b.unres, Unresolved.new(sym))
end
- mapping
+ unification(arestype, brestype, mapping)
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
+ if !unification(a.argtype, b.argtype, mapping).nil?
+ unification(a.restype, b.restype, mapping)
+ else
+ nil
end
- mapping
- else
- nil
end
else
- if a == b
- mapping
- else
- nil
- end
+ raise "New Type? a: #{a.inspect}, b: #{b.inspect}"
end
end
module_function :unification
@@ -307,9 +327,11 @@ module Dhallish
"{#{ dhallval.map{ |key, val| "\"#{escape_str(key)}\": #{ to_json(val) }" }.join(", ") }}"
when nil
"null"
+ when Union
+ to_json(dhallval.init_val)
else
if Types::is_a_type? dhallval
- "\"#{dhallval.to_s}\""
+ "\"Dhallish::Type(#{dhallval.to_s})\""
else
"\"<#{escape_str(dhallval.class.to_s)}##{dhallval.hash.abs.to_s(16)}>\""
end
diff --git a/lib/utils.rb b/lib/utils.rb
index b03bd3a..300fb1e 100644
--- a/lib/utils.rb
+++ b/lib/utils.rb
@@ -16,7 +16,7 @@ end
$dhallish_internal_global_counter = 0
def get_new_sym()
$dhallish_internal_global_counter += 1
- ("__newsym_#{$dhallish_internal_global_counter}").to_sym
+ ("__#{$dhallish_internal_global_counter}").to_sym
end
def escape_str(str)
diff --git a/tests/test.rb b/tests/test.rb
index 6e12055..c6cc00e 100755
--- a/tests/test.rb
+++ b/tests/test.rb
@@ -36,7 +36,7 @@ positive_tests = {
"fallback for file import": ["let x = ./foobarfoobar.dhall as Text ? 1 in x", 1],
"more type annotation": [ "let f = \\(a: Type) -> \\(l: List a) -> \\(x: a) -> x in (f: forall(b: Type) -> forall(l: List b) -> b -> b) Natural [1, 2, 3] 5", 5 ],
"select from union": [ "let union = <a : Natural | b : Text>.a 17 in union.a : Optional Natural", 17 ],
- "union merge": [ "merge { Left = \\(x: Natural) -> Natural/show x, Right = \\(y: Integer) -> Integer/show y } < Left = 42 | Right : Integer >", "42" ]
+ "union merge": [ "merge { Left = \\(x: Natural) -> Natural/show x, Right = \\(y: Integer) -> Integer/show y } < Left = 42 | Right : Integer >", "42" ]
}
negative_tests = {
@@ -115,3 +115,12 @@ dhallfiles.each { |file|
print_msg(file, true)
end
}
+
+puts "\n=== Testing Typecheck on dhall-lang/Prelude/package.dhall"
+begin
+ Dhallish::evaluate("./" + File.join(File.dirname(__FILE__), "../dhall-lang/Prelude/package.dhall"))
+rescue
+ print_msg("Prelude/package.dhall", false)
+else
+ print_msg("Prelude/package.dhall", true)
+end
--
GitLab