{-# 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 
-- Copyright   :  Copyright (c) 2016 the Hakaru team
-- License     :  BSD3
-- Stability   :  experimental
-- Portability :  GHC-only
--
-- Take strings from Maple and interpret them in Haskell (Hakaru),
-- in a type-safe way.
----------------------------------------------------------------
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

-- Maple prints errors with "cursors" (^) which point to the specific position
-- of the error on the line above. The derived show instance doesn't preserve
-- positioning of the cursor.
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 
  , MapleOptions nm -> Map String String
extraOpts :: 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 }

--------------------------------------------------------------------------------

-- | Maple commands operate on closed terms and take a single argument, and can
--   be applied under functions.
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

----------------------------------------------------------------
----------------------------------------------------------- fin.