dojo: add tab completion

This is initial support for type-aware tab completion.  When you hit tab, it tries to complete the word you're in the middle of using a face or arm in the subject at that point in the code.  It also shows all possible matches and their associated types.  It's nearly instantaneous.  Notes:

- It advances to the longest common prefix, so if you hit tab on `ab` and the only possible results are `abcde` and `abcdz`, then it'll write `abcd` and print both out (with their types).

- If there are fewer than ten matches, it prints the type along with the face.  Printing types is too slow to use all the time, but with 10 it's essentially instantaneous.

- The match closest in the subject to you (i.e. smallest axis number) is displayed lowest (closest to your focus).

Examples below, where `<TAB>` represents me hitting tab while my cursor is at that position (the line with the `<TAB>` is not preserved in the actual output).

```
~zod:dojo> eth<TAB>
-----
ethereum        #t/<11.qcl {<3.ltb 27.ipf 7.ecf 36.uek 92.bjk 247.ows 51.mvt 126.xjf 41.mac 1.ane $141> <21.yeb 27.ipf 7.ecf 36.uek 92.bjk 247.ows 51.mvt 126.xjf 41.mac 1.ane $141>}>
ethereum-types  #t/<3.ltb 27.ipf 7.ecf 36.uek 92.bjk 247.ows 51.mvt 126.xjf 41.mac 1.ane $141>
~zod:dojo> ethereum
~zod:dojo> |=  zong=@ud  z<TAB>
-----
zing  #t/<1.dqs {* <126.xjf 41.mac 1.ane $141>}>
zap   #t/<1.iot {tub/{p/{p/@ud q/@ud} q/""} <1.rff {daf/@t <247.ows 51.mvt 126.xjf 41.mac 1.ane $141>}>}>
zuse  #t/$309
zong  #t/@ud
~zod:dojo> |=  zong=@ud  zo<TAB>
-----
zong  #t/@ud
~zod:dojo> |=  zong=@ud  zong
~zod:dojo> <TAB>
hoon-version
trel
quip
pole
unit
qual
lone
... about 600 more lines ...
unity
html
zuse
eny
now
our
~zod:dojo>
```

Functionally, this is in a state where I'd be comfortable shipping it.  It doesn't interfere with anything if you don't press tab, and it's perfectly OTA-able.  I do think its output is a little verbose, but that can be tuned over time as people try it and determine what feels good in practice.

Additional notes:

- There are plenty of similar systems for other languages, but my most direct inspiration is Idris's editor tools.  This is implemented for the dojo, but I actually want it in my editor, which is why the meat is all defind in a library.  I've only tested on dojo one-liners, so I don't know the performance on large blocks of code.

- The default type printer isn't great for this use case.  In particular,
	- Cores should not print anything about their context
  - The `#t/` should go away
  - If it looks like a gate, we should print its return value
  - Maybe special handling for molds, but if the above is done, then for example `bone` is  `* -> @ud`.

- The worst part about our wing ordering is that it really screws up tab completion.  You want to do `point.owner-address` instead of `owner-address.point` because that lets you type `point.ow<TAB>`.  I weakly prefer reading it how we do it now, but it's really not great.  You could do an (dojo-specific?) alternate syntax of `point;owner-address`; this is a simple transformation.

- Regardless of the above, this should handle the case where we're in the middle of defining a wing; it doesn't right now.

- When a variable is shadowed, we show both of them.  We should probably show the shadowed one with a `^`.

- We probably shouldn't print out hundreds of results.  Maybe just the closest 50 with ellipses.

- This gets you any face in your subject, regardless of whether its type is reasonable.  We could limit that some by copying the `gol` logic in mint, so that if the pseudo-backward-inference engine happens to know what type it should be, you can filter the tab results according to if they nest in that type.  This would be "strongly type-aware".
This commit is contained in:
Philip Monk 2019-10-30 20:39:02 -07:00
parent e77237d1a1
commit 76b917f426
No known key found for this signature in database
GPG Key ID: B66E1F02604E44EC
6 changed files with 342 additions and 25 deletions

View File

@ -301,6 +301,7 @@
%det (edit +.act)
%clr [~ this]
%ret obey
%tab [~ this]
==
:: +edit: apply sole edit
::

View File

