diff --git a/CHANGES.md b/CHANGES.md --- a/CHANGES.md +++ b/CHANGES.md @@ -1,58 +1,62 @@ -Clafer Version 0.4.2.1 released on Oct 19, 2015 +##### Clafer Version 0.4.3 released on Dec 22, 2015 +* [Release](https://github.com/gsdlab/clafer/pull/81) + +##### Clafer Version 0.4.2.1 released on Oct 19, 2015 + * Fixed Haddock build, updated README, fixed a test case. -Clafer Version 0.4.2 released on Oct 16, 2015 +##### Clafer Version 0.4.2 released on Oct 16, 2015 * [Release](https://github.com/gsdlab/clafer/pull/74) -Clafer Version 0.4.1 released on Sep 1, 2015 +##### Clafer Version 0.4.1 released on Sep 1, 2015 * [Release](https://github.com/gsdlab/clafer/pull/71) -Clafer Version 0.4.0 released on Jul 28, 2015 +##### Clafer Version 0.4.0 released on Jul 28, 2015 * [Release](https://github.com/gsdlab/clafer/pull/68) -Clafer Version 0.3.10 released on April 24, 2015 +##### Clafer Version 0.3.10 released on April 24, 2015 * [Release](https://github.com/gsdlab/clafer/pull/66) -Clafer Version 0.3.9 released on March 06, 2015 +##### Clafer Version 0.3.9 released on March 06, 2015 * [Release](https://github.com/gsdlab/clafer/pull/63) -Clafer Version 0.3.8 released on January 27, 2015 +##### Clafer Version 0.3.8 released on January 27, 2015 * [Release](https://github.com/gsdlab/clafer/pull/60) -Clafer Version 0.3.7 released on October 23, 2014 +##### Clafer Version 0.3.7 released on October 23, 2014 * [Release](https://github.com/gsdlab/clafer/pull/53) -Clafer Version 0.3.6.1 released on July 08, 2014 +##### Clafer Version 0.3.6.1 released on July 08, 2014 * [Release](https://github.com/gsdlab/clafer/pull/50) -Clafer Version 0.3.6 released on May 23, 2014 +##### Clafer Version 0.3.6 released on May 23, 2014 * [Release](https://github.com/gsdlab/clafer/pull/48) -Clafer Version 0.3.5 released on January 20, 2014 +##### Clafer Version 0.3.5 released on January 20, 2014 * [Release](https://github.com/gsdlab/clafer/pull/44) -Clafer Version 0.3.4 released on September 20, 2013 +##### Clafer Version 0.3.4 released on September 20, 2013 -Clafer Version 0.3.3 released on August 14, 2013 +##### Clafer Version 0.3.3 released on August 14, 2013 * [Release](https://github.com/gsdlab/clafer/pull/35) -Clafer Version 0.3.2 released on April 11, 2013 +##### Clafer Version 0.3.2 released on April 11, 2013 -Clafer Version 0.3.1 released on October 17, 2012 +##### Clafer Version 0.3.1 released on October 17, 2012 -Clafer Version 0.3 released on July 17, 2012 +##### Clafer Version 0.3 released on July 17, 2012 This was the first release of Clafer and included all code since the beginning of the project. diff --git a/Makefile b/Makefile --- a/Makefile +++ b/Makefile @@ -27,15 +27,14 @@ prof: alloy4.2.jar stack build --executable-profiling --library-profiling --ghc-options="-prof -fprof-auto -auto-all -caf-all -rtsopts -osuf p_o" -.PHONY : test - +.PHONY: test test: cp `stack path --local-install-root`/bin/clafer$(EXE) . - cabal test 2>/dev/null || : # supress error message and exit code if fail + stack test 2>/dev/null || : # supress error message and exit code if fail $(MAKE) -C $(TEST_DIR) test -generateAlloyJSPythonHTMLDot: - $(MAKE) -C $(TEST_DIR) generateAlloyJSPythonHTMLDot +generateAlloyJSHTMLDot: + $(MAKE) -C $(TEST_DIR) generateAlloyJSHTMLDot diffRegressions: $(MAKE) -C $(TEST_DIR) diffRegressions @@ -43,21 +42,26 @@ reg: $(MAKE) -C $(TEST_DIR) reg +.PHONY: clean clean: stack clean $(MAKE) -C $(SRC_DIR) clean $(MAKE) cleanTools $(MAKE) cleanTest +.PHONY: cleanTest cleanTest: $(MAKE) -C $(TEST_DIR) clean +.PHONY: cleanTools cleanTools: find . -type f -name '*.class' -print0 | xargs -0 rm -f +.PHONY: tags tags: hasktags --ctags --extendedctag --ignore-close-implementation . +.PHONY: codex codex: codex update mv codex.tags tags diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,9 +1,9 @@ [![Hackage](https://img.shields.io/hackage/v/clafer.svg)](https://hackage.haskell.org/package/clafer) [![Build Status](https://secure.travis-ci.org/gsdlab/clafer.svg)](http://travis-ci.org/gsdlab/clafer) -# Clafer, the Language +# Clafer, the language -v0.4.2.1 +##### v0.4.3 [Clafer](http://clafer.org) is a general-purpose lightweight structural modeling language developed by @@ -30,7 +30,7 @@ * [Syntax Documentation](doc/clafer.pdf) * [Grammar](src/clafer.cf) -# Clafer, the Compiler +# Clafer, the compiler Clafer compiler provides a reference implementation of Clafer, the language. It translates models in Clafer to other formats (e.g., Alloy, JSON, JS, HTML, DOT) to allow for reasoning and processing with existing tools (Alloy Analyzer, Choco3, and GraphViz). @@ -39,7 +39,7 @@ * Backends * Alloy-based Instance Generator ([ClaferIG](https://github.com/gsdlab/claferIG)), - * Choco3-based Instance Generator and Multi-Objective Optimizer ([chocosolver](https://github.com/gsdlab/chocosolver), [ClaferChocoIG](https://github.com/gsdlab/ClaferChocoIG)). + * Choco3-based Instance Generator and Multi-Objective Optimizer ([chocosolver](https://github.com/gsdlab/chocosolver). * Web Frontends * Clafer Integrated Development Environment ([ClaferIDE](https://github.com/gsdlab/claferIDE)), * Clafer Configurator ([ClaferConfigurator](https://github.com/gsdlab/ClaferConfigurator)), @@ -51,12 +51,11 @@ * [Michał Antkiewicz](http://gsd.uwaterloo.ca/mantkiew), Main developer. * [Kacper Bak](http://gsd.uwaterloo.ca/kbak), Original developer. * [Jimmy Liang](http://gsd.uwaterloo.ca/jliang), Developer. -* [Ed Zulkoski](http://gsd.uwaterloo.ca/ezulkosk), Python IR Generator. * Luke Michael Brown, co-op student May-Aug 2013. Many improvements. * Paulius Juodisius, [customized BNFC generator](https://github.com/juodaspaulius/bnfc) and layout resolver. * [Rafael Olaechea](http://gsd.uwaterloo.ca/rolaechea), Multi-Objective Optimization extensions. -## Getting the Clafer Compiler +## Getting the Clafer compiler Clafer can be installed from a binary distribution (preferred), from Hackage, and from the source code. @@ -66,7 +65,7 @@ Optional: -* [Java Platform (JDK)](http://www.oracle.com/technetwork/java/javase/downloads/index.html) v8+, 32bit on Windows, 64bit otherwise +* [Java Platform (JDK)](http://www.oracle.com/technetwork/java/javase/downloads/index.html) v8+, 64bit * only needed for running Alloy validation * [Alloy4.2](http://alloy.mit.edu/alloy/download.html) * only needed for Alloy output validation @@ -75,7 +74,7 @@ ### Installation from binaries -Binary distributions of the release 0.4.2.1 of Clafer Tools for Windows, Mac, and Linux, +Binary distributions of the release 0.4.3 of Clafer Tools for Windows, Mac, and Linux, can be downloaded from [Clafer Tools - Binary Distributions](http://gsd.uwaterloo.ca/clafer-tools-binary-distributions). @@ -84,7 +83,7 @@ ### Installation from Hackage -Clafer is now available on [Hackage](http://hackage.haskell.org/package/clafer-0.4.2.1/) and it can be installed using either [`stack`](https://github.com/commercialhaskell/stack) or [`cabal-install`](https://hackage.haskell.org/package/cabal-install). +Clafer is now available on [Hackage](http://hackage.haskell.org/package/clafer-0.4.3/) and it can be installed using either [`stack`](https://github.com/commercialhaskell/stack) or [`cabal-install`](https://hackage.haskell.org/package/cabal-install). #### Installation using `stack` @@ -106,8 +105,8 @@ 2. `cabal update` 3. `cabal install alex happy` 4. `cabal install clafer` -5. on Windows `cd C:\Users\\AppData\Roaming\cabal\i386-windows-ghc-7.10.2\clafer-0.4.2.1` -6. on Linux `ca ~/.cabal/share/x86_64-linux-ghc-7.10.2/clafer-0.4.2.1/` +5. on Windows `cd C:\Users\\AppData\Roaming\cabal\i386-windows-ghc-7.10.2\clafer-0.4.3` +6. on Linux `ca ~/.cabal/share/x86_64-linux-ghc-7.10.2/clafer-0.4.3/` 7. to automatically download Alloy jars, execute * `make alloy4.2.jar`, * move `alloy4.2.jar` to the location of the clafer executable. @@ -122,12 +121,14 @@ On Windows * [MSYS2](http://msys2.sourceforge.net/) - * it is installed automatically by `stack` - * after building clafer, execute - * `pacman -Syu` + * it is installed automatically by `stack setup` + * to open MinGW64 shell, execute `mingw64_shell.bat` in `C:\Users\\AppData\Local\Programs\stack\x86_64-windows\msys2-`, where `` is the release date of your MSYS installation + * update MSYS2 packages + * follow guide for [III. Updating packages](http://sourceforge.net/p/msys2/wiki/MSYS2%20installation/) + * execute * `pacman -S make wget unzip diffutils` -#### Important: Branches must correspond +#### Important: branches must correspond All related projects are following the *simultaneous release model*. The branch `master` contains releases, whereas the branch `develop` contains code under development. @@ -157,7 +158,7 @@ * `make install to=` #### Note: -> On Windows, use `/` with the `make` command instead of `\`. +> On Windows, use `/` with the `make` command instead of `\`, e.g., `make install to=/c/clafer-tools-0.4.3/` ## Integration with Sublime Text 2/3 @@ -174,7 +175,7 @@ (As printed by `clafer --help`) ``` -Clafer 0.4.2.1 +Clafer 0.4.3 clafer [OPTIONS] [FILE] @@ -189,8 +190,7 @@ representation written in DOT language); 'cvlgraph' (cvl notation representation written in DOT - language); 'python' (generates IR in - python); 'choco' (Choco constraint + language); 'choco' (Choco constraint programming solver). Multiple modes can be specified at the same time, e.g., '-m alloy -m html'. @@ -209,7 +209,7 @@ -s --no-stats Don't print statistics. -v --validate Validate outputs of all modes. Uses '/alloy4.2.jar' for Alloy - models, '/claferchocoig.jar' + models, '/chocosolver.jar' for Alloy models, and Clafer translator for desugared Clafer models. Use '--tooldir' to override diff --git a/clafer.cabal b/clafer.cabal --- a/clafer.cabal +++ b/clafer.cabal @@ -1,5 +1,5 @@ Name: clafer -Version: 0.4.2.1 +Version: 0.4.3 Synopsis: Compiles Clafer models to other formats: Alloy, JavaScript, JSON, HTML, Dot. Description: Clafer is a general purpose, lightweight, structural modeling language developed at GSD Lab, University of Waterloo, and MODELS group at IT University of Copenhagen. Lightweight modeling aims at improving the understanding of the problem domain in the early stages of software development and determining the requirements with fewer defects. Clafer's goal is to make modeling more accessible to a wider range of users and domains. The tool provides a reference language implementation. It translates models to other formats (e.g. Alloy, JavaScript, JSON) to allow for reasoning with existing tools. Homepage: http://clafer.org @@ -14,6 +14,7 @@ , GHC == 7.8.4 , GHC == 7.10.1 , GHC == 7.10.2 + , GHC == 7.10.3 Cabal-version: >= 1.18 data-files: README.md , CHANGES.md @@ -40,7 +41,7 @@ , cmdargs >= 0.10.12 , split >= 0.2.2 - , clafer == 0.4.2.1 + , clafer == 0.4.3 other-modules: Paths_clafer library @@ -98,7 +99,6 @@ , Language.Clafer.Generator.Concat , Language.Clafer.Generator.Graph , Language.Clafer.Generator.Html - , Language.Clafer.Generator.Python , Language.Clafer.Generator.Stats , Language.Clafer.Intermediate.Desugarer , Language.Clafer.Intermediate.Intclafer @@ -140,7 +140,7 @@ , tasty-th >= 0.1.3 , transformers-compat >= 0.3 && < 0.5 , mtl-compat >= 0.2.1 - , clafer == 0.4.2.1 + , clafer == 0.4.3 ghc-options: -Wall diff --git a/src/Language/Clafer.hs b/src/Language/Clafer.hs --- a/src/Language/Clafer.hs +++ b/src/Language/Clafer.hs @@ -1,698 +1,679 @@ -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE NamedFieldPuns #-} -{- - Copyright (C) 2012-2015 Kacper Bak, Jimmy Liang, Michal Antkiewicz - - 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. --} -{- | Top-level interface to the Clafer compiler - -Normal usage: - -> t :: InputModel -> InputModel -> Either [ClaferErr] [String] -> t a b = -> runClafer defaultClaferArgs $ -> do -> addModuleFragment a -> addModuleFragment b -> parse -> iModule <- desugar "" -> compile iModule -> generate - -Example of compiling a model consisting of one fragment: - -> compileOneFragment :: ClaferArgs -> InputModel -> Either ClaferErr CompilerResult -> compileOneFragment args model = -> runClafer args $ -> do -> addModuleFragment model -> parse -> iModule <- desugar "http://mydomain.org/mymodel.cfr" -> compile iModule -> generate - -> compileTwoFragments :: ClaferArgs -> InputModel -> InputModel -> Either ClaferErr [String] -> compileTwoFragments args frag1 frag2 = -> runClafer args $ -> do -> addModuleFragment frag1 -> addModuleFragment frag2 -> parse -> iModule <- desugar "" -> compile iModule -> generate - -Use "throwErr" to halt execution: - -> runClafer args $ -> when (notValid args) $ throwErr (ClaferErr "Invalid arguments.") - -Use "catchErrs" to catch the errors. --} -module Language.Clafer - ( runCompiler - , addModuleFragment - , compile - , parse - , desugar - , generate - , generateHtml - , runClaferT - , runClafer - , ClaferErr - , getEnv - , putEnv - , CompilerResult(..) - , InputModel - , Token - , Module - , GEnv - , IModule - , ClaferEnv(..) - , getIr - , getAst - , makeEnv - , Pos(..) - , IrTrace(..) - , module Language.Clafer.ClaferArgs - , module Language.Clafer.Front.ErrM - ) where - -import Control.Lens.Plated -import Control.Monad -import Control.Monad.State -import Data.Aeson -import Data.Data.Lens -import Data.Either -import Data.List -import qualified Data.Map as Map -import Data.Maybe -import Data.String.Conversions -import System.Exit -import System.FilePath (dropExtension, takeBaseName) -import System.IO -import System.Process (readProcessWithExitCode, system) - -import Language.Clafer.ClaferArgs hiding (Clafer) -import qualified Language.Clafer.ClaferArgs as Mode (ClaferMode (Clafer)) -import Language.Clafer.Comments -import Language.Clafer.Common -import qualified Language.Clafer.Css as Css -import Language.Clafer.Front.AbsClafer -import Language.Clafer.Front.ErrM -import Language.Clafer.Front.LayoutResolver -import Language.Clafer.Front.LexClafer -import Language.Clafer.Front.ParClafer -import Language.Clafer.Front.PrintClafer -import Language.Clafer.Generator.Alloy -import Language.Clafer.Generator.Choco -import Language.Clafer.Generator.Concat -import Language.Clafer.Generator.Graph -import Language.Clafer.Generator.Html -import Language.Clafer.Generator.Python -import Language.Clafer.Generator.Stats -import Language.Clafer.Intermediate.Desugarer -import Language.Clafer.Intermediate.Intclafer -import Language.Clafer.Intermediate.Resolver -import Language.Clafer.Intermediate.ScopeAnalysis -import Language.Clafer.Intermediate.StringAnalyzer -import Language.Clafer.Intermediate.Tracing -import Language.Clafer.Intermediate.Transformer -import Language.Clafer.JSONMetaData -import Language.Clafer.Optimizer.Optimizer -import Language.Clafer.QNameUID -import Language.ClaferT - -type InputModel = String - --- | Run the Clafer compiler. --- mURL = Nothing means compile the top-level module --- mURL = Just url means compile an imported module from the given url -runCompiler :: Maybe URL -> ClaferArgs -> InputModel -> IO () -runCompiler mURL args' inputModel = - do - result <- runClaferT args' $ - do - forM_ (fragments inputModel) addModuleFragment - parse - iModule <- desugar mURL - {- need to runCompiler on imports - liftIO $ do - forM_ (_mModules iModule) $ \url -> do - -- use the same args just change the file name - importedModel <- retrieveModelFromURL url - runCompiler (Just url) (args' { file = getFileName url }) importedModel - -} - compile iModule - - when (validate args') $ liftIO $ do - hSetBuffering stdout LineBuffering - putStrLn $ "[clafer] Validating " ++ file args' - - fs <- save args' - - when (validate args') $ liftIO $ do - forM_ fs (runValidate args') - putStrLn "\n" - if Html `elem` (mode args') - then htmlCatch result args' inputModel - else return () - result `cth` handleErrs - where - cth (Left err) f = f err - cth (Right r) _ = return r - fragments model = map unlines $ fragments' $ lines model - fragments' [] = [] - fragments' ("//# FRAGMENT":xs) = fragments' $ " " : xs - fragments' model = takeWhile (/= "//# FRAGMENT") model : fragments' (dropWhile (/= "//# FRAGMENT") model) --- htmlCatch :: Either ClaferErr CompilerResult -> ClaferArgs -> String -> IO(CompilerResult) - htmlCatch (Right r) _ _ = return r - htmlCatch (Left err) args'' model = - do let f = (dropExtension $ file args'') ++ ".html" - let result = (if (self_contained args'') - then Css.header ++ "" ++ "\n\n
\n"
-                     else "")
-                     ++ highlightErrors model err ++
-                     (if (self_contained args'')
-                      then "\n
\n" - else "") - liftIO $ if console_output args'' then putStrLn result else writeFile f result - - handleErrs = mapM_ handleErr - - handleErr (ClaferErr mesg) = - do - putStrLn "\nError...\n" - putStrLn mesg - exitFailure - -- We only use one fragment. Fragment id and position is not useful to us. We - -- only care about the position relative to - handleErr (ParseErr ErrPos{modelPos = Pos l c} mesg) = - do - putStrLn $ "\nParse failed at line " ++ show l ++ " column " ++ show c ++ "..." - putStrLn mesg - exitFailure - handleErr (SemanticErr ErrPos{modelPos = Pos l c} mesg) = - do - putStrLn $ "\nCompile error at line " ++ show l ++ " column " ++ show c ++ "..." - putStrLn mesg - exitFailure - -save :: MonadIO m => ClaferArgs -> ClaferT m [ String ] -save args'= - do - resultsMap <- generate - let results = snd $ unzip $ Map.toList resultsMap - -- print stats only once - when (not $ no_stats args') $ liftIO $ printStats results - -- save the outputs - (iModule, _, _) <- getIr - forM results $ saveResult iModule resultsMap - where - -- saveResult :: MonadIO m => CompilerResult -> IModule -> (Map.Map ClaferMode CompilerResult) -> ClaferT m String - saveResult iModule' resultsMap' result@CompilerResult { extension } = do - result' <- if (add_graph args') && (Html `elem` (mode args') && ("dot" `isSuffixOf` (extension))) - then do - ast' <- getAst - (_, graph, _) <- liftIO $ readProcessWithExitCode "dot" ["-Tsvg"] $ genSimpleGraph ast' iModule' (takeBaseName $ file args') (show_references args') - return $ summary graph result - else return result - let f = dropExtension $ file args' - let f' = f ++ "." ++ extension - liftIO $ if console_output args' then putStrLn (outputCode result') else writeFile f' (outputCode result') - liftIO $ when (alloy_mapping args') $ writeFile (f ++ ".map") $ show (mappingToAlloy result') - let - qNameMaps :: QNameMaps - qNameMaps = deriveQNameMaps iModule' - liftIO $ when (meta_data args') $ writeFile (f ++ ".cfr-map") $ generateJSONnameUIDMap qNameMaps - liftIO $ when (meta_data args' && inScopeModes) $ writeFile (f ++ ".cfr-scope") $ generateJSONScopes qNameMaps $ getScopesList resultsMap' - return f' - saveResult _ _ NoCompilerResult { reason } = do - liftIO $ putStrLn reason - return "" - printStats :: [CompilerResult] -> IO () - printStats [] = putStrLn "No compiler output." - printStats (r:rs) = case r of - CompilerResult { statistics } -> putStrLn statistics - (NoCompilerResult _) -> printStats rs - - inScopeModes :: Bool - inScopeModes = - Alloy `elem` mode args' || - Choco `elem` mode args' - - getScopesList :: (Map.Map ClaferMode CompilerResult) -> [(UID, Integer)] - getScopesList resultsMap = - let - alloyResult = Map.lookup Alloy resultsMap - chocoResult = Map.lookup Choco resultsMap - in - if (isNothing alloyResult) - then if (isNothing chocoResult) - then [] - else scopesList $ fromJust chocoResult - else scopesList $ fromJust alloyResult - -summary :: String -> CompilerResult -> CompilerResult -summary graph result = result{outputCode=unlines $ summary' graph ("
" ++ statistics result ++ "
") (lines $ outputCode result)} - -summary' :: String -> String -> [String] -> [String] -summary' _ _ [] = [] -summary' graph stats ("":xs) = graph:stats:summary' graph stats xs -summary' graph stats ("":xs) = stats:summary' graph stats xs -summary' graph stats ("":xs) = graph:summary' graph stats xs -summary' graph stats ("":xs) = graph:summary' graph stats xs -summary' graph stats (x:xs) = x:summary' graph stats xs - -runValidate :: ClaferArgs -> String -> IO () -runValidate args' fo = do - let path = (tooldir args') ++ "/" - let modes = mode args' - when (Alloy `elem` modes && ".als" `isSuffixOf` fo) $ do - void $ system $ validateAlloy path ++ fo - when (Choco `elem` modes && ".js" `isSuffixOf` fo) $ do - void $ system $ validateChoco path ++ fo - when (Graph `elem` modes && ".dot" `isSuffixOf` fo) $ do - liftIO $ putStrLn ("=========== Parsing+Generating " ++ fo ++ " =============") - void $ system $ validateGraph ++ fo - when (Mode.Clafer `elem` modes && ".des.cfr" `isSuffixOf` fo) $ do - liftIO $ putStrLn ("=========== Parsing+Typechecking " ++ fo ++ " =============") - void $ system $ validateClafer path ++ fo - -validateAlloy :: String -> String -validateAlloy path = "java -cp " ++ path ++ "alloy4.2.jar edu.mit.csail.sdg.alloy4whole.ExampleUsingTheCompiler " - -validateChoco :: String -> String -validateChoco path = "java -jar " ++ path ++ "claferchocoig.jar -v --file " - -validateGraph :: String -validateGraph = "dot -Tsvg -O " - -validateClafer :: String -> String -validateClafer path = path ++ "clafer -s -m=clafer " - - --- | Add a new fragment to the model. Fragments should be added in order. -addModuleFragment :: Monad m => InputModel -> ClaferT m () -addModuleFragment i = - do - env <- getEnv - let modelFrags' = modelFrags env ++ [i] - let frags' = frags env ++ [(endPos $ concat modelFrags')] - putEnv env{ modelFrags = modelFrags', frags = frags' } - where - endPos "" = Pos 1 1 - endPos model = - Pos line' column' - where - input' = lines' model - line' = toInteger $ length input' - column' = 1 + (toInteger $ length $ last input') - -- Can't use the builtin lines because it ignores the last empty lines (as of base 4.5). - lines' "" = [""] - lines' input'' = - line'' : rest' - where - (line'', rest) = break (== '\n') input'' - rest' = - case rest of - "" -> [] - ('\n' : r) -> lines' r - x -> error $ "linesing " ++ x -- How can it be nonempty and not start with a newline after the break? Should never happen. - --- | Converts the Err monads (created by the BNFC parser generator) to ClaferT -liftParseErrs :: Monad m => [Err a] -> ClaferT m [a] -liftParseErrs e = - do - result <- zipWithM extract [0..] e - case partitionEithers result of - ([], ok) -> return ok - (e', _) -> throwErrs e' - where - extract _ (Ok m) = return $ Right m - extract frgId (Bad p s) = - do - -- Bad maps to ParseErr - return $ Left $ ParseErr (ErrFragPos frgId p) s - --- | Converts one Err. liftParseErrs is better if you want to report multiple errors. --- | This method will only report one before ceasing execution. -liftParseErr :: Monad m => Err a -> ClaferT m a -liftParseErr e = head `liftM` liftParseErrs [e] - - --- | Parses the model into AST. Adding more fragments beyond this point will have no effect. -parse :: Monad m => ClaferT m () -parse = - do - env <- getEnv - let completeModel = concat $ modelFrags env - - (astErr, otherTokens') <- (parseFrag $ args env) completeModel - ast <- liftParseErr astErr - - putEnv env{ cAst = Just ast, astModuleTrace = traceAstModule ast, otherTokens = otherTokens' } - where - parseFrag :: (Monad m) => ClaferArgs -> String -> ClaferT m (Err Module, [Token]) - parseFrag args' inputModel = do - let model' = if (not $ no_layout args') && (new_layout args') then resLayout inputModel else inputModel - let allTokens = myLexer model' - let (parseableTokens, otherTokens') = partition isParseable allTokens - tokens2 <- if not ((new_layout args') || (no_layout args')) then resolveLayout parseableTokens else return parseableTokens - return (pModule tokens2, otherTokens') - where - isParseable (PT _ (T_PosLineComment _)) = False - isParseable (PT _ (T_PosBlockComment _)) = False - isParseable (PT _ (T_PosAlloy _)) = False - isParseable (PT _ (T_PosChoco _)) = False - isParseable _ = True - -desugar :: Monad m => Maybe URL -> ClaferT m IModule -desugar mURL = do - ast' <- getAst - return $ desugarModule mURL ast' - --- | Compiles the AST into IR. -compile :: Monad m => IModule -> ClaferT m () -compile desugaredMod = do - env <- getEnv - let clafersWithKeyWords = foldMapIR isKeyWord desugaredMod - when (""/=clafersWithKeyWords) $ throwErr (ClaferErr $ ("The model contains clafers with keywords as names in the following places:\n"++) $ clafersWithKeyWords :: CErr Span) - ir <- analyze (args env) desugaredMod - let (imodule, _, _) = ir - - let spanList = foldMapIR gt1 imodule - when ((afm $ args env) && spanList/="") $ throwErr (ClaferErr $ ("The model is not an attributed feature model.\nThe following places contain cardinality larger than 1:\n"++) $ spanList :: CErr Span) - putEnv $ env{ cIr = Just ir } - where - isKeyWord :: Ir -> String - isKeyWord (IRClafer IClafer{_cinPos = (Span (Pos l c) _) ,_ident=i}) = if (i `elem` keywordIdents) then ("Line " ++ show l ++ " column " ++ show c ++ "\n") else "" - isKeyWord _ = "" - gt1 :: Ir -> String - gt1 (IRClafer (IClafer (Span (Pos l c) _) False _ _ _ _ _ _ (Just (_, m)) _ _)) = if (m > 1 || m < 0) then ("Line " ++ show l ++ " column " ++ show c ++ "\n") else "" - gt1 _ = "" - - --- | Splits the AST into their fragments, and generates the output for each fragment. -generateHtml :: ClaferEnv -> String -generateHtml env = - let (Just (Module _ decls')) = cAst env; - cargs = args env; - irMap = irModuleTrace env; - comments = if add_comments cargs then getComments $ unlines $ modelFrags env else []; - in (if (self_contained cargs) then Css.header ++ "\n\n" else "") - ++ (unlines $ genFragments decls' (frags env) irMap comments) ++ - (if (self_contained cargs) then "\n" else "") - - where - lne :: Declaration -> Pos - lne (ElementDecl (Span p _) _) = p - lne (EnumDecl (Span p _) _ _) = p - genFragments :: [Declaration] -> [Pos] -> Map.Map Span [Ir] -> [(Span, String)] -> [String] - genFragments [] _ _ comments = printComments comments - genFragments (decl:decls') [] irMap comments = let (comments', c) = printPreComment (getSpan decl) comments in - [c] ++ (cleanOutput $ revertLayout $ printDeclaration decl 0 irMap True $ inDecl decl comments') : (genFragments decls' [] irMap $ afterDecl decl comments') - genFragments (decl:decls') (frg:frgs) irMap comments = if lne decl < frg - then let (comments', c) = printPreComment (getSpan decl) comments in - [c] ++ (cleanOutput $ revertLayout $ printDeclaration decl 0 irMap True $ inDecl decl comments') : (genFragments decls' (frg:frgs) irMap $ afterDecl decl comments') - else "" : genFragments (decl:decls') frgs irMap comments - inDecl :: Declaration -> [(Span, String)] -> [(Span, String)] - inDecl decl comments = let s = getSpan decl in dropWhile (\x -> fst x <= s) comments - afterDecl :: Declaration -> [(Span, String)] -> [(Span, String)] - afterDecl decl comments = let (Span _ (Pos line' _)) = getSpan decl in dropWhile (\(x, _) -> let (Span _ (Pos line'' _)) = x in line'' <= line') comments - printComments [] = [] - printComments ((s, comment):cs') = (snd (printComment s [(s, comment)]) ++ "
\n"):printComments cs' - -iExpBasedChecks :: IModule -> (Bool, Bool, Bool) -iExpBasedChecks iModule = (null realLiterals, null productOperators, null minMaxOperators) - where - iexps :: [ IExp ] - iexps = universeOn biplate iModule - realLiterals = filter isIDouble iexps - productOperators = filter isProductOperator iexps - minMaxOperators = filter isMinMaxOperator iexps - isIDouble (IDouble _) = True - isIDouble (IReal _) = True - isIDouble _ = False - isProductOperator (IFunExp op' _) = op' == iProdSet - isProductOperator _ = False - isMinMaxOperator (IFunExp op' _) = op' `elem` [iMinimum, iMaximum] - isMinMaxOperator _ = False - -iClaferBasedChecks :: IModule -> Bool -iClaferBasedChecks iModule = null $ filter hasReferenceToReal iClafers - where - iClafers :: [ IClafer ] - iClafers = universeOn biplate iModule - hasReferenceToReal (IClafer{_reference=(Just IReference{_ref=pexp'})}) = any (`elem` [ "real", "double" ]) $ getRefIds pexp' - hasReferenceToReal _ = False - --- | Generates outputs for the given IR. -generate :: Monad m => ClaferT m (Map.Map ClaferMode CompilerResult) -generate = - do - env <- getEnv - ast' <- getAst - (iModule, genv, au) <- getIr - let - (hasNoRealLiterals, hasNoProductOperator, hasNoMinMaxOperator) = iExpBasedChecks iModule - hasNoReferenceToReal = iClaferBasedChecks iModule - cargs = args env - otherTokens' = otherTokens env - modes = mode cargs - stats = showStats au $ statsModule iModule - scopes = getScopeStrategy (scope_strategy cargs) iModule - - return $ Map.fromList ( - -- result for Alloy - (if (Alloy `elem` modes) - then if (hasNoRealLiterals && hasNoReferenceToReal && hasNoProductOperator && hasNoMinMaxOperator) - then - let - (imod,strMap) = astrModule iModule - alloyCode = genModule cargs{mode = [Alloy]} (imod, genv) scopes otherTokens' - addCommentStats = if no_stats cargs then const else addStats - in - [ (Alloy, - CompilerResult { - extension = "als", - outputCode = addCommentStats (fst alloyCode) stats, - statistics = stats, - claferEnv = env, - mappingToAlloy = fromMaybe [] (Just $ snd alloyCode), - stringMap = strMap, - scopesList = scopes - }) - ] - else [ (Alloy, - NoCompilerResult { - reason = "Alloy output unavailable because the model contains: " - ++ (if hasNoRealLiterals then "" else "a real number literal, ") - ++ (if hasNoReferenceToReal then "" else "a reference to a real, ") - ++ (if hasNoProductOperator then "" else "the product operator, ") - ++ (if hasNoMinMaxOperator then "" else "the min or max operator, ") - }) - ] - else [] - ) - -- result for JSON - ++ (if (JSON `elem` modes) - then [ (JSON, - CompilerResult { - extension = "json", - outputCode = concat - [ "{" - , (case gatherObjectivesAndAttributes iModule $ astModuleTrace env of - Nothing -> "" - Just objectives -> "\"objectives\":" ++ (convertString $ encode $ toJSON objectives) ++ ",") - , "\"iModule\":" - , convertString $ encode $ toJSON iModule - , "}" - ], - statistics = stats, - claferEnv = env, - mappingToAlloy = [], - stringMap = Map.empty, - scopesList = [] - }) ] - else [] - ) - -- result for Clafer - ++ (if (Mode.Clafer `elem` modes) - then [ (Mode.Clafer, - CompilerResult { - extension = "des.cfr", - outputCode = printTree $ sugarModule iModule, - statistics = stats, - claferEnv = env, - mappingToAlloy = [], - stringMap = Map.empty, - scopesList = [] - }) ] - else [] - ) - -- result for Html - ++ (if (Html `elem` modes) - then [ (Html, - CompilerResult { - extension = "html", - outputCode = generateHtml env, - statistics = stats, - claferEnv = env, - mappingToAlloy = [], - stringMap = Map.empty, - scopesList = [] - }) ] - else [] - ) - ++ (if (Graph `elem` modes) - then [ (Graph, - CompilerResult { - extension = "dot", - outputCode = genSimpleGraph ast' iModule (takeBaseName $ file cargs) (show_references cargs), - statistics = stats, - claferEnv = env, - mappingToAlloy = [], - stringMap = Map.empty, - scopesList = [] - }) ] - else [] - ) - ++ (if (CVLGraph `elem` modes) - then [ (CVLGraph, - CompilerResult { - extension = "cvl.dot", - outputCode = genCVLGraph ast' iModule (takeBaseName $ file cargs), - statistics = stats, - claferEnv = env, - mappingToAlloy = [], - stringMap = Map.empty, - scopesList = [] - }) ] - else [] - ) - -- result for Python - ++ (if (Python `elem` modes) - then [ (Python, - CompilerResult { - extension = "py", - outputCode = genPythonModule (iModule, genv) scopes, - statistics = stats, - claferEnv = env, - mappingToAlloy = [], - stringMap = Map.empty, - scopesList = scopes - }) ] - else [] - ) - -- result for Choco - ++ (if (Choco `elem` modes) - then if (hasNoRealLiterals && hasNoReferenceToReal) - then [ (Choco, - CompilerResult { - extension = "js", - outputCode = genCModule (iModule, genv) scopes otherTokens', - statistics = stats, - claferEnv = env, - mappingToAlloy = [], - stringMap = Map.empty, - scopesList = scopes - }) ] - else [ (Choco, - NoCompilerResult { - reason = "Choco output unavailable because the model contains: " - ++ (if hasNoRealLiterals then "" else "a real number literal, ") - ++ (if hasNoReferenceToReal then "" else "a reference to a real, ") - }) - ] - else [] - )) - --- | Result of generation for a given mode -data CompilerResult - = CompilerResult - { extension :: String -- ^ output file extension - , outputCode :: String -- ^ output text - , statistics :: String -- ^ the final environment of the compiler - , claferEnv :: ClaferEnv -- ^ Maps source constraint spans in Alloy to the spans in the IR - , mappingToAlloy :: [(Span, IrTrace)] -- ^ Map back from Ints used to represent Strings - , stringMap :: (Map.Map Int String) -- ^ scopes generated by scope inference - , scopesList :: [(UID, Integer)] - } - | NoCompilerResult - { reason :: String - } - deriving Show - -liftError :: (Monad m, Language.ClaferT.Throwable t) => Either t a -> ClaferT m a -liftError = either throwErr return - -analyze :: Monad m => ClaferArgs -> IModule -> ClaferT m (IModule, GEnv, Bool) -analyze args' iModule = do - _ <-liftError $ findDupModule args' iModule - let - au = allUnique iModule - let args'' = args'{skip_resolver = au && (skip_resolver args')} - (rTree, genv) <- liftError $ resolveModule args'' iModule - let tTree = transModule rTree - return (optimizeModule args'' (tTree, genv), genv, au) - -addStats :: String -> String -> String -addStats code stats = "/*\n" ++ stats ++ "*/\n" ++ code - -showStats :: Bool -> Stats -> String -showStats au (Stats na nr nc nconst ngoals sgl) = - unlines [ "All clafers: " ++ (show (na + nc)) ++ " | Abstract: " ++ (show na) ++ " | Concrete: " ++ (show nc) ++ " | Reference: " ++ (show nr) - , "Constraints: " ++ show nconst - , "Goals: " ++ show ngoals - , "Global scope: " ++ showInterval sgl - , "Can skip name resolver: " ++ if au then "yes" else "no" ] - -showInterval :: (Integer, Integer) -> String -showInterval (n, -1) = show n ++ "..*" -showInterval (n, m) = show n ++ ".." ++ show m - -gatherObjectivesAndAttributes :: IModule -> Map.Map Span [Ast] -> Maybe ObjectivesAndAttributes -gatherObjectivesAndAttributes iModule astModuleTrace' = let - objectives = (foldl' gatherObjectives [] $ _mDecls iModule) - in if null objectives - then Nothing - else Just $ ObjectivesAndAttributes objectives (map _uid $ filter isIntClafer iClafers) - where - gatherObjectives :: [String] -> IElement -> [String] - gatherObjectives objs (IEGoal _ cpexp') = - printCPexp (Map.lookup (_inPos cpexp') astModuleTrace') - :objs - gatherObjectives objs _ = objs - - printCPexp :: Maybe [Ast] -> String - printCPexp (Just [_,_,(AstGoal g)]) = case g of - GoalMinimize _ [e] -> "min " ++ (printTree e) - GoalMaximize _ [e] -> "max " ++ (printTree e) - GoalMinDeprecated _ [e] -> "min " ++ (printTree e) - GoalMaxDeprecated _ [e] -> "max " ++ (printTree e) - g' -> "[BUG]: unexpected goal found!" ++ show g' - printCPexp e = "[BUG]: expression not found!" ++ show e - - iClafers :: [ IClafer ] - iClafers = universeOn biplate iModule - - isIntClafer (IClafer{_reference=(Just IReference{_ref=pexp'})}) = any (`elem` ["integer", "int"]) $ getRefIds pexp' - isIntClafer _ = False +{-# LANGUAGE NamedFieldPuns #-} +{- + Copyright (C) 2012-2015 Kacper Bak, Jimmy Liang, Michal Antkiewicz + + 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. +-} +{- | Top-level interface to the Clafer compiler + +Normal usage: + +> t :: InputModel -> InputModel -> Either [ClaferErr] [String] +> t a b = +> runClafer defaultClaferArgs $ +> do +> addModuleFragment a +> addModuleFragment b +> parse +> iModule <- desugar "" +> compile iModule +> generate + +Example of compiling a model consisting of one fragment: + +> compileOneFragment :: ClaferArgs -> InputModel -> Either ClaferErr CompilerResult +> compileOneFragment args model = +> runClafer args $ +> do +> addModuleFragment model +> parse +> iModule <- desugar "http://mydomain.org/mymodel.cfr" +> compile iModule +> generate + +> compileTwoFragments :: ClaferArgs -> InputModel -> InputModel -> Either ClaferErr [String] +> compileTwoFragments args frag1 frag2 = +> runClafer args $ +> do +> addModuleFragment frag1 +> addModuleFragment frag2 +> parse +> iModule <- desugar "" +> compile iModule +> generate + +Use "throwErr" to halt execution: + +> runClafer args $ +> when (notValid args) $ throwErr (ClaferErr "Invalid arguments.") + +Use "catchErrs" to catch the errors. +-} +module Language.Clafer + ( runCompiler + , addModuleFragment + , compile + , parse + , desugar + , generate + , generateHtml + , runClaferT + , runClafer + , ClaferErr + , getEnv + , putEnv + , CompilerResult(..) + , InputModel + , Token + , Module + , GEnv + , IModule + , ClaferEnv(..) + , getIr + , getAst + , makeEnv + , Pos(..) + , IrTrace(..) + , module Language.Clafer.ClaferArgs + , module Language.Clafer.Front.ErrM + ) where + +import Control.Lens.Plated +import Control.Monad +import Control.Monad.State +import Data.Aeson +import Data.Data.Lens +import Data.Either +import Data.List +import qualified Data.Map as Map +import Data.Maybe +import Data.String.Conversions +import System.Exit +import System.FilePath (dropExtension, takeBaseName) +import System.IO +import System.Process (readProcessWithExitCode, system) + +import Language.Clafer.ClaferArgs hiding (Clafer) +import qualified Language.Clafer.ClaferArgs as Mode (ClaferMode (Clafer)) +import Language.Clafer.Comments +import Language.Clafer.Common +import qualified Language.Clafer.Css as Css +import Language.Clafer.Front.AbsClafer +import Language.Clafer.Front.ErrM +import Language.Clafer.Front.LayoutResolver +import Language.Clafer.Front.LexClafer +import Language.Clafer.Front.ParClafer +import Language.Clafer.Front.PrintClafer +import Language.Clafer.Generator.Alloy +import Language.Clafer.Generator.Choco +import Language.Clafer.Generator.Concat +import Language.Clafer.Generator.Graph +import Language.Clafer.Generator.Html +import Language.Clafer.Generator.Stats +import Language.Clafer.Intermediate.Desugarer +import Language.Clafer.Intermediate.Intclafer +import Language.Clafer.Intermediate.Resolver +import Language.Clafer.Intermediate.ScopeAnalysis +import Language.Clafer.Intermediate.StringAnalyzer +import Language.Clafer.Intermediate.Tracing +import Language.Clafer.Intermediate.Transformer +import Language.Clafer.JSONMetaData +import Language.Clafer.Optimizer.Optimizer +import Language.Clafer.QNameUID +import Language.ClaferT + +type InputModel = String + +-- | Run the Clafer compiler. +-- mURL = Nothing means compile the top-level module +-- mURL = Just url means compile an imported module from the given url +runCompiler :: Maybe URL -> ClaferArgs -> InputModel -> IO () +runCompiler mURL args' inputModel = + do + hSetBuffering stdout LineBuffering + result <- runClaferT args' $ + do + forM_ (fragments inputModel) addModuleFragment + parse + iModule <- desugar mURL + {- need to runCompiler on imports + liftIO $ do + forM_ (_mModules iModule) $ \url -> do + -- use the same args just change the file name + importedModel <- retrieveModelFromURL url + runCompiler (Just url) (args' { file = getFileName url }) importedModel + -} + compile iModule + + fs <- save args' + + when (validate args') $ liftIO $ do + putStrLn $ "[clafer] Validating " ++ file args' + + when (validate args') $ liftIO $ do + forM_ fs (runValidate args') + putStrLn "\n" + when (Html `elem` mode args') $ + htmlCatch result args' inputModel + result `cth` handleErrs + where + cth (Left err) f = f err + cth (Right r) _ = return r + fragments model = map unlines $ fragments' $ lines model + fragments' [] = [] + fragments' ("//# FRAGMENT":xs) = fragments' $ " " : xs + fragments' model = takeWhile (/= "//# FRAGMENT") model : fragments' (dropWhile (/= "//# FRAGMENT") model) +-- htmlCatch :: Either ClaferErr CompilerResult -> ClaferArgs -> String -> IO(CompilerResult) + htmlCatch (Right r) _ _ = return r + htmlCatch (Left err) args'' model = + do let f = dropExtension (file args'') ++ ".html" + let result = (if (self_contained args'') + then Css.header ++ "" ++ "\n\n
\n"
+                     else "")
+                     ++ highlightErrors model err ++
+                     (if (self_contained args'')
+                      then "\n
\n" + else "") + liftIO $ if console_output args'' then putStrLn result else writeFile f result + + handleErrs = mapM_ handleErr + + handleErr (ClaferErr mesg) = + do + putStrLn "\nError...\n" + putStrLn mesg + exitFailure + -- We only use one fragment. Fragment id and position is not useful to us. We + -- only care about the position relative to + handleErr (ParseErr ErrPos{modelPos = Pos l c} mesg) = + do + putStrLn $ "\nParse failed at line " ++ show l ++ " column " ++ show c ++ "..." + putStrLn mesg + exitFailure + handleErr (SemanticErr ErrPos{modelPos = Pos l c} mesg) = + do + putStrLn $ "\nCompile error at line " ++ show l ++ " column " ++ show c ++ "..." + putStrLn mesg + exitFailure + +save :: MonadIO m => ClaferArgs -> ClaferT m [ String ] +save args'= + do + resultsMap <- generate + let results = snd $ unzip $ Map.toList resultsMap + -- print stats only once + unless (no_stats args') $ liftIO $ printStats results + -- save the outputs + (iModule, _, _) <- getIr + forM results $ saveResult iModule resultsMap + where + -- saveResult :: MonadIO m => CompilerResult -> IModule -> (Map.Map ClaferMode CompilerResult) -> ClaferT m String + saveResult iModule' resultsMap' result@CompilerResult { extension } = do + result' <- if (add_graph args') && (Html `elem` (mode args') && ("dot" `isSuffixOf` (extension))) + then do + ast' <- getAst + (_, graph, _) <- liftIO $ readProcessWithExitCode "dot" ["-Tsvg"] $ genSimpleGraph ast' iModule' (takeBaseName $ file args') (show_references args') + return $ summary graph result + else return result + let f = dropExtension $ file args' + let f' = f ++ "." ++ extension + liftIO $ if console_output args' then putStrLn (outputCode result') else writeFile f' (outputCode result') + liftIO $ when (alloy_mapping args') $ writeFile (f ++ ".map") $ show (mappingToAlloy result') + let + qNameMaps :: QNameMaps + qNameMaps = deriveQNameMaps iModule' + liftIO $ when (meta_data args') $ writeFile (f ++ ".cfr-map") $ generateJSONnameUIDMap qNameMaps + liftIO $ when (meta_data args' && inScopeModes) $ writeFile (f ++ ".cfr-scope") $ generateJSONScopes qNameMaps $ getScopesList resultsMap' + return f' + saveResult _ _ NoCompilerResult { reason } = do + liftIO $ putStrLn reason + return "" + printStats :: [CompilerResult] -> IO () + printStats [] = putStrLn "No compiler output." + printStats (r:rs) = case r of + CompilerResult { statistics } -> putStrLn statistics + (NoCompilerResult _) -> printStats rs + + inScopeModes :: Bool + inScopeModes = + Alloy `elem` mode args' || + Choco `elem` mode args' + + getScopesList :: Map.Map ClaferMode CompilerResult -> [(UID, Integer)] + getScopesList resultsMap = + let + alloyResult = Map.lookup Alloy resultsMap + chocoResult = Map.lookup Choco resultsMap + in + if (isNothing alloyResult) + then if (isNothing chocoResult) + then [] + else scopesList $ fromJust chocoResult + else scopesList $ fromJust alloyResult + +summary :: String -> CompilerResult -> CompilerResult +summary graph result = result{outputCode=unlines $ summary' graph ("
" ++ statistics result ++ "
") (lines $ outputCode result)} + +summary' :: String -> String -> [String] -> [String] +summary' _ _ [] = [] +summary' graph stats ("":xs) = graph:stats:summary' graph stats xs +summary' graph stats ("":xs) = stats:summary' graph stats xs +summary' graph stats ("":xs) = graph:summary' graph stats xs +summary' graph stats ("":xs) = graph:summary' graph stats xs +summary' graph stats (x:xs) = x:summary' graph stats xs + +runValidate :: ClaferArgs -> String -> IO () +runValidate args' fo = do + let path = (tooldir args') ++ "/" + let modes = mode args' + let fo' = "\"" ++ fo ++ "\"" + when (Alloy `elem` modes && ".als" `isSuffixOf` fo) $ do + void $ system $ validateAlloy path ++ fo' + when (Choco `elem` modes && ".js" `isSuffixOf` fo) $ do + void $ system $ validateChoco path ++ fo' + when (Graph `elem` modes && ".dot" `isSuffixOf` fo) $ do + liftIO $ putStrLn ("=========== Parsing+Generating " ++ fo ++ " =============") + void $ system $ validateGraph ++ fo' + -- when (Mode.Clafer `elem` modes && ".des.cfr" `isSuffixOf` fo) $ do + -- liftIO $ putStrLn ("=========== Parsing+Typechecking " ++ fo ++ " =============") + -- liftIO $ putStrLn $ validateClafer path ++ fo' + -- void $ system $ validateClafer path ++ fo' + +validateAlloy :: String -> String +validateAlloy path = "java -cp \"" ++ path ++ "alloy4.2.jar\" edu.mit.csail.sdg.alloy4whole.ExampleUsingTheCompiler " + +validateChoco :: String -> String +validateChoco path = "java -jar \"" ++ path ++ "chocosolver.jar\" -v --file " + +validateGraph :: String +validateGraph = "dot -Tsvg -O " + +-- validateClafer :: String -> String +-- validateClafer path = "\"" ++ path ++ "clafer\" -s -k -m=clafer " + + +-- | Add a new fragment to the model. Fragments should be added in order. +addModuleFragment :: Monad m => InputModel -> ClaferT m () +addModuleFragment i = + do + env <- getEnv + let modelFrags' = modelFrags env ++ [i] + let frags' = frags env ++ [(endPos $ concat modelFrags')] + putEnv env{ modelFrags = modelFrags', frags = frags' } + where + endPos "" = Pos 1 1 + endPos model = + Pos line' column' + where + input' = lines' model + line' = toInteger $ length input' + column' = 1 + (toInteger $ length $ last input') + -- Can't use the builtin lines because it ignores the last empty lines (as of base 4.5). + lines' "" = [""] + lines' input'' = + line'' : rest' + where + (line'', rest) = break (== '\n') input'' + rest' = + case rest of + "" -> [] + ('\n' : r) -> lines' r + x -> error $ "linesing " ++ x -- How can it be nonempty and not start with a newline after the break? Should never happen. + +-- | Converts the Err monads (created by the BNFC parser generator) to ClaferT +liftParseErrs :: Monad m => [Err a] -> ClaferT m [a] +liftParseErrs e = + do + result <- zipWithM extract [0..] e + case partitionEithers result of + ([], ok) -> return ok + (e', _) -> throwErrs e' + where + extract _ (Ok m) = return $ Right m + extract frgId (Bad p s) = + do + -- Bad maps to ParseErr + return $ Left $ ParseErr (ErrFragPos frgId p) s + +-- | Converts one Err. liftParseErrs is better if you want to report multiple errors. +-- | This method will only report one before ceasing execution. +liftParseErr :: Monad m => Err a -> ClaferT m a +liftParseErr e = head `liftM` liftParseErrs [e] + + +-- | Parses the model into AST. Adding more fragments beyond this point will have no effect. +parse :: Monad m => ClaferT m () +parse = + do + env <- getEnv + let completeModel = concat $ modelFrags env + + (astErr, otherTokens') <- (parseFrag $ args env) completeModel + ast <- liftParseErr astErr + + putEnv env{ cAst = Just ast, astModuleTrace = traceAstModule ast, otherTokens = otherTokens' } + where + parseFrag :: (Monad m) => ClaferArgs -> String -> ClaferT m (Err Module, [Token]) + parseFrag args' inputModel = do + let model' = if (not $ no_layout args') && (new_layout args') then resLayout inputModel else inputModel + let allTokens = myLexer model' + let (parseableTokens, otherTokens') = partition isParseable allTokens + tokens2 <- if not ((new_layout args') || (no_layout args')) then resolveLayout parseableTokens else return parseableTokens + return (pModule tokens2, otherTokens') + where + isParseable (PT _ (T_PosLineComment _)) = False + isParseable (PT _ (T_PosBlockComment _)) = False + isParseable (PT _ (T_PosAlloy _)) = False + isParseable (PT _ (T_PosChoco _)) = False + isParseable _ = True + +desugar :: Monad m => Maybe URL -> ClaferT m IModule +desugar mURL = do + ast' <- getAst + return $ desugarModule mURL ast' + +-- | Compiles the AST into IR. +compile :: Monad m => IModule -> ClaferT m () +compile desugaredMod = do + env <- getEnv + let clafersWithKeyWords = foldMapIR isKeyWord desugaredMod + when (""/=clafersWithKeyWords) $ throwErr (ClaferErr $ ("The model contains clafers with keywords as names in the following places:\n"++) $ clafersWithKeyWords :: CErr Span) + ir <- analyze (args env) desugaredMod + let (imodule, _, _) = ir + + let spanList = foldMapIR gt1 imodule + when ((afm $ args env) && spanList/="") $ throwErr (ClaferErr $ ("The model is not an attributed feature model.\nThe following places contain cardinality larger than 1:\n"++) $ spanList :: CErr Span) + putEnv $ env{ cIr = Just ir } + where + isKeyWord :: Ir -> String + isKeyWord (IRClafer IClafer{_cinPos = (Span (Pos l c) _) ,_ident=i}) = if (i `elem` keywordIdents) then ("Line " ++ show l ++ " column " ++ show c ++ "\n") else "" + isKeyWord _ = "" + gt1 :: Ir -> String + gt1 (IRClafer (IClafer (Span (Pos l c) _) False _ _ _ _ _ _ (Just (_, m)) _ _)) = if (m > 1 || m < 0) then ("Line " ++ show l ++ " column " ++ show c ++ "\n") else "" + gt1 _ = "" + + +-- | Splits the AST into their fragments, and generates the output for each fragment. +generateHtml :: ClaferEnv -> String +generateHtml env = + let (Just (Module _ decls')) = cAst env; + cargs = args env; + irMap = irModuleTrace env; + comments = if add_comments cargs then getComments $ unlines $ modelFrags env else []; + in (if (self_contained cargs) then Css.header ++ "\n\n" else "") + ++ (unlines $ genFragments decls' (frags env) irMap comments) ++ + (if (self_contained cargs) then "\n" else "") + + where + lne :: Declaration -> Pos + lne (ElementDecl (Span p _) _) = p + lne (EnumDecl (Span p _) _ _) = p + genFragments :: [Declaration] -> [Pos] -> Map.Map Span [Ir] -> [(Span, String)] -> [String] + genFragments [] _ _ comments = printComments comments + genFragments (decl:decls') [] irMap comments = let (comments', c) = printPreComment (getSpan decl) comments in + [c] ++ (cleanOutput $ revertLayout $ printDeclaration decl 0 irMap True $ inDecl decl comments') : (genFragments decls' [] irMap $ afterDecl decl comments') + genFragments (decl:decls') (frg:frgs) irMap comments = if lne decl < frg + then let (comments', c) = printPreComment (getSpan decl) comments in + [c] ++ (cleanOutput $ revertLayout $ printDeclaration decl 0 irMap True $ inDecl decl comments') : (genFragments decls' (frg:frgs) irMap $ afterDecl decl comments') + else "" : genFragments (decl:decls') frgs irMap comments + inDecl :: Declaration -> [(Span, String)] -> [(Span, String)] + inDecl decl comments = let s = getSpan decl in dropWhile (\x -> fst x <= s) comments + afterDecl :: Declaration -> [(Span, String)] -> [(Span, String)] + afterDecl decl comments = let (Span _ (Pos line' _)) = getSpan decl in dropWhile (\(x, _) -> let (Span _ (Pos line'' _)) = x in line'' <= line') comments + printComments [] = [] + printComments ((s, comment):cs') = (snd (printComment s [(s, comment)]) ++ "
\n"):printComments cs' + +iExpBasedChecks :: IModule -> (Bool, Bool) +iExpBasedChecks iModule = (null realLiterals, null productOperators) + where + iexps :: [ IExp ] + iexps = universeOn biplate iModule + realLiterals = filter isIDouble iexps + productOperators = filter isProductOperator iexps + isIDouble (IDouble _) = True + isIDouble (IReal _) = True + isIDouble _ = False + isProductOperator (IFunExp op' _) = op' == iProdSet + isProductOperator _ = False + +iClaferBasedChecks :: IModule -> Bool +iClaferBasedChecks iModule = null $ filter hasReferenceToReal iClafers + where + iClafers :: [ IClafer ] + iClafers = universeOn biplate iModule + hasReferenceToReal (IClafer{_reference=(Just IReference{_ref=pexp'})}) = any (`elem` [ "real", "double" ]) $ getRefIds pexp' + hasReferenceToReal _ = False + +-- | Generates outputs for the given IR. +generate :: Monad m => ClaferT m (Map.Map ClaferMode CompilerResult) +generate = + do + env <- getEnv + ast' <- getAst + (iModule, genv, au) <- getIr + let + (hasNoRealLiterals, hasNoProductOperator) = iExpBasedChecks iModule + hasNoReferenceToReal = iClaferBasedChecks iModule + cargs = args env + otherTokens' = otherTokens env + modes = mode cargs + stats = showStats au $ statsModule iModule + scopes = getScopeStrategy (scope_strategy cargs) iModule + + return $ Map.fromList ( + -- result for Alloy + (if (Alloy `elem` modes) + then if (hasNoRealLiterals && hasNoReferenceToReal && hasNoProductOperator) + then + let + (imod,strMap) = astrModule iModule + alloyCode = genModule cargs{mode = [Alloy]} (imod, genv) scopes otherTokens' + addCommentStats = if no_stats cargs then const else addStats + in + [ (Alloy, + CompilerResult { + extension = "als", + outputCode = addCommentStats (fst alloyCode) stats, + statistics = stats, + claferEnv = env, + mappingToAlloy = fromMaybe [] (Just $ snd alloyCode), + stringMap = strMap, + scopesList = scopes + }) + ] + else [ (Alloy, + NoCompilerResult { + reason = "Alloy output unavailable because the model contains: " + ++ (if hasNoRealLiterals then "" else "a real number literal, ") + ++ (if hasNoReferenceToReal then "" else "a reference to a real, ") + ++ (if hasNoProductOperator then "" else "the product operator, ") + }) + ] + else [] + ) + -- result for JSON + ++ (if (JSON `elem` modes) + then [ (JSON, + CompilerResult { + extension = "json", + outputCode = concat + [ "{" + , (case gatherObjectivesAndAttributes iModule $ astModuleTrace env of + Nothing -> "" + Just objectives -> "\"objectives\":" ++ (convertString $ encode $ toJSON objectives) ++ ",") + , "\"iModule\":" + , convertString $ encode $ toJSON iModule + , "}" + ], + statistics = stats, + claferEnv = env, + mappingToAlloy = [], + stringMap = Map.empty, + scopesList = [] + }) ] + else [] + ) + -- result for Clafer + ++ (if (Mode.Clafer `elem` modes) + then [ (Mode.Clafer, + CompilerResult { + extension = "des.cfr", + outputCode = printTree $ sugarModule iModule, + statistics = stats, + claferEnv = env, + mappingToAlloy = [], + stringMap = Map.empty, + scopesList = [] + }) ] + else [] + ) + -- result for Html + ++ (if (Html `elem` modes) + then [ (Html, + CompilerResult { + extension = "html", + outputCode = generateHtml env, + statistics = stats, + claferEnv = env, + mappingToAlloy = [], + stringMap = Map.empty, + scopesList = [] + }) ] + else [] + ) + ++ (if (Graph `elem` modes) + then [ (Graph, + CompilerResult { + extension = "dot", + outputCode = genSimpleGraph ast' iModule (takeBaseName $ file cargs) (show_references cargs), + statistics = stats, + claferEnv = env, + mappingToAlloy = [], + stringMap = Map.empty, + scopesList = [] + }) ] + else [] + ) + ++ (if (CVLGraph `elem` modes) + then [ (CVLGraph, + CompilerResult { + extension = "cvl.dot", + outputCode = genCVLGraph ast' iModule (takeBaseName $ file cargs), + statistics = stats, + claferEnv = env, + mappingToAlloy = [], + stringMap = Map.empty, + scopesList = [] + }) ] + else [] + ) + -- result for Choco + ++ (if (Choco `elem` modes) + then if (hasNoRealLiterals && hasNoReferenceToReal) + then [ (Choco, + CompilerResult { + extension = "js", + outputCode = genCModule (iModule, genv) scopes otherTokens', + statistics = stats, + claferEnv = env, + mappingToAlloy = [], + stringMap = Map.empty, + scopesList = scopes + }) ] + else [ (Choco, + NoCompilerResult { + reason = "Choco output unavailable because the model contains: " + ++ (if hasNoRealLiterals then "" else "a real number literal, ") + ++ (if hasNoReferenceToReal then "" else "a reference to a real, ") + }) + ] + else [] + )) + +-- | Result of generation for a given mode +data CompilerResult + = CompilerResult + { extension :: String -- ^ output file extension + , outputCode :: String -- ^ output text + , statistics :: String -- ^ the final environment of the compiler + , claferEnv :: ClaferEnv -- ^ Maps source constraint spans in Alloy to the spans in the IR + , mappingToAlloy :: [(Span, IrTrace)] -- ^ Map back from Ints used to represent Strings + , stringMap :: (Map.Map Int String) -- ^ scopes generated by scope inference + , scopesList :: [(UID, Integer)] + } + | NoCompilerResult + { reason :: String + } + deriving Show + +liftError :: (Monad m, Language.ClaferT.Throwable t) => Either t a -> ClaferT m a +liftError = either throwErr return + +analyze :: Monad m => ClaferArgs -> IModule -> ClaferT m (IModule, GEnv, Bool) +analyze args' iModule = do + _ <-liftError $ findDupModule args' iModule + let + au = allUnique iModule + let args'' = args'{skip_resolver = au && (skip_resolver args')} + (rTree, genv) <- liftError $ resolveModule args'' iModule + let tTree = transModule rTree + return (optimizeModule args'' (tTree, genv), genv, au) + +addStats :: String -> String -> String +addStats code stats = "/*\n" ++ stats ++ "*/\n" ++ code + +showStats :: Bool -> Stats -> String +showStats au (Stats na nr nc nconst ngoals sgl) = + unlines [ "All clafers: " ++ (show (na + nc)) ++ " | Abstract: " ++ (show na) ++ " | Concrete: " ++ (show nc) ++ " | Reference: " ++ (show nr) + , "Constraints: " ++ show nconst + , "Goals: " ++ show ngoals + , "Global scope: " ++ showInterval sgl + , "Can skip name resolver: " ++ if au then "yes" else "no" ] + +showInterval :: (Integer, Integer) -> String +showInterval (n, -1) = show n ++ "..*" +showInterval (n, m) = show n ++ ".." ++ show m + +gatherObjectivesAndAttributes :: IModule -> Map.Map Span [Ast] -> Maybe ObjectivesAndAttributes +gatherObjectivesAndAttributes iModule astModuleTrace' = let + objectives = (foldl' gatherObjectives [] $ _mDecls iModule) + in if null objectives + then Nothing + else Just $ ObjectivesAndAttributes objectives (map _uid $ filter isIntClafer iClafers) + where + gatherObjectives :: [String] -> IElement -> [String] + gatherObjectives objs (IEGoal _ cpexp') = + printCPexp (Map.lookup (_inPos cpexp') astModuleTrace') + :objs + gatherObjectives objs _ = objs + + printCPexp :: Maybe [Ast] -> String + printCPexp (Just [_,_,(AstGoal g)]) = case g of + GoalMinimize _ [e] -> "min " ++ (printTree e) + GoalMaximize _ [e] -> "max " ++ (printTree e) + GoalMinDeprecated _ [e] -> "min " ++ (printTree e) + GoalMaxDeprecated _ [e] -> "max " ++ (printTree e) + g' -> "[BUG]: unexpected goal found!" ++ show g' + printCPexp e = "[BUG]: expression not found!" ++ show e + + iClafers :: [ IClafer ] + iClafers = universeOn biplate iModule + + isIntClafer (IClafer{_reference=(Just IReference{_ref=pexp'})}) = any (`elem` ["integer", "int"]) $ getRefIds pexp' + isIntClafer _ = False diff --git a/src/Language/Clafer/ClaferArgs.hs b/src/Language/Clafer/ClaferArgs.hs --- a/src/Language/Clafer/ClaferArgs.hs +++ b/src/Language/Clafer/ClaferArgs.hs @@ -36,7 +36,7 @@ import GetURL -- | Type of output to be generated at the end of compilation -data ClaferMode = Alloy | JSON | Clafer | Html | Graph | CVLGraph | Python | Choco +data ClaferMode = Alloy | JSON | Clafer | Html | Graph | CVLGraph | Choco deriving (Eq, Show, Ord, Data, Typeable) instance Default ClaferMode where def = Alloy @@ -74,7 +74,7 @@ clafer :: ClaferArgs clafer = ClaferArgs { - mode = [] &= help "Generated output type. Available CLAFERMODEs are: 'alloy' (default, Alloy 4.2); 'json' (intermediate representation of Clafer model); 'clafer' (analyzed and desugared clafer model); 'html' (original model in HTML); 'graph' (graphical representation written in DOT language); 'cvlgraph' (cvl notation representation written in DOT language); 'python' (generates IR in python); 'choco' (Choco constraint programming solver). Multiple modes can be specified at the same time, e.g., '-m alloy -m html'." &= name "m", + mode = [] &= help "Generated output type. Available CLAFERMODEs are: 'alloy' (default, Alloy 4.2); 'json' (intermediate representation of Clafer model); 'clafer' (analyzed and desugared clafer model); 'html' (original model in HTML); 'graph' (graphical representation written in DOT language); 'cvlgraph' (cvl notation representation written in DOT language); 'choco' (Choco constraint programming solver). Multiple modes can be specified at the same time, e.g., '-m alloy -m html'." &= name "m", console_output = def &= help "Output code on console." &= name "o", flatten_inheritance = def &= help "Flatten inheritance ('alloy' mode only)." &= name "i", timeout_analysis = def &= help "Timeout for analysis.", @@ -84,7 +84,7 @@ skip_resolver = def &= help "Skip name resolution." &= name "f", keep_unused = def &= help "Keep uninstantated abstract clafers ('alloy' mode only)." &= name "k", no_stats = def &= help "Don't print statistics." &= name "s", - validate = def &= help "Validate outputs of all modes. Uses '/alloy4.2.jar' for Alloy models, '/claferchocoig.jar' for Alloy models, and Clafer translator for desugared Clafer models. Use '--tooldir' to override the default location ('.') of these tools." &= name "v", + validate = def &= help "Validate outputs of all modes. Uses '/alloy4.2.jar' for Alloy models, '/chocosolver.jar' for Alloy models, and Clafer translator for desugared Clafer models. Use '--tooldir' to override the default location ('.') of these tools." &= name "v", tooldir = "." &= typDir &= help "Specify the tools directory ('validate' only). Default: '.' (current directory).", alloy_mapping = def &= help "Generate mapping to Alloy source code ('alloy' mode only)." &= name "a", self_contained = def &= help "Generate a self-contained html document ('html' mode only).", diff --git a/src/Language/Clafer/Common.hs b/src/Language/Clafer/Common.hs --- a/src/Language/Clafer/Common.hs +++ b/src/Language/Clafer/Common.hs @@ -1,584 +1,583 @@ -{-# LANGUAGE DeriveDataTypeable, RankNTypes, KindSignatures, FlexibleContexts #-} -{- - Copyright (C) 2012-2015 Kacper Bak, Jimmy Liang, Michal Antkiewicz - - 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. --} -module Language.Clafer.Common where - -import Control.Applicative -import Control.Lens (universeOn) -import Data.Char -import Data.Data.Lens (biplate) -import Data.List -import qualified Data.Map as Map -import Data.Maybe -import Data.StringMap (StringMap) -import qualified Data.StringMap as SMap -import Data.Tree -import Prelude - -import Language.Clafer.Front.AbsClafer -import Language.Clafer.Intermediate.Intclafer - --- ----------------------------------------------------------------------------- --- basic functions shared by desugarer, analyzer and code generator -type Result = String - -transIdent :: PosIdent -> String -transIdent (PosIdent (_, "ref")) = "dref" -transIdent (PosIdent (_, str)) = str - -mkIdent :: String -> PosIdent -mkIdent str = PosIdent ((0, 0), str) - -mkInteger :: Read a => PosInteger -> a -mkInteger (PosInteger (_, n)) = read n - --- | Returns only [] or [_] -getSuper :: IClafer -> [String] -getSuper claf = case getSuperId <$> _super claf of - Nothing -> [] - Just "clafer" -> error "Bug: The identifier 'clafer' should never be returned as super type" - Just x -> [x] - --- | Returns a list of any length -getReference :: IClafer -> [String] -getReference c = case _ref <$> _reference c of - Nothing -> [] - Just ref' -> getRefIds ref' - --- | Returns a list of any length -getSuperAndReference :: IClafer -> [String] -getSuperAndReference c = (getSuper c) ++ (getReference c) - -getSuperId :: PExp -> String -getSuperId (PExp _ _ _ (IClaferId{ _sident = s})) = s -getSuperId (PExp _ _ _ (IFunExp{_op=".", _exps = [_, rightExp]})) = getSuperId rightExp -getSuperId pexp' = error $ "[Bug] Commmon.getSuperId called on unexpected argument '" ++ show pexp' ++ "'" - -getRefIds :: PExp -> [String] -getRefIds (PExp _ _ _ (IClaferId{ _sident = s})) = [s] -getRefIds (PExp _ _ _ (IFunExp{_op=".", _exps = [_, rightExp]})) = getRefIds rightExp -getRefIds (PExp _ _ _ (IFunExp{_op="++", _exps = [leftExp, rightExp]})) = getRefIds leftExp ++ getRefIds rightExp -getRefIds (PExp _ _ _ (IFunExp{_op=",", _exps = [leftExp, rightExp]})) = getRefIds leftExp ++ getRefIds rightExp -getRefIds (PExp _ _ _ (IFunExp{_op="--", _exps = [leftExp, rightExp]})) = getRefIds leftExp ++ getRefIds rightExp -getRefIds (PExp _ _ _ (IFunExp{_op="**", _exps = [leftExp, rightExp]})) = getRefIds leftExp ++ getRefIds rightExp -getRefIds (PExp _ _ _ (IInt _)) = [integerType] -getRefIds (PExp _ _ _ (IDouble _)) = [doubleType] -getRefIds (PExp _ _ _ (IReal _)) = [realType] -getRefIds (PExp _ _ _ (IStr _)) = [stringType] -getRefIds (PExp _ _ _ (IDeclPExp{_quant = ISome})) = [] -getRefIds pexp' = error $ "[Bug] Commmon.getRefIds called on unexpected argument '" ++ show pexp' ++ "'" - -isEqClaferId :: String -> IClafer -> Bool -isEqClaferId uid' claf' = _uid claf' == uid' - -mkPLClaferId :: Span -> CName -> Bool -> ClaferBinding -> PExp -mkPLClaferId pos' id' isTop' bind' = pExpDefPid pos' $ IClaferId "" id' isTop' bind' - -pExpDefPid :: Span -> IExp -> PExp -pExpDefPid = pExpDef "" - -pExpDef :: String -> Span -> IExp -> PExp -pExpDef = PExp Nothing - -isParent :: PExp -> Bool -isParent (PExp _ _ _ (IClaferId _ id' _ _)) = id' == parentIdent -isParent _ = False - -isClaferName :: PExp -> Bool -isClaferName (PExp _ _ _ (IClaferId _ id' _ _)) = - id' `notElem` (specialNames ++ primitiveTypes) -isClaferName _ = False - -isClaferName' :: PExp -> Bool -isClaferName' (PExp _ _ _ (IClaferId _ _ _ _)) = True -isClaferName' _ = False - -getClaferName :: PExp -> String -getClaferName (PExp _ _ _ (IClaferId _ id' _ _)) = id' -getClaferName _ = "" - -isTopLevel :: IClafer -> Bool -isTopLevel IClafer{_parentUID="root"} = True -isTopLevel IClafer{_parentUID="clafer"} = True -isTopLevel _ = False - --- ----------------------------------------------------------------------------- --- conversions -elemToClafer :: IElement -> Maybe IClafer -elemToClafer x = case x of - IEClafer clafer -> Just clafer - _ -> Nothing - -toClafers :: [IElement] -> [IClafer] -toClafers = mapMaybe elemToClafer - - --- ----------------------------------------------------------------------------- --- UID -> IClafer map construction functions - -type UIDIClaferMap = StringMap IClafer - -createUidIClaferMap :: IModule -> UIDIClaferMap -createUidIClaferMap iModule = foldl' - (\accumMap' claf -> SMap.insert (_uid claf) claf accumMap') - (SMap.singleton rootIdent rootClafer) - (integerClafer : intClafer : stringClafer : doubleClafer : realClafer : booleanClafer : clafer : allClafers) - where - allClafers :: [ IClafer ] - allClafers = universeOn biplate iModule - rootClafer = IClafer noSpan False (Just $ IGCard False (0, -1)) rootIdent rootIdent "" Nothing Nothing (Just (1,1)) (1, 1) (_mDecls iModule) - integerClafer = IClafer noSpan False (Just $ IGCard False (0, -1)) integerType integerType "" (Just $ pExpDefPid noSpan $ IClaferId "" doubleType True $ Just doubleType) Nothing (Just (1,1)) (1, 1) [] - intClafer = IClafer noSpan False (Just $ IGCard False (0, -1)) "int" "int" "" (Just $ pExpDefPid noSpan $ IClaferId "" doubleType True $ Just doubleType) Nothing (Just (1,1)) (1, 1) [] - stringClafer = IClafer noSpan False (Just $ IGCard False (0, -1)) stringType stringType "" Nothing Nothing (Just (1,1)) (1, 1) [] - doubleClafer = IClafer noSpan False (Just $ IGCard False (0, -1)) doubleType doubleType "" (Just $ pExpDefPid noSpan $ IClaferId "" realType True $ Just realType) Nothing (Just (1,1)) (1, 1) [] - realClafer = IClafer noSpan False (Just $ IGCard False (0, -1)) realType realType "" Nothing Nothing (Just (1,1)) (1, 1) [] - booleanClafer = IClafer noSpan False (Just $ IGCard False (0, -1)) booleanType booleanType "" Nothing Nothing (Just (1,1)) (1, 1) [] - clafer = IClafer noSpan False (Just $ IGCard False (0, -1)) baseClafer baseClafer "" Nothing Nothing (Just (1,1)) (1, 1) [] - --- ----------------------------------------------------------------------------- --- functions using the UID -> IClafer map - -findIClafer :: UIDIClaferMap -> UID -> Maybe IClafer -findIClafer uidIClaferMap uid' = SMap.lookup uid' uidIClaferMap - -isTopLevelByUID :: UIDIClaferMap -> UID -> Maybe Bool -isTopLevelByUID uidIClaferMap uid' = isTopLevel <$> (findIClafer uidIClaferMap uid') - --- | Finds all super clafers according to sFun -findHierarchy :: (IClafer -> [String]) -> UIDIClaferMap -> IClafer -> [IClafer] -findHierarchy sFun uidIClaferMap clafer = case sFun clafer of - [] -> [clafer] -- no super and no reference - supersOrRefs -> let - superOrRefClafers = mapMaybe (findIClafer uidIClaferMap) supersOrRefs - in - clafer - : concatMap (findHierarchy sFun uidIClaferMap) superOrRefClafers - --- | Finds hierarchy and transforms each element -mapHierarchy :: (IClafer -> b) - -> (IClafer -> [String]) - -> UIDIClaferMap - -> IClafer - -> [b] -mapHierarchy f sf = (map f.).(findHierarchy sf) - --- | traverse the inheritance hierarchy upwards to find a clafer with the given uidToFind -findUIDinSupers :: UIDIClaferMap -> UID -> IClafer -> Maybe IClafer -findUIDinSupers uidIClaferMap uidToFind currentClafer = - if uidToFind == _uid currentClafer - then return currentClafer - else do - superClaferUID <- getSuperId <$> _super currentClafer - superClafer <- findIClafer uidIClaferMap superClaferUID - findUIDinSupers uidIClaferMap uidToFind superClafer - --- | traverse the containment hierarchy upwards to find a clafer with the given uidToFind -findUIDinParents :: UIDIClaferMap -> UID -> IClafer -> Maybe IClafer -findUIDinParents uidIClaferMap uidToFind currentClafer = - if uidToFind == _uid currentClafer - then return currentClafer - else do - parentClafer <- findIClafer uidIClaferMap $ _parentUID currentClafer - findUIDinParents uidIClaferMap uidToFind parentClafer - -data NestedInheritanceMatch - = NestedInheritanceMatch - { _headClafer :: IClafer -- ^ the clafer for which the match is computed - , _parentClafer :: IClafer -- ^ parent of the head clafer - , _parentsSuperClafer :: Maybe IClafer -- ^ parent of the super of the head clafer - , _targetClafer :: [IClafer] -- ^ targets of the head clafer - , _targetsSuperClafer :: [IClafer] -- ^ super of the target of the head clafer - , _superClafer :: IClafer -- ^ super of the head clafer (must exist, otherwise no match) - , _superClafersParent :: IClafer -- ^ parent of the super of the head clafer - , _superClafersTarget :: [IClafer] -- ^ targets of the super of the head clafer - } deriving Show - --- | This represents a match of this shape --- --- superClafersParent --- /\ <> --- ?1| \* --- parentsSuperClafer \ --- /\ [=] superClafer --*-> superClafersTarget --- *| /\ /\ --- parentClafer | |?2 --- <> *| [=] targetsSuperClafer --- *\ | /\ --- \ | *| --- headClafer -----*-----> targetClafer --- --- The clafers are obtained by navigating from the headClafer --- by following the links marked by * --- The link marked by ?1 is checked for correctness of nesting (isProperNesting): --- - _uid parentsSuperClafer == _parentUID superClafer --- - top-level abstract clafers which extend nested abstract clafers are made into siblings of their supers (see https://github.com/gsdlab/clafer/issues/67) --- The link marked by ?2 is checked for correctness of redefinition (isProperRefinement): --- - proper subtyping, bag to set, proper cardinality restriction --- Redefinition occurs when the name of headClafer is the same as the name of superClafer (isProperRedefinition): --- - isProperNesting && isProperRefinement && (_ident headClafer) == (_ident superClafer) - -isProperNesting :: UIDIClaferMap -> Maybe NestedInheritanceMatch -> Bool -isProperNesting _ Nothing = True -isProperNesting uidIClaferMap (Just m) = - if ((isTopLevel $ _superClafer m) && (_isAbstract $ _superClafer m)) - then True - else case (_parentsSuperClafer m) of - Nothing -> (_uid $ _parentClafer m) == (_uid $ _superClafersParent m) - Just parentsSuperClafer -> isJust $ findUIDinSupers uidIClaferMap (_parentUID $ _superClafer m) parentsSuperClafer - --- ^ assumes that isProperNesting m == True -isProperRefinement :: UIDIClaferMap -> Maybe NestedInheritanceMatch - -> (Bool, Bool, Bool) -isProperRefinement _ Nothing - = ( True - , True - , True ) -isProperRefinement uidIClaferMap (Just m) - = ( properCardinalityRefinement m - , properBagToSetRefinement m - , properTargetSubtyping m ) - where - properCardinalityRefinement NestedInheritanceMatch{_headClafer=hc, _superClafer=hcs} - = case (_card hc, _card hcs) of - (Just (hcl, hcu), Just (hcsl, hcsu)) -> hcl >= hcsl && (hcu <= hcsu || hcsu == -1) - _ -> True - properBagToSetRefinement NestedInheritanceMatch{_headClafer=hc, _superClafer=hcs} - = case (_reference hc, _reference hcs) of - (Just IReference{_isSet=headIsSet}, Just IReference{_isSet=superIsSet}) -> superIsSet <= headIsSet -- set (True) implies set (True), bag (False) allows bag (False) or set (True) - _ -> True -- covers 1) only one of them has a ref, and 2) none of them has a ref - properTargetSubtyping NestedInheritanceMatch{_targetClafer=[targetClafer], _superClafersTarget=[superClafersTarget]} - = isJust $ findUIDinSupers uidIClaferMap (_uid superClafersTarget) targetClafer - properTargetSubtyping _ - = True -- covers 1) only one of the target clafers exists, and 2) none of the target clafers exist - --- ^ assumes that isProperNesting m == True and isProperRefinement m == (True, True, True) -isRedefinition :: Maybe NestedInheritanceMatch -> Bool -- ^ whether the name of headClafer is the same as superClafer -isRedefinition Nothing = True -isRedefinition (Just NestedInheritanceMatch{_headClafer=hc, _superClafer=hs}) - = (_ident hc) == (_ident hs) - - - --- ^ try to match the nested inheritance pattern --- ^ only available after the parentUIDs were computed -matchNestedInheritance :: UIDIClaferMap -> IClafer - -> Maybe NestedInheritanceMatch -matchNestedInheritance _ IClafer{_super=Nothing} = Nothing -matchNestedInheritance uidIClaferMap headClafer = do --- traceM $ "matching nested inheritance for " ++ _uid headClafer - parentClafer <- findIClafer uidIClaferMap $ _parentUID headClafer --- traceM $ "matched parentClafer " ++ _uid parentClafer - superClafer <- (findIClafer uidIClaferMap) =<< (getSuperId <$> _super headClafer) --- traceM $ "matched superClafer " ++ _uid superClafer - superClafersParent <- findIClafer uidIClaferMap $ _parentUID superClafer --- traceM $ "matched superClafersParent " ++ _uid superClafersParent - let - parentsSuperClafer :: Maybe IClafer - parentsSuperClafer = findIClafer uidIClaferMap =<< getSuperId <$> _super parentClafer -- safe to use fromJust becuase _super is not isNothing - targetClafer :: [IClafer] - targetClafer = case _ref <$> _reference headClafer of - Just pexp' -> mapMaybe (findIClafer uidIClaferMap) (getRefIds pexp') - Nothing -> [] - targetsSuperClafer :: [IClafer] - targetsSuperClafer = mapMaybe (findIClafer uidIClaferMap) $ map getSuperId $ catMaybes $ map _super targetClafer - superClafersTarget :: [IClafer] - superClafersTarget = case _ref <$> _reference superClafer of - Just pexp' -> mapMaybe (findIClafer uidIClaferMap) (getRefIds pexp') - Nothing -> [] --- traceM $ "matched parentsSuperClafer " ++ show (_uid <$> parentsSuperClafer) --- traceM $ "matched targetClafer " ++ show (_uid <$> targetClafer) --- traceM $ "matched targetsSuperClafer " ++ show (_uid <$> targetsSuperClafer) --- traceM $ "matched superClafersTarget " ++ show (_uid <$> superClafersTarget) - return $ NestedInheritanceMatch - { _headClafer = headClafer - , _parentClafer = parentClafer - , _parentsSuperClafer = parentsSuperClafer - , _superClafer = superClafer - , _superClafersParent = superClafersParent - , _targetClafer = targetClafer - , _targetsSuperClafer = targetsSuperClafer - , _superClafersTarget = superClafersTarget - } - - --- ----------------------------------------------------------------------------- --- generic functions - -apply :: forall t t1. (t -> t1) -> t -> (t, t1) -apply f x = (x, f x) - --- lists all nodes of a tree (BFS). Take a function to extract subforest -bfs :: forall b b1. (b1 -> (b, [b1])) -> [b1] -> [b] -bfs toNode seed = map rootLabel $ concat $ takeWhile (not.null) $ - iterate (concatMap subForest) $ unfoldForest toNode seed - - -toNodeShallow :: IClafer -> (IClafer, [IClafer]) -toNodeShallow = apply (getSubclafers._elements) - - -getSubclafers :: [IElement] -> [IClafer] -getSubclafers = mapMaybe elemToClafer - - -bfsClafers :: [IClafer] -> [IClafer] -bfsClafers clafers = bfs toNodeShallow clafers - -lurry :: forall t t1. ([t1] -> t) -> t1 -> t1 -> t -lurry f x y = f [x,y] - -fst3 :: forall t t1 t2. (t, t1, t2) -> t -fst3 (a, _, _) = a -snd3 :: forall t t1 t2. (t, t1, t2) -> t1 -snd3 (_, b, _) = b -trd3 :: forall t t1 t2. (t, t1, t2) -> t2 -trd3 (_, _, c) = c - - -toTriple :: forall t t1 t2. t -> (t1, t2) -> (t, t1, t2) -toTriple a (b,c) = (a, b, c) - -toMTriple :: forall t t1 t2. t -> (t1, t2) -> Maybe (t, t1, t2) -toMTriple a (b,c) = Just (a, b, c) - --- unary operators -iNot :: String -iNot = "!" - -iCSet :: String -iCSet = "#" - -iMin :: String -iMin = "-" - -iMaximum :: String -iMaximum = "max" - -iMinimum :: String -iMinimum = "min" - -iMaximize :: String -iMaximize = "maximize" - -iMinimize :: String -iMinimize = "minimize" - -iSumSet :: String -iSumSet = "sum" - -iProdSet :: String -iProdSet = "product" - -unOps :: [String] -unOps = [iNot, iCSet, iMin, iMaximum, iMinimum, iMaximize, iMinimize, iSumSet, iProdSet] - --- binary operators -iIff :: String -iIff = "<=>" - -iImpl :: String -iImpl = "=>" - -iOr :: String -iOr = "||" - -iXor :: String -iXor = "xor" - -iAnd :: String -iAnd = "&&" - -logBinOps :: [String] -logBinOps = [iIff, iImpl, iOr, iXor, iAnd] - -iLt :: String -iLt = "<" - -iGt :: String -iGt = ">" - -iEq :: String -iEq = "=" - -iLte :: String -iLte = "<=" - -iGte :: String -iGte = ">=" - -iNeq :: String -iNeq = "!=" - -iIn :: String -iIn = "in" - -iNin :: String -iNin = "not in" - -relGenBinOps :: [String] -relGenBinOps = [iLt, iGt, iEq, iLte, iGte, iNeq] - -relSetBinOps :: [String] -relSetBinOps = [iIn, iNin] - -relBinOps :: [String] -relBinOps = relGenBinOps ++ relSetBinOps - -iPlus :: String -iPlus = "+" - -iSub :: String -iSub = "-" - -iMul :: String -iMul = "*" - -iDiv :: String -iDiv = "/" - -iRem :: String -iRem = "%" - -iSumSet' :: String -iSumSet' = "sum'" - -arithBinOps :: [String] -arithBinOps = [iPlus, iSub, iMul, iDiv, iRem, iSumSet'] - -iUnion :: String -iUnion = "++" - -iDifference :: String -iDifference = "--" - -iIntersection :: String -iIntersection = "**" - -iDomain :: String -iDomain = "<:" - -iRange :: String -iRange = ":>" - -iJoin :: String -iJoin = "." - -setBinOps :: [String] -setBinOps = [iUnion, iDifference, iIntersection, iDomain, iRange, iJoin] - -binOps :: [String] -binOps = logBinOps ++ relBinOps ++ arithBinOps ++ setBinOps - --- ternary operators -iIfThenElse :: String -iIfThenElse = "ifthenelse" - -mkIFunExp :: Span -> String -> [IExp] -> IExp -mkIFunExp _ _ (x:[]) = x -mkIFunExp pos' op' xs = foldl1 (\x y -> IFunExp op' $ map (PExp Nothing "" pos') [x,y]) xs - -toLowerS :: String -> String -toLowerS "" = "" -toLowerS (s:ss) = toLower s : ss - --- ----------------------------------------------------------------------------- --- Constants - -rootIdent :: String -rootIdent = "root" - -rootUID :: String -rootUID = "root" - -thisIdent :: String -thisIdent = "this" - -parentIdent :: String -parentIdent = "parent" - -drefIdent :: String -drefIdent = "dref" - -childrenIdent :: String -childrenIdent = "children" - -specialNames :: [String] -specialNames = [thisIdent, parentIdent, drefIdent, rootIdent, childrenIdent] - -isSpecial :: String -> Bool -isSpecial = flip elem specialNames - -stringType :: String -stringType = "string" - -intType :: String -intType = "int" - -integerType :: String -integerType = "integer" - -realType :: String -realType = "real" - -doubleType :: String -doubleType = "double" - -booleanType :: String -booleanType = "boolean" - -baseClafer :: String -baseClafer = "clafer" - -modSep :: String -modSep = "\\" - -primitiveTypes :: [String] -primitiveTypes = [stringType, intType, integerType, doubleType, realType] - -isPrimitive :: String -> Bool -isPrimitive = flip elem primitiveTypes - --- | reserved keywords which cannot be used as clafer identifiers -keywordIdents :: [String] -keywordIdents = - baseClafer : - specialNames ++ - primitiveTypes ++ - [ iMaximum, iMinimum, iMaximize, iMinimize, iSumSet, iProdSet ] ++ -- unary operators - [ iXor, iIn ] ++ -- binary operators - [ "if", "then", "else" ] ++ -- ternary operators - [ "no", "not", "some", "one", "all", "disj" ] ++ -- quantifiers - [ "opt", "mux", "or", "lone" ] ++ -- group cardinalities - [ "abstract", "enum" ] -- keywords - -data GEnv - = GEnv - { identCountMap :: Map.Map String Int - , expCount :: Int - , stable :: Map.Map UID [[UID]] -- super clafer names of a given clafer - , sClafers ::[IClafer] -- all clafers (no going through references) - , uidClaferMap :: UIDIClaferMap -- the map needs to be re-created everytime IModule is rewritten - } deriving (Eq, Show) - -safeTail :: [a] -> [a] -safeTail [] = [] -safeTail (_:xs) = xs +{-# LANGUAGE DeriveDataTypeable, RankNTypes, KindSignatures, FlexibleContexts #-} +{- + Copyright (C) 2012-2015 Kacper Bak, Jimmy Liang, Michal Antkiewicz + + 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. +-} +module Language.Clafer.Common where + +import Control.Applicative +import Control.Lens (universeOn) +import Data.Char +import Data.Data.Lens (biplate) +import Data.List +import qualified Data.Map as Map +import Data.Maybe +import Data.StringMap (StringMap) +import qualified Data.StringMap as SMap +import Data.Tree +import Prelude + +import Language.Clafer.Front.AbsClafer +import Language.Clafer.Intermediate.Intclafer + +-- ----------------------------------------------------------------------------- +-- basic functions shared by desugarer, analyzer and code generator +type Result = String + +transIdent :: PosIdent -> String +transIdent (PosIdent (_, "ref")) = "dref" +transIdent (PosIdent (_, str)) = str + +mkIdent :: String -> PosIdent +mkIdent str = PosIdent ((0, 0), str) + +mkInteger :: Read a => PosInteger -> a +mkInteger (PosInteger (_, n)) = read n + +-- | Returns only [] or [_] +getSuper :: IClafer -> [String] +getSuper claf = case getSuperId <$> _super claf of + Nothing -> [] + Just "clafer" -> error "Bug: The identifier 'clafer' should never be returned as super type" + Just x -> [x] + +-- | Returns a list of any length +getReference :: IClafer -> [String] +getReference c = case _ref <$> _reference c of + Nothing -> [] + Just ref' -> getRefIds ref' + +-- | Returns a list of any length +getSuperAndReference :: IClafer -> [String] +getSuperAndReference c = (getSuper c) ++ (getReference c) + +getSuperId :: PExp -> String +getSuperId (PExp _ _ _ (IClaferId{ _sident = s})) = s +getSuperId (PExp _ _ _ (IFunExp{_op=".", _exps = [_, rightExp]})) = getSuperId rightExp +getSuperId pexp' = error $ "[Bug] Commmon.getSuperId called on unexpected argument '" ++ show pexp' ++ "'" + +getRefIds :: PExp -> [String] +getRefIds (PExp _ _ _ (IClaferId{ _sident = s})) = [s] +getRefIds (PExp _ _ _ (IFunExp{_op=".", _exps = [_, rightExp]})) = getRefIds rightExp +getRefIds (PExp _ _ _ (IFunExp{_op="++", _exps = [leftExp, rightExp]})) = getRefIds leftExp ++ getRefIds rightExp +getRefIds (PExp _ _ _ (IFunExp{_op=",", _exps = [leftExp, rightExp]})) = getRefIds leftExp ++ getRefIds rightExp +getRefIds (PExp _ _ _ (IFunExp{_op="--", _exps = [leftExp, rightExp]})) = getRefIds leftExp ++ getRefIds rightExp +getRefIds (PExp _ _ _ (IFunExp{_op="**", _exps = [leftExp, rightExp]})) = getRefIds leftExp ++ getRefIds rightExp +getRefIds (PExp _ _ _ (IInt _)) = [integerType] +getRefIds (PExp _ _ _ (IDouble _)) = [doubleType] +getRefIds (PExp _ _ _ (IReal _)) = [realType] +getRefIds (PExp _ _ _ (IStr _)) = [stringType] +getRefIds (PExp _ _ _ (IDeclPExp{_quant = ISome})) = [] +getRefIds pexp' = error $ "[Bug] Commmon.getRefIds called on unexpected argument '" ++ show pexp' ++ "'" + +isEqClaferId :: String -> IClafer -> Bool +isEqClaferId uid' claf' = _uid claf' == uid' + +mkPLClaferId :: Span -> CName -> Bool -> ClaferBinding -> PExp +mkPLClaferId pos' id' isTop' bind' = pExpDefPid pos' $ IClaferId "" id' isTop' bind' + +pExpDefPid :: Span -> IExp -> PExp +pExpDefPid = pExpDef "" + +pExpDef :: String -> Span -> IExp -> PExp +pExpDef = PExp Nothing + +isParent :: PExp -> Bool +isParent (PExp _ _ _ (IClaferId _ id' _ _)) = id' == parentIdent +isParent _ = False + +isClaferName :: PExp -> Bool +isClaferName (PExp _ _ _ (IClaferId _ id' _ _)) = + id' `notElem` (specialNames ++ primitiveTypes) +isClaferName _ = False + +isClaferName' :: PExp -> Bool +isClaferName' (PExp _ _ _ (IClaferId _ _ _ _)) = True +isClaferName' _ = False + +getClaferName :: PExp -> String +getClaferName (PExp _ _ _ (IClaferId _ id' _ _)) = id' +getClaferName _ = "" + +isTopLevel :: IClafer -> Bool +isTopLevel IClafer{_parentUID="root"} = True +isTopLevel IClafer{_parentUID="clafer"} = True +isTopLevel _ = False + +-- ----------------------------------------------------------------------------- +-- conversions +elemToClafer :: IElement -> Maybe IClafer +elemToClafer x = case x of + IEClafer clafer -> Just clafer + _ -> Nothing + +toClafers :: [IElement] -> [IClafer] +toClafers = mapMaybe elemToClafer + + +-- ----------------------------------------------------------------------------- +-- UID -> IClafer map construction functions + +type UIDIClaferMap = StringMap IClafer + +createUidIClaferMap :: IModule -> UIDIClaferMap +createUidIClaferMap iModule = foldl' + (\accumMap' claf -> SMap.insert (_uid claf) claf accumMap') + (SMap.singleton rootIdent rootClafer) + (integerClafer : intClafer : stringClafer : doubleClafer : realClafer : booleanClafer : clafer : allClafers) + where + allClafers :: [ IClafer ] + allClafers = universeOn biplate iModule + rootClafer = IClafer noSpan False (Just $ IGCard False (0, -1)) rootIdent rootIdent "" Nothing Nothing (Just (1,1)) (1, 1) (_mDecls iModule) + integerClafer = IClafer noSpan False (Just $ IGCard False (0, -1)) integerType integerType "" (Just $ pExpDefPid noSpan $ IClaferId "" doubleType True $ Just doubleType) Nothing (Just (1,1)) (1, 1) [] + intClafer = IClafer noSpan False (Just $ IGCard False (0, -1)) "int" "int" "" (Just $ pExpDefPid noSpan $ IClaferId "" doubleType True $ Just doubleType) Nothing (Just (1,1)) (1, 1) [] + stringClafer = IClafer noSpan False (Just $ IGCard False (0, -1)) stringType stringType "" Nothing Nothing (Just (1,1)) (1, 1) [] + doubleClafer = IClafer noSpan False (Just $ IGCard False (0, -1)) doubleType doubleType "" (Just $ pExpDefPid noSpan $ IClaferId "" realType True $ Just realType) Nothing (Just (1,1)) (1, 1) [] + realClafer = IClafer noSpan False (Just $ IGCard False (0, -1)) realType realType "" Nothing Nothing (Just (1,1)) (1, 1) [] + booleanClafer = IClafer noSpan False (Just $ IGCard False (0, -1)) booleanType booleanType "" Nothing Nothing (Just (1,1)) (1, 1) [] + clafer = IClafer noSpan False (Just $ IGCard False (0, -1)) baseClafer baseClafer "" Nothing Nothing (Just (1,1)) (1, 1) [] + +-- ----------------------------------------------------------------------------- +-- functions using the UID -> IClafer map + +findIClafer :: UIDIClaferMap -> UID -> Maybe IClafer +findIClafer uidIClaferMap uid' = SMap.lookup uid' uidIClaferMap + +isTopLevelByUID :: UIDIClaferMap -> UID -> Maybe Bool +isTopLevelByUID uidIClaferMap uid' = isTopLevel <$> (findIClafer uidIClaferMap uid') + +-- | Finds all super clafers according to sFun +findHierarchy :: (IClafer -> [String]) -> UIDIClaferMap -> IClafer -> [IClafer] +findHierarchy sFun uidIClaferMap clafer = case sFun clafer of + [] -> [clafer] -- no super and no reference + supersOrRefs -> let + superOrRefClafers = mapMaybe (findIClafer uidIClaferMap) supersOrRefs + in + clafer + : concatMap (findHierarchy sFun uidIClaferMap) superOrRefClafers + +-- | Finds hierarchy and transforms each element +mapHierarchy :: (IClafer -> b) + -> (IClafer -> [String]) + -> UIDIClaferMap + -> IClafer + -> [b] +mapHierarchy f sf = (map f.).(findHierarchy sf) + +-- | traverse the inheritance hierarchy upwards to find a clafer with the given uidToFind +findUIDinSupers :: UIDIClaferMap -> UID -> IClafer -> Maybe IClafer +findUIDinSupers uidIClaferMap uidToFind currentClafer = + if uidToFind == _uid currentClafer + then return currentClafer + else do + superClaferUID <- getSuperId <$> _super currentClafer + superClafer <- findIClafer uidIClaferMap superClaferUID + findUIDinSupers uidIClaferMap uidToFind superClafer + +-- | traverse the containment hierarchy upwards to find a clafer with the given uidToFind +findUIDinParents :: UIDIClaferMap -> UID -> IClafer -> Maybe IClafer +findUIDinParents uidIClaferMap uidToFind currentClafer = + if uidToFind == _uid currentClafer + then return currentClafer + else do + parentClafer <- findIClafer uidIClaferMap $ _parentUID currentClafer + findUIDinParents uidIClaferMap uidToFind parentClafer + +data NestedInheritanceMatch + = NestedInheritanceMatch + { _headClafer :: IClafer -- ^ the clafer for which the match is computed + , _parentClafer :: IClafer -- ^ parent of the head clafer + , _parentsSuperClafer :: Maybe IClafer -- ^ parent of the super of the head clafer + , _targetClafer :: [IClafer] -- ^ targets of the head clafer + , _targetsSuperClafer :: [IClafer] -- ^ super of the target of the head clafer + , _superClafer :: IClafer -- ^ super of the head clafer (must exist, otherwise no match) + , _superClafersParent :: IClafer -- ^ parent of the super of the head clafer + , _superClafersTarget :: [IClafer] -- ^ targets of the super of the head clafer + } deriving Show + +-- | This represents a match of this shape +-- +-- superClafersParent +-- /\ <> +-- ?1| \* +-- parentsSuperClafer \ +-- /\ [=] superClafer --*-> superClafersTarget +-- *| /\ /\ +-- parentClafer | |?2 +-- <> *| [=] targetsSuperClafer +-- *\ | /\ +-- \ | *| +-- headClafer -----*-----> targetClafer +-- +-- The clafers are obtained by navigating from the headClafer +-- by following the links marked by * +-- The link marked by ?1 is checked for correctness of nesting (isProperNesting): +-- - _uid parentsSuperClafer == _parentUID superClafer +-- - top-level abstract clafers which extend nested abstract clafers are made into siblings of their supers (see https://github.com/gsdlab/clafer/issues/67) +-- The link marked by ?2 is checked for correctness of redefinition (isProperRefinement): +-- - proper subtyping, bag to set, proper cardinality restriction +-- Redefinition occurs when the name of headClafer is the same as the name of superClafer (isProperRedefinition): +-- - isProperNesting && isProperRefinement && (_ident headClafer) == (_ident superClafer) + +isProperNesting :: UIDIClaferMap -> Maybe NestedInheritanceMatch -> Bool +isProperNesting _ Nothing = True +isProperNesting uidIClaferMap (Just m) = + (isTopLevel (_superClafer m) && _isAbstract (_superClafer m)) + || + (_parentUID (_headClafer m) == _parentUID (_superClafer m)) + || + (case _parentsSuperClafer m of + Nothing -> _uid (_parentClafer m) == _uid (_superClafersParent m) + Just parentsSuperClafer -> isJust $ findUIDinSupers uidIClaferMap (_parentUID $ _superClafer m) parentsSuperClafer + ) +-- ^ assumes that isProperNesting m == True +isProperRefinement :: UIDIClaferMap -> Maybe NestedInheritanceMatch + -> (Bool, Bool, Bool) +isProperRefinement _ Nothing + = ( True + , True + , True ) +isProperRefinement uidIClaferMap (Just m) + = ( properCardinalityRefinement m + , properBagToSetRefinement m + , properTargetSubtyping m ) + where + properCardinalityRefinement NestedInheritanceMatch{_headClafer=hc, _superClafer=hcs} + = case (_card hc, _card hcs) of + (Just (hcl, hcu), Just (hcsl, hcsu)) -> hcl >= hcsl && (hcu <= hcsu || hcsu == -1) + _ -> True + properBagToSetRefinement NestedInheritanceMatch{_headClafer=hc, _superClafer=hcs} + = case (_reference hc, _reference hcs) of + (Just IReference{_isSet=headIsSet}, Just IReference{_isSet=superIsSet}) -> superIsSet <= headIsSet -- set (True) implies set (True), bag (False) allows bag (False) or set (True) + _ -> True -- covers 1) only one of them has a ref, and 2) none of them has a ref + properTargetSubtyping NestedInheritanceMatch{_targetClafer=[targetClafer], _superClafersTarget=[superClafersTarget]} + = isJust $ findUIDinSupers uidIClaferMap (_uid superClafersTarget) targetClafer + properTargetSubtyping _ + = True -- covers 1) only one of the target clafers exists, and 2) none of the target clafers exist + +-- ^ assumes that isProperNesting m == True and isProperRefinement m == (True, True, True) +isRedefinition :: Maybe NestedInheritanceMatch -> Bool -- ^ whether the name of headClafer is the same as superClafer +isRedefinition Nothing = True +isRedefinition (Just NestedInheritanceMatch{_headClafer=hc, _superClafer=hs}) + = (_ident hc) == (_ident hs) + + + +-- ^ try to match the nested inheritance pattern +-- ^ only available after the parentUIDs were computed +matchNestedInheritance :: UIDIClaferMap -> IClafer + -> Maybe NestedInheritanceMatch +matchNestedInheritance _ IClafer{_super=Nothing} = Nothing +matchNestedInheritance uidIClaferMap headClafer = do +-- traceM $ "matching nested inheritance for " ++ _uid headClafer + parentClafer <- findIClafer uidIClaferMap $ _parentUID headClafer +-- traceM $ "matched parentClafer " ++ _uid parentClafer + superClafer <- (findIClafer uidIClaferMap) =<< (getSuperId <$> _super headClafer) +-- traceM $ "matched superClafer " ++ _uid superClafer + superClafersParent <- findIClafer uidIClaferMap $ _parentUID superClafer +-- traceM $ "matched superClafersParent " ++ _uid superClafersParent + let + parentsSuperClafer :: Maybe IClafer + parentsSuperClafer = findIClafer uidIClaferMap =<< getSuperId <$> _super parentClafer -- safe to use fromJust becuase _super is not isNothing + targetClafer :: [IClafer] + targetClafer = case _ref <$> _reference headClafer of + Just pexp' -> mapMaybe (findIClafer uidIClaferMap) (getRefIds pexp') + Nothing -> [] + targetsSuperClafer :: [IClafer] + targetsSuperClafer = mapMaybe (findIClafer uidIClaferMap) $ map getSuperId $ catMaybes $ map _super targetClafer + superClafersTarget :: [IClafer] + superClafersTarget = case _ref <$> _reference superClafer of + Just pexp' -> mapMaybe (findIClafer uidIClaferMap) (getRefIds pexp') + Nothing -> [] +-- traceM $ "matched parentsSuperClafer " ++ show (_uid <$> parentsSuperClafer) +-- traceM $ "matched targetClafer " ++ show (_uid <$> targetClafer) +-- traceM $ "matched targetsSuperClafer " ++ show (_uid <$> targetsSuperClafer) +-- traceM $ "matched superClafersTarget " ++ show (_uid <$> superClafersTarget) + return $ NestedInheritanceMatch + { _headClafer = headClafer + , _parentClafer = parentClafer + , _parentsSuperClafer = parentsSuperClafer + , _superClafer = superClafer + , _superClafersParent = superClafersParent + , _targetClafer = targetClafer + , _targetsSuperClafer = targetsSuperClafer + , _superClafersTarget = superClafersTarget + } + + +-- ----------------------------------------------------------------------------- +-- generic functions + +apply :: forall t t1. (t -> t1) -> t -> (t, t1) +apply f x = (x, f x) + +-- lists all nodes of a tree (BFS). Take a function to extract subforest +bfs :: forall b b1. (b1 -> (b, [b1])) -> [b1] -> [b] +bfs toNode seed = map rootLabel $ concat $ takeWhile (not.null) $ + iterate (concatMap subForest) $ unfoldForest toNode seed + + +toNodeShallow :: IClafer -> (IClafer, [IClafer]) +toNodeShallow = apply (getSubclafers._elements) + + +getSubclafers :: [IElement] -> [IClafer] +getSubclafers = mapMaybe elemToClafer + + +bfsClafers :: [IClafer] -> [IClafer] +bfsClafers clafers = bfs toNodeShallow clafers + +lurry :: forall t t1. ([t1] -> t) -> t1 -> t1 -> t +lurry f x y = f [x,y] + +fst3 :: forall t t1 t2. (t, t1, t2) -> t +fst3 (a, _, _) = a +snd3 :: forall t t1 t2. (t, t1, t2) -> t1 +snd3 (_, b, _) = b +trd3 :: forall t t1 t2. (t, t1, t2) -> t2 +trd3 (_, _, c) = c + + +toTriple :: forall t t1 t2. t -> (t1, t2) -> (t, t1, t2) +toTriple a (b,c) = (a, b, c) + +toMTriple :: forall t t1 t2. t -> (t1, t2) -> Maybe (t, t1, t2) +toMTriple a (b,c) = Just (a, b, c) + +-- unary operators +iNot :: String +iNot = "!" + +iCSet :: String +iCSet = "#" + +iMin :: String +iMin = "-" + +iMaximum :: String +iMaximum = "max" + +iMinimum :: String +iMinimum = "min" + +iMaximize :: String +iMaximize = "maximize" + +iMinimize :: String +iMinimize = "minimize" + +iSumSet :: String +iSumSet = "sum" + +iProdSet :: String +iProdSet = "product" + +unOps :: [String] +unOps = [iNot, iCSet, iMin, iMaximum, iMinimum, iMaximize, iMinimize, iSumSet, iProdSet] + +-- binary operators +iIff :: String +iIff = "<=>" + +iImpl :: String +iImpl = "=>" + +iOr :: String +iOr = "||" + +iXor :: String +iXor = "xor" + +iAnd :: String +iAnd = "&&" + +logBinOps :: [String] +logBinOps = [iIff, iImpl, iOr, iXor, iAnd] + +iLt :: String +iLt = "<" + +iGt :: String +iGt = ">" + +iEq :: String +iEq = "=" + +iLte :: String +iLte = "<=" + +iGte :: String +iGte = ">=" + +iNeq :: String +iNeq = "!=" + +iIn :: String +iIn = "in" + +iNin :: String +iNin = "not in" + +relGenBinOps :: [String] +relGenBinOps = [iLt, iGt, iEq, iLte, iGte, iNeq] + +relSetBinOps :: [String] +relSetBinOps = [iIn, iNin] + +relBinOps :: [String] +relBinOps = relGenBinOps ++ relSetBinOps + +iPlus :: String +iPlus = "+" + +iSub :: String +iSub = "-" + +iMul :: String +iMul = "*" + +iDiv :: String +iDiv = "/" + +iRem :: String +iRem = "%" + +arithBinOps :: [String] +arithBinOps = [iPlus, iSub, iMul, iDiv, iRem] + +iUnion :: String +iUnion = "++" + +iDifference :: String +iDifference = "--" + +iIntersection :: String +iIntersection = "**" + +iDomain :: String +iDomain = "<:" + +iRange :: String +iRange = ":>" + +iJoin :: String +iJoin = "." + +setBinOps :: [String] +setBinOps = [iUnion, iDifference, iIntersection, iDomain, iRange, iJoin] + +binOps :: [String] +binOps = logBinOps ++ relBinOps ++ arithBinOps ++ setBinOps + +-- ternary operators +iIfThenElse :: String +iIfThenElse = "ifthenelse" + +mkIFunExp :: Span -> String -> [IExp] -> IExp +mkIFunExp _ _ (x:[]) = x +mkIFunExp pos' op' xs = foldl1 (\x y -> IFunExp op' $ map (PExp Nothing "" pos') [x,y]) xs + +toLowerS :: String -> String +toLowerS "" = "" +toLowerS (s:ss) = toLower s : ss + +-- ----------------------------------------------------------------------------- +-- Constants + +rootIdent :: String +rootIdent = "root" + +rootUID :: String +rootUID = "root" + +thisIdent :: String +thisIdent = "this" + +parentIdent :: String +parentIdent = "parent" + +drefIdent :: String +drefIdent = "dref" + +childrenIdent :: String +childrenIdent = "children" + +specialNames :: [String] +specialNames = [thisIdent, parentIdent, drefIdent, rootIdent, childrenIdent] + +isSpecial :: String -> Bool +isSpecial = flip elem specialNames + +stringType :: String +stringType = "string" + +intType :: String +intType = "int" + +integerType :: String +integerType = "integer" + +realType :: String +realType = "real" + +doubleType :: String +doubleType = "double" + +booleanType :: String +booleanType = "boolean" + +baseClafer :: String +baseClafer = "clafer" + +modSep :: String +modSep = "\\" + +primitiveTypes :: [String] +primitiveTypes = [stringType, intType, integerType, doubleType, realType] + +isPrimitive :: String -> Bool +isPrimitive = flip elem primitiveTypes + +-- | reserved keywords which cannot be used as clafer identifiers +keywordIdents :: [String] +keywordIdents = + baseClafer : + specialNames ++ + primitiveTypes ++ + [ iMaximum, iMinimum, iMaximize, iMinimize, iSumSet, iProdSet ] ++ -- unary operators + [ iXor, iIn ] ++ -- binary operators + [ "if", "then", "else" ] ++ -- ternary operators + [ "no", "not", "some", "one", "all", "disj" ] ++ -- quantifiers + [ "opt", "mux", "or", "lone" ] ++ -- group cardinalities + [ "abstract", "enum" ] -- keywords + +data GEnv + = GEnv + { identCountMap :: Map.Map String Int + , expCount :: Int + , stable :: Map.Map UID [[UID]] -- super clafer names of a given clafer + , sClafers ::[IClafer] -- all clafers (no going through references) + , uidClaferMap :: UIDIClaferMap -- the map needs to be re-created everytime IModule is rewritten + } deriving (Eq, Show) + +safeTail :: [a] -> [a] +safeTail [] = [] +safeTail (_:xs) = xs diff --git a/src/Language/Clafer/Front/LexClafer.x b/src/Language/Clafer/Front/LexClafer.x --- a/src/Language/Clafer/Front/LexClafer.x +++ b/src/Language/Clafer/Front/LexClafer.x @@ -1,206 +1,206 @@ --- -*- haskell -*- --- This Alex file was machine-generated by the BNF converter -{ -{-# OPTIONS -fno-warn-incomplete-patterns #-} -{-# OPTIONS_GHC -w #-} -module Language.Clafer.Front.LexClafer where - - - -import qualified Data.Bits -import Data.Word (Word8) -} - - -$l = [a-zA-Z\192 - \255] # [\215 \247] -- isolatin1 letter FIXME -$c = [A-Z\192-\221] # [\215] -- capital isolatin1 letter FIXME -$s = [a-z\222-\255] # [\247] -- small isolatin1 letter FIXME -$d = [0-9] -- digit -$i = [$l $d _ '] -- identifier character -$u = [\0-\255] -- universal: any character - -@rsyms = -- symbols and non-identifier-like reserved words - \= | \[ | \] | \< \< | \> \> | \{ | \} | \` | \: | \- \> | \- \> \> | \: \= | \? | \+ | \* | \. \. | \| | \< \= \> | \= \> | \| \| | \& \& | \! | \< | \> | \< \= | \> \= | \! \= | \- | \/ | \% | \# | \< \: | \: \> | \+ \+ | \, | \- \- | \* \* | \& | \. | \; | \\ | \( | \) - -:- - -$white+ ; -@rsyms { tok (\p s -> PT p (eitherResIdent (TV . share) s)) } -$d + { tok (\p s -> PT p (eitherResIdent (T_PosInteger . share) s)) } -$d + \. $d + e \- ? $d + { tok (\p s -> PT p (eitherResIdent (T_PosDouble . share) s)) } -$d + \. $d + { tok (\p s -> PT p (eitherResIdent (T_PosReal . share) s)) } -\" ($u # [\" \\]| \\ [\" \\ n t]) * \" { tok (\p s -> PT p (eitherResIdent (T_PosString . share) s)) } -$l ($l | $d | \_ | \')* { tok (\p s -> PT p (eitherResIdent (T_PosIdent . share) s)) } -\/ \/ ($u # \n)* { tok (\p s -> PT p (eitherResIdent (T_PosLineComment . share) s)) } -\/ \* ($u # \* | \* + ($u # [\* \/]))* \* + \/ { tok (\p s -> PT p (eitherResIdent (T_PosBlockComment . share) s)) } -\[ a l l o y \| ($u # \| | \| + ($u # \])) * (\| \]) { tok (\p s -> PT p (eitherResIdent (T_PosAlloy . share) s)) } -\[ c h o c o \| ($u # \| | \| + ($u # \])) * (\| \]) { tok (\p s -> PT p (eitherResIdent (T_PosChoco . share) s)) } - -$l $i* { tok (\p s -> PT p (eitherResIdent (TV . share) s)) } - - - - - -{ - -tok :: (Posn -> String -> Token) -> (Posn -> String -> Token) -tok f p s = f p s - -share :: String -> String -share = id - -data Tok = - TS !String !Int -- reserved words and symbols - | TL !String -- string literals - | TI !String -- integer literals - | TV !String -- identifiers - | TD !String -- double precision float literals - | TC !String -- character literals - | T_PosInteger !String - | T_PosDouble !String - | T_PosReal !String - | T_PosString !String - | T_PosIdent !String - | T_PosLineComment !String - | T_PosBlockComment !String - | T_PosAlloy !String - | T_PosChoco !String - - deriving (Eq,Show,Ord) - -data Token = - PT Posn Tok - | Err Posn - deriving (Eq,Show,Ord) - -tokenPos :: [Token] -> String -tokenPos (PT (Pn _ l _) _ :_) = "line " ++ show l -tokenPos (Err (Pn _ l _) :_) = "line " ++ show l -tokenPos _ = "end of file" - -tokenPosn :: Token -> Posn -tokenPosn (PT p _) = p -tokenPosn (Err p) = p - -tokenLineCol :: Token -> (Int, Int) -tokenLineCol = posLineCol . tokenPosn - -posLineCol :: Posn -> (Int, Int) -posLineCol (Pn _ l c) = (l,c) - -mkPosToken :: Token -> ((Int, Int), String) -mkPosToken t@(PT p _) = (posLineCol p, prToken t) - -prToken :: Token -> String -prToken t = case t of - PT _ (TS s _) -> s - PT _ (TL s) -> show s - PT _ (TI s) -> s - PT _ (TV s) -> s - PT _ (TD s) -> s - PT _ (TC s) -> s - PT _ (T_PosInteger s) -> s - PT _ (T_PosDouble s) -> s - PT _ (T_PosReal s) -> s - PT _ (T_PosString s) -> s - PT _ (T_PosIdent s) -> s - PT _ (T_PosLineComment s) -> s - PT _ (T_PosBlockComment s) -> s - PT _ (T_PosAlloy s) -> s - PT _ (T_PosChoco s) -> s - - -data BTree = N | B String Tok BTree BTree deriving (Show) - -eitherResIdent :: (String -> Tok) -> String -> Tok -eitherResIdent tv s = treeFind resWords - where - treeFind N = tv s - treeFind (B a t left right) | s < a = treeFind left - | s > a = treeFind right - | s == a = t - -resWords :: BTree -resWords = b ">>" 34 (b "->>" 17 (b "*" 9 (b "&" 5 (b "#" 3 (b "!=" 2 (b "!" 1 N N) N) (b "%" 4 N N)) (b "(" 7 (b "&&" 6 N N) (b ")" 8 N N))) (b "," 13 (b "+" 11 (b "**" 10 N N) (b "++" 12 N N)) (b "--" 15 (b "-" 14 N N) (b "->" 16 N N)))) (b "<:" 26 (b ":=" 22 (b "/" 20 (b ".." 19 (b "." 18 N N) N) (b ":" 21 N N)) (b ";" 24 (b ":>" 23 N N) (b "<" 25 N N))) (b "=" 30 (b "<=" 28 (b "<<" 27 N N) (b "<=>" 29 N N)) (b ">" 32 (b "=>" 31 N N) (b ">=" 33 N N))))) (b "min" 51 (b "disj" 43 (b "`" 39 (b "\\" 37 (b "[" 36 (b "?" 35 N N) N) (b "]" 38 N N)) (b "all" 41 (b "abstract" 40 N N) (b "assert" 42 N N))) (b "in" 47 (b "enum" 45 (b "else" 44 N N) (b "if" 46 N N)) (b "max" 49 (b "lone" 48 N N) (b "maximize" 50 N N)))) (b "some" 60 (b "one" 56 (b "no" 54 (b "mux" 53 (b "minimize" 52 N N) N) (b "not" 55 N N)) (b "or" 58 (b "opt" 57 N N) (b "product" 59 N N))) (b "{" 64 (b "then" 62 (b "sum" 61 N N) (b "xor" 63 N N)) (b "||" 66 (b "|" 65 N N) (b "}" 67 N N))))) - where b s n = let bs = id s - in B bs (TS bs n) - -unescapeInitTail :: String -> String -unescapeInitTail = id . unesc . tail . id where - unesc s = case s of - '\\':c:cs | elem c ['\"', '\\', '\''] -> c : unesc cs - '\\':'n':cs -> '\n' : unesc cs - '\\':'t':cs -> '\t' : unesc cs - '"':[] -> [] - c:cs -> c : unesc cs - _ -> [] - -------------------------------------------------------------------- --- Alex wrapper code. --- A modified "posn" wrapper. -------------------------------------------------------------------- - -data Posn = Pn !Int !Int !Int - deriving (Eq, Show,Ord) - -alexStartPos :: Posn -alexStartPos = Pn 0 1 1 - -alexMove :: Posn -> Char -> Posn -alexMove (Pn a l c) '\t' = Pn (a+1) l (((c+7) `div` 8)*8+1) -alexMove (Pn a l c) '\n' = Pn (a+1) (l+1) 1 -alexMove (Pn a l c) _ = Pn (a+1) l (c+1) - -type Byte = Word8 - -type AlexInput = (Posn, -- current position, - Char, -- previous char - [Byte], -- pending bytes on the current char - String) -- current input string - -tokens :: String -> [Token] -tokens str = go (alexStartPos, '\n', [], str) - where - go :: AlexInput -> [Token] - go inp@(pos, _, _, str) = - case alexScan inp 0 of - AlexEOF -> [] - AlexError (pos, _, _, _) -> [Err pos] - AlexSkip inp' len -> go inp' - AlexToken inp' len act -> act pos (take len str) : (go inp') - -alexGetByte :: AlexInput -> Maybe (Byte,AlexInput) -alexGetByte (p, c, (b:bs), s) = Just (b, (p, c, bs, s)) -alexGetByte (p, _, [], s) = - case s of - [] -> Nothing - (c:s) -> - let p' = alexMove p c - (b:bs) = utf8Encode c - in p' `seq` Just (b, (p', c, bs, s)) - -alexInputPrevChar :: AlexInput -> Char -alexInputPrevChar (p, c, bs, s) = c - --- | Encode a Haskell String to a list of Word8 values, in UTF8 format. -utf8Encode :: Char -> [Word8] -utf8Encode = map fromIntegral . go . ord - where - go oc - | oc <= 0x7f = [oc] - - | oc <= 0x7ff = [ 0xc0 + (oc `Data.Bits.shiftR` 6) - , 0x80 + oc Data.Bits..&. 0x3f - ] - - | oc <= 0xffff = [ 0xe0 + (oc `Data.Bits.shiftR` 12) - , 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f) - , 0x80 + oc Data.Bits..&. 0x3f - ] - | otherwise = [ 0xf0 + (oc `Data.Bits.shiftR` 18) - , 0x80 + ((oc `Data.Bits.shiftR` 12) Data.Bits..&. 0x3f) - , 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f) - , 0x80 + oc Data.Bits..&. 0x3f - ] -} +-- -*- haskell -*- +-- This Alex file was machine-generated by the BNF converter +{ +{-# OPTIONS -fno-warn-incomplete-patterns #-} +{-# OPTIONS_GHC -w #-} +module Language.Clafer.Front.LexClafer where + + + +import qualified Data.Bits +import Data.Word (Word8) +} + + +$l = [a-zA-Z\192 - \255] # [\215 \247] -- isolatin1 letter FIXME +$c = [A-Z\192-\221] # [\215] -- capital isolatin1 letter FIXME +$s = [a-z\222-\255] # [\247] -- small isolatin1 letter FIXME +$d = [0-9] -- digit +$i = [$l $d _ '] -- identifier character +$u = [\0-\255] -- universal: any character + +@rsyms = -- symbols and non-identifier-like reserved words + \= | \[ | \] | \< \< | \> \> | \{ | \} | \` | \: | \- \> | \- \> \> | \: \= | \? | \+ | \* | \. \. | \| | \< \= \> | \= \> | \| \| | \& \& | \! | \< | \> | \< \= | \> \= | \! \= | \- | \/ | \% | \# | \< \: | \: \> | \+ \+ | \, | \- \- | \* \* | \& | \. | \; | \\ | \( | \) + +:- + +$white+ ; +@rsyms { tok (\p s -> PT p (eitherResIdent (TV . share) s)) } +$d + { tok (\p s -> PT p (eitherResIdent (T_PosInteger . share) s)) } +$d + \. $d + e \- ? $d + { tok (\p s -> PT p (eitherResIdent (T_PosDouble . share) s)) } +$d + \. $d + { tok (\p s -> PT p (eitherResIdent (T_PosReal . share) s)) } +\" ($u # [\" \\]| \\ [\" \\ n t]) * \" { tok (\p s -> PT p (eitherResIdent (T_PosString . share) s)) } +$l ($l | $d | \_ | \')* { tok (\p s -> PT p (eitherResIdent (T_PosIdent . share) s)) } +\/ \/ ($u # \n)* { tok (\p s -> PT p (eitherResIdent (T_PosLineComment . share) s)) } +\/ \* ($u # \* | \* + ($u # [\* \/]))* \* + \/ { tok (\p s -> PT p (eitherResIdent (T_PosBlockComment . share) s)) } +\[ a l l o y \| ($u # \| | \| + ($u # \])) * (\| \]) { tok (\p s -> PT p (eitherResIdent (T_PosAlloy . share) s)) } +\[ c h o c o \| ($u # \| | \| + ($u # \])) * (\| \]) { tok (\p s -> PT p (eitherResIdent (T_PosChoco . share) s)) } + +$l $i* { tok (\p s -> PT p (eitherResIdent (TV . share) s)) } + + + + + +{ + +tok :: (Posn -> String -> Token) -> (Posn -> String -> Token) +tok f p s = f p s + +share :: String -> String +share = id + +data Tok = + TS !String !Int -- reserved words and symbols + | TL !String -- string literals + | TI !String -- integer literals + | TV !String -- identifiers + | TD !String -- double precision float literals + | TC !String -- character literals + | T_PosInteger !String + | T_PosDouble !String + | T_PosReal !String + | T_PosString !String + | T_PosIdent !String + | T_PosLineComment !String + | T_PosBlockComment !String + | T_PosAlloy !String + | T_PosChoco !String + + deriving (Eq,Show,Ord) + +data Token = + PT Posn Tok + | Err Posn + deriving (Eq,Show,Ord) + +tokenPos :: [Token] -> String +tokenPos (PT (Pn _ l _) _ :_) = "line " ++ show l +tokenPos (Err (Pn _ l _) :_) = "line " ++ show l +tokenPos _ = "end of file" + +tokenPosn :: Token -> Posn +tokenPosn (PT p _) = p +tokenPosn (Err p) = p + +tokenLineCol :: Token -> (Int, Int) +tokenLineCol = posLineCol . tokenPosn + +posLineCol :: Posn -> (Int, Int) +posLineCol (Pn _ l c) = (l,c) + +mkPosToken :: Token -> ((Int, Int), String) +mkPosToken t@(PT p _) = (posLineCol p, prToken t) + +prToken :: Token -> String +prToken t = case t of + PT _ (TS s _) -> s + PT _ (TL s) -> show s + PT _ (TI s) -> s + PT _ (TV s) -> s + PT _ (TD s) -> s + PT _ (TC s) -> s + PT _ (T_PosInteger s) -> s + PT _ (T_PosDouble s) -> s + PT _ (T_PosReal s) -> s + PT _ (T_PosString s) -> s + PT _ (T_PosIdent s) -> s + PT _ (T_PosLineComment s) -> s + PT _ (T_PosBlockComment s) -> s + PT _ (T_PosAlloy s) -> s + PT _ (T_PosChoco s) -> s + + +data BTree = N | B String Tok BTree BTree deriving (Show) + +eitherResIdent :: (String -> Tok) -> String -> Tok +eitherResIdent tv s = treeFind resWords + where + treeFind N = tv s + treeFind (B a t left right) | s < a = treeFind left + | s > a = treeFind right + | s == a = t + +resWords :: BTree +resWords = b ">>" 34 (b "->>" 17 (b "*" 9 (b "&" 5 (b "#" 3 (b "!=" 2 (b "!" 1 N N) N) (b "%" 4 N N)) (b "(" 7 (b "&&" 6 N N) (b ")" 8 N N))) (b "," 13 (b "+" 11 (b "**" 10 N N) (b "++" 12 N N)) (b "--" 15 (b "-" 14 N N) (b "->" 16 N N)))) (b "<:" 26 (b ":=" 22 (b "/" 20 (b ".." 19 (b "." 18 N N) N) (b ":" 21 N N)) (b ";" 24 (b ":>" 23 N N) (b "<" 25 N N))) (b "=" 30 (b "<=" 28 (b "<<" 27 N N) (b "<=>" 29 N N)) (b ">" 32 (b "=>" 31 N N) (b ">=" 33 N N))))) (b "min" 51 (b "disj" 43 (b "`" 39 (b "\\" 37 (b "[" 36 (b "?" 35 N N) N) (b "]" 38 N N)) (b "all" 41 (b "abstract" 40 N N) (b "assert" 42 N N))) (b "in" 47 (b "enum" 45 (b "else" 44 N N) (b "if" 46 N N)) (b "max" 49 (b "lone" 48 N N) (b "maximize" 50 N N)))) (b "some" 60 (b "one" 56 (b "no" 54 (b "mux" 53 (b "minimize" 52 N N) N) (b "not" 55 N N)) (b "or" 58 (b "opt" 57 N N) (b "product" 59 N N))) (b "{" 64 (b "then" 62 (b "sum" 61 N N) (b "xor" 63 N N)) (b "||" 66 (b "|" 65 N N) (b "}" 67 N N))))) + where b s n = let bs = id s + in B bs (TS bs n) + +unescapeInitTail :: String -> String +unescapeInitTail = id . unesc . tail . id where + unesc s = case s of + '\\':c:cs | elem c ['\"', '\\', '\''] -> c : unesc cs + '\\':'n':cs -> '\n' : unesc cs + '\\':'t':cs -> '\t' : unesc cs + '"':[] -> [] + c:cs -> c : unesc cs + _ -> [] + +------------------------------------------------------------------- +-- Alex wrapper code. +-- A modified "posn" wrapper. +------------------------------------------------------------------- + +data Posn = Pn !Int !Int !Int + deriving (Eq, Show,Ord) + +alexStartPos :: Posn +alexStartPos = Pn 0 1 1 + +alexMove :: Posn -> Char -> Posn +alexMove (Pn a l c) '\t' = Pn (a+1) l (((c+7) `div` 8)*8+1) +alexMove (Pn a l c) '\n' = Pn (a+1) (l+1) 1 +alexMove (Pn a l c) _ = Pn (a+1) l (c+1) + +type Byte = Word8 + +type AlexInput = (Posn, -- current position, + Char, -- previous char + [Byte], -- pending bytes on the current char + String) -- current input string + +tokens :: String -> [Token] +tokens str = go (alexStartPos, '\n', [], str) + where + go :: AlexInput -> [Token] + go inp@(pos, _, _, str) = + case alexScan inp 0 of + AlexEOF -> [] + AlexError (pos, _, _, _) -> [Err pos] + AlexSkip inp' len -> go inp' + AlexToken inp' len act -> act pos (take len str) : (go inp') + +alexGetByte :: AlexInput -> Maybe (Byte,AlexInput) +alexGetByte (p, c, (b:bs), s) = Just (b, (p, c, bs, s)) +alexGetByte (p, _, [], s) = + case s of + [] -> Nothing + (c:s) -> + let p' = alexMove p c + (b:bs) = utf8Encode c + in p' `seq` Just (b, (p', c, bs, s)) + +alexInputPrevChar :: AlexInput -> Char +alexInputPrevChar (p, c, bs, s) = c + +-- | Encode a Haskell String to a list of Word8 values, in UTF8 format. +utf8Encode :: Char -> [Word8] +utf8Encode = map fromIntegral . go . ord + where + go oc + | oc <= 0x7f = [oc] + + | oc <= 0x7ff = [ 0xc0 + (oc `Data.Bits.shiftR` 6) + , 0x80 + oc Data.Bits..&. 0x3f + ] + + | oc <= 0xffff = [ 0xe0 + (oc `Data.Bits.shiftR` 12) + , 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f) + , 0x80 + oc Data.Bits..&. 0x3f + ] + | otherwise = [ 0xf0 + (oc `Data.Bits.shiftR` 18) + , 0x80 + ((oc `Data.Bits.shiftR` 12) Data.Bits..&. 0x3f) + , 0x80 + ((oc `Data.Bits.shiftR` 6) Data.Bits..&. 0x3f) + , 0x80 + oc Data.Bits..&. 0x3f + ] +} diff --git a/src/Language/Clafer/Generator/Alloy.hs b/src/Language/Clafer/Generator/Alloy.hs --- a/src/Language/Clafer/Generator/Alloy.hs +++ b/src/Language/Clafer/Generator/Alloy.hs @@ -236,7 +236,7 @@ where constraints = concatMap genConst $ _elements c genConst x = case x of - IEConstraint True pexp -> [ genPExp genEnv ((_uid c) : resPath) pexp ] + IEConstraint True pexp -> [ genPExp genEnv (_uid c : resPath) pexp ] IEConstraint False pexp -> [ CString "// Assertion " +++ (genAssertName pexp) +++ CString " ignored since nested assertions are not supported in Alloy.\n"] IEClafer c' -> (if genCardCrude (_card c') `elem` ["one", "lone", "some"] @@ -479,19 +479,20 @@ | otherwise = x transformExp x = x -genIFunExp :: String -> GenEnv -> [String] -> IExp -> Concat -genIFunExp pid' genEnv resPath (IFunExp op' exps') = - if (op' == iSumSet) - then genIFunExp pid' genEnv resPath (IFunExp iSumSet' [(removeright (head exps')), (getRight $ head exps')]) - else if (op' == iSumSet') - then Concat (IrPExp pid') $ intl exps'' (map CString $ genOp iSumSet) - else Concat (IrPExp pid') $ intl exps'' (map CString $ genOp op') +genIFunExp :: String -> GenEnv -> [String] -> IExp -> Concat +genIFunExp pid' genEnv resPath (IFunExp "min" [exp']) = Concat (IrPExp pid') $ (CString "min[") : (genPExp' genEnv resPath exp') : [CString "]"] +genIFunExp pid' genEnv resPath (IFunExp "max" [exp']) = Concat (IrPExp pid') $ (CString "max[") : (genPExp' genEnv resPath exp') : [CString "]"] +genIFunExp pid' genEnv resPath (IFunExp op' exps') + | op' == iSumSet = genIFunExp pid' genEnv resPath (IFunExp iSumSet' [(removeright (head exps')), (getRight $ head exps')]) + | op' == iSumSet' = Concat (IrPExp pid') $ intl exps'' (map CString $ genOp iSumSet) + | otherwise = Concat (IrPExp pid') $ intl exps'' (map CString $ genOp op') where - intl - | op' == iSumSet' = flip interleave - | op' `elem` arithBinOps && length exps' == 2 = interleave - | otherwise = \xs ys -> reverse $ interleave (reverse xs) (reverse ys) - exps'' = map (optBrArg genEnv resPath) exps' + iSumSet' = "sum'" + intl + | op' == iSumSet' = flip interleave + | op' `elem` arithBinOps && length exps' == 2 = interleave + | otherwise = \xs ys -> reverse $ interleave (reverse xs) (reverse ys) + exps'' = map (optBrArg genEnv resPath) exps' genIFunExp _ _ _ x = error $ "[bug] Alloy.genIFunExp: expecting a IFunExp, instead got: " ++ show x--This should never happen diff --git a/src/Language/Clafer/Generator/Choco.hs b/src/Language/Clafer/Generator/Choco.hs --- a/src/Language/Clafer/Generator/Choco.hs +++ b/src/Language/Clafer/Generator/Choco.hs @@ -1,5 +1,4 @@ {-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE ViewPatterns #-} -- | Generates JS representation of IR for the . module Language.Clafer.Generator.Choco (genCModule) where @@ -22,35 +21,41 @@ genCModule (imodule@IModule{_mDecls}, genv') scopes otherTokens' = genScopes ++ "\n" - ++ (genAbstractClafer =<< abstractClafers) - ++ (genConcreteClafer =<< concreteClafers) - ++ (genRefClafer =<< clafers) - ++ (genTopConstraintAssert =<< _mDecls) - ++ (genConstraint =<< clafers) - ++ (genGoal =<< _mDecls) + ++ (genClafers =<< _mDecls) + ++ (genSuperRefConstraintAssertGoal "root" =<< _mDecls) ++ genChocoEscapes where uidIClaferMap' = uidClaferMap genv' - root :: IClafer - root = fromJust $ findIClafer uidIClaferMap' rootIdent - toplevelClafers = mapMaybe iclafer _mDecls - -- The sort is so that we encounter sub clafers before super clafers when abstract clafers extend other abstract clafers - abstractClafers = sortBy (comparing $ length . supersOf . _uid) $ filter _isAbstract toplevelClafers - parentChildMap = childClafers root - clafers = snd <$> parentChildMap - claferUids = _uid <$> clafers - concreteClafers = filter isNotAbstract clafers + genClafers :: IElement -> String + genClafers (IEClafer (c@IClafer{_uid, _gcard, _elements})) + = _uid + ++ genClaferNesting c + ++ prop "withGroupCard" (genCard $ _interval <$> _gcard) + ++ ";\n" + ++ (genClafers =<< _elements) + genClafers _ = "" - claferWithUid u = fromMaybe (error $ "claferWithUid: \"" ++ u ++ "\" is not a clafer") $ findIClafer uidIClaferMap' u + genClaferNesting (IClafer{_isAbstract=True, _uid, _parentUID="root"}) + = " = Abstract(\"" ++ _uid ++ "\")" + genClaferNesting (IClafer{_isAbstract=True, _uid, _parentUID}) + = " = " ++ _parentUID ++ ".addAbstractChild(\"" ++ _uid ++ "\")" + genClaferNesting (IClafer{_isAbstract=False, _uid, _card, _parentUID="root"}) + = " = Clafer(\"" ++ _uid ++ "\")" + ++ prop "withCard" (genCard _card) + genClaferNesting (IClafer{_isAbstract=False, _uid, _card, _parentUID}) + = " = " + ++ _parentUID + ++ ".addChild(\"" ++ _uid ++ "\")" + ++ prop "withCard" (genCard _card) - -- All abstract clafers u inherits - supersOf :: String -> [String] - supersOf u = - case superOf u of - Just su -> su : supersOf su - Nothing -> [] + prop name value = + case value of + Just value' -> "." ++ name ++ "(" ++ value' ++ ")" + Nothing -> "" + claferWithUid u = fromMaybe (error $ "claferWithUid: \"" ++ u ++ "\" is not a clafer") $ findIClafer uidIClaferMap' u + superOf u = case _super $ claferWithUid u of Just (PExp{_exp = IClaferId{_sident}}) @@ -59,20 +64,11 @@ | otherwise -> Just _sident _ -> Nothing -{- refOf u = - case _reference $ claferWithUid u of - Just (IReference{_ref=PExp{_exp = IClaferId{_sident}}}) - | _sident == "int" -> Just "integer" - | isPrimitive _sident -> Just _sident - | otherwise -> Nothing - _ -> Nothing --} - parentOf u = fst $ fromMaybe (error $ "parentOf: \"" ++ u ++ "\" is not a clafer") $ find ((== u) . _uid . snd) parentChildMap - - genCard :: Interval -> Maybe String - genCard (0, -1) = Nothing - genCard (low, -1) = return $ show low - genCard (low, high) = return $ show low ++ ", " ++ show high + genCard :: Maybe Interval -> Maybe String + genCard (Just (0, -1)) = Nothing + genCard (Just (low, -1)) = return $ show low + genCard (Just (low, high)) = return $ show low ++ ", " ++ show high + genCard _ = Nothing genScopes :: Result @@ -87,12 +83,12 @@ scopeMap = [uid' ++ ":" ++ show scope | (uid', scope) <- scopes, uid' /= "int"] genChocoEscapes :: String - genChocoEscapes = concat $ map printChocoEscape otherTokens' + genChocoEscapes = concatMap printChocoEscape otherTokens' where printChocoEscape (PT _ (T_PosChoco code)) = let code' = fromJust $ stripPrefix "[choco|" code in - take ((length code') - 2) code' + take (length code' - 2) code' printChocoEscape _ = "" exprs :: [IExp] @@ -105,58 +101,32 @@ longestString :: Int longestString = maximum $ 16 : mapMaybe stringLength exprs - genConcreteClafer :: IClafer -> Result - genConcreteClafer IClafer{_uid, _card = Just _card, _gcard = Just (IGCard _ _gcard)} = - _uid ++ " = " ++ constructor ++ "(\"" ++ _uid ++ "\")" ++ prop "withCard" (genCard _card) ++ prop "withGroupCard" (genCard _gcard) ++ prop "extending" (superOf _uid) ++ ";\n" - where - constructor = - case parentOf _uid of - "root" -> "Clafer" - puid -> puid ++ ".addChild" - genConcreteClafer (IClafer _ _ Nothing _ _ _ _ _ _ _ _) = error "Choco.getConcreteClafer undefined" - genConcreteClafer (IClafer _ _ (Just (IGCard _ _)) _ _ _ _ _ Nothing _ _) = error "Choco.getConcreteClafer undefined" - - prop name value = - case value of - Just value' -> "." ++ name ++ "(" ++ value' ++ ")" - Nothing -> "" - - - genRefClafer :: IClafer -> Result - genRefClafer c@IClafer{_uid, _reference, _card} = - case (getReference c, _reference, _card) of - ([target], Just (IReference True _), Just (lb, ub)) -> if (lb > 1 || ub > 1 || lb == -1 || ub == -1) - then _uid ++ ".refToUnique(" ++ genTarget target ++ ");\n" - else _uid ++ ".refTo(" ++ genTarget target ++ ");\n" - ([target], Just (IReference _ _), _) -> _uid ++ ".refTo(" ++ genTarget target ++ ");\n" - _ -> "" + genSuperRefConstraintAssertGoal :: String -> IElement -> Result + genSuperRefConstraintAssertGoal _ IEClafer{_iClafer=IClafer{_uid, _super=Nothing, _reference=Nothing, _elements}} + = genSuperRefConstraintAssertGoal _uid =<< _elements + genSuperRefConstraintAssertGoal _ (IEClafer c@IClafer{_uid, _card, _super, _reference, _elements}) + = _uid + ++ prop "extending" (superOf _uid) + ++ (case (getReference c, _reference, _card) of + ([target], Just (IReference True _), Just (lb, ub)) -> if lb > 1 || ub > 1 || lb == -1 || ub == -1 + then ".refToUnique(" ++ genTarget target ++ ")" + else ".refTo(" ++ genTarget target ++ ")" + ([target], Just (IReference _ _), _) -> ".refTo(" ++ genTarget target ++ ")" + _ -> "") + ++ ";\n" + ++ (genSuperRefConstraintAssertGoal _uid =<< _elements) where genTarget "integer" = "Int" genTarget "int" = "Int" genTarget target = target - - genAbstractClafer :: IClafer -> Result - genAbstractClafer IClafer{_uid, _gcard = Just (IGCard _ _gcard)} = - _uid ++ " = Abstract(\"" ++ _uid ++ "\")" ++ prop "extending" (superOf _uid) ++ prop "withGroupCard" (genCard _gcard) ++ ";\n" - genAbstractClafer IClafer{_uid, _gcard = Nothing} = - _uid ++ " = Abstract(\"" ++ _uid ++ "\")" ++ prop "extending" (superOf _uid) ++ ";\n" + genSuperRefConstraintAssertGoal "root" (IEConstraint True pexp) = "Constraint(" ++ genConstraintPExp pexp ++ ");\n" + genSuperRefConstraintAssertGoal pUID (IEConstraint True pexp) = pUID ++ ".addConstraint(" ++ genConstraintPExp pexp ++ ");\n" + genSuperRefConstraintAssertGoal _ (IEConstraint False pexp) = "assert(" ++ genConstraintPExp pexp ++ ");\n" + genSuperRefConstraintAssertGoal _ (IEGoal True PExp{_exp=IFunExp _ [pexp]}) = "max(" ++ genConstraintPExp pexp ++ ");\n" + genSuperRefConstraintAssertGoal _ (IEGoal False PExp{_exp=IFunExp _ [pexp]}) = "min(" ++ genConstraintPExp pexp ++ ");\n" + genSuperRefConstraintAssertGoal _ _ = "" - genTopConstraintAssert :: IElement -> Result - genTopConstraintAssert (IEConstraint True pexp) = "Constraint(" ++ genConstraintPExp pexp ++ ");\n" - genTopConstraintAssert (IEConstraint False pexp) = "assert(" ++ genConstraintPExp pexp ++ ");\n" - genTopConstraintAssert _ = "" - - genConstraint :: IClafer -> Result - genConstraint IClafer{_uid, _elements} = - unlines [_uid ++ ".addConstraint(" ++ genConstraintPExp c ++ ");" - | c <- mapMaybe iconstraint _elements] - - genGoal :: IElement -> Result - genGoal (IEGoal True PExp{_exp=IFunExp _ [pexp]}) = "max(" ++ genConstraintPExp pexp ++ ");\n" - genGoal (IEGoal False PExp{_exp=IFunExp _ [pexp]}) = "min(" ++ genConstraintPExp pexp ++ ");\n" - genGoal _ = "" - rewrite :: PExp -> PExp -- Rearrange right joins to left joins. rewrite p1@PExp{_iType = Just _, _exp = IFunExp "." [p2, p3@PExp{_exp = IFunExp "." _}]} = @@ -190,7 +160,7 @@ genConstraintExp (IFunExp "." [e1, PExp{_exp = IClaferId{_sident}}]) = "join(" ++ genConstraintPExp e1 ++ ", " ++ _sident ++ ")" genConstraintExp (IFunExp "." [_, _]) = - error $ "Did not rewrite all joins to left joins." + error "Did not rewrite all joins to left joins." genConstraintExp (IFunExp "-" [arg]) = "minus(" ++ genConstraintPExp arg ++ ")" genConstraintExp (IFunExp "-" [arg1, arg2]) = @@ -213,7 +183,7 @@ -- this is a keyword in Javascript so use "$this" instead genConstraintExp IClaferId{_sident = "this"} = "$this()" genConstraintExp IClaferId{_sident} - | _sident `elem` claferUids = "global(" ++ _sident ++ ")" + | isJust $ findIClafer uidIClaferMap' _sident = "global(" ++ _sident ++ ")" | otherwise = _sident genConstraintExp (IInt val) = "constant(" ++ show val ++ ")" genConstraintExp (IStr val) = "constant(" ++ show val ++ ")" @@ -253,28 +223,4 @@ mapFunc "ifthenelse" = "ifThenElse" mapFunc op' = error $ "Choco: Unknown op: " ++ op' -{- sidentOf u = ident $ claferWithUid u - scopeOf "integer" = undefined - scopeOf "int" = undefined - scopeOf i = fromMaybe 1 $ lookup i scopes -} bitwidth = fromMaybe 4 $ lookup "int" scopes :: Integer - --- isQuant PExp{_exp = IDeclPExp{}} = True --- isQuant _ = False - -isNotAbstract :: IClafer -> Bool -isNotAbstract = not . _isAbstract - -iclafer :: IElement -> Maybe IClafer -iclafer (IEClafer c) = Just c -iclafer _ = Nothing - -iconstraint :: IElement -> Maybe PExp -iconstraint (IEConstraint _ pexp) = Just pexp -iconstraint _ = Nothing - -childClafers :: IClafer -> [(String, IClafer)] -childClafers IClafer{_uid, _elements} = - childClafers' _uid =<< mapMaybe iclafer _elements - where - childClafers' parent' c@IClafer{_uid, _elements} = (parent', c) : (childClafers' _uid =<< mapMaybe iclafer _elements) diff --git a/src/Language/Clafer/Generator/Python.hs b/src/Language/Clafer/Generator/Python.hs deleted file mode 100644 --- a/src/Language/Clafer/Generator/Python.hs +++ /dev/null @@ -1,268 +0,0 @@ -{-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE ViewPatterns #-} - --- | Generates JS representation of IR for the . -module Language.Clafer.Generator.Python (genPythonModule) where - -import Control.Applicative -import Control.Lens.Plated hiding (rewrite) -import Control.Monad -import Data.Data.Lens -import Data.List -import Data.Maybe -import Data.Ord -import Prelude hiding (exp) -import Language.Clafer.Common -import Language.Clafer.Intermediate.Intclafer - --- | Choco 3 code generation -genPythonModule :: (IModule, GEnv) -> [(UID, Integer)] -> Result -genPythonModule (imodule@IModule{_mDecls}, genv') scopes = - genImports - ++ "\n" - ++ (genAbstractClafer =<< abstractClafers) - ++ (genConcreteClafer =<< concreteClafers) - ++ (genRefClafer =<< clafers) - ++ (genTopConstraint =<< _mDecls) - ++ (genConstraint =<< clafers) - ++ (genGoal =<< _mDecls) - ++ genScopes - where - uidIClaferMap' = uidClaferMap genv' - root :: IClafer - root = fromJust $ findIClafer uidIClaferMap' rootIdent - - toplevelClafers = mapMaybe iclafer _mDecls - -- The sort is so that we encounter sub clafers before super clafers when abstract clafers extend other abstract clafers - abstractClafers = sortBy (comparing $ length . supersOf . _uid) $ filter _isAbstract toplevelClafers - parentChildMap = childClafers root - clafers = snd <$> parentChildMap - claferUids = _uid <$> clafers - concreteClafers = filter isNotAbstract clafers - - claferWithUid u = fromMaybe (error $ "claferWithUid: \"" ++ u ++ "\" is not a clafer") $ findIClafer uidIClaferMap' u - - -- All abstract clafers u inherits - supersOf :: String -> [String] - supersOf u = - case superOf u of - Just su -> su : supersOf su - Nothing -> [] - - superOf u = - case _super $ claferWithUid u of - Just (PExp{_exp = IClaferId{_sident}}) - | _sident == baseClafer -> Nothing - | isPrimitive _sident -> Nothing - | otherwise -> Just _sident - _ -> Nothing - -{- refOf u = - case _reference $ claferWithUid u of - Just (IReference{_ref=PExp{_exp = IClaferId{_sident}}}) - | _sident == "int" -> Just "integer" - | isPrimitive _sident -> Just _sident - | otherwise -> Nothing - _ -> Nothing --} - parentOf u = fst $ fromMaybe (error $ "parentOf: \"" ++ u ++ "\" is not a clafer") $ find ((== u) . _uid . snd) parentChildMap - - genCard :: Interval -> Maybe String - genCard (0, -1) = Nothing - genCard (low, -1) = return $ show low - genCard (low, high) = return $ show low ++ ", " ++ show high - - genImports = concat - [ "from jsir.IR import *\n" - - ] - - genScopes :: Result - genScopes = - (if null scopeMap then "" else "scope({" ++ intercalate ", " scopeMap ++ "});\n") - ++ "defaultScope(1);\n" - ++ "stringLength(" ++ show longestString ++ ");\n" - where - scopeMap = [uid' ++ ":" ++ show scope | (uid', scope) <- scopes, uid' /= "int"] - exprs :: [IExp] - exprs = universeOn biplate imodule - - stringLength :: IExp -> Maybe Int - stringLength (IStr string) = Just $ length string - stringLength _ = Nothing - - longestString :: Int - longestString = maximum $ 16 : mapMaybe stringLength exprs - - genConcreteClafer :: IClafer -> Result - genConcreteClafer IClafer{_uid, _card = Just _card, _gcard = Just (IGCard _ _gcard)} = - _uid ++ " = " ++ constructor ++ "(\"" ++ _uid ++ "\")" ++ prop "withCard" (genCard _card) ++ prop "withGroupCard" (genCard _gcard) ++ prop "extending" (superOf _uid) ++ ";\n" - where - constructor = - case parentOf _uid of - "root" -> "Clafer" - puid -> puid ++ ".addChild" - genConcreteClafer (IClafer _ _ Nothing _ _ _ _ _ _ _ _) = error "Choco.getConcreteClafer undefined" - genConcreteClafer (IClafer _ _ (Just (IGCard _ _)) _ _ _ _ _ Nothing _ _) = error "Choco.getConcreteClafer undefined" - - prop name value = - case value of - Just value' -> "." ++ name ++ "(" ++ value' ++ ")" - Nothing -> "" - - - genRefClafer :: IClafer -> Result - genRefClafer c@IClafer{_uid, _reference, _card} = - case (getReference c, _reference, _card) of - ([target], Just (IReference True _), Just (lb, ub)) -> if (lb > 1 || ub > 1 || lb == -1 || ub == -1) - then _uid ++ ".refToUnique(" ++ genTarget target ++ ");\n" - else _uid ++ ".refTo(" ++ genTarget target ++ ");\n" - ([target], Just (IReference _ _), _) -> _uid ++ ".refTo(" ++ genTarget target ++ ");\n" - _ -> "" - where - genTarget "integer" = "\"int\"" - genTarget "int" = "\"int\"" - genTarget target = target - - genAbstractClafer :: IClafer -> Result - genAbstractClafer IClafer{_uid, _card = Just _} = - _uid ++ " = Abstract(\"" ++ _uid ++ "\")" ++ prop "extending" (superOf _uid) ++ ";\n" - genAbstractClafer IClafer{_uid, _card = Nothing} = - _uid ++ " = Abstract(\"" ++ _uid ++ "\")" ++ prop "extending" (superOf _uid) ++ ";\n" - - - genTopConstraint :: IElement -> Result - genTopConstraint (IEConstraint _ pexp) = "Constraint(" ++ genConstraintPExp pexp ++ ");\n" - genTopConstraint _ = "" - - genConstraint :: IClafer -> Result - genConstraint IClafer{_uid, _elements} = - unlines [_uid ++ ".addConstraint(" ++ genConstraintPExp c ++ ");" - | c <- mapMaybe iconstraint _elements] - - genGoal :: IElement -> Result - genGoal (IEGoal True PExp{_exp=IFunExp _ [pexp]}) = "max(" ++ genConstraintPExp pexp ++ ");\n" - genGoal (IEGoal False PExp{_exp=IFunExp _ [pexp]}) = "min(" ++ genConstraintPExp pexp ++ ");\n" - genGoal _ = "" - - rewrite :: PExp -> PExp - -- Rearrange right joins to left joins. - rewrite p1@PExp{_iType = Just _, _exp = IFunExp "." [p2, p3@PExp{_exp = IFunExp "." _}]} = - p1{_exp = IFunExp "." [p3{_iType = _iType p4, _exp = IFunExp "." [p2, p4]}, p5]} - where - PExp{_exp = IFunExp "." [p4, p5]} = rewrite p3 - rewrite p1@PExp{_exp = IFunExp{_op = "-", _exps = [PExp{_exp = IInt i}]}} = - -- This is so that the output looks cleaner, no other purpose since the Choco optimizer - -- in the backend will treat the pre-rewritten expression the same. - p1{_exp = IInt (-i)} - rewrite p = p - - genConstraintPExp :: PExp -> String - genConstraintPExp = genConstraintExp . _exp . rewrite - - genConstraintExp :: IExp -> String - genConstraintExp (IDeclPExp quant' [] body') = - mapQuant quant' ++ "(" ++ genConstraintPExp body' ++ ")" - genConstraintExp (IDeclPExp quant' decls' body') = - mapQuant quant' ++ "([" ++ intercalate ", " (map genDecl decls') ++ "], " ++ genConstraintPExp body' ++ ")" - where - genDecl (IDecl isDisj' locals body'') = - (if isDisj' then "disjDecl" else "decl") ++ "([" ++ intercalate ", " (map genLocal locals) ++ "], " ++ genConstraintPExp body'' ++ ")" - genLocal local = - local ++ " = local(\"" ++ local ++ "\")" - - genConstraintExp (IFunExp "." [e1, PExp{_exp = IClaferId{_sident = "dref"}}]) = - "joinRef(" ++ genConstraintPExp e1 ++ ")" - genConstraintExp (IFunExp "." [e1, PExp{_exp = IClaferId{_sident = "parent"}}]) = - "joinParent(" ++ genConstraintPExp e1 ++ ")" - genConstraintExp (IFunExp "." [e1, PExp{_exp = IClaferId{_sident}}]) = - "join(" ++ genConstraintPExp e1 ++ ", " ++ _sident ++ ")" - genConstraintExp (IFunExp "." [_, _]) = - error $ "Did not rewrite all joins to left joins." - genConstraintExp (IFunExp "-" [arg]) = - "minus(" ++ genConstraintPExp arg ++ ")" - genConstraintExp (IFunExp "-" [arg1, arg2]) = - "sub(" ++ genConstraintPExp arg1 ++ ", " ++ genConstraintPExp arg2 ++ ")" - genConstraintExp (IFunExp "sum" args') - | [arg] <- args', PExp{_exp = IFunExp{_exps = [a, PExp{_exp = IClaferId{_sident = "dref"}}]}} <- rewrite arg = - "sum(" ++ genConstraintPExp a ++ ")" - | [arg] <- args' = - "sum(" ++ genConstraintPExp arg ++ ")" - | otherwise = error $ "[bug] Python.genConstraintExp: Unexpected sum argument: " ++ show args' - genConstraintExp (IFunExp "product" args') - | [arg] <- args', PExp{_exp = IFunExp{_exps = [a, PExp{_exp = IClaferId{_sident = "dref"}}]}} <- rewrite arg = - "product(" ++ genConstraintPExp a ++ ")" - | otherwise = error "Python: Unexpected product argument." - genConstraintExp (IFunExp "+" args') = - (if _iType (head args') == Just TString then "concat" else "add") ++ - "(" ++ intercalate ", " (map genConstraintPExp args') ++ ")" - genConstraintExp (IFunExp op' args') = - mapFunc op' ++ "(" ++ intercalate ", " (map genConstraintPExp args') ++ ")" - -- this is a keyword in Javascript so use "$this" instead - genConstraintExp IClaferId{_sident = "this"} = "$this()" - genConstraintExp IClaferId{_sident} - | _sident `elem` claferUids = "glob(" ++ _sident ++ ")" - | otherwise = _sident - genConstraintExp (IInt val) = "constant(" ++ show val ++ ")" - genConstraintExp (IStr val) = "constant(" ++ show val ++ ")" - genConstraintExp (IDouble val) = "constant(" ++ show val ++ ")" - genConstraintExp (IReal val) = "constant(" ++ show val ++ ")" - - mapQuant INo = "none" - mapQuant ISome = "some" - mapQuant IAll = "all" - mapQuant IOne = "one" - mapQuant ILone = "lone" - - mapFunc "!" = "not" - mapFunc "#" = "card" - mapFunc "min" = "minimum" - mapFunc "max" = "maximum" - mapFunc "<=>" = "ifOnlyIf" - mapFunc "=>" = "implies" - mapFunc "||" = "or" - mapFunc "xor" = "xor" - mapFunc "&&" = "and" - mapFunc "<" = "lessThan" - mapFunc ">" = "greaterThan" - mapFunc "=" = "equal" - mapFunc "<=" = "lessThanEqual" - mapFunc ">=" = "greaterThanEqual" - mapFunc "!=" = "notEqual" - mapFunc "in" = "set_in" - mapFunc "not in" = "set_nin" - mapFunc "+" = "add" - mapFunc "*" = "mul" - mapFunc "/" = "div" - mapFunc "%" = "mod" - mapFunc "++" = "set_union" - mapFunc "--" = "set_diff" - mapFunc "**" = "set_inter" - mapFunc "ifthenelse" = "ifThenElse" - mapFunc op' = error $ "Python: Unknown op: " ++ op' - -{- sidentOf u = ident $ claferWithUid u - scopeOf "integer" = undefined - scopeOf "int" = undefined - scopeOf i = fromMaybe 1 $ lookup i scopes - bitwidth = fromMaybe 4 $ lookup "int" scopes :: Integer -} - --- isQuant PExp{_exp = IDeclPExp{}} = True --- isQuant _ = False - -isNotAbstract :: IClafer -> Bool -isNotAbstract = not . _isAbstract - -iclafer :: IElement -> Maybe IClafer -iclafer (IEClafer c) = Just c -iclafer _ = Nothing - -iconstraint :: IElement -> Maybe PExp -iconstraint (IEConstraint _ pexp) = Just pexp -iconstraint _ = Nothing - -childClafers :: IClafer -> [(String, IClafer)] -childClafers IClafer{_uid, _elements} = - childClafers' _uid =<< mapMaybe iclafer _elements - where - childClafers' parent' c@IClafer{_uid, _elements} = (parent', c) : (childClafers' _uid =<< mapMaybe iclafer _elements) diff --git a/src/Language/Clafer/Intermediate/Intclafer.hs b/src/Language/Clafer/Intermediate/Intclafer.hs --- a/src/Language/Clafer/Intermediate/Intclafer.hs +++ b/src/Language/Clafer/Intermediate/Intclafer.hs @@ -198,8 +198,8 @@ ! - not (logical) # - set counting operator - - negation (arithmetic) - max - maximum (created for goals) - min - minimum (created for goals) + max - maximum (created for goals and maximum of a set) + min - minimum (created for goals and minimum of a set) 2. Binary operators: \<=\> - equivalence =\> - implication diff --git a/src/Language/Clafer/Intermediate/ResolverInheritance.hs b/src/Language/Clafer/Intermediate/ResolverInheritance.hs --- a/src/Language/Clafer/Intermediate/ResolverInheritance.hs +++ b/src/Language/Clafer/Intermediate/ResolverInheritance.hs @@ -1,345 +1,350 @@ -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE NamedFieldPuns #-} -{- - Copyright (C) 2012-2015 Kacper Bak, Michal Antkiewicz - - 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. --} -module Language.Clafer.Intermediate.ResolverInheritance where - -import Control.Applicative -import Control.Lens ((^.), (&), (%~), (.~), mapped) -import Control.Monad -import Control.Monad.Except -import Control.Monad.State -import Data.Maybe -import Data.Graph -import Data.Tree -import Data.List -import qualified Data.Map as Map -import Data.StringMap (StringMap) -import qualified Data.StringMap as SMap -import Prelude - -import Language.ClaferT -import Language.Clafer.Common -import Language.Clafer.Front.AbsClafer -import Language.Clafer.Intermediate.Intclafer -import Language.Clafer.Intermediate.ResolverName - - --- | Resolve Non-overlapping inheritance -resolveNModule :: (IModule, GEnv) -> Resolve (IModule, GEnv) -resolveNModule (imodule, genv') = - do - let - unresolvedDecls = _mDecls imodule - abstractClafers = filter _isAbstract $ bfsClafers $ toClafers unresolvedDecls - resolvedDecls <- mapM (resolveNElement abstractClafers) unresolvedDecls - let - relocatedDecls = relocateTopLevelAbstractToParents resolvedDecls -- F> Top-level abstract clafer extending a nested abstract clafer IClafer -> Resolve IClafer -resolveNClafer abstractClafers clafer = - do - (super', superIClafer') <- resolveNSuper abstractClafers $ _super clafer - -- F> Top-level abstract clafer extending a nested abstract clafer F> - let - parentUID' = - case superIClafer' of - (Just superIClafer'') -> - if _isAbstract clafer && isTopLevel clafer && not (isTopLevel superIClafer'') - then _parentUID superIClafer'' -- make clafer a sibling of the superIClafer' - else _parentUID clafer - Nothing -> _parentUID clafer - -- Maybe PExp -> Resolve (Maybe PExp, Maybe IClafer) -resolveNSuper _ Nothing = return (Nothing, Nothing) -resolveNSuper abstractClafers (Just (PExp _ pid' pos' (IClaferId _ id' _ _))) = - if isPrimitive id' - then throwError $ SemanticErr pos' $ "Primitive types are not allowed as super types: " ++ id' - else do - r <- resolveN pos' abstractClafers id' - (id'', [superClafer']) <- case r of - Nothing -> throwError $ SemanticErr pos' $ "No superclafer found: " ++ id' - Just m -> return m - return $ (Just $ PExp (Just $ TClafer [id'']) pid' pos' (IClaferId "" id'' (isTopLevel superClafer') (Just $ id'')) - , Just superClafer') -resolveNSuper _ x = return (x, Nothing) - - -resolveNElement :: [IClafer] -> IElement -> Resolve IElement -resolveNElement abstractClafers x = case x of - IEClafer clafer -> IEClafer <$> resolveNClafer abstractClafers clafer - IEConstraint _ _ -> return x - IEGoal _ _ -> return x - -resolveN :: Span -> [IClafer] -> String -> Resolve (Maybe (String, [IClafer])) -resolveN pos' abstractClafers id' = - findUnique pos' id' $ map (\x -> (x, [x])) abstractClafers - - -resolveHierarchy :: UIDIClaferMap -> IElement -> IElement -resolveHierarchy uidClaferMap' (IEClafer iClafer') = IEClafer $ super.mapped.iType.mapped %~ addHierarchy $ iClafer' - where - addHierarchy :: IType -> IType - addHierarchy (TClafer _) = TClafer $ tail $ mapHierarchy _uid getSuper uidClaferMap' iClafer' - addHierarchy x = x -resolveHierarchy _ x = x - - --- | Resolve overlapping inheritance -resolveOModule :: (IModule, GEnv) -> Resolve (IModule, GEnv) -resolveOModule (imodule, genv') = - do - let decls' = _mDecls imodule - decls'' <- mapM (resolveOElement (defSEnv genv' decls')) decls' - let imodule' = imodule{_mDecls = decls''} - return ( imodule' - , genv'{sClafers = bfs toNodeShallow $ toClafers decls'', uidClaferMap = createUidIClaferMap imodule'}) - - -resolveOClafer :: SEnv -> IClafer -> Resolve IClafer -resolveOClafer env clafer = - do - reference' <- resolveOReference env {context = Just clafer} $ _reference clafer - elements' <- mapM (resolveOElement env {context = Just clafer}) $ _elements clafer - return $ clafer {_reference = reference', _elements = elements'} - - -resolveOReference :: SEnv -> Maybe IReference -> Resolve (Maybe IReference) -resolveOReference _ Nothing = return Nothing -resolveOReference env (Just (IReference is' exp')) = Just <$> IReference is' <$> resolvePExp env exp' - - -resolveOElement :: SEnv -> IElement -> Resolve IElement -resolveOElement env x = case x of - IEClafer clafer -> IEClafer <$> resolveOClafer env clafer - IEConstraint _ _ -> return x - IEGoal _ _ -> return x - - --- | Resolve inherited and default cardinalities -analyzeModule :: (IModule, GEnv) -> IModule -analyzeModule (imodule, genv') = - imodule{_mDecls = map (analyzeElement (defSEnv genv' decls')) decls'} - where - decls' = _mDecls imodule - - -analyzeClafer :: SEnv -> IClafer -> IClafer -analyzeClafer env clafer = - clafer' {_elements = map (analyzeElement env {context = Just clafer'}) $ - _elements clafer'} - where - clafer' = clafer {_gcard = analyzeGCard env clafer, - _card = analyzeCard env clafer} - - --- only for non-overlapping -analyzeGCard :: SEnv -> IClafer -> Maybe IGCard -analyzeGCard env clafer = gcard' `mplus` (Just $ IGCard False (0, -1)) - where - gcard' - | isNothing $ _super clafer = _gcard clafer - | otherwise = listToMaybe $ mapMaybe _gcard $ findHierarchy getSuper (uidClaferMap $ genv env) clafer - - -analyzeCard :: SEnv -> IClafer -> Maybe Interval -analyzeCard env clafer = _card clafer `mplus` Just card' - where - card' - | _isAbstract clafer = (0, -1) - | (isJust $ context env) && pGcard == (0, -1) - || (isTopLevel clafer) = (1, 1) - | otherwise = (0, 1) - pGcard = _interval $ fromJust $ _gcard $ fromJust $ context env - -analyzeElement :: SEnv -> IElement -> IElement -analyzeElement env x = case x of - IEClafer clafer -> IEClafer $ analyzeClafer env clafer - IEConstraint _ _ -> x - IEGoal _ _ -> x - --- | Expand inheritance -resolveEModule :: (IModule, GEnv) -> (IModule, GEnv) -resolveEModule (imodule, genv') = (imodule', newGenv) - where - decls' = _mDecls imodule - imodule' = imodule{_mDecls = decls''} - newGenv = genv''{uidClaferMap = createUidIClaferMap imodule'} - (decls'', genv'') = runState (mapM (resolveEElement [] - (unrollableModule imodule) - False decls') decls') genv' - --- ----------------------------------------------------------------------------- -unrollableModule :: IModule -> [String] -unrollableModule imodule = getDirUnrollables $ - mapMaybe unrollabeDeclaration $ _mDecls imodule - -unrollabeDeclaration :: IElement -> Maybe (String, [String]) -unrollabeDeclaration x = case x of - IEClafer clafer -> if _isAbstract clafer - then Just (_uid clafer, unrollableClafer clafer) - else Nothing - IEConstraint _ _ -> Nothing - IEGoal _ _ -> Nothing - -unrollableClafer :: IClafer -> [String] -unrollableClafer clafer = (getSuper clafer) ++ deps - where - deps = (toClafers $ _elements clafer) >>= unrollableClafer - - -getDirUnrollables :: [(String, [String])] -> [String] -getDirUnrollables dependencies = (filter isUnrollable $ map (map v2n) $ - map flatten (scc graph)) >>= map fst3 - where - (graph, v2n, _) = graphFromEdges $map (\(c, ss) -> (c, c, ss)) dependencies - isUnrollable (x:[]) = fst3 x `elem` trd3 x - isUnrollable _ = True - --- ----------------------------------------------------------------------------- -resolveEClafer :: MonadState GEnv m => [String] -> [String] -> Bool -> [IElement] -> IClafer -> m IClafer -resolveEClafer predecessors unrollables absAncestor declarations clafer = do - uidClaferMap' <- gets uidClaferMap - clafer' <- renameClafer absAncestor (_parentUID clafer) clafer - let predecessors' = _uid clafer' : predecessors - (sElements, super', superList) <- - resolveEInheritance predecessors' unrollables absAncestor declarations - (findHierarchy getSuper uidClaferMap' clafer) - let sClafer = Map.fromList $ zip (map _uid superList) $ repeat [predecessors'] - modify (\e -> e {stable = Map.delete "clafer" $ - Map.unionWith ((nub.).(++)) sClafer $ - stable e}) - elements' <- - mapM (resolveEElement predecessors' unrollables absAncestor declarations) - $ _elements clafer - return $ clafer' {_super = super', _elements = elements' ++ sElements} - -renameClafer :: MonadState GEnv m => Bool -> UID -> IClafer -> m IClafer -renameClafer False _ clafer = return clafer -renameClafer True puid clafer = renameClafer' puid clafer - -renameClafer' :: MonadState GEnv m => UID -> IClafer -> m IClafer -renameClafer' puid clafer = do - let claferIdent = _ident clafer - identCountMap' <- gets identCountMap - let count = Map.findWithDefault 0 claferIdent identCountMap' - modify (\e -> e { identCountMap = Map.alter (\_ -> Just (count+1)) claferIdent identCountMap' } ) - return $ clafer { _uid = genId claferIdent count, _parentUID = puid } - -genId :: String -> Int -> String -genId id' count = concat ["c", show count, "_", id'] - -resolveEInheritance :: MonadState GEnv m => [String] -> [String] -> Bool -> [IElement] -> [IClafer] -> m ([IElement], Maybe PExp, [IClafer]) -resolveEInheritance predecessors unrollables absAncestor declarations allSuper = do - let superList = (if absAncestor then id else tail) allSuper - let unrollSuper = filter (\s -> _uid s `notElem` unrollables) $ tail allSuper - elements' <- - mapM (resolveEElement predecessors unrollables True declarations) $ - unrollSuper >>= _elements - - let super' = case (`elem` unrollables) <$> getSuper clafer of - [True] -> _super clafer - _ -> Nothing - return (elements', super', superList) - where - clafer = head allSuper - -resolveEElement :: MonadState GEnv m => [String] -> [String] -> Bool -> [IElement] -> IElement -> m IElement -resolveEElement predecessors unrollables absAncestor declarations x = case x of - IEClafer clafer -> if _isAbstract clafer then return x else IEClafer `liftM` - resolveEClafer predecessors unrollables absAncestor declarations clafer - IEConstraint _ _ -> return x - IEGoal _ _ -> return x - --- ----------------------------------------------------------------------------- - -resolveRedefinition :: (IModule, GEnv) -> Resolve IModule -resolveRedefinition (iModule, _) = - if (not $ null improperClafers) - then throwError $ SemanticErr noSpan ("Refinement errors in the following places:\n" ++ improperClafers) - else return iModule - where - uidIClaferMap' = createUidIClaferMap iModule - improperClafers :: String - improperClafers = foldMapIR isImproper iModule - - isImproper :: Ir -> String - isImproper (IRClafer claf@IClafer{_cinPos = (Span (Pos l c) _) ,_ident=i}) = - let - match = matchNestedInheritance uidIClaferMap' claf - in - if (isProperNesting uidIClaferMap' match) - then let - (properCardinalityRefinement, properBagToSetRefinement, properTargetSubtyping) = isProperRefinement uidIClaferMap' match - in if (properCardinalityRefinement) - then if (properBagToSetRefinement) - then if (properTargetSubtyping) - then "" - else ("Improper target subtyping for clafer '" ++ i ++ "' on line " ++ show l ++ " column " ++ show c ++ "\n") - else ("Improper bag to set refinement for clafer '" ++ i ++ "' on line " ++ show l ++ " column " ++ show c ++ "\n") - else ("Improper cardinality refinement for clafer '" ++ i ++ "' on line " ++ show l ++ " column " ++ show c ++ "\n") - else ("Improperly nested clafer '" ++ i ++ "' on line " ++ show l ++ " column " ++ show c ++ "\n") - isImproper _ = "" - --- F> Top-level abstract clafer extending a nested abstract clafer F> -relocateTopLevelAbstractToParents :: [IElement] -> [IElement] -relocateTopLevelAbstractToParents originalElements = - let - (elementsToBeRelocated, remainingElements) = partition needsRelocation originalElements - in - case elementsToBeRelocated of - [] -> originalElements - _ -> map (insertElements $ mkParentUIDIElementMap elementsToBeRelocated) remainingElements - where - needsRelocation :: IElement -> Bool - needsRelocation IEClafer{_iClafer} = not $ isTopLevel _iClafer - needsRelocation _ = False - - -- creates a map from parentUID to a list of elements to be added as children of a clafer with that UID - mkParentUIDIElementMap :: [IElement] -> StringMap [IElement] - mkParentUIDIElementMap elems = foldl' - (\accumMap' (parentUID', elem') -> SMap.insertWith (++) parentUID' [elem'] accumMap') - SMap.empty - (map (\e -> (_parentUID $ _iClafer e, e)) elems) - - insertElements :: StringMap [IElement] -> IElement -> IElement - insertElements parentMap targetElement = let - targetUID = targetElement ^. iClafer . uid - newChildren = SMap.findWithDefault [] targetUID parentMap - currentElements = targetElement ^. iClafer . elements - newElements = map (insertElements parentMap) currentElements - ++ newChildren - in - targetElement & iClafer . elements .~ newElements --- + + 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. +-} +module Language.Clafer.Intermediate.ResolverInheritance where + +import Control.Applicative +import Control.Lens ((^.), (&), (%%~), (.~), traverse) +import Control.Monad +import Control.Monad.Except +import Control.Monad.State +import Data.Maybe +import Data.Graph +import Data.Tree +import Data.List +import qualified Data.Map as Map +import Data.StringMap (StringMap) +import qualified Data.StringMap as SMap +import Prelude hiding (traverse) + +import Language.ClaferT +import Language.Clafer.Common +import Language.Clafer.Front.AbsClafer +import Language.Clafer.Intermediate.Intclafer +import Language.Clafer.Intermediate.ResolverName + + +-- | Resolve Non-overlapping inheritance +resolveNModule :: (IModule, GEnv) -> Resolve (IModule, GEnv) +resolveNModule (imodule, genv') = + do + let + unresolvedDecls = _mDecls imodule + abstractClafers = filter _isAbstract $ bfsClafers $ toClafers unresolvedDecls + resolvedDecls <- mapM (resolveNElement abstractClafers) unresolvedDecls + let + relocatedDecls = relocateTopLevelAbstractToParents resolvedDecls -- F> Top-level abstract clafer extending a nested abstract clafer IClafer -> Resolve IClafer +resolveNClafer abstractClafers clafer = + do + (super', superIClafer') <- resolveNSuper abstractClafers $ _super clafer + -- F> Top-level abstract clafer extending a nested abstract clafer F> + let + parentUID' = + case superIClafer' of + (Just superIClafer'') -> + if _isAbstract clafer && isTopLevel clafer && not (isTopLevel superIClafer'') + then _parentUID superIClafer'' -- make clafer a sibling of the superIClafer' + else _parentUID clafer + Nothing -> _parentUID clafer + -- Maybe PExp -> Resolve (Maybe PExp, Maybe IClafer) +resolveNSuper _ Nothing = return (Nothing, Nothing) +resolveNSuper abstractClafers (Just (PExp _ pid' pos' (IClaferId _ id' _ _))) = + if isPrimitive id' + then throwError $ SemanticErr pos' $ "Primitive types are not allowed as super types: " ++ id' + else do + r <- resolveN pos' abstractClafers id' + (id'', [superClafer']) <- case r of + Nothing -> throwError $ SemanticErr pos' $ "No superclafer found: " ++ id' + Just m -> return m + return (Just $ PExp (Just $ TClafer [id'']) pid' pos' (IClaferId "" id'' (isTopLevel superClafer') (Just id'')) + , Just superClafer') +resolveNSuper _ x = return (x, Nothing) + + +resolveNElement :: [IClafer] -> IElement -> Resolve IElement +resolveNElement abstractClafers x = case x of + IEClafer clafer -> IEClafer <$> resolveNClafer abstractClafers clafer + IEConstraint _ _ -> return x + IEGoal _ _ -> return x + +resolveN :: Span -> [IClafer] -> String -> Resolve (Maybe (String, [IClafer])) +resolveN pos' abstractClafers id' = + findUnique pos' id' $ map (\x -> (x, [x])) abstractClafers + + +resolveHierarchy :: UIDIClaferMap -> IElement -> Resolve IElement +resolveHierarchy uidClaferMap' (IEClafer iClafer') = IEClafer <$> (super.traverse.iType.traverse %%~ addHierarchy $ iClafer') + where + addHierarchy :: IType -> Resolve IType + addHierarchy (TClafer _) = TClafer <$> checkForLoop (tail $ mapHierarchy _uid getSuper uidClaferMap' iClafer') + addHierarchy x = return x + checkForLoop :: [String] -> Resolve [String] + checkForLoop supers = case find (_uid iClafer' ==) supers of + Nothing -> return supers + Just _ -> throwError $ SemanticErr (_cinPos iClafer') $ "ResolverInheritance: clafer " ++ _uid iClafer' ++ " inherits from itself" +resolveHierarchy _ x = return x + + +-- | Resolve overlapping inheritance +resolveOModule :: (IModule, GEnv) -> Resolve (IModule, GEnv) +resolveOModule (imodule, genv') = + do + let decls' = _mDecls imodule + decls'' <- mapM (resolveOElement (defSEnv genv' decls')) decls' + let imodule' = imodule{_mDecls = decls''} + return ( imodule' + , genv'{sClafers = bfs toNodeShallow $ toClafers decls'', uidClaferMap = createUidIClaferMap imodule'}) + + +resolveOClafer :: SEnv -> IClafer -> Resolve IClafer +resolveOClafer env clafer = + do + reference' <- resolveOReference env {context = Just clafer} $ _reference clafer + elements' <- mapM (resolveOElement env {context = Just clafer}) $ _elements clafer + return $ clafer {_reference = reference', _elements = elements'} + + +resolveOReference :: SEnv -> Maybe IReference -> Resolve (Maybe IReference) +resolveOReference _ Nothing = return Nothing +resolveOReference env (Just (IReference is' exp')) = Just <$> IReference is' <$> resolvePExp env exp' + + +resolveOElement :: SEnv -> IElement -> Resolve IElement +resolveOElement env x = case x of + IEClafer clafer -> IEClafer <$> resolveOClafer env clafer + IEConstraint _ _ -> return x + IEGoal _ _ -> return x + + +-- | Resolve inherited and default cardinalities +analyzeModule :: (IModule, GEnv) -> IModule +analyzeModule (imodule, genv') = + imodule{_mDecls = map (analyzeElement (defSEnv genv' decls')) decls'} + where + decls' = _mDecls imodule + + +analyzeClafer :: SEnv -> IClafer -> IClafer +analyzeClafer env clafer = + clafer' {_elements = map (analyzeElement env {context = Just clafer'}) $ + _elements clafer'} + where + clafer' = clafer {_gcard = analyzeGCard env clafer, + _card = analyzeCard env clafer} + + +-- only for non-overlapping +analyzeGCard :: SEnv -> IClafer -> Maybe IGCard +analyzeGCard env clafer = gcard' `mplus` (Just $ IGCard False (0, -1)) + where + gcard' + | isNothing $ _super clafer = _gcard clafer + | otherwise = listToMaybe $ mapMaybe _gcard $ findHierarchy getSuper (uidClaferMap $ genv env) clafer + + +analyzeCard :: SEnv -> IClafer -> Maybe Interval +analyzeCard env clafer = _card clafer `mplus` Just card' + where + card' + | _isAbstract clafer = (0, -1) + | (isJust $ context env) && pGcard == (0, -1) + || (isTopLevel clafer) = (1, 1) + | otherwise = (0, 1) + pGcard = _interval $ fromJust $ _gcard $ fromJust $ context env + +analyzeElement :: SEnv -> IElement -> IElement +analyzeElement env x = case x of + IEClafer clafer -> IEClafer $ analyzeClafer env clafer + IEConstraint _ _ -> x + IEGoal _ _ -> x + +-- | Expand inheritance +resolveEModule :: (IModule, GEnv) -> (IModule, GEnv) +resolveEModule (imodule, genv') = (imodule', newGenv) + where + decls' = _mDecls imodule + imodule' = imodule{_mDecls = decls''} + newGenv = genv''{uidClaferMap = createUidIClaferMap imodule'} + (decls'', genv'') = runState (mapM (resolveEElement [] + (unrollableModule imodule) + False decls') decls') genv' + +-- ----------------------------------------------------------------------------- +unrollableModule :: IModule -> [String] +unrollableModule imodule = getDirUnrollables $ + mapMaybe unrollabeDeclaration $ _mDecls imodule + +unrollabeDeclaration :: IElement -> Maybe (String, [String]) +unrollabeDeclaration x = case x of + IEClafer clafer -> if _isAbstract clafer + then Just (_uid clafer, unrollableClafer clafer) + else Nothing + IEConstraint _ _ -> Nothing + IEGoal _ _ -> Nothing + +unrollableClafer :: IClafer -> [String] +unrollableClafer clafer = (getSuper clafer) ++ deps + where + deps = (toClafers $ _elements clafer) >>= unrollableClafer + + +getDirUnrollables :: [(String, [String])] -> [String] +getDirUnrollables dependencies = (filter isUnrollable $ map (map v2n) $ + map flatten (scc graph)) >>= map fst3 + where + (graph, v2n, _) = graphFromEdges $map (\(c, ss) -> (c, c, ss)) dependencies + isUnrollable (x:[]) = fst3 x `elem` trd3 x + isUnrollable _ = True + +-- ----------------------------------------------------------------------------- +resolveEClafer :: MonadState GEnv m => [String] -> [String] -> Bool -> [IElement] -> IClafer -> m IClafer +resolveEClafer predecessors unrollables absAncestor declarations clafer = do + uidClaferMap' <- gets uidClaferMap + clafer' <- renameClafer absAncestor (_parentUID clafer) clafer + let predecessors' = _uid clafer' : predecessors + (sElements, super', superList) <- + resolveEInheritance predecessors' unrollables absAncestor declarations + (findHierarchy getSuper uidClaferMap' clafer) + let sClafer = Map.fromList $ zip (map _uid superList) $ repeat [predecessors'] + modify (\e -> e {stable = Map.delete "clafer" $ + Map.unionWith ((nub.).(++)) sClafer $ + stable e}) + elements' <- + mapM (resolveEElement predecessors' unrollables absAncestor declarations) + $ _elements clafer + return $ clafer' {_super = super', _elements = elements' ++ sElements} + +renameClafer :: MonadState GEnv m => Bool -> UID -> IClafer -> m IClafer +renameClafer False _ clafer = return clafer +renameClafer True puid clafer = renameClafer' puid clafer + +renameClafer' :: MonadState GEnv m => UID -> IClafer -> m IClafer +renameClafer' puid clafer = do + let claferIdent = _ident clafer + identCountMap' <- gets identCountMap + let count = Map.findWithDefault 0 claferIdent identCountMap' + modify (\e -> e { identCountMap = Map.alter (\_ -> Just (count+1)) claferIdent identCountMap' } ) + return $ clafer { _uid = genId claferIdent count, _parentUID = puid } + +genId :: String -> Int -> String +genId id' count = concat ["c", show count, "_", id'] + +resolveEInheritance :: MonadState GEnv m => [String] -> [String] -> Bool -> [IElement] -> [IClafer] -> m ([IElement], Maybe PExp, [IClafer]) +resolveEInheritance predecessors unrollables absAncestor declarations allSuper = do + let superList = (if absAncestor then id else tail) allSuper + let unrollSuper = filter (\s -> _uid s `notElem` unrollables) $ tail allSuper + elements' <- + mapM (resolveEElement predecessors unrollables True declarations) $ + unrollSuper >>= _elements + + let super' = case (`elem` unrollables) <$> getSuper clafer of + [True] -> _super clafer + _ -> Nothing + return (elements', super', superList) + where + clafer = head allSuper + +resolveEElement :: MonadState GEnv m => [String] -> [String] -> Bool -> [IElement] -> IElement -> m IElement +resolveEElement predecessors unrollables absAncestor declarations x = case x of + IEClafer clafer -> if _isAbstract clafer then return x else IEClafer `liftM` + resolveEClafer predecessors unrollables absAncestor declarations clafer + IEConstraint _ _ -> return x + IEGoal _ _ -> return x + +-- ----------------------------------------------------------------------------- + +resolveRedefinition :: (IModule, GEnv) -> Resolve IModule +resolveRedefinition (iModule, _) = + if (not $ null improperClafers) + then throwError $ SemanticErr noSpan ("Refinement errors in the following places:\n" ++ improperClafers) + else return iModule + where + uidIClaferMap' = createUidIClaferMap iModule + improperClafers :: String + improperClafers = foldMapIR isImproper iModule + + isImproper :: Ir -> String + isImproper (IRClafer claf@IClafer{_cinPos = (Span (Pos l c) _) ,_ident=i}) = + let + match = matchNestedInheritance uidIClaferMap' claf + in + if (isProperNesting uidIClaferMap' match) + then let + (properCardinalityRefinement, properBagToSetRefinement, properTargetSubtyping) = isProperRefinement uidIClaferMap' match + in if (properCardinalityRefinement) + then if (properBagToSetRefinement) + then if (properTargetSubtyping) + then "" + else ("Improper target subtyping for clafer '" ++ i ++ "' on line " ++ show l ++ " column " ++ show c ++ "\n") + else ("Improper bag to set refinement for clafer '" ++ i ++ "' on line " ++ show l ++ " column " ++ show c ++ "\n") + else ("Improper cardinality refinement for clafer '" ++ i ++ "' on line " ++ show l ++ " column " ++ show c ++ "\n") + else ("Improperly nested clafer '" ++ i ++ "' on line " ++ show l ++ " column " ++ show c ++ "\n") + isImproper _ = "" + +-- F> Top-level abstract clafer extending a nested abstract clafer F> +relocateTopLevelAbstractToParents :: [IElement] -> [IElement] +relocateTopLevelAbstractToParents originalElements = + let + (elementsToBeRelocated, remainingElements) = partition needsRelocation originalElements + in + case elementsToBeRelocated of + [] -> originalElements + _ -> map (insertElements $ mkParentUIDIElementMap elementsToBeRelocated) remainingElements + where + needsRelocation :: IElement -> Bool + needsRelocation IEClafer{_iClafer} = not $ isTopLevel _iClafer + needsRelocation _ = False + + -- creates a map from parentUID to a list of elements to be added as children of a clafer with that UID + mkParentUIDIElementMap :: [IElement] -> StringMap [IElement] + mkParentUIDIElementMap elems = foldl' + (\accumMap' (parentUID', elem') -> SMap.insertWith (++) parentUID' [elem'] accumMap') + SMap.empty + (map (\e -> (_parentUID $ _iClafer e, e)) elems) + + insertElements :: StringMap [IElement] -> IElement -> IElement + insertElements parentMap targetElement = let + targetUID = targetElement ^. iClafer . uid + newChildren = SMap.findWithDefault [] targetUID parentMap + currentElements = targetElement ^. iClafer . elements + newElements = map (insertElements parentMap) currentElements + ++ newChildren + in + targetElement & iClafer . elements .~ newElements +--