~plan/plunder

9b7d850ba9839e407ebdd91533221c330c105442 — Sol 4 months ago fae9aa1
viceroy: col rune, bugfixes, pq_vice.sire

Viceroy is getting close to being able to handle pq.sire

This commit starts a temporary hacked-up version of pq.sire
which does not use type-inference and manually annotates
every binding.
2 files changed, 358 insertions(+), 32 deletions(-)

A sire/pq_vice.sire
M sire/viceroy.sire
A sire/pq_vice.sire => sire/pq_vice.sire +214 -0
@@ 0,0 1,214 @@
; Copyright 2023 The Plunder Authors
; Use of this source code is governed by a BSD-style license that can be
; found in the LICENSE file.

#### pq_vice <- viceroy

;;;; Priority Queues
;;;; ===============
;;;;
;;;; This implementation is based on section 4.16 of the book 'ML for the
;;;; Working Programmer' by Larry C. Paulson (Cambridge University Press
;;;; [1996]).
;;;;
;;;; It is modified to support a customizeable comparator function (`cmp`,
;;;; below) which is passed as an argument to many `pq.*` functions. This
;;;; allows similar functionality to, for example, a Haskell `Ord`
;;;; instance. `cmp` takes 2 arguments and outputs a LT/EQ/GT value
;;;; (see 03_nat.sire) indicating their relation to each other.


;;; Imports ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

:| sire_02_bit [if and TRUE FALSE]
:| sire_03_nat [LT EQ GT div sub]
:| sire_04_cmp [eql cmp neq]
:| sire_07_dat [listUnsafeHead listDrop NIL listRev listFoldr]
:| sire_07_dat [SOME NONE maybeCase]
:| viceroy


;;; Types ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

# data Pq
- LF
- BR Nat Pq Pq

= pqEmpty LF

= pqNull
? (pqNull t/Pq >Bit)
| (t == pqEmpty)

#* =?= TRUE  | pqNull LF
#* =?= FALSE | pqNull (BR 7 LF LF)

= pqInsert
? (pqInsert cmp/NatCmp w/Nat t/Pq >Pq)
^       >(Nat -> Pq -> Pq)
    | _ w t
? (go w/Nat t/Pq >Pq)
# case t
- LF
    | BR w LF LF
- BR v t1 t2
    | if (cmp w v == GT) | (BR v (go w t2) t1)
    | else               | (BR w (go v t2) t1)

= leftRem
? (leftRem cmp/NatCmp t/Pq >(MaybeNat, Pq))
# case t
- LF [NONE t]
- BR w t1 t2
    | if (pqNull t1 && pqNull t2)
        | (SOME w, LF)
    | else
        ; [mbW t] (leftRem cmp t1)
        @ pair/(MaybeNat, Pq) (leftRem cmp t1)
        @ mbW/MaybeNat        (fst pair)
        @ t/Pq                (snd pair)
        | (mbW, BR w t2 t)

* = test1 | pqInsert cmp 0 pqEmpty
* = test2 | pqInsert cmp 1 test1
* = test3 | leftRem cmp test2

= siftDown
? (siftDown cmp/NatCmp w/Nat t1/Pq t2/Pq >Pq)
^       > (Nat -> Pq -> Pq -> Pq)
    | _ w t1 t2
? (go w/Nat t1/Pq t2/Pq >Pq)
# case t1
- LF
    # case t2
    - LF | BR w LF LF
    - _  | go w t2 t1
- BR v1 t1L t1R
    # case t2
    - LF
        | if (and (pqNull t1L) (pqNull t1R))
            | if (cmp w v1 == GT)
                | BR v1 (BR w LF LF) LF
            | else
                | BR w t1 LF
        | die {siftDown: wat}
    - BR v2 t2L t2R
        | if ((GT /= cmp w v1) && (GT /= cmp w v2))
            | BR w t1 t2
        | if (GT == cmp v1 v2)
            | BR v2 t1 (go w t2L t2R)
        | else
            | BR v1 (go w t1L t1R) t2

= pqDelMin
? (pqDelMin cmp/NatCmp t/Pq >(MaybeNat, Pq))
# case t
- LF [NONE LF]
- BR v t1 t2
    @ pair/(MaybeNat, Pq) | leftRem cmp t1
    @ mbW/MaybeNat        | fst pair
    @ t/Pq                | snd pair
    | maybeCase mbW (SOME v, LF)
    & (w/Nat >(MaybeNat, Pq))
    | (SOME v, siftDown cmp w t2 t)

