abc2002 · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+2−3

compare with master

unifiedsplit

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

1068 let stpos = staticList statics' tm

1069 i <- getIState

1070 when (not (null statics)) $

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

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

1072− ++ showTmImpls ptm

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

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

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

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

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

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

1076 addIBC (IBCStatic n)

1075 addIBC (IBCStatic n)

1077 where

1076 where

src/Idris/Core/Elaborate.hs+2

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

373

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

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

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

376patvar n = do env <- get_env

377patvar n = do env <- get_env

377 hs <- get_holes

378 hs <- get_holes

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

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

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

380 UN _ -> return $! n

381 UN _ -> return $! n

381 MN _ _ -> unique_hole n

382 MN _ _ -> unique_hole n

382 NS _ _ -> return $! n

383 NS _ _ -> return $! n

384+ x -> return $! n

383 processTactic' (PatVar n')

385 processTactic' (PatVar n')

384

386

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

387patbind :: 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

220

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

222 = 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

224

225

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

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

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

227 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 =

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

319 mapMaybe specName (snd specapp))]

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

321− ++ " with " ++ show cgns

321+ ++ " with " ++ show opts

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

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

324 ++ "\n" ++ show opts

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

370

371 -- get the clause of a specialised application

372 getSpecClause ist (n, args)

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

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

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

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

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

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

377 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

223

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

225

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

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

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

227 conbind [] x = x

228 conbind [] x = x

228

229

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

230 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

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

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

132 ctxt <- getContext

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

133 let nty' = normalise ctxt [] nty

134 let nty' = normalise ctxt [] nty

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

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

135

136

src/Idris/ParseExpr.hs+2−1

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

721typeExpr :: SyntaxInfo -> IdrisParser PTerm

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

723 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)

725 <?> "type signature"

726 <?> "type signature"

726

727

727{- | Parses a lambda expression

728{- | Parses a lambda expression

src/Idris/Parser.hs+2−1

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

639 cn <- fnName

640 args <- many (simpleExpr syn)

641 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

643 ds <- option [] (instanceBlock syn)

644 ds <- option [] (instanceBlock syn)

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

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

645 <?> "instance declaration"

646 <?> "instance declaration"

src/Idris/PartialEval.hs+1

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

163 lookupCtxt n (idris_implicits ist)) of

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

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

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

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

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

167 args -> [(n, args)]

168 args -> [(n, args)]

168-- _ -> []

169-- _ -> []