Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Feature/dsl to UI #32

Merged
merged 48 commits into from
Aug 22, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
48 commits
Select commit Hold shift + click to select a range
3e5a38f
fixed parentheses for named function call
eneoli Aug 19, 2024
630b978
Let rules hold full Identifier
eneoli Aug 19, 2024
a4ddb3c
fixed print for datatype
eneoli Aug 19, 2024
cf889c7
adjusted print to work with Identifier
eneoli Aug 19, 2024
0722f20
use full identifier in rule
eneoli Aug 19, 2024
80ee175
handle error kind IncompatibleProofTerm
eneoli Aug 19, 2024
3d6a025
set progress to 100 when no goals left
eneoli Aug 19, 2024
c3ccb00
set value to initialValue only when it changes
eneoli Aug 19, 2024
25acfcd
added initialPrimaryReasoningContext and initialAssumptions
eneoli Aug 19, 2024
d079f51
added aliceProofTreeIntoVisualProofEditorProofTree
eneoli Aug 19, 2024
7c2f31c
added dsl to ui feature for main proof tree
eneoli Aug 19, 2024
b82827b
minor fix
eneoli Aug 19, 2024
4f9a668
added dist.zip
eneoli Aug 19, 2024
d759699
added rule delete button
eneoli Aug 21, 2024
4f68bcc
added rule delete button
eneoli Aug 21, 2024
908e577
added Cross svg
eneoli Aug 21, 2024
080ca02
added margin-bottom for FireFox ^-^
eneoli Aug 21, 2024
df6f540
added rule for direction
eneoli Aug 21, 2024
41c449d
fixed assumption direction
eneoli Aug 21, 2024
94529c1
debounce, remove assumptions when prop changes
eneoli Aug 21, 2024
7609655
added onRuleDeleteClick prop
eneoli Aug 21, 2024
b3cba6a
added onRuleDeleteClick prop
eneoli Aug 21, 2024
69857e1
Added button for Upwards and Downwards reasoning
eneoli Aug 21, 2024
c662cd6
added canReasonUpwards and canReasonDownwards
eneoli Aug 21, 2024
5f1ac7b
canReasonDownwards false
eneoli Aug 21, 2024
6347e25
canReasonDownwards false
eneoli Aug 21, 2024
2e7f7ec
export SelectedProofTreeNode
eneoli Aug 21, 2024
fce3100
fixed premisses order
eneoli Aug 21, 2024
509f007
implemented canReasonUpwards and canReasonDownwards
eneoli Aug 22, 2024
9e8b4db
cleanup
eneoli Aug 22, 2024
082e4d9
implemented canReasonUpwards and canReasonDownwards
eneoli Aug 22, 2024
22bb2aa
bugfix for OrElim export
eneoli Aug 22, 2024
1e76c0b
added Type ascription to CaseExpr
eneoli Aug 22, 2024
eed2cbc
add type ascriptions to sorry when needed
eneoli Aug 22, 2024
994c140
added possibility to unglue proof trees
eneoli Aug 22, 2024
6286e30
added atom as keyword
eneoli Aug 22, 2024
be90b0c
added display for kind DatatypeUnknown
eneoli Aug 22, 2024
013e323
cleanup
eneoli Aug 22, 2024
9405a78
added get_datatypes method
eneoli Aug 22, 2024
20b47e8
cleanup
eneoli Aug 22, 2024
134d69b
added prop to ProofPipeline process/apply method
eneoli Aug 22, 2024
de8518e
added declarations to tests
eneoli Aug 22, 2024
0ffd520
skip identifiers that used in initialAssumptions
eneoli Aug 22, 2024
c6567b6
add decls to sorry proof term
eneoli Aug 22, 2024
d34b31d
added print_prop_decls, add prop for ProofPipeline
eneoli Aug 22, 2024
a78ef07
check for atoms/datatypes in prop
eneoli Aug 22, 2024
e8c0219
Replaced -> with ⊃
eneoli Aug 22, 2024
fd8c105
cleanup
eneoli Aug 22, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions .gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ target
pkg

dist
dist.zip
frontend/dist
frontend/node_modules

