Skip to content

Commit 79389ef

Browse files
daejunparkdaejunpark
committed
fix prelude modules
1 parent 6e6ed1e commit 79389ef

7 files changed

+142
-130
lines changed

‎autoinclude-java.k

-24
This file was deleted.

‎js-core-syntax.k

+10
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,15 @@
1+
require "builtins/bool.k"
2+
require "builtins/int.k"
3+
require "builtins/float.k"
4+
require "builtins/string.k"
5+
16
module JS-CORE-SYNTAX
27

8+
imports BOOL-SYNTAX-HOOKS
9+
imports INT-SYNTAX-HOOKS
10+
imports FLOAT-SYNTAX-HOOKS
11+
imports STRING-SYNTAX-HOOKS
12+
313
syntax Pgm ::= Stmt
414

515
syntax Stmt ::= "%fdecl" "(" Var "," Exps "," Stmt ")"

‎js-main.k

+2-6
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,6 @@
1-
require "builtins/mint.k"
2-
//require "modules/substitution.k"
3-
require "modules/k-functional-visitor.k"
41
require "js-trans.k"
52
require "js-str-numeric-literal.k"
3+
require "js-prelude.k"
64

75
module JS-SYNTAX
86
imports JS-ORIG-SYNTAX
@@ -11,11 +9,9 @@ endmodule
119

1210
module JS
1311

14-
imports MINT
15-
//imports SUBSTITUTION
16-
imports K-FUNCTIONAL-VISITOR
1712
imports JS-SYNTAX
1813
imports JS-TRANS
14+
imports JS-PRELUDE
1915

2016
//////////////////////////////////////////////////////////////////////////////
2117
// Configuration

‎js-orig-syntax-util.k

