alms 0.6.5 → 0.6.6
raw patch · 11 files changed
+582/−22 lines, 11 files
Files
- Makefile +1/−1
- README +1/−1
- alms.cabal +3/−4
- alms.cabal.sh +2/−2
- lib/libsessionregion.alms +156/−0
- lib/libsessiontype3.alms +130/−0
- lib/libsocketcap3.alms +144/−0
- src/Meta/Quasi.hs +42/−1
- src/Util.hs +12/−12
- src/extensions.txt +0/−1
- util +91/−0
Makefile view
@@ -66,7 +66,7 @@ $(RM) html -VERSION = 0.6.5+VERSION = 0.6.6 DISTDIR = alms-$(VERSION) TARBALL = $(DISTDIR).tar.gz
README view
@@ -14,7 +14,7 @@ GETTING STARTED - Alms requires GHC to build. It is known to work with GHC 7.0.2, and+ Alms requires GHC to build. It is known to work with GHC 7.4.1, and and likely no longer works with GHC 6. Provided that a recent ghc is in your path, to build on UNIX it ought
alms.cabal view
@@ -1,13 +1,13 @@ Name: alms-Version: 0.6.5-Copyright: 2011, Jesse A. Tov+Version: 0.6.6+Copyright: 2012-2015, Jesse A. Tov Cabal-Version: >= 1.8 License: BSD3 License-File: LICENSE Stability: experimental Author: Jesse A. Tov <tov@ccs.neu.edu> Maintainer: tov@ccs.neu.edu-Homepage: http://www.ccs.neu.edu/~tov/pubs/alms+Homepage: http://www.ccs.neu.edu/~tov/pubs/alms/ Category: Compilers/Interpreters Synopsis: a practical affine language Build-type: Simple@@ -184,7 +184,6 @@ StandaloneDeriving TemplateHaskell TupleSections- TypeOperators TypeSynonymInstances UndecidableInstances UnicodeSyntax
alms.cabal.sh view
@@ -3,14 +3,14 @@ cat <<EOF Name: alms Version: `./util`-Copyright: 2011, Jesse A. Tov+Copyright: 2012-2015, Jesse A. Tov Cabal-Version: >= 1.8 License: BSD3 License-File: LICENSE Stability: experimental Author: Jesse A. Tov <tov@ccs.neu.edu> Maintainer: tov@ccs.neu.edu-Homepage: http://www.ccs.neu.edu/~tov/pubs/alms+Homepage: http://www.ccs.neu.edu/~tov/pubs/alms/ Category: Compilers/Interpreters Synopsis: a practical affine language Build-type: Simple
+ lib/libsessionregion.alms view
@@ -0,0 +1,156 @@+(*+ Another session types library. Doesn't use equirecursive types.+*)++module type SESSION_REGION = sig+ type 1+ type +'a ; +'s rec 's+ type ! -`a+ type ? +`a+ type +'s ⊕ +'t+ type +'s & +'t++ type 1 dual = 1+ | (!`a; 's) dual = ?`a; 's dual+ | (?`a; 's) dual = !`a; 's dual+ | ('s ⊕ 't) dual = 's dual & 't dual+ | ('s & 't) dual = 's dual ⊕ 't dual++ type 's rendezvous++ type 'r @ 's : A+ type 'r @@ 's : A++ type 'r channel++ val newRendezvous : unit → 's rendezvous++ val request : 's rendezvous → ∃'r. 'r channel * 'r@'s+ val accept : 's rendezvous → ∃'r. 'r channel * 'r@'s dual++ val send : `a → 'r channel → 'r@(!`a; 's) → 'r@'s+ val recv : 'r channel → 'r@(?`a; 's) → `a * 'r@'s++ val sel₁ : 'r channel → 'r@('s ⊕ 't) → 'r@'s+ val sel₂ : 'r channel → 'r@('s ⊕ 't) → 'r@'t+ val follow : 'r channel → 'r@('s & 't) → ('r@'s + 'r@'t)++ type ('r₁, 's, 'r₂) refocus = 'r₂@'s → 'r₁@@'s++ val newGroup : unit → ∃'r. 'r@@'s+ val adopt : 'r₁ channel → 'r₁@'s → 'r₂@@'s → 'r₂ channel * 'r₂@@'s+ val focus : 'r₁ channel → 'r₁@@'s →+ ∃'r₂. 'r₂ channel * ('r₁, 's, 'r₂) refocus * 'r₂@'s+end++module SessionRegion : SESSION_REGION = struct+ type 1+ type +'a ; +'s+ type ! -`a+ type ? +`a+ type +'s ⊕ +'t+ type +'s & +'t++ type 1 dual = 1+ | (!`a; 's) dual = ?`a; 's dual+ | (?`a; 's) dual = !`a; 's dual+ | ('s ⊕ 't) dual = 's dual & 't dual+ | ('s & 't) dual = 's dual ⊕ 't dual++ module C = Channel++ type 's rendezvous = bool C.channel C.channel+ type 'r channel = bool C.channel+ type 'r @ 's = unit+ type 'r @@ 's = unit++ let newRendezvous = C.new++ let request rv : ∃'r. 'r channel * unit = (C.recv rv, ())++ let accept rv : ∃'r. 'r channel * unit =+ let c = C.new () in+ C.send rv c;+ (c, ())++ let send a c _ = C.send (Unsafe.unsafeCoerce c) a+ let recv c _ = (C.recv (Unsafe.unsafeCoerce c), ())++ let sel₁ c _ = C.send c true+ let sel₂ c _ = C.send c false+ let follow c _ = if C.recv c then Left () else Right ()++ type ('r₁, 's, 'r₂) refocus = 'r₂@'s → 'r₁@@'s++ let newGroup _ : ∃'r. 'r@@'s = ()++ let adopt c _ _ = (c, ())+ let focus c _ : ∃'r₂. 'r₂ channel * (unit → unit) * unit = (c, id, ())+end++module PubSub = struct+ open SessionRegion++ type 'a subscription = ?string; (1 ⊕ μ's. ?'a; 's)++ type 'a control = ?'a; 'a control+ & ?(∃'r. 'r channel * 'r@'a subscription dual);+ 'a control++ let deliver msg subChan !(subRgn : 'rs@@(μ's. !'a; 's)) =+ let (subChan, refocus) = focus subChan subRgn in+ send msg subChan $> subRgn;+ refocus subRgn++ let broadcast msg subChans (subRgn : 'rs@@(μ's. !'a; 's)) =+ foldl (deliver msg) subRgn subChans++ let server (ctlChan, ctlRgn) =+ let rec loop subChans+ !(ctlRgn : 'r@'a control,+ subsRgn : 'q@@(μ's. !'a; 's)) =+ follow ctlChan $> ctlRgn;+ let subChans = match ctlRgn with+ | Left ctlRgn →+ let msg = recv ctlChan ctlRgn in+ broadcast msg subChans $> subsRgn;+ subChans+ | Right ctlRgn → fst $+ let (subChan, !subRgn) = recv ctlChan ctlRgn in+ send "Hello!" subChan $> subRgn;+ follow subChan $> subRgn;+ match subRgn with+ | Left _ → subChans+ | Right subRgn → (adopt subChan $< subRgn) subsRgn :: subChans+ in loop subChans (ctlRgn, subsRgn)+ in loop [] (ctlRgn, newGroup ())++ let subscriber each (rv : 'a subscription rendezvous) =+ let (subChan, !subRgn) = request rv in+ let rec loop () =+ each (recv subChan subRgn);+ loop () in+ putStrLn (recv subChan subRgn);+ sel₂ subChan $> subRgn;+ loop ()++ let rec client ctlChan !(ctlRgn : 'r@string control dual) =+ match getLine () with+ | "+" →+ let rv = newRendezvous () in+ Thread.fork (λ_ → subscriber putStrLn rv);+ sel₂ ctlChan $> ctlRgn;+ send (accept rv) ctlChan $> ctlRgn;+ client ctlChan ctlRgn+ | "q" →+ exit 0+ | msg →+ sel₁ ctlChan $> ctlRgn;+ send msg ctlChan $> ctlRgn;+ client ctlChan ctlRgn++ let main () =+ let rv = newRendezvous () in+ Thread.fork (λ_ → server (request rv));+ uncurry client (accept rv)+end
+ lib/libsessiontype3.alms view
@@ -0,0 +1,130 @@+(*+ Another session types library. Doesn't work yet!+*)++module type SESSION_TYPE = sig+ type 1+ type +'a ; +'s+ type ! -`a+ type ? +`a+ type ~⊕ +`a+ type ~& +`a++ type 1 dual = 1+ | (!`a ; 's) dual = ?`a ; 's dual+ | (?`a ; 's) dual = !`a ; 's dual+ | ~⊕ ('a ...) dual = ~& ('a dual ...)+ | ~& ('a ...) dual = ~⊕ ('a dual ...)++ type 's rendezvous+ type +'s channel : A++ val newRendezvous : unit → 's rendezvous++ val request : 's rendezvous → 's channel+ val accept : 's rendezvous → 's dual channel++ val send : `a → (!`a; 's) channel → 's channel+ val recv : (?`a; 's) channel → `a * 's channel++ type `a ... &-> `r = {+ (`a channel -A> `r) ... +}+ type `a ... ⊕-> `r = [ (`a channel -A> `r) ... ]++ val follow : ~&`c channel → (`c &-> `r) → `r+ val choose : ~⊕`c channel → (`c ⊕-> `r) → `r+end++module SessionType : SESSION_TYPE = struct+ module C = Channel++ type 1+ type +'a ; +'s+ type ! -`a+ type ? +`a+ type ~⊕ +`a+ type ~& +`a++ type 1 dual = 1+ | (!`a ; 's) dual = ?`a ; 's dual+ | (?`a ; 's) dual = !`a ; 's dual+ | ~⊕ ('a ...) dual = ~& ('a dual ...)+ | ~& ('a ...) dual = ~⊕ ('a dual ...)++ type rep = int C.channel+ type 's channel = rep+ type 's rendezvous = rep C.channel++ let newRendezvous = C.new++ let request (r: unit rendezvous) = C.recv r++ let accept (r: unit rendezvous) =+ let c = C.new () in+ C.send r c;+ c++ let send a c = C.send c (Unsafe.unsafeCoerce a); c+ let recv c = (Unsafe.unsafeCoerce (C.recv c), c)++ type `a ... &-> `r = {+ (`a channel -A> `r) ... +}+ type `a ... ⊕-> `r = [ (`a channel -A> `r) ... ]++ let follow c choices =+ let sel = Unsafe.unsafeCoerce (C.recv c) in+ let (i, lab) = Prim.Row.variantLabel sel in+ Prim.Row.unsafeGetRecordFieldThunk i lab choices () c++ let choose c choice =+ let choice = Unsafe.unsafeCoerce choice in+ C.send c choice;+ Prim.Row.unsafeVariantValue choice c+end++(*+module SessionType2Test = struct+ open SessionType++ type state1 = !int; state2+ and state2 = ~&(+ `Done of ?int; 1+ | `More of !int; state2+ | `Again of ?int; state1)++ let client (c : state1 channel) =+ let rec s1 c = let c = send 1 c in s2 c+ and s2 c = follow c {++ done c = fst (recv c),+ more c = s2 (send 2 c),+ again c = let (z, c) = recv c in s1 c+ +}+ in s1 c++ let client (c: state1 channel) =+ let rec s1 !c =+ send 1 $> c;+ s2 c+ and s2 !c =+ follow c;+ match c with+ | Done c -> recv c+ | More c -> send 2 $> c;+ s2 c+ | Again c -> let z = recv c in+ s1 c+ in fst (s1 c)++ let server (c: state1 dual channel) =+ let rec s1 !c =+ match recv c with+ | 0 -> choose More c;+ let z' = recv c in+ choose Done c;+ send z' $> c+ | 1 -> choose Again c;+ send 1 $> c;+ s1 c+ | z -> choose Done c;+ send z $> c+ in fst (s1 c)+end+*)
+ lib/libsocketcap3.alms view
@@ -0,0 +1,144 @@+(*+ A typestate sockets library++ This is a bit more involved than the example in the paper,+ because we have error cases. We deal with this by raising+ an exception which contains a witness that allows recovering+ the capability if presented with the corresponding socket.+*)++#load "libsocket"++module type SOCKET_CAP = sig+ (* The representation of a socket *)+ type 'a socket++ (* Socket capabilities and the socket states *)+ type 'a @ 'c : A+ type raw+ type named+ type listening+ type ready++ (* Socket operations *)+ val socket : unit → ∃ 'a. 'a socket × 'a@raw+ val bind : 'a socket → int → 'a@raw → 'a@named++ val connect : 'a socket → string → string →+ 'a@raw + 'a@named → 'a@ready+ val listen : 'a socket → 'a@named → 'a@listening+ val accept : 'a socket → 'a@listening →+ (∃ 'b. 'b socket × 'b@ready) × 'a@listening+ val send : 'a socket → string → 'a@ready → 'a@ready+ val recv : 'a socket → int → 'a@ready → string × 'a@ready+ val close : 'a socket → 'a@'c → unit++ val isSame : 'a socket → 'b socket → ('a@'c → 'b@'c) option++ (* Operations for catching the error state associated with a given+ socket. *)+ val catchRaw : (unit -A> `r) → 'a socket × ('a@raw -A> `r) → `r+ val catchNamed : (unit -A> `r) → 'a socket × ('a@named -A> `r) → `r+ val catchListening : (unit -A> `r) → 'a socket × ('a@listening -A> `r) → `r+ val catchReady : (unit -A> `r) → 'a socket × ('a@ready -A> `r) → `r++ type 'a dynamicCap = Raw of 'a@raw+ | Named of 'a@named+ | Listening of 'a@listening+ | Ready of 'a@ready++ exception Socket of (∃'a. 'a socket × 'a dynamicCap) option × string+end++module SocketCap : SOCKET_CAP = struct+ module S = Socket++ type 'a socket = S.socket+ type 'a @ 'c = unit+ type raw+ type named+ type listening+ type ready++ type 'a dynamicCap = Raw of 'a@raw+ | Named of 'a@named+ | Listening of 'a@listening+ | Ready of 'a@ready++ exception Socket of (∃'a. 'a socket × 'a dynamicCap) option × string++ let lift thunk sock mkcap =+ try thunk ()+ with IOError msg → raise (Socket (Some (sock, mkcap ()), msg))++ let socket _ : ∃ 'a. 'a socket × 'a@raw =+ try (S.socket (), ())+ with IOError msg → raise (Socket (None, msg))++ let bind sock port _ = lift (λ_ → S.bind sock port) sock Raw++ let connect sock host port cap =+ lift (λ_ → S.connect sock host port) sock+ (match cap with Left _ → Raw | Right _ → Named)++ let listen sock _ = lift (λ_ → S.listen sock) sock Named++ let accept sock _ =+ lift (λ_ → ((S.accept sock, ()) : ∃ 'a. 'a socket × 'a@ready, ()))+ sock Listening++ let send sock data _ = lift (λ_ → S.send sock data; ()) sock Ready++ let recv sock len _ = lift (λ_ → (S.recv sock len, ())) sock Ready++ let close sock _ =+ try S.close sock+ with IOError msg → raise (Socket (None, msg))++ let isSame sock sock' =+ if sock == sock'+ then Some (λ_ → ())+ else None++ let catchBy body state (sock', handler) =+ try body () with+ Socket ((Some (sock, dyncap), msg) as se) →+ if dyncap == state () && sock == sock'+ then handler ()+ else raise (Socket se)++ let catchRaw body = catchBy body Raw+ let catchNamed body = catchBy body Named+ let catchListening body = catchBy body Listening+ let catchReady body = catchBy body Ready+end++module SocketCap2 : SOCKET_CAP = struct+ open SocketCap+ let catchBy body+ (prj : ∀'a. 'a dynamicCap →+ 'a dynamicCap + ('a@'c -A> 'a dynamicCap) × 'a@'c)+ (sock', handler) =+ try body () with+ | Socket (Some (sock, dyncap), msg) →+ match prj dyncap with+ | Left dyncap+ → raise (Socket (Some (sock, dyncap), msg))+ | Right (uncap, cap)+ → match isSame sock sock' with+ | None → raise (Socket (Some (sock, uncap cap), msg))+ | Some witness → handler (witness cap)++ let catchRaw body =+ catchBy body (function Raw cap → Right (Raw, cap)+ | dyncap → Left dyncap)+ let catchNamed body =+ catchBy body (function Named cap → Right (Named, cap)+ | dyncap → Left dyncap)+ let catchListening body =+ catchBy body (function Listening cap → Right (Listening, cap)+ | dyncap → Left dyncap)+ let catchReady body =+ catchBy body (function Ready cap → Right (Ready, cap)+ | dyncap → Left dyncap)+end
src/Meta/Quasi.hs view
@@ -97,7 +97,8 @@ sgQ = mkQuasi "sgQ" parseSigItem mkQuasi :: forall stx note.- (Data (note Raw), Data (stx Raw),+ (Typeable1 note, Typeable1 stx,+ Data (note Raw), Data (stx Raw), LocAst (N (note Raw) (stx Raw)), Data (note Renamed), Data (stx Renamed), LocAst (N (note Renamed) (stx Renamed))) =>@@ -113,6 +114,46 @@ "+'" -> do stx <- parser :: P (N (note Renamed) (stx Renamed)) convert' filename stx++{-+src/Meta/Quasi.hs:115:13:+ Could not deduce (Typeable1 stx) arising from a use of convert'+ from the context (Data (note Raw),+ Data (stx Raw),+ LocAst (N (note Raw) (stx Raw)),+ Data (note Renamed),+ Data (stx Renamed),+ LocAst (N (note Renamed) (stx Renamed)))+ bound by the type signature for+ mkQuasi :: (Data (note Raw), Data (stx Raw),+ LocAst (N (note Raw) (stx Raw)), Data (note Renamed),+ Data (stx Renamed), LocAst (N (note Renamed) (stx Renamed))) =>+ String+ -> (forall i. Tag i => P (N (note i) (stx i))) -> QuasiQuoter+ at src/Meta/Quasi.hs:(99,12)-(106,22)+ or from (ToSyntax a)+ bound by the inferred type of+ qast :: ToSyntax a => String -> TH.Q a+ at src/Meta/Quasi.hs:(109,3)-(124,38)+ Possible fix:+ add (Typeable1 stx) to the context of+ the inferred type of qast :: ToSyntax a => String -> TH.Q a+ or the type signature for+ mkQuasi :: (Data (note Raw), Data (stx Raw),+ LocAst (N (note Raw) (stx Raw)), Data (note Renamed),+ Data (stx Renamed), LocAst (N (note Renamed) (stx Renamed))) =>+ String+ -> (forall i. Tag i => P (N (note i) (stx i))) -> QuasiQuoter+ In a stmt of a 'do' block: convert' filename stx+ In the expression:+ do { stx <- parser :: P (N (note Renamed) (stx Renamed));+ convert' filename stx }+ In a case alternative:+ "+'"+ -> do { stx <- parser :: P (N (note Renamed) (stx Renamed));+ convert' filename stx }+-}+ "+" -> do stx <- parser :: P (N (note Renamed) (stx Renamed)) convert filename lflag stx
src/Util.hs view
@@ -366,24 +366,24 @@ infixl 4 <$$>, <$$$>, <$$$$>, <$$$$$>, <$$$$$$> -(<$.>) ∷ (Arrow (⇝), Functor f) ⇒- f (b ⇝ c) → (a ⇝ b) →- f (a ⇝ c)+(<$.>) ∷ (Arrow arr, Functor f) ⇒+ f (b `arr` c) → (a `arr` b) →+ f (a `arr` c) f <$.> g = (g >>>) <$> f -(<$$.>) ∷ (Arrow (⇝), Functor f, Functor g) ⇒- g (f (b ⇝ c)) → (a ⇝ b) →- g (f (a ⇝ c))+(<$$.>) ∷ (Arrow arr, Functor f, Functor g) ⇒+ g (f (b `arr` c)) → (a `arr` b) →+ g (f (a `arr` c)) f <$$.> g = (g >>>) <$$> f -(<$$$.>) ∷ (Arrow (⇝), Functor f, Functor g, Functor h) ⇒- h (g (f (b ⇝ c))) → (a ⇝ b) →- h (g (f (a ⇝ c)))+(<$$$.>) ∷ (Arrow arr, Functor f, Functor g, Functor h) ⇒+ h (g (f (b `arr` c))) → (a `arr` b) →+ h (g (f (a `arr` c))) f <$$$.> g = (g >>>) <$$$> f -(<$$$$.>) ∷ (Arrow (⇝), Functor f, Functor g, Functor h, Functor i) ⇒- i (h (g (f (b ⇝ c)))) → (a ⇝ b) →- i (h (g (f (a ⇝ c))))+(<$$$$.>) ∷ (Arrow arr, Functor f, Functor g, Functor h, Functor i) ⇒+ i (h (g (f (b `arr` c)))) → (a `arr` b) →+ i (h (g (f (a `arr` c)))) f <$$$$.> g = (g >>>) <$$$$> f infixl 4 <$.>, <$$.>, <$$$.>, <$$$$.>
src/extensions.txt view
@@ -17,7 +17,6 @@ StandaloneDeriving TemplateHaskell TupleSections-TypeOperators TypeSynonymInstances UndecidableInstances UnicodeSyntax
+ util view
@@ -0,0 +1,91 @@+#!/bin/sh++name=alms+host=login.ccs.neu.edu+remote=.www/pubs/$name++version="`awk '$0 ~ /^VERSION *= / { print $3 }' Makefile`"++if [ -z "$1" ]; then+ set showVersion+fi++while [ -n "$1" ]; do+ cmd="$1"+ shift+ case "$cmd" in+ release)+ ver="$1"; shift+ set version "$ver" ci "version bump: $ver" tagversion "$ver" \+ clean dist send link $@+ ;;+ hackage-check)+ cabal upload -c $name-$version.tar.gz+ ;;+ hackage-upload)+ cabal upload $name-$version.tar.gz+ ;;+ hackage)+ set dist hackage-upload $@+ ;;+ clean)+ rm $name*.tar.gz+ ;;+ dist)+ make dist+ ;;+ send)+ scp -p $name-$version.tar.gz $host:$remote/+ ;;+ link)+ ssh $host "cd $remote;+ DISPLAY='' ex -c '/$name-[0-9.]*[.]tar[.]gz/s/-[0-9.]*[.]tar/-$version.tar/|:wq' index.html;+ rm $name.tar.gz;+ ln -s '$name-$version.tar.gz' $name.tar.gz"+ ;;+ edit)+ ssh $host -t vim $remote/index.html+ ;;+ mv)+ src="$1"; shift+ dst="$1"; shift+ git mv "$src" "$dst" &&+ mv "$dst" "$src" &&+ svn mv "$src" "$dst"+ ;;+ ci)+ msg="$1"; shift+ git ca -m "$msg"+ svn ci -m "$msg"+ ;;+ add)+ git add $@+ svn add $@+ set --+ ;;+ tagversion)+ gitversion="$1"+ shift+ git tag "$gitversion"+ ;;+ version)+ version="$1"+ shift+ if [ -n "$version" ]; then+ ex -c "/^VERSION *=/s/=.*/= $version/|:wq" Makefile+ make $name.cabal+ $0 showVersion+ else+ echo "Need to specify a version" >&2+ exit 1+ fi+ ;;+ showVersion)+ echo $version+ ;;+ *)+ echo "What does '$cmd' mean?" >&2+ exit 1+ ;;+ esac+done