juvix/tests/Rust/Compilation/positive/test026.juvix

-- functional queues
module test026;

import Stdlib.Prelude open;

type Queue (A : Type) := queue : List A → List A → Queue A;

qfst : {A : Type} → Queue A → List A
  | (queue x _) := x;

qsnd : {A : Type} → Queue A → List A
  | (queue _ x) := x;

front {{Partial}} : {A : Type} → Queue A → A
  | q := phead (qfst q);

pop_front : {A : Type} → Queue A → Queue A
  | {A} q :=
    let
      q' : Queue A := queue (tail (qfst q)) (qsnd q);
    in case qfst q' of
         | nil := queue (reverse (qsnd q')) nil
         | _ := q';

push_back : {A : Type} → Queue A → A → Queue A
  | q x :=
    case qfst q of
      | nil := queue (x :: nil) (qsnd q)
      | q' := queue q' (x :: qsnd q);

is_empty : {A : Type} → Queue A → Bool
  | q :=
    case qfst q of
      | nil :=
        case qsnd q of {
          | nil := true
          | _ := false
        }
      | _ := false;

empty : {A : Type} → Queue A := queue nil nil;

terminating
g {{Partial}} : List Nat → Queue Nat → List Nat
  | acc q :=
    ite (is_empty q) acc (g (front q :: acc) (pop_front q));

f {{Partial}} : Nat → Queue Nat → List Nat
  | zero q := g nil q
  | n@(suc n') q := f n' (push_back q n);

sum : List Nat → Nat
  | nil := 0
  | (h :: t) := h + sum t;

main : Nat := sum (runPartial λ {{{_}} := f 100 empty});