{-# LANGUAGE DataKinds                 #-}
{-# LANGUAGE EmptyCase                 #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE KindSignatures            #-}
{-# LANGUAGE MultiParamTypeClasses     #-}
{-# LANGUAGE OverloadedStrings         #-}
{-# LANGUAGE PolyKinds                 #-}
{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE TypeFamilies              #-}
{-# LANGUAGE TypeOperators             #-}

{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
----------------------------------------------------------------
--                                                    2017.02.01
-- |
-- Module      :  Language.Hakaru.Syntax.ANF
-- Copyright   :  Copyright (c) 2016 the Hakaru team
-- License     :  BSD3
-- Maintainer  :
-- Stability   :  experimental
-- Portability :  GHC-only
--
--
----------------------------------------------------------------
module Language.Hakaru.Syntax.ANF (normalize, isValue) where

import           Data.Maybe
import           Control.Monad.Cont              (Cont, runCont, cont)

import           Language.Hakaru.Syntax.ABT
import           Language.Hakaru.Syntax.AST
import           Language.Hakaru.Syntax.IClasses
import           Language.Hakaru.Types.DataKind

import           Language.Hakaru.Syntax.Prelude

-- The renaming environment which maps variables in the original term to their
-- counterparts in the new term. This is needed since the mechanism which
-- ensures hygiene for the AST only factors in binders, but not free variables
-- in the expression being constructed. When we construct a new binding form, a
-- new variable is introduced and the variable in the old expression must be
-- mapped to the new one.

type Env = Assocs (Variable :: Hakaru -> *)

updateEnv :: forall (a :: Hakaru) . Variable a -> Variable a -> Env -> Env
updateEnv :: Variable a -> Variable a -> Env -> Env
updateEnv Variable a
vin Variable a
vout = Assoc Variable -> Env -> Env
forall k (ast :: k -> *). Assoc ast -> Assocs ast -> Assocs ast
insertAssoc (Variable a -> Variable a -> Assoc Variable
forall k (ast :: k -> *) (a :: k). Variable a -> ast a -> Assoc ast
Assoc Variable a
vin Variable a
vout)

-- | The context in which A-normalization occurs. Represented as a continuation,
-- the context expects an expression of a particular type (usually a variable)
-- and produces a new expression as a result.
type Context abt a b = abt '[] a -> abt '[] b

-- | Extract a variable from an abt. This function is partial
getVar :: (ABT Term abt) => abt xs a -> Variable a
getVar :: abt xs a -> Variable a
getVar abt xs a
abt = case abt xs a -> View (Term abt) xs a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt xs a
abt of
               Var Variable a
v -> Variable a
v
               View (Term abt) xs a
_     -> [Char] -> Variable a
forall a. HasCallStack => [Char] -> a
error [Char]
"getVar: not given a variable"

-- | Useful function for generating fresh variables from an existing variable by
-- wrapping @binder@.
freshVar
  :: (ABT Term abt)
  => Variable a
  -> (Variable a -> abt xs b)
  -> abt (a ': xs) b
freshVar :: Variable a -> (Variable a -> abt xs b) -> abt (a : xs) b
freshVar Variable a
v Variable a -> abt xs b
f = Text -> Sing a -> (abt '[] a -> abt xs b) -> abt (a : xs) b
forall a1 (syn :: ([a1] -> a1 -> *) -> a1 -> *)
       (abt :: [a1] -> a1 -> *) (a2 :: a1) (xs :: [a1]) (b :: a1).
ABT syn abt =>
Text -> Sing a2 -> (abt '[] a2 -> abt xs b) -> abt (a2 : xs) b
binder (Variable a -> Text
forall k (a :: k). Variable a -> Text
varHint Variable a
v) (Variable a -> Sing a
forall k (a :: k). Variable a -> Sing a
varType Variable a
v) (Variable a -> abt xs b
f (Variable a -> abt xs b)
-> (abt '[] a -> Variable a) -> abt '[] a -> abt xs b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt '[] a -> Variable a
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
ABT Term abt =>
abt xs a -> Variable a
getVar)

remapVar
  :: (ABT Term abt)
  => Variable a
  -> Env
  -> (Env -> abt xs b)
  -> abt (a ': xs) b
remapVar :: Variable a -> Env -> (Env -> abt xs b) -> abt (a : xs) b
remapVar Variable a
v Env
env Env -> abt xs b
f = Variable a -> (Variable a -> abt xs b) -> abt (a : xs) b
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (xs :: [Hakaru]) (b :: Hakaru).
ABT Term abt =>
Variable a -> (Variable a -> abt xs b) -> abt (a : xs) b
freshVar Variable a
v ((Variable a -> abt xs b) -> abt (a : xs) b)
-> (Variable a -> abt xs b) -> abt (a : xs) b
forall a b. (a -> b) -> a -> b
$ \Variable a
v' -> Env -> abt xs b
f (Variable a -> Variable a -> Env -> Env
forall (a :: Hakaru). Variable a -> Variable a -> Env -> Env
updateEnv Variable a
v Variable a
v' Env
env)

-- | Entry point for the normalization process. Initializes normalize' with the
-- empty context.
normalize
  :: (ABT Term abt)
  => abt '[] a
  -> abt '[] a
normalize :: abt '[] a -> abt '[] a
normalize abt '[] a
abt = abt '[] a -> Env -> (abt '[] a -> abt '[] a) -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] a -> Env -> Context abt a b -> abt '[] b
normalize' abt '[] a
abt Env
forall k (abt :: k -> *). Assocs abt
emptyAssocs abt '[] a -> abt '[] a
forall a. a -> a
id

normalize'
  :: (ABT Term abt)
  => abt '[] a
  -> Env
  -> Context abt a b
  -> abt '[] b
normalize' :: abt '[] a -> Env -> Context abt a b -> abt '[] b
normalize' = View (Term abt) '[] a -> Env -> Context abt a b -> abt '[] b
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru) (b :: Hakaru).
ABT Term abt =>
View (Term abt) xs a -> Env -> (abt xs a -> abt '[] b) -> abt '[] b
normalizeTail (View (Term abt) '[] a -> Env -> Context abt a b -> abt '[] b)
-> (abt '[] a -> View (Term abt) '[] a)
-> abt '[] a
-> Env
-> Context abt a b
-> abt '[] b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt '[] a -> View (Term abt) '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT

normalizeTail, normalizeSave
  :: (ABT Term abt)
  => View (Term abt) xs a
  -> Env
  -> (abt xs a -> abt '[] b)
  -> abt '[] b
normalizeTail :: View (Term abt) xs a -> Env -> (abt xs a -> abt '[] b) -> abt '[] b
normalizeTail (Var Variable a
v)     Env
env abt xs a -> abt '[] b
ctxt = abt xs a -> abt '[] b
ctxt (Variable a -> Env -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Variable a -> Env -> abt '[] a
normalizeVar Variable a
v Env
env)
normalizeTail (Syn Term abt a
s)     Env
env abt xs a -> abt '[] b
ctxt = Term abt a -> Env -> Context abt a b -> abt '[] b
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
Term abt a -> Env -> Context abt a b -> abt '[] b
normalizeTerm Term abt a
s Env
env abt xs a -> abt '[] b
Context abt a b
ctxt
normalizeTail view :: View (Term abt) xs a
view@Bind{} Env
env abt xs a -> abt '[] b
ctxt = abt xs a -> abt '[] b
ctxt (View (Term abt) xs a -> Env -> abt xs a
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
ABT Term abt =>
View (Term abt) xs a -> Env -> abt xs a
normalizeReset View (Term abt) xs a
view Env
env)
normalizeSave :: View (Term abt) xs a -> Env -> (abt xs a -> abt '[] b) -> abt '[] b
normalizeSave (Var Variable a
v)     Env
env abt xs a -> abt '[] b
ctxt = abt xs a -> abt '[] b
ctxt (Variable a -> Env -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Variable a -> Env -> abt '[] a
normalizeVar Variable a
v Env
env)
normalizeSave (Syn Term abt a
s)     Env
env abt xs a -> abt '[] b
ctxt = Term abt a -> Env -> Context abt a b -> abt '[] b
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
Term abt a -> Env -> Context abt a b -> abt '[] b
normalizeTerm Term abt a
s Env
env abt xs a -> abt '[] b
Context abt a b
giveName
  where giveName :: abt xs a -> abt '[] b
giveName abt xs a
abt' | abt xs a -> Bool
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
ABT Term abt =>
abt xs a -> Bool
isValue abt xs a
abt' = abt xs a -> abt '[] b
ctxt abt xs a
abt'
                      | Bool
otherwise    = abt '[] a -> Context abt a b -> abt '[] b
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] a -> (abt '[] a -> abt '[] b) -> abt '[] b
let_ abt xs a
abt '[] a
abt' abt xs a -> abt '[] b
Context abt a b
ctxt
normalizeSave view :: View (Term abt) xs a
view@Bind{} Env
env abt xs a -> abt '[] b
ctxt = abt xs a -> abt '[] b
ctxt (View (Term abt) xs a -> Env -> abt xs a
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
ABT Term abt =>
View (Term abt) xs a -> Env -> abt xs a
normalizeReset View (Term abt) xs a
view Env
env)

normalizeReset :: (ABT Term abt) => View (Term abt) xs a -> Env -> abt xs a
normalizeReset :: View (Term abt) xs a -> Env -> abt xs a
normalizeReset (Var Variable a
v)    Env
env = Variable a -> Env -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Variable a -> Env -> abt '[] a
normalizeVar Variable a
v Env
env
normalizeReset (Syn Term abt a
s)    Env
env = Term abt a -> Env -> Context abt a a -> abt '[] a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
Term abt a -> Env -> Context abt a b -> abt '[] b
normalizeTerm Term abt a
s Env
env Context abt a a
forall a. a -> a
id
normalizeReset (Bind Variable a
v View (Term abt) xs a
b) Env
env = Variable a -> Env -> (Env -> abt xs a) -> abt (a : xs) a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (xs :: [Hakaru]) (b :: Hakaru).
ABT Term abt =>
Variable a -> Env -> (Env -> abt xs b) -> abt (a : xs) b
remapVar Variable a
v Env
env (View (Term abt) xs a -> Env -> abt xs a
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
ABT Term abt =>
View (Term abt) xs a -> Env -> abt xs a
normalizeReset View (Term abt) xs a
b)

normalizeVar :: (ABT Term abt) => Variable a -> Env -> abt '[] a
normalizeVar :: Variable a -> Env -> abt '[] a
normalizeVar Variable a
v Env
env = Variable a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var (Variable a -> abt '[] a) -> Variable a -> abt '[] a
forall a b. (a -> b) -> a -> b
$ Variable a -> Maybe (Variable a) -> Variable a
forall a. a -> Maybe a -> a
fromMaybe Variable a
v (Variable a -> Env -> Maybe (Variable a)
forall k (a :: k) (ast :: k -> *).
(Show1 Sing, JmEq1 Sing) =>
Variable a -> Assocs ast -> Maybe (ast a)
lookupAssoc Variable a
v Env
env)

isValue
  :: (ABT Term abt)
  => abt xs a
  -> Bool
isValue :: abt xs a -> Bool
isValue abt xs a
abt =
  case abt xs a -> View (Term abt) xs a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt xs a
abt of
    Var{}  -> Bool
True
    Bind{} -> Bool
False
    Syn Term abt a
s  -> Term abt a -> Bool
forall (a :: [Hakaru] -> Hakaru -> *) (b :: Hakaru).
Term a b -> Bool
isValueTerm Term abt a
s
  where
    isValueTerm :: Term a b -> Bool
isValueTerm Literal_{}  = Bool
True
    isValueTerm (SCon args b
Lam_ :$ SArgs a args
_) = Bool
True
    isValueTerm Term a b
_           = Bool
False

normalizeTerm
  :: forall abt a b
  .  (ABT Term abt)
  => Term abt a
  -> Env
  -> Context abt a b
  -> abt '[] b

normalizeTerm :: Term abt a -> Env -> Context abt a b -> abt '[] b
normalizeTerm (SCon args a
Let_ :$ (abt vars a
rhs :* abt vars a
body :* SArgs abt args
End)) Env
env Context abt a b
ctxt =
  abt '[a] a -> (Variable a -> abt '[] a -> abt '[] b) -> abt '[] b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (x :: k) (xs :: [k]) (a :: k) r.
ABT syn abt =>
abt (x : xs) a -> (Variable x -> abt xs a -> r) -> r
caseBind abt vars a
abt '[a] a
body ((Variable a -> abt '[] a -> abt '[] b) -> abt '[] b)
-> (Variable a -> abt '[] a -> abt '[] b) -> abt '[] b
forall a b. (a -> b) -> a -> b
$ \Variable a
v abt '[] a
body' ->
  abt '[] a -> Env -> Context abt a b -> abt '[] b
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] a -> Env -> Context abt a b -> abt '[] b
normalize' abt vars a
abt '[] a
rhs Env
env (Context abt a b -> abt '[] b) -> Context abt a b -> abt '[] b
forall a b. (a -> b) -> a -> b
$ \abt '[] a
rhs' ->
  let mkbody :: Env -> abt '[] b
mkbody Env
env' = abt '[] a -> Env -> (abt '[] a -> abt '[] b) -> abt '[] b
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
ABT Term abt =>
abt '[] a -> Env -> Context abt a b -> abt '[] b
normalize' abt '[] a
body' Env
env' Context abt a b
abt '[] a -> abt '[] b
ctxt
  in Term abt b -> abt '[] b
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (SCon '[LC a, '( '[a], b)] b
forall (a :: Hakaru) (b :: Hakaru). SCon '[LC a, '( '[a], b)] b
Let_ SCon '[LC a, '( '[a], b)] b
-> SArgs abt '[LC a, '( '[a], b)] -> Term abt b
forall (args :: [([Hakaru], Hakaru)]) (a :: Hakaru)
       (abt :: [Hakaru] -> Hakaru -> *).
SCon args a -> SArgs abt args -> Term abt a
:$ abt '[] a
rhs' abt '[] a
-> SArgs abt '[ '( '[a], b)] -> SArgs abt '[LC a, '( '[a], b)]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
       (a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* Variable a -> Env -> (Env -> abt '[] b) -> abt '[a] b
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (xs :: [Hakaru]) (b :: Hakaru).
ABT Term abt =>
Variable a -> Env -> (Env -> abt xs b) -> abt (a : xs) b
remapVar Variable a
v Env
env Env -> abt '[] b
mkbody abt '[a] b -> SArgs abt '[] -> SArgs abt '[ '( '[a], b)]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
       (a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* SArgs abt '[]
forall (abt :: [Hakaru] -> Hakaru -> *). SArgs abt '[]
End)

normalizeTerm (Case_ abt '[] a
cond [Branch a abt a]
bs) Env
env Context abt a b
ctxt =
  View (Term abt) '[] a
-> Env -> (abt '[] a -> abt '[] b) -> abt '[] b
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru) (b :: Hakaru).
ABT Term abt =>
View (Term abt) xs a -> Env -> (abt xs a -> abt '[] b) -> abt '[] b
normalizeSave (abt '[] a -> View (Term abt) '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt '[] a
cond) Env
env ((abt '[] a -> abt '[] b) -> abt '[] b)
-> (abt '[] a -> abt '[] b) -> abt '[] b
forall a b. (a -> b) -> a -> b
$ \ abt '[] a
cond' ->
    let normalizeBranch :: forall xs d . abt xs d -> abt xs d
        normalizeBranch :: abt xs d -> abt xs d
normalizeBranch abt xs d
body = View (Term abt) xs d -> Env -> abt xs d
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru).
ABT Term abt =>
View (Term abt) xs a -> Env -> abt xs a
normalizeReset (abt xs d -> View (Term abt) xs d
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt xs d
body) Env
env
        branches :: [Branch a abt a]
branches = (Branch a abt a -> Branch a abt a)
-> [Branch a abt a] -> [Branch a abt a]
forall a b. (a -> b) -> [a] -> [b]
map ((forall (h :: [Hakaru]) (i :: Hakaru). abt h i -> abt h i)
-> Branch a abt a -> Branch a abt a
forall k1 k2 k3 (f :: (k1 -> k2 -> *) -> k3 -> *)
       (a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3).
Functor21 f =>
(forall (h :: k1) (i :: k2). a h i -> b h i) -> f a j -> f b j
fmap21 forall (h :: [Hakaru]) (i :: Hakaru). abt h i -> abt h i
normalizeBranch) [Branch a abt a]
bs
    -- A possible optimization is to push the context into each conditional,
    -- possibly opening up other optimizations at the cost of code growth.
    in Context abt a b
ctxt Context abt a b -> Context abt a b
forall a b. (a -> b) -> a -> b
$ Term abt a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn (Term abt a -> abt '[] a) -> Term abt a -> abt '[] a
forall a b. (a -> b) -> a -> b
$ abt '[] a -> [Branch a abt a] -> Term abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
       (b :: Hakaru).
abt '[] a -> [Branch a abt b] -> Term abt b
Case_ abt '[] a
cond' [Branch a abt a]
branches

normalizeTerm Term abt a
term Env
env Context abt a b
ctxt = Cont (abt '[] b) (abt '[] a) -> Context abt a b -> abt '[] b
forall r a. Cont r a -> (a -> r) -> r
runCont ((Term abt a -> abt '[] a)
-> ContT (abt '[] b) Identity (Term abt a)
-> Cont (abt '[] b) (abt '[] a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Term abt a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (a :: k).
ABT syn abt =>
syn abt a -> abt '[] a
syn ((forall (h :: [Hakaru]) (i :: Hakaru).
 abt h i -> ContT (abt '[] b) Identity (abt h i))
-> Term abt a -> ContT (abt '[] b) Identity (Term abt a)
forall k1 k2 k3 (t :: (k1 -> k2 -> *) -> k3 -> *) (f :: * -> *)
       (a :: k1 -> k2 -> *) (b :: k1 -> k2 -> *) (j :: k3).
(Traversable21 t, Applicative f) =>
(forall (h :: k1) (i :: k2). a h i -> f (b h i))
-> t a j -> f (t b j)
traverse21 forall (h :: [Hakaru]) (i :: Hakaru).
abt h i -> ContT (abt '[] b) Identity (abt h i)
f Term abt a
term)) Context abt a b
ctxt
  where f :: forall xs c . abt xs c -> Cont (abt '[] b) (abt xs c)
        f :: abt xs c -> Cont (abt '[] b) (abt xs c)
f abt xs c
abt = ((abt xs c -> abt '[] b) -> abt '[] b)
-> Cont (abt '[] b) (abt xs c)
forall a r. ((a -> r) -> r) -> Cont r a
cont (View (Term abt) xs c -> Env -> (abt xs c -> abt '[] b) -> abt '[] b
forall (xs :: [Hakaru]) (c :: Hakaru).
View (Term abt) xs c -> Env -> (abt xs c -> abt '[] b) -> abt '[] b
n (abt xs c -> View (Term abt) xs c
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
       (xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> View (syn abt) xs a
viewABT abt xs c
abt) Env
env)
        n :: forall xs c
          .  View (Term abt) xs c
          -> Env
          -> (abt xs c -> abt '[] b)
          -> abt '[] b
        -- TODO: Can we just let n=normalizeTail or n=normalizeSave?
        n :: View (Term abt) xs c -> Env -> (abt xs c -> abt '[] b) -> abt '[] b
n = case Term abt a
term of SCon args a
MBind         :$ SArgs abt args
_ -> View (Term abt) xs c -> Env -> (abt xs c -> abt '[] b) -> abt '[] b
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru) (b :: Hakaru).
ABT Term abt =>
View (Term abt) xs a -> Env -> (abt xs a -> abt '[] b) -> abt '[] b
normalizeTail
                         SCon args a
Plate         :$ SArgs abt args
_ -> View (Term abt) xs c -> Env -> (abt xs c -> abt '[] b) -> abt '[] b
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru) (b :: Hakaru).
ABT Term abt =>
View (Term abt) xs a -> Env -> (abt xs a -> abt '[] b) -> abt '[] b
normalizeTail
                         SCon args a
Dirac         :$ SArgs abt args
_ -> View (Term abt) xs c -> Env -> (abt xs c -> abt '[] b) -> abt '[] b
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru) (b :: Hakaru).
ABT Term abt =>
View (Term abt) xs a -> Env -> (abt xs a -> abt '[] b) -> abt '[] b
normalizeTail
                         UnsafeFrom_ Coercion a b
_ :$ SArgs abt args
_ -> View (Term abt) xs c -> Env -> (abt xs c -> abt '[] b) -> abt '[] b
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru) (b :: Hakaru).
ABT Term abt =>
View (Term abt) xs a -> Env -> (abt xs a -> abt '[] b) -> abt '[] b
normalizeTail
                         CoerceTo_   Coercion a a
_ :$ SArgs abt args
_ -> View (Term abt) xs c -> Env -> (abt xs c -> abt '[] b) -> abt '[] b
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru) (b :: Hakaru).
ABT Term abt =>
View (Term abt) xs a -> Env -> (abt xs a -> abt '[] b) -> abt '[] b
normalizeTail
                         Term abt a
_                  -> View (Term abt) xs c -> Env -> (abt xs c -> abt '[] b) -> abt '[] b
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [Hakaru])
       (a :: Hakaru) (b :: Hakaru).
ABT Term abt =>
View (Term abt) xs a -> Env -> (abt xs a -> abt '[] b) -> abt '[] b
normalizeSave