mirror of
https://github.com/GaloisInc/cryptol.git
synced 2024-08-17 01:41:09 +03:00
Revert "Fix Array.cry comment. (#748)"
This reverts commit2ff4d4c031
. Revert "Add SMT Array primitives. (#732)" This reverts commitc1bdd77ff0
.
This commit is contained in:
parent
c53f3cf172
commit
9e444bf40f
@ -1,13 +0,0 @@
|
|||||||
/*
|
|
||||||
* 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)
|
|
||||||
|
|
@ -428,7 +428,6 @@ etaDelay sym msg env0 Forall{ sVars = vs0, sType = tp0 } = goTpVars env0 vs0
|
|||||||
TVInteger -> v
|
TVInteger -> v
|
||||||
TVIntMod _ -> v
|
TVIntMod _ -> v
|
||||||
TVRational -> v
|
TVRational -> v
|
||||||
TVArray{} -> v
|
|
||||||
|
|
||||||
TVSeq n TVBit ->
|
TVSeq n TVBit ->
|
||||||
do w <- sDelayFill sym (fromWordVal "during eta-expansion" =<< v) (etaWord sym n v)
|
do w <- sDelayFill sym (fromWordVal "during eta-expansion" =<< v) (etaWord sym n v)
|
||||||
|
@ -160,9 +160,6 @@ ringBinary sym opw opi opz opq = loop
|
|||||||
TVRational ->
|
TVRational ->
|
||||||
VRational <$> opq (fromVRational l) (fromVRational r)
|
VRational <$> opq (fromVRational l) (fromVRational r)
|
||||||
|
|
||||||
TVArray{} ->
|
|
||||||
evalPanic "arithBinary" ["Array not in class Ring"]
|
|
||||||
|
|
||||||
TVSeq w a
|
TVSeq w a
|
||||||
-- words and finite sequences
|
-- words and finite sequences
|
||||||
| isTBit a -> do
|
| isTBit a -> do
|
||||||
@ -239,9 +236,6 @@ ringUnary sym opw opi opz opq = loop
|
|||||||
TVRational ->
|
TVRational ->
|
||||||
VRational <$> opq (fromVRational v)
|
VRational <$> opq (fromVRational v)
|
||||||
|
|
||||||
TVArray{} ->
|
|
||||||
evalPanic "arithUnary" ["Array not in class Ring"]
|
|
||||||
|
|
||||||
TVSeq w a
|
TVSeq w a
|
||||||
-- words and finite sequences
|
-- words and finite sequences
|
||||||
| isTBit a -> do
|
| isTBit a -> do
|
||||||
@ -303,8 +297,6 @@ ringNullary sym opw opi opz opq = loop
|
|||||||
|
|
||||||
TVRational -> VRational <$> opq
|
TVRational -> VRational <$> opq
|
||||||
|
|
||||||
TVArray{} -> evalPanic "arithNullary" ["Array not in class Ring"]
|
|
||||||
|
|
||||||
TVSeq w a
|
TVSeq w a
|
||||||
-- words and finite sequences
|
-- words and finite sequences
|
||||||
| isTBit a -> pure $ VWord w $ (WordVal <$> opw w)
|
| isTBit a -> pure $ VWord w $ (WordVal <$> opw w)
|
||||||
@ -631,8 +623,6 @@ cmpValue sym fb fw fi fz fq = cmp
|
|||||||
TVInteger -> fi (fromVInteger v1) (fromVInteger v2) k
|
TVInteger -> fi (fromVInteger v1) (fromVInteger v2) k
|
||||||
TVIntMod n -> fz n (fromVInteger v1) (fromVInteger v2) k
|
TVIntMod n -> fz n (fromVInteger v1) (fromVInteger v2) k
|
||||||
TVRational -> fq (fromVRational v1) (fromVRational v2) k
|
TVRational -> fq (fromVRational v1) (fromVRational v2) k
|
||||||
TVArray{} -> panic "Cryptol.Prims.Value.cmpValue"
|
|
||||||
[ "Arrays are not comparable" ]
|
|
||||||
TVSeq n t
|
TVSeq n t
|
||||||
| isTBit t -> do w1 <- fromVWord sym "cmpValue" v1
|
| isTBit t -> do w1 <- fromVWord sym "cmpValue" v1
|
||||||
w2 <- fromVWord sym "cmpValue" v2
|
w2 <- fromVWord sym "cmpValue" v2
|
||||||
@ -786,8 +776,6 @@ zeroV sym ty = case ty of
|
|||||||
TVRational ->
|
TVRational ->
|
||||||
VRational <$> (intToRational sym =<< integerLit sym 0)
|
VRational <$> (intToRational sym =<< integerLit sym 0)
|
||||||
|
|
||||||
TVArray{} -> evalPanic "zeroV" ["Array not in class Zero"]
|
|
||||||
|
|
||||||
-- sequences
|
-- sequences
|
||||||
TVSeq w ety
|
TVSeq w ety
|
||||||
| isTBit ety -> pure $ word sym w 0
|
| isTBit ety -> pure $ word sym w 0
|
||||||
@ -1191,7 +1179,6 @@ logicBinary sym opb opw = loop
|
|||||||
TVInteger -> evalPanic "logicBinary" ["Integer not in class Logic"]
|
TVInteger -> evalPanic "logicBinary" ["Integer not in class Logic"]
|
||||||
TVIntMod _ -> evalPanic "logicBinary" ["Z not in class Logic"]
|
TVIntMod _ -> evalPanic "logicBinary" ["Z not in class Logic"]
|
||||||
TVRational -> evalPanic "logicBinary" ["Rational not in class Logic"]
|
TVRational -> evalPanic "logicBinary" ["Rational not in class Logic"]
|
||||||
TVArray{} -> evalPanic "logicBinary" ["Array not in class Logic"]
|
|
||||||
|
|
||||||
TVSeq w aty
|
TVSeq w aty
|
||||||
-- words
|
-- words
|
||||||
@ -1269,7 +1256,6 @@ logicUnary sym opb opw = loop
|
|||||||
TVInteger -> evalPanic "logicUnary" ["Integer not in class Logic"]
|
TVInteger -> evalPanic "logicUnary" ["Integer not in class Logic"]
|
||||||
TVIntMod _ -> evalPanic "logicUnary" ["Z not in class Logic"]
|
TVIntMod _ -> evalPanic "logicUnary" ["Z not in class Logic"]
|
||||||
TVRational -> evalPanic "logicBinary" ["Rational not in class Logic"]
|
TVRational -> evalPanic "logicBinary" ["Rational not in class Logic"]
|
||||||
TVArray{} -> evalPanic "logicUnary" ["Array not in class Logic"]
|
|
||||||
|
|
||||||
TVSeq w ety
|
TVSeq w ety
|
||||||
-- words
|
-- words
|
||||||
@ -1712,7 +1698,6 @@ errorV sym ty msg = case ty of
|
|||||||
TVInteger -> cryUserError sym msg
|
TVInteger -> cryUserError sym msg
|
||||||
TVIntMod _ -> cryUserError sym msg
|
TVIntMod _ -> cryUserError sym msg
|
||||||
TVRational -> cryUserError sym msg
|
TVRational -> cryUserError sym msg
|
||||||
TVArray{} -> cryUserError sym msg
|
|
||||||
|
|
||||||
-- sequences
|
-- sequences
|
||||||
TVSeq w ety
|
TVSeq w ety
|
||||||
|
@ -68,7 +68,6 @@ are as follows:
|
|||||||
| `Integer` | integers | `TVInteger` |
|
| `Integer` | integers | `TVInteger` |
|
||||||
| `Z n` | integers modulo n | `TVIntMod n` |
|
| `Z n` | integers modulo n | `TVIntMod n` |
|
||||||
| `Rational` | rationals | `TVRational` |
|
| `Rational` | rationals | `TVRational` |
|
||||||
| `Array` | arrays | `TVArray` |
|
|
||||||
| `[n]a` | finite lists | `TVSeq n a` |
|
| `[n]a` | finite lists | `TVSeq n a` |
|
||||||
| `[inf]a` | infinite lists | `TVStream a` |
|
| `[inf]a` | infinite lists | `TVStream a` |
|
||||||
| `(a, b, c)` | tuples | `TVTuple [a,b,c]` |
|
| `(a, b, c)` | tuples | `TVTuple [a,b,c]` |
|
||||||
@ -177,7 +176,6 @@ cpo that represents any given schema.
|
|||||||
> TVInteger -> VInteger (fromVInteger val)
|
> TVInteger -> VInteger (fromVInteger val)
|
||||||
> TVIntMod _ -> VInteger (fromVInteger val)
|
> TVIntMod _ -> VInteger (fromVInteger val)
|
||||||
> TVRational -> VRational (fromVRational val)
|
> TVRational -> VRational (fromVRational val)
|
||||||
> TVArray{} -> evalPanic "copyByTValue" ["Unsupported Array type"]
|
|
||||||
> TVSeq w ety -> VList (Nat w) (map (go ety) (copyList w (fromVList val)))
|
> TVSeq w ety -> VList (Nat w) (map (go ety) (copyList w (fromVList val)))
|
||||||
> TVStream ety -> VList Inf (map (go ety) (copyStream (fromVList val)))
|
> TVStream ety -> VList Inf (map (go ety) (copyStream (fromVList val)))
|
||||||
> TVTuple etys -> VTuple (zipWith go etys (copyList (genericLength etys) (fromVTuple val)))
|
> TVTuple etys -> VTuple (zipWith go etys (copyList (genericLength etys) (fromVTuple val)))
|
||||||
@ -823,7 +821,6 @@ where the given error is "pushed down" into the leaf types.
|
|||||||
> cryError e TVInteger = VInteger (Left e)
|
> cryError e TVInteger = VInteger (Left e)
|
||||||
> cryError e TVIntMod{} = VInteger (Left e)
|
> cryError e TVIntMod{} = VInteger (Left e)
|
||||||
> cryError e TVRational = VRational (Left e)
|
> cryError e TVRational = VRational (Left e)
|
||||||
> cryError _ TVArray{} = evalPanic "error" ["Array type not supported in `error`"]
|
|
||||||
> cryError e (TVSeq n ety) = VList (Nat n) (genericReplicate n (cryError e ety))
|
> cryError e (TVSeq n ety) = VList (Nat n) (genericReplicate n (cryError e ety))
|
||||||
> cryError e (TVStream ety) = VList Inf (repeat (cryError e ety))
|
> cryError e (TVStream ety) = VList Inf (repeat (cryError e ety))
|
||||||
> cryError e (TVTuple tys) = VTuple (map (cryError e) tys)
|
> cryError e (TVTuple tys) = VTuple (map (cryError e) tys)
|
||||||
@ -848,7 +845,6 @@ For functions, `zero` returns the constant function that returns
|
|||||||
> zero TVInteger = VInteger (Right 0)
|
> zero TVInteger = VInteger (Right 0)
|
||||||
> zero TVIntMod{} = VInteger (Right 0)
|
> zero TVIntMod{} = VInteger (Right 0)
|
||||||
> zero TVRational = VRational (Right 0)
|
> zero TVRational = VRational (Right 0)
|
||||||
> zero TVArray{} = evalPanic "zero" ["Array type not in `Zero`"]
|
|
||||||
> zero (TVSeq n ety) = VList (Nat n) (genericReplicate n (zero ety))
|
> zero (TVSeq n ety) = VList (Nat n) (genericReplicate n (zero ety))
|
||||||
> zero (TVStream ety) = VList Inf (repeat (zero ety))
|
> zero (TVStream ety) = VList Inf (repeat (zero ety))
|
||||||
> zero (TVTuple tys) = VTuple (map zero tys)
|
> zero (TVTuple tys) = VTuple (map zero tys)
|
||||||
@ -899,7 +895,6 @@ at the same positions.
|
|||||||
> TVFun _ bty -> VFun (\v -> go bty (fromVFun val v))
|
> TVFun _ bty -> VFun (\v -> go bty (fromVFun val v))
|
||||||
> TVInteger -> evalPanic "logicUnary" ["Integer not in class Logic"]
|
> TVInteger -> evalPanic "logicUnary" ["Integer not in class Logic"]
|
||||||
> TVIntMod _ -> evalPanic "logicUnary" ["Z 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"]
|
> TVRational -> evalPanic "logicUnary" ["Rational not in class Logic"]
|
||||||
> TVAbstract{} -> evalPanic "logicUnary" ["Abstract type not in `Logic`"]
|
> TVAbstract{} -> evalPanic "logicUnary" ["Abstract type not in `Logic`"]
|
||||||
|
|
||||||
@ -918,7 +913,6 @@ at the same positions.
|
|||||||
> TVFun _ bty -> VFun (\v -> go bty (fromVFun l v) (fromVFun r v))
|
> TVFun _ bty -> VFun (\v -> go bty (fromVFun l v) (fromVFun r v))
|
||||||
> TVInteger -> evalPanic "logicBinary" ["Integer not in class Logic"]
|
> TVInteger -> evalPanic "logicBinary" ["Integer not in class Logic"]
|
||||||
> TVIntMod _ -> evalPanic "logicBinary" ["Z 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"]
|
> TVRational -> evalPanic "logicBinary" ["Rational not in class Logic"]
|
||||||
> TVAbstract{} -> evalPanic "logicBinary" ["Abstract type not in `Logic`"]
|
> TVAbstract{} -> evalPanic "logicBinary" ["Abstract type not in `Logic`"]
|
||||||
|
|
||||||
@ -950,8 +944,6 @@ False]`, but to `[error "foo", error "foo"]`.
|
|||||||
> VInteger (flip mod n <$> i)
|
> VInteger (flip mod n <$> i)
|
||||||
> TVRational ->
|
> TVRational ->
|
||||||
> VRational q
|
> VRational q
|
||||||
> TVArray{} ->
|
|
||||||
> evalPanic "arithNullary" ["Array not in class Ring"]
|
|
||||||
> TVSeq w a
|
> TVSeq w a
|
||||||
> | isTBit a -> vWord w i
|
> | isTBit a -> vWord w i
|
||||||
> | otherwise -> VList (Nat w) (genericReplicate w (go a))
|
> | otherwise -> VList (Nat w) (genericReplicate w (go a))
|
||||||
@ -979,8 +971,6 @@ False]`, but to `[error "foo", error "foo"]`.
|
|||||||
> evalPanic "arithUnary" ["Bit not in class Ring"]
|
> evalPanic "arithUnary" ["Bit not in class Ring"]
|
||||||
> TVInteger ->
|
> TVInteger ->
|
||||||
> VInteger $ appOp1 iop (fromVInteger val)
|
> VInteger $ appOp1 iop (fromVInteger val)
|
||||||
> TVArray{} ->
|
|
||||||
> evalPanic "arithUnary" ["Array not in class Ring"]
|
|
||||||
> TVIntMod n ->
|
> TVIntMod n ->
|
||||||
> VInteger $ appOp1 (\i -> flip mod n <$> iop i) (fromVInteger val)
|
> VInteger $ appOp1 (\i -> flip mod n <$> iop i) (fromVInteger val)
|
||||||
> TVRational ->
|
> TVRational ->
|
||||||
@ -1016,8 +1006,6 @@ False]`, but to `[error "foo", error "foo"]`.
|
|||||||
> VInteger $ appOp2 (\i j -> flip mod n <$> iop i j) (fromVInteger l) (fromVInteger r)
|
> VInteger $ appOp2 (\i j -> flip mod n <$> iop i j) (fromVInteger l) (fromVInteger r)
|
||||||
> TVRational ->
|
> TVRational ->
|
||||||
> VRational $ appOp2 qop (fromVRational l) (fromVRational r)
|
> VRational $ appOp2 qop (fromVRational l) (fromVRational r)
|
||||||
> TVArray{} ->
|
|
||||||
> evalPanic "arithBinary" ["Array not in class Ring"]
|
|
||||||
> TVSeq w a
|
> TVSeq w a
|
||||||
> | isTBit a -> vWord w $ appOp2 iop (fromVWord l) (fromVWord r)
|
> | isTBit a -> vWord w $ appOp2 iop (fromVWord l) (fromVWord r)
|
||||||
> | otherwise -> VList (Nat w) (zipWith (go a) (fromVList l) (fromVList r))
|
> | otherwise -> VList (Nat w) (zipWith (go a) (fromVList l) (fromVList r))
|
||||||
@ -1161,8 +1149,6 @@ bits to the *left* of that position are equal.
|
|||||||
> compare <$> fromVInteger l <*> fromVInteger r
|
> compare <$> fromVInteger l <*> fromVInteger r
|
||||||
> TVRational ->
|
> TVRational ->
|
||||||
> compare <$> fromVRational l <*> fromVRational r
|
> compare <$> fromVRational l <*> fromVRational r
|
||||||
> TVArray{} ->
|
|
||||||
> evalPanic "lexCompare" ["invalid type"]
|
|
||||||
> TVSeq _w ety ->
|
> TVSeq _w ety ->
|
||||||
> lexList (zipWith (lexCompare ety) (fromVList l) (fromVList r))
|
> lexList (zipWith (lexCompare ety) (fromVList l) (fromVList r))
|
||||||
> TVStream _ ->
|
> TVStream _ ->
|
||||||
@ -1208,8 +1194,6 @@ fields are compared in alphabetical order.
|
|||||||
> evalPanic "lexSignedCompare" ["invalid type"]
|
> evalPanic "lexSignedCompare" ["invalid type"]
|
||||||
> TVRational ->
|
> TVRational ->
|
||||||
> evalPanic "lexSignedCompare" ["invalid type"]
|
> evalPanic "lexSignedCompare" ["invalid type"]
|
||||||
> TVArray{} ->
|
|
||||||
> evalPanic "lexSignedCompare" ["invalid type"]
|
|
||||||
> TVSeq _w ety
|
> TVSeq _w ety
|
||||||
> | isTBit ety -> compare <$> fromSignedVWord l <*> fromSignedVWord r
|
> | isTBit ety -> compare <$> fromSignedVWord l <*> fromSignedVWord r
|
||||||
> | otherwise ->
|
> | otherwise ->
|
||||||
|
@ -31,7 +31,6 @@ data TValue
|
|||||||
| TVInteger -- ^ @ Integer @
|
| TVInteger -- ^ @ Integer @
|
||||||
| TVIntMod Integer -- ^ @ Z n @
|
| TVIntMod Integer -- ^ @ Z n @
|
||||||
| TVRational -- ^ @Rational@
|
| TVRational -- ^ @Rational@
|
||||||
| TVArray TValue TValue -- ^ @ Array a b @
|
|
||||||
| TVSeq Integer TValue -- ^ @ [n]a @
|
| TVSeq Integer TValue -- ^ @ [n]a @
|
||||||
| TVStream TValue -- ^ @ [inf]t @
|
| TVStream TValue -- ^ @ [inf]t @
|
||||||
| TVTuple [TValue] -- ^ @ (a, b, c )@
|
| TVTuple [TValue] -- ^ @ (a, b, c )@
|
||||||
@ -48,7 +47,6 @@ tValTy tv =
|
|||||||
TVInteger -> tInteger
|
TVInteger -> tInteger
|
||||||
TVIntMod n -> tIntMod (tNum n)
|
TVIntMod n -> tIntMod (tNum n)
|
||||||
TVRational -> tRational
|
TVRational -> tRational
|
||||||
TVArray a b -> tArray (tValTy a) (tValTy b)
|
|
||||||
TVSeq n t -> tSeq (tNum n) (tValTy t)
|
TVSeq n t -> tSeq (tNum n) (tValTy t)
|
||||||
TVStream t -> tSeq tInf (tValTy t)
|
TVStream t -> tSeq tInf (tValTy t)
|
||||||
TVTuple ts -> tTuple (map tValTy ts)
|
TVTuple ts -> tTuple (map tValTy ts)
|
||||||
@ -110,7 +108,6 @@ evalType env ty =
|
|||||||
(TCIntMod, [n]) -> case num n of
|
(TCIntMod, [n]) -> case num n of
|
||||||
Inf -> evalPanic "evalType" ["invalid type Z inf"]
|
Inf -> evalPanic "evalType" ["invalid type Z inf"]
|
||||||
Nat m -> Right $ TVIntMod m
|
Nat m -> Right $ TVIntMod m
|
||||||
(TCArray, [a, b]) -> Right $ TVArray (val a) (val b)
|
|
||||||
(TCSeq, [n, t]) -> Right $ tvSeq (num n) (val t)
|
(TCSeq, [n, t]) -> Right $ tvSeq (num n) (val t)
|
||||||
(TCFun, [a, b]) -> Right $ TVFun (val a) (val b)
|
(TCFun, [a, b]) -> Right $ TVFun (val a) (val b)
|
||||||
(TCTuple _, _) -> Right $ TVTuple (map val ts)
|
(TCTuple _, _) -> Right $ TVTuple (map val ts)
|
||||||
|
@ -42,14 +42,14 @@ import qualified Cryptol.TypeCheck.AST as T
|
|||||||
import qualified Cryptol.TypeCheck.PP as T
|
import qualified Cryptol.TypeCheck.PP as T
|
||||||
import qualified Cryptol.TypeCheck.Sanity as TcSanity
|
import qualified Cryptol.TypeCheck.Sanity as TcSanity
|
||||||
import Cryptol.Transform.AddModParams (addModParams)
|
import Cryptol.Transform.AddModParams (addModParams)
|
||||||
import Cryptol.Utils.Ident (preludeName, arrayName, interactiveName
|
import Cryptol.Utils.Ident (preludeName, interactiveName
|
||||||
, modNameChunks, notParamInstModName
|
, modNameChunks, notParamInstModName
|
||||||
, isParamInstModName )
|
, isParamInstModName )
|
||||||
import Cryptol.Utils.PP (pretty)
|
import Cryptol.Utils.PP (pretty)
|
||||||
import Cryptol.Utils.Panic (panic)
|
import Cryptol.Utils.Panic (panic)
|
||||||
import Cryptol.Utils.Logger(logPutStrLn, logPrint)
|
import Cryptol.Utils.Logger(logPutStrLn, logPrint)
|
||||||
|
|
||||||
import Cryptol.Prelude (preludeContents, arrayContents)
|
import Cryptol.Prelude (preludeContents)
|
||||||
|
|
||||||
import Cryptol.Transform.MonoValues (rewModule)
|
import Cryptol.Transform.MonoValues (rewModule)
|
||||||
|
|
||||||
@ -259,7 +259,6 @@ findModule n = do
|
|||||||
handleNotFound =
|
handleNotFound =
|
||||||
case n of
|
case n of
|
||||||
m | m == preludeName -> pure (InMem "Cryptol" preludeContents)
|
m | m == preludeName -> pure (InMem "Cryptol" preludeContents)
|
||||||
| m == arrayName -> pure (InMem "Array" arrayContents)
|
|
||||||
_ -> moduleNotFound n =<< getSearchPath
|
_ -> moduleNotFound n =<< getSearchPath
|
||||||
|
|
||||||
-- generate all possible search paths
|
-- generate all possible search paths
|
||||||
|
@ -13,7 +13,6 @@
|
|||||||
{-# LANGUAGE FlexibleInstances #-}
|
{-# LANGUAGE FlexibleInstances #-}
|
||||||
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
|
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
|
||||||
{-# LANGUAGE MultiParamTypeClasses #-}
|
{-# LANGUAGE MultiParamTypeClasses #-}
|
||||||
{-# LANGUAGE OverloadedStrings #-}
|
|
||||||
{-# LANGUAGE RecordWildCards #-}
|
{-# LANGUAGE RecordWildCards #-}
|
||||||
-- for the instances of RunM and BaseM
|
-- for the instances of RunM and BaseM
|
||||||
{-# LANGUAGE UndecidableInstances #-}
|
{-# LANGUAGE UndecidableInstances #-}
|
||||||
@ -222,10 +221,7 @@ nameFixity = nFixity
|
|||||||
asPrim :: Name -> Maybe Ident
|
asPrim :: Name -> Maybe Ident
|
||||||
asPrim Name { .. } =
|
asPrim Name { .. } =
|
||||||
case nInfo of
|
case nInfo of
|
||||||
Declared p _
|
Declared p _ | p == preludeName -> Just nIdent
|
||||||
| p == preludeName -> Just nIdent
|
|
||||||
| p == arrayName ->
|
|
||||||
Just $ mkIdent $ modNameToText p <> "::" <> identText nIdent
|
|
||||||
_ -> Nothing
|
_ -> Nothing
|
||||||
|
|
||||||
toParamInstName :: Name -> Name
|
toParamInstName :: Name -> Name
|
||||||
|
@ -13,11 +13,7 @@
|
|||||||
{-# LANGUAGE QuasiQuotes #-}
|
{-# LANGUAGE QuasiQuotes #-}
|
||||||
{-# LANGUAGE OverloadedStrings #-}
|
{-# LANGUAGE OverloadedStrings #-}
|
||||||
|
|
||||||
module Cryptol.Prelude
|
module Cryptol.Prelude (preludeContents,cryptolTcContents) where
|
||||||
( preludeContents
|
|
||||||
, arrayContents
|
|
||||||
, cryptolTcContents
|
|
||||||
) where
|
|
||||||
|
|
||||||
import Data.ByteString(ByteString)
|
import Data.ByteString(ByteString)
|
||||||
import qualified Data.ByteString.Char8 as B
|
import qualified Data.ByteString.Char8 as B
|
||||||
@ -27,8 +23,5 @@ import Text.Heredoc (there)
|
|||||||
preludeContents :: ByteString
|
preludeContents :: ByteString
|
||||||
preludeContents = B.pack [there|lib/Cryptol.cry|]
|
preludeContents = B.pack [there|lib/Cryptol.cry|]
|
||||||
|
|
||||||
arrayContents :: ByteString
|
|
||||||
arrayContents = B.pack [there|lib/Array.cry|]
|
|
||||||
|
|
||||||
cryptolTcContents :: String
|
cryptolTcContents :: String
|
||||||
cryptolTcContents = [there|lib/CryptolTC.z3|]
|
cryptolTcContents = [there|lib/CryptolTC.z3|]
|
||||||
|
@ -363,7 +363,6 @@ typeSize ty =
|
|||||||
TCon (TC (TCNum n)) _ -> Just n
|
TCon (TC (TCNum n)) _ -> Just n
|
||||||
_ -> Nothing
|
_ -> Nothing
|
||||||
(TCIntMod, _) -> Nothing
|
(TCIntMod, _) -> Nothing
|
||||||
(TCArray, _) -> Nothing
|
|
||||||
(TCSeq, [sz,el]) -> case tNoUser sz of
|
(TCSeq, [sz,el]) -> case tNoUser sz of
|
||||||
TCon (TC (TCNum n)) _ -> (^ n) <$> typeSize el
|
TCon (TC (TCNum n)) _ -> (^ n) <$> typeSize el
|
||||||
_ -> Nothing
|
_ -> Nothing
|
||||||
@ -398,7 +397,6 @@ typeValues ty =
|
|||||||
[ TCon (TC (TCNum n)) _ ] | 0 < n ->
|
[ TCon (TC (TCNum n)) _ ] | 0 < n ->
|
||||||
[ VInteger x | x <- [ 0 .. n - 1 ] ]
|
[ VInteger x | x <- [ 0 .. n - 1 ] ]
|
||||||
_ -> []
|
_ -> []
|
||||||
TCArray -> []
|
|
||||||
TCSeq ->
|
TCSeq ->
|
||||||
case map tNoUser ts of
|
case map tNoUser ts of
|
||||||
[ TCon (TC (TCNum n)) _, TCon (TC TCBit) [] ] ->
|
[ TCon (TC (TCNum n)) _, TCon (TC TCBit) [] ] ->
|
||||||
|
@ -42,7 +42,6 @@ builtInType nm =
|
|||||||
case M.nameInfo nm of
|
case M.nameInfo nm of
|
||||||
M.Declared m _
|
M.Declared m _
|
||||||
| m == preludeName -> Map.lookup (M.nameIdent nm) builtInTypes
|
| m == preludeName -> Map.lookup (M.nameIdent nm) builtInTypes
|
||||||
| m == arrayName -> Map.lookup (M.nameIdent nm) builtInArray
|
|
||||||
_ -> Nothing
|
_ -> Nothing
|
||||||
|
|
||||||
where
|
where
|
||||||
@ -86,11 +85,6 @@ builtInType nm =
|
|||||||
, "lengthFromThenTo" ~> TF TCLenFromThenTo
|
, "lengthFromThenTo" ~> TF TCLenFromThenTo
|
||||||
]
|
]
|
||||||
|
|
||||||
-- Built-in types from Array.cry
|
|
||||||
builtInArray = Map.fromList
|
|
||||||
[ "Array" ~> TC TCArray
|
|
||||||
]
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
@ -126,7 +120,6 @@ instance HasKind TC where
|
|||||||
TCInteger -> KType
|
TCInteger -> KType
|
||||||
TCRational -> KType
|
TCRational -> KType
|
||||||
TCIntMod -> KNum :-> KType
|
TCIntMod -> KNum :-> KType
|
||||||
TCArray -> KType :-> KType :-> KType
|
|
||||||
TCSeq -> KNum :-> KType :-> KType
|
TCSeq -> KNum :-> KType :-> KType
|
||||||
TCFun -> KType :-> KType :-> KType
|
TCFun -> KType :-> KType :-> KType
|
||||||
TCTuple n -> foldr (:->) KType (replicate n KType)
|
TCTuple n -> foldr (:->) KType (replicate n KType)
|
||||||
@ -209,7 +202,6 @@ data TC = TCNum Integer -- ^ Numbers
|
|||||||
| TCInteger -- ^ Integer
|
| TCInteger -- ^ Integer
|
||||||
| TCIntMod -- ^ @Z _@
|
| TCIntMod -- ^ @Z _@
|
||||||
| TCRational -- ^ @Rational@
|
| TCRational -- ^ @Rational@
|
||||||
| TCArray -- ^ @Array _ _@
|
|
||||||
| TCSeq -- ^ @[_] _@
|
| TCSeq -- ^ @[_] _@
|
||||||
| TCFun -- ^ @_ -> _@
|
| TCFun -- ^ @_ -> _@
|
||||||
| TCTuple Int -- ^ @(_, _, _)@
|
| TCTuple Int -- ^ @(_, _, _)@
|
||||||
@ -310,7 +302,6 @@ instance PP TC where
|
|||||||
TCInteger -> text "Integer"
|
TCInteger -> text "Integer"
|
||||||
TCIntMod -> text "Z"
|
TCIntMod -> text "Z"
|
||||||
TCRational -> text "Rational"
|
TCRational -> text "Rational"
|
||||||
TCArray -> text "Array"
|
|
||||||
TCSeq -> text "[]"
|
TCSeq -> text "[]"
|
||||||
TCFun -> text "(->)"
|
TCFun -> text "(->)"
|
||||||
TCTuple 0 -> text "()"
|
TCTuple 0 -> text "()"
|
||||||
|
@ -507,9 +507,6 @@ tRational = TCon (TC TCRational) []
|
|||||||
tIntMod :: Type -> Type
|
tIntMod :: Type -> Type
|
||||||
tIntMod n = TCon (TC TCIntMod) [n]
|
tIntMod n = TCon (TC TCIntMod) [n]
|
||||||
|
|
||||||
tArray :: Type -> Type -> Type
|
|
||||||
tArray a b = TCon (TC TCArray) [a, b]
|
|
||||||
|
|
||||||
tWord :: Type -> Type
|
tWord :: Type -> Type
|
||||||
tWord a = tSeq a tBit
|
tWord a = tSeq a tBit
|
||||||
|
|
||||||
|
@ -16,7 +16,6 @@ module Cryptol.Utils.Ident
|
|||||||
, modNameChunks
|
, modNameChunks
|
||||||
, packModName
|
, packModName
|
||||||
, preludeName
|
, preludeName
|
||||||
, arrayName
|
|
||||||
, interactiveName
|
, interactiveName
|
||||||
, noModuleName
|
, noModuleName
|
||||||
, exprModName
|
, exprModName
|
||||||
@ -101,9 +100,6 @@ modInstPref = "`"
|
|||||||
preludeName :: ModName
|
preludeName :: ModName
|
||||||
preludeName = packModName ["Cryptol"]
|
preludeName = packModName ["Cryptol"]
|
||||||
|
|
||||||
arrayName :: ModName
|
|
||||||
arrayName = packModName ["Array"]
|
|
||||||
|
|
||||||
interactiveName :: ModName
|
interactiveName :: ModName
|
||||||
interactiveName = packModName ["<interactive>"]
|
interactiveName = packModName ["<interactive>"]
|
||||||
|
|
||||||
|
@ -1,3 +0,0 @@
|
|||||||
:module Array
|
|
||||||
:browse Array
|
|
||||||
|
|
@ -1,20 +0,0 @@
|
|||||||
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
|
|
||||||
|
|
Loading…
Reference in New Issue
Block a user