= pqMin
? (pqMin t/Pq >MaybeNat)
# case t
- LF       | NONE
- BR w _ _ | SOME w

=?= (SOME 7) | pqMin (BR 7 LF LF)

= heapify
? (heapify cmp/NatCmp ls/ListNat >(Pq, ListNat))
^       >(Nat -> ListNat -> (Pq, ListNat))
    | _ (listLen ls) ls
? (go n/Nat vs/ListNat >(Pq, ListNat))
# case vs
- LN_NIL
    | [LF vs]
- LN_CONS v vs
    @ p1/(Pq, ListNat) | go (div n 2) vs
    @ t1/Pq            | fst p1
    @ vs1/ListNat      | snd p1
    @ p2/(Pq, ListNat) | go (div (sub n 1) 2) vs1
    @ t2/Pq            | fst p2
    @ vs2/ListNat      | snd p2
    | (siftDown cmp v t1 t2, vs2)

= pqFromList
? (pqFromList cmp/NatCmp vs/ListNat >Pq)
| fst (heapify cmp vs)

= pqFromList0
? (pqFromList0 cmp/NatCmp vs/ListNat >Pq)
| listFoldl (acc x & pqInsert cmp x acc) pqEmpty vs

= (pqToList cmp/NatCmp t/Pq >ListNat)
^ _ NIL t
? (go acc t)
@ [mbW t1] (pqDelMin cmp t)
: w < maybeCase mbW (listRev acc)
| go (w::acc) t1

= (pqSort cmp/NatCmp xs/Pq >ListNat)
| pqToList cmp
| pqFromList cmp
| xs

= (pqSort0 cmp/NatCmp xs)
| pqToList cmp
| pqFromList0 cmp
| xs

=?= ~[0 1 2 3 5 7 9 9]
  | pqSort  cmp ~[1 9 7 5 2 0 9 3]

=?= ~[0 1 2 3 5 7 9 9]
  | pqSort0 cmp ~[1 9 7 5 2 0 9 3]

;; more sophisticated tests, examining laziness of pq values.
;; we ensure that infinite values at position 1 of a tuple can pass in/out of
;; pqs, provided they are not touched.

= (cmpPairNatKey p1 p2)
| cmp idx-0-p1 idx-0-p2

= (repeat n)
@@ z=(n::z)
 z

=?= 9
  # case
      | pqMin
      | pqInsert cmpPairNatKey (9, repeat 3) pqEmpty
  - NONE   | 7
  - SOME x | idx 0 x

; insert in ascending order of key
=?= 110
  @ ls0 : x < listGen 11
        | (x, repeat x)
  @ pq (pqFromList0 cmpPairNatKey ls0)
  @ ls1 (pqToList cmpPairNatKey pq)
  | listSum : p < listForEach ls1
            | add idx-0-p (listUnsafeHead idx-1-p)

; insert in descending order of key

=?= 110
  @ ls0 : x < listGen 11
        | (sub 10 x, repeat (sub 10 x))
  @ pq (pqFromList0 cmpPairNatKey ls0)
  @ ls1 (pqToList cmpPairNatKey pq)
  | listSum : p < listForEach ls1
            | add idx-0-p (listUnsafeHead idx-1-p)


;;; Exports ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

^-^
^-^ pqEmpty pqInsert pqDelMin pqMin pqNull
^-^ pqFromList pqToList pqSort
^-^

M sire/viceroy.sire => sire/viceroy.sire +144 -32
@@ 11,7 11,7 @@
;;;; DONE Implement the (~) rune (list literals)
;;;; DONE Implement List[3 4] literals.
;;;; DONE Implement the (::) rune (cons)
;;;; TODO Implement the (:) rune (monadic bind)
;;;; DONE Implement the (:) rune (monadic bind)
;;;;
;;;; DONE Implement the (@@) rune (LETREC bindings).
;;;; DONE _-patterns in LET bindings (not included in namespace).


