{-- A Sudoku puzzle application

To start an instance of the application a Dealer publishes a partial
 transaction which creates two ;Resource;s:

1.1 A Sudoku ;Resource; that contains the initial state of the puzzle.

1.2 A ;Resource; containing a logic function that checks the completed
 solution to the puzzle.

And consumes another resource:

2.1 A Reward ;Resource; with quantity equal to the number of unfilled
 squares in the puzzle.

Participants publish partial transactions which consume:

3.1 A Sudoku ;Resource; which represents the current parital solution to the puzzle.

And create:

3.2. A Reward ;Resource; with quantity equal to the number of squares that the participant fills in on the Sudoku grid.

3.3. A Sudoku ;Resource; that contains an updated Sudoku grid with their solutions filled in.

In the partial transaction which contains a full solution to the puzzle, the
 participant additionally consumes the ;Resource; containing the Dealer's
 logic function which was created in 1.2. --}
module Apps.Sudoku;

import Anoma open;
import Anoma.Resource open using {mkResource as mkResource'};

import Apps.Sudoku.Validator as Sudoku;
import Apps.Sudoku.Serializer as Sudoku;

import Data.Map as Map open using {Map};

import Anoma.Prelude open;
import Stdlib.Trait.Partial open;

open PartialTx;

module Reward;
  label : ByteString := [0];
  
  mkResource (n : Int) : Resource :=
    mkResource'
      (logicHash := AlwaysValid.logicHash;
      label := label;
      data := nil;
      quantity := n);
  
  kind : Kind := AlwaysValid.logicHash :: label;
end;

--- Definitions related to the Sudoku ;Resource; in the application
module Sudoku;
  
  type Puzzle :=
    mkPuzzle {
      logicHash : LogicHash;
      solution : ByteString
    };
  
  mkResource (p : Puzzle) (d : ByteString) (n : Int) : Resource :=
    mkResource'
      (logicHash := Puzzle.logicHash p;
      label := Puzzle.solution p;
      data := d;
      quantity := n);
  
  kind (p : Puzzle) : Kind := Puzzle.logicHash p :: Puzzle.solution p;
end;

{-- Checks the state transition.
    * The new ;Resource; represents a valid Sudoku grid
    * The size of the encoded solution doesn't change.
    * The number of filled in squares does not decrease.
    * The claimed reward is equal to the number of newly filled in squares.
    * The only squares that change between the previous and new solutinos
    are changes from zero (i.e unfilled) to non-zero (i.e filled).
 --}
checkTransition {{Partial}} (fromResource : Resource) (toResource : Resource) (reward : Resource)
  : Bool :=
  let
    fromSolution : ByteString := Resource.data fromResource;
    toSolution : ByteString := Resource.data toResource;
    rewardQuantity : Int := Resource.quantity reward;
    
    -- Find the differences between the fromSolution and the toSolution,
    -- compared index-wise
    diff : List (Nat × Nat) :=
      filter (x, y in zip fromSolution toSolution)
        x /= y;
    
    -- Check that any solved squares in the toSolution are unsolved in the
    -- fromSolution
    checkSolvedFromUnsolved : Bool :=
      all (consumedSquare, _ in diff)
        not (Sudoku.entryFilled? consumedSquare);

  in length toSolution == length fromSolution
    && Sudoku.filledSquares toSolution >= Sudoku.filledSquares fromSolution
    && Sudoku.validGrid? (Sudoku.decode toSolution)
    && checkSolvedFromUnsolved
    && ofNat (length diff) == rewardQuantity;

{-- The logic function for the Sudoku solution parital transaction.

Performs the following check:

If there is a consumed ;Resource; representing a Sudoku puzzle then:

1. There is exactly one created ;Resource; corresponding to a new solution and
exactly one created ;Resource; representing the claimed reward.

2. The transition from a Sudoku puzzle to the new solution and reward
satisfies the ;checkTransition; function.

If the partial transaction does not consume a Sudoku puzzle then it is
vacuously valid.

If the logic function part of a ;Resource; that is created by the partial
transaction then it is valid. --}
logicFunction {{Partial}} : Sudoku.Puzzle -> LogicFunction
  | data kind tx :=
    let
      puzzleKind : Kind := Sudoku.kind data;
      fromResources : List Resource :=
        resourcesForKind puzzleKind (consumedResources tx);
      toResources : List Resource :=
        resourcesForKind puzzleKind (createdResources tx);
      rewardResources : List Resource :=
        resourcesForKind Reward.kind (createdResources tx);
    in isCreated kind
      || case fromResources, toResources, rewardResources of {
           | nil, _, _ := true
           | [fromResource], [toResource], [reward] :=
             checkTransition fromResource toResource reward
           | _, _, _ := false
         };

-- Definitions relating to the Dealer participant in the application
module Dealer;
  {-- The logic function for the Sudoku dealer parital transaction.

  Performs the following check:

  If there is exactly one consumed ;Resource; representing a Sudoku puzzle then:

  1. The solution matches the Dealer's solution.

  If the partial transaction does not consume a Sudoku puzzle then it is vacuously valid.

  If the logic function part of a ;Resource; that is created by the partial transaction then it is valid.
   --}
  
  logicFunction : Sudoku.Puzzle -> LogicFunction
    | p kind tx :=
      let
        puzzleResources : List Resource :=
          resourcesForKind (Sudoku.kind p) (createdResources tx);
        
        checkPuzzle (r : Resource) : Bool :=
          Sudoku.Puzzle.solution p == Resource.data r;
      in isCreated kind
        || case puzzleResources of {
             | nil := true
             | [puzzleResource] := checkPuzzle puzzleResource
             | _ := false
           };
  
  logicHash : Sudoku.Puzzle -> LogicHash
    | _ := 2;
  
  label : Sudoku.Puzzle -> ByteString
    | _ := [2];
  
  kind (d : Sudoku.Puzzle) : Kind := logicHash d :: label d;
  
  mkResource (d : Sudoku.Puzzle) (n : Int) : Resource :=
    mkResource'
      (logicHash := logicHash d; label := label d; data := nil; quantity := n);
end;

dealer (puzzle : Sudoku.Puzzle) (initialBoard : ByteString) : PartialTx :=
  mkPartialTx
    (consumedResources := [ Reward.mkResource
                            (ofNat (Sudoku.emptySquares initialBoard))
                          ];
    createdResources := [ Dealer.mkResource puzzle 1
                        ; Sudoku.mkResource puzzle initialBoard 1
                        ]);

logicFunctions {{Partial}} (puzzle : Sudoku.Puzzle)
  : Map LogicHash LogicFunction :=
  mkLogicFunctionMap
    [ Sudoku.Puzzle.logicHash puzzle, logicFunction puzzle
    ; Dealer.logicHash puzzle, Dealer.logicFunction puzzle
    ];