phc
/
lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

convert tabs to spaces

Browse Source
pull/43/head
Alexander Bentkamp 2 years ago
parent 054e28c1ec
commit d2fd1c5915
6 changed files with 293 additions and 293 deletions
Show Stats Download Patch File Download Diff File

96
client/src/App.tsx
Unescape Escape View File

@ -16,67 +16,67 @@ import GoodBye from './components/GoodBye';
import useWebSocket from 'react-use-websocket';
function App() {
const [title, setTitle] = useState("")
const [conclusion, setConclusion] = useState("")
const [levelTitle, setLevelTitle] = useState("")
const [nbLevels, setNbLevels] = useState(0)
const [curLevel, setCurLevel] = useState(0)
const [finished, setFinished] = useState(false)
const [rpcConnection, setRpcConnection] = useState<null|rpc.MessageConnection>(null)
const [title, setTitle] = useState("")
const [conclusion, setConclusion] = useState("")
const [levelTitle, setLevelTitle] = useState("")
const [nbLevels, setNbLevels] = useState(0)
const [curLevel, setCurLevel] = useState(0)
const [finished, setFinished] = useState(false)
const [rpcConnection, setRpcConnection] = useState<null|rpc.MessageConnection>(null)
const socketUrl = 'ws://' + window.location.host + '/websocket/'
const socketUrl = 'ws://' + window.location.host + '/websocket/'
useWebSocket(socketUrl, {
onOpen: function (ev) {
const logger = new rpc.ConsoleLogger();
useWebSocket(socketUrl, {
onOpen: function (ev) {
const logger = new rpc.ConsoleLogger();
const socket = rpc.toSocket(ev.target as WebSocket);
let rpcConnection = rpc.createWebSocketConnection(socket, logger)
let rpcConnection = rpc.createWebSocketConnection(socket, logger)
setRpcConnection(rpcConnection);
rpcConnection.listen();
}
})
rpcConnection.listen();
}
})
const mathJaxConfig = {
loader: {
load: ['input/tex-base', 'output/svg']
},
const mathJaxConfig = {
loader: {
load: ['input/tex-base', 'output/svg']
},
tex: {
inlineMath: [['$', '$'], ['\\(', '\\)']]
},
svg: {
fontCache: 'global'
}
inlineMath: [['$', '$'], ['\\(', '\\)']]
},
svg: {
fontCache: 'global'
}
}
function startGame() {
setCurLevel(1)
}
function startGame() {
setCurLevel(1)
}
let mainComponent;
if (finished) {
mainComponent = <GoodBye message={conclusion} />
} else if (curLevel > 0) {
mainComponent = <Level rpcConnection={rpcConnection} nbLevels={nbLevels} level={curLevel} setCurLevel={setCurLevel} setLevelTitle={setLevelTitle} setFinished={setFinished}/>
} else {
let mainComponent;
if (finished) {
mainComponent = <GoodBye message={conclusion} />
} else if (curLevel > 0) {
mainComponent = <Level rpcConnection={rpcConnection} nbLevels={nbLevels} level={curLevel} setCurLevel={setCurLevel} setLevelTitle={setLevelTitle} setFinished={setFinished}/>
} else {
mainComponent = <Welcome rpcConnection={rpcConnection} setNbLevels={setNbLevels} setTitle={setTitle} startGame={startGame} setConclusion={setConclusion}/>
}
}
return (
<div className="App">
<MathJaxContext config={mathJaxConfig}>
<CssBaseline />
<AppBar position="sticky" sx={{ zIndex: (theme) => theme.zIndex.drawer + 1 }}>
<Toolbar sx={{ justifyContent: "space-between" }}>
<Typography variant="h6" noWrap component="div">
{title}
</Typography>
<Typography variant="h6" noWrap component="div">
{levelTitle}
</Typography>
</Toolbar>
</AppBar>
{mainComponent}
</MathJaxContext>
<MathJaxContext config={mathJaxConfig}>
<CssBaseline />
<AppBar position="sticky" sx={{ zIndex: (theme) => theme.zIndex.drawer + 1 }}>
<Toolbar sx={{ justifyContent: "space-between" }}>
<Typography variant="h6" noWrap component="div">
{title}
</Typography>
<Typography variant="h6" noWrap component="div">
{levelTitle}
</Typography>
</Toolbar>
</AppBar>
{mainComponent}
</MathJaxContext>
</div>
)
}

20
client/src/components/GoodBye.tsx
Unescape Escape View File

@ -8,16 +8,16 @@ import { Box, Typography, Grid } from '@mui/material';
function GoodBye({ message }) {
return (<Grid container
direction="row"
justifyContent="center"
alignItems="center">
<Grid item xs={12} sm={6}>
<Box sx={{ m: 3 }}>
<Typography variant="body1" component="div">{message}</Typography>
</Box>
</Grid>
</Grid>)
return (<Grid container
direction="row"
justifyContent="center"
alignItems="center">
<Grid item xs={12} sm={6}>
<Box sx={{ m: 3 }}>
<Typography variant="body1" component="div">{message}</Typography>
</Box>
</Grid>
</Grid>)
}
export default GoodBye

110
client/src/components/LeftPanel.tsx
Unescape Escape View File

@ -12,72 +12,72 @@ import ExpandMoreIcon from '@mui/icons-material/ExpandMore';
function TacticDoc(props) {
return (
<Accordion>
<AccordionSummary expandIcon={<ExpandMoreIcon />}>
<Typography>{props.tactic.name}</Typography>
</AccordionSummary>
<AccordionDetails>
<MathJax>
<ReactMarkdown>{props.tactic.content}</ReactMarkdown>
</MathJax>
</AccordionDetails>
</Accordion>)
return (
<Accordion>
<AccordionSummary expandIcon={<ExpandMoreIcon />}>
<Typography>{props.tactic.name}</Typography>
</AccordionSummary>
<AccordionDetails>
<MathJax>
<ReactMarkdown>{props.tactic.content}</ReactMarkdown>
</MathJax>
</AccordionDetails>
</Accordion>)
}
function LemmaDoc({ lemma }) {
return (
<Accordion>
<AccordionSummary expandIcon={<ExpandMoreIcon />}>
<Typography>{lemma.userName}</Typography>
</AccordionSummary>
<AccordionDetails>
<MathJax>
<ReactMarkdown>{lemma.content}</ReactMarkdown>
</MathJax>
</AccordionDetails>
</Accordion>)
return (
<Accordion>
<AccordionSummary expandIcon={<ExpandMoreIcon />}>
<Typography>{lemma.userName}</Typography>
</AccordionSummary>
<AccordionDetails>
<MathJax>
<ReactMarkdown>{lemma.content}</ReactMarkdown>
</MathJax>
</AccordionDetails>
</Accordion>)
}
function LemmaDocs({ lemmas }) {
const [categories, setCategories] = useState(new Map())
const [curCategory, setCurCategory] = useState("")
const [categories, setCategories] = useState(new Map())
const [curCategory, setCurCategory] = useState("")
useEffect(() => {
const cats = new Map()
lemmas.forEach(function (item) {
const category = item.category
cats.set(category, (cats.get(category) || []).concat([item]))
});
setCategories(cats)
setCurCategory(cats.keys().next().value)
}, [lemmas]);
useEffect(() => {
const cats = new Map()
lemmas.forEach(function (item) {
const category = item.category
cats.set(category, (cats.get(category) || []).concat([item]))
});
setCategories(cats)
setCurCategory(cats.keys().next().value)
}, [lemmas]);
return (
<Paper sx={{ px: 2, py: 1, mt: 2 }}>
<Typography variant="h5">Inventory</Typography>
<Box sx={{ borderBottom: 1, borderColor: 'divider' }}>
<Tabs
value={curCategory}
aria-label="Categories" variant="scrollable" scrollButtons="auto">
{(Array.from(categories)).map(([category, _]) => <Tab value={category} label={category} key={category} wrapped />)}
</Tabs>
</Box>
{curCategory && categories.get(curCategory).map((lemma) => <LemmaDoc lemma={lemma} key={lemma.name} />)}
</Paper>
)
return (
<Paper sx={{ px: 2, py: 1, mt: 2 }}>
<Typography variant="h5">Inventory</Typography>
<Box sx={{ borderBottom: 1, borderColor: 'divider' }}>
<Tabs
value={curCategory}
aria-label="Categories" variant="scrollable" scrollButtons="auto">
{(Array.from(categories)).map(([category, _]) => <Tab value={category} label={category} key={category} wrapped />)}
</Tabs>
</Box>
{curCategory && categories.get(curCategory).map((lemma) => <LemmaDoc lemma={lemma} key={lemma.name} />)}
</Paper>
)
}
function LeftPanel({ spells, inventory }) {
return (
<Box>
{spells.length > 0 &&
<Paper sx={{ px: 2, py: 1 }}>
<Typography variant="h5" sx={{ mb: 2 }}>Spell book</Typography>
{spells.map((spell) => <TacticDoc key={spell.name} tactic={spell} />)}
</Paper>}
{inventory.length > 0 && <LemmaDocs lemmas={inventory} />}
</Box>)
return (
<Box>
{spells.length > 0 &&
<Paper sx={{ px: 2, py: 1 }}>
<Typography variant="h5" sx={{ mb: 2 }}>Spell book</Typography>
{spells.map((spell) => <TacticDoc key={spell.name} tactic={spell} />)}
</Paper>}
{inventory.length > 0 && <LemmaDocs lemmas={inventory} />}
</Box>)
}
export default LeftPanel;

186
client/src/components/Level.tsx
Unescape Escape View File

@ -16,102 +16,102 @@ import * as rpc from 'vscode-ws-jsonrpc';
interface LevelProps {
rpcConnection: null|rpc.MessageConnection;
nbLevels: any;
level: any;
setCurLevel: any;
setLevelTitle: any;
setFinished: any
level: any;
setCurLevel: any;
setLevelTitle: any;
setFinished: any
}
function Level({ rpcConnection, nbLevels, level, setCurLevel, setLevelTitle, setFinished }: LevelProps) {
const [index, setIndex] = useState(level) // Level number
const [tacticDocs, setTacticDocs] = useState([])
const [lemmaDocs, setLemmaDocs] = useState([])
const [leanData, setLeanData] = useState({goals: []})
const [history, setHistory] = useState([])
const [lastTactic, setLastTactic] = useState("")
const [errors, setErrors] = useState([])
const [message, setMessage] = useState("")
const [messageOpen, setMessageOpen] = useState(false)
const [completed, setCompleted] = useState(false)
const processResponse = (res:any) => {
setLeanData(res);
setErrors(res.errors);
if (res.message !== "" && res.errors?.length === 0) {
setMessage(res.message)
setMessageOpen(true)
}
if (res.goals?.length === 0 && res.errors?.length === 0) {
setCompleted(true)
}
}
// The next function will be called when the level changes
useEffect(() => {
if (rpcConnection) {
rpcConnection.sendRequest("loadLevel", {number: level}).then((res) => {
setLevelTitle("Level " + res["index"] + ": " + res["title"])
setIndex(parseInt(res["index"]))
setTacticDocs(res["tactics"])
setLemmaDocs(res["lemmas"])
processResponse(res)
});
}
}, [level, rpcConnection])
function sendTactic(input) {
rpcConnection.sendRequest("runTactic", {tactic: input}).then(processResponse);
setLastTactic(input);
setHistory(history.concat([input]));
}
function undo() {
if (errors.length === 0) {
rpcConnection.sendRequest('undo').then(processResponse);
}
if (history.length > 1) {
setLastTactic(history[history.length - 1]);
} else {
setLastTactic("");
};
setErrors([]);
setHistory(history.slice(0, -1));
}
function loadNextLevel() {
setCompleted(false)
setHistory([])
setCurLevel(index + 1)
}
function closeMessage() {
setMessageOpen(false)
}
function finishGame() {
setLevelTitle("")
setFinished(true)
}
return (
<Grid container sx={{ mt: 3, ml: 1, mr: 1 }} columnSpacing={{ xs: 1, sm: 2, md: 3 }}>
<Grid xs={4}>
<LeftPanel spells={tacticDocs} inventory={lemmaDocs} />
</Grid>
<Grid xs={4}>
<InputZone index={index} history={history} messageOpen={messageOpen} setMessageOpen={setMessageOpen} completed={completed} sendTactic={sendTactic} nbLevels={nbLevels} loadNextLevel={loadNextLevel}
errors={errors} lastTactic={lastTactic} undo={undo} finishGame={finishGame} />
<Message isOpen={messageOpen} content={message} close={closeMessage} />
</Grid>
<Grid xs={4}>
<TacticState goals={leanData.goals} errors={errors} lastTactic={lastTactic} completed={completed} />
</Grid>
</Grid>
)
const [index, setIndex] = useState(level) // Level number
const [tacticDocs, setTacticDocs] = useState([])
const [lemmaDocs, setLemmaDocs] = useState([])
const [leanData, setLeanData] = useState({goals: []})
const [history, setHistory] = useState([])
const [lastTactic, setLastTactic] = useState("")
const [errors, setErrors] = useState([])
const [message, setMessage] = useState("")
const [messageOpen, setMessageOpen] = useState(false)
const [completed, setCompleted] = useState(false)
const processResponse = (res:any) => {
setLeanData(res);
setErrors(res.errors);
if (res.message !== "" && res.errors?.length === 0) {
setMessage(res.message)
setMessageOpen(true)
}
if (res.goals?.length === 0 && res.errors?.length === 0) {
setCompleted(true)
}
}
// The next function will be called when the level changes
useEffect(() => {
if (rpcConnection) {
rpcConnection.sendRequest("loadLevel", {number: level}).then((res) => {
setLevelTitle("Level " + res["index"] + ": " + res["title"])
setIndex(parseInt(res["index"]))
setTacticDocs(res["tactics"])
setLemmaDocs(res["lemmas"])
processResponse(res)
});
}
}, [level, rpcConnection])
function sendTactic(input) {
rpcConnection.sendRequest("runTactic", {tactic: input}).then(processResponse);
setLastTactic(input);
setHistory(history.concat([input]));
}
function undo() {
if (errors.length === 0) {
rpcConnection.sendRequest('undo').then(processResponse);
}
if (history.length > 1) {
setLastTactic(history[history.length - 1]);
} else {
setLastTactic("");
};
setErrors([]);
setHistory(history.slice(0, -1));
}
function loadNextLevel() {
setCompleted(false)
setHistory([])
setCurLevel(index + 1)
}
function closeMessage() {
setMessageOpen(false)
}
function finishGame() {
setLevelTitle("")
setFinished(true)
}
return (
<Grid container sx={{ mt: 3, ml: 1, mr: 1 }} columnSpacing={{ xs: 1, sm: 2, md: 3 }}>
<Grid xs={4}>
<LeftPanel spells={tacticDocs} inventory={lemmaDocs} />
</Grid>
<Grid xs={4}>
<InputZone index={index} history={history} messageOpen={messageOpen} setMessageOpen={setMessageOpen} completed={completed} sendTactic={sendTactic} nbLevels={nbLevels} loadNextLevel={loadNextLevel}
errors={errors} lastTactic={lastTactic} undo={undo} finishGame={finishGame} />
<Message isOpen={messageOpen} content={message} close={closeMessage} />
</Grid>
<Grid xs={4}>
<TacticState goals={leanData.goals} errors={errors} lastTactic={lastTactic} completed={completed} />
</Grid>
</Grid>
)
}
export default Level

