refactoring: split literate-unitb into

* literate-unitb-verifier
* literate-unitb-synthesis
* literate-unitb-docs
* literate-unitb-cli

Author: cipher1024

.travis.yml

@@ -29,7 +29,10 @@ cache:
   - $HOME/build/unitb/literate-unitb-complete/literate-unitb-logic/.stack-work/ 
   - $HOME/build/unitb/literate-unitb-complete/literate-unitb-scripts/.stack-work/ 
   - $HOME/build/unitb/literate-unitb-complete/literate-unitb-utils/.stack-work/ 
-  - $HOME/build/unitb/literate-unitb-complete/literate-unitb/.stack-work/ 
+  - $HOME/build/unitb/literate-unitb-complete/literate-unitb-verifier/.stack-work/ 
+  - $HOME/build/unitb/literate-unitb-complete/literate-unitb-cli/.stack-work/ 
+  - $HOME/build/unitb/literate-unitb-complete/literate-unitb-docs/.stack-work/ 
+  - $HOME/build/unitb/literate-unitb-complete/literate-unitb-synthesis/.stack-work/ 
   - $HOME/build/unitb/literate-unitb-complete/syntax-error/.stack-work/
   - $HOME/build/unitb/literate-unitb-complete/unitb-testing/.stack-work/
   - $HOME/build/unitb/literate-unitb-complete/libs/bipartite-graph/.stack-work/
@@ -182,85 +185,103 @@ jobs:
     compiler: ": #stack default"
     addons: {apt: {packages: [libgmp-dev]}}
     script: 
-      - travis_long stack --no-terminal $ARGS build literate-unitb --bench --no-run-benchmarks
+      - travis_long stack --no-terminal $ARGS build literate-unitb-verifier literate-unitb-docs literate-unitb-synthesis literate-unitb-cli --bench --no-run-benchmarks
 
   - env: BUILD=stack ARGS="--stack-yaml stack-lts-3.yaml"
     compiler: ": #stack 7.10.2"
     addons: {apt: {packages: [libgmp-dev]}}
     script: 
-      - travis_long stack --no-terminal $ARGS build literate-unitb --bench --no-run-benchmarks
+      - travis_long stack --no-terminal $ARGS build literate-unitb-verifier literate-unitb-docs literate-unitb-synthesis literate-unitb-cli --bench --no-run-benchmarks
 
   - env: BUILD=stack ARGS="--stack-yaml stack-lts-6.yaml"
     compiler: ": #stack 7.10.3"
     addons: {apt: {packages: [libgmp-dev]}}
     script: 
-      - travis_long stack --no-terminal $ARGS build literate-unitb --bench --no-run-benchmarks
+      - travis_long stack --no-terminal $ARGS build literate-unitb-verifier literate-unitb-docs literate-unitb-synthesis literate-unitb-cli --bench --no-run-benchmarks
 
   - env: BUILD=stack ARGS="--stack-yaml stack-lts-7.yaml"
     compiler: ": #stack 8.0.1"
     addons: {apt: {packages: [libgmp-dev]}}
     script: 
-      - travis_long stack --no-terminal $ARGS build literate-unitb --bench --no-run-benchmarks
+      - travis_long stack --no-terminal $ARGS build literate-unitb-verifier literate-unitb-docs literate-unitb-synthesis literate-unitb-cli --bench --no-run-benchmarks
 
   - env: BUILD=stack ARGS="--stack-yaml stack-lts-8.yaml"
     compiler: ": #stack 8.0.2"
     addons: {apt: {packages: [libgmp-dev]}}
     script: 
-      - travis_long stack --no-terminal $ARGS build literate-unitb --bench --no-run-benchmarks
+      - travis_long stack --no-terminal $ARGS build literate-unitb-verifier literate-unitb-docs literate-unitb-synthesis literate-unitb-cli --bench --no-run-benchmarks
 
   - env: BUILD=stack ARGS="--stack-yaml stack-nightly.yaml --resolver nightly"
     compiler: ": #stack nightly"
     addons: {apt: {packages: [libgmp-dev]}}
     script: 
-      - travis_long stack --no-terminal $ARGS build literate-unitb --bench --no-run-benchmarks
+      - travis_long stack --no-terminal $ARGS build literate-unitb-verifier literate-unitb-docs literate-unitb-synthesis literate-unitb-cli --bench --no-run-benchmarks
 
   - stage: Test Literate Unit-B
     env: BUILD=stack ARGS=""
     compiler: ": #stack default"
     addons: {apt: {packages: [libgmp-dev]}}
     script: 
       - unitb-option --capacity $Z3_CAPACITY --hard-timeout $Z3_HARD_TIMEOUT --default-timeout $Z3_DEFAULT_TIMEOUT
