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

git.iko.soy/Idris-dev

Expose equality proofs in with rule

Given a pattern matching definition of the form: foo args with (expr) proof q foo args | pat = rhs In 'rhs', 'q' is in scope, and is a proof that pat = expr. This can simplify some proofs (e.g. as in #1920) I'm not sure about the syntax for this (and I haven't documented it anyway), so this is EXPERIMENTAL for the moment. Syntax could change or disappear...

commit40d094dda971b24e4ee43eea4854e819873cc6f7 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 14 Feb 2015, 22:32 (12 years ago) parentc918f44

9 files changed+91−61

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+2−1 src/Idris/AbsSyntaxTree.hs+5−5 src/Idris/DeepSeq.hs+4−4 src/Idris/Elab/Clause.hs+40−22 src/Idris/Elab/Utils.hs+2−2 src/Idris/IBC.hs+19−15 src/Idris/ParseHelpers.hs+4−4 src/Idris/Parser.hs+12−5 src/Idris/REPL.hs+3−3

src/Idris/AbsSyntax.hs+2−1

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

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

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

10181018 (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)

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

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

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

10251025 PWith fc n' lhs'

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

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

1028+ pn

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

10291030 updateps yn nm [] = []

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

src/Idris/AbsSyntaxTree.hs+5−5

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

637637--

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

639639

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]

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

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

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

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

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

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

644644 deriving Functor

645645{-!

646646deriving instance Binary PClause'

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

16921692 where

16931693 showWs [] = empty

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

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

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

16981698 where

src/Idris/DeepSeq.hs+4−4

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

178178 rnf (PClause x1 x2 x3 x4 x5 x6)

179179 = rnf x1 `seq`

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

182182 = 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` ()

184184 rnf (PClauseR x1 x2 x3 x4)

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

186− rnf (PWithR x1 x2 x3 x4)

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

186+ rnf (PWithR x1 x2 x3 x4 x5)

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

188188

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

190190 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

796796 isArg' _ = False

797797 isArg _ _ = False

798798

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)

800800 = do let tcgen = Dictionary `elem` opts

801801 ctxt <- getContext

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

859859 -- rather than a de Bruijn index.

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

861861 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+

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

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

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

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

868873 let wargval = getRetTy cwvalN

869874 let wargtype = getRetTy cwvaltyN

875+ let wargname = sMN windex "warg"

876+

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

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

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

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

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

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

879+ (wargname, wargtype) :

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 -> [])

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

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

876888 let wname = SN (WithN windex fname)

877889

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

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

893905 -- in the subdecls, lhs becomes:

894906 -- fname pats | wpat [rest]

895907 -- ==> 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))

897909 withblock

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

899911 -- propagate totality assertion to the new definitions

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

901913 mapM_ (rec_elabDecl info EAll info) wb

902914

903− -- rhs becomes: fname' ps wval

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

904916 let rhs = PApp fc (PRef fc wname)

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

906918 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)])

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

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

910925 i <- getIState

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

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

928943 getImps _ = []

929944

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

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

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

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

932947 return $ PClauses fc o wname cs'

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

935950

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)

937952 = do i <- getIState

938953 let tm = addImplPat i tm_in

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

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

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

943958 Right mvars ->

944959 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

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

948963 = do i <- getIState

949964 let tm = addImplPat i tm_in

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

951966 showTmImpls toplhs)

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

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

953968 case matchClause i toplhs tm of

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

955970 Right mvars ->

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

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

958− mkAux wname toplhs ns ns' c

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

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

973+ mkAux pn wname toplhs ns ns' c

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

960975

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

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

963978

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

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

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

967982 return $ substMatches mvars $

968983 PApp fc (PRef fc' wname)

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

970− updateLHS n wname mvars ns_in ns_in' tm w

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

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

985+ case pn of

986+ Nothing -> []

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

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

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

972990

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

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

120120decorateid decorate (PClauses f o n cs)

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

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

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

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

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

125125 (map (decorateid decorate) ds)

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

127127 dappname t = t

src/Idris/IBC.hs+19−15

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

3636import Util.Zlib (decompressEither)

3737

3838ibcVersion :: Word8

39−ibcVersion = 95

39+ibcVersion = 96

4040

4141data IBCFile = IBCFile { ver :: Word8,

4242 sourcefile :: FilePath,

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

13681368 put x4

13691369 put x5

13701370 put x6

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

1372− put x1

1373− put x2

1374− put x3

1375− put x4

1376− put x5

1377− put x6

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

1372+ put x1

1373+ put x2

1374+ put x3

1375+ put x4

1376+ put x5

1377+ put x6

1378+ put x7

13781379 PClauseR x1 x2 x3 x4 -> do putWord8 2

13791380 put x1

13801381 put x2

13811382 put x3

13821383 put x4

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

1384− put x1

1385− put x2

1386− put x3

1387− put x4

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

1385+ put x1

1386+ put x2

1387+ put x3

1388+ put x4

1389+ put x5

13881390 get

13891391 = do i <- getWord8

13901392 case i of

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

14011403 x4 <- get

14021404 x5 <- get

14031405 x6 <- get

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

1406+ x7 <- get

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

14051408 2 -> do x1 <- get

14061409 x2 <- get

14071410 x3 <- get

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

14111414 x2 <- get

14121415 x3 <- get

14131416 x4 <- get

1414− return (PWithR x1 x2 x3 x4)

1417+ x5 <- get

1418+ return (PWithR x1 x2 x3 x4 x5)

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

14161420

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

src/Idris/ParseHelpers.hs+4−4

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

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

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

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

568− | n == n' = clauses j (PWith fc' n' l ws r (collect w) : acc) 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 pn (collect w) : acc) ds

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

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

571571 clauses Nothing acc [] = []

572572

573573 cname :: PDecl -> Maybe Name

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

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

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

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

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

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

578578 fcOf :: PDecl -> FC

579579 fcOf (PClauses fc _ _ _) = fc

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

src/Idris/Parser.hs+12−5

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

826826 popIndent

827827 reserved "with"

828828 wval <- simpleExpr syn

829+ pn <- optProof

829830 openBlock

830831 ds <- some $ fnDecl syn

831832 let withs = concat ds

832833 closeBlock

833− return $ PWithR fc wargs wval withs)

834+ return $ PWithR fc wargs wval pn withs)

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

835836 ty <- simpleExpr syn

836837 symbol "<=="

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

878879 popIndent

879880 reserved "with"

880881 wval <- bracketed syn

882+ pn <- optProof

881883 openBlock

882884 ds <- some $ fnDecl syn

883885 closeBlock

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

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

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

887889 put (ist { lastParse = Just n })

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

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

889891 <|> do pushIndent

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

891893 cargs <- many (constraintArg syn)

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

911913 ist <- get

912914 put (ist { lastParse = Just n })

913915 wval <- bracketed syn

916+ pn <- optProof

914917 openBlock

915918 ds <- some $ fnDecl syn

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

917920 closeBlock

918921 popIndent

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

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

920923 <?> "function clause"

921924 where

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

926+ n <- fnName

927+ return (Just n))

928+

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

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

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

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

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

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

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

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

928935 fillLHS _ _ _ c = c

929936

src/Idris/REPL.hs+3−3

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

756756 getName _ = Nothing

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

758758 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

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

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

762762 elabDecl EAll recinfo tyDecl

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

785785 getClauses _ = []

786786 getRHS :: PClause -> PTerm

787787 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

789789 getRHS (PClauseR fc with rhs whereBlock) = rhs

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

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

791791 setReplDefined :: Maybe Name -> Idris ()

792792 setReplDefined Nothing = return ()

793793 setReplDefined (Just n) = do