78ff448 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Bug fixing of induction bugs

Allow renaming according to introduced context Allow induction on records

commit78ff448fbdf4d1c92e98ba885a769acfc86b76c2 authorAhmad Salim Al-Sibahi <asal@itu.dk> dateThu 1 May 2014, 10:44 (12 years ago) parentfd1219b

9 files changed+42−23

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+3−3 src/Idris/AbsSyntaxTree.hs+4−4 src/Idris/Core/Evaluate.hs+8−1 src/Idris/Core/ProofState.hs+2−2 src/Idris/Core/TT.hs+9 src/Idris/DeepSeq.hs+2−2 src/Idris/ElabDecls.hs+5−5 src/Idris/IBC.hs+5−3 src/Idris/ParseData.hs+4−3

src/Idris/AbsSyntax.hs+3−3

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

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

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

961961 = (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)

963963 = if tn `elem` ns

964964 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

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

967− cdoc (dec cn) conty

967+ opts cdoc (dec cn) conty

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

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

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

src/Idris/AbsSyntaxTree.hs+4−4

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

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

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

485485 | 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

487487 | PClass Docstring SyntaxInfo FC

488488 [t] -- constraints

489489 Name

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

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

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

571571declared (PNamespace _ ds) = concatMap declared ds

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

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

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

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

575575declared (PDSL n _) = [n]

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

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

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

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

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

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

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

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

589589tldeclared (PParams _ _ ds) = []

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

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

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

606606defined (PNamespace _ ds) = concatMap defined ds

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

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

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

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

610610defined (PDSL n _) = [n]

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

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

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

1212 mapDefCtxt,

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

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

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

1515

1616import Debug.Trace

1717import Control.Applicative hiding (Const)

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

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

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

963963 | 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

1515

1616import Control.Monad.State.Strict

1717import Control.Applicative hiding (empty)

18−import Control.Arrow (first)

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

1919import Data.List

2020import Debug.Trace

2121

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

666666 let scr = last $ tail args'

667667 let indxnames = makeIndexNames indicies

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

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

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

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

src/Idris/Core/TT.hs+9

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

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

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

12251225

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

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

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

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

142142 = rnf x1 `seq`

143143 rnf x2 `seq`

144144 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` ()

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

147147 = rnf x1 `seq`

148148 rnf x2 `seq`

src/Idris/ElabDecls.hs+5−5

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

770770

771771

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

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

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

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

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

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

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

776776 -- TODO think: something more in info?

777777 cty' <- implicit info syn cn cty

778778 i <- getIState

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

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

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

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

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

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

23222322 | what /= ETypes

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

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

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

23252325 | otherwise

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

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

src/Idris/IBC.hs+5−3

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

3030import Util.Zlib (decompressEither)

3131

3232ibcVersion :: Word8

33−ibcVersion = 67

33+ibcVersion = 68

3434

3535data IBCFile = IBCFile { ver :: Word8,

3636 sourcefile :: FilePath,

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

14251425 PNamespace x1 x2 -> do putWord8 5

14261426 put x1

14271427 put x2

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

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

14291429 do putWord8 6

14301430 put x1

14311431 put x2

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

14351435 put x6

14361436 put x7

14371437 put x8

1438+ put x9

14381439 PClass x1 x2 x3 x4 x5 x6 x7

14391440 -> do putWord8 7

14401441 put x1

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

15131514 x6 <- get

15141515 x7 <- get

15151516 x8 <- get

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

1517+ x9 <- get

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

15171519 7 -> do x1 <- get

15181520 x2 <- get

15191521 x3 <- get

src/Idris/ParseData.hs+4−3

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

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

4343-}

4444record :: SyntaxInfo -> IdrisParser PDecl

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

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

4646 doc <- option noDocs docComment

4747 acc <- optional accessibility

48+ opts <- dataOpts []

4849 reserved "record"

49− return (doc, acc))

50+ return (doc, acc, opts))

5051 fc <- getFC

5152 tyn_in <- fnName

5253 lchar ':'

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

5960 syn_namespace syn }

6061 let fns = getRecNames rsyn cty

6162 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

6364 <?> "record type declaration"

6465 where

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