f1ff8fb · Idris-dev · git.iko.soy

994 [Name] -> -- all names

995 [Name] -> -- names with no declaration

996 PTerm -> PTerm

997−expandParams dec ps ns infs tm = en tm

997+expandParams dec ps ns infs tm = en 0 tm

998 where

999 -- if we shadow a name (say in a lambda binding) that is used in a call to

1000 -- a lifted function, we need access to both names - once in the scope of the

1006 mkShadow (MN i n) = MN (i+1) n

1007 mkShadow (NS x s) = NS (mkShadow x) s

1008

1009+ en :: Int -- ^ The quotation level - only transform terms that are used, not terms

1010+ -- that are merely mentioned.

1011+ -> PTerm -> PTerm

1009− en (PLam fc n nfc t s)

1012+ en 0 (PLam fc n nfc t s)

1010 | n `elem` (map fst ps ++ ns)

1013 | n `elem` (map fst ps ++ ns)

1011 = let n' = mkShadow n in

1014 = let n' = mkShadow n in

1012− PLam fc n' nfc (en t) (en (shadow n n' s))

1015+ PLam fc n' nfc (en 0 t) (en 0 (shadow n n' s))

1013− | otherwise = PLam fc n nfc (en t) (en s)

1016+ | otherwise = PLam fc n nfc (en 0 t) (en 0 s)

1014− en (PPi p n nfc t s)

1017+ en 0 (PPi p n nfc t s)

1015 | n `elem` (map fst ps ++ ns)

1018 | n `elem` (map fst ps ++ ns)

1016 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?

1019 = let n' = mkShadow n in -- TODO THINK SHADOWING TacImp?

1017− PPi (enTacImp p) n' nfc (en t) (en (shadow n n' s))

1020+ PPi (enTacImp 0 p) n' nfc (en 0 t) (en 0 (shadow n n' s))

1018− | otherwise = PPi (enTacImp p) n nfc (en t) (en s)

1021+ | otherwise = PPi (enTacImp 0 p) n nfc (en 0 t) (en 0 s)

1019− en (PLet fc n nfc ty v s)

1022+ en 0 (PLet fc n nfc ty v s)

1020 | n `elem` (map fst ps ++ ns)

1023 | n `elem` (map fst ps ++ ns)

1021 = let n' = mkShadow n in

1024 = let n' = mkShadow n in

1022− PLet fc n' nfc (en ty) (en v) (en (shadow n n' s))

1025+ PLet fc n' nfc (en 0 ty) (en 0 v) (en 0 (shadow n n' s))

1023− | otherwise = PLet fc n nfc (en ty) (en v) (en s)

1026+ | otherwise = PLet fc n nfc (en 0 ty) (en 0 v) (en 0 s)

1024 -- FIXME: Should only do this in a type signature!

1027 -- 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)

1026 | n `elem` (map fst ps ++ ns) && t /= Placeholder

1029 | n `elem` (map fst ps ++ ns) && t /= Placeholder

1027 = let n' = mkShadow n in

1030 = let n' = mkShadow n in

