Update Fantomas

Smaug123 · Jun 17, 2023 · baadea6 · baadea6
1 parent 7dd8f0d
commit baadea6
Show file tree

Hide file tree

Showing 11 changed files with 135 additions and 201 deletions.
diff --git a/.config/dotnet-tools.json b/.config/dotnet-tools.json
@@ -2,11 +2,11 @@
   "version": 1,
   "isRoot": true,
   "tools": {
-    "fantomas-tool": {
-      "version": "4.6.0",
+    "fantomas": {
+      "version": "6.0.5",
       "commands": [
         "fantomas"
       ]
     }
   }
-}
+}
diff --git a/.editorconfig b/.editorconfig
@@ -7,8 +7,12 @@ fsharp_space_before_colon=true
 fsharp_space_before_semicolon=true
 fsharp_multiline_block_brackets_on_same_column=true
 fsharp_newline_between_type_definition_and_members=true
-fsharp_keep_indent_in_branch=true
+fsharp_experimental_keep_indent_in_branch=true
 fsharp_align_function_signature_to_indentation=true
 fsharp_alternative_long_member_definitions=true
-fsharp_disable_elmish_syntax=true
+fsharp_multiline_bracket_style=aligned
 fsharp_multi_line_lambda_closing_newline=true
+fsharp_max_value_binding_width=80
+fsharp_max_record_width=0
+max_line_length=120
+end_of_line=lf
diff --git a/FicroKanSharp.Test/Arithmetic.fs b/FicroKanSharp.Test/Arithmetic.fs
@@ -13,10 +13,7 @@ module Arithmetic =
         let succ (x : Term) : Term = Term.Symbol ("succ", [ x ])
 
         let rec ofInt (n : int) : Term =
-            if n = 0 then
-                zero
-            else
-                succ (ofInt (n - 1))
+            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 =
@@ -125,7 +122,9 @@ module Arithmetic =
 
                         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)))
+                            (Goal.conj
+                                (Goal.equiv z (succ m |> TypedTerm.compile))
+                                (Goal.delay (fun () -> pluso n y m)))
                     )
                 )
 

diff --git a/FicroKanSharp.Test/Recursive.fs b/FicroKanSharp.Test/Recursive.fs
@@ -101,11 +101,7 @@ module Recursive =
         |> shouldEqual (
             Map.ofList
                 [
-                    VariableCount 0,
-                    TypedTerm.literal (Human "bridget")
-                    |> TypedTerm.compile
-                    VariableCount 1,
-                    TypedTerm.literal (Human "caroline")
-                    |> TypedTerm.compile
+                    VariableCount 0, TypedTerm.literal (Human "bridget") |> TypedTerm.compile
+                    VariableCount 1, TypedTerm.literal (Human "caroline") |> TypedTerm.compile
                 ]
         )
diff --git a/FicroKanSharp.Test/TestExamples.fs b/FicroKanSharp.Test/TestExamples.fs
@@ -58,12 +58,7 @@ module TestThing =
         | None -> failwith "oh no"
         | Some (s, rest) ->
 
-        s
-        |> Map.toList
-        |> shouldEqual
-            [
-                Variable.VariableCount 0, Term.Symbol (5, [])
-            ]
+        s |> Map.toList |> shouldEqual [ Variable.VariableCount 0, Term.Symbol (5, []) ]
 
         match Stream.peel rest with
         | None -> ()
@@ -78,18 +73,9 @@ module TestThing =
         |> Stream.take 3
         |> shouldEqual
             [
-                Map.ofList
-                    [
-                        Variable.VariableCount 0, Term.Symbol (5, [])
-                    ]
-                Map.ofList
-                    [
-                        Variable.VariableCount 0, Term.Symbol (5, [])
-                    ]
-                Map.ofList
-                    [
-                        Variable.VariableCount 0, Term.Symbol (5, [])
-                    ]
+                Map.ofList [ Variable.VariableCount 0, Term.Symbol (5, []) ]
+                Map.ofList [ Variable.VariableCount 0, Term.Symbol (5, []) ]
+                Map.ofList [ Variable.VariableCount 0, Term.Symbol (5, []) ]
             ]
 
     [<Fact>]
@@ -108,45 +94,25 @@ module TestThing =
         | None -> failwith "oh no"
         | Some (s, rest) ->
 
-        s
-        |> Map.toList
-        |> shouldEqual
-            [
-                Variable.VariableCount 0, Term.Symbol (5, [])
-            ]
+        s |> Map.toList |> shouldEqual [ Variable.VariableCount 0, Term.Symbol (5, []) ]
 
         match Stream.peel rest with
         | None -> failwith "oh no"
         | Some (s, rest) ->
 
