funcons-intgen-0.2.0.1: src/Simplify/TargetToIML.hs
{-# 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
-}