index
:
aeneas
isabelle
aeneas rust verifier with a hacky Isabelle backend
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
src
/
PureMicroPasses.ml
(
follow
)
Commit message (
Collapse
)
Author
Age
Files
Lines
*
Finish implementing to_monadic
Son Ho
2022-01-28
1
-13
/
+41
|
*
Add a comment
Son Ho
2022-01-28
1
-0
/
+1
|
*
Implement get_expression_min_var_counter
Son Ho
2022-01-28
1
-3
/
+16
|
*
Start working on to_monadic and make the expression visitors an
Son Ho
2022-01-28
1
-7
/
+45
|
|
|
|
extension of the typed_lvalue visitors
*
Remove the Return and Fail variants from Pure.expression and add a
Son Ho
2022-01-28
1
-10
/
+10
|
|
|
|
`monadic` boolean field to `Let`
*
Change the type of [Pure.call.args] to [expression list] rather than
Son Ho
2022-01-28
1
-8
/
+5
|
|
|
|
[typed_rvalue list]
*
Make minor modifications
Son Ho
2022-01-28
1
-1
/
+8
|
*
Simplify the let-bindings in the pure AST
Son Ho
2022-01-28
1
-18
/
+23
|
*
Make substantial simplifications to the pure AST
Son Ho
2022-01-28
1
-76
/
+54
|
*
Make minor modifications
Son Ho
2022-01-28
1
-29
/
+31
|
*
Apply the micro-passes to the pure ASTs
Son Ho
2022-01-28
1
-0
/
+16
|
*
Make a lot of small modifications
Son Ho
2022-01-28
1
-0
/
+20
|
*
Finish the function PureMicroPasses.compute_pretty_names
Son Ho
2022-01-28
1
-2
/
+14
|
*
Make more progress on PureMicroPasses
Son Ho
2022-01-28
1
-14
/
+65
|
*
Make good progress on PureMicroPasses.compute_pretty_names
Son Ho
2022-01-28
1
-3
/
+140
|
*
Implement visitors for Pure.expression and make minor modifications
Son Ho
2022-01-28
1
-17
/
+54
|
*
Rename the meta-places to [mplace] and update some comments
Son Ho
2022-01-27
1
-2
/
+21
|
*
Make minor modifications and create PureMicroPasses.ml
Son Ho
2022-01-27
1
-0
/
+43