-        s
-        |> Map.toList
-        |> shouldEqual
-            [
-                Variable.VariableCount 0, Term.Symbol (6, [])
-            ]
+        s |> Map.toList |> shouldEqual [ Variable.VariableCount 0, Term.Symbol (6, []) ]
 
         match Stream.peel rest with
         | None -> failwith "oh no"
         | Some (s, rest) ->
 
-        s
-        |> Map.toList
-        |> shouldEqual
-            [
-                Variable.VariableCount 0, Term.Symbol (5, [])
-            ]
+        s |> Map.toList |> shouldEqual [ Variable.VariableCount 0, Term.Symbol (5, []) ]
 
         match Stream.peel rest with
         | None -> failwith "oh no"
         | Some (s, _rest) ->
 
-            s
-            |> Map.toList
-            |> shouldEqual
-                [
-                    Variable.VariableCount 0, Term.Symbol (6, [])
-                ]
+            s |> Map.toList |> shouldEqual [ Variable.VariableCount 0, Term.Symbol (6, []) ]
 
     /// This arose because x0 unified to x1, x1 unified to 1, but x0 didn't get reduced to 1 by `walk`.
     [<Fact>]

diff --git a/FicroKanSharp.Test/TypedArithmetic.fs b/FicroKanSharp.Test/TypedArithmetic.fs
@@ -26,12 +26,7 @@ module TypedArithmetic =
                 if t2 = 0 then
                     None
                 else
-                    unify
-                        (TypedTerm.compile t1)
-                        (Pure (t2 - 1)
-                         |> TypedTerm.literal
-                         |> TypedTerm.compile)
-                        state
+                    unify (TypedTerm.compile t1) (Pure (t2 - 1) |> TypedTerm.literal |> TypedTerm.compile) state
             | Pure t1, Succ t2 ->
                 if t1 = 0 then
                     None
@@ -69,7 +64,8 @@ module TypedArithmetic =
             TypedTerm.Goal.callFresh (fun n ->
                 Goal.conj
                     (TypedTerm.Goal.equiv x (succ n))
-                    (TypedTerm.Goal.callFresh (fun ny -> Goal.conj (Goal.delay (fun () -> timeso n y ny)) (pluso y ny z)
+                    (TypedTerm.Goal.callFresh (fun ny ->
+                        Goal.conj (Goal.delay (fun () -> timeso n y ny)) (pluso y ny z)
                     ))
             )
 

diff --git a/FicroKanSharp/Domain.fs b/FicroKanSharp/Domain.fs
@@ -16,10 +16,7 @@ type Term =
     override this.ToString () =
         match this with
         | Symbol (name, args) ->
-            let s =
-                args
-                |> List.map (sprintf "%O")
-                |> String.concat ", "
+            let s = args |> List.map (sprintf "%O") |> String.concat ", "
 
             $"{name}[{s}]"
         | Variable (VariableCount v) -> $"x{v}"
@@ -38,8 +35,7 @@ type Goal =
             if variableCount > 4 then
                 "<exists x: ...>"
             else
-                $"exists x{variableCount}: ({(g (VariableCount variableCount))
-                                                 .ToString (variableCount + 1)})"
+                $"exists x{variableCount}: ({(g (VariableCount variableCount)).ToString (variableCount + 1)})"
         | Conj (g1, g2) -> sprintf "((%s) AND (%s))" (g1.ToString variableCount) (g2.ToString variableCount)
         | Disj (g1, g2) -> sprintf "((%s) OR  (%s))" (g1.ToString variableCount) (g2.ToString variableCount)
         | Equiv (g1, g2) -> sprintf "(%O) == (%O)" g1 g2

diff --git a/FicroKanSharp/Goal.fs b/FicroKanSharp/Goal.fs
@@ -59,9 +59,9 @@ module Goal =
         | [], _ -> None
         | arg1 :: args1, arg2 :: args2 ->
 
-        match unify arg1 arg2 state with
-        | None -> None
-        | Some state -> unifyList args1 args2 state
+            match unify arg1 arg2 state with
+            | None -> None
+            | Some state -> unifyList args1 args2 state
 
     and private customUnification<'a>
         (ty : System.Type)
@@ -85,61 +85,50 @@ module Goal =
             // Custom unification fails because the user didn't provide any unification rules
             None
         else
