@@ -52,6 +52,9 @@ data ElabResult =
5252 , resultTyDecls :: [RDeclInstructions]
5353 -- ^ Meta-info about the new type declarations
5454 , resultHighlighting :: [(FC, OutputAnnotation)]
55+ -- ^ Saved highlights from elaboration
56+ , resultName :: Int
57+ -- ^ The new global name counter
5558 }
5659
5760
@@ -122,9 +125,10 @@ build ist info emode opts fn tm
122125 ctxt <- get_context
123126 let (tm, ds) = runState (collectDeferred (Just fn) (map fst is) ctxt tt) []
124127 log <- getLog
128+ g_nextname <- get_global_nextname
125129 if log /= ""
126− then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights)
127− else 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)
131+ else return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)
128132 where pattern = emode == ELHS
129133 tydecl = emode == ETyDecl
130134
@@ -166,9 +170,10 @@ buildTC ist info emode opts fn ns tm
166170 ctxt <- get_context
167171 let (tm, ds) = runState (collectDeferred (Just fn) (map fst is) ctxt tt) []
168172 log <- getLog
173+ g_nextname <- get_global_nextname
169174 if (log /= "")
170− then trace log $ return (ElabResult tm ds (map snd is) ctxt impls highlights)
171− else 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)
176+ else return (ElabResult tm ds (map snd is) ctxt impls highlights g_nextname)
172177 where pattern = emode == ELHS
173178
174179-- return whether arguments of the given constructor name can be
@@ -1158,9 +1163,10 @@ elab ist info emode opts fn tm
11581163 -- capturing lexically available variables in the quoted term.
11591164 ctxt <- get_context
11601165 datatypes <- get_datatypes
1166+ g_nextname <- get_global_nextname
11611167 saveState
11621168 updatePS (const .
1163− newProof (sMN 0 "q") ctxt datatypes $
1169+ newProof (sMN 0 "q") ctxt datatypes g_nextname $
11641170 P Ref (reflm "TT") Erased)
11651171
11661172 -- Re-add the unquotes, letting Idris infer the (fictional)
@@ -1839,11 +1845,74 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
18391845 updateAux $ \e -> e { new_tyDecls = RClausesInstrs n clauses'' : new_tyDecls e}
18401846 return ()
18411847
1848+
18421849 checkClosed :: Raw -> Elab' aux (Term, Type)
18431850 checkClosed tm = do ctxt <- get_context
18441851 (val, ty) <- lift $ check ctxt [] tm
18451852 return $! (finalise val, finalise ty)
18461853
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+
18471916 -- | Do a step in the reflected elaborator monad. The input is the
18481917 -- step, the output is the (reflected) term returned.
18491918 runTacTm :: Term -> ElabD Term
@@ -2052,20 +2121,10 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
20522121 | n == tacN "Prim__DeclareType", [decl] <- args
20532122 = do (RDeclare n args res) <- reifyTyDecl decl
20542123 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
20592125 (checked, ty') <- lift $ check ctxt [] rty
2060− case normaliseAll ctxt [] (finalise ty') of
2061− UType _ -> return ()
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 ()
2126+ mustBeType ctxt checked ty'
2127+ mustNotBeDefined ctxt n
20692128 let decl = TyDecl Ref checked
20702129 ctxt' = addCtxtDef n decl ctxt
20712130 set_context ctxt'
@@ -2076,11 +2135,46 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
20762135 = do defn <- reifyFunDefn decl
20772136 defineFunction defn
20782137 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
20792173 | n == tacN "Prim__AddInstance", [cls, inst] <- args
20802174 = do className <- reifyTTName cls
20812175 instName <- reifyTTName inst
20822176 updateAux $ \e -> e { new_tyDecls = RAddInstance className instName :
2083− new_tyDecls e}
2177+ new_tyDecls e }
20842178 returnUnit
20852179 | n == tacN "Prim__IsTCName", [n] <- args
20862180 = do n' <- reifyTTName n
@@ -2115,6 +2209,7 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
21152209 aux <- getAux
21162210 datatypes <- get_datatypes
21172211 env <- get_env
2212+ g_next <- get_global_nextname
21182213
21192214 (ctxt', ES (p, aux') _ _) <-
21202215 do (ES (current_p, _) _ _) <- get
@@ -2122,13 +2217,15 @@ runElabAction ist fc env tm ns = do tm' <- eval tm
21222217 (do runElabAction ist fc [] script ns
21232218 ctxt' <- get_context
21242219 return ctxt')
2125− ((newProof recH ctxt datatypes goalTT)
2220+ ((newProof recH ctxt datatypes g_next goalTT)
21262221 { nextname = nextname current_p })
21272222 set_context ctxt'
21282223
21292224 let tm_out = getProofTerm (pterm p)
21302225 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+ }
21322229 put (ES (p', aux') s e)
21332230 env' <- get_env
21342231 (tm, ty, _) <- lift $ recheck ctxt' env (forget tm_out) tm_out
@@ -2520,6 +2617,44 @@ processTacticDecls info steps =
25202617 let ds' = map (\(n, (i, top, t, ns)) -> (n, (i, top, t, ns, True, True))) ds
25212618 in addDeferred ds'
25222619 _ -> 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+
25232658 RAddInstance className instName ->
25242659 do -- The type class resolution machinery relies on a special
25252660 logElab 2 $ "Adding elab script instance " ++ show instName ++
@@ -2581,13 +2716,14 @@ processTacticDecls info steps =
25812716 let lhs = addImplPat ist lhs_in
25822717 let fc = fileFC "elab_reflected_totality"
25832718 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
25852720 (erun fc (buildTC ist info ELHS [] fname (allNamesIn lhs_in)
25862721 (infTerm lhs))) of
2587− OK (ElabResult lhs' _ _ _ _ _, _) ->
2722+ OK (ElabResult lhs' _ _ _ _ _ name', _) ->
25882723 do -- not recursively calling here, because we don't
25892724 -- want to run infinitely many times
25902725 let lhs_tm = orderPats (getInferTerm lhs')
2726+ updateIState $ \i -> i { idris_name = name' }
25912727 case recheck ctxt [] (forget lhs_tm) lhs_tm of
25922728 OK _ -> return True
25932729 err -> return False