6c4d0f1 · Idris-dev · git.iko.soy

src/Idris/AbsSyntaxTree.hs+8−1

compare with master

unifiedsplit

@@ -112,6 +112,7 @@ data IState = IState {

112 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos

113 idris_calledgraph :: Ctxt [Name],

114 idris_docstrings :: Ctxt String,

115+ idris_tyinfodata :: Ctxt TIData,

115 idris_totcheck :: [(FC, Name)], -- names to check totality on

116 idris_totcheck :: [(FC, Name)], -- names to check totality on

116 idris_defertotcheck :: [(FC, Name)], -- names to check at the end

117 idris_defertotcheck :: [(FC, Name)], -- names to check at the end

117 idris_options :: IOption,

118 idris_options :: IOption,

@@ -216,7 +217,7 @@ idrisInit :: IState

216idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

217idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

217 emptyContext emptyContext emptyContext emptyContext

218 emptyContext emptyContext emptyContext emptyContext

219 emptyContext emptyContext emptyContext emptyContext

219− emptyContext

220+ emptyContext emptyContext

220 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

221 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

221 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

222 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

222 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty

223 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty

@@ -811,6 +812,12 @@ deriving instance Binary ClassInfo

811deriving instance NFData ClassInfo

812deriving instance NFData ClassInfo

812!-}

813!-}

813

814

815+-- Type inference data

816+

817+data TIData = TIPartial -- ^ a function with a partially defined type

818+ | TISolution Term -- ^ solution to a metavariable in a type

819+ deriving Show

820+

814-- An argument is conditionally forceable iff its forceability

821-- An argument is conditionally forceable iff its forceability

815-- depends on the collapsibility of the whole type.

822-- depends on the collapsibility of the whole type.

816data Forceability = Conditional | Unconditional deriving (Show, Enum, Bounded, Eq, Ord)

823data Forceability = Conditional | Unconditional deriving (Show, Enum, Bounded, Eq, Ord)

src/Idris/Core/Elaborate.hs−2

@@ -466,8 +466,6 @@ apply' fillt fn imps =

466 do args <- prepare_apply fn (map fst imps)

467 -- _Don't_ solve the arguments we're specifying by hand.

468 -- (remove from unified list before calling end_unify)

469− -- HMMM: Actually, if we get it wrong, the typechecker will complain!

470− -- so do nothing

471 hs <- get_holes

469 hs <- get_holes

472 ES (p, a) s prev <- get

470 ES (p, a) s prev <- get

473 let dont = head hs : dontunify p ++

471 let dont = head hs : dontunify p ++

src/Idris/Delaborate.hs+1−1

@@ -151,7 +151,7 @@ pprintErr' i (CantUnify _ x y e sc s) =

151 _ -> line <> line <> text "Specifically:" <>

152 indented (pprintErr' i e) <>

153 if (opt_errContext (idris_options i)) then text $ showSc i sc else empty

154−pprintErr' i (CantConvert x y env) =

154+pprintErr' i (CantConvert x y env) = trace (show (x,y)) $

155 text "Can't convert" <> indented (pprintTerm i (delab i x)) <$>

156 text "with" <> indented (pprintTerm i (delab i y)) <>

157 if (opt_errContext (idris_options i)) then line <> text (showSc i env) else empty

src/Idris/ElabDecls.hs+15−6

@@ -49,9 +49,18 @@ recheckC fc env t

49 addConstraints fc cs

50 return (tm, ty)

51

52+

53+checkDef fc ns = checkAddDef False fc ns

54+

55+checkAddDef add fc [] = return []

56+checkAddDef add fc ((n, (i, top, t)) : ns)

52−checkDef fc ns = do ctxt <- getContext

57+ = do ctxt <- getContext

58+ (t', _) <- recheckC fc [] t

59+ when add $ addDeferred [(n, (i, top, t, True))]

60+ ns' <- checkAddDef add fc ns

61+ return ((n, (i, top, t')) : ns')

53− mapM (\(n, (i, top, t)) -> do (t', _) <- recheckC fc [] t

62+-- mapM (\(n, (i, top, t)) -> do (t', _) <- recheckC fc [] t

54− return (n, (i, top, t'))) ns

63+-- return (n, (i, top, t'))) ns

55

64

56-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

65-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

57elabType :: ElabInfo -> SyntaxInfo -> String ->

66elabType :: ElabInfo -> SyntaxInfo -> String ->

@@ -76,9 +85,9 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty

76 ((tyT, defer, is), log) <-

85 ((tyT, defer, is), log) <-

77 tclift $ elaborate ctxt n (TType (UVal 0)) []

86 tclift $ elaborate ctxt n (TType (UVal 0)) []

78 (errAt "type of " n (erun fc (build i info False [] n ty)))

87 (errAt "type of " n (erun fc (build i info False [] n ty)))

79− ds <- checkDef fc defer

88+ ds <- checkAddDef True fc defer

80− let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds

89+-- let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds

81− addDeferred ds'

90+-- addDeferred ds'

82 mapM_ (elabCaseBlock info opts) is

91 mapM_ (elabCaseBlock info opts) is

83 ctxt <- getContext

92 ctxt <- getContext

84 logLvl 5 $ "Rechecking"

93 logLvl 5 $ "Rechecking"

src/Idris/ElabTerm.hs+2−1

@@ -841,7 +841,8 @@ collectDeferred :: Maybe Name ->

841 Term -> State [(Name, (Int, Maybe Name, Type))] Term

842collectDeferred top (Bind n (GHole i t) app) =

843 do ds <- get

844+ t' <- collectDeferred top t

844− when (not (n `elem` map fst ds)) $ put ((n, (i, top, t)) : ds)

845+ when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, t'))])

845 collectDeferred top app

846 collectDeferred top app

846collectDeferred top (Bind n b t) = do b' <- cdb b

847collectDeferred top (Bind n b t) = do b' <- cdb b

847 t' <- collectDeferred top t

848 t' <- collectDeferred top t

src/Idris/ParseOps.hs+1−1

@@ -39,7 +39,7 @@ table fixes

39 [[backtick],

40 [binary "$" (\fc x y -> PApp fc x [pexp y]) AssocRight],

41 [binary "=" PEq AssocLeft],

42− [binary "->" (\fc x y -> PPi expl (sMN 42 "__pi_arg") x y) AssocRight]]

42+ [binary "->" (\fc x y -> PPi expl (sUN "__pi_arg") x y) AssocRight]]

43

44-- | Calculates table for fixtiy declarations

45toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm