isTypeList :: Env -> [Term] -> Bool
isTypeList e l = case mapM termToType l of
mapM ( \ t -> anaTypeM (Nothing, t) e) ts
in isJust ml && not (hasErrors ds)
termToType :: Term -> Maybe Type
>> parseType <<
P.eof) (emptyAnnos ()) "" $ showDoc t "" of
termToId :: Term -> Maybe Id
termToId t = case
P.parse (uninstOpId <<
P.eof) "" $ showDoc t "" of
iterateCharts :: GlobalAnnos ->
Set.Set [Id] -> [Term] -> Chart Term
-> State Env (Chart Term)
iterateCharts ga compIds terms chart =
let self = iterateCharts ga compIds
oneStep = nextChart addType (toMixTerm e) ga chart
let recurse trm = self tt $
oneStep (trm, exprTok {tokPos = getRange trm})
MixfixTerm ts -> self (ts ++ tt) chart
MixTypeTerm q typ ps -> do
Just nTyp -> self tt $ oneStep
(MixTypeTerm q (monoType nTyp) ps,
let bres = self (expandPos TermToken
(getBrackets b) ts ps ++ tt) chart
if isCompoundList compIds ts then do
addDiags [mkDiag Hint "is compound list" t]
else if isTypeList e ts then do
addDiags [mkDiag Hint "is type list" t]
self tt $ oneStep (t, typeInstTok {tokPos = ps})
QualVar (VarDecl v typ ok ps) -> do
Just nType -> recurse $ QualVar $
VarDecl v (monoType nType) ok ps
QualOp b (InstOpId v ts qs) sc ps -> do
Nothing -> addDiags [mkDiag Error
recurse $ QualOp b (InstOpId v newTs qs) nSc ps
QuantifiedTerm quant decls hd ps -> do
newDs <- mapM (anaddGenVarDecl False) decls
let newT = case mt of Just trm -> trm
recurse $ QuantifiedTerm quant (catMaybes newDs) newT ps
LambdaTerm decls part hd ps -> do
mDecls <- mapM (resolvePattern ga) decls
let anaDecls = catMaybes mDecls
bs = concatMap extractVars anaDecls
mapM_ (addLocalVar False) bs
recurse $ LambdaTerm anaDecls part (maybe hd id mt) ps
newEs <- resolveCaseEqs ga eqs
recurse $ CaseTerm (maybe hd id mt) newEs ps
LetTerm b eqs hd ps -> do
newEs <- resolveLetEqs ga eqs
recurse $ LetTerm b newEs (maybe hd id mt) ps
let (ds1, trm) = convertMixfixToken
(flip ResolvedMixTerm [])
TermToken _ -> (trm, tok)
mp <- resolvePattern ga p
let newP = case mp of Just pat -> pat
recurse $ AsPattern vd newP ps
TypedTerm trm k ty ps -> do
-- assume that type is analysed
recurse $ TypedTerm (maybe trm id mt) k ty ps
_ -> error ("iterCharts: " ++ show t)
resolveCaseEq :: GlobalAnnos -> ProgEq -> State Env (Maybe ProgEq)
resolveCaseEq ga (ProgEq p t ps) =
do mp <- resolvePattern ga p
Nothing -> return Nothing
let bs = extractVars newP
mapM_ (addLocalVar False) bs
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
Just newEq -> newEq : eqs
resolveLetEqs :: GlobalAnnos -> [ProgEq] -> State Env [ProgEq]
resolveLetEqs _ [] = return []
resolveLetEqs ga (ProgEq pat trm ps : rt) =
do mPat <- resolvePattern ga pat
Nothing -> do resolve ga trm
let bs = extractVars newPat
mapM_ (addLocalVar False) bs
Nothing -> resolveLetEqs ga rt
eqs <- resolveLetEqs ga rt
return (ProgEq newPat newTrm ps : eqs)
mkPatAppl :: Term -> Term -> Range -> Term
QualVar (VarDecl i (MixfixType []) _ _) ->
ResolvedMixTerm i [] [arg] qs
bracketTermToTypes :: Env -> Term -> [Type]
bracketTermToTypes e t = case t of
BracketTerm Squares tys _ ->
map (monoType . snd) $ maybe (error "bracketTermToTypes") id $
maybeResult $ mapM ( \ ty -> anaTypeM (Nothing, ty) e) $
maybe (error "bracketTermToTypes1") id $ mapM termToType tys
_ -> error "bracketTermToTypes2"
toMixTerm :: Env -> Id -> [Term] -> Range -> Term
if i == applId then assert (length ar == 2) $
let [op, arg] = ar in mkPatAppl op arg qs
else if i == tupleId || i == unitId then
if isMixfix j && isSingle ar then
ResolvedMixTerm j (bracketTermToTypes e $ head ar) [] qs
else assert (length ar == 1 + placeCount j) $
splitAt (placeCount $ mkId $ fst $ splitMixToken ts) ar
in ResolvedMixTerm j (bracketTermToTypes e tar) (far ++ sar) qs
_ -> ResolvedMixTerm i [] ar qs
resolvePattern :: GlobalAnnos -> Pattern -> State Env (Maybe Pattern)
resolvePattern = resolver True
resolve :: GlobalAnnos -> Term -> State Env (Maybe Term)
resolver :: Bool -> GlobalAnnos -> Term -> State Env (Maybe Term)
compIds = getCompoundLists e
let (addRule, ruleS, sIds) = makeRules ga ps (getPolyIds ass)
chart <- iterateCharts ga compIds [trm] $ initChart addRule ruleS
let Result ds mr = getResolved
(showDoc . parenTerm) (getRange trm)
Just pat -> fmap Just $ anaPattern sIds pat
getPolyIds :: Assumps ->
Set.Set Id
getPolyIds =
Set.unions . map ( \ (i, OpInfos l) ->
foldr ( \ oi s -> case opType oi of
getCompound :: Id -> [Id]
getCompound (Id _ cs _) = cs
getCompoundLists :: Env ->
Set.Set [Id]
builtinIds = [unitId, parenId, tupleId, exprId, typeId, applId]
makeRules ga ps@(p, _) polyIds aIds =
in ( \ tok -> if isSimpleToken tok
[(simpleIdToId tok, m2, [tok])] else []
, partitionRules $ listRules m2 ga ++
initRules :: (PrecMap,
Set.Set Id) -> [Id] -> [Id] -> [Id] -> [Rule]
initRules (p, ps) polyIds bs is =
map ( \ i -> mixRule (getIdPrec p ps i) i)
map ( \ i -> (protect i, maxWeight p + 3, getPlainTokenList i))
-- identifiers with a positive number of type arguments
map ( \ i -> ( polyId i, getIdPrec p ps i
, getPolyTokenList termStr i)) polyIds ++
map ( \ i -> ( protect $ polyId i, maxWeight p + 3
, getPolyTokenList place i)) (filter isMixfix polyIds)
polyId (Id ts cs ps) = let (toks, pls) = splitMixToken ts in
Id (toks ++ [typeInstTok] ++ pls) cs ps
getPolyTokenList :: String -> Id -> [Token]
getPolyTokenList str (Id ts cs ps) =
let (toks, pls) = splitMixToken ts in
getTokenList str (Id toks cs ps) ++
typeInstTok : getTokenList str (Id pls [] ps)
unPolyId :: Id -> Maybe Id
unPolyId (Id ts cs ps) = let (ft, rt) = partition (== typeInstTok) ts in
[_] -> Just $ Id rt cs ps
-- create fresh type vars for unknown ids tagged with type MixfixType [].
anaPattern ::
Set.Set Id -> Pattern -> State Env Pattern
anaPattern s pat = case pat of
QualVar vd -> do newVd <- checkVarDecl vd
ResolvedMixTerm i tys pats ps | null pats && null tys &&
(isSimpleId i || i == simpleIdToId uTok) &&
(tvar, c) <- toEnvState $ freshVar $ posOfId i
return $ QualVar $ VarDecl i (TypeName tvar rStar c) Other ps
l <- mapM (anaPattern s) pats
return $ ResolvedMixTerm i tys l ps
return $ ApplTerm p3 p4 ps
l <- mapM (anaPattern s) pats
TypedTerm p q ty ps -> do
QualVar (VarDecl v (MixfixType []) ok qs) ->
let newVd = VarDecl v ty ok (qs `appRange` ps) in
_ -> do newP <- anaPattern s p
return $ TypedTerm newP q ty ps
return $ AsPattern newVd p4 ps
where checkVarDecl vd@(VarDecl v t ok ps) = case t of
(tvar, c) <- toEnvState $ freshVar $ posOfId v
return $ VarDecl v (TypeName tvar rStar c) ok ps