eaf5211 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add the ability to define datatypes in Elab

eaf5211David Raymond Christiansen11 years ago

CHANGELOG+10

compare with master

unifiedsplit

@@ -23,6 +23,16 @@ in a C function pointer.

23* C function pointers can be called.

24* Idris can access pointers to C globals.

26+Elaborator reflection updates

27+-----------------------------

28+

29+* Datatypes can now be defined from elaborator reflection:

30+ - declareDatatype adds the type constructor declaration to the context

31+ - defineDatatype adds the constructors to the datatype

32+ - To declare an inductive-recursive family, declare the types of the

33+ function and the type constructor before defining the pattern-match

34+ cases and constructors.

35+

26Minor language changes

36Minor language changes

27----------------------

37----------------------

libs/prelude/Language/Reflection/Elab.idr+43−2

@@ -57,11 +57,11 @@ data TyConArg =

57 ||| Indices are not uniform

58 TyConIndex FunArg

60−||| A type declaration

60+||| A type declaration for a function or datatype

61record TyDecl where

62 constructor Declare

64− ||| The name of the function being declared.

64+ ||| The fully-qualified name of the function or datatype being declared.

65 name : TTName

67 ||| Each argument is in the scope of the names of previous arguments.

@@ -83,6 +83,34 @@ record FunDefn a where

83 clauses : List (FunClause a)

86+||| A constructor to be associated with a new datatype.

87+record ConstructorDefn where

88+ constructor Constructor

89+

90+ ||| The name of the constructor. The name must _not_ be qualified -

91+ ||| that is, it should begin with the `UN` or `MN` constructors.

92+ name : TTName

93+

94+ ||| The constructor arguments. Idris will infer which arguments are

95+ ||| datatype parameters.

96+ arguments : List FunArg

97+

98+ ||| The specific type constructed by the constructor.

99+ returnType : Raw

100+

101+

102+||| A definition of a datatype to be added during an elaboration script.

103+record DataDefn where

104+ constructor DefineDatatype

105+ ||| The name of the datatype being defined. It must be

106+ ||| fully-qualified, and it must have been previously declared as a

107+ ||| datatype.

108+ name : TTName

109+

110+ ||| A list of constructors for the datatype.

111+ constructors : List ConstructorDefn

112+

113+

86data CtorArg = CtorParameter FunArg | CtorField FunArg

114data CtorArg = CtorParameter FunArg | CtorField FunArg

115

88||| A reflected datatype definition

116||| A reflected datatype definition

@@ -151,6 +179,8 @@ data Elab : Type -> Type where

151

179

152 Prim__DeclareType : TyDecl -> Elab ()

180 Prim__DeclareType : TyDecl -> Elab ()

153 Prim__DefineFunction : FunDefn Raw -> Elab ()

181 Prim__DefineFunction : FunDefn Raw -> Elab ()

182+ Prim__DeclareDatatype : TyDecl -> Elab ()

183+ Prim__DefineDatatype : DataDefn -> Elab ()

154 Prim__AddInstance : TTName -> TTName -> Elab ()

184 Prim__AddInstance : TTName -> TTName -> Elab ()

155 Prim__IsTCName : TTName -> Elab Bool

185 Prim__IsTCName : TTName -> Elab Bool

156

186

@@ -510,6 +540,17 @@ namespace Tactics

510 defineFunction : FunDefn Raw -> Elab ()

540 defineFunction : FunDefn Raw -> Elab ()

511 defineFunction defun = Prim__DefineFunction defun

541 defineFunction defun = Prim__DefineFunction defun

512

542

543+ ||| Declare a datatype in the global context. This step only

544+ ||| establishes the type constructor; use `defineDatatype` to give

545+ ||| it constructors.

546+ export

547+ declareDatatype : TyDecl -> Elab ()

548+ declareDatatype decl = Prim__DeclareDatatype decl

549+

550+ export

551+ defineDatatype : DataDefn -> Elab ()

552+ defineDatatype defn = Prim__DefineDatatype defn

553+

513 ||| Register a new implementation for interface resolution.

554 ||| Register a new implementation for interface resolution.

514 |||

555 |||

515 ||| @ ifaceName the name of the interface for which an implementation is being registered

556 ||| @ ifaceName the name of the interface for which an implementation is being registered

src/Idris/AbsSyntaxTree.hs+3

@@ -775,6 +775,9 @@ data Directive = DLib Codegen String |

775data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type

776 | RClausesInstrs Name [([(Name, Term)], Term, Term)]

777 | RAddInstance Name Name

778+ | RDatatypeDeclInstrs Name [PArg]

779+ | RDatatypeDefnInstrs Name Type [(Name, [PArg], Type)]

780+ -- ^ Datatype, constructors

778

781

779-- | For elaborator state

782-- | For elaborator state

