{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
module Test.IOTasks.Term.Prelude (
  -- * Accessors
  currentValue, allValues,
  valueBefore, valuesBefore,
  -- * Arithmetic functions
  (.+.), (.-.), (.*.),
  intLit,
  -- * Comparison functions
  (.==.), (./=.), (.>.), (.>=.), (.<.), (.<=.),
  -- * Boolean functions
  not',
  (.&&.), (.||.),
  true, false,
  -- * embedded values
  embeddedLit,
  -- * Simple list functions
  sum', product', length', reverse',
  isIn, isNotIn,
  listLit,
  -- * Complexer list functions
  filter',
  -- * Lifting of opaque functions
  liftOpaqueValue, liftOpaque, liftOpaque2,
  ) where

import Data.Char (isAlphaNum)
import Data.Express (Expr((:$)), value)

import Test.IOTasks.Internal.Term (Term(..), TermKind(..), toExpr, transparentSubterms, termVarExps)
import Test.IOTasks.Var (VarExp(..), Embedded, varname, Embeddable)

import Type.Match (matchType, inCaseOfE', inCaseOfApp', fallbackCase')
import Type.Reflection (Typeable, typeRep, (:~~:)(HRefl))

currentValue :: (Typeable a, VarExp e) => e a -> Term k a
-- ^ Defined as @'currentValue' = 'valueBefore' 0@, providing access to the current value.
currentValue :: forall a (e :: * -> *) (k :: TermKind).
(Typeable a, VarExp e) =>
e a -> Term k a
currentValue = Int -> e a -> Term k a
forall a (e :: * -> *) (k :: TermKind).
(Typeable a, VarExp e) =>
Int -> e a -> Term k a
valueBefore Int
0

allValues :: (Typeable a, VarExp e) => e a -> Term k [a]
-- ^ Defined as @'allValues' = 'valuesBefore' 0@, providing access to all values.
allValues :: forall a (e :: * -> *) (k :: TermKind).
(Typeable a, VarExp e) =>
e a -> Term k [a]
allValues = Int -> e a -> Term k [a]
forall a (e :: * -> *) (k :: TermKind).
(Typeable a, VarExp e) =>
Int -> e a -> Term k [a]
valuesBefore Int
0

valueBefore :: (Typeable a, VarExp e) => Int -> e a -> Term k a
-- ^ If the variable-expression x is associated with the values [x_1,..,x_n],
-- @'valueBefore' i x@ provides access to x_(n-i).
valueBefore :: forall a (e :: * -> *) (k :: TermKind).
(Typeable a, VarExp e) =>
Int -> e a -> Term k a
valueBefore = Int -> e a -> Term k a
forall a (e :: * -> *) (k :: TermKind).
(Typeable a, VarExp e) =>
Int -> e a -> Term k a
valueBefore' where
  valueBefore' :: forall a e k. (Typeable a, VarExp e) => Int -> e a -> Term k a
  valueBefore' :: forall a (e :: * -> *) (k :: TermKind).
(Typeable a, VarExp e) =>
Int -> e a -> Term k a
valueBefore' Int
n e a
x = e a -> Term k a -> Term k a
forall (e :: * -> *) a x. VarExp e => e a -> x -> x
checkNames e a
x (Term k a -> Term k a) -> Term k a -> Term k a
forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k) r. Typeable a => [Case a r] -> r
forall a r. Typeable a => [Case a r] -> r
matchType @a
    [ forall {k1} {k} (a :: k1) (x :: k) r.
Typeable a =>
((a :~~: x) -> r) -> Case x r
forall a x r. Typeable a => ((a :~~: x) -> r) -> Case x r
inCaseOfE' @Integer (((Integer :~~: a) -> Term k a) -> Case a (Term k a))
-> ((Integer :~~: a) -> Term k a) -> Case a (Term k a)
forall a b. (a -> b) -> a -> b
$ \Integer :~~: a
HRefl -> e a -> Int -> Term k a
forall (e :: * -> *) a (k :: TermKind).
VarExp e =>
e a -> Int -> Term k a
Current e a
x Int
n
    , forall {k1} {k} (a :: k1) (x :: k) r.
Typeable a =>
((a :~~: x) -> r) -> Case x r
forall a x r. Typeable a => ((a :~~: x) -> r) -> Case x r
inCaseOfE' @Bool (((Bool :~~: a) -> Term k a) -> Case a (Term k a))
-> ((Bool :~~: a) -> Term k a) -> Case a (Term k a)
forall a b. (a -> b) -> a -> b
$ \Bool :~~: a
HRefl -> e a -> Int -> Term k a
forall (e :: * -> *) a (k :: TermKind).
VarExp e =>
e a -> Int -> Term k a
Current e a
x Int
n
    , forall {k1} {k} (a :: k1) (x :: k) r.
Typeable a =>
((a :~~: x) -> r) -> Case x r
forall a x r. Typeable a => ((a :~~: x) -> r) -> Case x r
inCaseOfE' @String (((String :~~: a) -> Term k a) -> Case a (Term k a))
-> ((String :~~: a) -> Term k a) -> Case a (Term k a)
forall a b. (a -> b) -> a -> b
$ \String :~~: a
HRefl -> e a -> Int -> Term k a
forall (e :: * -> *) a (k :: TermKind).
VarExp e =>
e a -> Int -> Term k a
Current e a
x Int
n
    , forall {k1} {k2} {k3} (f :: k1 -> k2) (x :: k3) r.
Typeable f =>
(forall (a :: k1). (f a :~~: x) -> r) -> Case x r
forall (f :: * -> *) x r.
Typeable f =>
(forall a. (f a :~~: x) -> r) -> Case x r
inCaseOfApp' @Embedded ((forall a. (Embedded a :~~: a) -> Term k a) -> Case a (Term k a))
-> (forall a. (Embedded a :~~: a) -> Term k a) -> Case a (Term k a)
forall a b. (a -> b) -> a -> b
$ \Embedded a :~~: a
HRefl -> e a -> Int -> Term k a
forall (e :: * -> *) a (k :: TermKind).
VarExp e =>
e a -> Int -> Term k a
Current e a
x Int
n
    , Term k a -> Case a (Term k a)
forall {k} r (x :: k). r -> Case x r
fallbackCase' (Term k a -> Case a (Term k a)) -> Term k a -> Case a (Term k a)
forall a b. (a -> b) -> a -> b
$ String -> Term k a
forall a. HasCallStack => String -> a
error (String -> Term k a) -> String -> Term k a
forall a b. (a -> b) -> a -> b
$ String
"variable type not supported for Terms: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRep a -> String
forall a. Show a => a -> String
show (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a)
    ]
valuesBefore :: (Typeable a, VarExp e) => Int -> e a -> Term k [a]
-- ^ If the variable-expression x is associated with the values [x_1,..,x_n],
-- @'valuesBefore' i x@ provides access to [x_1,..,x_(n-i)].
valuesBefore :: forall a (e :: * -> *) (k :: TermKind).
(Typeable a, VarExp e) =>
Int -> e a -> Term k [a]
valuesBefore = Int -> e a -> Term k [a]
forall a (e :: * -> *) (k :: TermKind).
(Typeable a, VarExp e) =>
Int -> e a -> Term k [a]
valuesBefore' where
  valuesBefore' :: forall a e k. (Typeable a, VarExp e) => Int -> e a -> Term k [a]
  valuesBefore' :: forall a (e :: * -> *) (k :: TermKind).
(Typeable a, VarExp e) =>
Int -> e a -> Term k [a]
valuesBefore' Int
n e a
x = e a -> Term k [a] -> Term k [a]
forall (e :: * -> *) a x. VarExp e => e a -> x -> x
checkNames e a
x (Term k [a] -> Term k [a]) -> Term k [a] -> Term k [a]
forall a b. (a -> b) -> a -> b
$ forall {k} (a :: k) r. Typeable a => [Case a r] -> r
forall a r. Typeable a => [Case a r] -> r
matchType @a
    [ forall {k1} {k} (a :: k1) (x :: k) r.
Typeable a =>
((a :~~: x) -> r) -> Case x r
forall a x r. Typeable a => ((a :~~: x) -> r) -> Case x r
inCaseOfE' @Integer (((Integer :~~: a) -> Term k [a]) -> Case a (Term k [a]))
-> ((Integer :~~: a) -> Term k [a]) -> Case a (Term k [a])
forall a b. (a -> b) -> a -> b
$ \Integer :~~: a
HRefl -> e a -> Int -> Term k [a]
forall a1 (e :: * -> *) (k :: TermKind).
(Typeable a1, VarExp e) =>
e a1 -> Int -> Term k [a1]
All e a
x Int
n
    , forall {k1} {k} (a :: k1) (x :: k) r.
Typeable a =>
((a :~~: x) -> r) -> Case x r
forall a x r. Typeable a => ((a :~~: x) -> r) -> Case x r
inCaseOfE' @Bool (((Bool :~~: a) -> Term k [a]) -> Case a (Term k [a]))
-> ((Bool :~~: a) -> Term k [a]) -> Case a (Term k [a])
forall a b. (a -> b) -> a -> b
$ \Bool :~~: a
HRefl -> e a -> Int -> Term k [a]
forall a1 (e :: * -> *) (k :: TermKind).
(Typeable a1, VarExp e) =>
e a1 -> Int -> Term k [a1]
All e a
x Int
n
    , forall {k1} {k} (a :: k1) (x :: k) r.
Typeable a =>
((a :~~: x) -> r) -> Case x r
forall a x r. Typeable a => ((a :~~: x) -> r) -> Case x r
inCaseOfE' @String (((String :~~: a) -> Term k [a]) -> Case a (Term k [a]))
-> ((String :~~: a) -> Term k [a]) -> Case a (Term k [a])
forall a b. (a -> b) -> a -> b
$ \String :~~: a
HRefl -> e a -> Int -> Term k [a]
forall a1 (e :: * -> *) (k :: TermKind).
(Typeable a1, VarExp e) =>
e a1 -> Int -> Term k [a1]
All e a
x Int
n
    , forall {k1} {k2} {k3} (f :: k1 -> k2) (x :: k3) r.
Typeable f =>
(forall (a :: k1). (f a :~~: x) -> r) -> Case x r
forall (f :: * -> *) x r.
Typeable f =>
(forall a. (f a :~~: x) -> r) -> Case x r
inCaseOfApp' @Embedded ((forall a. (Embedded a :~~: a) -> Term k [a])
 -> Case a (Term k [a]))
-> (forall a. (Embedded a :~~: a) -> Term k [a])
-> Case a (Term k [a])
forall a b. (a -> b) -> a -> b
$ \Embedded a :~~: a
HRefl -> e a -> Int -> Term k [a]
forall a1 (e :: * -> *) (k :: TermKind).
(Typeable a1, VarExp e) =>
e a1 -> Int -> Term k [a1]
All e a
x Int
n
    , Term k [a] -> Case a (Term k [a])
forall {k} r (x :: k). r -> Case x r
fallbackCase' (Term k [a] -> Case a (Term k [a]))
-> Term k [a] -> Case a (Term k [a])
forall a b. (a -> b) -> a -> b
$ String -> Term k [a]
forall a. HasCallStack => String -> a
error (String -> Term k [a]) -> String -> Term k [a]
forall a b. (a -> b) -> a -> b
$ String
"variable type not supported for Terms: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRep a -> String
forall a. Show a => a -> String
show (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a)
    ]

