Package char-utf8-def: char-utf8-def

Information

Files

• Package tarball char-utf8-def-1.0.tgz
• Theory file char-utf8-def.thy (included in the package tarball)

Defined Constants

• Data
  • Char
    • UTF8
      • Data.Char.UTF8.decode
      • Data.Char.UTF8.decodeStream
      • Data.Char.UTF8.decoder
        • Data.Char.UTF8.decoder.decode1
        • Data.Char.UTF8.decoder.decode2
        • Data.Char.UTF8.decoder.decode3
        • Data.Char.UTF8.decoder.parse
      • Data.Char.UTF8.encode
      • Data.Char.UTF8.encoder
        • Data.Char.UTF8.encoder.encode1
        • Data.Char.UTF8.encoder.encode2
        • Data.Char.UTF8.encoder.encode3
      • Data.Char.UTF8.isContinuationByte
      • Data.Char.UTF8.parseContinuationByte
      • Data.Char.UTF8.parseThreeContinuationBytes
      • Data.Char.UTF8.parseTwoContinuationBytes

Theorems

⊦ Data.Char.UTF8.parseContinuationByte =
  Parser.parseSome Data.Char.UTF8.isContinuationByte

⊦ Data.Char.UTF8.decoder = Parser.mkParser Data.Char.UTF8.decoder.parse

⊦ Data.Char.UTF8.decodeStream = Parser.parseStream Data.Char.UTF8.decoder

⊦ Data.Char.UTF8.parseTwoContinuationBytes =
  Parser.parsePair Data.Char.UTF8.parseContinuationByte
    Data.Char.UTF8.parseContinuationByte

⊦ Data.Char.UTF8.parseThreeContinuationBytes =
  Parser.parsePair Data.Char.UTF8.parseContinuationByte
    Data.Char.UTF8.parseTwoContinuationBytes

⊦ ∀bs.
    Data.Char.UTF8.decode bs =
    Parser.Stream.toList
      (Data.Char.UTF8.decodeStream (Parser.Stream.fromList bs))

⊦ ∀chs.
    Data.Char.UTF8.encode chs =
    Data.List.concat (Data.List.map Data.Char.UTF8.encoder chs)

⊦ ∀b.
    Data.Char.UTF8.isContinuationByte b ⇔
    Data.Byte.bit b
      (Number.Numeral.bit1
         (Number.Numeral.bit1 (Number.Numeral.bit1 Number.Numeral.zero))) ∧
    ¬Data.Byte.bit b
        (Number.Numeral.bit0
           (Number.Numeral.bit1 (Number.Numeral.bit1 Number.Numeral.zero)))

⊦ ∀p0 p1.
    Data.Char.UTF8.encoder.encode1 p0 p1 =
    let
      (λb00.
         let
           (λb01.
              let
                (λb0.
                   let
                     (λb10.
                        let
                          (λb1.
                             Data.List.:: b0
                               (Data.List.:: b1 Data.List.[]))
                          (Data.Byte.or
                             (Data.Byte.fromNatural
                                (Number.Numeral.bit0
                                   (Number.Numeral.bit0
                                      (Number.Numeral.bit0
                                         (Number.Numeral.bit0
                                            (Number.Numeral.bit0
                                               (Number.Numeral.bit0
                                                  (Number.Numeral.bit0
                                                     (Number.Numeral.bit1
                                                        Number.Numeral.zero)))))))))
                             b10))
                     (Data.Byte.and p1
                        (Data.Byte.fromNatural
                           (Number.Numeral.bit1
                              (Number.Numeral.bit1
                                 (Number.Numeral.bit1
                                    (Number.Numeral.bit1
                                       (Number.Numeral.bit1
                                          (Number.Numeral.bit1
                                             Number.Numeral.zero)))))))))
                (Data.Byte.or
                   (Data.Byte.fromNatural
                      (Number.Numeral.bit0
                         (Number.Numeral.bit0
                            (Number.Numeral.bit0
                               (Number.Numeral.bit0
                                  (Number.Numeral.bit0
                                     (Number.Numeral.bit0
                                        (Number.Numeral.bit1
                                           (Number.Numeral.bit1
                                              Number.Numeral.zero)))))))))
                   (Data.Byte.or b00 b01)))
           (Data.Byte.shiftRight
              (Data.Byte.and p1
                 (Data.Byte.fromNatural
                    (Number.Numeral.bit0
                       (Number.Numeral.bit0
                          (Number.Numeral.bit0
                             (Number.Numeral.bit0
                                (Number.Numeral.bit0
                                   (Number.Numeral.bit0
                                      (Number.Numeral.bit1
                                         (Number.Numeral.bit1
                                            Number.Numeral.zero))))))))))
              (Number.Numeral.bit0
                 (Number.Numeral.bit1
                    (Number.Numeral.bit1 Number.Numeral.zero)))))
      (Data.Byte.shiftLeft p0
         (Number.Numeral.bit0 (Number.Numeral.bit1 Number.Numeral.zero)))

