dune

(library
 (name isla_lang)
 (public_name isla-lang)
 (flags (:standard -warn-error -A -w -27 -w -26))
 (modules (:standard \ main))
 (synopsis "A Ocaml library to parse print and manipulate trace from the isla symbolic evaluator")
 (libraries pprint))

(executable
 (package isla-lang)
 (name main)
 (public_name isla-lang)
 (flags (:standard -warn-error -A -w -27 -w -26))
 (modules main)
 (libraries pprint isla_lang))

(coq.theory
 (name isla_lang)
 (package coq-isla-lang)
 (modules lang traces litmus)
 (synopsis "A Coq library to manipulate traces from the isla symbolic evaluator"))

(rule
 (targets isla_lang_parser.mly isla_lang_parser_pp.ml isla_lang_lexer.mll
   isla_lang_ast.ml isla_lang.v)
 (deps isla_lang.ott fix-substs.sed)
 (action
  (progn
   (run ott -show_sort false -quotient_rules false -aux_style_rules false -i
     isla_lang.ott -o isla_lang_parser.mly -o isla_lang_lexer.mll -o
     isla_lang_ast.ml -o isla_lang.v)
   (run sed -i.bak -f fix-substs.sed isla_lang_ast.ml isla_lang.v))))

(rule
 (target ott.path)
 (action (with-stdout-to %{target} (system "opam var ott:share"))))

(rule
 (target ottlib.mly)
 (action (copy "%{read-lines:ott.path}/menhir_library_extra.mly" %{target})))

(menhir
 (modules isla_lang_parser ottlib)
 (merge_into isla_lang_parser)
 (infer true))

(ocamllex
 (modules isla_lang_lexer))

(rule
 (target isla_lang_quotiented_generated.tex)
 (deps isla_lang.ott)
 (action (run ott -quotient_rules true -i %{deps} -o %{target})))

(rule
 (target isla_lang_quotiented_generated.pdf)
 (deps isla_lang_quotiented_generated.tex)
 (action (ignore-stdout (run pdflatex %{deps}))))

(rule
 (target isla_lang_quotiented.pdf)
 (deps doc/isla_lang_quotiented.pdf)
 (action (copy %{deps} %{target})))

(rule
 (target isla_lang_unquotiented_generated.tex)
 (deps isla_lang.ott)
 (action (run ott -quotient_rules false -i %{deps} -o %{target})))

(rule
 (target isla_lang_unquotiented_generated.pdf)
 (deps isla_lang_unquotiented_generated.tex)
 (action (ignore-stdout (run pdflatex %{deps}))))

(rule
 (target isla_lang_unquotiented.pdf)
 (deps doc/isla_lang_unquotiented.pdf)
 (action (copy %{deps} %{target})))

(install
 (package isla-lang)
 (files isla_lang.ott)
 (section share))

(install
 (package isla-lang)
 (files isla_lang_unquotiented.pdf isla_lang_quotiented.pdf)
 (section doc))

(rule
 (target lang.v)
 (deps isla_lang.v)
 (action
  (with-stdout-to %{target}
   (system "sed '2,/(\\*REAL_START\\*)/d' %{deps}"))))

; TODO remove this when Islaris depends on coq-isla-lang
(install
 (package isla-lang)
 (files (lang.v as isla_lang.v))
 (section share))