Commit c71d0241 authored by charguer's avatar charguer

docgen

parent 87e1c36f
see if we can get rid of make_cmj
xwhile: error reporting when arguments don't have the right types.
notation "# H" uniquement lorsque H est au type hprop.
......
......@@ -21,4 +21,11 @@ clean:
# TODO: understand if myocamldeb is needed or not.
\ No newline at end of file
# TODO: understand if myocamldeb is needed or not.
doc: README.html
README.html: README.md
pandoc -o $@ $<
#####################################################################
# Binaries
`main`
: for building `*_ml.v` files from `*.ml` files. The `*_ml.v` files contain the characteristic formulae.
`makecmj`
: for building `*.cmj` files from `*.ml` and `*.mli` files, which are like `*.cmi` files, but named differently to avoid conflicts. The `*.cmj` files are required for the separate compilation performed by the `main` tool.
#####################################################################
# Compilation of the binaries
Execute:
```
make
```
#####################################################################
# Options for `main` and `makecmj`
`-I` *folder*
: Add an include directory where to look for `*.cmj` files.
`-rectypes`
: Allow type-checking with recursive types.
`-nostdlib`
: Use this file to compile `*.ml` files from the standard library.
`-nopervasives`
: Use this file to compile Pervasives.ml.
#####################################################################
# Options for `main`
`-o` *FILENAME*
: Set the output file name. By default, `*_ml.v` for `*.ml`
`-rectypes`
: Allow type-checking with recursive types.
`-left2right`
: Assume that side-effects are performed in the left subexpressions first, unlike OCaml's convention.
`-only_normalize`
: Normalize the code, but do not attempt building the characteristic formula file.
`-debug`
: Trace the various steps performed by the tool.
`-width`
: Set the pretty-printing width for the output file.
`-credits`
: [FUTURE USE] Generate characteristic formulae with time credits.
#####################################################################
# Organization of the code
`main.ml`
: Drives the operations.
`renaming.ml`
: Contains the convention for mapping names of variables, types, constructors and modules. It includes the list of builtin types and operators that are treated specially.
`normalize.ml`
: Describes a source-to-source translation at the level of the parse tree. This translation implements a form of A-normalization: it pulls out all side-effectful sub-expressions, and all function definitions, into seperate let bindings. This translation also rejects programs using features that are not supported by CFML.
`formula.ml`
: Describes a data type called `formula`, which serves as an intermediate representation for characteristic formulae before they get dumped as Coq syntax.
`coq.ml`
: Describes a data type called `coq`, which serves as a structured representation for Coq terms.
`characteristic.ml`
: Converts a typed abstract syntax tree into a structure of type `formula`.
`formula_to_coq.ml`
: Converts a structure of type `formula` into a structured `coq` term.
`print_coq.ml`
: Converts a structured `coq` term into a pretty-printed string.
`print_past.ml`
: Prints an AST, obtained from the parser.
`print_tast.ml`
: Prints a typed AST, obtained from type-checker.
#####################################################################
# Debugging
For debugging purposes, when compiling a `*.ml` file, the `main` tool
generates three files:
* `output/*_original.ml`
* `output/*_normalized.ml`
* `output/*_normalized_types.ml`
These files are not in valid syntax, and are not pretty-printed,
but they allow debugging the normalization process.
......@@ -13,7 +13,7 @@ let trace s =
let ppf = Format.std_formatter
let onlycmj = ref false
let only_normalize = ref false
let no_mystd_include = ref false
......@@ -34,7 +34,7 @@ let spec =
("-nostdlib", Arg.Set no_mystd_include, " do not include standard library");
("-nopervasives", Arg.Set Clflags.nopervasives, " do not include standard pervasives file");
("-o", Arg.String (fun s -> outputfile := Some s), " set the output file name");
("-onlycmj", Arg.Set onlycmj, " only generate the .cmj file, not the .v file");
("-only_normalize", Arg.Set only_normalize, " only generate the .cmj file, not the .v file");
("-debug", Arg.Set is_tracing, " trace the various steps");
("-width", Arg.Set_int Print_coq.width, " set pretty-printing width for the .v file");
]
......@@ -121,12 +121,12 @@ let _ =
in
(*---------------------------------------------------*)
trace "5) dumping .cmj file";
trace "5) dumping normalized file";
file_put_contents (debugdirBase ^ "_normalized_typed.ml") (Print_tast.string_of_structure typedtree2);
(* ignore (typedtree2); *)
if !onlycmj then begin
trace "6) exiting since -onlycmj";
if !only_normalize then begin
trace "6) exiting since -only_normalize";
exit 0;
end;
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment