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

the Plus predicate from NQueens is replaced with definition for function plus

Browse Source
This commit is contained in:
krasimir
2010-03-24 16:14:36 +00:00
parent 17897bc286
commit 925fb9dc85
3 changed files with 5 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files

4
examples/nqueens/NQueens.gf
View File

@@ -6,13 +6,13 @@ 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 ;
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 ;
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) ;
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 ;

6
examples/nqueens/Nat.gf
View File

@@ -7,7 +7,6 @@ data zero : 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) ;
@@ -16,7 +15,8 @@ data zNE : (i,j : Nat) -> NE i j -> NE (succ i) (succ j) ;
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) ;
fun plus : Nat -> Nat -> Nat ;
def plus zero n = n ;
plus (succ m) n = succ (plus m n) ;
}

1
examples/nqueens/NatAscii.gf
View File

@@ -7,7 +7,6 @@ lin zero = "" ;
lincat LT = Str ;
NE = {} ;
Plus = {} ;
lin zLT n = n ;
sLT _ _ l = l ;