Skip to content

Commit

Permalink
documentation & renamings
Browse files Browse the repository at this point in the history
  • Loading branch information
flupe authored and omelkonian committed Feb 16, 2024
1 parent 7d1d0be commit 2cb06f6
Show file tree
Hide file tree
Showing 5 changed files with 144 additions and 90 deletions.
11 changes: 11 additions & 0 deletions src/Agda2Hs/AgdaUtils.hs
Original file line number Diff line number Diff line change
Expand Up @@ -125,3 +125,14 @@ maybeUnfoldCopy f es onTerm onDef =
inRecordMod :: MonadTCM m => QName -> m Bool
inRecordMod = liftTCM . fmap isJust . isDatatypeModule . qnameModule


-- | Check whether a pattern is forced.
isForcedPat :: DeBruijnPattern -> Bool
isForcedPat = \case
VarP{} -> False
DotP{} -> True
ConP c cpi ps -> conPLazy cpi
LitP{} -> False
ProjP{} -> False
IApplyP{} -> False
DefP{} -> False
85 changes: 48 additions & 37 deletions src/Agda2Hs/Compile/Function.hs
Original file line number Diff line number Diff line change
Expand Up @@ -43,16 +43,18 @@ import Agda2Hs.Compile.Utils
import Agda2Hs.HsUtils
import Agda.TypeChecking.Datatypes (isDataOrRecord)

isSpecialPat :: QName -> Maybe (ConHead -> ConPatternInfo -> [NamedArg DeBruijnPattern] -> C (Hs.Pat ()))
isSpecialPat qn = case prettyShow qn of

