Fully normalized top-level definitions
This commit is contained in:
@@ -46,14 +46,72 @@ nodePayloadValid? = (nodePayload :
|
||||
(nodePayloadStem? nodePayload)
|
||||
(nodePayloadFork? nodePayload)))
|
||||
|
||||
nodeU32FromBytes4 = (b0 b1 b2 b3 :
|
||||
u32BEBytesToNat
|
||||
(pair b0
|
||||
(pair b1
|
||||
(pair b2
|
||||
(pair b3 t)))))
|
||||
|
||||
withNodePayloadStemIndex = (nodePayload shortK indexK :
|
||||
matchList
|
||||
(shortK t)
|
||||
(tag r0 :
|
||||
matchList
|
||||
(shortK t)
|
||||
(b0 r1 :
|
||||
matchList
|
||||
(shortK t)
|
||||
(b1 r2 :
|
||||
matchList
|
||||
(shortK t)
|
||||
(b2 r3 :
|
||||
matchList
|
||||
(shortK t)
|
||||
(b3 _ :
|
||||
indexK (nodeU32FromBytes4 b0 b1 b2 b3))
|
||||
r3) r2) r1) r0) nodePayload)
|
||||
|
||||
withNodePayloadForkIndices = (nodePayload shortK indicesK :
|
||||
matchList
|
||||
(shortK t)
|
||||
(tag r0 :
|
||||
matchList
|
||||
(shortK t)
|
||||
(l0 r1 :
|
||||
matchList
|
||||
(shortK t)
|
||||
(l1 r2 :
|
||||
matchList
|
||||
(shortK t)
|
||||
(l2 r3 :
|
||||
matchList
|
||||
(shortK t)
|
||||
(l3 r4 :
|
||||
matchList
|
||||
(shortK t)
|
||||
(r0b r5 :
|
||||
matchList
|
||||
(shortK t)
|
||||
(r1b r6 :
|
||||
matchList
|
||||
(shortK t)
|
||||
(r2b r7 :
|
||||
matchList
|
||||
(shortK t)
|
||||
(r3b _ :
|
||||
indicesK
|
||||
(nodeU32FromBytes4 l0 l1 l2 l3)
|
||||
(nodeU32FromBytes4 r0b r1b r2b r3b)) r7) r6) r5) r4) r3) r2) r1) r0) nodePayload)
|
||||
|
||||
nodePayloadStemChildIndex = (nodePayload :
|
||||
u32BEBytesToNat (bytesTake 4 (bytesDrop 1 nodePayload)))
|
||||
withNodePayloadStemIndex nodePayload (_ : 0) (index : index))
|
||||
|
||||
nodePayloadForkLeftIndex = (nodePayload :
|
||||
u32BEBytesToNat (bytesTake 4 (bytesDrop 1 nodePayload)))
|
||||
withNodePayloadForkIndices nodePayload (_ : 0) (left right : left))
|
||||
|
||||
nodePayloadForkRightIndex = (nodePayload :
|
||||
u32BEBytesToNat (bytesTake 4 (bytesDrop 5 nodePayload)))
|
||||
withNodePayloadForkIndices nodePayload (_ : 0) (left right : right))
|
||||
|
||||
nodeRecordsHaveInvalidPayload? = y (self nodeRecords :
|
||||
matchList
|
||||
@@ -65,31 +123,44 @@ nodeRecordsHaveInvalidPayload? = y (self nodeRecords :
|
||||
nodeRecords)
|
||||
|
||||
nodePayloadChildIndices = (nodePayload :
|
||||
matchBool
|
||||
matchList
|
||||
t
|
||||
(matchBool
|
||||
(pair (nodePayloadStemChildIndex nodePayload) t)
|
||||
(pair (nodePayloadForkLeftIndex nodePayload)
|
||||
(pair (nodePayloadForkRightIndex nodePayload) t))
|
||||
(nodePayloadStem? nodePayload))
|
||||
(nodePayloadLeaf? nodePayload))
|
||||
(tag rest :
|
||||
lazyBool
|
||||
(_ :
|
||||
withNodePayloadStemIndex
|
||||
nodePayload
|
||||
(_ : t)
|
||||
(childIndex : pair childIndex t))
|
||||
(_ :
|
||||
lazyBool
|
||||
(_ :
|
||||
withNodePayloadForkIndices
|
||||
nodePayload
|
||||
(_ : t)
|
||||
(leftIndex rightIndex :
|
||||
pair leftIndex (pair rightIndex t)))
|
||||
(_ : t)
|
||||
(equal? tag nodePayloadForkTag))
|
||||
(equal? tag nodePayloadStemTag))
|
||||
nodePayload)
|
||||
|
||||
-- True iff index n names an element before limit in records.
|
||||
-- For topologically sorted indexed bundles, every child of record i must
|
||||
-- satisfy childIndex < i, so searching only the prefix [0, i) validates both
|
||||
-- bounds and acyclicity.
|
||||
nodeIndexInPrefix? = y (self n records i limit :
|
||||
matchBool
|
||||
nodeIndexInPrefix? = y (self records n i limit :
|
||||
matchList
|
||||
false
|
||||
(matchList
|
||||
false
|
||||
(_ rest :
|
||||
matchBool
|
||||
(_ rest :
|
||||
matchBool
|
||||
false
|
||||
(matchBool
|
||||
true
|
||||
(self n rest (succ i) limit)
|
||||
(self rest n (succ i) limit)
|
||||
(equal? i n))
|
||||
records)
|
||||
(equal? i limit))
|
||||
(equal? i limit))
|
||||
records)
|
||||
|
||||
nodeChildIndicesInPrefix? = y (self childIndices records limit :
|
||||
matchList
|
||||
@@ -98,7 +169,7 @@ nodeChildIndicesInPrefix? = y (self childIndices records limit :
|
||||
matchBool
|
||||
(self rest records limit)
|
||||
false
|
||||
(nodeIndexInPrefix? childIndex records 0 limit))
|
||||
(nodeIndexInPrefix? records childIndex 0 limit))
|
||||
childIndices)
|
||||
|
||||
nodePayloadIndicesValid? = (nodePayload i records :
|
||||
@@ -178,31 +249,124 @@ nodesSectionRecords = (nodesSection :
|
||||
(_ nodeRecords : nodeRecords)
|
||||
nodesSection)
|
||||
|
||||
nodePayloadToTreeWith = (self nodeRecords nodePayload :
|
||||
matchBool
|
||||
(ok t t)
|
||||
(matchBool
|
||||
(bindResult (self (nodePayloadStemChildIndex nodePayload) nodeRecords)
|
||||
(child _ : ok (t child) t))
|
||||
(bindResult (self (nodePayloadForkLeftIndex nodePayload) nodeRecords)
|
||||
(left _ :
|
||||
bindResult (self (nodePayloadForkRightIndex nodePayload) nodeRecords)
|
||||
(right _ : ok (pair left right) t)))
|
||||
(nodePayloadStem? nodePayload))
|
||||
(nodePayloadLeaf? nodePayload))
|
||||
nodeBuiltTreeIndex = (entry :
|
||||
matchPair
|
||||
(index _ : index)
|
||||
entry)
|
||||
|
||||
nodeIndexToTree = y (self nodeIndex nodeRecords :
|
||||
(nodePayload :
|
||||
matchBool
|
||||
(nodePayloadToTreeWith self nodeRecords nodePayload)
|
||||
(err errMissingNode t)
|
||||
(not? (equal? nodePayload t)))
|
||||
(nth nodeIndex nodeRecords))
|
||||
nodeBuiltTreeValue = (entry :
|
||||
matchPair
|
||||
(_ tree : tree)
|
||||
entry)
|
||||
|
||||
nodeTreeByIndex_ = (self builtTrees targetIndex :
|
||||
lazyList
|
||||
(_ : err errMissingNode t)
|
||||
(entry rest :
|
||||
lazyBool
|
||||
(_ : ok (nodeBuiltTreeValue entry) t)
|
||||
(_ : self rest targetIndex)
|
||||
(equal? (nodeBuiltTreeIndex entry) targetIndex))
|
||||
builtTrees)
|
||||
|
||||
nodeTreeByIndex = (builtTrees targetIndex :
|
||||
y nodeTreeByIndex_ builtTrees targetIndex)
|
||||
|
||||
nodePayloadToTreeFromBuilt = (builtTrees nodePayload :
|
||||
matchList
|
||||
(err errInvalidNodePayload t)
|
||||
(tag rest :
|
||||
lazyBool
|
||||
(_ : ok t t)
|
||||
(_ :
|
||||
lazyBool
|
||||
(_ :
|
||||
withNodePayloadStemIndex
|
||||
nodePayload
|
||||
(_ : err errInvalidNodePayload t)
|
||||
(childIndex :
|
||||
lazyResult
|
||||
(code after : err code after)
|
||||
(child _ : ok (t child) t)
|
||||
(nodeTreeByIndex builtTrees childIndex)))
|
||||
(_ :
|
||||
lazyBool
|
||||
(_ :
|
||||
withNodePayloadForkIndices
|
||||
nodePayload
|
||||
(_ : err errInvalidNodePayload t)
|
||||
(leftIndex rightIndex :
|
||||
lazyResult
|
||||
(code after : err code after)
|
||||
(left _ :
|
||||
lazyResult
|
||||
(code after : err code after)
|
||||
(right _ : ok (pair left right) t)
|
||||
(nodeTreeByIndex builtTrees rightIndex))
|
||||
(nodeTreeByIndex builtTrees leftIndex)))
|
||||
(_ : err errInvalidNodePayload t)
|
||||
(equal? tag nodePayloadForkTag))
|
||||
(equal? tag nodePayloadStemTag))
|
||||
(equal? tag 0))
|
||||
nodePayload)
|
||||
|
||||
nodeBuildState = (targetIndex i builtTrees :
|
||||
pair targetIndex (pair i builtTrees))
|
||||
|
||||
nodeBuildStateTargetIndex = (state :
|
||||
matchPair
|
||||
(targetIndex _ : targetIndex)
|
||||
state)
|
||||
|
||||
nodeBuildStateI = (state :
|
||||
matchPair
|
||||
(_ rest :
|
||||
matchPair
|
||||
(i _ : i)
|
||||
rest)
|
||||
state)
|
||||
|
||||
nodeBuildStateBuiltTrees = (state :
|
||||
matchPair
|
||||
(_ rest :
|
||||
matchPair
|
||||
(_ builtTrees : builtTrees)
|
||||
rest)
|
||||
state)
|
||||
|
||||
nodeIndexToTree_ = (self remainingRecords state :
|
||||
((nodeIndex :
|
||||
((i :
|
||||
((builtTrees :
|
||||
lazyList
|
||||
(_ : err errMissingNode t)
|
||||
(nodePayload rest :
|
||||
lazyResult
|
||||
(code after : err code after)
|
||||
(tree _ :
|
||||
lazyBool
|
||||
(_ : ok tree t)
|
||||
(_ :
|
||||
self
|
||||
rest
|
||||
(nodeBuildState
|
||||
nodeIndex
|
||||
(succ i)
|
||||
(pair (pair i tree) builtTrees)))
|
||||
(equal? i nodeIndex))
|
||||
(nodePayloadToTreeFromBuilt builtTrees nodePayload))
|
||||
remainingRecords)
|
||||
(nodeBuildStateBuiltTrees state)))
|
||||
(nodeBuildStateI state)))
|
||||
(nodeBuildStateTargetIndex state)))
|
||||
|
||||
nodeIndexToTree = (nodeRecords nodeIndex :
|
||||
y nodeIndexToTree_ nodeRecords (nodeBuildState nodeIndex 0 t))
|
||||
|
||||
readArboricxTreeFromIndex = (rootIndexBytes bs :
|
||||
bindResult (readArboricxNodesSection bs)
|
||||
(nodesSection afterContainer :
|
||||
bindResult (nodeIndexToTree (u32BEBytesToNat rootIndexBytes) (nodesSectionRecords nodesSection))
|
||||
bindResult (nodeIndexToTree (nodesSectionRecords nodesSection) (u32BEBytesToNat rootIndexBytes))
|
||||
(tree _ : ok tree afterContainer)))
|
||||
|
||||
readArboricxExecutableFromIndex = readArboricxTreeFromIndex
|
||||
|
||||
Reference in New Issue
Block a user