7fc4865 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Allow 'rewrite ... in' to assert the resulting type

7fc4865Edwin Brady13 years ago

lib/Language/Reflection.idr+2

compare with master

unifiedsplit

@@ -1,5 +1,7 @@

1module Language.Reflection

3+import Prelude.Vect

3%access public

5%access public

5data TTName = UN String

7data TTName = UN String

src/Idris/AbsSyntax.hs+11−9

@@ -598,7 +598,7 @@ expandParams dec ps ns infs tm = en tm

598 PLet n' (en ty) (en v) (en (shadow n n' s))

599 | otherwise = PLet n (en ty) (en v) (en s)

600 en (PEq f l r) = PEq f (en l) (en r)

601− en (PRewrite f l r) = PRewrite f (en l) (en r)

601+ en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)

602 en (PTyped l r) = PTyped (en l) (en r)

603 en (PPair f l r) = PPair f (en l) (en r)

604 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)

@@ -735,7 +735,7 @@ getPriority i tm = 1 -- pri tm

735 pri (PFalse _) = 0

736 pri (PRefl _ _) = 1

737 pri (PEq _ l r) = max 1 (max (pri l) (pri r))

738− pri (PRewrite _ l r) = max 1 (max (pri l) (pri r))

738+ pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))

739 pri (PApp _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.getTm) as)))

740 pri (PCase _ f as) = max 1 (max (pri f) (foldr max 0 (map (pri.snd) as)))

741 pri (PTyped l r) = pri l

@@ -892,7 +892,7 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

892 = do (decls, ns) <- get

893 let isn = namesIn uvars ist l ++ namesIn uvars ist r

894 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

895− imps top env (PRewrite _ l r)

895+ imps top env (PRewrite _ l r _)

896 = do (decls, ns) <- get

897 let isn = namesIn uvars ist l ++ namesIn uvars ist r

898 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

@@ -956,9 +956,10 @@ addImpl' inpat env infns ist ptm = ai (zip env (repeat Nothing)) ptm

956 ai env (PEq fc l r) = let l' = ai env l

957 r' = ai env r in

958 PEq fc l' r'

959− ai env (PRewrite fc l r) = let l' = ai env l

959+ ai env (PRewrite fc l r g) = let l' = ai env l

960− r' = ai env r in

960+ r' = ai env r

961+ g' = fmap (ai env) g in

961− PRewrite fc l' r'

962+ PRewrite fc l' r' g'

962 ai env (PTyped l r) = let l' = ai env l

963 ai env (PTyped l r) = let l' = ai env l

963 r' = ai env r in

964 r' = ai env r in

964 PTyped l' r'

965 PTyped l' r'

@@ -1220,7 +1221,7 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

1220 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'

1221 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'

1221 mr <- match' r r'

1222 mr <- match' r r'

1222 return (ml ++ mr)

1223 return (ml ++ mr)

1223− match (PRewrite _ l r) (PRewrite _ l' r')

1224+ match (PRewrite _ l r _) (PRewrite _ l' r' _)

1224 = do ml <- match' l l'

1225 = do ml <- match' l l'

1225 mr <- match' r r'

1226 mr <- match' r r'

1226 return (ml ++ mr)

1227 return (ml ++ mr)

@@ -1307,7 +1308,8 @@ substMatchShadow n shs tm t = sm shs t where

1307 sm xs (PApp f x as) = PApp f (sm xs x) (map (fmap (sm xs)) as)

1308 sm xs (PApp f x as) = PApp f (sm xs x) (map (fmap (sm xs)) as)

1308 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)

1309 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)

1309 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)

1310 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)

1310− sm xs (PRewrite f x y) = PRewrite f (sm xs x) (sm xs y)

1311+ sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)

1312+ (fmap (sm xs) tm)

1311 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)

1313 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)

1312 sm xs (PPair f x y) = PPair f (sm xs x) (sm xs y)

1314 sm xs (PPair f x y) = PPair f (sm xs x) (sm xs y)

1313 sm xs (PDPair f x t y) = PDPair f (sm xs x) (sm xs t) (sm xs y)

1315 sm xs (PDPair f x t y) = PDPair f (sm xs x) (sm xs t) (sm xs y)

