docs/compiler.rst

How To Use The Cogent Compiler
==============================

Command-line Arguments
------------------------------------

The Cogent compiler accepts
a large number of command-line arguments,
which are either *commands*,
directing the compiler to produce particular outputs,
or *flags*,
influencing the compiler's behaviour as it works.

.. comment:

   In typical use,
   only a small number of the commands and flags are used,
   the most common of which
   (and those listed by ``--help`` by default) are:

   --parse  \
       parse Cogent source code
   -t, --typecheck  \
       typecheck surface program
   -d, --desugar  \
       desugar surface program and re-type it
   --normal  \
       normalise core language and re-type it
   --mono  \
       monomorphise core language and re-type it
   -g, --code-gen  \
       generate C code
   --build-info  \
       log how cogent is being invoked by generating BUILD_INFO file;
       implied by any collective commands
   -C, --c-refinement  \
       [COLLECTIVE] generate all files needed for the C refinement proof
   -F, --functional-correctness  \
       [COLLECTIVE] generate all files needed for the functional correctness proof
   -A, --all  \
       [COLLECTIVE] generate everything
   --libgum-dir  \
       display directory where standard gum headers are installed
       (can be set by COGENT_LIBGUM_DIR environment variable)
   -h, --help  \
       display help message;
       optionally including a verbosity from 0 to 4, defaulting to 1
   -v, -V, --version  \
       show the Cogent compiler's version number

   -O LEVEL, --optimisation=LEVEL  \
       set optimisation level (0, 1, 2, d, n, s or u; default -Od)

.. highlight:: bash

A typical invocation might be::

  $ cogent -g -o generated \
           --infer-c-funcs=main.ac \
           --infer-c-types=abstract/Grid.ah \
           mandelbrot.cogent

Commands
^^^^^^^^^^^^^^^^^^^^^^^^

--ast-c  \
    parse C file with Cogent antiquotation and print AST
--stack-usage=FILE  \
    parse a stack usage ``.su`` file generated by gcc; ``FILE`` optional
--parse  \
    parse Cogent source code
-t, --typecheck  \
    typecheck surface program
-d, --desugar  \
    desugar surface program and re-type it
--normal  \
    normalise core language and re-type it
--simplify  \
    simplify core language and re-type it
--mono  \
    monomorphise core language and re-type it
-g, --code-gen  \
    generate C code
--ast-parse  \
    display surface language AST
--ast-tc  \
    display type-checked surface language AST
--ast-desugar  \
    display desugared core language AST
--ast-normal  \
    display normalised core language AST
--ast-simpl  \
    display simplified core language AST
--ast-mono  \
    display monomorphised core language AST
-i, --repl  \
    run Cogent REPL
--docgent  \
    generate HTML documentation from Docgent comments;
    must be enabled at Cogent compile time
--pretty-parse  \
    pretty-print surface language
-T, --pretty-tc  \
    pretty-print type-checked surface language
-D, --pretty-desugar  \
    pretty-print desugared core language
--pretty-normal  \
    pretty-print normalised core language
--pretty-simpl  \
    pretty-print simplified core language
--pretty-mono  \
    pretty-print monomorphised core language
--hs-shallow-desugar  \
    generate Haskell shallow embedding (desugared core)
--hs-shallow-desugar-tuples  \
    generate Haskell shallow embedding (desugared core, with Haskell tuples)
--hs-ffi  \
    generate Haskell FFI code to access generated C code
    (including a ``.hsc`` module for types
    and a ``.hs`` module for functions)
--deep-desugar  \
    generate Isabelle deep embedding (desugared core)
--deep-normal  \
    generate Isabelle deep embedding (normalised core)
--deep-mono  \
    generate Isabelle deep embedding (monomorphised core)
--shallow-desugar  \
    generate Isabelle shallow embedding (desugared core)
--shallow-normal  \
    generate Isabelle shallow embedding (normalised core)
--shallow-mono  \
    generate Isabelle shallow embedding (monomorphised core)
--shallow-desugar-tuples  \
    enerate Isabelle shallow embedding (desugared core, with HOL tuples)
--scorres-desugar  \
    generate scorres (desugared core)
--scorres-normal  \
    generate scorres (normalised core)
--scorres-mono  \
    generate scorres (monomorphised core)
--shallow-consts-desugar  \
    generate constant definitions for shallow embedding (desugared core)
--shallow-consts-normal  \
    generate constant definitions for shallow embedding (normalised core)
--shallow-consts-mono  \
    generate constant definitions for shallow embedding (monomorphised core)
--shallow-consts-desugar-tuples  \
    generate constant definitions for shallow embedding (desugared core, with HOL tuples)
