diff options
| author | Alasdair Armstrong | 2017-11-27 17:30:03 +0000 |
|---|---|---|
| committer | Alasdair Armstrong | 2017-11-27 17:30:03 +0000 |
| commit | 4de5d52ee0f525d7c472e8aa3ee2a8158d888148 (patch) | |
| tree | ec200546002b15167715057e0d5530f0643d559b /src/rewrites.mli | |
| parent | 4a7d6e6d7e9221a19bc50c627b5714e45b1748bc (diff) | |
Split rewriter into separate rewriting library and rewrite passes
As discussed previously, we wanted to start refactoring the re-writer
to make it a bit less monolithic, and in the future potentially break
it into separate files for backend-specific rewrites and stuff.
- rewriter.ml now contains the generic re-writing code
- rewrites.ml contains the rewriting passes themselves
It would be nice if the generic rewriting code didn't depend on the
typechecker, because then it could be used in ASL parser on untyped
code.
Diffstat (limited to 'src/rewrites.mli')
| -rw-r--r-- | src/rewrites.mli | 60 |
1 files changed, 60 insertions, 0 deletions
diff --git a/src/rewrites.mli b/src/rewrites.mli new file mode 100644 index 00000000..628296ec --- /dev/null +++ b/src/rewrites.mli @@ -0,0 +1,60 @@ +(**************************************************************************) +(* Sail *) +(* *) +(* Copyright (c) 2013-2017 *) +(* Kathyrn Gray *) +(* Shaked Flur *) +(* Stephen Kell *) +(* Gabriel Kerneis *) +(* Robert Norton-Wright *) +(* Christopher Pulte *) +(* Peter Sewell *) +(* Thomas Bauereiss *) +(* *) +(* All rights reserved. *) +(* *) +(* This software was developed by the University of Cambridge Computer *) +(* Laboratory as part of the Rigorous Engineering of Mainstream Systems *) +(* (REMS) project, funded by EPSRC grant EP/K008528/1. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions *) +(* are met: *) +(* 1. Redistributions of source code must retain the above copyright *) +(* notice, this list of conditions and the following disclaimer. *) +(* 2. Redistributions in binary form must reproduce the above copyright *) +(* notice, this list of conditions and the following disclaimer in *) +(* the documentation and/or other materials provided with the *) +(* distribution. *) +(* *) +(* THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS'' *) +(* AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED *) +(* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A *) +(* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE AUTHOR OR *) +(* CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, *) +(* SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT *) +(* LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF *) +(* USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND *) +(* ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, *) +(* OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT *) +(* OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF *) +(* SUCH DAMAGE. *) +(**************************************************************************) + +open Ast +open Type_check + +(* Re-write undefined to functions created by -undefined_gen flag *) +val rewrite_undefined : bool -> tannot defs -> tannot defs + +(* Perform rewrites to exclude AST nodes not supported for ocaml out*) +val rewrite_defs_ocaml : (string * (tannot defs -> tannot defs)) list + +(* Perform rewrites to exclude AST nodes not supported for lem out*) +val rewrite_defs_lem : (string * (tannot defs -> tannot defs)) list + +(* This is a special rewriter pass that checks AST invariants without + actually doing any re-writing *) +val rewrite_defs_check : (string * (tannot defs -> tannot defs)) list + +val simple_typ : typ -> typ |