Merge pull request #17 from eneoli/alpha-eq

Alpha eq in UI

frontend/src/domain/app/components/app.tsx

@@ -162,5 +162,6 @@ const generateCode: (proofTree: VisualProofEditorProofTree) => string = (proofTr
         case 'ExistsIntro': return `(${generateCode(proofTree.premisses[0])}, ${generateCode(proofTree.premisses[1])})`;
         case 'ExistsElim': return `let (${rule.value[0]}, ${rule.value[1]}) = ${generateCode(proofTree.premisses[0])} in ${generateCode(proofTree.premisses[1])}`;
         case 'Sorry': return 'sorry';
+        case 'AlphaEquivalent': return generateCode(proofTree.premisses[0]);
     }
 };

frontend/src/domain/proof-tree/components/proof-line.tsx

@@ -1,12 +1,14 @@
 import { css } from '@emotion/css';
 import React, { useEffect, useRef } from 'react';
 import Katex from 'katex';
+import { ProofTreeRule } from 'alice';
+import { printProofRule } from '../../../util/print-proof-rule';
 
 interface ProofLineProps {
-    label: string;
+    rule: ProofTreeRule;
 }
 
-export function ProofLine({ label }: ProofLineProps) {
+export function ProofLine({ rule }: ProofLineProps) {
 
     const labelRef = useRef<HTMLDivElement>(null);
 
@@ -16,15 +18,18 @@ export function ProofLine({ label }: ProofLineProps) {
             return;
         }
 
-        Katex.render(label, labelRef.current, {
+        Katex.render(printProofRule(rule), labelRef.current, {
             throwOnError: false,
 
         });
-    }, [labelRef.current, label]);
+    }, [labelRef.current, rule]);
 
     return (
         <div className={cssLineContainer}>
-            <div className={cssLine} />
+            <div
+                className={cssLine}
+                style={{ borderStyle: rule.kind === 'AlphaEquivalent' ? 'dashed' : undefined }}
+            />
             <div className={cssLabelContainer}>
                 <div className={cssLabel}>
                     <div ref={labelRef} />
@@ -43,10 +48,8 @@ const cssLineContainer = css`
 const cssLine = css`
     width: 100%;
     color: #002D62;
-    background-color: #002D62;
-    height: 3px;
+    border: 2px solid #002D62;
     margin: 0;
-    border: 0;
 `;
 
 const cssLabelContainer = css`

frontend/src/domain/proof-tree/components/proof-node.tsx

@@ -1,9 +1,10 @@
 import { css } from '@emotion/css';
 import React, { ReactNode } from 'react';
 import { ProofLine } from './proof-line';
+import { ProofTreeRule } from 'alice';
 
 interface ProofNodeProps {
-    rule: string | null;
+    rule: ProofTreeRule | null;
     content: ReactNode
     children?: ReactNode
 }
@@ -17,7 +18,7 @@ export function ProofNode({ children, content, rule }: ProofNodeProps) {
             </div>
 
             {rule && (
-                <ProofLine label={rule} />
+                <ProofLine rule={rule} />
             )}
 
             <div className={cssConclusion}>

frontend/src/domain/visual-proof-editor/components/reasoning-context-visualizer.tsx

@@ -4,7 +4,6 @@ import { ProofNode } from '../../proof-tree/components/proof-node';
 import { printProp, printTypeJudgment } from '../../../util/print-prop';
 import { useDraggable, useDroppable } from '@dnd-kit/core';
 import { ProofTreeConclusion } from 'alice';
-import { printProofRule } from '../../../util/print-proof-rule';
 import { VisualProofEditorReasoningContext } from '../lib/visual-proof-editor-reasoning-context';
 import { VisualProofEditorProofTree } from '../lib/visual-proof-editor-proof-tree';
 
@@ -57,7 +56,7 @@ export function ReasoningContextVisualizer(props: ReasoningContextVisualizerProp
 
         return (
             <div onClick={onNodeClick}>
-                <ProofNode rule={proofTree.rule ? printProofRule(proofTree.rule) : null} content={conclusion}>
+                <ProofNode rule={proofTree.rule} content={conclusion}>
                     {
                         proofTree.premisses.map((child: VisualProofEditorProofTree, i: number) => (
                             <Fragment key={i}>

frontend/src/domain/visual-proof-editor/components/visual-proof-editor.tsx

@@ -1,7 +1,7 @@
 import { css } from '@emotion/css';
 import React, { useCallback, useEffect, useRef, useState } from 'react';
 import { VisualProofEditorSidebar } from './visual-proof-editor-sidebar';
-import { Prop } from 'alice';
+import { proof_tree_conclusion_alpha_eq, Prop } from 'alice';
 import { notification } from 'antd';
 import { DndContext, DragCancelEvent, DragEndEvent, DragStartEvent, PointerSensor, useSensor, useSensors } from '@dnd-kit/core';
 import { SelectedProofTreeNode, VisualProofEditorProofTreeView, VisualProofEditorProofTreeViewId } from './visual-proof-editor-proof-tree-view';
@@ -17,6 +17,7 @@ import { createEmptyVisualProofEditorReasoningContextFromConclusion, createEmpty
 import { useReasoningContexts } from '../hooks/use-reasoning-contexts';
 import { useKeyPressed, useKeyUpEvent } from '../../../lib/hooks/use-key-event';
 import { createNumberGenerator } from '../proof-rule/proof-rule-handler/create-number-generator';
+import { v4 } from 'uuid';
 
 interface VisualProofEditorProps {
     prop: Prop;
@@ -146,17 +147,30 @@ export function VisualProofEditor({ prop, onProofTreeChange }: VisualProofEditor
         const droppedConclusion = droppedContext.proofTree.conclusion;
 
         // check if proof trees are compatible
-        if (!isEqual(droppedOnPremisse?.conclusion, droppedConclusion)) {
+
+        if (!proof_tree_conclusion_alpha_eq(droppedOnPremisse?.conclusion, droppedConclusion)) {
             notificationApi.error({ message: 'Proof trees not compatible.' });
             restorePositions();
             return;
         }
 
+        let replacementTree = droppedContext.proofTree;
+
+        // only alpha equivalent - add alpah-eq rule
+        if (!isEqual(droppedOnPremisse?.conclusion, droppedConclusion)) {
+            replacementTree = {
+                id: v4(),
+                premisses: [{ ...replacementTree }],
+                rule: { kind: 'AlphaEquivalent' },
+                conclusion: droppedOnPremisse.conclusion,
+            }
+        }
+
         // FIXME: shall I check if all assumptions can be used?
 
         // Merge
 
-        replaceTreeNodeById(droppedOnContext.proofTree, droppedOnPremisse.id, droppedContext.proofTree);
+        replaceTreeNodeById(droppedOnContext.proofTree, droppedOnPremisse.id, replacementTree);
 
         updateReasoningContexts([
             ...reasoningContexts.filter((ctx) => ctx.id !== droppedContext.id && ctx.id !== droppedOnContext.id),
@@ -381,6 +395,6 @@ const cssVisualProofEditorProofTreeViewContainer = css`
 
 const cssDivider = css`
     border-bottom: 1px solid #233348;
-    width: '99%';
+    width: 99%;
     align-self: center;
 `;

frontend/src/util/print-proof-rule.ts

@@ -18,5 +18,6 @@ export function printProofRule(proofTreeRule: ProofTreeRule): string {
         case 'ExistsIntro': return '\\exists I';
         case 'ExistsElim': return `\\exists E^{${proofTreeRule.value[0]}, ${proofTreeRule.value[1]}}`;
         case 'Sorry': return 'sorry';
+        case 'AlphaEquivalent': return ' \\alpha\\text{-Eq}'
     }
 }

src/kernel/checker/check.rs

@@ -3,6 +3,7 @@ use thiserror::Error;
 
 use crate::{
     kernel::{
+        proof::Proof,
         proof_term::{
             Abort, Application, Case, Function, Ident, LetIn, OrLeft, OrRight, Pair, ProjectFst,
             ProjectSnd, ProofTerm, ProofTermKind, ProofTermVisitor, Type, TypeAscription,
@@ -121,14 +122,23 @@ impl<'a> ProofTermVisitor<Result<ProofTree, CheckError>> for CheckVisitor<'a> {
             self.identifier_factory,
         )?;
 
+        if Type::eq(&_type, &self.expected_type) {
+            return Ok(proof_tree);
+        }
+
         if Type::alpha_eq(&_type, &self.expected_type) {
-            Ok(proof_tree)
-        } else {
-            Err(CheckError::UnexpectedType {
-                expected: self.expected_type.clone(),
-                received: _type,
-            })
+            let conclusion = match &self.expected_type {
+                Type::Prop(prop) => ProofTreeConclusion::PropIsTrue(prop.clone()),
+                Type::Datatype(_) => proof_tree.conclusion.clone(),
+            };
+
+            return Ok(proof_tree.create_alphq_eq_tree(conclusion));
         }
+
+        Err(CheckError::UnexpectedType {
+            expected: self.expected_type.clone(),
+            received: _type,
+        })
     }
 
     fn visit_pair(&mut self, pair: &Pair) -> Result<ProofTree, CheckError> {
@@ -211,14 +221,23 @@ impl<'a> ProofTermVisitor<Result<ProofTree, CheckError>> for CheckVisitor<'a> {
             self.identifier_factory,
         )?;
 
+        if Type::eq(&self.expected_type, &projection_type) {
+            return Ok(projection_proof_tree);
+        }
+
         if Type::alpha_eq(&self.expected_type, &projection_type) {
-            Ok(projection_proof_tree)
-        } else {
-            Err(CheckError::UnexpectedType {
-                expected: self.expected_type.clone(),
-                received: projection_type,
-            })
+            let conclusion = match self.expected_type {
+                Type::Prop(ref prop) => ProofTreeConclusion::PropIsTrue(prop.clone()),
+                Type::Datatype(_) => projection_proof_tree.conclusion.clone(),
+            };
+
+            return Ok(projection_proof_tree.create_alphq_eq_tree(conclusion));
         }
+
+        Err(CheckError::UnexpectedType {
+            expected: self.expected_type.clone(),
+            received: projection_type,
+        })
     }
 
     fn visit_project_snd(&mut self, projection: &ProjectSnd) -> Result<ProofTree, CheckError> {
@@ -231,14 +250,23 @@ impl<'a> ProofTermVisitor<Result<ProofTree, CheckError>> for CheckVisitor<'a> {
             self.identifier_factory,
         )?;
 
+        if Type::eq(&self.expected_type, &projection_type) {
+            return Ok(projection_proof_tree);
+        }
+
         if Type::alpha_eq(&self.expected_type, &projection_type) {
-            Ok(projection_proof_tree)
-        } else {
-            Err(CheckError::UnexpectedType {
-                expected: self.expected_type.clone(),
-                received: projection_type,
-            })
+            let conclusion = match &self.expected_type {
+                Type::Prop(prop) => ProofTreeConclusion::PropIsTrue(prop.clone()),
+                Type::Datatype(_) => projection_proof_tree.conclusion.clone(),
+            };
+
+            return Ok(projection_proof_tree.create_alphq_eq_tree(conclusion));
         }
+
+        Err(CheckError::UnexpectedType {
+            expected: self.expected_type.clone(),
+            received: projection_type,
+        })
     }
 
     fn visit_function(&mut self, function: &Function) -> Result<ProofTree, CheckError> {
@@ -360,15 +388,23 @@ impl<'a> ProofTermVisitor<Result<ProofTree, CheckError>> for CheckVisitor<'a> {
             self.identifier_factory,
         )?;
 
-        // test for alpha-equivalence
-        if !Type::alpha_eq(&application_type, &self.expected_type) {
-            return Err(CheckError::UnexpectedType {
-                expected: self.expected_type.clone(),
-                received: application_type,
-            });
+        if Type::eq(&application_type, &self.expected_type) {
+            return Ok(application_proof_tree);
         }
 
-        Ok(application_proof_tree)
+        if Type::alpha_eq(&application_type, &self.expected_type) {
+            let conclusion = match &self.expected_type {
+                Type::Prop(prop) => ProofTreeConclusion::PropIsTrue(prop.clone()),
+                Type::Datatype(_) => application_proof_tree.conclusion.clone(),
+            };
+
+            return Ok(application_proof_tree.create_alphq_eq_tree(conclusion));
+        }
+
+        Err(CheckError::UnexpectedType {
+            expected: self.expected_type.clone(),
+            received: application_type,
+        })
     }
 
     fn visit_let_in(&mut self, let_in: &LetIn) -> Result<ProofTree, CheckError> {

src/kernel/proof_tree.rs

@@ -4,7 +4,7 @@ use tsify_next::Tsify;
 
 use super::{checker::identifier::Identifier, prop::Prop};
 
-#[derive(PartialEq, Eq, Serialize, Deserialize, Tsify, Debug)]
+#[derive(Clone, PartialEq, Eq, Serialize, Deserialize, Tsify, Debug)]
 #[tsify(into_wasm_abi, from_wasm_abi)]
 #[serde(tag = "kind", content = "value")]
 pub enum ProofTreeRule {
@@ -24,20 +24,53 @@ pub enum ProofTreeRule {
     ExistsIntro,
     ExistsElim(String, String),
     Sorry,
+    AlphaEquivalent,
 }
 
-#[derive(PartialEq, Eq, Serialize, Deserialize, Tsify, Debug)]
+#[derive(Clone, PartialEq, Eq, Serialize, Deserialize, Tsify, Debug)]
 #[tsify(into_wasm_abi, from_wasm_abi)]
 #[serde(tag = "kind", content = "value")]
 pub enum ProofTreeConclusion {
     PropIsTrue(Prop),
     TypeJudgement(Identifier, String),
 }
 
-#[derive(PartialEq, Eq, Serialize, Deserialize, Tsify, Debug)]
+#[derive(Clone, PartialEq, Eq, Serialize, Deserialize, Tsify, Debug)]
 #[tsify(into_wasm_abi, from_wasm_abi)]
 pub struct ProofTree {
     pub premisses: Vec<ProofTree>,
     pub rule: ProofTreeRule,
     pub conclusion: ProofTreeConclusion,
 }
+
+impl ProofTree {
+    pub fn create_alphq_eq_tree(&self, conclusion: ProofTreeConclusion) -> ProofTree {
+        let own_conclusion = &self.conclusion;
+
+        match (own_conclusion, &conclusion) {
+            (
+                ProofTreeConclusion::PropIsTrue(ref own_prop),
+                ProofTreeConclusion::PropIsTrue(ref prop),
+            ) => {
+                if !Prop::alpha_eq(own_prop, prop) {
+                    panic!("Conclusions not alpha equivalent.");
+                }
+            }
+            (
+                ProofTreeConclusion::TypeJudgement(ref own_ident, ref own_datatype),
+                ProofTreeConclusion::TypeJudgement(ref ident, ref datatype),
+            ) => {
+                if !Identifier::eq(own_ident, ident) || !String::eq(own_datatype, datatype) {
+                    panic!("Conclusions not alpha equivalent.");
+                }
+            }
+            _ => panic!("Conclusions not alpha equivalent."),
+        }
+
+        ProofTree {
+            premisses: vec![self.to_owned()],
+            rule: ProofTreeRule::AlphaEquivalent,
+            conclusion,
+        }
+    }
+}

src/lib.rs

@@ -10,7 +10,7 @@ use kernel::{
     parse::{fol::fol_parser, lexer::lexer, proof::proof_parser},
     process::{stages::resolve_datatypes::ResolveDatatypes, ProofPipeline, ProofPipelineError},
     proof::Proof,
-    proof_tree::ProofTree,
+    proof_tree::{ProofTree, ProofTreeConclusion},
     prop::{Prop, PropParameter, QuantifierKind},
 };
 
@@ -172,6 +172,21 @@ pub fn bind_identifier(
     )
 }
 
+#[wasm_bindgen]
+pub fn proof_tree_conclusion_alpha_eq(fst: ProofTreeConclusion, snd: ProofTreeConclusion) -> bool {
+    match (fst, snd) {
+        (
+            ProofTreeConclusion::PropIsTrue(ref fst_prop),
+            ProofTreeConclusion::PropIsTrue(ref snd_prop),
+        ) => Prop::alpha_eq(fst_prop, snd_prop),
+        (
+            ProofTreeConclusion::TypeJudgement(fst_ident, fst_datatype),
+            ProofTreeConclusion::TypeJudgement(snd_ident, snd_datatype),
+        ) => (fst_ident == snd_ident) && (fst_datatype == snd_datatype),
+        _ => false,
+    }
+}
+
 #[wasm_bindgen]
 pub fn export_as_ocaml(prop: &Prop, proof_term: &str) -> String {
     if prop.has_quantifiers() {