Leonardo de Moura
84bcc4445a
feat(library/init/compiler/ir): missing phi node validation
2018-04-25 17:12:44 -07:00
Leonardo de Moura
4bf97be30a
chore(library/init/compiler/ir): cleanup
2018-04-24 13:00:39 -07:00
Leonardo de Moura
1fd399d06f
feat(library/init/compiler/ir): use run_state and run_reader
2018-04-24 12:48:12 -07:00
Leonardo de Moura
c0d782ce3c
feat(library/init/compiler/ir): we don't need collector
2018-04-23 08:56:22 -07:00
Leonardo de Moura
563c9fce4e
fix(library/init/compiler/ir): SSA validator
...
TODO: check whether the assumptions made here match LLVM IR semantics
2018-04-20 18:27:13 -07:00
Leonardo de Moura
3eeb337423
fix(library/init/compiler/ir): phi instructions must only occur in the beggining of the block
2018-04-20 18:27:13 -07:00
Leonardo de Moura
b35be8e6b7
feat(library/init/compiler/ir): simplify phi instruction
...
The blockid is only needed by LLVM, and we can infer this information
when mapping to LLVM.
2018-04-20 18:27:13 -07:00
Leonardo de Moura
29ee8493c0
feat(library/init/compiler/ir): blockid validator
2018-04-20 18:27:13 -07:00
Leonardo de Moura
ba9782bc5a
feat(library/init/compiler/ir): collect used variables
2018-04-20 18:27:13 -07:00
Leonardo de Moura
7260ac91ed
feat(library/init/compiler/ir): declare new IR in Lean
...
Next steps:
- Implement more validators (e.g., blockid validator, type checker).
- Implement C++ code generator (in Lean). We can use it for testing the new
lean_obj module implemented in C++.
- Implement interpreter (in C++) for sanity checking.
- Implement LLVM IR generator (in Lean). It just outputs a text file using LLVM
syntax. After, we are confident we are generating valid LLVM IR, we
can try to link LLVM with Lean.
2018-04-20 18:27:13 -07:00