checkNames :: VarExp e => e a -> x -> x
checkNames :: forall (e :: * -> *) a x. VarExp e => e a -> x -> x
checkNames = (Var a -> (x -> x) -> x -> x) -> (x -> x) -> [Var a] -> x -> x
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (String -> (x -> x) -> x -> x
forall {p}. String -> p -> p
f (String -> (x -> x) -> x -> x)
-> (Var a -> String) -> Var a -> (x -> x) -> x -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var a -> String
forall a. Var a -> String
varname) x -> x
forall a. a -> a
id ([Var a] -> x -> x) -> (e a -> [Var a]) -> e a -> x -> x
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e a -> [Var a]
forall a. e a -> [Var a]
forall (e :: * -> *) a. VarExp e => e a -> [Var a]
toVarList
  where
    f :: String -> p -> p
f String
x p
c = if String -> Bool
legalVar String
x then p
c else String -> p
forall a. HasCallStack => String -> a
error (String -> p) -> String -> p
forall a b. (a -> b) -> a -> b
$ String
"illegal variable name: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\variable names must start with a letter and can only contain letters, digits, _ and '"

legalVar :: String -> Bool
legalVar :: String -> Bool
legalVar [] = Bool
False
legalVar (Char
x:String
xs) = Char -> Bool
isAlphaNum Char
x Bool -> Bool -> Bool
&& (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\Char
c -> Char -> Bool
isAlphaNum Char
c Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'_' Bool -> Bool -> Bool
|| Char
c Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
== Char
'\'') String
xs

(.+.) :: Term k Integer -> Term k Integer -> Term k Integer
.+. :: forall (k :: TermKind).
Term k Integer -> Term k Integer -> Term k Integer
(.+.) = Term k Integer -> Term k Integer -> Term k Integer
forall a (k :: TermKind). Num a => Term k a -> Term k a -> Term k a
Add

(.-.) :: Term k Integer -> Term k Integer -> Term k Integer
.-. :: forall (k :: TermKind).
Term k Integer -> Term k Integer -> Term k Integer
(.-.) = Term k Integer -> Term k Integer -> Term k Integer
forall a (k :: TermKind). Num a => Term k a -> Term k a -> Term k a
Sub

(.*.) :: Term k Integer -> Term k Integer -> Term k Integer
.*. :: forall (k :: TermKind).
Term k Integer -> Term k Integer -> Term k Integer
(.*.) = Term k Integer -> Term k Integer -> Term k Integer
forall a (k :: TermKind). Num a => Term k a -> Term k a -> Term k a
Mul

intLit :: Integer -> Term k Integer
intLit :: forall (k :: TermKind). Integer -> Term k Integer
intLit = Integer -> Term k Integer
forall (k :: TermKind). Integer -> Term k Integer
IntLit (Integer -> Term k Integer)
-> (Integer -> Integer) -> Integer -> Term k Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Integer
forall a. Num a => Integer -> a
fromInteger

(.==.) :: (Typeable a, Eq a) => Term k a -> Term k a -> Term k Bool
.==. :: forall a (k :: TermKind).
(Typeable a, Eq a) =>
Term k a -> Term k a -> Term k Bool
(.==.) = Term k a -> Term k a -> Term k Bool
forall a (k :: TermKind).
(Typeable a, Eq a) =>
Term k a -> Term k a -> Term k Bool
Equals

(./=.) :: (Typeable a, Eq a) => Term k a -> Term k a -> Term k Bool
Term k a
x ./=. :: forall a (k :: TermKind).
(Typeable a, Eq a) =>
Term k a -> Term k a -> Term k Bool
./=. Term k a
y = Term k Bool -> Term k Bool
forall (k :: TermKind). Term k Bool -> Term k Bool
not' (Term k Bool -> Term k Bool) -> Term k Bool -> Term k Bool
forall a b. (a -> b) -> a -> b
$ Term k a
x Term k a -> Term k a -> Term k Bool
forall a (k :: TermKind).
(Typeable a, Eq a) =>
Term k a -> Term k a -> Term k Bool
.==. Term k a
y

(.>.) :: (Typeable a, Ord a) => Term k a -> Term k a -> Term k Bool
.>. :: forall a (k :: TermKind).
(Typeable a, Ord a) =>
Term k a -> Term k a -> Term k Bool
(.>.) = Term k a -> Term k a -> Term k Bool
forall a (k :: TermKind).
(Typeable a, Ord a) =>
Term k a -> Term k a -> Term k Bool
Gt

(.>=.) :: (Typeable a, Ord a) => Term k a -> Term k a -> Term k Bool

.>=. :: forall a (k :: TermKind).
(Typeable a, Ord a) =>
Term k a -> Term k a -> Term k Bool
(.>=.) = Term k a -> Term k a -> Term k Bool
forall a (k :: TermKind).
(Typeable a, Ord a) =>
Term k a -> Term k a -> Term k Bool
Ge

(.<.) :: (Typeable a, Ord a) => Term k a -> Term k a -> Term k Bool

.<. :: forall a (k :: TermKind).
(Typeable a, Ord a) =>
Term k a -> Term k a -> Term k Bool
(.<.) = Term k a -> Term k a -> Term k Bool
forall a (k :: TermKind).
(Typeable a, Ord a) =>
Term k a -> Term k a -> Term k Bool
Lt

(.<=.) :: (Typeable a, Ord a) => Term k a -> Term k a -> Term k Bool
.<=. :: forall a (k :: TermKind).
(Typeable a, Ord a) =>
Term k a -> Term k a -> Term k Bool
(.<=.) = Term k a -> Term k a -> Term k Bool
forall a (k :: TermKind).
(Typeable a, Ord a) =>
Term k a -> Term k a -> Term k Bool
Le

not' :: Term k Bool -> Term k Bool
not' :: forall (k :: TermKind). Term k Bool -> Term k Bool
not' = Term k Bool -> Term k Bool
forall (k :: TermKind). Term k Bool -> Term k Bool
Not

(.&&.) :: Term k Bool -> Term k Bool -> Term k Bool
Term k Bool
x .&&. :: forall (k :: TermKind). Term k Bool -> Term k Bool -> Term k Bool
.&&. (BoolLit Bool
True) = Term k Bool
x
BoolLit Bool
True .&&. Term k Bool
y  = Term k Bool
y
Term k Bool
x .&&. Term k Bool
y = Term k Bool -> Term k Bool -> Term k Bool
forall (k :: TermKind). Term k Bool -> Term k Bool -> Term k Bool
And Term k Bool
x Term k Bool
y

(.||.) :: Term k Bool -> Term k Bool -> Term k Bool
Term k Bool
x .||. :: forall (k :: TermKind). Term k Bool -> Term k Bool -> Term k Bool
.||. BoolLit Bool
False = Term k Bool
x
BoolLit Bool
False .||. Term k Bool
y  = Term k Bool
y
Term k Bool
x .||. Term k Bool
y = Term k Bool -> Term k Bool -> Term k Bool
forall (k :: TermKind). Term k Bool -> Term k Bool -> Term k Bool
Or Term k Bool
x Term k Bool
y

true :: Term k Bool
true :: forall (k :: TermKind). Term k Bool
true = Bool -> Term k Bool
forall (k :: TermKind). Bool -> Term k Bool
BoolLit Bool
True

false :: Term k Bool
false :: forall (k :: TermKind). Term k Bool
false = Bool -> Term k Bool
forall (k :: TermKind). Bool -> Term k Bool
BoolLit Bool
False

isIn :: (Typeable a, Eq a) => Term k a -> Term k [a] -> Term k Bool
isIn :: forall a (k :: TermKind).
(Typeable a, Eq a) =>
Term k a -> Term k [a] -> Term k Bool
isIn = Term k a -> Term k [a] -> Term k Bool
forall a (k :: TermKind).
(Typeable a, Eq a) =>
Term k a -> Term k [a] -> Term k Bool
IsIn

isNotIn :: (Typeable a, Eq a) => Term k a -> Term k [a] -> Term k Bool
isNotIn :: forall a (k :: TermKind).
(Typeable a, Eq a) =>
Term k a -> Term k [a] -> Term k Bool
isNotIn Term k a
x Term k [a]
xs = Term k Bool -> Term k Bool
forall (k :: TermKind). Term k Bool -> Term k Bool
not' (Term k a
x Term k a -> Term k [a] -> Term k Bool
forall a (k :: TermKind).
(Typeable a, Eq a) =>
Term k a -> Term k [a] -> Term k Bool
`isIn` Term k [a]
xs)

length' :: Typeable a => Term k [a] -> Term k Integer
length' :: forall a (k :: TermKind).
Typeable a =>
Term k [a] -> Term k Integer
length' = Term k [a] -> Term k Integer
forall a (k :: TermKind).
Typeable a =>
Term k [a] -> Term k Integer
Length

