Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
I
inox
Manage
Activity
Members
Labels
Plan
Issues
Issue boards
Milestones
Wiki
Code
Merge requests
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Snippets
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Package registry
Model registry
Operate
Environments
Terraform modules
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
LARA
inox
Commits
a50cf05c
Commit
a50cf05c
authored
15 years ago
by
Mirco Dotta
Browse files
Options
Downloads
Patches
Plain Diff
Fixed bug for handling any arbitrary number of input parameters.
parent
921788db
No related branches found
No related tags found
No related merge requests found
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
src/funcheck/scalacheck/ForAllTransformer.scala
+64
-67
64 additions, 67 deletions
src/funcheck/scalacheck/ForAllTransformer.scala
with
64 additions
and
67 deletions
src/funcheck/scalacheck/ForAllTransformer.scala
+
64
−
67
View file @
a50cf05c
...
@@ -33,101 +33,98 @@ trait ForAllTransformer extends TypingTransformers
...
@@ -33,101 +33,98 @@ trait ForAllTransformer extends TypingTransformers
// println(lhs.symbol + " and "+lhs.symbol.tpe)
// println(lhs.symbol + " and "+lhs.symbol.tpe)
// tree
// tree
case
Apply
(
TypeApply
(
s
:
Select
,
partpes
),
rhs
@
List
(
f
@
Function
(
vparams
,
body
)))
if
isForall
(
s
)
=>
case
Apply
(
TypeApply
(
s
:
Select
,
_
),
rhs
@
List
(
f
@
Function
(
vparams
,
body
)))
if
isForall
(
s
)
=>
atOwner
(
currentOwner
)
{
atOwner
(
currentOwner
)
{
assert
(
vparams
.
size
==
1
,
"funcheck.Specs.forAll properties are expected to take a single (tuple) parameter"
)
assert
(
vparams
.
size
==
1
,
"funcheck.Specs.forAll properties are expected to take a single (tuple) parameter"
)
val
v
@
ValDef
(
mods
,
name
,
vtpt
,
vinit
)
=
vparams
.
head
val
v
@
ValDef
(
mods
,
name
,
vtpt
,
vinit
)
=
vparams
.
head
partpes
.
head
.
tpe
match
{
vtpt
.
tpe
match
{
case
tpe
@
TypeRef
(
_
,
_
,
p
tpes
)
=>
case
tpe
@
TypeRef
(
_
,
value
,
v
tpes
)
=>
v
tpt
.
tpe
match
{
v
ar
fun
:
Function
=
{
case
TypeRef
(
_
,
value
,
vtpes
)
=>
if
(
vtpes
.
size
<=
1
)
{
var
fun
:
Function
=
{
f
if
(
vtpes
.
size
<=
1
)
{
}
else
{
f
// create a fresh name for each parameter declared parametric type
}
else
{
val
freshNames
=
vtpes
.
map
(
i
=>
fresh
.
newName
(
"v"
))
// create a fresh name for each parameter declared parametric type
val
funSym
=
tree
.
symbol
val
freshNames
=
vtpes
.
map
(
i
=>
fresh
.
newName
(
"v"
))
val
funSym
=
tree
.
symbol
val
subst
=
for
{
i
<-
0
to
vtpes
.
size
-
1
}
yield
{
val
toSym
=
funSym
.
newValueParameter
(
funSym
.
pos
,
freshNames
(
i
)).
setInfo
(
vtpes
(
i
))
val
subst
=
for
{
i
<-
0
to
vtpes
.
size
-
1
}
yield
{
val
toSym
=
funSym
.
newValueParameter
(
funSym
.
pos
,
freshNames
(
i
)).
setInfo
(
vtpes
(
i
))
val
from
=
Select
(
v
,
v
.
symbol
.
tpe
.
decl
(
"_"
+(
i
+
1
)))
val
from
=
Select
(
v
,
v
.
symbol
.
tpe
.
decl
(
"_"
+(
i
+
1
)))
val
to
=
ValDef
(
toSym
,
EmptyTree
)
setPos
(
tree
.
pos
)
val
to
=
ValDef
(
toSym
,
EmptyTree
)
setPos
(
tree
.
pos
)
(
from
,
to
)
(
from
,
to
)
}
}
val
valdefs
=
subst
.
map
(
_
.
_2
).
toList
val
valdefs
=
subst
.
map
(
_
.
_2
).
toList
val
fun
=
localTyper
.
typed
{
val
fun
=
localTyper
.
typed
{
val
newBody
=
new
MyTreeSubstituter
(
subst
.
map
(
p
=>
p
.
_1
.
symbol
).
toList
,
valdefs
.
map
(
v
=>
Ident
(
v
.
symbol
)).
toList
).
transform
(
resetAttrs
(
body
))
val
newBody
=
new
MyTreeSubstituter
(
subst
.
map
(
p
=>
p
.
_1
.
symbol
).
toList
,
valdefs
.
map
(
v
=>
Ident
(
v
.
symbol
)).
toList
).
transform
(
resetAttrs
(
body
))
Function
(
valdefs
,
newBody
)
Function
(
valdefs
,
newBody
)
}.
asInstanceOf
[
Function
]
}.
asInstanceOf
[
Function
]
new
ChangeOwnerTraverser
(
funSym
,
fun
.
symbol
).
traverse
(
fun
);
new
ChangeOwnerTraverser
(
funSym
,
fun
.
symbol
).
traverse
(
fun
);
new
ForeachTreeTraverser
({
t
:
Tree
=>
t
setPos
tree
.
pos
}).
traverse
(
fun
)
new
ForeachTreeTraverser
({
t
:
Tree
=>
t
setPos
tree
.
pos
}).
traverse
(
fun
)
fun
fun
}
}
}
}
val
prop
=
Prop
.
forAll
(
List
(
fun
))
val
prop
=
Prop
.
forAll
(
List
(
fun
))
var
buf
=
new
collection
.
mutable
.
ListBuffer
[
Tree
]()
var
buf
=
new
collection
.
mutable
.
ListBuffer
[
Tree
]()
val
blockValSym
=
newSyntheticValueParam
(
fun
.
symbol
,
definitions
.
BooleanClass
.
typeConstructor
)
val
blockValSym
=
newSyntheticValueParam
(
fun
.
symbol
,
definitions
.
BooleanClass
.
typeConstructor
)
val
fun2
=
localTyper
.
typed
{
val
fun2
=
localTyper
.
typed
{
val
body
=
Prop
.
propBoolean
(
resetAttrs
(
Ident
(
blockValSym
)))
val
body
=
Prop
.
propBoolean
(
resetAttrs
(
Ident
(
blockValSym
)))
Function
(
List
(
ValDef
(
blockValSym
,
EmptyTree
)),
body
)
Function
(
List
(
ValDef
(
blockValSym
,
EmptyTree
)),
body
)
}.
asInstanceOf
[
Function
]
}.
asInstanceOf
[
Function
]
new
ChangeOwnerTraverser
(
fun
.
symbol
,
fun2
.
symbol
).
traverse
(
fun2
);
new
ChangeOwnerTraverser
(
fun
.
symbol
,
fun2
.
symbol
).
traverse
(
fun2
);
new
ForeachTreeTraverser
({
t
:
Tree
=>
t
setPos
tree
.
pos
}).
traverse
(
fun2
)
new
ForeachTreeTraverser
({
t
:
Tree
=>
t
setPos
tree
.
pos
}).
traverse
(
fun2
)
buf
+=
Block
(
Nil
,
fun2
)
buf
+=
Block
(
Nil
,
fun2
)
if
(
vtpes
.
isEmpty
)
{
buf
+=
resetAttrs
(
Arbitrary
.
arbitrary
(
value
.
tpe
))
if
(
vtpes
.
size
<=
1
)
{
buf
+=
resetAttrs
(
Shrink
.
shrinker
(
value
.
tpe
))
buf
+=
resetAttrs
(
Arbitrary
.
arbitrary
(
tpe
))
}
else
{
buf
+=
resetAttrs
(
Shrink
.
shrinker
(
tpe
))
for
{
tpe
<-
vtpes
}
{
}
else
{
buf
+=
resetAttrs
(
Arbitrary
.
arbitrary
(
tpe
))
for
{
tpe
<-
vtpes
}
{
buf
+=
resetAttrs
(
Shrink
.
shrinker
(
tpe
))
buf
+=
resetAttrs
(
Arbitrary
.
arbitrary
(
tpe
))
}
buf
+=
resetAttrs
(
Shrink
.
shrinker
(
tpe
))
}
}
}
import
posAssigner.atPos
// for filling in tree positions
import
posAssigner.atPos
// for filling in tree positions
val
property
=
localTyper
.
typed
{
val
property
=
localTyper
.
typed
{
atPos
(
tree
.
pos
)
{
atPos
(
tree
.
pos
)
{
Apply
(
prop
,
buf
.
toList
)
Apply
(
prop
,
buf
.
toList
)
}
}
}
}
localTyper
.
typed
{
localTyper
.
typed
{
atPos
(
tree
.
pos
)
{
atPos
(
tree
.
pos
)
{
ConsoleReporter
.
testStatsEx
(
Test
.
check
(
property
))
ConsoleReporter
.
testStatsEx
(
Test
.
check
(
property
))
}
}
case
t
=>
assert
(
false
,
"expected ValDef of type TypeRef, found "
+
t
)
tree
}
}
}
case
t
=>
tree
}
case
t
=>
assert
(
false
,
"expected ValDef of type TypeRef, found "
+
t
)
tree
}
}
}
/** Delegates the recursive traversal of the tree. */
/** Delegates the recursive traversal of the tree. */
case
_
=>
super
.
transform
(
tree
)
case
_
=>
super
.
transform
(
tree
)
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment