{-# LANGUAGE CPP
, FlexibleInstances
, FlexibleContexts
, DeriveDataTypeable
, DataKinds
, ScopedTypeVariables
, RecordWildCards
, ViewPatterns
, LambdaCase
, KindSignatures
, TypeOperators
, GADTs
, RankNTypes
, DeriveFunctor, DeriveFoldable, DeriveTraversable
#-}
{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
module Language.Hakaru.Maple
( MapleException(..)
, MapleOptions(..)
, MapleCommand(MapleCommand)
, defaultMapleOptions
, sendToMaple, sendToMaple'
, maple
) where
import Control.Exception (Exception, throw)
import Control.Monad (when)
import Data.Typeable (Typeable)
import qualified Language.Hakaru.Pretty.Maple as Maple
import Language.Hakaru.Parser.Maple
import Language.Hakaru.Parser.AST (Name)
import Language.Hakaru.Pretty.Concrete (prettyType)
import qualified Language.Hakaru.Parser.SymbolResolve as SR
(resolveAST', fromVarSet)
import Language.Hakaru.Types.Sing
import Language.Hakaru.Types.DataKind
import Language.Hakaru.Syntax.ABT
import Language.Hakaru.Syntax.AST
import Language.Hakaru.Syntax.TypeCheck
import Language.Hakaru.Syntax.TypeOf
import Language.Hakaru.Syntax.IClasses
import Language.Hakaru.Evaluation.ConstantPropagation
import System.MapleSSH (maple)
import System.IO
import Data.Text (pack)
import qualified Data.Map as M
import Data.List (isInfixOf, intercalate)
import Data.Char (toLower)
import Data.Function (on)
import Data.Foldable (Foldable)
import Data.Traversable (Traversable)
#if __GLASGOW_HASKELL__ < 710
import Data.Monoid (mempty)
#endif
data MapleException
= MapleInterpreterException String String
| MapleInputTypeMismatch String String
| MapleUnknownCommand String
| MapleAmbiguousCommand String [String]
| MultipleErrors [MapleException]
deriving Typeable
instance Exception MapleException
instance Show MapleException where
show :: MapleException -> String
show (MapleInterpreterException String
toMaple_ String
fromMaple) =
String
"MapleException:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
fromMaple String -> ShowS
forall a. [a] -> [a] -> [a]
++
String
"\nafter sending to Maple:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
toMaple_
show (MapleInputTypeMismatch String
command String
ty) =
[String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat[String
"Maple command ", String
command, String
" does not take input of type ", String
ty]
show (MapleUnknownCommand String
command) =
[String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat[String
"Maple command ", String
command, String
" does not exist"]
show (MapleAmbiguousCommand String
str [String]
cmds) =
[String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ String
"Ambiguous command\n"
, String
str, String
" could refer to any of\n"
, String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," [String]
cmds ]
show (MultipleErrors [MapleException]
es) =
[String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ String
"Multiple errors" String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (MapleException -> String) -> [MapleException] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ((String
"\n\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++) ShowS -> (MapleException -> String) -> MapleException -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapleException -> String
forall a. Show a => a -> String
show) [MapleException]
es
data MapleOptions nm = MapleOptions
{ MapleOptions nm -> nm
command :: nm
, MapleOptions nm -> Bool
debug :: Bool
, MapleOptions nm -> Int
timelimit :: Int
, :: M.Map String String
, MapleOptions nm -> TransformCtx
context :: TransformCtx
} deriving (a -> MapleOptions b -> MapleOptions a
(a -> b) -> MapleOptions a -> MapleOptions b
(forall a b. (a -> b) -> MapleOptions a -> MapleOptions b)
-> (forall a b. a -> MapleOptions b -> MapleOptions a)
-> Functor MapleOptions
forall a b. a -> MapleOptions b -> MapleOptions a
forall a b. (a -> b) -> MapleOptions a -> MapleOptions b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> MapleOptions b -> MapleOptions a
$c<$ :: forall a b. a -> MapleOptions b -> MapleOptions a
fmap :: (a -> b) -> MapleOptions a -> MapleOptions b
$cfmap :: forall a b. (a -> b) -> MapleOptions a -> MapleOptions b
Functor, MapleOptions a -> Bool
(a -> m) -> MapleOptions a -> m
(a -> b -> b) -> b -> MapleOptions a -> b
(forall m. Monoid m => MapleOptions m -> m)
-> (forall m a. Monoid m => (a -> m) -> MapleOptions a -> m)
-> (forall m a. Monoid m => (a -> m) -> MapleOptions a -> m)
-> (forall a b. (a -> b -> b) -> b -> MapleOptions a -> b)
-> (forall a b. (a -> b -> b) -> b -> MapleOptions a -> b)
-> (forall b a. (b -> a -> b) -> b -> MapleOptions a -> b)
-> (forall b a. (b -> a -> b) -> b -> MapleOptions a -> b)
-> (forall a. (a -> a -> a) -> MapleOptions a -> a)
-> (forall a. (a -> a -> a) -> MapleOptions a -> a)
-> (forall a. MapleOptions a -> [a])
-> (forall a. MapleOptions a -> Bool)
-> (forall a. MapleOptions a -> Int)
-> (forall a. Eq a => a -> MapleOptions a -> Bool)
-> (forall a. Ord a => MapleOptions a -> a)
-> (forall a. Ord a => MapleOptions a -> a)
-> (forall a. Num a => MapleOptions a -> a)
-> (forall a. Num a => MapleOptions a -> a)
-> Foldable MapleOptions
forall a. Eq a => a -> MapleOptions a -> Bool
forall a. Num a => MapleOptions a -> a
forall a. Ord a => MapleOptions a -> a
forall m. Monoid m => MapleOptions m -> m
forall a. MapleOptions a -> Bool
forall a. MapleOptions a -> Int
forall a. MapleOptions a -> [a]
forall a. (a -> a -> a) -> MapleOptions a -> a
forall m a. Monoid m => (a -> m) -> MapleOptions a -> m
forall b a. (b -> a -> b) -> b -> MapleOptions a -> b
forall a b. (a -> b -> b) -> b -> MapleOptions a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
product :: MapleOptions a -> a
$cproduct :: forall a. Num a => MapleOptions a -> a
sum :: MapleOptions a -> a
$csum :: forall a. Num a => MapleOptions a -> a
minimum :: MapleOptions a -> a
$cminimum :: forall a. Ord a => MapleOptions a -> a
maximum :: MapleOptions a -> a
$cmaximum :: forall a. Ord a => MapleOptions a -> a
elem :: a -> MapleOptions a -> Bool
$celem :: forall a. Eq a => a -> MapleOptions a -> Bool
length :: MapleOptions a -> Int
$clength :: forall a. MapleOptions a -> Int
null :: MapleOptions a -> Bool
$cnull :: forall a. MapleOptions a -> Bool
toList :: MapleOptions a -> [a]
$ctoList :: forall a. MapleOptions a -> [a]
foldl1 :: (a -> a -> a) -> MapleOptions a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> MapleOptions a -> a
foldr1 :: (a -> a -> a) -> MapleOptions a -> a
$cfoldr1 :: forall a. (a -> a -> a) -> MapleOptions a -> a
foldl' :: (b -> a -> b) -> b -> MapleOptions a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> MapleOptions a -> b
foldl :: (b -> a -> b) -> b -> MapleOptions a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> MapleOptions a -> b
foldr' :: (a -> b -> b) -> b -> MapleOptions a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> MapleOptions a -> b
foldr :: (a -> b -> b) -> b -> MapleOptions a -> b
$cfoldr :: forall a b. (a -> b -> b) -> b -> MapleOptions a -> b
foldMap' :: (a -> m) -> MapleOptions a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> MapleOptions a -> m
foldMap :: (a -> m) -> MapleOptions a -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> MapleOptions a -> m
fold :: MapleOptions m -> m
$cfold :: forall m. Monoid m => MapleOptions m -> m
Foldable, Functor MapleOptions
Foldable MapleOptions
Functor MapleOptions
-> Foldable MapleOptions
-> (forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> MapleOptions a -> f (MapleOptions b))
-> (forall (f :: * -> *) a.
Applicative f =>
MapleOptions (f a) -> f (MapleOptions a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> MapleOptions a -> m (MapleOptions b))
-> (forall (m :: * -> *) a.
Monad m =>
MapleOptions (m a) -> m (MapleOptions a))
-> Traversable MapleOptions
(a -> f b) -> MapleOptions a -> f (MapleOptions b)
forall (t :: * -> *).
Functor t
-> Foldable t
-> (forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
MapleOptions (m a) -> m (MapleOptions a)
forall (f :: * -> *) a.
Applicative f =>
MapleOptions (f a) -> f (MapleOptions a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> MapleOptions a -> m (MapleOptions b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> MapleOptions a -> f (MapleOptions b)
sequence :: MapleOptions (m a) -> m (MapleOptions a)
$csequence :: forall (m :: * -> *) a.
Monad m =>
MapleOptions (m a) -> m (MapleOptions a)
mapM :: (a -> m b) -> MapleOptions a -> m (MapleOptions b)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> MapleOptions a -> m (MapleOptions b)
sequenceA :: MapleOptions (f a) -> f (MapleOptions a)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
MapleOptions (f a) -> f (MapleOptions a)
traverse :: (a -> f b) -> MapleOptions a -> f (MapleOptions b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> MapleOptions a -> f (MapleOptions b)
$cp2Traversable :: Foldable MapleOptions
$cp1Traversable :: Functor MapleOptions
Traversable)
defaultMapleOptions :: MapleOptions ()
defaultMapleOptions :: MapleOptions ()
defaultMapleOptions = MapleOptions :: forall nm.
nm
-> Bool
-> Int
-> Map String String
-> TransformCtx
-> MapleOptions nm
MapleOptions
{ command :: ()
command = ()
, debug :: Bool
debug = Bool
False
, timelimit :: Int
timelimit = Int
90
, extraOpts :: Map String String
extraOpts = Map String String
forall k a. Map k a
M.empty
, context :: TransformCtx
context = TransformCtx
forall a. Monoid a => a
mempty }
data MapleCommand (i :: Hakaru) (o :: Hakaru) where
MapleCommand :: !(Transform '[ '( '[], i ) ] o) -> MapleCommand i o
UnderFun :: !(MapleCommand i o) -> MapleCommand (x ':-> i) (x ':-> o)
typeOfMapleCommand :: MapleCommand i o -> Sing i -> Sing o
typeOfMapleCommand :: MapleCommand i o -> Sing i -> Sing o
typeOfMapleCommand (MapleCommand Transform '[ '( '[], i)] o
t) Sing i
i =
Transform '[ '( '[], i)] o -> SArgsSing '[ '( '[], i)] -> Sing o
forall (as :: [([Hakaru], Hakaru)]) (x :: Hakaru).
Transform as x -> SArgsSing as -> Sing x
typeOfTransform Transform '[ '( '[], i)] o
t (Lift1 () '[] -> Sing i -> Pointwise (Lift1 ()) Sing '[] i
forall k0 k1 (f :: k0 -> *) (x :: k0) (g :: k1 -> *) (y :: k1).
f x -> g y -> Pointwise f g x y
Pw (() -> Lift1 () '[]
forall k a (i :: k). a -> Lift1 a i
Lift1 ()) Sing i
i Pointwise (Lift1 ()) Sing '[] i
-> SArgs (Pointwise (Lift1 ()) Sing) '[]
-> SArgsSing '[ '( '[], i)]
forall (abt :: [Hakaru] -> Hakaru -> *) (vars :: [Hakaru])
(a :: Hakaru) (args :: [([Hakaru], Hakaru)]).
abt vars a -> SArgs abt args -> SArgs abt ('(vars, a) : args)
:* SArgs (Pointwise (Lift1 ()) Sing) '[]
forall (abt :: [Hakaru] -> Hakaru -> *). SArgs abt '[]
End)
typeOfMapleCommand (UnderFun MapleCommand i o
c) (SFun x i) =
Sing a -> Sing o -> Sing (a ':-> o)
forall (a :: Hakaru) (b :: Hakaru).
Sing a -> Sing b -> Sing (a ':-> b)
SFun Sing a
x (MapleCommand i o -> Sing i -> Sing o
forall (i :: Hakaru) (o :: Hakaru).
MapleCommand i o -> Sing i -> Sing o
typeOfMapleCommand MapleCommand i o
c Sing i
Sing b
i)
newtype CommandMatcher
= CommandMatcher (forall i . Sing i
-> Either MapleException (Some1 (MapleCommand i)))
infixl 3 <-|>
(<-|>) :: Either MapleException x
-> Either MapleException x
-> Either MapleException x
<-|> :: Either MapleException x
-> Either MapleException x -> Either MapleException x
(<-|>) (Left MapleException
x) (Left MapleException
y) =
MapleException -> Either MapleException x
forall a b. a -> Either a b
Left (MapleException -> Either MapleException x)
-> MapleException -> Either MapleException x
forall a b. (a -> b) -> a -> b
$ [MapleException] -> MapleException
MultipleErrors (MapleException -> [MapleException]
unnest MapleException
x [MapleException] -> [MapleException] -> [MapleException]
forall a. [a] -> [a] -> [a]
++ MapleException -> [MapleException]
unnest MapleException
y) where
unnest :: MapleException -> [MapleException]
unnest (MultipleErrors [MapleException]
e) = (MapleException -> [MapleException])
-> [MapleException] -> [MapleException]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap MapleException -> [MapleException]
unnest [MapleException]
e
unnest MapleException
e = [MapleException
e]
(<-|>) Left{} Either MapleException x
x = Either MapleException x
x
(<-|>) x :: Either MapleException x
x@Right{} Either MapleException x
_ = Either MapleException x
x
matchUnderFun :: CommandMatcher -> CommandMatcher
matchUnderFun :: CommandMatcher -> CommandMatcher
matchUnderFun (CommandMatcher forall (i :: Hakaru).
Sing i -> Either MapleException (Some1 (MapleCommand i))
k) = (forall (i :: Hakaru).
Sing i -> Either MapleException (Some1 (MapleCommand i)))
-> CommandMatcher
CommandMatcher forall (i :: Hakaru).
Sing i -> Either MapleException (Some1 (MapleCommand i))
go where
go :: Sing i -> Either MapleException (Some1 (MapleCommand i))
go :: Sing i -> Either MapleException (Some1 (MapleCommand i))
go ty :: Sing i
ty@(SFun _ i) =
(Some1 (MapleCommand b) -> Some1 (MapleCommand i))
-> Either MapleException (Some1 (MapleCommand b))
-> Either MapleException (Some1 (MapleCommand i))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\(Some1 MapleCommand b i
c) -> MapleCommand (a ':-> b) (a ':-> i)
-> Some1 (MapleCommand (a ':-> b))
forall k (a :: k -> *) (i :: k). a i -> Some1 a
Some1 (MapleCommand b i -> MapleCommand (a ':-> b) (a ':-> i)
forall (i :: Hakaru) (o :: Hakaru) (x :: Hakaru).
MapleCommand i o -> MapleCommand (x ':-> i) (x ':-> o)
UnderFun MapleCommand b i
c)) (Sing b -> Either MapleException (Some1 (MapleCommand b))
forall (i :: Hakaru).
Sing i -> Either MapleException (Some1 (MapleCommand i))
go Sing b
i) Either MapleException (Some1 (MapleCommand i))
-> Either MapleException (Some1 (MapleCommand i))
-> Either MapleException (Some1 (MapleCommand i))
forall x.
Either MapleException x
-> Either MapleException x -> Either MapleException x
<-|>
Sing i -> Either MapleException (Some1 (MapleCommand i))
forall (i :: Hakaru).
Sing i -> Either MapleException (Some1 (MapleCommand i))
k Sing i
ty
go Sing i
ty =
Sing i -> Either MapleException (Some1 (MapleCommand i))
forall (i :: Hakaru).
Sing i -> Either MapleException (Some1 (MapleCommand i))
k Sing i
ty Either MapleException (Some1 (MapleCommand i))
-> Either MapleException (Some1 (MapleCommand i))
-> Either MapleException (Some1 (MapleCommand i))
forall x.
Either MapleException x
-> Either MapleException x -> Either MapleException x
<-|>
MapleException -> Either MapleException (Some1 (MapleCommand i))
forall a b. a -> Either a b
Left (String -> String -> MapleException
MapleInputTypeMismatch String
"x -> y" (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ Int -> Sing i -> Doc
forall (a :: Hakaru). Int -> Sing a -> Doc
prettyType Int
0 Sing i
ty))
mapleCommands
:: [ (String, CommandMatcher) ]
mapleCommands :: [(String, CommandMatcher)]
mapleCommands =
[ (String
"Simplify"
, (forall (i :: Hakaru).
Sing i -> Either MapleException (Some1 (MapleCommand i)))
-> CommandMatcher
CommandMatcher ((forall (i :: Hakaru).
Sing i -> Either MapleException (Some1 (MapleCommand i)))
-> CommandMatcher)
-> (forall (i :: Hakaru).
Sing i -> Either MapleException (Some1 (MapleCommand i)))
-> CommandMatcher
forall a b. (a -> b) -> a -> b
$ \Sing i
_ -> Some1 (MapleCommand i)
-> Either MapleException (Some1 (MapleCommand i))
forall (m :: * -> *) a. Monad m => a -> m a
return (Some1 (MapleCommand i)
-> Either MapleException (Some1 (MapleCommand i)))
-> Some1 (MapleCommand i)
-> Either MapleException (Some1 (MapleCommand i))
forall a b. (a -> b) -> a -> b
$ MapleCommand i i -> Some1 (MapleCommand i)
forall k (a :: k -> *) (i :: k). a i -> Some1 a
Some1 (MapleCommand i i -> Some1 (MapleCommand i))
-> MapleCommand i i -> Some1 (MapleCommand i)
forall a b. (a -> b) -> a -> b
$ Transform '[ '( '[], i)] i -> MapleCommand i i
forall (i :: Hakaru) (o :: Hakaru).
Transform '[ '( '[], i)] o -> MapleCommand i o
MapleCommand Transform '[ '( '[], i)] i
forall (a :: Hakaru). Transform '[LC a] a
Simplify)
, (String
"Reparam"
, (forall (i :: Hakaru).
Sing i -> Either MapleException (Some1 (MapleCommand i)))
-> CommandMatcher
CommandMatcher ((forall (i :: Hakaru).
Sing i -> Either MapleException (Some1 (MapleCommand i)))
-> CommandMatcher)
-> (forall (i :: Hakaru).
Sing i -> Either MapleException (Some1 (MapleCommand i)))
-> CommandMatcher
forall a b. (a -> b) -> a -> b
$ \Sing i
_ -> Some1 (MapleCommand i)
-> Either MapleException (Some1 (MapleCommand i))
forall (m :: * -> *) a. Monad m => a -> m a
return (Some1 (MapleCommand i)
-> Either MapleException (Some1 (MapleCommand i)))
-> Some1 (MapleCommand i)
-> Either MapleException (Some1 (MapleCommand i))
forall a b. (a -> b) -> a -> b
$ MapleCommand i i -> Some1 (MapleCommand i)
forall k (a :: k -> *) (i :: k). a i -> Some1 a
Some1 (MapleCommand i i -> Some1 (MapleCommand i))
-> MapleCommand i i -> Some1 (MapleCommand i)
forall a b. (a -> b) -> a -> b
$ Transform '[ '( '[], i)] i -> MapleCommand i i
forall (i :: Hakaru) (o :: Hakaru).
Transform '[ '( '[], i)] o -> MapleCommand i o
MapleCommand Transform '[ '( '[], i)] i
forall (a :: Hakaru). Transform '[LC a] a
Reparam)
, (String
"Summarize"
, (forall (i :: Hakaru).
Sing i -> Either MapleException (Some1 (MapleCommand i)))
-> CommandMatcher
CommandMatcher ((forall (i :: Hakaru).
Sing i -> Either MapleException (Some1 (MapleCommand i)))
-> CommandMatcher)
-> (forall (i :: Hakaru).
Sing i -> Either MapleException (Some1 (MapleCommand i)))
-> CommandMatcher
forall a b. (a -> b) -> a -> b
$ \Sing i
_ -> Some1 (MapleCommand i)
-> Either MapleException (Some1 (MapleCommand i))
forall (m :: * -> *) a. Monad m => a -> m a
return (Some1 (MapleCommand i)
-> Either MapleException (Some1 (MapleCommand i)))
-> Some1 (MapleCommand i)
-> Either MapleException (Some1 (MapleCommand i))
forall a b. (a -> b) -> a -> b
$ MapleCommand i i -> Some1 (MapleCommand i)
forall k (a :: k -> *) (i :: k). a i -> Some1 a
Some1 (MapleCommand i i -> Some1 (MapleCommand i))
-> MapleCommand i i -> Some1 (MapleCommand i)
forall a b. (a -> b) -> a -> b
$ Transform '[ '( '[], i)] i -> MapleCommand i i
forall (i :: Hakaru) (o :: Hakaru).
Transform '[ '( '[], i)] o -> MapleCommand i o
MapleCommand Transform '[ '( '[], i)] i
forall (a :: Hakaru). Transform '[LC a] a
Summarize)
, (String
"Disintegrate"
, CommandMatcher -> CommandMatcher
matchUnderFun (CommandMatcher -> CommandMatcher)
-> CommandMatcher -> CommandMatcher
forall a b. (a -> b) -> a -> b
$ (forall (i :: Hakaru).
Sing i -> Either MapleException (Some1 (MapleCommand i)))
-> CommandMatcher
CommandMatcher ((forall (i :: Hakaru).
Sing i -> Either MapleException (Some1 (MapleCommand i)))
-> CommandMatcher)
-> (forall (i :: Hakaru).
Sing i -> Either MapleException (Some1 (MapleCommand i)))
-> CommandMatcher
forall a b. (a -> b) -> a -> b
$ \Sing i
i ->
case Sing i
i of
SMeasure (SData (STyApp (STyApp
(STyCon (jmEq1 sSymbol_Pair -> Just Refl)) _) _) _) ->
Some1 (MapleCommand ('HMeasure (HPair b b)))
-> Either
MapleException (Some1 (MapleCommand ('HMeasure (HPair b b))))
forall (m :: * -> *) a. Monad m => a -> m a
return (Some1 (MapleCommand ('HMeasure (HPair b b)))
-> Either
MapleException (Some1 (MapleCommand ('HMeasure (HPair b b)))))
-> Some1 (MapleCommand ('HMeasure (HPair b b)))
-> Either
MapleException (Some1 (MapleCommand ('HMeasure (HPair b b))))
forall a b. (a -> b) -> a -> b
$ MapleCommand ('HMeasure (HPair b b)) (b ':-> 'HMeasure b)
-> Some1 (MapleCommand ('HMeasure (HPair b b)))
forall k (a :: k -> *) (i :: k). a i -> Some1 a
Some1 (MapleCommand ('HMeasure (HPair b b)) (b ':-> 'HMeasure b)
-> Some1 (MapleCommand ('HMeasure (HPair b b))))
-> MapleCommand ('HMeasure (HPair b b)) (b ':-> 'HMeasure b)
-> Some1 (MapleCommand ('HMeasure (HPair b b)))
forall a b. (a -> b) -> a -> b
$ Transform '[ '( '[], 'HMeasure (HPair b b))] (b ':-> 'HMeasure b)
-> MapleCommand ('HMeasure (HPair b b)) (b ':-> 'HMeasure b)
forall (i :: Hakaru) (o :: Hakaru).
Transform '[ '( '[], i)] o -> MapleCommand i o
MapleCommand (Transform '[ '( '[], 'HMeasure (HPair b b))] (b ':-> 'HMeasure b)
-> MapleCommand ('HMeasure (HPair b b)) (b ':-> 'HMeasure b))
-> Transform
'[ '( '[], 'HMeasure (HPair b b))] (b ':-> 'HMeasure b)
-> MapleCommand ('HMeasure (HPair b b)) (b ':-> 'HMeasure b)
forall a b. (a -> b) -> a -> b
$ TransformImpl
-> Transform
'[ '( '[], 'HMeasure (HPair b b))] (b ':-> 'HMeasure b)
forall (a :: Hakaru) (b :: Hakaru).
TransformImpl
-> Transform '[LC ('HMeasure (HPair a b))] (a ':-> 'HMeasure b)
Disint TransformImpl
InMaple
Sing i
_ -> MapleException -> Either MapleException (Some1 (MapleCommand i))
forall a b. a -> Either a b
Left (MapleException -> Either MapleException (Some1 (MapleCommand i)))
-> MapleException -> Either MapleException (Some1 (MapleCommand i))
forall a b. (a -> b) -> a -> b
$
String -> String -> MapleException
MapleInputTypeMismatch String
"measure (pair (a,b))"
(Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ Int -> Sing i -> Doc
forall (a :: Hakaru). Int -> Sing a -> Doc
prettyType Int
0 Sing i
i))
]
matchCommandName :: String -> Sing i
-> Either MapleException (Some1 (MapleCommand i))
matchCommandName :: String -> Sing i -> Either MapleException (Some1 (MapleCommand i))
matchCommandName String
s Sing i
i =
case ((String, CommandMatcher) -> Bool)
-> [(String, CommandMatcher)] -> [(String, CommandMatcher)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((String -> String -> Bool
forall a. Eq a => [a] -> [a] -> Bool
isInfixOf (String -> String -> Bool) -> ShowS -> String -> String -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Char -> Char) -> ShowS
forall a b. (a -> b) -> [a] -> [b]
map Char -> Char
toLower) String
s (String -> Bool)
-> ((String, CommandMatcher) -> String)
-> (String, CommandMatcher)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, CommandMatcher) -> String
forall a b. (a, b) -> a
fst) [(String, CommandMatcher)]
mapleCommands of
[(String
_,CommandMatcher forall (i :: Hakaru).
Sing i -> Either MapleException (Some1 (MapleCommand i))
m)]
-> Sing i -> Either MapleException (Some1 (MapleCommand i))
forall (i :: Hakaru).
Sing i -> Either MapleException (Some1 (MapleCommand i))
m Sing i
i
[] -> MapleException -> Either MapleException (Some1 (MapleCommand i))
forall a b. a -> Either a b
Left (MapleException -> Either MapleException (Some1 (MapleCommand i)))
-> MapleException -> Either MapleException (Some1 (MapleCommand i))
forall a b. (a -> b) -> a -> b
$ String -> MapleException
MapleUnknownCommand String
s
[(String, CommandMatcher)]
cs -> MapleException -> Either MapleException (Some1 (MapleCommand i))
forall a b. a -> Either a b
Left (MapleException -> Either MapleException (Some1 (MapleCommand i)))
-> MapleException -> Either MapleException (Some1 (MapleCommand i))
forall a b. (a -> b) -> a -> b
$ String -> [String] -> MapleException
MapleAmbiguousCommand String
s (((String, CommandMatcher) -> String)
-> [(String, CommandMatcher)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, CommandMatcher) -> String
forall a b. (a, b) -> a
fst [(String, CommandMatcher)]
cs)
nameOfMapleCommand :: MapleCommand i o -> Either MapleException String
nameOfMapleCommand :: MapleCommand i o -> Either MapleException String
nameOfMapleCommand (MapleCommand Transform '[ '( '[], i)] o
t) = Transform '[ '( '[], i)] o -> Either MapleException String
forall (xs :: [([Hakaru], Hakaru)]) (x :: Hakaru).
Transform xs x -> Either MapleException String
nm Transform '[ '( '[], i)] o
t where
nm :: Transform xs x -> Either MapleException String
nm :: Transform xs x -> Either MapleException String
nm Transform xs x
Simplify = String -> Either MapleException String
forall a b. b -> Either a b
Right String
"Simplify"
nm (Disint TransformImpl
InMaple) = String -> Either MapleException String
forall a b. b -> Either a b
Right String
"Disintegrate"
nm Transform xs x
Summarize = String -> Either MapleException String
forall a b. b -> Either a b
Right String
"Summarize"
nm Transform xs x
Reparam = String -> Either MapleException String
forall a b. b -> Either a b
Right String
"Reparam"
nm Transform xs x
tt = MapleException -> Either MapleException String
forall a b. a -> Either a b
Left (MapleException -> Either MapleException String)
-> MapleException -> Either MapleException String
forall a b. (a -> b) -> a -> b
$ String -> MapleException
MapleUnknownCommand (Transform xs x -> String
forall a. Show a => a -> String
show Transform xs x
tt)
nameOfMapleCommand (UnderFun MapleCommand i o
c) = MapleCommand i o -> Either MapleException String
forall (i :: Hakaru) (o :: Hakaru).
MapleCommand i o -> Either MapleException String
nameOfMapleCommand MapleCommand i o
c
sendToMaple'
:: ABT Term (abt Term)
=> MapleOptions String
-> TypedAST (abt Term)
-> IO (TypedAST (abt Term))
sendToMaple' :: MapleOptions String
-> TypedAST (abt Term) -> IO (TypedAST (abt Term))
sendToMaple' o :: MapleOptions String
o@MapleOptions{Bool
Int
String
Map String String
TransformCtx
context :: TransformCtx
extraOpts :: Map String String
timelimit :: Int
debug :: Bool
command :: String
context :: forall nm. MapleOptions nm -> TransformCtx
extraOpts :: forall nm. MapleOptions nm -> Map String String
timelimit :: forall a. MapleOptions a -> Int
debug :: forall a. MapleOptions a -> Bool
command :: forall nm. MapleOptions nm -> nm
..} (TypedAST Sing b
typ abt Term '[] b
term) = do
Some1 MapleCommand b i
cmdT <- (MapleException -> IO (Some1 (MapleCommand b)))
-> (Some1 (MapleCommand b) -> IO (Some1 (MapleCommand b)))
-> Either MapleException (Some1 (MapleCommand b))
-> IO (Some1 (MapleCommand b))
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either MapleException -> IO (Some1 (MapleCommand b))
forall a e. Exception e => e -> a
throw Some1 (MapleCommand b) -> IO (Some1 (MapleCommand b))
forall (m :: * -> *) a. Monad m => a -> m a
return (Either MapleException (Some1 (MapleCommand b))
-> IO (Some1 (MapleCommand b)))
-> Either MapleException (Some1 (MapleCommand b))
-> IO (Some1 (MapleCommand b))
forall a b. (a -> b) -> a -> b
$ String -> Sing b -> Either MapleException (Some1 (MapleCommand b))
forall (i :: Hakaru).
String -> Sing i -> Either MapleException (Some1 (MapleCommand i))
matchCommandName String
command Sing b
typ
abt Term '[] i
res <- MapleOptions (MapleCommand b i)
-> abt Term '[] b -> IO (abt Term '[] i)
forall (abt :: [Hakaru] -> Hakaru -> *) (i :: Hakaru)
(o :: Hakaru).
ABT Term abt =>
MapleOptions (MapleCommand i o) -> abt '[] i -> IO (abt '[] o)
sendToMaple MapleOptions String
o{command :: MapleCommand b i
command=MapleCommand b i
cmdT} abt Term '[] b
term
TypedAST (abt Term) -> IO (TypedAST (abt Term))
forall (m :: * -> *) a. Monad m => a -> m a
return (TypedAST (abt Term) -> IO (TypedAST (abt Term)))
-> TypedAST (abt Term) -> IO (TypedAST (abt Term))
forall a b. (a -> b) -> a -> b
$ Sing i -> abt Term '[] i -> TypedAST (abt Term)
forall (abt :: [Hakaru] -> Hakaru -> *) (b :: Hakaru).
Sing b -> abt '[] b -> TypedAST abt
TypedAST (abt Term '[] i -> Sing i
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt Term '[] i
res) abt Term '[] i
res
sendToMaple
:: (ABT Term abt)
=> MapleOptions (MapleCommand i o)
-> abt '[] i
-> IO (abt '[] o)
sendToMaple :: MapleOptions (MapleCommand i o) -> abt '[] i -> IO (abt '[] o)
sendToMaple MapleOptions{Bool
Int
Map String String
TransformCtx
MapleCommand i o
context :: TransformCtx
extraOpts :: Map String String
timelimit :: Int
debug :: Bool
command :: MapleCommand i o
context :: forall nm. MapleOptions nm -> TransformCtx
extraOpts :: forall nm. MapleOptions nm -> Map String String
timelimit :: forall a. MapleOptions a -> Int
debug :: forall a. MapleOptions a -> Bool
command :: forall nm. MapleOptions nm -> nm
..} abt '[] i
e = do
String
nm <- (MapleException -> IO String)
-> (String -> IO String)
-> Either MapleException String
-> IO String
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either MapleException -> IO String
forall a e. Exception e => e -> a
throw String -> IO String
forall (m :: * -> *) a. Monad m => a -> m a
return (Either MapleException String -> IO String)
-> Either MapleException String -> IO String
forall a b. (a -> b) -> a -> b
$ MapleCommand i o -> Either MapleException String
forall (i :: Hakaru) (o :: Hakaru).
MapleCommand i o -> Either MapleException String
nameOfMapleCommand MapleCommand i o
command
let typ_in :: Sing i
typ_in = abt '[] i -> Sing i
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> Sing a
typeOf abt '[] i
e
typ_out :: Sing o
typ_out = MapleCommand i o -> Sing i -> Sing o
forall (i :: Hakaru) (o :: Hakaru).
MapleCommand i o -> Sing i -> Sing o
typeOfMapleCommand MapleCommand i o
command Sing i
typ_in
optStr :: (String, String) -> String
optStr (String
k,String
v) = [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat[String
"_",String
k,String
"=",String
v]
optsStr :: String
optsStr =
String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate 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
optStr ([(String, String)] -> [String]) -> [(String, String)] -> [String]
forall a b. (a -> b) -> a -> b
$ Map String String -> [(String, String)]
forall k a. Map k a -> [(k, a)]
M.assocs (Map String String -> [(String, String)])
-> Map String String -> [(String, String)]
forall a b. (a -> b) -> a -> b
$
String -> String -> Map String String -> Map String String
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert String
"command" String
nm Map String String
extraOpts
toMaple_ :: String
toMaple_ = String
"use Hakaru, NewSLO in timelimit("
String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
timelimit String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", RoundTrip("
String -> ShowS
forall a. [a] -> [a] -> [a]
++ abt '[] i -> String
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> String
Maple.pretty abt '[] i
e String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Sing i -> ShowS
forall (a :: Hakaru). Sing a -> ShowS
Maple.mapleType Sing i
typ_in (String
", "
String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
optsStr String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")) end use;")
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
debug (Handle -> String -> IO ()
hPutStrLn Handle
stderr (String
"Sent to Maple:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
toMaple_))
String
fromMaple <- String -> IO String
maple String
toMaple_
case String
fromMaple of
Char
'_':Char
'I':Char
'n':Char
'e':Char
'r':Char
't':String
_ -> do
Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
debug (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
String
ret <- String -> IO String
maple (String
"FromInert(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
fromMaple String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")")
Handle -> String -> IO ()
hPutStrLn Handle
stderr (String
"Returning from Maple:\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
ret)
(String -> IO (abt '[] o))
-> (abt '[] o -> IO (abt '[] o))
-> Either String (abt '[] o)
-> IO (abt '[] o)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (MapleException -> IO (abt '[] o)
forall a e. Exception e => e -> a
throw (MapleException -> IO (abt '[] o))
-> (String -> MapleException) -> String -> IO (abt '[] o)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String -> MapleException
MapleInterpreterException String
toMaple_)
(abt '[] o -> IO (abt '[] o)
forall (m :: * -> *) a. Monad m => a -> m a
return (abt '[] o -> IO (abt '[] o))
-> (abt '[] o -> abt '[] o) -> abt '[] o -> IO (abt '[] o)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt '[] o -> abt '[] o
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> abt '[] a
constantPropagation) (Either String (abt '[] o) -> IO (abt '[] o))
-> Either String (abt '[] o) -> IO (abt '[] o)
forall a b. (a -> b) -> a -> b
$ do
InertExpr
past <- Either ParseError InertExpr -> Either String InertExpr
forall b c. Show b => Either b c -> Either String c
leftShow (Either ParseError InertExpr -> Either String InertExpr)
-> Either ParseError InertExpr -> Either String InertExpr
forall a b. (a -> b) -> a -> b
$ Text -> Either ParseError InertExpr
parseMaple (String -> Text
pack String
fromMaple)
let m :: TypeCheckMonad (abt '[] o)
m = Sing o -> AST -> TypeCheckMonad (abt '[] o)
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
Sing a -> AST -> TypeCheckMonad (abt '[] a)
checkType Sing o
typ_out
(Nat -> [Name] -> AST' Text -> AST
SR.resolveAST' (Nat -> Nat -> Nat
forall a. Ord a => a -> a -> a
max (abt '[] i -> Nat
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> Nat
nextFreeOrBind abt '[] i
e) (TransformCtx -> Nat
nextFreeVar TransformCtx
context))
(abt '[] i -> [Name]
forall (abt :: [Hakaru] -> Hakaru -> *) (a :: Hakaru).
ABT Term abt =>
abt '[] a -> [Name]
getNames abt '[] i
e) (InertExpr -> AST' Text
maple2AST InertExpr
past))
Either Text (abt '[] o) -> Either String (abt '[] o)
forall b c. Show b => Either b c -> Either String c
leftShow (Either Text (abt '[] o) -> Either String (abt '[] o))
-> Either Text (abt '[] o) -> Either String (abt '[] o)
forall a b. (a -> b) -> a -> b
$ TypeCheckMonad (abt '[] o)
-> Ctx -> Input -> TypeCheckMode -> Either Text (abt '[] o)
forall a.
TypeCheckMonad a -> Ctx -> Input -> TypeCheckMode -> Either Text a
unTCM TypeCheckMonad (abt '[] o)
m (abt '[] i -> Ctx
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> VarSet (KindOf a)
freeVars abt '[] i
e) Input
forall a. Maybe a
Nothing TypeCheckMode
UnsafeMode
String
_ -> MapleException -> IO (abt '[] o)
forall a e. Exception e => e -> a
throw (String -> String -> MapleException
MapleInterpreterException String
toMaple_ String
fromMaple)
leftShow :: forall b c. Show b => Either b c -> Either String c
leftShow :: Either b c -> Either String c
leftShow (Left b
err) = String -> Either String c
forall a b. a -> Either a b
Left (b -> String
forall a. Show a => a -> String
show b
err)
leftShow (Right c
x) = c -> Either String c
forall a b. b -> Either a b
Right c
x
getNames :: ABT Term abt => abt '[] a -> [Name]
getNames :: abt '[] a -> [Name]
getNames = Ctx -> [Name]
SR.fromVarSet (Ctx -> [Name]) -> (abt '[] a -> Ctx) -> abt '[] a -> [Name]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. abt '[] a -> Ctx
forall k (syn :: ([k] -> k -> *) -> k -> *) (abt :: [k] -> k -> *)
(xs :: [k]) (a :: k).
ABT syn abt =>
abt xs a -> VarSet (KindOf a)
freeVars