{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilyDependencies #-}
module Test.IOTasks.Internal.Term (
  Term(..),
  TermKind(..),
  oEval,
  evalI, evalIs,
  showResult,
  termVarExps, transparentSubterms,
  toExpr,
  showTerm, showIndexedTerm,
  SomeTerm(..), withSomeTerm,
  SomeTermK(..), withSomeTermK,
  castTerm,
  compareK,
  ) where

import Data.Express (Expr((:$)), var, val, value, (//-), evl, vars, isVar, showExpr)
import Data.Function (on)
import Data.Kind (Type)
import Data.List ( nub, intercalate, sortBy, intercalate )
import Data.List.Extra (maximumOn)
import Data.Map (Map)
import qualified Data.Map as Map (lookup)
import Data.Maybe ( fromMaybe, mapMaybe, maybeToList )

import Control.Applicative (liftA2) -- not redundant for base-4.17.x.x and below!

import Test.IOTasks.Internal.Overflow
import Test.IOTasks.ValueMap as ValueMap
import Test.IOTasks.Var

import Text.Parsec (parse, char, many1, alphaNum, sepBy1, (<|>), string, digit)
import Text.Parsec.String (Parser)

import Type.Match
import Type.Reflection

data TermKind = Transparent | PartiallyOpaque

data Term (k :: TermKind) a where
  Add :: Num a => Term k a -> Term k a -> Term k a
  Sub :: Num a => Term k a -> Term k a -> Term k a
  Mul :: Num a => Term k a -> Term k a -> Term k a
  Equals :: (Typeable a, Eq a) => Term k a -> Term k a -> Term k Bool
  Gt :: (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
  Lt :: (Typeable a, Ord a) => Term k a -> Term k a -> Term k Bool
  Le :: (Typeable a, Ord a) => Term k a -> Term k a -> Term k Bool
  And :: Term k Bool -> Term k Bool -> Term k Bool
  Or :: Term k Bool -> Term k Bool -> Term k Bool
  IsIn :: (Typeable a, Eq a) => Term k a -> Term k [a] -> Term k Bool
  Not :: Term k Bool -> Term k Bool
  Sum :: Num a => Term k [a] -> Term k a
  Product :: Num a => Term k [a] -> Term k a
  Length :: Typeable a => Term k [a] -> Term k Integer
  Reverse :: Typeable a => Term k [a] -> Term k [a]
  IntLit :: Integer -> Term k Integer
  ListLit :: (Show a, Typeable a) => [a] -> Term k [a]
  EmbeddedLit :: (Embeddable a, Typeable a, Show a) => a -> Term k (Embedded a)
  BoolLit :: Bool -> Term k Bool
  Current :: VarExp e => e a -> Int -> Term k a
  All :: (Typeable a, VarExp e) => e a -> Int -> Term k [a]

  Opaque :: Expr -> [[SomeVar]] -> [SomeTerm 'Transparent] -> Term 'PartiallyOpaque a

termVarExps :: Typeable a => Term k a -> [[SomeVar]]
termVarExps :: forall a (k :: TermKind). Typeable a => Term k a -> [[SomeVar]]
termVarExps (Add Term k a
x Term k a
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 a -> [[SomeVar]]
forall a (k :: TermKind). Typeable a => Term k a -> [[SomeVar]]
termVarExps Term k a
y
termVarExps (Sub Term k a
x Term k a
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 a -> [[SomeVar]]
forall a (k :: TermKind). Typeable a => Term k a -> [[SomeVar]]
termVarExps Term k a
y
termVarExps (Mul Term k a
x Term k a
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 a -> [[SomeVar]]
forall a (k :: TermKind). Typeable a => Term k a -> [[SomeVar]]
termVarExps Term k a
y
termVarExps (Equals Term k a
x Term k a
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 a -> [[SomeVar]]
forall a (k :: TermKind). Typeable a => Term k a -> [[SomeVar]]
termVarExps Term k a
y
termVarExps (Gt Term k a
x Term k a
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 a -> [[SomeVar]]
forall a (k :: TermKind). Typeable a => Term k a -> [[SomeVar]]
termVarExps Term k a
y
termVarExps (Ge Term k a
x Term k a
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 a -> [[SomeVar]]
forall a (k :: TermKind). Typeable a => Term k a -> [[SomeVar]]
termVarExps Term k a
y
termVarExps (Lt Term k a
x Term k a
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 a -> [[SomeVar]]
forall a (k :: TermKind). Typeable a => Term k a -> [[SomeVar]]
termVarExps Term k a
y
termVarExps (Le Term k a
x Term k a
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 a -> [[SomeVar]]
forall a (k :: TermKind). Typeable a => Term k a -> [[SomeVar]]
termVarExps Term k a
y
termVarExps (And Term k Bool
x Term k Bool
y) = Term k Bool -> [[SomeVar]]
forall a (k :: TermKind). Typeable a => Term k a -> [[SomeVar]]
termVarExps Term k Bool
x [[SomeVar]] -> [[SomeVar]] -> [[SomeVar]]
forall a. [a] -> [a] -> [a]
++ Term k Bool -> [[SomeVar]]
forall a (k :: TermKind). Typeable a => Term k a -> [[SomeVar]]
termVarExps Term k Bool
y
termVarExps (Or Term k Bool
x Term k Bool
y) = Term k Bool -> [[SomeVar]]
forall a (k :: TermKind). Typeable a => Term k a -> [[SomeVar]]
termVarExps Term k Bool
x [[SomeVar]] -> [[SomeVar]] -> [[SomeVar]]
forall a. [a] -> [a] -> [a]
++ Term k Bool -> [[SomeVar]]
forall a (k :: TermKind). Typeable a => Term k a -> [[SomeVar]]
termVarExps Term k Bool
y
termVarExps (IsIn Term k a
x Term k [a]
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 [a] -> [[SomeVar]]
forall a (k :: TermKind). Typeable a => Term k a -> [[SomeVar]]
termVarExps Term k [a]
y
termVarExps (Sum Term k [a]
x) = Term k [a] -> [[SomeVar]]
forall a (k :: TermKind). Typeable a => Term k a -> [[SomeVar]]
termVarExps Term k [a]
x
termVarExps (Product Term k [a]
x) = Term k [a] -> [[SomeVar]]
forall a (k :: TermKind). Typeable a => Term k a -> [[SomeVar]]
termVarExps Term k [a]
x
termVarExps (Length Term k [a]
x) = Term k [a] -> [[SomeVar]]
forall a (k :: TermKind). Typeable a => Term k a -> [[SomeVar]]
termVarExps Term k [a]
x
termVarExps (Reverse Term k [a]
x) = Term k [a] -> [[SomeVar]]
forall a (k :: TermKind). Typeable a => Term k a -> [[SomeVar]]
termVarExps Term k [a]
x
termVarExps (Not Term k Bool
x) = Term k Bool -> [[SomeVar]]
forall a (k :: TermKind). Typeable a => Term k a -> [[SomeVar]]
termVarExps Term k Bool
x
termVarExps (IntLit Integer
_) = []
termVarExps (ListLit [a]
_) = []
termVarExps (EmbeddedLit a
_) = []
termVarExps (BoolLit Bool
_) = []
termVarExps (Current e a
e Int
_) = [(Var a -> SomeVar) -> [Var a] -> [SomeVar]
forall a b. (a -> b) -> [a] -> [b]
map Var a -> SomeVar
forall a. Typeable a => Var a -> SomeVar
someVar ([Var a] -> [SomeVar]) -> [Var a] -> [SomeVar]
forall a b. (a -> b) -> a -> b
$ e a -> [Var a]
forall a. e a -> [Var a]
forall (e :: * -> *) a. VarExp e => e a -> [Var a]
toVarList e a
e]
termVarExps (All e a
e Int
_) = [(Var a -> SomeVar) -> [Var a] -> [SomeVar]
forall a b. (a -> b) -> [a] -> [b]
map Var a -> SomeVar
forall a. Typeable a => Var a -> SomeVar
someVar ([Var a] -> [SomeVar]) -> [Var a] -> [SomeVar]
forall a b. (a -> b) -> a -> b
$ e a -> [Var a]
forall a. e a -> [Var a]
forall (e :: * -> *) a. VarExp e => e a -> [Var a]
toVarList e a
e]
termVarExps (Opaque Expr
_ [[SomeVar]]
vars [SomeTerm 'Transparent]
_) = [[SomeVar]]
vars

instance EffectEval (Term k) where
  type Env (Term k) = ValueMap
  pureEval :: forall (f :: * -> *) a.
(Applicative f, Typeable a) =>
(forall x. Typeable x => Term k x -> f x)
-> Env (Term k) -> Term k a -> f a
pureEval forall x. Typeable x => Term k x -> f x
f Env (Term k)
_ (Add Term k a
x Term k a
y) = (a -> a -> a) -> f a -> f a -> f a
forall a b c. (a -> b -> c) -> f a -> f b -> f c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> a -> a
forall a. Num a => a -> a -> a
(+) (Term k a -> f a
forall x. Typeable x => Term k x -> f x
f Term k a
x) (Term k a -> f a
forall x. Typeable x => Term k x -> f x
f Term k a
y)
  pureEval forall x. Typeable x => Term k x -> f x
f Env (Term k)
_ (Sub Term k a
x Term k a
y) = (a -> a -> a) -> f a -> f a -> f a
forall a b c. (a -> b -> c) -> f a -> f b -> f c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (-) (Term k a -> f a
forall x. Typeable x => Term k x -> f x
f Term k a
x) (Term k a -> f a
forall x. Typeable x => Term k x -> f x
f Term k a
y)
  pureEval forall x. Typeable x => Term k x -> f x
f Env (Term k)
_ (Mul Term k a
x Term k a
y) = (a -> a -> a) -> f a -> f a -> f a
forall a b c. (a -> b -> c) -> f a -> f b -> f c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> a -> a
forall a. Num a => a -> a -> a
(*) (Term k a -> f a
forall x. Typeable x => Term k x -> f x
f Term k a
x) (Term k a -> f a
forall x. Typeable x => Term k x -> f x
f Term k a
y)
  pureEval forall x. Typeable x => Term k x -> f x
f Env (Term k)
_ (Equals Term k a
x Term k a
y) = (a -> a -> a) -> f a -> f a -> f a
forall a b c. (a -> b -> c) -> f a -> f b -> f c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> a -> a
a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Term k a -> f a
forall x. Typeable x => Term k x -> f x
f Term k a
x) (Term k a -> f a
forall x. Typeable x => Term k x -> f x
f Term k a
y)
  pureEval forall x. Typeable x => Term k x -> f x
f Env (Term k)
_ (Gt Term k a
x Term k a
y) = (a -> a -> a) -> f a -> f a -> f a
forall a b c. (a -> b -> c) -> f a -> f b -> f c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> a -> a
a -> a -> Bool
forall a. Ord a => a -> a -> Bool
(>) (Term k a -> f a
forall x. Typeable x => Term k x -> f x
f Term k a
x) (Term k a -> f a
forall x. Typeable x => Term k x -> f x
f Term k a
y)
  pureEval forall x. Typeable x => Term k x -> f x
f Env (Term k)
_ (Ge Term k a
x Term k a
y) = (a -> a -> a) -> f a -> f a -> f a
forall a b c. (a -> b -> c) -> f a -> f b -> f c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> a -> a
a -> a -> Bool
forall a. Ord a => a -> a -> Bool
(>=) (Term k a -> f a
forall x. Typeable x => Term k x -> f x
f Term k a
x) (Term k a -> f a
forall x. Typeable x => Term k x -> f x
f Term k a
y)
  pureEval forall x. Typeable x => Term k x -> f x
f Env (Term k)
_ (Lt Term k a
x Term k a
y) = (a -> a -> a) -> f a -> f a -> f a
forall a b c. (a -> b -> c) -> f a -> f b -> f c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> a -> a
a -> a -> Bool
forall a. Ord a => a -> a -> Bool
(<) (Term k a -> f a
forall x. Typeable x => Term k x -> f x
f Term k a
x) (Term k a -> f a
forall x. Typeable x => Term k x -> f x
f Term k a
y)
  pureEval forall x. Typeable x => Term k x -> f x
f Env (Term k)
_ (Le Term k a
x Term k a
y) = (a -> a -> a) -> f a -> f a -> f a
forall a b c. (a -> b -> c) -> f a -> f b -> f c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> a -> a
a -> a -> Bool
forall a. Ord a => a -> a -> Bool
(<=) (Term k a -> f a
forall x. Typeable x => Term k x -> f x
f Term k a
x) (Term k a -> f a
forall x. Typeable x => Term k x -> f x
f Term k a
y)
  pureEval forall x. Typeable x => Term k x -> f x
f Env (Term k)
_ (And Term k Bool
x Term k Bool
y) = (Bool -> Bool -> a) -> f Bool -> f Bool -> f a
forall a b c. (a -> b -> c) -> f a -> f b -> f c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bool -> Bool -> a
Bool -> Bool -> Bool
(&&) (Term k Bool -> f Bool
forall x. Typeable x => Term k x -> f x
f Term k Bool
x) (Term k Bool -> f Bool
forall x. Typeable x => Term k x -> f x
f Term k Bool
y)
  pureEval forall x. Typeable x => Term k x -> f x
f Env (Term k)
_ (Or Term k Bool
x Term k Bool
y) = (Bool -> Bool -> a) -> f Bool -> f Bool -> f a
forall a b c. (a -> b -> c) -> f a -> f b -> f c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Bool -> Bool -> a
Bool -> Bool -> Bool
(||) (Term k Bool -> f Bool
forall x. Typeable x => Term k x -> f x
f Term k Bool
x) (Term k Bool -> f Bool
forall x. Typeable x => Term k x -> f x
f Term k Bool
y)
  pureEval forall x. Typeable x => Term k x -> f x
f Env (Term k)
_ (IsIn Term k a
x Term k [a]
xs) = (a -> [a] -> a) -> f a -> f [a] -> f a
forall a b c. (a -> b -> c) -> f a -> f b -> f c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 a -> [a] -> a
a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem (Term k a -> f a
forall x. Typeable x => Term k x -> f x
f Term k a
x) (Term k [a] -> f [a]
forall x. Typeable x => Term k x -> f x
f Term k [a]
xs)
  pureEval forall x. Typeable x => Term k x -> f x
f Env (Term k)
_ (Not Term k Bool
x) = Bool -> a
Bool -> Bool
not (Bool -> a) -> f Bool -> f a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k Bool -> f Bool
forall x. Typeable x => Term k x -> f x
f Term k Bool
x
  pureEval forall x. Typeable x => Term k x -> f x
f Env (Term k)
_ (Sum Term k [a]
xs) = [a] -> a
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([a] -> a) -> f [a] -> f a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k [a] -> f [a]
forall x. Typeable x => Term k x -> f x
f Term k [a]
xs
  pureEval forall x. Typeable x => Term k x -> f x
f Env (Term k)
_ (Product Term k [a]
xs) = [a] -> a
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product ([a] -> a) -> f [a] -> f a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k [a] -> f [a]
forall x. Typeable x => Term k x -> f x
f Term k [a]
xs
  pureEval forall x. Typeable x => Term k x -> f x
f Env (Term k)
_ (Length Term k [a]
xs) = Int -> a
Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> a) -> ([a] -> Int) -> [a] -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([a] -> a) -> f [a] -> f a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k [a] -> f [a]
forall x. Typeable x => Term k x -> f x
f Term k [a]
xs
  pureEval forall x. Typeable x => Term k x -> f x
f Env (Term k)
_ (Reverse Term k [a]
xs) = [a] -> a
[a] -> [a]
forall a. [a] -> [a]
reverse ([a] -> a) -> f [a] -> f a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k [a] -> f [a]
forall x. Typeable x => Term k x -> f x
f Term k [a]
xs
  pureEval forall x. Typeable x => Term k x -> f x
_ Env (Term k)
_ (IntLit Integer
x) = a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
Integer
x
  pureEval forall x. Typeable x => Term k x -> f x
_ Env (Term k)
_ (ListLit [a]
xs) = a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
[a]
xs
  pureEval forall x. Typeable x => Term k x -> f x
_ Env (Term k)
_ (EmbeddedLit a
x) = a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Integer -> Embedded a
forall a. (Show a, Embeddable a) => Integer -> Embedded a
Embedded (Integer -> Embedded a) -> Integer -> Embedded a
forall a b. (a -> b) -> a -> b
$ a -> Integer
forall a. Embeddable a => a -> Integer
asInteger a
x)
  pureEval forall x. Typeable x => Term k x -> f x
_ Env (Term k)
_ (BoolLit Bool
x) = a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
Bool
x
  pureEval forall x. Typeable x => Term k x -> f x
_ Env (Term k)
e (Current e a
x Int
n) = a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> f a) -> a -> f a
forall a b. (a -> b) -> a -> b
$ a -> Maybe a -> a
forall a. a -> Maybe a -> a
fromMaybe (String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$ String
"empty list for {" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ((Var a -> String) -> [Var a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Var a -> String
forall a. Var a -> String
varname ([Var a] -> [String]) -> [Var a] -> [String]
forall a b. (a -> b) -> a -> b
$ e a -> [Var a]
forall a. e a -> [Var a]
forall (e :: * -> *) a. VarExp e => e a -> [Var a]
toVarList e a
x) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}") (Maybe a -> a) -> ([a] -> Maybe a) -> [a] -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Maybe a
forall a. [a] -> Maybe a
safeHead ([a] -> a) -> [a] -> a
forall a b. (a -> b) -> a -> b
$ e a -> Int -> ValueMap -> [a]
forall a (e :: * -> *).
(Typeable a, VarExp e) =>
e a -> Int -> ValueMap -> [a]
primEvalVar e a
x Int
n Env (Term k)
ValueMap
e
  pureEval forall x. Typeable x => Term k x -> f x
_ Env (Term k)
e (All e a
x Int
n) = a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> f a) -> a -> f a
forall a b. (a -> b) -> a -> b
$ [a] -> [a]
forall a. [a] -> [a]
reverse ([a] -> [a]) -> [a] -> [a]
forall a b. (a -> b) -> a -> b
$ e a -> Int -> ValueMap -> [a]
forall a (e :: * -> *).
(Typeable a, VarExp e) =>
e a -> Int -> ValueMap -> [a]
primEvalVar e a
x Int
n Env (Term k)
ValueMap
e
  pureEval forall x. Typeable x => Term k x -> f x
_ Env (Term k)
e (Opaque Expr
expr [[SomeVar]]
vss [SomeTerm 'Transparent]
_) = a -> f a
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (a -> f a) -> a -> f a
forall a b. (a -> b) -> a -> b
$ Expr -> [[SomeVar]] -> ValueMap -> a
forall a. Typeable a => Expr -> [[SomeVar]] -> ValueMap -> a
eval' Expr
expr [[SomeVar]]
vss Env (Term k)
ValueMap
e

oEval :: Typeable a => ValueMap -> Term k a -> (OverflowWarning, a)
oEval :: forall a (k :: TermKind).
Typeable a =>
ValueMap -> Term k a -> (OverflowWarning, a)
oEval = OverflowTreatment (Term k)
-> Env (Term k) -> Term k a -> (OverflowWarning, a)
forall (t :: * -> *) a.
(EffectEval t, Typeable a) =>
OverflowTreatment t -> Env t -> t a -> (OverflowWarning, a)
evalOverflow ((Env (Term k) -> Term k Integer -> Either (SubCheck (Term k) I) I)
-> (Env (Term k)
    -> Term k [Integer] -> Either (SubCheck (Term k) [I]) [I])
-> OverflowTreatment (Term k)
forall (t :: * -> *).
(Env t -> t Integer -> Either (SubCheck t I) I)
-> (Env t -> t [Integer] -> Either (SubCheck t [I]) [I])
-> OverflowTreatment t
OverflowTreatment Env (Term k) -> Term k Integer -> Either (SubCheck (Term k) I) I
ValueMap -> Term k Integer -> Either (SubCheck (Term k) I) I
forall (k :: TermKind).
ValueMap -> Term k Integer -> Either (SubCheck (Term k) I) I
evalI (\Env (Term k)
d -> [I] -> Either (SubCheck (Term k) [I]) [I]
forall a b. b -> Either a b
Right ([I] -> Either (SubCheck (Term k) [I]) [I])
-> (Term k [Integer] -> [I])
-> Term k [Integer]
-> Either (SubCheck (Term k) [I]) [I]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValueMap -> Term k [Integer] -> [I]
forall (k :: TermKind). ValueMap -> Term k [Integer] -> [I]
evalIs Env (Term k)
ValueMap
d))

evalI :: ValueMap -> Term k Integer -> Either (SubCheck (Term k) I) I
evalI :: forall (k :: TermKind).
ValueMap -> Term k Integer -> Either (SubCheck (Term k) I) I
evalI ValueMap
e (Add Term k Integer
x Term k Integer
y) = (I -> I -> I)
-> Either (SubCheck (Term k) I) I
-> Either (SubCheck (Term k) I) I
-> Either (SubCheck (Term k) I) I
forall a b c.
(a -> b -> c)
-> Either (SubCheck (Term k) I) a
-> Either (SubCheck (Term k) I) b
-> Either (SubCheck (Term k) I) c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 I -> I -> I
forall a. Num a => a -> a -> a
(+) (ValueMap -> Term k Integer -> Either (SubCheck (Term k) I) I
forall (k :: TermKind).
ValueMap -> Term k Integer -> Either (SubCheck (Term k) I) I
evalI ValueMap
e Term k Integer
x) (ValueMap -> Term k Integer -> Either (SubCheck (Term k) I) I
forall (k :: TermKind).
ValueMap -> Term k Integer -> Either (SubCheck (Term k) I) I
evalI ValueMap
e Term k Integer
y)
evalI ValueMap
e (Sub Term k Integer
x Term k Integer
y) = (I -> I -> I)
-> Either (SubCheck (Term k) I) I
-> Either (SubCheck (Term k) I) I
-> Either (SubCheck (Term k) I) I
forall a b c.
(a -> b -> c)
-> Either (SubCheck (Term k) I) a
-> Either (SubCheck (Term k) I) b
-> Either (SubCheck (Term k) I) c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 (-) (ValueMap -> Term k Integer -> Either (SubCheck (Term k) I) I
forall (k :: TermKind).
ValueMap -> Term k Integer -> Either (SubCheck (Term k) I) I
evalI ValueMap
e Term k Integer
x) (ValueMap -> Term k Integer -> Either (SubCheck (Term k) I) I
forall (k :: TermKind).
ValueMap -> Term k Integer -> Either (SubCheck (Term k) I) I
evalI ValueMap
e Term k Integer
y)
evalI ValueMap
e (Mul Term k Integer
x Term k Integer
y) = (I -> I -> I)
-> Either (SubCheck (Term k) I) I
-> Either (SubCheck (Term k) I) I
-> Either (SubCheck (Term k) I) I
forall a b c.
(a -> b -> c)
-> Either (SubCheck (Term k) I) a
-> Either (SubCheck (Term k) I) b
-> Either (SubCheck (Term k) I) c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 I -> I -> I
forall a. Num a => a -> a -> a
(*) (ValueMap -> Term k Integer -> Either (SubCheck (Term k) I) I
forall (k :: TermKind).
ValueMap -> Term k Integer -> Either (SubCheck (Term k) I) I
evalI ValueMap
e Term k Integer
x) (ValueMap -> Term k Integer -> Either (SubCheck (Term k) I) I
forall (k :: TermKind).
ValueMap -> Term k Integer -> Either (SubCheck (Term k) I) I
evalI ValueMap
e Term k Integer
y)
evalI ValueMap
e (Sum Term k [Integer]
xs) = I -> Either (SubCheck (Term k) I) I
forall a b. b -> Either a b
Right (I -> Either (SubCheck (Term k) I) I)
-> I -> Either (SubCheck (Term k) I) I
forall a b. (a -> b) -> a -> b
$ [I] -> I
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([I] -> I) -> [I] -> I
forall a b. (a -> b) -> a -> b
$ ValueMap -> Term k [Integer] -> [I]
forall (k :: TermKind). ValueMap -> Term k [Integer] -> [I]
evalIs ValueMap
e Term k [Integer]
xs
evalI ValueMap
e (Product Term k [Integer]
xs) = I -> Either (SubCheck (Term k) I) I
forall a b. b -> Either a b
Right (I -> Either (SubCheck (Term k) I) I)
-> I -> Either (SubCheck (Term k) I) I
forall a b. (a -> b) -> a -> b
$ [I] -> I
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product ([I] -> I) -> [I] -> I
forall a b. (a -> b) -> a -> b
$ ValueMap -> Term k [Integer] -> [I]
forall (k :: TermKind). ValueMap -> Term k [Integer] -> [I]
evalIs ValueMap
e Term k [Integer]
xs
evalI ValueMap
e (Length (Term k [a]
xs :: Term k [a])) =
  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) -> Either (SubCheck (Term k) I) I)
 -> Case a (Either (SubCheck (Term k) I) I))
-> ((Integer :~~: a) -> Either (SubCheck (Term k) I) I)
-> Case a (Either (SubCheck (Term k) I) I)
forall a b. (a -> b) -> a -> b
$ \Integer :~~: a
HRefl -> I -> Either (SubCheck (Term k) I) I
forall a b. b -> Either a b
Right (I -> Either (SubCheck (Term k) I) I)
-> ([I] -> I) -> [I] -> Either (SubCheck (Term k) I) I
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> I
fromInt (Int -> I) -> ([I] -> Int) -> [I] -> I
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [I] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([I] -> Either (SubCheck (Term k) I) I)
-> [I] -> Either (SubCheck (Term k) I) I
forall a b. (a -> b) -> a -> b
$ ValueMap -> Term k [Integer] -> [I]
forall (k :: TermKind). ValueMap -> Term k [Integer] -> [I]
evalIs ValueMap
e Term k [a]
Term k [Integer]
xs
    , Either (SubCheck (Term k) I) I
-> Case a (Either (SubCheck (Term k) I) I)
forall {k} r (x :: k). r -> Case x r
fallbackCase' (Either (SubCheck (Term k) I) I
 -> Case a (Either (SubCheck (Term k) I) I))
-> Either (SubCheck (Term k) I) I
-> Case a (Either (SubCheck (Term k) I) I)
forall a b. (a -> b) -> a -> b
$ SubCheck (Term k) I -> Either (SubCheck (Term k) I) I
forall a b. a -> Either a b
Left (SubCheck (Term k) I -> Either (SubCheck (Term k) I) I)
-> SubCheck (Term k) I -> Either (SubCheck (Term k) I) I
forall a b. (a -> b) -> a -> b
$ Term k [a] -> ([a] -> I) -> SubCheck (Term k) I
forall a (t :: * -> *) x.
Typeable a =>
t a -> (a -> x) -> SubCheck t x
SubCheck Term k [a]
xs (Int -> I
fromInt (Int -> I) -> ([a] -> Int) -> [a] -> I
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length)
    ]
evalI ValueMap
_ (IntLit Integer
x) = I -> Either (SubCheck (Term k) I) I
forall a b. b -> Either a b
Right (I -> Either (SubCheck (Term k) I) I)
-> I -> Either (SubCheck (Term k) I) I
forall a b. (a -> b) -> a -> b
$ Integer -> I
forall a. Num a => Integer -> a
fromInteger Integer
x
evalI ValueMap
e (Current e Integer
x Int
n) = I -> Either (SubCheck (Term k) I) I
forall a b. b -> Either a b
Right (I -> Either (SubCheck (Term k) I) I)
-> I -> Either (SubCheck (Term k) I) I
forall a b. (a -> b) -> a -> b
$ Integer -> I
forall a. Num a => Integer -> a
fromInteger (Integer -> I) -> Integer -> I
forall a b. (a -> b) -> a -> b
$ Integer -> Maybe Integer -> Integer
forall a. a -> Maybe a -> a
fromMaybe (String -> Integer
forall a. HasCallStack => String -> a
error (String -> Integer) -> String -> Integer
forall a b. (a -> b) -> a -> b
$ String
"empty list for {" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ((Var Integer -> String) -> [Var Integer] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Var Integer -> String
forall a. Var a -> String
varname ([Var Integer] -> [String]) -> [Var Integer] -> [String]
forall a b. (a -> b) -> a -> b
$ e Integer -> [Var Integer]
forall a. e a -> [Var a]
forall (e :: * -> *) a. VarExp e => e a -> [Var a]
toVarList e Integer
x) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}") (Maybe Integer -> Integer)
-> ([Integer] -> Maybe Integer) -> [Integer] -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Integer] -> Maybe Integer
forall a. [a] -> Maybe a
safeHead ([Integer] -> Integer) -> [Integer] -> Integer
forall a b. (a -> b) -> a -> b
$ e Integer -> Int -> ValueMap -> [Integer]
forall a (e :: * -> *).
(Typeable a, VarExp e) =>
e a -> Int -> ValueMap -> [a]
primEvalVar e Integer
x Int
n ValueMap
e
evalI ValueMap
e (Opaque Expr
expr [[SomeVar]]
vss [SomeTerm 'Transparent]
_) = I -> Either (SubCheck (Term k) I) I
forall a b. b -> Either a b
Right (I -> Either (SubCheck (Term k) I) I)
-> I -> Either (SubCheck (Term k) I) I
forall a b. (a -> b) -> a -> b
$ Integer -> I
forall a. Num a => Integer -> a
fromInteger (Integer -> I) -> Integer -> I
forall a b. (a -> b) -> a -> b
$ Expr -> [[SomeVar]] -> ValueMap -> Integer
forall a. Typeable a => Expr -> [[SomeVar]] -> ValueMap -> a
eval' Expr
expr [[SomeVar]]
vss ValueMap
e

evalIs :: ValueMap -> Term k [Integer] -> [I]
evalIs :: forall (k :: TermKind). ValueMap -> Term k [Integer] -> [I]
evalIs ValueMap
d (Reverse Term k [a]
xs) = [I] -> [I]
forall a. [a] -> [a]
reverse ([I] -> [I]) -> [I] -> [I]
forall a b. (a -> b) -> a -> b
$ ValueMap -> Term k [Integer] -> [I]
forall (k :: TermKind). ValueMap -> Term k [Integer] -> [I]
evalIs ValueMap
d Term k [a]
Term k [Integer]
xs
evalIs ValueMap
d (All e a
v Int
n) = (Integer -> I) -> [Integer] -> [I]
forall a b. (a -> b) -> [a] -> [b]
map Integer -> I
forall a. Num a => Integer -> a
fromInteger ([Integer] -> [I]) -> [Integer] -> [I]
forall a b. (a -> b) -> a -> b
$ e Integer -> Int -> ValueMap -> [Integer]
forall a (e :: * -> *).
(Typeable a, VarExp e) =>
e a -> Int -> ValueMap -> [a]
primEvalVar e a
e Integer
v Int
n ValueMap
d
evalIs ValueMap
_ (ListLit [a]
xs) = (Integer -> I) -> [Integer] -> [I]
forall a b. (a -> b) -> [a] -> [b]
map Integer -> I
forall a. Num a => Integer -> a
fromInteger [a]
[Integer]
xs
evalIs ValueMap
_ Current{} = String -> [I]
forall a. HasCallStack => String -> a
error String
"list variables are not supported"
evalIs ValueMap
_ Add{} = String -> [I]
forall a. HasCallStack => String -> a
error String
"lists should not have a Num instance"
evalIs ValueMap
_ Sub{} = String -> [I]
forall a. HasCallStack => String -> a
error String
"lists should not have a Num instance"
evalIs ValueMap
_ Mul{} = String -> [I]
forall a. HasCallStack => String -> a
error String
"lists should not have a Num instance"
evalIs ValueMap
_ Sum{} = String -> [I]
forall a. HasCallStack => String -> a
error String
"lists should not have a Num instance"
evalIs ValueMap
_ Product{} = String -> [I]
forall a. HasCallStack => String -> a
error String
"lists should not have a Num instance"
evalIs ValueMap
e (Opaque Expr
expr [[SomeVar]]
vss [SomeTerm 'Transparent]
_ ) = Integer -> I
forall a. Num a => Integer -> a
fromInteger (Integer -> I) -> [Integer] -> [I]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> [[SomeVar]] -> ValueMap -> [Integer]
forall a. Typeable a => Expr -> [[SomeVar]] -> ValueMap -> a
eval' Expr
expr [[SomeVar]]
vss ValueMap
e

primEvalVar :: forall a e. (Typeable a, VarExp e) => e a -> Int -> ValueMap -> [a]
primEvalVar :: forall a (e :: * -> *).
(Typeable a, VarExp e) =>
e a -> Int -> ValueMap -> [a]
primEvalVar e a
x Int
n ValueMap
e =
  Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop Int
n ([a] -> [a]) -> ([ValueEntry] -> [a]) -> [ValueEntry] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a, Int) -> a) -> [(a, Int)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (a, Int) -> a
forall a b. (a, b) -> a
fst ([(a, Int)] -> [a])
-> ([ValueEntry] -> [(a, Int)]) -> [ValueEntry] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a, Int) -> (a, Int) -> Ordering) -> [(a, Int)] -> [(a, Int)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy ((Int -> Int -> Ordering) -> Int -> Int -> Ordering
forall a b c. (a -> b -> c) -> b -> a -> c
flip Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int -> Int -> Ordering)
-> ((a, Int) -> Int) -> (a, Int) -> (a, Int) -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (a, Int) -> Int
forall a b. (a, b) -> b
snd) ([(a, Int)] -> [(a, Int)])
-> ([ValueEntry] -> [(a, Int)]) -> [ValueEntry] -> [(a, Int)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ValueEntry -> [(a, Int)]) -> [ValueEntry] -> [(a, Int)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Var a -> ValueEntry -> [(a, Int)]
forall a. Var a -> ValueEntry -> [(a, Int)]
unwrapValueEntry ([Var a] -> Var a
forall a. HasCallStack => [a] -> a
head [Var a]
varList)) ([ValueEntry] -> [a]) -> [ValueEntry] -> [a]
forall a b. (a -> b) -> a -> b
$ (Var a -> Maybe ValueEntry) -> [Var a] -> [ValueEntry]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((SomeVar -> ValueMap -> Maybe ValueEntry
`ValueMap.lookup` ValueMap
e) (SomeVar -> Maybe ValueEntry)
-> (Var a -> SomeVar) -> Var a -> Maybe ValueEntry
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var a -> SomeVar
forall a. Typeable a => Var a -> SomeVar
someVar) [Var a]
varList
  where
    varList :: [Var a]
    varList :: [Var a]
varList = e a -> [Var a]
forall a. e a -> [Var a]
forall (e :: * -> *) a. VarExp e => e a -> [Var a]
toVarList e a
x

safeHead :: [a] -> Maybe a
safeHead :: forall a. [a] -> Maybe a
safeHead [] = Maybe a
forall a. Maybe a
Nothing
safeHead (a
x:[a]
_) = a -> Maybe a
forall a. a -> Maybe a
Just a
x

showResult :: (Show a, Typeable a) => a -> String
showResult :: forall a. (Show a, Typeable a) => a -> String
showResult a
x = a -> [Case a String] -> String
forall a r. Typeable a => a -> [Case a r] -> r
matchTypeOf a
x
  [ forall {k} a (x :: k) r. Typeable a => (a -> r) -> Case x r
forall a x r. Typeable a => (a -> r) -> Case x r
inCaseOf @String String -> String
forall a. a -> a
id
  , forall {k} a (x :: k) r. Typeable a => (a -> r) -> Case x r
forall a x r. Typeable a => (a -> r) -> Case x r
inCaseOf @Integer Integer -> String
forall a. Show a => a -> String
show
  , forall {k1} {k2} (f :: k1 -> *) (x :: k2) r.
Typeable f =>
(forall (a :: k1). (f a :~~: x) -> f a -> r) -> Case x r
forall (f :: * -> *) x r.
Typeable f =>
(forall a. (f a :~~: x) -> f a -> r) -> Case x r
inCaseOfApp @Embedded ((forall a. (Embedded a :~~: a) -> Embedded a -> String)
 -> Case a String)
-> (forall a. (Embedded a :~~: a) -> Embedded a -> String)
-> Case a String
forall a b. (a -> b) -> a -> b
$ \Embedded a :~~: a
HRefl (Embedded Integer
i :: Embedded a) -> forall a. Show a => a -> String
show @a (a -> String) -> a -> String
forall a b. (a -> b) -> a -> b
$ Integer -> a
forall a. Embeddable a => Integer -> a
asOriginal Integer
i
  , String -> Case a String
forall {k} r (x :: k). r -> Case x r
fallbackCase' (String -> Case a String) -> String -> Case a String
forall a b. (a -> b) -> a -> b
$ a -> String
forall a. Show a => a -> String
show a
x
  ]

showIndexedTerm :: Typeable a => Term k a -> Map SomeVar (Int,[Int]) -> String
showIndexedTerm :: forall a (k :: TermKind).
Typeable a =>
Term k a -> Map SomeVar (Int, [Int]) -> String
showIndexedTerm Term k a
t = Term k a -> Maybe (Map SomeVar (Int, [Int])) -> String
forall a (k :: TermKind).
Typeable a =>
Term k a -> Maybe (Map SomeVar (Int, [Int])) -> String
showTerm' Term k a
t (Maybe (Map SomeVar (Int, [Int])) -> String)
-> (Map SomeVar (Int, [Int]) -> Maybe (Map SomeVar (Int, [Int])))
-> Map SomeVar (Int, [Int])
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map SomeVar (Int, [Int]) -> Maybe (Map SomeVar (Int, [Int]))
forall a. a -> Maybe a
Just

showTerm :: Typeable a => Term k a -> String
showTerm :: forall a (k :: TermKind). Typeable a => Term k a -> String
showTerm Term k a
t = Term k a -> Maybe (Map SomeVar (Int, [Int])) -> String
forall a (k :: TermKind).
Typeable a =>
Term k a -> Maybe (Map SomeVar (Int, [Int])) -> String
showTerm' Term k a
t Maybe (Map SomeVar (Int, [Int]))
forall a. Maybe a
Nothing

showTerm' :: Typeable a => Term k a -> Maybe (Map SomeVar (Int,[Int])) -> String
showTerm' :: forall a (k :: TermKind).
Typeable a =>
Term k a -> Maybe (Map SomeVar (Int, [Int])) -> String
showTerm' (Add Term k a
x Term k a
y) Maybe (Map SomeVar (Int, [Int]))
m = String
-> Term k a
-> Term k a
-> Maybe (Map SomeVar (Int, [Int]))
-> String
forall a b (k1 :: TermKind) (k2 :: TermKind).
(Typeable a, Typeable b) =>
String
-> Term k1 a
-> Term k2 b
-> Maybe (Map SomeVar (Int, [Int]))
-> String
showBinary String
"+" Term k a
x Term k a
y Maybe (Map SomeVar (Int, [Int]))
m
showTerm' (Sub Term k a
x Term k a
y) Maybe (Map SomeVar (Int, [Int]))
m = String
-> Term k a
-> Term k a
-> Maybe (Map SomeVar (Int, [Int]))
-> String
forall a b (k1 :: TermKind) (k2 :: TermKind).
(Typeable a, Typeable b) =>
String
-> Term k1 a
-> Term k2 b
-> Maybe (Map SomeVar (Int, [Int]))
-> String
showBinary String
"-" Term k a
x Term k a
y Maybe (Map SomeVar (Int, [Int]))
m
showTerm' (Mul Term k a
x Term k a
y) Maybe (Map SomeVar (Int, [Int]))
m = String
-> Term k a
-> Term k a
-> Maybe (Map SomeVar (Int, [Int]))
-> String
forall a b (k1 :: TermKind) (k2 :: TermKind).
(Typeable a, Typeable b) =>
String
-> Term k1 a
-> Term k2 b
-> Maybe (Map SomeVar (Int, [Int]))
-> String
showBinary String
"*" Term k a
x Term k a
y Maybe (Map SomeVar (Int, [Int]))
m
showTerm' (Equals Term k a
x Term k a
y) Maybe (Map SomeVar (Int, [Int]))
m = String
-> Term k a
-> Term k a
-> Maybe (Map SomeVar (Int, [Int]))
-> String
forall a b (k1 :: TermKind) (k2 :: TermKind).
(Typeable a, Typeable b) =>
String
-> Term k1 a
-> Term k2 b
-> Maybe (Map SomeVar (Int, [Int]))
-> String
showBinary String
"==" Term k a
x Term k a
y Maybe (Map SomeVar (Int, [Int]))
m
showTerm' (Gt Term k a
x Term k a
y) Maybe (Map SomeVar (Int, [Int]))
m = String
-> Term k a
-> Term k a
-> Maybe (Map SomeVar (Int, [Int]))
-> String
forall a b (k1 :: TermKind) (k2 :: TermKind).
(Typeable a, Typeable b) =>
String
-> Term k1 a
-> Term k2 b
-> Maybe (Map SomeVar (Int, [Int]))
-> String
showBinary String
">" Term k a
x Term k a
y Maybe (Map SomeVar (Int, [Int]))
m
showTerm' (Ge Term k a
x Term k a
y) Maybe (Map SomeVar (Int, [Int]))
m = String
-> Term k a
-> Term k a
-> Maybe (Map SomeVar (Int, [Int]))
-> String
forall a b (k1 :: TermKind) (k2 :: TermKind).
(Typeable a, Typeable b) =>
String
-> Term k1 a
-> Term k2 b
-> Maybe (Map SomeVar (Int, [Int]))
-> String
showBinary String
">=" Term k a
x Term k a
y Maybe (Map SomeVar (Int, [Int]))
m
showTerm' (Lt Term k a
x Term k a
y) Maybe (Map SomeVar (Int, [Int]))
m = String
-> Term k a
-> Term k a
-> Maybe (Map SomeVar (Int, [Int]))
-> String
forall a b (k1 :: TermKind) (k2 :: TermKind).
(Typeable a, Typeable b) =>
String
-> Term k1 a
-> Term k2 b
-> Maybe (Map SomeVar (Int, [Int]))
-> String
showBinary String
"<" Term k a
x Term k a
y Maybe (Map SomeVar (Int, [Int]))
m
showTerm' (Le Term k a
x Term k a
y) Maybe (Map SomeVar (Int, [Int]))
m = String
-> Term k a
-> Term k a
-> Maybe (Map SomeVar (Int, [Int]))
-> String
forall a b (k1 :: TermKind) (k2 :: TermKind).
(Typeable a, Typeable b) =>
String
-> Term k1 a
-> Term k2 b
-> Maybe (Map SomeVar (Int, [Int]))
-> String
showBinary String
"<=" Term k a
x Term k a
y Maybe (Map SomeVar (Int, [Int]))
m
showTerm' (And Term k Bool
x Term k Bool
y) Maybe (Map SomeVar (Int, [Int]))
m = String
-> Term k Bool
-> Term k Bool
-> Maybe (Map SomeVar (Int, [Int]))
-> String
forall a b (k1 :: TermKind) (k2 :: TermKind).
(Typeable a, Typeable b) =>
String
-> Term k1 a
-> Term k2 b
-> Maybe (Map SomeVar (Int, [Int]))
-> String
showBinary String
"&&" Term k Bool
x Term k Bool
y Maybe (Map SomeVar (Int, [Int]))
m
showTerm' (Or Term k Bool
x Term k Bool
y) Maybe (Map SomeVar (Int, [Int]))
m = String
-> Term k Bool
-> Term k Bool
-> Maybe (Map SomeVar (Int, [Int]))
-> String
forall a b (k1 :: TermKind) (k2 :: TermKind).
(Typeable a, Typeable b) =>
String
-> Term k1 a
-> Term k2 b
-> Maybe (Map SomeVar (Int, [Int]))
-> String
showBinary String
"||" Term k Bool
x Term k Bool
y Maybe (Map SomeVar (Int, [Int]))
m
showTerm' (IsIn Term k a
x Term k [a]
xs) Maybe (Map SomeVar (Int, [Int]))
m = Term k a -> Maybe (Map SomeVar (Int, [Int])) -> String
forall a (k :: TermKind).
Typeable a =>
Term k a -> Maybe (Map SomeVar (Int, [Int])) -> String
showTerm' Term k a
x Maybe (Map SomeVar (Int, [Int]))
m String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ∈ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term k [a] -> Maybe (Map SomeVar (Int, [Int])) -> String
forall a (k :: TermKind).
Typeable a =>
Term k a -> Maybe (Map SomeVar (Int, [Int])) -> String
showTerm' Term k [a]
xs Maybe (Map SomeVar (Int, [Int]))
m
showTerm' (Not (IsIn Term k a
x Term k [a]
xs)) Maybe (Map SomeVar (Int, [Int]))
m = Term k a -> Maybe (Map SomeVar (Int, [Int])) -> String
forall a (k :: TermKind).
Typeable a =>
Term k a -> Maybe (Map SomeVar (Int, [Int])) -> String
showTerm' Term k a
x Maybe (Map SomeVar (Int, [Int]))
m String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ∉ " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term k [a] -> Maybe (Map SomeVar (Int, [Int])) -> String
forall a (k :: TermKind).
Typeable a =>
Term k a -> Maybe (Map SomeVar (Int, [Int])) -> String
showTerm' Term k [a]
xs Maybe (Map SomeVar (Int, [Int]))
m
showTerm' (Not Term k Bool
t) Maybe (Map SomeVar (Int, [Int]))
m = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"not (", Term k Bool -> Maybe (Map SomeVar (Int, [Int])) -> String
forall a (k :: TermKind).
Typeable a =>
Term k a -> Maybe (Map SomeVar (Int, [Int])) -> String
showTerm' Term k Bool
t Maybe (Map SomeVar (Int, [Int]))
m, String
")"]
showTerm' (BoolLit Bool
b) Maybe (Map SomeVar (Int, [Int]))
_ = Bool -> String
forall a. Show a => a -> String
show Bool
b
showTerm' (Length Term k [a]
xs) Maybe (Map SomeVar (Int, [Int]))
m = String -> Term k [a] -> Maybe (Map SomeVar (Int, [Int])) -> String
forall a (k :: TermKind).
Typeable a =>
String -> Term k a -> Maybe (Map SomeVar (Int, [Int])) -> String
showUnary String
"length" Term k [a]
xs Maybe (Map SomeVar (Int, [Int]))
m
showTerm' (Reverse Term k [a]
xs) Maybe (Map SomeVar (Int, [Int]))
m = String -> Term k [a] -> Maybe (Map SomeVar (Int, [Int])) -> String
forall a (k :: TermKind).
Typeable a =>
String -> Term k a -> Maybe (Map SomeVar (Int, [Int])) -> String
showUnary String
"reverse" Term k [a]
xs Maybe (Map SomeVar (Int, [Int]))
m
showTerm' (Sum Term k [a]
xs) Maybe (Map SomeVar (Int, [Int]))
m = String -> Term k [a] -> Maybe (Map SomeVar (Int, [Int])) -> String
forall a (k :: TermKind).
Typeable a =>
String -> Term k a -> Maybe (Map SomeVar (Int, [Int])) -> String
showUnary String
"sum" Term k [a]
xs Maybe (Map SomeVar (Int, [Int]))
m
showTerm' (Product Term k [a]
xs) Maybe (Map SomeVar (Int, [Int]))
m = String -> Term k [a] -> Maybe (Map SomeVar (Int, [Int])) -> String
forall a (k :: TermKind).
Typeable a =>
String -> Term k a -> Maybe (Map SomeVar (Int, [Int])) -> String
showUnary String
"product" Term k [a]
xs Maybe (Map SomeVar (Int, [Int]))
m
showTerm' (Current e a
x Int
n) (Just Map SomeVar (Int, [Int])
m) = (\(String
x,(Int
i,[Int]
_)) -> String
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i) ((String, (Int, [Int])) -> String)
-> (String, (Int, [Int])) -> String
forall a b. (a -> b) -> a -> b
$ ((String, (Int, [Int])) -> Int)
-> [(String, (Int, [Int]))] -> (String, (Int, [Int]))
forall b a. (HasCallStack, Ord b) => (a -> b) -> [a] -> a
maximumOn ([Int] -> Int
forall a. HasCallStack => [a] -> a
head([Int] -> Int)
-> ((String, (Int, [Int])) -> [Int])
-> (String, (Int, [Int]))
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Int, [Int]) -> [Int]
forall a b. (a, b) -> b
snd((Int, [Int]) -> [Int])
-> ((String, (Int, [Int])) -> (Int, [Int]))
-> (String, (Int, [Int]))
-> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(String, (Int, [Int])) -> (Int, [Int])
forall a b. (a, b) -> b
snd) ([(String, (Int, [Int]))] -> (String, (Int, [Int])))
-> [(String, (Int, [Int]))] -> (String, (Int, [Int]))
forall a b. (a -> b) -> a -> b
$ (\[(String, (Int, [Int]))]
xs -> Int -> [(String, (Int, [Int]))] -> [(String, (Int, [Int]))]
forall a. Int -> [a] -> [a]
take ([(String, (Int, [Int]))] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(String, (Int, [Int]))]
xs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n) [(String, (Int, [Int]))]
xs) ([(String, (Int, [Int]))] -> [(String, (Int, [Int]))])
-> [(String, (Int, [Int]))] -> [(String, (Int, [Int]))]
forall a b. (a -> b) -> a -> b
$ (Var a -> Maybe (String, (Int, [Int])))
-> [Var a] -> [(String, (Int, [Int]))]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (\Var a
x -> (Var a -> String
forall a. Var a -> String
varname Var a
x,) ((Int, [Int]) -> (String, (Int, [Int])))
-> Maybe (Int, [Int]) -> Maybe (String, (Int, [Int]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SomeVar -> Map SomeVar (Int, [Int]) -> Maybe (Int, [Int])
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Var a -> SomeVar
forall a. Typeable a => Var a -> SomeVar
someVar Var a
x) Map SomeVar (Int, [Int])
m) (e a -> [Var a]
forall a. e a -> [Var a]
forall (e :: * -> *) a. VarExp e => e a -> [Var a]
toVarList e a
x)
showTerm' (Current e a
x Int
n) Maybe (Map SomeVar (Int, [Int]))
Nothing = String
"{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ((Var a -> String) -> [Var a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Var a -> String
forall a. Var a -> String
varname ([Var a] -> [String]) -> [Var a] -> [String]
forall a b. (a -> b) -> a -> b
$ e a -> [Var a]
forall a. e a -> [Var a]
forall (e :: * -> *) a. VarExp e => e a -> [Var a]
toVarList e a
x) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}"String -> String -> String
forall a. [a] -> [a] -> [a]
++String
":"String -> String -> String
forall a. [a] -> [a] -> [a]
++Int -> String
forall a. Show a => a -> String
show Int
nString -> String -> String
forall a. [a] -> [a] -> [a]
++String
"_C"
showTerm' (All e a
x Int
n) Maybe (Map SomeVar (Int, [Int]))
_ = String
"{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ((Var a -> String) -> [Var a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Var a -> String
forall a. Var a -> String
varname ([Var a] -> [String]) -> [Var a] -> [String]
forall a b. (a -> b) -> a -> b
$ e a -> [Var a]
forall a. e a -> [Var a]
forall (e :: * -> *) a. VarExp e => e a -> [Var a]
toVarList e a
x) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}"String -> String -> String
forall a. [a] -> [a] -> [a]
++String
":"String -> String -> String
forall a. [a] -> [a] -> [a]
++Int -> String
forall a. Show a => a -> String
show Int
nString -> String -> String
forall a. [a] -> [a] -> [a]
++String
"_A"
showTerm' (IntLit Integer
x) Maybe (Map SomeVar (Int, [Int]))
_ = Integer -> String
forall a. Show a => a -> String
show Integer
x
showTerm' (ListLit [a]
xs) Maybe (Map SomeVar (Int, [Int]))
_ = [a] -> String
forall a. Show a => a -> String
show [a]
xs
showTerm' (EmbeddedLit a
x) Maybe (Map SomeVar (Int, [Int]))
_ = a -> String
forall a. Show a => a -> String
show a
x
showTerm' t :: Term k a
t@Opaque{} Maybe (Map SomeVar (Int, [Int]))
_ = Term k a -> String
forall a. Show a => a -> String
show Term k a
t -- TODO: improve

