Merge remote-tracking branch 'origin' into signed-arith

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,

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))
+
+
+
+
+
+
+
+
+

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

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

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] }
+
+
+
+

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
+
+
+

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)

examples/demote.cry

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

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
+

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] ]
+  

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
+
+*/

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
+
+

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
+

examples/width.cry

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

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

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

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

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)
 

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)
 

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
 

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

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))

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.