5e7fc5d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add 'byReflection' tactic

Similar to 'applyTactic', but its argument is a reflection function which builds a tactic by reflection on the goal.

commit5e7fc5db1533e2fc4ab39ccaf268a2c14f1ad73f authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 22 Dec 2013, 01:39 (13 years ago) parentdc64734

7 files changed+84−29

compare with master

unifiedsplit

libs/effects/Effect/Memory.idr+2−1 libs/effects/Effects.idr+41−27 src/Idris/AbsSyntaxTree.hs+2−1 src/Idris/Completion.hs+1 src/Idris/ElabTerm.hs+31 src/Idris/IBC.hs+4 src/Idris/ParseExpr.hs+3

libs/effects/Effect/Memory.idr+2−1

@@ -165,4 +165,5 @@ move : {dst_size : Nat} ->

165165move dst_offset src_offset size dst_bounds src_bounds

166166 = do src_ptr <- Src :- getRawPtr

167167 Dst :- move' src_ptr dst_offset src_offset size dst_bounds src_bounds

168− return ()

168+ return ()

169+

libs/effects/Effects.idr+41−27

@@ -62,19 +62,32 @@ rebuildEnv (x :: xs) SubNil [] = x :: xs

6262---- The Effect EDSL itself ----

6363

6464-- some proof automation

65−findEffElem : Nat -> List (TTName, Binder TT) -> TT -> Tactic -- Nat is maximum search depth

66−findEffElem Z ctxt goal = Refine "Here" `Seq` Solve

67−findEffElem (S n) ctxt goal = GoalType "EffElem"

68− (Try (Refine "Here" `Seq` Solve)

69− (Refine "There" `Seq` (Solve `Seq` findEffElem n ctxt goal)))

70−

71−findSubList : Nat -> List (TTName, Binder TT) -> TT -> Tactic

72−findSubList Z ctxt goal = Refine "SubNil" `Seq` Solve

73−findSubList (S n) ctxt goal

74− = GoalType "SubList"

75− (Try (Refine "subListId" `Seq` Solve)

76− ((Try (Refine "Keep" `Seq` Solve)

77− (Refine "Drop" `Seq` Solve)) `Seq` findSubList n ctxt goal))

65+

66+%reflection

67+reflectListEffElem : List a -> Tactic

68+reflectListEffElem [] = Refine "Here" `Seq` Solve

69+reflectListEffElem (x :: xs)

70+ = Try (Refine "Here" `Seq` Solve)

71+ (Refine "There" `Seq` (Solve `Seq` reflectListEffElem xs))

72+reflectListEffElem (x ++ y) = Refine "Here" `Seq` Solve

73+reflectListEffElem _ = Refine "Here" `Seq` Solve

74+

75+%reflection

76+reflectSubList : List a -> Tactic

77+reflectSubList [] = Refine "SubNil" `Seq` Solve

78+reflectSubList (x :: xs)

79+ = Try (Refine "subListId" `Seq` Solve)

80+ (Try (Refine "Keep" `Seq` (Solve `Seq` reflectSubList xs))

81+ (Refine "Drop" `Seq` (Solve `Seq` reflectSubList xs)))

82+reflectSubList (x ++ y) = Refine "subListId" `Seq` Solve

83+reflectSubList _ = Refine "subListId" `Seq` Solve

84+

85+%reflection

86+reflectEff : (P : Type) -> Tactic

87+reflectEff (EffElem m a xs)

88+ = reflectListEffElem xs `Seq` Solve

89+reflectEff (SubList xs ys)

90+ = reflectSubList ys `Seq` Solve

7891

7992updateResTy : (xs : List EFFECT) -> EffElem e a xs -> e a b t ->

8093 List EFFECT

@@ -135,46 +148,47 @@ syntax [tag] ":!" [val] = !(tag :- val)

135148-- Eff : List (EFFECT m) -> Type -> Type

136149

137150implicit

