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

git.iko.soy/Idris-dev

on master help sign in

Add 'byReflection' tactic

5e7fc5dEdwin Brady13 years ago

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

compare with master

unifiedsplit

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

165move dst_offset src_offset size dst_bounds src_bounds

166 = do src_ptr <- Src :- getRawPtr

167 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

62---- The Effect EDSL itself ----

64-- some proof automation

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

65+

66+%reflection

67+reflectListEffElem : List a -> Tactic

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

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

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

69+reflectListEffElem (x :: xs)

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

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

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

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

70−

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

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

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

74+

75+%reflection

76+reflectSubList : List a -> Tactic

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

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

73−findSubList (S n) ctxt goal

78+reflectSubList (x :: xs)

74− = GoalType "SubList"

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

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

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

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

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

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

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

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

80 List EFFECT

93 List EFFECT

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

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

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

136

149

137implicit

150implicit

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

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

152+ {default tactics { byReflection reflectEff; }

139 prf : SubList ys xs} ->

153 prf : SubList ys xs} ->

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

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

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

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

142

156

143implicit

157implicit

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

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

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

146− prf : EffElem e a xs} ->

147 (eff : e a b t) ->

159 (eff : e a b t) ->

160+ {default tactics { byReflection reflectEff; }

161+ prf : EffElem e a xs} ->

148 EffM m xs (updateResTy xs prf eff) t

162 EffM m xs (updateResTy xs prf eff) t

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

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

150

164

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

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

152

166

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

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

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

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

155

169

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

170syntax 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

158

172

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

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

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

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

161

175

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

176syntax 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

164

178

165-- These may read better in some contexts

179-- These may read better in some contexts

166

180

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

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

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

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

169

183

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

184syntax 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

172

186

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

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

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

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

175

189

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

190syntax 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

178

192

179

193

180-- for 'do' notation

194-- for 'do' notation

src/Idris/AbsSyntaxTree.hs+2−1

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

650 | Try (PTactic' t) (PTactic' t)

651 | TSeq (PTactic' t) (PTactic' t)

652 | ApplyTactic t -- see Language.Reflection module

653+ | ByReflection t

653 | Reflect t

654 | Reflect t

654 | Fill t

655 | Fill t

655 | GoalType String (PTactic' t)

656 | GoalType String (PTactic' t)

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

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

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

742pexp t = PExp 1 False t ""

743pexp t = PExp 1 False t ""

743pconst t = PConstraint 1 False t ""

744pconst 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 ""

745

746

746type PArg = PArg' PTerm

747type PArg = PArg' PTerm

747

748

src/Idris/Completion.hs+1

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

40 , ("exact", Just ExprTArg)

41 , ("equiv", Just ExprTArg)

42 , ("applyTactic", Just ExprTArg)

43+ , ("byReflection", Just ExprTArg)

43 , ("reflect", Just ExprTArg)

44 , ("reflect", Just ExprTArg)

44 , ("fill", Just ExprTArg)

45 , ("fill", Just ExprTArg)

45 , ("try", Just AltsTArg)

46 , ("try", Just AltsTArg)

src/Idris/ElabTerm.hs+31

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

206-- case as' of

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

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

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

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

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

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

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

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

211 showHd x = show x

213 showHd x = show x

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

906 (Pi (RApp listTy envTupleType))

908 (Pi (RApp listTy envTupleType))

907 (RBind (UN "__pi_arg1")

909 (RBind (UN "__pi_arg1")

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

910 (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

909

940

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

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

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

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

src/Idris/IBC.hs+4

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

1608 put x1

1609 Induction x1 -> do putWord8 19

1610 put x1

1611+ ByReflection x1 -> do putWord8 20

1612+ put x1

1611 get

1613 get

1612 = do i <- getWord8

1614 = do i <- getWord8

1613 case i of

1615 case i of

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

1647 return (Fill x1)

1649 return (Fill x1)

1648 19 -> do x1 <- get

1650 19 -> do x1 <- get

1649 return (Induction x1)

1651 return (Induction x1)

1652+ 20 -> do x1 <- get

1653+ return (ByReflection x1)

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

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

1651

1655

1652

1656

src/Idris/ParseExpr.hs+3

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

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

1096 i <- get

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

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

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

1099 i <- get

1102 i <- get

1100 return $ Reflect (desugar syn i t)

1103 return $ Reflect (desugar syn i t)