! Sudoku.txt - axioms for Sudoku puzzle solution
!/
  for paper "A More General Specification Language"
  Progress Toward the Holy Grail Workshop
  August 28, 2017, Melbourne, Australia
  part of ICLP'17

! Our top-level axiom defines a program that reads an input text file with
! a Sudoku puzzle and writes an output file that shows the input puzzle
! along with its solution.

  (Program %infile %outfile)<    ! Program valid exprs for Sudoku solver
    (sudoku_in %infile %inarr),    ! map input file to 9x9 board array
         ! Array is just a sequence of 9 rows each with 9 elements,
         ! each of which is a digit '1'-'9' or underscore character.
         ! (A digit '0' in the input file prevents a solution.)
    (sudoku_soln %inarr %outarr),          ! solve the Sudoku puzzle!
         ! Output array is input array with '_' chars replaced with digits.
    (sudoku_out %inarr %outarr %outfile).  ! we output both puzzle & solution
         ! If the input puzzle has more than one solution, then a Program
         ! valid expression is generated for each solution.

! The input file contains 9 lines each with 9 digit/underscore characters.
! Characters other than digit/_ are ignored.
! Additional lines (without any digit/_ characters) are ignored.

! An example input file could look as follows:

   _ 1 _  _ 8 _  _ _ _
   6  5  _ | 7  _  _ | 4  _  _   -- spacing and non-digit/_ chars ignored
   _  _  _   _  2  4   _  9  _
  ---------+---------+---------    -- lines without digit/_ chars ignored
   _ 9 _  _ _ 7  6 _ _
    ...

! sudoku_in - map an input text file to a 9x9 array of digits and _ chars
! On input, all characters except digits and _ are treated as blanks.
! At this point digit 0 is treated like digits 1-9.

  (sudoku_in () ()).
  (sudoku_in (%line $lines) ((% $) $d_rows))<
    (sudoku_in_line %line (% $)),   ! line has one or more digit and _ chars
    (sudoku_in ($lines) ($d_rows)).
  (sudoku_in (%line $lines) ($d_rows))<
    (sudoku_in_line %line ()),      ! line doesn't have any digit or _ chars
    (sudoku_in ($lines) ($d_rows)).

  ! Note that lines with digit and _ characters produce an array row.
  ! Lines without any digit and _ characters are skipped.
  ! If array is not exactly 9x9 then we won't get a solution. 

! sudoku_in_line - get just the digit and _ characters from a line
! (sudoku_in_line <text line> <just the digit/_ chars>)
! - note that 0 is included in the set of digits (but there won't be a soln)

  (sudoku_in_line () ()).
  (axioms                   ! a higher-order form!
    ((sudoku_in_line ( %d_ $chars) (%d_ $d_)) (    in  %d_ %digit_)))
    ((sudoku_in_line (%~d_ $chars) (    $d_)) (not_in %~d_ %digit_)))
  )< (sudoku_in_line ($chars) ($d_)),
     (== %digit_ "0123456789_").   ! we allow '0' here but won't get a solution

! The corresponding output file in the Program valid expression is as follows:

         Sudoku Puzzle

Input:
  _  1  _ | _  8  _ | _  _  _
  6  5  _ | 7  _  _ | 4  _  _
  _  _  _ | _  2  4 | _  9  _
 ---------+---------+---------
  _  9  _ | _  _  7 | 6  _  _ 
    ...

Solution:
  2  1  4 | 9  8  6 | 5  7  3
  6  5  9 | 7  3  1 | 4  2  8
  8  7  3 | 5  2  4 | 1  9  6
 ---------+---------+---------
  4  9  8 | 2  1  7 | 6  3  5
    ...

! sudoku_out - form output file with nicely formated input and solved puzzle

  (sudoku_out %inarr %outarr
    ("        Sudoku Puzzle"     ! title is centered over board
     "" "Input:"
     $inlines
     "" "Solution:"
     $outlines
    ))<
    (sudoku_out_arr %inarr ($inlines)),  ! both input & output arrays displayed
    (sudoku_out_arr %outarr ($outlines)).

! sudoku_out_arr - output Sudoku array to a nicely formated block of lines
! (sudoku_out_arr <9x9 digit/_ array> <output lines>)

  (sudoku_out_arr %arr ($lns1-3 %sep_ln $lns4-6 %sep_ln $lns7-9))<
    (3=parts %arr %3_3rows),    ! partition array rows into 3-row subseqs
    ((map (map sudoku_out_row)) %3_3rows (($lns1-3) ($lns4-6) ($lns7-9))),
        ! map each row into an output line
    (== %sep_ln " ---------+---------+---------").  ! separator line
                !  1  2  3   4  5  6   7  8  9      -- digits wrt sep line

! sudoku_out_row - map row of Sudoku array to output line

  (sudoku_out_line %row (' ' $str1-3 '|' $str4-6 '|' $str7-9))<  ! form line
    (3=parts %row (%3_3elems),     ! partition row into 3-elem subseqs
    ((map (map sudoku_out_elem)) %3_3elems %3_3strs),
       ! map row's elements to blank-surrounded strings
    ((map concat*) %3_3strs (($str1-3) ($str4-6) ($str7-9))).
       ! concat element strings into 3-element strings

! sudoku_out_elem - surround each Sudoku element character with blanks
 
  (sudoku_out_elem % (' ' % ' ')).      ! '3' -> " 3 "


! sudoku_soln - get an instance of input array that satisfies perm dig property

  (sudoku_soln %inarr %outarr)<
    (instance '_' %inarr %outarr),   ! '_' instanced with arbitrary exprs
    (sudoku_rows %outarr %rows),     ! rows of board
    (sudoku_cols %outarr %cols),     ! columns of board
    (sudoku_subarrs %outarr %subarrs),  ! 3x3 subarrays of board
        ! -- these 3x3 subarrs are expressed as 9 9-elem sequences
    (concat* (%rows %cols %subarrs) %allseqs),
    (1* perm "123456789" %allseqs).
        ! all sequences of the output array are permutations of 1-9

  (sudoku_rows %arr %arr).         ! array is already a sequence of rows

  (sudoku_cols %arr %cols)<        ! columns of sudoku board
    (transpose %arr %cols).        ! transpose to get columns

  (sukoku_subarrs %arr %subarrs)<   ! get the 9 3x3 arrays as sequences
    (3=parts %arr %3_3row_groups),   ! sequence of 3-row groups
    ((map (map 3=parts)) %3_3row_groups %3_3row_3elem_seqs),
       ! map each row of 3-row groups into three sequences of 3 elements
    ((map transpose) %3_3row_3elem_seqs %3x3_3x3subarrs),
       ! get 3x3 subarrays grouped in 3-row groups
    (concat* %3x3_3x3subarrs %3x3subarrs),  ! get seq of 9 3x3 subarrays
    ((map concat*) %3x3subarrs %subarrs).   ! flatten 3x3 subarrs into seqs