Hernán Rajchert (Oct 28 2022 at 12:29): Hernán Rajchert (Oct 28 2022 at 12:29):How can I force an Eq Haskell instance export? I am able to export the equality functions, but I need to manually create the instances... and for some types the instances are created automatically.
export_code
-- ...
equal_TransactionWarning_inst.equal_TransactionWarning
equal_Payment_inst.equal_Payment
in Haskell (string_classes)
maybe also export "(=) :: type_you_want => _"?
Hernán Rajchert (Oct 28 2022 at 12:55):Screen-Shot-2022-10-28-at-09.54.44.png
Mathias Fleury (Oct 28 2022 at 13:06):datatype 'a test = T 'a
export_code "equal_class.equal :: 'a test ⇒ _" in Haskell
?
Mathias Fleury (Oct 28 2022 at 13:09):(I don't understand Haskell… so this is just a guess)
Hernán Rajchert (Oct 28 2022 at 13:17):That by itselfs exports the following Screen-Shot-2022-10-28-at-10.17.01.png
Hernán Rajchert (Oct 28 2022 at 13:18):Not sure if you meant to use it like this, but this has the same problem than before Screen-Shot-2022-10-28-at-10.17.57.png
Mathias Fleury (Oct 28 2022 at 13:21):I expected that equal_class.equal :: 'a test ⇒ _ would cover the second case…
Mathias Fleury (Oct 28 2022 at 13:21):so exporting the first would be sufficient for your aim
Mathias Fleury (Oct 28 2022 at 13:22):if not, I think that I need a MWE…
Hernán Rajchert (Oct 28 2022 at 13:27):MWE?
Mathias Fleury (Oct 28 2022 at 13:29):minimal working example
Hernán Rajchert (Oct 28 2022 at 13:43):so, this code
theory Example
imports Main
begin
datatype Custom = A | B
datatype 'a test = T 'a
export_code
equal_Custom_inst.equal_Custom
"equal_class.equal :: 'a test ⇒ _" in Haskell
end
is exported as
{-# LANGUAGE EmptyDataDecls, RankNTypes, ScopedTypeVariables #-}
module Example(Test, Custom, equal_test, equal_Custom) where {
import Prelude ((==), (/=), (<), (<=), (>=), (>), (+), (-), (*), (/), (**),
(>>=), (>>), (=<<), (&&), (||), (^), (^^), (.), ($), ($!), (++), (!!), Eq,
error, id, return, not, fst, snd, map, filter, concat, concatMap, reverse,
zip, null, takeWhile, dropWhile, all, any, Integer, negate, abs, divMod,
String, Bool(True, False), Maybe(Nothing, Just));
import qualified Prelude;
newtype Test a = T a;
data Custom = A | B;
equal_test :: forall a. (Eq a) => Test a -> Test a -> Bool;
equal_test (T x) (T ya) = x == ya;
equal_Custom :: Custom -> Custom -> Bool;
equal_Custom A B = False;
equal_Custom B A = False;
equal_Custom B B = True;
equal_Custom A A = True;
}
I can export equal_Custom, but I don't know how to export Eq Custom.
Hernán Rajchert (Oct 28 2022 at 13:44):In the real code, I do get some Eq instances generated, but I don't know what triggers them https://github.com/input-output-hk/marlowe/blob/master/isabelle/generated/SemanticsTypes.hs#L366
Simon Roßkopf (Oct 28 2022 at 15:13):I never tried exporting code to Haskell, but here is a hack that might help. I guess the problem is that your code "never needs" the actual Eq instance, so it is not generated.
If we force a use of Eq by means of the following the instances are generated:
definition eq_wrap :: "'a ⇒ 'a ⇒ bool" where
"eq_wrap x y = (x=y)"
definition eq_export_helper_test :: "'a test ⇒ 'a test ⇒ bool" where
"eq_export_helper_test x y = eq_wrap x y"
definition eq_export_helper_Custom :: "Custom ⇒ Custom ⇒ bool" where
"eq_export_helper_Custom x y = eq_wrap x y"
export_code eq_export_helper_test eq_export_helper_Custom in Haskell
Maybe this can give you an idea on how to proceed.
Hernán Rajchert (Oct 28 2022 at 16:42):This works
definition eq_wrap :: "'a ⇒ 'a ⇒ bool" where
"eq_wrap x y = (x=y)"
definition eq_export_helper_Custom :: "Custom ⇒ Custom ⇒ bool" where
"eq_export_helper_Custom x y = eq_wrap x y"
export_code eq_export_helper_Custom in Haskell
This doesn't.
definition eq_export_helper_Custom :: "Custom ⇒ Custom ⇒ bool" where
"eq_export_helper_Custom x y = (x = y)"
export_code eq_export_helper_Custom in Haskell
I assume because eq_wrap works generically on a type that has Eq... Not the pretiest solution, but it works :D.
Thanks!
Last updated: Apr 26 2024 at 12:28 UTC