Unscrambling without Prolog

Inductive Bit : Set :=
  H  | V
| TL | TR
| BL | BR.

Definition State :=
 (Bit * Bit * Bit *
  Bit *       Bit *
  Bit * Bit * Bit)%type.

Inductive Move : State -> State -> Set :=
| refl : forall S, Move S S

| top_left : forall A B C D E F G H, Move
  (A, B, C,
   D,    E,
   F, G, H)
  (B, C, A,
   D,    E,
   F, G, H)

| left_down : forall A B C D E F G H, Move
  (A, B, C,
   D,    E,
   F, G, H)
  (F, B, C,
   A,    E,
   D, G, H)

| right_down : forall A B C D E F G H, Move
  (A, B, C,
   D,    E,
   F, G, H)
  (A, B, H,
   D,    C,
   F, G, E)

| bottom_left : forall A B C D E F G H, Move
  (A, B, C,
   D,    E,
   F, G, H)
  (A, B, C,
   D,    E,
   G, H, F)

| trans_closure : forall A M Z,
  Move A M -> Move M Z -> Move A Z.


Definition solution state := Move state (TL, H, TR,
                                         V,     V,
                                         BL, H, BR).

Theorem prolog_example :
  solution (H, BR, BL,
            H,     TL,
            TR, V, V).


unfold solution.
eapply trans_closure.
apply top_left.
change (solution (BR, BL, H, H, TL, TR, V, V)).

Ltac whack direction :=
  unfold solution;
  eapply trans_closure;
    [ apply direction
    | match goal with
        | |- Move ?x _ => change (solution x)
      end
    ].

Ltac wtop := whack top_left.
Ltac wleft := whack left_down.
Ltac wright := whack right_down.
Ltac wbottom := whack bottom_left.

wtop.
wtop.

wtop.
wtop.
wbottom.
wbottom.
wleft.
wright.
wbottom.
wbottom.
wleft.
wright.

unfold solution.

apply refl.

Qed.

Theorem automated_example :
  solution (H, BR, BL,
            H,     TL,
            TR, V, V).

Inductive Marker (A : State) : Set := mkMarker.

Ltac save_state :=
  match goal with
    | |- solution ?state =>
      let seen := fresh "seen"
        in pose (seen := mkMarker state)
  end.

Ltac check_progress :=
  match goal with
    | |- solution ?State =>
      match goal with
        | _ : Marker State |- _ =>
          pose (dead_end := True)
        | _ => idtac
      end
  end.

Ltac swtop := save_state; whack top_left; check_progress.
Ltac swleft := save_state; whack left_down; check_progress.
Ltac swright := save_state; whack right_down; check_progress.
Ltac swbottom := save_state; whack bottom_left; check_progress.

Ltac swhack n :=
  (unfold solution; apply refl) ||
    match n with
      | 0 => fail
      | S ?m => swtop; pose (dead_end := False); clear dead_end; swhack m
      | S ?m => swleft; pose (dead_end := False); clear dead_end; swhack m
      | S ?m => swright; pose (dead_end := False); clear dead_end; swhack m
      | S ?m => swbottom; pose (dead_end := False); clear dead_end; swhack m
    end.

swhack 12.

Defined.

Print automated_example.

