ee11033 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Elaborate quasiquote patterns to something useful

ee11033David Raymond Christiansen12 years ago

src/Idris/AbsSyntax.hs+67−65

compare with master

unifiedsplit

@@ -1280,87 +1280,89 @@ addImpl = addImpl' False [] []

1280-- and *not* inside a PHidden

1281

1282addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm

1283−addImpl' inpat env infns ist ptm

1283+addImpl' inpat env infns ist ptm

1284− = mkUniqueNames env (ai (zip env (repeat Nothing)) [] ptm)

1284+ = mkUniqueNames env (ai False (zip env (repeat Nothing)) [] ptm)

1285 where

1286+ ai :: Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm

1286− ai env ds (PRef fc f)

1287+ ai qq env ds (PRef fc f)

1287 | f `elem` infns = PInferRef fc f

1288 | f `elem` infns = PInferRef fc f

1288− | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat ist fc f ds []

1289+ | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq ist fc f ds []

1289− ai env ds (PHidden (PRef fc f))

1290+ ai qq env ds (PHidden (PRef fc f))

1290− | not (f `elem` map fst env) = handleErr $ aiFn inpat False ist fc f ds []

1291+ | not (f `elem` map fst env) = handleErr $ aiFn inpat False qq ist fc f ds []

1291− ai env ds (PEq fc l r)

1292+ ai qq env ds (PEq fc l r)

1292− = let l' = ai env ds l

1293+ = let l' = ai qq env ds l

1293− r' = ai env ds r in

1294+ r' = ai qq env ds r in

1294 PEq fc l' r'

1295 PEq fc l' r'

1295− ai env ds (PRewrite fc l r g)

1296+ ai qq env ds (PRewrite fc l r g)

1296− = let l' = ai env ds l

1297+ = let l' = ai qq env ds l

1297− r' = ai env ds r

1298+ r' = ai qq env ds r

1298− g' = fmap (ai env ds) g in

1299+ g' = fmap (ai qq env ds) g in

1299 PRewrite fc l' r' g'

1300 PRewrite fc l' r' g'

1300− ai env ds (PTyped l r)

1301+ ai qq env ds (PTyped l r)

1301− = let l' = ai env ds l

1302+ = let l' = ai qq env ds l

1302− r' = ai env ds r in

1303+ r' = ai qq env ds r in

1303 PTyped l' r'

1304 PTyped l' r'

1304− ai env ds (PPair fc p l r)

1305+ ai qq env ds (PPair fc p l r)

1305− = let l' = ai env ds l

1306+ = let l' = ai qq env ds l

1306− r' = ai env ds r in

1307+ r' = ai qq env ds r in

1307 PPair fc p l' r'

1308 PPair fc p l' r'

1308− ai env ds (PDPair fc p l t r)

1309+ ai qq env ds (PDPair fc p l t r)

1309− = let l' = ai env ds l

1310+ = let l' = ai qq env ds l

1310− t' = ai env ds t

1311+ t' = ai qq env ds t

1311− r' = ai env ds r in

1312+ r' = ai qq env ds r in

1312 PDPair fc p l' t' r'

1313 PDPair fc p l' t' r'

1313− ai env ds (PAlternative a as)

1314+ ai qq env ds (PAlternative a as)

1314− = let as' = map (ai env ds) as in

1315+ = let as' = map (ai qq env ds) as in

1315 PAlternative a as'

1316 PAlternative a as'

1316− ai env _ (PDisamb ds' as) = ai env ds' as

1317+ ai qq env _ (PDisamb ds' as) = ai qq env ds' as

1317− ai env ds (PApp fc (PInferRef _ f) as)

1318+ ai qq env ds (PApp fc (PInferRef _ f) as)

1318− = let as' = map (fmap (ai env ds)) as in

1319+ = let as' = map (fmap (ai qq env ds)) as in

1319 PApp fc (PInferRef fc f) as'

1320 PApp fc (PInferRef fc f) as'

1320− ai env ds (PApp fc ftm@(PRef _ f) as)

1321+ ai qq env ds (PApp fc ftm@(PRef _ f) as)

1321− | f `elem` infns = ai env ds (PApp fc (PInferRef fc f) as)

1322+ | f `elem` infns = ai qq env ds (PApp fc (PInferRef fc f) as)

1322 | not (f `elem` map fst env)

1323 | not (f `elem` map fst env)

1323− = let as' = map (fmap (ai env ds)) as in

1324+ = let as' = map (fmap (ai qq env ds)) as in

1324− handleErr $ aiFn inpat False ist fc f ds as'

1325+ handleErr $ aiFn inpat False qq ist fc f ds as'

1325 | Just (Just ty) <- lookup f env =

1326 | Just (Just ty) <- lookup f env =

1326− let as' = map (fmap (ai env ds)) as

1327+ let as' = map (fmap (ai qq env ds)) as

1327 arity = getPArity ty in

1328 arity = getPArity ty in

1328 mkPApp fc arity ftm as'

1329 mkPApp fc arity ftm as'

1329− ai env ds (PApp fc f as)

1330+ ai qq env ds (PApp fc f as)

1330− = let f' = ai env ds f

1331+ = let f' = ai qq env ds f

1331− as' = map (fmap (ai env ds)) as in

1332+ as' = map (fmap (ai qq env ds)) as in

1332 mkPApp fc 1 f' as'

1333 mkPApp fc 1 f' as'

1333− ai env ds (PCase fc c os)

1334+ ai qq env ds (PCase fc c os)

1334− = let c' = ai env ds c in

1335+ = let c' = ai qq env ds c in

1335 -- leave os alone, because they get lifted into a new pattern match

1336 -- leave os alone, because they get lifted into a new pattern match

1336 -- definition which is passed through addImpl again with more scope

1337 -- definition which is passed through addImpl again with more scope

1337 -- information

1338 -- information

1338 PCase fc c' os

1339 PCase fc c' os

1339− ai env ds (PLam n ty sc)

1340+ ai qq env ds (PLam n ty sc)

1340− = let ty' = ai env ds ty

1341+ = let ty' = ai qq env ds ty

1341− sc' = ai ((n, Just ty):env) ds sc in

1342+ sc' = ai qq ((n, Just ty):env) ds sc in

1342 PLam n ty' sc'

1343 PLam n ty' sc'

1343− ai env ds (PLet n ty val sc)

1344+ ai qq env ds (PLet n ty val sc)

1344− = let ty' = ai env ds ty

1345+ = let ty' = ai qq env ds ty

1345− val' = ai env ds val

1346+ val' = ai qq env ds val

1346− sc' = ai ((n, Just ty):env) ds sc in

1347+ sc' = ai qq ((n, Just ty):env) ds sc in

1347 PLet n ty' val' sc'

1348 PLet n ty' val' sc'

1348− ai env ds (PPi p n ty sc)

1349+ ai qq env ds (PPi p n ty sc)

1349− = let ty' = ai env ds ty

1350+ = let ty' = ai qq env ds ty

1350− sc' = ai ((n, Just ty):env) ds sc in

1351+ sc' = ai qq ((n, Just ty):env) ds sc in

1351 PPi p n ty' sc'

1352 PPi p n ty' sc'

1352− ai env ds (PGoal fc r n sc)

1353+ ai qq env ds (PGoal fc r n sc)

1353− = let r' = ai env ds r

1354+ = let r' = ai qq env ds r

1354− sc' = ai ((n, Nothing):env) ds sc in

1355+ sc' = ai qq ((n, Nothing):env) ds sc in

1355 PGoal fc r' n sc'

1356 PGoal fc r' n sc'

1356− ai env ds (PHidden tm) = PHidden (ai env ds tm)

1357+ ai qq env ds (PHidden tm) = PHidden (ai qq env ds tm)

1357− ai env ds (PProof ts) = PProof (map (fmap (ai env ds)) ts)

1358+ ai qq env ds (PProof ts) = PProof (map (fmap (ai qq env ds)) ts)

1358− ai env ds (PTactics ts) = PTactics (map (fmap (ai env ds)) ts)

1359+ ai qq env ds (PTactics ts) = PTactics (map (fmap (ai qq env ds)) ts)

1359− ai env ds (PRefl fc tm) = PRefl fc (ai env ds tm)

1360+ ai qq env ds (PRefl fc tm) = PRefl fc (ai qq env ds tm)

1360− ai env ds (PUnifyLog tm) = PUnifyLog (ai env ds tm)

1361+ ai qq env ds (PUnifyLog tm) = PUnifyLog (ai qq env ds tm)

1361− ai env ds (PNoImplicits tm) = PNoImplicits (ai env ds tm)

1362+ ai qq env ds (PNoImplicits tm) = PNoImplicits (ai qq env ds tm)

1362− ai env ds (PQuasiquote tm) = PQuasiquote (ai env ds tm)

1363+ ai qq env ds (PQuasiquote tm) = PQuasiquote (ai True env ds tm)

1364+ ai qq env ds (PUnquote tm) = PUnquote (ai False env ds tm)

1363− ai env ds tm = tm

1365+ ai qq env ds tm = tm

1364

1366

1365 handleErr (Left err) = PElabError err

1367 handleErr (Left err) = PElabError err

1366 handleErr (Right x) = x

1368 handleErr (Right x) = x

@@ -1368,8 +1370,8 @@ addImpl' inpat env infns ist ptm

1368-- if in a pattern, and there are no arguments, and there's no possible

1370-- if in a pattern, and there are no arguments, and there's no possible

1369-- names with zero explicit arguments, don't add implicits.

1371-- names with zero explicit arguments, don't add implicits.

1370

1372

1371−aiFn :: Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm

1373+aiFn :: Bool -> Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm

1372−aiFn inpat True ist fc f ds []

1374+aiFn inpat True qq ist fc f ds []

1373 = case lookupDef f (tt_ctxt ist) of

1375 = case lookupDef f (tt_ctxt ist) of

1374 [] -> Right $ PPatvar fc f

1376 [] -> Right $ PPatvar fc f

1375 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in

1377 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in

@@ -1377,7 +1379,7 @@ aiFn inpat True ist fc f ds []

1377 if (not (vname f) || tcname f

1379 if (not (vname f) || tcname f

1378 || any (conCaf (tt_ctxt ist)) ialts)

1380 || any (conCaf (tt_ctxt ist)) ialts)

1379-- any constructor alts || any allImp ialts))

