f327f18 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Raw quasiquote patterns

f327f18David Raymond Christiansen12 years ago

src/Idris/ElabTerm.hs+131−62

compare with master

unifiedsplit

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

975 saveState

976 updatePS (const .

977 newProof (sMN 0 "q") ctxt $

978− P Ref tt Erased)

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

979

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

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

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

1022 Just q -> do ctxt <- get_context

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

1024 if pattern

1025− then reflectTTQuotePattern unquoteNames q'

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

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

1026+ (reflectRawQuotePattern unquoteNames (forget q'))

1027+ True

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

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

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

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

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

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

@@ -1036,9 +1037,7 @@ elab ist info emode opts fn tm

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

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

1037 -- the main quotation.

1038 -- the main quotation.

1038 mapM_ elabUnquote unq

1039 mapM_ elabUnquote unq

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

1040−

1041− elabUnquote (n, tm)

1040+ where elabUnquote (n, tm)

1042 = do focus n

1041 = do focus n

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

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

1044

1043

@@ -2167,62 +2166,7 @@ reflectTTQuotePattern unq (Bind n b x)

2167 Var x']

2166 Var x']

2168 solve

2167 solve

2169 focus x'; reflectTTQuotePattern unq x

2168 focus x'; reflectTTQuotePattern unq x

2170− focus b'; reflectBinderQuotePattern unq b

2169+ focus b'; reflectBinderQuotePattern reflectTTQuotePattern unq b

2171−

2172− where

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

2174− reflectBinderQuotePattern unq (Lam t)

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

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

2177− solve

2178− focus t'; reflectTTQuotePattern unq t

2179− reflectBinderQuotePattern unq (Pi _ t k)

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

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

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

2183− solve

2184− focus t'; reflectTTQuotePattern unq t

2185− reflectBinderQuotePattern unq (Let x y)

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

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

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

2189− solve

2190− focus x'; reflectTTQuotePattern unq x

2191− focus y'; reflectTTQuotePattern unq y

2192− reflectBinderQuotePattern unq (NLet x y)

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

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

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

2196− solve

2197− focus x'; reflectTTQuotePattern unq x

2198− focus y'; reflectTTQuotePattern unq y

2199− reflectBinderQuotePattern unq (Hole t)

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

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

2202− solve

2203− focus t'; reflectTTQuotePattern unq t

2204− reflectBinderQuotePattern unq (GHole _ t)

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

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

2207− solve

2208− focus t'; reflectTTQuotePattern unq t

2209− reflectBinderQuotePattern unq (Guess x y)

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

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

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

2213− solve

2214− focus x'; reflectTTQuotePattern unq x

2215− focus y'; reflectTTQuotePattern unq y

2216− reflectBinderQuotePattern unq (PVar t)

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

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

2219− solve

2220− focus t'; reflectTTQuotePattern unq t

2221− reflectBinderQuotePattern unq (PVTy t)

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

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

2224− solve

2225− focus t'; reflectTTQuotePattern unq t

2226reflectTTQuotePattern unq (App f x)

2170reflectTTQuotePattern unq (App f x)

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

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

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

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

@@ -2265,6 +2209,131 @@ reflectTTQuotePattern unq (UType u)

2265 AllTypes -> "AllTypes")))

2209 AllTypes -> "AllTypes")))

2266 solve

2210 solve

2267

2211

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

2213+reflectRawQuotePattern unq (Var n)

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

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

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

2217+reflectRawQuotePattern unq (RBind n b sc) =

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

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

2220+ movelast scH

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

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

2223+ (Var (reflm "Raw")))

2224+ if n `elem` freeNamesR sc

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

2226+ Var bH,

2227+ Var scH]

2228+ solve

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

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

2231+ movelast any

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

2233+ solve

2234+ focus scH; reflectRawQuotePattern unq sc

2235+ focus bH; reflectBinderQuotePattern reflectRawQuotePattern unq b

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

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

2238+ freeNamesR body \\ [n],

2239+ freeNamesR t]

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

2241+ (freeNamesR body \\ [n])

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

2243+ freeNamesR RType = []

2244+ freeNamesR (RUType _) = []

2245+ freeNamesR (RForce r) = freeNamesR r

2246+ freeNamesR (RConstant _) = []

2247+reflectRawQuotePattern unq (RApp f x) =

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

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

2250+ movelast fH

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

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

2253+ movelast xH

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

2255+ solve

2256+ focus fH; reflectRawQuotePattern unq f

2257+ focus xH; reflectRawQuotePattern unq x

2258+reflectRawQuotePattern unq RType =

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

2260+ solve

2261+reflectRawQuotePattern unq (RUType univ) =

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

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

2264+ movelast uH

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

2266+ solve

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

2268+reflectRawQuotePattern unq (RForce r) =

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

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

2271+ movelast rH

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

2273+ solve

2274+ focus rH; reflectRawQuotePattern unq r

2275+reflectRawQuotePattern unq (RConstant c) =

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

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

2278+ movelast cH

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

2280+ focus cH

2281+ fill (reflectConstant c); solve

2282+

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

2284+reflectBinderQuotePattern q unq (Lam t)

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

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

2287+ solve

2288+ focus t'; q unq t

2289+reflectBinderQuotePattern q unq (Pi _ t k)

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

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

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

2293+ solve

2294+ focus t'; q unq t

2295+reflectBinderQuotePattern q unq (Let x y)

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

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

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

2299+ solve

2300+ focus x'; q unq x

2301+ focus y'; q unq y

2302+reflectBinderQuotePattern q unq (NLet x y)

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

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

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

2306+ solve

2307+ focus x'; q unq x

2308+ focus y'; q unq y

2309+reflectBinderQuotePattern q unq (Hole t)

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

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

2312+ solve

2313+ focus t'; q unq t

2314+reflectBinderQuotePattern q unq (GHole _ t)

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

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

2317+ solve

2318+ focus t'; q unq t

2319+reflectBinderQuotePattern q unq (Guess x y)

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

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

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

2323+ solve

2324+ focus x'; q unq x

2325+ focus y'; q unq y

2326+reflectBinderQuotePattern q unq (PVar t)

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

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

2329+ solve

2330+ focus t'; q unq t

2331+reflectBinderQuotePattern q unq (PVTy t)

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

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

2334+ solve

2335+ focus t'; q unq t

2336+

2268reflectUniverse :: Universe -> Raw

2337reflectUniverse :: Universe -> Raw

2269reflectUniverse u =

2338reflectUniverse u =

2270 (Var (reflm (case u of

2339 (Var (reflm (case u of

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