Perform arity checking on predicates and modify syntax highlighting t…

…o treat predicates differently

docs/src/content/docs/docs/api/dusa.md

@@ -78,7 +78,6 @@ dusa.solution; // raises DusaError
 
 [Explore this example on StackBlitz](https://stackblitz.com/edit/node-ybvpcq?file=index.js&view=editor)
 
-
 For programs with multiple solutions, use the `sample()` method or the `solutions`
 getter, which returns an iterator.
 
@@ -122,7 +121,6 @@ for (const solution of dusa.solutions) {
 
 [Explore this example on StackBlitz](https://stackblitz.com/edit/node-cysbcb?file=index.js&view=editor)
 
-
 Each time the `dusa.solutions` getter is accessed, an iterator is returned that
 re-runs solution search, potentially returning solutions in a different order.
 

docs/src/content/docs/docs/api/dusasolution.md

@@ -74,7 +74,6 @@ dusa.solution.get('color', 9); // === undefined
 
 [Explore this example on StackBlitz](https://stackblitz.com/edit/node-kk2qno?file=index.js&view=editor)
 
-
 ## Enumerating all facts
 
 ### `facts` getter
@@ -95,7 +94,6 @@ for (const fact of dusa.solution.facts) {
 
 [Explore this example on StackBlitz](https://stackblitz.com/edit/node-4fvfea?file=index.js&view=editor)
 
-
 ## Querying solutions
 
 ### `lookup()` method
@@ -118,7 +116,6 @@ for (const [a, b] of dusa.solution.lookup('path')) {
 
 [Explore this example on StackBlitz](https://stackblitz.com/edit/node-xhjrt3?file=index.js&view=editor)
 
-
 This will print the following:
 
     Path from 1 to 2

src/language/syntax.ts

@@ -122,6 +122,97 @@ export function declToString(decl: Declaration): string {
   }
 }
 
+export function* visitPropsInProgram(decls: (Issue | ParsedDeclaration)[]) {
+  for (const decl of decls) {
+    if (decl.type === 'Rule') {
+      yield decl.conclusion;
+    }
+    if (decl.type === 'Demand' || decl.type === 'Forbid' || decl.type === 'Rule') {
+      for (const premise of decl.premises) {
+        if (premise.type === 'Proposition') {
+          yield premise;
+        }
+      }
+    }
+  }
+}
+
+function* visitSubterms(term: ParsedPattern): IterableIterator<ParsedPattern> {
+  yield term;
+  switch (term.type) {
+    case 'special':
+    case 'const':
+      for (const subterm of term.args) {
+        yield* visitSubterms(subterm);
+      }
+  }
+}
+
+export function* visitTermsinProgram(decls: (Issue | ParsedDeclaration)[]) {
+  for (const decl of decls) {
+    if (decl.type === 'Rule') {
+      for (const term of decl.conclusion.args) {
+        yield* visitSubterms(term);
+      }
+      for (const term of decl.conclusion.values ?? []) {
+        yield* visitSubterms(term);
+      }
+    }
+    if (decl.type === 'Demand' || decl.type === 'Forbid' || decl.type === 'Rule') {
+      for (const premise of decl.premises) {
+        if (premise.type === 'Proposition') {
+          for (const term of premise.args) {
+            yield* visitSubterms(term);
+          }
+          if (premise.value) {
+            yield* visitSubterms(premise.value);
+          }
+        } else {
+          yield* visitSubterms(premise.a);
+          yield* visitSubterms(premise.b);
+        }
+      }
+    }
+  }
+}
+
+function checkPropositionArity(
+  decls: (Issue | ParsedDeclaration)[],
+): { issues: null; arities: { [pred: string]: number } } | { issues: Issue[] } {
+  const arities: Map<string, Map<number, SourceLocation[]>> = new Map();
+  for (const prop of visitPropsInProgram(decls)) {
+    if (!arities.get(prop.name)) arities.set(prop.name, new Map());
+    if (!arities.get(prop.name)!.get(prop.args.length)) {
+      arities.get(prop.name)!.set(prop.args.length, [prop.loc]);
+    } else {
+      arities.get(prop.name)!.get(prop.args.length)!.push(prop.loc);
+    }
+  }
+
+  const actualArities: { [pred: string]: number } = {};
+  const issues: Issue[] = [];
+  for (const [pred, map] of arities.entries()) {
+    const arityList = [...map.entries()].sort((a, b) => b[1].length - a[1].length);
+    const expectedArity = arityList[0][0];
+    actualArities[pred] = expectedArity;
+    for (let i = 1; i < arityList.length; i++) {
+      const [arity, occurrences] = arityList[i];
+      for (const occurrence of occurrences) {
+        issues.push({
+          type: 'Issue',
+          msg: `Predicate '${pred}' usually has ${expectedArity} argument${
+            expectedArity === 1 ? '' : 's'
+          }, but here it has ${arity}`,
+          loc: occurrence,
+        });
+      }
+    }
+  }
+
+  if (issues.length > 0) return { issues };
+  return { issues: null, arities: actualArities };
+}
+
 /**
  * Gathers uses of free variables in premises and checks that
  * free variables are being used correctly and that named wildcards
@@ -295,7 +386,8 @@ export function checkFreeVarsInDecl(
 export function check(
   decls: ParsedDeclaration[],
 ): { errors: Issue[] } | { errors: null; decls: ParsedDeclaration[] } {
-  const errors: Issue[] = [];
+  const arityInfo = checkPropositionArity(decls);
+  const errors: Issue[] = arityInfo.issues || [];
   const newDecls = decls.map((decl) => {
     const res = checkFreeVarsInDecl(decl);
     if (res.errors !== null) {

src/web/codemirror.css

@@ -31,11 +31,16 @@
 }
 
 .tok-variableName {
+  color: var(--oksolar-text-violet);
+}
+
+.tok-predicate .tok-variableName,
+.tok-variableName .tok-predicate {
   color: var(--oksolar-text-blue);
 }
 
 .tok-variableName2 {
-  color: var(--oksolar-text-violet);
+  color: var(--oksolar-text-pink);
 }
 
 .tok-variableName.tok-local {

src/web/codemirror.ts

@@ -1,6 +1,15 @@
 import { HighlightStyle, StreamLanguage, syntaxHighlighting } from '@codemirror/language';
-import { EditorState } from '@codemirror/state';
-import { EditorView, ViewUpdate, keymap, lineNumbers, tooltips } from '@codemirror/view';
+import { EditorState, RangeSet, StateEffect, StateField } from '@codemirror/state';
+import {
+  Decoration,
+  DecorationSet,
+  EditorView,
+  ViewPlugin,
+  ViewUpdate,
+  keymap,
+  lineNumbers,
+  tooltips,
+} from '@codemirror/view';
 import { ParserState, dusaTokenizer } from '../language/dusa-tokenizer.js';
 import { StringStream } from '../parsing/string-stream.js';
 import { classHighlighter, tags } from '@lezer/highlight';
@@ -9,13 +18,13 @@ import { SourcePosition } from '../parsing/source-location.js';
 import { Issue, parseWithStreamParser } from '../parsing/parser.js';
 import { defaultKeymap, history, historyKeymap } from '@codemirror/commands';
 import { parseTokens } from '../language/dusa-parser.js';
-import { ParsedDeclaration, check } from '../language/syntax.js';
+import { ParsedDeclaration, check, visitPropsInProgram } from '../language/syntax.js';
 
 const bogusPosition = {
   start: { line: 1, column: 1 },
   end: { line: 1, column: 2 },
 };
-/** Create a Codemirror-compliant parser from our streamparser.
+/** Create a Codemirror-compliant parser from our stream parser.
  * The token method is given a Codemirror-style StringStream,
  * and we have to use that to implement the StringStream interface
  * that our parser expects. Because we're not using the syntax
@@ -116,6 +125,77 @@ function dusaLinter(view: EditorView): readonly Diagnostic[] {
   return issueToDiagnostic(checkedDecls.errors ?? []);
 }
 
+/** highlightPredicates is based on simplifying the Linter infrastructure */
+const highlightPredicatesUpdateEffect = StateEffect.define<[number, number][]>();
+const highlightPredicatesState = StateField.define<DecorationSet>({
+  create() {
+    return RangeSet.empty;
+  },
+  update(value, transaction) {
+    if (transaction.docChanged) {
+      value = value.map(transaction.changes);
+    }
+
+    for (const effect of transaction.effects) {
+      if (effect.is(highlightPredicatesUpdateEffect)) {
+        return RangeSet.of(
+          effect.value.map(([from, to]) => ({
+            from,
+            to,
+            value: Decoration.mark({ inclusive: true, class: 'tok-predicate' }),
+          })),
+          true,
+        );
+      }
+    }
+    return value;
+  },
+  provide(field) {
+    return EditorView.decorations.from(field);
+  },
+});
+const highlightPredicatesPlugin = ViewPlugin.define((view: EditorView) => {
+  const delay = 750;
+  let timeout: null | ReturnType<typeof setTimeout> = setTimeout(() => run(), delay);
+  let nextUpdateCanHappenOnlyAfter = Date.now() + delay;
+  function run() {
+    const now = Date.now();
+    // Debounce logic, part 1
+    if (now < nextUpdateCanHappenOnlyAfter - 5) {
+      timeout = setTimeout(run, nextUpdateCanHappenOnlyAfter - now);
+    } else {
+      timeout = null;
+      const contents = view.state.doc.toString();
+      const tokens = parseWithStreamParser(dusaTokenizer, contents);
+      if (tokens.issues.length > 0) return;
+      const parsed = parseTokens(tokens.document);
+      const ranges: [number, number][] = [];
+      for (const prop of visitPropsInProgram(parsed)) {
+        const start = position(view.state, prop.loc.start);
+        ranges.push([start, start + prop.name.length]);
+      }
+      view.dispatch({ effects: [highlightPredicatesUpdateEffect.of(ranges)] });
+    }
+  }
+
+  return {
+    update(update: ViewUpdate) {
+      if (update.docChanged) {
+        // Debounce logic, part 2
+        nextUpdateCanHappenOnlyAfter = Date.now() + delay;
+        if (timeout === null) {
+          timeout = setTimeout(run, delay);
+        }
+      }
+    },
+    destroy() {
+      if (timeout !== null) {
+        clearTimeout(timeout);
+      }
+    },
+  };
+});
+
 export const editorChangeListener: { current: null | ((update: ViewUpdate) => void) } = {
   current: null,
 };
@@ -135,6 +215,8 @@ const state = EditorState.create({
     }),
     linter(dusaLinter),
     tooltips({ parent: document.body }),
+    highlightPredicatesPlugin,
+    highlightPredicatesState,
     keymap.of([...defaultKeymap, ...historyKeymap]),
   ],
 });