UI/prop prompts with params

frontend/src/domain/visual-proof-editor/components/visual-proof-editor-parameter-identifier-selector.tsx

@@ -0,0 +1,207 @@
+import { get_free_parameters, Identifier, instantiate_free_parameter_by_index, Prop } from 'alice';
+import { Select, Space } from 'antd';
+import React, { Fragment, ReactElement, useCallback, useEffect, useRef, useState } from 'react';
+
+interface VisualProofEditorParameterIdentifierSelectorProps {
+    prop: Prop;
+    options: { [name: string]: Identifier[] },
+    onAllSelect: (prop: Prop) => void;
+    getPopupContainer?: () => HTMLElement;
+}
+
+interface RenderPropResult {
+    node: ReactElement;
+    newIndex: number;
+}
+
+type RenderProp = (prop: Prop, index: number, boundIdentifiers: string[]) => RenderPropResult;
+
+export function VisualProofEditorParameterIdentifierSelector(props: VisualProofEditorParameterIdentifierSelectorProps) {
+    const {
+        prop,
+        options,
+        onAllSelect,
+        getPopupContainer,
+    } = props;
+
+    const containerRef = useRef<HTMLDivElement | null>(null);
+    const [paramMapping, setParamMapping] = useState<{ [idx: number]: number } | null>(null);
+
+    useEffect(() => {
+        const selectableParamSize = get_free_parameters(prop)
+            .filter((param) => param.kind === 'Uninstantiated')
+            .length;
+
+        setParamMapping(Object.assign({}, Array(selectableParamSize).fill(0)));
+    }, [prop]);
+
+    useEffect(() => {
+
+        if (!paramMapping) {
+            return;
+        }
+
+        const params = get_free_parameters(prop);
+        let instantiatedProp = { ...prop };
+        for (const [paramIndex, identifierIndex] of Object.entries(paramMapping)) {
+            const param = params[parseInt(paramIndex)];
+            const paramName = param.kind === 'Instantiated' ? param.value.name : param.value;
+
+            instantiatedProp = instantiate_free_parameter_by_index(
+                instantiatedProp,
+                parseInt(paramIndex),
+                options[paramName][identifierIndex],
+            );
+        }
+
+        onAllSelect(instantiatedProp);
+    }, [paramMapping]);
+
+    const renderProp: RenderProp = (prop: Prop, index: number, boundIdentifiers: string[]) => {
+
+        const handlePrimitive = useCallback((symbol: string, index: number) => {
+            return {
+                node: (<span>{symbol}</span>),
+                newIndex: index,
+            };
+        }, []);
+
+        const handleBinaryConnective = useCallback((symbol: string, prop: Prop & { kind: 'And' | 'Or' | 'Impl' }, index: number, boundIdentifiers: string[]) => {
+            const fst = renderProp(prop, index, [...boundIdentifiers]);
+            const snd = renderProp(prop, fst.newIndex, boundIdentifiers);
+
+            const node = (
+                <>
+                    {fst.node}
+                    <span>
+                        {symbol}
+                    </span>
+                    {snd.node}
+                </>
+            );
+
+            return {
+                node,
+                newIndex: snd.newIndex,
+            };
+        }, []);
+
+        const handleQuantifier = useCallback((symbol: string, prop: Prop & { kind: 'ForAll' | 'Exists' }, index: number, boundIdentifiers: string[]) => {
+            const body = renderProp(
+                prop.value.body,
+                index,
+                [...boundIdentifiers, prop.value.object_ident],
+            );
+
+            const node = (
+                <>
+                    <span>{symbol}</span>
+                    <span>{prop.value.object_ident}</span>
+                    <span>:</span>
+                    <span>{prop.value.object_type_ident}</span>
+                    <span>. </span>
+                    <span>{body.node}</span>
+                </>
+            );
+
+            return {
+                node,
+                newIndex: body.newIndex,
+            };
+        }, []);
+
+        const handleAtom = useCallback((prop: Prop & { kind: 'Atom' }, index: number, boundIdentifiers: string[]) => {
+            const params = prop.value[1];
+
+            const paramNodes = [];
+            for (const param of params) {
+                const paramIndex = index;
+                const paramName = param.kind === 'Instantiated' ? param.value.name : param.value;
+
+                if (param.kind === 'Instantiated' || boundIdentifiers.includes(paramName)) {
+                    paramNodes.push(<span>{paramName}</span>);
+
+                    index++;
+                    continue;
+                }
+
+                const identOptions = options[paramName];
+
+                if (!identOptions || identOptions.length === 0) {
+                    throw new Error(`No options for name ${paramName}.`);
+                }
+
+                const selectionOptions = identOptions
+                    .map((option, i) => ({
+                        label: `${option.name} - ${option.unique_id}`,
+                        value: i,
+                    }));
+
+                const handleSelect = (idx: number) => {
+                    setParamMapping({
+                        ...paramMapping,
+                        [paramIndex]: idx,
+                    });
+                };
+
+                const node = (
+                    <Space wrap>
+                        <Select
+                            getPopupContainer={getPopupContainer}
+                            onChange={handleSelect}
+                            defaultValue={0}
+                            options={selectionOptions}
+                        />
+                    </Space>
+                );
+
+                paramNodes.push(node);
+                index++;
+            }
+
+            const propName = prop.value[0];
+
+            const node = (
+                <>
+                    <span>{propName}</span>
+                    {paramNodes.length > 0 && (
+                        <>
+                            <span>(</span>
+                            {
+                                paramNodes.map((node, i) => (
+                                    <Fragment key={i}>
+                                        {i > 0 && <span>, </span>}
+                                        {node}
+                                    </Fragment>
+                                ))
+                            }
+                            <span>)</span>
+                        </>
+                    )}
+                </>
+            );
+
+            return {
+                node,
+                newIndex: index,
+            }
+        }, []);
+
+        switch (prop.kind) {
+            case 'True': return handlePrimitive('⊤', index);
+            case 'False': return handlePrimitive('⊥', index);
+            case 'And': return handleBinaryConnective('∧', prop, index, boundIdentifiers);
+            case 'Or': return handleBinaryConnective('∨', prop, index, boundIdentifiers);
+            case 'Impl': return handleBinaryConnective('⊃', prop, index, boundIdentifiers);
+            case 'ForAll': return handleQuantifier('∀', prop, index, boundIdentifiers);
+            case 'Exists': return handleQuantifier('∃', prop, index, boundIdentifiers);
+            case 'Atom': return handleAtom(prop, index, boundIdentifiers);
+        }
+    };
+
+    return (
+        <div ref={containerRef}>
+            {renderProp(prop, 0, []).node}
+        </div>
+    );
+}

frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/and-elim-fst-rule-handler.ts

@@ -1,6 +1,5 @@
 import { v4 } from 'uuid';
 import { ProofRuleHandlerResult, VisualProofEditorRuleHandlerParams } from '..';
-import Swal from 'sweetalert2';
 import { ProofRuleHandler } from './proof-rule-handler';
 import { Prop } from 'alice';
 import { createEmptyVisualProofEditorProofTreeFromProp } from '../../lib/visual-proof-editor-proof-tree';
@@ -18,7 +17,7 @@ export class AndElimFstRuleHandler extends ProofRuleHandler {
     }
 
     protected async handleRuleUpwards(params: VisualProofEditorRuleHandlerParams): Promise<ProofRuleHandlerResult | undefined> {
-        const { selectedProofTreeNodes, error } = params;
+        const { selectedProofTreeNodes, error, assumptions } = params;
 
         if (selectedProofTreeNodes.length !== 1) {
             error('Cannot apply this rule on multiple nodes.');
@@ -33,20 +32,17 @@ export class AndElimFstRuleHandler extends ProofRuleHandler {
             return;
         }
 
-        const secondComponentResult = await Swal.fire({
-            title: 'Enter second component of conjunction.',
-            input: 'text',
+        const secondComponent = await this.promptProp({
+            title: 'Enter second component of conjunction',
             inputPlaceholder: 'B',
-            showCloseButton: true,
+            assumptions,
+            error,
         });
 
-        let secondComponent = secondComponentResult.value;
         if (!secondComponent) {
             return;
         }
 
-        secondComponent = this.parseProp(secondComponent);
-
         const conjunction: Prop = { kind: 'And', value: [conclusion.value, secondComponent] };
 
         return {

frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/and-elim-snd-rule-handler.ts

@@ -1,6 +1,5 @@
 import { v4 } from 'uuid';
 import { ProofRuleHandlerResult, VisualProofEditorRuleHandlerParams } from '..';
-import Swal from 'sweetalert2';
 import { ProofRuleHandler } from './proof-rule-handler';
 import { Prop } from 'alice';
 import { createEmptyVisualProofEditorProofTreeFromProp } from '../../lib/visual-proof-editor-proof-tree';
@@ -18,7 +17,7 @@ export class AndElimSndRuleHandler extends ProofRuleHandler {
     }
 
     protected async handleRuleUpwards(params: VisualProofEditorRuleHandlerParams): Promise<ProofRuleHandlerResult | undefined> {
-        const { selectedProofTreeNodes, error } = params;
+        const { selectedProofTreeNodes, assumptions, error } = params;
 
         if (selectedProofTreeNodes.length !== 1) {
             error('Cannot apply this rule on multiple nodes.');
@@ -33,20 +32,17 @@ export class AndElimSndRuleHandler extends ProofRuleHandler {
             return;
         }
 
-        const firstComponentResult = await Swal.fire({
-            title: 'Enter first component of conjunction.',
-            input: 'text',
+        const firstConclusion = await this.promptProp({
+            title: 'Enter first component of conjunction',
             inputPlaceholder: 'A',
-            showCloseButton: true,
+            assumptions,
+            error,
         });
 
-        let firstConclusion = firstComponentResult.value;
         if (!firstConclusion) {
             return;
         }
 
-        firstConclusion = this.parseProp(firstConclusion);
-
         const conjunction: Prop = { kind: 'And', value: [firstConclusion, conclusion.value] };
 
         return {

frontend/src/domain/visual-proof-editor/proof-rule/proof-rule-handler/exists-elim-rule-handler.ts

@@ -1,4 +1,3 @@
-import Swal from 'sweetalert2';
 import { instantiate_free_parameter } from 'alice';
 import { v4 } from 'uuid';
 import { VisualProofEditorRuleHandlerParams, ProofRuleHandlerResult } from '..';
@@ -26,6 +25,7 @@ export class ExistsElimRuleHandler extends ProofRuleHandler {
             selectedProofTreeNodes,
             generateIdentifier,
             generateUniqueNumber,
+            assumptions,
             error,
         } = params;
 
@@ -42,19 +42,17 @@ export class ExistsElimRuleHandler extends ProofRuleHandler {
             return;
         }
 
-        let existsProp = (await Swal.fire({
+        const existsProp = await this.promptProp({
             title: 'Enter existential quantification you want to eliminate.',
-            input: 'text',
             inputPlaceholder: '∃x:t. A(x)',
-            showCloseButton: true,
-        })).value;
+            assumptions,
+            error,
+        });
 
         if (!existsProp) {
             return;
         }
 
-        existsProp = this.parseProp(existsProp);
-
         if (existsProp.kind !== 'Exists') {
             error('You did not enter an existential quantification.');
             return;
@@ -101,6 +99,7 @@ export class ExistsElimRuleHandler extends ProofRuleHandler {
             selectedProofTreeNodes,
             generateIdentifier,
             generateUniqueNumber,
+            assumptions,
             error,
         } = params;
 
@@ -124,23 +123,19 @@ export class ExistsElimRuleHandler extends ProofRuleHandler {
             return;
         }
 
-        // ask for new conclusion
-        let newConclusion = (await Swal.fire({
+        const newConclusion = await this.promptProp({
             title: 'Enter new conclusion',
-            input: 'text',
             inputPlaceholder: 'C',
-            showCloseButton: true,
-        })).value;
+            assumptions,
+            error,
+        });
 
         if (!newConclusion) {
-            return this.createEmptyProofRuleHandlerResult();
+            return;
         }
 
-        newConclusion = this.parseProp(newConclusion);
-
-
         // TODO check that free parameter does not escape scope
-
+        // Let that handle the type checker
 
         const { object_ident, object_type_ident, body } = propConclusion.value;