showBinary :: (Typeable a, Typeable b) => String -> Term k1 a -> Term k2 b -> Maybe (Map SomeVar (Int,[Int])) -> String
showBinary :: forall a b (k1 :: TermKind) (k2 :: TermKind).
(Typeable a, Typeable b) =>
String
-> Term k1 a
-> Term k2 b
-> Maybe (Map SomeVar (Int, [Int]))
-> String
showBinary String
op Term k1 a
x Term k2 b
y Maybe (Map SomeVar (Int, [Int]))
m = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
"(",Term k1 a -> Maybe (Map SomeVar (Int, [Int])) -> String
forall a (k :: TermKind).
Typeable a =>
Term k a -> Maybe (Map SomeVar (Int, [Int])) -> String
showTerm' Term k1 a
x Maybe (Map SomeVar (Int, [Int]))
m, String
") ",String
op,String
" (", Term k2 b -> Maybe (Map SomeVar (Int, [Int])) -> String
forall a (k :: TermKind).
Typeable a =>
Term k a -> Maybe (Map SomeVar (Int, [Int])) -> String
showTerm' Term k2 b
y Maybe (Map SomeVar (Int, [Int]))
m,String
")"]

showUnary :: Typeable a => String -> Term k a -> Maybe (Map SomeVar (Int,[Int])) -> String
showUnary :: forall a (k :: TermKind).
Typeable a =>
String -> Term k a -> Maybe (Map SomeVar (Int, [Int])) -> String
showUnary String
op Term k a
x Maybe (Map SomeVar (Int, [Int]))
m = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [String
op String -> String -> String
forall a. [a] -> [a] -> [a]
++String
" (", Term k a -> Maybe (Map SomeVar (Int, [Int])) -> String
forall a (k :: TermKind).
Typeable a =>
Term k a -> Maybe (Map SomeVar (Int, [Int])) -> String
showTerm' Term k a
x Maybe (Map SomeVar (Int, [Int]))
m, String
")"]

