d97715e · Idris-dev · git.iko.soy

src/Idris/AbsSyntaxTree.hs+1−22

compare with master

unifiedsplit

@@ -581,14 +581,6 @@ dictionary :: FnOpts -> Bool

581dictionary = elem Dictionary

582

583

584−-- | Data declaration options

585−data DataOpt = Codata -- ^ Set if the the data-type is coinductive

586− | DefaultEliminator -- ^ Set if an eliminator should be generated for data type

587− | DefaultCaseFun -- ^ Set if a case function should be generated for data type

588− | DataErrRev

589− deriving (Show, Eq)

590−

591−type DataOpts = [DataOpt]

592

584

593-- | Type provider - what to provide

585-- | Type provider - what to provide

594data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term

586data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term

@@ -1083,20 +1075,7 @@ deriving instance Binary OptInfo

1083deriving instance NFData OptInfo

1075deriving instance NFData OptInfo

1084!-}

1076!-}

1085

1077

1086−

1087−data TypeInfo = TI { con_names :: [Name],

1088− codata :: Bool,

1089− data_opts :: DataOpts,

1090− param_pos :: [Int],

1091− mutual_types :: [Name] }

1092− deriving Show

1093−{-!

1094−deriving instance Binary TypeInfo

1095−deriving instance NFData TypeInfo

1096−!-}

1097−

1098−-- Syntactic sugar info

1078+-- | Syntactic sugar info

1099−

1100data DSL' t = DSL { dsl_bind :: t,

1079data DSL' t = DSL { dsl_bind :: t,

1101 dsl_return :: t,

1080 dsl_return :: t,

1102 dsl_apply :: t,

1081 dsl_apply :: t,

src/Idris/Core/Elaborate.hs+13−5

@@ -115,13 +115,13 @@ runElab a e ps = runStateT e (ES (ps, a) "" Nothing)

115execElab :: aux -> Elab' aux a -> ProofState -> TC (ElabState aux)

116execElab a e ps = execStateT e (ES (ps, a) "" Nothing)

117

118−initElaborator :: Name -> Context -> Type -> ProofState

118+initElaborator :: Name -> Context -> Ctxt TypeInfo -> Type -> ProofState

119initElaborator = newProof

120

121−elaborate :: Context -> Name -> Type -> aux -> Elab' aux a -> TC (a, String)

121+elaborate :: Context -> Ctxt TypeInfo -> Name -> Type -> aux -> Elab' aux a -> TC (a, String)

122−elaborate ctxt n ty d elab = do let ps = initElaborator n ctxt ty

122+elaborate ctxt datatypes n ty d elab = do let ps = initElaborator n ctxt datatypes ty

123− (a, ES ps' str _) <- runElab d elab ps

123+ (a, ES ps' str _) <- runElab d elab ps

124− return $! (a, str)

124+ return $! (a, str)

125

126-- | Modify the auxiliary state

127updateAux :: (aux -> aux) -> Elab' aux ()

@@ -178,6 +178,14 @@ set_context :: Context -> Elab' aux ()

178set_context ctxt = do ES (p, a) logs prev <- get

179 put (ES (p { context = ctxt }, a) logs prev)

180

181+get_datatypes :: Elab' aux (Ctxt TypeInfo)

182+get_datatypes = do ES p _ _ <- get

183+ return $! (datatypes (fst p))

184+

185+set_datatypes :: Ctxt TypeInfo -> Elab' aux ()

186+set_datatypes ds = do ES (p, a) logs prev <- get

187+ put (ES (p { datatypes = ds }, a) logs prev)

188+

181-- | get the proof term

189-- | get the proof term

182get_term :: Elab' aux Term

190get_term :: Elab' aux Term

183get_term = do ES p _ _ <- get

191get_term = do ES p _ _ <- get

src/Idris/Core/ProofState.hs+10−8

@@ -41,6 +41,7 @@ data ProofState = PS { thname :: Name,

41 autos :: [(Name, [Name])], -- ^ unsolved 'auto' implicits with their holes

42 previous :: Maybe ProofState, -- ^ for undo

43 context :: Context,

44+ datatypes :: Ctxt TypeInfo,

44 plog :: String,

45 plog :: String,

45 unifylog :: Bool,

46 unifylog :: Bool,

46 done :: Bool,

47 done :: Bool,

@@ -292,14 +293,15 @@ query q = do ps <- get

292addLog :: Monad m => String -> StateT TState m ()

293addLog :: Monad m => String -> StateT TState m ()

293addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })

294addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })

294

295

295−newProof :: Name -> Context -> Type -> ProofState

296+newProof :: Name -> Context -> Ctxt TypeInfo -> Type -> ProofState

297+newProof n ctxt datatypes ty =

296−newProof n ctxt ty = let h = holeName 0

298+ let h = holeName 0

297− ty' = vToP ty

299+ ty' = vToP ty

298− in PS n [h] [] 1 (mkProofTerm (Bind h (Hole ty')

300+ in PS n [h] [] 1 (mkProofTerm (Bind h (Hole ty')

299− (P Bound h ty'))) ty [] (h, []) [] []

301+ (P Bound h ty'))) ty [] (h, []) [] []

300− Nothing [] []

302+ Nothing [] []

301− [] [] []

303+ [] [] []

302− Nothing ctxt "" False False [] []

304+ Nothing ctxt datatypes "" False False [] []

303

305

304type TState = ProofState -- [TacticAction])

306type TState = ProofState -- [TacticAction])

305type RunTactic = RunTactic' TState

307type RunTactic = RunTactic' TState

src/Idris/Core/TT.hs+20

@@ -882,6 +882,26 @@ data Datatype n = Data { d_typename :: n,

882 d_cons :: [(n, TT n)] }

883 deriving (Show, Functor, Eq)

884

885+-- | Data declaration options

886+data DataOpt = Codata -- ^ Set if the the data-type is coinductive

887+ | DefaultEliminator -- ^ Set if an eliminator should be generated for data type

888+ | DefaultCaseFun -- ^ Set if a case function should be generated for data type

889+ | DataErrRev

890+ deriving (Show, Eq)

891+

892+type DataOpts = [DataOpt]

893+

894+data TypeInfo = TI { con_names :: [Name],

895+ codata :: Bool,

896+ data_opts :: DataOpts,

897+ param_pos :: [Int],

898+ mutual_types :: [Name] }

899+ deriving Show

900+{-!

901+deriving instance Binary TypeInfo

902+deriving instance NFData TypeInfo

903+!-}

904+

885instance Eq n => Eq (TT n) where

905instance Eq n => Eq (TT n) where

886 (==) (P xt x _) (P yt y _) = x == y

906 (==) (P xt x _) (P yt y _) = x == y

887 (==) (V x) (V y) = x == y

907 (==) (V x) (V y) = x == y

src/Idris/Elab/Clause.hs+6−6

@@ -451,7 +451,7 @@ checkPossible info fc tcgen fname lhs_in

451 i <- getIState

452 let lhs = addImplPat i lhs_in

453 -- if the LHS type checks, it is possible

454− case elaborate ctxt (sMN 0 "patLHS") infP initEState

454+ case elaborate ctxt (idris_datatypes i) (sMN 0 "patLHS") infP initEState

455 (erun fc (buildTC i info ELHS [] fname (infTerm lhs))) of

456 OK (ElabResult lhs' _ _ ctxt' newDecls, _) ->

457 do setContext ctxt'

@@ -538,7 +538,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

538 "\n" ++ show (fn_ty, fn_is))

539

540 ((ElabResult lhs' dlhs [] ctxt' newDecls, probs, inj), _) <-

541− tclift $ elaborate ctxt (sMN 0 "patLHS") infP initEState

541+ tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "patLHS") infP initEState

542 (do res <- errAt "left hand side of " fname

543 (erun fc (buildTC i info ELHS opts fname (infTerm lhs)))

544 probs <- get_probs

@@ -613,7 +613,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

613 ctxt <- getContext -- new context with where block added

614 logLvl 5 "STARTING CHECK"

615 ((rhs', defer, is, probs, ctxt', newDecls), _) <-

616− tclift $ elaborate ctxt (sMN 0 "patRHS") clhsty initEState

616+ tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "patRHS") clhsty initEState

617 (do pbinds ist lhs_tm

618 mapM_ setinj (nub (params ++ inj))

619 setNextName

@@ -774,7 +774,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

774 let lhs = stripLinear i $ stripUnmatchable i $ propagateParams i params fn_ty (addImplPat i lhs_in)

775 logLvl 2 ("LHS: " ++ show lhs)

776 (ElabResult lhs' dlhs [] ctxt' newDecls, _) <-

777− tclift $ elaborate ctxt (sMN 0 "patLHS") infP initEState

777+ tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "patLHS") infP initEState

778 (errAt "left hand side of with in " fname

779 (erun fc (buildTC i info ELHS opts fname (infTerm lhs))) )

780 setContext ctxt'

@@ -791,7 +791,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

791 logLvl 5 ("Checking " ++ showTmImpls wval)

792 -- Elaborate wval in this context

793 ((wval', defer, is, ctxt', newDecls), _) <-

794− tclift $ elaborate ctxt (sMN 0 "withRHS")

794+ tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "withRHS")

795 (bindTyArgs PVTy bargs infP) initEState

796 (do pbinds i lhs_tm

797 setNextName

@@ -889,7 +889,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

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

890 i <- getIState

891 ((rhs', defer, is, ctxt', newDecls), _) <-

892− tclift $ elaborate ctxt (sMN 0 "wpatRHS") clhsty initEState

892+ tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "wpatRHS") clhsty initEState

893 (do pbinds i lhs_tm

894 setNextName

895 (ElabResult _ d is ctxt' newDecls) <- erun fc (build i info ERHS opts fname rhs)

src/Idris/Elab/Instance.hs+1−1

@@ -177,7 +177,7 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

177 let ty = addImpl [] i ty'

178 ctxt <- getContext

179 (ElabResult tyT _ _ ctxt' newDecls, _) <-

180− tclift $ elaborate ctxt iname (TType (UVal 0)) initEState

180+ tclift $ elaborate ctxt (idris_datatypes i) iname (TType (UVal 0)) initEState

181 (errAt "type of " iname (erun fc (build i info ERHS [] iname ty)))

182 setContext ctxt'

183 processTacticDecls info newDecls

src/Idris/Elab/Term.hs+3−2

@@ -1000,9 +1000,10 @@ elab ist info emode opts fn tm

1000 -- Save the old state - we need a fresh proof state to avoid

1001 -- capturing lexically available variables in the quoted term.

1002 ctxt <- get_context

1003+ datatypes <- get_datatypes

1003 saveState

1004 saveState

1004 updatePS (const .

1005 updatePS (const .

1005− newProof (sMN 0 "q") ctxt $

1006+ newProof (sMN 0 "q") ctxt datatypes $

1006 P Ref (reflm "TT") Erased)

1007 P Ref (reflm "TT") Erased)

1007

1008

1008 -- Re-add the unquotes, letting Idris infer the (fictional)

1009 -- Re-add the unquotes, letting Idris infer the (fictional)

@@ -2188,7 +2189,7 @@ processTacticDecls info steps =

2188 let lhs = addImplPat ist lhs_in

2189 let lhs = addImplPat ist lhs_in

2189 let fc = fileFC "elab_reflected_totality"

2190 let fc = fileFC "elab_reflected_totality"

2190 let tcgen = False -- TODO: later we may support dictionary generation

2191 let tcgen = False -- TODO: later we may support dictionary generation

2191− case elaborate ctxt (sMN 0 "refPatLHS") infP initEState

2192+ case elaborate ctxt (idris_datatypes ist) (sMN 0 "refPatLHS") infP initEState

2192 (erun fc (buildTC ist info ELHS [] fname (infTerm lhs))) of

2193 (erun fc (buildTC ist info ELHS [] fname (infTerm lhs))) of

2193 OK (ElabResult lhs' _ _ _ _, _) ->

2194 OK (ElabResult lhs' _ _ _ _, _) ->

2194 do -- not recursively calling here, because we don't

2195 do -- not recursively calling here, because we don't

src/Idris/Elab/Transform.hs+2−2

@@ -54,7 +54,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in

54 i <- getIState

55 let lhs = addImplPat i lhs_in

56 (ElabResult lhs' dlhs [] ctxt' newDecls, _) <-

57− tclift $ elaborate ctxt (sMN 0 "transLHS") infP initEState

57+ tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "transLHS") infP initEState

58 (erun fc (buildTC i info ELHS [] (sUN "transform")

59 (infTerm lhs)))

60 setContext ctxt'

@@ -69,7 +69,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in

69

70 let rhs = addImplBound i (map fst newargs) rhs_in

71 ((rhs', defer, ctxt', newDecls), _) <-

72− tclift $ elaborate ctxt (sMN 0 "transRHS") clhs_ty initEState

72+ tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "transRHS") clhs_ty initEState

73 (do pbinds i lhs_tm

74 setNextName

75 (ElabResult _ _ _ ctxt' newDecls) <- erun fc (build i info ERHS [] (sUN "transform") rhs)

src/Idris/Elab/Type.hs+1−1

@@ -67,7 +67,7 @@ buildType info syn fc opts n ty' = do

67 logLvl 2 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty

68

69 (ElabResult tyT' defer is ctxt' newDecls, log) <-

70− tclift $ elaborate ctxt n (TType (UVal 0)) initEState

70+ tclift $ elaborate ctxt (idris_datatypes i) n (TType (UVal 0)) initEState

71 (errAt "type of " n (erun fc (build i info ETyDecl [] n ty)))

72 setContext ctxt'

73 processTacticDecls info newDecls

src/Idris/Elab/Value.hs+1−1

@@ -64,7 +64,7 @@ elabValBind info aspat norm tm_in

64 -- * elaboration as a function a -> b

65

66 (ElabResult tm' defer is ctxt' newDecls, _) <-

67− tclift (elaborate ctxt (sMN 0 "val") infP initEState

67+ tclift (elaborate ctxt (idris_datatypes i) (sMN 0 "val") infP initEState

68 (build i info aspat [Reflection] (sMN 0 "val") (infTerm tm)))

69

70 -- Extend the context with new definitions created

src/Idris/Prover.hs+1−1

@@ -66,7 +66,7 @@ assumptionNames e

66

67prove :: Ctxt OptInfo -> Context -> Bool -> Name -> Type -> Idris ()

68prove opt ctxt lit n ty

69− = do let ps = initElaborator n ctxt ty

69+ = do ps <- fmap (\ist -> initElaborator n ctxt (idris_datatypes ist) ty) getIState

70 idemodePutSExp "start-proof-mode" n

71 (tm, prf) <- ploop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) Nothing

72 iLOG $ "Adding " ++ show tm

src/Idris/Reflection.hs+2−2

@@ -829,7 +829,7 @@ reifyReportPart (App _ (P (DCon _ _ _) n _) (Constant (Str msg))) | n == reflm "

829 Right (TextPart msg)

830reifyReportPart (App _ (P (DCon _ _ _) n _) ttn)

831 | n == reflm "NamePart" =

832− case runElab initEState (reifyTTName ttn) (initElaborator NErased initContext Erased) of

832+ case runElab initEState (reifyTTName ttn) (initElaborator NErased initContext emptyContext Erased) of

833 Error e -> Left . InternalMsg $

834 "could not reify name term " ++

835 show ttn ++

@@ -837,7 +837,7 @@ reifyReportPart (App _ (P (DCon _ _ _) n _) ttn)

837 OK (n', _)-> Right $ NamePart n'

838reifyReportPart (App _ (P (DCon _ _ _) n _) tm)

839 | n == reflm "TermPart" =

840− case runElab initEState (reifyTT tm) (initElaborator NErased initContext Erased) of

840+ case runElab initEState (reifyTT tm) (initElaborator NErased initContext emptyContext Erased) of

841 Error e -> Left . InternalMsg $

842 "could not reify reflected term " ++

843 show tm ++