claferIG 0.3.7 → 0.3.8
raw patch · 16 files changed
+323/−338 lines, 16 filesdep ~claferdep ~claferIGPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: clafer, claferIG
API changes (from Hackage documentation)
Files
- CHANGES.md +4/−19
- Makefile +5/−5
- README.md +8/−8
- alloyIG.jar binary
- claferIG.cabal +26/−26
- src/Language/Clafer/IG/AlloyIGInterface.hs +16/−16
- src/Language/Clafer/IG/ClaferIG.hs +50/−49
- src/Language/Clafer/IG/ClaferModel.hs +11/−11
- src/Language/Clafer/IG/CommandLine.hs +74/−74
- src/Language/Clafer/IG/CommandLineParser.hs +23/−23
- src/Language/Clafer/IG/Constraints.hs +2/−2
- src/Language/Clafer/IG/JSONGenerator.hs +37/−40
- src/Language/Clafer/IG/Process.hs +5/−5
- src/Language/Clafer/IG/Solution.hs +5/−5
- src/Language/Clafer/IG/Sugarer.hs +27/−25
- test/test-suite.hs +30/−30
CHANGES.md view
@@ -1,3 +1,7 @@+**ClaferIG Version 0.3.8 released on Jan 27, 2015** + +[Release](https://github.com/gsdlab/claferIG/pull/23) + **ClaferIG Version 0.3.7 released on Oct 23, 2014** [Release](https://github.com/gsdlab/claferIG/pull/22) @@ -14,35 +18,16 @@ [Release](https://github.com/gsdlab/claferIG/pull/17) -[New features and bug fixes](http://gsd.uwaterloo.ca:8888/questions/scope:all/sort:activity-desc/tags:v0.3.5,claferig/page:1/) - **ClaferIG Version 0.3.4 released on September 20, 2013** -[New features and bug fixes](http://gsd.uwaterloo.ca:8888/questions/scope:all/sort:activity-desc/tags:v0.3.4,claferig/page:1/) - **ClaferIG Version 0.3.3 released on August 14, 2013** [Release](https://github.com/gsdlab/claferIG/pull/12) -[New features and bug fixes](http://gsd.uwaterloo.ca:8888/questions/scope:all/sort:activity-desc/tags:v0.3.3,claferig/page:1/) - **ClaferIG Version 0.3.2 released on April 11, 2013** -[New features and bug fixes](http://gsd.uwaterloo.ca:8888/questions/scope:all/sort:activity-desc/tags:v0.3.2,claferig/page:1/) - **ClaferIG Version 0.3.1 released on October 17, 2012** -[New features and bug fixes](http://gsd.uwaterloo.ca:8888/questions/scope:all/sort:activity-desc/tags:v0.3.1,claferig/page:1/) - **ClaferIG Version 0.3 released on July 17, 2012** This was the first release of Clafer Instance Generator and included all code since the beginning of the project. - -[New features and bug fixes](http://gsd.uwaterloo.ca:8888/questions/scope:all/sort:activity-desc/tags:v0.3,claferig/page:1/) - -Undocumented features - See the `README.md`. - - - - -
Makefile view
@@ -21,9 +21,9 @@ make clean ghc-pkg unregister claferIG rm `which claferIG` - make + make -# this takes the version from the .cabal file. Need to run install first to produce Paths_claferIG.hs +# this takes the version from the .cabal file. Need to run install first to produce Paths_claferIG.hs newVersion: ghc -isrc src/dateVer.hs dist/build/autogen/Paths_claferIG.hs -outputdir dist/build --make -o dateVer ./dateVer > src/Language/Clafer/IG/Version.hs @@ -40,7 +40,7 @@ alloyIG.jar: src/manifest src/org/clafer/ig/AlloyIG.java src/manifest src/org/clafer/ig/Util.java src/org/clafer/ig/AlloyIGException.java src/edu/mit/csail/sdg/alloy4compiler/parser/AlloyCompiler.java $(MAKE) -C $(TOOL_DIR) mkdir -p dist/javabuild - javac -source 1.6 -target 1.6 -cp "tools/alloy4.2.jar" -d dist/javabuild src/org/clafer/ig/AlloyIG.java src/org/clafer/ig/Util.java src/org/clafer/ig/AlloyIGException.java src/edu/mit/csail/sdg/alloy4compiler/parser/AlloyCompiler.java + javac -cp "tools/alloy4.2.jar" -d dist/javabuild src/org/clafer/ig/AlloyIG.java src/org/clafer/ig/Util.java src/org/clafer/ig/AlloyIGException.java src/edu/mit/csail/sdg/alloy4compiler/parser/AlloyCompiler.java jar cfm alloyIG.jar src/manifest -C dist/javabuild org/clafer/ig/ -C dist/javabuild edu lib: @@ -51,7 +51,7 @@ chmod +x lib/$(LIB); \ cp lib/$(LIB) lib; \ fi - + test: # Only test a subset of the suite. The other cases do not work yet. cabal configure --enable-tests @@ -65,7 +65,7 @@ cp -r lib/ dist/build/claferIG/ # On Windows, also need to manually copy glpk_4_52.dll to dist/build/test-suite/ cabal test - + clean: rm -rf dist rm -f alloyIG.jar
README.md view
@@ -1,7 +1,7 @@ Clafer Instance Generator ========================= -v0.3.7 +v0.3.8 [Clafer](http://clafer.org) is a powerful (equivalent to first-order predicate logic) yet lightweight structural modeling language. Despite simplicity and conciseness of Clafer, writing correct models remains challenging due to hard-to-predict interactions among all constraints expressed in the model. **Clafer instance generator** (ClaferIG) is an interactive tool that generates instances and counter examples of concrete clafers in a Clafer model. If the concrete clafers do not have contradicting constraints, the generator produces valid instance data. Otherwise, the generator produces an unsatisfiable core which included all contradicting constraints and generates a counter example by removing one constraint from the core. The generator can potentially produce many instances if the concrete clafers are not fully specialized. The generator produces different instances on-demand. With these capabilities, the instance generator can be used for debugging models: checking the consistency of the model and detecting under- and overconstraining of the model. The instance generator can also be used programmatically via API (the command line and interactive session interfaces only use the API). @@ -24,13 +24,13 @@ Regardless of the installation method, the following are required: -* [Clafer](https://github.com/gsdlab/clafer) v0.3.7 +* [Clafer](https://github.com/gsdlab/clafer) v0.3.8 * [Java Platform (JDK)](http://www.oracle.com/technetwork/java/javase/downloads/index.html) v7+, 32bit * [Alloy4.2](http://alloy.mit.edu/alloy/download.html) ### Installation from binaries -Binary distributions of the release 0.3.7 of Clafer Tools for Windows, Mac, and Linux, +Binary distributions of the release 0.3.8 of Clafer Tools for Windows, Mac, and Linux, can be downloaded from [Clafer Tools - Binary Distributions](http://http://gsd.uwaterloo.ca/clafer-tools-binary-distributions). 1. download the binaries and unpack `<target directory>` of your choice @@ -42,11 +42,11 @@ * [The Haskell Platform](http://hackage.haskell.org/platform/) v2013.2.0.0 -ClaferIG is now available on [Hackage](http://hackage.haskell.org/package/claferIG-0.3.7/) and it can be installed using +ClaferIG is now available on [Hackage](http://hackage.haskell.org/package/claferIG-0.3.8/) and it can be installed using 1. `cabal update` 2. `cabal install claferIG` -3. `cd <cabal's lib or share folder>` (`C:\Users\<user>\AppData\Roaming\cabal\i386-windows-ghc-7.6.3\claferIG-0.3.7` on Windows or `.cabal/share/x86_64-linux-ghc-7.6.3/claferIG-0.3.7/` on Linux) +3. `cd <cabal's lib or share folder>` (`C:\Users\<user>\AppData\Roaming\cabal\i386-windows-ghc-7.6.3\claferIG-0.3.8` on Windows or `.cabal/share/x86_64-linux-ghc-7.6.3/claferIG-0.3.8/` on Linux) 3. to automatically download Alloy4.2 jar * execute `make` in `tools` 4. To get the `minisatproover` library @@ -112,7 +112,7 @@ (As printed by `claferIG --help`) -``` v0.3.7 +``` v0.3.8 igaONS] FILE @@ -164,7 +164,7 @@ ``` ------------------ -| ClaferIG 0.3.7 | +| ClaferIG 0.3.8 | ------------------ You can invoke the following commands as indicated by single quotes: @@ -317,4 +317,4 @@ * Try a live instance of [ClaferMooVisualizer](http://t3-necsis.cs.uwaterloo.ca:8092) * Take a look at (incomplete) [Clafer by examples wiki](https://github.com/gsdlab/clafer/wiki) * Browse example models in the [test suite](https://github.com/gsdlab/clafer/tree/master/test/positive) and [MOO examples](https://github.com/gsdlab/clafer/tree/master/spl_configurator/dataset) -* Post questions, report bugs, suggest improvements [GSD Lab Bug Tracker](http://gsd.uwaterloo.ca:8888/questions/). Tag your entries with `clafer` (so that we know what they are related to) and with `jimmy-liang` or `michal` (so that Jimmy or Michał gets a notification).+* Post questions, report bugs, suggest improvements [GSD Lab Bug Tracker](http://gsd.uwaterloo.ca:8888/questions/). Tag your entries with `clafer` (so that we know what they are related to) and with `jimmy-liang` or `michal` (so that Jimmy or Michał gets a notification).
alloyIG.jar view
binary file changed (22360 → 22370 bytes)
claferIG.cabal view
@@ -1,5 +1,5 @@ Name: claferIG -Version: 0.3.7 +Version: 0.3.8 Synopsis: claferIG is an interactive tool that generates instances of Clafer models. Description: Clafer is a powerful (equivalent to first-order predicate logic) yet lightweight structural modeling language. Despite simplicity and conciseness of Clafer, writing correct models remains challenging due to hard-to-predict interactions among all constraints expressed in the model. Clafer instance generator (ClaferIG) is an interactive tool that generates instances and counter examples of concrete clafers in a Clafer model. If the concrete clafers do not have contradicting constraints, the generator produces valid instance data. Otherwise, the generator produces an unsatisfiable core which included all contradicting constraints and generates a counter example by removing one constraint from the core. The generator can potentially produce many instances if the concrete clafers are not fully specialized. The generator produces different instances on-demand. With these capabilities, the instance generator can be used for debugging models: checking the consistency of the model and detecting under- and overconstraining of the model. The instance generator can also be used programmatically via API (the command line and interactive session interfaces only use the API). Homepage: https://github.com/gsdlab/claferIG @@ -16,7 +16,7 @@ CHANGES.md, Makefile, lib/minisatprover.md, - tools/Makefile + tools/Makefile source-repository head type: git location: git://github.com/gsdlab/claferIG.git @@ -26,48 +26,48 @@ default-extensions: DeriveDataTypeable Main-is: Main.hs - Build-depends: + Build-depends: base >= 4.6.0.1 && < 5, - clafer == 0.3.7, - claferIG == 0.3.7, - cmdargs >= 0.10.7, - containers >= 0.5.0.0, - directory >= 1.2.0.1, - executable-path >= 0.0.3, - filepath >= 1.3.0.1, - haskeline >= 0.7.1.2, + clafer == 0.3.8, + claferIG == 0.3.8, + cmdargs >= 0.10.7, + containers >= 0.5.0.0, + directory >= 1.2.0.1, + executable-path >= 0.0.3, + filepath >= 1.3.0.1, + haskeline >= 0.7.1.2, mtl >= 2.1.2, transformers >= 0.3.0.0 other-modules: Paths_claferIG Hs-Source-Dirs: src-cmd ghc-options: -Wall -fno-warn-unused-do-bind -fno-warn-orphans -rtsopts -library +library build-tools: ghc >= 7.6.3 default-language: Haskell2010 default-extensions: DeriveDataTypeable build-depends: array >= 0.4.0.1, base >= 4.6.0.1 && < 5, containers >= 0.5.0.0, - directory >= 1.2.0.1, + directory >= 1.2.0.1, filepath >= 1.3.0.1, - process >= 1.1.0.2, + process >= 1.1.0.2, - mtl >= 2.1.2, + mtl >= 2.1.2, parsec >= 3.1.3, transformers >= 0.3.0.0, data-stringmap >= 1.0.1.1, - executable-path >= 0.0.3, + executable-path >= 0.0.3, haskeline >= 0.7.1.2, - HaXml >= 1.24, - json-builder >= 0.3, + HaXml >= 1.24, + json-builder >= 0.3, string-conversions >= 0.3.0.2, - clafer == 0.3.7 + clafer == 0.3.8 hs-source-dirs: src ghc-options: -Wall -fno-warn-unused-do-bind -fno-warn-orphans -rtsopts - exposed-modules: Language.Clafer.IG.AlloyIGInterface, + exposed-modules: Language.Clafer.IG.AlloyIGInterface, Language.Clafer.IG.ClaferIG, Language.Clafer.IG.ClaferModel, Language.Clafer.IG.CommandLine, @@ -79,24 +79,24 @@ Language.Clafer.IG.Sugarer other-modules: Paths_claferIG Test-Suite test-suite - type: exitcode-stdio-1.0 + type: exitcode-stdio-1.0 default-language: Haskell2010 main-is: test-suite.hs hs-source-dirs: test build-depends: array >= 0.4.0.1, base >= 4.6.0.1 && < 5, - directory >= 1.2.0.1, + directory >= 1.2.0.1, filepath >= 1.3.0.1, HUnit >= 1.2.5.2, transformers >= 0.3.0.0, - cmdargs >= 0.10.7, + cmdargs >= 0.10.7, tasty >= 0.10, tasty-hunit >= 0.9, tasty-th >= 0.1.2, - clafer == 0.3.7, - claferIG == 0.3.7 + clafer == 0.3.8, + claferIG == 0.3.8 other-modules: Paths_claferIG - ghc-options: -Wall -fno-warn-unused-do-bind -fno-warn-orphans+ ghc-options: -Wall -fno-warn-unused-do-bind -fno-warn-orphans
src/Language/Clafer/IG/AlloyIGInterface.hs view
@@ -82,12 +82,12 @@ do execPath <- liftIO $ executableDirectory proce <- liftIO $ pipeProcess "java" ["-Djava.library.path=" ++ execPath ++ "lib" , "-jar", execPath ++ "alloyIG.jar"] - + runReaderT (evalStateT (unwrap run) Nothing) proce where unwrap (AlloyIGT a) = a - + getAlloyModel :: MonadIO m => AlloyIGT m String getAlloyModel = fetches alloyModel @@ -107,7 +107,7 @@ let sigMap' = fromList [(s_name sig, sig) | sig <- sigs] let scopes' = Map.empty globalScope' <- readMessage proce - + return $ AlloyIGEnv alloyModel' sigMap' scopes' globalScope' where readSig = @@ -127,7 +127,7 @@ proc' <- proc env <- liftIO $ load proc' alloyModel' set env - + sigs <- elems `liftM` fetches sigMap mapM_ resetScope sigs where @@ -155,19 +155,19 @@ case Map.lookup sig rscopes of Just scope -> return scope Nothing -> getGlobalScope - + getScopes :: MonadIO m => AlloyIGT m [(String, Integer)] getScopes = toList `liftM` fetches scopes - + -- | Tell alloyIG to change the scope of a sig sendSetScopeCommand :: MonadIO m => String -> Integer -> AlloyIGT m (Maybe String) sendSetScopeCommand sig scope = do sigMap' <- fetches sigMap let Sig{s_multiplicity = multiplicity, s_subset = subset} = sigMap' ! sig - + -- Alloy has a fit when trying to set a scope outside its multiplicity -- Don't send command if outside its multiplicity but continue the illusion that -- the scope was set @@ -185,8 +185,8 @@ return $ Nothing Just sub -> return $ Just sub - + getGlobalScope :: MonadIO m => AlloyIGT m Integer getGlobalScope = fetches globalScope @@ -197,7 +197,7 @@ do putMsg "setGlobalScope" putMsg $ show scope - + env <- fetch set env {globalScope = scope} @@ -220,15 +220,15 @@ -- | Tell alloyIG to remove the constraint sendRemoveConstraintCommand :: MonadIO m => Span -> AlloyIGT m () sendRemoveConstraintCommand s = case s of - (Span from to) -> + (Span from to) -> do putMsg "removeConstraint" sendPosition from >> sendPosition to where sendPosition (Pos line column) = - putMsg (show line) >> putMsg (show column) + putMsg (show line) >> putMsg (show column) --- | Tell alloyIG to return the unsat core of the previous operation +-- | Tell alloyIG to return the unsat core of the previous operation sendUnsatCoreCommand :: MonadIO m => AlloyIGT m UnsatCore sendUnsatCoreCommand = do @@ -239,8 +239,8 @@ where readPosition = liftM2 Pos readMsg readMsg readConstraint = liftM2 Span readPosition readPosition - - + + -- | Tell alloyIG to change the unsat core minimization level. -- 0 -> Fastest, -- 1 -> Medium, @@ -250,9 +250,9 @@ do putMsg "unsatCoreMinimization" putMsg $ show level - --- | Tell alloyIG to change the bitwidth + +-- | Tell alloyIG to change the bitwidth sendSetBitwidthCommand :: MonadIO m => Integer -> AlloyIGT m () sendSetBitwidthCommand bitwidth = do
src/Language/Clafer/IG/ClaferIG.hs view
@@ -32,27 +32,27 @@ getClaferModel, getInfo, getStrMap, - ClaferIGT(..), - Instance(..), - Counterexample(..), - runClaferIGT, - getAlloyModel, - solve, - getClafers, - getGlobalScope, + ClaferIGT(..), + Instance(..), + Counterexample(..), + runClaferIGT, + getAlloyModel, + solve, + getClafers, + getGlobalScope, getBitwidth, - setGlobalScope, - getScopes, - getScope, + setGlobalScope, + getScopes, + getScope, getQNameMaps, - valueOfScope, - increaseScope, - setScope, - setAlloyScope, - next, - setUnsatCoreMinimization, - setBitwidth, - quit, + valueOfScope, + increaseScope, + setScope, + setAlloyScope, + next, + setUnsatCoreMinimization, + setBitwidth, + quit, reload, findRemovable, fst3, @@ -91,7 +91,7 @@ data IGArgs = IGArgs { all :: Maybe Integer, - saveDir :: Maybe FilePath, + saveDir :: Maybe FilePath, claferModelFile :: FilePath, alloySolution :: Bool, bitwidth :: Integer, @@ -136,8 +136,8 @@ data ClaferIGEnv = ClaferIGEnv{ claferEnv'::ClaferEnv, claferIGArgs :: IGArgs, - constraints:: [Constraint], - claferModel:: String, + constraints:: [Constraint], + claferModel:: String, qNameMaps :: QNameMaps, info :: Analysis.Info, strMap :: Map Int String, @@ -148,8 +148,8 @@ Instance {modelInstance::ClaferModel, alloyModelInstance::String} | UnsatCore {unsatConstraints::[Constraint], counterexample::Maybe Counterexample} | NoInstance - + data Counterexample = Counterexample {removedConstraints::[Constraint], counterexampleInstance::ClaferModel, counterexampleAlloyInstance::String} getClaferEnv :: Monad m => ClaferIGT m ClaferEnv @@ -177,30 +177,30 @@ load igArgs = runErrorT $ do claferModel <- liftIO $ strictReadFile claferFile' - - (claferEnv', alloyModel, mapping, sMap) <- ErrorT $ return $ callClaferTranslator claferModel + (claferEnv', alloyModel, mapping, sMap) <- ErrorT $ return $ callClaferTranslator claferModel + let ir = fst3 $ fromJust $ cIr claferEnv' let constraints = parseConstraints claferModel ir mapping - + lift $ AlloyIG.sendLoadCommand alloyModel lift $ AlloyIG.sendSetBitwidthCommand bitwidth' let qNameMaps = deriveQNameMaps ir - let info = Analysis.gatherInfo ir + let info = Analysis.gatherInfo ir let irTrace = editMap $ irModuleTrace claferEnv' return $ ClaferIGEnv claferEnv' igArgs constraints claferModel qNameMaps info sMap irTrace where editMap :: (Map.Map Span [Ir]) -> (Map.Map Integer String) -- Map Line Number to Clafer Name - editMap = - fromList . removeConstraints . Data.List.foldr (\(num, ir) acc -> case (getIClafer ir) of - Just (IClafer _ _ _ _ uid' _ _ _ _) -> (num, uid') : acc + editMap = + fromList . removeConstraints . Data.List.foldr (\(num, ir) acc -> case (getIClafer ir) of + Just (IClafer _ _ _ _ uid' _ _ _ _ _ _) -> (num, uid') : acc _ -> acc) [] . tail . (Data.List.foldr (\((Span (Pos l1 _) (Pos l2 _)), irs) acc -> (zip [l1..l2] (replicate (fromIntegral $ l2 - l1 + 1) irs)) ++ acc) []) . toList getIClafer :: [Ir] -> Maybe IClafer getIClafer [] = Nothing - getIClafer ((IRClafer c):_) = Just c + getIClafer ((IRClafer c):_) = Just c getIClafer (_:rs) = getIClafer rs removeConstraints :: [(Integer, String)] -> [(Integer, String)] removeConstraints = map swap . reverse . toList . fromList . reverse . map swap @@ -209,7 +209,8 @@ mapLeft ClaferErrs $ runClafer claferArgs $ do addModuleFragment code parse - compile + iModule <- desugar Nothing + compile iModule results <- generate let (Just alloyResult) = Map.lookup Alloy42 results return (claferEnv alloyResult, outputCode alloyResult, mappingToAlloy alloyResult, stringMap alloyResult) @@ -219,9 +220,9 @@ claferFile' = claferModelFile igArgs bitwidth' = bitwidth igArgs - -strictReadFile :: FilePath -> IO String -strictReadFile filePath = + +strictReadFile :: FilePath -> IO String +strictReadFile filePath = do contents <- readFile filePath -- readFile is lazy. Force it to evaluate by mapping over everything doing nothing @@ -236,7 +237,7 @@ solve :: MonadIO m => ClaferIGT m () solve = ClaferIGT $ lift AlloyIG.sendResolveCommand - + getClafers :: MonadIO m => ClaferIGT m [String] getClafers = do @@ -248,7 +249,7 @@ getGlobalScope = ClaferIGT $ lift AlloyIG.getGlobalScope getBitwidth :: MonadIO m => ClaferIGT m Integer -getBitwidth = +getBitwidth = do claferIGArgs' <- getClaferIGArgs return $ bitwidth claferIGArgs' @@ -259,8 +260,8 @@ getScopes :: MonadIO m => ClaferIGT m [ (String, Integer) ] getScopes = ClaferIGT $ lift AlloyIG.getScopes - - + + getScope :: MonadIO m => QName -> ClaferIGT m ([String]) getScope qName = do qNameMaps' <- fetches qNameMaps @@ -275,7 +276,7 @@ increaseScope :: MonadIO m => Integer -> (String, Integer) -> ClaferIGT m (Either String ()) increaseScope increment (sigName, value) = setAlloyScope (value + increment) sigName - + setScope :: MonadIO m => Integer -> (String, Integer) -> ClaferIGT m (Either String ()) setScope value (sigName, _) = setAlloyScope value sigName @@ -290,7 +291,7 @@ next = do env <- getClaferEnv claferIGArgs' <- getClaferIGArgs - let + let useUids' = useUids claferIGArgs' addTypes' = addTypes claferIGArgs' constraints' <- getConstraints @@ -325,7 +326,7 @@ counterexample' env'' core' (remove : removed) useUids''' addTypes''' info''' constraints' sMap' Nothing -> -- It is possible that none of the constraints are removable return NoInstance - + xmlToModel :: Bool -> Bool -> Analysis.Info -> String -> (Map Int String) -> ClaferModel xmlToModel useUids' addTypes' info' xml sMap = (sugarClaferModel useUids' addTypes' (Just info') $ buildClaferModel $ parseSolution xml) sMap @@ -337,8 +338,8 @@ env <- ErrorT $ ClaferIGT $ lift $ load claferIGArgs' lift $ set env lift $ setGlobalScope globalScope - - + + setUnsatCoreMinimization :: MonadIO m => Integer -> ClaferIGT m () setUnsatCoreMinimization level = ClaferIGT $ lift $ AlloyIG.sendSetUnsatCoreMinimizationCommand level @@ -350,11 +351,11 @@ set igEnv{claferIGArgs = claferIGArgs'{bitwidth=bitwidth'}} ClaferIGT $ lift $ AlloyIG.sendSetBitwidthCommand bitwidth' - + quit :: MonadIO m => ClaferIGT m () quit = ClaferIGT $ lift AlloyIG.sendQuitCommand - - + + sigToClaferName :: String -> String sigToClaferName n = case snd $ break ('_' ==) n of @@ -370,8 +371,8 @@ removeAbsZero absIDs (Just (UpperCardinalityConstraint _ (ClaferInfo uID (Cardinality 0 (Just 0))))) = ((Seq.elemIndexL uID absIDs)==Nothing) removeAbsZero _ _ = True getId :: Ir -> (Seq.Seq String) - getId (IRClafer (IClafer _ True _ uID _ _ _ _ _)) = Seq.singleton uID + getId (IRClafer (IClafer _ True _ uID _ _ _ _ _ _ _)) = Seq.singleton uID getId _ = mempty fst3 :: (IModule, GEnv, Bool) -> IModule -fst3 (imod, _, _) = imod+fst3 (imod, _, _) = imod
src/Language/Clafer/IG/ClaferModel.hs view
@@ -22,7 +22,7 @@ module Language.Clafer.IG.ClaferModel (ClaferModel(..), Clafer(..), Id(..), Value(..), c_name, buildClaferModel, traverse) where -import Data.List +import Data.List import Data.Either import Data.Map as Map hiding (filter, map, foldr, singleton) import Data.Maybe @@ -64,11 +64,11 @@ indent ++ i_name id ++ maybe "" displayValue value ++ "\n" ++ concatMap (displayClafer $ indent ++ " ") children displayValue (AliasValue alias) = " = " ++ i_name alias - displayValue (IntValue value) = " = " ++ show value + displayValue (IntValue value) = " = " ++ show value displayValue (StringValue value) = " = " ++ value - + traverse :: ClaferModel -> [Clafer] traverse (ClaferModel clafers) = traverseClafers clafers @@ -110,16 +110,16 @@ renameSigLabel label | label `elem` ["univ", "Int", "seq/Int", "String"] = label | otherwise = fromMaybe (error $ "Unexpected sig label " ++ label) $ dropDelimiter '/' label - + renameField field = field{f_label = renameFieldLabel $ f_label field} renameFieldLabel "ref" = "ref" renameFieldLabel label = fromMaybe (error $ "Unexpected field label " ++ label) $ dropDelimiter '_' label - + dropDelimiter char string = case snd $ break (== char) string of [] -> Nothing x -> Just $ tail x --} +-} buildFamilyTree :: Solution -> FamilyTree buildFamilyTree (Solution sigs fields) = @@ -129,7 +129,7 @@ asNodes Sig{s_id = id, s_atoms = atoms} = map (flip ClaferNode id) $ map (labelAsId . a_label) atoms rootNodes :: [(Id, Node)] rootNodes = [(n_id rootNode, rootNode) | rootNode <- concatMap asNodes sigs] - + buildFields fields' = foldr buildField (FamilyTree (fromList rootNodes) Map.empty) fields' buildField field tree = foldr (uncurry buildTuple) tree (zip ([0,1..]::[Integer]) $ f_tuples field) where @@ -153,7 +153,7 @@ addChild (labelAsId $ a_label from) (buildNode (labelAsId $ a_label to) toType) tree' where buildNode = if label == "ref" then ValueNode else ClaferNode - + labelAsId :: String -> Id labelAsId label = case e of @@ -174,13 +174,13 @@ where sigMap = buildSigMap solution ftree = buildFamilyTree solution - + intType = s_id $ findWithDefault (error "Missing Int sig") "Int" sigMap - + singleton [] = Nothing singleton [x] = Just x singleton xs = error $ "Received more than one value " ++ show xs - + buildClafer :: Node -> Either Clafer Value buildClafer (ClaferNode id _) = Left $ Clafer id (singleton valueChildren) claferChildren
src/Language/Clafer/IG/CommandLine.hs view
@@ -74,29 +74,29 @@ historyFile = Nothing, autoAddHistory = True } $ loop Next (Context Nothing [] [] autoCompleteContext) - where + where loop :: Command -> Context -> InputT (ClaferIGT IO) () - + loop Quit _ = return () - + loop Next context = do solution <- lift next - claferIGArgs' <- lift getClaferIGArgs + claferIGArgs' <- lift getClaferIGArgs info <- lift getInfo case solution of Instance claferModel xml -> do liftIO $ writeIORef (claferInstances $ autoCompleteContext context) $ map c_name (traverse claferModel) - - outputStrLn $ if json claferIGArgs' + + outputStrLn $ if json claferIGArgs' then generateJSON info claferModel else let iNumber = show $ 1 + (length $ unsaved context) in - "=== Instance " ++ iNumber ++ " Begin ===\n\n" ++ - (show claferModel) ++ + "=== Instance " ++ iNumber ++ " Begin ===\n\n" ++ + (show claferModel) ++ "\n--- Instance " ++ iNumber ++ " End ---\n\n" nextLoop context{unsaved=claferModel:(unsaved context), currentAlloyInstance=Just xml} UnsatCore core counterexample -> do @@ -114,8 +114,8 @@ NoInstance -> do liftIO $ hPutStrLn stderr "No more instances found. Try increasing scope to get more instances." nextLoop context - where - printTransformation :: Constraint -> [Constraint] -> (String, [Constraint]) + where + printTransformation :: Constraint -> [Constraint] -> (String, [Constraint]) printTransformation UserConstraint{constraintInfo = info} rest = ("removed " ++ syntax info, rest) printTransformation ExactCardinalityConstraint{claferInfo = info} rest = (show info ++ " changed to " ++ show (setUpper (setLower info 0) Nothing), rest) @@ -149,26 +149,26 @@ let (prnt, rest) = printTransformation c cs liftIO $ hPutStrLn stderr $ " " ++ show i ++ ") " ++ prnt printTransformations' (i + 1) rest - + setLower info@ClaferInfo{cardinality = c} lower = info{cardinality = c{lower = lower}} setUpper info@ClaferInfo{cardinality = c} upper = info{cardinality = c{upper = upper}} - deleteLower :: String -> [Constraint] -> Maybe [Constraint] + deleteLower :: String -> [Constraint] -> Maybe [Constraint] deleteLower id ys = findAndDelete id (filter isLowerCardinalityConstraint ys) - + deleteUpper :: String -> [Constraint] -> Maybe [Constraint] deleteUpper id ys = findAndDelete id (filter isUpperCardinalityConstraint ys) - + findAndDelete :: String -> [Constraint] -> Maybe [Constraint] findAndDelete _ [] = Nothing findAndDelete id (c:cs) | id == uniqueId (claferInfo c) = Just cs | otherwise = (c :) `fmap` findAndDelete id cs - - + + loop Help context = do outputStrLn ( @@ -176,13 +176,13 @@ "| " ++ claferIGVersion ++ " |\n" ++ "--------------------\n\n" ++ "You can invoke the following commands as indicated by single quotes:\n" ++ - "[tab] - print the available commands\n" ++ + "[tab] - print the available commands\n" ++ " - auto-complete command name, a clafer name, or clafer instance name in a given context\n" ++ "'n'ext, [enter] - to produce the next instance if available or to output a message that no more \n" ++ " instances exist within the given scope\n" ++ "'i'ncrease - to increase the maximum number of instances of a given clafer or all clafers (scope)\n" ++ - "'s'et - to set the maximum number of instances of a given clafer or all clafers (scope)\n" ++ - "'m'axint, 'maxint' - to set the bitwidth by providing the largest integer\n" ++ + "'s'et - to set the maximum number of instances of a given clafer or all clafers (scope)\n" ++ + "'m'axint, 'maxint' - to set the bitwidth by providing the largest integer\n" ++ "sa'v'e - to save all instances displayed so far or a counterexample to files named \n" ++ " <model file name>.cfr.<instance number>.data, one instance per file\n" ++ "'q'uit - to quit the interactive session\n" ++ @@ -190,8 +190,8 @@ "'h'elp - to display this menu options summary\n" ++ "'scope' - to print out the values of the global scope and individual Clafer scopes\n" ++ "'saveScopes' - to generate a '<model>.cfr-scope' file with the current scopes\n" ++ - "'loadScopes' - to load scopes from a '<model>.cfr-scope' file\n" ++ - "'setUnsatCoreMinimization' - to choose UnSAT core minimization strategy [fastest | medium | best]. Default: fastest\n" ++ + "'loadScopes' - to load scopes from a '<model>.cfr-scope' file\n" ++ + "'setUnsatCoreMinimization' - to choose UnSAT core minimization strategy [fastest | medium | best]. Default: fastest\n" ++ "'c', 'claferModel' - to print out the original Clafer model verbatim\n" ++ "'a', 'alloyModel' - to print out the output of Clafer translator verbatim\n" ++ "'alloyInstance' - to print out the Alloy xml document of the most recent solution\n" ++ @@ -203,13 +203,13 @@ "'s <number> [enter]'- to set for the clafers to <number>\n" ++ "'s <name> <number>' - to set for the clafer <name> to <number>\n" ++ "'f <name>' - to display a clafer <name>\n" ++ - "'setUnsatCoreMinimization fastest' - fastest but the worst\n" ++ - "'setUnsatCoreMinimization medium'\n" ++ - "'setUnsatCoreMinimization best' - best but slowest even for modest size cores" + "'setUnsatCoreMinimization fastest' - fastest but the worst\n" ++ + "'setUnsatCoreMinimization medium'\n" ++ + "'setUnsatCoreMinimization best' - best but slowest even for modest size cores" ) - + nextLoop context - + loop Save context@Context{saved=saved, unsaved=unsaved} = do save unsaved (toInteger $ length saved) @@ -221,7 +221,7 @@ oldBw <- lift getBitwidth runErrorT $ ErrorT (lift reload) `catchError` (liftIO . mapM_ (hPutStrLn stderr) . printError) - + env <- lift getClaferEnv let ir = fst3 $ fromJust $ cIr env tempScopes <- lift getScopes @@ -248,7 +248,7 @@ oldScopes <- lift getScopes mapM ( \(sigName', val') -> setAlloyScopeAndBitwidth bitwidth' (max 1 $ val'+inc') (sigToClaferName sigName') sigName') oldScopes - lift solve + lift solve outputStrLn ("Global scope changed to " ++ show newGlobalScope) nextLoop context loop (SetGlobalScope newGlobalScope') context = @@ -261,7 +261,7 @@ lift $ setBitwidth $ requiredBitwidth newGlobalScope newBw <- lift getBitwidth printBitwidthWarning newBw - lift solve + lift solve outputStrLn ("Global scope set to " ++ show newGlobalScope) nextLoop context @@ -274,7 +274,7 @@ bitwidth' <- lift $ lift getBitwidth lift $ mapM_ (incAlloyScopeAndBitwidth bitwidth' inc' fqName) sigs - + lift $ lift $ solve nextLoop context @@ -287,26 +287,26 @@ bitwidth' <- lift $ lift getBitwidth lift $ mapM_ (setAlloyScopeAndBitwidth bitwidth' val' qName) sigs - + lift $ lift $ solve nextLoop context loop (SetBitwidth newBitwidth) context = - do + do when (newBitwidth >=4) $ do lift $ setBitwidth newBitwidth printBitwidthWarning newBitwidth - lift solve + lift solve printBitwidthIntRange newBitwidth nextLoop context loop (SetMaxInt newMaxInt) context = - do + do when (newMaxInt >= 7) $ do let newBitwidth = requiredBitwidth newMaxInt lift $ setBitwidth newBitwidth printBitwidthWarning newBitwidth - lift solve + lift solve printBitwidthIntRange newBitwidth nextLoop context @@ -318,15 +318,15 @@ -- remove the "this/" prefix mapM_ printScope originalScopes nextLoop context - + where printScope (sigName, value) = outputStrLn $ " " ++ (drop 5 sigName) ++ " scope = " ++ show value - + loop SaveScopes context = do globalScope <- lift getGlobalScope - originalScopes <- lift getScopes + originalScopes <- lift getScopes claferIGArgs' <- lift getClaferIGArgs qNameMaps' <- lift getQNameMaps let @@ -336,7 +336,7 @@ liftIO $ writeCfrScopeFile uidScopes qNameMaps' $ claferModelFile claferIGArgs' outputStrLn "Scopes saved to the `.cfr-scope` file." nextLoop context - + loop LoadScopes context = do claferIGArgs' <- lift getClaferIGArgs @@ -346,8 +346,8 @@ Nothing -> do outputStrLn "The `.cfr-scope` file does not exist. Use the command `saveScopes` to create one." nextLoop context - Just uidScopes -> do - let + Just uidScopes -> do + let (globalScopes, normalScopes) = partition (\(uid', _) -> null uid') uidScopes -- from the globalScopes, take the maximum globalScopeVals = map snd globalScopes @@ -374,14 +374,14 @@ printBitwidthIntRange bitwidth' originalScopes <- lift getScopes -- remove the "this/" prefix - let + let scopes = map ( \ (uid', val') -> (drop 5 uid', val') ) originalScopes scopesMap = Map.fromList scopes globalScope' <- lift getGlobalScope outputStrLn $ "Global scope = " ++ show globalScope' ++ "\n" - env <- lift getClaferEnv + env <- lift getClaferEnv constraints' <- lift getConstraints AlloyIG.UnsatCore core <- lift $ ClaferIGT $ lift AlloyIG.sendUnsatCoreCommand let unSATs = map getConstraintInfo $ catMaybes $ findRemovable env core constraints' @@ -395,18 +395,18 @@ nextLoop context where editModel :: String -> [Integer] -> [String] -> (Map.Map Integer String) -> (Map.Map String Integer) -> String - editModel model cLines unSATs lineNumMap scopesMap' = - let + editModel model cLines unSATs lineNumMap scopesMap' = + let claferLines = lines $ removeCommentsAndUnify model maxLineLength = maximum $ map length claferLines in unlines $ editLines cLines unSATs (numberOfDigits $ length claferLines) maxLineLength scopesMap' lineNumMap (zip [1..] claferLines) editLines :: [Integer] -> [String] -> Int -> Int -> (Map.Map String Integer) -> (Map.Map Integer String) -> [(Integer, String)] -> [String] editLines _ _ _ _ _ _ [] = [] - editLines cLines unSATs m1 m2 scopesMap' lineNumMap ((num, l):rest) = - if (num `elem` cLines && isEmptyLine l) - then editLines cLines unSATs m1 m2 scopesMap' lineNumMap rest - else (show num ++ "." ++ (replicate (1 + m1 - (numberOfDigits $ fromIntegral num)) ' ') ++ (if (isUnSAT unSATs l num) then "> " else "| ") ++ l ++ (replicate (3 + m2 - (length l)) ' ') ++ (if (isUnSAT unSATs l num) then "<UnSAT " else "| ") ++ (addScopeVal scopesMap' (Map.lookup num lineNumMap))) + editLines cLines unSATs m1 m2 scopesMap' lineNumMap ((num, l):rest) = + if (num `elem` cLines && isEmptyLine l) + then editLines cLines unSATs m1 m2 scopesMap' lineNumMap rest + else (show num ++ "." ++ (replicate (1 + m1 - (numberOfDigits $ fromIntegral num)) ' ') ++ (if (isUnSAT unSATs l num) then "> " else "| ") ++ l ++ (replicate (3 + m2 - (length l)) ' ') ++ (if (isUnSAT unSATs l num) then "<UnSAT " else "| ") ++ (addScopeVal scopesMap' (Map.lookup num lineNumMap))) : editLines cLines unSATs m1 m2 scopesMap' lineNumMap rest isUnSAT :: [String] -> String -> Integer -> Bool @@ -416,7 +416,7 @@ addScopeVal :: (Map.Map String Integer) -> (Maybe String) ->String addScopeVal _ Nothing = "" - addScopeVal scopesMap' (Just name) = "scope = " ++ (fromJustShow $ Map.lookup name scopesMap') + addScopeVal scopesMap' (Just name) = "scope = " ++ (fromJustShow $ Map.lookup name scopesMap') getCommentLines :: String -> [Integer] getCommentLines = foldr (\((Span (Pos l1 _) (Pos l2 _)), _) acc -> [l1..l2] ++ acc) [] . getComments @@ -432,37 +432,37 @@ scopes <- lift getScopes outputStrLn $ editAlloyModel alloyModel scopes globalScope' - nextLoop context + nextLoop context where editAlloyModel :: String -> [(String, Integer)] -> Integer -> String - editAlloyModel model s globalScope' = + editAlloyModel model s globalScope' = let alloyLines = lines $ removeCommentsAndUnify model splitNum = 1 + (length $ takeWhile (not . isEmptyLine) alloyLines) (alloyInfo, alloyLines') = splitAt splitNum $ alloyLines in unlines $ (("global scope = " ++ show globalScope' ++ "\n") :) $ alloyInfo ++ map (\(num, line) -> show num ++ ('.' : (replicate (1 + (numberOfDigits $ length alloyLines) - (numberOfDigits num)) ' ') ++ ('|' : ' ' : line))) (zip [(1 + splitNum)..] (addScopeVals alloyLines' s (maximum $ map length alloyLines'))) addScopeVals :: [String] -> [(String, Integer)] -> Int -> [String] addScopeVals [] _ _ = [] - addScopeVals (l:ls) ss m = - let val = Data.List.lookup (takeWhile (`notElem` [' ','\t','\n']) $ tail $ dropWhile (/='_') l) ss + addScopeVals (l:ls) ss m = + let val = Data.List.lookup (takeWhile (`notElem` [' ','\t','\n']) $ tail $ dropWhile (/='_') l) ss in if ("sig" `notElem` words l) then ((l ++ (replicate (3 + m - (length l)) ' ') ++ " |") : addScopeVals ls ss m) - else (l ++ (replicate (3 + m - (length l)) ' ') ++ " | scope = " ++ (fromJustShow val)) : addScopeVals ls ss m - + else (l ++ (replicate (3 + m - (length l)) ' ') ++ " | scope = " ++ (fromJustShow val)) : addScopeVals ls ss m + loop ShowAlloyInstance context = do case currentAlloyInstance context of Just alloyInstance -> outputStrLn alloyInstance Nothing -> outputStrLn $ "No instance" nextLoop context - + loop (SetUnsatCoreMinimization level) context = do - let level' = + let level' = case level of Fastest -> 2 Medium -> 1 Best -> 0 lift $ setUnsatCoreMinimization level' >> solve - + nextLoop context nextLoop context = @@ -474,12 +474,12 @@ case parseCommandLine input of Left msg -> outputStrLn (show msg) >> nextLoop context Right command -> loop command context - + save :: MonadIO m => [ClaferModel] -> Integer -> InputT (ClaferIGT m) () save [] _ = return () save (c:cs) counter = do claferIGArgs' <- lift $ getClaferIGArgs - let + let claferModelFile' = claferModelFile claferIGArgs' saveName = claferModelFile' ++ "." ++ (show counter) ++ ".data" liftIO $ writeFile saveName (show c) @@ -491,7 +491,7 @@ incAlloyScopeAndBitwidth :: MonadIO m => Integer -> Integer -> String -> UID -> InputT (ClaferIGT m) () incAlloyScopeAndBitwidth bitwidth' inc' fqName' sigName' = do - scopeValue <- lift $ valueOfScope sigName' + scopeValue <- lift $ valueOfScope sigName' setAlloyScopeAndBitwidth bitwidth' (max 1 $ scopeValue+inc') fqName' sigName' setAlloyScopeAndBitwidth :: MonadIO m => Integer -> Integer -> String -> UID -> InputT (ClaferIGT m) () @@ -502,7 +502,7 @@ outputStrLn $ "Warning! Requested scope for " ++ fqName' ++ " is larger than maximum allowed by bitwidth ... increasing bitwidth" printBitwidthWarning newBw lift $ setAlloyScope newValue' sigName' - outputStrLn $ "Scope of " ++ fqName' ++ " (" ++ (drop 5 sigName') ++ ") changed to " ++ show newValue' + outputStrLn $ "Scope of " ++ fqName' ++ " (" ++ (drop 5 sigName') ++ ") changed to " ++ show newValue' mergeScopes :: MonadIO m => [(UID, Integer)] -> [(UID, Integer)] -> ClaferIGT m () mergeScopes _ [] = return() @@ -512,7 +512,7 @@ pickLargerScope :: [(String, Integer)] -> (String, Integer) -> (String, Integer) pickLargerScope oldScopes (uid', val) = - let + let oldScopesMap = SMap.fromList oldScopes oldVal = SMap.findWithDefault val uid' oldScopesMap in (uid', max val oldVal) @@ -536,7 +536,7 @@ "..", show $ allowedMaxInt bw, " (", - "bitwidth = ", + "bitwidth = ", show bw, ")" ] @@ -553,7 +553,7 @@ completeFunc :: MonadIO m => AutoCompleteContext -> CompletionFunc m -completeFunc context (prev, nxt) = +completeFunc context (prev, nxt) = if isOpen prev nxt then liftIO $ evalComplete context prev else @@ -565,7 +565,7 @@ evalComplete :: AutoCompleteContext -> String -> IO (String, [Completion]) -evalComplete context prev = +evalComplete context prev = do completion <- autoComplete context word auto return (reverseRest, completion) @@ -574,8 +574,8 @@ (reverseWord, reverseRest) = break isSpace prev word = reverse reverseWord auto = autoCompleteDetect $ parseCommandLineAutoComplete input - + autoComplete :: AutoCompleteContext -> String -> AutoComplete -> IO [Completion] autoComplete _ word Auto_Command = return $ completePrefix word commandStrings autoComplete context word Auto_Clafer = @@ -606,9 +606,9 @@ messages = errorMessages error' unexpectedMessages = mapMaybe unexpectedMessage messages expectedMessages = mapMaybe expectedMessage messages - -printError :: ClaferErrs -> [String] + +printError :: ClaferErrs -> [String] printError (ClaferErrs errs) = map printErr errs where @@ -644,20 +644,20 @@ numberOfDigits x = length $ show x findNecessaryBitwidth :: IModule -> Integer -> [ Integer ] -> Integer -findNecessaryBitwidth ir oldBw scopeValues = +findNecessaryBitwidth ir oldBw scopeValues = if (newBw < oldBw) then oldBw else newBw where newBw = ceiling $ logBase 2 $ (+1) $ (*2) $ maxInModel ir maxInModel :: IModule -> Float maxInModel ir' = intToFloat $ max (maximum scopeValues) $ foldIR getMax 0 ir' - getMax :: Ir -> Integer -> Integer + getMax :: Ir -> Integer -> Integer getMax (IRIExp (IInt n)) m = max m $ abs n getMax (IRClafer IClafer{_card = Just (_, n)}) m = max m n getMax _ m = m intToFloat :: Integer -> Float -intToFloat = fromInteger . toInteger +intToFloat = fromInteger . toInteger fromJustShow :: (Maybe Integer) -> String fromJustShow (Just x) = show x -fromJustShow Nothing = "Nothing"+fromJustShow Nothing = "Nothing"
src/Language/Clafer/IG/CommandLineParser.hs view
@@ -31,24 +31,24 @@ -- | Interactive session commands -data Command = Next | - IncreaseGlobalScope Integer | - IncreaseScope String Integer | - SetGlobalScope Integer | - SetScope String Integer | +data Command = Next | + IncreaseGlobalScope Integer | + IncreaseScope String Integer | + SetGlobalScope Integer | + SetScope String Integer | SetBitwidth Integer | - SetMaxInt Integer | - Save | - Quit | - Reload | - Help | - Find String | - ShowScopes | + SetMaxInt Integer | + Save | + Quit | + Reload | + Help | + Find String | + ShowScopes | SaveScopes | LoadScopes | - ShowClaferModel | - ShowAlloyModel | - ShowAlloyInstance | + ShowClaferModel | + ShowAlloyModel | + ShowAlloyInstance | SetUnsatCoreMinimization UnsatCoreMinimization deriving Show @@ -96,7 +96,7 @@ commandLine :: Parser Command -commandLine = +commandLine = do name <- command case lookup name commandMap of @@ -108,8 +108,8 @@ didYouMean = filter (name `isPrefixOf`) commandStrings hint [] = "" hint _ = ", did you mean " ++ intercalate " or " (map quote didYouMean) ++ "?" - + command :: Parser String command = many1 (letter <?> "command") @@ -193,7 +193,7 @@ setGlobalScope :: Parser Command setGlobalScope = do - try (gap >> explicitSetGlobalScope) + try (gap >> explicitSetGlobalScope) <|> do try (gap >> explicitSetScope) @@ -206,16 +206,16 @@ explicitSetGlobalScope :: Parser Command explicitSetGlobalScope = fmap SetGlobalScope number - + increaseScope :: Parser Command -increaseScope = +increaseScope = do name <- clafer do try (gap >> explicitIncreaseScope name) <|> return (IncreaseScope name 1) - + explicitIncreaseScope :: String -> Parser Command explicitIncreaseScope name = fmap (IncreaseScope name) signedNumber @@ -242,7 +242,7 @@ return $ SetMaxInt b number :: Parser Integer -number = do +number = do n <- many1 digit return $ read n @@ -252,7 +252,7 @@ n <- many1 digit return $ read $ s ++ n -clafer :: Parser String +clafer :: Parser String clafer = many1 ((alphaNum <|> char ':' <|> char '_') <?> "clafer")
src/Language/Clafer/IG/Constraints.hs view
@@ -97,13 +97,13 @@ convert s IrPExp{pUid} = Just $ UserConstraint s $ ConstraintInfo pUid (_inPos $ findPExp pUid) $ extract $ _inPos $ findPExp pUid convert s LowerCard{pUid, isGroup = False} = - Just $ LowerCardinalityConstraint s $ claferInfo pUid + Just $ LowerCardinalityConstraint s $ claferInfo pUid convert s UpperCard{pUid, isGroup = False} = Just $ UpperCardinalityConstraint s $ claferInfo pUid convert s ExactCard{pUid, isGroup = False} = Just $ ExactCardinalityConstraint s $ claferInfo pUid convert _ _ = Nothing - + findPExp pUid = fromMaybe (error $ "Unknown constraint " ++ pUid) $ find ((== pUid) . _pid) pexps findClafer pUid = fromMaybe (error $ "Unknown clafer " ++ pUid) $ find ((== pUid) . _uid) clafers text = lines claferModel
src/Language/Clafer/IG/JSONGenerator.hs view
@@ -24,65 +24,62 @@ import qualified Language.Clafer.IG.ClaferModel as M import qualified Language.Clafer.Intermediate.Analysis as A +import Data.Maybe (fromMaybe) import Data.Json.Builder import Data.String.Conversions import Prelude hiding (id) -- | Generate a representation of the instance in JSON format generateJSON :: A.Info -> M.ClaferModel -> String -generateJSON info (M.ClaferModel topLevelClafers) = - convertString $ toJsonBS $ constructElements $ map (printClafer info) topLevelClafers +generateJSON info (M.ClaferModel topLevelClafers) = + convertString $ toJsonBS $ constructElements $ map (printClafer info) topLevelClafers printClafer :: A.Info -> M.Clafer -> Object -printClafer info (M.Clafer id value children) = - (map (printClafer info) children) `addElements` completeClaferObject - where - uid = M.i_name id - sclafer = A.runAnalysis (A.claferWithUid $ removeOrdinal uid) info - ident = A.uid sclafer +printClafer info (M.Clafer id value children) = + (map (printClafer info) children) `addElements` completeClaferObject + where + uid = M.i_name id + sclafer = A.runAnalysis (A.claferWithUid $ removeOrdinal uid) info + ident = A.uid sclafer - getSuper :: Maybe A.SSuper -> (Bool, String) - getSuper Nothing = (False, "") - getSuper (Just (A.Ref s)) = (True, s) - getSuper (Just (A.Colon s)) = (False, s) + super = fromMaybe "" $ A.super sclafer + reference = fromMaybe "" $ A.reference sclafer + cardMin = A.low sclafer + cardMax = A.high sclafer + basicClaferObject = makeBasicClaferObject ident uid super reference cardMin cardMax - (isOverlapping, super) = getSuper $ A.super sclafer - cardMin = A.low sclafer - cardMax = A.high sclafer - basicClaferObject = makeBasicClaferObject ident uid super isOverlapping cardMin cardMax + addValue :: Maybe M.Value -> Object -> Object + addValue Nothing object = object + addValue (Just (M.IntValue i)) object = addIntValue i object + addValue (Just (M.AliasValue a)) object = addStringValue (M.i_name a) object + addValue (Just (M.StringValue _)) _ = error "Function addValue from JSONGenerator does not accept StringValues" -- Should never happen, string values are not generated yet - addValue :: Maybe M.Value -> Object -> Object - addValue Nothing object = object - addValue (Just (M.IntValue i)) object = addIntValue i object - addValue (Just (M.AliasValue a)) object = addStringValue (M.i_name a) object - addValue (Just (M.StringValue _)) _ = error "Function addValue from JSONGenerator does not accept StringValues" -- Should never happen, string values are not generated yet - - completeClaferObject = addValue value basicClaferObject + completeClaferObject = addValue value basicClaferObject - removeOrdinal :: String -> String - removeOrdinal = takeWhile (/= '$') + removeOrdinal :: String -> String + removeOrdinal = takeWhile (/= '$') -makeBasicClaferObject :: String -> String -> String -> Bool -> Integer -> Integer -> Object -makeBasicClaferObject ident uid super isOverlapping cardMin cardMax = - mconcat [ row "ident" ident, - row "uid" uid, - row "super" super, - row "isOverlapping" isOverlapping, - row "cardMin" cardMin, - row "cardMax" cardMax ] +makeBasicClaferObject :: String -> String -> String -> String -> Integer -> Integer -> Object +makeBasicClaferObject ident uid super reference cardMin cardMax = + mconcat [ row "ident" ident, + row "uid" uid, + row "super" super, + row "reference" reference, + row "cardMin" cardMin, + row "cardMax" cardMax ] addIntValue :: Int -> Object -> Object -addIntValue value claferObject = - claferObject `mappend` (row "value" value) +addIntValue value claferObject = + claferObject `mappend` (row "value" value) addStringValue :: String -> Object -> Object -addStringValue value claferObject = - claferObject `mappend` (row "value" value) +addStringValue value claferObject = + claferObject `mappend` (row "value" value) addElements :: [ Object ] -> Object -> Object -addElements elements claferObject = - claferObject `mappend` (constructElements elements) +addElements elements claferObject = + claferObject `mappend` (constructElements elements) constructElements :: [ Object ] -> Object constructElements elements = - row "elements" $ mconcat $ map element elements+ row "elements" $ mconcat $ map element elements
src/Language/Clafer/IG/Process.hs view
@@ -45,8 +45,8 @@ (Just stdIn', Just stdOut', _, proceHandle) <- createProcess process hSetNewlineMode stdIn' noNewlineTranslation return $ Process stdIn' stdOut' proceHandle -- Pipe always has a handle according to docs - - + + -- | Wait until the process terminates waitFor :: Process -> IO ExitCode waitFor proce = waitForProcess (procHandle proce) @@ -61,7 +61,7 @@ mapM_ return contents return contents - + -- | Read the message getMessage :: MonadIO m => Process -> m String getMessage proce = @@ -69,7 +69,7 @@ len <- read `liftM` hGetLine (stdOut proce) mapM hGetChar $ replicate len (stdOut proce) -readMessage :: (Read r, MonadIO m) => Process -> m r +readMessage :: (Read r, MonadIO m) => Process -> m r readMessage proce = read `liftM` getMessage proce -- | Put the message @@ -79,4 +79,4 @@ hPutStrLn (stdIn proce) (show $ length message) hPutStr (stdIn proce) message hFlush (stdIn proce) - +
src/Language/Clafer/IG/Solution.hs view
@@ -48,7 +48,7 @@ rootElem = CElem root noPos sigElems = tag "alloy" /> tag "instance" /> tag "sig" fieldElems = tag "alloy" /> tag "instance" /> tag "field" - + sigs = map parseSig $ sigElems rootElem fields = map parseField $ fieldElems rootElem in @@ -63,8 +63,8 @@ label = findAttr "label" content' id = read $ findAttr "ID" content' atoms = map parseAtom $ (keep /> tag "atom") content' - + parseAtom :: Content i -> Atom parseAtom = Atom . findAttr "label" @@ -77,9 +77,9 @@ (read $ findAttr "parentID" content') (map parseTuple $ (keep /> tag "tuple") content') where - + parseType :: Content i -> (Int, Int) - parseType content'' = + parseType content'' = (toFromType !! 0, toFromType !! 1) where toFromType = map (read . findAttr "ID") $ (keep /> tag "types" /> tag "type") content'' @@ -101,4 +101,4 @@ getAttrs :: Content i -> [Attribute] getAttrs (CElem (Elem _ attributes _) _) = attributes -getAttrs _ = error "Function getAttrs from Solution was given an invliad argument expected of type (CElem (Elem _ attributes _) _)" -- This should never happen+getAttrs _ = error "Function getAttrs from Solution was given an invliad argument expected of type (CElem (Elem _ attributes _) _)" -- This should never happen
src/Language/Clafer/IG/Sugarer.hs view
@@ -32,8 +32,8 @@ -- | Sample: maps the id to the its simple name and the number of times its simple name appeared in the census before it -- | Count: maps the simple name to the total count of the simple name -data Census = Census - (Map Id (Int, String)) -- Sample +data Census = Census + (Map Id (Int, String)) -- Sample (Map String Int) -- Counts deriving Show @@ -60,7 +60,7 @@ clafersCensus (Census Map.empty Map.empty) topLevelClafers where clafersCensus = foldl claferCensus - claferCensus census Clafer{c_id=id, c_children=children} = poll id (clafersCensus census children) + claferCensus census Clafer{c_id=id, c_children=children} = poll id (clafersCensus census children) -- | Rewrite the model into a human-friendlier format @@ -68,35 +68,33 @@ sugarClaferModel useUids addTypes info model@(ClaferModel topLevelClafers) sMap = ClaferModel $ map sugarClafer topLevelClafers where - sugarClafer (Clafer id value children) = + sugarClafer (Clafer id value children) = Clafer (sugarId useUids addTypes True id) (sugarValue (Clafer id value children)) (map sugarClafer children) sugarValue (Clafer _ (Just (AliasValue alias)) _) = Just $ AliasValue $ sugarId useUids addTypes False alias sugarValue (Clafer _ Nothing _) = Nothing sugarValue c = if (cType c) == "string" then (Just ((StringValue) (getString c))) else (c_value c) - cType (Clafer id _ _) = - case (fromJust (Analysis.super (Analysis.runAnalysis (Analysis.claferWithUid (i_name id)) (fromJust info)))) of - (Analysis.Ref s) -> cTypeSolve s - (Analysis.Colon s) -> cTypeSolve s - - cTypeSolve "string" = "string" - cTypeSolve "integer" = "integer" - cTypeSolve "int" = "integer" - cTypeSolve "real" = "real" - cTypeSolve x = cType (Clafer (Id x 0) Nothing []) + cType (Clafer id _ _) = cTypeSolve $ (Analysis.super (Analysis.runAnalysis (Analysis.claferWithUid (i_name id)) (fromJust info))) + cTypeSolve Nothing = "" + cTypeSolve (Just "string") = "string" + cTypeSolve (Just "integer") = "integer" + cTypeSolve (Just "int") = "integer" + cTypeSolve (Just "real") = "real" + cTypeSolve (Just x) = cType (Clafer (Id x 0) Nothing []) + getString c = case (Map.lookup strNumber sMap) of Nothing -> "\"<text " ++ show strNumber ++ ">\"" Just s -> s where strNumber = v_value $ fromJust $ c_value c - + Census sample' counts' = claferModelCensus model - + sugarId :: Bool -> Bool -> Bool -> Id -> Id sugarId useUids' addTypes' addRefDecl id = - Id (finalName ++ ordinalDisplay ++ (refDecl addTypes' addRefDecl info)) 0 + Id (finalName ++ ordinalDisplay ++ (refDecl addTypes' addRefDecl info)) 0 where fullName = i_name id ordinalDisplay = if (useUids || count > 1) @@ -106,19 +104,23 @@ refDecl :: Bool -> Bool -> Maybe Analysis.Info -> String refDecl True True (Just info') = retrieveSuper info' $ i_name id refDecl _ _ _ = "" - + (ordinal, simpleName) = findWithDefault (error $ "Sample lookup " ++ show id ++ " failed.") id sample' count = findWithDefault (error $ "Count lookup " ++ simpleName ++ " failed.") simpleName counts' finalName = if useUids' then fullName else simpleName retrieveSuper :: Analysis.Info -> String -> String -retrieveSuper info uid = - if (Analysis.isBase sclafer) - then "" - else maybe "" sugarSuper (Analysis.super sclafer) +retrieveSuper info uid = + (if (Analysis.isBase sclafer) + then "" + else sugarSuper (Analysis.super sclafer)) + ++ sugarReference (Analysis.reference sclafer) where sclafer = Analysis.runAnalysis (Analysis.claferWithUid uid) info - sugarSuper :: Analysis.SSuper -> String - sugarSuper (Analysis.Ref s) = " -> " ++ s - sugarSuper (Analysis.Colon s) = " : " ++ s + sugarSuper :: Maybe String -> String + sugarSuper (Just s) = " : " ++ s + sugarSuper Nothing = "" + sugarReference :: Maybe String -> String + sugarReference (Just s) = " -> " ++ s + sugarReference Nothing = ""
test/test-suite.hs view
@@ -66,26 +66,26 @@ --getModel :: MonadIO m => FilePath -> ClaferIGT m (Either Language.ClaferT.ClaferErrs Instance) getModel fPath = runClaferIGT (defaultIGArgs fPath) $ do - setGlobalScope (fromMaybe 1 $ all $ defaultIGArgs fPath) - solve - counterRef <- liftIO $ newIORef 1 - let saveDirectory = fromMaybe return $ underDirectory `liftM` saveDir (defaultIGArgs fPath) - let nextFile = savePath fPath counterRef >>= saveDirectory - file <- liftIO nextFile - liftIO $ createDirectoryIfMissing True $ takeDirectory file - next - where - savePath :: FilePath -> IORef Int -> IO FilePath - savePath fPath' counterRef = - do - counter <- readIORef counterRef - writeIORef counterRef (counter + 1) - return $ fPath' ++ "." ++ (show counter) ++ ".data" - underDirectory :: FilePath -> FilePath -> IO FilePath - underDirectory dir file = - do - createDirectoryIfMissing True dir - return $ joinPath [dir, file] + setGlobalScope (fromMaybe 1 $ all $ defaultIGArgs fPath) + solve + counterRef <- liftIO $ newIORef 1 + let saveDirectory = fromMaybe return $ underDirectory `liftM` saveDir (defaultIGArgs fPath) + let nextFile = savePath fPath counterRef >>= saveDirectory + file <- liftIO nextFile + liftIO $ createDirectoryIfMissing True $ takeDirectory file + next + where + savePath :: FilePath -> IORef Int -> IO FilePath + savePath fPath' counterRef = + do + counter <- readIORef counterRef + writeIORef counterRef (counter + 1) + return $ fPath' ++ "." ++ (show counter) ++ ".data" + underDirectory :: FilePath -> FilePath -> IO FilePath + underDirectory dir file = + do + createDirectoryIfMissing True dir + return $ joinPath [dir, file] fromRight (Right x) = x @@ -94,22 +94,22 @@ case_strMapCheck :: Assertion case_strMapCheck = do - --let claferModel = Right $ Instance (ClaferModel [(Clafer (Id "" 0) (Just (StringValue "")) [])]) "" - claferModel' <- getModel "test/positive/i220.cfr" - (valueCheck $ c_value $ head $ c_topLevel $ modelInstance $ fromRight $ claferModel') @? "Mapping Int back to String Failed!" - where - valueCheck Nothing = False - valueCheck (Just (AliasValue _)) = False - valueCheck (Just (IntValue _)) = False - valueCheck (Just (StringValue _)) = True - + --let claferModel = Right $ Instance (ClaferModel [(Clafer (Id "" 0) (Just (StringValue "")) [])]) "" + claferModel' <- getModel "test/positive/i220.cfr" + (valueCheck $ c_value $ head $ c_topLevel $ modelInstance $ fromRight $ claferModel') @? "Mapping Int back to String Failed!" + where + valueCheck Nothing = False + valueCheck (Just (AliasValue _)) = False + valueCheck (Just (IntValue _)) = False + valueCheck (Just (StringValue _)) = True + case_pickLargerScope :: Assertion case_pickLargerScope = do let oldScopes = [ ("c0_1", 1), ("c1_b", 2), ("c0_x", 5) ] newScopes = [ ("c0_1", 2), ("c0_b", 2), ("c1_b", 1)] mergedScopes = map (pickLargerScope oldScopes) newScopes - + mergedScopes @?= [ ("c0_1", 2), ("c0_b", 2), ("c1_b", 2)]