@ -3,7 +3,7 @@
:: :: ::
/? 309 :: arvo kelvin
/- *sole, lens ::
/+ sole, pprint ::
/+ sole, pprint, auto ::
:: :: ::
:::: :: ::::
:: :: ::
@ -678,6 +678,7 @@
$det (dy-edit +.act)
$ret (dy-done (tufa buf.say))
$clr dy-stop
$tab +>+>
==
::
++ dy-cage |=(num/@ud (~(got by rez) num)) :: known cage
@ -724,23 +725,6 @@
:+ %$ %noun
?~(b !>([~ ~]) (dy-vase p.u.b))
::
++ dy-hoon-head :: dynamic state
:: todo: how do i separate the toplevel 'dojo state' comment?
:: dojo state
::
:: our: the name of this urbit
:: now: the current time
:: eny: a piece of random entropy
::
^- cage
:- %noun
=+ sloop=|=({a/vase b/vase} ?:(=(*vase a) b ?:(=(*vase b) a (slop a b))))
%+ sloop
%- ~(rep by var)
|= {{a/term @ b/vase} c/vase} ^- vase
(sloop b(p face+[a p.b]) c)
!>([our=our now=now eny=eny]:hid)
::
++ dy-made-dial :: dialog product
|= cag/cage
^+ +>+>
@ -814,7 +798,7 @@
=+ too=(dy-hoon-mark gen)
=- ?~(too - [%cast he-disc u.too -])
:+ %ride gen
:- [%$ dy-hoon-head]
:- [%$ he-hoon-head]
:^ %plan he-rail `coin`blob+**
`scaffold:ford`[he-rail zuse sur lib ~ ~]
::
@ -1112,6 +1096,76 @@
==
==
::
++ he-tab
|= pos=@ud
^+ +>
=* res +>
=/ buf (tufa buf.say)
:: Find beg-pos by searching backward to where the current term
:: begins
=+ ^- [id=(unit term) *]
(scan `tape`(flop (scag pos buf)) ;~(plug (punt sym) (star prn)))
=/ beg-pos
?~ id
pos
(sub pos (met 3 u.id))
=/ txt=tape
;: weld
(scag beg-pos buf)
"magic-spoon"
?~ id
""
"."
(slag beg-pos buf)
"\0a"
==
=+ vex=((full parse-command-line:he-parser) [1 1] txt)
?. ?=([* ~ [* @ %ex *] *] vex)
res
=/ typ p:(slop q:he-hoon-head !>(..dawn))
=/ tl (tablist:auto typ p.q.q.p.u.q.vex)
=/ advance (autoadvance:auto typ p.q.q.p.u.q.vex)
=? res ?=(^ advance)
=/ to-send (trip (rsh 3 (sub pos beg-pos) u.advance))
=| fxs=(list sole-effect)
|- ^+ res
?~ to-send
(he-diff %mor (flop fxs))
=^ lic say (~(transmit sole say) %ins pos `@c`i.to-send)
$(to-send t.to-send, fxs [`sole-effect`det+lic fxs], pos +(pos))
:: If couldn't search (eg cursor not in appropriate position), do
:: nothing.
::
?: ?=(~ tl)
res
:: If no options, ring the bell
::
?: =([~ ~] tl)
(he-diff %bel ~)
:: If only one option, don't print unless the option is already
:: typed in.
::
?: &(?=([* ~] u.tl) !=((met 3 (need advance)) (sub pos beg-pos)))
res
:: Else, print results
::
=+ =/ lots (gth (lent u.tl) 10)
=/ long
?: lots
0
(roll (turn u.tl |=([=term *] (met 3 term))) max)
%- (slog leaf/"-----" ~)
%+ turn u.tl
|= [=term =type]
?: lots
%- (slog leaf+(trip term) ~)
~
=/ =tape
"{(trip term)} {(trip (fil 3 (sub long (met 3 term)) ' '))} {<type>}"
%- (slog leaf+tape ~)
~
res
::
++ he-type :: apply input
|= act/sole-action
^+ +>
@ -1121,6 +1175,7 @@
$det (he-stir +.act)
$ret (he-done (tufa buf.say))
$clr he-pine(buf "")
$tab (he-tab +.act)
==
::
++ he-lame :: handle error
@ -1130,6 +1185,23 @@
?^ poy
he-pine:~(dy-amok dy u.poy)
he-pine :: XX give mean to original keystroke
::
++ he-hoon-head :: dynamic state
:: todo: how do i separate the toplevel 'dojo state' comment?
:: dojo state
::
:: our: the name of this urbit
:: now: the current time
:: eny: a piece of random entropy
::
^- cage
:- %noun
=+ sloop=|=({a/vase b/vase} ?:(=(*vase a) b ?:(=(*vase b) a (slop a b))))
%+ sloop
%- ~(rep by var)
|= {{a/term @ b/vase} c/vase} ^- vase
(sloop b(p face+[a p.b]) c)
!>([our=our now=now eny=eny]:hid)
--
::
++ prep

