categorize-abst.hs

-- 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)))))))

simplifiers.hs

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
      }