9265e7c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Added 'public', 'abstract' and 'private' modifiers

9265e7cEdwin Brady15 years ago

src/Core/CoreParser.hs+3−2

compare with master

unifiedsplit

@@ -19,11 +19,12 @@ idrisDef = haskellDef {

19 opLetter = iOpLetter,

20 identLetter = identLetter haskellDef <|> lchar '.',

21 reservedOpNames = [":", "..", "=", "\\", "|", "<-", "->", "=>", "**"],

22− reservedNames = ["let", "in", "data", "Set", -- "if", "then", "else",

22+ reservedNames = ["let", "in", "data", "Set",

23− "do", "dsl", "import", "impossible", -- "refl",

23+ "do", "dsl", "import", "impossible",

24 "infix", "infixl", "infixr", "prefix",

25 "where", "with", "forall", "syntax", "proof",

26 "using", "params", "namespace", "class", "instance",

27+ "public", "private", "abstract",

27 "Int", "Integer", "Float", "Char", "String", "Ptr"]

28 "Int", "Integer", "Float", "Char", "String", "Ptr"]

28 }

29 }

src/Core/Evaluate.hs+16−7

@@ -1,7 +1,8 @@

1{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances,

2 PatternGuards #-}

4−module Core.Evaluate(normalise, normaliseC, simplify, specialise, hnf,

4+module Core.Evaluate(normalise, normaliseC, normaliseAll,

5+ simplify, specialise, hnf,

5 Def(..), Accessibility(..),

6 Def(..), Accessibility(..),

6 Context, initContext, ctxtAlist, uconstraints, next_tvar,

7 Context, initContext, ctxtAlist, uconstraints, next_tvar,

7 addToCtxt, setAccess, addCtxtDef, addTyDecl, addDatatype,

8 addToCtxt, setAccess, addCtxtDef, addTyDecl, addDatatype,

@@ -20,7 +21,7 @@ import Core.CaseTree

20type EvalState = ()

21type EvalState = ()

21type Eval a = State EvalState a

22type Eval a = State EvalState a

23−data EvalOpt = Spec | HNF | Simplify

24+data EvalOpt = Spec | HNF | Simplify | AtREPL

24 deriving (Show, Eq)

25 deriving (Show, Eq)

26-- VALUES (as HOAS) ---------------------------------------------------------

27-- VALUES (as HOAS) ---------------------------------------------------------

@@ -60,6 +61,11 @@ normaliseC ctxt env t

60 = evalState (do val <- eval ctxt emptyContext env t []

61 = evalState (do val <- eval ctxt emptyContext env t []

61 quote 0 val) ()

62 quote 0 val) ()

64+normaliseAll :: Context -> Env -> TT Name -> TT Name

65+normaliseAll ctxt env t

66+ = evalState (do val <- eval ctxt emptyContext env t [AtREPL]

67+ quote 0 val) ()

68+

63normalise :: Context -> Env -> TT Name -> TT Name

69normalise :: Context -> Env -> TT Name -> TT Name

64normalise ctxt env t

70normalise ctxt env t

65 = evalState (do val <- eval ctxt emptyContext (map finalEntry env) (finalise t) []

71 = evalState (do val <- eval ctxt emptyContext (map finalEntry env) (finalise t) []

@@ -105,11 +111,12 @@ eval :: Context -> Ctxt [Bool] -> Env -> TT Name -> [EvalOpt] -> Eval Value

105eval ctxt statics genv tm opts = ev True [] tm where

111eval ctxt statics genv tm opts = ev True [] tm where

106 spec = Spec `elem` opts

112 spec = Spec `elem` opts

107 simpl = Simplify `elem` opts

113 simpl = Simplify `elem` opts

114+ atRepl = AtREPL `elem` opts

108

115

109 ev top env (P _ n ty)

116 ev top env (P _ n ty)

110 | Just (Let t v) <- lookup n genv = ev top env v

117 | Just (Let t v) <- lookup n genv = ev top env v

111− ev top env (P Ref n ty) = case lookupDefAcc Nothing n ctxt of

118+ ev top env (P Ref n ty) = case lookupDefAcc Nothing n atRepl ctxt of

112− [(Function _ tm, Public)] -> trace ("Eval " ++ show n) $ ev True env tm

119+ [(Function _ tm, Public)] -> ev True env tm

113 [(TyDecl nt ty, _)] -> do vty <- ev True env ty

120 [(TyDecl nt ty, _)] -> do vty <- ev True env ty

114 return $ VP nt n vty

121 return $ VP nt n vty

115 [(CaseOp inl _ _ [] tree, Public)] ->

122 [(CaseOp inl _ _ [] tree, Public)] ->

@@ -153,7 +160,7 @@ eval ctxt statics genv tm opts = ev True [] tm where

153 apply False env f args

160 apply False env f args

154 | spec = return $ unload env f args

161 | spec = return $ unload env f args

155 apply top env (VP Ref n ty) args

162 apply top env (VP Ref n ty) args

156− | [(CaseOp inl _ _ ns tree, Public)] <- lookupDefAcc Nothing n ctxt

163+ | [(CaseOp inl _ _ ns tree, Public)] <- lookupDefAcc Nothing n atRepl ctxt

157 = -- traceWhen (n == UN ["interp"]) (show (n, args)) $

164 = -- traceWhen (n == UN ["interp"]) (show (n, args)) $

158 if simpl && (not inl) then return $ unload env (VP Ref n ty) args

165 if simpl && (not inl) then return $ unload env (VP Ref n ty) args

159 else do c <- evCase top env ns args tree

166 else do c <- evCase top env ns args tree

@@ -548,8 +555,10 @@ lookupP root n ctxt

548lookupDef :: Maybe [String] -> Name -> Context -> [Def]

555lookupDef :: Maybe [String] -> Name -> Context -> [Def]

549lookupDef root n ctxt = map fst $ lookupCtxt root n (definitions ctxt)

556lookupDef root n ctxt = map fst $ lookupCtxt root n (definitions ctxt)

550

557

551−lookupDefAcc :: Maybe [String] -> Name -> Context -> [(Def, Accessibility)]

558+lookupDefAcc :: Maybe [String] -> Name -> Bool -> Context -> [(Def, Accessibility)]

559+lookupDefAcc root n mkpublic ctxt

552−lookupDefAcc root n ctxt = lookupCtxt root n (definitions ctxt)

560+ = map mkp $ lookupCtxt root n (definitions ctxt)

561+ where mkp (d, a) = if mkpublic then (d, Public) else (d, a)

553

562

554lookupVal :: Maybe [String] -> Name -> Context -> [Value]

563lookupVal :: Maybe [String] -> Name -> Context -> [Value]

555lookupVal root n ctxt

564lookupVal root n ctxt

src/Idris/AbsSyntax.hs+3−1

@@ -50,6 +50,7 @@ data IState = IState { tt_ctxt :: Context,

50 last_proof :: Maybe (Name, [String]),

51 errLine :: Maybe Int,

52 lastParse :: Maybe Name,

53+ hide_list :: [(Name, Maybe Accessibility)],

53 ibc_write :: [IBCWrite]

54 ibc_write :: [IBCWrite]

54 }

55 }

@@ -69,7 +70,8 @@ data IBCWrite = IBCFix FixDecl

69 deriving Show

70 deriving Show

71idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

72idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

73+ "" defaultOpts 6 [] [] [] [] [] [] [] []

72− "" defaultOpts 6 [] [] [] [] [] [] [] [] Nothing Nothing Nothing []

74+ Nothing Nothing Nothing [] []

74-- The monad for the main REPL - reading and processing files and updating

76-- The monad for the main REPL - reading and processing files and updating

75-- global state (hence the IO inner monad).

77-- global state (hence the IO inner monad).

src/Idris/Parser.hs+45−5

@@ -98,6 +98,8 @@ loadSource lidr f

98 iLOG ("Finished " ++ f)

99 let ibc = dropExtension f ++ ".ibc"

100 iucheck

101+ i <- getIState

102+ addHides (hide_list i)

101 ok <- noErrors

103 ok <- noErrors

102 when ok $

104 when ok $

103 idrisCatch (do writeIBC f ibc; clearIBC)

105 idrisCatch (do writeIBC f ibc; clearIBC)

@@ -107,6 +109,18 @@ loadSource lidr f

107 namespaces [] ds = ds

109 namespaces [] ds = ds

108 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]

110 namespaces (x:xs) ds = [PNamespace x (namespaces xs ds)]

109

111

112+addHides :: [(Name, Maybe Accessibility)] -> Idris ()

113+addHides xs = let (hs, as) = partition isNothing xs in

114+ if null as then return ()

115+ else mapM_ doHide

116+ (map (\ (n, _) -> (n, Hidden)) hs ++

117+ map (\ (n, Just a) -> (n, a)) as)

118+ where isNothing (_, Nothing) = True

119+ isNothing _ = False

120+

121+ doHide (n, a) = do setAccessibility n a

122+ addIBC (IBCAccess n a)

123+

110parseExpr i = runParser (pFullExpr defaultSyntax) i "(input)"

124parseExpr i = runParser (pFullExpr defaultSyntax) i "(input)"

111parseTac i = runParser (do t <- pTactic defaultSyntax

125parseTac i = runParser (do t <- pTactic defaultSyntax

112 eof

126 eof

@@ -278,12 +292,14 @@ pSynSym = try (do lchar '['; n <- pName; lchar ']'

278 return (Symbol sym)

292 return (Symbol sym)

279

293

280pFunDecl' :: SyntaxInfo -> IParser PDecl

294pFunDecl' :: SyntaxInfo -> IParser PDecl

295+pFunDecl' syn = try (do acc <- pAccessibility

281−pFunDecl' syn = try (do n_in <- pfName

296+ n_in <- pfName

282 let n = expandNS syn n_in

297 let n = expandNS syn n_in

283 ty <- pTSig syn

298 ty <- pTSig syn

284 fc <- pfc

299 fc <- pfc

285 lchar ';'

300 lchar ';'

286-- ty' <- implicit syn n ty

301-- ty' <- implicit syn n ty

302+ addAcc n acc

287 return (PTy syn fc n ty))

303 return (PTy syn fc n ty))

288 <|> try (pPattern syn)

304 <|> try (pPattern syn)

289

305

@@ -349,7 +365,8 @@ fixity = try (do reserved "infixl"; return Infixl)

349--------- Tyoe classes ---------

365--------- Tyoe classes ---------

350

366

351pClass :: SyntaxInfo -> IParser [PDecl]

367pClass :: SyntaxInfo -> IParser [PDecl]

368+pClass syn = do acc <- pAccessibility

352−pClass syn = do reserved "class"

369+ reserved "class"

353 fc <- pfc

370 fc <- pfc

354 cons <- pConstList syn

371 cons <- pConstList syn

355 n_in <- pName; let n = expandNS syn n_in

372 n_in <- pName; let n = expandNS syn n_in

@@ -357,7 +374,9 @@ pClass syn = do reserved "class"

357 reserved "where"; lchar '{'

374 reserved "where"; lchar '{'

358 ds <- many1 $ pFunDecl syn;

375 ds <- many1 $ pFunDecl syn;

359 lchar '}'

376 lchar '}'

377+ let allDs = concat ds

378+ accData acc n (concatMap declared allDs)

360− return [PClass syn fc cons n cs (concat ds)]

379+ return [PClass syn fc cons n cs allDs]

361 where

380 where

362 carg = do lchar '('; i <- pName; lchar ':'; ty <- pExpr syn; lchar ')'

381 carg = do lchar '('; i <- pName; lchar ':'; ty <- pExpr syn; lchar ')'

363 return (i, ty)

382 return (i, ty)

@@ -465,6 +484,17 @@ pName = do i <- getState

465pfName = try pName

484pfName = try pName

466 <|> do lchar '('; o <- operator; lchar ')'; return (UN o)

485 <|> do lchar '('; o <- operator; lchar ')'; return (UN o)

467

486

487+pAccessibility :: IParser (Maybe Accessibility)

488+pAccessibility

489+ = do reserved "public"; return (Just Public)

490+ <|> do reserved "abstract"; return (Just Frozen)

491+ <|> do reserved "private"; return (Just Hidden)

492+ <|> return Nothing

493+

494+addAcc :: Name -> Maybe Accessibility -> IParser ()

495+addAcc n a = do i <- getState

496+ setState (i { hide_list = (n, a) : hide_list i })

497+

468pSimpleExpr syn =

498pSimpleExpr syn =

469 try (do symbol "!["; t <- pTerm; lchar ']'

499 try (do symbol "!["; t <- pTerm; lchar ']'

470 return $ PQuote t)

500 return $ PQuote t)

@@ -670,16 +700,25 @@ prefix name f = Prefix (do { reservedOp name; fc <- pfc;

670

700

671--------- Data declarations ---------

701--------- Data declarations ---------

672

702

703+-- (works for classes too - 'abstract' means the data/class is visible but members not)

704+accData :: Maybe Accessibility -> Name -> [Name] -> IParser ()

705+accData (Just Frozen) n ns = do addAcc n (Just Frozen)

706+ mapM_ (\n -> addAcc n (Just Hidden)) ns

707+accData a n ns = do addAcc n a; mapM_ (\n -> addAcc n a) ns

708+

673pData :: SyntaxInfo -> IParser PDecl

709pData :: SyntaxInfo -> IParser PDecl

710+pData syn = try (do acc <- pAccessibility

674−pData syn = try (do reserved "data"; fc <- pfc

711+ reserved "data"; fc <- pfc

675 tyn_in <- pfName; ty <- pTSig syn

712 tyn_in <- pfName; ty <- pTSig syn

676 let tyn = expandNS syn tyn_in

713 let tyn = expandNS syn tyn_in

677 reserved "where"

714 reserved "where"

678-- ty' <- implicit syn tyn ty

715-- ty' <- implicit syn tyn ty

679 cons <- sepBy (pConstructor syn) (lchar '|')

716 cons <- sepBy (pConstructor syn) (lchar '|')

680 lchar ';'

717 lchar ';'

718+ accData acc tyn (map (\ (n, _, _) -> n) cons)

681 return $ PData syn fc (PDatadecl tyn ty cons))

719 return $ PData syn fc (PDatadecl tyn ty cons))

720+ <|> do acc <- pAccessibility

682− <|> do reserved "data"; fc <- pfc

721+ reserved "data"; fc <- pfc

683 tyn_in <- pfName; args <- many pName

722 tyn_in <- pfName; args <- many pName

684 let tyn = expandNS syn tyn_in

723 let tyn = expandNS syn tyn_in

685 lchar '='

724 lchar '='

@@ -692,6 +731,7 @@ pData syn = try (do reserved "data"; fc <- pfc

692 do let cty = bindArgs cargs conty

731 do let cty = bindArgs cargs conty

693-- cty' <- implicit syn x cty

732-- cty' <- implicit syn x cty

694 return (x, cty, cfc)) cons

733 return (x, cty, cfc)) cons

734+ accData acc tyn (map (\ (n, _, _) -> n) cons')

695 return $ PData syn fc (PDatadecl tyn ty cons')

735 return $ PData syn fc (PDatadecl tyn ty cons')

696 where

736 where

697 mkPApp fc t [] = t

737 mkPApp fc t [] = t

src/Idris/REPL.hs+2−2

@@ -117,8 +117,8 @@ process Help = iputStrLn displayHelp

117process (Eval t) = do (tm, ty) <- elabVal toplevel False t

118 ctxt <- getContext

119 ist <- get

120− let tm' = normaliseC ctxt [] tm

120+ let tm' = normaliseAll ctxt [] tm

121− let ty' = normaliseC ctxt [] ty

121+ let ty' = normaliseAll ctxt [] ty

122 logLvl 3 $ "Raw: " ++ show (tm', ty')

123 imp <- impShow

124 iputStrLn (showImp imp (delab ist tm') ++ " : " ++