GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-04-09 04:59:31 -06:00
Code Issues Packages Projects Releases Wiki 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 f305587a62
commit 3ac637ddcb
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 ** {
cat Matrix Nat ;
cat Constr ;
cat Vec (s,l : Nat) Constr ;
cat Sat Nat Nat Constr ;
cat [Nat] ;
cat Vec (s,l : Nat) [Nat] ;
cat Sat Nat Nat [Nat] ;
data nilV : (s : Nat) -> (c : Constr) -> Vec s zero c ;
consV : (l,j,k : Nat) ->
data nilV : ({s} : Nat) -> ({c} : [Nat]) -> Vec s zero 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 ;
in ({c} : [Nat]) -> Sat j (succ zero) c -> Vec s l (ConsNat j c) -> Vec s (succ l) c ;
nilC : Constr ;
consC : (j : Nat) -> Constr -> Constr ;
nilS : ({j,d} : Nat) -> Sat j d BaseNat ;
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 ;
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 BaseNat -> Matrix s ;
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 ** {
lincat Matrix, Vec = Str ;
Constr, Sat = {} ;
ListNat, Sat = {} ;
lin nilV _ _ = "" ;
consV _ j k _ _ v = j ++ "X" ++ k ++ "\n" ++ v ;
matrix _ v = v ;
}
}