Merge branch 'master' of https://github.com/agda/agda2hs into instanc…

…e-args

.github/workflows/ci.yml

@@ -0,0 +1,54 @@
+name: CI
+
+# Trigger the workflow on push or pull request, but only for the master branch
+on:
+  pull_request:
+  push:
+    branches: [master]
+
+jobs:
+  cabal:
+    name: ${{ matrix.os }} / ghc ${{ matrix.ghc }}
+    runs-on: ${{ matrix.os }}
+    strategy:
+      matrix:
+        os: [ubuntu-latest]   # macOS-latest, windows-latest
+        cabal: ["3.4"]
+        ghc:
+          - "8.6.5"
+          - "8.8.4"
+          - "8.10.2"
+
+    steps:
+    - uses: actions/checkout@v2
+      if: github.event.action == 'opened' || github.event.action == 'synchronize' || github.event.ref == 'refs/heads/master'
+
+    # Takes care of ghc and cabal. See https://github.com/actions/setup-haskell.
+    - uses: actions/setup-haskell@v1
+      id: setup-haskell-cabal
+      name: Setup Haskell
+      with:
+        ghc-version: ${{ matrix.ghc }}
+        cabal-version: ${{ matrix.cabal }}
+
+    # Generate a cabal.project.freeze file with all dependencies. We use the
+    # hash of this as the cache key, so when a dependency changes we upload a
+    # new cache.
+    - name: Freeze
+      run: cabal freeze
+
+    # Cache the contents of ~/.cabal/store to avoid rebuilding dependencies for
+    # every build. `restore-keys` makes it use the latest cache even if the
+    # fingerprint doesn't match, so we don't need to start from scratch every
+    # time a dependency changes.
+    - uses: actions/cache@v2
+      name: Cache ~/.cabal/store
+      with:
+        path:         ${{ steps.setup-haskell-cabal.outputs.cabal-store }}
+        key:          ${{ runner.os }}-${{ matrix.ghc }}-${{ hashFiles('cabal.project.freeze') }}
+        restore-keys: ${{ runner.os }}-${{ matrix.ghc }}-
+
+    # The actual job.
+    - name: Test
+      run: make test
+

.gitignore

@@ -1,3 +1,5 @@
+_build
 dist
 dist-newstyle
 test/build
+test/agda2hs

HsUtils.hs

