Skip to content

Conversation

@MaximilianAlgehed
Copy link
Collaborator

@MaximilianAlgehed MaximilianAlgehed commented Sep 4, 2025

A little bit of special casing to make nested projections pretty-print using the provided sel function instead of horrible nesting. Closes #20.

Before:

$> prettyPlan manyInconsistent
Simplified spec:
  constrained $ \ v_7 ->
    let a_5 = ProdFstW (toSimpleRep v_7) in
    let v_4 = ProdFstW (ProdSndW (toSimpleRep v_7)) in
    let v_3 = ProdFstW (ProdSndW (ProdSndW (toSimpleRep v_7))) in
    let v_2 = ProdFstW (ProdSndW (ProdSndW (ProdSndW (toSimpleRep v_7)))) in
    let v_1 =
      ProdFstW (ProdSndW (ProdSndW (ProdSndW (ProdSndW (toSimpleRep v_7))))) in
    let f_0 =
      ProdSndW (ProdSndW (ProdSndW (ProdSndW (ProdSndW (toSimpleRep v_7))))) in
    {assert $ f_0 <. a_5
     assert $ f_0 >. 10
     f_0 <- v_1
     assert $ v_1 >. v_2
     assert $ v_2 >. v_3
     assert $ v_3 >. v_4
     assert $ v_4 >. a_5
     assert $ a_5 <. 10}
SolverPlan
  a_5 :: Int <- TypeSpec [..9] [ ]
  v_4 :: Int <- assert $ v_4 >. a_5
  v_3 :: Int <- assert $ v_3 >. v_4
  v_2 :: Int <- assert $ v_2 >. v_3
  v_1 :: Int <- assert $ v_1 >. v_2
  f_0 :: Int <-
    TypeSpec [11..] [ ]
    ---
    assert $ f_0 <. a_5
  v_7 :: (Int,Int,Int,Int,Int,Int) <-
    assert $ ProdFstW (toSimpleRep v_7) ==. a_5
    assert $ ProdFstW (ProdSndW (toSimpleRep v_7)) ==. v_4
    assert $ ProdFstW (ProdSndW (ProdSndW (toSimpleRep v_7))) ==. v_3
    assert $ ProdFstW (ProdSndW (ProdSndW (ProdSndW (toSimpleRep v_7)))) ==. v_2
    assert $ ProdFstW (ProdSndW (ProdSndW (ProdSndW (ProdSndW (toSimpleRep v_7))))) ==. v_1
    assert $ ProdSndW (ProdSndW (ProdSndW (ProdSndW (ProdSndW (toSimpleRep v_7))))) ==. f_0

after:

$> prettyPlan manyInconsistent
Simplified spec:
  constrained $ \ v_7 ->
    let a_5 = sel @0 v_7 in
    let v_4 = sel @1 v_7 in
    let v_3 = sel @2 v_7 in
    let v_2 = sel @3 v_7 in
    let v_1 = sel @4 v_7 in
    let f_0 = sel @5 v_7 in
    {assert $ f_0 <. a_5
     assert $ f_0 >. 10
     f_0 <- v_1
     assert $ v_1 >. v_2
     assert $ v_2 >. v_3
     assert $ v_3 >. v_4
     assert $ v_4 >. a_5
     assert $ a_5 <. 10}
SolverPlan
  a_5 :: Int <- TypeSpec [..9] [ ]
  v_4 :: Int <- assert $ v_4 >. a_5
  v_3 :: Int <- assert $ v_3 >. v_4
  v_2 :: Int <- assert $ v_2 >. v_3
  v_1 :: Int <- assert $ v_1 >. v_2
  f_0 :: Int <-
    TypeSpec [11..] [ ]
    ---
    assert $ f_0 <. a_5
  v_7 :: (Int,Int,Int,Int,Int,Int) <-
    assert $ sel @0 v_7 ==. a_5
    assert $ sel @1 v_7 ==. v_4
    assert $ sel @2 v_7 ==. v_3
    assert $ sel @3 v_7 ==. v_2
    assert $ sel @4 v_7 ==. v_1
    assert $ sel @5 v_7 ==. f_0

@MaximilianAlgehed MaximilianAlgehed merged commit 588e6cc into master Sep 4, 2025
7 checks passed
@MaximilianAlgehed MaximilianAlgehed deleted the prettyprint-selectors branch September 4, 2025 11:17
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Improve pretty-printing of nested projections on generic types

3 participants