Skip to content

Highlight ancestors and descendants in transformation mode #164

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

Open
etiennecallies wants to merge 4 commits into
base: master
Choose a base branch
from
Open

Highlight ancestors and descendants in transformation mode #164

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
ed65397
highlight ancestor and descendants in transformation mode. Implements…
etiennecallies Jul 26, 2021
a44986e
use displayPermutation. Fixes #165
etiennecallies Jul 28, 2021
0ed4c87
UI test: underline instead of highlight
etiennecallies Aug 24, 2021
1a5dedb
FIX issue with permutation
etiennecallies Sep 2, 2021
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
6 changes: 6 additions & 0 deletions permutations.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -49,6 +49,12 @@ let perm_minus_element n perm =
let perm_plus_element n perm =
List.concat_map (fun k -> if k = n then [n; n + 1] else if k > n then [k + 1] else [k]) perm

let remove_nth_element n perm =
List.filter (fun k -> k <> n) perm

let duplicate_nth_element n perm =
List.concat_map (fun k -> if k = n then [n; n] else [k]) perm

(* HEAD / TAIL *)

let rec head_tail element = function
Expand Down
41 changes: 36 additions & 5 deletions proof_transformation.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -103,13 +103,44 @@ let can_eliminate_key_case notations = function
| Cut_proof (head, _formula, _tail, p1, p2) -> let enabled, _ = can_cut_key_case (List.length head) 0 notations p1 p2 in enabled
| _ -> false

let identity_head_tail head tail =
identity (List.length head + 1 + List.length tail)

let get_ancestors_lists = function
| Axiom_proof _ -> []
| One_proof -> []
| Top_proof (_, _) -> []
| Bottom_proof (head, tail, _) -> [remove_nth_element (List.length head) (identity_head_tail head tail)]
| Tensor_proof (head, _, _, tail, _, _) ->
let h = List.length head in
let t = List.length tail in
[(identity (h + 1)); List.map (fun n -> n + h) (identity (1 + t))]
| Par_proof (head, _, _, tail, _) -> [duplicate_nth_element (List.length head) (identity_head_tail head tail)]
| With_proof (head, _, _, tail, _, _) -> [identity_head_tail head tail; identity_head_tail head tail]
| Plus_left_proof (head, _, _, tail, _) -> [identity_head_tail head tail]
| Plus_right_proof (head, _, _, tail, _) -> [identity_head_tail head tail]
| Promotion_proof (head_without_whynot, _, tail_without_whynot, _) -> [identity_head_tail head_without_whynot tail_without_whynot]
| Dereliction_proof (head, _, tail, _) -> [identity_head_tail head tail]
| Weakening_proof (head, _, tail, _) -> [remove_nth_element (List.length head) (identity_head_tail head tail)]
| Contraction_proof (head, _, tail, _) -> [duplicate_nth_element (List.length head) (identity_head_tail head tail)]
| Exchange_proof (_, _, permutation, _) -> [permutation_inverse permutation]
| Cut_proof (head, _, tail, _, _) ->
let h = List.length head in
let t = List.length tail in
[(identity h) @ [-1]; [-1] @ List.map (fun n -> n + h) (identity t)]
| Unfold_litt_proof (head, _, tail, _) -> [identity_head_tail head tail]
| Unfold_dual_proof (head, _, tail, _) -> [identity_head_tail head tail]
| Hypothesis_proof _ -> [];;

let get_transform_options_as_json notations not_cyclic proof =
let transform_options = get_transform_options notations not_cyclic proof in
["transformOptions", `List (List.map (fun (transform_option, (enabled, title)) -> `Assoc [
("transformation", `String (Transform_request.to_string transform_option));
("enabled", `Bool enabled);
("title", `String title)
]) transform_options)]
[
"transformOptions", `List (List.map (fun (transform_option, (enabled, title)) -> `Assoc [
("transformation", `String (Transform_request.to_string transform_option));
("enabled", `Bool enabled);
("title", `String title)
]) transform_options);
"ancestorsLists", `List (List.map (fun l -> `List (List.map (fun x -> `Int x) l)) (get_ancestors_lists proof))]

let rec has_cut_that_can_be_eliminated notations not_cyclic proof =
let transform_options = get_transform_options notations not_cyclic proof in
Expand Down
1 change: 1 addition & 0 deletions static/css/style.css
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -76,6 +76,7 @@ input[type=text], .code { background-color: #FFF; font-family: "Courier New", sa
.turnstile.not-auto-provable { color: orange; }
.proof .commaList { display: inline-block; list-style: none; margin: 0; padding: 0; }
.proof .commaList li { display: inline-block; margin-left: 0.2em; }
.proof .commaList li.highlight span.main-formula { border-bottom: solid #66a3e0; }
.proof.proof-transformation li span.cut-formula, .proof.proof-transformation .tagBox.cut, .tagBox.cut .transform { color: #b300b3; }
.tagBox.cut .transform-button.enabled { border-color: #b300b3; }
.tagBox.cut .transform-button.enabled:hover { background-color: #b300b3; }
Expand Down
40 changes: 29 additions & 11 deletions static/js/proof.js
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -95,7 +95,14 @@ function buildProof(proofAsJson, $container) {
}

function createSubProof(proofAsJson, $subProofDivContainer, options) {
let $sequentTable = createSequentTable(proofAsJson.sequent, options);
let displayPermutation = getSequentIdentityPermutation(proofAsJson.sequent);
let ancestorList = proofAsJson.ancestorList;
if (proofAsJson.appliedRule?.ruleRequest?.rule === 'exchange') {
let invertedPermutation = invertPermutation(proofAsJson.appliedRule.ruleRequest.permutation);
displayPermutation = {'hyp': [], 'cons': permute(invertedPermutation, proofAsJson.appliedRule.ruleRequest.displayPermutation)};
ancestorList = ancestorList ? permute(ancestorList, invertedPermutation) : ancestorList;
}
let $sequentTable = createSequentTable(proofAsJson.sequent, displayPermutation, ancestorList || null, options);
$subProofDivContainer.prepend($sequentTable);

if (proofAsJson.appliedRule) {
Expand All @@ -121,12 +128,12 @@ function createSubProof(proofAsJson, $subProofDivContainer, options) {
}
}

function createSequentTable(sequent, options) {
function createSequentTable(sequent, displayPermutation, ancestorList, options) {
let $sequentTable = $('<table>')
.data('sequentWithoutPermutation', sequent);

let $td = $('<td>');
$td.append(createSequent(sequent, $sequentTable, options));
$td.append(createSequent(sequent, displayPermutation, ancestorList, $sequentTable, options));
$sequentTable.append($td);

let $tagBox = $('<div>', {'class': 'tagBox'})
Expand Down Expand Up @@ -276,6 +283,7 @@ function addPremises($sequentTable, proofAsJson, permutationBeforeRule, options)

// Add premises
let premises = proofAsJson.appliedRule.premises;
addPremisesAncestorsLists(premises, proofAsJson.appliedRule['ancestorsLists'] || []);
if (premises.length === 0) {
if (options.withInteraction) {
markParentSequentsAsProved($sequentTable);
Expand All @@ -300,6 +308,22 @@ function addPremises($sequentTable, proofAsJson, permutationBeforeRule, options)
}
}

function addPremisesAncestorsLists(premises, ancestorsLists) {
if (ancestorsLists.length === 0) {
return premises;
}

if (ancestorsLists.length !== premises.length) {
console.error('ancestors and premises do not have same length', ancestorsLists, premises);

return;
}

for (let i = 0; i < premises.length; i++) {
premises[i].ancestorList = ancestorsLists[i];
}
}

function undoRule($sequentTable) {
if (isProved($sequentTable)) {
// Mark all conclusions as provable
Expand Down Expand Up @@ -520,24 +544,18 @@ function getParentSequentTable($sequentTable) {
}

function getPremisesSequentTable($sequentTable) {
let ruleRequest = $sequentTable.data('ruleRequest') || null;
if (ruleRequest === null) {
return [];
}

let $prev = $sequentTable.prev();

if ($prev.prop('tagName') === 'TABLE') {
return [$prev];
}

let $premises = [];
$prev.children('div.sibling').each(function (i, sibling) {
let $siblingTable = $(sibling).children('table').last();
$premises = $premises.concat($siblingTable);
$premises.push($siblingTable);
})

if ($premises.length < 2) {
if ($premises.length === 1) {
// Proof has not been completely set up
return null;
}
Expand Down
74 changes: 66 additions & 8 deletions static/js/sequent.js
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,11 +32,11 @@ const NEUTRAL_ELEMENTS = {
// DISPLAY SEQUENT
// ***************

function createSequent(sequent, $sequentTable, options) {
function createSequent(sequent, displayPermutation, ancestorList, $sequentTable, options) {
let $sequentDiv = $('<div>', {'class': 'sequent'});

if ('hyp' in sequent) {
createFormulaList(sequent, 'hyp', $sequentDiv, options);
createFormulaList(sequent, displayPermutation, null, 'hyp', $sequentDiv, options);
}

let $thesisSpan = $('<span class="turnstile">⊢</span>');
Expand All @@ -51,13 +51,13 @@ function createSequent(sequent, $sequentTable, options) {
$sequentDiv.append($thesisSpan);

if ('cons' in sequent) {
createFormulaList(sequent, 'cons', $sequentDiv, options);
createFormulaList(sequent, displayPermutation, ancestorList, 'cons', $sequentDiv, options);
}

return $sequentDiv;
}

function createFormulaList(sequent, sequentPart, $sequentDiv, options) {
function createFormulaList(sequent, displayPermutation, ancestorList, sequentPart, $sequentDiv, options) {
let $firstPoint = $('<span>', {'class': 'first-point'});
$sequentDiv.append($firstPoint);

Expand All @@ -77,10 +77,16 @@ function createFormulaList(sequent, sequentPart, $sequentDiv, options) {
}

for (let i = 0; i < sequent[sequentPart].length; i++) {
let formulaAsJson = sequent[sequentPart][i];
let position = displayPermutation[sequentPart][i];
let formulaAsJson = sequent[sequentPart][position];
let $li = $('<li>')
.data('initialPosition', i)
.data('initialPosition', position)
.data('formula', formulaAsJson);

if (ancestorList !== null) {
$li.data('ancestorPosition', ancestorList[i]);
}

$ul.append($li);

// Build formula
Expand Down Expand Up @@ -223,7 +229,7 @@ function getRules(formulaAsJson, options) {
default:
return [];
}
} else if (options.proofTransformation.value) {
} else if (options.proofTransformation?.value) {
switch (formulaAsJson.type) {
case 'par':
case 'with':
Expand All @@ -245,6 +251,13 @@ function getRules(formulaAsJson, options) {
}

function addEventsAndStyle($li, formulaAsJson, options) {
if (options.proofTransformation?.value) {
$li.hover(
function () { hoverAncestorsAndDescendents($li, true); },
function () { hoverAncestorsAndDescendents($li, false); }
);
}

let rules = getRules(formulaAsJson, options);

if (rules.length === 0) {
Expand Down Expand Up @@ -302,7 +315,7 @@ function buildApplyRuleCallBack(ruleConfig, $li, options) {

if (options.withInteraction) {
applyRule(ruleRequest, $sequentTable);
} else if (options.proofTransformation.value) {
} else if (options.proofTransformation?.value) {
applyTransformation($sequentTable, {transformation: ruleConfigCopy.transformation, ruleRequest});
}
}
Expand Down Expand Up @@ -436,6 +449,51 @@ function autoProveSequent($sequentTable) {
});
}

// ***************
// HOVER ANCESTORS
// ***************

function hoverAncestorsAndDescendents($li, toggleOn) {
highlight($li, toggleOn);
let $sequentTable = $li.closest('table');
recHoverAncestors($sequentTable, $li.data('ancestorPosition'), toggleOn);
let liPosition = $li.prevAll('li').length;
recHoverDescendents($sequentTable, liPosition, toggleOn)
}

function highlight($li, toggleOn) {
if (toggleOn) {
$li.addClass('highlight');
} else {
$li.removeClass('highlight');
}
}

function recHoverAncestors($sequentTable, ancestorPosition, toggleOn) {
if (ancestorPosition === -1) {
return;
}

let $parentSequentTable = getParentSequentTable($sequentTable);
if ($parentSequentTable !== null) {
let $li = $parentSequentTable.find('li').eq(ancestorPosition);
highlight($li, toggleOn);
recHoverAncestors($parentSequentTable, $li.data('ancestorPosition'), toggleOn);
}
}

function recHoverDescendents($sequentTable, ancestorPosition, toggleOn) {
let $premisesTables = getPremisesSequentTable($sequentTable);
for (let $premiseTable of $premisesTables) {
$premiseTable.find('li').each(function (position, li) {
if ($(li).data('ancestorPosition') === ancestorPosition) {
highlight($(li), toggleOn);
recHoverDescendents($premiseTable, position, toggleOn);
}
});
}
}

// **************
// SEQUENT STATUS
// **************
Expand Down