Refactor match and instantiate
This commit is contained in:
parent
d1e196f6f0
commit
0bf6b684fe
|
@ -171,8 +171,7 @@ proc enqueue(turn: var Turn; target: Facet; action: TurnAction) =
|
||||||
|
|
||||||
type Bindings = Table[Preserve[Ref], Preserve[Ref]]
|
type Bindings = Table[Preserve[Ref], Preserve[Ref]]
|
||||||
|
|
||||||
proc match(p: Pattern; v: Assertion): Option[Bindings] =
|
proc match(bindings: var Bindings; p: Pattern; v: Assertion): bool =
|
||||||
proc walk(bindings: var Bindings; p: Pattern; v: Assertion): bool =
|
|
||||||
case p.orKind
|
case p.orKind
|
||||||
of PatternKind.Pdiscard: result = true
|
of PatternKind.Pdiscard: result = true
|
||||||
of PatternKind.Patom:
|
of PatternKind.Patom:
|
||||||
|
@ -187,59 +186,58 @@ proc match(p: Pattern; v: Assertion): Option[Bindings] =
|
||||||
of PatternKind.Pembedded:
|
of PatternKind.Pembedded:
|
||||||
result = v.isEmbedded
|
result = v.isEmbedded
|
||||||
of PatternKind.Pbind:
|
of PatternKind.Pbind:
|
||||||
if walk(bindings, p.pbind.pattern, v):
|
if match(bindings, p.pbind.pattern, v):
|
||||||
bindings[toPreserve(p.pbind.pattern, Ref)] = v
|
bindings[toPreserve(p.pbind.pattern, Ref)] = v
|
||||||
result = true
|
result = true
|
||||||
of PatternKind.Pand:
|
of PatternKind.Pand:
|
||||||
for pp in p.pand.patterns:
|
for pp in p.pand.patterns:
|
||||||
result = walk(bindings, pp, v)
|
result = match(bindings, pp, v)
|
||||||
if not result: break
|
if not result: break
|
||||||
of PatternKind.Pnot:
|
of PatternKind.Pnot:
|
||||||
var b: Bindings
|
var b: Bindings
|
||||||
result = not walk(b, p.pnot.pattern, v)
|
result = not match(b, p.pnot.pattern, v)
|
||||||
of PatternKind.Lit:
|
of PatternKind.Lit:
|
||||||
result = p.lit.value == v
|
result = p.lit.value == v
|
||||||
of PatternKind.Pcompound:
|
of PatternKind.PCompound:
|
||||||
let
|
case p.pcompound.orKind
|
||||||
ctor = p.pcompound.ctor
|
of PCompoundKind.rec:
|
||||||
case ctor.orKind
|
|
||||||
of ConstructorspecKind.Crec:
|
|
||||||
if v.isRecord and
|
if v.isRecord and
|
||||||
ctor.crec.label == v.label and
|
p.pcompound.rec.label == v.label and
|
||||||
ctor.crec.arity == v.arity:
|
p.pcompound.rec.fields.len == v.arity:
|
||||||
for key, pp in p.pcompound.members:
|
result = true
|
||||||
if not key.isInteger:
|
for i, pp in p.pcompound.rec.fields:
|
||||||
|
if not match(bindings, pp, v[i]):
|
||||||
result = false
|
result = false
|
||||||
else:
|
break
|
||||||
result = walk(bindings, pp, v.record[key.int])
|
of PCompoundKind.arr:
|
||||||
if not result: break
|
if v.isSequence and p.pcompound.arr.items.len == v.sequence.len:
|
||||||
of ConstructorspecKind.Carr:
|
result = true
|
||||||
if v.isSequence and ctor.carr.arity == v.sequence.len:
|
for i, pp in p.pcompound.arr.items:
|
||||||
for key, pp in p.pcompound.members:
|
if not match(bindings, pp, v[i]):
|
||||||
result =
|
result = false
|
||||||
if not key.isInteger: false
|
break
|
||||||
else: walk(bindings, pp, v.sequence[key.int])
|
of PCompoundKind.dict:
|
||||||
if not result: break
|
|
||||||
of ConstructorspecKind.Cdict:
|
|
||||||
if v.isDictionary:
|
if v.isDictionary:
|
||||||
for key, pp in p.pcompound.members:
|
result = true
|
||||||
|
for key, pp in p.pcompound.dict.entries:
|
||||||
let vv = v[key]
|
let vv = v[key]
|
||||||
result =
|
if vv.isFalse or not match(bindings, pp, vv):
|
||||||
if vv.isFalse: false
|
result = true
|
||||||
else: walk(bindings, pp, vv)
|
break
|
||||||
if not result: break
|
|
||||||
|
proc match(p: Pattern; v: Assertion): Option[Bindings] =
|
||||||
var b: Bindings
|
var b: Bindings
|
||||||
if walk(b, p, v): result = some b
|
if match(b, p, v):
|
||||||
|
result = some b
|
||||||
|
|
||||||
proc instantiate(t: Template; bindings: Bindings): Assertion =
|
proc instantiate(t: Template; bindings: Bindings): Assertion =
|
||||||
proc walk(t: Template): Assertion =
|
|
||||||
case t.orKind
|
case t.orKind
|
||||||
of TemplateKind.Tattenuate:
|
of TemplateKind.Tattenuate:
|
||||||
let v = walk(t.tattenuate.template)
|
let v = instantiate(t.tattenuate.template, bindings)
|
||||||
if not v.isEmbedded:
|
if not v.isEmbedded:
|
||||||
raise newException(ValueError, "Attempt to attenuate non-capability: " & $v)
|
raise newException(ValueError, "Attempt to attenuate non-capability")
|
||||||
result = embed(attenuate(v.embed, t.tattenuate.attenuation))
|
result = embed(attenuate(v.embed, t.tattenuate.attenuation))
|
||||||
of TemplateKind.Tref:
|
of TemplateKind.TRef:
|
||||||
let n = $t.tref.binding
|
let n = $t.tref.binding
|
||||||
try: result = bindings[toPreserve(n, Ref)]
|
try: result = bindings[toPreserve(n, Ref)]
|
||||||
except KeyError:
|
except KeyError:
|
||||||
|
@ -247,21 +245,19 @@ proc instantiate(t: Template; bindings: Bindings): Assertion =
|
||||||
of TemplateKind.Lit:
|
of TemplateKind.Lit:
|
||||||
result = t.lit.value
|
result = t.lit.value
|
||||||
of TemplateKind.Tcompound:
|
of TemplateKind.Tcompound:
|
||||||
let ctor = t.tcompound.ctor
|
case t.tcompound.orKind
|
||||||
case ctor.orKind
|
of TCompoundKind.rec:
|
||||||
of ConstructorspecKind.Crec:
|
result = initRecord(t.tcompound.rec.label, t.tcompound.rec.fields.len)
|
||||||
result = initRecord(ctor.crec.label, ctor.crec.arity)
|
for i, tt in t.tcompound.rec.fields:
|
||||||
for key, tt in t.tcompound.members:
|
result[i] = instantiate(tt, bindings)
|
||||||
result.record[key.int] = walk(tt)
|
of TCompoundKind.arr:
|
||||||
of ConstructorspecKind.Carr:
|
result = initSequence[Ref](t.tcompound.arr.items.len)
|
||||||
result = initSequence[Ref](ctor.carr.arity)
|
for i, tt in t.tcompound.arr.items:
|
||||||
for key, tt in t.tcompound.members:
|
result[i] = instantiate(tt, bindings)
|
||||||
result.sequence[key.int] = walk(tt)
|
of TCompoundKind.dict:
|
||||||
of ConstructorspecKind.Cdict:
|
|
||||||
result = initDictionary[Ref]()
|
result = initDictionary[Ref]()
|
||||||
for key, tt in t.tcompound.members:
|
for key, tt in t.tcompound.dict.entries:
|
||||||
result[key] = walk(tt)
|
result[key] = instantiate(tt, bindings)
|
||||||
walk(t)
|
|
||||||
|
|
||||||
proc rewrite(r: Rewrite; v: Assertion): Assertion =
|
proc rewrite(r: Rewrite; v: Assertion): Assertion =
|
||||||
let bindings = match(r.pattern, v)
|
let bindings = match(r.pattern, v)
|
||||||
|
|
Loading…
Reference in New Issue