From ae60d2bf48d1eee6e68157ae96f02c04532ba007 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 19 Mar 2018 18:42:34 -0700 Subject: [PATCH] doc(tmp/lean4): add SSA/SIL remark --- tmp/lean4.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/tmp/lean4.md b/tmp/lean4.md index 04e32abdb4..34fde43ace 100644 --- a/tmp/lean4.md +++ b/tmp/lean4.md @@ -303,6 +303,10 @@ operation needed to retrieve them. We will use this table when converting the Sy representation into the IR. Open issue: should we use SSA or SIL? +BTW, most of the benefits of SSA/SIL seem to be irrelevant for Lean. +The paper https://arxiv.org/pdf/1507.05762.pdf send by Nuno describes the pros/cons for SSA. +Most of them seem to be related to static analysis procedures. I think we will need very few +static analysis steps, most optimizations will be implemented at System-F before we convert the code into IR. # VM