ab498e9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add syntax for language extensions and turn off type providers by default

ab498e9David Christiansen14 years ago

src/Idris/AbsSyntax.hs+3

compare with master

unifiedsplit

@@ -52,6 +52,9 @@ addDyLib lib = do i <- getIState

52addHdr :: String -> Idris ()

53addHdr f = do i <- getIState; putIState $ i { idris_hdrs = f : idris_hdrs i }

55+addLangExt :: LanguageExt -> Idris ()

56+addLangExt TypeProviders = do i <- getIState ; putIState $ i { idris_language_extensions = [TypeProviders] }

57+

55totcheck :: (FC, Name) -> Idris ()

58totcheck :: (FC, Name) -> Idris ()

56totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }

59totcheck n = do i <- getIState; putIState $ i { idris_totcheck = idris_totcheck i ++ [n] }

src/Idris/AbsSyntaxTree.hs+6−2

@@ -43,6 +43,8 @@ data IOption = IOption { opt_logLevel :: Int,

44defaultOpts = IOption 0 False False True False False True True False ViaC Executable "" [] []

46+data LanguageExt = TypeProviders deriving (Show, Eq, Read, Ord)

47+

46-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e

48-- TODO: Add 'module data' to IState, which can be saved out and reloaded quickly (i.e

47-- without typechecking).

49-- without typechecking).

48-- This will include all the functions and data declarations, plus fixity declarations

50-- This will include all the functions and data declarations, plus fixity declarations

@@ -88,7 +90,8 @@ data IState = IState {

88 default_total :: Bool,

90 default_total :: Bool,

89 ibc_write :: [IBCWrite],

91 ibc_write :: [IBCWrite],

90 compiled_so :: Maybe String,

92 compiled_so :: Maybe String,

91− idris_dynamic_libs :: [DynamicLib]

93+ idris_dynamic_libs :: [DynamicLib],

94+ idris_language_extensions :: [LanguageExt]

92 }

95 }

94data SizeChange = Smaller | Same | Bigger | Unknown

97data SizeChange = Smaller | Same | Bigger | Unknown

@@ -140,7 +143,7 @@ idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext

140 emptyContext emptyContext emptyContext emptyContext

143 emptyContext emptyContext emptyContext emptyContext

141 emptyContext emptyContext emptyContext emptyContext

144 emptyContext emptyContext emptyContext emptyContext

142 [] "" defaultOpts 6 [] [] [] [] [] [] [] [] []

145 [] "" defaultOpts 6 [] [] [] [] [] [] [] [] []

143− [] Nothing Nothing [] [] [] Hidden False [] Nothing []

146+ [] Nothing Nothing [] [] [] Hidden False [] Nothing [] []

144

147

145-- | The monad for the main REPL - reading and processing files and updating

148-- | The monad for the main REPL - reading and processing files and updating

146-- global state (hence the IO inner monad).

149-- global state (hence the IO inner monad).

@@ -227,6 +230,7 @@ data Opt = Filename String

227 | FOVM String

230 | FOVM String

228 | UseTarget Target

231 | UseTarget Target

229 | OutputTy OutputType

232 | OutputTy OutputType

233+ | Extension LanguageExt

230 deriving (Show, Eq)

234 deriving (Show, Eq)

231

235

232-- Parsed declarations

236-- Parsed declarations

src/Idris/ElabDecls.hs+19−16

@@ -191,22 +191,25 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)

191-- | Elaborate a type provider

192elabProvider :: ElabInfo -> SyntaxInfo -> FC -> Name -> PTerm -> PTerm -> Idris ()

193elabProvider info syn fc n ty tm

194+ = do i <- getIState

195+ if not (TypeProviders `elem` idris_language_extensions i)

196+ then fail $ "Failed to define type provider \"" ++ show n ++

197+ "\".\nYou must turn on TypeProviders extension."

194− = do let expected = providerTy fc ty

198+ else do let expected = providerTy fc ty

195− let using = unProv fc tm

199+ let using = unProv fc tm

196− logLvl 1 $ "** Providing " ++

200+ logLvl 1 $ "** Providing " ++

197− show n ++ " : " ++ show expected ++

201+ show n ++ " : " ++ show expected ++

198− " as " ++ show using

202+ " as " ++ show using

199− i <- getIState

