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

git.iko.soy/Idris-dev

on master help sign in

Abstract matched terms from goal type in with clauses

8d83f38Edwin Brady14 years ago

src/Core/TT.hs+16

compare with master

unifiedsplit

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

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

519 subst i t = t

520

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+

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

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

522pToV n = pToV' n 0

531pToV n = pToV' n 0

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

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

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

557substNames [] t = t

566substNames [] t = t

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

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

559

568

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+

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

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

561

577

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

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

src/Idris/AbsSyntaxTree.hs+27

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

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

1025getPArity _ = 0

1026

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

1028+

1027allNamesIn :: PTerm -> [Name]

1029allNamesIn :: PTerm -> [Name]

1028allNamesIn tm = nub $ ni [] tm

1030allNamesIn tm = nub $ ni [] tm

1029 where

1031 where

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

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

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

1043 ni env _ = []

1045 ni env _ = []

1044

1046

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

1048+

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

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

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

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

1047 where

1051 where

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

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

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

1063 ni env (PHidden tm) = ni env tm

1067 ni env (PHidden tm) = ni env tm

1064 ni env _ = []

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

624 addDeferred def'

625 mapM_ (elabCaseBlock info) is

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

627+ let cwvaltyN = explicitNames cwvalty

628+ let cwvalN = explicitNames cwval

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

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)

628 windex <- getName

638 windex <- getName

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

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

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

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)

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

644+ let wtype = bindTyArgs Pi (bargs_pre ++

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

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

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

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

633 let wname = MN windex (show fname)

648 let wname = MN windex (show fname)

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

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

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

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

640 -- in the subdecls, lhs becomes:

655 -- in the subdecls, lhs becomes:

641 -- fname pats | wpat [rest]

656 -- fname pats | wpat [rest]

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

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

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

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

659+ withblock

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

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

645 mapM_ (elabDecl EAll info) wb

661 mapM_ (elabDecl EAll info) wb

646

662

647 -- rhs becomes: fname' ps wval

663 -- rhs becomes: fname' ps wval

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

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

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

649− [pexp wval])

666+ pexp wval :

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

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

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

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

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

652 i <- get

670 i <- get

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

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

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

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

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

667 getImps _ = []

685 getImps _ = []

668

686

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

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

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

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

671 return $ PClauses fc o wname cs'

689 return $ PClauses fc o wname cs'

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

690 | 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

674

692

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)

676 = do i <- get

694 = do i <- get

677 let tm = addImpl i tm_in

695 let tm = addImpl i tm_in

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

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

679 showImp True toplhs)

697 showImp True toplhs)

680 case matchClause i toplhs tm of

698 case matchClause i toplhs tm of

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

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

700+ Right mvars ->

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

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

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

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

684− return $ PClause fc wname lhs ws rhs wheres

703+ return $ PClause fc wname lhs ws rhs wheres

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

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

686 = do i <- get

705 = do i <- get

687 let tm = addImpl i tm_in

706 let tm = addImpl i tm_in

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

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

689 showImp True toplhs)

708 showImp True toplhs)

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

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

691 case matchClause i toplhs tm of

710 case matchClause i toplhs tm of

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

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

712+ Right mvars ->

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

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

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

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

695− mkAux wname toplhs ns c

715+ mkAux wname toplhs ns ns' c

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

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

697

717

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

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

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

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

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

700 return $ substMatches mvars $

721 return $ substMatches mvars $

701 PApp fc (PRef fc' wname)

722 PApp fc (PRef fc' wname)

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

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

724+ updateLHS n wname mvars ns ns' tm w

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

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

704

726

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

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

706 | otherwise = Placeholder

728 | otherwise = Placeholder

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

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

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

709 fullApp x = x

731 fullApp x = x

710

732

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+

711data MArgTy = IA | EA | CA deriving Show

741data MArgTy = IA | EA | CA deriving Show

712

742

713elabClass :: ElabInfo -> SyntaxInfo -> String ->

743elabClass :: ElabInfo -> SyntaxInfo -> String ->

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

1026pbty _ tm = tm

1056pbty _ tm = tm

1027

1057

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

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

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

1029getPBtys _ = []

1060getPBtys _ = []

1030

1061

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

1062psolve (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+