MixfixParser.hs revision 75a6279dbae159d018ef812185416cf6df386c10
66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder
5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian Maeder{- |
66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederModule : $Header$
66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederCopyright : Christian Maeder and Uni Bremen 2002-2003
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder
ffd01020a4f35f434b912844ad6e0d6918fadffdChristian MaederMaintainer : hets@tzi.de
66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederStability : experimental
66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederPortability : portable
fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder
fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder Mixfix analysis of terms
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder
fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder Missing features:
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder - the positions of ids from string, list, number and floating annotations
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder is not changed within applications (and might be misleading)
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder-}
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maedermodule CASL.MixfixParser ( resolveFormula, resolveMixfix)
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder where
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport CASL.AS_Basic_CASL
5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian Maederimport Common.GlobalAnnotations
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport Common.Result
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport Common.Id
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport qualified Common.Lib.Set as Set
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport Common.Lexer
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport Control.Monad
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport Common.Lib.Parsec
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport Common.Earley
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport CASL.ShowMixfix
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- import Control.Exception (assert)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maederassert :: Bool -> a -> a
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maederassert b a = if b then a else error ("assert")
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maedertype Rule = (Id, Bool, [Token]) -- True means predicate
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermkRule :: Id -> Rule
024621f43239cfe9629e35d35a8669fad7acbba2Christian MaedermkRule = mixRule False
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermkSingleArgRule :: Bool -> Id -> Rule
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedermkSingleArgRule b ide = (protect ide, b, getPlainTokenList ide ++ [varTok])
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
27912d626bf179b82fcb337077e5cd9653bb71cfChristian MaedermkSingleOpArgRule :: Bool -> Id -> Rule
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermkSingleOpArgRule b ide = (protect ide, b, getPlainTokenList ide ++ [exprTok])
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian MaedermkArgsRule :: Bool -> Id -> Rule
5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian MaedermkArgsRule b ide = (protect ide, b, getPlainTokenList ide
5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian Maeder ++ getTokenPlaceList tupleId)
8c81b727b788d90ff3b8cbda7b0900c9009243bbChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedersingleArgId, singleOpArgId, multiArgsId :: Id
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedersingleArgId = mkId (getPlainTokenList exprId ++ [varTok])
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedersingleOpArgId = mkId (getPlainTokenList exprId ++ [exprTok])
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedermultiArgsId = mkId (getPlainTokenList exprId ++
07b1bf56f3a486f26d69514d05b73100abb25a0eChristian Maeder getPlainTokenList tupleId)
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederinitRules :: GlobalAnnos -> IdSet -> Bool -> [Rule]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederinitRules ga (opS, predS, _) maybeFormula =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder let ops = Set.toList opS
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder preds = if maybeFormula then
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Set.toList predS else []
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder in concat [ mkRule typeId :
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder mkRule exprId :
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder mkRule varId :
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder mkRule singleArgId :
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder mkRule singleOpArgId :
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder mkRule multiArgsId :
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder listRules False ga,
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder map (mixRule True) preds,
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder map (mkSingleArgRule True) preds,
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder map (mkSingleOpArgRule True) preds,
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder map (mkArgsRule True) preds,
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder map mkRule ops,
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder map (mkSingleArgRule False) ops,
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder map (mkSingleOpArgRule False) ops,
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder map (mkArgsRule False) ops]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- | meaningful position of a term
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederposOfTerm :: TERM -> Pos
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederposOfTerm trm =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder case trm of
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Mixfix_token t -> tokPos t
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Mixfix_term ts -> posOfTerm (head ts)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Simple_id i -> tokPos i
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Mixfix_qual_pred p ->
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder case p of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Pred_name i -> posOfId i
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Qual_pred_name _ _ ps -> first (Just ps)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Application o [] [] ->
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder case o of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Op_name i -> posOfId i
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Qual_op_name _ _ ps -> first (Just ps)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder _ -> first $ get_pos_l trm
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder where first ps = case ps of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Nothing -> nullPos
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Just l -> if null l then nullPos else head l
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- | construct application
5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian MaederasAppl :: Id -> [TERM] -> [Pos] -> TERM
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederasAppl f as ps = Application (Op_name f) as ps
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian Maeder-- | constructing the parse tree from (the final) parser state(s)
5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian MaedertoAppl :: Id -> Bool -> [TERM] -> [Pos] -> TERM
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaedertoAppl ide _ ar qs =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder if ide == singleArgId || ide == multiArgsId
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder then assert (length ar > 1) $
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder let har:tar = ar
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder ps = posOfTerm har : qs
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder in case har of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Application q ts _ -> assert (null ts) $
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Application q tar ps
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Mixfix_qual_pred _ -> Mixfix_term [har,
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Mixfix_parenthesized tar ps]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder _ -> error "stateToAppl"
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder else asAppl ide ar qs
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder
8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian Maedertype IdSet = (Set.Set Id, Set.Set Id, Set.Set Id)
8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian Maeder
8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian MaederaddType :: TERM -> TERM -> TERM
c438c79d00fc438f99627e612498744bdc0d0c89Christian MaederaddType tt t =
8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian Maeder case tt of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Mixfix_sorted_term s ps -> Sorted_term t s ps
8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian Maeder Mixfix_cast s ps -> Cast t s ps
8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian Maeder _ -> error "addType"
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian MaederfilterByPredicate :: Bool -> Bool -> Maybe Bool
8aea46773664711e0910accc5cf80ef9ee1bcfbfChristian MaederfilterByPredicate bArg bOp =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder if bArg then Just False else
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder if bOp then Just True else Nothing
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
61091743da1a9ed6dfd5e077fdcc972553358962Christian Maedertype TermChart = Chart TERM Bool
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederiterateCharts :: GlobalAnnos -> IdSet -> Bool -> [TERM] -> TermChart
08b724e8dcbba5820d80f0974b9a5385140815baChristian Maeder -> TermChart
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederiterateCharts g ids maybeFormula terms c =
5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian Maeder let self = iterateCharts g ids maybeFormula
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder expand = expandPos Mixfix_token
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder oneStep = nextChart addType filterByPredicate toAppl g c
5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian Maeder resolveTerm = resolveMixTrm g ids False
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder in if null terms then c
5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian Maeder else case head terms of
5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian Maeder Mixfix_term ts -> self (ts ++ tail terms) c
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Mixfix_bracketed ts ps ->
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder self (expand ("[", "]") ts ps ++ tail terms) c
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Mixfix_braced ts ps ->
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder self (expand ("{", "}") ts ps ++ tail terms) c
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder Mixfix_parenthesized ts ps ->
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder if isSingle ts then
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder let Result mds v = resolveMixTrm g ids maybeFormula
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder $ head ts
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder tNew = case v of Nothing -> head ts
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder Just x -> x
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder c2 = self (tail terms) (oneStep (tNew, varTok))
405b95208385572f491e1e0207d8d14e31022fa6Christian Maeder in mixDiags mds c2
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder else self (expand ("(", ")") ts ps ++ tail terms) c
8c81b727b788d90ff3b8cbda7b0900c9009243bbChristian Maeder Conditional t1 f2 t3 ps ->
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder let Result mds v =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder do t4 <- resolveTerm t1
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder f5 <- resolveMixFrm g ids f2
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder t6 <- resolveTerm t3
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder return (Conditional t4 f5 t6 ps)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder tNew = case v of Nothing -> head terms
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Just x -> x
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder c2 = self (tail terms)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (oneStep (tNew, varTok {tokPos = posOfTerm tNew}))
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder in mixDiags mds c2
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Mixfix_token t -> let (ds1, trm) =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder convertMixfixToken (literal_annos g) t
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder c2 = self (tail terms) $ oneStep $
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maeder case trm of
76647324ed70f33b95a881b536d883daccf9568dChristian Maeder Mixfix_token tok -> (trm, tok)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder _ -> (trm, varTok
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder {tokPos = tokPos t})
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder in mixDiags ds1 c2
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder t@(Mixfix_sorted_term _ (p:_)) -> self (tail terms)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (oneStep (t, typeTok {tokPos = p}))
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder t@(Mixfix_cast _ (p:_)) -> self (tail terms)
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder (oneStep (t, typeTok {tokPos = p}))
341d00318de2d0ea9b6f0ab43f7e4d10ee4fb454Christian Maeder t@(Qual_var _ _ (p:_)) -> self (tail terms)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (oneStep (t, varTok {tokPos = p}))
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder t@(Application (Qual_op_name _ _ (p:_)) _ _) ->
self (tail terms) (oneStep (t, exprTok{tokPos = p} ))
t@(Mixfix_qual_pred (Qual_pred_name _ _ (p:_))) ->
self (tail terms) (oneStep (t, exprTok{tokPos = p} ))
t -> error ("iterate mixfix states: " ++ show t)
mkIdSet :: Set.Set Id -> Set.Set Id -> IdSet
mkIdSet ops preds =
let both = Set.intersection ops preds in
(ops, Set.difference preds both, preds)
resolveMixfix :: GlobalAnnos -> Set.Set Id -> Set.Set Id -> Bool -> TERM
-> Result TERM
resolveMixfix g ops preds maybeFormula t =
let r@(Result ds _) = resolveMixTrm g (mkIdSet ops preds) maybeFormula t
in if null ds then r else Result ds Nothing
resolveMixTrm :: GlobalAnnos -> IdSet -> Bool
-> TERM -> Result TERM
resolveMixTrm ga ids maybeFormula trm =
getResolved showTerm (posOfTerm trm) toAppl
$ iterateCharts ga ids maybeFormula [trm] $
initChart (initRules ga ids maybeFormula) Set.empty
resolveFormula :: GlobalAnnos -> Set.Set Id -> Set.Set Id -> FORMULA
-> Result FORMULA
resolveFormula g ops preds f =
let r@(Result ds _) = resolveMixFrm g (mkIdSet ops preds) f
in if null ds then r else Result ds Nothing
resolveMixFrm :: GlobalAnnos -> IdSet-> FORMULA -> Result FORMULA
resolveMixFrm g ids@(ops, onlyPreds, preds) frm =
let self = resolveMixFrm g ids
resolveTerm = resolveMixTrm g ids False in
case frm of
Quantification q vs fOld ps ->
let varIds = Set.fromList $ concatMap (\ (Var_decl va _ _) ->
map simpleIdToId va) vs
newIds = (Set.union ops varIds,
(Set.\\) onlyPreds varIds, preds)
in
do fNew <- resolveMixFrm g newIds fOld
return $ Quantification q vs fNew ps
Conjunction fsOld ps ->
do fsNew <- mapM self fsOld
return $ Conjunction fsNew ps
Disjunction fsOld ps ->
do fsNew <- mapM self fsOld
return $ Disjunction fsNew ps
Implication f1 f2 ps ->
do f3 <- self f1
f4 <- self f2
return $ Implication f3 f4 ps
Equivalence f1 f2 ps ->
do f3 <- self f1
f4 <- self f2
return $ Equivalence f3 f4 ps
Negation fOld ps ->
do fNew <- self fOld
return $ Negation fNew ps
Predication sym tsOld ps ->
do tsNew <- mapM resolveTerm tsOld
return $ Predication sym tsNew ps
Definedness tOld ps ->
do tNew <- resolveTerm tOld
return $ Definedness tNew ps
Existl_equation t1 t2 ps ->
do t3 <- resolveTerm t1
t4 <- resolveTerm t2
return $ Existl_equation t3 t4 ps
Strong_equation t1 t2 ps ->
do t3 <- resolveTerm t1
t4 <- resolveTerm t2
return $ Strong_equation t3 t4 ps
Membership tOld s ps ->
do tNew <- resolveTerm tOld
return $ Membership tNew s ps
Mixfix_formula tOld ->
do tNew <- resolveMixTrm g ids True tOld
mkPredication tNew
where mkPredication t =
case t of
Application (Op_name ide) as ps ->
let p = Predication (Pred_name ide) as ps in
if ide `Set.member` preds
then return p else
plain_error p
("not a predicate: " ++ showId ide "")
(posOfId ide)
Mixfix_qual_pred qide ->
return $ Predication qide [] []
Mixfix_term [Mixfix_qual_pred qide,
Mixfix_parenthesized ts ps] ->
return $ Predication qide ts ps
_ -> plain_error (Mixfix_formula t)
("not a formula: " ++ showTerm t "")
(posOfTerm t)
f -> return f
-- ---------------------------------------------------------------
-- convert literals
-- ---------------------------------------------------------------
makeStringTerm :: Id -> Id -> Token -> TERM
makeStringTerm c f tok =
makeStrTerm (incSourceColumn sp 1) str
where
sp = tokPos tok
str = init (tail (tokStr tok))
makeStrTerm p l =
if null l then asAppl c [] [p]
else let (hd, tl) = splitString caslChar l
in asAppl f [asAppl (Id [Token ("'" ++ hd ++ "'") p] [] []) [] [p],
makeStrTerm (incSourceColumn p $ length hd) tl] [p]
makeNumberTerm :: Id -> Token -> TERM
makeNumberTerm f t@(Token n p) =
case n of
[] -> error "makeNumberTerm"
[_] -> asAppl (Id [t] [] []) [] [p]
hd:tl -> asAppl f [asAppl (Id [Token [hd] p] [] []) [] [p],
makeNumberTerm f (Token tl
(incSourceColumn p 1))] [p]
makeFraction :: Id -> Id -> Token -> TERM
makeFraction f d t@(Token s p) =
let (n, r) = span (\c -> c /= '.') s
dotOffset = length n
in if null r then makeNumberTerm f t
else asAppl d [makeNumberTerm f (Token n p),
makeNumberTerm f (Token (tail r)
(incSourceColumn p $ dotOffset + 1))]
[incSourceColumn p dotOffset]
makeSignedNumber :: Id -> Token -> TERM
makeSignedNumber f t@(Token n p) =
case n of
[] -> error "makeSignedNumber"
hd:tl ->
if hd == '-' || hd == '+' then
asAppl (Id [Token [hd] p] [] [])
[makeNumberTerm f (Token tl $ incSourceColumn p 1)] [p]
else makeNumberTerm f t
makeFloatTerm :: Id -> Id -> Id -> Token -> TERM
makeFloatTerm f d e t@(Token s p) =
let (m, r) = span (\c -> c /= 'E') s
offset = length m
in if null r then makeFraction f d t
else asAppl e [makeFraction f d (Token m p),
makeSignedNumber f (Token (tail r)
$ incSourceColumn p (offset + 1))]
[incSourceColumn p offset]
-- analyse Mixfix_token
convertMixfixToken:: LiteralAnnos -> Token -> ([Diagnosis], TERM)
convertMixfixToken ga t =
if isString t then
case string_lit ga of
Nothing -> err "string"
Just (c, f) -> ([], makeStringTerm c f t)
else if isNumber t then
case number_lit ga of
Nothing -> err "number"
Just f -> if isFloating t then
case float_lit ga of
Nothing -> err "floating"
Just (d, e) -> ([], makeFloatTerm f d e t)
else ([], makeNumberTerm f t)
else ([], te)
where te = Mixfix_token t
err s = ([Diag Error ("missing %" ++ s ++ " annotation") (tokPos t)]
, te)