+120
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,120 @@
1+
require "builtins/bool.k"
2+
require "builtins/int.k"
3+
require "builtins/float.k"
4+
require "builtins/string.k"
5+
6+
module JS-ORIG-SYNTAX-UTIL
7+
8+
imports JS-ORIG-SYNTAX
9+
10+
imports BOOL-HOOKS
11+
imports INT-HOOKS
12+
imports FLOAT-HOOKS
13+
imports STRING-HOOKS
14+
15+
// Name
16+
17+
syntax String ::= StringOfName(Name) [function, notInPrograms]
18+
rule StringOfName(N:Name) => #tokenToString(N)
19+
20+
syntax Name ::= NameOfString(String) [function, notInPrograms]
21+
rule NameOfString(S:String) => #parseToken("Name", S)
22+
23+
// APIName
24+
25+
syntax String ::= StringOfAPIName(APIName) [function, notInPrograms]
26+
rule StringOfAPIName(N:APIName) => #tokenToString(N)
27+
28+
// MyFloat
29+
30+
syntax Float ::= "MyFloat2Float" "(" MyFloat ")" [function, notInPrograms]
31+
rule MyFloat2Float(F:MyFloat) => String2Float(#tokenToString(F))
32+
33+
// MyString
34+
35+
syntax String ::= "MyString2String" "(" MyString ")" [function, notInPrograms]
36+
rule MyString2String(S:MyString) => processEscapes(processBackslashes(processQuotes(#tokenToString(S))))
37+
38+
syntax String ::= "processQuotes" "(" String ")" [function, notInPrograms]
39+
rule processQuotes(S:String) => replaceAll(substrString(S, 1, lengthString(S) -Int 1), "\\\"", "\"") when substrString(S,0,1) ==String "\""
40+
rule processQuotes(S:String) => replaceAll(substrString(S, 1, lengthString(S) -Int 1), "\\'", "'") when substrString(S,0,1) ==String "'"
41+
42+
syntax String ::= "processBackslashes" "(" String ")" [function, notInPrograms]
43+
rule processBackslashes(S:String) => substrString(S, 0, findString(S, "\\", 0)) +String processBackslashesAux(substrString(S, findString(S, "\\", 0), lengthString(S))) when findString(S, "\\", 0) =/=Int -1
44+
rule processBackslashes(S:String) => S when findString(S, "\\", 0) ==Int -1
45+
46+
syntax String ::= "processBackslashesAux" "(" String ")" [function, notInPrograms]
47+
rule processBackslashesAux(S:String) => processBackslashesAuxAux(S) when lengthString(S) >Int 1
48+
rule processBackslashesAux(S:String) => S when lengthString(S) ==Int 1
49+
50+
syntax String ::= "processBackslashesAuxAux" "(" String ")" [function, notInPrograms]
51+
rule processBackslashesAuxAux(S:String) => processBackslashes(substrString(S,1,lengthString(S))) when notBool(isEscapeChar(substrString(S,1,2)))
52+
rule processBackslashesAuxAux(S:String) => substrString(S,0,2) +String processBackslashes(substrString(S,2,lengthString(S))) when isEscapeChar(substrString(S,1,2))
53+
54+
syntax Bool ::= "isEscapeChar" "(" String ")" [function, notInPrograms]
55+
rule isEscapeChar(S:String) => S ==String "b"
56+
orBool S ==String "t"
57+
orBool S ==String "n"
58+
orBool S ==String "v"
59+
orBool S ==String "f"
60+
orBool S ==String "r"
61+
orBool S ==String "\\"
62+
//
63+
orBool S ==String "0"
64+
//
65+
orBool S ==String "\n"
66+
orBool S ==String "\r"
67+
orBool S ==String "\u2028"
68+
orBool S ==String "\u2029"
69+
//
70+
orBool S ==String "x"
71+
orBool S ==String "u"
72+
73+
syntax String ::= "processEscapes" "(" String ")" [function, notInPrograms]
74+
rule processEscapes(S:String) => S when findString(S, "\\b" , 0) ==Int -1
75+
andBool findString(S, "\\t" , 0) ==Int -1
76+
andBool findString(S, "\\n" , 0) ==Int -1
77+
andBool findString(S, "\\v" , 0) ==Int -1
78+
andBool findString(S, "\\f" , 0) ==Int -1
79+
andBool findString(S, "\\r" , 0) ==Int -1
80+
andBool findString(S, "\\\\" , 0) ==Int -1
81+
//
82+
andBool findString(S, "\\0" , 0) ==Int -1
83+
//
84+
andBool findString(S, "\\\n" , 0) ==Int -1
85+
andBool findString(S, "\\\r" , 0) ==Int -1
86+
andBool findString(S, "\\\r\n" , 0) ==Int -1
87+
andBool findString(S, "\\\u2028" , 0) ==Int -1
88+
andBool findString(S, "\\\u2029" , 0) ==Int -1
89+
//
90+
andBool findString(S, "\\x" , 0) ==Int -1
91+
andBool findString(S, "\\u" , 0) ==Int -1
92+
// \ [one of ' " \ b f n r t v]
93+
rule processEscapes(S:String) => processEscapes(replaceAll(S, "\\b" , "\u0008")) when findString(S, "\\b" , 0) =/=Int -1
94+
rule processEscapes(S:String) => processEscapes(replaceAll(S, "\\t" , "\t" )) when findString(S, "\\t" , 0) =/=Int -1
95+
rule processEscapes(S:String) => processEscapes(replaceAll(S, "\\n" , "\n" )) when findString(S, "\\n" , 0) =/=Int -1
96+
rule processEscapes(S:String) => processEscapes(replaceAll(S, "\\v" , "\u000B")) when findString(S, "\\v" , 0) =/=Int -1
97+
rule processEscapes(S:String) => processEscapes(replaceAll(S, "\\f" , "\f" )) when findString(S, "\\f" , 0) =/=Int -1
98+
rule processEscapes(S:String) => processEscapes(replaceAll(S, "\\r" , "\r" )) when findString(S, "\\r" , 0) =/=Int -1
99+
rule processEscapes(S:String) => processEscapes(replaceAll(S, "\\\\" , "\\" )) when findString(S, "\\\\" , 0) =/=Int -1
100+
// \ 0 [lookahead \not\in DecimalDigit]
101+
// FIXME: check if lookahead is not a decimal degit.
102+
rule processEscapes(S:String) => processEscapes(replaceAll(S, "\\0" , "\u0000")) when findString(S, "\\0" , 0) =/=Int -1
103+
// LineContinuation ::= \ LineTerminatorSequence
104+
rule processEscapes(S:String) => processEscapes(replaceAll(S, "\\\n" , "" )) when findString(S, "\\\n" , 0) =/=Int -1
105+
rule processEscapes(S:String) => processEscapes(replaceAll(S, "\\\r" , "" )) when findString(S, "\\\r" , 0) =/=Int -1 andBool findString(S, "\\\r\n", 0) ==Int -1
106+
rule processEscapes(S:String) => processEscapes(replaceAll(S, "\\\r\n" , "" )) when findString(S, "\\\r\n" , 0) =/=Int -1
107+
rule processEscapes(S:String) => processEscapes(replaceAll(S, "\\\u2028", "" )) when findString(S, "\\\u2028", 0) =/=Int -1
108+
rule processEscapes(S:String) => processEscapes(replaceAll(S, "\\\u2029", "" )) when findString(S, "\\\u2029", 0) =/=Int -1
109+
// HexEscapeSequence ::= x HexDigit HexDigit
110+
// UnicodeEscapeSequence ::= u HexDigit HexDigit HexDigit HexDigit
111+
rule processEscapes(S:String) => processEscapes(processHexEscapes (S, findString(S, "\\x", 0))) when findString(S, "\\x", 0) =/=Int -1
112+
rule processEscapes(S:String) => processEscapes(processUnicodeEscapes(S, findString(S, "\\u", 0))) when findString(S, "\\u", 0) =/=Int -1
113+
114+
syntax String ::= "processHexEscapes" "(" String "," Int ")" [function, notInPrograms]
115+
rule processHexEscapes (S:String, I:Int) => substrString(S, 0, I) +String chrChar(String2Base(substrString(S, I +Int 2, I +Int 2 +Int 2), 16)) +String substrString(S, I +Int 2 +Int 2, lengthString(S))
116+
117+
syntax String ::= "processUnicodeEscapes" "(" String "," Int ")" [function, notInPrograms]
118+
rule processUnicodeEscapes(S:String, I:Int) => substrString(S, 0, I) +String chrChar(String2Base(substrString(S, I +Int 2, I +Int 2 +Int 4), 16)) +String substrString(S, I +Int 2 +Int 4, lengthString(S))
119+
120+
endmodule

‎js-orig-syntax.k

+6-99
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,11 @@
1+
require "builtins/bool.k"
2+
require "builtins/int.k"
3+
14
module JS-ORIG-SYNTAX
25

6+
imports BOOL-SYNTAX-HOOKS
7+
imports INT-SYNTAX-HOOKS
8+
39
// Based on ECMA-262, 5.1 Edition, June 2011
410

511
// A.5 Programs
@@ -214,109 +220,10 @@ syntax Expression ::= LeftExpression
214220
| LeftExpression "^=" Expression [right]
215221
| LeftExpression "|=" Expression [right]
216222

217-
218-
// Utils
219-
syntax String ::= StringOfName(Name) [function, notInPrograms]
220-
rule StringOfName(N:Name) => #tokenToString(N)
221-
//
222-
syntax Name ::= NameOfString(String) [function, notInPrograms]
223-
rule NameOfString(S:String) => #parseToken("Name", S)
224-
225-
syntax Float ::= "MyFloat2Float" "(" MyFloat ")" [function, notInPrograms]
226-
rule MyFloat2Float(F:MyFloat) => String2Float(#tokenToString(F))
227-
228-
syntax String ::= "MyString2String" "(" MyString ")" [function, notInPrograms]
229-
rule MyString2String(S:MyString) => processEscapes(processBackslashes(processQuotes(#tokenToString(S))))
230-
231-
syntax String ::= "processQuotes" "(" String ")" [function, notInPrograms]
232-
rule processQuotes(S:String) => replaceAll(substrString(S, 1, lengthString(S) -Int 1), "\\\"", "\"") when substrString(S,0,1) ==String "\""
233-
rule processQuotes(S:String) => replaceAll(substrString(S, 1, lengthString(S) -Int 1), "\\'", "'") when substrString(S,0,1) ==String "'"
234-
235-
syntax String ::= "processBackslashes" "(" String ")" [function, notInPrograms]
236-
rule processBackslashes(S:String) => substrString(S, 0, findString(S, "\\", 0)) +String processBackslashesAux(substrString(S, findString(S, "\\", 0), lengthString(S))) when findString(S, "\\", 0) =/=Int -1
237-
rule processBackslashes(S:String) => S when findString(S, "\\", 0) ==Int -1
238-
239-
syntax String ::= "processBackslashesAux" "(" String ")" [function, notInPrograms]
240-
rule processBackslashesAux(S:String) => processBackslashesAuxAux(S) when lengthString(S) >Int 1
241-
rule processBackslashesAux(S:String) => S when lengthString(S) ==Int 1
242-
243-
syntax String ::= "processBackslashesAuxAux" "(" String ")" [function, notInPrograms]
244-
rule processBackslashesAuxAux(S:String) => processBackslashes(substrString(S,1,lengthString(S))) when notBool(isEscapeChar(substrString(S,1,2)))
245-
rule processBackslashesAuxAux(S:String) => substrString(S,0,2) +String processBackslashes(substrString(S,2,lengthString(S))) when isEscapeChar(substrString(S,1,2))
246-
247-
syntax Bool ::= "isEscapeChar" "(" String ")" [function, notInPrograms]
248-
rule isEscapeChar(S:String) => S ==String "b"
249-
orBool S ==String "t"
250-
orBool S ==String "n"
251-
orBool S ==String "v"
252-
orBool S ==String "f"
253-
orBool S ==String "r"
254-
orBool S ==String "\\"
255-
//
256-
orBool S ==String "0"
257-
//
258-
orBool S ==String "\n"
259-
orBool S ==String "\r"
260-
orBool S ==String "\u2028"
261-
orBool S ==String "\u2029"
262-
//
263-
orBool S ==String "x"
264-
orBool S ==String "u"
265-
266-
syntax String ::= "processEscapes" "(" String ")" [function, notInPrograms]
267-
rule processEscapes(S:String) => S when findString(S, "\\b" , 0) ==Int -1
268-
andBool findString(S, "\\t" , 0) ==Int -1
269-
andBool findString(S, "\\n" , 0) ==Int -1
270-
andBool findString(S, "\\v" , 0) ==Int -1
271-
andBool findString(S, "\\f" , 0) ==Int -1
272-
andBool findString(S, "\\r" , 0) ==Int -1
273-
andBool findString(S, "\\\\" , 0) ==Int -1
274-
//
275-
andBool findString(S, "\\0" , 0) ==Int -1
276-
//
277-
andBool findString(S, "\\\n" , 0) ==Int -1
278-
andBool findString(S, "\\\r" , 0) ==Int -1
279-
andBool findString(S, "\\\r\n" , 0) ==Int -1
280-
andBool findString(S, "\\\u2028" , 0) ==Int -1
281-
andBool findString(S, "\\\u2029" , 0) ==Int -1
282-
//
283-
andBool findString(S, "\\x" , 0) ==Int -1
284-
andBool findString(S, "\\u" , 0) ==Int -1
285-
// \ [one of ' " \ b f n r t v]
286-
rule processEscapes(S:String) => processEscapes(replaceAll(S, "\\b" , "\u0008")) when findString(S, "\\b" , 0) =/=Int -1
287-
rule processEscapes(S:String) => processEscapes(replaceAll(S, "\\t" , "\t" )) when findString(S, "\\t" , 0) =/=Int -1
288-
rule processEscapes(S:String) => processEscapes(replaceAll(S, "\\n" , "\n" )) when findString(S, "\\n" , 0) =/=Int -1
289-
rule processEscapes(S:String) => processEscapes(replaceAll(S, "\\v" , "\u000B")) when findString(S, "\\v" , 0) =/=Int -1
290-
rule processEscapes(S:String) => processEscapes(replaceAll(S, "\\f" , "\f" )) when findString(S, "\\f" , 0) =/=Int -1
291-
rule processEscapes(S:String) => processEscapes(replaceAll(S, "\\r" , "\r" )) when findString(S, "\\r" , 0) =/=Int -1
292-
rule processEscapes(S:String) => processEscapes(replaceAll(S, "\\\\" , "\\" )) when findString(S, "\\\\" , 0) =/=Int -1
293-
// \ 0 [lookahead \not\in DecimalDigit]
294-
// FIXME: check if lookahead is not a decimal degit.
295-
rule processEscapes(S:String) => processEscapes(replaceAll(S, "\\0" , "\u0000")) when findString(S, "\\0" , 0) =/=Int -1
296-
// LineContinuation ::= \ LineTerminatorSequence
297-
rule processEscapes(S:String) => processEscapes(replaceAll(S, "\\\n" , "" )) when findString(S, "\\\n" , 0) =/=Int -1
298-
rule processEscapes(S:String) => processEscapes(replaceAll(S, "\\\r" , "" )) when findString(S, "\\\r" , 0) =/=Int -1 andBool findString(S, "\\\r\n", 0) ==Int -1
299-
rule processEscapes(S:String) => processEscapes(replaceAll(S, "\\\r\n" , "" )) when findString(S, "\\\r\n" , 0) =/=Int -1
300-
rule processEscapes(S:String) => processEscapes(replaceAll(S, "\\\u2028", "" )) when findString(S, "\\\u2028", 0) =/=Int -1
301-
rule processEscapes(S:String) => processEscapes(replaceAll(S, "\\\u2029", "" )) when findString(S, "\\\u2029", 0) =/=Int -1
302-
// HexEscapeSequence ::= x HexDigit HexDigit
303-
// UnicodeEscapeSequence ::= u HexDigit HexDigit HexDigit HexDigit
304-
rule processEscapes(S:String) => processEscapes(processHexEscapes (S, findString(S, "\\x", 0))) when findString(S, "\\x", 0) =/=Int -1
305-
rule processEscapes(S:String) => processEscapes(processUnicodeEscapes(S, findString(S, "\\u", 0))) when findString(S, "\\u", 0) =/=Int -1
306-
307-
syntax String ::= "processHexEscapes" "(" String "," Int ")" [function, notInPrograms]
308-
rule processHexEscapes (S:String, I:Int) => substrString(S, 0, I) +String chrChar(String2Base(substrString(S, I +Int 2, I +Int 2 +Int 2), 16)) +String substrString(S, I +Int 2 +Int 2, lengthString(S))
309-
310-
syntax String ::= "processUnicodeEscapes" "(" String "," Int ")" [function, notInPrograms]
311-
rule processUnicodeEscapes(S:String, I:Int) => substrString(S, 0, I) +String chrChar(String2Base(substrString(S, I +Int 2, I +Int 2 +Int 4), 16)) +String substrString(S, I +Int 2 +Int 4, lengthString(S))
312-
313223
// Internal Semantic Methods API Call
314224

315225
syntax CallExpression ::= APIName "(" Expressions ")"
316226

317227
syntax APIName ::= Token{[\@][\_\$A-Za-z0-9]*} [notInRules]
318228

319-
syntax String ::= StringOfAPIName(APIName) [function, notInPrograms]
320-
rule StringOfAPIName(N:APIName) => #tokenToString(N)
321-
322229
endmodule

‎js-trans.k

+3
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,14 @@
11
require "js-orig-syntax.k"
2+
require "js-orig-syntax-util.k"
23
require "js-core-syntax.k"
34

45
module JS-TRANS
56

67
imports JS-ORIG-SYNTAX
78
imports JS-CORE-SYNTAX
89

10+
imports JS-ORIG-SYNTAX-UTIL
11+
912
// top-level
1013
syntax Stmt ::= "^SourceElements" "(" SourceElements ")" [function]
1114
rule ^SourceElements(S:SourceElement Ss:SourceElements) => %seq(^SourceElement(S), ^SourceElements(Ss)) when Ss =/=K .SourceElements

‎kbuild.sh

+1-1
Original file line numberDiff line numberDiff line change
@@ -4,4 +4,4 @@ dir=`dirname $0`
44

55
echo "rule @PWD => \"`pwd`\"" >$dir/js-pwd.k
66
$dir/kpp.py $dir/js-main.k >$dir/js.k
7-
$dir/k/bin/kompile --backend java $dir/js.k
7+
$dir/k/bin/kompile --no-prelude --backend java $dir/js.k

0 commit comments

Comments
 (0)