Library zoo_std.clist__code

Require Import zoo.prelude.
Require Import zoo.language.typeclasses.
Require Import zoo.language.notations.
Require Import zoo.options.

Notation "'clistู Closed'" := (
  in_type "zoo_std.clist.t" 0
)(in custom zoo_tag
).
Notation "'clistู Open'" := (
  in_type "zoo_std.clist.t" 1
)(in custom zoo_tag
).
Notation "'clistู Cons'" := (
  in_type "zoo_std.clist.t" 2
)(in custom zoo_tag
).

Definition clistู app : val :=
  ๐—ฟ๐—ฒ๐—ฐ "app" "t1" "t2" โ†’
    ๐—บ๐—ฎ๐˜๐—ฐ๐—ต "t1" ๐˜„๐—ถ๐˜๐—ต
    | clistู Closed โ†’
        ๐—ณ๐—ฎ๐—ถ๐—น
    | clistู Open โ†’
        "t2"
    | clistู Cons "v" "t1" โ†’
        โ€˜clistู Cons[ "v", "app" "t1" "t2" ]
    ๐—ฒ๐—ป๐—ฑ.

Definition clistู rev_app : val :=
  ๐—ฟ๐—ฒ๐—ฐ "rev_app" "t1" "t2" โ†’
    ๐—บ๐—ฎ๐˜๐—ฐ๐—ต "t1" ๐˜„๐—ถ๐˜๐—ต
    | clistู Closed โ†’
        ๐—ณ๐—ฎ๐—ถ๐—น
    | clistู Open โ†’
        "t2"
    | clistู Cons "v" "t1" โ†’
        "rev_app" "t1" โ€˜clistู Cons[ "v", "t2" ]
    ๐—ฒ๐—ป๐—ฑ.

Definition clistู iter : val :=
  ๐—ฟ๐—ฒ๐—ฐ "iter" "fn" "param" โ†’
    ๐—บ๐—ฎ๐˜๐—ฐ๐—ต "param" ๐˜„๐—ถ๐˜๐—ต
    | clistู Closed โ†’
        ๐—ณ๐—ฎ๐—ถ๐—น
    | clistู Open โ†’
        ()
    | clistู Cons "v" "t" โ†’
        "fn" "v" โฎ
        "iter" "fn" "t"
    ๐—ฒ๐—ป๐—ฑ.