Expand Down
148 changes: 113 additions & 35 deletions frontend/src/domain/app/components/app.tsx
Original file line number Diff line number Diff line change
@@ -1,17 +1,20 @@
import React, { useState } from 'react';
import React, { useCallback, useState } from 'react';
import { Header } from './header';
import { CodeEditor } from '../../code-editor/components/code-editor';
import { VisualProofEditor } from '../../visual-proof-editor/components/visual-proof-editor';
import { ConfigProvider, message, theme as antdTheme, ThemeConfig } from 'antd';
import { Prop, VerificationResult, export_as_ocaml, generate_proof_term_from_proof_tree, parse_prop, verify } from 'alice';
import { Prop, VerificationResult, export_as_ocaml, generate_proof_term_from_proof_tree, parse_prop, print_prop_decls, verify } from 'alice';
import { debounce, isEqual } from 'lodash';
import { CodeModal } from './code-modal';
import { VisualProofEditorProofTree, visualProofEditorProofTreeIntoAliceProofTree } from '../../visual-proof-editor/lib/visual-proof-editor-proof-tree';
import { aliceProofTreeIntoVisualProofEditorProofTree, VisualProofEditorProofTree, visualProofEditorProofTreeIntoAliceProofTree } from '../../visual-proof-editor/lib/visual-proof-editor-proof-tree';
import { MathJax3Config, MathJaxContext } from 'better-react-mathjax';
import mathjax from 'mathjax/es5/tex-svg';
import bussproofs from 'mathjax/es5/input/tex/extensions/bussproofs'
import { Tutor } from '../../tutor/components/tutor';
import { css } from '@emotion/css';
import { AssumptionContext } from '../../visual-proof-editor/proof-rule';
import { v4 } from 'uuid';
import { VisualProofEditorReasoningContext } from '../../visual-proof-editor/lib/visual-proof-editor-reasoning-context';