--shallow-tuples-proof  \
    generate proof for shallow tuples embedding
--normal-proof  \
    generate Isabelle proof of normalisation
--mono-proof  \
    generate monomorphisation proof
--ac-install  \
    generate an Isabelle theory to install AutoCorres
--corres-setup  \
    generate Isabelle lemmas for c-refinement
--corres-proof  \
    generate Isabelle proof of c-refinement
--type-proof-normal  \
    generate Isabelle proof of type correctness of normalised AST
--type-proof  \
    generate Isabelle proof of type correctness of normal-mono AST
--all-refine  \
    generate shallow-to-C refinement proof  (*collective*)
--root  \
    generate an Isabelle ROOT file
--table-c-types  \
    generate a table of Cogent and C type correspondence
--table-shallow  \
    generate a table of type synonyms for shallow embedding
--table-abs-func-mono  \
    generate a table of monomorphised abstract functions
--table-abs-type-mono  \
    generate a table of monomorphised abstract types
-G, --graph-gen  \
    generate graph for graph-refine
--build-info  \
    log how cogent is being invoked by generating ``BUILD_INFO`` file;
    implied by any collective commands
-C, --c-refinement  \
    generate all files needed for the C refinement proof  (*collective*)
-F, --functional-correctness  \
    generate all files needed for the functional correctness proof  (*collective*)
-A, --all  \
    generate all possible outputs  (*collective*)
-Q, --quickcheck  \
    generate QuickCheck related artifacts  (*collective*)
--libgum-dir  \
    display directory where standard gum headers are installed
    (can be set by the ``$COGENT_LIBGUM_DIR`` environment variable)
-v, -V, --version  \
    show version number


All Flags
^^^^^^^^^^^^^^^^^^^^^^^^

-o NAME, --output-name=NAME  \
    specify base name for output files;
    by default, derived from name of source Cogent file
--proof-name=NAME  \
    specify Isabelle theory file name;
    by default, derived from name of source Cogent file
--abs-type-dir=PATH  \
    abstract type definitions will be in ``PATH/abstract/``,
    which must exist (default is ``./``)
--dist-dir=PATH  \
    specify path to all output files (default is ``./``)
--fake-header-dir=PATH  \
    specify path to fake C header files
--root-dir=PATH  \
    specify path to top-level directory (for imports in theory files only, default is ``./``)
--cust-ty-gen=FILE  \
    config file to customise type generation
--entry-funcs=FILE  \
    give a list of Cogent functions that are only called from outside
--ext-types=FILE  \
    give external type names to C parser
--infer-c-funcs=FILE  \
    infer Cogent abstract function definitions
    (can be specified multiple times)
--infer-c-types=FILE  \
    infer Cogent abstract type definitions
    (can be specified multiple times)
--name-cache=FILE  \
    specify the name cache file to use
--proof-input-c=FILE  \
    specify input C file to generate proofs;
    defaults to the same base name as input Cogent file
--prune-call-graph=FILE  \
    specify Cogent entry-point definitions
--cogent-pp-args=ARG  \
    arguments given to Cogent preprocessor
    (same as for cpphs; can be specified multiple times)
--cpp=PROG  \
    set which C-preprocessor to use (default to ``cpp``)
--cpp-args=ARG  \
    arguments given to C-preprocessor (default to ``$CPPIN -P -o $CPPOUT``)
--ddump-smt  \
    dump verbose SMT-solving information
--ddump-tc  \
    dump (massive) surface typechecking internals
--ddump-tc-ctx  \
    dump surface typechecking with context
--ddump-tc-filter=KEYWORDS  \
    a space-separated list of keywords to indicate
    which groups of info to display;
    possible keywords are ``gen``, ``sol``, ``post``, ``tc``
--ddump-to-file=FILE  \
    dump debugging output to specific file instead of terminal
--ddump-pretty-ds-no-tc  \
    dump the pretty printed desugared expression before typechecking
--fcheck-undefined, --fno-check-undefined  \
    check for undefined behaviours in C (default enabled)
-B, --fdisambiguate-pp  \
    when pretty-printing, also display internal representation as comments
--fffi-c-functions  \
    generate FFI functions in the C code
    (should be used when ``-Q``/``--quickcheck`` is specified)
--fflatten-nestings, --fno-flatten-nestings  \
    flatten out nested structs in C code (does nothing; default is disabled)
--ffncall-as-macro, --fno-fncall-as-macro  \
    generate macros instead of real function calls (default is disabled)
--ffull-src-path  \
    display full path for source file locations
--ffunc-purity-attr, --fno-func-purity-attr  \
    generate GCC attributes to classify purity of Cogent functions (default is enabled)