⊦ ∀ch.
    Data.Char.UTF8.encoder ch =
    let
      (λ(Data.Pair., pl pos).
         let
           (λp.
              let
                (λ(Data.Pair., p0 p1).
                   if p = Data.Byte.fromNatural Number.Numeral.zero
                   then (if p0 =
                    Data.Byte.fromNatural Number.Numeral.zero ∧
                    ¬Data.Byte.bit p1
                        (Number.Numeral.bit1
                           (Number.Numeral.bit1
                              (Number.Numeral.bit1 Number.Numeral.zero)))
                    then Data.List.:: p1 Data.List.[]
                    else if Data.Byte.and
                      (Data.Byte.fromNatural
                         (Number.Numeral.bit0
                            (Number.Numeral.bit0
                               (Number.Numeral.bit0
                                  (Number.Numeral.bit1
                                     (Number.Numeral.bit1
                                        (Number.Numeral.bit1
                                           (Number.Numeral.bit1
                                              (Number.Numeral.bit1
                                                 Number.Numeral.zero)))))))))
                      p0 = Data.Byte.fromNatural Number.Numeral.zero
                    then Data.Char.UTF8.encoder.encode1 p0 p1
                    else Data.Char.UTF8.encoder.encode2 p0 p1)
                   else Data.Char.UTF8.encoder.encode3 p p0 p1)
                (Data.Word16.toBytes (Data.Char.destPosition pos)))
           (Data.Char.destPlane pl)) (Data.Char.destChar ch)

⊦ ∀b0 s.
    Data.Char.UTF8.decoder.parse b0 s =
    (if Data.Byte.bit b0
       (Number.Numeral.bit1
          (Number.Numeral.bit1 (Number.Numeral.bit1 Number.Numeral.zero)))
     then (if Data.Byte.bit b0
        (Number.Numeral.bit0
           (Number.Numeral.bit1 (Number.Numeral.bit1 Number.Numeral.zero)))
      then (if Data.Byte.bit b0
         (Number.Numeral.bit1
            (Number.Numeral.bit0
               (Number.Numeral.bit1 Number.Numeral.zero)))
       then (if Data.Byte.bit b0
          (Number.Numeral.bit0
             (Number.Numeral.bit0
                (Number.Numeral.bit1 Number.Numeral.zero)))
        then (if Data.Byte.bit b0
           (Number.Numeral.bit1 (Number.Numeral.bit1 Number.Numeral.zero))
         then Data.Option.none
         else Parser.parse
           (Parser.partialMap (Data.Char.UTF8.decoder.decode3 b0)
              Data.Char.UTF8.parseThreeContinuationBytes) s)
        else Parser.parse
          (Parser.partialMap (Data.Char.UTF8.decoder.decode2 b0)
             Data.Char.UTF8.parseTwoContinuationBytes) s)
       else Parser.parse
         (Parser.partialMap (Data.Char.UTF8.decoder.decode1 b0)
            Data.Char.UTF8.parseContinuationByte) s) else Data.Option.none)
     else let
       (λpl.
          let
            (λpos.
               let (λch. Data.Option.some (Data.Pair., ch s))
                 (Data.Char.mkChar (Data.Pair., pl pos)))
            (Data.Char.mkPosition
               (Data.Word16.fromBytes
                  (Data.Byte.fromNatural Number.Numeral.zero) b0)))
       (Data.Char.mkPlane (Data.Byte.fromNatural Number.Numeral.zero)))

