git.iko.soy/Idris-dev
on master help sign in
Changed record update syntax...

...since {} is too overloaded now record { field = val } rec Also put records in their own namespace

commit02501efae72c9b3c651335119aa1066474904ace authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 27 Jan 2012, 15:32 (15 years ago) parent4cd20b3
4 files changed+19−14
compare with master
unifiedsplit
lib/network/cgi.idr+2−2 src/Idris/AbsSyntax.hs+7 src/Idris/ElabDecls.hs+6−4 src/Idris/Parser.hs+4−8
lib/network/cgi.idr+2−2
@@ -15,10 +15,10 @@ record CGIInfo : Set where
1515 (Output : String) -> CGIInfo
1616
1717add_Headers : String -> CGIInfo -> CGIInfo
18−add_Headers str st = { Headers = Headers st ++ str } st
18+add_Headers str st = record { Headers = Headers st ++ str } st
1919
2020add_Output : String -> CGIInfo -> CGIInfo
21−add_Output str st = { Output = Output st ++ str } st
21+add_Output str st = record { Output = Output st ++ str } st
2222
2323abstract
2424data CGI : Set -> Set where
src/Idris/AbsSyntax.hs+7
@@ -652,6 +652,13 @@ data SyntaxInfo = Syn { using :: [(Name, PTerm)],
652652
653653defaultSyntax = Syn [] [] [] [] id False initDSL
654654
655+expandNS :: SyntaxInfo -> Name -> Name
656+expandNS syn n@(NS _ _) = n
657+expandNS syn n = case syn_namespace syn of
658+ [] -> n
659+ xs -> NS n xs
660+
661+
655662--- Pretty printing declarations and terms
656663
657664instance Show PTerm where
src/Idris/ElabDecls.hs+6−4
@@ -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 fc tyn ty cn cty
89+elabRecord info syn_in 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,6 +106,7 @@ elabRecord info syn 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 }
109110
110111 isNonImp (PExp _ _ _, a) = Just a
111112 isNonImp _ = Nothing
@@ -135,8 +136,9 @@ elabRecord info syn fc tyn ty cn cty
135136 mkSet (MN 0 n) = MN 0 ("set_" ++ n)
136137 mkSet (NS n s) = NS (mkSet n) s
137138
138− mkProj recty substs cimp ((pn, pty), pos)
139− = do let pfnTy = PTy defaultSyntax fc [] pn
139+ mkProj recty substs cimp ((pn_in, pty), pos)
140+ = do let pn = expandNS syn pn_in
141+ let pfnTy = PTy defaultSyntax fc [] pn
140142 (PPi expl rec recty
141143 (substMatches substs pty))
142144 let pls = repeat Placeholder
@@ -153,7 +155,7 @@ elabRecord info syn fc tyn ty cn cty
153155 implicitise (pa, t) = pa { getTm = t }
154156
155157 mkUpdate recty num ((pn, pty), pos)
156− = do let setname = mkSet pn
158+ = do let setname = expandNS syn $ mkSet pn
157159 let valname = MN 0 "updateval"
158160 let pfnTy = PTy defaultSyntax fc [] setname
159161 (PPi expl pn pty
src/Idris/Parser.hs+4−8
@@ -444,12 +444,6 @@ pNamespace syn =
444444 close_block
445445 return [PNamespace n (concat ds)]
446446
447−expandNS :: SyntaxInfo -> Name -> Name
448−expandNS syn n@(NS _ _) = n
449−expandNS syn n = case syn_namespace syn of
450− [] -> n
451− xs -> NS n xs
452−
453447--------- Fixity ---------
454448
455449pFixity :: IParser PDecl
@@ -763,7 +757,8 @@ pConstraintArg syn = do symbol "@{"; e <- pExpr syn; symbol "}"
763757 return (pconst e)
764758
765759pRecordSet syn
766− = do lchar '{'
760+ = do reserved "record"
761+ lchar '{'
767762 fields <- sepBy1 pFieldSet (lchar ',')
768763 lchar '}'
769764 fc <- pfc
@@ -1017,12 +1012,13 @@ bindArgs [] t = t
10171012bindArgs (x:xs) t = PPi expl (MN 0 "t") x (bindArgs xs t)
10181013
10191014pConstructor :: SyntaxInfo -> IParser (Name, PTerm, FC)
1020−pConstructor syn
1015+pConstructor syn
10211016 = do cn_in <- pfName; fc <- pfc
10221017 let cn = expandNS syn cn_in
10231018 ty <- pTSig syn
10241019-- ty' <- implicit syn cn ty
10251020 return (cn, ty, fc)
1021+
10261022
10271023pSimpleCon :: SyntaxInfo -> IParser (Name, [PTerm], FC)
10281024pSimpleCon syn