git.iko.soy/Idris-dev
on master help sign in
Fix elaboration of higher order dependent function types

Fixes issue #116

commit2c58eba48c37b1c7bcea1b3c19533b641af991d8 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 3 Dec 2012, 12:48 (14 years ago) parent5803d2b
3 files changed+17−8
compare with master
unifiedsplit
src/Idris/AbsSyntax.hs+12−8 src/Idris/AbsSyntaxTree.hs+4 src/Idris/ElabDecls.hs+1
src/Idris/AbsSyntax.hs+12−8
@@ -772,13 +772,13 @@ addImpl = addImpl' False [] []
772772-- and *not* inside a PHidden
773773
774774addImpl' :: 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
776776 where
777777 ai env (PRef fc f)
778778 | 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 []
780780 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 []
782782 ai env (PEq fc l r) = let l' = ai env l
783783 r' = ai env r in
784784 PEq fc l' r'
@@ -797,11 +797,15 @@ addImpl' inpat env infns ist ptm = ai env ptm
797797 ai env (PApp fc (PInferRef _ f) as)
798798 = let as' = map (fmap (ai env)) as in
799799 PApp fc (PInferRef fc f) as'
800− ai env (PApp fc (PRef _ f) as)
800+ ai env (PApp fc ftm@(PRef _ f) as)
801801 | f `elem` infns = ai env (PApp fc (PInferRef fc f) as)
802− | not (f `elem` env)
802+ | not (f `elem` map fst env)
803803 = let as' = map (fmap (ai env)) as in
804804 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'
805809 ai env (PApp fc f as) = let f' = ai env f
806810 as' = map (fmap (ai env)) as in
807811 mkPApp fc 1 f' as'
@@ -809,15 +813,15 @@ addImpl' inpat env infns ist ptm = ai env ptm
809813 os' = map (pmap (ai env)) os in
810814 PCase fc c' os'
811815 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
813817 PLam n ty' sc'
814818 ai env (PLet n ty val sc)
815819 = let ty' = ai env ty
816820 val' = ai env val
817− sc' = ai (n:env) sc in
821+ sc' = ai ((n, Just ty):env) sc in
818822 PLet n ty' val' sc'
819823 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
821825 PPi p n ty' sc'
822826 ai env (PHidden tm) = PHidden (ai env tm)
823827 ai env (PProof ts) = PProof (map (fmap (ai env)) ts)
src/Idris/AbsSyntaxTree.hs+4
@@ -1007,6 +1007,10 @@ instance Sized PTerm where
10071007 size (PElabError err) = size err
10081008 size PImpossible = 1
10091009
1010+getPArity :: PTerm -> Int
1011+getPArity (PPi _ _ _ sc) = 1 + getPArity sc
1012+getPArity _ = 0
1013+
10101014allNamesIn :: PTerm -> [Name]
10111015allNamesIn tm = nub $ ni [] tm
10121016 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
5656 mapM_ (elabCaseBlock info) is
5757 ctxt <- getContext
5858 logLvl 5 $ "Rechecking"
59+ logLvl 6 $ show tyT
5960 (cty, _) <- recheckC fc [] tyT
6061 addStatics n cty ty'
6162 logLvl 6 $ "Elaborated to " ++ showEnvDbg [] tyT