Skip to content
This repository has been archived by the owner on Jun 9, 2021. It is now read-only.

Naming-aware term pretty-printing. #126

Merged
merged 2 commits into from
Jan 22, 2021
Merged

Naming-aware term pretty-printing. #126

merged 2 commits into from
Jan 22, 2021

Conversation

brianhuffman
Copy link
Contributor

Add some new functions for pretty-printing shared terms using information from the SAWNamingEnv to choose best aliases for names.

This PR avoids changing the types or behavior of any existing functions, in order to avoid requiring PRs for five other packages.

@brianhuffman
Copy link
Contributor Author

So far, this lets us avoid some of the redundant qualified names in saw-core pretty printing (#17). This is limited by the fact that only defined saw-core constants are registered in the SAWNamingEnv at the moment, and we are not yet registering axioms, primitives, datatypes, or data constructors.

sawscript> print_term {{ sum [1..10] + 0x23 }}
[23:47:41.877] let { x@1 = Prelude.Vec 8 Prelude.Bool
      x@2 = Cryptol.TCNum 1
      x@3 = Cryptol.TCNum 8
      x@4 = PLiteralSeqBool x@3
      x@5 = PRingSeqBool x@3
      x@6 = Cryptol.TCNum 10
      x@7 = tcAdd x@2 (tcSub x@6 x@2)
    }
 in ecPlus x@1 x@5
      (sum x@6 x@1 (PEqSeqBool x@3) x@5
         (Prelude.coerce (seq x@7 x@1) (Prelude.Vec 10 x@1)
            (seq_cong1 x@7 x@6 x@1
               (Prelude.unsafeAssert Cryptol.Num x@7 x@6))
            (ecFromTo x@2 x@6 x@1 x@4 x@4)))
      (ecNumber (Cryptol.TCNum 35) x@1 x@4)

brianhuffman pushed a commit to GaloisInc/saw-script that referenced this pull request Jan 20, 2021
brianhuffman pushed a commit to GaloisInc/saw-script that referenced this pull request Jan 21, 2021
brianhuffman pushed a commit to GaloisInc/saw-script that referenced this pull request Jan 21, 2021
brianhuffman pushed a commit to GaloisInc/saw-script that referenced this pull request Jan 21, 2021
Brian Huffman added 2 commits January 21, 2021 17:14
- ppTermWithNames :: PPOpts -> SAWNamingEnv -> Term -> SawDoc
- showTermWithNames :: PPOpts -> SAWNamingEnv -> Term -> String
scShowTerm :: SharedContext -> PPOpts -> Term -> IO String
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant