21ec023 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge branch 'master' of https://github.com/edwinb/Idris-dev into JavaRepairs

21ec023Jan Bessai13 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/Core/Elaborate.hs+3

@@ -287,6 +287,9 @@ letbind n t v = processTactic' (LetBind n t v)

287rewrite :: Raw -> Elab' aux ()

288rewrite tm = processTactic' (Rewrite tm)

289

290+equiv :: Raw -> Elab' aux ()

291+equiv tm = processTactic' (Equiv tm)

292+

290patvar :: Name -> Elab' aux ()

293patvar :: Name -> Elab' aux ()

291patvar n = do env <- get_env

294patvar n = do env <- get_env

292 if (n `elem` map fst env) then do apply (Var n) []; solve

295 if (n `elem` map fst env) then do apply (Var n) []; solve

src/Core/ProofState.hs+9

@@ -66,6 +66,7 @@ data Tactic = Attack

66 | Forall Name Raw

67 | LetBind Name Raw Raw

68 | Rewrite Raw

69+ | Equiv Raw

69 | PatVar Name

70 | PatVar Name

70 | PatBind Name

71 | PatBind Name

71 | Focus Name

72 | Focus Name

@@ -539,6 +540,13 @@ rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =

539 rname = MN 0 "replaced"

540 rname = MN 0 "replaced"

540rewrite _ _ _ _ = fail "Can't rewrite here"

541rewrite _ _ _ _ = fail "Can't rewrite here"

541

542

543+equiv :: Raw -> RunTactic

544+equiv tm ctxt env (Bind x (Hole t) sc) =

545+ do (tmv, tmt) <- lift $ check ctxt env tm

546+ lift $ converts ctxt env tmv t

547+ return $ Bind x (Hole tmv) sc

548+equiv tm ctxt env _ = fail "Can't equiv here"

549+

542patbind :: Name -> RunTactic

550patbind :: Name -> RunTactic

543patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

551patbind n ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' =

544 do let t' = case t of

552 do let t' = case t of

@@ -724,6 +732,7 @@ process t h = tactic (Just h) (mktac t)

724 mktac (Forall n t) = forall n t

732 mktac (Forall n t) = forall n t

725 mktac (LetBind n t v) = letbind n t v

733 mktac (LetBind n t v) = letbind n t v

726 mktac (Rewrite t) = rewrite t

734 mktac (Rewrite t) = rewrite t

735+ mktac (Equiv t) = equiv t

727 mktac (PatVar n) = patvar n

736 mktac (PatVar n) = patvar n

728 mktac (PatBind n) = patbind n

737 mktac (PatBind n) = patbind n

729 mktac (CheckIn r) = check_in r

738 mktac (CheckIn r) = check_in r

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+14−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)

@@ -557,6 +561,7 @@ mapPT f t = f (mpt t) where

557

561

558data PTactic' t = Intro [Name] | Intros | Focus Name

562data PTactic' t = Intro [Name] | Intros | Focus Name

559 | Refine Name [Bool] | Rewrite t

563 | Refine Name [Bool] | Rewrite t

564+ | Equiv t

560 | MatchRefine Name

565 | MatchRefine Name

561 | LetTac Name t | LetTacTy Name t t

566 | LetTac Name t | LetTacTy Name t t

562 | Exact t | Compute | Trivial

567 | Exact t | Compute | Trivial

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

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

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

965 else

970 else

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

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

967− prettySe p (PRewrite _ l r) =

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

968 bracket p 2 $

973 bracket p 2 $

969 if size r > breakingSize then

974 if size r > breakingSize then

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

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

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

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

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

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

1083 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

1084− 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

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

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

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

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

1087 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 ++ ")"

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

1159 size (PRefl fc _) = 1

1164 size (PRefl fc _) = 1

1160 size (PResolveTC fc) = 1

1165 size (PResolveTC fc) = 1

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

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

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

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

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

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

1164 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

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

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

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

1193 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

1194 ni env (PHidden tm) = ni env tm

1199 ni env (PHidden tm) = ni env tm

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

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

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

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

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

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

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

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

1199 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

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

1217 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

1218 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

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

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

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

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

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

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

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

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

1223 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

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

1242 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

1243 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

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

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

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

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

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

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

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

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

1248 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+30−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")

@@ -769,6 +785,18 @@ runTac autoSolve ist tac

769 _ -> return []

785 _ -> return []

770 runT (Refine fn imps) = do ns <- apply (Var fn) (map (\x -> (x,0)) imps)

786 runT (Refine fn imps) = do ns <- apply (Var fn) (map (\x -> (x,0)) imps)

771 when autoSolve solveAll

787 when autoSolve solveAll

788+ runT (Equiv tm) -- let bind tm, then

789+ = do attack

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

791+ claim tyn RType

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

793+ claim valn (Var tyn)

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

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

796+ focus tyn

797+ elab ist toplevel False False (MN 0 "tac") tm

798+ focus valn

799+ when autoSolve solveAll

772 runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that

800 runT (Rewrite tm) -- to elaborate tm, let bind it, then rewrite by that

773 = do attack; -- (h:_) <- get_holes

801 = do attack; -- (h:_) <- get_holes

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

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

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+8−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)

@@ -1608,6 +1612,9 @@ pTactic syn = do reserved "intro"; ns <- sepBy pName (lchar ',')

1608 <|> do reserved "rewrite"; t <- pExpr syn;

1612 <|> do reserved "rewrite"; t <- pExpr syn;

1609 i <- getState

1613 i <- getState

1610 return $ Rewrite (desugar syn i t)

1614 return $ Rewrite (desugar syn i t)

1615+ <|> do reserved "equiv"; t <- pExpr syn;

1616+ i <- getState

1617+ return $ Equiv (desugar syn i t)

1611 <|> try (do reserved "let"; n <- pName; lchar ':';

1618 <|> try (do reserved "let"; n <- pName; lchar ':';

1612 ty <- pExpr' syn; lchar '='; t <- pExpr syn;

1619 ty <- pExpr' syn; lchar '='; t <- pExpr syn;

1613 i <- getState

1620 i <- getState