Type the terms

2025-10-08 13:08:40 +00:00 · 2021-12-24 21:37:27 +00:00
parent 200f94b72d
commit 35b567d181
5 changed files with 142 additions and 82 deletions
--- a/FicroKanSharp.Test/TestExamples.fs
+++ b/FicroKanSharp.Test/TestExamples.fs
@@ -24,6 +24,7 @@ module TestThing =
        | Some (s, rest) ->

        s
+        |> Map.map (fun _ -> TypedTerm.force<int>)
        |> Map.toList
        |> shouldEqual
            [
@@ -36,6 +37,7 @@ module TestThing =
        | Some (s, rest) ->

        s
+        |> Map.map (fun _ -> TypedTerm.force<int>)
        |> Map.toList
        |> shouldEqual
            [
@@ -59,6 +61,7 @@ module TestThing =
        | Some (s, rest) ->

        s
+        |> Map.map (fun _ -> TypedTerm.force<int>)
        |> Map.toList
        |> shouldEqual
            [
@@ -82,6 +85,7 @@ module TestThing =
        | Some (s, rest) ->

        s
+        |> Map.map (fun _ -> TypedTerm.force<int>)
        |> Map.toList
        |> shouldEqual
            [
@@ -93,6 +97,7 @@ module TestThing =
        | Some (s, rest) ->

        s
+        |> Map.map (fun _ -> TypedTerm.force<int>)
        |> Map.toList
        |> shouldEqual
            [
@@ -104,6 +109,7 @@ module TestThing =
        | Some (s, _rest) ->

            s
+            |> Map.map (fun _ -> TypedTerm.force<int>)
            |> Map.toList
            |> shouldEqual
                [
@@ -128,6 +134,7 @@ module TestThing =
        | Some (s, rest) ->

        s
+        |> Map.map (fun _ -> TypedTerm.force<int>)
        |> Map.toList
        |> shouldEqual
            [
@@ -139,6 +146,7 @@ module TestThing =
        | Some (s, rest) ->

        s
+        |> Map.map (fun _ -> TypedTerm.force<int>)
        |> Map.toList
        |> shouldEqual
            [
@@ -150,6 +158,7 @@ module TestThing =
        | Some (s, rest) ->

        s
+        |> Map.map (fun _ -> TypedTerm.force<int>)
        |> Map.toList
        |> shouldEqual
            [
@@ -161,6 +170,7 @@ module TestThing =
        | Some (s, _rest) ->

            s
+            |> Map.map (fun _ -> TypedTerm.force<int>)
            |> Map.toList
            |> shouldEqual
                [
--- a/FicroKanSharp/Domain.fs
+++ b/FicroKanSharp/Domain.fs
@@ -6,13 +6,50 @@ type Variable = internal VariableCount of int
 module private Variable =
    let incr (VariableCount v) = VariableCount (v + 1)

-type Term =
-    | Literal of int
+type Term<'a> =
+    | Literal of 'a
    | Variable of Variable

+/// 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
+
+[<RequireQualifiedAccess>]
+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 internal TermEvaluator<'ret> =
+    abstract Eval<'a> : 'a Term -> 'ret
+
+type internal TermCrate =
+    abstract Apply<'ret> : TermEvaluator<'ret> -> 'ret
+
+[<RequireQualifiedAccess>]
+module internal TermCrate =
+    let make<'a> (t1 : 'a Term) =
+        { new TermCrate with
+            member _.Apply eval = eval.Eval t1
+        }
+
+type TypedTerm = internal TypedTerm of TermCrate
+
+[<RequireQualifiedAccess>]
+module TypedTerm =
+    let force<'a> (TypedTerm t) : 'a Term =
+        { new TermEvaluator<_> with
+            member _.Eval t = unbox t
+        }
+        |> t.Apply
+
 type Goal =
    private
-    | Equiv of Term * Term
+    | Equiv of TermPairCrate
    | Disj of Goal * Goal
    | Conj of Goal * Goal
    | Fresh of (Variable -> Goal)
@@ -21,7 +58,7 @@ type Goal =
 type State =
    internal
        {
-            Substitution : Map<Variable, Term>
+            Substitution : Map<Variable, TypedTerm>
            VariableCounter : Variable
        }

@@ -38,80 +75,3 @@ module State =
            VariableCounter = VariableCount 0
            Substitution = Map.empty
        }
-
-[<RequireQualifiedAccess>]
-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)
-
-    let rec peel (s : Stream) : (Map<Variable, Term> * Stream) option =
-        match s with
-        | Stream.Empty -> None
-        | Stream.Nonempty (fst, rest) -> Some (fst.Substitution, rest)
-        | Stream.Procedure p -> peel (p ())
-
-[<RequireQualifiedAccess>]
-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)
-
-    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)
-        | Goal.Delay g -> Stream.Procedure (fun () -> evaluate (g ()) state)
--- a/FicroKanSharp/FicroKanSharp.fsproj
+++ b/FicroKanSharp/FicroKanSharp.fsproj
@@ -6,8 +6,10 @@
    </PropertyGroup>

    <ItemGroup>
-        <Compile Include="Domain.fs" />
        <Compile Include="AssemblyInfo.fs" />
+        <Compile Include="Domain.fs" />
+        <Compile Include="Stream.fs" />
+        <Compile Include="Goal.fs" />
    </ItemGroup>

 </Project>
--- a/FicroKanSharp/Goal.fs
+++ b/FicroKanSharp/Goal.fs
@@ -0,0 +1,64 @@
+namespace FicroKanSharp
+
+[<RequireQualifiedAccess>]
+[<CompilationRepresentation(CompilationRepresentationFlags.ModuleSuffix)>]
+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)
+
+    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 walk<'a> (u : Term<'a>) (s : State) : Term<'a> =
+        match u with
+        | Term.Variable u ->
+            match Map.tryFind u s.Substitution with
+            | None -> Term.Variable u
+            | Some (TypedTerm subst) ->
+                { new TermEvaluator<_> with
+                    member _.Eval x = unbox x
+                }
+                |> subst.Apply
+        | u -> u
+
+    let extend<'a> (v : Variable) (t : Term<'a>) (s : State) =
+        { s with
+            Substitution = Map.add v (TermCrate.make t |> TypedTerm) s.Substitution
+        }
+
+    let rec unify<'a when 'a : equality> (u : 'a Term) (v : 'a Term) (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 pair ->
+            { new TermPairEvaluator<_> with
+                member _.Eval u v =
+                    match unify u v state with
+                    | None -> Stream.mzero
+                    | Some unification -> Stream.Nonempty (unification, Stream.mzero)
+            }
+            |> pair.Apply
+        | 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)
+        | Goal.Delay g -> Stream.Procedure (fun () -> evaluate (g ()) state)
--- a/FicroKanSharp/Stream.fs
+++ b/FicroKanSharp/Stream.fs
@@ -0,0 +1,24 @@
+namespace FicroKanSharp
+
+[<RequireQualifiedAccess>]
+[<CompilationRepresentation(CompilationRepresentationFlags.ModuleSuffix)>]
+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)
+
+    let rec peel (s : Stream) : (Map<Variable, TypedTerm> * Stream) option =
+        match s with
+        | Stream.Empty -> None
+        | Stream.Nonempty (fst, rest) -> Some (fst.Substitution, rest)
+        | Stream.Procedure p -> peel (p ())