git.iko.soy/Idris-dev
on master help sign in
Add accessibility recognition.
commitec85560fb78e1d91e08f492e1452c8408070e9ef authorMatus Tejiscak <ziman@functor.sk> dateTue 11 Feb 2014, 13:47 (13 years ago) parent5047cc5
4 files changed+19−6
compare with master
unifiedsplit
src/Idris/AbsSyntaxTree.hs+2−2 src/Idris/ElabDecls.hs+14−1 src/Idris/IBC.hs+2−2 src/Idris/ParseExpr.hs+1−1
src/Idris/AbsSyntaxTree.hs+2−2
@@ -399,7 +399,7 @@ data Plicity = Imp { pargopts :: [ArgOpt],
399399 pparam :: Bool }
400400 | Exp { pargopts :: [ArgOpt],
401401 pstatic :: Static,
402− pparam :: Bool }
402+ pparam :: Bool } -- this is a param (rather than index)
403403 | Constraint { pargopts :: [ArgOpt],
404404 pstatic :: Static }
405405 | TacImp { pargopts :: [ArgOpt],
@@ -793,7 +793,7 @@ data PArg' t = PImp { priority :: Int,
793793 getTm :: t }
794794 deriving (Show, Eq, Functor)
795795
796−data ArgOpt = Lazy | HideDisplay | ErasedArg
796+data ArgOpt = Lazy | HideDisplay | InaccessibleArg
797797 deriving (Show, Eq)
798798
799799lazyarg :: 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
8484 ty' <- addUsingConstraints syn fc ty'
8585 ty' <- implicit info syn n ty'
8686
87− let ty = addImpl i ty'
87+ let ty = addImpl i ty'
88+ inacc = inaccessible 0 ty
8889 logLvl 3 $ show n ++ " type " ++ showTmImpls ty
90+ logLvl 5 $ "Erased params: " ++ show inacc
91+
8992 ((tyT, defer, is), log) <-
9093 tclift $ elaborate ctxt n (TType (UVal 0)) []
9194 (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
161164 lst = txt "List"
162165 errrep = txt "ErrorReportPart"
163166
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+
164177 tyIsHandler (Bind _ (Pi (P _ (NS (UN e) ns1) _))
165178 (App (P _ (NS (UN m) ns2) _)
166179 (App (P _ (NS (UN l) ns3) _)
src/Idris/IBC.hs+2−2
@@ -1319,13 +1319,13 @@ instance Binary ArgOpt where
13191319 = case x of
13201320 Lazy -> putWord8 0
13211321 HideDisplay -> putWord8 1
1322− ErasedArg -> putWord8 2
1322+ InaccessibleArg -> putWord8 2
13231323 get
13241324 = do i <- getWord8
13251325 case i of
13261326 0 -> return Lazy
13271327 1 -> return HideDisplay
1328− 2 -> return ErasedArg
1328+ 2 -> return InaccessibleArg
13291329 _ -> error "Corrupted binary data for Static"
13301330
13311331instance Binary Static where
src/Idris/ParseExpr.hs+1−1
@@ -835,7 +835,7 @@ pi syn =
835835
836836piOpts :: SyntaxInfo -> IdrisParser [ArgOpt]
837837piOpts syn | implicitAllowed syn =
838− lchar '.' *> return [ErasedArg]
838+ lchar '.' *> return [InaccessibleArg]
839839 <|> return []
840840piOpts syn = return []
841841