Skip to content

Commit

Permalink
Case splitting
Browse files Browse the repository at this point in the history
  • Loading branch information
@donald-pinckney
donald-pinckney committed May 22, 2019
1 parent a593a91 commit 6668d1c
Show file tree
Hide file tree
Showing 5 changed files with 163 additions and 34 deletions.
2 changes: 1 addition & 1 deletion _drafts/idris-testing.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@ axiom3 : (x : PNat) -> (N x) = O -> Void
axiom3 _ Refl impossible
axiom4 : Nat -> Nat
axiom4 x = if True then x else x
axiom4 x = ?easdfasdf
```

No path:
Expand Down
35 changes: 32 additions & 3 deletions nonsite/deps/idris-runner/function/file-processing.js
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,16 @@ function processUploads(uploads, tmpdir, command, callback) {
idrisCommand = `${command.file}`;
replCommand = `:t ${command.expr}`;
}
} else if (command.action == "addclause") {
if(command.file !== undefined && command.f !== undefined && command.n !== undefined) {
idrisCommand = `${command.file}`;
replCommand = `:ac ${command.n} ${command.f}`;
}
} else if (command.action == "casesplit") {
if(command.file !== undefined && command.x !== undefined && command.n !== undefined) {
idrisCommand = `${command.file}`;
replCommand = `:cs ${command.n} ${command.x}`;
}
}

if(idrisCommand === null) {
Expand All @@ -39,9 +49,28 @@ function processUploads(uploads, tmpdir, command, callback) {
exec(cmd, function(error, stdout, stderr) {
// command output is in stdout
// res.status(200).send(stdout);
var res = {
idrisOutput: stdout
};
stdout = stdout.trim();
let numLines = stdout.split("\n").length;

if(command.action == "addclause" && numLines == 1) {
var res = {
displayAction: "insert",
toInsert: stdout,
line: command.n
};
} else if(command.action == "casesplit") {
var res = {
displayAction: "replace",
toReplace: stdout,
line: command.n
};
} else {
var res = {
displayAction: "showtext",
text: stdout
};
}

callback(JSON.stringify(res));
});

Expand Down
1 change: 0 additions & 1 deletion nonsite/deps/idris-runner/function/test_bad.idr
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,6 @@
module Main

test : List Nat -> List Nat
test xs = map (\x => x + 3) xs

test_main : List Nat
test_main = test [4, 3, "cat"]
8 changes: 4 additions & 4 deletions nonsite/deps/idris-runner/function/test_p.idr
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ module Main
test : List Nat -> List Nat
test xs = map (\x => x + 3) xs

test_main : List Nat
test_main = test [4, 3, 8]
test_main : List Nat -> List Nat
test_main xs = ?test_main_rhs

main : IO ()
main = putStrLn (show test_main)
-- main : IO ()
-- main = putStrLn (show test_main)
151 changes: 126 additions & 25 deletions public/js/code-snippets.js
View file
Original file line number Diff line number Diff line change
Expand Up @@ -204,39 +204,98 @@ function playpen_get_lang(playpen) {


function get_idris_token(editor) {
let sess = editor.getSession();
let cursor = editor.getCursorPosition();
let token = editor.getSession().getTokenAt(cursor.row, cursor.column);
if(token.type == "entity.name.function.idris"
|| token.type == "support.constant.prelude.idris"
|| token.type == "support.type.prelude.idris"
|| token.type == "text"
|| token.type == "meta.parameter.named.idris"
|| token.type == "meta.function.type-signature.idris"
|| token.type == "constant.language.bottom.idris") {
return token.value.trim();
} else {
return null;
let line = sess.getLine(cursor.row);

function isLeftWord(c) {
return (65 <= c && c <= 90) // A-Z
|| (97 <= c && c <= 122) // a-z
|| (48 <= c && c <= 57) // 0-9
|| c == 95; // _
}
function isRightWord(c) {
return isLeftWord(c);
}

// var start = Math.max(cursor.column - 1, 0);
var start = cursor.column;
while (start > 0 && isLeftWord(line.charCodeAt(start-1))) {
start--;
}

var endInc = cursor.column - 1;
while (endInc < line.length - 1 && isRightWord(line.charCodeAt(endInc+1))) {
endInc++;
}

let tok = line.substring(start, endInc + 1);
// alert(`"${tok}"`);

return tok;

// let token = editor.getSession().getTokenAt(cursor.row, cursor.column);
// if(token.type == "entity.name.function.idris"
// || token.type == "support.constant.prelude.idris"
// || token.type == "support.type.prelude.idris"
// || token.type == "text"
// || token.type == "meta.parameter.named.idris"
// || token.type == "meta.function.type-signature.idris"
// || token.type == "constant.language.bottom.idris") {
// return token.value.trim();
// } else {
// return null;
// }
}

// var res = {
// displayAction: "showtext",
// text: stdout
// };
// } else {
// var res = {
// displayAction: "insert",
// toInsert: stdout,
// line: command.n
// };

function handle_idris_result(code_block, result_block, editor, result) {
if(result == null || result.displayAction == null) {
result_block.innerText = "Communication error.";
return;
}

function handle_idris_result(code_block, result_block, result) {
if(result == null || result.idrisOutput == null || result.idrisOutput == "") {
// result_block.style.display = 'none';
result_block.innerText = 'No type errors.';
if(result.displayAction == "insert") {
let sess = editor.getSession();
sess.insert({row: result.line, column: 0}, result.toInsert);

result_block.style.display = 'none';
} else if(result.displayAction == "replace") {
let sess = editor.getSession();
let line = sess.getLine(result.line - 1);
let replaceRange = new ace.Range(result.line - 1, 0, result.line - 1, line.length);
sess.replace(replaceRange, result.toReplace);

result_block.style.display = 'none';
} else if(result.displayAction == "showtext") {
if(result.text == null || result.text == "") {
result_block.innerText = 'No type errors.';
} else {
result_block.innerText = result.text;
}
} else {
result_block.innerText = result.idrisOutput;
result_block.innerText = "Unknown display action: " + result.displayAction;
}
}

function idris_action(code_block, editor, actionFn) {
function idris_action(code_block, editor, waiting_text, actionFn) {
var result_block = get_result_block(code_block);

// result_block.style.display = 'block';
result_block.innerText = "Typechecking...";
result_block.style.display = 'block';
result_block.innerText = waiting_text;

actionFn(code_block, editor)
.then(result => handle_idris_result(code_block, result_block, result))
.then(result => handle_idris_result(code_block, result_block, editor, result))
.catch(error => result_block.innerText = "Playground Communication: " + error.message);
}

Expand Down Expand Up @@ -269,6 +328,32 @@ function playpen_get_lang(playpen) {
return run_idris_files(files, {action: "typeof", file: pkg.activeFilename, expr: token});
}

function idris_add_def(block, editor) {
let pkg = package_idris_files(block);
let files = pkg.files;

let token = get_idris_token(editor);
if(token == null) {
return;
}

let lineNumber = editor.getCursorPosition().row + 1;
return run_idris_files(files, {action: "addclause", file: pkg.activeFilename, n: lineNumber, f: token});
}

function idris_case_split(block, editor) {
let pkg = package_idris_files(block);
let files = pkg.files;

let token = get_idris_token(editor);
if(token == null) {
return;
}

let lineNumber = editor.getCursorPosition().row + 1;
return run_idris_files(files, {action: "casesplit", file: pkg.activeFilename, n: lineNumber, x: token});
}




Expand All @@ -282,7 +367,7 @@ function playpen_get_lang(playpen) {
var runFunc = language_dispatch_table[lang];
if(lang == "language-idris") {
let editor = get_editor(code_block);
idris_action(editor.container.parentNode, editor, idris_typecheck);
idris_action(editor.container.parentNode, editor, "Typechecking...", idris_typecheck);
} else if(runFunc !== undefined) {
runFunc(code_block)
.then(result => result_block.innerText = result)
Expand All @@ -297,8 +382,7 @@ function playpen_get_lang(playpen) {
name: 'typecheck',
bindKey: {win: 'Ctrl-Alt-R', mac: 'Ctrl-Alt-R'},
exec: function(editor) {
idris_action(editor.container.parentNode, editor, idris_typecheck);
// idris_typecheck(editor.container.parentNode, editor);
idris_action(editor.container.parentNode, editor, "Typechecking...", idris_typecheck);
},
readOnly: true,
});
Expand All @@ -307,11 +391,28 @@ function playpen_get_lang(playpen) {
name: 'typeof',
bindKey: {win: 'Ctrl-Alt-T', mac: 'Ctrl-Alt-T'},
exec: function(editor) {
idris_action(editor.container.parentNode, editor, idris_typeof);
// idris_typeof(editor.container.parentNode, editor);
idris_action(editor.container.parentNode, editor, "Finding type...", idris_typeof);
},
readOnly: true,
});

editor.commands.addCommand({
name: 'addclause',
bindKey: {win: 'Ctrl-Alt-A', mac: 'Ctrl-Alt-A'},
exec: function(editor) {
idris_action(editor.container.parentNode, editor, "Adding clause...", idris_add_def);
},
readOnly: false,
});

editor.commands.addCommand({
name: 'casesplit',
bindKey: {win: 'Ctrl-Alt-C', mac: 'Ctrl-Alt-C'},
exec: function(editor) {
idris_action(editor.container.parentNode, editor, "Splitting case...", idris_case_split);
},
readOnly: false,
});
}

// Syntax highlighting Configuration
Expand Down

0 comments on commit 6668d1c

Please sign in to comment.