1 package acl2s.lib.parse.no_obj;
2
3 import static acl2s.lib.parse.obj.Sym.acl2PkgName;
4 import static acl2s.lib.parse.obj.Sym.keywordPkgName;
5 import acl2s.lib.parse.ObjectNotSupported;
6 import acl2s.lib.parse.IParseContext;
7 import acl2s.lib.parse.ParseException;
8 import acl2s.lib.parse.Parser;
9 import acl2s.lib.parse.SymOrNumFns;
10
11 public class Sym extends SymOrNum {
12 public static void parse(Parser p) throws ParseException {
13 char c = p.peek();
14 if (c == '(') {
15 p.advance(1);
16 p.skipSpaceAndComments();
17 if (p.peek() != ')') {
18 throw new ParseException("Expected: ()");
19 }
20 p.advance(1);
21 return;
22 }
23 if (c == '.') {
24 int i = 1;
25 while (p.peek(i) == '.') i++;
26 if (SymOrNumFns.isTerminator(p.peek(i))) {
27 p.advance(i);
28 throw new ParseException("Illegal dot(s).");
29 }
30 } else if (c == '#') {
31 p.advance(1);
32 p.skipToTerminator();
33 throw new ParseException("Unrecognized #-sequence");
34 }
35 if (SymOrNumFns.isTerminator(p.peek())) {
36 p.skip();
37 throw new ParseException("Symbol expected.");
38 }
39 StringBuilder s1 = new StringBuilder();
40 boolean mustBeExternal = false;
41 boolean firstCharColon = false;
42 c = p.peek();
43 if (c == ':' && p.peek(1) != ':') {
44 firstCharColon = true;
45 p.skip();
46 // p.skipSpace(); // GCL-ism. not portable
47 c = p.peek();
48 if (SymOrNumFns.isTerminator(c)) {
49 throw new ParseException("For portability, symbol syntax must immediately follow package delimiter.");
50 }
51 }
52 while (!SymOrNumFns.isTerminator(c) && (firstCharColon || c != ':')) {
53 if (c == '\\') {
54 c = p.next();
55 if (c == Parser.EOF) throw new ParseException("EOF after \\.");
56 s1.append(c);
57 } else if (c == '|') {
58 c = p.next();
59 while (c != '|' && c != Parser.EOF) {
60 if (c == '\\') {
61 c = p.next();
62 if (c == Parser.EOF) throw new ParseException("EOF after \\.");
63 s1.append(c);
64 } else if (c == '\n' || c == '\r') {
65 throw new ParseException("Unescaped newlines in symbols are not supported in ACL2s.");
66 } else {
67 s1.append(c);
68 }
69 c = p.next();
70 }
71 if (c == Parser.EOF) throw new ParseException("EOF before matching |.");
72 } else {
73 s1.append(Character.toUpperCase(c));
74 }
75 c = p.next();
76 }
77 if (firstCharColon) {
78 create(p.getContext(),keywordPkgName,s1.toString());
79 } else if (c == ':') {
80 StringBuilder s2 = new StringBuilder();
81 p.skip();
82 if (p.peek() == ':') {
83 p.skip();
84 } else {
85 mustBeExternal = true;
86 }
87 // p.skipSpace(); // GCL-ism. not portable
88 c = p.peek();
89 if (SymOrNumFns.isTerminator(c)) {
90 throw new ParseException("For portability, symbol syntax must immediately follow package delimiter.");
91 }
92 do {
93 if (c == '\\') {
94 c = p.next();
95 if (c == Parser.EOF) throw new ParseException("EOF after \\.");
96 s2.append(c);
97 } else if (c == '|') {
98 c = p.next();
99 while (c != '|' && c != Parser.EOF) {
100 if (c == '\\') {
101 c = p.next();
102 if (c == Parser.EOF) throw new ParseException("EOF after \\.");
103 s2.append(c);
104 } else if (c == '\n' || c == '\r') {
105 throw new ParseException("Unescaped newlines in symbols are not supported in ACL2s.");
106 } else {
107 s2.append(c);
108 }
109 c = p.next();
110 }
111 if (c == Parser.EOF) throw new ParseException("EOF before matching |.");
112 } else if (c == ':') {
113 p.skipToTerminator();
114 throw new ParseException("Extra : after :: in symbol designator.");
115 } else {
116 s2.append(Character.toUpperCase(c));
117 }
118 c = p.next();
119 } while (!SymOrNumFns.isTerminator(c));
120 create(p.getContext(),s1.toString(),s2.toString(),mustBeExternal);
121 } else {
122 create(p.getContext(),s1.toString());
123 }
124 }
125
126 public static void createACL2(IParseContext pc, String sym) {
127 try {
128 create(pc,acl2PkgName,sym);
129 } catch (ParseException e) {
130 e.printStackTrace(); // won't happen
131 }
132 }
133
134 public static void create(IParseContext pc, String sym) throws ParseException {
135 create(pc,null,sym);
136 }
137
138 public static void create(IParseContext pc, String pack, String sym) throws ParseException {
139 create(pc,pack,sym,false);
140 }
141
142 public static void create(IParseContext pc, String pack, String sym, boolean external)
143 throws ParseException {
144 if (external) {
145 throw new ObjectNotSupported("External symbol references not supported in ACL2. Use '::'.");
146 }
147 if (pack == null) {
148 if (pc != null) {
149 pack = pc.getDefaultPackage();
150 }
151 if (pack == null) { // don't know what package it's supposed to go in
152 return;// new UnpackagedSym(sym);
153 }
154 }
|
Event do_not_call: |
"java.lang.String.toUpperCase()" implicitly uses the environment's default character set, which might lead to unexpected behavior. Consider using toUpperCase(Locale locale). |
155 if (!pack.equals(pack.toUpperCase())) {
156 throw new ObjectNotSupported("Package names may not contain lower-case characters.");
157 }
158 if (pack.equals("")) {
159 throw new ObjectNotSupported("The empty string is not a valid ACL2 package name.");
160 }
161 String truePack = null;
162 if (pc != null) {
163 truePack = pc.internedPackage(pack,sym); // could throw NoSuchPackageException
164 }
165 if (truePack == null) { // unknown how it should be interned
166 return;// new UninternedSym(pack,sym);
167 } else {
168 return;// SymDb.get(truePack,sym);
169 }
170 }
171 }