Skip to content

Commit 7250ffd

Browse files
traiansftraiansf
committed
MErged trunk into branch
git-svn-id: http://k-framework.googlecode.com/svn/branches/sortcells@9922 82a86efa-2583-11df-8ea0-49ba94de29ab Former-commit-id: c9ae05d3aa26a9e5c02c3c1754354f1f91062cb4 [formerly c285bd929b7e2fdb0c1adb16f0c59fb871565223] Former-commit-id: bf273f2c2363ff39519d6947b9de09b03d1e6f50
1 parent ace5768 commit 7250ffd

334 files changed

Lines changed: 7451 additions & 4677 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎.idea/misc.xml‎

Lines changed: 17 additions & 0 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎dist/bin/kast.sh‎

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
#!/usr/bin/env sh
2+
3+
case $(uname) in
4+
Linux) OS=linux;;
5+
Darwin) OS=macos;;
6+
*) echo "Unknown OS $(uname)"; exit 1;;
7+
esac
8+
BIN=$(dirname $0)/native/$OS
9+
10+
#pwd >> log.txt
11+
#echo $* >> log.txt
12+
#echo $FK >> log.txt
13+
#env >> log.txt
14+
15+
if [ "$1" = --new-kast ] ; then
16+
MODE="--new-kast";
17+
shift;
18+
else
19+
MODE='';
20+
fi
21+
22+
if [ -z "$1" -o ! -z "$2" -o ! -f "$1" ] ; then
23+
echo 'Usage: kast.sh <inputfile>';
24+
exit 1;
25+
fi
26+
27+
INPUTFILE=$1
28+
SORT=${KRUN_SORT:-K}
29+
DEF=${KRUN_COMPILED_DEF:-*-kompiled}
30+
if [ ! -d $DEF ] ; then
31+
if [ -z "$KRUN_COMPILED_DEF" ] ; then
32+
if [ "*-kompiled" = '*-kompiled' ] ; then
33+
echo "No compiled definitions in current directory"
34+
else
35+
echo "Multiple compiled definitions in current directory"
36+
fi;
37+
else
38+
echo "Definition ${KRUN_COMPILED_DEF} does not exist";
39+
fi;
40+
exit 1;
41+
fi
42+
43+
KDIR=$(dirname $DEF)/.k
44+
mkdir -p $KDIR
45+
RAWPARSE=$(mktemp $KDIR/parseXXXXXX.baf)
46+
if $BIN/sglr -fp -s$SORT -p $DEF/pgm/Program.tbl -i $INPUTFILE > $RAWPARSE 2> /dev/null ; then
47+
$BIN/implodePT < $RAWPARSE | $BIN/baffle -rb -wt | $BIN/FastKast $MODE $DEF/consTable.txt
48+
else
49+
$BIN/baffle -rb -wt < $RAWPARSE | $BIN/FastKast $DEF/consTable.txt
50+
fi
51+
rm $RAWPARSE

‎dist/bin/kio‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
#!/usr/bin/env sh
2+
3+
java -jar -Xmx1024m "$(dirname $0)/java/k3.jar" -ioserver "$@"

‎dist/bin/kompile‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
11
#!/usr/bin/env sh
22
ulimit -s `ulimit -H -s`
3-
/Library/Java/JavaVirtualMachines/jdk1.7.0_17.jdk/Contents/Home/bin/java -ss8m -Xms64m -Xmx1G -jar "$(dirname $0)/java/k3.jar" -kompile "$@"
3+
java -ea -ss8m -Xms64m -Xmx1G -jar "$(dirname $0)/java/k3.jar" -kompile "$@"
4+

‎dist/bin/maude/lib/TCPSupport.maude‎

