diff --git a/assets/gen-hslibrary.sh b/assets/gen-hslibrary.sh new file mode 100644 --- /dev/null +++ b/assets/gen-hslibrary.sh @@ -0,0 +1,107 @@ +#!/bin/bash +# e.g. $1 = Core, $2 = cbs/ +LANG=$1 +HSLANG=${LANG//-/} +HSDIR=${2%/} +LIBRARYPATH="$HSDIR/Funcons/$HSLANG" +LIBRARY="$LIBRARYPATH/Library.hs" +LIBRARYMOD="Funcons.$HSLANG.Library" +LANGMOD="Funcons.$HSLANG" + +if [[ -z ${1+x} || -z ${2+x} ]]; then + echo "usage: gen-hslibrary.sh + for example: ./gen-hslibrary.sh CamlLight hs-gen/" + exit +fi + +echo "Generating funcon library" + +FILES=$(find $HSDIR/Funcons -type f -name "*.hs") +echo "module $LIBRARYMOD (" > $LIBRARY + +echo " funcons, entities, types," >> $LIBRARY + +for full in $FILES +do + path=${full##"$LIBRARYPATH/"} + if [ $path != "Library.hs" ]; then + strippath=${path%".hs"} + mod=$LANGMOD"."${strippath//"/"/"."} + echo " module $mod," >> $LIBRARY + fi +done +echo " ) where " >> $LIBRARY + + +echo "import Funcons.EDSL" >> $LIBRARY +if [ "Core" != "$LANG" ]; then + echo "import Funcons.Tools" >> $LIBRARY +fi + +for full in $FILES +do + path=${full##"$LIBRARYPATH/"} + if [ $path != "Library.hs" ]; then + strippath=${path%".hs"} + mod=$LANGMOD"."${strippath//"/"/"."} + echo "import $mod hiding (funcons,types,entities)" >> $LIBRARY + echo "import qualified $mod" >> $LIBRARY + fi +done + +if [ "Core" != "$LANG" ]; then + echo "main = mkMainWithLibraryEntitiesTypes funcons entities types" >> $LIBRARY +fi +echo "funcons = libUnions" >> $LIBRARY +echo " [" >> $LIBRARY + +for full in $FILES +do + path=${full##"$LIBRARYPATH/"} + if [ $path != "Library.hs" ]; then + ((i++)) + strippath=${path%".hs"} + mod=$LANGMOD"."${strippath//"/"/"."} + if [ "$i" -gt 1 ]; then + comma="," + fi + echo " $comma $mod.funcons" >> $LIBRARY + fi +done +echo " ]" >> $LIBRARY + +comma="" +echo "entities = concat " >> $LIBRARY +echo " [" >> $LIBRARY +for full in $FILES +do + path=${full##"$LIBRARYPATH/"} + if [ $path != "Library.hs" ]; then + ((j++)) + strippath=${path%".hs"} + mod=$LANGMOD"."${strippath//"/"/"."} + if [ "$j" -gt 1 ]; then + comma="," + fi + echo " $comma $mod.entities" >> $LIBRARY + fi +done +echo " ]" >> $LIBRARY + +comma="" +echo "types = typeEnvUnions " >> $LIBRARY +echo " [" >> $LIBRARY +for full in $FILES +do + path=${full##"$LIBRARYPATH/"} + if [ $path != "Library.hs" ]; then + ((h++)) + strippath=${path%".hs"} + mod=$LANGMOD"."${strippath//"/"/"."} + if [ "$h" -gt 1 ]; then + comma="," + fi + echo " $comma $mod.types" >> $LIBRARY + fi +done +echo " ]" >> $LIBRARY diff --git a/assets/gen-hss-cbsc.sh b/assets/gen-hss-cbsc.sh new file mode 100644 --- /dev/null +++ b/assets/gen-hss-cbsc.sh @@ -0,0 +1,30 @@ +#!/bin/bash + +## e.g. to generate Unstables-Funcons-Beta +## $1 = Core, $2 = cbs/, #3 = Unstable-Funcons-Beta/ + +CBSC=cbsc +FDIR=${3%/}/$4 +HSDIR=${2%/} +LANG=$1 +HSLANG=${LANG//-/} +LIBRARYPATH=$HSDIR/Funcons/$LANG +LIBRARY=$LIBRARYPATH/Library.hs +LIBRARYMOD="Funcons.$HSLANG.Library" + +if [[ -z ${3+x} || -z ${2+x} || -z ${1+x} ]]; then + echo "usage: gen-hss.sh + for example: ./gen-hss.hs CamlLight hs-gen/ ../Funcons" + exit +fi +echo "Generating Haskell modules in $HSDIR for language $LANG ($HSLANG) from .cbs files found in $FDIR." + +function run-compile { + ${CBSC} ${i} ${HSDIR} ${LANG} +} + +#find $FDIR -type f -name "*.cbs" -exec $CBSC {} $HSDIR $LANG \; +for i in $(find $FDIR -type f -name "*.cbs") +do + run-compile $i +done diff --git a/funcons-intgen.cabal b/funcons-intgen.cabal --- a/funcons-intgen.cabal +++ b/funcons-intgen.cabal @@ -1,5 +1,6 @@ name: funcons-intgen -version: 0.2.0.1 +description: Transpiler generating Haskell micro-interpreters from CBS funcon definitions, see [Executable Component-Based Semantics](https://doi.org/10.1016/j.jlamp.2018.12.004) +version: 0.2.0.3 synopsis: Generate Funcons interpreters from CBS description files homepage: http://plancomps.org license: MIT @@ -10,6 +11,7 @@ category: Compilers build-type: Simple cabal-version: >=1.10 +extra-source-files: assets/*.sh executable cbsc main-is: Main.hs @@ -20,15 +22,12 @@ 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, @@ -36,20 +35,19 @@ 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 + build-depends: base >=4.8 && < 5 + ,containers >= 0.5 && < 0.7 + ,filepath >= 1.3.0 && < 2 + ,directory >= 1.3.8.5 && < 2 + ,split >= 0.2.5 && < 0.3 + ,pretty >= 1.1.2 && < 1.2 + ,text >= 1.2 && < 3 + ,mtl >= 2.2.1 && < 3 + ,gll >=0.4.1 && < 5 + ,regex-applicative >= 0.3 && < 0.4 + ,funcons-values >= 0.1.0.9 && < 0.2 + ,funcons-tools >= 0.2.0.16 && < 0.3 + ,uu-cco==0.1.0.6 && < 0.2 hs-source-dirs: src default-language: Haskell2010 ghc-options: -fwarn-incomplete-patterns diff --git a/src/Main.hs b/src/Main.hs --- a/src/Main.hs +++ b/src/Main.hs @@ -6,21 +6,14 @@ 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) @@ -29,8 +22,6 @@ 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 @@ -44,35 +35,24 @@ \LANG: the language for which the .cbs file contains a specification.\n" run cbsfile srcdir lang options = do - when (not toIML) (putStrLn ("Generating " ++ cbsfile)) + 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 + fmodule <- ioRun (target2fmodule pholder) target + m_contents <- ioRun ((cbs2 options) cbsfile srcdir lang) fmodule + case m_contents of + Nothing -> putStrLn "No funcons, types or entities to generate" + Just make_contents -> make_contents where pholder = any (== "--generate-unspecified-funcons") options - toIML = any (== "--IML") options cbs2 :: [String] -> FilePath -> Maybe FilePath -> Maybe String -> CCO.Component.Component FunconModule (Maybe (IO ())) cbs2 options {-| "--java" `elem` options = cbs2classes | "--ascii" `elem` options = cbs2ascii | otherwise -} = cbs2module - -run_iml iml options = do - let chain | "--LaTeX" `elem` options = spec2latex_module >>> component_ show - | otherwise = spec2highstring - printable <- runComponentIO (IML.Trans.ProMan.runOptions options) chain iml - putStrLn printable diff --git a/src/Parsing/Spec.hs b/src/Parsing/Spec.hs --- a/src/Parsing/Spec.hs +++ b/src/Parsing/Spec.hs @@ -135,6 +135,10 @@ <||> CommentTerm <$$ token "TICK" <**> multipleSepBy1 pTerm (keychar ',') <** token "TICK" <||> CommentPremise <$$ token "TICK" <** token "TICK" <**> pPremise <** token "TICK" <** token "TICK" + <||> CommentPhraseType <$$ token "TICK" <** token "TICK" <**> pPhraseType + <** token "TICK" <** token "TICK" + <||> CommentProds <$$ token "TICK" <** token "TICK" <**> multiple1 pProd + <** token "TICK" <** token "TICK" <||> SpecInComment <$$ token "TICK" <** token "TICK" <** token "TICK" <**> pSpec <** token "TICK" <** token "TICK" <** token "TICK" diff --git a/src/Print/HaskellModule.hs b/src/Print/HaskellModule.hs --- a/src/Print/HaskellModule.hs +++ b/src/Print/HaskellModule.hs @@ -15,10 +15,9 @@ import CCO.Component -import Prelude hiding ((<$>)) +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) @@ -56,7 +55,8 @@ 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" + \import Funcons." ++ camelcase lang ++ ".Library\n\ + \main = mkMainWithLibraryEntitiesTypes funcons entities types" (Just srcdir, _) -> do writeFile (srcdir hs_file_name FP.<.> "hs") (render' doc) putStrLn ("Generated " ++ (hs_file_name FP.<.> "hs")) @@ -315,9 +315,9 @@ readInh nm pat = text env_var <<-> text fgetINHPatt <+> gString nm <+> ppVPatterns pat <+> text env_var -readInhMut :: String -> Name -> FPattern -> Doc +readInhMut :: String -> Name -> [FPattern] -> Doc readInhMut entitytype nm pat = text env_var <<-> text entitytype <+> - gString nm <+> parens (ppVPattern pat) <+> text env_var + gString nm <+> ppVPatterns pat <+> text env_var writeMutable :: Name -> FTerm -> Doc writeMutable nm term = text fputMUTTerm <+> gString nm <+> diff --git a/src/Print/Util.hs b/src/Print/Util.hs --- a/src/Print/Util.hs +++ b/src/Print/Util.hs @@ -2,6 +2,8 @@ module Print.Util where +import Prelude hiding ((<>)) + import Types.SourceAbstractSyntax (SeqSortOp(..)) import Types.CoreAbstractSyntax @@ -139,4 +141,4 @@ splitDirectories $ dropFileName $ dropExtension file - roots = ["Funcons", "Funcons-beta", lang] + roots = ["Funcons", "Funcons-beta", "Unstable-Funcons-beta", lang] diff --git a/src/Simplify/ConcreteToAbstract.hs b/src/Simplify/ConcreteToAbstract.hs --- a/src/Simplify/ConcreteToAbstract.hs +++ b/src/Simplify/ConcreteToAbstract.hs @@ -11,7 +11,7 @@ import CCO.Feedback import CCO.Printing -import Control.Applicative +import Control.Monad (forM) import Control.Monad.Except import Data.Either (rights) @@ -289,6 +289,7 @@ TermComplement _ -> throwError "sort-complement in pattern" TermTuple ts -> S.PSeq <$> terms2pats ts TermList ts -> S.PList <$> terms2pats ts + TermSet [] -> return S.PEmptySet TermSet ts -> throwError "set notation in pattern" TermMap ts -> throwError "map notation in pattern" TermPower t1 t2 -> throwError "term power in pattern" diff --git a/src/Simplify/CoreToTarget.hs b/src/Simplify/CoreToTarget.hs --- a/src/Simplify/CoreToTarget.hs +++ b/src/Simplify/CoreToTarget.hs @@ -10,20 +10,16 @@ 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 Funcons.EDSL (string_, limitedSubsTypeVarWildcard, showOp, SeqSortOp(..)) import Types.SourceAbstractSyntax (Name, MetaVar) import Types.Bindings(HasPatVar(..)) @@ -131,7 +127,8 @@ { T.stepSource = stepSource st , T.stepTarget = stepTarget st , T.stepInheritedEntities = stepInheritedEntities st - , T.stepMutableEntities = stepMutableEntities st + , T.stepMutableEntitiesSource = stepMutableEntitiesSource st + , T.stepMutableEntitiesTarget = stepMutableEntitiesTarget st , T.stepInputEntities = map (\(n,ps,_) -> (n,ps)) (stepInputEntities st) , T.stepOutputEntities = stepOutputEntities st @@ -150,7 +147,8 @@ { T.premiseSource = premiseSource pst , T.premiseTarget = premiseTarget pst , T.premiseInheritedEntities = premiseInheritedEntities pst - , T.premiseMutableEntities = premiseMutableEntities pst + , T.premiseMutableEntitiesSource = premiseMutableEntitiesSource pst + , T.premiseMutableEntitiesTarget = premiseMutableEntitiesTarget pst , T.premiseInputEntities = map simplifyInputEntityPremise (premiseInputEntities pst) , T.premiseOutputEntities = premiseOutputEntities pst , T.premiseControlEntities = premiseControlEntities pst diff --git a/src/Simplify/LiftStrictness.hs b/src/Simplify/LiftStrictness.hs --- a/src/Simplify/LiftStrictness.hs +++ b/src/Simplify/LiftStrictness.hs @@ -4,7 +4,7 @@ import Types.SourceAbstractSyntax (SeqSortOp(..)) import Types.CoreAbstractSyntax (FSig(..), FTerm(..), FPattern (..) - ,Strictness(..),FSideCondition(..)) + ,Strictness(..)) import Types.TargetAbstractSyntax hiding (FPattern(..)) import Data.Text (pack) @@ -28,8 +28,8 @@ ,PMetaVar "X" ,PSeqVar "Y*" StarOp] (TApp (pack nm) [TVar "V*", TVar "X'", TVar "Y*"]) - [] [] [] [] [] - premise = FPremiseStep (TVar "X") [PMetaVar "X'"] [] [] [] [] [] + [] [] [] [] [] [] + premise = FPremiseStep (TVar "X") [PMetaVar "X'"] [] [] [] [] [] [] {- moved to TargetToIML rewrule = FRewriteRule [PSeqVar "X*" StarOp] (Just (TApp (pack nm) [TVar "Y*"])) [cond] @@ -43,7 +43,7 @@ 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) [] [] [] [] [] + where step = FStep pats (TApp (pack nm) terms) [] [] [] [] [] [] (pats,terms) = foldr op base keys where base = case mseqvar of Just _ -> ([PSeqVar "X*" StarOp] @@ -59,5 +59,5 @@ | True = (PMetaVar var : pats, TVar var : terms) where var = "X" ++ show k' premise = FPremiseStep (TVar var) [PMetaVar (var ++ "'")] - [] [] [] [] [] + [] [] [] [] [] [] where var = "X" ++ show k diff --git a/src/Simplify/Simplifier.hs b/src/Simplify/Simplifier.hs --- a/src/Simplify/Simplifier.hs +++ b/src/Simplify/Simplifier.hs @@ -2,18 +2,17 @@ module Simplify.Simplifier where -import Funcons.EDSL (Values(..), Funcons(..), string__) +import Funcons.EDSL (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 (forM, mzero, msum) 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 @@ -238,7 +237,6 @@ = 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 @@ -253,8 +251,8 @@ 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 + = do mut_src <- mapM (uncurry simplifyNamePatternsPair') (fst $ stepMutableEntities st) + mut_tgt <- mapM (uncurry simplifyNameTermPair) (snd $ stepMutableEntities st) inp <- mapM (uncurry simplifyInputEntity) (stepInputEntities st) ctrl <- mapM (uncurry simplifyControlEntity) (stepControlEntities st) outs <- mapM (uncurry simplifyNameTermPair) (stepOutputEntities st) @@ -265,7 +263,8 @@ { C.stepSource = source , C.stepTarget = target , C.stepInheritedEntities = inhs - , C.stepMutableEntities = mut' + , C.stepMutableEntitiesSource = mut_src + , C.stepMutableEntitiesTarget = mut_tgt , C.stepInputEntities = inp , C.stepOutputEntities = outs , C.stepControlEntities = ctrl @@ -273,9 +272,8 @@ 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 + = do mut_src <- mapM (uncurry simplifyNameTermPair) (fst $ premiseMutableEntities pst) + mut_tgt <- mapM (uncurry simplifyNamePatternsPair') (snd $ premiseMutableEntities pst) ctrl <- mapM (uncurry simplifyControlEntityPremise) (premiseControlEntities pst) outs <- mapM (uncurry simplifyNamePatternPair) (premiseOutputEntities pst) ins <- mapM (uncurry simplifyInputEntityPremise) (premiseInputEntities pst) @@ -286,15 +284,12 @@ { C.premiseSource = source , C.premiseTarget = target , C.premiseInheritedEntities = inhs - , C.premiseMutableEntities = mut' + , C.premiseMutableEntitiesSource = mut_src + , C.premiseMutableEntitiesTarget = mut_tgt , 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 @@ -314,8 +309,8 @@ 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 +simplifyMutableEntityPremise :: MonadError String m => (Name, FTerm, FPattern) -> m (Name, C.FTerm, [C.FPattern]) +simplifyMutableEntityPremise (n,t,p) = (n,,) <$> simplifyFTerm t <*> simplifyFPatterns p -- special meaning of tuple notation for control entities simplifyControlEntityPremise :: MonadError String m => Name -> FPattern -> m (Name,Maybe C.FPattern) @@ -328,6 +323,8 @@ simplifyNamePatternsPair :: MonadError String m => Name -> [FPattern] -> m (Name,[C.FPattern]) simplifyNamePatternsPair n p = (n,) <$> topLevelFPatterns p +simplifyNamePatternsPair' :: MonadError String m => Name -> FPattern -> m (Name,[C.FPattern]) +simplifyNamePatternsPair' n p = (n,) <$> simplifyFPatterns p simplifyInputEntityPremise :: MonadError String m => Name -> FTerm -> m (Name,[C.FTerm],Maybe MetaVar) simplifyInputEntityPremise n t = case t of @@ -367,6 +364,7 @@ simplify2VPattern :: MonadError String m => FPattern -> m C.VPattern simplify2VPattern (PSeq pats) = error "sequence in simple pattern" +simplify2VPattern PEmptySet = return $ C.PADT "set" [] simplify2VPattern (PList pats) = C.PADT "datatype-value" <$> (((C.VPLit (string__ "list")):) . concat <$> mapM simplify2VPatterns pats) simplify2VPattern (PADT cons pats) = C.PADT (pack cons) <$> @@ -428,23 +426,6 @@ 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) - ) -------------------------------------------------------------------- diff --git a/src/Simplify/TargetToFunconModules.hs b/src/Simplify/TargetToFunconModules.hs --- a/src/Simplify/TargetToFunconModules.hs +++ b/src/Simplify/TargetToFunconModules.hs @@ -8,12 +8,11 @@ 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 Funcons.EDSL (FTerm(..), DataTypeMembers(..), DataTypeAltt(..), pat2term) +import Types.SourceAbstractSyntax (Name,) +import Types.CoreAbstractSyntax (FSig(..), 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 @@ -74,10 +73,8 @@ 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_mut_ps = map (uncurry F.ReadMutable) (stepMutableEntitiesSource fstep) + source_mut_ts = map (uncurry F.WriteMutable) (stepMutableEntitiesTarget fstep) source_inps = map (uncurry F.ReadInput) (stepInputEntities fstep) source_dsigs = map (uncurry F.ReadDownControl) (stepControlEntities fstep) target_outs = map (uncurry F.WriteOutput) (stepOutputEntities fstep) @@ -89,9 +86,8 @@ 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) + where muts_ts = map (uncurry F.WriteMutable) (premiseMutableEntitiesSource prem) + muts_ps = map (uncurry F.ReadMutable) (premiseMutableEntitiesTarget prem) sigReads = map op (premiseControlEntities prem) where op (nm,mpat) = F.ReadControl nm mpat premise = diff --git a/src/Simplify/TargetToIML.hs b/src/Simplify/TargetToIML.hs deleted file mode 100644 --- a/src/Simplify/TargetToIML.hs +++ /dev/null @@ -1,737 +0,0 @@ -{-# Language FlexibleContexts, ScopedTypeVariables, FlexibleInstances, - TupleSections, OverloadedStrings #-} - -module Simplify.TargetToIML where - --------------------------------------------------------------------- -import Funcons.EDSL (Values(..), Funcons(FValue), isString_, unString, pat2term, typat2term) -import Types.SourceAbstractSyntax (Name, FLiteral(..), SeqSortOp(..),MetaVar, AliasMap, my_aliases) -import Types.CoreAbstractSyntax (FPattern(..), FTerm(..), isSeqVarSort, - FSideCondition(..), DataTypeSpec(..),DataTypeAlt(..), - EntitySpec(..), ConsSpec(..), FSig(..), Strictness(..)) -import Types.TargetAbstractSyntax -import Simplify.Utils -import qualified IML.Grammar as RF -import qualified IML.Grammar.Specs as IS -import qualified IML.Trans.ProMan as IML -import IML.Trans.FromFuncons (translate, remVarOp, translate_term) -import qualified Funcons.Operations as VAL -import IML.EDSL -------------------------------------------------------------------- - -import Control.Arrow ((***)) -import Control.Monad.Trans -import Control.Monad.Writer -import Control.Monad.State -import Data.Text (unpack,pack) -import Data.Map (assocs) -import Data.String (fromString) - -import System.IO.Unsafe -trace a b = unsafePerformIO (putStrLn a >> return b) - --- | Type representing value constructors -type VCons = Name -type Cons = Name - --- | The constructor used for the type-membership predicate -stepR, tyR :: RF.RSymb -stepR = "->" -rewVR = "~>" -tyR = "=ty=>" - -rewrite,step :: IsExprs exprs => exprs -> RuleBuilder () -step = commit stepR -rewrite = commit rewVR -type_member = commit tyR (RF.TVal (VAL.tobool True)) - -target2iml :: IML.Component CBSFile IS.HighSpec -target2iml = IML.component (\file -> return (execRuleBuilder (gCBSFile file))) - -lFSpec :: FunconSpec -> FunconSpec -lFSpec spec@(FRules nm sig mcs rs ss) = case sig of - FLazy -> spec - FNullary -> spec - FStrict -> FRules nm sig mcs rs' ss' - where FRules _ _ _ rs' ss' = lFSpec - (FRules nm (FPartiallyLazy [] (Just Strict)) mcs rs ss) - FPartiallyLazy ann mseqvar -> FRules nm sig mcs rs ss' - where ss' = map mkRule ruleKeys ++ seqvarRule ++ ss - ruleKeys = map fst $ filter ((Strict ==) . snd) keys - keys = zip [1..] ann - seqvarRule = case mseqvar of - Nothing -> [] - Just Lazy -> [] - Just Strict -> [rule] - where rule = FStepRule step (map Right scs ++ [Left premise]) - step = FStep (map mkPat (take (length ann) [1..]) ++ [PSeqVar "X*" StarOp]) - (TApp (pack nm) (map mkTerm (take (length ann) [1..]) ++ [TVar "Y*"])) - [] [] [] [] [] - where mkPat i = PMetaVar (mkVar i) - mkTerm i = TVar (mkVar i) - premise = FPremiseStep (TVar "X*") [PSeqVar "Y*" StarOp] [] [] [] [] [] - mkVar i = "X" ++ show i - scs = map mkSC ruleKeys - where mkSC i = SCIsInSort (TVar (mkVar i)) (TSortSeq (TName "values") QuestionMarkOp) - - mkRule k = FStepRule step [Left premise] - where step = FStep pats (TApp (pack nm) terms) [] [] [] [] [] - (pats,terms) = foldr op base keys - where base = case mseqvar of - Just _ -> ([PSeqVar "X*" StarOp] - ,[TVar "X*"]) - _ -> ([], []) - op (k',sness) (pats, terms) - | k' == k = (PMetaVar var:pats - ,TVar (var ++ "'") : terms) - | k' < k, Strict <- sness = - (PAnnotated (PMetaVar var) - (TName "values"):pats - ,TVar var : terms) - | True = (PMetaVar var : pats, TVar var : terms) - where var = "X" ++ show k' - premise = FPremiseStep (TVar var) [PMetaVar (var ++ "'")] - [] [] [] [] [] - where var = "X" ++ show k - - -gCBSFile :: CBSFile -> RuleBuilder () -gCBSFile cbsfile = do - {- THESE RELATIONS ARE NOW DECLARED IN main.iml - rel_decl stepR [{-IS.Repeatable-}] - rel_decl rewR [{-IS.Repeatable-}] - rel_decl tyR [] -- type-member relation - -} - mapM_ (gCBSSpec (aliases cbsfile)) (cbs cbsfile) - - {- THESE RULES ARE NOW SPECIFIED IN main.iml FILE - -- fall back rule for type-membership - -- that checks whether first argument is a value - [v1,v2,v3] <- mapM (const fresh_var) [1..3] - lhs (RF.PCons ty_cons [RF.PVar v1, RF.PVar v2]) - gRewrite (RF.TVar v1) (RF.PVar v3) - gRewrite (RF.TVar v2) (RF.PCons "values" []) - is_terminating stepR (RF.TVar v3) - commit tyR (RF.TVal (VAL.tobool True)) - -- fall back rule that determines non-membership - [v1,v2,v3,v4,v5] <- mapM (const fresh_var) [1..5] - lhs (RF.PCons ty_cons [RF.PVar v1, RF.PVar v2]) - gRewrite (RF.TVar v1) (RF.PVar v3) - gRewrite (RF.TVar v2) (RF.PVar v4) - pm (vop "type-member" [RF.TVar v3, RF.TVar v4]) (RF.PVar v5) - commit_prio 0 tyR (RF.TVar v5) - -} - -gCBSSpec :: AliasMap -> CBSSpec -> RuleBuilder () -gCBSSpec am (FunconSpec spec) = gFSpecWithMP_Aliases am (lFSpec spec) -gCBSSpec am (DataTypeSpec spec) = gData_Aliases am spec -gCBSSpec am (MetaSpec _) = return () -gCBSSpec am (EntitySpec spec) = gEntitySpec spec -gCBSSpec am (ConsSpec spec) = gCons_Aliases am spec - -gEntitySpec :: EntitySpec -> RuleBuilder () -gEntitySpec spec = case spec of - InheritedSpec n t -> ent_decl n [tTermAsExpr t] - MutableSpec n t -> ent_decl n [tTermAsExpr t] - OutputSpec n -> ent_decl n ([] :: [RF.Expr]) - InputSpec n -> ent_decl n ([] :: [RF.Expr]) - ControlSpec n -> ent_decl n ([] :: [RF.Expr]) - -gFSpecWithMP_Aliases :: AliasMap -> FunconSpec -> RuleBuilder() -gFSpecWithMP_Aliases am (FRules nm a b c d) = - forM_ (my_aliases nm am) (\nm' -> gFSpecWithMP (FRules nm' a b c d)) - -gFSpecWithMP :: FunconSpec -> RuleBuilder () -gFSpecWithMP spec@(FRules nm sig _ _ _) = gFSpec spec >> - astFuncons nm (Just 2)-- rules for meta-programming - where - gFSpec (FRules nm sig _ rs ss) = do - mapM_ (gRewriteRule sig nm) rs - mapM_ (gStepRule sig nm) ss - -mk_strict_lhs :: Name -> [RF.Pattern] -> RuleBuilder () -mk_strict_lhs nm pats = do - args_var <- fresh_var - add_var_decl_ (gVarDecl args_var (Just StarOp)) - lhs (RF.PCons nm [RF.PVar args_var]) - premise [RF.TVar args_var] (mRel rewVR) pats - -mk_partial_lhs :: Name -> [RF.Pattern] -> [RF.Pattern] -> RuleBuilder () -mk_partial_lhs nm init_pats rest_pats = do - arg_var <- fresh_var - add_var_decl_ (gVarDecl arg_var (Just StarOp)) - lhs (RF.PCons nm (init_pats ++ [RF.PVar arg_var])) - premise [RF.TVar arg_var] (mRel rewVR) rest_pats - -gRewriteRule :: FSig -> Name -> FRewriteRule -> RuleBuilder () -gRewriteRule sig nm (FRewriteRule source target bar) = do - pats <- mapM tFPattern source - case sig of FStrict -> mk_strict_lhs nm pats - FPartiallyLazy ann (Just Strict) -> mk_partial_lhs nm init_pats rest_pats - where (init_pats,rest_pats) = splitAt (length ann) pats - _ -> lhs (RF.PCons nm pats) - mapM gSideCond bar - rewrite $ case target of Nothing -> map RF.ETerm $ tTerm2Seq (TName "null") - Just t -> map RF.ETerm $ tTerm2Seq t -gStepRule :: FSig -> Name -> FStepRule -> RuleBuilder () -gStepRule sig nm (FStepRule fstep bar) = do - pats <- mapM tFPattern (stepSource fstep) - lhs (RF.PCons nm pats) - -- contextual/ inherited entities - ros <- mapM gRO (stepInheritedEntities fstep) - mapM_ (\(n, p, t) -> acc n p >> up n t) ros - -- mutable entities (IN) - forM (stepMutableEntities fstep) $ \(n,p,t) -> do - tFPattern p >>= acc n - -- TODO: input entities - -- * The "rest" of the input must be bound by a meta-var so that - -- the first premise can provide this as additional input --- forM (stepInputEntities fstep) $ \(n, vars) -> --- acc n =<< tSeqPattern (map PMetaVar vars) - - gConditions bar - -- control entities - forM (stepControlEntities fstep) $ \(n, mt) -> - acc n ([] :: [RF.Pattern]) >> - case mt of - Nothing -> up n ([] :: [RF.Term]) - Just t -> rewAndPut n (pat2term t) - -- mutable entities (OUT) - forM (stepMutableEntities fstep) $ \(n,p,t) -> do - rewAndPut n t - -- output entities - forM (stepOutputEntities fstep) $ \(n, t) -> do - var1 <- fresh_var - var2 <- fresh_var - add_var_decl_ (gVarDecl var1 (Just StarOp)) - add_var_decl_ (gVarDecl var2 (Just StarOp)) - acc n (RF.PVar var1) - gOptRewrite (tTerm2Seq t) [RF.PVar var2] - up n [RF.TVar var1, RF.TVar var2] - step (tTerm2Seq (stepTarget fstep)) --- ros <- let op (n,p) = (n,) <$> tPattern p --- in mapM op (stepInheritedEntities fstep) --acc --- rws <- mapM rewriteMutVal (stepMutableEntities fstep) --- wos1 <- mapM (uncurry rewriteOutVal) (stepOutputEntities fstep) --- wos2 <- mapM (uncurry rewriteConVal) (stepControlEntities fstep) --- let conditions = --concatMap (map Left . fst) wos1 ++ - --concatMap (map Left . fst) rws ++ - --concatMap (map Left . fst) wos2 ++ - where gRO (n,ps) = case ps of - [] -> return (n, [], []) - [PMetaVar var]-> return (n, [RF.PVar var], [RF.TVar var]) - [PWildCard] -> do var <- fresh_var - return (n, [RF.PVar var],[RF.TVar var]) - _ -> do var <- fresh_var - add_var_decl_ (gVarDecl var (Just StarOp)) - gSideCond (SCPatternMatch (TVar var) ps) - return (n, [RF.PVar var], [RF.TVar var]) - rewAndPut n t = do var <- fresh_var - gOptRewrite (tTerm2Seq t) [RF.PVar var] - up n (RF.TVar var) - -gConditions :: [Either FPremiseStep FSideCondition] -> RuleBuilder () -gConditions cs = mapM_ (mapeither gPremise gSideCond) cs - where mapeither f _ (Left e) = f e - mapeither _ f (Right e) = f e - -gPremise :: FPremiseStep -> RuleBuilder () -gPremise pstep = do - target' <- mapM tFPattern (premiseTarget pstep) - let source' = tTerm2Seq (premiseSource pstep) - var <- fresh_var - add_var_decl_ (gVarDecl var (Just StarOp)) - gOptRewrite source' [RF.PVar var] - -- contextual/inherited entities - inhI <- forM (premiseInheritedEntities pstep) $ \(n,t) -> do - var <- fresh_var - gOptRewrite (tTerm2Seq t) [RF.PVar var] - add_var_decl_ (gVarDecl var (Just StarOp)) - return (n, [RF.ETerm $ RF.TVar var]) - - -- mutable entities - mutI <- forM (premiseMutableEntities pstep) $ \(n,t,p) -> do - var <- fresh_var - gOptRewrite (tTerm2Seq t) [RF.PVar var] - return (n, [RF.ETerm (RF.TVar var)]) - mutO <- mapM (\(n,t,p) -> (n,) . (:[]) <$> tFPattern p) - (premiseMutableEntities pstep) - -- output entities - let outI = map (\(n,_) -> (n, [])) - (premiseOutputEntities pstep) - let matchOutList n p = case p of - (PValue (PADT "list" ps)) -> (n,) <$> tSeqPattern (map PValue ps) -- TODO pattern matching lists currently not supported, requires usage of destructors like `head` and `tail` - _ -> error "premise output not formed by a list of patterns" - outO <- mapM (uncurry matchOutList) (premiseOutputEntities pstep) - -- control entities - let ctrlI = map (\(n,_) -> (n, [])) - (premiseControlEntities pstep) - ctrlO <- forM (premiseControlEntities pstep) $ \(n,mp) -> case mp of - Just p -> (n,) . (:[]) <$> tFPattern p - Nothing -> return (n, []) - -- TODO: input entities - --ExtraInput determines that there is `other` input than provided by the terms - -- this input is the `left over' from the conclusion (or last premise?) - {- - inpI <- forM (premiseInputEntities pstep) $ \(n,vars,_) -> do - var <- fresh_var - gRewriteExpr (vop "list" (map tTerm vars)) (RF.PVar var) - return (n, RF.TVar var)-} - -- Check whether all provided input has been consumed. - -- If ExtraInput than more may be consumed - -- If ExactInput than inpO must be equal to [] - {- let inpO = map (\(n,_,access) -> -} --- woaccs <- let op (n,p) = (n,) <$> tPattern p --- opm (n,Nothing) = (n++"-nothing",) . RF.PVar <$> IML.fresh_var_ --- opm (n,Just p) = op (n,p) --- in (++) <$> mapM op (premiseOutputEntities pstep) --- <*> mapM opm (premiseControlEntities pstep) --- inhs <- mapM (uncurry rewriteOutVal) (premiseInheritedEntities pstep) --- muts <- mapM rewriteMutVal (premiseMutableEntities pstep) --- let roups = map snd inhs --- rwups = map snd muts - let ins = inhI ++ mutI ++ outI ++ ctrlI -- ++ inpI - outs = mutO ++ outO ++ ctrlO -- ++ inpO - refocus_var <- fresh_var -- static refocussing 1/4 - add_var_decl_ (gVarDecl refocus_var (Just StarOp)) -- static refocussing 2/4 - premise (RF.TConf [RF.ETerm (RF.TVar var)] ins) stepR (RF.PConf [RF.PVar refocus_var] []) -- static refocussing 3/4 - premise (RF.TConf [RF.ETerm (RF.TVar refocus_var)] []) (mRel stepR) (RF.PConf target' outs) -- static refocussing 4/4 --- premise (RF.TConf [RF.ETerm (RF.TVar var)] ins) stepR (RF.PConf target' outs) -- disabling static refocussing - -tSeqPattern :: [FPattern] -> RuleBuilder [RF.Pattern] -tSeqPattern ps = mapM tFPattern ps -{-foldM attach (RF.PCons nil_v []) . reverse - where attach acc p = do pat <- tPattern p - return (RF.PCons "cons" [pat, acc])-} - -gSideCond :: FSideCondition -> RuleBuilder () -gSideCond sc = - case sc of - SCEquality t1 t2 -> mkEquality t1 t2 truePat - SCInequality t1 t2 -> mkEquality t1 t2 falsePat - SCIsInSort t1 sort -> case sort of - TSortComplement sort' -> mkSort t1 sort' falsePat - _ -> mkSort t1 sort truePat - SCNotInSort t1 sort -> mkSort t1 sort falsePat - SCPatternMatch t ps -> do - ps' <- mapM tFPattern ps - gOptRewriteExpr (map RF.ETerm $ tTerm2Seq t) ps' - where mkEquality (TSeq []) t2 _ = gSideCond (SCPatternMatch t2 []) - mkEquality t1 (TSeq []) _ = gSideCond (SCPatternMatch t1 []) - mkEquality (TName "true") t _ = gRewriteTo (tTerm t) truePat - mkEquality t (TName "true") _ = gRewriteTo (tTerm t) truePat - mkEquality (TName "false") t _= gRewriteTo (tTerm t) falsePat - mkEquality t (TName "false") _= gRewriteTo (tTerm t) falsePat - mkEquality t1 t2 b = do - v1 <- fresh_var - gRewriteToVal (tTerm2Seq t1) v1 - v2 <- fresh_var - gRewriteToVal (tTerm2Seq t2) v2 - pm (vop "is-equal" [RF.TVar v1, RF.TVar v2]) b -{- mkSort (TVar v1) sort b - | let mop = last v1, mop == '*' || mop == '?' || mop == '+' = - let tup = TTuple [TVar v1] - seqs = TApp "tyseq" (TTuple [sort, TFuncon (FValue (String [mop]))]) - in mkSort tup seqs b-} - mkSort t1 sort b = - tycheck t1' sort' b --rewriting performed in rules for tychecking - where (t1',sort') = (tTerm2Seq t1, maybeApplyTySeq sort) - -tycheck :: [RF.Term] -> RF.Term -> RF.Pattern -> RuleBuilder () -tycheck vals ty b = premise (ty : vals) (mRel tyR) b - -tycheck_direct :: [RF.Term] -> RF.Term -> RF.Pattern -> RuleBuilder () -tycheck_direct vals ty b = premise (ty : vals) (sRel tyR) b - -maybeApplyTySeq :: FTerm -> RF.Term -maybeApplyTySeq sort - | isSeqVarSort sort = ty' - | otherwise = case tys of [ty] -> ty - _ -> ty' - where tys = tTerm2Seq sort - ty' = RF.TCons "tyseq" tys - -lit2Val :: VAL.HasValues t => FLiteral -> VAL.Values t -lit2Val lit = case lit of - FLiteralNat nat -> VAL.Nat (toInteger nat) - FLiteralFloat f -> VAL.Float f - FLiteralString s -> fromString s - FLiteralAtom c -> fromString c - - --- | Assuming no other patterns than the conclusions' left-hand side --- have annotation. For other patterns it is safe to use `tPattern` -tFPattern :: FPattern -> RuleBuilder RF.Pattern -tFPattern (PValue vpat) = tVPattern vpat -tFPattern (PAnnotated PWildCard sort) = do - v <- fresh_var - tFPattern (PAnnotated (PMetaVar v) sort) -tFPattern (PAnnotated (PMetaVar v) sort) = do - add_var_decl_ (gVarDecl v Nothing) - tycheck [RF.TVar v] (maybeApplyTySeq sort) truePat - return (RF.PVar v) -tFPattern (PAnnotated (PSeqVar v op) sort) - | v == "___" = fresh_var >>= \v' -> tFPattern (PAnnotated (PSeqVar v' op) sort) - | otherwise = do - add_var_decl_ (gVarDecl (remVarOp v) (Just op)) - tycheck [RF.TVar (remVarOp v)] (maybeApplyTySeq sort) truePat - return (RF.PVar (remVarOp v)) -tFPattern (PAnnotated p v) = error "unexpected annotation" -tFPattern (PMetaVar var) = return $ RF.PVar var -tFPattern (PSeqVar var op) - | var == "___" = fresh_var >>= \v' -> tFPattern (PSeqVar v' op) - | otherwise = do - add_var_decl_ (gVarDecl (remVarOp var) (Just op)) - return $ RF.PVar (remVarOp var) -tFPattern PWildCard = RF.PVar <$> fresh_var - -tVPattern :: VPattern -> RuleBuilder RF.Pattern -tVPattern (VPAnnotated VPWildCard sort) = do - v <- fresh_var - tVPattern (VPAnnotated (VPMetaVar v) sort) -tVPattern (VPAnnotated (VPMetaVar v) sort) = do - add_var_decl_ (gVarDecl v Nothing) - return (RF.PVar v) -tVPattern (VPAnnotated (VPSeqVar v op) sort) - | v == "___" = fresh_var >>= \v' -> tVPattern (VPAnnotated (VPSeqVar v' op) sort) - | otherwise = do - add_var_decl_ (gVarDecl (remVarOp v) (Just op)) - tycheck [RF.TVar (remVarOp v)] (maybeApplyTySeq sort) truePat - return (RF.PVar (remVarOp v)) -tVPattern (VPAnnotated p v) = error "unexpected annotation" -tVPattern (PADT cons ps) - -- TODO: generate variable with conditions that say that : - -- a) the matched value has `adt-constructor` equal to `string__ cons` - -- b) the matched value has `adt-fields` that match the patterns `ps` - | cons == "datatype-value", not (null ps) = do - p' <- tVPattern (head ps) - ps' <- mapM tVPattern (tail ps) - var_rewrite <- fresh_var - var <- fresh_var - gRewriteToVal [RF.TVar var_rewrite] var - premise (RF.TConf [RF.VOP "adt-constructor" [RF.ETerm $ RF.TVar var]] []) - (mRel rewVR) (RF.PConf [p'] []) - premise (RF.TConf [RF.ETerm $ RF.TCons "list-elements" - [RF.TCons "adt-fields" [RF.TVar var]]] []) - (mRel rewVR) (RF.PConf ps' []) - return (RF.PVar var_rewrite) --TODO rewrite to `var` instead?? - | otherwise = do - v <- fresh_var - pat' <- RF.PVal . VAL.ADTVal cons <$> mapM tVPattern ps - premise (toTConf (RF.TVar v)) (mRel rewVR) (toPConf pat') - return (RF.PVar v) -tVPattern VPWildCard = RF.PVar <$> fresh_var -tVPattern (VPMetaVar var) = return $ RF.PVar var -tVPattern (VPSeqVar var op) - | var == "___" = fresh_var >>= \v' -> tVPattern (VPSeqVar v' op) - | otherwise = do - add_var_decl_ (gVarDecl (remVarOp var) (Just op)) - return $ RF.PVar (remVarOp var) -tVPattern (VPLit lit) = return $ RF.PVal (VAL.vmap (RF.term2pattern . translate) lit) -tVPattern (VPType tpat) = tTPattern tpat - -tTPattern :: TPattern -> RuleBuilder RF.Pattern -tTPattern TPWildCard = RF.PVar <$> fresh_var -tTPattern (TPVar var) = return $ RF.PVar (remVarOp var) -tTPattern (TPSeqVar var op) - | var == "___" = fresh_var >>= \v' -> tTPattern (TPSeqVar v' op) - | otherwise = do - add_var_decl_ (gVarDecl (remVarOp var) (Just op)) - return $ RF.PVar (remVarOp var) -tTPattern (TPLit fterm) = error "missing translation for type-literals" -tTPattern (TPComputes tp) = RF.PVal . VAL.ADTVal "tycomp" . (:[]) <$> tTPattern tp -tTPattern (TPComputesFrom fp tp) = RF.PVal . VAL.ADTVal "tycomp" <$> mapM tTPattern [fp,tp] -tTPattern (TPADT cons ps) = RF.PVal . VAL.ComputationType . VAL.Type . VAL.ADT cons <$> mapM tTPattern ps - -tTerms :: [FTerm] -> [RF.Term] -tTerms = map tTerm - -tTermAsExpr :: FTerm -> RF.Expr -tTermAsExpr (TName nm) = RF.VOP (unpack nm) [] -tTermAsExpr (TApp nm ts) = RF.VOP (unpack nm) (map tTermAsExpr ts) -tTermAsExpr t = RF.ETerm (tTerm t) - -tTerm2Seq :: FTerm -> [RF.Term] -tTerm2Seq (TSeq ts) = concatMap tTerm2Seq ts -tTerm2Seq t = [tTerm t] - -tTerm :: FTerm -> RF.Term -tTerm = translate_term - -{- -tFuncons :: [Funcons] -> [RF.Term] -tFuncons = map tFuncon - -tFuncon :: Funcons -> RF.Term -tFuncon (FName nm) = RF.TCons False (unpack nm) [] -tFuncon (FApp nm f) = RF.TCons False (unpack nm) $ case f of - FTuple ts -> tFuncons ts - _ -> [tFuncon f] -tFuncon (FTuple fs) = RF.TCons False "tuple" (tFuncons fs) -tFuncon (FList fs) = RF.TCons False "list" (tFuncons fs) -tFuncon (FSet fs) = RF.TCons False "set" (tFuncons fs) -tFuncon (FMap fs) = RF.TCons False "map" (tFuncons fs) -tFuncon (FValue v) = trace "warning: missing value translations" - $ RF.TCons True "some-value" [] -tFuncon _ = error "missing Funcons translation" --} - -gVarDecl :: RF.MVar -> Maybe SeqSortOp -> RF.VarDecl -gVarDecl x mop = RF.VarDecl x lb mub RF.Longest [] - where (lb,mub) = case mop of Just StarOp -> (0, Nothing) - Just PlusOp -> (1, Nothing) - Just QuestionMarkOp -> (0, Just 1) - Nothing -> (1, Just 1) - -is_terminating_or_null t = tycheck [t] (RF.TCons "tystar" [RF.TCons "values" []]) truePat - -gRewriteToValExpr :: [RF.Expr] -> RF.MVar -> RuleBuilder () -gRewriteToValExpr expr var = do - gOptRewriteExpr expr [RF.PVar var] - is_terminating_or_null (RF.TVar var) - -gRewriteToVal :: [RF.Term] -> RF.MVar -> RuleBuilder () -gRewriteToVal term = gRewriteToValExpr (map RF.ETerm term) - -gRewriteTo :: RF.Term -> RF.Pattern -> RuleBuilder() -gRewriteTo t p = gOptRewriteExpr [RF.ETerm t] [p] - -gOptRewriteExpr :: [RF.Expr] -> [RF.Pattern] -> RuleBuilder () -gOptRewriteExpr expr pat = premise expr (mRel rewVR) pat - -gOptRewrite :: [RF.Term] -> [RF.Pattern] -> RuleBuilder () -gOptRewrite term = gOptRewriteExpr (map RF.ETerm term) - -truePat, falsePat :: RF.Pattern -truePat = RF.PVal (VAL.tobool True) -falsePat = RF.PVal (VAL.tobool False) - -gData_Aliases :: AliasMap -> DataTypeSpec -> RuleBuilder () -gData_Aliases am (DataTypeDecl nm tyargs alts) = - forM_ (my_aliases nm am) (\nm' -> gData (DataTypeDecl nm' tyargs alts)) - -gData :: DataTypeSpec -> RuleBuilder () -gData d@(DataTypeDecl nm tyargs alts) = do - -- generate rules for inclusion constructors - gAlts d - --term_pc stepR (Right $ toVCons nm) - --term_pc rewVR (Right $ toVCons nm) - -- axiom for type - (vars,typats) <- unzip <$> mapM mkPat tyargs - pats <- mapM tTPattern typats - lhs (RF.PCons nm pats) - vars' <- forM vars $ \var -> do - var' <- fresh_var - gRewriteToVal [RF.TVar var] var' - return var' -- TODO share these rewrites with sidecons in bar1 - rewrite (VAL.ADT (pack nm) (map RF.TVar vars')) --rewrite - -- congruence rules - strictFCongs nm - -- type alternative for type -- no longer required since ADT-builtin - --typeMemberAltCons "types" [] nm (map snd tyargs) - astFuncons nm (Just $ length pats) -- meta-funcons for type - where mkPat :: TPattern -> RuleBuilder (MetaVar, TPattern) - mkPat tpat = case tpat of - TPVar var -> return (var, tpat) - TPSeqVar var op -> return (remVarOp var, tpat) - TPWildCard -> do var <- fresh_var - return (var, TPVar var) - _ -> error "unexpected type-parameter pattern" - -gAlts :: DataTypeSpec -> RuleBuilder () -gAlts dt@(DataTypeDecl _ _ alts) = mapM_ (gAlt dt) alts - -gAlt :: DataTypeSpec -> DataTypeAlt -> RuleBuilder () -gAlt (DataTypeDecl tyname tyargs _) alt = case alt of - DataTypeInclusion sort -> - typeMemberAltIncl tyname tyargs sort - -gCons_Aliases :: AliasMap -> ConsSpec -> RuleBuilder () -gCons_Aliases am (ValCons nm a b tynm d) = - forM_ (my_aliases nm am) (\nm' -> - forM_ (my_aliases tynm am) (\tynm' -> gCons (ValCons nm' a b tynm' d))) - -gCons :: ConsSpec -> RuleBuilder() --- SIMPLIFICATION: all constructors are strict -gCons (ValCons nm _ argstys tynm typats) = do --- gDataTypeValue nm -- rules for the operational behaviour of cons - typeMemberAltCons tynm typats nm argstys -- type-membership rule - astFuncons nm (Just nr_args) - where nr_args = length argstys - - -{- DataTypeMemberConstructor nm' args mtyargs -> do - --term_pc stepR (Right $ toVCons nm) - --term_pc rewVR (Right $ toVCons nm) - gDataTypeValue (length args) nm -- rules for the operational behaviour of cons - typeMemberAltCons tyname (maybe tyargs id mtyargs) nm args -- type-membership rule - astFuncons nm (length args) - where nm = unpack nm' --} - -typeMemberAltIncl :: Name -> [TPattern] -> FTerm -> RuleBuilder () -typeMemberAltIncl tyname tyargs sort = do - v1 <- fresh_var - typats <- mapM tTPattern tyargs - lhs [RF.PVal (adt_type (pack tyname) typats), RF.PVar v1] - tycheck [RF.TVar v1] (maybeApplyTySeq sort) truePat - type_member - - -- TODO extend the `sorts` argument to contain information about the variable - -- in order to avoid generating sequence-variables where not necessary -typeMemberAltCons :: Name -> [TPattern] -> Name -> [FTerm] -> RuleBuilder () -typeMemberAltCons tyname tyargs nm sorts = do - typats <- mapM tTPattern tyargs - patvars <- forM sorts $ \sort -> do - var <- fresh_var - case mkSort sort of - Nothing -> do - tycheck [RF.TVar var] (maybeApplyTySeq sort) truePat - return var - Just op -> do - add_var_decl_ (gVarDecl var (Just op)) - tycheck [RF.TVar var] (maybeApplyTySeq sort) truePat - return var - lhs [RF.PVal (adt_type (pack tyname) typats) - ,RF.PVal (adt (pack nm) (map RF.PVar patvars))] - type_member - where mkSort t = case t of - TSortSeq t' op -> Just op - TSortPower _ _ -> Just StarOp - TVar var -> case last var of - '*' -> Just StarOp - '?' -> Just QuestionMarkOp - '+' -> Just PlusOp - _ -> Nothing - _ -> Nothing - -{- -gDataTypeValue :: Cons -> RuleBuilder () -gDataTypeValue cs = do -- build axiom - var <- fresh_var - lhs (RF.PCons cs [RF.PVar var]) - add_var_decl_ (gVarDecl var (Just StarOp)) - tycheck [RF.TVar var] (tTerm (TName "values")) truePat - rewrite (RF.TCons "datatype-value" (RF.TVal (fromString cs) : [RF.TVar var])) --rewrite - strictFCongs cs -- build congruences --} - -strictFCongs :: Cons -> RuleBuilder () -strictFCongs cs = do - x_var <- fresh_var - x_var_rw<- fresh_var - x_var' <- fresh_var - lhs (RF.PCons cs [RF.PVar x_var]) - add_var_decl_ (gVarDecl x_var (Just StarOp)) - add_var_decl_ (gVarDecl x_var_rw (Just StarOp)) - add_var_decl_ (gVarDecl x_var' (Just StarOp)) - gOptRewrite [RF.TVar x_var] [RF.PVar x_var_rw] - premise (RF.TVar x_var_rw) (sRel stepR) (RF.PVar x_var') - commit (sRel stepR) (RF.TCons cs [RF.TVar x_var']) - -mkValOpRules :: [RF.Rule] -mkValOpRules = rules - where IS.Spec new = execRuleBuilder $ mapM_ (uncurry mkrule) - $ assocs (VAL.library :: VAL.Library RF.Term) - (_,_,_,_,rules) = IS.partition_decls new - - mkrule :: VAL.OP {- String, operation name -} -> VAL.ValueOp t -> RuleBuilder () - mkrule nm op = case op of - VAL.NullaryExpr _ -> build $ Just 0 - VAL.UnaryExpr _ -> build $ Just 1 - VAL.BinaryExpr _ -> build $ Just 2 - VAL.TernaryExpr _ -> build $ Just 3 - VAL.NaryExpr _ -> build Nothing - where - build marity = do - strictFCongs nm -- congruence rules - mkAxiom marity -- axiom - astFuncons nm marity --ast-* funcons - mkAxiom marity= case marity of - Just arity -> do - vars <- mapM (const fresh_var) [1..arity] - mk_strict_lhs nm (map RF.PVar vars) - vars' <- forM vars $ \var -> do -- termination side conditions - var' <- fresh_var - gSideCond (SCPatternMatch (TVar var) [PMetaVar var']) - is_terminating_or_null (RF.TVar var') - return var' - rewrite (vop nm (map RF.TVar vars')) - Nothing -> do - var <- fresh_var - lhs (RF.PCons nm [RF.PVar var]) - var' <- fresh_var - add_var_decl_ (gVarDecl var (Just StarOp)) - add_var_decl_ (gVarDecl var' (Just StarOp)) - gOptRewrite [RF.TVar var] [RF.PVar var'] - is_terminating_or_null (RF.TVar var') - rewrite (vop nm [RF.TVar var']) - - --- meta-programming specific stuff - -ctR, dlR, ulR :: RF.RSymb -ctR = "=ct=>" -dlR = "=dl=>" -ulR = "=ul=>" - -ctRelRule :: Name -> RuleBuilder () -ctRelRule nm = do - var <- fresh_var - var' <- fresh_var - lhs (RF.PCons nm [RF.PVar var]) - var_decl var 0 Nothing RF.Longest [] - var_decl var' 0 Nothing RF.Longest [] - premise (RF.TVar var) ctR (RF.PVar var') - commit ctR (RF.TCons nm [RF.TVar var']) - -dlRelRule :: Name -> RuleBuilder () -dlRelRule nm = do - var <- fresh_var - var' <- fresh_var - lhs (RF.PVal (VAL.ADTVal (pack astv_nm) [RF.PVar var])) - var_decl var 0 Nothing RF.Longest [] - var_decl var' 0 Nothing RF.Longest [] - premise (RF.TVar var) dlR (RF.PVar var') - commit dlR (RF.TCons nm [RF.TVar var']) - where astv_nm = "astv-" ++ nm - -ulRelRule :: Name -> RuleBuilder () -ulRelRule nm = do - var <- fresh_var - var' <- fresh_var - lhs (RF.PCons nm [RF.PVar var]) - var_decl var 0 Nothing RF.Longest [] - var_decl var' 0 Nothing RF.Longest [] - premise (RF.TVar var) ulR (RF.PVar var') - commit ulR (RF.TCons astv_nm [RF.TVar var']) - where astv_nm = "astv-" ++ nm - -promoteRule :: Name -> RuleBuilder () -promoteRule nm = do - var <- fresh_var - lhs (RF.PCons nm [RF.PVar var]) - commit ulR (RF.TCons "astv-promote" [RF.TCons nm [RF.TVar var]]) - --- --- 1 Generate funcon for funcon named, say "scope", with arity 2 --- > value constructor astv-scope with congruence rules --- 2 Termination for value constructor --- 3 Rule that types astv-scope(A:asts,B:asts) as asts --- 4 astv-scope(A,B) =dl=> scope(Ac, Bc) --- 5 scope(Ac,Bc) =ul=> astv-scope(A,B) --- 6 astv-scope(A,B) =ct=> astv-scope(A,B) --- 7 astv-scope(A,B) =ul=> astv-promote(astv-scope(A,B)) -astFuncons :: Name -> Maybe Int -> RuleBuilder() -astFuncons nm marity = return () {-do - ctRelRule nm - --term_pc stepR (Right $ "astv-" ++ nm) -- 2 - --term_pc rewR (Right $ "astv-" ++ nm) -- 2 - gDataTypeValue astv_nm -- 1a - typeMemberAltCons "asts" [] astv_nm [TSortSeq (TName "asts") StarOp] --3 - dlRelRule nm -- 4 - ulRelRule nm -- 5 - ctRelRule astv_nm -- 6 - promoteRule astv_nm - where astv_nm = "astv-" ++ nm --} diff --git a/src/Simplify/Utils.hs b/src/Simplify/Utils.hs --- a/src/Simplify/Utils.hs +++ b/src/Simplify/Utils.hs @@ -8,7 +8,7 @@ import Control.Applicative import Control.Monad.Except -import Funcons.EDSL (SeqSortOp(..), Funcons(..), Values(..), string__) +import Funcons.EDSL (SeqSortOp(..), Funcons(..), Values(..), string__, char__) import Funcons.Operations hiding (Values) import Types.SourceAbstractSyntax (FLiteral(..)) @@ -17,13 +17,6 @@ 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 @@ -42,7 +35,7 @@ simplifyLiteral :: FLiteral -> Values simplifyLiteral lit = case lit of FLiteralNat n -> Nat (toInteger n) - FLiteralAtom char | length char == 1 -> Char (head char) + FLiteralAtom char | length char == 1 -> char__ (head char) | otherwise -> error "atom of size != 1" FLiteralString str -> string__ str FLiteralFloat f -> Float f diff --git a/src/Types/Bindings.hs b/src/Types/Bindings.hs --- a/src/Types/Bindings.hs +++ b/src/Types/Bindings.hs @@ -63,14 +63,14 @@ 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 (map (\(_,x) -> x) $ C.stepMutableEntitiesSource 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` pvars (map (\(_,x) -> x) $ C.premiseMutableEntitiesTarget premise) `S.union` S.fromList (concatMap (\(_,_,x) -> maybe [] (:[]) x) $ C.premiseInputEntities premise) `S.union` pvars (map snd $ C.premiseOutputEntities premise) `S.union` pvars (map snd $ C.premiseControlEntities premise) diff --git a/src/Types/ConcreteSyntax.hs b/src/Types/ConcreteSyntax.hs --- a/src/Types/ConcreteSyntax.hs +++ b/src/Types/ConcreteSyntax.hs @@ -282,6 +282,8 @@ | At String | CommentTerm [Term] | CommentPremise Premise + | CommentPhraseType PhraseType + | CommentProds [Prod] | SpecInComment CBSSpec deriving Show diff --git a/src/Types/CoreAbstractSyntax.hs b/src/Types/CoreAbstractSyntax.hs --- a/src/Types/CoreAbstractSyntax.hs +++ b/src/Types/CoreAbstractSyntax.hs @@ -89,7 +89,8 @@ { stepSource :: [FPattern] , stepTarget :: FTerm , stepInheritedEntities :: [(Name,[FPattern])] - , stepMutableEntities :: [(Name,FPattern,FTerm)] + , stepMutableEntitiesSource :: [(Name,[FPattern])] + , stepMutableEntitiesTarget :: [(Name,FTerm)] , stepInputEntities :: [(Name,[FPattern],[MetaVar])] , stepOutputEntities :: [(Name,FTerm)] , stepControlEntities :: [(Name,Maybe FPattern)] @@ -100,7 +101,8 @@ { premiseSource :: FTerm , premiseTarget :: [FPattern] , premiseInheritedEntities :: [(Name,FTerm)] - , premiseMutableEntities :: [(Name,FTerm,FPattern)] + , premiseMutableEntitiesSource :: [(Name,FTerm)] + , premiseMutableEntitiesTarget :: [(Name,[FPattern])] , premiseInputEntities :: [(Name,[FTerm],Maybe MetaVar)] , premiseOutputEntities :: [(Name,FPattern)] , premiseControlEntities :: [(Name,Maybe FPattern)] diff --git a/src/Types/FunconModule.hs b/src/Types/FunconModule.hs --- a/src/Types/FunconModule.hs +++ b/src/Types/FunconModule.hs @@ -38,7 +38,7 @@ | ReadInherited Name [FPattern] | ScopeInherited Name FTerm FStepStmt --set inh for the next stmt | WriteMutable Name FTerm - | ReadMutable Name FPattern + | ReadMutable Name [FPattern] | ReceiveControl [Name] FStepStmt | ReadControl Name (Maybe FPattern) | WriteControl Name (Maybe FTerm) diff --git a/src/Types/SourceAbstractSyntax.hs b/src/Types/SourceAbstractSyntax.hs --- a/src/Types/SourceAbstractSyntax.hs +++ b/src/Types/SourceAbstractSyntax.hs @@ -134,6 +134,7 @@ data FPattern = PSeq [FPattern] | PList [FPattern] + | PEmptySet | PAnnotated FPattern FSort | PADT ADTConstructor [FPattern] | PAny diff --git a/src/Types/TargetAbstractSyntax.hs b/src/Types/TargetAbstractSyntax.hs --- a/src/Types/TargetAbstractSyntax.hs +++ b/src/Types/TargetAbstractSyntax.hs @@ -8,7 +8,7 @@ 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 Funcons.EDSL (HasTypeVar(..)) import qualified Funcons.EDSL as FCT data CBSFile = CBSFile {cbs :: [CBSSpec], env :: TypeEnv, aliases :: AliasMap} @@ -61,7 +61,8 @@ { stepSource :: [FPattern] , stepTarget :: FTerm , stepInheritedEntities :: [(Name,[FPattern])] - , stepMutableEntities :: [(Name,FPattern,FTerm)] + , stepMutableEntitiesSource :: [(Name,[FPattern])] + , stepMutableEntitiesTarget :: [(Name,FTerm)] , stepInputEntities :: [(Name,[FPattern])] , stepOutputEntities :: [(Name,FTerm)] , stepControlEntities :: [(Name,Maybe FPattern)] @@ -72,7 +73,8 @@ { premiseSource :: FTerm , premiseTarget :: [FPattern] , premiseInheritedEntities :: [(Name,FTerm)] - , premiseMutableEntities :: [(Name,FTerm,FPattern)] + , premiseMutableEntitiesSource :: [(Name,FTerm)] + , premiseMutableEntitiesTarget :: [(Name,[FPattern])] , premiseInputEntities :: [(Name,[FTerm],InputAccess)] , premiseOutputEntities :: [(Name,FPattern)] , premiseControlEntities :: [(Name,Maybe FPattern)] @@ -108,13 +110,15 @@ 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) + ,stepMutableEntitiesSource = map (subs2of2 env) (stepMutableEntitiesSource step) + ,stepMutableEntitiesTarget = map (subs2of2 env) (stepMutableEntitiesTarget 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) + ,premiseMutableEntitiesSource = map (subs2of2 env) (premiseMutableEntitiesSource step) + ,premiseMutableEntitiesTarget = map (subs2of2 env) (premiseMutableEntitiesTarget step) ,premiseOutputEntities = map (subs2of2 env) (premiseOutputEntities step) ,premiseControlEntities = map (subs2of2 env) (premiseControlEntities step)}