1381-- any constructor alts || any allImp ialts))

1380− then aiFn inpat False ist fc f ds [] -- use it as a constructor

1382+ then aiFn inpat False qq ist fc f ds [] -- use it as a constructor

1381 else Right $ PPatvar fc f

1383 else Right $ PPatvar fc f

1382 where imp (PExp _ _ _ _) = False

1384 where imp (PExp _ _ _ _) = False

1383 imp _ = True

1385 imp _ = True

@@ -1386,14 +1388,14 @@ aiFn inpat True ist fc f ds []

1386 constructor (TyDecl (DCon _ _) _) = True

1388 constructor (TyDecl (DCon _ _) _) = True

1387 constructor _ = False

1389 constructor _ = False

1388

1390

1389− conCaf ctxt (n, cia) = isDConName n ctxt && allImp cia

1391+ conCaf ctxt (n, cia) = (isDConName n ctxt || (qq && isTConName n ctxt)) && allImp cia

1390

1392

1391 vname (UN n) = True -- non qualified

1393 vname (UN n) = True -- non qualified

1392 vname _ = False

1394 vname _ = False

1393

1395

1394−aiFn inpat expat ist fc f ds as

1396+aiFn inpat expat qq ist fc f ds as

1395 | f `elem` primNames = Right $ PApp fc (PRef fc f) as

1397 | f `elem` primNames = Right $ PApp fc (PRef fc f) as

1396−aiFn inpat expat ist fc f ds as

1398+aiFn inpat expat qq ist fc f ds as

1397 -- This is where namespaces get resolved by adding PAlternative

1399 -- This is where namespaces get resolved by adding PAlternative

1398 = do let ns = lookupCtxtName f (idris_implicits ist)

1400 = do let ns = lookupCtxtName f (idris_implicits ist)

1399 let nh = filter (\(n, _) -> notHidden n) ns

1401 let nh = filter (\(n, _) -> notHidden n) ns

src/Idris/Core/Elaborate.hs+1

@@ -380,6 +380,7 @@ casetac tm = processTactic' (CaseTac tm)

380equiv :: Raw -> Elab' aux ()

381equiv tm = processTactic' (Equiv tm)

382

383+-- | Turn the current hole into a pattern variable with the provided name, made unique if MN

383patvar :: Name -> Elab' aux ()

384patvar :: Name -> Elab' aux ()

384patvar n = do env <- get_env

385patvar n = do env <- get_env

385 hs <- get_holes

386 hs <- get_holes

src/Idris/ElabTerm.hs+161−11

@@ -293,8 +293,8 @@ elab ist info pattern opts fn tm

293 elab' ina (PPatvar fc n) | pattern = patvar n

294-- elab' (_, _, inty) (PRef fc f)

295-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty

296−-- = lift $ tfail (Msg "Typecase is not allowed")

296+-- = lift $ tfail (Msg "Typecase is not allowed")

297− elab' (ina, guarded, inty, qq) (PRef fc n) | pattern && not (inparamBlock n)

297+ elab' (ina, guarded, inty, qq) (PRef fc n) | pattern && not (inparamBlock n) && not qq

298 = do ctxt <- get_context

299 let defined = case lookupTy n ctxt of

300 [] -> False

@@ -640,8 +640,9 @@ elab ist info pattern opts fn tm

640 = do -- First elaborate the unquoted subterms, replacing them with

641 -- fresh names in the quasiquoted term

642 (t, unq) <- extractUnquotes t

643− mapM_ (flip claim (Var tt) . fst) unq

644 let unquoteNames = map fst unq

643 let unquoteNames = map fst unq

644+ mapM_ (flip claim (Var tt)) unquoteNames

645+

645

646

646 -- Save the old state - we need a fresh proof state for this to

647 -- Save the old state - we need a fresh proof state for this to

647 -- avoid capture

648 -- avoid capture

@@ -676,17 +677,18 @@ elab ist info pattern opts fn tm

676 focus qTm

677 focus qTm

677 elabE (ina, g, inty, True) t

678 elabE (ina, g, inty, True) t

678 end_unify

679 end_unify

680+

679 -- We now have an elaborated term. Reflect it and solve the

681 -- We now have an elaborated term. Reflect it and solve the

680 -- original goal

682 -- original goal

681 env <- get_env

683 env <- get_env

684+ loadState

682− let qTerm = fmap (reflectQuote unquoteNames . binderVal) $ lookup nTm env

685+ case fmap (explicitNames . binderVal) $ lookup nTm env of

683−

684− case qTerm of

685− Just q -> do loadState

686+ Just q

686− fill q

687+ | pattern -> reflectQuotePattern unquoteNames q

688+ | otherwise -> do fill $ reflectQuote unquoteNames q

687− solve

689+ solve

688− mapM_ elabUnquote unq

689 Nothing -> fail "Broken elaboration of quasiquote"

690 Nothing -> fail "Broken elaboration of quasiquote"

691+ mapM_ elabUnquote unq

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

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

691

693

