Permalink
Browse files

Update Set to Type

  • Loading branch information...
1 parent ee21e2d commit db65516b87863fcc0b066d26cb262bcddfff5514 @edwinb committed Dec 11, 2012
Showing with 93 additions and 38 deletions.
  1. +1 −1 Bounded.idr
  2. +3 −6 CheckLang.idr
  3. +11 −10 Interp.idr
  4. +11 −11 Lang.idr
  5. +47 −2 Main.idr
  6. +1 −1 NatCmp.idr
  7. +16 −4 Parser.idr
  8. +1 −1 RawLang.idr
  9. +2 −2 wspace.ipkg
View
@@ -10,7 +10,7 @@ import NatCmp
%default total
-- | Bounded natural numbers
-data Bounded : Nat -> Set where
+data Bounded : Nat -> Type where
Bound : (k : Nat) -> Bounded (plus (S k) n)
instance Show (Bounded n) where
View
@@ -105,12 +105,9 @@ check' : Vect Label lbls -> List RInstr -> (stkIn : Nat) ->
Maybe (stkOut ** Prog stkIn stkOut lbls)
check' ls [] stk = return (_ ** [])
check' ls (i :: is) stk
- = do ci <- checkI ls i stk
- case ci of
- (stk' ** i') =>
- do cis <- check' ls is stk'
- case cis of
- (stk'' ** is') => return (stk'' ** i' :: is')
+ = do (stk' ** i') <- checkI ls i stk
+ (stk'' ** is') <- check' ls is stk'
+ return (stk'' ** i' :: is')
findLabels : Prog x y lbls -> LabelCache lbls
findLabels {lbls} prog = updateLabels blank prog
View
@@ -5,7 +5,7 @@ import RawLang
import CheckLang
import Bounded
-ErrMsg : Set
+ErrMsg : Type
ErrMsg = String
doCheck : Stack k -> (i : Nat) -> Maybe (Stack i)
@@ -28,11 +28,12 @@ getHeap n [] = 0
%assert_total -- can't spot decreasing Integer
setHeap : Integer -> Integer -> List Integer -> List Integer
-setHeap 0 val (x :: xs) = val :: xs
-setHeap n val (x :: xs) = x :: setHeap (n - 1) val xs
-setHeap 0 val [] = [val]
-setHeap n val [] = if n > 0 then 0 :: setHeap (n - 1) val [] else []
+setHeap val 0 (x :: xs) = val :: xs
+setHeap val n (x :: xs) = x :: setHeap val (n - 1) xs
+setHeap val 0 [] = [val]
+setHeap val n [] = if n > 0 then 0 :: setHeap val (n - 1) [] else []
+%assert_total -- coverage problem
interpStk : StackInst stkIn stkOut l -> Stack stkIn ->
IO (Stack stkOut)
interpStk (PUSH n) stk = return (n :: stk)
@@ -43,7 +44,7 @@ interpStk SWAP (x :: y :: stk) = return (y :: x :: stk)
interpStk DISCARD (x :: stk) = return stk
interpStk (SLIDE n) (x :: stk) = return (x :: drop stk)
-interpArith : ArithInst stkIn stkOut l -> Stack stkIn ->
+interpArith : ArithInst stkIn stkOut l -> Stack stkIn ->
IO (Stack stkOut)
interpArith ADD (x :: y :: stk) = return (y + x :: stk)
interpArith SUB (x :: y :: stk) = return (y - x :: stk)
@@ -54,7 +55,7 @@ interpArith MOD (x :: y :: stk) = return ((y `prim__modBigInt` x) :: stk)
interpHeap : HeapInst stkIn stkOut l -> Stack stkIn -> List Integer ->
IO (Stack stkOut, List Integer)
interpHeap STORE (val :: addr :: stk) hp
- = return (stk, setHeap addr val hp)
+ = return (stk, setHeap val addr hp)
interpHeap RETRIEVE (addr :: stk) hp
= return (getHeap addr hp :: stk, hp)
@@ -103,11 +104,11 @@ interpIO OUTPUTNUM (x :: stk) hp
interpIO READCHAR (addr :: stk) hp
= do c <- getChar
let x : Int = cast c
- return (stk, setHeap addr (fromInteger x) hp)
+ return (stk, setHeap (fromInteger x) addr hp)
interpIO READNUM (addr :: stk) hp
= do n <- getLine
let x : Int = cast n
- return (stk, setHeap addr (fromInteger x) hp)
+ return (stk, setHeap (fromInteger x) addr hp)
interpInst : Machine l -> IO (Maybe (Machine l))
interpInst (MkMachine (Lang.Nil) l s h c)
@@ -125,7 +126,7 @@ interpInst (MkMachine (Stk i :: prog) l s h c)
= do stk' <- interpStk i s
return (Just (MkMachine prog l stk' h c))
interpInst (MkMachine (Ar i :: prog) l s h c)
- = do stk' <- interpArith i s
+ = do stk' <- interpArith i s
return (Just (MkMachine prog l stk' h c))
interpInst (MkMachine (Hp i :: prog) l s h c)
= do (stk', hp') <- interpHeap i s h
View
@@ -4,28 +4,28 @@ import NatCmp
import Bounded
import RawLang
-data StackInst : Nat -> Nat -> Nat -> Set where
+data StackInst : Nat -> Nat -> Nat -> Type where
PUSH : Integer -> StackInst x (S x) lbls
DUP : StackInst (S x) (S (S x)) lbls
COPY : (x : Nat) -> StackInst (plus x (S k)) (S (plus x (S k))) lbls
SWAP : StackInst (S (S x)) (S (S x)) lbls
DISCARD : StackInst (S x) x lbls
SLIDE : (x : Nat) -> StackInst (S (plus x k)) (S k) lbls
-data ArithInst : Nat -> Nat -> Nat -> Set where
+data ArithInst : Nat -> Nat -> Nat -> Type where
ADD : ArithInst (S (S x)) (S x) lbls
SUB : ArithInst (S (S x)) (S x) lbls
MUL : ArithInst (S (S x)) (S x) lbls
DIV : ArithInst (S (S x)) (S x) lbls
MOD : ArithInst (S (S x)) (S x) lbls
-data HeapInst : Nat -> Nat -> Nat -> Set where
+data HeapInst : Nat -> Nat -> Nat -> Type where
STORE : HeapInst (S (S x)) x lbls
RETRIEVE : HeapInst (S x) (S x) lbls
-- For flow control, have to assume nothing on the stack at target of
-- a label
-data FlowInst : Nat -> Nat -> Nat -> Set where
+data FlowInst : Nat -> Nat -> Nat -> Type where
LABEL : Bounded lbls -> FlowInst x O lbls
CALL : Bounded lbls -> FlowInst x O lbls
JUMP : Bounded lbls -> FlowInst x O lbls
@@ -34,21 +34,21 @@ data FlowInst : Nat -> Nat -> Nat -> Set where
RETURN : FlowInst x O lbls
END : FlowInst x x lbls
-data IOInst : Nat -> Nat -> Nat -> Set where
+data IOInst : Nat -> Nat -> Nat -> Type where
OUTPUT : IOInst (S x) x lbls
OUTPUTNUM : IOInst (S x) x lbls
READCHAR : IOInst (S x) x lbls
READNUM : IOInst (S x) x lbls
-data Instr : Nat -> Nat -> Nat -> Set where
+data Instr : Nat -> Nat -> Nat -> Type where
Stk : StackInst x y lbls -> Instr x y lbls
Ar : ArithInst x y lbls -> Instr x y lbls
Hp : HeapInst x y lbls -> Instr x y lbls
Fl : FlowInst x y lbls -> Instr x y lbls
IOi : IOInst x y lbls -> Instr x y lbls
Check : (x' : Nat) -> Instr x' y lbls -> Instr x y lbls
-data Prog : Nat -> Nat -> Nat -> Set where
+data Prog : Nat -> Nat -> Nat -> Type where
Nil : Prog x x lbls
(::) : Instr x y lbls -> Prog y z lbls -> Prog x z lbls
@@ -63,7 +63,7 @@ data Program = MkProg (Prog O e O)
namespace Stack
-- | A Stack n is a stack which has at least n things in it,
-- but may have more
- data Stack : Nat -> Set where
+ data Stack : Nat -> Type where
Nil : Stack O
(::) : Integer -> Stack k -> Stack (S k)
Unchecked : Stack k -> Stack O
@@ -73,13 +73,13 @@ lookup : Bounded n -> Stack n -> Integer
lookup (Bound O) (x :: xs) = x
lookup (Bound (S k)) (x :: xs) = lookup (Bound k) xs
-data CallStackEntry : Nat -> Set where
+data CallStackEntry : Nat -> Type where
CSE : Prog O y lbls -> CallStackEntry lbls
-LabelCache : Nat -> Set
+LabelCache : Nat -> Type
LabelCache n = Vect (out ** Prog O out n) n
-record Machine : Nat -> Set where
+record Machine : Nat -> Type where
MkMachine : (program : Prog x y lbls) ->
(lblcache : LabelCache lbls) ->
(stack : Stack x) ->
View
@@ -16,7 +16,38 @@ testProg = [RFl (RLABEL "Start"),
RFl (RLABEL "addup"),
RAr RADD,
RFl RRETURN]
-
+
+{-
+dumpI : Instr x y l -> String
+dumpI (Stk (PUSH n)) = "PUSH " ++ show n
+dumpI (Stk DUP) = "DUP"
+dumpI (Stk (COPY n)) = "COPY " ++ show n
+dumpI (Stk SWAP) = "SWAP"
+dumpI (Stk DISCARD) = "DISCARD"
+dumpI (Stk (SLIDE n)) = "SLIDE " ++ show n
+
+dumpI (Ar ADD) = "ADD"
+dumpI (Ar SUB) = "SUB"
+dumpI (Ar MUL) = "MUL"
+dumpI (Ar DIV) = "DIV"
+dumpI (Ar MOD) = "MOD"
+
+dumpI (Hp STORE) = "STORE"
+dumpI (Hp RETRIEVE) = "RETRIEVE"
+
+dumpI (Fl (LABEL x)) = "LABEL " ++ show x
+dumpI (Fl (CALL x)) = "CALL " ++ show x
+dumpI (Fl (JUMP x)) = "JUMP " ++ show x
+dumpI (Fl (JZ x)) = "JZ " ++ show x
+dumpI (Fl (JNEG x)) = "JNEG " ++ show x
+dumpI (Fl RETURN) = "RETURN"
+dumpI (Fl END) = "END"
+
+dumpI (IOi OUTPUT) = "OUTPUT"
+dumpI (IOi OUTPUTNUM) = "OUTPUTNUM"
+dumpI (IOi READCHAR) = "READCHAR"
+dumpI (IOi READNUM) = "READNUM"
+-}
dumpIStk : StackInst x y l -> String
dumpIStk (PUSH n) = "PUSH " ++ show n
@@ -64,15 +95,29 @@ dump : Prog x y l -> String
dump [] = ""
dump (x :: xs) = dumpI x ++ "\n" ++ dump xs
+tspan : List Char -> (List Char, List Char)
+tspan [] = ([], [])
+tspan (x::xs) =
+ if isDigit x then
+ let (ys, zs) = trace (show xs) (tspan xs) in
+ (x::ys, zs)
+ else
+ ([], x::xs)
+
+gcInfo : IO ()
+gcInfo = mkForeign (FFun "idris_gcInfo" [] FUnit)
+
main : IO ()
main = do xs <- getArgs
case xs of
(_ :: prog :: _) =>
+-- print (tspan (unpack ("1234" ++ prog)))
+-- print $ parseNum (unpack (" \t\t \t\t \t\t \n fooasdklfjsahdlkfjashdflkjashfsldkjfhalksdjfh" ++ prog))
do src <- readFile prog
let raw = parse src
case check raw of
Just (_ ** m) => do -- print (dump (program m))
loop m
+ gcInfo
Nothing => putStrLn "FAIL"
_ => putStrLn "Usage: wspace <file>"
-
View
@@ -1,6 +1,6 @@
module NatCmp
-data Cmp : Nat -> Nat -> Set where
+data Cmp : Nat -> Nat -> Type where
cmpLT : (y : _) -> Cmp x (x + S y)
cmpEQ : Cmp x x
cmpGT : (x : _) -> Cmp (y + S x) y
View
@@ -2,15 +2,28 @@ module Parser
import RawLang
+{-
mspan : (a -> Bool) -> List a -> (List a, List a)
mspan p xs = (takeWhile p xs, dropWhile p xs)
+-}
+
+trace : String -> a -> a
+trace x val = unsafePerformIO (do putStrLn x; return val)
+
+mspan : Show a => (a -> Bool) -> List a -> (List a, List a)
+mspan p [] = ([], [])
+mspan p (x::xs) =
+ if p x then
+ let (ys, zs) = mspan p xs in
+ (x::ys, zs)
+ else
+ ([], x::xs)
parseNum : List Char -> (Integer, List Char)
-parseNum xs = case (mspan isWDigit xs) of
+parseNum xs = case (span isWDigit xs) of
(num, (_ :: rest)) => (process 0 1 (reverse num), rest)
(num, []) => (process 0 1 (reverse num), [])
where
- isWDigit : Char -> Bool
isWDigit ' ' = True
isWDigit '\t' = True
isWDigit _ = False
@@ -22,11 +35,10 @@ parseNum xs = case (mspan isWDigit xs) of
process acc p _ = acc
parseLbl : List Char -> (String, List Char)
-parseLbl xs = case (mspan isWDigit xs) of
+parseLbl xs = case (span isWDigit xs) of
(arg, (_ :: rest)) => (process "" arg, rest)
(arg, []) => (process "" arg, [])
where
- isWDigit : Char -> Bool
isWDigit ' ' = True
isWDigit '\t' = True
isWDigit _ = False
View
@@ -3,7 +3,7 @@ module RawLang
import NatCmp
import Bounded
-Label : Set
+Label : Type
Label = String
data RStackInst = RPUSH Integer
View
@@ -1,7 +1,7 @@
package wspace
-modules = Bounded, Interp, Parser, Lang, RawLang, CheckLang, Main
+modules = Bounded, Interp, Parser, NatCmp, Lang, RawLang, CheckLang, Main
main = Main
-opts = "--nocoverage"
+opts = "--dumpdefuns wspace.dc" -- --nocoverage"
executable = wspace

0 comments on commit db65516

Please sign in to comment.