diff --git a/.gitignore b/.gitignore
index 39c9242..1a5f2ee 100644
--- a/.gitignore
+++ b/.gitignore
@@ -4,3 +4,4 @@ obj/
riderModule.iml
/_ReSharper.Caches/
.idea/
+*.user
diff --git a/FicroKanSharp.Test/FicroKanSharp.Test.fsproj b/FicroKanSharp.Test/FicroKanSharp.Test.fsproj
index 1c39d3c..0b0cb52 100644
--- a/FicroKanSharp.Test/FicroKanSharp.Test.fsproj
+++ b/FicroKanSharp.Test/FicroKanSharp.Test.fsproj
@@ -5,12 +5,13 @@
-
+
+
diff --git a/FicroKanSharp.Test/TestExamples.fs b/FicroKanSharp.Test/TestExamples.fs
new file mode 100644
index 0000000..e2d0683
--- /dev/null
+++ b/FicroKanSharp.Test/TestExamples.fs
@@ -0,0 +1,133 @@
+namespace FicroKanSharp.Test
+
+open FicroKanSharp
+open Xunit
+open FsUnitTyped
+
+module TestThing =
+
+ []
+ let ``Example from the docs`` () : unit =
+ let aAndB =
+ Goal.conj
+ (Goal.callFresh (fun x -> Goal.equiv (Term.Variable x) (Term.Literal 7)))
+ (Goal.callFresh (fun x -> Goal.disj (Goal.equiv (Term.Variable x) (Term.Literal 5)) (Goal.equiv (Term.Variable x) (Term.Literal 6))))
+
+ let u = Goal.evaluate aAndB State.empty
+ match u |> Stream.peel with
+ | None -> failwith "oh no"
+ | Some (s, rest) ->
+
+ s
+ |> Map.toList
+ |> shouldEqual
+ [
+ Variable.VariableCount 0, Term.Literal 7
+ Variable.VariableCount 1, Term.Literal 5
+ ]
+
+ match rest |> Stream.peel with
+ | None -> failwith "oh no"
+ | Some (s, rest) ->
+
+ s
+ |> Map.toList
+ |> shouldEqual
+ [
+ Variable.VariableCount 0, Term.Literal 7
+ Variable.VariableCount 1, Term.Literal 6
+ ]
+
+ match rest |> Stream.peel with
+ | None -> ()
+ | Some s -> failwith $"{s}"
+
+ []
+ let ``Another example`` () =
+ let aAndB =
+ (Goal.callFresh (fun x -> Goal.equiv (Term.Variable x) (Term.Literal 5)))
+
+ let u = Goal.evaluate aAndB State.empty
+ match u |> Stream.peel with
+ | None -> failwith "oh no"
+ | Some (s, rest) ->
+
+ s
+ |> Map.toList
+ |> shouldEqual [Variable.VariableCount 0, Term.Literal 5]
+
+ match Stream.peel rest with
+ | None -> ()
+ | Some s -> failwithf $"{s}"
+
+ []
+ let ``Recursive example`` () =
+ let rec fives (x : Variable) =
+ (Goal.disj (Goal.equiv (Term.Variable x) (Term.Literal 5)) (Goal.delay (fun () -> fives x)))
+
+ let u = Goal.evaluate (Goal.callFresh fives) State.empty
+ match u |> Stream.peel with
+ | None -> failwith "oh no"
+ | Some (s, rest) ->
+
+ s
+ |> Map.toList
+ |> shouldEqual [Variable.VariableCount 0, Term.Literal 5]
+
+ match Stream.peel rest with
+ | None -> failwith "oh no"
+ | Some (s, rest) ->
+
+ s
+ |> Map.toList
+ |> shouldEqual [Variable.VariableCount 0, Term.Literal 5]
+
+ match Stream.peel rest with
+ | None -> failwith "oh no"
+ | Some (s, _rest) ->
+
+ s
+ |> Map.toList
+ |> shouldEqual [Variable.VariableCount 0, Term.Literal 5]
+
+ []
+ let ``Another recursive example`` () =
+ let rec fives (x : Variable) =
+ (Goal.disj (Goal.equiv (Term.Variable x) (Term.Literal 5)) (Goal.delay (fun () -> fives x)))
+ let rec sixes (x : Variable) =
+ (Goal.disj (Goal.equiv (Term.Variable x) (Term.Literal 6)) (Goal.delay (fun () -> sixes x)))
+ let fivesAndSixes =
+ Goal.callFresh (fun x -> Goal.disj (fives x) (sixes x))
+
+ let u = Goal.evaluate fivesAndSixes State.empty
+ match u |> Stream.peel with
+ | None -> failwith "oh no"
+ | Some (s, rest) ->
+
+ s
+ |> Map.toList
+ |> shouldEqual [Variable.VariableCount 0, Term.Literal 5]
+
+ match Stream.peel rest with
+ | None -> failwith "oh no"
+ | Some (s, rest) ->
+
+ s
+ |> Map.toList
+ |> shouldEqual [Variable.VariableCount 0, Term.Literal 6]
+
+ match Stream.peel rest with
+ | None -> failwith "oh no"
+ | Some (s, rest) ->
+
+ s
+ |> Map.toList
+ |> shouldEqual [Variable.VariableCount 0, Term.Literal 5]
+
+ match Stream.peel rest with
+ | None -> failwith "oh no"
+ | Some (s, _rest) ->
+
+ s
+ |> Map.toList
+ |> shouldEqual [Variable.VariableCount 0, Term.Literal 6]
diff --git a/FicroKanSharp.Test/UnitTest1.fs b/FicroKanSharp.Test/UnitTest1.fs
deleted file mode 100644
index 4459e04..0000000
--- a/FicroKanSharp.Test/UnitTest1.fs
+++ /dev/null
@@ -1,10 +0,0 @@
-namespace FicroKanSharp.Test
-
-open FicroKanSharp
-open Xunit
-
-module TestThing =
-
- []
- let ``Foo`` () : unit =
- failwith "TODO!"
\ No newline at end of file
diff --git a/FicroKanSharp/AssemblyInfo.fs b/FicroKanSharp/AssemblyInfo.fs
new file mode 100644
index 0000000..8913209
--- /dev/null
+++ b/FicroKanSharp/AssemblyInfo.fs
@@ -0,0 +1,6 @@
+module AssemblyInfo
+
+open System.Runtime.CompilerServices
+
+[]
+do()
diff --git a/FicroKanSharp/Domain.fs b/FicroKanSharp/Domain.fs
index f5ba44f..715dbec 100644
--- a/FicroKanSharp/Domain.fs
+++ b/FicroKanSharp/Domain.fs
@@ -1,6 +1,6 @@
namespace FicroKanSharp
-type Variable = private | VariableCount of int
+type Variable = internal | VariableCount of int
[]
module private Variable =
@@ -16,9 +16,10 @@ type Goal =
| Disj of Goal * Goal
| Conj of Goal * Goal
| Fresh of (Variable -> Goal)
+ | Delay of (unit -> Goal)
type State =
- private
+ internal
{
Substitution : Map
VariableCounter : Variable
@@ -56,11 +57,19 @@ module Stream =
| Stream.Nonempty (fst, rest) ->
mplus (g fst) (bind rest g)
+ let rec peel (s : Stream) : (Map * Stream) option =
+ match s with
+ | Stream.Empty -> None
+ | Stream.Nonempty (fst, rest) -> Some (fst.Substitution, rest)
+ | Stream.Procedure p -> peel (p ())
+
[]
module Goal =
let callFresh (f : Variable -> Goal) =
Goal.Fresh f
+ let delay g = Goal.Delay g
+
let disj (goal1 : Goal) (goal2 : Goal) : Goal =
Goal.Disj (goal1, goal2)
@@ -117,4 +126,6 @@ module Goal =
| Goal.Disj (goal1, goal2) ->
Stream.mplus (evaluate goal1 state) (evaluate goal2 state)
| Goal.Conj (goal1, goal2) ->
- Stream.bind (evaluate goal1 state) (evaluate goal2)
\ No newline at end of file
+ Stream.bind (evaluate goal1 state) (evaluate goal2)
+ | Goal.Delay g ->
+ Stream.Procedure (fun () -> evaluate (g ()) state)
\ No newline at end of file
diff --git a/FicroKanSharp/FicroKanSharp.fsproj b/FicroKanSharp/FicroKanSharp.fsproj
index 39071d4..25ed7a6 100644
--- a/FicroKanSharp/FicroKanSharp.fsproj
+++ b/FicroKanSharp/FicroKanSharp.fsproj
@@ -7,6 +7,7 @@
+