7c9a1d0 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge branch 'master' of github.com:idris-lang/Idris-dev

7c9a1d0Edwin Brady12 years ago

src/Idris/DSL.hs+2

compare with master

unifiedsplit

@@ -76,6 +76,7 @@ expandDo dsl (PDoBlock ds)

76 block b _ = PElabError (Msg "Invalid statement in do block")

78expandDo dsl (PIdiom fc e) = expandDo dsl $ unIdiom (dsl_apply dsl) (dsl_pure dsl) fc e

79+expandDo dsl (PRunTactics fc tm) = PRunTactics fc $ expandDo dsl tm

79expandDo dsl t = t

80expandDo dsl t = t

81-- | Replace DSL-bound variable in a term

82-- | Replace DSL-bound variable in a term

@@ -162,6 +163,7 @@ debind b tm = let (tm', (bs, _)) = runState (db' tm) ([], 0) in

162 db' (PDPair fc p l t r) = do l' <- db' l

163 db' (PDPair fc p l t r) = do l' <- db' l

163 r' <- db' r

164 r' <- db' r

164 return (PDPair fc p l' t r')

165 return (PDPair fc p l' t r')

166+ db' (PRunTactics fc t) = fmap (PRunTactics fc) (db' t)

165 db' t = return t

167 db' t = return t

166

168

167 dbArg a = do t' <- db' (getTm a)

169 dbArg a = do t' <- db' (getTm a)

src/Idris/ElabTerm.hs+131−62

@@ -983,7 +983,7 @@ elab ist info emode opts fn tm

983 saveState

984 updatePS (const .

985 newProof (sMN 0 "q") ctxt $

986− P Ref tt Erased)

986+ P Ref (reflm "TT") Erased)

987

988 -- Re-add the unquotes, letting Idris infer the (fictional)

989 -- types. Here, they represent the real type rather than the type

@@ -1030,8 +1030,9 @@ elab ist info emode opts fn tm

1030 Just q -> do ctxt <- get_context

1031 (q', _, _) <- lift $ recheck ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q

1032 if pattern

1033− then reflectTTQuotePattern unquoteNames q'

1033+ then do try' (reflectTTQuotePattern unquoteNames q')

1034− -- TODO: support quasiquote patterns of Raw terms

1034+ (reflectRawQuotePattern unquoteNames (forget q'))

1035+ True

1035 else do try' (fill $ reflectTTQuote unquoteNames q')

1036 else do try' (fill $ reflectTTQuote unquoteNames q')

1036 -- we forget q' instead of using q to ensure rechecking

1037 -- we forget q' instead of using q to ensure rechecking

