Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Implement Full Alive Translation #126

Merged
merged 12 commits into from
Nov 1, 2023
Merged

Implement Full Alive Translation #126

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
a8da70a
wip: implement alive translation
bollu Oct 30, 2023
1c50181
add simp lemma for -1
bollu Oct 30, 2023
7b8c209
haven't seen this one before: failed to compile pattern match
bollu Oct 30, 2023
a6ada9e
add support for icmp.*
bollu Oct 31, 2023
d351e38
toString instances
bollu Oct 31, 2023
ff38eed
TODO: we should delete mkOpExpr, and add special handlers for each of…
bollu Oct 31, 2023
88d3ef6
add support for copy, select
bollu Nov 1, 2023
4238f6f
feat: add working version of AliveAutoGenerated, with code that doesn…
bollu Nov 1, 2023
3a97602
fix: add proof of bitvec fact
bollu Nov 1, 2023
c8a2d7d
fixup diff nits
bollu Nov 1, 2023
7b42b46
add new alive commit
bollu Nov 1, 2023
fd083a3
remove 'dsimp' as it was causing the proof state to explode
bollu Nov 1, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 5 additions & 1 deletion SSA/Core/Util/ConcreteOrMVar.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,10 @@ inductive ConcreteOrMVar (α : Type u) (φ : Nat)
| mvar (i : Fin φ)
deriving DecidableEq, Repr, Inhabited

instance [ToString α] : ToString (ConcreteOrMVar α n) where
toString
| .concrete a => s!"concrete({a})"
| .mvar i => s!"mvar({i})"
/-- A coercion from the concrete type `α` to the `ConcreteOrMVar` -/
instance : Coe α (ConcreteOrMVar α φ) := ⟨.concrete⟩

Expand Down Expand Up @@ -42,4 +46,4 @@ def instantiate (as : Vector α φ) : ConcreteOrMVar α φ → α
| .mvar i => as.get i


end ConcreteOrMVar
end ConcreteOrMVar
7 changes: 5 additions & 2 deletions SSA/Projects/InstCombine/Alive.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,8 +1,11 @@

-- Auto generated alive statements
import SSA.Projects.InstCombine.AliveAutoGenerated
-- Do not import these into the default tree, because they take a long
-- time to elaborate and typecheck.
-- import SSA.Projects.InstCombine.AliveAutoGenerated

-- Pure math statements needed to proof alive statements
-- Pure math statements needed to prove alive statements.
-- Include these, as they are reasonably fast to typecheck.
import SSA.Projects.InstCombine.AliveStatements

-- The semantics for the MLIR base dialect
Expand Down
Loading