 5 people like it.

# A type-level SAT solver in F#

A type-level SAT solver in F#, inspired by https://gist.github.com/wouter-swierstra/0b6062c9660e751cd535

 ``` 1: 2: 3: 4: 5: 6: 7: 8: 9: 10: 11: 12: 13: 14: 15: 16: 17: 18: 19: 20: 21: 22: 23: 24: 25: 26: 27: 28: 29: 30: 31: 32: 33: 34: ``` ``````type Bool = interface end and True = True with interface Bool and False = False with interface Bool type And = And with static member inline (?<-) (True, And, True) = True static member inline (?<-) (True, And, False) = False static member inline (?<-) (False, And, True) = False static member inline (?<-) (False, And, False) = False and Or = Or with static member inline (?<-) (True, Or, True) = True static member inline (?<-) (True, Or, False) = True static member inline (?<-) (False, Or, True) = True static member inline (?<-) (False, Or, False) = False and Not = Not with static member inline (\$) (Not, True) = False static member inline (\$) (Not, False) = True let inline (<&&>) a b = (a ? (And) <- b ) let inline (<||>) a b = (a ? (Or) <- b ) let inline not a = Not \$ a let inline solve (p : ^T -> True) = typeof< ^T>.FullName solve (fun a -> not a) // False solve (fun a -> not (not a)) // True solve (fun (a, b) -> a <&&> (not b)) // (True, False) solve (fun a -> a <&&> (not a)) // type error ``````
Multiple items
union case True.True: True

--------------------
type True =
| True
interface Bool

Full name: Script.True
type Bool

Full name: Script.Bool
type False =
| False
interface Bool

Full name: Script.False
Multiple items
union case False.False: False

--------------------
type False =
| False
interface Bool

Full name: Script.False
Multiple items
union case And.And: And

--------------------
type And =
| And
static member ( ?<- ) : True:True * And:And * True:True -> True
static member ( ?<- ) : True:True * And:And * False:False -> False
static member ( ?<- ) : False:False * And:And * True:True -> False
static member ( ?<- ) : False:False * And:And * False:False -> False

Full name: Script.And
Multiple items
union case Or.Or: Or

--------------------
type Or =
| Or
static member ( ?<- ) : True:True * Or:Or * True:True -> True
static member ( ?<- ) : True:True * Or:Or * False:False -> True
static member ( ?<- ) : False:False * Or:Or * True:True -> True
static member ( ?<- ) : False:False * Or:Or * False:False -> False

Full name: Script.Or
Multiple items
union case Not.Not: Not

--------------------
type Not =
| Not
static member ( \$ ) : Not:Not * True:True -> False
static member ( \$ ) : Not:Not * False:False -> True

Full name: Script.Not
val a : 'a (requires member ( ?<- ))
val b : 'b (requires member ( ?<- ))
val not : a:'a -> '_arg3 (requires member ( \$ ))

Full name: Script.not
val a : 'a (requires member ( \$ ))
val solve : p:('T -> True) -> string

Full name: Script.solve
val p : ('T -> True)
val typeof<'T> : System.Type

Full name: Microsoft.FSharp.Core.Operators.typeof
val a : False
val a : True
val b : False
val a : obj