reverse' :: Typeable a => Term k [a] -> Term k [a]
reverse' :: forall a (k :: TermKind). Typeable a => Term k [a] -> Term k [a]
reverse' = Term k [a] -> Term k [a]
forall a (k :: TermKind). Typeable a => Term k [a] -> Term k [a]
Reverse

sum' :: Term k [Integer] -> Term k Integer
sum' :: forall (k :: TermKind). Term k [Integer] -> Term k Integer
sum' = Term k [Integer] -> Term k Integer
forall a (k :: TermKind). Num a => Term k [a] -> Term k a
Sum

product' :: Term k [Integer] -> Term k Integer
product' :: forall (k :: TermKind). Term k [Integer] -> Term k Integer
product' = Term k [Integer] -> Term k Integer
forall a (k :: TermKind). Num a => Term k [a] -> Term k a
Product

listLit :: (Show a, Typeable a) => [a] -> Term k [a]
listLit :: forall a (k :: TermKind). (Show a, Typeable a) => [a] -> Term k [a]
listLit = [a] -> Term k [a]
forall a (k :: TermKind). (Show a, Typeable a) => [a] -> Term k [a]
ListLit

embeddedLit :: (Embeddable a, Typeable a, Show a) => a -> Term k (Embedded a)
embeddedLit :: forall a (k :: TermKind).
(Embeddable a, Typeable a, Show a) =>
a -> Term k (Embedded a)
embeddedLit = a -> Term k (Embedded a)
forall a (k :: TermKind).
(Embeddable a, Typeable a, Show a) =>
a -> Term k (Embedded a)
EmbeddedLit

