6c4d0f1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix for metavariables in type declarations

Allow multiple, with later allowed to depend on earlier

commit6c4d0f1f794eff2ce576113fe6ff83b5d49befbc authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 8 Feb 2014, 21:05 (13 years ago) parent39636cf

6 files changed+27−12

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+8−1 src/Idris/Core/Elaborate.hs−2 src/Idris/Delaborate.hs+1−1 src/Idris/ElabDecls.hs+15−6 src/Idris/ElabTerm.hs+2−1 src/Idris/ParseOps.hs+1−1

src/Idris/AbsSyntaxTree.hs+8−1

@@ -112,6 +112,7 @@ data IState = IState {

112112 idris_callgraph :: Ctxt CGInfo, -- name, args used in each pos

113113 idris_calledgraph :: Ctxt [Name],

114114 idris_docstrings :: Ctxt String,

115+ idris_tyinfodata :: Ctxt TIData,

115116 idris_totcheck :: [(FC, Name)], -- names to check totality on

116117 idris_defertotcheck :: [(FC, Name)], -- names to check at the end

117118 idris_options :: IOption,

@@ -216,7 +217,7 @@ idrisInit :: IState

216217idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

217218 emptyContext emptyContext emptyContext emptyContext

218219 emptyContext emptyContext emptyContext emptyContext

219− emptyContext

220+ emptyContext emptyContext

220221 [] [] defaultOpts 6 [] [] [] [] [] [] [] [] [] [] [] [] []

221222 [] Nothing Nothing [] [] [] Hidden False [] Nothing [] [] RawOutput

222223 True defaultTheme stdout [] (0, emptyContext) emptyContext M.empty

@@ -811,6 +812,12 @@ deriving instance Binary ClassInfo

811812deriving instance NFData ClassInfo

812813!-}

813814

815+-- Type inference data

816+

817+data TIData = TIPartial -- ^ a function with a partially defined type

818+ | TISolution Term -- ^ solution to a metavariable in a type

819+ deriving Show

820+

814821-- An argument is conditionally forceable iff its forceability

815822-- depends on the collapsibility of the whole type.

816823data Forceability = Conditional | Unconditional deriving (Show, Enum, Bounded, Eq, Ord)

src/Idris/Core/Elaborate.hs−2

@@ -466,8 +466,6 @@ apply' fillt fn imps =

466466 do args <- prepare_apply fn (map fst imps)

467467 -- _Don't_ solve the arguments we're specifying by hand.

468468 -- (remove from unified list before calling end_unify)

469− -- HMMM: Actually, if we get it wrong, the typechecker will complain!

470− -- so do nothing

471469 hs <- get_holes

472470 ES (p, a) s prev <- get

473471 let dont = head hs : dontunify p ++

src/Idris/Delaborate.hs+1−1

@@ -151,7 +151,7 @@ pprintErr' i (CantUnify _ x y e sc s) =

151151 _ -> line <> line <> text "Specifically:" <>

152152 indented (pprintErr' i e) <>

153153 if (opt_errContext (idris_options i)) then text $ showSc i sc else empty

154−pprintErr' i (CantConvert x y env) =

154+pprintErr' i (CantConvert x y env) = trace (show (x,y)) $

155155 text "Can't convert" <> indented (pprintTerm i (delab i x)) <$>

156156 text "with" <> indented (pprintTerm i (delab i y)) <>

157157 if (opt_errContext (idris_options i)) then line <> text (showSc i env) else empty

src/Idris/ElabDecls.hs+15−6

@@ -49,9 +49,18 @@ recheckC fc env t

4949 addConstraints fc cs

5050 return (tm, ty)

5151

52−checkDef fc ns = do ctxt <- getContext

53− mapM (\(n, (i, top, t)) -> do (t', _) <- recheckC fc [] t

54− return (n, (i, top, t'))) ns

52+

53+checkDef fc ns = checkAddDef False fc ns

54+

55+checkAddDef add fc [] = return []

56+checkAddDef add fc ((n, (i, top, t)) : ns)

57+ = do ctxt <- getContext

58+ (t', _) <- recheckC fc [] t

59+ when add $ addDeferred [(n, (i, top, t, True))]

60+ ns' <- checkAddDef add fc ns

61+ return ((n, (i, top, t')) : ns')

62+-- mapM (\(n, (i, top, t)) -> do (t', _) <- recheckC fc [] t

63+-- return (n, (i, top, t'))) ns

5564

5665-- | Elaborate a top-level type declaration - for example, "foo : Int -> Int".

5766elabType :: ElabInfo -> SyntaxInfo -> String ->

@@ -76,9 +85,9 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty

7685 ((tyT, defer, is), log) <-

7786 tclift $ elaborate ctxt n (TType (UVal 0)) []

7887 (errAt "type of " n (erun fc (build i info False [] n ty)))

79− ds <- checkDef fc defer

80− let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds

81− addDeferred ds'

88+ ds <- checkAddDef True fc defer

89+-- let ds' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) ds

90+-- addDeferred ds'

8291 mapM_ (elabCaseBlock info opts) is

8392 ctxt <- getContext

8493 logLvl 5 $ "Rechecking"

src/Idris/ElabTerm.hs+2−1

@@ -841,7 +841,8 @@ collectDeferred :: Maybe Name ->

841841 Term -> State [(Name, (Int, Maybe Name, Type))] Term

842842collectDeferred top (Bind n (GHole i t) app) =

843843 do ds <- get

844− when (not (n `elem` map fst ds)) $ put ((n, (i, top, t)) : ds)

844+ t' <- collectDeferred top t

845+ when (not (n `elem` map fst ds)) $ put (ds ++ [(n, (i, top, t'))])

845846 collectDeferred top app

846847collectDeferred top (Bind n b t) = do b' <- cdb b

847848 t' <- collectDeferred top t

src/Idris/ParseOps.hs+1−1

@@ -39,7 +39,7 @@ table fixes

3939 [[backtick],

4040 [binary "$" (\fc x y -> PApp fc x [pexp y]) AssocRight],

4141 [binary "=" PEq AssocLeft],

42− [binary "->" (\fc x y -> PPi expl (sMN 42 "__pi_arg") x y) AssocRight]]

42+ [binary "->" (\fc x y -> PPi expl (sUN "__pi_arg") x y) AssocRight]]

4343

4444-- | Calculates table for fixtiy declarations

4545toTable :: [FixDecl] -> OperatorTable IdrisParser PTerm