b1028f0 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

TacImp script handling to various functions.

b1028f0Timo Petteri Sinnemäki13 years ago

src/Idris/AbsSyntax.hs+6−3

compare with master

unifiedsplit

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

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

946 en (PPi p n t s)

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

948− = let n' = mkShadow n in

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

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

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

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

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

951 en (PLet n ty v s)

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

953 = let n' = mkShadow n in

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

1006

1007 nseq x y = nsroot x == nsroot y

1008

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

1010+ enTacImp other = other

1011+

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

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

1010 IState ->

1013 IState ->

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

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

src/Idris/AbsSyntaxTree.hs+19−7

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

1482

1483allNamesIn :: PTerm -> [Name]

1484allNamesIn tm = nub $ ni [] tm

1485− where

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

1486 ni env (PRef _ n)

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

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

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

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

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

1492 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

1494 ni env (PHidden tm) = ni env tm

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

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

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

1504 ni env (PNoImplicits tm) = ni env tm

1505 ni env _ = []

1506

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

1508+ niTacImp _ = []

1509+

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

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

1508boundNamesIn :: PTerm -> [Name]

1511boundNamesIn :: PTerm -> [Name]

1509boundNamesIn tm = nub $ ni tm

1512boundNamesIn tm = nub $ ni tm

1510− where

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1527 ni (PNoImplicits tm) = ni tm

1530 ni (PNoImplicits tm) = ni tm

1528 ni _ = []

1531 ni _ = []

1529

1532

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

1534+ niTacImp _ = []

1535+

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

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

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

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

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

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

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

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

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

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

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

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

1548 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

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

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

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

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

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

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

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

1554 ni env (PNoImplicits tm) = ni env tm

1560 ni env (PNoImplicits tm) = ni env tm

1555 ni env _ = []

1561 ni env _ = []

1556

1562

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

1564+ niTacImp _ _ = []

1565+

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

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

1558

1567

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

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

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

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

1561− where

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

1562 ni env (PRef _ n)

1571 ni env (PRef _ n)

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

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

1564 = case lookupTy n (tt_ctxt ist) of

1573 = case lookupTy n (tt_ctxt ist) of

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

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

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

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

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

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

1579 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

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

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

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

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

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

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

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

1582 ni env (PNoImplicits tm) = ni env tm

1591 ni env (PNoImplicits tm) = ni env tm

1583 ni env _ = []

1592 ni env _ = []

1584

1593

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

1595+ niTacImp _ = []

1596+