@@ -1324,7 +1326,7 @@ shadow n n' t = sm t where

1324 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)

1326 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)

1325 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)

1327 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)

1326 sm (PEq f x y) = PEq f (sm x) (sm y)

1328 sm (PEq f x y) = PEq f (sm x) (sm y)

1327− sm (PRewrite f x y) = PRewrite f (sm x) (sm y)

1329+ sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)

1328 sm (PTyped x y) = PTyped (sm x) (sm y)

1330 sm (PTyped x y) = PTyped (sm x) (sm y)

1329 sm (PPair f x y) = PPair f (sm x) (sm y)

1331 sm (PPair f x y) = PPair f (sm x) (sm y)

1330 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)

1332 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)

src/Idris/AbsSyntaxTree.hs+13−9

@@ -375,7 +375,10 @@ data PDecl' t

375 | PMutual FC [PDecl' t] -- ^ Mutual block

376 | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.

377 | PProvider SyntaxInfo FC Name t t -- ^ Type provider. The first t is the type, the second is the term

378+ | PReflection FC Name -- type to reflect to

379+ t -- type of variables

380+ [PClause' t] -- ^ Pattern clauses

378− deriving Functor

381+ deriving Functor

379{-!

382{-!

380deriving instance Binary PDecl'

383deriving instance Binary PDecl'

381!-}

384!-}

@@ -511,7 +514,7 @@ data PTerm = PQuote Raw

511 | PRefl FC PTerm

514 | PRefl FC PTerm

512 | PResolveTC FC

515 | PResolveTC FC

513 | PEq FC PTerm PTerm

516 | PEq FC PTerm PTerm

514− | PRewrite FC PTerm PTerm

517+ | PRewrite FC PTerm PTerm (Maybe PTerm)

515 | PPair FC PTerm PTerm

518 | PPair FC PTerm PTerm

516 | PDPair FC PTerm PTerm PTerm

519 | PDPair FC PTerm PTerm PTerm

517 | PAlternative Bool [PTerm] -- True if only one may work

520 | PAlternative Bool [PTerm] -- True if only one may work

@@ -539,7 +542,8 @@ mapPT f t = f (mpt t) where

539 mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)

542 mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)

540 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)

543 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)

541 mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)

544 mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)

542− mpt (PRewrite fc t s) = PRewrite fc (mapPT f t) (mapPT f s)

545+ mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)

546+ (fmap (mapPT f) g)

543 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)

547 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)

544 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)

548 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)

545 mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)

549 mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)

@@ -965,7 +969,7 @@ prettyImp impl = prettySe 10

965 prettySe 10 l <+> text "=" $$ nest nestingSize (prettySe 10 r)

969 prettySe 10 l <+> text "=" $$ nest nestingSize (prettySe 10 r)

966 else

970 else

967 prettySe 10 l <+> text "=" <+> prettySe 10 r

971 prettySe 10 l <+> text "=" <+> prettySe 10 r

968− prettySe p (PRewrite _ l r) =

972+ prettySe p (PRewrite _ l r _) =

969 bracket p 2 $

973 bracket p 2 $

970 if size r > breakingSize then

974 if size r > breakingSize then

971 text "rewrite" <+> prettySe 10 l <+> text "in" $$ nest nestingSize (prettySe 10 r)

975 text "rewrite" <+> prettySe 10 l <+> text "in" $$ nest nestingSize (prettySe 10 r)

@@ -1082,7 +1086,7 @@ showImp impl tm = se 10 tm where

1082 se p (PTrue _) = "()"

1086 se p (PTrue _) = "()"

1083 se p (PFalse _) = "_|_"

1087 se p (PFalse _) = "_|_"

1084 se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r

1088 se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r

1085− se p (PRewrite _ l r) = bracket p 2 $ "rewrite " ++ se 10 l ++ " in " ++ se 10 r

1089+ se p (PRewrite _ l r _) = bracket p 2 $ "rewrite " ++ se 10 l ++ " in " ++ se 10 r

1086 se p (PTyped l r) = "(" ++ se 10 l ++ " : " ++ se 10 r ++ ")"

1090 se p (PTyped l r) = "(" ++ se 10 l ++ " : " ++ se 10 r ++ ")"

1087 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"

1091 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"

