/* 

  Mu problem in Picat.

  Ported from Prolog program mu.pl
  http://sicstus.sics.se/sicstus/bench.zip
  """
  generated: 9 November 1989
  option(s): 

  mu

  derived from Douglas R. Hofstadter, "Godel, Escher, Bach," pages 33-35.

  prove "mu-math" theorem muiiu
  """

  Also, see http://en.wikipedia.org/wiki/MU_puzzle

  This Picat model was created by Hakan Kjellerstrand, hakank@gmail.com
  See also my Picat page: http://www.hakank.org/picat/

*/


% import util.
import cp.


main => go.

go => 
   data(Data),
   % writeln(data=Data),
   All=findall(Out, $benchmark(Data, Out)),
   foreach(Sol in All) writeln(Sol) end,
   nl.

% From fast_mu.pl (from SICStus' bench.zip)
%
%     string          steps
%	miui		8
%	muii		8
%	muui		11
%	muiiu		6
%	miuuu		9
%	muiuu		9
%	muuiu		9
%	muuui		9

go2 => 
    Test = ["miiiii","miui","muii","muui","muiiu","miuuu","muiuu","muuiu","muuui"],
    foreach(T in Test)
       writeln(t=T),
       All=findall(Out, benchmark(T, Out)),
       foreach(Sol in All) writeln(Sol) end
    end,
    nl.

% random input
go3 => 
    UI = "ui",
    foreach(_T in 1..20)
      Len = 2+random2() mod 8,
      String := "m" ++ [UI[1+random2() mod 2] : _I in 2..Len],
     writeln(string=String),
      All=findall(Out, $benchmark(String, Out)),
      foreach(Sol in All) writeln(Sol) end,
      % benchmark(String, Out),
      % writeln(out=Out),
      nl
    end,
    nl.

% Get the shortest length
go4 => 
    String = "miiiii",
    Len :: 2..20,
    indomain(Len),
    writeln(len=Len),
    All=findall(Out, $theorem(String, Len, Out)),
    foreach(Sol in All) writeln(Sol) end,
    nl,
    (All.length == 0 -> fail ; true).




benchmark(Data, Out) =>
   Len = length(Data),
   theorem(Data, Len, Out).

data(Data) => Data = [m,u,i,i,u].

%% -> mi
theorem(MI, _, AMI) ?=> 
   MI = [m,i],
   AMI = [[a|[m,i]]].

%% -> mu
% theorem(MI, _, MU) ?=> 
%   MI = [m,i],
%   MU = [[a|[m,u]]].

theorem(R, Depth, NRP) =>
   NRP = [[N|R]|P],
   Depth > 0,
   D = Depth-1,
   theorem(S, D, P),
   rule(N, S, R).


rule(N, S, R), N= 1 ?=> rule1(S, R).
rule(N, S, R), N= 2 ?=> rule2(S, R).
rule(N, S, R), N= 3 ?=> rule3(S, R).
rule(N, S, R), N= 4  => rule4(S, R).


% Xi -> Xiu
rule1([i], R) ?=> R=[i,u].
rule1([H|X], R) =>
   R = [H|Y],
   rule1(X, Y).

% mX -> mXX
rule2([m|X], MY) => 
   MY = [m|Y],
   concatenate(X, X, Y).

% XiiiY -> XuY
rule3([i,i,i|X], R) ?=> 
   R = [u|X].
rule3([H|X], HY) =>
   HY = [H|Y],
   rule3(X, Y).

% XuuY -> XY
rule4(UUX, X) ?=>
   UUX = [u,u|X].
rule4([H|X], HY) =>
   HY = [H|Y],
   rule4(X, Y).

concatenate([], X, X2) => 
   X2 = X.
concatenate(AB, X, AB1) =>
   AB = [A|B],
   AB1 = [A|B1],
   concatenate(B, X, B1).