--fgen-header, --fno-gen-header  \
    generate build info header in all output files (default is disabled)
--fintermediate-vars, --fno-intermediate-vars  \
    generate intermediate variables for Cogent expressions (default is enabled)
--flax-take-put, --fno-lax-take-put  \
    allow take/put type operators on abstract datatypes (default is disabled)
--flet-in-if, --fno-let-in-if  \
    put binding of a ``let`` inside an ``if``\ -clause (default is enabled)
--fletbang-in-if, --fno-letbang-in-if  \
    put binding of a ``let!`` inside an ``if``\ -clause (default is enabled)
--fml-typing-tree, --fno-ml-typing-tree  \
    generate ML typing tree in type proofs (default is enabled)
--fnormalisation=NF, --fno-normalisation  \
    normalise (or don't normalise) the core language
    to the *NF* normal form,
    which may be ``anf``, ``knf``, or ``lnf``;
    the default is to normalise to ``anf``
--fpragmas, --fno-pragmas  \
    preprocess pragmas (default is enabled)
--fpretty-errmsgs, --fno-pretty-errmsgs  \
    enable/disable pretty-printing of error messages
    (requires ANSI support; default is enabled)
--freverse-tc-errors, --fno-reverse-tc-errors  \
    reverse the order of type errors printed
--fshare-linear-vars, --fno-share-linear-vars  \
    reuse C variables for linear objects (default is disabled)
--fshow-types-in-pretty, --fno-show-types-in-pretty  \
    show inferred types of each AST node
    when doing pretty-printing  (default is disabled)
--fsimplifier, --fno-simplifier  \
    enable or disabled simplifier on core language (default is disabled)
--fsimplifier-level=NUMBER  \
    number of iterations simplifier does
    (default is 4; no effect if simplifier disabled)
--fstatic-inline, --fno-static-inline  \
    mark generated C functions as ``static inline`` (default is enabled)
--ftuples-as-sugar, --fno-tuples-as-sugar  \
    treat tuples as syntactic sugar to unboxed records,
    which gives better performance; or don't
    (default is enabled)
--ftc-ctx-constraints, --fno-tc-ctx-constraints  \
    display (or don't display) constraints in type errors (default is disabled)
--ftc-ctx-len=NUMBER  \
    set the depth for printing error context in typechecker (default is 3)
--ftp-with-bodies, --fno-tp-with-bodies  \
    generate type proof with bodies (default is enabled)
--ftp-with-decls, --fno-typ-with-decls  \
    generate type proof with declarations (default is enabled)
--funion-for-variants, --fno-union-for-variants  \
    use union types for variants in C code;
    this cannot be verified  (default is disabled)
--funtyped-func-enum, --fno-untyped-func-enum  \
    use untyped function ``enum`` type  (default is enabled)
--fuse-compound-literals, --fno-use-compound-literals  \
    use compound literals when possible in C code;
    otherwise, create new variables
    (default is enabled)
--fwrap-put-in-let, --fno-wrap-put-in-let  \
    ``Put`` always appears in a ``Let``-binding when normalised
    (default is disabled)
-O LEVEL, --optimisation=LEVEL  \
    set optimisation level to one of
    ``-O0``, [TODO] no optimisations;
    ``-O1``, [TODO] some optimisations;
    ``-O2``, [TODO] more optimisations;
    ``-Od``, [TODO] (default);
    ``-On``, [TODO];
    ``-Os``, [TODO] size;
    ``-Ou``, [TODO]
--Wall  \
    issue all warnings
-w, --Wno-warn  \
    turn off all warnings
--Wwarn  \
    warnings are treated only as warnings, not as errors (default is enabled)
-E, --Werror  \
    make any warning into a fatal error (default is disabled)
--Wdodgy-take-put, --Wno-dodgy-take-put  \
    enable/disable warnings on ill-formed ``take`` or ``put`` in types
    (default is enabled)
--Wdynamic-variant-promotion, --Wno-dynamic-variant-promotion  \
    enable/disable warnings on dynamic variant type promotion
    (default is disabled)
--Wimplicit-int-lit-promotion, --Wno-implicit-int-lit-promotion  \
    enable/disable warning on implicit integer literal promotion
    (default is enabled)
--Wmono, --Wno-mono  \
    enable/disable warnings during monomorphisation
    (default is disabled)
--Wunused-local-binds, --Wno-unused-local-binds  \
    enable/disable warnings about unused local binders
    (default is disabled)
-q, --quiet  \
    do not display compilation progress
-x, --fdump-to-stdout  \
    dump all output to stdout
--interactive  \
    interactive compiler mode
--type-proof-sorry-before=FUN_NAME  \
    bad hack: ``sorry`` all type proofs for functions that precede given function name