:browse feature request

[weaversa]

In the current :browse, no distinction is made between the public and private members of the currently loaded module. I think it would be nice to see this distinction, specifically to know what functions/properties a module exports.

[brianhuffman]

Good idea. Currently we have properties separated into their own subheading in the :browse output; we could do exactly the same thing with private declarations.

Can we have private property declarations too? Maybe we'd also need another heading for those (if there are any).

[weaversa]

When I write a module I always mark properties as private.

[yav]

I made a pull request that implements this. Basically now each existing section has a nested sub-sections classifying things in various ways (e.g., public/private, imported from somewhere, or defined at the REPL).

The output looks like this:

Cryptol> :l A.cry
Loading module Cryptol
Loading module B
Loading module A
A> :browse 
Type Synonyms
=============

  From Cryptol
  ------------

    type Bool = Bit
    type Char = [8]
    type lg2 n = width (max 1 n - 1)
    type String n = [n][8]
    type Word n = [n]

Constraint Synonyms
===================

  From Cryptol
  ------------

    type constraint i < j = j >= 1 + i
    type constraint i <= j = j >= i
    type constraint i > j = i >= 1 + j

Primitive Types
===============

  From Cryptol
  ------------

    (!=) : # -> # -> Prop
    (==) : # -> # -> Prop
    (>=) : # -> # -> Prop
    (+) : # -> # -> #
    (-) : # -> # -> #
    (%) : # -> # -> #
    (%^) : # -> # -> #
    (*) : # -> # -> #
    (/) : # -> # -> #
    (/^) : # -> # -> #
    (^^) : # -> # -> #
    Arith : * -> Prop
    Bit : *
    Cmp : * -> Prop
    fin : * -> Prop
    Integer : *
    inf : #
    Literal : # -> * -> Prop
    Logic : * -> Prop
    lengthFromThenTo : # -> # -> # -> #
    max : # -> # -> #
    min : # -> # -> #
    SignedCmp : * -> Prop
    width : # -> #
    Z : # -> *
    Zero : * -> Prop

