{-# LANGUAGE MultiParamTypeClasses
, OverloadedStrings
, FlexibleInstances
, FlexibleContexts
, ScopedTypeVariables
, CPP
, GADTs
, TypeFamilies
, DataKinds
, TypeOperators
#-}
{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
module Language.Hakaru.Pretty.Maple (pretty, mapleType) where
import qualified Data.Text as Text
import Data.Ratio
import Data.Number.Nat (fromNat)
import Data.Sequence (Seq)
import qualified Data.Foldable as F
import qualified Data.List.NonEmpty as L
import Control.Monad.State (MonadState(..), State, runState)
import Data.Maybe (isJust)
#if __GLASGOW_HASKELL__ < 710
import Control.Applicative (Applicative(..), (<$>))
#endif
import Language.Hakaru.Types.DataKind
import Language.Hakaru.Types.Sing
import Language.Hakaru.Syntax.AST
import Language.Hakaru.Syntax.Datum
import Language.Hakaru.Syntax.ABT
import Language.Hakaru.Syntax.IClasses
import Language.Hakaru.Expect
pretty :: (ABT Term abt) => abt '[] a -> String
pretty :: abt '[] a -> String
pretty = ((String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$[]) ((String -> String) -> String)
-> (abt '[] a -> String -> String) -> abt '[] a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LC_ abt a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
LC_ abt a -> String -> String
mapleAST (LC_ abt a -> String -> String)
-> (abt '[] a -> LC_ abt a) -> abt '[] a -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt '[] a -> LC_ abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> LC_ abt a
LC_
app1 :: (ABT Term abt) => String -> abt '[] a -> ShowS
app1 :: String -> abt '[] a -> String -> String
app1 String
fn abt '[] a
x = String -> (String -> String) -> String -> String
op1 String
fn (abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg abt '[] a
x)
{-# INLINE app1 #-}
app2 :: (ABT Term abt) => String -> abt '[] a -> abt '[] b -> ShowS
app2 :: String -> abt '[] a -> abt '[] b -> String -> String
app2 String
fn abt '[] a
x abt '[] b
y = String
-> (String -> String) -> (String -> String) -> String -> String
op2 String
fn (abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg abt '[] a
x) (abt '[] b -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg abt '[] b
y)
{-# INLINE app2 #-}
app3 :: (ABT Term abt)
=> String -> abt '[] a -> abt '[] b -> abt '[] c -> ShowS
app3 :: String -> abt '[] a -> abt '[] b -> abt '[] c -> String -> String
app3 String
fn abt '[] a
x abt '[] b
y abt '[] c
z = String
-> (String -> String)
-> (String -> String)
-> (String -> String)
-> String
-> String
op3 String
fn (abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg abt '[] a
x) (abt '[] b -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg abt '[] b
y) (abt '[] c -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg abt '[] c
z)
{-# INLINE app3 #-}
appN :: (ABT Term abt, Functor f, F.Foldable f)
=> String -> f (abt '[] a) -> ShowS
appN :: String -> f (abt '[] a) -> String -> String
appN String
fn f (abt '[] a)
xs = String -> f (String -> String) -> String -> String
forall (f :: * -> *).
Foldable f =>
String -> f (String -> String) -> String -> String
opN String
fn (abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg (abt '[] a -> String -> String)
-> f (abt '[] a) -> f (String -> String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (abt '[] a)
xs)
{-# INLINE appN #-}
op1 :: String -> ShowS -> ShowS
op1 :: String -> (String -> String) -> String -> String
op1 String
fn String -> String
x = String -> String -> String
showString String
fn (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String) -> String -> String
parens String -> String
x
{-# INLINE op1 #-}
op2 :: String -> ShowS -> ShowS -> ShowS
op2 :: String
-> (String -> String) -> (String -> String) -> String -> String
op2 String
fn String -> String
x String -> String
y = String -> String -> String
showString String
fn (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String) -> String -> String
parens (String -> String
x (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
showString String
", " (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
y)
{-# INLINE op2 #-}
op3 :: String -> ShowS -> ShowS -> ShowS -> ShowS
op3 :: String
-> (String -> String)
-> (String -> String)
-> (String -> String)
-> String
-> String
op3 String
fn String -> String
x String -> String
y String -> String
z
= String -> String -> String
showString String
fn
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String) -> String -> String
parens
( String -> String
x
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
showString String
", "
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
y
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
showString String
", "
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
z
)
{-# INLINE op3 #-}
opN :: F.Foldable f => String -> f ShowS -> ShowS
opN :: String -> f (String -> String) -> String -> String
opN String
fn f (String -> String)
xs = String -> String -> String
showString String
fn (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String) -> String -> String
parens (f (String -> String) -> String -> String
forall (f :: * -> *).
Foldable f =>
f (String -> String) -> String -> String
commaSep f (String -> String)
xs)
{-# INLINE opN #-}
meq :: (ABT Term abt) => abt '[] a -> abt '[] b -> ShowS
meq :: abt '[] a -> abt '[] b -> String -> String
meq abt '[] a
x abt '[] b
y = abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg abt '[] a
x (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> String -> String
showChar Char
'=' (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String) -> String -> String
parens (abt '[] b -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg abt '[] b
y)
{-# INLINE meq #-}
parens :: ShowS -> ShowS
parens :: (String -> String) -> String -> String
parens String -> String
a = Char -> String -> String
showChar Char
'(' (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
a (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> String -> String
showChar Char
')'
{-# INLINE parens #-}
brackets :: ShowS -> ShowS
brackets :: (String -> String) -> String -> String
brackets String -> String
a = Char -> String -> String
showChar Char
'[' (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
a (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> String -> String
showChar Char
']'
{-# INLINE brackets #-}
intercalate :: F.Foldable f => ShowS -> f ShowS -> ShowS
intercalate :: (String -> String) -> f (String -> String) -> String -> String
intercalate String -> String
sep = ((String -> String) -> (String -> String) -> String -> String)
-> f (String -> String) -> String -> String
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
F.foldr1 (\String -> String
a String -> String
b -> String -> String
a (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
sep (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
b)
{-# INLINE intercalate #-}
commaSep :: F.Foldable f => f ShowS -> ShowS
commaSep :: f (String -> String) -> String -> String
commaSep = (String -> String) -> f (String -> String) -> String -> String
forall (f :: * -> *).
Foldable f =>
(String -> String) -> f (String -> String) -> String -> String
intercalate (String -> String -> String
showString String
", ")
{-# INLINE commaSep #-}
mapleAST :: (ABT Term abt) => LC_ abt a -> ShowS
mapleAST :: LC_ abt a -> String -> String
mapleAST (LC_ abt '[] a
e) =
abt '[] a
-> (Variable a -> String -> String)
-> (Term abt a -> String -> String)
-> String
-> String
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k) r.
ABT syn abt =>
abt '[] a -> (Variable a -> r) -> (syn abt a -> r) -> r
caseVarSyn abt '[] a
e Variable a -> String -> String
forall (a :: Hakaru). Variable a -> String -> String
var1 ((Term abt a -> String -> String) -> String -> String)
-> (Term abt a -> String -> String) -> String -> String
forall a b. (a -> b) -> a -> b
$ \Term abt a
t ->
case Term abt a
t of
SCon args a
o :$ SArgs abt args
es -> SCon args a -> SArgs abt args -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *)
(args :: [([Hakaru], Hakaru)]) (a :: Hakaru).
ABT Term abt =>
SCon args a -> SArgs abt args -> String -> String
mapleSCon SCon args a
o SArgs abt args
es
NaryOp_ NaryOp a
op Seq (abt '[] a)
es -> NaryOp a -> Seq (abt '[] a) -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
NaryOp a -> Seq (abt '[] a) -> String -> String
mapleNary NaryOp a
op Seq (abt '[] a)
es
Literal_ Literal a
v -> Literal a -> String -> String
forall (a :: Hakaru). Literal a -> String -> String
mapleLiteral Literal a
v
Empty_ Sing ('HArray a)
_ -> (String -> String) -> String -> String
brackets String -> String
forall a. a -> a
id
Array_ abt '[] 'HNat
e1 abt '[ 'HNat] a
e2 ->
abt '[ 'HNat] a
-> (Variable 'HNat -> abt '[] a -> String -> String)
-> String
-> String
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(x :: k) (xs :: [k]) (a :: k) r.
ABT syn abt =>
abt (x : xs) a -> (Variable x -> abt xs a -> r) -> r
caseBind abt '[ 'HNat] a
e2 ((Variable 'HNat -> abt '[] a -> String -> String)
-> String -> String)
-> (Variable 'HNat -> abt '[] a -> String -> String)
-> String
-> String
forall a b. (a -> b) -> a -> b
$ \Variable 'HNat
x abt '[] a
e2' ->
String
-> abt '[] 'HNat -> abt '[] 'HNat -> abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru) (b :: Hakaru)
(c :: Hakaru).
ABT Term abt =>
String -> abt '[] a -> abt '[] b -> abt '[] c -> String -> String
app3 String
"ary" abt '[] 'HNat
e1 (Variable 'HNat -> abt '[] 'HNat
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var Variable 'HNat
x) abt '[] a
e2'
ArrayLiteral_ [abt '[] a]
es -> (String -> String) -> String -> String
brackets ([String -> String] -> String -> String
forall (f :: * -> *).
Foldable f =>
f (String -> String) -> String -> String
commaSep ((abt '[] a -> String -> String)
-> [abt '[] a] -> [String -> String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg [abt '[] a]
es))
Datum_ (Datum Text
"true" Sing (HData' t)
_typ (Inl DatumStruct xs (abt '[]) (HData' t)
Done) ) -> String -> String -> String
showString String
"true"
Datum_ (Datum Text
"false" Sing (HData' t)
_typ (Inr (Inl DatumStruct xs (abt '[]) (HData' t)
Done))) -> String -> String -> String
showString String
"false"
Datum_ Datum (abt '[]) (HData' t)
d -> Datum (abt '[]) (HData' t) -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (t :: Hakaru).
ABT Term abt =>
Datum (abt '[]) t -> String -> String
mapleDatum Datum (abt '[]) (HData' t)
d
Case_ abt '[] a
e' [Branch a abt a]
bs ->
String
-> (String -> String) -> (String -> String) -> String -> String
op2 String
"case" (abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg abt '[] a
e') (String -> [String -> String] -> String -> String
forall (f :: * -> *).
Foldable f =>
String -> f (String -> String) -> String -> String
opN String
"Branches" (Branch a abt a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
(b :: Hakaru).
ABT Term abt =>
Branch a abt b -> String -> String
mapleBranch (Branch a abt a -> String -> String)
-> [Branch a abt a] -> [String -> String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Branch a abt a]
bs))
Superpose_ NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
pms ->
String -> [String -> String] -> String -> String
forall (f :: * -> *).
Foldable f =>
String -> f (String -> String) -> String -> String
opN String
"Msum" ((abt '[] 'HProb -> abt '[] ('HMeasure a) -> String -> String)
-> (abt '[] 'HProb, abt '[] ('HMeasure a)) -> String -> String
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (String
-> abt '[] 'HProb -> abt '[] ('HMeasure a) -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
(b :: Hakaru).
ABT Term abt =>
String -> abt '[] a -> abt '[] b -> String -> String
app2 String
"Weight") ((abt '[] 'HProb, abt '[] ('HMeasure a)) -> String -> String)
-> [(abt '[] 'HProb, abt '[] ('HMeasure a))] -> [String -> String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
-> [(abt '[] 'HProb, abt '[] ('HMeasure a))]
forall a. NonEmpty a -> [a]
L.toList NonEmpty (abt '[] 'HProb, abt '[] ('HMeasure a))
pms)
Reject_ Sing ('HMeasure a)
_ -> String -> String -> String
showString String
"Msum()"
mapleLiteral :: Literal a -> ShowS
mapleLiteral :: Literal a -> String -> String
mapleLiteral (LNat Natural
v) = Natural -> String -> String
forall a. Show a => a -> String -> String
shows Natural
v
mapleLiteral (LInt Integer
v) = (String -> String) -> String -> String
parens (Integer -> String -> String
forall a. Show a => a -> String -> String
shows Integer
v)
mapleLiteral (LProb NonNegativeRational
v) = NonNegativeRational -> String -> String
forall a. (Integral a, Show a) => Ratio a -> String -> String
showsRational NonNegativeRational
v
mapleLiteral (LReal Rational
v) = Rational -> String -> String
forall a. (Integral a, Show a) => Ratio a -> String -> String
showsRational Rational
v
showsRational :: (Integral a, Show a) => Ratio a -> ShowS
showsRational :: Ratio a -> String -> String
showsRational Ratio a
a =
(String -> String) -> String -> String
parens
( a -> String -> String
forall a. Show a => a -> String -> String
shows (Ratio a -> a
forall a. Ratio a -> a
numerator Ratio a
a)
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> String -> String
showChar Char
'/'
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> String -> String
forall a. Show a => a -> String -> String
shows (Ratio a -> a
forall a. Ratio a -> a
denominator Ratio a
a)
)
var1 :: Variable (a :: Hakaru) -> ShowS
var1 :: Variable a -> String -> String
var1 Variable a
x | Text -> Bool
Text.null (Variable a -> Text
forall k (a :: k). Variable a -> Text
varHint Variable a
x) = Char -> String -> String
showChar Char
'x' (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> String -> String
forall a. Show a => a -> String -> String
shows (Int -> String -> String)
-> (Variable a -> Int) -> Variable a -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Nat -> Int
fromNat (Nat -> Int) -> (Variable a -> Nat) -> Variable a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Variable a -> Nat
forall k (a :: k). Variable a -> Nat
varID) Variable a
x
| Bool
otherwise = String -> String -> String
quoteName (String -> String -> String)
-> (Variable a -> String) -> Variable a -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
Text.unpack (Text -> String) -> (Variable a -> Text) -> Variable a -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Variable a -> Text
forall k (a :: k). Variable a -> Text
varHint (Variable a -> String -> String) -> Variable a -> String -> String
forall a b. (a -> b) -> a -> b
$ Variable a
x
quoteName :: String -> ShowS
quoteName :: String -> String -> String
quoteName String
s =
((String -> String) -> (String -> String) -> String -> String)
-> [String -> String] -> String -> String
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) ([String -> String] -> String -> String)
-> [String -> String] -> String -> String
forall a b. (a -> b) -> a -> b
$ (String -> String -> String) -> [String] -> [String -> String]
forall a b. (a -> b) -> [a] -> [b]
map String -> String -> String
showString
[String
"`", (Char -> String) -> String -> String
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Char -> String
quoteChar String
s, String
"`"]
where quoteChar :: Char -> String
quoteChar Char
'`' = String
"\\`"
quoteChar Char
'\\' = String
"\\\\"
quoteChar Char
c = [Char
c]
list1vars :: List1 Variable (vars :: [Hakaru]) -> [String]
list1vars :: List1 Variable vars -> [String]
list1vars List1 Variable vars
Nil1 = []
list1vars (Cons1 Variable x
x List1 Variable xs
xs) = Variable x -> String -> String
forall (a :: Hakaru). Variable a -> String -> String
var1 Variable x
x [] String -> [String] -> [String]
forall a. a -> [a] -> [a]
: List1 Variable xs -> [String]
forall (vars :: [Hakaru]). List1 Variable vars -> [String]
list1vars List1 Variable xs
xs
mapleSCon :: (ABT Term abt) => SCon args a -> SArgs abt args -> ShowS
mapleSCon :: SCon args a -> SArgs abt args -> String -> String
mapleSCon SCon args a
Lam_ = \(abt vars a
e1 :* SArgs abt args
End) ->
abt '[a] a
-> (Variable a -> abt '[] a -> String -> String)
-> String
-> String
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(x :: k) (xs :: [k]) (a :: k) r.
ABT syn abt =>
abt (x : xs) a -> (Variable x -> abt xs a -> r) -> r
caseBind abt vars a
abt '[a] a
e1 ((Variable a -> abt '[] a -> String -> String) -> String -> String)
-> (Variable a -> abt '[] a -> String -> String)
-> String
-> String
forall a b. (a -> b) -> a -> b
$ \Variable a
x abt '[] a
e1' ->
String
-> (String -> String)
-> (String -> String)
-> (String -> String)
-> String
-> String
op3 String
"lam" (Variable a -> String -> String
forall (a :: Hakaru). Variable a -> String -> String
var1 Variable a
x) (Sing a -> String -> String
forall (a :: Hakaru). Sing a -> String -> String
mapleType (Sing a -> String -> String) -> Sing a -> String -> String
forall a b. (a -> b) -> a -> b
$ Variable a -> Sing a
forall k (a :: k). Variable a -> Sing a
varType Variable a
x) (abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg abt '[] a
e1')
mapleSCon SCon args a
App_ = \(abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) -> String -> abt '[] a -> abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
(b :: Hakaru).
ABT Term abt =>
String -> abt '[] a -> abt '[] b -> String -> String
app2 String
"app" abt vars a
abt '[] a
e1 abt vars a
abt '[] a
e2
mapleSCon SCon args a
Let_ = \(abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) ->
abt '[a] a
-> (Variable a -> abt '[] a -> String -> String)
-> String
-> String
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(x :: k) (xs :: [k]) (a :: k) r.
ABT syn abt =>
abt (x : xs) a -> (Variable x -> abt xs a -> r) -> r
caseBind abt vars a
abt '[a] a
e2 ((Variable a -> abt '[] a -> String -> String) -> String -> String)
-> (Variable a -> abt '[] a -> String -> String)
-> String
-> String
forall a b. (a -> b) -> a -> b
$ \Variable a
x abt '[] a
e2' ->
String
-> (String -> String) -> (String -> String) -> String -> String
op2 String
"eval" (abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg abt '[] a
e2') (Variable a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var Variable a
x abt '[] a -> abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
(b :: Hakaru).
ABT Term abt =>
abt '[] a -> abt '[] b -> String -> String
`meq` abt vars a
abt '[] a
e1)
mapleSCon (CoerceTo_ Coercion a a
_) = \(abt vars a
e :* SArgs abt args
End) -> abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg abt vars a
abt '[] a
e
mapleSCon (UnsafeFrom_ Coercion a b
_) = \(abt vars a
e :* SArgs abt args
End) -> abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg abt vars a
abt '[] a
e
mapleSCon (PrimOp_ PrimOp typs a
o) = \SArgs abt args
es -> PrimOp typs a -> SArgs abt args -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (typs :: [Hakaru])
(args :: [([Hakaru], Hakaru)]) (a :: Hakaru).
(ABT Term abt, typs ~ UnLCs args, args ~ LCs typs) =>
PrimOp typs a -> SArgs abt args -> String -> String
maplePrimOp PrimOp typs a
o SArgs abt args
es
mapleSCon (ArrayOp_ ArrayOp typs a
o) = \SArgs abt args
es -> ArrayOp typs a -> SArgs abt args -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (typs :: [Hakaru])
(args :: [([Hakaru], Hakaru)]) (a :: Hakaru).
(ABT Term abt, typs ~ UnLCs args, args ~ LCs typs) =>
ArrayOp typs a -> SArgs abt args -> String -> String
mapleArrayOp ArrayOp typs a
o SArgs abt args
es
mapleSCon (MeasureOp_ MeasureOp typs a
o) = \SArgs abt args
es -> MeasureOp typs a -> SArgs abt args -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (typs :: [Hakaru])
(args :: [([Hakaru], Hakaru)]) (a :: Hakaru).
(ABT Term abt, typs ~ UnLCs args, args ~ LCs typs) =>
MeasureOp typs a -> SArgs abt args -> String -> String
mapleMeasureOp MeasureOp typs a
o SArgs abt args
es
mapleSCon SCon args a
Dirac = \(abt vars a
e1 :* SArgs abt args
End) -> String -> abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
String -> abt '[] a -> String -> String
app1 String
"Ret" abt vars a
abt '[] a
e1
mapleSCon SCon args a
MBind = \(abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) ->
abt '[a] a
-> (Variable a -> abt '[] a -> String -> String)
-> String
-> String
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(x :: k) (xs :: [k]) (a :: k) r.
ABT syn abt =>
abt (x : xs) a -> (Variable x -> abt xs a -> r) -> r
caseBind abt vars a
abt '[a] a
e2 ((Variable a -> abt '[] a -> String -> String) -> String -> String)
-> (Variable a -> abt '[] a -> String -> String)
-> String
-> String
forall a b. (a -> b) -> a -> b
$ \Variable a
x abt '[] a
e2' ->
String -> abt '[] a -> abt '[] a -> abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru) (b :: Hakaru)
(c :: Hakaru).
ABT Term abt =>
String -> abt '[] a -> abt '[] b -> abt '[] c -> String -> String
app3 String
"Bind" abt vars a
abt '[] a
e1 (Variable a -> abt '[] a
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var Variable a
x) abt '[] a
e2'
mapleSCon SCon args a
Plate = \(abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) ->
abt '[ 'HNat] a
-> (Variable 'HNat -> abt '[] a -> String -> String)
-> String
-> String
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(x :: k) (xs :: [k]) (a :: k) r.
ABT syn abt =>
abt (x : xs) a -> (Variable x -> abt xs a -> r) -> r
caseBind abt vars a
abt '[ 'HNat] a
e2 ((Variable 'HNat -> abt '[] a -> String -> String)
-> String -> String)
-> (Variable 'HNat -> abt '[] a -> String -> String)
-> String
-> String
forall a b. (a -> b) -> a -> b
$ \Variable 'HNat
x abt '[] a
e2' ->
String
-> abt '[] a -> abt '[] 'HNat -> abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru) (b :: Hakaru)
(c :: Hakaru).
ABT Term abt =>
String -> abt '[] a -> abt '[] b -> abt '[] c -> String -> String
app3 String
"Plate" abt vars a
abt '[] a
e1 (Variable 'HNat -> abt '[] 'HNat
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(a :: k).
ABT syn abt =>
Variable a -> abt '[] a
var Variable 'HNat
x) abt '[] a
e2'
mapleSCon SCon args a
Chain = \(abt vars a
e1 :* abt vars a
e2 :* abt vars a
e3 :* SArgs abt args
End) ->
String -> String -> String
forall a. HasCallStack => String -> a
error String
"TODO: mapleSCon{Chain}"
mapleSCon SCon args a
Integrate = \(abt vars a
e1 :* abt vars a
e2 :* abt vars a
e3 :* SArgs abt args
End) ->
abt '[ 'HReal] a
-> (Variable 'HReal -> abt '[] a -> String -> String)
-> String
-> String
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(x :: k) (xs :: [k]) (a :: k) r.
ABT syn abt =>
abt (x : xs) a -> (Variable x -> abt xs a -> r) -> r
caseBind abt vars a
abt '[ 'HReal] a
e3 ((Variable 'HReal -> abt '[] a -> String -> String)
-> String -> String)
-> (Variable 'HReal -> abt '[] a -> String -> String)
-> String
-> String
forall a b. (a -> b) -> a -> b
$ \Variable 'HReal
x abt '[] a
e3' ->
String -> String -> String
showString String
"Int("
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg abt '[] a
e3'
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
showString String
", ["
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Variable 'HReal -> String -> String
forall (a :: Hakaru). Variable a -> String -> String
var1 Variable 'HReal
x
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> String -> String
showChar Char
'='
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg abt vars a
abt '[] a
e1
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
showString String
".."
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg abt vars a
abt '[] a
e2
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
showString String
"])"
mapleSCon (Summate HDiscrete a
_ HSemiring a
_) = \(abt vars a
e1 :* abt vars a
e2 :* abt vars a
e3 :* SArgs abt args
End) ->
abt '[a] a
-> (Variable a -> abt '[] a -> String -> String)
-> String
-> String
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(x :: k) (xs :: [k]) (a :: k) r.
ABT syn abt =>
abt (x : xs) a -> (Variable x -> abt xs a -> r) -> r
caseBind abt vars a
abt '[a] a
e3 ((Variable a -> abt '[] a -> String -> String) -> String -> String)
-> (Variable a -> abt '[] a -> String -> String)
-> String
-> String
forall a b. (a -> b) -> a -> b
$ \Variable a
x abt '[] a
e3' ->
String -> String -> String
showString String
"Sum("
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg abt '[] a
e3'
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
showString String
", "
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Variable a -> String -> String
forall (a :: Hakaru). Variable a -> String -> String
var1 Variable a
x
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> String -> String
showChar Char
'='
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg abt vars a
abt '[] a
e1
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
showString String
"..("
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg abt vars a
abt '[] a
e2
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
showString String
")-1)"
mapleSCon (Product HDiscrete a
_ HSemiring a
_) = \(abt vars a
e1 :* abt vars a
e2 :* abt vars a
e3 :* SArgs abt args
End) ->
abt '[a] a
-> (Variable a -> abt '[] a -> String -> String)
-> String
-> String
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(x :: k) (xs :: [k]) (a :: k) r.
ABT syn abt =>
abt (x : xs) a -> (Variable x -> abt xs a -> r) -> r
caseBind abt vars a
abt '[a] a
e3 ((Variable a -> abt '[] a -> String -> String) -> String -> String)
-> (Variable a -> abt '[] a -> String -> String)
-> String
-> String
forall a b. (a -> b) -> a -> b
$ \Variable a
x abt '[] a
e3' ->
String -> String -> String
showString String
"Product("
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg abt '[] a
e3'
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
showString String
", "
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Variable a -> String -> String
forall (a :: Hakaru). Variable a -> String -> String
var1 Variable a
x
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Char -> String -> String
showChar Char
'='
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg abt vars a
abt '[] a
e1
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
showString String
"..("
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg abt vars a
abt '[] a
e2
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
showString String
")-1)"
mapleSCon (Transform_ Transform args a
t) = \SArgs abt args
_ -> String -> String -> String
forall a. HasCallStack => String -> a
error (String -> String -> String) -> String -> String -> String
forall a b. (a -> b) -> a -> b
$
[String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ String
"mapleSCon{", Transform args a -> String
forall a. Show a => a -> String
show Transform args a
t, String
"}"
, String
": Maple doesn't recognize transforms; expand them first" ]
mapleNary :: (ABT Term abt) => NaryOp a -> Seq (abt '[] a) -> ShowS
mapleNary :: NaryOp a -> Seq (abt '[] a) -> String -> String
mapleNary NaryOp a
And = String -> Seq (abt '[] a) -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (f :: * -> *)
(a :: Hakaru).
(ABT Term abt, Functor f, Foldable f) =>
String -> f (abt '[] a) -> String -> String
appN String
"And"
mapleNary NaryOp a
Or = String -> Seq (abt '[] a) -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (f :: * -> *)
(a :: Hakaru).
(ABT Term abt, Functor f, Foldable f) =>
String -> f (abt '[] a) -> String -> String
appN String
"Or"
mapleNary (Sum HSemiring a
_) = (String -> String) -> String -> String
parens ((String -> String) -> String -> String)
-> (Seq (abt '[] a) -> String -> String)
-> Seq (abt '[] a)
-> String
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String) -> Seq (String -> String) -> String -> String
forall (f :: * -> *).
Foldable f =>
(String -> String) -> f (String -> String) -> String -> String
intercalate (String -> String -> String
showString String
" + ") (Seq (String -> String) -> String -> String)
-> (Seq (abt '[] a) -> Seq (String -> String))
-> Seq (abt '[] a)
-> String
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (abt '[] a -> String -> String)
-> Seq (abt '[] a) -> Seq (String -> String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg
mapleNary (Prod HSemiring a
_) = (String -> String) -> String -> String
parens ((String -> String) -> String -> String)
-> (Seq (abt '[] a) -> String -> String)
-> Seq (abt '[] a)
-> String
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String) -> Seq (String -> String) -> String -> String
forall (f :: * -> *).
Foldable f =>
(String -> String) -> f (String -> String) -> String -> String
intercalate (String -> String -> String
showString String
" * ") (Seq (String -> String) -> String -> String)
-> (Seq (abt '[] a) -> Seq (String -> String))
-> Seq (abt '[] a)
-> String
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (abt '[] a -> String -> String)
-> Seq (abt '[] a) -> Seq (String -> String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg
mapleNary (Min HOrd a
_) = String -> Seq (abt '[] a) -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (f :: * -> *)
(a :: Hakaru).
(ABT Term abt, Functor f, Foldable f) =>
String -> f (abt '[] a) -> String -> String
appN String
"min"
mapleNary (Max HOrd a
_) = String -> Seq (abt '[] a) -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (f :: * -> *)
(a :: Hakaru).
(ABT Term abt, Functor f, Foldable f) =>
String -> f (abt '[] a) -> String -> String
appN String
"max"
mapleNary NaryOp a
op = String -> Seq (abt '[] a) -> String -> String
forall a. HasCallStack => String -> a
error (String -> Seq (abt '[] a) -> String -> String)
-> String -> Seq (abt '[] a) -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"TODO: mapleNary{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ NaryOp a -> String
forall a. Show a => a -> String
show NaryOp a
op String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}"
mapleDatum :: (ABT Term abt) => Datum (abt '[]) t -> ShowS
mapleDatum :: Datum (abt '[]) t -> String -> String
mapleDatum (Datum Text
hint Sing (HData' t)
_ DatumCode (Code t) (abt '[]) (HData' t)
d) =
String
-> (String -> String) -> (String -> String) -> String -> String
op2 String
"Datum"
(String -> String -> String
showString (Text -> String
Text.unpack Text
hint))
(DatumCode (Code t) (abt '[]) (HData' t) -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (xss :: [[HakaruFun]])
(a :: Hakaru).
ABT Term abt =>
DatumCode xss (abt '[]) a -> String -> String
mapleDatumCode DatumCode (Code t) (abt '[]) (HData' t)
d)
mapleDatumCode :: (ABT Term abt) => DatumCode xss (abt '[]) a -> ShowS
mapleDatumCode :: DatumCode xss (abt '[]) a -> String -> String
mapleDatumCode (Inr DatumCode xss (abt '[]) a
d) = String -> (String -> String) -> String -> String
op1 String
"Inr" (DatumCode xss (abt '[]) a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (xss :: [[HakaruFun]])
(a :: Hakaru).
ABT Term abt =>
DatumCode xss (abt '[]) a -> String -> String
mapleDatumCode DatumCode xss (abt '[]) a
d)
mapleDatumCode (Inl DatumStruct xs (abt '[]) a
d) = String -> (String -> String) -> String -> String
op1 String
"Inl" (DatumStruct xs (abt '[]) a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [HakaruFun])
(a :: Hakaru).
ABT Term abt =>
DatumStruct xs (abt '[]) a -> String -> String
mapleDatumStruct DatumStruct xs (abt '[]) a
d)
mapleDatumStruct :: (ABT Term abt) => DatumStruct xs (abt '[]) a -> ShowS
mapleDatumStruct :: DatumStruct xs (abt '[]) a -> String -> String
mapleDatumStruct DatumStruct xs (abt '[]) a
Done = String -> String -> String
showString String
"Done"
mapleDatumStruct (Et DatumFun x (abt '[]) a
d1 DatumStruct xs (abt '[]) a
d2) =
String
-> (String -> String) -> (String -> String) -> String -> String
op2 String
"Et" (DatumFun x (abt '[]) a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (x :: HakaruFun)
(a :: Hakaru).
ABT Term abt =>
DatumFun x (abt '[]) a -> String -> String
mapleDatumFun DatumFun x (abt '[]) a
d1) (DatumStruct xs (abt '[]) a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (xs :: [HakaruFun])
(a :: Hakaru).
ABT Term abt =>
DatumStruct xs (abt '[]) a -> String -> String
mapleDatumStruct DatumStruct xs (abt '[]) a
d2)
mapleDatumFun :: (ABT Term abt) => DatumFun x (abt '[]) a -> ShowS
mapleDatumFun :: DatumFun x (abt '[]) a -> String -> String
mapleDatumFun (Konst abt '[] b
a) = String -> abt '[] b -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
String -> abt '[] a -> String -> String
app1 String
"Konst" abt '[] b
a
mapleDatumFun (Ident abt '[] a
a) = String -> abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
String -> abt '[] a -> String -> String
app1 String
"Ident" abt '[] a
a
mapleBranch :: (ABT Term abt) => Branch a abt b -> ShowS
mapleBranch :: Branch a abt b -> String -> String
mapleBranch (Branch Pattern xs a
pat abt xs b
e) =
let (List1 Variable xs
vars, abt '[] b
e') = abt xs b -> (List1 Variable xs, abt '[] b)
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> (List1 Variable xs, abt '[] a)
caseBinds abt xs b
e
(String -> String
pat', [String]
vars') = State [String] (String -> String)
-> [String] -> (String -> String, [String])
forall s a. State s a -> s -> (a, s)
runState (Pattern xs a -> State [String] (String -> String)
forall (xs :: [Hakaru]) (a :: Hakaru).
Pattern xs a -> State [String] (String -> String)
maplePattern Pattern xs a
pat) (List1 Variable xs -> [String]
forall (vars :: [Hakaru]). List1 Variable vars -> [String]
list1vars List1 Variable xs
vars)
in
case [String]
vars' of
String
_:[String]
_ -> String -> String -> String
forall a. HasCallStack => String -> a
error String
"mapleBranch: didn't use all the variable names"
[] -> String
-> (String -> String) -> (String -> String) -> String -> String
op2 String
"Branch" String -> String
pat' (abt '[] b -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg abt '[] b
e')
maplePattern :: Pattern xs a -> State [String] ShowS
maplePattern :: Pattern xs a -> State [String] (String -> String)
maplePattern Pattern xs a
PWild = (String -> String) -> State [String] (String -> String)
forall (m :: * -> *) a. Monad m => a -> m a
return ((String -> String) -> State [String] (String -> String))
-> (String -> String) -> State [String] (String -> String)
forall a b. (a -> b) -> a -> b
$ String -> String -> String
showString String
"PWild"
maplePattern Pattern xs a
PVar = do
[String]
vs <- StateT [String] Identity [String]
forall s (m :: * -> *). MonadState s m => m s
get
case [String]
vs of
[] -> String -> State [String] (String -> String)
forall a. HasCallStack => String -> a
error String
"maplePattern: ran out of variable names"
String
v:[String]
vs' -> do
[String] -> StateT [String] Identity ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put [String]
vs'
(String -> String) -> State [String] (String -> String)
forall (m :: * -> *) a. Monad m => a -> m a
return ((String -> String) -> State [String] (String -> String))
-> (String -> String) -> State [String] (String -> String)
forall a b. (a -> b) -> a -> b
$ String -> (String -> String) -> String -> String
op1 String
"PVar" (String -> String -> String
showString String
v)
maplePattern (PDatum Text
hint PDatumCode (Code t) xs (HData' t)
pat) =
String
-> (String -> String) -> (String -> String) -> String -> String
op2 String
"PDatum" (String -> String -> String
showString (String -> String -> String) -> String -> String -> String
forall a b. (a -> b) -> a -> b
$ Text -> String
Text.unpack Text
hint) ((String -> String) -> String -> String)
-> State [String] (String -> String)
-> State [String] (String -> String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PDatumCode (Code t) xs (HData' t)
-> State [String] (String -> String)
forall (xss :: [[HakaruFun]]) (vars :: [Hakaru]) (a :: Hakaru).
PDatumCode xss vars a -> State [String] (String -> String)
maplePDatumCode PDatumCode (Code t) xs (HData' t)
pat
maplePDatumCode :: PDatumCode xss vars a -> State [String] ShowS
maplePDatumCode :: PDatumCode xss vars a -> State [String] (String -> String)
maplePDatumCode (PInr PDatumCode xss vars a
pat) = String -> (String -> String) -> String -> String
op1 String
"PInr" ((String -> String) -> String -> String)
-> State [String] (String -> String)
-> State [String] (String -> String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PDatumCode xss vars a -> State [String] (String -> String)
forall (xss :: [[HakaruFun]]) (vars :: [Hakaru]) (a :: Hakaru).
PDatumCode xss vars a -> State [String] (String -> String)
maplePDatumCode PDatumCode xss vars a
pat
maplePDatumCode (PInl PDatumStruct xs vars a
pat) = String -> (String -> String) -> String -> String
op1 String
"PInl" ((String -> String) -> String -> String)
-> State [String] (String -> String)
-> State [String] (String -> String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PDatumStruct xs vars a -> State [String] (String -> String)
forall (xs :: [HakaruFun]) (vars :: [Hakaru]) (a :: Hakaru).
PDatumStruct xs vars a -> State [String] (String -> String)
maplePDatumStruct PDatumStruct xs vars a
pat
maplePDatumStruct :: PDatumStruct xs vars a -> State [String] ShowS
maplePDatumStruct :: PDatumStruct xs vars a -> State [String] (String -> String)
maplePDatumStruct PDatumStruct xs vars a
PDone = (String -> String) -> State [String] (String -> String)
forall (m :: * -> *) a. Monad m => a -> m a
return ((String -> String) -> State [String] (String -> String))
-> (String -> String) -> State [String] (String -> String)
forall a b. (a -> b) -> a -> b
$ String -> String -> String
showString String
"PDone"
maplePDatumStruct (PEt PDatumFun x vars1 a
pat1 PDatumStruct xs vars2 a
pat2) =
String
-> (String -> String) -> (String -> String) -> String -> String
op2 String
"PEt"
((String -> String) -> (String -> String) -> String -> String)
-> State [String] (String -> String)
-> StateT
[String] Identity ((String -> String) -> String -> String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PDatumFun x vars1 a -> State [String] (String -> String)
forall (x :: HakaruFun) (vars :: [Hakaru]) (a :: Hakaru).
PDatumFun x vars a -> State [String] (String -> String)
maplePDatumFun PDatumFun x vars1 a
pat1
StateT [String] Identity ((String -> String) -> String -> String)
-> State [String] (String -> String)
-> State [String] (String -> String)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> PDatumStruct xs vars2 a -> State [String] (String -> String)
forall (xs :: [HakaruFun]) (vars :: [Hakaru]) (a :: Hakaru).
PDatumStruct xs vars a -> State [String] (String -> String)
maplePDatumStruct PDatumStruct xs vars2 a
pat2
maplePDatumFun :: PDatumFun x vars a -> State [String] ShowS
maplePDatumFun :: PDatumFun x vars a -> State [String] (String -> String)
maplePDatumFun (PKonst Pattern vars b
pat) = String -> (String -> String) -> String -> String
op1 String
"PKonst" ((String -> String) -> String -> String)
-> State [String] (String -> String)
-> State [String] (String -> String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern vars b -> State [String] (String -> String)
forall (xs :: [Hakaru]) (a :: Hakaru).
Pattern xs a -> State [String] (String -> String)
maplePattern Pattern vars b
pat
maplePDatumFun (PIdent Pattern vars a
pat) = String -> (String -> String) -> String -> String
op1 String
"PIdent" ((String -> String) -> String -> String)
-> State [String] (String -> String)
-> State [String] (String -> String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pattern vars a -> State [String] (String -> String)
forall (xs :: [Hakaru]) (a :: Hakaru).
Pattern xs a -> State [String] (String -> String)
maplePattern Pattern vars a
pat
arg :: (ABT Term abt) => abt '[] a -> ShowS
arg :: abt '[] a -> String -> String
arg = LC_ abt a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
LC_ abt a -> String -> String
mapleAST (LC_ abt a -> String -> String)
-> (abt '[] a -> LC_ abt a) -> abt '[] a -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt '[] a -> LC_ abt a
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
abt '[] a -> LC_ abt a
LC_
maplePrimOp
:: (ABT Term abt, typs ~ UnLCs args, args ~ LCs typs)
=> PrimOp typs a -> SArgs abt args -> ShowS
maplePrimOp :: PrimOp typs a -> SArgs abt args -> String -> String
maplePrimOp PrimOp typs a
Not (abt vars a
e1 :* SArgs abt args
End) = String -> abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
String -> abt '[] a -> String -> String
app1 String
"Not" abt vars a
abt '[] a
e1
maplePrimOp PrimOp typs a
Pi SArgs abt args
End = String -> String -> String
showString String
"Pi"
maplePrimOp PrimOp typs a
Cos (abt vars a
e1 :* SArgs abt args
End) = String -> abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
String -> abt '[] a -> String -> String
app1 String
"cos" abt vars a
abt '[] a
e1
maplePrimOp PrimOp typs a
Sin (abt vars a
e1 :* SArgs abt args
End) = String -> abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
String -> abt '[] a -> String -> String
app1 String
"sin" abt vars a
abt '[] a
e1
maplePrimOp PrimOp typs a
RealPow (abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) =
(String -> String) -> String -> String
parens (abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg abt vars a
abt '[] a
e1 (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
showString String
" ^ " (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg abt vars a
abt '[] a
e2)
maplePrimOp PrimOp typs a
Choose (abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) = String -> abt '[] a -> abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
(b :: Hakaru).
ABT Term abt =>
String -> abt '[] a -> abt '[] b -> String -> String
app2 String
"binomial" abt vars a
abt '[] a
e1 abt vars a
abt '[] a
e2
maplePrimOp PrimOp typs a
Exp (abt vars a
e1 :* SArgs abt args
End) = String -> abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
String -> abt '[] a -> String -> String
app1 String
"exp" abt vars a
abt '[] a
e1
maplePrimOp PrimOp typs a
Log (abt vars a
e1 :* SArgs abt args
End) = String -> abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
String -> abt '[] a -> String -> String
app1 String
"log" abt vars a
abt '[] a
e1
maplePrimOp (Infinity HIntegrable a
_) SArgs abt args
End = String -> String -> String
showString String
"infinity"
maplePrimOp PrimOp typs a
GammaFunc (abt vars a
e1 :* SArgs abt args
End) = String -> abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
String -> abt '[] a -> String -> String
app1 String
"GAMMA" abt vars a
abt '[] a
e1
maplePrimOp PrimOp typs a
BetaFunc (abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) = String -> abt '[] a -> abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
(b :: Hakaru).
ABT Term abt =>
String -> abt '[] a -> abt '[] b -> String -> String
app2 String
"Beta" abt vars a
abt '[] a
e1 abt vars a
abt '[] a
e2
maplePrimOp (Equal HEq a
_) (abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) =
(String -> String) -> String -> String
parens (abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg abt vars a
abt '[] a
e1 (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
showString String
" = " (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg abt vars a
abt '[] a
e2)
maplePrimOp (Less HOrd a
_) (abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) =
abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg abt vars a
abt '[] a
e1 (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
showString String
" < " (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg abt vars a
abt '[] a
e2
maplePrimOp (NatPow HSemiring a
_) (abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) =
(String -> String) -> String -> String
parens (abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg abt vars a
abt '[] a
e1 (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
showString String
" ^ " (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String -> String
arg abt vars a
abt '[] a
e2)
maplePrimOp (Negate HRing a
_) (abt vars a
e1 :* SArgs abt args
End) = (String -> String) -> String -> String
parens (String -> abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
String -> abt '[] a -> String -> String
app1 String
"-" abt vars a
abt '[] a
e1)
maplePrimOp (Abs HRing a
_) (abt vars a
e1 :* SArgs abt args
End) = String -> abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
String -> abt '[] a -> String -> String
app1 String
"abs" abt vars a
abt '[] a
e1
maplePrimOp (Recip HFractional a
_) (abt vars a
e1 :* SArgs abt args
End) = String -> abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
String -> abt '[] a -> String -> String
app1 String
"1/" abt vars a
abt '[] a
e1
maplePrimOp (NatRoot HRadical a
_) (abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) = String -> abt '[] a -> abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
(b :: Hakaru).
ABT Term abt =>
String -> abt '[] a -> abt '[] b -> String -> String
app2 String
"root" abt vars a
abt '[] a
e1 abt vars a
abt '[] a
e2
maplePrimOp PrimOp typs a
Floor (abt vars a
e1 :* SArgs abt args
End) = String -> abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
String -> abt '[] a -> String -> String
app1 String
"floor" abt vars a
abt '[] a
e1
maplePrimOp PrimOp typs a
x SArgs abt args
_ =
String -> String -> String
forall a. HasCallStack => String -> a
error (String -> String -> String) -> String -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"TODO: maplePrimOp{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ PrimOp typs a -> String
forall a. Show a => a -> String
show PrimOp typs a
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}"
mapleArrayOp
:: (ABT Term abt, typs ~ UnLCs args, args ~ LCs typs)
=> ArrayOp typs a -> SArgs abt args -> ShowS
mapleArrayOp :: ArrayOp typs a -> SArgs abt args -> String -> String
mapleArrayOp (Index Sing a
_) (abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) = String -> abt '[] a -> abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
(b :: Hakaru).
ABT Term abt =>
String -> abt '[] a -> abt '[] b -> String -> String
app2 String
"idx" abt vars a
abt '[] a
e1 abt vars a
abt '[] a
e2
mapleArrayOp (Size Sing a
_) (abt vars a
e1 :* SArgs abt args
End) = String -> abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
String -> abt '[] a -> String -> String
app1 String
"size" abt vars a
abt '[] a
e1
mapleArrayOp ArrayOp typs a
_ SArgs abt args
_ = String -> String -> String
forall a. HasCallStack => String -> a
error String
"TODO: mapleArrayOp{Reduce}"
mapleMeasureOp
:: (ABT Term abt, typs ~ UnLCs args, args ~ LCs typs)
=> MeasureOp typs a -> SArgs abt args -> ShowS
mapleMeasureOp :: MeasureOp typs a -> SArgs abt args -> String -> String
mapleMeasureOp MeasureOp typs a
Lebesgue = \(abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) -> String -> abt '[] a -> abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
(b :: Hakaru).
ABT Term abt =>
String -> abt '[] a -> abt '[] b -> String -> String
app2 String
"Lebesgue" abt vars a
abt '[] a
e1 abt vars a
abt '[] a
e2
mapleMeasureOp MeasureOp typs a
Counting = \SArgs abt args
End -> String -> String -> String
showString String
"Counting(-infinity,infinity)"
mapleMeasureOp MeasureOp typs a
Categorical = \(abt vars a
e1 :* SArgs abt args
End) -> String -> abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
String -> abt '[] a -> String -> String
app1 String
"Categorical" abt vars a
abt '[] a
e1
mapleMeasureOp MeasureOp typs a
Uniform = \(abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) -> String -> abt '[] a -> abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
(b :: Hakaru).
ABT Term abt =>
String -> abt '[] a -> abt '[] b -> String -> String
app2 String
"Uniform" abt vars a
abt '[] a
e1 abt vars a
abt '[] a
e2
mapleMeasureOp MeasureOp typs a
Normal = \(abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) -> String -> abt '[] a -> abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
(b :: Hakaru).
ABT Term abt =>
String -> abt '[] a -> abt '[] b -> String -> String
app2 String
"Gaussian" abt vars a
abt '[] a
e1 abt vars a
abt '[] a
e2
mapleMeasureOp MeasureOp typs a
Poisson = \(abt vars a
e1 :* SArgs abt args
End) -> String -> abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
String -> abt '[] a -> String -> String
app1 String
"PoissonD" abt vars a
abt '[] a
e1
mapleMeasureOp MeasureOp typs a
Gamma = \(abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) -> String -> abt '[] a -> abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
(b :: Hakaru).
ABT Term abt =>
String -> abt '[] a -> abt '[] b -> String -> String
app2 String
"GammaD" abt vars a
abt '[] a
e1 abt vars a
abt '[] a
e2
mapleMeasureOp MeasureOp typs a
Beta = \(abt vars a
e1 :* abt vars a
e2 :* SArgs abt args
End) -> String -> abt '[] a -> abt '[] a -> String -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru)
(b :: Hakaru).
ABT Term abt =>
String -> abt '[] a -> abt '[] b -> String -> String
app2 String
"BetaD" abt vars a
abt '[] a
e1 abt vars a
abt '[] a
e2
mapleType :: Sing (a :: Hakaru) -> ShowS
mapleType :: Sing a -> String -> String
mapleType Sing a
SNat = String -> String -> String
showString String
"HInt(Bound(`>=`,0))"
mapleType Sing a
SInt = String -> String -> String
showString String
"HInt()"
mapleType Sing a
SProb = String -> String -> String
showString String
"HReal(Bound(`>=`,0))"
mapleType Sing a
SReal = String -> String -> String
showString String
"HReal()"
mapleType (SFun a b) = String
-> (String -> String) -> (String -> String) -> String -> String
op2 String
"HFunction" (Sing a -> String -> String
forall (a :: Hakaru). Sing a -> String -> String
mapleType Sing a
a) (Sing b -> String -> String
forall (a :: Hakaru). Sing a -> String -> String
mapleType Sing b
b)
mapleType (SArray a) = String -> (String -> String) -> String -> String
op1 String
"HArray" (Sing a -> String -> String
forall (a :: Hakaru). Sing a -> String -> String
mapleType Sing a
a)
mapleType (SMeasure a) = String -> (String -> String) -> String -> String
op1 String
"HMeasure" (Sing a -> String -> String
forall (a :: Hakaru). Sing a -> String -> String
mapleType Sing a
a)
mapleType (SData (STyCon c `STyApp` _ `STyApp` _) (SPlus x SVoid))
| Maybe (TypeEq s "Pair") -> Bool
forall a. Maybe a -> Bool
isJust (Sing s -> Sing "Pair" -> Maybe (TypeEq s "Pair")
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing s
c Sing "Pair"
sSymbol_Pair)
= String -> String -> String
showString String
"HData(DatumStruct(pair,["
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing xs -> String -> String
forall (a :: [HakaruFun]). Sing a -> String -> String
mapleTypeDStruct Sing xs
x
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
showString String
"]))"
mapleType (SData (STyCon c) (SPlus SDone SVoid))
| Maybe (TypeEq s "Unit") -> Bool
forall a. Maybe a -> Bool
isJust (Sing s -> Sing "Unit" -> Maybe (TypeEq s "Unit")
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing s
c Sing "Unit"
sSymbol_Unit)
= String -> String -> String
showString String
"HData(DatumStruct(unit,[]))"
mapleType (SData (STyCon c) (SPlus SDone (SPlus SDone SVoid)))
| Maybe (TypeEq s "Bool") -> Bool
forall a. Maybe a -> Bool
isJust (Sing s -> Sing "Bool" -> Maybe (TypeEq s "Bool")
forall k (a :: k -> *) (i :: k) (j :: k).
JmEq1 a =>
a i -> a j -> Maybe (TypeEq i j)
jmEq1 Sing s
c Sing "Bool"
sSymbol_Bool)
= String -> String -> String
showString String
"HData(DatumStruct(true,[]),DatumStruct(false,[]))"
mapleType Sing a
x = String -> String -> String
forall a. HasCallStack => String -> a
error (String -> String -> String) -> String -> String -> String
forall a b. (a -> b) -> a -> b
$ String
"TODO: mapleType{" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Sing a -> String
forall a. Show a => a -> String
show Sing a
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"}"
mapleTypeDStruct :: Sing (a :: [HakaruFun]) -> ShowS
mapleTypeDStruct :: Sing a -> String -> String
mapleTypeDStruct Sing a
SDone = String -> String -> String
showString String
"NULL"
mapleTypeDStruct (SEt x xs) =
Sing x -> String -> String
forall (a :: HakaruFun). Sing a -> String -> String
mapleTypeDFun Sing x
x
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> String
showString String
","
(String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sing xs -> String -> String
forall (a :: [HakaruFun]). Sing a -> String -> String
mapleTypeDStruct Sing xs
xs
mapleTypeDFun :: Sing (a :: HakaruFun) -> ShowS
mapleTypeDFun :: Sing a -> String -> String
mapleTypeDFun (SKonst a) = String -> (String -> String) -> String -> String
op1 String
"Konst" (Sing a -> String -> String
forall (a :: Hakaru). Sing a -> String -> String
mapleType Sing a
a)
mapleTypeDFun Sing a
SIdent = String -> String -> String
showString String
"Ident"