ee11033 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Elaborate quasiquote patterns to something useful

This causes parts of the terms that either vary unpredictably or don't contain interesting information to be elaborated to _ in a pattern-match context.

commitee11033af732991f7932f0a918bd2fc0a4e876de authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 26 Jun 2014, 17:53 (12 years ago) parent6e3fd45

3 files changed+229−76

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+67−65 src/Idris/Core/Elaborate.hs+1 src/Idris/ElabTerm.hs+161−11

src/Idris/AbsSyntax.hs+67−65

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

12801280-- and *not* inside a PHidden

12811281

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

1283−addImpl' inpat env infns ist ptm

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

1283+addImpl' inpat env infns ist ptm

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

12851285 where

1286− ai env ds (PRef fc f)

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

1287+ ai qq env ds (PRef fc f)

12871288 | f `elem` infns = PInferRef fc f

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

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

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

1291− ai env ds (PEq fc l r)

1292− = let l' = ai env ds l

1293− r' = ai env ds r in

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

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

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

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

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

1294+ r' = ai qq env ds r in

12941295 PEq fc l' r'

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

1296− = let l' = ai env ds l

1297− r' = ai env ds r

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

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

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

1298+ r' = ai qq env ds r

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

12991300 PRewrite fc l' r' g'

1300− ai env ds (PTyped l r)

1301− = let l' = ai env ds l

1302− r' = ai env ds r in

1301+ ai qq env ds (PTyped l r)

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

1303+ r' = ai qq env ds r in

13031304 PTyped l' r'

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

1305− = let l' = ai env ds l

1306− r' = ai env ds r in

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

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

1307+ r' = ai qq env ds r in

13071308 PPair fc p l' r'

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

1309− = let l' = ai env ds l

1310− t' = ai env ds t

1311− r' = ai env ds r in

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

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

1311+ t' = ai qq env ds t

1312+ r' = ai qq env ds r in

13121313 PDPair fc p l' t' r'

1313− ai env ds (PAlternative a as)

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

1314+ ai qq env ds (PAlternative a as)

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

13151316 PAlternative a as'

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

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

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

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

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

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

13191320 PApp fc (PInferRef fc f) as'

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

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

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

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

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

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

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

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

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

13251326 | 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

13271328 arity = getPArity ty in

13281329 mkPApp fc arity ftm as'

1329− ai env ds (PApp fc f as)

1330− = let f' = ai env ds f

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

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

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

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

13321333 mkPApp fc 1 f' as'

1333− ai env ds (PCase fc c os)

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

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

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

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

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

13371338 -- information

13381339 PCase fc c' os

1339− ai env ds (PLam n ty sc)

1340− = let ty' = ai env ds ty

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

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

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

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

13421343 PLam n ty' sc'

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

1344− = let ty' = ai env ds ty

1345− val' = ai env ds val

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

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

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

1346+ val' = ai qq env ds val

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

13471348 PLet n ty' val' sc'

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

1349− = let ty' = ai env ds ty

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

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

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

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

13511352 PPi p n ty' sc'

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

1353− = let r' = ai env ds r

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

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

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

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

13551356 PGoal fc r' n sc'

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

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

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

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

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

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

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

1363− ai env ds tm = tm

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

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

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

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

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

1362+ ai qq env ds (PNoImplicits tm) = PNoImplicits (ai qq 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)

1365+ ai qq env ds tm = tm

13641366

13651367 handleErr (Left err) = PElabError err

13661368 handleErr (Right x) = x

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

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

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

13701372

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

1372−aiFn inpat True ist fc f ds []

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

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

13731375 = case lookupDef f (tt_ctxt ist) of

13741376 [] -> Right $ PPatvar fc f

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

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

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

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

13791381-- 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

13811383 else Right $ PPatvar fc f

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

13831385 imp _ = True

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

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

13871389 constructor _ = False

13881390

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

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

13901392

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

13921394 vname _ = False

13931395

1394−aiFn inpat expat ist fc f ds as

1396+aiFn inpat expat qq ist fc f ds as

13951397 | 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

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

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

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

src/Idris/Core/Elaborate.hs+1

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

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

381381equiv tm = processTactic' (Equiv tm)

382382

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

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

384385patvar n = do env <- get_env

385386 hs <- get_holes

src/Idris/ElabTerm.hs+161−11

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

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

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

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

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

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

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

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

298298 = do ctxt <- get_context

299299 let defined = case lookupTy n ctxt of

300300 [] -> False

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

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

641641 -- fresh names in the quasiquoted term

642642 (t, unq) <- extractUnquotes t

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

644643 let unquoteNames = map fst unq

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

645+

645646

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

647648 -- avoid capture

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

676677 focus qTm

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

678679 end_unify

680+

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

680682 -- original goal

681683 env <- get_env

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

683−

684− case qTerm of

685− Just q -> do loadState

686− fill q

687− solve

688− mapM_ elabUnquote unq

684+ loadState

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

686+ Just q

687+ | pattern -> reflectQuotePattern unquoteNames q

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

689+ solve

689690 Nothing -> fail "Broken elaboration of quasiquote"

691+ mapM_ elabUnquote unq

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

691693

692694 elabUnquote (n, tm)

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

15091511reflect :: Term -> Raw

15101512reflect = reflectQuote []

15111513

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+

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

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

15141648reflectQuote unq (P nt n t)

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

15171651reflectQuote unq (V n)

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

15191653reflectQuote 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]

15211655reflectQuote unq (App f x)

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

15231657reflectQuote unq (Constant c)

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

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

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

15551689

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+

15561706reflectBinder :: Binder Term -> Raw

15571707reflectBinder = reflectBinderQuote []

15581708