(*
automated_example = 
let seen := mkMarker (H, BR, BL, H, TL, TR, V, V) in
trans_closure (H, BR, BL, H, TL, TR, V, V) (BR, BL, H, H, TL, TR, V, V)
  (TL, H, TR, V, V, BL, H, BR) (top_left H BR BL H TL TR V V)
  (let dead_end := False in
   let seen0 := mkMarker (BR, BL, H, H, TL, TR, V, V) in
   trans_closure (BR, BL, H, H, TL, TR, V, V) (BL, H, BR, H, TL, TR, V, V)
     (TL, H, TR, V, V, BL, H, BR) (top_left BR BL H H TL TR V V)
     (let dead_end0 := False in
      let seen1 := mkMarker (BL, H, BR, H, TL, TR, V, V) in
      trans_closure (BL, H, BR, H, TL, TR, V, V) (TR, H, BR, BL, TL, H, V, V)
        (TL, H, TR, V, V, BL, H, BR) (left_down BL H BR H TL TR V V)
        (let dead_end1 := False in
         let seen2 := mkMarker (TR, H, BR, BL, TL, H, V, V) in
         ...
*)

Require Import List.
Inductive Move2 : Set := top_left2 | left_down2 | right_down2 | bottom_left2.
Fixpoint display_moves p q (m : Move p q) : list Move2 :=
  match m with
    | refl _ => nil
    | top_left _ _ _ _ _ _ _ _ => top_left2::nil
    | left_down _ _ _ _ _ _ _ _ => left_down2::nil
    | right_down _ _ _ _ _ _ _ _ => right_down2::nil
    | bottom_left _ _ _ _ _ _ _ _ => bottom_left2::nil
    | trans_closure _ _ _ x y => display_moves _ _ x ++ display_moves _ _ y
  end.

Eval compute in (display_moves _ _ automated_example).
(*
     = top_left2
       :: top_left2
       :: left_down2
       :: top_left2
       :: right_down2
       :: top_left2
       :: top_left2
       :: bottom_left2
       :: bottom_left2
       :: left_down2
       :: right_down2
       :: right_down2
       :: nil
     : list Move2
*)

Unscrambling with Prolog

%% I'm playing this Oxyd game (inside Enigma [link])
%% One of the puzzles is this scrambled configuration

starting(([-,⌋,⌊]
         ,[-,  ⌈]
         ,[⌉,|,|])).

%% And you've to hit against the sides to unscramble it into:

solution(([⌈,-,⌉]
         ,[|,  |]
         ,[⌊,-,⌋])).

%% Then it explodes and you win a spring
%% The moves you can do are:

move(top_left,
    ([A,B,C]
    ,[D,  E]
    ,[F,G,H]) --> ([B,C,A]
                  ,[D,  E]
                  ,[F,G,H])).

move(left_down,
    ([A,B,C]
    ,[D,  E]
    ,[F,G,H]) --> ([F,B,C]
                  ,[A,  E]
                  ,[D,G,H])).

move(right_down,
    ([A,B,C]
    ,[D,  E]
    ,[F,G,H]) --> ([A,B,H]
                  ,[D,  C]
                  ,[F,G,E])).

move(bottom_left,
    ([A,B,C]
    ,[D,  E]
    ,[F,G,H]) --> ([A,B,C]
                  ,[D,  E]
                  ,[G,H,F])).

%% I want Prolog to solve this automatically for me though,
%% My first attempt is to use recursion like so,

%: solve(Win,[]) :- solution(Win).
%: solve(State,[Move|Moves]) :- move(Move,State --> Next), solve(Next,Moves).

%! ?- starting(State), solve(State,Moves).
%! ERROR: Out of local stack

%% Since Prolog searches depth first, this just kept trying top_left,
%% again and again, getting nowhere, infact it seeing the same config.
%% so I can pass along a list of seen configurations now, and fail when
%% the same one is seen twice.

%: solve(Win,[],_) :- solution(Win).
%: solve(State,[Move|Moves],Seen) :- move(Move,State --> Next), not(member(Next,Seen)), solve(Next,Moves,[State|Seen]).

%! ?- starting(State), solve(State,Moves,[State]).
%! State = ([-, '⌋', '⌊'], [-, '⌈'], ['⌉', ('|'), ('|')]),
%! Moves = [top_left, top_left, left_down, top_left, top_left, left_down, ...]

%% I got a solution this time... but it's thousands of moves, I think the puzzle can be solved
%% Within at least 10 moves, so Prolog should fail if it gets into a branch in the search tree that deep

solve(Win,[],_,_) :- solution(Win).
solve(State,[Move|Moves],Seen,Limit) :-
 move(Move,State --> Next), not(member(Next,Seen)), succ(LowerLimit,Limit), solve(Next,Moves,[State|Seen],LowerLimit).

solve(Solution) :- starting(State), solve(State,Solution,[State],10).

%! ?- solve(Moves).
%! Moves = [top_left, top_left, bottom_left, bottom_left, left_down, right_down, bottom_left,
%!          bottom_left, left_down, right_down].

Lights out solver using CLP

:- use_module(library(clpfd)).

solve(Puzzle,Solution) :-
 dimensions(Puzzle,Rows,Cols), dimensions(Solution,Rows,Cols),
 flatten(Solution,Variables), Variables ins 0..1,
 cells_of(Puzzle --> configure(Solution)), label(Variables).

configure(Solution,(X,Y,o)) :- around(X,Y,Solution,Group), off(Group).
configure(Solution,(X,Y,*)) :- around(X,Y,Solution,Group), on(Group).

on(Lights) :- sum(Lights, #=, On), 1 #= On mod 2.
off(Lights) :- sum(Lights, #=, Off), 0 #= Off mod 2.

around(X,Y,Grid,[Up,Left,Down,Right,Middle]) :-
 Yu is Y-1, Xl is X-1,
 Yd is Y+1, Xr is X+1,
 ( Grid@([Yu,X]->Up) -> true ; Up = 0 ),
 ( Grid@([Y,Xl]->Left) -> true ; Left = 0 ),
 ( Grid@([Yd,X]->Down) -> true ; Down = 0 ),
 ( Grid@([Y,Xr]->Right) -> true ; Right = 0 ),
 ( Grid@([Y,X]->Middle) -> true ; Middle = 0 ).

game([[*,o,o,o,o,o,*,o],
      [*,*,o,*,*,*,*,*],
      [*,*,o,*,*,*,o,*],
      [*,o,o,o,o,o,o,o],
      [o,*,*,o,o,o,*,*],
      [o,*,o,o,o,o,o,o],
      [*,*,*,*,*,*,o,o],
      [o,*,*,*,*,*,*,*]]).





:- op(500,xfy,@).
:- op(1050,yfx,<-).

flatten([],[]).
flatten([X|Xs],Zs) :- flatten(Xs,Ys), append(X,Ys,Zs).

flip(P,Y,X) :- call(P,X,Y).
dimensions(Grid, Rows, Cols) :- length(Grid, Rows), maplist(flip(length,Cols),Grid).

E@([]->E)         :- !.
[X|_]@([0|Ns]->E) :- !, X@(Ns->E).
[_|X]@([N|Ns]->E) :- !, N > 0, succ(M, N), X@([M|Ns]->E).

_/E@([]<-E)               :- !.
[X|Xs]/[Y|Xs]@([0|Ns]<-E) :- !, X/Y@(Ns<-E).
[X|Xs]/[X|Ys]@([N|Ns]<-E) :- !, N > 0, succ(M, N), Xs/Ys@([M|Ns]<-E).

tuple(Board,Tuples) :- tuple((0,0),Board,Tuples).
tuple(_,[],[]).
tuple((X,Y),[Row|Rows],Tuples) :-
 tuprow((X,Y),Row-Tail,Tuples),
 succ(Y,Y1), tuple((X,Y1),Rows,Tail).
tuprow(_,[]-X,X).
tuprow((I,J),[E|Es]-X,[(I,J,E)|Xs]) :- succ(I,I1),tuprow((I1,J),Es-X,Xs).

cells_of(Grid --> Pred) :- tuple(Grid, Tuples), maplist(Pred, Tuples).

Interpreter for Prolog without cut

I thought this was a good way to write a Prolog interpreter but it is very hard to add cut to. How could it be done?

{-# OPTIONS_GHC -XTypeOperators #-}
{-# OPTIONS_GHC -fno-monomorphism-restriction #-}

import Prelude hiding ((.),(+))
import Data.List hiding (groupBy)
import Control.Applicative
import Control.Monad
import Control.Monad.State
import Control.Monad.List
import Control.Monad.Identity
import Control.Arrow

infix 8 ≡
infix 8 ⤴
infix 8 ↗

(.) = fmap
(<||>) = liftA2 (||)
(&) = liftM2 (,)
p << q = do x <- q ; p ; return x
message `should` assertion = if assertion then mzero else return ()

groupBy p [] = []
groupBy p (x:xs) = let (yes,no) = sift p (p x) (x:xs)
                    in yes : groupBy p no

sift p e = foldr sort ([],[])
 where sort x (ys,ns) | e == p x  = (x:ys,ns)
                      | otherwise = (ys,x:ns)

type Identifier = String
type Name = String
type Arity = Integer
------------------------------------------------------------------------------------------

------------------------------------------------------------------------------------------
type key :--> val = [(key,val)]
(k ~~> v) σ = (k,v):σ

-- type key -> val
(i --> t) σ = \e -> if e == Var i then t else σ e
------------------------------------------------------------------------------------------

------------------------------------------------------------------------------------------
data Term = Var Identifier | (Name,Arity):>[Term]  deriving Eq

instance Show Term where
 show (Var v) = v
 show ((name,0):>[]) = name
 show ((name,_):>args) = name ++ "(" ++ intercalate "," (show . args) ++ ")"

functor (f:>_) = f
variables (Var v) = [v] ; variables (_:>vs) = variables=<<vs

σ⤴ t = case σ t of p:>ps -> p:>(σ↗ps) ; v -> if t == v then t else σ⤴ v
σ↗ ts = (σ⤴).ts

i `occur` Var _ = False
i `occur` (_:>ts) = any ((== Var i) <||> (i `occur`)) ts

(p:>ps ≡ q:>qs) σ = do "Cyclic" `should` (p /= q) ; foldM unify σ (zip (σ↗ ps) (σ↗ qs))
(Var x ≡ t) σ = do "Occurs check" `should` (x `occur` (σ⤴ t)) ; return $ (x --> t) σ
(t ≡ Var x) σ = (Var x ≡ t) σ
unify σ (p,q) = (p ≡ q) σ
------------------------------------------------------------------------------------------

------------------------------------------------------------------------------------------
type Gensym k v m a = StateT (k :--> v,[v]) m a

withGensyms freshVariables = flip evalStateT ([],freshVariables)
names = flip replicateM ['A'..'Z'] =<< [1..]

gensym k = get >>= \(sto,g:gs) -> case lookup k sto of
  Nothing -> do put ((k ~~> g) sto,gs) ; return g
  Just v  -> do                          return v

putSupply = modify . second . const
symScope p = get >>= runStateT p >>= \(v,s) -> putSupply (snd s) >> return v

copyTerm (Var v) = Var . gensym v
copyTerm (a:>as) = (a:>) . mapM copyTerm as
copyRule (p,q) = symScope (copyTerm p & mapM copyTerm q)
------------------------------------------------------------------------------------------

------------------------------------------------------------------------------------------
type Prolog m a = ListT (StateT (Identifier :--> Identifier,[Identifier]) m) a
--type Prolog m a = ListT (StateT (Identifier :--> Identifier,[Identifier]) (StateT Bool m)) a

type Database = [((Name, Arity), [(Term, [Term])])]

--cut = lift $ lift $ put True
--uncut = lift $ lift $ put False
--branch p q = do b <- lift $ lift $ get ; if b then p else q

clause :: Database -> (Name,Arity) -> Prolog Identity (Term, [Term])
clause db functor = ListT . mapM copyRule $ lookup' db functor
lookup' q db = maybe [] id (lookup db q)

(?-) :: (Database,Term -> Term) -> Term -> Prolog Identity (Term -> Term)
--(db,σ) ?- (("!",0):>[]) = do cut ; return σ
(db,σ) ?- query = do (head,body) <- clause db (functor query)
                     σ <- (head ≡ query) σ
                     foldM (prove db) σ body

prove db σ query = (db,σ) ?- (σ⤴ query)

runQuery db query = map (⤴ query).
  runIdentity.
--    flip evalStateT False.
      withGensyms (names \\ variables query).
        runListT$
          (db,id) ?- query
------------------------------------------------------------------------------------------

------------------------------------------------------------------------------------------
data Syntax = Term :- [Term]
makeRule (head :- body) = (functor head,[(head,body)])
mergeGroups ((functor,body):rest) = (functor,concat (body:map snd rest))
exampleDb :: Database
exampleDb = map mergeGroups $ groupBy fst $ map makeRule
 [true :- [],
 
  Var "X" == Var "X" :- [],
  
  call(Var "P") :- [Var "P"],
  
  and(Var "This",Var "That") :- [Var "This", Var "That"],
  
  or(Var "This",Var "That") :- [Var "This"],
  or(Var "This",Var "That") :- [Var "That"],
  
--  not(Var "P") :- [call(Var "P"), (!), fail],
--  not(Var "P") :- [],
  
  flip(heads) :- [],
  flip(tails) :- [],
  
  n(z) :- [],
  n(s(Var "N")) :- [n(Var "N")],
  
  member(Var"E", Var "E" . Var "Xs") :- [],
  member(Var"E", Var "X" . Var "Xs") :- [member(Var "E",Var "Xs")],
  
  append(nil,               Var "Ys",Var "Ys") :- [],
  append(Var "X" . Var "XS",Var "YS",Var "X" . Var "Zs") :- [append(Var "XS",Var "YS",Var "Zs")] 
  
  ] where true = ("true",0):>[];fail = ("fail",0):>[]
          x==y = ("=",2):>[x,y]
          call(p) = ("call",1):>[p];flip(p) = ("flip",1):>[p];not(p) = ("not",1):>[p]
          (!) = ("!",0):>[];heads = ("heads",0):>[];tails = ("tails",0):>[]
          and(p,q) = (",",2):>[p,q];or(p,q) = (";",2):>[p,q]
          member(x,y) = ("member",2):>[x,y];append(x,y,z) = ("append",3):>[x,y,z]
          nil = ("[]",0):>[];t . ts = (".",2):>[t,ts]
          z = ("z",0):>[];s(x) = ("s",1):>[x];n(x) = ("n",1):>[x]

instance Show Syntax where
  show (head :- []) = show head ++ "."
  show (head :- body) = show head ++ " :- " ++ intercalate ", " (map show body) ++ "."

showDb = unlines (map show exampleDb)
------------------------------------------------------------------------------------------

HOAS based self interpreter for lambda calculus

Just copied this out of Self-applicable Partial Evaluation for Pure Lambda Calculus

(define-syntax Q ; quote a lambda term
  (syntax-rules (lambda)
    ((Q (lambda (x) M)) (lambda (a)
                          (lambda (b)
                            (lambda (c)
                              (a (lambda (x) (Q M)))))))
    ((Q (M N)) (lambda (a)
                 (lambda (b)
                   (lambda (c)
                     ((b (Q M)) (Q N))))))
    ((Q x) (lambda (a)
             (lambda (b)
               (lambda (c)
                 (c x)))))))

(define E ; evaluate a quoted lambda term
  ((lambda (m)
    ((lambda (f) (m (lambda (a) ((f f) a))))
     (lambda (f) (m (lambda (a) ((f f) a))))))
   (lambda (E)
     (lambda (t)
       (((t (lambda (M) (lambda (x) (E (M x)))))
         (lambda (M) (lambda (N) ((E M) (E N)))))
        (lambda (x) x))))))

(define test-1
  (E (Q (lambda (i) i))))

(define test-2
  (E (Q (((lambda (m)
            ((lambda (f) (m (lambda (a) ((f f) a))))
             (lambda (f) (m (lambda (a) ((f f) a))))))
          (lambda (E)
            (lambda (t)
              (((t (lambda (M) (lambda (x) (E (M x)))))
                (lambda (M) (lambda (N) ((E M) (E N)))))
               (lambda (x) x)))))
         (lambda (a) (lambda (b) (lambda (c) (a (lambda (i) (lambda (a) (lambda (b) (lambda (c) (c i)))))))))))))

; ((lambda (i) i) 'ok)
; ok 
; > (test-1 'ok)
; ok
; > (test-2 'ok)
; ok

Rascal - Mini-haskell like language

http://rascal-haskell.googlecode.com/files/Rascal.zip
http://code.google.com/p/rascal-haskell/source/checkout

Thank you to google for hosting this.

more code: http://code.google.com/p/janus-haskell/

more still: http://prolog-thoughts.googlecode.com/files/Prolog.zip

How could I fix this line spacing?

The line spacing is huge now for no reason, how do I change it back? :/
not that anyone reads this anyway..