5a5eeca · Idris-dev · git.iko.soy

src/Idris/AbsSyntax.hs+3−3

compare with master

unifiedsplit

@@ -959,12 +959,12 @@ expandParamsD rhs ist dec ps ns (PData doc argDocs syn fc co pd)

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

960 econ (doc, argDocs, n, t, fc, fs)

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

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

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

963 = if tn `elem` ns

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

965− cdoc (dec cn) conty

965+ opts cdoc (dec cn) conty

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

967− cdoc (dec cn) conty

967+ opts cdoc (dec cn) conty

968 where conty = piBindp expl ps (expandParams dec ps ns [] cty)

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

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

src/Idris/AbsSyntaxTree.hs+4−4

@@ -483,7 +483,7 @@ data PDecl' t

483 | PData Docstring [(Name, Docstring)] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.

484 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block

485 | PNamespace String [PDecl' t] -- ^ New namespace

486− | PRecord Docstring SyntaxInfo FC Name t Docstring Name t -- ^ Record declaration

486+ | PRecord Docstring SyntaxInfo FC Name t DataOpts Docstring Name t -- ^ Record declaration

487 | PClass Docstring SyntaxInfo FC

488 [t] -- constraints

489 Name

@@ -569,7 +569,7 @@ declared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

569declared (PData _ _ _ _ _ (PLaterdecl n _)) = [n]

570declared (PParams _ _ ds) = concatMap declared ds

571declared (PNamespace _ ds) = concatMap declared ds

572−declared (PRecord _ _ _ n _ _ c _) = [n, c]

572+declared (PRecord _ _ _ n _ _ _ c _) = [n, c]

573declared (PClass _ _ _ _ n _ ms) = n : concatMap declared ms

574declared (PInstance _ _ _ _ _ _ _ _) = []

575declared (PDSL n _) = [n]

@@ -583,7 +583,7 @@ tldeclared (PFix _ _ _) = []

583tldeclared (PTy _ _ _ _ _ n t) = [n]

584tldeclared (PPostulate _ _ _ _ n t) = [n]

585tldeclared (PClauses _ _ n _) = [] -- not a declaration

586−tldeclared (PRecord _ _ _ n _ _ c _) = [n, c]

586+tldeclared (PRecord _ _ _ n _ _ _ c _) = [n, c]

587tldeclared (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

588 where fstt (_, _, a, _, _, _) = a

589tldeclared (PParams _ _ ds) = []

@@ -604,7 +604,7 @@ defined (PData _ _ _ _ _ (PDatadecl n _ ts)) = n : map fstt ts

604defined (PData _ _ _ _ _ (PLaterdecl n _)) = []

605defined (PParams _ _ ds) = concatMap defined ds

606defined (PNamespace _ ds) = concatMap defined ds

607−defined (PRecord _ _ _ n _ _ c _) = [n, c]

607+defined (PRecord _ _ _ n _ _ _ c _) = [n, c]

608defined (PClass _ _ _ _ n _ ms) = n : concatMap defined ms

609defined (PInstance _ _ _ _ _ _ _ _) = []

610defined (PDSL n _) = [n]

src/Idris/Core/Evaluate.hs+8−1

@@ -11,7 +11,7 @@ module Idris.Core.Evaluate(normalise, normaliseTrace, normaliseC, normaliseAll,

11 lookupNames, lookupTy, lookupP, lookupDef, lookupNameDef, lookupDefExact, lookupDefAcc, lookupVal,

12 mapDefCtxt,

13 lookupTotal, lookupNameTotal, lookupMetaInformation, lookupTyEnv, isDConName, isTConName, isConName, isFnName,

14− Value(..), Quote(..), initEval, uniqueNameCtxt, definitions) where

14+ Value(..), Quote(..), initEval, uniqueNameCtxt, uniqueBindersCtxt, definitions) where

15

16import Debug.Trace

17import Control.Applicative hiding (Const)

@@ -961,3 +961,10 @@ uniqueNameCtxt ctxt n hs

961 | n `elem` hs = uniqueNameCtxt ctxt (nextName n) hs

962 | [_] <- lookupTy n ctxt = uniqueNameCtxt ctxt (nextName n) hs

963 | otherwise = n

964+

965+uniqueBindersCtxt :: Context -> [Name] -> TT Name -> TT Name

966+uniqueBindersCtxt ctxt ns (Bind n b sc)

967+ = let n' = uniqueNameCtxt ctxt n ns in

968+ Bind n' (fmap (uniqueBindersCtxt ctxt (n':ns)) b) (uniqueBindersCtxt ctxt ns sc)

