One structural fold serves semantic evaluators, use analysis and lowerings.
The value domain may differ from the literal word representation: reference
models use exact natural bit patterns, while a lowering uses typed fragments.
112def pointwiseFold =
113 (lambda erased word : Type 0 .
114 (lambda erased value : Type 0 .
115 (lambda erased inputs : Nat .
116 (lambda unrestricted unary : (pi unrestricted operation : (family PointwiseUnary) . (pi unrestricted x : value . value)) .
117 (lambda unrestricted binary : (pi unrestricted operation : (family PointwiseBinary) . (pi unrestricted x : value . (pi unrestricted y : value . value))) .
118 (lambda unrestricted literal : (pi unrestricted bits : word . value) .
119 (lambda unrestricted expression : (family PointwiseExpression word inputs) .
120 (lambda unrestricted values : (pi unrestricted index : (family StdFin inputs) . value) .
121 (eliminate
122 PointwiseExpression
123 (lambda unrestricted current : (family PointwiseExpression word inputs) . value)
124 expression
125 (branch PointwiseInput index . (values index))
126 (branch PointwiseConstant bits . (literal bits))
127 (branch
128 PointwiseUnaryExpression
129 operation
130 operand
131 result
132 .
133 (unary operation result))
134 (branch
135 PointwiseBinaryExpression
136 operation
137 left
138 right
139 leftResult
140 rightResult
141 .
142 (binary operation leftResult rightResult)))))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.