Skip to content

Commit

Permalink
[ refactor ] Move con clause creation out
Browse files Browse the repository at this point in the history
  • Loading branch information
buzden committed Sep 19, 2023
1 parent a445767 commit 25dacbd
Showing 1 changed file with 3 additions and 3 deletions.
6 changes: 3 additions & 3 deletions src/Test/DepTyCheck/Gen/Coverage.idr
Original file line number Diff line number Diff line change
Expand Up @@ -112,14 +112,14 @@ withCoverage gen = do
tyLabelStr <- quote "\{show tyName}[?]"
let matchCon = \con => reAppAny (var con.name) $ con.args <&> flip appArg implicitTrue
let matchDPair = \expr => foldr (\_, r => var "Builtin.DPair.MkDPair" .$ implicitTrue .$ r) expr dpairLefts
labeller <- check `(\val => Test.DepTyCheck.Gen.label (fromString ~tyLabelStr) ~(
iCase (var "val") implicitTrue $ tyInfo.cons <&> \con =>
patClause
let conClause = \con => patClause
(as `{x} $ matchDPair $ matchCon con)
(var "Test.DepTyCheck.Gen.label"
.$ (var "fromString" .$ primVal (Str "\{show con.name} (user-defined)"))
.$ `(pure x)
)
labeller <- check `(\val => Test.DepTyCheck.Gen.label (fromString ~tyLabelStr) ~(
iCase (var "val") implicitTrue $ tyInfo.cons <&> conClause
))
pure $ gen >>= labeller

Expand Down

0 comments on commit 25dacbd

Please sign in to comment.