@@ -982,7 +982,7 @@ expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
982982 [Name] -> -- all names
983983 [Name] -> -- names with no declaration
984984 PTerm -> PTerm
985−expandParams dec ps ns infs tm = en tm
985+expandParams dec ps ns infs tm = en 0 tm
986986 where
987987 -- if we shadow a name (say in a lambda binding) that is used in a call to
988988 -- a lifted function, we need access to both names - once in the scope of the
@@ -994,69 +994,76 @@ expandParams dec ps ns infs tm = en tm
994994 mkShadow (MN i n) = MN (i+1) n
995995 mkShadow (NS x s) = NS (mkShadow x) s
996996
997− en (PLam fc n nfc t s)
997+ en :: Int -- ^ The quotation level - only transform terms that are used, not terms
998+ -- that are merely mentioned.
999+ -> PTerm -> PTerm
1000+ en 0 (PLam fc n nfc t s)
9981001 | n `elem` (map fst ps ++ ns)
9991002 = let n' = mkShadow n in
1000− PLam fc n' nfc (en t) (en (shadow n n' s))
1001− | otherwise = PLam fc n nfc (en t) (en s)
1002− en (PPi p n nfc t s)
1003+ PLam fc n' nfc (en 0 t) (en 0 (shadow n n' s))
1004+ | otherwise = PLam fc n nfc (en 0 t) (en 0 s)
1005+ en 0 (PPi p n nfc t s)
10031006 | n `elem` (map fst ps ++ ns)
10041007 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
1005− PPi (enTacImp p) n' nfc (en t) (en (shadow n n' s))
1006− | otherwise = PPi (enTacImp p) n nfc (en t) (en s)
1007− en (PLet fc n nfc ty v s)
1008+ PPi (enTacImp 0 p) n' nfc (en 0 t) (en 0 (shadow n n' s))
1009+ | otherwise = PPi (enTacImp 0 p) n nfc (en 0 t) (en 0 s)
1010+ en 0 (PLet fc n nfc ty v s)
10081011 | n `elem` (map fst ps ++ ns)
10091012 = let n' = mkShadow n in
1010− PLet fc n' nfc (en ty) (en v) (en (shadow n n' s))
1011− | otherwise = PLet fc n nfc (en ty) (en v) (en s)
1013+ PLet fc n' nfc (en 0 ty) (en 0 v) (en 0 (shadow n n' s))
1014+ | otherwise = PLet fc n nfc (en 0 ty) (en 0 v) (en 0 s)
10121015 -- FIXME: Should only do this in a type signature!
1013− en (PDPair f hls p (PRef f' fcs n) t r)
1016+ en 0 (PDPair f hls p (PRef f' fcs n) t r)
10141017 | n `elem` (map fst ps ++ ns) && t /= Placeholder
10151018 = let n' = mkShadow n in
1016− PDPair f hls p (PRef f' fcs n') (en t) (en (shadow n n' r))
1017− en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
1018− en (PTyped l r) = PTyped (en l) (en r)
1019− en (PPair f hls p l r) = PPair f hls p (en l) (en r)
1020− en (PDPair f hls p l t r) = PDPair f hls p (en l) (en t) (en r)
1021− en (PAlternative ns a as) = PAlternative ns a (map en as)
1022− en (PHidden t) = PHidden (en t)
1023− en (PUnifyLog t) = PUnifyLog (en t)
1024− en (PDisamb ds t) = PDisamb ds (en t)
1025− en (PNoImplicits t) = PNoImplicits (en t)
1026− en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
1027− en (PProof ts) = PProof (map (fmap en) ts)
1028− en (PTactics ts) = PTactics (map (fmap en) ts)
1029−
1030− en (PQuote (Var n))
1019+ PDPair f hls p (PRef f' fcs n') (en 0 t) (en 0 (shadow n n' r))
1020+ en 0 (PRewrite f l r g) = PRewrite f (en 0 l) (en 0 r) (fmap (en 0) g)
1021+ en 0 (PTyped l r) = PTyped (en 0 l) (en 0 r)
1022+ en 0 (PPair f hls p l r) = PPair f hls p (en 0 l) (en 0 r)
1023+ en 0 (PDPair f hls p l t r) = PDPair f hls p (en 0 l) (en 0 t) (en 0 r)
1024+ en 0 (PAlternative ns a as) = PAlternative ns a (map (en 0) as)
1025+ en 0 (PHidden t) = PHidden (en 0 t)
1026+ en 0 (PUnifyLog t) = PUnifyLog (en 0 t)
1027+ en 0 (PDisamb ds t) = PDisamb ds (en 0 t)
1028+ en 0 (PNoImplicits t) = PNoImplicits (en 0 t)
1029+ en 0 (PDoBlock ds) = PDoBlock (map (fmap (en 0)) ds)
1030+ en 0 (PProof ts) = PProof (map (fmap (en 0)) ts)
1031+ en 0 (PTactics ts) = PTactics (map (fmap (en 0)) ts)
1032+
1033+ en 0 (PQuote (Var n))
10311034 | n `nselem` ns = PQuote (Var (dec n))
1032− en (PApp fc (PInferRef fc' hl n) as)
1035+ en 0 (PApp fc (PInferRef fc' hl n) as)
10331036 | n `nselem` ns = PApp fc (PInferRef fc' hl (dec n))
1034− (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap en) as))
1035− en (PApp fc (PRef fc' hl n) as)
1037+ (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))
1038+ en 0 (PApp fc (PRef fc' hl n) as)
10361039 | n `elem` infs = PApp fc (PInferRef fc' hl (dec n))
1037− (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap en) as))
1040+ (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))
10381041 | n `nselem` ns = PApp fc (PRef fc' hl (dec n))
1039− (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap en) as))
1040− en (PAppBind fc (PRef fc' hl n) as)
1042+ (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))
1043+ en 0 (PAppBind fc (PRef fc' hl n) as)
10411044 | n `elem` infs = PAppBind fc (PInferRef fc' hl (dec n))
1042− (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap en) as))
1045+ (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))
10431046 | n `nselem` ns = PAppBind fc (PRef fc' hl (dec n))
1044− (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap en) as))
1045− en (PRef fc hl n)
1047+ (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))
1048+ en 0 (PRef fc hl n)
10461049 | n `elem` infs = PApp fc (PInferRef fc hl (dec n))
10471050 (map (pexp . (PRef fc hl)) (map fst ps))
10481051 | n `nselem` ns = PApp fc (PRef fc hl (dec n))
10491052 (map (pexp . (PRef fc hl)) (map fst ps))
1050− en (PInferRef fc hl n)
1053+ en 0 (PInferRef fc hl n)
10511054 | n `nselem` ns = PApp fc (PInferRef fc hl (dec n))
10521055 (map (pexp . (PRef fc hl)) (map fst ps))
1053− en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
1054− en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
1055− en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
1056− en (PIfThenElse fc c t f) = PIfThenElse fc (en c) (en t) (en f)
1057− en (PRunElab fc tm ns) = PRunElab fc (en tm) ns
1058− en (PConstSugar fc tm) = PConstSugar fc (en tm)
1059− en t = t
1056+ en 0 (PApp fc f as) = PApp fc (en 0 f) (map (fmap (en 0)) as)
1057+ en 0 (PAppBind fc f as) = PAppBind fc (en 0 f) (map (fmap (en 0)) as)
1058+ en 0 (PCase fc c os) = PCase fc (en 0 c) (map (pmap (en 0)) os)
1059+ en 0 (PIfThenElse fc c t f) = PIfThenElse fc (en 0 c) (en 0 t) (en 0 f)
1060+ en 0 (PRunElab fc tm ns) = PRunElab fc (en 0 tm) ns
1061+ en 0 (PConstSugar fc tm) = PConstSugar fc (en 0 tm)
1062+
1063+ en ql (PQuasiquote tm ty) = PQuasiquote (en (ql + 1) tm) (fmap (en ql) ty)
1064+ en ql (PUnquote tm) = PUnquote (en (ql - 1) tm)
1065+
1066+ en ql t = descend (en ql) t
10601067
10611068 nselem x [] = False
10621069 nselem x (y : xs) | nseq x y = True
@@ -1064,8 +1071,8 @@ expandParams dec ps ns infs tm = en tm
10641071
10651072 nseq x y = nsroot x == nsroot y
10661073
1067− enTacImp (TacImp aos st scr) = TacImp aos st (en scr)
1068− enTacImp other = other
1074+ enTacImp ql (TacImp aos st scr) = TacImp aos st (en ql scr)
1075+ enTacImp ql other = other
10691076
10701077expandParamsD :: Bool -> -- True = RHS only
10711078 IState ->