780data EState = EState {

783data EState = EState {

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

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

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

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

141

142−initElaborator :: Name -> Context -> Ctxt TypeInfo -> Type -> ProofState

142+initElaborator :: Name -- ^ the name of what's to be elaborated

143+ -> Context -- ^ the current global context

144+ -> Ctxt TypeInfo -- ^ the value of the idris_datatypes field of IState

145+ -> Int -- ^ the value of the idris_name field of IState

146+ -> Type -- ^ the goal type

147+ -> ProofState

143initElaborator = newProof

148initElaborator = newProof

144

149

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

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

151+elaborate ctxt datatypes globalNames n ty d elab =

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

152+ do let ps = initElaborator n ctxt datatypes globalNames ty

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

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

148− return $! (a, str)

154+ return $! (a, str)

149

155

150-- | Modify the auxiliary state

156-- | Modify the auxiliary state

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

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

@@ -210,6 +216,14 @@ set_datatypes :: Ctxt TypeInfo -> Elab' aux ()

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

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

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

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

212

218

219+get_global_nextname :: Elab' aux Int

220+get_global_nextname = do ES (ps, _) _ _ <- get

221+ return (global_nextname ps)

222+

223+set_global_nextname :: Int -> Elab' aux ()

224+set_global_nextname i = do ES (ps, a) logs prev <- get

225+ put $ ES (ps { global_nextname = i}, a) logs prev

226+

213-- | get the proof term

227-- | get the proof term

214get_term :: Elab' aux Term

228get_term :: Elab' aux Term

215get_term = do ES p _ _ <- get

229get_term = do ES p _ _ <- get

src/Idris/Core/ProofState.hs+12−4

@@ -25,7 +25,10 @@ import Util.Pretty hiding (fill)

25data ProofState = PS { thname :: Name,

26 holes :: [Name], -- ^ holes still to be solved

27 usedns :: [Name], -- ^ used names, don't use again

28− nextname :: Int, -- ^ name supply

28+ nextname :: Int, -- ^ name supply, for locally unique names

29+ global_nextname :: Int, -- ^ a mirror of the global name supply,

30+ -- for generating things like type tags

31+ -- in reflection

29 pterm :: ProofTerm, -- ^ current proof term

32 pterm :: ProofTerm, -- ^ current proof term

30 ptype :: Type, -- ^ original goal

33 ptype :: Type, -- ^ original goal

31 dontunify :: [Name], -- ^ explicitly given by programmer, leave it

34 dontunify :: [Name], -- ^ explicitly given by programmer, leave it

@@ -305,11 +308,16 @@ query q = do ps <- get

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

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

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

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

307

310

308−newProof :: Name -> Context -> Ctxt TypeInfo -> Type -> ProofState

311+newProof :: Name -- ^ the name of what's to be elaborated

312+ -> Context -- ^ the current global context

313+ -> Ctxt TypeInfo -- ^ the value of the idris_datatypes field of IState

314+ -> Int -- ^ the value of the idris_name field of IState

315+ -> Type -- ^ the goal type

316+ -> ProofState

309−newProof n ctxt datatypes ty =

317+newProof n ctxt datatypes globalNames ty =

310 let h = holeName 0

318 let h = holeName 0

311 ty' = vToP ty

319 ty' = vToP ty

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

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

313 (P Bound h ty'))) ty [] (h, []) [] []

321 (P Bound h ty'))) ty [] (h, []) [] []

314 Nothing [] []

322 Nothing [] []

315 [] [] [] []

323 [] [] [] []

src/Idris/Elab/Clause.hs+24−18

@@ -486,14 +486,15 @@ checkPossible info fc tcgen fname lhs_in

486 i <- getIState

487 let lhs = addImplPat i lhs_in

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

489− case elaborate ctxt (idris_datatypes i) (sMN 0 "patLHS") infP initEState

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

490 (erun fc (buildTC i info ELHS [] fname

491 (allNamesIn lhs_in)

492 (infTerm lhs))) of

493− OK (ElabResult lhs' _ _ ctxt' newDecls highlights, _) ->

493+ OK (ElabResult lhs' _ _ ctxt' newDecls highlights newGName, _) ->

494 do setContext ctxt'

495 processTacticDecls info newDecls

496 sendHighlighting highlights

497+ updateIState $ \i -> i { idris_name = newGName }

497 let lhs_tm = orderPats (getInferTerm lhs')

498 let lhs_tm = orderPats (getInferTerm lhs')

498 case recheck ctxt' [] (forget lhs_tm) lhs_tm of

499 case recheck ctxt' [] (forget lhs_tm) lhs_tm of

499 OK _ -> return True

500 OK _ -> return True

@@ -587,8 +588,8 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

587 logElab 4 ("Fixed parameters: " ++ show params ++ " from " ++ showTmImpls lhs_in ++

588 logElab 4 ("Fixed parameters: " ++ show params ++ " from " ++ showTmImpls lhs_in ++

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

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

589

590

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

591+ ((ElabResult lhs' dlhs [] ctxt' newDecls highlights newGName, probs, inj), _) <-

591− tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "patLHS") infP initEState

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

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

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

593 (erun fc (buildTC i info ELHS opts fname

594 (erun fc (buildTC i info ELHS opts fname

594 (allNamesIn lhs_in)

595 (allNamesIn lhs_in)

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

599 setContext ctxt'

600 setContext ctxt'

600 processTacticDecls info newDecls

601 processTacticDecls info newDecls

601 sendHighlighting highlights

602 sendHighlighting highlights

603+ updateIState $ \i -> i { idris_name = newGName }

602

604

603 when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)

605 when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)

604

606

@@ -670,14 +672,14 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

670 logElab 2 $ "RHS: " ++ show (map fst newargs_all) ++ " " ++ showTmImpls rhs

672 logElab 2 $ "RHS: " ++ show (map fst newargs_all) ++ " " ++ showTmImpls rhs

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

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

672 logElab 5 "STARTING CHECK"

674 logElab 5 "STARTING CHECK"

673− ((rhs', defer, holes, is, probs, ctxt', newDecls, highlights), _) <-

675+ ((rhs', defer, holes, is, probs, ctxt', newDecls, highlights, newGName), _) <-

674− tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "patRHS") clhsty initEState

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

675 (do pbinds ist lhs_tm

677 (do pbinds ist lhs_tm

676 -- proof search can use explicitly written names

678 -- proof search can use explicitly written names

677 mapM_ addPSname (allNamesIn lhs_in)

679 mapM_ addPSname (allNamesIn lhs_in)

678 mapM_ setinj (nub (tcparams ++ inj))

680 mapM_ setinj (nub (tcparams ++ inj))

679 setNextName

681 setNextName

680− (ElabResult _ _ is ctxt' newDecls highlights) <-

682+ (ElabResult _ _ is ctxt' newDecls highlights newGName) <-

681 errAt "right hand side of " fname (Just clhsty)

683 errAt "right hand side of " fname (Just clhsty)

682 (erun fc (build i winfo ERHS opts fname rhs))

684 (erun fc (build i winfo ERHS opts fname rhs))

683 errAt "right hand side of " fname (Just clhsty)

685 errAt "right hand side of " fname (Just clhsty)

@@ -688,10 +690,11 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

688 (map fst $ case_decls aux) ctxt tt) []

690 (map fst $ case_decls aux) ctxt tt) []

689 probs <- get_probs

691 probs <- get_probs

690 hs <- get_holes

692 hs <- get_holes

691− return (tm, ds, hs, is, probs, ctxt', newDecls, highlights))

693+ return (tm, ds, hs, is, probs, ctxt', newDecls, highlights, newGName))

692 setContext ctxt'

694 setContext ctxt'

693 processTacticDecls info newDecls

695 processTacticDecls info newDecls

694 sendHighlighting highlights

696 sendHighlighting highlights

697+ updateIState $ \i -> i { idris_name = newGName }

695

698

696 when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)

699 when inf $ addTyInfConstraints fc (map (\(x,y,_,_,_,_,_) -> (x,y)) probs)

697

700

@@ -838,8 +841,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

838 propagateParams i params fn_ty (allNamesIn lhs_in)

841 propagateParams i params fn_ty (allNamesIn lhs_in)

839 (addImplPat i lhs_in)

842 (addImplPat i lhs_in)

840 logElab 2 ("LHS: " ++ show lhs)

843 logElab 2 ("LHS: " ++ show lhs)

841− (ElabResult lhs' dlhs [] ctxt' newDecls highlights, _) <-

844+ (ElabResult lhs' dlhs [] ctxt' newDecls highlights newGName, _) <-

842− tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "patLHS") infP initEState

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

843 (errAt "left hand side of with in " fname Nothing

846 (errAt "left hand side of with in " fname Nothing

844 (erun fc (buildTC i info ELHS opts fname

847 (erun fc (buildTC i info ELHS opts fname

845 (allNamesIn lhs_in)

848 (allNamesIn lhs_in)

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

847 setContext ctxt'

850 setContext ctxt'

848 processTacticDecls info newDecls

851 processTacticDecls info newDecls

849 sendHighlighting highlights

852 sendHighlighting highlights

853+ updateIState $ \i -> i { idris_name = newGName }

850

854

851 ctxt <- getContext

855 ctxt <- getContext

852 let lhs_tm = orderPats (getInferTerm lhs')

856 let lhs_tm = orderPats (getInferTerm lhs')

@@ -860,22 +864,23 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

860 let wval = addImplBound i (map fst bargs) wval_in

864 let wval = addImplBound i (map fst bargs) wval_in

861 logElab 5 ("Checking " ++ showTmImpls wval)

865 logElab 5 ("Checking " ++ showTmImpls wval)

862 -- Elaborate wval in this context

866 -- Elaborate wval in this context

863− ((wval', defer, is, ctxt', newDecls, highlights), _) <-

867+ ((wval', defer, is, ctxt', newDecls, highlights, newGName), _) <-

864− tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "withRHS")

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

865 (bindTyArgs PVTy bargs infP) initEState

869 (bindTyArgs PVTy bargs infP) initEState

866 (do pbinds i lhs_tm

870 (do pbinds i lhs_tm

867 -- proof search can use explicitly written names

871 -- proof search can use explicitly written names

868 mapM_ addPSname (allNamesIn lhs_in)

872 mapM_ addPSname (allNamesIn lhs_in)

869 setNextName

873 setNextName

870 -- TODO: may want where here - see winfo abpve

874 -- TODO: may want where here - see winfo abpve

871− (ElabResult _ d is ctxt' newDecls highlights) <- errAt "with value in " fname Nothing

875+ (ElabResult _ d is ctxt' newDecls highlights newGName) <- errAt "with value in " fname Nothing

872 (erun fc (build i info ERHS opts fname (infTerm wval)))

876 (erun fc (build i info ERHS opts fname (infTerm wval)))

873 erun fc $ psolve lhs_tm

877 erun fc $ psolve lhs_tm

874 tt <- get_term

878 tt <- get_term

875− return (tt, d, is, ctxt', newDecls, highlights))

879+ return (tt, d, is, ctxt', newDecls, highlights, newGName))

876 setContext ctxt'

880 setContext ctxt'

877 processTacticDecls info newDecls

881 processTacticDecls info newDecls

878 sendHighlighting highlights

882 sendHighlighting highlights

883+ updateIState $ \i -> i { idris_name = newGName }

879

884

880 def' <- checkDef fc iderr True defer

885 def' <- checkDef fc iderr True defer

881 let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'

886 let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'

@@ -970,18 +975,19 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

970 logElab 5 ("New RHS " ++ showTmImpls rhs)

975 logElab 5 ("New RHS " ++ showTmImpls rhs)

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

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

972 i <- getIState

977 i <- getIState

973− ((rhs', defer, is, ctxt', newDecls, highlights), _) <-

978+ ((rhs', defer, is, ctxt', newDecls, highlights, newGName), _) <-

974− tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "wpatRHS") clhsty initEState

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

975 (do pbinds i lhs_tm

980 (do pbinds i lhs_tm

976 setNextName

981 setNextName

977− (ElabResult _ d is ctxt' newDecls highlights) <-

982+ (ElabResult _ d is ctxt' newDecls highlights newGName) <-

978 erun fc (build i info ERHS opts fname rhs)

983 erun fc (build i info ERHS opts fname rhs)

979 psolve lhs_tm

984 psolve lhs_tm

980 tt <- get_term

985 tt <- get_term

981− return (tt, d, is, ctxt', newDecls, highlights))

986+ return (tt, d, is, ctxt', newDecls, highlights, newGName))

982 setContext ctxt'

987 setContext ctxt'

983 processTacticDecls info newDecls

988 processTacticDecls info newDecls

984 sendHighlighting highlights

989 sendHighlighting highlights

990+ updateIState $ \i -> i { idris_name = newGName }

985

991

986 def' <- checkDef fc iderr True defer

992 def' <- checkDef fc iderr True defer

987 let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'

993 let def'' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, False, True))) def'

src/Idris/Elab/Data.hs+3−65

@@ -90,7 +90,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)

90 ttag <- getName

91 i <- getIState

92 let as = map (const (Left (Msg ""))) (getArgTys cty)

93− let params = findParams (map snd cons)

93+ let params = findParams n (map snd cons)

94 logElab 2 $ "Parameters : " ++ show params

95 -- TI contains information about mutually declared types - this will

96 -- be updated when the mutual block is complete

@@ -132,13 +132,6 @@ elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)

132 (nfc, AnnName n Nothing Nothing Nothing))

133 dcons

134 where

135− setDetaggable :: Name -> Idris ()

136− setDetaggable n = do

137− ist <- getIState

138− let opt = idris_optimisation ist

139− case lookupCtxt n opt of

140− [oi] -> putIState ist{ idris_optimisation = addDef n oi{ detaggable = True } opt }

141− _ -> putIState ist{ idris_optimisation = addDef n (Optimise [] True) opt }

142

135

143 checkDefinedAs fc n t i

136 checkDefinedAs fc n t i

144 = let defined = tclift $ tfail (At fc (AlreadyDefined n))

137 = let defined = tclift $ tfail (At fc (AlreadyDefined n))

@@ -152,62 +145,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n nfc t_in dcons)

152 _ -> defined

145 _ -> defined

153 _ -> defined

146 _ -> defined

154 _ -> defined

147 _ -> defined

155− -- parameters are names which are unchanged across the structure,

148+

156− -- which appear exactly once in the return type of a constructor

157−

158− -- First, find all applications of the constructor, then check over

159− -- them for repeated arguments

160−

161− findParams :: [Type] -> [Int]

162− findParams ts = let allapps = map getDataApp ts

163− -- do each constructor separately, then merge the results (names

164− -- may change between constructors)

165− conParams = map paramPos allapps in

166− inAll conParams

167−

168− inAll :: [[Int]] -> [Int]

169− inAll [] = []

170− inAll (x : xs) = filter (\p -> all (\ps -> p `elem` ps) xs) x

171−

172− paramPos [] = []

173− paramPos (args : rest)

174− = dropNothing $ keepSame (zip [0..] args) rest

175−

176− dropNothing [] = []

177− dropNothing ((x, Nothing) : ts) = dropNothing ts

178− dropNothing ((x, _) : ts) = x : dropNothing ts

179−

180− keepSame :: [(Int, Maybe Name)] -> [[Maybe Name]] ->

181− [(Int, Maybe Name)]

182− keepSame as [] = as

183− keepSame as (args : rest) = keepSame (update as args) rest

184− where

185− update [] _ = []

186− update _ [] = []

187− update ((n, Just x) : as) (Just x' : args)

188− | x == x' = (n, Just x) : update as args

189− update ((n, _) : as) (_ : args) = (n, Nothing) : update as args

190−

191− getDataApp :: Type -> [[Maybe Name]]

192− getDataApp f@(App _ _ _)

193− | (P _ d _, args) <- unApply f

194− = if (d == n) then [mParam args args] else []

195− getDataApp (Bind n (Pi _ t _) sc)

196− = getDataApp t ++ getDataApp (instantiate (P Bound n t) sc)

197− getDataApp _ = []

198−

199− -- keep the arguments which are single names, which don't appear

200− -- elsewhere

201−

202− mParam args [] = []

203− mParam args (P Bound n _ : rest)

204− | count n args == 1

205− = Just n : mParam args rest

206− where count n [] = 0

207− count n (t : ts)

208− | n `elem` freeNames t = 1 + count n ts

209− | otherwise = count n ts

210− mParam args (_ : rest) = Nothing : mParam args rest

211

149

212 cname (_, _, n, _, _, _, _) = n

150 cname (_, _, n, _, _, _, _) = n

213

151

@@ -263,7 +201,7 @@ elabCon info syn tn codata expkind dkind (doc, argDocs, n, nfc, t_in, fc, forcen

263 where

201 where

264 tyIs con (Bind n b sc) = tyIs con (substV (P Bound n Erased) sc)

202 tyIs con (Bind n b sc) = tyIs con (substV (P Bound n Erased) sc)

265 tyIs con t | (P Bound n' _, _) <- unApply t

203 tyIs con t | (P Bound n' _, _) <- unApply t

266− = if n' /= tn then

204+ = if n' /= tn then

267 tclift $ tfail (At fc (Elaborating "constructor " con Nothing

205 tclift $ tfail (At fc (Elaborating "constructor " con Nothing

268 (Msg ("Type level variable " ++ show n' ++ " is not " ++ show tn))))

206 (Msg ("Type level variable " ++ show n' ++ " is not " ++ show tn))))

269 else return ()

207 else return ()

src/Idris/Elab/Instance.hs+4−2

@@ -186,12 +186,14 @@ elabInstance info syn doc argDocs what fc cs acc opts n nfc ps t expn ds = do

186 ty' <- implicit info syn iname ty'

187 let ty = addImpl [] i ty'

188 ctxt <- getContext

189− (ElabResult tyT _ _ ctxt' newDecls highlights, _) <-

189+ (ElabResult tyT _ _ ctxt' newDecls highlights newGName, _) <-

190− tclift $ elaborate ctxt (idris_datatypes i) iname (TType (UVal 0)) initEState

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

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

192 setContext ctxt'

193 processTacticDecls info newDecls

194 sendHighlighting highlights

195+ updateIState $ \i -> i { idris_name = newGName }

196+

195 ctxt <- getContext

197 ctxt <- getContext

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

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

197 let nty = normalise ctxt [] cty

199 let nty = normalise ctxt [] cty

src/Idris/Elab/RunElab.hs+5−3

@@ -32,18 +32,20 @@ elabRunElab info fc script' ns =

32 mustBeElabScript scriptTy

33 ist <- getIState

34 ctxt <- getContext

35− (ElabResult tyT' defer is ctxt' newDecls highlights, log) <-

35+ (ElabResult tyT' defer is ctxt' newDecls highlights newGName, log) <-

36− tclift $ elaborate ctxt (idris_datatypes ist) (sMN 0 "toplLevelElab") elabScriptTy initEState

36+ tclift $ elaborate ctxt (idris_datatypes ist) (idris_name ist) (sMN 0 "toplLevelElab") elabScriptTy initEState

37 (transformErr RunningElabScript

38 (erun fc (do tm <- runElabAction ist fc [] script ns

39 EState is _ impls highlights <- getAux

40 ctxt <- get_context

41 let ds = [] -- todo

42 log <- getLog

43+ newGName <- get_global_nextname

43− return (ElabResult tm ds (map snd is) ctxt impls highlights))))

44+ return (ElabResult tm ds (map snd is) ctxt impls highlights newGName))))

47 setContext ctxt'

48 setContext ctxt'

48 processTacticDecls info newDecls

49 processTacticDecls info newDecls

49 sendHighlighting highlights

50 sendHighlighting highlights

51+ updateIState $ \i -> i { idris_name = newGName }

src/Idris/Elab/Term.hs+159−23

@@ -52,6 +52,9 @@ data ElabResult =

52 , resultTyDecls :: [RDeclInstructions]

53 -- ^ Meta-info about the new type declarations

54 , resultHighlighting :: [(FC, OutputAnnotation)]

55+ -- ^ Saved highlights from elaboration

56+ , resultName :: Int

57+ -- ^ The new global name counter

55 }

58 }

@@ -122,9 +125,10 @@ build ist info emode opts fn tm

122 ctxt <- get_context

125 ctxt <- get_context

123 let (tm, ds) = runState (collectDeferred (Just fn) (map fst is) ctxt tt) []

126 let (tm, ds) = runState (collectDeferred (Just fn) (map fst is) ctxt tt) []

124 log <- getLog

127 log <- getLog

128+ g_nextname <- get_global_nextname

125 if log /= ""

129 if log /= ""

126− then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights)

130+ then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)

127− else return (ElabResult tm ds (map snd is) ctxt impls highlights)

131+ else return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)

128 where pattern = emode == ELHS

132 where pattern = emode == ELHS

129 tydecl = emode == ETyDecl

133 tydecl = emode == ETyDecl

130

134

@@ -166,9 +170,10 @@ buildTC ist info emode opts fn ns tm

166 ctxt <- get_context

170 ctxt <- get_context

167 let (tm, ds) = runState (collectDeferred (Just fn) (map fst is) ctxt tt) []

171 let (tm, ds) = runState (collectDeferred (Just fn) (map fst is) ctxt tt) []

168 log <- getLog

172 log <- getLog

173+ g_nextname <- get_global_nextname

169 if (log /= "")

174 if (log /= "")

170− then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights)

175+ then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)

171− else return (ElabResult tm ds (map snd is) ctxt impls highlights)

176+ else return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)

172 where pattern = emode == ELHS

177 where pattern = emode == ELHS

173

178

174-- return whether arguments of the given constructor name can be

179-- return whether arguments of the given constructor name can be

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

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

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

1159 ctxt <- get_context

1164 ctxt <- get_context

1160 datatypes <- get_datatypes

1165 datatypes <- get_datatypes

1166+ g_nextname <- get_global_nextname

1161 saveState

1167 saveState

1162 updatePS (const .

1168 updatePS (const .

1163− newProof (sMN 0 "q") ctxt datatypes $

1169+ newProof (sMN 0 "q") ctxt datatypes g_nextname $

1164 P Ref (reflm "TT") Erased)

1170 P Ref (reflm "TT") Erased)

1165

1171

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

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

@@ -1839,11 +1845,74 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

1839 updateAux $ \e -> e { new_tyDecls = RClausesInstrs n clauses'' : new_tyDecls e}

1845 updateAux $ \e -> e { new_tyDecls = RClausesInstrs n clauses'' : new_tyDecls e}

1840 return ()

1846 return ()

1841

1847

1848+

1842 checkClosed :: Raw -> Elab' aux (Term, Type)

1849 checkClosed :: Raw -> Elab' aux (Term, Type)

1843 checkClosed tm = do ctxt <- get_context

1850 checkClosed tm = do ctxt <- get_context

1844 (val, ty) <- lift $ check ctxt [] tm

1851 (val, ty) <- lift $ check ctxt [] tm

1845 return $! (finalise val, finalise ty)

1852 return $! (finalise val, finalise ty)

1846

1853

1854+ -- | Add another argument to a Pi

1855+ mkPi :: RFunArg -> Raw -> Raw

1856+ mkPi arg rTy = RBind (argName arg) (Pi Nothing (argTy arg) (RUType AllTypes)) rTy

1857+

1858+ mustBeType ctxt tm ty =

1859+ case normaliseAll ctxt [] (finalise ty) of

1860+ UType _ -> return ()

1861+ TType _ -> return ()

1862+ ty' -> lift . tfail . InternalMsg $

1863+ show tm ++ " is not a type: it's " ++ show ty'

1864+

1865+ mustNotBeDefined ctxt n =

1866+ case lookupDefExact n ctxt of

1867+ Just _ -> lift . tfail . InternalMsg $

1868+ show n ++ " is already defined."

1869+ Nothing -> return ()

1870+

1871+ -- | Prepare a constructor to be added to a datatype being defined here

1872+ prepareConstructor :: Name -> RConstructorDefn -> ElabD (Name, [PArg], Type)

1873+ prepareConstructor tyn (RConstructor cn args resTy) =

1874+ do ctxt <- get_context

1875+ -- ensure the constructor name is not qualified, and

1876+ -- construct a qualified one

1877+ notQualified cn

1878+ let qcn = qualify cn

1879+

1880+ -- ensure that the constructor name is not defined already

1881+ mustNotBeDefined ctxt qcn

1882+

1883+ -- construct the actual type for the constructor

1884+ let cty = foldr mkPi resTy args

1885+ (checkedTy, ctyTy) <- lift $ check ctxt [] cty

1886+ mustBeType ctxt checkedTy ctyTy

1887+

1888+ -- ensure that the constructor builds the right family

1889+ case unApply (getRetTy (normaliseAll ctxt [] (finalise checkedTy))) of

1890+ (P _ n _, _) | n == tyn -> return ()

1891+ t -> lift . tfail . Msg $ "The constructor " ++ show cn ++

1892+ " doesn't construct " ++ show tyn ++

1893+ " (return type is " ++ show t ++ ")"

1894+

1895+ -- add temporary type declaration for constructor (so it can

1896+ -- occur in later constructor types)

1897+ set_context (addTyDecl qcn (DCon 0 0 False) checkedTy ctxt)

1898+

1899+ -- Save the implicits for high-level Idris

1900+ let impls = map rFunArgToPArg args

1901+

1902+ return (qcn, impls, checkedTy)

1903+

1904+ where

1905+ notQualified (NS _ _) = lift . tfail . Msg $ "Constructor names may not be qualified"

1906+ notQualified _ = return ()

1907+

1908+ qualify n = case tyn of

1909+ (NS _ ns) -> NS n ns

1910+ _ -> n

1911+

1912+ getRetTy :: Type -> Type

1913+ getRetTy (Bind _ (Pi _ _ _) sc) = getRetTy sc

1914+ getRetTy ty = ty

1915+

1847 -- | Do a step in the reflected elaborator monad. The input is the

1916 -- | Do a step in the reflected elaborator monad. The input is the

1848 -- step, the output is the (reflected) term returned.

1917 -- step, the output is the (reflected) term returned.

1849 runTacTm :: Term -> ElabD Term

1918 runTacTm :: Term -> ElabD Term

@@ -2052,20 +2121,10 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

2052 | n == tacN "Prim__DeclareType", [decl] <- args

2121 | n == tacN "Prim__DeclareType", [decl] <- args

2053 = do (RDeclare n args res) <- reifyTyDecl decl

2122 = do (RDeclare n args res) <- reifyTyDecl decl

2054 ctxt <- get_context

2123 ctxt <- get_context

2055− let mkPi arg res = RBind (argName arg)

2056− (Pi Nothing (argTy arg) (RUType AllTypes))

2057− res

2058− rty = foldr mkPi res args

2124+ let rty = foldr mkPi res args

2059 (checked, ty') <- lift $ check ctxt [] rty

2125 (checked, ty') <- lift $ check ctxt [] rty

2060− case normaliseAll ctxt [] (finalise ty') of

2126+ mustBeType ctxt checked ty'

2061− UType _ -> return ()

2127+ mustNotBeDefined ctxt n

2062− TType _ -> return ()

2063− ty'' -> lift . tfail . InternalMsg $

2064− show checked ++ " is not a type: it's " ++ show ty''

2065− case lookupDefExact n ctxt of

2066− Just _ -> lift . tfail . InternalMsg $

2067− show n ++ " is already defined."

2068− Nothing -> return ()

2069 let decl = TyDecl Ref checked

2128 let decl = TyDecl Ref checked

2070 ctxt' = addCtxtDef n decl ctxt

2129 ctxt' = addCtxtDef n decl ctxt

2071 set_context ctxt'

2130 set_context ctxt'

@@ -2076,11 +2135,46 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

2076 = do defn <- reifyFunDefn decl

2135 = do defn <- reifyFunDefn decl

2077 defineFunction defn

2136 defineFunction defn

2078 returnUnit

2137 returnUnit

2138+ | n == tacN "Prim__DeclareDatatype", [decl] <- args

2139+ = do RDeclare n args resTy <- reifyTyDecl decl

2140+ ctxt <- get_context

2141+ let tcTy = foldr mkPi resTy args

2142+ (checked, ty') <- lift $ check ctxt [] tcTy

2143+ mustBeType ctxt checked ty'

2144+ mustNotBeDefined ctxt n

2145+ let ctxt' = addTyDecl n (TCon 0 0) checked ctxt

2146+ set_context ctxt'

2147+ updateAux $ \e -> e { new_tyDecls = RDatatypeDeclInstrs n (map rFunArgToPArg args) : new_tyDecls e }

2148+ returnUnit

2149+ | n == tacN "Prim__DefineDatatype", [defn] <- args

2150+ = do RDefineDatatype n ctors <- reifyRDataDefn defn

2151+ ctxt <- get_context

2152+ tyconTy <- case lookupTyExact n ctxt of

2153+ Just t -> return t

2154+ Nothing -> lift . tfail . Msg $ "Type not previously declared"

2155+ datatypes <- get_datatypes

2156+ case lookupCtxtName n datatypes of

2157+ [] -> return ()

2158+ _ -> lift . tfail . Msg $ show n ++ " is already defined as a datatype."

2159+ -- Prepare the constructors

2160+ ctors' <- mapM (prepareConstructor n) ctors

2161+ ttag <- do ES (ps, aux) str prev <- get

2162+ let i = global_nextname ps

2163+ put $ ES (ps { global_nextname = global_nextname ps + 1 },

2164+ aux)

2165+ str

2166+ prev

2167+ return i

2168+ let ctxt' = addDatatype (Data n ttag tyconTy False (map (\(cn, _, cty) -> (cn, cty)) ctors')) ctxt

2169+ set_context ctxt'

2170+ -- the rest happens in a bit

2171+ updateAux $ \e -> e { new_tyDecls = RDatatypeDefnInstrs n tyconTy ctors' : new_tyDecls e }

2172+ returnUnit

2079 | n == tacN "Prim__AddInstance", [cls, inst] <- args

2173 | n == tacN "Prim__AddInstance", [cls, inst] <- args

2080 = do className <- reifyTTName cls

2174 = do className <- reifyTTName cls

2081 instName <- reifyTTName inst

2175 instName <- reifyTTName inst

2082 updateAux $ \e -> e { new_tyDecls = RAddInstance className instName :

2176 updateAux $ \e -> e { new_tyDecls = RAddInstance className instName :

2083− new_tyDecls e}

2177+ new_tyDecls e }

2084 returnUnit

2178 returnUnit

2085 | n == tacN "Prim__IsTCName", [n] <- args

2179 | n == tacN "Prim__IsTCName", [n] <- args

2086 = do n' <- reifyTTName n

2180 = do n' <- reifyTTName n

@@ -2115,6 +2209,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

2115 aux <- getAux

2209 aux <- getAux

2116 datatypes <- get_datatypes

2210 datatypes <- get_datatypes

2117 env <- get_env

2211 env <- get_env

2212+ g_next <- get_global_nextname

2118

2213

2119 (ctxt', ES (p, aux') _ _) <-

2214 (ctxt', ES (p, aux') _ _) <-

2120 do (ES (current_p, _) _ _) <- get

2215 do (ES (current_p, _) _ _) <- get

@@ -2122,13 +2217,15 @@ runElabAction ist fc env tm ns = do tm' <- eval tm

2122 (do runElabAction ist fc [] script ns

2217 (do runElabAction ist fc [] script ns

2123 ctxt' <- get_context

2218 ctxt' <- get_context

2124 return ctxt')

2219 return ctxt')

2125− ((newProof recH ctxt datatypes goalTT)

2220+ ((newProof recH ctxt datatypes g_next goalTT)

2126 { nextname = nextname current_p })

2221 { nextname = nextname current_p })

2127 set_context ctxt'

2222 set_context ctxt'

2128

2223

2129 let tm_out = getProofTerm (pterm p)

2224 let tm_out = getProofTerm (pterm p)

2130 do (ES (prf, _) s e) <- get

2225 do (ES (prf, _) s e) <- get

2131− let p' = prf { nextname = nextname p }

2226+ let p' = prf { nextname = nextname p

2227+ , global_nextname = global_nextname p

2228+ }

2132 put (ES (p', aux') s e)

2229 put (ES (p', aux') s e)

2133 env' <- get_env

2230 env' <- get_env

2134 (tm, ty, _) <- lift $ recheck ctxt' env (forget tm_out) tm_out

2231 (tm, ty, _) <- lift $ recheck ctxt' env (forget tm_out) tm_out

@@ -2520,6 +2617,44 @@ processTacticDecls info steps =

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

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

2521 in addDeferred ds'

2618 in addDeferred ds'

2522 _ -> return ()

2619 _ -> return ()

2620+ RDatatypeDeclInstrs n impls ->

2621+ do addIBC (IBCDef n)

2622+ updateIState $ \i -> i { idris_implicits = addDef n impls (idris_implicits i) }

2623+ addIBC (IBCImp n)

2624+

2625+ RDatatypeDefnInstrs tyn tyconTy ctors ->

2626+ do let cn (n, _, _) = n

2627+ cimpls (_, impls, _) = impls

2628+ cty (_, _, t) = t

2629+ addIBC (IBCDef tyn)

2630+ mapM_ (addIBC . IBCDef . cn) ctors

2631+ let params = findParams tyn (map cty ctors)

2632+ let typeInfo = TI (map cn ctors) False [] params []

2633+ -- implicit precondition to IBCData is that idris_datatypes on the IState is populated.

2634+ -- otherwise writing the IBC just fails silently!

2635+ updateIState $ \i -> i { idris_datatypes =

2636+ addDef tyn typeInfo (idris_datatypes i) }

2637+ addIBC (IBCData tyn)

2638+

2639+

2640+ ttag <- getName -- from AbsSyntax.hs, really returns a disambiguating Int

2641+

2642+ let metainf = DataMI params

2643+ addIBC (IBCMetaInformation tyn metainf)

2644+ updateContext (setMetaInformation tyn metainf)

2645+

2646+ for_ ctors $ \(cn, impls, _) ->

2647+ do updateIState $ \i -> i { idris_implicits = addDef cn impls (idris_implicits i) }

2648+ addIBC (IBCImp cn)

2649+

2650+ for_ ctors $ \(cn, _, _) -> totcheck (NoFC, cn)

2651+

2652+ case ctors of

2653+ [ctor] -> do setDetaggable (cn ctor); setDetaggable tyn

2654+ addIBC (IBCOpt (cn ctor)); addIBC (IBCOpt tyn)

2655+ _ -> return ()

2656+ -- TODO: inaccessible

2657+

2523 RAddInstance className instName ->

2658 RAddInstance className instName ->

2524 do -- The type class resolution machinery relies on a special

2659 do -- The type class resolution machinery relies on a special

2525 logElab 2 $ "Adding elab script instance " ++ show instName ++

2660 logElab 2 $ "Adding elab script instance " ++ show instName ++

@@ -2581,13 +2716,14 @@ processTacticDecls info steps =

2581 let lhs = addImplPat ist lhs_in

2716 let lhs = addImplPat ist lhs_in

2582 let fc = fileFC "elab_reflected_totality"

2717 let fc = fileFC "elab_reflected_totality"

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

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

2584− case elaborate ctxt (idris_datatypes ist) (sMN 0 "refPatLHS") infP initEState

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

2585 (erun fc (buildTC ist info ELHS [] fname (allNamesIn lhs_in)

2720 (erun fc (buildTC ist info ELHS [] fname (allNamesIn lhs_in)

2586 (infTerm lhs))) of

2721 (infTerm lhs))) of

2587− OK (ElabResult lhs' _ _ _ _ _, _) ->

2722+ OK (ElabResult lhs' _ _ _ _ _ name', _) ->

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

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

2589 -- want to run infinitely many times

2724 -- want to run infinitely many times

2590 let lhs_tm = orderPats (getInferTerm lhs')

2725 let lhs_tm = orderPats (getInferTerm lhs')

2726+ updateIState $ \i -> i { idris_name = name' }

2591 case recheck ctxt [] (forget lhs_tm) lhs_tm of

2727 case recheck ctxt [] (forget lhs_tm) lhs_tm of

2592 OK _ -> return True

2728 OK _ -> return True

2593 err -> return False

2729 err -> return False

src/Idris/Elab/Transform.hs+10−6

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

54 i <- getIState

55 let lhs = addImplPat i lhs_in

56 logElab 5 ("Transform LHS input: " ++ showTmImpls lhs)

57− (ElabResult lhs' dlhs [] ctxt' newDecls highlights, _) <-

57+ (ElabResult lhs' dlhs [] ctxt' newDecls highlights newGName, _) <-

58− tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "transLHS") infP initEState

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

59 (erun fc (buildTC i info ETransLHS [] (sUN "transform")

60 (allNamesIn lhs_in) (infTerm lhs)))

61 setContext ctxt'

62 processTacticDecls info newDecls

63 sendHighlighting highlights

64+ updateIState $ \i -> i { idris_name = newGName }

64 let lhs_tm = orderPats (getInferTerm lhs')

65 let lhs_tm = orderPats (getInferTerm lhs')

65 let lhs_ty = getInferType lhs'

66 let lhs_ty = getInferType lhs'

66 let newargs = pvars i lhs_tm

67 let newargs = pvars i lhs_tm

@@ -73,18 +74,21 @@ elabTransform info fc safe lhs_in@(PApp _ (PRef _ _ tf) _) rhs_in

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

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

74 logElab 5 ("Transform RHS input: " ++ showTmImpls rhs)

75 logElab 5 ("Transform RHS input: " ++ showTmImpls rhs)

76− ((rhs', defer, ctxt', newDecls), _) <-

77+ ((rhs', defer, ctxt', newDecls, newGName), _) <-

77− tclift $ elaborate ctxt (idris_datatypes i) (sMN 0 "transRHS") clhs_ty initEState

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

78 (do pbinds i lhs_tm

79 (do pbinds i lhs_tm

79 setNextName

80 setNextName

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

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

82+ set_global_nextname newGName

81 erun fc $ psolve lhs_tm

83 erun fc $ psolve lhs_tm

82 tt <- get_term

84 tt <- get_term

83 let (rhs', defer) = runState (collectDeferred Nothing [] ctxt tt) []

85 let (rhs', defer) = runState (collectDeferred Nothing [] ctxt tt) []

86+ newGName <- get_global_nextname

84− return (rhs', defer, ctxt', newDecls))

87+ return (rhs', defer, ctxt', newDecls, newGName))

85 setContext ctxt'

88 setContext ctxt'

86 processTacticDecls info newDecls

89 processTacticDecls info newDecls

87 sendHighlighting highlights

90 sendHighlighting highlights

91+ updateIState $ \i -> i { idris_name = newGName }

89 (crhs_tm_in, crhs_ty) <- recheckC_borrowing False False [] fc id [] rhs'

93 (crhs_tm_in, crhs_ty) <- recheckC_borrowing False False [] fc id [] rhs'

90 let crhs_tm = renamepats pnames crhs_tm_in

94 let crhs_tm = renamepats pnames crhs_tm_in

src/Idris/Elab/Type.hs+4−3

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

67 logElab 5 $ show "with methods " ++ show (imp_methods syn)

68 logElab 2 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty

70− (ElabResult tyT' defer is ctxt' newDecls highlights, log) <-

70+ (ElabResult tyT' defer is ctxt' newDecls highlights newGName, log) <-

71− tclift $ elaborate ctxt (idris_datatypes i) n (TType (UVal 0)) initEState

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

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

73 setContext ctxt'

74 processTacticDecls info newDecls

75− sendHighlighting highlights

75+ sendHighlighting highlights

76+ updateIState $ \i -> i { idris_name = newGName }

77 let tyT = patToImp tyT'

78 let tyT = patToImp tyT'

src/Idris/Elab/Utils.hs+63

@@ -331,4 +331,67 @@ checkVisibility fc n minAcc acc ref

331 else return ()

332

333

334+-- | Find the type constructor arguments that are parameters, given a list of constructor types.

335+-- Parameters are names which are unchanged across the structure,

336+-- which appear exactly once in the return type of a constructor

337+-- First, find all applications of the constructor, then check over

338+-- them for repeated arguments

339+findParams :: Name -- ^ the name of the family that we are finding parameters for

340+ -> [Type] -- ^ the declared constructor types

341+ -> [Int]

342+findParams tyn ts =

343+ let allapps = map getDataApp ts

344+ -- do each constructor separately, then merge the results (names

345+ -- may change between constructors)

346+ conParams = map paramPos allapps

347+ in inAll conParams

334

348

349+ where

350+ inAll :: [[Int]] -> [Int]

351+ inAll [] = []

352+ inAll (x : xs) = filter (\p -> all (\ps -> p `elem` ps) xs) x

353+

354+ paramPos [] = []

355+ paramPos (args : rest)

356+ = dropNothing $ keepSame (zip [0..] args) rest

357+ dropNothing [] = []

358+ dropNothing ((x, Nothing) : ts) = dropNothing ts

359+ dropNothing ((x, _) : ts) = x : dropNothing ts

360+ keepSame :: [(Int, Maybe Name)] -> [[Maybe Name]] ->

361+ [(Int, Maybe Name)]

362+ keepSame as [] = as

363+ keepSame as (args : rest) = keepSame (update as args) rest

364+ where

365+ update [] _ = []

366+ update _ [] = []

367+ update ((n, Just x) : as) (Just x' : args)

368+ | x == x' = (n, Just x) : update as args

369+ update ((n, _) : as) (_ : args) = (n, Nothing) : update as args

370+ getDataApp :: Type -> [[Maybe Name]]

371+ getDataApp f@(App _ _ _)

372+ | (P _ d _, args) <- unApply f

373+ = if (d == tyn) then [mParam args args] else []

374+ getDataApp (Bind n (Pi _ t _) sc)

375+ = getDataApp t ++ getDataApp (instantiate (P Bound n t) sc)

376+ getDataApp _ = []

377+ -- keep the arguments which are single names, which don't appear

378+ -- elsewhere

379+ mParam args [] = []

380+ mParam args (P Bound n _ : rest)

381+ | count n args == 1

382+ = Just n : mParam args rest

383+ where count n [] = 0

384+ count n (t : ts)

385+ | n `elem` freeNames t = 1 + count n ts

386+ | otherwise = count n ts

387+ mParam args (_ : rest) = Nothing : mParam args rest

388+

389+-- | Mark a name as detaggable in the global state (should be called

390+-- for type and constructor names of single-constructor datatypes)

391+setDetaggable :: Name -> Idris ()

392+setDetaggable n = do

393+ ist <- getIState

394+ let opt = idris_optimisation ist

395+ case lookupCtxt n opt of

396+ [oi] -> putIState ist { idris_optimisation = addDef n oi { detaggable = True } opt }

397+ _ -> putIState ist { idris_optimisation = addDef n (Optimise [] True) opt }

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

@@ -64,14 +64,15 @@ elabValBind info aspat norm tm_in

64 -- * elaboration as a Type

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

67− (ElabResult tm' defer is ctxt' newDecls highlights, _) <-

67+ (ElabResult tm' defer is ctxt' newDecls highlights newGName, _) <-

68− tclift (elaborate ctxt (idris_datatypes i) (sMN 0 "val") infP initEState

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

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

71 -- Extend the context with new definitions created

72 setContext ctxt'

73 processTacticDecls info newDecls

74 sendHighlighting highlights

75+ updateIState $ \i -> i { idris_name = newGName }

76 let vtm = orderPats (getInferTerm tm')

77 let vtm = orderPats (getInferTerm tm')

src/Idris/Prover.hs+1−1

@@ -85,7 +85,7 @@ assumptionNames e

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

87prove mode opt ctxt lit n ty

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

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

89 idemodePutSExp "start-proof-mode" n

90 (tm, prf) <-

91 if mode

src/Idris/Reflection.hs+19−3

@@ -48,6 +48,10 @@ data RCtorArg = RCtorParameter RFunArg | RCtorField RFunArg deriving Show

49data RDatatype = RDatatype Name [RTyConArg] Raw [(Name, [RCtorArg], Raw)] deriving Show

51+data RConstructorDefn = RConstructor Name [RFunArg] Raw

52+

53+data RDataDefn = RDefineDatatype Name [RConstructorDefn]

54+

51rArgOpts :: RErasure -> [ArgOpt]

55rArgOpts :: RErasure -> [ArgOpt]

52rArgOpts RErased = [InaccessibleArg]

56rArgOpts RErased = [InaccessibleArg]

53rArgOpts _ = []

57rArgOpts _ = []

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

963 Right (TextPart msg)

967 Right (TextPart msg)

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

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

965 | n == reflm "NamePart" =

969 | n == reflm "NamePart" =

966− case runElab initEState (reifyTTName ttn) (initElaborator (sMN 0 "hole") initContext emptyContext Erased) of

970+ case runElab initEState (reifyTTName ttn) (initElaborator (sMN 0 "hole") initContext emptyContext 0 Erased) of

967 Error e -> Left . InternalMsg $

971 Error e -> Left . InternalMsg $

968 "could not reify name term " ++

972 "could not reify name term " ++

969 show ttn ++

973 show ttn ++

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

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

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

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

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

973 | n == reflm "TermPart" =

977 | n == reflm "TermPart" =

974− case runElab initEState (reifyTT tm) (initElaborator (sMN 0 "hole") initContext emptyContext Erased) of

978+ case runElab initEState (reifyTT tm) (initElaborator (sMN 0 "hole") initContext emptyContext 0 Erased) of

975 Error e -> Left . InternalMsg $

979 Error e -> Left . InternalMsg $

976 "could not reify reflected term " ++

980 "could not reify reflected term " ++

977 show tm ++

981 show tm ++

@@ -979,7 +983,7 @@ reifyReportPart (App _ (P (DCon _ _ _) n _) tm)

979 OK (tm', _) -> Right $ TermPart tm'

983 OK (tm', _) -> Right $ TermPart tm'

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

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

981 | n == reflm "RawPart" =

985 | n == reflm "RawPart" =

982− case runElab initEState (reifyRaw tm) (initElaborator (sMN 0 "hole") initContext emptyContext Erased) of

986+ case runElab initEState (reifyRaw tm) (initElaborator (sMN 0 "hole") initContext emptyContext 0 Erased) of

983 Error e -> Left . InternalMsg $

987 Error e -> Left . InternalMsg $

984 "could not reify reflected raw term " ++

988 "could not reify reflected raw term " ++

985 show tm ++

989 show tm ++

@@ -1044,6 +1048,18 @@ reifyFunDefn (App _ (App _ (App _ (P _ n _) (P _ t _)) fnN) clauses)

1044 reifyC tm = fail $ "Couldn't reify " ++ show tm ++ " as a clause."

1048 reifyC tm = fail $ "Couldn't reify " ++ show tm ++ " as a clause."

1045reifyFunDefn tm = fail $ "Couldn't reify " ++ show tm ++ " as a function declaration."

1049reifyFunDefn tm = fail $ "Couldn't reify " ++ show tm ++ " as a function declaration."

1046

1050

1051+reifyRConstructorDefn :: Term -> ElabD RConstructorDefn

1052+reifyRConstructorDefn (App _ (App _ (App _ (P _ n _) cn) args) retTy)

1053+ | n == tacN "Constructor", Just args' <- unList args

1054+ = RConstructor <$> reifyTTName cn <*> mapM reifyRFunArg args' <*> reifyRaw retTy

1055+reifyRConstructorDefn aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RConstructorDefn"

1056+

1057+reifyRDataDefn :: Term -> ElabD RDataDefn

1058+reifyRDataDefn (App _ (App _ (P _ n _) tyn) ctors)

1059+ | n == tacN "DefineDatatype", Just ctors' <- unList ctors

1060+ = RDefineDatatype <$> reifyTTName tyn <*> mapM reifyRConstructorDefn ctors'

1061+reifyRDataDefn aTm = fail $ "Couldn't reify " ++ show aTm ++ " as an RDataDefn"

1062+

1047envTupleType :: Raw

1063envTupleType :: Raw

1048envTupleType

1064envTupleType

1049 = raw_apply (Var pairTy) [ (Var $ reflm "TTName")

1065 = raw_apply (Var pairTy) [ (Var $ reflm "TTName")

test/meta002/DataDef.idrnew file+73

@@ -0,0 +1,73 @@

1+module DataDef

3+foo : Elab ()

4+foo = do declareDatatype $ Declare `{{DataDef.N}} [MkFunArg `{{n}} `(Nat) Explicit NotErased] `(Type)

5+ defineDatatype $ DefineDatatype `{{DataDef.N}} [

6+ Constructor `{{MkN}} [MkFunArg `{{x}} `(Nat) Implicit NotErased] (RApp (Var `{{DataDef.N}}) (Var `{{x}})),

7+ Constructor `{{MkN'}} [MkFunArg `{{x}} `(Nat) Explicit NotErased] (RApp (Var `{{DataDef.N}}) (RApp (Var `{S}) (Var `{{x}})))

8+ ]

9+%runElab foo

10+

11+one : N 1

12+one = MkN

13+

14+two : N 2

15+two = MkN' 1

16+

17+

18+-- mutual

19+-- data U : Type where

20+-- Base : U

21+-- Pi : (code : U) -> (el code -> U) -> U

22+-- el : U -> Type

23+-- el Base = Bool

24+-- el (Pi code body) = (x : el code) -> el (body x)

25+

26+

27+

28+mkU : Elab ()

29+mkU = do let U = `{{DataDef.U}}

30+ let el = `{{DataDef.el}}

31+ declareDatatype $ Declare U [] `(Type)

32+ declareType $ Declare el [MkFunArg `{{code}} (Var U) Explicit NotErased] `(Type)

33+ defineDatatype $ DefineDatatype U [

34+ Constructor `{{Base}} [] (Var U),

35+ Constructor `{{Pi}}

36+ [MkFunArg `{{code}} (Var U) Explicit NotErased,

37+ MkFunArg `{{body}} `(~(RApp (Var el) (Var `{{code}})) -> ~(Var U)) Explicit NotErased]

38+ (Var U)

39+ ]

40+ defineFunction $ DefineFun el [

41+ MkFunClause (RBind `{{code}} (PVar (Var U))

42+ (RBind `{{body}} (PVar `(~(RApp (Var el) (Var `{{code}})) -> ~(Var U)))

43+ (RApp (Var el)

44+ (RApp (RApp (Var `{{DataDef.Pi}})

45+ (Var `{{code}}))

46+ (Var `{{body}})))))

47+ (RBind `{{code}} (PVar (Var U))

48+ (RBind `{{body}} (PVar `(~(RApp (Var el) (Var `{{code}})) -> ~(Var U)))

49+ (RBind `{{x}} (Pi (RApp (Var el) (Var `{{code}})) `(Type))

50+ (RApp (Var el) (RApp (Var `{{body}}) (Var `{{x}})))))),

51+ MkFunClause (RApp (Var el) (Var `{{DataDef.Base}})) `(Bool)

52+

53+ ]

54+

55+%runElab mkU

56+

57+tt : el Base

58+tt = True

59+

60+fun : el (Pi Base (\x => if x then Base else Pi Base (const Base)))

61+fun = \x => (case x of

62+ False => \y => False

63+ True => False)

64+

65+

66+nope : Elab ()

67+nope = defineDatatype $ DefineDatatype `{Either} [

68+ Constructor `{{Middle}} [ MkFunArg `{{x}} `(Type) Implicit NotErased

69+ , MkFunArg `{{y}} `(Type) Implicit NotErased

70+ ] `(Either ~(Var `{{x}}) ~(Var `{{y}}))

71+ ]

72+%runElab nope

73+

test/meta002/expected+3

@@ -1,3 +1,6 @@

1+DataDef.idr:72:1-9:

2+While running an elaboration script, the following error occurred:

3+Prelude.Either.Either is already defined as a datatype.

1Tacs.idr:298:15:

4Tacs.idr:298:15:

2When checking right hand side of testElab3 with expected type

5When checking right hand side of testElab3 with expected type

3 DPair Ty (Tm [])

6 DPair Ty (Tm [])

test/meta002/run+1

@@ -1,4 +1,5 @@

1#!/usr/bin/env bash

2+${IDRIS:-idris} $@ -p pruviloj --nocolour --check --consolewidth 70 DataDef.idr

2${IDRIS:-idris} $@ -p pruviloj --nocolour --check --consolewidth 70 Tacs.idr

3${IDRIS:-idris} $@ -p pruviloj --nocolour --check --consolewidth 70 Tacs.idr

3${IDRIS:-idris} $@ -p pruviloj --nocolour --check --consolewidth 70 AgdaStyleReflection.idr

4${IDRIS:-idris} $@ -p pruviloj --nocolour --check --consolewidth 70 AgdaStyleReflection.idr

4# Disabled due to excess memory consumption

5# Disabled due to excess memory consumption