1088 se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"

1092 se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"

@@ -1160,7 +1164,7 @@ instance Sized PTerm where

1160 size (PRefl fc _) = 1

1164 size (PRefl fc _) = 1

1161 size (PResolveTC fc) = 1

1165 size (PResolveTC fc) = 1

1162 size (PEq fc left right) = 1 + size left + size right

1166 size (PEq fc left right) = 1 + size left + size right

1163− size (PRewrite fc left right) = 1 + size left + size right

1167+ size (PRewrite fc left right _) = 1 + size left + size right

1164 size (PPair fc left right) = 1 + size left + size right

1168 size (PPair fc left right) = 1 + size left + size right

1165 size (PDPair fs left ty right) = 1 + size left + size ty + size right

1169 size (PDPair fs left ty right) = 1 + size left + size ty + size right

1166 size (PAlternative a alts) = 1 + size alts

1170 size (PAlternative a alts) = 1 + size alts

@@ -1194,7 +1198,7 @@ allNamesIn tm = nub $ ni [] tm

1194 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

1198 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

1195 ni env (PHidden tm) = ni env tm

1199 ni env (PHidden tm) = ni env tm

1196 ni env (PEq _ l r) = ni env l ++ ni env r

1200 ni env (PEq _ l r) = ni env l ++ ni env r

1197− ni env (PRewrite _ l r) = ni env l ++ ni env r

1201+ ni env (PRewrite _ l r _) = ni env l ++ ni env r

1198 ni env (PTyped l r) = ni env l ++ ni env r

1202 ni env (PTyped l r) = ni env l ++ ni env r

1199 ni env (PPair _ l r) = ni env l ++ ni env r

1203 ni env (PPair _ l r) = ni env l ++ ni env r

1200 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r

1204 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r

@@ -1218,7 +1222,7 @@ namesIn uvars ist tm = nub $ ni [] tm

1218 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1222 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1219 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

1223 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

1220 ni env (PEq _ l r) = ni env l ++ ni env r

1224 ni env (PEq _ l r) = ni env l ++ ni env r

1221− ni env (PRewrite _ l r) = ni env l ++ ni env r

1225+ ni env (PRewrite _ l r _) = ni env l ++ ni env r

1222 ni env (PTyped l r) = ni env l ++ ni env r

1226 ni env (PTyped l r) = ni env l ++ ni env r

1223 ni env (PPair _ l r) = ni env l ++ ni env r

1227 ni env (PPair _ l r) = ni env l ++ ni env r

1224 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r

1228 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r

@@ -1243,7 +1247,7 @@ usedNamesIn vars ist tm = nub $ ni [] tm

1243 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1247 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1244 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

1248 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

1245 ni env (PEq _ l r) = ni env l ++ ni env r

1249 ni env (PEq _ l r) = ni env l ++ ni env r

1246− ni env (PRewrite _ l r) = ni env l ++ ni env r

1250+ ni env (PRewrite _ l r _) = ni env l ++ ni env r

1247 ni env (PTyped l r) = ni env l ++ ni env r

1251 ni env (PTyped l r) = ni env l ++ ni env r

1248 ni env (PPair _ l r) = ni env l ++ ni env r

1252 ni env (PPair _ l r) = ni env l ++ ni env r

1249 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r

1253 ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r

src/Idris/ElabTerm.hs+18−2

@@ -420,7 +420,7 @@ elab ist info pattern tcgen fn tm

420 | not pattern = do mapM_ (runTac False ist) ts

421 | otherwise = elab' ina Placeholder

422 elab' ina (PElabError e) = fail (pshow ist e)

423− elab' ina (PRewrite fc r sc)

423+ elab' ina (PRewrite fc r sc newg)

424 = do attack

425 tyn <- unique_hole (MN 0 "rty")

426 claim tyn RType

@@ -435,8 +435,24 @@ elab ist info pattern tcgen fn tm

435 rewrite (Var letn)

436 g' <- goal

