@@ -994,7 +994,7 @@ expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
994994 [Name] -> -- all names
995995 [Name] -> -- names with no declaration
996996 PTerm -> PTerm
997−expandParams dec ps ns infs tm = en tm
997+expandParams dec ps ns infs tm = en 0 tm
998998 where
999999 -- if we shadow a name (say in a lambda binding) that is used in a call to
10001000 -- a lifted function, we need access to both names - once in the scope of the
@@ -1006,69 +1006,76 @@ expandParams dec ps ns infs tm = en tm
10061006 mkShadow (MN i n) = MN (i+1) n
10071007 mkShadow (NS x s) = NS (mkShadow x) s
10081008
1009− en (PLam fc n nfc t s)
1009+ en :: Int -- ^ The quotation level - only transform terms that are used, not terms
1010+ -- that are merely mentioned.
1011+ -> PTerm -> PTerm
1012+ en 0 (PLam fc n nfc t s)
10101013 | n `elem` (map fst ps ++ ns)
10111014 = let n' = mkShadow n in
1012− PLam fc n' nfc (en t) (en (shadow n n' s))
1013− | otherwise = PLam fc n nfc (en t) (en s)
1014− en (PPi p n nfc t s)
1015+ PLam fc n' nfc (en 0 t) (en 0 (shadow n n' s))
1016+ | otherwise = PLam fc n nfc (en 0 t) (en 0 s)
1017+ en 0 (PPi p n nfc t s)
10151018 | n `elem` (map fst ps ++ ns)
10161019 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?
1017− PPi (enTacImp p) n' nfc (en t) (en (shadow n n' s))
1018− | otherwise = PPi (enTacImp p) n nfc (en t) (en s)
1019− en (PLet fc n nfc ty v s)
1020+ PPi (enTacImp 0 p) n' nfc (en 0 t) (en 0 (shadow n n' s))
1021+ | otherwise = PPi (enTacImp 0 p) n nfc (en 0 t) (en 0 s)
1022+ en 0 (PLet fc n nfc ty v s)
10201023 | n `elem` (map fst ps ++ ns)
10211024 = let n' = mkShadow n in
1022− PLet fc n' nfc (en ty) (en v) (en (shadow n n' s))
1023− | otherwise = PLet fc n nfc (en ty) (en v) (en s)
1025+ PLet fc n' nfc (en 0 ty) (en 0 v) (en 0 (shadow n n' s))
1026+ | otherwise = PLet fc n nfc (en 0 ty) (en 0 v) (en 0 s)
10241027 -- FIXME: Should only do this in a type signature!
1025− en (PDPair f hls p (PRef f' fcs n) t r)
1028+ en 0 (PDPair f hls p (PRef f' fcs n) t r)
10261029 | n `elem` (map fst ps ++ ns) && t /= Placeholder
10271030 = let n' = mkShadow n in
1028− PDPair f hls p (PRef f' fcs n') (en t) (en (shadow n n' r))
1029− en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)
1030− en (PTyped l r) = PTyped (en l) (en r)
1031− en (PPair f hls p l r) = PPair f hls p (en l) (en r)
1032− en (PDPair f hls p l t r) = PDPair f hls p (en l) (en t) (en r)
1033− en (PAlternative ns a as) = PAlternative ns a (map en as)
1034− en (PHidden t) = PHidden (en t)
1035− en (PUnifyLog t) = PUnifyLog (en t)
1036− en (PDisamb ds t) = PDisamb ds (en t)
1037− en (PNoImplicits t) = PNoImplicits (en t)
1038− en (PDoBlock ds) = PDoBlock (map (fmap en) ds)
1039− en (PProof ts) = PProof (map (fmap en) ts)
1040− en (PTactics ts) = PTactics (map (fmap en) ts)
1041−
1042− en (PQuote (Var n))
1031+ PDPair f hls p (PRef f' fcs n') (en 0 t) (en 0 (shadow n n' r))
1032+ en 0 (PRewrite f l r g) = PRewrite f (en 0 l) (en 0 r) (fmap (en 0) g)
1033+ en 0 (PTyped l r) = PTyped (en 0 l) (en 0 r)
1034+ en 0 (PPair f hls p l r) = PPair f hls p (en 0 l) (en 0 r)
1035+ en 0 (PDPair f hls p l t r) = PDPair f hls p (en 0 l) (en 0 t) (en 0 r)
1036+ en 0 (PAlternative ns a as) = PAlternative ns a (map (en 0) as)
1037+ en 0 (PHidden t) = PHidden (en 0 t)
1038+ en 0 (PUnifyLog t) = PUnifyLog (en 0 t)
1039+ en 0 (PDisamb ds t) = PDisamb ds (en 0 t)
1040+ en 0 (PNoImplicits t) = PNoImplicits (en 0 t)
1041+ en 0 (PDoBlock ds) = PDoBlock (map (fmap (en 0)) ds)
1042+ en 0 (PProof ts) = PProof (map (fmap (en 0)) ts)
1043+ en 0 (PTactics ts) = PTactics (map (fmap (en 0)) ts)
1044+
1045+ en 0 (PQuote (Var n))
10431046 | n `nselem` ns = PQuote (Var (dec n))
1044− en (PApp fc (PInferRef fc' hl n) as)
1047+ en 0 (PApp fc (PInferRef fc' hl n) as)
10451048 | n `nselem` ns = PApp fc (PInferRef fc' hl (dec n))
1046− (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap en) as))
1047− en (PApp fc (PRef fc' hl n) as)
1049+ (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))
1050+ en 0 (PApp fc (PRef fc' hl n) as)
10481051 | n `elem` infs = PApp fc (PInferRef fc' hl (dec n))
1049− (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap en) as))
1052+ (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))
10501053 | n `nselem` ns = PApp fc (PRef fc' hl (dec n))
1051− (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap en) as))
1052− en (PAppBind fc (PRef fc' hl n) as)
1054+ (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))
1055+ en 0 (PAppBind fc (PRef fc' hl n) as)
10531056 | n `elem` infs = PAppBind fc (PInferRef fc' hl (dec n))
1054− (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap en) as))
1057+ (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))
10551058 | n `nselem` ns = PAppBind fc (PRef fc' hl (dec n))
1056− (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap en) as))
1057− en (PRef fc hl n)
1059+ (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))
1060+ en 0 (PRef fc hl n)
10581061 | n `elem` infs = PApp fc (PInferRef fc hl (dec n))
10591062 (map (pexp . (PRef fc hl)) (map fst ps))
10601063 | n `nselem` ns = PApp fc (PRef fc hl (dec n))
10611064 (map (pexp . (PRef fc hl)) (map fst ps))
1062− en (PInferRef fc hl n)
1065+ en 0 (PInferRef fc hl n)
10631066 | n `nselem` ns = PApp fc (PInferRef fc hl (dec n))
10641067 (map (pexp . (PRef fc hl)) (map fst ps))
1065− en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)
1066− en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)
1067− en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)
1068− en (PIfThenElse fc c t f) = PIfThenElse fc (en c) (en t) (en f)
1069− en (PRunElab fc tm ns) = PRunElab fc (en tm) ns
1070− en (PConstSugar fc tm) = PConstSugar fc (en tm)
1071− en t = t
1068+ en 0 (PApp fc f as) = PApp fc (en 0 f) (map (fmap (en 0)) as)
1069+ en 0 (PAppBind fc f as) = PAppBind fc (en 0 f) (map (fmap (en 0)) as)
1070+ en 0 (PCase fc c os) = PCase fc (en 0 c) (map (pmap (en 0)) os)
1071+ en 0 (PIfThenElse fc c t f) = PIfThenElse fc (en 0 c) (en 0 t) (en 0 f)
1072+ en 0 (PRunElab fc tm ns) = PRunElab fc (en 0 tm) ns
1073+ en 0 (PConstSugar fc tm) = PConstSugar fc (en 0 tm)
1074+
1075+ en ql (PQuasiquote tm ty) = PQuasiquote (en (ql + 1) tm) (fmap (en ql) ty)
1076+ en ql (PUnquote tm) = PUnquote (en (ql - 1) tm)
1077+
1078+ en ql t = descend (en ql) t
10721079
10731080 nselem x [] = False
10741081 nselem x (y : xs) | nseq x y = True
@@ -1076,8 +1083,8 @@ expandParams dec ps ns infs tm = en tm
10761083
10771084 nseq x y = nsroot x == nsroot y
10781085
1079− enTacImp (TacImp aos st scr) = TacImp aos st (en scr)
1080− enTacImp other = other
1086+ enTacImp ql (TacImp aos st scr) = TacImp aos st (en ql scr)
1087+ enTacImp ql other = other
10811088
10821089expandParamsD :: Bool -> -- True = RHS only
10831090 IState ->