2c58eba · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix elaboration of higher order dependent function types

2c58ebaEdwin Brady14 years ago

src/Idris/AbsSyntax.hs+12−8

compare with master

unifiedsplit

@@ -772,13 +772,13 @@ addImpl = addImpl' False [] []

772-- and *not* inside a PHidden

773

774addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm

775−addImpl' inpat env infns ist ptm = ai env ptm

775+addImpl' inpat env infns ist ptm = ai (zip env (repeat Nothing)) ptm

776 where

777 ai env (PRef fc f)

778 | f `elem` infns = PInferRef fc f

779− | not (f `elem` env) = handleErr $ aiFn inpat inpat ist fc f []

779+ | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat ist fc f []

780 ai env (PHidden (PRef fc f))

781− | not (f `elem` env) = handleErr $ aiFn inpat False ist fc f []

781+ | not (f `elem` map fst env) = handleErr $ aiFn inpat False ist fc f []

782 ai env (PEq fc l r) = let l' = ai env l

783 r' = ai env r in

784 PEq fc l' r'

@@ -797,11 +797,15 @@ addImpl' inpat env infns ist ptm = ai env ptm

797 ai env (PApp fc (PInferRef _ f) as)

798 = let as' = map (fmap (ai env)) as in

799 PApp fc (PInferRef fc f) as'

800− ai env (PApp fc (PRef _ f) as)

800+ ai env (PApp fc ftm@(PRef _ f) as)

801 | f `elem` infns = ai env (PApp fc (PInferRef fc f) as)

802− | not (f `elem` env)

802+ | not (f `elem` map fst env)

803 = let as' = map (fmap (ai env)) as in

804 handleErr $ aiFn inpat False ist fc f as'

805+ | Just (Just ty) <- lookup f env

806+ = let as' = map (fmap (ai env)) as

807+ arity = getPArity ty in

808+ mkPApp fc arity ftm as'

805 ai env (PApp fc f as) = let f' = ai env f

809 ai env (PApp fc f as) = let f' = ai env f

806 as' = map (fmap (ai env)) as in

810 as' = map (fmap (ai env)) as in

807 mkPApp fc 1 f' as'

811 mkPApp fc 1 f' as'

@@ -809,15 +813,15 @@ addImpl' inpat env infns ist ptm = ai env ptm

809 os' = map (pmap (ai env)) os in

813 os' = map (pmap (ai env)) os in

810 PCase fc c' os'

814 PCase fc c' os'

811 ai env (PLam n ty sc) = let ty' = ai env ty

815 ai env (PLam n ty sc) = let ty' = ai env ty

812− sc' = ai (n:env) sc in

816+ sc' = ai ((n, Just ty):env) sc in

813 PLam n ty' sc'

817 PLam n ty' sc'

814 ai env (PLet n ty val sc)

818 ai env (PLet n ty val sc)

815 = let ty' = ai env ty

819 = let ty' = ai env ty

816 val' = ai env val

820 val' = ai env val

817− sc' = ai (n:env) sc in

821+ sc' = ai ((n, Just ty):env) sc in

818 PLet n ty' val' sc'

822 PLet n ty' val' sc'

819 ai env (PPi p n ty sc) = let ty' = ai env ty

823 ai env (PPi p n ty sc) = let ty' = ai env ty

820− sc' = ai (n:env) sc in

824+ sc' = ai ((n, Just ty):env) sc in

821 PPi p n ty' sc'

825 PPi p n ty' sc'

822 ai env (PHidden tm) = PHidden (ai env tm)

826 ai env (PHidden tm) = PHidden (ai env tm)

823 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)

827 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)

src/Idris/AbsSyntaxTree.hs+4

@@ -1007,6 +1007,10 @@ instance Sized PTerm where

1007 size (PElabError err) = size err

1008 size PImpossible = 1

1009

1010+getPArity :: PTerm -> Int

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

1012+getPArity _ = 0

1013+

1010allNamesIn :: PTerm -> [Name]

1014allNamesIn :: PTerm -> [Name]

1011allNamesIn tm = nub $ ni [] tm

1015allNamesIn tm = nub $ ni [] tm

1012 where

1016 where

src/Idris/ElabDecls.hs+1

@@ -56,6 +56,7 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in

56 mapM_ (elabCaseBlock info) is

57 ctxt <- getContext

58 logLvl 5 $ "Rechecking"

59+ logLvl 6 $ show tyT

59 (cty, _) <- recheckC fc [] tyT

60 (cty, _) <- recheckC fc [] tyT

60 addStatics n cty ty'

61 addStatics n cty ty'

61 logLvl 6 $ "Elaborated to " ++ showEnvDbg [] tyT

62 logLvl 6 $ "Elaborated to " ++ showEnvDbg [] tyT