diff options
author | Kristóf Marussy <kristof@marussy.com> | 2024-02-20 01:27:51 +0100 |
---|---|---|
committer | Kristóf Marussy <kristof@marussy.com> | 2024-04-07 14:55:46 +0200 |
commit | 01960723de5ca42e28dc8f162d4fe9e24c23c0b8 (patch) | |
tree | c391738a378d079d4c3b1aa8966c6b66d60ee4c9 /subprojects/frontend/src/language | |
parent | feat: subproject for z3 integration (diff) | |
download | refinery-01960723de5ca42e28dc8f162d4fe9e24c23c0b8.tar.gz refinery-01960723de5ca42e28dc8f162d4fe9e24c23c0b8.tar.zst refinery-01960723de5ca42e28dc8f162d4fe9e24c23c0b8.zip |
feat(language): datatype declarations
Also changes ReferenceDeclaration to declare attributes, since reference and
attributes can only be distinguished at linking time.
Diffstat (limited to 'subprojects/frontend/src/language')
-rw-r--r-- | subprojects/frontend/src/language/problem.grammar | 19 | ||||
-rw-r--r-- | subprojects/frontend/src/language/problemLanguageSupport.ts | 8 |
2 files changed, 14 insertions, 13 deletions
diff --git a/subprojects/frontend/src/language/problem.grammar b/subprojects/frontend/src/language/problem.grammar index b69ee73f..32f76f6a 100644 --- a/subprojects/frontend/src/language/problem.grammar +++ b/subprojects/frontend/src/language/problem.grammar | |||
@@ -42,6 +42,9 @@ statement { | |||
42 | kw<"enum"> RelationName | 42 | kw<"enum"> RelationName |
43 | (EnumBody { "{" sep<",", AtomNodeName> "}" } | ".") | 43 | (EnumBody { "{" sep<",", AtomNodeName> "}" } | ".") |
44 | } | | 44 | } | |
45 | DatatypeDeclaration { | ||
46 | kw<"extern"> kw<"datatype"> DatatypeName "." | ||
47 | } | | ||
45 | PredicateDefinition { | 48 | PredicateDefinition { |
46 | ( | 49 | ( |
47 | (kw<"error"> | ckw<"contained"> | kw<"containment">)? kw<"pred"> | | 50 | (kw<"error"> | ckw<"contained"> | kw<"containment">)? kw<"pred"> | |
@@ -50,10 +53,10 @@ statement { | |||
50 | RelationName ParameterList<Parameter>? | 53 | RelationName ParameterList<Parameter>? |
51 | PredicateBody { ("<->" sep<OrOp, Conjunction>)? "." } | 54 | PredicateBody { ("<->" sep<OrOp, Conjunction>)? "." } |
52 | } | | 55 | } | |
53 | FunctionDefinition { | 56 | // FunctionDefinition { |
54 | kw<"fn"> PrimitiveType RelationName ParameterList<Parameter>? | 57 | // kw<"fn"> RelationName RelationName ParameterList<Parameter>? |
55 | FunctionBody { ("=" sep<OrOp, Case>)? "." } | 58 | // FunctionBody { ("=" sep<OrOp, Case>)? "." } |
56 | } | | 59 | // } | |
57 | //RuleDefinition { | 60 | //RuleDefinition { |
58 | // kw<"rule"> | 61 | // kw<"rule"> |
59 | // RuleName ParameterList<Parameter>? | 62 | // RuleName ParameterList<Parameter>? |
@@ -77,7 +80,7 @@ FeatureDeclaration { | |||
77 | ReferenceKind !feature ~featureHead | 80 | ReferenceKind !feature ~featureHead |
78 | } | | 81 | } | |
79 | FeatureDeclarationHeadWithoutKind { | 82 | FeatureDeclarationHeadWithoutKind { |
80 | (PrimitiveType | kw<"bool">)? ~featureHead | 83 | ~featureHead |
81 | } | 84 | } |
82 | ) | 85 | ) |
83 | RelationName | 86 | RelationName |
@@ -137,10 +140,6 @@ ReferenceKind { | |||
137 | kw<"refers"> | ckw<"contains"> | kw<"container"> | 140 | kw<"refers"> | ckw<"contains"> | kw<"container"> |
138 | } | 141 | } |
139 | 142 | ||
140 | PrimitiveType { | ||
141 | kw<"int"> | kw<"real"> | kw<"string"> | ||
142 | } | ||
143 | |||
144 | LogicValue { | 143 | LogicValue { |
145 | kw<"true"> | kw<"false"> | kw<"unknown"> | kw<"error"> | 144 | kw<"true"> | kw<"false"> | kw<"unknown"> | kw<"error"> |
146 | } | 145 | } |
@@ -165,6 +164,8 @@ Multiplicity { (IntMult "..")? (IntMult | StarMult)} | |||
165 | // but will go with the transtive closure (and highlight `a` as a relation) if forced. | 164 | // but will go with the transtive closure (and highlight `a` as a relation) if forced. |
166 | RelationName { QualifiedName ~name } | 165 | RelationName { QualifiedName ~name } |
167 | 166 | ||
167 | DatatypeName { QualifiedName } | ||
168 | |||
168 | //RuleName { QualifiedName } | 169 | //RuleName { QualifiedName } |
169 | 170 | ||
170 | AtomNodeName { QualifiedName } | 171 | AtomNodeName { QualifiedName } |
diff --git a/subprojects/frontend/src/language/problemLanguageSupport.ts b/subprojects/frontend/src/language/problemLanguageSupport.ts index 14826363..9500fbf2 100644 --- a/subprojects/frontend/src/language/problemLanguageSupport.ts +++ b/subprojects/frontend/src/language/problemLanguageSupport.ts | |||
@@ -28,11 +28,10 @@ const parserWithMetadata = parser.configure({ | |||
28 | LineComment: t.lineComment, | 28 | LineComment: t.lineComment, |
29 | BlockComment: t.blockComment, | 29 | BlockComment: t.blockComment, |
30 | 'module problem class enum pred fn scope': t.definitionKeyword, | 30 | 'module problem class enum pred fn scope': t.definitionKeyword, |
31 | 'import as declare atom multi': t.definitionKeyword, | 31 | 'import as declare atom multi extern datatype': t.definitionKeyword, |
32 | 'abstract extends refers contains container opposite': t.modifier, | 32 | 'abstract extends refers contains container opposite': t.modifier, |
33 | 'default error contained containment': t.modifier, | 33 | 'default error contained containment': t.modifier, |
34 | 'true false unknown error': t.keyword, | 34 | 'true false unknown error': t.keyword, |
35 | 'int real string bool': t.keyword, | ||
36 | 'may must current count': t.operatorKeyword, | 35 | 'may must current count': t.operatorKeyword, |
37 | 'sum prod min max in': t.operatorKeyword, | 36 | 'sum prod min max in': t.operatorKeyword, |
38 | // 'new delete': t.keyword, | 37 | // 'new delete': t.keyword, |
@@ -44,6 +43,7 @@ const parserWithMetadata = parser.configure({ | |||
44 | StarMult: t.number, | 43 | StarMult: t.number, |
45 | String: t.string, | 44 | String: t.string, |
46 | 'RelationName/QualifiedName': t.typeName, | 45 | 'RelationName/QualifiedName': t.typeName, |
46 | 'DatatypeName/QualifiedName': t.keyword, | ||
47 | // 'RuleName/QualifiedName': t.typeName, | 47 | // 'RuleName/QualifiedName': t.typeName, |
48 | 'AtomNodeName/QualifiedName': t.atom, | 48 | 'AtomNodeName/QualifiedName': t.atom, |
49 | 'VariableName/QualifiedName': t.variableName, | 49 | 'VariableName/QualifiedName': t.variableName, |
@@ -60,7 +60,7 @@ const parserWithMetadata = parser.configure({ | |||
60 | NodeDeclaration: indentDeclaration, | 60 | NodeDeclaration: indentDeclaration, |
61 | ScopeDeclaration: indentDeclaration, | 61 | ScopeDeclaration: indentDeclaration, |
62 | PredicateBody: indentPredicateOrRule, | 62 | PredicateBody: indentPredicateOrRule, |
63 | FunctionBody: indentPredicateOrRule, | 63 | // FunctionBody: indentPredicateOrRule, |
64 | // RuleBody: indentPredicateOrRule, | 64 | // RuleBody: indentPredicateOrRule, |
65 | BlockComment: indentBlockComment, | 65 | BlockComment: indentBlockComment, |
66 | }), | 66 | }), |
@@ -69,7 +69,7 @@ const parserWithMetadata = parser.configure({ | |||
69 | EnumBody: foldInside, | 69 | EnumBody: foldInside, |
70 | ParameterList: foldInside, | 70 | ParameterList: foldInside, |
71 | PredicateBody: foldInside, | 71 | PredicateBody: foldInside, |
72 | FunctionBody: foldInside, | 72 | // FunctionBody: foldInside, |
73 | // RuleBody: foldInside, | 73 | // RuleBody: foldInside, |
74 | Conjunction: foldConjunction, | 74 | Conjunction: foldConjunction, |
75 | // Consequent: foldWholeNode, | 75 | // Consequent: foldWholeNode, |