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

record { a->b->c = val } x Returns a new record, with the field accessed by c (b (a x)) updated to have the new value 'val'

commit1df6fa9d7ceb444c4a820244e78b24d4f8505c4f authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 2 May 2014, 00:34 (12 years ago) parent9b1b1f1
2 files changed+14−6
compare with master
unifiedsplit
src/Idris/ParseExpr.hs+12−5 src/Idris/REPL.hs+2−1
src/Idris/ParseExpr.hs+12−5
@@ -618,16 +618,23 @@ recordType syn
618618 (applyAll fc fields (PRef fc (sMN 0 "fldx"))))
619619 Just v -> return (applyAll fc fields v)
620620 <?> "record setting expression"
621− where fieldType :: IdrisParser (Name, PTerm)
622− fieldType = do n <- fnName
621+ where fieldType :: IdrisParser ([Name], PTerm)
622+ fieldType = do n <- sepBy1 fnName (symbol "->")
623623 lchar '='
624624 e <- expr syn
625625 return (n, e)
626626 <?> "field setter"
627− applyAll :: FC -> [(Name, PTerm)] -> PTerm -> PTerm
627+ applyAll :: FC -> [([Name], PTerm)] -> PTerm -> PTerm
628628 applyAll fc [] x = x
629− applyAll fc ((n, e) : es) x
630− = applyAll fc es (PApp fc (PRef fc (mkType n)) [pexp e, pexp x])
629+ applyAll fc ((ns, e) : es) x
630+ = applyAll fc es (doUpdate fc ns e x)
631+
632+ doUpdate fc [n] e get
633+ = PApp fc (PRef fc (mkType n)) [pexp e, pexp get]
634+ doUpdate fc (n : ns) e get
635+ = PApp fc (PRef fc (mkType n))
636+ [pexp (doUpdate fc ns e (PApp fc (PRef fc n) [pexp get])),
637+ pexp get]
631638
632639-- | Creates setters for record types on necessary functions
633640mkType :: Name -> Name
src/Idris/REPL.hs+2−1
@@ -552,7 +552,8 @@ process h fn (ChangeDirectory f)
552552 = do runIO $ setCurrentDirectory f
553553 return ()
554554process h fn (Eval t)
555− = withErrorReflection $ do (tm, ty) <- elabVal toplevel False t
555+ = withErrorReflection $ do logLvl 5 $ show t
556+ (tm, ty) <- elabVal toplevel False t
556557 ctxt <- getContext
557558 let tm' = force (normaliseAll ctxt [] tm)
558559 let ty' = force (normaliseAll ctxt [] ty)