Contenu de ce dossier
---------------------

Les sources OCaml du transformateur PI.

lo.ml : le transformateur proprement dit.
lo_lex.mll : le lexeur (pour OCamlLex).
lo_parse.mly : le parseur (pour OCamlYacc).
lo_print.ml : l'imprimeur des formules Coq et des structures du langage
Lambda-O.
lo_top.ml : l'entrée interactive et la lecture de fichiers source.

Pour produire les fichiers OCaml du parseur et du lexeur :

ocamlyacc lo_parse.mly
ocamllex lo_lex.mll

Puis, pour compiler en natif :

ocamlopt -o pi.opt nums.cmxa lo.ml lo_parse.mli lo_parse.ml lo_lex.ml lo_print.ml lo_top.ml

Ou, pour compiler en bytecode :

ocamlc -o pi nums.cma lo.ml lo_parse.mli lo_parse.ml lo_lex.ml lo_print.ml lo_top.ml