Skip to content

Commit

Permalink
[ refactor ] Two small refactorings
Browse files Browse the repository at this point in the history
  • Loading branch information
jespercockx committed Mar 13, 2024
1 parent c103bb0 commit 1335c39
Showing 1 changed file with 5 additions and 5 deletions.
10 changes: 5 additions & 5 deletions src/Agda2Hs/Compile/Function.hs
Original file line number Diff line number Diff line change
Expand Up @@ -213,7 +213,7 @@ compileClause' curModule projName x ty c@Clause{..} = do

let rhs = Hs.UnGuardedRhs () hsBody
whereBinds | null whereDecls = Nothing
| otherwise = Just $ Hs.BDecls () (concat whereDecls)
| otherwise = Just $ Hs.BDecls () (concat whereDecls)
match = case (x, ps) of
(Hs.Symbol{}, p : q : ps) -> Hs.InfixMatch () p x (q : ps) rhs whereBinds
_ -> Hs.Match () x ps rhs whereBinds
Expand All @@ -223,11 +223,11 @@ keepClause :: Clause -> C Bool
keepClause c@Clause{..} = case (clauseBody, clauseType) of
(Nothing, _) -> pure False
(_, Nothing) -> pure False
(Just body, Just cty) -> compileDom (domFromArg cty) >>= \case
DODropped -> pure False
DOInstance -> pure False -- not __IMPOSSIBLE__ because of current hacky implementation of `compileInstanceClause`
(Just body, Just cty) -> compileDom (domFromArg cty) <&> \case
DODropped -> False
DOInstance -> False -- not __IMPOSSIBLE__ because of current hacky implementation of `compileInstanceClause`
DOType -> __IMPOSSIBLE__
DOTerm -> pure True
DOTerm -> True


-- TODO(flupe): projection-like definitions are missing the first (variable) patterns
Expand Down

0 comments on commit 1335c39

Please sign in to comment.