-      - travis_long stack --no-terminal $ARGS test literate-unitb --bench --no-run-benchmarks
+      - travis_long stack --no-terminal $ARGS test literate-unitb-verifier --bench --no-run-benchmarks
+      - travis_long stack --no-terminal $ARGS test literate-unitb-docs --bench --no-run-benchmarks
+      - travis_long stack --no-terminal $ARGS test literate-unitb-synthesis --bench --no-run-benchmarks
+      - travis_long stack --no-terminal $ARGS test literate-unitb-cli --bench --no-run-benchmarks
 
   - env: BUILD=stack ARGS="--stack-yaml stack-lts-3.yaml"
     compiler: ": #stack 7.10.2"
     addons: {apt: {packages: [libgmp-dev]}}
     script: 
       - unitb-option --capacity $Z3_CAPACITY --hard-timeout $Z3_HARD_TIMEOUT --default-timeout $Z3_DEFAULT_TIMEOUT
-      - travis_long stack --no-terminal $ARGS test literate-unitb --bench --no-run-benchmarks
+      - travis_long stack --no-terminal $ARGS test literate-unitb-verifier --bench --no-run-benchmarks
+      - travis_long stack --no-terminal $ARGS test literate-unitb-docs --bench --no-run-benchmarks
+      - travis_long stack --no-terminal $ARGS test literate-unitb-synthesis --bench --no-run-benchmarks
+      - travis_long stack --no-terminal $ARGS test literate-unitb-cli --bench --no-run-benchmarks
 
   - env: BUILD=stack ARGS="--stack-yaml stack-lts-6.yaml"
     compiler: ": #stack 7.10.3"
     addons: {apt: {packages: [libgmp-dev]}}
     script: 
       - unitb-option --capacity $Z3_CAPACITY --hard-timeout $Z3_HARD_TIMEOUT --default-timeout $Z3_DEFAULT_TIMEOUT
-      - travis_long stack --no-terminal $ARGS test literate-unitb --bench --no-run-benchmarks
+      - travis_long stack --no-terminal $ARGS test literate-unitb-verifier --bench --no-run-benchmarks
+      - travis_long stack --no-terminal $ARGS test literate-unitb-docs --bench --no-run-benchmarks
+      - travis_long stack --no-terminal $ARGS test literate-unitb-synthesis --bench --no-run-benchmarks
+      - travis_long stack --no-terminal $ARGS test literate-unitb-cli --bench --no-run-benchmarks
 
   - env: BUILD=stack ARGS="--stack-yaml stack-lts-7.yaml"
     compiler: ": #stack 8.0.1"
     addons: {apt: {packages: [libgmp-dev]}}
     script: 
       - unitb-option --capacity $Z3_CAPACITY --hard-timeout $Z3_HARD_TIMEOUT --default-timeout $Z3_DEFAULT_TIMEOUT
-      - travis_long stack --no-terminal $ARGS test literate-unitb --bench --no-run-benchmarks
+      - travis_long stack --no-terminal $ARGS test literate-unitb-verifier --bench --no-run-benchmarks
+      - travis_long stack --no-terminal $ARGS test literate-unitb-docs --bench --no-run-benchmarks
+      - travis_long stack --no-terminal $ARGS test literate-unitb-synthesis --bench --no-run-benchmarks
+      - travis_long stack --no-terminal $ARGS test literate-unitb-cli --bench --no-run-benchmarks
 
   - env: BUILD=stack ARGS="--stack-yaml stack-lts-8.yaml"
     compiler: ": #stack 8.0.2"
     addons: {apt: {packages: [libgmp-dev]}}
     script: 
       - unitb-option --capacity $Z3_CAPACITY --hard-timeout $Z3_HARD_TIMEOUT --default-timeout $Z3_DEFAULT_TIMEOUT
-      - travis_long stack --no-terminal $ARGS test literate-unitb --bench --no-run-benchmarks
+      - travis_long stack --no-terminal $ARGS test literate-unitb-verifier --bench --no-run-benchmarks
+      - travis_long stack --no-terminal $ARGS test literate-unitb-docs --bench --no-run-benchmarks
+      - travis_long stack --no-terminal $ARGS test literate-unitb-synthesis --bench --no-run-benchmarks
+      - travis_long stack --no-terminal $ARGS test literate-unitb-cli --bench --no-run-benchmarks
 
   - env: BUILD=stack ARGS="--stack-yaml stack-nightly.yaml --resolver nightly"
     compiler: ": #stack nightly"
     addons: {apt: {packages: [libgmp-dev]}}
     script: 
       - unitb-option --capacity $Z3_CAPACITY --hard-timeout $Z3_HARD_TIMEOUT --default-timeout $Z3_DEFAULT_TIMEOUT
-      - travis_long stack --no-terminal $ARGS test literate-unitb --bench --no-run-benchmarks
+      - travis_long stack --no-terminal $ARGS test literate-unitb-verifier --bench --no-run-benchmarks
+      - travis_long stack --no-terminal $ARGS test literate-unitb-docs --bench --no-run-benchmarks
+      - travis_long stack --no-terminal $ARGS test literate-unitb-synthesis --bench --no-run-benchmarks
+      - travis_long stack --no-terminal $ARGS test literate-unitb-cli --bench --no-run-benchmarks
 
   allow_failures:
   - env: BUILD=cabal GHCVER=7.10.3 CABALVER=1.22 HAPPYVER=1.19.5 ALEXVER=3.1.7 STACKARGS=""
   # - env: BUILD=cabal GHCVER=head  CABALVER=head HAPPYVER=1.19.5 ALEXVER=3.1.7
-  - env: BUILD=stack ARGS="--stack-yaml stack-nightly.yaml"
+  - env: BUILD=stack ARGS="--stack-yaml stack-nightly.yaml --resolver nightly"
   # - env: BUILD=stack ARGS="--resolver lts-8 --stack-yaml stack-nightly.yaml"
   # - env: BUILD=cabal GHCVER=8.0.1 CABALVER=1.24 HAPPYVER=1.19.5 ALEXVER=3.1.7 STACKARGS=""
   # - env: BUILD=cabal GHCVER=8.0.2 CABALVER=1.24 HAPPYVER=1.19.5 ALEXVER=3.1.7 STACKARGS="--stack-yaml stack-nightly.yaml"

literate-unitb-cli/ChangeLog.md

@@ -0,0 +1,5 @@
+# Revision history for literate-unitb-cli
+
+## 0.1.0.0  -- YYYY-mm-dd
+
+* First version. Released on an unsuspecting world.

literate-unitb-cli/LICENSE

@@ -0,0 +1,20 @@
+Copyright (c) 2017 Simon Hudon
+
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be included
+in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

literate-unitb/Setup.hs literate-unitb-cli/Setup.hs

@@ -0,0 +1,3 @@
+module Main (main) where
+
+import Continuous

literate-unitb-cli/app/Main.hs

