Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

instance args #3

Merged
merged 11 commits into from
Dec 3, 2020
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
94 changes: 85 additions & 9 deletions Main.hs
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,7 @@ import Agda.TypeChecking.Rules.Term (isType_)
import Agda.TypeChecking.Reduce
import Agda.TypeChecking.Substitute
import Agda.TypeChecking.Telescope
import Agda.TypeChecking.Records
import Agda.Utils.Lens
import Agda.Utils.Pretty (prettyShow)
import qualified Agda.Utils.Pretty as P
Expand Down Expand Up @@ -243,20 +244,71 @@ tuplePat cons i ps = do

-- Compiling things -------------------------------------------------------

data CodeGen = YesCode | NoCode

data ParsedResult
= NoPragma
| DefaultPragma
| ClassPragma CodeGen

classes :: [String]
classes = ["Show"]

processPragma :: QName -> TCM ParsedResult
processPragma qn = getUniqueCompilerPragma pragmaName qn >>= \case
Nothing -> return NoPragma
Just (CompilerPragma _ s) | s == "class" && s `elem` classes ->
return $ ClassPragma NoCode
Just (CompilerPragma _ s) | s == "class" ->
return $ ClassPragma YesCode
_ -> return DefaultPragma

compile :: Options -> ModuleEnv -> IsMain -> Definition -> TCM CompiledDef
compile _ _ _ def = getUniqueCompilerPragma pragmaName (defName def) >>= \ case
Just _ -> compile' def
Nothing -> return []
compile _ _ _ def = processPragma (defName def) >>= \ case
NoPragma -> return []
DefaultPragma -> compile' def
ClassPragma NoCode -> return []

compile' :: Definition -> TCM CompiledDef
compile' def =
case theDef def of
Axiom -> tag <$> compilePostulate def
Function{} -> tag <$> compileFun def
Datatype{} -> tag <$> compileData def
Record{} -> tag <$> compileRecord def
_ -> return []
where tag code = [(nameBindingSite $ qnameName $ defName def, code)]

