Skip to content

Commit

Permalink
run expand -t4 on the original code
Browse files Browse the repository at this point in the history
  • Loading branch information
@yfyf
yfyf committed Jul 3, 2013
1 parent dec44c5 commit a8bd4fd
Show file tree
Hide file tree
Showing 6 changed files with 140 additions and 139 deletions.
76 changes: 38 additions & 38 deletions original_code/banking.idr
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,10 +21,10 @@ accounts (S k) = VCons (RState O (TyLift Account)) (accounts k);
mkAccounts : (n:Nat) -> (IO (REnv (accounts n)));
mkAccounts O = return Empty;
mkAccounts (S k) = do { kaccs <- mkAccounts k;
aref <- newIORef (MkAcc 10000);
alock <- newLock 1;
return (Extend (resource aref alock) kaccs);
};
aref <- newIORef (MkAcc 10000);
alock <- newLock 1;
return (Extend (resource aref alock) kaccs);
};

showAcc : Account -> String;
showAcc (MkAcc i) = "£" ++ (showInt i);
Expand All @@ -36,7 +36,7 @@ increase : Int -> Account -> Account;
increase sum (MkAcc v) = MkAcc (v+sum);

eq_resp_VCons : {xs,ys:Vect A n} ->
(xs=ys) -> ((VCons x xs) = (VCons x ys));
(xs=ys) -> ((VCons x xs) = (VCons x ys));
eq_resp_VCons (refl xs) = refl (VCons _ xs);

revert : {i:Fin n} -> {xs:Vect A n} ->
Expand All @@ -45,45 +45,45 @@ revert first = refl _;
revert (later p) = eq_resp_VCons (revert p);

revertLock : {tins:Vect ResState tin} ->
{i:Fin tin} ->
(ElemIs i x tins) ->
(Lang (update i y tins) (update i x (update i y tins)) ty) ->
(Lang (update i y tins) tins ty);
{i:Fin tin} ->
(ElemIs i x tins) ->
(Lang (update i y tins) (update i x (update i y tins)) ty) ->
(Lang (update i y tins) tins ty);
revertLock {i} {y} {tins} {ty} p l
= rewrite {A=\ ts . Lang (update i y tins) ts ty} l (revert p);

-- if i<j, updating index i does not affect index j
stillElem : {i,j:Fin n} -> {xs:Vect A n} ->
(LTFin i j) -> (ElemIs i x xs) -> (ElemIs i x (update j y xs));
(LTFin i j) -> (ElemIs i x xs) -> (ElemIs i x (update j y xs));
stillElem ltO first = first;
stillElem (ltS p) (later q) = later (stillElem p q);

updatedElemIs : {xs:Vect A n} ->
{i:Fin n} ->
(ElemIs i y (update i y xs));
{i:Fin n} ->
(ElemIs i y (update i y xs));
updatedElemIs {i=fO} {xs=VCons x xs} = first;
updatedElemIs {i=fS k} {xs=VCons x xs} = later updatedElemIs;

updated2ElemIs : {xs:Vect A n} -> {x,w:A} ->
{i,j:Fin n} -> (LTFin i j) ->
(ElemIs j x (update i w (update j x xs)));
{i,j:Fin n} -> (LTFin i j) ->
(ElemIs j x (update i w (update j x xs)));
updated2ElemIs ltO {xs=VCons x xs} = later updatedElemIs;
updated2ElemIs (ltS p) {xs=VCons x xs} = later (updated2ElemIs p);