data SomeTerm k where
  SomeTerm :: Typeable a => Term k a -> SomeTerm k

withSomeTerm :: SomeTerm k -> (forall a. Typeable a => Term k a -> r) -> r
withSomeTerm :: forall (k :: TermKind) r.
SomeTerm k -> (forall a. Typeable a => Term k a -> r) -> r
withSomeTerm (SomeTerm Term k a
t) forall a. Typeable a => Term k a -> r
f = Term k a -> r
forall a. Typeable a => Term k a -> r
f Term k a
t

data SomeTermK where
  SomeTermK :: SomeTerm k -> SomeTermK

{- HLINT ignore withSomeTermK "Eta reduce" -}
-- eta-reduced version causes type error in Haddock workflow
withSomeTermK :: SomeTermK -> (forall (k :: TermKind) a. Typeable a => Term k a -> r) -> r
withSomeTermK :: forall r.
SomeTermK
-> (forall (k :: TermKind) a. Typeable a => Term k a -> r) -> r
withSomeTermK (SomeTermK SomeTerm k
t) forall (k :: TermKind) a. Typeable a => Term k a -> r
f = SomeTerm k -> (forall a. Typeable a => Term k a -> r) -> r
forall (k :: TermKind) r.
SomeTerm k -> (forall a. Typeable a => Term k a -> r) -> r
withSomeTerm SomeTerm k
t Term k a -> r
forall a. Typeable a => Term k a -> r
forall (k :: TermKind) a. Typeable a => Term k a -> r
f
--
someTerm :: Typeable a => Term k a -> SomeTerm k
someTerm :: forall a (k :: TermKind). Typeable a => Term k a -> SomeTerm k
someTerm = Term k a -> SomeTerm k
forall a (k :: TermKind). Typeable a => Term k a -> SomeTerm k
SomeTerm

