msyds/gf-core
1
0
Fork 0
forked from GitHub/gf-core
Code Pull Requests Activity

update NQueens to use: 1) lists i.e. [Nat]; 2) implicit arguments

Browse Source
This commit is contained in:
krasimir
2010-10-11 17:17:04 +00:00
parent e7f6239bc6
commit c145f18a19
2 changed files with 12 additions and 15 deletions
Download Patch File Download Diff File Expand all files Collapse all files

23
examples/nqueens/NQueens.gf
View File

@@ -1,21 +1,18 @@
abstract NQueens = Nat ** { abstract NQueens = Nat ** {
cat Matrix Nat ; cat Matrix Nat ;
cat Constr ; cat [Nat] ;
cat Vec (s,l : Nat) Constr ; cat Vec (s,l : Nat) [Nat] ;
cat Sat Nat Nat Constr ; cat Sat Nat Nat [Nat] ;
data nilV : (s : Nat) -> (c : Constr) -> Vec s zero c ; data nilV : ({s} : Nat) -> ({c} : [Nat]) -> Vec s zero c ;
consV : (l,j,k : Nat) -> consV : ({l},j,k : Nat) ->
let s = succ (plus j k) 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 ; in ({c} : [Nat]) -> Sat j (succ zero) c -> Vec s l (ConsNat j c) -> Vec s (succ l) c ;
nilC : Constr ; nilS : ({j,d} : Nat) -> Sat j d BaseNat ;
consC : (j : Nat) -> Constr -> Constr ; consS : ({i,j,d} : Nat) -> ({c} : [Nat]) -> NE i j -> NE i (plus d j) -> NE (plus d i) j -> Sat j (succ d) c -> Sat j d (ConsNat i c) ;
nilS : (j,d : Nat) -> Sat j d nilC ; matrix : ({s} : Nat) -> Vec s s BaseNat -> Matrix s ;
consS : (i,j,d : Nat) -> (c : Constr) -> NE i j -> NE i (plus d j) -> NE (plus d i) j -> Sat j (succ d) c -> Sat j d (consC i c) ;
matrix : (s : Nat) -> Vec s s nilC -> Matrix s ; }
}

4
examples/nqueens/NQueensAscii.gf
View File

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