cb4b145 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #942 from ziman/instance-ctors

Add special names for instance constructors

commitcb4b1459cd5b7ecb58e46a068d4ed9e0842b4a8b authorEdwin Brady <edwin.brady@gmail.com> dateSun 2 Mar 2014, 23:39 (13 years ago) parentc2671c0 fe519db

4 files changed+8−2

compare with master

unifiedsplit

src/Idris/Core/DeepSeq.hs+1 src/Idris/Core/TT.hs+2 src/Idris/ElabDecls.hs+1−1 src/Idris/IBC.hs+4−1

src/Idris/Core/DeepSeq.hs+1

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

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

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

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

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

2223

2324instance NFData Raw where

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

src/Idris/Core/TT.hs+2

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

279279 | MethodN Name

280280 | CaseN Name

281281 | ElimN Name

282+ | InstanceCtorN Name

282283 deriving (Eq, Ord)

283284{-!

284285deriving instance Binary SpecialName

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

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

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

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

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

325327

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

327329showCG :: Name -> String

src/Idris/ElabDecls.hs+1−1

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

17211721 FC -> [PTerm] ->

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

17231723elabClass 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)

17251725 let tty = pibind ps PType

17261726 let constraint = PApp fc (PRef fc tn)

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

src/Idris/IBC.hs+4−1

@@ -25,7 +25,7 @@ import Codec.Compression.Zlib (compress)

2525import Util.Zlib (decompressEither)

2626

2727ibcVersion :: Word8

28−ibcVersion = 61

28+ibcVersion = 62

2929

3030

3131data IBCFile = IBCFile { ver :: Word8,

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

559559 put x1

560560 CaseN x1 -> do putWord8 4; put x1

561561 ElimN x1 -> do putWord8 5; put x1

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

562563 get

563564 = do i <- getWord8

564565 case i of

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

578579 return (CaseN x1)

579580 5 -> do x1 <- get

580581 return (ElimN x1)

582+ 6 -> do x1 <- get

583+ return (InstanceCtorN x1)

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

582585

583586