⊦ ∀b0 b1.
    Data.Char.UTF8.decoder.decode1 b0 b1 =
    let
      (λpl.
         let
           (λp0.
              let
                (λy1.
                   let
                     (λx1.
                        let
                          (λp1.
                             if p0 =
                             Data.Byte.fromNatural Number.Numeral.zero ∧
                             Data.Byte.< p1
                               (Data.Byte.fromNatural
                                  (Number.Numeral.bit0
                                     (Number.Numeral.bit0
                                        (Number.Numeral.bit0
                                           (Number.Numeral.bit0
                                              (Number.Numeral.bit0
                                                 (Number.Numeral.bit0
                                                    (Number.Numeral.bit0
                                                       (Number.Numeral.bit1
                                                          Number.Numeral.zero)))))))))
                             then Data.Option.none
                             else let
                               (λpos.
                                  let (λch. Data.Option.some ch)
                                    (Data.Char.mkChar
                                       (Data.Pair., pl pos)))
                               (Data.Char.mkPosition
                                  (Data.Word16.fromBytes p0 p1)))
                          (Data.Byte.or y1 x1))
                     (Data.Byte.and b1
                        (Data.Byte.fromNatural
                           (Number.Numeral.bit1
                              (Number.Numeral.bit1
                                 (Number.Numeral.bit1
                                    (Number.Numeral.bit1
                                       (Number.Numeral.bit1
                                          (Number.Numeral.bit1
                                             Number.Numeral.zero)))))))))
                (Data.Byte.shiftLeft
                   (Data.Byte.and b0
                      (Data.Byte.fromNatural
                         (Number.Numeral.bit1
                            (Number.Numeral.bit1 Number.Numeral.zero))))
                   (Number.Numeral.bit0
                      (Number.Numeral.bit1
                         (Number.Numeral.bit1 Number.Numeral.zero)))))
           (Data.Byte.shiftRight
              (Data.Byte.and b0
                 (Data.Byte.fromNatural
                    (Number.Numeral.bit0
                       (Number.Numeral.bit0
                          (Number.Numeral.bit1
                             (Number.Numeral.bit1
                                (Number.Numeral.bit1
                                   Number.Numeral.zero)))))))
              (Number.Numeral.bit0
                 (Number.Numeral.bit1 Number.Numeral.zero))))
      (Data.Char.mkPlane (Data.Byte.fromNatural Number.Numeral.zero))

