Skip to main content
Homepage
Explore
Search or go to…
/
Register
Sign in
Explore
Primary navigation
Project
W
why3
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
Model registry
Operate
Environments
Monitor
Incidents
Analyze
Value stream analytics
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
GitLab community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Collapse sidebar
Snippets
Groups
Projects
Show more breadcrumbs
Nils Fitinghoff
why3
Commits
780895af
Commit
780895af
authored
Nov 15, 2018
by
nilfit
Browse files
Options
Downloads
Patches
Plain Diff
remove option from Econst string option
There is no case that leads to None
parent
8b8b8663
No related branches found
No related tags found
No related merge requests found
Changes
1
Show whitespace changes
Inline
Side-by-side
Showing
1 changed file
src/mlw/rust_printer.ml
+3
-7
3 additions, 7 deletions
src/mlw/rust_printer.ml
with
3 additions
and
7 deletions
src/mlw/rust_printer.ml
+
3
−
7
View file @
780895af
...
...
@@ -43,7 +43,7 @@ module Rust = struct
type
fn
=
rsymbol
*
var
list
*
ty
*
expr
*
Stv
.
t
*
Slt
.
t
and
expr
=
|
Econst
of
string
option
*
BigInt
.
t
|
Econst
of
string
*
BigInt
.
t
|
Evar
of
ident
|
Efield
of
expr
*
ident
|
Eassign
of
pvsymbol
*
rsymbol
*
expr
...
...
@@ -322,8 +322,7 @@ module Translate = struct
|
I
{
ity_node
=
Ityapp
({
its_ts
=
ts
}
,_,_
)
}
->
ts
.
ts_name
|
_
->
assert
false
in
(
match
query_syntax
info
.
literal
id
with
|
Some
s
->
Rust
.
Econst
(
Some
s
,
n
)
(* TODO there can never be an Econst (None, ..), the option is not needed *)
|
Some
s
->
Rust
.
Econst
(
s
,
n
)
|
None
->
raise
(
MissingSyntaxLiteral
id
.
id_string
))
(* there is no default, driver must make a decision about how to represent
literals *)
...
...
@@ -949,10 +948,7 @@ module Print = struct
let
rec
print_expr
info
fmt
(
e
:
expr
)
=
match
e
with
|
Econst
(
s_opt
,
n
)
->
(
match
s_opt
with
|
Some
s
->
syntax_arguments
s
print_constant
fmt
[
n
]
|
None
->
raise
(
TODO
"const no syntax"
))
|
Econst
(
s
,
n
)
->
syntax_arguments
s
print_constant
fmt
[
n
]
|
Evar
id
->
print_lident
info
fmt
id
|
Efield
(
e
,
id
)
->
fprintf
fmt
"%a.%a"
(
print_expr
info
)
e
(
print_lident
info
)
id
...
...
...
...
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