(********************************************************************)
(*                                                                  *)
(*  lzma.s7i      LZMA compression support library                  *)
(*  Copyright (C) 2020, 2021, 2023, 2024  Thomas Mertes             *)
(*                                                                  *)
(*  This file is part of the Seed7 Runtime Library.                 *)
(*                                                                  *)
(*  The Seed7 Runtime Library is free software; you can             *)
(*  redistribute it and/or modify it under the terms of the GNU     *)
(*  Lesser General Public License as published by the Free Software *)
(*  Foundation; either version 2.1 of the License, or (at your      *)
(*  option) any later version.                                      *)
(*                                                                  *)
(*  The Seed7 Runtime Library is distributed in the hope that it    *)
(*  will be useful, but WITHOUT ANY WARRANTY; without even the      *)
(*  implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR *)
(*  PURPOSE.  See the GNU Lesser General Public License for more    *)
(*  details.                                                        *)
(*                                                                  *)
(*  You should have received a copy of the GNU Lesser General       *)
(*  Public License along with this program; if not, write to the    *)
(*  Free Software Foundation, Inc., 51 Franklin Street,             *)
(*  Fifth Floor, Boston, MA  02110-1301, USA.                       *)
(*                                                                  *)
(********************************************************************)


include "bytedata.s7i";


const type: lzmaRangeDecoderState is new struct
    var boolean: corrupted is FALSE;
    var integer: rangeSize is 0;
    var integer: code is 0;
    var file: compressed is STD_NULL;
    var string: inBuffer is "";
    var integer: inBufferPos is 1;
  end struct;


const func char: getc (inout lzmaRangeDecoderState: decoderState) is func
  result
    var char: ch is EOF;
  begin
    if decoderState.inBufferPos > length(decoderState.inBuffer) then
      decoderState.inBuffer := gets(decoderState.compressed, 65536);
      if length(decoderState.inBuffer) <> 0 then
        ch := decoderState.inBuffer[1];
        decoderState.inBufferPos := 2;
      else
        decoderState.inBufferPos := 1;
      end if;
    else
      ch := decoderState.inBuffer[decoderState.inBufferPos];
      incr(decoderState.inBufferPos);
    end if;
  end func;


const func string: gets (inout lzmaRangeDecoderState: decoderState, in integer: maxLength) is func
  result
    var string: stri is "";
  begin
    if maxLength > succ(length(decoderState.inBuffer) - decoderState.inBufferPos) then
      # Not enough chars in inBuffer.
      stri := decoderState.inBuffer[decoderState.inBufferPos ..] &
              gets(decoderState.compressed,
                   maxLength - succ(length(decoderState.inBuffer) - decoderState.inBufferPos));
      decoderState.inBuffer := "";
      decoderState.inBufferPos := 1;
    else
      stri := decoderState.inBuffer[decoderState.inBufferPos fixLen maxLength];
      decoderState.inBufferPos +:= length(stri);
    end if;
  end func;


const proc: resetRangeDecoder (inout lzmaRangeDecoderState: decoderState) is func
  local
    var char: ch is ' ';
    var string: codeStri is "";
  begin
    # writeln("resetRangeDecoder");
    decoderState.corrupted := FALSE;
    decoderState.rangeSize := 16#FFFFFFFF;
    decoderState.code := 0;
    ch := getc(decoderState);
    codeStri := gets(decoderState, 4);
    decoderState.code := bytes2Int(codeStri, UNSIGNED, BE);
    if ch <> '\0;' or length(codeStri) <> 4 or
        decoderState.code = decoderState.rangeSize then
      decoderState.corrupted := TRUE;
    end if;
    # writeln("resetRangeDecoder corrupted: " <& decoderState.corrupted);
  end func;


const func boolean: isFinishedOK (in lzmaRangeDecoderState: decoderState) is
  return decoderState.code = 0;


const proc: normalize (inout lzmaRangeDecoderState: decoderState) is func
  begin
    decoderState.rangeSize := (decoderState.rangeSize << 8) mod 16#100000000;
    decoderState.code := ((decoderState.code << 8) +
                          ord(getc(decoderState))) mod 16#100000000;
  end func;


