ab498e9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

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

commitab498e9fb2a77071f4ab338242acb9b90e2f227e authorDavid Christiansen <david@davidchristiansen.dk> dateThu 21 Mar 2013, 18:22 (14 years ago) parent161ef3d

5 files changed+71−53

compare with master

unifiedsplit

src/Idris/AbsSyntax.hs+3 src/Idris/AbsSyntaxTree.hs+6−2 src/Idris/ElabDecls.hs+19−16 src/Idris/Parser.hs+2 src/Idris/REPL.hs+41−35

src/Idris/AbsSyntax.hs+3

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

5252addHdr :: String -> Idris ()

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

5454

55+addLangExt :: LanguageExt -> Idris ()

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

57+

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

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

5760

src/Idris/AbsSyntaxTree.hs+6−2

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

4343

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

4545

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

47+

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

4749-- without typechecking).

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

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

8890 default_total :: Bool,

8991 ibc_write :: [IBCWrite],

9092 compiled_so :: Maybe String,

91− idris_dynamic_libs :: [DynamicLib]

93+ idris_dynamic_libs :: [DynamicLib],

94+ idris_language_extensions :: [LanguageExt]

9295 }

9396

9497data SizeChange = Smaller | Same | Bigger | Unknown

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

140143 emptyContext emptyContext emptyContext emptyContext

141144 emptyContext emptyContext emptyContext emptyContext

142145 [] "" defaultOpts 6 [] [] [] [] [] [] [] [] []

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

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

144147

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

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

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

227230 | FOVM String

228231 | UseTarget Target

229232 | OutputTy OutputType

233+ | Extension LanguageExt

230234 deriving (Show, Eq)

231235

232236-- Parsed declarations

src/Idris/ElabDecls.hs+19−16

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

191191-- | Elaborate a type provider

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

193193elabProvider info syn fc n ty tm

194− = do let expected = providerTy fc ty

195− let using = unProv fc tm

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

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

198− " as " ++ show using

199− i <- getIState

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

201− ctxt <- getContext

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

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

204− let et' = normaliseAll ctxt [] et

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

206− rhs <- execute e''

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

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

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

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."

198+ else do let expected = providerTy fc ty

199+ let using = unProv fc tm

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

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

202+ " as " ++ show using

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

204+ ctxt <- getContext

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

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

207+ let et' = normaliseAll ctxt [] et

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

209+ rhs <- execute e''

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

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

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

210213

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

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

src/Idris/Parser.hs+2

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

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

15011501 return [PDirective (do addIBC (IBCDyLib lib)

15021502 addDyLib lib)])

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

1504+ return [PDirective (addLangExt TypeProviders)])

15031505

15041506pProvider :: SyntaxInfo -> IParser [PDecl]

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

src/Idris/REPL.hs+41−35

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

458458

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

460460parseArgs [] = []

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

496497

497498helphead =

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

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

527528 xs -> last xs

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

529530 putIState (i { default_total = True })

531+ mapM_ addLangExt (opt getLanguageExt opts)

530532 setREPL runrepl

531533 setQuiet quiet

532534 setVerbose runrepl

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

626628getOutputTy (OutputTy t) = Just t

627629getOutputTy _ = Nothing

628630

631+getLanguageExt :: Opt -> Maybe LanguageExt

632+getLanguageExt (Extension e) = Just e

633+getLanguageExt _ = Nothing

634+

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

630636opt = mapMaybe

631637