-- Take two locks, do the body, then unlock.
lockTwo : {tins:Vect ResState tin} ->
{r1,r2:Fin tin} ->
(LTFin r1 r2) ->
(ElemIs r1 (RState k1 ty1) tins) ->
(ElemIs r2 (RState k2 ty2) tins) ->
(Unlocked r2 tins) ->
(body:Lang (update r1 (RState (S k1) ty1)
(update r2 (RState (S k2) ty2) tins))
(update r1 (RState (S k1) ty1)
(update r2 (RState (S k2) ty2) tins)) tyret) ->
(Lang tins tins tyret);
{r1,r2:Fin tin} ->
(LTFin r1 r2) ->
(ElemIs r1 (RState k1 ty1) tins) ->
(ElemIs r2 (RState k2 ty2) tins) ->
(Unlocked r2 tins) ->
(body:Lang (update r1 (RState (S k1) ty1)
(update r2 (RState (S k2) ty2) tins))
(update r1 (RState (S k1) ty1)
(update r2 (RState (S k2) ty2) tins)) tyret) ->
(Lang tins tins tyret);
lockTwo {r1} {r2} lt l1 l2 pri body
= BIND (LOCK l2 pri)
= BIND (LOCK l2 pri)
(\u . BIND (LOCK (stillElem lt l1) (unlockEarlier lt (unlockedId pri)))
(\u . BIND body
(\ret . BIND (revertLock (stillElem lt l1) (UNLOCK updatedElemIs))
Expand All @@ -100,12 +100,12 @@ accountIs {i=fO} = first;
accountIs {i=fS k} = later accountIs;

updateEq : {i:Fin n} -> {xs:Vect A n} -> {v:A} ->
((vlookup i (update i v xs)) = v);
((vlookup i (update i v xs)) = v);
updateEq {i=fO} {v} {xs=VCons x xs} = refl _;
updateEq {i=fS k} {v} {xs=VCons x xs} = updateEq {i=k} {xs};

moveMoneyCmp : {sender,receiver:Fin n} ->
(move:CmpFin sender receiver) -> Int ->
(move:CmpFin sender receiver) -> Int ->
(Lang (accounts n) (accounts n) TyUnit);
moveMoneyCmp {sender} {receiver} (lSmall p) amount
= lockTwo p accountIs accountIs unlockedAcc
Expand Down Expand Up @@ -140,10 +140,10 @@ dumpAccs : Int -> (REnv (accounts n)) -> (IO ());
dumpAccs num Empty = return II;
{-
dumpAccs num (Extend (resource v l) env) = do { acc <- readIORef v;
putStr ((showInt num)++" : ");
putStrLn (showAcc acc);
-- dumpAccs (num+1) env;
};
putStr ((showInt num)++" : ");
putStrLn (showAcc acc);
-- dumpAccs (num+1) env;
};
-}

one = S O; two = S one; three = S two; four = S three; five = S four;
Expand All @@ -153,10 +153,10 @@ thirty = mult ten three;

test : IO ();
test = do { -- ten accounts with £100 each.
accs : (REnv (accounts ten)) <- mkAccounts ten;
-- Move 50 from acct 1 to acct 0
accs <- runMove {n=ten} (fS fO) fO 50 accs;
-- Move 120 from acct 0 to acct 2
accs <- runMove {n=ten} fO (fS (fS fO)) 120 accs;
return II;
};
accs : (REnv (accounts ten)) <- mkAccounts ten;
-- Move 50 from acct 1 to acct 0
accs <- runMove {n=ten} (fS fO) fO 50 accs;
-- Move 120 from acct 0 to acct 2
accs <- runMove {n=ten} fO (fS (fS fO)) 120 accs;
return II;
};
130 changes: 65 additions & 65 deletions original_code/concdsl_dl.idr
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,8 +18,8 @@ getLock : (Resource r) -> Lock;
getLock (resource ref l) = l;

rlookup : {xs:Vect ResState rn} -> (p:ElemIs i (RState k ty) xs) ->
(REnv xs) ->
(IORef (interpTy ty));
(REnv xs) ->
(IORef (interpTy ty));
rlookup first (Extend (resource v l) env) = v;
rlookup (later p) (Extend v env) = rlookup p env;

Expand All @@ -30,16 +30,16 @@ llookup i env = getLock (envLookup i env);
-- the right lock state.

lockEnv : {i:Fin ln} -> {xs:Vect ResState ln} ->
(ElemIs i (RState k ty) xs) ->
(REnv xs) ->
(REnv (update i (RState (S k) ty) xs));
(ElemIs i (RState k ty) xs) ->
(REnv xs) ->
(REnv (update i (RState (S k) ty) xs));
lockEnv first (Extend (resource ref l) env) = Extend (resource ref l) env;
lockEnv (later p) (Extend r env) = Extend r (lockEnv p env);

unlockEnv : {i:Fin un} -> {xs:Vect ResState un} ->
(ElemIs i (RState (S k) ty) xs) ->
(REnv xs) ->
(REnv (update i (RState k ty) xs));
(ElemIs i (RState (S k) ty) xs) ->
(REnv xs) ->
(REnv (update i (RState k ty) xs));
unlockEnv first (Extend (resource ref l) env) = Extend (resource ref l) env;
unlockEnv (later p) (Extend r env) = Extend r (unlockEnv p env);

Expand All @@ -52,75 +52,75 @@ data Lang : (Vect ResState tin)->(Vect ResState tout)->Ty-># where
-- Read from a shared variable. Must have the lock.

READ : {tins:Vect ResState tin} ->
{i:Fin tin} ->
(locked:ElemIs i (RState (S k) ty) tins) ->
(Lang tins tins ty)
{i:Fin tin} ->
(locked:ElemIs i (RState (S k) ty) tins) ->
(Lang tins tins ty)

-- Write to a shared variable. Must have the lock.

| WRITE : {tins:Vect ResState tin} ->
{i:Fin tin} -> (val:interpTy ty) ->
(locked:ElemIs i (RState (S k) ty) tins) ->
(Lang tins tins TyUnit)
(locked:ElemIs i (RState (S k) ty) tins) ->
(Lang tins tins TyUnit)

-- Lock a shared variable.
-- Must know that no lower priority items are locked, that is everything
-- before 'i' in tins must be unlocked.

| LOCK : {tins:Vect ResState tin} ->
{i:Fin tin} ->
(locked:ElemIs i (RState k ty) tins) ->
(priOK:Unlocked i tins) ->
(Lang tins (update i (RState (S k) ty) tins) TyUnit)
{i:Fin tin} ->
(locked:ElemIs i (RState k ty) tins) ->
(priOK:Unlocked i tins) ->
(Lang tins (update i (RState (S k) ty) tins) TyUnit)

-- Unlock a shared variable. Must know it is locked at least once.

| UNLOCK : {tins:Vect ResState tin} ->
{i:Fin tin} ->
(locked:ElemIs i (RState (S k) ty) tins) ->
(Lang tins (update i (RState k ty) tins) TyUnit)
{i:Fin tin} ->
(locked:ElemIs i (RState (S k) ty) tins) ->
(Lang tins (update i (RState k ty) tins) TyUnit)

-- Create a new shared resource, and put it at the end of the list.
-- Leave it out for now until we work out the best way to represent handles.
{-
| CREATE : {tins:Vect ResState tin} ->
(val:interpTy ty) ->
(Lang tins (snoc tins (RState O ty)) (TyHandle (S tin)))
(val:interpTy ty) ->
(Lang tins (snoc tins (RState O ty)) (TyHandle (S tin)))
-}

-- Some control structures; loop n times, and fork a new process

| LOOP : {tins:Vect ResState tin} ->
(count:Nat) -> (body:Lang tins tins TyUnit) ->
(Lang tins tins TyUnit)
(count:Nat) -> (body:Lang tins tins TyUnit) ->
(Lang tins tins TyUnit)
| FORK : {tins:Vect ResState tin} ->
(AllUnlocked tins) ->
(proc:Lang tins tins TyUnit) ->
(Lang tins tins TyUnit)
(AllUnlocked tins) ->
(proc:Lang tins tins TyUnit) ->
(Lang tins tins TyUnit)

-- The rest are useful for any language; dynamic checking, IO action and
-- binding variables.

| CHECK : {tins:Vect ResState tin} -> {touts: Vect ResState tout} ->
(Maybe a) ->
(ifJ:a -> (Lang tins touts ty)) ->
(ifN:Lang tins touts ty) ->
(Lang tins touts ty)
(Maybe a) ->
(ifJ:a -> (Lang tins touts ty)) ->
(ifN:Lang tins touts ty) ->
(Lang tins touts ty)
| CHOOSE : {tins:Vect ResState tin} -> {touts: Vect ResState tout} ->
(Either a b) ->
(ifLeft : a -> (Lang tins touts ty)) ->
(ifRight : b -> (Lang tins touts ty)) ->
(Lang tins touts ty)
(Either a b) ->
(ifLeft : a -> (Lang tins touts ty)) ->
(ifRight : b -> (Lang tins touts ty)) ->
(Lang tins touts ty)
| ACTION : {tins:Vect ResState tin} ->
(IO ()) -> (Lang tins tins TyUnit)
| RETURN : {tins:Vect ResState tin} ->
(val:interpTy ty) -> (Lang tins tins ty)
(val:interpTy ty) -> (Lang tins tins ty)
| BIND : {tins:Vect ResState tin} ->
{ts1:Vect ResState ts1n} ->
{touts:Vect ResState tout} ->
(code:Lang tins ts1 ty)->
(k:(interpTy ty)->(Lang ts1 touts tyout))->
(Lang tins touts tyout);
{ts1:Vect ResState ts1n} ->
{touts:Vect ResState tout} ->
(code:Lang tins ts1 ty)->
(k:(interpTy ty)->(Lang ts1 touts tyout))->
(Lang tins touts tyout);

data I A B = MkPair A B;

Expand All @@ -134,56 +134,56 @@ interp : {ty:Vect ResState tin} -> {tyo:Vect ResState tout} -> {T:Ty} ->
(REnv ty) -> (Lang ty tyo T) -> (IO (I (REnv tyo) (interpTy T)));

interpBind : {tyin:Vect ResState tin} -> {tyout:Vect ResState tout} ->
(I (REnv tyin) A) -> (A -> (Lang tyin tyout B)) ->
(IO (I (REnv tyout) (interpTy B)));
(I (REnv tyin) A) -> (A -> (Lang tyin tyout B)) ->
(IO (I (REnv tyout) (interpTy B)));
interpBind (MkPair env val) k = interp env (k val);

interpLoop : {tyin:Vect ResState tin} ->
(REnv tyin) ->
(count:Nat) -> (body:Lang tyin tyin TyUnit) ->
(IO (I (REnv tyin) ()));
(REnv tyin) ->
(count:Nat) -> (body:Lang tyin tyin TyUnit) ->
(IO (I (REnv tyin) ()));
interpLoop env O code = return (MkPair env II);
interpLoop env (S k) code = do { ires <- interp env code;
interpLoop (fst ires) k code;
};
interpLoop (fst ires) k code;
};

