diff --git a/CHANGES.md b/CHANGES.md index 96de3227b..056215cde 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -2,6 +2,24 @@ ## Language changes +* Cryptol now supports *enum* declarations. An enum is a named typed which is + defined by one or more constructors. Enums correspond to the notion of + algebraic data types, which are commonly found in other programming + languages. See the [manual + section](https://galoisinc.github.io/cryptol/master/TypeDeclarations.html#enums) + for more information. + +* Add two enum declarations to the Cryptol standard library: + + ``` + enum Option a = None | Some a + + enum Result t e = Ok t | Err e + ``` + + These types are useful for representing optional values (`Option`) or values + that may fail in some way (`Result`). + * `foreign` functions can now have an optional Cryptol implementation, which by default is used when the foreign implementation cannot be found, or if the FFI is unavailable. The `:set evalForeign` REPL option controls this behavior. diff --git a/cryptol-remote-api/src/CryptolServer/Data/Expression.hs b/cryptol-remote-api/src/CryptolServer/Data/Expression.hs index 623775513..17af0f758 100644 --- a/cryptol-remote-api/src/CryptolServer/Data/Expression.hs +++ b/cryptol-remote-api/src/CryptolServer/Data/Expression.hs @@ -617,8 +617,7 @@ readBack ty val = TVTuple{} -> "tuple" TVRec{} -> "record" TVFun{} -> "fun" - TVNewtype nt _ _ -> identText $ nameIdent $ TC.ntName nt - TVAbstract{} -> "abstract" + TVNominal nt _ _ -> identText $ nameIdent $ TC.ntName nt -- | Given a suggested `name` and a type and value, attempt to bind the value diff --git a/cryptol-remote-api/src/CryptolServer/Data/Type.hs b/cryptol-remote-api/src/CryptolServer/Data/Type.hs index 1cbb9f355..2674fdcd5 100644 --- a/cryptol-remote-api/src/CryptolServer/Data/Type.hs +++ b/cryptol-remote-api/src/CryptolServer/Data/Type.hs @@ -20,7 +20,10 @@ import Cryptol.Parser.Position (emptyRange) import Cryptol.Parser.Selector (ppSelector) import Cryptol.Utils.RecordMap (recordFromFields) import Cryptol.TypeCheck.PP (NameMap, emptyNameMap, ppWithNames) -import Cryptol.TypeCheck.Type (Kind(..), PC(..), TC(..), TCon(..), TFun(..), TParam(..), Type(..), Schema(..), addTNames, kindOf) +import Cryptol.TypeCheck.Type (Kind(..), PC(..), TC(..), TCon(..), + TFun(..), TParam(..), Type(..), Schema(..), addTNames, kindOf, + NominalType(..), NominalTypeDef(..) + ) import Cryptol.Utils.Ident (mkIdent) import Cryptol.Utils.PP (pp) import Cryptol.Utils.RecordMap (canonicalFields) @@ -213,8 +216,14 @@ instance JSON.ToJSON JSONType where , "name" .= show (ppWithNames ns v) ] convert (TUser _n _args def) = convert def - convert (TNewtype _nt _ts) = - JSON.object [ "type" .= T.pack "newtype" ] + convert (TNominal nt ts) = + JSON.object [ "type" .= case ntDef nt of + Struct {} -> T.pack "newtype" + Enum {} -> T.pack "enum" + Abstract -> T.pack "primitive" + , "name" .= show (pp (ntName nt)) + , "arguments" .= map (JSONType ns) ts + ] convert (TRec fields) = JSON.object [ "type" .= T.pack "record" diff --git a/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex b/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex index 7e7913593..f8a01980f 100644 --- a/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex +++ b/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex @@ -791,7 +791,7 @@ \subsection{Appending and indexing} [] invalid sequence index: 12 -- Backtrace -- - (Cryptol::@) called at Cryptol:885:14--885:20 + (Cryptol::@) called at Cryptol:904:14--904:20 (Cryptol::@@) called at :9:1--9:28 [9, 8, 7, 6, 5, 4, 3, 2, 1, 0] 9 diff --git a/docs/RefMan/TypeDeclarations.rst b/docs/RefMan/TypeDeclarations.rst index 4e985334f..00bfe7de7 100644 --- a/docs/RefMan/TypeDeclarations.rst +++ b/docs/RefMan/TypeDeclarations.rst @@ -51,3 +51,185 @@ of newtypes to extract the values in the body of the type. > sum x.seq 6 +Enums +----- + +.. code-block:: cryptol + + enum Maybe a = Nothing | Just a + +An ``enum`` declaration introduces a new named type, which is defined by a +collection of *constructors*. ``enum`` declarations correspond to the notion of +*algebraic data types*, which are commonly found in other programming +languages. Each named ``enum`` type is treated like a separate type, even if it +has the exact same constructors as another ``enum`` type---in this way ``enum`` +is similar to ``newtype`` and unlike ``type`` synonyms. + +**Constructors.** The only way to create a value of an ``enum`` type is to +use one of its constructors. When used in an expression, the constructors +behave like an ordinary function, which has one parameter for each field of the +constructor. For example, the constructor ``Just`` has a type like this: + +.. code-block:: cryptol + + Just: {a} a -> Maybe a + +Constructors may have 0 or multiple fields, and values created with different +constructors are always distinct. + +**Case Expressions.** The only way to examine a value of an ``enum`` type is +with a ``case`` expression, which are similar to ``if`` expressions: + +.. code-block:: cryptol + + case e of + Nothing -> 0 + Just a -> a + 1 + +In this example, ``e`` is an expression of type ``Maybe``: + + * if it was created with the ``Nothing`` constructor, + then we'll use the first branch of the ``case`` expression, and + the result of the whole expression would be 0; + + * if, ``e`` was created by applying the ``Just`` constructor to some + value (e.g, ``Just 2``), then we'll use the second branch of the ``case`` + expression, and the variable ``a`` will be bound to the value of the field + (e.g., ``2``), and the whole expression will evaluate to ``a + 1`` + (e.g., ``3``). + +It is also possible to use just a variable (or ``_``) in a case expression +to define a catch-all clause---if a value does not match any of the previous +cases, then this branch will be used: + +.. code-block:: cryptol + + isNothing x = + case x of + Nothing -> True + _ -> False + +**``Option`` and ``Result``.** Currently, Cryptol defines two ``enum`` +declarations in the Cryptol standard library: ``Option`` and ``Result``: + +.. code-block:: cryptol + + enum Option a = None | Some a + + enum Result t e = Ok t | Err e + +The ``Option a`` type represents an optional value, which can either be a value +of type ``a`` (``Some``) or no value at all ``None``. A value of type ``Result +t e`` can either be a successful value of type ``t`` (``Ok``) or an error value +of type ``e`` (``Err``). + +``Option`` and ``Result`` values are commonly used to model the return type of +partial functions, i.e., functions that are not defined for all inputs. For +instance, if a function ``f`` is not defined on the input ``42``, then one +could model this with ``Option``: + +.. code-block:: cryptol + + f : [8] -> Option [8] + f x = + if x == 42 + then None + else Some (x+1) + +One could also model this with ``Result``: + +.. code-block:: cryptol + + f : [8] -> Result [8] (String [8]) + f x = + if x == 42 + then Err "`f 42` not defined" + else Ok (x+1) + +With either result type, one can gracefully recover from ``f 42`` erroring by +matching on ``None`` or ``Err`` in a ``case`` expression. + +**Upper Case Restriction.** +The names of the constructors in an ``enum`` declarations +need to start with an upper-case letter. This restriction makes it possible +to distinguish between constructors and variable +bindings in ``case`` patterns (e.g., between ``Just`` and ``a`` in the +previous example). + +**Non Recursive.** The fields in a constructor may be of any value type, +as long as this type does not depend on the type to which the constructor +belongs. This means that we do not support defining recursive types, +such as linked lists. + +**No Nested Constructor Patterns.** For simplicity, only non-constructor +patterns may be used in the fields of a constructor pattern. For example, +``Just (a,b)`` and ``Just (a # b)`` are OK, however, ``Just (Just a)`` +will be rejected. This is a restriction that we may lift in the future. + +**No Overlapping Patterns.** For simplicity, all patterns in a +``case`` expression must be disjoint. In particular, this means that: + + * No two patterns in a ``case`` expression can match the same constructor. + This means that Cryptol will reject the following example: + + .. code-block:: cryptol + + isNothing x = + case x of + Nothing -> True + Nothing -> False + + * If a ``case`` expression uses a catch-all clause, then that clause must + occur last in the expression. It is an error to match on additional + patterns after the catch-all clause. For instance, Cryptol will reject the + following example: + + .. code-block:: cryptol + + isNothing x = + case x of + Just _ -> False + _ -> True + Nothing -> False + +**Patterns Must Be Exhaustive.** The patterns in a ``case`` expression must +cover all constructors in the ``enum`` type being matched on. For example, +Cryptol will reject the following example, as it does not cover the ``Just`` +constructor: + +.. code-block:: cryptol + + isNothing x = + case x of + Nothing -> True + +**The Matched Expression Must Have a Known Enum Type.** Cryptol will reject +the following definition of ``f``, where ``f`` lacks a type signature: + +.. code-block:: cryptol + + f x = + case x of + _ -> () + +This is because it is not clear what the type of ``x`` (the expression being +matched) should be. The only pattern is a catch-all case, which does not reveal +anything about the type of ``x``. It would be incorrect to give ``f`` this type: + +.. code-block:: cryptol + + f : {a} a -> () + +This is because ``f`` is not really polymorphic in its argument type, as the +only values that can be matched in a ``case`` expression are those whose type +was declared as an ``enum``. As such, Cryptol rejects this example. + +Cryptol will also reject this definition, where the type of the value +being matched is not an ``enum`` type: + +.. code-block:: cryptol + + g : Integer -> () + g x = + case x of + _ -> () diff --git a/docs/RefMan/_build/doctrees/BasicSyntax.doctree b/docs/RefMan/_build/doctrees/BasicSyntax.doctree index 62d0e5374..061e84322 100644 Binary files a/docs/RefMan/_build/doctrees/BasicSyntax.doctree and b/docs/RefMan/_build/doctrees/BasicSyntax.doctree differ diff --git a/docs/RefMan/_build/doctrees/BasicTypes.doctree b/docs/RefMan/_build/doctrees/BasicTypes.doctree index b90e13da4..938661b77 100644 Binary files a/docs/RefMan/_build/doctrees/BasicTypes.doctree and b/docs/RefMan/_build/doctrees/BasicTypes.doctree differ diff --git a/docs/RefMan/_build/doctrees/Expressions.doctree b/docs/RefMan/_build/doctrees/Expressions.doctree index 1c8f46b2b..bdd96f434 100644 Binary files a/docs/RefMan/_build/doctrees/Expressions.doctree and b/docs/RefMan/_build/doctrees/Expressions.doctree differ diff --git a/docs/RefMan/_build/doctrees/FFI.doctree b/docs/RefMan/_build/doctrees/FFI.doctree index ffee8cc94..409f72a4d 100644 Binary files a/docs/RefMan/_build/doctrees/FFI.doctree and b/docs/RefMan/_build/doctrees/FFI.doctree differ diff --git a/docs/RefMan/_build/doctrees/Modules.doctree b/docs/RefMan/_build/doctrees/Modules.doctree index 1dd5fbe3b..dad639f6d 100644 Binary files a/docs/RefMan/_build/doctrees/Modules.doctree and b/docs/RefMan/_build/doctrees/Modules.doctree differ diff --git a/docs/RefMan/_build/doctrees/OverloadedOperations.doctree b/docs/RefMan/_build/doctrees/OverloadedOperations.doctree index a18310b7a..e2faaa677 100644 Binary files a/docs/RefMan/_build/doctrees/OverloadedOperations.doctree and b/docs/RefMan/_build/doctrees/OverloadedOperations.doctree differ diff --git a/docs/RefMan/_build/doctrees/RefMan.doctree b/docs/RefMan/_build/doctrees/RefMan.doctree index 603c38df0..3f7f9e8af 100644 Binary files a/docs/RefMan/_build/doctrees/RefMan.doctree and b/docs/RefMan/_build/doctrees/RefMan.doctree differ diff --git a/docs/RefMan/_build/doctrees/TypeDeclarations.doctree b/docs/RefMan/_build/doctrees/TypeDeclarations.doctree index dce440060..f399f7f99 100644 Binary files a/docs/RefMan/_build/doctrees/TypeDeclarations.doctree and b/docs/RefMan/_build/doctrees/TypeDeclarations.doctree differ diff --git a/docs/RefMan/_build/doctrees/environment.pickle b/docs/RefMan/_build/doctrees/environment.pickle index 1e0c6b9bd..0cf211973 100644 Binary files a/docs/RefMan/_build/doctrees/environment.pickle and b/docs/RefMan/_build/doctrees/environment.pickle differ diff --git a/docs/RefMan/_build/html/.buildinfo b/docs/RefMan/_build/html/.buildinfo index 31b3902b4..3b4193dce 100644 --- a/docs/RefMan/_build/html/.buildinfo +++ b/docs/RefMan/_build/html/.buildinfo @@ -1,4 +1,4 @@ # Sphinx build info version 1 # This file hashes the configuration used when building these files. When it is not found, a full rebuild will be done. -config: 49d6d89345e8bba027ef627e0adeb689 +config: 41758cdb8fafe65367e2aa727ac7d826 tags: 645f666f9bcd5a90fca523b33c5a78b7 diff --git a/docs/RefMan/_build/html/BasicSyntax.html b/docs/RefMan/_build/html/BasicSyntax.html index ce1524dff..3fc515845 100644 --- a/docs/RefMan/_build/html/BasicSyntax.html +++ b/docs/RefMan/_build/html/BasicSyntax.html @@ -1,7 +1,7 @@ - + Basic Syntax — Cryptol 2.11.0 documentation @@ -11,9 +11,7 @@ - - @@ -26,15 +24,11 @@