GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-05-23 09:52:55 -06:00
Code Issues Packages Projects Releases Wiki Activity

even simpler version of NQueens

Browse Source
This commit is contained in:
krasimir
2010-03-24 21:04:37 +00:00
parent 9a1d0e8d11
commit 887a552497
4 changed files with 5 additions and 11 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
examples/nqueens/NQueens.gf
View File

@@ -6,7 +6,9 @@ cat Vec (s,l : Nat) Constr ;
cat Sat Nat Nat Constr ; cat Sat Nat Nat Constr ;
data nilV : (s : Nat) -> (c : Constr) -> Vec s zero c ; data nilV : (s : Nat) -> (c : Constr) -> Vec s zero c ;
consV : (s,l,j : Nat) -> (c : Constr) -> LT j s -> Sat j (succ zero) c -> Vec s l (consC j c) -> Vec s (succ l) c ; consV : (l,j,k : Nat) ->
let s = succ (plus j k)
in (c : Constr) -> Sat j (succ zero) c -> Vec s l (consC j c) -> Vec s (succ l) c ;
nilC : Constr ; nilC : Constr ;
consC : (j : Nat) -> Constr -> Constr ; consC : (j : Nat) -> Constr -> Constr ;

2
examples/nqueens/NQueensAscii.gf
View File

@@ -4,7 +4,7 @@ lincat Matrix, Vec = Str ;
Constr, Sat = {} ; Constr, Sat = {} ;
lin nilV _ _ = "" ; lin nilV _ _ = "" ;
consV _ _ f _ l _ v = f ++ "X" ++ l ++ "\n" ++ v ; consV _ j k _ _ v = j ++ "X" ++ k ++ "\n" ++ v ;
matrix _ v = v ; matrix _ v = v ;

4
examples/nqueens/Nat.gf
View File

@@ -6,15 +6,11 @@ data zero : Nat ;
succ : Nat -> Nat ; succ : Nat -> Nat ;
cat NE (i,j : Nat) ; cat NE (i,j : Nat) ;
cat LT (i,j : Nat) ;
data zNE : (i,j : Nat) -> NE i j -> NE (succ i) (succ j) ; data zNE : (i,j : Nat) -> NE i j -> NE (succ i) (succ j) ;
lNE : (j : Nat) -> NE zero (succ j) ; lNE : (j : Nat) -> NE zero (succ j) ;
rNE : (j : Nat) -> NE (succ j) zero ; 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) ;
fun plus : Nat -> Nat -> Nat ; fun plus : Nat -> Nat -> Nat ;
def plus zero n = n ; def plus zero n = n ;
plus (succ m) n = succ (plus m n) ; plus (succ m) n = succ (plus m n) ;

6
examples/nqueens/NatAscii.gf
View File

@@ -5,10 +5,6 @@ lincat Nat = Str ;
lin zero = "" ; lin zero = "" ;
succ n = "_" ++ n ; succ n = "_" ++ n ;
lincat LT = Str ; lincat NE = {} ;
NE = {} ;
lin zLT n = n ;
sLT _ _ l = l ;
} }