40d094d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Expose equality proofs in with rule

40d094dEdwin Brady12 years ago

src/Idris/AbsSyntax.hs+2−1

compare with master

unifiedsplit

@@ -1016,7 +1016,7 @@ expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)

1016 (map (expandParams dec ps'' ns' []) ws)

1017 (expandParams dec ps'' ns' [] rhs)

1018 (map (expandParamsD True ist dec ps'' ns') ds)

1019− expandParamsC (PWith fc n lhs ws wval ds)

1019+ expandParamsC (PWith fc n lhs ws wval pn ds)

1020 = let -- ps' = updateps True (namesIn ist wval) (zip ps [0..])

1021 ps'' = updateps False (namesIn [] ist lhs) (zip ps [0..])

1022 lhs' = if rhsonly then lhs else (expandParams dec ps'' ns [] lhs)

@@ -1025,6 +1025,7 @@ expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)

1025 PWith fc n' lhs'

1026 (map (expandParams dec ps'' ns' []) ws)

1027 (expandParams dec ps'' ns' [] wval)

1028+ pn

1028 (map (expandParamsD rhsonly ist dec ps'' ns') ds)

1029 (map (expandParamsD rhsonly ist dec ps'' ns') ds)

1029 updateps yn nm [] = []

1030 updateps yn nm [] = []

1030 updateps yn nm (((a, t), i):as)

1031 updateps yn nm (((a, t), i):as)

src/Idris/AbsSyntaxTree.hs+5−5

@@ -637,10 +637,10 @@ type ElabD a = Elab' EState a

637--

638-- 4. The where block (PDecl' t)

639

640−data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.

640+data PClause' t = PClause FC Name t [t] t [PDecl' t] -- ^ A normal top-level definition.

641− | PWith FC Name t [t] t [PDecl' t]

641+ | PWith FC Name t [t] t (Maybe Name) [PDecl' t]

642− | PClauseR FC [t] t [PDecl' t]

642+ | PClauseR FC [t] t [PDecl' t]

643− | PWithR FC [t] t [PDecl' t]

643+ | PWithR FC [t] t (Maybe Name) [PDecl' t]

644 deriving Functor

645{-!

646deriving instance Binary PClause'

@@ -1692,7 +1692,7 @@ showCImp ppo (PClause _ n l ws r w)

1692 where

1693 showWs [] = empty

1694 showWs (x : xs) = text "|" <+> prettyImp ppo x <+> showWs xs

1695−showCImp ppo (PWith _ n l ws r w)

1695+showCImp ppo (PWith _ n l ws r pn w)

1696 = prettyImp ppo l <+> showWs ws <+> text "with" <+> prettyImp ppo r

1697 <+> braces (text (show w))

1698 where

src/Idris/DeepSeq.hs+4−4

@@ -178,13 +178,13 @@ instance (NFData t) => NFData (PClause' t) where

178 rnf (PClause x1 x2 x3 x4 x5 x6)

179 = rnf x1 `seq`

180 rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

181− rnf (PWith x1 x2 x3 x4 x5 x6)

181+ rnf (PWith x1 x2 x3 x4 x5 x6 x7)

182 = rnf x1 `seq`

183− rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

183+ rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` ()

184 rnf (PClauseR x1 x2 x3 x4)

185 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

186− rnf (PWithR x1 x2 x3 x4)

186+ rnf (PWithR x1 x2 x3 x4 x5)

187− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

187+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

188

189instance (NFData t) => NFData (PData' t) where

190 rnf (PDatadecl x1 x2 x3)

src/Idris/Elab/Clause.hs+40−22

@@ -796,7 +796,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

796 isArg' _ = False

797 isArg _ _ = False

798

799−elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

799+elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

800 = do let tcgen = Dictionary `elem` opts

801 ctxt <- getContext

802 -- Build the LHS as an "Infer", and pull out its type and

@@ -859,6 +859,11 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

859 -- rather than a de Bruijn index.

860 let pdeps = usedNamesIn pvars i (delab i cwvalty)

861 let (bargs_pre, bargs_post) = split pdeps bargs []

862+

863+ let mpn = case pn_in of

864+ Nothing -> Nothing

865+ Just n -> Just (uniqueName n (map fst bargs))

866+

862 logLvl 10 ("With type " ++ show (getRetTy cwvaltyN) ++

867 logLvl 10 ("With type " ++ show (getRetTy cwvaltyN) ++

863 " depends on " ++ show pdeps ++ " from " ++ show pvars)

868 " depends on " ++ show pdeps ++ " from " ++ show pvars)

864 logLvl 10 ("Pre " ++ show bargs_pre ++ "\nPost " ++ show bargs_post)

869 logLvl 10 ("Pre " ++ show bargs_pre ++ "\nPost " ++ show bargs_post)

@@ -867,12 +872,19 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

867 -- (ps : Xs) -> (withval : cwvalty) -> (ps' : Xs') -> ret_ty

872 -- (ps : Xs) -> (withval : cwvalty) -> (ps' : Xs') -> ret_ty

868 let wargval = getRetTy cwvalN

873 let wargval = getRetTy cwvalN

869 let wargtype = getRetTy cwvaltyN

874 let wargtype = getRetTy cwvaltyN

875+ let wargname = sMN windex "warg"

876+

870 logLvl 5 ("Abstract over " ++ show wargval ++ " in " ++ show wargtype)

877 logLvl 5 ("Abstract over " ++ show wargval ++ " in " ++ show wargtype)

871 let wtype = bindTyArgs (flip (Pi Nothing) (TType (UVar 0))) (bargs_pre ++

878 let wtype = bindTyArgs (flip (Pi Nothing) (TType (UVar 0))) (bargs_pre ++

872− (sMN 0 "warg", wargtype) :

879+ (wargname, wargtype) :

873− map (abstract (sMN 0 "warg") wargval wargtype) bargs_post)

880+ map (abstract wargname wargval wargtype) bargs_post ++

881+ case mpn of

882+ Just pn -> [(pn, mkApp (P Ref eqTy Erased)

883+ [wargtype, wargtype,

884+ P Bound wargname Erased, wargval])]

885+ Nothing -> [])

874− (substTerm wargval (P Bound (sMN 0 "warg") wargtype) ret_ty)

886+ (substTerm wargval (P Bound wargname wargtype) ret_ty)

875− logLvl 5 ("New function type " ++ show wtype)

887+ logLvl 3 ("New function type " ++ show wtype)

876 let wname = SN (WithN windex fname)

888 let wname = SN (WithN windex fname)

877

889

878 let imps = getImps wtype -- add to implicits context

890 let imps = getImps wtype -- add to implicits context

@@ -893,18 +905,21 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

893 -- in the subdecls, lhs becomes:

905 -- in the subdecls, lhs becomes:

894 -- fname pats | wpat [rest]

906 -- fname pats | wpat [rest]

895 -- ==> fname' ps wpat [rest], match pats against toplevel for ps

907 -- ==> fname' ps wpat [rest], match pats against toplevel for ps

896− wb <- mapM (mkAuxC wname lhs (map fst bargs_pre) (map fst bargs_post))

908+ wb <- mapM (mkAuxC mpn wname lhs (map fst bargs_pre) (map fst bargs_post))

897 withblock

909 withblock

898 logLvl 3 ("with block " ++ show wb)

910 logLvl 3 ("with block " ++ show wb)

899 -- propagate totality assertion to the new definitions

911 -- propagate totality assertion to the new definitions

900 when (AssertTotal `elem` opts) $ setFlags wname [AssertTotal]

912 when (AssertTotal `elem` opts) $ setFlags wname [AssertTotal]

901 mapM_ (rec_elabDecl info EAll info) wb

913 mapM_ (rec_elabDecl info EAll info) wb

902

914

903− -- rhs becomes: fname' ps wval

915+ -- rhs becomes: fname' ps_pre wval ps_post Refl

904 let rhs = PApp fc (PRef fc wname)

916 let rhs = PApp fc (PRef fc wname)

905 (map (pexp . (PRef fc) . fst) bargs_pre ++

917 (map (pexp . (PRef fc) . fst) bargs_pre ++

906 pexp wval :

918 pexp wval :

907− (map (pexp . (PRef fc) . fst) bargs_post))

919+ (map (pexp . (PRef fc) . fst) bargs_post) ++

920+ case mpn of

921+ Nothing -> []

922+ Just _ -> [pexp (PRefl fc Placeholder)])

908 logLvl 5 ("New RHS " ++ showTmImpls rhs)

923 logLvl 5 ("New RHS " ++ showTmImpls rhs)

909 ctxt <- getContext -- New context with block added

924 ctxt <- getContext -- New context with block added

910 i <- getIState

925 i <- getIState

@@ -927,13 +942,13 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

927 getImps (Bind n (Pi _ _ _) t) = pexp Placeholder : getImps t

942 getImps (Bind n (Pi _ _ _) t) = pexp Placeholder : getImps t

928 getImps _ = []

943 getImps _ = []

929

944

930− mkAuxC wname lhs ns ns' (PClauses fc o n cs)

945+ mkAuxC pn wname lhs ns ns' (PClauses fc o n cs)

931− | True = do cs' <- mapM (mkAux wname lhs ns ns') cs

946+ | True = do cs' <- mapM (mkAux pn wname lhs ns ns') cs

932 return $ PClauses fc o wname cs'

947 return $ PClauses fc o wname cs'

933 | otherwise = ifail $ show fc ++ "with clause uses wrong function name " ++ show n

948 | otherwise = ifail $ show fc ++ "with clause uses wrong function name " ++ show n

934− mkAuxC wname lhs ns ns' d = return $ d

949+ mkAuxC pn wname lhs ns ns' d = return $ d

935

950

936− mkAux wname toplhs ns ns' (PClause fc n tm_in (w:ws) rhs wheres)

951+ mkAux pn wname toplhs ns ns' (PClause fc n tm_in (w:ws) rhs wheres)

937 = do i <- getIState

952 = do i <- getIState

938 let tm = addImplPat i tm_in

953 let tm = addImplPat i tm_in

939 logLvl 2 ("Matching " ++ showTmImpls tm ++ " against " ++

954 logLvl 2 ("Matching " ++ showTmImpls tm ++ " against " ++

@@ -942,33 +957,36 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

942 Left (a,b) -> ifail $ show fc ++ ":with clause does not match top level"

957 Left (a,b) -> ifail $ show fc ++ ":with clause does not match top level"

943 Right mvars ->

958 Right mvars ->

944 do logLvl 3 ("Match vars : " ++ show mvars)

959 do logLvl 3 ("Match vars : " ++ show mvars)

945− lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w

960+ lhs <- updateLHS n pn wname mvars ns ns' (fullApp tm) w

946 return $ PClause fc wname lhs ws rhs wheres

961 return $ PClause fc wname lhs ws rhs wheres

947− mkAux wname toplhs ns ns' (PWith fc n tm_in (w:ws) wval withs)

962+ mkAux pn wname toplhs ns ns' (PWith fc n tm_in (w:ws) wval pn' withs)

948 = do i <- getIState

963 = do i <- getIState

949 let tm = addImplPat i tm_in

964 let tm = addImplPat i tm_in

950 logLvl 2 ("Matching " ++ showTmImpls tm ++ " against " ++

965 logLvl 2 ("Matching " ++ showTmImpls tm ++ " against " ++

951 showTmImpls toplhs)

966 showTmImpls toplhs)

952− withs' <- mapM (mkAuxC wname toplhs ns ns') withs

967+ withs' <- mapM (mkAuxC pn wname toplhs ns ns') withs

953 case matchClause i toplhs tm of

968 case matchClause i toplhs tm of

954 Left (a,b) -> trace ("matchClause: " ++ show a ++ " =/= " ++ show b) (ifail $ show fc ++ "with clause does not match top level")

969 Left (a,b) -> trace ("matchClause: " ++ show a ++ " =/= " ++ show b) (ifail $ show fc ++ "with clause does not match top level")

955 Right mvars ->

970 Right mvars ->

956− do lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w

971+ do lhs <- updateLHS n pn wname mvars ns ns' (fullApp tm) w

957− return $ PWith fc wname lhs ws wval withs'

972+ return $ PWith fc wname lhs ws wval pn' withs'

958− mkAux wname toplhs ns ns' c

973+ mkAux pn wname toplhs ns ns' c

959 = ifail $ show fc ++ ":badly formed with clause"

974 = ifail $ show fc ++ ":badly formed with clause"

960

975

961 addArg (PApp fc f args) w = PApp fc f (args ++ [pexp w])

976 addArg (PApp fc f args) w = PApp fc f (args ++ [pexp w])

962 addArg (PRef fc f) w = PApp fc (PRef fc f) [pexp w]

977 addArg (PRef fc f) w = PApp fc (PRef fc f) [pexp w]

963

978

964− updateLHS n wname mvars ns_in ns_in' (PApp fc (PRef fc' n') args) w

979+ updateLHS n pn wname mvars ns_in ns_in' (PApp fc (PRef fc' n') args) w

965 = let ns = map (keepMvar (map fst mvars) fc') ns_in

980 = let ns = map (keepMvar (map fst mvars) fc') ns_in

966 ns' = map (keepMvar (map fst mvars) fc') ns_in' in

981 ns' = map (keepMvar (map fst mvars) fc') ns_in' in

967 return $ substMatches mvars $

982 return $ substMatches mvars $

968 PApp fc (PRef fc' wname)

983 PApp fc (PRef fc' wname)

969− (map pexp ns ++ pexp w : (map pexp ns'))

984+ (map pexp ns ++ pexp w : (map pexp ns') ++

985+ case pn of

986+ Nothing -> []

987+ Just pnm -> [pexp (PRef fc pnm)])

970− updateLHS n wname mvars ns_in ns_in' tm w

988+ updateLHS n pn wname mvars ns_in ns_in' tm w

971− = updateLHS n wname mvars ns_in ns_in' (PApp fc tm []) w

989+ = updateLHS n pn wname mvars ns_in ns_in' (PApp fc tm []) w

972

990

973 keepMvar mvs fc v | v `elem` mvs = PRef fc v

991 keepMvar mvs fc v | v `elem` mvs = PRef fc v

974 | otherwise = Placeholder

992 | otherwise = Placeholder

src/Idris/Elab/Utils.hs+2−2

@@ -120,8 +120,8 @@ decorateid decorate (PTy doc argdocs s f o n t) = PTy doc argdocs s f o (decorat

120decorateid decorate (PClauses f o n cs)

121 = PClauses f o (decorate n) (map dc cs)

122 where dc (PClause fc n t as w ds) = PClause fc (decorate n) (dappname t) as w ds

123− dc (PWith fc n t as w ds)

123+ dc (PWith fc n t as w pn ds)

124− = PWith fc (decorate n) (dappname t) as w

124+ = PWith fc (decorate n) (dappname t) as w pn

125 (map (decorateid decorate) ds)

126 dappname (PApp fc (PRef fc' n) as) = PApp fc (PRef fc' (decorate n)) as

127 dappname t = t

src/Idris/IBC.hs+19−15

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

36import Util.Zlib (decompressEither)

38ibcVersion :: Word8

39−ibcVersion = 95

39+ibcVersion = 96

41data IBCFile = IBCFile { ver :: Word8,

42 sourcefile :: FilePath,

@@ -1368,23 +1368,25 @@ instance (Binary t) => Binary (PClause' t) where

1368 put x4

1369 put x5

1370 put x6

1371− PWith x1 x2 x3 x4 x5 x6 -> do putWord8 1

1371+ PWith x1 x2 x3 x4 x5 x6 x7 -> do putWord8 1

1372− put x1

1372+ put x1

1373− put x2

1373+ put x2

1374− put x3

1374+ put x3

1375− put x4

1375+ put x4

1376− put x5

1376+ put x5

1377− put x6

1377+ put x6

1378+ put x7

1378 PClauseR x1 x2 x3 x4 -> do putWord8 2

1379 PClauseR x1 x2 x3 x4 -> do putWord8 2

1379 put x1

1380 put x1

1380 put x2

1381 put x2

1381 put x3

1382 put x3

1382 put x4

1383 put x4

1383− PWithR x1 x2 x3 x4 -> do putWord8 3

1384+ PWithR x1 x2 x3 x4 x5 -> do putWord8 3

1384− put x1

1385+ put x1

1385− put x2

1386+ put x2

1386− put x3

1387+ put x3

1387− put x4

1388+ put x4

1389+ put x5

1388 get

1390 get

1389 = do i <- getWord8

1391 = do i <- getWord8

1390 case i of

1392 case i of

@@ -1401,7 +1403,8 @@ instance (Binary t) => Binary (PClause' t) where

1401 x4 <- get

1403 x4 <- get

1402 x5 <- get

1404 x5 <- get

1403 x6 <- get

1405 x6 <- get

1406+ x7 <- get

1404− return (PWith x1 x2 x3 x4 x5 x6)

1407+ return (PWith x1 x2 x3 x4 x5 x6 x7)

1405 2 -> do x1 <- get

1408 2 -> do x1 <- get

1406 x2 <- get

1409 x2 <- get

1407 x3 <- get

1410 x3 <- get

@@ -1411,7 +1414,8 @@ instance (Binary t) => Binary (PClause' t) where

1411 x2 <- get

1414 x2 <- get

1412 x3 <- get

1415 x3 <- get

1413 x4 <- get

1416 x4 <- get

1417+ x5 <- get

1414− return (PWithR x1 x2 x3 x4)

1418+ return (PWithR x1 x2 x3 x4 x5)

1415 _ -> error "Corrupted binary data for PClause'"

1419 _ -> error "Corrupted binary data for PClause'"

1416

1420

1417instance (Binary t) => Binary (PData' t) where

1421instance (Binary t) => Binary (PData' t) where

src/Idris/ParseHelpers.hs+4−4

@@ -564,17 +564,17 @@ collect (c@(PClauses _ o _ _) : ds)

564 where clauses :: Maybe Name -> [PClause] -> [PDecl] -> [PDecl]

565 clauses j@(Just n) acc (PClauses fc _ _ [PClause fc' n' l ws r w] : ds)

566 | n == n' = clauses j (PClause fc' n' l ws r (collect w) : acc) ds

567− clauses j@(Just n) acc (PClauses fc _ _ [PWith fc' n' l ws r w] : ds)

567+ clauses j@(Just n) acc (PClauses fc _ _ [PWith fc' n' l ws r pn w] : ds)

568− | n == n' = clauses j (PWith fc' n' l ws r (collect w) : acc) ds

568+ | n == n' = clauses j (PWith fc' n' l ws r pn (collect w) : acc) ds

569 clauses (Just n) acc xs = PClauses (fcOf c) o n (reverse acc) : collect xs

570 clauses Nothing acc (x:xs) = collect xs

571 clauses Nothing acc [] = []

572

573 cname :: PDecl -> Maybe Name

574 cname (PClauses fc _ _ [PClause _ n _ _ _ _]) = Just n

575− cname (PClauses fc _ _ [PWith _ n _ _ _ _]) = Just n

575+ cname (PClauses fc _ _ [PWith _ n _ _ _ _ _]) = Just n

576 cname (PClauses fc _ _ [PClauseR _ _ _ _]) = Nothing

577− cname (PClauses fc _ _ [PWithR _ _ _ _]) = Nothing

577+ cname (PClauses fc _ _ [PWithR _ _ _ _ _]) = Nothing

578 fcOf :: PDecl -> FC

579 fcOf (PClauses fc _ _ _) = fc

580collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds

src/Idris/Parser.hs+12−5

@@ -826,11 +826,12 @@ clause syn

826 popIndent

827 reserved "with"

828 wval <- simpleExpr syn

829+ pn <- optProof

829 openBlock

830 openBlock

830 ds <- some $ fnDecl syn

831 ds <- some $ fnDecl syn

831 let withs = concat ds

832 let withs = concat ds

832 closeBlock

833 closeBlock

833− return $ PWithR fc wargs wval withs)

834+ return $ PWithR fc wargs wval pn withs)

834 <|> do ty <- try (do pushIndent

835 <|> do ty <- try (do pushIndent

835 ty <- simpleExpr syn

836 ty <- simpleExpr syn

836 symbol "<=="

837 symbol "<=="

@@ -878,6 +879,7 @@ clause syn

878 popIndent

879 popIndent

879 reserved "with"

880 reserved "with"

880 wval <- bracketed syn

881 wval <- bracketed syn

882+ pn <- optProof

881 openBlock

883 openBlock

882 ds <- some $ fnDecl syn

884 ds <- some $ fnDecl syn

883 closeBlock

885 closeBlock

@@ -885,7 +887,7 @@ clause syn

885 let capp = PApp fc (PRef fc n) [pexp l, pexp r]

887 let capp = PApp fc (PRef fc n) [pexp l, pexp r]

886 let withs = map (fillLHSD n capp wargs) $ concat ds

888 let withs = map (fillLHSD n capp wargs) $ concat ds

887 put (ist { lastParse = Just n })

889 put (ist { lastParse = Just n })

888− return $ PWith fc n capp wargs wval withs)

890+ return $ PWith fc n capp wargs wval pn withs)

889 <|> do pushIndent

891 <|> do pushIndent

890 n_in <- fnName; let n = expandNS syn n_in

892 n_in <- fnName; let n = expandNS syn n_in

891 cargs <- many (constraintArg syn)

893 cargs <- many (constraintArg syn)

@@ -911,19 +913,24 @@ clause syn

911 ist <- get

913 ist <- get

912 put (ist { lastParse = Just n })

914 put (ist { lastParse = Just n })

913 wval <- bracketed syn

915 wval <- bracketed syn

916+ pn <- optProof

914 openBlock

917 openBlock

915 ds <- some $ fnDecl syn

918 ds <- some $ fnDecl syn

916 let withs = map (fillLHSD n capp wargs) $ concat ds

919 let withs = map (fillLHSD n capp wargs) $ concat ds

917 closeBlock

920 closeBlock

918 popIndent

921 popIndent

919− return $ PWith fc n capp wargs wval withs)

922+ return $ PWith fc n capp wargs wval pn withs)

920 <?> "function clause"

923 <?> "function clause"

921 where

924 where

925+ optProof = option Nothing (do reserved "proof"

926+ n <- fnName

927+ return (Just n))

928+

922 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause

929 fillLHS :: Name -> PTerm -> [PTerm] -> PClause -> PClause

923 fillLHS n capp owargs (PClauseR fc wargs v ws)

930 fillLHS n capp owargs (PClauseR fc wargs v ws)

924 = PClause fc n capp (owargs ++ wargs) v ws

931 = PClause fc n capp (owargs ++ wargs) v ws

925− fillLHS n capp owargs (PWithR fc wargs v ws)

932+ fillLHS n capp owargs (PWithR fc wargs v pn ws)

926− = PWith fc n capp (owargs ++ wargs) v

933+ = PWith fc n capp (owargs ++ wargs) v pn

927 (map (fillLHSD n capp (owargs ++ wargs)) ws)

934 (map (fillLHSD n capp (owargs ++ wargs)) ws)

928 fillLHS _ _ _ c = c

935 fillLHS _ _ _ c = c

929

936

src/Idris/REPL.hs+3−3

@@ -756,7 +756,7 @@ process fn (NewDefn decls) = do

756 getName _ = Nothing

757 -- getClauseName is partial and I am not sure it's used safely! -- trillioneyes

758 getClauseName (PClause fc name whole with rhs whereBlock) = name

759− getClauseName (PWith fc name whole with rhs whereBlock) = name

759+ getClauseName (PWith fc name whole with rhs pn whereBlock) = name

760 defineName :: [PDecl] -> Idris ()

761 defineName (tyDecl@(PTy docs argdocs syn fc opts name ty) : decls) = do

762 elabDecl EAll recinfo tyDecl

@@ -785,9 +785,9 @@ process fn (NewDefn decls) = do

785 getClauses _ = []

786 getRHS :: PClause -> PTerm

787 getRHS (PClause fc name whole with rhs whereBlock) = rhs

788− getRHS (PWith fc name whole with rhs whereBlock) = rhs

788+ getRHS (PWith fc name whole with rhs pn whereBlock) = rhs

789 getRHS (PClauseR fc with rhs whereBlock) = rhs

790− getRHS (PWithR fc with rhs whereBlock) = rhs

790+ getRHS (PWithR fc with rhs pn whereBlock) = rhs

791 setReplDefined :: Maybe Name -> Idris ()

792 setReplDefined Nothing = return ()

793 setReplDefined (Just n) = do