From b407409584220d8d56bffbc0f3c77ea17be53c7f Mon Sep 17 00:00:00 2001 From: Patrick Stevens Date: Sun, 26 Dec 2021 16:24:05 +0000 Subject: [PATCH] Split into an untyped core and a typed layer (#1) --- FicroKanSharp.Test/Arithmetic.fs | 206 ++++++++++++++++--- FicroKanSharp.Test/FicroKanSharp.Test.fsproj | 3 + FicroKanSharp.Test/Geometry.fs | 116 +++++++++++ FicroKanSharp.Test/NotWorking.fs | 124 +++++++++++ FicroKanSharp.Test/Recursive.fs | 117 +++++++++++ FicroKanSharp.Test/TestExamples.fs | 57 +++-- FicroKanSharp/Domain.fs | 105 ++-------- FicroKanSharp/FicroKanSharp.fsproj | 6 + FicroKanSharp/Goal.fs | 133 +++++------- FicroKanSharp/Reflection.fs | 22 ++ FicroKanSharp/Stream.fs | 23 ++- FicroKanSharp/Term.fs | 6 + FicroKanSharp/Typed.fs | 69 +++++++ 13 files changed, 745 insertions(+), 242 deletions(-) create mode 100644 FicroKanSharp.Test/Geometry.fs create mode 100644 FicroKanSharp.Test/NotWorking.fs create mode 100644 FicroKanSharp.Test/Recursive.fs create mode 100644 FicroKanSharp/Reflection.fs create mode 100644 FicroKanSharp/Term.fs create mode 100644 FicroKanSharp/Typed.fs diff --git a/FicroKanSharp.Test/Arithmetic.fs b/FicroKanSharp.Test/Arithmetic.fs index 8c42c98..b33471b 100644 --- a/FicroKanSharp.Test/Arithmetic.fs +++ b/FicroKanSharp.Test/Arithmetic.fs @@ -6,23 +6,20 @@ open Xunit module Arithmetic = - type Nat = Nat - [] - let ``Arithmetic example`` () = - let zero : Term = Term.Symbol ("zero", []) + let ``Arithmetic example, untyped`` () = + let zero : Term = Term.Symbol ("zero", []) - let succ (x : Term) : Term = - Term.Symbol ("succ", [ TypedTerm.make x ]) + let succ (x : Term) : Term = Term.Symbol ("succ", [ x ]) - let rec ofInt (n : int) : Term = + let rec ofInt (n : int) : Term = if n = 0 then zero else succ (ofInt (n - 1)) // "pluso x y z" is "x + y == z". - let rec pluso (x : Term) (y : Term) (z : Term) : Goal = + let rec pluso (x : Term) (y : Term) (z : Term) : Goal = let succCase = Goal.callFresh (fun n -> let n = Term.Variable n @@ -41,49 +38,206 @@ module Arithmetic = Goal.disj zeroCase succCase - Goal.evaluate (Goal.callFresh (fun z -> Goal.equiv (Term.Variable z) (Term.Variable z))) State.empty + Goal.evaluate (Goal.callFresh (fun z -> Goal.equiv (Term.Variable z) (Term.Variable z))) |> Stream.toList |> shouldEqual [ Map.empty ] - // Evaluate 1 + 1 - Goal.evaluate (Goal.callFresh (fun z -> pluso (ofInt 1) (ofInt 1) (Term.Variable z))) State.empty + Goal.evaluate (pluso (ofInt 2) (ofInt 2) (ofInt 4)) |> Stream.toList |> List.exactlyOne |> shouldEqual ( Map.ofList [ - VariableCount 0, TypedTerm.make (succ (Term.Variable (VariableCount 2))) - VariableCount 1, TypedTerm.make (ofInt 0) - VariableCount 2, TypedTerm.make (ofInt 1) + VariableCount 0, ofInt 1 + VariableCount 1, ofInt 3 + VariableCount 3, zero + VariableCount 4, ofInt 2 + ] + ) + + // Evaluate 1 + 1 + Goal.evaluate (Goal.callFresh (fun z -> pluso (ofInt 1) (ofInt 1) (Term.Variable z))) + |> Stream.toList + |> List.exactlyOne + |> shouldEqual ( + Map.ofList + [ + VariableCount 0, succ (Term.Variable (VariableCount 2)) + VariableCount 1, ofInt 0 + VariableCount 2, ofInt 1 ] ) // Evaluate 2 + 2 - Goal.evaluate (Goal.callFresh (fun z -> pluso (ofInt 2) (ofInt 2) (Term.Variable z))) State.empty + Goal.evaluate (Goal.callFresh (fun z -> pluso (ofInt 2) (ofInt 2) (Term.Variable z))) |> Stream.toList |> List.exactlyOne |> shouldEqual ( Map.ofList [ - VariableCount 0, TypedTerm.make (succ (Term.Variable (VariableCount 2))) - VariableCount 1, TypedTerm.make (ofInt 1) - VariableCount 2, TypedTerm.make (succ (Term.Variable (VariableCount 4))) - VariableCount 3, TypedTerm.make zero - VariableCount 4, TypedTerm.make (ofInt 2) + VariableCount 0, succ (Term.Variable (VariableCount 2)) + VariableCount 1, ofInt 1 + VariableCount 2, succ (Term.Variable (VariableCount 5)) + VariableCount 4, zero + VariableCount 5, ofInt 2 ] ) // Find n such that n + n = 4 - Goal.evaluate (Goal.callFresh (fun z -> pluso (Term.Variable z) (Term.Variable z) (ofInt 4))) State.empty + Goal.evaluate (Goal.callFresh (fun z -> pluso (Term.Variable z) (Term.Variable z) (ofInt 4))) |> Stream.toList |> List.exactlyOne |> shouldEqual ( Map.ofList [ - VariableCount 0, TypedTerm.make (succ (Term.Variable (VariableCount 1))) - VariableCount 1, TypedTerm.make (succ (Term.Variable (VariableCount 3))) - VariableCount 2, TypedTerm.make (ofInt 3) - VariableCount 3, TypedTerm.make zero - VariableCount 4, TypedTerm.make (ofInt 2) + VariableCount 0, succ (Term.Variable (VariableCount 1)) + VariableCount 1, succ (Term.Variable (VariableCount 4)) + VariableCount 2, ofInt 3 + VariableCount 4, zero + VariableCount 5, ofInt 2 + ] + ) + + type Nat = + | Zero + | Succ of TypedTerm + + [] + let ``Arithmetic example, typed`` () = + let rec ofInt (n : int) : TypedTerm = + if n = 0 then + Nat.Zero |> TypedTerm.literal + else + Nat.Succ (ofInt (n - 1)) |> TypedTerm.literal + + let succ (n : TypedTerm) = Nat.Succ n |> TypedTerm.literal + let zero = Nat.Zero |> TypedTerm.literal + + let rec numeralo (x : TypedTerm) : Goal = + Goal.disj + (TypedTerm.Goal.equiv x (TypedTerm.literal Nat.Zero)) + (TypedTerm.Goal.callFresh (fun y -> + Goal.conj (Goal.delay (fun () -> numeralo y)) (TypedTerm.Goal.equiv x (succ y)) + )) + + // By the power of microKanren, let some numerals be manifested! + + Goal.evaluate (TypedTerm.Goal.callFresh numeralo) + |> Stream.take 4 + |> shouldEqual + [ + Map.ofList + [ + VariableCount 0, TypedTerm.literal Nat.Zero |> TypedTerm.compile + ] + Map.ofList + [ + VariableCount 0, + TypedTerm.literal (Nat.Succ (TypedTerm.variable (VariableCount 1))) + |> TypedTerm.compile + VariableCount 1, TypedTerm.literal Nat.Zero |> TypedTerm.compile + ] + Map.ofList + [ + VariableCount 0, + TypedTerm.literal (Nat.Succ (TypedTerm.variable (VariableCount 1))) + |> TypedTerm.compile + VariableCount 1, + TypedTerm.literal (Nat.Succ (TypedTerm.variable (VariableCount 3))) + |> TypedTerm.compile + VariableCount 3, TypedTerm.literal Nat.Zero |> TypedTerm.compile + ] + Map.ofList + [ + VariableCount 0, + TypedTerm.literal (Nat.Succ (TypedTerm.variable (VariableCount 1))) + |> TypedTerm.compile + VariableCount 1, + TypedTerm.literal (Nat.Succ (TypedTerm.variable (VariableCount 3))) + |> TypedTerm.compile + VariableCount 3, + TypedTerm.literal (Nat.Succ (TypedTerm.variable (VariableCount 5))) + |> TypedTerm.compile + VariableCount 5, TypedTerm.literal Nat.Zero |> TypedTerm.compile + ] + ] + + // "pluso x y z" is "x + y == z". + let rec pluso (x : TypedTerm) (y : TypedTerm) (z : TypedTerm) : Goal = + let z = z |> TypedTerm.compile + + let succCase = + Goal.callFresh (fun n -> + let n = TypedTerm.variable n + + Goal.callFresh (fun m -> + let m = TypedTerm.variable m + + Goal.conj + (Goal.equiv (TypedTerm.compile x) (TypedTerm.compile (succ n))) + (Goal.conj (Goal.equiv z (succ m |> TypedTerm.compile)) (Goal.delay (fun () -> pluso n y m))) + ) + ) + + let zeroCase = + Goal.conj + (Goal.equiv (TypedTerm.compile x) (TypedTerm.compile zero)) + (Goal.equiv (TypedTerm.compile y) z) + + Goal.disj zeroCase succCase + + Goal.evaluate (pluso (ofInt 2) (ofInt 2) (ofInt 4)) + |> Stream.toList + |> List.exactlyOne + |> shouldEqual ( + Map.ofList + [ + VariableCount 0, (ofInt 1 |> TypedTerm.compile) + VariableCount 1, (ofInt 3 |> TypedTerm.compile) + VariableCount 3, TypedTerm.compile zero + VariableCount 4, (ofInt 2 |> TypedTerm.compile) + ] + ) + + // Evaluate 1 + 1 + Goal.evaluate (Goal.callFresh (fun z -> pluso (ofInt 1) (ofInt 1) (TypedTerm.variable z))) + |> Stream.toList + |> List.exactlyOne + |> shouldEqual ( + Map.ofList + [ + VariableCount 0, TypedTerm.compile (succ (TypedTerm.variable (VariableCount 2))) + VariableCount 1, TypedTerm.compile (ofInt 0) + VariableCount 2, TypedTerm.compile (ofInt 1) + ] + ) + + // Evaluate 2 + 2 + Goal.evaluate (Goal.callFresh (fun z -> pluso (ofInt 2) (ofInt 2) (TypedTerm.variable z))) + |> Stream.toList + |> List.exactlyOne + |> shouldEqual ( + Map.ofList + [ + VariableCount 0, TypedTerm.compile (succ (TypedTerm.variable (VariableCount 2))) + VariableCount 1, TypedTerm.compile (ofInt 1) + VariableCount 2, TypedTerm.compile (succ (TypedTerm.variable (VariableCount 5))) + VariableCount 4, TypedTerm.compile zero + VariableCount 5, TypedTerm.compile (ofInt 2) + ] + ) + + // Find n such that n + n = 4 + Goal.evaluate (Goal.callFresh (fun z -> pluso (TypedTerm.variable z) (TypedTerm.variable z) (ofInt 4))) + |> Stream.toList + |> List.exactlyOne + |> shouldEqual ( + Map.ofList + [ + VariableCount 0, TypedTerm.compile (succ (TypedTerm.variable (VariableCount 1))) + VariableCount 1, TypedTerm.compile (succ (TypedTerm.variable (VariableCount 4))) + VariableCount 2, TypedTerm.compile (ofInt 3) + VariableCount 4, TypedTerm.compile zero + VariableCount 5, TypedTerm.compile (ofInt 2) ] ) diff --git a/FicroKanSharp.Test/FicroKanSharp.Test.fsproj b/FicroKanSharp.Test/FicroKanSharp.Test.fsproj index aeeefe5..f621f68 100644 --- a/FicroKanSharp.Test/FicroKanSharp.Test.fsproj +++ b/FicroKanSharp.Test/FicroKanSharp.Test.fsproj @@ -7,6 +7,9 @@ + + + diff --git a/FicroKanSharp.Test/Geometry.fs b/FicroKanSharp.Test/Geometry.fs new file mode 100644 index 0000000..ee00252 --- /dev/null +++ b/FicroKanSharp.Test/Geometry.fs @@ -0,0 +1,116 @@ +namespace FicroKanSharp.Test + +// Taken from http://www.let.rug.nl/bos/lpn//lpnpage.php?pagetype=html&pageid=lpn-htmlse5 + +open FsUnitTyped +open FicroKanSharp +open Xunit + +module Geometry = + + type Point<'a> = Point of TypedTerm<'a> * TypedTerm<'a> + + type Line<'a> = Line of TypedTerm> * TypedTerm> + + let verticalo<'a when 'a : equality> (line : TypedTerm>) : Goal = + fun x -> + fun y -> + fun z -> + Line (TypedTerm>.Literal (Point (x, y)), TypedTerm.Literal (Point (x, z))) + |> TypedTerm.Literal + |> TypedTerm.Goal.equiv line + |> TypedTerm.Goal.callFresh + |> TypedTerm.Goal.callFresh + |> TypedTerm.Goal.callFresh + + let horizontalo<'a when 'a : equality> (line : TypedTerm>) : Goal = + fun x -> + fun y -> + fun z -> + Line (TypedTerm>.Literal (Point (x, y)), TypedTerm.Literal (Point (z, y))) + |> TypedTerm.Literal + |> TypedTerm.Goal.equiv line + |> TypedTerm.Goal.callFresh + |> TypedTerm.Goal.callFresh + |> TypedTerm.Goal.callFresh + + [] + let ``Geometry example from Learn Prolog Now`` () = + Line ( + TypedTerm.Literal (Point (TypedTerm.Literal 1, TypedTerm.Literal 1)), + TypedTerm.Literal (Point (TypedTerm.Literal 1, TypedTerm.Literal 3)) + ) + |> TypedTerm.Literal + |> verticalo + |> Goal.evaluate + |> Stream.toList + |> List.exactlyOne + |> shouldEqual ( + Map.ofList + [ + VariableCount 0, TypedTerm.compile (TypedTerm.Literal 1) + VariableCount 1, TypedTerm.compile (TypedTerm.Literal 1) + VariableCount 2, TypedTerm.compile (TypedTerm.Literal 3) + ] + ) + + (Line ( + TypedTerm.Literal (Point (TypedTerm.Literal 1, TypedTerm.Literal 1)), + TypedTerm.Literal (Point (TypedTerm.Literal 3, TypedTerm.Literal 2)) + )) + |> TypedTerm.Literal + |> verticalo + |> Goal.evaluate + |> Stream.toList + |> shouldEqual [] + + Goal.callFresh (fun y -> + Line ( + TypedTerm.Literal (Point (TypedTerm.Literal 1, TypedTerm.Literal 1)), + TypedTerm.Literal (Point (TypedTerm.Literal 2, TypedTerm.variable y)) + ) + |> TypedTerm.Literal + |> horizontalo + ) + |> Goal.evaluate + |> Stream.toList + |> List.exactlyOne + |> shouldEqual ( + Map.ofList + [ + // There is y such that (1,1) = (2, y), and it is 1. + VariableCount 0, TypedTerm.compile (TypedTerm.Literal 1) + // There is x,y,z such that (x,y) = (z,y) where (x,y) = (1,1) and (z,y) = (2, y) + // and they are 1, 1, and 2. + VariableCount 1, TypedTerm.compile (TypedTerm.Literal 1) + VariableCount 2, TypedTerm.compile (TypedTerm.Literal 1) + VariableCount 3, TypedTerm.compile (TypedTerm.Literal 2) + ] + ) + + Goal.callFresh (fun y -> + Line (TypedTerm.Literal (Point (TypedTerm.Literal 2, TypedTerm.Literal 3)), TypedTerm.variable y) + |> TypedTerm.Literal + |> horizontalo + ) + |> Goal.evaluate + |> Stream.toList + |> List.exactlyOne + |> shouldEqual ( + Map.ofList + [ + // There is a point p such that (2,3) -> p is horizontal. + // It is (x3, x2). + VariableCount 0, + TypedTerm.compile ( + TypedTerm.Literal ( + Point (TypedTerm.variable (VariableCount 3), TypedTerm.variable (VariableCount 2)) + ) + ) + // This is the x-coordinate, which doesn't reify in the final answer. + VariableCount 1, TypedTerm.compile (TypedTerm.Literal 2) + // x2 is 3. + VariableCount 2, TypedTerm.compile (TypedTerm.Literal 3) + // Notice that x3 is not constrained. + ] + ) diff --git a/FicroKanSharp.Test/NotWorking.fs b/FicroKanSharp.Test/NotWorking.fs new file mode 100644 index 0000000..f13d74c --- /dev/null +++ b/FicroKanSharp.Test/NotWorking.fs @@ -0,0 +1,124 @@ +namespace FicroKanSharp.Test + +open FicroKanSharp +open Xunit +open FsUnitTyped + +module NotWorking = + + type Int = + | Pure of int + | Succ of TypedTerm + + [] + let ``Arithmetic example using literals`` () = + let zero = TypedTerm.literal (Int.Pure 0) + + let succ (x : TypedTerm) : TypedTerm = + match x with + // Little efficiency saving + | TypedTerm.Literal (Int.Pure x) -> TypedTerm.Literal (x + 1 |> Int.Pure) + | _ -> TypedTerm.Literal (Int.Succ x) + + let rec ofInt (n : int) : TypedTerm = Int.Pure n |> TypedTerm.Literal + + let rec equal (x : Int) (y : Int) : Goal = + match x, y with + | Int.Pure x, Int.Pure y -> + if x = y then + Goal.always + else + Goal.never + | Int.Succ x, Int.Succ y -> equal x y + | TypedTerm.Literal (Int.Pure x), TypedTerm.Literal (Int.Succ y) -> + Goal.delay (fun () -> equal (TypedTerm.Literal (Int.Pure (x - 1))) y) + | TypedTerm.Literal (Int.Succ x), TypedTerm.Literal (Int.Pure y) -> + Goal.delay (fun () -> equal x (TypedTerm.Literal (Int.Pure (y - 1)))) + + // "pluso x y z" is "x + y == z". + let rec pluso (x : TypedTerm) (y : TypedTerm) (z : TypedTerm) : Goal = + let succCase = + TypedTerm.Goal.callFresh (fun n -> + TypedTerm.Goal.callFresh (fun m -> + Goal.conj (equal x (succ n)) (Goal.conj (equal z (succ m)) (Goal.delay (fun () -> pluso n y m))) + ) + ) + + let zeroCase = Goal.conj (equal x zero) (equal y z) + + Goal.disj zeroCase succCase + + Goal.callFresh (fun n -> + let n = TypedTerm.variable n // should be 1 + + Goal.callFresh (fun m -> + let m = TypedTerm.variable m // should be 3 + + let delayed = + Goal.callFresh (fun a -> + let a = TypedTerm.variable a // should be 0 + + Goal.callFresh (fun b -> + let b = TypedTerm.variable b // should be 2 + + Goal.conj + (equal n (succ a)) + (Goal.conj (equal m (succ b)) (Goal.conj (equal a zero) (equal (ofInt 2) b))) + ) + ) + + Goal.conj (equal (ofInt 2) (succ n)) (Goal.conj (equal (ofInt 4) (succ m)) delayed) + ) + ) + |> Goal.evaluate + //Goal.evaluate (pluso (ofInt 2) (ofInt 2) (ofInt 4)) + |> Stream.toList + |> List.exactlyOne + |> shouldEqual Map.empty + + Goal.evaluate (pluso (ofInt 2) (ofInt 2) (ofInt 5)) + |> Stream.toList + |> printfn "%O" + + // Evaluate 1 + 1 + Goal.evaluate (Goal.callFresh (fun z -> pluso (ofInt 1) (ofInt 1) (TypedTerm.variable z))) + |> Stream.toList + |> List.exactlyOne + |> shouldEqual ( + Map.ofList + [ + VariableCount 0, TypedTerm.compile (succ (TypedTerm.variable (VariableCount 2))) + VariableCount 1, TypedTerm.compile (ofInt 0) + VariableCount 2, TypedTerm.compile (ofInt 1) + ] + ) + + // Evaluate 2 + 2 + Goal.evaluate (Goal.callFresh (fun z -> pluso (ofInt 2) (ofInt 2) (TypedTerm.variable z))) + |> Stream.toList + |> List.exactlyOne + |> shouldEqual ( + Map.ofList + [ + VariableCount 0, TypedTerm.compile (succ (TypedTerm.variable (VariableCount 2))) + VariableCount 1, TypedTerm.compile (ofInt 1) + VariableCount 2, TypedTerm.compile (succ (TypedTerm.variable (VariableCount 4))) + VariableCount 3, TypedTerm.compile zero + VariableCount 4, TypedTerm.compile (ofInt 2) + ] + ) + + // Find n such that n + n = 4 + Goal.evaluate (Goal.callFresh (fun z -> pluso (TypedTerm.variable z) (TypedTerm.variable z) (ofInt 4))) + |> Stream.toList + |> List.exactlyOne + |> shouldEqual ( + Map.ofList + [ + VariableCount 0, TypedTerm.compile (succ (TypedTerm.variable (VariableCount 1))) + VariableCount 1, TypedTerm.compile (succ (TypedTerm.variable (VariableCount 3))) + VariableCount 2, TypedTerm.compile (ofInt 3) + VariableCount 3, TypedTerm.compile zero + VariableCount 4, TypedTerm.compile (ofInt 2) + ] + ) diff --git a/FicroKanSharp.Test/Recursive.fs b/FicroKanSharp.Test/Recursive.fs new file mode 100644 index 0000000..ea9d605 --- /dev/null +++ b/FicroKanSharp.Test/Recursive.fs @@ -0,0 +1,117 @@ +namespace FicroKanSharp.Test + +open Xunit +open FsUnitTyped +open FicroKanSharp + +module Recursive = + + type Entity = + | Mosquito + | Frog + | Stork + | Blood of TypedTerm + | Name of TypedTerm + + [] + let ``Recursive definitions, example 1`` () : unit = + let justAte (t1 : TypedTerm) (t2 : TypedTerm) : Goal = + Goal.disj + (Goal.conj + (TypedTerm.Goal.equiv t1 (TypedTerm.literal Entity.Mosquito)) + (TypedTerm.Goal.equiv + t2 + (TypedTerm.Literal (Entity.Blood (TypedTerm.literal (Entity.Name (TypedTerm.literal "john"))))))) + (Goal.disj + (Goal.conj + (TypedTerm.Goal.equiv t1 (TypedTerm.literal Entity.Frog)) + (TypedTerm.Goal.equiv t2 (TypedTerm.literal Entity.Mosquito))) + (Goal.conj + (TypedTerm.Goal.equiv t1 (TypedTerm.literal Entity.Stork)) + (TypedTerm.Goal.equiv t2 (TypedTerm.literal Entity.Frog)))) + + let rec isDigesting (t1 : TypedTerm) (t2 : TypedTerm) : Goal = + Goal.disj + (justAte t1 t2) + (TypedTerm.Goal.callFresh (fun z -> + Goal.delay (fun () -> Goal.conj (isDigesting t1 z) (isDigesting z t2)) + )) + + let stream = + isDigesting (TypedTerm.literal Entity.Stork) (TypedTerm.literal Entity.Mosquito) + |> Goal.evaluate + + let fst, _ = stream |> Stream.peel |> Option.get + + fst + |> shouldEqual ( + Map.ofList + [ + // The stork is digesting the mosquito, via the frog which the stork just ate. + VariableCount 0, TypedTerm.Literal Entity.Frog |> TypedTerm.compile + ] + ) + + // There is no second element of the stream, but FicroKanSharp will search + // forever without realising this. + // It will forever try to find z such that `isDigesting Stork z` and `isDigesting z Mosquito`. + + type Human = Human of string + + [] + let ``Recursive definitions, example 2`` () : unit = + let children = + [ + "anne", "bridget" + "bridget", "caroline" + "caroline", "donna" + "donna", "emily" + ] + |> List.map (fun (parent, child) -> TypedTerm.literal (Human parent), TypedTerm.literal (Human child)) + + let child (t1 : TypedTerm) (t2 : TypedTerm) : Goal = + children + |> List.fold + (fun state (parent, child) -> + Goal.conj (TypedTerm.Goal.equiv parent t1) (TypedTerm.Goal.equiv t2 child) + |> Goal.disj state + ) + Goal.never + + let rec descend (t1 : TypedTerm) (t2 : TypedTerm) : Goal = + Goal.disj + (child t1 t2) + (TypedTerm.Goal.callFresh (fun z -> Goal.conj (child t1 z) (Goal.delay (fun () -> descend z t2)))) + + let emptyStream = + child (TypedTerm.literal (Human "anne")) (TypedTerm.literal (Human "donna")) + |> Goal.evaluate + |> Stream.peel + + match emptyStream with + | None -> () + | Some s -> failwith $"{s}" + + child (TypedTerm.literal (Human "anne")) (TypedTerm.literal (Human "bridget")) + |> Goal.evaluate + |> Stream.peel + |> Option.get + |> fst + |> shouldEqual (Map.ofList []) + + descend (TypedTerm.literal (Human "anne")) (TypedTerm.literal (Human "donna")) + |> Goal.evaluate + |> Stream.peel + |> Option.get + |> fst + |> shouldEqual ( + Map.ofList + [ + VariableCount 0, + TypedTerm.literal (Human "bridget") + |> TypedTerm.compile + VariableCount 2, + TypedTerm.literal (Human "caroline") + |> TypedTerm.compile + ] + ) diff --git a/FicroKanSharp.Test/TestExamples.fs b/FicroKanSharp.Test/TestExamples.fs index d084d9e..65aafc9 100644 --- a/FicroKanSharp.Test/TestExamples.fs +++ b/FicroKanSharp.Test/TestExamples.fs @@ -10,26 +10,25 @@ 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.equiv (Term.Variable x) (Term.Symbol (7, [])))) (Goal.callFresh (fun x -> Goal.disj - (Goal.equiv (Term.Variable x) (Term.Literal 5)) - (Goal.equiv (Term.Variable x) (Term.Literal 6)) + (Goal.equiv (Term.Variable x) (Term.Symbol (5, []))) + (Goal.equiv (Term.Variable x) (Term.Symbol (6, []))) )) - let u = Goal.evaluate aAndB State.empty + let u = Goal.evaluate aAndB match u |> Stream.peel with | None -> failwith "oh no" | Some (s, rest) -> s - |> Map.map (fun _ -> TypedTerm.force) |> Map.toList |> shouldEqual [ - Variable.VariableCount 0, Term.Literal 7 - Variable.VariableCount 1, Term.Literal 5 + Variable.VariableCount 0, Term.Symbol (7, []) + Variable.VariableCount 1, Term.Symbol (5, []) ] match rest |> Stream.peel with @@ -37,12 +36,11 @@ module TestThing = | Some (s, rest) -> s - |> Map.map (fun _ -> TypedTerm.force) |> Map.toList |> shouldEqual [ - Variable.VariableCount 0, Term.Literal 7 - Variable.VariableCount 1, Term.Literal 6 + Variable.VariableCount 0, Term.Symbol (7, []) + Variable.VariableCount 1, Term.Symbol (6, []) ] match rest |> Stream.peel with @@ -52,20 +50,19 @@ module TestThing = [] let ``Another example`` () = let aAndB = - (Goal.callFresh (fun x -> Goal.equiv (Term.Variable x) (Term.Literal 5))) + (Goal.callFresh (fun x -> Goal.equiv (Term.Variable x) (Term.Symbol (5, [])))) - let u = Goal.evaluate aAndB State.empty + let u = Goal.evaluate aAndB match u |> Stream.peel with | None -> failwith "oh no" | Some (s, rest) -> s - |> Map.map (fun _ -> TypedTerm.force) |> Map.toList |> shouldEqual [ - Variable.VariableCount 0, Term.Literal 5 + Variable.VariableCount 0, Term.Symbol (5, []) ] match Stream.peel rest with @@ -75,21 +72,19 @@ module TestThing = [] let ``Recursive example`` () = let rec fives (x : Variable) = - (Goal.disj (Goal.equiv (Term.Variable x) (Term.Literal 5)) (Goal.delay (fun () -> fives x))) + (Goal.disj (Goal.equiv (Term.Variable x) (Term.Symbol (5, []))) (Goal.delay (fun () -> fives x))) - let u = - Goal.evaluate (Goal.callFresh fives) State.empty + let u = Goal.evaluate (Goal.callFresh fives) match u |> Stream.peel with | None -> failwith "oh no" | Some (s, rest) -> s - |> Map.map (fun _ -> TypedTerm.force) |> Map.toList |> shouldEqual [ - Variable.VariableCount 0, Term.Literal 5 + Variable.VariableCount 0, Term.Symbol (5, []) ] match Stream.peel rest with @@ -97,11 +92,10 @@ module TestThing = | Some (s, rest) -> s - |> Map.map (fun _ -> TypedTerm.force) |> Map.toList |> shouldEqual [ - Variable.VariableCount 0, Term.Literal 5 + Variable.VariableCount 0, Term.Symbol (5, []) ] match Stream.peel rest with @@ -109,36 +103,34 @@ module TestThing = | Some (s, _rest) -> s - |> Map.map (fun _ -> TypedTerm.force) |> Map.toList |> shouldEqual [ - Variable.VariableCount 0, Term.Literal 5 + Variable.VariableCount 0, Term.Symbol (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))) + (Goal.disj (Goal.equiv (Term.Variable x) (Term.Symbol (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))) + (Goal.disj (Goal.equiv (Term.Variable x) (Term.Symbol (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 + let u = Goal.evaluate fivesAndSixes match u |> Stream.peel with | None -> failwith "oh no" | Some (s, rest) -> s - |> Map.map (fun _ -> TypedTerm.force) |> Map.toList |> shouldEqual [ - Variable.VariableCount 0, Term.Literal 5 + Variable.VariableCount 0, Term.Symbol (5, []) ] match Stream.peel rest with @@ -146,11 +138,10 @@ module TestThing = | Some (s, rest) -> s - |> Map.map (fun _ -> TypedTerm.force) |> Map.toList |> shouldEqual [ - Variable.VariableCount 0, Term.Literal 6 + Variable.VariableCount 0, Term.Symbol (6, []) ] match Stream.peel rest with @@ -158,11 +149,10 @@ module TestThing = | Some (s, rest) -> s - |> Map.map (fun _ -> TypedTerm.force) |> Map.toList |> shouldEqual [ - Variable.VariableCount 0, Term.Literal 5 + Variable.VariableCount 0, Term.Symbol (5, []) ] match Stream.peel rest with @@ -170,9 +160,8 @@ module TestThing = | Some (s, _rest) -> s - |> Map.map (fun _ -> TypedTerm.force) |> Map.toList |> shouldEqual [ - Variable.VariableCount 0, Term.Literal 6 + Variable.VariableCount 0, Term.Symbol (6, []) ] diff --git a/FicroKanSharp/Domain.fs b/FicroKanSharp/Domain.fs index e4b9f6c..ff64ceb 100644 --- a/FicroKanSharp/Domain.fs +++ b/FicroKanSharp/Domain.fs @@ -1,15 +1,17 @@ namespace FicroKanSharp +open Microsoft.FSharp.Core + type Variable = internal VariableCount of int [] module private Variable = let incr (VariableCount v) = VariableCount (v + 1) -type Term<'a> = - | Literal of 'a +type Term = + internal | Variable of Variable - | Symbol of name : string * args : TypedTerm list + | Symbol of name : obj * args : Term list override this.ToString () = match this with @@ -21,102 +23,19 @@ type Term<'a> = $"{name}[{s}]" | Variable (VariableCount v) -> $"x{v}" - | Literal t -> t.ToString () - -and internal TermEvaluator<'ret> = - abstract Eval<'a when 'a : equality> : 'a Term -> 'ret - -and internal TermCrate = - abstract Apply<'ret> : TermEvaluator<'ret> -> 'ret - -and [] TypedTerm = - internal - | TypedTerm of TermCrate - - override this.Equals (other : obj) : bool = - match this with - | TypedTerm tc -> - - match other with - | :? TypedTerm as other -> - match other with - | TypedTerm other -> tc.Equals other - | _ -> false - - override this.GetHashCode () = - match this with - | TypedTerm tc -> - { new TermEvaluator<_> with - override _.Eval t = t.GetHashCode () - } - |> tc.Apply - - override this.ToString () = - match this with - | TypedTerm tc -> tc.ToString () - -[] -module internal TermCrate = - let make<'a when 'a : equality> (t1 : 'a Term) = - { new obj() with - override this.ToString () = t1.ToString () - - override this.Equals other = - match other with - | :? TermCrate as other -> - { new TermEvaluator<_> with - member _.Eval<'b when 'b : equality> (other : 'b Term) = - if typeof<'a> = typeof<'b> then - t1 = unbox other - else - - printfn "%+A, %+A" typeof<'a> typeof<'b> - false - } - |> other.Apply - | _ -> false - interface TermCrate with - member _.Apply eval = eval.Eval t1 - } - -[] -module TypedTerm = - let force<'a> (TypedTerm t) : 'a Term = - { new TermEvaluator<_> with - member _.Eval t = unbox t - } - |> t.Apply - - let make<'a when 'a : equality> (t : 'a Term) : TypedTerm = TermCrate.make t |> TypedTerm - -/// Equality constraint is required because we use this crate for unification -type internal TermPairEvaluator<'ret> = - abstract Eval<'a when 'a : equality> : 'a Term -> 'a Term -> 'ret - -type internal TermPairCrate = - abstract Apply<'ret> : TermPairEvaluator<'ret> -> 'ret - -[] -module internal TermPairCrate = - let make<'a when 'a : equality> (t1 : 'a Term) (t2 : 'a Term) = - { new TermPairCrate with - member _.Apply eval = eval.Eval t1 t2 - } type Goal = private - | Equiv of TermPairCrate + | Equiv of Term * Term | Disj of Goal * Goal | Conj of Goal * Goal | Fresh of (Variable -> Goal) - | Delay of (unit -> Goal) -type State = - internal - { - Substitution : Map - VariableCounter : Variable - } +type internal State = + { + Substitution : Map + VariableCounter : Variable + } type Stream = private @@ -125,7 +44,7 @@ type Stream = | Nonempty of State * Stream [] -module State = +module private State = let empty = { VariableCounter = VariableCount 0 diff --git a/FicroKanSharp/FicroKanSharp.fsproj b/FicroKanSharp/FicroKanSharp.fsproj index f6b38fd..eb27334 100644 --- a/FicroKanSharp/FicroKanSharp.fsproj +++ b/FicroKanSharp/FicroKanSharp.fsproj @@ -7,9 +7,15 @@ + + + + + + diff --git a/FicroKanSharp/Goal.fs b/FicroKanSharp/Goal.fs index 4336377..aff355c 100644 --- a/FicroKanSharp/Goal.fs +++ b/FicroKanSharp/Goal.fs @@ -1,11 +1,13 @@ namespace FicroKanSharp +open FicroKanSharp + [] [] module Goal = let callFresh (f : Variable -> Goal) = Goal.Fresh f - let delay g = Goal.Delay g + let delay (g : unit -> Goal) = Goal.Fresh (fun _ -> g ()) /// Boolean "or": either goal must be satisfied. let disj (goal1 : Goal) (goal2 : Goal) : Goal = Goal.Disj (goal1, goal2) @@ -13,27 +15,39 @@ module Goal = /// Boolean "and": both goals must be satisfied simultaneously. let conj (goal1 : Goal) (goal2 : Goal) : Goal = Goal.Conj (goal1, goal2) - let equiv<'a when 'a : equality> (term1 : 'a Term) (term2 : 'a Term) : Goal = - TermPairCrate.make term1 term2 |> Goal.Equiv + let equiv (term1 : Term) (term2 : Term) : Goal = Goal.Equiv (term1, term2) - let private walk<'a> (u : Term<'a>) (s : State) : Term<'a> = + let never : Goal = + equiv (Term.Symbol ("_internal", [])) (Term.Symbol ("_internal", [ Term.Symbol ("_internal", []) ])) + + let always : Goal = + equiv (Term.Symbol ("_internal", [])) (Term.Symbol ("_internal", [])) + + let private walk (u : Term) (s : State) : Term = match u with - | Term.Variable u -> + | Term.Variable u as x -> match Map.tryFind u s.Substitution with - | None -> Term.Variable u - | Some (TypedTerm subst) -> - { new TermEvaluator<_> with - member _.Eval x = unbox x - } - |> subst.Apply + | None -> x + | Some subst -> subst | u -> u - let private extend<'a when 'a : equality> (v : Variable) (t : Term<'a>) (s : State) = + let private extend (v : Variable) (t : Term) (s : State) = { s with - Substitution = Map.add v (TermCrate.make t |> TypedTerm) s.Substitution + Substitution = Map.add v t s.Substitution } - let rec private unify<'a when 'a : equality> (u : 'a Term) (v : 'a Term) (s : State) : State option = + let rec private unifyList (args1 : _) (args2 : _) (state : State) : State option = + match args1, args2 with + | [], [] -> Some state + | _, [] + | [], _ -> None + | arg1 :: args1, arg2 :: args2 -> + + match unify arg1 arg2 state with + | None -> None + | Some state -> unifyList args1 args2 state + + and private unify (u : Term) (v : Term) (s : State) : State option = let u = walk u s let v = walk v s @@ -41,85 +55,36 @@ module Goal = | 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 | Term.Symbol (name1, args1), Term.Symbol (name2, args2) -> - if (name1 <> name2) || (args1.Length <> args2.Length) then + if name1.GetType () <> name2.GetType () then None else + let name2 = unbox name2 - let rec go state args1 args2 = - match args1, args2 with - | [], [] -> Some state - | _, [] - | [], _ -> None - | TypedTerm arg1 :: args1, TypedTerm arg2 :: args2 -> - { new TermEvaluator<_> with - member _.Eval<'t when 't : equality> (arg1 : Term<'t>) = - { new TermEvaluator<_> with - member _.Eval<'u when 'u : equality> (arg2 : Term<'u>) = - if typeof<'t> = typeof<'u> then - match unify arg1 (arg2 |> unbox) state with - | None -> None - | Some s -> go s args1 args2 - else - None - } - |> arg2.Apply - } - |> arg1.Apply - - go s args1 args2 + if (name1 <> name2) || (args1.Length <> args2.Length) then + None + else + unifyList args1 args2 s | _, _ -> None - let rec evaluate (goal : Goal) (state : State) : Stream = + let rec private evaluate' (goal : Goal) (state : State) : Stream = match goal with - | Goal.Equiv pair -> - { new TermPairEvaluator<_> with - member _.Eval u v = - match unify u v state with - | None -> Stream.empty - | Some unification -> Stream.Nonempty (unification, Stream.empty) - } - |> pair.Apply + | Goal.Equiv (t1, t2) -> + match unify t1 t2 state with + | None -> Stream.empty + | Some unification -> Stream.Nonempty (unification, Stream.empty) | Goal.Fresh goal -> let newVar = state.VariableCounter - evaluate - (goal newVar) - { state with - VariableCounter = Variable.incr state.VariableCounter - } - | Goal.Disj (goal1, goal2) -> Stream.union (evaluate goal1 state) (evaluate goal2 state) - | Goal.Conj (goal1, goal2) -> Stream.bind (evaluate goal1 state) (evaluate goal2) - | Goal.Delay g -> Stream.Procedure (fun () -> evaluate (g ()) state) + Stream.Procedure (fun () -> + evaluate' + (goal newVar) + { state with + VariableCounter = Variable.incr state.VariableCounter + } + ) + | Goal.Disj (goal1, goal2) -> Stream.union (evaluate' goal1 state) (evaluate' goal2 state) + | Goal.Conj (goal1, goal2) -> Stream.bind (evaluate' goal1 state) (evaluate' goal2) -(* - (dene (mK-reify s/c* ) -(map reify-state/1st-var s/c* )) -(dene (reify-state/1st -var s/c) -(let ((v (walk* (var 0) (car s/c)))) -(walk* v (reify-s v ' ())))) -The reier here, mK-reify, reies a list of states s/c* -by reifying each state's substitution with respect to the rst -variable. The reify-s, reify-name, and walk* helpers are -required for reify-state/1st-var. -(dene (reify-s v s) -(let ((v (walk v s))) -(cond -((var? v) -(let ((n (reify-name (length s)))) -(cons `(, v . , n) s))) -((pair? v) (reify-s (cdr v) (reify-s (car v) s))) -(else s)))) -(dene (reify-name n) -(stringsymbol -(string - append "_" "." (numberstring n)))) -(dene (walk* v s) -(let ((v (walk v s))) -(cond -((var? v) v) -((pair? v) (cons (walk* (car v) s) -(walk* (cdr v) s))) -(else v)))) -*) + let evaluate (goal : Goal) = evaluate' goal State.empty diff --git a/FicroKanSharp/Reflection.fs b/FicroKanSharp/Reflection.fs new file mode 100644 index 0000000..44487af --- /dev/null +++ b/FicroKanSharp/Reflection.fs @@ -0,0 +1,22 @@ +namespace FicroKanSharp + +open System +open FSharp.Quotations +open FSharp.Quotations.Patterns + +[] +module internal Reflection = + + let invokeStaticMethod (e : Expr) : Type seq -> obj seq -> obj = + let rec getMethodInfo = + function + | Call (_, mi, _) -> mi + | Lambda (_, e) -> getMethodInfo e + | _ -> failwith "Could not get MethodInfo" + + let mi = + (getMethodInfo e).GetGenericMethodDefinition () + + fun ts vs -> + mi.MakeGenericMethod (ts |> Array.ofSeq) + |> fun mi -> mi.Invoke (null, vs |> Array.ofSeq) diff --git a/FicroKanSharp/Stream.fs b/FicroKanSharp/Stream.fs index 3613e38..602929a 100644 --- a/FicroKanSharp/Stream.fs +++ b/FicroKanSharp/Stream.fs @@ -4,29 +4,29 @@ namespace FicroKanSharp [] module Stream = /// This is called mzero in the microKanren paper. - let empty : Stream = Stream.Empty + let internal empty : Stream = Stream.Empty /// This is called mplus in the microKanren paper. - let rec union (s1 : Stream) (s2 : Stream) : Stream = + let rec internal union (s1 : Stream) (s2 : Stream) : Stream = match s1 with | Stream.Empty -> s2 | Stream.Procedure s -> Stream.Procedure (fun () -> union s2 (s ())) | Stream.Nonempty (fst, rest) -> Stream.Nonempty (fst, union rest s2) - let rec bind (s : Stream) (g : State -> Stream) : Stream = + let rec internal bind (s : Stream) (g : State -> Stream) : Stream = match s with | Stream.Empty -> empty | Stream.Procedure s -> Stream.Procedure (fun () -> bind (s ()) g) | Stream.Nonempty (fst, rest) -> union (g fst) (bind rest g) - let rec peel (s : Stream) : (Map * Stream) option = + 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 ()) /// This will stack-overflow for an infinite stream. - let toList (s : Stream) : Map list = + let toList (s : Stream) : Map list = let rec go acc s = match s with | Stream.Empty -> acc @@ -34,3 +34,16 @@ module Stream = | Stream.Procedure p -> go acc (p ()) go [] s |> List.rev + + let take (n : int) (s : Stream) : Map list = + let rec go acc n s = + if n = 0 then + acc + else + + match s with + | Stream.Empty -> acc + | Stream.Nonempty (fst, rest) -> go (fst.Substitution :: acc) (n - 1) rest + | Stream.Procedure p -> go acc n (p ()) + + go [] n s |> List.rev diff --git a/FicroKanSharp/Term.fs b/FicroKanSharp/Term.fs new file mode 100644 index 0000000..2efecfa --- /dev/null +++ b/FicroKanSharp/Term.fs @@ -0,0 +1,6 @@ +namespace FicroKanSharp + +[] +module Term = + + let ofLiteral<'a> (a : 'a) : Term<'a> = Term.Symbol diff --git a/FicroKanSharp/Typed.fs b/FicroKanSharp/Typed.fs new file mode 100644 index 0000000..76d2994 --- /dev/null +++ b/FicroKanSharp/Typed.fs @@ -0,0 +1,69 @@ +namespace FicroKanSharp + +open System +open Microsoft.FSharp.Reflection + +type TypedTerm<'a> = + | Term of Term + | Literal of 'a + +[] +module TypedTerm = + + let variable<'a> (t : Variable) : TypedTerm<'a> = TypedTerm.Term (Term.Variable t) + + let literal<'a> (t : 'a) : TypedTerm<'a> = TypedTerm.Literal t + + let rec private toUntypedLiteral<'a when 'a : equality> (t : 'a) : Term = + let ty = typeof<'a> + + if ty = typeof then + Term.Variable (unbox t) + elif FSharpType.IsUnion ty then + let fieldU, valuesU = + FSharpValue.GetUnionFields (t, typeof<'a>) + + let toTermList (o : obj []) : Term list = + o + |> List.ofArray + |> List.map (fun (o : obj) -> + let ty = o.GetType () + + if ty.BaseType.IsGenericType + && ty.BaseType.GetGenericTypeDefinition () = typedefof>.GetGenericTypeDefinition + () then + o |> compileUntyped ty.GenericTypeArguments.[0] + else + ofLiteral ty o + ) + + let valuesU = toTermList valuesU + let td = typedefof<'a> + + Term.Symbol ((td, fieldU.Name), valuesU) + else + Term.Symbol ((ty, t), []) + + and private ofLiteral : Type -> obj -> Term = + let m = + Reflection.invokeStaticMethod <@ toUntypedLiteral @> + + fun tl o -> m [ tl ] [ o ] |> unbox + + and private compileUntyped : Type -> obj -> Term = + let m = + Reflection.invokeStaticMethod <@ compile @> + + fun tl o -> m [ tl ] [ o ] |> unbox + + and compile<'a when 'a : equality> (t : TypedTerm<'a>) : Term = + match t with + | TypedTerm.Term t -> t + | TypedTerm.Literal u -> toUntypedLiteral u + + [] + module Goal = + let callFresh<'a> (f : TypedTerm<'a> -> Goal) : Goal = + Goal.callFresh (fun v -> f (variable<'a> v)) + + let equiv (t1 : TypedTerm<'a>) (t2 : TypedTerm<'a>) : Goal = Goal.equiv (compile t1) (compile t2)