969+uniqueBindersCtxt ctxt ns (App f a) = App (uniqueBindersCtxt ctxt ns f) (uniqueBindersCtxt ctxt ns a)

970+uniqueBindersCtxt ctxt ns t = t

src/Idris/Core/ProofState.hs+2−2

@@ -15,7 +15,7 @@ import Idris.Core.Unify

15

16import Control.Monad.State.Strict

17import Control.Applicative hiding (empty)

18−import Control.Arrow (first)

18+import Control.Arrow ((***))

19import Data.List

20import Debug.Trace

21

@@ -666,7 +666,7 @@ induction nm ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

666 let scr = last $ tail args'

667 let indxnames = makeIndexNames indicies

668 prop <- replaceIndicies indxnames indicies $ Bind nm (Lam tmt') t

669− consargs' <- query (\ps -> map (first $ flip (uniqueNameCtxt (context ps)) (holes ps)) consargs)

669+ consargs' <- query (\ps -> map (flip (uniqueNameCtxt (context ps)) (holes ps ++ allTTNames (pterm ps)) *** uniqueBindersCtxt (context ps) (holes ps ++ allTTNames (pterm ps))) consargs)

670 let res = flip (foldr substV) params $ (substV prop $ bindConsArgs consargs' (mkApp (P Ref (SN (ElimN tnm)) (TType (UVal 0)))

671 (params ++ [prop] ++ map makeConsArg consargs' ++ indicies ++ [tmv])))

672 action (\ps -> ps {holes = holes ps \\ [x]})

src/Idris/Core/TT.hs+9

@@ -1223,3 +1223,12 @@ orderPats tm = op [] tm

1223 = (n', t') : insert n t ps

1224 | otherwise = (n,t):(n',t'):ps

1225

1226+allTTNames :: Eq n => TT n -> [n]

1227+allTTNames = nub . allNamesIn

1228+ where allNamesIn (P _ n _) = [n]

1229+ allNamesIn (Bind n b t) = [n] ++ nb b ++ allNamesIn t

1230+ where nb (Let t v) = allNamesIn t ++ allNamesIn v

1231+ nb (Guess t v) = allNamesIn t ++ allNamesIn v

1232+ nb t = allNamesIn (binderTy t)

1233+ allNamesIn (App f a) = allNamesIn f ++ allNamesIn a

1234+ allNamesIn _ = []

src/Idris/DeepSeq.hs+2−2

@@ -138,11 +138,11 @@ instance (NFData t) => NFData (PDecl' t) where

138 rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

139 rnf (PParams x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

140 rnf (PNamespace x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

141− rnf (PRecord x1 x2 x3 x4 x5 x6 x7 x8)

141+ rnf (PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9)

142 = rnf x1 `seq`

143 rnf x2 `seq`

144 rnf x3 `seq`

145− rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` ()

145+ rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` ()

146 rnf (PClass x1 x2 x3 x4 x5 x6 x7)

147 = rnf x1 `seq`

148 rnf x2 `seq`

src/Idris/ElabDecls.hs+5−5

@@ -771,9 +771,9 @@ elabTransform info fc safe lhs_in rhs_in

771

772

773elabRecord :: ElabInfo -> SyntaxInfo -> Docstring -> FC -> Name ->

774− PTerm -> Docstring -> Name -> PTerm -> Idris ()

774+ PTerm -> DataOpts -> Docstring -> Name -> PTerm -> Idris ()

775−elabRecord info syn doc fc tyn ty cdoc cn cty

775+elabRecord info syn doc fc tyn ty opts cdoc cn cty

776− = do elabData info syn doc [] fc [] (PDatadecl tyn ty [(cdoc, [], cn, cty, fc, [])])

776+ = do elabData info syn doc [] fc opts (PDatadecl tyn ty [(cdoc, [], cn, cty, fc, [])])

777 -- TODO think: something more in info?

778 cty' <- implicit info syn cn cty

779 i <- getIState

@@ -2320,10 +2320,10 @@ elabDecl' what info (PClass doc s f cs n ps ds)

2320elabDecl' what info (PInstance s f cs n ps t expn ds)

2321 = do iLOG $ "Elaborating instance " ++ show n

2322 elabInstance info s what f cs n ps t expn ds

2323−elabDecl' what info (PRecord doc s f tyn ty cdoc cn cty)

2323+elabDecl' what info (PRecord doc s f tyn ty opts cdoc cn cty)

2324 | what /= ETypes

2325 = do iLOG $ "Elaborating record " ++ show tyn

2326− elabRecord info s doc f tyn ty cdoc cn cty

2326+ elabRecord info s doc f tyn ty opts cdoc cn cty

2327 | otherwise

2328 = do iLOG $ "Elaborating [type of] " ++ show tyn

2329 elabData info s doc [] f [] (PLaterdecl tyn ty)

src/Idris/IBC.hs+5−3

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

30import Util.Zlib (decompressEither)

31

32ibcVersion :: Word8

33−ibcVersion = 67

33+ibcVersion = 68

34

35data IBCFile = IBCFile { ver :: Word8,

36 sourcefile :: FilePath,

@@ -1425,7 +1425,7 @@ instance (Binary t) => Binary (PDecl' t) where

1425 PNamespace x1 x2 -> do putWord8 5

1426 put x1

1427 put x2

1428− PRecord x1 x2 x3 x4 x5 x6 x7 x8 ->

1428+ PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9 ->

1429 do putWord8 6

1430 put x1

1431 put x2

@@ -1435,6 +1435,7 @@ instance (Binary t) => Binary (PDecl' t) where

1435 put x6

1436 put x7

1437 put x8

1438+ put x9

1438 PClass x1 x2 x3 x4 x5 x6 x7

1439 PClass x1 x2 x3 x4 x5 x6 x7

1439 -> do putWord8 7

1440 -> do putWord8 7

1440 put x1

1441 put x1

@@ -1513,7 +1514,8 @@ instance (Binary t) => Binary (PDecl' t) where

1513 x6 <- get

1514 x6 <- get

1514 x7 <- get

1515 x7 <- get

1515 x8 <- get

1516 x8 <- get

1517+ x9 <- get

1516− return (PRecord x1 x2 x3 x4 x5 x6 x7 x8)

1518+ return (PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9)

1517 7 -> do x1 <- get

1519 7 -> do x1 <- get

1518 x2 <- get

1520 x2 <- get

1519 x3 <- get

1521 x3 <- get

src/Idris/ParseData.hs+4−3

@@ -42,11 +42,12 @@ Record ::=

42 DocComment Accessibility? 'record' FnName TypeSig 'where' OpenBlock Constructor KeepTerminator CloseBlock;

43-}

44record :: SyntaxInfo -> IdrisParser PDecl

45−record syn = do (doc, acc) <- try (do

45+record syn = do (doc, acc, opts) <- try (do

46 doc <- option noDocs docComment

47 acc <- optional accessibility

48+ opts <- dataOpts []

48 reserved "record"

49 reserved "record"

49− return (doc, acc))

50+ return (doc, acc, opts))

50 fc <- getFC

51 fc <- getFC

51 tyn_in <- fnName

52 tyn_in <- fnName

52 lchar ':'

53 lchar ':'

@@ -59,7 +60,7 @@ record syn = do (doc, acc) <- try (do

59 syn_namespace syn }

60 syn_namespace syn }

60 let fns = getRecNames rsyn cty

61 let fns = getRecNames rsyn cty

61 mapM_ (\n -> addAcc n acc) fns

62 mapM_ (\n -> addAcc n acc) fns

62− return $ PRecord (fst doc) rsyn fc tyn ty cdoc cn cty

63+ return $ PRecord (fst doc) rsyn fc tyn ty opts cdoc cn cty

63 <?> "record type declaration"

64 <?> "record type declaration"

64 where

65 where

65 getRecNames :: SyntaxInfo -> PTerm -> [Name]

66 getRecNames :: SyntaxInfo -> PTerm -> [Name]