mirror of
https://github.com/Smaug123/FicroKanSharp
synced 2025-10-11 06:18:40 +00:00
Split into an untyped core and a typed layer (#1)
This commit is contained in:
Patrick Stevens
GitHub
@@ -6,23 +6,20 @@ open Xunit
|
||||
|
||||
module Arithmetic =
|
||||
|
||||
type Nat = Nat
|
||||
|
||||
[<Fact>]
|
||||
let ``Arithmetic example`` () =
|
||||
let zero : Term<Nat> = Term.Symbol ("zero", [])
|
||||
let ``Arithmetic example, untyped`` () =
|
||||
let zero : Term = Term.Symbol ("zero", [])
|
||||
|
||||
let succ (x : Term<Nat>) : Term<Nat> =
|
||||
Term.Symbol ("succ", [ TypedTerm.make x ])
|
||||
let succ (x : Term) : Term = Term.Symbol ("succ", [ x ])
|
||||
|
||||
let rec ofInt (n : int) : Term<Nat> =
|
||||
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<Nat>) (y : Term<Nat>) (z : Term<Nat>) : 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<Nat> (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<Nat>
|
||||
|
||||
[<Fact>]
|
||||
let ``Arithmetic example, typed`` () =
|
||||
let rec ofInt (n : int) : TypedTerm<Nat> =
|
||||
if n = 0 then
|
||||
Nat.Zero |> TypedTerm.literal
|
||||
else
|
||||
Nat.Succ (ofInt (n - 1)) |> TypedTerm.literal
|
||||
|
||||
let succ (n : TypedTerm<Nat>) = Nat.Succ n |> TypedTerm.literal
|
||||
let zero = Nat.Zero |> TypedTerm.literal
|
||||
|
||||
let rec numeralo (x : TypedTerm<Nat>) : 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<Nat>) (y : TypedTerm<Nat>) (z : TypedTerm<Nat>) : 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)
|
||||
]
|
||||
)
|
||||
|
||||
Reference in New Issue
Block a user