⊦ ∀p0 p1.
    Data.Char.UTF8.encoder.encode2 p0 p1 =
    let
      (λb00.
         let
           (λb0.
              let
                (λb10.
                   let
                     (λb11.
                        let
                          (λb1.
                             let
                               (λb20.
                                  let
                                    (λb2.
                                       Data.List.:: b0
                                         (Data.List.:: b1
                                            (Data.List.:: b2
                                               Data.List.[])))
                                    (Data.Byte.or
                                       (Data.Byte.fromNatural
                                          (Number.Numeral.bit0
                                             (Number.Numeral.bit0
                                                (Number.Numeral.bit0
                                                   (Number.Numeral.bit0
                                                      (Number.Numeral.bit0
                                                         (Number.Numeral.bit0
                                                            (Number.Numeral.bit0
                                                               (Number.Numeral.bit1
                                                                  Number.Numeral.zero)))))))))
                                       b20))
                               (Data.Byte.and p1
                                  (Data.Byte.fromNatural
                                     (Number.Numeral.bit1
                                        (Number.Numeral.bit1
                                           (Number.Numeral.bit1
                                              (Number.Numeral.bit1
                                                 (Number.Numeral.bit1
                                                    (Number.Numeral.bit1
                                                       Number.Numeral.zero)))))))))
                          (Data.Byte.or
                             (Data.Byte.fromNatural
                                (Number.Numeral.bit0
                                   (Number.Numeral.bit0
                                      (Number.Numeral.bit0
                                         (Number.Numeral.bit0
                                            (Number.Numeral.bit0
                                               (Number.Numeral.bit0
                                                  (Number.Numeral.bit0
                                                     (Number.Numeral.bit1
                                                        Number.Numeral.zero)))))))))
                             (Data.Byte.or b10 b11)))
                     (Data.Byte.shiftRight
                        (Data.Byte.and p1
                           (Data.Byte.fromNatural
                              (Number.Numeral.bit0
                                 (Number.Numeral.bit0
                                    (Number.Numeral.bit0
                                       (Number.Numeral.bit0
                                          (Number.Numeral.bit0
                                             (Number.Numeral.bit0
                                                (Number.Numeral.bit1
                                                   (Number.Numeral.bit1
                                                      Number.Numeral.zero))))))))))
                        (Number.Numeral.bit0
                           (Number.Numeral.bit1
                              (Number.Numeral.bit1 Number.Numeral.zero)))))
                (Data.Byte.shiftLeft
                   (Data.Byte.and p0
                      (Data.Byte.fromNatural
                         (Number.Numeral.bit1
                            (Number.Numeral.bit1
                               (Number.Numeral.bit1
                                  (Number.Numeral.bit1
                                     Number.Numeral.zero))))))
                   (Number.Numeral.bit0
                      (Number.Numeral.bit1 Number.Numeral.zero))))
           (Data.Byte.or
              (Data.Byte.fromNatural
                 (Number.Numeral.bit0
                    (Number.Numeral.bit0
                       (Number.Numeral.bit0
                          (Number.Numeral.bit0
                             (Number.Numeral.bit0
                                (Number.Numeral.bit1
                                   (Number.Numeral.bit1
                                      (Number.Numeral.bit1
                                         Number.Numeral.zero))))))))) b00))
      (Data.Byte.shiftRight
         (Data.Byte.and p0
            (Data.Byte.fromNatural
               (Number.Numeral.bit0
                  (Number.Numeral.bit0
                     (Number.Numeral.bit0
                        (Number.Numeral.bit0
                           (Number.Numeral.bit1
                              (Number.Numeral.bit1
                                 (Number.Numeral.bit1
                                    (Number.Numeral.bit1
                                       Number.Numeral.zero))))))))))
         (Number.Numeral.bit0
            (Number.Numeral.bit0
               (Number.Numeral.bit1 Number.Numeral.zero))))

