GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-04-23 19:42:50 -06:00
Code Issues Packages Projects Releases Wiki Activity

the NQueens algorithm written in GF

Browse Source
This commit is contained in:
krasimir
2010-03-21 19:01:57 +00:00
parent 5c9062f5ea
commit f4d3da0ccc
4 changed files with 67 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

19
examples/nqueens/NQueens.gf Normal file
View File

@@ -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 ;
}