Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Update Fantomas #5

Merged
merged 2 commits into from
Jun 17, 2023
Merged

Update Fantomas #5

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
5e0c3e3
Update Fantomas
Smaug123 Jun 17, 2023
bb842d0
Fix workflow
Smaug123 Jun 17, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions .config/dotnet-tools.json
View file
Open in desktop
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
View file
Open in desktop
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
2 changes: 1 addition & 1 deletion .github/workflows/dotnet-core.yaml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,4 +26,4 @@ jobs:
- name: Install Fantomas
run: dotnet tool restore
- name: Run Fantomas
run: dotnet tool run fantomas --check -r .
run: dotnet tool run fantomas --check .
9 changes: 4 additions & 5 deletions FicroKanSharp.Test/Arithmetic.fs
View file
Open in desktop
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
View file
Open in desktop
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
View file
Open in desktop
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
View file
Open in desktop
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
View file
Open in desktop
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
20 changes: 3 additions & 17 deletions FicroKanSharp/Goal.fs
View file
Open in desktop
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 All @@ -178,8 +166,6 @@ module Goal =
else
customUnification ty name1 args1 name2 args2 s

| _, _ -> None

let rec private evaluate' (debug : bool) (goal : Goal) (state : State) : Stream =
if debug then
let varState =
Expand Down
49 changes: 19 additions & 30 deletions FicroKanSharp/Typed.fs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,17 +12,17 @@ type TypedTerm<'a> =

type private TermConstructor =
{
Literal : obj [] -> obj
Term : obj [] -> obj
Literal : obj[] -> obj
Term : obj[] -> obj
}

type private FSharpUnionCase =
{
Name : string
/// The PropertyInfo for the field, and the Literal case constructor of the TypedTerm
/// if it is one
Fields : (PropertyInfo * Option<TermConstructor>) []
Constructor : obj [] -> obj
Fields : (PropertyInfo * Option<TermConstructor>)[]
Constructor : obj[] -> obj
}

[<NoComparison ; CustomEquality>]
Expand All @@ -37,9 +37,7 @@ type internal TypeName<'a when 'a : equality> =

override this.Equals (other : obj) : bool =
match other with
| :? TypeName<'a> as other ->
this.UserType = other.UserType
&& this.FieldValue = other.FieldValue
| :? TypeName<'a> as other -> this.UserType = other.UserType && this.FieldValue = other.FieldValue
| _ -> false

override this.GetHashCode () = hash (this.UserType, this.FieldValue)
Expand All @@ -50,9 +48,7 @@ type internal TypeName<'a when 'a : equality> =
| Some (cases, tagDiscriminator) ->

if t1.FieldValue.GetType () = typeof<string> then
let case =
cases
|> Array.find (fun case -> case.Name = unbox<string> t1.FieldValue)
let case = cases |> Array.find (fun case -> case.Name = unbox<string> t1.FieldValue)

args
|> List.mapi (fun i term ->
Expand All @@ -65,11 +61,10 @@ type internal TypeName<'a when 'a : equality> =
.GetType()
.GetMethod(
"Unbox",
BindingFlags.Public
||| BindingFlags.NonPublic
||| BindingFlags.Instance
BindingFlags.Public ||| BindingFlags.NonPublic ||| BindingFlags.Instance
)
.MakeGenericMethod typeof<obj>
.MakeGenericMethod
typeof<obj>

let unboxed = mi.Invoke (name, [||]) |> unbox<TypeName<obj>>

Expand Down Expand Up @@ -110,8 +105,7 @@ type internal TypeName<'a when 'a : equality> =
None
else

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 @@ -169,24 +163,23 @@ module TypedTerm =
let literal<'a> (t : 'a) : TypedTerm<'a> = TypedTerm.Literal t

let resolveGeneric (t : Type) : Type =
if t.IsGenericType then
t.GetGenericTypeDefinition ()
else
t
if t.IsGenericType then t.GetGenericTypeDefinition () else t

let rec private toUntypedLiteral' (ty : Type) : obj -> Term =
if ty = typeof<Variable> then
fun t -> Term.Variable (unbox t)
elif FSharpType.IsUnion ty then
let toTermList (o : obj []) : Term list =
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<TypedTerm<obj>>.GetGenericTypeDefinition
() then
if
ty.BaseType.IsGenericType
&& ty.BaseType.GetGenericTypeDefinition () = typedefof<TypedTerm<obj>>
.GetGenericTypeDefinition ()
then
o |> compileUntyped ty.GenericTypeArguments.[0]
else
toUntypedLiteral o
Expand All @@ -208,8 +201,7 @@ module TypedTerm =
let ty = pi.PropertyType

let isTypedTerm =
ty.IsGenericType
&& ty.GetGenericTypeDefinition () = typedefof<TypedTerm<obj>>
ty.IsGenericType && ty.GetGenericTypeDefinition () = typedefof<TypedTerm<obj>>

let constructor =
if isTypedTerm then
Expand Down Expand Up @@ -240,10 +232,7 @@ module TypedTerm =
fun t ->
let case = cases.[precomputed t]

let values =
case.Fields
|> Array.map (fun (pi, _) -> pi.GetValue t)
|> toTermList
let values = case.Fields |> Array.map (fun (pi, _) -> pi.GetValue t) |> toTermList

Term.Symbol (
{
Expand Down