abc2002 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #1623 from edwinb/patvars

Fix for pattern vars in transforms

commitabc20022a6c055544a34e0179a582579f49c4092 authorEdwin Brady <edwin.brady@gmail.com> dateSun 12 Oct 2014, 21:45 (12 years ago) parent2f26892 6e74e33

9 files changed+17−10

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+2−3 src/Idris/Core/Elaborate.hs+2 src/Idris/Elab/Class.hs+2−1 src/Idris/Elab/Clause.hs+3−3 src/Idris/Elab/Instance.hs+2−1 src/Idris/Elab/Type.hs+1 src/Idris/ParseExpr.hs+2−1 src/Idris/Parser.hs+2−1 src/Idris/PartialEval.hs+1

src/Idris/AbsSyntax.hs+2−3

@@ -1068,10 +1068,9 @@ addStatics n tm ptm =

10681068 let stpos = staticList statics' tm

10691069 i <- getIState

10701070 when (not (null statics)) $

1071− logLvl 2 $ "Statics for " ++ show n ++ " " ++ show tm ++ " "

1072− ++ showTmImpls ptm

1071+ logLvl 3 $ "Statics for " ++ show n ++ " " ++ show tm ++ " "

10731072 ++ show statics' ++ "\n" ++ show dynamics

1074− ++ "\n" ++ show stnames ++ "\n" ++ show dnames

1073+ ++ "\n" ++ show stpos

10751074 putIState $ i { idris_statics = addDef n stpos (idris_statics i) }

10761075 addIBC (IBCStatic n)

10771076 where

src/Idris/Core/Elaborate.hs+2

@@ -373,6 +373,7 @@ equiv tm = processTactic' (Equiv tm)

373373

374374-- | Turn the current hole into a pattern variable with the provided name, made unique if MN

375375patvar :: Name -> Elab' aux ()

376+patvar n@(SN _) = do apply (Var n) []; solve

376377patvar n = do env <- get_env

377378 hs <- get_holes

378379 if (n `elem` map fst env) then do apply (Var n) []; solve

@@ -380,6 +381,7 @@ patvar n = do env <- get_env

380381 UN _ -> return $! n

381382 MN _ _ -> unique_hole n

382383 NS _ _ -> return $! n

384+ x -> return $! n

383385 processTactic' (PatVar n')

384386

385387patbind :: Name -> Elab' aux ()

src/Idris/Elab/Class.hs+2−1

@@ -220,7 +220,8 @@ elabClass info syn_in doc fc constraints tn ps pDocs ds

220220

221221 insertConstraint c (PPi p@(Imp _ _ _) n ty sc)

222222 = PPi p n ty (insertConstraint c sc)

223− insertConstraint c sc = PPi constraint (sMN 0 "class") c sc

223+ insertConstraint c sc = PPi (constraint) -- { pstatic = Static })

224+ (sMN 0 "class") c sc

224225

225226 -- make arguments explicit and don't bind class parameters

226227 toExp ns e (PPi (Imp l s p) n ty sc)

src/Idris/Elab/Clause.hs+3−3

@@ -318,7 +318,7 @@ elabPE info fc caller r =

318318 let opts = [Specialise (map (\x -> (x, Nothing)) cgns ++

319319 mapMaybe specName (snd specapp))]

320320 logLvl 3 $ "Specialising application: " ++ show specapp

321− ++ " with " ++ show cgns

321+ ++ " with " ++ show opts

322322 logLvl 3 $ "New name: " ++ show newnm

323323 logLvl 3 $ "PE definition type : " ++ (show specTy)

324324 ++ "\n" ++ show opts

@@ -370,8 +370,8 @@ elabPE info fc caller r =

370370

371371 -- get the clause of a specialised application

372372 getSpecClause ist (n, args)

373− = let newnm = sUN ("PE_"++show (nsroot n) ++ "_" ++

374− qhash 0 (showSep "_" (map showArg args))) in

373+ = let newnm = sUN ("PE_"++ show (nsroot n) ++ "_" ++

374+ qhash 0 (showSep "_" (map showArg args))) in

375375 -- UN (show n ++ show (map snd args)) in

376376 (n, newnm, mkPE_TermDecl ist newnm n args)

377377 where showArg (ExplicitS, n) = show n

src/Idris/Elab/Instance.hs+2−1

@@ -223,7 +223,8 @@ elabInstance info syn what fc cs n ps t expn ds = do

223223

224224 mkTyDecl (n, op, t, _) = PTy emptyDocstring [] syn fc op n t

225225

226− conbind (ty : ns) x = PPi constraint (sMN 0 "class") ty (conbind ns x)

226+ conbind (ty : ns) x = PPi (constraint { pstatic = Dynamic })

227+ (sMN 0 "class") ty (conbind ns x)

227228 conbind [] x = x

228229

229230 coninsert cs (PPi p@(Imp _ _ _) n t sc) = PPi p n t (coninsert cs sc)

src/Idris/Elab/Type.hs+1

@@ -130,6 +130,7 @@ elabType' norm info syn doc argDocs fc opts n ty' = {- let ty' = piBind (params

130130 let nty = cty -- normalise ctxt [] cty

131131 -- if the return type is something coinductive, freeze the definition

132132 ctxt <- getContext

133+ logLvl 2 $ "Rechecked to " ++ show nty

133134 let nty' = normalise ctxt [] nty

134135 logLvl 2 $ "Rechecked to " ++ show nty'

135136

src/Idris/ParseExpr.hs+2−1

@@ -721,7 +721,8 @@ TypeExpr ::= ConstraintList? Expr;

721721typeExpr :: SyntaxInfo -> IdrisParser PTerm

722722typeExpr syn = do cs <- if implicitAllowed syn then constraintList syn else return []

723723 sc <- expr syn

724− return (bindList (PPi constraint) (map (\x -> (sMN 0 "constrarg", x)) cs) sc)

724+ return (bindList (PPi constraint)

725+ (map (\x -> (sMN 0 "constrarg", x)) cs) sc)

725726 <?> "type signature"

726727

727728{- | Parses a lambda expression

src/Idris/Parser.hs+2−1

@@ -639,7 +639,8 @@ instance_ syn = do reserved "instance"; fc <- getFC

639639 cn <- fnName

640640 args <- many (simpleExpr syn)

641641 let sc = PApp fc (PRef fc cn) (map pexp args)

642− let t = bindList (PPi constraint) (map (\x -> (sMN 0 "constraint", x)) cs) sc

642+ let t = bindList (PPi constraint)

643+ (map (\x -> (sMN 0 "constraint", x)) cs) sc

643644 ds <- option [] (instanceBlock syn)

644645 return [PInstance syn fc cs cn args t en ds]

645646 <?> "instance declaration"

src/Idris/PartialEval.hs+1

@@ -163,6 +163,7 @@ getSpecApps ist env tm = ga env (explicitNames tm) where

163163 lookupCtxt n (idris_implicits ist)) of

164164 ([statics], [imps]) ->

165165 if (length statics == length args && or statics) then

166+-- trace (show (n, statics, imps, args)) $

166167 case buildApp env statics imps args [0..] of

167168 args -> [(n, args)]

168169-- _ -> []