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

Raw view Test code New version

More information

Link:	http://fssnip.net/pn
Posted:	9 years ago
Author:	Nick Palladinos
Tags:	type level