Commit e7d28795 authored by Damien Morard's avatar Damien Morard
Browse files

Improvement of the code example

parent cd94f483
...@@ -6,7 +6,7 @@ ...@@ -6,7 +6,7 @@
"repositoryURL": "https://github.com/kyouko-taiga/LogicKit", "repositoryURL": "https://github.com/kyouko-taiga/LogicKit",
"state": { "state": {
"branch": "master", "branch": "master",
"revision": "32b7b2cf30d44468cbb290fefb17ca2f2a1c6d4d", "revision": "da786139ba76313b1cd1fb956c1d4b7b63ad5ba7",
"version": null "version": null
} }
} }
......
import LogicKit import LogicKit
import LogicKitBuiltins
// Generator // Generator
let zero: Term = "zero" let zero: Term = "zero"
// Free variable // Free variables
let x: Term = .var("x") let x: Term = .var("x")
let y: Term = .var("y") let y: Term = .var("y")
let z: Term = .var("z") let z: Term = .var("z")
let empty: Term = "empty"
let res: Term = .var("res") let res: Term = .var("res")
let head: Term = .var("head") let head: Term = .var("head")
let tail: Term = .var("tail") let tail: Term = .var("tail")
// Literals
let empty: Term = "empty"
let null: Term = "null" let null: Term = "null"
// Easy way to write succ // Easy way to write succ
// succ(zero) -> .fact("succ", zero)
func succ(_ x: Term) -> Term { func succ(_ x: Term) -> Term {
return .fact("succ", x) return .fact("succ", x)
} }
...@@ -29,33 +31,42 @@ func n(_ x: Int) -> Term { ...@@ -29,33 +31,42 @@ func n(_ x: Int) -> Term {
: zero : zero
} }
// Construct a list with cons
// cons(head: zero, tail: empty) -> .fact("cons", zero, empty)
func cons(head: Term, tail: Term) -> Term { func cons(head: Term, tail: Term) -> Term {
return .fact("cons", head, tail) return .fact("cons", head, tail)
} }
let kb1: KnowledgeBase = [ let kb: KnowledgeBase = [
// Basic case for Nat: Generator
.fact("zero", zero), .fact("zero", zero),
// Function greater than
// Basic case + one rule
.fact("gt", succ(x), zero), .fact("gt", succ(x), zero),
.rule("gt", succ(x), succ(y)) { .rule("gt", succ(x), succ(y)) {
.fact("gt", x, y) .fact("gt", x, y)
}, },
// Function add (+)
.fact("add", zero, y, y), .fact("add", zero, y, y),
.rule("add", succ(x), y, z) { .rule("add", succ(x), y, z) {
.fact("add", x, succ(y), z) .fact("add", x, succ(y), z)
}, },
// Basic case for List: Generator
.fact("empty", empty), .fact("empty", empty),
// Function to know if an element is contained in a list
.fact("contains", cons(head: head, tail: tail), head), .fact("contains", cons(head: head, tail: tail), head),
.rule("contains", cons(head: head, tail: tail), x) { .rule("contains", cons(head: head, tail: tail), x) {
.fact("contains", tail, x) .fact("contains", tail, x)
}, },
// Function to compute max in a list
.fact("max", empty, null), .fact("max", empty, null),
.fact("max", cons(head: head, tail: empty), head), .fact("max", cons(head: head, tail: empty), head),
.rule("max", cons(head: head, tail: tail), x) { .rule("max", cons(head: head, tail: tail), x) {
...@@ -64,55 +75,110 @@ let kb1: KnowledgeBase = [ ...@@ -64,55 +75,110 @@ let kb1: KnowledgeBase = [
.rule("max", cons(head: head, tail: tail), head) { .rule("max", cons(head: head, tail: tail), head) {
.fact("max", tail, x) && .fact("gt", head, x) .fact("max", tail, x) && .fact("gt", head, x)
}, },
//// Alternative method to compute max
// .rule("max", cons(head: head, tail: tail), z) { // .rule("max", cons(head: head, tail: tail), z) {
// .fact("max", tail, x) && // .fact("max", tail, x) &&
// (.fact("gt", head, x) && z ~=~ head || .fact("gt", x, head) && z ~=~ x) // (.fact("gt", head, x) && z ~=~ head || .fact("gt", x, head) && z ~=~ x)
// }, // },
.fact("gt", "5", "4"),
.fact("gt", "5", "2"),
.fact("gt", "4", "2"),
] ]
var p1 = kb1.ask(.fact("gt", n(2), n(1))) // Tests on "Nat"
var p2 = kb1.ask(.fact("gt", n(1), n(2)))
var p3 = kb1.ask(.fact("gt", n(0), n(0)))
print("Does n(2) is greather than n(1) ? ", p1.next() != nil) // We test our gt function
print("Does n(1) is greather than n(2) ? ", p2.next() != nil) var gt0 = kb.ask(.fact("gt", n(0), n(0)))
print("Does n(0) is greather than n(0) ? ", p3.next() != nil) var gt1 = kb.ask(.fact("gt", n(2), n(1)))
var gt2 = kb.ask(.fact("gt", n(1), n(2)))
// Print results
print("Does n(0) is greather than n(0) ? ", gt0.next() != nil)
print("Does n(2) is greather than n(1) ? ", gt1.next() != nil)
print("Does n(1) is greather than n(2) ? ", gt2.next() != nil)
var p4 = kb1.ask(.fact("add", n(3), n(2), z)) // We test our add function, result will be in the z variable
var add1 = kb.ask(.fact("add", n(3), n(2), z))
for binding in p4 { // Care to use the same variable name between the ask request and the print binding
for binding in add1 {
print("Result of addition : ", binding["z"]!) print("Result of addition : ", binding["z"]!)
} }
/* --------------------------------------------------------------------- */ /* --------------------------------------------------------------------- */
// Tests on "List"
//let list0: Term = cons(head: n(2), tail: empty) let list0: Term = cons(head: n(2), tail: empty)
let list1: Term = cons(head: n(2), tail: cons(head: n(3), tail: cons(head: n(1), tail: empty))) let list1: Term = cons(head: n(2), tail: cons(head: n(3), tail: cons(head: n(1), tail: empty)))
//
//var r1 = kb1.ask(.fact("contains", list1, n(4))/*, logger: DefaultLogger(useFontAttributes: false)*/)
//
//print("Does n(4) in list ? ", r1.next() != nil)
var r2 = kb1.ask(.fact("max", list1, res), logger: DefaultLogger(useFontAttributes: true)) // Test to know if a list contain an element
var contains0 = kb.ask(.fact("contains", list0, n(3))/*, logger: DefaultLogger(useFontAttributes: false)*/)
var contains1 = kb.ask(.fact("contains", list1, n(3)))
print("Does list0 contains 3 ? ", contains0.next() != nil)
print("Does list1 contains 3 ? ", contains1.next() != nil)
var max0 = kb.ask(.fact("max", list0, res))
var max1 = kb.ask(.fact("max", list1, res))
for binding in r2 {
print(binding["res"]!) for binding in max0 {
print("Max of list0 is ", binding["res"]!)
break break
} }
//var r3 = kb1.ask(.fact("max", list0, res)) for binding in max1 {
// print("Max of list1 is ", binding["res"]!)
//for binding in r3 { break
// print(binding["res"]!) }
// break
//}
/* --------------------------------------------------------------------- */
// In this part, we show how we can use builtins types.
// It means LogicKit can use types as Nat or List.
// What we did until now is already integrated in LogicKit !
// You can see all of these information in: https://github.com/kyouko-taiga/LogicKit/tree/master/Sources/LogicKitBuiltins
// We use List and Nat that are directly implemented in LogicKit
// We can merge them with the operator "+". It works for every knowledge base
let kbEvolved = KnowledgeBase(knowledge: (List.axioms + Nat.axioms))
// Nat.from allow us to convert a swift int to a nat term in LogicKit
let query0 = Nat.add(Nat.from(2), Nat.from(1), x)
let res0 = kbEvolved.ask(query0)
// Function Nat.asSwiftInt convert a term (which is a Nat) into a classic swift int
// We use
for binding in res0 {
print("Result of addition : ", Nat.asSwiftInt(binding["x"]!)! )
}
// We can create a list with "List.from", which takes a list of Term
// So, if we want to use a list of Nat we have to convert Nat into Term before
let query1 = List.count(list: List.from(elements: [1,5,2,4].map(Nat.from)), count: x)
// query1 = query1_2
// let query1_2 = List.count(list: List.from(elements: [Nat.from(1), Nat.from(5), Nat.from(2), Nat.from(4)]), count: x)
let res1 = kbEvolved.ask(query1)
for binding in res1 {
print("Result of count : ", Nat.asSwiftInt(binding["x"]!)!)
}
// We create two lists and we concat them
let list2 = List.from(elements: [1,2,3].map(Nat.from))
let list3 = List.from(elements: [4,5,6].map(Nat.from))
let query2 = List.concat(list2, list3, x)
let res2 = kbEvolved.ask(query2)
for binding in res2 {
print("Result of concat : ", binding["x"]!)
}
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment