deriving Ord for "Width" type in CmmType.hs

[lastland]

Issue by sweirich Monday Oct 16, 2017 at 13:03 GMT Originally opened as https://github.com/antalsz/hs-to-coq/issues/29

---

data Width   = W8 | W16 | W32 | W64
             | W80      -- Extended double-precision float,
                        -- used in x86 native codegen only.
                        -- (we use Ord, so it'd better be in this order)
             | W128
             | W256
             | W512
             deriving (Eq, Ord, Show)

The output of the derived Ord instance of this datatype looks weird. I'm not sure what is going on. Maybe something to do with Enum?

[lastland]

Comment by antalsz Monday Oct 16, 2017 at 15:39 GMT

---

Could you include it in the issue?

[lastland]

Comment by sweirich Monday Oct 16, 2017 at 15:50 GMT

---

Local Definition instance_GHC_Base_Ord_Width_op_zlze__
    : Width -> Width -> bool :=
  fun arg_142__ arg_143__ =>
    match arg_142__ , arg_143__ with
      | a , b => let scrut_144__ :=
                   (Deriving.op_zdcon2tagzu7BaO2wD9tNnI4ofEJBxUXs__ a) in
                 match scrut_144__ with
                   | a# => let scrut_145__ :=
                             (Deriving.op_zdcon2tagzu7BaO2wD9tNnI4ofEJBxUXs__ b) in
                           match scrut_145__ with
                             | b# => (GHC.Prim.op_tagToEnumzh__ (GHC.Prim.op_zlzezh__ op_azh__ op_bzh__))
                           end
                 end
    end.

[lastland]

Comment by antalsz Monday Oct 16, 2017 at 16:09 GMT

---

So, here's the Haskell version (generated from GHCi):

(GHC.Classes.<=) a_a4res b_a4ret
  = case (Ghci4.$con2tag_1pkeUNKOpaw5YfScuo8o77 a_a4res) of {
      a#_a4reu
        -> case (Ghci4.$con2tag_1pkeUNKOpaw5YfScuo8o77 b_a4ret) of {
             b#_a4rev
               -> (GHC.Prim.tagToEnum# (a#_a4reu GHC.Prim.<=# b#_a4rev)) } }

There's a lot of funky stuff going on there. Looks like the issues are:

1. It compares things by (1) extracting the raw Int# from the tag and then (2) casting a raw 0# or 1# to a Bool by reinterpreting it. These are both highly unsupported operations for hs-to-coq. And frankly, I'm surprised it does this in terms of the generated $con2tag_… function instead of GHC.Prim.dataToTag# :: a -> Int# (or the marginally-higher-level GHC.Base.getTag :: a -> Int#), which would be even harder to deal with.

2. Just… really weird variable names. We don't handle names like a# (or a#_a4reu) or $con2tag_…. The former is just for unboxed things, the latter is just for generated code.

---

For reference, the con2tag_… function:

Ghci4.$con2tag_1pkeUNKOpaw5YfScuo8o77 ::
  Ghci4.Width -> GHC.Prim.Int#
Ghci4.$con2tag_1pkeUNKOpaw5YfScuo8o77 Ghci4.W8 = 0#
Ghci4.$con2tag_1pkeUNKOpaw5YfScuo8o77 Ghci4.W16 = 1#
Ghci4.$con2tag_1pkeUNKOpaw5YfScuo8o77 Ghci4.W32 = 2#
Ghci4.$con2tag_1pkeUNKOpaw5YfScuo8o77 Ghci4.W64 = 3#
Ghci4.$con2tag_1pkeUNKOpaw5YfScuo8o77 Ghci4.W80 = 4#
Ghci4.$con2tag_1pkeUNKOpaw5YfScuo8o77 Ghci4.W128 = 5#
Ghci4.$con2tag_1pkeUNKOpaw5YfScuo8o77 Ghci4.W256 = 6#
Ghci4.$con2tag_1pkeUNKOpaw5YfScuo8o77 Ghci4.W512 = 7#

[lastland]

Comment by antalsz Wednesday Oct 18, 2017 at 20:11 GMT

---

cc @nomeata