⊦ ∀b0 b1 b2 b3.
    Data.Char.UTF8.decoder.decode3 b0
      (Data.Pair., b1 (Data.Pair., b2 b3)) =
    let
      (λw.
         let
           (λz.
              let
                (λp.
                   if p = Data.Byte.fromNatural Number.Numeral.zero ∨
                   Data.Byte.<
                     (Data.Byte.fromNatural
                        (Number.Numeral.bit0
                           (Number.Numeral.bit0
                              (Number.Numeral.bit0
                                 (Number.Numeral.bit0
                                    (Number.Numeral.bit1
                                       Number.Numeral.zero)))))) p
                   then Data.Option.none
                   else let
                     (λpl.
                        let
                          (λz0.
                             let
                               (λy0.
                                  let
                                    (λp0.
                                       let
                                         (λy1.
                                            let
                                              (λx1.
                                                 let
                                                   (λp1.
                                                      let
                                                        (λpos.
                                                           let
                                                             (λch.
                                                                Data.Option.some
                                                                  ch)
                                                             (Data.Char.mkChar
                                                                (Data.Pair.,
                                                                   pl
                                                                   pos)))
                                                        (Data.Char.mkPosition
                                                           (Data.Word16.fromBytes
                                                              p0 p1)))
                                                   (Data.Byte.or y1 x1))
                                              (Data.Byte.and b3
                                                 (Data.Byte.fromNatural
                                                    (Number.Numeral.bit1
                                                       (Number.Numeral.bit1
                                                          (Number.Numeral.bit1
                                                             (Number.Numeral.bit1
                                                                (Number.Numeral.bit1
                                                                   (Number.Numeral.bit1
                                                                      Number.Numeral.zero)))))))))
                                         (Data.Byte.shiftLeft
                                            (Data.Byte.and b2
                                               (Data.Byte.fromNatural
                                                  (Number.Numeral.bit1
                                                     (Number.Numeral.bit1
                                                        Number.Numeral.zero))))
                                            (Number.Numeral.bit0
                                               (Number.Numeral.bit1
                                                  (Number.Numeral.bit1
                                                     Number.Numeral.zero)))))
                                    (Data.Byte.or z0 y0))
                               (Data.Byte.shiftRight
                                  (Data.Byte.and b2
                                     (Data.Byte.fromNatural
                                        (Number.Numeral.bit0
                                           (Number.Numeral.bit0
                                              (Number.Numeral.bit1
                                                 (Number.Numeral.bit1
                                                    (Number.Numeral.bit1
                                                       (Number.Numeral.bit1
                                                          Number.Numeral.zero))))))))
                                  (Number.Numeral.bit0
                                     (Number.Numeral.bit1
                                        Number.Numeral.zero))))
                          (Data.Byte.shiftLeft
                             (Data.Byte.and b1
                                (Data.Byte.fromNatural
                                   (Number.Numeral.bit1
                                      (Number.Numeral.bit1
                                         (Number.Numeral.bit1
                                            (Number.Numeral.bit1
                                               Number.Numeral.zero))))))
                             (Number.Numeral.bit0
                                (Number.Numeral.bit0
                                   (Number.Numeral.bit1
                                      Number.Numeral.zero)))))
                     (Data.Char.mkPlane p)) (Data.Byte.or w z))
           (Data.Byte.shiftRight
              (Data.Byte.and b1
                 (Data.Byte.fromNatural
                    (Number.Numeral.bit0
                       (Number.Numeral.bit0
                          (Number.Numeral.bit0
                             (Number.Numeral.bit0
                                (Number.Numeral.bit1
                                   (Number.Numeral.bit1
                                      Number.Numeral.zero))))))))
              (Number.Numeral.bit0
                 (Number.Numeral.bit0
                    (Number.Numeral.bit1 Number.Numeral.zero)))))
      (Data.Byte.shiftLeft
         (Data.Byte.and b0
            (Data.Byte.fromNatural
               (Number.Numeral.bit1
                  (Number.Numeral.bit1
                     (Number.Numeral.bit1 Number.Numeral.zero)))))
         (Number.Numeral.bit0 (Number.Numeral.bit1 Number.Numeral.zero)))