-- TODO: improve signature?
filter' :: (Integer -> Bool) -> Term k [Integer] -> Term 'PartiallyOpaque [Integer]
filter' :: forall (k :: TermKind).
(Integer -> Bool)
-> Term k [Integer] -> Term 'PartiallyOpaque [Integer]
filter' Integer -> Bool
p (Opaque Expr
x [[SomeVar]]
vs [SomeTerm 'Transparent]
ts) = Expr
-> [[SomeVar]]
-> [SomeTerm 'Transparent]
-> Term 'PartiallyOpaque [Integer]
forall a.
Expr
-> [[SomeVar]]
-> [SomeTerm 'Transparent]
-> Term 'PartiallyOpaque a
Opaque (String -> ([Integer] -> [Integer]) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"filter ?p" ((Integer -> Bool) -> [Integer] -> [Integer]
forall a. (a -> Bool) -> [a] -> [a]
filter Integer -> Bool
p) Expr -> Expr -> Expr
:$ Expr
x) [[SomeVar]]
vs [SomeTerm 'Transparent]
ts
filter' Integer -> Bool
p Term k [Integer]
x = Expr
-> [[SomeVar]]
-> [SomeTerm 'Transparent]
-> Term 'PartiallyOpaque [Integer]
forall a.
Expr
-> [[SomeVar]]
-> [SomeTerm 'Transparent]
-> Term 'PartiallyOpaque a
Opaque (String -> ([Integer] -> [Integer]) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"filter ?p" ((Integer -> Bool) -> [Integer] -> [Integer]
forall a. (a -> Bool) -> [a] -> [a]
filter Integer -> Bool
p) Expr -> Expr -> Expr
:$ Term k [Integer] -> Expr
forall a (k :: TermKind). Typeable a => Term k a -> Expr
toExpr Term k [Integer]
x) (Term k [Integer] -> [[SomeVar]]
forall a (k :: TermKind). Typeable a => Term k a -> [[SomeVar]]
termVarExps Term k [Integer]
x) (Term k [Integer] -> [SomeTerm 'Transparent]
forall a (k :: TermKind).
Typeable a =>
Term k a -> [SomeTerm 'Transparent]
transparentSubterms Term k [Integer]
x)

liftOpaqueValue :: Typeable a => (a, String) -> Term 'PartiallyOpaque a
liftOpaqueValue :: forall a. Typeable a => (a, String) -> Term 'PartiallyOpaque a
liftOpaqueValue (a
x,String
str) = Expr
-> [[SomeVar]]
-> [SomeTerm 'Transparent]
-> Term 'PartiallyOpaque a
forall a.
Expr
-> [[SomeVar]]
-> [SomeTerm 'Transparent]
-> Term 'PartiallyOpaque a
Opaque (String -> a -> Expr
forall a. Typeable a => String -> a -> Expr
value String
str a
x) [] []

liftOpaque :: (Typeable a, Typeable b) => (a -> b, String) -> Term k a -> Term 'PartiallyOpaque b
liftOpaque :: forall a b (k :: TermKind).
(Typeable a, Typeable b) =>
(a -> b, String) -> Term k a -> Term 'PartiallyOpaque b
liftOpaque (a -> b
f,String
str) (Opaque Expr
x [[SomeVar]]
vs [SomeTerm 'Transparent]
ts) = Expr
-> [[SomeVar]]
-> [SomeTerm 'Transparent]
-> Term 'PartiallyOpaque b
forall a.
Expr
-> [[SomeVar]]
-> [SomeTerm 'Transparent]
-> Term 'PartiallyOpaque a
Opaque (String -> (a -> b) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
str a -> b
f Expr -> Expr -> Expr
:$ Expr
x) [[SomeVar]]
vs [SomeTerm 'Transparent]
ts
liftOpaque (a -> b
f,String
str) Term k a
x = Expr
-> [[SomeVar]]
-> [SomeTerm 'Transparent]
-> Term 'PartiallyOpaque b
forall a.
Expr
-> [[SomeVar]]
-> [SomeTerm 'Transparent]
-> Term 'PartiallyOpaque a
Opaque (String -> (a -> b) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
str a -> b
f Expr -> Expr -> Expr
:$ Term k a -> Expr
forall a (k :: TermKind). Typeable a => Term k a -> Expr
toExpr Term k a
x) (Term k a -> [[SomeVar]]
forall a (k :: TermKind). Typeable a => Term k a -> [[SomeVar]]
termVarExps Term k a
x) (Term k a -> [SomeTerm 'Transparent]
forall a (k :: TermKind).
Typeable a =>
Term k a -> [SomeTerm 'Transparent]
transparentSubterms Term k a
x)

liftOpaque2 :: (Typeable a, Typeable b, Typeable c) => (a -> b -> c, String) -> Term k a -> Term k b -> Term 'PartiallyOpaque c
liftOpaque2 :: forall a b c (k :: TermKind).
(Typeable a, Typeable b, Typeable c) =>
(a -> b -> c, String)
-> Term k a -> Term k b -> Term 'PartiallyOpaque c
liftOpaque2 (a -> b -> c
f,String
str) (Opaque Expr
x [[SomeVar]]
vx [SomeTerm 'Transparent]
tx) (Opaque Expr
y [[SomeVar]]
vy [SomeTerm 'Transparent]
ty) = Expr
-> [[SomeVar]]
-> [SomeTerm 'Transparent]
-> Term 'PartiallyOpaque c
forall a.
Expr
-> [[SomeVar]]
-> [SomeTerm 'Transparent]
-> Term 'PartiallyOpaque a
Opaque (String -> (a -> b -> c) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
str a -> b -> c
f Expr -> Expr -> Expr
:$ Expr
x Expr -> Expr -> Expr
:$ Expr
y) ([[SomeVar]]
vx [[SomeVar]] -> [[SomeVar]] -> [[SomeVar]]
forall a. [a] -> [a] -> [a]
++ [[SomeVar]]
vy) ([SomeTerm 'Transparent]
tx [SomeTerm 'Transparent]
-> [SomeTerm 'Transparent] -> [SomeTerm 'Transparent]
forall a. [a] -> [a] -> [a]
++ [SomeTerm 'Transparent]
ty)
liftOpaque2 (a -> b -> c
f,String
str) (Opaque Expr
x [[SomeVar]]
vx [SomeTerm 'Transparent]
tx) Term k b
y = Expr
-> [[SomeVar]]
-> [SomeTerm 'Transparent]
-> Term 'PartiallyOpaque c
forall a.
Expr
-> [[SomeVar]]
-> [SomeTerm 'Transparent]
-> Term 'PartiallyOpaque a
Opaque (String -> (a -> b -> c) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
str a -> b -> c
f Expr -> Expr -> Expr
:$ Expr
x Expr -> Expr -> Expr
:$ Term k b -> Expr
forall a (k :: TermKind). Typeable a => Term k a -> Expr
toExpr Term k b
y) ([[SomeVar]]
vx [[SomeVar]] -> [[SomeVar]] -> [[SomeVar]]
forall a. [a] -> [a] -> [a]
++ Term k b -> [[SomeVar]]
forall a (k :: TermKind). Typeable a => Term k a -> [[SomeVar]]
termVarExps Term k b
y) ([SomeTerm 'Transparent]
tx [SomeTerm 'Transparent]
-> [SomeTerm 'Transparent] -> [SomeTerm 'Transparent]
forall a. [a] -> [a] -> [a]
++ Term k b -> [SomeTerm 'Transparent]
forall a (k :: TermKind).
Typeable a =>
Term k a -> [SomeTerm 'Transparent]
transparentSubterms Term k b
y)
liftOpaque2 (a -> b -> c
f,String
str) Term k a
x (Opaque Expr
y [[SomeVar]]
vy [SomeTerm 'Transparent]
ty) = Expr
-> [[SomeVar]]
-> [SomeTerm 'Transparent]
-> Term 'PartiallyOpaque c
forall a.
Expr
-> [[SomeVar]]
-> [SomeTerm 'Transparent]
-> Term 'PartiallyOpaque a
Opaque (String -> (a -> b -> c) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
str a -> b -> c
f Expr -> Expr -> Expr
:$ Term k a -> Expr
forall a (k :: TermKind). Typeable a => Term k a -> Expr
toExpr Term k a
x Expr -> Expr -> Expr
:$ Expr
y) (Term k a -> [[SomeVar]]
forall a (k :: TermKind). Typeable a => Term k a -> [[SomeVar]]
termVarExps Term k a
x [[SomeVar]] -> [[SomeVar]] -> [[SomeVar]]
forall a. [a] -> [a] -> [a]
++ [[SomeVar]]
vy) (Term k a -> [SomeTerm 'Transparent]
forall a (k :: TermKind).
Typeable a =>
Term k a -> [SomeTerm 'Transparent]
transparentSubterms Term k a
x [SomeTerm 'Transparent]
-> [SomeTerm 'Transparent] -> [SomeTerm 'Transparent]
forall a. [a] -> [a] -> [a]
++ [SomeTerm 'Transparent]
ty)
liftOpaque2 (a -> b -> c
f,String
str) Term k a
x Term k b
y = Expr
-> [[SomeVar]]
-> [SomeTerm 'Transparent]
-> Term 'PartiallyOpaque c
forall a.
Expr
-> [[SomeVar]]
-> [SomeTerm 'Transparent]
-> Term 'PartiallyOpaque a
Opaque (String -> (a -> b -> c) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
str a -> b -> c
f Expr -> Expr -> Expr
:$ Term k a -> Expr
forall a (k :: TermKind). Typeable a => Term k a -> Expr
toExpr Term k a
x Expr -> Expr -> Expr
:$ Term k b -> Expr
forall a (k :: TermKind). Typeable a => Term k a -> Expr
toExpr Term k b
y) (Term k a -> [[SomeVar]]
forall a (k :: TermKind). Typeable a => Term k a -> [[SomeVar]]
termVarExps Term k a
x [[SomeVar]] -> [[SomeVar]] -> [[SomeVar]]
forall a. [a] -> [a] -> [a]
++ Term k b -> [[SomeVar]]
forall a (k :: TermKind). Typeable a => Term k a -> [[SomeVar]]
termVarExps Term k b
y) (Term k a -> [SomeTerm 'Transparent]
forall a (k :: TermKind).
Typeable a =>
Term k a -> [SomeTerm 'Transparent]
transparentSubterms Term k a
x [SomeTerm 'Transparent]
-> [SomeTerm 'Transparent] -> [SomeTerm 'Transparent]
forall a. [a] -> [a] -> [a]
++ Term k b -> [SomeTerm 'Transparent]
forall a (k :: TermKind).
Typeable a =>
Term k a -> [SomeTerm 'Transparent]
transparentSubterms Term k b
y)