View File

@ -658,6 +658,7 @@
$det (sh-edit +.act)
$clr ..sh-sole :: (sh-pact ~) :: XX clear to PM-to-self?
$ret sh-obey
$tab ..sh-sole
==
::
++ sh-edit

238
pkg/arvo/lib/auto.hoon Normal file
View File

@ -0,0 +1,238 @@
:: Autocompletion for hoon.
::
|%
+$ ids (list [=term =type])
++ get-identifiers
|= ty=type
%- flop
|- ^- ids
?- ty
%noun ~
%void ~
[%atom *] ~
[%cell *]
%+ weld
$(ty p.ty)
$(ty q.ty)
::
[%core *]
%- weld
:_ $(ty p.ty)
^- (list (pair term type))
%- zing
%+ turn ~(tap by q.r.q.ty)
|= [term =tome]
%+ turn
~(tap by q.tome)
|= [name=term =hoon]
^- (pair term type)
~| term=term
[name ~(play ~(et ut ty) ~[name] ~)]
::
[%face *]
?^ p.ty
~
[p.ty q.ty]~
::
[%fork *]
~| %find-fork
!! :: eh, fuse?
::
[%hint *] $(ty q.ty)
[%hold *] $(ty ~(repo ut ty))
==
::
++ search-prefix
|= [sid=term =ids]
^- (list [term type])
%+ skim ids
|= [id=term ty=type]
=(sid (end 3 (met 3 sid) id))
::
++ longest-match
|= matches=(list [=term =type])
^- term
?~ matches
''
=/ n 1
=/ last (met 3 term.i.matches)
|- ^- term
?: (gth n last)
term.i.matches
=/ prefix (end 3 n term.i.matches)
?: |- ^- ?
?| ?=(~ t.matches)
?& =(prefix (end 3 n term.i.t.matches))
$(t.matches t.t.matches)
== ==
$(n +(n))
(end 3 (dec n) term.i.matches)
::
++ find-type-mule
|= [sut=type gen=hoon]
^- (unit [term type])
=/ res (mule |.((find-type sut gen)))
?- -.res
%& p.res
%| ((slog (flop (scag 1 p.res))) ~)
==
::
:: Get the subject type of the wing where you've put the "magic-spoon".
::
++ find-type
|= [sut=type gen=hoon]
=* loop $
|^
^- (unit [term type])
?- gen
[%cnts [%magic-spoon ~] *] `['' sut]
[%cnts [%magic-spoon @ ~] *] `[i.t.p.gen sut]
[^ *] (both p.gen q.gen)
[%ktcn *] loop(gen p.gen)
[%brcn *] (grow q.gen)
[%brvt *] (grow q.gen)
[%cnts *]
|- ^- (unit [term type])
=* inner-loop $
?~ q.gen
~
%+ replace
loop(gen q.i.q.gen)
|. inner-loop(q.gen t.q.gen)
::
[%dtkt *] (spec-and-hoon p.gen q.gen)
[%dtls *] loop(gen p.gen)
[%rock *] ~
[%sand *] ~
[%tune *] ~
[%dttr *] (both p.gen q.gen)
[%dtts *] (both p.gen q.gen)
[%dtwt *] loop(gen p.gen)
[%hand *] ~
[%ktbr *] loop(gen p.gen)
[%ktls *] (both p.gen q.gen)
[%ktpd *] loop(gen p.gen)
[%ktsg *] loop(gen p.gen)
[%ktwt *] loop(gen p.gen)
[%note *] loop(gen q.gen)
[%sgzp *] (both p.gen q.gen)
[%sgbn *] loop(gen q.gen) :: should check for hoon in p.gen
[%tsbn *] (change p.gen q.gen)
[%tscm *]
%+ replace
loop(gen p.gen)
|.(loop(gen q.gen, sut (~(busk ut sut) p.gen)))
::
[%wtcl *] (bell p.gen q.gen r.gen)
[%fits *] (both p.gen wing+q.gen)
[%wthx *] loop(gen wing+q.gen)
[%dbug *] loop(gen q.gen)
[%zpcm *] (both p.gen q.gen)
[%lost *] loop(gen p.gen)
[%zpmc *] (both p.gen q.gen)
[%zpts *] loop(gen p.gen)
[%zpvt *] !!
[%zpzp *] ~
*
=+ doz=~(open ap gen)
?: =(doz gen)
~_ (show [%c 'hoon'] [%q gen])
~> %mean.'play-open'
!!
loop(gen doz)
==
::
++ replace
|= [a=(unit [term type]) b=(trap (unit [term type]))]
^- (unit [term type])
?~(a $:b a)
::
++ both
|= [a=hoon b=hoon]
(replace loop(gen a) |.(loop(gen b)))
::
++ bell
|= [a=hoon b=hoon c=hoon]
(replace loop(gen a) |.((replace loop(gen b) |.(loop(gen c)))))
::
++ spec-and-hoon
|= [a=spec b=hoon]
(replace (find-type-in-spec sut a) |.(loop(gen b)))
::
++ change
|= [a=hoon b=hoon]
(replace loop(gen a) |.(loop(gen b, sut (~(play ut sut) a))))
::
++ grow
|= m=(map term tome)
=/ tomes ~(tap by m)
|- ^- (unit [term type])
=* outer-loop $
?~ tomes
~
=/ arms ~(tap by q.q.i.tomes)
|- ^- (unit [term type])
=* inner-loop $
?~ arms
outer-loop(tomes t.tomes)
%+ replace
loop(gen q.i.arms, sut (~(play ut sut) gen))
|. inner-loop(arms t.arms)
--
::
:: Not implemented yet. I wonder whether we should modify types found
:: in spec mode such that if it's a mold that produces a type, it
:: should just display the type and not that it's technically a
:: function.
::
++ find-type-in-spec
|= [sut=type pec=spec]
^- (unit [term type])
!!
::
++ replace-hax
|= code=tape
%+ scan code
%+ cook
|= res=(list $@(@ [~ (unit term)]))
%- trip
%- crip
%+ turn res
|= elem=$@(@ [~ (unit term)])
?@ elem
elem
?~ +.elem
'magic-spoon'
(cat 3 'magic-spoon.' u.+.elem)
%- star
;~ pose
;~ less
hax
prn
==
::
(stag ~ ;~(pfix hax (punt sym)))
==
::
++ autoadvance
|= [sut=type gen=hoon]
%+ bind (find-type-mule sut gen)
|= [id=term typ=type]
(longest-match (search-prefix id (get-identifiers typ)))
::
++ auto-advance
|= [sut=type code=cord]
(autoadvance sut (scan (replace-hax (trip code)) vest))
::
++ tablist
|= [sut=type gen=hoon]
%+ bind (find-type-mule sut gen)
|= [id=term typ=type]
(search-prefix id (get-identifiers typ))
::
++ tab-list
|= [sut=type code=cord]
%+ bind (find-type sut (scan (replace-hax (trip code)) vest))
|= [id=term typ=type]
(search-prefix id (get-identifiers typ))
--

