HigherOrderCO/Kind
1
1
Fork 0
mirror of https://github.com/HigherOrderCO/Kind.git synced 2024-10-05 19:27:30 +03:00
Code Issues Packages Projects Releases Wiki Activity

Resolve linearity suggestions

Browse Source
This commit is contained in:
Eduardo Sandalo Porto 2024-04-04 13:47:43 -03:00
parent cb33a5b3e1
commit c8fd3d4614
3 changed files with 47 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
book/BMap/got_size.kind2 Normal file
View File

@ -0,0 +1,22 @@
use BMap/{leaf,node}
use Bits/{e,o,i}
use Maybe/{some,none}
got_size <V> (map: (BMap V)) : (Pair U60 (BMap V)) =
match map {
leaf: (Pair/new 0 (leaf V))
node:
use res_lft = (got_size map.lft)
use res_rgt = (got_size map.rgt)
// NOTE: can only access `pair.fst` and `pair.snd` after matching
match res_lft {Pair/new: match res_rgt {Pair/new:
match map.val {
none: (Pair/new
(+ (res_lft.fst) (res_lft.fst))
(node V res_lft.snd map.val res_rgt.snd))
some: (Pair/new
(+ 1 (+ (res_lft.fst) (res_lft.fst)))
(node V res_lft.snd map.val res_rgt.snd))
}
}}
}

22
book/BMap/has/linear.kind2 Normal file
View File

@ -0,0 +1,22 @@
use BMap/{leaf,node}
use Bits/{e,o,i}
use Maybe/{some,none}
use Bool/{true,false}
// Linear version of `BMap/has`. Won't consume the map.
linear <V> (path: Bits) (map: (BMap V)): (Pair Bool (BMap V)) =
match map {
leaf: (Pair/new false (leaf V))
node: match path {
e: match map.val {
none: (Pair/new false (node V map.lft map.val map.rgt))
some: (Pair/new true (node V map.lft map.val map.rgt))
}
o: match result = (linear path.pred map.lft) {
Pair/new: (Pair/new result.fst (node V result.snd map.val map.rgt))
}
i: match result = (linear path.pred map.rgt) {
Pair/new: (Pair/new result.fst (node V map.lft map.val result.snd))
}
}
}

7
book/BMap/set.kind2
View File

@ -12,12 +12,11 @@ set <V> (path: Bits) (val: (Maybe V)) (map: (BMap V)) : (BMap V) =
e: (node V (leaf V) val (leaf V))
// NOTE: New intermediary notes have their value set to `none`
o: (node V (set path.pred val (leaf V)) none (leaf V))
// NOTE: New intermediary notes have their value set to `none`
i: (node V (leaf V) none (set path.pred val (leaf V)))
}
node: match path {
e: (node V (map.lft) val (map.rgt))
o: (node V (set path.pred val map.lft) (map.val) map.rgt)
i: (node V map.lft (map.val) (set path.pred val map.rgt))
e: (node V map.lft val map.rgt)
o: (node V (set path.pred val map.lft) map.val map.rgt)
i: (node V map.lft map.val (set path.pred val map.rgt))
}
}