@@ -0,0 +1,23 @@
+{-# LANGUAGE TemplateHaskell #-}
+module Main where
+
+import Data.List
+import Data.Version
+import Development.GitRev
+import Paths_literate_unitb_cli
+
+import System.Environment
+import Text.Printf.TH
+
+printUnitBZipName :: [String] -> IO ()
+printUnitBZipName os = do
+        let v = showVersion version
+            h = take 12 $gitHash
+        putStrLn $ [s|literate-unitb-cli-%s-%s-%s|] v (intercalate "-" os) h
+
+main :: IO ()
+main = do
+    xs <- getArgs
+    if null xs 
+        then putStrLn "usage: unitb-zip-name os"
+        else printUnitBZipName xs

literate-unitb-cli/app/ZipName.hs

@@ -0,0 +1,100 @@
+-- Initial literate-unitb-cli.cabal generated by cabal init.  For further 
+-- documentation, see http://haskell.org/cabal/users-guide/
+
+name:                literate-unitb-cli
+version:             0.1.0.0
+synopsis:            Command line interface for Literate Unit-B verifier
+-- description:         
+homepage:            unitb.github.io
+license:             MIT
+license-file:        LICENSE
+author:              Simon Hudon
+maintainer:          [email protected]
+-- copyright:           
+category:            Development
+build-type:          Simple
+extra-source-files:  ChangeLog.md
+cabal-version:       >=1.10
+
+library
+  exposed-modules:
+        Interactive.Observable
+        Interactive.Pipeline
+        Interactive.Serialize
+        Paths_literate_unitb_cli
+        Continuous
+  build-depends:       base >=4.9 && <4.10,
+                       file-system-mockup,
+                       directory,
+                       generic-instances,
+                       cereal,
+                       containers,
+                       unordered-containers,
+                       control-invariants,
+                       either,
+                       bytestring,
+                       mtl,
+                       parallel,
+                       lens-extra,
+                       lens,
+                       deepseq,
+                       literate-unitb-verifier,
+                       literate-unitb-logic,
+                       literate-unitb-utils,
+                       literate-unitb-config,
+                       literate-unitb-docs,
+                       syntax-error,
+                       th-printf,
+                       filepath,
+                       text,
+                       data-default,
+                       transformers,
+                       process,
+                       ansi-terminal,
+                       stm,
+                       pseudomacros,
+                       time,
+                       gitrev
+  hs-source-dirs:      src
+  default-extensions:  QuasiQuotes, TemplateHaskell, DeriveGeneric, FlexibleContexts, TypeSynonymInstances, FlexibleInstances, OverloadedStrings
+  default-language:    Haskell2010
+
+executable unitb
+  -- .hs or .lhs file containing the Main module.
+  hs-source-dirs: app
+  main-is:             Main.hs
+  default-language:    Haskell2010
+
+  build-depends:       base >=4.8 && < 5, directory >= 1.2.2.0, either, control-invariants, lens, literate-unitb-verifier, literate-unitb-logic, literate-unitb-utils, mtl, pseudomacros, time, file-system-mockup, containers, lens-extra, literate-unitb-config, syntax-error, gitrev, text, literate-unitb-cli
+
+  ghc-options: -W -fwarn-missing-signatures 
+         -fwarn-incomplete-uni-patterns
+         -fwarn-missing-methods
+         -threaded  -fno-ignore-asserts
+         -fwarn-tabs
+         -j8
+  
+  -- LANGUAGE extensions used by modules in this package.
+  default-extensions:  TupleSections, DeriveFunctor, DeriveGeneric, DeriveFoldable, RankNTypes, MultiParamTypeClasses, GeneralizedNewtypeDeriving, TemplateHaskell, FlexibleContexts, FlexibleInstances, DeriveDataTypeable, TypeSynonymInstances, DefaultSignatures, DeriveTraversable, FunctionalDependencies, ImplicitParams, QuasiQuotes, OverloadedStrings
+
+executable unitb-zip-name
+  -- .hs or .lhs file containing the Main module.
+  hs-source-dirs: app
+  main-is:  ZipName.hs
+  default-language:    Haskell2010
+
+  build-depends:       base >=4.8 && < 5
+      , th-printf
+      , literate-unitb-cli
+      , gitrev
+
+  ghc-options: -W -fwarn-missing-signatures 
+         -fwarn-incomplete-uni-patterns
+         -fwarn-missing-methods
+         -threaded  -fno-ignore-asserts
+         -fwarn-tabs
+         -j8
+  
+  -- LANGUAGE extensions used by modules in this package.
+  default-extensions:  TupleSections, DeriveFunctor, DeriveGeneric, DeriveFoldable, RankNTypes, MultiParamTypeClasses, GeneralizedNewtypeDeriving, TemplateHaskell, FlexibleContexts, FlexibleInstances, DeriveDataTypeable, TypeSynonymInstances, DefaultSignatures, DeriveTraversable, FunctionalDependencies, ImplicitParams, QuasiQuotes
+

literate-unitb-cli/literate-unitb-cli.cabal

@@ -1,7 +1,4 @@
-#!/usr/bin/env runhaskell
-module Main 
-    (main)
-where
+module Continuous where
 
     -- Modules
 import Interactive.Pipeline
@@ -10,7 +7,7 @@ import Documentation.SummaryGen
 
 import Logic.Expr
 
-import Paths_literate_unitb
+-- import Paths_literate_unitb
 
 import Language.UnitB hiding (timeout)
 import Language.UnitB.PO
@@ -42,6 +39,7 @@ import Development.GitRev
 import Interactive.Serialize hiding (dump_pos)
 
 import PseudoMacros
+import Paths_literate_unitb_cli
 
 import System.Console.GetOpt
 import System.Directory

literate-unitb/app/Continuous.hs literate-unitb-cli/src/Continuous.hs

@@ -1,4 +1,4 @@
-{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE RecordWildCards,OverloadedStrings #-}
 module Interactive.Pipeline 
    ( run_pipeline, Params' (..), Params, pos )
 where

literate-unitb/src/Interactive/Cpipeline.hs literate-unitb-cli/src/Interactive/Cpipeline.hs

@@ -0,0 +1,5 @@
+# Revision history for literate-unitb-docs
+
+## 0.1.0.0  -- YYYY-mm-dd
+
+* First version. Released on an unsuspecting world.

literate-unitb/src/Interactive/Observable.hs literate-unitb-cli/src/Interactive/Observable.hs

@@ -0,0 +1,20 @@
+Copyright (c) 2017 Simon Hudon
+
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be included
+in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.

literate-unitb/src/Interactive/Pipeline.hs literate-unitb-cli/src/Interactive/Pipeline.hs

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