Port of the Objective Caml code supporting John Harrison's logic textbook Handbook of Practical Logic and Automated Reasoning to Scala.
scala-atp is an EDLA project.
The purpose of edla.org is to promote the state of the art in various domains.
F# : complete and 'official'
SML: almost complete and 'official'
Haskell : complete and published
OCaml : original code for Ocam 3 adapted to fit OCaml 4
Haskell : complete, original code for GHC 6.10.4 adapted to fit GHC 8.x
Haskell : almost complete
JavaScript : almost complete (generated with GHCJS compiler)
scala : uncomplete (chap 1 & 2)
Haskell : uncomplete (chap 1)
Haskell : uncomplete
Rust : uncomplete
Swift : uncomplete
Running examples with Jupyter notebook
All examples will be available in the notebooks directory
This is a very convenient way to play with Scala
You need first to publish scala-atp locally :
git clone https://github.com/newca12/scala-atp.git
cd scala-atp
sbt publishLocal
Follow instructions here to install a scala kernel for Jupyter.
To run the notebook, run the following command at the Terminal
jupyter-notebook
We kept the file names of the original mostly intact, though use Scala naming conventions.
This project contain also a study about parsers and some code from :
- DSLs in Action from Debasish Ghosh
- Eugen Labun's thesis : Combinator Parsing in Scala
© 2003-2007, John Harrison.
© 2012-2019, Olivier ROLAND.
(See "LICENSE.txt" for details.)