wordle.v

Require Import Coq.Strings.String.
Require Import Coq.Strings.Ascii.
Require Import Coq.Lists.List.
Import ListNotations.

Open Scope string_scope.

(* Make it print lists one item per line*)
Notation "[ x ; y ; .. ; z ]" :=  (cons x (cons y .. (cons z nil) ..))
  (format "[ '[' x ;  '//' y ;  '//' .. ;  '//' z ']' ]") : list_scope.

Record gameState {word : string} := mkState
{
    turn : nat
    ; responses : list string
}.

Definition freshGameState {word: string} : @gameState word :=
    {| turn := O; responses := ["_ _ _ _ _ "] |}.

(* allow simpl to unfold this *)
Arguments freshGameState /.

Fixpoint containsChar (str : string) (char : ascii) : bool :=
    match str with
    | "" => false
    | String c rest => if eqb c char then true else containsChar rest char
    end.

Fixpoint matchLetters (startGoal : string) (goal : string) (guess : string) : string :=
    match goal, guess with
    | String c1 r1, String c2 r2 => (if eqb c1 c2 
                                        then "X " 
                                        else if containsChar startGoal c2
                                            then "O " 
                                            else "_ ") ++ 
                                            (matchLetters startGoal r1 r2)
    | _, _ => "" 
    end.

Definition updateGameState {word} (guess : string) (state : @gameState word) : @gameState word := 
    {|turn := S (turn state); responses := (responses state) ++ [matchLetters word word guess]|}.

Arguments updateGameState /.

Compute updateGameState "stain" (@freshGameState "saint").

Inductive wonGame {word} : @gameState word -> Prop :=
| advance : forall (guess: string) (st: gameState), wonGame (updateGameState guess st) -> wonGame st
| win : forall st : gameState, turn st < 6 -> In "X X X X X " (responses st) -> wonGame st.

Ltac start := simpl.
Ltac guess st := apply (advance st); try (solve [apply win; repeat constructor]); simpl.

Notation "> rs" := (wonGame {|turn := _; responses := rs|}) (at level 70).

Goal wonGame (@freshGameState "value").
start.
guess "stain".
guess "overt".
guess "venue".
guess "value".
Qed.