feat(fitch): added Derived Rule Option and changed Abs handling

Added option for derived rules which can be used to use whatever derived rule. Also put absurdity in
the rule select instead of having a button for adding absurdities.

src/components/Formula.tsx

@@ -30,7 +30,7 @@ const Formula = (props: FormulaProps) => {
   const [cursor, setCursor] = createSignal(props.value.length);
 
   const onKeyPress: EventHandler = (e) => {
-    const value = e.key;
+    const value = e.key.match(/[fgh]/) ? e.key.toUpperCase() : e.key;
     const last = props.value[cursor() - 1] ?? "";
 
     if (value.match(/[1-9]/)) {

src/components/FormulaRender.tsx

@@ -49,6 +49,9 @@ const FormulaRender = (props: FormulaRenderProps) => {
               <Match when={c === "e"}>
                 <div>&exist;</div>
               </Match>
+              <Match when={c === "m"}>
+                <div>{"\u22A5"}</div>
+              </Match>
               <Match when={c.match(/[pqrxyxabc]/)}>
                 <div>
                   {c[0]}

src/components/fitch/Inserter.tsx

@@ -26,21 +26,13 @@ const Inserter = (props: InserterProps) => {
         })
       );
       set(
-        (line) => line.type === "rule" || line.type == "abs",
+        (line) => line.type === "rule",
         "from" as never,
         (from: number) => from >= index,
         (from: number) => (from + 1) as never
       );
     });
 
-  const insertAbs = (indentation: number) =>
-    insert({
-      id: createUniqueId(),
-      type: "abs",
-      indentation,
-      from: [-1, -1],
-    });
-
   const insertPrem = () =>
     insert({
       id: createUniqueId(),
@@ -105,14 +97,6 @@ const Inserter = (props: InserterProps) => {
                 >
                   <ArrowDownCircle />
                 </IconButton>
-                <Show when={newIndentation > 0}>
-                  <IconButton
-                    title="Add Absurdity"
-                    onClick={[insertAbs, newIndentation]}
-                  >
-                    {"\u22A5"}
-                  </IconButton>
-                </Show>
               </Show>
               <Show when={props.type === "prem"}>
                 <IconButton title="Add Premise" onClick={insertPrem}>

src/components/fitch/line/additional.solve.tsx

@@ -31,16 +31,16 @@ const FitchLineAdditionalSolve = (props: FitchLineProps) => {
     }
     batch(() => {
       set(
-        (state) => state.type === "rule" || state.type === "abs",
+        (state) => state.type === "rule",
         "from" as never,
         (from) => from >= props.index && from < props.index + deleteCount,
         -1 as never
       );
       set(
-        (state) => state.type === "rule" || state.type === "abs",
+        (state) => state.type === "rule",
         "from" as never,
         (from) => from >= props.index + deleteCount,
-        (from) => from - deleteCount
+        (from) => from - deleteCount as never
       );
       set(
         produce((state) => {

src/components/fitch/line/annotation.solve.tsx

@@ -30,10 +30,17 @@ const FitchLineAnnotationSolve = (props: {
           set(
             props.index,
             "annotation",
-            e.currentTarget.value === "" ? undefined : e.currentTarget.value
+            e.currentTarget.value
           )
         }
       />
+      <IconButton 
+        class="text-red-600"
+        title="Remove annotation"
+        onClick={() => set(props.index, "annotation", undefined)}
+      >
+        <Tag />
+      </IconButton>
     </Show>
   );
 };

src/rules/fitch.ts

@@ -11,6 +11,8 @@ const propRules = [
   "d-intro",
   "dn",
   "d-elim",
+  "dr",
+  "abs",
 ] as const;
 const predRules = [
   ...propRules,
@@ -70,6 +72,14 @@ const propRulesOptions: Record<
     label: "DN",
     count: 1,
   },
+  dr: {
+    label: "DR",
+    count: 2,
+  },
+  abs: {
+    label: "Abs.",
+    count: 2,
+  }
 };
 
 const predRulesOptions: Record<

src/schemas/common.ts

@@ -1,8 +1,8 @@
 import { createUniqueId } from "solid-js";
 import { z } from "zod";
 
-const propFormulaRegex = /[pqr][1-9]?|[iklno()]/;
-const predFormulaRegex = /[pqrFGHxyzabc][1-9]?|[iklno()ue=]/;
+const propFormulaRegex = /[pqr][1-9]?|[iklno()m]/;
+const predFormulaRegex = /[pqrFGHxyzabc][1-9]?|[iklno()mue=]/;
 
 export const id = z.object({ id: z.string().default(() => createUniqueId()) });
 

src/schemas/fitch.ts

@@ -6,15 +6,6 @@ const indentation = z.number().min(0);
 
 const annotation = z.string().optional();
 
-const fitchAbs = z.object({
-  type: z.literal("abs"),
-  indentation,
-  from: from.length(2),
-  annotation,
-});
-
-export type FitchAbsurdityType = z.infer<typeof fitchAbs>;
-
 const fitchPrem = z.object({
   type: z.literal("prem"),
   indentation: z.literal(0),
@@ -47,7 +38,7 @@ export type FitchRuleType = z.infer<typeof fitchRule>;
 const fitchProofSchema = z
   .array(
     z
-      .discriminatedUnion("type", [fitchAbs, fitchPrem, fitchRule, fitchAss])
+      .discriminatedUnion("type", [fitchPrem, fitchRule, fitchAss])
       .and(id)
   )
   .default([]);