8d83f38 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Abstract matched terms from goal type in with clauses

(like 'magic with' in Agda)

commit8d83f3894e6667c7b5087d3bff0a61a6a1b40750 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 18 Dec 2012, 15:21 (14 years ago) parent11dbfc0

6 files changed+120−25

compare with master

unifiedsplit

src/Core/TT.hs+16 src/Idris/AbsSyntaxTree.hs+27 src/Idris/ElabDecls.hs+56−25 test/test019/expected+1 test/test019/run+4 test/test019/test019.lidr+16

src/Core/TT.hs+16

@@ -518,6 +518,15 @@ instantiate e = subst 0 where

518518 subst i (Proj x idx) = Proj (subst i x) idx

519519 subst i t = t

520520

521+explicitNames :: TT n -> TT n

522+explicitNames (Bind x b sc) = let b' = fmap explicitNames b in

523+ Bind x b'

524+ (explicitNames (instantiate

525+ (P Bound x (binderTy b')) sc))

526+explicitNames (App f a) = App (explicitNames f) (explicitNames a)

527+explicitNames (Proj x idx) = Proj (explicitNames x) idx

528+explicitNames t = t

529+

521530pToV :: Eq n => n -> TT n -> TT n

522531pToV n = pToV' n 0

523532pToV' n i (P _ x _) | n == x = V i

@@ -557,6 +566,13 @@ substNames :: Eq n => [(n, TT n)] -> TT n -> TT n

557566substNames [] t = t

558567substNames ((n, tm) : xs) t = subst n tm (substNames xs t)

559568

569+substTerm :: Eq n => TT n -> TT n -> TT n -> TT n

570+substTerm old new = st where

571+ st t | t == old = new

572+ st (App f a) = App (st f) (st a)

573+ st (Bind x b sc) = Bind x (fmap st b) (st sc)

574+ st t = t

575+

560576-- Returns true if V 0 and bound name n do not occur in the term

561577

562578noOccurrence :: Eq n => n -> TT n -> Bool

src/Idris/AbsSyntaxTree.hs+27

@@ -1024,6 +1024,8 @@ getPArity :: PTerm -> Int

10241024getPArity (PPi _ _ _ sc) = 1 + getPArity sc

10251025getPArity _ = 0

10261026

1027+-- Return all names, free or globally bound, in the given term.

1028+

10271029allNamesIn :: PTerm -> [Name]

10281030allNamesIn tm = nub $ ni [] tm

10291031 where

@@ -1042,6 +1044,8 @@ allNamesIn tm = nub $ ni [] tm

10421044 ni env (PAlternative a ls) = concatMap (ni env) ls

10431045 ni env _ = []

10441046

1047+-- Return names which are free in the given term.

1048+

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

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

10471051 where

@@ -1062,3 +1066,26 @@ namesIn uvars ist tm = nub $ ni [] tm

10621066 ni env (PAlternative a as) = concatMap (ni env) as

10631067 ni env (PHidden tm) = ni env tm

10641068 ni env _ = []

1069+

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

1071+

1072+usedNamesIn :: [Name] -> IState -> PTerm -> [Name]

1073+usedNamesIn vars ist tm = nub $ ni [] tm

1074+ where

1075+ ni env (PRef _ n)

1076+ | n `elem` vars && not (n `elem` env)

1077+ = case lookupTy Nothing n (tt_ctxt ist) of

1078+ [] -> [n]

1079+ _ -> []

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

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

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

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

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

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

1086+ ni env (PPair _ l r) = ni env l ++ ni env r

1087+ ni env (PDPair _ (PRef _ n) t r) = ni env t ++ ni (n:env) r

1088+ ni env (PDPair _ l t r) = ni env l ++ ni env t ++ ni env r

1089+ ni env (PAlternative a as) = concatMap (ni env) as

1090+ ni env (PHidden tm) = ni env tm

1091+ ni env _ = []

src/Idris/ElabDecls.hs+56−25

@@ -624,12 +624,27 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)

624624 addDeferred def'

625625 mapM_ (elabCaseBlock info) is

626626 (cwval, cwvalty) <- recheckC fc [] (getInferTerm wval')

627− logLvl 3 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)

627+ let cwvaltyN = explicitNames cwvalty

628+ let cwvalN = explicitNames cwval

629+ logLvl 1 ("With type " ++ show cwvalty ++ "\nRet type " ++ show ret_ty)

630+ let pvars = map fst (getPBtys cwvalty)

631+ -- we need the unelaborated term to get the names it depends on

632+ -- rather than a de Bruijn index.

633+ let pdeps = usedNamesIn pvars i (delab i cwvalty)

634+ let (bargs_pre, bargs_post) = split pdeps bargs []

635+ logLvl 1 ("With type " ++ show (getRetTy cwvaltyN) ++

636+ " depends on " ++ show pdeps ++ " from " ++ show pvars)

637+ logLvl 1 ("Pre " ++ show bargs_pre ++ "\nPost " ++ show bargs_post)

628638 windex <- getName

629639 -- build a type declaration for the new function:

630− -- (ps : Xs) -> (withval : cwvalty) -> ret_ty

631− let wtype = bindTyArgs Pi (bargs ++ [(MN 0 "warg", getRetTy cwvalty)]) ret_ty

632− logLvl 3 ("New function type " ++ show wtype)

640+ -- (ps : Xs) -> (withval : cwvalty) -> (ps' : Xs') -> ret_ty

641+ let wargval = getRetTy cwvalN

642+ let wargtype = getRetTy cwvaltyN

643+ logLvl 1 ("Abstract over " ++ show wargval)

644+ let wtype = bindTyArgs Pi (bargs_pre ++

645+ (MN 0 "warg", wargtype) :

646+ map (abstract (MN 0 "warg") wargval) bargs_post) ret_ty

647+ logLvl 1 ("New function type " ++ show wtype)

633648 let wname = MN windex (show fname)

634649 let imps = getImps wtype -- add to implicits context

635650 put (i { idris_implicits = addDef wname imps (idris_implicits i) })

@@ -640,14 +655,17 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)

640655 -- in the subdecls, lhs becomes:

641656 -- fname pats | wpat [rest]

642657 -- ==> fname' ps wpat [rest], match pats against toplevel for ps

643− wb <- mapM (mkAuxC wname lhs (map fst bargs)) withblock

644− logLvl 5 ("with block " ++ show wb)

658+ wb <- mapM (mkAuxC wname lhs (map fst bargs_pre) (map fst bargs_post))

659+ withblock

660+ logLvl 1 ("with block " ++ show wb)

645661 mapM_ (elabDecl EAll info) wb

646662

647663 -- rhs becomes: fname' ps wval

648− let rhs = PApp fc (PRef fc wname) (map (pexp . (PRef fc) . fst) bargs ++

649− [pexp wval])

650− logLvl 3 ("New RHS " ++ show rhs)

664+ let rhs = PApp fc (PRef fc wname)

665+ (map (pexp . (PRef fc) . fst) bargs_pre ++

666+ pexp wval :

667+ (map (pexp . (PRef fc) . fst) bargs_post))

668+ logLvl 1 ("New RHS " ++ show rhs)

651669 ctxt <- getContext -- New context with block added

652670 i <- get

653671 ((rhs', defer, is), _) <-

@@ -666,41 +684,45 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)

666684 getImps (Bind n (Pi _) t) = pexp Placeholder : getImps t

667685 getImps _ = []

668686

669− mkAuxC wname lhs ns (PClauses fc o n cs)

670− | True = do cs' <- mapM (mkAux wname lhs ns) cs

687+ mkAuxC wname lhs ns ns' (PClauses fc o n cs)

688+ | True = do cs' <- mapM (mkAux wname lhs ns ns') cs

671689 return $ PClauses fc o wname cs'

672690 | otherwise = fail $ show fc ++ "with clause uses wrong function name " ++ show n

673− mkAuxC wname lhs ns d = return $ d

691+ mkAuxC wname lhs ns ns' d = return $ d

674692

675− mkAux wname toplhs ns (PClause fc n tm_in (w:ws) rhs wheres)

693+ mkAux wname toplhs ns ns' (PClause fc n tm_in (w:ws) rhs wheres)

676694 = do i <- get

677695 let tm = addImpl i tm_in

678696 logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++

679697 showImp True toplhs)

680698 case matchClause i toplhs tm of

681699 Left _ -> fail $ show fc ++ "with clause does not match top level"

682− Right mvars -> do logLvl 3 ("Match vars : " ++ show mvars)

683− lhs <- updateLHS n wname mvars ns (fullApp tm) w

684− return $ PClause fc wname lhs ws rhs wheres

685− mkAux wname toplhs ns (PWith fc n tm_in (w:ws) wval withs)

700+ Right mvars ->

701+ do logLvl 3 ("Match vars : " ++ show mvars)

702+ lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w

703+ return $ PClause fc wname lhs ws rhs wheres

704+ mkAux wname toplhs ns ns' (PWith fc n tm_in (w:ws) wval withs)

686705 = do i <- get

687706 let tm = addImpl i tm_in

688707 logLvl 2 ("Matching " ++ showImp True tm ++ " against " ++

689708 showImp True toplhs)

690− withs' <- mapM (mkAuxC wname toplhs ns) withs

709+ withs' <- mapM (mkAuxC wname toplhs ns ns') withs