Lines changed: 13 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ mod #TCP-CLIENT is
2020
op Client : -> #Socket-Cid .
2121
op cnum : #Nat -> #Socket-Oid .
2222
op #checkAnswer : #Socket-Oid #String ~> #String .
23-
eq #checkAnswer(cnum(N),S) = #checkAnswer-aux(int2String(N), findString(S, "#", 0), S) .
23+
eq #checkAnswer(cnum(N),S) = #checkAnswer-aux(int2String(N), findString(S, "\001", 0), S) .
2424
op #checkAnswer-aux : #String #Nat #String ~> #String .
2525
ceq #checkAnswer-aux(SN:#String, P:#Nat, S)
2626
= substrString(S, P:#Nat +Nat 1, lengthString(S))
@@ -36,7 +36,7 @@ mod #TCP-CLIENT is
3636

3737
vars Me Server : #Socket-Oid .
3838
var A : #Socket-AttributeSet .
39-
var S : #String .
39+
var S S2 : #String .
4040
var M : #Socket-Msg .
4141
var C : #Socket-Configuration .
4242
var N : #Nat .
@@ -62,18 +62,14 @@ mod #TCP-CLIENT is
6262
[print Me " sending"] .
6363

6464
rl < Me : Client | #state: #sending,#Socket A > #Socket #sent(Me, Server)
65-
=> < Me : Client | #state: #receiving,#Socket A > #Socket #receive(Server, Me)
65+
=> < Me : Client | #state: #receiving,#Socket answer: "",#Socket A > #Socket #receive(Server, Me)
6666
[print Me " receiving"] .
6767

68-
rl < Me : Client | #state: #receiving,#Socket A > #Socket #received(Me, Server, S)
69-
=> < Me : Client | #state: #haveAnswer,#Socket answer: S,#Socket A >
68+
rl < Me : Client | #state: #receiving,#Socket answer: S,#Socket A > #Socket #received(Me, Server, S2)
69+
=> < Me : Client | #state: #receiving,#Socket answer: (S +String S2),#Socket A > #Socket #receive(Server, Me)
7070
[print Me " have answer"] .
71-
72-
rl < Me : Client | #state: #haveAnswer,#Socket #connectedTo: Server,#Socket A >
73-
=> < Me : Client | #state: #closing,#Socket #connectedTo: Server,#Socket A > #Socket #closeSocket(Server, Me)
74-
[print Me " closing"] .
75-
76-
rl < Me : Client | #state: #closing,#Socket A > #Socket #closedSocket(Me, Server, S)
71+
72+
rl < Me : Client | #state: #receiving,#Socket A > #Socket #closedSocket(Me, Server, S)
7773
=> < Me : Client | #state: #finished,#Socket A >
7874
[print Me " finished"] .
7975

@@ -101,24 +97,24 @@ mod #TCP is
10197

10298
op #tcpRequest : #String [#Nat] -> [#String] .
10399
eq #tcpRequest(S:#String, N:#Nat) =
104-
#checkResult(#containedRequest(#start(N:#Nat) #Socket #toSend(int2String(N:#Nat) +String "#" +String int2String(lengthString(S:#String)) +String "#" +String S:#String))) .
100+
#checkResult(#containedRequest(#start(N:#Nat) #Socket #toSend(int2String(N:#Nat) +String "\001" +String int2String(lengthString(S:#String)) +String "\001" +String S:#String))) .
105101

106102
op #checkResult : #String -> #String .
107103
op #getTCPData : #String -> #String .
108104

109105

110-
ceq #checkResult(S:#String) = #getTCPData(substrString(S:#String, lengthString("success#"), lengthString(S:#String)))
111-
if substrString(S:#String, 0, lengthString("success#")) ==Universal "success#" [print "full output: " S:#String] .
106+
ceq #checkResult(S:#String) = #getTCPData(substrString(S:#String, lengthString("success\001"), lengthString(S:#String)))
107+
if substrString(S:#String, 0, lengthString("success#")) ==Universal "success\001" [print "full output: " S:#String] .
112108

113109
ceq #getTCPData(S:#String)
114110
= substrString(S:#String, 0, N:#Nat)
115-
if N:#Nat := findString(S:#String, "###", 0) .
111+
if N:#Nat := findString(S:#String, "\001\001\001", 0) .
116112

117113
eq #getTCPData(S:#String)
118114
= #errorTCPSyntax("Incorrect Output: " +String S:#String) [owise] .
119115

120-
ceq #checkResult(S:#String) = #errorTCPSyntax(#getTCPData(substrString(S:#String, lengthString("fail#"), lengthString(S:#String))))
121-
if substrString(S:#String, 0, lengthString("fail#")) ==Universal "fail#" [print "full error string: " S:#String] .
116+
ceq #checkResult(S:#String) = #errorTCPSyntax(#getTCPData(substrString(S:#String, lengthString("fail\001"), lengthString(S:#String))))
117+
if substrString(S:#String, 0, lengthString("fail\001")) ==Universal "fail\001" [print "full error string: " S:#String] .
122118

123119
eq #checkResult("") = #errorTCPSyntax("Unknown error") .
124120
eq #checkResult(#error) = #errorTCPSyntax("Unknown error") .

‎dist/bin/maude/lib/builtins.maude‎

Lines changed: 72 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -885,11 +885,82 @@ mod #K-EQUAL is
885885
eq K1:K ==K K2:K = K1:K ==Universal K2:K .
886886
endm
887887

888+
load pl-meta-level
889+
890+
mod #K-PARSER is
891+
including K-TECHNIQUE .
892+
including #STRING .
893+
including #INT .
894+
including #QID .
895+
including #META-LEVEL .
896+
897+
op string2k : #String -> K .
898+
op string2bag : #String -> Bag .
899+
op string2term : #String -> #Term .
900+
901+
op metaTokenize : #String #String -> #QidList .
902+
903+
op breaksToken : #Char -> #Bool .
904+
905+
op mainModule : -> #Qid .
906+
907+
eq string2term(S:#String) = getTermRP(metaParse(upModule(mainModule, false), metaTokenize("", S:#String), anyTypeMeta)) .
908+
eq string2k(S:#String) = downTerm(string2term(S:#String), .K) .
909+
eq string2bag(S:#String) = downTerm(string2term(S:#String), .Bag) .
910+
911+
ceq metaTokenize(Prefix:#String, S:#String) = if Prefix:#String ==String "" then nilQidList else qid(Prefix:#String) fi plQidList qid(substrString(S:#String, 0, 1)) plQidList metaTokenize("", substrString(S:#String, 1, lengthString(S:#String))) if breaksToken(substrString(S:#String, 0, 1)) and-then substrString(Prefix:#String, 0, 1) =/=Universal "\"" .
912+
ceq metaTokenize(Prefix:#String, S:#String) = if Prefix:#String ==String "" then nilQidList else qid(Prefix:#String) fi plQidList metaTokenize("", substrString(S:#String, 1, lengthString(S:#String))) if substrString(S:#String, 0, 1) ==String " " and-then substrString(Prefix:#String, 0, 1) =/=Universal "\"" .
913+
ceq metaTokenize(Prefix:#String, S:#String) = metaTokenize(Prefix:#String +String substrString(S:#String, 0, 2), substrString(S:#String, 2, lengthString(S:#String))) if substrString(S:#String, 0, 1) ==String "\\" and-then substrString(Prefix:#String, 0, 1) ==String "\"" .
914+
ceq metaTokenize(Prefix:#String, S:#String) = qid(Prefix:#String +String "\"") plQidList metaTokenize("", substrString(S:#String, 1, lengthString(S:#String))) if substrString(S:#String, 0, 1) ==String "\"" and-then substrString(Prefix:#String, 0, 1) ==String "\"" .
915+
ceq metaTokenize(Prefix:#String, S:#String) = metaTokenize(Prefix:#String +String substrString(S:#String, 0, 2), substrString(S:#String, 2, lengthString(S:#String))) if substrString(S:#String, 0, 1) ==String "`" .
916+
eq metaTokenize(Prefix:#String, "") = if Prefix:#String ==String "" then nilQidList else qid(Prefix:#String) fi [label metaTokenize-finish] .
917+
eq metaTokenize(Prefix:#String, S:#String) = metaTokenize(Prefix:#String +String substrString(S:#String, 0, 1), substrString(S:#String, 1, lengthString(S:#String))) [owise] .
918+
919+
920+
eq breaksToken("{") = true .
921+
eq breaksToken("}") = true .
922+
eq breaksToken("[") = true .
923+
eq breaksToken("]") = true .
924+
eq breaksToken("(") = true .
925+
eq breaksToken(")") = true .
926+
eq breaksToken(",") = true .
927+
eq breaksToken(C:#Char) = false [owise] .
928+
929+
endm
930+
931+
mod #K-PRINTER is
932+
including #K-PARSER .
933+
934+
op k2string : K -> #String .
935+
op bag2string : Bag -> #String .
936+
op term2string : #Term -> #String .
937+
938+
eq k2string(K:K) = term2string(upTerm(K:K)) .
939+
eq bag2string(B:Bag) = term2string(upTerm(B:Bag)) .
940+
941+
eq term2string(T:#Term) = metaDetokenize(metaPrettyPrint(upModule(mainModule, false), T:#Term, nonePOS)) .
942+
943+
op metaDetokenize : #QidList -> #String .
944+
op convertToken : #String -> #String .
945+
946+
eq metaDetokenize(Q:#Qid plQidList L:#QidList) = convertToken(string(Q:#Qid)) +String " " +String metaDetokenize(L:#QidList) .
947+
eq metaDetokenize(nilQidList) = "" .
948+
949+
eq convertToken("`{") = "{" .
950+
eq convertToken("`}") = "}" .
951+
eq convertToken("`[") = "[" .
952+
eq convertToken("`]") = "]" .
953+
eq convertToken("`(") = "(" .
954+
eq convertToken("`)") = ")" .
955+
eq convertToken("`,") = "," .
956+
eq convertToken(S:#String) = S:#String [owise] .
957+
958+
endm
959+
888960
load k-model-checker
889961
load socket.maude
890962
load TCPSupport
891963
load smt.maude
892-
--- load pl-meta-level
893964

894965

895966
mod BUILTINS is

‎dist/bin/native/linux/FastKast.REMOVED.git-id‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
c1fef7a9506f8620a3ca23250648f565f39c9f17

‎dist/bin/native/linux/baffle‎

869 KB
Binary file not shown.

‎dist/bin/native/linux/sglr.REMOVED.git-id‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
cdd1bf8e566925c1c11e6140f0d359ecff748176

‎dist/bin/native/macosx/FastKast.REMOVED.git-id‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
90571d6805eb98b524ac59ab68e143399e54b687

0 commit comments

Comments
 (0)