{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE ViewPatterns #-}
module Symantic.Parser.Haskell.Optimize where
import Data.Bool (Bool(..))
import Data.Functor.Identity (Identity(..))
import Data.String (String)
import Prelude (undefined)
import Text.Show (Show(..))
import qualified Data.Eq as Eq
import qualified Data.Function as Fun
import qualified Language.Haskell.TH as TH
import qualified Language.Haskell.TH.Syntax as TH
import Symantic.Univariant.Trans
import Symantic.Parser.Haskell.Term
data Term repr a where
Term :: { forall (repr :: * -> *) a. Term repr a -> repr a
unTerm :: repr a } -> Term repr a
(:@) :: Term repr (a->b) -> Term repr a -> Term repr b
Lam :: (Term repr a -> Term repr b) -> Term repr (a->b)
Lam1 :: (Term repr a -> Term repr b) -> Term repr (a->b)
Var :: String -> Term repr a
Char :: (TH.Lift tok, Show tok) => tok -> Term repr tok
Cons :: Term repr (a -> [a] -> [a])
Eq :: Eq.Eq a => Term repr (a -> a -> Bool)
infixl 9 :@
type instance Output (Term repr) = repr
instance Trans repr (Term repr) where
trans :: forall a. repr a -> Term repr a
trans = repr a -> Term repr a
forall (repr :: * -> *) a. repr a -> Term repr a
Term
instance Termable repr => Termable (Term repr) where
lam :: forall a b. (Term repr a -> Term repr b) -> Term repr (a -> b)
lam = (Term repr a -> Term repr b) -> Term repr (a -> b)
forall (repr :: * -> *) a b.
(Term repr a -> Term repr b) -> Term repr (a -> b)
Lam
lam1 :: forall a b. (Term repr a -> Term repr b) -> Term repr (a -> b)
lam1 = (Term repr a -> Term repr b) -> Term repr (a -> b)
forall (repr :: * -> *) a b.
(Term repr a -> Term repr b) -> Term repr (a -> b)
Lam1
.@ :: forall a b. Term repr (a -> b) -> Term repr a -> Term repr b
(.@) = Term repr (a -> b) -> Term repr a -> Term repr b
forall (repr :: * -> *) a b.
Term repr (a -> b) -> Term repr a -> Term repr b
(:@)
cons :: forall a. Term repr (a -> [a] -> [a])
cons = Term repr (a -> [a] -> [a])
forall (repr :: * -> *) a. Term repr (a -> [a] -> [a])
Cons
eq :: forall a. Eq a => Term repr (a -> a -> Bool)
eq = Term repr (a -> a -> Bool)
forall a (repr :: * -> *). Eq a => Term repr (a -> a -> Bool)
Eq
unit :: Term repr ()
unit = repr () -> Term repr ()
forall (repr :: * -> *) a. repr a -> Term repr a
Term repr ()
forall (repr :: * -> *). Termable repr => repr ()
unit
bool :: Bool -> Term repr Bool
bool Bool
b = repr Bool -> Term repr Bool
forall (repr :: * -> *) a. repr a -> Term repr a
Term (Bool -> repr Bool
forall (repr :: * -> *). Termable repr => Bool -> repr Bool
bool Bool
b)
char :: forall tok. (Lift tok, Show tok) => tok -> Term repr tok
char = tok -> Term repr tok
forall tok (repr :: * -> *).
(Lift tok, Show tok) =>
tok -> Term repr tok
Char
nil :: forall a. Term repr [a]
nil = repr [a] -> Term repr [a]
forall (repr :: * -> *) a. repr a -> Term repr a
Term repr [a]
forall (repr :: * -> *) a. Termable repr => repr [a]
nil
left :: forall l r. Term repr (l -> Either l r)
left = repr (l -> Either l r) -> Term repr (l -> Either l r)
forall (repr :: * -> *) a. repr a -> Term repr a
Term repr (l -> Either l r)
forall (repr :: * -> *) l r.
Termable repr =>
repr (l -> Either l r)
left
right :: forall r l. Term repr (r -> Either l r)
right = repr (r -> Either l r) -> Term repr (r -> Either l r)
forall (repr :: * -> *) a. repr a -> Term repr a
Term repr (r -> Either l r)
forall (repr :: * -> *) r l.
Termable repr =>
repr (r -> Either l r)
right
nothing :: forall a. Term repr (Maybe a)
nothing = repr (Maybe a) -> Term repr (Maybe a)
forall (repr :: * -> *) a. repr a -> Term repr a
Term repr (Maybe a)
forall (repr :: * -> *) a. Termable repr => repr (Maybe a)
nothing
just :: forall a. Term repr (a -> Maybe a)
just = repr (a -> Maybe a) -> Term repr (a -> Maybe a)
forall (repr :: * -> *) a. repr a -> Term repr a
Term repr (a -> Maybe a)
forall (repr :: * -> *) a. Termable repr => repr (a -> Maybe a)
just
const :: forall a b. Term repr (a -> b -> a)
const = (Term repr a -> Term repr (b -> a)) -> Term repr (a -> b -> a)
forall (repr :: * -> *) a b.
(Term repr a -> Term repr b) -> Term repr (a -> b)
Lam1 (\Term repr a
x -> (Term repr b -> Term repr a) -> Term repr (b -> a)
forall (repr :: * -> *) a b.
(Term repr a -> Term repr b) -> Term repr (a -> b)
Lam1 (\Term repr b
_y -> Term repr a
x))
flip :: forall a b c. Term repr ((a -> b -> c) -> b -> a -> c)
flip = (Term repr (a -> b -> c) -> Term repr (b -> a -> c))
-> Term repr ((a -> b -> c) -> b -> a -> c)
forall (repr :: * -> *) a b.
(Term repr a -> Term repr b) -> Term repr (a -> b)
Lam1 (\Term repr (a -> b -> c)
f -> (Term repr b -> Term repr (a -> c)) -> Term repr (b -> a -> c)
forall (repr :: * -> *) a b.
(Term repr a -> Term repr b) -> Term repr (a -> b)
Lam1 (\Term repr b
x -> (Term repr a -> Term repr c) -> Term repr (a -> c)
forall (repr :: * -> *) a b.
(Term repr a -> Term repr b) -> Term repr (a -> b)
Lam1 (\Term repr a
y -> Term repr (a -> b -> c)
f Term repr (a -> b -> c) -> Term repr a -> Term repr (b -> c)
forall (repr :: * -> *) a b.
Termable repr =>
repr (a -> b) -> repr a -> repr b
.@ Term repr a
y Term repr (b -> c) -> Term repr b -> Term repr c
forall (repr :: * -> *) a b.
Termable repr =>
repr (a -> b) -> repr a -> repr b
.@ Term repr b
x)))
id :: forall a. Term repr (a -> a)
id = (Term repr a -> Term repr a) -> Term repr (a -> a)
forall (repr :: * -> *) a b.
(Term repr a -> Term repr b) -> Term repr (a -> b)
Lam1 (\Term repr a
x -> Term repr a
x)
$ :: forall a b. Term repr ((a -> b) -> a -> b)
($) = (Term repr (a -> b) -> Term repr (a -> b))
-> Term repr ((a -> b) -> a -> b)
forall (repr :: * -> *) a b.
(Term repr a -> Term repr b) -> Term repr (a -> b)
Lam1 (\Term repr (a -> b)
f -> (Term repr a -> Term repr b) -> Term repr (a -> b)
forall (repr :: * -> *) a b.
(Term repr a -> Term repr b) -> Term repr (a -> b)
Lam1 (\Term repr a
x -> Term repr (a -> b)
f Term repr (a -> b) -> Term repr a -> Term repr b
forall (repr :: * -> *) a b.
Termable repr =>
repr (a -> b) -> repr a -> repr b
.@ Term repr a
x))
. :: forall b c a. Term repr ((b -> c) -> (a -> b) -> a -> c)
(.) = (Term repr (b -> c) -> Term repr ((a -> b) -> a -> c))
-> Term repr ((b -> c) -> (a -> b) -> a -> c)
forall (repr :: * -> *) a b.
(Term repr a -> Term repr b) -> Term repr (a -> b)
Lam1 (\Term repr (b -> c)
f -> (Term repr (a -> b) -> Term repr (a -> c))
-> Term repr ((a -> b) -> a -> c)
forall (repr :: * -> *) a b.
(Term repr a -> Term repr b) -> Term repr (a -> b)
Lam1 (\Term repr (a -> b)
g -> (Term repr a -> Term repr c) -> Term repr (a -> c)
forall (repr :: * -> *) a b.
(Term repr a -> Term repr b) -> Term repr (a -> b)
Lam1 (\Term repr a
x -> Term repr (b -> c)
f Term repr (b -> c) -> Term repr b -> Term repr c
forall (repr :: * -> *) a b.
Termable repr =>
repr (a -> b) -> repr a -> repr b
.@ (Term repr (a -> b)
g Term repr (a -> b) -> Term repr a -> Term repr b
forall (repr :: * -> *) a b.
Termable repr =>
repr (a -> b) -> repr a -> repr b
.@ Term repr a
x))))
optimizeTerm :: Term repr a -> Term repr a
optimizeTerm :: forall (repr :: * -> *) a. Term repr a -> Term repr a
optimizeTerm = Term repr a -> Term repr a
forall (repr :: * -> *) a. Term repr a -> Term repr a
nor
where
nor :: Term repr a -> Term repr a
nor :: forall (repr :: * -> *) a. Term repr a -> Term repr a
nor = \case
Lam Term repr a -> Term repr b
f -> (Term repr a -> Term repr b) -> Term repr (a -> b)
forall (repr :: * -> *) a b.
(Term repr a -> Term repr b) -> Term repr (a -> b)
Lam (Term repr b -> Term repr b
forall (repr :: * -> *) a. Term repr a -> Term repr a
nor (Term repr b -> Term repr b)
-> (Term repr a -> Term repr b) -> Term repr a -> Term repr b
forall b c a. (b -> c) -> (a -> b) -> a -> c
Fun.. Term repr a -> Term repr b
f)
Lam1 Term repr a -> Term repr b
f -> (Term repr a -> Term repr b) -> Term repr (a -> b)
forall (repr :: * -> *) a b.
(Term repr a -> Term repr b) -> Term repr (a -> b)
Lam1 (Term repr b -> Term repr b
forall (repr :: * -> *) a. Term repr a -> Term repr a
nor (Term repr b -> Term repr b)
-> (Term repr a -> Term repr b) -> Term repr a -> Term repr b
forall b c a. (b -> c) -> (a -> b) -> a -> c
Fun.. Term repr a -> Term repr b
f)
Term repr (a -> a)
x :@ Term repr a
y -> case Term repr (a -> a) -> Term repr (a -> a)
forall (repr :: * -> *) a. Term repr a -> Term repr a
whnf Term repr (a -> a)
x of
Lam1 Term repr a -> Term repr b
f -> Term repr b -> Term repr b
forall (repr :: * -> *) a. Term repr a -> Term repr a
nor (Term repr a -> Term repr b
f Term repr a
Term repr a
y)
Term repr (a -> a)
x' -> Term repr (a -> a) -> Term repr (a -> a)
forall (repr :: * -> *) a. Term repr a -> Term repr a
nor Term repr (a -> a)
x' Term repr (a -> a) -> Term repr a -> Term repr a
forall (repr :: * -> *) a b.
Term repr (a -> b) -> Term repr a -> Term repr b
:@ Term repr a -> Term repr a
forall (repr :: * -> *) a. Term repr a -> Term repr a
nor Term repr a
y
Term repr a
x -> Term repr a
x
whnf :: Term repr a -> Term repr a
whnf :: forall (repr :: * -> *) a. Term repr a -> Term repr a
whnf = \case
Term repr (a -> a)
x :@ Term repr a
y -> case Term repr (a -> a) -> Term repr (a -> a)
forall (repr :: * -> *) a. Term repr a -> Term repr a
whnf Term repr (a -> a)
x of
Lam1 Term repr a -> Term repr b
f -> Term repr b -> Term repr b
forall (repr :: * -> *) a. Term repr a -> Term repr a
whnf (Term repr a -> Term repr b
f Term repr a
Term repr a
y)
Term repr (a -> a)
x' -> Term repr (a -> a)
x' Term repr (a -> a) -> Term repr a -> Term repr a
forall (repr :: * -> *) a b.
Term repr (a -> b) -> Term repr a -> Term repr b
:@ Term repr a
y
Term repr a
x -> Term repr a
x
instance Trans (Term Identity) Identity where
trans :: forall a. Term Identity a -> Identity a
trans = \case
Term Identity a
Cons -> Identity a
forall (repr :: * -> *) a. Termable repr => repr (a -> [a] -> [a])
cons
Char a
t -> a -> Identity a
forall (repr :: * -> *) tok.
(Termable repr, Lift tok, Show tok) =>
tok -> repr tok
char a
t
Term Identity a
Eq -> Identity a
forall (repr :: * -> *) a.
(Termable repr, Eq a) =>
repr (a -> a -> Bool)
eq
Term Identity a
repr -> Identity a
repr
Term Identity (a -> a)
x :@ Term Identity a
y -> a -> Identity a
forall a. a -> Identity a
Identity (Identity (a -> a) -> a -> a
forall a. Identity a -> a
runIdentity (Term Identity (a -> a) -> Identity (a -> a)
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans Term Identity (a -> a)
x) (Identity a -> a
forall a. Identity a -> a
runIdentity (Term Identity a -> Identity a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans Term Identity a
y)))
Lam Term Identity a -> Term Identity b
f -> (a -> b) -> Identity (a -> b)
forall a. a -> Identity a
Identity (Identity b -> b
forall a. Identity a -> a
runIdentity (Identity b -> b) -> (a -> Identity b) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
Fun.. Term Identity b -> Identity b
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans (Term Identity b -> Identity b)
-> (a -> Term Identity b) -> a -> Identity b
forall b c a. (b -> c) -> (a -> b) -> a -> c
Fun.. Term Identity a -> Term Identity b
f (Term Identity a -> Term Identity b)
-> (a -> Term Identity a) -> a -> Term Identity b
forall b c a. (b -> c) -> (a -> b) -> a -> c
Fun.. Identity a -> Term Identity a
forall (repr :: * -> *) a. repr a -> Term repr a
Term (Identity a -> Term Identity a)
-> (a -> Identity a) -> a -> Term Identity a
forall b c a. (b -> c) -> (a -> b) -> a -> c
Fun.. a -> Identity a
forall a. a -> Identity a
Identity)
Lam1 Term Identity a -> Term Identity b
f -> Term Identity (a -> b) -> Identity (a -> b)
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans ((Term Identity a -> Term Identity b) -> Term Identity (a -> b)
forall (repr :: * -> *) a b.
(Term repr a -> Term repr b) -> Term repr (a -> b)
Lam Term Identity a -> Term Identity b
f)
Var{} -> Identity a
forall a. HasCallStack => a
undefined
instance Trans (Term TH.CodeQ) TH.CodeQ where
trans :: forall a. Term CodeQ a -> CodeQ a
trans = \case
Term CodeQ (a -> a -> a)
Cons :@ Term CodeQ a
x :@ Term CodeQ a
y -> [|| $$(trans x) : $$(trans y) ||]
Term CodeQ (a -> a)
Cons :@ Term CodeQ a
x -> [|| ($$(trans x) :) ||]
Term CodeQ a
Cons -> CodeQ a
forall (repr :: * -> *) a. Termable repr => repr (a -> [a] -> [a])
cons
Char a
t -> a -> CodeQ a
forall (repr :: * -> *) tok.
(Termable repr, Lift tok, Show tok) =>
tok -> repr tok
char a
t
Term CodeQ (a -> a -> a)
Eq :@ Term CodeQ a
x :@ Term CodeQ a
y -> [|| $$(trans x) Eq.== $$(trans y) ||]
Term CodeQ (a -> a)
Eq :@ Term CodeQ a
x -> [|| ($$(trans x) Eq.==) ||]
Term CodeQ a
Eq -> CodeQ a
forall (repr :: * -> *) a.
(Termable repr, Eq a) =>
repr (a -> a -> Bool)
eq
Term CodeQ a
repr -> CodeQ a
repr
Term CodeQ (a -> a)
x :@ Term CodeQ a
y -> [|| $$(trans x) $$(trans y) ||]
Lam Term CodeQ a -> Term CodeQ b
f -> [|| \x -> $$(trans (f (Term [||x||]))) ||]
Lam1 Term CodeQ a -> Term CodeQ b
f -> Term CodeQ (a -> b) -> Code Q (a -> b)
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans ((Term CodeQ a -> Term CodeQ b) -> Term CodeQ (a -> b)
forall (repr :: * -> *) a b.
(Term repr a -> Term repr b) -> Term repr (a -> b)
Lam Term CodeQ a -> Term CodeQ b
f)
Var{} -> CodeQ a
forall a. HasCallStack => a
undefined
instance Trans (Term ValueCode) ValueCode where
trans :: forall a. Term ValueCode a -> ValueCode a
trans = \case
Term ValueCode a
x -> ValueCode a
x
Char a
c -> a -> ValueCode a
forall (repr :: * -> *) tok.
(Termable repr, Lift tok, Show tok) =>
tok -> repr tok
char a
c
Term ValueCode a
Cons -> ValueCode a
forall (repr :: * -> *) a. Termable repr => repr (a -> [a] -> [a])
cons
Term ValueCode a
Eq -> ValueCode a
forall (repr :: * -> *) a.
(Termable repr, Eq a) =>
repr (a -> a -> Bool)
eq
(:@) Term ValueCode (a -> a)
f Term ValueCode a
x -> ValueCode (a -> a) -> ValueCode a -> ValueCode a
forall (repr :: * -> *) a b.
Termable repr =>
repr (a -> b) -> repr a -> repr b
(.@) (Term ValueCode (a -> a) -> ValueCode (a -> a)
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans Term ValueCode (a -> a)
f) (Term ValueCode a -> ValueCode a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans Term ValueCode a
x)
Lam Term ValueCode a -> Term ValueCode b
f -> ValueCode :: forall a. a -> CodeQ a -> ValueCode a
ValueCode
{ value :: a -> b
value = ValueCode b -> b
forall a. ValueCode a -> a
value (ValueCode b -> b) -> (a -> ValueCode b) -> a -> b
forall b c a. (b -> c) -> (a -> b) -> a -> c
Fun.. Term ValueCode b -> ValueCode b
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans (Term ValueCode b -> ValueCode b)
-> (a -> Term ValueCode b) -> a -> ValueCode b
forall b c a. (b -> c) -> (a -> b) -> a -> c
Fun.. Term ValueCode a -> Term ValueCode b
f (Term ValueCode a -> Term ValueCode b)
-> (a -> Term ValueCode a) -> a -> Term ValueCode b
forall b c a. (b -> c) -> (a -> b) -> a -> c
Fun.. ValueCode a -> Term ValueCode a
forall (repr :: * -> *) a. repr a -> Term repr a
Term (ValueCode a -> Term ValueCode a)
-> (a -> ValueCode a) -> a -> Term ValueCode a
forall b c a. (b -> c) -> (a -> b) -> a -> c
Fun.. (a -> CodeQ a -> ValueCode a
forall a. a -> CodeQ a -> ValueCode a
`ValueCode` CodeQ a
forall a. HasCallStack => a
undefined)
, code :: CodeQ (a -> b)
code = [|| \x -> $$(code Fun.. trans Fun.. f Fun.. Term Fun.. (undefined `ValueCode`) Fun.$ [||x||]) ||]
}
Lam1 Term ValueCode a -> Term ValueCode b
f -> Term ValueCode (a -> b) -> ValueCode (a -> b)
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans ((Term ValueCode a -> Term ValueCode b) -> Term ValueCode (a -> b)
forall (repr :: * -> *) a b.
(Term repr a -> Term repr b) -> Term repr (a -> b)
Lam Term ValueCode a -> Term ValueCode b
f)
Var{} -> ValueCode a
forall a. HasCallStack => a
undefined
instance Trans (Term ValueCode) (Term TH.CodeQ) where
trans :: forall a. Term ValueCode a -> Term CodeQ a
trans = \case
Term ValueCode a
x -> Code Q a -> Term CodeQ a
forall (repr :: * -> *) a. repr a -> Term repr a
Term (ValueCode a -> Code Q a
forall a. ValueCode a -> CodeQ a
code ValueCode a
x)
Char a
c -> a -> Term CodeQ a
forall (repr :: * -> *) tok.
(Termable repr, Lift tok, Show tok) =>
tok -> repr tok
char a
c
Term ValueCode a
Cons -> Term CodeQ a
forall (repr :: * -> *) a. Termable repr => repr (a -> [a] -> [a])
cons
Term ValueCode a
Eq -> Term CodeQ a
forall (repr :: * -> *) a.
(Termable repr, Eq a) =>
repr (a -> a -> Bool)
eq
(:@) Term ValueCode (a -> a)
f Term ValueCode a
x -> Term CodeQ (a -> a) -> Term CodeQ a -> Term CodeQ a
forall (repr :: * -> *) a b.
Termable repr =>
repr (a -> b) -> repr a -> repr b
(.@) (Term ValueCode (a -> a) -> Term CodeQ (a -> a)
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans Term ValueCode (a -> a)
f) (Term ValueCode a -> Term CodeQ a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans Term ValueCode a
x)
Lam Term ValueCode a -> Term ValueCode b
f -> (Term CodeQ a -> Term CodeQ b) -> Term CodeQ (a -> b)
forall (repr :: * -> *) a b.
(Term repr a -> Term repr b) -> Term repr (a -> b)
Lam (\Term CodeQ a
x -> Term ValueCode b -> Term CodeQ b
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans (Term ValueCode a -> Term ValueCode b
f (Term CodeQ a -> Term ValueCode a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans Term CodeQ a
x)))
Lam1 Term ValueCode a -> Term ValueCode b
f -> (Term CodeQ a -> Term CodeQ b) -> Term CodeQ (a -> b)
forall (repr :: * -> *) a b.
(Term repr a -> Term repr b) -> Term repr (a -> b)
Lam1 (\Term CodeQ a
x -> Term ValueCode b -> Term CodeQ b
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans (Term ValueCode a -> Term ValueCode b
f (Term CodeQ a -> Term ValueCode a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans Term CodeQ a
x)))
Var String
v -> String -> Term CodeQ a
forall (repr :: * -> *) a. String -> Term repr a
Var String
v
instance Trans (Term TH.CodeQ) (Term ValueCode) where
trans :: forall a. Term CodeQ a -> Term ValueCode a
trans = \case
Term CodeQ a
x -> ValueCode a -> Term ValueCode a
forall (repr :: * -> *) a. repr a -> Term repr a
Term (a -> CodeQ a -> ValueCode a
forall a. a -> CodeQ a -> ValueCode a
ValueCode a
forall a. HasCallStack => a
undefined CodeQ a
x)
Char a
c -> a -> Term ValueCode a
forall (repr :: * -> *) tok.
(Termable repr, Lift tok, Show tok) =>
tok -> repr tok
char a
c
Term CodeQ a
Cons -> Term ValueCode a
forall (repr :: * -> *) a. Termable repr => repr (a -> [a] -> [a])
cons
Term CodeQ a
Eq -> Term ValueCode a
forall (repr :: * -> *) a.
(Termable repr, Eq a) =>
repr (a -> a -> Bool)
eq
(:@) Term CodeQ (a -> a)
f Term CodeQ a
x -> Term ValueCode (a -> a) -> Term ValueCode a -> Term ValueCode a
forall (repr :: * -> *) a b.
Termable repr =>
repr (a -> b) -> repr a -> repr b
(.@) (Term CodeQ (a -> a) -> Term ValueCode (a -> a)
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans Term CodeQ (a -> a)
f) (Term CodeQ a -> Term ValueCode a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans Term CodeQ a
x)
Lam Term CodeQ a -> Term CodeQ b
f -> (Term ValueCode a -> Term ValueCode b) -> Term ValueCode (a -> b)
forall (repr :: * -> *) a b.
(Term repr a -> Term repr b) -> Term repr (a -> b)
Lam (\Term ValueCode a
x -> Term CodeQ b -> Term ValueCode b
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans (Term CodeQ a -> Term CodeQ b
f (Term ValueCode a -> Term CodeQ a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans Term ValueCode a
x)))
Lam1 Term CodeQ a -> Term CodeQ b
f -> (Term ValueCode a -> Term ValueCode b) -> Term ValueCode (a -> b)
forall (repr :: * -> *) a b.
(Term repr a -> Term repr b) -> Term repr (a -> b)
Lam1 (\Term ValueCode a
x -> Term CodeQ b -> Term ValueCode b
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans (Term CodeQ a -> Term CodeQ b
f (Term ValueCode a -> Term CodeQ a
forall (from :: * -> *) (to :: * -> *) a.
Trans from to =>
from a -> to a
trans Term ValueCode a
x)))
Var String
v -> String -> Term ValueCode a
forall (repr :: * -> *) a. String -> Term repr a
Var String
v