437 when (g == g') $ lift $ tfail (NoRewriting g)

438+ case newg of

438− elab' ina sc

439+ Nothing -> elab' ina sc

440+ Just t -> doEquiv t sc

439 solve

441 solve

442+ where doEquiv t sc =

443+ do attack

444+ tyn <- unique_hole (MN 0 "ety")

445+ claim tyn RType

446+ valn <- unique_hole (MN 0 "eqval")

447+ claim valn (Var tyn)

448+ letn <- unique_hole (MN 0 "equiv_val")

449+ letbind letn (Var tyn) (Var valn)

450+ focus tyn

451+ elab' ina t

452+ focus valn

453+ elab' ina sc

454+ elab' ina (PRef fc letn)

455+ solve

440 elab' ina@(_, a) c@(PCase fc scr opts)

456 elab' ina@(_, a) c@(PCase fc scr opts)

441 = do attack

457 = do attack

442 tyn <- unique_hole (MN 0 "scty")

458 tyn <- unique_hole (MN 0 "scty")

src/Idris/IBC.hs+17−5

@@ -1037,6 +1037,11 @@ instance (Binary t) => Binary (PDecl' t) where

1037 put x4

1038 put x5

1039 put x6

1040+ PReflection x1 x2 x3 x4 -> do putWord8 13

1041+ put x1

1042+ put x2

1043+ put x3

1044+ put x4

1040 get

1045 get

1041 = do i <- getWord8

1046 = do i <- getWord8

1042 case i of

1047 case i of

@@ -1112,6 +1117,11 @@ instance (Binary t) => Binary (PDecl' t) where

1112 x5 <- get

1117 x5 <- get

1113 x6 <- get

1118 x6 <- get

1114 return (PPostulate x1 x2 x3 x4 x5 x6)

1119 return (PPostulate x1 x2 x3 x4 x5 x6)

1120+ 13 -> do x1 <- get

1121+ x2 <- get

1122+ x3 <- get

1123+ x4 <- get

1124+ return (PReflection x1 x2 x3 x4)

1115 _ -> error "Corrupted binary data for PDecl'"

1125 _ -> error "Corrupted binary data for PDecl'"

1116

1126

1117instance Binary Using where

1127instance Binary Using where

@@ -1306,10 +1316,11 @@ instance Binary PTerm where

1306 PInferRef x1 x2 -> do putWord8 29

1316 PInferRef x1 x2 -> do putWord8 29

1307 put x1

1317 put x1

1308 put x2

1318 put x2

1309− PRewrite x1 x2 x3 -> do putWord8 30

1319+ PRewrite x1 x2 x3 x4 -> do putWord8 30

1310− put x1

1320+ put x1

1311− put x2

1321+ put x2

1312− put x3

1322+ put x3

1323+ put x4

1313 get

1324 get

1314 = do i <- getWord8

1325 = do i <- getWord8

1315 case i of

1326 case i of

@@ -1397,7 +1408,8 @@ instance Binary PTerm where

1397 30 -> do x1 <- get

1408 30 -> do x1 <- get

1398 x2 <- get

1409 x2 <- get

1399 x3 <- get

1410 x3 <- get

1411+ x4 <- get

1400− return (PRewrite x1 x2 x3)

1412+ return (PRewrite x1 x2 x3 x4)

1401 _ -> error "Corrupted binary data for PTerm"

1413 _ -> error "Corrupted binary data for PTerm"

1402

1414

1403instance (Binary t) => Binary (PTactic' t) where

1415instance (Binary t) => Binary (PTactic' t) where

src/Idris/Parser.hs+5−1

@@ -974,9 +974,13 @@ pRewriteTerm syn =

974 do reserved "rewrite"

975 fc <- pfc

976 prf <- pExpr syn

977+ giving <- option Nothing

978+ (do symbol "==>"; tm <- pExpr' syn

979+ return (Just tm))

977 reserved "in"; sc <- pExpr syn

980 reserved "in"; sc <- pExpr syn

978 return (PRewrite fc

981 return (PRewrite fc

979− (PApp fc (PRef fc (UN "sym")) [pexp prf]) sc)

982+ (PApp fc (PRef fc (UN "sym")) [pexp prf]) sc

983+ giving)

980

984

981pLet syn = try (do reserved "let"; n <- pName;

985pLet syn = try (do reserved "let"; n <- pName;

982 ty <- option Placeholder (do lchar ':'; pExpr' syn)

986 ty <- option Placeholder (do lchar ':'; pExpr' syn)