diff --git a/cryptol.cabal b/cryptol.cabal index 169fbba3..a559dba7 100644 --- a/cryptol.cabal +++ b/cryptol.cabal @@ -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, diff --git a/examples/HMAC.cry b/examples/HMAC.cry new file mode 100644 index 00000000..58378f45 --- /dev/null +++ b/examples/HMAC.cry @@ -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)) + + + + + + + + + diff --git a/examples/SHA256.cry b/examples/SHA256.cry new file mode 100644 index 00000000..36a663e2 --- /dev/null +++ b/examples/SHA256.cry @@ -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 \ No newline at end of file diff --git a/examples/append.cry b/examples/append.cry new file mode 100644 index 00000000..ccb7cd9b --- /dev/null +++ b/examples/append.cry @@ -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 diff --git a/examples/builtin_lifting.cry b/examples/builtin_lifting.cry new file mode 100644 index 00000000..aae8ee10 --- /dev/null +++ b/examples/builtin_lifting.cry @@ -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] } + + + + diff --git a/examples/builtins.cry b/examples/builtins.cry new file mode 100644 index 00000000..85e2061f --- /dev/null +++ b/examples/builtins.cry @@ -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 + + + diff --git a/examples/comp.cry b/examples/comp.cry new file mode 100644 index 00000000..23b14d12 --- /dev/null +++ b/examples/comp.cry @@ -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) diff --git a/examples/demote.cry b/examples/demote.cry new file mode 100644 index 00000000..bb01bbec --- /dev/null +++ b/examples/demote.cry @@ -0,0 +1,5 @@ +x : {a}(fin a) => [a] -> [(a*2)+3] +x v = 0 + 1 + +y = x (2 : [3]) + diff --git a/examples/inflist.cry b/examples/inflist.cry new file mode 100644 index 00000000..1b537f56 --- /dev/null +++ b/examples/inflist.cry @@ -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 + diff --git a/examples/mini.cry b/examples/mini.cry new file mode 100644 index 00000000..3e9bb1c8 --- /dev/null +++ b/examples/mini.cry @@ -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] ] + \ No newline at end of file diff --git a/examples/props.cry b/examples/props.cry new file mode 100644 index 00000000..9b1b5965 --- /dev/null +++ b/examples/props.cry @@ -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 + +*/ \ No newline at end of file diff --git a/examples/split.cry b/examples/split.cry new file mode 100644 index 00000000..b5212949 --- /dev/null +++ b/examples/split.cry @@ -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 + + diff --git a/examples/splitAt.cry b/examples/splitAt.cry new file mode 100644 index 00000000..5d389e94 --- /dev/null +++ b/examples/splitAt.cry @@ -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 + diff --git a/examples/width.cry b/examples/width.cry new file mode 100644 index 00000000..18dd248c --- /dev/null +++ b/examples/width.cry @@ -0,0 +1,2 @@ +x : [8] +x = width (252 : [8]) \ No newline at end of file diff --git a/examples/xor_cipher.cry b/examples/xor_cipher.cry new file mode 100644 index 00000000..c20b2273 --- /dev/null +++ b/examples/xor_cipher.cry @@ -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 \ No newline at end of file diff --git a/examples/zero_weird.cry b/examples/zero_weird.cry new file mode 100644 index 00000000..b9eef494 --- /dev/null +++ b/examples/zero_weird.cry @@ -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 diff --git a/src/Cryptol/ModuleSystem/Name.hs b/src/Cryptol/ModuleSystem/Name.hs index ed3ae643..2509feab 100644 --- a/src/Cryptol/ModuleSystem/Name.hs +++ b/src/Cryptol/ModuleSystem/Name.hs @@ -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 diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs index ce6da481..5c20c413 100644 --- a/src/Cryptol/Parser/AST.hs +++ b/src/Cryptol/Parser/AST.hs @@ -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 @@ -377,7 +377,7 @@ data Prop n = CFin (Type n) -- ^ @ fin x @ | CSignedCmp (Type n) -- ^ @ SignedCmp 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 @@ -904,7 +904,6 @@ instance NoPos Pragma where - instance NoPos (TySyn name) where noPos (TySyn x y z) = TySyn (noPos x) (noPos y) (noPos z) diff --git a/src/Cryptol/Parser/Position.hs b/src/Cryptol/Parser/Position.hs index 14edb916..33d1bc9a 100644 --- a/src/Cryptol/Parser/Position.hs +++ b/src/Cryptol/Parser/Position.hs @@ -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) diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index 4d4de33a..1deefe78 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -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 diff --git a/src/Cryptol/TypeCheck/AST.hs b/src/Cryptol/TypeCheck/AST.hs index d6d5cacf..a118a6bb 100644 --- a/src/Cryptol/TypeCheck/AST.hs +++ b/src/Cryptol/TypeCheck/AST.hs @@ -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 diff --git a/src/Cryptol/TypeCheck/Parseable.hs b/src/Cryptol/TypeCheck/Parseable.hs new file mode 100644 index 00000000..e04a4f59 --- /dev/null +++ b/src/Cryptol/TypeCheck/Parseable.hs @@ -0,0 +1,109 @@ +-- | +-- 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) + +instance (ShowParseable a) => ShowParseable [a] where + showParseable a = case a of + [] -> text "[]" + [x] -> brackets (showParseable x) + x : xs -> text "[" <+> showParseable x $$ + vcat [ comma <+> showParseable y | y <- xs ] $$ + text "]" + +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)) diff --git a/src/Cryptol/TypeCheck/Type.hs b/src/Cryptol/TypeCheck/Type.hs index f10ee8cc..a57aa6e3 100644 --- a/src/Cryptol/TypeCheck/Type.hs +++ b/src/Cryptol/TypeCheck/Type.hs @@ -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.