@@ -0,0 +1,122 @@
+module HsUtils where
+
+import Data.Data
+import Data.Generics.Schemes (listify)
+
+import Language.Haskell.Exts.SrcLoc
+import Language.Haskell.Exts.Syntax
+import Language.Haskell.Exts.Build
+import Language.Haskell.Exts.Comments
+import Language.Haskell.Exts.Pretty
+
+import Agda.Syntax.Position
+import Agda.Utils.FileName
+import Agda.Utils.List
+import Agda.Utils.Maybe.Strict (toStrict)
+
+-- Names ------------------------------------------------------------------
+
+isInfix :: String -> Maybe String
+isInfix ('_' : f) = do
+  (op, '_') <- initLast f
+  return op
+isInfix _ = Nothing
+
+hsName :: String -> Name ()
+hsName x
+  | Just op <- isInfix x = Symbol () op
+  | otherwise            = Ident () (map underscore x)
+  where
+    -- Agda uses underscores for operators, which means that you can't have both mapM and mapM_
+    -- without getting ambiguities. To work around this we translate subscript '-' to underscore.
+    underscore '₋' = '_'
+    underscore c   = c
+
+isOp :: QName () -> Bool
+isOp (UnQual _ Symbol{}) = True
+isOp (Special _ Cons{})  = True
+isOp _                   = False
+
+-- Utilities for building Haskell constructs
+
+pp :: Pretty a => a -> String
+pp = prettyPrintWithMode defaultMode{ spacing = False }
+
+-- exactPrint really looks at the line numbers (and we're using the locations from the agda source
+-- to report Haskell parse errors at the right location), so shift everything to start at line 1.
+moveToTop :: Annotated ast => (ast SrcSpanInfo, [Comment]) -> (ast SrcSpanInfo, [Comment])
+moveToTop (x, cs) = (subtractLine l <$> x, [ Comment b (sub l r) str | Comment b r str <- cs ])
+  where l = startLine (ann x) - 1
+        subtractLine :: Int -> SrcSpanInfo -> SrcSpanInfo
+        subtractLine l (SrcSpanInfo s ss) = SrcSpanInfo (sub l s) (map (sub l) ss)
+
+        sub :: Int -> SrcSpan -> SrcSpan
+        sub l (SrcSpan f l0 c0 l1 c1) = SrcSpan f (l0 - l) c0 (l1 - l) c1
+
+pApp :: QName () -> [Pat ()] -> Pat ()
+pApp c@(UnQual () (Symbol () _)) [p, q] = PInfixApp () p c q
+pApp c@(Special () Cons{}) [p, q] = PInfixApp () p c q
+pApp c ps = PApp () c ps
+
+getOp :: Exp () -> Maybe (QOp ())
+getOp (Var _ x) | isOp x = Just $ QVarOp () x
+getOp (Con _ c) | isOp c = Just $ QConOp () c
+getOp _                  = Nothing
+
+eApp :: Exp () -> [Exp ()] -> Exp ()
+eApp f (a : b : as) | Just op <- getOp f = foldl (App ()) (InfixApp () a op b) as
+eApp f [a]          | Just op <- getOp f = LeftSection () a op
+eApp f es = foldl (App ()) f es
+
+tApp :: Type () -> [Type ()] -> Type ()
+tApp (TyCon () (Special () ListCon{})) [a] = TyList () a
+tApp t vs = foldl (TyApp ()) t vs
+
+hsLambda :: String -> Exp () -> Exp ()
+hsLambda x e =
+  case e of
+    Lambda l ps b -> Lambda l (p : ps) b
+    _             -> Lambda () [p] e
+  where
+    p = PVar () $ hsName x
+
+hsUndefined :: Exp ()
+hsUndefined = Var () $ UnQual () (hsName "undefined")
+
+hsError :: String -> Exp ()
+hsError s = Var () (UnQual () $ hsName "error") `eApp` [strE s]
+
+getExplicitImports :: ImportSpec l -> [String]
+getExplicitImports = map pp . \case
+  IVar _ n -> [n]
+  IAbs _ _ n -> [n]
+  IThingAll _ n -> [n]
+  IThingWith _ n ns -> n : map cname ns
+
+cname :: CName l -> Name l
+cname (VarName _ n) = n
+cname (ConName _ n) = n
+
+cloc :: CName l -> l
+cloc (VarName l _) = l
+cloc (ConName l _) = l
+
+srcSpanToRange :: SrcSpan -> Range
+srcSpanToRange (SrcSpan file l1 c1 l2 c2) =
+  intervalToRange (toStrict $ Just $ mkAbsolute file) $ Interval (pos l1 c1) (pos l2 c2)
+  where pos l c = Pn () 0 (fromIntegral l) (fromIntegral c)
+
+srcLocToRange :: SrcLoc -> Range
+srcLocToRange (SrcLoc file l c) = srcSpanToRange (SrcSpan file l c l c)
+
+srcSpanInfoToRange :: SrcSpanInfo -> Range
+srcSpanInfoToRange = srcSpanToRange . srcInfoSpan
+
+allUsedTypes :: Data a => a -> [Type ()]
+allUsedTypes = listify (const True)
+
+usedTypesOf :: Data a => String -> a -> [Type ()]
+usedTypesOf s = listify $ (== s) . pp
+
+usesWord64 :: Data a => a -> Bool
+usesWord64 = not . null . usedTypesOf "Word64"

LICENSE

@@ -1,4 +1,4 @@
-Copyright 2018 Ulf Norell
+Copyright 2020 Ulf Norell
 
 Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal in the Software without restriction, including without limitation the rights to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is furnished to do so, subject to the following conditions: