Allow edit files to specify notations

[samuelgruetter]

The Haskell file

module Test where

test x y =
  let q | x == 2 && y == -1 = x
        | y == 0 = -1
        | otherwise = quot x y
  in q * 2

is translated into

Definition test :=
  fun x y =>
    let q :=
      if (x GHC.Classes.== #2) GHC.Classes.&&
         (y GHC.Classes.== GHC.Num.negate #1) : bool
      then x
      else if y GHC.Classes.== #0 : bool
           then GHC.Num.negate #1
           else GHC.Real.quot x y in
    q GHC.Num.* #2.

while I would like it to be translated into

Require Import Coq.ZArith.BinInt.

Open Scope bool_scope.
Open Scope Z_scope.

Definition test(x y: Z) :=
  let q := if (x =? 2) && (y =? -1) then x
           else if (y =? 0) then -1
           else x / y
  in q * 2.

In particular, I'd like to tell hs-to-coq

• to use Z
• to replace == by =?
• to omit prefixes in front of operators

[samuelgruetter]

To give another example of the same issue: I'd like to specify my own notations for monadic bind, depending on whether the result of the first monad is used in the function passed to bind. For instance, here's a Haskell source file:

{-# LANGUAGE ScopedTypeVariables #-}
module ProgramMonadTest where
import Control.Monad
import Prelude
import Data.Int
import Data.Bits

type Register = Int32

class (Monad p) => RiscvProgram p where
  getRegister :: Register -> p Int32
  setRegister :: Register -> Int32 -> p ()
  loadByte :: Int32 -> p Int8
  loadHalf :: Int32 -> p Int16
  loadWord :: Int32 -> p Int32
  loadDouble :: Int32 -> p Int64
  storeByte :: Int32 -> Int8 -> p ()
  storeHalf :: Int32 -> Int16 -> p ()
  storeWord :: Int32 -> Int32 -> p ()
  storeDouble :: Int32 -> Int64 -> p ()
  getPC :: p Int32
  setPC :: Int32 -> p ()
  step :: p ()
  endCycle :: forall a. p a

test1 :: (RiscvProgram p) => Register -> Int32 -> Int32 -> p Int32
test1 reg addr value = do
  setRegister reg value
  v <- getRegister reg
  storeWord addr v
  loadWord addr

Its test1 function is translated as follows:

Definition test1 {p} `{(RiscvProgram p)}
   : Register -> GHC.Int.Int32 -> GHC.Int.Int32 -> p GHC.Int.Int32 :=
  fun reg addr value =>
    setRegister reg value GHC.Base.>>
    (getRegister reg GHC.Base.>>=
     (fun v => storeWord addr v GHC.Base.>> loadWord addr)).

But I'd like to not depend on anything from GHC.Base, and to use my own monad implementation in Coq, and to use two different notations for bind with ignored/used value, respectively, resulting in something like this:

Definition test1{p}`{RiscvProgram p}: Register -> Int32 -> Int32 -> p Int32 :=
fun reg addr value =>
  setRegister reg value;;
  v <- getRegister reg;
  storeWord addr v;;
  loadWord addr.

[sweirich]

Thanks! I've just added a new test case (tests/Notations.hs) to the repo so that we can try out your simple example above. You are OK with adding a type annotation to this example so that it is not polymorphic, right?

This example currently fails to compile as there are several places in hs-to-coq where we assume dependencies on Base (i.e. treatment of number literals and negation here). We also do not have edits that work with notations.

Stepping back, can you say a bit more about your motivation for avoiding base? Is it that you want to avoid working with typeclasses in the output?

[samuelgruetter]

In this simplified example, I'm OK with adding the type annotation test :: Int -> Int -> Int, but eventually I'd like to have polymorphic operators. See https://github.com/mit-plv/riscv-semantics/blob/master/src/ExecuteM.hs, that's one of the files I'd like to translate.

The motivation for avoiding base is that I consider the GHC base a Haskell-specific technicality, on which the Coq RISCV-spec should not depend. Typeclasses are not a problem (I use them in the Coq code, too), but dependence on very Haskell-specific ones such as Eq would be bad. I tried to split the Haskell RISCV spec into Haskell-specific technical files, which I will translate to Coq by hand, and into "spec" files, which should not contain any Haskell-specific things, and will be translated automatically. While trying to use hs-to-coq, I notice that I'll have to improve this split, but I think if I do that properly, it should work.

Is it correct that hs-to-coq does not use any Coq notations when printing terms? For arithmetic expressions, this shouldn't be a problem, but what about monadic style? How hard would it be to get output like this? https://github.com/samuelgruetter/riscv-coq/blob/master/src/ExecuteI.v (definitely not the top priority, but having to replace that file with one containing tons of nested Binds makes me a bit sad :wink:)

[nomeata]

Is it correct that hs-to-coq does not use any Coq notations when printing terms?

hs-to-coq can be told to use binary operators, i.e.

rename value GHC.Classes.&&    = &&

works just fine (it is your responsibility to ensure that that notation is in scope, i.e. add Import Coq.Bool.Bool to the preamble.v)

Monadic style would require more work, since it is not just binary operators. Is there a globally accepted Monad notation across the Coq universe that we could desugar to?

BTW, do you know about coqc -beautify?

Pretty-print each command to file.beautified when compiling file.v, in order to get old-fashioned syntax/definitions/notations.

So in theory, you should take the notation-free output of hs-to-coq and get Coq to pretty-print (including all notations) all the code. coq_makefile-produced Makefiles have a make beatuify target, AFAIR.

[samuelgruetter]

Nice :+1: Just tried out coqc -beautify on a small example, and I think this will solve the monad pretty printing. So I'm quite optimistic regarding "code prettiness" now (but probably that's just because I haven't actually tried it on all the code yet :wink:)

[nomeata]

Yeah, last time I tried beautify it was not bug free… but I think it was mostly stumbling over proofs, not terms, your mileage may vary.