View File

@ -589,6 +589,7 @@
$f (ta-aro %r)
$g ?~ ris ta-bel
(ta-hom(pos.hit num.hit, ris ~) [%set ~])
$i ta-tab
$k =+ len=(lent buf.say.inp)
?: =(pos.inp len)
ta-bel
@ -856,6 +857,9 @@
++ ta-ret :: hear return
(ta-act %ret ~)
::
++ ta-tab :: hear tab
(ta-act %tab pos.inp)
::
++ ta-ser :: reverse search
|= ext/(list @c)
^+ +>

View File

@ -6,8 +6,9 @@
++ sole-action :: sole to app
$% :: {$abo ~} :: reset interaction
{$det sole-change} :: command line edit
{$ret ~} :: submit and clear
{$clr ~} :: exit context
{$ret ~} :: submit and clear
{$clr ~} :: exit context
{$tab pos=@ud} :: tab complete
== ::
++ sole-buffer (list @c) :: command state
++ sole-change :: network change
@ -20,18 +21,18 @@
$% {$del p/@ud} :: delete one at
{$ins p/@ud q/@c} :: insert at
{$mor p/(list sole-edit)} :: combination
{$nop ~} :: no-op
{$nop ~} :: no-op
{$set p/sole-buffer} :: discontinuity
== ::
++ sole-effect :: app to sole
$% {$bel ~} :: beep
$% {$bel ~} :: beep
{$blk p/@ud q/@c} :: blink+match char at
{$clr ~} :: clear screen
{$clr ~} :: clear screen
{$det sole-change} :: edit command
{$err p/@ud} :: error point
{$klr p/styx} :: styled text line
{$mor p/(list sole-effect)} :: multiple effects
{$nex ~} :: save clear command
{$nex ~} :: save clear command
{$pro sole-prompt} :: set prompt
{$sag p/path q/*} :: save to jamfile
{$sav p/path q/@} :: save to file