From be51ed9685128b08a18ef3ff58a3fd06a782acc7 Mon Sep 17 00:00:00 2001
From: Lou Knauer <lou.knauer@gmx.de>
Date: Mon, 4 Mar 2019 17:37:11 +0100
Subject: [PATCH] unificator-function for types
---
lib/types.rb | 67 ++++++++++++++++++++++++++++++++++++++++++++++++++++
lib/utils.rb | 6 +++++
2 files changed, 73 insertions(+)
diff --git a/lib/types.rb b/lib/types.rb
index d5d7aca..6dbd9d8 100644
--- a/lib/types.rb
+++ b/lib/types.rb
@@ -148,6 +148,73 @@ module Dhallish
end
module_function :resolve
+ def unification(a, b, mapping={})
+ assert("a and b must be types") { is_a_type(a) and is_a_type(b) }
+ case a
+ when Type
+ if b.is_a? Type
+ unification(a.metadata, b.metadata, mapping)
+ else
+ nil
+ end
+ when Unresolved
+ if b.is_a? Unresolved
+ if mapping[a.name] == nil
+ mapping[a.name] = b.name
+ mapping
+ elsif mapping[a.name] != mapping[b.name]
+ nil
+ else
+ mapping
+ end
+ else
+ nil
+ 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)
+ 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
+ end
+ mapping
+ else
+ nil
+ end
+ else
+ a == b
+ end
+ end
+ module_function :unification
+
def not_a_type?(x)
if x.is_a? Symbol
x != Natural and x != Integer and x != Double and x != Bool and x != Text
diff --git a/lib/utils.rb b/lib/utils.rb
index ce32df8..4670dc3 100644
--- a/lib/utils.rb
+++ b/lib/utils.rb
@@ -12,3 +12,9 @@ class DhallError < StandardError
super(msg)
end
end
+
+$dhallish_internal_global_counter = 0
+def get_new_sym()
+ $dhallish_internal_global_counter += 1
+ ("__newsym_#{$dhallish_internal_global_counter}").to_sym
+end
--
GitLab