@@ 161,6 161,7 @@ TNAT=(TREF "Nat")
- EBIT Bit
- ENAT Nat
- EEQL Exp Exp
- ENEQ Exp Exp
- ECONS Exp Exp
- EAND Exp Exp
- EREF Str


@@ 171,7 172,8 @@ TNAT=(TREF "Nat")
- ELIST xs/(Row Exp)
- EKET t/Txp b/Exp v/Exp
- EREC n/Str t/Txp v/Exp b/Exp
- EFUN inline/Bit pin/Bit nm/Str Row-(Exp,Txp) rTy/Txp b/Exp
- ELAM inline/Bit pin/Bit nm/Str Row-(Exp,Txp) rTy/Txp b/Exp
- ECOL (Txp, Row-(Exp,Txp)) x/Exp b/Exp

# typedef CaseBranch (CaseBranchE Exp)



@@ 309,7 311,7 @@ abstype#TypeTree
        | failStr rex {What is this nonsense?}
    | readExp (INFX {#} (WORD txt 0, heir) 0)
| if (rexStyle rex /= {WORD})
    | failStr rex {viceroy has no strings}
    | ENAT txt
| if (txt == {true})  | EBIT TRUE
| if (txt == {false}) | EBIT FALSE
| if (okIdn bar)      | EREF txt


@@ 332,6 334,11 @@ abstype#TypeTree
| if (len kids /= 2) | failStr rex {nonsense (==) rune}
| EEQL (readExp a) (readExp b)

= (readNeq readExp rex)
@ kids@[a b]         | rexKids rex
| if (len kids /= 2) | failStr rex {nonsense (/=) rune}
| ENEQ (readExp a) (readExp b)

; TODO: Support more items.
= (readAnd readExp rex)
@ kids@[a b]         | rexKids rex


@@ 339,6 346,7 @@ abstype#TypeTree
| EAND (readExp a) (readExp b)

= (readTxp rex)
@ kids (rexKids rex)
# switch (rexType rex)
* _
    | failStr rex {invalid type: what is this?}


@@ 348,8 356,12 @@ abstype#TypeTree
    | TREF (rexText rex)
* {NODE}
    # switch (rexRune rex)
    * {,} | TTUP (map readTxp rexKids-rex)
    * _   | failStr rex {unknown rune in type expression}
    * {,}  | TTUP (map readTxp kids)
    * {->} | foldr1 TFUN (map readTxp kids)
    ; {|}  @ tys (map readTxp kids)
    ;      | if null-tys (failStr rex {use [] instead})
    ;      | tyApp (fst tys) (drop 1 tys)
    * _    | failStr rex {unknown rune in type expression}

= (readApp readExp rex)
@ exps


@@ 424,7 436,7 @@ abstype#TypeTree
@ bodExp                  | readExp body
@ nm                      | readSym name
@ (retTy, args)           | readAnonSig sig (drop 1 sigs)
| EFUN FALSE pinned nm args retTy bodExp
| ELAM FALSE pinned nm args retTy bodExp

= (readAnonLambda readExp rex)
@ badLam                  | failStr rex {malformed lambda}


@@ 434,7 446,7 @@ abstype#TypeTree
| if (len kids /= 2)      | badLam
| if (rexRune sig /= {|}) | badSig
@ (retTy, args)           | readAnonSig sig argRxs
| EFUN FALSE FALSE 0 args retTy (readExp body)
| ELAM FALSE FALSE 0 args retTy (readExp body)

= (readLet readExp rex)
@ kids@[patRex val body] | rexKids rex


@@ 447,6 459,30 @@ abstype#TypeTree
    | failStr rex {internal error: trying to create empty APP node}
| foldl EAPP (idx 0 row) (drop 1 row)

= (readColBinder readExp rex)
@ rune (rexRune rex)
| if (rune /= {<})      | failStr rex } Expected a < node in : binder
| if null-(rexKids rex) | failStr rex } Empty bind expression
| readExp (rexSetRune {|} rex)

; : arg/Nat < func
; body
= (readCol readExp rex)
    @ sons   | rexSons rex
    @ nSon   | len sons
    @ lastIx | dec nSon
    @ heir   | rexHeir rex

    | ifz heir        | failStr rex {: requires an heir}
    | if (lth nSon 2) | failStr rex {: requires two params}

    @ valRex (idx lastIx sons)
    | if (rexRune valRex /= "<")
        | failStr valRex {< rune was expected here}
    @ !valExp (readExp | rexSetRune {|} valRex)

    | ECOL (readAnonSig rex | take lastIx sons) valExp (readExp heir)

= (readKet readExp rex)
@ kids     | rexKids rex
@ nKid     | len kids


@@ 531,6 567,7 @@ abstype#TypeTree
* {LEAF} | readLeaf readExp rex
* {NODE} # switch (rexRune rex)
         * {==} | readEql readExp rex
         * {/=} | readNeq readExp rex
         * {&&} | readAnd readExp rex
         * {|}  | readApp readExp rex
         * {.+} | readAdd readExp rex


@@ 538,6 575,7 @@ abstype#TypeTree
         * {+}  | ETUP (readSeq readExp rex)
         * {,}  | ETUP (readSeq readExp rex)
         * {^}  | readKet readExp rex
         * {:}  | readCol readExp rex
         * {~}  | readSig readExp rex
         * {::} | readCons readExp rex
         * {@}  | readLet readExp rex


@@ 626,6 664,12 @@ abstype#TypeTree
=?= (BIND "x" (EADD ENAT-3 EREF-{y}))
  | readCmd '(x = (3.+y))

=?=   | readExp '(: x/Nat >Nat < 7 8)x
  | ECOL
  * (TNAT, [({x},TNAT)])
  * EAPP ENAT-7 ENAT-8
  * EREF-{x}


;;; Converting Between Type Representations ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;



@@ 656,7 700,7 @@ abstype#TypeTree

= (showViceType vty)
# case vty
- TREF-nm  | `[$(symToRex "nm")]
- TREF-nm  | symToRex nm
- TFUN a b | `($(showViceType a) -> $(showViceType b))
- TTUP xs  | NEST {,} (map showViceType xs) 0



@@ 687,6 731,7 @@ abstype#TypeTree
    - EBIT b       | if b 'true 'false
    - ENAT n       | WORD (showNat n) 0
    - EEQL a b     | `($(showExp a) == $(showExp b))
    - ENEQ a b     | `($(showExp a) /= $(showExp b))
    - EAND a b     | `($(showExp a) && $(showExp b))
    - EADD a b     | `($(showExp a) .+ $(showExp b))
    - ECONS a b    | `($(showExp a) :: $(showExp b))


@@ 710,7 755,13 @@ abstype#TypeTree
        ` @@ $(showPat (PVAR n t)) $(showExp v)
           $(showExp b)

    - EFUN inlined pinned name args resTy body
    - ECOL (rTy, args) expr body
        ^ OPEN {:} _ (showExp body)
        | weld (map showTypedSym args)
       ++ ` >($(showViceType rTy))
       ++ ` < $(showExp expr)

    - ELAM inlined pinned name args resTy body
        | if (not inlined && not pinned && eqz name)
            @ argList
                ^ NEST {|} _ 0


@@ 718,7 769,16 @@ abstype#TypeTree
                ` >($(showViceType resTy))
            ` & $argList
              $(showExp body)
        | die "umm",(inlined, pinned, name, args, resTy, body)
        | if (not inlined && not pinned)
            @ argList
                ^ NEST {|} _ 0
                | rowCons (symToRex name)
                | rowSnoc (map showTypedSym args)
                ` >($(showViceType resTy))
            ` ? $argList
              $(showExp body)
        | else
            | die "show fancy functions",(=inlined, =pinned, =name, =args, =resTy, =body)





@@ 826,7 886,7 @@ abstype#TypeTree
++
    ^ sizedListToRow numBinds adtSire::_
    : [bindNum fieldIx] < listForEach (listIndexed | setToList slots)
    | A K-(idx | inc fieldIx) V-(inc bindNum)
    | A K-(idx | inc fieldIx) V-bindNum
++
    ^ map _ branches
    & (_c, fields, expr)


@@ 840,9 900,9 @@ abstype#TypeTree
              ++ ("BAR", [0 0 0 0 SOME-{z}], EREF-{z})

=?=  ++   ++ K {lol}
          ++ A K-(idx 2) V-1
          ++ A K-(idx 3) V-2
          ++ A K-(idx 5) V-3
          ++ A K-(idx 2) V-0
          ++ A K-(idx 3) V-1
          ++ A K-(idx 5) V-2
     ++   ++ [0 SOME-{x} SOME-{y} 0]
          ++ [0 0 0 SOME-{z}]
  | caseBinds K-{lol}


