packages feed

funcons-intgen (empty) → 0.2.0.1

raw patch · 25 files changed

+4453/−0 lines, 25 filesdep +basedep +containersdep +directorysetup-changed

Dependencies added: base, containers, directory, filepath, funcons-tools, funcons-values, gll, iml-tools, mtl, pretty, regex-applicative, split, text, uu-cco

Files

+ LICENSE view
@@ -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.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ funcons-intgen.cabal view
@@ -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 <ltvanbinsbergen@acm.org>, Neil Sculthorpe <n.a.sculthorpe@swansea.ac.uk>+maintainer:          L. Thomas van Binsbergen <ltvanbinsbergen@acm.org>+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
+ src/Main.hs view
@@ -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 <CBS-PATH> <SRC-DIR> <LANG>\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 ++
+ src/Parsing/Lexer.hs view
@@ -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+-}++
+ src/Parsing/Mutual.hs view
@@ -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"
+ src/Parsing/Rule.hs view
@@ -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 '|'))
+ src/Parsing/Spec.hs view
@@ -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++
+ src/Parsing/Syntax.hs view
@@ -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
+ src/Parsing/Term.hs view
@@ -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
+ src/Print/HaskellModule.hs view
@@ -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  -> "<PREMISE>"+  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"
+ src/Print/Util.hs view
@@ -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]
+ src/Simplify/ConcreteToAbstract.hs view
@@ -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+
+ src/Simplify/CoreToTarget.hs view
@@ -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++--------------------------------------------------------------------
+ src/Simplify/LiftStrictness.hs view
@@ -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
+ src/Simplify/Simplifier.hs view
@@ -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
+ src/Simplify/TargetToFunconModules.hs view
@@ -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)+
+ src/Simplify/TargetToIML.hs view
@@ -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+-}
+ src/Simplify/Utils.hs view
@@ -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+
+ src/Types/Bindings.hs view
@@ -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)++
+ src/Types/ConcreteSyntax.hs view
@@ -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 = "<missing comment-part>"+++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++
+ src/Types/CoreAbstractSyntax.hs view
@@ -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+-}
+ src/Types/FunconModule.hs view
@@ -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)+
+ src/Types/SourceAbstractSyntax.hs view
@@ -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++-------------------------------------------------
+ src/Types/TargetAbstractSyntax.hs view
@@ -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)+