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