-        //(unify : Term -> Term -> bool option)
-        if unifyMethod.ReturnParameter.ParameterType
-           <> typeof<State option> then
-            failwith
-                $"Incorrect unify return parameter should have been Option<State>: {unifyMethod.ReturnParameter.ParameterType}"
+            //(unify : Term -> Term -> bool option)
+            if unifyMethod.ReturnParameter.ParameterType <> typeof<State option> then
+                failwith
+                    $"Incorrect unify return parameter should have been Option<State>: {unifyMethod.ReturnParameter.ParameterType}"
 
-        match unifyMethod.GetParameters () with
-        | [| unifyParam ; _name1Param ; args1Param ; _name2Param ; args2Param ; stateParam |] ->
-            let wrongParams =
-                [
-                    let t = typeof<Term -> Term -> State -> State option>
+            match unifyMethod.GetParameters () with
+            | [| unifyParam ; _name1Param ; args1Param ; _name2Param ; args2Param ; stateParam |] ->
+                let wrongParams =
+                    [
+                        let t = typeof<Term -> Term -> State -> State option>
 
-                    if unifyParam.ParameterType <> t then
-                        yield nameof unifyParam, t
+                        if unifyParam.ParameterType <> t then
+                            yield nameof unifyParam, t
 
-                    let t = typeof<Term list>
+                        let t = typeof<Term list>
 
-                    if args1Param.ParameterType <> t then
-                        yield nameof args1Param, t
+                        if args1Param.ParameterType <> t then
+                            yield nameof args1Param, t
 
-                    if args2Param.ParameterType <> t then
-                        yield nameof args2Param, t
+                        if args2Param.ParameterType <> t then
+                            yield nameof args2Param, t
 
-                    let t = typeof<State>
+                        let t = typeof<State>
 
-                    if stateParam.ParameterType <> t then
-                        yield nameof stateParam, t
-                ]
+                        if stateParam.ParameterType <> t then
+                            yield nameof stateParam, t
+                    ]
 
-            match wrongParams with
-            | [] -> ()
-            | wrongParams ->
-                let wrongParams =
-                    wrongParams
-                    |> List.map (fun (s, ty) -> $"{s} (expected: {ty.Name})")
-                    |> String.concat "; "
-
-                failwith $"Wrong parameters on Unify method of type {ty.Name}: {wrongParams}"
-
-            let result =
-                unifyMethod.Invoke (
-                    name1,
-                    [|
-                        unify
-                        name1
-                        args1
-                        name2
-                        args2
-                        state
-                    |]
-                )
-                |> unbox<State option>
-
-            result
-        | parameters -> failwith $"Incorrect unify parameters: {parameters |> Array.toList}"
+                match wrongParams with
+                | [] -> ()
+                | wrongParams ->
+                    let wrongParams =
+                        wrongParams
+                        |> List.map (fun (s, ty) -> $"{s} (expected: {ty.Name})")
+                        |> String.concat "; "
+
+                    failwith $"Wrong parameters on Unify method of type {ty.Name}: {wrongParams}"
+
+                let result =
+                    unifyMethod.Invoke (name1, [| unify ; name1 ; args1 ; name2 ; args2 ; state |])
+                    |> unbox<State option>
+
+                result
+            | parameters -> failwith $"Incorrect unify parameters: {parameters |> Array.toList}"
 
 
     and private unify (uIn : Term) (vIn : Term) (s : State) : State option =
@@ -155,8 +144,7 @@ module Goal =
                 name1.GetType ()
                 |> fun ty ->
                     if FSharpType.IsUnion ty then
-                        if FSharpType.GetUnionCases ty
-                           |> Array.forall (fun i -> i.GetFields().Length = 0) then
+                        if FSharpType.GetUnionCases ty |> Array.forall (fun i -> i.GetFields().Length = 0) then
                             // reference enum
                             ty
                         else

diff --git a/FicroKanSharp/Reify.fs b/FicroKanSharp/Reify.fs
@@ -17,9 +17,9 @@ module Reify =
         | Term.Variable v -> Map.find v state |> reify state
         | Term.Symbol (name, args) ->
 
-        let args = args |> List.map (reify state)
+            let args = args |> List.map (reify state)
 
-        Term.Symbol (name, args)
+            Term.Symbol (name, args)
 
     let rec withRespectToFirst (s : Stream) : seq<Term option> =
         seq {
@@ -43,6 +43,6 @@ module Reify =
         | None -> false
         | Some (_, other) ->
 
-        match Stream.peel other with
-        | None -> true
-        | Some _ -> failwith "expected exactly one solution"
+            match Stream.peel other with
+            | None -> true
+            | Some _ -> failwith "expected exactly one solution"
diff --git a/FicroKanSharp/Stream.fs b/FicroKanSharp/Stream.fs
@@ -41,9 +41,9 @@ module Stream =
                 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 ())
+                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