b1028f0 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

TacImp script handling to various functions.

Namely, expandParams and the various 'namesIn' funcs. Some of the latter could possibly use some review -- see FIXMEs in AbsSyntaxTree.hs

commitb1028f0074ebd6c2477d94afcc7d2919f6986d02 authorTimo Petteri Sinnemäki <timo.sinnemaki@helsinki.fi> dateFri 28 Mar 2014, 15:28 (13 years ago) parent569a30c

2 files changed+25−10

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+6−3 src/Idris/AbsSyntaxTree.hs+19−7

src/Idris/AbsSyntax.hs+6−3

@@ -945,9 +945,9 @@ expandParams dec ps ns infs tm = en tm

945945 | otherwise = PLam n (en t) (en s)

946946 en (PPi p n t s)

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

948− = let n' = mkShadow n in

949− PPi p n' (en t) (en (shadow n n' s))

950− | otherwise = PPi p n (en t) (en s)

948+ = let n' = mkShadow n in -- FIXME THINK SHADOWING TacImp?

949+ PPi (enTacImp p) n' (en t) (en (shadow n n' s))

950+ | otherwise = PPi (enTacImp p) n (en t) (en s)

951951 en (PLet n ty v s)

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

953953 = let n' = mkShadow n in

@@ -1006,6 +1006,9 @@ expandParams dec ps ns infs tm = en tm

10061006

10071007 nseq x y = nsroot x == nsroot y

10081008

1009+ enTacImp (TacImp aos st scr) = TacImp aos st (en scr)

1010+ enTacImp other = other

1011+

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

10101013 IState ->

10111014 (Name -> Name) -> [(Name, PTerm)] -> [Name] -> PDecl -> PDecl

src/Idris/AbsSyntaxTree.hs+19−7

@@ -1482,7 +1482,7 @@ getPArity _ = 0

14821482

14831483allNamesIn :: PTerm -> [Name]

14841484allNamesIn tm = nub $ ni [] tm

1485− where

1485+ where -- FIXME added niTacImp, but is it right?

14861486 ni env (PRef _ n)

14871487 | not (n `elem` env) = [n]

14881488 ni env (PPatvar _ n) = [n]

@@ -1490,7 +1490,7 @@ allNamesIn tm = nub $ ni [] tm

14901490 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

14911491 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

14921492 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1493− ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

1493+ ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

14941494 ni env (PHidden tm) = ni env tm

14951495 ni env (PEq _ l r) = ni env l ++ ni env r

14961496 ni env (PRewrite _ l r _) = ni env l ++ ni env r

@@ -1504,16 +1504,19 @@ allNamesIn tm = nub $ ni [] tm

15041504 ni env (PNoImplicits tm) = ni env tm

15051505 ni env _ = []

15061506

1507+ niTacImp env (TacImp _ _ scr) = ni env scr

1508+ niTacImp _ = []

1509+

15071510-- Return all names defined in binders in the given term

15081511boundNamesIn :: PTerm -> [Name]

15091512boundNamesIn tm = nub $ ni tm

1510− where

1513+ where -- FIXME Added niTacImp, but is it right?

15111514 ni (PApp _ f as) = ni f ++ concatMap (ni) (map getTm as)

15121515 ni (PAppBind _ f as) = ni f ++ concatMap (ni) (map getTm as)

15131516 ni (PCase _ c os) = ni c ++ concatMap (ni) (map snd os)

15141517 ni (PLam n ty sc) = n : (ni ty ++ ni sc)

15151518 ni (PLet n ty val sc) = n : (ni ty ++ ni val ++ ni sc)

1516− ni (PPi _ n ty sc) = n : (ni ty ++ ni sc)

1519+ ni (PPi p n ty sc) = niTacImp p ++ (n : (ni ty ++ ni sc))

15171520 ni (PEq _ l r) = ni l ++ ni r

15181521 ni (PRewrite _ l r _) = ni l ++ ni r

15191522 ni (PTyped l r) = ni l ++ ni r

@@ -1527,6 +1530,9 @@ boundNamesIn tm = nub $ ni tm

15271530 ni (PNoImplicits tm) = ni tm

15281531 ni _ = []

15291532

1533+ niTacImp (TacImp _ _ scr) = ni scr

1534+ niTacImp _ = []

1535+

15301536-- Return names which are free in the given term.

15311537namesIn :: [(Name, PTerm)] -> IState -> PTerm -> [Name]

15321538namesIn uvars ist tm = nub $ ni [] tm

@@ -1540,7 +1546,7 @@ namesIn uvars ist tm = nub $ ni [] tm

15401546 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

15411547 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

15421548 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1543− ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

1549+ ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

15441550 ni env (PEq _ l r) = ni env l ++ ni env r

15451551 ni env (PRewrite _ l r _) = ni env l ++ ni env r

15461552 ni env (PTyped l r) = ni env l ++ ni env r

@@ -1554,11 +1560,14 @@ namesIn uvars ist tm = nub $ ni [] tm

15541560 ni env (PNoImplicits tm) = ni env tm

15551561 ni env _ = []

15561562

1563+ niTacImp env (TacImp _ _ scr) = ni env scr

1564+ niTacImp _ _ = []

1565+

15571566-- Return which of the given names are used in the given term.

15581567

15591568usedNamesIn :: [Name] -> IState -> PTerm -> [Name]

15601569usedNamesIn vars ist tm = nub $ ni [] tm

1561− where

1570+ where -- FIXME added niTacImp, but is it right?

15621571 ni env (PRef _ n)

15631572 | n `elem` vars && not (n `elem` env)

15641573 = case lookupTy n (tt_ctxt ist) of

@@ -1568,7 +1577,7 @@ usedNamesIn vars ist tm = nub $ ni [] tm

15681577 ni env (PAppBind _ f as) = ni env f ++ concatMap (ni env) (map getTm as)

15691578 ni env (PCase _ c os) = ni env c ++ concatMap (ni env) (map snd os)

15701579 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

1571− ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

1580+ ni env (PPi p n ty sc) = niTacImp env p ++ ni env ty ++ ni (n:env) sc

15721581 ni env (PEq _ l r) = ni env l ++ ni env r

15731582 ni env (PRewrite _ l r _) = ni env l ++ ni env r

15741583 ni env (PTyped l r) = ni env l ++ ni env r

@@ -1582,3 +1591,6 @@ usedNamesIn vars ist tm = nub $ ni [] tm

15821591 ni env (PNoImplicits tm) = ni env tm

15831592 ni env _ = []

15841593

1594+ niTacImp (TacImp _ _ scr) = ni scr

1595+ niTacImp _ = []

1596+