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

git.iko.soy/Idris-dev

Fix export of record fields

commit68194cea1c6d01595f0939339f9d47e79c0ec897 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateSat 28 Jan 2012, 21:57 (15 years ago) parent88de6d0

5 files changed+42−18

compare with master

unifiedsplit

lib/Makefile+1 lib/checkall.idr+1 lib/control/monad/identity.idr+10 src/Idris/ElabDecls.hs+2−2 src/Idris/Parser.hs+28−16

lib/Makefile+1

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

1515 rm -f *.ibc

1616 rm -f prelude/*.ibc

1717 rm -f network/*.ibc

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

1819

1920linecount: .PHONY

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

lib/checkall.idr+1

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

2323

2424import network.cgi

2525

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)

8686

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

8888 PTerm -> Name -> PTerm -> Idris ()

89−elabRecord info syn_in fc tyn ty cn cty

89+elabRecord info syn fc tyn ty cn cty

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

9191 cty <- implicit syn cn cty

9292 i <- get

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

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

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

108108 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 }

110110

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

112112 isNonImp _ = Nothing

src/Idris/Parser.hs+28−16

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

109109 when ok $

110110 idrisCatch (do writeIBC f ibc; clearIBC)

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

112+ i <- getIState

112113 putIState (i { hide_list = [] })

113114 return ()

114115 where

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

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

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

777778

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

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

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

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

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

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

781782

782783pTSig syn = do lchar ':'

783784 cs <- pConstList syn

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

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

959960

960961pRecord :: SyntaxInfo -> IParser PDecl

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

962− reserved "record"; fc <- pfc

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

964− let tyn = expandNS syn tyn_in

965− reserved "where"

966− open_block

967− push_indent

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

969− pKeepTerminator

970− pop_indent

971− close_block

972− accData acc tyn [cn]

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

962+pRecord syn = do acc <- pAccessibility

963+ reserved "record"; fc <- pfc

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

965+ let tyn = expandNS syn tyn_in

966+ reserved "where"

967+ open_block

968+ push_indent

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

970+ pKeepTerminator

971+ pop_indent

972+ close_block

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

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

974986

975987pData :: SyntaxInfo -> IParser PDecl

976988pData syn = try (do acc <- pAccessibility