Why ? Because I'm tired of writing assertions everywhere.
type
AtomicNode= refinement x: Node
x.kind in AtomicNodes
proc getParent(node: not AtomicNode): Node =
impl
If it can't prove at CT that node is not AtomicNode, then it tries it in realtime. Generated code for realtime is like this (at place of call):
var result =
if not (x.kind in AtomicNodes):
getParent(x)
else:
raise newException(ValueError, "refinement predicate failed")
It's less than ideal, but thanks to converter and distinct a subset of refinement types are possible with present Nim.
import std/[macros, genasts]
type RefinementError* = object of CatchableError
macro refineType(name: untyped, base: typedesc, expressions: varargs[untyped]): untyped =
if expressions.len == 0:
error("Cannot refine nothing, need to provide atleast one requirement", expressions)
var expr = expressions[0]
for arg in expressions[1..^1]:
expr = infix(expr, "and", arg)
result = genast(name, base, expr):
type name* {.borrow: `.`.} = distinct base
converter toBase*(val: name): base = base(val)
#converter toBase*(val: var name): var base = base(val)
converter `to name`(it {.inject.}: base): name =
if not expr:
raise (ref RefinementError)(msg: "Failed to refine to type.")
name(it)
converter `to name`(it {.inject.}: var base): var name =
if not expr:
raise (ref RefinementError)(msg: "Failed to refine to type.")
name(it)
refineType DivBy10, int, (it mod 10 == 0)
var a: DivBy10 = 20
doAssertRaises RefinementError: a = a + 3
a = a + 10
type MyType = object
case kind: uint8
of 0, 1, 2:
a, b: int
of 3, 4:
c, d: float
else:
e, f: string
refineType Atom, MyType, it.kind in {0u8, 1, 2}
proc doThing(atom: Atom): string = $atom.a & $atom.b
assert MyType(kind: 0, a: 300, b: 400).doThing == "300400"
doAssertRaises RefinementError: discard MyType(kind: 3, c: 300, d: 400).doThing()
I was too lazy to do it this way but using type section macros one could also write it in the more clear syntax as the following.
type Atom {.refinement.} = concept it
it.kind in {0u8, 1, 2}
Wow that's really amazing, thanks for sharing!
Nim is very powerful indeed.
Would you mind to put this into a library and make it available via nimble ?