f09605b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Require unique global names in TT

f09605bDavid Raymond Christiansen11 years ago

libs/prelude/IO.idr+29−29

compare with master

unifiedsplit

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

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

120

121--------- The C FFI

122−

122+namespace FFI_C

123−data Raw : Type -> Type where

123+ data Raw : Type -> Type where

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

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

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

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

126−

126+

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

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

128−%used MkRaw x

128+ %used MkRaw x

129−

129+

130−-- Supported C integer types

130+ -- Supported C integer types

131−data C_IntTypes : Type -> Type where

131+ data C_IntTypes : Type -> Type where

132− C_IntChar : C_IntTypes Char

132+ C_IntChar : C_IntTypes Char

133− C_IntNative : C_IntTypes Int

133+ C_IntNative : C_IntTypes Int

134− C_IntBits8 : C_IntTypes Bits8

134+ C_IntBits8 : C_IntTypes Bits8

135− C_IntBits16 : C_IntTypes Bits16

135+ C_IntBits16 : C_IntTypes Bits16

136− C_IntBits32 : C_IntTypes Bits32

136+ C_IntBits32 : C_IntTypes Bits32

137− C_IntBits64 : C_IntTypes Bits64

137+ C_IntBits64 : C_IntTypes Bits64

138−

138+

139−-- Supported C foreign types

139+ -- Supported C foreign types

140−data C_Types : Type -> Type where

140+ data C_Types : Type -> Type where

141− C_Str : C_Types String

141+ C_Str : C_Types String

142− C_Float : C_Types Float

142+ C_Float : C_Types Float

143− C_Ptr : C_Types Ptr

143+ C_Ptr : C_Types Ptr

144− C_MPtr : C_Types ManagedPtr

144+ C_MPtr : C_Types ManagedPtr

145− C_Unit : C_Types ()

145+ C_Unit : C_Types ()

146− C_Any : C_Types (Raw a)

146+ C_Any : C_Types (Raw a)

147− C_IntT : C_IntTypes i -> C_Types i

147+ C_IntT : C_IntTypes i -> C_Types i

148−

148+

149−FFI_C : FFI

149+ FFI_C : FFI

150−FFI_C = MkFFI C_Types String String

150+ FFI_C = MkFFI C_Types String String

151

152IO : Type -> Type

153IO = IO' FFI_C

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

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

58 prim__Solve : Elab ()

59 prim__Fill : Raw -> Elab ()

60+ prim__Apply : Raw -> Elab ()

60 prim__Focus : TTName -> Elab ()

61 prim__Focus : TTName -> Elab ()

61 prim__Unfocus : TTName -> Elab ()

62 prim__Unfocus : TTName -> Elab ()

62 prim__Attack : Elab ()

63 prim__Attack : Elab ()

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

143fill : Raw -> Elab ()

144fill : Raw -> Elab ()

144fill tm = prim__Fill tm

145fill tm = prim__Fill tm

145

146

147+||| Fill with unification

148+apply : Raw -> Elab ()

149+apply tm = prim__Apply tm

150+

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

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

147focus hole = prim__Focus hole

152focus hole = prim__Focus hole

148

153

src/IRTS/CodegenC.hs+1−1

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

647

648writeIFace :: ExportIFace -> IO ()

649writeIFace (Export ffic hdr exps)

650− | ffic == sUN "FFI_C"

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

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

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

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

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

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

1011

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

1013lookupP_all all n ctxt

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

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

1015 p <- case def of

1016− (Function ty tm, 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)

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

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

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

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

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

1020 case snd p of

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

1022 _ -> 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

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

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

88 -- checking an already elaborated term, we do

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

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

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

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

91 | otherwise = do lift $ tfail $ NoSuchVariable n

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

93 -- special case to reduce constraintss

src/Idris/Elab/Term.hs+4

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

1747 alt' <- eval alt

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

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

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

1751+ fill raw'

1752+ returnUnit

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

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

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

1751 apply raw' []

1755 apply raw' []

1752 returnUnit

1756 returnUnit

test/meta002/Tacs.idr+10−10

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

181 mkIx : Fin n -> Elab ()

182 mkIx FZ = do envH <- mkEnvH

183 tH <- mkTyH

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

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

185 solve

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

187 tH <- mkTyH

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

189 argH <- gensym "arg"

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

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

193 solve

194 focus argH

195 mkIx i

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

200 tH' <- mkTyH

201 bodyH <- gensym "body"

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

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

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

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

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

205− ~(Var bodyH))

205+ ~(Var bodyH))

206

207 solve

208 focus bodyH

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

216 argH <- gensym "arg"

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

218 unfocus argH

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

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

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

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

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

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

222 solve

223 focus fH

224 mkTerm xs tm

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

229 ixH <- gensym "ix"

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

231 unfocus ixH

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

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

233 solve

234 focus ixH

235 mkIx i

236 mkTerm xs UnitCon = do envH <- mkEnvH

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

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

238 solve

239 testElab : Sigma Ty (Tm [])

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

test/reg035/expected+1−4

@@ -1,4 +1 @@

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

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

2− Additive -> Nat

3−with

4− Fin 0