Skip to content

Commit

Permalink
Update Fantomas
Browse files Browse the repository at this point in the history
  • Loading branch information
Smaug123 committed Jun 17, 2023
1 parent 7dd8f0d commit 02f8b6e
Show file tree
Hide file tree
Showing 11 changed files with 98 additions and 164 deletions.
6 changes: 3 additions & 3 deletions .config/dotnet-tools.json
Original file line number Diff line number Diff line change
Expand Up @@ -2,11 +2,11 @@
"version": 1,
"isRoot": true,
"tools": {
"fantomas-tool": {
"version": "4.6.0",
"fantomas": {
"version": "6.0.5",
"commands": [
"fantomas"
]
}
}
}
}
8 changes: 6 additions & 2 deletions .editorconfig
Original file line number Diff line number Diff line change
Expand Up @@ -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
9 changes: 4 additions & 5 deletions FicroKanSharp.Test/Arithmetic.fs
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down Expand Up @@ -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)))
)
)

Expand Down
8 changes: 2 additions & 6 deletions FicroKanSharp.Test/Recursive.fs
Original file line number Diff line number Diff line change
Expand Up @@ -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
]
)
50 changes: 8 additions & 42 deletions FicroKanSharp.Test/TestExamples.fs
Original file line number Diff line number Diff line change
Expand Up @@ -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 -> ()
Expand All @@ -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>]
Expand All @@ -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>]
Expand Down
10 changes: 3 additions & 7 deletions FicroKanSharp.Test/TypedArithmetic.fs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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)
))
)

Expand Down
8 changes: 2 additions & 6 deletions FicroKanSharp/Domain.fs
Original file line number Diff line number Diff line change
Expand Up @@ -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}"
Expand All @@ -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
Expand Down
18 changes: 3 additions & 15 deletions FicroKanSharp/Goal.fs
Original file line number Diff line number Diff line change
Expand Up @@ -86,8 +86,7 @@ module Goal =
None
else
//(unify : Term -> Term -> bool option)
if unifyMethod.ReturnParameter.ParameterType
<> typeof<State option> then
if unifyMethod.ReturnParameter.ParameterType <> typeof<State option> then
failwith
$"Incorrect unify return parameter should have been Option<State>: {unifyMethod.ReturnParameter.ParameterType}"

Expand Down Expand Up @@ -125,17 +124,7 @@ module Goal =
failwith $"Wrong parameters on Unify method of type {ty.Name}: {wrongParams}"

let result =
unifyMethod.Invoke (
name1,
[|
unify
name1
args1
name2
args2
state
|]
)
unifyMethod.Invoke (name1, [| unify ; name1 ; args1 ; name2 ; args2 ; state |])
|> unbox<State option>

result
Expand All @@ -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
Expand Down
10 changes: 5 additions & 5 deletions FicroKanSharp/Reify.fs
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand All @@ -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"
8 changes: 4 additions & 4 deletions FicroKanSharp/Stream.fs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Loading

0 comments on commit 02f8b6e

Please sign in to comment.