692 elabUnquote (n, tm)

694 elabUnquote (n, tm)

@@ -1509,6 +1511,138 @@ reflCall funName args

1509reflect :: Term -> Raw

1511reflect :: Term -> Raw

1510reflect = reflectQuote []

1512reflect = reflectQuote []

1511

1513

1514+claimTT :: Name -> ElabD Name

1515+claimTT n = do n' <- getNameFrom n

1516+ claim n' (Var (sNS (sUN "TT") ["Reflection", "Language"]))

1517+ return n'

1518+

1519+-- | Convert a reflected term to a more suitable form for pattern-matching.

1520+-- In particular, the less-interesting bits are elaborated to _ patterns. This

1521+-- happens to NameTypes, universe levels, names that are bound but not used,

1522+-- and the type annotation field of the P constructor.

1523+reflectQuotePattern :: [Name] -> Term -> ElabD ()

1524+reflectQuotePattern unq (P _ n _)

1525+ | n `elem` unq = -- the unquoted names have been claimed as TT already - just use them

1526+ do fill (Var n) ; solve

1527+ | otherwise =

1528+ do tyannot <- claimTT (sMN 0 "pTyAnnot")

1529+ movelast tyannot -- use a _ pattern here

1530+ nt <- getNameFrom (sMN 0 "nt")

1531+ claim nt (Var (reflm "NameType"))

1532+ movelast nt -- use a _ pattern here

1533+ n' <- getNameFrom (sMN 0 "n")

1534+ claim n' (Var (reflm "TTName"))

1535+ fill $ reflCall "P" [Var nt, Var n', Var tyannot]

1536+ solve

1537+ focus n'; reflectNameQuotePattern n

1538+reflectQuotePattern unq (V n)

1539+ = do fill $ reflCall "V" [RConstant (I n)]

1540+ solve

1541+reflectQuotePattern unq (Bind n b x)

1542+ = do x' <- claimTT (sMN 0 "sc")

1543+ movelast x'

1544+ b' <- getNameFrom (sMN 0 "binder")

1545+ claim b' (RApp (Var (sNS (sUN "Binder") ["Reflection", "Language"]))

1546+ (Var (sNS (sUN "TT") ["Reflection", "Language"])))

1547+ if n `elem` freeNames x

1548+ then do fill $ reflCall "Bind"