const mathjaxConfig: MathJax3Config = {
loader: {
Expand All @@ -35,34 +38,99 @@ export function App() {
const [verificationResult, setVerificationResult] = useState<VerificationResult | null>(null);
const [_messageApi, contextHolder] = message.useMessage();

const [initialPrimaryContext, setInitialPrimaryContext] = useState<VisualProofEditorReasoningContext | null>(null);
const [initialAssumptions, setInitialAssumptions] = useState<AssumptionContext[]>([]);

const handlePropChange = debounce((propString: string) => {
try {
const newProp = parse_prop(propString);

if (!isEqual(prop, newProp)) {
setProp(newProp);
setProofTerm('sorry');

const verificationResult = verify(newProp, 'sorry');
setVerificationResult(verificationResult);
if (isEqual(prop, newProp)) {
return;
}

setProp(newProp);

const newProofTerm = `${print_prop_decls(newProp)}\n\nsorry`;

setProofTerm(newProofTerm);
setInitialAssumptions([]);

const verificationResult = verify(newProp, newProofTerm);
setVerificationResult(verificationResult);

const proofTree: VisualProofEditorProofTree = {
id: v4(),
premisses: [],
rule: null,
conclusion: { kind: 'PropIsTrue', value: newProp },
};

const primaryCtx: VisualProofEditorReasoningContext = {
id: v4(),
selectedNodeId: null,
isDragging: false,
x: 0,
y: 0,
proofTree: proofTree,
};

setInitialPrimaryContext(primaryCtx);
} catch (e) {
setProp(null);
console.error(e);
}
}, 500);

const handleProofTreeChange = (proofTree: VisualProofEditorProofTree) => {
const code = generate_proof_term_from_proof_tree(visualProofEditorProofTreeIntoAliceProofTree(proofTree));
setProofTerm(code);
const handleProofTermChange = useCallback(debounce((newProofTerm: string) => {
if (newProofTerm.trim() === proofTerm.trim()) {
return;
}

if (prop) {
const result = verify(prop, code);
setVerificationResult(result);
setProofTerm(newProofTerm);

if (!prop) {
return;
}

const verificationResult = verify(prop, newProofTerm);
setVerificationResult(verificationResult);

if (verificationResult.kind === 'TypeCheckSucceeded') {
const primaryReasoningCtxId = v4();
const proofTree = verificationResult.value.result.proof_tree;
const proofTreeResult = aliceProofTreeIntoVisualProofEditorProofTree(primaryReasoningCtxId, proofTree);

const primaryCtx: VisualProofEditorReasoningContext = {
id: primaryReasoningCtxId,
selectedNodeId: null,
isDragging: false,
x: 0,
y: 0,
proofTree: proofTreeResult.proofTree
};

setInitialPrimaryContext(primaryCtx);
setInitialAssumptions(proofTreeResult.assumptions);
}
}, 500), [proofTerm, prop]);

const handleProofTreeChange = useCallback((proofTree: VisualProofEditorProofTree) => {
if (!prop) {
return;
}
};

const handleVerify = (prop: string) => {
const code = generate_proof_term_from_proof_tree(
visualProofEditorProofTreeIntoAliceProofTree(proofTree),
prop,
);
setProofTerm(code);

const result = verify(prop, code);
setVerificationResult(result);
}, [prop]);

const handleVerify = useCallback((prop: string) => {
const result = verify(parse_prop(prop), proofTerm);
setVerificationResult(result);

Expand All @@ -89,23 +157,27 @@ export function App() {
if (!isProof) {
message.error('Your proof contains errors.');
}
};
}, [proofTerm, message]);

const handleOcamlExport = () => {
const handleOcamlExport = useCallback(() => {
if (!prop) {
return;
}

setShowCodeExport(true);
};

const handleVisualEditorReset = () => {
setProofTerm('sorry');
}, [prop]);

if (prop) {
setVerificationResult(verify(prop, 'sorry'));
const handleVisualEditorReset = useCallback(() => {
if (!prop) {
return;
}
};

const proofTerm = `${print_prop_decls(prop)}\n\nsorry`;

setProofTerm(proofTerm);

setVerificationResult(verify(prop, proofTerm));
}, [prop]);

return (
<ConfigProvider theme={theme}>
Expand All @@ -125,27 +197,33 @@ export function App() {

<div className={cssBodyContainer}>
<div className={cssEditorContainer}>
{prop && (
{!(prop && initialPrimaryContext) && (
<div style={{ textAlign: 'center', color: '#192434' }}>
<h1>Alice is ready.</h1>
<h2>Please enter a proposition to begin.</h2>
</div>
)}

{prop && initialPrimaryContext && (
<>
<VisualProofEditor
prop={prop}
initialPrimaryReasoningContext={initialPrimaryContext}
initialAssumptions={initialAssumptions}
onProofTreeChange={handleProofTreeChange}
onReset={handleVisualEditorReset}
/>

<div style={{ marginTop: 20 }}>
<CodeEditor height={'20vh'} initialValue={proofTerm} onChange={setProofTerm} />
<CodeEditor
height={'20vh'}
initialValue={proofTerm}
onChange={handleProofTermChange}
/>
</div>
</>
)}

{!prop && (
<div style={{ textAlign: 'center', color: '#192434' }}>
<h1>Alice is ready.</h1>
<h2>Please enter a proposition to begin.</h2>
</div>
)}

{
(showCodeExport && prop) && (
<CodeModal
Expand Down
8 changes: 5 additions & 3 deletions frontend/src/domain/app/components/header.tsx
Original file line number Diff line number Diff line change
Expand Up @@ -36,16 +36,17 @@ export function Header({ onPropChange, onVerify, onExportAsOcaml, enableTutor, o

replaceSymbol('\\not', '¬');
replaceSymbol('!', '¬');
replaceSymbol('~', '¬');

replaceSymbol('\\and', '∧');
replaceSymbol('&', '∧');

replaceSymbol('\\or', '∨');
replaceSymbol('|', '∨');

replaceSymbol('\\implies', '');
replaceSymbol('->', '');
replaceSymbol('=>', '');
replaceSymbol('\\implies', '');
replaceSymbol('->', '');
replaceSymbol('=>', '');

replaceSymbol('\\top', '⊤');
replaceSymbol('\\bot', '⊥');
Expand Down Expand Up @@ -114,6 +115,7 @@ const cssHeaderTitle = css`
font-size: 35px;
color: white;
text-align: center;
margin-bottom: 10px;
`;

const cssHeaderSubtitle = css`
Expand Down
4 changes: 2 additions & 2 deletions frontend/src/domain/code-editor/components/code-editor.tsx
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ interface CodeEditorProps {
function handleEditorWillMount(monaco: Monaco) {
monaco.languages.typescript.javascriptDefaults.setEagerModelSync(true);

const keywords = ['fn', 'case', 'of', 'let', 'in', 'datatype', 'inl', 'inr', 'fst', 'snd', 'sorry'];
const keywords = ['fn', 'case', 'of', 'let', 'in', 'atom', 'datatype', 'inl', 'inr', 'fst', 'snd', 'sorry'];

monaco.languages.register({ id: 'alice' });
monaco.languages.setMonarchTokensProvider('alice', {
Expand Down Expand Up @@ -125,7 +125,7 @@ export function CodeEditor(props: CodeEditorProps) {

useEffect(() => {
setValue(initialValue);
});
}, [initialValue]);

const onValueChange = (value: string | undefined) => {
setValue(value || '');
Expand Down
9 changes: 9 additions & 0 deletions frontend/src/domain/proof-tree/components/cross.tsx
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
import React from 'react';

export function Cross() {
return (
<svg width={'25px'} height={'25px'} xmlns="http://www.w3.org/2000/svg" fill="none" viewBox="0 0 24 24" strokeWidth={1.5} stroke="currentColor" className="size-6">
<path strokeLinecap="round" strokeLinejoin="round" d="m9.75 9.75 4.5 4.5m0-4.5-4.5 4.5M21 12a9 9 0 1 1-18 0 9 9 0 0 1 18 0Z" />
</svg>
);
}
28 changes: 25 additions & 3 deletions frontend/src/domain/proof-tree/components/proof-line.tsx
Original file line number Diff line number Diff line change
@@ -1,14 +1,16 @@
import { css } from '@emotion/css';
import React, { useEffect, useRef } from 'react';
import React, { useEffect, useRef, MouseEvent } from 'react';
import Katex from 'katex';
import { ProofTreeRule } from 'alice';
import { printProofRule } from '../../../util/print-proof-rule';
import { Cross } from './cross';

interface ProofLineProps {
rule: ProofTreeRule;
onDeleteClick: () => void;
}

export function ProofLine({ rule }: ProofLineProps) {
export function ProofLine({ rule, onDeleteClick }: ProofLineProps) {

const labelRef = useRef<HTMLDivElement>(null);

Expand All @@ -24,15 +26,27 @@ export function ProofLine({ rule }: ProofLineProps) {
});
}, [labelRef.current, rule]);

const handleDeleteClick = (e: MouseEvent) => {
e.stopPropagation();
onDeleteClick();
}

return (
<div className={cssLineContainer}>
<div
className={cssLine}
style={{ borderStyle: rule.kind === 'AlphaEquivalent' ? 'dashed' : undefined }}
/>
<div className={cssLabelContainer}>
<div className={cssLabel}>
<div className={cssLabel} style={{ display: 'flex' }}>
<div ref={labelRef} />
<span
className='cssProofRuleDeleteButton'
style={{ cursor: 'pointer' }}
onClick={handleDeleteClick}
>
<Cross />
</span>
</div>
</div>
</div>);
Expand All @@ -43,6 +57,14 @@ const cssLineContainer = css`
align-items: center;
gap: 2px;
user-select: none;

.cssProofRuleDeleteButton {
display: none;
}

:hover .cssProofRuleDeleteButton {
display: block;
}
`;

const cssLine = css`
Expand Down
6 changes: 4 additions & 2 deletions frontend/src/domain/proof-tree/components/proof-node.tsx
Original file line number Diff line number Diff line change
Expand Up @@ -7,9 +7,11 @@ interface ProofNodeProps {
rule: ProofTreeRule | null;
content: ReactNode
children?: ReactNode
onRuleDeleteClick: () => void;
}

export function ProofNode({ children, content, rule }: ProofNodeProps) {
export function ProofNode(props: ProofNodeProps) {
const { rule, content, children, onRuleDeleteClick } = props;

return (
<div className={cssProofNode}>
Expand All @@ -18,7 +20,7 @@ export function ProofNode({ children, content, rule }: ProofNodeProps) {
</div>

{rule && (
<ProofLine rule={rule} />
<ProofLine onDeleteClick={onRuleDeleteClick} rule={rule} />
)}

<div className={cssConclusion}>
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,17 @@ export function TutorProofPipelineErrorDisplay(props: TutorProofPipelineErrorDis
</li>
)
}
{
resolveDatatypesError.kind === 'DatatypeUnknown' && (
<li>
{ei('DatatypeUnknown')}
Datatype `{resolveDatatypesError.value}` is unknown.
<br />
<br />
<span style={{ color: '#50B498' }}>Hint</span>: Add a declaration: `datatype {resolveDatatypesError.value};`
</li>
)
}
{
resolveDatatypesError.kind === 'DuplicateIdentifier' && (
<li>
Expand Down
Loading