Commit 23a1bfed authored by Giuseppe Castagna's avatar Giuseppe Castagna
Browse files


parent 8214fed0
......@@ -77,7 +77,7 @@ do it when the variable occurs at top-level in the test (i.e., the variable is t
expression being tested) or under some specific positions such as in
nested pairs or at the end of a path of selectors. \beppe{Not precise,
please check which are the cases that are handled in the cited
papers}. In this work we aim at removing this limitation on the
papers} In this work we aim at removing this limitation on the
contexts and develop a general theory to refine the type of variables
that occur in tested expressions under generic contexts, such as variables occurring on the
left or the right expressions of an application. In other words, we aim at establishing a formal framework to
......@@ -99,7 +99,7 @@ the latter.
We focus our study on conditionals that test types and consider the following syntax:
\) (e.g., in this syntax the body of \code{foo} rendered as
\) (e.g., in this syntax the body of \code{foo} is rendered as
\ifty{x}{\Int}{x+1}{(\textsf{trim } x)}
......@@ -10,7 +10,7 @@
......@@ -163,7 +163,7 @@ since, \texttt{or\_} has type\\
We consider \True, \Any and $\lnot\True$ as candidate types for
\texttt{x} which, in turn allows us to deduce a precise type given in the table. Finally, thanks to this rule it is no longer necessary to use a type case to force refinement. As a consequence we can define the functions \texttt{and\_} and \texttt{xor\_} more naturally as:
let and_ = fun (x : Any) -> fun (y : Any) -> not_ (or_ (not_ x) (not_ y))
let xor_ = fun (x : Any) -> fun (y : Any) -> and_ (or_ x y) (not_ (and_ x y))
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