transparentSubterms :: Typeable a => Term k a -> [SomeTerm 'Transparent]
transparentSubterms :: forall a (k :: TermKind).
Typeable a =>
Term k a -> [SomeTerm 'Transparent]
transparentSubterms t :: Term k a
t@(Add Term k a
x Term k a
y) = Maybe (SomeTerm 'Transparent) -> [SomeTerm 'Transparent]
forall a. Maybe a -> [a]
maybeToList (Term 'Transparent a -> SomeTerm 'Transparent
forall a (k :: TermKind). Typeable a => Term k a -> SomeTerm k
someTerm (Term 'Transparent a -> SomeTerm 'Transparent)
-> Maybe (Term 'Transparent a) -> Maybe (SomeTerm 'Transparent)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
t) [SomeTerm 'Transparent]
-> [SomeTerm 'Transparent] -> [SomeTerm 'Transparent]
forall a. [a] -> [a] -> [a]
++ 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 a -> [SomeTerm 'Transparent]
forall a (k :: TermKind).
Typeable a =>
Term k a -> [SomeTerm 'Transparent]
transparentSubterms Term k a
y
transparentSubterms t :: Term k a
t@(Sub Term k a
x Term k a
y) = Maybe (SomeTerm 'Transparent) -> [SomeTerm 'Transparent]
forall a. Maybe a -> [a]
maybeToList (Term 'Transparent a -> SomeTerm 'Transparent
forall a (k :: TermKind). Typeable a => Term k a -> SomeTerm k
someTerm (Term 'Transparent a -> SomeTerm 'Transparent)
-> Maybe (Term 'Transparent a) -> Maybe (SomeTerm 'Transparent)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
t) [SomeTerm 'Transparent]
-> [SomeTerm 'Transparent] -> [SomeTerm 'Transparent]
forall a. [a] -> [a] -> [a]
++ 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 a -> [SomeTerm 'Transparent]
forall a (k :: TermKind).
Typeable a =>
Term k a -> [SomeTerm 'Transparent]
transparentSubterms Term k a
y
transparentSubterms t :: Term k a
t@(Mul Term k a
x Term k a
y) = Maybe (SomeTerm 'Transparent) -> [SomeTerm 'Transparent]
forall a. Maybe a -> [a]
maybeToList (Term 'Transparent a -> SomeTerm 'Transparent
forall a (k :: TermKind). Typeable a => Term k a -> SomeTerm k
someTerm (Term 'Transparent a -> SomeTerm 'Transparent)
-> Maybe (Term 'Transparent a) -> Maybe (SomeTerm 'Transparent)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
t) [SomeTerm 'Transparent]
-> [SomeTerm 'Transparent] -> [SomeTerm 'Transparent]
forall a. [a] -> [a] -> [a]
++ 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 a -> [SomeTerm 'Transparent]
forall a (k :: TermKind).
Typeable a =>
Term k a -> [SomeTerm 'Transparent]
transparentSubterms Term k a
y
transparentSubterms t :: Term k a
t@(Equals Term k a
x Term k a
y) = Maybe (SomeTerm 'Transparent) -> [SomeTerm 'Transparent]
forall a. Maybe a -> [a]
maybeToList (Term 'Transparent a -> SomeTerm 'Transparent
forall a (k :: TermKind). Typeable a => Term k a -> SomeTerm k
someTerm (Term 'Transparent a -> SomeTerm 'Transparent)
-> Maybe (Term 'Transparent a) -> Maybe (SomeTerm 'Transparent)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
t) [SomeTerm 'Transparent]
-> [SomeTerm 'Transparent] -> [SomeTerm 'Transparent]
forall a. [a] -> [a] -> [a]
++ 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 a -> [SomeTerm 'Transparent]
forall a (k :: TermKind).
Typeable a =>
Term k a -> [SomeTerm 'Transparent]
transparentSubterms Term k a
y
transparentSubterms t :: Term k a
t@(Gt Term k a
x Term k a
y) = Maybe (SomeTerm 'Transparent) -> [SomeTerm 'Transparent]
forall a. Maybe a -> [a]
maybeToList (Term 'Transparent a -> SomeTerm 'Transparent
forall a (k :: TermKind). Typeable a => Term k a -> SomeTerm k
someTerm (Term 'Transparent a -> SomeTerm 'Transparent)
-> Maybe (Term 'Transparent a) -> Maybe (SomeTerm 'Transparent)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
t) [SomeTerm 'Transparent]
-> [SomeTerm 'Transparent] -> [SomeTerm 'Transparent]
forall a. [a] -> [a] -> [a]
++ 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 a -> [SomeTerm 'Transparent]
forall a (k :: TermKind).
Typeable a =>
Term k a -> [SomeTerm 'Transparent]
transparentSubterms Term k a
y
transparentSubterms t :: Term k a
t@(Ge Term k a
x Term k a
y) = Maybe (SomeTerm 'Transparent) -> [SomeTerm 'Transparent]
forall a. Maybe a -> [a]
maybeToList (Term 'Transparent a -> SomeTerm 'Transparent
forall a (k :: TermKind). Typeable a => Term k a -> SomeTerm k
someTerm (Term 'Transparent a -> SomeTerm 'Transparent)
-> Maybe (Term 'Transparent a) -> Maybe (SomeTerm 'Transparent)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
t) [SomeTerm 'Transparent]
-> [SomeTerm 'Transparent] -> [SomeTerm 'Transparent]
forall a. [a] -> [a] -> [a]
++ 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 a -> [SomeTerm 'Transparent]
forall a (k :: TermKind).
Typeable a =>
Term k a -> [SomeTerm 'Transparent]
transparentSubterms Term k a
y
transparentSubterms t :: Term k a
t@(Lt Term k a
x Term k a
y) = Maybe (SomeTerm 'Transparent) -> [SomeTerm 'Transparent]
forall a. Maybe a -> [a]
maybeToList (Term 'Transparent a -> SomeTerm 'Transparent
forall a (k :: TermKind). Typeable a => Term k a -> SomeTerm k
someTerm (Term 'Transparent a -> SomeTerm 'Transparent)
-> Maybe (Term 'Transparent a) -> Maybe (SomeTerm 'Transparent)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
t) [SomeTerm 'Transparent]
-> [SomeTerm 'Transparent] -> [SomeTerm 'Transparent]
forall a. [a] -> [a] -> [a]
++ 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 a -> [SomeTerm 'Transparent]
forall a (k :: TermKind).
Typeable a =>
Term k a -> [SomeTerm 'Transparent]
transparentSubterms Term k a
y
transparentSubterms t :: Term k a
t@(Le Term k a
x Term k a
y) = Maybe (SomeTerm 'Transparent) -> [SomeTerm 'Transparent]
forall a. Maybe a -> [a]
maybeToList (Term 'Transparent a -> SomeTerm 'Transparent
forall a (k :: TermKind). Typeable a => Term k a -> SomeTerm k
someTerm (Term 'Transparent a -> SomeTerm 'Transparent)
-> Maybe (Term 'Transparent a) -> Maybe (SomeTerm 'Transparent)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
t) [SomeTerm 'Transparent]
-> [SomeTerm 'Transparent] -> [SomeTerm 'Transparent]
forall a. [a] -> [a] -> [a]
++ 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 a -> [SomeTerm 'Transparent]
forall a (k :: TermKind).
Typeable a =>
Term k a -> [SomeTerm 'Transparent]
transparentSubterms Term k a
y
transparentSubterms t :: Term k a
t@(And Term k Bool
x Term k Bool
y) = Maybe (SomeTerm 'Transparent) -> [SomeTerm 'Transparent]
forall a. Maybe a -> [a]
maybeToList (Term 'Transparent a -> SomeTerm 'Transparent
forall a (k :: TermKind). Typeable a => Term k a -> SomeTerm k
someTerm (Term 'Transparent a -> SomeTerm 'Transparent)
-> Maybe (Term 'Transparent a) -> Maybe (SomeTerm 'Transparent)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
t) [SomeTerm 'Transparent]
-> [SomeTerm 'Transparent] -> [SomeTerm 'Transparent]
forall a. [a] -> [a] -> [a]
++ Term k Bool -> [SomeTerm 'Transparent]
forall a (k :: TermKind).
Typeable a =>
Term k a -> [SomeTerm 'Transparent]
transparentSubterms Term k Bool
x [SomeTerm 'Transparent]
-> [SomeTerm 'Transparent] -> [SomeTerm 'Transparent]
forall a. [a] -> [a] -> [a]
++ Term k Bool -> [SomeTerm 'Transparent]
forall a (k :: TermKind).
Typeable a =>
Term k a -> [SomeTerm 'Transparent]
transparentSubterms Term k Bool
y
transparentSubterms t :: Term k a
t@(Or Term k Bool
x Term k Bool
y) = Maybe (SomeTerm 'Transparent) -> [SomeTerm 'Transparent]
forall a. Maybe a -> [a]
maybeToList (Term 'Transparent a -> SomeTerm 'Transparent
forall a (k :: TermKind). Typeable a => Term k a -> SomeTerm k
someTerm (Term 'Transparent a -> SomeTerm 'Transparent)
-> Maybe (Term 'Transparent a) -> Maybe (SomeTerm 'Transparent)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
t) [SomeTerm 'Transparent]
-> [SomeTerm 'Transparent] -> [SomeTerm 'Transparent]
forall a. [a] -> [a] -> [a]
++ Term k Bool -> [SomeTerm 'Transparent]
forall a (k :: TermKind).
Typeable a =>
Term k a -> [SomeTerm 'Transparent]
transparentSubterms Term k Bool
x [SomeTerm 'Transparent]
-> [SomeTerm 'Transparent] -> [SomeTerm 'Transparent]
forall a. [a] -> [a] -> [a]
++ Term k Bool -> [SomeTerm 'Transparent]
forall a (k :: TermKind).
Typeable a =>
Term k a -> [SomeTerm 'Transparent]
transparentSubterms Term k Bool
y
transparentSubterms t :: Term k a
t@(IsIn Term k a
x Term k [a]
y) = Maybe (SomeTerm 'Transparent) -> [SomeTerm 'Transparent]
forall a. Maybe a -> [a]
maybeToList (Term 'Transparent a -> SomeTerm 'Transparent
forall a (k :: TermKind). Typeable a => Term k a -> SomeTerm k
someTerm (Term 'Transparent a -> SomeTerm 'Transparent)
-> Maybe (Term 'Transparent a) -> Maybe (SomeTerm 'Transparent)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
t) [SomeTerm 'Transparent]
-> [SomeTerm 'Transparent] -> [SomeTerm 'Transparent]
forall a. [a] -> [a] -> [a]
++ 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 [a] -> [SomeTerm 'Transparent]
forall a (k :: TermKind).
Typeable a =>
Term k a -> [SomeTerm 'Transparent]
transparentSubterms Term k [a]
y
transparentSubterms t :: Term k a
t@(Sum Term k [a]
x) = Maybe (SomeTerm 'Transparent) -> [SomeTerm 'Transparent]
forall a. Maybe a -> [a]
maybeToList (Term 'Transparent a -> SomeTerm 'Transparent
forall a (k :: TermKind). Typeable a => Term k a -> SomeTerm k
someTerm (Term 'Transparent a -> SomeTerm 'Transparent)
-> Maybe (Term 'Transparent a) -> Maybe (SomeTerm 'Transparent)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
t) [SomeTerm 'Transparent]
-> [SomeTerm 'Transparent] -> [SomeTerm 'Transparent]
forall a. [a] -> [a] -> [a]
++ Term k [a] -> [SomeTerm 'Transparent]
forall a (k :: TermKind).
Typeable a =>
Term k a -> [SomeTerm 'Transparent]
transparentSubterms Term k [a]
x
transparentSubterms t :: Term k a
t@(Product Term k [a]
x) = Maybe (SomeTerm 'Transparent) -> [SomeTerm 'Transparent]
forall a. Maybe a -> [a]
maybeToList (Term 'Transparent a -> SomeTerm 'Transparent
forall a (k :: TermKind). Typeable a => Term k a -> SomeTerm k
someTerm (Term 'Transparent a -> SomeTerm 'Transparent)
-> Maybe (Term 'Transparent a) -> Maybe (SomeTerm 'Transparent)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
t) [SomeTerm 'Transparent]
-> [SomeTerm 'Transparent] -> [SomeTerm 'Transparent]
forall a. [a] -> [a] -> [a]
++ Term k [a] -> [SomeTerm 'Transparent]
forall a (k :: TermKind).
Typeable a =>
Term k a -> [SomeTerm 'Transparent]
transparentSubterms Term k [a]
x
transparentSubterms t :: Term k a
t@(Length Term k [a]
x) = Maybe (SomeTerm 'Transparent) -> [SomeTerm 'Transparent]
forall a. Maybe a -> [a]
maybeToList (Term 'Transparent a -> SomeTerm 'Transparent
forall a (k :: TermKind). Typeable a => Term k a -> SomeTerm k
someTerm (Term 'Transparent a -> SomeTerm 'Transparent)
-> Maybe (Term 'Transparent a) -> Maybe (SomeTerm 'Transparent)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
t) [SomeTerm 'Transparent]
-> [SomeTerm 'Transparent] -> [SomeTerm 'Transparent]
forall a. [a] -> [a] -> [a]
++ Term k [a] -> [SomeTerm 'Transparent]
forall a (k :: TermKind).
Typeable a =>
Term k a -> [SomeTerm 'Transparent]
transparentSubterms Term k [a]
x
transparentSubterms t :: Term k a
t@(Reverse Term k [a]
x) = Maybe (SomeTerm 'Transparent) -> [SomeTerm 'Transparent]
forall a. Maybe a -> [a]
maybeToList (Term 'Transparent a -> SomeTerm 'Transparent
forall a (k :: TermKind). Typeable a => Term k a -> SomeTerm k
someTerm (Term 'Transparent a -> SomeTerm 'Transparent)
-> Maybe (Term 'Transparent a) -> Maybe (SomeTerm 'Transparent)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
t) [SomeTerm 'Transparent]
-> [SomeTerm 'Transparent] -> [SomeTerm 'Transparent]
forall a. [a] -> [a] -> [a]
++ Term k [a] -> [SomeTerm 'Transparent]
forall a (k :: TermKind).
Typeable a =>
Term k a -> [SomeTerm 'Transparent]
transparentSubterms Term k [a]
x
transparentSubterms t :: Term k a
t@(Not Term k Bool
x) = Maybe (SomeTerm 'Transparent) -> [SomeTerm 'Transparent]
forall a. Maybe a -> [a]
maybeToList (Term 'Transparent a -> SomeTerm 'Transparent
forall a (k :: TermKind). Typeable a => Term k a -> SomeTerm k
someTerm (Term 'Transparent a -> SomeTerm 'Transparent)
-> Maybe (Term 'Transparent a) -> Maybe (SomeTerm 'Transparent)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
t) [SomeTerm 'Transparent]
-> [SomeTerm 'Transparent] -> [SomeTerm 'Transparent]
forall a. [a] -> [a] -> [a]
++ Term k Bool -> [SomeTerm 'Transparent]
forall a (k :: TermKind).
Typeable a =>
Term k a -> [SomeTerm 'Transparent]
transparentSubterms Term k Bool
x
transparentSubterms t :: Term k a
t@(IntLit Integer
_) =  Maybe (SomeTerm 'Transparent) -> [SomeTerm 'Transparent]
forall a. Maybe a -> [a]
maybeToList (Term 'Transparent a -> SomeTerm 'Transparent
forall a (k :: TermKind). Typeable a => Term k a -> SomeTerm k
someTerm (Term 'Transparent a -> SomeTerm 'Transparent)
-> Maybe (Term 'Transparent a) -> Maybe (SomeTerm 'Transparent)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
t)
transparentSubterms t :: Term k a
t@(ListLit [a]
_) =  Maybe (SomeTerm 'Transparent) -> [SomeTerm 'Transparent]
forall a. Maybe a -> [a]
maybeToList (Term 'Transparent a -> SomeTerm 'Transparent
forall a (k :: TermKind). Typeable a => Term k a -> SomeTerm k
someTerm (Term 'Transparent a -> SomeTerm 'Transparent)
-> Maybe (Term 'Transparent a) -> Maybe (SomeTerm 'Transparent)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
t)
transparentSubterms t :: Term k a
t@(EmbeddedLit a
_) =  Maybe (SomeTerm 'Transparent) -> [SomeTerm 'Transparent]
forall a. Maybe a -> [a]
maybeToList (Term 'Transparent a -> SomeTerm 'Transparent
forall a (k :: TermKind). Typeable a => Term k a -> SomeTerm k
someTerm (Term 'Transparent a -> SomeTerm 'Transparent)
-> Maybe (Term 'Transparent a) -> Maybe (SomeTerm 'Transparent)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
t)
transparentSubterms t :: Term k a
t@(BoolLit Bool
_) =  Maybe (SomeTerm 'Transparent) -> [SomeTerm 'Transparent]
forall a. Maybe a -> [a]
maybeToList (Term 'Transparent a -> SomeTerm 'Transparent
forall a (k :: TermKind). Typeable a => Term k a -> SomeTerm k
someTerm (Term 'Transparent a -> SomeTerm 'Transparent)
-> Maybe (Term 'Transparent a) -> Maybe (SomeTerm 'Transparent)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
t)
transparentSubterms t :: Term k a
t@(Current e a
_ Int
_) =  Maybe (SomeTerm 'Transparent) -> [SomeTerm 'Transparent]
forall a. Maybe a -> [a]
maybeToList (Term 'Transparent a -> SomeTerm 'Transparent
forall a (k :: TermKind). Typeable a => Term k a -> SomeTerm k
someTerm (Term 'Transparent a -> SomeTerm 'Transparent)
-> Maybe (Term 'Transparent a) -> Maybe (SomeTerm 'Transparent)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
t)
transparentSubterms t :: Term k a
t@(All e a
_ Int
_) =  Maybe (SomeTerm 'Transparent) -> [SomeTerm 'Transparent]
forall a. Maybe a -> [a]
maybeToList (Term 'Transparent a -> SomeTerm 'Transparent
forall a (k :: TermKind). Typeable a => Term k a -> SomeTerm k
someTerm (Term 'Transparent a -> SomeTerm 'Transparent)
-> Maybe (Term 'Transparent a) -> Maybe (SomeTerm 'Transparent)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
t)
transparentSubterms (Opaque Expr
_ [[SomeVar]]
_ [SomeTerm 'Transparent]
ts) = [SomeTerm 'Transparent]
ts

maybeTransparentTerm :: forall (k :: TermKind) a. Typeable a => Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm :: forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Opaque{} = Maybe (Term 'Transparent a)
forall a. Maybe a
Nothing
maybeTransparentTerm (Add Term k a
x Term k a
y) = Term 'Transparent a -> Term 'Transparent a -> Term 'Transparent a
forall a (k :: TermKind). Num a => Term k a -> Term k a -> Term k a
Add (Term 'Transparent a -> Term 'Transparent a -> Term 'Transparent a)
-> Maybe (Term 'Transparent a)
-> Maybe (Term 'Transparent a -> Term 'Transparent a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
x Maybe (Term 'Transparent a -> Term 'Transparent a)
-> Maybe (Term 'Transparent a) -> Maybe (Term 'Transparent a)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
y
maybeTransparentTerm (Sub Term k a
x Term k a
y) = Term 'Transparent a -> Term 'Transparent a -> Term 'Transparent a
forall a (k :: TermKind). Num a => Term k a -> Term k a -> Term k a
Sub (Term 'Transparent a -> Term 'Transparent a -> Term 'Transparent a)
-> Maybe (Term 'Transparent a)
-> Maybe (Term 'Transparent a -> Term 'Transparent a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
x Maybe (Term 'Transparent a -> Term 'Transparent a)
-> Maybe (Term 'Transparent a) -> Maybe (Term 'Transparent a)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
y
maybeTransparentTerm (Mul Term k a
x Term k a
y) = Term 'Transparent a -> Term 'Transparent a -> Term 'Transparent a
forall a (k :: TermKind). Num a => Term k a -> Term k a -> Term k a
Mul (Term 'Transparent a -> Term 'Transparent a -> Term 'Transparent a)
-> Maybe (Term 'Transparent a)
-> Maybe (Term 'Transparent a -> Term 'Transparent a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
x Maybe (Term 'Transparent a -> Term 'Transparent a)
-> Maybe (Term 'Transparent a) -> Maybe (Term 'Transparent a)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
y
maybeTransparentTerm (Equals Term k a
x Term k a
y) = Term 'Transparent a -> Term 'Transparent a -> Term 'Transparent a
Term 'Transparent a
-> Term 'Transparent a -> Term 'Transparent Bool
forall a (k :: TermKind).
(Typeable a, Eq a) =>
Term k a -> Term k a -> Term k Bool
Equals (Term 'Transparent a -> Term 'Transparent a -> Term 'Transparent a)
-> Maybe (Term 'Transparent a)
-> Maybe (Term 'Transparent a -> Term 'Transparent a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
x Maybe (Term 'Transparent a -> Term 'Transparent a)
-> Maybe (Term 'Transparent a) -> Maybe (Term 'Transparent a)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
y
maybeTransparentTerm (Gt Term k a
x Term k a
y) = Term 'Transparent a -> Term 'Transparent a -> Term 'Transparent a
Term 'Transparent a
-> Term 'Transparent a -> Term 'Transparent Bool
forall a (k :: TermKind).
(Typeable a, Ord a) =>
Term k a -> Term k a -> Term k Bool
Gt (Term 'Transparent a -> Term 'Transparent a -> Term 'Transparent a)
-> Maybe (Term 'Transparent a)
-> Maybe (Term 'Transparent a -> Term 'Transparent a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
x Maybe (Term 'Transparent a -> Term 'Transparent a)
-> Maybe (Term 'Transparent a) -> Maybe (Term 'Transparent a)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
y
maybeTransparentTerm (Ge Term k a
x Term k a
y) = Term 'Transparent a -> Term 'Transparent a -> Term 'Transparent a
Term 'Transparent a
-> Term 'Transparent a -> Term 'Transparent Bool
forall a (k :: TermKind).
(Typeable a, Ord a) =>
Term k a -> Term k a -> Term k Bool
Ge (Term 'Transparent a -> Term 'Transparent a -> Term 'Transparent a)
-> Maybe (Term 'Transparent a)
-> Maybe (Term 'Transparent a -> Term 'Transparent a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
x Maybe (Term 'Transparent a -> Term 'Transparent a)
-> Maybe (Term 'Transparent a) -> Maybe (Term 'Transparent a)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
y
maybeTransparentTerm (Lt Term k a
x Term k a
y) = Term 'Transparent a -> Term 'Transparent a -> Term 'Transparent a
Term 'Transparent a
-> Term 'Transparent a -> Term 'Transparent Bool
forall a (k :: TermKind).
(Typeable a, Ord a) =>
Term k a -> Term k a -> Term k Bool
Lt (Term 'Transparent a -> Term 'Transparent a -> Term 'Transparent a)
-> Maybe (Term 'Transparent a)
-> Maybe (Term 'Transparent a -> Term 'Transparent a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
x Maybe (Term 'Transparent a -> Term 'Transparent a)
-> Maybe (Term 'Transparent a) -> Maybe (Term 'Transparent a)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
y
maybeTransparentTerm (Le Term k a
x Term k a
y) = Term 'Transparent a -> Term 'Transparent a -> Term 'Transparent a
Term 'Transparent a
-> Term 'Transparent a -> Term 'Transparent Bool
forall a (k :: TermKind).
(Typeable a, Ord a) =>
Term k a -> Term k a -> Term k Bool
Le (Term 'Transparent a -> Term 'Transparent a -> Term 'Transparent a)
-> Maybe (Term 'Transparent a)
-> Maybe (Term 'Transparent a -> Term 'Transparent a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
x Maybe (Term 'Transparent a -> Term 'Transparent a)
-> Maybe (Term 'Transparent a) -> Maybe (Term 'Transparent a)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
y
maybeTransparentTerm (And Term k Bool
x Term k Bool
y) = Term 'Transparent Bool
-> Term 'Transparent Bool -> Term 'Transparent a
Term 'Transparent Bool
-> Term 'Transparent Bool -> Term 'Transparent Bool
forall (k :: TermKind). Term k Bool -> Term k Bool -> Term k Bool
And (Term 'Transparent Bool
 -> Term 'Transparent Bool -> Term 'Transparent a)
-> Maybe (Term 'Transparent Bool)
-> Maybe (Term 'Transparent Bool -> Term 'Transparent a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k Bool -> Maybe (Term 'Transparent Bool)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k Bool
x Maybe (Term 'Transparent Bool -> Term 'Transparent a)
-> Maybe (Term 'Transparent Bool) -> Maybe (Term 'Transparent a)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term k Bool -> Maybe (Term 'Transparent Bool)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k Bool
y
maybeTransparentTerm (Or Term k Bool
x Term k Bool
y) = Term 'Transparent Bool
-> Term 'Transparent Bool -> Term 'Transparent a
Term 'Transparent Bool
-> Term 'Transparent Bool -> Term 'Transparent Bool
forall (k :: TermKind). Term k Bool -> Term k Bool -> Term k Bool
Or (Term 'Transparent Bool
 -> Term 'Transparent Bool -> Term 'Transparent a)
-> Maybe (Term 'Transparent Bool)
-> Maybe (Term 'Transparent Bool -> Term 'Transparent a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k Bool -> Maybe (Term 'Transparent Bool)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k Bool
x Maybe (Term 'Transparent Bool -> Term 'Transparent a)
-> Maybe (Term 'Transparent Bool) -> Maybe (Term 'Transparent a)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term k Bool -> Maybe (Term 'Transparent Bool)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k Bool
y
maybeTransparentTerm (IsIn Term k a
x Term k [a]
y) = Term 'Transparent a -> Term 'Transparent [a] -> Term 'Transparent a
Term 'Transparent a
-> Term 'Transparent [a] -> Term 'Transparent Bool
forall a (k :: TermKind).
(Typeable a, Eq a) =>
Term k a -> Term k [a] -> Term k Bool
IsIn (Term 'Transparent a
 -> Term 'Transparent [a] -> Term 'Transparent a)
-> Maybe (Term 'Transparent a)
-> Maybe (Term 'Transparent [a] -> Term 'Transparent a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k a -> Maybe (Term 'Transparent a)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k a
x Maybe (Term 'Transparent [a] -> Term 'Transparent a)
-> Maybe (Term 'Transparent [a]) -> Maybe (Term 'Transparent a)
forall a b. Maybe (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Term k [a] -> Maybe (Term 'Transparent [a])
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k [a]
y
maybeTransparentTerm (Sum Term k [a]
x) = Term 'Transparent [a] -> Term 'Transparent a
forall a (k :: TermKind). Num a => Term k [a] -> Term k a
Sum (Term 'Transparent [a] -> Term 'Transparent a)
-> Maybe (Term 'Transparent [a]) -> Maybe (Term 'Transparent a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k [a] -> Maybe (Term 'Transparent [a])
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k [a]
x
maybeTransparentTerm (Product Term k [a]
x) = Term 'Transparent [a] -> Term 'Transparent a
forall a (k :: TermKind). Num a => Term k [a] -> Term k a
Product (Term 'Transparent [a] -> Term 'Transparent a)
-> Maybe (Term 'Transparent [a]) -> Maybe (Term 'Transparent a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k [a] -> Maybe (Term 'Transparent [a])
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k [a]
x
maybeTransparentTerm (Length Term k [a]
x) = Term 'Transparent [a] -> Term 'Transparent a
Term 'Transparent [a] -> Term 'Transparent Integer
forall a (k :: TermKind).
Typeable a =>
Term k [a] -> Term k Integer
Length (Term 'Transparent [a] -> Term 'Transparent a)
-> Maybe (Term 'Transparent [a]) -> Maybe (Term 'Transparent a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k [a] -> Maybe (Term 'Transparent [a])
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k [a]
x
maybeTransparentTerm (Reverse Term k [a]
x) = Term 'Transparent [a] -> Term 'Transparent a
Term 'Transparent [a] -> Term 'Transparent [a]
forall a (k :: TermKind). Typeable a => Term k [a] -> Term k [a]
Reverse (Term 'Transparent [a] -> Term 'Transparent a)
-> Maybe (Term 'Transparent [a]) -> Maybe (Term 'Transparent a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k [a] -> Maybe (Term 'Transparent [a])
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k [a]
x
maybeTransparentTerm (Not Term k Bool
x) = Term 'Transparent Bool -> Term 'Transparent a
Term 'Transparent Bool -> Term 'Transparent Bool
forall (k :: TermKind). Term k Bool -> Term k Bool
Not (Term 'Transparent Bool -> Term 'Transparent a)
-> Maybe (Term 'Transparent Bool) -> Maybe (Term 'Transparent a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Term k Bool -> Maybe (Term 'Transparent Bool)
forall (k :: TermKind) a.
Typeable a =>
Term k a -> Maybe (Term 'Transparent a)
maybeTransparentTerm Term k Bool
x
maybeTransparentTerm (IntLit Integer
x) = Term 'Transparent a -> Maybe (Term 'Transparent a)
forall a. a -> Maybe a
Just (Term 'Transparent a -> Maybe (Term 'Transparent a))
-> Term 'Transparent a -> Maybe (Term 'Transparent a)
forall a b. (a -> b) -> a -> b
$ Integer -> Term 'Transparent Integer
forall (k :: TermKind). Integer -> Term k Integer
IntLit Integer
x
maybeTransparentTerm (ListLit [a]
xs) = Term 'Transparent a -> Maybe (Term 'Transparent a)
forall a. a -> Maybe a
Just (Term 'Transparent a -> Maybe (Term 'Transparent a))
-> Term 'Transparent a -> Maybe (Term 'Transparent a)
forall a b. (a -> b) -> a -> b
$ [a] -> Term 'Transparent [a]
forall a (k :: TermKind). (Show a, Typeable a) => [a] -> Term k [a]
ListLit [a]
xs
maybeTransparentTerm (EmbeddedLit a
x) = Term 'Transparent a -> Maybe (Term 'Transparent a)
forall a. a -> Maybe a
Just (Term 'Transparent a -> Maybe (Term 'Transparent a))
-> Term 'Transparent a -> Maybe (Term 'Transparent a)
forall a b. (a -> b) -> a -> b
$ a -> Term 'Transparent (Embedded a)
forall a (k :: TermKind).
(Embeddable a, Typeable a, Show a) =>
a -> Term k (Embedded a)
EmbeddedLit a
x
maybeTransparentTerm (BoolLit Bool
x) = Term 'Transparent a -> Maybe (Term 'Transparent a)
forall a. a -> Maybe a
Just (Term 'Transparent a -> Maybe (Term 'Transparent a))
-> Term 'Transparent a -> Maybe (Term 'Transparent a)
forall a b. (a -> b) -> a -> b
$ Bool -> Term 'Transparent Bool
forall (k :: TermKind). Bool -> Term k Bool
BoolLit Bool
x
maybeTransparentTerm (Current e a
x Int
n) = Term 'Transparent a -> Maybe (Term 'Transparent a)
forall a. a -> Maybe a
Just (Term 'Transparent a -> Maybe (Term 'Transparent a))
-> Term 'Transparent a -> Maybe (Term 'Transparent a)
forall a b. (a -> b) -> a -> b
$ e a -> Int -> Term 'Transparent a
forall (a :: * -> *) a (k :: TermKind).
VarExp a =>
a a -> Int -> Term k a
Current e a
x Int
n
maybeTransparentTerm (All e a
x Int
n) = Term 'Transparent a -> Maybe (Term 'Transparent a)
forall a. a -> Maybe a
Just (Term 'Transparent a -> Maybe (Term 'Transparent a))
-> Term 'Transparent a -> Maybe (Term 'Transparent a)
forall a b. (a -> b) -> a -> b
$ e a -> Int -> Term 'Transparent [a]
forall a (e :: * -> *) (k :: TermKind).
(Typeable a, VarExp e) =>
e a -> Int -> Term k [a]
All e a
x Int
n

castTerm :: forall {k} a. Typeable a => SomeTerm k -> Maybe (Term k a)
castTerm :: forall {k :: TermKind} a.
Typeable a =>
SomeTerm k -> Maybe (Term k a)
castTerm (SomeTerm (Term k a
t :: Term k 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' @b (((a :~~: a) -> Maybe (Term k a)) -> Case a (Maybe (Term k a)))
-> ((a :~~: a) -> Maybe (Term k a)) -> Case a (Maybe (Term k a))
forall a b. (a -> b) -> a -> b
$ \a :~~: a
HRefl -> Term k a -> Maybe (Term k a)
forall a. a -> Maybe a
Just Term k a
Term k a
t
    , Maybe (Term k a) -> Case a (Maybe (Term k a))
forall {k} r (x :: k). r -> Case x r
fallbackCase' Maybe (Term k a)
forall a. Maybe a
Nothing
    ]

-- simple instance lifting based on Expr's instances
instance Typeable a => Show (Term k a) where
  show :: Term k a -> String
show = Expr -> String
forall a. Show a => a -> String
show (Expr -> String) -> (Term k a -> Expr) -> Term k a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term k a -> Expr
forall a (k :: TermKind). Typeable a => Term k a -> Expr
toExpr

instance Typeable a => Eq (Term k a) where
  == :: Term k a -> Term k a -> Bool
(==) = Expr -> Expr -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Expr -> Expr -> Bool)
-> (Term k a -> Expr) -> Term k a -> Term k a -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Term k a -> Expr
forall a (k :: TermKind). Typeable a => Term k a -> Expr
toExpr

instance Typeable a => Ord (Term k a) where
  compare :: Term k a -> Term k a -> Ordering
compare = Expr -> Expr -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Expr -> Expr -> Ordering)
-> (Term k a -> Expr) -> Term k a -> Term k a -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Term k a -> Expr
forall a (k :: TermKind). Typeable a => Term k a -> Expr
toExpr

compareK :: Typeable a => Term k1 a -> Term k2 a -> Ordering
compareK :: forall a (k1 :: TermKind) (k2 :: TermKind).
Typeable a =>
Term k1 a -> Term k2 a -> Ordering
compareK Term k1 a
x Term k2 a
y = Expr -> Expr -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Term k1 a -> Expr
forall a (k :: TermKind). Typeable a => Term k a -> Expr
toExpr Term k1 a
x) (Term k2 a -> Expr
forall a (k :: TermKind). Typeable a => Term k a -> Expr
toExpr Term k2 a
y)

currentE ::  forall e a. (VarExp e, Typeable a) => e a -> Int -> Expr
currentE :: forall (e :: * -> *) a.
(VarExp e, Typeable a) =>
e a -> Int -> Expr
currentE e a
x Int
n =
  String -> a -> Expr
forall a. Typeable a => String -> a -> Expr
Data.Express.var
    (String
"[" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ((Var a -> String) -> [Var a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Var a -> String
forall a. Var a -> String
varname ([Var a] -> [String]) -> [Var a] -> [String]
forall a b. (a -> b) -> a -> b
$ e a -> [Var a]
forall a. e a -> [Var a]
forall (e :: * -> *) a. VarExp e => e a -> [Var a]
toVarList e a
x) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]_C^" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n)
    (a
forall a. HasCallStack => a
undefined :: a)

allE :: forall e a. (VarExp e, Typeable a) => e a -> Int -> Expr
allE :: forall (e :: * -> *) a.
(VarExp e, Typeable a) =>
e a -> Int -> Expr
allE e a
x Int
n =
  String -> [a] -> Expr
forall a. Typeable a => String -> a -> Expr
Data.Express.var
    (String
"[" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ((Var a -> String) -> [Var a] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Var a -> String
forall a. Var a -> String
varname ([Var a] -> [String]) -> [Var a] -> [String]
forall a b. (a -> b) -> a -> b
$ e a -> [Var a]
forall a. e a -> [Var a]
forall (e :: * -> *) a. VarExp e => e a -> [Var a]
toVarList e a
x) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"]_A^" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n)
    ([a]
forall a. HasCallStack => a
undefined :: [a])

-- Assumption: each list in xss contains variables in ascending order
eval' :: Typeable a => Expr -> [[SomeVar]] -> ValueMap -> a
eval' :: forall a. Typeable a => Expr -> [[SomeVar]] -> ValueMap -> a
eval' Expr
expr [[SomeVar]]
xss ValueMap
e = Expr -> a
forall a. Typeable a => Expr -> a
evl (Expr -> a) -> (Expr -> Expr) -> Expr -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[SomeVar]] -> ValueMap -> Expr -> Expr
fillAVars [[SomeVar]]
xss ValueMap
e (Expr -> Expr) -> (Expr -> Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValueMap -> Expr -> Expr
reduceAVarsIndex ValueMap
e (Expr -> Expr) -> (Expr -> Expr) -> Expr -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ValueMap -> Expr -> Expr
replaceCVars ValueMap
e (Expr -> a) -> Expr -> a
forall a b. (a -> b) -> a -> b
$ Expr
expr

-- evaluation preprocessing

-- replace <var>_C^n with head(<var>_A^n)
replaceCVars :: ValueMap -> Expr -> Expr
replaceCVars :: ValueMap -> Expr -> Expr
replaceCVars ValueMap
m Expr
expr = Expr
expr Expr -> [(Expr, Expr)] -> Expr
//-
  [ (Expr
oldExpr, SomeTypeRep -> Expr
headF SomeTypeRep
ty Expr -> Expr -> Expr
:$ SomeConsistentVars
-> (forall a. Typeable a => [Var a] -> Expr) -> Expr
forall r.
SomeConsistentVars -> (forall a. Typeable a => [Var a] -> r) -> r
withSomeConsistentVars SomeConsistentVars
xs ((MergedVars a -> Int -> Expr
forall (e :: * -> *) a.
(VarExp e, Typeable a) =>
e a -> Int -> Expr
`allE` Int
n) (MergedVars a -> Expr)
-> ([Var a] -> MergedVars a) -> [Var a] -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Var a] -> MergedVars a
forall a. [Var a] -> MergedVars a
merge))
  | Just (Expr
oldExpr, (Int
n,[String]
x)) <- (Expr -> Maybe (Expr, (Int, [String])))
-> [Expr] -> [Maybe (Expr, (Int, [String]))]
forall a b. (a -> b) -> [a] -> [b]
map (AccessType -> Expr -> Maybe (Expr, (Int, [String]))
varStruct AccessType
C) (Expr -> [Expr]
vars Expr
expr)
  , SomeTypeRep
ty <- Maybe SomeTypeRep -> [SomeTypeRep]
forall a. Maybe a -> [a]
maybeToList (Maybe SomeTypeRep -> [SomeTypeRep])
-> Maybe SomeTypeRep -> [SomeTypeRep]
forall a b. (a -> b) -> a -> b
$ [String] -> ValueMap -> Maybe SomeTypeRep
varnameTypeRep [String]
x ValueMap
m
  , SomeConsistentVars
xs <- Maybe SomeConsistentVars -> [SomeConsistentVars]
forall a. Maybe a -> [a]
maybeToList (Maybe SomeConsistentVars -> [SomeConsistentVars])
-> Maybe SomeConsistentVars -> [SomeConsistentVars]
forall a b. (a -> b) -> a -> b
$ [String] -> ValueMap -> Maybe SomeConsistentVars
varnameVarList [String]
x ValueMap
m
  ]

-- given SomeTypeRep of a build Expr for head :: [a] -> a
headF :: SomeTypeRep -> Expr
headF :: SomeTypeRep -> Expr
headF (SomeTypeRep (TypeRep a
ta :: TypeRep (a :: k))) =
    TypeRep a -> (Typeable a => Expr) -> Expr
forall k (a :: k) r. TypeRep a -> (Typeable a => r) -> r
withTypeable TypeRep a
ta ((Typeable a => Expr) -> Expr) -> (Typeable a => Expr) -> Expr
forall a b. (a -> b) -> a -> b
$
      TypeRep k -> (Typeable k => Expr) -> Expr
forall k (a :: k) r. TypeRep a -> (Typeable a => r) -> r
withTypeable (TypeRep a -> TypeRep k
forall k (a :: k). TypeRep a -> TypeRep k
typeRepKind TypeRep a
ta) ((Typeable k => Expr) -> Expr) -> (Typeable k => Expr) -> Expr
forall a b. (a -> b) -> a -> b
$
        case TypeRep k -> TypeRep (*) -> Maybe (k :~~: *)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @k) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @Type) of
          Just k :~~: *
HRefl -> String -> ([a] -> a) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"head" ([a] -> a
forall a. HasCallStack => [a] -> a
head :: [a] -> a)
          Maybe (k :~~: *)
Nothing -> String -> Expr
forall a. HasCallStack => String -> a
error (String -> Expr) -> String -> Expr
forall a b. (a -> b) -> a -> b
$ String
"a does not have kind Type in TypeRep a, with a = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRep a -> String
forall a. Show a => a -> String
show (forall (a :: k). Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a)

-- replace <var>_A^n with reverse(tail^n(<var>_A^0))
reduceAVarsIndex :: ValueMap -> Expr -> Expr
reduceAVarsIndex :: ValueMap -> Expr -> Expr
reduceAVarsIndex ValueMap
m Expr
expr = Expr
expr Expr -> [(Expr, Expr)] -> Expr
//-
  [ (Expr
expr, SomeTypeRep -> Int -> Expr
tailF SomeTypeRep
ty Int
n Expr -> Expr -> Expr
:$ SomeConsistentVars
-> (forall a. Typeable a => [Var a] -> Expr) -> Expr
forall r.
SomeConsistentVars -> (forall a. Typeable a => [Var a] -> r) -> r
withSomeConsistentVars SomeConsistentVars
xs ((MergedVars a -> Int -> Expr
forall (e :: * -> *) a.
(VarExp e, Typeable a) =>
e a -> Int -> Expr
`allE` Int
0) (MergedVars a -> Expr)
-> ([Var a] -> MergedVars a) -> [Var a] -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Var a] -> MergedVars a
forall a. [Var a] -> MergedVars a
merge))
  | Just (Expr
expr, (Int
n,[String]
x)) <- (Expr -> Maybe (Expr, (Int, [String])))
-> [Expr] -> [Maybe (Expr, (Int, [String]))]
forall a b. (a -> b) -> [a] -> [b]
map (AccessType -> Expr -> Maybe (Expr, (Int, [String]))
varStruct AccessType
A) (Expr -> [Expr]
vars Expr
expr)
  , SomeTypeRep
ty <- Maybe SomeTypeRep -> [SomeTypeRep]
forall a. Maybe a -> [a]
maybeToList (Maybe SomeTypeRep -> [SomeTypeRep])
-> Maybe SomeTypeRep -> [SomeTypeRep]
forall a b. (a -> b) -> a -> b
$ [String] -> ValueMap -> Maybe SomeTypeRep
varnameTypeRep [String]
x ValueMap
m
  , SomeConsistentVars
xs <- Maybe SomeConsistentVars -> [SomeConsistentVars]
forall a. Maybe a -> [a]
maybeToList (Maybe SomeConsistentVars -> [SomeConsistentVars])
-> Maybe SomeConsistentVars -> [SomeConsistentVars]
forall a b. (a -> b) -> a -> b
$ [String] -> ValueMap -> Maybe SomeConsistentVars
varnameVarList [String]
x ValueMap
m
  ]

-- given SomeTypeRep of a build Expr for reverse . replicateF tail n :: [a] -> [a]
tailF :: SomeTypeRep -> Int -> Expr
tailF :: SomeTypeRep -> Int -> Expr
tailF (SomeTypeRep (TypeRep a
ta :: TypeRep (a :: k))) Int
n =
  TypeRep a -> (Typeable a => Expr) -> Expr
forall k (a :: k) r. TypeRep a -> (Typeable a => r) -> r
withTypeable TypeRep a
ta ((Typeable a => Expr) -> Expr) -> (Typeable a => Expr) -> Expr
forall a b. (a -> b) -> a -> b
$
    TypeRep k -> (Typeable k => Expr) -> Expr
forall k (a :: k) r. TypeRep a -> (Typeable a => r) -> r
withTypeable (TypeRep a -> TypeRep k
forall k (a :: k). TypeRep a -> TypeRep k
typeRepKind TypeRep a
ta) ((Typeable k => Expr) -> Expr) -> (Typeable k => Expr) -> Expr
forall a b. (a -> b) -> a -> b
$
      case TypeRep k -> TypeRep (*) -> Maybe (k :~~: *)
forall k1 k2 (a :: k1) (b :: k2).
TypeRep a -> TypeRep b -> Maybe (a :~~: b)
eqTypeRep (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @k) (forall a. Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @Type) of
        Just k :~~: *
HRefl -> String -> ([a] -> [a]) -> Expr
forall a. Typeable a => String -> a -> Expr
value (String
"tail^"String -> String -> String
forall a. [a] -> [a] -> [a]
++Int -> String
forall a. Show a => a -> String
show Int
n) ([a] -> [a]
forall a. [a] -> [a]
reverse ([a] -> [a]) -> ([a] -> [a]) -> [a] -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([a] -> [a]) -> Int -> [a] -> [a]
forall a. (a -> a) -> Int -> a -> a
replicateF [a] -> [a]
forall a. HasCallStack => [a] -> [a]
tail Int
n :: [a] -> [a])
        Maybe (k :~~: *)
Nothing -> String -> Expr
forall a. HasCallStack => String -> a
error (String -> Expr) -> String -> Expr
forall a b. (a -> b) -> a -> b
$ String
"a does not have kind Type in TypeRep a, with a = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ TypeRep a -> String
forall a. Show a => a -> String
show (forall (a :: k). Typeable a => TypeRep a
forall {k} (a :: k). Typeable a => TypeRep a
typeRep @a)

replicateF :: (a -> a) -> Int -> a -> a
replicateF :: forall a. (a -> a) -> Int -> a -> a
replicateF a -> a
f Int
n = ((a -> a) -> (a -> a) -> a -> a) -> (a -> a) -> [a -> a] -> a -> a
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (a -> a) -> (a -> a) -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) a -> a
forall a. a -> a
id ([a -> a] -> a -> a) -> [a -> a] -> a -> a
forall a b. (a -> b) -> a -> b
$ Int -> (a -> a) -> [a -> a]
forall a. Int -> a -> [a]
replicate Int
n a -> a
f

data AccessType = C | A deriving Int -> AccessType -> String -> String
[AccessType] -> String -> String
AccessType -> String
(Int -> AccessType -> String -> String)
-> (AccessType -> String)
-> ([AccessType] -> String -> String)
-> Show AccessType
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> AccessType -> String -> String
showsPrec :: Int -> AccessType -> String -> String
$cshow :: AccessType -> String
show :: AccessType -> String
$cshowList :: [AccessType] -> String -> String
showList :: [AccessType] -> String -> String
Show

varStruct :: AccessType -> Expr -> Maybe (Expr,(Int,[Varname]))
varStruct :: AccessType -> Expr -> Maybe (Expr, (Int, [String]))
varStruct AccessType
acc Expr
x
  | Expr -> Bool
isVar Expr
x = (ParseError -> Maybe (Expr, (Int, [String])))
-> ((Int, [String]) -> Maybe (Expr, (Int, [String])))
-> Either ParseError (Int, [String])
-> Maybe (Expr, (Int, [String]))
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe (Expr, (Int, [String]))
-> ParseError -> Maybe (Expr, (Int, [String]))
forall a b. a -> b -> a
const Maybe (Expr, (Int, [String]))
forall a. Maybe a
Nothing) ((Expr, (Int, [String])) -> Maybe (Expr, (Int, [String]))
forall a. a -> Maybe a
Just ((Expr, (Int, [String])) -> Maybe (Expr, (Int, [String])))
-> ((Int, [String]) -> (Expr, (Int, [String])))
-> (Int, [String])
-> Maybe (Expr, (Int, [String]))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Expr
x,)) (Either ParseError (Int, [String])
 -> Maybe (Expr, (Int, [String])))
-> Either ParseError (Int, [String])
-> Maybe (Expr, (Int, [String]))
forall a b. (a -> b) -> a -> b
$ Parsec String () (Int, [String])
-> String -> String -> Either ParseError (Int, [String])
forall s t a.
Stream s Identity t =>
Parsec s () a -> String -> s -> Either ParseError a
parse (AccessType -> Parsec String () (Int, [String])
varParser AccessType
acc) String
"" (Expr -> String
showExpr Expr
x)
  | Bool
otherwise = Maybe (Expr, (Int, [String]))
forall a. Maybe a
Nothing
  where
    varParser :: AccessType -> Parser (Int,[Varname]) -- parses a variable's string representation
    varParser :: AccessType -> Parsec String () (Int, [String])
varParser AccessType
acc = do
      Char
_ <- Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
'['
      [String]
xs <- ParsecT String () Identity String
-> ParsecT String () Identity Char
-> ParsecT String () Identity [String]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy1 (ParsecT String () Identity Char
-> ParsecT String () Identity String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many1 (ParsecT String () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
alphaNum ParsecT String () Identity Char
-> ParsecT String () Identity Char
-> ParsecT String () Identity Char
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
'_' ParsecT String () Identity Char
-> ParsecT String () Identity Char
-> ParsecT String () Identity Char
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
'\'')) (Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
',')
      Char
_ <- Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
']'
      String
_ <- String -> ParsecT String () Identity String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string (String
"_"String -> String -> String
forall a. [a] -> [a] -> [a]
++AccessType -> String
forall a. Show a => a -> String
show AccessType
accString -> String -> String
forall a. [a] -> [a] -> [a]
++String
"^")
      String
n <- ParsecT String () Identity Char
-> ParsecT String () Identity String
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many1 ParsecT String () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
digit
      (Int, [String]) -> Parsec String () (Int, [String])
forall a. a -> ParsecT String () Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Int
forall a. Read a => String -> a
read String
n,[String]
xs)

-- replace <var>_A^0 with values from variable environment
fillAVars :: [[SomeVar]] -> ValueMap -> Expr -> Expr
fillAVars :: [[SomeVar]] -> ValueMap -> Expr -> Expr
fillAVars [[SomeVar]]
xss ValueMap
e Expr
expr =
  Expr
expr Expr -> [(Expr, Expr)] -> Expr
//-
    [ (Expr
allExpr,Expr
xs')
    | [SomeVar]
someXs <- [[SomeVar]] -> [[SomeVar]]
forall a. Eq a => [a] -> [a]
nub [[SomeVar]]
xss
    , SomeConsistentVars
xs <- Maybe SomeConsistentVars -> [SomeConsistentVars]
forall a. Maybe a -> [a]
maybeToList (Maybe SomeConsistentVars -> [SomeConsistentVars])
-> Maybe SomeConsistentVars -> [SomeConsistentVars]
forall a b. (a -> b) -> a -> b
$ [SomeVar] -> Maybe SomeConsistentVars
someConsistentVars [SomeVar]
someXs
    , let xs' :: Expr
xs' = SomeConsistentVars
-> (forall a. Typeable a => [Var a] -> Expr) -> Expr
forall r.
SomeConsistentVars -> (forall a. Typeable a => [Var a] -> r) -> r
withSomeConsistentVars SomeConsistentVars
xs [Var a] -> Expr
forall a. Typeable a => [Var a] -> Expr
combinedVarsExpr
    , let allExpr :: Expr
allExpr = SomeConsistentVars
-> (forall a. Typeable a => [Var a] -> Expr) -> Expr
forall r.
SomeConsistentVars -> (forall a. Typeable a => [Var a] -> r) -> r
withSomeConsistentVars SomeConsistentVars
xs ((MergedVars a -> Int -> Expr
forall (e :: * -> *) a.
(VarExp e, Typeable a) =>
e a -> Int -> Expr
`allE` Int
0) (MergedVars a -> Expr)
-> ([Var a] -> MergedVars a) -> [Var a] -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Var a] -> MergedVars a
forall a. [Var a] -> MergedVars a
merge)
    ]
  where
    combinedVarsExpr :: Typeable a => [Var a] -> Expr
    combinedVarsExpr :: forall a. Typeable a => [Var a] -> Expr
combinedVarsExpr [Var a]
xs =
      let x :: ValueEntry
x = [Var a] -> ValueMap -> ValueEntry
forall a. Typeable a => [Var a] -> ValueMap -> ValueEntry
sortedEntries [Var a]
xs ValueMap
e
      in ValueEntry
-> Expr
-> (forall a. (Typeable a, Show a) => [(a, Int)] -> Expr)
-> Expr
forall r.
ValueEntry
-> r -> (forall a. (Typeable a, Show a) => [(a, Int)] -> r) -> r
withValueEntry ValueEntry
x (String -> Expr
forall a. HasCallStack => String -> a
error String
"fillAVars: something went wrong") ([a] -> Expr
forall a. (Typeable a, Show a) => a -> Expr
val ([a] -> Expr) -> ([(a, Int)] -> [a]) -> [(a, Int)] -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a, Int) -> a) -> [(a, Int)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (a, Int) -> a
forall a b. (a, b) -> a
fst)

toExpr :: Typeable a => Term k a -> Expr
toExpr :: forall a (k :: TermKind). Typeable a => Term k a -> Expr
toExpr (Add Term k a
x Term k a
y) = String -> (Integer -> Integer -> Integer) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"(+)" (Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(+) :: Integer -> Integer -> Integer) 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 a -> Expr
forall a (k :: TermKind). Typeable a => Term k a -> Expr
toExpr Term k a
y
toExpr (Sub Term k a
x Term k a
y) = String -> (Integer -> Integer -> Integer) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"(-)" ((-) :: Integer -> Integer -> Integer) 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 a -> Expr
forall a (k :: TermKind). Typeable a => Term k a -> Expr
toExpr Term k a
y
toExpr (Mul Term k a
x Term k a
y) = String -> (Integer -> Integer -> Integer) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"(*)" (Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
(*) :: Integer -> Integer -> Integer) 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 a -> Expr
forall a (k :: TermKind). Typeable a => Term k a -> Expr
toExpr Term k a
y
toExpr (Equals (Term k a
x :: Term k x) Term k a
y) = String -> (a -> a -> Bool) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"(==)" (a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==) :: x -> x -> Bool) 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 a -> Expr
forall a (k :: TermKind). Typeable a => Term k a -> Expr
toExpr Term k a
y
toExpr (Gt (Term k a
x :: Term k x) Term k a
y) = String -> (a -> a -> Bool) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"(>)" (a -> a -> Bool
forall a. Ord a => a -> a -> Bool
(>) :: x -> x -> Bool) 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 a -> Expr
forall a (k :: TermKind). Typeable a => Term k a -> Expr
toExpr Term k a
y
toExpr (Ge (Term k a
x :: Term k x) Term k a
y) = String -> (a -> a -> Bool) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"(>=)" (a -> a -> Bool
forall a. Ord a => a -> a -> Bool
(>=) :: x -> x -> Bool) 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 a -> Expr
forall a (k :: TermKind). Typeable a => Term k a -> Expr
toExpr Term k a
y
toExpr (Lt (Term k a
x :: Term k x) Term k a
y) = String -> (a -> a -> Bool) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"(<)" (a -> a -> Bool
forall a. Ord a => a -> a -> Bool
(<) :: x -> x -> Bool) 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 a -> Expr
forall a (k :: TermKind). Typeable a => Term k a -> Expr
toExpr Term k a
y
toExpr (Le (Term k a
x :: Term k x) Term k a
y) = String -> (a -> a -> Bool) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"(<=)" (a -> a -> Bool
forall a. Ord a => a -> a -> Bool
(<=) :: x -> x -> Bool) 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 a -> Expr
forall a (k :: TermKind). Typeable a => Term k a -> Expr
toExpr Term k a
y
toExpr (And Term k Bool
x Term k Bool
y) = String -> (Bool -> Bool -> Bool) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"(&&)" (Bool -> Bool -> Bool
(&&) :: Bool -> Bool -> Bool) Expr -> Expr -> Expr
:$ Term k Bool -> Expr
forall a (k :: TermKind). Typeable a => Term k a -> Expr
toExpr Term k Bool
x Expr -> Expr -> Expr
:$ Term k Bool -> Expr
forall a (k :: TermKind). Typeable a => Term k a -> Expr
toExpr Term k Bool
y
toExpr (Or Term k Bool
x Term k Bool
y) = String -> (Bool -> Bool -> Bool) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"(||)" (Bool -> Bool -> Bool
(||) :: Bool -> Bool -> Bool) Expr -> Expr -> Expr
:$ Term k Bool -> Expr
forall a (k :: TermKind). Typeable a => Term k a -> Expr
toExpr Term k Bool
x Expr -> Expr -> Expr
:$ Term k Bool -> Expr
forall a (k :: TermKind). Typeable a => Term k a -> Expr
toExpr Term k Bool
y
toExpr (IsIn (Term k a
x :: Term k x) Term k [a]
xs) = String -> (a -> [a] -> Bool) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"elem" (a -> [a] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem :: x -> [x] -> Bool) 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 [a] -> Expr
forall a (k :: TermKind). Typeable a => Term k a -> Expr
toExpr Term k [a]
xs
toExpr (Not Term k Bool
x) = String -> (Bool -> Bool) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"not" (Bool -> Bool
not :: Bool -> Bool) Expr -> Expr -> Expr
:$ Term k Bool -> Expr
forall a (k :: TermKind). Typeable a => Term k a -> Expr
toExpr Term k Bool
x
toExpr (Length (Term k [a]
xs :: Term k [b])) = String -> ([a] -> Integer) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"length" (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Integer) -> ([a] -> Int) -> [a] -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length :: [b] -> Integer) Expr -> Expr -> Expr
:$ Term k [a] -> Expr
forall a (k :: TermKind). Typeable a => Term k a -> Expr
toExpr Term k [a]
xs
toExpr (Reverse (Term k [a]
xs :: Term k [x])) = String -> ([a] -> [a]) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"reverse" ([a] -> [a]
forall a. [a] -> [a]
reverse :: [x] -> [x]) Expr -> Expr -> Expr
:$ Term k [a] -> Expr
forall a (k :: TermKind). Typeable a => Term k a -> Expr
toExpr Term k [a]
xs
toExpr (Sum Term k [a]
xs) = String -> ([Integer] -> Integer) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"sum" ([Integer] -> Integer
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum :: [Integer] -> Integer) Expr -> Expr -> Expr
:$ Term k [a] -> Expr
forall a (k :: TermKind). Typeable a => Term k a -> Expr
toExpr Term k [a]
xs
toExpr (Product Term k [a]
xs) = String -> ([Integer] -> Integer) -> Expr
forall a. Typeable a => String -> a -> Expr
value String
"product" ([Integer] -> Integer
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
product :: [Integer] -> Integer) Expr -> Expr -> Expr
:$ Term k [a] -> Expr
forall a (k :: TermKind). Typeable a => Term k a -> Expr
toExpr Term k [a]
xs
toExpr (IntLit Integer
x) = Integer -> Expr
forall a. (Typeable a, Show a) => a -> Expr
val Integer
x
toExpr (ListLit [a]
xs) = [a] -> Expr
forall a. (Typeable a, Show a) => a -> Expr
val [a]
xs
toExpr (EmbeddedLit (a
x :: x)) = forall a. (Typeable a, Show a) => a -> Expr
val @(Embedded x) (Integer -> Embedded a
forall a. (Show a, Embeddable a) => Integer -> Embedded a
Embedded (Integer -> Embedded a) -> Integer -> Embedded a
forall a b. (a -> b) -> a -> b
$ a -> Integer
forall a. Embeddable a => a -> Integer
asInteger a
x)
toExpr (BoolLit Bool
x) = Bool -> Expr
forall a. (Typeable a, Show a) => a -> Expr
val Bool
x
toExpr (Current e a
x Int
n) = e a -> Int -> Expr
forall (e :: * -> *) a.
(VarExp e, Typeable a) =>
e a -> Int -> Expr
currentE e a
x Int
n
toExpr (All e a
x Int
n) = e a -> Int -> Expr
forall (e :: * -> *) a.
(VarExp e, Typeable a) =>
e a -> Int -> Expr
allE e a
x Int
n
toExpr (Opaque Expr
expr [[SomeVar]]
_ [SomeTerm 'Transparent]
_) = Expr
expr