6619640338

Committed 23 Oct 2023 10:15PM UTC coverage: 56.344% (-0.3%) from 56.621%

Build # 6619640338

Build Type

push

github

Committed by

robsimmons

Commit Message

Multiple-decl check

Run Details

143 of 291 branches covered (0.0%)

Branch coverage included in aggregate %.

6 of 6 new or added lines in 1 file covered. (100.0%)

230 of 371 relevant lines covered (61.99%)

10.96 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

11.83

/src/syntax.ts

import { Pattern, freeVars, termToString } from './terms';

export interface Proposition {
  type: 'Proposition';
  name: string;
  args: Pattern[];
}

export interface Equality {
  type: 'Equality';
  a: Pattern;
  b: Pattern;
}

export interface Inequality {
  type: 'Inequality';
  a: Pattern;
  b: Pattern;
}

export type Premise = Proposition | Equality | Inequality;

export interface Conclusion {
  name: string;
  args: Pattern[];
  values: Pattern[];
  exhaustive: boolean;
}

export type Declaration =
  | { type: 'Constraint'; premises: Premise[] }
  | {
      type: 'Rule';
      premises: Premise[];
      conclusion: Conclusion;
    };

export function propToString(p: Proposition) {
  const args = p.args
    .slice(0, p.args.length - 1)
    .map((arg) => ` ${termToString(arg)}`)
    .join('');
  const value = p.args[p.args.length - 1];
  return value.type === 'triv' ? `${p.name}${args}` : `${p.name}${args} is ${termToString(value)}`;
}

function headToString(head: Conclusion) {
  const args = head.args.map((arg) => ` ${termToString(arg)}`).join('');
  if (head.values.length !== 1 || !head.exhaustive) {
    return `${head.name}${args} is { ${head.values.map(termToString).join(', ')}${
      head.exhaustive ? '' : ', ...'
    } }`;
  } else if (head.values[0].type === 'triv') {
    return `${head.name}${args}`;
  } else {
    return `${head.name}${args} is ${termToString(head.values[0])}`;
  }
}

function premiseToString(premise: Premise) {
  switch (premise.type) {
    case 'Equality':
      return `${termToString(premise.a)} == ${termToString(premise.b)}`;
    case 'Inequality':
      return `${termToString(premise.a)} != ${termToString(premise.b)}`;
    case 'Proposition':
      return propToString(premise);
  }
}

export function declToString(decl: Declaration): string {
  switch (decl.type) {
    case 'Constraint':
      return `:- ${decl.premises.map(premiseToString).join(', ')}.`;
    case 'Rule':
      if (decl.premises.length === 0) {
        return `${headToString(decl.conclusion)}.`;
      }
      return `${headToString(decl.conclusion)} :- ${decl.premises
        .map(premiseToString)
        .join(', ')}.`;
  }
}

function checkPremises(premises: Premise[]): {
  fv: Set<string>;
  errors: string[];
} {
  const knownFreeVars = new Set<string>();
  const errors: string[] = [];
  for (let premise of premises) {
    switch (premise.type) {
      case 'Inequality': {
        const fv = freeVars(premise.a, premise.b);
        for (const v of fv) {
          if (!knownFreeVars.has(v)) {
            errors.push(`Variable '${v}' not defined before being used in an inequality.`);
          }
        }
        break;
      }
      case 'Equality': {
        const fvA = freeVars(premise.a);
        const fvB = freeVars(premise.b);
        for (const v of fvA) {
          if (!knownFreeVars.has(v)) {
            errors.push(
              `The left side of an equality premise must include only previously ground variables`,
            );
          }
        }
        for (const v of fvB) {
          knownFreeVars.add(v);
        }
        break;
      }
      case 'Proposition':
        const fv = freeVars(...premise.args);
        for (const v of fv) {
          knownFreeVars.add(v);
        }
        break;
    }
  }

  return { fv: knownFreeVars, errors };
}

export function checkDecl(decl: Declaration): string[] {
  const { fv, errors } = checkPremises(decl.premises);
  switch (decl.type) {
    case 'Rule':
      const headVars = freeVars(...decl.conclusion.args, ...decl.conclusion.values);
      for (const v of headVars) {
        if (!fv.has(v)) {
          errors.push(`Variable '${v}' used in head of rule but not defined in a premise.`);
        }
      }
      break;
    case 'Constraint':
      break;
  }
  return errors;
}

export function check(decls: Declaration[]) {
  const errors: string[] = [];
  for (let decl of decls) {
    errors.push(...checkDecl(decl))
  }
  return errors;
}

