-
Notifications
You must be signed in to change notification settings - Fork 4
/
GuarderTests.fs
123 lines (116 loc) · 5.04 KB
/
GuarderTests.fs
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
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
/// <summary>
/// Tests for the guarder.
/// </summary>
module Starling.Tests.Guarder
open NUnit.Framework
open Starling.Utils.Testing
open Starling.Collections
open Starling.Core.Expr
open Starling.Core.Var
open Starling.Core.Symbolic
open Starling.Core.Model
open Starling.Core.GuardedView
open Starling.Core.View
open Starling.Lang.Modeller
open Starling.Lang.Guarder
/// Tests for the view guarder.
module Tests =
let oneGFunc (cnd : BoolExpr<Sym<Var>>) (name : string)
(ps : Expr<Sym<Var>> list)
: IteratedGFunc<Sym<Var>> =
iteratedGFunc cnd name ps (IInt 1L)
[<Test>]
let ``Convert the empty CView to the empty GView`` () =
assertEqual
(Multiset.empty : IteratedGView<Sym<Var>>)
(guardCView (Multiset.empty : CView))
[<Test>]
let ``Convert a flat CondView-list to a GuarView-list with no guard`` () =
assertEqual
(Multiset.ofFlatList
[ oneGFunc BTrue "foo" [ normalIntExpr (siVar "bar") ]
oneGFunc BTrue "bar" [ normalIntExpr (siVar "baz") ]] )
(guardCView
(Multiset.ofFlatList
[ iterated
(Func <| svfunc "foo" [ normalIntExpr (siVar "bar") ])
None
iterated
(Func <| svfunc "bar" [ normalIntExpr (siVar "baz") ] )
None ] ))
[<Test>]
let ``Convert a singly-nested CondView-list to a GuarView-list with unit guard`` () =
assertEqual
(Multiset.ofFlatList
[ oneGFunc (sbVar "s") "foo" [ normalIntExpr (siVar "bar") ]
oneGFunc (BNot (sbVar "s")) "bar" [ normalIntExpr (siVar "baz") ]] )
(guardCView <| Multiset.ofFlatList
[ iterated
(CFunc.ITE
(sbVar "s",
Multiset.ofFlatList
[ iterated
(Func <| svfunc "foo" [ normalIntExpr (siVar "bar") ] )
None ],
Multiset.ofFlatList
[ iterated
(Func <| svfunc "bar" [ normalIntExpr (siVar "baz") ] )
None ] ))
None ] )
[<Test>]
let ``Convert a complex-nested CondView-list to a GuarView-list with complex guards`` () =
assertEqual
(Multiset.ofFlatList
[ oneGFunc (BAnd [ sbVar "s"; sbVar "t" ] )
"foo"
[ normalIntExpr (siVar "bar") ]
oneGFunc (BAnd [ sbVar "s"; sbVar "t" ] )
"bar"
[ normalIntExpr (siVar "baz") ]
oneGFunc (BAnd [ sbVar "s"; BNot (sbVar "t") ] )
"fizz"
[ normalIntExpr (siVar "buzz") ]
oneGFunc (sbVar "s")
"in"
[ normalIntExpr (siVar "out") ]
oneGFunc (BNot (sbVar "s"))
"ding"
[ normalIntExpr (siVar "dong") ]] )
(guardCView <| Multiset.ofFlatList
[ iterated
(CFunc.ITE
(sbVar "s",
Multiset.ofFlatList
[ iterated
(CFunc.ITE
(sbVar "t",
Multiset.ofFlatList
[ iterated
(Func <| svfunc
"foo"
[ normalIntExpr (siVar "bar") ] )
None
iterated
(Func <| svfunc
"bar"
[ normalIntExpr (siVar "baz") ] )
None],
Multiset.ofFlatList
[ iterated
(Func <| svfunc
"fizz"
[ normalIntExpr (siVar "buzz") ] )
None]))
None
iterated
(Func <| svfunc
"in"
[ normalIntExpr (siVar "out") ])
None],
Multiset.ofFlatList
[ iterated
(Func <| svfunc
"ding"
[ normalIntExpr (siVar "dong") ])
None] ))
None ] )