refactor

packages/viewer/src/components/Traits/Redundancy.svelte

@@ -1,26 +1,19 @@
 <script lang="ts">
-  import { checkNegation } from '@/stores/deduction'
+  import { checkIfRedundant } from '@/stores/deduction'
   import context from '@/context'
   import type { Space, Property } from '@/types'
-  import type { Theorem } from '@/models'
   import Table from '../Theorems/Table.svelte'
   export let space: Space
   export let property: Property
   const { theorems, traits } = context()
-  $: result = checkNegation($theorems, space, $traits, property)
-  let thms: Theorem[]
-  $: if (result.kind === 'contradiction') {
-    thms = result.contradiction.theorems
-      .map(i => $theorems.find(i))
-      .filter(t => t !== null)
-  }
+  $: result = checkIfRedundant(space, property, $theorems, $traits)
 </script>
 
-{#if result.kind === 'contradiction'}
+{#if result.redundant}
   <div class="alert alert-warning">
     <strong>Notice:</strong>
-    This asserted property can be deduced from the other asserted traits for
-    this space.
+    This asserted property can be deduced from the other asserted traits for this
+    space, due to the following theorems.
   </div>
-  <Table theorems={thms} />
+  <Table theorems={result.theorems} />
 {/if}

packages/viewer/src/stores/deduction.ts

@@ -18,7 +18,6 @@ import type {
   Traits,
 } from '@/models'
 import { eachTick, read, subscribeUntil } from '@/util'
-import type { Result } from '@pi-base/core'
 
 export type State = {
   checked: Set<number>
@@ -190,12 +189,12 @@ function loadProof(
   return result
 }
 
-export function checkNegation(
-  theorems: Theorems,
+export function checkIfRedundant(
   space: Space,
-  traits: Traits,
   property: Property,
-): Result<number, number> {
+  thms: Theorems,
+  traits: Traits,
+): { redundant: boolean; theorems: Theorem[] } {
   const assertedTraits = traits.forSpace(space).filter(([_, t]) => t.asserted)
   const map = new Map(
     assertedTraits.map(([p, t]) => {
@@ -206,5 +205,14 @@ export function checkNegation(
       }
     }),
   )
-  return deduceTraits(indexTheorems(theorems), map)
+  const result = deduceTraits(indexTheorems(thms), map)
+  const redundant = result.kind === 'contradiction'
+  if (!redundant) {
+    const theorems: Theorem[] = []
+    return { redundant, theorems }
+  }
+  const theorems = result.contradiction.theorems
+    .map(t => thms.find(t))
+    .filter(t => t !== null)
+  return { redundant, theorems }
 }