05a46f2 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Generate better record update functions

Specifically, make sure that the type respects any updates in parameters, and leave parameter positions implicit so that the elaborator can infer them (which is much easier than doing the hard work in the setter itself...)

commit05a46f2328968162d7b2b654c5564c2cfc08a638 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 1 May 2014, 21:27 (12 years ago) parent555d58f

5 files changed+37−8

compare with master

unifiedsplit

idris.cabal+3 src/Idris/ElabDecls.hs+17−8 test/record002/expected+2 test/record002/record002.idr+11 test/record002/run+4

idris.cabal+3

@@ -407,6 +407,9 @@ Extra-source-files:

407407 test/records001/run

408408 test/records001/*.idr

409409 test/records001/expected

410+ test/records002/run

411+ test/records002/*.idr

412+ test/records002/expected

410413

411414 test/sugar001/run

412415 test/sugar001/*.idr

src/Idris/ElabDecls.hs+17−8

@@ -792,16 +792,14 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty

792792 let index_names_in = getRecNameMap "_in" recty

793793 let recty_in = substMatches index_names_in recty

794794

795− let index_names_out = getRecNameMap "'" recty

796− let recty_out = substMatches index_names_out recty

797−

798795 logLvl 1 $ show (recty, ptys)

799796 let substs = map (\ (n, _) -> (n, PApp fc (PRef fc n)

800797 [pexp (PRef fc rec)])) ptys

801798 proj_decls <- mapM (mkProj recty_in substs cimp) (zip ptys [0..])

802799 let nonImp = mapMaybe isNonImp (zip cimp ptys_u)

803800 let implBinds = getImplB id cty'

804− update_decls <- mapM (mkUpdate recty

801+ update_decls <- mapM (mkUpdate recty index_names_in

802+ (getFieldNames cty')

805803 implBinds (length nonImp)) (zip nonImp [0..])

806804 mapM_ (elabDecl EAll info) (concat proj_decls)

807805 logLvl 1 $ show update_decls

@@ -838,6 +836,10 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty

838836 getProjs acc (PPi _ n ty s) = getProjs ((n, ty) : acc) s

839837 getProjs acc r = reverse acc

840838

839+ getFieldNames (PPi (Exp _ _ _) n _ s) = n : getFieldNames s

840+ getFieldNames (PPi _ _ _ s) = getFieldNames s

841+ getFieldNames _ = []

842+

841843 getRecTy (PPi _ n ty s) = getRecTy s

842844 getRecTy t = t

843845

@@ -882,13 +884,20 @@ elabRecord info syn doc fc tyn ty opts cdoc cn cty

882884 -- If the 'pty' we're updating includes anything in 'substs', we're

883885 -- updating the type as well, so use recty', otherwise just use

884886 -- recty

885− mkUpdate recty k num ((pn, pty), pos)

887+ mkUpdate recty inames fnames k num ((pn, pty), pos)

886888 = do let setname = expandNS syn $ mkType pn

887889 let valname = sMN 0 "updateval"

888− let pt = k (PPi expl pn pty

889− (PPi expl rec recty recty))

890+ let pn_out = sMN 0 (show pn ++ "_out")

891+ let pn_in = sMN 0 (show pn ++ "_in")

892+ let recty_in = substMatches [(pn, PRef fc pn_in)] recty

893+ let recty_out = substMatches [(pn, PRef fc pn_out)] recty

894+ let pt = substMatches inames $

895+ k (PPi expl pn_out pty

896+ (PPi expl rec recty_in recty_out))

890897 let pfnTy = PTy emptyDocstring [] defaultSyntax fc [] setname pt

891− let pls = map (\x -> PRef fc (sMN x ("field" ++ show x))) [0..num-1]

898+-- let pls = map (\x -> PRef fc (sMN x ("field" ++ show x))) [0..num-1]

899+ let inames_imp = map (\ (x,_) -> (x, Placeholder)) inames

900+ let pls = map (\x -> substMatches inames_imp (PRef fc x)) fnames

892901 let lhsArgs = pls

893902 let rhsArgs = take pos pls ++ (PRef fc valname) :

894903 drop (pos + 1) pls

test/record002/expectednew file+2

@@ -0,0 +1,2 @@

1+42, 20

2+10, 42

test/record002/record002.idrnew file+11

@@ -0,0 +1,11 @@

2+record Foo : Nat -> Type where

3+ MkFoo : (param : Nat) -> (num : Int) -> Foo param

5+instance Show (Foo n) where

6+ show f = show (param f) ++ ", " ++ show (num f)

8+main : IO ()

9+main = do let x = MkFoo 10 20

10+ putStrLn (show (record { param = 42 } x))

11+ putStrLn (show (record { num = 42 } x))

test/record002/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+idris $@ record002.idr -o record002

3+./record002

4+rm -f record002 *.ibc