-- | Pattern compilation rules for specific constructors.
isSpecialCon :: QName -> Maybe (NAPs -> C (Hs.Pat ()))
isSpecialCon qn = case prettyShow qn of
"Haskell.Prim.Tuple._,_" -> Just tuplePat
"Haskell.Prim.Tuple._×_×_._,_,_" -> Just tuplePat
"Haskell.Extra.Erase.Erased" -> Just tuplePat
"Agda.Builtin.Int.Int.pos" -> Just posIntPat
"Agda.Builtin.Int.Int.negsuc" -> Just negSucIntPat
s | s `elem` badConstructors -> Just $ \ _ _ _ -> genericDocError =<<
"Agda.Builtin.Int.Int.pos" -> Just posIntPat
"Agda.Builtin.Int.Int.negsuc" -> Just negSucIntPat
s | s `elem` badConstructors -> Just $ \ _ -> genericDocError =<<
"constructor `" <> prettyTCM qn <> "` not supported in patterns"
_ -> Nothing
_ -> Nothing
where
badConstructors =
[ "Agda.Builtin.Nat.Nat.zero"
Expand All @@ -65,11 +67,30 @@ isUnboxCopattern :: DeBruijnPattern -> C Bool
isUnboxCopattern (ProjP _ q) = isJust <$> isUnboxProjection q
isUnboxCopattern _ = return False

tuplePat :: ConHead -> ConPatternInfo -> [NamedArg DeBruijnPattern] -> C (Hs.Pat ())
tuplePat cons i ps =

-- | Translate list of patterns into a Haskell n-uple pattern.
tuplePat :: NAPs -> C (Hs.Pat ())
tuplePat ps =
mapM (compilePat . namedArg) (filter keepArg ps)
<&> Hs.PTuple () Hs.Boxed


-- | Translate Int.pos pattern.
posIntPat :: NAPs -> C (Hs.Pat ())
posIntPat [p] = do
n <- compileLitNatPat (namedArg p)
return $ Hs.PLit () (Hs.Signless ()) (Hs.Int () n (show n))
posIntPat _ = __IMPOSSIBLE__


-- | Translate Int.negsuc pattern.
negSucIntPat :: NAPs -> C (Hs.Pat ())
negSucIntPat [p] = do
n <- (1+) <$> compileLitNatPat (namedArg p)
return $ Hs.PLit () (Hs.Negative ()) (Hs.Int () n (show (negate n)))
negSucIntPat _ = __IMPOSSIBLE__


-- Agda2Hs does not support natural number patterns directly (since
-- they don't exist in Haskell), however they occur as part of
-- patterns of type Integer, so we need to compile literal natural
Expand All @@ -82,17 +103,6 @@ compileLitNatPat = \case
, [p] <- ps -> (1+) <$> compileLitNatPat (namedArg p)
p -> genericDocError =<< "not a literal natural number pattern:" <?> prettyTCM p

posIntPat :: ConHead -> ConPatternInfo -> [NamedArg DeBruijnPattern] -> C (Hs.Pat ())
posIntPat c i [p] = do
n <- compileLitNatPat (namedArg p)
return $ Hs.PLit () (Hs.Signless ()) (Hs.Int () n (show n))
posIntPat _ _ _ = __IMPOSSIBLE__

negSucIntPat :: ConHead -> ConPatternInfo -> [NamedArg DeBruijnPattern] -> C (Hs.Pat ())
negSucIntPat c i [p] = do
n <- (1+) <$> compileLitNatPat (namedArg p)
return $ Hs.PLit () (Hs.Negative ()) (Hs.Int () n (show (negate n)))
negSucIntPat _ _ _ = __IMPOSSIBLE__

compileFun, compileFun'
:: Bool -- ^ Whether the type signature shuuld also be generated
Expand Down Expand Up @@ -177,45 +187,38 @@ compileClause' curModule x c@Clause{..} = do
_ -> Hs.Match () x ps rhs whereBinds
return $ Just match

noAsPatterns :: DeBruijnPattern -> C ()
noAsPatterns = \case
checkNoAsPatterns :: DeBruijnPattern -> C ()
checkNoAsPatterns = \case
VarP i _ -> checkPatternInfo i
DotP i _ -> checkPatternInfo i
ConP _ cpi ps -> do
checkPatternInfo $ conPInfo cpi
forM_ ps $ noAsPatterns . namedArg
forM_ ps $ checkNoAsPatterns . namedArg
LitP i _ -> checkPatternInfo i
ProjP{} -> return ()
IApplyP i _ _ _ -> checkPatternInfo i
DefP i _ ps -> do
checkPatternInfo i
forM_ ps $ noAsPatterns . namedArg
forM_ ps $ checkNoAsPatterns . namedArg
where
checkPatternInfo i = unless (null $ patAsNames i) $
genericDocError =<< "not supported by agda2hs: as patterns"


compilePats :: NAPs -> C [Hs.Pat ()]
compilePats ps = mapM (compilePat . namedArg) =<< filterM keepPat ps
where
keepPat :: NamedArg DeBruijnPattern -> C Bool
keepPat p = do
keep <- return (keepArg p) `and2M` (not <$> isUnboxCopattern (namedArg p))
when keep $ noAsPatterns $ namedArg p

when keep $ checkNoAsPatterns $ namedArg p

-- We do not allow forced (dot) patterns for non-erased arguments (see issue #142).
when (usableModality p && isForcedPat (namedArg p)) $
genericDocError =<< "not supported by agda2hs: forced (dot) patterns in non-erased positions"
return keep

isForcedPat :: DeBruijnPattern -> Bool
isForcedPat = \case
VarP{} -> False
DotP{} -> True
ConP c cpi ps -> conPLazy cpi
LitP{} -> False
ProjP{} -> False
IApplyP{} -> False
DefP{} -> False


compilePat :: DeBruijnPattern -> C (Hs.Pat ())
compilePat p@(VarP o x)
Expand All @@ -225,7 +228,7 @@ compilePat p@(VarP o x)
checkValidVarName n
return $ Hs.PVar () n
compilePat (ConP h i ps)
| Just semantics <- isSpecialPat (conName h) = setCurrentRange h $ semantics h i ps
| Just semantics <- isSpecialCon (conName h) = setCurrentRange h $ semantics ps
compilePat (ConP h _ ps) = isUnboxConstructor (conName h) >>= \case
Just s -> compileErasedConP ps >>= addPatBang s
Nothing -> do
Expand All @@ -251,10 +254,12 @@ compileLitPat = \case
LitChar c -> return $ Hs.charP c
l -> genericDocError =<< "bad literal pattern:" <?> prettyTCM l


-- Local (where) declarations ---------------------------------------------

-- | Before checking a function, grab all of its local declarations.

-- TODO: simplify this when Agda exposes where-provenance in 'Internal' syntax
-- | Run a computation with all the local declarations in the state.
withFunctionLocals :: QName -> C a -> C a
withFunctionLocals q k = do
ls <- takeWhile (isAnonymousModuleName . qnameModule)
Expand All @@ -265,10 +270,12 @@ withFunctionLocals q k = do
reportSDoc "agda2hs.compile.locals" 17 $ "Function locals: "<+> prettyTCM ls
withLocals ls k

-- | Retain only those local declarations that belong to current clause's module.

-- | Filter local declarations that belong to the given module.
zoomLocals :: ModuleName -> LocalDecls -> LocalDecls
zoomLocals mname = filter ((mname `isLeParentModuleOf`) . qnameModule)


-- | Before checking a clause, grab all of its local declarations.
-- TODO: simplify this when Agda exposes where-provenance in 'Internal' syntax
withClauseLocals :: ModuleName -> Clause -> C a -> C a
Expand All @@ -289,6 +296,8 @@ withClauseLocals curModule c@Clause{..} k = do
reportSDoc "agda2hs.compile.locals" 18 $ "Clause locals: "<+> prettyTCM ls'
withLocals ls' k


-- | Ensure a definition can be defined as transparent.
checkTransparentPragma :: Definition -> C ()
checkTransparentPragma def = compileFun False def >>= \case
[Hs.FunBind _ cls] ->
Expand All @@ -310,6 +319,8 @@ checkTransparentPragma def = compileFun False def >>= \case
"Cannot make function" <+> prettyTCM (defName def) <+> "transparent." <+>
"A transparent function must have exactly one non-erased argument and return it unchanged."


-- | Ensure a definition can be defined as inline.
checkInlinePragma :: Definition -> C ()
checkInlinePragma def@Defn{defName = f} = do
let Function{funClauses = cs} = theDef def
Expand Down
106 changes: 53 additions & 53 deletions src/Agda2Hs/Compile/Type.hs
Original file line number Diff line number Diff line change
Expand Up @@ -40,62 +40,47 @@ import Agda2Hs.Compile.Utils
import Agda2Hs.AgdaUtils
import Agda2Hs.HsUtils

isSpecialType :: QName -> Maybe (QName -> Elims -> C (Hs.Type ()))

-- | Type definitions from the prelude that get special translation rules.
isSpecialType :: QName -> Maybe (Elims -> C (Hs.Type ()))
isSpecialType x = case prettyShow x of
"Haskell.Prim.Tuple._×_" -> Just tupleType
"Haskell.Prim.Tuple._×_×_" -> Just tupleType
"Haskell.Extra.Erase.Erase" -> Just erasedType
"Haskell.Extra.Erase.Erase" -> Just unitType
"Haskell.Extra.Delay.Delay" -> Just delayType
_ -> Nothing

tupleType :: QName -> Elims -> C (Hs.Type ())
tupleType q es = do

-- | Compile all the elims into a n-uple.
tupleType :: Elims -> C (Hs.Type ())
tupleType es = do
let Just as = allApplyElims es
ts <- mapM (compileType . unArg) as
return $ Hs.TyTuple () Hs.Boxed ts

erasedType :: QName -> Elims -> C (Hs.Type ())
erasedType _ _ = return $ Hs.TyTuple () Hs.Boxed []

delayType :: QName -> Elims -> C (Hs.Type ())
delayType _ (Apply a : _) = compileType (unArg a)
delayType _ (_ : _) = __IMPOSSIBLE__
delayType _ [] = genericDocError =<< text "Cannot compile unapplied Delay type"


-- | Add a class constraint to a Haskell type.
constrainType
:: Hs.Asst () -- ^ The class assertion.
-> Hs.Type () -- ^ The type to constrain.
-> Hs.Type ()
constrainType c = \case
Hs.TyForall _ as (Just (Hs.CxTuple _ cs)) t -> Hs.TyForall () as (Just (Hs.CxTuple () (c:cs))) t
Hs.TyForall _ as (Just (Hs.CxSingle _ c')) t -> Hs.TyForall () as (Just (Hs.CxTuple () [c,c'])) t
Hs.TyForall _ as Nothing t -> Hs.TyForall () as (Just (Hs.CxSingle () c )) t
t -> Hs.TyForall () Nothing (Just (Hs.CxSingle () c )) t

-- | Add explicit quantification over a variable to a Haskell type.
qualifyType
:: String -- ^ Name of the variable.
-> Hs.Type () -- ^ Type to quantify.
-> Hs.Type ()
qualifyType s = \case
Hs.TyForall _ (Just as) cs t -> Hs.TyForall () (Just (a:as)) cs t
Hs.TyForall _ Nothing cs t -> Hs.TyForall () (Just [a] ) cs t
t -> Hs.TyForall () (Just [a] ) Nothing t
where
a = Hs.UnkindedVar () $ Hs.Ident () s


-- | Compile a top-level type, such that:
--
-- * erased parameters of the current module are dropped.
-- * usable hidden type parameters of the current module are explicitely quantified.
-- * usable instance parameters are added as type constraints.
-- * usable explicit parameters are forbidden (for now).
--
-- The continuation is called in an extended context with these type
-- arguments bound.

-- | Ignore arguments and return the unit type.
unitType :: Elims -> C (Hs.Type ())
unitType _ = return $ Hs.TyTuple () Hs.Boxed []


-- | Compile fully applied Delay type as its only type argument.
delayType :: Elims -> C (Hs.Type ())
delayType (Apply a : _) = compileType (unArg a)
delayType (_ : _) = __IMPOSSIBLE__
delayType [] = genericDocError =<< text "Cannot compile unapplied Delay type"


{- | Compile a top-level type, such that:
* erased parameters of the current module are dropped.
* usable hidden type parameters of the current module are explicitely quantified.
* usable instance parameters are added as type constraints.
* usable explicit parameters are forbidden (for now).
The continuation is called in an extended context with these type
arguments bound.
-}
compileTopLevelType
:: Bool
-- ^ Whether the generated Haskell type will end up in
Expand Down Expand Up @@ -132,16 +117,21 @@ compileTopLevelType keepType t cont = do
underAbstraction a atel $ \tel ->
go onTop tel (cont . qualifier)

compileType' :: Term -> C (Strictness, Hs.Type ())
compileType' t = do

-- | Compile an Agda term into a Haskell type, along with its strictness.
compileTypeStrictness :: Term -> C (Strictness, Hs.Type ())
compileTypeStrictness t = do
s <- case t of
Def f es -> fromMaybe Lazy <$> isUnboxRecord f
_ -> return Lazy
(s,) <$> compileType t
ty <- compileType t
pure (s, ty)


-- | Compile an Agda term into a Haskell type.
compileType :: Term -> C (Hs.Type ())
compileType t = do

reportSDoc "agda2hs.compile.type" 12 $ text "Compiling type" <+> prettyTCM t
reportSDoc "agda2hs.compile.type" 22 $ text "Compiling type" <+> pretty t

Expand All @@ -154,13 +144,14 @@ compileType t = do
hsB <- underAbstraction a b (compileType . unEl)
return $ constrainType hsA hsB
DomDropped -> underAbstr a b (compileType . unEl)

Def f es -> maybeUnfoldCopy f es compileType $ \f es -> do
def <- getConstInfo f
if | not (usableModality def) ->
genericDocError
=<< text "Cannot use erased definition" <+> prettyTCM f
<+> text "in Haskell type"
| Just semantics <- isSpecialType f -> setCurrentRange f $ semantics f es
| Just semantics <- isSpecialType f -> setCurrentRange f $ semantics es
| Just args <- allApplyElims es ->
ifJustM (isUnboxRecord f) (\_ -> compileUnboxType f args) $
ifM (isTransparentFunction f) (compileTransparentType args) $
Expand All @@ -169,31 +160,39 @@ compileType t = do
f <- compileQName f
return $ tApp (Hs.TyCon () f) vs
| otherwise -> fail

Var x es | Just args <- allApplyElims es -> do
vs <- compileTypeArgs args
x <- hsName <$> compileVar x
return $ tApp (Hs.TyVar () x) vs

Sort s -> return (Hs.TyStar ())

Lam argInfo restAbs
| not (keepArg argInfo) -> underAbstraction_ restAbs compileType

_ -> fail
where fail = genericDocError =<< text "Bad Haskell type:" <?> prettyTCM t


compileTypeArgs :: Args -> C [Hs.Type ()]
compileTypeArgs args = mapM (compileType . unArg) $ filter keepArg args


compileUnboxType :: QName -> Args -> C (Hs.Type ())
compileUnboxType r pars = do
def <- theDef <$> getConstInfo r
let tel = telToList $ recTel def `apply` pars
case find keepArg tel of
Just t -> compileType $ unEl $ snd (unDom t)
Nothing -> __IMPOSSIBLE__
Just t -> compileType $ unEl $ snd (unDom t)


compileTransparentType :: Args -> C (Hs.Type ())
compileTransparentType args = compileTypeArgs args >>= \case
[] -> __IMPOSSIBLE__
(v:vs) -> return $ v `tApp` vs
[] -> __IMPOSSIBLE__


compileInlineType :: QName -> Elims -> C (Hs.Type ())
compileInlineType f args = do
Expand All @@ -215,13 +214,14 @@ compileDom :: ArgName -> Dom Type -> C CompiledDom
compileDom x a
| usableModality a = case getHiding a of
Instance{} -> DomConstraint . Hs.TypeA () <$> compileType (unEl $ unDom a)
NotHidden -> uncurry DomType <$> compileType' (unEl $ unDom a)
NotHidden -> uncurry DomType <$> compileTypeStrictness (unEl $ unDom a)
Hidden ->
ifM (canErase $ unDom a)
(return DomDropped)
(genericDocError =<< do text "Implicit type argument not supported: " <+> prettyTCM x)
| otherwise = return DomDropped


compileTeleBinds :: Telescope -> C [Hs.TyVarBind ()]
compileTeleBinds tel =
forM
Expand Down
Loading

0 comments on commit 2cb06f6

Please sign in to comment.