From bce3b47ae39e39981dee4380c421e48ff3718bba Mon Sep 17 00:00:00 2001 From: Stephen Paul Weber Date: Fri, 8 Mar 2019 20:07:49 -0500 Subject: [PATCH] Beta normalization complete --- lib/dhall/ast.rb | 16 ++++ lib/dhall/builtins.rb | 84 ++++++++++++++++++ lib/dhall/normalize.rb | 22 ++++- .../beta/FunctionApplicationCaptureA.dhallb | Bin 0 -> 24 bytes .../beta/FunctionApplicationCaptureB.dhallb | 1 + .../FunctionApplicationNoSubstituteA.dhallb | Bin 0 -> 19 bytes .../FunctionApplicationNoSubstituteB.dhallb | 1 + ...ctionApplicationNormalizeArgumentsA.dhallb | Bin 0 -> 23 bytes ...ctionApplicationNormalizeArgumentsB.dhallb | Bin 0 -> 13 bytes .../FunctionApplicationSubstituteA.dhallb | Bin 0 -> 19 bytes .../FunctionApplicationSubstituteB.dhallb | 1 + .../beta/FunctionNormalizeArgumentsA.dhallb | 1 + .../beta/FunctionNormalizeArgumentsB.dhallb | 1 + .../FunctionTypeNormalizeArgumentsA.dhallb | 1 + .../FunctionTypeNormalizeArgumentsB.dhallb | 1 + test/test_normalization.rb | 30 +++++++ 16 files changed, 157 insertions(+), 2 deletions(-) create mode 100644 test/normalization/beta/FunctionApplicationCaptureA.dhallb create mode 100644 test/normalization/beta/FunctionApplicationCaptureB.dhallb create mode 100644 test/normalization/beta/FunctionApplicationNoSubstituteA.dhallb create mode 100644 test/normalization/beta/FunctionApplicationNoSubstituteB.dhallb create mode 100644 test/normalization/beta/FunctionApplicationNormalizeArgumentsA.dhallb create mode 100644 test/normalization/beta/FunctionApplicationNormalizeArgumentsB.dhallb create mode 100644 test/normalization/beta/FunctionApplicationSubstituteA.dhallb create mode 100644 test/normalization/beta/FunctionApplicationSubstituteB.dhallb create mode 100644 test/normalization/beta/FunctionNormalizeArgumentsA.dhallb create mode 100644 test/normalization/beta/FunctionNormalizeArgumentsB.dhallb create mode 100644 test/normalization/beta/FunctionTypeNormalizeArgumentsA.dhallb create mode 100644 test/normalization/beta/FunctionTypeNormalizeArgumentsB.dhallb diff --git a/lib/dhall/ast.rb b/lib/dhall/ast.rb index 28e8ca6..69a4263 100644 --- a/lib/dhall/ast.rb +++ b/lib/dhall/ast.rb @@ -129,6 +129,14 @@ module Dhall def map_subexpressions(&block) with(var: var, type: type.nil? ? nil : block[type], body: block[body]) 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 @@ -279,6 +287,10 @@ module Dhall def map_subexpressions(&block) with(value: block[value], type: type.nil? ? type : block[type]) end + + def reduce(_, &block) + block[value] + end end class OptionalNone < Optional @@ -289,6 +301,10 @@ module Dhall def map_subexpressions(&block) with(type: block[@type]) end + + def reduce(z) + z + end end class Merge < Expression diff --git a/lib/dhall/builtins.rb b/lib/dhall/builtins.rb index 8d27f9b..b5d55ef 100644 --- a/lib/dhall/builtins.rb +++ b/lib/dhall/builtins.rb @@ -154,6 +154,10 @@ module Dhall end class List_build < Builtin + def initialize(type=nil) + @type = type + end + def fusion(*args) _, arg, = args if arg.is_a?(Application) && @@ -165,6 +169,37 @@ module Dhall super end end + + def call(arg) + if @type.nil? + self.class.new(arg) + else + arg.call( + Application.new( + function: Variable.new(name: "List"), + arguments: [@type] + ), + Function.new( + var: "_", + type: @type, + body: Function.new( + var: "_", + type: Application.new( + function: Variable.new(name: "List"), + arguments: [@type.shift(1, "_", 0)] + ), + body: Operator::ListConcatenate.new( + lhs: List.new( + elements: [Variable.new(name: "_", index: 1)] + ), + rhs: Variable.new(name: "_") + ) + ), + ), + EmptyList.new(type: @type) + ) + end + end end class List_fold < Builtin @@ -249,6 +284,10 @@ module Dhall end class Optional_build < Builtin + def initialize(type=nil) + @type = type + end + def fusion(*args) _, arg, = args if arg.is_a?(Application) && @@ -260,9 +299,54 @@ module Dhall super end end + + def call(arg) + if @type.nil? + self.class.new(arg) + else + arg.call( + Application.new( + function: Variable.new(name: "Optional"), + arguments: [@type] + ), + Function.new( + var: "_", + type: @type, + body: Optional.new( + value: Variable.new(name: "_"), + type: @type + ) + ), + OptionalNone.new(type: @type) + ) + end + end + end class Optional_fold < Builtin + def initialize(type=nil, optional=nil, ztype=nil, f=nil) + @type = type + @optional = optional + @ztype = ztype + @f = f + end + + def call(arg) + if @type.nil? + self.class.new(arg) + elsif arg.is_a?(Optional) + self.class.new(@type, arg) + elsif !@optional.nil? && @ztype.nil? + self.class.new(@type, @optional, arg) + elsif !@optional.nil? && @f.nil? + self.class.new(@type, @optional, @ztype, arg) + elsif !@optional.nil? + @optional.reduce(arg, &@f) + else + super + end + end end class Text_show < Builtin diff --git a/lib/dhall/normalize.rb b/lib/dhall/normalize.rb index fe6cd84..80724ab 100644 --- a/lib/dhall/normalize.rb +++ b/lib/dhall/normalize.rb @@ -12,6 +12,10 @@ module Dhall map_subexpressions { |expr| expr.shift(amount, name, min_index) } end + def substitute(var, with_expr) + map_subexpressions { |expr| expr.substitute(var, with_expr) } + end + def fusion(*); end end @@ -21,7 +25,8 @@ module Dhall normalized = super return normalized.fuse if normalized.fuse - if normalized.function.is_a?(Builtin) + if normalized.function.is_a?(Builtin) || + normalized.function.is_a?(Function) return normalized.function.call(*normalized.arguments) end @@ -46,6 +51,15 @@ module Dhall body: body.shift(amount, name, min_index + 1) ) end + + def substitute(svar, with_expr) + with_expr = with_expr.shift(1, var, 0) + if var == svar.name + super(svar.with(index: svar.index + 1), with_expr) + else + super(svar, with_expr) + end + end end class Forall; end @@ -58,6 +72,10 @@ module Dhall return self if self.name != name || min_index > index with(index: index + amount) end + + def substitute(var, with_expr) + self == var ? with_expr : self + end end class Operator @@ -293,7 +311,7 @@ module Dhall end def desugar - lets.reduce(body) { |inside, let| + lets.reverse.reduce(body) { |inside, let| Application.new( function: Function.new( var: let.var, diff --git a/test/normalization/beta/FunctionApplicationCaptureA.dhallb b/test/normalization/beta/FunctionApplicationCaptureA.dhallb new file mode 100644 index 0000000000000000000000000000000000000000..69f3770ef70c5d38562e50ba6d54a405736fbeac GIT binary patch literal 24 bcmZolHPtiFGiYW2LdL`h5N1rQNUQ_^RBZ