59f5e64 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #2221 from david-christiansen/wip/tactical

Improvements to elab reflection

commit59f5e64d0121fb68c5c7111f9a0a05c74a0bc18e authorDavid Christiansen <david@davidchristiansen.dk> dateThu 30 Apr 2015, 20:35 (11 years ago) parentcd23076 c69ff4e

9 files changed+76−58

compare with master

unifiedsplit

CHANGELOG+4−2 libs/prelude/IO.idr+29−29 libs/prelude/Language/Reflection/Elab.idr+9 src/IRTS/CodegenC.hs+1−1 src/Idris/Core/Evaluate.hs+5−5 src/Idris/Core/Typecheck.hs+2−2 src/Idris/Elab/Term.hs+15−5 test/meta002/Tacs.idr+10−10 test/reg035/expected+1−4

CHANGELOG+4−2

@@ -32,8 +32,10 @@ New in 0.9.18:

3232* The return types of `Vect.findIndex`, `Vect.elemIndex` and

3333 `Vect.elemIndexBy` were changed from `Maybe Nat` to `Maybe (Fin n)`

3434* A new :browse command shows the contents of a namespace

35−* `{n} is syntax for a quotation of the reflected representation of the global

36− name n, if it is uniquely determined

35+* `{n} is syntax for a quotation of the reflected representation of the name

36+ "n". If "n" is lexically bound, then the resulting quotation will be for it,

37+ whereas if it is not, then it will succeed with a quotation of the unique

38+ global name that matches.

3739

3840New in 0.9.17:

3941--------------

libs/prelude/IO.idr+29−29

@@ -119,35 +119,35 @@ prim_fwrite h s

119119 = MkIO (\w => prim_io_return (prim__writeFile (world w) h s))

120120

121121--------- The C FFI

122−

123−data Raw : Type -> Type where

124− -- code generated can assume it's compiled just as 't'

125− MkRaw : (x : t) -> Raw t

126−

127−-- Tell erasure analysis not to erase the argument

128−%used MkRaw x

129−

130−-- Supported C integer types

131−data C_IntTypes : Type -> Type where

132− C_IntChar : C_IntTypes Char

133− C_IntNative : C_IntTypes Int

134− C_IntBits8 : C_IntTypes Bits8

135− C_IntBits16 : C_IntTypes Bits16

136− C_IntBits32 : C_IntTypes Bits32

137− C_IntBits64 : C_IntTypes Bits64

138−

139−-- Supported C foreign types

140−data C_Types : Type -> Type where

141− C_Str : C_Types String

142− C_Float : C_Types Float

143− C_Ptr : C_Types Ptr

144− C_MPtr : C_Types ManagedPtr

145− C_Unit : C_Types ()

146− C_Any : C_Types (Raw a)

147− C_IntT : C_IntTypes i -> C_Types i

148−

149−FFI_C : FFI

150−FFI_C = MkFFI C_Types String String

122+namespace FFI_C

123+ data Raw : Type -> Type where

124+ -- code generated can assume it's compiled just as 't'

125+ MkRaw : (x : t) -> Raw t

126+

127+ -- Tell erasure analysis not to erase the argument

128+ %used MkRaw x

129+

130+ -- Supported C integer types

131+ data C_IntTypes : Type -> Type where

132+ C_IntChar : C_IntTypes Char

133+ C_IntNative : C_IntTypes Int

134+ C_IntBits8 : C_IntTypes Bits8

135+ C_IntBits16 : C_IntTypes Bits16

136+ C_IntBits32 : C_IntTypes Bits32

137+ C_IntBits64 : C_IntTypes Bits64

138+

139+ -- Supported C foreign types

140+ data C_Types : Type -> Type where

141+ C_Str : C_Types String

142+ C_Float : C_Types Float

143+ C_Ptr : C_Types Ptr

144+ C_MPtr : C_Types ManagedPtr

145+ C_Unit : C_Types ()

146+ C_Any : C_Types (Raw a)

147+ C_IntT : C_IntTypes i -> C_Types i

148+

149+ FFI_C : FFI

150+ FFI_C = MkFFI C_Types String String

151151

152152IO : Type -> Type

153153IO = IO' FFI_C

libs/prelude/Language/Reflection/Elab.idr+9

@@ -57,6 +57,7 @@ data Elab : Type -> Type where

5757

5858 prim__Solve : Elab ()

5959 prim__Fill : Raw -> Elab ()

60+ prim__Apply : Raw -> Elab ()

6061 prim__Focus : TTName -> Elab ()

6162 prim__Unfocus : TTName -> Elab ()

6263 prim__Attack : Elab ()

