Component.Pointwise

236def pointwiseProgramEvaluate =
237  (lambda erased word : Type 0 .
238    (lambda erased value : Type 0 .
239      (lambda erased inputs : Nat .
240        (lambda unrestricted unary : (pi unrestricted operation : (family PointwiseUnary) . (pi unrestricted x : value . value)) .
241          (lambda unrestricted binary : (pi unrestricted operation : (family PointwiseBinary) . (pi unrestricted x : value . (pi unrestricted y : value . value))) .
242            (lambda unrestricted literal : (pi unrestricted bits : word . value) .
243              (lambda unrestricted program : (family StdList (family PointwiseAssignment word inputs)) .
244                (eliminate
245                  StdList
246                  (lambda unrestricted current : (family StdList (family PointwiseAssignment word inputs)) .
247                    (pi unrestricted state : (pi unrestricted index : (family StdFin inputs) . value) .
248                      (pi unrestricted index : (family StdFin inputs) . value)))
249                  program
250                  (branch
251                    StdListEmpty
252                    .
253                    (lambda unrestricted state : (pi unrestricted index : (family StdFin inputs) . value) .
254                      state))
255                  (branch
256                    StdListCons
257                    head
258                    tail
259                    next
260                    .
261                    (lambda unrestricted state : (pi unrestricted index : (family StdFin inputs) . value) .
262                      (eliminate
263                        PointwiseAssignment
264                        (lambda unrestricted current : (family PointwiseAssignment word inputs) .
265                          (pi unrestricted index : (family StdFin inputs) . value))
266                        head
267                        (branch
268                          PointwiseAssign
269                          destination
270                          expression
271                          .
272                          (let unrestricted result =
273                            (pointwiseFold word value inputs unary binary literal expression state)
274                            in
275                            (next
276                              (lambda unrestricted index : (family StdFin inputs) .
277                                (nat-eliminate
278                                  (lambda unrestricted same : Nat . value)
279                                  (state index)
280                                  (lambda unrestricted previous : Nat .
281                                    (lambda unrestricted ignored : value . result))
282                                  (naturalEqual
283                                    (stdFinToNatural inputs destination)
284                                    (stdFinToNatural inputs index))))))))))))))))))