f0bf615 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #2227 from melted/snappy_load

f0bf615Niklas Larsson11 years ago

src/Idris/IBC.hs+22−45

compare with master

unifiedsplit

@@ -443,33 +443,22 @@ pInstances :: [(Bool, Name, Name)] -> Idris ()

443pInstances cs = mapM_ (\ (i, n, ins) -> addInstance i n ins) cs

444

445pDSLs :: [(Name, DSL)] -> Idris ()

446−pDSLs cs = mapM_ (\ (n, c) ->

446+pDSLs cs = mapM_ (\ (n, c) -> updateIState (\i ->

447− do i <- getIState

448− putIState (i { idris_dsls

449− = addDef n c (idris_dsls i) }))

447+ i { idris_dsls = addDef n c (idris_dsls i) })) cs

450− cs

451

448

452pDatatypes :: [(Name, TypeInfo)] -> Idris ()

449pDatatypes :: [(Name, TypeInfo)] -> Idris ()

453−pDatatypes cs = mapM_ (\ (n, c) ->

450+pDatatypes cs = mapM_ (\ (n, c) -> updateIState (\i ->

454− do i <- getIState

455− putIState (i { idris_datatypes

456− = addDef n c (idris_datatypes i) }))

451+ i { idris_datatypes = addDef n c (idris_datatypes i) })) cs

457− cs

458

452

459pOptimise :: [(Name, OptInfo)] -> Idris ()

453pOptimise :: [(Name, OptInfo)] -> Idris ()

460−pOptimise cs = mapM_ (\ (n, c) ->

454+pOptimise cs = mapM_ (\ (n, c) -> updateIState (\i ->

461− do i <- getIState

462− putIState (i { idris_optimisation

463− = addDef n c (idris_optimisation i) }))

455+ i { idris_optimisation = addDef n c (idris_optimisation i) })) cs

464− cs

465

456

466pSyntax :: [Syntax] -> Idris ()

457pSyntax :: [Syntax] -> Idris ()

467−pSyntax s = do i <- getIState

468− putIState (i { syntax_rules = updateSyntaxRules s (syntax_rules i) })

458+pSyntax s = updateIState (\i -> i { syntax_rules = updateSyntaxRules s (syntax_rules i) })

469

459

470pKeywords :: [String] -> Idris ()

460pKeywords :: [String] -> Idris ()

471−pKeywords k = do i <- getIState

472− putIState (i { syntax_keywords = k ++ syntax_keywords i })

461+pKeywords k = updateIState (\i -> i { syntax_keywords = k ++ syntax_keywords i })

473

462

474pObjs :: [(Codegen, FilePath)] -> Idris ()

463pObjs :: [(Codegen, FilePath)] -> Idris ()

475pObjs os = mapM_ (\ (cg, obj) -> do dirs <- allImportDirs

464pObjs os = mapM_ (\ (cg, obj) -> do dirs <- allImportDirs

@@ -493,11 +482,8 @@ pHdrs :: [(Codegen, String)] -> Idris ()

493pHdrs hs = mapM_ (uncurry addHdr) hs

482pHdrs hs = mapM_ (uncurry addHdr) hs

494

483

495pPatdefs :: [(Name, ([([Name], Term, Term)], [PTerm]))] -> Idris ()

484pPatdefs :: [(Name, ([([Name], Term, Term)], [PTerm]))] -> Idris ()

496−pPatdefs ds

485+pPatdefs ds = mapM_ (\ (n, d) -> updateIState (\i ->

497− = mapM_ (\ (n, d) ->

498− do i <- getIState

499− putIState (i { idris_patdefs = addDef n (force d) (idris_patdefs i) }))

486+ i { idris_patdefs = addDef n (force d) (idris_patdefs i) })) ds

500− ds

501

487

502pDefs :: Bool -> [Name] -> [(Name, Def)] -> Idris ()

488pDefs :: Bool -> [Name] -> [(Name, Def)] -> Idris ()

503pDefs reexp syms ds

489pDefs reexp syms ds

@@ -507,9 +493,8 @@ pDefs reexp syms ds

507 TyDecl _ _ -> return ()

493 TyDecl _ _ -> return ()

508 _ -> do iLOG $ "SOLVING " ++ show n

494 _ -> do iLOG $ "SOLVING " ++ show n

509 solveDeferred n

495 solveDeferred n

510− i <- getIState

496+ updateIState (\i -> i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })

511-- logLvl 1 $ "Added " ++ show (n, d')

497-- logLvl 1 $ "Added " ++ show (n, d')

512− putIState (i { tt_ctxt = addCtxtDef n d' (tt_ctxt i) })

513 if (not reexp) then do iLOG $ "Not exporting " ++ show n

498 if (not reexp) then do iLOG $ "Not exporting " ++ show n

514 setAccessibility n Hidden

499 setAccessibility n Hidden

515 else iLOG $ "Exporting " ++ show n) ds

500 else iLOG $ "Exporting " ++ show n) ds

@@ -569,9 +554,8 @@ pDocs :: [(Name, (Docstring D.DocTerm, [(Name, Docstring D.DocTerm)]))] -> Idris

569pDocs ds = mapM_ (\(n, a) -> addDocStr n (fst a) (snd a)) ds

554pDocs ds = mapM_ (\(n, a) -> addDocStr n (fst a) (snd a)) ds

570

555

571pMDocs :: [(Name, Docstring D.DocTerm)] -> Idris ()

556pMDocs :: [(Name, Docstring D.DocTerm)] -> Idris ()

572−pMDocs ds = mapM_ addMDocStr ds

557+pMDocs ds = mapM_ (\ (n, d) -> updateIState (\i ->

573− where addMDocStr (n, d) = do ist <- getIState

574− putIState ist { idris_moduledocs = addDef n d (idris_moduledocs ist) }

558+ i { idris_moduledocs = addDef n d (idris_moduledocs i) })) ds

575

559

576pAccess :: Bool -- ^ Reexporting?

560pAccess :: Bool -- ^ Reexporting?

577 -> [(Name, Accessibility)] -> Idris ()

561 -> [(Name, Accessibility)] -> Idris ()

@@ -579,8 +563,7 @@ pAccess reexp ds

579 = mapM_ (\ (n, a_in) ->

563 = mapM_ (\ (n, a_in) ->

580 do let a = if reexp then a_in else Hidden

564 do let a = if reexp then a_in else Hidden

581 logLvl 3 $ "Setting " ++ show (a, n) ++ " to " ++ show a

565 logLvl 3 $ "Setting " ++ show (a, n) ++ " to " ++ show a

582− updateIState (\i -> i { tt_ctxt = setAccess n a (tt_ctxt i) }))

566+ updateIState (\i -> i { tt_ctxt = setAccess n a (tt_ctxt i) })) ds

583− ds

584

567

585pFlags :: [(Name, [FnOpt])] -> Idris ()

568pFlags :: [(Name, [FnOpt])] -> Idris ()

586pFlags ds = mapM_ (\ (n, a) -> setFlags n a) ds

569pFlags ds = mapM_ (\ (n, a) -> setFlags n a) ds

@@ -592,8 +575,7 @@ pTotal :: [(Name, Totality)] -> Idris ()

592pTotal ds = mapM_ (\ (n, a) -> updateIState (\i -> i { tt_ctxt = setTotal n a (tt_ctxt i) })) ds

575pTotal ds = mapM_ (\ (n, a) -> updateIState (\i -> i { tt_ctxt = setTotal n a (tt_ctxt i) })) ds

593

576

594pTotCheckErr :: [(FC, String)] -> Idris ()

577pTotCheckErr :: [(FC, String)] -> Idris ()

595−pTotCheckErr es = do ist <- getIState

596− putIState ist { idris_totcheckfail = idris_totcheckfail ist ++ es }

578+pTotCheckErr es = updateIState (\i -> i { idris_totcheckfail = idris_totcheckfail i ++ es })

597

579

598pCG :: [(Name, CGInfo)] -> Idris ()

580pCG :: [(Name, CGInfo)] -> Idris ()

599pCG ds = mapM_ (\ (n, a) -> addToCG n a) ds

581pCG ds = mapM_ (\ (n, a) -> addToCG n a) ds

@@ -614,24 +596,19 @@ pNameHints :: [(Name, Name)] -> Idris ()

614pNameHints ns = mapM_ (\ (n, ty) -> addNameHint n ty) ns

596pNameHints ns = mapM_ (\ (n, ty) -> addNameHint n ty) ns

615

597

616pMetaInformation :: [(Name, MetaInformation)] -> Idris ()

598pMetaInformation :: [(Name, MetaInformation)] -> Idris ()

617−pMetaInformation ds = mapM_ (\ (n, m) ->

599+pMetaInformation ds = mapM_ (\ (n, m) -> updateIState (\i ->

618− do i <- getIState

619− putIState (i { tt_ctxt = setMetaInformation n m (tt_ctxt i) }))

600+ i { tt_ctxt = setMetaInformation n m (tt_ctxt i) })) ds

620− ds

621

601

622pErrorHandlers :: [Name] -> Idris ()

602pErrorHandlers :: [Name] -> Idris ()

623−pErrorHandlers ns = do i <- getIState

603+pErrorHandlers ns = updateIState (\i ->

624− putIState $ i { idris_errorhandlers = idris_errorhandlers i ++ ns }

604+ i { idris_errorhandlers = idris_errorhandlers i ++ ns })

625

605

626pFunctionErrorHandlers :: [(Name, Name, Name)] -> Idris ()

606pFunctionErrorHandlers :: [(Name, Name, Name)] -> Idris ()

627−pFunctionErrorHandlers [] = return ()

607+pFunctionErrorHandlers ns = mapM_ (\ (fn,arg,handler) ->

628−pFunctionErrorHandlers ((fn, arg, handler):ns) = do addFunctionErrorHandlers fn arg [handler]

608+ addFunctionErrorHandlers fn arg [handler]) ns

629− pFunctionErrorHandlers ns

630

609

631pMetavars :: [(Name, (Maybe Name, Int, Bool))] -> Idris ()

610pMetavars :: [(Name, (Maybe Name, Int, Bool))] -> Idris ()

632−pMetavars ns = do i <- getIState

633− putIState $ i { idris_metavars = L.reverse ns

611+pMetavars ns = updateIState (\i -> i { idris_metavars = L.reverse ns ++ idris_metavars i })

634− ++ idris_metavars i }

635

612

636----- For Cheapskate and docstrings

613----- For Cheapskate and docstrings

637

614