200− (e', et) <- elabVal toplevel False using

203+ (e', et) <- elabVal toplevel False using

201− ctxt <- getContext

204+ ctxt <- getContext

202− let e'' = normaliseAll ctxt [] e'

205+ let e'' = normaliseAll ctxt [] e'

203− logLvl 1 $ "Term is " ++ show e''

206+ logLvl 1 $ "Term is " ++ show e''

204− let et' = normaliseAll ctxt [] et

207+ let et' = normaliseAll ctxt [] et

205− elabType info syn "" fc [] n ty

208+ elabType info syn "" fc [] n ty

206− rhs <- execute e''

209+ rhs <- execute e''

207− elabClauses info fc [] n [PClause fc n (PRef fc $ n) [] (delab i rhs) []]

210+ elabClauses info fc [] n [PClause fc n (PRef fc $ n) [] (delab i rhs) []]

208− logLvl 1 $ "** Elaborated: " ++ show e' ++ " :as: " ++ show et

211+ logLvl 1 $ "** Elaborated: " ++ show e' ++ " :as: " ++ show et

209− logLvl 1 $ "** Evaluated: " ++ show rhs ++ " :as: " ++ show et'

212+ logLvl 1 $ "** Evaluated: " ++ show rhs ++ " :as: " ++ show et'

210

213

211elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->

214elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->

212 PTerm -> String -> Name -> PTerm -> Idris ()

215 PTerm -> String -> Name -> PTerm -> Idris ()

src/Idris/Parser.hs+2

@@ -1500,6 +1500,8 @@ pDirective syn = try (do lchar '%'; reserved "lib"; lib <- strlit;

1500 <|> try (do lchar '%'; reserved "dynamic"; lib <- strlit;

1501 return [PDirective (do addIBC (IBCDyLib lib)

1502 addDyLib lib)])

1503+ <|> try (do lchar '%'; reserved "language"; ext <- reserved "TypeProviders";

1504+ return [PDirective (addLangExt TypeProviders)])

1503

1505

1504pProvider :: SyntaxInfo -> IParser [PDecl]

1506pProvider :: SyntaxInfo -> IParser [PDecl]

1505pProvider syn = do lchar '%'; reserved "provide";

1507pProvider syn = do lchar '%'; reserved "provide";

src/Idris/REPL.hs+41−35

@@ -458,41 +458,42 @@ parseTarget _ = error "unknown target" -- FIXME: partial function

458

459parseArgs :: [String] -> [Opt]

460parseArgs [] = []

461−parseArgs ("--quiet":ns) = Quiet : (parseArgs ns)

461+parseArgs ("--quiet":ns) = Quiet : (parseArgs ns)

462−parseArgs ("--log":lvl:ns) = OLogging (read lvl) : (parseArgs ns)

462+parseArgs ("--log":lvl:ns) = OLogging (read lvl) : (parseArgs ns)

463−parseArgs ("--noprelude":ns) = NoPrelude : (parseArgs ns)

463+parseArgs ("--noprelude":ns) = NoPrelude : (parseArgs ns)

464−parseArgs ("--check":ns) = NoREPL : (parseArgs ns)

464+parseArgs ("--check":ns) = NoREPL : (parseArgs ns)

465−parseArgs ("-o":n:ns) = NoREPL : Output n : (parseArgs ns)

465+parseArgs ("-o":n:ns) = NoREPL : Output n : (parseArgs ns)

466−parseArgs ("-no":n:ns) = NoREPL : NewOutput n : (parseArgs ns)

466+parseArgs ("-no":n:ns) = NoREPL : NewOutput n : (parseArgs ns)

467−parseArgs ("--typecase":ns) = TypeCase : (parseArgs ns)

467+parseArgs ("--typecase":ns) = TypeCase : (parseArgs ns)

468−parseArgs ("--typeintype":ns) = TypeInType : (parseArgs ns)

468+parseArgs ("--typeintype":ns) = TypeInType : (parseArgs ns)

469−parseArgs ("--total":ns) = DefaultTotal : (parseArgs ns)

469+parseArgs ("--total":ns) = DefaultTotal : (parseArgs ns)

470−parseArgs ("--partial":ns) = DefaultPartial : (parseArgs ns)

470+parseArgs ("--partial":ns) = DefaultPartial : (parseArgs ns)

471−parseArgs ("--warnpartial":ns) = WarnPartial : (parseArgs ns)

471+parseArgs ("--warnpartial":ns) = WarnPartial : (parseArgs ns)

472−parseArgs ("--nocoverage":ns) = NoCoverage : (parseArgs ns)

472+parseArgs ("--nocoverage":ns) = NoCoverage : (parseArgs ns)

473−parseArgs ("--errorcontext":ns) = ErrContext : (parseArgs ns)

473+parseArgs ("--errorcontext":ns) = ErrContext : (parseArgs ns)

474−parseArgs ("--help":ns) = Usage : (parseArgs ns)

474+parseArgs ("--help":ns) = Usage : (parseArgs ns)

475−parseArgs ("--link":ns) = ShowLibs : (parseArgs ns)

475+parseArgs ("--link":ns) = ShowLibs : (parseArgs ns)

476−parseArgs ("--libdir":ns) = ShowLibdir : (parseArgs ns)

476+parseArgs ("--libdir":ns) = ShowLibdir : (parseArgs ns)

477−parseArgs ("--include":ns) = ShowIncs : (parseArgs ns)

477+parseArgs ("--include":ns) = ShowIncs : (parseArgs ns)

478−parseArgs ("--version":ns) = Ver : (parseArgs ns)

478+parseArgs ("--version":ns) = Ver : (parseArgs ns)

479−parseArgs ("--verbose":ns) = Verbose : (parseArgs ns)

479+parseArgs ("--verbose":ns) = Verbose : (parseArgs ns)

480−parseArgs ("--ibcsubdir":n:ns) = IBCSubDir n : (parseArgs ns)

480+parseArgs ("--ibcsubdir":n:ns) = IBCSubDir n : (parseArgs ns)

481−parseArgs ("-i":n:ns) = ImportDir n : (parseArgs ns)

481+parseArgs ("-i":n:ns) = ImportDir n : (parseArgs ns)

482−parseArgs ("--warn":ns) = WarnOnly : (parseArgs ns)

482+parseArgs ("--warn":ns) = WarnOnly : (parseArgs ns)

483−parseArgs ("--package":n:ns) = Pkg n : (parseArgs ns)

483+parseArgs ("--package":n:ns) = Pkg n : (parseArgs ns)

484−parseArgs ("-p":n:ns) = Pkg n : (parseArgs ns)

484+parseArgs ("-p":n:ns) = Pkg n : (parseArgs ns)

485−parseArgs ("--build":n:ns) = PkgBuild n : (parseArgs ns)

485+parseArgs ("--build":n:ns) = PkgBuild n : (parseArgs ns)

486−parseArgs ("--install":n:ns) = PkgInstall n : (parseArgs ns)

486+parseArgs ("--install":n:ns) = PkgInstall n : (parseArgs ns)

487−parseArgs ("--clean":n:ns) = PkgClean n : (parseArgs ns)

487+parseArgs ("--clean":n:ns) = PkgClean n : (parseArgs ns)

488−parseArgs ("--bytecode":n:ns) = NoREPL : BCAsm n : (parseArgs ns)

488+parseArgs ("--bytecode":n:ns) = NoREPL : BCAsm n : (parseArgs ns)

489−parseArgs ("--fovm":n:ns) = NoREPL : FOVM n : (parseArgs ns)

489+parseArgs ("--fovm":n:ns) = NoREPL : FOVM n : (parseArgs ns)

490−parseArgs ("-S":ns) = OutputTy Raw : (parseArgs ns)

490+parseArgs ("-S":ns) = OutputTy Raw : (parseArgs ns)

491−parseArgs ("-c":ns) = OutputTy Object : (parseArgs ns)

491+parseArgs ("-c":ns) = OutputTy Object : (parseArgs ns)

492−parseArgs ("--dumpdefuns":n:ns) = DumpDefun n : (parseArgs ns)

492+parseArgs ("--dumpdefuns":n:ns) = DumpDefun n : (parseArgs ns)

493−parseArgs ("--dumpcases":n:ns) = DumpCases n : (parseArgs ns)

493+parseArgs ("--dumpcases":n:ns) = DumpCases n : (parseArgs ns)

494−parseArgs ("--target":n:ns) = UseTarget (parseTarget n) : (parseArgs ns)

494+parseArgs ("--target":n:ns) = UseTarget (parseTarget n) : (parseArgs ns)

495+parseArgs ("-XTypeProviders":ns) = Extension TypeProviders : (parseArgs ns)

495−parseArgs (n:ns) = Filename n : (parseArgs ns)

496+parseArgs (n:ns) = Filename n : (parseArgs ns)

496

497

497helphead =

498helphead =

498 [ (["Command"], "Arguments", "Purpose", ""),

499 [ (["Command"], "Arguments", "Purpose", ""),

@@ -527,6 +528,7 @@ idrisMain opts =

527 xs -> last xs

528 xs -> last xs

528 when (DefaultTotal `elem` opts) $ do i <- getIState

529 when (DefaultTotal `elem` opts) $ do i <- getIState

529 putIState (i { default_total = True })

530 putIState (i { default_total = True })

531+ mapM_ addLangExt (opt getLanguageExt opts)

530 setREPL runrepl

532 setREPL runrepl

531 setQuiet quiet

533 setQuiet quiet

532 setVerbose runrepl

534 setVerbose runrepl

@@ -626,6 +628,10 @@ getOutputTy :: Opt -> Maybe OutputType

626getOutputTy (OutputTy t) = Just t

628getOutputTy (OutputTy t) = Just t

627getOutputTy _ = Nothing

629getOutputTy _ = Nothing

628

630

631+getLanguageExt :: Opt -> Maybe LanguageExt

632+getLanguageExt (Extension e) = Just e

633+getLanguageExt _ = Nothing

634+

629opt :: (Opt -> Maybe a) -> [Opt] -> [a]

635opt :: (Opt -> Maybe a) -> [Opt] -> [a]

630opt = mapMaybe

636opt = mapMaybe

631

637