const func integer: getBit (inout lzmaRangeDecoderState: decoderState, inout integer: prob) is func
  result
    var integer: bit is 0;
  local
    var integer: bound is 0;
  begin
    # Context-based range decoding of a bit using the prob probability variable proceeds in this way:
    bound := (decoderState.rangeSize mdiv 16#800) * prob;
    if decoderState.code < bound then
      decoderState.rangeSize := bound;
      prob +:= (16#800 - prob) mdiv 32;
    else
      decoderState.rangeSize -:= bound;
      decoderState.code -:= bound;
      prob -:= prob mdiv 32;
      bit := 1;
    end if;
    if decoderState.rangeSize < 16#1000000 then
      normalize(decoderState);
    end if;
  end func;


const func integer: getDirectBit (inout lzmaRangeDecoderState: decoderState) is func
  result
    var integer: bit is 0;
  local
    var integer: bound is 0;
  begin
    # Fixed-probability range decoding of a bit proceeds in this way:
    if decoderState.rangeSize < 16#1000000 then
      normalize(decoderState);
    end if;
    decoderState.rangeSize >>:= 1;
    if decoderState.code >= decoderState.rangeSize then
      decoderState.code -:= decoderState.rangeSize;
      bit := 1;
    end if;
  end func;


const func integer: getDirectBits (inout lzmaRangeDecoderState: decoderState, in integer: numBits) is func
  result
    var integer: bits is 0;
  begin
    for numBits do
      bits <<:= 1;
      decoderState.rangeSize >>:= 1;
      if decoderState.code >= decoderState.rangeSize then
        decoderState.code -:= decoderState.rangeSize;
        bits +:= 1;
      end if;
      if decoderState.code = decoderState.rangeSize then
        decoderState.corrupted := TRUE;
      end if;
      if decoderState.rangeSize < 16#1000000 then
        normalize(decoderState);
      end if;
    end for;
  end func;


const integer: LZMA_MODEL_TOTAL_BITS is 11;
const integer: LZMA_PROB_INIT_VAL is (1 << LZMA_MODEL_TOTAL_BITS) mdiv 2;


const func type: lzmaBitTreeDecoder (in integer: numBits) is func
  result
    var type: decoderType is void;
  local
    var type: probsType is void;
  begin
    probsType := array [0 .. pred(1 << numBits)] integer;
    decoderType := new struct
        var probsType: probs is probsType times LZMA_PROB_INIT_VAL;
      end struct;

    global

      const proc: init (inout decoderType: decoder) is func
        begin
          decoder.probs := probsType times LZMA_PROB_INIT_VAL;
        end func;

      const func integer: decode (inout decoderType: decoder, inout lzmaRangeDecoderState: decoderState) is func
        result
          var integer: bits is 1;
        local
          var integer: count is 0;
        begin
          for count range 1 to numBits do
            bits := (bits << 1) + getBit(decoderState, decoder.probs[bits]);
          end for;
          bits -:= 1 << numBits;
        end func;

      const func integer: reverseDecode (inout decoderType: decoder, inout lzmaRangeDecoderState: decoderState) is func
        result
          var integer: bits is 0;
        local
          var integer: m is 1;
          var integer: bitNum is 0;
          var integer: bit is 0;
        begin
          for bitNum range 0 to pred(numBits) do
            # writeln("decoder.probs[" <& m <& "]");
            bit := getBit(decoderState, decoder.probs[m]);
            m <<:= 1;
            m +:= bit;
            bits +:= bit << bitNum;
          end for;
        end func;

    end global;
  end func;


const integer: LZMA_NUM_POS_BITS_MAX is 4;
const integer: LZMA_POS_STATE_MAX is pred(1 << LZMA_NUM_POS_BITS_MAX);

const type: lzmaBitTreeDecoder3 is lzmaBitTreeDecoder(3);
const type: lzmaBitTreeDecoder4 is lzmaBitTreeDecoder(4);
const type: lzmaBitTreeDecoder6 is lzmaBitTreeDecoder(6);
const type: lzmaBitTreeDecoder8 is lzmaBitTreeDecoder(8);

const type: decoder3ArrayType is array [0 .. LZMA_POS_STATE_MAX] lzmaBitTreeDecoder3;

const type: lzmaLenDecoder is new struct
    var integer: choice is LZMA_PROB_INIT_VAL;
    var integer: choice2 is LZMA_PROB_INIT_VAL;
    var decoder3ArrayType: lowCoder is decoder3ArrayType.value;
    var decoder3ArrayType: midCoder is decoder3ArrayType.value;
    var lzmaBitTreeDecoder8: highCoder is lzmaBitTreeDecoder8.value;
  end struct;


const proc: init (inout lzmaLenDecoder: decoder) is func
  local
    var integer: posState is 0;
  begin
    decoder.choice := LZMA_PROB_INIT_VAL;
    decoder.choice2 := LZMA_PROB_INIT_VAL;
    init(decoder.highCoder);
    decoder.lowCoder := decoder3ArrayType.value;
    decoder.midCoder := decoder3ArrayType.value;
    for posState range 0 to LZMA_POS_STATE_MAX do
      init(decoder.lowCoder[posState]);
      init(decoder.midCoder[posState]);
    end for;
  end func;


const func integer: decodeLen (inout lzmaLenDecoder: decoder, inout lzmaRangeDecoderState: decoderState, in integer: posState) is func
  result
    var integer: bits is 0;
  begin
    if getBit(decoderState, decoder.choice) = 0 then
      bits := decode(decoder.lowCoder[posState], decoderState);
    elsif getBit(decoderState, decoder.choice2) = 0 then
      bits := 8 + decode(decoder.midCoder[posState], decoderState);
    else
      bits := 16 + decode(decoder.highCoder, decoderState);
    end if;
  end func;


const func integer: updateState_Literal (in integer: state) is func
  result
    var integer: newState is 0;
  begin
    if state < 4 then
      newState := 0;
    elsif state < 10 then
      newState := state - 3;
    else
      newState := state - 6;
    end if;
  end func;


const func integer: updateState_Match (in integer: state) is func
  result
    var integer: newState is 0;
  begin
    if state < 7 then
      newState := 7;
    else
      newState := 10;
    end if;
  end func;


const func integer: updateState_Rep (in integer: state) is func
  result
    var integer: newState is 0;
  begin
    if state < 7 then
      newState := 8;
    else
      newState := 11;
    end if;
  end func;


const func integer: updateState_ShortRep (in integer: state) is func
  result
    var integer: newState is 0;
  begin
    if state < 7 then
      newState := 9;
    else
      newState := 11;
    end if;
  end func;


const integer: LZMA_STATE_MAX is 11;
const integer: LZMA_LEN_STATE_MAX is 3;
const integer: LZMA_NUM_ALIGN_BITS is 4;
const integer: LZMA_POS_DECODER_MAX_INDEX is 13;
const integer: LZMA_MATCH_MIN_LEN is 2;

const integer: LZMA_DIC_MIN is 1 << 12;


const type: litProbsType             is array [0 .. 16#2ff] integer;
const type: decoder6ArrayType        is array [0 .. LZMA_LEN_STATE_MAX] lzmaBitTreeDecoder6;
const type: posDecoderProbsType      is array [1 .. 127] integer;
const type: posDecoderProbsArrayType is array [4 .. LZMA_POS_DECODER_MAX_INDEX] posDecoderProbsType;
const type: posStateProbsType        is array [0 .. LZMA_POS_STATE_MAX] integer;
const type: posStateProbsArrayType   is array [0 .. LZMA_STATE_MAX] posStateProbsType;
const type: repProbsType             is array [0 .. LZMA_STATE_MAX] integer;

const type: lzmaDecoder is new struct
    var lzmaRangeDecoderState: rangeDec is lzmaRangeDecoderState.value;
    var string: uncompressed is "";
    var integer: dictStartPos is 1;
    var integer: lc is 0;
    var integer: pb is 0;
    var integer: lp is 0;
    var integer: dictSize is 0;
    var integer: state is 0;
    var array litProbsType: litProbs is 0 times litProbsType times LZMA_PROB_INIT_VAL;
    var decoder6ArrayType: posSlotDecoder is decoder6ArrayType.value;
    var lzmaBitTreeDecoder4: alignDecoder is lzmaBitTreeDecoder4.value;
    var posDecoderProbsArrayType: posDecoders is posDecoderProbsArrayType times posDecoderProbsType times LZMA_PROB_INIT_VAL;
    var posStateProbsArrayType: IsMatch is posStateProbsArrayType times posStateProbsType times LZMA_PROB_INIT_VAL;
    var repProbsType: IsRep is repProbsType times LZMA_PROB_INIT_VAL;
    var repProbsType: IsRepG0 is repProbsType times LZMA_PROB_INIT_VAL;
    var repProbsType: IsRepG1 is repProbsType times LZMA_PROB_INIT_VAL;
    var repProbsType: IsRepG2 is repProbsType times LZMA_PROB_INIT_VAL;
    var posStateProbsArrayType: IsRep0Long is posStateProbsArrayType times posStateProbsType times LZMA_PROB_INIT_VAL;
    var integer: rep0 is 0;
    var integer: rep1 is 0;
    var integer: rep2 is 0;
    var integer: rep3 is 0;
    var lzmaLenDecoder: lenDecoder is lzmaLenDecoder.value;
    var lzmaLenDecoder: repLenDecoder is lzmaLenDecoder.value;
  end struct;


const proc: showLzmaDecoder (inout lzmaDecoder: lzma) is func
  begin
    writeln("rangeDec: (" <& lzma.rangeDec.corrupted <& ", " <&
                             lzma.rangeDec.rangeSize <& ", " <&
                             lzma.rangeDec.code <& ", " <&
                             lzma.rangeDec.compressed <> STD_NULL <& ")");
    writeln("lc: " <& lzma.lc);
    writeln("pb: " <& lzma.pb);
    writeln("lp: " <& lzma.lp);
    writeln("dictSize: " <& lzma.dictSize);
    writeln("state: " <& lzma.state);
    writeln("litProbs: " <& minIdx(lzma.litProbs) <& " .. " <& maxIdx(lzma.litProbs));
    writeln("posSlotDecoder: " <& minIdx(lzma.posSlotDecoder) <& " .. " <& maxIdx(lzma.posSlotDecoder));
    writeln("alignDecoder: " <& minIdx(lzma.alignDecoder.probs) <& " .. " <& maxIdx(lzma.alignDecoder.probs));
    writeln("posDecoders: " <& minIdx(lzma.posDecoders) <& " .. " <& maxIdx(lzma.posDecoders));
    writeln("IsMatch: " <& minIdx(lzma.IsMatch) <& " .. " <& maxIdx(lzma.IsMatch));
    writeln("IsRep: " <& minIdx(lzma.IsRep) <& " .. " <& maxIdx(lzma.IsRep));
    writeln("IsRepG0: " <& minIdx(lzma.IsRepG0) <& " .. " <& maxIdx(lzma.IsRepG0));
    writeln("IsRepG1: " <& minIdx(lzma.IsRepG1) <& " .. " <& maxIdx(lzma.IsRepG1));
    writeln("IsRepG2: " <& minIdx(lzma.IsRepG2) <& " .. " <& maxIdx(lzma.IsRepG2));
    writeln("IsRep0Long: " <& minIdx(lzma.IsRep0Long) <& " .. " <& maxIdx(lzma.IsRep0Long));
    writeln("rep0: " <& lzma.rep0);
    writeln("rep1: " <& lzma.rep1);
    writeln("rep2: " <& lzma.rep2);
    writeln("rep3: " <& lzma.rep3);
    writeln("lenDecoder: (" <& lzma.lenDecoder.choice <& ", " <& lzma.lenDecoder.choice2 <& ")");
    writeln("repLenDecoder: (" <& lzma.repLenDecoder.choice <& ", " <& lzma.repLenDecoder.choice2 <& ")");
  end func;


const func boolean: decodeProperties (inout lzmaDecoder: decoder, in string: properties) is func
  result
    var boolean: okay is TRUE;
  local
    var integer: aByte is 0;
    var integer: dictSizeInProperties is 0;
  begin
    aByte := ord(properties[1]);
    if aByte >= 9 * 5 * 5 then
      # writeln("Incorrect LZMA properties");
      okay := FALSE;
    else
      decoder.lc := aByte rem 9;
      aByte := aByte div 9;
      decoder.pb := aByte div 5;
      decoder.lp := aByte rem 5;
      dictSizeInProperties := bytes2Int(properties[2 fixLen 4], UNSIGNED, LE);
      # writeln("dictSizeInProperties: " <& dictSizeInProperties);
      decoder.dictSize := dictSizeInProperties;
      if decoder.dictSize < LZMA_DIC_MIN then
        decoder.dictSize := LZMA_DIC_MIN;
      end if;
    end if;
  end func;


const proc: resetDictionary (inout lzmaDecoder: lzma) is func
  begin
    # writeln("resetDictionary");
    lzma.dictStartPos := succ(length(lzma.uncompressed));
  end func;


const proc: decodeLiteral (inout lzmaDecoder: lzma, in integer: state, in integer: rep0) is func
  local
    var integer: prevByte is 0;
    var integer: symbol is 1;
    var integer: litState is 0;
    var integer: matchByte is 0;
    var integer: matchBit is 0;
    var integer: bit is 0;
  begin
    if length(lzma.uncompressed) >= lzma.dictStartPos then
      prevByte := ord(lzma.uncompressed[length(lzma.uncompressed)]);
    end if;

    litState := ((length(lzma.uncompressed) mod (1 << lzma.lp)) << lzma.lc) + (prevByte >> (8 - lzma.lc));

    if state >= 7 then
      matchByte := ord(lzma.uncompressed[length(lzma.uncompressed) - rep0]);
      repeat
        matchBit := (matchByte >> 7) mod 2;
        matchByte <<:= 1;
        bit := getBit(lzma.rangeDec, lzma.litProbs[litState][((1 + matchBit) << 8) + symbol]);
        symbol := (symbol << 1) + bit;
      until matchBit <> bit or symbol >= 16#100;
    end if;
    while symbol < 16#100 do
      symbol := (symbol << 1) + getBit(lzma.rangeDec, lzma.litProbs[litState][symbol]);
    end while;
    lzma.uncompressed &:= chr(symbol - 16#100);
  end func;


const proc: initDist (inout lzmaDecoder: lzma) is func
  local
    var integer: lenState is 0;
  begin
    for lenState range 0 to LZMA_LEN_STATE_MAX do
      init(lzma.posSlotDecoder[lenState]);
    end for;
    init(lzma.alignDecoder);
    lzma.posDecoders := posDecoderProbsArrayType times posDecoderProbsType times LZMA_PROB_INIT_VAL;
  end func;


const func integer: bitTreeReverseDecode (inout lzmaRangeDecoderState: decoderState,
    inout posDecoderProbsType: probs, in integer: numBits) is func
  result
    var integer: bits is 0;
  local
    var integer: m is 1;
    var integer: bitNum is 0;
    var integer: bit is 0;
  begin
    for bitNum range 0 to pred(numBits) do
      # writeln("probs[" <& m <& "]");
      bit := getBit(decoderState, probs[m]);
      m <<:= 1;
      m +:= bit;
      bits +:= bit << bitNum;
    end for;
  end func;


const func integer: decodeDistance (inout lzmaDecoder: lzma, in integer: length) is func
  result
    var integer: dist is 0;
  local
    var integer: lenState is 0;
    var integer: posSlot is 0;
    var integer: numDirectBits is 0;
  begin
    lenState := length;
    if lenState > LZMA_LEN_STATE_MAX then
      lenState := LZMA_LEN_STATE_MAX;
    end if;
    posSlot := decode(lzma.posSlotDecoder[lenState], lzma.rangeDec);
    if posSlot < 4 then
      dist := posSlot;
    else
      numDirectBits := pred(posSlot >> 1);
      dist := (2 + posSlot mod 2) << numDirectBits;
      if posSlot <= LZMA_POS_DECODER_MAX_INDEX then
        dist +:= bitTreeReverseDecode(lzma.rangeDec, lzma.posDecoders[posSlot], numDirectBits);
      else
        dist +:= getDirectBits(lzma.rangeDec, numDirectBits - LZMA_NUM_ALIGN_BITS) << LZMA_NUM_ALIGN_BITS;
        dist +:= reverseDecode(lzma.alignDecoder, lzma.rangeDec);
      end if;
    end if;
  end func;


const proc: resetPropabilities (inout lzmaDecoder: lzma) is func
  begin
    lzma.litProbs := [0 .. pred(1 << (lzma.lc + lzma.lp))] times litProbsType times LZMA_PROB_INIT_VAL;

    initDist(lzma);

    lzma.IsMatch := posStateProbsArrayType times posStateProbsType times LZMA_PROB_INIT_VAL;
    lzma.IsRep := repProbsType times LZMA_PROB_INIT_VAL;
    lzma.IsRepG0 := repProbsType times LZMA_PROB_INIT_VAL;
    lzma.IsRepG1 := repProbsType times LZMA_PROB_INIT_VAL;
    lzma.IsRepG2 := repProbsType times LZMA_PROB_INIT_VAL;
    lzma.IsRep0Long := posStateProbsArrayType times posStateProbsType times LZMA_PROB_INIT_VAL;

    init(lzma.lenDecoder);
    init(lzma.repLenDecoder);
  end func;


const proc: resetState (inout lzmaDecoder: lzma) is func
  begin
    # writeln("resetState");
    # LZMA state resets cause a reset of all LZMA state except the dictionary, and specifically:
    #   The range coder
    resetRangeDecoder(lzma.rangeDec);
    #   The state value
    lzma.state := 0;
    #   The last distances for repeated matches
    lzma.rep0 := 0;
    lzma.rep1 := 0;
    lzma.rep2 := 0;
    lzma.rep3 := 0;
    #   All LZMA probabilities
    resetPropabilities(lzma);
  end func;


const proc: copyMatch (inout string: uncompressed, in integer: distance, in var integer: length) is func
  local
    var integer: nextPos is 0;
    var integer: number is 0;
  begin
    # writeln("copyMatch: distance=" <& distance <& ", length=" <& length <& " ");
    if length > distance then
      nextPos := succ(length(uncompressed));
      uncompressed &:= "\0;" mult length;
      for number range nextPos to nextPos + length - 1 do
        uncompressed @:= [number] uncompressed[number - distance];
      end for;
    else # hopefully length(uncompressed) >= distance holds
      uncompressed &:= uncompressed[succ(length(uncompressed)) - distance fixLen length];
    end if;
  end func;


const integer: LZMA_RES_PROCESSING              is 0;
const integer: LZMA_RES_ONGOING                 is 1;
const integer: LZMA_RES_FINISHED_WITH_MARKER    is 2;
const integer: LZMA_RES_FINISHED_WITHOUT_MARKER is 3;
const integer: LZMA_RES_ERROR                   is 4;


const func integer: decodePacket (inout lzmaDecoder: lzma,
    in boolean: useRequestedSize, in var integer: unpackSizeRequested) is func
  result
    var integer: decodeResult is LZMA_RES_PROCESSING;
  local
    var integer: state is 0;
    var integer: posState is 0;
    var integer: length is 0;
    var integer: dist is 0;
    var boolean: handleCopyMatch is FALSE;
  begin
    state := lzma.state;
    repeat
      if unpackSizeRequested <= 0 and useRequestedSize then
        if unpackSizeRequested = 0 and isFinishedOK(lzma.rangeDec) then
          decodeResult := LZMA_RES_FINISHED_WITHOUT_MARKER;
        else
          decodeResult := LZMA_RES_ONGOING;
        end if;
      else
        posState := length(lzma.uncompressed) mod (1 << lzma.pb);

        if getBit(lzma.rangeDec, lzma.IsMatch[state][posState]) = 0 then
          decodeLiteral(lzma, state, lzma.rep0);
          state := updateState_Literal(state);
          decr(unpackSizeRequested);
        else

          handleCopyMatch := TRUE;
          if getBit(lzma.rangeDec, lzma.IsRep[state]) <> 0 then
            if length(lzma.uncompressed) < lzma.dictStartPos then
              decodeResult := LZMA_RES_ERROR;
            elsif getBit(lzma.rangeDec, lzma.IsRepG0[state]) = 0 then
              if getBit(lzma.rangeDec, lzma.IsRep0Long[state][posState]) = 0 then
                state := updateState_ShortRep(state);
                lzma.uncompressed &:= lzma.uncompressed[length(lzma.uncompressed) - lzma.rep0];
                decr(unpackSizeRequested);
                handleCopyMatch := FALSE;
              else
                length := decodeLen(lzma.repLenDecoder, lzma.rangeDec, posState);
                state := updateState_Rep(state);
              end if;
            else
              if getBit(lzma.rangeDec, lzma.IsRepG1[state]) = 0 then
                dist := lzma.rep1;
              else
                if getBit(lzma.rangeDec, lzma.IsRepG2[state]) = 0 then
                  dist := lzma.rep2;
                else
                  dist := lzma.rep3;
                  lzma.rep3 := lzma.rep2;
                end if;
                lzma.rep2 := lzma.rep1;
              end if;
              lzma.rep1 := lzma.rep0;
              lzma.rep0 := dist;
              length := decodeLen(lzma.repLenDecoder, lzma.rangeDec, posState);
              state := updateState_Rep(state);
            end if;
          else
            lzma.rep3 := lzma.rep2;
            lzma.rep2 := lzma.rep1;
            lzma.rep1 := lzma.rep0;
            length := decodeLen(lzma.lenDecoder, lzma.rangeDec, posState);
            state := updateState_Match(state);
            lzma.rep0 := decodeDistance(lzma, length);
            if lzma.rep0 = 16#ffffffff then
              if isFinishedOK(lzma.rangeDec) then
                decodeResult := LZMA_RES_FINISHED_WITH_MARKER;
              else
                decodeResult := LZMA_RES_ERROR;
              end if;
            elsif lzma.rep0 >= lzma.dictSize or
                length(lzma.uncompressed) - lzma.rep0 < lzma.dictStartPos then
              decodeResult := LZMA_RES_ERROR;
            end if;
          end if;
          if handleCopyMatch and decodeResult = LZMA_RES_PROCESSING then
            length +:= LZMA_MATCH_MIN_LEN;
            copyMatch(lzma.uncompressed, lzma.rep0 + 1, length);
            unpackSizeRequested -:= length;
          end if;
        end if;
      end if;
    until decodeResult <> LZMA_RES_PROCESSING;
    lzma.state := state;
  end func;


(**
 *  Decompress a file that was compressed with LZMA.
 *  LZMA is the Lempel–Ziv–Markov chain algorithm. LZMA performs
 *  lossless data compression. This LZMA decompression function
 *  is tailored towards the header format used in [[zip|ZIP]] files.
 *  @return the uncompressed string.
 *  @exception RANGE_ERROR If ''compressed'' is not in LZMA format.
 *)
const func string: lzmaDecompress (inout file: compressed,
    in integer: uncompressedSize) is func
  result
    var string: uncompressed is "";
  local
    var string: header is "";
    var integer: majorVersion is 0;
    var integer: minorVersion is 0;
    var integer: size is 0;
    var lzmaDecoder: lzmaDec is lzmaDecoder.value;
    var integer: decodeResult is LZMA_RES_ONGOING;
  begin
    header := gets(compressed, 9);
    if length(header) = 9 then
      majorVersion :=       ord(header[1]);
      minorVersion :=       ord(header[2]);
      size         := bytes2Int(header[3 fixLen 2], UNSIGNED, LE);
      if size = 5 and decodeProperties(lzmaDec, header[5 ..]) then
        lzmaDec.rangeDec.compressed := compressed;
        resetDictionary(lzmaDec);
        resetRangeDecoder(lzmaDec.rangeDec);
        if not lzmaDec.rangeDec.corrupted then
          resetPropabilities(lzmaDec);
          repeat
            decodeResult := decodePacket(lzmaDec, TRUE, uncompressedSize);
          until decodeResult <> LZMA_RES_ONGOING;
        end if;
      end if;
    end if;
    if decodeResult = LZMA_RES_FINISHED_WITH_MARKER or
        decodeResult = LZMA_RES_FINISHED_WITHOUT_MARKER then
      uncompressed := lzmaDec.uncompressed;
    else
      raise RANGE_ERROR;
    end if;
  end func;


(**
 *  [[file|File]] implementation type to decompress a LZMA file.
 *  LZMA is the Lempel–Ziv–Markov chain algorithm. LZMA performs
 *  lossless data compression.
 *)
const type: lzmaFile is sub null_file struct
    var file: compressed is STD_NULL;
    var integer: unpackSize is 0;
    var boolean: unpackSizeDefined is FALSE;
    var integer: decodeResult is LZMA_RES_ONGOING;
    var lzmaDecoder: lzmaDec is lzmaDecoder.value;
    var integer: position is 1;
  end struct;

type_implements_interface(lzmaFile, file);


(**
 *  Open a LZMA file for reading (decompression).
 *  LZMA is the Lempel–Ziv–Markov chain algorithm. LZMA performs
 *  lossless data compression. Reading from the file delivers
 *  decompressed data. Writing is not supported.
 *  @return the file opened, or [[null_file#STD_NULL|STD_NULL]]
 *          if the file is not in LZMA format.
 *)
const func file: openLzmaFile (inout file: compressed) is func
  result
    var file: newFile is STD_NULL;
  local
    var string: header is "";
    var lzmaFile: new_lzmaFile is lzmaFile.value;
  begin
    header := gets(compressed, 13);
    if length(header) = 13 and
        decodeProperties(new_lzmaFile.lzmaDec, header) then
      if header[6 fixLen 8] <> "\16#ff;\16#ff;\16#ff;\16#ff;\16#ff;\16#ff;\16#ff;\16#ff;" then
        new_lzmaFile.unpackSizeDefined := TRUE;
        new_lzmaFile.unpackSize := bytes2Int(header[6 fixLen 8], UNSIGNED, LE);
      end if;
      new_lzmaFile.lzmaDec.rangeDec.compressed := compressed;
      resetDictionary(new_lzmaFile.lzmaDec);
      resetRangeDecoder(new_lzmaFile.lzmaDec.rangeDec);
      if not new_lzmaFile.lzmaDec.rangeDec.corrupted then
        resetPropabilities(new_lzmaFile.lzmaDec);
        newFile := toInterface(new_lzmaFile);
      end if;
    end if;
  end func;


(**
 *  Close a ''lzmaFile''.
 *)
const proc: close (in lzmaFile: aFile) is noop;


(**
 *  Read a character from a ''lzmaFile''.
 *  @return the character read.
 *)
const func char: getc (inout lzmaFile: inFile) is func
  result
    var char: charRead is ' ';
  local
    const integer: BUFFER_SIZE is 1024;
    var integer: missing is integer.last;
  begin
    if inFile.position > length(inFile.lzmaDec.uncompressed) and
        inFile.decodeResult = LZMA_RES_ONGOING then
      if inFile.position - length(inFile.lzmaDec.uncompressed) <=
          integer.last - BUFFER_SIZE then
        # The number of missing characters can be computed without integer overflow.
        missing := inFile.position - length(inFile.lzmaDec.uncompressed) + BUFFER_SIZE;
      end if;
      inFile.decodeResult := decodePacket(inFile.lzmaDec, TRUE, missing);
    end if;
    if inFile.position <= length(inFile.lzmaDec.uncompressed) then
      charRead := inFile.lzmaDec.uncompressed[inFile.position];
      incr(inFile.position);
    else
      charRead := EOF;
    end if;
  end func;


(**
 *  Read a string with maximum length from a ''lzmaFile''.
 *  @return the string read.
 *  @exception RANGE_ERROR The parameter ''maxLength'' is negative.
 *)
const func string: gets (inout lzmaFile: inFile, in integer: maxLength) is func
  result
    var string: striRead is "";
  local
    const integer: BUFFER_SIZE is 1024;
    var integer: charsPresent is 0;
    var integer: missing is integer.last;
  begin
    if maxLength <= 0 then
      if maxLength <> 0 then
        raise RANGE_ERROR;
      end if;
    else
      charsPresent := succ(length(inFile.lzmaDec.uncompressed) - inFile.position);
      if maxLength > charsPresent and inFile.decodeResult = LZMA_RES_ONGOING then
        if (charsPresent >= 0 and maxLength - charsPresent <= integer.last - BUFFER_SIZE) or
            (charsPresent < 0 and maxLength - integer.last + BUFFER_SIZE <= charsPresent) then
          # The number of missing characters can be computed without integer overflow.
          missing := maxLength - charsPresent + BUFFER_SIZE;
        end if;
        inFile.decodeResult := decodePacket(inFile.lzmaDec, TRUE, missing);
      end if;
      if maxLength <= succ(length(inFile.lzmaDec.uncompressed) - inFile.position) then
        striRead := inFile.lzmaDec.uncompressed[inFile.position fixLen maxLength];
        inFile.position +:= maxLength;
      else
        striRead := inFile.lzmaDec.uncompressed[inFile.position ..];
        inFile.position := succ(length(inFile.lzmaDec.uncompressed));
      end if;
    end if;
  end func;


(**
 *  Determine the end-of-file indicator.
 *  The end-of-file indicator is set if at least one request to read
 *  from the file failed.
 *  @return TRUE if the end-of-file indicator is set, FALSE otherwise.
 *)
const func boolean: eof (in lzmaFile: inFile) is
  return inFile.position > length(inFile.lzmaDec.uncompressed) and
      (inFile.decodeResult = LZMA_RES_FINISHED_WITH_MARKER or
       inFile.decodeResult = LZMA_RES_FINISHED_WITHOUT_MARKER);


(**
 *  Determine if at least one character can be read successfully.
 *  This function allows a file to be handled like an iterator.
 *  @return FALSE if ''getc'' would return EOF, TRUE otherwise.
 *)
const func boolean: hasNext (inout lzmaFile: inFile) is func
  result
    var boolean: hasNext is FALSE;
  local
    const integer: BUFFER_SIZE is 1024;
    var integer: missing is integer.last;
  begin
    if inFile.position > length(inFile.lzmaDec.uncompressed) and
        inFile.decodeResult = LZMA_RES_ONGOING then
      if inFile.position - length(inFile.lzmaDec.uncompressed) <=
          integer.last - BUFFER_SIZE then
        # The number of missing characters can be computed without integer overflow.
        missing := inFile.position - length(inFile.lzmaDec.uncompressed) + BUFFER_SIZE;
      end if;
      inFile.decodeResult := decodePacket(inFile.lzmaDec, TRUE, missing);
    end if;
    hasNext := inFile.position <= length(inFile.lzmaDec.uncompressed);
  end func;


(**
 *  Obtain the length of a file.
 *  The file length is measured in bytes.
 *  @return the length of a file, or 0 if it cannot be obtained.
 *)
const func integer: length (inout lzmaFile: aFile) is func
  result
    var integer: length is 0;
  begin
    if aFile.unpackSizeDefined then
      length := aFile.unpackSize;
    else
      if aFile.decodeResult = LZMA_RES_ONGOING then
        aFile.decodeResult := decodePacket(aFile.lzmaDec, TRUE, integer.last);
      end if;
      length := length(aFile.lzmaDec.uncompressed);
    end if;
  end func;


(**
 *  Determine if the file ''aFile'' is seekable.
 *  If a file is seekable the functions ''seek'' and ''tell''
 *  can be used to set and and obtain the current file position.
 *  @return TRUE, since a ''lzmaFile'' is seekable.
 *)
const boolean: seekable (in lzmaFile: aFile) is TRUE;


(**
 *  Set the current file position.
 *  The file position is measured in bytes from the start of the file.
 *  The first byte in the file has the position 1.
 *  @exception RANGE_ERROR The file position is negative or zero.
 *)
const proc: seek (inout lzmaFile: aFile, in integer: position) is func
  begin
    if position <= 0 then
      raise RANGE_ERROR;
    else
      aFile.position := position;
    end if;
  end func;


(**
 *  Obtain the current file position.
 *  The file position is measured in bytes from the start of the file.
 *  The first byte in the file has the position 1.
 *  @return the current file position.
 *)
const func integer: tell (in lzmaFile: aFile) is
  return aFile.position;