From 8442a467a232b86cb8bf080522453aed7f0b779c Mon Sep 17 00:00:00 2001 From: Drazen Popovic Date: Tue, 21 Mar 2023 16:30:14 +0100 Subject: [PATCH] Removed goal cycle error in favor of what is supposedly a co-inductive logic --- lambda-buffers-compiler/build.nix | 2 +- .../data/minilog-goldens/cycle.pl | 4 + .../cycled_goals_1/compiler_error.textproto | 463 ------------------ .../cycled_goals_1/foo.pl | 125 +++++ .../cycled_goals_1/prelude.pl | 98 ++++ .../cycled_goals_2/foo.pl | 143 ++++++ .../cycled_goals_2/prelude.pl | 98 ++++ .../src/LambdaBuffers/Compiler/MiniLog.hs | 2 - .../Compiler/MiniLog/UniFdSolver.hs | 59 ++- .../Compiler/TypeClassCheck/Errors.hs | 9 - .../Compiler/TypeClassCheck/MiniLog.hs | 6 +- .../Test/LambdaBuffers/Compiler/MiniLog.hs | 97 ++-- .../LambdaBuffers/Compiler/TypeClassCheck.hs | 62 ++- .../data/goldens/good/PreludeT.lbf | 10 +- .../data/goldens/good/Rules.lbf | 23 + lambda-buffers-frontend/data/run.sh | 7 +- lambda-buffers-proto/compiler.proto | 13 +- 17 files changed, 658 insertions(+), 563 deletions(-) delete mode 100644 lambda-buffers-compiler/data/typeclasscheck-goldens/cycled_goals_1/compiler_error.textproto create mode 100644 lambda-buffers-compiler/data/typeclasscheck-goldens/cycled_goals_1/foo.pl create mode 100644 lambda-buffers-compiler/data/typeclasscheck-goldens/cycled_goals_1/prelude.pl create mode 100644 lambda-buffers-compiler/data/typeclasscheck-goldens/cycled_goals_2/foo.pl create mode 100644 lambda-buffers-compiler/data/typeclasscheck-goldens/cycled_goals_2/prelude.pl create mode 100644 lambda-buffers-frontend/data/goldens/good/Rules.lbf diff --git a/lambda-buffers-compiler/build.nix b/lambda-buffers-compiler/build.nix index 393831ae..d200150b 100644 --- a/lambda-buffers-compiler/build.nix +++ b/lambda-buffers-compiler/build.nix @@ -38,7 +38,7 @@ let exactDeps = true; - nativeBuildInputs = builtins.attrValues commonTools; + nativeBuildInputs = [ pkgs.swiPrologWithGui ] ++ builtins.attrValues commonTools; tools = { cabal = { }; diff --git a/lambda-buffers-compiler/data/minilog-goldens/cycle.pl b/lambda-buffers-compiler/data/minilog-goldens/cycle.pl index 2450e09c..0d98333c 100644 --- a/lambda-buffers-compiler/data/minilog-goldens/cycle.pl +++ b/lambda-buffers-compiler/data/minilog-goldens/cycle.pl @@ -3,6 +3,10 @@ 'eq'('int'). +'eq'('rectype') :- + 'eq'('int'),'eq'('rectype'). + + 'eq'('list'(VX)) :- 'eq'(VX). diff --git a/lambda-buffers-compiler/data/typeclasscheck-goldens/cycled_goals_1/compiler_error.textproto b/lambda-buffers-compiler/data/typeclasscheck-goldens/cycled_goals_1/compiler_error.textproto deleted file mode 100644 index cac3b912..00000000 --- a/lambda-buffers-compiler/data/typeclasscheck-goldens/cycled_goals_1/compiler_error.textproto +++ /dev/null @@ -1,463 +0,0 @@ -ty_class_check_errors { - constraint_cycle_err { - module_name { - parts { name: "Foo" source_info { pos_from {} pos_to {} } } - source_info { pos_from {} pos_to {} } - } - constraint { - class_ref { - foreign_class_ref { - class_name { name: "Eq" source_info { pos_from {} pos_to {} } } - module_name { - parts { name: "Prelude" source_info { pos_from {} pos_to {} } } - source_info { pos_from {} pos_to {} } - } - source_info { pos_from {} pos_to {} } - } - } - args { - ty_app { - ty_func { - ty_ref { - local_ty_ref { - ty_name { name: "Bar" source_info { pos_from {} pos_to {} } } - source_info { pos_from {} pos_to {} } - } - } - } - ty_args { - ty_var { - var_name { name: "a" source_info { pos_from {} pos_to {} } } - } - } - source_info { pos_from {} pos_to {} } - } - } - source_info { pos_from {} pos_to {} } - } - cycled_constraints { - class_ref { - foreign_class_ref { - class_name { name: "Eq" source_info { pos_from {} pos_to {} } } - module_name { - parts { name: "Prelude" source_info { pos_from {} pos_to {} } } - source_info { pos_from {} pos_to {} } - } - source_info { pos_from {} pos_to {} } - } - } - args { - ty_app { - ty_func { - ty_ref { - local_ty_ref { - ty_name { name: "Bar" source_info { pos_from {} pos_to {} } } - source_info { pos_from {} pos_to {} } - } - } - } - ty_args { - ty_var { - var_name { name: "a" source_info { pos_from {} pos_to {} } } - } - } - source_info { pos_from {} pos_to {} } - } - } - source_info { pos_from {} pos_to {} } - } - cycled_constraints { - class_ref { - foreign_class_ref { - class_name { name: "Eq" source_info { pos_from {} pos_to {} } } - module_name { - parts { name: "Prelude" source_info { pos_from {} pos_to {} } } - source_info { pos_from {} pos_to {} } - } - source_info { pos_from {} pos_to {} } - } - } - args { - ty_app { - ty_func { - ty_ref { - local_ty_ref { - ty_name { name: "Baz" source_info { pos_from {} pos_to {} } } - source_info { pos_from {} pos_to {} } - } - } - } - ty_args { - ty_var { - var_name { name: "a" source_info { pos_from {} pos_to {} } } - } - } - source_info { pos_from {} pos_to {} } - } - } - source_info { pos_from {} pos_to {} } - } - } -} -ty_class_check_errors { - constraint_cycle_err { - module_name { - parts { name: "Foo" source_info { pos_from {} pos_to {} } } - source_info { pos_from {} pos_to {} } - } - constraint { - class_ref { - foreign_class_ref { - class_name { name: "Eq" source_info { pos_from {} pos_to {} } } - module_name { - parts { name: "Prelude" source_info { pos_from {} pos_to {} } } - source_info { pos_from {} pos_to {} } - } - source_info { pos_from {} pos_to {} } - } - } - args { - ty_app { - ty_func { - ty_ref { - local_ty_ref { - ty_name { name: "Baz" source_info { pos_from {} pos_to {} } } - source_info { pos_from {} pos_to {} } - } - } - } - ty_args { - ty_var { - var_name { name: "a" source_info { pos_from {} pos_to {} } } - } - } - source_info { pos_from {} pos_to {} } - } - } - source_info { pos_from {} pos_to {} } - } - cycled_constraints { - class_ref { - foreign_class_ref { - class_name { name: "Eq" source_info { pos_from {} pos_to {} } } - module_name { - parts { name: "Prelude" source_info { pos_from {} pos_to {} } } - source_info { pos_from {} pos_to {} } - } - source_info { pos_from {} pos_to {} } - } - } - args { - ty_app { - ty_func { - ty_ref { - local_ty_ref { - ty_name { name: "Baz" source_info { pos_from {} pos_to {} } } - source_info { pos_from {} pos_to {} } - } - } - } - ty_args { - ty_var { - var_name { name: "a" source_info { pos_from {} pos_to {} } } - } - } - source_info { pos_from {} pos_to {} } - } - } - source_info { pos_from {} pos_to {} } - } - cycled_constraints { - class_ref { - foreign_class_ref { - class_name { name: "Eq" source_info { pos_from {} pos_to {} } } - module_name { - parts { name: "Prelude" source_info { pos_from {} pos_to {} } } - source_info { pos_from {} pos_to {} } - } - source_info { pos_from {} pos_to {} } - } - } - args { - ty_app { - ty_func { - ty_ref { - local_ty_ref { - ty_name { name: "Bar" source_info { pos_from {} pos_to {} } } - source_info { pos_from {} pos_to {} } - } - } - } - ty_args { - ty_var { - var_name { name: "a" source_info { pos_from {} pos_to {} } } - } - } - source_info { pos_from {} pos_to {} } - } - } - source_info { pos_from {} pos_to {} } - } - } -} -ty_class_check_errors { - derive_opaque_err { - module_name { - parts { name: "Foo" source_info { pos_from {} pos_to {} } } - source_info { pos_from {} pos_to {} } - } - constraint { - class_ref { - foreign_class_ref { - class_name { name: "Ord" source_info { pos_from {} pos_to {} } } - module_name { - parts { name: "Prelude" source_info { pos_from {} pos_to {} } } - source_info { pos_from {} pos_to {} } - } - source_info { pos_from {} pos_to {} } - } - } - args { - ty_app { - ty_func { - ty_ref { - local_ty_ref { - ty_name { name: "Bar" source_info { pos_from {} pos_to {} } } - source_info { pos_from {} pos_to {} } - } - } - } - ty_args { - ty_var { - var_name { name: "a" source_info { pos_from {} pos_to {} } } - } - } - source_info { pos_from {} pos_to {} } - } - } - source_info { pos_from {} pos_to {} } - } - sub_constraint { - class_ref { - foreign_class_ref { - class_name { name: "Ord" source_info { pos_from {} pos_to {} } } - module_name { - parts { name: "Prelude" source_info { pos_from {} pos_to {} } } - source_info { pos_from {} pos_to {} } - } - source_info { pos_from {} pos_to {} } - } - } - args { - ty_app { - ty_func { - ty_ref { - local_ty_ref { - ty_name { name: "Bar" source_info { pos_from {} pos_to {} } } - source_info { pos_from {} pos_to {} } - } - } - } - ty_args { - ty_var { - var_name { name: "a" source_info { pos_from {} pos_to {} } } - } - } - source_info { pos_from {} pos_to {} } - } - } - source_info { pos_from {} pos_to {} } - } - } -} -ty_class_check_errors { - constraint_cycle_err { - module_name { - parts { name: "Foo" source_info { pos_from {} pos_to {} } } - source_info { pos_from {} pos_to {} } - } - constraint { - class_ref { - foreign_class_ref { - class_name { name: "Eq" source_info { pos_from {} pos_to {} } } - module_name { - parts { name: "Prelude" source_info { pos_from {} pos_to {} } } - source_info { pos_from {} pos_to {} } - } - source_info { pos_from {} pos_to {} } - } - } - args { - ty_app { - ty_func { - ty_ref { - local_ty_ref { - ty_name { name: "Foo" source_info { pos_from {} pos_to {} } } - source_info { pos_from {} pos_to {} } - } - } - } - ty_args { - ty_var { - var_name { name: "a" source_info { pos_from {} pos_to {} } } - } - } - ty_args { - ty_var { - var_name { name: "b" source_info { pos_from {} pos_to {} } } - } - } - ty_args { - ty_var { - var_name { name: "c" source_info { pos_from {} pos_to {} } } - } - } - source_info { pos_from {} pos_to {} } - } - } - source_info { pos_from {} pos_to {} } - } - cycled_constraints { - class_ref { - foreign_class_ref { - class_name { name: "Eq" source_info { pos_from {} pos_to {} } } - module_name { - parts { name: "Prelude" source_info { pos_from {} pos_to {} } } - source_info { pos_from {} pos_to {} } - } - source_info { pos_from {} pos_to {} } - } - } - args { - ty_app { - ty_func { - ty_ref { - local_ty_ref { - ty_name { name: "Bar" source_info { pos_from {} pos_to {} } } - source_info { pos_from {} pos_to {} } - } - } - } - ty_args { - ty_var { - var_name { name: "a" source_info { pos_from {} pos_to {} } } - } - } - source_info { pos_from {} pos_to {} } - } - } - source_info { pos_from {} pos_to {} } - } - cycled_constraints { - class_ref { - foreign_class_ref { - class_name { name: "Eq" source_info { pos_from {} pos_to {} } } - module_name { - parts { name: "Prelude" source_info { pos_from {} pos_to {} } } - source_info { pos_from {} pos_to {} } - } - source_info { pos_from {} pos_to {} } - } - } - args { - ty_app { - ty_func { - ty_ref { - local_ty_ref { - ty_name { name: "Baz" source_info { pos_from {} pos_to {} } } - source_info { pos_from {} pos_to {} } - } - } - } - ty_args { - ty_var { - var_name { name: "a" source_info { pos_from {} pos_to {} } } - } - } - source_info { pos_from {} pos_to {} } - } - } - source_info { pos_from {} pos_to {} } - } - } -} -ty_class_check_errors { - derive_opaque_err { - module_name { - parts { name: "Foo" source_info { pos_from {} pos_to {} } } - source_info { pos_from {} pos_to {} } - } - constraint { - class_ref { - foreign_class_ref { - class_name { name: "Ord" source_info { pos_from {} pos_to {} } } - module_name { - parts { name: "Prelude" source_info { pos_from {} pos_to {} } } - source_info { pos_from {} pos_to {} } - } - source_info { pos_from {} pos_to {} } - } - } - args { - ty_app { - ty_func { - ty_ref { - local_ty_ref { - ty_name { name: "Foo" source_info { pos_from {} pos_to {} } } - source_info { pos_from {} pos_to {} } - } - } - } - ty_args { - ty_var { - var_name { name: "a" source_info { pos_from {} pos_to {} } } - } - } - ty_args { - ty_var { - var_name { name: "b" source_info { pos_from {} pos_to {} } } - } - } - ty_args { - ty_var { - var_name { name: "c" source_info { pos_from {} pos_to {} } } - } - } - source_info { pos_from {} pos_to {} } - } - } - source_info { pos_from {} pos_to {} } - } - sub_constraint { - class_ref { - foreign_class_ref { - class_name { name: "Ord" source_info { pos_from {} pos_to {} } } - module_name { - parts { name: "Prelude" source_info { pos_from {} pos_to {} } } - source_info { pos_from {} pos_to {} } - } - source_info { pos_from {} pos_to {} } - } - } - args { - ty_app { - ty_func { - ty_ref { - local_ty_ref { - ty_name { name: "Bar" source_info { pos_from {} pos_to {} } } - source_info { pos_from {} pos_to {} } - } - } - } - ty_args { - ty_var { - var_name { name: "a" source_info { pos_from {} pos_to {} } } - } - } - source_info { pos_from {} pos_to {} } - } - } - source_info { pos_from {} pos_to {} } - } - } -} diff --git a/lambda-buffers-compiler/data/typeclasscheck-goldens/cycled_goals_1/foo.pl b/lambda-buffers-compiler/data/typeclasscheck-goldens/cycled_goals_1/foo.pl new file mode 100644 index 00000000..f91daa24 --- /dev/null +++ b/lambda-buffers-compiler/data/typeclasscheck-goldens/cycled_goals_1/foo.pl @@ -0,0 +1,125 @@ +:- module('Foo',['Prelude.Eq'/1,'Prelude.Ord'/1]). + +'Prelude.Ord'('Prelude.Int8') :- + 'Prelude.Eq'('Prelude.Int8'). + + +'Prelude.Ord'('Prelude.Bytes') :- + 'Prelude.Eq'('Prelude.Bytes'). + + +'Prelude.Ord'('app'('Prelude.Maybe','|'(Va,'[]'))) :- + 'Prelude.Ord'(Va),'Prelude.Eq'('app'('Prelude.Maybe','|'(Va,'[]'))). + + +'Prelude.Ord'('app'('Prelude.Map','|'(Va,'|'(Vb,'[]')))) :- + 'Prelude.Ord'(Va) + ,'Prelude.Ord'(Vb) + ,'Prelude.Eq'('app'('Prelude.Map','|'(Va,'|'(Vb,'[]')))). + + +'Prelude.Ord'('app'('Prelude.List','|'(Va,'[]'))) :- + 'Prelude.Ord'(Va),'Prelude.Eq'('app'('Prelude.List','|'(Va,'[]'))). + + +'Prelude.Ord'('app'('Prelude.Either','|'(Va,'|'(Vb,'[]')))) :- + 'Prelude.Ord'(Va) + ,'Prelude.Ord'(Vb) + ,'Prelude.Eq'('app'('Prelude.Either','|'(Va,'|'(Vb,'[]')))). + + +'Prelude.Ord'('app'('Foo.Foo','|'(Va,'|'(Vb,'|'(Vc,'[]'))))) :- + 'Prelude.Ord'('sum'('|'('ctor'('MkFoo' + ,'tuple'('|'('app'('Foo.Bar','|'(Va,'[]')) + ,'[]'))) + ,'[]'))) + ,'Prelude.Eq'('app'('Foo.Foo','|'(Va,'|'(Vb,'|'(Vc,'[]'))))). + + +'Prelude.Ord'('app'('Foo.Bar','|'(Va,'[]'))) :- + 'Prelude.Eq'(Va),'Prelude.Eq'('app'('Foo.Bar','|'(Va,'[]'))). + + +'Prelude.Ord'('var'(VX)). + + +'Prelude.Ord'('rec'('[]')). + + +'Prelude.Ord'('rec'('|'('field'(VFn,VFTy),VFs))) :- + 'Prelude.Ord'(VFTy),'Prelude.Ord'('rec'(VFs)). + + +'Prelude.Ord'('tuple'('[]')). + + +'Prelude.Ord'('tuple'('|'(VH,VT))) :- + 'Prelude.Ord'(VH),'Prelude.Ord'('tuple'(VT)). + + +'Prelude.Ord'('sum'('[]')). + + +'Prelude.Ord'('sum'('|'('ctor'(VC,VP),VT))) :- + 'Prelude.Ord'(VP),'Prelude.Ord'('sum'(VT)). + + +'Prelude.Eq'('Prelude.Int8'). + + +'Prelude.Eq'('Prelude.Bytes'). + + +'Prelude.Eq'('app'('Prelude.Maybe','|'(Va,'[]'))) :- + 'Prelude.Eq'(Va). + + +'Prelude.Eq'('app'('Prelude.Map','|'(Va,'|'(Vb,'[]')))) :- + 'Prelude.Eq'(Va),'Prelude.Eq'(Vb). + + +'Prelude.Eq'('app'('Prelude.List','|'(Va,'[]'))) :- + 'Prelude.Eq'(Va). + + +'Prelude.Eq'('app'('Prelude.Either','|'(Va,'|'(Vb,'[]')))) :- + 'Prelude.Eq'(Va),'Prelude.Eq'(Vb). + + +'Prelude.Eq'('app'('Foo.Foo','|'(Va,'|'(Vb,'|'(Vc,'[]'))))) :- + 'Prelude.Eq'('sum'('|'('ctor'('MkFoo' + ,'tuple'('|'('app'('Foo.Bar','|'(Va,'[]')) + ,'[]'))) + ,'[]'))). + + +'Prelude.Eq'('app'('Foo.Baz','|'(Va,'[]'))) :- + 'Prelude.Eq'('app'('Foo.Bar','|'(Va,'[]'))). + + +'Prelude.Eq'('app'('Foo.Bar','|'(Va,'[]'))) :- + 'Prelude.Eq'('app'('Foo.Baz','|'(Va,'[]'))). + + +'Prelude.Eq'('var'(VX)). + + +'Prelude.Eq'('rec'('[]')). + + +'Prelude.Eq'('rec'('|'('field'(VFn,VFTy),VFs))) :- + 'Prelude.Eq'(VFTy),'Prelude.Eq'('rec'(VFs)). + + +'Prelude.Eq'('tuple'('[]')). + + +'Prelude.Eq'('tuple'('|'(VH,VT))) :- + 'Prelude.Eq'(VH),'Prelude.Eq'('tuple'(VT)). + + +'Prelude.Eq'('sum'('[]')). + + +'Prelude.Eq'('sum'('|'('ctor'(VC,VP),VT))) :- + 'Prelude.Eq'(VP),'Prelude.Eq'('sum'(VT)). diff --git a/lambda-buffers-compiler/data/typeclasscheck-goldens/cycled_goals_1/prelude.pl b/lambda-buffers-compiler/data/typeclasscheck-goldens/cycled_goals_1/prelude.pl new file mode 100644 index 00000000..7a448703 --- /dev/null +++ b/lambda-buffers-compiler/data/typeclasscheck-goldens/cycled_goals_1/prelude.pl @@ -0,0 +1,98 @@ +:- module('Prelude',['Prelude.Eq'/1,'Prelude.Ord'/1]). + +'Prelude.Ord'('Prelude.Int8') :- + 'Prelude.Eq'('Prelude.Int8'). + + +'Prelude.Ord'('Prelude.Bytes') :- + 'Prelude.Eq'('Prelude.Bytes'). + + +'Prelude.Ord'('app'('Prelude.Maybe','|'(Va,'[]'))) :- + 'Prelude.Ord'(Va),'Prelude.Eq'('app'('Prelude.Maybe','|'(Va,'[]'))). + + +'Prelude.Ord'('app'('Prelude.Map','|'(Va,'|'(Vb,'[]')))) :- + 'Prelude.Ord'(Va) + ,'Prelude.Ord'(Vb) + ,'Prelude.Eq'('app'('Prelude.Map','|'(Va,'|'(Vb,'[]')))). + + +'Prelude.Ord'('app'('Prelude.List','|'(Va,'[]'))) :- + 'Prelude.Ord'(Va),'Prelude.Eq'('app'('Prelude.List','|'(Va,'[]'))). + + +'Prelude.Ord'('app'('Prelude.Either','|'(Va,'|'(Vb,'[]')))) :- + 'Prelude.Ord'(Va) + ,'Prelude.Ord'(Vb) + ,'Prelude.Eq'('app'('Prelude.Either','|'(Va,'|'(Vb,'[]')))). + + +'Prelude.Ord'('var'(VX)). + + +'Prelude.Ord'('rec'('[]')). + + +'Prelude.Ord'('rec'('|'('field'(VFn,VFTy),VFs))) :- + 'Prelude.Ord'(VFTy),'Prelude.Ord'('rec'(VFs)). + + +'Prelude.Ord'('tuple'('[]')). + + +'Prelude.Ord'('tuple'('|'(VH,VT))) :- + 'Prelude.Ord'(VH),'Prelude.Ord'('tuple'(VT)). + + +'Prelude.Ord'('sum'('[]')). + + +'Prelude.Ord'('sum'('|'('ctor'(VC,VP),VT))) :- + 'Prelude.Ord'(VP),'Prelude.Ord'('sum'(VT)). + + +'Prelude.Eq'('Prelude.Int8'). + + +'Prelude.Eq'('Prelude.Bytes'). + + +'Prelude.Eq'('app'('Prelude.Maybe','|'(Va,'[]'))) :- + 'Prelude.Eq'(Va). + + +'Prelude.Eq'('app'('Prelude.Map','|'(Va,'|'(Vb,'[]')))) :- + 'Prelude.Eq'(Va),'Prelude.Eq'(Vb). + + +'Prelude.Eq'('app'('Prelude.List','|'(Va,'[]'))) :- + 'Prelude.Eq'(Va). + + +'Prelude.Eq'('app'('Prelude.Either','|'(Va,'|'(Vb,'[]')))) :- + 'Prelude.Eq'(Va),'Prelude.Eq'(Vb). + + +'Prelude.Eq'('var'(VX)). + + +'Prelude.Eq'('rec'('[]')). + + +'Prelude.Eq'('rec'('|'('field'(VFn,VFTy),VFs))) :- + 'Prelude.Eq'(VFTy),'Prelude.Eq'('rec'(VFs)). + + +'Prelude.Eq'('tuple'('[]')). + + +'Prelude.Eq'('tuple'('|'(VH,VT))) :- + 'Prelude.Eq'(VH),'Prelude.Eq'('tuple'(VT)). + + +'Prelude.Eq'('sum'('[]')). + + +'Prelude.Eq'('sum'('|'('ctor'(VC,VP),VT))) :- + 'Prelude.Eq'(VP),'Prelude.Eq'('sum'(VT)). diff --git a/lambda-buffers-compiler/data/typeclasscheck-goldens/cycled_goals_2/foo.pl b/lambda-buffers-compiler/data/typeclasscheck-goldens/cycled_goals_2/foo.pl new file mode 100644 index 00000000..b22525f9 --- /dev/null +++ b/lambda-buffers-compiler/data/typeclasscheck-goldens/cycled_goals_2/foo.pl @@ -0,0 +1,143 @@ +:- module('Foo',['Prelude.Eq'/1,'Prelude.Ord'/1]). + +'Prelude.Ord'('Prelude.Int8') :- + 'Prelude.Eq'('Prelude.Int8'). + + +'Prelude.Ord'('Prelude.Bytes') :- + 'Prelude.Eq'('Prelude.Bytes'). + + +'Prelude.Ord'('app'('Prelude.Maybe','|'(Va,'[]'))) :- + 'Prelude.Ord'(Va),'Prelude.Eq'('app'('Prelude.Maybe','|'(Va,'[]'))). + + +'Prelude.Ord'('app'('Prelude.Map','|'(Va,'|'(Vb,'[]')))) :- + 'Prelude.Ord'(Va) + ,'Prelude.Ord'(Vb) + ,'Prelude.Eq'('app'('Prelude.Map','|'(Va,'|'(Vb,'[]')))). + + +'Prelude.Ord'('app'('Prelude.List','|'(Va,'[]'))) :- + 'Prelude.Ord'(Va),'Prelude.Eq'('app'('Prelude.List','|'(Va,'[]'))). + + +'Prelude.Ord'('app'('Prelude.Either','|'(Va,'|'(Vb,'[]')))) :- + 'Prelude.Ord'(Va) + ,'Prelude.Ord'(Vb) + ,'Prelude.Eq'('app'('Prelude.Either','|'(Va,'|'(Vb,'[]')))). + + +'Prelude.Ord'('app'('Foo.Foo','|'(Va,'|'(Vb,'[]')))) :- + 'Prelude.Ord'('sum'('|'('ctor'('FooA' + ,'tuple'('|'('app'('Foo.Foo' + ,'|'(Va,'|'(Vb,'[]'))) + ,'[]'))) + ,'|'('ctor'('FooB' + ,'tuple'('|'('app'('Foo.Foo' + ,'|'(Va,'|'(Vb,'[]'))) + ,'[]'))) + ,'[]')))) + ,'Prelude.Eq'('app'('Foo.Foo','|'(Va,'|'(Vb,'[]')))). + + +'Prelude.Ord'('app'('Foo.Baz','|'(Va,'|'(Vb,'[]')))) :- + 'Prelude.Ord'('rec'('|'('field'('baz','app'('Foo.Baz','|'(Va,'|'(Vb,'[]')))) + ,'[]'))) + ,'Prelude.Eq'('app'('Foo.Baz','|'(Va,'|'(Vb,'[]')))). + + +'Prelude.Ord'('app'('Foo.Bar','|'(Va,'[]'))) :- + 'Prelude.Ord'('tuple'('|'('app'('Foo.Bar','|'(Va,'[]')),'[]'))) + ,'Prelude.Eq'('app'('Foo.Bar','|'(Va,'[]'))). + + +'Prelude.Ord'('var'(VX)). + + +'Prelude.Ord'('rec'('[]')). + + +'Prelude.Ord'('rec'('|'('field'(VFn,VFTy),VFs))) :- + 'Prelude.Ord'(VFTy),'Prelude.Ord'('rec'(VFs)). + + +'Prelude.Ord'('tuple'('[]')). + + +'Prelude.Ord'('tuple'('|'(VH,VT))) :- + 'Prelude.Ord'(VH),'Prelude.Ord'('tuple'(VT)). + + +'Prelude.Ord'('sum'('[]')). + + +'Prelude.Ord'('sum'('|'('ctor'(VC,VP),VT))) :- + 'Prelude.Ord'(VP),'Prelude.Ord'('sum'(VT)). + + +'Prelude.Eq'('Prelude.Int8'). + + +'Prelude.Eq'('Prelude.Bytes'). + + +'Prelude.Eq'('app'('Prelude.Maybe','|'(Va,'[]'))) :- + 'Prelude.Eq'(Va). + + +'Prelude.Eq'('app'('Prelude.Map','|'(Va,'|'(Vb,'[]')))) :- + 'Prelude.Eq'(Va),'Prelude.Eq'(Vb). + + +'Prelude.Eq'('app'('Prelude.List','|'(Va,'[]'))) :- + 'Prelude.Eq'(Va). + + +'Prelude.Eq'('app'('Prelude.Either','|'(Va,'|'(Vb,'[]')))) :- + 'Prelude.Eq'(Va),'Prelude.Eq'(Vb). + + +'Prelude.Eq'('app'('Foo.Foo','|'(Va,'|'(Vb,'[]')))) :- + 'Prelude.Eq'('sum'('|'('ctor'('FooA' + ,'tuple'('|'('app'('Foo.Foo' + ,'|'(Va,'|'(Vb,'[]'))) + ,'[]'))) + ,'|'('ctor'('FooB' + ,'tuple'('|'('app'('Foo.Foo' + ,'|'(Va,'|'(Vb,'[]'))) + ,'[]'))) + ,'[]')))). + + +'Prelude.Eq'('app'('Foo.Baz','|'(Va,'|'(Vb,'[]')))) :- + 'Prelude.Eq'('rec'('|'('field'('baz','app'('Foo.Baz','|'(Va,'|'(Vb,'[]')))) + ,'[]'))). + + +'Prelude.Eq'('app'('Foo.Bar','|'(Va,'[]'))) :- + 'Prelude.Eq'('tuple'('|'('app'('Foo.Bar','|'(Va,'[]')),'[]'))). + + +'Prelude.Eq'('var'(VX)). + + +'Prelude.Eq'('rec'('[]')). + + +'Prelude.Eq'('rec'('|'('field'(VFn,VFTy),VFs))) :- + 'Prelude.Eq'(VFTy),'Prelude.Eq'('rec'(VFs)). + + +'Prelude.Eq'('tuple'('[]')). + + +'Prelude.Eq'('tuple'('|'(VH,VT))) :- + 'Prelude.Eq'(VH),'Prelude.Eq'('tuple'(VT)). + + +'Prelude.Eq'('sum'('[]')). + + +'Prelude.Eq'('sum'('|'('ctor'(VC,VP),VT))) :- + 'Prelude.Eq'(VP),'Prelude.Eq'('sum'(VT)). diff --git a/lambda-buffers-compiler/data/typeclasscheck-goldens/cycled_goals_2/prelude.pl b/lambda-buffers-compiler/data/typeclasscheck-goldens/cycled_goals_2/prelude.pl new file mode 100644 index 00000000..7a448703 --- /dev/null +++ b/lambda-buffers-compiler/data/typeclasscheck-goldens/cycled_goals_2/prelude.pl @@ -0,0 +1,98 @@ +:- module('Prelude',['Prelude.Eq'/1,'Prelude.Ord'/1]). + +'Prelude.Ord'('Prelude.Int8') :- + 'Prelude.Eq'('Prelude.Int8'). + + +'Prelude.Ord'('Prelude.Bytes') :- + 'Prelude.Eq'('Prelude.Bytes'). + + +'Prelude.Ord'('app'('Prelude.Maybe','|'(Va,'[]'))) :- + 'Prelude.Ord'(Va),'Prelude.Eq'('app'('Prelude.Maybe','|'(Va,'[]'))). + + +'Prelude.Ord'('app'('Prelude.Map','|'(Va,'|'(Vb,'[]')))) :- + 'Prelude.Ord'(Va) + ,'Prelude.Ord'(Vb) + ,'Prelude.Eq'('app'('Prelude.Map','|'(Va,'|'(Vb,'[]')))). + + +'Prelude.Ord'('app'('Prelude.List','|'(Va,'[]'))) :- + 'Prelude.Ord'(Va),'Prelude.Eq'('app'('Prelude.List','|'(Va,'[]'))). + + +'Prelude.Ord'('app'('Prelude.Either','|'(Va,'|'(Vb,'[]')))) :- + 'Prelude.Ord'(Va) + ,'Prelude.Ord'(Vb) + ,'Prelude.Eq'('app'('Prelude.Either','|'(Va,'|'(Vb,'[]')))). + + +'Prelude.Ord'('var'(VX)). + + +'Prelude.Ord'('rec'('[]')). + + +'Prelude.Ord'('rec'('|'('field'(VFn,VFTy),VFs))) :- + 'Prelude.Ord'(VFTy),'Prelude.Ord'('rec'(VFs)). + + +'Prelude.Ord'('tuple'('[]')). + + +'Prelude.Ord'('tuple'('|'(VH,VT))) :- + 'Prelude.Ord'(VH),'Prelude.Ord'('tuple'(VT)). + + +'Prelude.Ord'('sum'('[]')). + + +'Prelude.Ord'('sum'('|'('ctor'(VC,VP),VT))) :- + 'Prelude.Ord'(VP),'Prelude.Ord'('sum'(VT)). + + +'Prelude.Eq'('Prelude.Int8'). + + +'Prelude.Eq'('Prelude.Bytes'). + + +'Prelude.Eq'('app'('Prelude.Maybe','|'(Va,'[]'))) :- + 'Prelude.Eq'(Va). + + +'Prelude.Eq'('app'('Prelude.Map','|'(Va,'|'(Vb,'[]')))) :- + 'Prelude.Eq'(Va),'Prelude.Eq'(Vb). + + +'Prelude.Eq'('app'('Prelude.List','|'(Va,'[]'))) :- + 'Prelude.Eq'(Va). + + +'Prelude.Eq'('app'('Prelude.Either','|'(Va,'|'(Vb,'[]')))) :- + 'Prelude.Eq'(Va),'Prelude.Eq'(Vb). + + +'Prelude.Eq'('var'(VX)). + + +'Prelude.Eq'('rec'('[]')). + + +'Prelude.Eq'('rec'('|'('field'(VFn,VFTy),VFs))) :- + 'Prelude.Eq'(VFTy),'Prelude.Eq'('rec'(VFs)). + + +'Prelude.Eq'('tuple'('[]')). + + +'Prelude.Eq'('tuple'('|'(VH,VT))) :- + 'Prelude.Eq'(VH),'Prelude.Eq'('tuple'(VT)). + + +'Prelude.Eq'('sum'('[]')). + + +'Prelude.Eq'('sum'('|'('ctor'(VC,VP),VT))) :- + 'Prelude.Eq'(VP),'Prelude.Eq'('sum'(VT)). diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/MiniLog.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/MiniLog.hs index f412f536..d2711a3d 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/MiniLog.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/MiniLog.hs @@ -81,8 +81,6 @@ data MiniLogError f a MissingClauseError (Term f a) | -- | Multiple overlapping `Clauses` were found. OverlappingClausesError [Clause f a] (Term f a) - | -- | A goal cycle was detected. - CycledGoalsError [Term f a] | -- | Implementation/provider internal error conditions. InternalError Text deriving stock (Eq, Ord, Show) diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/MiniLog/UniFdSolver.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/MiniLog/UniFdSolver.hs index 2d60af4c..4e04b0d3 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/MiniLog/UniFdSolver.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/MiniLog/UniFdSolver.hs @@ -1,7 +1,7 @@ -- | unification-fd based solver. module LambdaBuffers.Compiler.MiniLog.UniFdSolver (solve) where -import Control.Monad (filterM, foldM, foldM_, void) +import Control.Monad (filterM, foldM) import Control.Monad.Error.Class (MonadError (catchError, throwError)) import Control.Monad.Except (ExceptT, runExceptT) import Control.Monad.Reader (MonadReader (local), ReaderT (runReaderT), asks) @@ -13,6 +13,7 @@ import Control.Unification qualified as Unif import Control.Unification.IntVar (IntBindingT, IntVar, runIntBindingT) import Data.Map (Map) import Data.Map qualified as Map +import Data.Maybe (isJust) import Data.Text qualified as Text import LambdaBuffers.Compiler.MiniLog qualified as ML @@ -100,11 +101,12 @@ solveGoal goal' = do mlGoal <- fromUTerm goal trace $ ML.SolveGoal mlGoal clause <- lookupClause goal - checkCycle goal - g <- duplicateTerm goal - _ <- local (\r -> r {cctxTrace = g : cctxTrace r}) (callClause clause goal) + mayAncestor <- checkCycle goal + retGoal <- case mayAncestor of + Nothing -> local (\r -> r {cctxTrace = goal : cctxTrace r}) (callClause clause goal) + Just ancestorGoal -> ancestorGoal `unify` goal trace $ ML.DoneGoal mlGoal - return goal + return retGoal {- | In functional speak, this is like a function call (application), where clause is a function and a goal is the argument. We simply `interpretClause` and unify the given argument with the head of the clause. @@ -115,34 +117,39 @@ callClause clause arg = do mlArg <- fromUTerm arg trace $ ML.CallClause clause mlArg (clauseHead', clauseBody') <- interpretClause clause - clauseHead' `unify` arg + retGoal <- clauseHead' `unify` arg _ <- solveGoal `traverse` clauseBody' trace $ ML.DoneClause clause mlArg - return clauseHead' + return retGoal {- | Checks if the supplied goal was already visited. - TODO(bladyjoker): Revisit this topic, perhaps this shouldn't error out rather it could just terminate with solutions. + + References: + - https://www.swi-prolog.org/pldoc/doc/_SWI_/library/coinduction.pl + - https://personal.utdallas.edu/~gupta/courses/acl/2021/other-papers/colp.pdf + - https://arxiv.org/pdf/1511.09394.pdf -} -checkCycle :: (Eq fun, Eq atom, Show fun, Show atom) => UTerm fun atom -> UniM fun atom () +checkCycle :: (Eq fun, Eq atom, Show fun, Show atom) => UTerm fun atom -> UniM fun atom (Maybe (UTerm fun atom)) checkCycle goal = do visitedGoals <- asks cctxTrace - foldM_ + foldM ( \mayCycle visited -> do - visited' <- duplicateTerm visited - goal' <- duplicateTerm goal - catchError - ( do - goal' `unify` visited' -- NOTE(bladyjoker): Perhaps subsumes? - fromUTerm goal >>= throwError . MLError . ML.CycledGoalsError . (: mayCycle) - ) - ( \case - MismatchFailure _ _ -> do - checked <- fromUTerm visited - return (checked : mayCycle) - err -> throwError err - ) + if isJust mayCycle + then return mayCycle + else do + visited' <- duplicateTerm visited + goal' <- duplicateTerm goal + catchError + ( do + _ <- goal' `unify` visited' + return $ Just visited + ) + ( \case + MismatchFailure _ _ -> return mayCycle + err -> throwError err + ) ) - mempty + Nothing visitedGoals {- | Given a unifiable term and the knowledge base (clauses) find a next `MiniLog.Clause` to `callClause` on. @@ -246,10 +253,10 @@ trace x = lift . lift . lift $ tell [x] force :: (Eq fun, Eq atom) => UTerm fun atom -> UniM fun atom (UTerm fun atom) force = lift . U.applyBindings -unify :: (Eq fun, Eq atom, Show atom, Show fun) => UTerm fun atom -> UTerm fun atom -> UniM fun atom () +unify :: (Eq fun, Eq atom, Show atom, Show fun) => UTerm fun atom -> UTerm fun atom -> UniM fun atom (UTerm fun atom) unify l r = do debug ("unify" :: String, l, r) - void $ lift $ Unif.unify l r + lift $ Unif.unify l r freeVar :: (Eq fun, Eq atom) => UniM fun atom (UTerm fun atom) freeVar = U.UVar <$> freeVar' diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/TypeClassCheck/Errors.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/TypeClassCheck/Errors.hs index 6f9881ca..c931d4e9 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/TypeClassCheck/Errors.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/TypeClassCheck/Errors.hs @@ -4,7 +4,6 @@ module LambdaBuffers.Compiler.TypeClassCheck.Errors ( superClassCycleDetectedError, unboundTyClassRefError', deriveOpaqueError, - cycledGoalsError, missingRuleError, internalError, internalError', @@ -60,14 +59,6 @@ deriveOpaqueError locMn cstr subCstr = & P.deriveOpaqueErr . P.constraint .~ PC.toProto cstr & P.deriveOpaqueErr . P.subConstraint .~ PC.toProto subCstr -cycledGoalsError :: PC.ModuleName -> PC.Constraint -> [PC.Constraint] -> P.CompilerError -cycledGoalsError locMn cstr cycledConstraints = - tyClassCheckError $ - defMessage - & P.constraintCycleErr . P.moduleName .~ PC.toProto locMn - & P.constraintCycleErr . P.constraint .~ PC.toProto cstr - & P.constraintCycleErr . P.cycledConstraints .~ (PC.toProto <$> cycledConstraints) - missingRuleError :: PC.ModuleName -> PC.Constraint -> PC.Constraint -> P.CompilerError missingRuleError locMn cstr subCstr = tyClassCheckError $ diff --git a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/TypeClassCheck/MiniLog.hs b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/TypeClassCheck/MiniLog.hs index 095e5052..81c1b7c7 100644 --- a/lambda-buffers-compiler/src/LambdaBuffers/Compiler/TypeClassCheck/MiniLog.hs +++ b/lambda-buffers-compiler/src/LambdaBuffers/Compiler/TypeClassCheck/MiniLog.hs @@ -17,7 +17,6 @@ import Control.Lens (view, (^.)) import Data.Default (Default (def)) import Data.Map qualified as Map import Data.Map.Ordered qualified as OMap -import Data.Maybe (maybeToList) import Data.Text (Text) import LambdaBuffers.Compiler.MiniLog ((@), (@<=)) import LambdaBuffers.Compiler.MiniLog qualified as ML @@ -26,7 +25,7 @@ import LambdaBuffers.Compiler.ProtoCompat qualified as PC import LambdaBuffers.Compiler.ProtoCompat.Eval qualified as E import LambdaBuffers.Compiler.ProtoCompat.Indexing qualified as PC import LambdaBuffers.Compiler.ProtoCompat.Utils qualified as PC -import LambdaBuffers.Compiler.TypeClassCheck.Errors (cycledGoalsError, deriveOpaqueError, internalError, internalError', mappendErrs, memptyErr, missingRuleError, overlappingRulesError, unboundTyClassRefError') +import LambdaBuffers.Compiler.TypeClassCheck.Errors (deriveOpaqueError, internalError, internalError', mappendErrs, memptyErr, missingRuleError, overlappingRulesError, unboundTyClassRefError') import Proto.Compiler qualified as P type Term = ML.Term Funct Atom @@ -305,9 +304,6 @@ runSolve' locMn clauses goal = do -- | Convert to API errors. fromMiniLogError :: PC.ModuleName -> PC.Constraint -> [ML.MiniLogTrace Funct Atom] -> ML.MiniLogError Funct Atom -> P.CompilerError -fromMiniLogError locMn currentCstr _trace (ML.CycledGoalsError gs) = - let userDefinedGoals = [c | g <- gs, c <- maybeToList (goalToConstraint locMn g)] - in cycledGoalsError locMn currentCstr userDefinedGoals fromMiniLogError locMn currentCstr _trace err@(ML.OverlappingClausesError clauses goal) = case originalConstraint `traverse` clauses of Nothing -> internalError locMn currentCstr ("Failed extracting the original `Constraint` when constructing a report for the `OverlappingRulesError`" <> show err) diff --git a/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler/MiniLog.hs b/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler/MiniLog.hs index 4c1b9da0..7469522d 100644 --- a/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler/MiniLog.hs +++ b/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler/MiniLog.hs @@ -3,7 +3,7 @@ module Test.LambdaBuffers.Compiler.MiniLog (test) where import Control.Monad (void) import Data.Map qualified as Map import Data.Text qualified as Text -import LambdaBuffers.Compiler.MiniLog (Clause, MiniLogError (CycledGoalsError, MissingClauseError, OverlappingClausesError), Term (Atom, Struct, Var), VarName, (@<=)) +import LambdaBuffers.Compiler.MiniLog (Clause, MiniLogError (MissingClauseError, OverlappingClausesError), Term (Atom, Struct, Var), VarName, (@<=)) import LambdaBuffers.Compiler.MiniLog.Pretty (toPrologModule) import LambdaBuffers.Compiler.MiniLog.UniFdSolver (solve) import System.FilePath ((<.>)) @@ -17,7 +17,7 @@ test = adjustOption (\_ -> H.HedgehogTestLimit $ Just 1000) $ testGroup "LambdaBuffers.Compiler.MiniLog checks" - [shouldSolve, shouldFailToSolve, printingToPrologTests] + [shouldSolve, overlapTests, printingToPrologTests, missingClauseTests, cycleTests] printingToPrologTests :: TestTree printingToPrologTests = @@ -31,10 +31,62 @@ printingToPrologTests = , shouldPrint "very_long_arguments" [Struct "foo" (replicate 50 (Var "X")) @<= replicate 2 (Struct "foo" (replicate 50 (Var "X")))] ] -shouldFailToSolve :: TestTree -shouldFailToSolve = +cycleTests :: TestTree +cycleTests = testGroup - "Should fail to solve" + "Cycle tests" + [ testCase "cycle.pl ?- eq(beep(int))." $ + succeedsWith + cycleKnowledge + [eq (Struct "beep" [Atom "int"])] + [] + , testCase "cycle.pl ?- eq(beep(X))." $ + succeedsWith + cycleKnowledge + [eq (Struct "beep" [Var "X"])] + [("X", Var "-9223372036854775808")] + , testCase "cycle.pl ?- eq(foo(int))." $ + succeedsWith + cycleKnowledge + [eq (Struct "foo" [Atom "int"])] + [] + , testCase "cycle.pl ?- eq(list(list(int)))." $ + succeedsWith + cycleKnowledge + [eq (Struct "list" [Struct "list" [Atom "int"]])] + mempty + , testCase "cycle.pl ?- eq(list(list(list(int))))." $ + succeedsWith + cycleKnowledge + [eq (Struct "list" [Struct "list" [Struct "list" [Atom "int"]]])] + mempty + , testCase "cycle.pl ?- eq(rectype)." $ + succeedsWith + cycleKnowledge + [eq (Struct "rectype" [])] + mempty + ] + +missingClauseTests :: TestTree +missingClauseTests = + testGroup + "Should fail to solve with because overlapping rules" + [ testCase "greeks.pl ?- animal(aristotle). % missing goal human(ariostotle)" $ + failsWith + greekKnowledge + [animal (Atom "aristotle")] + (missesClauseFor (human (Atom "aristotle"))) + , testCase "greeks.pl ?- animal(plato), animal(socrates), human(plato), human(socrates), animal(aristotle) % missing goal human(aristotle)" $ + failsWith + greekKnowledge + [animal (Atom "plato"), animal (Atom "socrates"), human (Atom "plato"), human (Atom "socrates"), animal (Atom "aristotle")] + (missesClauseFor (human (Atom "aristotle"))) + ] + +overlapTests :: TestTree +overlapTests = + testGroup + "Should fail to solve with because overlapping rules" [ testCase "greeks.pl ?- animal(X). % overlaps on human(plato|socrates)" $ failsWith greekKnowledge @@ -55,11 +107,6 @@ shouldFailToSolve = greekKnowledge [human (Var "X"), human (Var "Y")] (overlapsOn [socratesIsHuman, platoIsHuman]) - , testCase "greeks.pl ?- animal(aristotle). % missing goal human(ariostotle)" $ - failsWith - greekKnowledge - [animal (Atom "aristotle")] - (missesClauseFor (human (Atom "aristotle"))) , testCase "human(plato).;human(plato). greeks.pl ?- human(plato). % overlaps on human(plato|socrates)" $ failsWith (platoIsHuman : greekKnowledge) @@ -80,21 +127,6 @@ shouldFailToSolve = eqTypeClassKnowledge [eq (Struct "maybe" [Var "X"])] (overlapsOn eqTypeClassKnowledge) - , testCase "greeks.pl ?- animal(plato), animal(socrates), human(plato), human(socrates), animal(aristotle) % missing goal human(aristotle)" $ - failsWith - greekKnowledge - [animal (Atom "plato"), animal (Atom "socrates"), human (Atom "plato"), human (Atom "socrates"), animal (Atom "aristotle")] - (missesClauseFor (human (Atom "aristotle"))) - , testCase "cycle.pl ?- eq(beep(int))." $ - failsWith - cycleKnowledge - [eq (Struct "beep" [Atom "int"])] - (cycledGoals [eq (Struct "beep" [Atom "int"])]) - , testCase "cycle.pl ?- eq(foo(int))." $ - failsWith - cycleKnowledge - [eq (Struct "foo" [Atom "int"])] - (cycledGoals [eq (Struct "foo" [Atom "int"]), eq (Struct "bar" [Atom "int"]), eq (Struct "baz" [Atom "int"])]) ] shouldSolve :: TestTree @@ -176,16 +208,6 @@ shouldSolve = eqTypeClassKnowledge [eq (Atom "int")] mempty - , testCase "cycle.pl ?- eq(list(list(int)))." $ - succeedsWith - cycleKnowledge - [eq (Struct "list" [Struct "list" [Atom "int"]])] - mempty - , testCase "cycle.pl ?- eq(list(list(list(int))))." $ - succeedsWith - cycleKnowledge - [eq (Struct "list" [Struct "list" [Struct "list" [Atom "int"]]])] - mempty ] type TestTerm = Term String String @@ -280,6 +302,7 @@ cycleKnowledge = , eq (Struct "bar" [Var "X"]) @<= [eq (Struct "baz" [Var "X"])] , eq (Struct "baz" [Var "X"]) @<= [eq (Struct "foo" [Var "X"])] , eq (Struct "beep" [Var "X"]) @<= [eq (Struct "beep" [Var "X"])] + , eq (Struct "rectype" []) @<= [eq (Atom "int"), eq (Struct "rectype" [])] , eq (Atom "int") @<= [] ] @@ -320,10 +343,6 @@ missesClauseFor :: TestTerm -> MiniLogError String String -> Bool missesClauseFor goal' (MissingClauseError goal) = goal' == goal missesClauseFor _ _ = False -cycledGoals :: [TestTerm] -> MiniLogError String String -> Bool -cycledGoals goals' (CycledGoalsError goals) = goals' == goals -cycledGoals _ _ = False - printLogs :: (Traversable t, Show a) => t a -> Assertion printLogs logs = do putStrLn "" diff --git a/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler/TypeClassCheck.hs b/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler/TypeClassCheck.hs index cb99e759..3ff02f0e 100644 --- a/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler/TypeClassCheck.hs +++ b/lambda-buffers-compiler/test/Test/LambdaBuffers/Compiler/TypeClassCheck.hs @@ -28,12 +28,16 @@ test = "Should fail" [ fails "derive_opaque_1" testDeriveOpaque1 , fails "derive_opaque_2" testDeriveOpaque2 - , fails "cycled_goals_1" testCycledGoals1 , fails "missing_rule_1" testMissingRule1 , fails "missing_rule_2" testMissingRule2 , fails "missing_rule_3" testMissingRule3 , fails "overlapping_rules_1" testOverlaps1 ] + , testGroup + "Cycled goals should succeed" + [ succeeds "cycled_goals_1" testCycledGoals1 + , succeeds "cycled_goals_2" testCycledGoals2 + ] ] {- Test 1 - should succeed @@ -448,7 +452,7 @@ testDeriveOpaque2 = [["Prelude"]] ] -{- Test Cycled goals 1 - a cycle should fail +{- Test Cycled goals 1 - a cycle should succeed module Foo @@ -457,7 +461,7 @@ import Prelude opaque Bar a instance Eq (Baz a) => Eq (Bar a) -derive Ord (Bar a) +instance (Eq a) => Ord (Bar a) opaque Baz a @@ -487,14 +491,62 @@ testCycledGoals1 = [] [ U.inst' (eqCstr (U.lr "Bar" U.@ [U.tv "a"])) [eqCstr (U.lr "Baz" U.@ [U.tv "a"])] , U.inst' (eqCstr (U.lr "Baz" U.@ [U.tv "a"])) [eqCstr (U.lr "Bar" U.@ [U.tv "a"])] + , U.inst' (ordCstr (U.lr "Bar" U.@ [U.tv "a"])) [eqCstr (U.tv "a")] ] - [ deriveOrd (U.lr "Bar" U.@ [U.tv "a"]) - , deriveEq (U.lr "Foo" U.@ [U.tv "a", U.tv "b", U.tv "c"]) + [ deriveEq (U.lr "Foo" U.@ [U.tv "a", U.tv "b", U.tv "c"]) , deriveOrd (U.lr "Foo" U.@ [U.tv "a", U.tv "b", U.tv "c"]) ] [["Prelude"]] ] +{- Test Cycled goals 1 - a cycle should succeed on recursive types + +module Foo + +import Prelude + +prod Bar a = Bar a + +derive Eq (Bar a) + +record Baz a b = { baz : Baz a b} + +derive Eq (Baz a b) + +sum Foo a b = FooA (Foo a b) | FooB (Foo a b) + +derive Eq (Foo a b) +derive Ord (Foo a b) +-} +testCycledGoals2 :: PC.CompilerInput +testCycledGoals2 = + U.ci + [ U.mod'preludeO + , U.mod' + ["Foo"] + [ U.td "Bar" (U.abs ["a"] $ U.prod' [U.lr "Bar" U.@ [U.tv "a"]]) + , U.td "Baz" (U.abs ["a", "b"] $ U.recrd [("baz", U.lr "Baz" U.@ [U.tv "a", U.tv "b"])]) + , U.td + "Foo" + ( U.abs ["a", "b"] $ + U.sum + [ ("FooA", [U.lr "Foo" U.@ [U.tv "a", U.tv "b"]]) + , ("FooB", [U.lr "Foo" U.@ [U.tv "a", U.tv "b"]]) + ] + ) + ] + [] + [] + [ deriveEq (U.lr "Bar" U.@ [U.tv "a"]) + , deriveOrd (U.lr "Bar" U.@ [U.tv "a"]) + , deriveEq (U.lr "Foo" U.@ [U.tv "a", U.tv "b"]) + , deriveOrd (U.lr "Foo" U.@ [U.tv "a", U.tv "b"]) + , deriveEq (U.lr "Baz" U.@ [U.tv "a", U.tv "b"]) + , deriveOrd (U.lr "Baz" U.@ [U.tv "a", U.tv "b"]) + ] + [["Prelude"]] + ] + {- Test Missing Rule1 - should fail module Foo diff --git a/lambda-buffers-frontend/data/goldens/good/PreludeT.lbf b/lambda-buffers-frontend/data/goldens/good/PreludeT.lbf index 62759c21..edc0d7f2 100644 --- a/lambda-buffers-frontend/data/goldens/good/PreludeT.lbf +++ b/lambda-buffers-frontend/data/goldens/good/PreludeT.lbf @@ -1,7 +1,15 @@ module PreludeT +import Prelude (Eq) + sum Maybe a = Just a | Nothing +derive Eq (Maybe a) + sum Either a b = Left a | Right b -sum List a = Nil | Cons a (List a) \ No newline at end of file +derive Eq (Either a b) + +sum List a = Nil | Cons a (List a) + +instance Eq (List a) :- Eq a \ No newline at end of file diff --git a/lambda-buffers-frontend/data/goldens/good/Rules.lbf b/lambda-buffers-frontend/data/goldens/good/Rules.lbf new file mode 100644 index 00000000..97923901 --- /dev/null +++ b/lambda-buffers-frontend/data/goldens/good/Rules.lbf @@ -0,0 +1,23 @@ +module Rules + +import Prelude + +class (Eq a) <= Ord a + +prod X = X + +derive Eq X + +derive Ord X + +prod OddList a = a (EvenList a) + +instance Eq (OddList a) :- Eq a,Eq (EvenList a) + +derive Ord (OddList a) + +sum EvenList a = Nil | ECons a (OddList a) + +instance Eq (EvenList a) :- Eq a,Eq (OddList a) + +derive Ord (EvenList a) \ No newline at end of file diff --git a/lambda-buffers-frontend/data/run.sh b/lambda-buffers-frontend/data/run.sh index 2665fb61..7160aeca 100755 --- a/lambda-buffers-frontend/data/run.sh +++ b/lambda-buffers-frontend/data/run.sh @@ -1,6 +1,6 @@ #!/bin/bash function lbf { - cabal run lbf -- $@ + cabal run lbf -- $@ } function lbf-comp { @@ -41,6 +41,11 @@ lbf-comp -w goldens/good/work-dir -i goldens/good -f goldens/good/Plutus.lbf lbf-form goldens/good/Plutus.lbf lbf-comp -w goldens/good/work-dir -i goldens/good -f goldens/good/Plutus.lbf +echo "goldens/good/Rules.lbf" +lbf-comp -w goldens/good/work-dir -i goldens/good -f goldens/good/Rules.lbf +lbf-form goldens/good/Rules.lbf +lbf-comp -w goldens/good/work-dir -i goldens/good -f goldens/good/Rules.lbf + echo "goldens/good/LambdaBuffers.lbf" lbf-comp -w goldens/good/work-dir -i goldens/good -f goldens/good/LambdaBuffers.lbf lbf-form goldens/good/LambdaBuffers.lbf diff --git a/lambda-buffers-proto/compiler.proto b/lambda-buffers-proto/compiler.proto index 93699b8b..7a8c5291 100644 --- a/lambda-buffers-proto/compiler.proto +++ b/lambda-buffers-proto/compiler.proto @@ -785,14 +785,6 @@ message TyClassCheckError { Constraint sub_constraint = 3; } - // In `module_name` a cycle of `cycled_constraints` was detected while trying - // to solve `constraint`. - message ConstraintCycleError { - ModuleName module_name = 1; - Constraint constraint = 2; - repeated Constraint cycled_constraints = 3; - } - // In `module_name` while trying to solve `constraint` it wasn't possible to // find a rule (`Derive` or `InstanceClause`) for `sub_constraint`. message MissingRuleError { @@ -823,9 +815,8 @@ message TyClassCheckError { SuperclassCycleError superclass_cycle_err = 2; ImportNotFoundError import_not_found_err = 3; DeriveOpaqueError derive_opaque_err = 4; - ConstraintCycleError constraint_cycle_err = 5; - MissingRuleError missing_rule_err = 6; - OverlappingRulesError overlapping_rules_err = 7; + MissingRuleError missing_rule_err = 5; + OverlappingRulesError overlapping_rules_err = 6; } }