MixAna.hs revision 5e224517e0f2d6286d8c55e676066715fc358edf
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder
75a6279dbae159d018ef812185416cf6df386c10Till Mossakowski{- |
75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiModule : $Header$
75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiCopyright : (c) Christian Maeder and Uni Bremen 2003
75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
75a6279dbae159d018ef812185416cf6df386c10Till Mossakowski
75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiMaintainer : hets@tzi.de
75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiStability : experimental
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian MaederPortability : portable
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian MaederMixfix analysis of terms and patterns, types annotations are also analysed
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder-}
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maeder
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maedermodule HasCASL.MixAna where
ee1c7c5796832536932d7b06cbfb1ca13f9a0d7bMartin Kühl
06d7655040315f69ae152a74373ad16a9c2e09c2Martin Kühlimport Common.GlobalAnnotations
ee1c7c5796832536932d7b06cbfb1ca13f9a0d7bMartin Kühlimport Common.AS_Annotation
06d7655040315f69ae152a74373ad16a9c2e09c2Martin Kühlimport Common.Result
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maederimport Common.Id
b49276c9f50038e0bd499ad49f7bd6444566a834Christian Maederimport Common.PrettyPrint
06d7655040315f69ae152a74373ad16a9c2e09c2Martin Kühlimport Common.Keywords
06d7655040315f69ae152a74373ad16a9c2e09c2Martin Kühlimport qualified Common.Lib.Map as Map
f6efd319ac43b72b37eff648e93b939d16174121Christian Maederimport qualified Common.Lib.Set as Set
06d7655040315f69ae152a74373ad16a9c2e09c2Martin Kühlimport qualified Common.Lib.Rel as Rel
caf544dc9b8f02e05e37786681153f5660e67f64Martin Kühlimport Common.Earley
caf544dc9b8f02e05e37786681153f5660e67f64Martin Kühlimport Common.ConvertLiteral
caf544dc9b8f02e05e37786681153f5660e67f64Martin Kühlimport Common.Lib.State
caf544dc9b8f02e05e37786681153f5660e67f64Martin Kühlimport HasCASL.As
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maederimport HasCASL.AsUtils
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maederimport HasCASL.VarDecl
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maederimport HasCASL.Le
06d7655040315f69ae152a74373ad16a9c2e09c2Martin Kühlimport HasCASL.Unify
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maederimport HasCASL.TypeAna
f66fcd981f556c238df7dd6dfa42123745e3b1d2Christian Maederimport Data.Maybe
acde06dd6089b05f501690e471467da09f90d894Martin Kühl
acde06dd6089b05f501690e471467da09f90d894Martin Kühl-- import Debug.Trace
61745001283cdb80c0ed9715919cff9747eb5f35Martin Kühl-- import Control.Exception(assert)
acde06dd6089b05f501690e471467da09f90d894Martin Kühlassert :: Bool -> a -> a
ee1c7c5796832536932d7b06cbfb1ca13f9a0d7bMartin Kühlassert b a = if b then a else error ("assert")
ee1c7c5796832536932d7b06cbfb1ca13f9a0d7bMartin Kühl
ee1c7c5796832536932d7b06cbfb1ca13f9a0d7bMartin Kühltype Rule = (Id, Int, [Token])
06d7655040315f69ae152a74373ad16a9c2e09c2Martin Kühl
06d7655040315f69ae152a74373ad16a9c2e09c2Martin KühltrueId :: Id
ee1c7c5796832536932d7b06cbfb1ca13f9a0d7bMartin KühltrueId = mkId [mkSimpleId trueS]
d1b6336b151759984fcea8d279e874a41e25eb58Martin Kühl
2eb86e6017c065aa54cc31c5169250985ac7b36cMartin KühlfalseId :: Id
2eb86e6017c065aa54cc31c5169250985ac7b36cMartin KühlfalseId = mkId [mkSimpleId falseS]
2eb86e6017c065aa54cc31c5169250985ac7b36cMartin Kühl
06d7655040315f69ae152a74373ad16a9c2e09c2Martin KühlifThenElse :: Id
2eb86e6017c065aa54cc31c5169250985ac7b36cMartin KühlifThenElse = mkId (map mkSimpleId [ifS, place, thenS, place, elseS, place])
a205324331077b7d5a2c08fb3f0f57e5c029f9aaTill Mossakowski
2eb86e6017c065aa54cc31c5169250985ac7b36cMartin KühlwhenElse :: Id
caf544dc9b8f02e05e37786681153f5660e67f64Martin KühlwhenElse = mkId (map mkSimpleId [place, whenS, place, elseS, place])
2eb86e6017c065aa54cc31c5169250985ac7b36cMartin Kühl
50ea34ea29d0121f3e692b7029b09d28dc7988fdTill MossakowskimkInfix :: String -> Id
dd30accd995f6af9461ad42e142da90e783ecdc2Klaus LuettichmkInfix s = mkId $ map mkSimpleId [place, s, place]
dd30accd995f6af9461ad42e142da90e783ecdc2Klaus Luettich
dd30accd995f6af9461ad42e142da90e783ecdc2Klaus LuettichinfixIf :: Id
06d7655040315f69ae152a74373ad16a9c2e09c2Martin KühlinfixIf = mkInfix ifS
06d7655040315f69ae152a74373ad16a9c2e09c2Martin Kühl
caf544dc9b8f02e05e37786681153f5660e67f64Martin KühlexEq :: Id
caf544dc9b8f02e05e37786681153f5660e67f64Martin KühlexEq = mkInfix exEqual
caf544dc9b8f02e05e37786681153f5660e67f64Martin Kühl
caf544dc9b8f02e05e37786681153f5660e67f64Martin KühleqId :: Id
caf544dc9b8f02e05e37786681153f5660e67f64Martin KühleqId = mkInfix equalS
caf544dc9b8f02e05e37786681153f5660e67f64Martin Kühl
caf544dc9b8f02e05e37786681153f5660e67f64Martin KühlandId :: Id
caf544dc9b8f02e05e37786681153f5660e67f64Martin KühlandId = mkInfix lAnd
caf544dc9b8f02e05e37786681153f5660e67f64Martin Kühl
caf544dc9b8f02e05e37786681153f5660e67f64Martin KühlorId :: Id
caf544dc9b8f02e05e37786681153f5660e67f64Martin KühlorId = mkInfix lOr
caf544dc9b8f02e05e37786681153f5660e67f64Martin Kühl
caf544dc9b8f02e05e37786681153f5660e67f64Martin KühlimplId :: Id
caf544dc9b8f02e05e37786681153f5660e67f64Martin KühlimplId = mkInfix implS
caf544dc9b8f02e05e37786681153f5660e67f64Martin Kühl
caf544dc9b8f02e05e37786681153f5660e67f64Martin KühleqvId :: Id
caf544dc9b8f02e05e37786681153f5660e67f64Martin KühleqvId = mkInfix equivS
caf544dc9b8f02e05e37786681153f5660e67f64Martin Kühl
caf544dc9b8f02e05e37786681153f5660e67f64Martin KühldefId :: Id
caf544dc9b8f02e05e37786681153f5660e67f64Martin KühldefId = mkId $ map mkSimpleId [defS, place]
caf544dc9b8f02e05e37786681153f5660e67f64Martin Kühl
caf544dc9b8f02e05e37786681153f5660e67f64Martin KühlnotId :: Id
caf544dc9b8f02e05e37786681153f5660e67f64Martin KühlnotId = mkId $ map mkSimpleId [notS, place]
caf544dc9b8f02e05e37786681153f5660e67f64Martin Kühl
ee1c7c5796832536932d7b06cbfb1ca13f9a0d7bMartin KühlbuiltinRelIds :: Set.Set Id
builtinRelIds = Set.fromDistinctAscList [typeId, eqId, exEq, defId]
builtinLogIds :: Set.Set Id
builtinLogIds = Set.fromDistinctAscList
[andId, eqvId, implId, orId, infixIf, notId]
addBuiltins :: GlobalAnnos -> GlobalAnnos
addBuiltins ga =
let ass = assoc_annos ga
newAss = Map.union ass $ Map.fromList
[(applId, ALeft), (andId, ALeft), (orId, ALeft),
(implId, ARight), (infixIf, ALeft),
(whenElse, ARight)]
precs = prec_annos ga
pMap = Rel.toMap precs
opIds = Set.unions (Set.fromDistinctAscList (Map.keys pMap)
:Map.elems pMap)
opIs = Set.toList ((((Set.filter isInfix opIds)
Set.\\ builtinRelIds) Set.\\ builtinLogIds)
Set.\\ Set.fromDistinctAscList [applId, whenElse])
logs = [(eqvId, implId), (implId, andId), (implId, orId),
(eqvId, infixIf), (infixIf, andId), (infixIf, orId),
(andId, notId), (orId, notId)]
rels1 = map ( \ i -> (notId, i)) $ Set.toList builtinRelIds
rels2 = map ( \ i -> (i, whenElse)) $ Set.toList builtinRelIds
ops1 = map ( \ i -> (whenElse, i)) (applId : opIs)
ops2 = map ( \ i -> (i, applId)) (whenElse : opIs)
newPrecs = foldr (\ (a, b) p -> if Rel.member b a p then p else
Rel.insert a b p) precs $
concat [logs, rels1, rels2, ops1, ops2]
in ga { assoc_annos = newAss
, prec_annos = Rel.transClosure newPrecs }
opKindFilter :: Int -> Int -> Int -> Maybe Bool
opKindFilter relPrec arg op =
if op < arg then Just True
else if arg < op && (op <= relPrec || arg < relPrec) then Just False
else Nothing
mkPrecIntMap :: Rel.Rel Id -> PrecMap
mkPrecIntMap r =
let t = Rel.topSort r
l = length t
m = foldr ( \ (n, s) m1 ->
Set.fold ( \ i m2 ->Map.insert i n m2) m1 s)
Map.empty $ zip [1..l] t
in (m, Map.find eqId m, l)
getIdPrec :: PrecMap -> Set.Set Id -> Id -> Int
getIdPrec (pm, r, m) ps i = Map.findWithDefault
(if Set.member i ps then r
else m) i pm
initTermRules :: (PrecMap, Set.Set Id) -> Set.Set Id -> [Rule]
initTermRules (pm, ps) is =
(map ( \ i -> mixRule (getIdPrec pm ps i) i)
(Set.toList
(Set.fromDistinctAscList
[unitId, parenId, tupleId, exprId, typeId, applId]
`Set.union` is))) ++
(map ( \ i -> (protect i, getIdPrec pm ps i, getPlainTokenList i))
(filter isMixfix $ Set.toList is))
addType :: Term -> Term -> Term
addType (TypedTerm _ qual ty ps) t = TypedTerm t qual ty ps
addType (MixInTerm ty ps) t = TypedTerm t InType ty ps
addType _ _ = error "addType"
toMixTerm :: Id -> Int -> [Term] -> [Pos] -> Term
toMixTerm ide _ ar qs =
if ide == applId then assert (length ar == 2) $
let [op, arg] = ar in ApplTerm op arg qs
else if ide == tupleId || ide == unitId then
mkTupleTerm ar qs
else ResolvedMixTerm ide ar qs
type TermChart = Chart Term Int
-- | find information for qualified operation
findOpId :: Assumps -> TypeMap -> Int -> UninstOpId -> Type -> Maybe OpInfo
findOpId as tm c i ty = listToMaybe $ fst $
partitionOpId as tm c i $ TypeScheme [] ([] :=> ty) []
iterateCharts :: GlobalAnnos -> [Term] -> TermChart
-> State Env TermChart
iterateCharts ga terms chart =
do e <- get
let ((_, relId, _), _) = preIds e
self = iterateCharts ga
oneStep = nextChart addType (opKindFilter relId)
toMixTerm ga chart
as = assumps e
tm = typeMap e
if null terms then return chart else
do let t:tt = terms
recurse trm = self tt $
oneStep (trm, exprTok {tokPos = posOfTerm trm})
case t of
MixfixTerm ts -> self (ts ++ tt) chart
MixInTerm _ ps -> self tt $ oneStep (t,
typeTok {tokPos = headPos ps})
BracketTerm b ts ps -> self
(expandPos TermToken (getBrackets b) ts ps ++ tt) chart
QualVar v typ ps -> do
mTyp <- anaStarType typ
case mTyp of
Nothing -> recurse t
Just nTyp -> do
let mi = findOpId as tm (counter e) v nTyp
case mi of
Nothing -> addDiags [mkDiag Error
"value not found" v]
_ -> return ()
recurse $ QualVar v nTyp ps
QualOp b io@(InstOpId v _ _)
(TypeScheme rs (qs :=> typ) ss) ps -> do
mTyp <- anaStarType typ
case mTyp of
Nothing -> recurse t
Just nTyp -> do
let mi = findOpId as tm (counter e) v nTyp
case mi of
Nothing -> addDiags [mkDiag Error
"value not found" v]
_ -> return ()
recurse $ QualOp b io
(TypeScheme rs (qs :=> nTyp) ss) ps
TypedTerm hd tqual typ ps -> do
mTyp <- anaStarType typ
case mTyp of
Nothing -> recurse t
Just nTyp -> do
mt <- resolve ga hd
let newT = case mt of Just trm -> trm
_ -> hd
recurse $ TypedTerm newT tqual nTyp ps
QuantifiedTerm quant decls hd ps -> do
newDs <- mapM anaGenVarDecl decls
mt <- resolve ga hd
putAssumps as
putTypeMap tm
let newT = case mt of Just trm -> trm
_ -> hd
recurse $ QuantifiedTerm quant (catMaybes newDs) newT ps
LambdaTerm decls part hd ps -> do
mDecls <- mapM (resolveConstrPattern ga) decls
let newDecls = catMaybes mDecls
l <- mapM extractBindings newDecls
let bs = concatMap snd l
checkUniqueVars bs
mapM_ addVarDecl bs
mt <- resolve ga hd
putAssumps as
let newT = case mt of Just trm -> trm
_ -> hd
recurse $ LambdaTerm (map fst l) part newT ps
CaseTerm hd eqs ps -> do
mt <- resolve ga hd
let newT = case mt of Just trm -> trm
_ -> hd
newEs <- resolveCaseEqs ga eqs
recurse $ CaseTerm newT newEs ps
LetTerm b eqs hd ps -> do
newEs <- resolveLetEqs ga eqs
mt <- resolve ga hd
let newT = case mt of Just trm -> trm
_ -> hd
putAssumps as
recurse $ LetTerm b newEs newT ps
TermToken tok -> do
let (ds1, trm) = convertMixfixToken
(literal_annos ga)
ResolvedMixTerm TermToken tok
addDiags ds1
self tt $ oneStep $
case trm of
TermToken _ -> (trm, tok)
_ -> (trm, exprTok
{tokPos = tokPos tok})
_ -> error ("iterCharts: " ++ show t)
resolve :: GlobalAnnos -> Term -> State Env (Maybe Term)
resolve ga trm =
do as <- gets assumps
ps@((_, _, m), _) <- gets preIds
chart<- iterateCharts ga [trm] $
initChart (listRules m ga ++
(initTermRules ps $ Set.fromDistinctAscList
$ Map.keys as)) Set.empty
let Result ds mr = getResolved showPretty (posOfTerm trm)
toMixTerm chart
addDiags ds
return mr
-- * equation stuff
resolveCaseEq :: GlobalAnnos -> ProgEq -> State Env (Maybe ProgEq)
resolveCaseEq ga (ProgEq p t ps) =
do mp <- resolveConstrPattern ga p
case mp of
Nothing -> return Nothing
Just np -> do
as <- gets assumps
(newP, bs) <- extractBindings np
checkUniqueVars bs
mapM_ addVarDecl bs
mtt <- resolve ga t
putAssumps as
return $ case mtt of
Nothing -> Nothing
Just newT -> Just $ ProgEq newP newT ps
resolveCaseEqs :: GlobalAnnos -> [ProgEq] -> State Env [ProgEq]
resolveCaseEqs _ [] = return []
resolveCaseEqs ga (eq:rt) =
do mEq <- resolveCaseEq ga eq
eqs <- resolveCaseEqs ga rt
return $ case mEq of
Nothing -> eqs
Just newEq -> newEq : eqs
resolveLetEqs :: GlobalAnnos -> [ProgEq] -> State Env [ProgEq]
resolveLetEqs _ [] = return []
resolveLetEqs ga (ProgEq pat trm ps : rt) =
do mPat <- resolveConstrPattern ga pat
case mPat of
Nothing -> do resolve ga trm
resolveLetEqs ga rt
Just nPat -> do
(newPat, bs) <- extractBindings nPat
checkUniqueVars bs
mapM addVarDecl bs
mTrm <- resolve ga trm
case mTrm of
Nothing -> resolveLetEqs ga rt
Just newTrm -> do
eqs <- resolveLetEqs ga rt
return (ProgEq newPat newTrm ps : eqs)
-- * pattern stuff
-- | extract bindings from a pattern
extractBindings :: Pattern -> State Env (Pattern, [VarDecl])
extractBindings pat =
case pat of
PatternVar l@(VarDecl v t sk ps) -> case t of
MixfixType [] ->
do tvar <- toEnvState freshVar
let ty = TypeName tvar star 1
vd = VarDecl v ty sk ps
return (PatternVar vd, [vd])
_ -> do mt <- anaStarType t
case mt of
Just ty -> do
let vd = VarDecl v ty sk ps
return (PatternVar vd, [vd])
_ -> return (pat, [l])
-- PatternConstr _ _ _ -> return (pat, [])
ResolvedMixPattern i pats ps -> do
l <- mapM extractBindings pats
return (ResolvedMixPattern i (map fst l) ps, concatMap snd l)
ApplPattern p1 p2 ps -> do
(p3, l1) <- extractBindings p1
(p4, l2) <- extractBindings p2
return (ApplPattern p3 p4 ps, l1 ++ l2)
TuplePattern pats ps -> do
l <- mapM extractBindings pats
return (mkTuplePattern (map fst l) ps, concatMap snd l)
TypedPattern p ty ps -> do
mt <- anaStarType ty
let newT = case mt of Just t -> t
_ -> ty
case p of
PatternVar (VarDecl v (MixfixType []) sk _) -> do
let vd = VarDecl v newT sk ps
return (PatternVar vd, [vd])
_ -> do (newP, bs) <- extractBindings p
return (TypedPattern newP newT ps, bs)
AsPattern p1 p2 ps -> do
(p3, l1) <- extractBindings p1
(p4, l2) <- extractBindings p2
return (AsPattern p3 p4 ps, l1 ++ l2)
_ -> return (pat, [])
-- _ -> error ("extractBindings: " ++ show pat)
resolveConstrPattern :: GlobalAnnos -> Pattern
-> State Env (Maybe Pattern)
resolveConstrPattern ga pat =
do as <- gets assumps
let newAs = filterAssumps ( \ o -> case opDefn o of
ConstructData _ -> True
VarDefn -> True
_ -> False) as
putAssumps newAs
mp <- resolvePattern ga pat
putAssumps as
return mp
initPatternRules :: (PrecMap, Set.Set Id) -> [Id] -> [Rule]
initPatternRules (pm, ps) is =
map ( \ i -> mixRule (getIdPrec pm ps i) i)
([parenId, tupleId, exprId, unknownId, applId]
++ is) ++
map ( \ i -> (protect i, getIdPrec pm ps i,
getPlainTokenList i )) (filter isMixfix is)
addPatternType :: Pattern -> Pattern -> Pattern
addPatternType (TypedPattern _ ty ps) p = TypedPattern p ty ps
addPatternType _ _ = error "addPatternType"
mkPatAppl :: Pattern -> Pattern -> [Pos] -> Pattern
mkPatAppl op arg qs =
case op of
ResolvedMixPattern i as ps ->
ResolvedMixPattern i (as++[arg]) (ps++qs)
PatternVar (VarDecl i (MixfixType []) _ _) ->
ResolvedMixPattern i [arg] qs
TypedPattern p ty ps ->
TypedPattern (mkPatAppl p arg qs) ty ps
_ -> error ("mkPatAppl: " ++ show op)
toPat :: Id -> Int -> [Pattern] -> [Pos] -> Pattern
toPat i _ ar qs =
if i == applId then assert (length ar == 2) $
let [op, arg] = ar in mkPatAppl op arg qs
else if i == tupleId then
mkTuplePattern ar qs
else if isUnknownId i then
PatternVar (VarDecl (simpleIdToId $ unToken i)
(MixfixType []) Other qs)
else ResolvedMixPattern i
(if null ar then []
else if isSingle ar then [head ar]
else [mkTuplePattern ar qs]) qs
type PatChart = Chart Pattern Int
iterPatCharts :: GlobalAnnos -> [Pattern] -> PatChart -> State Env PatChart
iterPatCharts ga pats chart=
let self = iterPatCharts ga
oneStep = nextChart addPatternType (opKindFilter 0)
toPat ga chart
in if null pats then return chart
else
do let p:pp = pats
recurse pt = self pp $
oneStep (pt, exprTok {tokPos = posOfPat pt})
case p of
MixfixPattern ps -> self (ps ++ pp) chart
BracketPattern b ps qs -> self
(expandPos PatternToken (getBrackets b) ps qs ++ pp) chart
TypedPattern hd typ ps -> do
mp <- resolvePattern ga hd
let np = case mp of Just pt -> pt
_ -> p
recurse $ TypedPattern np typ ps
PatternToken tok -> self pp $ oneStep (p, tok)
_ -> error ("iterPatCharts: " ++ show p)
getKnowns :: Id -> Knowns
getKnowns (Id ts cs _) = Set.union (Set.fromList (map tokStr ts)) $
Set.unions (map getKnowns cs)
resolvePattern :: GlobalAnnos -> Pattern -> State Env (Maybe Pattern)
resolvePattern ga pat =
do as <- gets assumps
ps <- gets preIds
let ids = Map.keys as
ks = Set.union (Set.fromList (tokStr exprTok: inS :
map (:[]) "{}[](),"))
$ Set.unions $ map getKnowns ids
chart <- iterPatCharts ga [pat] $ initChart (initPatternRules ps ids) ks
let Result ds mp = getResolved showPretty (posOfPat pat) toPat chart
addDiags ds
return mp