@@ 889,12 949,12 @@ abstype#TypeTree
    | {internal error: failed to lookup constructor information}
| [tag fieldTys]

= (badCase adt)
^ die (strCat _)
= (badCase adt scrutVal)
^ die [(strCat _) scrutVal]
++ {unhandled case when pattern-matching on }
++ lawName (pinItem (snd (fst (pinItem adt))))

(defaultFallback adt)=(A K-badCase K-adt)
(defaultFallback adt scrutVar)=(apple K-badCase (K-adt, scrutVar))

= (checkExaustivity (PIN [ty cnstrs]) info branches mFall)
@ rex       | `(#case)


@@ 914,9 974,10 @@ abstype#TypeTree
@ (binds, envs) | caseBinds (go e scrut) branches
@ (adt, info)   | getBranchInfo ss branches
| seq           | checkExaustivity adt info branches mFall
@ fall          | maybeCase mFall (defaultFallback adt) f&(go e f)
@ scrutVar      | V dec-(len binds)
@ fall          | maybeCase mFall (defaultFallback adt scrutVar) f&(go e f)
^ foldr L _ binds
| switchSire (A K-dataTag V-(len binds)) fall
| switchSire (A K-dataTag scrutVar) fall
| tabFromPairs
: [[[cNm binds x] enu] [tag fieldTys]]
    < foreach (zip (zip branches envs) info)


@@ 938,6 999,7 @@ abstype#TypeTree
= (addSire a b) | apple (G getBind#add) [a b]
= (andSire a b) | apple (G getBind#and) [a b]
= (eqlSire a b) | apple (G getBind#eql) [a b]
= (neqSire a b) | apple (G getBind#neq) [a b]

= (consSire a b) | apple (G getBind#CONS) [a b]



@@ 956,6 1018,7 @@ abstype#TypeTree
    - EADD a b  | addSire (go e a) (go e b)
    - ECONS a b | consSire (go e a) (go e b)
    - EEQL a b  | eqlSire (go e a) (go e b)
    - ENEQ a b  | neqSire (go e a) (go e b)
    - EAND a b  | andSire (go e a) (go e b)
    - ETUP xs   | rowSire (map go-e xs)



@@ 995,7 1058,10 @@ abstype#TypeTree
        @ e2 (SOME n :: e)
        | R [(go e2 var)] (go e2 body)

    - EFUN inline pinned name args _rTy body
    - ECOL (rTy, args) expr body
        | go e (EAPP expr (ELAM FALSE FALSE 0 args rTy body))

    - ELAM inline pinned name args _rTy body
        @ tag     | name
        @ arity   | len args
        ^ mkF pinned inline tag arity _


@@ 1006,10 1072,10 @@ abstype#TypeTree
    - _ (die {malformed ast},exp)

=?=   | L (K {ADT})
      | L (A K-(idx 2) V-1)
      | L (A K-(idx 3) V-2)
      | L (A K-(idx 5) V-3)
      ^ apple K-tabSwitch (A K-dataTag V-4, K-{fallback}, tabSire _)
      | L (A K-(idx 2) V-0)
      | L (A K-(idx 3) V-1)
      | L (A K-(idx 5) V-2)
      ^ apple K-tabSwitch (A K-dataTag V-3, K-{fallback}, tabSire _)
     ## =FOO | addSire V-2 V-1
     ## =BAR | V-0



@@ 1086,6 1152,11 @@ abstype#TypeTree
        @ !bTy | go {eql} e SOME-aTy b
        | bitRoot

    - ENEQ a b
        @ !aTy | go {neq} e NONE a
        @ !bTy | go {neq} e SOME-aTy b
        | bitRoot

    - EAND a b
        @ !aTy | go {and} e SOME-bitRoot
        @ !bTy | go {and} e SOME-bitRoot


@@ 1144,7 1215,10 @@ abstype#TypeTree
        | maybeCase mExpect natRoot id
        ; TODO

    - EFUN inlined pinned name args resTxp body
    - ECOL (rTy, args) expr body
        | go {ecol} e mExpect (EAPP expr (ELAM FALSE FALSE 0 args rTy body))

    - ELAM inlined pinned name args resTxp body
        @ argTxps  | map snd args
        @ !argTys  | force | map (viceType ss #[]) argTxps
        @ !resTy   | force | viceType ss #[] resTxp


@@ 1210,7 1284,7 @@ ex=(readExp '(const x/Nat y/Bit >Nat ? x))
(funcType a b)=(tyApp Fun [a b])
(mkFun xs)=(foldr1 funcType xs)

=?= ex                     | EFUN 0 0 "const" ({x},TNAT, {y},TBIT) TNAT EREF-{x}
=?= ex                     | ELAM 0 0 "const" ({x},TNAT, {y},TBIT) TNAT EREF-{x}

=?= (compile ss ex)        | F (LAM 0 0 0 %const 2 V-1)



@@ 1294,7 1368,7 @@ ex=(readExp '(const x/Nat y/Bit >Nat ? x))

    @ props | bstSave (bstPut props {type} type)
    @ plan  | evalSire sire
    @ bind  | PIN [nex plan sire ctx name props]
    @ !bind | PIN [nex plan sire ctx name props]
    @ ss    | (inc nex, ctx, tabPut binds name bind, mods)

    | trk ` > $(showType type)


