feat(language): type inference

* Customizable operator overloads.
* Customizable aggregation operators.
* Simplify ProblemQualifiedNameProvider.

3 files changed, 21 insertions, 21 deletions

diff --git a/subprojects/frontend/src/editor/EditorTheme.ts b/subprojects/frontend/src/editor/EditorTheme.ts
index b211f2a7..1f8152d3 100644
--- a/subprojects/frontend/src/editor/EditorTheme.ts
+++ b/subprojects/frontend/src/editor/EditorTheme.ts
@@ -166,7 +166,7 @@ export default styled('div', {
     '.tok-problem-abstract': {
       fontStyle: 'italic',
     },
-    '.tok-problem-datatype': {
+    '.tok-problem-datatype, .tok-problem-aggregator': {
       '&, & .tok-typeName': {
         color: theme.palette.primary.main,
       },
diff --git a/subprojects/frontend/src/language/problem.grammar b/subprojects/frontend/src/language/problem.grammar
index 0f6ea3e1..829dc138 100644
--- a/subprojects/frontend/src/language/problem.grammar
+++ b/subprojects/frontend/src/language/problem.grammar
@@ -11,12 +11,13 @@
 @precedence {
   cast,
   prefix,
+  range @left,
   exponential @right,
   multiplicative @left,
   additive @left,
-  range @left,
   lattice @left,
   comparison @left,
+  boolean @left,
   assignment,
   feature @cut
 }
@@ -45,7 +46,10 @@ statement {
     (EnumBody { "{" sep<",", AtomNodeName> "}" } | ".")
   } |
   DatatypeDeclaration {
-    kw<"extern"> kw<"datatype"> DatatypeName "."
+    kw<"extern"> ckw<"datatype"> DatatypeName "."
+  } |
+  AggregatorDeclaration {
+    kw<"extern"> ckw<"aggregator"> AggregatorName "."
   } |
   PredicateDefinition {
     (
@@ -92,7 +96,7 @@ FeatureDeclaration {
   ";"?
 }
 
-Parameter { Modality? RelationName? VariableName }
+Parameter { RelationName? VariableName }
 
 // Use @dynamicPrecedence to prevent a(b) from being parsed as Expr { a } Expr { b }
 // instead of Atom { a(b) }
@@ -111,22 +115,23 @@ Expr {
 AssignmentExpr { !assignment VariableName kw<"is"> Expr }
 
 BinaryExpr {
+  Expr !boolean ("&&" | "||" | "^^") Expr |
   Expr !comparison ComparisonOp Expr |
   Expr !lattice (LatticeMeet | "\\/") Expr |
-  Expr !range ".." Expr |
   Expr !additive ("+" | "-") Expr |
   Expr !multiplicative (StarMult | Divide) Expr |
-  Expr !exponential "**" Expr
+  Expr !exponential "**" Expr |
+  Expr !range ".." Expr
 }
 
 UnaryExpr {
-  !prefix ("+" | "-" | "!" | kw<"count"> | Modality) Expr
+  !prefix ("+" | "-" | "!" | kw<"count">) Expr
 }
 
 CastExpr { !cast Expr kw<"as"> DatatypeName }
 
 Aggregation {
-  AggregationOp "{" Expr "|" Expr "}"
+  AggregatorName "{" Expr "|" Expr "}"
 }
 
 Atom { RelationName "+"? ParameterList<Expr> }
@@ -151,14 +156,6 @@ LogicValue {
   kw<"true"> | kw<"false"> | kw<"unknown"> | kw<"error">
 }
 
-Modality {
-  kw<"must"> | kw<"may"> | kw<"current">
-}
-
-AggregationOp {
-  ckw<"sum"> | ckw<"prod"> | ckw<"min"> | ckw<"max">
-}
-
 ComparisonOp { SymbolicComparisonOp | kw<"in"> }
 
 ScopeElement { RelationName ("=" | "+=") Multiplicity }
@@ -183,6 +180,8 @@ NodeName { QualifiedName }
 
 ModuleName { QualifiedName }
 
+AggregatorName { QualifiedName }
+
 QualifiedName[implicitCompletion=true] { "::"? identifier (QualifiedNameSeparator "::" identifier)* }
 
 kw<term> { @specialize[@name={term},implicitCompletion=true]<identifier, term> }
@@ -237,7 +236,7 @@ sep1<separator, content> { content (separator content)* }
 
   SymbolicComparisonOp {
     ">" | ">=" | "<" | "<=" | "==" | "!=" |
-    "<:" | ":>" | "===" | "!=="
+    "===" | "!=="
   }
 
   NotOp { "!" }
diff --git a/subprojects/frontend/src/language/problemLanguageSupport.ts b/subprojects/frontend/src/language/problemLanguageSupport.ts
index 3d25d699..594351d6 100644
--- a/subprojects/frontend/src/language/problemLanguageSupport.ts
+++ b/subprojects/frontend/src/language/problemLanguageSupport.ts
@@ -28,12 +28,12 @@ const parserWithMetadata = parser.configure({
       LineComment: t.lineComment,
       BlockComment: t.blockComment,
       'module problem class enum pred fn scope': t.definitionKeyword,
-      'import as declare atom multi extern datatype': t.definitionKeyword,
+      'import as declare atom multi': t.definitionKeyword,
+      'extern datatype aggregator': t.definitionKeyword,
       'abstract extends refers contains container opposite': t.modifier,
-      'default error contained containment': t.modifier,
+      default: t.modifier,
       'true false unknown error': t.keyword,
-      'may must current count': t.operatorKeyword,
-      'sum prod min max in is': t.operatorKeyword,
+      'count in is': t.operatorKeyword,
       // 'new delete': t.keyword,
       NotOp: t.operator,
       UnknownOp: t.operator,
@@ -44,6 +44,7 @@ const parserWithMetadata = parser.configure({
       String: t.string,
       'RelationName/QualifiedName': t.typeName,
       'DatatypeName/QualifiedName': t.keyword,
+      'AggregatorName/QualifiedName': t.operatorKeyword,
       // 'RuleName/QualifiedName': t.typeName,
       'AtomNodeName/QualifiedName': t.atom,
       'VariableName/QualifiedName': t.variableName,