diff --git a/LICENSE b/LICENSE index c3281ac4..833c98de 100644 --- a/LICENSE +++ b/LICENSE @@ -1,4 +1,4 @@ -Copyright (c) 2013-2015 Galois Inc. +Copyright (c) 2013-2016 Galois Inc. All rights reserved. Redistribution and use in source and binary forms, with or without diff --git a/LICENSE.rtf b/LICENSE.rtf index 429233b5..2ca3930d 100644 --- a/LICENSE.rtf +++ b/LICENSE.rtf @@ -4,7 +4,7 @@ \margl1440\margr1440\vieww12600\viewh7800\viewkind0 \pard\tx720\tx1440\tx2160\tx2880\tx3600\tx4320\tx5040\tx5760\tx6480\tx7200\tx7920\tx8640\pardirnatural -\f0\fs24 \cf0 Copyright (c) 2013-2015 Galois Inc.\ +\f0\fs24 \cf0 Copyright (c) 2013-2016 Galois Inc.\ All rights reserved.\ \ Redistribution and use in source and binary forms, with or without\ diff --git a/README.md b/README.md index 729f51cf..7c6ee04e 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,6 @@ # Cryptol, version 2 - This version of Cryptol is (C) 2013-2015 Galois, Inc., and + This version of Cryptol is (C) 2013-2016 Galois, Inc., and distributed under a standard, three-clause BSD license. Please see the file LICENSE, distributed with this software, for specific terms and conditions. diff --git a/Setup.hs b/Setup.hs index 9a3e1ef0..b957e6f3 100644 --- a/Setup.hs +++ b/Setup.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/bench/Main.hs b/bench/Main.hs index 2922e0a4..a9823366 100644 --- a/bench/Main.hs +++ b/bench/Main.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2015 Galois, Inc. +-- Copyright : (c) 2015-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/bench/data/ZUC.cry b/bench/data/ZUC.cry index 0ee2c0c6..5633a423 100644 --- a/bench/data/ZUC.cry +++ b/bench/data/ZUC.cry @@ -1,4 +1,4 @@ -// Copyright (c) 2011-2015 Galois, Inc. +// Copyright (c) 2011-2016 Galois, Inc. // An implementation of ZUC, Version 1.5 // Version info: If the following variable is set to True, then we implement diff --git a/cryptol-server/Cryptol/Aeson.hs b/cryptol-server/Cryptol/Aeson.hs index 452cf4cd..f688ea94 100644 --- a/cryptol-server/Cryptol/Aeson.hs +++ b/cryptol-server/Cryptol/Aeson.hs @@ -1,13 +1,22 @@ +-- | +-- Module : $Header$ +-- Copyright : (c) 2015-2016 Galois, Inc. +-- License : BSD3 +-- Maintainer : cryptol@galois.com +-- Stability : provisional +-- Portability : portable +-- +-- Orphan 'FromJSON' and 'ToJSON' instances for certain Cryptol +-- types. Since these are meant to be consumed over a wire, they are +-- mostly focused on base values and interfaces rather than a full +-- serialization of internal ASTs and such. + {-# LANGUAGE ExtendedDefaultRules #-} {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE RecordWildCards #-} {-# OPTIONS_GHC -Wall -fno-warn-orphans -fno-warn-type-defaults #-} --- | Orphan 'FromJSON' and 'ToJSON' instances for certain Cryptol --- types. Since these are meant to be consumed over a wire, they are --- mostly focused on base values and interfaces rather than a full --- serialization of internal ASTs and such. module Cryptol.Aeson where import Control.Applicative diff --git a/cryptol-server/Main.hs b/cryptol-server/Main.hs index 88ca7197..21e90d6a 100644 --- a/cryptol-server/Main.hs +++ b/cryptol-server/Main.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2015 Galois, Inc. +-- Copyright : (c) 2015-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/cryptol.cabal b/cryptol.cabal index 383a117b..d33952c8 100644 --- a/cryptol.cabal +++ b/cryptol.cabal @@ -8,7 +8,7 @@ Author: Galois, Inc. Maintainer: cryptol@galois.com Homepage: http://www.cryptol.net/ Bug-reports: https://github.com/GaloisInc/cryptol/issues -Copyright: 2013-2015 Galois Inc. +Copyright: 2013-2016 Galois Inc. Category: Language Build-type: Simple Cabal-version: >= 1.18 diff --git a/cryptol/Main.hs b/cryptol/Main.hs index 85e2b936..87cf739c 100644 --- a/cryptol/Main.hs +++ b/cryptol/Main.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/cryptol/OptParser.hs b/cryptol/OptParser.hs index 57136a33..50082677 100644 --- a/cryptol/OptParser.hs +++ b/cryptol/OptParser.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/cryptol/REPL/Haskeline.hs b/cryptol/REPL/Haskeline.hs index 929ba082..1c0fcbf1 100644 --- a/cryptol/REPL/Haskeline.hs +++ b/cryptol/REPL/Haskeline.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/cryptol/REPL/Logo.hs b/cryptol/REPL/Logo.hs index fef87b0a..5199bc45 100644 --- a/cryptol/REPL/Logo.hs +++ b/cryptol/REPL/Logo.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/docs/ProgrammingCryptol/enigma/Enigma.cry b/docs/ProgrammingCryptol/enigma/Enigma.cry index addf27be..cddbfeb0 100644 --- a/docs/ProgrammingCryptol/enigma/Enigma.cry +++ b/docs/ProgrammingCryptol/enigma/Enigma.cry @@ -1,5 +1,5 @@ // Cryptol Enigma Simulator -// Copyright (c) 2010-2015, Galois Inc. +// Copyright (c) 2010-2016, Galois Inc. // www.cryptol.net // You can freely use this source code for educational purposes. diff --git a/docs/ProgrammingCryptol/enigma/Finite.cry b/docs/ProgrammingCryptol/enigma/Finite.cry index 580318de..19e63e32 100644 --- a/docs/ProgrammingCryptol/enigma/Finite.cry +++ b/docs/ProgrammingCryptol/enigma/Finite.cry @@ -1,5 +1,5 @@ /* - * Copyright (c) 2013-2015 Galois, Inc. + * Copyright (c) 2013-2016 Galois, Inc. * Distributed under the terms of the BSD3 license (see LICENSE file) */ diff --git a/docs/ProgrammingCryptol/enigma/Simple.cry b/docs/ProgrammingCryptol/enigma/Simple.cry index 1daefc04..afa11a78 100644 --- a/docs/ProgrammingCryptol/enigma/Simple.cry +++ b/docs/ProgrammingCryptol/enigma/Simple.cry @@ -1,5 +1,5 @@ /* - * Copyright (c) 2013-2015 Galois, Inc. + * Copyright (c) 2013-2016 Galois, Inc. * Distributed under the terms of the BSD3 license (see LICENSE file) */ diff --git a/docs/ProgrammingCryptol/enigma/ticket141.cry b/docs/ProgrammingCryptol/enigma/ticket141.cry index 767be9e3..9a9661de 100644 --- a/docs/ProgrammingCryptol/enigma/ticket141.cry +++ b/docs/ProgrammingCryptol/enigma/ticket141.cry @@ -1,5 +1,5 @@ /* - * Copyright (c) 2013-2015 Galois, Inc. + * Copyright (c) 2013-2016 Galois, Inc. * Distributed under the terms of the BSD3 license (see LICENSE file) */ diff --git a/docs/ProgrammingCryptol/main/Cryptol-fullpage.tex b/docs/ProgrammingCryptol/main/Cryptol-fullpage.tex index a110d04f..fa42ee71 100644 --- a/docs/ProgrammingCryptol/main/Cryptol-fullpage.tex +++ b/docs/ProgrammingCryptol/main/Cryptol-fullpage.tex @@ -94,7 +94,7 @@ is aimed for the more advanced reader. It can be skipped on a first reading with \renewcommand{\sectionmark}[1]{\markright{#1}{}} \cfoot{} \fancyfoot[LE,RO]{\fancyplain{}{\textsf{\thepage}}} -\fancyfoot[LO,RE]{\fancyplain{}{\textsf{\copyright\ 2010--2015, Galois, Inc.}}} +\fancyfoot[LO,RE]{\fancyplain{}{\textsf{\copyright\ 2010--2016, Galois, Inc.}}} %% \fancyhead[LE]{\fancyplain{}{\textsf{\draftdate}}} %% \fancyhead[RO]{\fancyplain{}{\textsf{DO NOT DISTRIBUTE!}}} \fancyhead[RO,LE]{\fancyplain{}{}} %% outer diff --git a/docs/ProgrammingCryptol/main/Cryptol.tex b/docs/ProgrammingCryptol/main/Cryptol.tex index eb15856b..1781cb46 100644 --- a/docs/ProgrammingCryptol/main/Cryptol.tex +++ b/docs/ProgrammingCryptol/main/Cryptol.tex @@ -109,7 +109,7 @@ without loss of continuity.}\end{minipage}}\end{center}} } \cfoot{} \fancyfoot[LE,RO]{\changefont{\textsf{\thepage}}} -\fancyfoot[LO,RE]{\changefont{\textsf{\copyright\ 2010--2015, Galois, Inc.}}} +\fancyfoot[LO,RE]{\changefont{\textsf{\copyright\ 2010--2016, Galois, Inc.}}} %% \fancyhead[LE]{\fancyplain{}{\textsf{\draftdate}}} %% \fancyhead[RO]{\fancyplain{}{\textsf{DO NOT DISTRIBUTE!}}} \fancyhead[RO,LE]{\fancyplain{}{}} %% outer diff --git a/docs/ProgrammingCryptol/preface/Notice.tex b/docs/ProgrammingCryptol/preface/Notice.tex index 5556d29e..2776dcd8 100644 --- a/docs/ProgrammingCryptol/preface/Notice.tex +++ b/docs/ProgrammingCryptol/preface/Notice.tex @@ -8,7 +8,7 @@ appear in this documentation. Of course, we appreciate bug reports and clarification suggestions. - Copyright 2003--2015 Galois, Inc. All rights reserved by Galois, + Copyright 2003--2016 Galois, Inc. All rights reserved by Galois, Inc. The software installed in accordance with this documentation is diff --git a/docs/ProgrammingCryptol/tools/compileProgrammingCryptol.hs b/docs/ProgrammingCryptol/tools/compileProgrammingCryptol.hs index a4edc98f..182a7f28 100644 --- a/docs/ProgrammingCryptol/tools/compileProgrammingCryptol.hs +++ b/docs/ProgrammingCryptol/tools/compileProgrammingCryptol.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/docs/ProgrammingCryptol/tools/genAlph.hs b/docs/ProgrammingCryptol/tools/genAlph.hs index b4184259..3a5fd3d8 100644 --- a/docs/ProgrammingCryptol/tools/genAlph.hs +++ b/docs/ProgrammingCryptol/tools/genAlph.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/docs/chop.hs b/docs/chop.hs index f1347ba3..dc1cb667 100755 --- a/docs/chop.hs +++ b/docs/chop.hs @@ -2,7 +2,7 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/examples/Cipher.cry b/examples/Cipher.cry index c3d8697a..3374a185 100644 --- a/examples/Cipher.cry +++ b/examples/Cipher.cry @@ -1,5 +1,5 @@ /* - * Copyright (c) 2013-2015 Galois, Inc. + * Copyright (c) 2013-2016 Galois, Inc. * Distributed under the terms of the BSD3 license (see LICENSE file) */ diff --git a/examples/DES.cry b/examples/DES.cry index acb51ab3..905ddf07 100644 --- a/examples/DES.cry +++ b/examples/DES.cry @@ -1,5 +1,5 @@ /* - * Copyright (c) 2013-2015 Galois, Inc. + * Copyright (c) 2013-2016 Galois, Inc. * Distributed under the terms of the BSD3 license (see LICENSE file) */ diff --git a/examples/DEStest.cry b/examples/DEStest.cry index 0bccc7db..4ce013dd 100644 --- a/examples/DEStest.cry +++ b/examples/DEStest.cry @@ -1,5 +1,5 @@ /* - * Copyright (c) 2013-2015 Galois, Inc. + * Copyright (c) 2013-2016 Galois, Inc. * Distributed under the terms of the BSD3 license (see LICENSE file) */ diff --git a/examples/FNV-a1.cry b/examples/FNV-a1.cry index 5c12b768..9c50570f 100644 --- a/examples/FNV-a1.cry +++ b/examples/FNV-a1.cry @@ -1,5 +1,5 @@ /* - * Copyright (c) 2014-2015 Galois, Inc. + * Copyright (c) 2014-2016 Galois, Inc. * Distributed under the terms of the BSD3 license (see LICENSE file) */ diff --git a/examples/SHA1.cry b/examples/SHA1.cry index e6db8c3b..9e10f578 100644 --- a/examples/SHA1.cry +++ b/examples/SHA1.cry @@ -1,5 +1,5 @@ /* - * Copyright (c) 2004, 2013-2015 Galois, Inc. + * Copyright (c) 2004, 2013-2016 Galois, Inc. * Distributed under the terms of the BSD3 license (see LICENSE file) */ diff --git a/examples/Salsa20.cry b/examples/Salsa20.cry index 6654496a..9d24180a 100644 --- a/examples/Salsa20.cry +++ b/examples/Salsa20.cry @@ -1,5 +1,5 @@ /* - * Copyright (c) 2013-2015 Galois, Inc. + * Copyright (c) 2013-2016 Galois, Inc. * Distributed under the terms of the BSD3 license (see LICENSE file) */ diff --git a/examples/Test.cry b/examples/Test.cry index 4436de3c..286d1ee2 100644 --- a/examples/Test.cry +++ b/examples/Test.cry @@ -1,5 +1,5 @@ /* - * Copyright (c) 2013-2015 Galois, Inc. + * Copyright (c) 2013-2016 Galois, Inc. * Distributed under the terms of the BSD3 license (see LICENSE file) */ diff --git a/examples/TripleDES.cry b/examples/TripleDES.cry index fe4eca1e..5d745ee7 100644 --- a/examples/TripleDES.cry +++ b/examples/TripleDES.cry @@ -1,5 +1,5 @@ /* - * Copyright (c) 2013-2015 Galois, Inc. + * Copyright (c) 2013-2016 Galois, Inc. * Distributed under the terms of the BSD3 license (see LICENSE file) */ diff --git a/examples/ZUC.cry b/examples/ZUC.cry index aa1bd335..ff28e2bf 100644 --- a/examples/ZUC.cry +++ b/examples/ZUC.cry @@ -1,4 +1,4 @@ -// Copyright (c) 2011-2015 Galois, Inc. +// Copyright (c) 2011-2016 Galois, Inc. // An implementation of ZUC, Version 1.5 // Version info: If the following variable is set to True, then we implement diff --git a/examples/contrib/RC4.cry b/examples/contrib/RC4.cry index ffe1508f..2da3dfb3 100644 --- a/examples/contrib/RC4.cry +++ b/examples/contrib/RC4.cry @@ -1,3 +1,5 @@ +// Contributed by GitHub user orchid-hybrid + swap : [256][8] -> [8] -> [8] -> [256][8] swap s i j = [ s @ (if n == i then j else if n == j then i else diff --git a/examples/contrib/simon.cry b/examples/contrib/simon.cry index 582063a3..4d15893d 100644 --- a/examples/contrib/simon.cry +++ b/examples/contrib/simon.cry @@ -1,5 +1,5 @@ /* - * Copyright (c) 2013-2015 Galois, Inc. + * Copyright (c) 2013-2016 Galois, Inc. * Distributed under the terms of the BSD3 license (see LICENSE file) */ diff --git a/examples/contrib/speck.cry b/examples/contrib/speck.cry index 1f8672da..3f9b973c 100644 --- a/examples/contrib/speck.cry +++ b/examples/contrib/speck.cry @@ -1,5 +1,5 @@ /* - * Copyright (c) 2013-2015 Galois, Inc. + * Copyright (c) 2013-2016 Galois, Inc. * Distributed under the terms of the BSD3 license (see LICENSE file) */ diff --git a/examples/funstuff/Coins.cry b/examples/funstuff/Coins.cry index 90880fae..d3f2d6f8 100644 --- a/examples/funstuff/Coins.cry +++ b/examples/funstuff/Coins.cry @@ -1,3 +1,5 @@ +// Copyright (c) 2015-2016 Galois, Inc. + // The puzzle goes like this: // You've got 30 coins that add up to $1.09 - what are they? coinPuzzle : [10] -> [10] -> [10] -> [10] -> Bit diff --git a/examples/funstuff/FoxChickenCorn.cry b/examples/funstuff/FoxChickenCorn.cry index af14dab2..a7c83b76 100644 --- a/examples/funstuff/FoxChickenCorn.cry +++ b/examples/funstuff/FoxChickenCorn.cry @@ -1,5 +1,5 @@ /* - * Copyright (c) 2013-2015 Galois, Inc. + * Copyright (c) 2013-2016 Galois, Inc. * Distributed under the terms of the BSD3 license (see LICENSE file) */ diff --git a/examples/funstuff/NQueens.cry b/examples/funstuff/NQueens.cry index ecfb7fa0..6cd24a1a 100644 --- a/examples/funstuff/NQueens.cry +++ b/examples/funstuff/NQueens.cry @@ -1,5 +1,5 @@ /* - * Copyright (c) 2013-2015 Galois, Inc. + * Copyright (c) 2013-2016 Galois, Inc. * Distributed under the terms of the BSD3 license (see LICENSE file) */ diff --git a/examples/funstuff/marble.cry b/examples/funstuff/marble.cry index 49e4262e..18021038 100644 --- a/examples/funstuff/marble.cry +++ b/examples/funstuff/marble.cry @@ -1,5 +1,5 @@ /* - * Copyright (c) 2013-2015 Galois, Inc. + * Copyright (c) 2013-2016 Galois, Inc. * Distributed under the terms of the BSD3 license (see LICENSE file) */ diff --git a/examples/maliciousSHA/malicious_SHA1.cry b/examples/maliciousSHA/malicious_SHA1.cry index 322d57fc..faf122eb 100755 --- a/examples/maliciousSHA/malicious_SHA1.cry +++ b/examples/maliciousSHA/malicious_SHA1.cry @@ -1,5 +1,5 @@ /* - * Copyright (c) 2004, 2013-2015 Galois, Inc. + * Copyright (c) 2004, 2013-2016 Galois, Inc. * Distributed under the terms of the BSD3 license (see LICENSE file) */ diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry index 9bf08f94..e6f407b3 100644 --- a/lib/Cryptol.cry +++ b/lib/Cryptol.cry @@ -1,5 +1,5 @@ /* - * Copyright (c) 2013-2015 Galois, Inc. + * Copyright (c) 2013-2016 Galois, Inc. * Distributed under the terms of the BSD3 license (see LICENSE file) */ diff --git a/src/Cryptol/Eval.hs b/src/Cryptol/Eval.hs index 981d68bd..88945d43 100644 --- a/src/Cryptol/Eval.hs +++ b/src/Cryptol/Eval.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/Eval/Arch.hs b/src/Cryptol/Eval/Arch.hs index 8165aba3..08f46b75 100644 --- a/src/Cryptol/Eval/Arch.hs +++ b/src/Cryptol/Eval/Arch.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2014-2015 Galois, Inc. +-- Copyright : (c) 2014-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/Eval/Env.hs b/src/Cryptol/Eval/Env.hs index a5592813..04c1a52c 100644 --- a/src/Cryptol/Eval/Env.hs +++ b/src/Cryptol/Eval/Env.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/Eval/Error.hs b/src/Cryptol/Eval/Error.hs index af861732..75ff7b1a 100644 --- a/src/Cryptol/Eval/Error.hs +++ b/src/Cryptol/Eval/Error.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/Eval/Type.hs b/src/Cryptol/Eval/Type.hs index 6abe50db..274780df 100644 --- a/src/Cryptol/Eval/Type.hs +++ b/src/Cryptol/Eval/Type.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/Eval/Value.hs b/src/Cryptol/Eval/Value.hs index 2113fece..0211e99f 100644 --- a/src/Cryptol/Eval/Value.hs +++ b/src/Cryptol/Eval/Value.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/ModuleSystem.hs b/src/Cryptol/ModuleSystem.hs index b0bc2f14..9924aaae 100644 --- a/src/Cryptol/ModuleSystem.hs +++ b/src/Cryptol/ModuleSystem.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/ModuleSystem/Base.hs b/src/Cryptol/ModuleSystem/Base.hs index 339f0c6f..51fbbfbe 100644 --- a/src/Cryptol/ModuleSystem/Base.hs +++ b/src/Cryptol/ModuleSystem/Base.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/ModuleSystem/Env.hs b/src/Cryptol/ModuleSystem/Env.hs index fe94e5b9..00b17764 100644 --- a/src/Cryptol/ModuleSystem/Env.hs +++ b/src/Cryptol/ModuleSystem/Env.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/ModuleSystem/Interface.hs b/src/Cryptol/ModuleSystem/Interface.hs index a4619912..290acbbb 100644 --- a/src/Cryptol/ModuleSystem/Interface.hs +++ b/src/Cryptol/ModuleSystem/Interface.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/ModuleSystem/Monad.hs b/src/Cryptol/ModuleSystem/Monad.hs index 227f2af4..dcb62c1c 100644 --- a/src/Cryptol/ModuleSystem/Monad.hs +++ b/src/Cryptol/ModuleSystem/Monad.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/ModuleSystem/Name.hs b/src/Cryptol/ModuleSystem/Name.hs index 8e58b0e1..b4864aea 100644 --- a/src/Cryptol/ModuleSystem/Name.hs +++ b/src/Cryptol/ModuleSystem/Name.hs @@ -1,3 +1,11 @@ +-- | +-- Module : $Header$ +-- Copyright : (c) 2015-2016 Galois, Inc. +-- License : BSD3 +-- Maintainer : cryptol@galois.com +-- Stability : provisional +-- Portability : portable + {-# LANGUAGE Trustworthy #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE DeriveGeneric #-} diff --git a/src/Cryptol/ModuleSystem/NamingEnv.hs b/src/Cryptol/ModuleSystem/NamingEnv.hs index 563f7eb7..86684ea5 100644 --- a/src/Cryptol/ModuleSystem/NamingEnv.hs +++ b/src/Cryptol/ModuleSystem/NamingEnv.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/ModuleSystem/Renamer.hs b/src/Cryptol/ModuleSystem/Renamer.hs index 8656760a..d9880fa1 100644 --- a/src/Cryptol/ModuleSystem/Renamer.hs +++ b/src/Cryptol/ModuleSystem/Renamer.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/Parser.y b/src/Cryptol/Parser.y index de609ad1..c4197f47 100644 --- a/src/Cryptol/Parser.y +++ b/src/Cryptol/Parser.y @@ -1,4 +1,12 @@ { +-- | +-- Module : $Header$ +-- Copyright : (c) 2013-2016 Galois, Inc. +-- License : BSD3 +-- Maintainer : cryptol@galois.com +-- Stability : provisional +-- Portability : portable + {-# LANGUAGE Trustworthy #-} module Cryptol.Parser ( parseModule diff --git a/src/Cryptol/Parser/AST.hs b/src/Cryptol/Parser/AST.hs index f000606d..deceede4 100644 --- a/src/Cryptol/Parser/AST.hs +++ b/src/Cryptol/Parser/AST.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/Parser/Lexer.x b/src/Cryptol/Parser/Lexer.x index b8891de1..e8bba6d2 100644 --- a/src/Cryptol/Parser/Lexer.x +++ b/src/Cryptol/Parser/Lexer.x @@ -1,4 +1,12 @@ { +-- | +-- Module : $Header$ +-- Copyright : (c) 2013-2016 Galois, Inc. +-- License : BSD3 +-- Maintainer : cryptol@galois.com +-- Stability : provisional +-- Portability : portable +-- -- At present Alex generates code with too many warnings. {-# LANGUAGE Trustworthy #-} {-# LANGUAGE OverloadedStrings #-} diff --git a/src/Cryptol/Parser/LexerUtils.hs b/src/Cryptol/Parser/LexerUtils.hs index e43963bc..c009204b 100644 --- a/src/Cryptol/Parser/LexerUtils.hs +++ b/src/Cryptol/Parser/LexerUtils.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/Parser/Name.hs b/src/Cryptol/Parser/Name.hs index 7c39e8f5..e6f8c74d 100644 --- a/src/Cryptol/Parser/Name.hs +++ b/src/Cryptol/Parser/Name.hs @@ -1,3 +1,11 @@ +-- | +-- Module : $Header$ +-- Copyright : (c) 2015-2016 Galois, Inc. +-- License : BSD3 +-- Maintainer : cryptol@galois.com +-- Stability : provisional +-- Portability : portable + {-# LANGUAGE DeriveGeneric #-} module Cryptol.Parser.Name where diff --git a/src/Cryptol/Parser/Names.hs b/src/Cryptol/Parser/Names.hs index 67119d13..8252f647 100644 --- a/src/Cryptol/Parser/Names.hs +++ b/src/Cryptol/Parser/Names.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/Parser/NoInclude.hs b/src/Cryptol/Parser/NoInclude.hs index da8cbd82..29a58b14 100644 --- a/src/Cryptol/Parser/NoInclude.hs +++ b/src/Cryptol/Parser/NoInclude.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/Parser/NoPat.hs b/src/Cryptol/Parser/NoPat.hs index a9912bd0..e2ea1d64 100644 --- a/src/Cryptol/Parser/NoPat.hs +++ b/src/Cryptol/Parser/NoPat.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/Parser/ParserUtils.hs b/src/Cryptol/Parser/ParserUtils.hs index fe41ed16..053de7e1 100644 --- a/src/Cryptol/Parser/ParserUtils.hs +++ b/src/Cryptol/Parser/ParserUtils.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/Parser/Position.hs b/src/Cryptol/Parser/Position.hs index 0a68c7a2..f18e6ca6 100644 --- a/src/Cryptol/Parser/Position.hs +++ b/src/Cryptol/Parser/Position.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/Parser/Unlit.hs b/src/Cryptol/Parser/Unlit.hs index e9f93320..902b4164 100644 --- a/src/Cryptol/Parser/Unlit.hs +++ b/src/Cryptol/Parser/Unlit.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/Parser/Utils.hs b/src/Cryptol/Parser/Utils.hs index e3128464..491cb094 100644 --- a/src/Cryptol/Parser/Utils.hs +++ b/src/Cryptol/Parser/Utils.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/Prelude.hs b/src/Cryptol/Prelude.hs index e986b496..93cb943e 100644 --- a/src/Cryptol/Prelude.hs +++ b/src/Cryptol/Prelude.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2015 Galois, Inc. +-- Copyright : (c) 2015-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/Prims/Eval.hs b/src/Cryptol/Prims/Eval.hs index f98ce0dc..3612bdf0 100644 --- a/src/Cryptol/Prims/Eval.hs +++ b/src/Cryptol/Prims/Eval.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/Prims/Syntax.hs b/src/Cryptol/Prims/Syntax.hs index 20dce24e..a386bb93 100644 --- a/src/Cryptol/Prims/Syntax.hs +++ b/src/Cryptol/Prims/Syntax.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/REPL/Command.hs b/src/Cryptol/REPL/Command.hs index 0a13cb75..62fe7f43 100644 --- a/src/Cryptol/REPL/Command.hs +++ b/src/Cryptol/REPL/Command.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/REPL/Monad.hs b/src/Cryptol/REPL/Monad.hs index e79b5c51..c0022b85 100644 --- a/src/Cryptol/REPL/Monad.hs +++ b/src/Cryptol/REPL/Monad.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/REPL/Trie.hs b/src/Cryptol/REPL/Trie.hs index ac00b69f..68d36ba9 100644 --- a/src/Cryptol/REPL/Trie.hs +++ b/src/Cryptol/REPL/Trie.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/Symbolic.hs b/src/Cryptol/Symbolic.hs index 56aedd26..a25fcac2 100644 --- a/src/Cryptol/Symbolic.hs +++ b/src/Cryptol/Symbolic.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/Symbolic/Prims.hs b/src/Cryptol/Symbolic/Prims.hs index d59279f7..9c6c7c80 100644 --- a/src/Cryptol/Symbolic/Prims.hs +++ b/src/Cryptol/Symbolic/Prims.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/Symbolic/Value.hs b/src/Cryptol/Symbolic/Value.hs index a1116041..2604ec5c 100644 --- a/src/Cryptol/Symbolic/Value.hs +++ b/src/Cryptol/Symbolic/Value.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/Testing/Concrete.hs b/src/Cryptol/Testing/Concrete.hs index 87bb1407..81bdc8e0 100644 --- a/src/Cryptol/Testing/Concrete.hs +++ b/src/Cryptol/Testing/Concrete.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/Testing/Random.hs b/src/Cryptol/Testing/Random.hs index 985291af..d50f60b2 100644 --- a/src/Cryptol/Testing/Random.hs +++ b/src/Cryptol/Testing/Random.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/Transform/MonoValues.hs b/src/Cryptol/Transform/MonoValues.hs index b7fb16db..324a8ff2 100644 --- a/src/Cryptol/Transform/MonoValues.hs +++ b/src/Cryptol/Transform/MonoValues.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/Transform/Specialize.hs b/src/Cryptol/Transform/Specialize.hs index 77f78608..bea7afc5 100644 --- a/src/Cryptol/Transform/Specialize.hs +++ b/src/Cryptol/Transform/Specialize.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/TypeCheck.hs b/src/Cryptol/TypeCheck.hs index 9fdd4f3f..d917718f 100644 --- a/src/Cryptol/TypeCheck.hs +++ b/src/Cryptol/TypeCheck.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/TypeCheck/AST.hs b/src/Cryptol/TypeCheck/AST.hs index 4635958e..2ab895a3 100644 --- a/src/Cryptol/TypeCheck/AST.hs +++ b/src/Cryptol/TypeCheck/AST.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/TypeCheck/Depends.hs b/src/Cryptol/TypeCheck/Depends.hs index 7f97c4d5..a0d788a2 100644 --- a/src/Cryptol/TypeCheck/Depends.hs +++ b/src/Cryptol/TypeCheck/Depends.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/TypeCheck/Infer.hs b/src/Cryptol/TypeCheck/Infer.hs index bde30222..b5ca5825 100644 --- a/src/Cryptol/TypeCheck/Infer.hs +++ b/src/Cryptol/TypeCheck/Infer.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/TypeCheck/InferTypes.hs b/src/Cryptol/TypeCheck/InferTypes.hs index 3d79950c..2d579f9e 100644 --- a/src/Cryptol/TypeCheck/InferTypes.hs +++ b/src/Cryptol/TypeCheck/InferTypes.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/TypeCheck/Instantiate.hs b/src/Cryptol/TypeCheck/Instantiate.hs index 5186ddbc..4703b5e5 100644 --- a/src/Cryptol/TypeCheck/Instantiate.hs +++ b/src/Cryptol/TypeCheck/Instantiate.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/TypeCheck/Kind.hs b/src/Cryptol/TypeCheck/Kind.hs index 598aea63..d09cc77a 100644 --- a/src/Cryptol/TypeCheck/Kind.hs +++ b/src/Cryptol/TypeCheck/Kind.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/TypeCheck/Monad.hs b/src/Cryptol/TypeCheck/Monad.hs index 22c6103f..5eeb6eb5 100644 --- a/src/Cryptol/TypeCheck/Monad.hs +++ b/src/Cryptol/TypeCheck/Monad.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/TypeCheck/PP.hs b/src/Cryptol/TypeCheck/PP.hs index 4d9f164d..4e6587c9 100644 --- a/src/Cryptol/TypeCheck/PP.hs +++ b/src/Cryptol/TypeCheck/PP.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/TypeCheck/Sanity.hs b/src/Cryptol/TypeCheck/Sanity.hs index c627530c..40dbb755 100644 --- a/src/Cryptol/TypeCheck/Sanity.hs +++ b/src/Cryptol/TypeCheck/Sanity.hs @@ -1,3 +1,10 @@ +-- | +-- Module : $Header$ +-- Copyright : (c) 2015-2016 Galois, Inc. +-- License : BSD3 +-- Maintainer : cryptol@galois.com +-- Stability : provisional +-- Portability : portable module Cryptol.TypeCheck.Sanity ( tcExpr , tcDecls diff --git a/src/Cryptol/TypeCheck/Solve.hs b/src/Cryptol/TypeCheck/Solve.hs index e1d5a747..0251b3d9 100644 --- a/src/Cryptol/TypeCheck/Solve.hs +++ b/src/Cryptol/TypeCheck/Solve.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/TypeCheck/Solver/Class.hs b/src/Cryptol/TypeCheck/Solver/Class.hs index c1657573..3c1b82f6 100644 --- a/src/Cryptol/TypeCheck/Solver/Class.hs +++ b/src/Cryptol/TypeCheck/Solver/Class.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/TypeCheck/Solver/CrySAT.hs b/src/Cryptol/TypeCheck/Solver/CrySAT.hs index 1fc2dcfd..03f165bc 100644 --- a/src/Cryptol/TypeCheck/Solver/CrySAT.hs +++ b/src/Cryptol/TypeCheck/Solver/CrySAT.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/TypeCheck/Solver/InfNat.hs b/src/Cryptol/TypeCheck/Solver/InfNat.hs index 12eda8b2..c43663be 100644 --- a/src/Cryptol/TypeCheck/Solver/InfNat.hs +++ b/src/Cryptol/TypeCheck/Solver/InfNat.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/TypeCheck/Solver/Numeric/AST.hs b/src/Cryptol/TypeCheck/Solver/Numeric/AST.hs index 2bb8e092..b901e235 100644 --- a/src/Cryptol/TypeCheck/Solver/Numeric/AST.hs +++ b/src/Cryptol/TypeCheck/Solver/Numeric/AST.hs @@ -1,8 +1,17 @@ +-- | +-- Module : $Header$ +-- Copyright : (c) 2014-2016 Galois, Inc. +-- License : BSD3 +-- Maintainer : cryptol@galois.com +-- Stability : provisional +-- Portability : portable +-- +-- The sytnax of numeric propositions. + {-# LANGUAGE Safe #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE DeriveGeneric #-} --- | The sytnax of numeric propositions. module Cryptol.TypeCheck.Solver.Numeric.AST ( Name(..), ppName diff --git a/src/Cryptol/TypeCheck/Solver/Numeric/Defined.hs b/src/Cryptol/TypeCheck/Solver/Numeric/Defined.hs index dde8ff5a..d6d769f3 100644 --- a/src/Cryptol/TypeCheck/Solver/Numeric/Defined.hs +++ b/src/Cryptol/TypeCheck/Solver/Numeric/Defined.hs @@ -1,3 +1,11 @@ +-- | +-- Module : $Header$ +-- Copyright : (c) 2014-2016 Galois, Inc. +-- License : BSD3 +-- Maintainer : cryptol@galois.com +-- Stability : provisional +-- Portability : portable + {-# LANGUAGE Safe #-} module Cryptol.TypeCheck.Solver.Numeric.Defined where @@ -45,6 +53,3 @@ cryDefined expr = LenFromThenTo x y z -> cryDefined x :&& cryDefined y :&& cryDefined z :&& Fin x :&& Fin y :&& Fin z :&& Not (x :== y) - - - diff --git a/src/Cryptol/TypeCheck/Solver/Numeric/Fin.hs b/src/Cryptol/TypeCheck/Solver/Numeric/Fin.hs index f647fb6e..5492cf77 100644 --- a/src/Cryptol/TypeCheck/Solver/Numeric/Fin.hs +++ b/src/Cryptol/TypeCheck/Solver/Numeric/Fin.hs @@ -1,6 +1,14 @@ -{-# LANGUAGE PatternGuards #-} +-- | +-- Module : $Header$ +-- Copyright : (c) 2015-2016 Galois, Inc. +-- License : BSD3 +-- Maintainer : cryptol@galois.com +-- Stability : provisional +-- Portability : portable +-- +-- Simplification of `fin` constraints. --- | Simplification of `fin` constraints. +{-# LANGUAGE PatternGuards #-} module Cryptol.TypeCheck.Solver.Numeric.Fin where import Data.Map (Map) diff --git a/src/Cryptol/TypeCheck/Solver/Numeric/ImportExport.hs b/src/Cryptol/TypeCheck/Solver/Numeric/ImportExport.hs index 20ec69dd..230a1169 100644 --- a/src/Cryptol/TypeCheck/Solver/Numeric/ImportExport.hs +++ b/src/Cryptol/TypeCheck/Solver/Numeric/ImportExport.hs @@ -1,3 +1,11 @@ +-- | +-- Module : $Header$ +-- Copyright : (c) 2014-2016 Galois, Inc. +-- License : BSD3 +-- Maintainer : cryptol@galois.com +-- Stability : provisional +-- Portability : portable + {-# LANGUAGE Safe #-} module Cryptol.TypeCheck.Solver.Numeric.ImportExport ( ExportM diff --git a/src/Cryptol/TypeCheck/Solver/Numeric/Interval.hs b/src/Cryptol/TypeCheck/Solver/Numeric/Interval.hs index fa580e2f..f7be0da8 100644 --- a/src/Cryptol/TypeCheck/Solver/Numeric/Interval.hs +++ b/src/Cryptol/TypeCheck/Solver/Numeric/Interval.hs @@ -1,7 +1,16 @@ +-- | +-- Module : $Header$ +-- Copyright : (c) 2015-2016 Galois, Inc. +-- License : BSD3 +-- Maintainer : cryptol@galois.com +-- Stability : provisional +-- Portability : portable +-- +-- An interval interpretation of types. + {-# LANGUAGE PatternGuards #-} {-# LANGUAGE BangPatterns #-} --- | An interval interpretation of types. module Cryptol.TypeCheck.Solver.Numeric.Interval where import Cryptol.TypeCheck.AST diff --git a/src/Cryptol/TypeCheck/Solver/Numeric/NonLin.hs b/src/Cryptol/TypeCheck/Solver/Numeric/NonLin.hs index 3da5c51b..5e399240 100644 --- a/src/Cryptol/TypeCheck/Solver/Numeric/NonLin.hs +++ b/src/Cryptol/TypeCheck/Solver/Numeric/NonLin.hs @@ -1,12 +1,20 @@ +-- | +-- Module : $Header$ +-- Copyright : (c) 2014-2016 Galois, Inc. +-- License : BSD3 +-- Maintainer : cryptol@galois.com +-- Stability : provisional +-- Portability : portable +-- +-- Separate Non-Linear Constraints +-- When we spot a non-linear expression, we name it and add it to a map. +-- +-- If we see the same expression multiple times, then we give it the same name. +-- +-- The body of the non-linear expression is not processed further, +-- so the resulting map should not contain any of the newly minted names. + {-# LANGUAGE Safe, RecordWildCards #-} -{- | Separate Non-Linear Constraints -When we spot a non-linear expression, we name it and add it to a map. - -If we see the same expression multiple times, then we give it the same name. - -The body of the non-linear expression is not processed further, -so the resulting map should not contain any of the newly minted names. --} module Cryptol.TypeCheck.Solver.Numeric.NonLin ( nonLinProp diff --git a/src/Cryptol/TypeCheck/Solver/Numeric/SMT.hs b/src/Cryptol/TypeCheck/Solver/Numeric/SMT.hs index 360aedff..99be2f37 100644 --- a/src/Cryptol/TypeCheck/Solver/Numeric/SMT.hs +++ b/src/Cryptol/TypeCheck/Solver/Numeric/SMT.hs @@ -1,5 +1,15 @@ +-- | +-- Module : $Header$ +-- Copyright : (c) 2014-2016 Galois, Inc. +-- License : BSD3 +-- Maintainer : cryptol@galois.com +-- Stability : provisional +-- Portability : portable +-- +-- Desugar into SMTLIB Terminology + {-# LANGUAGE Safe #-} --- | Desugar into SMTLIB Terminology + module Cryptol.TypeCheck.Solver.Numeric.SMT ( desugarProp , smtName diff --git a/src/Cryptol/TypeCheck/Solver/Numeric/Simplify.hs b/src/Cryptol/TypeCheck/Solver/Numeric/Simplify.hs index 9fdc0521..383b5c47 100644 --- a/src/Cryptol/TypeCheck/Solver/Numeric/Simplify.hs +++ b/src/Cryptol/TypeCheck/Solver/Numeric/Simplify.hs @@ -1,11 +1,19 @@ -{-# LANGUAGE Safe, PatternGuards, BangPatterns #-} -{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-} --- | Simplification. +-- | +-- Module : $Header$ +-- Copyright : (c) 2014-2016 Galois, Inc. +-- License : BSD3 +-- Maintainer : cryptol@galois.com +-- Stability : provisional +-- Portability : portable +-- -- TODO: -- - Putting in a normal form to spot "prove by assumption" -- - Additional simplification rules, namely various cancelation. -- - Things like: lg2 e(x) = x, where we know thate is increasing. +{-# LANGUAGE Safe, PatternGuards, BangPatterns #-} +{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-} + module Cryptol.TypeCheck.Solver.Numeric.Simplify ( -- * Simplify a property diff --git a/src/Cryptol/TypeCheck/Solver/Numeric/Simplify1.hs b/src/Cryptol/TypeCheck/Solver/Numeric/Simplify1.hs index 0f81aab7..5e5e6ef0 100644 --- a/src/Cryptol/TypeCheck/Solver/Numeric/Simplify1.hs +++ b/src/Cryptol/TypeCheck/Solver/Numeric/Simplify1.hs @@ -1,17 +1,25 @@ +-- | +-- Module : $Header$ +-- Copyright : (c) 2015-2016 Galois, Inc. +-- License : BSD3 +-- Maintainer : cryptol@galois.com +-- Stability : provisional +-- Portability : portable +-- +-- Simplification. +-- The rules in this module are all conditional on the expressions being +-- well-defined. +-- +-- So, for example, consider the formula `P`, which corresponds to `fin e`. +-- `P` says the following: +-- +-- if e is well-formed, then will evaluate to a finite natural number. +-- +-- More concretely, consider `fin (3 - 5)`. This will be simplified to `True`, +-- which does not mean that `3 - 5` is actually finite. + {-# LANGUAGE Safe, PatternGuards, BangPatterns #-} {-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-} -{- | Simplification. -The rules in this module are all conditional on the expressions being -well-defined. - -So, for example, consider the formula `P`, which corresponds to `fin e`. -`P` says the following: - - if e is well-formed, then will evaluate to a finite natural number. - -More concretely, consider `fin (3 - 5)`. This will be simplified to `True`, -which does not mean that `3 - 5` is actually finite. --} module Cryptol.TypeCheck.Solver.Numeric.Simplify1 (propToProp', ppProp') where diff --git a/src/Cryptol/TypeCheck/Solver/Numeric/SimplifyExpr.hs b/src/Cryptol/TypeCheck/Solver/Numeric/SimplifyExpr.hs index 18d26c4a..15c2bca5 100644 --- a/src/Cryptol/TypeCheck/Solver/Numeric/SimplifyExpr.hs +++ b/src/Cryptol/TypeCheck/Solver/Numeric/SimplifyExpr.hs @@ -1,11 +1,19 @@ +-- | +-- Module : $Header$ +-- Copyright : (c) 2015-2016 Galois, Inc. +-- License : BSD3 +-- Maintainer : cryptol@galois.com +-- Stability : provisional +-- Portability : portable +-- +-- Simplification of expressions. +-- The result of simplifying an expression `e`, is a new expression `e'`, +-- which satisfies the property: +-- +-- if e is well-defined then e and e' will evaluate to the same type. +-- + {-# LANGUAGE Safe, BangPatterns #-} -{- | Simplification of expressions. -The result of simplifying an expression `e`, is a new expression `e'`, -which satisfies the property: - - if e is well-defined then e and e' will evaluate to the same type. - --} module Cryptol.TypeCheck.Solver.Numeric.SimplifyExpr where import Cryptol.TypeCheck.Solver.Numeric.AST diff --git a/src/Cryptol/TypeCheck/Solver/Selector.hs b/src/Cryptol/TypeCheck/Solver/Selector.hs index aa6747f6..1a2b1c20 100644 --- a/src/Cryptol/TypeCheck/Solver/Selector.hs +++ b/src/Cryptol/TypeCheck/Solver/Selector.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/TypeCheck/Solver/Simplify.hs b/src/Cryptol/TypeCheck/Solver/Simplify.hs index 43114045..308975b0 100644 --- a/src/Cryptol/TypeCheck/Solver/Simplify.hs +++ b/src/Cryptol/TypeCheck/Solver/Simplify.hs @@ -1,3 +1,11 @@ +-- | +-- Module : $Header$ +-- Copyright : (c) 2015-2016 Galois, Inc. +-- License : BSD3 +-- Maintainer : cryptol@galois.com +-- Stability : provisional +-- Portability : portable + {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE MultiWayIf #-} diff --git a/src/Cryptol/TypeCheck/Solver/Utils.hs b/src/Cryptol/TypeCheck/Solver/Utils.hs index 5e676d00..4638dc3d 100644 --- a/src/Cryptol/TypeCheck/Solver/Utils.hs +++ b/src/Cryptol/TypeCheck/Solver/Utils.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/TypeCheck/Subst.hs b/src/Cryptol/TypeCheck/Subst.hs index 2b9a6c31..4f45326b 100644 --- a/src/Cryptol/TypeCheck/Subst.hs +++ b/src/Cryptol/TypeCheck/Subst.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/TypeCheck/TypeMap.hs b/src/Cryptol/TypeCheck/TypeMap.hs index eb84e249..1efeec2d 100644 --- a/src/Cryptol/TypeCheck/TypeMap.hs +++ b/src/Cryptol/TypeCheck/TypeMap.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/TypeCheck/TypeOf.hs b/src/Cryptol/TypeCheck/TypeOf.hs index cdcf7bd8..8862b37d 100644 --- a/src/Cryptol/TypeCheck/TypeOf.hs +++ b/src/Cryptol/TypeCheck/TypeOf.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2014-2015 Galois, Inc. +-- Copyright : (c) 2014-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/TypeCheck/Unify.hs b/src/Cryptol/TypeCheck/Unify.hs index eb959abc..fd7053ba 100644 --- a/src/Cryptol/TypeCheck/Unify.hs +++ b/src/Cryptol/TypeCheck/Unify.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/Utils/Debug.hs b/src/Cryptol/Utils/Debug.hs index 94fad0ef..5c75d0c7 100644 --- a/src/Cryptol/Utils/Debug.hs +++ b/src/Cryptol/Utils/Debug.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/Utils/Ident.hs b/src/Cryptol/Utils/Ident.hs index 7612971d..36121ede 100644 --- a/src/Cryptol/Utils/Ident.hs +++ b/src/Cryptol/Utils/Ident.hs @@ -1,3 +1,11 @@ +-- | +-- Module : $Header$ +-- Copyright : (c) 2015-2016 Galois, Inc. +-- License : BSD3 +-- Maintainer : cryptol@galois.com +-- Stability : provisional +-- Portability : portable + {-# LANGUAGE DeriveGeneric #-} module Cryptol.Utils.Ident where diff --git a/src/Cryptol/Utils/Misc.hs b/src/Cryptol/Utils/Misc.hs index c1c5932b..6b5bb2e4 100644 --- a/src/Cryptol/Utils/Misc.hs +++ b/src/Cryptol/Utils/Misc.hs @@ -1,3 +1,11 @@ +-- | +-- Module : $Header$ +-- Copyright : (c) 2014-2016 Galois, Inc. +-- License : BSD3 +-- Maintainer : cryptol@galois.com +-- Stability : provisional +-- Portability : portable + {-# LANGUAGE Safe, FlexibleContexts #-} module Cryptol.Utils.Misc where diff --git a/src/Cryptol/Utils/PP.hs b/src/Cryptol/Utils/PP.hs index f028b864..b63b173f 100644 --- a/src/Cryptol/Utils/PP.hs +++ b/src/Cryptol/Utils/PP.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/Utils/Panic.hs b/src/Cryptol/Utils/Panic.hs index 6e34bd01..6c36f4f6 100644 --- a/src/Cryptol/Utils/Panic.hs +++ b/src/Cryptol/Utils/Panic.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/Cryptol/Version.hs b/src/Cryptol/Version.hs index adbb0f80..5496d265 100644 --- a/src/Cryptol/Version.hs +++ b/src/Cryptol/Version.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/src/GitRev.hs b/src/GitRev.hs index 1edcf3a7..fdeed370 100644 --- a/src/GitRev.hs +++ b/src/GitRev.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2014-2015 Galois, Inc. +-- Copyright : (c) 2014-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/tests/Main.hs b/tests/Main.hs index 212e21cd..74c0ed9d 100644 --- a/tests/Main.hs +++ b/tests/Main.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/tests/parser/RunLexer.hs b/tests/parser/RunLexer.hs index 435c4afd..4a192527 100644 --- a/tests/parser/RunLexer.hs +++ b/tests/parser/RunLexer.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/tests/parser/RunTests.hs b/tests/parser/RunTests.hs index 6ae774d0..469f301a 100644 --- a/tests/parser/RunTests.hs +++ b/tests/parser/RunTests.hs @@ -1,6 +1,6 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/tests/regression/AES.cry b/tests/regression/AES.cry index 1325c855..2cc9a19a 100644 --- a/tests/regression/AES.cry +++ b/tests/regression/AES.cry @@ -1,5 +1,5 @@ // Cryptol AES Implementation -// Copyright (c) 2010-2015, Galois Inc. +// Copyright (c) 2010-2016, Galois Inc. // www.cryptol.net // You can freely use this source code for educational purposes. diff --git a/utils/CryAST.hs b/utils/CryAST.hs index 24599492..d4a704be 100755 --- a/utils/CryAST.hs +++ b/utils/CryAST.hs @@ -2,7 +2,7 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/utils/CryHtml.hs b/utils/CryHtml.hs index eb87c5fc..78c9a8e3 100755 --- a/utils/CryHtml.hs +++ b/utils/CryHtml.hs @@ -2,7 +2,7 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/utils/CryNoPat.hs b/utils/CryNoPat.hs index 4abf7ab7..29e7757b 100755 --- a/utils/CryNoPat.hs +++ b/utils/CryNoPat.hs @@ -2,7 +2,7 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/utils/CryPP.hs b/utils/CryPP.hs index 35bdb68e..03e848b8 100755 --- a/utils/CryPP.hs +++ b/utils/CryPP.hs @@ -2,7 +2,7 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional diff --git a/utils/CryTC.hs b/utils/CryTC.hs index 3e216426..b7e77464 100755 --- a/utils/CryTC.hs +++ b/utils/CryTC.hs @@ -2,7 +2,7 @@ -- | -- Module : $Header$ --- Copyright : (c) 2013-2015 Galois, Inc. +-- Copyright : (c) 2013-2016 Galois, Inc. -- License : BSD3 -- Maintainer : cryptol@galois.com -- Stability : provisional