the NQueens algorithm written in GF

examples/nqueens/NQueens.gf

@@ -0,0 +1,19 @@
+abstract NQueens = Nat ** {
+
+cat Matrix Nat ;
+cat Constr ;
+cat Vec (s,l : Nat) Constr ;
+cat Sat Nat Nat Constr ;
+
+data nilV  : (s : Nat) -> (c : Constr) -> Vec s zero c ;
+     consV : (s,l : Nat) -> (j : Nat) -> (c : Constr) -> LT j s -> Sat j (succ zero) c -> Vec s l (consC j c) -> Vec s (succ l) c ;
+
+     nilC  : Constr ;
+     consC : (j : Nat) -> Constr -> Constr ;
+
+     nilS : (j,d : Nat) -> Sat j d nilC ;
+     consS : (i,j : Nat) -> (d,dj,di : Nat) -> (c : Constr) -> NE i j -> Plus d j dj -> Plus d i di -> NE i dj -> NE di j -> Sat j (succ d) c -> Sat j d (consC i c) ;
+
+     matrix : (s : Nat) -> Vec s s nilC -> Matrix s ;
+
+}

examples/nqueens/NQueensAscii.gf

@@ -0,0 +1,11 @@
+concrete NQueensAscii of NQueens = NatAscii ** {
+
+lincat Matrix, Vec = Str ;
+       Constr, Sat = {} ;
+
+lin nilV _ _ = "" ;
+    consV _ _ f _ l _ v = f ++ "X" ++ l ++ "\n" ++ v ;
+
+    matrix _ v = v ;
+
+}

examples/nqueens/Nat.gf

@@ -0,0 +1,22 @@
+abstract Nat = {
+
+cat Nat ;
+
+data zero : Nat ;
+     succ : Nat -> Nat ;
+
+cat NE (i,j : Nat) ;
+cat LT (i,j : Nat) ;
+cat Plus Nat Nat Nat ;
+
+data zNE : (i,j : Nat) -> NE i j -> NE (succ i) (succ j) ;
+     lNE : (j : Nat) -> NE zero (succ j) ;
+     rNE : (j : Nat) -> NE (succ j) zero ;
+
+     zLT : (n : Nat) -> LT zero (succ n) ;
+     sLT : (m,n : Nat) -> LT m n -> LT (succ m) (succ n) ;
+
+     zP : (n : Nat) -> Plus zero n n ;
+     sP : (m,n,s : Nat) -> Plus m n s -> Plus (succ m) n (succ s) ;
+
+}

examples/nqueens/NatAscii.gf

@@ -0,0 +1,15 @@
+concrete NatAscii of Nat = {
+
+lincat Nat = Str ;
+
+lin zero   = "" ;
+    succ n = "_" ++ n ;
+
+lincat LT = Str ;
+       NE = {} ;
+       Plus = {} ;
+
+lin zLT n = n ;
+    sLT _ _ l = l ;
+
+}