c37de47 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Propagate parameters to records

Also a minor change in propagating parameters to data, for consistency. Parameters become *implicit* arguments to constuctors (they are already in the type after all).

commitc37de4788a5233c8b5d3b6af4efe87e3df4569d7 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 28 Feb 2014, 18:02 (13 years ago) parent87e9604

3 files changed+11−2

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+8−1 src/Idris/Completion.hs+1−1 src/Idris/ParseExpr.hs+2

src/Idris/AbsSyntax.hs+8−1

@@ -1061,7 +1061,14 @@ expandParamsD rhs ist dec ps ns (PData doc syn fc co pd)

10611061 (map econ cons)

10621062 else PDatadecl n (expandParams dec ps ns [] ty) (map econ cons)

10631063 econ (doc, n, t, fc, fs)

1064− = (doc, dec n, piBindp expl ps (expandParams dec ps ns [] t), fc, fs)

1064+ = (doc, dec n, piBindp impl ps (expandParams dec ps ns [] t), fc, fs)

1065+expandParamsD rhs ist dec ps ns (PRecord doc syn fc tn tty cdoc cn cty)

1066+ = if tn `elem` ns

1067+ then PRecord doc syn fc (dec tn) (piBind ps (expandParams dec ps ns [] tty))

1068+ cdoc (dec cn) conty

1069+ else PRecord doc syn fc (dec tn) (expandParams dec ps ns [] tty)

1070+ cdoc (dec cn) conty

1071+ where conty = piBindp impl ps (expandParams dec ps ns [] cty)

10651072expandParamsD rhs ist dec ps ns (PParams f params pds)

10661073 = PParams f (ps ++ map (mapsnd (expandParams dec ps ns [])) params)

10671074 (map (expandParamsD True ist dec ps ns) pds)

src/Idris/Completion.hs+1−1

@@ -50,7 +50,7 @@ tacticArgs = [ ("intro", Nothing) -- FIXME syntax for intro (fresh name)

5050 , (":e", Just ExprTArg)

5151 , (":eval", Just ExprTArg)

5252 ] ++ map (\x -> (x, Nothing)) [

53− "intros", "compute", "trivial", "solve", "attack",

53+ "intros", "compute", "trivial", "search", "solve", "attack",

5454 "state", "term", "undo", "qed", "abandon", ":q"

5555 ]

5656tactics = map fst tacticArgs

src/Idris/ParseExpr.hs+2

@@ -1165,6 +1165,8 @@ tactic syn = do reserved "intro"; ns <- sepBy (indentPropHolds gtProp *> name) (

11651165 return $ TSeq t (mergeSeq ts)

11661166 <|> do reserved "compute"; return Compute

11671167 <|> do reserved "trivial"; return Trivial

1168+ <|> do reserved "search"; n <- (indentPropHolds gtProp *> fnName)

1169+ return (ProofSearch Nothing n [])

11681170 <|> do reserved "instance"; return TCInstance

11691171 <|> do reserved "solve"; return Solve

11701172 <|> do reserved "attack"; return Attack