@@ -69,6 +70,8 @@ data Elab : Type -> Type where

6970 prim__PatVar : TTName -> Elab ()

7071 prim__PatBind : TTName -> Elab ()

7172

73+ prim__Compute : Elab ()

74+

7275 prim__DeclareType : TyDecl -> Elab ()

7376 prim__DefineFunction : FunDefn -> Elab ()

7477

@@ -143,6 +146,10 @@ solve = prim__Solve

143146fill : Raw -> Elab ()

144147fill tm = prim__Fill tm

145148

149+||| Fill with unification

150+apply : Raw -> Elab ()

151+apply tm = prim__Apply tm

152+

146153focus : (hole : TTName) -> Elab ()

147154focus hole = prim__Focus hole

148155

@@ -175,6 +182,8 @@ patvar n = prim__PatVar n

175182patbind : TTName -> Elab ()

176183patbind n = prim__PatBind n

177184

185+compute : Elab ()

186+compute = prim__Compute

178187

179188||| Find out the present source context for the tactic script

180189getSourceLocation : Elab SourceLocation

src/IRTS/CodegenC.hs+1−1

@@ -647,7 +647,7 @@ codegenH es = mapM_ writeIFace es

647647

648648writeIFace :: ExportIFace -> IO ()

649649writeIFace (Export ffic hdr exps)

650− | ffic == sUN "FFI_C"

650+ | ffic == sNS (sUN "FFI_C") ["FFI_C"]

651651 = do let hfile = "#ifndef " ++ hdr_guard hdr ++ "\n" ++

652652 "#define " ++ hdr_guard hdr ++ "\n\n" ++

653653 "#include <idris_rts.h>\n\n" ++

src/Idris/Core/Evaluate.hs+5−5

@@ -1011,12 +1011,12 @@ lookupP = lookupP_all False

10111011

10121012lookupP_all :: Bool -> Name -> Context -> [Term]

10131013lookupP_all all n ctxt

1014− = do def <- lookupCtxt n (definitions ctxt)

1014+ = do (n', def) <- lookupCtxtName n (definitions ctxt)

10151015 p <- case def of

1016− (Function ty tm, a, _, _) -> return (P Ref n ty, a)

1017− (TyDecl nt ty, a, _, _) -> return (P nt n ty, a)

1018− (CaseOp _ ty _ _ _ _, a, _, _) -> return (P Ref n ty, a)

1019− (Operator ty _ _, a, _, _) -> return (P Ref n ty, a)

1016+ (Function ty tm, a, _, _) -> return (P Ref n' ty, a)

1017+ (TyDecl nt ty, a, _, _) -> return (P nt n' ty, a)

1018+ (CaseOp _ ty _ _ _ _, a, _, _) -> return (P Ref n' ty, a)

1019+ (Operator ty _ _, a, _, _) -> return (P Ref n' ty, a)

10201020 case snd p of

10211021 Hidden -> if all then return (fst p) else []

10221022 _ -> return (fst p)

src/Idris/Core/Typecheck.hs+2−2

@@ -86,8 +86,8 @@ check' holes ctxt env top = chk (TType (UVar (-5))) env top where

8686 | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)

8787 -- If we're elaborating, we don't want the private names; if we're

8888 -- checking an already elaborated term, we do

89− | (P nt n' ty : _) <- lookupP_all (not holes) n ctxt

90− = return (P nt n' ty, ty)

89+ | [P nt n' ty] <- lookupP_all (not holes) n ctxt

90+ = return (P nt n' ty, ty)

9191 | otherwise = do lift $ tfail $ NoSuchVariable n

9292 chk u env ap@(RApp f RType) | not holes

9393 -- special case to reduce constraintss

src/Idris/Elab/Term.hs+15−5

@@ -1076,11 +1076,15 @@ elab ist info emode opts fn tm

10761076 elab' ina fc (PUnquote t) = fail "Found unquote outside of quasiquote"

10771077 elab' ina fc (PQuoteName n) =

10781078 do ctxt <- get_context

1079− case lookupNameDef n ctxt of

1080− [(n', _)] -> do fill $ reflectName n'

1081− solve

1082− [] -> lift . tfail . NoSuchVariable $ n

1083− more -> lift . tfail . CantResolveAlts $ map fst more

1079+ env <- get_env

1080+ case lookup n env of

1081+ Just _ -> do fill $ reflectName n ; solve

1082+ Nothing ->

1083+ case lookupNameDef n ctxt of

1084+ [(n', _)] -> do fill $ reflectName n'

1085+ solve

1086+ [] -> lift . tfail . NoSuchVariable $ n

1087+ more -> lift . tfail . CantResolveAlts $ map fst more

10841088 elab' ina fc (PAs _ n t) = lift . tfail . Msg $ "@-pattern not allowed here"

10851089 elab' ina fc (PHidden t)

10861090 | reflection = elab' ina fc t

@@ -1747,6 +1751,10 @@ runTactical fc env tm = do tm' <- eval tm

17471751 alt' <- eval alt

17481752 try' (runTacTm first') (runTacTm alt') True

17491753 | n == tacN "prim__Fill", [raw] <- args

1754+ = do raw' <- reifyRaw =<< eval raw

1755+ fill raw'

1756+ returnUnit

1757+ | n == tacN "prim__Apply", [raw] <- args

17501758 = do raw' <- reifyRaw =<< eval raw

17511759 apply raw' []

17521760 returnUnit

@@ -1799,6 +1807,8 @@ runTactical fc env tm = do tm' <- eval tm

17991807 = do n' <- reifyTTName n

18001808 patbind n'

18011809 returnUnit

1810+ | n == tacN "prim__Compute", [] <- args

1811+ = do compute ; returnUnit

18021812 | n == tacN "prim__DeclareType", [decl] <- args

18031813 = do (RDeclare n args res) <- reifyTyDecl decl

18041814 ctxt <- get_context

test/meta002/Tacs.idr+10−10

@@ -181,7 +181,7 @@ namespace STLC

181181 mkIx : Fin n -> Elab ()

182182 mkIx FZ = do envH <- mkEnvH

183183 tH <- mkTyH

184− fill `(Z {t=~(Var tH)} {env=~(Var envH)})

184+ apply `(Z {t=~(Var tH)} {env=~(Var envH)})

185185 solve

186186 mkIx (FS i) = do envH <- mkEnvH

187187 tH <- mkTyH

@@ -189,7 +189,7 @@ namespace STLC

189189 argH <- gensym "arg"

190190 claim argH `(Ix ~(Var envH) ~(Var tH))

191191 unfocus argH

192− fill `(S {env=~(Var envH)} {t=~(Var tH)} {t'=~(Var vH)} ~(Var argH))

192+ apply `(S {env=~(Var envH)} {t=~(Var tH)} {t'=~(Var vH)} ~(Var argH))

193193 solve

194194 focus argH

195195 mkIx i

@@ -200,9 +200,9 @@ namespace STLC

200200 tH' <- mkTyH

201201 bodyH <- gensym "body"

202202 claim bodyH `(Tm ((::) ~(Var tH) ~(Var envH)) ~(Var tH'))

203− fill `(Lam {env=~(Var envH)}

204− {t=~(Var tH)} {t'=~(Var tH')}

205− ~(Var bodyH))

203+ apply `(Lam {env=~(Var envH)}

204+ {t=~(Var tH)} {t'=~(Var tH')}

205+ ~(Var bodyH))

206206

207207 solve

208208 focus bodyH

@@ -216,9 +216,9 @@ namespace STLC

216216 argH <- gensym "arg"

217217 claim argH `(Tm ~(Var envH) ~(Var tH))

218218 unfocus argH

219− fill `(App {env=~(Var envH)}

220− {t=~(Var tH)} {t'=~(Var tH')}

221− ~(Var fH) ~(Var argH))

219+ apply `(App {env=~(Var envH)}

220+ {t=~(Var tH)} {t'=~(Var tH')}

221+ ~(Var fH) ~(Var argH))

222222 solve

223223 focus fH

224224 mkTerm xs tm

@@ -229,12 +229,12 @@ namespace STLC

229229 ixH <- gensym "ix"

230230 claim ixH `(Ix ~(Var envH) ~(Var tH))

231231 unfocus ixH

232− fill `(Var {env=~(Var envH)} {t=~(Var tH)} ~(Var ixH))

232+ apply `(Var {env=~(Var envH)} {t=~(Var tH)} ~(Var ixH))

233233 solve

234234 focus ixH

235235 mkIx i

236236 mkTerm xs UnitCon = do envH <- mkEnvH

237− fill `(UnitCon {env=~(Var envH)})

237+ apply `(UnitCon {env=~(Var envH)})

238238 solve

239239 testElab : Sigma Ty (Tm [])

240240 testElab = %runElab (elaborateSTLC (App (Lam "x" UnitCon) UnitCon))

test/reg035/expected+1−4

@@ -1,4 +1 @@

1−reg035b.idr:8:6:Can't convert

2− Additive -> Nat

3−with

4− Fin 0

1+reg035b.idr:8:6:No such variable __pi_arg