Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Sign in
Toggle navigation
Menu
Open sidebar
i7
peregrine
Commits
2e4a81db
Commit
2e4a81db
authored
Nov 28, 2017
by
Stefan Jaax
Browse files
Change default format to JSON
parent
cb83555d
Changes
3
Hide whitespace changes
Inline
Side-by-side
peregrine.cabal
View file @
2e4a81db
...
...
@@ -22,8 +22,8 @@ executable peregrine
main-is: Main.hs
other-modules:
-- other-extensions:
build-depends: base >=4 && <5, sbv, parsec, containers, transformers,
bytestring, mtl, stm, async, parallel-io
build-depends: base >=4 && <5, sbv, parsec
>= 3.1
, containers, transformers,
bytestring, mtl, stm, async, parallel-io
, text, aeson
hs-source-dirs: src
default-language: Haskell2010
ghc-options: -fsimpl-tick-factor=1000 -threaded -rtsopts -with-rtsopts=-N
src/Parser.hs
View file @
2e4a81db
...
...
@@ -3,6 +3,8 @@ module Parser
where
import
Text.Parsec
import
qualified
Data.Text
as
T
import
qualified
Data.Text.IO
as
TIO
type
Parser
a
=
Parsec
String
()
a
...
...
@@ -14,7 +16,7 @@ parseString p str =
parseFile
::
Parser
a
->
String
->
IO
a
parseFile
p
file
=
do
contents
<-
readFile
file
case
parse
p
file
contents
of
contents
<-
T
.
unpack
<$>
TIO
.
readFile
file
case
parse
p
file
contents
of
Left
e
->
print
e
>>
fail
"parse error"
Right
r
->
return
r
src/Parser/PP.hs
View file @
2e4a81db
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}
module
Parser.PP
(
parseContent
)
where
import
Data.Aeson
import
Data.Aeson.TH
(
deriveJSON
,
defaultOptions
)
import
Control.Applicative
((
<*
),(
*>
),(
<$>
))
import
Data.Functor.Identity
import
Text.Parsec
import
qualified
Data.Set
as
S
import
qualified
Data.ByteString.Lazy.Char8
as
BS
import
qualified
Data.Text
as
T
import
Text.Parsec.Expr
import
Text.Parsec.Language
(
LanguageDef
,
emptyDef
)
import
qualified
Text.Parsec.Token
as
Token
import
Parser
import
PopulationProtocol
(
PopulationProtocol
,
makePopulationProtocolFromStrings
,
State
(
..
),
Transition
(
..
))
import
Property
...
...
@@ -25,7 +33,7 @@ languageDef =
Token
.
reservedOpNames
=
[
"->"
,
"<"
,
"<="
,
"="
,
"!="
,
">="
,
">"
,
"+"
,
"-"
,
"*"
,
"&&"
,
"||"
,
"!"
,
":"
]
}
lexer
::
Token
.
TokenParser
()
lexer
=
Token
.
makeTokenParser
languageDef
...
...
@@ -68,78 +76,6 @@ ident = (identifier <|> stringLiteral) <?> "identifier"
identList
::
Parser
[
String
]
identList
=
singleOrList
ident
states
::
Parser
[
String
]
states
=
reserved
"states"
*>
identList
transitions
::
Parser
[
String
]
transitions
=
reserved
"transitions"
*>
identList
initial
::
Parser
[
String
]
initial
=
reserved
"initial"
*>
identList
trueStates
::
Parser
[
String
]
trueStates
=
reserved
"true"
*>
identList
falseStates
::
Parser
[
String
]
falseStates
=
reserved
"false"
*>
identList
arc
::
Parser
[(
String
,
String
,
Integer
)]
arc
=
do
lhs
<-
identList
rhsList
<-
many1
(
do
reservedOp
"->"
w
<-
numberOption
ids
<-
identList
return
(
ids
,
w
)
)
return
$
fst
$
foldl
makeArc
(
[]
,
lhs
)
rhsList
where
makeArc
(
as
,
lhs
)
(
rhs
,
w
)
=
([(
l
,
r
,
w
)
|
l
<-
lhs
,
r
<-
rhs
]
++
as
,
rhs
)
arcs
::
Parser
[(
String
,
String
,
Integer
)]
arcs
=
do
reserved
"arcs"
as
<-
singleOrList
arc
return
$
concat
as
data
Statement
=
States
[
String
]
|
Transitions
[
String
]
|
Initial
[
String
]
|
TrueStatement
[
String
]
|
FalseStatement
[
String
]
|
PredicateStatement
(
QuantFormula
String
)
|
Arcs
[(
String
,
String
,
Integer
)]
statement
::
Parser
Statement
statement
=
States
<$>
states
<|>
Transitions
<$>
transitions
<|>
Arcs
<$>
arcs
<|>
Initial
<$>
initial
<|>
TrueStatement
<$>
trueStates
<|>
FalseStatement
<$>
falseStates
<|>
PredicateStatement
<$>
predicate
populationProtocol
::
Parser
PopulationProtocol
populationProtocol
=
do
reserved
"population"
reserved
"protocol"
name
<-
option
""
ident
statements
<-
braces
(
many
statement
)
let
(
qs
,
ts
,
qinitial
,
qtrue
,
qfalse
,
ps
,
as
)
=
foldl
splitStatement
(
[]
,
[]
,
[]
,
[]
,
[]
,
Nothing
,
[]
)
statements
let
predicate
=
case
ps
of
Nothing
->
ExQuantFormula
[]
FTrue
Just
p
->
p
return
$
makePopulationProtocolFromStrings
name
qs
ts
qinitial
qtrue
qfalse
predicate
as
where
splitStatement
(
qs
,
ts
,
qinitial
,
qtrue
,
qfalse
,
ps
,
as
)
stmnt
=
case
stmnt
of
States
q
->
(
q
++
qs
,
ts
,
qinitial
,
qtrue
,
qfalse
,
ps
,
as
)
Transitions
t
->
(
qs
,
t
++
ts
,
qinitial
,
qtrue
,
qfalse
,
ps
,
as
)
Initial
q
->
(
qs
,
ts
,
q
++
qinitial
,
qtrue
,
qfalse
,
ps
,
as
)
TrueStatement
q
->
(
qs
,
ts
,
qinitial
,
q
++
qtrue
,
qfalse
,
ps
,
as
)
FalseStatement
q
->
(
qs
,
ts
,
qinitial
,
qtrue
,
q
++
qfalse
,
ps
,
as
)
PredicateStatement
p
->
(
qs
,
ts
,
qinitial
,
qtrue
,
qfalse
,
Just
p
,
as
)
Arcs
a
->
(
qs
,
ts
,
qinitial
,
qtrue
,
qfalse
,
ps
,
a
++
as
)
binary
::
String
->
(
a
->
a
->
a
)
->
Assoc
->
Operator
String
()
Identity
a
binary
name
fun
=
Infix
(
reservedOp
name
*>
return
fun
)
prefix
::
String
->
(
a
->
a
)
->
Operator
String
()
Identity
a
...
...
@@ -205,16 +141,50 @@ quantFormula =
<|>
(
ExQuantFormula
[]
<$>
formula
)
predicate
::
Parser
(
QuantFormula
String
)
predicate
=
do
reserved
"predicate"
form
<-
braces
quantFormula
return
form
instance
FromJSON
(
QuantFormula
String
)
where
parseJSON
(
String
v
)
=
do
let
formula
=
parse
quantFormula
""
(
T
.
unpack
v
)
case
formula
of
Left
e
->
fail
"Predicate formula not well-formed."
Right
r
->
return
r
parseJSON
_
=
fail
"Expect string for predicate."
instance
ToJSON
(
QuantFormula
String
)
where
toJSON
x
=
String
""
data
RecordTransition
=
RecordTransition
{
name
::
String
,
pre
::
[
String
],
post
::
[
String
]
}
deriving
(
Show
)
data
RecordPP
=
RecordPP
{
title
::
String
,
states
::
[
String
],
transitions
::
[
RecordTransition
],
initialStates
::
[
String
],
trueStates
::
[
String
],
predicate
::
Maybe
(
QuantFormula
String
)
}
deriving
(
Show
)
$
(
deriveJSON
defaultOptions
''RecordTransition
)
$
(
deriveJSON
defaultOptions
''RecordPP
)
recordPP2PopulationProtocol
::
RecordPP
->
PopulationProtocol
recordPP2PopulationProtocol
r
=
makePopulationProtocolFromStrings
(
title
r
)
(
states
r
)
(
map
name
(
transitions
r
))
(
initialStates
r
)
(
trueStates
r
)
falseStates
p
arcs
where
falseStates
=
[
q
|
q
<-
states
r
,
not
(
S
.
member
q
(
S
.
fromList
(
trueStates
r
)))]
count
=
\
x
->
length
.
(
filter
(
==
x
))
arcs
=
[(
name
t
,
q
,
toInteger
m
)
|
t
<-
transitions
r
,
q
<-
(
pre
t
++
post
t
),
let
m
=
(
count
q
)
(
post
t
)
-
(
count
q
)
(
pre
t
)]
p
=
case
predicate
r
of
Nothing
->
ExQuantFormula
[]
FTrue
(
Just
p'
)
->
p'
parseContent
::
Parser
PopulationProtocol
parseContent
=
do
whiteSpace
pp
<-
populationProtocol
properties
<-
many
predicate
eof
return
pp
parseContent
=
do
str
<-
manyTill
anyChar
eof
let
r
=
eitherDecode
(
BS
.
pack
str
)
case
r
of
(
Left
e
)
->
fail
e
(
Right
pp
)
->
return
(
recordPP2PopulationProtocol
pp
)
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment