Skip to content

[WIP] well typed idris protocol #250

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.

Sign up for GitHub

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

Closed
wants to merge 4 commits into from
Closed

[WIP] well typed idris protocol #250

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
42911e8
remplace parsers with typed one
archaeron Jun 1, 2020
17265f8
fixup with parser change
archaeron Jun 1, 2020
54705a8
wip
archaeron Jun 9, 2020
82ff7f2
wip
archaeron Jun 9, 2020
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 .vscode/settings.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
{
"editor.rulers": [80],
"[typescript]": {
"editor.formatOnSave": true
},
Expand Down
28 changes: 0 additions & 28 deletions coffeelint.json
View file
Open in desktop

This file was deleted.

4 changes: 4 additions & 0 deletions jest.config.js
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
module.exports = {
preset: 'ts-jest',
testEnvironment: 'node',
};
8 changes: 5 additions & 3 deletions lib/idris-ide-mode.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,9 +1,9 @@
import Logger from './utils/Logger'
import * as sexpFormatter from './protocol/sexp-formatter'
import * as parse from './utils/parse'
import { EventEmitter } from 'events'
import { spawn, ChildProcessWithoutNullStreams } from 'child_process'
import { SExp } from './protocol/ide-protocol'
import { listP } from './protocol/parser'
import { CompilerOptions } from './utils/ipkg'

export class IdrisIdeMode extends EventEmitter {
Expand Down Expand Up @@ -120,8 +120,10 @@ export class IdrisIdeMode extends EventEmitter {
// Remove the length + command from the buffer
this.buffer = this.buffer.substr(6 + len)
// And then we can try to parse to command..
const obj = parse.parseCommand(cmd.trim())
result.push(this.emit('message', obj))
const typedCommand = listP.parse(cmd.trim())
if (typedCommand.isOk) {
result.push(this.emit('message', typedCommand.value))
}
} else {
// We didn't have the entire command, so let's break the
// while-loop and wait for the next data-event
Expand Down
133 changes: 68 additions & 65 deletions lib/idris-model.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,10 @@ import * as Rx from 'rx-lite'
import * as JS from './utils/js'
import * as path from 'path'
import { CompilerOptions } from './utils/ipkg'
import { IDECommand, SExp } from './protocol/ide-protocol'
import { IDECommand, SExp, SExpList } from './protocol/ide-protocol'
import { ideCommandToSExp } from './protocol/to-sexp'
import Logger from './utils/Logger'
import { fromSExp } from './protocol/from-sexp'

export class IdrisModel {
requestId = 0
Expand Down Expand Up @@ -46,70 +47,72 @@ export class IdrisModel {
this.compilerOptions = options
}

handleCommand(cmd: any) {
if (cmd.length > 0) {
const op = cmd[0],
adjustedLength = Math.max(cmd.length, 2),
params = cmd.slice(1, adjustedLength - 1),
id = cmd[adjustedLength - 1]
if (this.subjects[id] != null) {
const subject = this.subjects[id]
switch (op) {
case ':return':
var ret = params[0]
if (ret[0] === ':ok') {
const okparams = ret[1]
if (okparams[0] === ':metavariable-lemma') {
subject.onNext({
responseType: 'return',
msg: okparams,
})
} else {
subject.onNext({
responseType: 'return',
msg: ret.slice(1),
})
}
} else {
subject.onError({
message: ret[1],
warnings: this.warnings[id],
highlightInformation: ret[2],
cwd: this.compilerOptions.src,
})
}
subject.onCompleted()
return delete this.subjects[id]
case ':write-string':
var msg = params[0]
atom.notifications.addInfo(msg)
return subject.onNext({
responseType: 'write-string',
msg,
})
case ':warning':
var warning = params[0]
return this.warnings[id].push(warning)
case ':run-program':
var options = {
detail:
'The path for the compiled program. It was copied to your clipboard. Paste it into a terminal to execute.',
dismissible: true,
icon: 'comment',
buttons: [{ text: 'Confirm' }],
}
atom.clipboard.write(params[0])
return atom.notifications.addSuccess(params[0], options)
case ':set-prompt':
// Ignore
default: {
Logger.logObject('Unhandled Operator', op)
Logger.logObject('Params', params)
return
}
}
}
}
handleCommand(cmd: SExpList) {
const answer = fromSExp(cmd)
console.log('Answer', answer)
// if (cmd.length > 0) {
// const op = cmd[0],
// adjustedLength = Math.max(cmd.length, 2),
// params = cmd.slice(1, adjustedLength - 1),
// id = cmd[adjustedLength - 1]
// if (this.subjects[id] != null) {
// const subject = this.subjects[id]
// switch (op) {
// case ':return':
// var ret = params[0]
// if (ret[0] === ':ok') {
// const okparams = ret[1]
// if (okparams[0] === ':metavariable-lemma') {
// subject.onNext({
// responseType: 'return',
// msg: okparams,
// })
// } else {
// subject.onNext({
// responseType: 'return',
// msg: ret.slice(1),
// })
// }
// } else {
// subject.onError({
// message: ret[1],
// warnings: this.warnings[id],
// highlightInformation: ret[2],
// cwd: this.compilerOptions.src,
// })
// }
// subject.onCompleted()
// return delete this.subjects[id]
// case ':write-string':
// var msg = params[0]
// atom.notifications.addInfo(msg)
// return subject.onNext({
// responseType: 'write-string',
// msg,
// })
// case ':warning':
// var warning = params[0]
// return this.warnings[id].push(warning)
// case ':run-program':
// var options = {
// detail:
// 'The path for the compiled program. It was copied to your clipboard. Paste it into a terminal to execute.',
// dismissible: true,
// icon: 'comment',
// buttons: [{ text: 'Confirm' }],
// }
// atom.clipboard.write(params[0])
// return atom.notifications.addSuccess(params[0], options)
// case ':set-prompt':
// // Ignore
// default: {
// Logger.logObject('Unhandled Operator', op)
// Logger.logObject('Params', params)
// return
// }
// }
// }
// }
}

getUID(): number {
Expand Down
49 changes: 49 additions & 0 deletions lib/protocol/answers.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,49 @@
import { SExp } from './ide-protocol'

export type ProtocolVersion = {
type: 'protocol-version'
major: number
minor: number
}

export type WithCommandId = { id: number }

export type HighlightSource = {
type: 'highlight-source'
}

export type Premise = {
name: string
type: string
metadata: any
}

export type Conclusion = {
type: string
highlightingInformation: Array<any>
}

export type Hole = {
type: 'hole'
name: string
premises: Array<Premise>
conclusions: Array<Conclusion>
}

export type SuccessCommand = HighlightSource | Hole
export type Success = { type: 'success'; command: SuccessCommand }
export type Error = { type: 'error'; message: string }
export type Result = Success | Error
export type Output = { type: 'output'; result: Result } & WithCommandId
export type Return = { type: 'return'; result: Result } & WithCommandId

export type SetPrompt = { type: 'set-prompt'; prompt: string } & WithCommandId

export type UnknownAnswer = { type: 'unknown'; msg: string; expr: SExp }

export type Answer =
| ProtocolVersion
| Output
| Return
| SetPrompt
| UnknownAnswer
Loading