Skip to content

Commit 4ab9b82

Browse files
viktorcsimmaviktorcsimma
authored
Option for user-defined rewrite rules given in a config file (#189)
* First commit for the user-defined rewrite rules feature * Adding an example config file * Prettifying agda2hs.cabal * Adding documentation
1 parent 5905f43 commit 4ab9b82

File tree

8 files changed

+348
-25
lines changed

8 files changed

+348
-25
lines changed

‎agda2hs.cabal‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,7 @@ executable agda2hs
4444
Agda2Hs.Compile.Name,
4545
Agda2Hs.Compile.Postulate,
4646
Agda2Hs.Compile.Record,
47+
Agda2Hs.Compile.Rewrites,
4748
Agda2Hs.Compile.Term,
4849
Agda2Hs.Compile.Type,
4950
Agda2Hs.Compile.TypeDefinition,
@@ -55,6 +56,7 @@ executable agda2hs
5556
AgdaInternals
5657
build-depends: base >= 4.10 && < 4.18,
5758
Agda >= 2.6.3 && < 2.6.4,
59+
bytestring >= 0.11,
5860
containers >= 0.6 && < 0.7,
5961
unordered-containers >= 0.2,
6062
mtl >= 2.2,
@@ -63,7 +65,8 @@ executable agda2hs
6365
haskell-src-exts >= 1.23 && < 1.25,
6466
syb >= 0.7,
6567
text >= 1.2.3.0,
66-
deepseq >= 1.4.1.1
68+
deepseq >= 1.4.1.1,
69+
yaml-light >= 0.1.4
6770
default-language: Haskell2010
6871
default-extensions: LambdaCase,
6972
RecordWildCards,

‎docs/source/features.md‎

Lines changed: 120 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -891,5 +891,125 @@ testA = A.foo
891891
testB = A.foo
892892
```
893893

894+
# Rewrite rules
894895

896+
User-defined rewrite rules for names can be defined through YAML configuration files. These should be provided via the `--rewrite-rules` option.
895897

898+
This feature is particularly useful if you have a project depending on a large library which is not agda2hs-compatible
899+
(the most evident example is probably the Agda standard library).
900+
In this case, you might not want to rewrite the entire library, but you might still have to use it for your proofs.
901+
User-defined rewrite rules can help you translate the library's functions to the ones in the Haskell Prelude,
902+
or even to those written by yourself.
903+
In the latter case, place a Haskell file (e.g. `Base.hs`) next to your `.agda` files that contains your custom definitions
904+
and provide this custom module in the `importing` clauses of the config file.
905+
906+
To an extent, this compromises the mathematically proven correctness of your project.
907+
But if you trust that your (or Prelude's) functions are equivalent to the original ones,
908+
this might not be a problem.
909+
You can also prove the equivalence of the two definitions to be safe.
910+
911+
For example, let's suppose we want to compile the following file:
912+
913+
```agda
914+
open import Data.Nat as ℕ
915+
open import Data.Integer as ℤ
916+
open import Data.Rational.Unnormalised as ℚ
917+
918+
double : ℚᵘ → ℚᵘ
919+
double p = (+ 2 / 1) ℚ.* p
920+
{-# COMPILE AGDA2HS double #-}
921+
922+
-- this will use denominator-1 and suc from BaseExample.hs
923+
twoDenoms : ℚᵘ → ℕ
924+
twoDenoms p = 2 ℕ.* (ℕ.suc (ℚᵘ.denominator-1 p))
925+
{-# COMPILE AGDA2HS twoDenoms #-}
926+
```
927+
928+
By default, the output would be this:
929+
930+
```hs
931+
module Example where
932+
933+
import Data.Rational.Unnormalised.Base (ℚᵘ(denominator-1), (/))
934+
import qualified Data.Rational.Unnormalised.Base as ℚ ((*))
935+
import Numeric.Natural (Natural)
936+
import qualified Prelude as ℕ ((*))
937+
938+
double :: ℚᵘ -> ℚᵘ
939+
double p = (ℚ.*) (pos 2 / 1) p
940+
941+
twoDenoms :: ℚᵘ -> Natural
942+
twoDenoms p = (ℕ.*) 2 (suc (denominator-1 p))
943+
```
944+
945+
Here, agda2hs doesn't know where to find these definitions; so it simply leaves them as they are.
946+
947+
Run this again with the following rewrite rules:
948+
949+
```yaml
950+
- from: Agda.Builtin.Nat.Nat.suc
951+
to: suc
952+
importing: BaseExample
953+
- from: Agda.Builtin.Nat._*_
954+
to: _*_
955+
importing: Prelude
956+
957+
- from: Agda.Builtin.Int.Int.pos
958+
to: toInteger
959+
importing: Prelude
960+
961+
- from: Data.Rational.Unnormalised.Base.ℚᵘ
962+
to: Rational
963+
importing: Data.Ratio
964+
- from: Data.Rational.Unnormalised.Base._*_
965+
to: _*_
966+
importing: Prelude
967+
- from: Data.Rational.Unnormalised.Base._/_
968+
to: _%_
969+
importing: Data.Ratio
970+
- from: Data.Rational.Unnormalised.Base.ℚᵘ.denominator-1
971+
to: denominatorMinus1
972+
importing: BaseExample
973+
```
974+
975+
The names are a bit difficult to find. It helps if you run agda2hs with a verbosity level of 26 and check the logs (specifically the parts beginning with `compiling name`).
976+
977+
The output is now this:
978+
979+
```hs
980+
module Example where
981+
982+
import BaseExample (denominatorMinus1, suc)
983+
import Data.Ratio (Rational, (%))
984+
import Numeric.Natural (Natural)
985+
import Prelude (toInteger, (*))
986+
987+
double :: Rational -> Rational
988+
double p = toInteger 2 % 1 * p
989+
990+
twoDenoms :: Rational -> Natural
991+
twoDenoms p = 2 * suc (denominatorMinus1 p)
992+
```
993+
994+
With a manually written `BaseExample.hs` file like this, GHCi accepts it:
995+
996+
```hs
997+
module BaseExample where
998+
999+
import Numeric.Natural
1000+
import Data.Ratio
1001+
1002+
suc :: Natural -> Natural
1003+
suc = (1 +)
1004+
1005+
denominatorMinus1 :: Rational -> Natural
1006+
denominatorMinus1 = fromIntegral . denominator
1007+
```
1008+
1009+
See also `rewrite-rules-example.yaml` in the root of the repository.
1010+
1011+
**Known issues:**
1012+
- If you import something from Prelude, you have to state this explicitly.
1013+
- Then, it will add an import like import Prelude (...), which shadows all the other functions in Prelude. This is not necessarily a problem; as we will probably not modify the generated Haskell files by hand, and so we won't add any new Prelude functions.
1014+
- But this only works for things you do use, not for those that you only define. For example, if you write an instance of the Num class and define signum but do not use it, it will not get into Prelude's import list, and so GHC will complain.
1015+
- You cannot change to a version with arguments of different modality without getting useless code. So if you rewrite a function to a version which has some of its parameters erased, the parameters remain there; probably because rewriting happens only after compiling the type signature.

‎rewrite-rules-example.yaml‎

Lines changed: 103 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,103 @@
1+
# An example config file for the '--rewrite-rules' option.
2+
# Imagine a library which uses the Agda standard library extensively and let's suppose we would like to translate its operators to the Haskell equivalents. The library includes a Haskell.Prim.Num.Num instance.
3+
4+
# We have to include this so that Num is written to the import list of Prelude.
5+
- from: Haskell.Prim.Num.Num
6+
to: Num
7+
importing: Prelude
8+
# And it doesn't see these by default either, if not included in Prelude's import list.
9+
- from: Haskell.Prim.Num.Num.fromInteger
10+
to: fromInteger
11+
importing: Prelude
12+
- from: Haskell.Prim.Num.Num.signum
13+
to: signum
14+
importing: Prelude
15+
16+
# The rational type.
17+
- from: Data.Rational.Unnormalised.Base.ℚᵘ
18+
to: Rational
19+
importing: Data.Ratio
20+
21+
# Arithmetic operators.
22+
# Note: Prelude has to be specified too!
23+
- from: Agda.Builtin.Nat._+_
24+
to: _+_
25+
importing: Prelude
26+
- from: Agda.Builtin.Nat._*_
27+
to: _*_
28+
importing: Prelude
29+
- from: Agda.Builtin.Nat.-_
30+
to: negate
31+
importing: Prelude
32+
- from: Agda.Builtin.Nat._-_
33+
to: _-_
34+
importing: Prelude
35+
- from: Data.Nat.Base._⊔_
36+
to: max
37+
importing: Prelude
38+
39+
- from: Agda.Builtin.Integer._+_
40+
to: _+_
41+
importing: Prelude
42+
- from: Data.Integer.Base._*_
43+
to: _*_
44+
importing: Prelude
45+
- from: Agda.Builtin.Integer.-_
46+
to: negate
47+
importing: Prelude
48+
- from: Agda.Builtin.Integer._-_
49+
to: _-_
50+
importing: Prelude
51+
52+
- from: Data.Rational.Unnormalised.Base._+_
53+
to: _+_
54+
importing: Prelude
55+
- from: Data.Rational.Unnormalised.Base._*_
56+
to: _*_
57+
importing: Prelude
58+
- from: Data.Rational.Unnormalised.Base.-_
59+
to: negate
60+
importing: Prelude
61+
- from: Data.Rational.Unnormalised.Base._-_
62+
to: _-_
63+
importing: Prelude
64+
- from: Data.Rational.Unnormalised.Base._/_
65+
to: _%_
66+
importing: Data.Ratio
67+
- from: Data.Rational.Unnormalised.Base._⊔_
68+
to: max
69+
importing: Prelude
70+
- from: Data.Rational.Unnormalised.Base._⊓_
71+
to: min
72+
importing: Prelude
73+
- from: Data.Rational.Unnormalised.Base.∣_∣
74+
to: abs
75+
importing: Prelude
76+
- from: Data.Integer.Base.∣_∣
77+
to: intAbs
78+
importing: Base
79+
80+
# Standard library functions related to naturals and integers.
81+
- from: Agda.Builtin.Nat.Nat.suc
82+
to: suc
83+
importing: Base
84+
- from: Agda.Builtin.Int.Int.pos
85+
to: toInteger
86+
importing: Prelude
87+
- from: Data.Integer.DivMod._divℕ_
88+
to: divNat
89+
importing: Base
90+
- from: Data.Nat.DivMod._/_
91+
to: div
92+
importing: Prelude
93+
94+
# Standard library functions related to rationals.
95+
- from: Data.Rational.Unnormalised.Base.ℚᵘ.numerator
96+
to: numerator
97+
importing: Data.Ratio
98+
- from: Data.Rational.Unnormalised.Base.ℚᵘ.denominator
99+
to: denominatorNat
100+
importing: Base #the Base version returns a Natural
101+
- from: Data.Rational.Unnormalised.Base.ℚᵘ.denominator-1
102+
to: denominatorMinus1
103+
importing: Base

‎src/Agda2Hs/Compile.hs‎

Lines changed: 9 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -19,33 +19,36 @@ import Agda2Hs.Compile.Data ( compileData )
1919
import Agda2Hs.Compile.Function ( compileFun, checkTransparentPragma )
2020
import Agda2Hs.Compile.Postulate ( compilePostulate )
2121
import Agda2Hs.Compile.Record ( compileRecord, checkUnboxPragma )
22+
import Agda2Hs.Compile.Rewrites
2223
import Agda2Hs.Compile.Types
2324
import Agda2Hs.Compile.Utils ( tellExtension )
2425
import Agda2Hs.Pragma
2526

26-
initCompileEnv :: TopLevelModuleName -> CompileEnv
27-
initCompileEnv tlm = CompileEnv
27+
-- Needs a list of rewrite rules too.
28+
initCompileEnv :: TopLevelModuleName -> Rewrites -> CompileEnv
29+
initCompileEnv tlm rewrites = CompileEnv
2830
{ currModule = tlm
2931
, minRecordName = Nothing
3032
, locals = []
3133
, copatternsEnabled = False
3234
, checkVar = False
35+
, rewrites = rewrites
3336
}
3437

3538
initCompileState :: CompileState
3639
initCompileState = CompileState { lcaseUsed = 0 }
3740

38-
runC :: TopLevelModuleName -> C a -> TCM (a, CompileOutput)
39-
runC tlm = runWriterT
40-
. flip runReaderT (initCompileEnv tlm)
41+
runC :: TopLevelModuleName -> Rewrites -> C a -> TCM (a, CompileOutput)
42+
runC tlm rewrites = runWriterT
43+
. flip runReaderT (initCompileEnv tlm rewrites)
4144
. flip evalStateT initCompileState
4245

4346
-- Main compile function
4447
------------------------
4548

4649
compile :: Options -> ModuleEnv -> IsMain -> Definition ->
4750
TCM (CompiledDef, CompileOutput)
48-
compile _ tlm _ def = withCurrentModule (qnameModule $ defName def) $ runC tlm $
51+
compile opts tlm _ def = withCurrentModule (qnameModule $ defName def) $ runC tlm (rewriteRules opts) $
4952
compileAndTag <* postCompile
5053
where
5154
tag code = [(nameBindingSite $ qnameName $ defName def, code)]

‎src/Agda2Hs/Compile/Name.hs‎

Lines changed: 30 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,7 @@ import Agda.Utils.Pretty ( prettyShow )
2828
import qualified Agda.Utils.Pretty as P ( Pretty(pretty) )
2929

3030
import Agda2Hs.AgdaUtils
31+
import Agda2Hs.Compile.Rewrites
3132
import Agda2Hs.Compile.Types
3233
import Agda2Hs.Compile.Utils
3334
import Agda2Hs.HsUtils
@@ -42,27 +43,39 @@ isSpecialCon = prettyShow >>> \case
4243
_ -> Nothing
4344
where special c = Just (Hs.Special () $ c ())
4445

45-
isSpecialName :: QName -> Maybe (Hs.Name (), Maybe Import)
46-
isSpecialName = prettyShow >>> \case
47-
"Agda.Builtin.Nat.Nat" -> withImport "Numeric.Natural" "Natural"
48-
"Haskell.Control.Monad.guard" -> withImport "Control.Monad" "guard"
49-
"Agda.Builtin.Int.Int" -> noImport "Integer"
50-
"Agda.Builtin.Word.Word64" -> noImport "Word"
51-
"Agda.Builtin.Float.Float" -> noImport "Double"
52-
"Agda.Builtin.Bool.Bool.false" -> noImport "False"
53-
"Agda.Builtin.Bool.Bool.true" -> noImport "True"
54-
"Haskell.Prim._∘_" -> noImport "_._"
55-
"Haskell.Prim.seq" -> noImport "seq"
56-
"Haskell.Prim._$!_" -> noImport "_$!_"
57-
"Haskell.Prim.Monad.Dont._>>=_" -> noImport "_>>=_"
58-
"Haskell.Prim.Monad.Dont._>>_" -> noImport "_>>_"
59-
_ -> Nothing
46+
-- Gets an extra parameter, with the user-defined rewrite rules in it.
47+
-- If finds it in the user-defined or the built-in rewrite rules, then it returns the new name and a possible import in a Just; otherwise returns Nothing.
48+
isSpecialName :: QName -> Rewrites -> Maybe (Hs.Name (), Maybe Import)
49+
isSpecialName f rules = let pretty = prettyShow f in case lookupRules pretty rules of
50+
result@(Just _) -> result
51+
Nothing -> case pretty of
52+
"Agda.Builtin.Nat.Nat" -> withImport "Numeric.Natural" "Natural"
53+
"Haskell.Control.Monad.guard" -> withImport "Control.Monad" "guard"
54+
"Agda.Builtin.Int.Int" -> noImport "Integer"
55+
"Agda.Builtin.Word.Word64" -> noImport "Word"
56+
"Agda.Builtin.Float.Float" -> noImport "Double"
57+
"Agda.Builtin.Bool.Bool.false" -> noImport "False"
58+
"Agda.Builtin.Bool.Bool.true" -> noImport "True"
59+
"Haskell.Prim._∘_" -> noImport "_._"
60+
"Haskell.Prim.seq" -> noImport "seq"
61+
"Haskell.Prim._$!_" -> noImport "_$!_"
62+
"Haskell.Prim.Monad.Dont._>>=_" -> noImport "_>>=_"
63+
"Haskell.Prim.Monad.Dont._>>_" -> noImport "_>>_"
64+
_ -> Nothing
6065
where
6166
noImport x = Just (hsName x, Nothing)
6267
withImport mod x =
6368
let imp = Import (hsModuleName mod) Unqualified Nothing (hsName x)
6469
in Just (hsName x, Just imp)
6570

71+
lookupRules :: String -> Rewrites -> Maybe (Hs.Name (), Maybe Import)
72+
lookupRules _ [] = Nothing
73+
lookupRules pretty (rule:ls)
74+
| pretty == from rule = case (importing rule) of -- check if there is a new import
75+
Just lib -> withImport lib (to rule)
76+
Nothing -> noImport (to rule)
77+
| otherwise = lookupRules pretty ls
78+
6679
compileName :: Applicative m => Name -> m (Hs.Name ())
6780
compileName n = hsName . show <$> pretty (nameConcrete n)
6881

@@ -79,7 +92,8 @@ compileQName f
7992
Just (r, Record{recNamedCon = False}) -> r -- use record name for unnamed constructors
8093
_ -> f
8194
hf0 <- compileName (qnameName f)
82-
let (hf, mimpBuiltin) = fromMaybe (hf0, Nothing) (isSpecialName f)
95+
rules <- asks rewrites
96+
let (hf, mimpBuiltin) = fromMaybe (hf0, Nothing) (isSpecialName f rules)
8397
parent <- parentName f
8498
par <- traverse (compileName . qnameName) parent
8599
let mod0 = qnameModule $ fromMaybe f parent

0 commit comments

Comments
 (0)