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
3b63c054
Commit
3b63c054
authored
9 years ago
by
Mikaël Mayer
Browse files
Options
Downloads
Patches
Plain Diff
SelfPrettyPrinter can now return functions with free variables.
parent
65b760e9
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/main/scala/leon/purescala/SelfPrettyPrinter.scala
+102
-37
102 additions, 37 deletions
src/main/scala/leon/purescala/SelfPrettyPrinter.scala
with
102 additions
and
37 deletions
src/main/scala/leon/purescala/SelfPrettyPrinter.scala
+
102
−
37
View file @
3b63c054
...
@@ -33,64 +33,129 @@ object SelfPrettyPrinter {
...
@@ -33,64 +33,129 @@ object SelfPrettyPrinter {
}
}
}
}
/** This pretty-printer uses functions defined in Leon itself.
/** T is the type of pretty-printers which have to be found (e.g. Lambda or Lambdas with identifiers)
* If not pretty printing function is defined, return the default value instead
* U is the type of the arguments during gathering */
*/
trait
PrettyPrinterFinder
[
T
,
U
>:
T
]
{
class
SelfPrettyPrinter
{
protected
def
isExcluded
(
fd
:
FunDef
)
:
Boolean
implicit
val
section
=
leon
.
utils
.
DebugSectionEvaluation
protected
def
isAllowed
(
fd
:
FunDef
)
:
Boolean
private
var
allowedFunctions
=
Set
[
FunDef
]()
private
var
excluded
=
Set
[
FunDef
]()
/** Functions whose name does not need to end with `tostring` or which can be abstract, i.e. which may contain a choose construct.*/
def
allowFunction
(
fd
:
FunDef
)
=
{
allowedFunctions
+=
fd
;
this
}
def
excludeFunctions
(
fds
:
Set
[
FunDef
])
=
{
excluded
++=
fds
;
this
}
@inline
def
isValidPrinterName
(
s
:
String
)
=
{
val
n
=
s
.
toLowerCase
();
n
.
endsWith
(
"tostring"
)
||
n
.
endsWith
(
"mkstring"
)
}
def
excludeFunction
(
fd
:
FunDef
)
=
{
excluded
+=
fd
;
this
}
@inline
def
isCandidate
(
fd
:
FunDef
)
=
fd
.
returnType
==
StringType
&&
fd
.
params
.
nonEmpty
&&
!
isExcluded
(
fd
)
&&
(
isAllowed
(
fd
)
||
isValidPrinterName
(
fd
.
id
.
name
))
/** Returns a list of possible lambdas that can transform the input type to a String.
/** Returns a list of possible lambdas that can transform the input type to a String.
* At this point, it does not consider yet the inputType. Only [[prettyPrinterFromCandidate]] will consider it. */
* At this point, it does not consider yet the inputType. Only [[prettyPrinterFromCandidate]] will consider it. */
def
prettyPrintersForType
(
inputType
:
TypeTree/*
,
existingPp
:
Map
[
TypeTree
,
List
[
Lambda
]]
=
Map
()*/)(
implicit
ctx
:
LeonContext
,
program
:
Program
)
:
Stream
[
Lambda
]
=
{
def
prettyPrintersForType
(
inputType
:
TypeTree/*
,
existingPp
:
Map
[
TypeTree
,
List
[
Lambda
]]
=
Map
()*/)(
implicit
ctx
:
LeonContext
,
program
:
Program
)
:
Stream
[
T
]
=
{
program
.
definedFunctions
.
toStream
flatMap
{
fd
=>
program
.
definedFunctions
.
toStream
flatMap
{
fd
=>
val
isCandidate
=
if
(
isCandidate
(
fd
))
prettyPrinterFromCandidate
(
fd
,
inputType
)
else
Stream
.
Empty
fd
.
returnType
==
StringType
&&
fd
.
params
.
nonEmpty
&&
!
excluded
(
fd
)
&&
(
allowedFunctions
(
fd
)
||
fd
.
id
.
name
.
toLowerCase
().
endsWith
(
"tostring"
))
if
(
isCandidate
)
{
prettyPrinterFromCandidate
(
fd
,
inputType
)
}
else
{
Stream
.
Empty
}
}
}
}
}
def
getPrintersForType
(
t
:
TypeTree
)(
implicit
ctx
:
LeonContext
,
program
:
Program
)
:
Option
[
Stream
[
U
]]
=
t
match
{
case
FunctionType
(
Seq
(
in
),
StringType
)
=>
// Should have one argument.
Some
(
prettyPrintersForType
(
in
))
case
_
=>
None
}
// To Implement
def
buildLambda
(
inputType
:
TypeTree
,
fd
:
FunDef
,
slu
:
Stream
[
List
[
U
]])
:
Stream
[
T
]
def
prettyPrinterFromCandidate
(
fd
:
FunDef
,
inputType
:
TypeTree
)(
implicit
ctx
:
LeonContext
,
program
:
Program
)
:
Stream
[
Lambda
]
=
{
def
prettyPrinterFromCandidate
(
fd
:
FunDef
,
inputType
:
TypeTree
)(
implicit
ctx
:
LeonContext
,
program
:
Program
)
:
Stream
[
T
]
=
{
println
(
"Considering pretty printer "
+
fd
.
id
.
name
+
" with arg "
+
fd
.
params
.
head
.
getType
+
" for type "
+
inputType
)
TypeOps
.
canBeSubtypeOf
(
inputType
,
fd
.
tparams
.
map
(
_
.
tp
),
fd
.
params
.
head
.
getType
)
match
{
TypeOps
.
canBeSubtypeOf
(
inputType
,
fd
.
tparams
.
map
(
_
.
tp
),
fd
.
params
.
head
.
getType
)
match
{
case
Some
(
genericTypeMap
)
=>
case
Some
(
genericTypeMap
)
=>
println
(
"Found a mapping"
)
val
defGenericTypeMap
=
genericTypeMap
.
map
{
case
(
k
,
v
)
=>
(
Definitions
.
TypeParameterDef
(
k
),
v
)
}
val
defGenericTypeMap
=
genericTypeMap
.
map
{
case
(
k
,
v
)
=>
(
Definitions
.
TypeParameterDef
(
k
),
v
)
}
def
gatherPrettyPrinters
(
funIds
:
List
[
Identifier
],
acc
:
ListBuffer
[
Stream
[
Lambda
]]
=
ListBuffer
())
:
Option
[
Stream
[
List
[
Lambda
]]]
=
funIds
match
{
def
gatherPrettyPrinters
(
funIds
:
List
[
Identifier
],
acc
:
ListBuffer
[
Stream
[
U
]]
=
ListBuffer
[
Stream
[
U
]]
())
:
Option
[
Stream
[
List
[
U
]]]
=
funIds
match
{
case
Nil
=>
Some
(
StreamUtils
.
cartesianProduct
(
acc
.
toList
))
case
Nil
=>
Some
(
StreamUtils
.
cartesianProduct
(
acc
.
toList
))
case
funId
::
tail
=>
// For each function, find an expression which could be provided if it exists.
case
funId
::
tail
=>
// For each function, find an expression which could be provided if it exists.
funId
.
getType
match
{
getPrintersForType
(
funId
.
getType
)
match
{
case
FunctionType
(
Seq
(
in
),
StringType
)
=>
// Should have one argument.
case
Some
(
u
)
=>
gatherPrettyPrinters
(
tail
,
acc
+=
u
)
val
candidates
=
prettyPrintersForType
(
in
)
case
None
=>
gatherPrettyPrinters
(
tail
,
acc
+=
candidates
)
println
(
"could not finish"
)
case
_
=>
None
None
}
}
}
}
val
funIds
=
fd
.
params
.
tail
.
map
(
x
=>
TypeOps
.
instantiateType
(
x
.
id
,
defGenericTypeMap
)).
toList
val
funIds
=
fd
.
params
.
tail
.
map
(
x
=>
TypeOps
.
instantiateType
(
x
.
id
,
defGenericTypeMap
)).
toList
gatherPrettyPrinters
(
funIds
)
match
{
gatherPrettyPrinters
(
funIds
)
match
{
case
Some
(
l
)
=>
for
(
lambdas
<-
l
)
yield
{
case
Some
(
l
)
=>
buildLambda
(
inputType
,
fd
,
l
)
val
x
=
FreshIdentifier
(
"x"
,
inputType
)
// verify the type
case
None
=>
Stream
.
empty
Lambda
(
Seq
(
ValDef
(
x
)),
functionInvocation
(
fd
,
Variable
(
x
)::
lambdas
))
}
case
_
=>
Stream
.
empty
}
}
case
None
=>
Stream
.
empty
case
None
=>
Stream
.
empty
}
}
}
}
}
/** This pretty-printer uses functions defined in Leon itself.
* If not pretty printing function is defined, return the default value instead
*/
class
SelfPrettyPrinter
extends
PrettyPrinterFinder
[
Lambda
,
Lambda
]
{
top
=>
implicit
val
section
=
leon
.
utils
.
DebugSectionEvaluation
/* Functions whose name does not need to end with `tostring` or which can be abstract, i.e. which may contain a choose construct.*/
protected
var
allowedFunctions
=
Set
[
FunDef
]()
/* Functions totally excluded from the set of pretty-printer candidates */
protected
var
excluded
=
Set
[
FunDef
]()
/** Functions whose name does not need to end with `tostring` or which can be abstract, i.e. which may contain a choose construct.*/
def
allowFunction
(
fd
:
FunDef
)
=
{
allowedFunctions
+=
fd
;
this
}
/** Functions totally excluded from the set of pretty-printer candidates*/
def
excludeFunctions
(
fds
:
Set
[
FunDef
])
=
{
excluded
++=
fds
;
this
}
/** Function totally excluded from the set of pretty-printer candidates*/
def
excludeFunction
(
fd
:
FunDef
)
=
{
excluded
+=
fd
;
this
}
protected
def
isExcluded
(
fd
:
FunDef
)
:
Boolean
=
top
.
excluded
(
fd
)
protected
def
isAllowed
(
fd
:
FunDef
)
:
Boolean
=
top
.
allowedFunctions
(
fd
)
override
def
getPrintersForType
(
t
:
TypeTree
)(
implicit
ctx
:
LeonContext
,
program
:
Program
)
:
Option
[
Stream
[
Lambda
]]
=
t
match
{
case
FunctionType
(
Seq
(
StringType
),
StringType
)
=>
// Should have one argument.
val
s
=
FreshIdentifier
(
"s"
,
StringType
)
// verify the type
Some
(
Stream
(
Lambda
(
Seq
(
ValDef
(
s
)),
Variable
(
s
)))
++
super
.
getPrintersForType
(
t
).
getOrElse
(
Stream
.
empty
)
)
case
_
=>
super
.
getPrintersForType
(
t
)
}
/** From a list of lambdas used for pretty-printing the arguments of a function, builds the lambda for the function itself. */
def
buildLambda
(
inputType
:
TypeTree
,
fd
:
FunDef
,
slu
:
Stream
[
List
[
Lambda
]])
:
Stream
[
Lambda
]
=
{
for
(
lambdas
<-
slu
)
yield
{
val
x
=
FreshIdentifier
(
"x"
,
inputType
)
// verify the type
Lambda
(
Seq
(
ValDef
(
x
)),
functionInvocation
(
fd
,
Variable
(
x
)::
lambdas
))
}
}
object
withPossibleParameters
extends
PrettyPrinterFinder
[(
Lambda
,
List
[
Identifier
])
,
(
Expr
,
List
[
Identifier
])]
{
protected
def
isExcluded
(
fd
:
FunDef
)
:
Boolean
=
top
.
excluded
(
fd
)
protected
def
isAllowed
(
fd
:
FunDef
)
:
Boolean
=
top
.
allowedFunctions
(
fd
)
/** If the returned identifiers are instantiated, each lambda becomes a pretty-printer.
* This allows to make use of mkString functions such as for maps */
def
prettyPrintersForTypes
(
inputType
:
TypeTree
)(
implicit
ctx
:
LeonContext
,
program
:
Program
)
=
{
program
.
definedFunctions
.
toStream
flatMap
{
fd
=>
if
(
isCandidate
(
fd
))
prettyPrinterFromCandidate
(
fd
,
inputType
)
else
Stream
.
Empty
}
}
/** Adds the possibility to have holes in expression */
override
def
getPrintersForType
(
t
:
TypeTree
)(
implicit
ctx
:
LeonContext
,
program
:
Program
)
=
t
match
{
case
FunctionType
(
Seq
(
StringType
),
StringType
)
=>
// Should have one argument.
val
s
=
FreshIdentifier
(
"s"
,
StringType
)
// verify the type
Some
(
Stream
((
Lambda
(
Seq
(
ValDef
(
s
)),
Variable
(
s
)),
List
()))
++
super
.
getPrintersForType
(
t
).
getOrElse
(
Stream
.
empty
)
)
case
StringType
=>
val
const
=
FreshIdentifier
(
"const"
,
StringType
)
Some
(
Stream
((
Variable
(
const
),
List
(
const
))))
case
_
=>
super
.
getPrintersForType
(
t
)
}
/** From a list of expressions gathered for the parameters of the function definition, builds the lambda. */
def
buildLambda
(
inputType
:
TypeTree
,
fd
:
FunDef
,
slu
:
Stream
[
List
[(
Expr
,
List
[
Identifier
])]])
=
{
for
(
lambdas
<-
slu
)
yield
{
val
(
args
,
ids
)
=
lambdas
.
unzip
val
all_ids
=
ids
.
flatten
val
x
=
FreshIdentifier
(
"x"
,
inputType
)
// verify the type
(
Lambda
(
Seq
(
ValDef
(
x
)),
functionInvocation
(
fd
,
Variable
(
x
)::
args
)),
all_ids
)
}
}
}
/** Actually prints the expression with as alternative the given orElse
/** Actually prints the expression with as alternative the given orElse
* @param excluded The list of functions which should be excluded from pretty-printing
* @param excluded The list of functions which should be excluded from pretty-printing
...
...
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