SAWCore copyright headers, licence files and .cabal file fixes

LICENSE

@@ -0,0 +1,30 @@
+Copyright (c) 2012-2014, Galois, Inc.
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the names of the authors nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

Setup.hs

@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain

prelude/Prelude.sawcore

@@ -1,3 +1,7 @@
+-- Copyright   : Galois, Inc. 2012-2014
+-- License     : BSD3
+-- Maintainer  : [email protected]
+
 module Prelude where
 
 -- Grammar for the core prelude types.

src/Verifier/SAW.hs

@@ -1,3 +1,12 @@
+{- |
+Module      : Verifier.SAW
+Copyright   : Galois, Inc. 2012-2014
+License     : BSD3
+Maintainer  : [email protected]
+Stability   : experimental
+Portability : non-portable (language extensions)
+-}
+
 module Verifier.SAW 
   ( module Verifier.SAW.SharedTerm
   , Module

src/Verifier/SAW/Cache.hs

@@ -1,4 +1,14 @@
 {-# LANGUAGE ExistentialQuantification #-}
+
+{- |
+Module      : Verifier.SAW.Cache
+Copyright   : Galois, Inc. 2012-2014
+License     : BSD3
+Maintainer  : [email protected]
+Stability   : experimental
+Portability : non-portable (language extensions)
+-}
+
 module Verifier.SAW.Cache
   ( Cache
   , newCache
@@ -9,6 +19,7 @@ module Verifier.SAW.Cache
   , useCache
   ) where
 
+
 import Control.Monad (liftM)
 import Control.Monad.Ref
 import qualified Data.IntMap as IntMap

src/Verifier/SAW/Change.hs

@@ -2,6 +2,16 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE UndecidableInstances #-}
+
+{- |
+Module      : Verifier.SAW.Change
+Copyright   : Galois, Inc. 2012-2014
+License     : BSD3
+Maintainer  : [email protected]
+Stability   : experimental
+Portability : non-portable (language extensions)
+-}
+
 module Verifier.SAW.Change
   ( ChangeMonad(..)
   , Change(..)

src/Verifier/SAW/Conversion.hs

@@ -9,6 +9,16 @@
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE ViewPatterns #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
+
+{- |
+Module      : Verifier.SAW.Conversion
+Copyright   : Galois, Inc. 2012-2014
+License     : BSD3
+Maintainer  : [email protected]
+Stability   : experimental
+Portability : non-portable (language extensions)
+-}
+
 module Verifier.SAW.Conversion
   ( (:*:)(..)
   , Net.toPat

src/Verifier/SAW/Grammar.y

@@ -1,6 +1,16 @@
 {
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE ViewPatterns #-}
+
+{- |
+Module      : Verifier.SAW.Grammar
+Copyright   : Galois, Inc. 2012-2014
+License     : BSD3
+Maintainer  : jhendrix@galois.com
+Stability   : experimental
+Portability : non-portable (language extensions)
+-}
+
 module Verifier.SAW.Grammar
   ( Decl(..)
   , Term(..)

src/Verifier/SAW/Lexer.x

@@ -9,6 +9,16 @@
 {-# OPTIONS_GHC -fno-warn-unused-binds #-}
 {-# OPTIONS_GHC -fno-warn-unused-imports #-}
 {-# OPTIONS_GHC -fno-warn-unused-matches #-}
+
+{- |
+Module      : Verifier.SAW.Lexer
+Copyright   : Galois, Inc. 2012-2014
+License     : BSD3
+Maintainer  : jhendrix@galois.com
+Stability   : experimental
+Portability : non-portable (language extensions)
+-}
+
 module Verifier.SAW.Lexer
   ( module Verifier.SAW.Position
   , Token(..)

src/Verifier/SAW/ParserUtils.hs

@@ -1,6 +1,16 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TemplateHaskell #-}
+
+{- |
+Module      : Verifier.SAW.ParserUtils
+Copyright   : Galois, Inc. 2012-2014
+License     : BSD3
+Maintainer  : [email protected]
+Stability   : experimental
+Portability : non-portable (language extensions)
+-}
+
 module Verifier.SAW.ParserUtils
  ( module Verifier.SAW.TypedAST
    -- * Parser utilities.

src/Verifier/SAW/Position.hs

@@ -1,4 +1,14 @@
 {-# LANGUAGE DeriveFunctor #-}
+
+{- |
+Module      : Verifier.SAW.Position
+Copyright   : Galois, Inc. 2012-2014
+License     : BSD3
+Maintainer  : [email protected]
+Stability   : experimental
+Portability : non-portable (language extensions)
+-}
+
 module Verifier.SAW.Position
   ( Pos(..)
   , ppPos

src/Verifier/SAW/Prelude.hs

@@ -1,5 +1,15 @@
 {-# LANGUAGE CPP #-}
 {-# LANGUAGE TemplateHaskell #-}
+
+{- |
+Module      : Verifier.SAW.Prelude
+Copyright   : Galois, Inc. 2012-2014
+License     : BSD3
+Maintainer  : [email protected]
+Stability   : experimental
+Portability : non-portable (language extensions)
+-}
+
 module Verifier.SAW.Prelude
   ( Module
   , module Verifier.SAW.Prelude

src/Verifier/SAW/Prelude/Constants.hs

@@ -1,3 +1,12 @@
+{- |
+Module      : Verifier.SAW.Prelude.Constants
+Copyright   : Galois, Inc. 2012-2014
+License     : BSD3
+Maintainer  : [email protected]
+Stability   : experimental
+Portability : non-portable (language extensions)
+-}
+
 module Verifier.SAW.Prelude.Constants where
 
 import Verifier.SAW.TypedAST

src/Verifier/SAW/Prim.hs

@@ -1,4 +1,14 @@
 {-# LANGUAGE CPP #-}
+
+{- |
+Module      : Verifier.SAW.Prim
+Copyright   : Galois, Inc. 2012-2014
+License     : BSD3
+Maintainer  : [email protected]
+Stability   : experimental
+Portability : non-portable (language extensions)
+-}
+
 module Verifier.SAW.Prim where
 
 import Control.Applicative

src/Verifier/SAW/Recognizer.hs

@@ -4,6 +4,16 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE ViewPatterns #-}
+
+{- |
+Module      : Verifier.SAW.Recognizer
+Copyright   : Galois, Inc. 2012-2014
+License     : BSD3
+Maintainer  : [email protected]
+Stability   : experimental
+Portability : non-portable (language extensions)
+-}
+
 module Verifier.SAW.Recognizer 
   ( Recognizer
   , (<:), emptyl, endl

src/Verifier/SAW/Rewriter.hs

@@ -7,6 +7,15 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE ViewPatterns #-}
 
+{- |
+Module      : Verifier.SAW.Rewriter
+Copyright   : Galois, Inc. 2012-2014
+License     : BSD3
+Maintainer  : [email protected]
+Stability   : experimental
+Portability : non-portable (language extensions)
+-}
+
 module Verifier.SAW.Rewriter
   -- * Rewrite rules
   ( RewriteRule

src/Verifier/SAW/SharedTerm.hs

@@ -8,6 +8,16 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE ViewPatterns #-}
 {-# LANGUAGE CPP #-}
+
+{- |
+Module      : Verifier.SAW.SharedTerm
+Copyright   : Galois, Inc. 2012-2014
+License     : BSD3
+Maintainer  : [email protected]
+Stability   : experimental
+Portability : non-portable (language extensions)
+-}
+
 module Verifier.SAW.SharedTerm
   ( TermF(..)
   , Ident, mkIdent

src/Verifier/SAW/Simulator.hs

@@ -1,7 +1,3 @@
-{-
-Evaluator for SAWCore terms, with lazy evaluation order.
--}
-
 {-# LANGUAGE BangPatterns #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE OverloadedStrings #-}
@@ -10,6 +6,17 @@ Evaluator for SAWCore terms, with lazy evaluation order.
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE ViewPatterns #-}
 
+{- |
+Module      : Verifier.SAW.Simulator
+Copyright   : Galois, Inc. 2012-2014
+License     : BSD3
+Maintainer  : [email protected]
+Stability   : experimental
+Portability : non-portable (language extensions)
+
+Evaluator for SAWCore terms, with lazy evaluation order.
+-}
+
 module Verifier.SAW.Simulator where
 
 import Prelude hiding (mapM)

src/Verifier/SAW/Simulator/BitBlast.hs

@@ -1,6 +1,15 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 
+{- |
+Module      : Verifier.SAW.BitBlast
+Copyright   : Galois, Inc. 2012-2014
+License     : BSD3
+Maintainer  : [email protected]
+Stability   : experimental
+Portability : non-portable (language extensions)
+-}
+
 module Verifier.SAW.Simulator.BitBlast where
 
 import Control.Applicative

src/Verifier/SAW/Simulator/Prims.hs

@@ -1,5 +1,14 @@
 {-# LANGUAGE OverloadedStrings #-}
 
+{- |
+Module      : Verifier.SAW.Simulator.Prims
+Copyright   : Galois, Inc. 2012-2014
+License     : BSD3
+Maintainer  : [email protected]
+Stability   : experimental
+Portability : non-portable (language extensions)
+-}
+
 module Verifier.SAW.Simulator.Prims where
 
 import Control.Monad (liftM)

src/Verifier/SAW/Simulator/Value.hs

@@ -1,5 +1,14 @@
 {-# LANGUAGE PatternGuards #-}
 
+{- |
+Module      : Verifier.SAW.Simulator.Value
+Copyright   : Galois, Inc. 2012-2014
+License     : BSD3
+Maintainer  : [email protected]
+Stability   : experimental
+Portability : non-portable (language extensions)
+-}
+
 module Verifier.SAW.Simulator.Value where
 
 import Prelude hiding (mapM)

src/Verifier/SAW/TermNet.hs

@@ -2,6 +2,15 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE RecordWildCards #-}
 
+{- |
+Module      : Verifier.SAW.TermNet
+Copyright   : Galois, Inc. 2012-2014
+License     : BSD3
+Maintainer  : [email protected]
+Stability   : experimental
+Portability : non-portable (language extensions)
+-}
+
 module Verifier.SAW.TermNet
   ( Pat(..)
   , Pattern(..)

src/Verifier/SAW/Typechecker.hs

@@ -9,6 +9,16 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TupleSections #-}
 {-# LANGUAGE ViewPatterns #-}
+
+{- |
+Module      : Verifier.SAW.Typechecker
+Copyright   : Galois, Inc. 2012-2014
+License     : BSD3
+Maintainer  : [email protected]
+Stability   : experimental
+Portability : non-portable (language extensions)
+-}
+
 module Verifier.SAW.Typechecker
   ( tcModule
   ) where

src/Verifier/SAW/Typechecker/Context.hs

@@ -6,6 +6,16 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE TupleSections #-}
 {-# LANGUAGE ViewPatterns #-}
+
+{- |
+Module      : Verifier.SAW.Typechecker.Context
+Copyright   : Galois, Inc. 2012-2014
+License     : BSD3
+Maintainer  : [email protected]
+Stability   : experimental
+Portability : non-portable (language extensions)
+-}
+
 module Verifier.SAW.Typechecker.Context
   ( -- * Term definitions
     TCTerm(..)