The Coq mailing list

[Christoph-Simon Senjak <christoph.senjak AT ifi.lmu.de>]

Hello.

I am using the current trunk (db8e0d7ecaf233ae73705d2f57635a38f8825dad). 
My overall project can be found under 
https://github.com/dasuxullebt/deflate/, I updated the file 
"InflateUnverified.v", I attached here.

When I come to its last line, I get an error "The reference inflate was 
not found in the current environment". When I remove everything inside 
the "inflate" function, and only leave the (commented) catch-all 
pattern, it works.

(Originally I wanted to do recursive extraction, which failed with the 
same error.)

Best Regards
Christoph-Simon Senjak
Require Import Coq.QArith.QArith_base.
Require Import Coq.QArith.QArith.
Require Import Coq.QArith.Qfield.
Require Import Omega.
Require Import Recdef.
Require Import Program.
Require Import Coq.Arith.Euclid.
Require Import Coq.Lists.List.
Require Import DeflateNotations.
Require Import Lex.
Require Import Transports.
Require Import Prefix.
Require Import Repeat.
Require Import Combi.
Require Import KraftList.
Require Import KraftVec.
Require Import DeflateCoding.

Open Scope nat_scope.

Fixpoint xrepeat {A : Set} (n : nat) (a : A) :=
  match n with
    | 0 => nil
    | (S n') => a :: xrepeat n' a
  end.

Inductive BackBufferBase (A : Set) : Set :=
| bbnil : BackBufferBase A
| bbcons1 : A -> BackBufferBase (A * A)%type -> BackBufferBase A
| bbcons2 : A -> A -> BackBufferBase (A * A)%type -> BackBufferBase A.

Record BackBufferWithLength (A : Set) : Set :=
  mkBackBufferWithLength {
      l : nat ;
      buffer : BackBufferBase A
    }.

Fixpoint bbbcons {A : Set} (x : A) (bbb : BackBufferBase A) : BackBufferBase A :=
  match bbb with
    | bbnil _ => bbcons1 A x (bbnil (A * A)%type)
    | bbcons1 _ a bb => bbcons2 A x a bb
    | bbcons2 _ a b bb => bbcons1 A x (bbbcons (a, b) bb)
  end.

Function bbwlcons {A : Set} (x : A) (bbwl : BackBufferWithLength A) : BackBufferWithLength A :=
  mkBackBufferWithLength A (S (l A bbwl)) (bbbcons x (buffer A bbwl)).

Lemma bbbget {A : Set} (nn : nat) (bbbb : BackBufferBase A) : option A.
  refine
    ((fix rec (B : Set) (bbb : BackBufferBase B) (n : nat) : option B :=
       match bbb with
         | bbnil _ => error
         | bbcons1 _ a bb =>
           match n with
             | 0 => value a
             | (S n') =>
               match (eucl_dev 2 _ n') with
                 | divex _ _ q r _ _ =>
                   option_map  (match r with
                                  | 0 => fst
                                  | _ => snd
                                end) (rec (B * B)%type bb q)
               end
           end
         | bbcons2 _ a b bb =>
           match n with
             | 0 => value a
             | 1 => value b
             | (S (S n')) =>
               match (eucl_dev 2 _ n') with
                 | divex _ _ q r _ _ =>
                   option_map  (match r with
                                  | 0 => fst
                                  | _ => snd
                                end) (rec (B * B)%type bb q) 
               end
           end
       end) A bbbb nn).
  omega.
  omega.
Defined.

Function bbwlget {A : Set} (n : nat) (bbwl : BackBufferWithLength A) : option A :=
  match (Compare_dec.lt_dec n (l A bbwl)) with (* this is for efficiency *)
    | left _ => bbbget n (buffer A bbwl)
    | right _ => error
  end.

Record BackBuffer (A : Set) : Set :=
  mkBackBuffer {
      length : nat ;
      topbuf : BackBufferWithLength A ;
      botbuf : BackBufferWithLength A
    }.

Function bbcons {A : Set} (x : A) (bb : BackBuffer A) : BackBuffer A :=
  match Compare_dec.le_dec (l A (topbuf A bb)) (length A bb) with
    | left _ => mkBackBuffer A (length A bb) (bbwlcons x (topbuf A bb)) (botbuf A bb)
    | right _ => mkBackBuffer (* move topbuffer to bottom, drop botbuffer, start new buffer *)
                   A
                   (length A bb)
                   (mkBackBufferWithLength A 1
                                           (bbcons1 A x (bbnil (A * A)%type)))
                   (topbuf A bb)
  end.

Function bbget {A : Set} (n : nat) (bb : BackBuffer A) : option A :=
  match Compare_dec.le_dec n (length A bb) with
    | left _ =>
      match (bbwlget n (topbuf A bb)) with
        | Some a => value a
        | None => bbwlget (n - (l A (topbuf A bb))) (botbuf A bb)
      end
    | right _ => error
  end.

Inductive BitByteList : Set :=
  | BBLNil : BitByteList
  | BBLConsBit : bool -> BitByteList -> BitByteList
  | BBLConsByte : Byte -> BitByteList -> BitByteList -> BitByteList.

Fixpoint bbllength (bbl : BitByteList) : nat :=
  match bbl with
    | BBLNil => 0
    | BBLConsBit _ bb => S (bbllength bb)
    | BBLConsByte _ bb _ => bbllength bb
  end.

(* this function requires laziness *)
Fixpoint LByteToBBL (lb : LByte) :  BitByteList :=
  match lb with
    | nil => BBLNil
    | (x :: L) =>
      let next := (LByteToBBL L) in
      BBLConsByte x
                  ((fix f b c :=
                    match b with
                      | nil => c
                      | (bb :: bbb) => BBLConsBit bb (f bbb c)
                    end) (rev (VectorDef.to_list x)) next) next
  end.

Fixpoint nextBit (BBL : BitByteList) : option (bool * BitByteList) :=
  match BBL with
    | BBLNil => None
    | BBLConsBit bit bb => Some (bit, bb)
    | BBLConsByte _ bb _ => nextBit bb
  end.

Fixpoint nBits (BBL : BitByteList) (n : nat) : option (LB * BitByteList) :=
  match n with
    | 0 => Some (nil, BBL)
    | (S n) => match nextBit BBL with
                 | None => None
                 | Some (bit, rest) =>
                   option_map (fun x => (bit :: fst x, snd x)) (nBits rest n)
               end
  end.

Fixpoint lsbToInt (l : LB) : nat :=
  match l with
    | nil => 0
    | false :: R => 2 * (lsbToInt R)
    | true :: R => S (2 * (lsbToInt R))
  end.

Function nBitsToInt (BBL : BitByteList) (n : nat) : option (nat * BitByteList) :=
  match (nBits BBL n) with
    | None => None
    | Some (bits, rest) => Some (lsbToInt bits, rest)
  end.

Definition StreamEndedEarly := 1.
Definition WrongBlockHeader := 2.

Fixpoint isneg (a b : LB) : bool :=
  match (a, b) with
    | (nil, nil) => true
    | (false :: L1, true :: L2) => isneg L1 L2
    | (true :: L1, false :: L2) => isneg L1 L2
    | _ => false
  end.               

Definition clcOrder := Vector.of_list (16 :: 17 :: 18 :: 0 :: 8 :: 7 :: 9 :: 6 :: 10 :: 5 :: 11 :: 4 :: 12 :: 3 :: 13 :: 2 :: 14 :: 1 :: 15 :: nil).

Function clcLensToVec (l : list nat) : (vec nat 19) :=
  Vmap (fun x : nat => (nth x l 0)) clcOrder.

Fixpoint clcBitsSplice (m : LB) : list nat :=
  match m with
    | (a :: (b :: (c :: R))) => (lsbToInt (a :: b :: c :: nil)) :: (clcBitsSplice R)
    | _ => nil
  end.

Function clcBitsToVec (l : LB) : (vec nat 19) :=
  clcLensToVec (clcBitsSplice l).


Function MayBeCoding {alpha : nat} (lens : vec nat alpha) : option deflateCoding :=
  match Qlt_le_dec 1%Q (kraft_nvec lens) with
    | left _ => None
    | right krafteq =>
      Some (proj1_sig (existence alpha lens krafteq))
  end.

Function StartsWith (prefix : LB) (input : BitByteList) : option BitByteList :=
  match prefix with
    | nil => Some input
    | (x :: L) =>
      match (x, (nextBit input)) with
        | (true, Some (true, rest)) => StartsWith L rest
        | (false, Some (false, rest)) => StartsWith L rest
        | _ => None
      end
  end.

SearchAbout le.

Function ReadCode (d : deflateCoding) (input : BitByteList) : option (nat * BitByteList) :=
  match fold (0, None)
             (fun x y => match x with
                           | (n, None) =>
                             match y with
                               | (_, None) => ((S n), None)
                               | (_, Some bbl) => (n, Some bbl)
                             end
                           | _ => x
                         end)
             (Vmap (fun x => (0, StartsWith x input)) (C d)) with
    | (_, None) => None
    | (n, Some bbl) => Some (n, bbl)
  end.

Lemma nat2byte {n : nat} : (n <= 255) -> Byte.
Admitted.

Definition lenCodeBitNumAndBase : list (nat * nat) := 
  (0, 3) :: (0, 4) :: (0, 5) :: (0, 6) ::  (0, 7) :: (0, 8) :: (0, 9) :: (0, 10) ::
         (1, 11) :: (1, 13) :: (1, 15) :: (1, 17) :: (2, 19) :: (2, 23) :: (2, 27) ::
         (2, 31) :: (3, 35) :: (3, 43) :: (3, 51) :: (3, 59) :: (4, 67) :: (4, 83) ::
         (4, 99) :: (4, 115) :: (5, 131) :: (5, 163) :: (5, 195) :: (5, 227) :: (0, 258) :: nil.

Definition distCodeBitNumAndBase : list (nat * nat) :=
  (0, 1) :: (0, 2) :: (0, 3) :: (0, 4) :: (1, 5) :: (1, 7) :: (2, 9) :: (2, 13) ::
         (3, 17) :: (3, 25) :: (4, 33) :: (4, 49) :: (5, 65) :: (5, 97) :: (6, 129) ::
         (6, 193) :: (7, 257) :: (7, 385) :: (8, 513) :: (8, 769) :: (9, 1025) ::
         (9, 1537) :: (10, 2049) :: (10, 3073) :: (11, 4097) :: (11, 6145) :: (12, 8193) ::
         (12, 12289) :: (13, 16385) :: (13, 24577) :: nil.

Definition vector_for_fixed_litlen_codes : vec nat 288 := Vector.of_list ((xrepeat 144 8) ++ (xrepeat (255 - 143) 9) ++ (xrepeat (279 - 255) 7) ++ (xrepeat (287 - 279) 8)).

Definition fixed_litlen_coding_exists : { D : deflateCoding | {eq : M D = 288 |
                                                               vector_for_fixed_litlen_codes =
                                                               (Vmap (ll(A:=bool)) (vec_id(A:=LB) eq (C D)))}}.
Proof.
apply existence.
compute.
intros Q.
inversion Q.
Defined.

Definition fixed_litlen_coding := proj1_sig fixed_litlen_coding_exists.

Definition fixed_dist_coding_exists : { D : deflateCoding | {eq : M D = 30 |
                                        (Vector.of_list (xrepeat 30 5)) = (Vmap (ll(A:=bool)) (vec_id(A:=LB) eq (C D)))}}.
Proof.
  apply existence.
  compute.
  intros Q.
  inversion Q.
Defined.

Definition fixed_dist_coding := proj1_sig fixed_dist_coding_exists.


Inductive CoqCantIntoMutualRecursion : Set :=
| Start : CoqCantIntoMutualRecursion
| BlockParse : bool -> CoqCantIntoMutualRecursion
| UncompressedBlockParse : bool -> CoqCantIntoMutualRecursion
| UncompressedBlockPass : nat -> bool -> CoqCantIntoMutualRecursion
| DynamicallyCompressedBlockParse : bool -> CoqCantIntoMutualRecursion
| StaticallyCompressedBlockParse : bool -> CoqCantIntoMutualRecursion
| DynamicallyCompressedBlockCodeLengtCode : bool -> nat -> nat -> nat -> CoqCantIntoMutualRecursion (* hlit hdist hclen *)
| DynamicallyCompressedBlockCodeLengths : bool -> (list nat) -> nat -> nat -> nat -> deflateCoding -> CoqCantIntoMutualRecursion (* lengths remaining hlit hdist code-length-coding *)
| DynamicallyCompressedLit : bool -> list nat -> list nat -> nat -> nat -> CoqCantIntoMutualRecursion (* allcodes litcodes hlit-remaining hdist *)
| CompressedBlock : bool -> deflateCoding -> deflateCoding -> CoqCantIntoMutualRecursion
| CompressedBlockBackReference : bool -> nat -> deflateCoding -> deflateCoding -> CoqCantIntoMutualRecursion
| CompressedBlockBackReferenceResolve : bool -> nat -> nat -> deflateCoding -> deflateCoding -> CoqCantIntoMutualRecursion.

(* if there is some error, "onerror" is called with a number *)

Function inflate {errtype : Set} (status : CoqCantIntoMutualRecursion) (input : BitByteList) (back : BackBuffer Byte)
         (onerror :  CoqCantIntoMutualRecursion -> BitByteList -> nat -> list (Byte + errtype)) {measure bbllength input} : list (Byte + errtype) :=
  match status with
    | Start => match (nextBit input) with
                 | None => onerror Start input StreamEndedEarly
                 | Some (bit, rest) => inflate (BlockParse bit) rest back onerror
               end
    | BlockParse x =>
      match (nBits input 2) with
        | None => onerror (BlockParse x) input StreamEndedEarly
        | Some (lb, rest) =>
          match lb with
            | false :: false :: nil => inflate (UncompressedBlockParse x) rest back onerror
            | false :: true :: nil => inflate (DynamicallyCompressedBlockParse x) rest back onerror
            | true :: false :: nil => inflate (StaticallyCompressedBlockParse x) rest back onerror
            | _ => onerror (BlockParse x) rest WrongBlockHeader
          end
      end
    | UncompressedBlockParse x => (* first, overjump bits *)
      match input with
        | BBLConsBit bit rest => inflate (UncompressedBlockParse x) rest back onerror
        | BBLConsByte _ bb _ =>
          match nBits bb 16 with
            | None => onerror (UncompressedBlockParse x) bb 0
            | Some (bits1, bbb) =>
              match nBits bbb 16 with
                | None => onerror (UncompressedBlockParse x) bb 1
                | Some (bits2, rest) =>
                  match isneg bits1 bits2 with
                    | true => inflate (UncompressedBlockPass (lsbToInt bits1) x) rest back onerror
                    | false => onerror (UncompressedBlockParse x) rest 2
                  end
              end
          end
        | _ => onerror (UncompressedBlockParse x) input 3
      end
    | UncompressedBlockPass n x => (* pass bytes *)
      match n with
        | 0 => match x with
                 | false => inflate Start input back onerror
                 | true => nil (* last block *)
               end
        | (S n) =>
          match input with
            | BBLConsByte byte _ bb => (inl byte) :: inflate (UncompressedBlockPass n x) bb (bbcons byte back) onerror
            | _ => onerror (UncompressedBlockPass n x) input 0
          end
      end
    | DynamicallyCompressedBlockParse x =>
      match (nBitsToInt input 5) with
        | None => onerror (DynamicallyCompressedBlockParse x) input 0
        | Some (hlit, b2) =>
          match (nBitsToInt b2 5) with
            | None => onerror (DynamicallyCompressedBlockParse x) b2 1
            | Some (hdist, b3) =>
              match (nBitsToInt b3 4) with
                | None => onerror (DynamicallyCompressedBlockParse x) b3 2
                | Some (hclen, b4) => inflate
                                        (DynamicallyCompressedBlockCodeLengtCode
                                           x (257 + hlit) (1 + hdist) (4 + hclen))
                                        b4 back onerror
              end
          end
      end
    | DynamicallyCompressedBlockCodeLengtCode x hlit hdist hclen =>
      match (nBits input (3 * hclen)) with
        | None => onerror (DynamicallyCompressedBlockCodeLengtCode x hlit hdist hclen) input 0
        | Some (clcbits, rest) =>
          match MayBeCoding (clcBitsToVec clcbits) with
            | None => onerror (DynamicallyCompressedBlockCodeLengtCode x hlit hdist hclen) rest 1
            | Some clc => inflate (DynamicallyCompressedBlockCodeLengths x nil (hlit + hdist) hlit hdist clc) rest back onerror
          end
      end
    | DynamicallyCompressedBlockCodeLengths x revcodelist remaining hlit hdist clc =>
      match remaining with
        | 0 => inflate (DynamicallyCompressedLit x revcodelist nil hlit hdist) input back onerror
        | (S n) => match ReadCode clc input with
                     | None => onerror (DynamicallyCompressedBlockCodeLengths x revcodelist remaining hlit hdist clc) input 0
                     | Some (code, rest) =>
                       match code with
                         | 16 => 
                           match revcodelist with
                             | nil => onerror (DynamicallyCompressedBlockCodeLengths x revcodelist remaining hlit hdist clc) rest 5
                             | rep :: _ =>  match (nBitsToInt rest 2) with
                                              | None => onerror (DynamicallyCompressedBlockCodeLengths x revcodelist remaining hlit hdist clc) rest 6
                                              | Some (count, rest2) =>
                                                let realcount := 3 + count in
                                                match le_dec realcount remaining with
                                                  | left _ => inflate 
                                                                (DynamicallyCompressedBlockCodeLengths
                                                                   x ((xrepeat realcount rep) ++ revcodelist) (remaining - realcount) hlit hdist clc) rest2 back onerror
                                                  | right _ => onerror (DynamicallyCompressedBlockCodeLengths x revcodelist remaining hlit hdist clc) rest2 7
                                                end
                                            end
                           end
                         | 17 =>
                           match (nBitsToInt rest 3) with
                             | None => onerror (DynamicallyCompressedBlockCodeLengths x revcodelist remaining hlit hdist clc) rest 1
                             | Some (count, rest2) =>
                               let realcount := 3 + count in
                               match le_dec realcount remaining with
                                 | left _ => inflate
                                               (DynamicallyCompressedBlockCodeLengths
                                                  x ((xrepeat realcount 0) ++ revcodelist) (remaining - realcount) hlit hdist clc) rest2 back onerror
                                 | right _ => onerror (DynamicallyCompressedBlockCodeLengths x revcodelist remaining hlit hdist clc) rest2 2
                               end
                           end
                         | 18 =>
                           match (nBitsToInt rest 7) with
                             | None => onerror (DynamicallyCompressedBlockCodeLengths x revcodelist remaining hlit hdist clc) rest 3
                             | Some (count, rest2) =>
                               let realcount := 11 + count in
                               match le_dec realcount remaining with
                                 | left _ => inflate
                                               (DynamicallyCompressedBlockCodeLengths
                                                  x ((xrepeat realcount 0) ++ revcodelist) (remaining - realcount) hlit hdist clc) rest2 back onerror
                                 | right _ => onerror (DynamicallyCompressedBlockCodeLengths x revcodelist remaining hlit hdist clc) rest2 4
                               end
                           end
                         | q => inflate (DynamicallyCompressedBlockCodeLengths x (q :: revcodelist) n hlit hdist clc) rest back onerror
                       end
                   end
      end
    | DynamicallyCompressedLit x revcodelist litlist hlit hdist =>
      match (hlit, revcodelist) with
        | (0, _) => match MayBeCoding (Vector.of_list litlist) with
                      | None => onerror (DynamicallyCompressedLit x revcodelist litlist hlit hdist) input 1
                      | Some litlencode => 
                        match MayBeCoding (Vector.of_list (rev revcodelist)) with
                          | None => onerror (DynamicallyCompressedLit x revcodelist litlist hlit hdist) input 2
                          | Some distcode => inflate (CompressedBlock x litlencode distcode) input back onerror
                        end
                    end
        | ((S hlit'), (k :: revcodelist')) => inflate (DynamicallyCompressedLit x revcodelist' (k :: litlist) hlit' hdist) input back onerror
        | _ => onerror (DynamicallyCompressedLit x revcodelist litlist hlit hdist) input 0
      end
    | StaticallyCompressedBlockParse x =>
      inflate (CompressedBlock x fixed_litlen_coding fixed_dist_coding) input back onerror
    | CompressedBlock x lit dist =>
      match ReadCode lit input with
        | None => onerror (CompressedBlock x lit dist) input 0
        | Some (char, rest) =>
          match le_dec char 255 with
            | left isle => let byte := (nat2byte isle) in
                           (inl byte) :: inflate (CompressedBlock x lit dist) rest (bbcons byte back) onerror
            | right isgt =>
              match lt_dec 256 char with
                | right _ => (* char == 256 *)
                  match x with
                    | false => inflate Start rest back onerror
                    | true => nil
                  end
                | left _ => inflate (CompressedBlockBackReference x (char - 257) lit dist) rest back onerror
              end
          end
      end
    | CompressedBlockBackReference x code litcodes distcodes =>
      match (nth_error lenCodeBitNumAndBase code) with
        | None => onerror (CompressedBlockBackReference x code litcodes distcodes) input 0
        | Some (bits, base) =>
          match (nBitsToInt input bits) with
            | None => onerror (CompressedBlockBackReference x code litcodes distcodes) input 1
            | Some (len, rest) =>
              match ReadCode distcodes rest with
                | None => onerror (CompressedBlockBackReference x code litcodes distcodes) rest 2
                | Some (distcode, rest2) =>
                  match (nth_error distCodeBitNumAndBase distcode) with
                    | None => onerror (CompressedBlockBackReference x code litcodes distcodes) rest2 3
                    | Some (bits2, base2) =>
                      match (nBitsToInt rest2 bits2) with
                        | None => onerror (CompressedBlockBackReference x code litcodes distcodes) rest2 4
                        | Some (dist, rest3) =>
                          (* we now have len and dist *)
                          inflate (CompressedBlockBackReferenceResolve x (bits + base) (bits2 + base2 - 1) (* TODO: check off-by-one *) litcodes distcodes) rest3  back onerror
                      end
                  end
              end
          end
      end
    | CompressedBlockBackReferenceResolve x 0 dist litcoding distcoding => inflate (CompressedBlock x litcoding distcoding) input back onerror
    | CompressedBlockBackReferenceResolve x (S len) dist litcoding distcoding =>
      match bbget dist back with
        | None => onerror (CompressedBlockBackReferenceResolve x (S len) dist litcoding distcoding) input 0
        | Some q => (inl q) :: inflate (CompressedBlockBackReferenceResolve x len dist litcoding distcoding) input (bbcons q back) onerror
      end
    (*| _ => onerror Start input 9*)
  end.

Definition infl := inflate.