bc34332 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Improve quasiquote patterns for MN

bc34332David Raymond Christiansen12 years ago

src/Idris/ElabTerm.hs+9−2

@@ -1806,8 +1806,9 @@ reflectName (MN i n)

1806reflectName (NErased) = Var (reflm "NErased")

1807reflectName n = Var (reflm "NErased") -- special name, not yet implemented

1808

1809−-- | Elaborate a name to a pattern. This means that NS and UN will be intact,

1809+-- | Elaborate a name to a pattern. This means that NS and UN will be intact.

1810+-- MNs corresponding to will care about the string but not the number. All

1810−-- while all others become _

1811+-- others become _.

1811reflectNameQuotePattern :: Name -> ElabD ()

1812reflectNameQuotePattern :: Name -> ElabD ()

1812reflectNameQuotePattern n@(UN s)

1813reflectNameQuotePattern n@(UN s)

1813 = do fill $ reflectName n

1814 = do fill $ reflectName n

@@ -1815,6 +1816,12 @@ reflectNameQuotePattern n@(UN s)

1815reflectNameQuotePattern n@(NS _ _)

1816reflectNameQuotePattern n@(NS _ _)

1816 = do fill $ reflectName n

1817 = do fill $ reflectName n

1817 solve

1818 solve

1819+reflectNameQuotePattern (MN _ n)

1820+ = do i <- getNameFrom (sMN 0 "mnCounter")

1821+ claim i (RConstant (AType (ATInt ITNative)))

1822+ movelast i

1823+ fill $ reflCall "MN" [Var i, RConstant (Str $ T.unpack n)]

1824+ solve

1818reflectNameQuotePattern _ -- for all other names, match any

1825reflectNameQuotePattern _ -- for all other names, match any

1819 = do nameHole <- getNameFrom (sMN 0 "name")

1826 = do nameHole <- getNameFrom (sMN 0 "name")

1820 claim nameHole (Var (reflm "TTName"))

1827 claim nameHole (Var (reflm "TTName"))