git.iko.soy/Idris-dev
on master help sign in
Plumb datatype information through the proof state

This will allow looking up the constructors and parameters of datatypes: a necessary precondition to doing things like eliminator generation.

commitd97715efd18d0517b0a8792e90329d198f0b9377 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 16 Apr 2015, 14:54 (12 years ago) parent0c047fd
12 files changed+61−51
compare with master
unifiedsplit
src/Idris/AbsSyntaxTree.hs+1−22 src/Idris/Core/Elaborate.hs+13−5 src/Idris/Core/ProofState.hs+10−8 src/Idris/Core/TT.hs+20 src/Idris/Elab/Clause.hs+6−6 src/Idris/Elab/Instance.hs+1−1 src/Idris/Elab/Term.hs+3−2 src/Idris/Elab/Transform.hs+2−2 src/Idris/Elab/Type.hs+1−1 src/Idris/Elab/Value.hs+1−1 src/Idris/Prover.hs+1−1 src/Idris/Reflection.hs+2−2
src/Idris/AbsSyntaxTree.hs+1−22
@@ -581,14 +581,6 @@ dictionary :: FnOpts -> Bool
581581dictionary = elem Dictionary
582582
583583
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]
592584
593585-- | Type provider - what to provide
594586data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the second is the term
@@ -1083,20 +1075,7 @@ deriving instance Binary OptInfo
10831075deriving instance NFData OptInfo
10841076!-}
10851077
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
1099−
1078+-- | Syntactic sugar info
11001079data DSL' t = DSL { dsl_bind :: t,
11011080 dsl_return :: t,
11021081 dsl_apply :: t,
src/Idris/Core/Elaborate.hs+13−5
@@ -115,13 +115,13 @@ runElab a e ps = runStateT e (ES (ps, a) "" Nothing)
115115execElab :: aux -> Elab' aux a -> ProofState -> TC (ElabState aux)
116116execElab a e ps = execStateT e (ES (ps, a) "" Nothing)
117117
118−initElaborator :: Name -> Context -> Type -> ProofState
118+initElaborator :: Name -> Context -> Ctxt TypeInfo -> Type -> ProofState
119119initElaborator = newProof
120120
121−elaborate :: Context -> Name -> Type -> aux -> Elab' aux a -> TC (a, String)
122−elaborate ctxt n ty d elab = do let ps = initElaborator n ctxt ty
123− (a, ES ps' str _) <- runElab d elab ps
124− return $! (a, str)
121+elaborate :: Context -> Ctxt TypeInfo -> Name -> Type -> aux -> Elab' aux a -> TC (a, String)
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
124+ return $! (a, str)
125125
126126-- | Modify the auxiliary state
127127updateAux :: (aux -> aux) -> Elab' aux ()
@@ -178,6 +178,14 @@ set_context :: Context -> Elab' aux ()
178178set_context ctxt = do ES (p, a) logs prev <- get
179179 put (ES (p { context = ctxt }, a) logs prev)
180180
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+
181189-- | get the proof term
182190get_term :: Elab' aux Term
183191get_term = do ES p _ _ <- get
src/Idris/Core/ProofState.hs+10−8
@@ -41,6 +41,7 @@ data ProofState = PS { thname :: Name,
4141 autos :: [(Name, [Name])], -- ^ unsolved 'auto' implicits with their holes
4242 previous :: Maybe ProofState, -- ^ for undo
4343 context :: Context,
44+ datatypes :: Ctxt TypeInfo,
4445 plog :: String,
4546 unifylog :: Bool,
4647 done :: Bool,
@@ -292,14 +293,15 @@ query q = do ps <- get
292293addLog :: Monad m => String -> StateT TState m ()
293294addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })
294295
295−newProof :: Name -> Context -> Type -> ProofState
296−newProof n ctxt ty = let h = holeName 0
297− ty' = vToP ty
298− in PS n [h] [] 1 (mkProofTerm (Bind h (Hole ty')
299− (P Bound h ty'))) ty [] (h, []) [] []
300− Nothing [] []
301− [] [] []
302− Nothing ctxt "" False False [] []
296+newProof :: Name -> Context -> Ctxt TypeInfo -> Type -> ProofState
297+newProof n ctxt datatypes ty =
298+ let h = holeName 0
299+ ty' = vToP ty
300+ in PS n [h] [] 1 (mkProofTerm (Bind h (Hole ty')
301+ (P Bound h ty'))) ty [] (h, []) [] []
302+ Nothing [] []
303+ [] [] []
304+ Nothing ctxt datatypes "" False False [] []
303305
304306type TState = ProofState -- [TacticAction])
305307type RunTactic = RunTactic' TState
src/Idris/Core/TT.hs+20
@@ -882,6 +882,26 @@ data Datatype n = Data { d_typename :: n,
882882 d_cons :: [(n, TT n)] }
883883 deriving (Show, Functor, Eq)
884884
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+
885905instance Eq n => Eq (TT n) where
886906 (==) (P xt x _) (P yt y _) = x == y
887907 (==) (V x) (V y) = x == y
src/Idris/Elab/Clause.hs+6−6
@@ -451,7 +451,7 @@ checkPossible info fc tcgen fname lhs_in
451451 i <- getIState
452452 let lhs = addImplPat i lhs_in
453453 -- 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
455455 (erun fc (buildTC i info ELHS [] fname (infTerm lhs))) of
456456 OK (ElabResult lhs' _ _ ctxt' newDecls, _) ->
457457 do setContext ctxt'
@@ -538,7 +538,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
538538 "\n" ++ show (fn_ty, fn_is))
539539
540540 ((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
542542 (do res <- errAt "left hand side of " fname
543543 (erun fc (buildTC i info ELHS opts fname (infTerm lhs)))
544544 probs <- get_probs
@@ -613,7 +613,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc
613613 ctxt <- getContext -- new context with where block added
614614 logLvl 5 "STARTING CHECK"
615615 ((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
617617 (do pbinds ist lhs_tm
618618 mapM_ setinj (nub (params ++ inj))
619619 setNextName
@@ -774,7 +774,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
774774 let lhs = stripLinear i $ stripUnmatchable i $ propagateParams i params fn_ty (addImplPat i lhs_in)
775775 logLvl 2 ("LHS: " ++ show lhs)
776776 (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
778778 (errAt "left hand side of with in " fname
779779 (erun fc (buildTC i info ELHS opts fname (infTerm lhs))) )
780780 setContext ctxt'
@@ -791,7 +791,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
791791 logLvl 5 ("Checking " ++ showTmImpls wval)
792792 -- Elaborate wval in this context
793793 ((wval', defer, is, ctxt', newDecls), _) <-
794− tclift $ elaborate ctxt (sMN 0 "withRHS")
794+ tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "withRHS")
795795 (bindTyArgs PVTy bargs infP) initEState
796796 (do pbinds i lhs_tm
797797 setNextName
@@ -889,7 +889,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
889889 ctxt <- getContext -- New context with block added
890890 i <- getIState
891891 ((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
893893 (do pbinds i lhs_tm
894894 setNextName
895895 (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
177177 let ty = addImpl [] i ty'
178178 ctxt <- getContext
179179 (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
181181 (errAt "type of " iname (erun fc (build i info ERHS [] iname ty)))
182182 setContext ctxt'
183183 processTacticDecls info newDecls
src/Idris/Elab/Term.hs+3−2
@@ -1000,9 +1000,10 @@ elab ist info emode opts fn tm
10001000 -- Save the old state - we need a fresh proof state to avoid
10011001 -- capturing lexically available variables in the quoted term.
10021002 ctxt <- get_context
1003+ datatypes <- get_datatypes
10031004 saveState
10041005 updatePS (const .
1005− newProof (sMN 0 "q") ctxt $
1006+ newProof (sMN 0 "q") ctxt datatypes $
10061007 P Ref (reflm "TT") Erased)
10071008
10081009 -- Re-add the unquotes, letting Idris infer the (fictional)
@@ -2188,7 +2189,7 @@ processTacticDecls info steps =
21882189 let lhs = addImplPat ist lhs_in
21892190 let fc = fileFC "elab_reflected_totality"
21902191 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
21922193 (erun fc (buildTC ist info ELHS [] fname (infTerm lhs))) of
21932194 OK (ElabResult lhs' _ _ _ _, _) ->
21942195 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
5454 i <- getIState
5555 let lhs = addImplPat i lhs_in
5656 (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
5858 (erun fc (buildTC i info ELHS [] (sUN "transform")
5959 (infTerm lhs)))
6060 setContext ctxt'
@@ -69,7 +69,7 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ tf) _) rhs_in
6969
7070 let rhs = addImplBound i (map fst newargs) rhs_in
7171 ((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
7373 (do pbinds i lhs_tm
7474 setNextName
7575 (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
6767 logLvl 2 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty
6868
6969 (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
7171 (errAt "type of " n (erun fc (build i info ETyDecl [] n ty)))
7272 setContext ctxt'
7373 processTacticDecls info newDecls
src/Idris/Elab/Value.hs+1−1
@@ -64,7 +64,7 @@ elabValBind info aspat norm tm_in
6464 -- * elaboration as a function a -> b
6565
6666 (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
6868 (build i info aspat [Reflection] (sMN 0 "val") (infTerm tm)))
6969
7070 -- Extend the context with new definitions created
src/Idris/Prover.hs+1−1
@@ -66,7 +66,7 @@ assumptionNames e
6666
6767prove :: Ctxt OptInfo -> Context -> Bool -> Name -> Type -> Idris ()
6868prove 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
7070 idemodePutSExp "start-proof-mode" n
7171 (tm, prf) <- ploop n True ("-" ++ show n) [] (ES (ps, initEState) "" Nothing) Nothing
7272 iLOG $ "Adding " ++ show tm
src/Idris/Reflection.hs+2−2
@@ -829,7 +829,7 @@ reifyReportPart (App _ (P (DCon _ _ _) n _) (Constant (Str msg))) | n == reflm "
829829 Right (TextPart msg)
830830reifyReportPart (App _ (P (DCon _ _ _) n _) ttn)
831831 | 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
833833 Error e -> Left . InternalMsg $
834834 "could not reify name term " ++
835835 show ttn ++
@@ -837,7 +837,7 @@ reifyReportPart (App _ (P (DCon _ _ _) n _) ttn)
837837 OK (n', _)-> Right $ NamePart n'
838838reifyReportPart (App _ (P (DCon _ _ _) n _) tm)
839839 | 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
841841 Error e -> Left . InternalMsg $
842842 "could not reify reflected term " ++
843843 show tm ++