⊦ ∀b0 b1 b2.
    Data.Char.UTF8.decoder.decode2 b0 (Data.Pair., b1 b2) =
    let
      (λz0.
         let
           (λy0.
              let
                (λp0.
                   if Data.Byte.< p0
                     (Data.Byte.fromNatural
                        (Number.Numeral.bit0
                           (Number.Numeral.bit0
                              (Number.Numeral.bit0
                                 (Number.Numeral.bit1
                                    Number.Numeral.zero))))) ∨
                   Data.Byte.≤
                     (Data.Byte.fromNatural
                        (Number.Numeral.bit0
                           (Number.Numeral.bit0
                              (Number.Numeral.bit0
                                 (Number.Numeral.bit1
                                    (Number.Numeral.bit1
                                       (Number.Numeral.bit0
                                          (Number.Numeral.bit1
                                             (Number.Numeral.bit1
                                                Number.Numeral.zero)))))))))
                     p0 ∧
                   Data.Byte.≤ p0
                     (Data.Byte.fromNatural
                        (Number.Numeral.bit1
                           (Number.Numeral.bit1
                              (Number.Numeral.bit1
                                 (Number.Numeral.bit1
                                    (Number.Numeral.bit1
                                       (Number.Numeral.bit0
                                          (Number.Numeral.bit1
                                             (Number.Numeral.bit1
                                                Number.Numeral.zero)))))))))
                   then Data.Option.none
                   else let
                     (λy1.
                        let
                          (λx1.
                             let
                               (λp1.
                                  if p0 =
                                  Data.Byte.fromNatural
                                    (Number.Numeral.bit1
                                       (Number.Numeral.bit1
                                          (Number.Numeral.bit1
                                             (Number.Numeral.bit1
                                                (Number.Numeral.bit1
                                                   (Number.Numeral.bit1
                                                      (Number.Numeral.bit1
                                                         (Number.Numeral.bit1
                                                            Number.Numeral.zero)))))))) ∧
                                  Data.Byte.≤
                                    (Data.Byte.fromNatural
                                       (Number.Numeral.bit0
                                          (Number.Numeral.bit1
                                             (Number.Numeral.bit1
                                                (Number.Numeral.bit1
                                                   (Number.Numeral.bit1
                                                      (Number.Numeral.bit1
                                                         (Number.Numeral.bit1
                                                            (Number.Numeral.bit1
                                                               Number.Numeral.zero)))))))))
                                    p1 then Data.Option.none
                                  else let
                                    (λpl.
                                       let
                                         (λpos.
                                            let (λch. Data.Option.some ch)
                                              (Data.Char.mkChar
                                                 (Data.Pair., pl pos)))
                                         (Data.Char.mkPosition
                                            (Data.Word16.fromBytes p0 p1)))
                                    (Data.Char.mkPlane
                                       (Data.Byte.fromNatural
                                          Number.Numeral.zero)))
                               (Data.Byte.or y1 x1))
                          (Data.Byte.and b2
                             (Data.Byte.fromNatural
                                (Number.Numeral.bit1
                                   (Number.Numeral.bit1
                                      (Number.Numeral.bit1
                                         (Number.Numeral.bit1
                                            (Number.Numeral.bit1
                                               (Number.Numeral.bit1
                                                  Number.Numeral.zero)))))))))
                     (Data.Byte.shiftLeft
                        (Data.Byte.and b1
                           (Data.Byte.fromNatural
                              (Number.Numeral.bit1
                                 (Number.Numeral.bit1
                                    Number.Numeral.zero))))
                        (Number.Numeral.bit0
                           (Number.Numeral.bit1
                              (Number.Numeral.bit1 Number.Numeral.zero)))))
                (Data.Byte.or z0 y0))
           (Data.Byte.shiftRight
              (Data.Byte.and b1
                 (Data.Byte.fromNatural
                    (Number.Numeral.bit0
                       (Number.Numeral.bit0
                          (Number.Numeral.bit1
                             (Number.Numeral.bit1
                                (Number.Numeral.bit1
                                   (Number.Numeral.bit1
                                      Number.Numeral.zero))))))))
              (Number.Numeral.bit0
                 (Number.Numeral.bit1 Number.Numeral.zero))))
      (Data.Byte.shiftLeft
         (Data.Byte.and b0
            (Data.Byte.fromNatural
               (Number.Numeral.bit1
                  (Number.Numeral.bit1
                     (Number.Numeral.bit1
                        (Number.Numeral.bit1 Number.Numeral.zero))))))
         (Number.Numeral.bit0
            (Number.Numeral.bit0
               (Number.Numeral.bit1 Number.Numeral.zero))))

