diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,20 @@ +Copyright (c) 2015 L. Thomas van Binsbergen + +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. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/funcons-intgen.cabal b/funcons-intgen.cabal new file mode 100644 --- /dev/null +++ b/funcons-intgen.cabal @@ -0,0 +1,56 @@ +name: funcons-intgen +version: 0.2.0.1 +synopsis: Generate Funcons interpreters from CBS description files +homepage: http://plancomps.org +license: MIT +license-file: LICENSE +author: L. Thomas van Binsbergen , Neil Sculthorpe +maintainer: L. Thomas van Binsbergen +copyright: Copyright (C) 2015 L. Thomas van Binsbergen and Neil Schulthorpe +category: Compilers +build-type: Simple +cabal-version: >=1.10 + +executable cbsc + main-is: Main.hs + other-modules: Parsing.Spec, + Parsing.Mutual, + Parsing.Term, + Parsing.Rule, + Parsing.Syntax, + Parsing.Lexer, + Print.HaskellModule, +-- Print.JavaClasses, +-- Print.Ascii, + Print.Util, + Simplify.ConcreteToAbstract + Simplify.Simplifier, + Simplify.CoreToTarget, + Simplify.LiftStrictness, + Simplify.TargetToFunconModules, + Simplify.TargetToIML, + Simplify.Utils, + Types.Bindings, + Types.ConcreteSyntax, + Types.SourceAbstractSyntax, + Types.CoreAbstractSyntax, + Types.TargetAbstractSyntax, + Types.FunconModule + build-depends: base >=4.8 && <= 5 + ,filepath >= 1.3.0 + ,directory + ,split + ,pretty >= 1.1.2 + ,uu-cco>=0.1.0.5 + ,text >= 1.2 && < 1.3 + ,mtl >= 2.2.1 + ,containers >= 0.5 && < 0.6 + ,funcons-tools >= 0.2.0.7 + ,gll>=0.4.0.9 + ,regex-applicative + ,iml-tools>=0.3.0.4 + ,funcons-values >= 0.1.0.5 + hs-source-dirs: src + default-language: Haskell2010 + ghc-options: -fwarn-incomplete-patterns + -fwarn-unused-imports diff --git a/src/Main.hs b/src/Main.hs new file mode 100644 --- /dev/null +++ b/src/Main.hs @@ -0,0 +1,78 @@ +module Main where + +import Parsing.Lexer (lexer) +import Parsing.Spec (parser) +import Simplify.ConcreteToAbstract (cs2as) +import Simplify.Simplifier (simplifier) +import Simplify.CoreToTarget (core2target) +import Simplify.LiftStrictness (lift_strictness) +import Simplify.TargetToIML (target2iml, stepR, mkValOpRules) +import Simplify.TargetToFunconModules (target2fmodule) +import Print.HaskellModule (cbs2module) +--import Print.JavaClasses (cbs2classes) +--import Print.Ascii (cbs2ascii) +import Types.FunconModule (FunconModule) + +import IML.CodeGen.LaTeX +import IML.Printer +import IML.Trans.ProMan +import IML.Grammar.Specs (Spec(Spec),AnyDecls(ARuleDecl)) + +import CCO.Component (Component, ioRun) + +import Control.Monad (when) +import Data.List (isPrefixOf) +import Control.Arrow ((>>>)) +import System.Environment (getArgs) + +main = do all_args <- getArgs + let (options,args) = (filter pred all_args, filter (not . pred) all_args) + where pred = isPrefixOf "--" + case args of + [] | any (== ("--iml-value-operations")) options -> + run_iml (Spec (map ARuleDecl mkValOpRules)) options + [cbsf] -> run cbsf Nothing Nothing options + [cbsf,srcdir] -> run cbsf (Just srcdir) Nothing options + [cbsf,srcdir,lang] -> run cbsf (Just srcdir) (Just lang) options + _ -> putStrLn $ + "version CBS-beta\n\ + \usage: cbsc \n\ + \CBS-PATH: path to the .cbs file\n\ + \ for which code is to be generated.\n\ + \ The file should be within a directory named \"Funcons\".\n\ + \SRC-DIR: the source-directory in which the code is to be generated.\n\ + \LANG: the language for which the .cbs file contains a specification.\n" + +run cbsfile srcdir lang options = do + when (not toIML) (putStrLn ("Generating " ++ cbsfile)) + cbs_contents <- readFile cbsfile + let core2target' + | "--generate-congruences" `elem` options = core2target >>> lift_strictness + | otherwise = core2target + target <- ioRun (lexer >>> parser >>> cs2as pholder >>> simplifier + >>> core2target') cbs_contents + if toIML + then do let ran_options = IML.Trans.ProMan.runOptions options + iml <- runComponentIO ran_options target2iml target + run_iml iml options + else do fmodule <- ioRun (target2fmodule pholder) target + m_contents <- ioRun ((cbs2 options) cbsfile srcdir lang) fmodule + case m_contents of + Nothing -> putStrLn "No funcons, types or entities to generate" + Just make_contents -> make_contents + where pholder = any (== "--generate-unspecified-funcons") options + toIML = any (== "--IML") options + +cbs2 :: [String] -> FilePath -> Maybe FilePath -> Maybe String -> + CCO.Component.Component FunconModule (Maybe (IO ())) +cbs2 options {-| "--java" `elem` options = cbs2classes + | "--ascii" `elem` options = cbs2ascii + | otherwise -} = cbs2module + +run_iml iml options = do + let chain | "--LaTeX" `elem` options = spec2latex_module >>> component_ show + | otherwise = spec2highstring + printable <- runComponentIO (IML.Trans.ProMan.runOptions options) chain iml + putStrLn printable + + diff --git a/src/Parsing/Lexer.hs b/src/Parsing/Lexer.hs new file mode 100644 --- /dev/null +++ b/src/Parsing/Lexer.hs @@ -0,0 +1,217 @@ + +module Parsing.Lexer (Parsing.Lexer.lexer, mylexer) where + +import GLL.Combinators (Token(..),SubsumesToken(..)) + +import CCO.Component + +import Data.Char (isDigit, isAlpha, isUpper, isLower, isAlphaNum, isSpace) +import Text.Regex.Applicative +import Text.Read (readEither) + +lexer :: Component String [Token] +lexer = component (return . mylexer) +--lexer = component (((\x -> trace (show x) (return x))) . mylexer) + +mylexer = sSpecs + +-- Do not forget that states can be created that do not perform +-- longest match by default. Could help to disambiguate atoms for example. +lState :: String -> Bool -> RE Char t -> (t -> String -> [Token]) -> + (t -> Maybe Token) -> String -> [Token] +lState _ _ _ _ _ [] = [] +lState stateName discardLayout myTokens mySelector adder s = + let re | discardLayout = Just <$> myTokens <|> ws + | otherwise = Just <$> myTokens + ws = (Nothing <$ some (psym isSpace)) + <|> (Nothing <$ string "//" <* many (psym ((/=) '\n'))) + <|> (Nothing <$ string "#" <* many (psym ((/=) '\n'))) + in case findLongestPrefix re s of + Just (Just tok, rest) -> (maybe id (:) (adder tok)) (mySelector tok rest) + Just (Nothing,rest) -> lState stateName discardLayout myTokens mySelector adder rest + Nothing -> error ("lexical error at " ++ stateName ++ ": " ++ show (take 10 s)) + + +sSpecs = lState "SPECS" True (lCommentStart <|> lTokens) sel Just + where sel tok = case tok of Keyword "/*" -> sComment + Keyword "/*HS-IMPORTS" -> sComment + Keyword "Section" -> sSectionNum + Keyword "Subsection" -> sSectionNum + _ -> sSpecs + +sSectionNum = lState "SECTION-NUM" True (optional lSectNum) sel id + where sel tok = sSection + +sSection = lState "SECTION" False lTitleWords (const sSpecs) Just + +sComment = lState "COMMENT" False + (lHS_import <|> lTick <|> lCommentEnd <|> lCommentPart) sel Just + where sel tok = case tok of Token "TICK" _ -> sTickIn + Keyword "*/" -> sSpecs + _ -> sComment + lHS_import = Keyword <$> string "HS-IMPORTS" + +sTickIn = lState "TICK-IN" True (lTick <|> lTokens) sel Just + where sel tok = case tok of Token "TICK" _ -> sTickIn + _ -> sSpecInTick + +sTickOut = lState "TICK-OUT" False (lTick <|> lCommentPart) sel Just + where sel tok = case tok of Token "TICK" _ -> sTickOut + _ -> sComment + +sSpecInTick = lState "SPEC-IN-TICK" True (lTick <|> lTokens) sel Just + where sel tok = case tok of Token "TICK" _ -> sTickOut + _ -> sSpecInTick + + +lTokens :: SubsumesToken t => RE Char t +lTokens = + lCharacters + <|> lKeywords + <|> charsToInt <$> optional (sym '-') <*> some (psym isDigit) + <|> upcast . IDLit . Just <$> lName + <|> upcast . AltIDLit . Just <$> lVar +-- <|> upcast . CharLit . Just <$> lCharLit + <|> upcast . StringLit . Just <$> lStringLit + <|> lMore + where + charsToInt Nothing n = upcast (IntLit (Just (read n))) + charsToInt (Just _) n = upcast (IntLit (Just (-(read n)))) + + lChar c = upcast (Char c) <$ sym c + lCharacters = foldr ((<|>) . lChar) empty cbs_characters + + lKeyword k = upcast (Keyword k) <$ string k + lKeywords = foldr ((<|>) . lKeyword) empty cbs_keywords + + lMore = foldr ((<|>) . uncurry lToken) empty myTokens + lToken t re = upcast . Token t . Just <$> re + + lStringLit = toString <$ sym '\"' <*> many strChar <* sym '\"' + where strChar = sym '\\' *> sym '\"' + <|> psym ((/=) '\"') + toString inner = case readEither ("\"" ++ inner ++ "\"") of + Left _ -> inner + Right v -> v + + lCharLit = id <$ sym '\'' <*> charChar <* sym '\'' + where charChar = sym '\\' *> sym '\'' + <|> psym ((/=) '\'') + +cbs_characters = "~():,*+?!|[]{}.@=<>-_&^" + +cbs_keywords = [ "Alias" + , "Assert" + , "Auxiliary" + , "Built-in" + , "Datatype" + , "Entity" + , "Funcon" + , "Hidden" + , "Language" + , "Lexis" + , "Meta-variables" + , "Otherwise" + , "Rule" + , "SDF" + , "Semantics" + , "Syntax" + , "Type" + , "Variables" + , "...", ">:", "<:", "=>", "|->", "==", "~>" + , "=/=", "|-", "--", "->", "::=", "[[", "]]"] + +lCommentStart = Keyword "/*" <$ sym '/' <* sym '*' + <|> Keyword "/*HS-IMPORTS" <$ string "/*HS-IMPORTS" +lCommentEnd = Keyword "*/" <$ sym '*' <* sym '/' + +myTokens = [("ATOM", lAtom), ("FILE", lFile), ("BAR", lBar) + ,("ORDINAL", lOrdinal), ("DQUOTE", lDQuote) ] + +lDQuote = "\\\"" <$ sym '\\' <* sym '\"' + +lBar = "----" <$ sym '-' <* sym '-' <* sym '-' <* sym '-' <* many (sym '-') + +lName = (:) <$> psym isLower <*> many (psym (\c -> isAlphaNum c || c == '-')) + +lCommentPart :: SubsumesToken t => RE Char t +lCommentPart = + upcast (Char '*') <$ sym '*' + <|> upcast (Char '@') <$ sym '@' + <|> upcast <$ sym '@' <*> lSectNum + <|> upcast . Token "ORDINARY" . Just <$> lOrdinary + + +lOrdinary = some $ psym (\c -> c /= '*' && c /= '`' && c /= '@') + +--TODO atoms are not being lexed correctly +-- for example '\' | '`' should be two atoms separated by a char '|' +-- this is an interesting example of ambiguity +-- +-- ambiguity: '\' '\' , one atom '\' ' followed by \', or two atoms '\' +-- +-- Lexis +-- capitalized-characters ::= '\' | '`' +lAtom = sym '\'' *> ((concat <$> few atom_char) <|> lBackslash <|> escaped) <* sym '\'' + where atom_char = (:[]) <$> psym (not . invC) +-- TODO how to allow escaped single quotes in atoms (see ambiguities above) +-- <|> escaped + where invC c = c == '\'' || c == '\t' || c == '\n' || c == '\r' + -- || c == '|' {- temporary fix -} + + escaped = (\a b -> [a,b]) <$> sym '\\' <*> sym '\'' +lVar = (\c xs ys zs -> c:xs++ys++zs) <$> psym isUpper <*> many (psym isAlpha) + <*> stem_rest <*> rest + where stem_rest = (++) <$> (concat <$> many ((:) <$> sym '-' <*> some (psym isAlpha))) + <*> stem_suffix + stem_suffix = maybe [] id <$> optional ((\a b -> [a,b]) <$> sym '-' <*> psym isDigit) + rest = (++) <$> suffix <*> (maybe [] id <$> (optional postfix)) + where suffix = (++) <$> many (psym isDigit) <*> many (sym '\'') + postfix = (:[]) <$> (sym '*' <|> sym '+' <|> sym '?') + +lFile = ((++)) . concat <$> many part_sep <*> part + where part = some (psym isAlphaNum) + part_sep = (\a b -> a ++ [b]) <$> part <*> (sym '-' <|> sym '_') + +lSectNum :: RE Char Token +lSectNum = Token "SECT-NUM" . Just <$> lSect1Num + <|> Token "SECT-NUM" . Just <$> lSect2Num + <|> Token "SECT-NUM" . Just <$> lSect3Num + <|> Token "SECT-NUM" . Just <$> lSect4Num + +-- ambiguity MISC lexes both as lSect1Num, but should be interpreted as lTitleWords +lSect1Num = lOrdinal +lSect2Num = (\x y z -> x++[y]++z) <$> lOrdinal <*> sym '.' <*> lOrdinal +lSect3Num = (\x1 x2 x3 x4 x5 -> x1++[x2]++x3++[x4]++x5) <$> + lOrdinal <*> sym '.' <*> lOrdinal <*> sym '.' <*> lOrdinal +lSect4Num = (\x1 x2 x3 x4 x5 x6 x7 -> x1++[x2]++x3++[x4]++x5++[x6]++x7) <$> + lOrdinal <*> sym '.' <*> lOrdinal <*> sym '.' <*> lOrdinal + <*> sym '.' <*> lOrdinal +lOrdinal = some (psym isDigit) {- CAUSES AMBIGUITY, IS IT USED? <|> (:[]) <$> psym isAlpha-} + +lTitleWords :: RE Char Token +lTitleWords = Token "TITLE" . Just <$> many (psym ((/=) '\n')) <* sym '\n' + +lTick :: SubsumesToken t => RE Char t +lTick = upcast (Token "TICK" (Just "`")) <$ sym '`' + +-- | Escaped backslash +lBackslash = "\\" <$ sym '\\' <* sym '\\' + +concatMany :: RE Char String -> RE Char String +concatMany p = concat <$> many p + +concatSome p = concat <$> some p + +{- +notFollowedBy :: RE c s1 -> RE c s2 -> RE c s1 +notFollowedBy p q = do + -- apply the regex p + (res, matched) <- withMatched p + case match q of --then see if the regex q matches + Just _ -> -- if it does we need to insert `matched` back into the input string + empty + Nothing -> return res -- otherwise just return the result +-} + + diff --git a/src/Parsing/Mutual.hs b/src/Parsing/Mutual.hs new file mode 100644 --- /dev/null +++ b/src/Parsing/Mutual.hs @@ -0,0 +1,63 @@ + +module Parsing.Mutual where + +import Funcons.EDSL (SeqSortOp(..)) + +import GLL.Combinators + +import Types.ConcreteSyntax +import Parsing.Lexer (mylexer) + +type Parser a = BNF Token a + +debug :: Parser a -> String -> [a] +debug p = parseWithOptions [throwErrors] p . mylexer + +-- solves ambiguity B:=>booleans +pDef :: Parser String +pDef = "DEF" <:=> keyword "~>" + +pVar :: Parser Var +pVar = "VAR" <:=> Nothing <$$ keychar '_' + <||> Just <$$> alt_id_lit + <||> Nothing <$$ keyword "..." + +pVarString :: Parser String +pVarString = "VAR" <:=> (:[]) <$$> keychar '_' <||> alt_id_lit + +pSynName :: Parser String +pSynName = "SYN-NAME" <:=> name_lit + +pPostfix :: Parser SeqSortOp +pPostfix = "POSTFIX" + <::=> StarOp <$$ keychar '*' + <||> PlusOp <$$ keychar '+' + <||> QuestionMarkOp <$$ keychar '?' + + +-- TODO: debug pConst "\"\\\"\"" +pConst :: Parser Const +pConst = "CONST" + <:=> ConstAtom <$$> atom_lit + <||> ConstString <$$> string_lit + <||> ConstNat <$$> int_lit + <||> ConstFloat <$$> float_lit -- TODO add float_lit to GLL.Combinators + +-- tokens +atom_lit :: Parser String +atom_lit = token "ATOM" + +name_lit :: Parser String +name_lit = id_lit + +bar :: Parser String +bar = token "BAR" + +file_name :: Parser String +file_name = token "FILE" + +ordinal :: Parser String +ordinal = "NT-ORDINAL" <:=> token "ORDINAL" <||> (show <$$> int_lit) + +double_quote :: Parser String +double_quote = token "DQUOTE" diff --git a/src/Parsing/Rule.hs b/src/Parsing/Rule.hs new file mode 100644 --- /dev/null +++ b/src/Parsing/Rule.hs @@ -0,0 +1,102 @@ + +module Parsing.Rule where + +import Parsing.Syntax +import Parsing.Mutual +import Parsing.Term +import Types.ConcreteSyntax + +import GLL.Combinators + +pRuleSpec :: Parser Rule +pRuleSpec = "RULE-SPEC" + <:=> keyword "Rule" **> pRule + +-- ambiguity: +-- X ---> X atomic(X) ---> V ------ X ---> V +-- alternative interpretation is X ---> X atomic (X) ---> V ------- X ---> V +pRule :: Parser Rule +pRule = "RULE" + <:=> Inference [] <$$> pConclusion + <||> Inference <$$> many pPremise <** bar <**> pConclusion + <||> Desugar <$$> pPhrasePatt <** keychar ':' <**> pPhraseType <** + keychar '=' <**> pPhraseTerm + <||> Semantics <$$> name_lit <**> pPhrasePatt <**> optional pTerm <** + keychar '=' <**> pTerms + +pConclusion :: Parser Conclusion +pConclusion = "CONCLUSION" + <:=> ConcDynamic <$$> optional pContext <**> pState <**> pDynamic <**> pState + <||> ConcTyping <$$> optional pContext <**> pState <** keychar ':' <**> pTerm + <||> ConcStatic <$$> optional pContext <**> pState <** keychar ':' <**> + pTerm <**> pStatic <**> pState + <||> ConcRewrite <$$> pTerm <** keyword "~>" <**> pTerm + +pPremise :: Parser Premise +pPremise = "PREMISE" + <:=> PremDynamic <$$> optional pContext <**> pState <**> pDynamic <**> pState + <||> PremTyping <$$> optional pContext <**> pState <** keychar ':' <**> pTerm + <||> PremStatic <$$> optional pContext <**> pState <** keychar ':' <**> + pTerm <**> pStatic <**> pState + <||> PremRewrite <$$> pTerm <** keyword "~>" <**> pTerm + <||> PremEquality <$$> pTerm <** keyword "==" <**> pTerm + <||> PremInequality <$$> pTerm <** keyword "=/=" <**> pTerm + <||> PremSubtype <$$> pTerm <** keyword "<:" <**> pTerm + +pContext :: Parser Context +pContext = "CONTEXT" + <:=> Context <$$> multipleSepBy1 pEntTerm (keychar ',') <** keyword "|-" + +pPolarEntTerm :: Parser PolarEntTerm +pPolarEntTerm = "POLAR-ENT-TERM" + <:=> (\n mp t -> (n,t,mp)) <$$> name_lit <**> optional pPolarity <**> pTerm + +pEntTerm :: Parser EntTerm +pEntTerm = "ENT-TERM" + <:=> (,) <$$> name_lit <**> pTerm + +pPolarity :: Parser Polarity +pPolarity = "POLARITY" <:=> In <$$ keychar '?' <||> Out <$$ keychar '!' + +pState :: Parser State +pState = "STATE" + <:=> StateExplicit <$$ keychar '<' <**> pTerm <** keychar ',' <**> + multipleSepBy1 (pEntTerm) (keychar ',') <** keychar '>' + <||> StateImplicit <$$> pTerm + +pDynamic :: Parser Dynamic +pDynamic = "DYNAMIC" + <::=> DynamicExplicit <$$ keyword "--" <**> multipleSepBy1 (pPolarEntTerm) (keychar ',') <** keyword "->" <**> optional (int_lit) + <||> DynamicImplicit <$$ keyword "--" <** keyword "->" <**> optional int_lit + <||> DynamicComposition <$$> pDynamic <** keychar ';' <**>>> pDynamic + +pStatic :: Parser Static +pStatic = "STATIC" + <:=> StaticExplicit <$$ keyword "==" <**> multipleSepBy1 pPolarEntTerm (keychar ',') + <** keyword "=>" + <||> StaticImplicit <$$ keyword "==" <** keyword "=>" + +pArrow :: Parser Arrow +pArrow = "ARROW" + <:=> AStatic <$$ keyword "==" <** keyword "=>" + <||> ADynamic <$$ keyword "--" <** keyword "->" + +pPred :: Parser Pred +pPred = "PRED" + <:=> PredType <$$ keychar ':' <**> pTerm + <||> PredSubType <$$ keyword "<:" <**> pTerm + +pPhrasePatt :: Parser PhrasePatt +pPhrasePatt = "PHRASE-PATT" + <:=> keyword "[[" **> pWordPatts <** keyword "]]" + +pWordPatts :: Parser [WordPatt] +pWordPatts = many pWordPatt + +pWordPatt :: Parser WordPatt +pWordPatt = "WORD-PATT" + <::=> WPVar <$$> pVar + <||> WPAtom <$$> atom_lit + <||> WPGroup <$$> parens pWordPatts + <||> parens (WPUnion <$$> atom_lit <** keychar '|' <**> + manySepBy1 atom_lit (keychar '|')) diff --git a/src/Parsing/Spec.hs b/src/Parsing/Spec.hs new file mode 100644 --- /dev/null +++ b/src/Parsing/Spec.hs @@ -0,0 +1,161 @@ +{-# LANGUAGE TupleSections #-} + +module Parsing.Spec where + +import Parsing.Term +import Parsing.Mutual +import Parsing.Rule +import Parsing.Syntax +import Types.ConcreteSyntax + +import CCO.Component + +import GLL.Combinators + + +parser :: Component [Token] CBSFile +parser = component (return . head . parseWithOptions [throwErrors, maximumPivot] pCBS) + +pCBS :: Parser CBSFile +pCBS = "CBS-FILE" + <:=> optional (keyword "Language" <** string_lit) **> pManySpecs + +pManySpecs :: Parser [CBSSpec] +pManySpecs = "MANY-SPECS" + <::=> (:) <$$> pComment <**> pManySpecs --comments + <||> id <$$ keyword "Assert" <** pPremise <**> pManySpecs -- discard assertions + <||> id <$$ keyword "Built-in" <** pSpec <**> pManySpecs -- ignore built-ins + <||> (:) <$$> pSpec <**> pManySpecs + <||> id <$$ brackets (multiple pRef) <**> pManySpecs + <||> satisfy [] + +pRef :: Parser String +pRef = "RefKindName" <:=> pKind <** id_lit + +pSpec :: Parser CBSSpec +pSpec = "SPEC" + <::=> keyword "Auxiliary" **> pSpec + <||> pFuncon + <||> pSyntaxSpec + <||> pSemanticsSpec + <||> RuleSpec <$$> pRuleSpec + <||> AliasSpec <$$ keyword "Alias" <**> id_lit <** keychar '=' <**> id_lit + <||> OtherwiseSpec <$$ keyword "Otherwise" <**> pRule + <||> TypeSpec <$$ keyword "Type" <**> id_lit <**> optional pParams <**> multiple pBounded <**> optional pDefRewrite + <||> DatatypeSpec <$$ keyword "Datatype" <**> id_lit <**> optional pParams <**> + optional pBounded <**> optionalWithDef (keyword "::=" **> pDataAlts) [] + <||> EntitySpec <$$ keyword "Entity" <**> pEntityDecl + <||> MetaVariablesSpec . concat <$$ keyword "Meta-variables" <**> (many1 pVarDecl) + +pVarDecl :: Parser [VarDecl] +pVarDecl = "VARS-DECL" + <:=> apply <$$> manySepBy1 alt_id_lit (keychar ',') <**> + (Left <$$ keyword "<:" <**> pTerm <||> + Right <$$ keychar ':' <**> pTerm) + where apply vars (Left ty) = map (flip VarDeclSubType ty) vars + apply vars (Right ty) = map (flip VarDeclType ty) vars + +pFuncon :: Parser CBSSpec +pFuncon = "FUNCON" + <::=> build_funcon <$$ keyword "Funcon" <**> id_lit + <**> optional pParams + <** keychar ':' + <**> pTerm + <**> optional pDefRewrite + where build_funcon nm mparams cs = FunconSpec nm mparams cs + +pSemanticsSpec :: Parser CBSSpec +pSemanticsSpec = "SEMANTICS" + <:=> SemanticsSpec <$$ keyword "Semantics" <**> name_lit <** keyword "[[" <**> + pVar <** keychar ':' <**> pPhraseType <** keyword "]]" <**> + optional pParams <** keychar ':' <**> pTerm <**> optional pDefEqual + +-- ambiguity "(X:T,Y:T) +-- alternative interpretation: +pParams :: Parser Params +pParams = "PARAMS" + <::=> keychar '(' **> multipleSepBy pParam (keychar ',') <** keychar ')' + +pParam :: Parser Param +pParam = "PARAM" + <::= Param <$$> pVar <**> optional pBounded + +pDefEqual :: Parser DefEqual +pDefEqual = "DEFINED-EQUAL" <::=> DefEqual <$$ keychar '=' <**> pTerm +pDefRewrite :: Parser DefRewrite +pDefRewrite = "DEFINED-REWRITE" <::=> DefRewrite <$$ keyword "~>" <**> pTerm + +pBounded :: Parser Bounds +pBounded = "BOUNDED" + <:=> InType <$$ keychar ':' <**> pType + <||> Sub <$$ keyword ">:" <**> pType + <||> Sup <$$ keyword "<:" <**> pType + +pDataAlts :: Parser [DatatypeAlt] +pDataAlts = "ALT+ |" <:=> multipleSepBy pDataAlt (keychar '|') + +pDataAlt :: Parser DatatypeAlt +pDataAlt = "ALT" + <:=> AltDots <$$ keyword "..." + <||> Inj <$$ keychar '{' <**> pVar <** keychar ':' <**> pType <** keychar '}' + <||> Cons <$$> id_lit <**> optional pParams + +pEntityDecl :: Parser Entity +pEntityDecl = "ENTITY" + <:=> EntContextual <$$> pEnt <** keyword "|-" <** keychar '_' <**> pArrow + <** keychar '_' + <||> EntMutable <$$> angles ((keychar '_' **> keychar ',') **> pEnt) <**> + pArrow <**> + angles ((keychar '_' **> keychar ',') **> pEnt) + <||> EntObservable <$$ keychar '_' <**> pEntArrow <** keychar '_' + +pEnt :: Parser Ent +pEnt = "ENT" + <:=> EntVarStem <$$> pVarStem <**> optional (pPolarity) + <||> EntName <$$> name_lit <**> optional pPolarity <** + keychar '(' <**> pVar <** keychar ':' <**> pTerm <** keychar ')' + +pEntArrow :: Parser EntArrow +pEntArrow = "ENT-ARROW" + <:=> EADynamic <$$ keyword "--" <**> pEnt <** keyword "->" + <||> EAStatic <$$ keyword "==" <**> pEnt <** keyword "=>" + +pComment :: Parser CBSSpec +pComment = "COMMENT" + <:=> CommentSpec <$$ keyword "/*" <**> multiple pCommentPart <** keyword "*/" + <||> MetaSpec . HS_Imports <$$ keyword "/*HS-IMPORTS" + <**> token "ORDINARY" <** keyword "*/" + +pCommentPart :: Parser CommentPart +pCommentPart = "COMMENT-PART" + <::=> Ordinary <$$> token "ORDINARY" + <||> Asterisk <$$ keychar '*' + <||> At <$$ keychar '@' <**> optionalWithDef (token "SECT-NUM") "" + <||> At <$$> token "SECT-NUM" + <||> CommentTerm <$$ token "TICK" <**> multipleSepBy1 pTerm (keychar ',') <** token "TICK" + <||> CommentPremise <$$ token "TICK" <** token "TICK" <**> pPremise + <** token "TICK" <** token "TICK" + <||> SpecInComment <$$ token "TICK" <** token "TICK" <** token "TICK" + <**> pSpec + <** token "TICK" <** token "TICK" <** token "TICK" + +-- sections +pKind :: Parser String +pKind = "KIND" <:=> + keyword "Funcon" <||> keyword "Type" <||> keyword "Datatype" <||> + keyword "Entity" <||> keyword "Lexis" <||> keyword "Syntax" <||> + keyword "Semantics" <||> keyword "Alias" + +-- related to syntax +pSyntaxSpec :: Parser CBSSpec +pSyntaxSpec = "SYNTAX-SPEC" + <:=> SyntaxSpec <$$ keyword "Syntax" <**> multiple1 pProd + <||> LexisSpec <$$ keyword "Lexis" <**> multiple1 pProd + +pProd :: Parser Prod +pProd = "PROD" + <:=> Prod <$$> optionalWithDef (pVarStems) [] <**> pSynName <** + keyword "::=" <**> pAlts + <||> SDFComment [] <$$ keyword "SDF" <** pComment + + diff --git a/src/Parsing/Syntax.hs b/src/Parsing/Syntax.hs new file mode 100644 --- /dev/null +++ b/src/Parsing/Syntax.hs @@ -0,0 +1,41 @@ + +module Parsing.Syntax where + +import Types.ConcreteSyntax + +import Parsing.Mutual + +import GLL.Combinators + +pVarSynName :: Parser VarSynName +pVarSynName = "VAR-SYN-NAME" + <:=> VarName <$$> pVarString <** keychar ':' <**> name_lit + <||> SynName <$$> name_lit + +pVarStems :: Parser [VarStem] +pVarStems = "VAR-STEMS" + <:=> multipleSepBy1 pVarString (keychar ',') <** keychar ':' + +pVarStem :: Parser VarStem +pVarStem = "VAR-STEM" <:=> pVarString + +pAlts :: Parser PhraseType +pAlts = "PT-ALTS" <:=> foldr1 PTUnion <$$> multipleSepBy1 pAlt (keychar '|') + +pAlt :: Parser PhraseType +pAlt = "SINGLE-PT-ALT" <:=> foldr1 PTSeq <$$> multiple1 pPhraseType + +pPhraseType :: Parser PhraseType +pPhraseType = "PHRASE-TYPE" + <::=> PTSynName <$$> pSynName + <||> atom_or_range <$$> atom_lit <**> optional (keychar '-' **> atom_lit) + <||> PTComplement <$$ keychar '~' <**> pPhraseType + <||> flip ($) <$$> pPhraseType <**> pPhraseTypeRest + <||> PTGroup <$$> parens (optional pAlts) + where atom_or_range a1 (Just a2) = PTRange a1 a2 + atom_or_range a1 Nothing = PTAtom a1 + +pPhraseTypeRest :: Parser (PhraseType -> PhraseType) +pPhraseTypeRest = "REST-PHRASE-TYPE" + <::=> flip PTPostfix <$$> pPostfix + <||> flip PTNoLayout <$$ keychar '_' <**> pPhraseType diff --git a/src/Parsing/Term.hs b/src/Parsing/Term.hs new file mode 100644 --- /dev/null +++ b/src/Parsing/Term.hs @@ -0,0 +1,97 @@ + +module Parsing.Term where + +import Parsing.Mutual +import Types.ConcreteSyntax + +import GLL.Combinators + +pType :: Parser Type +pType = "TYPE" <:=> pTerm + +-- ambiguity: +-- S=>T (alternative interpretation S applied to =>) +pTerm :: Parser Term +pTerm = "TERM" + <::= SemanticsApp <$$> name_lit <**> pPhraseTerm <**> optional pTerm + <||> TermConst <$$> pConst + <||> TermVar <$$> pVar + <||> TermDots <$$ keyword "..." + <||> TermName <$$> name_lit + -- ambiguity "X:T,Y:T" (non-associative, no nesting) + <||> Typed <$$> pTerm <** keychar ':' <**> pType + <||> Computes <$$ keyword "=>" <**> pType + <||> ComputesFrom <$$> pType <** keyword "=>" <**> pType + <||> TermComplement <$$ keychar '~' <**> pTerm + <||> TermPostfix <$$> pType <**> pPostfix + <||> TermUnion <$$> pTerm <** keychar '|' <**>>> pTerm + <||> TermInter <$$> pTerm <** keychar '&' <**>>> pTerm + <||> termTuple <$$ keychar '(' <**> pTerms <** keychar ')' + <||> TermList <$$ keychar '[' <**> pTerms <** keychar ']' + <||> TermSet <$$ keychar '{' <**> pTerms <** keychar '}' + <||> TermMap <$$ keychar '{' <**> pPoints <** keychar '}' + <||> TermPower <$$> pTerm <** keychar '^' <**> pTerm +-- <||> pTermSeq {- replaced by specific occurrence as rhs of semantics spec -} + <||> NameApp <$$> name_lit <**> pTerm + <||> VarApp <$$> pVar <**> pTerm + <||> double_quote **> pTerm <** double_quote +{- +pTermSeq :: Parser Term +pTermSeq = "TERMS" <::=> + merge <$$> pTerm <**> optional (keychar ',' **> pTermSeq) + <||> satisfy (TermSequence []) + where merge t (Just (TermSequence ts)) = TermSequence (t:ts) + merge t1 (Just t2) = TermSequence [t1,t2] + merge t1 Nothing = t1 +-} +-- obvious ambiguity (associativity) +-- 1,2,3 (why does manySepBy2 not resolve this?) +pTermSeq :: Parser Term +pTermSeq = "TERMSEQ" <:=> shortest_match (TermSequence <$$> multipleSepBy2 pTerm (keychar ',')) + +-- obvious ambiguity (associativity) +-- 1,2,3 (why does manySepBy2 not resolve this?) +-- TODO generalise type argument of first parameter of rassoc? +pTerms :: Parser [Term] +pTerms = "TERMS" <:=> shortest_match (manySepBy pTerm (keychar ',') <** satisfy ()) + +pTermUnions :: Parser [Term] +pTermUnions = "TERMUNIONS" <::=> + (:) <$$> pType <** keychar '|' <**> pTermUnions0 + where pTermUnions0 = "0TERMUNIONS" <:=> + (:[]) <$$> pType + <||> pTermUnions + +pTermInters :: Parser [Term] +pTermInters = "TERM-INTERS" <::=> + (:) <$$> pType <** keychar '&' <**> pTermInters0 + where pTermInters0 = "0TERM-INTERS" <:=> + (:[]) <$$> pType + <||> pTermInters + + +{- +pTermUnions :: Parser [Term] +pTermUnions = "TERMUNIONS" <:=> multipleSepBy1 pType (keychar '|') +-} + +-- | Key-Value pairs of terms in a map +-- pair is optional, can be given as ... +pPoints :: Parser [Maybe (Term, Term)] +pPoints = "POINTS" <:=> multipleSepBy1 pPair (keychar ',') + where pPair :: Parser (Maybe (Term, Term)) + pPair = "PAIR" <:=> (Just .) . (,) <$$> pTerm <** keyword "|->" <**> pTerm + <||> Nothing <$$ keyword "..." + +pPhraseTerm :: Parser PhraseTerm +pPhraseTerm = "PHRASE-TERM" + <:=> keyword "[[" **> pWordTerms <** keyword "]]" + +pWordTerms :: Parser [WordTerm] +pWordTerms = many pWordTerm + +pWordTerm :: Parser WordTerm +pWordTerm = "WORD-TERM" + <::=> WTVar <$$> pVar + <||> WTAtom <$$> atom_lit + <||> WTGroup <$$> parens pWordTerms diff --git a/src/Print/HaskellModule.hs b/src/Print/HaskellModule.hs new file mode 100644 --- /dev/null +++ b/src/Print/HaskellModule.hs @@ -0,0 +1,572 @@ +{-# LANGUAGE LambdaCase #-} +-- many opportunities for small optimisations +-- e.g. do not apply (map text), gList, nameOfSig, stepTypeOfSig, etc. multiple times +module Print.HaskellModule where + +import Funcons.EDSL (Funcons(..),DataTypeMembers(..), f2vPattern) + +import Print.Util +import Types.ConcreteSyntax (showConcreteTerm) +import Types.SourceAbstractSyntax hiding (CBSFile(..),CBSSpec(..),FunconSpec(..),FSig,FStep,FPremiseStep,FValueSorts(..),Name,FValueSort(..),EntitySpec(..),FSideCondition(..),DataTypeSpec(..),FTerm(..),DataTypeAlt(..),FValSorts(..),FPattern(..), CommentPart(..)) +import Types.CoreAbstractSyntax hiding (Lazy, Strict, CBSFile(..),CBSSPec(..),FunconSpec(..),FRewriteRule(..),FPremiseStep(..),FStep(..),FStepRule(..), DataTypeSpec(..), DataTypeAlt(..)) +import qualified Types.CoreAbstractSyntax as C +import Types.FunconModule as F +import Types.TargetAbstractSyntax (InputAccess(..)) + +import CCO.Component + +import Prelude hiding ((<$>)) + +import Control.Monad (unless) +import Data.Maybe (catMaybes) +import Data.List(intercalate, findIndices) +import Data.List.Split (splitOn) +import Data.Char (toUpper, isUpper, toLower) +import Text.PrettyPrint.HughesPJ +import Data.Text(pack,unpack) + +import System.FilePath hiding ((<.>)) +import qualified System.FilePath as FP +import System.Directory (createDirectoryIfMissing, doesFileExist) + +type Name = String +type StepName = Name -- name of a step function + +cbs2module :: FilePath -> Maybe FilePath -> Maybe String -> + Component FunconModule (Maybe (IO ())) +cbs2module cbsfile msrcdir mlang = component (\cbsfile -> return $ + let mfiledoc = fmap ((gHeader modName $+$)) $ + gFile (aliases cbsfile) + (funcons cbsfile) + (entities cbsfile) + (datatypes cbsfile) + + in (fmap doPrint mfiledoc)) + where render' filedoc = render (text "-- GeNeRaTeD fOr:" <+> text cbsfile $+$ filedoc) + doPrint doc = case (msrcdir, mlang) of + (Just srcdir, Just lang) -> do + main_exists <- doesFileExist (srcdir "Main.hs") + unless main_exists $ do + createDirectoryIfMissing False srcdir + writeFile (srcdir "Main.hs") main_contents + putStrLn "Generated Main.hs" + createDirectoryIfMissing True hs_file_dir + writeFile hs_file (render' doc) + putStrLn ("Generated " ++ hs_file) + where hs_file_dir = srcdir foldr () "" hs_file_dir_as_list + hs_file = hs_file_dir hs_file_name FP.<.> "hs" + main_contents = "import Funcons.Tools (mkMainWithLibraryEntitiesTypes)\n\ + \import Funcons." ++ camelcase lang ++ ".Library\n" + (Just srcdir, _) -> do + writeFile (srcdir hs_file_name FP.<.> "hs") (render' doc) + putStrLn ("Generated " ++ (hs_file_name FP.<.> "hs")) + _ -> putStrLn (render' doc) --simply print to stdout + lang = maybe "Core" id mlang + modName = case mlang of Nothing -> Nothing + _ -> Just (intercalate "." modNameAsList) + modNameAsList = hsmodNameFromPath lang cbsfile + hs_file_name = last modNameAsList + hs_file_dir_as_list = init modNameAsList + +gHeader :: Maybe String -> Doc +gHeader mmodname = vsep $ + [text "{-# LANGUAGE" <+> text "OverloadedStrings" <+> text "#-}"] ++ + (maybe [] (\nm -> [text "module" <+> text nm <+> text "where"]) mmodname) ++ + [text "import" <+> text "Funcons.EDSL" + ,text "import" <+> text "Funcons.Operations" <+> text "hiding" <+> parens (text "Values" <> comma <> text "libFromList")] ++ + (maybe [text "import" <+> text "Funcons.Tools"] (const []) mmodname) + +gFile :: AliasMap -> [FunconSpec] -> [EntitySpec] -> [DataTypeMembers] -> Maybe Doc +gFile als fspecs especs dspecs + | null fspecs && null especs && null dspecs = Nothing + | otherwise = Just $ + vsep $ + [text fEntities <=> gList [] -- {- defaults have been removed from beta -} + ,text fTypes <=> text ftypeEnvFromList $+$ + nest 4 (gList (concatMap (gTypes als) dspecs)) + ,text fFuncons <=> text fLibFromList $+$ + nest 4 (gList lib_entries)] + ++ map (gStep als) fspecs +-- ++ concatMap (\(DataTypeDecl _ _ alts) -> map gCons alts) dspecs + ++ map gData dspecs + where lib_entries = concatMap (gLibF als) fspecs + ++ concatMap (gLibD als) dspecs +-- ++ concatMap (gLibC als) dspecs + + gLibF :: AliasMap -> FunconSpec -> [Doc] + gLibF als (F.FunconSpec name sig _ _ _) = + [ gTuple [gString alias + ,gStepType steptype <+> text (stepName name)] + | alias <- my_aliases name als ] + where steptype = stepTypeOfSig sig + + gLibD :: AliasMap -> DataTypeMembers -> [Doc] + gLibD als (DataTypeMemberss _ _ []) = [] + gLibD als (DataTypeMemberss nm tyargs _) = + [ gTuple [gString alias + ,gStepType steptype <+> text (stepName (unpack nm))] + | alias <- my_aliases (unpack nm) als ] + where steptype | null tyargs = Nullary + | otherwise = Strict + +gData :: DataTypeMembers -> Doc +gData (DataTypeMemberss nm' tyargs _) = + text (smart_cons_name nm) <=> smart_body $+$ + text sname <+> tyarg_pat <=> main + where nm = unpack nm' + sname = stepName nm + main = text frewriteType <+> gString nm <+> tyarg + tyarg_pat | null tyargs = empty + | otherwise = text "ts" + tyarg | null tyargs = brackets empty + | otherwise = text "ts" + smart_body + | null tyargs = text cFunconName <+> gString nm + | otherwise = text cFunconApp <+> gString nm + +{- +gCons :: DataTypeAlt -> Doc +gCons (DataTypeInclusion _) = empty +gCons (DataTypeConstructor nm args strictns) = + text (smart_cons_name nm) <=> smart_body $+$ + text sname <+> args_pat <=> main + where args_pat | null args = empty + | otherwise = text "fs" + sname = stepName nm + main = text fRewritten <+> parens return_val + where return_val = text cADTVal <+> gString nm <+> arg + where arg | null args = brackets empty + | all isStrict strictns = + parens (text "fvalues" <+> text "fs") + | otherwise = text "fs" + smart_body = case args of + [] -> text cFunconName <+> gString nm + _ -> text cFunconApp <+> gString nm +-} + +gStep :: AliasMap -> FunconSpec -> Doc +gStep als fspec@(F.FunconSpec fname fsig mdoc r_rules s_rules) = + ppMaybeDoc mdoc $+$ + vcat [ text (smart_cons_name name) <+> smart_fargs_var <=> smart_body + | name <- my_aliases fname als ] $+$ + case steptype of + Nullary -> text sname <=> main $+$ whereClause + _ -> text sname <+> text fargs_var <+> text "=" $+$ + nest 4 main $+$ + whereClause + where sname = stepName fname + steptype = stepTypeOfSig fsig + nullary = case steptype of Nullary -> True + _ -> False + smart_fargs_var | nullary = empty + | otherwise = text "fargs" + smart_body = case steptype of + Nullary -> text cFunconName <+> gString fname + _ -> gFunconApp fname (text fargs_var) + + + main | null r_rules && null s_rules = text fNorule <+> selfApp + --TODO ignore rewrites or steps if null + | otherwise = text fEvalRules <+> + mkList "rewrite" [1..length r_rules] <+> + mkList "step" [1..length s_rules] + where mkList str = gList . map (\i -> text (str ++ show i)) + + args = case steptype of + Lazy i is _ -> generateArgs i + _ -> error "fargs_var only specified for lazy funcons" + + selfApp = parens $ case steptype of + Nullary -> text cFunconName <+> gString fname + Strict -> gFunconApp fname (parens (text ffvalues <+> text fargs_var)) + _ -> gFunconApp fname (text fargs_var) + + whereClause | null r_rules && null s_rules = empty + | otherwise = nest 4 (text "where" <+> nest 2 + (rewriteRules (zip [1..] r_rules) $+$ + stepRules (zip [1..] s_rules))) + + rewriteRules :: [(Int, [FRewriteStmt])] -> Doc + rewriteRules rules = vcat (map rewriteRule rules) + rewriteRule (idx, stmts) = rule $ initEnv $+$ + vcat (map (ppRewriteStmt steptype False) stmts) + where rule :: Doc -> Doc + rule = ppDoBinding (text ("rewrite" ++ show idx)) [] + + stepRules :: [(Int, [FStepStmt])] -> Doc + stepRules rules = vcat (map (stepRule) rules) + stepRule (idx, stmts) = rule $ initEnv $+$ ppStepStmts steptype stmts + where + rule = ppDoBinding (text ("step" ++ show idx)) [] + + initEnv = text "let" <+> text env_var <=> text empty_env + +ppDoBinding :: Doc -> [Doc] -> Doc -> Doc +ppDoBinding nm args body = nameWithArgs <=> text "do" $$ nest 2 body + where nameWithArgs = hsep (nm : args) + +ppLetDoBinding :: Doc -> [Doc] -> Doc -> Doc +ppLetDoBinding nm args body = text "let" <+> ppDoBinding nm args body + +ppBranches rec fnm bs = + vcat (zipWith printLet [1..] bs) $+$ + text fnm <+> gList (zipWith printCall [1..] bs) + where printLet i b = ppLetDoBinding (printCall i b) [] + (vcat (map rec b)) + printCall i b = text ("branch" ++ (show i)) <+> text env_var + +ppRewriteStmt :: StepType -> Bool -> FRewriteStmt -> Doc +ppRewriteStmt stype lift stmt = case stmt of + RBranches bs -> ppBranches (ppRewriteStmt stype False) "rewriteRules" bs + ArgsPattern _ _ | Nullary <- stype -> empty + ArgsPattern var pats -> + text env_var <<-> text matcher <+> text var <+> ppPatterns pats <+> text env_var + EnvStore var term -> + text env_var <<-> text envStore <+> gString var <+> parens (ppTerm term) <+> text env_var + EnvRewrite var -> text env_var <<-> text envRewrite <+> gString var <+> text env_var + CheckSideCondition side -> ppSideCondition checker side + where checker | lift = lifted_fSideCondition + | otherwise = fSideCondition + RewriteTarget term -> text fRewTermTo <+> parens (ppTerm term) <+> text env_var + where matcher | strict, lift = fliftvsMatch + | strict = fvsMatch + | lift = fliftfsMatch + | otherwise = ffsMatch + ppPatterns | strict = ppVPatterns + | otherwise = ppFPatterns + envRewrite | lift = fliftEnvRewrite + | otherwise = fEnvRewrite + envStore | lift = fliftEnvStore + | otherwise = fEnvStore + strict = stepTypeStrict stype + +ppStepStmts :: StepType -> [FStepStmt] -> Doc +ppStepStmts stype = vcat . map (ppStepStmt stype) + +ppStepStmt :: StepType -> FStepStmt -> Doc +ppStepStmt stype = ppStepStmt' True + where + ppStepStmt' nocont stmt = case stmt of + SBranches bs -> ppBranches (ppStepStmt stype) "stepRules" bs + PremiseBlock s -> ppStepStmt' nocont s + StepTarget term -> text fStepTermTo <+> parens (ppTerm term) <+> text env_var + ReadInherited nm pats -> readInh nm pats + ReadInput nm pats -> readInputs nm pats + WriteMutable nm term -> writeMutable nm term + ReadMutable nm pat -> readInhMut fgetMUTPatt nm pat + WriteOutput nm term -> writeOutput nm term + WriteControl nm mterm -> writeControl nm mterm + -- these stmts are applied to a continuation + -- the first of which should receive the env (e.g. env <- ...) + ScopeInherited nm term cont -> + (if nocont then receive_result else id) $ + text fWithINHTerm <+> gString nm <+> parens (ppTerm term) <+> + text env_var <$> ppStepStmt' False cont + ScopeInput nm terms acc cont -> + (if nocont then receive_result else id) $ + text withInput <+> gString nm <+> + gList (map ppTerm terms) <+> text env_var <$> ppStepStmt' False cont + where withInput = case acc of + ExactInput -> fwithExactInput + ExtraInput -> fwithExtraInput + ScopeDownControl nm mterm cont -> + (if nocont then receive_result else id) $ + text fWithCTRLTerm <+> gString nm <+> parens (ppMaybeTerm mterm) <+> + text env_var <$> ppStepStmt' False cont + ReceiveControl nms cont | nocont -> + gTuple [text env_var, gList (map sig_var nms)] <<-> + text "receiveSignals" <+> gList (map gString nms) <$> ppStepStmt' False cont + | otherwise -> error "assert ppStepStmt ReceiveControl" + ReadControl nm mpat -> + (if nocont then receive_result else id) $ + text "receiveSignalPatt" <+> sig_var nm <+> + parens (ppMVPattern mpat) <+> text env_var + ReadDownControl nm mpat -> + text env_var <<-> text fgetDCTRLPatt <+> gString nm <+> parens (ppMaybeVPattern mpat) <+> text env_var + ReceiveOutput nm pat cont -> + (if nocont then receive_result else id) $ + text freadOUTPatt <+> gString nm<+> + parens (ppVPattern pat) <$> ppStepStmt' False cont + FRewriteStmt stmt -> ppRewriteStmt stype True stmt + Premise term pats -> + (if nocont then receive_result else id) $ + text fpremise <+> parens (ppTerm term) <+> + (ppFPatterns pats) <+> text env_var + where receive_result :: Doc -> Doc + receive_result doc = text env_var <<-> doc + + sig_var sigNm = text ("__var" ++ var2id sigNm) + +gTypes :: AliasMap -> DataTypeMembers -> [Doc] +gTypes alt (DataTypeMemberss nm' params []) = [] +gTypes als (DataTypeMemberss nm' params alts) = + [ gTuple [gString alias, gType (DataTypeMemberss (pack alias) params alts)] + | alias <- my_aliases nm als ] + where nm = unpack nm' + gType :: DataTypeMembers -> Doc + gType = text . show + +readInputs :: Name -> [FPattern] -> Doc +readInputs nm pats = vcat (map readInput pats) + where readInput pat = text env_var <<-> text fmatchInput <+> + gString nm <+> parens (ppVPattern pat) <+> text env_var + +readInh :: Name -> [FPattern] -> Doc +readInh nm pat = text env_var <<-> text fgetINHPatt <+> + gString nm <+> ppVPatterns pat <+> text env_var + +readInhMut :: String -> Name -> FPattern -> Doc +readInhMut entitytype nm pat = text env_var <<-> text entitytype <+> + gString nm <+> parens (ppVPattern pat) <+> text env_var + +writeMutable :: Name -> FTerm -> Doc +writeMutable nm term = text fputMUTTerm <+> gString nm <+> + parens (ppTerm term) <+> text env_var + +writeControl :: Name -> (Maybe FTerm) -> Doc +writeControl nm mterm = case mterm of + Nothing -> empty + Just term -> text fraiseTerm <+> gString nm <+> + parens (ppTerm term) <+> text env_var + +writeOutput :: Name -> FTerm -> Doc +writeOutput nm term = text fwriteOUTTerm <+> gString nm <+> + parens (ppTerm term) <+> text env_var + +ppFuncons :: Funcons -> Doc +ppFuncons f = text (show f) + +ppMaybeTerm :: Maybe FTerm -> Doc +ppMaybeTerm = text. show + +-- | Sequence operators are ignore in pattern annotations +ppSort :: FTerm -> Doc +ppSort (TSortSeq sort op) = ppSort sort +ppSort term = ppTerm term + +ppTerm :: FTerm -> Doc +ppTerm term = text (show term) + +ppSideCondition :: String -> FSideCondition -> Doc +ppSideCondition checker sc = text env_var <<-> text checker <+> parens cond <+> text env_var + where cond = case sc of + SCEquality term1 term2-> text cSCEquality <+> + parens (ppTerm term1) <+> parens (ppTerm term2) + SCInequality term1 term2-> text cSCInequality <+> + parens (ppTerm term1) <+> parens (ppTerm term2) + SCIsInSort term1 sort -> text cSCIsInSort <+> + parens (ppTerm term1) <+> parens (ppTerm sort) + SCNotInSort term1 sort -> text cSCNotInSort <+> + parens (ppTerm term1) <+> parens (ppTerm sort) + SCPatternMatch term pats -> text cSCPatternMatch <+> + parens (ppTerm term) <+> ppVPatterns pats + -- We no longer allow this + -- SCPatternMismatch term pat -> text cSCPatternMismatch <+> + -- parens (ppTerm term) <+> parens (ppVPattern pat) + +ppMaybeDoc :: Maybe [CommentPart] -> Doc +ppMaybeDoc Nothing = empty +ppMaybeDoc (Just cs) = text "-- |" $+$ + vcat (map ((text "-- " <>) . text) (lines (concatMap ppCommentPart cs))) + +ppCommentPart :: CommentPart -> String +ppCommentPart cp = case cp of + Ordinary c -> c + Asterisk -> "*" + At s -> "@" ++ s + CommentTerm ts -> "`" ++ intercalate "," (map showConcreteTerm ts) ++ "`" + CommentPremise p -> "" + SpecInComment s -> "\n" ++ show s ++ "\n" + +ppMVPattern :: Maybe FPattern -> Doc +ppMVPattern Nothing = text cNothing +ppMVPattern (Just pat) = text cJust <$> ppVPattern pat + +ppVPattern :: FPattern -> Doc +ppVPattern = text . show . f2vPattern + +ppVPatterns :: [FPattern] -> Doc +ppVPatterns pats = gList (map ppVPattern pats) + +ppFPatterns :: [FPattern] -> Doc +ppFPatterns pats = gList (map ppFPattern pats) + +ppMaybeVPattern :: Maybe FPattern -> Doc +ppMaybeVPattern Nothing = text "Nothing" +ppMaybeVPattern (Just pat) = text "Just" <+> parens (ppVPattern pat) + +ppFPattern :: FPattern -> Doc +ppFPattern = text . show + +-- | +-- Fake a curried smart constructor for the given funcon (name). +-- useful for congruence rules and other helpers that require a +-- smart constructor argument. +gFunconApp :: Name -> Doc -> Doc +gFunconApp nm args = text cFunconApp <+> gString nm <+> parens args + +stepName :: Name -> Name +stepName = stepName' . var2id + where stepName' "" = error "empty name" + stepName' (hd:tl) = "step" ++ (toUpper hd : tl) + +-- gathering information +data StepType = Strict + | Lazy Int [Int] (Maybe Strictness)-- number of args + indices of value-arguments + | Nullary + +stepTypeStrict :: StepType -> Bool +stepTypeStrict Strict = True +stepTypeStrict _ = False + +gStepType Strict = text cStrictF +gStepType Nullary = text cNullaryF +gStepType (Lazy args stricts mstrict) + | null stricts, Nothing <- mstrict = text cNonStrictF + | otherwise = text cPartialLazyF <+> gList (map rep [0..args-1]) + <+> (maybe (text cNonStrict) op mstrict) + where rep i | i `elem` stricts = op C.Strict + | otherwise = op C.Lazy + op C.Strict = text cStrict + op C.Lazy = text cNonStrict + +stepTypeOfSig :: FSig -> StepType +stepTypeOfSig FStrict = Strict +stepTypeOfSig FLazy = Lazy 0 [] Nothing +stepTypeOfSig FNullary = Nullary +stepTypeOfSig (FPartiallyLazy ss ms) = Lazy (length ss) noncomputing ms + where noncomputing = findIndices needsCongruence ss + +needsCongruence :: Strictness -> Bool +needsCongruence C.Lazy = False +needsCongruence C.Strict = True + +hsid :: Name -> Doc +hsid = text . var2id + +var2id [] = [] +var2id ('-':cs) = '_' : var2id cs +var2id (c:cs) | isUpper c = toLower c : var2id cs + | otherwise = c : var2id cs + +generateArgs :: Int -> [MetaVar] +generateArgs max = foldr op [] [1..max] + where op idx terms = ("arg" ++ show idx):terms + +smart_cons_name nm = intercalate "_" (splitOn "-" nm) ++ "_" + +-- function names +cType = "Type" +cComps = "ComputationType" +cValue = "FValue" +cFunconName = "FName" +cFunconApp = "FApp" +cTupleNot = "FTuple" +cListNot = "FList" +cMapNot = "FMap" +cSetNot = "FSet" +cStrictF = "StrictFuncon" +cStrict = "Strict" +cNonStrictF = "NonStrictFuncon" +cNonStrict = "NonStrict" +cPartialLazyF = "PartiallyStrictFuncon" +cNullaryF = "NullaryFuncon" +cTupleType = "Tuples" +cFVar = "TVar" +cFApp = "TApp" +cFName = "TName" +cFList = "TList" +cChar = "Char" +cFMap = "FMap" +cFSet = "FSet" +cTFuncon = "TFuncon" +cFSortUnion = "FSortUnion" +cFSortComputes = "FSortComputes" +cFSortComputesFrom = "FSortComputesFrom" +cString = "String" +cFloat = "Float" +cNat = "Nat" +cPValue = "PValue" +cPSeqVar = "PSeqVar" +cPMetaVar = "PMetaVar" +cPWildCard = "PWildCard" +cVPLit = "VPLit" +cVPWildCard = "VPWildCard" +cVPSeqVar = "VPSeqVar" +cPADT = "PADT" +cPList = "PList" +cPTuple = "PTuple" +cVPMetavar = "VPMetaVar" +cPAnnotated = "PAnnotated" +cVPAnnotated = "VPAnnotated" +cSCEquality = "SCEquality" +cSCInequality = "SCInequality" +cSCIsInSort = "SCIsInSort" +cSCNotInSort = "SCNotInSort" +cSCPatternMatch = "SCPatternMatch" +cSCPatternMismatch = "SCPatternMismatch" +cDefMutable = "DefMutable" +cDefInherited = "DefInherited" +cDefInput = "DefInput" +cDefOutput = "DefOutput" +cDefControl = "DefControl" +cFStarOp = "StarOp" +cFPlusOp = "PlusOp" +cFQuestionMarkOp = "QuestionMarkOp" +cADTVal = "ADTVal" +cADTType = "ADT" +cDataTypeMembers = "DataTypeMembers" +--TODO can we use show and read? +cDataTypeInclusion = "DataTypeInclusion" +cDataTypeConstructor = "DataTypeConstructor" + +lifted_fSideCondition = "lifted_sideCondition" +fSideCondition = "sideCondition" +fSubsEval = "subsAndRewrite" +fliftfsMatch = "lifted_fsMatch" +fliftvsMatch = "lifted_vsMatch" +fliftvMatch = "lifted_vMatch" +fliftvMaybeMatch = "lifted_vMaybeMatch" +ffsMatch = "fsMatch" +fvsMatch = "vsMatch" +fvMatch = "vMatch" +fvMaybeMatch = "vMaybeMatch" +fRewritten = "rewritten" +fRewTo = "rewriteTo" +fRewTermTo = "rewriteTermTo" +fStepTo = "stepTo" +fStepTermTo = "stepTermTo" +fEvalRules = "evalRules" +fNorule = "norule" +fSortErr = "sortErr" +fApplyFuncon = "applyFuncon" +fCongruence = "congruence" +fAfterRewrite = "afterRewrite" +fFuncons= "funcons" +fEntities = "entities" +fTypes = "types" +fLibFromList = "libFromList" +ftypeEnvFromList = "typeEnvFromList" +fIsVal = "isVal" +fHasStep = "hasStep" +fpremise = "premise" +fgetDCTRLPatt = "getControlPatt" +fgetINHPatt = "getInhPatt" +fgetMUTPatt = "getMutPatt" +fputMUTTerm = "putMutTerm" +fWithINHTerm = "withInhTerm" +fWithCTRLTerm = "withControlTerm" +fraiseTerm = "raiseTerm" +fwriteOUTTerm = "writeOutTerm" +freceiveSignalPatt = "receiveSignalPatt" +freadOUTPatt = "readOutPatt" +fTypes_unval = "types_unval" +ffvalues = "map FValue" +fmatchInput = "matchInput" +frewriteType = "rewriteType" +fwithExactInput = "withExactInputTerms" +fwithExtraInput = "withExtraInputTerms" +fliftEnvStore = "lifted_envStore" +fliftEnvRewrite = "lifted_envRewrite" +fEnvStore = "envStore" +fEnvRewrite = "envRewrite" diff --git a/src/Print/Util.hs b/src/Print/Util.hs new file mode 100644 --- /dev/null +++ b/src/Print/Util.hs @@ -0,0 +1,142 @@ +{-# LANGUAGE LambdaCase #-} + +module Print.Util where + +import Types.SourceAbstractSyntax (SeqSortOp(..)) +import Types.CoreAbstractSyntax + +import Data.List (intersperse, intercalate) +import Data.List.Split +import Data.Char (toUpper) +import Data.Text (Text, unpack) +import Text.PrettyPrint.HughesPJ + +import Funcons.EDSL (Funcons(..)) + +import System.FilePath (splitDirectories, dropFileName, dropExtension, takeBaseName) + + +text' :: Text -> Doc +text' = text . unpack + +gList :: [Doc] -> Doc +gList = brackets . hcat . punctuate comma + +gTuple :: [Doc] -> Doc +gTuple = parens . hcat . punctuate comma + +gAngle :: [Doc] -> Doc +gAngle = angles . hcat . punctuate comma + where angles d = text "<" <> d <> text ">" + +gString :: String -> Doc +gString = doubleQuotes . text + +ppSortOp :: SeqSortOp -> Doc +ppSortOp PlusOp = text "+" +ppSortOp StarOp = text "*" +ppSortOp QuestionMarkOp = text "?" + +gMaybe :: Maybe Doc -> Doc +gMaybe Nothing = text cNothing +gMaybe (Just d) = text cJust <+> parens d +cNothing = "Nothing" +cJust = "Just" + +camelcase :: String -> String +camelcase str = concatMap firstToCap (splitOneOf " -" str) + where firstToCap [] = [] + firstToCap (hd:tl) = (toUpper hd):tl + +dropUntil :: (a -> Bool) -> [a] -> [a] +dropUntil prop xs = + case dropWhile prop xs of + [] -> xs + xs' -> dropUntil prop (tail xs') + +replace :: String -> String -> String -> String +replace f t orig = intercalate t (splitOn f orig) + +infixl 6 <.> +infixl 6 <$> +infixl 6 <=> +infixl 6 <->> +infixl 6 <<-> +d1 <$> d2 = d1 <+> parens d2 +d1 <=> d2 = d1 <+> text "=" <+> d2 +d1 <->> d2 = d1 <+> text "->" <+> d2 +d1 <<-> d2 = d1 <+> text "<-" <+> d2 +(<.>) :: Doc -> Doc -> Doc +d1 <.> d2 = d1 <> text "." <> d2 +vsep = vcat . intersperse (text "") + +{- +termHasVar :: FTerm -> Bool +termHasVar = \case + TVar _ -> True + TName nm -> False + TApp nm term -> any termHasVar term + TSeq terms -> any termHasVar terms + TSet terms -> any termHasVar terms + TMap terms -> any termHasVar terms + TList terms -> any termHasVar terms + TFuncon f -> False + TSortSeq term op -> termHasVar term + TSortUnion ty1 ty2 -> termHasVar ty1 || termHasVar ty2 + TSortInter ty1 ty2 -> termHasVar ty1 || termHasVar ty2 + TSortComplement ty -> termHasVar ty + TSortComputes term -> termHasVar term + TSortComputesFrom from to -> termHasVar from || termHasVar to + TAny -> False + +staticSubstitute :: FTerm -> Funcons +staticSubstitute = \case + TVar "_" -> FValue VAny + TVar var -> error ("failed to apply static substitution to: " ++ var) + TName nm -> FName nm + TApp nm term -> FApp nm (map staticSubstitute term) +-- TSeq terms -> map staticSubstitute terms + TSet terms -> FSet (map staticSubstitute terms) + TMap terms -> FMap (map staticSubstitute terms) + TList terms -> FList (map staticSubstitute terms) + TFuncon f -> f + TSortSeq term op -> FSortSeq (staticSubstitute term) op + TSortUnion ty1 ty2 -> FSortUnion (staticSubstitute ty1) (staticSubstitute ty2) + TSortInter ty1 ty2 -> FSortInter (staticSubstitute ty1) (staticSubstitute ty2) + TSortComplement ty -> FSortComplement (staticSubstitute ty) + TSortComputes term -> FSortComputes (staticSubstitute term) + TSortComputesFrom from to -> FSortComputesFrom (staticSubstitute from) + (staticSubstitute to) + TAny -> FValue VAny +-} + +funcons2FTerm :: Funcons -> FTerm +funcons2FTerm = \case + FName nm -> TName nm + FApp nm term -> TApp nm (map funcons2FTerm term) +-- FTuple terms -> TTuple (map funcons2FTerm terms) + FSet terms -> TSet (map funcons2FTerm terms) + FMap terms -> TMap (map funcons2FTerm terms) + FBinding t1 t2 -> TBinding (funcons2FTerm t1) (TSeq (map funcons2FTerm t2)) +-- FList terms -> TList (map funcons2FTerm terms) + FSortSeq term op -> TSortSeq (funcons2FTerm term) op + FSortUnion ty1 ty2 -> TSortUnion (funcons2FTerm ty1) (funcons2FTerm ty2) + FSortInter ty1 ty2 -> TSortInter (funcons2FTerm ty1) (funcons2FTerm ty2) + FSortComplement ty -> TSortComplement (funcons2FTerm ty) + FSortComputes term -> TSortComputes (funcons2FTerm term) + FSortComputesFrom from to -> TSortComputesFrom (funcons2FTerm from) + (funcons2FTerm to) + FValue v -> TFuncon (FValue v) + FSortPower ty1 ty2 -> TSortPower (funcons2FTerm ty1) (funcons2FTerm ty2) + +hsmodNameFromPath :: String -> FilePath -> [String] +hsmodNameFromPath lang file = hs_file_dir_as_list ++ [hs_file_name] + where hs_file_name = camelcase (takeBaseName file) + hs_file_dir_as_list = + (["Funcons", camelcase lang] ++) $ + map camelcase $ + dropUntil (not . (\x -> x `elem` roots)) $ + splitDirectories $ + dropFileName $ + dropExtension file + roots = ["Funcons", "Funcons-beta", lang] diff --git a/src/Simplify/ConcreteToAbstract.hs b/src/Simplify/ConcreteToAbstract.hs new file mode 100644 --- /dev/null +++ b/src/Simplify/ConcreteToAbstract.hs @@ -0,0 +1,364 @@ +{-# LANGUAGE FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, TupleSections #-} +{-# LANGUAGE LambdaCase #-} + +module Simplify.ConcreteToAbstract + (cs2as) where + +import Types.ConcreteSyntax +import qualified Types.SourceAbstractSyntax as S + +import CCO.Component +import CCO.Feedback +import CCO.Printing + +import Control.Applicative +import Control.Monad.Except + +import Data.Either (rights) +import Data.Foldable (foldrM) +import qualified Data.Map as M + +instance MonadError String Feedback where + throwError = errorMessage . wrapped + +cs2as :: Bool -> Component CBSFile S.CBSFile +cs2as gen_ph = component (sFile gen_ph) + +sFile :: MonadError String m => Bool -> CBSFile -> m S.CBSFile +sFile gen_ph file = toFile =<< sFilterSpecs gen_ph Nothing file + where toFile (als, vardecls, specs) = do + vts <- forM vardecls $ \decl -> case decl of + VarDeclSubType x t -> (:[]) . (x,) . S.SubTyOf <$> sSort t + VarDeclType x t -> (:[]) . (x,) . S.ElemOf <$> sSort t + return (S.CBSFile specs (M.fromList (concat vts)) (M.fromListWith (++) als)) + +sFilterSpecs :: MonadError String m => + Bool -> (Maybe [CommentPart]) -> [CBSSpec] + -> m ([(Name, [Name])], [VarDecl], [S.CBSSpec]) +sFilterSpecs _ _ [] = return ([], [], []) +sFilterSpecs gen_ph mdoc (f@(FunconSpec _ _ _ _):c@(CommentSpec _):r@(RuleSpec _):rest) + = sFilterSpecs gen_ph mdoc (c:f:r:rest) +sFilterSpecs gen_ph mdoc (spec:specs) = case spec of + -- completely ignore entity declarations (CBS-beta) + EntitySpec _ -> sFilterSpecs gen_ph Nothing specs + FunconSpec _ _ _ (Just (DefRewrite TermDots)) | not gen_ph -> + sFilterSpecs gen_ph Nothing specs + FunconSpec nm _ _ _ -> + let (relatedspecs, otherspecs') = span isRelated specs + otherspecs = aliases ++ otherspecs' + (aliases, rulespecs) = foldr op ([], []) relatedspecs + where op a@(AliasSpec _ _) (as,rs) = (a:as,rs) + op r@(RuleSpec _) (as,rs) = (as,r:rs) + op _ acc = acc + isRelated (AliasSpec _ _) = True + isRelated (CommentSpec _) = True + isRelated spec = isFunconRuleSpec spec + isFunconRuleSpec (RuleSpec r) = case r of + Inference _ conc -> nm == termName (concSource conc) + _ -> False + isFunconRuleSpec _ = False + in do spec <- sSpec spec mdoc (map (\(RuleSpec r) -> r) rulespecs) + (als,decls,specs) <- sFilterSpecs gen_ph Nothing otherspecs + return (als, decls, spec:specs) + CommentSpec parts -> case specs of + ((FunconSpec _ _ _ _):otherspecs) -> sFilterSpecs gen_ph Nothing specs + otherspecs -> sFilterSpecs gen_ph Nothing specs + TypeSpec _ _ _ (Just (DefRewrite TermDots)) + | not gen_ph -> sFilterSpecs gen_ph Nothing specs + LexisSpec _ -> sFilterSpecs gen_ph Nothing specs + SyntaxSpec _ -> sFilterSpecs gen_ph Nothing specs + SemanticsSpec _ _ _ _ _ _ -> sFilterSpecs gen_ph Nothing specs + RuleSpec _ -> sFilterSpecs gen_ph Nothing specs + OtherwiseSpec _ -> sFilterSpecs gen_ph Nothing specs + AliasSpec t f -> do (als, decls, specs) <- sFilterSpecs gen_ph Nothing specs + return ((f,[t]):als,decls,specs) + MetaVariablesSpec ds -> do (als, decls, specs) <- sFilterSpecs gen_ph Nothing specs + return (als, ds++decls,specs) + _ -> do spec <- sSpec spec mdoc [] + (als, decls, specs) <- sFilterSpecs gen_ph Nothing specs + return (als, decls, (spec:specs)) + +sSpec :: MonadError String m => CBSSpec -> (Maybe [CommentPart]) -> [Rule] -> m S.CBSSpec +sSpec spec mdoc rules = case spec of + MetaSpec s -> return (S.MetaSpec s) + Auxiliary s -> sSpec s mdoc rules + FunconSpec nm mparams ty mcs -> do + sig <- buildFSig nm mparams ty mdoc + case mcs of + Just (DefRewrite term) -> S.FunconSpec . S.FAbbrv sig <$> sMaybeTerm term + _ -> S.FunconSpec . S.FRules sig <$> sRules rules + TypeSpec nm mparams _ Nothing -> S.TypeSpec <$> decl + where decl = S.DataTypeDecl nm <$> params <*> return [] + params = maybe (return []) (mapM sValParam) mparams + TypeSpec nm mparams _ tcs -> (S.TypeSynonymSpec <$>) $ case tcs of + Just (DefRewrite ty) -> S.TypeSynonymDecl nm <$> params <*> sSort ty + where params = maybe (return []) (mapM sValParam) mparams + _ -> throwError ("unexpected type synonym: " ++ nm) + DatatypeSpec nm mparams mbound alts -> S.DataTypeSpec <$> decl + where decl = S.DataTypeDecl nm <$> params <*> sAlts alts + params = maybe (return []) (mapM sValParam) mparams + sAlts = mapM sAlt + sAlt alt = case alt of + Inj _ ty -> S.DataTypeInclusion <$> sSort ty + Cons nm mparams -> S.DataTypeConstructor nm <$> mapM sSortOfParam params + where params = maybe [] id mparams + AltDots -> throwError "undefined datatype alternative" + _ -> throwError "unexpected lexis/syntax/semantics specification" + +sSortOfParam :: MonadError String m => Param -> m S.FSort +sSortOfParam p = case p of + Param _ (Just (InType ty)) -> sSort ty + Param _ (Just (Sup ty)) -> sSort ty + _ -> throwError ("unexpected type parameter: " ++ show p) + +sValParam :: MonadError String m => Param -> m S.FParam +sValParam (Param var mbound) = case mbound of + Nothing -> return (mkVar var, Nothing) + Just bound -> case bound of + Sub ty -> (mkVar var,) . Just <$> bValSort ty + Sup ty -> (mkVar var,) . Just <$> bValSort (NameApp "nullabe" (TermName "values")) + InType ty -> (mkVar var,) . Just <$> bValSort ty + where mkVar var = case var of + Nothing -> S.PPAny + Just str -> case last str of + '*' -> S.PPSeqMetaVar str S.StarOp + '?' -> S.PPSeqMetaVar str S.QuestionMarkOp + '+' -> S.PPSeqMetaVar str S.PlusOp + _ -> S.PPMetaVar str + +buildFSig :: MonadError String m => + Name -> Maybe Params -> Term -> Maybe [CommentPart] -> m S.FSig +buildFSig nm mparams ty mdoc = do + params <- maybe (return []) (mapM sValParam) mparams + S.FSig nm params <$> bValSort ty <*> sMDoc mdoc + +sMDoc :: MonadError String m => Maybe [CommentPart] -> m (Maybe [S.CommentPart]) +sMDoc Nothing = return Nothing +sMDoc (Just cs) = Just <$> mapM sCommentPart cs + +sCommentPart :: MonadError String m => CommentPart -> m S.CommentPart +sCommentPart (Ordinary o) = return $ S.Ordinary o +sCommentPart (Asterisk) = return $ S.Asterisk +sCommentPart (At s) = return $ S.At s +sCommentPart (CommentTerm t) = return $ S.CommentTerm t +sCommentPart (CommentPremise f) = return $ S.CommentPremise f +sCommentPart (SpecInComment spec) = S.SpecInComment <$> sSpec spec Nothing [] + +bValSort :: MonadError String m => Type -> m S.FSort +bValSort ty = case ty of + TermTuple [t2] -> bValSort t2 + _ -> sTerm ty + +sMaybeTerm :: MonadError String m => Term -> m (Maybe S.FTerm) +sMaybeTerm TermDots = return Nothing +sMaybeTerm t = Just <$> sTerm t + +sTerm :: MonadError String m => Term -> m S.FTerm +sTerm t = case t of + TermDots -> return (S.TTuple []) + TermVar Nothing -> return $ S.TAny + TermVar (Just var) -> return $ S.TMetaVar var + TermConst cnst -> case cnst of + ConstAtom a -> return $ S.TLiteral (S.FLiteralString a) + ConstString str -> return $ S.TLiteral (S.FLiteralString str) + ConstNat n -> return $ S.TLiteral (S.FLiteralNat n) + ConstFloat f -> throwError "CBS compiler does not support float constants" + TermName nm -> return $ S.TName nm + VarApp var term -> throwError ("CBS compiler does not support variable application: " ++ show var) + NameApp nm (TermTuple terms) + -> S.TApp nm <$> mapM sTerm terms + NameApp nm term -> S.TApp nm . (:[]) <$> sTerm term + Typed term ty -> sTerm term --throwError ("unexpected typed term: " ++ show (term,ty)) + Computes ty -> S.TSortComputes <$> sTerm ty + ComputesFrom f t -> S.TSortComputesFrom <$> sTerm f <*> sTerm t + TermPostfix t op -> flip S.TSortSeq op <$> sTerm t + TermSequence ts -> throwError "top-level term-sequence" + TermTuple ts -> S.TTuple <$> mapM sTerm ts + TermList ts -> S.TList <$> mapM sTerm ts + TermSet ts -> S.TSet <$> mapM sTerm ts + TermMap ps -> S.TMap <$> mapM sPoint ps + where sPoint Nothing = throwError "... in map literal" + sPoint (Just (f,t)) = S.TBinding <$> sTerm f <*> sTerm t + TermUnion t1 t2 -> S.TSortUnion <$> sTerm t1 <*> sTerm t2 + TermInter t1 t2 -> S.TSortInter <$> sTerm t1 <*> sTerm t2 + TermPower t1 t2 -> S.TSortPower <$> sTerm t1 <*> sTerm t2 + TermComplement ty -> S.TSortComplement <$> sTerm ty + + SemanticsApp _ _ _ -> throwError "unexpected semantic application in term" + +sRules :: MonadError String m => [Rule] -> m [S.FRule] +sRules = mapM sRule + +sRule :: MonadError String m => Rule -> m S.FRule +sRule r = case r of + Inference _ (ConcStatic _ _ _ _ _) -> throwError "missing translation for static rules" + Inference _ (ConcTyping _ _ _) -> throwError "missing translation for typing rules" + Desugar _ _ _ -> error "translating desugar rule" + Semantics _ _ _ _ -> error "translation semantics rule" + Inference scs (ConcRewrite t1 t2) -> rewriteRule t1 t2 scs + Inference scs (ConcDynamic mc st1 arr st2) -> stepRule mc st1 st2 arr scs + where nmOfTerm t = case t of + TermName nm -> return nm + NameApp nm _ -> return nm + _ -> throwError ("invalid rule pattern: " ++ show t) + patsOf t = case t of + TermName nm -> return Nothing + NameApp _ (TermTuple []) -> return Nothing + NameApp _ term -> Just <$> term2pats term + _ -> throwError ("invalid rule pattern: " ++ show t) + + rewriteRule :: MonadError String m => + Term -> Term -> [Premise] -> m S.FRule + rewriteRule t1 t2 scs = do + S.FRuleRewrite (termName t1) + <$> case termArgs t1 of + Nothing -> return Nothing + Just args -> Just <$> mapM term2pat args + <*> fmap Just (sTerm t2) + <*> prem2sideconds scs + + stepRule :: MonadError String m => + (Maybe Context) -> State -> State -> Dynamic -> [Premise] -> m S.FRule + stepRule mc s1 s2 arr prs = do + source <- case termArgs (stateTerm s1) of + Nothing -> return Nothing + Just args -> Just <$> mapM term2pat args + target <- sTerm (stateTerm s2) + inhs <- sEntities term2pats (contextEnts mc) + muts_in <- sEntities term2pat (stateEnts s1) + muts_out <- sEntities sTerm (stateEnts s2) + (inps, outs, ctrs) <- foldrM arrowEnts ([], [], []) (dynamicEnts arr) + let fstep = S.FStep source target inhs (muts_in, muts_out) inps outs ctrs + S.FRuleStep (termName t1) fstep <$> prem2conds prs + where t1 = stateTerm s1 + muts_in = stateEnts s1 + t2 = stateTerm s2 + muts_out = stateEnts s2 + arrowEnts (n,t,pol) (is, os, cs) = case pol of + Nothing -> (\t' -> (is,os,(n,t'):cs)) <$> term2pat t + Just In -> (\t' -> ((n,t'):is,os,cs)) <$> term2pat t + Just Out -> (\t' -> (is,(n,t'):os,cs)) <$> sTerm t +{- + mpats <- patsOf t1 + target <- sTerm t2 + context <- sMaybeContext term2pat mc + muts_pat <- sMutEntities term2pat muts_in + muts_term <- sMutEntities sTerm muts_out + (ins, outs, sigs) <- sArrow term2pat sTerm term2pat arr + let step = S.FStep mpats target context (muts_pat, muts_term) ins outs sigs + nm <- nmOfTerm t1 + antecedents <- forms2prems scs + return (S.FRuleStep nm step antecedents) +-} + +term2pats :: MonadError String m => Term -> m [S.FPattern] +term2pats term = case term of + TermSequence ts -> terms2pats ts + TermTuple ts -> terms2pats ts + _ -> (:[]) <$> term2pat term + +terms2pats :: MonadError String m => [Term] -> m [S.FPattern] +terms2pats = mapM term2pat + +term2pat :: MonadError String m => Term -> m S.FPattern +term2pat t = case t of + TermConst cnst -> case cnst of + ConstAtom str -> return $ S.PLit (S.FLiteralAtom str) + ConstString str -> return $ S.PLit (S.FLiteralString str) + ConstNat n -> return $ S.PLit (S.FLiteralNat n) + ConstFloat f -> return $ S.PLit (S.FLiteralFloat f) + TermVar (Just var) + | last var == '*' -> return $ S.PSeqMetaVar var S.StarOp + | last var == '+' -> return $ S.PSeqMetaVar var S.PlusOp + | last var == '?' -> return $ S.PSeqMetaVar var S.QuestionMarkOp + | otherwise -> return $ S.PMetaVar var + TermVar Nothing -> return $ S.PAny + TermDots -> return $ S.PAny + TermName nm -> return $ S.PADT nm [] + NameApp nm term -> S.PADT nm <$> term2pats term + VarApp var term -> throwError "variable application not allowed in a pattern" + Typed term ty -> S.PAnnotated <$> term2pat term <*> sSort ty + Computes _ -> throwError " =>_ appearing in pattern" + ComputesFrom _ _ -> throwError " _=>_ appearing in pattern" + TermPostfix (TermVar Nothing) op -> return $ S.PSeqMetaVar "___" op + TermPostfix TermDots op -> return $ S.PSeqMetaVar "___" op + TermPostfix _ _ -> throwError "postfix in pattern" + TermSequence ts -> throwError "top-level term-sequence in pattern" + TermUnion _ _ -> throwError "sort-union in pattern" + TermInter _ _ -> throwError "sort-intersect in pattern" + TermComplement _ -> throwError "sort-complement in pattern" + TermTuple ts -> S.PSeq <$> terms2pats ts + TermList ts -> S.PList <$> terms2pats ts + TermSet ts -> throwError "set notation in pattern" + TermMap ts -> throwError "map notation in pattern" + TermPower t1 t2 -> throwError "term power in pattern" + SemanticsApp _ _ _-> throwError "unexpected semantic application in pattern" + +prem2sideconds :: MonadError String m => [Premise] -> m [S.FSideCondition] +prem2sideconds prems = concat <$> mapM filterOp prems + where filterOp prem = rights <$> prem2cond prem + +prem2conds :: MonadError String m => [Premise] -> m [Either S.FPremiseStep S.FSideCondition] +prem2conds prems = concat <$> mapM prem2cond prems + +prem2cond :: MonadError String m => Premise -> m [Either S.FPremiseStep S.FSideCondition] +prem2cond prem = case prem of + PremStatic _ _ _ _ _ -> + throwError "missing translation for static premises" + PremTyping (Just _) _ _ -> + throwError "missing translation for typing premises" + PremTyping _ (StateExplicit _ _) _ -> + throwError "missing translation for typing premises" + PremDynamic mc st1 arr st2 -> + (:[]) . Left <$> bPremiseStep mc st1 arr st2 + PremRewrite t1 t2 -> + (((:[]) . Right) .) . S.SCPatternMatch <$> sTerm t1 <*> term2pats t2 + PremEquality t1 t2 -> + (((:[]) . Right) .) . S.SCEquality <$> sTerm t1 <*> sTerm t2 + PremInequality t1 t2 -> + (((:[]) . Right) .) . S.SCInequality <$> sTerm t1 <*> sTerm t2 + PremTyping Nothing (StateImplicit t1) t2 -> + (((:[]) . Right) .) . S.SCIsInSort <$> sTerm t1 <*> sSort t2 + PremSubtype t1 t2 -> + return [] + +bPremiseStep :: MonadError String m => + Maybe Context -> State -> Dynamic -> State -> m S.FPremiseStep +bPremiseStep mc lhs arr rhs = do + source <- sTerm (stateTerm lhs) + target <- term2pats (stateTerm rhs) + inhs <- sEntities sTerm (contextEnts mc) + muts_in <- sEntities sTerm (stateEnts lhs) + muts_out <- sEntities term2pat (stateEnts rhs) + (inps,outs,ctrs) <- foldrM op ([],[],[]) (dynamicEnts arr) + return (S.FPremiseStep source target inhs (muts_in,muts_out) inps outs ctrs) + where op (n,t,pol) (is, os, cs) = case pol of + Nothing -> (\t' -> (is,os,(n,t'):cs)) <$> term2pat t + Just In -> (\t' -> ((n,t'):is,os,cs)) <$> sTerm t + Just Out -> (\t' -> (is,(n,t'):os,cs)) <$> term2pat t + +sEntities :: MonadError String m => (Term -> m a) -> [EntTerm] -> m [(Name, a)] +sEntities simplifier = mapM op + where op (nm, t) = (nm,) <$> simplifier t +{- +sArrow :: MonadError String m => + (Term -> m ins) -> (Term -> m outs) -> (Term -> m sigs) -> + Arrow -> m ([(Name, ins)],[(Name, outs)],[(Name, sigs)]) +sArrow sIns sOuts sSigs arr = case arr of + Normal es -> mkEntities es + Static es -> mkEntities es + Rewrite -> mkEntities [] + where mkEntities = foldM op ([],[],[]) + where op (ins,outs,sigs) (EmitIn nm term) = do + s <- sIns term + return ((nm,s):ins,outs,sigs) + op (ins,outs,sigs) (EmitOut nm term) = do + s <- sOuts term + return (ins,(nm,s):outs,sigs) + op (ins,outs,sigs) (EmitSig nm term) = do + s <- sSigs term + return (ins,outs,(nm,s):sigs) +-} +sSort :: MonadError String m => Term -> m S.FSort +sSort = sTerm + diff --git a/src/Simplify/CoreToTarget.hs b/src/Simplify/CoreToTarget.hs new file mode 100644 --- /dev/null +++ b/src/Simplify/CoreToTarget.hs @@ -0,0 +1,174 @@ +{-# Language FlexibleContexts, ScopedTypeVariables, LambdaCase, MultiParamTypeClasses, TupleSections, FlexibleInstances, OverloadedStrings #-} + +-- | +-- Sanity checking and simplifications regarding: +-- +-- * input entities +module Simplify.CoreToTarget where + +import CCO.Component (Component, component) +import CCO.Feedback (Feedback, errorMessage) +import CCO.Printing (wrapped) + +import Control.Applicative +import Control.Arrow ((***)) +import Control.Monad.Except + +import Simplify.Utils + +import Data.Either (lefts) +import Data.Maybe (catMaybes) +import Data.Text (pack) + + +-------------------------------------------------------------------- + +import Funcons.EDSL (FTerm(TVar), string_, HasTypeVar(..), limitedSubsTypeVarWildcard, showOp, SeqSortOp(..)) + +import Types.SourceAbstractSyntax (Name, MetaVar) +import Types.Bindings(HasPatVar(..)) +import Types.CoreAbstractSyntax + +import qualified Types.TargetAbstractSyntax as T + +-------------------------------------------------------------------- + +-- require for forming a pipeline with uu-cco library +core2target :: Component CBSFile T.CBSFile +core2target = component simplifyCBSFile + +instance MonadError String Feedback where + throwError = errorMessage . wrapped + +-------------------------------------------------------------------- + +simplifyCBSFile :: MonadError String m => CBSFile -> m T.CBSFile +simplifyCBSFile (CBSFile file env als) = + T.CBSFile <$> (concat <$> mapM (simplifySpecs env) file) + <*> return env <*> return als + +simplifySpecs :: MonadError String m => TypeEnv -> CBSSpec -> m [T.CBSSpec] +simplifySpecs env (FunconSpec fspec) = return . T.FunconSpec <$> simplifyFSpec env fspec +simplifySpecs env (DataTypeSpec spec) = return [T.DataTypeSpec spec] +simplifySpecs env (EntitySpec spec) = return [T.EntitySpec spec] +simplifySpecs env (MetaSpec spec) = return [T.MetaSpec spec] +simplifySpecs env (ConsSpec spec) = + return (T.FunconSpec (simplifyConsSpec spec) : [T.ConsSpec spec]) + +-------------------------------------------------------------------- + +simplifyConsSpec :: ConsSpec -> T.FunconSpec +simplifyConsSpec (ValCons nm (TypeCons ss) pattypes _ _) = + genValConsFuncons nm ss "non-strict-datatype-value" pattypes +simplifyConsSpec (ValCons nm sig pattypes _ _) = + genValConsFuncons nm sig "datatype-value" pattypes + where sig = if null pattypes then FNullary else FStrict + +genValConsFuncons nm sig cons pattypes = + T.FRules nm sig Nothing [rule] [] + where rule = T.FRewriteRule pats (Just (TApp cons (cname:args))) scds + cname = TFuncon (string_ nm) + args = map (TVar . fst) vars + pats = zipWith mkPat vars pattypes + -- sorts are ignored (no substitution available) + where mkPat (var, mop) sort = msvar + where msvar = case mop of Nothing -> PMetaVar var + Just op -> PSeqVar var op +-- sides = zipWith mkSide vars pattypes +-- where mkSide (var,mop) sort = SCIsInSort (TVar var) sort + vars = zipWith mkOp [1..] pattypes + where mkOp i pat = case pat of + TSortSeq _ op -> var $ Just op + TSortPower _ _ -> var $ Just StarOp + TVar str -> case last str of + '*' -> var $ Just StarOp + '?' -> var $ Just QuestionMarkOp + '+' -> var $ Just PlusOp + _ -> var Nothing + _ -> var Nothing + where var mop = ("_X" ++ show i ++ maybe "" showOp mop, mop) + scds = case sig of FStrict -> map (uncurry toVal) vars + where toVal x mop = case mop of + Just op -> SCIsInSort (TVar x) (TSortSeq (TSortSeq (TName "values") QuestionMarkOp) op) + Nothing -> SCIsInSort (TVar x) (TSortSeq (TName "values") QuestionMarkOp) + _ -> [] + +simplifyFSpec :: MonadError String m => TypeEnv -> FunconSpec -> m T.FunconSpec +simplifyFSpec env (FRules nm sig mdoc rews steps) = + T.FRules nm sig mdoc <$> mapM (simplifyRewrite env) rews + <*> mapM (simplifyFStepRule env) steps + +simplifyRewrite :: MonadError String m => TypeEnv -> FRewriteRule -> m T.FRewriteRule +simplifyRewrite env rule@(FRewriteRule pats rhs conds) = -- TODO why do we need a different FRewriteRule datatype? + return (limitedSubsTypeVarWildcard (pvars rule) (Just (TSortSeq (TName "values") QuestionMarkOp)) env $ T.FRewriteRule pats rhs conds) + +simplifyFStepRule :: MonadError String m => TypeEnv -> FStepRule -> m T.FStepRule +simplifyFStepRule env rule@(FStepRule step pcs) = + do b <- checkInputRouting step (lefts pcs) + guardM b "Unsupported routing between input entities." + limitedSubsTypeVarWildcard (pvars rule) (Just (TSortSeq (TName "values") QuestionMarkOp)) env <$> + (T.FStepRule <$> simplifyFStep step <*> mapM (traverseEither simplifyFPremiseStep return) pcs) + +-------------------------------------------------------------------- + +{- +simplifyF2TPattern :: MonadError String m => FPattern -> m T.TPattern +simplifyF2TPattern p = case p of + PTuple ps -> T.TPADT "tuples" <$> mapM simplifyF2TPattern ps + PList [p] -> T.TPADT "lists" . (:[]) <$> simplifyF2TPattern p + PList ps -> throwError "cannot simplify list-notation to type-pattern" + PAnnotated pat s -> simplifyF2TPattern pat + PADT cons ps -> T.TPADT (pack cons) <$> mapM simplifyF2TPattern ps + PAny -> return $ T.TPWildCard + PLit lit -> return $ T.TPLit (TFuncon $ simplifyLiteral lit) + PMetaVar var -> return $ T.TPVar var + PSeqMetaVar var op -> return $ T.TPSeqVar var op +-} + +simplifyFStep :: MonadError String m => FStep -> m T.FStep +simplifyFStep st = + return $ T.FStep + { T.stepSource = stepSource st + , T.stepTarget = stepTarget st + , T.stepInheritedEntities = stepInheritedEntities st + , T.stepMutableEntities = stepMutableEntities st + , T.stepInputEntities = map (\(n,ps,_) -> (n,ps)) + (stepInputEntities st) + , T.stepOutputEntities = stepOutputEntities st + , T.stepControlEntities = stepControlEntities st + } + +simplifyInputEntity :: MonadError String m => (Name,[FPattern],[MetaVar]) -> m (Name,[MetaVar]) +simplifyInputEntity (n,ps,_) = (n,) <$> mapM patToMV ps + where + patToMV (PMetaVar mv) = return mv + patToMV _ = throwError "Currently we only allow meta-variables in input patterns." -- TODO: could also allow underscores + +simplifyFPremiseStep :: MonadError String m => FPremiseStep -> m T.FPremiseStep +simplifyFPremiseStep pst = + return $ T.FPremiseStep + { T.premiseSource = premiseSource pst + , T.premiseTarget = premiseTarget pst + , T.premiseInheritedEntities = premiseInheritedEntities pst + , T.premiseMutableEntities = premiseMutableEntities pst + , T.premiseInputEntities = map simplifyInputEntityPremise (premiseInputEntities pst) + , T.premiseOutputEntities = premiseOutputEntities pst + , T.premiseControlEntities = premiseControlEntities pst + } + +simplifyInputEntityPremise :: (Name,[FTerm],Maybe MetaVar) -> (Name,[FTerm],T.InputAccess) +simplifyInputEntityPremise (n,ts,Nothing) = (n,ts,T.ExactInput) +simplifyInputEntityPremise (n,ts,Just _) = (n,ts,T.ExtraInput) + +-------------------------------------------------------------------- + +checkInputRouting :: forall m. MonadError String m => FStep -> [FPremiseStep] -> m Bool +checkInputRouting step psteps = + and <$> mapM (\(n,_,mvs) -> (mvs ==) <$> catMaybes <$> mapM (premiseMv n) psteps) (stepInputEntities step) + where + premiseMv :: Name -> FPremiseStep -> m (Maybe MetaVar) + premiseMv n pstep = case lookup2 n (premiseInputEntities pstep) of + Nothing -> throwError "Mismatched input entity in rule" -- do we check this earlier? + Just (_,mmv) -> return mmv + +-------------------------------------------------------------------- diff --git a/src/Simplify/LiftStrictness.hs b/src/Simplify/LiftStrictness.hs new file mode 100644 --- /dev/null +++ b/src/Simplify/LiftStrictness.hs @@ -0,0 +1,63 @@ +{-# LANGUAGE OverloadedStrings #-} + +module Simplify.LiftStrictness where + +import Types.SourceAbstractSyntax (SeqSortOp(..)) +import Types.CoreAbstractSyntax (FSig(..), FTerm(..), FPattern (..) + ,Strictness(..),FSideCondition(..)) +import Types.TargetAbstractSyntax hiding (FPattern(..)) + +import Data.Text (pack) +import CCO.Component + +lift_strictness :: Component CBSFile CBSFile +lift_strictness = component (return . lCBSFile) + +lCBSFile :: CBSFile -> CBSFile +lCBSFile cbsf = doToFuncons lFSpec cbsf + +lFSpec :: FunconSpec -> FunconSpec +lFSpec spec@(FRules nm sig mcs rs ss) = case sig of + FLazy -> spec + FNullary -> spec + FStrict -> FRules nm FLazy mcs rs ss' + where ss' = steprule : ss + steprule = FStepRule step [Left premise] + step = FStep [PAnnotated (PSeqVar "V*" StarOp) + (TSortSeq (TSortSeq (TName "values") QuestionMarkOp) StarOp) + ,PMetaVar "X" + ,PSeqVar "Y*" StarOp] + (TApp (pack nm) [TVar "V*", TVar "X'", TVar "Y*"]) + [] [] [] [] [] + premise = FPremiseStep (TVar "X") [PMetaVar "X'"] [] [] [] [] [] +{- moved to TargetToIML + rewrule = FRewriteRule [PSeqVar "X*" StarOp] + (Just (TApp (pack nm) [TVar "Y*"])) [cond] + where cond = SCPatternMatch (TVar "X*") (PSeqVar "Y*" StarOp) -} + FPartiallyLazy ann mseqvar -> FRules nm FLazy mcs rs ss' + where ss' = map mkRule ruleKeys ++ seqvarRule ++ ss + ruleKeys = map fst $ filter ((Strict ==) . snd) keys + keys = zip [1..] ann + seqvarRule = case mseqvar of + Nothing -> [] + Just sann -> [] --[rule] -- TODO similar to strict case but taking annotation into account + + mkRule k = FStepRule step [Left premise] + where step = FStep pats (TApp (pack nm) terms) [] [] [] [] [] + (pats,terms) = foldr op base keys + where base = case mseqvar of + Just _ -> ([PSeqVar "X*" StarOp] + ,[TVar "X*"]) + _ -> ([], []) + op (k',sness) (pats, terms) + | k' == k = (PMetaVar var:pats + ,TVar (var ++ "'") : terms) + | k' < k, Strict <- sness = + (PAnnotated (PMetaVar var) + (TSortSeq (TName "values") QuestionMarkOp):pats + ,TVar var : terms) + | True = (PMetaVar var : pats, TVar var : terms) + where var = "X" ++ show k' + premise = FPremiseStep (TVar var) [PMetaVar (var ++ "'")] + [] [] [] [] [] + where var = "X" ++ show k diff --git a/src/Simplify/Simplifier.hs b/src/Simplify/Simplifier.hs new file mode 100644 --- /dev/null +++ b/src/Simplify/Simplifier.hs @@ -0,0 +1,460 @@ +{-# Language FlexibleContexts, LambdaCase, MultiParamTypeClasses, TupleSections, FlexibleInstances, OverloadedStrings #-} + +module Simplify.Simplifier where + +import Funcons.EDSL (Values(..), Funcons(..), string__) +import qualified Funcons.EDSL as EDSL + +import CCO.Component (Component, component) +import CCO.Feedback (Feedback, errorMessage) +import CCO.Printing (wrapped) + +import Control.Applicative +import Control.Monad.Except + +import Data.Either +import Data.Monoid +import Data.Text (pack) +import qualified Data.Map as M +import qualified Data.Set as S + +import Simplify.Utils + +-------------------------------------------------------------------- + +import Types.Bindings +import Types.SourceAbstractSyntax +import qualified Types.CoreAbstractSyntax as C + +-------------------------------------------------------------------- + +-- require for forming a pipeline with uu-cco library +simplifier :: Component CBSFile C.CBSFile +simplifier = component simplifyCBSFile + +instance MonadError String Feedback where + throwError = errorMessage . wrapped + +-------------------------------------------------------------------- + +simplifyCBSFile :: MonadError String m => CBSFile -> m C.CBSFile +simplifyCBSFile (CBSFile file env als) = do + env' <- simplifyTypeEnv env + let kindMap = foldr bindTypeDecl M.empty file + specss <- mapM (simplifyCBSSpec kindMap env') file + let specs = map (mvarConditions env') (concat specss) + return $ C.CBSFile specs env' als + +bindTypeDecl :: CBSSpec -> KindMap -> KindMap +bindTypeDecl (TypeSpec (DataTypeDecl nm _ _)) = M.insert nm Type +bindTypeDecl (DataTypeSpec (DataTypeDecl nm _ _)) = M.insert nm DataType +bindTypeDecl _ = id + +mvarConditions :: C.TypeEnv -> C.CBSSpec -> C.CBSSpec +mvarConditions env s = case s of + C.FunconSpec (C.FRules nm sig mcs rs ss) + -> C.FunconSpec (C.FRules nm sig mcs rs' ss') + where rs' = map mvarRs rs + ss' = map mvarSs ss + _ -> s + where mvarRs r@(C.FRewriteRule p f ss) = + -- added last to ensure bindings + C.FRewriteRule p f (ss ++ M.foldrWithKey op [] env) + where op x (C.ElemOf ty) acc = case x `S.member` patvars of + True -> C.SCIsInSort (C.TVar x) ty : acc + False -> acc + op x (C.SubTyOf _) acc = acc + patvars = pvars r + mvarSs r@(C.FStepRule f scs) = C.FStepRule f (scs ++ M.foldrWithKey op [] env) + where patvars = pvars r + op x (C.ElemOf ty) acc = case x `S.member` patvars of + True -> Right (C.SCIsInSort (C.TVar x) ty) : acc + False -> acc + op x (C.SubTyOf _) acc = acc + +-- add side-conditions to rules based on the declarations of meta-variables + +simplifyTypeEnv :: MonadError String m => TypeEnv -> m C.TypeEnv +simplifyTypeEnv = mapM simplifyTyAssoc + +simplifyTyAssoc :: MonadError String m => TyAssoc -> m C.TyAssoc +simplifyTyAssoc (ElemOf t) = C.ElemOf <$> simplifyFTerm t +simplifyTyAssoc (SubTyOf t) = C.SubTyOf <$> simplifyFTerm t + +type KindMap = M.Map Name {- type name -} Kind +data Kind = DataType | Type deriving (Show, Enum) + +simplifyCBSSpec :: MonadError String m => KindMap -> C.TypeEnv -> CBSSpec -> m [C.CBSSpec] +simplifyCBSSpec _ _ (TypeSynonymSpec spec) = return . C.FunconSpec <$> simplifyTypeSynonymSpec spec +simplifyCBSSpec km tyenv (TypeSpec spec) = simplifyCBSSpec km tyenv (DataTypeSpec spec) +simplifyCBSSpec _ tyenv (DataTypeSpec spec@(DataTypeDecl tynm typarams alts)) = do + conss <- forM alts $ \alt -> case alt of + DataTypeInclusion _ -> return mzero + DataTypeConstructor nm sorts -> do + sorts' <- mapM simplifyFTerm sorts + typarams' <- mapM (simplifyParamPattern tyenv) typarams + return [genDataValCons tynm typarams' nm sorts'] + dspec <- simplifyDataTypeSpec tyenv spec + return (C.DataTypeSpec dspec : msum conss) +simplifyCBSSpec km _ (FunconSpec spec@(FRules sig rules)) + | Just (tyname, kind) <- mNameKind -- recognised as a value-constructor + , null rules -- and definition is missing + = do args <- mapM sortInPattern (sigParams sig) + typarams <- maybe (return []) (mapM toTypeParam) $ termArgs (sigSort sig) + sig' <- mkCSig kind + return [C.ConsSpec (C.ValCons (sigName sig) sig' + args tyname typarams)] + where toTypeParam t = term2tpat <$> simplifyFTerm t + mNameKind = case sigSort sig of + TName tnm -> fmap (tnm,) (M.lookup tnm km) + TApp tnm _ -> fmap (tnm,) (M.lookup tnm km) + _ -> Nothing + where nameOf (TName nm) = nm + nameOf (TApp nm _) = nm + nameOf t = error ("nameOf assert1: " ++ show t) + mkCSig kind = case kind of + DataType -> return C.DataTypeCons + Type -> C.TypeCons <$> simplifyFSig sig + sortInPattern (_, Nothing) = throwError ("constructor " ++ (sigName sig) ++ " without typed arguments") + sortInPattern (_, Just sort) = simplifyFTerm sort + +simplifyCBSSpec _ _ (FunconSpec spec) = return . C.FunconSpec <$> simplifyFunconSpec spec +simplifyCBSSpec _ _ (EntitySpec spec) = return . C.EntitySpec <$> simplifyEntitySpec spec +simplifyCBSSpec _ _ (MetaSpec spec) = return . return $ C.MetaSpec spec + +simplifyTypeSynonymSpec :: MonadError String m => TypeSynonymSpec -> m C.FunconSpec +simplifyTypeSynonymSpec (TypeSynonymDecl n ps ty) = + simplifyFunconSpec $ + FAbbrv (FSig n ps (TName "types") Nothing) (Just ty) + +genDataValCons :: Name -> [C.TPattern] -> Name -> [C.FSort] -> C.CBSSpec +genDataValCons tynm typarams nm ptypes = + C.ConsSpec (C.ValCons nm C.DataTypeCons ptypes tynm typarams) + +simplifyDataTypeSpec :: MonadError String m => C.TypeEnv -> DataTypeSpec -> m C.DataTypeSpec +simplifyDataTypeSpec tyenv (DataTypeDecl nm ps alts) = + C.DataTypeDecl nm <$> mapM (simplifyParamPattern tyenv) ps <*> simplifyDataTypeAlts alts + +simplifyParamPattern :: MonadError String m => + C.TypeEnv -> FParam -> m (C.TPattern) +simplifyParamPattern tyenv (pat,_) = simplifyPat pat + where simplifyPat (PPMetaVar var) = return $ C.TPVar var + simplifyPat PPAny = return $ C.TPWildCard + simplifyPat (PPSeqMetaVar var op) = return $ C.TPSeqVar var op + +simplifyDataTypeAlts :: MonadError String m => [DataTypeAlt] -> m [C.DataTypeAlt] +simplifyDataTypeAlts alts = concat <$> mapM simplifyDataTypeAlt alts +simplifyDataTypeAlt :: MonadError String m => DataTypeAlt -> m [C.DataTypeAlt] +simplifyDataTypeAlt (DataTypeInclusion term) = + return . C.DataTypeInclusion <$> simplifyFTerm term +simplifyDataTypeAlt (DataTypeConstructor nm terms) = return [] + +simplifyEntitySpec :: MonadError String m => EntitySpec -> m C.EntitySpec +simplifyEntitySpec (InheritedSpec (name,term,_)) + = C.InheritedSpec name <$> simplifyFTerm term +simplifyEntitySpec (MutableSpec (name1,term,ty1) (name2,_,ty2)) + = do guardM (name1 == name2) "mutable entity name mismatch" + guardM (ty1 == ty2) "mutable entity type mismatch" + C.MutableSpec name1 <$> simplifyFTerm term + +simplifyEntitySpec (InputSpec (name,_,ty)) = + return (C.InputSpec name) + +simplifyEntitySpec (OutputSpec (name,_,ty)) = + do guardM (isAppOf "lists" ty) "output entities must be declared to contain lists" + return (C.OutputSpec name) + +simplifyEntitySpec (ControlSpec (name,ty)) = + do guardM (isSortSeq QuestionMarkOp ty) "control entities must be declared to contain option types `(T)?`" + return (C.ControlSpec name) + + +simplifyFunconSpec :: MonadError String m => FunconSpec -> m C.FunconSpec + +simplifyFunconSpec (FAbbrv sig mterm) + = do term' <- maybe (return Nothing) ((Just <$>) . simplifyFTerm) mterm + mdoc <- sMDoc (sigDoc sig) + params <- mapM abbrvParamPatt (sigParams sig) + sig' <- simplifyFSig sig + return $ C.FRules (sigName sig) sig' mdoc + [ C.FRewriteRule params term' [] ] [] +simplifyFunconSpec (FRules sig rules) = do + mdoc <- sMDoc (sigDoc sig) + sig' <- simplifyFSig sig + uncurry (C.FRules n sig' mdoc) <$> simplifyFRules n rules + where + n = sigName sig + + +sMDoc :: MonadError String m => Maybe [CommentPart] -> m (Maybe [C.CommentPart]) +sMDoc Nothing = return Nothing +sMDoc (Just cs) = Just <$> mapM sCommentPart cs + +sCommentPart :: MonadError String m => CommentPart -> m C.CommentPart +sCommentPart (Ordinary o) = return $ C.Ordinary o +sCommentPart (Asterisk) = return $ C.Asterisk +sCommentPart (At s) = return $ C.At s +sCommentPart (SpecInComment spec) = do + specs <- simplifyCBSSpec M.empty M.empty spec + case specs of + [cspec] -> return (C.SpecInComment cspec) + _ -> throwError "multi-spec in comment" +sCommentPart (CommentTerm t) = return $ C.CommentTerm t +sCommentPart (CommentPremise f) = return $ C.CommentPremise f + +simplifyFSig :: MonadError String m => FSig -> m C.FSig +simplifyFSig (FSig nm ps sort mcs) + | null ps = return C.FNullary + | and strictArgs = return C.FStrict + | not (or strictArgs) = return C.FLazy + -- checks requirement that only last parameter is variadic, if any + | any isVariadic (init ps) = + throwError (nm ++ " not a valid variadic funcon") + | or strictArgs + , not variadic = return $ + C.FPartiallyLazy (map toStrict strictArgs) Nothing + | otherwise {-or strictArgs + , variadic-} = return $ + C.FPartiallyLazy (map toStrict (init strictArgs)) + (Just $ toStrict (last strictArgs)) + where strictArgs = map isStrictParam ps + variadic = isVariadic (last ps) + toStrict strict = if strict then C.Strict else C.Lazy + + +simplifyFRules :: MonadError String m => Name -> [FRule] -> m ([C.FRewriteRule],[C.FStepRule]) +simplifyFRules n rs = partitionEithers <$> mapM (simplifyFRule n) rs + + +simplifyFRule :: MonadError String m => Name -> FRule -> m (Either C.FRewriteRule C.FStepRule) +simplifyFRule n (FRuleRewrite name mpats rhs conds) + = do guardM (n == name) ("rule name '" <> name <> "' does not match signature '" <> n <> "'") + pats <- topLevelFPatterns (maybePattsToPatts mpats) + rhs' <- case rhs of Nothing -> return Nothing + Just t -> Just <$> simplifyFTerm t + Left <$> C.FRewriteRule pats rhs' <$> mapM simplifyFSideCondition conds + +simplifyFRule n (FRuleStep name st ps_cs) + = do guardM (n == name) ("rule name '" <> name <> "' does not match signature '" <> n <> "'") + st' <- simplifyFStep st + ps_cs' <- mapM (traverseEither simplifyFPremiseStep simplifyFSideCondition) ps_cs + guardM (all (== entitiesOfStep st') (map entitiesOfPremiseStep $ lefts ps_cs')) "the entities in a premise must match the entites used in the conclusion" + return $ Right $ C.FStepRule st' ps_cs' + +simplifyFSideCondition :: MonadError String m => FSideCondition -> m C.FSideCondition +simplifyFSideCondition (SCEquality e1 e2) = + C.SCEquality <$> simplifyFTerm e1 <*> simplifyFTerm e2 +simplifyFSideCondition (SCInequality e1 e2) = + C.SCInequality <$> simplifyFTerm e1 <*> simplifyFTerm e2 +simplifyFSideCondition (SCPatternMatch e p) = + C.SCPatternMatch <$> simplifyFTerm e <*> topLevelFPatterns p +simplifyFSideCondition (SCIsInSort e ty) = + C.SCIsInSort <$> simplifyFTerm e <*> simplifyFTerm ty + +simplifyFStep :: MonadError String m => FStep -> m C.FStep +simplifyFStep st + = do mut <- uncurry (mergeAssocListsM "mismatched mutable entities in conclusion") (stepMutableEntities st) + mut' <- mapM simplifyMutableEntity mut + inp <- mapM (uncurry simplifyInputEntity) (stepInputEntities st) + ctrl <- mapM (uncurry simplifyControlEntity) (stepControlEntities st) + outs <- mapM (uncurry simplifyNameTermPair) (stepOutputEntities st) + inhs <- mapM (uncurry simplifyNamePatternsPair) (stepInheritedEntities st) + source <- topLevelFPatterns (maybePattsToPatts (stepSource st)) + target <- simplifyFTerm (stepTarget st) + return $ C.FStep + { C.stepSource = source + , C.stepTarget = target + , C.stepInheritedEntities = inhs + , C.stepMutableEntities = mut' + , C.stepInputEntities = inp + , C.stepOutputEntities = outs + , C.stepControlEntities = ctrl + } + +simplifyFPremiseStep :: MonadError String m => FPremiseStep -> m C.FPremiseStep +simplifyFPremiseStep pst + = do mut <- uncurry (mergeAssocListsM "mismatched mutable entities in premise") + (premiseMutableEntities pst) + mut' <- mapM simplifyMutableEntityPremise mut + ctrl <- mapM (uncurry simplifyControlEntityPremise) (premiseControlEntities pst) + outs <- mapM (uncurry simplifyNamePatternPair) (premiseOutputEntities pst) + ins <- mapM (uncurry simplifyInputEntityPremise) (premiseInputEntities pst) + inhs <- mapM (uncurry simplifyNameTermPair) (premiseInheritedEntities pst) + source <- simplifyFTerm (premiseSource pst) + target <- topLevelFPatterns (premiseTarget pst) + return $ C.FPremiseStep + { C.premiseSource = source + , C.premiseTarget = target + , C.premiseInheritedEntities = inhs + , C.premiseMutableEntities = mut' + , C.premiseInputEntities = ins + , C.premiseOutputEntities = outs + , C.premiseControlEntities = ctrl + } + +simplifyMutableEntity :: MonadError String m => (Name, FPattern, FTerm) -> m (Name, C.FPattern, C.FTerm) +simplifyMutableEntity (n,p,t) = (n,,) <$> simplifyFPattern p <*> simplifyFTerm t + +simplifyInputEntity :: MonadError String m => Name -> FPattern -> m (Name,[C.FPattern],[MetaVar]) +simplifyInputEntity n p = case p of + PSeq ps -> splitInputPattern ps + PList ps -> splitInputPattern ps + _ -> splitInputPattern [p] + where + takeStarMetaVars :: ([FPattern],[MetaVar]) -> ([FPattern],[MetaVar]) + takeStarMetaVars (PSeqMetaVar mv StarOp : ps', mvs) = + takeStarMetaVars (ps',mv:mvs) + takeStarMetaVars pmvs = pmvs + splitInputPattern ps = + (n,,reverse rmvs) <$> topLevelFPatterns (reverse rps) + where (rps,rmvs) = takeStarMetaVars (reverse ps,[]) + +-- special meaning of tuple notation for control entities +simplifyControlEntity :: MonadError String m => Name -> FPattern -> m (Name,Maybe C.FPattern) +simplifyControlEntity n (PSeq []) = return (n,Nothing) +simplifyControlEntity n t = (n,) . Just <$> simplifyFPattern t + +simplifyMutableEntityPremise :: MonadError String m => (Name, FTerm, FPattern) -> m (Name, C.FTerm, C.FPattern) +simplifyMutableEntityPremise (n,t,p) = (n,,) <$> simplifyFTerm t <*> simplifyFPattern p + +-- special meaning of tuple notation for control entities +simplifyControlEntityPremise :: MonadError String m => Name -> FPattern -> m (Name,Maybe C.FPattern) +simplifyControlEntityPremise n (PSeq []) = return (n,Nothing) +simplifyControlEntityPremise n p = (n,) . Just <$> simplifyFPattern p + +simplifyNamePatternPair :: MonadError String m => Name -> FPattern -> m (Name,C.FPattern) +simplifyNamePatternPair n p = (n,) <$> simplifyFPattern p + +simplifyNamePatternsPair :: MonadError String m => Name -> [FPattern] -> m (Name,[C.FPattern]) +simplifyNamePatternsPair n p = (n,) <$> topLevelFPatterns p + + +simplifyInputEntityPremise :: MonadError String m => Name -> FTerm -> m (Name,[C.FTerm],Maybe MetaVar) +simplifyInputEntityPremise n t = case t of + TList [] -> return (n,[],Nothing) + TList ts -> splitInputTerms ts + TTuple [] -> return (n,[],Nothing) + TTuple ts -> splitInputTerms ts + _ -> throwError $ "premise input entity " ++ n ++ " not a list or sequence of terms: " ++ show t + where splitInputTerms ts = do + ts' <- mapM simplifyFTerm ts + case last ts' of + C.TVar mv | last mv == '*' -> return (n,init ts',Just mv) + _ -> return (n,ts',Nothing) + +simplifyNameTermPair :: MonadError String m => Name -> FTerm -> m (Name,C.FTerm) +simplifyNameTermPair n t = (n,) <$> simplifyFTerm t + +topLevelFPatterns :: MonadError String m => [FPattern] -> m [C.FPattern] +topLevelFPatterns xs = concat <$> mapM simplifyFPatterns xs + +simplifyFPatterns :: MonadError String m => FPattern -> m [C.FPattern] +simplifyFPatterns (PSeq pats) = concat <$> + mapM (\x -> map C.PValue <$> simplify2VPatterns x) pats +simplifyFPatterns p = (:[]) <$> simplifyFPattern p + +simplifyFPattern :: MonadError String m => FPattern -> m C.FPattern +simplifyFPattern (PAnnotated pat sort) = C.PAnnotated <$> simplifyFPattern pat + <*> simplifyFTerm sort +simplifyFPattern PAny = return C.PWildCard +simplifyFPattern (PMetaVar var) = return (C.PMetaVar var) +simplifyFPattern (PSeqMetaVar var op) = return (C.PSeqVar var op) +simplifyFPattern vpat = C.PValue <$> simplify2VPattern vpat + +simplify2VPatterns :: MonadError String m => FPattern -> m [C.VPattern] +simplify2VPatterns (PSeq pats) = concat <$> mapM simplify2VPatterns pats +simplify2VPatterns p = (:[]) <$> simplify2VPattern p + +simplify2VPattern :: MonadError String m => FPattern -> m C.VPattern +simplify2VPattern (PSeq pats) = error "sequence in simple pattern" +simplify2VPattern (PList pats) = C.PADT "datatype-value" <$> + (((C.VPLit (string__ "list")):) . concat <$> mapM simplify2VPatterns pats) +simplify2VPattern (PADT cons pats) = C.PADT (pack cons) <$> + (concat <$> mapM simplify2VPatterns pats) +simplify2VPattern (PLit lit) = return (C.VPLit (simplifyLiteral lit)) +simplify2VPattern (PAnnotated pat sort) = C.VPAnnotated <$> simplify2VPattern pat + <*> simplifyFTerm sort +simplify2VPattern PAny = return C.VPWildCard +simplify2VPattern (PMetaVar var) = return (C.VPMetaVar var) +simplify2VPattern (PSeqMetaVar var op) = return (C.VPSeqVar var op) + + +simplifyFTerm :: MonadError String m => FTerm -> m C.FTerm +simplifyFTerm (TMetaVar var) = return $ C.TVar var +simplifyFTerm (TLiteral lit) = return $ C.TFuncon $ FValue $ simplifyLiteral lit +simplifyFTerm (TName nm) = return $ C.TName (pack nm) +simplifyFTerm (TApp nm term) = C.TApp (pack nm) <$> mapM simplifyFTerm term +simplifyFTerm (TTuple terms) = C.TSeq <$> mapM simplifyFTerm terms +simplifyFTerm (TList terms) = C.TApp "list" <$> mapM simplifyFTerm terms +simplifyFTerm (TSet terms) = C.TSet <$> mapM simplifyFTerm terms +simplifyFTerm (TMap terms) = C.TMap <$> mapM simplifyFTerm terms +simplifyFTerm (TBinding t1 t2) = C.TBinding <$> simplifyFTerm t1 <*> simplifyFTerm t2 +simplifyFTerm (TSortUnion t1 t2) = C.TSortUnion <$> simplifyFTerm t1 <*> + simplifyFTerm t2 +simplifyFTerm (TSortInter t1 t2) = C.TSortInter <$> simplifyFTerm t1 <*> + simplifyFTerm t2 +simplifyFTerm (TSortComplement t1) = C.TSortComplement <$> simplifyFTerm t1 +simplifyFTerm (TSortSeq t1 op) = C.TSortSeq <$> simplifyFTerm t1 <*> pure op +simplifyFTerm (TSortComputes term) = C.TSortComputes <$> simplifyFTerm term +simplifyFTerm (TSortComputesFrom t1 t2) = C.TSortComputesFrom <$> simplifyFTerm t1 + <*> simplifyFTerm t2 +simplifyFTerm (TSortPower t1 t2) = C.TSortPower <$> simplifyFTerm t1 <*> simplifyFTerm t2 +simplifyFTerm TAny = return C.TAny + +-------------------------------------------------------------------- + +isAppOf :: String -> FTerm -> Bool +isAppOf n (TApp f _) = f == n +isAppOf _ _ = False + +isSortSeq :: SeqSortOp -> FTerm -> Bool +isSortSeq op1 (TSortSeq _ op2) = op1 == op2 +isSortSeq _ _ = False + +abbrvParamPatt :: MonadError String m => FParam -> m C.FPattern +abbrvParamPatt (pp, sorts) = case sorts of + Just sort | isStrictSort sort -> do + sort' <- simplifyFTerm sort + return $ C.PAnnotated p sort' + _ -> return p + where + p = case pp of + PPAny -> C.PWildCard + PPMetaVar mvar -> C.PMetaVar mvar + PPSeqMetaVar mvar op -> C.PSeqVar mvar op + +-- Interpret "f()" as a pattern matching an empty tuple argument +maybePattsToPatts :: Maybe [FPattern] -> [FPattern] +maybePattsToPatts Nothing = [] +maybePattsToPatts (Just []) = [ PSeq [] ] +maybePattsToPatts (Just ps) = ps + +entitiesOfStep :: C.FStep -> ([Name],[Name],[Name],[Name],[Name]) +entitiesOfStep st = ( map fst (C.stepInheritedEntities st) + , map (\(n,_,_) -> n) (C.stepMutableEntities st) + , map (\(n,_,_) -> n) (C.stepInputEntities st) + , map fst (C.stepOutputEntities st) + , map fst (C.stepControlEntities st) + ) + +entitiesOfPremiseStep :: C.FPremiseStep -> ([Name],[Name],[Name],[Name],[Name]) +entitiesOfPremiseStep st = + ( map fst (C.premiseInheritedEntities st) + , map (\(n,_,_) -> n) (C.premiseMutableEntities st) + , map (\(n,_,_) -> n) (C.premiseInputEntities st) + , map fst (C.premiseOutputEntities st) + , map fst (C.premiseControlEntities st) + ) + +-------------------------------------------------------------------- + +term2tpat :: C.FTerm -> C.TPattern +term2tpat t = case t of + C.TSortComputes f -> C.TPComputes (term2tpat f) + C.TSortComputesFrom f t -> C.TPComputesFrom (term2tpat f) (term2tpat t) + C.TSortSeq (C.TVar x) op -> C.TPSeqVar x op + C.TVar x -> C.TPVar x + C.TAny -> C.TPWildCard + C.TName nm -> C.TPADT nm [] + C.TApp nm ts -> C.TPADT nm (map term2tpat ts) + _ -> C.TPLit t diff --git a/src/Simplify/TargetToFunconModules.hs b/src/Simplify/TargetToFunconModules.hs new file mode 100644 --- /dev/null +++ b/src/Simplify/TargetToFunconModules.hs @@ -0,0 +1,124 @@ +{-# Language FlexibleContexts, ScopedTypeVariables, LambdaCase + , MultiParamTypeClasses, TupleSections, FlexibleInstances #-} + +module Simplify.TargetToFunconModules where + +import Control.Arrow ((***)) +import CCO.Component (Component, component) +import Data.Text (pack) + +-------------------------------------------------------------------- +import Funcons.EDSL (type_, Funcons(FValue), Values(..), FTerm(..), string__, DataTypeMembers(..), DataTypeAltt(..), pat2term) +import Types.SourceAbstractSyntax (Name, FLiteral(..)) +import Types.CoreAbstractSyntax (FSig(..), FTerm(TSeq), funconIsNullary, ConsSpec(..), DataTypeSpec(..), DataTypeAlt(..)) +import Types.TargetAbstractSyntax +import qualified Types.FunconModule as F +import Simplify.Utils +-------------------------------------------------------------------- + +-- require for forming a pipeline with uu-cco library +target2fmodule :: Bool -> Component CBSFile F.FunconModule +target2fmodule gen_ph = component (return . simplifyCBSFile gen_ph) + +simplifyCBSFile :: Bool -> CBSFile -> F.FunconModule +simplifyCBSFile gen_ph cbsfile = + let fspecs = concatMap (simplifyFunconSpec gen_ph) (funcons cbsfile) + in F.FunconModule fspecs + (entities cbsfile) + (map (gTypeMember (constructors cbsfile)) (datatypes cbsfile)) + (env cbsfile) + (aliases cbsfile) + +gTypeMember :: [ConsSpec] -> DataTypeSpec -> DataTypeMembers +gTypeMember css (DataTypeDecl nm typarams alts) = + DataTypeMemberss (pack nm) typarams (concatMap gAlts alts ++ gCons) + where gAlts (Types.CoreAbstractSyntax.DataTypeInclusion term) = + [Funcons.EDSL.DataTypeInclusionn term] + gCons = foldr op [] css + where op (ValCons cons _ args nm' tparams) acc + | nm == nm' = Funcons.EDSL.DataTypeMemberConstructor (pack cons) args (Just tparams):acc + | otherwise = acc + +simplifyFunconSpec :: Bool -> FunconSpec -> [F.FunconSpec] +simplifyFunconSpec gen_ph (FRules _ _ _ [] []) + | not gen_ph = [] -- remove funcons without rules +simplifyFunconSpec _ (FRules nm sig mdoc rewrites steps) = + let rewrites' = map (simplifyRewriteRule sig) rewrites + steps' = map (simplifyStepRule sig) steps + in [F.FunconSpec nm sig mdoc rewrites' steps'] + +simplifyRewriteRule :: FSig -> FRewriteRule -> [F.FRewriteStmt] +simplifyRewriteRule sig (FRewriteRule pats mterm sides) = + source ++ sideconditions ++ [target] + where source | funconIsNullary sig = [] + | otherwise = [F.ArgsPattern F.fargs_var pats] + sideconditions = map F.CheckSideCondition sides + target = F.RewriteTarget (maybe (TSeq []) id mterm) + +simplifyStepRule :: FSig -> FStepRule -> [F.FStepStmt] +simplifyStepRule sig (FStepRule fstep e_prem_sides) = + source_pat ++ + source_mut_ps ++ + source_inhs ++ + source_inps ++ + source_dsigs ++ + bar ++ + target_ctrls ++ + target_outs ++ + source_mut_ts ++ + [target] + where source_pat + | funconIsNullary sig = [] + | otherwise = [F.FRewriteStmt(F.ArgsPattern F.fargs_var pats)] + where pats = stepSource fstep + target = F.StepTarget (stepTarget fstep) + source_inhs = map (uncurry F.ReadInherited) + (stepInheritedEntities fstep) + (source_mut_ps,source_mut_ts) = + foldr op ([],[]) (stepMutableEntities fstep) + where op (nm,p,t) (ps,ts) = (F.ReadMutable nm p:ps + ,F.WriteMutable nm t:ts) + source_inps = map (uncurry F.ReadInput) (stepInputEntities fstep) + source_dsigs = map (uncurry F.ReadDownControl) (stepControlEntities fstep) + target_outs = map (uncurry F.WriteOutput) (stepOutputEntities fstep) + target_ctrls = map (uncurry F.WriteControl) + (map (id *** fmap pat2term) $ stepControlEntities fstep) + bar = concatMap sel e_prem_sides + where sel (Right side) = [F.FRewriteStmt + (F.CheckSideCondition side)] + sel (Left prem) = premToStmts prem + + premToStmts prem = muts_ts ++ [premise] ++ sigReads ++ muts_ps + where (muts_ts,muts_ps) = foldr op ([],[]) (premiseMutableEntities prem) + where op (nm,t,p) (ts,ps) = (F.WriteMutable nm t:ts + ,F.ReadMutable nm p:ps) + sigReads = map op (premiseControlEntities prem) + where op (nm,mpat) = F.ReadControl nm mpat + premise = + -- receive + flip (foldr out_op) (premiseOutputEntities prem) $ + receiveControl (premiseControlEntities prem) $ + -- scope + flip (foldr dsigs_op) (premiseControlEntities prem) $ + flip (foldr inhs_op) (premiseInheritedEntities prem) $ + flip (foldr inps_op) (premiseInputEntities prem) $ + (F.Premise (premiseSource prem) + (premiseTarget prem)) + where + out_op :: (Name,FPattern) -> F.FStepStmt -> F.FStepStmt + out_op (nm,pat) = F.ReceiveOutput nm pat + + inps_op :: (Name, [FTerm], InputAccess) -> F.FStepStmt + -> F.FStepStmt + inps_op (nm, fcts, acc) = F.ScopeInput nm fcts acc + + inhs_op :: (Name, FTerm) -> F.FStepStmt -> F.FStepStmt + inhs_op (nm, fct) = F.ScopeInherited nm fct + + dsigs_op :: (Name, Maybe FPattern) -> F.FStepStmt -> F.FStepStmt + dsigs_op (nm, fct) = F.ScopeDownControl nm (fmap pat2term fct) + + receiveControl ents + | null ents = id + | otherwise = F.ReceiveControl (map fst $ ents) + diff --git a/src/Simplify/TargetToIML.hs b/src/Simplify/TargetToIML.hs new file mode 100644 --- /dev/null +++ b/src/Simplify/TargetToIML.hs @@ -0,0 +1,737 @@ +{-# Language FlexibleContexts, ScopedTypeVariables, FlexibleInstances, + TupleSections, OverloadedStrings #-} + +module Simplify.TargetToIML where + +-------------------------------------------------------------------- +import Funcons.EDSL (Values(..), Funcons(FValue), isString_, unString, pat2term, typat2term) +import Types.SourceAbstractSyntax (Name, FLiteral(..), SeqSortOp(..),MetaVar, AliasMap, my_aliases) +import Types.CoreAbstractSyntax (FPattern(..), FTerm(..), isSeqVarSort, + FSideCondition(..), DataTypeSpec(..),DataTypeAlt(..), + EntitySpec(..), ConsSpec(..), FSig(..), Strictness(..)) +import Types.TargetAbstractSyntax +import Simplify.Utils +import qualified IML.Grammar as RF +import qualified IML.Grammar.Specs as IS +import qualified IML.Trans.ProMan as IML +import IML.Trans.FromFuncons (translate, remVarOp, translate_term) +import qualified Funcons.Operations as VAL +import IML.EDSL +------------------------------------------------------------------- + +import Control.Arrow ((***)) +import Control.Monad.Trans +import Control.Monad.Writer +import Control.Monad.State +import Data.Text (unpack,pack) +import Data.Map (assocs) +import Data.String (fromString) + +import System.IO.Unsafe +trace a b = unsafePerformIO (putStrLn a >> return b) + +-- | Type representing value constructors +type VCons = Name +type Cons = Name + +-- | The constructor used for the type-membership predicate +stepR, tyR :: RF.RSymb +stepR = "->" +rewVR = "~>" +tyR = "=ty=>" + +rewrite,step :: IsExprs exprs => exprs -> RuleBuilder () +step = commit stepR +rewrite = commit rewVR +type_member = commit tyR (RF.TVal (VAL.tobool True)) + +target2iml :: IML.Component CBSFile IS.HighSpec +target2iml = IML.component (\file -> return (execRuleBuilder (gCBSFile file))) + +lFSpec :: FunconSpec -> FunconSpec +lFSpec spec@(FRules nm sig mcs rs ss) = case sig of + FLazy -> spec + FNullary -> spec + FStrict -> FRules nm sig mcs rs' ss' + where FRules _ _ _ rs' ss' = lFSpec + (FRules nm (FPartiallyLazy [] (Just Strict)) mcs rs ss) + FPartiallyLazy ann mseqvar -> FRules nm sig mcs rs ss' + where ss' = map mkRule ruleKeys ++ seqvarRule ++ ss + ruleKeys = map fst $ filter ((Strict ==) . snd) keys + keys = zip [1..] ann + seqvarRule = case mseqvar of + Nothing -> [] + Just Lazy -> [] + Just Strict -> [rule] + where rule = FStepRule step (map Right scs ++ [Left premise]) + step = FStep (map mkPat (take (length ann) [1..]) ++ [PSeqVar "X*" StarOp]) + (TApp (pack nm) (map mkTerm (take (length ann) [1..]) ++ [TVar "Y*"])) + [] [] [] [] [] + where mkPat i = PMetaVar (mkVar i) + mkTerm i = TVar (mkVar i) + premise = FPremiseStep (TVar "X*") [PSeqVar "Y*" StarOp] [] [] [] [] [] + mkVar i = "X" ++ show i + scs = map mkSC ruleKeys + where mkSC i = SCIsInSort (TVar (mkVar i)) (TSortSeq (TName "values") QuestionMarkOp) + + mkRule k = FStepRule step [Left premise] + where step = FStep pats (TApp (pack nm) terms) [] [] [] [] [] + (pats,terms) = foldr op base keys + where base = case mseqvar of + Just _ -> ([PSeqVar "X*" StarOp] + ,[TVar "X*"]) + _ -> ([], []) + op (k',sness) (pats, terms) + | k' == k = (PMetaVar var:pats + ,TVar (var ++ "'") : terms) + | k' < k, Strict <- sness = + (PAnnotated (PMetaVar var) + (TName "values"):pats + ,TVar var : terms) + | True = (PMetaVar var : pats, TVar var : terms) + where var = "X" ++ show k' + premise = FPremiseStep (TVar var) [PMetaVar (var ++ "'")] + [] [] [] [] [] + where var = "X" ++ show k + + +gCBSFile :: CBSFile -> RuleBuilder () +gCBSFile cbsfile = do + {- THESE RELATIONS ARE NOW DECLARED IN main.iml + rel_decl stepR [{-IS.Repeatable-}] + rel_decl rewR [{-IS.Repeatable-}] + rel_decl tyR [] -- type-member relation + -} + mapM_ (gCBSSpec (aliases cbsfile)) (cbs cbsfile) + + {- THESE RULES ARE NOW SPECIFIED IN main.iml FILE + -- fall back rule for type-membership + -- that checks whether first argument is a value + [v1,v2,v3] <- mapM (const fresh_var) [1..3] + lhs (RF.PCons ty_cons [RF.PVar v1, RF.PVar v2]) + gRewrite (RF.TVar v1) (RF.PVar v3) + gRewrite (RF.TVar v2) (RF.PCons "values" []) + is_terminating stepR (RF.TVar v3) + commit tyR (RF.TVal (VAL.tobool True)) + -- fall back rule that determines non-membership + [v1,v2,v3,v4,v5] <- mapM (const fresh_var) [1..5] + lhs (RF.PCons ty_cons [RF.PVar v1, RF.PVar v2]) + gRewrite (RF.TVar v1) (RF.PVar v3) + gRewrite (RF.TVar v2) (RF.PVar v4) + pm (vop "type-member" [RF.TVar v3, RF.TVar v4]) (RF.PVar v5) + commit_prio 0 tyR (RF.TVar v5) + -} + +gCBSSpec :: AliasMap -> CBSSpec -> RuleBuilder () +gCBSSpec am (FunconSpec spec) = gFSpecWithMP_Aliases am (lFSpec spec) +gCBSSpec am (DataTypeSpec spec) = gData_Aliases am spec +gCBSSpec am (MetaSpec _) = return () +gCBSSpec am (EntitySpec spec) = gEntitySpec spec +gCBSSpec am (ConsSpec spec) = gCons_Aliases am spec + +gEntitySpec :: EntitySpec -> RuleBuilder () +gEntitySpec spec = case spec of + InheritedSpec n t -> ent_decl n [tTermAsExpr t] + MutableSpec n t -> ent_decl n [tTermAsExpr t] + OutputSpec n -> ent_decl n ([] :: [RF.Expr]) + InputSpec n -> ent_decl n ([] :: [RF.Expr]) + ControlSpec n -> ent_decl n ([] :: [RF.Expr]) + +gFSpecWithMP_Aliases :: AliasMap -> FunconSpec -> RuleBuilder() +gFSpecWithMP_Aliases am (FRules nm a b c d) = + forM_ (my_aliases nm am) (\nm' -> gFSpecWithMP (FRules nm' a b c d)) + +gFSpecWithMP :: FunconSpec -> RuleBuilder () +gFSpecWithMP spec@(FRules nm sig _ _ _) = gFSpec spec >> + astFuncons nm (Just 2)-- rules for meta-programming + where + gFSpec (FRules nm sig _ rs ss) = do + mapM_ (gRewriteRule sig nm) rs + mapM_ (gStepRule sig nm) ss + +mk_strict_lhs :: Name -> [RF.Pattern] -> RuleBuilder () +mk_strict_lhs nm pats = do + args_var <- fresh_var + add_var_decl_ (gVarDecl args_var (Just StarOp)) + lhs (RF.PCons nm [RF.PVar args_var]) + premise [RF.TVar args_var] (mRel rewVR) pats + +mk_partial_lhs :: Name -> [RF.Pattern] -> [RF.Pattern] -> RuleBuilder () +mk_partial_lhs nm init_pats rest_pats = do + arg_var <- fresh_var + add_var_decl_ (gVarDecl arg_var (Just StarOp)) + lhs (RF.PCons nm (init_pats ++ [RF.PVar arg_var])) + premise [RF.TVar arg_var] (mRel rewVR) rest_pats + +gRewriteRule :: FSig -> Name -> FRewriteRule -> RuleBuilder () +gRewriteRule sig nm (FRewriteRule source target bar) = do + pats <- mapM tFPattern source + case sig of FStrict -> mk_strict_lhs nm pats + FPartiallyLazy ann (Just Strict) -> mk_partial_lhs nm init_pats rest_pats + where (init_pats,rest_pats) = splitAt (length ann) pats + _ -> lhs (RF.PCons nm pats) + mapM gSideCond bar + rewrite $ case target of Nothing -> map RF.ETerm $ tTerm2Seq (TName "null") + Just t -> map RF.ETerm $ tTerm2Seq t +gStepRule :: FSig -> Name -> FStepRule -> RuleBuilder () +gStepRule sig nm (FStepRule fstep bar) = do + pats <- mapM tFPattern (stepSource fstep) + lhs (RF.PCons nm pats) + -- contextual/ inherited entities + ros <- mapM gRO (stepInheritedEntities fstep) + mapM_ (\(n, p, t) -> acc n p >> up n t) ros + -- mutable entities (IN) + forM (stepMutableEntities fstep) $ \(n,p,t) -> do + tFPattern p >>= acc n + -- TODO: input entities + -- * The "rest" of the input must be bound by a meta-var so that + -- the first premise can provide this as additional input +-- forM (stepInputEntities fstep) $ \(n, vars) -> +-- acc n =<< tSeqPattern (map PMetaVar vars) + + gConditions bar + -- control entities + forM (stepControlEntities fstep) $ \(n, mt) -> + acc n ([] :: [RF.Pattern]) >> + case mt of + Nothing -> up n ([] :: [RF.Term]) + Just t -> rewAndPut n (pat2term t) + -- mutable entities (OUT) + forM (stepMutableEntities fstep) $ \(n,p,t) -> do + rewAndPut n t + -- output entities + forM (stepOutputEntities fstep) $ \(n, t) -> do + var1 <- fresh_var + var2 <- fresh_var + add_var_decl_ (gVarDecl var1 (Just StarOp)) + add_var_decl_ (gVarDecl var2 (Just StarOp)) + acc n (RF.PVar var1) + gOptRewrite (tTerm2Seq t) [RF.PVar var2] + up n [RF.TVar var1, RF.TVar var2] + step (tTerm2Seq (stepTarget fstep)) +-- ros <- let op (n,p) = (n,) <$> tPattern p +-- in mapM op (stepInheritedEntities fstep) --acc +-- rws <- mapM rewriteMutVal (stepMutableEntities fstep) +-- wos1 <- mapM (uncurry rewriteOutVal) (stepOutputEntities fstep) +-- wos2 <- mapM (uncurry rewriteConVal) (stepControlEntities fstep) +-- let conditions = --concatMap (map Left . fst) wos1 ++ + --concatMap (map Left . fst) rws ++ + --concatMap (map Left . fst) wos2 ++ + where gRO (n,ps) = case ps of + [] -> return (n, [], []) + [PMetaVar var]-> return (n, [RF.PVar var], [RF.TVar var]) + [PWildCard] -> do var <- fresh_var + return (n, [RF.PVar var],[RF.TVar var]) + _ -> do var <- fresh_var + add_var_decl_ (gVarDecl var (Just StarOp)) + gSideCond (SCPatternMatch (TVar var) ps) + return (n, [RF.PVar var], [RF.TVar var]) + rewAndPut n t = do var <- fresh_var + gOptRewrite (tTerm2Seq t) [RF.PVar var] + up n (RF.TVar var) + +gConditions :: [Either FPremiseStep FSideCondition] -> RuleBuilder () +gConditions cs = mapM_ (mapeither gPremise gSideCond) cs + where mapeither f _ (Left e) = f e + mapeither _ f (Right e) = f e + +gPremise :: FPremiseStep -> RuleBuilder () +gPremise pstep = do + target' <- mapM tFPattern (premiseTarget pstep) + let source' = tTerm2Seq (premiseSource pstep) + var <- fresh_var + add_var_decl_ (gVarDecl var (Just StarOp)) + gOptRewrite source' [RF.PVar var] + -- contextual/inherited entities + inhI <- forM (premiseInheritedEntities pstep) $ \(n,t) -> do + var <- fresh_var + gOptRewrite (tTerm2Seq t) [RF.PVar var] + add_var_decl_ (gVarDecl var (Just StarOp)) + return (n, [RF.ETerm $ RF.TVar var]) + + -- mutable entities + mutI <- forM (premiseMutableEntities pstep) $ \(n,t,p) -> do + var <- fresh_var + gOptRewrite (tTerm2Seq t) [RF.PVar var] + return (n, [RF.ETerm (RF.TVar var)]) + mutO <- mapM (\(n,t,p) -> (n,) . (:[]) <$> tFPattern p) + (premiseMutableEntities pstep) + -- output entities + let outI = map (\(n,_) -> (n, [])) + (premiseOutputEntities pstep) + let matchOutList n p = case p of + (PValue (PADT "list" ps)) -> (n,) <$> tSeqPattern (map PValue ps) -- TODO pattern matching lists currently not supported, requires usage of destructors like `head` and `tail` + _ -> error "premise output not formed by a list of patterns" + outO <- mapM (uncurry matchOutList) (premiseOutputEntities pstep) + -- control entities + let ctrlI = map (\(n,_) -> (n, [])) + (premiseControlEntities pstep) + ctrlO <- forM (premiseControlEntities pstep) $ \(n,mp) -> case mp of + Just p -> (n,) . (:[]) <$> tFPattern p + Nothing -> return (n, []) + -- TODO: input entities + --ExtraInput determines that there is `other` input than provided by the terms + -- this input is the `left over' from the conclusion (or last premise?) + {- + inpI <- forM (premiseInputEntities pstep) $ \(n,vars,_) -> do + var <- fresh_var + gRewriteExpr (vop "list" (map tTerm vars)) (RF.PVar var) + return (n, RF.TVar var)-} + -- Check whether all provided input has been consumed. + -- If ExtraInput than more may be consumed + -- If ExactInput than inpO must be equal to [] + {- let inpO = map (\(n,_,access) -> -} +-- woaccs <- let op (n,p) = (n,) <$> tPattern p +-- opm (n,Nothing) = (n++"-nothing",) . RF.PVar <$> IML.fresh_var_ +-- opm (n,Just p) = op (n,p) +-- in (++) <$> mapM op (premiseOutputEntities pstep) +-- <*> mapM opm (premiseControlEntities pstep) +-- inhs <- mapM (uncurry rewriteOutVal) (premiseInheritedEntities pstep) +-- muts <- mapM rewriteMutVal (premiseMutableEntities pstep) +-- let roups = map snd inhs +-- rwups = map snd muts + let ins = inhI ++ mutI ++ outI ++ ctrlI -- ++ inpI + outs = mutO ++ outO ++ ctrlO -- ++ inpO + refocus_var <- fresh_var -- static refocussing 1/4 + add_var_decl_ (gVarDecl refocus_var (Just StarOp)) -- static refocussing 2/4 + premise (RF.TConf [RF.ETerm (RF.TVar var)] ins) stepR (RF.PConf [RF.PVar refocus_var] []) -- static refocussing 3/4 + premise (RF.TConf [RF.ETerm (RF.TVar refocus_var)] []) (mRel stepR) (RF.PConf target' outs) -- static refocussing 4/4 +-- premise (RF.TConf [RF.ETerm (RF.TVar var)] ins) stepR (RF.PConf target' outs) -- disabling static refocussing + +tSeqPattern :: [FPattern] -> RuleBuilder [RF.Pattern] +tSeqPattern ps = mapM tFPattern ps +{-foldM attach (RF.PCons nil_v []) . reverse + where attach acc p = do pat <- tPattern p + return (RF.PCons "cons" [pat, acc])-} + +gSideCond :: FSideCondition -> RuleBuilder () +gSideCond sc = + case sc of + SCEquality t1 t2 -> mkEquality t1 t2 truePat + SCInequality t1 t2 -> mkEquality t1 t2 falsePat + SCIsInSort t1 sort -> case sort of + TSortComplement sort' -> mkSort t1 sort' falsePat + _ -> mkSort t1 sort truePat + SCNotInSort t1 sort -> mkSort t1 sort falsePat + SCPatternMatch t ps -> do + ps' <- mapM tFPattern ps + gOptRewriteExpr (map RF.ETerm $ tTerm2Seq t) ps' + where mkEquality (TSeq []) t2 _ = gSideCond (SCPatternMatch t2 []) + mkEquality t1 (TSeq []) _ = gSideCond (SCPatternMatch t1 []) + mkEquality (TName "true") t _ = gRewriteTo (tTerm t) truePat + mkEquality t (TName "true") _ = gRewriteTo (tTerm t) truePat + mkEquality (TName "false") t _= gRewriteTo (tTerm t) falsePat + mkEquality t (TName "false") _= gRewriteTo (tTerm t) falsePat + mkEquality t1 t2 b = do + v1 <- fresh_var + gRewriteToVal (tTerm2Seq t1) v1 + v2 <- fresh_var + gRewriteToVal (tTerm2Seq t2) v2 + pm (vop "is-equal" [RF.TVar v1, RF.TVar v2]) b +{- mkSort (TVar v1) sort b + | let mop = last v1, mop == '*' || mop == '?' || mop == '+' = + let tup = TTuple [TVar v1] + seqs = TApp "tyseq" (TTuple [sort, TFuncon (FValue (String [mop]))]) + in mkSort tup seqs b-} + mkSort t1 sort b = + tycheck t1' sort' b --rewriting performed in rules for tychecking + where (t1',sort') = (tTerm2Seq t1, maybeApplyTySeq sort) + +tycheck :: [RF.Term] -> RF.Term -> RF.Pattern -> RuleBuilder () +tycheck vals ty b = premise (ty : vals) (mRel tyR) b + +tycheck_direct :: [RF.Term] -> RF.Term -> RF.Pattern -> RuleBuilder () +tycheck_direct vals ty b = premise (ty : vals) (sRel tyR) b + +maybeApplyTySeq :: FTerm -> RF.Term +maybeApplyTySeq sort + | isSeqVarSort sort = ty' + | otherwise = case tys of [ty] -> ty + _ -> ty' + where tys = tTerm2Seq sort + ty' = RF.TCons "tyseq" tys + +lit2Val :: VAL.HasValues t => FLiteral -> VAL.Values t +lit2Val lit = case lit of + FLiteralNat nat -> VAL.Nat (toInteger nat) + FLiteralFloat f -> VAL.Float f + FLiteralString s -> fromString s + FLiteralAtom c -> fromString c + + +-- | Assuming no other patterns than the conclusions' left-hand side +-- have annotation. For other patterns it is safe to use `tPattern` +tFPattern :: FPattern -> RuleBuilder RF.Pattern +tFPattern (PValue vpat) = tVPattern vpat +tFPattern (PAnnotated PWildCard sort) = do + v <- fresh_var + tFPattern (PAnnotated (PMetaVar v) sort) +tFPattern (PAnnotated (PMetaVar v) sort) = do + add_var_decl_ (gVarDecl v Nothing) + tycheck [RF.TVar v] (maybeApplyTySeq sort) truePat + return (RF.PVar v) +tFPattern (PAnnotated (PSeqVar v op) sort) + | v == "___" = fresh_var >>= \v' -> tFPattern (PAnnotated (PSeqVar v' op) sort) + | otherwise = do + add_var_decl_ (gVarDecl (remVarOp v) (Just op)) + tycheck [RF.TVar (remVarOp v)] (maybeApplyTySeq sort) truePat + return (RF.PVar (remVarOp v)) +tFPattern (PAnnotated p v) = error "unexpected annotation" +tFPattern (PMetaVar var) = return $ RF.PVar var +tFPattern (PSeqVar var op) + | var == "___" = fresh_var >>= \v' -> tFPattern (PSeqVar v' op) + | otherwise = do + add_var_decl_ (gVarDecl (remVarOp var) (Just op)) + return $ RF.PVar (remVarOp var) +tFPattern PWildCard = RF.PVar <$> fresh_var + +tVPattern :: VPattern -> RuleBuilder RF.Pattern +tVPattern (VPAnnotated VPWildCard sort) = do + v <- fresh_var + tVPattern (VPAnnotated (VPMetaVar v) sort) +tVPattern (VPAnnotated (VPMetaVar v) sort) = do + add_var_decl_ (gVarDecl v Nothing) + return (RF.PVar v) +tVPattern (VPAnnotated (VPSeqVar v op) sort) + | v == "___" = fresh_var >>= \v' -> tVPattern (VPAnnotated (VPSeqVar v' op) sort) + | otherwise = do + add_var_decl_ (gVarDecl (remVarOp v) (Just op)) + tycheck [RF.TVar (remVarOp v)] (maybeApplyTySeq sort) truePat + return (RF.PVar (remVarOp v)) +tVPattern (VPAnnotated p v) = error "unexpected annotation" +tVPattern (PADT cons ps) + -- TODO: generate variable with conditions that say that : + -- a) the matched value has `adt-constructor` equal to `string__ cons` + -- b) the matched value has `adt-fields` that match the patterns `ps` + | cons == "datatype-value", not (null ps) = do + p' <- tVPattern (head ps) + ps' <- mapM tVPattern (tail ps) + var_rewrite <- fresh_var + var <- fresh_var + gRewriteToVal [RF.TVar var_rewrite] var + premise (RF.TConf [RF.VOP "adt-constructor" [RF.ETerm $ RF.TVar var]] []) + (mRel rewVR) (RF.PConf [p'] []) + premise (RF.TConf [RF.ETerm $ RF.TCons "list-elements" + [RF.TCons "adt-fields" [RF.TVar var]]] []) + (mRel rewVR) (RF.PConf ps' []) + return (RF.PVar var_rewrite) --TODO rewrite to `var` instead?? + | otherwise = do + v <- fresh_var + pat' <- RF.PVal . VAL.ADTVal cons <$> mapM tVPattern ps + premise (toTConf (RF.TVar v)) (mRel rewVR) (toPConf pat') + return (RF.PVar v) +tVPattern VPWildCard = RF.PVar <$> fresh_var +tVPattern (VPMetaVar var) = return $ RF.PVar var +tVPattern (VPSeqVar var op) + | var == "___" = fresh_var >>= \v' -> tVPattern (VPSeqVar v' op) + | otherwise = do + add_var_decl_ (gVarDecl (remVarOp var) (Just op)) + return $ RF.PVar (remVarOp var) +tVPattern (VPLit lit) = return $ RF.PVal (VAL.vmap (RF.term2pattern . translate) lit) +tVPattern (VPType tpat) = tTPattern tpat + +tTPattern :: TPattern -> RuleBuilder RF.Pattern +tTPattern TPWildCard = RF.PVar <$> fresh_var +tTPattern (TPVar var) = return $ RF.PVar (remVarOp var) +tTPattern (TPSeqVar var op) + | var == "___" = fresh_var >>= \v' -> tTPattern (TPSeqVar v' op) + | otherwise = do + add_var_decl_ (gVarDecl (remVarOp var) (Just op)) + return $ RF.PVar (remVarOp var) +tTPattern (TPLit fterm) = error "missing translation for type-literals" +tTPattern (TPComputes tp) = RF.PVal . VAL.ADTVal "tycomp" . (:[]) <$> tTPattern tp +tTPattern (TPComputesFrom fp tp) = RF.PVal . VAL.ADTVal "tycomp" <$> mapM tTPattern [fp,tp] +tTPattern (TPADT cons ps) = RF.PVal . VAL.ComputationType . VAL.Type . VAL.ADT cons <$> mapM tTPattern ps + +tTerms :: [FTerm] -> [RF.Term] +tTerms = map tTerm + +tTermAsExpr :: FTerm -> RF.Expr +tTermAsExpr (TName nm) = RF.VOP (unpack nm) [] +tTermAsExpr (TApp nm ts) = RF.VOP (unpack nm) (map tTermAsExpr ts) +tTermAsExpr t = RF.ETerm (tTerm t) + +tTerm2Seq :: FTerm -> [RF.Term] +tTerm2Seq (TSeq ts) = concatMap tTerm2Seq ts +tTerm2Seq t = [tTerm t] + +tTerm :: FTerm -> RF.Term +tTerm = translate_term + +{- +tFuncons :: [Funcons] -> [RF.Term] +tFuncons = map tFuncon + +tFuncon :: Funcons -> RF.Term +tFuncon (FName nm) = RF.TCons False (unpack nm) [] +tFuncon (FApp nm f) = RF.TCons False (unpack nm) $ case f of + FTuple ts -> tFuncons ts + _ -> [tFuncon f] +tFuncon (FTuple fs) = RF.TCons False "tuple" (tFuncons fs) +tFuncon (FList fs) = RF.TCons False "list" (tFuncons fs) +tFuncon (FSet fs) = RF.TCons False "set" (tFuncons fs) +tFuncon (FMap fs) = RF.TCons False "map" (tFuncons fs) +tFuncon (FValue v) = trace "warning: missing value translations" + $ RF.TCons True "some-value" [] +tFuncon _ = error "missing Funcons translation" +-} + +gVarDecl :: RF.MVar -> Maybe SeqSortOp -> RF.VarDecl +gVarDecl x mop = RF.VarDecl x lb mub RF.Longest [] + where (lb,mub) = case mop of Just StarOp -> (0, Nothing) + Just PlusOp -> (1, Nothing) + Just QuestionMarkOp -> (0, Just 1) + Nothing -> (1, Just 1) + +is_terminating_or_null t = tycheck [t] (RF.TCons "tystar" [RF.TCons "values" []]) truePat + +gRewriteToValExpr :: [RF.Expr] -> RF.MVar -> RuleBuilder () +gRewriteToValExpr expr var = do + gOptRewriteExpr expr [RF.PVar var] + is_terminating_or_null (RF.TVar var) + +gRewriteToVal :: [RF.Term] -> RF.MVar -> RuleBuilder () +gRewriteToVal term = gRewriteToValExpr (map RF.ETerm term) + +gRewriteTo :: RF.Term -> RF.Pattern -> RuleBuilder() +gRewriteTo t p = gOptRewriteExpr [RF.ETerm t] [p] + +gOptRewriteExpr :: [RF.Expr] -> [RF.Pattern] -> RuleBuilder () +gOptRewriteExpr expr pat = premise expr (mRel rewVR) pat + +gOptRewrite :: [RF.Term] -> [RF.Pattern] -> RuleBuilder () +gOptRewrite term = gOptRewriteExpr (map RF.ETerm term) + +truePat, falsePat :: RF.Pattern +truePat = RF.PVal (VAL.tobool True) +falsePat = RF.PVal (VAL.tobool False) + +gData_Aliases :: AliasMap -> DataTypeSpec -> RuleBuilder () +gData_Aliases am (DataTypeDecl nm tyargs alts) = + forM_ (my_aliases nm am) (\nm' -> gData (DataTypeDecl nm' tyargs alts)) + +gData :: DataTypeSpec -> RuleBuilder () +gData d@(DataTypeDecl nm tyargs alts) = do + -- generate rules for inclusion constructors + gAlts d + --term_pc stepR (Right $ toVCons nm) + --term_pc rewVR (Right $ toVCons nm) + -- axiom for type + (vars,typats) <- unzip <$> mapM mkPat tyargs + pats <- mapM tTPattern typats + lhs (RF.PCons nm pats) + vars' <- forM vars $ \var -> do + var' <- fresh_var + gRewriteToVal [RF.TVar var] var' + return var' -- TODO share these rewrites with sidecons in bar1 + rewrite (VAL.ADT (pack nm) (map RF.TVar vars')) --rewrite + -- congruence rules + strictFCongs nm + -- type alternative for type -- no longer required since ADT-builtin + --typeMemberAltCons "types" [] nm (map snd tyargs) + astFuncons nm (Just $ length pats) -- meta-funcons for type + where mkPat :: TPattern -> RuleBuilder (MetaVar, TPattern) + mkPat tpat = case tpat of + TPVar var -> return (var, tpat) + TPSeqVar var op -> return (remVarOp var, tpat) + TPWildCard -> do var <- fresh_var + return (var, TPVar var) + _ -> error "unexpected type-parameter pattern" + +gAlts :: DataTypeSpec -> RuleBuilder () +gAlts dt@(DataTypeDecl _ _ alts) = mapM_ (gAlt dt) alts + +gAlt :: DataTypeSpec -> DataTypeAlt -> RuleBuilder () +gAlt (DataTypeDecl tyname tyargs _) alt = case alt of + DataTypeInclusion sort -> + typeMemberAltIncl tyname tyargs sort + +gCons_Aliases :: AliasMap -> ConsSpec -> RuleBuilder () +gCons_Aliases am (ValCons nm a b tynm d) = + forM_ (my_aliases nm am) (\nm' -> + forM_ (my_aliases tynm am) (\tynm' -> gCons (ValCons nm' a b tynm' d))) + +gCons :: ConsSpec -> RuleBuilder() +-- SIMPLIFICATION: all constructors are strict +gCons (ValCons nm _ argstys tynm typats) = do +-- gDataTypeValue nm -- rules for the operational behaviour of cons + typeMemberAltCons tynm typats nm argstys -- type-membership rule + astFuncons nm (Just nr_args) + where nr_args = length argstys + + +{- DataTypeMemberConstructor nm' args mtyargs -> do + --term_pc stepR (Right $ toVCons nm) + --term_pc rewVR (Right $ toVCons nm) + gDataTypeValue (length args) nm -- rules for the operational behaviour of cons + typeMemberAltCons tyname (maybe tyargs id mtyargs) nm args -- type-membership rule + astFuncons nm (length args) + where nm = unpack nm' +-} + +typeMemberAltIncl :: Name -> [TPattern] -> FTerm -> RuleBuilder () +typeMemberAltIncl tyname tyargs sort = do + v1 <- fresh_var + typats <- mapM tTPattern tyargs + lhs [RF.PVal (adt_type (pack tyname) typats), RF.PVar v1] + tycheck [RF.TVar v1] (maybeApplyTySeq sort) truePat + type_member + + -- TODO extend the `sorts` argument to contain information about the variable + -- in order to avoid generating sequence-variables where not necessary +typeMemberAltCons :: Name -> [TPattern] -> Name -> [FTerm] -> RuleBuilder () +typeMemberAltCons tyname tyargs nm sorts = do + typats <- mapM tTPattern tyargs + patvars <- forM sorts $ \sort -> do + var <- fresh_var + case mkSort sort of + Nothing -> do + tycheck [RF.TVar var] (maybeApplyTySeq sort) truePat + return var + Just op -> do + add_var_decl_ (gVarDecl var (Just op)) + tycheck [RF.TVar var] (maybeApplyTySeq sort) truePat + return var + lhs [RF.PVal (adt_type (pack tyname) typats) + ,RF.PVal (adt (pack nm) (map RF.PVar patvars))] + type_member + where mkSort t = case t of + TSortSeq t' op -> Just op + TSortPower _ _ -> Just StarOp + TVar var -> case last var of + '*' -> Just StarOp + '?' -> Just QuestionMarkOp + '+' -> Just PlusOp + _ -> Nothing + _ -> Nothing + +{- +gDataTypeValue :: Cons -> RuleBuilder () +gDataTypeValue cs = do -- build axiom + var <- fresh_var + lhs (RF.PCons cs [RF.PVar var]) + add_var_decl_ (gVarDecl var (Just StarOp)) + tycheck [RF.TVar var] (tTerm (TName "values")) truePat + rewrite (RF.TCons "datatype-value" (RF.TVal (fromString cs) : [RF.TVar var])) --rewrite + strictFCongs cs -- build congruences +-} + +strictFCongs :: Cons -> RuleBuilder () +strictFCongs cs = do + x_var <- fresh_var + x_var_rw<- fresh_var + x_var' <- fresh_var + lhs (RF.PCons cs [RF.PVar x_var]) + add_var_decl_ (gVarDecl x_var (Just StarOp)) + add_var_decl_ (gVarDecl x_var_rw (Just StarOp)) + add_var_decl_ (gVarDecl x_var' (Just StarOp)) + gOptRewrite [RF.TVar x_var] [RF.PVar x_var_rw] + premise (RF.TVar x_var_rw) (sRel stepR) (RF.PVar x_var') + commit (sRel stepR) (RF.TCons cs [RF.TVar x_var']) + +mkValOpRules :: [RF.Rule] +mkValOpRules = rules + where IS.Spec new = execRuleBuilder $ mapM_ (uncurry mkrule) + $ assocs (VAL.library :: VAL.Library RF.Term) + (_,_,_,_,rules) = IS.partition_decls new + + mkrule :: VAL.OP {- String, operation name -} -> VAL.ValueOp t -> RuleBuilder () + mkrule nm op = case op of + VAL.NullaryExpr _ -> build $ Just 0 + VAL.UnaryExpr _ -> build $ Just 1 + VAL.BinaryExpr _ -> build $ Just 2 + VAL.TernaryExpr _ -> build $ Just 3 + VAL.NaryExpr _ -> build Nothing + where + build marity = do + strictFCongs nm -- congruence rules + mkAxiom marity -- axiom + astFuncons nm marity --ast-* funcons + mkAxiom marity= case marity of + Just arity -> do + vars <- mapM (const fresh_var) [1..arity] + mk_strict_lhs nm (map RF.PVar vars) + vars' <- forM vars $ \var -> do -- termination side conditions + var' <- fresh_var + gSideCond (SCPatternMatch (TVar var) [PMetaVar var']) + is_terminating_or_null (RF.TVar var') + return var' + rewrite (vop nm (map RF.TVar vars')) + Nothing -> do + var <- fresh_var + lhs (RF.PCons nm [RF.PVar var]) + var' <- fresh_var + add_var_decl_ (gVarDecl var (Just StarOp)) + add_var_decl_ (gVarDecl var' (Just StarOp)) + gOptRewrite [RF.TVar var] [RF.PVar var'] + is_terminating_or_null (RF.TVar var') + rewrite (vop nm [RF.TVar var']) + + +-- meta-programming specific stuff + +ctR, dlR, ulR :: RF.RSymb +ctR = "=ct=>" +dlR = "=dl=>" +ulR = "=ul=>" + +ctRelRule :: Name -> RuleBuilder () +ctRelRule nm = do + var <- fresh_var + var' <- fresh_var + lhs (RF.PCons nm [RF.PVar var]) + var_decl var 0 Nothing RF.Longest [] + var_decl var' 0 Nothing RF.Longest [] + premise (RF.TVar var) ctR (RF.PVar var') + commit ctR (RF.TCons nm [RF.TVar var']) + +dlRelRule :: Name -> RuleBuilder () +dlRelRule nm = do + var <- fresh_var + var' <- fresh_var + lhs (RF.PVal (VAL.ADTVal (pack astv_nm) [RF.PVar var])) + var_decl var 0 Nothing RF.Longest [] + var_decl var' 0 Nothing RF.Longest [] + premise (RF.TVar var) dlR (RF.PVar var') + commit dlR (RF.TCons nm [RF.TVar var']) + where astv_nm = "astv-" ++ nm + +ulRelRule :: Name -> RuleBuilder () +ulRelRule nm = do + var <- fresh_var + var' <- fresh_var + lhs (RF.PCons nm [RF.PVar var]) + var_decl var 0 Nothing RF.Longest [] + var_decl var' 0 Nothing RF.Longest [] + premise (RF.TVar var) ulR (RF.PVar var') + commit ulR (RF.TCons astv_nm [RF.TVar var']) + where astv_nm = "astv-" ++ nm + +promoteRule :: Name -> RuleBuilder () +promoteRule nm = do + var <- fresh_var + lhs (RF.PCons nm [RF.PVar var]) + commit ulR (RF.TCons "astv-promote" [RF.TCons nm [RF.TVar var]]) + +-- +-- 1 Generate funcon for funcon named, say "scope", with arity 2 +-- > value constructor astv-scope with congruence rules +-- 2 Termination for value constructor +-- 3 Rule that types astv-scope(A:asts,B:asts) as asts +-- 4 astv-scope(A,B) =dl=> scope(Ac, Bc) +-- 5 scope(Ac,Bc) =ul=> astv-scope(A,B) +-- 6 astv-scope(A,B) =ct=> astv-scope(A,B) +-- 7 astv-scope(A,B) =ul=> astv-promote(astv-scope(A,B)) +astFuncons :: Name -> Maybe Int -> RuleBuilder() +astFuncons nm marity = return () {-do + ctRelRule nm + --term_pc stepR (Right $ "astv-" ++ nm) -- 2 + --term_pc rewR (Right $ "astv-" ++ nm) -- 2 + gDataTypeValue astv_nm -- 1a + typeMemberAltCons "asts" [] astv_nm [TSortSeq (TName "asts") StarOp] --3 + dlRelRule nm -- 4 + ulRelRule nm -- 5 + ctRelRule astv_nm -- 6 + promoteRule astv_nm + where astv_nm = "astv-" ++ nm +-} diff --git a/src/Simplify/Utils.hs b/src/Simplify/Utils.hs new file mode 100644 --- /dev/null +++ b/src/Simplify/Utils.hs @@ -0,0 +1,49 @@ +{-# LANGUAGE ScopedTypeVariables #-} + +module Simplify.Utils where + +import Data.List (sortBy) +import Data.Ord (comparing) + +import Control.Applicative +import Control.Monad.Except + +import Funcons.EDSL (SeqSortOp(..), Funcons(..), Values(..), string__) +import Funcons.Operations hiding (Values) + +import Types.SourceAbstractSyntax (FLiteral(..)) + +guardM :: MonadError e m => Bool -> e -> m () +guardM True _ = return () +guardM False e = throwError e + +mergeAssocListsM :: forall k e m a b. (Ord k, MonadError e m) => e -> [(k,a)] -> [(k,b)] -> m [(k,a,b)] +mergeAssocListsM e kas kbs = sequence $ zipWith mergeM (sortBy (comparing fst) kas) (sortBy (comparing fst) kbs) + where + mergeM :: (k,a) -> (k,b) -> m (k,a,b) + mergeM (n1,p) (n2,t) = do guardM (n1 == n2) e + return (n1,p,t) + +traverseEither :: Applicative m => (a -> m c) -> (b -> m d) -> Either a b -> m (Either c d) +traverseEither f _ (Left a) = Left <$> f a +traverseEither _ g (Right b) = Right <$> g b + +lookup2 :: Eq a => a -> [(a,b,c)] -> Maybe (b,c) +lookup2 _ [] = Nothing +lookup2 k ((a,b,c):abcs) = if a == k then Just (b,c) else lookup2 a abcs + +isSeqVar :: String -> Maybe SeqSortOp +isSeqVar var + | last var == '*' = return StarOp + | last var == '+' = return PlusOp + | last var == '?' = return QuestionMarkOp + | otherwise = Nothing + +simplifyLiteral :: FLiteral -> Values +simplifyLiteral lit = case lit of + FLiteralNat n -> Nat (toInteger n) + FLiteralAtom char | length char == 1 -> Char (head char) + | otherwise -> error "atom of size != 1" + FLiteralString str -> string__ str + FLiteralFloat f -> Float f + diff --git a/src/Types/Bindings.hs b/src/Types/Bindings.hs new file mode 100644 --- /dev/null +++ b/src/Types/Bindings.hs @@ -0,0 +1,78 @@ +module Types.Bindings where + +import Types.SourceAbstractSyntax (MetaVar) + +import qualified Types.CoreAbstractSyntax as C + +import qualified Data.Set as S + +class HasPatVar a where + pvars :: a -> S.Set MetaVar + +instance HasPatVar a => HasPatVar [a] where + pvars c = S.unions $ fmap pvars c + +instance (HasPatVar a, HasPatVar b) => HasPatVar (Either a b) where + pvars (Left l) = pvars l + pvars (Right r) = pvars r + +instance (HasPatVar a) => HasPatVar (Maybe a) where + pvars (Just j) = pvars j + pvars Nothing = S.empty + +instance HasPatVar C.FRewriteRule where + pvars (C.FRewriteRule ps _ ss) = pvars ps `S.union` pvars ss + +instance HasPatVar C.FPattern where + pvars p = case p of + C.PMetaVar v -> S.singleton v + C.PSeqVar v _ -> S.singleton v + C.PAnnotated pat _ -> pvars pat + C.PWildCard -> S.empty + C.PValue vpat -> pvars vpat + +instance HasPatVar C.VPattern where + pvars p = case p of + C.PADT _ ps -> S.unions $ fmap pvars ps + C.VPWildCard -> S.empty +-- C.PList ps -> S.unions $ fmap pvars ps + C.VPMetaVar var -> S.singleton var + C.VPSeqVar var _ -> S.singleton var + C.VPLit _ -> S.empty + C.VPAnnotated pat _ -> pvars pat + C.VPType tpat -> pvars tpat + +instance HasPatVar C.TPattern where + pvars p = case p of + C.TPWildCard -> S.empty + C.TPVar var -> S.singleton var + C.TPSeqVar var _ -> S.singleton var + C.TPLit _ -> S.empty + C.TPComputes pat -> pvars pat + C.TPComputesFrom f t -> pvars f `S.union` pvars t + C.TPADT _ ps -> S.unions $ fmap pvars ps + +instance HasPatVar C.FSideCondition where + pvars sc = case sc of + C.SCPatternMatch _ p -> pvars p + _ -> S.empty + +instance HasPatVar C.FStepRule where + pvars (C.FStepRule step scs) = pvars step `S.union` pvars scs + +instance HasPatVar C.FStep where + pvars step = pvars (C.stepSource step) + `S.union` pvars (map snd $ C.stepInheritedEntities step) + `S.union` pvars (map (\(_,x,_) -> x) $ C.stepMutableEntities step) + `S.union` pvars (concatMap (\(_,x,_) -> x) $ C.stepInputEntities step) + `S.union` S.fromList (concatMap (\(_,_,x) -> x) $ C.stepInputEntities step) + `S.union` pvars (map snd $ C.stepControlEntities step) + +instance HasPatVar C.FPremiseStep where + pvars premise = pvars (C.premiseTarget premise) + `S.union` pvars (map (\(_,_,x) -> x) $ C.premiseMutableEntities premise) + `S.union` S.fromList (concatMap (\(_,_,x) -> maybe [] (:[]) x) $ C.premiseInputEntities premise) + `S.union` pvars (map snd $ C.premiseOutputEntities premise) + `S.union` pvars (map snd $ C.premiseControlEntities premise) + + diff --git a/src/Types/ConcreteSyntax.hs b/src/Types/ConcreteSyntax.hs new file mode 100644 --- /dev/null +++ b/src/Types/ConcreteSyntax.hs @@ -0,0 +1,311 @@ + +module Types.ConcreteSyntax where + +import Funcons.EDSL (SeqSortOp(..)) + +import Data.List (intercalate) + +type Name = String + +type Var = Maybe String {- wildcard otherwise -} +showVar Nothing = "_" +showVar (Just x) = x + +type CBSFile = [CBSSpec] + +data CBSSpec = Auxiliary CBSSpec + | AliasSpec Name Name + | FunconSpec Name (Maybe Params) Term (Maybe DefRewrite) + | TypeSpec Name (Maybe Params) [Bounds] (Maybe DefRewrite) + | DatatypeSpec Name (Maybe Params) (Maybe Bounds) [DatatypeAlt] + | EntitySpec Entity + | SyntaxSpec [Prod] + | LexisSpec [Prod] + | SemanticsSpec Name Var PhraseType (Maybe Params) Term (Maybe DefEqual) {- [Rule] -} + {- RuleSpec and CommentSpec are not necessary for funcon generation + however, how to ignore them at parse time without causing ambiguity + and possible inefficiency? -} + | RuleSpec Rule + | OtherwiseSpec Rule + | CommentSpec [CommentPart] + | MetaSpec MetaSpec + | MetaVariablesSpec [VarDecl] + deriving Show + +newtype DefRewrite = DefRewrite Term deriving Show +newtype DefEqual = DefEqual Term deriving Show + +data VarDecl = VarDeclSubType String Term + | VarDeclType String Term + deriving Show + +data MetaSpec = HS_Imports String {- to be directly copied into a HS module -} + deriving Show + +type Params = [Param] +data Param = Param Var (Maybe Bounds) + deriving Show + +data Bounds = InType Type + | Sub Type + | Sup Type + deriving Show + +data DatatypeAlt = Cons Name (Maybe Params) + | Inj Var Type + | AltDots + deriving Show + +type Type = Term +showType = showConcreteTerm + +data Term = TermConst Const + | TermVar Var + | TermDots + | TermName Name + | NameApp Name Term + | VarApp Var Term + | Typed Term Type + | Computes Type + | ComputesFrom Type Type + | TermPostfix Type SeqSortOp + | TermSequence [Term] -- wrapped inside 'group' + | TermComplement Term + | TermUnion Type Type + | TermInter Type Type + | TermTuple [Term] + | TermList [Term] + | TermSet [Term] + | TermMap [Maybe (Term, Term)] --nothing when "..." + | TermPower Term Term + -- semantic translation + | SemanticsApp Name PhraseTerm (Maybe Term) + deriving Show + +-- | Smart constructor to replace `TermTuple` that prevents singleton tuples +termTuple :: [Term] -> Term +termTuple [t] = t +termTuple ts = TermTuple ts + +termName :: Term -> Name +termName (NameApp nm _) = nm +termName (TermName nm) = nm +termName t = error ("termName: " ++ show t) + +termArgs :: Term -> Maybe [Term] +termArgs (NameApp nm arg) = case arg of + TermTuple [] -> Nothing + TermTuple args -> Just args + _ -> Just [arg] +termArgs _ = Nothing + +data Const = ConstAtom String + | ConstString String + | ConstNat Int + | ConstFloat Double + deriving Show + +showConst c = case c of + ConstAtom str -> "'" ++ str ++ "'" + ConstString str -> show str + ConstNat i -> show i + ConstFloat d -> show d + +showConcreteTerm :: Term -> String +showConcreteTerm t = case t of + TermConst c -> showConst c + TermVar x -> showVar x + TermDots -> "..." + TermComplement t2 -> "~" ++ showConcreteTerm t2 + TermName n -> n + NameApp n t2 -> n ++ showConcreteTerm t2 + VarApp x t2 -> showVar x ++ showConcreteTerm t2 + Typed t2 ty -> showConcreteTerm t2 ++ ":" ++ showType ty + Computes ty -> "=>" ++ showType ty + ComputesFrom fty tty -> showType fty ++ "=>" ++ showType tty + TermPostfix ty op -> showType ty ++ show op + TermSequence seq -> intercalate "," (map showConcreteTerm seq) + TermUnion t1 t2 -> showConcreteTerm t1 ++ "|" ++ showConcreteTerm t2 + TermInter t1 t2 -> showConcreteTerm t1 ++ "&" ++ showConcreteTerm t2 + TermTuple ts -> "(" ++ showConcreteTerm (TermSequence ts) ++ ")" + TermList ts -> "[" ++ showConcreteTerm (TermSequence ts) ++ "]" + TermSet ts -> "{" ++ showConcreteTerm (TermSequence ts) ++ "}" + TermMap mkvs -> "{" ++ intercalate "," (map showMKV mkvs) ++ "}" + TermPower t1 t2 -> showConcreteTerm t1 ++ "^" ++ showConcreteTerm t2 + SemanticsApp nm sxs Nothing -> nm ++ "[[" ++ concatMap showPhraseTerm sxs ++ "]]" + SemanticsApp nm sxs (Just ty2) -> showConcreteTerm (SemanticsApp nm sxs Nothing) ++ + "(" ++ showConcreteTerm ty2 ++ ")" + where + showMKV mkv = case mkv of + Nothing -> "..." + Just (k, v) -> showConcreteTerm k ++ "|->" ++ showConcreteTerm v + +data Rule = Inference [Premise] Conclusion + -- semantics + | Desugar PhrasePatt PhraseType PhraseTerm + | Semantics Name PhrasePatt (Maybe Term) [Term] + deriving Show + +type PhrasePatt = [WordPatt] +type PhraseTerm = [WordTerm] +data PhraseType = PTSynName Name + | PTAtom Atom + | PTRange Atom Atom + | PTPostfix PhraseType SeqSortOp + | PTComplement PhraseType + | PTSeq PhraseType PhraseType + | PTNoLayout PhraseType PhraseType + | PTUnion PhraseType PhraseType + | PTGroup (Maybe PhraseType) + deriving (Show) + +data WordTerm = WTVar Var + | WTAtom String + | WTGroup [WordTerm] + deriving (Show) + +data Premise = PremDynamic (Maybe Context) State Dynamic State + | PremTyping (Maybe Context) State Term + | PremStatic (Maybe Context) State Term Static State + | PremRewrite Term Term + | PremEquality Term Term + | PremInequality Term Term + | PremSubtype Term Term + deriving (Show) + +premSource :: Premise -> Term +premSource (PremRewrite t1 _) = t1 +premSource (PremStatic _ s _ _ _) = stateTerm s +premSource (PremTyping _ s _) = stateTerm s +premSource (PremDynamic _ s _ _) = stateTerm s +premSource (PremEquality t _) = t +premSource (PremInequality t _) = t +premSource (PremSubtype t _) = t + +premTarget :: Premise -> Term +premTarget (PremRewrite _ t) = t +premTarget (PremStatic _ _ _ _ s) = stateTerm s +premTarget (PremTyping _ _ t) = t -- type +premTarget (PremDynamic _ _ _ s) = stateTerm s +premTarget (PremEquality _ t) = t +premTarget (PremInequality _ t) = t +premTarget (PremSubtype _ t) = t + +data Conclusion = ConcDynamic (Maybe Context) State Dynamic State + | ConcTyping (Maybe Context) State Term + | ConcStatic (Maybe Context) State Term Static State + | ConcRewrite Term Term + deriving (Show) + +concSource :: Conclusion -> Term +concSource (ConcRewrite t1 _) = t1 +concSource (ConcStatic _ s _ _ _) = stateTerm s +concSource (ConcTyping _ s _) = stateTerm s +concSource (ConcDynamic _ s _ _) = stateTerm s + +concTarget :: Conclusion -> Term +concTarget (ConcRewrite _ t) = t +concTarget (ConcStatic _ _ _ _ s) = stateTerm s +concTarget (ConcTyping _ _ t) = t -- type +concTarget (ConcDynamic _ _ _ s) = stateTerm s + +data State = StateExplicit Term [EntTerm] + | StateImplicit Term + deriving (Show) + +stateTerm :: State -> Term +stateTerm (StateExplicit t _) = t +stateTerm (StateImplicit t) = t + +stateEnts :: State -> [EntTerm] +stateEnts (StateExplicit _ es) = es +stateEnts (StateImplicit _) = [] + +data Dynamic = DynamicExplicit [PolarEntTerm] (Maybe Int) -- premise id + | DynamicImplicit (Maybe Int) --premise id + | DynamicComposition Dynamic Dynamic + deriving Show + +dynamicEnts :: Dynamic -> [PolarEntTerm] +dynamicEnts (DynamicExplicit ps _) = ps +dynamicEnts _ = [] + +data Static = StaticExplicit [PolarEntTerm] + | StaticImplicit + deriving Show + +data WordPatt = WPVar Var + | WPAtom String + | WPGroup [WordPatt] + | WPUnion Atom [Atom] + deriving (Show) + +type Atom = String + +showPhraseTerm :: WordTerm -> String +showPhraseTerm wt = case wt of + WTVar x -> showVar x + WTAtom a -> "'" ++ a ++ "'" + WTGroup wts -> "(" ++ concatMap showPhraseTerm wts ++ ")" + +data Entity = EntContextual Ent Arrow + | EntMutable Ent Arrow Ent + | EntObservable EntArrow + deriving Show + +data Arrow = ADynamic | AStatic + deriving Show +data EntArrow = EADynamic Ent | EAStatic Ent + deriving Show + +type EntTerm = (Name, Term) +type PolarEntTerm = (Name, Term, Maybe Polarity) + +data Ent = EntVarStem VarStem (Maybe Polarity) + | EntName Name (Maybe Polarity) Var Term + deriving Show + +data Polarity = In | Out + deriving (Show, Enum) + +data Context = Context [EntTerm] deriving Show + +contextEnts :: Maybe Context -> [EntTerm] +contextEnts = maybe [] (\(Context es) -> es) + +data Pred = PredType Term + | PredSubType Term + deriving Show + +data CommentPart = Ordinary String + | Asterisk + | At String + | CommentTerm [Term] + | CommentPremise Premise + | SpecInComment CBSSpec + deriving Show + + +showComments :: [CommentPart] -> String +showComments = concatMap showComment + +showComment :: CommentPart -> String +showComment (Ordinary c) = c +showComment (Asterisk) = "*" +showComment (At sect) = "@" ++ sect +-- TODO should use showFuncons, but requires static substitute + simplification +showComment (CommentTerm t) = "`" ++ show t ++ "`" +showComment c = "" + + +data Prod = Prod [VarStem] SynName PhraseType -- lists of alternatives + | SDFComment [CommentPart] + deriving Show + +type VarStem = String +type SynName = String +data VarSynName = VarName VarStem SynName + | SynName String + deriving Show + + diff --git a/src/Types/CoreAbstractSyntax.hs b/src/Types/CoreAbstractSyntax.hs new file mode 100644 --- /dev/null +++ b/src/Types/CoreAbstractSyntax.hs @@ -0,0 +1,162 @@ +{-# LANGUAGE LambdaCase, OverloadedStrings #-} + +-- This is a simplified version of SourceAbstractSyntax. +-- Information not needed for code generation has been discarded. +module Types.CoreAbstractSyntax ( + -- copies of source + CBSFile(..), CBSSpec(..), EntitySpec(..),FunconSpec(..),FSig(..),FStep(..), + FPremiseStep(..), FSideCondition(..), DataTypeSpec(..), DataTypeAlt(..), + FSort, + -- defined here + FStepRule(..), Strictness(..), FRewriteRule(..), + isStrict, isSeqVarSort, funconIsStrict, funconIsNullary, CommentPart(..), + ConsSpec(..),CSig(..), + -- defined in the interpreter + FTerm(..),TypeEnv, FPattern(..), VPattern(..), TPattern(..),TyAssoc(..), + )where + +import Funcons.EDSL (FTerm(..), FPattern(..), VPattern(..), TPattern(..), TypeEnv(..), TyAssoc(..), HasTypeVar(..)) + +import Types.ConcreteSyntax (MetaSpec(..), Term, Premise) +import Types.SourceAbstractSyntax hiding (CBSFile,CBSSpec,EntitySpec,FunconSpec,FSig(..),FStep,FPremiseStep,FSideCondition,DataTypeSpec(..), FTerm(..), FPattern(..),FSort(..),TypeEnv, TyAssoc(..), DataTypeAlt(..),FPattern(..), CommentPart(..)) + +data CBSFile = CBSFile {cbs :: [CBSSpec], env :: TypeEnv, aliases :: AliasMap} + +data CBSSpec = FunconSpec FunconSpec + | DataTypeSpec DataTypeSpec + | EntitySpec EntitySpec + | MetaSpec MetaSpec + | ConsSpec ConsSpec + deriving (Show) + +data EntitySpec = InheritedSpec Name FTerm + | MutableSpec Name FTerm + | InputSpec Name + | OutputSpec Name + | ControlSpec Name + deriving (Show) + +data FunconSpec = FRules Name FSig (Maybe [CommentPart]) [FRewriteRule] [FStepRule] + deriving (Show) + +data ConsSpec = ValCons Name -- constructor name + CSig -- datatype or type constructor? + [FSort] -- the types the arguments should have + Name -- name of type for which it constructs values + [TPattern] -- type params for type (required for GADTs) + deriving (Show) + +data CommentPart = Ordinary String + | Asterisk + | At String + | CommentTerm [Term] + | CommentPremise Premise + | SpecInComment CBSSpec + deriving Show + +data FSig = FStrict -- fully strict, possibly variadic + | FLazy -- fully non-strict, possibly variadic + | FPartiallyLazy [Strictness] -- mixed strict, non-variadic + (Maybe Strictness) -- zero or more args with this strictness + | FNullary -- no arguments + deriving (Eq,Ord,Show) + +data CSig = DataTypeCons + | TypeCons FSig + deriving (Show) + +funconIsStrict :: FSig -> Bool +funconIsStrict = \case FStrict -> True + _ -> False + +funconIsNullary :: FSig -> Bool +funconIsNullary = \case FNullary -> True + _ -> False + +data Strictness = Strict | Lazy + deriving (Eq,Ord,Show) + +isStrict Strict = True +isStrict Lazy = False + +data FRewriteRule = FRewriteRule [FPattern] (Maybe FTerm) [FSideCondition] + deriving (Eq,Ord,Show) + +data FStepRule = FStepRule FStep [Either FPremiseStep FSideCondition] + deriving (Eq,Ord,Show) + +data FStep = FStep + { stepSource :: [FPattern] + , stepTarget :: FTerm + , stepInheritedEntities :: [(Name,[FPattern])] + , stepMutableEntities :: [(Name,FPattern,FTerm)] + , stepInputEntities :: [(Name,[FPattern],[MetaVar])] + , stepOutputEntities :: [(Name,FTerm)] + , stepControlEntities :: [(Name,Maybe FPattern)] + } + deriving (Eq,Ord,Show) + +data FPremiseStep = FPremiseStep + { premiseSource :: FTerm + , premiseTarget :: [FPattern] + , premiseInheritedEntities :: [(Name,FTerm)] + , premiseMutableEntities :: [(Name,FTerm,FPattern)] + , premiseInputEntities :: [(Name,[FTerm],Maybe MetaVar)] + , premiseOutputEntities :: [(Name,FPattern)] + , premiseControlEntities :: [(Name,Maybe FPattern)] + } + deriving (Eq,Ord,Show) + +data FSideCondition = SCEquality FTerm FTerm + | SCInequality FTerm FTerm + | SCPatternMatch FTerm [FPattern] + | SCIsInSort FTerm FSort + | SCNotInSort FTerm FSort + deriving (Eq,Ord,Show) + +type FSort = FTerm + +termComputes :: FSort -> Bool +termComputes (TSortComputes _) = True +termComputes (TSortComputesFrom _ _) = True +termComputes _ = False + +isSeqVarSort :: FSort -> Bool +isSeqVarSort (TVar var) = seqChar (last var) + where seqChar c = case c of '*' -> True + '?' -> True + '+' -> True + _ -> False +isSeqVarSort _ = False + +data DataTypeSpec = DataTypeDecl Name [TPattern] [DataTypeAlt] + deriving (Show) + +data DataTypeAlt = DataTypeInclusion FSort + deriving (Eq,Ord,Show) + +{- +data FPattern = PTuple [FPattern] + | PList [FPattern] + | PAnnotated FPattern FSort + | PADT ADTConstructor [FPattern] + | PAny + | PLit FLiteral + | PMetaVar MetaVar + | PSeqMetaVar MetaVar SeqSortOp -- Note: the MetaVar should also contain the operator suffix + deriving (Eq,Ord,Show) +-} +------------------------------------------------- + +{- +instance HasTypeVar FPattern where + subsTypeVarWildcard mt env pat = case pat of + PAnnotated p t -> PAnnotated (subsTypeVarWildcard mt env p) (subsTypeVarWildcard mt env t) + PADT n pats -> PADT n (map (subsTypeVarWildcard mt env) pats) + PTuple pats -> PTuple (map (subsTypeVarWildcard mt env) pats) + PList pats -> PList (map (subsTypeVarWildcard mt env) pats) + PMetaVar var -> PMetaVar var + PSeqMetaVar var op -> PSeqMetaVar var op + PLit v -> PLit v + PAny -> PAny +-} diff --git a/src/Types/FunconModule.hs b/src/Types/FunconModule.hs new file mode 100644 --- /dev/null +++ b/src/Types/FunconModule.hs @@ -0,0 +1,68 @@ + +module Types.FunconModule where + +import Funcons.EDSL(DataTypeMembers(..)) +import Types.SourceAbstractSyntax (Name, MetaVar, AliasMap) +import Types.CoreAbstractSyntax (FSig(..), EntitySpec(..), FPattern(..) + , FTerm(..), FSideCondition, CommentPart(..), TypeEnv) +import Types.TargetAbstractSyntax (InputAccess) + +data FunconModule = FunconModule { funcons :: [FunconSpec] + , entities :: [EntitySpec] + , datatypes :: [DataTypeMembers] + , env :: TypeEnv + , aliases :: AliasMap } + +-- A funcon: +-- * Has a name +-- * Is either strict, lazy or partially lazy +-- * Has a number of rewrite rules (each a sequence of rewrite statements) +-- * Has a number of step rules (each a sequence of step statements) +data FunconSpec = FunconSpec Name FSig (Maybe [CommentPart]) [[FRewriteStmt]] [[FStepStmt]] + +-- | Representation of a variable in the target language (Haskell/Java) +type TargetVar = String + +fargs_var, env_var, empty_env :: TargetVar +empty_env = "emptyEnv" +fargs_var = "fargs" +env_var = "env" + +-- an entity value is either: +-- * read : just ask the monad to get the value +-- * written : just insert the value into the monad +-- * scoped : execute further computation with given entity value +-- * received : what is the value after computation? +data FStepStmt + = FRewriteStmt FRewriteStmt -- subtyping + | ReadInherited Name [FPattern] + | ScopeInherited Name FTerm FStepStmt --set inh for the next stmt + | WriteMutable Name FTerm + | ReadMutable Name FPattern + | ReceiveControl [Name] FStepStmt + | ReadControl Name (Maybe FPattern) + | WriteControl Name (Maybe FTerm) + | ReadDownControl Name (Maybe FPattern) + | ScopeDownControl Name (Maybe FTerm) FStepStmt + | ReceiveOutput Name FPattern FStepStmt + | WriteOutput Name FTerm + | ReadInput Name [FPattern] + | ScopeInput Name [FTerm] InputAccess{-exact?-} FStepStmt + | PremiseBlock FStepStmt -- groups statements particular to a premise + | Premise FTerm [FPattern] + | StepTarget FTerm + | SBranches [[FStepStmt]] + deriving (Ord, Eq) + +-- subtype of FStepStmt +-- define two evaluation, 1 producing code for rewrite rules, 1 for steps +-- (applying lifted version of helpers) +data FRewriteStmt + = ArgsPattern TargetVar [FPattern] -- match a sequence of funcons + | EnvStore MetaVar FTerm -- bind var to term in the meta-environment + | EnvRewrite MetaVar -- rewrite var inside the meta-environment + | CheckSideCondition FSideCondition + | RewriteTarget FTerm + | RBranches [[FRewriteStmt]] + deriving (Ord, Eq) + diff --git a/src/Types/SourceAbstractSyntax.hs b/src/Types/SourceAbstractSyntax.hs new file mode 100644 --- /dev/null +++ b/src/Types/SourceAbstractSyntax.hs @@ -0,0 +1,183 @@ +module Types.SourceAbstractSyntax ( + -- defined here + CBSFile(..), CBSSpec(..), TypeSynonymSpec(..), DataTypeSpec(..), + EntitySpec(..), FunconSpec(..), FRule(..), FSideCondition(..), + FSig(..), FParam(..), ParamPattern(..), Name, FStep(..), FPremiseStep(..), + FPattern(..), FLiteral(..), ADTConstructor, + FSort, TypeEnv, TyAssoc(..), AliasMap, my_aliases, + MetaVar, FTerm(..), DataTypeAlt(..), + CommentPart(..), isStrictParam, isStrictSort, termArgs, isVariadic, + -- defined in Funcons.EDSL + SeqSortOp(..), + ) where + +import Funcons.EDSL (SeqSortOp(..)) +import Types.ConcreteSyntax (MetaSpec(..), Term, Premise) + +import qualified Data.Map as M + +type Name = String + +data CBSFile = CBSFile {cbs :: [CBSSpec], env :: TypeEnv, aliases :: AliasMap } + +type TypeEnv = M.Map MetaVar TyAssoc +data TyAssoc = ElemOf FSort | SubTyOf FSort +type AliasMap = M.Map Name [Name] + +my_aliases :: Name -> AliasMap -> [Name] +my_aliases nm als = my_aliases' [] nm als + where my_aliases' ctx nm als + | nm `elem` ctx = error "cyclic aliases" + | otherwise = nm : concatMap (\n -> my_aliases' (nm:ctx) n als) + (maybe [] id (M.lookup nm als)) + +data CBSSpec = FunconSpec FunconSpec + | TypeSynonymSpec TypeSynonymSpec + | DataTypeSpec DataTypeSpec + | TypeSpec DataTypeSpec + | EntitySpec EntitySpec + | MetaSpec MetaSpec + deriving (Show) + +data TypeSynonymSpec = TypeSynonymDecl Name [FParam] FSort + deriving (Show) + +data DataTypeSpec = DataTypeDecl Name [FParam] [DataTypeAlt] + deriving (Show) + +data DataTypeAlt = DataTypeInclusion FSort + | DataTypeConstructor Name [FSort] + deriving (Eq,Ord,Show) + +data EntitySpec = InheritedSpec (Name,FTerm,FSort) + | MutableSpec (Name,FTerm,FSort) (Name,FPattern,FSort) + | InputSpec (Name,FPattern,FSort) + | OutputSpec (Name,FPattern,FSort) + | ControlSpec (Name,FSort) + deriving (Show) + +data FunconSpec = FAbbrv FSig (Maybe FTerm) {- nothing if := ... -} + | FRules FSig [FRule] + deriving (Show) + +data FRule = FRuleRewrite Name (Maybe [FPattern]) (Maybe FTerm) [FSideCondition] + | FRuleStep Name FStep [Either FPremiseStep FSideCondition] + deriving (Eq,Ord,Show) + +data FSideCondition = SCEquality FTerm FTerm + | SCInequality FTerm FTerm + | SCPatternMatch FTerm [FPattern] + | SCIsInSort FTerm FSort + deriving (Eq,Ord,Show) + +data FSig = FSig + { sigName :: Name, + sigParams :: [FParam], + sigSort :: FSort, + sigDoc :: Maybe [CommentPart] + } + deriving (Show) + +data CommentPart = Ordinary String + | Asterisk + | At String + | CommentTerm [Term] + | CommentPremise Premise + | SpecInComment CBSSpec + deriving Show + + + +type FParam = (ParamPattern, Maybe FSort) + +isStrictParam :: FParam -> Bool +isStrictParam param@(_,sorts) = maybe False isStrictSort sorts + +isStrictSort :: FSort -> Bool +isStrictSort sort = case sort of + TSortSeq (TTuple [t]) _ -> isStrictSort t + TSortSeq t _ -> isStrictSort t + TSortComputes _ -> False + TSortComputesFrom _ _ -> False + _ -> True + +isVariadic :: FParam -> Bool +isVariadic (_, Just (TSortSeq _ _)) = True +isVariadic _ = False + +data ParamPattern = PPMetaVar MetaVar + | PPSeqMetaVar MetaVar SeqSortOp + | PPAny + deriving (Eq,Ord,Show) + +data FStep = FStep + { stepSource :: Maybe [FPattern] + , stepTarget :: FTerm + , stepInheritedEntities :: [(Name,[FPattern])] + , stepMutableEntities :: ([(Name,FPattern)],[(Name,FTerm)]) + , stepInputEntities :: [(Name,FPattern)] + , stepOutputEntities :: [(Name,FTerm)] + , stepControlEntities :: [(Name,FPattern)] + } + deriving (Eq,Ord,Show) + +data FPremiseStep = FPremiseStep + { premiseSource :: FTerm + , premiseTarget :: [FPattern] + , premiseInheritedEntities :: [(Name,FTerm)] + , premiseMutableEntities :: ([(Name,FTerm)],[(Name,FPattern)]) + , premiseInputEntities :: [(Name,FTerm)] + , premiseOutputEntities :: [(Name,FPattern)] + , premiseControlEntities :: [(Name,FPattern)] + } + deriving (Eq,Ord,Show) + +data FPattern = PSeq [FPattern] + | PList [FPattern] + | PAnnotated FPattern FSort + | PADT ADTConstructor [FPattern] + | PAny + | PLit FLiteral + | PMetaVar MetaVar + | PSeqMetaVar MetaVar SeqSortOp -- Note: the MetaVar should also contain the operator suffix + deriving (Eq,Ord,Show) + +data FLiteral = FLiteralNat Int + | FLiteralFloat Double + | FLiteralString String + | FLiteralAtom String + deriving (Eq,Ord,Show) + +type ADTConstructor = String + + +type FSort = FTerm + +type MetaVar = String + +data FTerm = TMetaVar MetaVar + | TLiteral FLiteral + | TName Name + | TApp Name [FTerm] + | TTuple [FTerm] + | TList [FTerm] + | TSet [FTerm] + | TMap [FTerm] + | TBinding FTerm FTerm + | TSortPower FTerm FTerm + | TSortUnion FTerm FTerm + | TSortInter FTerm FTerm + | TSortComplement FTerm + | TSortSeq FTerm SeqSortOp + | TSortComputes FTerm + | TSortComputesFrom FTerm FTerm + | TAny + deriving (Eq,Ord,Show) + +termArgs :: FTerm -> Maybe [FTerm] +termArgs t = case t of + TName _ -> Nothing + TApp _ ts -> Just ts + _ -> Nothing + +------------------------------------------------- diff --git a/src/Types/TargetAbstractSyntax.hs b/src/Types/TargetAbstractSyntax.hs new file mode 100644 --- /dev/null +++ b/src/Types/TargetAbstractSyntax.hs @@ -0,0 +1,129 @@ +-- This is a version of CoreAbstractSyntax +-- with some modifications helpful towards code-generation. +-- Information not needed for code generation has been discarded. +module Types.TargetAbstractSyntax + (module Types.TargetAbstractSyntax + ,TPattern(..), FCT.FPattern(..), VPattern(..)) where + +import Types.ConcreteSyntax (MetaSpec) +import Types.SourceAbstractSyntax hiding (CBSFile(..),CBSSpec(..),EntitySpec,FunconSpec,FSig,FStep(..),FPremiseStep(..),FSideCondition(..),DataTypeAlt(..), DataTypeSpec(..),FTerm(..),FPattern(..), CommentPart(..),cbs, FValSort, TypeEnv) +import Types.CoreAbstractSyntax hiding (CBSSpec(..),FunconSpec(..),FStepRule(..),FRewriteRule(..),FStep(..),FPremiseStep(..),CBSFile(..),cbs) +import Funcons.EDSL (TypeEnv, HasTypeVar(..), TPattern(..), VPattern(..)) +import qualified Funcons.EDSL as FCT + +data CBSFile = CBSFile {cbs :: [CBSSpec], env :: TypeEnv, aliases :: AliasMap} + +data CBSSpec = FunconSpec FunconSpec + | DataTypeSpec DataTypeSpec + | EntitySpec EntitySpec + | MetaSpec MetaSpec + | ConsSpec ConsSpec + deriving (Show) + +funcons :: CBSFile -> [FunconSpec] +entities :: CBSFile -> [EntitySpec] +datatypes :: CBSFile -> [DataTypeSpec] +metadata :: CBSFile -> [MetaSpec] +constructors :: CBSFile -> [ConsSpec] + +funcons = foldr op [] . cbs + where op (FunconSpec f) xs = (f:xs) + op _ xs = xs +entities = foldr op [] . cbs + where op (EntitySpec e) xs = e:xs + op _ xs = xs +datatypes = foldr op [] . cbs + where op (DataTypeSpec d) xs = d:xs + op _ xs = xs +metadata = foldr op [] . cbs + where op (MetaSpec f) xs = f:xs + op _ xs = xs +constructors = foldr op [] . cbs + where op (ConsSpec f) xs = f:xs + op _ xs = xs + +doToFuncons :: (FunconSpec -> FunconSpec) -> CBSFile -> CBSFile +doToFuncons f file = file{cbs = map op $ cbs file} + where op (FunconSpec spec) = FunconSpec (f spec) + op spec = spec + +-- TODO migrate commentpart to meta-data? +data FunconSpec = FRules Name FSig (Maybe [CommentPart]) [FRewriteRule] [FStepRule] + deriving (Show) + +data FStepRule = FStepRule FStep [Either FPremiseStep FSideCondition] + deriving (Show) + +data FRewriteRule = FRewriteRule [FPattern] (Maybe FTerm) [FSideCondition] + deriving (Show) + +data FStep = FStep + { stepSource :: [FPattern] + , stepTarget :: FTerm + , stepInheritedEntities :: [(Name,[FPattern])] + , stepMutableEntities :: [(Name,FPattern,FTerm)] + , stepInputEntities :: [(Name,[FPattern])] + , stepOutputEntities :: [(Name,FTerm)] + , stepControlEntities :: [(Name,Maybe FPattern)] + } + deriving (Eq,Ord,Show) + +data FPremiseStep = FPremiseStep + { premiseSource :: FTerm + , premiseTarget :: [FPattern] + , premiseInheritedEntities :: [(Name,FTerm)] + , premiseMutableEntities :: [(Name,FTerm,FPattern)] + , premiseInputEntities :: [(Name,[FTerm],InputAccess)] + , premiseOutputEntities :: [(Name,FPattern)] + , premiseControlEntities :: [(Name,Maybe FPattern)] + } + deriving (Eq,Ord,Show) + +data InputAccess = ExactInput | ExtraInput + deriving (Eq,Ord,Show) + +instance HasTypeVar FSideCondition where + subsTypeVarWildcard mt env sc = case sc of + SCIsInSort t ty -> SCIsInSort t (subsTypeVarWildcard mt env ty) + SCNotInSort t ty -> SCNotInSort t (subsTypeVarWildcard mt env ty) + SCPatternMatch t pat -> SCPatternMatch t (subsTypeVarWildcard mt env pat) + SCEquality t1 t2 -> SCEquality t1 t2 + SCInequality t1 t2 -> SCInequality t1 t2 + +instance (HasTypeVar a, HasTypeVar b) => HasTypeVar (Either a b) where + subsTypeVarWildcard mt env (Left l) = Left $ subsTypeVarWildcard mt env l + subsTypeVarWildcard mt env (Right r) = Right $ subsTypeVarWildcard mt env r + +instance (HasTypeVar a) => HasTypeVar (Maybe a) where + subsTypeVarWildcard mt env = fmap (subsTypeVarWildcard mt env) +instance (HasTypeVar a) => HasTypeVar [a] where + subsTypeVarWildcard mt env = fmap (subsTypeVarWildcard mt env) + +instance HasTypeVar FStepRule where + subsTypeVarWildcard mt env (FStepRule step scs) = FStepRule (subsTypeVarWildcard mt env step) (subsTypeVarWildcard mt env scs) + +instance HasTypeVar FRewriteRule where + subsTypeVarWildcard mt env (FRewriteRule pats t scs) = FRewriteRule (subsTypeVarWildcard mt env pats) (subsTypeVarWildcard mt env t) (subsTypeVarWildcard mt env scs) + +instance HasTypeVar FStep where + subsTypeVarWildcard mt env step = step {stepSource = subsTypeVarWildcard mt env (stepSource step) + ,stepInheritedEntities = map (subs2of2 env) (stepInheritedEntities step) + ,stepMutableEntities = map (subs2of3 env) (stepMutableEntities step) + ,stepInputEntities = map (subs2of2 env) (stepInputEntities step) + ,stepControlEntities = map (subs2of2 env) (stepControlEntities step)} + +instance HasTypeVar FPremiseStep where + subsTypeVarWildcard mt env step = step {premiseTarget = subsTypeVarWildcard mt env (premiseTarget step) + ,premiseMutableEntities = map (subs3of3 env) (premiseMutableEntities step) + ,premiseOutputEntities = map (subs2of2 env) (premiseOutputEntities step) + ,premiseControlEntities = map (subs2of2 env) (premiseControlEntities step)} + +subs2of2 :: HasTypeVar b => TypeEnv -> (a, b) -> (a, b) +subs2of2 env (a,b) = (a, subsTypeVar env b) + +subs2of3 :: HasTypeVar b => TypeEnv -> (a,b,c) -> (a,b,c) +subs2of3 env (a,b,c) = (a, subsTypeVar env b,c) + +subs3of3 :: HasTypeVar c => TypeEnv -> (a,b,c) -> (a,b,c) +subs3of3 env (a,b,c) = (a, b, subsTypeVar env c) +