Commit 1bf3ca02 authored by Gaspard Ferey's avatar Gaspard Ferey

Makefile and a couple of examples.

parent dd9ab2f9
DKCHECK=dkcheck
all : empty easy medium hardest
empty : solve_empty.dko
easy : solve_easy.dko
medium : solve_medium.dko
hardest: solve_hardest.dko
sudoku.dko : sudoku.dk
$(DKCHECK) -nl -e sudoku.dk
%.dko: %.dk sudoku.dko
$(DKCHECK) $<
clean:
rm -rf *.dko
def 1 := sudoku.1.
def 2 := sudoku.2.
def 3 := sudoku.3.
def 4 := sudoku.4.
def 5 := sudoku.5.
def 6 := sudoku.6.
def 7 := sudoku.7.
def 8 := sudoku.8.
def 9 := sudoku.9.
def X := sudoku.X.
def l := sudoku.l.
def c := sudoku.c.
def sudoku :=
c (l X X X 2 6 X 7 X 1)
(l 6 8 X X 7 X X 9 X)
(l 1 9 X X X 4 5 X X)
(l 8 2 X 1 X X X 4 X)
(l X X 4 6 X 2 9 X X)
(l X 5 X X X 3 X 2 8)
(l X X 9 3 X X X 7 4)
(l X 4 X X 5 X X 3 6)
(l 7 X 3 X 1 8 X X X).
#EVAL sudoku.solve_sudo sudoku.
#EVAL sudoku.solve_sudo sudoku.empty_sudo.
(;
c (l 1 2 3 4 5 6 7 8 9)
(l 4 5 6 7 8 9 1 2 3)
(l 7 8 9 1 2 3 4 5 6)
(l 2 1 4 3 6 5 8 9 7)
(l 3 6 5 8 9 7 2 1 4)
(l 8 9 7 2 1 4 3 6 5)
(l 5 3 1 6 4 2 9 7 8)
(l 6 4 2 9 7 8 5 3 1)
(l 9 7 8 5 3 1 6 4 2)
;)
def 1 := sudoku.1.
def 2 := sudoku.2.
def 3 := sudoku.3.
def 4 := sudoku.4.
def 5 := sudoku.5.
def 6 := sudoku.6.
def 7 := sudoku.7.
def 8 := sudoku.8.
def 9 := sudoku.9.
def X := sudoku.X.
def l := sudoku.l.
def c := sudoku.c.
def sudoku :=
c (l 8 X X X X X X X X)
(l X X 3 6 X X X X X)
(l X 7 X X 9 X 2 X X)
(l X 5 X X X 7 X X X)
(l X X X X 4 5 7 X X)
(l X X X 1 X X X 3 X)
(l X X 1 X X X X 6 8)
(l X X 8 5 X X X 1 X)
(l X 9 X X X X 4 X X).
#EVAL sudoku.solve_sudo sudoku.
def 1 := sudoku.1.
def 2 := sudoku.2.
def 3 := sudoku.3.
def 4 := sudoku.4.
def 5 := sudoku.5.
def 6 := sudoku.6.
def 7 := sudoku.7.
def 8 := sudoku.8.
def 9 := sudoku.9.
def X := sudoku.X.
def l := sudoku.l.
def c := sudoku.c.
def sudoku :=
c (l X 2 X 6 X 8 X X X)
(l 5 8 X X X 9 7 X X)
(l X X X X 4 X X X X)
(l 3 7 X X X X 6 X X)
(l 6 X X X X X X X 4)
(l X X 8 X X X X 1 3)
(l X X X X 2 X X X X)
(l X X 9 8 X X X 3 6)
(l X X X 3 X 6 X 9 X).
#EVAL sudoku.solve_sudo sudoku.
ind : Type.
1 : ind.
2 : ind.
......@@ -37,11 +33,15 @@ def S : ind -> ind.
[] S 9 --> X.
def trunc3 : ind -> ind.
[] trunc3 X --> X.
[] trunc3 1 --> 1.
[] trunc3 4 --> 1.
[] trunc3 7 --> 1.
[i] trunc3 i --> P i.
[] trunc3 1 --> 1
[] trunc3 2 --> 1
[] trunc3 3 --> 1
[] trunc3 4 --> 4
[] trunc3 5 --> 4
[] trunc3 6 --> 4
[] trunc3 7 --> 7
[] trunc3 8 --> 7
[] trunc3 9 --> 7.
bool : Type.
T : bool.
......@@ -64,37 +64,73 @@ def eq : ind -> ind -> bool.
[x,y] eq x y --> F.
def ite : A : Type -> bool -> A -> A -> A.
[A,x] ite A T x _ --> x
[A,x] ite A F _ x --> x.
ind_list : Type.
Empty' : ind_list.
Cons' : ind -> ind_list -> ind_list.
line : Type.
l : ind -> ind -> ind -> ind -> ind -> ind -> ind -> ind -> ind -> line.
sudo : Type.
Empty : sudo.
Cons : ind_list -> sudo -> sudo.
def sudo : Type.
def c : line -> line -> line -> line -> line -> line -> line -> line -> line -> sudo.
def getl : ind -> line -> ind.
[x] getl 1 (l x _ _ _ _ _ _ _ _) --> x
[x] getl 2 (l _ x _ _ _ _ _ _ _) --> x
[x] getl 3 (l _ _ x _ _ _ _ _ _) --> x
[x] getl 4 (l _ _ _ x _ _ _ _ _) --> x
[x] getl 5 (l _ _ _ _ x _ _ _ _) --> x
[x] getl 6 (l _ _ _ _ _ x _ _ _) --> x
[x] getl 7 (l _ _ _ _ _ _ x _ _) --> x
[x] getl 8 (l _ _ _ _ _ _ _ x _) --> x
[x] getl 9 (l _ _ _ _ _ _ _ _ x) --> x.
def getc : ind -> sudo -> line.
[x] getc 1 (c x _ _ _ _ _ _ _ _) --> x
[x] getc 2 (c _ x _ _ _ _ _ _ _) --> x
[x] getc 3 (c _ _ x _ _ _ _ _ _) --> x
[x] getc 4 (c _ _ _ x _ _ _ _ _) --> x
[x] getc 5 (c _ _ _ _ x _ _ _ _) --> x
[x] getc 6 (c _ _ _ _ _ x _ _ _) --> x
[x] getc 7 (c _ _ _ _ _ _ x _ _) --> x
[x] getc 8 (c _ _ _ _ _ _ _ x _) --> x
[x] getc 9 (c _ _ _ _ _ _ _ _ x) --> x.
def setl : ind -> ind -> line -> line.
[k,x1,x2,x3,x4,x5,x6,x7,x8,x9] setl 1 k (l x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l k x2 x3 x4 x5 x6 x7 x8 x9)
[k,x1,x2,x3,x4,x5,x6,x7,x8,x9] setl 2 k (l x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l x1 k x3 x4 x5 x6 x7 x8 x9)
[k,x1,x2,x3,x4,x5,x6,x7,x8,x9] setl 3 k (l x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l x1 x2 k x4 x5 x6 x7 x8 x9)
[k,x1,x2,x3,x4,x5,x6,x7,x8,x9] setl 4 k (l x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l x1 x2 x3 k x5 x6 x7 x8 x9)
[k,x1,x2,x3,x4,x5,x6,x7,x8,x9] setl 5 k (l x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l x1 x2 x3 x4 k x6 x7 x8 x9)
[k,x1,x2,x3,x4,x5,x6,x7,x8,x9] setl 6 k (l x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l x1 x2 x3 x4 x5 k x7 x8 x9)
[k,x1,x2,x3,x4,x5,x6,x7,x8,x9] setl 7 k (l x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l x1 x2 x3 x4 x5 x6 k x8 x9)
[k,x1,x2,x3,x4,x5,x6,x7,x8,x9] setl 8 k (l x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l x1 x2 x3 x4 x5 x6 x7 k x9)
[k,x1,x2,x3,x4,x5,x6,x7,x8,x9] setl 9 k (l x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l x1 x2 x3 x4 x5 x6 x7 x8 k ).
def setc : ind -> (line -> line) -> sudo -> sudo.
[k,x1,x2,x3,x4,x5,x6,x7,x8,x9] setc 1 k (c x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (c (k x1) x2 x3 x4 x5 x6 x7 x8 x9)
[k,x1,x2,x3,x4,x5,x6,x7,x8,x9] setc 2 k (c x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (c x1 (k x2) x3 x4 x5 x6 x7 x8 x9)
[k,x1,x2,x3,x4,x5,x6,x7,x8,x9] setc 3 k (c x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (c x1 x2 (k x3) x4 x5 x6 x7 x8 x9)
[k,x1,x2,x3,x4,x5,x6,x7,x8,x9] setc 4 k (c x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (c x1 x2 x3 (k x4) x5 x6 x7 x8 x9)
[k,x1,x2,x3,x4,x5,x6,x7,x8,x9] setc 5 k (c x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (c x1 x2 x3 x4 (k x5) x6 x7 x8 x9)
[k,x1,x2,x3,x4,x5,x6,x7,x8,x9] setc 6 k (c x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (c x1 x2 x3 x4 x5 (k x6) x7 x8 x9)
[k,x1,x2,x3,x4,x5,x6,x7,x8,x9] setc 7 k (c x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (c x1 x2 x3 x4 x5 x6 (k x7) x8 x9)
[k,x1,x2,x3,x4,x5,x6,x7,x8,x9] setc 8 k (c x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (c x1 x2 x3 x4 x5 x6 x7 (k x8) x9)
[k,x1,x2,x3,x4,x5,x6,x7,x8,x9] setc 9 k (c x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (c x1 x2 x3 x4 x5 x6 x7 x8 (k x9) ).
def E : ind_list :=
Cons' X (Cons' X (Cons' X (Cons' X (Cons' X (Cons' X (Cons' X (Cons' X (Cons' X Empty')))))))).
def empty_sudo : sudo :=
Cons E (Cons E (Cons E (Cons E (Cons E (Cons E (Cons E (Cons E (Cons E Empty )))))))).
def set' : ind -> ind -> ind_list -> ind_list.
[j,k,a,l] set' j k (Cons' a l) --> ite ind_list (eq j 1) (Cons' k l) (Cons' a (set' (P j) k l)).
def set : ind -> ind -> ind -> sudo -> sudo.
[i,j,k,a,l] set i j k (Cons a l) --> ite sudo (eq i 1) (Cons (set' j k a) l) (Cons a (set (P i) j k l)).
def get' : ind -> ind_list -> ind.
[j,a,l] get' j (Cons' a l) --> ite ind (eq j 1) a (get' (P j) l).
def E : line := l X X X X X X X X X.
def empty_sudo : sudo := c E E E E E E E E E.
def get : ind -> ind -> sudo -> ind.
[i,j,a,l] get i j (Cons a l) --> ite ind (eq i 1) (get' j a) (get (P i) j l).
[i,j,s] get i j s --> getl j (getc i s).
def set : ind -> ind -> ind -> sudo -> sudo.
[i,j,k,s] set i j k s --> setc i (setl j k) s.
def exists' : (ind -> bool) -> ind -> bool.
......@@ -104,6 +140,7 @@ def exists' : (ind -> bool) -> ind -> bool.
def exists : (ind -> bool) -> bool := f => exists' f 1.
def mem_line : ind -> ind -> ind -> sudo -> bool.
[i,j,k,s] mem_line i j k s --> exists (i' => eq (get i' j s) k).
......@@ -114,20 +151,19 @@ def mem_squ : ind -> ind -> ind -> sudo -> bool.
[i,j,k,s] mem_squ i j k s -->
(i':ind =>
j':ind =>
or (or (eq (get i' j' s) k)
(or (eq (get (S i') j' s) k)
(eq (get (S (S i')) j' s) k)))
(or (or (eq (get i' (S j') s) k)
(or (eq (get (S i') (S j') s) k)
(eq (get (S (S i')) (S j') s) k)))
(or (eq (get i' (S (S j')) s) k)
(or (eq (get (S i') (S (S j')) s) k)
(eq (get (S (S i')) (S (S j')) s) k))))
(or (eq (get i' j' s) k)
(or (eq (get (S i') j' s) k)
(or (eq (get (S (S i')) j' s) k)
(or (eq (get i' (S j') s) k)
(or (eq (get (S i') (S j') s) k)
(or (eq (get (S (S i')) (S j') s) k)
(or (eq (get i' (S (S j')) s) k)
(or (eq (get (S i') (S (S j')) s) k)
(eq (get (S (S i')) (S (S j')) s) k)))))))))
)
(trunc3 i) (trunc3 j).
def check : ind -> ind -> ind -> sudo -> bool :=
i => j => k => s =>
and (not (mem_line i j k s))
......@@ -140,6 +176,10 @@ success : sudo -> solution.
fail : solution.
def ite : bool -> solution -> solution -> solution.
[x] ite T x _ --> x
[x] ite F _ x --> x.
def iffail : solution -> solution -> solution.
[x] iffail (success x) _ --> success x
[d] iffail fail d --> d.
......@@ -149,9 +189,9 @@ def solve : ind -> ind -> ind -> sudo -> solution.
[ s] solve X _ _ s --> success s.
[i,j,s] solve i j X s --> fail.
[i,j,k,s] solve i j k s -->
ite solution
ite
(eq (get i j s) X)
(ite solution
(ite
(check i j k s)
(iffail
(solve i (S j) 1 (set i j k s))
......@@ -163,13 +203,3 @@ def solve : ind -> ind -> ind -> sudo -> solution.
def solve_sudo : sudo -> solution := s => solve 1 1 1 s.
def extract_sol : solution -> sudo.
[x] extract_sol (success x) --> x.
def sol := solve_sudo empty_sudo.
#EVAL sol.
ind : Type.
1 : ind.
2 : ind.
......@@ -33,15 +37,11 @@ def S : ind -> ind.
[] S 9 --> X.
def trunc3 : ind -> ind.
[] trunc3 1 --> 1
[] trunc3 2 --> 1
[] trunc3 3 --> 1
[] trunc3 4 --> 4
[] trunc3 5 --> 4
[] trunc3 6 --> 4
[] trunc3 7 --> 7
[] trunc3 8 --> 7
[] trunc3 9 --> 7.
[] trunc3 X --> X.
[] trunc3 1 --> 1.
[] trunc3 4 --> 1.
[] trunc3 7 --> 1.
[i] trunc3 i --> P i.
bool : Type.
T : bool.
......@@ -69,43 +69,32 @@ def ite : A : Type -> bool -> A -> A -> A.
[A,x] ite A F _ x --> x.
list : A : Type -> Type.
l : A : Type -> A -> A -> A -> A -> A -> A -> A -> A -> A -> list A.
ind_list : Type.
Empty' : ind_list.
Cons' : ind -> ind_list -> ind_list.
def get' : A : Type -> ind -> list A -> A.
[A,x] get' A 1 (l A x _ _ _ _ _ _ _ _) --> x
[A,x] get' A 2 (l A _ x _ _ _ _ _ _ _) --> x
[A,x] get' A 3 (l A _ _ x _ _ _ _ _ _) --> x
[A,x] get' A 4 (l A _ _ _ x _ _ _ _ _) --> x
[A,x] get' A 5 (l A _ _ _ _ x _ _ _ _) --> x
[A,x] get' A 6 (l A _ _ _ _ _ x _ _ _) --> x
[A,x] get' A 7 (l A _ _ _ _ _ _ x _ _) --> x
[A,x] get' A 8 (l A _ _ _ _ _ _ _ x _) --> x
[A,x] get' A 9 (l A _ _ _ _ _ _ _ _ x) --> x.
sudo : Type.
Empty : sudo.
Cons : ind_list -> sudo -> sudo.
def set' : A : Type -> ind -> (A -> A) -> list A -> list A.
[A,k,x1,x2,x3,x4,x5,x6,x7,x8,x9] set' A 1 k (l A x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l A (k x1) x2 x3 x4 x5 x6 x7 x8 x9)
[A,k,x1,x2,x3,x4,x5,x6,x7,x8,x9] set' A 2 k (l A x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l A x1 (k x2) x3 x4 x5 x6 x7 x8 x9)
[A,k,x1,x2,x3,x4,x5,x6,x7,x8,x9] set' A 3 k (l A x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l A x1 x2 (k x3) x4 x5 x6 x7 x8 x9)
[A,k,x1,x2,x3,x4,x5,x6,x7,x8,x9] set' A 4 k (l A x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l A x1 x2 x3 (k x4) x5 x6 x7 x8 x9)
[A,k,x1,x2,x3,x4,x5,x6,x7,x8,x9] set' A 5 k (l A x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l A x1 x2 x3 x4 (k x5) x6 x7 x8 x9)
[A,k,x1,x2,x3,x4,x5,x6,x7,x8,x9] set' A 6 k (l A x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l A x1 x2 x3 x4 x5 (k x6) x7 x8 x9)
[A,k,x1,x2,x3,x4,x5,x6,x7,x8,x9] set' A 7 k (l A x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l A x1 x2 x3 x4 x5 x6 (k x7) x8 x9)
[A,k,x1,x2,x3,x4,x5,x6,x7,x8,x9] set' A 8 k (l A x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l A x1 x2 x3 x4 x5 x6 x7 (k x8) x9)
[A,k,x1,x2,x3,x4,x5,x6,x7,x8,x9] set' A 9 k (l A x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l A x1 x2 x3 x4 x5 x6 x7 x8 (k x9) ).
def E : ind_list :=
Cons' X (Cons' X (Cons' X (Cons' X (Cons' X (Cons' X (Cons' X (Cons' X (Cons' X Empty')))))))).
def empty_sudo : sudo :=
Cons E (Cons E (Cons E (Cons E (Cons E (Cons E (Cons E (Cons E (Cons E Empty )))))))).
def set' : ind -> ind -> ind_list -> ind_list.
[j,k,a,l] set' j k (Cons' a l) --> ite ind_list (eq j 1) (Cons' k l) (Cons' a (set' (P j) k l)).
def set : ind -> ind -> ind -> sudo -> sudo.
[i,j,k,a,l] set i j k (Cons a l) --> ite sudo (eq i 1) (Cons (set' j k a) l) (Cons a (set (P i) j k l)).
def sudo : Type := list (list ind).
def E : list ind := l ind X X X X X X X X X.
def empty_sudo : sudo := l (list ind) E E E E E E E E E.
def get' : ind -> ind_list -> ind.
[j,a,l] get' j (Cons' a l) --> ite ind (eq j 1) a (get' (P j) l).
def get : ind -> ind -> sudo -> ind.
[i,j,s] get i j s --> (get' ind j (get' (list ind) i s)).
[i,j,a,l] get i j (Cons a l) --> ite ind (eq i 1) (get' j a) (get (P i) j l).
def set : ind -> ind -> ind -> sudo -> sudo.
[i,j,k,s] set i j k s --> set' (list ind) i (set' ind j (x => k)) s.
def exists' : (ind -> bool) -> ind -> bool.
......@@ -115,7 +104,6 @@ def exists' : (ind -> bool) -> ind -> bool.
def exists : (ind -> bool) -> bool := f => exists' f 1.
def mem_line : ind -> ind -> ind -> sudo -> bool.
[i,j,k,s] mem_line i j k s --> exists (i' => eq (get i' j s) k).
......@@ -123,29 +111,23 @@ def mem_col : ind -> ind -> ind -> sudo -> bool.
[i,j,k,s] mem_col i j k s --> exists (j' => eq (get i j' s) k).
def mem_squ : ind -> ind -> ind -> sudo -> bool.
[i,j,k,s] mem_squ i j k s --> F.
def mem_squ2 : ind -> ind -> ind -> sudo -> bool.
[i,j,k,s] mem_squ2 i j k s -->
[i,j,k,s] mem_squ i j k s -->
(i':ind =>
j':ind =>
(or (eq (get i' j' s) k)
(or (eq (get (S i') j' s) k)
(or (eq (get (S (S i')) j' s) k)
(or (eq (get i' (S j') s) k)
(or (eq (get (S i') (S j') s) k)
(or (eq (get (S (S i')) (S j') s) k)
(or (eq (get i' (S (S j')) s) k)
(or (eq (get (S i') (S (S j')) s) k)
(eq (get (S (S i')) (S (S j')) s) k)))))))))
or (or (eq (get i' j' s) k)
(or (eq (get (S i') j' s) k)
(eq (get (S (S i')) j' s) k)))
(or (or (eq (get i' (S j') s) k)
(or (eq (get (S i') (S j') s) k)
(eq (get (S (S i')) (S j') s) k)))
(or (eq (get i' (S (S j')) s) k)
(or (eq (get (S i') (S (S j')) s) k)
(eq (get (S (S i')) (S (S j')) s) k))))
)
(trunc3 i) (trunc3 j).
def check : ind -> ind -> ind -> sudo -> bool :=
i => j => k => s =>
and (not (mem_line i j k s))
......@@ -191,8 +173,3 @@ def extract_sol : solution -> sudo.
def sol := solve_sudo empty_sudo.
#EVAL sol.
#EVAL[SNF,1] get 2 2 (extract_sol sol).
#EVAL[SNF,2] get 2 2 (extract_sol sol).
#EVAL[SNF,3] get 2 2 (extract_sol sol).
#EVAL[WHNF,4] mem_squ2 2 2 3 (extract_sol sol).
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment