68194ce · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix export of record fields

68194ceEdwin Brady15 years ago

lib/Makefile+1

compare with master

unifiedsplit

@@ -15,6 +15,7 @@ clean: .PHONY

15 rm -f *.ibc

16 rm -f prelude/*.ibc

17 rm -f network/*.ibc

18+ rm -f control/monad/*.ibc

19linecount: .PHONY

20linecount: .PHONY

20 wc -l *.idr network/*.idr prelude/*.idr

21 wc -l *.idr network/*.idr prelude/*.idr

lib/checkall.idr+1

@@ -23,3 +23,4 @@ import prelude.char

24import network.cgi

26+import control.monad.identity

lib/control/monad/identity.idrnew file+10

@@ -0,0 +1,10 @@

1+module control.monad.identity

3+import prelude.monad

5+public record Identity : Set -> Set where

6+ Id : (runIdentity : a) -> Identity a

8+instance Monad Identity where

9+ return x = Id x

10+ (Id x) >>= k = k x

src/Idris/ElabDecls.hs+2−2

@@ -86,7 +86,7 @@ elabData info syn fc (PDatadecl n t_in dcons)

87elabRecord :: ElabInfo -> SyntaxInfo -> FC -> Name ->

88 PTerm -> Name -> PTerm -> Idris ()

89−elabRecord info syn_in fc tyn ty cn cty

89+elabRecord info syn fc tyn ty cn cty

90 = do elabData info syn fc (PDatadecl tyn ty [(cn, cty, fc)])

91 cty <- implicit syn cn cty

92 i <- get

@@ -106,7 +106,7 @@ elabRecord info syn_in fc tyn ty cn cty

106 update_decls <- mapM (mkUpdate recty (length nonImp)) (zip nonImp [0..])

107 mapM_ (elabDecl info) (concat (proj_decls ++ update_decls))

108 where

109− syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }

109+-- syn = syn_in { syn_namespace = show (nsroot tyn) : syn_namespace syn_in }

110

111 isNonImp (PExp _ _ _, a) = Just a

112 isNonImp _ = Nothing

src/Idris/Parser.hs+28−16

@@ -109,6 +109,7 @@ loadSource lidr f

109 when ok $

110 idrisCatch (do writeIBC f ibc; clearIBC)

111 (\c -> return ()) -- failure is harmless

112+ i <- getIState

112 putIState (i { hide_list = [] })

113 putIState (i { hide_list = [] })

113 return ()

114 return ()

114 where

115 where

@@ -775,9 +776,9 @@ pRecordSet syn

775 applyAll fc ((n, e) : es) x

776 applyAll fc ((n, e) : es) x

776 = applyAll fc es (PApp fc (PRef fc (mkSet n)) [pexp e, pexp x])

777 = applyAll fc es (PApp fc (PRef fc (mkSet n)) [pexp e, pexp x])

777

778

778− mkSet (UN n) = UN ("set_" ++ n)

779+mkSet (UN n) = UN ("set_" ++ n)

779− mkSet (MN 0 n) = MN 0 ("set_" ++ n)

780+mkSet (MN 0 n) = MN 0 ("set_" ++ n)

780− mkSet (NS n s) = NS (mkSet n) s

781+mkSet (NS n s) = NS (mkSet n) s

781

782

782pTSig syn = do lchar ':'

783pTSig syn = do lchar ':'

783 cs <- pConstList syn

784 cs <- pConstList syn

@@ -958,19 +959,30 @@ accData (Just Frozen) n ns = do addAcc n (Just Frozen)

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

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

959

960

960pRecord :: SyntaxInfo -> IParser PDecl

961pRecord :: SyntaxInfo -> IParser PDecl

961−pRecord syn = try (do acc <- pAccessibility

962+pRecord syn = do acc <- pAccessibility

962− reserved "record"; fc <- pfc

963+ reserved "record"; fc <- pfc

963− tyn_in <- pfName; ty <- pTSig syn

964+ tyn_in <- pfName; ty <- pTSig syn

964− let tyn = expandNS syn tyn_in

965+ let tyn = expandNS syn tyn_in

965− reserved "where"

966+ reserved "where"

966− open_block

967+ open_block

967− push_indent

968+ push_indent

968− (cn, cty, _) <- pConstructor syn

969+ (cn, cty, _) <- pConstructor syn

969− pKeepTerminator

970+ pKeepTerminator

970− pop_indent

971+ pop_indent

971− close_block

972+ close_block

972− accData acc tyn [cn]

973+ accData acc tyn [cn]

974+ let rsyn = syn { syn_namespace = show (nsroot tyn) :

975+ syn_namespace syn }

976+ let fns = getRecNames rsyn cty

977+ mapM_ (\n -> addAcc n (toFreeze acc)) fns

973− return $ PRecord syn fc tyn ty cn cty)

978+ return $ PRecord rsyn fc tyn ty cn cty

979+ where

980+ getRecNames syn (PPi _ n _ sc) = [expandNS syn n, expandNS syn (mkSet n)]

981+ ++ getRecNames syn sc

982+ getRecNames _ _ = []

983+

984+ toFreeze (Just Frozen) = Just Hidden

985+ toFreeze x = x

974

986

975pData :: SyntaxInfo -> IParser PDecl

987pData :: SyntaxInfo -> IParser PDecl

976pData syn = try (do acc <- pAccessibility

988pData syn = try (do acc <- pAccessibility