59 lines
1.3 KiB
Plaintext
59 lines
1.3 KiB
Plaintext
%if false
|
|
Copyright (c) 2009 ETH Zurich.
|
|
All rights reserved.
|
|
|
|
This file is distributed under the terms in the attached LICENSE file.
|
|
If you do not find this file, copies can be found by writing to:
|
|
ETH Zurich D-INFK, Universitaetstrasse 6, CH-8092 Zurich. Attn: Systems Group.
|
|
%endif
|
|
|
|
%include polycode.fmt
|
|
|
|
%if false
|
|
|
|
> module Libc.Assert where
|
|
|
|
> import Text.PrettyPrint.HughesPJ as Pprinter
|
|
|
|
> import Semantics
|
|
|
|
> import Constructs
|
|
> import PureExpressions
|
|
> import {-# SOURCE #-} Expressions
|
|
|
|
> import IL.FoF.FoF
|
|
|
|
%endif
|
|
|
|
\section{Assert}
|
|
|
|
The construct |Assert| embeds the C @assert@ function into FoF.
|
|
|
|
\subsection{Smart Constructors}
|
|
|
|
The use of |assert| is obvious, by its definition.
|
|
|
|
> assert :: PureExpr -> FoFCode PureExpr
|
|
> assert test = inject (Assert test (return Void))
|
|
|
|
\subsection{Compile Instantiation}
|
|
|
|
The compilation is a direct translation into a foreign function:
|
|
|
|
> compileAssert (Assert e r) binding =
|
|
> let (cont, binding1) = r binding in
|
|
> (FStatement (FFFICall "assert" [e]) cont,
|
|
> binding1)
|
|
|
|
|
|
\subsection{Run Instantiation}
|
|
|
|
As mentioned with |Printf|, we take here the easy option of ignoring
|
|
the run-time behaviour of an assertion.
|
|
|
|
> runAssert (Assert a r) heap = r heap
|
|
|
|
Being able to capture the semantics of that operation would be helpful
|
|
when debugging a compiler. So, some efforts are worth being devoted
|
|
here.
|