interpCheck : {tyin:Vect ResState tin} -> {tyout:Vect ResState tout} ->
(env:REnv tyin) -> (Maybe a) ->
(ifJ : a -> (Lang tyin tyout ty)) ->
(ifN : Lang tyin tyout ty) ->
(IO (I (REnv tyout) (interpTy ty)));
(env:REnv tyin) -> (Maybe a) ->
(ifJ : a -> (Lang tyin tyout ty)) ->
(ifN : Lang tyin tyout ty) ->
(IO (I (REnv tyout) (interpTy ty)));
interpCheck env Nothing ifJ ifN = interp env ifN;
interpCheck env (Just a) ifJ ifN = interp env (ifJ a);

interpChoose : {tyin:Vect ResState tin} -> {tyout:Vect ResState tout} ->
(env:REnv tyin) -> (Either a b) ->
(ifL : a -> (Lang tyin tyout ty)) ->
(ifL : b -> (Lang tyin tyout ty)) ->
(IO (I (REnv tyout) (interpTy ty)));
(env:REnv tyin) -> (Either a b) ->
(ifL : a -> (Lang tyin tyout ty)) ->
(ifL : b -> (Lang tyin tyout ty)) ->
(IO (I (REnv tyout) (interpTy ty)));
interpChoose env (Left a) ifL ifR = interp env (ifL a);
interpChoose env (Right b) ifL ifR = interp env (ifR b);

interp env (READ p) = do { val <- readIORef (rlookup p env);
return (MkPair env val);
};
return (MkPair env val);
};
interp env (WRITE v p) = do { val <- writeIORef (rlookup p env) v;
return (MkPair env II); };
return (MkPair env II); };
interp env (LOCK {i} p pri) = do { lock (llookup i env);
return (MkPair (lockEnv p env) II); };
return (MkPair (lockEnv p env) II); };
interp env (UNLOCK {i} p) = do { unlock (llookup i env);
return (MkPair (unlockEnv p env) II); };
return (MkPair (unlockEnv p env) II); };
interp env (ACTION io) = do { io;
return (MkPair env II); };
return (MkPair env II); };
interp env (RETURN val) = return (MkPair env val);
interp env (CHECK m j n) = interpCheck env m j n;
interp env (CHOOSE m l r) = interpChoose env m l r;
interp env (LOOP n body) = interpLoop env n body;
-- Interpret the given process in a new thread, and carry on.
interp env (FORK _ proc)
= do { fork (do { f <- interp env proc; return II; });
return (MkPair env II);
};
return (MkPair env II);
};
-- interp {tin} env CREATE = return (MkPair (addEnd env O) (bound {n=tin}));
interp env (BIND code k) = do { coderes <- interp env code;
interpBind coderes k; };
interpBind coderes k; };

Loading

0 comments on commit a8bd4fd

Please sign in to comment.