Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- module Term
- type Term =
- // Constants
- | False
- | True
- // Variables
- | Var of int
- // Quantifiers
- | All of Term * Term
- // Predicates
- | Eqv of Term * Term
- | Not of Term
- | Or of Term list
- // Comparison
- | Equal of Term * Term
- type ShapeInfo = Shape of Term
- let (|Leaf|Node|) a =
- match a with
- | False
- | True ->
- Leaf(Shape a)
- | Var n ->
- Leaf(Shape a)
- | Not x ->
- Node(Shape a, [x])
- | All(x, y)
- | Equal(x, y)
- | Eqv(x, y) ->
- Node(Shape a, [x; y])
- | Or xs ->
- Node(Shape a, xs)
- let FromLeaf(Shape a) =
- a
- let FromNode(Shape a, xs) =
- match a, xs with
- | All(_, _), [x; y] ->
- All(x, y)
- | Eqv(_, _), [x; y] ->
- Eqv(x, y)
- | Not _, [x] ->
- Not x
- | Or _, xs ->
- Or xs
- | Equal(_, _), [x; y] ->
- Equal(x, y)
- | _ ->
- failwith "Internal error"
- let rec eval model a =
- match a with
- | Equal(x, y) when x = y ->
- True
- | Not False ->
- True
- | Not True ->
- False
- | Or xs ->
- let xs' = List.map(eval model) xs
- |> List.filter(fun x -> x <> False)
- if List.exists(fun x -> x = True) xs' then
- True
- else
- match xs' with
- | [] ->
- False
- | [x] ->
- x
- | _ ->
- Or xs'
- | Node(s, xs) ->
- FromNode(s, List.map(eval model) xs)
- | Leaf _ ->
- a
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement