9071856 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Make isTConName and friends exact

9071856David Raymond Christiansen12 years ago

src/Idris/Core/Evaluate.hs+21−25

compare with master

unifiedsplit

@@ -971,47 +971,43 @@ isConName n ctxt = isTConName n ctxt || isDConName n ctxt

971

972isTConName :: Name -> Context -> Bool

973isTConName n ctxt

974− = or $ do def <- lookupCtxt n (definitions ctxt)

974+ = case lookupDefExact n ctxt of

975− case tfst def of

976− (TyDecl (TCon _ _) _) -> return True

975+ Just (TyDecl (TCon _ _) _) -> True

977− _ -> return False

976+ _ -> False

978

977

979isDConName :: Name -> Context -> Bool

978isDConName :: Name -> Context -> Bool

980isDConName n ctxt

979isDConName n ctxt

981− = or $ do def <- lookupCtxt n (definitions ctxt)

980+ = case lookupDefExact n ctxt of

982− case tfst def of

983− (TyDecl (DCon _ _ _) _) -> return True

981+ Just (TyDecl (DCon _ _ _) _) -> True

984− _ -> return False

982+ _ -> False

985

983

986isFnName :: Name -> Context -> Bool

984isFnName :: Name -> Context -> Bool

987isFnName n ctxt

985isFnName n ctxt

988− = let def = lookupCtxtExact n (definitions ctxt) in

986+ = case lookupDefExact n ctxt of

989− case def of

990− Just (Function _ _, _, _, _) -> True

987+ Just (Function _ _) -> True

991− Just (Operator _ _ _, _, _, _) -> True

988+ Just (Operator _ _ _) -> True

992− Just (CaseOp _ _ _ _ _ _, _, _, _) -> True

989+ Just (CaseOp _ _ _ _ _ _) -> True

993− _ -> False

990+ _ -> False

994

991

995isTCDict :: Name -> Context -> Bool

992isTCDict :: Name -> Context -> Bool

996isTCDict n ctxt

993isTCDict n ctxt

997− = let def = lookupCtxtExact n (definitions ctxt) in

994+ = case lookupDefExact n ctxt of

998− case def of

999− Just (Function _ _, _, _, _) -> False

995+ Just (Function _ _) -> False

1000− Just (Operator _ _ _, _, _, _) -> False

996+ Just (Operator _ _ _) -> False

1001− Just (CaseOp ci _ _ _ _ _, _, _, _) -> tc_dictionary ci

997+ Just (CaseOp ci _ _ _ _ _) -> tc_dictionary ci

1002− _ -> False

998+ _ -> False

1003

999

1004lookupP :: Name -> Context -> [Term]

1000lookupP :: Name -> Context -> [Term]

1005lookupP n ctxt

1001lookupP n ctxt

1006 = do def <- lookupCtxt n (definitions ctxt)

1002 = do def <- lookupCtxt n (definitions ctxt)

1007 p <- case def of

1003 p <- case def of

1008− (Function ty tm, a, _, _) -> return (P Ref n ty, a)

1004+ (Function ty tm, a, _, _) -> return (P Ref n ty, a)

1009− (TyDecl nt ty, a, _, _) -> return (P nt n ty, a)

1005+ (TyDecl nt ty, a, _, _) -> return (P nt n ty, a)

1010 (CaseOp _ ty _ _ _ _, a, _, _) -> return (P Ref n ty, a)

1006 (CaseOp _ ty _ _ _ _, a, _, _) -> return (P Ref n ty, a)

1011− (Operator ty _ _, a, _, _) -> return (P Ref n ty, a)

1007+ (Operator ty _ _, a, _, _) -> return (P Ref n ty, a)

1012 case snd p of

1008 case snd p of

1013− Hidden -> []

1009+ Hidden -> []

1014− _ -> return (fst p)

1010+ _ -> return (fst p)

1015

1011

1016lookupDefExact :: Name -> Context -> Maybe Def

1012lookupDefExact :: Name -> Context -> Maybe Def

1017lookupDefExact n ctxt = tfst <$> lookupCtxtExact n (definitions ctxt)

1013lookupDefExact n ctxt = tfst <$> lookupCtxtExact n (definitions ctxt)

src/Idris/Delaborate.hs+1−1

@@ -488,7 +488,7 @@ fancifyAnnots ist annot@(AnnName n _ _ _) =

488 _ | isTConName n ctxt -> AnnName n (Just TypeOutput) docs ty

489 _ | isMetavarName n ist -> AnnName n (Just MetavarOutput) docs ty

490 _ | isPostulateName n ist -> AnnName n (Just PostulateOutput) docs ty

491− _ | otherwise -> annot

491+ _ | otherwise -> annot

492 where docOverview :: IState -> Name -> Maybe String -- pretty-print first paragraph of docs

493 docOverview ist n = do docs <- lookupCtxtExact n (idris_docstrings ist)

494 let o = overview (fst docs)