Skip to content

Instantly share code, notes, and snippets.

@sellout sellout/categorize-abst.hs
Last active Apr 28, 2020

Embed
What would you like to do?
-- step>
(abst @ (Pair a) ($fHasRepPair @ a))
`cast` (Sub (D:R:RepPair[0] <a>_N) ->_R <Pair a>_R
:: Coercible (Rep (Pair a) -> Pair a) ((a, a) -> Pair a))
-- result>
. @ (->)
$fCategory->
@ (Pair a)
@ (Pair a)
@ (a, a)
(($fYes1ka @ * @ (a, a), $fYes1ka @ * @ (Pair a),
$fYes1ka @ * @ (Pair a))
`cast` (((%,,%)
(Sym (R:Ok->[0]) <(a, a)>_N)
(Sym (R:Ok->[0]) <Pair a>_N)
(Sym (R:Ok->[0]) <Pair a>_N))_R
:: Coercible
(Yes1 (a, a), Yes1 (Pair a), Yes1 (Pair a))
(Ok (->) (a, a), Ok (->) (Pair a), Ok (->) (Pair a))))
(coerceC
@ *
@ *
@ (->)
@ (Pair a)
@ (Pair a)
($fCoerceCatTYPETYPE->ab
@ (Pair a)
@ (Pair a)
(MkCoercible
@ *
@ (Pair a)
@ (Pair a)
@~ (<Pair a>_R :: Coercible (Pair a) (Pair a)))))
(. @ (->)
$fCategory->
@ (Rep (Pair a))
@ (Pair a)
@ (a, a)
(($fYes1ka @ * @ (a, a), $fYes1ka @ * @ (a, a),
$fYes1ka @ * @ (Pair a))
`cast` (((%,,%)
(Sym (R:Ok->[0]) <(a, a)>_N)
(Sym (R:Ok->[0]) (Sym (D:R:RepPair[0] <a>_N)))
(Sym (R:Ok->[0]) <Pair a>_N))_R
:: Coercible
(Yes1 (a, a), Yes1 (a, a), Yes1 (Pair a))
(Ok (->) (a, a), Ok (->) (Rep (Pair a)), Ok (->) (Pair a))))
(abstC
@ *
@ (->)
@ (Pair a)
@ (Rep (Pair a))
(($fRepCatTYPE->ar
@ (Pair a)
@ (a, a)
($fHasRepPair @ a)
((Eq# @ * @ (a, a) @ (a, a) @~ (<(a, a)>_N :: (a, a) ~ (a, a)))
`cast` (((~) <*>_N <(a, a)>_N (Sym (D:R:RepPair[0] <a>_N)))_R
:: Coercible ((a, a) ~ (a, a)) ((a, a) ~ Rep (Pair a)))))
`cast` ((RepCat
<*>_N <(->)>_N <Pair a>_N (Sym (D:R:RepPair[0] <a>_N)))_R
:: Coercible
(RepCat (->) (Pair a) (a, a))
(RepCat (->) (Pair a) (Rep (Pair a))))))
(coerceC
@ *
@ *
@ (->)
@ (a, a)
@ (Rep (Pair a))
(($fCoerceCatTYPETYPE->ab
@ (a, a)
@ (a, a)
(MkCoercible
@ * @ (a, a) @ (a, a) @~ (<(a, a)>_R :: Coercible (a, a) (a, a))))
`cast` ((CoerceCat
<*>_N <*>_N <(->)>_N <(a, a)>_N (Sym (D:R:RepPair[0] <a>_N)))_R
:: Coercible
(CoerceCat (->) (a, a) (a, a))
(CoerceCat (->) (a, a) (Rep (Pair a)))))))
presimplifier :: Plugins.DynFlags -> Plugins.CoreToDo
presimplifier dflags =
Plugins.CoreDoSimplify
1
Plugins.SimplMode
{ Plugins.sm_case_case = False,
Plugins.sm_dflags = dflags,
Plugins.sm_eta_expand = False,
Plugins.sm_inline = True,
Plugins.sm_names = ["pre-categorize"],
Plugins.sm_phase = Plugins.Phase 1,
Plugins.sm_rules = False
}
postsimplifier :: Plugins.DynFlags -> Plugins.CoreToDo
postsimplifier dflags =
Plugins.CoreDoSimplify
1
Plugins.SimplMode
{ Plugins.sm_case_case = False,
Plugins.sm_dflags = dflags,
Plugins.sm_eta_expand = False,
Plugins.sm_inline = False,
Plugins.sm_names = ["categorize"],
Plugins.sm_phase = Plugins.Phase 1,
Plugins.sm_rules = False
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.