f09605b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Require unique global names in TT

Fixes #2217 by demanding that global names in TT terms be unambiguous. The elaborator will always produce them that way, but user elab scripts might not, which led to confusion. Also, disentagle 'apply' and 'fill'.

commitf09605b3ddec944b0fab9a66bd5d68dfdba8db77 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 30 Apr 2015, 12:40 (11 years ago) parenta244cd5

8 files changed+57−51

compare with master

unifiedsplit

libs/prelude/IO.idr+29−29 libs/prelude/Language/Reflection/Elab.idr+5 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+4 test/meta002/Tacs.idr+10−10 test/reg035/expected+1−4

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+5

@@ -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 ()

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

143144fill : Raw -> Elab ()

144145fill tm = prim__Fill tm

145146

147+||| Fill with unification

148+apply : Raw -> Elab ()

149+apply tm = prim__Apply tm

150+

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

147152focus hole = prim__Focus hole

148153

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+4

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

17471747 alt' <- eval alt

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

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

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

1751+ fill raw'

1752+ returnUnit

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

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

17511755 apply raw' []

17521756 returnUnit

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