691710 case matchClause i toplhs tm of

692711 Left _ -> fail $ show fc ++ "with clause does not match top level"

693− Right mvars -> do lhs <- updateLHS n wname mvars ns (fullApp tm) w

694− return $ PWith fc wname lhs ws wval withs'

695− mkAux wname toplhs ns c

712+ Right mvars ->

713+ do lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w

714+ return $ PWith fc wname lhs ws wval withs'

715+ mkAux wname toplhs ns ns' c

696716 = fail $ show fc ++ "badly formed with clause"

697717

698− updateLHS n wname mvars ns (PApp fc (PRef fc' n') args) w

699− = let ns' = map (keepMvar (map fst mvars) fc') ns in

718+ updateLHS n wname mvars ns_in ns_in' (PApp fc (PRef fc' n') args) w

719+ = let ns = map (keepMvar (map fst mvars) fc') ns_in

720+ ns' = map (keepMvar (map fst mvars) fc') ns_in' in

700721 return $ substMatches mvars $

701722 PApp fc (PRef fc' wname)

702− (map pexp ns' ++ [pexp w])

703− updateLHS n wname mvars ns tm w = fail $ "Not implemented match " ++ show tm

723+ (map pexp ns ++ pexp w : (map pexp ns'))

724+ updateLHS n wname mvars ns ns' tm w

725+ = fail $ "Not implemented match " ++ show tm

704726

705727 keepMvar mvs fc v | v `elem` mvs = PRef fc v

706728 | otherwise = Placeholder

@@ -708,6 +730,14 @@ elabClause info tcgen (_, PWith fc fname lhs_in withs wval_in withblock)

708730 fullApp (PApp _ (PApp fc f args) xs) = fullApp (PApp fc f (args ++ xs))

709731 fullApp x = x

710732

733+ split [] rest pre = (reverse pre, rest)

734+ split deps ((n, ty) : rest) pre

735+ | n `elem` deps = split (deps \\ [n]) rest ((n, ty) : pre)

736+ | otherwise = split deps rest ((n, ty) : pre)

737+ split deps [] pre = (reverse pre, [])

738+

739+ abstract wn wty (n, argty) = (n, substTerm wty (P Bound wn wty) argty)

740+

711741data MArgTy = IA | EA | CA deriving Show

712742

713743elabClass :: ElabInfo -> SyntaxInfo -> String ->

@@ -1026,6 +1056,7 @@ pbty (Bind n (PVar t) sc) tm = Bind n (PVTy t) (pbty sc tm)

10261056pbty _ tm = tm

10271057

10281058getPBtys (Bind n (PVar t) sc) = (n, t) : getPBtys sc

1059+getPBtys (Bind n (PVTy t) sc) = (n, t) : getPBtys sc

10291060getPBtys _ = []

10301061

10311062psolve (Bind n (PVar t) sc) = do solve; psolve sc

test/test019/expectednew file+1

@@ -0,0 +1 @@

1+sO

test/test019/runnew file+4

@@ -0,0 +1,4 @@

1+#!/bin/bash

2+idris $@ test019.lidr -o test019

3+./test019

4+rm -f test019 *.ibc

test/test019/test019.lidrnew file+16

@@ -0,0 +1,16 @@

1+> module Main

3+> ifTrue : so True -> Nat

4+> ifTrue oh = S O

6+> ifFalse : so False -> Nat

7+> ifFalse oh impossible

9+> test : (f : Nat -> Bool) -> (n : Nat) -> so (f n) -> Nat

10+> test f n x with (f n)

11+> | True = ifTrue x

12+> | False = ifFalse x

13+

14+> main : IO ()

15+> main = print (test ((S 4) ==) 5 oh)

16+