GaloisInc/cryptol
1
1
Fork 0
mirror of https://github.com/GaloisInc/cryptol.git synced 2024-11-30 23:45:23 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #440 from sliverdragon37/master

Browse Source 
Adds the :ast and :extract-coq commands for printing out a parseable AST
This commit is contained in:
Iavor S. Diatchki 2017-08-15 10:25:08 -07:00 committed by GitHub
commit ca2136fab9
23 changed files with 632 additions and 22 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
cryptol.cabal
View File

@ -114,6 +114,7 @@ library
Cryptol.TypeCheck.TypePat,
Cryptol.TypeCheck.SimpType,
Cryptol.TypeCheck.AST,
Cryptol.TypeCheck.Parseable,
Cryptol.TypeCheck.Monad,
Cryptol.TypeCheck.Infer,
Cryptol.TypeCheck.InferTypes,

72
examples/HMAC.cry Normal file
View File

@ -0,0 +1,72 @@
////////////////////////////////////////////////////////////////
// Copyright 2016 Galois, Inc. All Rights Reserved
//
// Authors:
// Aaron Tomb : atomb@galois.com
// Nathan Collins : conathan@galois.com
// Joey Dodds : jdodds@galois.com
//
// Licensed under the Apache License, Version 2.0 (the "License").
// You may not use this file except in compliance with the License.
// A copy of the License is located at
//
// http://aws.amazon.com/apache2.0
//
// or in the "license" file accompanying this file. This file is distributed
// on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either
// express or implied. See the License for the specific language governing
// permissions and limitations under the License.
//
////////////////////////////////////////////////////////////////
module HMAC where
import SHA256
//////// Functional version ////////
hmacSHA256 : {pwBytes, msgBytes}
(fin pwBytes, fin msgBytes
, 32 >= width msgBytes
, 64 >= width (8*pwBytes)
, 64 >= width (8 * (64 + msgBytes))
) => [pwBytes][8] -> [msgBytes][8] -> [256]
hmacSHA256 = hmac `{blockLength=64} SHA256 SHA256 SHA256
kinit : { pwBytes, blockLength, digest }
( fin pwBytes, fin blockLength, fin digest )
=> ([pwBytes][8] -> [8*digest])
-> [pwBytes][8]
-> [blockLength][8]
kinit hash key =
if `pwBytes > (`blockLength : [max (width pwBytes) (width blockLength)])
then take `{blockLength} (split (hash key) # (zero : [blockLength][8]))
else take `{blockLength} (key # (zero : [blockLength][8]))
// Due to limitations of the type system we must accept two
// separate arguments (both aledgedly the same) for two
// separate length inputs.
hmac : { msgBytes, pwBytes, digest, blockLength }
( fin pwBytes, fin digest, fin blockLength )
=> ([blockLength + msgBytes][8] -> [8*digest])
-> ([blockLength + digest][8] -> [8*digest])
-> ([pwBytes][8] -> [8*digest])
-> [pwBytes][8]
-> [msgBytes][8]
-> [digest*8]
hmac hash hash2 hash3 key message = hash2 (okey # internal)
where
ks : [blockLength][8]
ks = kinit hash3 key
okey = [k ^ 0x5C | k <- ks]
ikey = [k ^ 0x36 | k <- ks]
internal = split (hash (ikey # message))

194
examples/SHA256.cry Normal file
View File

@ -0,0 +1,194 @@
/*
* Copyright (c) 2013-2016 Galois, Inc.
* Distributed under the terms of the BSD3 license (see LICENSE file)
*
* @tmd - 24 April 2015 - took Ian's SHA512, converted to SHA256
* @ian - 15 August 2015 - he lies, probably ment 2014.
*
* This is a very simple implementation of SHA256, designed to be as clearly
* mathced to the specification in NIST's FIPS-PUB-180-4 as possible
*
* * The output correctly matches on all test vectors from
* http://csrc.nist.gov/groups/ST/toolkit/documents/Examples/SHA256.pdf
*/
module SHA256 where
/*
* SHA256 Functions : Section 4.1.2
*/
Ch : [32] -> [32] -> [32] -> [32]
Ch x y z = (x && y) ^ (~x && z)
Maj : [32] -> [32] -> [32] -> [32]
Maj x y z = (x && y) ^ (x && z) ^ (y && z)
S0 : [32] -> [32]
S0 x = (x >>> 2) ^ (x >>> 13) ^ (x >>> 22)
S1 : [32] -> [32]
S1 x = (x >>> 6) ^ (x >>> 11) ^ (x >>> 25)
s0 : [32] -> [32]
s0 x = (x >>> 7) ^ (x >>> 18) ^ (x >> 3)
s1 : [32] -> [32]
s1 x = (x >>> 17) ^ (x >>> 19) ^ (x >> 10)
/*
* SHA256 Constants : Section 4.2.2
*/
K : [64][32]
K = [ 0x428a2f98, 0x71374491, 0xb5c0fbcf, 0xe9b5dba5, 0x3956c25b, 0x59f111f1, 0x923f82a4, 0xab1c5ed5,
0xd807aa98, 0x12835b01, 0x243185be, 0x550c7dc3, 0x72be5d74, 0x80deb1fe, 0x9bdc06a7, 0xc19bf174,
0xe49b69c1, 0xefbe4786, 0x0fc19dc6, 0x240ca1cc, 0x2de92c6f, 0x4a7484aa, 0x5cb0a9dc, 0x76f988da,
0x983e5152, 0xa831c66d, 0xb00327c8, 0xbf597fc7, 0xc6e00bf3, 0xd5a79147, 0x06ca6351, 0x14292967,
0x27b70a85, 0x2e1b2138, 0x4d2c6dfc, 0x53380d13, 0x650a7354, 0x766a0abb, 0x81c2c92e, 0x92722c85,
0xa2bfe8a1, 0xa81a664b, 0xc24b8b70, 0xc76c51a3, 0xd192e819, 0xd6990624, 0xf40e3585, 0x106aa070,
0x19a4c116, 0x1e376c08, 0x2748774c, 0x34b0bcb5, 0x391c0cb3, 0x4ed8aa4a, 0x5b9cca4f, 0x682e6ff3,
0x748f82ee, 0x78a5636f, 0x84c87814, 0x8cc70208, 0x90befffa, 0xa4506ceb, 0xbef9a3f7, 0xc67178f2
]
/*
* Preprocessing (padding and parsing) for SHA256 : Section 5.1.1 and 5.2.1
*/
preprocess : {msgLen,contentLen,chunks,padding}
( fin msgLen
, 64 >= width msgLen // message width fits in a word
, contentLen == msgLen + 65 // message + header
, chunks == (contentLen+511) / 512
, padding == (512 - contentLen % 512) % 512 // prettier if type #'s could be < 0
)
=> [msgLen] -> [chunks][512]
preprocess msg = split (msg # [True] # (zero:[padding]) # (`msgLen:[64]))
/*
* SHA256 Initial Hash Value : Section 5.3.3
*/
H0 : [8][32]
H0 = [ 0x6a09e667, 0xbb67ae85, 0x3c6ef372, 0xa54ff53a,
0x510e527f, 0x9b05688c, 0x1f83d9ab, 0x5be0cd19]
/*
* The SHA256 Hash computation : Section 6.2.2
*
* We have split the computation into a message scheduling function, corresponding
* to step 1 in the documents loop, and a compression function, corresponding to steps 2-4.
*/
SHA256MessageSchedule : [16][32] -> [64][32]
SHA256MessageSchedule M = W where
W = M # [ s1 (W@(j-2)) + (W@(j-7)) + s0 (W@(j-15)) + (W@(j-16)) | j <- [16 .. 63]:[_][8] ]
SHA256Compress : [8][32] -> [64][32] -> [8][32]
SHA256Compress H W = [as!0 + H@0, bs!0 + H@1, cs!0 + H@2, ds!0 + H@3, es!0 + H@4, fs!0 + H@5, gs!0 + H@6, hs!0 + H@7] where
T1 = [h + S1 e + Ch e f g + k + w | h <- hs | e <- es | f <- fs | g <- gs | k <- K | w <- W]
T2 = [S0 a + Maj a b c | a <- as | b <- bs | c <- cs]
hs = take `{65} ([H@7] # gs)
gs = take `{65} ([H@6] # fs)
fs = take `{65} ([H@5] # es)
es = take `{65} ([H@4] # [d + t1 | d <- ds | t1 <- T1])
ds = take `{65} ([H@3] # cs)
cs = take `{65} ([H@2] # bs)
bs = take `{65} ([H@1] # as)
as = take `{65} ([H@0] # [t1 + t2 | t1 <- T1 | t2 <- T2])
SHA256Block : [8][32] -> [16][32] -> [8][32]
SHA256Block H M = SHA256Compress H (SHA256MessageSchedule M)
//////// Functional/idiomatic top level ////////
/*
* The SHA256' function hashes a preprocessed sequence of blocks with the
* compression function. The SHA256 function hashes a sequence of bytes, and
* is more likely the function that will be similar to those seein in an
* implementation to be verified.
*/
SHA256' : {a} (fin a) => [a][16][32] -> [8][32]
SHA256' blocks = hash!0 where
hash = [H0] # [SHA256Block h b | h <- hash | b <- blocks]
SHA256 : {a} (fin a, 64 >= width (8*a)) => [a][8] -> [256]
SHA256 msg = join (SHA256' [ split x | x <- preprocess(join msg)])
property katsPass = ~zero == [test == kat | (test,kat) <- kats ]
kats = [ (SHA256 "abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq"
, 0x248d6a61d20638b8e5c026930c3e6039a33ce45964ff2167f6ecedd419db06c1)
, (SHA256 ""
,0xe3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855)
, (SHA256 "abcdefghbcdefghicdefghijdefghijkefghijklfghijklmghijklmnhijklmnoijklmnopjklmnopqklmnopqrlmnopqrsmnopqrstnopqrstu"
, 0xcf5b16a778af8380036ce59e7b0492370b249b11e8f07a51afac45037afee9d1)
// , ([0x61 | i <- [1..1000000] : [_][32]]
// , 0xcdc76e5c9914fb9281a1c7e284d73e67f1809a48a497200e046d39ccc7112cd0)
]
//////// Imperative top level ////////
type SHA256State = { h : [8][32]
, block : [64][8]
, n : [16]
, sz : [64]
}
SHA256Init : SHA256State
SHA256Init = { h = H0
, block = zero
, n = 0
, sz = 0
}
SHA256Update1 : SHA256State -> [8] -> SHA256State
SHA256Update1 s b =
if s.n == 64
then { h = SHA256Block s.h (split (join s.block))
, block = [b] # zero
, n = 1
, sz = s.sz + 8
}
else { h = s.h
, block = update s.block s.n b
, n = s.n + 1
, sz = s.sz + 8
}
SHA256Update : {n} (fin n) => SHA256State -> [n][8] -> SHA256State
SHA256Update sinit bs = ss!0
where ss = [sinit] # [ SHA256Update1 s b | s <- ss | b <- bs ]
update : {a, b, c} (fin c, c >= width (2 ^^ c - 1)) => [b]a -> [c] -> a -> [min b (2 ^^ c)]a
update a i x = [ if j == i then x else e | e <- a | j <- [0 ..] ]
// Add padding and size and process the final block.
SHA256Final : SHA256State -> [256]
SHA256Final s = join (SHA256Block h b')
// Because the message is always made up of bytes, and the size is a
// fixed number of bytes, the 1 pad will always be at least a byte.
where s' = SHA256Update1 s 0x80
// Don't need to add zeros. They're already there. Just update
// the count of bytes in this block. After adding the 1 pad, there
// are two possible cases: the size will fit in the current block,
// or it won't.
(h, b) = if s'.n <= 56 then (s'.h, s'.block)
else (SHA256Block s'.h (split (join s'.block)), zero)
b' = split (join b || (zero # s.sz))
SHA256Imp : {a} (64 >= width (8*a)) => [a][8] -> [256]
SHA256Imp msg = SHA256Final (SHA256Update SHA256Init msg)
property katsPassImp = ~zero == [test == kat | (test,kat) <- katsImp ]
katsImp = [ (SHA256Imp "abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq", 0x248d6a61d20638b8e5c026930c3e6039a33ce45964ff2167f6ecedd419db06c1), (SHA256Imp ""
, 0xe3b0c44298fc1c149afbf4c8996fb92427ae41e4649b934ca495991b7852b855)
, (SHA256Imp "abcdefghbcdefghicdefghijdefghijkefghijklfghijklmghijklmnhijklmnoijklmnopjklmnopqklmnopqrlmnopqrsmnopqrstnopqrstu"
, 0xcf5b16a778af8380036ce59e7b0492370b249b11e8f07a51afac45037afee9d1)
// , ([0x61 | i <- [1..1000000] : [_][32]]
// , 0xcdc76e5c9914fb9281a1c7e284d73e67f1809a48a497200e046d39ccc7112cd0)
]
property imp_correct msg = SHA256 msg == SHA256Imp msg

13
examples/append.cry Normal file
View File

@ -0,0 +1,13 @@
x : [_][8]
x = [1,2,3,4,5,19,12,38,5,3]
y : [_][8]
y = [19,3,27,5,12]
z = x # y
m = z @ (0 : [1]) //1
w = z @ 2 //3
t = z @ 10 //19 (0x13)
v = z @ 11 //3

48
examples/builtin_lifting.cry Normal file
View File

@ -0,0 +1,48 @@
//builtins lift over tuples, seqs, and records
//this file uses addition to model a builtin
//but this should work for any builtin operators
x = [True,False]
y = [False,True]
//make sure bitvectors are numbers
property p1 = x == (2 : [2])
//same thing written 2 different ways
property p2 = x + y == 3
property p3 = x + y == [True,True]
xx = [[True,False]]
yy = [[False,True]]
//addition lifts pointwise over sequences
property p4 = xx + yy == [3]
//negation is a unary operator that also lifts over sequences
property p5 = ~ xx == yy
xinf = [2 ... ]
yinf = [3 ... ]
//addition lifts pointwise over infinite lists
property p6 = (xinf + yinf) @ (0 : [0]) == (1 : [2])
//negation lifts pointwise over an infinite list
property p7 = (~ xinf) @ (0 : [0]) == (1 : [2])
xrec = { x = 2 : [2], y = 2 : [2] } : {x : [2], y : [2]}
property p8 = xrec + xrec + xrec == xrec
//lift over tuples and records at the same time
property p9 = (2,2,xrec) + (2,2,xrec) + (2,2,xrec) == (2:[2],2:[2],xrec)
//lift unary over tuples and lists
property p10 = (~ { x = (1,2), y = [3,4,5] }) == {x = (0:[1],1:[2]), y = [4, 3, 2] : [3][3] }

38
examples/builtins.cry Normal file
View File

@ -0,0 +1,38 @@
//Here's a test of some builtin operators
//nothing too deep, just making sure they all work out
t : [8]
t = if True then 5 else 4 //5
f : [8]
f = if False then 3 else 5 //5
times : [8]
times = 5 * 1 * 2 * 3 //30
div : [8]
div = (((30/1)/2)/3) //5
mod : [8]
mod = 205%10 //5
exp : [8]
exp = 2^^7 //128
lgtest : [8]
lgtest = lg2 128 //7
p : [8]
p = 3+2 //5
m : [8]
m = 8-3 //5
neg : [8]
neg = -(-5) //5
comp : [8]
comp = ~250 //5

10
examples/comp.cry Normal file
View File

@ -0,0 +1,10 @@
x : [_]([2],[3],[3],[4])
x = [(a,b,c,d) | a <- [1,2], b <- [3,4] | c <- [5,6], d <- [7,8,9] ]
property t1 = x @ 0 == (1,3,5,7)
property t2 = x @ 2 == (2,3,5,9)
property t3 = x @ 3 == (2,4,6,7)
y = [(a,b,c) | a <- [1,2,3], b <- [1,2] | c <- [1 ... ] ]
property t4 = y @ 3 == (2,2,0)

5
examples/demote.cry Normal file
View File

@ -0,0 +1,5 @@
x : {a}(fin a) => [a] -> [(a*2)+3]
x v = 0 + 1
y = x (2 : [3])

10
examples/inflist.cry Normal file
View File

@ -0,0 +1,10 @@
a = [1 ... ]
b = [1,2 ... ]
c = [1 .. 5]
d = [1,3 .. 9]
property t1 = a @ 3 == 1
property t2 = b @ 3 == 1
property t3 = c @ 3 == 4
property t4 = d @ 3 == 4

28
examples/mini.cry Normal file
View File

@ -0,0 +1,28 @@
id : [32] -> [32]
id x = rec x
where rec k = if (k == 0) then 0 else 1 + rec (k + (-1))
inflist = [1 ... ] : [_][8]
rc = {x = 3 : [8], y = 5 : [8]}
my_true = rc.x
tup = (1 : [8], 2 : [8], 3 : [8], 4 : [8])
my_3 = tup.2
sup = y where y = 3 : [8]
gf28Add : {n} (fin n) => [n][8] -> [8]
gf28Add ps = sums ! 0
where sums = [zero] # [ p ^ s | p <- ps | s <- sums ]
gex = gf28Add [1,2]
sum : [_][8] -> [_][8]
sum x = rec
where rec = [ p + q | p <- x | q <- [1,2,3,4] ]

27
examples/props.cry Normal file
View File

@ -0,0 +1,27 @@
x = [True, False]
y = [False, True]
z = x + y
property p1 = z == 3
xx = [[True,False]]
yy = [[False, True]]
zz = xx + yy
t : {a} [a*3] -> [a*3][a*3]
t d = zero
/*
t1 : [8] -> [2][2][2]
t1 x = split (split x)
t2 : [8] -> ([4],[4])
t2 x = splitAt x
t3 : [8] ->[8] -> [16]
t3 x y = x # y
*/

10
examples/split.cry Normal file
View File

@ -0,0 +1,10 @@
x = [1,2,3,4] : [_][8]
y = (split x) : [2][2][8]
a = (y@0) @ 0
b = (y@0) @ 1
c = (y@1) @ 0
d = (y@1) @ 1

9
examples/splitAt.cry Normal file
View File

@ -0,0 +1,9 @@
x = [1,2,3,4] : [_][8]
y = (splitAt x) : ([2][8],[2][8])
a = y.0 @ 0
b = y.0 @ 1
c = y.1 @ 0
d = y.1 @ 1

2
examples/width.cry Normal file
View File

@ -0,0 +1,2 @@
x : [8]
x = width (252 : [8])

7
examples/xor_cipher.cry Normal file
View File

@ -0,0 +1,7 @@
encrypt : {a}(fin a) => [8] -> [a][8] -> [a][8]
encrypt key plaintext = [pt ^ key | pt <- plaintext ]
decrypt : {a}(fin a) => [8] -> [a][8] -> [a][8]
decrypt key ciphertext = [ct ^ key | ct <- ciphertext ]
property roundtrip k ip = decrypt k (encrypt k ip) == ip

12
examples/zero_weird.cry Normal file
View File

@ -0,0 +1,12 @@
x : {a}() => a -> [16]
x v = zero v
property xprop v = x v == 0
y : [12] -> [4] -> [17]
y a b = zero a b
property yprop v w = y v w == 0
t1 = x 13
t2 = y 2 3

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

@ -88,7 +88,8 @@ data Name = Name { nUnique :: {-# UNPACK #-} !Int
, nLoc :: !Range
-- ^ Where this name was defined
} deriving (Show, Generic, NFData)
} deriving (Generic, NFData, Show)
instance Eq Name where
a == b = compare a b == EQ

28
src/Cryptol/Parser/AST.hs
View File

@ -131,7 +131,7 @@ data Decl name = DSignature [Located name] (Schema name)
| DPatBind (Pattern name) (Expr name)
| DType (TySyn name)
| DLocated (Decl name) Range
deriving (Eq, Show, Generic, NFData)
deriving (Eq, Show, Generic, NFData, Functor)
-- | An import declaration.
data Import = Import { iModule :: !ModName
@ -149,7 +149,7 @@ data ImportSpec = Hiding [Ident]
deriving (Eq, Show, Generic, NFData)
data TySyn n = TySyn (Located n) [TParam n] (Type n)
deriving (Eq, Show, Generic, NFData)
deriving (Eq, Show, Generic, NFData, Functor)
{- | Bindings. Notes:
@ -172,17 +172,17 @@ data Bind name = Bind { bName :: Located name -- ^ Defined thing
, bPragmas :: [Pragma] -- ^ Optional pragmas
, bMono :: Bool -- ^ Is this a monomorphic binding
, bDoc :: Maybe String -- ^ Optional doc string
} deriving (Eq, Show, Generic, NFData)
} deriving (Eq, Generic, NFData, Functor, Show)
type LBindDef = Located (BindDef PName)
data BindDef name = DPrim
| DExpr (Expr name)
deriving (Eq, Show, Generic, NFData)
deriving (Eq, Show, Generic, NFData, Functor)
data Fixity = Fixity { fAssoc :: !Assoc
, fLevel :: !Int
} deriving (Eq, Show, Generic, NFData)
} deriving (Eq, Generic, NFData, Show)
data FixityCmp = FCError
| FCLeft
@ -293,11 +293,11 @@ data Expr n = EVar n -- ^ @ x @
| EParens (Expr n) -- ^ @ (e) @ (Removed by Fixity)
| EInfix (Expr n) (Located n) Fixity (Expr n)-- ^ @ a + b @ (Removed by Fixity)
deriving (Eq, Show, Generic, NFData)
deriving (Eq, Show, Generic, NFData, Functor)
data TypeInst name = NamedInst (Named (Type name))
| PosInst (Type name)
deriving (Eq, Show, Generic, NFData)
deriving (Eq, Show, Generic, NFData, Functor)
{- | Selectors are used for projecting from various components.
Each selector has an option spec to specify the shape of the thing
@ -320,7 +320,7 @@ data Selector = TupleSel Int (Maybe Int)
data Match name = Match (Pattern name) (Expr name) -- ^ p <- e
| MatchLet (Bind name)
deriving (Eq, Show, Generic, NFData)
deriving (Eq, Show, Generic, NFData, Functor)
data Pattern n = PVar (Located n) -- ^ @ x @
| PWild -- ^ @ _ @
@ -330,13 +330,13 @@ data Pattern n = PVar (Located n) -- ^ @ x @
| PTyped (Pattern n) (Type n) -- ^ @ x : [8] @
| PSplit (Pattern n) (Pattern n)-- ^ @ (x # y) @
| PLocated (Pattern n) Range -- ^ Location information
deriving (Eq, Show, Generic, NFData)
deriving (Eq, Show, Generic, NFData, Functor)
data Named a = Named { name :: Located Ident, value :: a }
deriving (Eq, Show, Foldable, Traversable, Generic, NFData, Functor)
data Schema n = Forall [TParam n] [Prop n] (Type n) (Maybe Range)
deriving (Eq, Show, Generic, NFData)
deriving (Eq, Show, Generic, NFData, Functor)
data Kind = KNum | KType
deriving (Eq, Show, Generic, NFData)
@ -345,7 +345,7 @@ data TParam n = TParam { tpName :: n
, tpKind :: Maybe Kind
, tpRange :: Maybe Range
}
deriving (Eq, Show, Generic, NFData)
deriving (Eq, Show, Generic, NFData, Functor)
data Type n = TFun (Type n) (Type n) -- ^ @[8] -> [8]@
| TSeq (Type n) (Type n) -- ^ @[8] a@
@ -361,7 +361,7 @@ data Type n = TFun (Type n) (Type n) -- ^ @[8] -> [8]@
| TLocated (Type n) Range -- ^ Location information
| TParens (Type n) -- ^ @ (ty) @
| TInfix (Type n) (Located n) Fixity (Type n) -- ^ @ ty + ty @
deriving (Eq, Show, Generic, NFData)
deriving (Eq, Show, Generic, NFData, Functor)
tconNames :: Map.Map PName (Type PName)
tconNames = Map.fromList
@ -376,7 +376,7 @@ data Prop n = CFin (Type n) -- ^ @ fin x @
| CCmp (Type n) -- ^ @ Cmp a @
| CLocated (Prop n) Range -- ^ Location information
| CType (Type n) -- ^ After parsing
deriving (Eq, Show, Generic, NFData)
deriving (Eq, Show, Generic, NFData, Functor)
--------------------------------------------------------------------------------
-- Note: When an explicit location is missing, we could use the sub-components
@ -902,7 +902,6 @@ instance NoPos Pragma where
instance NoPos (TySyn name) where
noPos (TySyn x y z) = TySyn (noPos x) (noPos y) (noPos z)
@ -985,4 +984,3 @@ instance NoPos (Prop name) where
CLocated c _ -> noPos c
CType t -> CType (noPos t)

1
src/Cryptol/Parser/Position.hs
View File

@ -24,6 +24,7 @@ import Cryptol.Utils.PP
data Located a = Located { srcRange :: !Range, thing :: !a }
deriving (Eq, Show, Generic, NFData)
data Position = Position { line :: !Int, col :: !Int }
deriving (Eq, Ord, Show, Generic, NFData)

17
src/Cryptol/REPL/Command.hs
View File

@ -55,6 +55,7 @@ import qualified Cryptol.ModuleSystem.Name as M
import qualified Cryptol.ModuleSystem.NamingEnv as M
import qualified Cryptol.ModuleSystem.Renamer as M (RenamerWarning(SymbolShadowed))
import qualified Cryptol.Utils.Ident as M
import qualified Cryptol.ModuleSystem.Env as M
import qualified Cryptol.Eval.Monad as E
import qualified Cryptol.Eval.Value as E
@ -65,6 +66,7 @@ import Cryptol.Parser
(parseExprWith,parseReplWith,ParseError(),Config(..),defaultConfig
,parseModName,parseHelpName)
import qualified Cryptol.TypeCheck.AST as T
import qualified Cryptol.TypeCheck.Parseable as T
import qualified Cryptol.TypeCheck.Subst as T
import qualified Cryptol.TypeCheck.InferTypes as T
import Cryptol.TypeCheck.Solve(defaultReplExpr)
@ -184,6 +186,10 @@ nbCommandList =
"do type specialization on a closed expression"
, CommandDescr [ ":eval" ] (ExprArg refEvalCmd)
"evaluate an expression with the reference evaluator"
, CommandDescr [ ":ast" ] (ExprArg astOfCmd)
"print out the pre-typechecked AST of a given term"
, CommandDescr [ ":extract-coq" ] (NoArg allTerms)
"print out the post-typechecked AST of all currently defined terms, in a Coq parseable format"
]
commandList :: [CommandDescr]
@ -581,6 +587,17 @@ refEvalCmd str = do
val <- liftModuleCmd (rethrowEvalError . R.evaluate expr)
rPrint $ R.ppValue val
astOfCmd :: String -> REPL ()
astOfCmd str = do
expr <- replParseExpr str
(re,_,_) <- replCheckExpr (P.noPos expr)
rPrint (fmap M.nameUnique re)
allTerms :: REPL ()
allTerms = do
me <- getModuleEnv
rPrint $ T.showParseable $ concatMap T.mDecls $ M.loadedModules me
typeOfCmd :: String -> REPL ()
typeOfCmd str = do

12
src/Cryptol/TypeCheck/AST.hs
View File

@ -33,7 +33,7 @@ import Cryptol.Prims.Syntax
import Cryptol.Parser.AST ( Selector(..),Pragma(..)
, Import(..), ImportSpec(..), ExportType(..)
, ExportSpec(..), isExportedBind
, isExportedType, Fixity(..) )
, isExportedType, Fixity(..))
import Cryptol.Utils.Ident (Ident,isInfixIdent,ModName,packIdent)
import Cryptol.TypeCheck.PP
import Cryptol.TypeCheck.Type
@ -44,6 +44,9 @@ import Control.DeepSeq
import Data.Map (Map)
import qualified Data.IntMap as IntMap
-- | A Cryptol module.
data Module = Module { mName :: !ModName
, mExports :: ExportSpec Name
@ -54,7 +57,6 @@ data Module = Module { mName :: !ModName
} deriving (Show, Generic, NFData)
data Expr = EList [Expr] Type -- ^ List value (with type of elements)
| ETuple [Expr] -- ^ Tuple value
| ERec [(Ident,Expr)] -- ^ Record value
@ -112,6 +114,7 @@ groupDecls dg = case dg of
Recursive ds -> ds
NonRecursive d -> [d]
data Decl = Decl { dName :: !Name
, dSignature :: Schema
, dDefinition :: DeclDef
@ -119,16 +122,15 @@ data Decl = Decl { dName :: !Name
, dInfix :: !Bool
, dFixity :: Maybe Fixity
, dDoc :: Maybe String
} deriving (Show, Generic, NFData)
} deriving (Generic, NFData, Show)
data DeclDef = DPrim
| DExpr Expr
deriving (Show, Generic, NFData)
--------------------------------------------------------------------------------
-- | Construct a primitive, given a map to the unique names of the Cryptol
-- module.
ePrim :: PrimMap -> Ident -> Expr

105
src/Cryptol/TypeCheck/Parseable.hs Normal file
View File

@ -0,0 +1,105 @@
-- |
-- Module : $Header$
-- Copyright : (c) 2013-2017 Galois, Inc.
-- License : BSD3
-- Maintainer : cryptol@galois.com
-- Stability : provisional
-- Portability : portable
{-# LANGUAGE Safe #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
{-# LANGUAGE DeriveAnyClass, DeriveGeneric #-}
module Cryptol.TypeCheck.Parseable
( module Cryptol.TypeCheck.Parseable
, ShowParseable(..)
) where
import Cryptol.TypeCheck.AST
import Cryptol.Utils.Ident (Ident,unpackIdent)
import Cryptol.Parser.AST ( Located(..))
import Cryptol.ModuleSystem.Name
import Text.PrettyPrint
-- ShowParseable prints out a cryptol program in a way that it's parseable by Coq (and likely other things)
-- Used mainly for reasoning about the semantics of cryptol programs in Coq (https://github.com/GaloisInc/cryptol-semantics)
class ShowParseable t where
showParseable :: t -> Doc
instance ShowParseable Expr where
showParseable (EList es _) = parens (text "EList" <+> showParseable es)
showParseable (ETuple es) = parens (text "ETuple" <+> showParseable es)
showParseable (ERec ides) = parens (text "ERec" <+> showParseable ides)
showParseable (ESel e s) = parens (text "ESel" <+> showParseable e <+> showParseable s)
showParseable (EIf c t f) = parens (text "EIf" <+> showParseable c <+> showParseable t <+> showParseable f)
showParseable (EComp _ _ e mss) = parens (text "EComp" <+> showParseable e <+> showParseable mss)
showParseable (EVar n) = parens (text "EVar" <+> showParseable n)
showParseable (EApp fe ae) = parens (text "EApp" <+> showParseable fe <+> showParseable ae)
showParseable (EAbs n _ e) = parens (text "EAbs" <+> showParseable n <+> showParseable e)
showParseable (EWhere e dclg) = parens (text "EWhere" <+> showParseable e <+> showParseable dclg)
showParseable (ETAbs tp e) = parens (text "ETAbs" <+> showParseable tp <+> showParseable e)
showParseable (ETApp e t) = parens (text "ETApp" <+> showParseable e <+> parens (text "ETyp" <+> showParseable t))
--NOTE: erase all "proofs" for now (change the following two lines to change that)
showParseable (EProofAbs {-p-}_ e) = showParseable e --"(EProofAbs " ++ show p ++ showParseable e ++ ")"
showParseable (EProofApp e) = showParseable e --"(EProofApp " ++ showParseable e ++ ")"
instance (ShowParseable a, ShowParseable b) => ShowParseable (a,b) where
showParseable (x,y) = parens (showParseable x <> comma <> showParseable y)
instance ShowParseable Int where
showParseable i = int i
instance ShowParseable Ident where
showParseable i = text $ show $ unpackIdent i
instance ShowParseable Type where
showParseable (TUser n lt t) = parens (text "TUser" <+> showParseable n <+> showParseable lt <+> showParseable t)
showParseable (TRec lidt) = parens (text "TRec" <+> showParseable lidt)
showParseable t = parens $ text $ show t
instance ShowParseable Selector where
showParseable (TupleSel n _) = parens (text "TupleSel" <+> showParseable n)
showParseable (RecordSel n _) = parens (text "RecordSel" <+> showParseable n)
showParseable (ListSel n _) = parens (text "ListSel" <+> showParseable n)
instance ShowParseable Match where
showParseable (From n _ _ e) = parens (text "From" <+> showParseable n <+> showParseable e)
showParseable (Let d) = parens (text "MLet" <+> showParseable d)
instance ShowParseable Decl where
showParseable d = parens (text "Decl" <+> showParseable (dName d) <+> showParseable (dDefinition d))
instance ShowParseable DeclDef where
showParseable DPrim = text (show DPrim)
showParseable (DExpr e) = parens (text "DExpr" <+> showParseable e)
instance ShowParseable DeclGroup where
showParseable (Recursive ds) = parens (text "Recursive" <+> showParseable ds)
showParseable (NonRecursive d) = parens (text "NonRecursive" <+> showParseable d)
showParseableList :: (ShowParseable a) => [a] -> Doc
showParseableList [] = empty
showParseableList [x] = showParseable x
showParseableList (x : y) = (showParseable x) <> comma <> showParseableList y
instance (ShowParseable a) => ShowParseable [a] where
showParseable a = brackets $ showParseableList a
instance (ShowParseable a) => ShowParseable (Maybe a) where
showParseable Nothing = text "(0,\"\")" --empty ident, won't shadow demote
showParseable (Just x) = showParseable x
instance (ShowParseable a) => ShowParseable (Located a) where
showParseable l = showParseable (thing l)
instance ShowParseable TParam where
showParseable tp = parens (text (show (tpUnique tp)) <> comma <> maybeNameDoc (tpName tp))
maybeNameDoc :: Maybe Name -> Doc
maybeNameDoc Nothing = doubleQuotes empty
maybeNameDoc (Just n) = showParseable (nameIdent n)
instance ShowParseable Name where
showParseable n = parens (text (show (nameUnique n)) <> comma <> showParseable (nameIdent n))

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

@ -45,7 +45,7 @@ data TParam = TParam { tpUnique :: !Int -- ^ Parameter identifier
, tpKind :: Kind -- ^ Kind of parameter
, tpName :: Maybe Name -- ^ Name from source, if any.
}
deriving (Show, Generic, NFData)
deriving (Generic, NFData, Show)
-- | The internal representation of types.