ec85560 · Idris-dev · git.iko.soy

src/Idris/AbsSyntaxTree.hs+2−2

compare with master

unifiedsplit

@@ -399,7 +399,7 @@ data Plicity = Imp { pargopts :: [ArgOpt],

399 pparam :: Bool }

400 | Exp { pargopts :: [ArgOpt],

401 pstatic :: Static,

402− pparam :: Bool }

402+ pparam :: Bool } -- this is a param (rather than index)

403 | Constraint { pargopts :: [ArgOpt],

404 pstatic :: Static }

405 | TacImp { pargopts :: [ArgOpt],

@@ -793,7 +793,7 @@ data PArg' t = PImp { priority :: Int,

793 getTm :: t }

794 deriving (Show, Eq, Functor)

795

796−data ArgOpt = Lazy | HideDisplay | ErasedArg

796+data ArgOpt = Lazy | HideDisplay | InaccessibleArg

797 deriving (Show, Eq)

798

799lazyarg :: PArg' t -> Bool

src/Idris/ElabDecls.hs+14−1

@@ -84,8 +84,11 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

84 ty' <- addUsingConstraints syn fc ty'

85 ty' <- implicit info syn n ty'

86

87− let ty = addImpl i ty'

87+ let ty = addImpl i ty'

88+ inacc = inaccessible 0 ty

88 logLvl 3 $ show n ++ " type " ++ showTmImpls ty

89 logLvl 3 $ show n ++ " type " ++ showTmImpls ty

90+ logLvl 5 $ "Erased params: " ++ show inacc

91+

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

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

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

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

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

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

@@ -161,6 +164,16 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

161 lst = txt "List"

164 lst = txt "List"

162 errrep = txt "ErrorReportPart"

165 errrep = txt "ErrorReportPart"

163

166

167+ inaccessible :: Int -> PTerm -> [Int]

168+ inaccessible i (PPi (Imp _ _ _ _) n Placeholder t)

169+ = i : inaccessible (i+1) t -- unbound implicit

170+ inaccessible i (PPi plicity n ty t)

171+ | InaccessibleArg `elem` pargopts plicity

172+ = i : inaccessible (i+1) t -- an .{erased : Implicit}

173+ | otherwise

174+ = inaccessible (i+1) t -- a {regular : Implicit}

175+ inaccessible _ _ = []

176+

164 tyIsHandler (Bind _ (Pi (P _ (NS (UN e) ns1) _))

177 tyIsHandler (Bind _ (Pi (P _ (NS (UN e) ns1) _))

165 (App (P _ (NS (UN m) ns2) _)

178 (App (P _ (NS (UN m) ns2) _)

166 (App (P _ (NS (UN l) ns3) _)

179 (App (P _ (NS (UN l) ns3) _)

src/Idris/IBC.hs+2−2

@@ -1319,13 +1319,13 @@ instance Binary ArgOpt where

1319 = case x of

1320 Lazy -> putWord8 0

1321 HideDisplay -> putWord8 1

1322− ErasedArg -> putWord8 2

1322+ InaccessibleArg -> putWord8 2

1323 get

1324 = do i <- getWord8

1325 case i of

1326 0 -> return Lazy

1327 1 -> return HideDisplay

1328− 2 -> return ErasedArg

1328+ 2 -> return InaccessibleArg

1329 _ -> error "Corrupted binary data for Static"

1330

1331instance Binary Static where

src/Idris/ParseExpr.hs+1−1

@@ -835,7 +835,7 @@ pi syn =

835

836piOpts :: SyntaxInfo -> IdrisParser [ArgOpt]

837piOpts syn | implicitAllowed syn =

838− lchar '.' *> return [ErasedArg]

838+ lchar '.' *> return [InaccessibleArg]

839 <|> return []

840piOpts syn = return []

841