GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-09-11 14:06:13 +03:00
Code Issues Projects Releases Wiki Activity

Merge remote-tracking branch 'origin/master' into split-arith

Browse Source 
Minor merge conflicts resolved.
This commit is contained in:
Rob Dockins 2020-06-03 13:35:04 -07:00
commit 88c98c4c03
14 changed files with 104 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
lib/Array.cry Normal file
View File

@ -0,0 +1,13 @@
/*
* Copyright (c) 2020 Galois, Inc.
* Distributed under the terms of the BSD3 license (see LICENSE file)
*/
module Array where
primitive type Array : * -> * -> *
primitive arrayConstant : {a, b} b -> (Array a b)
primitive arrayLookup : {a, b} (Array a b) -> a -> b
primitive arrayUpdate : {a, b} (Array a b) -> a -> b -> (Array a b)

1
src/Cryptol/Eval.hs
View File

@ -428,6 +428,7 @@ etaDelay sym msg env0 Forall{ sVars = vs0, sType = tp0 } = goTpVars env0 vs0
TVInteger -> v
TVIntMod _ -> v
TVRational -> v
TVArray{} -> v
TVSeq n TVBit ->
do w <- sDelayFill sym (fromWordVal "during eta-expansion" =<< v) (etaWord sym n v)

16
src/Cryptol/Eval/Generic.hs
View File

@ -160,6 +160,9 @@ ringBinary sym opw opi opz opq = loop
TVRational ->
VRational <$> opq (fromVRational l) (fromVRational r)
TVArray{} ->
evalPanic "arithBinary" ["Array not in class Ring"]
TVSeq w a
-- words and finite sequences
| isTBit a -> do
@ -236,6 +239,9 @@ ringUnary sym opw opi opz opq = loop
TVRational ->
VRational <$> opq (fromVRational v)
TVArray{} ->
evalPanic "arithUnary" ["Array not in class Ring"]
TVSeq w a
-- words and finite sequences
| isTBit a -> do
@ -297,6 +303,8 @@ ringNullary sym opw opi opz opq = loop
TVRational -> VRational <$> opq
TVArray{} -> evalPanic "arithNullary" ["Array not in class Ring"]
TVSeq w a
-- words and finite sequences
| isTBit a -> pure $ VWord w $ (WordVal <$> opw w)
@ -623,6 +631,8 @@ cmpValue sym fb fw fi fz fq = cmp
TVInteger -> fi (fromVInteger v1) (fromVInteger v2) k
TVIntMod n -> fz n (fromVInteger v1) (fromVInteger v2) k
TVRational -> fq (fromVRational v1) (fromVRational v2) k
TVArray{} -> panic "Cryptol.Prims.Value.cmpValue"
[ "Arrays are not comparable" ]
TVSeq n t
| isTBit t -> do w1 <- fromVWord sym "cmpValue" v1
w2 <- fromVWord sym "cmpValue" v2
@ -776,6 +786,8 @@ zeroV sym ty = case ty of
TVRational ->
VRational <$> (intToRational sym =<< integerLit sym 0)
TVArray{} -> evalPanic "zeroV" ["Array not in class Zero"]
-- sequences
TVSeq w ety
| isTBit ety -> pure $ word sym w 0
@ -1179,6 +1191,8 @@ logicBinary sym opb opw = loop
TVInteger -> evalPanic "logicBinary" ["Integer not in class Logic"]
TVIntMod _ -> evalPanic "logicBinary" ["Z not in class Logic"]
TVRational -> evalPanic "logicBinary" ["Rational not in class Logic"]
TVArray{} -> evalPanic "logicBinary" ["Array not in class Logic"]
TVSeq w aty
-- words
| isTBit aty
@ -1255,6 +1269,7 @@ logicUnary sym opb opw = loop
TVInteger -> evalPanic "logicUnary" ["Integer not in class Logic"]
TVIntMod _ -> evalPanic "logicUnary" ["Z not in class Logic"]
TVRational -> evalPanic "logicBinary" ["Rational not in class Logic"]
TVArray{} -> evalPanic "logicUnary" ["Array not in class Logic"]
TVSeq w ety
-- words
@ -1658,6 +1673,7 @@ errorV sym ty msg = case ty of
TVInteger -> cryUserError sym msg
TVIntMod _ -> cryUserError sym msg
TVRational -> cryUserError sym msg
TVArray{} -> cryUserError sym msg
-- sequences
TVSeq w ety

14
src/Cryptol/Eval/Reference.lhs
View File

@ -68,6 +68,7 @@ are as follows:
| `Integer` | integers | `TVInteger` |
| `Z n` | integers modulo n | `TVIntMod n` |
| `Rational` | rationals | `TVRational` |
| `Array` | arrays | `TVArray` |
| `[n]a` | finite lists | `TVSeq n a` |
| `[inf]a` | infinite lists | `TVStream a` |
| `(a, b, c)` | tuples | `TVTuple [a,b,c]` |
@ -176,6 +177,7 @@ cpo that represents any given schema.
> TVInteger -> VInteger (fromVInteger val)
> TVIntMod _ -> VInteger (fromVInteger val)
> TVRational -> VRational (fromVRational val)
> TVArray{} -> evalPanic "copyByTValue" ["Unsupported Array type"]
> TVSeq w ety -> VList (Nat w) (map (go ety) (copyList w (fromVList val)))
> TVStream ety -> VList Inf (map (go ety) (copyStream (fromVList val)))
> TVTuple etys -> VTuple (zipWith go etys (copyList (genericLength etys) (fromVTuple val)))
@ -895,6 +897,7 @@ at the same positions.
> TVFun _ bty -> VFun (\v -> go bty (fromVFun val v))
> TVInteger -> evalPanic "logicUnary" ["Integer not in class Logic"]
> TVIntMod _ -> evalPanic "logicUnary" ["Z not in class Logic"]
> TVArray{} -> evalPanic "logicUnary" ["Array not in class Logic"]
> TVRational -> evalPanic "logicUnary" ["Rational not in class Logic"]
> TVAbstract{} -> evalPanic "logicUnary" ["Abstract type not in `Logic`"]
@ -913,6 +916,7 @@ at the same positions.
> TVFun _ bty -> VFun (\v -> go bty (fromVFun l v) (fromVFun r v))
> TVInteger -> evalPanic "logicBinary" ["Integer not in class Logic"]
> TVIntMod _ -> evalPanic "logicBinary" ["Z not in class Logic"]
> TVArray{} -> evalPanic "logicBinary" ["Array not in class Logic"]
> TVRational -> evalPanic "logicBinary" ["Rational not in class Logic"]
> TVAbstract{} -> evalPanic "logicBinary" ["Abstract type not in `Logic`"]
@ -944,6 +948,8 @@ False]`, but to `[error "foo", error "foo"]`.
> VInteger (flip mod n <$> i)
> TVRational ->
> VRational q
> TVArray{} ->
> evalPanic "arithNullary" ["Array not in class Arith"]
> TVSeq w a
> | isTBit a -> vWord w i
> | otherwise -> VList (Nat w) (genericReplicate w (go a))
@ -971,6 +977,8 @@ False]`, but to `[error "foo", error "foo"]`.
> evalPanic "arithUnary" ["Bit not in class Arith"]
> TVInteger ->
> VInteger $ appOp1 iop (fromVInteger val)
> TVArray{} ->
> evalPanic "arithUnary" ["Array not in class Arith"]
> TVIntMod n ->
> VInteger $ appOp1 (\i -> flip mod n <$> iop i) (fromVInteger val)
> TVRational ->
@ -1006,6 +1014,8 @@ False]`, but to `[error "foo", error "foo"]`.
> VInteger $ appOp2 (\i j -> flip mod n <$> iop i j) (fromVInteger l) (fromVInteger r)
> TVRational ->
> VRational $ appOp2 qop (fromVRational l) (fromVRational r)
> TVArray{} ->
> evalPanic "arithBinary" ["Array not in class Arith"]
> TVSeq w a
> | isTBit a -> vWord w $ appOp2 iop (fromVWord l) (fromVWord r)
> | otherwise -> VList (Nat w) (zipWith (go a) (fromVList l) (fromVList r))
@ -1149,6 +1159,8 @@ bits to the *left* of that position are equal.
> compare <$> fromVInteger l <*> fromVInteger r
> TVRational ->
> compare <$> fromVRational l <*> fromVRational r
> TVArray{} ->
> evalPanic "lexCompare" ["invalid type"]
> TVSeq _w ety ->
> lexList (zipWith (lexCompare ety) (fromVList l) (fromVList r))
> TVStream _ ->
@ -1194,6 +1206,8 @@ fields are compared in alphabetical order.
> evalPanic "lexSignedCompare" ["invalid type"]
> TVRational ->
> evalPanic "lexSignedCompare" ["invalid type"]
> TVArray{} ->
> evalPanic "lexSignedCompare" ["invalid type"]
> TVSeq _w ety
> | isTBit ety -> compare <$> fromSignedVWord l <*> fromSignedVWord r
> | otherwise ->

3
src/Cryptol/Eval/Type.hs
View File

@ -31,6 +31,7 @@ data TValue
| TVInteger -- ^ @ Integer @
| TVIntMod Integer -- ^ @ Z n @
| TVRational -- ^ @Rational@
| TVArray TValue TValue -- ^ @ Array a b @
| TVSeq Integer TValue -- ^ @ [n]a @
| TVStream TValue -- ^ @ [inf]t @
| TVTuple [TValue] -- ^ @ (a, b, c )@
@ -47,6 +48,7 @@ tValTy tv =
TVInteger -> tInteger
TVIntMod n -> tIntMod (tNum n)
TVRational -> tRational
TVArray a b -> tArray (tValTy a) (tValTy b)
TVSeq n t -> tSeq (tNum n) (tValTy t)
TVStream t -> tSeq tInf (tValTy t)
TVTuple ts -> tTuple (map tValTy ts)
@ -108,6 +110,7 @@ evalType env ty =
(TCIntMod, [n]) -> case num n of
Inf -> evalPanic "evalType" ["invalid type Z inf"]
Nat m -> Right $ TVIntMod m
(TCArray, [a, b]) -> Right $ TVArray (val a) (val b)
(TCSeq, [n, t]) -> Right $ tvSeq (num n) (val t)
(TCFun, [a, b]) -> Right $ TVFun (val a) (val b)
(TCTuple _, _) -> Right $ TVTuple (map val ts)

5
src/Cryptol/ModuleSystem/Base.hs
View File

@ -42,14 +42,14 @@ import qualified Cryptol.TypeCheck.AST as T
import qualified Cryptol.TypeCheck.PP as T
import qualified Cryptol.TypeCheck.Sanity as TcSanity
import Cryptol.Transform.AddModParams (addModParams)
import Cryptol.Utils.Ident (preludeName, interactiveName
import Cryptol.Utils.Ident (preludeName, arrayName, interactiveName
, modNameChunks, notParamInstModName
, isParamInstModName )
import Cryptol.Utils.PP (pretty)
import Cryptol.Utils.Panic (panic)
import Cryptol.Utils.Logger(logPutStrLn, logPrint)
import Cryptol.Prelude (preludeContents)
import Cryptol.Prelude (preludeContents, arrayContents)
import Cryptol.Transform.MonoValues (rewModule)
@ -259,6 +259,7 @@ findModule n = do
handleNotFound =
case n of
m | m == preludeName -> pure (InMem "Cryptol" preludeContents)
| m == arrayName -> pure (InMem "Array" arrayContents)
_ -> moduleNotFound n =<< getSearchPath
-- generate all possible search paths

6
src/Cryptol/ModuleSystem/Name.hs
View File

@ -13,6 +13,7 @@
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
-- for the instances of RunM and BaseM
{-# LANGUAGE UndecidableInstances #-}
@ -221,7 +222,10 @@ nameFixity = nFixity
asPrim :: Name -> Maybe Ident
asPrim Name { .. } =
case nInfo of
Declared p _ | p == preludeName -> Just nIdent
Declared p _
| p == preludeName -> Just nIdent
| p == arrayName ->
Just $ mkIdent $ modNameToText p <> "::" <> identText nIdent
_ -> Nothing
toParamInstName :: Name -> Name

9
src/Cryptol/Prelude.hs
View File

@ -13,7 +13,11 @@
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE OverloadedStrings #-}
module Cryptol.Prelude (preludeContents,cryptolTcContents) where
module Cryptol.Prelude
( preludeContents
, arrayContents
, cryptolTcContents
) where
import Data.ByteString(ByteString)
import qualified Data.ByteString.Char8 as B
@ -23,5 +27,8 @@ import Text.Heredoc (there)
preludeContents :: ByteString
preludeContents = B.pack [there|lib/Cryptol.cry|]
arrayContents :: ByteString
arrayContents = B.pack [there|lib/Array.cry|]
cryptolTcContents :: String
cryptolTcContents = [there|lib/CryptolTC.z3|]

2
src/Cryptol/Testing/Random.hs
View File

@ -363,6 +363,7 @@ typeSize ty =
TCon (TC (TCNum n)) _ -> Just n
_ -> Nothing
(TCIntMod, _) -> Nothing
(TCArray, _) -> Nothing
(TCSeq, [sz,el]) -> case tNoUser sz of
TCon (TC (TCNum n)) _ -> (^ n) <$> typeSize el
_ -> Nothing
@ -397,6 +398,7 @@ typeValues ty =
[ TCon (TC (TCNum n)) _ ] | 0 < n ->
[ VInteger x | x <- [ 0 .. n - 1 ] ]
_ -> []
TCArray -> []
TCSeq ->
case map tNoUser ts of
[ TCon (TC (TCNum n)) _, TCon (TC TCBit) [] ] ->

9
src/Cryptol/TypeCheck/TCon.hs
View File

@ -42,6 +42,7 @@ builtInType nm =
case M.nameInfo nm of
M.Declared m _
| m == preludeName -> Map.lookup (M.nameIdent nm) builtInTypes
| m == arrayName -> Map.lookup (M.nameIdent nm) builtInArray
_ -> Nothing
where
@ -85,6 +86,11 @@ builtInType nm =
, "lengthFromThenTo" ~> TF TCLenFromThenTo
]
-- Built-in types from Array.cry
builtInArray = Map.fromList
[ "Array" ~> TC TCArray
]
@ -120,6 +126,7 @@ instance HasKind TC where
TCInteger -> KType
TCRational -> KType
TCIntMod -> KNum :-> KType
TCArray -> KType :-> KType :-> KType
TCSeq -> KNum :-> KType :-> KType
TCFun -> KType :-> KType :-> KType
TCTuple n -> foldr (:->) KType (replicate n KType)
@ -202,6 +209,7 @@ data TC = TCNum Integer -- ^ Numbers
| TCInteger -- ^ Integer
| TCIntMod -- ^ @Z _@
| TCRational -- ^ @Rational@
| TCArray -- ^ @Array _ _@
| TCSeq -- ^ @[_] _@
| TCFun -- ^ @_ -> _@
| TCTuple Int -- ^ @(_, _, _)@
@ -302,6 +310,7 @@ instance PP TC where
TCInteger -> text "Integer"
TCIntMod -> text "Z"
TCRational -> text "Rational"
TCArray -> text "Array"
TCSeq -> text "[]"
TCFun -> text "(->)"
TCTuple 0 -> text "()"

3
src/Cryptol/TypeCheck/Type.hs
View File

@ -507,6 +507,9 @@ tRational = TCon (TC TCRational) []
tIntMod :: Type -> Type
tIntMod n = TCon (TC TCIntMod) [n]
tArray :: Type -> Type -> Type
tArray a b = TCon (TC TCArray) [a, b]
tWord :: Type -> Type
tWord a = tSeq a tBit

4
src/Cryptol/Utils/Ident.hs
View File

@ -16,6 +16,7 @@ module Cryptol.Utils.Ident
, modNameChunks
, packModName
, preludeName
, arrayName
, interactiveName
, noModuleName
, exprModName
@ -100,6 +101,9 @@ modInstPref = "`"
preludeName :: ModName
preludeName = packModName ["Cryptol"]
arrayName :: ModName
arrayName = packModName ["Array"]
interactiveName :: ModName
interactiveName = packModName ["<interactive>"]

3
tests/regression/array.icry Normal file
View File

@ -0,0 +1,3 @@
:module Array
:browse Array

20
tests/regression/array.icry.stdout Normal file
View File

@ -0,0 +1,20 @@
Loading module Cryptol
Loading module Array
Primitive Types
===============
Public
------
Array : * -> * -> *
Symbols
=======
Public
------
arrayConstant : {a, b} b -> Array a b
arrayLookup : {a, b} Array a b -> a -> b
arrayUpdate : {a, b} Array a b -> a -> b -> Array a b