1a79f2b · Idris-dev · git.iko.soy

src/Idris/Core/DeepSeq.hs+1

compare with master

unifiedsplit

@@ -19,6 +19,7 @@ instance NFData SpecialName where

19 rnf (MethodN x1) = rnf x1 `seq` ()

20 rnf (CaseN x1) = rnf x1 `seq` ()

21 rnf (ElimN x1) = rnf x1 `seq` ()

22+ rnf (InstanceCtorN x1) = rnf x1 `seq` ()

22

23

23instance NFData Raw where

24instance NFData Raw where

24 rnf (Var x1) = rnf x1 `seq` ()

25 rnf (Var x1) = rnf x1 `seq` ()

src/Idris/Core/TT.hs+2

@@ -279,6 +279,7 @@ data SpecialName = WhereN Int Name Name

279 | MethodN Name

280 | CaseN Name

281 | ElimN Name

282+ | InstanceCtorN Name

282 deriving (Eq, Ord)

283 deriving (Eq, Ord)

283{-!

284{-!

284deriving instance Binary SpecialName

285deriving instance Binary SpecialName

@@ -322,6 +323,7 @@ instance Show SpecialName where

322 show (ParentN p c) = show p ++ "#" ++ T.unpack c

323 show (ParentN p c) = show p ++ "#" ++ T.unpack c

323 show (CaseN n) = "case block in " ++ show n

324 show (CaseN n) = "case block in " ++ show n

324 show (ElimN n) = "<<" ++ show n ++ " eliminator>>"

325 show (ElimN n) = "<<" ++ show n ++ " eliminator>>"

326+ show (InstanceCtorN n) = "constructor of " ++ show n

325

327

326-- Show a name in a way decorated for code generation, not human reading

328-- Show a name in a way decorated for code generation, not human reading

327showCG :: Name -> String

329showCG :: Name -> String

src/Idris/ElabDecls.hs+1−1

@@ -1721,7 +1721,7 @@ elabClass :: ElabInfo -> SyntaxInfo -> String ->

1721 FC -> [PTerm] ->

1722 Name -> [(Name, PTerm)] -> [PDecl] -> Idris ()

1723elabClass info syn doc fc constraints tn ps ds

1724− = do let cn = sUN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)

1724+ = do let cn = SN (InstanceCtorN tn) -- sUN ("instance" ++ show tn) -- MN 0 ("instance" ++ show tn)

1725 let tty = pibind ps PType

1726 let constraint = PApp fc (PRef fc tn)

1727 (map (pexp . PRef fc) (map fst ps))

src/Idris/IBC.hs+3

@@ -559,6 +559,7 @@ instance Binary SpecialName where

559 put x1

560 CaseN x1 -> do putWord8 4; put x1

561 ElimN x1 -> do putWord8 5; put x1

562+ InstanceCtorN x1 -> do putWord8 6; put x1

562 get

563 get

563 = do i <- getWord8

564 = do i <- getWord8

564 case i of

565 case i of

@@ -578,6 +579,8 @@ instance Binary SpecialName where

578 return (CaseN x1)

579 return (CaseN x1)

579 5 -> do x1 <- get

580 5 -> do x1 <- get

580 return (ElimN x1)

581 return (ElimN x1)

582+ 6 -> do x1 <- get

583+ return (InstanceCtorN x1)

581 _ -> error "Corrupted binary data for SpecialName"

584 _ -> error "Corrupted binary data for SpecialName"

582

585

583

586