1028− PDPair f hls p (PRef f' fcs n') (en t) (en (shadow n n' r))

1031+ PDPair f hls p (PRef f' fcs n') (en 0 t) (en 0 (shadow n n' r))

1029− en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)

1032+ en 0 (PRewrite f l r g) = PRewrite f (en 0 l) (en 0 r) (fmap (en 0) g)

1030− en (PTyped l r) = PTyped (en l) (en r)

1033+ en 0 (PTyped l r) = PTyped (en 0 l) (en 0 r)

1031− en (PPair f hls p l r) = PPair f hls p (en l) (en r)

1034+ en 0 (PPair f hls p l r) = PPair f hls p (en 0 l) (en 0 r)

1032− en (PDPair f hls p l t r) = PDPair f hls p (en l) (en t) (en r)

1035+ en 0 (PDPair f hls p l t r) = PDPair f hls p (en 0 l) (en 0 t) (en 0 r)

1033− en (PAlternative ns a as) = PAlternative ns a (map en as)

1036+ en 0 (PAlternative ns a as) = PAlternative ns a (map (en 0) as)

1034− en (PHidden t) = PHidden (en t)

1037+ en 0 (PHidden t) = PHidden (en 0 t)

1035− en (PUnifyLog t) = PUnifyLog (en t)

1038+ en 0 (PUnifyLog t) = PUnifyLog (en 0 t)

1036− en (PDisamb ds t) = PDisamb ds (en t)

1039+ en 0 (PDisamb ds t) = PDisamb ds (en 0 t)

1037− en (PNoImplicits t) = PNoImplicits (en t)

1040+ en 0 (PNoImplicits t) = PNoImplicits (en 0 t)

1038− en (PDoBlock ds) = PDoBlock (map (fmap en) ds)

1041+ en 0 (PDoBlock ds) = PDoBlock (map (fmap (en 0)) ds)

1039− en (PProof ts) = PProof (map (fmap en) ts)

1042+ en 0 (PProof ts) = PProof (map (fmap (en 0)) ts)

1040− en (PTactics ts) = PTactics (map (fmap en) ts)

1043+ en 0 (PTactics ts) = PTactics (map (fmap (en 0)) ts)

1041−

1044+

1042− en (PQuote (Var n))

1045+ en 0 (PQuote (Var n))

1043 | n `nselem` ns = PQuote (Var (dec n))

1046 | 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)

1045 | n `nselem` ns = PApp fc (PInferRef fc' hl (dec n))

1048 | n `nselem` ns = PApp fc (PInferRef fc' hl (dec n))

1046− (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap en) as))

1049+ (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))

1047− en (PApp fc (PRef fc' hl n) as)

1050+ en 0 (PApp fc (PRef fc' hl n) as)

1048 | n `elem` infs = PApp fc (PInferRef fc' hl (dec n))

1051 | 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))

1050 | n `nselem` ns = PApp fc (PRef fc' hl (dec n))

1053 | n `nselem` ns = PApp fc (PRef fc' hl (dec n))

1051− (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap en) as))

1054+ (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))

1052− en (PAppBind fc (PRef fc' hl n) as)

1055+ en 0 (PAppBind fc (PRef fc' hl n) as)

1053 | n `elem` infs = PAppBind fc (PInferRef fc' hl (dec n))

1056 | 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))

1055 | n `nselem` ns = PAppBind fc (PRef fc' hl (dec n))

1058 | n `nselem` ns = PAppBind fc (PRef fc' hl (dec n))

1056− (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap en) as))

1059+ (map (pexp . (PRef fc hl)) (map fst ps) ++ (map (fmap (en 0)) as))

1057− en (PRef fc hl n)

1060+ en 0 (PRef fc hl n)

1058 | n `elem` infs = PApp fc (PInferRef fc hl (dec n))

1061 | n `elem` infs = PApp fc (PInferRef fc hl (dec n))

1059 (map (pexp . (PRef fc hl)) (map fst ps))

1062 (map (pexp . (PRef fc hl)) (map fst ps))

1060 | n `nselem` ns = PApp fc (PRef fc hl (dec n))

1063 | n `nselem` ns = PApp fc (PRef fc hl (dec n))

1061 (map (pexp . (PRef fc hl)) (map fst ps))

1064 (map (pexp . (PRef fc hl)) (map fst ps))

1062− en (PInferRef fc hl n)

1065+ en 0 (PInferRef fc hl n)

1063 | n `nselem` ns = PApp fc (PInferRef fc hl (dec n))

1066 | n `nselem` ns = PApp fc (PInferRef fc hl (dec n))

1064 (map (pexp . (PRef fc hl)) (map fst ps))

1067 (map (pexp . (PRef fc hl)) (map fst ps))

1065− en (PApp fc f as) = PApp fc (en f) (map (fmap en) as)

1068+ en 0 (PApp fc f as) = PApp fc (en 0 f) (map (fmap (en 0)) as)

1066− en (PAppBind fc f as) = PAppBind fc (en f) (map (fmap en) as)

1069+ en 0 (PAppBind fc f as) = PAppBind fc (en 0 f) (map (fmap (en 0)) as)

1067− en (PCase fc c os) = PCase fc (en c) (map (pmap en) os)

1070+ en 0 (PCase fc c os) = PCase fc (en 0 c) (map (pmap (en 0)) os)

1068− en (PIfThenElse fc c t f) = PIfThenElse fc (en c) (en t) (en f)

1071+ en 0 (PIfThenElse fc c t f) = PIfThenElse fc (en 0 c) (en 0 t) (en 0 f)

1069− en (PRunElab fc tm ns) = PRunElab fc (en tm) ns

1072+ en 0 (PRunElab fc tm ns) = PRunElab fc (en 0 tm) ns

1070− en (PConstSugar fc tm) = PConstSugar fc (en tm)

1073+ en 0 (PConstSugar fc tm) = PConstSugar fc (en 0 tm)

1071− en t = t

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

1072

1079

1073 nselem x [] = False

1080 nselem x [] = False

1074 nselem x (y : xs) | nseq x y = True

1081 nselem x (y : xs) | nseq x y = True

1076

1083

1077 nseq x y = nsroot x == nsroot y

1084 nseq x y = nsroot x == nsroot y

1078

1085

1079− enTacImp (TacImp aos st scr) = TacImp aos st (en scr)

1086+ enTacImp ql (TacImp aos st scr) = TacImp aos st (en ql scr)

1080− enTacImp other = other

1087+ enTacImp ql other = other

1081

1088

1082expandParamsD :: Bool -> -- True = RHS only

1089expandParamsD :: Bool -> -- True = RHS only

1083 IState ->

1090 IState ->