Permalink
Browse files

Changed interface - TTM instead of Monad m

Ignore-this: 30f319d362597da8d0f1a03e55efae5d

darcs-hash:20090715114435-228f4-43595a0b748de9abd104a3103aea373d9fa4d21a.gz
  • Loading branch information...
1 parent 45428a7 commit 2f36338cc41ddd66b28cf334af0248dc86eeb40b eb committed Jul 15, 2009
Showing with 166 additions and 119 deletions.
  1. +18 −0 Ivor/Errors.lhs
  2. +2 −2 Ivor/Primitives.lhs
  3. +11 −11 Ivor/Shell.lhs
  4. +1 −1 Ivor/ShellState.lhs
  5. +132 −103 Ivor/TT.lhs
  6. +1 −1 ivor.cabal
  7. +1 −1 tests/Test.lhs
View
@@ -0,0 +1,18 @@
+> {-# OPTIONS_GHC -fglasgow-exts #-}
+
+> module Ivor.Errors where
+
+> import Ivor.TTCore
+> import Control.Monad.Error
+
+> data IError = ICantUnify (Indexed Name) (Indexed Name)
+> | IMessage String
+> deriving Show
+
+> instance Error IError where
+> noMsg = IMessage "Ivor Error"
+> strMsg s = IMessage s
+
+> type IvorM = Either IError
+
+> ifail = Left
View
@@ -58,7 +58,7 @@
> -- | Add primitive types for Int, Float and String, and some
> -- primitive operations [add,sub,mult,div][int,float] and concat.
-> addPrimitives :: Monad m => Context -> m Context
+> addPrimitives :: Context -> TTM Context
> addPrimitives c = do c <- addPrimitive c (name "Int")
> c <- addPrimitive c (name "Float")
> c <- addPrimitive c (name "String")
@@ -127,7 +127,7 @@
> parseInt = lexeme $ fmap read (many1 digit)
> -- | Parse a term including primitives
-> parsePrimTerm :: Monad m => String -> m ViewTerm
+> parsePrimTerm :: String -> TTM ViewTerm
> parsePrimTerm str
> = case parse (do t <- pTerm (Just parsePrimitives) ; eof ; return t)
> "(input)" str of
View
@@ -50,9 +50,8 @@
> newShell ctxt = Shell Nothing "> " False ctxt "" [] [] [] Nothing []
> -- | Update the context in a shell
-> updateShell :: Monad m =>
-> (Context -> m Context) -- ^ Function to update context
-> -> ShellState -> m ShellState
+> updateShell :: (Context -> TTM Context) -- ^ Function to update context
+> -> ShellState -> TTM ShellState
> updateShell fctxt (Shell r p f c resp tacs coms imp ext path)
> = do ctxt <- fctxt c
> return (Shell r p f ctxt resp tacs coms imp ext path)
@@ -96,7 +95,7 @@
output st = hPutStr (outputstream st)
outputLn st x = output st (x++"\n")
-> runCommand :: (Monad m) => Command -> ShellState -> m ShellState
+> runCommand :: Command -> ShellState -> TTM ShellState
> runCommand (Def nm tm) st = do let (_, tm') = addImplicit (context st) tm
> ctxt <- addDef (context st) (name nm) tm'
> return st { context = ctxt }
@@ -148,9 +147,9 @@
> return (respondLn st (show (whnf (context st) tm)))
> runCommand (Print n) st = do
> case (getDef (context st) (name n)) of
-> Just tm -> return (respondLn st (show (view tm)))
+> Right tm -> return (respondLn st (show (view tm)))
> _ -> case (getPatternDef (context st) (name n)) of
-> Just (_,pats) -> return (respondLn st (printPats pats))
+> Right (_,pats) -> return (respondLn st (printPats pats))
> _ -> do tm <- check (context st) n
> case view tm of
> (Name TypeCon _) -> return (respondLn st "Type constructor")
@@ -297,9 +296,10 @@ function which doesn't need to be in the IO Monad.
> (resp, ctxt) <- fn arg (context st)
> let st' = st { context = ctxt, response = resp }
> return st'
-> process x st = processInput x st
+> process x st = do let (Right r) = processInput x st
+> return r
-> processInput :: Monad m => Result Input -> ShellState -> m ShellState
+> processInput :: Result Input -> ShellState -> TTM ShellState
> processInput (Failure err) st = return $ respondLn st err
> processInput (Success (Command cmd)) st = runCommand cmd st
> processInput (Success (Tactic goal tac)) st
@@ -324,7 +324,7 @@ function which doesn't need to be in the IO Monad.
> where
> ctxt = context st
> showGoalState :: Goal -> String
-> showGoalState g = let (Just gd) = goalData ctxt True g
+> showGoalState g = let (Right gd) = goalData ctxt True g
> env = bindings gd
> ty = goalType gd
> nm = goalName gd in
@@ -365,7 +365,7 @@ function which doesn't need to be in the IO Monad.
> return st
> -- | Send a command directly to a shell
-> sendCommand :: Monad m => String -> ShellState -> m ShellState
+> sendCommand :: String -> ShellState -> TTM ShellState
> sendCommand str st = processInput
> (parseInput (extensions st)
> (gettacs (usertactics st))
@@ -383,7 +383,7 @@ Special case for importFile. Grr.
> (map fst (usercommands st)) str) $
> clearResponse st
-> gettacs :: [(String, String -> Goal -> Context -> IO Context)] -> [String]
+> gettacs :: [(String, String -> Goal -> Context -> TTM Context)] -> [String]
> gettacs = map fst
> -- | Get the install prefix of the library
View
@@ -23,7 +23,7 @@
> context :: !Context,
> -- | Get reply from last shell command
> response :: String,
-> usertactics :: forall m.Monad m => [(String, String -> Goal -> Context -> m Context)],
+> usertactics :: [(String, String -> Goal -> Context -> TTM Context)],
> usercommands :: [(String, String -> Context -> IO (String, Context))],
> imported :: [String],
> extensions :: Maybe (Parser ViewTerm),
Oops, something went wrong.

0 comments on commit 2f36338

Please sign in to comment.