Record construction

[sweirich]

We can't handle this idiom

 decodeI
      | opcode==opcode_LOAD, funct3==funct3_LB  = Lb  {rd=rd, rs1=rs1, oimm12=oimm12}
      | opcode==opcode_LOAD, funct3==funct3_LH  = Lh  {rd=rd, rs1=rs1, oimm12=oimm12}
     ...
       | True = InvalidI

The output is garbage in the RHS. Is it that record construction is still unsupported?

   let decodeI :=
      if andb (opcode GHC.Base.== opcode_LOAD) (funct3 GHC.Base.== funct3_LB) : bool
      then Lb missingValue missingValue missingValue
      else if andb (opcode GHC.Base.== opcode_LOAD) (funct3 GHC.Base.==
                    funct3_LH) : bool
           then Lh missingValue missingValue missingValue 
           ....
            else InvalidI 

[samuelgruetter]

After reading this issue, I found out that we can actually improve the Decode.hs (where this snippet comes from) to make it simpler and nicer, see https://github.com/mit-plv/riscv-semantics/pull/18

So it would certainly be nice to have hs-to-coq support record construction with {...}, but riscv-semantics will also work if it only supports record construction which is just bare function application.

[nomeata]

This works now (was a duplicate of #61 anyways)

[sweirich]

Thanks. We can close the issue (and #61?)