Permalink
Browse files

Added IOvor

Shell with IO monad (built from primitive RealWorld type). However, it doesn't
actually work yet (gives up with <<loop>> exception).

darcs-hash:20070417154603-974a0-bfe6cdf6e3e3c156fd6aa95681a641945d86c81a.gz
  • Loading branch information...
1 parent 4cce076 commit 6c8845d934083169e14ea7a8af73377a34c0e548 eb committed Apr 17, 2007
Showing with 140 additions and 6 deletions.
  1. +69 −0 IOvor/IOPrims.lhs
  2. +25 −0 IOvor/Main.lhs
  3. +6 −0 IOvor/iobasics.tt
  4. +4 −4 Ivor/Nobby.lhs
  5. +24 −1 Ivor/TT.lhs
  6. +9 −1 Makefile
  7. +3 −0 TODO
View
@@ -0,0 +1,69 @@
+> module IOPrims where
+
+> import System.IO
+> import System.IO.Unsafe
+> import Data.Typeable
+> import Debug.Trace
+
+> import Ivor.Primitives
+> import Ivor.TT
+
+IO primitives; adds 'RealWorld' and 'Handle'
+
+RealWorld is a dummy type representing the world state, Handle (from
+System.IO) gives file handles.
+
+> data RealWorld = RW ()
+> deriving Eq
+
+> instance Show RealWorld where
+> show _ = "<<World>>"
+
+> rwName = name "RealWorld"
+
+> instance Typeable RealWorld where
+> typeOf (RW ()) = mkTyConApp (mkTyCon "RW") []
+
+> instance ViewConst RealWorld where
+> typeof x = rwName
+
+> instance ViewConst Handle where
+> typeof x = (name "Handle")
+
+> addIOPrimTypes :: Monad m => Context -> m Context
+> addIOPrimTypes c = do c <- addPrimitives c
+> c <- addPrimitive c rwName
+> c <- addPrimitive c (name "Handle")
+> c <- addExternalFn c (name "initWorld") 1 initWorld
+> "True -> RealWorld"
+> return c
+
+> addIOPrimFns :: Monad m => Context -> m Context
+> addIOPrimFns c = do c <- addBinFn c (name "putStr") doPutStr
+> "String -> (IO True)"
+> c <- addPrimFn c (name "getLine") doGetLine
+> "(IO String)"
+> return c
+
+Make an instance of IOResult from the result of an IO action and a
+value
+
+> mkIO :: () -> ViewTerm -> ViewTerm
+> mkIO t v = case (t,v) of -- make sure they get evaluated
+> (tr,val) -> apply (Name DataCon (name "ioResult"))
+> [Placeholder, Constant (RW tr), val]
+
+> trueVal = Name DataCon (name "II")
+
+> {-# NOINLINE doPutStr #-}
+> doPutStr :: String -> RealWorld -> ViewTerm
+> doPutStr str w = mkIO () trueVal -- (unsafePerformIO (putStr str)) trueVal
+
+> {-# NOINLINE doGetLine #-}
+> doGetLine :: RealWorld -> ViewTerm
+> doGetLine w = mkIO () (Constant "foo") -- (unsafePerformIO getLine))
+
+Needs a dummy argument so that evaluator doesn't loop
+
+> initWorld :: [ViewTerm] -> ViewTerm
+> initWorld [_] = Constant (RW ())
View
@@ -0,0 +1,25 @@
+> module Main where
+
+Jones the Steam, with IO primitives.
+Simple program for starting up an interactive shell with Ivor library.
+
+> import Ivor.TT
+> import Ivor.Shell
+> import Ivor.Primitives
+
+> import IOPrims
+
+> main :: IO ()
+> main = do let shell = addModulePath (newShell emptyContext)
+> (prefix ++ "/lib/ivor")
+> shell <- importFile "basics.tt" shell
+> primCtxt <- addIOPrimTypes (getContext shell)
+> let shell' = addModulePath (newShell primCtxt)
+> (prefix ++ "/lib/ivor")
+> shell' <- importFile "iobasics.tt" shell'
+> primFnCtxt <- addIOPrimFns (getContext shell')
+> -- It is horrible to have to do this every time. Fix the API!
+> let shell'' = addModulePath (newShell primFnCtxt)
+> (prefix ++ "/lib/ivor")
+> ctxt <- runShell "> " (extendParser shell'' parsePrimitives)
+> putStrLn "Finished"
View
@@ -0,0 +1,6 @@
+Data IOResult (A:*) :* where
+ ioResult : (world:RealWorld)(a:A)(IOResult A);
+
+IO = [A:*](RealWorld -> (IOResult A));
+
+world = initWorld II;
View
@@ -341,10 +341,10 @@ Do the actual evaluation
> Nothing -> (MB pat (Snoc sp v))
> Just v -> v
> | otherwise = MB pat (Snoc sp v)
-> app g (MB (BPrimOp e n, ty) sp) v =
-> case e (Snoc sp v) of
-> Nothing -> (MB (BPrimOp e n, ty) (Snoc sp v))
-> (Just v) -> v
+> app g (MB (BPrimOp e n, ty) sp) v
+> = case e (Snoc sp v) of
+> Nothing -> (MB (BPrimOp e n, ty) (Snoc sp v))
+> (Just v) -> v
> app g (MB (BCon tag n i, ty) sp) v
> | size (Snoc sp v) == i = (MR (RCon tag n (Snoc sp v)))
> | otherwise = (MB (BCon tag n i, ty) (Snoc sp v))
View
@@ -21,7 +21,7 @@
> -- * Definitions and Theorems
> addDef,addTypedDef,addData,addAxiom,declare,declareData,
> theorem,interactive,
-> addPrimitive,addBinOp,addPrimFn,addExternalFn,
+> addPrimitive,addBinOp,addBinFn,addPrimFn,addExternalFn,
> addEquality,forgetDef,addGenRec,
> -- * Pattern matching definitions
> PClause(..), Patterns(..),PattOpt(..),addPatternDef,
@@ -406,6 +406,29 @@
> Nothing -> Nothing
> mkfun _ = Nothing
+> -- | Add a new binary function on constants. Warning: The type you give
+> -- is not checked!
+> addBinFn :: (ViewConst a, ViewConst b, IsTerm ty, Monad m) =>
+> Context -> Name -> (a->b->ViewTerm) -> ty -> m Context
+> addBinFn (Ctxt st) n f tyin = do
+> checkNotExists n (defs st)
+> Term (ty, _) <- Ivor.TT.check (Ctxt st) tyin
+> let fndef = PrimOp mkfun
+> let Gam ctxt = defs st
+> -- let newdefs = Gam ((n,(G fndef ty)):ctxt)
+> newdefs <- gInsert n (G fndef ty defplicit) (Gam ctxt)
+> return $ Ctxt st { defs = newdefs }
+> where mkfun :: Spine Value -> Maybe Value
+> mkfun (Snoc (Snoc Empty (MR (RdConst x))) (MR (RdConst y)))
+> = case cast x of
+> Just x' -> case cast y of
+> Just y' -> case Ivor.TT.check (Ctxt st) $ f x' y' of
+> Just (Term (Ind v,_)) ->
+> Just $ nf (Gam []) (VG []) [] False v
+> Nothing -> Nothing
+> Nothing -> Nothing
+> mkfun _ = Nothing
+
> -- | Add a new primitive function on constants, usually used for converting
> -- to some form which can be examined in the type theory itself.
> -- Warning: The type you give is not checked!
View
@@ -33,9 +33,17 @@ jones: .PHONY package install
jones_install: jones
install Jones/jones $(PREFIX)/bin
+iovor: .PHONY package install
+ cd IOvor; ghc --make $(GHCOPTS) Main.lhs -o iovor -package ivor
+
+iovor_install: iovor
+ install IOvor/iovor $(PREFIX)/bin
+ install IOvor/iobasics.tt $(PREFIX)/lib/ivor
+
clean:
runhaskell Setup.lhs clean
- rm -f Jones/jones Main.o Main.hi
+ rm -f Jones/jones *.o *.hi
+ rm -f IOvor/iovor *.o *.hi
make -C tests clean
decruft:
View
3 TODO
@@ -1,5 +1,8 @@
Short term things to do:
+* Need an easier way of updating a context with an input file
+ (currently have to create a shell, then load, then create a new
+ shell if you want to modify the context further)
* Improve error messages!
* Recursive functions shouldn't reduce at type level.
* Either better than Monad m? Define an Error type.

0 comments on commit 6c8845d

Please sign in to comment.