module arch.system.types.commitmenttree;

import prelude open;
import arch.node.types.crypto open;
import arch.system.types.commitment open;

trait
type CommitmentTreeOps A (Tree : Type -> Type) P :=
  mkCommitmentTreeOps@{
    hashRoot : Tree A -> Digest;
    add : A -> Tree A -> Pair (Tree A) P;
    read : P -> Tree A -> Option (Commitment A);
    verify : P -> Commitment A -> Tree A -> Bool;
  };

type MTree A B :=
  | mkMTreeLeaf@{
      value : A;
    }
  | mkMTreeNode@{
      merge : B;
      left : MTree A B;
      right : MTree A B;
    };

CTree (A : Type) : Type := MTree (Commitment A) Digest;

treeHash {A} (tree : CTree A) : Digest :=
  case tree of
    | mkMTreeLeaf@{value := c} := TODO
    -- Commitment.commitment c
    | mkMTreeNode@{merge := digest} := digest;

type PathDir :=
  | PathDirLeft
  | PathDirRight;

CTreePath : Type := List PathDir;

CommitmentTree (A : Type) : Type := CommitmentTreeOps A CTree PathDir;