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

lib/Language/Reflection.idr+2

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

11module Language.Reflection

22

3+import Prelude.Vect

4+

35%access public

46

57data TTName = UN String

src/Core/Elaborate.hs+3

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

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

288288rewrite tm = processTactic' (Rewrite tm)

289289

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

291+equiv tm = processTactic' (Equiv tm)

292+

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

291294patvar n = do env <- get_env

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

src/Core/ProofState.hs+9

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

6666 | Forall Name Raw

6767 | LetBind Name Raw Raw

6868 | Rewrite Raw

69+ | Equiv Raw

6970 | PatVar Name

7071 | PatBind Name

7172 | Focus Name

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

539540 rname = MN 0 "replaced"

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

541542

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+

542550patbind :: Name -> RunTactic

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

544552 do let t' = case t of

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

724732 mktac (Forall n t) = forall n t

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

726734 mktac (Rewrite t) = rewrite t

735+ mktac (Equiv t) = equiv t

727736 mktac (PatVar n) = patvar n

728737 mktac (PatBind n) = patbind n

729738 mktac (CheckIn r) = check_in r

src/Idris/AbsSyntax.hs+11−9

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

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

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

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

602602 en (PTyped l r) = PTyped (en l) (en r)

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

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

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

735735 pri (PFalse _) = 0

736736 pri (PRefl _ _) = 1

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

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

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

741741 pri (PTyped l r) = pri l

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

892892 = do (decls, ns) <- get

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

894894 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 _)

896896 = do (decls, ns) <- get

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

898898 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

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

957957 r' = ai env r in

958958 PEq fc l' r'

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

960− r' = ai env r in

961− PRewrite fc l' r'

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

960+ r' = ai env r

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

962+ PRewrite fc l' r' g'

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

963964 r' = ai env r in

964965 PTyped l' r'

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

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

12211222 mr <- match' r r'

12221223 return (ml ++ mr)

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

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

12241225 = do ml <- match' l l'

12251226 mr <- match' r r'

12261227 return (ml ++ mr)

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

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

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

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

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

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

13131315 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

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

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

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

13281330 sm (PTyped x y) = PTyped (sm x) (sm y)

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

13301332 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

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

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

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

378− deriving Functor

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

379+ t -- type of variables

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

381+ deriving Functor

379382{-!

380383deriving instance Binary PDecl'

381384!-}

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

511514 | PRefl FC PTerm

512515 | PResolveTC FC

513516 | PEq FC PTerm PTerm

514− | PRewrite FC PTerm PTerm

517+ | PRewrite FC PTerm PTerm (Maybe PTerm)

515518 | PPair FC PTerm PTerm

516519 | PDPair FC PTerm PTerm PTerm

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

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

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

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

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

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

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

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

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

557561

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

559563 | Refine Name [Bool] | Rewrite t

564+ | Equiv t

560565 | MatchRefine Name

561566 | LetTac Name t | LetTacTy Name t t

562567 | Exact t | Compute | Trivial

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

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

965970 else

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

967− prettySe p (PRewrite _ l r) =

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

968973 bracket p 2 $

969974 if size r > breakingSize then

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

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

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

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

10831088 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

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

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

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

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

11591164 size (PRefl fc _) = 1

11601165 size (PResolveTC fc) = 1

11611166 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

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

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

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

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

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

11941199 ni env (PHidden tm) = ni env tm

11951200 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

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

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

11991204 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

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

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

12191224 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

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

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

12231228 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

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

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

12441249 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

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

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

12481253 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

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

421421 | otherwise = elab' ina Placeholder

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

423− elab' ina (PRewrite fc r sc)

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

424424 = do attack

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

426426 claim tyn RType

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

435435 rewrite (Var letn)

436436 g' <- goal

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

438− elab' ina sc

438+ case newg of

439+ Nothing -> elab' ina sc

440+ Just t -> doEquiv t sc

439441 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

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

441457 = do attack

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

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

769785 _ -> return []

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

771787 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

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

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

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

src/Idris/IBC.hs+17−5

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

10371037 put x4

10381038 put x5

10391039 put x6

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

1041+ put x1

1042+ put x2

1043+ put x3

1044+ put x4

10401045 get

10411046 = do i <- getWord8

10421047 case i of

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

11121117 x5 <- get

11131118 x6 <- get

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

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

11161126

11171127instance Binary Using where

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

13061316 PInferRef x1 x2 -> do putWord8 29

13071317 put x1

13081318 put x2

1309− PRewrite x1 x2 x3 -> do putWord8 30

1310− put x1

1311− put x2

1312− put x3

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

1320+ put x1

1321+ put x2

1322+ put x3

1323+ put x4

13131324 get

13141325 = do i <- getWord8

13151326 case i of

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

13971408 30 -> do x1 <- get

13981409 x2 <- get

13991410 x3 <- get

1400− return (PRewrite x1 x2 x3)

1411+ x4 <- get

1412+ return (PRewrite x1 x2 x3 x4)

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

14021414

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

src/Idris/Parser.hs+8−1

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

974974 do reserved "rewrite"

975975 fc <- pfc

976976 prf <- pExpr syn

977+ giving <- option Nothing

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

979+ return (Just tm))

977980 reserved "in"; sc <- pExpr syn

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

980984

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

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

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

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

16091613 i <- getState

16101614 return $ Rewrite (desugar syn i t)

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

1616+ i <- getState

1617+ return $ Equiv (desugar syn i t)

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

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

16131620 i <- getState