1037 (fill $ reflectRawQuote unquoteNames (forget q'))

1038 (fill $ reflectRawQuote unquoteNames (forget q'))

@@ -1044,9 +1045,7 @@ elab ist info emode opts fn tm

1044 -- happens last so that their holes still exist while elaborating

1045 -- happens last so that their holes still exist while elaborating

1045 -- the main quotation.

1046 -- the main quotation.

1046 mapM_ elabUnquote unq

1047 mapM_ elabUnquote unq

1047− where tt = sNS (sUN "TT") ["Reflection", "Language"]

1048−

1049− elabUnquote (n, tm)

1048+ where elabUnquote (n, tm)

1050 = do focus n

1049 = do focus n

1051 elabE (ina { e_qq = False }) fc tm

1050 elabE (ina { e_qq = False }) fc tm

1052

1051

@@ -2175,62 +2174,7 @@ reflectTTQuotePattern unq (Bind n b x)

2175 Var x']

2174 Var x']

2176 solve

2175 solve

2177 focus x'; reflectTTQuotePattern unq x

2176 focus x'; reflectTTQuotePattern unq x

2178− focus b'; reflectBinderQuotePattern unq b

2177+ focus b'; reflectBinderQuotePattern reflectTTQuotePattern unq b

2179−

2180− where

2181− reflectBinderQuotePattern :: [Name] -> Binder Term -> ElabD ()

2182− reflectBinderQuotePattern unq (Lam t)

2183− = do t' <- claimTT (sMN 0 "ty"); movelast t'

2184− fill $ reflCall "Lam" [Var (reflm "TT"), Var t']

2185− solve

2186− focus t'; reflectTTQuotePattern unq t

2187− reflectBinderQuotePattern unq (Pi _ t k)

2188− = do t' <- claimTT (sMN 0 "ty") ; movelast t'

2189− k' <- claimTT (sMN 0 "k"); movelast k';

2190− fill $ reflCall "Pi" [Var (reflm "TT"), Var t', Var k']

2191− solve

2192− focus t'; reflectTTQuotePattern unq t

2193− reflectBinderQuotePattern unq (Let x y)

2194− = do x' <- claimTT (sMN 0 "ty"); movelast x';

2195− y' <- claimTT (sMN 0 "v"); movelast y';

2196− fill $ reflCall "Let" [Var (reflm "TT"), Var x', Var y']

2197− solve

2198− focus x'; reflectTTQuotePattern unq x

2199− focus y'; reflectTTQuotePattern unq y

2200− reflectBinderQuotePattern unq (NLet x y)

2201− = do x' <- claimTT (sMN 0 "ty"); movelast x'

2202− y' <- claimTT (sMN 0 "v"); movelast y'

2203− fill $ reflCall "NLet" [Var (reflm "TT"), Var x', Var y']

2204− solve

2205− focus x'; reflectTTQuotePattern unq x

2206− focus y'; reflectTTQuotePattern unq y

2207− reflectBinderQuotePattern unq (Hole t)

2208− = do t' <- claimTT (sMN 0 "ty"); movelast t'

2209− fill $ reflCall "Hole" [Var (reflm "TT"), Var t']

2210− solve

2211− focus t'; reflectTTQuotePattern unq t

2212− reflectBinderQuotePattern unq (GHole _ t)

2213− = do t' <- claimTT (sMN 0 "ty"); movelast t'

2214− fill $ reflCall "GHole" [Var (reflm "TT"), Var t']

2215− solve

2216− focus t'; reflectTTQuotePattern unq t

2217− reflectBinderQuotePattern unq (Guess x y)

2218− = do x' <- claimTT (sMN 0 "ty"); movelast x'

2219− y' <- claimTT (sMN 0 "v"); movelast y'

2220− fill $ reflCall "Guess" [Var (reflm "TT"), Var x', Var y']

2221− solve

2222− focus x'; reflectTTQuotePattern unq x

2223− focus y'; reflectTTQuotePattern unq y

2224− reflectBinderQuotePattern unq (PVar t)

2225− = do t' <- claimTT (sMN 0 "ty"); movelast t'

2226− fill $ reflCall "PVar" [Var (reflm "TT"), Var t']

2227− solve

2228− focus t'; reflectTTQuotePattern unq t

2229− reflectBinderQuotePattern unq (PVTy t)

2230− = do t' <- claimTT (sMN 0 "ty"); movelast t'

2231− fill $ reflCall "PVTy" [Var (reflm "TT"), Var t']

2232− solve

2233− focus t'; reflectTTQuotePattern unq t

2234reflectTTQuotePattern unq (App f x)

2178reflectTTQuotePattern unq (App f x)

2235 = do f' <- claimTT (sMN 0 "f"); movelast f'

2179 = do f' <- claimTT (sMN 0 "f"); movelast f'

2236 x' <- claimTT (sMN 0 "x"); movelast x'

2180 x' <- claimTT (sMN 0 "x"); movelast x'

@@ -2273,6 +2217,131 @@ reflectTTQuotePattern unq (UType u)

2273 AllTypes -> "AllTypes")))

2217 AllTypes -> "AllTypes")))

2274 solve

2218 solve

2275

2219

2220+reflectRawQuotePattern :: [Name] -> Raw -> ElabD ()

2221+reflectRawQuotePattern unq (Var n)

2222+ -- the unquoted names already have types, just use them

2223+ | n `elem` unq = do fill (Var n); solve

2224+ | otherwise = do fill (reflCall "Var" [reflectName n]); solve

2225+reflectRawQuotePattern unq (RBind n b sc) =

2226+ do scH <- getNameFrom (sMN 0 "sc")

2227+ claim scH (Var (reflm "Raw"))

2228+ movelast scH

2229+ bH <- getNameFrom (sMN 0 "binder")

2230+ claim bH (RApp (Var (reflm "Binder"))

2231+ (Var (reflm "Raw")))

2232+ if n `elem` freeNamesR sc

2233+ then do fill $ reflCall "RBind" [reflectName n,

2234+ Var bH,

2235+ Var scH]

2236+ solve

2237+ else do any <- getNameFrom (sMN 0 "anyName")

2238+ claim any (Var (reflm "TTName"))

2239+ movelast any

2240+ fill $ reflCall "RBind" [Var any, Var bH, Var scH]

2241+ solve

2242+ focus scH; reflectRawQuotePattern unq sc

2243+ focus bH; reflectBinderQuotePattern reflectRawQuotePattern unq b

2244+ where freeNamesR (Var n) = [n]

2245+ freeNamesR (RBind n (Let t v) body) = concat [freeNamesR v,

2246+ freeNamesR body \\ [n],

2247+ freeNamesR t]

2248+ freeNamesR (RBind n b body) = freeNamesR (binderTy b) ++

2249+ (freeNamesR body \\ [n])

2250+ freeNamesR (RApp f x) = freeNamesR f ++ freeNamesR x

2251+ freeNamesR RType = []

2252+ freeNamesR (RUType _) = []

2253+ freeNamesR (RForce r) = freeNamesR r

2254+ freeNamesR (RConstant _) = []

2255+reflectRawQuotePattern unq (RApp f x) =

2256+ do fH <- getNameFrom (sMN 0 "f")

2257+ claim fH (Var (reflm "Raw"))

2258+ movelast fH

2259+ xH <- getNameFrom (sMN 0 "x")

2260+ claim xH (Var (reflm "Raw"))

2261+ movelast xH

2262+ fill $ reflCall "RApp" [Var fH, Var xH]

2263+ solve

2264+ focus fH; reflectRawQuotePattern unq f

2265+ focus xH; reflectRawQuotePattern unq x

2266+reflectRawQuotePattern unq RType =

2267+ do fill (Var (reflm "RType"))

2268+ solve

2269+reflectRawQuotePattern unq (RUType univ) =

2270+ do uH <- getNameFrom (sMN 0 "universe")

2271+ claim uH (Var (reflm "Universe"))

2272+ movelast uH

2273+ fill $ reflCall "RUType" [Var uH]

2274+ solve

2275+ focus uH; fill (reflectUniverse univ); solve

2276+reflectRawQuotePattern unq (RForce r) =

2277+ do rH <- getNameFrom (sMN 0 "raw")

2278+ claim rH (Var (reflm "Raw"))

2279+ movelast rH

2280+ fill $ reflCall "RForce" [Var rH]

2281+ solve

2282+ focus rH; reflectRawQuotePattern unq r

2283+reflectRawQuotePattern unq (RConstant c) =

2284+ do cH <- getNameFrom (sMN 0 "const")

2285+ claim cH (Var (reflm "Constant"))

2286+ movelast cH

2287+ fill (reflCall "RConstant" [Var cH]); solve

2288+ focus cH

2289+ fill (reflectConstant c); solve

2290+

2291+reflectBinderQuotePattern :: ([Name] -> a -> ElabD ()) -> [Name] -> Binder a -> ElabD ()

2292+reflectBinderQuotePattern q unq (Lam t)

2293+ = do t' <- claimTT (sMN 0 "ty"); movelast t'

2294+ fill $ reflCall "Lam" [Var (reflm "TT"), Var t']

2295+ solve

2296+ focus t'; q unq t

2297+reflectBinderQuotePattern q unq (Pi _ t k)

2298+ = do t' <- claimTT (sMN 0 "ty") ; movelast t'

2299+ k' <- claimTT (sMN 0 "k"); movelast k';

2300+ fill $ reflCall "Pi" [Var (reflm "TT"), Var t', Var k']

2301+ solve

2302+ focus t'; q unq t

2303+reflectBinderQuotePattern q unq (Let x y)

2304+ = do x' <- claimTT (sMN 0 "ty"); movelast x';

2305+ y' <- claimTT (sMN 0 "v"); movelast y';

2306+ fill $ reflCall "Let" [Var (reflm "TT"), Var x', Var y']

2307+ solve

2308+ focus x'; q unq x

2309+ focus y'; q unq y

2310+reflectBinderQuotePattern q unq (NLet x y)

2311+ = do x' <- claimTT (sMN 0 "ty"); movelast x'

2312+ y' <- claimTT (sMN 0 "v"); movelast y'

2313+ fill $ reflCall "NLet" [Var (reflm "TT"), Var x', Var y']

2314+ solve

2315+ focus x'; q unq x

2316+ focus y'; q unq y

2317+reflectBinderQuotePattern q unq (Hole t)

2318+ = do t' <- claimTT (sMN 0 "ty"); movelast t'

2319+ fill $ reflCall "Hole" [Var (reflm "TT"), Var t']

2320+ solve

2321+ focus t'; q unq t

2322+reflectBinderQuotePattern q unq (GHole _ t)

2323+ = do t' <- claimTT (sMN 0 "ty"); movelast t'

2324+ fill $ reflCall "GHole" [Var (reflm "TT"), Var t']

2325+ solve

2326+ focus t'; q unq t

2327+reflectBinderQuotePattern q unq (Guess x y)

2328+ = do x' <- claimTT (sMN 0 "ty"); movelast x'

2329+ y' <- claimTT (sMN 0 "v"); movelast y'

2330+ fill $ reflCall "Guess" [Var (reflm "TT"), Var x', Var y']

2331+ solve

2332+ focus x'; q unq x

2333+ focus y'; q unq y

2334+reflectBinderQuotePattern q unq (PVar t)

2335+ = do t' <- claimTT (sMN 0 "ty"); movelast t'

2336+ fill $ reflCall "PVar" [Var (reflm "TT"), Var t']

2337+ solve

2338+ focus t'; q unq t

2339+reflectBinderQuotePattern q unq (PVTy t)

2340+ = do t' <- claimTT (sMN 0 "ty"); movelast t'

2341+ fill $ reflCall "PVTy" [Var (reflm "TT"), Var t']

2342+ solve

2343+ focus t'; q unq t

2344+

2276reflectUniverse :: Universe -> Raw

2345reflectUniverse :: Universe -> Raw

2277reflectUniverse u =

2346reflectUniverse u =

2278 (Var (reflm (case u of

2347 (Var (reflm (case u of

src/Idris/Error.hs+3

@@ -1,4 +1,5 @@

1{-# LANGUAGE DeriveDataTypeable #-}

2+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

3module Idris.Error where

4module Idris.Error where

@@ -146,3 +147,5 @@ warnDisamb ist (PQuasiquote tm goal) = warnDisamb ist tm >>

146 Foldable.mapM_ (warnDisamb ist) goal

147 Foldable.mapM_ (warnDisamb ist) goal

147warnDisamb ist (PUnquote tm) = warnDisamb ist tm

148warnDisamb ist (PUnquote tm) = warnDisamb ist tm

148warnDisamb ist (PAs _ _ tm) = warnDisamb ist tm

149warnDisamb ist (PAs _ _ tm) = warnDisamb ist tm

150+warnDisamb ist (PAppImpl tm _) = warnDisamb ist tm

151+warnDisamb ist (PRunTactics _ tm) = warnDisamb ist tm

src/Idris/ParseExpr.hs+1−1

@@ -498,7 +498,7 @@ runTactics syn = do try (lchar '%' *> reserved "runTactics")

498 fc <- getFC

499 tm <- simpleExpr syn

500 i <- get

501− return $ debindApp syn (desugar syn i (PRunTactics fc tm))

501+ return $ PRunTactics fc tm

502 <?> "new-style tactics expression"

503

504{- | Parses a disambiguation expression

test/quasiquote005/Quasiquote005.idr+13

@@ -1,5 +1,7 @@

1module Quasiquote005

3+-- Test Raw quasiquotes

3test : the Language.Reflection.Raw `(plus (S Z) (S Z)) =

5test : the Language.Reflection.Raw `(plus (S Z) (S Z)) =

4 RApp (RApp (Var (NS (UN "plus") ["Nat", "Prelude"]))

6 RApp (RApp (Var (NS (UN "plus") ["Nat", "Prelude"]))

5 (RApp (Var (NS (UN "S") ["Nat", "Prelude"]))

7 (RApp (Var (NS (UN "S") ["Nat", "Prelude"]))

@@ -7,3 +9,14 @@ test : the Language.Reflection.Raw `(plus (S Z) (S Z)) =

7 (RApp (Var (NS (UN "S") ["Nat", "Prelude"]))

9 (RApp (Var (NS (UN "S") ["Nat", "Prelude"]))

8 (Var (NS (UN "Z") ["Nat", "Prelude"])))

10 (Var (NS (UN "Z") ["Nat", "Prelude"])))

9test = Refl

11test = Refl

12+

13+firstAddend : Raw -> Maybe Raw

14+firstAddend `(plus ~first ~_) = Just first

15+firstAddend _ = Nothing

16+

17+firstAddendOk : firstAddend (RApp (RApp (Var (NS (UN "plus") ["Nat", "Prelude"]))

18+ (RApp (Var (NS (UN "S") ["Nat", "Prelude"]))

19+ (Var (NS (UN "Z") ["Nat", "Prelude"]))))

20+ (Var (NS (UN "Z") ["Nat", "Prelude"]))) =

21+ the (Maybe Raw) (Just `(S Z))

22+firstAddendOk = Refl