Symbols
=======

  Public
  ------

    x : {a} (Literal 2 a) => a

  From B
  ------

    bb : {a} (Literal 3 a) => a

  From Cryptol
  ------------

    (==>) : Bit -> Bit -> Bit
    (\/) : Bit -> Bit -> Bit
    (/\) : Bit -> Bit -> Bit
    (!=) : {a} (Cmp a) => a -> a -> Bit
    (!==) : {a, b} (Cmp b) => (a -> b) -> (a -> b) -> a -> Bit
    (==) : {a} (Cmp a) => a -> a -> Bit
    (===) : {a, b} (Cmp b) => (a -> b) -> (a -> b) -> a -> Bit
    (<) : {a} (Cmp a) => a -> a -> Bit
    (<$) : {a} (SignedCmp a) => a -> a -> Bit
    (<=) : {a} (Cmp a) => a -> a -> Bit
    (<=$) : {a} (SignedCmp a) => a -> a -> Bit
    (>) : {a} (Cmp a) => a -> a -> Bit
    (>$) : {a} (SignedCmp a) => a -> a -> Bit
    (>=) : {a} (Cmp a) => a -> a -> Bit
    (>=$) : {a} (SignedCmp a) => a -> a -> Bit
    (||) : {a} (Logic a) => a -> a -> a
    (^) : {a} (Logic a) => a -> a -> a
    (&&) : {a} (Logic a) => a -> a -> a
    (#) :
      {front, back, a} (fin front) =>
        [front]a -> [back]a -> [front + back]a
    (<<) : {n, ix, a} (fin ix, Zero a) => [n]a -> [ix] -> [n]a
    (<<<) : {n, ix, a} (fin n, fin ix) => [n]a -> [ix] -> [n]a
    (>>) : {n, ix, a} (fin ix, Zero a) => [n]a -> [ix] -> [n]a
    (>>$) : {n, ix} (fin n, n >= 1, fin ix) => [n] -> [ix] -> [n]
    (>>>) : {n, ix, a} (fin n, fin ix) => [n]a -> [ix] -> [n]a
    (+) : {a} (Arith a) => a -> a -> a
    (-) : {a} (Arith a) => a -> a -> a
    (%) : {a} (Arith a) => a -> a -> a
    (%$) : {a} (Arith a) => a -> a -> a
    (*) : {a} (Arith a) => a -> a -> a
    (/) : {a} (Arith a) => a -> a -> a
    (/$) : {a} (Arith a) => a -> a -> a
    (^^) : {a} (Arith a) => a -> a -> a
    (!) : {n, a, ix} (fin n, fin ix) => [n]a -> [ix] -> a
    (!!) : {n, k, ix, a} (fin n, fin ix) => [n]a -> [k][ix] -> [k]a
    (@) : {n, a, ix} (fin ix) => [n]a -> [ix] -> a
    (@@) : {n, k, ix, a} (fin ix) => [n]a -> [k][ix] -> [k]a
    all : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit
    and : {n} (fin n) => [n] -> Bit
    any : {n, a} (fin n) => (a -> Bit) -> [n]a -> Bit
    carry : {n} (fin n) => [n] -> [n] -> Bit
    complement : {a} (Logic a) => a -> a
    curry : {a, b, c} ((a, b) -> c) -> a -> b -> c
    demote : {val, rep} (Literal val rep) => rep
    drop : {front, back, a} (fin front) => [front + back]a -> [back]a
    elem : {n, a} (fin n, Cmp a) => a -> [n]a -> Bit
    error : {a, len} (fin len) => [len][8] -> a
    False : Bit
    foldl : {n, a, b} (fin n) => (a -> b -> a) -> a -> [n]b -> a
    foldr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> b
    fromInteger : {a} (Arith a) => Integer -> a
    fromThenTo :
      {first, next, last, a, len} (fin first, fin next, fin last,
                                   Literal first a, Literal next a, Literal last a, first != next,
                                   lengthFromThenTo first next last == len) =>
        [len]a
    fromTo :
      {first, last, a} (fin last, last >= first, Literal last a) =>
        [1 + (last - first)]a
    fromZ : {n} (fin n, n >= 1) => Z n -> Integer
    generate :
      {n, ix, a} (fin ix, n >= 1, ix >= width (n - 1)) =>
        ([ix] -> a) -> [n]a
    groupBy :
      {each, parts, a} (fin each) => [each * parts]a -> [parts][each]a
    head : {n, a} [1 + n]a -> a
    infFrom : {a} (Arith a) => a -> [inf]a
    infFromThen : {a} (Arith a) => a -> a -> [inf]a
    iterate : {a} (a -> a) -> a -> [inf]a
    join :
      {parts, each, a} (fin each) => [parts][each]a -> [parts * each]a
    last : {n, a} (fin n) => [1 + n]a -> a
    length : {n, a, b} (fin n, Literal n b) => [n]a -> b
    lg2 : {a} (Arith a) => a -> a
    map : {n, a, b} (a -> b) -> [n]a -> [n]b
    max : {a} (Cmp a) => a -> a -> a
    min : {a} (Cmp a) => a -> a -> a
    negate : {a} (Arith a) => a -> a
    number : {val, rep} (Literal val rep) => rep
    or : {n} (fin n) => [n] -> Bit
    pdiv : {u, v} (fin u, fin v) => [u] -> [v] -> [u]
    pmod : {u, v} (fin u, fin v) => [u] -> [1 + v] -> [v]
    pmult :
      {u, v} (fin u, fin v) => [1 + u] -> [1 + v] -> [1 + (u + v)]
    random : {a} [256] -> a
    repeat : {n, a} a -> [n]a
    reverse : {n, a} (fin n) => [n]a -> [n]a
    sborrow : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
    scanl : {n, b, a} (b -> a -> b) -> b -> [n]a -> [1 + n]b
    scanr : {n, a, b} (fin n) => (a -> b -> b) -> b -> [n]a -> [1 + n]b
    scarry : {n} (fin n, n >= 1) => [n] -> [n] -> Bit
    sext : {m, n} (fin m, m >= n, n >= 1) => [n] -> [m]
    split :
      {parts, each, a} (fin each) => [parts * each]a -> [parts][each]a
    splitAt :
      {front, back, a} (fin front) =>
        [front + back]a -> ([front]a, [back]a)
    sum : {n, a} (fin n, Arith a) => [n]a -> a
    True : Bit
    tail : {n, a} [1 + n]a -> [n]a
    take : {front, back, a} (fin front) => [front + back]a -> [front]a
    toInteger : {bits} (fin bits) => [bits] -> Integer
    trace : {n, a, b} (fin n) => [n][8] -> a -> b -> b
    traceVal : {n, a} (fin n) => [n][8] -> a -> a
    transpose : {rows, cols, a} [rows][cols]a -> [cols][rows]a
    uncurry : {a, b, c} (a -> b -> c) -> (a, b) -> c
    undefined : {a} a
    update : {n, a, ix} (fin ix) => [n]a -> [ix] -> a -> [n]a
    updateEnd : {n, a, ix} (fin n, fin ix) => [n]a -> [ix] -> a -> [n]a
    updates :
      {n, k, ix, a} (fin ix, fin k) => [n]a -> [k][ix] -> [k]a -> [n]a
    updatesEnd :
      {n, k, ix, a} (fin n, fin ix, fin k) =>
        [n]a -> [k][ix] -> [k]a -> [n]a
    zero : {a} (Zero a) => a
    zext : {m, n} (fin m, m >= n) => [n] -> [m]
    zip : {n, a, b} [n]a -> [n]b -> [n](a, b)
    zipWith : {n, a, b, c} (a -> b -> c) -> [n]a -> [n]b -> [n]c

[robdockins]

@yav, can we close this issue?

[yav]

Yep, should be done.

[weaversa]

Thanks @yav !