Reverse Factorial using constraints in Mozart/Oz

gistfile1.txt

proc {Fact ?N ?F}
   proc {Fact1 ?N ?F}
      choice
         N = 0
         F = 1
      []
         N1 F1
      in
         N1::0#FD.sup
         F1::0#FD.sup
         N >: 0
         N1 =: N - 1
         F =: N * F1
         {Fact1 N1 F1}
      end
   end
in
   N::0#FD.sup
   F::0#FD.sup      
   {Fact1 N F}
   {FD.distribute naive [N F]}
end

% Usage

% Gives answer of [120]
{Browse {SolveAll proc {$ ?F} {Fact 5 ?F} end}}

% Gives answer of [4]
{Browse {SolveAll proc {$ ?N} {Fact ?N 24} end}}

% Requires the following helper functions for enumerating solutions
fun {Solve Script}
   {SolStep {Space.new Script} nil}
end

fun {SolStep S Rest}
   case {Space.ask S}
   of failed then Rest
   [] succeeded then {Space.merge S}|Rest
   [] alternatives(N) then 
      {SolLoop S 1 N Rest}
   end
end

fun lazy {SolLoop S I N Rest}
   if I>N then Rest
   elseif I==N then
      {Space.commit S I}
      {SolStep S Rest}
   else Right C in
      Right={SolLoop S I+1 N Rest}
      C={Space.clone S}
      {Space.commit C I}
      {SolStep C Right}
   end
end

fun {SolveAll F}
   L={Solve F}
   proc {TouchAll L}
      if L == nil then skip else {TouchAll L.2} end
   end
in
   {TouchAll L}
   L
end