⊦ ∀p p0 p1.
    Data.Char.UTF8.encoder.encode3 p p0 p1 =
    let
      (λb00.
         let
           (λb0.
              let
                (λb10.
                   let
                     (λb11.
                        let
                          (λb1.
                             let
                               (λb20.
                                  let
                                    (λb21.
                                       let
                                         (λb2.
                                            let
                                              (λb30.
                                                 let
                                                   (λb3.
                                                      Data.List.:: b0
                                                        (Data.List.:: b1
                                                           (Data.List.:: b2
                                                              (Data.List.::
                                                                 b3
                                                                 Data.List.[]))))
                                                   (Data.Byte.or
                                                      (Data.Byte.fromNatural
                                                         (Number.Numeral.bit0
                                                            (Number.Numeral.bit0
                                                               (Number.Numeral.bit0
                                                                  (Number.Numeral.bit0
                                                                     (Number.Numeral.bit0
                                                                        (Number.Numeral.bit0
                                                                           (Number.Numeral.bit0
                                                                              (Number.Numeral.bit1
                                                                                 Number.Numeral.zero)))))))))
                                                      b30))
                                              (Data.Byte.and p1
                                                 (Data.Byte.fromNatural
                                                    (Number.Numeral.bit1
                                                       (Number.Numeral.bit1
                                                          (Number.Numeral.bit1
                                                             (Number.Numeral.bit1
                                                                (Number.Numeral.bit1
                                                                   (Number.Numeral.bit1
                                                                      Number.Numeral.zero)))))))))
                                         (Data.Byte.or
                                            (Data.Byte.fromNatural
                                               (Number.Numeral.bit0
                                                  (Number.Numeral.bit0
                                                     (Number.Numeral.bit0
                                                        (Number.Numeral.bit0
                                                           (Number.Numeral.bit0
                                                              (Number.Numeral.bit0
                                                                 (Number.Numeral.bit0
                                                                    (Number.Numeral.bit1
                                                                       Number.Numeral.zero)))))))))
                                            (Data.Byte.or b20 b21)))
                                    (Data.Byte.shiftRight
                                       (Data.Byte.and p1
                                          (Data.Byte.fromNatural
                                             (Number.Numeral.bit0
                                                (Number.Numeral.bit0
                                                   (Number.Numeral.bit0
                                                      (Number.Numeral.bit0
                                                         (Number.Numeral.bit0
                                                            (Number.Numeral.bit0
                                                               (Number.Numeral.bit1
                                                                  (Number.Numeral.bit1
                                                                     Number.Numeral.zero))))))))))
                                       (Number.Numeral.bit0
                                          (Number.Numeral.bit1
                                             (Number.Numeral.bit1
                                                Number.Numeral.zero)))))
                               (Data.Byte.shiftLeft
                                  (Data.Byte.and p0
                                     (Data.Byte.fromNatural
                                        (Number.Numeral.bit1
                                           (Number.Numeral.bit1
                                              (Number.Numeral.bit1
                                                 (Number.Numeral.bit1
                                                    Number.Numeral.zero))))))
                                  (Number.Numeral.bit0
                                     (Number.Numeral.bit1
                                        Number.Numeral.zero))))
                          (Data.Byte.or
                             (Data.Byte.fromNatural
                                (Number.Numeral.bit0
                                   (Number.Numeral.bit0
                                      (Number.Numeral.bit0
                                         (Number.Numeral.bit0
                                            (Number.Numeral.bit0
                                               (Number.Numeral.bit0
                                                  (Number.Numeral.bit0
                                                     (Number.Numeral.bit1
                                                        Number.Numeral.zero)))))))))
                             (Data.Byte.or b10 b11)))
                     (Data.Byte.shiftRight
                        (Data.Byte.and p0
                           (Data.Byte.fromNatural
                              (Number.Numeral.bit0
                                 (Number.Numeral.bit0
                                    (Number.Numeral.bit0
                                       (Number.Numeral.bit0
                                          (Number.Numeral.bit1
                                             (Number.Numeral.bit1
                                                (Number.Numeral.bit1
                                                   (Number.Numeral.bit1
                                                      Number.Numeral.zero))))))))))
                        (Number.Numeral.bit0
                           (Number.Numeral.bit0
                              (Number.Numeral.bit1 Number.Numeral.zero)))))
                (Data.Byte.shiftLeft
                   (Data.Byte.and p
                      (Data.Byte.fromNatural
                         (Number.Numeral.bit1
                            (Number.Numeral.bit1 Number.Numeral.zero))))
                   (Number.Numeral.bit0
                      (Number.Numeral.bit0
                         (Number.Numeral.bit1 Number.Numeral.zero)))))
           (Data.Byte.or
              (Data.Byte.fromNatural
                 (Number.Numeral.bit0
                    (Number.Numeral.bit0
                       (Number.Numeral.bit0
                          (Number.Numeral.bit0
                             (Number.Numeral.bit1
                                (Number.Numeral.bit1
                                   (Number.Numeral.bit1
                                      (Number.Numeral.bit1
                                         Number.Numeral.zero))))))))) b00))
      (Data.Byte.shiftRight
         (Data.Byte.and p
            (Data.Byte.fromNatural
               (Number.Numeral.bit0
                  (Number.Numeral.bit0
                     (Number.Numeral.bit1
                        (Number.Numeral.bit1
                           (Number.Numeral.bit1 Number.Numeral.zero)))))))
         (Number.Numeral.bit0 (Number.Numeral.bit1 Number.Numeral.zero)))

