$cone: a definition of type for Nock trees, surjective from hoon $type's with no cores

cone.hoon

=>
|%
+$  cone
  $@  %noun
  $%  [%back ix=@ud]
      [%loop =cone]
      [%cell p=cone q=cone]
      [%face p=term q=cone]
      [%atom =aura]
      [%mote =aura val=@]
      [%'$?' fan=(set [=aura val=@])]
      [%'$@' p=cone q=cone]
      [%'$^' p=cone q=cone]
      [%'$%' fan=(map [=aura val=@] cone)]
  ==
::
+$  aura
  $?  %$   %n   %f
      %da  %dr
      %if  %is  %p
      %c   %t   %ta  %tas
      %u   %uc  %ub  %ud  %ui  %ux  %uv  %uw
      %s   %sc  %sb  %so  %sd  %sx  %sv  %sw
  ==
+$  vest  [p=cone q=*]
--
|%
++  to-aura
  |=  a=@tas
  ^-  aura
  ;;(aura a)  ::  TODO: truncate
::
++  type-to-cone
  =|  holds=(list [=type =hoon])
  |=  typ=type
  =*  outer-loop  $
  ^-  cone
  ?-  typ
      %noun  typ
      %void  !!
      [%atom *]
    ?~  q.typ
      [%atom (to-aura p.typ)]
    [%mote (to-aura p.typ) u.q.typ]
  ::
      [%cell *]  [%cell $(typ p.typ) $(typ q.typ)]
      [%core *]  !!
      [%face *]  ?^(p.typ !! [%face p.typ $(typ q.typ)])
      [%fork *]
    |^  ^-  cone
    ?:  are-all-atoms
      make-bucpat
    ?.  are-all-cells
      make-bucpat
    ?:  are-all-heads-motes
      make-buccen
    make-bucket
    ::
    ++  fork-loop  $
    ::
    ++  are-all-atoms
      ^-  ?
      !(~(any in p.typ) nests-in-cell)
    ::
    ++  are-all-cells
      ^-  ?
      (~(all in p.typ) nests-in-cell)
    ::
    ++  nests-in-cell
      |=  tep=type
      ^-  ?
      (~(nest ut -:!>(*^)) | tep)
    ::
    ++  are-all-heads-motes
      ^-  ?
      %-  ~(all in p.typ)
      |=  t=type 
      ^-  ?
      =/  hed=type  (~(peek ut t) %free 2)
      .=  [%& %&]
      %-  mule
      |.  ^-  ?
      ?:  ?=([%atom @ ~ @] hed)
        &
      $(hed ~(repo ut hed))
    ::
    ++  make-bucwut
      ^-  cone
      :-  %'$?'
      %-  ~(run in p.typ)
      |=  tep=type
      ^-  [aura @]
      ?:  ?=([%atom *] tep)
        [(to-aura p.tep) (need q.tep)]
      $(tep ~(repo ut tep))
    ::
    ++  make-bucpat
      ^-  cone
      =/  [cells=(list type) atoms=(list type)]
        (skid ~(tap in p.typ) nests-in-cell)
      :+  %'$@'
        ?:  ?=([* ~] atoms)
          outer-loop(typ i.atoms)
        make-bucwut(p.typ (~(gas in *(set type)) atoms))
      ?:  ?=([* ~] cells)
        outer-loop(typ i.cells)
      fork-loop(p.typ (~(gas in *(set type)) cells))
    ::
    ++  make-buccen
      ^-  cone
      :-  %'$%'
      %-  ~(gas by *(map [aura @] cone))
      %+  turn  ~(tap in p.typ)
      |=  tep=type
      ^-  [[aura @] cone]
      =/  hed=type  (~(peek ut tep) %free 2)
      =/  tal=type  (~(peek ut tep) %free 3)
      =/  tag=[aura @]
        ~|  %buccen-head-not-mote
        |-  ^-  [aura @]
        ?:  ?=([%atom @ ~ @] hed)
          [(to-aura p.hed) u.q.hed]
        $(hed ~(repo ut hed))
      [tag outer-loop(typ tal)]
    ::
    ++  make-bucket
      ^-  cone
      =/  pairs=(list [hed=type tal=type])
        %+  turn  ~(tap in p.typ)
        |=  t=type
        [(~(peek ut t) %free 2) (~(peek ut t) %free 3)]
      =/  [cell-heads=_pairs atom-heads=_pairs]
        (skid pairs |=([h=type *] (nests-in-cell h)))
      :+  %'$^'
        ?.  ?=([* ~] cell-heads)
          ~|(%bucket-indiscriminable !!)
        outer-loop(typ [%cell i.cell-heads])
      ?:  ?=([* ~] atom-heads)
        outer-loop(typ [%cell i.atom-heads])
      =/  cases  (turn atom-heads |=([type type] [%cell +<]))
      make-buccen(p.typ (~(gas in *(set type)) cases))
    --
  ::
      [%hint *]  $(typ q.typ)
      [%hold *]
    =/  ix=(unit @ud)
      =/  ix  0
      |-  ^-  (unit @ud)
      ?~  holds  ~
      ?:  =(i.holds [p q]:typ)
        `ix
      $(ix +(ix), holds t.holds)
    ?^  ix
      [%back u.ix]
    =.  holds  [[p q]:typ holds]
    =/  nex  (~(play ut p.typ) q.typ)
    [%loop $(typ nex)]
  ==
++  cone-to-type
  =|  loops=(list cone)
  |=  con=cone
  ^-  type
  ?@  con  %noun
  ?-    -.con
      %cell  [%cell $(con p.con) $(con q.con)]
      %face  [%face p.con $(con q.con)]
      %atom  [%atom aura.con ~]
      %mote  [%atom aura.con `val.con]
      %'$?'  [%fork (~(run in fan.con) |=([a=aura v=@] [%atom a `v]))]
      %'$@'  [%fork (sy $(con p.con) $(con q.con) ~)]
      %'$^'  [%fork (sy $(con p.con) $(con q.con) ~)]
      %'$%'
    :-  %fork
    %-  sy
    %+  turn  ~(tap by fan.con)
    |=  [[=aura val=@] com=cone]
    ^-  type
    [%cell [%atom aura `val] ^$(con com)]
  ::
      %loop
    :+  %hold  -:!>(..zuse)
    !!
  ::
      %back
    !!
  ==
--