diff --git a/permutations.ml b/permutations.ml index 883e03d..80030f2 100644 --- a/permutations.ml +++ b/permutations.ml @@ -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 diff --git a/proof_transformation.ml b/proof_transformation.ml index 07b9149..e2cda26 100644 --- a/proof_transformation.ml +++ b/proof_transformation.ml @@ -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 diff --git a/static/css/style.css b/static/css/style.css index 7499ef3..1058e2a 100644 --- a/static/css/style.css +++ b/static/css/style.css @@ -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; } diff --git a/static/js/proof.js b/static/js/proof.js index 4ca3148..d61d4e2 100644 --- a/static/js/proof.js +++ b/static/js/proof.js @@ -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) { @@ -121,12 +128,12 @@ function createSubProof(proofAsJson, $subProofDivContainer, options) { } } -function createSequentTable(sequent, options) { +function createSequentTable(sequent, displayPermutation, ancestorList, options) { let $sequentTable = $('') .data('sequentWithoutPermutation', sequent); let $td = $('
'); - $td.append(createSequent(sequent, $sequentTable, options)); + $td.append(createSequent(sequent, displayPermutation, ancestorList, $sequentTable, options)); $sequentTable.append($td); let $tagBox = $('
', {'class': 'tagBox'}) @@ -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); @@ -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 @@ -520,13 +544,7 @@ 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]; } @@ -534,10 +552,10 @@ function getPremisesSequentTable($sequentTable) { 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; } diff --git a/static/js/sequent.js b/static/js/sequent.js index 5b99dd6..45c5763 100644 --- a/static/js/sequent.js +++ b/static/js/sequent.js @@ -32,11 +32,11 @@ const NEUTRAL_ELEMENTS = { // DISPLAY SEQUENT // *************** -function createSequent(sequent, $sequentTable, options) { +function createSequent(sequent, displayPermutation, ancestorList, $sequentTable, options) { let $sequentDiv = $('
', {'class': 'sequent'}); if ('hyp' in sequent) { - createFormulaList(sequent, 'hyp', $sequentDiv, options); + createFormulaList(sequent, displayPermutation, null, 'hyp', $sequentDiv, options); } let $thesisSpan = $('⊢'); @@ -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 = $('', {'class': 'first-point'}); $sequentDiv.append($firstPoint); @@ -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 = $('
  • ') - .data('initialPosition', i) + .data('initialPosition', position) .data('formula', formulaAsJson); + + if (ancestorList !== null) { + $li.data('ancestorPosition', ancestorList[i]); + } + $ul.append($li); // Build formula @@ -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': @@ -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) { @@ -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}); } } @@ -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 // **************