compileRecord :: Definition -> TCM [Hs.Decl ()]
compileRecord def = do
let r = hsName $ prettyShow $ qnameName $ defName def
TelV tel _ <- telViewUpTo (recPars (theDef def)) (defType def)
hd <- addContext tel $ do
let params = teleArgs tel :: [Arg Term]
pars <- mapM (showTCM . unArg) $ filter visible params
return $ foldl (\ h p -> Hs.DHApp () h (Hs.UnkindedVar () $ hsName p))
(Hs.DHead () r)
pars
let help :: Int -> [QName] -> Telescope -> TCM [Hs.ClassDecl ()]
help i ns tel = case (ns,splitTelescopeAt i tel) of
(_ ,(_ ,EmptyTel )) -> return []
((n:ns),(tel',ExtendTel ty _)) -> do
ty <- compileRecField tel' n (unDom ty)
tys <- help (i+1) ns tel
return (ty:tys)
telBig <- getRecordFieldTypes (defName def)
let fieldNames = map unDom $ recFields (theDef def)
y <- help (recPars (theDef def)) fieldNames telBig
return [Hs.ClassDecl () Nothing hd [] (Just y)]

compileRecField :: Telescope
-> QName
-> Type
-> TCM (Hs.ClassDecl ())
compileRecField tel n ty = addContext tel $ do
hty <- compileType (unEl ty)
return $ Hs.ClsDecl () (Hs.TypeSig () [hsName $ prettyShow $ qnameName n] hty)

compileData :: Definition -> TCM [Hs.Decl ()]
compileData def = do
let d = hsName $ prettyShow $ qnameName $ defName def
Expand Down Expand Up @@ -385,6 +437,11 @@ compileType t = do
hsA <- compileType (unEl $ unDom a)
hsB <- compileType (unEl b)
return $ Hs.TyFun () hsA hsB
Pi a b | isInstance a -> do
hsA <- compileType (unEl $ unDom a)
hsB <- underAbstraction a b (compileType . unEl)
return $ Hs.TyForall () Nothing (Just (Hs.CxSingle () (Hs.TypeA () hsA))) hsB
-- hsB Pi means Haskell typeclass constraint
Def f es
| Just semantics <- isSpecialType f -> setCurrentRange f $ semantics f es
| Just args <- allApplyElims es -> do
Expand All @@ -395,15 +452,25 @@ compileType t = do
vs <- mapM (compileType . unArg) $ filter visible args
x <- hsName <$> showTCM (Var x [])
return $ tApp (Hs.TyVar () x) vs
Sort s -> return (Hs.TyStar ())
t -> genericDocError =<< text "Bad Haskell type:" <?> prettyTCM t

compileTerm :: Term -> TCM (Hs.Exp ())
compileTerm v =
case unSpine v of
Var x es -> (`app` es) . Hs.Var () . Hs.UnQual () . hsName =<< showTCM (Var x [])
-- v currently we assume all record projections are instance
-- args that need attention
Def f es
| Just semantics <- isSpecialTerm f -> semantics f es
| otherwise -> (`app` es) . Hs.Var () =<< hsQName f
| otherwise -> isProjection f >>= \ case
Just _ -> do
-- v not sure why this fails to strip the name
--f <- hsQName builtins (qualify_ (qnameName f))
-- here's a horrible way to strip the module prefix off the name
let uf = Hs.UnQual () (hsName (show (nameConcrete (qnameName f))))
(`appStrip` es) (Hs.Var () uf)
Nothing -> (`app` es) . Hs.Var () =<< hsQName f
Con h i es
| Just semantics <- isSpecialCon (conName h) -> semantics h i es
Con h i es -> (`app` es) . Hs.Con () =<< hsQName (conName h)
Expand All @@ -423,16 +490,20 @@ compileTerm v =
Hs.InfixApp _ a op b
| a == hsx -> Hs.RightSection () op b -- System-inserted visible lambdas can only come from sections
_ -> hsLambda x body -- so we know x is not free in b.
Lam _ b -> underAbstraction_ b compileTerm
t -> genericDocError =<< text "bad term:" <?> prettyTCM t
where
app :: Hs.Exp () -> Elims -> TCM (Hs.Exp ())
app hd es = eApp <$> pure hd <*> compileArgs es

compileArgs :: Elims -> TCM [Hs.Exp ()]
compileArgs es = do
let Just args = allApplyElims es
mapM (compileTerm . unArg) $ filter visible args
-- `appStrip` is used when we have a record projection and we want to
-- drop the first visible arg (the record)
appStrip :: Hs.Exp () -> Elims -> TCM (Hs.Exp ())
appStrip hd es = do
let Just args = allApplyElims es
args <- mapM (compileTerm . unArg) $ tail $ filter visible args
return $ eApp hd args



compilePats :: NAPs -> TCM [Hs.Pat ()]
compilePats ps = mapM (compilePat . namedArg) $ filter visible ps
Expand All @@ -448,6 +519,11 @@ compilePat (ConP h _ ps) = do
-- TODO: LitP
compilePat p = genericDocError =<< text "bad pattern:" <?> prettyTCM p

compileArgs :: Elims -> TCM [Hs.Exp ()]
compileArgs es = do
let Just args = allApplyElims es
mapM (compileTerm . unArg) $ filter visible args

-- FOREIGN pragmas --------------------------------------------------------

type Code = (Hs.Module Hs.SrcSpanInfo, [Hs.Comment])
Expand Down
28 changes: 28 additions & 0 deletions test/Test.agda
Original file line number Diff line number Diff line change
Expand Up @@ -115,6 +115,34 @@ thm : ∀ xs ys → sum (xs ++ ys) ≡ sum xs + sum ys
thm [] ys = refl
thm (x ∷ xs) ys rewrite thm xs ys | assoc x (sum xs) (sum ys) = refl

-- (custom) Monoid instance

record MonoidX (a : Set) : Set where
field memptyX : a
mappendX : a → a → a

open MonoidX {{...}} public

{-# COMPILE AGDA2HS MonoidX #-}

instance
MonoidNat : MonoidX Nat
memptyX {{MonoidNat}} = 0
mappendX {{MonoidNat}} i j = i + j

-- instances cannot be compiled yet

sumMonX : ∀{a} → {{MonoidX a}} → List a → a
sumMonX [] = memptyX
sumMonX (x ∷ xs) = mappendX x (sumMonX xs)
{-# COMPILE AGDA2HS sumMonX #-}

sumMon : ∀{a} → {{Monoid a}} → List a → a
sumMon [] = mempty
sumMon (x ∷ xs) = x <> sumMon xs
{-# COMPILE AGDA2HS sumMon #-}


-- ** Booleans

ex_bool : Bool
Expand Down
12 changes: 12 additions & 0 deletions test/golden/Test.hs
Original file line number Diff line number Diff line change
Expand Up @@ -62,6 +62,18 @@ plus3 = map (\ n -> n + 3)
doubleLambda :: Integer -> Integer -> Integer
doubleLambda = \ a b -> a + 2 * b

class MonoidX a where
memptyX :: a
mappendX :: a -> a -> a

sumMonX :: MonoidX a => [a] -> a
sumMonX [] = memptyX
sumMonX (x : xs) = mappendX x (sumMonX xs)

sumMon :: Monoid a => [a] -> a
sumMon [] = mempty
sumMon (x : xs) = x <> sumMon xs

ex_bool :: Bool
ex_bool = True

Expand Down