138−lift' : {default tactics { applyTactic findSubList 20; solve; }

151+lift' : EffM m ys ys' t ->

152+ {default tactics { byReflection reflectEff; }

139153 prf : SubList ys xs} ->

140− EffM m ys ys' t -> EffM m xs (updateWith ys' xs prf) t

141−lift' {prf} e = lift prf e

154+ EffM m xs (updateWith ys' xs prf) t

155+lift' e {prf} = lift prf e

142156

143157implicit

144158effect' : {a, b: _} -> {e : Effect} ->

145− {default tactics { applyTactic findEffElem 20; solve; }

146− prf : EffElem e a xs} ->

147159 (eff : e a b t) ->

160+ {default tactics { byReflection reflectEff; }

161+ prf : EffElem e a xs} ->

148162 EffM m xs (updateResTy xs prf eff) t

149−effect' {prf} e = effect prf e

163+effect' e {prf} = effect prf e

150164

151165-- For making proofs implicitly for 'test' and 'test_lbl'

152166

153167syntax if_valid then [e] else [t] =

154− test (tactics { applyTactic findEffElem 20; solve; }) t e

168+ test (tactics { byReflection reflectEff; }) t e

155169

156170syntax if_valid [lbl] then [e] else [t] =

157− test_lbl {x=lbl} (tactics { applyTactic findEffElem 20; solve; }) t e

171+ test_lbl {x=lbl} (tactics { byReflection reflectEff; }) t e

158172

159173syntax if_error then [t] else [e] =

160− test (tactics { applyTactic findEffElem 20; solve; }) t e

174+ test (tactics { byReflection reflectEff; }) t e

161175

162176syntax if_error [lbl] then [t] else [e] =

163− test_lbl {x=lbl} (tactics { applyTactic findEffElem 20; solve; }) t e

177+ test_lbl {x=lbl} (tactics { byReflection reflectEff; }) t e

164178

165179-- These may read better in some contexts

166180

167181syntax if_right then [e] else [t] =

168− test (tactics { applyTactic findEffElem 20; solve; }) t e

182+ test (tactics { byReflection reflectEff; }) t e

169183

170184syntax if_right [lbl] then [e] else [t] =

171− test_lbl {x=lbl} (tactics { applyTactic findEffElem 20; solve; }) t e

185+ test_lbl {x=lbl} (tactics { byReflection reflectEff; }) t e

172186

173187syntax if_left then [t] else [e] =

174− test (tactics { applyTactic findEffElem 20; solve; }) t e

188+ test (tactics { byReflection reflectEff; }) t e

175189

176190syntax if_left [lbl] then [t] else [e] =

177− test_lbl {x=lbl} (tactics { applyTactic findEffElem 20; solve; }) t e

191+ test_lbl {x=lbl} (tactics { byReflection reflectEff; }) t e

178192

179193

180194-- for 'do' notation

src/Idris/AbsSyntaxTree.hs+2−1

@@ -650,6 +650,7 @@ data PTactic' t = Intro [Name] | Intros | Focus Name

650650 | Try (PTactic' t) (PTactic' t)

651651 | TSeq (PTactic' t) (PTactic' t)

652652 | ApplyTactic t -- see Language.Reflection module

653+ | ByReflection t

653654 | Reflect t

654655 | Fill t

655656 | GoalType String (PTactic' t)

@@ -741,7 +742,7 @@ deriving instance NFData PArg'

741742pimp n t mach = PImp 1 mach True n t ""

742743pexp t = PExp 1 False t ""

743744pconst t = PConstraint 1 False t ""

744−ptacimp n s t = PTacImplicit 0 True n s t ""

745+ptacimp n s t = PTacImplicit 2 True n s t ""

745746

746747type PArg = PArg' PTerm

747748

src/Idris/Completion.hs+1

@@ -40,6 +40,7 @@ tacticArgs = [ ("intro", Nothing) -- FIXME syntax for intro (fresh name)

4040 , ("exact", Just ExprTArg)

4141 , ("equiv", Just ExprTArg)

4242 , ("applyTactic", Just ExprTArg)

43+ , ("byReflection", Just ExprTArg)

4344 , ("reflect", Just ExprTArg)

4445 , ("fill", Just ExprTArg)

4546 , ("try", Just AltsTArg)

src/Idris/ElabTerm.hs+31

@@ -206,6 +206,8 @@ elab ist info pattern tcgen fn tm

206206-- case as' of

207207-- [a] -> elab' ina a

208208-- as -> lift $ tfail $ CantResolveAlts (map showHd as)

209+-- trace ("Original " ++ show (length as, as) ++ "\n" ++

210+-- "New " ++ show (length as', as)) $

209211 tryAll (zip (map (elab' ina) as') (map showHd as'))

210212 where showHd (PApp _ h _) = show h

211213 showHd x = show x

@@ -906,6 +908,35 @@ runTac autoSolve ist tac

906908 (Pi (RApp listTy envTupleType))

907909 (RBind (UN "__pi_arg1")

908910 (Pi (Var $ reflm "TT")) tacticTy))

911+ runT (ByReflection tm) -- run the reflection function 'tm' on the

912+ -- goal, then apply the resulting reflected Tactic

913+ = do tgoal <- goal

914+ attack

915+ script <- unique_hole (MN 0 "script")

916+ claim script scriptTy

917+ scriptvar <- unique_hole (MN 0 "scriptvar" )

918+ letbind scriptvar scriptTy (Var script)

919+ focus script

920+ ptm <- get_term

921+ elab ist toplevel False False (MN 0 "tac")

922+ (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True)])

923+ (script', _) <- get_type_val (Var scriptvar)

924+ -- now that we have the script apply

925+ -- it to the reflected goal

926+ restac <- unique_hole (MN 0 "restac")

927+ claim restac tacticTy

928+ focus restac

929+ fill (forget script')

930+ restac' <- get_guess

931+ solve

932+ -- normalise the result in order to

933+ -- reify it

934+ ctxt <- get_context

935+ env <- get_env

936+ let tactic = normalise ctxt env restac'

937+ runReflected tactic

938+ where tacticTy = Var (reflm "Tactic")

939+ scriptTy = tacticTy

909940

910941 runT (Reflect v) = do attack -- let x = reflect v in ...

911942 tyn <- unique_hole (MN 0 "letty")

src/Idris/IBC.hs+4

@@ -1608,6 +1608,8 @@ instance (Binary t) => Binary (PTactic' t) where

16081608 put x1

16091609 Induction x1 -> do putWord8 19

16101610 put x1

1611+ ByReflection x1 -> do putWord8 20

1612+ put x1

16111613 get

16121614 = do i <- getWord8

16131615 case i of

@@ -1647,6 +1649,8 @@ instance (Binary t) => Binary (PTactic' t) where

16471649 return (Fill x1)

16481650 19 -> do x1 <- get

16491651 return (Induction x1)

1652+ 20 -> do x1 <- get

1653+ return (ByReflection x1)

16501654 _ -> error "Corrupted binary data for PTactic'"

16511655

16521656

src/Idris/ParseExpr.hs+3

@@ -1095,6 +1095,9 @@ tactic syn = do reserved "intro"; ns <- sepBy (indentPropHolds gtProp *> name) (

10951095 <|> do reserved "applyTactic"; t <- (indentPropHolds gtProp *> expr syn);

10961096 i <- get

10971097 return $ ApplyTactic (desugar syn i t)

1098+ <|> do reserved "byReflection"; t <- (indentPropHolds gtProp *> expr syn);

1099+ i <- get

1100+ return $ ByReflection (desugar syn i t)

10981101 <|> do reserved "reflect"; t <- (indentPropHolds gtProp *> expr syn);

10991102 i <- get

11001103 return $ Reflect (desugar syn i t)