From 910a75d18e405794f40578fede1d667653cc0075 Mon Sep 17 00:00:00 2001 From: Smaug123 Date: Fri, 24 Dec 2021 18:44:45 +0000 Subject: [PATCH] Initial commit --- .gitignore | 6 + FicroKanSharp.Test/FicroKanSharp.Test.fsproj | 21 ++++ FicroKanSharp.Test/UnitTest1.fs | 10 ++ FicroKanSharp.sln | 22 ++++ FicroKanSharp/Domain.fs | 120 +++++++++++++++++++ FicroKanSharp/FicroKanSharp.fsproj | 12 ++ 6 files changed, 191 insertions(+) create mode 100644 .gitignore create mode 100644 FicroKanSharp.Test/FicroKanSharp.Test.fsproj create mode 100644 FicroKanSharp.Test/UnitTest1.fs create mode 100644 FicroKanSharp.sln create mode 100644 FicroKanSharp/Domain.fs create mode 100644 FicroKanSharp/FicroKanSharp.fsproj diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..39c9242 --- /dev/null +++ b/.gitignore @@ -0,0 +1,6 @@ +bin/ +obj/ +/packages/ +riderModule.iml +/_ReSharper.Caches/ +.idea/ diff --git a/FicroKanSharp.Test/FicroKanSharp.Test.fsproj b/FicroKanSharp.Test/FicroKanSharp.Test.fsproj new file mode 100644 index 0000000..1c39d3c --- /dev/null +++ b/FicroKanSharp.Test/FicroKanSharp.Test.fsproj @@ -0,0 +1,21 @@ + + + + net6.0 + + + + + + + + + + + + + + + + + diff --git a/FicroKanSharp.Test/UnitTest1.fs b/FicroKanSharp.Test/UnitTest1.fs new file mode 100644 index 0000000..4459e04 --- /dev/null +++ b/FicroKanSharp.Test/UnitTest1.fs @@ -0,0 +1,10 @@ +namespace FicroKanSharp.Test + +open FicroKanSharp +open Xunit + +module TestThing = + + [] + let ``Foo`` () : unit = + failwith "TODO!" \ No newline at end of file diff --git a/FicroKanSharp.sln b/FicroKanSharp.sln new file mode 100644 index 0000000..e03d2de --- /dev/null +++ b/FicroKanSharp.sln @@ -0,0 +1,22 @@ + +Microsoft Visual Studio Solution File, Format Version 12.00 +Project("{F2A71F9B-5D33-465A-A702-920D77279786}") = "FicroKanSharp", "FicroKanSharp\FicroKanSharp.fsproj", "{5CC2EFDA-B0BA-48EA-B7D4-102FFF239ED9}" +EndProject +Project("{F2A71F9B-5D33-465A-A702-920D77279786}") = "FicroKanSharp.Test", "FicroKanSharp.Test\FicroKanSharp.Test.fsproj", "{8F5B2B07-763B-4501-9E0E-3DB5B319DD7B}" +EndProject +Global + GlobalSection(SolutionConfigurationPlatforms) = preSolution + Debug|Any CPU = Debug|Any CPU + Release|Any CPU = Release|Any CPU + EndGlobalSection + GlobalSection(ProjectConfigurationPlatforms) = postSolution + {5CC2EFDA-B0BA-48EA-B7D4-102FFF239ED9}.Debug|Any CPU.ActiveCfg = Debug|Any CPU + {5CC2EFDA-B0BA-48EA-B7D4-102FFF239ED9}.Debug|Any CPU.Build.0 = Debug|Any CPU + {5CC2EFDA-B0BA-48EA-B7D4-102FFF239ED9}.Release|Any CPU.ActiveCfg = Release|Any CPU + {5CC2EFDA-B0BA-48EA-B7D4-102FFF239ED9}.Release|Any CPU.Build.0 = Release|Any CPU + {8F5B2B07-763B-4501-9E0E-3DB5B319DD7B}.Debug|Any CPU.ActiveCfg = Debug|Any CPU + {8F5B2B07-763B-4501-9E0E-3DB5B319DD7B}.Debug|Any CPU.Build.0 = Debug|Any CPU + {8F5B2B07-763B-4501-9E0E-3DB5B319DD7B}.Release|Any CPU.ActiveCfg = Release|Any CPU + {8F5B2B07-763B-4501-9E0E-3DB5B319DD7B}.Release|Any CPU.Build.0 = Release|Any CPU + EndGlobalSection +EndGlobal diff --git a/FicroKanSharp/Domain.fs b/FicroKanSharp/Domain.fs new file mode 100644 index 0000000..f5ba44f --- /dev/null +++ b/FicroKanSharp/Domain.fs @@ -0,0 +1,120 @@ +namespace FicroKanSharp + +type Variable = private | VariableCount of int + +[] +module private Variable = + let incr (VariableCount v) = VariableCount (v + 1) + +type Term = + | Literal of int + | Variable of Variable + +type Goal = + private + | Equiv of Term * Term + | Disj of Goal * Goal + | Conj of Goal * Goal + | Fresh of (Variable -> Goal) + +type State = + private + { + Substitution : Map + VariableCounter : Variable + } + +type Stream = + private + | Empty + | Procedure of (unit -> Stream) + | Nonempty of State * Stream + +[] +module State = + let empty = + { + VariableCounter = VariableCount 0 + Substitution = Map.empty + } + +[] +module Stream = + let mzero : Stream = + Stream.Empty + + let rec mplus (s1 : Stream) (s2 : Stream) : Stream = + match s1 with + | Stream.Empty -> s2 + | Stream.Procedure s -> Stream.Procedure (fun () -> mplus s2 (s ())) + | Stream.Nonempty (fst, rest) -> Stream.Nonempty (fst, mplus rest s2) + + let rec bind (s : Stream) (g : State -> Stream) = + match s with + | Stream.Empty -> mzero + | Stream.Procedure s -> Stream.Procedure (fun () -> bind (s ()) g) + | Stream.Nonempty (fst, rest) -> + mplus (g fst) (bind rest g) + +[] +module Goal = + let callFresh (f : Variable -> Goal) = + Goal.Fresh f + + let disj (goal1 : Goal) (goal2 : Goal) : Goal = + Goal.Disj (goal1, goal2) + + let conj (goal1 : Goal) (goal2 : Goal) : Goal = + Goal.Conj (goal1, goal2) + + let equiv (term1 : Term) (term2 : Term) : Goal = + Goal.Equiv (term1, term2) + + let walk (u : Term) (s : State) : Term = + match u with + | Term.Variable u -> + match Map.tryFind u s.Substitution with + | None -> Term.Variable u + | Some subst -> subst + | u -> u + + let extend (v : Variable) (t : Term) (s : State) = + { s with + Substitution = Map.add v t s.Substitution + } + + let rec unify u v (s : State) : State option = + let u = walk u s + let v = walk v s + + match u, v with + | Term.Variable u, Term.Variable v when u = v -> + s + |> Some + | Term.Variable u, v -> + extend u v s + |> Some + | u, Term.Variable v -> + extend v u s + |> Some + | Term.Literal u, Term.Literal v -> + if u = v then + Some s + else None + + let rec evaluate (goal : Goal) (state : State) : Stream = + match goal with + | Goal.Equiv (u, v) -> + // (let ((s (unify u v (car s/c)))) +//(if s (unit `(, s . , (cdr s/c))) mzero)))) + match unify u v state with + | None -> Stream.mzero + | Some unification -> + Stream.Nonempty (unification, Stream.mzero) + | Goal.Fresh goal -> + let newVar = state.VariableCounter + evaluate (goal newVar) { state with VariableCounter = Variable.incr state.VariableCounter } + | 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 diff --git a/FicroKanSharp/FicroKanSharp.fsproj b/FicroKanSharp/FicroKanSharp.fsproj new file mode 100644 index 0000000..39071d4 --- /dev/null +++ b/FicroKanSharp/FicroKanSharp.fsproj @@ -0,0 +1,12 @@ + + + + net6.0 + true + + + + + + +