@@ 1383,6 1457,10 @@ ex=(readExp '(const x/Nat y/Bit >Nat ? x))
* # backfill NIL (List Nat)
* NIL_BIT=NIL
* # backfill NIL_BIT (List Bit)
* # backfill cmp (Nat > Nat > Ordering)
* # backfill fst (Pair a b > a)
* # backfill snd (Pair a b > b)
* # typedef NatCmp (Nat > Nat > Ordering)

{=}#=viceroy
{=?=}#=viceroy


@@ 1509,9 1587,10 @@ s3=(SOME 3)

#=?= ex
   #& a
   #| tabSwitch (#| dataTag a) (#| badCase maybeNatAdt)
   #@ b (#| c2 a {SOME})
   #| tabSwitch (#| dataTag b) (#| badCase maybeNatAdt b)
   #| %[SOME NONE]
   #| c2 1 (#| inc (#| idx 1 a))
   #| c2 1 (#| inc (#| idx 1 b))


;;; Same thing, but without -legible ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


@@ 1537,8 1616,9 @@ s3=(SOME 3)

#=?= ex
   #& a
   #| switch (#| dataTag a) (#| badCase maybeNatAdt)
   #| c2 (#| inc (#| idx 1 a)) 1
   #@ b (#| SOME a)
   #| switch (#| dataTag b) (#| badCase maybeNatAdt b)
   #| c2 (#| inc (#| idx 1 b)) 1


;;; Testing Fallback Handlers ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


@@ 1550,7 1630,8 @@ s3=(SOME 3)

#=?= ex
   #& a
   #| switch (#| dataTag a) 2
   #@ b (#| SOME a)
   #| switch (#| dataTag b) 2
   #| c1 1




@@ 1607,6 1688,10 @@ s3=(SOME 3)
 #@@ ax=(#| LN_CONS x ax)
  #| ax

#* :| prelude [{#}]
#* # backfill listLen (ListNat > Nat)
#* {#}#=viceroy


;;; ^-rune ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;



@@ 1630,3 1715,30 @@ s3=(SOME 3)
(List[3 4] =?= (3 :: 4 :: NIL))

(List[true false] =?= (true :: false :: NIL_BIT))


;;; :-rune ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

= const
? (const a/ListNat b/Nat >ListNat)
# case a
- LN_NIL       | LN_NIL
- LN_CONS x xs | LN_CONS x (const xs b)

= listNatForEach
? (listNatForEach list/ListNat f/(Nat -> Nat) >ListNat)
# case list
- LN_NIL       | LN_NIL
- LN_CONS x xs | LN_CONS (f x) (listNatForEach xs f)

=?= (LN_CONS 7 (LN_CONS 8 LN_NIL))
  | listNatForEach (LN_CONS 3 (LN_CONS 4 LN_NIL)) (add 4)

= ex
& (xs/ListNat >ListNat)
: x/Nat >Nat < listNatForEach xs
| add x x

#=?= ex
  #& a
  #| listNatForEach a (#& b (#| add b b))