1549+ [reflectName n,

1550+ Var b',

1551+ Var x']

1552+ solve

1553+ else do any <- claimTT (sMN 0 "any")

1554+ movelast any

1555+ fill $ reflCall "Bind"

1556+ [Var any,

1557+ Var b',

1558+ Var x']

1559+ solve

1560+ focus x'; reflectQuotePattern unq x

1561+ focus b'; reflectBinderQuotePattern unq b

1562+

1563+ where

1564+ reflectBinderQuotePattern :: [Name] -> Binder Term -> ElabD ()

1565+ reflectBinderQuotePattern unq (Lam t)

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

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

1568+ solve

1569+ focus t'; reflectQuotePattern unq t

1570+ reflectBinderQuotePattern unq (Pi t)

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

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

1573+ solve

1574+ focus t'; reflectQuotePattern unq t

1575+ reflectBinderQuotePattern unq (Let x y)

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

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

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

1579+ solve

1580+ focus x'; reflectQuotePattern unq x

1581+ focus y'; reflectQuotePattern unq y

1582+ reflectBinderQuotePattern unq (NLet x y)

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

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

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

1586+ solve

1587+ focus x'; reflectQuotePattern unq x

1588+ focus y'; reflectQuotePattern unq y

1589+ reflectBinderQuotePattern unq (Hole t)

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

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

1592+ solve

1593+ focus t'; reflectQuotePattern unq t

1594+ reflectBinderQuotePattern unq (GHole _ t)

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

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

1597+ solve

1598+ focus t'; reflectQuotePattern unq t

1599+ reflectBinderQuotePattern unq (Guess x y)

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

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

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

1603+ solve

1604+ focus x'; reflectQuotePattern unq x

1605+ focus y'; reflectQuotePattern unq y

1606+ reflectBinderQuotePattern unq (PVar t)

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

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

1609+ solve

1610+ focus t'; reflectQuotePattern unq t

1611+ reflectBinderQuotePattern unq (PVTy t)

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

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

1614+ solve

1615+ focus t'; reflectQuotePattern unq t

1616+reflectQuotePattern unq (App f x)

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

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

1619+ fill $ reflCall "App" [Var f', Var x']

1620+ solve

1621+ focus f'; reflectQuotePattern unq f

1622+ focus x'; reflectQuotePattern unq x

1623+reflectQuotePattern unq (Constant c)

1624+ = do fill $ reflCall "TConst" [reflectConstant c]

1625+ solve

1626+reflectQuotePattern unq (Proj t i)

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

1628+ fill $ reflCall "Proj" [Var t', RConstant (I i)]

1629+ solve

1630+ focus t'; reflectQuotePattern unq t

1631+reflectQuotePattern unq (Erased)

1632+ = do erased <- claimTT (sMN 0 "erased")

1633+ movelast erased

1634+ fill $ (Var erased)

1635+ solve

1636+reflectQuotePattern unq (Impossible)

1637+ = do fill $ Var (reflm "Impossible")

1638+ solve

1639+reflectQuotePattern unq (TType exp)

1640+ = do ue <- getNameFrom (sMN 0 "uexp")

1641+ claim ue (Var (sNS (sUN "TTUExp") ["Reflection", "Language"]))

1642+ movelast ue

1643+ fill $ reflCall "TType" [Var ue]

1644+ solve

1645+

1512-- | Create a reflected term, but leave refs to the provided name intact

1646-- | Create a reflected term, but leave refs to the provided name intact

1513reflectQuote :: [Name] -> Term -> Raw

1647reflectQuote :: [Name] -> Term -> Raw

1514reflectQuote unq (P nt n t)

1648reflectQuote unq (P nt n t)

@@ -1517,7 +1651,7 @@ reflectQuote unq (P nt n t)

1517reflectQuote unq (V n)

1651reflectQuote unq (V n)

1518 = reflCall "V" [RConstant (I n)]

1652 = reflCall "V" [RConstant (I n)]

1519reflectQuote unq (Bind n b x)

1653reflectQuote unq (Bind n b x)

1520− = reflCall "Bind" [reflectName n, reflectBinder b, reflectQuote unq x]

1654+ = reflCall "Bind" [reflectName n, reflectBinderQuote unq b, reflectQuote unq x]

1521reflectQuote unq (App f x)

1655reflectQuote unq (App f x)

1522 = reflCall "App" [reflectQuote unq f, reflectQuote unq x]

1656 = reflCall "App" [reflectQuote unq f, reflectQuote unq x]

1523reflectQuote unq (Constant c)

1657reflectQuote unq (Constant c)

@@ -1553,6 +1687,22 @@ reflectName (MN i n)

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

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

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

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

1555

1689

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

1691+-- while all others become _

1692+reflectNameQuotePattern :: Name -> ElabD ()

1693+reflectNameQuotePattern n@(UN s)

1694+ = do fill $ reflectName n

1695+ solve

1696+reflectNameQuotePattern n@(NS _ _)

1697+ = do fill $ reflectName n

1698+ solve

1699+reflectNameQuotePattern _ -- for all other names, match any

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

1701+ claim nameHole (Var (reflm "TTName"))

1702+ movelast nameHole

1703+ fill (Var nameHole)

1704+ solve

1705+

1556reflectBinder :: Binder Term -> Raw

1706reflectBinder :: Binder Term -> Raw

1557reflectBinder = reflectBinderQuote []

1707reflectBinder = reflectBinderQuote []

1558

1708