102
client/src/components/TacticState.tsx
Unescape Escape View File

@ -11,59 +11,59 @@ import { Paper, Box, Typography } from '@mui/material';
const errorRegex = /<stdin>:1:(?<col>[^:]*): (?<msg>.*)/;
function Goal({ goal }) {
const hasObject = typeof goal.objects === "object" && goal.objects.length > 0
const hasAssumption = typeof goal.assumptions === "object" && goal.assumptions.length > 0
return (
<Box sx={{ pl: 2 }}>
{hasObject && <Box><Typography>Objects</Typography>
<List>
{goal.objects.map((item) =>
<ListItem key={item[0]}>
<Typography color="primary" sx={{ mr: 1 }}>{item[0]}</Typography> :
<Typography color="secondary" sx={{ ml: 1 }}>{item[1]}</Typography>
</ListItem>)}
</List></Box>}
{hasAssumption && <Box><Typography>Assumptions</Typography>
<List>
{goal.assumptions.map((item) => <ListItem key={item}><Typography color="primary" sx={{ mr: 1 }}>{item[0]}</Typography> :
<Typography color="secondary" sx={{ ml: 1 }}>{item[1]}</Typography></ListItem>)}
</List></Box>}
<Typography>Prove:</Typography>
<Typography color="primary" sx={{ ml: 2 }}>{goal.goal}</Typography>
</Box>)
const hasObject = typeof goal.objects === "object" && goal.objects.length > 0
const hasAssumption = typeof goal.assumptions === "object" && goal.assumptions.length > 0
return (
<Box sx={{ pl: 2 }}>
{hasObject && <Box><Typography>Objects</Typography>
<List>
{goal.objects.map((item) =>
<ListItem key={item[0]}>
<Typography color="primary" sx={{ mr: 1 }}>{item[0]}</Typography> :
<Typography color="secondary" sx={{ ml: 1 }}>{item[1]}</Typography>
</ListItem>)}
</List></Box>}
{hasAssumption && <Box><Typography>Assumptions</Typography>
<List>
{goal.assumptions.map((item) => <ListItem key={item}><Typography color="primary" sx={{ mr: 1 }}>{item[0]}</Typography> :
<Typography color="secondary" sx={{ ml: 1 }}>{item[1]}</Typography></ListItem>)}
</List></Box>}
<Typography>Prove:</Typography>
<Typography color="primary" sx={{ ml: 2 }}>{goal.goal}</Typography>
</Box>)
}
function TacticState({ goals, errors, lastTactic, completed }) {
const hasError = typeof errors === "object" && errors.length > 0
const hasGoal = typeof goals === "object" && goals.length > 0
const hasManyGoal = hasGoal && goals.length > 1
var col = ""
var msg = ""
if (hasError) {
const m = errors[0].match(errorRegex)
if (m) {
col = `Column ${m.groups.col}: `
msg = m.groups.msg
} else {
msg = errors[0]
if (msg === "Unrecognized tactic") { msg = "Unknown spell!" }
}
}
return (
<Box sx={{ height: "100%" }}>
{hasGoal && <Paper sx={{ pt: 1, pl: 2, pr: 3, pb: 1, height: "100%" }}><Typography variant="h5">Current goal</Typography> <Goal goal={goals[0]} /></Paper>}
{completed && <Typography variant="h6">Level completed ! 🎉</Typography>}
{hasError && <Paper sx={{ pt: 1, pl: 2, pr: 3, pb: 1, height: "100%" }}><Typography variant="h5" color="error">Spell invocation failed</Typography>
<Typography sx={{ my: 1 }}>{lastTactic}</Typography>
<Typography component="pre" sx={{ my: 1 }}>{col}{msg}</Typography>
<Typography>Use the undo button to go back to a sane state.</Typography>
</Paper>}
{hasManyGoal && <Paper sx={{ pt: 1, pl: 2, pr: 3, pb: 1, mt: 1 }}>
<Typography variant="h6" sx={{ mb: 2 }}>Other goals</Typography>
{goals.slice(1).map((goal, index) => <Paper><Goal key={index} goal={goal} /></Paper>)}
</Paper>}
</Box>
)
const hasError = typeof errors === "object" && errors.length > 0
const hasGoal = typeof goals === "object" && goals.length > 0
const hasManyGoal = hasGoal && goals.length > 1
var col = ""
var msg = ""
if (hasError) {
const m = errors[0].match(errorRegex)
if (m) {
col = `Column ${m.groups.col}: `
msg = m.groups.msg
} else {
msg = errors[0]
if (msg === "Unrecognized tactic") { msg = "Unknown spell!" }
}
}
return (
<Box sx={{ height: "100%" }}>
{hasGoal && <Paper sx={{ pt: 1, pl: 2, pr: 3, pb: 1, height: "100%" }}><Typography variant="h5">Current goal</Typography> <Goal goal={goals[0]} /></Paper>}
{completed && <Typography variant="h6">Level completed ! 🎉</Typography>}
{hasError && <Paper sx={{ pt: 1, pl: 2, pr: 3, pb: 1, height: "100%" }}><Typography variant="h5" color="error">Spell invocation failed</Typography>
<Typography sx={{ my: 1 }}>{lastTactic}</Typography>
<Typography component="pre" sx={{ my: 1 }}>{col}{msg}</Typography>
<Typography>Use the undo button to go back to a sane state.</Typography>
</Paper>}
{hasManyGoal && <Paper sx={{ pt: 1, pl: 2, pr: 3, pb: 1, mt: 1 }}>
<Typography variant="h6" sx={{ mb: 2 }}>Other goals</Typography>
{goals.slice(1).map((goal, index) => <Paper><Goal key={index} goal={goal} /></Paper>)}
</Paper>}
</Box>
)
}
export default TacticState
export default TacticState

72
client/src/components/Welcome.tsx
Unescape Escape View File

@ -13,53 +13,53 @@ import { Box, Typography, Button, CircularProgress, Grid } from '@mui/material';
interface WelcomeProps {
rpcConnection: null|rpc.MessageConnection;
setNbLevels: any;
setTitle: any;
startGame: any;
setConclusion: any;
setTitle: any;
startGame: any;
setConclusion: any;
}
type infoResultType = {
title: string,
nb_levels: any[],
conclusion: string
title: string,
nb_levels: any[],
conclusion: string
}
const infoRequestType = new rpc.RequestType0<infoResultType, void>("info")
function Welcome({ rpcConnection, setNbLevels, setTitle, startGame, setConclusion }: WelcomeProps) {
const [leanData, setLeanData] = useState<null|infoResultType>(null)
const [leanData, setLeanData] = useState<null|infoResultType>(null)
useEffect(() => {
if (rpcConnection) { // Will run in the beginning as soon as RPC connection is established
rpcConnection.sendRequest(infoRequestType).then((res: infoResultType) =>{
setLeanData(res)
setNbLevels(res.nb_levels)
setTitle(res.title)
document.title = res.title
setConclusion(res.conclusion)
});
}
}, [rpcConnection, setLeanData, setNbLevels, setTitle, setConclusion])
useEffect(() => {
if (rpcConnection) { // Will run in the beginning as soon as RPC connection is established
rpcConnection.sendRequest(infoRequestType).then((res: infoResultType) =>{
setLeanData(res)
setNbLevels(res.nb_levels)
setTitle(res.title)
document.title = res.title
setConclusion(res.conclusion)
});
}
}, [rpcConnection, setLeanData, setNbLevels, setTitle, setConclusion])
let content
if (leanData) {
content = (<Box sx={{ m: 3 }}>
<Typography variant="body1" component="div">
<MathJax>
<ReactMarkdown>{leanData["introduction"]}</ReactMarkdown>
</MathJax>
</Typography>
<Box textAlign='center' sx={{ m: 5 }}>
<Button onClick={startGame} variant="contained">Start rescue mission</Button>
</Box>
</Box>)
} else {
content = <Box display="flex" alignItems="center" justifyContent="center" sx={{ height: "calc(100vh - 64px)" }}><CircularProgress /></Box>
}
return <Grid container direction="row" justifyContent="center" alignItems="center">
<Grid item xs={12} sm={6}>{content}</Grid>
</Grid>
let content
if (leanData) {
content = (<Box sx={{ m: 3 }}>
<Typography variant="body1" component="div">
<MathJax>
<ReactMarkdown>{leanData["introduction"]}</ReactMarkdown>
</MathJax>
</Typography>
<Box textAlign='center' sx={{ m: 5 }}>
<Button onClick={startGame} variant="contained">Start rescue mission</Button>
</Box>
</Box>)
} else {
content = <Box display="flex" alignItems="center" justifyContent="center" sx={{ height: "calc(100vh - 64px)" }}><CircularProgress /></Box>
}
return <Grid container direction="row" justifyContent="center" alignItems="center">
<Grid item xs={12} sm={6}>{content}</Grid>
</Grid>
}
export default Welcome

Write Preview
Loading…
Cancel
Save