Skip to content

Commit

Permalink
Merge pull request #27 from eneoli/feature/tutor
Browse files Browse the repository at this point in the history 
Feature/tutor
  • Loading branch information
@eneoli
eneoli authored Aug 19, 2024
2 parents 838fccd + f12ef81 commit fd9d49d
Show file tree
Hide file tree
Showing 34 changed files with 2,424 additions and 853 deletions.
2 changes: 1 addition & 1 deletion frontend/index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,6 @@
<title>Alice</title>
</head>
<body style="padding: 0; margin: 0;">
<div id="app"></div>
<div style="height: 100vh;" id="app"></div>
</body>
</html>
33 changes: 24 additions & 9 deletions frontend/package-lock.json
View file

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

5 changes: 3 additions & 2 deletions frontend/package.json
View file
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,7 @@
"globals": "^15.3.0",
"html-webpack-plugin": "^5.6.0",
"style-loader": "^4.0.0",
"typescript": "^5.4.5",
"typescript": "^5.5.4",
"typescript-eslint": "^7.8.0",
"webpack": "^5.91.0",
"webpack-cli": "^5.1.4",
Expand All @@ -46,6 +46,7 @@
"@monaco-editor/react": "^4.6.0",
"@react-aria/example-theme": "^1.0.3",
"alice": "file:../pkg",
"ansi-to-html": "^0.7.2",
"antd": "^5.19.0",
"better-react-mathjax": "^2.0.3",
"core-js": "^3.37.0",
Expand All @@ -57,7 +58,7 @@
"react-code-blocks": "^0.1.6",
"react-dom": "^18.3.1",
"react-merge-refs": "^2.1.1",
"sweetalert2": "^11.12.3",
"sweetalert2": "^11.6.13",
"sweetalert2-react-content": "^5.0.7",
"uuid": "^10.0.0"
}
Expand Down
185 changes: 129 additions & 56 deletions frontend/src/domain/app/components/app.tsx
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,14 +2,16 @@ import React, { 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, Drawer, message, theme as antdTheme, ThemeConfig } from 'antd';
import { Prop, export_as_ocaml, generate_proof_term_from_proof_tree, parse_prop, verify } from 'alice';
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 { debounce, isEqual } from 'lodash';
import { CodeModal } from './code-modal';
import { 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';

const mathjaxConfig: MathJax3Config = {
loader: {
Expand All @@ -26,11 +28,11 @@ const mathjaxConfig: MathJax3Config = {
};

export function App() {

const [proofTerm, setProofTerm] = useState('');
const [prop, setProp] = useState<Prop | null>(null);
const [showCodeExport, setShowCodeExport] = useState(false);
const [showTutor, setShowTutor] = useState(false);
const [verificationResult, setVerificationResult] = useState<VerificationResult | null>(null);
const [_messageApi, contextHolder] = message.useMessage();

const handlePropChange = debounce((propString: string) => {
Expand All @@ -39,38 +41,53 @@ export function App() {

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

setProofTerm('sorry');
const verificationResult = verify(newProp, 'sorry');
setVerificationResult(verificationResult);
}
} catch (e) {
setProp(null);
console.error(e);
}
}, 500);

const handleProofTreeChange = (proofTree: VisualProofEditorProofTree) => {
try {
const code = generate_proof_term_from_proof_tree(visualProofEditorProofTreeIntoAliceProofTree(proofTree));
console.log(code);
setProofTerm(code);
} catch(_) {
console.error('Generation failed');
const code = generate_proof_term_from_proof_tree(visualProofEditorProofTreeIntoAliceProofTree(proofTree));
setProofTerm(code);

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

const handleVerify = (prop: string) => {
let isProof = false;
try {
verify(prop, proofTerm);
isProof = true;
} catch (e) {
console.error(e);
const result = verify(parse_prop(prop), proofTerm);
setVerificationResult(result);

if (
result.kind === 'LexerError' ||
result.kind === 'ParserError' ||
result.kind === 'ProofPipelineError'
) {
message.error('Your input is malformed. Check the Tutor for more information.');
return;
}

if (isProof) {
message.success('Your proof is correct! Well done.');
} else {
message.error('Your proof is wrong.');
const isProof = result.kind === 'TypeCheckSucceeded';
const allGoalsClosed = result.kind === 'TypeCheckSucceeded' && result.value.result.goals.length === 0;

if (isProof && allGoalsClosed) {
message.success('Your proof is correct. Well done!');
}

if (isProof && !allGoalsClosed) {
message.info('You still have open goals.');
}

if (!isProof) {
message.error('Your proof contains errors.');
}
};

Expand All @@ -82,55 +99,111 @@ export function App() {
setShowCodeExport(true);
};

const handleVisualEditorReset = () => {
setProofTerm('sorry');

if (prop) {
setVerificationResult(verify(prop, 'sorry'));
}
};

return (
<ConfigProvider theme={theme}>
<MathJaxContext
src={mathjax}
config={mathjaxConfig}
version={3}>
{contextHolder}
<Header
onPropChange={handlePropChange}
onVerify={handleVerify}
onExportAsOcaml={handleOcamlExport}
onTutorClick={() => setShowTutor(true)}
/>

{prop && (
<>
<VisualProofEditor prop={prop} onProofTreeChange={handleProofTreeChange} />

<div style={{ marginTop: 20 }}>
<CodeEditor height={'20vh'} initialValue={proofTerm} onChange={setProofTerm} />
<div className={cssAppContainer}>
<Header
onPropChange={handlePropChange}
onVerify={handleVerify}
onExportAsOcaml={handleOcamlExport}
enableTutor={!!prop}
onTutorClick={() => setShowTutor(!showTutor)}
/>

<div className={cssBodyContainer}>
<div className={cssEditorContainer}>
{prop && (
<>
<VisualProofEditor
prop={prop}
onProofTreeChange={handleProofTreeChange}
onReset={handleVisualEditorReset}
/>

<div style={{ marginTop: 20 }}>
<CodeEditor height={'20vh'} initialValue={proofTerm} onChange={setProofTerm} />
</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
title='🐫 OCaml Export'
code={export_as_ocaml(prop, proofTerm)}
language='ocaml'
onClose={() => { setShowCodeExport(false) }}
/>
)
}
</div>
<div className={cssTutorContainer} style={{ marginRight: showTutor ? 0 : '-450px' }}>
{
verificationResult && (
<Tutor
code={proofTerm}
verificationResult={verificationResult}
/>
)
}
</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
title='🐫 OCaml Export'
code={export_as_ocaml(prop, proofTerm)}
language='ocaml'
onClose={() => { setShowCodeExport(false) }}
/>
)
}
<Drawer title={'💡 Tutor'} open={showTutor} onClose={() => setShowTutor(false)}>
Hallo!
</Drawer>
</div>
</MathJaxContext>
</ConfigProvider>
);
}

const cssAppContainer = css`
display: flex;
flex-direction: column;
height: 100%;
`;

const cssBodyContainer = css`
display: flex;
flex: 1;
flex-direction: row;
overflow-x: hidden;
`;

const cssEditorContainer = css`
flex: 1 1 auto;
flex-wrap: wrap;
overflow: auto;
`;

const cssTutorContainer = css`
box-sizing: border-box;
flex: 0 0 450px;
background: linear-gradient(90deg, rgba(46,77,97,1) 0%, rgba(43,63,89,1) 100%);
width: 450px;
height: 100%;
padding: 25px;
transition: width, 0.3s ease-in-out;
color: #fefefe;
`;

const theme: ThemeConfig = {
algorithm: antdTheme.darkAlgorithm,
token: {
Expand Down
Loading

0 comments on commit fd9d49d

Please sign in to comment.