Input Type Operators

• →
• bool
• Data
  • Byte
    • Data.Byte.byte
  • Char
    • Data.Char.char
    • Data.Char.plane
    • Data.Char.position
  • List
    • Data.List.list
  • Option
    • Data.Option.option
  • Pair
    • Data.Pair.*
  • Word16
    • Data.Word16.word16
• Number
  • Natural
    • Number.Natural.natural
• Parser
  • Parser.parser
  • Stream
    • Parser.Stream.stream

Input Constants

• =
• Data
  • Bool
    • ∀
    • ∧
    • ⇒
    • ∨
    • ¬
    • cond
    • let
    • select
    • T
  • Byte
    • Data.Byte.<
    • Data.Byte.≤
    • Data.Byte.and
    • Data.Byte.bit
    • Data.Byte.fromNatural
    • Data.Byte.or
    • Data.Byte.shiftLeft
    • Data.Byte.shiftRight
  • Char
    • Data.Char.destChar
    • Data.Char.destPlane
    • Data.Char.destPosition
    • Data.Char.mkChar
    • Data.Char.mkPlane
    • Data.Char.mkPosition
  • List
    • Data.List.::
    • Data.List.[]
    • Data.List.concat
    • Data.List.map
  • Option
    • Data.Option.none
    • Data.Option.some
  • Pair
    • Data.Pair.,
    • Data.Pair.fst
    • Data.Pair.snd
  • Word16
    • Data.Word16.fromBytes
    • Data.Word16.toBytes
• Number
  • Numeral
    • Number.Numeral.bit0
    • Number.Numeral.bit1
    • Number.Numeral.zero
• Parser
  • Parser.mkParser
  • Parser.parse
  • Parser.parsePair
  • Parser.parseSome
  • Parser.parseStream
  • Parser.partialMap
  • Stream
    • Parser.Stream.fromList
    • Parser.Stream.toList

Assumptions

⊦ T

⊦ (∀) = λP. P = λx. T

⊦ (⇒) = λp q. p ∧ q ⇔ p

⊦ ∀x y. Data.Pair.fst (Data.Pair., x y) = x

⊦ ∀x y. Data.Pair.snd (Data.Pair., x y) = y

⊦ (∧) = λp q. (λf. f p q) = λf. f T T