1	import { Pattern, freeVars, termToString } from './terms';	2✔
2
3	export interface Proposition {
4	type: 'Proposition';
5	name: string;
6	args: Pattern[];
7	}
8
9	export interface Equality {
10	type: 'Equality';
11	a: Pattern;
12	b: Pattern;
13	}
14
15	export interface Inequality {
16	type: 'Inequality';
17	a: Pattern;
18	b: Pattern;
19	}
20
21	export type Premise = Proposition \| Equality \| Inequality;
22
23	export interface Conclusion {
24	name: string;
25	args: Pattern[];
26	values: Pattern[];
27	exhaustive: boolean;
28	}
29
30	export type Declaration =
31	\| { type: 'Constraint'; premises: Premise[] }
32	\| {
33	type: 'Rule';
34	premises: Premise[];
35	conclusion: Conclusion;
36	};
37
38	export function propToString(p: Proposition) {	2✔
39	const args = p.args	30✔
40	.slice(0, p.args.length - 1)
41	.map((arg) => ` ${termToString(arg)}`)	×
42	.join('');
43	const value = p.args[p.args.length - 1];	30✔
44	return value.type === 'triv' ? `${p.name}${args}` : `${p.name}${args} is ${termToString(value)}`;	30✔
45	}
46
47	function headToString(head: Conclusion) {
48	const args = head.args.map((arg) => ` ${termToString(arg)}`).join('');	×
49	if (head.values.length !== 1 \|\| !head.exhaustive) {	×
50	return `${head.name}${args} is { ${head.values.map(termToString).join(', ')}${	×
51	head.exhaustive ? '' : ', ...'	×
52	} }`;
53	} else if (head.values[0].type === 'triv') {	×
54	return `${head.name}${args}`;	×
55	} else {
56	return `${head.name}${args} is ${termToString(head.values[0])}`;	×
57	}
58	}
59
60	function premiseToString(premise: Premise) {
61	switch (premise.type) {	×
62	case 'Equality':
63	return `${termToString(premise.a)} == ${termToString(premise.b)}`;	×
64	case 'Inequality':
65	return `${termToString(premise.a)} != ${termToString(premise.b)}`;	×
66	case 'Proposition':
67	return propToString(premise);	×
68	}
69	}
70
71	export function declToString(decl: Declaration): string {	2✔
72	switch (decl.type) {	×
73	case 'Constraint':
74	return `:- ${decl.premises.map(premiseToString).join(', ')}.`;	×
75	case 'Rule':
76	if (decl.premises.length === 0) {	×
77	return `${headToString(decl.conclusion)}.`;	×
78	}
79	return `${headToString(decl.conclusion)} :- ${decl.premises	×
80	.map(premiseToString)
81	.join(', ')}.`;
82	}
83	}
84
85	function checkPremises(premises: Premise[]): {
86	fv: Set<string>;
87	errors: string[];
88	} {
89	const knownFreeVars = new Set<string>();	×
90	const errors: string[] = [];	×
91	for (let premise of premises) {	×
92	switch (premise.type) {	×
93	case 'Inequality': {
94	const fv = freeVars(premise.a, premise.b);	×
95	for (const v of fv) {	×
96	if (!knownFreeVars.has(v)) {	×
97	errors.push(`Variable '${v}' not defined before being used in an inequality.`);	×
98	}
99	}
100	break;	×
101	}
102	case 'Equality': {
103	const fvA = freeVars(premise.a);	×
104	const fvB = freeVars(premise.b);	×
105	for (const v of fvA) {	×
106	if (!knownFreeVars.has(v)) {	×
107	errors.push(	×
108	`The left side of an equality premise must include only previously ground variables`,
109	);
110	}
111	}
112	for (const v of fvB) {	×
113	knownFreeVars.add(v);	×
114	}
115	break;	×
116	}
117	case 'Proposition':
118	const fv = freeVars(...premise.args);	×
119	for (const v of fv) {	×
120	knownFreeVars.add(v);	×
121	}
122	break;	×
123	}
124	}
125
126	return { fv: knownFreeVars, errors };	×
127	}
128
129	export function checkDecl(decl: Declaration): string[] {	2✔
130	const { fv, errors } = checkPremises(decl.premises);	×
131	switch (decl.type) {	×
132	case 'Rule':
133	const headVars = freeVars(...decl.conclusion.args, ...decl.conclusion.values);	×
134	for (const v of headVars) {	×
135	if (!fv.has(v)) {	×
136	errors.push(`Variable '${v}' used in head of rule but not defined in a premise.`);	×
137	}
138	}
139	break;	×
140	case 'Constraint':
141	break;	×
142	}
143	return errors;	×
144	}
145
146	export function check(decls: Declaration[]) {	2✔
147	const errors: string[] = [];	×
148	for (let decl of decls) {	×
149	errors.push(...checkDecl(decl))	×
150	}
151	return errors;	×
152	}

robsimmons / aspis / 6619640338

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous